Theory Nat_Class
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