Theory ZFC_in_HOL.ZFC_Cardinals

section ‹Cartesian products, Disjoint Sums, Ranks, Cardinals›

theory ZFC_Cardinals
  imports ZFC_in_HOL

begin

declare [[coercion_enabled]]
declare [[coercion "ord_of_nat :: nat  V"]]

subsection ‹Ordered Pairs›

lemma singleton_eq_iff [iff]: "set {a} = set {b}  a=b"
  by simp

lemma doubleton_eq_iff: "set {a,b} = set {c,d}  (a=c  b=d)  (a=d  b=c)"
  by (simp add: Set.doubleton_eq_iff)

definition vpair :: "V  V  V"
  where "vpair a b = set {set {a},set {a,b}}"

definition vfst :: "V  V"
  where "vfst p  THE x. y. p = vpair x y"

definition vsnd :: "V  V"
  where "vsnd p  THE y. x. p = vpair x y"

definition vsplit :: "[[V, V]  'a, V]  'a::{}"  ― ‹for pattern-matching›
  where "vsplit c  λp. c (vfst p) (vsnd p)"

nonterminal Vs
syntax (ASCII)
  "_Tuple"    :: "[V, Vs]  V"              ("<(_,/ _)>")
  "_hpattern" :: "[pttrn, patterns]  pttrn"   ("<_,/ _>")
syntax
  ""          :: "V  Vs"                    ("_")
  "_Enum"     :: "[V, Vs]  Vs"             ("_,/ _")
  "_Tuple"    :: "[V, Vs]  V"              ("(_,/ _)")
  "_hpattern" :: "[pttrn, patterns]  pttrn"   ("_,/ _")
translations
  "<x, y, z>"     "<x, <y, z>>"
  "<x, y>"        "CONST vpair x y"
  "<x, y, z>"     "<x, <y, z>>"
  "λ<x,y,zs>. b"  "CONST vsplit(λx <y,zs>. b)"
  "λ<x,y>. b"     "CONST vsplit(λx y. b)"


lemma vpair_def': "vpair a b = set {set {a,a},set {a,b}}"
  by (simp add: vpair_def)

lemma vpair_iff [simp]: "vpair a b = vpair a' b'  a=a'  b=b'"
  unfolding vpair_def' doubleton_eq_iff by auto

lemmas vpair_inject = vpair_iff [THEN iffD1, THEN conjE, elim!]

lemma vfst_conv [simp]: "vfst a,b = a"
  by (simp add: vfst_def)

lemma vsnd_conv [simp]: "vsnd a,b = b"
  by (simp add: vsnd_def)

lemma vsplit [simp]: "vsplit c a,b = c a b"
  by (simp add: vsplit_def)

