src/HOL/Big_Operators.thy
 changeset 41550 efa734d9b221 parent 40786 0a54cfc9add3 child 42284 326f57825e1a
```     1.1 --- a/src/HOL/Big_Operators.thy	Fri Jan 14 15:43:04 2011 +0100
1.2 +++ b/src/HOL/Big_Operators.thy	Fri Jan 14 15:44:47 2011 +0100
1.3 @@ -172,7 +172,7 @@
1.4  lemma (in comm_monoid_add) setsum_reindex_cong:
1.5     "[|inj_on f A; B = f ` A; !!a. a:A \<Longrightarrow> g a = h (f a)|]
1.6      ==> setsum h B = setsum g A"
1.7 -  by (simp add: setsum_reindex cong: setsum_cong)
1.8 +  by (simp add: setsum_reindex)
1.9
1.10  lemma (in comm_monoid_add) setsum_0[simp]: "setsum (%i. 0) A = 0"
1.11    by (cases "finite A") (erule finite_induct, auto)
1.12 @@ -288,7 +288,7 @@
1.13    shows "setsum f (UNION I A) = (\<Sum>i\<in>I. setsum f (A i))"
1.14  proof -
1.15    interpret comm_monoid_mult "op +" 0 by (fact comm_monoid_mult)
1.16 -  from assms show ?thesis by (simp add: setsum_def fold_image_UN_disjoint cong: setsum_cong)
1.17 +  from assms show ?thesis by (simp add: setsum_def fold_image_UN_disjoint)
1.18  qed
1.19
1.20  text{*No need to assume that @{term C} is finite.  If infinite, the rhs is
1.21 @@ -310,7 +310,7 @@
1.22    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)"
1.23  proof -
1.24    interpret comm_monoid_mult "op +" 0 by (fact comm_monoid_mult)
1.25 -  from assms show ?thesis by (simp add: setsum_def fold_image_Sigma split_def cong: setsum_cong)
1.26 +  from assms show ?thesis by (simp add: setsum_def fold_image_Sigma split_def)
1.27  qed
1.28
1.29  text{*Here we can eliminate the finiteness assumptions, by cases.*}
1.30 @@ -498,7 +498,7 @@
1.31    assumes "finite A"  "A \<noteq> {}"
1.32      and "!!x. x:A \<Longrightarrow> f x < g x"
1.33    shows "setsum f A < setsum g A"
1.34 -  using prems
1.35 +  using assms
1.36  proof (induct rule: finite_ne_induct)
1.37    case singleton thus ?case by simp
1.38  next
1.39 @@ -775,7 +775,7 @@
1.40  apply (subgoal_tac
1.41           "setsum (%i. card (A i)) I = setsum (%i. (setsum (%x. 1) (A i))) I")
1.42  apply (simp add: setsum_UN_disjoint del: setsum_constant)
1.43 -apply (simp cong: setsum_cong)
1.44 +apply simp
1.45  done
1.46
1.47  lemma card_Union_disjoint:
1.48 @@ -947,7 +947,7 @@
1.49    let ?f = "(\<lambda>k. if k=a then b k else 1)"
1.50    {assume a: "a \<notin> S"
1.51      hence "\<forall> k\<in> S. ?f k = 1" by simp
1.52 -    hence ?thesis  using a by (simp add: setprod_1 cong add: setprod_cong) }
1.53 +    hence ?thesis  using a by (simp add: setprod_1) }
1.54    moreover
1.55    {assume a: "a \<in> S"
1.56      let ?A = "S - {a}"
1.57 @@ -959,7 +959,7 @@
1.58      have "setprod ?f ?A * setprod ?f ?B = setprod ?f S"
1.59        using setprod_Un_disjoint[OF fAB dj, of ?f, unfolded eq[symmetric]]
1.60        by simp
1.61 -    then have ?thesis  using a by (simp add: fA1 cong add: setprod_cong cong del: if_weak_cong)}
1.62 +    then have ?thesis using a by (simp add: fA1 cong: setprod_cong cong del: if_weak_cong)}
1.63    ultimately show ?thesis by blast
1.64  qed
1.65
1.66 @@ -975,7 +975,7 @@
1.67      "finite I ==> (ALL i:I. finite (A i)) ==>
1.68          (ALL i:I. ALL j:I. i \<noteq> j --> A i Int A j = {}) ==>
1.69        setprod f (UNION I A) = setprod (%i. setprod f (A i)) I"
1.70 -by(simp add: setprod_def fold_image_UN_disjoint cong: setprod_cong)
1.71 +  by (simp add: setprod_def fold_image_UN_disjoint)
1.72
1.73  lemma setprod_Union_disjoint:
1.74    "[| (ALL A:C. finite A);
1.75 @@ -990,7 +990,7 @@
1.76  lemma setprod_Sigma: "finite A ==> ALL x:A. finite (B x) ==>
1.77      (\<Prod>x\<in>A. (\<Prod>y\<in> B x. f x y)) =
1.78      (\<Prod>(x,y)\<in>(SIGMA x:A. B x). f x y)"
1.79 -by(simp add:setprod_def fold_image_Sigma split_def cong:setprod_cong)
1.80 +by(simp add:setprod_def fold_image_Sigma split_def)
1.81
1.82  text{*Here we can eliminate the finiteness assumptions, by cases.*}
1.83  lemma setprod_cartesian_product:
1.84 @@ -1332,7 +1332,7 @@
1.85    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}"
1.86  using A proof (induct rule: finite_ne_induct)
1.87    case singleton thus ?case
1.88 -    by (simp add: sup_Inf1_distrib [OF B] fold1_singleton_def [OF Inf_fin_def])
1.89 +    by (simp add: sup_Inf1_distrib [OF B])
1.90  next
1.91    interpret ab_semigroup_idem_mult inf
1.92      by (rule ab_semigroup_idem_mult_inf)
1.93 @@ -1347,7 +1347,7 @@
1.94    qed
1.95    have ne: "{sup a b |a b. a \<in> A \<and> b \<in> B} \<noteq> {}" using insert B by blast
1.96    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)"
1.97 -    using insert by (simp add: fold1_insert_idem_def [OF Inf_fin_def])
1.98 +    using insert by simp
1.99    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)
1.100    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})"
1.101      using insert by(simp add:sup_Inf1_distrib[OF B])
1.102 @@ -1391,7 +1391,7 @@
1.103    interpret ab_semigroup_idem_mult sup
1.104      by (rule ab_semigroup_idem_mult_sup)
1.105    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)"
1.106 -    using insert by (simp add: fold1_insert_idem_def [OF Sup_fin_def])
1.107 +    using insert by simp
1.108    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)
1.109    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})"
1.110      using insert by(simp add:inf_Sup1_distrib[OF B])
1.111 @@ -1551,15 +1551,15 @@
1.112  next
1.113    interpret ab_semigroup_idem_mult min
1.114      by (rule ab_semigroup_idem_mult_min)
1.115 -  assume "A \<noteq> B"
1.116 +  assume neq: "A \<noteq> B"
1.117    have B: "B = A \<union> (B-A)" using `A \<subseteq> B` by blast
1.118    have "fold1 min B = fold1 min (A \<union> (B-A))" by(subst B)(rule refl)
1.119    also have "\<dots> = min (fold1 min A) (fold1 min (B-A))"
1.120    proof -
1.121      have "finite A" by(rule finite_subset[OF `A \<subseteq> B` `finite B`])
1.122 -    moreover have "finite(B-A)" by(rule finite_Diff[OF `finite B`]) (* by(blast intro:finite_Diff prems) fails *)
1.123 -    moreover have "(B-A) \<noteq> {}" using prems by blast
1.124 -    moreover have "A Int (B-A) = {}" using prems by blast
1.125 +    moreover have "finite(B-A)" by(rule finite_Diff[OF `finite B`])
1.126 +    moreover have "(B-A) \<noteq> {}" using assms neq by blast
1.127 +    moreover have "A Int (B-A) = {}" using assms by blast
1.128      ultimately show ?thesis using `A \<noteq> {}` by (rule_tac fold1_Un)
1.129    qed
1.130    also have "\<dots> \<le> fold1 min A" by (simp add: min_le_iff_disj)
```