Theory Peano_Axioms

section ‹Peano's axioms for Natural Numbers›

theory Peano_Axioms
  imports Main
begin

locale peano =  ― ‹or: ⬚‹class››
  fixes zero :: 'a
  fixes succ :: "'a ⇒ 'a"
  assumes succ_neq_zero [simp]: "succ m ≠ zero"
  assumes succ_inject [simp]: "succ m = succ n ⟷ m = n"
  assumes induct [case_names zero succ, induct type: 'a]:
    "P zero ⟹ (⋀n. P n ⟹ P (succ n)) ⟹ P n"
begin

lemma zero_neq_succ [simp]: "zero ≠ succ m"
  by (rule succ_neq_zero [symmetric])


text ‹┉ Primitive recursion as a (functional) relation -- polymorphic!›

inductive Rec :: "'b ⇒ ('a ⇒ 'b ⇒ 'b) ⇒ 'a ⇒ 'b ⇒ bool"
  for e :: 'b and r :: "'a ⇒ 'b ⇒ 'b"
where
  Rec_zero: "Rec e r zero e"
| Rec_succ: "Rec e r m n ⟹ Rec e r (succ m) (r m n)"

lemma Rec_functional: "∃!y::'b. Rec e r x y" for x :: 'a
proof -
  let ?R = "Rec e r"
  show ?thesis
  proof (induct x)
    case zero
    show "∃!y. ?R zero y"
    proof
      show "?R zero e" ..
      show "y = e" if "?R zero y" for y
        using that by cases simp_all
    qed
  next
    case (succ m)
    from ‹∃!y. ?R m y›
    obtain y where y: "?R m y" and yy': "⋀y'. ?R m y' ⟹ y = y'"
      by blast
    show "∃!z. ?R (succ m) z"
    proof
      from y show "?R (succ m) (r m y)" ..
    next
      fix z
      assume "?R (succ m) z"
      then obtain u where "z = r m u" and "?R m u"
        by cases simp_all
      with yy' show "z = r m y"
        by (simp only:)
    qed
  qed
qed


text ‹┉ The recursion operator -- polymorphic!›

definition rec :: "'b ⇒ ('a ⇒ 'b ⇒ 'b) ⇒ 'a ⇒ 'b"
  where "rec e r x = (THE y. Rec e r x y)"

lemma rec_eval:
  assumes Rec: "Rec e r x y"
  shows "rec e r x = y"
  unfolding rec_def
  using Rec_functional and Rec by (rule the1_equality)

lemma rec_zero [simp]: "rec e r zero = e"
proof (rule rec_eval)
  show "Rec e r zero e" ..
qed

lemma rec_succ [simp]: "rec e r (succ m) = r m (rec e r m)"
proof (rule rec_eval)
  let ?R = "Rec e r"
  have "?R m (rec e r m)"
    unfolding rec_def using Rec_functional by (rule theI')
  then show "?R (succ m) (r m (rec e r m))" ..
qed


text ‹┉ Example: addition (monomorphic)›

definition add :: "'a ⇒ 'a ⇒ 'a"
  where "add m n = rec n (λ_ k. succ k) m"

lemma add_zero [simp]: "add zero n = n"
  and add_succ [simp]: "add (succ m) n = succ (add m n)"
  unfolding add_def by simp_all

lemma add_assoc: "add (add k m) n = add k (add m n)"
  by (induct k) simp_all

lemma add_zero_right: "add m zero = m"
  by (induct m) simp_all

lemma add_succ_right: "add m (succ n) = succ (add m n)"
  by (induct m) simp_all

lemma "add (succ (succ (succ zero))) (succ (succ zero)) =
    succ (succ (succ (succ (succ zero))))"
  by simp


text ‹┉ Example: replication (polymorphic)›

definition repl :: "'a ⇒ 'b ⇒ 'b list"
  where "repl n x = rec [] (λ_ xs. x # xs) n"

lemma repl_zero [simp]: "repl zero x = []"
  and repl_succ [simp]: "repl (succ n) x = x # repl n x"
  unfolding repl_def by simp_all

lemma "repl (succ (succ (succ zero))) True = [True, True, True]"
  by simp

end


text ‹┉ Just see that our abstract specification makes sense \dots›

interpretation peano 0 Suc
proof
  fix m n
  show "Suc m ≠ 0" by simp
  show "Suc m = Suc n ⟷ m = n" by simp
  show "P n"
    if zero: "P 0"
    and succ: "⋀n. P n ⟹ P (Suc n)"
    for P
  proof (induct n)
    case 0
    show ?case by (rule zero)
  next
    case Suc
    then show ?case by (rule succ)
  qed
qed

end