# HG changeset patch
# User nipkow
# Date 1238617767 -7200
# Node ID 7d0e10a961a623bd7f80604cc64349d633c2aefe
# Parent  d007dee0c372b80fcd2c55be7bb90968148f42cc# Parent  3419ca741dbf1a47fb84e9b39389e54720606cc7
merged

diff -r d007dee0c372 -r 7d0e10a961a6 src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Wed Apr 01 11:34:21 2009 -0700
+++ b/src/HOL/Finite_Set.thy	Wed Apr 01 22:29:27 2009 +0200
@@ -1795,32 +1795,19 @@
   --> 0 < setprod f A"
 by (cases "finite A", induct set: finite, simp_all add: mult_pos_pos)
 
-lemma setprod_nonzero [rule_format]:
-  "(ALL x y. (x::'a::comm_semiring_1) * y = 0 --> x = 0 | y = 0) ==>
-    finite A ==> (ALL x: A. f x \<noteq> (0::'a)) --> setprod f A \<noteq> 0"
-by (erule finite_induct, auto)
-
-lemma setprod_zero_eq:
-    "(ALL x y. (x::'a::comm_semiring_1) * y = 0 --> x = 0 | y = 0) ==>
-     finite A ==> (setprod f A = (0::'a)) = (EX x: A. f x = 0)"
-by (insert setprod_zero [of A f] setprod_nonzero [of A f], blast)
-
-lemma setprod_nonzero_field:
-    "finite A ==> (ALL x: A. f x \<noteq> (0::'a::idom)) ==> setprod f A \<noteq> 0"
-by (rule setprod_nonzero, auto)
-
-lemma setprod_zero_eq_field:
-    "finite A ==> (setprod f A = (0::'a::idom)) = (EX x: A. f x = 0)"
-by (rule setprod_zero_eq, auto)
+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)
+
+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])
 
 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)"
-apply (subst setprod_Un_Int [symmetric], auto)
-apply (subgoal_tac "finite (A Int B)")
-apply (frule setprod_nonzero_field [of "A Int B" f], assumption)
-apply (subst times_divide_eq_right [THEN sym], auto)
-done
+by (subst setprod_Un_Int [symmetric], auto)
 
 lemma setprod_diff1: "finite A ==> f a \<noteq> 0 ==>
   (setprod f (A - {a}) :: 'a :: {field}) =
diff -r d007dee0c372 -r 7d0e10a961a6 src/HOL/Int.thy
--- a/src/HOL/Int.thy	Wed Apr 01 11:34:21 2009 -0700
+++ b/src/HOL/Int.thy	Wed Apr 01 22:29:27 2009 +0200
@@ -1382,8 +1382,6 @@
 
 subsection {* @{term setsum} and @{term setprod} *}
 
-text {*By Jeremy Avigad*}
-
 lemma of_nat_setsum: "of_nat (setsum f A) = (\<Sum>x\<in>A. of_nat(f x))"
   apply (cases "finite A")
   apply (erule finite_induct, auto)
@@ -1404,26 +1402,6 @@
   apply (erule finite_induct, auto)
   done
 
-lemma setprod_nonzero_nat:
-    "finite A ==> (\<forall>x \<in> A. f x \<noteq> (0::nat)) ==> setprod f A \<noteq> 0"
-  by (rule setprod_nonzero, auto)
-
-lemma setprod_pos_nat:
-  "finite S ==> (ALL x : S. f x > (0::nat)) ==> setprod f S > 0"
-using setprod_nonzero_nat by simp
-
-lemma setprod_zero_eq_nat:
-    "finite A ==> (setprod f A = (0::nat)) = (\<exists>x \<in> A. f x = 0)"
-  by (rule setprod_zero_eq, auto)
-
-lemma setprod_nonzero_int:
-    "finite A ==> (\<forall>x \<in> A. f x \<noteq> (0::int)) ==> setprod f A \<noteq> 0"
-  by (rule setprod_nonzero, auto)
-
-lemma setprod_zero_eq_int:
-    "finite A ==> (setprod f A = (0::int)) = (\<exists>x \<in> A. f x = 0)"
-  by (rule setprod_zero_eq, auto)
-
 lemmas int_setsum = of_nat_setsum [where 'a=int]
 lemmas int_setprod = of_nat_setprod [where 'a=int]
 
diff -r d007dee0c372 -r 7d0e10a961a6 src/HOL/Library/Binomial.thy
--- a/src/HOL/Library/Binomial.thy	Wed Apr 01 11:34:21 2009 -0700
+++ b/src/HOL/Library/Binomial.thy	Wed Apr 01 22:29:27 2009 +0200
@@ -267,8 +267,6 @@
   moreover
   {assume n0: "n \<noteq> 0"
     then have ?thesis apply (simp add: h pochhammer_Suc_setprod)
-  apply (rule iffD2[OF setprod_zero_eq])
-  apply auto
   apply (rule_tac x="n" in bexI)
   using h kn by auto}
 ultimately show ?thesis by blast
@@ -281,8 +279,7 @@
   moreover
   {fix h assume h: "k = Suc h"
     then have ?thesis apply (simp add: pochhammer_Suc_setprod)
-      apply (subst setprod_zero_eq_field)
-      using h kn by (auto simp add: ring_simps)}
+      using h kn by (auto simp add: algebra_simps)}
   ultimately show ?thesis by (cases k, auto)
 qed
 
@@ -299,15 +296,14 @@
   where "a gchoose n = (if n = 0 then 1 else (setprod (\<lambda>i. a - of_nat i) {0 .. n - 1}) / of_nat (fact n))"
 
 lemma gbinomial_0[simp]: "a gchoose 0 = 1" "0 gchoose (Suc n) = 0"
-  apply (simp_all add: gbinomial_def)
-  apply (subgoal_tac "(\<Prod>i\<Colon>nat\<in>{0\<Colon>nat..n}. - of_nat i) = (0::'b)")
-  apply simp
-  apply (rule iffD2[OF setprod_zero_eq])
-  by auto
+apply (simp_all add: gbinomial_def)
+apply (subgoal_tac "(\<Prod>i\<Colon>nat\<in>{0\<Colon>nat..n}. - of_nat i) = (0::'b)")
+ apply (simp del:setprod_zero_iff)
+apply simp
+done
 
 lemma gbinomial_pochhammer: "a gchoose n = (- 1) ^ n * pochhammer (- a) n / of_nat (fact n)"
 proof-
-
   {assume "n=0" then have ?thesis by simp}
   moreover
   {assume n0: "n\<noteq>0"
@@ -388,7 +384,6 @@
       unfolding mult_assoc[symmetric] 
       unfolding setprod_timesf[symmetric]
       apply simp
-      apply (rule disjI2)
       apply (rule strong_setprod_reindex_cong[where f= "op - n"])
       apply (auto simp add: inj_on_def image_iff Bex_def)
       apply presburger
diff -r d007dee0c372 -r 7d0e10a961a6 src/HOL/Library/Determinants.thy
--- a/src/HOL/Library/Determinants.thy	Wed Apr 01 11:34:21 2009 -0700
+++ b/src/HOL/Library/Determinants.thy	Wed Apr 01 22:29:27 2009 +0200
@@ -310,10 +310,7 @@
 using r
 apply (simp add: row_def det_def Cart_eq)
 apply (rule setsum_0')
-apply (clarsimp simp add: sign_nz)
-apply (rule setprod_zero)
-apply simp
-apply auto
+apply (auto simp: sign_nz)
 done
 
 lemma det_zero_column: