# Theory OrdinalOmega

```(*  Title:       Countable Ordinals

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

section ‹Omega›

theory OrdinalOmega
imports OrdinalFix
begin

subsection ‹Embedding naturals in the ordinals›

primrec ordinal_of_nat :: "nat ⇒ ordinal"
where
"ordinal_of_nat 0 = 0"
| "ordinal_of_nat (Suc n) = oSuc (ordinal_of_nat n)"

lemma strict_mono_ordinal_of_nat: "strict_mono ordinal_of_nat"

lemma not_limit_ordinal_nat: "¬ limit_ordinal (ordinal_of_nat n)"
by (induct n) simp_all

lemma ordinal_of_nat_eq [simp]:
"(ordinal_of_nat x = ordinal_of_nat y) = (x = y)"
by (rule strict_mono_cancel_eq[OF strict_mono_ordinal_of_nat])

lemma ordinal_of_nat_less [simp]:
"(ordinal_of_nat x < ordinal_of_nat y) = (x < y)"
by (rule strict_mono_cancel_less[OF strict_mono_ordinal_of_nat])

lemma ordinal_of_nat_le [simp]:
"(ordinal_of_nat x ≤ ordinal_of_nat y) = (x ≤ y)"
by (rule strict_mono_cancel_le[OF strict_mono_ordinal_of_nat])

lemma ordinal_of_nat_plus [simp]:
"ordinal_of_nat x + ordinal_of_nat y = ordinal_of_nat (x + y)"
by (induct y) simp_all

lemma ordinal_of_nat_times [simp]:
"ordinal_of_nat x * ordinal_of_nat y = ordinal_of_nat (x * y)"

lemma ordinal_of_nat_exp [simp]:
"ordinal_of_nat x ** ordinal_of_nat y = ordinal_of_nat (x ^ y)"
by (induct y, cases x) (simp_all add: mult.commute)

lemma oSuc_plus_ordinal_of_nat:
"oSuc x + ordinal_of_nat n = oSuc (x + ordinal_of_nat n)"
by (induct n) simp_all

lemma less_ordinal_of_nat:
"(x < ordinal_of_nat n) = (∃m. x = ordinal_of_nat m ∧ m < n)"
by (induction n) (use less_oSuc_eq_le in force)+

lemma le_ordinal_of_nat:
"(x ≤ ordinal_of_nat n) = (∃m. x = ordinal_of_nat m ∧ m ≤ n)"
by (auto simp add: order_le_less less_ordinal_of_nat)

subsection ‹Omega, the least limit ordinal›

definition
omega :: "ordinal"  ("ω") where
"omega = oLimit ordinal_of_nat"

lemma less_omegaD: "x < ω ⟹ ∃n. x = ordinal_of_nat n"
by (metis less_oLimitD less_ordinal_of_nat omega_def)

lemma omega_leI: "∀n. ordinal_of_nat n ≤ x ⟹ ω ≤ x"

lemma nat_le_omega [simp]: "ordinal_of_nat n ≤ ω"

lemma nat_less_omega [simp]: "ordinal_of_nat n < ω"
by (simp add: omega_def strict_mono_less_oLimit strict_mono_ordinal_of_nat)

lemma zero_less_omega [simp]: "0 < ω"
using nat_less_omega ordinal_neq_0 by fastforce

lemma limit_ordinal_omega: "limit_ordinal ω"
by (metis limit_ordinal_oLimitI nat_less_omega omega_def)

lemma Least_limit_ordinal: "(LEAST x. limit_ordinal x) = ω"
proof (rule Least_equality)
show "⋀y. limit_ordinal y ⟹ ω ≤ y"
qed (rule limit_ordinal_omega)

lemma "range f = range ordinal_of_nat ⟹ oLimit f = ω"
by (metis le_oLimit oLimit_leI omega_def order_antisym rangeE rangeI)

subsection ‹Arithmetic properties of @{term ω}›

lemma oSuc_less_omega [simp]: "(oSuc x < ω) = (x < ω)"
by (rule oSuc_less_limit_ordinal[OF limit_ordinal_omega])

lemma oSuc_plus_omega [simp]: "oSuc x + ω = x + ω"
proof -
have "⋀n. ∃m. oSuc x + ordinal_of_nat n ≤ x + ordinal_of_nat m"
using oSuc_le_eq_less oSuc_plus_ordinal_of_nat by auto
moreover
have "⋀n. ∃m. x + ordinal_of_nat n ≤ oSuc x + ordinal_of_nat m"
using dual_order.order_iff_strict oSuc_plus_ordinal_of_nat by auto
ultimately show ?thesis
qed

lemma ordinal_of_nat_plus_omega [simp]:
"ordinal_of_nat n + ω = ω"
by (induct n) simp_all

lemma ordinal_of_nat_times_omega [simp]:
assumes "k > 0" shows "ordinal_of_nat k * ω = ω"
proof -
have "∃m. ordinal_of_nat n ≤ ordinal_of_nat (k * m)"
by (metis assms le_add1 mult_eq_if not_less_zero ordinal_of_nat_le)
then have "oLimit (λn. ordinal_of_nat (k * n)) = oLimit ordinal_of_nat"
by (metis assms oLimit_eqI gr0_conv_Suc le_add1 mult_Suc ordinal_of_nat_le)
then show ?thesis
qed

lemma ordinal_plus_times_omega: "x + x * ω = x * ω"
by (metis oSuc_plus_omega ordinal_0_plus ordinal_times_1 ordinal_times_distrib)

lemma ordinal_plus_absorb: "x * ω ≤ y ⟹ x + y = y"
by (metis ordinal_plus_assoc ordinal_plus_minus2 ordinal_plus_times_omega)

lemma ordinal_less_plusL:
assumes "y < x * ω" shows "y < x + y"
proof (cases "x = 0")
case True
with assms show ?thesis by auto
next
case False
then obtain n where n: "ordinal_of_nat n = y div x"
using assms less_omegaD ordinal_div_less by metis
then have "y < x * (1 + ordinal_of_nat n)"
using n unfolding ordinal_one_def oSuc_plus_ordinal_of_nat
by (metis False ordinal_0_plus ordinal_less_times_div_plus ordinal_neq_0 ordinal_times_oSuc)
also have "... ≤ x + y"
using n by (simp add: ordinal_times_distrib ordinal_times_div_le)
finally show ?thesis .
qed

lemma ordinal_plus_absorb_iff: "(x + y = y) = (x * ω ≤ y)"
by (metis linorder_linear order_le_less order_less_irrefl ordinal_less_plusL ordinal_plus_absorb)

lemma ordinal_less_plusL_iff: "(y < x + y) = (y < x * ω)"
by (metis leI linorder_neq_iff ordinal_less_plusL ordinal_plus_absorb)

fixes a :: ordinal
assumes not_0:  "0 < a"
assumes sum_eq: "⋀b. b < a ⟹ b + a = a"

"⟦x < a; y < a⟧ ⟹ x + y < a"
by (metis ordinal_plus_strict_monoR sum_eq)

"x < a ⟹ x * ordinal_of_nat n < a"
by (induct n) (auto simp: not_0 sum_less)

"additive_principal (oSuc a) = (a = 0)"
by (metis less_oSuc0 ordinal_plus_0 ordinal_plus_left_cancel_less ordinal_plus_oSuc)

assumes not_0: "0 < a" and lessa: "(∀x<a. ∀y<a. x + y < a)"
proof -
have "∀b<a. b + a = a"
using lessa
proof (induction a rule: oLimit_induct)
case zero
then show ?case by auto
next
case (suc x)
then show ?case
by (metis le_oSucE less_oSuc linorder_not_le ordinal_le_plusL ordinal_plus_oSuc)
next
case (lim f)
then show ?case
by (metis leD order_le_less ordinal_le_plusL ordinal_plus_minus2)
qed
then show ?thesis
qed

assumes "0 < x" shows "additive_principal (x * ω)"
fix b
assume "b < x * ω"
then obtain k where k: "b < x * ordinal_of_nat k"
by (metis less_oLimitD omega_def ordinal_times_oLimit)
then have "b + x * ordinal_of_nat n ≤ x * ordinal_of_nat (k + n)" for n
by (metis order_less_imp_le ordinal_of_nat_plus ordinal_plus_monoL ordinal_times_distrib)
then show "b + x * ω = x * ω"
by (metis oLimit_eqI omega_def ordinal_le_plusL ordinal_plus_oLimit ordinal_times_oLimit)
qed (use assms in auto)

show "0 < oLimit f"
by (metis assms less_oLimitI not_additive_principal_0 ordinal_neq_0)
next
fix b
assume "b < oLimit f"
then obtain k where "b < f k"
using less_oLimitD by auto
then have "∃m. b + f n ≤ f m" for n
by (metis additive_principal.sum_eq assms order.trans leI order_less_imp_le ordinal_plus_left_cancel_le)
then show "b + oLimit f = oLimit f"
by (metis ‹b < f k› additive_principal_def assms le_oLimit ordinal_plus_assoc ordinal_plus_minus2)
qed

by (induction x rule: oLimit_induct)

lemma (in additive_principal) omega_exp: "∃x. a = ω ** x"
proof -
have "∃x. ω ** x ≤ a ∧ a < ω ** (oSuc x)"
by (metis not_0 oSuc_less_omega ordinal_exp_oLog_le ordinal_exp_oSuc ordinal_less_exp_oLog zero_less_omega)
then show ?thesis
by (metis leD order_le_imp_less_or_eq ordinal_exp_oSuc ordinal_plus_absorb_iff sum_eq)
qed

"additive_principal a = (∃x. a = ω ** x)"

lemma absorb_omega_exp:
"x < ω ** a ⟹ x + ω ** a = ω ** a"

lemma absorb_omega_exp2: "a < b ⟹ ω ** a + ω ** b = ω ** b"
by (rule absorb_omega_exp, simp add: ordinal_exp_strict_monoR)

subsection ‹Cantor normal form›

lemma cnf_lemma: "x > 0 ⟹ x - ω ** oLog ω x < x"
by (simp add: ordinal_exp_oLog_le ordinal_less_exp_oLog ordinal_less_plusL)

primrec from_cnf where
"from_cnf []       = 0"
| "from_cnf (x # xs) = ω ** x + from_cnf xs"

function to_cnf where
[simp del]: "to_cnf x = (if x = 0 then [] else
oLog ω x # to_cnf (x - ω ** oLog ω x))"
by pat_completeness auto

termination by (relation "{(x, y). x < y}")

lemma to_cnf_0 [simp]: "to_cnf 0 = []"

lemma to_cnf_not_0:
"0 < x ⟹ to_cnf x = oLog ω x # to_cnf (x - ω ** oLog ω x)"

lemma to_cnf_eq_Cons: "to_cnf x = a # list ⟹ a = oLog ω x"
by (case_tac "x = 0", simp, simp add: to_cnf_not_0)

lemma to_cnf_inverse: "from_cnf (to_cnf x) = x"
using wf
proof (induction rule: wf_induct_rule)
case (less x)
then have IH: "∀y<x. from_cnf (to_cnf y) = y"
by simp
show ?case
proof (cases "x = 0")
case False
with cnf_lemma show ?thesis
by (simp add: ordinal_exp_oLog_le to_cnf_not_0 IH)
qed auto
qed

primrec normalize_cnf where
normalize_cnf_Nil: "normalize_cnf [] = []"
| normalize_cnf_Cons: "normalize_cnf (x # xs) =
(case xs of [] ⇒ [x] | y # ys ⇒
(if x < y then [] else [x]) @ normalize_cnf xs)"

lemma from_cnf_normalize_cnf: "from_cnf (normalize_cnf xs) = from_cnf xs"
proof (induction xs)
case Nil
then show ?case by auto
next
case (Cons a xs)
have "⋀x y. a < x ⟹ ω ** x + from_cnf y = ω ** a + (ω ** x + from_cnf y)"
by (metis absorb_omega_exp2 from_cnf.simps(2) ordinal_plus_assoc)
with Cons show ?case
by simp (auto simp del: normalize_cnf_Cons split: list.split)
qed

lemma normalize_cnf_to_cnf: "normalize_cnf (to_cnf x) = to_cnf x"
using wf
proof (induction rule: wf_induct_rule)
case (less x)
then have IH: "∀y<x. normalize_cnf (to_cnf y) = to_cnf y"
by simp
show ?case
proof (cases "x = 0")
case False
then have §: "normalize_cnf (to_cnf (x - ω ** oLog ω x)) = to_cnf (x - ω ** oLog ω x)"
using IH cnf_lemma by blast
with False show ?thesis
apply (case_tac "to_cnf (x - ω ** oLog ω x)", simp_all)
by (metis cnf_lemma linorder_not_le order_le_less ordinal_oLog_monoR to_cnf_eq_Cons)
qed auto
qed

text "alternate form of CNF"

lemma cnf2_lemma:
"0 < x ⟹ x mod ω ** oLog ω x < x"
by (meson oSuc_less_omega order_less_le_trans ordinal_exp_not_0 ordinal_exp_oLog_le ordinal_mod_less zero_less_omega)

primrec from_cnf2 where
"from_cnf2 []       = 0"
| "from_cnf2 (x # xs) = ω ** fst x * ordinal_of_nat (snd x) + from_cnf2 xs"

function to_cnf2 where
[simp del]: "to_cnf2 x = (if x = 0 then [] else
(oLog ω x, inv ordinal_of_nat (x div (ω ** oLog ω x)))
# to_cnf2 (x mod (ω ** oLog ω x)))"
by pat_completeness auto

termination by (relation "{(x,y). x < y}")

lemma to_cnf2_0 [simp]: "to_cnf2 0 = []"

lemma to_cnf2_not_0:
"0 < x ⟹ to_cnf2 x = (oLog ω x, inv ordinal_of_nat (x div (ω ** oLog ω x)))
# to_cnf2 (x mod (ω ** oLog ω x))"

lemma to_cnf2_eq_Cons: "to_cnf2 x = (a,b) # list ⟹ a = oLog ω x"
by (metis Pair_inject list.discI list.inject to_cnf2.elims)

lemma ordinal_of_nat_of_ordinal:
"x < ω ⟹ ordinal_of_nat (inv ordinal_of_nat x) = x"

lemma to_cnf2_inverse: "from_cnf2 (to_cnf2 x) = x"
using wf
proof (induction x rule: wf_induct_rule)
case (less x)
show ?case
proof (cases "x > 0")
case True
then show ?thesis
by (simp add: cnf2_lemma less ordinal_div_exp_oLog_less ordinal_div_plus_mod ordinal_of_nat_of_ordinal to_cnf2_not_0)
qed auto
qed

primrec is_normalized2 where
is_normalized2_Nil: "is_normalized2 [] = True"
| is_normalized2_Cons: "is_normalized2 (x # xs) =
(case xs of [] ⇒ True | y # ys ⇒ fst y < fst x ∧ is_normalized2 xs)"

lemma is_normalized2_to_cnf2: "is_normalized2 (to_cnf2 x)"
using wf
proof (induction x rule: wf_induct_rule)
case (less x)
show ?case
proof (cases "x > 0")
case True
then have *: "is_normalized2 (to_cnf2 (x mod ω ** oLog ω x))"
using cnf2_lemma less by blast
show ?thesis
proof (cases "x mod ω ** oLog ω x = 0")
case True
with to_cnf2_not_0 ‹x > 0› show ?thesis by simp
next
case False
with ‹x > 0› * show ?thesis
by (simp add: ordinal_mod_less ordinal_oLog_less to_cnf2_not_0)
qed
qed auto
qed

subsection ‹Epsilon 0›

definition epsilon0 :: ordinal  ("ε⇩0") where
"epsilon0 = oFix ((**) ω) 0"

lemma less_omega_exp: "x < ε⇩0 ⟹ x < ω ** x"
by (simp add: epsilon0_def less_oFix_0D normal.mono normal_exp)

lemma omega_exp_epsilon0: "ω ** ε⇩0 = ε⇩0"
by (simp add: continuous_exp epsilon0_def oFix_fixed)

lemma oLog_omega_less: "⟦0 < x; x < ε⇩0⟧ ⟹ oLog ω x < x"