Theory Ordinal_Exp

section ‹Exponentiation of ordinals›

theory Ordinal_Exp
  imports Kirby

begin

text ‹Source: Schlöder, Julian.  Ordinal Arithmetic; available online at
    \url{http://www.math.uni-bonn.de/ag/logik/teaching/2012WS/Set%20theory/oa.pdf}›

definition oexp :: "[V,V]  V" (infixr "" 80)
  where "oexp a b  transrec (λf x. if x=0 then 1
                                    else if Limit x then if a=0 then 0 else ξ  elts x. f ξ
                                    else f ((elts x)) * a)  b"

text @{term "0ω = 1"} if we don't make a special case for Limit ordinals and zero›


lemma oexp_0_right [simp]: "α0 = 1"
  by (simp add: def_transrec [OF oexp_def])

lemma oexp_succ [simp]: "Ord β  α(succ β) = αβ * α"
  by (simp add: def_transrec [OF oexp_def])

lemma oexp_Limit: "Limit β  αβ = (if α=0 then 0 else ξ  elts β. αξ)"
  by (auto simp: def_transrec [OF oexp_def, of _ β])

lemma oexp_1_right [simp]: "α1 = α"
  using one_V_def oexp_succ by fastforce

lemma oexp_1 [simp]: "Ord α  1α = 1"
  by (induction rule: Ord_induct3) (use Limit_def oexp_Limit in auto)

lemma oexp_0 [simp]: "Ord α  0α = (if α = 0 then 1 else 0)"
  by (induction rule: Ord_induct3) (use Limit_def oexp_Limit in auto)

lemma oexp_eq_0_iff [simp]:
  assumes "Ord β" shows "αβ = 0  α=0  β0"
  using Ord β
proof (induction rule: Ord_induct3)
  case (Limit μ)
  then show ?case
    using Limit_def oexp_Limit by auto
qed auto

lemma oexp_gt_0_iff [simp]:
  assumes "Ord β" shows "αβ > 0  α>0  β=0"
  by (simp add: assms less_V_def)

lemma ord_of_nat_oexp: "ord_of_nat (m^n) = ord_of_nat mord_of_nat n"
proof (induction n)
  case (Suc n)
  then show ?case
    by (simp add: mult.commute [of m]) (simp add: ord_of_nat_mult)
qed auto

lemma omega_closed_oexp [intro]:
  assumes "α  elts ω" "β  elts ω" shows "αβ  elts ω"
proof -
  obtain m n where "α = ord_of_nat m" "β = ord_of_nat n"
    using assms elts_ω by auto
  then have "αβ = ord_of_nat (m^n)"
    by (simp add: ord_of_nat_oexp)
  then show ?thesis
    by (simp add: ω_def)
qed


lemma Ord_oexp [simp]:
  assumes "Ord α" "Ord β" shows "Ord (αβ)"
  using Ord β
proof (induction rule: Ord_induct3)
  case (Limit α)
  then show ?case
    by (auto simp: oexp_Limit image_iff intro: Ord_Sup)
qed (auto intro: Ord_mult assms)

text ‹Lemma 3.19›
lemma le_oexp:
  assumes "Ord α" "Ord β" "β  0" shows "α  αβ"
  using Ord β β  0
proof (induction rule: Ord_induct3)
  case (succ β)
  then show ?case
    by simp (metis Ord α le_0 le_mult mult.left_neutral oexp_0_right order_refl order_trans)
next
  case (Limit μ)
  then show ?case
    by (metis Limit_def Limit_eq_Sup_self ZFC_in_HOL.Sup_upper eq_iff image_eqI image_ident oexp_1_right oexp_Limit replacement small_elts one_V_def)
qed auto


text ‹Lemma 3.20›
lemma le_oexp':
  assumes "Ord α" "1 < α" "Ord β" shows "β  αβ"
proof (cases "β = 0")
  case True
  then show ?thesis
    by auto
