7 primrec |
7 primrec |
8 "pred Zero n = None" |
8 "pred Zero n = None" |
9 "pred (Succ a) n = Some a" |
9 "pred (Succ a) n = Some a" |
10 "pred (Limit f) n = Some (f n)" |
10 "pred (Limit f) n = Some (f n)" |
11 |
11 |
12 constdefs |
12 definition OpLim :: "(nat \<Rightarrow> (ordinal \<Rightarrow> ordinal)) \<Rightarrow> (ordinal \<Rightarrow> ordinal)" where |
13 OpLim :: "(nat \<Rightarrow> (ordinal \<Rightarrow> ordinal)) \<Rightarrow> (ordinal \<Rightarrow> ordinal)" |
|
14 "OpLim F a \<equiv> Limit (\<lambda>n. F n a)" |
13 "OpLim F a \<equiv> Limit (\<lambda>n. F n a)" |
15 OpItw :: "(ordinal \<Rightarrow> ordinal) \<Rightarrow> (ordinal \<Rightarrow> ordinal)" ("\<Squnion>") |
14 OpItw :: "(ordinal \<Rightarrow> ordinal) \<Rightarrow> (ordinal \<Rightarrow> ordinal)" ("\<Squnion>") |
16 "\<Squnion>f \<equiv> OpLim (power f)" |
15 "\<Squnion>f \<equiv> OpLim (power f)" |
17 |
16 |
18 consts |
17 consts |
27 primrec |
26 primrec |
28 "\<nabla>f Zero = f Zero" |
27 "\<nabla>f Zero = f Zero" |
29 "\<nabla>f (Succ a) = f (Succ (\<nabla>f a))" |
28 "\<nabla>f (Succ a) = f (Succ (\<nabla>f a))" |
30 "\<nabla>f (Limit h) = Limit (\<lambda>n. \<nabla>f (h n))" |
29 "\<nabla>f (Limit h) = Limit (\<lambda>n. \<nabla>f (h n))" |
31 |
30 |
32 constdefs |
31 definition deriv :: "(ordinal \<Rightarrow> ordinal) \<Rightarrow> (ordinal \<Rightarrow> ordinal)" where |
33 deriv :: "(ordinal \<Rightarrow> ordinal) \<Rightarrow> (ordinal \<Rightarrow> ordinal)" |
|
34 "deriv f \<equiv> \<nabla>(\<Squnion>f)" |
32 "deriv f \<equiv> \<nabla>(\<Squnion>f)" |
35 |
33 |
36 consts |
34 consts |
37 veblen :: "ordinal \<Rightarrow> ordinal \<Rightarrow> ordinal" |
35 veblen :: "ordinal \<Rightarrow> ordinal \<Rightarrow> ordinal" |
38 primrec |
36 primrec |
39 "veblen Zero = \<nabla>(OpLim (power (cantor Zero)))" |
37 "veblen Zero = \<nabla>(OpLim (power (cantor Zero)))" |
40 "veblen (Succ a) = \<nabla>(OpLim (power (veblen a)))" |
38 "veblen (Succ a) = \<nabla>(OpLim (power (veblen a)))" |
41 "veblen (Limit f) = \<nabla>(OpLim (\<lambda>n. veblen (f n)))" |
39 "veblen (Limit f) = \<nabla>(OpLim (\<lambda>n. veblen (f n)))" |
42 |
40 |
43 constdefs |
41 definition veb :: "ordinal \<Rightarrow> ordinal" where |
44 veb :: "ordinal \<Rightarrow> ordinal" |
|
45 "veb a \<equiv> veblen a Zero" |
42 "veb a \<equiv> veblen a Zero" |
46 epsilon0 :: ordinal ("\<epsilon>\<^sub>0") |
43 epsilon0 :: ordinal ("\<epsilon>\<^sub>0") |
47 "\<epsilon>\<^sub>0 \<equiv> veb Zero" |
44 "\<epsilon>\<^sub>0 \<equiv> veb Zero" |
48 Gamma0 :: ordinal ("\<Gamma>\<^sub>0") |
45 Gamma0 :: ordinal ("\<Gamma>\<^sub>0") |
49 "\<Gamma>\<^sub>0 \<equiv> Limit (\<lambda>n. (veb^n) Zero)" |
46 "\<Gamma>\<^sub>0 \<equiv> Limit (\<lambda>n. (veb^n) Zero)" |