# Theory OrdinalVeblen

(*  Title:       Countable Ordinals
Author:      Brian Huffman, 2005
Maintainer:  Brian Huffman <brianh at cse.ogi.edu>
*)

section ‹Veblen Hierarchies›

theory OrdinalVeblen
imports OrdinalOmega
begin

subsection ‹Closed, unbounded sets›

locale normal_set =
fixes A :: "ordinal set"
assumes closed:    "⋀g. ∀n. g n ∈ A ⟹ oLimit g ∈ A"
and unbounded: "⋀x. ∃y∈A. x < y"

lemma (in normal_set) less_next: "x < (LEAST z. z ∈ A ∧ x < z)"
by (metis (no_types, lifting) LeastI unbounded)

lemma (in normal_set) mem_next: "(LEAST z. z ∈ A ∧ x < z) ∈ A"
by (metis (no_types, lifting) LeastI unbounded)

lemma (in normal) normal_set_range: "normal_set (range F)"
proof (rule normal_set.intro)
fix g :: "nat ⇒ ordinal"
assume "∀n. g n ∈ range F"
then have "⋀n. g n = F (LEAST z. g n = F z)"
by (meson LeastI rangeE)
then have "oLimit g = F (oLimit (λn. LEAST z. g n = F z))"
then show "oLimit g ∈ range F"
by simp
next
show "⋀x. ∃y∈range F. x < y"
using oInv_bound2 by blast
qed

lemma oLimit_mem_INTER:
assumes norm: "∀n. normal_set (A n)"
and A: "∀n. A (Suc n) ⊆ A n" "∀n. f n ∈ A n" and "mono f"
shows "oLimit f ∈ (⋂n. A n)"
proof
fix k
have "f (n + k) ∈ A k" for n
using A le_add2 lift_Suc_antimono_le by blast
then have "oLimit (λn. f (n + k)) ∈ A k"
then show "oLimit f ∈ A k"
by (simp add: ‹mono f› oLimit_shift_mono)
qed

lemma normal_set_INTER:
assumes norm: "∀n. normal_set (A n)"  and A: "∀n. A (Suc n) ⊆ A n"
shows "normal_set (⋂n. A n)"
proof (rule normal_set.intro)
fix g :: "nat ⇒ ordinal"
assume "∀n. g n ∈ ⋂ (range A)"
then show "oLimit g ∈ ⋂ (range A)"
using norm normal_set.closed by force
next
fix x
define F where "F ≡ λn. LEAST y. y ∈ A n ∧ x < y"
have "x < oLimit F"
by (simp add: F_def less_oLimitI norm normal_set.less_next)
moreover
have §: "F n ∈ A n" for n
by (simp add: F_def norm normal_set.mem_next)
then have "F n ≤ F (Suc n)" for n
unfolding F_def
by (metis (no_types, lifting) A LeastI Least_le norm normal_set_def subsetD)
then have "oLimit F ∈ ⋂ (range A)"
by (meson "§" A mono_natI norm oLimit_mem_INTER)
ultimately show "∃y∈⋂ (range A). x < y"
by blast
qed

subsection ‹Ordering functions›

text "There is a one-to-one correspondence between closed,
unbounded sets of ordinals and normal functions on ordinals."

definition
ordering  :: "(ordinal set) ⇒ (ordinal ⇒ ordinal)" where
"ordering A = ordinal_rec (LEAST z. z ∈ A) (λp x. LEAST z. z ∈ A ∧ x < z)"

lemma ordering_0:
"ordering A 0 = (LEAST z. z ∈ A)"

lemma ordering_oSuc:
"ordering A (oSuc x) = (LEAST z. z ∈ A ∧ ordering A x < z)"

lemma (in normal_set) normal_ordering: "normal (ordering A)"
by (simp add: OrdinalVeblen.ordering_def normal_ordinal_rec normal_set.less_next normal_set_axioms)

lemma (in normal_set) ordering_oLimit: "ordering A (oLimit f) = oLimit (λn. ordering A (f n))"