next
  case False
  show ?thesis
    using Ord β
  proof (induction rule: Ord_induct3)
    case 0
    then show ?case
      by auto
  next
    case (succ γ)
    then have "αγ * 1 < αγ * α"
      using Ord α 1 < α
      by (metis le_mult less_V_def mult.right_neutral mult_cancellation not_less_0 oexp_eq_0_iff succ.hyps)
    then have " γ < αsucc γ"
      using succ.IH succ.hyps by auto
    then show ?case
      using False Ord α 1 < α succ
      by (metis Ord_mem_iff_lt Ord_oexp Ord_succ elts_succ insert_subset less_eq_V_def less_imp_le)
  next
    case (Limit μ)
    with False 1 < α show ?case
      by (force simp: Limit_def oexp_Limit intro: elts_succ)
  qed
qed


lemma oexp_Limit_le:
  assumes "β < γ" "Limit γ" "Ord β" "α > 0" shows "αβ  αγ"
proof -
  have "Ord γ"
    using Limit_def assms(2) by blast
  with assms show ?thesis
    using Ord_mem_iff_lt ZFC_in_HOL.Sup_upper oexp_Limit by auto
qed

proposition oexp_less:
  assumes β: "β  elts γ" and "Ord γ" and α: "α > 1" "Ord α" shows "αβ < αγ"
proof -
  obtain "β < γ" "Ord β"
    using Ord_in_Ord OrdmemD assms by auto
  have gt0: "αβ > 0"
    using Ord β α dual_order.order_iff_strict by auto
  show ?thesis
    using Ord γ β
  proof (induction rule: Ord_induct3)
    case 0
    then show ?case
      by auto
  next
    case (succ δ)
    then consider "β = δ" | "β < δ"
      using OrdmemD elts_succ by blast
    then show ?case
    proof cases
      case 1
      then have "(αβ) * 1 < (αδ) * α"
        using Ord_1 Ord_oexp α gt0 mult_cancel_less_iff succ.hyps by metis
      then show ?thesis
        by (simp add: succ.hyps)
    next
      case 2
      then have "(αδ) * 1 < (αδ) * α"
        by (meson Ord_1 Ord_mem_iff_lt Ord_oexp Ord β α gt0 less_trans mult_cancel_less_iff succ)
      with 2 show ?thesis
        using Ord_mem_iff_lt Ord β succ by auto
    qed
  next
    case (Limit γ)
    then obtain "Ord γ" "succ β < γ"
      using Limit_def Ord_in_Ord OrdmemD assms by auto
    have "αβ = (αβ) * 1"
      by simp
    also have " < (αβ) * α"
      using Ord_oexp Ord β assms gt0 mult_cancel_less_iff by blast
    also have " = αsucc β"
      by (simp add: Ord β)
    also have "  (ξ  elts γ. αξ)"
    proof -
      have "succ β  elts γ"
        using Limit.hyps Limit.prems Limit_def by auto
      then show ?thesis
        by (simp add: ZFC_in_HOL.Sup_upper)
    qed
    finally
    have "αβ < (ξ  elts γ. αξ)" .
    then show ?case
      using Limit.hyps oexp_Limit α > 1 by auto
  qed
qed

corollary oexp_less_iff:
  assumes "α > 0" "Ord α" "Ord β" "Ord γ" shows "αβ < αγ  β  elts γ  α > 1"
proof safe
  show "β  elts γ" "1 < α"
    if "αβ < αγ"
  proof -
    show "α > 1"
    proof (rule ccontr)
      assume "¬ α > 1"
      then consider "α=0" | "α=1"
        using Ord α less_V_def mem_0_Ord by fastforce
      then show False
        by cases (use that α > 0 Ord β Ord γ in auto split: if_split_asm)
    qed
    show β: "β  elts γ"
    proof (rule ccontr)
      assume "β  elts γ"
      then have "γ  β"
        by (meson Ord_linear_le Ord_mem_iff_lt assms less_le_not_le)
      then consider "γ = β" | "γ < β"
        using less_V_def by blast
      then show False
      proof cases
        case 1
        then show ?thesis
          using that by blast
      next
        case 2
        with α > 1 have "αγ < αβ"
          by (simp add: Ord_mem_iff_lt assms oexp_less)
        with that show ?thesis
          by auto
      qed
    qed
  qed
  show "αβ < αγ" if "β  elts γ" "1 < α"
    using that by (simp add: assms oexp_less)
