Theory ZFC_in_HOL

section ‹The ZF Axioms, Ordinals and Transfinite Recursion›

theory ZFC_in_HOL
  imports ZFC_Library

begin

subsection‹Syntax and axioms›

hide_const (open) list.set Sum subset

unbundle lattice_syntax

typedecl V

text‹Presentation refined by Dmitriy Traytel›
axiomatization elts :: "V ⇒ V set"
 where ext [intro?]:    "elts x = elts y ⟹ x=y"
   and down_raw:        "Y ⊆ elts x ⟹ Y ∈ range elts"
   and Union_raw:       "X ∈ range elts ⟹ Union (elts ` X) ∈ range elts"
   and Pow_raw:         "X ∈ range elts ⟹ inv elts ` Pow X ∈ range elts"
   and replacement_raw: "X ∈ range elts ⟹ f ` X ∈ range elts"
   and inf_raw:         "range (g :: nat ⇒ V) ∈ range elts"
   and foundation:      "wf {(x,y). x ∈ elts y}"

lemma mem_not_refl [simp]: "i ∉ elts i"
  using wf_not_refl [OF foundation] by force

lemma mem_not_sym: "¬ (x ∈ elts y ∧ y ∈ elts x)"
  using wf_not_sym [OF foundation] by force

text ‹A set is small if it can be injected into the extension of a V-set.›
definition small :: "'a set ⇒ bool" 
  where "small X ≡ ∃V_of :: 'a ⇒ V. inj_on V_of X ∧ V_of ` X ∈ range elts"

lemma small_empty [iff]: "small {}"
  by (simp add: small_def down_raw)

lemma small_iff_range: "small X ⟷ X ∈ range elts"
  apply (simp add: small_def)
  by (metis inj_on_id2 replacement_raw the_inv_into_onto)

lemma small_eqpoll: "small A ⟷ (∃x. elts x ≈ A)"
  unfolding small_def by (metis UNIV_I bij_betw_def eqpoll_def eqpoll_sym imageE image_eqI)

text‹Small classes can be mapped to sets.›
definition set :: "V set ⇒ V"
  where "set X ≡ (if small X then inv elts X else inv elts {})"

lemma set_of_elts [simp]: "set (elts x) = x"
  by (force simp add: ext set_def f_inv_into_f small_def)

lemma elts_of_set [simp]: "elts (set X) = (if small X then X else {})"
  by (simp add: ZFC_in_HOL.set_def down_raw f_inv_into_f small_iff_range)

lemma down: "Y ⊆ elts x ⟹ small Y"
  by (simp add: down_raw small_iff_range)

lemma Union [intro]: "small X ⟹ small (Union (elts ` X))"
  by (simp add: Union_raw small_iff_range)

lemma Pow: "small X ⟹ small (set ` Pow X)"
  unfolding small_iff_range using Pow_raw set_def down by force

declare replacement_raw [intro,simp]

lemma replacement [intro,simp]:
  assumes "small X"
  shows "small (f ` X)" 
proof -
  let ?A = "inv_into X f ` (f ` X)"
  have AX: "?A ⊆ X"
    by (simp add: image_subsetI inv_into_into)
  have inj: "inj_on f ?A"
    by (simp add: f_inv_into_f inj_on_def)
  have injo: "inj_on (inv_into X f) (f ` X)"
    using inj_on_inv_into by blast
  have "∃V_of. inj_on V_of (f ` X) ∧ V_of ` f ` X ∈ range elts"
    if "inj_on V_of X" and "V_of ` X = elts x"
    for V_of :: "'a ⇒ V" and x
  proof (intro exI conjI)
    show "inj_on (V_of ∘ inv_into X f) (f ` X)"
      by (meson ‹inv_into X f ` f ` X ⊆ X› comp_inj_on inj_on_subset injo that)
    have "(λx. V_of (inv_into X f (f x))) ` X = elts (set (V_of ` ?A))"
      by (metis AX down elts_of_set image_image image_mono that(2))
    then show "(V_of ∘ inv_into X f) ` f ` X ∈ range elts"
      by (metis image_comp image_image rangeI)
  qed
  then show ?thesis
    using assms by (auto simp: small_def)
qed

lemma small_image_iff [simp]: "inj_on f A ⟹ small (f ` A) ⟷ small A"
  by (metis replacement the_inv_into_onto)

text ‹A little bootstrapping is needed to characterise @{term small} for sets of arbitrary type.›

lemma inf: "small (range (g :: nat ⇒ V))"
  by (simp add: inf_raw small_iff_range)

lemma small_image_nat_V [simp]: "small (g ` N)" for g :: "nat ⇒ V"
  by (metis (mono_tags, opaque_lifting) down elts_of_set image_iff inf rangeI subsetI)

lemma Finite_V:
  fixes X :: "V set"
  assumes "finite X" shows "small X"
  using ex_bij_betw_nat_finite [OF assms] unfolding bij_betw_def by (metis small_image_nat_V)

lemma small_insert_V:
  fixes X :: "V set"
  assumes "small X"
  shows "small (insert a X)"
proof (cases "finite X")
  case True
  then show ?thesis
    by (simp add: Finite_V)
next
  case False
  show ?thesis
    using infinite_imp_bij_betw2 [OF False]
    by (metis replacement Un_insert_right assms bij_betw_imp_surj_on sup_bot.right_neutral)
qed

lemma small_UN_V [simp,intro]:
  fixes B :: "'a ⇒ V set"
  assumes X: "small X" and B: "⋀x. x ∈ X ⟹ small (B x)"
  shows "small (⋃x∈X. B x)"
proof -
  have "(⋃ (elts ` (λx. ZFC_in_HOL.set (B x)) ` X)) = (⋃ (B ` X))"
    using B by force
  then show ?thesis
    using Union [OF replacement [OF X, of "λx. ZFC_in_HOL.set (B x)"]] by simp
qed
 
definition vinsert where "vinsert x y ≡ set (insert x (elts y))"

lemma elts_vinsert [simp]: "elts (vinsert x y) = insert x (elts y)"
  using down small_insert_V vinsert_def by auto

definition succ where "succ x ≡ vinsert x x"

lemma elts_succ [simp]: "elts (succ x) = insert x (elts x)"
  by (simp add: succ_def)

lemma finite_imp_small:
  assumes "finite X" shows "small X"
  using assms
proof induction
  case empty
  then show ?case
    by simp
next
  case (insert a X)
  then obtain V_of u where u: "inj_on V_of X" "V_of ` X = elts u"
    by (meson small_def image_iff)
  show ?case
    unfolding small_def
  proof (intro exI conjI)
    show "inj_on (V_of(a:=u)) (insert a X)"
      using u
      apply (clarsimp simp add: inj_on_def)
      by (metis image_eqI mem_not_refl)
    have "(V_of(a:=u)) ` insert a X = elts (vinsert u u)"
      using insert.hyps(2) u(2) by auto
    then show "(V_of(a:=u)) ` insert a X ∈ range elts"
      by (blast intro:  elim: )
  qed
qed

lemma small_insert:
  assumes "small X"
  shows "small (insert a X)"
proof (cases "finite X")
  case True
  then show ?thesis
    by (simp add: finite_imp_small)
next
  case False
  show ?thesis
    using infinite_imp_bij_betw2 [OF False]
    by (metis replacement Un_insert_right assms bij_betw_imp_surj_on sup_bot.right_neutral)
qed

