author | wenzelm |
Mon, 12 Jul 2010 21:38:37 +0200 | |
changeset 37781 | 2fbbf0a48cef |
parent 36862 | 952b2b102a0a |
child 39246 | 9e58f0499f57 |
permissions | -rw-r--r-- |
11649 | 1 |
(* Title: HOL/Induct/Ordinals.thy |
11641 | 2 |
Author: Stefan Berghofer and Markus Wenzel, TU Muenchen |
3 |
*) |
|
4 |
||
5 |
header {* Ordinals *} |
|
6 |
||
16417 | 7 |
theory Ordinals imports Main begin |
11641 | 8 |
|
9 |
text {* |
|
10 |
Some basic definitions of ordinal numbers. Draws an Agda |
|
11649 | 11 |
development (in Martin-L\"of type theory) by Peter Hancock (see |
11641 | 12 |
\url{http://www.dcs.ed.ac.uk/home/pgh/chat.html}). |
13 |
*} |
|
14 |
||
15 |
datatype ordinal = |
|
16 |
Zero |
|
17 |
| Succ ordinal |
|
18 |
| Limit "nat => ordinal" |
|
19 |
||
20 |
consts |
|
21 |
pred :: "ordinal => nat => ordinal option" |
|
22 |
primrec |
|
23 |
"pred Zero n = None" |
|
24 |
"pred (Succ a) n = Some a" |
|
25 |
"pred (Limit f) n = Some (f n)" |
|
26 |
||
27 |
consts |
|
28 |
iter :: "('a => 'a) => nat => ('a => 'a)" |
|
29 |
primrec |
|
30 |
"iter f 0 = id" |
|
31 |
"iter f (Suc n) = f \<circ> (iter f n)" |
|
32 |
||
19736 | 33 |
definition |
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
19736
diff
changeset
|
34 |
OpLim :: "(nat => (ordinal => ordinal)) => (ordinal => ordinal)" where |
19736 | 35 |
"OpLim F a = Limit (\<lambda>n. F n a)" |
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
19736
diff
changeset
|
36 |
|
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
19736
diff
changeset
|
37 |
definition |
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
19736
diff
changeset
|
38 |
OpItw :: "(ordinal => ordinal) => (ordinal => ordinal)" ("\<Squnion>") where |
19736 | 39 |
"\<Squnion>f = OpLim (iter f)" |
11641 | 40 |
|
41 |
consts |
|
42 |
cantor :: "ordinal => ordinal => ordinal" |
|
43 |
primrec |
|
44 |
"cantor a Zero = Succ a" |
|
45 |
"cantor a (Succ b) = \<Squnion>(\<lambda>x. cantor x b) a" |
|
46 |
"cantor a (Limit f) = Limit (\<lambda>n. cantor a (f n))" |
|
47 |
||
48 |
consts |
|
49 |
Nabla :: "(ordinal => ordinal) => (ordinal => ordinal)" ("\<nabla>") |
|
50 |
primrec |
|
51 |
"\<nabla>f Zero = f Zero" |
|
52 |
"\<nabla>f (Succ a) = f (Succ (\<nabla>f a))" |
|
53 |
"\<nabla>f (Limit h) = Limit (\<lambda>n. \<nabla>f (h n))" |
|
54 |
||
19736 | 55 |
definition |
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
19736
diff
changeset
|
56 |
deriv :: "(ordinal => ordinal) => (ordinal => ordinal)" where |
19736 | 57 |
"deriv f = \<nabla>(\<Squnion>f)" |
11641 | 58 |
|
59 |
consts |
|
60 |
veblen :: "ordinal => ordinal => ordinal" |
|
61 |
primrec |
|
62 |
"veblen Zero = \<nabla>(OpLim (iter (cantor Zero)))" |
|
63 |
"veblen (Succ a) = \<nabla>(OpLim (iter (veblen a)))" |
|
64 |
"veblen (Limit f) = \<nabla>(OpLim (\<lambda>n. veblen (f n)))" |
|
65 |
||
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
19736
diff
changeset
|
66 |
definition "veb a = veblen a Zero" |
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
19736
diff
changeset
|
67 |
definition "\<epsilon>\<^isub>0 = veb Zero" |
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
19736
diff
changeset
|
68 |
definition "\<Gamma>\<^isub>0 = Limit (\<lambda>n. iter veb n Zero)" |
11641 | 69 |
|
70 |
end |