src/HOL/Induct/Ordinals.thy
author wenzelm
Mon, 12 Jul 2010 21:38:37 +0200
changeset 37781 2fbbf0a48cef
parent 36862 952b2b102a0a
child 39246 9e58f0499f57
permissions -rw-r--r--
moved misc legacy stuff from OldGoals to Misc_Legacy; OldGoals: removed unused strip_context, metahyps_thms, read_term, read_prop, gethyps;
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
16417
9bc16273c2d4 migrated theory headers to new format
haftmann
parents: 14981
diff changeset
     7
theory Ordinals imports Main begin
11641
0c248bed5225 added Ordinals example;
wenzelm
parents:
diff changeset
     8
0c248bed5225 added Ordinals example;
wenzelm
parents:
diff changeset
     9
text {*
0c248bed5225 added Ordinals example;
wenzelm
parents:
diff changeset
    10
  Some basic definitions of ordinal numbers.  Draws an Agda
11649
wenzelm
parents: 11641
diff changeset
    11
  development (in Martin-L\"of type theory) by Peter Hancock (see
11641
0c248bed5225 added Ordinals example;
wenzelm
parents:
diff changeset
    12
  \url{http://www.dcs.ed.ac.uk/home/pgh/chat.html}).
0c248bed5225 added Ordinals example;
wenzelm
parents:
diff changeset
    13
*}
0c248bed5225 added Ordinals example;
wenzelm
parents:
diff changeset
    14
0c248bed5225 added Ordinals example;
wenzelm
parents:
diff changeset
    15
datatype ordinal =
0c248bed5225 added Ordinals example;
wenzelm
parents:
diff changeset
    16
    Zero
0c248bed5225 added Ordinals example;
wenzelm
parents:
diff changeset
    17
  | Succ ordinal
0c248bed5225 added Ordinals example;
wenzelm
parents:
diff changeset
    18
  | Limit "nat => ordinal"
0c248bed5225 added Ordinals example;
wenzelm
parents:
diff changeset
    19
0c248bed5225 added Ordinals example;
wenzelm
parents:
diff changeset
    20
consts
0c248bed5225 added Ordinals example;
wenzelm
parents:
diff changeset
    21
  pred :: "ordinal => nat => ordinal option"
0c248bed5225 added Ordinals example;
wenzelm
parents:
diff changeset
    22
primrec
0c248bed5225 added Ordinals example;
wenzelm
parents:
diff changeset
    23
  "pred Zero n = None"
0c248bed5225 added Ordinals example;
wenzelm
parents:
diff changeset
    24
  "pred (Succ a) n = Some a"
0c248bed5225 added Ordinals example;
wenzelm
parents:
diff changeset
    25
  "pred (Limit f) n = Some (f n)"
0c248bed5225 added Ordinals example;
wenzelm
parents:
diff changeset
    26
0c248bed5225 added Ordinals example;
wenzelm
parents:
diff changeset
    27
consts
0c248bed5225 added Ordinals example;
wenzelm
parents:
diff changeset
    28
  iter :: "('a => 'a) => nat => ('a => 'a)"
0c248bed5225 added Ordinals example;
wenzelm
parents:
diff changeset
    29
primrec
0c248bed5225 added Ordinals example;
wenzelm
parents:
diff changeset
    30
  "iter f 0 = id"
0c248bed5225 added Ordinals example;
wenzelm
parents:
diff changeset
    31
  "iter f (Suc n) = f \<circ> (iter f n)"
0c248bed5225 added Ordinals example;
wenzelm
parents:
diff changeset
    32
19736
wenzelm
parents: 16417
diff changeset
    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
wenzelm
parents: 16417
diff changeset
    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
wenzelm
parents: 16417
diff changeset
    39
  "\<Squnion>f = OpLim (iter f)"
11641
0c248bed5225 added Ordinals example;
wenzelm
parents:
diff changeset
    40
0c248bed5225 added Ordinals example;
wenzelm
parents:
diff changeset
    41
consts
0c248bed5225 added Ordinals example;
wenzelm
parents:
diff changeset
    42
  cantor :: "ordinal => ordinal => ordinal"
0c248bed5225 added Ordinals example;
wenzelm
parents:
diff changeset
    43
primrec
0c248bed5225 added Ordinals example;
wenzelm
parents:
diff changeset
    44
  "cantor a Zero = Succ a"
0c248bed5225 added Ordinals example;
wenzelm
parents:
diff changeset
    45
  "cantor a (Succ b) = \<Squnion>(\<lambda>x. cantor x b) a"
0c248bed5225 added Ordinals example;
wenzelm
parents:
diff changeset
    46
  "cantor a (Limit f) = Limit (\<lambda>n. cantor a (f n))"
0c248bed5225 added Ordinals example;
wenzelm
parents:
diff changeset
    47
0c248bed5225 added Ordinals example;
wenzelm
parents:
diff changeset
    48
consts
0c248bed5225 added Ordinals example;
wenzelm
parents:
diff changeset
    49
  Nabla :: "(ordinal => ordinal) => (ordinal => ordinal)"    ("\<nabla>")
0c248bed5225 added Ordinals example;
wenzelm
parents:
diff changeset
    50
primrec
0c248bed5225 added Ordinals example;
wenzelm
parents:
diff changeset
    51
  "\<nabla>f Zero = f Zero"
0c248bed5225 added Ordinals example;
wenzelm
parents:
diff changeset
    52
  "\<nabla>f (Succ a) = f (Succ (\<nabla>f a))"
0c248bed5225 added Ordinals example;
wenzelm
parents:
diff changeset
    53
  "\<nabla>f (Limit h) = Limit (\<lambda>n. \<nabla>f (h n))"
0c248bed5225 added Ordinals example;
wenzelm
parents:
diff changeset
    54
19736
wenzelm
parents: 16417
diff changeset
    55
definition
21404
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 19736
diff changeset
    56
  deriv :: "(ordinal => ordinal) => (ordinal => ordinal)" where
19736
wenzelm
parents: 16417
diff changeset
    57
  "deriv f = \<nabla>(\<Squnion>f)"
11641
0c248bed5225 added Ordinals example;
wenzelm
parents:
diff changeset
    58
0c248bed5225 added Ordinals example;
wenzelm
parents:
diff changeset
    59
consts
0c248bed5225 added Ordinals example;
wenzelm
parents:
diff changeset
    60
  veblen :: "ordinal => ordinal => ordinal"
0c248bed5225 added Ordinals example;
wenzelm
parents:
diff changeset
    61
primrec
0c248bed5225 added Ordinals example;
wenzelm
parents:
diff changeset
    62
  "veblen Zero = \<nabla>(OpLim (iter (cantor Zero)))"
0c248bed5225 added Ordinals example;
wenzelm
parents:
diff changeset
    63
  "veblen (Succ a) = \<nabla>(OpLim (iter (veblen a)))"
0c248bed5225 added Ordinals example;
wenzelm
parents:
diff changeset
    64
  "veblen (Limit f) = \<nabla>(OpLim (\<lambda>n. veblen (f n)))"
0c248bed5225 added Ordinals example;
wenzelm
parents:
diff changeset
    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
0c248bed5225 added Ordinals example;
wenzelm
parents:
diff changeset
    69
0c248bed5225 added Ordinals example;
wenzelm
parents:
diff changeset
    70
end