lemma smaller_than_small:
  assumes "small A" "B ⊆ A" shows "small B"
  using assms
  by (metis down elts_of_set image_mono small_def small_iff_range subset_inj_on) 

lemma small_insert_iff [iff]: "small (insert a X) ⟷ small X"
  by (meson small_insert smaller_than_small subset_insertI)

lemma small_iff: "small X ⟷ (∃x. X = elts x)"
  by (metis down elts_of_set subset_refl)

lemma small_elts [iff]: "small (elts x)"
  by (auto simp: small_iff)

lemma small_diff [iff]: "small (elts a - X)"
  by (meson Diff_subset down)

lemma small_set [simp]: "small (list.set xs)"
  by (simp add: ZFC_in_HOL.finite_imp_small)

lemma small_upair: "small {x,y}"
  by simp

lemma small_Un_elts: "small (elts x ∪ elts y)"
  using Union [OF small_upair] by auto

lemma small_eqcong: "⟦small X; X ≈ Y⟧ ⟹ small Y"
  by (metis bij_betw_imp_surj_on eqpoll_def replacement)

lemma lepoll_small: "⟦small Y; X ≲ Y⟧ ⟹ small X"
    by (meson lepoll_iff replacement smaller_than_small)

lemma big_UNIV [simp]: "¬ small (UNIV::V set)" (is  "¬ small ?U")
  proof
    assume "small ?U"
    then have "small A" for A :: "V set"
      by (metis (full_types) UNIV_I down small_iff subsetI)
    then have "range elts = UNIV"
      by (meson small_iff surj_def)
  then show False
    by (metis Cantors_theorem Pow_UNIV)
qed

lemma inj_on_set: "inj_on set (Collect small)"
  by (metis elts_of_set inj_onI mem_Collect_eq)

lemma set_injective [simp]: "⟦small X; small Y⟧ ⟹ set X = set Y ⟷ X=Y"
  by (metis elts_of_set)


subsection‹Type classes and other basic setup›

instantiation V :: zero
begin
definition zero_V where "0 ≡ set {}"
instance ..
end

lemma elts_0 [simp]: "elts 0 = {}"
  by (simp add: zero_V_def)

lemma set_empty [simp]: "set {} = 0"
  by (simp add: zero_V_def)

instantiation V :: one
begin
definition one_V where "1 ≡ succ 0"
instance ..
end

lemma elts_1 [simp]: "elts 1 = {0}"
  by (simp add: one_V_def)

lemma insert_neq_0 [simp]: "set (insert a X) = 0 ⟷ ¬ small X"
  unfolding zero_V_def
  by (metis elts_of_set empty_not_insert set_of_elts small_insert_iff)

lemma elts_eq_empty_iff [simp]: "elts x = {} ⟷ x=0"
  by (auto simp: ZFC_in_HOL.ext)

instantiation V :: distrib_lattice
begin

definition inf_V where "inf_V x y ≡ set (elts x ∩ elts y)"

definition sup_V where "sup_V x y ≡ set (elts x ∪ elts y)"

definition less_eq_V where "less_eq_V x y ≡ elts x ⊆ elts y"

definition less_V where "less_V x y ≡ less_eq x y ∧ x ≠ (y::V)"

instance
proof
  show "(x < y) = (x ≤ y ∧ ¬ y ≤ x)" for x :: V and y :: V
    using ext less_V_def less_eq_V_def by auto
  show "x ≤ x" for x :: V
    by (simp add: less_eq_V_def)
  show "x ≤ z" if "x ≤ y" "y ≤ z" for x y z :: V
    using that by (auto simp: less_eq_V_def)
  show "x = y" if "x ≤ y" "y ≤ x" for x y :: V
    using that by (simp add: ext less_eq_V_def)
  show "inf x y ≤ x" for x y :: V
    by (metis down elts_of_set inf_V_def inf_sup_ord(1) less_eq_V_def)
  show "inf x y ≤ y" for x y :: V
    by (metis Int_lower2 down elts_of_set inf_V_def less_eq_V_def)
  show "x ≤ inf y z" if "x ≤ y" "x ≤ z" for x y z :: V
  proof -
    have "small (elts y ∩ elts z)"
      by (meson down inf.cobounded1)
    then show ?thesis
      using elts_of_set inf_V_def less_eq_V_def that by auto
  qed
  show "x ≤ x ⊔ y" "y ≤ x ⊔ y" for x y :: V
    by (simp_all add: less_eq_V_def small_Un_elts sup_V_def)
  show "sup y z ≤ x" if "y ≤ x" "z ≤ x" for x y z :: V
    using less_eq_V_def sup_V_def that by auto
  show "sup x (inf y z) = inf (x ⊔ y) (sup x z)" for x y z :: V
  proof -
    have "small (elts y ∩ elts z)"
      by (meson down inf.cobounded2)
    then show ?thesis
      by (simp add: Un_Int_distrib inf_V_def small_Un_elts sup_V_def)
  qed
qed
end

lemma V_equalityI [intro]: "(⋀x. x ∈ elts a ⟷ x ∈ elts b) ⟹ a = b"
  by (meson dual_order.antisym less_eq_V_def subsetI)

lemma vsubsetI [intro!]: "(⋀x. x ∈ elts a ⟹ x ∈ elts b) ⟹ a ≤ b"
  by (simp add: less_eq_V_def subsetI)

lemma vsubsetD [elim, intro?]: "a ≤ b ⟹ c ∈ elts a ⟹ c ∈ elts b"
  using less_eq_V_def by auto

lemma rev_vsubsetD: "c ∈ elts a ⟹ a ≤ b ⟹ c ∈ elts b"
  ― ‹The same, with reversed premises for use with @{method erule} -- cf. @{thm rev_mp}.›
  by (rule vsubsetD)

lemma vsubsetCE [elim,no_atp]: "a ≤ b ⟹ (c ∉ elts a ⟹ P) ⟹ (c ∈ elts b ⟹ P) ⟹ P"
  ― ‹Classical elimination rule.›
  using vsubsetD by blast

lemma set_image_le_iff: "small A ⟹ set (f ` A) ≤ B ⟷ (∀x∈A. f x ∈ elts B)"
  by auto

lemma eq0_iff: "x = 0 ⟷ (∀y. y ∉ elts x)"
  by auto

lemma less_eq_V_0_iff [simp]: "x ≤ 0 ⟷ x = 0" for x::V
  by auto

lemma subset_iff_less_eq_V:
  assumes "small B" shows "A ⊆ B ⟷ set A ≤ set B ∧ small A"
  using assms down small_iff by auto

lemma small_Collect [simp]: "small A ⟹ small {x ∈ A. P x}"
  by (simp add: smaller_than_small)

lemma small_Union_iff: "small (⋃(elts ` X)) ⟷ small X"
  proof
  show "small X"
    if "small (⋃ (elts ` X))"
  proof -
    have "X ⊆ set ` Pow (⋃ (elts ` X))"
      by fastforce
    then show ?thesis
      using Pow subset_iff_less_eq_V that by auto
  qed
qed auto

lemma not_less_0 [iff]:
  fixes x::V shows "¬ x < 0"
  by (simp add: less_eq_V_def less_le_not_le)

lemma le_0 [iff]:
  fixes x::V shows "0 ≤ x"
  by auto

lemma min_0L [simp]: "min 0 n = 0" for n :: V
  by (simp add: min_absorb1)

lemma min_0R [simp]: "min n 0 = 0" for n :: V
  by (simp add: min_absorb2)

