--- 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
--- 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
--- 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>
--- 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>
--- 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