11649

1 
(* Title: HOL/Induct/Ordinals.thy

11641

2 
ID: $Id$


3 
Author: Stefan Berghofer and Markus Wenzel, TU Muenchen


4 
*)


5 


6 
header {* Ordinals *}


7 

16417

8 
theory Ordinals imports Main begin

11641

9 


10 
text {*


11 
Some basic definitions of ordinal numbers. Draws an Agda

11649

12 
development (in MartinL\"of type theory) by Peter Hancock (see

11641

13 
\url{http://www.dcs.ed.ac.uk/home/pgh/chat.html}).


14 
*}


15 


16 
datatype ordinal =


17 
Zero


18 
 Succ ordinal


19 
 Limit "nat => ordinal"


20 


21 
consts


22 
pred :: "ordinal => nat => ordinal option"


23 
primrec


24 
"pred Zero n = None"


25 
"pred (Succ a) n = Some a"


26 
"pred (Limit f) n = Some (f n)"


27 


28 
consts


29 
iter :: "('a => 'a) => nat => ('a => 'a)"


30 
primrec


31 
"iter f 0 = id"


32 
"iter f (Suc n) = f \<circ> (iter f n)"


33 


34 
constdefs


35 
OpLim :: "(nat => (ordinal => ordinal)) => (ordinal => ordinal)"


36 
"OpLim F a == Limit (\<lambda>n. F n a)"


37 
OpItw :: "(ordinal => ordinal) => (ordinal => ordinal)" ("\<Squnion>")


38 
"\<Squnion>f == OpLim (iter f)"


39 


40 
consts


41 
cantor :: "ordinal => ordinal => ordinal"


42 
primrec


43 
"cantor a Zero = Succ a"


44 
"cantor a (Succ b) = \<Squnion>(\<lambda>x. cantor x b) a"


45 
"cantor a (Limit f) = Limit (\<lambda>n. cantor a (f n))"


46 


47 
consts


48 
Nabla :: "(ordinal => ordinal) => (ordinal => ordinal)" ("\<nabla>")


49 
primrec


50 
"\<nabla>f Zero = f Zero"


51 
"\<nabla>f (Succ a) = f (Succ (\<nabla>f a))"


52 
"\<nabla>f (Limit h) = Limit (\<lambda>n. \<nabla>f (h n))"


53 


54 
constdefs


55 
deriv :: "(ordinal => ordinal) => (ordinal => ordinal)"


56 
"deriv f == \<nabla>(\<Squnion>f)"


57 


58 
consts


59 
veblen :: "ordinal => ordinal => ordinal"


60 
primrec


61 
"veblen Zero = \<nabla>(OpLim (iter (cantor Zero)))"


62 
"veblen (Succ a) = \<nabla>(OpLim (iter (veblen a)))"


63 
"veblen (Limit f) = \<nabla>(OpLim (\<lambda>n. veblen (f n)))"


64 


65 
constdefs


66 
"veb a == veblen a Zero"

14717

67 
"\<epsilon>\<^isub>0 == veb Zero"


68 
"\<Gamma>\<^isub>0 == Limit (\<lambda>n. iter veb n Zero)"

11641

69 


70 
end