lemma neq0_conv: "⋀n::V. n ≠ 0 ⟷ 0 < n"
  by (simp add: less_V_def)


definition VPow :: "V ⇒ V"
  where "VPow x ≡ set (set ` Pow (elts x))"

lemma VPow_iff [iff]: "y ∈ elts (VPow x) ⟷ y ≤ x"
  using down Pow
  apply (auto simp: VPow_def less_eq_V_def)
  using less_eq_V_def apply fastforce
  done

lemma VPow_le_VPow_iff [simp]: "VPow a ≤ VPow b ⟷ a ≤ b"
  by auto

lemma elts_VPow: "elts (VPow x) = set ` Pow (elts x)"
  by (auto simp: VPow_def Pow)

lemma small_sup_iff [simp]: "small (X ∪ Y) ⟷ small X ∧ small Y" for X::"V set"
  by (metis down elts_of_set small_Un_elts sup_ge1 sup_ge2)

lemma elts_sup_iff [simp]: "elts (x ⊔ y) = elts x ∪ elts y"
  by (simp add: sup_V_def)

lemma trad_foundation:
  assumes z: "z ≠ 0" shows "∃w. w ∈ elts z ∧ w ⊓ z = 0"
  using foundation assms
  by (simp add: wf_eq_minimal) (metis Int_emptyI equals0I inf_V_def set_of_elts zero_V_def)


instantiation "V" :: Sup
begin
definition Sup_V where "Sup_V X ≡ if small X then set (Union (elts ` X)) else 0"
instance ..
end

instantiation "V" :: Inf
begin
definition Inf_V where "Inf_V X ≡ if X = {} then 0 else set (Inter (elts ` X))"
instance ..
end

lemma V_disjoint_iff: "x ⊓ y = 0 ⟷ elts x ∩ elts y = {}"
  by (metis down elts_of_set inf_V_def inf_le1 zero_V_def)

text‹I've no idea why @{term bdd_above} is treated differently from @{term bdd_below}, but anyway›
lemma bdd_above_iff_small [simp]: "bdd_above X = small X" for X::"V set"
proof
  show "small X" if "bdd_above X"
  proof -
    obtain a where "∀x∈X. x ≤ a"
      using that ‹bdd_above X› bdd_above_def by blast
    then show "small X"
      by (meson VPow_iff ‹∀x∈X. x ≤ a› down subsetI)
  qed
  show "bdd_above X"
    if "small X"
  proof -
    have "∀x∈X. x ≤ ⨆ X"
      by (simp add: SUP_upper Sup_V_def Union less_eq_V_def that)
    then show ?thesis
      by (meson bdd_above_def)
  qed
qed


instantiation "V" :: conditionally_complete_lattice
begin

definition bdd_below_V where "bdd_below_V X ≡ X ≠ {}"

instance
  proof
  show "⨅ X ≤ x" if "x ∈ X" "bdd_below X"
    for x :: V and X :: "V set"
    using that by (auto simp: bdd_below_V_def Inf_V_def split: if_split_asm)
  show "z ≤ ⨅ X"
    if "X ≠ {}" "⋀x. x ∈ X ⟹ z ≤ x"
    for X :: "V set" and z :: V
    using that
    apply (clarsimp simp add: bdd_below_V_def Inf_V_def less_eq_V_def split: if_split_asm)
    by (meson INT_subset_iff down eq_refl equals0I)
  show "x ≤ ⨆ X" if "x ∈ X" and "bdd_above X" for x :: V and X :: "V set"
    using that Sup_V_def by auto
  show "⨆ X ≤ (z::V)" if "X ≠ {}" "⋀x. x ∈ X ⟹ x ≤ z" for X :: "V set" and z :: V
    using that  by (simp add: SUP_least Sup_V_def less_eq_V_def)
qed
end

lemma Sup_upper: "⟦x ∈ A; small A⟧ ⟹ x ≤ ⨆A" for A::"V set"
  by (auto simp: Sup_V_def SUP_upper Union less_eq_V_def)

lemma Sup_least:
  fixes z::V shows "(⋀x. x ∈ A ⟹ x ≤ z) ⟹ ⨆A ≤ z"
  by (auto simp: Sup_V_def SUP_least less_eq_V_def)

lemma Sup_empty [simp]: "⨆{} = (0::V)"
  using Sup_V_def by auto

lemma elts_Sup [simp]: "small X ⟹ elts (⨆ X) = ⋃(elts ` X)"
  by (auto simp: Sup_V_def)

lemma sup_V_0_left [simp]: "0 ⊔ a = a" and sup_V_0_right [simp]: "a ⊔ 0 = a" for a::V
  by auto

lemma Sup_V_insert:
  fixes x::V assumes "small A" shows "⨆(insert x A) = x ⊔ ⨆A"
  by (simp add: assms cSup_insert_If)

lemma Sup_Un_distrib: "⟦small A; small B⟧ ⟹ ⨆(A ∪ B) = ⨆A ⊔ ⨆B" for A::"V set"
  by auto

lemma SUP_sup_distrib:
  fixes f :: "V ⇒ V"
  shows "small A ⟹ (⨆x∈A. f x ⊔ g x) = ⨆ (f ` A) ⊔ ⨆ (g ` A)"
  by (force simp:)

lemma SUP_const [simp]: "(⨆y ∈ A. a) = (if A = {} then (0::V) else a)"
  by simp

lemma cSUP_subset_mono:
  fixes f :: "'a ⇒ V set" and g :: "'a ⇒ V set"
  shows "⟦A ⊆ B; ⋀x. x ∈ A ⟹ f x ≤ g x⟧ ⟹ ⨆ (f ` A) ≤ ⨆ (g ` B)"
  by (simp add: SUP_subset_mono)

lemma mem_Sup_iff [iff]: "x ∈ elts (⨆X) ⟷ x ∈ ⋃ (elts ` X) ∧ small X"
  using Sup_V_def by auto

lemma cSUP_UNION:
  fixes B :: "V ⇒ V set" and f :: "V ⇒ V"
  assumes ne: "small A" and bdd_UN: "small (⋃x∈A. f ` B x)"
  shows "⨆(f ` (⋃x∈A. B x)) = ⨆((λx. ⨆(f ` B x)) ` A)"
proof -
  have bdd: "⋀x. x ∈ A ⟹ small (f ` B x)"
    using bdd_UN subset_iff_less_eq_V
    by (meson SUP_upper smaller_than_small)
  then have bdd2: "small ((λx. ⨆(f ` B x)) ` A)"
    using ne(1) by blast
  have "⨆(f ` (⋃x∈A. B x)) ≤ ⨆((λx. ⨆(f ` B x)) ` A)"
    using assms by (fastforce simp add: intro!: cSUP_least intro: cSUP_upper2 simp: bdd2 bdd)
  moreover have "⨆((λx. ⨆(f ` B x)) ` A) ≤ ⨆(f ` (⋃x∈A. B x))"
    using assms by (fastforce simp add: intro!: cSUP_least intro: cSUP_upper simp: image_UN bdd_UN)
  ultimately show ?thesis
    by (rule order_antisym)
qed

lemma Sup_subset_mono: "small B ⟹ A ⊆ B ⟹ Sup A ≤ Sup B" for A::"V set"
  by auto

lemma Sup_le_iff: "small A ⟹ Sup A ≤ a ⟷ (∀x∈A. x ≤ a)" for A::"V set"
  by auto

lemma SUP_le_iff: "small (f ` A) ⟹ ⨆(f ` A) ≤ u ⟷ (∀x∈A. f x ≤ u)" for f :: "V ⇒ V"
  by blast

