Theory HOL-Library.Equipollence

section ‹Equipollence and Other Relations Connected with Cardinality›

theory "Equipollence"
  imports FuncSet Countable_Set
begin

subsection‹Eqpoll›

definition eqpoll :: "'a set  'b set  bool" (infixl "" 50)
  where "eqpoll A B  f. bij_betw f A B"

definition lepoll :: "'a set  'b set  bool" (infixl "" 50)
  where "lepoll A B  f. inj_on f A  f ` A  B"

definition lesspoll :: "'a set  'b set  bool" (infixl  50)
  where "A  B == A  B  ~(A  B)"

lemma lepoll_def': "lepoll A B  f. inj_on f A  f  A  B"
  by (simp add: Pi_iff image_subset_iff lepoll_def)

lemma eqpoll_empty_iff_empty [simp]: "A  {}  A={}"
  by (simp add: bij_betw_iff_bijections eqpoll_def)

lemma lepoll_empty_iff_empty [simp]: "A  {}  A = {}"
  by (auto simp: lepoll_def)

lemma not_lesspoll_empty: "¬ A  {}"
  by (simp add: lesspoll_def)

(*The HOL Light CARD_LE_RELATIONAL_FULL*)
lemma lepoll_relational_full:
  assumes "y. y  B  x. x  A  R x y"
    and "x y y'. x  A; y  B; y'  B; R x y; R x y'  y = y'"
  shows "B  A"
proof -
  obtain f where f: "y. y  B  f y  A  R (f y) y"
    using assms by metis
  with assms have "inj_on f B"
    by (metis inj_onI)
  with f show ?thesis
    unfolding lepoll_def by blast
qed

lemma eqpoll_iff_card_of_ordIso: "A  B  ordIso2 (card_of A) (card_of B)"
  by (simp add: card_of_ordIso eqpoll_def)

lemma eqpoll_refl [iff]: "A  A"
  by (simp add: card_of_refl eqpoll_iff_card_of_ordIso)

lemma eqpoll_finite_iff: "A  B  finite A  finite B"
  by (meson bij_betw_finite eqpoll_def)

lemma eqpoll_iff_card:
  assumes "finite A" "finite B"
  shows  "A  B  card A = card B"
  using assms by (auto simp: bij_betw_iff_card eqpoll_def)

lemma eqpoll_singleton_iff: "A  {x}  (u. A = {u})"
  by (metis card.infinite card_1_singleton_iff eqpoll_finite_iff eqpoll_iff_card not_less_eq_eq)

lemma eqpoll_doubleton_iff: "A  {x,y}  (u v. A = {u,v}  (u=v  x=y))"
proof (cases "x=y")
  case True
  then show ?thesis
    by (simp add: eqpoll_singleton_iff)
next
  case False
  then show ?thesis
    by (smt (verit, ccfv_threshold) card_1_singleton_iff card_Suc_eq_finite eqpoll_finite_iff
        eqpoll_iff_card finite.insertI singleton_iff)
qed

lemma lepoll_antisym:
  assumes "A  B" "B  A" shows "A  B"
  using assms unfolding eqpoll_def lepoll_def by (metis Schroeder_Bernstein)

lemma lepoll_trans [trans]:
  assumes "A  B" " B  C" shows "A  C"
