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"
  by (simp add: oStrictLimit_lub oSuc_def)

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)"
  by (simp add: oZero_least ordinal_zero_def)

lemma ordinal_not_less_0 [iff]: "¬ (x::ordinal) < 0"
  by (simp add: linorder_not_less)

lemma ordinal_le_0 [iff]: "(x ≤ 0) = (x = (0::ordinal))"
  by (simp add: order_le_less)

lemma ordinal_neq_0 [iff]: "(x ≠ 0) = (0 < (x::ordinal))"
  by (simp add: order_less_le)

lemma ordinal_not_0_less [iff]: "(¬ 0 < x) = (x = (0::ordinal))"
  by (simp add: linorder_not_less)

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)"
  by (simp add: less_oSuc_eq_le)

lemma oSuc_less_oSuc [iff]: "(oSuc x < oSuc y) = (x < y)"
  by (simp add: less_oSuc_eq_le oSuc_le_eq_less)

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)"
  by (simp add: order_le_less)

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"
  by (simp add: mono_iff_le_Suc)

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"
  by (simp add: oLimit_def wellorder_Least_lemma(2))

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"
  by (meson le_add1 monoD oLimit_eqI)


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"
  by (simp add: limit_ordinal_def)

lemma zero_less_limit_ordinal [simp]: "limit_ordinal x ⟹ 0 < x"
  by (simp add: limit_ordinal_def)

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

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)"
  by (simp add: limit_ordinal_oLimitI strict_mono_less_oLimit)

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 (auto simp add: order_le_less)
  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