renamed 2 lemmas
authornipkow
Tue Nov 23 16:42:54 2004 +0100 (2004-11-23)
changeset 15315a358e31572d9
parent 15314 55eec5c6d401
child 15316 2a6ff941a115
renamed 2 lemmas
src/HOL/Finite_Set.thy
     1.1 --- a/src/HOL/Finite_Set.thy	Tue Nov 23 15:50:27 2004 +0100
     1.2 +++ b/src/HOL/Finite_Set.thy	Tue Nov 23 16:42:54 2004 +0100
     1.3 @@ -962,7 +962,7 @@
     1.4        setsum f A + setsum f B - setsum f (A Int B)"
     1.5    by (subst setsum_Un_Int [symmetric], auto simp add: ring_eq_simps)
     1.6  
     1.7 -lemma setsum_diff1: "(setsum f (A - {a}) :: nat) =
     1.8 +lemma setsum_diff1_nat: "(setsum f (A - {a}) :: nat) =
     1.9      (if a:A then setsum f A - f a else setsum f A)"
    1.10    apply (case_tac "finite A")
    1.11     prefer 2 apply (simp add: setsum_def)
    1.12 @@ -971,9 +971,14 @@
    1.13    apply (drule_tac a = a in mk_disjoint_insert, auto)
    1.14    done
    1.15  
    1.16 +lemma setsum_diff1: "finite A \<Longrightarrow>
    1.17 +  (setsum f (A - {a}) :: ('a::{pordered_ab_group_add})) =
    1.18 +  (if a:A then setsum f A - f a else setsum f A)"
    1.19 +  by (erule finite_induct) (auto simp add: insert_Diff_if)
    1.20 +
    1.21  (* By Jeremy Siek: *)
    1.22  
    1.23 -lemma setsum_diff: 
    1.24 +lemma setsum_diff_nat: 
    1.25    assumes finB: "finite B"
    1.26    shows "B \<subseteq> A \<Longrightarrow> (setsum f (A - B) :: nat) = (setsum f A) - (setsum f B)"
    1.27  using finB
    1.28 @@ -985,7 +990,7 @@
    1.29      and IH: "F \<subseteq> A \<Longrightarrow> setsum f (A - F) = setsum f A - setsum f F"
    1.30    from xnotinF xFinA have xinAF: "x \<in> (A - F)" by simp
    1.31    from xinAF have A: "setsum f ((A - F) - {x}) = setsum f (A - F) - f x"
    1.32 -    by (simp add: setsum_diff1)
    1.33 +    by (simp add: setsum_diff1_nat)
    1.34    from xFinA have "F \<subseteq> A" by simp
    1.35    with IH have "setsum f (A - F) = setsum f A - setsum f F" by simp
    1.36    with A have B: "setsum f ((A - F) - {x}) = setsum f A - setsum f F - f x"
    1.37 @@ -999,6 +1004,26 @@
    1.38    thus "setsum f (A - insert x F) = setsum f A - setsum f (insert x F)" by simp
    1.39  qed
    1.40  
    1.41 +lemma setsum_diff:
    1.42 +  assumes le: "finite A" "B \<subseteq> A"
    1.43 +  shows "setsum f (A - B) = setsum f A - ((setsum f B)::('a::pordered_ab_group_add))"
    1.44 +proof -
    1.45 +  from le have finiteB: "finite B" using finite_subset by auto
    1.46 +  show ?thesis using le finiteB
    1.47 +    proof (induct rule: Finites.induct[OF finiteB])
    1.48 +      case 1
    1.49 +      thus ?case by auto
    1.50 +    next
    1.51 +      case 2
    1.52 +      thus ?case using le 
    1.53 +	apply auto
    1.54 +	apply (subst Diff_insert)
    1.55 +	apply (subst setsum_diff1)
    1.56 +	apply (auto simp add: insert_absorb)
    1.57 +	done
    1.58 +    qed
    1.59 +  qed
    1.60 +
    1.61  lemma setsum_mono:
    1.62    assumes le: "\<And>i. i\<in>K \<Longrightarrow> f (i::'a) \<le> ((g i)::('b::{comm_monoid_add, pordered_ab_semigroup_add}))"
    1.63    shows "(\<Sum>i\<in>K. f i) \<le> (\<Sum>i\<in>K. g i)"
    1.64 @@ -1019,30 +1044,6 @@
    1.65      by (simp add: setsum_def)
    1.66  qed
    1.67  
    1.68 -lemma finite_setsum_diff1: "finite A \<Longrightarrow> (setsum f (A - {a}) :: ('a::{pordered_ab_group_add})) =
    1.69 -    (if a:A then setsum f A - f a else setsum f A)"
    1.70 -  by (erule finite_induct) (auto simp add: insert_Diff_if)
    1.71 -
    1.72 -lemma finite_setsum_diff:
    1.73 -  assumes le: "finite A" "B \<subseteq> A"
    1.74 -  shows "setsum f (A - B) = setsum f A - ((setsum f B)::('a::pordered_ab_group_add))"
    1.75 -proof -
    1.76 -  from le have finiteB: "finite B" using finite_subset by auto
    1.77 -  show ?thesis using le finiteB
    1.78 -    proof (induct rule: Finites.induct[OF finiteB])
    1.79 -      case 1
    1.80 -      thus ?case by auto
    1.81 -    next
    1.82 -      case 2
    1.83 -      thus ?case using le 
    1.84 -	apply auto
    1.85 -	apply (subst Diff_insert)
    1.86 -	apply (subst finite_setsum_diff1)
    1.87 -	apply (auto simp add: insert_absorb)
    1.88 -	done
    1.89 -    qed
    1.90 -  qed
    1.91 -
    1.92  lemma setsum_negf: "finite A ==> setsum (%x. - (f x)::'a::ab_group_add) A =
    1.93    - setsum f A"
    1.94    by (induct set: Finites, auto)