Theory ZF_Library

section‹Library of basic $\ZF$ results\label{sec:zf-lib}›

theory ZF_Library
  imports
    "ZF-Constructible.Normal"

begin

text‹This theory gathers basic ``combinatorial'' results that can be proved
in $\ZF$ (that is, without using the Axiom of Choice $\AC$).
›

text‹We begin by setting up math-friendly notation.›

no_notation oadd (infixl ++ 65)
no_notation sum (infixr + 65)
notation oadd (infixl + 65)
notation nat (ω)
notation csucc (‹_+ [90])
no_notation Aleph (_› [90] 90)
notation Aleph (ℵ⇘_)
syntax "_ge"  :: "[i,i]  o"  (infixl  50)
translations "x  y"  "y  x"


subsection‹Some minimal arithmetic/ordinal stuff›

lemma Un_leD1 : "i  j  k  Ord(i)  Ord(j)  Ord(k)  i  k"
  by (rule Un_least_lt_iff[THEN iffD1[THEN conjunct1]],simp_all)

lemma Un_leD2 : "i  j  k  Ord(i)  Ord(j)  Ord(k)  j  k"
  by (rule Un_least_lt_iff[THEN iffD1[THEN conjunct2]],simp_all)

lemma Un_memD1: "i  j  k  Ord(i)  Ord(j)  Ord(k)  i  k"
  by (drule ltI, assumption, drule leI, rule Un_least_lt_iff[THEN iffD1[THEN conjunct1]],simp_all)

lemma Un_memD2 : "i  j  k  Ord(i)  Ord(j)  Ord(k)  j  k"
  by (drule ltI, assumption, drule leI, rule Un_least_lt_iff[THEN iffD1[THEN conjunct2]],simp_all)

text‹This lemma allows to apply arithmetic simprocs to ordinal addition›
lemma nat_oadd_add[simp]:
  assumes "m  ω" "n  ω" shows "n + m = n #+ m"
  using assms
  by induct simp_all

lemma Ord_has_max_imp_succ:
  assumes "Ord(γ)" "β  γ" "αγ. α  β"
  shows "γ = succ(β)"
  using assms Ord_trans[of _ β γ]
  unfolding lt_def
  by (intro equalityI subsetI) auto

lemma Least_antitone:
  assumes
    "Ord(j)" "P(j)" "i. P(i)  Q(i)"
  shows
    "(μ i. Q(i))  (μ i. P(i))"
  using assms LeastI2[of P j Q] Least_le by simp

lemma Least_set_antitone:
  "Ord(j)  jA  A  B  (μ i. iB)  (μ i. iA)"
  using subset_iff by (auto intro:Least_antitone)

lemma le_neq_imp_lt:
  "xy  xy  x<y"
  using ltD ltI[of x y] le_Ord2
  unfolding succ_def by auto

text‹Strict upper bound of a set of ordinals.›
definition
  str_bound :: "ii" where
  "str_bound(A)  aA. succ(a)"

lemma str_bound_type [TC]: "aA. Ord(a)  Ord(str_bound(A))"
  unfolding str_bound_def by auto

lemma str_bound_lt: "aA. Ord(a)  aA. a < str_bound(A)"
  unfolding str_bound_def using str_bound_type
  by (blast intro:ltI)

lemma naturals_lt_nat[intro]: "n  ω  n < ω"
  unfolding lt_def by simp

text‹The next two lemmas are handy when one is constructing
some object recursively. The first handles injectivity (of recursively
constructed sequences of sets), while the second is helpful for
establishing a symmetry argument.›
lemma Int_eq_zero_imp_not_eq:
  assumes
    "x y. xD  y  D  x  y  A(x)  A(y) = 0"
    "x. xD  A(x)  0" "aD" "bD" "ab"
  shows
    "A(a)  A(b)"
  using assms by fastforce

lemma lt_neq_symmetry:
  assumes
    "α β. α  γ  β  γ  α < β  Q(α,β)"
    "α β. Q(α,β)  Q(β,α)"
    "α  γ" "β  γ" "α  β"
    "Ord(γ)"
  shows
    "Q(α,β)"
proof -
  from assms
  consider "α<β" | "β<α"
    using Ord_linear_lt[of α β thesis] Ord_in_Ord[of γ]
    by auto
  then
  show ?thesis by cases (auto simp add:assms)
qed

lemma cardinal_succ_not_0: "|A| = succ(n)  A  0"
  by auto

lemma Ord_eq_Collect_lt: "i<α  {jα. j<i} = i"
  ― ‹almost the same proof as @{thm [source] nat_eq_Collect_lt}
  apply (rule equalityI)
  apply (blast dest: ltD)
  apply (auto simp add: Ord_mem_iff_lt)
  apply (rule Ord_trans ltI[OF _ lt_Ord]; auto simp add:lt_def dest:ltD)+
  done


subsection‹Manipulation of function spaces›

definition
  Finite_to_one :: "[i,i]  i" where
  "Finite_to_one(X,Y)  {f:XY. yY. Finite({xX . f`x = y})}"