lemma (in normal) ordering_range: "ordering (range F) = F"
proof
fix x
show "ordering (range F) x = F x"
proof (induction x rule: oLimit_induct)
case zero
have "(LEAST z. z ∈ range F) = F 0"
by (metis Least_equality Least_mono UNIV_I mono ordinal_0_le)
then show ?case
next
case (suc x)
have "ordering (range F) (oSuc x) = (LEAST z. z ∈ range F ∧ F x < z)"
also have "… = F (oSuc x)"
using cancel_less less_oInvD oInv_inverse
by (bestsimp intro!: Least_equality local.strict_monoD)
finally show ?case .
next
case (lim f)
then show ?case
using oLimit by (simp add: normal_set_range normal_set.ordering_oLimit)
qed
qed

lemma (in normal_set) ordering_mem: "ordering A x ∈ A"
proof (induction x rule: oLimit_induct)
case zero
then show ?case
by (metis LeastI ordering_0 unbounded)
next
case (suc x)
then show ?case
next
case (lim f)
then show ?case
by (simp add: closed normal.oLimit normal_ordering)
qed

lemma (in normal_set) range_ordering: "range (ordering A) = A"
proof -
have "∀y. y ∈ A ⟶ y < ordering A x ⟶ y ∈ range (ordering A)" for x
proof (induction x rule: oLimit_induct)
case zero
then show ?case
using not_less_Least ordering_0 by auto
next
case (suc x)
then show ?case
using not_less_Least ordering_oSuc by fastforce
next
case (lim f)
then show ?case
by (metis less_oLimitD ordering_oLimit)
qed
then show ?thesis
using normal.oInv_bound2 normal_ordering ordering_mem by fastforce
qed

lemma ordering_INTER_0:
assumes norm: "∀n. normal_set (A n)"  and A: "∀n. A (Suc n) ⊆ A n"
shows "ordering (⋂n. A n) 0 = oLimit (λn. ordering (A n) 0)"
proof -
have "oLimit (λn. OrdinalVeblen.ordering (A n) 0) ∈ ⋂ (range A)"
using assms
by (metis (mono_tags, lifting) Least_le mono_natI normal_set.ordering_mem oLimit_mem_INTER ordering_0 subsetD)
moreover have "⋀y. y ∈ ⋂ (range A) ⟹ oLimit (λn. ordering (A n) 0) ≤ y"
by (simp add: Least_le oLimit_def ordering_0)
ultimately show ?thesis
by (metis LeastI Least_le nle_le ordering_0)
qed

subsection ‹Critical ordinals›

definition
critical_set :: "ordinal set ⇒ ordinal ⇒ ordinal set" where
"critical_set A =
ordinal_rec0 A (λp x. x ∩ range (oDeriv (ordering x))) (λf. ⋂n. f n)"

lemma critical_set_0 [simp]: "critical_set A 0 = A"

lemma critical_set_oSuc_lemma:
"critical_set A (oSuc n) = critical_set A n ∩ range (oDeriv (ordering (critical_set A n)))"

lemma omega_complete_INTER: "omega_complete (λx y. y ⊆ x) (λf. ⋂ (range f))"
by (simp add: INF_greatest Inf_lower omega_complete_axioms_def omega_complete_def porder.flip porder_order)

lemma critical_set_oLimit: "critical_set A (oLimit f) = (⋂n. critical_set A (f n))"
unfolding critical_set_def
by (best intro!: omega_complete.ordinal_rec0_oLimit omega_complete_INTER)

lemma critical_set_mono: "x ≤ y ⟹ critical_set A y ⊆ critical_set A x"
unfolding critical_set_def
by (intro omega_complete.ordinal_rec0_mono [OF omega_complete_INTER]) force

lemma (in normal_set) range_oDeriv_subset: "range (oDeriv (ordering A)) ⊆ A"
by (metis image_subsetI normal_ordering oDeriv_fixed rangeI range_ordering)

lemma normal_set_critical_set: "normal_set A ⟹ normal_set (critical_set A x)"
proof (induction x rule: oLimit_induct)
case zero
then show ?case
by simp
next
case (suc x)
then show ?case
by (simp add: Int_absorb1 critical_set_oSuc_lemma normal.normal_set_range normal_oDeriv normal_set.range_oDeriv_subset)
next
case (lim f)
then show ?case
unfolding critical_set_oLimit
by (meson critical_set_mono lessI normal_set_INTER order_le_less strict_mono.strict_mono)
qed