lemma Sup_eq_0_iff [simp]: "⨆A = 0 ⟷ A ⊆ {0} ∨ ¬ small A" for A :: "V set"
  using Sup_upper by fastforce

lemma Sup_Union_commute:
  fixes f :: "V ⇒ V set"
  assumes "small A" "⋀x. x∈A ⟹ small (f x)"
  shows "⨆ (⋃x∈A. f x) = (⨆x∈A. ⨆ (f x))"
  using assms 
  by (force simp: subset_iff_less_eq_V intro!: antisym)

lemma Sup_eq_Sup:
  fixes B :: "V set"
  assumes "B ⊆ A" "small A" and *: "⋀x. x ∈ A ⟹ ∃y ∈ B. x ≤ y"
  shows "Sup A = Sup B"
proof -
  have "small B"
    using assms subset_iff_less_eq_V by auto
  moreover have "∃y∈B. u ∈ elts y"
    if "x ∈ A" "u ∈ elts x" for u x
    using that "*" by blast
  moreover have "∃x∈A. v ∈ elts x"
    if "y ∈ B" "v ∈ elts y" for v y
    using that ‹B ⊆ A› by blast
  ultimately show ?thesis
    using assms by auto
qed

subsection‹Successor function›

lemma vinsert_not_empty [simp]: "vinsert a A ≠ 0"
  and empty_not_vinsert [simp]: "0 ≠ vinsert a A"
  by (auto simp: vinsert_def)

lemma succ_not_0 [simp]: "succ n ≠ 0" and zero_not_succ [simp]: "0 ≠ succ n"
  by (auto simp: succ_def)

instantiation V :: zero_neq_one
begin
instance 
  by intro_classes (metis elts_0 elts_succ empty_iff insert_iff one_V_def set_of_elts)
end

instantiation V :: zero_less_one
begin
instance 
  by intro_classes (simp add: less_V_def)
end

lemma succ_ne_self [simp]: "i ≠ succ i"
  by (metis elts_succ insertI1 mem_not_refl)

lemma succ_notin_self: "succ i ∉ elts i"
  using elts_succ mem_not_refl by blast

lemma le_succE: "succ i ≤ succ j ⟹ i ≤ j"
  using less_eq_V_def mem_not_sym by auto

lemma succ_inject_iff [iff]: "succ i = succ j ⟷ i = j"
  by (simp add: dual_order.antisym le_succE)

lemma inj_succ: "inj succ"
  by (simp add: inj_def)

lemma succ_neq_zero: "succ x ≠ 0"
  by (metis elts_0 elts_succ insert_not_empty)

definition pred where "pred i ≡ THE j. i = succ j"

lemma pred_succ [simp]: "pred (succ i) = i"
  by (simp add: pred_def)


subsection ‹Ordinals›

definition Transset where "Transset x ≡ ∀y ∈ elts x. y ≤ x"

definition Ord where "Ord x ≡ Transset x ∧ (∀y ∈ elts x. Transset y)"

abbreviation ON where "ON ≡ Collect Ord"

subsubsection ‹Transitive sets›

lemma Transset_0 [iff]: "Transset 0"
  by (auto simp: Transset_def)

lemma Transset_succ [intro]:
  assumes "Transset x" shows "Transset (succ x)"
  using assms
  by (auto simp: Transset_def succ_def less_eq_V_def)

lemma Transset_Sup:
  assumes "⋀x. x ∈ X ⟹ Transset x" shows "Transset (⨆X)"
proof (cases "small X")
  case True
  with assms show ?thesis
    by (simp add: Transset_def) (meson Sup_upper assms dual_order.trans)
qed (simp add: Sup_V_def)

lemma Transset_sup:
  assumes "Transset x" "Transset y" shows "Transset (x ⊔ y)"
  using Transset_def assms by fastforce

lemma Transset_inf: "⟦Transset i; Transset j⟧ ⟹ Transset (i ⊓ j)"
  by (simp add: Transset_def rev_vsubsetD)

lemma Transset_VPow: "Transset(i) ⟹ Transset(VPow(i))"
  by (auto simp: Transset_def)

lemma Transset_Inf: "(⋀i. i ∈ A ⟹ Transset i) ⟹ Transset (⨅ A)"
  by (force simp: Transset_def Inf_V_def)

lemma Transset_SUP: "(⋀x. x ∈ A ⟹ Transset (B x)) ⟹ Transset (⨆ (B ` A))"
  by (metis Transset_Sup imageE)

lemma Transset_INT: "(⋀x. x ∈ A ⟹ Transset (B x)) ⟹ Transset (⨅ (B ` A))"
  by (metis Transset_Inf imageE)


subsubsection ‹Zero, successor, sups›

lemma Ord_0 [iff]: "Ord 0"
  by (auto simp: Ord_def)

lemma Ord_succ [intro]:
  assumes "Ord x" shows "Ord (succ x)"
  using assms by (auto simp: Ord_def)

lemma Ord_Sup:
  assumes "⋀x. x ∈ X ⟹ Ord x" shows "Ord (⨆X)"
proof (cases "small X")
  case True
  with assms show ?thesis
    by (auto simp: Ord_def Transset_Sup)
qed (simp add: Sup_V_def)

lemma Ord_Union:
  assumes "⋀x. x ∈ X ⟹ Ord x" "small X" shows "Ord (set (⋃ (elts ` X)))"
  by (metis Ord_Sup Sup_V_def assms)

lemma Ord_sup:
  assumes "Ord x" "Ord y" shows "Ord (x ⊔ y)"
  using assms
  proof (clarsimp simp: Ord_def)
  show "Transset (x ⊔ y) ∧ (∀y∈elts x ∪ elts y. Transset y)"
    if "Transset x" "Transset y" "∀y∈elts x. Transset y" "∀y∈elts y. Transset y"
    using Ord_def Transset_sup assms by auto
qed

lemma big_ON [simp]: "¬ small ON"
proof
  assume "small ON"
  then have "set ON ∈ ON"
    by (metis Ord_Union Ord_succ Sup_upper elts_Sup elts_succ insertI1 mem_Collect_eq mem_not_refl set_of_elts vsubsetD)
  then show False
    by (metis ‹small ON› elts_of_set mem_not_refl)
qed

lemma Ord_1 [iff]: "Ord 1"
  using Ord_succ one_V_def succ_def vinsert_def by fastforce

lemma OrdmemD: "Ord k ⟹ j ∈ elts k ⟹ j < k"
  using Ord_def Transset_def less_V_def by auto

lemma Ord_trans: "⟦ i ∈ elts j;  j ∈ elts k;  Ord k ⟧  ⟹ i ∈ elts k"
  using Ord_def Transset_def by blast

lemma mem_0_Ord:
  assumes k: "Ord k" and knz: "k ≠ 0" shows "0 ∈ elts k"
  by (metis Ord_def Transset_def inf.orderE k knz trad_foundation)

lemma Ord_in_Ord: "⟦ Ord k;  m ∈ elts k ⟧  ⟹ Ord m"
  using Ord_def Ord_trans by blast

lemma OrdI: "⟦Transset i; ⋀x. x ∈ elts i ⟹ Transset x⟧ ⟹ Ord i"
  by (simp add: Ord_def)

lemma Ord_is_Transset: "Ord i ⟹ Transset i"
  by (simp add: Ord_def)

