(* Title: HOL/Induct/Ordinals.thy ID: $Id: Ordinals.thy,v 1.5 2005/06/17 14:13:07 haftmann Exp $ Author: Stefan Berghofer and Markus Wenzel, TU Muenchen *) header {* Ordinals *} theory Ordinals imports Main begin text {* Some basic definitions of ordinal numbers. Draws an Agda development (in Martin-L\"of type theory) by Peter Hancock (see \url{http://www.dcs.ed.ac.uk/home/pgh/chat.html}). *} datatype ordinal = Zero | Succ ordinal | Limit "nat => ordinal" consts pred :: "ordinal => nat => ordinal option" primrec "pred Zero n = None" "pred (Succ a) n = Some a" "pred (Limit f) n = Some (f n)" consts iter :: "('a => 'a) => nat => ('a => 'a)" primrec "iter f 0 = id" "iter f (Suc n) = f o (iter f n)" constdefs OpLim :: "(nat => (ordinal => ordinal)) => (ordinal => ordinal)" "OpLim F a == Limit (λn. F n a)" OpItw :: "(ordinal => ordinal) => (ordinal => ordinal)" ("\<Squnion>") "\<Squnion>f == OpLim (iter f)" consts cantor :: "ordinal => ordinal => ordinal" primrec "cantor a Zero = Succ a" "cantor a (Succ b) = \<Squnion>(λx. cantor x b) a" "cantor a (Limit f) = Limit (λn. cantor a (f n))" consts Nabla :: "(ordinal => ordinal) => (ordinal => ordinal)" ("∇") primrec "∇f Zero = f Zero" "∇f (Succ a) = f (Succ (∇f a))" "∇f (Limit h) = Limit (λn. ∇f (h n))" constdefs deriv :: "(ordinal => ordinal) => (ordinal => ordinal)" "deriv f == ∇(\<Squnion>f)" consts veblen :: "ordinal => ordinal => ordinal" primrec "veblen Zero = ∇(OpLim (iter (cantor Zero)))" "veblen (Succ a) = ∇(OpLim (iter (veblen a)))" "veblen (Limit f) = ∇(OpLim (λn. veblen (f n)))" constdefs "veb a == veblen a Zero" "ε0 == veb Zero" "Γ0 == Limit (λn. iter veb n Zero)" end