author | haftmann |
Mon, 01 Mar 2010 13:40:23 +0100 | |
changeset 35416 | d8d7d1b785af |
parent 16417 | 9bc16273c2d4 |
child 35437 | fe196f61b970 |
permissions | -rw-r--r-- |
16417 | 1 |
theory Ordinal imports Main begin |
13262 | 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 |
||
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
16417
diff
changeset
|
12 |
definition OpLim :: "(nat \<Rightarrow> (ordinal \<Rightarrow> ordinal)) \<Rightarrow> (ordinal \<Rightarrow> ordinal)" where |
13262 | 13 |
"OpLim F a \<equiv> Limit (\<lambda>n. F n a)" |
14 |
OpItw :: "(ordinal \<Rightarrow> ordinal) \<Rightarrow> (ordinal \<Rightarrow> ordinal)" ("\<Squnion>") |
|
15 |
"\<Squnion>f \<equiv> OpLim (power f)" |
|
16 |
||
17 |
consts |
|
18 |
cantor :: "ordinal \<Rightarrow> ordinal \<Rightarrow> ordinal" |
|
19 |
primrec |
|
20 |
"cantor a Zero = Succ a" |
|
21 |
"cantor a (Succ b) = \<Squnion>(\<lambda>x. cantor x b) a" |
|
22 |
"cantor a (Limit f) = Limit (\<lambda>n. cantor a (f n))" |
|
23 |
||
24 |
consts |
|
25 |
Nabla :: "(ordinal \<Rightarrow> ordinal) \<Rightarrow> (ordinal \<Rightarrow> ordinal)" ("\<nabla>") |
|
26 |
primrec |
|
27 |
"\<nabla>f Zero = f Zero" |
|
28 |
"\<nabla>f (Succ a) = f (Succ (\<nabla>f a))" |
|
29 |
"\<nabla>f (Limit h) = Limit (\<lambda>n. \<nabla>f (h n))" |
|
30 |
||
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
16417
diff
changeset
|
31 |
definition deriv :: "(ordinal \<Rightarrow> ordinal) \<Rightarrow> (ordinal \<Rightarrow> ordinal)" where |
13262 | 32 |
"deriv f \<equiv> \<nabla>(\<Squnion>f)" |
33 |
||
34 |
consts |
|
35 |
veblen :: "ordinal \<Rightarrow> ordinal \<Rightarrow> ordinal" |
|
36 |
primrec |
|
37 |
"veblen Zero = \<nabla>(OpLim (power (cantor Zero)))" |
|
38 |
"veblen (Succ a) = \<nabla>(OpLim (power (veblen a)))" |
|
39 |
"veblen (Limit f) = \<nabla>(OpLim (\<lambda>n. veblen (f n)))" |
|
40 |
||
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
16417
diff
changeset
|
41 |
definition veb :: "ordinal \<Rightarrow> ordinal" where |
13262 | 42 |
"veb a \<equiv> veblen a Zero" |
43 |
epsilon0 :: ordinal ("\<epsilon>\<^sub>0") |
|
44 |
"\<epsilon>\<^sub>0 \<equiv> veb Zero" |
|
45 |
Gamma0 :: ordinal ("\<Gamma>\<^sub>0") |
|
46 |
"\<Gamma>\<^sub>0 \<equiv> Limit (\<lambda>n. (veb^n) Zero)" |
|
47 |
thm Gamma0_def |
|
48 |
||
49 |
end |