Eliminated two unnecessary inductions
authorpaulson <lp15@cam.ac.uk>
Mon, 23 May 2022 17:21:57 +0100
changeset 75955 4c3bc0d2568f
parent 75954 7c2fe41f5ee8
child 75956 7448423e5dba
Eliminated two unnecessary inductions
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"