# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1589983225 -3600
# Node ID 3c7852327787150604dfe89b8555e2364bb66966
# Parent  da12452c9be2532e4dc3b8916907e24c5593b0ea
A few new theorems, plus some tidying up

diff -r da12452c9be2 -r 3c7852327787 src/HOL/Library/Countable_Set.thy
--- a/src/HOL/Library/Countable_Set.thy	Wed May 20 08:33:53 2020 +0200
+++ b/src/HOL/Library/Countable_Set.thy	Wed May 20 15:00:25 2020 +0100
@@ -319,8 +319,12 @@
   "countable T \<Longrightarrow> countable {A. finite A \<and> A \<subseteq> T}"
   unfolding Collect_finite_subset_eq_lists by auto
 
+lemma countable_Fpow: "countable S \<Longrightarrow> countable (Fpow S)"
+  using countable_Collect_finite_subset
+  by (force simp add: Fpow_def conj_commute)
+
 lemma countable_set_option [simp]: "countable (set_option x)"
-by(cases x) auto
+  by (cases x) auto
 
 subsection \<open>Misc lemmas\<close>
 
@@ -420,4 +424,27 @@
 lemma countable_Diff_eq [simp]: "countable (A - {x}) = countable A"
   by (meson countable_Diff countable_empty countable_insert uncountable_minus_countable)
 
+text \<open>Every infinite set can be covered by a pairwise disjoint family of infinite sets.
+      This version doesn't achieve equality, as it only covers a countable subset\<close>
+lemma infinite_infinite_partition:
+  assumes "infinite A"
+  obtains C :: "nat \<Rightarrow> 'a set" 
+    where "pairwise (\<lambda>i j. disjnt (C i) (C j)) UNIV" "(\<Union>i. C i) \<subseteq> A" "\<And>i. infinite (C i)"
+proof -
+  obtain f :: "nat\<Rightarrow>'a" where "range f \<subseteq> A" "inj f"
+    using assms infinite_countable_subset by blast
+  let ?C = "\<lambda>i. range (\<lambda>j. f (prod_encode (i,j)))"
+  show thesis
+  proof
+    show "pairwise (\<lambda>i j. disjnt (?C i) (?C j)) UNIV"
+      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])
+    show "(\<Union>i. ?C i) \<subseteq> A"
+      using \<open>range f \<subseteq> A\<close> by blast
+    have "infinite (range (\<lambda>j. f (prod_encode (i, j))))" for i
+      by (rule range_inj_infinite) (meson Pair_inject \<open>inj f\<close> inj_def prod_encode_eq)
+    then show "\<And>i. infinite (?C i)"
+      using that by auto
+  qed
+qed
+
 end
diff -r da12452c9be2 -r 3c7852327787 src/HOL/Library/Nat_Bijection.thy
--- a/src/HOL/Library/Nat_Bijection.thy	Wed May 20 08:33:53 2020 +0200
+++ b/src/HOL/Library/Nat_Bijection.thy	Wed May 20 15:00:25 2020 +0100
@@ -40,29 +40,34 @@
   where "prod_decode = prod_decode_aux 0"
 
 lemma prod_encode_prod_decode_aux: "prod_encode (prod_decode_aux k m) = triangle k + m"
-  apply (induct k m rule: prod_decode_aux.induct)
-  apply (subst prod_decode_aux.simps)
-  apply (simp add: prod_encode_def)
-  done
+proof (induction k m rule: prod_decode_aux.induct)
+  case (1 k m)
+  then show ?case
+    by (simp add: prod_encode_def prod_decode_aux.simps)
+qed
 
 lemma prod_decode_inverse [simp]: "prod_encode (prod_decode n) = n"
   by (simp add: prod_decode_def prod_encode_prod_decode_aux)
 
 lemma prod_decode_triangle_add: "prod_decode (triangle k + m) = prod_decode_aux k m"
-  apply (induct k arbitrary: m)
-   apply (simp add: prod_decode_def)
-  apply (simp only: triangle_Suc add.assoc)
-  apply (subst prod_decode_aux.simps)
-  apply simp
-  done
+proof (induct k arbitrary: m)
+  case 0
+  then show ?case 
+    by (simp add: prod_decode_def)
+next
+  case (Suc k)
+  then show ?case
+    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)
+qed
+
 
 lemma prod_encode_inverse [simp]: "prod_decode (prod_encode x) = x"
   unfolding prod_encode_def