lemma Finite_to_oneI[intro]:
  assumes "f:XY" "y. yY  Finite({xX . f`x = y})"
  shows "f  Finite_to_one(X,Y)"
  using assms unfolding Finite_to_one_def by simp

lemma Finite_to_oneD[dest]:
  "f  Finite_to_one(X,Y)  f:XY"
  "f  Finite_to_one(X,Y)  yY   Finite({xX . f`x = y})"
  unfolding Finite_to_one_def by simp_all

lemma subset_Diff_Un: "X  A  A = (A - X)  X " by auto

lemma Diff_bij:
  assumes "AF. X  A" shows "(λAF. A-X)  bij(F, {A-X. AF})"
  using assms unfolding bij_def inj_def surj_def
  by (auto intro:lam_type, subst subset_Diff_Un[of X]) auto

lemma function_space_nonempty:
  assumes "bB"
  shows "(λxA. b) : A  B"
  using assms lam_type by force

lemma vimage_lam: "(λxA. f(x)) -`` B = { xA . f(x)  B }"
  using lam_funtype[of A f, THEN [2] domain_type]
    lam_funtype[of A f, THEN [2] apply_equality] lamI[of _ A f]
  by auto blast

lemma range_fun_subset_codomain:
  assumes "h:B  C"
  shows "range(h)  C"
  unfolding range_def domain_def converse_def using range_type[OF _ assms]  by auto

lemma Pi_rangeD:
  assumes "fPi(A,B)" "b  range(f)"
  shows "aA. f`a = b"
  using assms apply_equality[OF _ assms(1), of _ b]
    domain_type[OF _ assms(1)] by auto

lemma Pi_range_eq: "f  Pi(A,B)  range(f) = {f ` x . x  A}"
  using Pi_rangeD[of f A B] apply_rangeI[of f A B]
  by blast

lemma Pi_vimage_subset : "f  Pi(A,B)  f-``C  A"
  unfolding Pi_def by auto

lemma apply_in_codomain_Ord:
  assumes
    "Ord(γ)" "γ0" "f: A  γ"
  shows
    "f`xγ"
proof (cases "xA")
  case True
  from assms xA
  show ?thesis
    using   domain_of_fun apply_rangeI  by simp
next
  case False
  from assms xA
  show ?thesis
    using apply_0 Ord_0_lt ltD domain_of_fun by auto
qed

lemma range_eq_image:
  assumes "f:AB"
  shows "range(f) = f``A"
proof
  show "f `` A  range(f)"
    unfolding image_def by blast
  {
    fix x
    assume "xrange(f)"
    with assms
    have "xf``A"
      using domain_of_fun[of f A "λ_. B"] by auto
  }
  then
  show "range(f)  f `` A" ..
qed

lemma Image_sub_codomain: "f:AB  f``C  B"
  using image_subset fun_is_rel[of _ _ "λ_ . B"] by force

lemma inj_to_Image:
  assumes
    "f:AB" "f  inj(A,B)"
  shows
    "f  inj(A,f``A)"
  using assms inj_inj_range range_eq_image by force

lemma inj_imp_surj:
  fixes f b
  notes inj_is_fun[dest]
  defines [simp]: "ifx(x)  if xrange(f) then converse(f)`x else b"
  assumes "f  inj(B,A)" "bB"
  shows "(λxA. ifx(x))  surj(A,B)"
proof -
  from assms
  have "converse(f)  surj(range(f),B)" "range(f)  A"
    "converse(f) : range(f)  B"
    using inj_converse_surj range_fun_subset_codomain surj_is_fun by blast+
  with bB
  show "(λxA. ifx(x))  surj(A,B)"
    unfolding surj_def
  proof (intro CollectI lam_type ballI; elim CollectE)
    fix y
    assume "y  B" "yB. xrange(f). converse(f) ` x = y"
    with range(f)  A
    show "xA. (λxA. ifx(x)) ` x = y"
      by (drule_tac bspec, auto)
  qed simp
qed

lemma fun_Pi_disjoint_Un:
  assumes "f  Pi(A,B)" "g  Pi(C,D)"  "A  C = 0"
  shows "f  g  Pi(A  C, λx. B(x)  D(x))"
  using assms
  by (simp add: Pi_iff extension Un_rls) (unfold function_def, blast)

lemma Un_restrict_decomposition:
  assumes "f  Pi(A,B)"
  shows "f = restrict(f, A  C)  restrict(f, A - C)"
  using assms
proof (rule fun_extension)
  from assms
  have "restrict(f,AC)  restrict(f,A-C)  Pi(AC  (A-C), λx. B(x)B(x))"
    using restrict_type2[of f A B]
    by (rule_tac fun_Pi_disjoint_Un) force+
  moreover
  have "(A  C)  (A - C) = A" by auto
  ultimately
  show "restrict(f, A  C)  restrict(f, A - C)  Pi(A, B)" by simp
next
  fix x
  assume "x  A"
  with assms
  show "f ` x = (restrict(f, A  C)  restrict(f, A - C)) ` x"
    using restrict fun_disjoint_apply1[of _ "restrict(f,_)"]
      fun_disjoint_apply2[of _ "restrict(f,_)"]
      domain_restrict[of f] apply_0 domain_of_fun
    by (cases "xC") simp_all
