diff -r 2c65ad10bec8 -r efa734d9b221 src/HOL/Big_Operators.thy
--- a/src/HOL/Big_Operators.thy	Fri Jan 14 15:43:04 2011 +0100
+++ b/src/HOL/Big_Operators.thy	Fri Jan 14 15:44:47 2011 +0100
@@ -172,7 +172,7 @@
 lemma (in comm_monoid_add) setsum_reindex_cong:
    "[|inj_on f A; B = f ` A; !!a. a:A \<Longrightarrow> g a = h (f a)|] 
     ==> setsum h B = setsum g A"
-  by (simp add: setsum_reindex cong: setsum_cong)
+  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)
@@ -288,7 +288,7 @@
   shows "setsum f (UNION I A) = (\<Sum>i\<in>I. setsum f (A i))"
 proof -
   interpret comm_monoid_mult "op +" 0 by (fact comm_monoid_mult)
-  from assms show ?thesis by (simp add: setsum_def fold_image_UN_disjoint cong: setsum_cong)
+  from assms show ?thesis by (simp add: setsum_def fold_image_UN_disjoint)
 qed
 
 text{*No need to assume that @{term C} is finite.  If infinite, the rhs is
@@ -310,7 +310,7 @@
   shows "(\<Sum>x\<in>A. (\<Sum>y\<in>B x. f x y)) = (\<Sum>(x,y)\<in>(SIGMA x:A. B x). f x y)"
 proof -
   interpret comm_monoid_mult "op +" 0 by (fact comm_monoid_mult)
-  from assms show ?thesis by (simp add: setsum_def fold_image_Sigma split_def cong: setsum_cong)
+  from assms show ?thesis by (simp add: setsum_def fold_image_Sigma split_def)
 qed
 
 text{*Here we can eliminate the finiteness assumptions, by cases.*}
@@ -498,7 +498,7 @@
   assumes "finite A"  "A \<noteq> {}"
     and "!!x. x:A \<Longrightarrow> f x < g x"
   shows "setsum f A < setsum g A"
-  using prems
+  using assms
 proof (induct rule: finite_ne_induct)
   case singleton thus ?case by simp
 next
@@ -775,7 +775,7 @@
 apply (subgoal_tac
          "setsum (%i. card (A i)) I = setsum (%i. (setsum (%x. 1) (A i))) I")
 apply (simp add: setsum_UN_disjoint del: setsum_constant)
-apply (simp cong: setsum_cong)
+apply simp
 done
 
 lemma card_Union_disjoint:
@@ -947,7 +947,7 @@
   let ?f = "(\<lambda>k. if k=a then b k else 1)"
   {assume a: "a \<notin> S"
     hence "\<forall> k\<in> S. ?f k = 1" by simp
-    hence ?thesis  using a by (simp add: setprod_1 cong add: setprod_cong) }
+    hence ?thesis  using a by (simp add: setprod_1) }
   moreover 
   {assume a: "a \<in> S"
     let ?A = "S - {a}"
@@ -959,7 +959,7 @@
     have "setprod ?f ?A * setprod ?f ?B = setprod ?f S"
       using setprod_Un_disjoint[OF fAB dj, of ?f, unfolded eq[symmetric]]
       by simp
-    then have ?thesis  using a by (simp add: fA1 cong add: setprod_cong cong del: if_weak_cong)}
+    then have ?thesis using a by (simp add: fA1 cong: setprod_cong cong del: if_weak_cong)}
   ultimately show ?thesis by blast
 qed
 
@@ -975,7 +975,7 @@
     "finite I ==> (ALL i:I. finite (A i)) ==>
         (ALL i:I. ALL j:I. i \<noteq> j --> A i Int A j = {}) ==>
       setprod f (UNION I A) = setprod (%i. setprod f (A i)) I"
-by(simp add: setprod_def fold_image_UN_disjoint cong: setprod_cong)
+  by (simp add: setprod_def fold_image_UN_disjoint)
 
 lemma setprod_Union_disjoint:
   "[| (ALL A:C. finite A);
@@ -990,7 +990,7 @@
 lemma setprod_Sigma: "finite A ==> ALL x:A. finite (B x) ==>
     (\<Prod>x\<in>A. (\<Prod>y\<in> B x. f x y)) =
     (\<Prod>(x,y)\<in>(SIGMA x:A. B x). f x y)"
-by(simp add:setprod_def fold_image_Sigma split_def cong:setprod_cong)
+by(simp add:setprod_def fold_image_Sigma split_def)
 
 text{*Here we can eliminate the finiteness assumptions, by cases.*}
 lemma setprod_cartesian_product: 
