總理在伊莎貝爾的定義

我遵循伊莎貝爾教程。在第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

總理在伊莎貝爾的定義

回答

相關問題