Theory OrdinalInduct

(*  Title:       Countable Ordinals

    Author:      Brian Huffman, 2005
    Maintainer:  Brian Huffman <brianh at>

section ‹Ordinal Induction›

theory OrdinalInduct
imports OrdinalDef

subsection ‹Zero and successor ordinals›

  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}"

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

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

instance ..


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›

  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"

  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"
    "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)

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)