# HG changeset patch
# User nipkow
# Date 1345036242 -7200
# Node ID 65b205a6f56a04eeed46fe91db014d7f267fbba8
# Parent  20336d435682b94f1fce0818bb32c4efcc3902ba# Parent  21d4ed91912fd0d1830621729cda8cc69d822c0f
merged

diff -r 20336d435682 -r 65b205a6f56a src/HOL/Big_Operators.thy
--- a/src/HOL/Big_Operators.thy	Wed Aug 15 13:43:49 2012 +0200
+++ b/src/HOL/Big_Operators.thy	Wed Aug 15 15:10:42 2012 +0200
@@ -39,6 +39,12 @@
   then show ?thesis unfolding `A = B` by simp
 qed
 
+lemma F_neutral[simp]: "F (%i. 1) A = 1"
+by (cases "finite A") (simp_all add: neutral)
+
+lemma F_neutral': "ALL a:A. g a = 1 \<Longrightarrow> F g A = 1"
+by (simp cong: F_cong)
+
 lemma If_cases:
   fixes P :: "'b \<Rightarrow> bool" and g h :: "'b \<Rightarrow> 'a"
   assumes fA: "finite A"
@@ -202,11 +208,8 @@
     ==> setsum h B = setsum g A"
   by (simp add: setsum_reindex)
 
-lemma (in comm_monoid_add) setsum_0[simp]: "setsum (%i. 0) A = 0"
-  by (cases "finite A") (erule finite_induct, auto)
-
-lemma (in comm_monoid_add) setsum_0': "ALL a:A. f a = 0 ==> setsum f A = 0"
-  by (simp add:setsum_cong)
+lemmas setsum_0 = setsum.F_neutral
+lemmas setsum_0' = setsum.F_neutral'
 
 lemma (in comm_monoid_add) setsum_Un_Int: "finite A ==> finite B ==>
   setsum g (A Un B) + setsum g (A Int B) = setsum g A + setsum g B"
@@ -942,16 +945,9 @@
   using I0 by auto
 
 
-lemma setprod_1: "setprod (%i. 1) A = 1"
-apply (case_tac "finite A")
-apply (erule finite_induct, auto simp add: mult_ac)
-done
+lemmas setprod_1 = setprod.F_neutral
+lemmas setprod_1' = setprod.F_neutral'
 
-lemma setprod_1': "ALL a:F. f a = 1 ==> setprod f F = 1"
-apply (subgoal_tac "setprod f F = setprod (%x. 1) F")
-apply (erule ssubst, rule setprod_1)
-apply (rule setprod_cong, auto)
-done
 
 lemma setprod_Un_Int: "finite A ==> finite B
     ==> setprod g (A Un B) * setprod g (A Int B) = setprod g A * setprod g B"
diff -r 20336d435682 -r 65b205a6f56a src/HOL/Number_Theory/UniqueFactorization.thy
--- a/src/HOL/Number_Theory/UniqueFactorization.thy	Wed Aug 15 13:43:49 2012 +0200
+++ b/src/HOL/Number_Theory/UniqueFactorization.thy	Wed Aug 15 15:10:42 2012 +0200
@@ -544,12 +544,7 @@
   apply (erule ssubst)
   apply (subst setprod_Un_disjoint)
   apply auto
-  apply (subgoal_tac "(\<Prod>p\<in>prime_factors l - prime_factors k. p ^ multiplicity p k) = 
-      (\<Prod>p\<in>prime_factors l - prime_factors k. 1)")
-  apply (erule ssubst)
-  apply (simp add: setprod_1)
-  apply (erule prime_factorization_nat)
-  apply (rule setprod_cong, auto)
+  apply(simp add: prime_factorization_nat)
   apply (subgoal_tac "prime_factors k Un prime_factors l = prime_factors l Un 
       (prime_factors k - prime_factors l)")
   apply (erule ssubst)
@@ -557,9 +552,7 @@
   apply auto
   apply (subgoal_tac "(\<Prod>p\<in>prime_factors k - prime_factors l. p ^ multiplicity p l) = 
       (\<Prod>p\<in>prime_factors k - prime_factors l. 1)")
-  apply (erule ssubst)
-  apply (simp add: setprod_1)
-  apply (erule prime_factorization_nat)
+  apply (simp add: prime_factorization_nat)
   apply (rule setprod_cong, auto)
   done