时间戳

首页 > 解决方案 > 枚举集合元素的归纳谓词

isabelle - 枚举集合元素的归纳谓词

问题描述

是否可以使以下示例起作用？

inductive elems where
  "x |∈| xs ⟹
   elems xs x"

code_pred [show_modes] elems .

values "{x. elems {|1::nat,2,3|} x}"

标签： isabelle

解决方案

默认情况下，谓词编译器对有限集和成员运算符一无所知|∈|。但是，如果您添加以下代码段，则它可以工作。

lemma fmember_code_predI [code_pred_intro]:
  "x |∈| xs" if "Predicate_Compile.contains (fset xs) x"
  using that by(simp add: Predicate_Compile.contains_def fmember.rep_eq)

code_pred fmember
  by(simp add: Predicate_Compile.contains_def fmember.rep_eq)

这就是它起作用的原因：常量Predicate_Compile.contains实现了普通集合的枚举，谓词编译器知道它。具有属性的引理code_pred_intro告诉谓词编译器将成员资格fset视为好像它被定义为以引理语句作为引入规则的归纳谓词。在code_pred命令本身，您必须证明相应的排除规则。这两个规则（引入规则和排除规则）足以让谓词编译器进行模态分析并编译方程并证明它们是正确的。

您甚至不需要定义自己的 predicate elems。直接加入fset作品：

values "{x. x |∈| {|1::nat,2,3|}}"

推荐阅读