Theory Cardinal_Relative

section‹Relative, Choice-less Cardinal Numbers›

theory Cardinal_Relative
  imports
    Lambda_Replacement
    Univ_Relative
begin

txt‹The following command avoids that a commonly used one-letter variable be
captured by the definition of the constructible universe termL.›
hide_const (open) L

txt‹We also return to the old notation for termsum to preserve the old
Constructibility code.›
no_notation oadd (infixl + 65)
notation sum (infixr + 65)

definition
  Finite_rel   :: "[io,i]=>o"  where
  "Finite_rel(M,A)  om[M]. n[M]. omega(M,om)  nom  eqpoll_rel(M,A,n)"

definition
  banach_functor :: "[i,i,i,i,i]  i" where
  "banach_functor(X,Y,f,g,W)  X - g``(Y - f``W)"

lemma banach_functor_subset: "banach_functor(X,Y,f,g,W)  X"
  unfolding banach_functor_def by auto

definition
  is_banach_functor :: "[io,i,i,i,i,i,i]o"  where
  "is_banach_functor(M,X,Y,f,g,W,b) 
      fW[M]. YfW[M]. gYfW[M]. image(M,f,W,fW)  setdiff(M,Y,fW,YfW) 
                                 image(M,g,YfW,gYfW)  setdiff(M,X,gYfW,b)"


lemma (in M_basic) banach_functor_abs :
  assumes "M(X)" "M(Y)" "M(f)" "M(g)"
  shows "relation1(M,is_banach_functor(M,X,Y,f,g),banach_functor(X,Y,f,g))"
  unfolding relation1_def is_banach_functor_def banach_functor_def
  using assms
  by simp

lemma (in M_basic) banach_functor_closed:
  assumes "M(X)" "M(Y)" "M(f)" "M(g)"
  shows "W[M]. M(banach_functor(X,Y,f,g,W))"
  unfolding banach_functor_def using assms image_closed
  by simp

context M_trancl
begin

lemma iterates_banach_functor_closed:
  assumes "nω" "M(X)" "M(Y)" "M(f)" "M(g)"
  shows "M(banach_functor(X,Y,f,g)^n(0))"
  using assms banach_functor_closed
  by (induct) simp_all

lemma banach_repl_iter':
  assumes
    "A. M(A)  separation(M, λb. xA. x  ω  b = banach_functor(X, Y, f, g)^x (0))"
    "M(X)" "M(Y)" "M(f)" "M(g)"
  shows
    "strong_replacement(M, λx y. xnat  y = banach_functor(X, Y, f, g)^x (0))"
  unfolding strong_replacement_def
proof clarsimp
  fix A
  let ?Z="{b  Pow⇗M⇖(X) . (xA. x  ω  b = banach_functor(X, Y, f, g)^x (0))}"
  assume "M(A)"
  moreover
  note assms
  moreover from calculation
  have "M(?Z)" by simp
  moreover from assms(2-)
  have "b  ?Z  (xA. x  ω  b = banach_functor(X, Y, f, g)^x (0))" for b
    by (auto, rename_tac x, induct_tac x, (auto simp:def_Pow_rel)[1],
        rule_tac def_Pow_rel[THEN iffD2, OF iterates_banach_functor_closed[of _ X Y f g]])
          (simp_all add:banach_functor_subset)
  ultimately
  show "Z[M]. b[M]. b  Z  (xA. x  ω  b = banach_functor(X, Y, f, g)^x (0))"
    by (intro rexI[of _ ?Z]) simp
qed

end ― ‹localeM_trancl

context M_Perm
begin

lemma mem_Pow_rel: "M(r)  a  Pow_rel(M,r)  a  Pow(r)  M(a)"
  using Pow_rel_char by simp

lemma mem_bij_abs: "M(f);M(A);M(B)   f  bij⇗M⇖(A,B)  fbij(A,B)"
  using bij_rel_char by simp

lemma mem_inj_abs: "M(f);M(A);M(B)   f  inj⇗M⇖(A,B)  finj(A,B)"
  using inj_rel_char by simp

lemma mem_surj_abs: "M(f);M(A);M(B)   f  surj⇗M⇖(A,B)  fsurj(A,B)"
  using surj_rel_char by simp

end ― ‹localeM_Perm

