src/HOL/Induct/Ordinals.thy
author wenzelm
Sat, 07 Apr 2012 16:41:59 +0200
changeset 47389 e8552cba702d
parent 46914 c2ca2c3d23a6
child 53015 a1119cf551e8
permissions -rw-r--r--
explicit checks stable_finished_theory/stable_command allow parallel asynchronous command transactions; tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
11649
wenzelm
parents: 11641
diff changeset
     1
(*  Title:      HOL/Induct/Ordinals.thy
11641
0c248bed5225 added Ordinals example;
wenzelm
parents:
diff changeset
     2
    Author:     Stefan Berghofer and Markus Wenzel, TU Muenchen
0c248bed5225 added Ordinals example;
wenzelm
parents:
diff changeset
     3
*)
0c248bed5225 added Ordinals example;
wenzelm
parents:
diff changeset
     4
0c248bed5225 added Ordinals example;
wenzelm
parents:
diff changeset
     5
header {* Ordinals *}
0c248bed5225 added Ordinals example;
wenzelm
parents:
diff changeset
     6
46914
c2ca2c3d23a6 misc tuning;
wenzelm
parents: 39246
diff changeset
     7
theory Ordinals
c2ca2c3d23a6 misc tuning;
wenzelm
parents: 39246
diff changeset
     8
imports Main
c2ca2c3d23a6 misc tuning;
wenzelm
parents: 39246
diff changeset
     9
begin
11641
0c248bed5225 added Ordinals example;
wenzelm
parents:
diff changeset
    10
0c248bed5225 added Ordinals example;
wenzelm
parents:
diff changeset
    11