lemma Ord_contains_Transset: "⟦Ord i; j ∈ elts i⟧ ⟹ Transset j"
  using Ord_def by blast

lemma ON_imp_Ord:
  assumes "H ⊆ ON" "x ∈ H"
  shows "Ord x"
  using assms by blast

lemma elts_subset_ON: "Ord α ⟹ elts α ⊆ ON"
  using Ord_in_Ord by blast

lemma Transset_pred [simp]: "Transset x ⟹ ⨆(elts (succ x)) = x"
  by (fastforce simp: Transset_def)

lemma Ord_pred [simp]: "Ord β ⟹ ⨆ (insert β (elts β)) = β"
  using Ord_def Transset_pred by auto


subsubsection ‹Induction, Linearity, etc.›

lemma Ord_induct [consumes 1, case_names step]:
  assumes k: "Ord k"
      and step: "⋀x.⟦ Ord x; ⋀y. y ∈ elts x ⟹ P y ⟧  ⟹ P x"
    shows "P k"
  using foundation k
proof (induction k rule: wf_induct_rule)
  case (less x)
  then show ?case
    using Ord_in_Ord local.step by auto
qed

text ‹Comparability of ordinals›
lemma Ord_linear: "Ord k ⟹ Ord l ⟹ k ∈ elts l ∨ k=l ∨ l ∈ elts k"
proof (induct k arbitrary: l rule: Ord_induct)
  case (step k)
  note step_k = step
  show ?case using ‹Ord l›
    proof (induct l rule: Ord_induct)
      case (step l)
      thus ?case using step_k
        by (metis Ord_trans V_equalityI)
    qed
qed

text ‹The trichotomy law for ordinals›
lemma Ord_linear_lt:
  assumes "Ord k" "Ord l"
  obtains (lt) "k < l" | (eq) "k=l" | (gt) "l < k"
  using Ord_linear OrdmemD assms by blast

lemma Ord_linear2:
  assumes "Ord k" "Ord l"
  obtains (lt) "k < l" | (ge) "l ≤ k"
  by (metis Ord_linear_lt eq_refl assms order.strict_implies_order)

lemma Ord_linear_le:
  assumes "Ord k" "Ord l"
  obtains (le) "k ≤ l" | (ge) "l ≤ k"
  by (meson Ord_linear2 le_less assms)

lemma union_less_iff [simp]: "⟦Ord i; Ord j⟧ ⟹ i ⊔ j < k ⟷ i<k ∧ j<k"
  by (metis Ord_linear_le le_iff_sup sup.order_iff sup.strict_boundedE)

lemma Ord_mem_iff_lt: "Ord k ⟹ Ord l ⟹ k ∈ elts l ⟷ k < l"
  by (metis Ord_linear OrdmemD less_le_not_le)

lemma Ord_Collect_lt: "Ord α ⟹ {ξ. Ord ξ ∧ ξ < α} = elts α"
  by (auto simp flip: Ord_mem_iff_lt elim: Ord_in_Ord OrdmemD)

lemma Ord_not_less: "⟦Ord x; Ord y⟧ ⟹ ¬ x < y ⟷ y ≤ x"
  by (metis (no_types) Ord_linear2 leD)

lemma Ord_not_le: "⟦Ord x; Ord y⟧ ⟹ ¬ x ≤ y ⟷ y < x"
  by (metis (no_types) Ord_linear2 leD)

lemma le_succ_iff: "Ord i ⟹ Ord j ⟹ succ i ≤ succ j ⟷ i ≤ j"
  by (metis Ord_linear_le Ord_succ le_succE order_antisym)

lemma succ_le_iff: "Ord i ⟹ Ord j ⟹ succ i ≤ j ⟷ i < j"
  using Ord_mem_iff_lt dual_order.strict_implies_order less_eq_V_def by fastforce

lemma succ_in_Sup_Ord:
  assumes eq: "succ β = ⨆A" and "small A" "A ⊆ ON" "Ord β"
  shows "succ β ∈ A"
proof -
  have "¬ ⨆A ≤ β"
    using eq ‹Ord β› succ_le_iff by fastforce
  then show ?thesis
    using assms by (metis Ord_linear2 Sup_least Sup_upper eq_iff mem_Collect_eq subsetD succ_le_iff)
qed

lemma in_succ_iff: "Ord i ⟹ j ∈ elts (ZFC_in_HOL.succ i) ⟷ Ord j ∧ j ≤ i"
  by (metis Ord_in_Ord Ord_mem_iff_lt Ord_not_le Ord_succ succ_le_iff)

lemma zero_in_succ [simp,intro]: "Ord i ⟹ 0 ∈ elts (succ i)"
  using mem_0_Ord by auto

lemma less_succ_self: "x < succ x"
  by (simp add: less_eq_V_def order_neq_le_trans subset_insertI)

lemma Ord_finite_Sup: "⟦finite A; A ⊆ ON; A ≠ {}⟧ ⟹ ⨆A ∈ A"
proof (induction A rule: finite_induct)
  case (insert x A)
  then have *: "small A" "A ⊆ ON" "Ord x"
    by (auto simp add: ZFC_in_HOL.finite_imp_small insert.hyps)
  show ?case
  proof (cases "A = {}")
    case False
    then have "⨆A ∈ A"
      using insert by blast
    then have "⨆A ≤ x" if "x ⊔ ⨆A ∉ A"
      using * by (metis ON_imp_Ord Ord_linear_le sup.absorb2 that)
    then show ?thesis
      by (fastforce simp: ‹small A› Sup_V_insert)
  qed auto
qed auto


subsubsection ‹The natural numbers›

primrec ord_of_nat :: "nat ⇒ V" where
  "ord_of_nat 0 = 0"
| "ord_of_nat (Suc n) = succ (ord_of_nat n)"

lemma ord_of_nat_eq_initial: "ord_of_nat n = set (ord_of_nat ` {..<n})"
  by (induction n) (auto simp: lessThan_Suc succ_def)

lemma mem_ord_of_nat_iff [simp]: "x ∈ elts (ord_of_nat n) ⟷ (∃m<n. x = ord_of_nat m)"
  by (subst ord_of_nat_eq_initial) auto

lemma elts_ord_of_nat: "elts (ord_of_nat k) = ord_of_nat ` {..<k}"
  by auto

lemma Ord_equality: "Ord i ⟹ i = ⨆ (succ ` elts i)"
  by (force intro: Ord_trans)

lemma Ord_ord_of_nat [simp]: "Ord (ord_of_nat k)"
  by (induct k, auto)

lemma ord_of_nat_equality: "ord_of_nat n = ⨆ ((succ ∘ ord_of_nat) ` {..<n})"
  by (metis Ord_equality Ord_ord_of_nat elts_of_set image_comp small_image_nat_V ord_of_nat_eq_initial)

definition ω :: V where "ω ≡ set (range ord_of_nat)"

lemma elts_ω: "elts ω = {α. ∃n. α = ord_of_nat n}"
  by (auto simp: ω_def image_iff)

lemma nat_into_Ord [simp]: "n ∈ elts ω ⟹ Ord n"
  by (metis Ord_ord_of_nat ω_def elts_of_set image_iff inf)

lemma Sup_ω: "⨆(elts ω) = ω"
  unfolding ω_def by force

lemma Ord_ω [iff]: "Ord ω"
  by (metis Ord_Sup Sup_ω nat_into_Ord)

lemma zero_in_omega [iff]: "0 ∈ elts ω"
  by (metis ω_def elts_of_set inf ord_of_nat.simps(1) rangeI)