qed

lemma restrict_eq_imp_Un_into_Pi:
  assumes "f  Pi(A,B)" "g  Pi(C,D)" "restrict(f, A  C) = restrict(g, A  C)"
  shows "f  g  Pi(A  C, λx. B(x)  D(x))"
proof -
  note assms
  moreover from this
  have "x  g  x  restrict(g, A  C)" for x
    using restrict_subset[of g "A  C"] by auto
  moreover from calculation
  have "x  f  x  restrict(f, A - C)  x  restrict(g, A  C)" for x
    by (subst (asm) Un_restrict_decomposition[of f A B "C"]) auto
  ultimately
  have "f  g = restrict(f, A - C)  g"
    using restrict_subset[of g "A  C"]
    by (subst Un_restrict_decomposition[of f A B "C"]) auto
  moreover
  have "A - C  C = A  C" by auto
  moreover
  note assms
  ultimately
  show ?thesis
    using fun_Pi_disjoint_Un[OF
        restrict_type2[of f A B "A-C"], of g C D]
    by auto
qed

lemma restrict_eq_imp_Un_into_Pi':
  assumes "f  Pi(A,B)" "g  Pi(C,D)"
    "restrict(f, domain(f)  domain(g)) = restrict(g, domain(f)  domain(g))"
  shows "f  g  Pi(A  C, λx. B(x)  D(x))"
  using  assms domain_of_fun restrict_eq_imp_Un_into_Pi by simp

lemma restrict_subset_Sigma: "f  Sigma(C,B)  restrict(f,A)  Sigma(AC, B)"
  by (auto simp add: restrict_def)


subsection‹Finite sets›

lemma Replace_sing1:
  " (a. P(d,a))  (y y'. P(d,y)  P(d,y')  y=y')   a. {y . x  {d}, P(x,y)} = {a}"
  by blast

― ‹Not really necessary›
lemma Replace_sing2:
  assumes "a. ¬ P(d,a)"
  shows "{y . x  {d}, P(x,y)} = 0"
  using assms by auto

lemma Replace_sing3:
  assumes "c e. c  e  P(d,c)  P(d,e)"
  shows "{y . x  {d}, P(x,y)} = 0"
proof -
  {
    fix z
    {
      assume "y. P(d, y)  y = z"
      with assms
      have "False" by auto
    }
    then
    have "z  {y . x  {d}, P(x,y)}"
      using Replace_iff by auto
  }
  then
  show ?thesis
    by (intro equalityI subsetI) simp_all
qed

lemma Replace_Un: "{b . a  A  B, Q(a, b)} =
        {b . a  A, Q(a, b)}  {b . a  B, Q(a, b)}"
  by (intro equalityI subsetI) (auto simp add:Replace_iff)

lemma Replace_subset_sing: "z. {y . x  {d}, P(x,y)}  {z}"
proof -
  consider
    (1) "(a. P(d,a))  (y y'. P(d,y)  P(d,y')  y=y')" |
    (2) "a. ¬ P(d,a)" | (3) "c e. c  e  P(d,c)  P(d,e)" by auto
  then
  show "z. {y . x  {d}, P(x,y)}  {z}"
  proof (cases)
    case 1
    then show ?thesis using Replace_sing1[of P d] by auto
  next
    case 2
    then show ?thesis by auto
  next
    case 3
    then show ?thesis using Replace_sing3[of P d] by auto
  qed
qed

lemma Finite_Replace: "Finite(A)  Finite(Replace(A,Q))"
proof (induct rule:Finite_induct)
  case 0
  then
  show ?case by simp
next
  case (cons x B)
  moreover
  have "{b . a  cons(x, B), Q(a, b)} =
        {b . a  B, Q(a, b)}  {b . a  {x}, Q(a, b)}"
    using Replace_Un unfolding cons_def by auto
  moreover
  obtain d where "{b . a  {x}, Q(a, b)}  {d}"
    using Replace_subset_sing[of _ Q] by blast
  moreover from this
  have "Finite({b . a  {x}, Q(a, b)})"
    using subset_Finite by simp
  ultimately
  show ?case using subset_Finite by simp
qed

lemma Finite_domain: "Finite(A)  Finite(domain(A))"
  using Finite_Replace unfolding domain_def
  by auto

lemma Finite_converse: "Finite(A)  Finite(converse(A))"
  using Finite_Replace unfolding converse_def
  by auto

lemma Finite_range: "Finite(A)  Finite(range(A))"
  using Finite_domain Finite_converse unfolding range_def
  by blast

lemma Finite_Sigma: "Finite(A)  x. Finite(B(x))  Finite(Sigma(A,B))"
  unfolding Sigma_def using Finite_RepFun Finite_Union
  by simp

lemma Finite_Pi: "Finite(A)  x. Finite(B(x))  Finite(Pi(A,B))"
  using Finite_Sigma
    Finite_Pow subset_Finite[of "Pi(A,B)" "Pow(Sigma(A,B))"]
  unfolding Pi_def
  by auto


subsection‹Basic results on equipollence, cardinality and related concepts›

