# Theory Ordinals

(*  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
).
βΊ

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