13262
|
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
|