# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1633347170 -3600
# Node ID 5827b91ef30ef16ad85e3f098e3f4e2258171853
# Parent  75d14ac0547e9473279bf6852bd7377700d93ae6
new material from the Roth development, mostly about finite sets, disjoint famillies and partitions

diff -r 75d14ac0547e -r 5827b91ef30e src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Sun Oct 03 21:29:34 2021 +0200
+++ b/src/HOL/Finite_Set.thy	Mon Oct 04 12:32:50 2021 +0100
@@ -373,6 +373,17 @@
 lemma finite_vimage_iff: "bij h \<Longrightarrow> finite (h -` F) \<longleftrightarrow> finite F"
   unfolding bij_def by (auto elim: finite_vimageD finite_vimageI)
 
+lemma finite_inverse_image_gen:
+  assumes "finite A" "inj_on f D"
+  shows "finite {j\<in>D. f j \<in> A}"
+  using finite_vimage_IntI [OF assms]
+  by (simp add: Collect_conj_eq inf_commute vimage_def)
+
+lemma finite_inverse_image:
+  assumes "finite A" "inj f"
+  shows "finite {j. f j \<in> A}"
+  using finite_inverse_image_gen [OF assms] by simp
+
 lemma finite_Collect_bex [simp]:
   assumes "finite A"
   shows "finite {x. \<exists>y\<in>A. Q x y} \<longleftrightarrow> (\<forall>y\<in>A. finite {x. Q x y})"