qed

lemma ω_oexp_iff [simp]: "Ord α; Ord β  ωα = ωβ  α=β"
  by (metis Ord_ω Ord_linear ω_gt1 less_irrefl oexp_less)

lemma Limit_oexp:
  assumes "Limit γ" "Ord α" "α > 1" shows "Limit (αγ)"
  unfolding Limit_def
proof safe
  show Oαγ: "Ord (αγ)"
    using Limit_def Ord_oexp Limit γ assms(2) by blast
  show 0: "0  elts (αγ)"
    using Limit_def oexp_Limit Limit γ α > 1 by fastforce
  have "Ord γ"
    using Limit_def Limit γ by blast
  fix x
  assume x: "x  elts (αγ)"
  with Limit γ α > 1
  obtain β where "β < γ" "Ord β" "Ord x" and : "x  elts (αβ)"
    apply (simp add: oexp_Limit split: if_split_asm)
    using Ord_in_Ord OrdmemD Ord γ Oαγ x by blast
  then have Oαβ: "Ord (αβ)"
    using Ord_oexp assms(2) by blast
  have "β  elts γ"
    by (simp add: Ord_mem_iff_lt Ord β Ord γ β < γ)
  moreover have "α  0"
    using α > 1 by blast
  ultimately have αβγ: "αβ  αγ"
    by (simp add: Sup_upper oexp_Limit Limit γ)
  have "succ x  αβ"
    by (simp add: OrdmemD Oαβ Ord x succ_le_iff )
  then consider "succ x < αβ" | "succ x = αβ"
    using le_neq_trans by blast
  then show "succ x  elts (αγ)"
  proof cases
    case 1
    with αβγ show ?thesis
      using Oαβ Ord_mem_iff_lt Ord x by blast
  next
    case 2
    then have "succ β < γ"
      using Limit_def OrdmemD β  elts γ assms(1) by auto
    have ge1: "1  αβ"
      by (metis "2" Ord_0 Ord x le_0 le_succ_iff one_V_def)
    have "succ x < succ (αβ)"
      using "2" Oαβ succ_le_iff by auto
    also have "  (αβ) + (αβ)"
      using ge1 by (simp add: succ_eq_add1)
    also have " = (αβ) * succ (succ 0)"
      by (simp add: mult_succ)
    also have "  (αβ) * α"
      using Oαβ Ord_succ assms(2) assms(3) one_V_def succ_le_iff by auto
    also have " = αsucc β"
      by (simp add: Ord β)
    also have "  αγ"
      by (meson Limit_def β  elts γ assms dual_order.order_iff_strict oexp_less)
  finally show ?thesis
    by (simp add: "2" Oαβ Oαγ Ord_mem_iff_lt)
  qed
qed



lemma oexp_mono:
  assumes α: "Ord α" "α  0" and β: "Ord β" "γ  β" shows "αγ  αβ"
  using β
proof (induction rule: Ord_induct3)
  case 0
  then show ?case
    by simp
next
  case (succ β)
  with α le_mult show ?case
    by (auto simp: le_TC_succ)
next
  case (Limit μ)
  then have "αγ   ((↑) α ` elts μ)"
    using Limit.hyps Ord_less_TC_mem α  0 le_TC_def by (auto simp: oexp_Limit Limit_def)
  then show ?case
    using α by (simp add: oexp_Limit Limit.hyps)
qed

