Definition of Prime in Isabelle

Question

I am following the Isabelle Tutorial. On page 25 it refers a definition of a prime number. I wrote it so:

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

which is accepted by Isabelle. But when I try

value "prime (Suc 0)"

it gives the error

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

What am I doing wrong?

Answer 1

You have a universal quantifier in that definition. Isabelle cannot possibly evaluate a predicate involving a universal quantifier on a type with infinitely many values (in this case nat), and that is what this somewhat cryptic error message says: nat is not of sort enum. enum is a type class that essentially states that there is a computable finite list containing all the values of the type.

If you want to evalue your prime function with the code generator, you either need to change your definition to something executable or provide a code equation that shows that it is equivalent to something computable, e.g. like this:

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

The reason why this is executable is that the universal quantifier is bounded; it ranges over the finite set {1..p}. (You don't need to check for divisibility by numbers greater than the supposed prime)