イザベルのプライムの定義

Question

私はイザベルのチュートリアルに従っています。 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 

いますか？

おかげで、 ペドロ

Answer 1

あなたがその定義で普遍数量詞を持っています。 Isabelleは無限に多くの値を持つ型（この場合は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}の範囲です。 （あなたは素数よりも大きい数で除算をチェックする必要はありません）