Definition von Prime in Isabelle

Question

Ich folge dem Isabelle Tutorial. Auf Seite 25 bezieht es sich auf eine Definition einer Primzahl. Ich schrieb es so:

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

die von Isabelle akzeptiert wird. Aber wenn ich versuche

value "prime (Suc 0)" 

es gibt die Fehler

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 

Was mache ich falsch?

Danke, Pedro

Answer 1

Sie haben eine Allquantor in dieser Definition. Isabelle kann unmöglich ein Prädikat mit einem universellen Quantifizierer auf einem Typ mit unendlich vielen Werten (in diesem Fall) auswerten, und das ist, was diese etwas kryptische Fehlermeldung sagt: ist nicht von Sorte enum. enum ist eine Typklasse, die im Wesentlichen angibt, dass es eine berechenbare endliche Liste gibt, die alle Werte des Typs enthält.

Wenn Sie Ihre prime-Funktion mit dem Codegenerator auswerten möchten, müssen Sie entweder Ihre Definition in eine ausführbare Datei ändern oder eine Code-Gleichung angeben, die anzeigt, dass sie äquivalent zu etwas berechenbarem ist, z. wie folgt aus:

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" *) 

Der Grund, warum diese ausführbar ist, dass der Allquantor ist begrenzt; es erstreckt sich über die endliche Menge {1..p}. (Sie müssen die Teilbarkeit nicht durch Zahlen überprüfen, die größer als die angenommene Primzahl sind)