section ‹Ordinals›
theory Ordinals
imports Main
begin
text ‹
Some basic definitions of ordinal numbers. Draws an Agda
development (in Martin-L\"of 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