locale M_cardinals = M_ordertype + M_trancl + M_Perm + M_replacement +
  assumes
    radd_separation: "M(R)  M(S) 
    separation(M, λz.
      (x y. z = Inl(x), Inr(y)) 
         (x' x. z = Inl(x'), Inl(x)  x', x  R) 
         (y' y. z = Inr(y'), Inr(y)  y', y  S))"
    and
    rmult_separation: "M(b)  M(d)  separation(M,
    λz. x' y' x y. z = x', y', x, y  (x', x  b  x' = x  y', y  d))"

begin

lemma rvimage_separation: "M(f)  M(r) 
    separation(M, λz. x y. z = x, y  f ` x, f ` y  r)"
  using separation_Pair separation_in lam_replacement_product
    lam_replacement_fst lam_replacement_snd lam_replacement_constant
    lam_replacement_apply2[THEN [5] lam_replacement_hcomp2]
  by simp

lemma radd_closed[intro,simp]: "M(a)  M(b)  M(c)  M(d)  M(radd(a,b,c,d))"
  using radd_separation by (auto simp add: radd_def)

lemma rmult_closed[intro,simp]: "M(a)  M(b)  M(c)  M(d)  M(rmult(a,b,c,d))"
  using rmult_separation by (auto simp add: rmult_def)

end ― ‹localeM_cardinals

lemma (in M_cardinals) is_cardinal_iff_Least:
  assumes "M(A)" "M(κ)"
  shows "is_cardinal(M,A,κ)  κ = (μ i. M(i)  i ≈⇗MA)"
  using is_cardinal_iff assms
  unfolding cardinal_rel_def by simp

subsection‹The Schroeder-Bernstein Theorem›
text‹See Davey and Priestly, page 106›

context M_cardinals
begin

subsection‹Banach's Decomposition Theorem›

lemma bnd_mono_banach_functor: "bnd_mono(X, banach_functor(X,Y,f,g))"
  unfolding bnd_mono_def banach_functor_def
  by blast

lemma inj_Inter:
  assumes "g  inj(Y,X)" "A0" "aA. a  Y"
  shows "g``(A) = (aA. g``a)"
proof (intro equalityI subsetI)
  fix x
  from assms
  obtain a where "aA" by blast
  moreover
  assume "x  (aA. g `` a)"
  ultimately
  have x_in_im: "x  g``y" if "yA" for y
    using that by auto
  have exists: "z  y. x = g`z" if "yA" for y
  proof -
    note that
    moreover from this and x_in_im
    have "x  g``y" by simp
    moreover from calculation
    have "x  g``y" by simp
    moreover
    note assms
    ultimately
    show ?thesis
      using image_fun[OF inj_is_fun] by auto
  qed
  with aA
  obtain z where "z  a" "x = g`z" by auto
  moreover
  have "z  y" if "yA" for y
  proof -
    from that and exists
    obtain w where "w  y" "x = g`w" by auto
    moreover from this x = g`z assms that aA za
    have "z = w" unfolding inj_def by blast
    ultimately
    show ?thesis by simp
  qed
  moreover
  note assms
  moreover from calculation
  have "z  A" by auto
  moreover from calculation
  have "z  Y" by blast
  ultimately
  show "x  g `` (A)"
    using inj_is_fun[THEN funcI, of g] by fast
qed auto

lemma contin_banach_functor:
  assumes "g  inj(Y,X)"
  shows "contin(banach_functor(X,Y,f,g))"
  unfolding contin_def
proof (intro allI impI)
  fix A
  assume "directed(A)"
  then
  have "A  0"
    unfolding directed_def ..
  have "banach_functor(X, Y, f, g, A) = X - g``(Y - f``(A))"
    unfolding banach_functor_def ..
  also
  have "  = X - g``(Y - (aA. f``a))"
    by auto
  also from A0
  have "  = X - g``(aA. Y-f``a)"
    by auto
  also from A0 and assms
  have "  = X - (aA. g``(Y-f``a))"
    using inj_Inter[of g Y X "{Y-f``a. aA}" ] by fastforce
  also from A0
  have "  = (aA. X - g``(Y-f``a))" by simp
  also
  have "  = (aA. banach_functor(X, Y, f, g, a))"
    unfolding banach_functor_def ..
  finally
  show "banach_functor(X,Y,f,g,A) = (aA. banach_functor(X,Y,f,g,a))" .
qed

lemma lfp_banach_functor:
  assumes "ginj(Y,X)"
  shows "lfp(X, banach_functor(X,Y,f,g)) =
       (nnat. banach_functor(X,Y,f,g)^n (0))"
  using assms lfp_eq_Union bnd_mono_banach_functor contin_banach_functor
  by simp

lemma lfp_banach_functor_closed:
  assumes "M(g)" "M(X)" "M(Y)" "M(f)" "ginj(Y,X)"
    and banach_repl_iter: "M(X)  M(Y)  M(f)  M(g) 
               strong_replacement(M, λx y. xnat  y = banach_functor(X, Y, f, g)^x (0))"
  shows "M(lfp(X, banach_functor(X,Y,f,g)))"
proof -
  from assms
  have "M(banach_functor(X,Y,f,g)^n (0))" if "nnat" for n
    by(rule_tac nat_induct[OF that],simp_all add:banach_functor_closed)
  with assms
  show ?thesis
    using family_union_closed'[OF banach_repl_iter M_nat] lfp_banach_functor
    by simp
qed

lemma banach_decomposition_rel:
  assumes
    banach_repl_iter: "M(f)  M(g)  M(X)  M(Y) 
               strong_replacement(M, λx y. xnat  y = banach_functor(X, Y, f, g)^x (0))"
  shows
    "[| M(f); M(g); M(X); M(Y); f  X->Y;  g  inj(Y,X) |] ==>
      XA[M]. XB[M]. YA[M]. YB[M].
         (XA  XB = 0) & (XA  XB = X) &
         (YA  YB = 0) & (YA  YB = Y) &
         f``XA=YA & g``YB=XB"
  apply (intro rexI conjI)
           apply (rule_tac [6] Banach_last_equation)
           apply (rule_tac [5] refl)
          apply (assumption |
      rule inj_is_fun Diff_disjoint Diff_partition fun_is_rel
      image_subset lfp_subset)+
  using lfp_banach_functor_closed[of g X Y f] assms
  unfolding banach_functor_def by simp_all

lemma schroeder_bernstein_closed:
  assumes
    banach_repl_iter: "M(X)  M(Y)  M(f)  M(g) 
               strong_replacement(M, λx y. xnat  y = banach_functor(X, Y, f, g)^x (0))"
  shows
  "[| M(f); M(g); M(X); M(Y); f  inj(X,Y);  g  inj(Y,X) |] ==> h[M]. h  bij(X,Y)"
  apply (insert banach_decomposition_rel [of f g X Y, OF banach_repl_iter])
  apply (simp add: inj_is_fun)
  apply (auto)
  apply (rule_tac x="restrict(f,XA)  converse(restrict(g,YB))" in rexI)
   apply (auto intro!: restrict_bij bij_disjoint_Un intro: bij_converse_bij)
  done

text‹The previous lemmas finish our original, direct relativization
of the material involving the iterative proof (as appearing in theoryZF.Cardinal)
of the Schröder-Bernstein theorem. Next, we formalize 
Zermelo's proof that replaces the recursive construction by a fixed point
represented as an intersection cite‹Exr. x4.27› in "moschovakis1994notes". This allows
to avoid at least one replacement assumption.›

lemma dedekind_zermelo:
  assumes
    "A'  B" "B  A" "A ≈⇗MA'"
    and types: "M(A')" "M(B)" "M(A)"
  shows
    "A ≈⇗MB"
proof -
  from A ≈⇗MA' and types
  obtain f where "f  bij⇗M⇖(A,A')"
    unfolding eqpoll_rel_def by blast
  let ?Q="B - f``A"
  from f  _ A'  B types
  have "f``X  B" for X
    using mem_bij_rel[THEN bij_is_fun, THEN Image_sub_codomain, of f A A'] by auto
  moreover
  note B  A
  moreover from calculation
  have "f``X  A" for X by auto
  moreover
  define 𝒯 where "𝒯   { X  Pow⇗M⇖(A) . ?Q  f `` X  X}"
  moreover from calculation
  have "A  𝒯" using def_Pow_rel by (auto simp:types)
  ultimately
  have "𝒯  0" unfolding 𝒯_def by auto
  let ?T="𝒯"
  have "?T  A"
  proof
    fix x
    assume "x  ?T"
    with 𝒯  0
    obtain X where "x  X" "X  𝒯"
      by blast
    moreover from this
    have "X  Pow⇗M⇖(A)"
      unfolding 𝒯_def by simp
    moreover from calculation and M(A)
    have "M(x)" using Pow_rel_char by (auto dest:transM)
    ultimately
    show "x  A" using Pow_rel_char by (auto simp:types)
  qed
  moreover from 𝒯  0
  have "?Q  f``?T  ?T"
    using image_mono unfolding 𝒯_def by blast
  moreover from f  _
  have "M(𝒯)"
    using zermelo_separation unfolding 𝒯_def by (auto simp:types dest:transM)
  moreover from this
  have "M(?T)" by simp
  moreover
  note 𝒯  0
  ultimately
  have "?T  𝒯"
    unfolding 𝒯_def using def_Pow_rel
    by (auto simp:types)
  have "?T  ?Q  f``?T"
  proof (intro subsetI, rule ccontr)
    fix x
    from _  f ``?T  ?T
    have "f `` (?T - {x})  ?T" "f `` (?T - {x})  f`` ?T" by auto
    assume "x  ?T" "x  ?Q  f``?T"
    then
    have "?T - {x}  𝒯"
    proof -
      note f `` (?T - {x})  ?T
      moreover from this and x  _  f``?T
      have "x  f `` ?T" by simp
      ultimately
      have "f `` (?T - {x})  ?T - {x}" by auto
      moreover from x  ?Q  _ ?Q  _  ?T
      have "?Q  ?T - {x}" by auto
      moreover
      note ?T  _ x  ?T M(?T) ?T  _
      ultimately
      show ?thesis
        using def_Pow_rel[of "?T - {x}" A] transM[of _ ?T]
        unfolding 𝒯_def
        by (auto simp:types)
    qed
    moreover
    note f `` (?T - {x})  f`` ?T
    ultimately
    have "?T  ?T - {x}" by auto
    with x  ?T
    show False by auto
  qed
  with ?Q  f``?T  ?T
  have "?T = ?Q  f``?T" by auto
  from X. f``X  B
  have "(?Q  f``?T)  (f``A - f``?T)  B" by auto
  with ?T = _
  have "?T  (f``A - f``?T)  B" by simp
  with 𝒯  0 ?T = _
  have "B = ?T  (f``A - f``?T)"
  proof (intro equalityI, intro subsetI)
    fix x
    assume "x  B"
    with 𝒯  0 ?T = _
    show "x  ?T  (f``A - f``?T)"
      by (subst ?T = _, clarify)
  qed
  moreover from ?T  A
  have "A = ?T  (A - ?T)" by auto
  moreover from M(?T) f  _
  have "M(id(?T)  restrict(f,A-?T))"
    using bij_rel_closed[THEN [2] transM] id_closed by (auto simp:types)
  moreover from ?T = _ f  _
  have "f``A - f``?T = f``(A - ?T)"
    using bij_rel_char bij_is_inj[THEN inj_range_Diff, of f A]
    by (auto simp:types)
  from f  _ types
  have "id(?T)  restrict(f, A-?T)  bij(?T  (A - ?T),?T  (f``A - f``?T))"
    using id_bij mem_bij_rel[of _ A A', THEN bij_is_inj]
    by (rule_tac bij_disjoint_Un; clarsimp)
      (subst f``A - f``?T =_, auto intro:restrict_bij, subst ?T = _, auto)
  moreover
  note types
  ultimately
  show ?thesis
    using bij_rel_char unfolding eqpoll_rel_def by fastforce
qed

lemma schroeder_bernstein_closed':
  assumes "f  inj⇗M⇖(A,C)" " g  inj⇗M⇖(C,A)"
    and types:"M(A)" "M(C)"
  shows "A ≈⇗MC"
proof -
  from assms
  have "f  inj(A,C)" " g  inj(C,A)" "M(f)" "M(g)"
    using inj_rel_char by auto
  moreover from this
  have "g  bij(C,range(g))" "g O f  bij(A,range(g O f))"
    using inj_bij_range comp_inj by auto blast
  moreover from calculation
  have "range(g O f)  range(g)" "range(g)  A"
    using inj_is_fun[THEN range_fun_subset_codomain] by auto
  moreover from calculation
  obtain h where "h  bij⇗M⇖(A, range(g))"
    using dedekind_zermelo[of "range(g O f)" "range(g)" A]
      bij_rel_char def_eqpoll_rel
    by (auto simp:types)
  ultimately
  show ?thesis
    using bij_rel_char def_eqpoll_rel comp_bij[of h A "range(g)" "converse(g)" C]
      bij_converse_bij[of g C "range(g)"] by (auto simp:types)
qed

text‹Relative equipollence is an equivalence relation›

declare mem_bij_abs[simp] mem_inj_abs[simp]

lemma bij_imp_eqpoll_rel:
  assumes "f  bij(A,B)" "M(f)" "M(A)" "M(B)"
  shows "A ≈⇗MB"
  using assms by (auto simp add:def_eqpoll_rel)

lemma eqpoll_rel_refl: "M(A)  A ≈⇗MA"
  using bij_imp_eqpoll_rel[OF id_bij, OF id_closed] .

lemma eqpoll_rel_sym: "X ≈⇗MY  M(X)  M(Y)   Y ≈⇗MX"
  unfolding def_eqpoll_rel using converse_closed
  by (auto intro: bij_converse_bij)

lemma eqpoll_rel_trans [trans]:
  "[|X ≈⇗MY;  Y ≈⇗MZ;  M(X); M(Y) ; M(Z) |] ==> X ≈⇗MZ"
  unfolding def_eqpoll_rel by (auto intro: comp_bij)

text‹Relative le-pollence is a preorder›

lemma subset_imp_lepoll_rel: "X  Y  M(X)  M(Y)  X ≲⇗MY"
  unfolding def_lepoll_rel using id_subset_inj id_closed
  by simp blast

lemmas lepoll_rel_refl = subset_refl [THEN subset_imp_lepoll_rel, simp]

lemmas le_imp_lepoll_rel = le_imp_subset [THEN subset_imp_lepoll_rel]

lemma eqpoll_rel_imp_lepoll_rel: "X ≈⇗MY ==> M(X)  M(Y)  X ≲⇗MY"
  unfolding def_eqpoll_rel bij_def def_lepoll_rel using bij_is_inj
  by (auto)

lemma lepoll_rel_trans [trans]:
  assumes
    "X ≲⇗MY" "Y ≲⇗MZ" "M(X)" "M(Y)" "M(Z)"
  shows
    "X ≲⇗MZ"
  using assms def_lepoll_rel
  by (auto intro: comp_inj)

lemma eq_lepoll_rel_trans [trans]:
  assumes
    "X ≈⇗MY"  "Y ≲⇗MZ" "M(X)" "M(Y)" "M(Z)"
  shows
    "X ≲⇗MZ"
  using assms
  by (blast intro: eqpoll_rel_imp_lepoll_rel lepoll_rel_trans)

lemma lepoll_rel_eq_trans [trans]:
  assumes "X ≲⇗MY"  "Y ≈⇗MZ" "M(X)" "M(Y)" "M(Z)"
  shows "X ≲⇗MZ"
  using assms
    eqpoll_rel_imp_lepoll_rel[of Y Z] lepoll_rel_trans[of X Y Z]
  by simp

lemma eqpoll_relI: " X ≲⇗MY; Y ≲⇗MX; M(X) ; M(Y)   X ≈⇗MY"
  unfolding def_lepoll_rel using schroeder_bernstein_closed'
  by (auto simp del:mem_inj_abs)

lemma eqpoll_relE:
  "[| X ≈⇗MY; [| X ≲⇗MY; Y ≲⇗MX |] ==> P ;  M(X) ; M(Y) |] ==> P"
  by (blast intro: eqpoll_rel_imp_lepoll_rel eqpoll_rel_sym)

lemma eqpoll_rel_iff: "M(X)  M(Y)  X ≈⇗MY  X ≲⇗MY & Y ≲⇗MX"
  by (blast intro: eqpoll_relI elim: eqpoll_relE)

lemma lepoll_rel_0_is_0: "A ≲⇗M0  M(A)  A = 0"
  using def_lepoll_rel
  by (cases "A=0") (auto simp add: inj_def)

― ‹termM(Y)  0 ≲⇗MY
lemmas empty_lepoll_relI = empty_subsetI [THEN subset_imp_lepoll_rel, OF nonempty]

lemma lepoll_rel_0_iff: "M(A)  A ≲⇗M0  A=0"
  by (blast intro: lepoll_rel_0_is_0 lepoll_rel_refl)

lemma Un_lepoll_rel_Un:
  "[| A ≲⇗MB; C ≲⇗MD; B  D = 0; M(A); M(B); M(C); M(D) |] ==> A  C ≲⇗MB  D"
  using def_lepoll_rel using inj_disjoint_Un[of _ A B _ C D] if_then_replacement
  apply (auto)
  apply (rule, assumption)
  apply (auto intro!:lam_closed elim:transM)+
  done

lemma eqpoll_rel_0_is_0: "A ≈⇗M0  M(A)  A = 0"
  using eqpoll_rel_imp_lepoll_rel lepoll_rel_0_is_0 nonempty
  by blast

lemma eqpoll_rel_0_iff: "M(A)  A ≈⇗M0  A=0"
  by (blast intro: eqpoll_rel_0_is_0 eqpoll_rel_refl)

lemma eqpoll_rel_disjoint_Un:
  "[| A ≈⇗MB;  C ≈⇗MD;  A  C = 0;  B  D = 0; M(A); M(B); M(C) ; M(D) |]
     ==> A  C ≈⇗MB  D"
  by (auto intro: bij_disjoint_Un simp add:def_eqpoll_rel)

subsection‹lesspoll: contributions by Krzysztof Grabczewski›

lemma lesspoll_rel_not_refl: "M(i)  ~ (i ≺⇗Mi)"
  by (simp add: lesspoll_rel_def eqpoll_rel_refl)

lemma lesspoll_rel_irrefl: "i ≺⇗Mi ==> M(i)  P"
  by (simp add: lesspoll_rel_def eqpoll_rel_refl)

lemma lesspoll_rel_imp_lepoll_rel: "A ≺⇗MB; M(A); M(B) A ≲⇗MB"
  by (unfold lesspoll_rel_def, blast)

lemma rvimage_closed [intro,simp]:
  assumes
    "M(A)" "M(f)" "M(r)"
  shows
    "M(rvimage(A,f,r))"
  unfolding rvimage_def using assms rvimage_separation by auto

lemma lepoll_rel_well_ord: "[| A ≲⇗MB; well_ord(B,r); M(A); M(B); M(r) |] ==> s[M]. well_ord(A,s)"
  unfolding def_lepoll_rel by (auto intro:well_ord_rvimage)

lemma lepoll_rel_iff_leqpoll_rel: "M(A); M(B)  A ≲⇗MB  A ≺⇗MB | A ≈⇗MB"
  apply (unfold lesspoll_rel_def)
  apply (blast intro: eqpoll_relI elim: eqpoll_relE)
  done

end ― ‹localeM_cardinals

context M_cardinals
begin

lemma inj_rel_is_fun_M: "f  inj⇗M⇖(A,B)  M(f)  M(A)  M(B)  f  A →⇗MB"
  using inj_is_fun function_space_rel_char by simp

― ‹In porting the following theorem, I tried to follow the Discipline
strictly, though finally only an approach maximizing the use of
absoluteness results (@{thm [source] function_space_rel_char inj_rel_char}) was
 the one paying dividends.›
lemma inj_rel_not_surj_rel_succ:
  notes mem_inj_abs[simp del]
  assumes fi: "f  inj⇗M⇖(A, succ(m))" and fns: "f  surj⇗M⇖(A, succ(m))"
    and types: "M(f)" "M(A)" "M(m)"
  shows "f[M]. f  inj⇗M⇖(A,m)"
proof -
  from fi [THEN inj_rel_is_fun_M] fns types
  obtain y where y: "y  succ(m)" "x. xA  f ` x  y" "M(y)"
    by (auto simp add: def_surj_rel)
  show ?thesis
  proof
    from types and M(y)
    show "M(λzA. if f ` z = m then y else f ` z)"
      using transM[OF _ M(A)] lam_if_then_apply_replacement2 lam_replacement_iff_lam_closed
      by (auto)
    with types y fi
    have "(λzA. if f`z = m then y else f`z)  A→⇗Mm"
      using function_space_rel_char inj_rel_char inj_is_fun[of f A "succ(m)"]
      by (auto intro!: if_type [THEN lam_type] dest: apply_funtype)
    with types y fi
    show "(λzA. if f`z = m then y else f`z)  inj⇗M⇖(A, m)"
      by (simp add: def_inj_rel) blast
  qed
qed

― ‹Variations on transitivity›

lemma lesspoll_rel_trans [trans]:
  "[| X ≺⇗MY; Y ≺⇗MZ; M(X); M(Y) ; M(Z) |] ==> X ≺⇗MZ"
  apply (unfold lesspoll_rel_def)
  apply (blast elim: eqpoll_relE intro: eqpoll_relI lepoll_rel_trans)
  done

lemma lesspoll_rel_trans1 [trans]:
  "[| X ≲⇗MY; Y ≺⇗MZ; M(X); M(Y) ; M(Z) |] ==> X ≺⇗MZ"
  apply (unfold lesspoll_rel_def)
  apply (blast elim: eqpoll_relE intro: eqpoll_relI lepoll_rel_trans)
  done

lemma lesspoll_rel_trans2 [trans]:
  "[|  X ≺⇗MY; Y ≲⇗MZ; M(X); M(Y) ; M(Z)|] ==> X ≺⇗MZ"
  apply (unfold lesspoll_rel_def)
  apply (blast elim: eqpoll_relE intro: eqpoll_relI lepoll_rel_trans)
  done

lemma eq_lesspoll_rel_trans [trans]:
  "[| X ≈⇗MY; Y ≺⇗MZ; M(X); M(Y) ; M(Z) |] ==> X ≺⇗MZ"
  by (blast intro: eqpoll_rel_imp_lepoll_rel lesspoll_rel_trans1)

lemma lesspoll_rel_eq_trans [trans]:
  "[| X ≺⇗MY; Y ≈⇗MZ; M(X); M(Y) ; M(Z) |] ==> X ≺⇗MZ"
  by (blast intro: eqpoll_rel_imp_lepoll_rel lesspoll_rel_trans2)

lemma is_cardinal_cong:
  assumes "X ≈⇗MY" "M(X)" "M(Y)"
  shows "κ[M]. is_cardinal(M,X,κ)  is_cardinal(M,Y,κ)"
proof -
  from assms
  have "(μ i. M(i)  i ≈⇗MX) = (μ i. M(i)  i ≈⇗MY)"
    by (intro Least_cong) (auto intro: comp_bij bij_converse_bij simp add:def_eqpoll_rel)
  moreover from assms
  have "M(μ i. M(i)  i ≈⇗MX)"
    using Least_closed' by fastforce
  moreover
  note assms
  ultimately
  show ?thesis
    using is_cardinal_iff_Least
    by auto
qed

― ‹ported from Cardinal›
lemma cardinal_rel_cong: "X ≈⇗MY  M(X)  M(Y)  |X|⇗M= |Y|⇗M⇖"
  apply (simp add: def_eqpoll_rel cardinal_rel_def)
  apply (rule Least_cong)
  apply (auto intro: comp_bij bij_converse_bij)
  done

lemma well_ord_is_cardinal_eqpoll_rel:
  assumes "well_ord(A,r)" shows "is_cardinal(M,A,κ)  M(A)  M(κ)  M(r)  κ ≈⇗MA"
proof (subst is_cardinal_iff_Least[THEN iffD1, of A κ])
  assume "M(A)" "M(κ)" "M(r)" "is_cardinal(M,A,κ)"
  moreover from assms and calculation
  obtain f i where "M(f)" "Ord(i)" "M(i)" "f  bij(A,i)"
    using ordertype_exists[of A r] ord_iso_is_bij by auto
  moreover
  have "M(μ i. M(i)  i ≈⇗MA)"
    using Least_closed' by fastforce
  ultimately
  show "(μ i. M(i)  i ≈⇗MA) ≈⇗MA"
    using assms[THEN well_ord_imp_relativized]
      LeastI[of "λi. M(i)  i ≈⇗MA" i] Ord_ordertype[OF assms]
      bij_converse_bij[THEN bij_imp_eqpoll_rel, of f] by simp
qed

lemmas Ord_is_cardinal_eqpoll_rel = well_ord_Memrel[THEN well_ord_is_cardinal_eqpoll_rel]

section‹Porting from theoryZF.Cardinal

txt‹The following results were ported more or less directly from theoryZF.Cardinal

― ‹This result relies on various closure properties and
   thus cannot be translated directly›
lemma well_ord_cardinal_rel_eqpoll_rel:
  assumes r: "well_ord(A,r)" and "M(A)" "M(r)" shows "|A|⇗M⇖ ≈⇗MA"
  using assms well_ord_is_cardinal_eqpoll_rel is_cardinal_iff
  by blast

lemmas Ord_cardinal_rel_eqpoll_rel = well_ord_Memrel[THEN well_ord_cardinal_rel_eqpoll_rel]

lemma Ord_cardinal_rel_idem: "Ord(A)  M(A)  ||A|⇗M⇖|⇗M= |A|⇗M⇖"
  by (rule_tac Ord_cardinal_rel_eqpoll_rel [THEN cardinal_rel_cong]) auto

lemma well_ord_cardinal_rel_eqE:
  assumes woX: "well_ord(X,r)" and woY: "well_ord(Y,s)" and eq: "|X|⇗M= |Y|⇗M⇖"
    and types: "M(X)" "M(r)" "M(Y)" "M(s)"
  shows "X ≈⇗MY"
proof -
  from types
  have "X ≈⇗M|X|⇗M⇖" by (blast intro: well_ord_cardinal_rel_eqpoll_rel [OF woX] eqpoll_rel_sym)
  also
  have "... = |Y|⇗M⇖" by (rule eq)
  also from types
  have "... ≈⇗MY" by (rule_tac well_ord_cardinal_rel_eqpoll_rel [OF woY])
  finally show ?thesis  by (simp add:types)
qed

lemma well_ord_cardinal_rel_eqpoll_rel_iff:
  "[| well_ord(X,r);  well_ord(Y,s); M(X); M(r); M(Y); M(s) |] ==> |X|⇗M= |Y|⇗M X ≈⇗MY"
  by (blast intro: cardinal_rel_cong well_ord_cardinal_rel_eqE)

lemma Ord_cardinal_rel_le: "Ord(i)  M(i) ==> |i|⇗M i"
  unfolding cardinal_rel_def
  using eqpoll_rel_refl Least_le by simp

lemma Card_rel_cardinal_rel_eq: "Card⇗M⇖(K) ==> M(K)  |K|⇗M= K"
  apply (unfold Card_rel_def)
  apply (erule sym)
  done

lemma Card_relI: "[| Ord(i);  !!j. j<i  M(j) ==> ~(j ≈⇗Mi); M(i) |] ==> Card⇗M⇖(i)"
  apply (unfold Card_rel_def cardinal_rel_def)
  apply (subst Least_equality)
     apply (blast intro: eqpoll_rel_refl)+
  done

lemma Card_rel_is_Ord: "Card⇗M⇖(i) ==> M(i)  Ord(i)"
  apply (unfold Card_rel_def cardinal_rel_def)
  apply (erule ssubst)
  apply (rule Ord_Least)
  done

lemma Card_rel_cardinal_rel_le: "Card⇗M⇖(K) ==> M(K)  K  |K|⇗M⇖"
  apply (simp (no_asm_simp) add: Card_rel_is_Ord Card_rel_cardinal_rel_eq)
  done

lemma Ord_cardinal_rel [simp,intro!]: "M(A)  Ord(|A|⇗M)"
  apply (unfold cardinal_rel_def)
  apply (rule Ord_Least)
  done

lemma Card_rel_iff_initial: assumes types:"M(K)"
  shows "Card⇗M⇖(K)  Ord(K) & (j[M]. j<K  ~ (j ≈⇗MK))"
proof -
  { fix j
    assume K: "Card⇗M⇖(K)" "M(j)  j ≈⇗MK"
    assume "j < K"
    also have "... = (μ i. M(i)  i ≈⇗MK)" using K
      by (simp add: Card_rel_def cardinal_rel_def types)
    finally have "j < (μ i. M(i)  i ≈⇗MK)" .
    then have "False" using K
      by (best intro: less_LeastE[of "λj. M(j)  j ≈⇗MK"])
  }
  with types
  show ?thesis
    by (blast intro: Card_relI Card_rel_is_Ord)
qed

lemma lt_Card_rel_imp_lesspoll_rel: "[| Card⇗M⇖(a); i<a; M(a); M(i) |] ==> i ≺⇗Ma"
  apply (unfold lesspoll_rel_def)
  apply (frule Card_rel_iff_initial [THEN iffD1], assumption)
  apply (blast intro!: leI [THEN le_imp_lepoll_rel])
  done

lemma Card_rel_0: "Card⇗M⇖(0)"
  apply (rule Ord_0 [THEN Card_relI])
   apply (auto elim!: ltE)
  done

lemma Card_rel_Un: "[| Card⇗M⇖(K);  Card⇗M⇖(L); M(K); M(L) |] ==> Card⇗M⇖(K  L)"
  apply (rule Ord_linear_le [of K L])
     apply (simp_all add: subset_Un_iff [THEN iffD1]  Card_rel_is_Ord le_imp_subset
      subset_Un_iff2 [THEN iffD1])
  done

lemma Card_rel_cardinal_rel [iff]: assumes types:"M(A)" shows "Card⇗M⇖(|A|⇗M)"
  using assms
proof (unfold cardinal_rel_def)
  show "Card⇗M⇖(μ i. M(i)  i ≈⇗MA)"
  proof (cases "i[M]. Ord (i)  i ≈⇗MA")
    case False thus ?thesis           ― ‹degenerate case›
      using Least_0[of "λi. M(i)  i ≈⇗MA"] Card_rel_0
      by fastforce
  next
    case True                         ― ‹real case: termA is isomorphic to some ordinal›
    then obtain i where i: "Ord(i)" "i ≈⇗MA" "M(i)" by blast
    show ?thesis
    proof (rule Card_relI [OF Ord_Least], rule notI)
      fix j
      assume j: "j < (μ i. M(i)  i ≈⇗MA)" and "M(j)"
      assume "j ≈⇗M(μ i. M(i)  i ≈⇗MA)"
      also have "... ≈⇗MA" using i LeastI[of "λi. M(i)  i ≈⇗MA"] by (auto)
      finally have "j ≈⇗MA"
        using Least_closed'[of "λi. M(i)  i ≈⇗MA"] by (simp add: M(j) types)
      thus False
        using M(j) by (blast intro:less_LeastE [OF _ j])
    qed (auto intro:Least_closed)
  qed
qed

lemma cardinal_rel_eq_lemma:
  assumes i:"|i|⇗M j" and j: "j  i" and types: "M(i)" "M(j)"
  shows "|j|⇗M= |i|⇗M⇖"
proof (rule eqpoll_relI [THEN cardinal_rel_cong])
  show "j ≲⇗Mi" by (rule le_imp_lepoll_rel [OF j]) (simp_all add:types)
next
  have Oi: "Ord(i)" using j by (rule le_Ord2)
  with types
  have "i ≈⇗M|i|⇗M⇖"
    by (blast intro: Ord_cardinal_rel_eqpoll_rel eqpoll_rel_sym)
  also from types
  have "... ≲⇗Mj"
    by (blast intro: le_imp_lepoll_rel i)
  finally show "i ≲⇗Mj" by (simp_all add:types)
qed (simp_all add:types)

lemma cardinal_rel_mono:
  assumes ij: "i  j" and types:"M(i)" "M(j)" shows "|i|⇗M |j|⇗M⇖"
  using Ord_cardinal_rel [OF M(i)] Ord_cardinal_rel [OF M(j)]
proof (cases rule: Ord_linear_le)
  case le then show ?thesis .
next
  case ge
  have i: "Ord(i)" using ij
    by (simp add: lt_Ord)
  have ci: "|i|⇗M j"
    by (blast intro: Ord_cardinal_rel_le ij le_trans i types)
  have "|i|⇗M= ||i|⇗M⇖|⇗M⇖"
    by (auto simp add: Ord_cardinal_rel_idem i types)
  also have "... = |j|⇗M⇖"
    by (rule cardinal_rel_eq_lemma [OF ge ci]) (simp_all add:types)
  finally have "|i|⇗M= |j|⇗M⇖" .
  thus ?thesis by (simp add:types)
qed

lemma cardinal_rel_lt_imp_lt: "[| |i|⇗M< |j|⇗M;  Ord(i);  Ord(j); M(i); M(j) |] ==> i < j"
  apply (rule Ord_linear2 [of i j], assumption+)
  apply (erule lt_trans2 [THEN lt_irrefl])
  apply (erule cardinal_rel_mono, assumption+)
  done

lemma Card_rel_lt_imp_lt: "[| |i|⇗M< K;  Ord(i);  Card⇗M⇖(K); M(i); M(K)|] ==> i < K"
  by (simp (no_asm_simp) add: cardinal_rel_lt_imp_lt Card_rel_is_Ord Card_rel_cardinal_rel_eq)

lemma Card_rel_lt_iff: "[| Ord(i);  Card⇗M⇖(K); M(i); M(K) |] ==> (|i|⇗M< K)  (i < K)"
  by (blast intro: Card_rel_lt_imp_lt Ord_cardinal_rel_le [THEN lt_trans1])

lemma Card_rel_le_iff: "[| Ord(i);  Card⇗M⇖(K); M(i); M(K) |] ==> (K  |i|⇗M)  (K  i)"
  by (simp add: Card_rel_lt_iff Card_rel_is_Ord not_lt_iff_le [THEN iff_sym])

lemma well_ord_lepoll_rel_imp_cardinal_rel_le:
  assumes wB: "well_ord(B,r)" and AB: "A ≲⇗MB"
    and
    types: "M(B)" "M(r)" "M(A)"
  shows "|A|⇗M |B|⇗M⇖"
  using Ord_cardinal_rel [OF M(A)] Ord_cardinal_rel [OF M(B)]
proof (cases rule: Ord_linear_le)
  case le thus ?thesis .
next
  case ge
  from lepoll_rel_well_ord [OF AB wB]
  obtain s where s: "well_ord(A, s)" "M(s)" by (blast intro:types)
  have "B ≈⇗M|B|⇗M⇖" by (blast intro: wB eqpoll_rel_sym well_ord_cardinal_rel_eqpoll_rel types)
  also have "... ≲⇗M|A|⇗M⇖" by (rule le_imp_lepoll_rel [OF ge]) (simp_all add:types)
  also have "... ≈⇗MA" by (rule well_ord_cardinal_rel_eqpoll_rel [OF s(1) _ s(2)]) (simp_all add:types)
  finally have "B ≲⇗MA" by (simp_all add:types)
  hence "A ≈⇗MB" by (blast intro: eqpoll_relI AB types)
  hence "|A|⇗M= |B|⇗M⇖" by (rule cardinal_rel_cong) (simp_all add:types)
  thus ?thesis by (simp_all add:types)
qed

lemma lepoll_rel_cardinal_rel_le: "[| A ≲⇗Mi; Ord(i); M(A); M(i) |] ==> |A|⇗M i"
  using Memrel_closed
  apply (rule_tac le_trans)
   apply (erule well_ord_Memrel [THEN well_ord_lepoll_rel_imp_cardinal_rel_le], assumption+)
  apply (erule Ord_cardinal_rel_le, assumption)
  done

lemma lepoll_rel_Ord_imp_eqpoll_rel: "[| A ≲⇗Mi; Ord(i); M(A); M(i) |] ==> |A|⇗M⇖ ≈⇗MA"
  by (blast intro: lepoll_rel_cardinal_rel_le well_ord_Memrel well_ord_cardinal_rel_eqpoll_rel dest!: lepoll_rel_well_ord)

lemma lesspoll_rel_imp_eqpoll_rel: "[| A ≺⇗Mi; Ord(i); M(A); M(i) |] ==> |A|⇗M⇖ ≈⇗MA"
  using lepoll_rel_Ord_imp_eqpoll_rel[OF lesspoll_rel_imp_lepoll_rel] .

lemma lesspoll_cardinal_lt_rel:
  shows "[| A ≺⇗Mi; Ord(i); M(i); M(A) |] ==> |A|⇗M< i"
proof -
  assume assms:"A ≺⇗Mi" Ord(i) M(i) M(A)
  then
  have A:"Ord(|A|⇗M)" "|A|⇗M⇖ ≈⇗MA" "M(|A|⇗M)"
    using Ord_cardinal_rel lesspoll_rel_imp_eqpoll_rel
    by simp_all
  with assms
  have "|A|⇗M⇖ ≺⇗Mi"
    using eq_lesspoll_rel_trans by auto
  consider "|A|⇗Mi" | "|A|⇗M=i" | "i|A|⇗M⇖"
    using Ord_linear[OF Ord(i) Ord(|A|⇗M)] by auto
  then
  have "|A|⇗M< i"
  proof(cases)
    case 1
    then show ?thesis using ltI Ord(i) by simp
  next
    case 2
    with |A|⇗M⇖ ≺⇗Mi M(i)
    show ?thesis using lesspoll_rel_irrefl by simp
  next
    case 3
    with Ord(|A|⇗M)
    have "i<|A|⇗M⇖" using ltI by simp
    with M(A) A M(i)
    have "i ≺⇗M|A|⇗M⇖"
      using lt_Card_rel_imp_lesspoll_rel Card_rel_cardinal_rel by simp
    with M(|A|⇗M) M(i)
    show ?thesis
      using lesspoll_rel_irrefl lesspoll_rel_trans[OF |A|⇗M⇖ ≺⇗Mi i ≺⇗M_]
      by simp
  qed
  then show ?thesis by simp
qed

lemma cardinal_rel_subset_Ord: "[|A<=i; Ord(i); M(A); M(i)|] ==> |A|⇗M i"
  apply (drule subset_imp_lepoll_rel [THEN lepoll_rel_cardinal_rel_le])
       apply (auto simp add: lt_def)
  apply (blast intro: Ord_trans)
  done

― ‹The next lemma is the first with several porting issues›
lemma cons_lepoll_rel_consD:
  "[| cons(u,A) ≲⇗Mcons(v,B);  uA;  vB; M(u); M(A); M(v); M(B) |] ==> A ≲⇗MB"
  apply (simp add: def_lepoll_rel, unfold inj_def, safe)
  apply (rule_tac x = "λxA. if f`x=v then f`u else f`x" in rexI)
   apply (rule CollectI)
    ― ‹Proving it's in the function space termAB
    apply (rule if_type [THEN lam_type])
     apply (blast dest: apply_funtype)
    apply (blast elim!: mem_irrefl dest: apply_funtype)
    ― ‹Proving it's injective›
   apply (auto simp add:transM[of _ A])
  using lam_replacement_iff_lam_closed  lam_if_then_apply_replacement
  by simp

lemma cons_eqpoll_rel_consD: "[| cons(u,A) ≈⇗Mcons(v,B);  uA;  vB; M(u); M(A); M(v); M(B) |] ==> A ≈⇗MB"
  apply (simp add: eqpoll_rel_iff)
  apply (blast intro: cons_lepoll_rel_consD)
  done

lemma succ_lepoll_rel_succD: "succ(m) ≲⇗Msucc(n)  M(m)  M(n) ==> m ≲⇗Mn"
  apply (unfold succ_def)
  apply (erule cons_lepoll_rel_consD)
       apply (rule mem_not_refl)+
     apply assumption+
  done

lemma nat_lepoll_rel_imp_le:
  "m  nat ==> n  nat  m ≲⇗Mn  M(m)  M(n)  m  n"
proof (induct m arbitrary: n rule: nat_induct)
  case 0 thus ?case by (blast intro!: nat_0_le)
next
  case (succ m)
  show ?case  using n  nat
  proof (cases rule: natE)
    case 0 thus ?thesis using succ
      by (simp add: def_lepoll_rel inj_def)
  next
    case (succ n') thus ?thesis using succ.hyps succ(m) ≲⇗Mn
      by (blast dest!: succ_lepoll_rel_succD)
  qed
qed

lemma nat_eqpoll_rel_iff: "[| m  nat; n  nat; M(m); M(n) |] ==> m ≈⇗Mn  m = n"
  apply (rule iffI)
   apply (blast intro: nat_lepoll_rel_imp_le le_anti_sym elim!: eqpoll_relE)
  apply (simp add: eqpoll_rel_refl)
  done

lemma nat_into_Card_rel:
  assumes n: "n  nat" and types: "M(n)" shows "Card⇗M⇖(n)"
  using types
  apply (subst Card_rel_def)
proof (unfold cardinal_rel_def, rule sym)
  have "Ord(n)" using n  by auto
  moreover
  { fix i
    assume "i < n" "M(i)" "i ≈⇗Mn"
    hence False using n
      by (auto simp add: lt_nat_in_nat [THEN nat_eqpoll_rel_iff] types)
  }
  ultimately show "(μ i. M(i)  i ≈⇗Mn) = n" by (auto intro!: Least_equality types eqpoll_rel_refl)
qed

lemmas cardinal_rel_0 = nat_0I [THEN nat_into_Card_rel, THEN Card_rel_cardinal_rel_eq, simplified, iff]
lemmas cardinal_rel_1 = nat_1I [THEN nat_into_Card_rel, THEN Card_rel_cardinal_rel_eq, simplified, iff]

lemma succ_lepoll_rel_natE: "[| succ(n) ≲⇗Mn;  n  nat |] ==> P"
  by (rule nat_lepoll_rel_imp_le [THEN lt_irrefl], auto)

lemma nat_lepoll_rel_imp_ex_eqpoll_rel_n:
  "[| n  nat;  nat ≲⇗MX ; M(n); M(X)|] ==> Y[M]. Y  X & n ≈⇗MY"
  apply (simp add: def_lepoll_rel def_eqpoll_rel)
  apply (fast del: subsetI subsetCE
      intro!: subset_SIs
      dest!: Ord_nat [THEN [2] OrdmemD, THEN [2] restrict_inj]
      elim!: restrict_bij
      inj_is_fun [THEN fun_is_rel, THEN image_subset])
  done

lemma lepoll_rel_succ: "M(i)  i ≲⇗Msucc(i)"
  by (blast intro: subset_imp_lepoll_rel)

lemma lepoll_rel_imp_lesspoll_rel_succ:
  assumes A: "A ≲⇗Mm" and m: "m  nat"
    and types: "M(A)" "M(m)"
  shows "A ≺⇗Msucc(m)"
proof -
  { assume "A ≈⇗Msucc(m)"
    hence "succ(m) ≈⇗MA" by (rule eqpoll_rel_sym) (auto simp add:types)
    also have "... ≲⇗Mm" by (rule A)
    finally have "succ(m) ≲⇗Mm" by (auto simp add:types)
    hence False by (rule succ_lepoll_rel_natE) (rule m) }
  moreover have "A ≲⇗Msucc(m)" by (blast intro: lepoll_rel_trans A lepoll_rel_succ types)
  ultimately show ?thesis by (auto simp add: types lesspoll_rel_def)
qed

lemma lesspoll_rel_succ_imp_lepoll_rel:
  "[| A ≺⇗Msucc(m); m  nat; M(A); M(m) |] ==> A ≲⇗Mm"
proof -
  {
    assume "m  nat" "M(A)" "M(m)" "A ≲⇗Msucc(m)"
      "finj⇗M⇖(A, succ(m)). f  surj⇗M⇖(A, succ(m))"
    moreover from this
    obtain f where "M(f)" "finj⇗M⇖(A,succ(m))"
      using def_lepoll_rel by auto
    moreover from calculation
    have "f  surj⇗M⇖(A, succ(m))" by simp
    ultimately
    have "f[M]. f  inj⇗M⇖(A, m)"
      using inj_rel_not_surj_rel_succ by auto
  }
  from this
  show " A ≺⇗Msucc(m); m  nat; M(A); M(m)   A ≲⇗Mm"
    unfolding lepoll_rel_def eqpoll_rel_def bij_rel_def lesspoll_rel_def
    by (simp del:mem_inj_abs)
qed

lemma lesspoll_rel_succ_iff: "m  nat  M(A) ==> A ≺⇗Msucc(m)  A ≲⇗Mm"
  by (blast intro!: lepoll_rel_imp_lesspoll_rel_succ lesspoll_rel_succ_imp_lepoll_rel)

lemma lepoll_rel_succ_disj: "[| A ≲⇗Msucc(m);  m  nat; M(A) ; M(m)|] ==> A ≲⇗Mm | A ≈⇗Msucc(m)"
  apply (rule disjCI)
  apply (rule lesspoll_rel_succ_imp_lepoll_rel)
     prefer 2 apply assumption
    apply (simp (no_asm_simp) add: lesspoll_rel_def, assumption+)
  done

lemma lesspoll_rel_cardinal_rel_lt: "[| A ≺⇗Mi; Ord(i); M(A); M(i) |] ==> |A|⇗M< i"
  apply (unfold lesspoll_rel_def, clarify)
  apply (frule lepoll_rel_cardinal_rel_le, assumption+) ― ‹because of types›
  apply (blast intro: well_ord_Memrel well_ord_cardinal_rel_eqpoll_rel [THEN eqpoll_rel_sym]
      dest: lepoll_rel_well_ord  elim!: leE)
  done

lemma lt_not_lepoll_rel:
  assumes n: "n<i" "n  nat"
    and types:"M(n)" "M(i)" shows "~ i ≲⇗Mn"
proof -
  { assume i: "i ≲⇗Mn"
    have "succ(n) ≲⇗Mi" using n
      by (elim ltE, blast intro: Ord_succ_subsetI [THEN subset_imp_lepoll_rel] types)
    also have "... ≲⇗Mn" by (rule i)
    finally have "succ(n) ≲⇗Mn" by (simp add:types)
    hence False  by (rule succ_lepoll_rel_natE) (rule n) }
  thus ?thesis by auto
qed

text‹A slightly weaker version of nat_eqpoll_rel_iff›
lemma Ord_nat_eqpoll_rel_iff:
  assumes i: "Ord(i)" and n: "n  nat"
    and types: "M(i)" "M(n)"
  shows "i ≈⇗Mn  i=n"
  using i nat_into_Ord [OF n]
proof (cases rule: Ord_linear_lt)
  case lt
  hence  "i  nat" by (rule lt_nat_in_nat) (rule n)
  thus ?thesis by (simp add: nat_eqpoll_rel_iff n types)
next
  case eq
  thus ?thesis by (simp add: eqpoll_rel_refl types)
next
  case gt
  hence  "~ i ≲⇗Mn" using n  by (rule lt_not_lepoll_rel) (simp_all add: types)
  hence  "~ i ≈⇗Mn" using n  by (blast intro: eqpoll_rel_imp_lepoll_rel types)
  moreover have "i  n" using n<i by auto
  ultimately show ?thesis by blast
qed

lemma Card_rel_nat: "Card⇗M⇖(nat)"
proof -
  { fix i
    assume i: "i < nat" "i ≈⇗Mnat" "M(i)"
    hence "~ nat ≲⇗Mi"
      by (simp add: lt_def lt_not_lepoll_rel)
    hence False using i
      by (simp add: eqpoll_rel_iff)
  }
  hence "(μ i. M(i)  i ≈⇗Mnat) = nat" by (blast intro: Least_equality eqpoll_rel_refl)
  thus ?thesis
    by (auto simp add: Card_rel_def cardinal_rel_def)
qed

lemma nat_le_cardinal_rel: "nat  i  M(i) ==> nat  |i|⇗M⇖"
  apply (rule Card_rel_nat [THEN Card_rel_cardinal_rel_eq, THEN subst], simp_all)
  apply (erule cardinal_rel_mono, simp_all)
  done

lemma n_lesspoll_rel_nat: "n  nat ==> n ≺⇗Mnat"
  by (blast intro: Card_rel_nat ltI lt_Card_rel_imp_lesspoll_rel)

lemma cons_lepoll_rel_cong:
  "[| A ≲⇗MB;  b  B; M(A); M(B); M(b); M(a) |] ==> cons(a,A) ≲⇗Mcons(b,B)"
  apply (subst (asm) def_lepoll_rel, simp_all, subst def_lepoll_rel, simp_all, safe)
  apply (rule_tac x = "λycons (a,A) . if y=a then b else f`y" in rexI)
   apply (rule_tac d = "%z. if z  B then converse (f) `z else a" in lam_injective)
    apply (safe elim!: consE')
      apply simp_all
    apply (blast intro: inj_is_fun [THEN apply_type])+
  apply (auto intro:lam_closed lam_if_then_replacement simp add:transM[of _ A])
  done

lemma cons_eqpoll_rel_cong:
  "[| A ≈⇗MB;  a  A;  b  B;  M(A); M(B); M(a) ; M(b) |] ==> cons(a,A) ≈⇗Mcons(b,B)"
  by (simp add: eqpoll_rel_iff cons_lepoll_rel_cong)

lemma cons_lepoll_rel_cons_iff:
  "[| a  A;  b  B; M(a); M(A); M(b); M(B) |] ==> cons(a,A) ≲⇗Mcons(b,B)    A ≲⇗MB"
  by (blast intro: cons_lepoll_rel_cong cons_lepoll_rel_consD)

lemma cons_eqpoll_rel_cons_iff:
  "[| a  A;  b  B; M(a); M(A); M(b); M(B) |] ==> cons(a,A) ≈⇗Mcons(b,B)    A ≈⇗MB"
  by (blast intro: cons_eqpoll_rel_cong cons_eqpoll_rel_consD)

lemma singleton_eqpoll_rel_1: "M(a)  {a} ≈⇗M1"
  apply (unfold succ_def)
  apply (blast intro!: eqpoll_rel_refl [THEN cons_eqpoll_rel_cong])
  done

lemma cardinal_rel_singleton: "M(a)  |{a}|⇗M= 1"
  apply (rule singleton_eqpoll_rel_1 [THEN cardinal_rel_cong, THEN trans])
     apply (simp (no_asm) add: nat_into_Card_rel [THEN Card_rel_cardinal_rel_eq])
    apply auto
  done

lemma not_0_is_lepoll_rel_1: "A  0 ==> M(A)  1 ≲⇗MA"
  apply (erule not_emptyE)
  apply (rule_tac a = "cons (x, A-{x}) " in subst)
   apply (rule_tac [2] a = "cons(0,0)" and P= "%y. y ≲⇗Mcons (x, A-{x})" in subst)
    apply auto
proof -
  fix x
  assume "M(A)"
  then
  show "x  A  {0} ≲⇗Mcons(x, A - {x})"
    by (auto intro: cons_lepoll_rel_cong transM[OF _ M(A)] subset_imp_lepoll_rel)
qed

lemma succ_eqpoll_rel_cong: "A ≈⇗MB  M(A)  M(B) ==> succ(A) ≈⇗Msucc(B)"
  apply (unfold succ_def)
  apply (simp add: cons_eqpoll_rel_cong mem_not_refl)
  done

text‹The next result was not straightforward to port, and even a
different statement was needed.›

lemma sum_bij_rel:
  "[| f  bij⇗M⇖(A,C); g  bij⇗M⇖(B,D); M(f); M(A); M(C); M(g); M(B); M(D)|]
      ==> (λzA+B. case(%x. Inl(f`x), %y. Inr(g`y), z))  bij⇗M⇖(A+B, C+D)"
proof -
  assume asm:"f  bij⇗M⇖(A,C)" "g  bij⇗M⇖(B,D)" "M(f)" "M(A)" "M(C)" "M(g)" "M(B)" "M(D)"
  then
  have "M(λzA+B. case(%x. Inl(f`x), %y. Inr(g`y), z))"
    using transM[OF _ M(A)] transM[OF _ M(B)]
    by (auto intro:case_replacement4[THEN lam_closed])
  with asm
  show ?thesis
    apply simp
    apply (rule_tac d = "case (%x. Inl (converse(f)`x), %y. Inr(converse(g)`y))"
        in lam_bijective)
       apply (typecheck add: bij_is_inj inj_is_fun)
     apply (auto simp add: left_inverse_bij right_inverse_bij)
    done
qed

lemma sum_bij_rel':
  assumes "f  bij⇗M⇖(A,C)" "g  bij⇗M⇖(B,D)" "M(f)"
    "M(A)" "M(C)" "M(g)" "M(B)" "M(D)"
  shows
    "(λzA+B. case(λx. Inl(f`x), λy. Inr(g`y), z))  bij(A+B, C+D)"
    "M(λzA+B. case(λx. Inl(f`x), λy. Inr(g`y), z))"
proof -
  from assms
  show "M(λzA+B. case(λx. Inl(f`x), λy. Inr(g`y), z))"
    using transM[OF _ M(A)] transM[OF _ M(B)]
    by (auto intro:case_replacement4[THEN lam_closed])
  with assms
  show "(λzA+B. case(λx. Inl(f`x), λy. Inr(g`y), z))  bij(A+B, C+D)"
    apply simp
    apply (rule_tac d = "case (%x. Inl (converse(f)`x), %y. Inr(converse(g)`y))"
        in lam_bijective)
       apply (typecheck add: bij_is_inj inj_is_fun)
     apply (auto simp add: left_inverse_bij right_inverse_bij)
    done
qed

lemma sum_eqpoll_rel_cong:
  assumes "A ≈⇗MC" "B ≈⇗MD" "M(A)" "M(C)" "M(B)" "M(D)"
  shows "A+B ≈⇗MC+D"
  using assms
proof (simp add: def_eqpoll_rel, safe, rename_tac g)
  fix f g
  assume  "M(f)" "f  bij(A, C)" "M(g)" "g  bij(B, D)"
  with assms
  obtain h where "hbij(A+B, C+D)" "M(h)"
    using sum_bij_rel'[of f A C g B D] by simp
  then
  show "f[M]. f  bij(A + B, C + D)"
    by auto
qed

lemma prod_bij_rel':
  assumes "f  bij⇗M⇖(A,C)" "g  bij⇗M⇖(B,D)" "M(f)"
    "M(A)" "M(C)" "M(g)" "M(B)" "M(D)"
  shows
    "(λ<x,y>A*B. <f`x, g`y>)  bij(A*B, C*D)"
    "M(λ<x,y>A*B. <f`x, g`y>)"
proof -
  from assms
  show "M((λ<x,y>A*B. <f`x, g`y>))"
    using transM[OF _ M(A)] transM[OF _ M(B)]
      transM[OF _ cartprod_closed, of _ A B]
    by (auto intro:prod_fun_replacement[THEN lam_closed, of f g "A×B"])
  with assms
  show "(λ<x,y>A*B. <f`x, g`y>)  bij(A*B, C*D)"
    apply simp
    apply (rule_tac d = "%<x,y>. <converse (f) `x, converse (g) `y>"
        in lam_bijective)
       apply (typecheck add: bij_is_inj inj_is_fun)
     apply (auto simp add: left_inverse_bij right_inverse_bij)
    done
qed

lemma prod_eqpoll_rel_cong:
  assumes "A ≈⇗MC" "B ≈⇗MD" "M(A)" "M(C)" "M(B)" "M(D)"
  shows "A×B ≈⇗MC×D"
  using assms
proof (simp add: def_eqpoll_rel, safe, rename_tac g)
  fix f g
  assume  "M(f)" "f  bij(A, C)" "M(g)" "g  bij(B, D)"
  with assms
  obtain h where "hbij(A×B, C×D)" "M(h)"
    using prod_bij_rel'[of f A C g B D] by simp
  then
  show "f[M]. f  bij(A × B, C × D)"
    by auto
qed

lemma inj_rel_disjoint_eqpoll_rel:
  "[| f  inj⇗M⇖(A,B);  A  B = 0;M(f); M(A);M(B) |] ==> A  (B - range(f)) ≈⇗MB"
  apply (simp add: def_eqpoll_rel)
  apply (rule rexI)
   apply (rule_tac c = "%x. if x  A then f`x else x"
      and d = "%y. if y  range (f) then converse (f) `y else y"
      in lam_bijective)
      apply (blast intro!: if_type inj_is_fun [THEN apply_type])
     apply (simp (no_asm_simp) add: inj_converse_fun [THEN apply_funtype])
    apply (safe elim!: UnE')
     apply (simp_all add: inj_is_fun [THEN apply_rangeI])
   apply (blast intro: inj_converse_fun [THEN apply_type])
proof -
  assume "f  inj(A, B)" "A  B = 0" "M(f)" "M(A)" "M(B)"
  then
  show "M(λxA  (B - range(f)). if x  A then f ` x else x)"
    using  transM[OF _ M(A)] transM[OF _ M(B)]
      lam_replacement_iff_lam_closed lam_if_then_replacement2
    by auto
qed

lemma Diff_sing_lepoll_rel:
  "[| a  A;  A ≲⇗Msucc(n); M(a); M(A); M(n) |] ==> A - {a} ≲⇗Mn"
  apply (unfold succ_def)
  apply (rule cons_lepoll_rel_consD)
        apply (rule_tac [3] mem_not_refl)
       apply (erule cons_Diff [THEN ssubst], simp_all)
  done

lemma lepoll_rel_Diff_sing:
  assumes A: "succ(n) ≲⇗MA"
    and types: "M(n)" "M(A)" "M(a)"
  shows "n ≲⇗MA - {a}"
proof -
  have "cons(n,n) ≲⇗MA" using A
    by (unfold succ_def)
  also from types
  have "... ≲⇗Mcons(a, A-{a})"
    by (blast intro: subset_imp_lepoll_rel)
  finally have "cons(n,n) ≲⇗Mcons(a, A-{a})" by (simp_all add:types)
  with types
  show ?thesis
    by (blast intro: cons_lepoll_rel_consD mem_irrefl)
qed

lemma Diff_sing_eqpoll_rel: "[| a  A; A ≈⇗Msucc(n); M(a); M(A); M(n) |] ==> A - {a} ≈⇗Mn"
  by (blast intro!: eqpoll_relI
      elim!: eqpoll_relE
      intro: Diff_sing_lepoll_rel lepoll_rel_Diff_sing)

lemma lepoll_rel_1_is_sing: "[| A ≲⇗M1; a  A ;M(a); M(A) |] ==> A = {a}"
  apply (frule Diff_sing_lepoll_rel, assumption+, simp)
  apply (drule lepoll_rel_0_is_0, simp)
  apply (blast elim: equalityE)
  done

lemma Un_lepoll_rel_sum: "M(A)  M(B)  A  B ≲⇗MA+B"
  apply (simp add: def_lepoll_rel)
  apply (rule_tac x = "λxA  B. if xA then Inl (x) else Inr (x)" in rexI)
   apply (rule_tac d = "%z. snd (z)" in lam_injective)
    apply force
   apply (simp add: Inl_def Inr_def)
proof -
  assume "M(A)" "M(B)"
  then
  show "M(λxA  B. if x  A then Inl(x) else Inr(x))"
    using transM[OF _ M(A)] transM[OF _ M(B)] if_then_Inj_replacement
    by (rule_tac lam_closed) auto
qed

lemma well_ord_Un_M:
  assumes "well_ord(X,R)" "well_ord(Y,S)"
    and types: "M(X)" "M(R)" "M(Y)" "M(S)"
  shows "T[M]. well_ord(X  Y, T)"
  using assms
  by (erule_tac well_ord_radd [THEN [3] Un_lepoll_rel_sum [THEN lepoll_rel_well_ord]])
    (auto simp add: types)

lemma disj_Un_eqpoll_rel_sum: "M(A)  M(B)  A  B = 0  A  B ≈⇗MA + B"
  apply (simp add: def_eqpoll_rel)
  apply (rule_tac x = "λaA  B. if a  A then Inl (a) else Inr (a)" in rexI)
   apply (rule_tac d = "%z. case (%x. x, %x. x, z)" in lam_bijective)
      apply auto
proof -
  assume "M(A)" "M(B)"
  then
  show "M(λxA  B. if x  A then Inl(x) else Inr(x))"
    using transM[OF _ M(A)] transM[OF _ M(B)] if_then_Inj_replacement
    by (rule_tac lam_closed) auto
qed

lemma eqpoll_rel_imp_Finite_rel_iff: "A ≈⇗MB ==> M(A)  M(B)  Finite_rel(M,A)  Finite_rel(M,B)"
  apply (unfold Finite_rel_def)
  apply (blast intro: eqpoll_rel_trans eqpoll_rel_sym)
  done

― ‹It seems reasonable to have the absoluteness of termFinite here,
and deduce the rest of the results from this.

Perhaps modularize that proof to have absoluteness of injections and
bijections of finite sets (cf. @{thm [source] lesspoll_rel_succ_imp_lepoll_rel}.›

lemma Finite_abs[simp]:
  assumes "M(A)"
  shows "Finite_rel(M,A)  Finite(A)"
  unfolding Finite_rel_def Finite_def
proof (simp, intro iffI)
  assume "nnat. A ≈⇗Mn"
  then
  obtain n where "A ≈⇗Mn" "nnat" by blast
  with assms
  show "nnat. A  n"
    unfolding eqpoll_def using nat_into_M by (auto simp add:def_eqpoll_rel)
next
  fix n
  assume "nnat. A  n"
  then
  obtain n where "A  n" "nnat" by blast
  moreover from this
  obtain f where "f  bij(A,n)" unfolding eqpoll_def by auto
  moreover
  note assms
  moreover from calculation
  have "converse(f)  nA"  using bij_is_fun by simp
  moreover from calculation
  have "M(converse(f))" using transM[of _ "nA"] by simp
  moreover from calculation
  have "M(f)" using bij_is_fun
      fun_is_rel[of "f" A "λ_. n", THEN converse_converse]
      converse_closed[of "converse(f)"] by simp
  ultimately
  show "nnat. A ≈⇗Mn"
    by (force dest:nat_into_M simp add:def_eqpoll_rel)
qed

― ‹From the next result, the relative versions of
@{thm [source] Finite_Fin_lemma} and @{thm [source] Fin_lemma} should follow›

lemma lepoll_rel_nat_imp_Finite_rel:
  assumes A: "A ≲⇗Mn" and n: "n  nat"
    and types: "M(A)" "M(n)"
  shows "Finite_rel(M,A)"
proof -
  have "A ≲⇗Mn  Finite_rel(M,A)" using n
  proof (induct n)
    case 0
    hence "A = 0" by (rule lepoll_rel_0_is_0, simp_all add:types)
    thus ?case by simp
  next
    case (succ n)
    hence "A ≲⇗Mn  A ≈⇗Msucc(n)" by (blast dest: lepoll_rel_succ_disj intro:types)
    thus ?case using succ by (auto simp add: Finite_rel_def types)
  qed
  thus ?thesis using A .
qed

lemma lesspoll_rel_nat_is_Finite_rel:
  "A ≺⇗Mnat  M(A)  Finite_rel(M,A)"
  apply (unfold Finite_rel_def)
  apply (auto dest: ltD lesspoll_rel_cardinal_rel_lt
      lesspoll_rel_imp_eqpoll_rel [THEN eqpoll_rel_sym])
  done

lemma lepoll_rel_Finite_rel:
  assumes Y: "Y ≲⇗MX" and X: "Finite_rel(M,X)"
    and types:"M(Y)" "M(X)"
  shows "Finite_rel(M,Y)"
proof -
  obtain n where n: "n  nat" "X ≈⇗Mn" "M(n)" using X
    by (auto simp add: Finite_rel_def)
  have "Y ≲⇗MX"         by (rule Y)
  also have "... ≈⇗Mn"  by (rule n)
  finally have "Y ≲⇗Mn" by (simp_all add:types M(n))
  thus ?thesis using n
    by (simp add: lepoll_rel_nat_imp_Finite_rel types M(n) del:Finite_abs)
qed

lemma succ_lepoll_rel_imp_not_empty: "succ(x) ≲⇗My ==> M(x)  M(y)  y  0"
  by (fast dest!: lepoll_rel_0_is_0)

lemma eqpoll_rel_succ_imp_not_empty: "x ≈⇗Msucc(n) ==> M(x)  M(n)  x  0"
  by (fast elim!: eqpoll_rel_sym [THEN eqpoll_rel_0_is_0, THEN succ_neq_0])

lemma Finite_subset_closed:
  assumes "Finite(B)" "BA" "M(A)"
  shows "M(B)"
proof -
  from Finite(B) BA
  show ?thesis
  proof(induct,simp)
    case (cons x D)
    with assms
    have "M(D)" "xA"
      unfolding cons_def by auto
    then
    show ?case using transM[OF _ M(A)] by simp
  qed
qed

lemma Finite_Pow_abs:
  assumes "Finite(A)" " M(A)"
  shows "Pow(A) = Pow_rel(M,A)"
  using Finite_subset_closed[OF subset_Finite] assms Pow_rel_char
  by auto

lemma Finite_Pow_rel:
  assumes "Finite(A)" "M(A)"
  shows "Finite(Pow_rel(M,A))"
  using Finite_Pow Finite_Pow_abs[symmetric] assms by simp

lemma Pow_rel_0 [simp]: "Pow_rel(M,0) = {0}"
  using Finite_Pow_abs[of 0] by simp

lemma eqpoll_rel_imp_Finite: "A ≈⇗MB  Finite(A)  M(A)  M(B)  Finite(B)"
proof -
  assume "A ≈⇗MB" "Finite(A)" "M(A)" "M(B)"
  then obtain f n g where "fbij(A,B)" "nnat" "gbij(A,n)"
    unfolding Finite_def eqpoll_def eqpoll_rel_def
    using bij_rel_char
    by auto
  then
  have "g O converse(f)  bij(B,n)"
    using bij_converse_bij comp_bij by simp
  with n_
  show"Finite(B)"
    unfolding Finite_def eqpoll_def by auto
qed

lemma eqpoll_rel_imp_Finite_iff: "A ≈⇗MB  M(A)  M(B)  Finite(A)  Finite(B)"
  using eqpoll_rel_imp_Finite eqpoll_rel_sym by force

end ― ‹localeM_cardinals

end