lemma oexp_mono_le:
  assumes "γ  β" "α  0" "Ord α" "Ord β" "Ord γ" shows "αγ  αβ"
  by (simp add: assms oexp_mono vle2 vle_iff_le_Ord)

lemma oexp_sup:
  assumes "α  0" "Ord α" "Ord β" "Ord γ" shows "α(β  γ) = αβ  αγ"
  by (metis Ord_linear_le assms oexp_mono_le sup.absorb2 sup.orderE)

lemma oexp_Sup:
  assumes α: "α  0" "Ord α" and X: "X  ON" "small X" "X  {}" shows "α X =  ((↑) α ` X)"
proof (rule order_antisym)
  show " ((↑) α ` X)  α X"
    by (metis ON_imp_Ord Ord_Sup ZFC_in_HOL.Sup_upper assms cSUP_least oexp_mono_le)
next
  have "Ord (Sup X)"
    using Ord_Sup X by auto
  then show "α X   ((↑) α ` X)"
  proof (cases rule: Ord_cases)
    case 0
    then show ?thesis
      using X dual_order.antisym by fastforce
  next
    case (succ β)
    then show ?thesis
      using ZFC_in_HOL.Sup_upper X succ_in_Sup_Ord by auto
  next
    case limit
    show ?thesis
    proof (clarsimp simp: assms oexp_Limit limit)
      fix x y z
      assume x: "x  elts (α  y)" and "z  X" "y  elts z"
      then have "α  y  α  z"
        by (meson ON_imp_Ord Ord_in_Ord OrdmemD α X  ON le_less oexp_mono_le)
      with x have "x  elts (α  z)" by blast
      then show "uX. x  elts (α  u)"
        using z  X by blast
    qed
  qed
qed


lemma omega_le_Limit:
  assumes "Limit μ" shows "ω  μ"
proof
  fix ρ
  assume "ρ  elts ω"
  then obtain n where "ρ = ord_of_nat n"
    using elts_ω by auto
  have "ord_of_nat n  elts μ"
    by (induction n) (use Limit_def assms in auto)
  then show "ρ  elts μ"
    using ρ = ord_of_nat n by auto
qed

lemma finite_omega_power [simp]:
  assumes "1 < n" "n  elts ω" shows "nω = ω"
proof (rule order_antisym)
  have " ((↑) (ord_of_nat k) ` elts ω)  ω" for k
  proof (induction k)
    case 0
    then show ?case
      by auto
  next
    case (Suc k)
    then show ?case
      by (metis Ord_ω OrdmemD Sup_eq_0_iff ZFC_in_HOL.SUP_le_iff le_0 le_less omega_closed_oexp ord_of_nat_ω)
  qed
  then show "nω  ω"
    using assms
    by (simp add: elts_ω oexp_Limit) metis
  show "ω  nω"
    using Ord_in_Ord assms le_oexp' by blast
qed


proposition oexp_add:
  assumes "Ord α" "Ord β" "Ord γ" shows "α(β + γ) = αβ * αγ"
proof (cases α = 0)
  case True
  then show ?thesis
    using assms by simp
