src/HOL/Library/Equipollence.thy
 author haftmann Fri Mar 22 19:18:08 2019 +0000 (3 months ago) changeset 69946 494934c30f38 parent 69874 11065b70407d permissions -rw-r--r--
improved code equations taken over from AFP
```     1 section \<open>Equipollence and Other Relations Connected with Cardinality\<close>
```
```     2
```
```     3 theory "Equipollence"
```
```     4   imports FuncSet
```
```     5 begin
```
```     6
```
```     7 subsection\<open>Eqpoll\<close>
```
```     8
```
```     9 definition eqpoll :: "'a set \<Rightarrow> 'b set \<Rightarrow> bool" (infixl "\<approx>" 50)
```
```    10   where "eqpoll A B \<equiv> \<exists>f. bij_betw f A B"
```
```    11
```
```    12 definition lepoll :: "'a set \<Rightarrow> 'b set \<Rightarrow> bool" (infixl "\<lesssim>" 50)
```
```    13   where "lepoll A B \<equiv> \<exists>f. inj_on f A \<and> f ` A \<subseteq> B"
```
```    14
```
```    15 definition lesspoll :: "'a set \<Rightarrow> 'b set \<Rightarrow> bool" (infixl \<open>\<prec>\<close> 50)
```
```    16   where "A \<prec> B == A \<lesssim> B \<and> ~(A \<approx> B)"
```
```    17
```
```    18 lemma lepoll_empty_iff_empty [simp]: "A \<lesssim> {} \<longleftrightarrow> A = {}"
```
```    19   by (auto simp: lepoll_def)
```
```    20
```
```    21 lemma eqpoll_iff_card_of_ordIso: "A \<approx> B \<longleftrightarrow> ordIso2 (card_of A) (card_of B)"
```
```    22   by (simp add: card_of_ordIso eqpoll_def)
```
```    23
```
```    24 lemma eqpoll_finite_iff: "A \<approx> B \<Longrightarrow> finite A \<longleftrightarrow> finite B"
```
```    25   by (meson bij_betw_finite eqpoll_def)
```
```    26
```
```    27 lemma eqpoll_iff_card:
```
```    28   assumes "finite A" "finite B"
```
```    29   shows  "A \<approx> B \<longleftrightarrow> card A = card B"
```
```    30   using assms by (auto simp: bij_betw_iff_card eqpoll_def)
```
```    31
```
```    32 lemma lepoll_antisym:
```
```    33   assumes "A \<lesssim> B" "B \<lesssim> A" shows "A \<approx> B"
```
```    34   using assms unfolding eqpoll_def lepoll_def by (metis Schroeder_Bernstein)
```
```    35
```
```    36 lemma lepoll_trans [trans]: "\<lbrakk>A \<lesssim> B; B \<lesssim> C\<rbrakk> \<Longrightarrow> A \<lesssim> C"
```
```    37   apply (clarsimp simp: lepoll_def)
```
```    38   apply (rename_tac f g)
```
```    39   apply (rule_tac x="g \<circ> f" in exI)
```
```    40   apply (auto simp: image_subset_iff inj_on_def)
```
```    41   done
```
```    42
```
```    43 lemma lepoll_trans1 [trans]: "\<lbrakk>A \<approx> B; B \<lesssim> C\<rbrakk> \<Longrightarrow> A \<lesssim> C"
```
```    44   by (meson card_of_ordLeq eqpoll_iff_card_of_ordIso lepoll_def lepoll_trans ordIso_iff_ordLeq)
```
```    45
```
```    46 lemma lepoll_trans2 [trans]: "\<lbrakk>A \<lesssim> B; B \<approx> C\<rbrakk> \<Longrightarrow> A \<lesssim> C"
```
```    47   apply (clarsimp simp: eqpoll_def lepoll_def bij_betw_def)
```
```    48   apply (rename_tac f g)
```
```    49   apply (rule_tac x="g \<circ> f" in exI)
```
```    50   apply (auto simp: image_subset_iff inj_on_def)
```
```    51   done
```
```    52
```
```    53 lemma eqpoll_sym: "A \<approx> B \<Longrightarrow> B \<approx> A"
```
```    54   unfolding eqpoll_def
```
```    55   using bij_betw_the_inv_into by auto
```
```    56
```
```    57 lemma eqpoll_trans [trans]: "\<lbrakk>A \<approx> B; B \<approx> C\<rbrakk> \<Longrightarrow> A \<approx> C"
```
```    58   unfolding eqpoll_def using bij_betw_trans by blast
```
```    59
```
```    60 lemma eqpoll_imp_lepoll: "A \<approx> B \<Longrightarrow> A \<lesssim> B"
```
```    61   unfolding eqpoll_def lepoll_def by (metis bij_betw_def order_refl)
```
```    62
```
```    63 lemma subset_imp_lepoll: "A \<subseteq> B \<Longrightarrow> A \<lesssim> B"
```
```    64   by (force simp: lepoll_def)
```
```    65
```
```    66 lemma lepoll_iff: "A \<lesssim> B \<longleftrightarrow> (\<exists>g. A \<subseteq> g ` B)"
```
```    67   unfolding lepoll_def
```
```    68 proof safe
```
```    69   fix g assume "A \<subseteq> g ` B"
```
```    70   then show "\<exists>f. inj_on f A \<and> f ` A \<subseteq> B"
```
```    71     by (rule_tac x="inv_into B g" in exI) (auto simp: inv_into_into inj_on_inv_into)
```
```    72 qed (metis image_mono the_inv_into_onto)
```
```    73
```
```    74 lemma subset_image_lepoll: "B \<subseteq> f ` A \<Longrightarrow> B \<lesssim> A"
```
```    75   by (auto simp: lepoll_iff)
```
```    76
```
```    77 lemma image_lepoll: "f ` A \<lesssim> A"
```
```    78   by (auto simp: lepoll_iff)
```
```    79
```
```    80 lemma infinite_le_lepoll: "infinite A \<longleftrightarrow> (UNIV::nat set) \<lesssim> A"
```
```    81 apply (auto simp: lepoll_def)
```
```    82   apply (simp add: infinite_countable_subset)
```
```    83   using infinite_iff_countable_subset by blast
```
```    84
```
```    85 lemma bij_betw_iff_bijections:
```
```    86   "bij_betw f A B \<longleftrightarrow> (\<exists>g. (\<forall>x \<in> A. f x \<in> B \<and> g(f x) = x) \<and> (\<forall>y \<in> B. g y \<in> A \<and> f(g y) = y))"
```
```    87   (is "?lhs = ?rhs")
```
```    88 proof
```
```    89   assume L: ?lhs
```
```    90   then show ?rhs
```
```    91     apply (rule_tac x="the_inv_into A f" in exI)
```
```    92     apply (auto simp: bij_betw_def f_the_inv_into_f the_inv_into_f_f the_inv_into_into)
```
```    93     done
```
```    94 next
```
```    95   assume ?rhs
```
```    96   then show ?lhs
```
```    97     by (auto simp: bij_betw_def inj_on_def image_def; metis)
```
```    98 qed
```
```    99
```
```   100 lemma eqpoll_iff_bijections:
```
```   101    "A \<approx> B \<longleftrightarrow> (\<exists>f g. (\<forall>x \<in> A. f x \<in> B \<and> g(f x) = x) \<and> (\<forall>y \<in> B. g y \<in> A \<and> f(g y) = y))"
```
```   102     by (auto simp: eqpoll_def bij_betw_iff_bijections)
```
```   103
```
```   104 lemma lepoll_restricted_funspace:
```
```   105    "{f. f ` A \<subseteq> B \<and> {x. f x \<noteq> k x} \<subseteq> A \<and> finite {x. f x \<noteq> k x}} \<lesssim> Fpow (A \<times> B)"
```
```   106 proof -
```
```   107   have *: "\<exists>U \<in> Fpow (A \<times> B). f = (\<lambda>x. if \<exists>y. (x, y) \<in> U then SOME y. (x,y) \<in> U else k x)"
```
```   108     if "f ` A \<subseteq> B" "{x. f x \<noteq> k x} \<subseteq> A" "finite {x. f x \<noteq> k x}" for f
```
```   109     apply (rule_tac x="(\<lambda>x. (x, f x)) ` {x. f x \<noteq> k x}" in bexI)
```
```   110     using that by (auto simp: image_def Fpow_def)
```
```   111   show ?thesis
```
```   112     apply (rule subset_image_lepoll [where f = "\<lambda>U x. if \<exists>y. (x,y) \<in> U then @y. (x,y) \<in> U else k x"])
```
```   113     using * by (auto simp: image_def)
```
```   114 qed
```
```   115
```
```   116 lemma singleton_lepoll: "{x} \<lesssim> insert y A"
```
```   117   by (force simp: lepoll_def)
```
```   118
```
```   119 lemma singleton_eqpoll: "{x} \<approx> {y}"
```
```   120   by (blast intro: lepoll_antisym singleton_lepoll)
```
```   121
```
```   122 lemma subset_singleton_iff_lepoll: "(\<exists>x. S \<subseteq> {x}) \<longleftrightarrow> S \<lesssim> {()}"
```
```   123 proof safe
```
```   124   show "S \<lesssim> {()}" if "S \<subseteq> {x}" for x
```
```   125     using subset_imp_lepoll [OF that] by (simp add: singleton_eqpoll lepoll_trans2)
```
```   126   show "\<exists>x. S \<subseteq> {x}" if "S \<lesssim> {()}"
```
```   127   by (metis (no_types, hide_lams) image_empty image_insert lepoll_iff that)
```
```   128 qed
```
```   129
```
```   130
```
```   131 subsection\<open>The strict relation\<close>
```
```   132
```
```   133 lemma lesspoll_not_refl [iff]: "~ (i \<prec> i)"
```
```   134   by (simp add: lepoll_antisym lesspoll_def)
```
```   135
```
```   136 lemma lesspoll_imp_lepoll: "A \<prec> B ==> A \<lesssim> B"
```
```   137 by (unfold lesspoll_def, blast)
```
```   138
```
```   139 lemma lepoll_iff_leqpoll: "A \<lesssim> B \<longleftrightarrow> A \<prec> B | A \<approx> B"
```
```   140   using eqpoll_imp_lepoll lesspoll_def by blast
```
```   141
```
```   142 lemma lesspoll_trans [trans]: "\<lbrakk>X \<prec> Y; Y \<prec> Z\<rbrakk> \<Longrightarrow> X \<prec> Z"
```
```   143   by (meson eqpoll_sym lepoll_antisym lepoll_trans lepoll_trans1 lesspoll_def)
```
```   144
```
```   145 lemma lesspoll_trans1 [trans]: "\<lbrakk>X \<lesssim> Y; Y \<prec> Z\<rbrakk> \<Longrightarrow> X \<prec> Z"
```
```   146   by (meson eqpoll_sym lepoll_antisym lepoll_trans lepoll_trans1 lesspoll_def)
```
```   147
```
```   148 lemma lesspoll_trans2 [trans]: "\<lbrakk>X \<prec> Y; Y \<lesssim> Z\<rbrakk> \<Longrightarrow> X \<prec> Z"
```
```   149   by (meson eqpoll_imp_lepoll eqpoll_sym lepoll_antisym lepoll_trans lesspoll_def)
```
```   150
```
```   151 lemma eq_lesspoll_trans [trans]: "\<lbrakk>X \<approx> Y; Y \<prec> Z\<rbrakk> \<Longrightarrow> X \<prec> Z"
```
```   152   using eqpoll_imp_lepoll lesspoll_trans1 by blast
```
```   153
```
```   154 lemma lesspoll_eq_trans [trans]: "\<lbrakk>X \<prec> Y; Y \<approx> Z\<rbrakk> \<Longrightarrow> X \<prec> Z"
```
```   155   using eqpoll_imp_lepoll lesspoll_trans2 by blast
```
```   156
```
```   157 subsection\<open>Cartesian products\<close>
```
```   158
```
```   159 lemma PiE_sing_eqpoll_self: "({a} \<rightarrow>\<^sub>E B) \<approx> B"
```
```   160 proof -
```
```   161   have 1: "x = y"
```
```   162     if "x \<in> {a} \<rightarrow>\<^sub>E B" "y \<in> {a} \<rightarrow>\<^sub>E B" "x a = y a" for x y
```
```   163     by (metis IntD2 PiE_def extensionalityI singletonD that)
```
```   164   have 2: "x \<in> (\<lambda>h. h a) ` ({a} \<rightarrow>\<^sub>E B)" if "x \<in> B" for x
```
```   165     using that by (rule_tac x="\<lambda>z\<in>{a}. x" in image_eqI) auto
```
```   166   show ?thesis
```
```   167   unfolding eqpoll_def bij_betw_def inj_on_def
```
```   168   by (force intro: 1 2)
```
```   169 qed
```
```   170
```
```   171 lemma lepoll_funcset_right:
```
```   172    "B \<lesssim> B' \<Longrightarrow> A \<rightarrow>\<^sub>E B \<lesssim> A \<rightarrow>\<^sub>E B'"
```
```   173   apply (auto simp: lepoll_def inj_on_def)
```
```   174   apply (rule_tac x = "\<lambda>g. \<lambda>z \<in> A. f(g z)" in exI)
```
```   175   apply (auto simp: fun_eq_iff)
```
```   176   apply (metis PiE_E)
```
```   177   by blast
```
```   178
```
```   179 lemma lepoll_funcset_left:
```
```   180   assumes "B \<noteq> {}" "A \<lesssim> A'"
```
```   181   shows "A \<rightarrow>\<^sub>E B \<lesssim> A' \<rightarrow>\<^sub>E B"
```
```   182 proof -
```
```   183   obtain b where "b \<in> B"
```
```   184     using assms by blast
```
```   185   obtain f where "inj_on f A" and fim: "f ` A \<subseteq> A'"
```
```   186     using assms by (auto simp: lepoll_def)
```
```   187   then obtain h where h: "\<And>x. x \<in> A \<Longrightarrow> h (f x) = x"
```
```   188     using the_inv_into_f_f by fastforce
```
```   189   let ?F = "\<lambda>g. \<lambda>u \<in> A'. if h u \<in> A then g(h u) else b"
```
```   190   show ?thesis
```
```   191     unfolding lepoll_def inj_on_def
```
```   192   proof (intro exI conjI ballI impI ext)
```
```   193     fix k l x
```
```   194     assume k: "k \<in> A \<rightarrow>\<^sub>E B" and l: "l \<in> A \<rightarrow>\<^sub>E B" and "?F k = ?F l"
```
```   195     then have "?F k (f x) = ?F l (f x)"
```
```   196       by simp
```
```   197     then show "k x = l x"
```
```   198       apply (auto simp: h split: if_split_asm)
```
```   199       apply (metis PiE_arb h k l)
```
```   200       apply (metis (full_types) PiE_E h k l)
```
```   201       using fim k l by fastforce
```
```   202   next
```
```   203     show "?F ` (A \<rightarrow>\<^sub>E B) \<subseteq> A' \<rightarrow>\<^sub>E B"
```
```   204       using \<open>b \<in> B\<close> by force
```
```   205   qed
```
```   206 qed
```
```   207
```
```   208 lemma lepoll_funcset:
```
```   209    "\<lbrakk>B \<noteq> {}; A \<lesssim> A'; B \<lesssim> B'\<rbrakk> \<Longrightarrow> A \<rightarrow>\<^sub>E B \<lesssim> A' \<rightarrow>\<^sub>E B'"
```
```   210   by (rule lepoll_trans [OF lepoll_funcset_right lepoll_funcset_left]) auto
```
```   211
```
```   212 lemma lepoll_PiE:
```
```   213   assumes "\<And>i. i \<in> A \<Longrightarrow> B i \<lesssim> C i"
```
```   214   shows "PiE A B \<lesssim> PiE A C"
```
```   215 proof -
```
```   216   obtain f where f: "\<And>i. i \<in> A \<Longrightarrow> inj_on (f i) (B i) \<and> (f i) ` B i \<subseteq> C i"
```
```   217     using assms unfolding lepoll_def by metis
```
```   218   then show ?thesis
```
```   219     unfolding lepoll_def
```
```   220     apply (rule_tac x = "\<lambda>g. \<lambda>i \<in> A. f i (g i)" in exI)
```
```   221     apply (auto simp: inj_on_def)
```
```   222      apply (rule PiE_ext, auto)
```
```   223      apply (metis (full_types) PiE_mem restrict_apply')
```
```   224     by blast
```
```   225 qed
```
```   226
```
```   227
```
```   228 lemma card_le_PiE_subindex:
```
```   229   assumes "A \<subseteq> A'" "Pi\<^sub>E A' B \<noteq> {}"
```
```   230   shows "PiE A B \<lesssim> PiE A' B"
```
```   231 proof -
```
```   232   have "\<And>x. x \<in> A' \<Longrightarrow> \<exists>y. y \<in> B x"
```
```   233     using assms by blast
```
```   234   then obtain g where g: "\<And>x. x \<in> A' \<Longrightarrow> g x \<in> B x"
```
```   235     by metis
```
```   236   let ?F = "\<lambda>f x. if x \<in> A then f x else if x \<in> A' then g x else undefined"
```
```   237   have "Pi\<^sub>E A B \<subseteq> (\<lambda>f. restrict f A) ` Pi\<^sub>E A' B"
```
```   238   proof
```
```   239     show "f \<in> Pi\<^sub>E A B \<Longrightarrow> f \<in> (\<lambda>f. restrict f A) ` Pi\<^sub>E A' B" for f
```
```   240       using \<open>A \<subseteq> A'\<close>
```
```   241       by (rule_tac x="?F f" in image_eqI) (auto simp: g fun_eq_iff)
```
```   242   qed
```
```   243   then have "Pi\<^sub>E A B \<lesssim> (\<lambda>f. \<lambda>i \<in> A. f i) ` Pi\<^sub>E A' B"
```
```   244     by (simp add: subset_imp_lepoll)
```
```   245   also have "\<dots> \<lesssim> PiE A' B"
```
```   246     by (rule image_lepoll)
```
```   247   finally show ?thesis .
```
```   248 qed
```
```   249
```
```   250
```
```   251 lemma finite_restricted_funspace:
```
```   252   assumes "finite A" "finite B"
```
```   253   shows "finite {f. f ` A \<subseteq> B \<and> {x. f x \<noteq> k x} \<subseteq> A}" (is "finite ?F")
```
```   254 proof (rule finite_subset)
```
```   255   show "finite ((\<lambda>U x. if \<exists>y. (x,y) \<in> U then @y. (x,y) \<in> U else k x) ` Pow(A \<times> B))" (is "finite ?G")
```
```   256     using assms by auto
```
```   257   show "?F \<subseteq> ?G"
```
```   258   proof
```
```   259     fix f
```
```   260     assume "f \<in> ?F"
```
```   261     then show "f \<in> ?G"
```
```   262       by (rule_tac x="(\<lambda>x. (x,f x)) ` {x. f x \<noteq> k x}" in image_eqI) (auto simp: fun_eq_iff image_def)
```
```   263   qed
```
```   264 qed
```
```   265
```
```   266
```
```   267 proposition finite_PiE_iff:
```
```   268    "finite(PiE I S) \<longleftrightarrow> PiE I S = {} \<or> finite {i \<in> I. ~(\<exists>a. S i \<subseteq> {a})} \<and> (\<forall>i \<in> I. finite(S i))"
```
```   269  (is "?lhs = ?rhs")
```
```   270 proof (cases "PiE I S = {}")
```
```   271   case False
```
```   272   define J where "J \<equiv> {i \<in> I. \<nexists>a. S i \<subseteq> {a}}"
```
```   273   show ?thesis
```
```   274   proof
```
```   275     assume L: ?lhs
```
```   276     have "infinite (Pi\<^sub>E I S)" if "infinite J"
```
```   277     proof -
```
```   278       have "(UNIV::nat set) \<lesssim> (UNIV::(nat\<Rightarrow>bool) set)"
```
```   279       proof -
```
```   280         have "\<forall>N::nat set. inj_on (=) N"
```
```   281           by (simp add: inj_on_def)
```
```   282         then show ?thesis
```
```   283           by (meson infinite_iff_countable_subset infinite_le_lepoll top.extremum)
```
```   284       qed
```
```   285       also have "\<dots> = (UNIV::nat set) \<rightarrow>\<^sub>E (UNIV::bool set)"
```
```   286         by auto
```
```   287       also have "\<dots> \<lesssim> J \<rightarrow>\<^sub>E (UNIV::bool set)"
```
```   288         apply (rule lepoll_funcset_left)
```
```   289         using infinite_le_lepoll that by auto
```
```   290       also have "\<dots> \<lesssim> Pi\<^sub>E J S"
```
```   291       proof -
```
```   292         have *: "(UNIV::bool set) \<lesssim> S i" if "i \<in> I" and "\<forall>a. \<not> S i \<subseteq> {a}" for i
```
```   293         proof -
```
```   294           obtain a b where "{a,b} \<subseteq> S i" "a \<noteq> b"
```
```   295             by (metis \<open>\<forall>a. \<not> S i \<subseteq> {a}\<close> all_not_in_conv empty_subsetI insertCI insert_subset set_eq_subset subsetI)
```
```   296           then show ?thesis
```
```   297             apply (clarsimp simp: lepoll_def inj_on_def)
```
```   298             apply (rule_tac x="\<lambda>x. if x then a else b" in exI, auto)
```
```   299             done
```
```   300         qed
```
```   301         show ?thesis
```
```   302           by (auto simp: * J_def intro: lepoll_PiE)
```
```   303       qed
```
```   304       also have "\<dots> \<lesssim> Pi\<^sub>E I S"
```
```   305         using False by (auto simp: J_def intro: card_le_PiE_subindex)
```
```   306       finally have "(UNIV::nat set) \<lesssim> Pi\<^sub>E I S" .
```
```   307       then show ?thesis
```
```   308         by (simp add: infinite_le_lepoll)
```
```   309     qed
```
```   310     moreover have "finite (S i)" if "i \<in> I" for i
```
```   311     proof (rule finite_subset)
```
```   312       obtain f where f: "f \<in> PiE I S"
```
```   313         using False by blast
```
```   314       show "S i \<subseteq> (\<lambda>f. f i) ` Pi\<^sub>E I S"
```
```   315       proof
```
```   316         show "s \<in> (\<lambda>f. f i) ` Pi\<^sub>E I S" if "s \<in> S i" for s
```
```   317           using that f \<open>i \<in> I\<close>
```
```   318           by (rule_tac x="\<lambda>j. if j = i then s else f j" in image_eqI) auto
```
```   319       qed
```
```   320     next
```
```   321       show "finite ((\<lambda>x. x i) ` Pi\<^sub>E I S)"
```
```   322         using L by blast
```
```   323     qed
```
```   324     ultimately show ?rhs
```
```   325       using L
```
```   326       by (auto simp: J_def False)
```
```   327   next
```
```   328     assume R: ?rhs
```
```   329     have "\<forall>i \<in> I - J. \<exists>a. S i = {a}"
```
```   330       using False J_def by blast
```
```   331     then obtain a where a: "\<forall>i \<in> I - J. S i = {a i}"
```
```   332       by metis
```
```   333     let ?F = "{f. f ` J \<subseteq> (\<Union>i \<in> J. S i) \<and> {i. f i \<noteq> (if i \<in> I then a i else undefined)} \<subseteq> J}"
```
```   334     have *: "finite (Pi\<^sub>E I S)"
```
```   335       if "finite J" and "\<forall>i\<in>I. finite (S i)"
```
```   336     proof (rule finite_subset)
```
```   337       show "Pi\<^sub>E I S \<subseteq> ?F"
```
```   338         apply safe
```
```   339         using J_def apply blast
```
```   340         by (metis DiffI PiE_E a singletonD)
```
```   341       show "finite ?F"
```
```   342       proof (rule finite_restricted_funspace [OF \<open>finite J\<close>])
```
```   343         show "finite (\<Union> (S ` J))"
```
```   344           using that J_def by blast
```
```   345       qed
```
```   346   qed
```
```   347   show ?lhs
```
```   348       using R by (auto simp: * J_def)
```
```   349   qed
```
```   350 qed auto
```
```   351
```
```   352
```
```   353 corollary finite_funcset_iff:
```
```   354   "finite(I \<rightarrow>\<^sub>E S) \<longleftrightarrow> (\<exists>a. S \<subseteq> {a}) \<or> I = {} \<or> finite I \<and> finite S"
```
```   355   apply (auto simp: finite_PiE_iff PiE_eq_empty_iff dest: not_finite_existsD)
```
```   356   using finite.simps by auto
```
```   357
```
```   358 end
```