lemma lepollD[dest]: "A  B  f. f  inj(A, B)"
  unfolding lepoll_def .

lemma lepollI[intro]: "f  inj(A, B)  A  B"
  unfolding lepoll_def by blast

lemma eqpollD[dest]: "A  B  f. f  bij(A, B)"
  unfolding eqpoll_def .

declare bij_imp_eqpoll[intro]

lemma range_of_subset_eqpoll:
  assumes "f  inj(X,Y)" "S  X"
  shows "S  f `` S"
  using assms restrict_bij by blast

text‹I thank Miguel Pagano for this proof.›
lemma function_space_eqpoll_cong:
  assumes
    "A  A'" "B  B'"
  shows
    "A  B  A'  B'"
proof -
  from assms(1)[THEN eqpoll_sym] assms(2)
  obtain f g where "f  bij(A',A)" "g  bij(B,B')"
    by blast
  then
  have "converse(g) : B'  B" "converse(f): A  A'"
    using bij_converse_bij bij_is_fun by auto
  show ?thesis
    unfolding eqpoll_def
  proof (intro exI fg_imp_bijective, rule_tac [1-2] lam_type)
    fix F
    assume "F: A  B"
    with f  bij(A',A) g  bij(B,B')
    show "g O F O f : A'  B'"
      using bij_is_fun comp_fun by blast
  next
    fix F
    assume "F: A'  B'"
    with converse(g) : B'  B converse(f): A  A'
    show "converse(g) O F O converse(f) : A  B"
      using comp_fun by blast
  next
    from f_ g_ converse(f)_ converse(g)_
    have "(x. x  A'  B'  converse(g) O x O converse(f)  A  B)"
      using bij_is_fun comp_fun by blast
    then
    have "(λxA  B. g O x O f) O (λxA'  B'. converse(g) O x O converse(f))
          =  (λxA'  B' . (g O converse(g)) O x O (converse(f) O f))"
      using lam_cong comp_assoc comp_lam[of "A'  B'" ] by auto
    also
    have "... = (λxA'  B' . id(B') O x O (id(A')))"
      using left_comp_inverse[OF bij_is_inj[OF f_]]
        right_comp_inverse[OF bij_is_surj[OF g_]]
      by auto
    also
    have "... = (λxA'  B' . x)"
      using left_comp_id[OF fun_is_rel] right_comp_id[OF fun_is_rel]  lam_cong by auto
    also
    have "... = id(A'B')" unfolding id_def by simp
    finally
    show "(λxA -> B. g O x O f) O (λxA' -> B'. converse(g) O x O converse(f)) = id(A' -> B')" .
  next
    from f_ g_
    have "(x. x  A  B  g O x O f  A'  B')"
      using bij_is_fun comp_fun by blast
    then
    have "(λxA' -> B'. converse(g) O x O converse(f)) O (λxA -> B. g O x O f)
          = (λxA  B . (converse(g) O g) O x O (f O converse(f)))"
      using comp_lam comp_assoc by auto
    also
    have "... = (λxA  B . id(B) O x O (id(A)))"
      using
        right_comp_inverse[OF bij_is_surj[OF f_]]
        left_comp_inverse[OF bij_is_inj[OF g_]] lam_cong
      by auto
    also
    have "... = (λxA  B . x)"
      using left_comp_id[OF fun_is_rel] right_comp_id[OF fun_is_rel] lam_cong by auto
    also
    have "... = id(AB)" unfolding id_def by simp
    finally
    show "(λxA'  B'. converse(g) O x O converse(f)) O (λxA -> B. g O x O f) = id(A -> B)" .
  qed
qed

lemma curry_eqpoll:
  fixes d ν1 ν2  κ
  shows "ν1  ν2  κ  ν1 × ν2  κ"
  unfolding eqpoll_def
proof (intro exI, rule lam_bijective,
    rule_tac [1-2] lam_type, rule_tac [2] lam_type)
  fix f z
  assume "f : ν1  ν2  κ" "z  ν1 × ν2"
  then
  show "f`fst(z)`snd(z)  κ"
    by simp
next
  fix f x y
  assume "f : ν1 × ν2  κ" "xν1" "yν2"
  then
  show "f`x,y  κ" by simp
next ― ‹one composition is the identity:›
  fix f
  assume "f : ν1 × ν2  κ"
  then
  show "(λxν1 × ν2. (λxν1. λxaν2. f ` x, xa) ` fst(x) ` snd(x)) = f"
    by (auto intro:fun_extension)
qed simp ― ‹the other composition follows automatically›

lemma Pow_eqpoll_function_space:
  fixes d X
  notes bool_of_o_def [simp]
  defines [simp]:"d(A)  (λxX. bool_of_o(xA))"
    ― ‹the witnessing map for the thesis:›
  shows "Pow(X)  X  2"
  unfolding eqpoll_def
proof (intro exI, rule lam_bijective)
  ― ‹We give explicit mutual inverses›
  fix A
  assume "APow(X)"
  then
  show "d(A) : X  2"
    using lam_type[of _ "λx. bool_of_o(xA)" "λ_. 2"]
    by force
  from APow(X)
  show "{yX. d(A)`y = 1} = A"
    by (auto)
next
  fix f
  assume "f: X2"
  then
  show "d({y  X . f ` y = 1}) = f"
    using apply_type[OF f: X2]
    by (force intro:fun_extension)
qed blast

lemma cantor_inj: "f  inj(Pow(A),A)"
  using inj_imp_surj[OF _ Pow_bottom] cantor_surj by blast

definition
  cexp :: "[i,i]  i" ("_⇗↑_" [76,1] 75) where
  "κ⇗↑ν |ν  κ|"

lemma Card_cexp: "Card(κ⇗↑ν)"
  unfolding cexp_def Card_cardinal by simp

lemma eq_csucc_ord:
  "Ord(i)  i+ = |i|+"
  using Card_lt_iff Least_cong unfolding csucc_def by auto

text‹I thank Miguel Pagano for this proof.›
lemma lesspoll_csucc:
  assumes "Ord(κ)"
  shows "d  κ+  d  κ"
proof
  assume "d  κ+"
  moreover
  note Card_is_Ord Ord(κ)
  moreover from calculation
  have "κ < κ+" "Card(κ+)"
    using Ord_cardinal_eqpoll csucc_basic by simp_all
  moreover from calculation
  have "d  |κ|+" "Card(|κ|)" "d  |d|"
    using eq_csucc_ord[of κ] lesspoll_imp_eqpoll eqpoll_sym by simp_all
  moreover from calculation
  have "|d| < |κ|+"
    using lesspoll_cardinal_lt csucc_basic by simp
  moreover from calculation
  have "|d|  |κ|"
    using Card_lt_csucc_iff le_imp_lepoll by simp
  moreover from calculation
  have "|d|  κ"
    using lepoll_eq_trans Ord_cardinal_eqpoll by simp
  ultimately
  show "d  κ"
    using eq_lepoll_trans by simp
next
  from Ord(κ)
  have "κ < κ+" "Card(κ+)"
    using csucc_basic by simp_all
  moreover
  assume "d  κ"
  ultimately
  have "d  κ+"
    using le_imp_lepoll leI lepoll_trans by simp
  moreover
  from d  κ Ord(κ)
  have "κ+  κ" if "d  κ+"
    using eqpoll_sym[OF that] eq_lepoll_trans[OF _ dκ] by simp
  moreover from calculation Card(_)
  have "¬ d  κ+"
    using lesspoll_irrefl lesspoll_trans1 lt_Card_imp_lesspoll[OF _ κ <_]
    by auto
  ultimately
  show "d  κ+"
    unfolding lesspoll_def by simp
qed

abbreviation
  Infinite :: "io" where
  "Infinite(X)  ¬ Finite(X)"

lemma Infinite_not_empty: "Infinite(X)  X  0"
  using empty_lepollI by auto

lemma Infinite_imp_nats_lepoll:
  assumes "Infinite(X)" "n  ω"
  shows "n  X"
  using n  ω
proof (induct)
  case 0
  then
  show ?case using empty_lepollI by simp
next
  case (succ x)
  show ?case
  proof -
    from Infinite(X) and x  ω
    have "¬ (x  X)"
      using eqpoll_sym unfolding Finite_def by auto
    with x  X
    obtain f where "f  inj(x,X)" "f  surj(x,X)"
      unfolding bij_def eqpoll_def by auto
    moreover from this
    obtain b where "b  X" "ax. f`a  b"
      using inj_is_fun unfolding surj_def by auto
    ultimately
    have "f  inj(x,X-{b})"
      unfolding inj_def by (auto intro:Pi_type)
    then
    have "cons(x, b, f)  inj(succ(x), cons(b, X - {b}))"
      using inj_extend[of f x "X-{b}" x b] unfolding succ_def
      by (auto dest:mem_irrefl)
    moreover from bX
    have "cons(b, X - {b}) = X" by auto
    ultimately
    show "succ(x)  X" by auto
  qed
qed

lemma zero_lesspoll: assumes "0<κ" shows "0  κ"
  using assms eqpoll_0_iff[THEN iffD1, of κ] eqpoll_sym
  unfolding lesspoll_def lepoll_def
  by (auto simp add:inj_def)

lemma lepoll_nat_imp_Infinite: "ω  X  Infinite(X)"
proof (rule ccontr, simp)
  assume "ω  X" "Finite(X)"
  moreover from this
  obtain n where "X  n" "n  ω"
    unfolding Finite_def by auto
  moreover from calculation
  have "ω  n"
    using lepoll_eq_trans by simp
  ultimately
  show "False"
    using lepoll_nat_imp_Finite nat_not_Finite by simp
qed

lemma InfCard_imp_Infinite: "InfCard(κ)  Infinite(κ)"
  using le_imp_lepoll[THEN lepoll_nat_imp_Infinite, of κ]
  unfolding InfCard_def by simp

lemma lt_surj_empty_imp_Card:
  assumes "Ord(κ)" "α. α < κ  surj(α,κ) = 0"
  shows "Card(κ)"
