Theory CZH_Sets_Ordinals

(* Copyright 2021 (C) Mihails Milehins *)

section‹Further results about ordinal numbers›
theory CZH_Sets_Ordinals


The subsection presents several results about ordinal 
numbers. The primary general reference for this section 
is cite"takeuti_introduction_1971".

lemmas [intro] = Limit_is_Ord Ord_in_Ord

subsection‹Further ordinal arithmetic and inequalities›

lemma Ord_succ_mono:
  assumes "Ord β" and "α  β"
  shows "succ α  succ β"
  from assms have "Ord α" by blast
  from assms Ord α have "α < β" by (auto dest: Ord_mem_iff_lt)
  from assms(1,2) this have "succ α < succ β"
    by (meson assms Ord α Ord_linear2 Ord_succ leD le_succ_iff)
  with assms(1) Ord α Ord_mem_iff_lt show "succ α  succ β" by blast

lemma Limit_right_Limit_mult:
  ―‹Based on Theorem 8.23 in \cite{takeuti_introduction_1971}.›
  assumes "Ord α" and "Limit β" and "0  α" 
  shows "Limit (α * β)"
  have αβ: "α * β = (ξβ. α * ξ)" by (rule mult_Limit[OF assms(2), of α])
  from assms(1,2) Ord_mult have "Ord (α * β)" by blast
  then show ?thesis 
  proof(cases rule: Ord_cases)
    case (succ γ)
    from succ(1) have "γ  α * β" unfolding succ(2)[symmetric] by simp
    then obtain ξ where "ξ  β" and "γ  α * ξ" unfolding αβ by auto
    moreover with assms(2) have "Ord ξ" by auto
    ultimately have sγ_sαξ: "succ γ  succ (α * ξ)"
      using assms(1) Ord_succ_mono by simp
    from assms(2,3) have "succ (α * ξ)  α * ξ + α" 
      unfolding succ_eq_add1 by force
    with sγ_sαξ have "succ γ  α * succ ξ" 
      unfolding mult_succ[symmetric] by auto
    moreover have "succ ξ  β" 
      by (simp add: succ_in_Limit_iff ξ  β assms(2))
    ultimately have "succ γ  α * β" unfolding αβ by force
    with succ(2) show ?thesis by simp
  qed (use assms(2,3) in auto)

lemma Limit_left_Limit_mult:
  assumes "Limit α" and "Ord β" and "0  β" 
  shows "Limit (α * β)"
