Theory Nat_Class

(*  Title:      FOL/ex/Nat_Class.thy
    Author:     Markus Wenzel, TU Muenchen
*)

section ‹Theory of the natural numbers: Peano's axioms, primitive recursion›

theory Nat_Class
  imports FOL
begin

text ‹
  This is an abstract version of 🗏‹Nat.thy›. Instead of axiomatizing a
  single type ‹nat›, it defines the class of all these types (up to
  isomorphism).

  Note: The ‹rec› operator has been made ∗‹monomorphic›, because class
  axioms cannot contain more than one type variable.
›

class nat =
  fixes Zero :: ‹'a›  (‹0›)
    and Suc :: ‹'a ⇒ 'a›
    and rec :: ‹'a ⇒ 'a ⇒ ('a ⇒ 'a ⇒ 'a) ⇒ 'a›
  assumes induct: ‹P(0) ⟹ (⋀x. P(x) ⟹ P(Suc(x))) ⟹ P(n)›
    and Suc_inject: ‹Suc(m) = Suc(n) ⟹ m = n›
    and Suc_neq_Zero: ‹Suc(m) = 0 ⟹ R›
    and rec_Zero: ‹rec(0, a, f) = a›
    and rec_Suc: ‹rec(Suc(m), a, f) = f(m, rec(m, a, f))›
begin

definition add :: ‹'a ⇒ 'a ⇒ 'a›  (infixl ‹+› 60)
  where ‹m + n = rec(m, n, λx y. Suc(y))›

lemma Suc_n_not_n: ‹Suc(k) ≠ (k::'a)›
  apply (rule_tac n = ‹k› in induct)
   apply (rule notI)
   apply (erule Suc_neq_Zero)
  apply (rule notI)
  apply (erule notE)
  apply (erule Suc_inject)
  done

lemma ‹(k + m) + n = k + (m + n)›
  apply (rule induct)
  back
  back
  back
  back
  back
  oops

lemma add_Zero [simp]: ‹0 + n = n›
  apply (unfold add_def)
  apply (rule rec_Zero)
  done

lemma add_Suc [simp]: ‹Suc(m) + n = Suc(m + n)›
  apply (unfold add_def)
  apply (rule rec_Suc)
  done

lemma add_assoc: ‹(k + m) + n = k + (m + n)›
  apply (rule_tac n = ‹k› in induct)
   apply simp
  apply simp
  done

lemma add_Zero_right: ‹m + 0 = m›
  apply (rule_tac n = ‹m› in induct)
   apply simp
  apply simp
  done

lemma add_Suc_right: ‹m + Suc(n) = Suc(m + n)›
  apply (rule_tac n = ‹m› in induct)
   apply simp_all
  done

lemma
  assumes prem: ‹⋀n. f(Suc(n)) = Suc(f(n))›
  shows ‹f(i + j) = i + f(j)›
  apply (rule_tac n = ‹i› in induct)
   apply simp
  apply (simp add: prem)
  done

end

end