-  apply (induct x)
-  apply (simp add: prod_decode_triangle_add)
-  apply (subst prod_decode_aux.simps)
-  apply simp
-  done
+proof (induct x)
+  case (Pair a b)
+  then show ?case
+    by (simp add: prod_decode_triangle_add prod_decode_aux.simps)
+qed
 
 lemma inj_prod_encode: "inj_on prod_encode A"
   by (rule inj_on_inverseI) (rule prod_encode_inverse)
@@ -191,22 +196,22 @@
   by pat_completeness auto
 
 termination list_decode
-  apply (relation "measure id")
-   apply simp_all
-  apply (drule arg_cong [where f="prod_encode"])
-  apply (drule sym)
-  apply (simp add: le_imp_less_Suc le_prod_encode_2)
-  done
+proof -
+  have "\<And>n x y. (x, y) = prod_decode n \<Longrightarrow> y < Suc n"
+    by (metis le_imp_less_Suc le_prod_encode_2 prod_decode_inverse)
+  then show ?thesis
+    using "termination" by blast
+qed
 
 lemma list_encode_inverse [simp]: "list_decode (list_encode x) = x"
   by (induct x rule: list_encode.induct) simp_all
 
 lemma list_decode_inverse [simp]: "list_encode (list_decode n) = n"
-  apply (induct n rule: list_decode.induct)
-   apply simp
-  apply (simp split: prod.split)
-  apply (simp add: prod_decode_eq [symmetric])
-  done
+proof (induct n rule: list_decode.induct)
+  case (2 n)
+  then show ?case
+    by (metis list_encode.simps(2) list_encode_inverse prod_decode_inverse surj_pair)
+qed auto
 
 lemma inj_list_encode: "inj_on list_encode A"
   by (rule inj_on_inverseI) (rule list_encode_inverse)
@@ -238,15 +243,16 @@
 subsubsection \<open>Preliminaries\<close>
 
 lemma finite_vimage_Suc_iff: "finite (Suc -` F) \<longleftrightarrow> finite F"
-  apply (safe intro!: finite_vimageI inj_Suc)
-  apply (rule finite_subset [where B="insert 0 (Suc ` Suc -` F)"])
-   apply (rule subsetI)
-   apply (case_tac x)
-    apply simp
-   apply simp
-  apply (rule finite_insert [THEN iffD2])
-  apply (erule finite_imageI)
-  done
+proof 
+  have "F \<subseteq> insert 0 (Suc ` Suc -` F)"
+    using nat.nchotomy by force
+  moreover
+  assume "finite (Suc -` F)"
+  then have "finite (insert 0 (Suc ` Suc -` F))"
+    by blast
+  ultimately show "finite F"
+    using finite_subset by blast
+qed (force intro: finite_vimageI inj_Suc)
 
 lemma vimage_Suc_insert_0: "Suc -` insert 0 A = Suc -` A"
   by auto
@@ -287,14 +293,23 @@
   by (induct set: finite) (auto simp: set_encode_def)
 
 lemma set_encode_vimage_Suc: "set_encode (Suc -` A) = set_encode A div 2"
-  apply (cases "finite A")
-   apply (erule finite_induct)
-    apply simp
-   apply (case_tac x)
-    apply (simp add: even_set_encode_iff vimage_Suc_insert_0)
-   apply (simp add: finite_vimageI add.commute vimage_Suc_insert_Suc)
-  apply (simp add: set_encode_def finite_vimage_Suc_iff)
-  done
+proof (induction A rule: infinite_finite_induct)
+  case (infinite A)
+  then show ?case
+    by (simp add: finite_vimage_Suc_iff set_encode_inf)
+next
+  case (insert x A)
+  show ?case
+  proof (cases x)
+    case 0
+    with insert show ?thesis
+      by (simp add: even_set_encode_iff vimage_Suc_insert_0)
+  next
+    case (Suc y)
+    with insert show ?thesis
+      by (simp add: finite_vimageI add.commute vimage_Suc_insert_Suc)
+  qed   
+qed auto
 
 lemmas set_encode_div_2 = set_encode_vimage_Suc [symmetric]
 
@@ -335,34 +350,38 @@
 qed
 
 lemma finite_set_decode [simp]: "finite (set_decode n)"
