# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1653322917 -3600
# Node ID 4c3bc0d2568f19fc11510010ff2cc53497715724
# Parent  7c2fe41f5ee8cde79e6d30d31b475b7ab08b0669
Eliminated two unnecessary inductions

diff -r 7c2fe41f5ee8 -r 4c3bc0d2568f src/HOL/Groups_Big.thy
--- 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"