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)