proof -
  {
    assume "|κ| < κ"
    with assms
    have "False"
      using LeastI[of "λi. i  κ" κ, OF eqpoll_refl]
        Least_le[of "λi. i  κ" "|κ|", OF Ord_cardinal_eqpoll]
      unfolding Card_def cardinal_def eqpoll_def bij_def
      by simp
  }
  with assms
  show ?thesis
    using Ord_cardinal_le[of κ] not_lt_imp_le[of "|κ|" κ] le_anti_sym
    unfolding Card_def by auto
qed


subsection‹Morphisms of binary relations›

text‹The main case of interest is in the case of partial orders.›

lemma mono_map_mono:
  assumes
    "f  mono_map(A,r,B,s)" "B  C"
  shows
    "f  mono_map(A,r,C,s)"
  unfolding mono_map_def
proof (intro CollectI ballI impI)
  from f  mono_map(A,_,B,_)
  have "f: A  B"
    using mono_map_is_fun by simp
  with BC
  show "f: A  C"
    using fun_weaken_type by simp
  fix x y
  assume "xA" "yA" "x,y  r"
  moreover from this and f: A  B
  have "f`x  B" "f`y  B"
    using apply_type by simp_all
  moreover
  note f  mono_map(_,r,_,s)
  ultimately
  show "f ` x, f ` y  s"
    unfolding mono_map_def by blast
qed

lemma ordertype_zero_imp_zero: "ordertype(A,r) = 0  A = 0"
  using ordermap_type[of A r]
  by (cases "A=0") auto

lemma mono_map_increasing:
  "jmono_map(A,r,B,s)  aA  cA  a,cr  j`a,j`cs"
  unfolding mono_map_def by simp

lemma linear_mono_map_reflects:
  assumes
    "linear(α,r)" "trans[β](s)" "irrefl(β,s)" "fmono_map(α,r,β,s)"
    "xα" "yα" "f`x,f`ys"
  shows
    "x,yr"
proof -
  from fmono_map(_,_,_,_)
  have preserves:"xα  yα  x,yr  f`x,f`ys" for x y
    unfolding mono_map_def by blast
  {
    assume "x, y  r" "xα" "yα"
    moreover
    note f`x,f`ys and linear(α,r)
    moreover from calculation
    have "y = x  y,xr"
      unfolding linear_def by blast
    moreover
    note preserves [of y x]
    ultimately
    have "y = x  f`y, f`x s" by blast
    moreover from fmono_map(_,_,β,_) xα yα
    have "f`xβ" "f`yβ"
      using apply_type[OF mono_map_is_fun] by simp_all
    moreover
    note f`x,f`ys  trans[β](s) irrefl(β,s)
    ultimately
    have "False"
      using trans_onD[of β s "f`x" "f`y" "f`x"] irreflE by blast
  }
  with assms
  show "x,yr" by blast
qed

lemma irrefl_Memrel: "irrefl(x, Memrel(x))"
  unfolding irrefl_def using mem_irrefl by auto

lemmas Memrel_mono_map_reflects = linear_mono_map_reflects
  [OF well_ord_is_linear[OF well_ord_Memrel] well_ord_is_trans_on[OF well_ord_Memrel]
    irrefl_Memrel]

― ‹Same proof as Paulson's @{thm [source] mono_map_is_inj}
lemma mono_map_is_inj':
  " linear(A,r);  irrefl(B,s);  f  mono_map(A,r,B,s)   f  inj(A,B)"
  unfolding irrefl_def mono_map_def inj_def using linearE
  by (clarify, rename_tac x w)
    (erule_tac x=w and y=x in linearE, assumption+, (force intro: apply_type)+)

lemma mono_map_imp_ord_iso_image:
  assumes
    "linear(α,r)" "trans[β](s)"  "irrefl(β,s)" "fmono_map(α,r,β,s)"
  shows
    "f  ord_iso(α,r,f``α,s)"
  unfolding ord_iso_def
proof (intro CollectI ballI iffI)
  ― ‹Enough to show it's bijective and preserves both ways›
  from assms
  have "f  inj(α,β)"
    using mono_map_is_inj' by blast
  moreover from f  mono_map(_,_,_,_)
  have "f  surj(α, f``α)"
    unfolding mono_map_def using surj_image by auto
  ultimately
  show "f  bij(α, f``α)"
    unfolding bij_def using inj_is_fun inj_to_Image by simp
  from fmono_map(_,_,_,_)
  show "xα  yα  x,yr  f`x,f`ys" for x y
    unfolding mono_map_def by blast
  with assms
  show "f`x,f`ys  xα  yα  x,yr" for x y
    using linear_mono_map_reflects
    by blast
qed

text‹We introduce the following notation for strictly increasing maps
between ordinals.›

abbreviation
  mono_map_Memrel :: "[i,i]  i" (infixr < 60) where
  "α < β  mono_map(α,Memrel(α),β,Memrel(β))"

lemma mono_map_imp_ord_iso_Memrel:
  assumes
    "Ord(α)" "Ord(β)" "f:α < β"
  shows
    "f  ord_iso(α,Memrel(α),f``α,Memrel(β))"
  using assms mono_map_imp_ord_iso_image[OF well_ord_is_linear[OF well_ord_Memrel]
      well_ord_is_trans_on[OF well_ord_Memrel] irrefl_Memrel] by blast

