--- a/src/HOL/Finite_Set.thy Wed Apr 01 18:41:15 2009 +0200
+++ b/src/HOL/Finite_Set.thy Wed Apr 01 22:29:10 2009 +0200
@@ -1805,32 +1805,19 @@
apply (auto simp add: setprod_def)
done
-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}) =
--- a/src/HOL/Int.thy Wed Apr 01 18:41:15 2009 +0200
+++ b/src/HOL/Int.thy Wed Apr 01 22:29:10 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]
--- a/src/HOL/Library/Binomial.thy Wed Apr 01 18:41:15 2009 +0200
+++ b/src/HOL/Library/Binomial.thy Wed Apr 01 22:29:10 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
--- a/src/HOL/Library/Determinants.thy Wed Apr 01 18:41:15 2009 +0200
+++ b/src/HOL/Library/Determinants.thy Wed Apr 01 22:29:10 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: