|
1 theory Ordinal = Main: |
|
2 |
|
3 datatype ordinal = Zero | Succ ordinal | Limit "nat \<Rightarrow> ordinal" |
|
4 |
|
5 consts |
|
6 pred :: "ordinal \<Rightarrow> nat \<Rightarrow> ordinal option" |
|
7 primrec |
|
8 "pred Zero n = None" |
|
9 "pred (Succ a) n = Some a" |
|
10 "pred (Limit f) n = Some (f n)" |
|
11 |
|
12 constdefs |
|
13 OpLim :: "(nat \<Rightarrow> (ordinal \<Rightarrow> ordinal)) \<Rightarrow> (ordinal \<Rightarrow> ordinal)" |
|
14 "OpLim F a \<equiv> Limit (\<lambda>n. F n a)" |
|
15 OpItw :: "(ordinal \<Rightarrow> ordinal) \<Rightarrow> (ordinal \<Rightarrow> ordinal)" ("\<Squnion>") |
|
16 "\<Squnion>f \<equiv> OpLim (power f)" |
|
17 |
|
18 consts |
|
19 cantor :: "ordinal \<Rightarrow> ordinal \<Rightarrow> ordinal" |
|
20 primrec |
|
21 "cantor a Zero = Succ a" |
|
22 "cantor a (Succ b) = \<Squnion>(\<lambda>x. cantor x b) a" |
|
23 "cantor a (Limit f) = Limit (\<lambda>n. cantor a (f n))" |
|
24 |
|
25 consts |
|
26 Nabla :: "(ordinal \<Rightarrow> ordinal) \<Rightarrow> (ordinal \<Rightarrow> ordinal)" ("\<nabla>") |
|
27 primrec |
|
28 "\<nabla>f Zero = f Zero" |
|
29 "\<nabla>f (Succ a) = f (Succ (\<nabla>f a))" |
|
30 "\<nabla>f (Limit h) = Limit (\<lambda>n. \<nabla>f (h n))" |
|
31 |
|
32 constdefs |
|
33 deriv :: "(ordinal \<Rightarrow> ordinal) \<Rightarrow> (ordinal \<Rightarrow> ordinal)" |
|
34 "deriv f \<equiv> \<nabla>(\<Squnion>f)" |
|
35 |
|
36 consts |
|
37 veblen :: "ordinal \<Rightarrow> ordinal \<Rightarrow> ordinal" |
|
38 primrec |
|
39 "veblen Zero = \<nabla>(OpLim (power (cantor Zero)))" |
|
40 "veblen (Succ a) = \<nabla>(OpLim (power (veblen a)))" |
|
41 "veblen (Limit f) = \<nabla>(OpLim (\<lambda>n. veblen (f n)))" |
|
42 |
|
43 constdefs |
|
44 veb :: "ordinal \<Rightarrow> ordinal" |
|
45 "veb a \<equiv> veblen a Zero" |
|
46 epsilon0 :: ordinal ("\<epsilon>\<^sub>0") |
|
47 "\<epsilon>\<^sub>0 \<equiv> veb Zero" |
|
48 Gamma0 :: ordinal ("\<Gamma>\<^sub>0") |
|
49 "\<Gamma>\<^sub>0 \<equiv> Limit (\<lambda>n. (veb^n) Zero)" |
|
50 thm Gamma0_def |
|
51 |
|
52 end |