src/HOL/Finite_Set.thy
 changeset 15315 a358e31572d9 parent 15314 55eec5c6d401 child 15318 e9669e0d6452
```     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.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)
```