author paulson Wed May 20 15:00:25 2020 +0100 (11 days ago) changeset 71848 3c7852327787 parent 71847 da12452c9be2 child 71849 265bbad3d6af
A few new theorems, plus some tidying up
 src/HOL/Library/Countable_Set.thy file | annotate | diff | revisions src/HOL/Library/Nat_Bijection.thy file | annotate | diff | revisions src/HOL/Library/Ramsey.thy file | annotate | diff | revisions src/HOL/List.thy file | annotate | diff | revisions src/HOL/Set.thy file | annotate | diff | revisions
```     1.1 --- a/src/HOL/Library/Countable_Set.thy	Wed May 20 08:33:53 2020 +0200
1.2 +++ b/src/HOL/Library/Countable_Set.thy	Wed May 20 15:00:25 2020 +0100
1.3 @@ -319,8 +319,12 @@
1.4    "countable T \<Longrightarrow> countable {A. finite A \<and> A \<subseteq> T}"
1.5    unfolding Collect_finite_subset_eq_lists by auto
1.6
1.7 +lemma countable_Fpow: "countable S \<Longrightarrow> countable (Fpow S)"
1.8 +  using countable_Collect_finite_subset
1.9 +  by (force simp add: Fpow_def conj_commute)
1.10 +
1.11  lemma countable_set_option [simp]: "countable (set_option x)"
1.12 -by(cases x) auto
1.13 +  by (cases x) auto
1.14
1.15  subsection \<open>Misc lemmas\<close>
1.16
1.17 @@ -420,4 +424,27 @@
1.18  lemma countable_Diff_eq [simp]: "countable (A - {x}) = countable A"
1.19    by (meson countable_Diff countable_empty countable_insert uncountable_minus_countable)
1.20
1.21 +text \<open>Every infinite set can be covered by a pairwise disjoint family of infinite sets.
1.22 +      This version doesn't achieve equality, as it only covers a countable subset\<close>
1.23 +lemma infinite_infinite_partition:
1.24 +  assumes "infinite A"
1.25 +  obtains C :: "nat \<Rightarrow> 'a set"
1.26 +    where "pairwise (\<lambda>i j. disjnt (C i) (C j)) UNIV" "(\<Union>i. C i) \<subseteq> A" "\<And>i. infinite (C i)"
1.27 +proof -
1.28 +  obtain f :: "nat\<Rightarrow>'a" where "range f \<subseteq> A" "inj f"
1.29 +    using assms infinite_countable_subset by blast
1.30 +  let ?C = "\<lambda>i. range (\<lambda>j. f (prod_encode (i,j)))"
1.31 +  show thesis
1.32 +  proof
1.33 +    show "pairwise (\<lambda>i j. disjnt (?C i) (?C j)) UNIV"
1.34 +      by (auto simp: pairwise_def disjnt_def inj_on_eq_iff [OF \<open>inj f\<close>] inj_on_eq_iff [OF inj_prod_encode, of _ UNIV])
1.35 +    show "(\<Union>i. ?C i) \<subseteq> A"
1.36 +      using \<open>range f \<subseteq> A\<close> by blast
1.37 +    have "infinite (range (\<lambda>j. f (prod_encode (i, j))))" for i
1.38 +      by (rule range_inj_infinite) (meson Pair_inject \<open>inj f\<close> inj_def prod_encode_eq)
1.39 +    then show "\<And>i. infinite (?C i)"
1.40 +      using that by auto
1.41 +  qed
1.42 +qed
1.43 +
1.44  end
```
```     2.1 --- a/src/HOL/Library/Nat_Bijection.thy	Wed May 20 08:33:53 2020 +0200
2.2 +++ b/src/HOL/Library/Nat_Bijection.thy	Wed May 20 15:00:25 2020 +0100
2.3 @@ -40,29 +40,34 @@
2.4    where "prod_decode = prod_decode_aux 0"
2.5
2.6  lemma prod_encode_prod_decode_aux: "prod_encode (prod_decode_aux k m) = triangle k + m"
2.7 -  apply (induct k m rule: prod_decode_aux.induct)
2.8 -  apply (subst prod_decode_aux.simps)
2.9 -  apply (simp add: prod_encode_def)
2.10 -  done
2.11 +proof (induction k m rule: prod_decode_aux.induct)
2.12 +  case (1 k m)
2.13 +  then show ?case
2.14 +    by (simp add: prod_encode_def prod_decode_aux.simps)
2.15 +qed
2.16
2.17  lemma prod_decode_inverse [simp]: "prod_encode (prod_decode n) = n"
2.18    by (simp add: prod_decode_def prod_encode_prod_decode_aux)
2.19
2.20  lemma prod_decode_triangle_add: "prod_decode (triangle k + m) = prod_decode_aux k m"
2.21 -  apply (induct k arbitrary: m)
2.22 -   apply (simp add: prod_decode_def)
2.23 -  apply (simp only: triangle_Suc add.assoc)
2.24 -  apply (subst prod_decode_aux.simps)
2.25 -  apply simp
2.26 -  done
2.27 +proof (induct k arbitrary: m)
2.28 +  case 0
2.29 +  then show ?case
2.30 +    by (simp add: prod_decode_def)
2.31 +next
2.32 +  case (Suc k)
2.33 +  then show ?case
2.35 +qed
2.36 +
2.37
2.38  lemma prod_encode_inverse [simp]: "prod_decode (prod_encode x) = x"
2.39    unfolding prod_encode_def
2.40 -  apply (induct x)
2.42 -  apply (subst prod_decode_aux.simps)
2.43 -  apply simp
2.44 -  done
2.45 +proof (induct x)
2.46 +  case (Pair a b)
2.47 +  then show ?case
2.48 +    by (simp add: prod_decode_triangle_add prod_decode_aux.simps)
2.49 +qed
2.50
2.51  lemma inj_prod_encode: "inj_on prod_encode A"
2.52    by (rule inj_on_inverseI) (rule prod_encode_inverse)
2.53 @@ -191,22 +196,22 @@
2.54    by pat_completeness auto
2.55
2.56  termination list_decode
2.57 -  apply (relation "measure id")
2.58 -   apply simp_all
2.59 -  apply (drule arg_cong [where f="prod_encode"])
2.60 -  apply (drule sym)
2.61 -  apply (simp add: le_imp_less_Suc le_prod_encode_2)
2.62 -  done
2.63 +proof -
2.64 +  have "\<And>n x y. (x, y) = prod_decode n \<Longrightarrow> y < Suc n"
2.65 +    by (metis le_imp_less_Suc le_prod_encode_2 prod_decode_inverse)
2.66 +  then show ?thesis
2.67 +    using "termination" by blast
2.68 +qed
2.69
2.70  lemma list_encode_inverse [simp]: "list_decode (list_encode x) = x"
2.71    by (induct x rule: list_encode.induct) simp_all
2.72
2.73  lemma list_decode_inverse [simp]: "list_encode (list_decode n) = n"
2.74 -  apply (induct n rule: list_decode.induct)
2.75 -   apply simp
2.76 -  apply (simp split: prod.split)
2.77 -  apply (simp add: prod_decode_eq [symmetric])
2.78 -  done
2.79 +proof (induct n rule: list_decode.induct)
2.80 +  case (2 n)
2.81 +  then show ?case
2.82 +    by (metis list_encode.simps(2) list_encode_inverse prod_decode_inverse surj_pair)
2.83 +qed auto
2.84
2.85  lemma inj_list_encode: "inj_on list_encode A"
2.86    by (rule inj_on_inverseI) (rule list_encode_inverse)
2.87 @@ -238,15 +243,16 @@
2.88  subsubsection \<open>Preliminaries\<close>
2.89
2.90  lemma finite_vimage_Suc_iff: "finite (Suc -` F) \<longleftrightarrow> finite F"
2.91 -  apply (safe intro!: finite_vimageI inj_Suc)
2.92 -  apply (rule finite_subset [where B="insert 0 (Suc ` Suc -` F)"])
2.93 -   apply (rule subsetI)
2.94 -   apply (case_tac x)
2.95 -    apply simp
2.96 -   apply simp
2.97 -  apply (rule finite_insert [THEN iffD2])
2.98 -  apply (erule finite_imageI)
2.99 -  done
2.100 +proof
2.101 +  have "F \<subseteq> insert 0 (Suc ` Suc -` F)"
2.102 +    using nat.nchotomy by force
2.103 +  moreover
2.104 +  assume "finite (Suc -` F)"
2.105 +  then have "finite (insert 0 (Suc ` Suc -` F))"
2.106 +    by blast
2.107 +  ultimately show "finite F"
2.108 +    using finite_subset by blast
2.109 +qed (force intro: finite_vimageI inj_Suc)
2.110
2.111  lemma vimage_Suc_insert_0: "Suc -` insert 0 A = Suc -` A"
2.112    by auto
2.113 @@ -287,14 +293,23 @@
2.114    by (induct set: finite) (auto simp: set_encode_def)
2.115
2.116  lemma set_encode_vimage_Suc: "set_encode (Suc -` A) = set_encode A div 2"
2.117 -  apply (cases "finite A")
2.118 -   apply (erule finite_induct)
2.119 -    apply simp
2.120 -   apply (case_tac x)
2.121 -    apply (simp add: even_set_encode_iff vimage_Suc_insert_0)
2.122 -   apply (simp add: finite_vimageI add.commute vimage_Suc_insert_Suc)
2.123 -  apply (simp add: set_encode_def finite_vimage_Suc_iff)
2.124 -  done
2.125 +proof (induction A rule: infinite_finite_induct)
2.126 +  case (infinite A)
2.127 +  then show ?case
2.128 +    by (simp add: finite_vimage_Suc_iff set_encode_inf)
2.129 +next
2.130 +  case (insert x A)
2.131 +  show ?case
2.132 +  proof (cases x)
2.133 +    case 0
2.134 +    with insert show ?thesis
2.135 +      by (simp add: even_set_encode_iff vimage_Suc_insert_0)
2.136 +  next
2.137 +    case (Suc y)
2.138 +    with insert show ?thesis
2.139 +      by (simp add: finite_vimageI add.commute vimage_Suc_insert_Suc)
2.140 +  qed
2.141 +qed auto
2.142
2.143  lemmas set_encode_div_2 = set_encode_vimage_Suc [symmetric]
2.144
2.145 @@ -335,34 +350,38 @@
2.146  qed
2.147
2.148  lemma finite_set_decode [simp]: "finite (set_decode n)"
2.149 -  apply (induct n rule: nat_less_induct)
2.150 -  apply (case_tac "n = 0")
2.151 -   apply simp
2.152 -  apply (drule_tac x="n div 2" in spec)
2.153 -  apply simp
2.154 -  apply (simp add: set_decode_div_2)
2.155 -  apply (simp add: finite_vimage_Suc_iff)
2.156 -  done
2.157 +proof (induction n rule: less_induct)
2.158 +  case (less n)
2.159 +  show ?case
2.160 +  proof (cases "n = 0")
2.161 +    case False
2.162 +    then show ?thesis
2.163 +      using less.IH [of "n div 2"] finite_vimage_Suc_iff set_decode_div_2 by auto
2.164 +  qed auto
2.165 +qed
2.166
2.167
2.168  subsubsection \<open>Proof of isomorphism\<close>
2.169
2.170  lemma set_decode_inverse [simp]: "set_encode (set_decode n) = n"
2.171 -  apply (induct n rule: nat_less_induct)
2.172 -  apply (case_tac "n = 0")
2.173 -   apply simp
2.174 -  apply (drule_tac x="n div 2" in spec)
2.175 -  apply simp
2.176 -  apply (simp add: set_decode_div_2 set_encode_vimage_Suc)
2.177 -  apply (erule div2_even_ext_nat)
2.178 -  apply (simp add: even_set_encode_iff)
2.179 -  done
2.180 +proof (induction n rule: less_induct)
2.181 +  case (less n)
2.182 +  show ?case
2.183 +  proof (cases "n = 0")
2.184 +    case False
2.185 +    then have "set_encode (set_decode (n div 2)) = n div 2"
2.186 +      using less.IH by auto
2.187 +    then show ?thesis
2.188 +      by (metis div2_even_ext_nat even_set_encode_iff finite_set_decode set_decode_0 set_decode_div_2 set_encode_div_2)
2.189 +  qed auto
2.190 +qed
2.191
2.192  lemma set_encode_inverse [simp]: "finite A \<Longrightarrow> set_decode (set_encode A) = A"
2.193 -  apply (erule finite_induct)
2.194 -   apply simp_all
2.195 -  apply (simp add: set_decode_plus_power_2)
2.196 -  done
2.197 +proof (induction rule: finite_induct)
2.198 +  case (insert x A)
2.199 +  then show ?case
2.200 +    by (simp add: set_decode_plus_power_2)
2.201 +qed auto
2.202
2.203  lemma inj_on_set_encode: "inj_on set_encode (Collect finite)"
2.204    by (rule inj_on_inverseI [where g = "set_decode"]) simp
```
```     3.1 --- a/src/HOL/Library/Ramsey.thy	Wed May 20 08:33:53 2020 +0200
3.2 +++ b/src/HOL/Library/Ramsey.thy	Wed May 20 15:00:25 2020 +0100
3.3 @@ -882,7 +882,6 @@
3.4              \<and> (\<forall>X. X \<subseteq> Y \<and> finite X \<and> card X = r \<longrightarrow> f X = t)"
3.5    by (blast intro: Ramsey_induction [unfolded part_fn_def nsets_def])
3.6
3.7 -
3.8  corollary Ramsey2:
3.9    fixes s :: nat
3.10      and Z :: "'a set"
3.11 @@ -900,6 +899,12 @@
3.12    with * show ?thesis by iprover
3.13  qed
3.14
3.15 +corollary Ramsey_nsets:
3.16 +  fixes f :: "'a set \<Rightarrow> nat"
3.17 +  assumes "infinite Z" "f ` nsets Z r \<subseteq> {..<s}"
3.18 +  obtains Y t where "Y \<subseteq> Z" "infinite Y" "t < s" "f ` nsets Y r \<subseteq> {t}"
3.19 +  using Ramsey [of Z r f s] assms by (auto simp: nsets_def image_subset_iff)
3.20 +
3.21
3.22  subsection \<open>Disjunctive Well-Foundedness\<close>
3.23
```
```     4.1 --- a/src/HOL/List.thy	Wed May 20 08:33:53 2020 +0200
4.2 +++ b/src/HOL/List.thy	Wed May 20 15:00:25 2020 +0100
4.3 @@ -6460,6 +6460,10 @@
4.4    then show ?thesis by (intro that [of "length us"]) auto
4.5  qed
4.6
4.7 +lemma irrefl_lex: "irrefl r \<Longrightarrow> irrefl (lex r)"
4.8 +  by (meson irrefl_def lex_take_index)
4.9 +
4.10 +
4.11
4.12  subsubsection \<open>Lexicographic Ordering\<close>
4.13
```
```     5.1 --- a/src/HOL/Set.thy	Wed May 20 08:33:53 2020 +0200
5.2 +++ b/src/HOL/Set.thy	Wed May 20 15:00:25 2020 +0100
5.3 @@ -1246,6 +1246,9 @@
5.4  lemma disjoint_eq_subset_Compl: "A \<inter> B = {} \<longleftrightarrow> A \<subseteq> - B"
5.5    by blast
5.6
5.7 +lemma disjoint_iff: "A \<inter> B = {} \<longleftrightarrow> (\<forall>x. x\<in>A \<longrightarrow> x \<notin> B)"
5.8 +  by blast
5.9 +
5.10  lemma disjoint_iff_not_equal: "A \<inter> B = {} \<longleftrightarrow> (\<forall>x\<in>A. \<forall>y\<in>B. x \<noteq> y)"
5.11    by blast
5.12
```