lemma mono_map_ordertype_image':
  assumes
    "Xα" "Ord(α)" "Ord(β)" "f  mono_map(X,Memrel(α),β,Memrel(β))"
  shows
    "ordertype(f``X,Memrel(β)) = ordertype(X,Memrel(α))"
  using assms mono_map_is_fun[of f X _ β]  ordertype_eq
    mono_map_imp_ord_iso_image[OF well_ord_is_linear[OF well_ord_Memrel, THEN linear_subset]
      well_ord_is_trans_on[OF well_ord_Memrel] irrefl_Memrel, of α X β f]
    well_ord_subset[OF well_ord_Memrel]  Image_sub_codomain[of f X β X] by auto

lemma mono_map_ordertype_image:
  assumes
    "Ord(α)" "Ord(β)" "f:α < β"
  shows
    "ordertype(f``α,Memrel(β)) = α"
  using assms mono_map_is_fun ordertype_Memrel ordertype_eq[of f α "Memrel(α)"]
    mono_map_imp_ord_iso_Memrel well_ord_subset[OF well_ord_Memrel] Image_sub_codomain[of _ α]
  by auto

lemma apply_in_image: "f:AB  aA  f`a  f``A"
  using range_eq_image apply_rangeI[of f]  by simp

lemma Image_subset_Ord_imp_lt:
  assumes
    "Ord(α)" "h``A  α" "xdomain(h)" "xA" "function(h)"
  shows
    "h`x < α"
  using assms
  unfolding domain_def using imageI ltI function_apply_equality by auto

lemma ordermap_le_arg:
  assumes
    "Xβ" "xX" "Ord(β)"
  shows
    "xX  ordermap(X,Memrel(β))`xx"
proof (induct rule:Ord_induct[OF subsetD, OF assms])
  case (1 x)
  have "wf[X](Memrel(β))"
    using wf_imp_wf_on[OF wf_Memrel] .
  with 1
  have "ordermap(X,Memrel(β))`x = {ordermap(X,Memrel(β))`y . y{yX . yx  yβ}}"
    using ordermap_unfold Ord_trans[of _ x β] by auto
  also from assms
  have "... = {ordermap(X,Memrel(β))`y . y{yX . yx}}"
    using Ord_trans[of _ x β] Ord_in_Ord by blast
  finally
  have ordm:"ordermap(X,Memrel(β))`x = {ordermap(X,Memrel(β))`y . y{yX . yx}}" .
  from 1
  have "yx  yX  ordermap(X,Memrel(β))`y  y" for y by simp
  with xβ and Ord(β)
  have "yx  yX  ordermap(X,Memrel(β))`y  x" for y
    using ltI[OF _ Ord_in_Ord[of β x]] lt_trans1 ltD by blast
  with ordm
  have "ordermap(X,Memrel(β))`x  x" by auto
  with xX assms
  show ?case
    using subset_imp_le Ord_in_Ord[of β x] Ord_ordermap
      well_ord_subset[OF well_ord_Memrel, of β] by force
qed

lemma subset_imp_ordertype_le:
  assumes
    "Xβ" "Ord(β)"
  shows
    "ordertype(X,Memrel(β))β"
proof -
  {
    fix x
    assume "xX"
    with assms
    have "ordermap(X,Memrel(β))`x  x"
      using ordermap_le_arg by simp
    with xX and assms
    have "ordermap(X,Memrel(β))`x  β" (is "?y  _")
      using ltD[of ?y "succ(x)"] Ord_trans[of  ?y x β] by auto
  }
  then
  have "ordertype(X, Memrel(β))  β"
    using ordertype_unfold[of X] by auto
  with assms
  show ?thesis
    using subset_imp_le Ord_ordertype[OF well_ord_subset, OF well_ord_Memrel] by simp
qed

lemma mono_map_imp_le:
  assumes
    "fmono_map(α, Memrel(α),β, Memrel(β))" "Ord(α)" "Ord(β)"
  shows
    "αβ"
proof -
  from assms
  have "f  α, Memrel(α)  f``α, Memrel(β)"
    using mono_map_imp_ord_iso_Memrel by simp
  then
  have "converse(f)  f``α, Memrel(β)  α, Memrel(α)"
    using ord_iso_sym by simp
  with Ord(α)
  have "α = ordertype(f``α,Memrel(β))"
    using ordertype_eq well_ord_Memrel ordertype_Memrel by auto
  also from assms
  have "ordertype(f``α,Memrel(β))  β"
    using subset_imp_ordertype_le mono_map_is_fun[of f] Image_sub_codomain[of f] by force
  finally
  show ?thesis .
qed

― ‹termOrd(A)  f  mono_map(A, Memrel(A), B, Memrel(Aa))  f  inj(A, B) 
lemmas Memrel_mono_map_is_inj = mono_map_is_inj
  [OF well_ord_is_linear[OF well_ord_Memrel]
    wf_imp_wf_on[OF wf_Memrel]]

