Quelle  Ordinals.thy

(*  Title:      HOL/Induct/Ordinals.thy
  Author: Stefan Berghofer and Markus Wenzel, TU Muenchen
*)

section ‹Ordinals›

theory Ordinals
imports Main
begin

text ‹
  Some basic definitions of ordinal numbers. Draws an Agda
  development (in Martin-Löf type theory) by Peter Hancock (see
  🪙‹http://www.dcs.ed.ac.uk/home/pgh/chat.html›).
 ›

datatype ordinal =
    Zero
  | Succ ordinal
  | Limit "nat ==> ordinal"

primrec pred :: "ordinal ==> nat ==> ordinal option"
where
  "pred Zero n = None"
| "pred (Succ a) n = Some a"
| "pred (Limit f) n = Some (f n)"

abbreviation (input) iter :: "('a ==> 'a) ==> nat ==> ('a ==> 'a)"
  where "iter f n ≡ f ^^ n"

definition OpLim :: "(nat ==> (ordinal ==> ordinal)) ==> (ordinal ==> ordinal)"
  where "OpLim F a = Limit (λn. F n a)"

definition OpItw :: "(ordinal ==> ordinal) ==> (ordinal ==> ordinal)"  (‹⊔›)
  where "⊔f = OpLim (iter f)"

primrec cantor :: "ordinal ==> ordinal ==> ordinal"
where
  "cantor a Zero = Succ a"
| "cantor a (Succ b) = ⊔(λx. cantor x b) a"
| "cantor a (Limit f) = Limit (λn. cantor a (f n))"

primrec Nabla :: "(ordinal ==> ordinal) ==> (ordinal ==> ordinal)"  (‹∇›)
where
  "∇f Zero = f Zero"
| "∇f (Succ a) = f (Succ (∇f a))"
| "∇f (Limit h) = Limit (λn. ∇f (h n))"

definition deriv :: "(ordinal ==> ordinal) ==> (ordinal ==> ordinal)"
  where "deriv f = ∇(⊔f)"

primrec veblen :: "ordinal ==> ordinal ==> ordinal"
where
  "veblen Zero = ∇(OpLim (iter (cantor Zero)))"
| "veblen (Succ a) = ∇(OpLim (iter (veblen a)))"
| "veblen (Limit f) = ∇(OpLim (λn. veblen (f n)))"

definition "veb a = veblen a Zero"
definition "ε🪙0 = veb Zero"
definition "Γ🪙0 = Limit (λn. iter veb n Zero)"

end