next
  case False
  show ?thesis
    using Ord γ
  proof (induction rule: Ord_induct3)
    case 0
    then show ?case
      by auto
  next
    case (succ ξ)
    then show ?case
      using Ord β by (auto simp: plus_V_succ_right mult.assoc)
  next
    case (Limit μ)
    have "α(β + (ξelts μ. ξ)) = (ξelts (β + μ). αξ)"
      by (simp add: Limit.hyps oexp_Limit assms False)
    also have " = (ξ  {ξ. Ord ξ  β + ξ < β + μ}. α(β + ξ))"
    proof (rule Sup_eq_Sup)
      show "(λξ. α(β + ξ)) ` {ξ. Ord ξ  β + ξ < β + μ}  (↑) α ` elts (β + μ)"
        using Limit.hyps Limit_def Ord_mem_iff_lt imageI by blast
      fix x
      assume "x  (↑) α ` elts (β + μ)"
      then obtain ξ where ξ: "ξ  elts (β + μ)" and x: "x = αξ"
        by auto
      have "γ. Ord γ  γ < μ  αξ  α(β + γ)"
      proof (rule mem_plus_V_E [OF ξ])
        assume "ξ  elts β"
        then have "αξ  αβ"
          by (meson arg_subset_TC assms False le_TC_def less_TC_def oexp_mono vsubsetD)
        with zero_less_Limit [OF Limit μ]
        show "γ. Ord γ  γ < μ  αξ  α(β + γ)"
          by force
      next
        fix δ
        assume "δ  elts μ" and "ξ = β + δ"
        have "Ord δ"
          using Limit.hyps Limit_def Ord_in_Ord δ  elts μ by blast
        moreover have "δ < μ"
          using Limit.hyps Limit_def OrdmemD δ  elts μ by auto
        ultimately show "γ. Ord γ  γ < μ  αξ  α(β + γ)"
          using ξ = β + δ by blast
      qed
      then show "y(λξ. α(β + ξ)) ` {ξ. Ord ξ  β + ξ < β + μ}. x  y"
        using x by auto
    qed auto
    also have " = (ξelts μ. α(β + ξ))"
      using Limit μ
      by (simp add: Ord_Collect_lt Limit_def)
    also have " = (ξelts μ. αβ * αξ)"
      using Limit.IH by auto
    also have " = αβ * α(ξelts μ. ξ)"
      using α  0 Limit.hyps
      by (simp add: image_image oexp_Limit mult_Sup_distrib)
    finally show ?case .
  qed
qed

proposition oexp_mult:
  assumes "Ord α" "Ord β" "Ord γ" shows "α(β * γ) = (αβ)γ"
proof (cases "α = 0  β = 0")
  case True
  then show ?thesis
    by (auto simp: Ord β Ord γ)
next
  case False
  show ?thesis
    using Ord γ
  proof (induction rule: Ord_induct3)
    case 0
    then show ?case
      by auto
  next
    case succ
    then show ?case
      using assms by (auto simp: mult_succ oexp_add)
  next
    case (Limit μ)
    have Lim: "Limit ( ((*) β ` elts μ))"
      unfolding Limit_def
    proof (intro conjI allI impI)
      show "Ord ( ((*) β ` elts μ))"
        using Limit.hyps Limit_def Ord_in_Ord Ord β by (auto intro: Ord_Sup)
      have "succ 0  elts μ"
        using Limit.hyps Limit_def by blast
      then show "0  elts ( ((*) β ` elts μ))"
        using False Ord β mem_0_Ord by force
      show "succ y  elts ( ((*) β ` elts μ))"
        if "y  elts ( ((*) β ` elts μ))" for y
        using that False Limit.hyps
        apply (clarsimp simp: Limit_def)
        by (metis Ord_in_Ord Ord_linear Ord_mem_iff_lt Ord_mult Ord_succ assms(2) less_V_def mult_cancellation mult_succ not_add_mem_right succ_le_iff succ_ne_self)
    qed
    have "α(β * (ξelts μ. ξ)) = α ((*) β ` elts μ)"
      by (simp add: mult_Sup_distrib)
    also have " =  (xelts μ. (↑) α ` elts (β * x))"
      using False Lim oexp_Limit by fastforce
    also have " = (xelts μ. α(β * x))"
    proof (rule Sup_eq_Sup)
      show "(λx. α(β * x)) ` elts μ  (xelts μ. (↑) α ` elts (β * x))"
        using Ord α Ord β False Limit
        apply clarsimp
        by (metis Limit_def elts_succ imageI insertI1 mem_0_Ord mult_add_mem_0)
      show "y(λx. α(β * x)) ` elts μ. x  y"
        if "x  (xelts μ. (↑) α ` elts (β * x))" for x
        using that Ord α Ord β False Limit
        by clarsimp (metis Limit_def Ord_in_Ord Ord_mult VWO_TC_le mem_imp_VWO oexp_mono)
    qed auto
    also have " =  ((↑) (αβ) ` elts (ξelts μ. ξ))"
      using Limit.IH Limit.hyps by auto
    also have " = (αβ)(ξelts μ. ξ)"
      using False Limit.hyps oexp_Limit Ord β by auto
    finally show ?case .
  qed
qed

lemma Limit_omega_oexp:
  assumes "Ord δ" "δ  0"
  shows "Limit (ωδ)"
  using assms
proof (cases δ rule: Ord_cases)
  case 0
  then show ?thesis
    using assms(2) by blast
next
  case (succ l)
  have *: "succ β  elts (ωl * n + ωl)"
    if n: "n  elts ω" and β: "β  elts (ωl * n)" for n β
  proof -
    obtain "Ord n" "Ord β"
      by (meson Ord_ω Ord_in_Ord Ord_mult Ord_oexp β n succ(1))
    obtain oo: "Ord (ωl)" "Ord (ωl * n)"
      by (simp add: Ord n succ(1))
    moreover have f4: "β < ωl * n"
      using oo Ord_mem_iff_lt Ord β β  elts (ωl * n) by blast
    moreover have f5: "Ord (succ β)"
      using Ord β by blast
    moreover have "ωl  0"
      using oexp_eq_0_iff omega_nonzero succ(1) by blast
    ultimately show ?thesis
      by (metis add_less_cancel_left Ord_ω Ord_add Ord_mem_iff_lt OrdmemD Ord β add.right_neutral dual_order.strict_trans2 oexp_gt_0_iff succ(1) succ_le_iff zero_in_omega)
  qed
  show ?thesis
    using succ
    apply (clarsimp simp: Limit_def mem_0_Ord)
    apply (simp add: mult_Limit)
    by (metis * mult_succ succ_in_omega)
next
  case limit
  then show ?thesis
    by (metis Limit_oexp Ord_ω OrdmemD one_V_def succ_in_omega zero_in_omega)
qed

lemma oexp_mult_commute:
  fixes j::nat
  assumes "Ord α"
  shows "(α  j) * α = α * (α  j)"
proof -
  have "(α  j) * α = α  (1 + ord_of_nat j)"
    by (simp add: one_V_def)
  also have "... = α * (α  j)"
    by (simp add: assms oexp_add)
  finally show ?thesis .
qed

lemma oexp_ω_Limit: "Limit β  ωβ = (ξ  elts β. ωξ)"
  by (simp add: oexp_Limit)

lemma ω_power_succ_gtr: "Ord α  ω  α * ord_of_nat n < ω  succ α"
  by (simp add: OrdmemD)

lemma countable_oexp:
  assumes ν: "α  elts ω1" 
  shows "ω  α  elts ω1"
proof -
  have "Ord α"
    using Ord_ω1 Ord_in_Ord assms by blast
  then show ?thesis
    using assms
  proof (induction rule: Ord_induct3)
    case 0
    then show ?case
      by (simp add: Ord_mem_iff_lt)
  next
    case (succ α)
    then have "countable (elts (ω  α * ω))"
      by (simp add: succ_in_Limit_iff countable_mult less_ω1_imp_countable)
    then show ?case
      using Ord_mem_iff_lt countable_iff_less_ω1 succ.hyps by auto
  next
    case (Limit α)
    with Ord_ω1 have "countable (βelts α. elts (ω  β))" "Ord (ω   (elts α))"
      by (force simp: Limit_def intro: Ord_trans less_ω1_imp_countable)+
    then have "ω   (elts α) < ω1"
      using Limit.hyps countable_iff_less_ω1 oexp_Limit by fastforce
    then show ?case
      using Limit.hyps Limit_def Ord_mem_iff_lt by auto
  qed
qed

end