lemma succ_in_omega [simp]: "n ∈ elts ω ⟹ succ n ∈ elts ω"
  by (metis ω_def elts_of_set image_iff small_image_nat_V ord_of_nat.simps(2) rangeI)

lemma ord_of_eq_0: "ord_of_nat j = 0 ⟹ j = 0"
  by (induct j) (auto simp: succ_neq_zero)

lemma ord_of_nat_le_omega: "ord_of_nat n ≤ ω"
  by (metis Sup_ω ZFC_in_HOL.Sup_upper ω_def elts_of_set inf rangeI)

lemma ord_of_eq_0_iff [simp]: "ord_of_nat n = 0 ⟷ n=0"
  by (auto simp: ord_of_eq_0)

lemma ord_of_nat_inject [iff]: "ord_of_nat i = ord_of_nat j ⟷ i=j"
proof (induct i arbitrary: j)
  case 0 show ?case
    using ord_of_eq_0 by auto
next
  case (Suc i) then show ?case
    by auto (metis elts_0 elts_succ insert_not_empty not0_implies_Suc ord_of_nat.simps succ_inject_iff)
qed

corollary inj_ord_of_nat: "inj ord_of_nat"
  by (simp add: linorder_injI)

corollary countable:
  assumes "countable X" shows "small X"
proof -
  have "X ⊆ range (from_nat_into X)"
    by (simp add: assms subset_range_from_nat_into)
  then show ?thesis
    by (meson inf_raw inj_ord_of_nat replacement small_def smaller_than_small)
qed

corollary infinite_ω: "infinite (elts ω)"
  using range_inj_infinite [of ord_of_nat]
  by (simp add: ω_def inj_ord_of_nat)

corollary ord_of_nat_mono_iff [iff]: "ord_of_nat i ≤ ord_of_nat j ⟷ i ≤ j"
  by (metis Ord_def Ord_ord_of_nat Transset_def eq_iff mem_ord_of_nat_iff not_less ord_of_nat_inject)

corollary ord_of_nat_strict_mono_iff [iff]: "ord_of_nat i < ord_of_nat j ⟷ i < j"
  by (simp add: less_le_not_le)

lemma small_image_nat [simp]:
  fixes N :: "nat set" shows "small (g ` N)"
  by (simp add: countable)

lemma finite_Ord_omega: "α ∈ elts ω ⟹ finite (elts α)"
  proof (clarsimp simp add: ω_def)
  show "finite (elts (ord_of_nat n))" if "α = ord_of_nat n" for n
    using that by (simp add: ord_of_nat_eq_initial [of n])
qed

lemma infinite_Ord_omega: "Ord α ⟹ infinite (elts α) ⟹ ω ≤ α"
  by (meson Ord_ω Ord_linear2 Ord_mem_iff_lt finite_Ord_omega)

lemma ord_of_minus_1: "n > 0 ⟹ ord_of_nat n = succ (ord_of_nat (n - 1))"
  by (metis Suc_diff_1 ord_of_nat.simps(2))

lemma card_ord_of_nat [simp]: "card (elts (ord_of_nat m)) = m"
  by (induction m) (auto simp: ω_def finite_Ord_omega)

lemma ord_of_nat_ω [iff]:"ord_of_nat n ∈ elts ω"
  by (simp add: ω_def)

lemma succ_ω_iff [iff]: "succ n ∈ elts ω ⟷ n ∈ elts ω"
  by (metis Ord_ω OrdmemD elts_vinsert insert_iff less_V_def succ_def succ_in_omega vsubsetD)

lemma ω_gt0 [simp]: "ω > 0"
  by (simp add: OrdmemD)

lemma ω_gt1 [simp]: "ω > 1"
  by (simp add: OrdmemD one_V_def)

subsubsection‹Limit ordinals›

definition Limit :: "V⇒bool"
  where "Limit i ≡ Ord i ∧ 0 ∈ elts i ∧ (∀y. y ∈ elts i ⟶ succ y ∈ elts i)"

lemma zero_not_Limit [iff]: "¬ Limit 0"
  by (simp add: Limit_def)

lemma not_succ_Limit [simp]: "¬ Limit(succ i)"
  by (metis Limit_def Ord_mem_iff_lt elts_succ insertI1 less_irrefl)

lemma Limit_is_Ord: "Limit ξ ⟹ Ord ξ"
  by (simp add: Limit_def)

lemma succ_in_Limit_iff: "Limit ξ ⟹ succ α ∈ elts ξ ⟷ α ∈ elts ξ"
  by (metis Limit_def OrdmemD elts_succ insertI1 less_V_def vsubsetD)

lemma Limit_eq_Sup_self [simp]: "Limit i ⟹ Sup (elts i) = i"
  apply (rule order_antisym)
  apply (simp add: Limit_def Ord_def Transset_def Sup_least)
  by (metis Limit_def Ord_equality Sup_V_def SUP_le_iff Sup_upper small_elts)

lemma zero_less_Limit: "Limit β ⟹ 0 < β"
  by (simp add: Limit_def OrdmemD)

lemma non_Limit_ord_of_nat [iff]: "¬ Limit (ord_of_nat m)"
  by (metis Limit_def mem_ord_of_nat_iff not_succ_Limit ord_of_eq_0_iff ord_of_minus_1)

lemma Limit_omega [iff]: "Limit ω"
  by (simp add: Limit_def)

lemma omega_nonzero [simp]: "ω ≠ 0"
  using Limit_omega by fastforce

lemma Ord_cases_lemma:
  assumes "Ord k" shows "k = 0 ∨ (∃j. k = succ j) ∨ Limit k"
proof (cases "Limit k")
  case False
  have "succ j ∈ elts k" if  "∀j. k ≠ succ j" "j ∈ elts k" for j
    by (metis Ord_in_Ord Ord_linear Ord_succ assms elts_succ insertE mem_not_sym that)
  with assms show ?thesis
    by (auto simp: Limit_def mem_0_Ord)
qed auto

lemma Ord_cases [cases type: V, case_names 0 succ limit]:
  assumes "Ord k"
  obtains "k = 0" | l where "Ord l" "succ l = k" | "Limit k"
  by (metis assms Ord_cases_lemma Ord_in_Ord elts_succ insertI1)

lemma non_succ_LimitI:
  assumes "i≠0" "Ord(i)" "⋀y. succ(y) ≠ i"
  shows "Limit(i)"
  using Ord_cases_lemma assms by blast

lemma Ord_induct3 [consumes 1, case_names 0 succ Limit, induct type: V]:
  assumes α: "Ord α"
    and P: "P 0" "⋀α. ⟦Ord α; P α⟧ ⟹ P (succ α)"
           "⋀α. ⟦Limit α; ⋀ξ. ξ ∈ elts α ⟹ P ξ⟧ ⟹ P (⨆ξ ∈ elts α. ξ)"
  shows "P α"
  using α
proof (induction α rule: Ord_induct)
  case (step α)
  then show ?case
    by (metis Limit_eq_Sup_self Ord_cases P elts_succ image_ident insertI1)
qed


subsubsection‹Properties of LEAST for ordinals›

lemma
  assumes "Ord k" "P k"
  shows Ord_LeastI: "P (LEAST i. Ord i ∧ P i)" and Ord_Least_le: "(LEAST i. Ord i ∧ P i) ≤ k"
