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))"
    by (simp add: continuousD continuous_axioms)
  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"
    by (simp add: norm normal_set.closed)
  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)"
  by (simp add: ordering_def)

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

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))"
  by (simp add: normal.oLimit normal_ordering)

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
      by (simp add: ordering_0)
  next
    case (suc x)
    have "ordering (range F) (oSuc x) = (LEAST z. z ∈ range F ∧ F x < z)"
      by (simp add: ordering_oSuc suc)
    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
    by (simp add: mem_next ordering_oSuc)
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"
  by (simp add: critical_set_def)

lemma critical_set_oSuc_lemma:
  "critical_set A (oSuc n) = critical_set A n ∩ range (oDeriv (ordering (critical_set A n)))"
  by (simp add: critical_set_def ordinal_rec0_oSuc)

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"
    by (simp add: le_oFix1 oVeblen_oSuc)
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))"
    by (simp add: range_oVeblen_subset range_subsetD)
  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))"
        by (simp add: range_oVeblen critical_set_oLimit)
    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
    by (simp add: oFix_def omega_def)
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 
      by (simp add: oFix_eq_self ordinal_plus_absorb)
  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
      by (simp add: normal.oVeblen_0 normal_plus)
  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