author paulson Mon, 23 May 2022 17:21:57 +0100 changeset 75461 4c3bc0d2568f parent 75460 7c2fe41f5ee8 child 75462 7448423e5dba
Eliminated two unnecessary inductions
 src/HOL/Groups_Big.thy file | annotate | diff | comparison | revisions
```--- a/src/HOL/Groups_Big.thy	Mon May 23 10:23:33 2022 +0200
+++ b/src/HOL/Groups_Big.thy	Mon May 23 17:21:57 2022 +0100
@@ -695,29 +695,18 @@
by simp (subst sum.union_disjoint, auto)+
qed

+(*Like sum.subset_diff but expressed perhaps more conveniently using subtraction*)
+lemma sum_diff:
+  fixes f :: "'b \<Rightarrow> 'a::ab_group_add"
+  assumes "finite A" "B \<subseteq> A"
+  shows "sum f (A - B) = sum f A - sum f B"
+  using sum.subset_diff [of B A f] assms by simp
+
lemma sum_diff1:
fixes f :: "'b \<Rightarrow> 'a::ab_group_add"
assumes "finite A"
shows "sum f (A - {a}) = (if a \<in> A then sum f A - f a else sum f A)"
-  using assms by induct (auto simp: insert_Diff_if)
-
-lemma sum_diff:
-  fixes f :: "'b \<Rightarrow> 'a::ab_group_add"
-  assumes "finite A" "B \<subseteq> A"
-  shows "sum f (A - B) = sum f A - sum f B"
-proof -
-  from assms(2,1) have "finite B" by (rule finite_subset)
-  from this \<open>B \<subseteq> A\<close>
-  show ?thesis
-  proof induct
-    case empty
-    thus ?case by simp
-  next
-    case (insert x F)
-    with \<open>finite A\<close> \<open>finite B\<close> show ?case
-      by (simp add: Diff_insert[where a=x and B=F] sum_diff1 insert_absorb)
-  qed
-qed
+  using assms by (simp add: sum_diff)

lemma sum_diff1'_aux:
fixes f :: "'a \<Rightarrow> 'b::ab_group_add"```