proof -
  have "P (LEAST i. Ord i ∧ P i) ∧ (LEAST i. Ord i ∧ P i) ≤ k"
    using assms
  proof (induct k rule: Ord_induct)
    case (step x) then have "P x" by simp
    show ?case proof (rule classical)
      assume assm: "¬ (P (LEAST a. Ord a ∧ P a) ∧ (LEAST a. Ord a ∧ P a) ≤ x)"
      have "⋀y. Ord y ∧ P y ⟹ x ≤ y"
      proof (rule classical)
        fix y
        assume y: "Ord y ∧ P y" "¬ x ≤ y"
        with step obtain "P (LEAST a. Ord a ∧ P a)" and le: "(LEAST a. Ord a ∧ P a) ≤ y"
          by (meson Ord_linear2 Ord_mem_iff_lt)
        with assm have "x < (LEAST a. Ord a ∧ P a)"
          by (meson Ord_linear_le y order.trans ‹Ord x›)
        then show "x ≤ y"
          using le by auto
      qed
      then have Least: "(LEAST a. Ord a ∧ P a) = x"
        by (simp add: Least_equality ‹Ord x› step.prems)
      with ‹P x› show ?thesis by simp
    qed
  qed
  then show "P (LEAST i. Ord i ∧ P i)" and "(LEAST i. Ord i ∧ P i) ≤ k" by auto
qed

lemma Ord_Least:
  assumes "Ord k" "P k"
  shows "Ord (LEAST i. Ord i ∧ P i)"
proof -
  have "Ord (LEAST i. Ord i ∧ (Ord i ∧ P i))"
    using Ord_LeastI [where P = "λi. Ord i ∧ P i"] assms by blast
  then show ?thesis
    by simp
qed

― ‹The following 3 lemmas are due to Brian Huffman›
lemma Ord_LeastI_ex: "∃i. Ord i ∧ P i ⟹ P (LEAST i. Ord i ∧ P i)"
  using Ord_LeastI by blast

lemma Ord_LeastI2:
  "⟦Ord a; P a; ⋀x. ⟦Ord x; P x⟧ ⟹ Q x⟧ ⟹ Q (LEAST i. Ord i ∧ P i)"
  by (blast intro: Ord_LeastI Ord_Least)

lemma Ord_LeastI2_ex:
  "∃a. Ord a ∧ P a ⟹ (⋀x. ⟦Ord x; P x⟧ ⟹ Q x) ⟹ Q (LEAST i. Ord i ∧ P i)"
  by (blast intro: Ord_LeastI_ex Ord_Least)

lemma Ord_LeastI2_wellorder:
  assumes "Ord a" "P a"
  and "⋀a. ⟦ P a; ∀b. Ord b ∧ P b ⟶ a ≤ b ⟧ ⟹ Q a"
  shows "Q (LEAST i. Ord i ∧ P i)"
proof (rule LeastI2_order)
  show "Ord (LEAST i. Ord i ∧ P i) ∧ P (LEAST i. Ord i ∧ P i)"
    using Ord_Least Ord_LeastI assms by auto
next
  fix y assume "Ord y ∧ P y" thus "(LEAST i. Ord i ∧ P i) ≤ y"
    by (simp add: Ord_Least_le)
next
  fix x assume "Ord x ∧ P x" "∀y. Ord y ∧ P y ⟶ x ≤ y" thus "Q x"
    by (simp add: assms(3))
qed

lemma Ord_LeastI2_wellorder_ex:
  assumes "∃x. Ord x ∧ P x"
  and "⋀a. ⟦ P a; ∀b. Ord b ∧ P b ⟶ a ≤ b ⟧ ⟹ Q a"
  shows "Q (LEAST i. Ord i ∧ P i)"
using assms by clarify (blast intro!: Ord_LeastI2_wellorder)

lemma not_less_Ord_Least: "⟦k < (LEAST x. Ord x ∧ P x); Ord k⟧ ⟹ ¬ P k"
  using Ord_Least_le less_le_not_le by auto

lemma exists_Ord_Least_iff: "(∃α. Ord α ∧ P α) ⟷ (∃α. Ord α ∧ P α ∧ (∀β < α. Ord β ⟶ ¬ P β))" (is "?lhs ⟷ ?rhs")
proof
  assume ?rhs thus ?lhs by blast
next
  assume H: ?lhs then obtain α where α: "Ord α" "P α" by blast
  let ?x = "LEAST α. Ord α ∧ P α"
  have "Ord ?x"
    by (metis Ord_Least α)
  moreover
  { fix β assume m: "β < ?x" "Ord β"
    from not_less_Ord_Least[OF m] have "¬ P β" . }
  ultimately show ?rhs
    using Ord_LeastI_ex[OF H] by blast
qed

lemma Ord_mono_imp_increasing:
  assumes fun_hD: "h ∈ D → D"
    and mono_h: "strict_mono_on D h" 
    and "D ⊆ ON" and ν: "ν ∈ D"
  shows "ν ≤ h ν"
proof (rule ccontr)
  assume non: "¬ ν ≤ h ν"
  define μ where "μ ≡ LEAST μ. Ord μ ∧ ¬ μ ≤ h μ ∧ μ ∈ D"
  have "Ord ν"
    using ν ‹D ⊆ ON› by blast
  then have μ: "¬ μ ≤ h μ ∧ μ ∈ D"
    unfolding μ_def by (rule Ord_LeastI) (simp add: ν non)
  have "Ord (h ν)"
    using assms by auto
  then have "Ord (h (h ν))"
    by (meson ON_imp_Ord ν assms funcset_mem)
  have "Ord μ"
    using μ ‹D ⊆ ON› by blast
  then have "h μ < μ"
    by (metis ON_imp_Ord Ord_linear2 PiE μ ‹D ⊆ ON› fun_hD)
  then have "¬ h μ ≤ h (h μ)"
    using μ fun_hD mono_h by (force simp: strict_mono_on_def)
  moreover have *: "h μ ∈ D"
    using μ fun_hD by auto
  moreover have "Ord (h μ)"
    using ‹D ⊆ ON› * by blast
  ultimately have "μ ≤ h μ"
    by (simp add: μ_def Ord_Least_le)
  then show False
    using μ by blast
qed

lemma le_Sup_iff:
  assumes "A ⊆ ON" "Ord x" "small A" shows "x ≤ ⨆A ⟷ (∀y ∈ ON. y<x ⟶ (∃a∈A. y < a))"
proof (intro iffI ballI impI)
  show "∃a∈A. y < a"
    if "x ≤ ⨆ A" "y ∈ ON" "y < x"
    for y
  proof -
    have "¬ ⨆ A ≤ y" "Ord y"
      using that by auto
    then show ?thesis
      by (metis Ord_linear2 Sup_least ‹A ⊆ ON› mem_Collect_eq subset_eq)
  qed
  show "x ≤ ⨆ A"
    if "∀y∈ON. y < x ⟶ (∃a∈A. y < a)"
    using that assms
    by (metis Ord_Sup Ord_linear_le Sup_upper less_le_not_le mem_Collect_eq subsetD)
qed

lemma le_SUP_iff: "⟦f ` A ⊆ ON; Ord x; small A⟧ ⟹ x ≤ ⨆(f ` A) ⟷ (∀y ∈ ON. y<x ⟶ (∃i∈A. y < f i))"
  by (simp add: le_Sup_iff)

subsection‹Transfinite Recursion and the V-levels›

definition transrec :: "((V ⇒ 'a) ⇒ V ⇒ 'a) ⇒ V ⇒ 'a"
  where "transrec H a ≡ wfrec {(x,y). x ∈ elts y} H a"