lemma mono_mapI:
  assumes "f: AB" "x y. xA  yA  x,yr  f`x,f`ys"
  shows   "f  mono_map(A,r,B,s)"
  unfolding mono_map_def using assms by simp

lemmas mono_mapD = mono_map_is_fun mono_map_increasing

bundle mono_map_rules =  mono_mapI[intro!] mono_map_is_fun[dest] mono_mapD[dest]

lemma nats_le_InfCard:
  assumes "n  ω" "InfCard(κ)"
  shows "n  κ"
  using assms Ord_is_Transset
    le_trans[of n ω κ, OF le_subset_iff[THEN iffD2]]
  unfolding InfCard_def Transset_def by simp

lemma nat_into_InfCard:
  assumes "n  ω" "InfCard(κ)"
  shows "n  κ"
  using assms  le_imp_subset[of ω κ]
  unfolding InfCard_def by auto


subsection‹Alephs are infinite cardinals›

lemma Aleph_zero_eq_nat: "ℵ⇘0= ω"
  unfolding Aleph_def by simp

lemma InfCard_Aleph:
  notes Aleph_zero_eq_nat[simp]
  assumes "Ord(α)"
  shows "InfCard(ℵ⇘α)"
proof -
  have "¬ (ℵ⇘α ω)"
  proof (cases "α=0")
    case True
    then show ?thesis using mem_irrefl by auto
  next
    case False
    with Ord(α)
    have "ω  ℵ⇘α⇙" using Ord_0_lt[of α] ltD  by (auto dest:Aleph_increasing)
    then show ?thesis using foundation by blast
  qed
  with Ord(α)
  have "¬ (|ℵ⇘α|  ω)"
    using Card_cardinal_eq by auto
  then
  have "¬ Finite(ℵ⇘α)" by auto
  with Ord(α)
  show ?thesis
    using Inf_Card_is_InfCard by simp
qed

text‹Most properties of cardinals depend on $\AC$, even for the countable.
Here we just state the definition of this concept, and most proofs will
appear after assuming Choice.›
― ‹Kunen's Definition I.10.5›
definition
  countable :: "io" where
  "countable(X)  X  ω"

lemma countableI[intro]: "X  ω  countable(X)"
  unfolding countable_def by simp

lemma countableD[dest]: "countable(X)  X  ω"
  unfolding countable_def by simp


text‹A ‹delta system› is family of sets with a common pairwise
intersection. We will work with this notion in Section~\ref{sec:dsl},
but we state the definition here in order to have it available in a
choiceless context.›

definition
  delta_system :: "i  o" where
  "delta_system(D)  r. AD. BD. A  B  A  B = r"

lemma delta_systemI[intro]:
  assumes "AD. BD. A  B  A  B = r"
  shows "delta_system(D)"
  using assms unfolding delta_system_def by simp

lemma delta_systemD[dest]:
  "delta_system(D)  r. AD. BD. A  B  A  B = r"
  unfolding delta_system_def by simp

text‹Hence, pairwise intersections equal the intersection of the whole
family.›

lemma delta_system_root_eq_Inter:
  assumes "delta_system(D)"
  shows "AD. BD. A  B  A  B = D"
proof (clarify, intro equalityI, auto)
  fix A' B' x C
  assume hyp:"A'D" "B' D" "A'B'" "xA'" "xB'" "CD"
  with assms
  obtain r where delta:"AD. BD. A  B  A  B = r"
    by auto
  show "x  C"
  proof (cases "C=A'")
    case True
    with hyp and assms
    show ?thesis by simp
  next
    case False
    moreover
    note hyp
    moreover from calculation and delta
    have "r = C  A'" "A'  B' = r" "xr" by auto
    ultimately
    show ?thesis by simp
  qed
qed

lemmas Limit_Aleph = InfCard_Aleph[THEN InfCard_is_Limit]

lemmas Aleph_cont = Normal_imp_cont[OF Normal_Aleph]
lemmas Aleph_sup = Normal_Union[OF _ _ Normal_Aleph]

bundle Ord_dests = Limit_is_Ord[dest] Card_is_Ord[dest]
bundle Aleph_dests = Aleph_cont[dest] Aleph_sup[dest]
bundle Aleph_intros = Aleph_increasing[intro!]
bundle Aleph_mem_dests = Aleph_increasing[OF ltI, THEN ltD, dest]

subsection‹Transfinite recursive constructions›

definition
  rec_constr :: "[i,i]  i" where
  "rec_constr(f,α)  transrec(α,λa g. f`(g``a))"

text‹The function termrec_constr allows to perform ‹recursive
     constructions›: given a choice function on the powerset of some
     set, a transfinite sequence is created by successively choosing
     some new element.

     The next result explains its use.›

lemma rec_constr_unfold: "rec_constr(f,α) = f`({rec_constr(f,β). βα})"
  using def_transrec[OF rec_constr_def, of f α] image_lam by simp

lemma rec_constr_type: assumes "f:Pow(G) G" "Ord(α)"
  shows "rec_constr(f,α)  G"
  using assms(2,1)
  by (induct rule:trans_induct)
    (subst rec_constr_unfold, rule apply_type[of f "Pow(G)" "λ_. G"], auto)


end