# HG changeset patch
# User huffman
# Date 1238610684 25200
# Node ID 0813afc975228c8da505ca37e623b1cfde481e1a
# Parent  1344132160bb303faae60525e2d86bd8e0505990
generalized setprod_nonneg and setprod_pos to ordered_semidom, simplified proofs

diff -r 1344132160bb -r 0813afc97522 src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Wed Apr 01 15:16:09 2009 +0200
+++ b/src/HOL/Finite_Set.thy	Wed Apr 01 11:31:24 2009 -0700
@@ -1776,22 +1776,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_nonzero [rule_format]:
   "(ALL x y. (x::'a::comm_semiring_1) * y = 0 --> x = 0 | y = 0) ==>