-  apply (induct n rule: nat_less_induct)
-  apply (case_tac "n = 0")
-   apply simp
-  apply (drule_tac x="n div 2" in spec)
-  apply simp
-  apply (simp add: set_decode_div_2)
-  apply (simp add: finite_vimage_Suc_iff)
-  done
+proof (induction n rule: less_induct)
+  case (less n)
+  show ?case
+  proof (cases "n = 0")
+    case False
+    then show ?thesis
+      using less.IH [of "n div 2"] finite_vimage_Suc_iff set_decode_div_2 by auto
+  qed auto
+qed
 
 
 subsubsection \<open>Proof of isomorphism\<close>
 
 lemma set_decode_inverse [simp]: "set_encode (set_decode n) = n"
-  apply (induct n rule: nat_less_induct)
-  apply (case_tac "n = 0")
-   apply simp
-  apply (drule_tac x="n div 2" in spec)
-  apply simp
-  apply (simp add: set_decode_div_2 set_encode_vimage_Suc)
-  apply (erule div2_even_ext_nat)
-  apply (simp add: even_set_encode_iff)
-  done
+proof (induction n rule: less_induct)
+  case (less n)
+  show ?case
+  proof (cases "n = 0")
+    case False
+    then have "set_encode (set_decode (n div 2)) = n div 2"
+      using less.IH by auto
+    then show ?thesis
+      by (metis div2_even_ext_nat even_set_encode_iff finite_set_decode set_decode_0 set_decode_div_2 set_encode_div_2)
+  qed auto
+qed
 
 lemma set_encode_inverse [simp]: "finite A \<Longrightarrow> set_decode (set_encode A) = A"
-  apply (erule finite_induct)
-   apply simp_all
-  apply (simp add: set_decode_plus_power_2)
-  done
+proof (induction rule: finite_induct)
+  case (insert x A)
+  then show ?case
+    by (simp add: set_decode_plus_power_2)
+qed auto
 
 lemma inj_on_set_encode: "inj_on set_encode (Collect finite)"
   by (rule inj_on_inverseI [where g = "set_decode"]) simp
diff -r da12452c9be2 -r 3c7852327787 src/HOL/Library/Ramsey.thy
--- a/src/HOL/Library/Ramsey.thy	Wed May 20 08:33:53 2020 +0200
+++ b/src/HOL/Library/Ramsey.thy	Wed May 20 15:00:25 2020 +0100
@@ -882,7 +882,6 @@
             \<and> (\<forall>X. X \<subseteq> Y \<and> finite X \<and> card X = r \<longrightarrow> f X = t)"
   by (blast intro: Ramsey_induction [unfolded part_fn_def nsets_def])
 
-
 corollary Ramsey2:
   fixes s :: nat
     and Z :: "'a set"
@@ -900,6 +899,12 @@
   with * show ?thesis by iprover
 qed
 
+corollary Ramsey_nsets:
+  fixes f :: "'a set \<Rightarrow> nat"
+  assumes "infinite Z" "f ` nsets Z r \<subseteq> {..<s}"
+  obtains Y t where "Y \<subseteq> Z" "infinite Y" "t < s" "f ` nsets Y r \<subseteq> {t}"
+  using Ramsey [of Z r f s] assms by (auto simp: nsets_def image_subset_iff)
+
 
 subsection \<open>Disjunctive Well-Foundedness\<close>
 
diff -r da12452c9be2 -r 3c7852327787 src/HOL/List.thy
--- a/src/HOL/List.thy	Wed May 20 08:33:53 2020 +0200
+++ b/src/HOL/List.thy	Wed May 20 15:00:25 2020 +0100
@@ -6460,6 +6460,10 @@
   then show ?thesis by (intro that [of "length us"]) auto
 qed
 
+lemma irrefl_lex: "irrefl r \<Longrightarrow> irrefl (lex r)"
+  by (meson irrefl_def lex_take_index)
+
+
 
 subsubsection \<open>Lexicographic Ordering\<close>
 
diff -r da12452c9be2 -r 3c7852327787 src/HOL/Set.thy
--- a/src/HOL/Set.thy	Wed May 20 08:33:53 2020 +0200
+++ b/src/HOL/Set.thy	Wed May 20 15:00:25 2020 +0100
@@ -1246,6 +1246,9 @@
 lemma disjoint_eq_subset_Compl: "A \<inter> B = {} \<longleftrightarrow> A \<subseteq> - B"
   by blast
 
+lemma disjoint_iff: "A \<inter> B = {} \<longleftrightarrow> (\<forall>x. x\<in>A \<longrightarrow> x \<notin> B)"
+  by blast
+
 lemma disjoint_iff_not_equal: "A \<inter> B = {} \<longleftrightarrow> (\<forall>x\<in>A. \<forall>y\<in>B. x \<noteq> y)"
   by blast