# Theory OrdinalInduct

```(*  Title:       Countable Ordinals

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

section ‹Ordinal Induction›

theory OrdinalInduct
imports OrdinalDef
begin

subsection ‹Zero and successor ordinals›

definition
oSuc :: "ordinal ⇒ ordinal" where
"oSuc x = oStrictLimit (λn. x)"

lemma less_oSuc[iff]: "x < oSuc x"
by (metis oStrictLimit_ub oSuc_def)

lemma oSuc_leI: "x < y ⟹ oSuc x ≤ y"

instantiation ordinal :: "{zero, one}"
begin

definition
ordinal_zero_def:       "(0::ordinal) = oZero"

definition
ordinal_one_def [simp]: "(1::ordinal) = oSuc 0"

instance ..

end

subsubsection ‹Derived properties of 0 and oSuc›

lemma less_oSuc_eq_le: "(x < oSuc y) = (x ≤ y)"
by (metis dual_order.strict_trans1 less_oSuc linorder_not_le oSuc_leI)

lemma ordinal_0_le [iff]: "0 ≤ (x::ordinal)"

lemma ordinal_not_less_0 [iff]: "¬ (x::ordinal) < 0"

lemma ordinal_le_0 [iff]: "(x ≤ 0) = (x = (0::ordinal))"

lemma ordinal_neq_0 [iff]: "(x ≠ 0) = (0 < (x::ordinal))"

lemma ordinal_not_0_less [iff]: "(¬ 0 < x) = (x = (0::ordinal))"

lemma oSuc_le_eq_less: "(oSuc x ≤ y) = (x < y)"
by (meson leD leI less_oSuc_eq_le)

lemma zero_less_oSuc [iff]: "0 < oSuc x"
by (rule order_le_less_trans, rule ordinal_0_le, rule less_oSuc)

lemma oSuc_not_0 [iff]: "oSuc x ≠ 0"
by simp

lemma less_oSuc0 [iff]: "(x < oSuc 0) = (x = 0)"

lemma oSuc_less_oSuc [iff]: "(oSuc x < oSuc y) = (x < y)"

lemma oSuc_eq_oSuc [iff]: "(oSuc x = oSuc y) = (x = y)"
by (metis less_oSuc less_oSuc_eq_le order_antisym)

lemma oSuc_le_oSuc [iff]: "(oSuc x ≤ oSuc y) = (x ≤ y)"

lemma le_oSucE:
"⟦x ≤ oSuc y; x ≤ y ⟹ R; x = oSuc y ⟹ R⟧ ⟹ R"
by (auto simp add: order_le_less less_oSuc_eq_le)

lemma less_oSucE:
"⟦x < oSuc y; x < y ⟹ P; x = y ⟹ P⟧ ⟹ P"
by (auto simp add: less_oSuc_eq_le order_le_less)

subsection ‹Strict monotonicity›

locale strict_mono =
fixes f
assumes strict_mono: "A < B ⟹ f A < f B"

lemmas strict_monoI = strict_mono.intro
and strict_monoD = strict_mono.strict_mono

lemma strict_mono_natI:
fixes f :: "nat ⇒ 'a::order"
shows "(⋀n. f n < f (Suc n)) ⟹ strict_mono f"
using OrdinalInduct.strict_monoI lift_Suc_mono_less by blast

lemma mono_natI:
fixes f :: "nat ⇒ 'a::order"
shows "(⋀n. f n ≤ f (Suc n)) ⟹ mono f"

lemma strict_mono_mono:
fixes f :: "'a::order ⇒ 'b::order"
shows "strict_mono f ⟹ mono f"
by (auto intro!: monoI simp add: order_le_less strict_monoD)

lemma strict_mono_monoD:
fixes f :: "'a::order ⇒ 'b::order"
shows "⟦strict_mono f; A ≤ B⟧ ⟹ f A ≤ f B"
by (rule monoD[OF strict_mono_mono])

lemma strict_mono_cancel_eq:
fixes f :: "'a::linorder ⇒ 'b::linorder"
shows "strict_mono f ⟹ (f x = f y) = (x = y)"
by (metis OrdinalInduct.strict_monoD not_less_iff_gr_or_eq)

lemma strict_mono_cancel_less:
fixes f :: "'a::linorder ⇒ 'b::linorder"
shows "strict_mono f ⟹ (f x < f y) = (x < y)"
using OrdinalInduct.strict_monoD linorder_neq_iff by fastforce

lemma strict_mono_cancel_le:
fixes f :: "'a::linorder ⇒ 'b::linorder"
shows "strict_mono f ⟹ (f x ≤ f y) = (x ≤ y)"
by (meson linorder_not_less strict_mono_cancel_less)

subsection ‹Limit ordinals›

definition
oLimit :: "(nat ⇒ ordinal) ⇒ ordinal" where
"oLimit f = (LEAST k. ∀n. f n ≤ k)"

lemma oLimit_leI: "∀n. f n ≤ x ⟹ oLimit f ≤ x"

lemma le_oLimit [iff]: "f n ≤ oLimit f"
by (smt (verit, best) LeastI_ex leD oLimit_def oStrictLimit_ub ordinal_linear)

lemma le_oLimitI: "x ≤ f n ⟹ x ≤ oLimit f"
by (erule order_trans, rule le_oLimit)

lemma less_oLimitI: "x < f n ⟹ x < oLimit f"
by (erule order_less_le_trans, rule le_oLimit)

lemma less_oLimitD: "x < oLimit f ⟹ ∃n. x < f n"
by (meson linorder_not_le oLimit_leI)

lemma less_oLimitE: "⟦x < oLimit f; ⋀n. x < f n ⟹ P⟧ ⟹ P"
by (auto dest: less_oLimitD)

lemma le_oLimitE:
"⟦x ≤ oLimit f; ⋀n. x ≤ f n ⟹ R; x = oLimit f ⟹ R⟧ ⟹ R"
by (auto simp add: order_le_less dest: less_oLimitD)

lemma oLimit_const [simp]: "oLimit (λn. x) = x"
by (meson dual_order.refl le_oLimit oLimit_leI order_antisym)

lemma strict_mono_less_oLimit: "strict_mono f ⟹ f n < oLimit f"
by (meson OrdinalInduct.strict_monoD lessI less_oLimitI)

lemma oLimit_eqI:
"⟦⋀n. ∃m. f n ≤ g m; ⋀n. ∃m. g n ≤ f m⟧ ⟹ oLimit f = oLimit g"
by (meson le_oLimitI nle_le oLimit_leI)

lemma oLimit_Suc:
"f 0 < oLimit f ⟹ oLimit (λn. f (Suc n)) = oLimit f"
by (smt (verit, ccfv_SIG) linorder_not_le nle_le oLimit_eqI oLimit_leI old.nat.exhaust)

lemma oLimit_shift:
"∀n. f n < oLimit f ⟹ oLimit (λn. f (n + k)) = oLimit f"
apply (induct_tac k, simp)
by (metis (no_types, lifting) add_Suc_shift leD le_oLimit less_oLimitD not_less_iff_gr_or_eq oLimit_Suc)

lemma oLimit_shift_mono:
"mono f ⟹ oLimit (λn. f (n + k)) = oLimit f"

text "limit ordinal predicate"

definition
limit_ordinal :: "ordinal ⇒ bool" where
"limit_ordinal x ⟷ (x ≠ 0) ∧ (∀y. x ≠ oSuc y)"

lemma limit_ordinal_not_0 [simp]: "¬ limit_ordinal 0"

lemma zero_less_limit_ordinal [simp]: "limit_ordinal x ⟹ 0 < x"

lemma limit_ordinal_not_oSuc [simp]: "¬ limit_ordinal (oSuc p)"

lemma oSuc_less_limit_ordinal:
"limit_ordinal x ⟹ (oSuc w < x) = (w < x)"
by (metis limit_ordinal_not_oSuc oSuc_le_eq_less order_le_less)

lemma limit_ordinal_oLimitI:
"∀n. f n < oLimit f ⟹ limit_ordinal (oLimit f)"
by (metis less_oLimitD less_oSuc less_oSucE limit_ordinal_def order_less_imp_triv ordinal_neq_0)

lemma strict_mono_limit_ordinal:
"strict_mono f ⟹ limit_ordinal (oLimit f)"

lemma limit_ordinalI:
"⟦0 < z; ∀x<z. oSuc x < z⟧ ⟹ limit_ordinal z"
using limit_ordinal_def by blast

subsubsection ‹Making strict monotonic sequences›

primrec make_mono :: "(nat ⇒ ordinal) ⇒ nat ⇒ nat"
where
"make_mono f 0       = 0"
| "make_mono f (Suc n) = (LEAST x. f (make_mono f n) < f x)"

lemma f_make_mono_less:
"∀n. f n < oLimit f ⟹ f (make_mono f n) < f (make_mono f (Suc n))"
by (metis less_oLimitD make_mono.simps(2) wellorder_Least_lemma(1))

lemma strict_mono_f_make_mono:
"∀n. f n < oLimit f ⟹ strict_mono (λn. f (make_mono f n))"
by (rule strict_mono_natI, erule f_make_mono_less)

lemma le_f_make_mono:
"⟦∀n. f n < oLimit f; m ≤ make_mono f n⟧ ⟹ f m ≤ f (make_mono f n)"
apply (case_tac n, simp_all)
by (metis LeastI less_oLimitD linorder_le_less_linear not_less_Least order_le_less_trans)

lemma make_mono_less:
"∀n. f n < oLimit f ⟹ make_mono f n < make_mono f (Suc n)"
by (meson f_make_mono_less le_f_make_mono linorder_not_less)

declare make_mono.simps [simp del]

lemma oLimit_make_mono_eq:
assumes "∀n. f n < oLimit f" shows "oLimit (λn. f (make_mono f n)) = oLimit f"
proof -
have "k ≤ make_mono f k" for k
by (induction k) (auto simp: Suc_leI assms make_mono_less order_le_less_trans)
then show ?thesis
by (meson assms le_f_make_mono oLimit_eqI)
qed

subsection ‹Induction principle for ordinals›

lemma oLimit_le_oStrictLimit: "oLimit f ≤ oStrictLimit f"
by (simp add: oLimit_leI oStrictLimit_ub order_less_imp_le)

lemma oLimit_induct [case_names zero suc lim]:
assumes zero: "P 0"
and suc:  "⋀x. P x ⟹ P (oSuc x)"
and lim:  "⋀f. ⟦strict_mono f; ∀n. P (f n)⟧ ⟹ P (oLimit f)"
shows "P a"
apply (rule oStrictLimit_induct)
apply (rule zero[unfolded ordinal_zero_def])
apply (cut_tac f=f in oLimit_le_oStrictLimit)
apply (simp add: order_le_less, erule disjE)
apply (metis dual_order.order_iff_strict leD le_oLimit less_oStrictLimitD oSuc_le_eq_less suc)
by (metis lim oLimit_make_mono_eq oStrictLimit_ub strict_mono_f_make_mono)

lemma ordinal_cases [case_names zero suc lim]:
assumes zero: "a = 0 ⟹ P"
and suc:  "⋀x. a = oSuc x ⟹ P"
and lim:  "⋀f. ⟦strict_mono f; a = oLimit f⟧ ⟹ P"
shows "P"
apply (subgoal_tac "∀x. a = x ⟶ P", force)
apply (rule allI)
apply (rule_tac a=x in oLimit_induct)
apply (rule impI, erule zero)
apply (rule impI, erule suc)
apply (rule impI, erule lim, assumption)
done

end
```