Quelle  OrdinalInduct.thy

(*  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