# Theory OrdinalRec

```(*  Title:       Countable Ordinals

Author:      Brian Huffman, 2005
Maintainer:  Brian Huffman <brianh at cse.ogi.edu>
*)

section ‹Recursive Definitions›

theory OrdinalRec
imports OrdinalCont
begin

definition
oPrec :: "ordinal ⇒ ordinal" where
"oPrec x = (THE p. x = oSuc p)"

lemma oPrec_oSuc [simp]: "oPrec (oSuc x) = x"

lemma oPrec_less: "∃p. x = oSuc p ⟹ oPrec x < x"
by clarsimp

definition
ordinal_rec0 ::
"['a, ordinal ⇒ 'a ⇒ 'a, (nat ⇒ 'a) ⇒ 'a, ordinal] ⇒ 'a" where
"ordinal_rec0 z s l ≡ wfrec {(x,y). x < y} (λF x.
if x = 0 then z else
if (∃p. x = oSuc p) then s (oPrec x) (F (oPrec x)) else
(THE y. ∀f. (∀n. f n < oLimit f) ∧ oLimit f = x
⟶ l (λn. F (f n)) = y))"

lemma ordinal_rec0_0 [simp]: "ordinal_rec0 z s l 0 = z"
by (simp add: cut_apply def_wfrec[OF ordinal_rec0_def wf])

lemma ordinal_rec0_oSuc: "ordinal_rec0 z s l (oSuc x) = s x (ordinal_rec0 z s l x)"
by (simp add: cut_apply def_wfrec[OF ordinal_rec0_def wf])

lemma limit_ordinal_not_0: "limit_ordinal x ⟹ x ≠ 0" and limit_ordinal_not_oSuc: "limit_ordinal x ⟹ x ≠ oSuc p"
by auto

lemma ordinal_rec0_limit_ordinal:
"limit_ordinal x ⟹ ordinal_rec0 z s l x =
(THE y. ∀f. (∀n. f n < oLimit f) ∧ oLimit f = x ⟶
l (λn. ordinal_rec0 z s l (f n)) = y)"
apply (rule trans[OF def_wfrec[OF ordinal_rec0_def wf]])
apply (rule_tac f=The in arg_cong, rule ext)
apply (rule_tac f=All in arg_cong, rule ext)
apply safe
done

subsection ‹Partial orders›

locale porder =
fixes le  :: "'a ⇒ 'a ⇒ bool" (infixl "<<" 55)
assumes po_refl:    "⋀x. x << x"
and po_trans:   "⋀x y z. ⟦x << y; y << z⟧ ⟹ x << z"
and po_antisym: "⋀x y. ⟦x << y; y << x⟧ ⟹ x = y"

lemma porder_order: "porder ((≤) :: 'a::order ⇒ 'a ⇒ bool)"
using porder_def by fastforce

lemma (in porder) flip: "porder (λx y. y << x)"
by (metis (no_types, lifting) po_antisym po_refl po_trans porder_def)

locale omega_complete = porder +
fixes lub :: "(nat ⇒ 'a) ⇒ 'a"
assumes is_ub_lub: "⋀f n. f n << lub f"
assumes is_lub_lub: "⋀f x. ∀n. f n << x ⟹ lub f << x"

lemma (in omega_complete) lub_cong_lemma:
"⟦∀n. f n < oLimit f; ∀m. g m < oLimit g; oLimit f ≤ oLimit g;
∀y<oLimit g. ∀x≤y. F x << F y⟧
⟹ lub (λn. F (f n)) << lub (λn. F (g n))"
apply (rule is_lub_lub[rule_format])
by (metis dual_order.trans is_ub_lub leD linorder_le_cases oLimit_leI po_trans)

lemma (in omega_complete) lub_cong:
"⟦∀n. f n < oLimit f; ∀m. g m < oLimit g; oLimit f = oLimit g;
∀y<oLimit g. ∀x≤y. F x << F y⟧
⟹ lub (λn. F (f n)) = lub (λn. F (g n))"

lemma (in omega_complete) ordinal_rec0_mono:
assumes s: "∀p x. x << s p x" and "x ≤ y"
shows "ordinal_rec0 z s lub x << ordinal_rec0 z s lub y"
proof -
have "∀y≤w. ∀x≤y. ordinal_rec0 z s lub x << ordinal_rec0 z s lub y" for w
proof (induction w rule: oLimit_induct)
case zero
then show ?case
next
case (suc x)
then show ?case
by (metis le_oSucE oSuc_le_oSuc ordinal_rec0_oSuc po_refl po_trans s)
next
case (lim f)
then have "∀g. (∀n. g n < oLimit g) ∧ oLimit g = oLimit f ⟶
lub (λn. ordinal_rec0 z s lub (g n)) =
lub (λn. ordinal_rec0 z s lub (f n))"
by (metis linorder_not_le lub_cong oLimit_leI order_le_less strict_mono_less_oLimit)
with lim have "ordinal_rec0 z s lub (oLimit f) =
lub (λn. ordinal_rec0 z s lub (f n))"
by (smt (verit, del_insts) the_equality strict_mono_less_oLimit)
then show ?case
by (smt (verit, ccfv_SIG) is_ub_lub le_oLimitE lim.IH order_le_less po_refl po_trans)
qed
with assms show ?thesis
by blast
qed

lemma (in omega_complete) ordinal_rec0_oLimit:
assumes s: "∀p x. x << s p x"
shows "ordinal_rec0 z s lub (oLimit f) =
lub (λn. ordinal_rec0 z s lub (f n))"
proof (cases "∀n. f n < oLimit f")
case True
then show ?thesis
apply (rule the_equality)
apply (metis lub_cong omega_complete.ordinal_rec0_mono omega_complete_axioms s)
by simp
next
case False
then show ?thesis
by (smt (verit, best) is_lub_lub is_ub_lub le_oLimit ordinal_rec0_mono po_antisym s)
qed

subsection ‹Recursive definitions for @{typ "ordinal => ordinal"}›

definition
ordinal_rec ::
"[ordinal, ordinal ⇒ ordinal ⇒ ordinal, ordinal] ⇒ ordinal" where
"ordinal_rec z s = ordinal_rec0 z s oLimit"

lemma omega_complete_oLimit: "omega_complete (≤) oLimit"
by (simp add: oLimit_leI omega_complete_axioms_def omega_complete_def porder_order)

lemma ordinal_rec_0 [simp]: "ordinal_rec z s 0 = z"

lemma ordinal_rec_oSuc [simp]:
"ordinal_rec z s (oSuc x) = s x (ordinal_rec z s x)"
by (unfold ordinal_rec_def, rule ordinal_rec0_oSuc)

lemma ordinal_rec_oLimit:
assumes s: "∀p x. x ≤ s p x"
shows "ordinal_rec z s (oLimit f) = oLimit (λn. ordinal_rec z s (f n))"
by (metis omega_complete.ordinal_rec0_oLimit omega_complete_oLimit ordinal_rec_def s)

lemma continuous_ordinal_rec:
assumes s: "∀p x. x ≤ s p x"
shows "continuous (ordinal_rec z s)"
by (simp add: continuous.intro ordinal_rec_oLimit s)

lemma mono_ordinal_rec:
assumes s: "∀p x. x ≤ s p x"
shows "mono (ordinal_rec z s)"
by (simp add: continuous.mono continuous_ordinal_rec s)

lemma normal_ordinal_rec:
assumes s: "∀p x. x < s p x"
shows "normal (ordinal_rec z s)"
by (simp add: assms continuous.cont continuous_ordinal_rec less_imp_le normalI)

end
```