lemma critical_set_oSuc:
"normal_set A ⟹ critical_set A (oSuc x) = range (oDeriv (ordering (critical_set A x)))"
by (metis critical_set_oSuc_lemma inf.absorb_iff2 normal_set.range_oDeriv_subset normal_set_critical_set)

subsection ‹Veblen hierarchy over a normal function›

definition
oVeblen :: "(ordinal ⇒ ordinal) ⇒ ordinal ⇒ ordinal ⇒ ordinal" where
"oVeblen F = (λx. ordering (critical_set (range F) x))"

lemma (in normal) oVeblen_0: "oVeblen F 0 = F"
by (simp add: normal.ordering_range normal_axioms oVeblen_def)

lemma (in normal) oVeblen_oSuc: "oVeblen F (oSuc x) = oDeriv (oVeblen F x)"
using critical_set_oSuc normal.normal_set_range normal.ordering_range normal_axioms normal_oDeriv oVeblen_def by presburger

lemma (in normal) oVeblen_oLimit:
"oVeblen F (oLimit f) = ordering (⋂n. range (oVeblen F (f n)))"
unfolding oVeblen_def
using critical_set_oLimit normal_set.range_ordering normal_set_critical_set normal_set_range by presburger

lemma (in normal) normal_oVeblen: "normal (oVeblen F x)"
unfolding oVeblen_def
by (simp add: normal_set.normal_ordering normal_set_critical_set normal_set_range)

lemma (in normal) continuous_oVeblen_0: "continuous (λx. oVeblen F x 0)"
proof (rule continuousI)
fix f:: "nat ⇒ ordinal"
assume f: "OrdinalInduct.strict_mono f"
have "normal_set (critical_set (range F) (f n))" for n
using normal_set_critical_set normal_set_range by blast
moreover
have "critical_set (range F) (f (Suc n)) ⊆ critical_set (range F) (f n)" for n
by (simp add: f critical_set_mono strict_mono_monoD)
ultimately show "oVeblen F (oLimit f) 0 = oLimit (λn. oVeblen F (f n) 0)"
using ordering_INTER_0 by (simp add: oVeblen_def critical_set_oLimit)
next
show "⋀x. oVeblen F x 0 ≤ oVeblen F (oSuc x) 0"
qed

lemma (in normal) oVeblen_oLimit_0:
"oVeblen F (oLimit f) 0 = oLimit (λn. oVeblen F (f n) 0)"
by (rule continuousD[OF continuous_oVeblen_0])

lemma (in normal) normal_oVeblen_0:
assumes "0 < F 0" shows "normal (λx. oVeblen F x 0)"
proof -
{ fix x
have "0 < oVeblen F x 0"
by (metis leD ordinal_0_le ordinal_neq_0 continuous.monoD continuous_oVeblen_0 oVeblen_0 assms)
then have "oVeblen F x 0 < oVeblen F x (oDeriv (oVeblen F x) 0)"
by (simp add: normal.strict_monoD normal_oVeblen zero_less_oFix_eq)
then have "oVeblen F x 0 < oVeblen F (oSuc x) 0"
by (metis normal_oVeblen oDeriv_fixed oVeblen_oSuc)
}
then show ?thesis
using continuous_def continuous_oVeblen_0 normalI by blast
qed

lemma (in normal) range_oVeblen:
"range (oVeblen F x) = critical_set (range F) x"
unfolding oVeblen_def
using normal_set.range_ordering normal_set_critical_set normal_set_range by blast

lemma (in normal) range_oVeblen_subset:
"x ≤ y ⟹ range (oVeblen F y) ⊆ range (oVeblen F x)"
using critical_set_mono range_oVeblen by presburger

