# HG changeset patch
# User haftmann
# Date 1416232534 -3600
# Node ID ec2b4270a50286783807d82201cacb07ff53ff5d
# Parent  348561aa3869f0631522674f8f098871a046e9b5
generalized lemmas and tuned proofs

diff -r 348561aa3869 -r ec2b4270a502 src/HOL/Groups_Big.thy
--- a/src/HOL/Groups_Big.thy	Mon Nov 17 14:55:33 2014 +0100
+++ b/src/HOL/Groups_Big.thy	Mon Nov 17 14:55:34 2014 +0100
@@ -926,6 +926,10 @@
   case True then show ?thesis by (induct A) (simp_all add: assms)
 qed
 
+lemma (in comm_semiring_1) dvd_setsum:
+  "(\<And>a. a \<in> A \<Longrightarrow> d dvd f a) \<Longrightarrow> d dvd setsum f A"
+  by (induct A rule: infinite_finite_induct) simp_all
+
 
 subsubsection {* Cardinality as special case of @{const setsum} *}
 
@@ -1072,128 +1076,133 @@
   "PROD x|P. t" => "CONST setprod (%x. t) {x. P}"
   "\<Prod>x|P. t" => "CONST setprod (%x. t) {x. P}"
 
+context comm_monoid_mult
+begin
+
+lemma setprod_dvd_setprod: 
+  "(\<And>a. a \<in> A \<Longrightarrow> f a dvd g a) \<Longrightarrow> setprod f A dvd setprod g A"
+proof (induct A rule: infinite_finite_induct)
+  case infinite then show ?case by (auto intro: dvdI)
+next
+  case empty then show ?case by (auto intro: dvdI)
+next
+  case (insert a A) then
+  have "f a dvd g a" and "setprod f A dvd setprod g A" by simp_all
+  then obtain r s where "g a = f a * r" and "setprod g A = setprod f A * s" by (auto elim!: dvdE)
+  then have "g a * setprod g A = f a * setprod f A * (r * s)" by (simp add: ac_simps)
+  with insert.hyps show ?case by (auto intro: dvdI)
+qed
+
+lemma setprod_dvd_setprod_subset:
+  "finite B \<Longrightarrow> A \<subseteq> B \<Longrightarrow> setprod f A dvd setprod f B"
+  by (auto simp add: setprod.subset_diff ac_simps intro: dvdI)
+
+end
+
 
 subsubsection {* Properties in more restricted classes of structures *}
 
