# Theory OrdinalCont

```(*  Title:       Countable Ordinals

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

section ‹Continuity›

theory OrdinalCont
imports OrdinalInduct
begin

subsection ‹Continuous functions›

locale continuous =
fixes F :: "ordinal ⇒ ordinal"
assumes cont: "F (oLimit f) = oLimit (λn. F (f n))"

lemmas continuousD = continuous.cont

lemma (in continuous) monoD: assumes "x ≤ y" shows "F x ≤ F y"
proof -
have "oLimit (case_nat u (λn. v)) = max u v" for u v
by (metis (no_types, lifting) le_oLimit less_oLimitE linorder_not_le oLimit_Suc nat.case order_le_less)
then show "F x ≤ F y"
by (metis ‹x ≤ y› cont le_oLimit max.absorb2 nat.case(1))
qed

lemma (in continuous) mono: "mono F"

lemma continuousI:
assumes lim: "⋀f. strict_mono f ⟹ F (oLimit f) = oLimit (λn. F (f n))"
assumes suc: "⋀x. F x ≤ F (oSuc x)"
shows "continuous F"
proof -
have mono: "x ≤ y ⟹ F x ≤ F y" for x y
proof (induction y arbitrary: x rule: oLimit_induct)
case zero
then show ?case by auto
next
case (suc x)
with assms show ?case
by (metis antisym_conv1 le_oSucE nless_le order.trans)
next
case (lim f)
with assms show ?case thm assms(1)
by (metis le_oLimitI nle_le oLimit_leI)
qed
have "F (oLimit f) = oLimit (λn. F (f n))" for f
proof (cases "∀n. f n < oLimit f")
case True
then have §: "oLimit (λn. f (make_mono f n)) = oLimit f"
have "⋀n. ∃m. F (f n) ≤ F (f (make_mono f m))"
by (metis True mono less_oLimitD linorder_not_less oLimit_make_mono_eq ordinal_linear)
then show ?thesis
by (metis True § oLimit_eqI lim strict_mono_f_make_mono)
next
case False
then show ?thesis
by (metis le_oLimit less_oLimitE linorder_not_le mono nle_le)
qed
with mono show ?thesis
qed

subsection ‹Normal functions›

locale normal = continuous +
assumes strict: "strict_mono F"

lemma (in normal) mono: "mono F"
by (rule mono)

lemma (in normal) continuous: "continuous F"
by (rule continuous.intro, rule cont)

lemma (in normal) monoD: "x ≤ y ⟹ F x ≤ F y"
by (rule monoD)

lemma (in normal) strict_monoD: "x < y ⟹ F x < F y"
by (erule strict_monoD[OF strict])

lemma (in normal) cancel_eq: "(F x = F y) = (x = y)"
by (rule strict_mono_cancel_eq[OF strict])

lemma (in normal) cancel_less: "(F x < F y) = (x < y)"
by (rule strict_mono_cancel_less[OF strict])

lemma (in normal) cancel_le: "(F x ≤ F y) = (x ≤ y)"
by (rule strict_mono_cancel_le[OF strict])

lemma (in normal) oLimit: "F (oLimit f) = oLimit (λn. F (f n))"
by (rule cont)

lemma (in normal) increasing: "x ≤ F x"
proof (induction x rule: oLimit_induct)
case zero
then show ?case
by simp
next
case (suc x)
then show ?case
by (simp add: normal.strict_monoD normal_axioms oSuc_leI order.strict_trans1)
next
case (lim f)
then show ?case
by (metis cont le_oLimitI oLimit_leI)
qed

lemma normalI:
assumes lim: "⋀f. strict_mono f ⟹ F (oLimit f) = oLimit (λn. F (f n))"
assumes suc: "⋀x. F x < F (oSuc x)"
shows "normal F"
proof -
have mono: "x ≤ y ⟹ F x ≤ F y" for x y
using continuousI assms
by (metis continuous.monoD linorder_not_less ordinal_linear)
then have "OrdinalInduct.strict_mono F"
by (metis OrdinalInduct.strict_monoI leD oSuc_leI order_less_le suc)
then show ?thesis
by (meson continuousI leD lim nle_le normal.intro normal_axioms.intro suc)
qed

lemma normal_range_le:
assumes nml: "normal F" "normal G" and "range G ⊆ range F"
shows "F x ≤ G x"
proof (induction x rule: oLimit_induct)
case zero
with assms show ?case
by (metis image_iff normal.monoD ordinal_0_le range_subsetD)
next
case (suc x)
then have "G (oSuc x) ∈ range F"
using assms(3) by blast
then show ?case
by (smt (verit, ccfv_SIG) nml dual_order.trans leD le_oSucE less_oSuc normal.cancel_le ordinal_linear rangeE suc)
next
case (lim f)
then show ?case
by (metis nml le_oLimitI normal.oLimit oLimit_leI)
qed

lemma normal_range_eq:
"⟦normal F; normal G; range F = range G⟧ ⟹ F = G"
by (force simp add: normal_range_le intro: order_antisym)

end
```