lemma (in normal) oVeblen_fixed:
assumes "x<y"
shows "oVeblen F x (oVeblen F y a) = oVeblen F y a"
using assms
proof (induction y arbitrary: x a rule: oLimit_induct)
case zero
then show ?case
by auto
next
case (suc u)
then show ?case
by (metis antisym_conv3 leD normal_oVeblen oDeriv_fixed oSuc_le_eq_less oVeblen_oSuc)
next
case (lim f x a)
then obtain n where "x < f n"
using less_oLimitD by blast
have "oVeblen F (oLimit f) a ∈ range (oVeblen F (f n))"
then show ?case
using lim.IH ‹x < f n› by force
qed

lemma (in normal) critical_set_fixed:
assumes "0 < z"
shows "range (oVeblen F z) = {x. ∀y<z. oVeblen F y x = x}" (is "?L = ?R")
proof
show "?L ⊆ ?R"
using oVeblen_fixed by auto
have "{x. ∀y<z. oVeblen F y x = x} ⊆ range (oVeblen F z)"
using assms
proof (induction z rule: oLimit_induct)
case zero
then show ?case by auto
next
case (suc x)
then show ?case
by (force simp: normal_oVeblen oVeblen_oSuc range_oDeriv)
next
case (lim f)
show ?case
proof clarsimp
fix x
assume "∀y<oLimit f. oVeblen F y x = x"
then have "x ∈ critical_set (range F) (f n)" for n
by (metis lim.hyps rangeI range_oVeblen strict_mono_less_oLimit)
then show "x ∈ range (oVeblen F (oLimit f))"
qed
qed
then show "?R ⊆ ?L"
by blast
qed

subsection ‹Veblen hierarchy over $\lambda x.\ 1 + x$›

lemma oDeriv_id: "oDeriv id = id"
proof
fix x show "oDeriv id x = id x"
by (induction x rule: oLimit_induct) (auto simp add: oFix_eq_self)
qed

lemma oFix_plus: "oFix (λx. a + x) 0 = a * ω"
proof -
have "iter n ((+) a) 0 = a * ordinal_of_nat n" for n
proof (induction n)
case 0
then show ?case by auto
next
case (Suc n)
have "a + a * ordinal_of_nat n = a * ordinal_of_nat n + a" for n
by (induction n) (simp_all flip: ordinal_plus_assoc)
with Suc show ?case by simp
qed
then show ?thesis
qed

lemma oDeriv_plus: "oDeriv ((+) a) = ((+) (a * ω))"
proof
show "oDeriv ((+) a) x = a * ω + x" for x
proof (induction x rule: oLimit_induct)
case (suc x)
then show ?case
qed (auto simp: oFix_plus)
qed

lemma oVeblen_1_plus: "oVeblen ((+) 1) x = ((+) (ω ** x))"
using wf
proof (induction x rule: wf_induct_rule)
case (less x)
have "oVeblen ((+) (oSuc 0)) x = (+) (ω ** x)"
proof (cases x rule: ordinal_cases)
case zero
then show ?thesis
next
case (suc y)
with less show ?thesis
by (simp add: normal.oVeblen_oSuc[OF normal_plus] oDeriv_plus)
next
case (lim f)
show ?thesis
proof (rule normal_range_eq)
show "normal (oVeblen ((+) (oSuc 0)) x)"
using normal.normal_oVeblen normal_plus by blast
show "normal ((+) (ω ** x))"
using normal_plus by blast
have "∀y<oLimit f. ω ** y + u = u ⟹ u ∈ range ((+) (oLimit (λn. ω ** f n)))" for u
by (metis rangeI lim oLimit_leI ordinal_le_plusR strict_mono_less_oLimit ordinal_plus_minus2)
moreover
have "ω ** y + (oLimit (λn. ω ** f n) + u) = oLimit (λn. ω ** f n) + u"
if "y < oLimit f" for u y
by (metis absorb_omega_exp2 ordinal_exp_oLimit ordinal_plus_assoc that zero_less_omega)
ultimately show "range (oVeblen ((+) (oSuc 0)) x) = range ((+) (ω ** x))"
using less lim
by (force simp add: strict_mono_limit_ordinal normal.critical_set_fixed[OF normal_plus])
qed
qed
then show ?case
by simp
qed

end