lemma transrec: "transrec H a = H (λx ∈ elts a. transrec H x) a"
proof -
  have "(cut (wfrec {(x, y). x ∈ elts y} H) {(x, y). x ∈ elts y} a)
      = (λx∈elts a. wfrec {(x, y). x ∈ elts y} H x)"
    by (force simp: cut_def)
  then show ?thesis
    unfolding transrec_def
    by (simp add: foundation wfrec)
qed

text‹Avoids explosions in proofs; resolve it with a meta-level definition›
lemma def_transrec:
    "⟦⋀x. f x ≡ transrec H x⟧ ⟹ f a = H(λx ∈ elts a. f x) a"
  by (metis restrict_ext transrec)

lemma eps_induct [case_names step]:
  assumes "⋀x. (⋀y. y ∈ elts x ⟹ P y) ⟹ P x"
  shows "P a"
  using wf_induct [OF foundation] assms by auto


definition Vfrom :: "[V,V] ⇒ V"
  where "Vfrom a ≡ transrec (λf x. a ⊔ ⨆((λy. VPow(f y)) ` elts x))"

abbreviation Vset :: "V ⇒ V" where "Vset ≡ Vfrom 0"

lemma Vfrom: "Vfrom a i = a ⊔ ⨆((λj. VPow(Vfrom a j)) ` elts i)"
  apply (subst Vfrom_def)
  apply (subst transrec)
  using Vfrom_def by auto

lemma Vfrom_0 [simp]: "Vfrom a 0 = a"
  by (subst Vfrom) auto

lemma Vset: "Vset i = ⨆((λj. VPow(Vset j)) ` elts i)"
  by (subst Vfrom) auto

lemma Vfrom_mono1:
  assumes "a ≤ b" shows "Vfrom a i ≤ Vfrom b i"
proof (induction i rule: eps_induct)
  case (step i)
  then have "a ⊔ (⨆j∈elts i. VPow (Vfrom a j)) ≤ b ⊔ (⨆j∈elts i. VPow (Vfrom b j))"
    by (intro sup_mono cSUP_subset_mono ‹a ≤ b›) auto
  then show ?case
    by (metis Vfrom)
qed

lemma Vfrom_mono2: "Vfrom a i ≤ Vfrom a (i ⊔ j)"
proof (induction arbitrary: j rule: eps_induct)
  case (step i)
  then have "a ⊔ (⨆j∈elts i. VPow (Vfrom a j))
           ≤ a ⊔ (⨆j∈elts (i ⊔ j). VPow (Vfrom a j))"
    by (intro sup_mono cSUP_subset_mono order_refl) auto
  then show ?case
    by (metis Vfrom)
qed

lemma Vfrom_mono: "⟦Ord i; a≤b; i≤j⟧ ⟹ Vfrom a i ≤ Vfrom b j"
  by (metis (no_types) Vfrom_mono1 Vfrom_mono2 dual_order.trans sup.absorb_iff2)

lemma Transset_Vfrom: "Transset(A) ⟹ Transset(Vfrom A i)"
proof (induction i rule: eps_induct)
  case (step i)
  then show ?case
    by (metis Transset_SUP Transset_VPow Transset_sup Vfrom)
qed

lemma Transset_Vset [simp]: "Transset(Vset i)"
  by (simp add: Transset_Vfrom)

lemma Vfrom_sup: "Vfrom a (i ⊔ j) = Vfrom a i ⊔ Vfrom a j"
proof (rule order_antisym)
  show "Vfrom a (i ⊔ j) ≤ Vfrom a i ⊔ Vfrom a j"
    by (simp add: Vfrom [of a "i ⊔ j"] Vfrom [of a i] Vfrom [of a j] Sup_Un_distrib image_Un sup.assoc sup.left_commute)
  show "Vfrom a i ⊔ Vfrom a j ≤ Vfrom a (i ⊔ j)"
    by (metis Vfrom_mono2 le_supI sup_commute)
qed

lemma Vfrom_succ_Ord:
  assumes "Ord i" shows "Vfrom a (succ i) = a ⊔ VPow(Vfrom a i)"
proof (cases "i = 0")
  case True
  then show ?thesis
    by (simp add: Vfrom [of _ "succ 0"])
next
  case False
  have *: "(⨆x∈elts i. VPow (Vfrom a x)) ≤ VPow (Vfrom a i)"
  proof (rule cSup_least)
    show "(λx. VPow (Vfrom a x)) ` elts i ≠ {}"
      using False by auto
    show "x ≤ VPow (Vfrom a i)" if "x ∈ (λx. VPow (Vfrom a x)) ` elts i" for x
      using that
      by clarsimp (meson Ord_in_Ord Ord_linear_le Vfrom_mono assms mem_not_refl order_refl vsubsetD)
  qed
  show ?thesis
  proof (rule Vfrom [THEN trans])
    show "a ⊔ (⨆j∈elts (succ i). VPow (Vfrom a j)) = a ⊔ VPow (Vfrom a i)"
      using assms
      by (intro sup_mono order_antisym) (auto simp: Sup_V_insert *)
  qed
qed

lemma Vset_succ: "Ord i ⟹ Vset(succ(i)) = VPow(Vset(i))"
  by (simp add: Vfrom_succ_Ord)

lemma Vfrom_Sup:
  assumes "X ≠ {}" "small X"
  shows "Vfrom a (Sup X) = (⨆y∈X. Vfrom a y)"
proof (rule order_antisym)
  have "Vfrom a (⨆ X) = a ⊔ (⨆j∈elts (⨆ X). VPow (Vfrom a j))"
    by (metis Vfrom)
  also have "… ≤ ⨆ (Vfrom a ` X)"
  proof -
    have "a ≤ ⨆ (Vfrom a ` X)"
      by (metis Vfrom all_not_in_conv assms bdd_above_iff_small cSUP_upper2 replacement sup_ge1)
    moreover have "(⨆j∈elts (⨆ X). VPow (Vfrom a j)) ≤ ⨆ (Vfrom a ` X)"
    proof -
      have "VPow (Vfrom a x) ≤ ⨆ (Vfrom a ` X)"
        if "y ∈ X" "x ∈ elts y" for x y
      proof -
        have "VPow (Vfrom a x) ≤ Vfrom a y"
          by (metis Vfrom bdd_above_iff_small cSUP_upper2 le_supI2 order_refl replacement small_elts that(2))
        also have "… ≤ ⨆ (Vfrom a ` X)"
          using assms that by (force intro: cSUP_upper)
        finally show ?thesis .
      qed
      then show ?thesis
        by (simp add: SUP_le_iff ‹small X›)
    qed
    ultimately show ?thesis
      by auto
  qed
  finally show "Vfrom a (⨆ X) ≤ ⨆ (Vfrom a ` X)" .
  have "⋀x. x ∈ X ⟹
         a ⊔ (⨆j∈elts x. VPow (Vfrom a j))
         ≤ a ⊔ (⨆j∈elts (⨆ X). VPow (Vfrom a j))"
    using cSUP_subset_mono ‹small X› by auto
  then show "⨆ (Vfrom a ` X) ≤ Vfrom a (⨆ X)"
    by (metis Vfrom assms(1) cSUP_least)
qed

lemma Limit_Vfrom_eq:
    "Limit(i) ⟹ Vfrom a i = (⨆y ∈ elts i. Vfrom a y)"
  by (metis Limit_def Limit_eq_Sup_self Vfrom_Sup ex_in_conv small_elts)

end