2 Author: Stefan Berghofer and Markus Wenzel, TU Muenchen |
2 Author: Stefan Berghofer and Markus Wenzel, TU Muenchen |
3 *) |
3 *) |
4 |
4 |
5 header {* Ordinals *} |
5 header {* Ordinals *} |
6 |
6 |
7 theory Ordinals imports Main begin |
7 theory Ordinals |
|
8 imports Main |
|
9 begin |
8 |
10 |
9 text {* |
11 text {* |
10 Some basic definitions of ordinal numbers. Draws an Agda |
12 Some basic definitions of ordinal numbers. Draws an Agda |
11 development (in Martin-L\"of type theory) by Peter Hancock (see |
13 development (in Martin-L\"of type theory) by Peter Hancock (see |
12 \url{http://www.dcs.ed.ac.uk/home/pgh/chat.html}). |
14 \url{http://www.dcs.ed.ac.uk/home/pgh/chat.html}). |
15 datatype ordinal = |
17 datatype ordinal = |
16 Zero |
18 Zero |
17 | Succ ordinal |
19 | Succ ordinal |
18 | Limit "nat => ordinal" |
20 | Limit "nat => ordinal" |
19 |
21 |
20 primrec pred :: "ordinal => nat => ordinal option" where |
22 primrec pred :: "ordinal => nat => ordinal option" |
|
23 where |
21 "pred Zero n = None" |
24 "pred Zero n = None" |
22 | "pred (Succ a) n = Some a" |
25 | "pred (Succ a) n = Some a" |
23 | "pred (Limit f) n = Some (f n)" |
26 | "pred (Limit f) n = Some (f n)" |
24 |
27 |
25 abbreviation (input) iter :: "('a => 'a) => nat => ('a => 'a)" where |
28 abbreviation (input) iter :: "('a => 'a) => nat => ('a => 'a)" |
26 "iter f n \<equiv> f ^^ n" |
29 where "iter f n \<equiv> f ^^ n" |
27 |
30 |
28 definition |
31 definition OpLim :: "(nat => (ordinal => ordinal)) => (ordinal => ordinal)" |
29 OpLim :: "(nat => (ordinal => ordinal)) => (ordinal => ordinal)" where |
32 where "OpLim F a = Limit (\<lambda>n. F n a)" |
30 "OpLim F a = Limit (\<lambda>n. F n a)" |
|
31 |
33 |
32 definition |
34 definition OpItw :: "(ordinal => ordinal) => (ordinal => ordinal)" ("\<Squnion>") |
33 OpItw :: "(ordinal => ordinal) => (ordinal => ordinal)" ("\<Squnion>") where |
35 where "\<Squnion>f = OpLim (iter f)" |
34 "\<Squnion>f = OpLim (iter f)" |
|
35 |
36 |
36 primrec cantor :: "ordinal => ordinal => ordinal" where |
37 primrec cantor :: "ordinal => ordinal => ordinal" |
|
38 where |
37 "cantor a Zero = Succ a" |
39 "cantor a Zero = Succ a" |
38 | "cantor a (Succ b) = \<Squnion>(\<lambda>x. cantor x b) a" |
40 | "cantor a (Succ b) = \<Squnion>(\<lambda>x. cantor x b) a" |
39 | "cantor a (Limit f) = Limit (\<lambda>n. cantor a (f n))" |
41 | "cantor a (Limit f) = Limit (\<lambda>n. cantor a (f n))" |
40 |
42 |
41 primrec Nabla :: "(ordinal => ordinal) => (ordinal => ordinal)" ("\<nabla>") where |
43 primrec Nabla :: "(ordinal => ordinal) => (ordinal => ordinal)" ("\<nabla>") |
|
44 where |
42 "\<nabla>f Zero = f Zero" |
45 "\<nabla>f Zero = f Zero" |
43 | "\<nabla>f (Succ a) = f (Succ (\<nabla>f a))" |
46 | "\<nabla>f (Succ a) = f (Succ (\<nabla>f a))" |
44 | "\<nabla>f (Limit h) = Limit (\<lambda>n. \<nabla>f (h n))" |
47 | "\<nabla>f (Limit h) = Limit (\<lambda>n. \<nabla>f (h n))" |
45 |
48 |
46 definition |
49 definition deriv :: "(ordinal => ordinal) => (ordinal => ordinal)" |
47 deriv :: "(ordinal => ordinal) => (ordinal => ordinal)" where |
50 where "deriv f = \<nabla>(\<Squnion>f)" |
48 "deriv f = \<nabla>(\<Squnion>f)" |
|
49 |
51 |
50 primrec veblen :: "ordinal => ordinal => ordinal" where |
52 primrec veblen :: "ordinal => ordinal => ordinal" |
|
53 where |
51 "veblen Zero = \<nabla>(OpLim (iter (cantor Zero)))" |
54 "veblen Zero = \<nabla>(OpLim (iter (cantor Zero)))" |
52 | "veblen (Succ a) = \<nabla>(OpLim (iter (veblen a)))" |
55 | "veblen (Succ a) = \<nabla>(OpLim (iter (veblen a)))" |
53 | "veblen (Limit f) = \<nabla>(OpLim (\<lambda>n. veblen (f n)))" |
56 | "veblen (Limit f) = \<nabla>(OpLim (\<lambda>n. veblen (f n)))" |
54 |
57 |
55 definition "veb a = veblen a Zero" |
58 definition "veb a = veblen a Zero" |