A few new theorems, plus some tidying up
authorpaulson <lp15@cam.ac.uk>
Wed May 20 15:00:25 2020 +0100 (11 days ago)
changeset 718483c7852327787
parent 71847 da12452c9be2
child 71849 265bbad3d6af
A few new theorems, plus some tidying up
src/HOL/Library/Countable_Set.thy
src/HOL/Library/Nat_Bijection.thy
src/HOL/Library/Ramsey.thy
src/HOL/List.thy
src/HOL/Set.thy
     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.34 +    by (metis ab_semigroup_add_class.add_ac(1) add_diff_cancel_left' le_add1 not_less_eq_eq prod_decode_aux.simps triangle_Suc)
    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.41 -  apply (simp add: prod_decode_triangle_add)
    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