merged
authornipkow
Wed, 01 Apr 2009 22:29:27 +0200
changeset 30844 7d0e10a961a6
parent 30842 d007dee0c372 (diff)
parent 30843 3419ca741dbf (current diff)
child 30846 fd8ed5a39a8e
merged
src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Wed Apr 01 22:29:10 2009 +0200
+++ b/src/HOL/Finite_Set.thy	Wed Apr 01 22:29:27 2009 +0200
@@ -1788,22 +1788,12 @@
 done
 
 lemma setprod_nonneg [rule_format]:
-   "(ALL x: A. (0::'a::ordered_idom) \<le> f x) --> 0 \<le> setprod f A"
-apply (case_tac "finite A")
-apply (induct set: finite, force, clarsimp)
-apply (subgoal_tac "0 * 0 \<le> f x * setprod f F", force)
-apply (rule mult_mono, assumption+)
-apply (auto simp add: setprod_def)
-done
-
-lemma setprod_pos [rule_format]: "(ALL x: A. (0::'a::ordered_idom) < f x)
+   "(ALL x: A. (0::'a::ordered_semidom) \<le> f x) --> 0 \<le> setprod f A"
+by (cases "finite A", induct set: finite, simp_all add: mult_nonneg_nonneg)
+
+lemma setprod_pos [rule_format]: "(ALL x: A. (0::'a::ordered_semidom) < f x)
   --> 0 < setprod f A"
-apply (case_tac "finite A")
-apply (induct set: finite, force, clarsimp)
-apply (subgoal_tac "0 * 0 < f x * setprod f F", force)
-apply (rule mult_strict_mono, assumption+)
-apply (auto simp add: setprod_def)
-done
+by (cases "finite A", induct set: finite, simp_all add: mult_pos_pos)
 
 lemma setprod_zero_iff[simp]: "finite A ==> 
   (setprod f A = (0::'a::{comm_semiring_1,no_zero_divisors})) =