doc-src/TutorialI/Overview/LNCS/Ordinal.thy

A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
the tactic has also changed and allows the abstaction over fuction occurences whose type is nat or int.

theory Ordinal = Main:

datatype ordinal = Zero | Succ ordinal | Limit "nat \<Rightarrow> ordinal"

consts
  pred :: "ordinal \<Rightarrow> nat \<Rightarrow> ordinal option"
primrec
  "pred Zero n = None"
  "pred (Succ a) n = Some a"
  "pred (Limit f) n = Some (f n)"

constdefs
  OpLim :: "(nat \<Rightarrow> (ordinal \<Rightarrow> ordinal)) \<Rightarrow> (ordinal \<Rightarrow> ordinal)"
  "OpLim F a \<equiv> Limit (\<lambda>n. F n a)"
  OpItw :: "(ordinal \<Rightarrow> ordinal) \<Rightarrow> (ordinal \<Rightarrow> ordinal)"    ("\<Squnion>")
  "\<Squnion>f \<equiv> OpLim (power f)"

consts
  cantor :: "ordinal \<Rightarrow> ordinal \<Rightarrow> ordinal"
primrec
  "cantor a Zero = Succ a"
  "cantor a (Succ b) = \<Squnion>(\<lambda>x. cantor x b) a"
  "cantor a (Limit f) = Limit (\<lambda>n. cantor a (f n))"

consts
  Nabla :: "(ordinal \<Rightarrow> ordinal) \<Rightarrow> (ordinal \<Rightarrow> ordinal)"    ("\<nabla>")
primrec
  "\<nabla>f Zero = f Zero"
  "\<nabla>f (Succ a) = f (Succ (\<nabla>f a))"
  "\<nabla>f (Limit h) = Limit (\<lambda>n. \<nabla>f (h n))"

constdefs
  deriv :: "(ordinal \<Rightarrow> ordinal) \<Rightarrow> (ordinal \<Rightarrow> ordinal)"
  "deriv f \<equiv> \<nabla>(\<Squnion>f)"

consts
  veblen :: "ordinal \<Rightarrow> ordinal \<Rightarrow> ordinal"
primrec
  "veblen Zero = \<nabla>(OpLim (power (cantor Zero)))"
  "veblen (Succ a) = \<nabla>(OpLim (power (veblen a)))"
  "veblen (Limit f) = \<nabla>(OpLim (\<lambda>n. veblen (f n)))"

constdefs
  veb :: "ordinal \<Rightarrow> ordinal"
  "veb a \<equiv> veblen a Zero"
  epsilon0 :: ordinal    ("\<epsilon>\<^sub>0")
  "\<epsilon>\<^sub>0 \<equiv> veb Zero"
  Gamma0 :: ordinal    ("\<Gamma>\<^sub>0")
  "\<Gamma>\<^sub>0 \<equiv> Limit (\<lambda>n. (veb^n) Zero)"
thm Gamma0_def

end