author  wenzelm 
Sat, 07 Apr 2012 16:41:59 +0200  
changeset 47389  e8552cba702d 
parent 46914  c2ca2c3d23a6 
child 53015  a1119cf551e8 
permissions  rwrr 
11649  1 
(* Title: HOL/Induct/Ordinals.thy 
11641  2 
Author: Stefan Berghofer and Markus Wenzel, TU Muenchen 
3 
*) 

4 

5 
header {* Ordinals *} 

6 

46914  7 
theory Ordinals 
8 
imports Main 

9 
begin 

11641  10 

11 
text {* 

12 
Some basic definitions of ordinal numbers. Draws an Agda 

11649  13 
development (in MartinL\"of type theory) by Peter Hancock (see 
11641  14 
\url{http://www.dcs.ed.ac.uk/home/pgh/chat.html}). 
15 
*} 

16 

17 
datatype ordinal = 

18 
Zero 

19 
 Succ ordinal 

20 
 Limit "nat => ordinal" 

21 

46914  22 
primrec pred :: "ordinal => nat => ordinal option" 
23 
where 

11641  24 
"pred Zero n = None" 
39246  25 
 "pred (Succ a) n = Some a" 
26 
 "pred (Limit f) n = Some (f n)" 

11641  27 

46914  28 
abbreviation (input) iter :: "('a => 'a) => nat => ('a => 'a)" 
29 
where "iter f n \<equiv> f ^^ n" 

30 

31 
definition OpLim :: "(nat => (ordinal => ordinal)) => (ordinal => ordinal)" 

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

11641  33 

46914  34 
definition OpItw :: "(ordinal => ordinal) => (ordinal => ordinal)" ("\<Squnion>") 
35 
where "\<Squnion>f = OpLim (iter f)" 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
19736
diff
changeset

36 

46914  37 
primrec cantor :: "ordinal => ordinal => ordinal" 
38 
where 

11641  39 
"cantor a Zero = Succ a" 
39246  40 
 "cantor a (Succ b) = \<Squnion>(\<lambda>x. cantor x b) a" 
41 
 "cantor a (Limit f) = Limit (\<lambda>n. cantor a (f n))" 

11641  42 

46914  43 
primrec Nabla :: "(ordinal => ordinal) => (ordinal => ordinal)" ("\<nabla>") 
44 
where 

11641  45 
"\<nabla>f Zero = f Zero" 
39246  46 
 "\<nabla>f (Succ a) = f (Succ (\<nabla>f a))" 
47 
 "\<nabla>f (Limit h) = Limit (\<lambda>n. \<nabla>f (h n))" 

11641  48 

46914  49 
definition deriv :: "(ordinal => ordinal) => (ordinal => ordinal)" 
50 
where "deriv f = \<nabla>(\<Squnion>f)" 

11641  51 

46914  52 
primrec veblen :: "ordinal => ordinal => ordinal" 
53 
where 

11641  54 
"veblen Zero = \<nabla>(OpLim (iter (cantor Zero)))" 
39246  55 
 "veblen (Succ a) = \<nabla>(OpLim (iter (veblen a)))" 
56 
 "veblen (Limit f) = \<nabla>(OpLim (\<lambda>n. veblen (f n)))" 

11641  57 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
19736
diff
changeset

58 
definition "veb a = veblen a Zero" 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
19736
diff
changeset

59 
definition "\<epsilon>\<^isub>0 = veb Zero" 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
19736
diff
changeset

60 
definition "\<Gamma>\<^isub>0 = Limit (\<lambda>n. iter veb n Zero)" 
11641  61 

62 
end 