总理在伊莎贝尔的定义

我遵循伊莎贝尔教程。在第25页，它引用了素数的定义。我这样写：总理在伊莎贝尔的定义

definition prime :: "nat ⇒ bool" where "prime p ≡ 1 < p ∧ (∀m. m dvd p ⟶ m = 1 ∨ m = p)"

这被伊莎贝尔接受。但是，当我尝试

value "prime (Suc 0)"

它给人的错误

Wellsortedness error 
(in code equation prime ?p ≡ 
        ord_nat_inst.less_nat one_nat_inst.one_nat ?p ∧ 
        (∀m. m dvd ?p ⟶ 
         equal_nat_inst.equal_nat m one_nat_inst.one_nat ∨ 
         equal_nat_inst.equal_nat m ?p), 
with dependency "Pure.dummy_pattern" -> "prime"): 
Type nat not of sort enum 
No type arity nat :: enum

我在做什么错？

感谢，佩德罗

来源

2016-12-01 Pedro

你必须在定义中的全称量词。伊莎贝尔不可能评估一个谓词，它涉及一个具有无限多值的类型（在这种情况下为nat），并且这是一个有点神秘的错误信息：nat不是enum。 enum是一个类型类，基本上规定有一个包含所有类型值的可计算有限列表。

如果您想用代码生成器来评估您的prime函数，您需要将您的定义更改为可执行文件或提供代码方程，以表明它等同于可计算的内容，例如，像这样：

lemma prime_code [code]: 
    "prime p = (1 < p ∧ (∀m∈{1..p}. m dvd p ⟶ m = 1 ∨ m = p))" 
proof safe 
    assume p: "p > 1" "∀m∈{1..p}. m dvd p ⟶ m = 1 ∨ m = p" 
    show "prime p" unfolding prime_def 
    proof (intro conjI allI impI) 
    fix m assume m: "m dvd p" 
    with p have "m ≠ 0" by (intro notI) simp 
    moreover from p m have "m ≤ p" by (simp add: dvd_imp_le) 
    ultimately show "m = 1 ∨ m = p" using p m by auto 
    qed fact+ 
qed (auto simp: prime_def) 

value "prime 5" 
(* "True" :: "bool" *)

之所以这样，是可执行文件的全称量词是界;它范围在有限集{1..p}。（你不需要通过数字大于假定的素数来检查可分性）

来源

2016-12-01 15:22:24

总理在伊莎贝尔的定义

回答

相关问题