proof(cases Limit β)
  case False
  then obtain β' where "Ord β'" and β_def: "β = succ β'" 
    by (metis Ord_cases assms(2,3) eq0_iff)
  have α_sβ': "α * succ β' = α * β' + α" by (simp add: mult_succ)
  from assms(1) have "Limit (α * β' + α)" by (simp add: Limit_is_Ord Ord β')
  then show "Limit (α * β)" unfolding β_def α_sβ' by simp
qed (use assms in auto simp: Limit_def dest: Limit_right_Limit_mult)

lemma zero_if_Limit_eq_Limit_plus_vnat:
  assumes "Limit α" and "Limit β" and "α = β + n" and "n  ω"
  shows "n = 0"
proof(rule ccontr)
  assume prems: "n  0"
  from assms(1,2,4) have "Ord α" and "Ord β" and "Ord 0" and "Ord n" by auto
  have "0  n" by (simp add: mem_0_Ord prems assms(4)) 
  with assms(4) obtain m where n_def: "n = succ m" by (auto elim: omega_prev)
  from assms(1,3) show False by (simp add: n_def plus_V_succ_right)

lemma Ord_vsubset_closed: 
  assumes "Ord α" and "Ord γ" and "α  β" and "β  γ" 
  shows "α  γ" 
  from assms have "Ord β" by auto
  with assms show ?thesis by (simp add: Ord_mem_iff_lt)

  ―‹Based on Exercise 1, page 53 in \cite{takeuti_introduction_1971}.›
  assumes "Ord α" and "Ord γ" and "α + β  γ" 
  shows Ord_plus_Ord_closed_augend: "α  γ" 
    and Ord_plus_Ord_closed_addend: "β  γ"
  from assms have "α + β  α + γ" by (meson vsubsetD add_le_left)
  from add_mem_right_cancel[THEN iffD1, OF this] show "β  γ" .
  from assms have "α  α + β" by simp
  from Ord_vsubset_closed[OF assms(1,2) this assms(3)] show "α  γ" .

lemma Ord_ex1_Limit_plus_in_omega:
  ―‹Based on Theorem 8.13 in \cite{takeuti_introduction_1971}.›
  assumes "Ord α" and "ω  α"
  shows "∃!β. ∃!n. n  ω  Limit β  α = β + n"
  let ?A = set {γ. Limit γ  γ  α}
  have small[simp]: "small {γ. Limit γ  γ  α}"
    from Ord_mem_iff_lt  have "{γ. Limit γ  γ  α}  elts (succ α)"
      by (auto dest: order.not_eq_order_implies_strict intro: assms(1))
    then show "small {γ. Limit γ  γ  α}" by (meson down)
  let  = ?A
  have "  α" by auto
  moreover have L_β: "Limit "
  proof(subst Limit_def, intro conjI allI impI)
    show "Ord " by (fastforce intro: Ord_Sup)
    from assms(2) show "0  " by auto
    fix y assume "y  "
    then obtain γ where "y  γ" and "γ  ?A" by clarsimp
    then show "succ y  " by (auto simp: succ_in_Limit_iff)
  ultimately obtain γ where "Ord γ" and α_def: "α =  + γ"
    by (metis assms(1) le_Ord_diff Limit_is_Ord)
  from L_β have L_βω: "Limit ( + ω)" by (blast intro: Limit_add_Limit)
  have "γ  ω"
  proof(rule ccontr)
    assume "~γ  ω"
    with Ord γ Ord_linear2 have "ω  γ" by auto
    then obtain δ where γ_def: "γ = ω + δ" 
      by (blast dest: Ord_odiff_eq intro: Ord γ)
    from α_def have "α = ( + ω) + δ" by (simp add: add.assoc γ_def)
    then have " + ω  α" by (metis add_le_cancel_left0)
    with L_βω have " + ω  " by auto
    with add_le_cancel_left[of  ω 0, THEN iffD1] show False by simp
  with α_def have "γ  ω" by (auto simp: Ord_mem_iff_lt Ord γ)
  show ?thesis
      intro ex1I conjI; 
      (elim conjE ex1E allE conjE impE | tacticall_tac);
      (intro conjI | tacticall_tac)
    show "γ  ω" by (rule γ  ω)
    show "Limit " by (rule Limit )
    show "α =  + γ" by (rule α_def)
    from α_def show "α =  + n  n = γ" for n by auto
    show "n  ω  Limit β  α = β + n  β = " for n β
      assume prems: "n  ω" "Limit β" "α = β + n"
      from L_β prems(2,3) have "β  " by auto
      then obtain η where β_def: " = β + η" and "Ord η" 
        by (metis (lifting) L_β Limit_is_Ord le_Ord_diff prems(2))
      moreover have "η  ω"
        from α_def β_def have "β + η + γ = β + n" by (simp add: prems(3))
        then have "η + γ = n" by (simp add: add.assoc)
        with γ  ω n  ω Ord γ show "η  ω"
          by (blast intro: calculation(2) Ord_plus_Ord_closed_augend)
      ultimately show ?thesis 
        using prems(2) L_β by (force dest: zero_if_Limit_eq_Limit_plus_vnat)

lemma not_Limit_if_in_Limit_plus_omega:
  assumes "Limit α" and "α  β" and "β  α + ω"
  shows "~Limit β"
  from assms Ord_add have "Ord β" by blast
  show ?thesis
    using assms(3)
  proof(cases rule: mem_plus_V_E)
    case 1 with mem_not_sym show ?thesis by (auto simp: assms(2,3))
    case (2 z)
    from zero_if_Limit_eq_Limit_plus_vnat[OF _ assms(1) 2(2) 2(1)] 2(2) assms(2) 
    show ?thesis  
      by force

lemma Limit_plus_omega_vsubset_Limit: 
  assumes "Limit α" and "Limit β" and "α  β"
  shows "α + ω  β"
  from assms(1) have Lαω: "Limit (α + ω)" by (simp add: Limit_is_Ord)
  from not_Limit_if_in_Limit_plus_omega[OF assms(1,3)] assms(2) have
    "β  α + ω"
    by clarsimp
  with assms(2) have "~β  α + ω"
    by (blast intro: Lαω dest: Ord_mem_iff_lt Limit_is_Ord)
  then show "α + ω  β" by (meson assms Lαω Limit_is_Ord Ord_linear2)

lemma Limit_plus_nat_in_Limit:
  assumes "Limit α" and "Limit β" and "α  β"
  shows "α + a  β"
  using assms Limit_plus_omega_vsubset_Limit[OF assms] by auto

lemma omega2_vsubset_Limit:
  assumes "Limit α" and "ω  α"
  shows "ω + ω  α"
  using assms by (simp add: Limit_plus_omega_vsubset_Limit)