diff -r 75d14ac0547e -r 5827b91ef30e src/HOL/Groups_Big.thy
--- a/src/HOL/Groups_Big.thy	Sun Oct 03 21:29:34 2021 +0200
+++ b/src/HOL/Groups_Big.thy	Mon Oct 04 12:32:50 2021 +0100
@@ -1560,6 +1560,20 @@
   then show ?case by (force intro: mult_strict_mono' prod_nonneg)
 qed
 
+lemma prod_le_power:
+  assumes A: "\<And>i. i \<in> A \<Longrightarrow> 0 \<le> f i \<and> f i \<le> n" "card A \<le> k" and "n \<ge> 1"
+  shows "prod f A \<le> n ^ k"
+  using A
+proof (induction A arbitrary: k rule: infinite_finite_induct)
+  case (insert i A)
+  then obtain k' where k': "card A \<le> k'" "k = Suc k'"
+    using Suc_le_D by force
+  have "f i * prod f A \<le> n * n ^ k'"
+    using insert \<open>n \<ge> 1\<close> k' by (intro prod_nonneg mult_mono; force)
+  then show ?case 
+    by (auto simp: \<open>k = Suc k'\<close> insert.hyps)
+qed (use \<open>n \<ge> 1\<close> in auto)
+
 end
 
 lemma prod_mono2:
diff -r 75d14ac0547e -r 5827b91ef30e src/HOL/Library/Countable_Set.thy
--- a/src/HOL/Library/Countable_Set.thy	Sun Oct 03 21:29:34 2021 +0200
+++ b/src/HOL/Library/Countable_Set.thy	Mon Oct 04 12:32:50 2021 +0100
@@ -110,6 +110,25 @@
   using to_nat_on_infinite[of S, unfolded bij_betw_def]
   by (auto cong: bij_betw_cong intro: bij_betw_inv_into to_nat_on_infinite)
 
+text \<open>
+  The sum/product over the enumeration of a finite set equals simply the sum/product over the set
+\<close>
+context comm_monoid_set
+begin
+
+lemma card_from_nat_into:
+  "F (\<lambda>i. h (from_nat_into A i)) {..<card A} = F h A"
+proof (cases "finite A")
+  case True
+  have "F (\<lambda>i. h (from_nat_into A i)) {..<card A} = F h (from_nat_into A ` {..<card A})"
+    by (metis True bij_betw_def bij_betw_from_nat_into_finite reindex_cong)
+  also have "... = F h A"
+    by (metis True bij_betw_def bij_betw_from_nat_into_finite)
+  finally show ?thesis .
+qed auto
+
+end
+
 lemma countable_as_injective_image:
   assumes "countable A" "infinite A"
   obtains f :: "nat \<Rightarrow> 'a" where "A = range f" "inj f"
diff -r 75d14ac0547e -r 5827b91ef30e src/HOL/Library/Disjoint_Sets.thy
--- a/src/HOL/Library/Disjoint_Sets.thy	Sun Oct 03 21:29:34 2021 +0200
+++ b/src/HOL/Library/Disjoint_Sets.thy	Mon Oct 04 12:32:50 2021 +0100
@@ -167,6 +167,20 @@
     by (intro disjointD[OF d]) auto
 qed
 
+lemma disjoint_family_on_iff_disjoint_image:
+  assumes "\<And>i. i \<in> I \<Longrightarrow> A i \<noteq> {}"
+  shows "disjoint_family_on A I \<longleftrightarrow> disjoint (A ` I) \<and> inj_on A I"
+proof
+  assume "disjoint_family_on A I"
+  then show "disjoint (A ` I) \<and> inj_on A I"
+    by (metis (mono_tags, lifting) assms disjoint_family_onD disjoint_family_on_disjoint_image inf.idem inj_onI)
+qed (use disjoint_image_disjoint_family_on in metis)
+
+lemma card_UN_disjoint':
+  assumes "disjoint_family_on A I" "\<And>i. i \<in> I \<Longrightarrow> finite (A i)" "finite I"
+  shows "card (\<Union>i\<in>I. A i) = (\<Sum>i\<in>I. card (A i))"
+  using assms   by (simp add: card_UN_disjoint disjoint_family_on_def)
+
 lemma disjoint_UN:
   assumes F: "\<And>i. i \<in> I \<Longrightarrow> disjoint (F i)" and *: "disjoint_family_on (\<lambda>i. \<Union>(F i)) I"
   shows "disjoint (\<Union>i\<in>I. F i)"
@@ -217,6 +231,25 @@
   using disjoint_UN[of "{C, B}" "\<lambda>x. x"] by (auto simp add: disjoint_family_on_def)
 
 text \<open>
+  Sum/product of the union of a finite disjoint family
+\<close>
+context comm_monoid_set
+begin
+
+lemma UNION_disjoint_family:
+  assumes "finite I" and "\<forall>i\<in>I. finite (A i)"
+    and "disjoint_family_on A I"
+  shows "F g (\<Union>(A ` I)) = F (\<lambda>x. F g (A x)) I"
+  using assms unfolding disjoint_family_on_def  by (rule UNION_disjoint)
+
+lemma Union_disjoint_sets:
+  assumes "\<forall>A\<in>C. finite A" and "disjoint C"
+  shows "F g (\<Union>C) = (F \<circ> F) g C"
+  using assms unfolding disjoint_def  by (rule Union_disjoint)
+
+end
+
+text \<open>
   The union of an infinite disjoint family of non-empty sets is infinite.
 \<close>
 lemma infinite_disjoint_family_imp_infinite_UNION:
@@ -353,6 +386,11 @@
 lemma finite_elements: "finite A \<Longrightarrow> partition_on A P \<Longrightarrow> finite P"
   using partition_onD1[of A P] by (simp add: finite_UnionD)
 
+lemma product_partition:
+  assumes "partition_on A P" and "\<And>p. p \<in> P \<Longrightarrow> finite p" 
+  shows "card A = (\<Sum>p\<in>P. card p)"
+  using assms unfolding partition_on_def  by (meson card_Union_disjoint)
+
 subsection \<open>Equivalence of partitions and equivalence classes\<close>
 
 lemma partition_on_quotient:
diff -r 75d14ac0547e -r 5827b91ef30e src/HOL/Power.thy
--- a/src/HOL/Power.thy	Sun Oct 03 21:29:34 2021 +0200
+++ b/src/HOL/Power.thy	Mon Oct 04 12:32:50 2021 +0100
@@ -810,6 +810,10 @@
     by (auto intro!: power2_le_imp_le [OF _ abs_ge_zero])
 qed
 
+lemma power2_le_iff_abs_le:
+  "y \<ge> 0 \<Longrightarrow> x\<^sup>2 \<le> y\<^sup>2 \<longleftrightarrow> \<bar>x\<bar> \<le> y"
+  by (metis abs_le_square_iff abs_of_nonneg)
+
 lemma abs_square_le_1:"x\<^sup>2 \<le> 1 \<longleftrightarrow> \<bar>x\<bar> \<le> 1"
   using abs_le_square_iff [of x 1] by simp