lemma vpair_neq_fst: "a,b  a"
  by (metis elts_of_set insertI1 mem_not_sym small_upair vpair_def')

lemma vpair_neq_snd: "a,b  b"
  by (metis elts_of_set insertI1 mem_not_sym small_upair subsetD subset_insertI vpair_def')

lemma vpair_nonzero [simp]: "x,y  0"
  by (metis elts_0 elts_of_set empty_not_insert small_upair vpair_def)

lemma zero_notin_vpair: "0  elts x,y"
  by (auto simp: vpair_def)

lemma inj_on_vpair [simp]: "inj_on (λ(x, y). x, y) A"
  by (auto simp: inj_on_def)


subsection ‹Generalized Cartesian product›

definition VSigma :: "V  (V  V)  V"
  where "VSigma A B  set(x  elts A. y  elts (B x). {x,y})"

abbreviation vtimes where "vtimes A B  VSigma A (λx. B)"

definition pairs :: "V  (V * V)set"
  where "pairs r  {(x,y). x,y  elts r} "

lemma pairs_iff_elts: "(x,y)  pairs z  x,y  elts z"
  by (simp add: pairs_def)

lemma VSigma_iff [simp]: "a,b  elts (VSigma A B)  a  elts A  b  elts (B a)"
  by (auto simp: VSigma_def UNION_singleton_eq_range)

lemma VSigmaI [intro!]: " a  elts A;  b  elts (B a)   a,b  elts (VSigma A B)"
  by simp

lemmas VSigmaD1 = VSigma_iff [THEN iffD1, THEN conjunct1]
lemmas VSigmaD2 = VSigma_iff [THEN iffD1, THEN conjunct2]

text ‹The general elimination rule›
lemma VSigmaE [elim!]:
  assumes "c  elts (VSigma A B)"
  obtains x y where "x  elts A" "y  elts (B x)" "c=x,y"
  using assms by (auto simp: VSigma_def split: if_split_asm)

lemma VSigmaE2 [elim!]:
  assumes "a,b  elts (VSigma A B)" obtains "a  elts A" and "b  elts (B a)"
  using assms  by auto

lemma VSigma_empty1 [simp]: "VSigma 0 B = 0"
  by auto

lemma times_iff [simp]: "a,b  elts (vtimes A B)  a  elts A  b  elts B"
  by simp

lemma timesI [intro!]: "a  elts A;  b  elts B   a,b  elts (vtimes A B)"
  by simp

lemma times_empty2 [simp]: "vtimes A 0 = 0"
  using elts_0 by blast

lemma times_empty_iff: "VSigma A B = 0  A=0  (x  elts A. B x = 0)"
  by (metis VSigmaE VSigmaI elts_0 empty_iff trad_foundation)

lemma elts_VSigma: "elts (VSigma A B) = (λ(x,y). vpair x y) ` Sigma (elts A) (λx. elts (B x))"
  by auto
    
lemma small_Sigma [simp]:
  assumes A: "small A" and B: "x. x  A  small (B x)"
  shows "small (Sigma A B)"
proof -
  obtain a where "elts a  A" 
    by (meson assms small_eqpoll)
  then obtain f where f: "bij_betw f (elts a) A"
    using eqpoll_def by blast
  have "y. elts y  B x" if "x  A" for x
    using B small_eqpoll that by blast
  then obtain g where g: "x. x  A  elts (g x)  B x"
    by metis 
  with f have "elts (VSigma a (g  f))  Sigma A B"
    by (simp add: elts_VSigma Sigma_eqpoll_cong bij_betwE)
  then show ?thesis
    using small_eqpoll by blast
qed

lemma small_Times [simp]:
  assumes "small A" "small B"  shows "small (A × B)"
  by (simp add: assms)

lemma small_Times_iff: "small (A × B)  small A  small B  A={}  B={}"  (is "_ = ?rhs")
proof
  assume *: "small (A × B)"
  { have "small A  small B" if "x  A" "y  B" for x y
    proof -
      have "A  fst ` (A × B)" "B  snd ` (A × B)"
        using that by auto
      with that show ?thesis
        by (metis * replacement smaller_than_small)
    qed    }
  then show ?rhs
    by (metis equals0I)
next
  assume ?rhs
  then show "small (A × B)"
    by auto
qed

subsection ‹Disjoint Sum›

definition vsum :: "V  V  V" (infixl "" 65) where
 "A  B  (VSigma (set {0}) (λx. A))  (VSigma (set {1}) (λx. B))"

definition Inl :: "VV" where
     "Inl a  0,a"

definition Inr :: "VV" where
     "Inr b  1,b"

lemmas sum_defs = vsum_def Inl_def Inr_def

lemma Inl_nonzero [simp]:"Inl x  0"
  by (metis Inl_def vpair_nonzero)

lemma Inr_nonzero [simp]:"Inr x  0"
  by (metis Inr_def vpair_nonzero)

subsubsection‹Equivalences for the injections and an elimination rule›

lemma Inl_in_sum_iff [iff]: "Inl a  elts (A  B)  a  elts A"
  by (auto simp: sum_defs)

lemma Inr_in_sum_iff [iff]: "Inr b  elts (A  B)  b  elts B"
  by (auto simp: sum_defs)

lemma sumE [elim!]:
  assumes u: "u  elts (A  B)"
  obtains x where "x  elts A" "u=Inl x" | y where "y  elts B" "u=Inr y" using u
  by (auto simp: sum_defs)

subsubsection ‹Injection and freeness equivalences, for rewriting›

lemma Inl_iff [iff]: "Inl a=Inl b  a=b"
  by (simp add: sum_defs)

lemma Inr_iff [iff]: "Inr a=Inr b  a=b"
  by (simp add: sum_defs)

lemma inj_on_Inl [simp]: "inj_on Inl A"
  by (simp add: inj_on_def)

lemma inj_on_Inr [simp]: "inj_on Inr A"
  by (simp add: inj_on_def)

lemma Inl_Inr_iff [iff]: "Inl a=Inr b  False"
  by (simp add: sum_defs)

lemma Inr_Inl_iff [iff]: "Inr b=Inl a  False"
  by (simp add: sum_defs)

lemma sum_empty [simp]: "0  0 = 0"
  by auto

lemma elts_vsum: "elts (a  b) = Inl ` (elts a)  Inr ` (elts b)"
  by auto

lemma sum_iff: "u  elts (A  B)  (x. x  elts A  u=Inl x)  (y. y  elts B  u=Inr y)"
  by blast

lemma sum_subset_iff: "AB  CD  AC  BD"
  by (auto simp: less_eq_V_def)

lemma sum_equal_iff:
  fixes A :: V shows "AB = CD  A=C  B=D"
  by (simp add: eq_iff sum_subset_iff)

definition is_sum :: "V  bool"
  where "is_sum z = (x. z = Inl x  z = Inr x)"

definition sum_case  :: "(V  'a)  (V  'a)  V  'a"
  where
  "sum_case f g a 
    THE z. (x. a = Inl x  z = f x)  (y. a = Inr y  z = g y)  (¬ is_sum a  z = undefined)"

lemma sum_case_Inl [simp]: "sum_case f g (Inl x) = f x"
  by (simp add: sum_case_def is_sum_def)

lemma sum_case_Inr [simp]: "sum_case f g (Inr y) = g y"
  by (simp add: sum_case_def is_sum_def)

lemma sum_case_non [simp]: "¬ is_sum a  sum_case f g a = undefined"
  by (simp add: sum_case_def is_sum_def)

lemma is_sum_cases: "(x. z = Inl x  z = Inr x)  ¬ is_sum z"
  by (auto simp: is_sum_def)

lemma sum_case_split:
  "P (sum_case f g a)  (x. a = Inl x  P(f x))  (y. a = Inr y  P(g y))  (¬ is_sum a  P undefined)"
  by (cases "is_sum a") (auto simp: is_sum_def)

lemma sum_case_split_asm:
  "P (sum_case f g a)  ¬ ((x. a = Inl x  ¬ P(f x))  (y. a = Inr y  ¬ P(g y))  (¬ is_sum a  ¬ P undefined))"
  by (auto simp: sum_case_split)

subsubsection ‹Applications of disjoint sums and pairs: general union theorems for small sets›

lemma small_Un:
  assumes X: "small X" and Y: "small Y"
  shows "small (X  Y)"
proof -
  obtain x y where "elts x  X" "elts y  Y"
    by (meson assms small_eqpoll)
  then have "X  Y  Inl ` (elts x)  Inr ` (elts y)"
    by (metis (mono_tags, lifting) Inr_Inl_iff Un_lepoll_mono disjnt_iff eqpoll_imp_lepoll eqpoll_sym f_inv_into_f inj_on_Inl inj_on_Inr inj_on_image_lepoll_2)
  then show ?thesis
    by (metis lepoll_iff replacement small_elts small_sup_iff smaller_than_small)
qed

lemma small_UN [simp,intro]:
  assumes A: "small A" and B: "x. x  A  small (B x)"
  shows "small (xA. B x)"
proof -
  obtain a where "elts a  A" 
    by (meson assms small_eqpoll)
  then obtain f where f: "bij_betw f (elts a) A"
    using eqpoll_def by blast
  have "y. elts y  B x" if "x  A" for x
    using B small_eqpoll that by blast
  then obtain g where g: "x. x  A  elts (g x)  B x" 
    by metis
  have sm: "small (Sigma (elts a) (elts  g  f))"
    by simp
  have "(xA. B x)  Sigma A B"
    by (metis image_lepoll snd_image_Sigma)
  also have "...   Sigma (elts a) (elts  g  f)"
    by (smt (verit) Sigma_eqpoll_cong bij_betw_iff_bijections comp_apply eqpoll_imp_lepoll eqpoll_sym f g)
  finally show ?thesis
    using lepoll_small sm by blast
qed

lemma small_Union [simp,intro]:
  assumes "𝒜  Collect small" "small 𝒜"
  shows "small ( 𝒜)"
  using small_UN [of 𝒜 "λx. x"] assms by (simp add: subset_iff)

subsection‹Generalised function space and lambda›

definition VLambda :: "V  (V  V)  V"
  where "VLambda A b  set ((λx. x,b x) ` elts A)"

definition app :: "[V,V]  V"
  where "app f x  THE y. x,y  elts f"

lemma beta [simp]:
  assumes "x  elts A"
  shows "app (VLambda A b) x = b x"
  using assms by (auto simp: VLambda_def app_def)

definition VPi :: "V  (V  V)  V"
  where "VPi A B  set {f  elts (VPow(VSigma A B)). elts A  Domain (pairs f)  single_valued (pairs f)}"

lemma VPi_I:
  assumes "x. x  elts A  b x  elts (B x)"
  shows "VLambda A b  elts (VPi A B)"
  proof (clarsimp simp: VPi_def, intro conjI impI)
  show "VLambda A b  VSigma A B"
    by (auto simp: assms VLambda_def split: if_split_asm)
  show "elts A  Domain (pairs (VLambda A b))"
    by (force simp: VLambda_def pairs_iff_elts)
  show "single_valued (pairs (VLambda A b))"
    by (auto simp: VLambda_def single_valued_def pairs_iff_elts)
  show "small {f. f  VSigma A B  elts A  Domain (pairs f)  single_valued (pairs f)}"
    by (metis (mono_tags, lifting) down VPow_iff mem_Collect_eq subsetI)
qed

lemma apply_pair:
  assumes f: "f  elts (VPi A B)" and x: "x  elts A"
  shows "x, app f x  elts f"
proof -
  have "x  Domain (pairs f)"
    by (metis (no_types, lifting) VPi_def assms elts_of_set empty_iff mem_Collect_eq subsetD)
  then obtain y where y: "x,y  elts f"
    using pairs_iff_elts by auto
  show ?thesis
    unfolding app_def
  proof (rule theI)
    show "x, y  elts f"
      by (rule y)
    show "z = y" if "x, z  elts f" for z
      using f unfolding VPi_def
      by (metis (mono_tags, lifting) that elts_of_set empty_iff mem_Collect_eq pairs_iff_elts single_valued_def y)
  qed
qed

lemma VPi_D:
  assumes f: "f  elts (VPi A B)" and x: "x  elts A"
  shows "app f x  elts (B x)"
proof -
  have "f  VSigma A B"
    by (metis (no_types, lifting) VPi_def elts_of_set empty_iff f VPow_iff mem_Collect_eq)
  then show ?thesis
    using apply_pair [OF assms] by blast
qed

lemma VPi_memberD:
  assumes f: "f  elts (VPi A B)" and p: "p  elts f"
  obtains x where "x  elts A" "p = x, app f x"
proof -
  have "f  VSigma A B"
    by (metis (no_types, lifting) VPi_def elts_of_set empty_iff f VPow_iff mem_Collect_eq)
  then obtain x y where "p = x,y" "x  elts A"
    using p by blast
  then have "y = app f x"
    by (metis (no_types, lifting) VPi_def apply_pair elts_of_set equals0D f mem_Collect_eq p pairs_iff_elts single_valuedD)
  then show thesis
    using p = x, y x  elts A that by blast
qed

lemma fun_ext:
  assumes "f  elts (VPi A B)" "g  elts (VPi A B)" "x. x  elts A  app f x = app g x"
  shows "f = g"
  by (metis VPi_memberD V_equalityI apply_pair assms)

lemma eta[simp]:
  assumes "f  elts (VPi A B)"
  shows "VLambda A ((app)f) = f"
  proof (rule fun_ext [OF _ assms])
  show "VLambda A (app f)  elts (VPi A B)"
    using VPi_D VPi_I assms by auto
qed auto


lemma fst_pairs_VLambda: "fst ` pairs (VLambda A f) = elts A"
  by (force simp: VLambda_def pairs_def)

lemma snd_pairs_VLambda: "snd ` pairs (VLambda A f) = f ` elts A"
  by (force simp: VLambda_def pairs_def)

lemma VLambda_eq_D1: "VLambda A f = VLambda B g  A = B"
  by (metis ZFC_in_HOL.ext fst_pairs_VLambda)

lemma VLambda_eq_D2: "VLambda A f = VLambda A g; x  elts A  f x = g x"
  by (metis beta)


subsection‹Transitive closure of a set›

definition TC :: "VV"
  where "TC  transrec (λf x. x   (f ` elts x))"

lemma TC: "TC a = a   (TC ` elts a)"
  by (metis (no_types, lifting) SUP_cong TC_def restrict_apply' transrec)

lemma TC_0 [simp]: "TC 0 = 0"
  by (metis TC ZFC_in_HOL.Sup_empty elts_0 image_is_empty sup_V_0_left)

lemma arg_subset_TC: "a  TC a"
  by (metis (no_types) TC sup_ge1)

lemma Transset_TC: "Transset(TC a)"
proof (induction a rule: eps_induct)
  case (step x)
  have 1: "v  elts (TC x)" if "v  elts u" "u  elts x" for u v
    using that unfolding TC [of x]
    using arg_subset_TC by fastforce
  have 2: "v  elts (TC x)" if "v  elts u" "xelts x. u  elts (TC x)" for u v
    using that step unfolding TC [of x] Transset_def by auto
  show ?case
    unfolding Transset_def
    by (subst TC) (force intro: 1 2)
qed

lemma TC_least: "Transset x;  ax  TC a  x"
proof (induction a rule: eps_induct)
  case (step y)
  show ?case
  proof (cases "y=0")
    case True
    then show ?thesis
      by auto
  next
    case False
    have " (TC ` elts y)  x"
    proof (rule cSup_least)
      show "TC ` elts y  {}"
        using False by auto
      show "z  x" if "z  TC ` elts y" for z
        using that by (metis Transset_def image_iff step.IH step.prems vsubsetD)
    qed
    then show ?thesis
      by (simp add: step TC [of y])
  qed
qed

definition less_TC (infix "" 50)
  where "x  y  x  elts (TC y)"

definition le_TC (infix "" 50)
  where "x  y  x  y  x=y"

lemma less_TC_imp_not_le: "x  a  ¬ a  x"
proof (induction a arbitrary: x rule: eps_induct)
  case (step a)
  then show ?case
    unfolding TC[of a] less_TC_def
    using Transset_TC Transset_def by force
qed

lemma non_TC_less_0 [iff]: "¬ (x  0)"
  using less_TC_imp_not_le by blast

lemma less_TC_iff: "x  y  (z  elts y. x  z)"
  by (auto simp: less_TC_def le_TC_def TC [of y])

lemma nonzero_less_TC: "x  0  0  x"
  by (metis eps_induct le_TC_def less_TC_iff trad_foundation)

lemma less_irrefl_TC [simp]: "¬ x  x"
  using less_TC_imp_not_le by blast

lemma less_asym_TC: "x  y; y  x  False"
  by (metis TC_least Transset_TC Transset_def antisym_conv less_TC_def less_TC_imp_not_le order_refl)

lemma le_antisym_TC: "x  y; y  x  x = y"
  using le_TC_def less_asym_TC by auto

lemma less_le_TC: "x  y  x  y  x  y"
  using le_TC_def less_asym_TC by blast

lemma less_imp_le_TC [iff]: "x  y  x  y"
  by (simp add: le_TC_def)

lemma le_TC_refl [iff]: "x  x"
  by (simp add: le_TC_def)

lemma le_TC_trans [trans]: "x  y; y  z  x  z"
  by (smt (verit, best) TC_least Transset_TC Transset_def le_TC_def less_TC_def vsubsetD)

context order
begin

lemma nless_le_TC: "(¬ a  b)  (¬ a  b)  a = b"
  using le_TC_def less_asym_TC by blast

lemma eq_refl_TC: "x = y  x  y"
  by simp

local_setup HOL_Order_Tac.declare_order {
    ops = {eq = @{term (=) :: V  V  bool}, le = @{term (⊑)}, lt = @{term (⊏)}},
    thms = {trans = @{thm le_TC_trans}, refl = @{thm le_TC_refl}, eqD1 = @{thm eq_refl_TC},
            eqD2 = @{thm eq_refl_TC[OF sym]}, antisym = @{thm le_antisym_TC}, contr = @{thm notE}},
    conv_thms = {less_le = @{thm eq_reflection[OF less_le_TC]},
                 nless_le = @{thm eq_reflection[OF nless_le_TC]}}
  }

end


lemma less_TC_trans [trans]: "x  y; y  z  x  z" 
  and less_le_TC_trans: "x  y; y  z  x  z" 
  and le_less_TC_trans [trans]: "x  y; y  z  x  z"
  by simp_all

lemma TC_sup_distrib: "TC (x  y) = TC x  TC y"
  by (simp add: Sup_Un_distrib TC [of "x  y"] TC [of x] TC [of y] image_Un sup.assoc sup_left_commute)

lemma TC_Sup_distrib:
  assumes "small X" shows "TC (X) = (TC ` X)"
proof -
  have "X   (TC ` X)"
    using arg_subset_TC by fastforce
  moreover have " (xX. TC ` elts x)   (TC ` X)"
    using assms 
    by clarsimp (meson TC_least Transset_TC Transset_def arg_subset_TC replacement vsubsetD)
  ultimately
  have " X   (xX. TC ` elts x)   (TC ` X)"
    by simp
  moreover have " (TC ` X)   X   (xX. TC ` elts x)"
  proof (clarsimp simp add: Sup_le_iff assms)
    show "xX. y  elts x"
      if "x  X" "y  elts (TC x)" "xX. uelts x. y  elts (TC u)" for x y
      using that by (auto simp: TC [of x])
  qed
  ultimately show ?thesis
    using Sup_Un_distrib TC [of "X"] image_Union assms
    by (simp add: image_Union inf_sup_aci(5) sup.absorb_iff2)
qed

lemma TC': "TC x = x  TC ( (elts x))"
  by (simp add: TC [of x] TC_Sup_distrib)

lemma TC_eq_0_iff [simp]: "TC x = 0  x=0"
  using arg_subset_TC by fastforce

text‹A distinctive induction principle›
lemma TC_induct_down_lemma:
  assumes ab: "a  b" and base: "b  d"
      and step: "y z. y  b; y  elts d; z  elts y  z  elts d"
    shows "a  elts d"
proof -
  have "Transset (TC b  d)"
    using Transset_TC
    unfolding Transset_def
    by (metis inf.bounded_iff less_TC_def less_eq_V_def local.step subsetI vsubsetD) 
  moreover have "b  TC b  d"
    by (simp add: arg_subset_TC base)
  ultimately show ?thesis
    using TC_least [THEN vsubsetD] ab unfolding less_TC_def
    by (meson TC_least le_inf_iff vsubsetD)
qed

lemma TC_induct_down [consumes 1, case_names base step small]:
  assumes "a  b"
    and "y. y  elts b  P y"
    and "y z. y  b; P y; z  elts y  P z"
    and "small (Collect P)"
  shows "P a"
  using TC_induct_down_lemma [of a b "set (Collect P)"] assms
  by (metis elts_of_set mem_Collect_eq vsubsetI)

subsection‹Rank of a set›

definition rank :: "VV"
  where "rank a  transrec (λf x. set (yelts x. elts (succ(f y)))) a"

lemma rank: "rank a = set(y  elts a. elts (succ(rank y)))"
  by (subst rank_def [THEN def_transrec], simp)

lemma rank_Sup: "rank a = ((λy. succ(rank y)) ` elts a)"
  by (metis elts_Sup image_image rank replacement set_of_elts small_elts)

lemma Ord_rank [simp]: "Ord(rank a)"
proof (induction a rule: eps_induct)
  case (step x)
  then show ?case
    unfolding rank_Sup [of x]
    by (metis (mono_tags, lifting) Ord_Sup Ord_succ imageE)
qed

lemma rank_of_Ord: "Ord i  rank i = i"
  by (induction rule: Ord_induct) (metis (no_types, lifting) Ord_equality SUP_cong rank_Sup)

lemma Ord_iff_rank: "Ord x  rank x = x"
  using Ord_rank [of x] rank_of_Ord by fastforce

lemma rank_lt: "a  elts b  rank a < rank b"
  by (metis Ord_linear2 Ord_rank ZFC_in_HOL.SUP_le_iff rank_Sup replacement small_elts succ_le_iff order.irrefl)

lemma rank_0 [simp]: "rank 0 = 0"
  using transrec Ord_0 rank_def rank_of_Ord by presburger

lemma rank_succ [simp]: "rank(succ x) = succ(rank x)"
proof (rule order_antisym)
  show "rank (succ x)  succ (rank x)"
    by (metis (no_types, lifting) Sup_insert elts_of_set elts_succ image_insert rank small_UN small_elts subset_insertI sup.orderE vsubsetI)
  show "succ (rank x)  rank (succ x)"
    by (metis (mono_tags, lifting) ZFC_in_HOL.Sup_upper elts_succ image_insert insertI1 rank_Sup replacement small_elts)
qed

lemma rank_mono: "a  b  rank a  rank b"
  using rank [of a] rank [of b] small_UN by force

lemma VsetI: "rank b  i  b  elts (Vset i)"
proof (induction i arbitrary: b rule: eps_induct)
  case (step x)
  then consider "rank b  elts x" | "(yelts x. rank b  elts (TC y))"
    using le_TC_def less_TC_def less_TC_iff by fastforce
  then have "yelts x. b  Vset y"
  proof cases
    case 1
    then have "b  Vset (rank b)"
      unfolding less_eq_V_def subset_iff
      by (meson Ord_mem_iff_lt Ord_rank le_TC_refl less_TC_iff rank_lt step.IH)
    then show ?thesis
      using "1" by blast
  next
    case 2
    then show ?thesis
      using step.IH
      unfolding less_eq_V_def subset_iff less_TC_def
      by (meson Ord_mem_iff_lt Ord_rank Transset_TC Transset_def rank_lt vsubsetD)
  qed
  then show ?case
    by (simp add: Vset [of x])
qed

lemma Ord_VsetI: "Ord i; rank b < i  b  elts (Vset i)"
  by (meson Ord_mem_iff_lt Ord_rank VsetI arg_subset_TC less_TC_def vsubsetD)

lemma arg_le_Vset_rank: "a  Vset(rank a)"
  by (simp add: Ord_VsetI rank_lt vsubsetI)

lemma two_in_Vset:
  obtains α where  "x  elts (Vset α)" "y  elts (Vset α)"
  by (metis Ord_rank Ord_VsetI elts_of_set insert_iff rank_lt small_elts small_insert_iff)

lemma rank_eq_0_iff [simp]: "rank x = 0  x=0"
  using arg_le_Vset_rank by fastforce

lemma small_ranks_imp_small:
  assumes "small (rank ` A)" shows "small A"
proof -
  define i where "i  set ((elts ` (rank ` A)))"
  have "Ord i"
    unfolding i_def using Ord_Union Ord_rank assms imageE by blast
  have *: "Vset (rank x)  (Vset i)" if "x  A" for x
    unfolding i_def by (metis Ord_rank Sup_V_def ZFC_in_HOL.Sup_upper Vfrom_mono assms imageI le_less that)
  have "A  elts (VPow (Vset i))"
    by (meson "*" VPow_iff arg_le_Vset_rank order.trans subsetI)
  then show ?thesis
    using down by blast
qed

lemma rank_Union: "rank( A) =  (rank ` A)"
proof (rule order_antisym)
  have "elts (yelts ( A). succ (rank y))  elts ( (rank ` A))"
    by clarsimp (meson Ord_mem_iff_lt Ord_rank less_V_def rank_lt vsubsetD)
  then show "rank ( A)   (rank ` A)"
    by (metis less_eq_V_def rank_Sup)
  show " (rank ` A)  rank ( A)"
  proof (cases "small A")
    case True
    then show ?thesis
      by (simp add: ZFC_in_HOL.SUP_le_iff ZFC_in_HOL.Sup_upper rank_mono)
  next
    case False
    then have "¬ small (rank ` A)"
      using small_ranks_imp_small by blast
    then show ?thesis
      by blast
  qed
qed

lemma small_bounded_rank:  "small {x. rank x  elts a}"
proof -
  have "{x. rank x  elts a}  {x. rank x  a}"
    using less_TC_iff by auto
  also have "  elts (Vset a)"
    using VsetI by blast
  finally show ?thesis
    using down by simp
qed

lemma small_bounded_rank_le:  "small {x. rank x  a}"
  using small_bounded_rank [of "VPow a"] VPow_iff [of _ a]  by simp

lemma TC_rank_lt: "a  b  rank a < rank b"
proof (induction rule: TC_induct_down)
  case (base y)
  then show ?case
    by (simp add: rank_lt)
next
  case (step y z)
  then show ?case
    using less_trans rank_lt by blast
next
  case small
  show ?case
    using smaller_than_small [OF small_bounded_rank_le [of "rank b"]]
    by (simp add: Collect_mono less_V_def)
qed

lemma TC_rank_mem: "x  y  rank x  elts (rank y)"
  by (simp add: Ord_mem_iff_lt TC_rank_lt)

lemma wf_TC_less: "wf {(x,y). x  y}"
  proof (rule wf_subset [OF wf_inv_image [OF foundation, of rank]])
    show "{(x, y). x  y}  inv_image {(x, y). x  elts y} rank"
      by (auto simp: TC_rank_mem inv_image_def)
qed

lemma less_TC_minimal:
  assumes "P a"
  obtains x where "P x" "x  a" "y. y  x  ¬ P y"
  using wfE_min' [OF wf_TC_less, of "{x. P x  x  a}"]
  by simp (metis le_TC_def less_le_TC_trans assms)

lemma Vfrom_rank_eq: "Vfrom A (rank(x)) = Vfrom A x"
proof (rule order_antisym)
  show "Vfrom A (rank x)  Vfrom A x"
  proof (induction x rule: eps_induct)
    case (step x)
    have "(jelts (rank x). VPow (Vfrom A j))  (jelts x. VPow (Vfrom A j))"
      apply (rule Sup_least)
      apply (clarsimp simp add: rank [of x])
      by (meson Ord_in_Ord Ord_rank OrdmemD Vfrom_mono order.trans less_imp_le order.refl step)
    then show ?case
      by (simp add: Vfrom [of _ x] Vfrom [of _ "rank(x)"] sup.coboundedI2)
qed
  show "Vfrom A x  Vfrom A (rank x)"
  proof (induction x rule: eps_induct)
    case (step x)
    have "(jelts x. VPow (Vfrom A j))  (jelts (rank x). VPow (Vfrom A j))"
      using step.IH TC_rank_mem less_TC_iff by force
    then show ?case
      by (simp add: Vfrom [of _ x] Vfrom [of _ "rank(x)"] sup.coboundedI2)
  qed
qed

lemma Vfrom_succ: "Vfrom A (succ(i)) = A  VPow(Vfrom A i)"
  by (metis Ord_rank Vfrom_rank_eq Vfrom_succ_Ord rank_succ)

lemma Vset_succ_TC:
  assumes "x  elts (Vset (ZFC_in_HOL.succ k))" "u  x"
  shows "u  elts (Vset k)"
  using assms
  using TC_least Transset_Vfrom Vfrom_succ less_TC_def by auto

subsection‹Cardinal Numbers›

text‹We extend the membership relation to a wellordering›
definition VWO :: "(V × V) set"
  where "VWO  @r. {(x,y). x  elts y}  r  Well_order r  Field r = UNIV"

lemma VWO: "{(x,y). x  elts y}  VWO  Well_order VWO  Field VWO = UNIV"
  unfolding VWO_def
  by (metis (mono_tags, lifting) VWO_def foundation someI_ex total_well_order_extension)

lemma wf_VWO: "wf(VWO - Id)"
  using VWO well_order_on_def by blast

lemma wf_Ord_less: "wf {(x, y). Ord y  x < y}"
  by (metis (no_types, lifting) Ord_mem_iff_lt eps_induct wfPUNIVI wfP_def)

lemma refl_VWO: "refl VWO"
  using VWO order_on_defs by fastforce

lemma trans_VWO: "trans VWO"
  using VWO by (simp add: VWO wo_rel.TRANS wo_rel_def)

lemma antisym_VWO: "antisym VWO"
  using VWO by (simp add: VWO wo_rel.ANTISYM wo_rel_def)

lemma total_VWO: "total VWO"
    using VWO by (metis wo_rel.TOTAL wo_rel.intro)

lemma total_VWOId: "total (VWO-Id)"
  by (simp add: total_VWO)

lemma Linear_order_VWO: "Linear_order VWO"
  using VWO well_order_on_def by blast

lemma wo_rel_VWO: "wo_rel VWO"
  using VWO wo_rel_def by blast

subsubsection ‹Transitive Closure and VWO›

lemma mem_imp_VWO: "x  elts y  (x,y)  VWO"
  using VWO by blast

lemma less_TC_imp_VWO: "x  y  (x,y)  VWO"
  unfolding less_TC_def
proof (induction y arbitrary: x rule: eps_induct)
  case (step y' u)
  then consider "u  elts y'" | v where "v  elts y'" "u  elts (TC v)"
    by (auto simp: TC [of y'])
  then show ?case
  proof cases
    case 2
    then show ?thesis
      by (meson mem_imp_VWO step.IH transD trans_VWO)
  qed (use mem_imp_VWO in blast)
qed

lemma le_TC_imp_VWO: "x  y  (x,y)  VWO"
  by (metis Diff_iff Linear_order_VWO Linear_order_in_diff_Id UNIV_I VWO le_TC_def less_TC_imp_VWO)

lemma le_TC_0_iff [simp]: "x  0  x = 0"
  by (simp add: le_TC_def)

lemma less_TC_succ: " x  succ β  x  β  x = β"
  by (metis elts_succ insert_iff le_TC_def less_TC_iff)

lemma le_TC_succ: "x  succ β  x  β  x = succ β"
  by (simp add: le_TC_def less_TC_succ)

lemma Transset_TC_eq [simp]: "Transset x  TC x = x"
  by (simp add: TC_least arg_subset_TC eq_iff)

lemma Ord_TC_less_iff: "Ord α; Ord β  β  α  β < α"
  by (metis Ord_def Ord_mem_iff_lt Transset_TC_eq less_TC_def)

lemma Ord_mem_iff_less_TC: "Ord l  k  elts l  k  l"
  by (simp add: Ord_def less_TC_def)

lemma le_TC_Ord: "β  α; Ord α  Ord β"
  by (metis Ord_def Ord_in_Ord Transset_TC_eq le_TC_def less_TC_def)

lemma Ord_less_TC_mem:
  assumes "Ord α" "β  α" shows "β  elts α"
  using Ord_def assms less_TC_def by auto

lemma VWO_TC_le: "Ord α; Ord β; (β, α)  VWO  β  α"
proof (induct α arbitrary: β rule: Ord_induct)
  case (step α)
  then show ?case
    by (metis DiffI IdD Linear_order_VWO Linear_order_in_diff_Id Ord_linear Ord_mem_iff_less_TC VWO iso_tuple_UNIV_I le_TC_def mem_imp_VWO)
qed

lemma VWO_iff_Ord_le [simp]: "Ord α; Ord β  (β, α)  VWO  β  α"
  by (metis VWO_TC_le Ord_TC_less_iff le_TC_def le_TC_imp_VWO le_less)

lemma zero_TC_le [iff]: "0  y"
  using le_TC_def nonzero_less_TC by auto

lemma succ_le_TC_iff: "Ord j  succ i  j  i  j"
  by (metis Ord_in_Ord Ord_linear Ord_mem_iff_less_TC Ord_succ le_TC_def less_TC_succ less_asym_TC)

lemma VWO_0_iff [simp]: "(x,0)  VWO  x=0"
proof
  show "x = 0" if "(x, 0)  VWO"
    using zero_TC_le [of x] le_TC_imp_VWO that
    by (metis DiffI Linear_order_VWO Linear_order_in_diff_Id UNIV_I VWO pair_in_Id_conv)
qed auto

lemma VWO_antisym:
  assumes "(x,y)  VWO" "(y,x)  VWO" shows "x=y"
  by (metis Diff_iff IdD Linear_order_VWO Linear_order_in_diff_Id UNIV_I VWO assms)

subsubsection ‹Relation VWF›

definition VWF where "VWF  VWO - Id"

lemma wf_VWF [iff]: "wf VWF"
  by (simp add: VWF_def wf_VWO)

lemma trans_VWF [iff]: "trans VWF"
  by (simp add: VWF_def antisym_VWO trans_VWO trans_diff_Id)

lemma asym_VWF [iff]: "asym VWF"
  by (metis wf_VWF wf_imp_asym)

lemma total_VWF [iff]: "total VWF"
  using VWF_def total_VWOId by auto

lemma total_on_VWF [iff]: "total_on A VWF"
  by (meson UNIV_I total_VWF total_on_def)

lemma VWF_asym:
  assumes "(x,y)  VWF" "(y,x)  VWF" shows False
  using VWF_def assms wf_VWO wf_not_sym by fastforce

lemma VWF_non_refl [iff]: "(x,x)  VWF"
  by simp

lemma VWF_iff_Ord_less [simp]: "Ord α; Ord β  (α,β)  VWF  α < β"
  by (simp add: VWF_def less_V_def)

lemma mem_imp_VWF: "x  elts y  (x,y)  VWF"
  using VWF_def mem_imp_VWO by fastforce


subsection‹Order types›

definition ordermap :: "'a set  ('a × 'a) set  'a  V"
  where "ordermap A r  wfrec r (λf x. set (f ` {y  A. (y,x)  r}))"

definition ordertype :: "'a set  ('a × 'a) set  V"
  where "ordertype A r  set (ordermap A r ` A)"

lemma ordermap_type:
    "small A  ordermap A r  A  elts (ordertype A r)"
  by (simp add: ordertype_def)

lemma ordermap_in_ordertype [intro]: "a  A; small A  ordermap A r a  elts (ordertype A r)"
  by (simp add: ordertype_def)

lemma ordermap: "wf r  ordermap A r a = set (ordermap A r ` {y  A. (y,a)  r})"
  unfolding ordermap_def
  by (auto simp: wfrec_fixpoint adm_wf_def)

lemma wf_Ord_ordermap [iff]: assumes "wf r" "trans r" shows "Ord (ordermap A r x)"
  using wf r
proof (induction x rule: wf_induct_rule)
  case (less u)
  have "Transset (set (ordermap A r ` {y  A. (y, u)  r}))"
  proof (clarsimp simp add: Transset_def)
    show "x  ordermap A r ` {y  A. (y, u)  r}"
      if "small (ordermap A r ` {y  A. (y, u)  r})"
        and x: "x  elts (ordermap A r y)" and "y  A" "(y, u)  r" for x y
    proof -
      have "ordermap A r y = ZFC_in_HOL.set (ordermap A r ` {a  A. (a, y)  r})"
        using ordermap assms(1) by force
      then have "x  ordermap A r ` {z  A. (z, y)  r}"
        by (metis (no_types, lifting) elts_of_set empty_iff x)
      then have "v. v  A  (v, u)  r  x = ordermap A r v"
        using that transD [OF trans r] by blast
      then show ?thesis
        by blast
    qed
  qed
  moreover have "Ord x"
    if "x  elts (set (ordermap A r ` {y  A. (y, u)  r}))" for x
    using that less by (auto simp: split: if_split_asm)
  ultimately show ?case
    by (metis (full_types) Ord_def ordermap assms(1))
qed

lemma wf_Ord_ordertype: assumes "wf r" "trans r" shows "Ord(ordertype A r)"
proof -
  have "y  set (ordermap A r ` A)"
    if "y = ordermap A r x" "x  A" "small (ordermap A r ` A)" for x y
    using that by (auto simp: less_eq_V_def ordermap [OF wf r, of A x])
  moreover have "z  y" if "y  ordermap A r ` A" "z  elts y" for y z
    by (metis wf_Ord_ordermap OrdmemD assms imageE order.strict_implies_order that)
  ultimately show ?thesis
    unfolding ordertype_def Ord_def Transset_def by simp
qed

lemma Ord_ordertype [simp]: "Ord(ordertype A VWF)"
  using wf_Ord_ordertype by blast

lemma Ord_ordermap [simp]: "Ord (ordermap A VWF x)"
  by blast

lemma ordertype_singleton [simp]:
  assumes "wf r" 
  shows "ordertype {x} r = 1"
proof -
  have : "{y. y = x  (y, x)  r} = {}"
    using assms by auto
  show ?thesis
    by (auto simp add: ordertype_def assms  ordermap [where a=x])
qed


subsubsection@{term ordermap} preserves the orderings in both directions›

lemma ordermap_mono:
  assumes wx: "(w, x)  r" and "wf r" "w  A" "small A"
    shows "ordermap A r w  elts (ordermap A r x)"
proof -
  have "small {a  A. (a, x)  r}  w  A  (w, x)  r"
    by (simp add: assms)
  then show ?thesis
    using assms ordermap [of r A]
    by (metis (no_types, lifting) elts_of_set image_eqI mem_Collect_eq replacement)
qed

lemma converse_ordermap_mono:
  assumes "ordermap A r y  elts (ordermap A r x)" "wf r" "total_on A r" "x  A" "y  A" "small A"
  shows "(y, x)  r"
proof (cases "x = y")
  case True
  then show ?thesis
    using assms(1) mem_not_refl by blast
next
  case False
  then consider "(x,y)  r" | "(y,x)  r"
    using total_on A r assms by (meson UNIV_I total_on_def)
  then show ?thesis
    by (meson ordermap_mono assms mem_not_sym)
qed

lemma converse_ordermap_mono_iff:
  assumes "wf r" "total_on A r" "x  A" "y  A" "small A"
  shows "ordermap A r y  elts (ordermap A r x)  (y, x)  r"
  by (metis assms converse_ordermap_mono ordermap_mono)

lemma ordermap_surj: "elts (ordertype A r)  ordermap A r ` A"
  unfolding ordertype_def by simp

lemma ordermap_bij:
  assumes "wf r" "total_on A r" "small A"
  shows "bij_betw (ordermap A r) A (elts (ordertype A r))"
  unfolding bij_betw_def
  proof (intro conjI)
    show "inj_on (ordermap A r) A"
    unfolding inj_on_def by (metis assms mem_not_refl ordermap_mono total_on_def)
  show "ordermap A r ` A = elts (ordertype A r)"
    by (metis ordertype_def small A elts_of_set replacement)
qed

lemma ordermap_eq_iff [simp]: 
  "x  A; y  A; wf r; total_on A r; small A  ordermap A r x = ordermap A r y  x = y"
  by (metis bij_betw_iff_bijections ordermap_bij)

lemma inv_into_ordermap: "α  elts (ordertype A r)  inv_into A (ordermap A r) α  A"
  by (meson in_mono inv_into_into ordermap_surj)

lemma ordertype_nat_imp_finite:
  assumes "ordertype A r = ord_of_nat m" "small A" "wf r" "total_on A r"
  shows "finite A"
proof -
  have "A  elts m"
    using eqpoll_def assms ordermap_bij by fastforce 
  then show ?thesis
    using eqpoll_finite_iff finite_Ord_omega by blast
qed

lemma wf_ordertype_eqpoll:
  assumes "wf r" "total_on A r" "small A"
  shows "elts (ordertype A r)  A"
  using assms eqpoll_def eqpoll_sym ordermap_bij by blast

lemma ordertype_eqpoll:
  assumes "small A"
  shows "elts (ordertype A VWF)  A"
  using assms wf_ordertype_eqpoll total_VWF wf_VWF
  by (simp add: wf_ordertype_eqpoll total_on_def)

subsection ‹More advanced @{term ordertype} and @{term ordermap} results›

lemma ordermap_VWF_0 [simp]: "ordermap A VWF 0 = 0"
  by (simp add: ordermap wf_VWO VWF_def)

lemma ordertype_empty [simp]: "ordertype {} r = 0"
  by (simp add: ordertype_def)

lemma ordertype_eq_0_iff [simp]: "small X; wf r  ordertype X r = 0  X = {}"
  by (metis ordertype_def elts_of_set replacement image_is_empty zero_V_def)

lemma ordermap_mono_less:
  assumes "(w, x)  r"
      and "wf r" "trans r"
      and "w  A" "x  A"
      and "small A"
    shows "ordermap A r w < ordermap A r x"
  by (simp add: OrdmemD assms ordermap_mono)

lemma ordermap_mono_le:
  assumes "(w, x)  r  w=x"
      and "wf r" "trans r"
      and "w  A" "x  A"
      and "small A"
    shows "ordermap A r w  ordermap A r x"
  by (metis assms dual_order.strict_implies_order eq_refl ordermap_mono_less)

lemma converse_ordermap_le_mono:
  assumes "ordermap A r y  ordermap A r x" "wf r" "total r"  "x  A" "small A"
  shows "(y, x)  r  y=x"
  by (meson UNIV_I assms mem_not_refl ordermap_mono total_on_def vsubsetD)

lemma ordertype_mono:
  assumes "X  Y" and r: "wf r" "trans r" and "small Y"
  shows "ordertype X r  ordertype Y r"
proof -
  have "small X"
    using assms smaller_than_small by fastforce 
  have *: "ordermap X r x  ordermap Y r x" for x
    using wf r
  proof (induction x rule: wf_induct_rule)
    case (less x)
    have "ordermap X r z < ordermap Y r x" if "z  X" and zx: "(z,x)  r" for z
      using less [OF zx] assms
      by (meson Ord_linear2 OrdmemD wf_Ord_ordermap ordermap_mono in_mono leD that(1) vsubsetD zx)
    then show ?case
      by (auto simp add: ordermap [of _ X x] small X Ord_mem_iff_lt set_image_le_iff less_eq_V_def r)
  qed
  show ?thesis
  proof -
    have "ordermap Y r ` Y = elts (ordertype Y r)"
      by (metis ordertype_def small Y elts_of_set replacement)
    then have "ordertype Y r  ordermap X r ` X"
      using "*" X  Y by fastforce
    then show ?thesis
      by (metis Ord_linear2 Ord_mem_iff_lt ordertype_def wf_Ord_ordertype small X elts_of_set replacement r)
  qed
qed

corollary ordertype_VWF_mono:
  assumes "X  Y" "small Y"
  shows "ordertype X VWF  ordertype Y VWF"
  using assms by (simp add: ordertype_mono)

lemma ordertype_UNION_ge:
  assumes "A  𝒜" "wf r" "trans r" "𝒜  Collect small" "small 𝒜"
  shows "ordertype A r  ordertype (𝒜) r" 
  by (rule ordertype_mono) (use assms in auto)

lemma inv_ordermap_mono_less:
  assumes "(inv_into M (ordermap M r) α, inv_into M (ordermap M r) β)  r" 
    and "small M" and α: "α  elts (ordertype M r)" and β: "β  elts (ordertype M r)"
    and "wf r" "trans r"
  shows "α < β"
proof -
  have "α = ordermap M r (inv_into M (ordermap M r) α)"
    by (metis α f_inv_into_f ordermap_surj subset_eq)
  also have " < ordermap M r (inv_into M (ordermap M r) β)"
    by (meson α β assms in_mono inv_into_into ordermap_mono_less ordermap_surj)
  also have " = β"
    by (meson β f_inv_into_f in_mono ordermap_surj)
  finally show ?thesis .
qed

lemma inv_ordermap_mono_eq:
  assumes "inv_into M (ordermap M r) α = inv_into M (ordermap M r) β" 
    and "α  elts (ordertype M r)" "β  elts (ordertype M r)"
  shows "α = β"
  by (metis assms f_inv_into_f ordermap_surj subsetD)

lemma inv_ordermap_VWF_mono_le:
  assumes "inv_into M (ordermap M VWF) α  inv_into M (ordermap M VWF) β" 
    and "M  ON" "small M" and α: "α  elts (ordertype M VWF)" and β: "β  elts (ordertype M VWF)"
  shows "α  β"
proof -
  have "α = ordermap M VWF (inv_into M (ordermap M VWF) α)"
    by (metis α f_inv_into_f ordermap_surj subset_eq)
  also have "  ordermap M VWF (inv_into M (ordermap M VWF) β)"
    by (metis ON_imp_Ord VWF_iff_Ord_less assms dual_order.strict_implies_order elts_of_set eq_refl inv_into_into order.not_eq_order_implies_strict ordermap_mono_less ordertype_def replacement trans_VWF wf_VWF)
  also have " = β"
    by (meson β f_inv_into_f in_mono ordermap_surj)
  finally show ?thesis .
qed

lemma inv_ordermap_VWF_mono_iff:
  assumes "M  ON" "small M" and "α  elts (ordertype M VWF)" and "β  elts (ordertype M VWF)"
  shows "inv_into M (ordermap M VWF) α  inv_into M (ordermap M VWF) β  α  β"
  by (metis ON_imp_Ord Ord_linear_le assms dual_order.eq_iff inv_into_ordermap inv_ordermap_VWF_mono_le)

lemma inv_ordermap_VWF_strict_mono_iff:
  assumes "M  ON" "small M" and "α  elts (ordertype M VWF)" and "β  elts (ordertype M VWF)"
  shows "inv_into M (ordermap M VWF) α < inv_into M (ordermap M VWF) β  α < β"
  by (simp add: assms inv_ordermap_VWF_mono_iff less_le_not_le)

lemma strict_mono_on_ordertype:
  assumes "M  ON" "small M"
  obtains f where "f  elts (ordertype M VWF)  M" "strict_mono_on (elts (ordertype M VWF)) f"
proof 
  show "inv_into M (ordermap M VWF)  elts (ordertype M VWF)  M"
    by (meson Pi_I' in_mono inv_into_into ordermap_surj)
  show "strict_mono_on (elts (ordertype M VWF)) (inv_into M (ordermap M VWF))"
  proof (clarsimp simp: strict_mono_on_def)
    fix x y
    assume "x  elts (ordertype M VWF)" "y  elts (ordertype M VWF)" "x < y"
    then show "inv_into M (ordermap M VWF) x < inv_into M (ordermap M VWF) y"
      using assms by (meson ON_imp_Ord Ord_linear2 inv_into_into inv_ordermap_VWF_mono_le leD ordermap_surj subsetD)
  qed
qed

lemma ordermap_inc_eq:
  assumes "x  A" "small A"
    and π: "x y. xA; yA; (x,y)  r  (π x, π y)  s"
    and r: "wf r" "total_on A r" and "wf s" 
  shows "ordermap (π ` A) s (π x) = ordermap A r x"
  using wf r x  A
proof (induction x rule: wf_induct_rule)
  case (less x)
  then have 1: "{y  A. (y, x)  r} = A  {y. (y, x)  r}"
    using r by auto
  have 2: "{y  π ` A. (y, π x)  s} = π ` A  {y. (y, π x)  s}"
    by auto
  have invπ: "x y. xA; yA; (π x, π y)  s  (x, y)  r"
    by (metis π wf s total_on A r total_on_def wf_not_sym)
  have eq: "f ` (π ` A  {y. (y, π x)  s}) = (f  π) ` (A  {y. (y, x)  r})" for f :: "'b  V"
    using less by (auto simp: image_subset_iff invπ π)
  show ?case
    using less
    by (simp add: ordermap [OF wf r, of _ x] ordermap [OF wf s, of _ "π x"] 1 2 eq)
qed

lemma ordertype_inc_eq:
  assumes "small A"
    and π: "x y. xA; yA; (x,y)  r  (π x, π y)  s"
    and r: "wf r" "total_on A r" and "wf s" 
  shows "ordertype (π ` A) s = ordertype A r"
proof -
  have "ordermap (π ` A) s (π x) = ordermap A r x" if "x  A" for x
    using assms that by (auto simp: ordermap_inc_eq)
  then show ?thesis
    unfolding ordertype_def
    by (metis (no_types, lifting) image_cong image_image)
qed

lemma ordertype_inc_le:
  assumes "small A" "small B"
    and π: "x y. xA; yA; (x,y)  r  (π x, π y)  s"
    and r: "wf r" "total_on A r" and "wf s" "trans s"
    and "π ` A  B"
  shows "ordertype A r  ordertype B s"
  by (metis assms ordertype_inc_eq ordertype_mono)

corollary ordertype_VWF_inc_eq:
  assumes "A  ON" "π ` A  ON" "small A" and "x y. xA; yA; x<y  π x < π y"
  shows "ordertype (π ` A) VWF = ordertype A VWF"
proof (rule ordertype_inc_eq)
  show "(π x, π y)  VWF"
    if "x  A" "y  A" "(x, y)  VWF" for x y
    using that ON_imp_Ord assms by auto
  show "total_on A VWF"
    by (meson UNIV_I total_VWF total_on_def)
qed (use assms in auto)

lemma ordertype_image_ordermap:
  assumes "small A" "X  A" "wf r" "trans r" "total_on X r"
  shows "ordertype (ordermap A r ` X) VWF = ordertype X r"
proof (rule ordertype_inc_eq)
  show "small X"
    by (meson assms smaller_than_small)
  show "(ordermap A r x, ordermap A r y)  VWF"
    if "x  X" "y  X" "(x, y)  r" for x y
    by (meson that wf_Ord_ordermap VWF_iff_Ord_less assms ordermap_mono_less subsetD)
qed (use assms in auto)
    
lemma ordertype_map_image:
  assumes "B  A" "small A"
  shows "ordertype (ordermap A VWF ` A - ordermap A VWF ` B) VWF = ordertype (A - B) VWF"
proof -
  have "ordermap A VWF ` A - ordermap A VWF ` B = ordermap A VWF ` (A - B)"
    using assms by auto
  then have "ordertype (ordermap A VWF ` A - ordermap A VWF ` B) VWF = ordertype (ordermap A VWF ` (A - B)) VWF"
    by simp
  also have " = ordertype (A - B) VWF"
    using small A ordertype_image_ordermap by fastforce
  finally show ?thesis .
qed

proposition ordertype_le_ordertype:
  assumes r: "wf r" "total_on A r" and "small A"
  assumes s: "wf s" "total_on B s" "trans s" and "small B"
  shows "ordertype A r  ordertype B s 
         (f  A  B. inj_on f A  (x  A. y  A. ((x,y)  r  (f x, f y)  s)))"
    (is "?lhs = ?rhs")
proof
  assume L: ?lhs
  define f where "f  inv_into B (ordermap B s)  ordermap A r"
  show ?rhs
  proof (intro bexI conjI ballI impI)
    have AB: "elts (ordertype A r)  ordermap B s ` B"
      by (metis L assms(7) ordertype_def replacement set_of_elts small_elts subset_iff_less_eq_V)
    have bijA: "bij_betw (ordermap A r) A (elts (ordertype A r))"
      using ordermap_bij small A r by blast
    have "inv_into B (ordermap B s) (ordermap A r i)  B" if "i  A" for i
      by (meson L small A inv_into_into ordermap_in_ordertype ordermap_surj subsetD that vsubsetD)
    then show "f  A  B"
      by (auto simp: Pi_iff f_def)
    show "inj_on f A"
    proof (clarsimp simp add: f_def inj_on_def)
      fix x y
      assume "x  A" "y  A"
        and "inv_into B (ordermap B s) (ordermap A r x) = inv_into B (ordermap B s) (ordermap A r y)"
      then have "ordermap A r x = ordermap A r y"
        by (meson AB small A inv_into_injective ordermap_in_ordertype subsetD)
      then show "x = y"
        by (metis x  A y  A bijA bij_betw_inv_into_left)
    qed
  next
    fix x y
    assume "x  A" "y  A" and "(x, y)  r"
    have : "ordermap A r y  ordermap B s ` B"
      by (meson L y  A small A in_mono ordermap_in_ordertype ordermap_surj vsubsetD)
    moreover have : "x. inv_into B (ordermap B s) (ordermap A r x) = f x"
      by (simp add: f_def)
    then have *: "ordermap B s (f y) = ordermap A r y"
      using  by (metis f_inv_into_f)
    moreover have "ordermap A r x  ordermap B s ` B"
      by (meson L x  A small A in_mono ordermap_in_ordertype ordermap_surj vsubsetD)
    moreover have "ordermap A r x < ordermap A r y"
      using * r s by (metis (no_types) wf_Ord_ordermap OrdmemD (x, y)  r x  A small A ordermap_mono)
    ultimately show "(f x, f y)  s"
      using  s by (metis assms(7) f_inv_into_f inv_into_into less_asym ordermap_mono_less total_on_def)
  qed
next
  assume R: ?rhs
  then obtain f where f: "fA  B" "inj_on f A" "xA. yA. (x, y)  r  (f x, f y)  s"
    by blast
  show ?lhs
    by (rule ordertype_inc_le [where π=f]) (use f assms in auto)
qed

lemma iso_imp_ordertype_eq_ordertype:
  assumes iso: "iso r r' f"
    and "wf r"
    and "Total r"
    and sm: "small (Field r)"
  shows "ordertype (Field r) r = ordertype (Field r') r'"
  by (metis (no_types, lifting) iso_forward iso_wf assms iso_Field ordertype_inc_eq sm)

lemma ordertype_infinite_ge_ω:
  assumes "infinite A" "small A"
  shows "ordertype A VWF  ω"
proof -
  have "inj_on (ordermap A VWF) A"
    by (meson ordermap_bij small A bij_betw_def total_on_VWF wf_VWF)
  then have "infinite (ordermap A VWF ` A)"
    using infinite A finite_image_iff by blast
  then show ?thesis
    using Ord_ordertype small A infinite_Ord_omega by (auto simp: ordertype_def)
qed

lemma ordertype_eqI:
  assumes "wf r" "total_on A r" "small A" "wf s" 
          "bij_betw f A B" "(x  A. y  A. (f x, f y)  s  (x,y)  r)"
  shows "ordertype A r = ordertype B s"
  by (metis assms bij_betw_imp_surj_on ordertype_inc_eq)

lemma ordermap_eq_self:
  assumes "Ord α" and x: "x  elts α" 
  shows "ordermap (elts α) VWF x = x" 
  using Ord_in_Ord [OF assms] x 
proof (induction x rule: Ord_induct)
  case (step x)
  have 1: "{y  elts α. (y, x)  VWF} = elts x" (is "?A = _")
  proof
    show "?A  elts x"
      using Ord α by clarify (meson Ord_in_Ord Ord_mem_iff_lt VWF_iff_Ord_less step.hyps)
    show "elts x  ?A"
      using Ord α by clarify (meson Ord_in_Ord Ord_trans OrdmemD VWF_iff_Ord_less step.prems)
  qed
  show ?case
    using step
    by (simp add: ordermap [OF wf_VWF, of _ x] 1 Ord_trans [of _ _ α] step.prems Ord α cong: image_cong)
qed

lemma ordertype_eq_Ord [simp]:
  assumes "Ord α" 
  shows "ordertype (elts α) VWF = α"
  using assms ordermap_eq_self [OF assms] by (simp add: ordertype_def)


proposition ordertype_eq_iff:
  assumes α: "Ord α" and r: "wf r" and "small A" "total_on A r" "trans r"
  shows "ordertype A r = α 
         (f. bij_betw f A (elts α)  (x  A. y  A. f x < f y  (x,y)  r))"
    (is "?lhs = ?rhs")
proof safe
  assume eq: "α = ordertype A r"
  show "f. bij_betw f A (elts (ordertype A r))  (xA. yA. f x < f y  ((x, y)  r))"
  proof (intro exI conjI ballI)
    show "bij_betw (ordermap A r) A (elts (ordertype A r))"
      by (simp add: assms ordermap_bij)
    then show "ordermap A r x < ordermap A r y  (x, y)  r"
      if "x  A" "y  A" for x y
      using that assms
      by (metis order.asym ordermap_mono_less total_on_def)
  qed
next
  fix f 
  assume f: "bij_betw f A (elts α)" "xA. yA. f x < f y  (x, y)  r"
  have "ordertype A r = ordertype (elts α) VWF"
  proof (rule ordertype_eqI)
    show "xA. yA. ((f x, f y)  VWF) = ((x, y)  r)"
      by (meson Ord_in_Ord VWF_iff_Ord_less α bij_betwE f)
  qed (use assms f in auto)
  then show ?lhs
    by (simp add: α)
qed

corollary ordertype_VWF_eq_iff:
  assumes "Ord α" "small A"
  shows "ordertype A VWF = α 
         (f. bij_betw f A (elts α)  (x  A. y  A. f x < f y  (x,y)  VWF))"
  by (metis UNIV_I assms ordertype_eq_iff total_VWF total_on_def trans_VWF wf_VWF)


lemma ordertype_le_Ord:
  assumes "Ord α" "X  elts α"
  shows "ordertype X VWF  α"
  by (metis assms ordertype_VWF_mono ordertype_eq_Ord small_elts)

lemma ordertype_inc_le_Ord:
  assumes "small A" "Ord α"
    and π: "x y. xA; yA; (x,y)  r  π x < π y"
    and "wf r" "total_on A r" 
    and sub: "π ` A  elts α"
  shows "ordertype A r  α"
proof -
  have "x y. xA; yA; (x,y)  r  (π x, π y)  VWF"
    by (meson Ord_in_Ord VWF_iff_Ord_less π Ord α sub image_subset_iff)
  with assms show ?thesis
    by (metis ordertype_inc_eq ordertype_le_Ord wf_VWF)
qed

lemma le_ordertype_obtains_subset:
  assumes α: "β  α" "ordertype H VWF = α" and "small H" "Ord β"
  obtains G where "G  H" "ordertype G VWF = β" 
proof (intro exI conjI that)
  let ?f = "ordermap H VWF"
  show : "inv_into H ?f ` elts β  H"
    unfolding image_subset_iff
    by (metis α inv_into_into ordermap_surj subsetD vsubsetD)
  have "f. bij_betw f (inv_into H ?f ` elts β) (elts β)  (xinv_into H ?f ` elts β. yinv_into H ?f ` elts β. (f x < f y) = ((x, y)  VWF))"
  proof (intro exI conjI ballI iffI)
    show "bij_betw ?f (inv_into H ?f ` elts β) (elts β)"
      using ordermap_bij [OF wf_VWF total_on_VWF small H] α 
      by (metis bij_betw_inv_into_RIGHT bij_betw_subset less_eq_V_def )
  next
    fix x y
    assume x: "x  inv_into H ?f ` elts β"
        and y: "y  inv_into H ?f ` elts β"
    show "?f x < ?f y" if "(x,y)  VWF"
      using that  small H in_mono ordermap_mono_less x y by fastforce
    show "(x,y)  VWF" if "?f x < ?f y"
      using that  small H in_mono ordermap_mono_less [OF _ wf_VWF trans_VWF] x y
      by (metis UNIV_I less_imp_not_less total_VWF total_on_def)
  qed
  then show "ordertype (inv_into H ?f ` elts β) VWF = β"
    by (subst ordertype_eq_iff) (use assms in auto)
qed

lemma ordertype_infinite_ω:
  assumes "A  elts ω" "infinite A"
  shows "ordertype A VWF = ω"
proof (rule antisym)
  show "ordertype A VWF  ω"
    by (simp add: assms ordertype_le_Ord)
  show "ω  ordertype A VWF"
    using assms down ordertype_infinite_ge_ω by auto
qed

text ‹For infinite sets of natural numbers›
lemma ordertype_nat_ω:
  assumes "infinite N" shows "ordertype N less_than = ω"
proof -
  have "small N"
    by (meson inj_on_def ord_of_nat_inject small_def small_iff_range small_image_nat_V)
  have "ordertype (ord_of_nat ` N) VWF = ω"
    by (force simp: assms finite_image_iff inj_on_def intro: