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

lemma ord_of_nat_oexp: "ord_of_nat (m^n) = ord_of_nat m↑ord_of_nat n"
proof (induction n)
case (Suc n)
then show ?case
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)"
then show ?thesis
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
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 β"
also have "… ≤ (⨆ξ ∈ elts γ. α↑ξ)"
proof -
have "succ β ∈ elts γ"
using Limit.hyps Limit.prems Limit_def by auto
then show ?thesis
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β: "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 xβ)
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 "… ≤ (α↑β) + (α↑β)"
also have "… = (α↑β) * succ (succ 0)"
also have "… ≤ (α↑β) * α"
using Oαβ Ord_succ assms(2) assms(3) one_V_def succ_le_iff by auto
also have "… = α↑succ β"
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 "∃u∈X. 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

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 μ›
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 μ)"
also have "… = ⨆ (⋃x∈elts μ. (↑) α ` elts (β * x))"
using False Lim oexp_Limit by fastforce
also have "… = (⨆x∈elts μ. α↑(β * x))"
proof (rule Sup_eq_Sup)
show "(λx. α↑(β * x)) ` elts μ ⊆ (⋃x∈elts μ. (↑) α ` 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 ∈ (⋃x∈elts μ. (↑) α ` 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
qed
show ?thesis
using succ
apply (clarsimp simp: Limit_def mem_0_Ord)
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)"
also have "... = α * (α ↑ j)"
finally show ?thesis .
qed

lemma oexp_ω_Limit: "Limit β ⟹ ω↑β = (⨆ξ ∈ elts β. ω↑ξ)"

lemma ω_power_succ_gtr: "Ord α ⟹ ω ↑ α * ord_of_nat n < ω ↑ succ α"

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
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
```