proof -
  obtain f g where fg: "inj_on f A" "inj_on g B" and "f : A  B" "g  B  C"
    by (metis assms lepoll_def')
  then have "g  f  A  C"
    by auto
  with fg show ?thesis
    unfolding lepoll_def
    by (metis f  A  B comp_inj_on image_subset_iff_funcset inj_on_subset)
qed

lemma lepoll_trans1 [trans]: "A  B; B  C  A  C"
  by (meson card_of_ordLeq eqpoll_iff_card_of_ordIso lepoll_def lepoll_trans ordIso_iff_ordLeq)

lemma lepoll_trans2 [trans]: "A  B; B  C  A  C"
  by (metis bij_betw_def eqpoll_def lepoll_def lepoll_trans order_refl)

lemma eqpoll_sym: "A  B  B  A"
  unfolding eqpoll_def
  using bij_betw_the_inv_into by auto

lemma eqpoll_trans [trans]: "A  B; B  C  A  C"
  unfolding eqpoll_def using bij_betw_trans by blast

lemma eqpoll_imp_lepoll: "A  B  A  B"
  unfolding eqpoll_def lepoll_def by (metis bij_betw_def order_refl)

lemma subset_imp_lepoll: "A  B  A  B"
  by (force simp: lepoll_def)

lemma lepoll_refl [iff]: "A  A"
  by (simp add: subset_imp_lepoll)

lemma lepoll_iff: "A  B  (g. A  g ` B)"
  unfolding lepoll_def
proof safe
  fix g assume "A  g ` B"
  then show "f. inj_on f A  f ` A  B"
    by (rule_tac x="inv_into B g" in exI) (auto simp: inv_into_into inj_on_inv_into)
qed (metis image_mono the_inv_into_onto)

lemma empty_lepoll [iff]: "{}  A"
  by (simp add: lepoll_iff)

lemma subset_image_lepoll: "B  f ` A  B  A"
  by (auto simp: lepoll_iff)

lemma image_lepoll: "f ` A  A"
  by (auto simp: lepoll_iff)

lemma infinite_le_lepoll: "infinite A  (UNIV::nat set)  A"
  by (simp add: infinite_iff_countable_subset lepoll_def)

lemma lepoll_Pow_self: "A  Pow A"
  unfolding lepoll_def inj_def
  proof (intro exI conjI)
    show "inj_on (λx. {x}) A"
      by (auto simp: inj_on_def)
qed auto

lemma eqpoll_iff_bijections:
   "A  B  (f g. (x  A. f x  B  g(f x) = x)  (y  B. g y  A  f(g y) = y))"
    by (auto simp: eqpoll_def bij_betw_iff_bijections)

lemma lepoll_restricted_funspace:
   "{f. f ` A  B  {x. f x  k x}  A  finite {x. f x  k x}}  Fpow (A × B)"
proof -
  have *: "U  Fpow (A × B). f = (λx. if y. (x, y)  U then SOME y. (x,y)  U else k x)"
    if "f ` A  B" "{x. f x  k x}  A" "finite {x. f x  k x}" for f
    apply (rule_tac x="(λx. (x, f x)) ` {x. f x  k x}" in bexI)
    using that by (auto simp: image_def Fpow_def)
  show ?thesis
    apply (rule subset_image_lepoll [where f = "λU x. if y. (x,y)  U then @y. (x,y)  U else k x"])
    using * by (auto simp: image_def)
qed

lemma singleton_lepoll: "{x}  insert y A"
  by (force simp: lepoll_def)

lemma singleton_eqpoll: "{x}  {y}"
  by (blast intro: lepoll_antisym singleton_lepoll)

lemma subset_singleton_iff_lepoll: "(x. S  {x})  S  {()}"
  using lepoll_iff by fastforce

lemma infinite_insert_lepoll:
  assumes "infinite A" shows "insert a A  A"
proof -
  obtain f :: "nat  'a" where "inj f" and f: "range f  A"
    using assms infinite_countable_subset by blast
  let ?g = "(λz. if z=a then f 0 else if z  range f then f (Suc (inv f z)) else z)"
  show ?thesis
    unfolding lepoll_def
  proof (intro exI conjI)
    show "inj_on ?g (insert a A)"
      using inj_on_eq_iff [OF inj f]
      by (auto simp: inj_on_def)
    show "?g ` insert a A  A"
      using f by auto
  qed
qed

lemma infinite_insert_eqpoll: "infinite A  insert a A  A"
  by (simp add: lepoll_antisym infinite_insert_lepoll subset_imp_lepoll subset_insertI)

lemma finite_lepoll_infinite:
  assumes "infinite A" "finite B" shows "B  A"
proof -
  have "B  (UNIV::nat set)"
    unfolding lepoll_def
    using finite_imp_inj_to_nat_seg [OF finite B] by blast
  then show ?thesis
    using infinite A infinite_le_lepoll lepoll_trans by auto
qed

lemma countable_lepoll: "countable A; B  A  countable B"
  by (meson countable_image countable_subset lepoll_iff)

lemma countable_eqpoll: "countable A; B  A  countable B"
  using countable_lepoll eqpoll_imp_lepoll by blast

subsection‹The strict relation›

lemma lesspoll_not_refl [iff]: "~ (i  i)"
  by (simp add: lepoll_antisym lesspoll_def)

lemma lesspoll_imp_lepoll: "A  B ==> A  B"
by (unfold lesspoll_def, blast)

lemma lepoll_iff_leqpoll: "A  B  A  B | A  B"
  using eqpoll_imp_lepoll lesspoll_def by blast

lemma lesspoll_trans [trans]: "X  Y; Y  Z  X  Z"
  by (meson eqpoll_sym lepoll_antisym lepoll_trans lepoll_trans1 lesspoll_def)

lemma lesspoll_trans1 [trans]: "X  Y; Y  Z  X  Z"
  by (meson eqpoll_sym lepoll_antisym lepoll_trans lepoll_trans1 lesspoll_def)

lemma lesspoll_trans2 [trans]: "X  Y; Y  Z  X  Z"
  by (meson eqpoll_imp_lepoll eqpoll_sym lepoll_antisym lepoll_trans lesspoll_def)

lemma eq_lesspoll_trans [trans]: "X  Y; Y  Z  X  Z"
  using eqpoll_imp_lepoll lesspoll_trans1 by blast

lemma lesspoll_eq_trans [trans]: "X  Y; Y  Z  X  Z"
  using eqpoll_imp_lepoll lesspoll_trans2 by blast

lemma lesspoll_Pow_self: "A  Pow A"
  unfolding lesspoll_def bij_betw_def eqpoll_def
  by (meson lepoll_Pow_self Cantors_theorem)

lemma finite_lesspoll_infinite:
  assumes "infinite A" "finite B" shows "B  A"
  by (meson assms eqpoll_finite_iff finite_lepoll_infinite lesspoll_def)

lemma countable_lesspoll: "countable A; B  A  countable B"
  using countable_lepoll lesspoll_def by blast

lemma lepoll_iff_card_le: "finite A; finite B  A  B  card A  card B"
  by (simp add: inj_on_iff_card_le lepoll_def)

lemma lepoll_iff_finite_card: "A  {..<n::nat}  finite A  card A  n"
  by (metis card_lessThan finite_lessThan finite_surj lepoll_iff lepoll_iff_card_le)

lemma eqpoll_iff_finite_card: "A  {..<n::nat}  finite A  card A = n"
  by (metis card_lessThan eqpoll_finite_iff eqpoll_iff_card finite_lessThan)

lemma lesspoll_iff_finite_card: "A  {..<n::nat}  finite A  card A < n"
  by (metis eqpoll_iff_finite_card lepoll_iff_finite_card lesspoll_def order_less_le)

subsection‹Mapping by an injection›

lemma inj_on_image_eqpoll_self: "inj_on f A  f ` A  A"
  by (meson bij_betw_def eqpoll_def eqpoll_sym)

lemma inj_on_image_lepoll_1 [simp]:
  assumes "inj_on f A" shows "f ` A  B  A  B"
  by (meson assms image_lepoll lepoll_def lepoll_trans order_refl)

lemma inj_on_image_lepoll_2 [simp]:
  assumes "inj_on f B" shows "A  f ` B  A  B"
  by (meson assms eq_iff image_lepoll lepoll_def lepoll_trans)

lemma inj_on_image_lesspoll_1 [simp]:
  assumes "inj_on f A" shows "f ` A  B  A  B"
  by (meson assms image_lepoll le_less lepoll_def lesspoll_trans1)

lemma inj_on_image_lesspoll_2 [simp]:
  assumes "inj_on f B" shows "A  f ` B  A  B"
  by (meson assms eqpoll_sym inj_on_image_eqpoll_self lesspoll_eq_trans)

lemma inj_on_image_eqpoll_1 [simp]:
  assumes "inj_on f A" shows "f ` A  B  A  B"
  by (metis assms eqpoll_trans inj_on_image_eqpoll_self eqpoll_sym)

lemma inj_on_image_eqpoll_2 [simp]:
  assumes "inj_on f B" shows "A  f ` B  A  B"
  by (metis assms inj_on_image_eqpoll_1 eqpoll_sym)

subsection ‹Inserting elements into sets›

lemma insert_lepoll_insertD:
  assumes "insert u A  insert v B" "u  A" "v  B" shows "A  B"
proof -
  obtain f where inj: "inj_on f (insert u A)" and fim: "f ` (insert u A)  insert v B"
    by (meson assms lepoll_def)
  show ?thesis
    unfolding lepoll_def
  proof (intro exI conjI)
    let ?g = "λxA. if f x = v then f u else f x"
    show "inj_on ?g A"
      using inj u  A by (auto simp: inj_on_def)
    show "?g ` A  B"
      using fim u  A image_subset_iff inj inj_on_image_mem_iff by fastforce
  qed
qed

lemma insert_eqpoll_insertD: "insert u A  insert v B; u  A; v  B  A  B"
  by (meson insert_lepoll_insertD eqpoll_imp_lepoll eqpoll_sym lepoll_antisym)

lemma insert_lepoll_cong:
  assumes "A  B" "b  B" shows "insert a A  insert b B"
proof -
  obtain f where f: "inj_on f A" "f ` A  B"
    by (meson assms lepoll_def)
  let ?f = "λu  insert a A. if u=a then b else f u"
  show ?thesis
    unfolding lepoll_def
  proof (intro exI conjI)
    show "inj_on ?f (insert a A)"
      using f b  B by (auto simp: inj_on_def)
    show "?f ` insert a A  insert b B"
      using f b  B by auto
  qed
qed

lemma insert_eqpoll_cong:
     "A  B; a  A; b  B  insert a A  insert b B"
  apply (rule lepoll_antisym)
  apply (simp add: eqpoll_imp_lepoll insert_lepoll_cong)+
  by (meson eqpoll_imp_lepoll eqpoll_sym insert_lepoll_cong)

lemma insert_eqpoll_insert_iff:
     "a  A; b  B  insert a A  insert b B    A  B"
  by (meson insert_eqpoll_insertD insert_eqpoll_cong)

lemma insert_lepoll_insert_iff:
     " a  A; b  B  (insert a A  insert b B)  (A  B)"
  by (meson insert_lepoll_insertD insert_lepoll_cong)

lemma less_imp_insert_lepoll:
  assumes "A  B" shows "insert a A  B"
proof -
  obtain f where "inj_on f A" "f ` A  B"
    using assms by (metis bij_betw_def eqpoll_def lepoll_def lesspoll_def psubset_eq)
  then obtain b where b: "b  B" "b  f ` A"
    by auto
  show ?thesis
    unfolding lepoll_def
  proof (intro exI conjI)
    show "inj_on (f(a:=b)) (insert a A)"
      using b inj_on f A by (auto simp: inj_on_def)
    show "(f(a:=b)) ` insert a A  B"
      using f ` A  B  by (auto simp: b)
  qed
qed

lemma finite_insert_lepoll: "finite A  (insert a A  A)  (a  A)"
proof (induction A rule: finite_induct)
  case (insert x A)
  then show ?case
    apply (auto simp: insert_absorb)
    by (metis insert_commute insert_iff insert_lepoll_insertD)
qed auto


subsection‹Binary sums and unions›

lemma Un_lepoll_mono:
  assumes "A  C" "B  D" "disjnt C D" shows "A  B  C  D"
proof -
  obtain f g where inj: "inj_on f A" "inj_on g B" and fg: "f ` A  C" "g ` B  D"
    by (meson assms lepoll_def)
  have "inj_on (λx. if x  A then f x else g x) (A  B)"
    using inj disjnt C D fg unfolding disjnt_iff
    by (fastforce intro: inj_onI dest: inj_on_contraD split: if_split_asm)
  with fg show ?thesis
    unfolding lepoll_def
    by (rule_tac x="λx. if x  A then f x else g x" in exI) auto
qed

lemma Un_eqpoll_cong: "A  C; B  D; disjnt A B; disjnt C D  A  B  C  D"
  by (meson Un_lepoll_mono eqpoll_imp_lepoll eqpoll_sym lepoll_antisym)

lemma sum_lepoll_mono:
  assumes "A  C" "B  D" shows "A <+> B  C <+> D"
proof -
  obtain f g where "inj_on f A" "f ` A  C" "inj_on g B" "g ` B  D"
    by (meson assms lepoll_def)
  then show ?thesis
    unfolding lepoll_def
    by (rule_tac x="case_sum (Inl  f) (Inr  g)" in exI) (force simp: inj_on_def)
qed

lemma sum_eqpoll_cong: "A  C; B  D  A <+> B  C <+> D"
  by (meson eqpoll_imp_lepoll eqpoll_sym lepoll_antisym sum_lepoll_mono)

subsection‹Binary Cartesian products›

lemma times_square_lepoll: "A  A × A"
  unfolding lepoll_def inj_def
proof (intro exI conjI)
  show "inj_on (λx. (x,x)) A"
    by (auto simp: inj_on_def)
qed auto

lemma times_commute_eqpoll: "A × B  B × A"
  unfolding eqpoll_def
  by (force intro: bij_betw_byWitness [where f = "λ(x,y). (y,x)" and f' = "λ(x,y). (y,x)"])

lemma times_assoc_eqpoll: "(A × B) × C  A × (B × C)"
  unfolding eqpoll_def
  by (force intro: bij_betw_byWitness [where f = "λ((x,y),z). (x,(y,z))" and f' = "λ(x,(y,z)). ((x,y),z)"])

lemma times_singleton_eqpoll: "{a} × A  A"
proof -
  have "{a} × A = (λx. (a,x)) ` A"
    by auto
  also have "   A"
    proof (rule inj_on_image_eqpoll_self)
      show "inj_on (Pair a) A"
        by (auto simp: inj_on_def)
    qed
    finally show ?thesis .
qed

lemma times_lepoll_mono:
  assumes "A  C" "B  D" shows "A × B  C × D"
proof -
  obtain f g where "inj_on f A" "f ` A  C" "inj_on g B" "g ` B  D"
    by (meson assms lepoll_def)
  then show ?thesis
    unfolding lepoll_def
    by (rule_tac x="λ(x,y). (f x, g y)" in exI) (auto simp: inj_on_def)
qed

lemma times_eqpoll_cong: "A  C; B  D  A × B  C × D"
  by (metis eqpoll_imp_lepoll eqpoll_sym lepoll_antisym times_lepoll_mono)

lemma
  assumes "B  {}" shows lepoll_times1: "A  A × B" and lepoll_times2:  "A  B × A"
  using assms lepoll_iff by fastforce+

lemma times_0_eqpoll: "{} × A  {}"
  by (simp add: eqpoll_iff_bijections)

lemma Sigma_inj_lepoll_mono:
  assumes h: "inj_on h A" "h ` A  C" and "x. x  A  B x  D (h x)" 
  shows "Sigma A B  Sigma C D"
proof -
  have "x. x  A  f. inj_on f (B x)  f ` (B x)  D (h x)"
    by (meson assms lepoll_def)
  then obtain f where  "x. x  A  inj_on (f x) (B x)  f x ` B x  D (h x)"
    by metis
  with h show ?thesis
    unfolding lepoll_def inj_on_def
    by (rule_tac x="λ(x,y). (h x, f x y)" in exI) force
qed

lemma Sigma_lepoll_mono:
  assumes "A  C" "x. x  A  B x  D x" shows "Sigma A B  Sigma C D"
  using Sigma_inj_lepoll_mono [of id] assms by auto

lemma sum_times_distrib_eqpoll: "(A <+> B) × C  (A × C) <+> (B × C)"
  unfolding eqpoll_def
proof
  show "bij_betw (λ(x,z). case_sum(λy. Inl(y,z)) (λy. Inr(y,z)) x) ((A <+> B) × C) (A × C <+> B × C)"
    by (rule bij_betw_byWitness [where f' = "case_sum (λ(x,z). (Inl x, z)) (λ(y,z). (Inr y, z))"]) auto
qed

lemma Sigma_eqpoll_cong:
  assumes h: "bij_betw h A C"  and BD: "x. x  A  B x  D (h x)" 
  shows "Sigma A B  Sigma C D"
proof (intro lepoll_antisym)
  show "Sigma A B  Sigma C D"
    by (metis Sigma_inj_lepoll_mono bij_betw_def eqpoll_imp_lepoll subset_refl assms)
  have "inj_on (inv_into A h) C  inv_into A h ` C  A"
    by (metis bij_betw_def bij_betw_inv_into h set_eq_subset)
  then show "Sigma C D  Sigma A B"
    by (smt (verit, best) BD Sigma_inj_lepoll_mono bij_betw_inv_into_right eqpoll_sym h image_subset_iff lepoll_refl lepoll_trans2)
qed

lemma prod_insert_eqpoll:
  assumes "a  A" shows "insert a A × B  B <+> A × B"
  unfolding eqpoll_def
  proof
  show "bij_betw (λ(x,y). if x=a then Inl y else Inr (x,y)) (insert a A × B) (B <+> A × B)"
    by (rule bij_betw_byWitness [where f' = "case_sum (λy. (a,y)) id"]) (auto simp: assms)
qed

subsection‹General Unions›

lemma Union_eqpoll_Times:
  assumes B: "x. x  A  F x  B" and disj: "pairwise (λx y. disjnt (F x) (F y)) A"
  shows "(xA. F x)  A × B"
proof (rule lepoll_antisym)
  obtain b where b: "x. x  A  bij_betw (b x) (F x) B"
    using B unfolding eqpoll_def by metis
  show "(F ` A)  A × B"
    unfolding lepoll_def
  proof (intro exI conjI)
    define χ where "χ  λz. THE x. x  A  z  F x"
    have χ: "χ z = x" if "x  A" "z  F x" for x z
      unfolding χ_def
      apply (rule the_equality)
      apply (simp add: that)
      by (metis disj disjnt_iff pairwiseD that)
    let ?f = "λz. (χ z, b (χ z) z)"
    show "inj_on ?f ((F ` A))"
      unfolding inj_on_def
      by clarify (metis χ b bij_betw_inv_into_left)
    show "?f ` (F ` A)  A × B"
      using χ b bij_betwE by blast
  qed
  show "A × B  (F ` A)"
    unfolding lepoll_def
  proof (intro exI conjI)
    let ?f = "λ(x,y). inv_into (F x) (b x) y"
    have *: "inv_into (F x) (b x) y  F x" if "x  A" "y  B" for x y
      by (metis b bij_betw_imp_surj_on inv_into_into that)
    then show "inj_on ?f (A × B)"
      unfolding inj_on_def
      by clarsimp (metis (mono_tags, lifting) b bij_betw_inv_into_right disj disjnt_iff pairwiseD)
    show "?f ` (A × B)   (F ` A)"
      by clarsimp (metis b bij_betw_imp_surj_on inv_into_into)
  qed
qed

lemma UN_lepoll_UN:
  assumes A: "x. x  A  B x  C x"
    and disj: "pairwise (λx y. disjnt (C x) (C y)) A"
  shows " (B`A)   (C`A)"
proof -
  obtain f where f: "x. x  A  inj_on (f x) (B x)  f x ` (B x)  (C x)"
    using A unfolding lepoll_def by metis
  show ?thesis
    unfolding lepoll_def
  proof (intro exI conjI)
    define χ where "χ  λz. @x. x  A  z  B x"
    have χ: "χ z  A  z  B (χ z)" if "x  A" "z  B x" for x z
      unfolding χ_def by (metis (mono_tags, lifting) someI_ex that)
    let ?f = "λz. (f (χ z) z)"
    show "inj_on ?f ((B ` A))"
      using disj f unfolding inj_on_def disjnt_iff pairwise_def image_subset_iff
      by (metis UN_iff χ)
    show "?f `  (B ` A)   (C ` A)"
      using χ f unfolding image_subset_iff by blast
  qed
qed

lemma UN_eqpoll_UN:
  assumes A: "x. x  A  B x  C x"
    and B: "pairwise (λx y. disjnt (B x) (B y)) A"
    and C: "pairwise (λx y. disjnt (C x) (C y)) A"
  shows "(xA. B x)  (xA. C x)"
proof (rule lepoll_antisym)
  show " (B ` A)   (C ` A)"
    by (meson A C UN_lepoll_UN eqpoll_imp_lepoll)
  show " (C ` A)   (B ` A)"
    by (simp add: A B UN_lepoll_UN eqpoll_imp_lepoll eqpoll_sym)
qed

subsection‹General Cartesian products (Pi)›

lemma PiE_sing_eqpoll_self: "({a} E B)  B"
proof -
  have 1: "x = y"
    if "x  {a} E B" "y  {a} E B" "x a = y a" for x y
    by (metis IntD2 PiE_def extensionalityI singletonD that)
  have 2: "x  (λh. h a) ` ({a} E B)" if "x  B" for x
    using that by (rule_tac x="λz{a}. x" in image_eqI) auto
  show ?thesis
  unfolding eqpoll_def bij_betw_def inj_on_def
  by (force intro: 1 2)
qed

lemma lepoll_funcset_right:
   "B  B'  A E B  A E B'"
  apply (auto simp: lepoll_def inj_on_def)
  apply (rule_tac x = "λg. λz  A. f(g z)" in exI)
  apply (auto simp: fun_eq_iff)
  apply (metis PiE_E)
  by blast

lemma lepoll_funcset_left:
  assumes "B  {}" "A  A'"
  shows "A E B  A' E B"
proof -
  obtain b where "b  B"
    using assms by blast
  obtain f where "inj_on f A" and fim: "f ` A  A'"
    using assms by (auto simp: lepoll_def)
  then obtain h where h: "x. x  A  h (f x) = x"
    using the_inv_into_f_f by fastforce
  let ?F = "λg. λu  A'. if h u  A then g(h u) else b"
  show ?thesis
    unfolding lepoll_def inj_on_def
  proof (intro exI conjI ballI impI ext)
    fix k l x
    assume k: "k  A E B" and l: "l  A E B" and "?F k = ?F l"
    then have "?F k (f x) = ?F l (f x)"
      by simp
    then show "k x = l x"
      apply (auto simp: h split: if_split_asm)
      apply (metis PiE_arb h k l)
      apply (metis (full_types) PiE_E h k l)
      using fim k l by fastforce
  next
    show "?F ` (A E B)  A' E B"
      using b  B by force
  qed
qed

lemma lepoll_funcset:
   "B  {}; A  A'; B  B'  A E B  A' E B'"
  by (rule lepoll_trans [OF lepoll_funcset_right lepoll_funcset_left]) auto

lemma lepoll_PiE:
  assumes "i. i  A  B i  C i"
  shows "PiE A B  PiE A C"
proof -
  obtain f where f: "i. i  A  inj_on (f i) (B i)  (f i) ` B i  C i"
    using assms unfolding lepoll_def by metis
  then show ?thesis
    unfolding lepoll_def
    apply (rule_tac x = "λg. λi  A. f i (g i)" in exI)
    apply (auto simp: inj_on_def)
     apply (rule PiE_ext, auto)
     apply (metis (full_types) PiE_mem restrict_apply')
    by blast
qed


lemma card_le_PiE_subindex:
  assumes "A  A'" "PiE A' B  {}"
  shows "PiE A B  PiE A' B"
proof -
  have "x. x  A'  y. y  B x"
    using assms by blast
  then obtain g where g: "x. x  A'  g x  B x"
    by metis
  let ?F = "λf x. if x  A then f x else if x  A' then g x else undefined"
  have "PiE A B  (λf. restrict f A) ` PiE A' B"
  proof
    show "f  PiE A B  f  (λf. restrict f A) ` PiE A' B" for f
      using A  A'
      by (rule_tac x="?F f" in image_eqI) (auto simp: g fun_eq_iff)
  qed
  then have "PiE A B  (λf. λi  A. f i) ` PiE A' B"
    by (simp add: subset_imp_lepoll)
  also have "  PiE A' B"
    by (rule image_lepoll)
  finally show ?thesis .
qed


lemma finite_restricted_funspace:
  assumes "finite A" "finite B"
  shows "finite {f. f ` A  B  {x. f x  k x}  A}" (is "finite ?F")
proof (rule finite_subset)
  show "finite ((λU x. if y. (x,y)  U then @y. (x,y)  U else k x) ` Pow(A × B))" (is "finite ?G")
    using assms by auto
  show "?F  ?G"
  proof
    fix f
    assume "f  ?F"
    then show "f  ?G"
      by (rule_tac x="(λx. (x,f x)) ` {x. f x  k x}" in image_eqI) (auto simp: fun_eq_iff image_def)
  qed
qed


proposition finite_PiE_iff:
   "finite(PiE I S)  PiE I S = {}  finite {i  I. ~(a. S i  {a})}  (i  I. finite(S i))"
 (is "?lhs = ?rhs")
proof (cases "PiE I S = {}")
  case False
  define J where "J  {i  I. a. S i  {a}}"
  show ?thesis
  proof
    assume L: ?lhs
    have "infinite (PiE I S)" if "infinite J"
    proof -
      have "(UNIV::nat set)  (UNIV::(natbool) set)"
      proof -
        have "N::nat set. inj_on (=) N"
          by (simp add: inj_on_def)
        then show ?thesis
          by (meson infinite_iff_countable_subset infinite_le_lepoll top.extremum)
      qed
      also have " = (UNIV::nat set) E (UNIV::bool set)"
        by auto
      also have "  J E (UNIV::bool set)"
        apply (rule lepoll_funcset_left)
        using infinite_le_lepoll that by auto
      also have "  PiE J S"
      proof -
        have *: "(UNIV::bool set)  S i" if "i  I" and "a. ¬ S i  {a}" for i
        proof -
          obtain a b where "{a,b}  S i" "a  b"
            by (metis a. ¬ S i  {a} all_not_in_conv empty_subsetI insertCI insert_subset set_eq_subset subsetI)
          then show ?thesis
            apply (clarsimp simp: lepoll_def inj_on_def)
            apply (rule_tac x="λx. if x then a else b" in exI, auto)
            done
        qed
        show ?thesis
          by (auto simp: * J_def intro: lepoll_PiE)
      qed
      also have "  PiE I S"
        using False by (auto simp: J_def intro: card_le_PiE_subindex)
      finally have "(UNIV::nat set)  PiE I S" .
      then show ?thesis
        by (simp add: infinite_le_lepoll)
    qed
    moreover have "finite (S i)" if "i  I" for i
    proof (rule finite_subset)
      obtain f where f: "f  PiE I S"
        using False by blast
      show "S i  (λf. f i) ` PiE I S"
      proof
        show "s  (λf. f i) ` PiE I S" if "s  S i" for s
          using that f i  I
          by (rule_tac x="λj. if j = i then s else f j" in image_eqI) auto
      qed
    next
      show "finite ((λx. x i) ` PiE I S)"
        using L by blast
    qed
    ultimately show ?rhs
      using L
      by (auto simp: J_def False)
  next
    assume R: ?rhs
    have "i  I - J. a. S i = {a}"
      using False J_def by blast
    then obtain a where a: "i  I - J. S i = {a i}"
      by metis
    let ?F = "{f. f ` J  (i  J. S i)  {i. f i  (if i  I then a i else undefined)}  J}"
    have *: "finite (PiE I S)"
      if "finite J" and "iI. finite (S i)"
    proof (rule finite_subset)
      show "PiE I S  ?F"
        apply safe
        using J_def apply blast
        by (metis DiffI PiE_E a singletonD)
      show "finite ?F"
      proof (rule finite_restricted_funspace [OF finite J])
        show "finite ( (S ` J))"
          using that J_def by blast
      qed
  qed
  show ?lhs
      using R by (auto simp: * J_def)
  qed
qed auto


corollary finite_funcset_iff:
  "finite(I E S)  (a. S  {a})  I = {}  finite I  finite S"
  by (fastforce simp: finite_PiE_iff PiE_eq_empty_iff dest: subset_singletonD)

subsection ‹Misc other resultd›

lemma lists_lepoll_mono:
  assumes "A  B" shows "lists A  lists B"
proof -
  obtain f where f: "inj_on f A" "f ` A  B"
    by (meson assms lepoll_def)
  moreover have "inj_on (map f) (lists A)"
    using f unfolding inj_on_def
    by clarsimp (metis list.inj_map_strong)
  ultimately show ?thesis
    unfolding lepoll_def by force
qed

lemma lepoll_lists: "A  lists A"
  unfolding lepoll_def inj_on_def by(rule_tac x="λx. [x]" in exI) auto

text ‹Dedekind's definition of infinite set›

lemma infinite_iff_psubset: "infinite A  (B. B  A  AB)"
proof
  assume "infinite A"
  then obtain f :: "nat  'a" where "inj f" and f: "range f  A"
    by (meson infinite_countable_subset)
  define C where "C  A - range f"
  have C: "A = range f  C" "range f  C = {}"
    using f by (auto simp: C_def)
  have *: "range (f  Suc)  range f"
    using inj_eq [OF inj f] by (fastforce simp: set_eq_iff)
  have "range f  C  range (f  Suc)  C"
  proof (intro Un_eqpoll_cong)
    show "range f  range (f  Suc)"
      by (meson inj f eqpoll_refl inj_Suc inj_compose inj_on_image_eqpoll_2)
    show "disjnt (range f) C"
      by (simp add: C disjnt_def)
    then show "disjnt (range (f  Suc)) C"
      using "*" disjnt_subset1 by blast
  qed auto
  moreover have "range (f  Suc)  C  A"
    using "*" f C_def by blast
  ultimately show "BA. A  B"
    by (metis C(1))
next
  assume "BA. A  B" then show "infinite A"
    by (metis card_subset_eq eqpoll_finite_iff eqpoll_iff_card psubsetE)
qed

lemma infinite_iff_psubset_le: "infinite A  (B. B  A  A  B)"
  by (meson eqpoll_imp_lepoll infinite_iff_psubset lepoll_antisym psubsetE subset_imp_lepoll)

end