# Theory OrdinalInverse

```(*  Title:       Countable Ordinals

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

section ‹Inverse Functions›

theory OrdinalInverse
imports OrdinalArith
begin

lemma (in normal) oInv_ex:
assumes "F 0 ≤ a" shows "∃q. F q ≤ a ∧ a < F (oSuc q)"
proof -
have "a < F z ⟹ (∃q<z. F q ≤ a ∧ a < F (oSuc q))" for z
proof (induction z rule: oLimit_induct)
case zero
then show ?case
using assms by auto
next
case (suc x)
then show ?case
by (metis less_oSuc linorder_not_le order_less_trans)
next
case (lim f)
then show ?case
by (metis less_oLimitD less_oLimitI oLimit)
qed
then show ?thesis
by (metis increasing oSuc_le_eq_less)
qed

lemma oInv_uniq:
assumes "mono (F::ordinal ⇒ ordinal)" "F x ≤ a" "a < F (oSuc x)" "F y ≤ a" "a < F (oSuc y)"
shows "x = y"
proof (cases "x<y")
case True
with assms show ?thesis
by (meson dual_order.trans leD monoD oSuc_leI)
next
case False
with assms show ?thesis
by (meson dual_order.strict_trans2 less_oSucE mono_strict_invE)
qed

definition
oInv :: "(ordinal ⇒ ordinal) ⇒ ordinal ⇒ ordinal" where
"oInv F a = (if F 0 ≤ a then (THE x. F x ≤ a ∧ a < F (oSuc x)) else 0)"

lemma (in normal) oInv_bounds: "F 0 ≤ a ⟹ F (oInv F a) ≤ a ∧ a < F (oSuc (oInv F a))"
by (simp add: oInv_def) (metis (no_types, lifting) theI' mono oInv_ex oInv_uniq)

lemma (in normal) oInv_bound1:
"F 0 ≤ a ⟹ F (oInv F a) ≤ a"
by (rule oInv_bounds[THEN conjunct1])

lemma (in normal) oInv_bound2: "a < F (oSuc (oInv F a))"
by (metis cancel_less linorder_not_le oInv_bounds order.strict_trans ordinal_not_0_less)

lemma (in normal) oInv_equality: "⟦F x ≤ a; a < F (oSuc x)⟧ ⟹ oInv F a = x"
by (meson mono normal.cancel_le normal_axioms oInv_bound1 oInv_bound2 oInv_uniq ordinal_0_le order_trans)

lemma (in normal) oInv_inverse: "oInv F (F x) = x"
by (rule oInv_equality, simp_all add: cancel_less)

lemma (in normal) oInv_equality': "a = F x ⟹ oInv F a = x"

lemma (in normal) oInv_eq_0: "a ≤ F 0 ⟹ oInv F a = 0"
by (metis nle_le oInv_def oInv_equality')

lemma (in normal) oInv_less: "⟦F 0 ≤ a; a < F z⟧ ⟹ oInv F a < z"
using cancel_less oInv_bound1 by fastforce

lemma (in normal) le_oInv: "F z ≤ a ⟹ z ≤ oInv F a"
by (metis cancel_le dual_order.trans le_oSucE linorder_not_less oInv_bound2 order_le_less)

lemma (in normal) less_oInvD: "x < oInv F a ⟹ F (oSuc x) ≤ a"
by (metis (no_types) linorder_not_le nle_le oInv_eq_0 oInv_less oSuc_leI ordinal_0_le)

lemma (in normal) oInv_le: "a < F (oSuc x) ⟹ oInv F a ≤ x"
by (metis leD less_oInvD nle_le order_le_less)

lemma (in normal) mono_oInv: "mono (oInv F)"
proof
fix x y :: ordinal
assume "x ≤ y"
show "oInv F x ≤ oInv F y"
proof (rule linorder_le_cases [of x "F 0"])
assume "x ≤ F 0" then show ?thesis by (simp add: oInv_eq_0)
next
assume "F 0 ≤ x" show ?thesis
by (rule le_oInv, simp only: ‹x ≤ y› ‹F 0 ≤ x› order_trans [OF oInv_bound1])
qed
qed

lemma (in normal) oInv_decreasing: "F 0 ≤ x ⟹ oInv F x ≤ x"
by (meson dual_order.trans increasing oInv_bound1)

subsection ‹Division›

instantiation ordinal :: modulo
begin

definition
div_ordinal_def:
"x div y = (if 0 < y then oInv ((*) y) x else 0)"

definition
mod_ordinal_def:
"x mod y = ((x::ordinal) - y * (x div y))"

instance ..

end

lemma ordinal_divI: "⟦x = y * q + r; r < y⟧ ⟹ x div y = (q::ordinal)"
using div_ordinal_def normal.oInv_equality normal_times by auto

lemma ordinal_times_div_le: "y * (x div y) ≤ (x::ordinal)"
by (simp add: div_ordinal_def normal.oInv_bound1 normal_times)

lemma ordinal_less_times_div_plus: "0 < y ⟹ x < y * (x div y) + (y::ordinal)"
by (metis div_ordinal_def normal.oInv_bound2 normal_times ordinal_times_oSuc)

lemma ordinal_modI: "⟦x = y * q + r; r < y⟧ ⟹ x mod y = (r::ordinal)"

lemma ordinal_mod_less: "0 < y ⟹ x mod y < (y::ordinal)"
by (simp add: mod_ordinal_def ordinal_less_times_div_plus ordinal_times_div_le)

lemma ordinal_div_plus_mod: "y * (x div y) + (x mod y) = (x::ordinal)"

lemma ordinal_div_less: "x < y * z ⟹ x div y < (z::ordinal)"
using div_ordinal_def normal.oInv_less normal_times by auto

lemma ordinal_le_div: "⟦0 < y; y * z ≤ x⟧ ⟹ (z::ordinal) ≤ x div y"
by (simp add: div_ordinal_def normal.le_oInv normal_times)

lemma ordinal_mono_div: "mono (λx. x div y::ordinal)"
by (smt (verit) Orderings.order_eq_iff div_ordinal_def monoD monoI normal.mono_oInv normal_times)

lemma ordinal_div_monoL: "x ≤ x' ⟹ x div y ≤ x' div (y::ordinal)"
by (erule monoD[OF ordinal_mono_div])

lemma ordinal_div_decreasing: "(x::ordinal) div y ≤ x"
by (simp add: div_ordinal_def normal.oInv_decreasing normal_times)

lemma ordinal_div_0: "x div 0 = (0::ordinal)"

lemma ordinal_mod_0: "x mod 0 = (x::ordinal)"

subsection ‹Derived properties of division›

lemma ordinal_div_1 [simp]: "x div oSuc 0 = x"
using ordinal_divI by force

lemma ordinal_mod_1 [simp]: "x mod oSuc 0 = 0"

lemma ordinal_div_self [simp]: "0 < x ⟹ x div x = (1::ordinal)"
by (metis ordinal_divI ordinal_one_def ordinal_plus_0 ordinal_times_1)

lemma ordinal_mod_self [simp]: "x mod x = (0::ordinal)"
by (metis ordinal_modI ordinal_mod_0 ordinal_neq_0 ordinal_plus_0 ordinal_times_1)

lemma ordinal_div_greater [simp]: "x < y ⟹ x div y = (0::ordinal)"

lemma ordinal_mod_greater [simp]: "x < y ⟹ x mod y = (x::ordinal)"

lemma ordinal_0_div [simp]: "0 div x = (0::ordinal)"
by (metis div_ordinal_def ordinal_div_greater)

lemma ordinal_0_mod [simp]: "0 mod x = (0::ordinal)"

lemma ordinal_1_dvd [simp]: "oSuc 0 dvd x"

lemma ordinal_dvd_mod: "y dvd x = (x mod y = (0::ordinal))"
by (metis dvd_def ordinal_0_times ordinal_div_plus_mod ordinal_modI ordinal_mod_0 ordinal_neq_0 ordinal_plus_0)

lemma ordinal_dvd_times_div: "y dvd x ⟹ y * (x div y) = (x::ordinal)"
by (metis ordinal_div_plus_mod ordinal_dvd_mod ordinal_plus_0)

lemma ordinal_dvd_oLimit:
assumes "∀n. x dvd f n" shows "x dvd oLimit f"
proof
show "oLimit f = x * oLimit (λn. f n div x)"
using assms by (simp add: ordinal_dvd_times_div)
qed

subsection ‹Logarithms›

definition
oLog :: "ordinal ⇒ ordinal ⇒ ordinal" where
"oLog b = (λx. if 1 < b then oInv ((**) b) x else 0)"

lemma ordinal_oLogI:
assumes "b ** y ≤ x" "x < b ** y * b" shows "oLog b x = y"
proof (cases "1 < b")
case True
then show ?thesis
by (simp add: assms normal.oInv_equality normal_exp oLog_def)
qed (use assms linorder_neq_iff in fastforce)

lemma ordinal_exp_oLog_le: "⟦0 < x; oSuc 0 < b⟧ ⟹ b ** (oLog b x) ≤ x"
by (simp add: normal.oInv_bound1 normal_exp oLog_def oSuc_leI)

lemma ordinal_less_exp_oLog: "oSuc 0 < b ⟹ x < b ** (oLog b x) * b"
by (metis normal.oInv_bound2 normal_exp oLog_def ordinal_exp_oSuc ordinal_one_def)

lemma ordinal_oLog_less: "⟦0 < x; oSuc 0 < b; x < b ** y⟧ ⟹ oLog b x < y"
by (simp add: normal.oInv_less normal_exp oLog_def oSuc_leI)

lemma ordinal_le_oLog:
"⟦oSuc 0 < b; b ** y ≤ x⟧ ⟹ y ≤ oLog b x"
by (simp add: oLog_def normal.le_oInv[OF normal_exp])

lemma ordinal_oLogI2:
assumes "oSuc 0 < b" "x = b ** y * q + r" "0 < q" "q < b" "r < b ** y"
shows "oLog b x = y"
proof (rule ordinal_oLogI)
show "b ** y ≤ x"
using assms by (metis dual_order.trans ordinal_le_plusR ordinal_le_timesR)
show "x < b ** y * b"
using assms
by (metis leD leI order_less_trans ordinal_divI ordinal_exp_not_0 ordinal_le_div)
qed

lemma ordinal_div_exp_oLog_less: "oSuc 0 < b ⟹ x div (b ** oLog b x) < b"

lemma ordinal_oLog_base_0: "oLog 0 x = 0"

lemma ordinal_oLog_base_1: "oLog (oSuc 0) x = 0"

lemma ordinal_oLog_0: "oLog b 0 = 0"
by (simp add: oLog_def normal.oInv_eq_0[OF normal_exp])

lemma ordinal_oLog_exp: "oSuc 0 < b ⟹ oLog b (b ** x) = x"
by (simp add: oLog_def normal.oInv_inverse[OF normal_exp])

lemma ordinal_oLog_self: "oSuc 0 < b ⟹ oLog b b = oSuc 0"
by (metis ordinal_exp_1 ordinal_oLog_exp)

lemma ordinal_mono_oLog: "mono (oLog b)"
by (simp add: monoD monoI normal.mono_oInv normal_exp oLog_def)

lemma ordinal_oLog_monoR: "x ≤ y ⟹ oLog b x ≤ oLog b y"
by (erule monoD[OF ordinal_mono_oLog])

lemma ordinal_oLog_decreasing: "oLog b x ≤ x"
by (metis normal.increasing normal_exp oLog_def ordinal_0_le ordinal_oLog_exp ordinal_oLog_monoR ordinal_one_def)

end
```