-lemma setprod_zero:
-     "finite A ==> EX x: A. f x = (0::'a::comm_semiring_1) ==> setprod f A = 0"
-apply (induct set: finite, force, clarsimp)
-apply (erule disjE, auto)
-done
-
-lemma setprod_zero_iff[simp]: "finite A ==> 
-  (setprod f A = (0::'a::{comm_semiring_1,no_zero_divisors})) =
-  (EX x: A. f x = 0)"
-by (erule finite_induct, auto simp:no_zero_divisors)
+context comm_semiring_1
+begin
 
-lemma setprod_Un: "finite A ==> finite B ==> (ALL x: A Int B. f x \<noteq> 0) ==>
-  (setprod f (A Un B) :: 'a ::{field})
-   = setprod f A * setprod f B / setprod f (A Int B)"
-by (subst setprod.union_inter [symmetric], auto)
-
-lemma setprod_nonneg [rule_format]:
-   "(ALL x: A. (0::'a::linordered_semidom) \<le> f x) --> 0 \<le> setprod f A"
-by (cases "finite A", induct set: finite, simp_all)
-
-lemma setprod_pos [rule_format]: "(ALL x: A. (0::'a::linordered_semidom) < f x)
-  --> 0 < setprod f A"
-by (cases "finite A", induct set: finite, simp_all)
-
-lemma setprod_diff1: "finite A ==> f a \<noteq> 0 ==>
-  (setprod f (A - {a}) :: 'a :: {field}) =
-  (if a:A then setprod f A / f a else setprod f A)"
-  by (erule finite_induct) (auto simp add: insert_Diff_if)
+lemma dvd_setprod_eqI [intro]:
+  assumes "finite A" and "a \<in> A" and "b = f a"
+  shows "b dvd setprod f A"
+proof -
+  from `finite A` have "setprod f (insert a (A - {a})) = f a * setprod f (A - {a})"
+    by (intro setprod.insert) auto
+  also from `a \<in> A` have "insert a (A - {a}) = A" by blast
+  finally have "setprod f A = f a * setprod f (A - {a})" .
+  with `b = f a` show ?thesis by simp
+qed
 
-lemma setprod_inversef: 
-  fixes f :: "'b \<Rightarrow> 'a::field_inverse_zero"
-  shows "finite A ==> setprod (inverse \<circ> f) A = inverse (setprod f A)"
-by (erule finite_induct) auto
+lemma dvd_setprodI [intro]:
+  assumes "finite A" and "a \<in> A"
+  shows "f a dvd setprod f A"
+  using assms by auto
 
-lemma setprod_dividef:
-  fixes f :: "'b \<Rightarrow> 'a::field_inverse_zero"
-  shows "finite A
-    ==> setprod (%x. f x / g x) A = setprod f A / setprod g A"
-apply (subgoal_tac
-         "setprod (%x. f x / g x) A = setprod (%x. f x * (inverse \<circ> g) x) A")
-apply (erule ssubst)
-apply (subst divide_inverse)
-apply (subst setprod.distrib)
-apply (subst setprod_inversef, assumption+, rule refl)
-apply (rule setprod.cong, rule refl)
-apply (subst divide_inverse, auto)
-done
-
-lemma setprod_dvd_setprod [rule_format]: 
-    "(ALL x : A. f x dvd g x) \<longrightarrow> setprod f A dvd setprod g A"
-  apply (cases "finite A")
-  apply (induct set: finite)
-  apply (auto simp add: dvd_def)
-  apply (rule_tac x = "k * ka" in exI)
-  apply (simp add: algebra_simps)
-done
-
-lemma setprod_dvd_setprod_subset:
-  "finite B \<Longrightarrow> A <= B \<Longrightarrow> setprod f A dvd setprod f B"
-  apply (subgoal_tac "setprod f B = setprod f A * setprod f (B - A)")
-  apply (unfold dvd_def, blast)
-  apply (subst setprod.union_disjoint [symmetric])
-  apply (auto elim: finite_subset intro: setprod.cong)
-done
+lemma setprod_zero:
+  assumes "finite A" and "\<exists>a\<in>A. f a = 0"
+  shows "setprod f A = 0"
+using assms proof (induct A)
+  case empty then show ?case by simp
+next
+  case (insert a A)
+  then have "f a = 0 \<or> (\<exists>a\<in>A. f a = 0)" by simp
+  then have "f a * setprod f A = 0" by rule (simp_all add: insert)
+  with insert show ?case by simp
+qed
 
 lemma setprod_dvd_setprod_subset2:
-  "finite B \<Longrightarrow> A <= B \<Longrightarrow> ALL x : A. (f x::'a::comm_semiring_1) dvd g x \<Longrightarrow> 
-      setprod f A dvd setprod g B"
-  apply (rule dvd_trans)
-  apply (rule setprod_dvd_setprod, erule (1) bspec)
-  apply (erule (1) setprod_dvd_setprod_subset)
-done
+  assumes "finite B" and "A \<subseteq> B" and "\<And>a. a \<in> A \<Longrightarrow> f a dvd g a"
+  shows "setprod f A dvd setprod g B"
+proof -
+  from assms have "setprod f A dvd setprod g A"
+    by (auto intro: setprod_dvd_setprod)
+  moreover from assms have "setprod g A dvd setprod g B"
+    by (auto intro: setprod_dvd_setprod_subset)
+  ultimately show ?thesis by (rule dvd_trans)
+qed
+
+end
+
+lemma setprod_zero_iff [simp]:
+  assumes "finite A"
+  shows "setprod f A = (0::'a::{comm_semiring_1,no_zero_divisors}) \<longleftrightarrow> (\<exists>a\<in>A. f a = 0)"
+  using assms by (induct A) (auto simp: no_zero_divisors)
+
+lemma (in field) setprod_diff1:
+  "finite A \<Longrightarrow> f a \<noteq> 0 \<Longrightarrow>
+    (setprod f (A - {a})) = (if a \<in> A then setprod f A / f a else setprod f A)"
+  by (induct A rule: finite_induct) (auto simp add: insert_Diff_if)
 
-lemma dvd_setprod: "finite A \<Longrightarrow> i:A \<Longrightarrow> 
-    (f i ::'a::comm_semiring_1) dvd setprod f A"
-by (induct set: finite) (auto intro: dvd_mult)
+lemma (in field_inverse_zero) setprod_inversef: 
+  "finite A \<Longrightarrow> setprod (inverse \<circ> f) A = inverse (setprod f A)"
+  by (induct A rule: finite_induct) simp_all
+
+lemma (in field_inverse_zero) setprod_dividef:
+  "finite A \<Longrightarrow> (\<Prod>x\<in>A. f x / g x) = setprod f A / setprod g A"
+  using setprod_inversef [of A g] by (simp add: divide_inverse setprod.distrib)
 
-lemma dvd_setsum [rule_format]: "(ALL i : A. d dvd f i) \<longrightarrow> 
-    (d::'a::comm_semiring_1) dvd (SUM x : A. f x)"
-  apply (cases "finite A")
-  apply (induct set: finite)
-  apply auto
-done
+lemma setprod_Un:
+  fixes f :: "'b \<Rightarrow> 'a :: field"
+  assumes "finite A" and "finite B"
+  and "\<forall>x\<in>A \<inter> B. f x \<noteq> 0"
+  shows "setprod f (A \<union> B) = setprod f A * setprod f B / setprod f (A \<inter> B)"
+proof -
+  from assms have "setprod f A * setprod f B = setprod f (A \<union> B) * setprod f (A \<inter> B)"
+    by (simp add: setprod.union_inter [symmetric, of A B])
+  with assms show ?thesis by simp
+qed
 
-lemma setprod_mono:
-  fixes f :: "'a \<Rightarrow> 'b\<Colon>linordered_semidom"
+lemma (in linordered_semidom) setprod_nonneg:
+  "(\<forall>a\<in>A. 0 \<le> f a) \<Longrightarrow> 0 \<le> setprod f A"
+  by (induct A rule: infinite_finite_induct) simp_all
+
+lemma (in linordered_semidom) setprod_pos:
+  "(\<forall>a\<in>A. 0 < f a) \<Longrightarrow> 0 < setprod f A"
+  by (induct A rule: infinite_finite_induct) simp_all
+
+lemma (in linordered_semidom) setprod_mono:
   assumes "\<forall>i\<in>A. 0 \<le> f i \<and> f i \<le> g i"
   shows "setprod f A \<le> setprod g A"
-proof (cases "finite A")
-  case True
-  hence ?thesis "setprod f A \<ge> 0" using subset_refl[of A]
-  proof (induct A rule: finite_subset_induct)
-    case (insert a F)
-    thus "setprod f (insert a F) \<le> setprod g (insert a F)" "0 \<le> setprod f (insert a F)"
-      unfolding setprod.insert[OF insert(1,3)]
-      using assms[rule_format,OF insert(2)] insert
-      by (auto intro: mult_mono)
-  qed auto
-  thus ?thesis by simp
-qed auto
+  using assms by (induct A rule: infinite_finite_induct)
+    (auto intro!: setprod_nonneg mult_mono)
 
-lemma abs_setprod:
-  fixes f :: "'a \<Rightarrow> 'b\<Colon>{linordered_field,abs}"
-  shows "abs (setprod f A) = setprod (\<lambda>x. abs (f x)) A"
-proof (cases "finite A")
-  case True thus ?thesis
-    by induct (auto simp add: field_simps abs_mult)
-qed auto
+lemma (in linordered_field) abs_setprod:
+  "\<bar>setprod f A\<bar> = (\<Prod>x\<in>A. \<bar>f x\<bar>)"
+  by (induct A rule: infinite_finite_induct) (simp_all add: abs_mult)
 
 lemma setprod_eq_1_iff [simp]:
-  "finite F ==> setprod f F = 1 \<longleftrightarrow> (ALL a:F. f a = (1::nat))"
-  by (induct set: finite) auto
+  "finite A \<Longrightarrow> setprod f A = 1 \<longleftrightarrow> (\<forall>a\<in>A. f a = (1::nat))"
+  by (induct A rule: finite_induct) simp_all
 
 lemma setprod_pos_nat:
-  "finite S ==> (ALL x : S. f x > (0::nat)) ==> setprod f S > 0"
-using setprod_zero_iff by(simp del:neq0_conv add:neq0_conv[symmetric])
+  "finite A \<Longrightarrow> (\<forall>a\<in>A. f a > (0::nat)) \<Longrightarrow> setprod f A > 0"
+  using setprod_zero_iff by (simp del: neq0_conv add: neq0_conv [symmetric])
 
-lemma setprod_pos_nat_iff[simp]:
-  "finite S ==> (setprod f S > 0) = (ALL x : S. f x > (0::nat))"
-using setprod_zero_iff by(simp del:neq0_conv add:neq0_conv[symmetric])
+lemma setprod_pos_nat_iff [simp]:
+  "finite A \<Longrightarrow> setprod f A > 0 \<longleftrightarrow> (\<forall>a\<in>A. f a > (0::nat))"
+  using setprod_zero_iff by (simp del:neq0_conv add:neq0_conv [symmetric])
 
 end
diff -r 348561aa3869 -r ec2b4270a502 src/HOL/Number_Theory/Cong.thy
--- a/src/HOL/Number_Theory/Cong.thy	Mon Nov 17 14:55:33 2014 +0100
+++ b/src/HOL/Number_Theory/Cong.thy	Mon Nov 17 14:55:34 2014 +0100
@@ -820,7 +820,7 @@
         apply (drule (1) bspec)
         apply (erule conjE)
         apply assumption
-        apply (rule dvd_setprod)
+        apply rule
         using fin a apply auto
         done
       finally show ?thesis
@@ -863,7 +863,7 @@
     apply (rule cong_dvd_modulus_nat)
     apply (rule cong_mod_nat)
     using prodnz apply auto
-    apply (rule dvd_setprod)
+    apply rule
     apply (rule fin)
     apply assumption
     done
diff -r 348561aa3869 -r ec2b4270a502 src/HOL/Number_Theory/Euclidean_Algorithm.thy
--- a/src/HOL/Number_Theory/Euclidean_Algorithm.thy	Mon Nov 17 14:55:33 2014 +0100
+++ b/src/HOL/Number_Theory/Euclidean_Algorithm.thy	Mon Nov 17 14:55:34 2014 +0100
@@ -7,21 +7,6 @@
 begin
 
 context semiring_div
-begin
-
-lemma dvd_setprod [intro]:
-  assumes "finite A" and "x \<in> A"
-  shows "f x dvd setprod f A"
-proof
-  from `finite A` have "setprod f (insert x (A - {x})) = f x * setprod f (A - {x})"
-    by (intro setprod.insert) auto
-  also from `x \<in> A` have "insert x (A - {x}) = A" by blast
-  finally show "setprod f A = f x * setprod f (A - {x})" .
-qed
-
-end
-
-context semiring_div
 begin 
 
 definition ring_inv :: "'a \<Rightarrow> 'a"
@@ -1463,7 +1448,7 @@
       apply (rule no_zero_divisors)
       apply blast+
       done
-    moreover from `finite A` have "\<forall>x\<in>A. x dvd \<Prod>A" by (intro ballI dvd_setprod)
+    moreover from `finite A` have "\<forall>x\<in>A. x dvd \<Prod>A" by blast
     ultimately have "\<exists>l. l \<noteq> 0 \<and> (\<forall>x\<in>A. x dvd l)" by blast
     with Lcm0_iff' have "Lcm A \<noteq> 0" by simp
   }
diff -r 348561aa3869 -r ec2b4270a502 src/HOL/Number_Theory/UniqueFactorization.thy
--- a/src/HOL/Number_Theory/UniqueFactorization.thy	Mon Nov 17 14:55:33 2014 +0100
+++ b/src/HOL/Number_Theory/UniqueFactorization.thy	Mon Nov 17 14:55:34 2014 +0100
@@ -79,7 +79,7 @@
   assume M: "a : set_of M"
   with assms have a: "prime a" by auto
   with M have "a ^ count M a dvd (PROD i :# M. i)"
-    by (auto simp add: msetprod_multiplicity intro: dvd_setprod)
+    by (auto simp add: msetprod_multiplicity)
   also have "... dvd (PROD i :# N. i)" by (rule assms)
   also have "... = (PROD i : (set_of N). i ^ (count N i))"
     by (simp add: msetprod_multiplicity)
@@ -309,7 +309,7 @@
     apply (simp add: set_of_def msetprod_multiplicity)
     done
   with `f \<in> multiset` have "count (multiset_prime_factorization n) = f"
-    by (simp add: Abs_multiset_inverse)
+    by simp
   with S_eq show ?thesis
     by (simp add: set_of_def multiset_def prime_factors_nat_def multiplicity_nat_def)
 qed
@@ -681,7 +681,7 @@
   apply (rule dvd_trans) 
   apply (rule dvd_power [where x = p and n = "multiplicity p n"])
   apply (subst (asm) prime_factors_altdef_nat, force)
-  apply (rule dvd_setprod)
+  apply rule
   apply auto
   apply (metis One_nat_def Zero_not_Suc dvd_multiplicity_nat le0 le_antisym multiplicity_not_factor_nat multiplicity_prime_nat)  
   done