text {*
0c248bed5225 added Ordinals example;
wenzelm
parents:
diff changeset
    12
  Some basic definitions of ordinal numbers.  Draws an Agda
11649
wenzelm
parents: 11641
diff changeset
    13
  development (in Martin-L\"of type theory) by Peter Hancock (see
11641
0c248bed5225 added Ordinals example;
wenzelm
parents:
diff changeset
    14
  \url{http://www.dcs.ed.ac.uk/home/pgh/chat.html}).
0c248bed5225 added Ordinals example;
wenzelm
parents:
diff changeset
    15
*}
0c248bed5225 added Ordinals example;
wenzelm
parents:
diff changeset
    16
0c248bed5225 added Ordinals example;
wenzelm
parents:
diff changeset
    17
datatype ordinal =
0c248bed5225 added Ordinals example;
wenzelm
parents:
diff changeset
    18
    Zero
0c248bed5225 added Ordinals example;
wenzelm
parents:
diff changeset
    19
  | Succ ordinal
0c248bed5225 added Ordinals example;
wenzelm
parents:
diff changeset
    20
  | Limit "nat => ordinal"
0c248bed5225 added Ordinals example;
wenzelm
parents:
diff changeset
    21
46914
c2ca2c3d23a6 misc tuning;
wenzelm
parents: 39246
diff changeset
    22
primrec pred :: "ordinal => nat => ordinal option"
c2ca2c3d23a6 misc tuning;
wenzelm
parents: 39246
diff changeset
    23
where
11641
0c248bed5225 added Ordinals example;
wenzelm
parents:
diff changeset
    24
  "pred Zero n = None"
39246
9e58f0499f57 modernized primrec
haftmann
parents: 36862
diff changeset
    25
| "pred (Succ a) n = Some a"
9e58f0499f57 modernized primrec
haftmann
parents: 36862
diff changeset
    26
| "pred (Limit f) n = Some (f n)"
11641
0c248bed5225 added Ordinals example;
wenzelm
parents:
diff changeset
    27
46914
c2ca2c3d23a6 misc tuning;
wenzelm
parents: 39246
diff changeset
    28
abbreviation (input) iter :: "('a => 'a) => nat => ('a => 'a)"
c2ca2c3d23a6 misc tuning;
wenzelm
parents: 39246
diff changeset
    29
  where "iter f n \<equiv> f ^^ n"
c2ca2c3d23a6 misc tuning;
wenzelm
parents: 39246
diff changeset
    30
c2ca2c3d23a6 misc tuning;
wenzelm
parents: 39246
diff changeset
    31
definition OpLim :: "(nat => (ordinal => ordinal)) => (ordinal => ordinal)"
c2ca2c3d23a6 misc tuning;
wenzelm
parents: 39246
diff changeset
    32
  where "OpLim F a = Limit (\<lambda>n. F n a)"
11641
0c248bed5225 added Ordinals example;
wenzelm
parents:
diff changeset
    33
46914
c2ca2c3d23a6 misc tuning;
wenzelm
parents: 39246
diff changeset
    34
definition OpItw :: "(ordinal => ordinal) => (ordinal => ordinal)"  ("\<Squnion>")
c2ca2c3d23a6 misc tuning;
wenzelm
parents: 39246
diff changeset
    35
  where "\<Squnion>f = OpLim (iter f)"
21404
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 19736
diff changeset
    36
46914
c2ca2c3d23a6 misc tuning;
wenzelm
parents: 39246
diff changeset
    37
primrec cantor :: "ordinal => ordinal => ordinal"
c2ca2c3d23a6 misc tuning;
wenzelm
parents: 39246
diff changeset
    38
where
11641
0c248bed5225 added Ordinals example;
wenzelm
parents:
diff changeset
    39
  "cantor a Zero = Succ a"
39246
9e58f0499f57 modernized primrec
haftmann
parents: 36862
diff changeset
    40
| "cantor a (Succ b) = \<Squnion>(\<lambda>x. cantor x b) a"
9e58f0499f57 modernized primrec
haftmann
parents: 36862
diff changeset
    41
| "cantor a (Limit f) = Limit (\<lambda>n. cantor a (f n))"
11641
0c248bed5225 added Ordinals example;
wenzelm
parents:
diff changeset
    42
46914
c2ca2c3d23a6 misc tuning;
wenzelm
parents: 39246
diff changeset
    43
primrec Nabla :: "(ordinal => ordinal) => (ordinal => ordinal)"  ("\<nabla>")
c2ca2c3d23a6 misc tuning;
wenzelm
parents: 39246
diff changeset
    44
where
11641
0c248bed5225 added Ordinals example;
wenzelm
parents:
diff changeset
    45
  "\<nabla>f Zero = f Zero"
39246
9e58f0499f57 modernized primrec
haftmann
parents: 36862
diff changeset
    46
| "\<nabla>f (Succ a) = f (Succ (\<nabla>f a))"
9e58f0499f57 modernized primrec
haftmann
parents: 36862
diff changeset
    47
| "\<nabla>f (Limit h) = Limit (\<lambda>n. \<nabla>f (h n))"
11641
0c248bed5225 added Ordinals example;
wenzelm
parents:
diff changeset
    48
46914
c2ca2c3d23a6 misc tuning;
wenzelm
parents: 39246
diff changeset
    49
definition deriv :: "(ordinal => ordinal) => (ordinal => ordinal)"
c2ca2c3d23a6 misc tuning;
wenzelm
parents: 39246
diff changeset
    50
  where "deriv f = \<nabla>(\<Squnion>f)"
11641
0c248bed5225 added Ordinals example;
wenzelm
parents:
diff changeset
    51
46914
c2ca2c3d23a6 misc tuning;
wenzelm
parents: 39246
diff changeset
    52
primrec veblen :: "ordinal => ordinal => ordinal"
c2ca2c3d23a6 misc tuning;
wenzelm
parents: 39246
diff changeset
    53
where
11641
0c248bed5225 added Ordinals example;
wenzelm
parents:
diff changeset
    54
  "veblen Zero = \<nabla>(OpLim (iter (cantor Zero)))"
39246
9e58f0499f57 modernized primrec
haftmann
parents: 36862
diff changeset
    55
| "veblen (Succ a) = \<nabla>(OpLim (iter (veblen a)))"
9e58f0499f57 modernized primrec
haftmann
parents: 36862
diff changeset
    56
| "veblen (Limit f) = \<nabla>(OpLim (\<lambda>n. veblen (f n)))"
11641
0c248bed5225 added Ordinals example;
wenzelm
parents:
diff changeset
    57
21404
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 19736
diff changeset
    58
definition "veb a = veblen a Zero"
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 19736
diff changeset
    59
definition "\<epsilon>\<^isub>0 = veb Zero"
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 19736
diff changeset
    60
definition "\<Gamma>\<^isub>0 = Limit (\<lambda>n. iter veb n Zero)"
11641
0c248bed5225 added Ordinals example;
wenzelm
parents:
diff changeset
    61
0c248bed5225 added Ordinals example;
wenzelm
parents:
diff changeset
    62
end