@@ -1332,7 +1332,7 @@
   shows "sup (\<Sqinter>\<^bsub>fin\<^esub>A) (\<Sqinter>\<^bsub>fin\<^esub>B) = \<Sqinter>\<^bsub>fin\<^esub>{sup a b|a b. a \<in> A \<and> b \<in> B}"
 using A proof (induct rule: finite_ne_induct)
   case singleton thus ?case
-    by (simp add: sup_Inf1_distrib [OF B] fold1_singleton_def [OF Inf_fin_def])
+    by (simp add: sup_Inf1_distrib [OF B])
 next
   interpret ab_semigroup_idem_mult inf
     by (rule ab_semigroup_idem_mult_inf)
@@ -1347,7 +1347,7 @@
   qed
   have ne: "{sup a b |a b. a \<in> A \<and> b \<in> B} \<noteq> {}" using insert B by blast
   have "sup (\<Sqinter>\<^bsub>fin\<^esub>(insert x A)) (\<Sqinter>\<^bsub>fin\<^esub>B) = sup (inf x (\<Sqinter>\<^bsub>fin\<^esub>A)) (\<Sqinter>\<^bsub>fin\<^esub>B)"
-    using insert by (simp add: fold1_insert_idem_def [OF Inf_fin_def])
+    using insert by simp
   also have "\<dots> = inf (sup x (\<Sqinter>\<^bsub>fin\<^esub>B)) (sup (\<Sqinter>\<^bsub>fin\<^esub>A) (\<Sqinter>\<^bsub>fin\<^esub>B))" by(rule sup_inf_distrib2)
   also have "\<dots> = inf (\<Sqinter>\<^bsub>fin\<^esub>{sup x b|b. b \<in> B}) (\<Sqinter>\<^bsub>fin\<^esub>{sup a b|a b. a \<in> A \<and> b \<in> B})"
     using insert by(simp add:sup_Inf1_distrib[OF B])
@@ -1391,7 +1391,7 @@
   interpret ab_semigroup_idem_mult sup
     by (rule ab_semigroup_idem_mult_sup)
   have "inf (\<Squnion>\<^bsub>fin\<^esub>(insert x A)) (\<Squnion>\<^bsub>fin\<^esub>B) = inf (sup x (\<Squnion>\<^bsub>fin\<^esub>A)) (\<Squnion>\<^bsub>fin\<^esub>B)"
-    using insert by (simp add: fold1_insert_idem_def [OF Sup_fin_def])
+    using insert by simp
   also have "\<dots> = sup (inf x (\<Squnion>\<^bsub>fin\<^esub>B)) (inf (\<Squnion>\<^bsub>fin\<^esub>A) (\<Squnion>\<^bsub>fin\<^esub>B))" by(rule inf_sup_distrib2)
   also have "\<dots> = sup (\<Squnion>\<^bsub>fin\<^esub>{inf x b|b. b \<in> B}) (\<Squnion>\<^bsub>fin\<^esub>{inf a b|a b. a \<in> A \<and> b \<in> B})"
     using insert by(simp add:inf_Sup1_distrib[OF B])
@@ -1551,15 +1551,15 @@
 next
   interpret ab_semigroup_idem_mult min
     by (rule ab_semigroup_idem_mult_min)
-  assume "A \<noteq> B"
+  assume neq: "A \<noteq> B"
   have B: "B = A \<union> (B-A)" using `A \<subseteq> B` by blast
   have "fold1 min B = fold1 min (A \<union> (B-A))" by(subst B)(rule refl)
   also have "\<dots> = min (fold1 min A) (fold1 min (B-A))"
   proof -
     have "finite A" by(rule finite_subset[OF `A \<subseteq> B` `finite B`])
-    moreover have "finite(B-A)" by(rule finite_Diff[OF `finite B`]) (* by(blast intro:finite_Diff prems) fails *)
-    moreover have "(B-A) \<noteq> {}" using prems by blast
-    moreover have "A Int (B-A) = {}" using prems by blast
+    moreover have "finite(B-A)" by(rule finite_Diff[OF `finite B`])
+    moreover have "(B-A) \<noteq> {}" using assms neq by blast
+    moreover have "A Int (B-A) = {}" using assms by blast
     ultimately show ?thesis using `A \<noteq> {}` by (rule_tac fold1_Un)
   qed
   also have "\<dots> \<le> fold1 min A" by (simp add: min_le_iff_disj)