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 \ 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) = (\i\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 "(\x\A. (\y\B x. f x y)) = (\(x,y)\(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 \ {}" and "!!x. x:A \ 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 = "(\k. if k=a then b k else 1)" {assume a: "a \ S" hence "\ k\ 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 \ 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 \ 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) ==> (\x\A. (\y\ B x. f x y)) = (\(x,y)\(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 (\\<^bsub>fin\<^esub>A) (\\<^bsub>fin\<^esub>B) = \\<^bsub>fin\<^esub>{sup a b|a b. a \ A \ b \ 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 \ A \ b \ B} \ {}" using insert B by blast have "sup (\\<^bsub>fin\<^esub>(insert x A)) (\\<^bsub>fin\<^esub>B) = sup (inf x (\\<^bsub>fin\<^esub>A)) (\\<^bsub>fin\<^esub>B)" - using insert by (simp add: fold1_insert_idem_def [OF Inf_fin_def]) + using insert by simp also have "\ = inf (sup x (\\<^bsub>fin\<^esub>B)) (sup (\\<^bsub>fin\<^esub>A) (\\<^bsub>fin\<^esub>B))" by(rule sup_inf_distrib2) also have "\ = inf (\\<^bsub>fin\<^esub>{sup x b|b. b \ B}) (\\<^bsub>fin\<^esub>{sup a b|a b. a \ A \ b \ 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 (\\<^bsub>fin\<^esub>(insert x A)) (\\<^bsub>fin\<^esub>B) = inf (sup x (\\<^bsub>fin\<^esub>A)) (\\<^bsub>fin\<^esub>B)" - using insert by (simp add: fold1_insert_idem_def [OF Sup_fin_def]) + using insert by simp also have "\ = sup (inf x (\\<^bsub>fin\<^esub>B)) (inf (\\<^bsub>fin\<^esub>A) (\\<^bsub>fin\<^esub>B))" by(rule inf_sup_distrib2) also have "\ = sup (\\<^bsub>fin\<^esub>{inf x b|b. b \ B}) (\\<^bsub>fin\<^esub>{inf a b|a b. a \ A \ b \ 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 \ B" + assume neq: "A \ B" have B: "B = A \ (B-A)" using `A \ B` by blast have "fold1 min B = fold1 min (A \ (B-A))" by(subst B)(rule refl) also have "\ = min (fold1 min A) (fold1 min (B-A))" proof - have "finite A" by(rule finite_subset[OF `A \ 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) \ {}" 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) \ {}" using assms neq by blast + moreover have "A Int (B-A) = {}" using assms by blast ultimately show ?thesis using `A \ {}` by (rule_tac fold1_Un) qed also have "\ \ fold1 min A" by (simp add: min_le_iff_disj)