# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1630705971 -3600
# Node ID e04ec2b9ed9769cdddf9ab037c8cdab2f7f714e8
# Parent  527088d4a89b69db8cd0788e93c4a6d031b90322
some fixes connected with card_Diff_singleton

diff -r 527088d4a89b -r e04ec2b9ed97 src/HOL/Analysis/Affine.thy
--- a/src/HOL/Analysis/Affine.thy	Fri Sep 03 18:20:13 2021 +0100
+++ b/src/HOL/Analysis/Affine.thy	Fri Sep 03 22:52:51 2021 +0100
@@ -798,7 +798,7 @@
   have "card {x - a |x. x \<in> s - {a}} = card (s - {a})"
     unfolding * by (simp add: card_image inj_on_def)
   also have "\<dots> > DIM('a)" using assms(2)
-    unfolding card_Diff_singleton[OF assms(1) \<open>a\<in>s\<close>] by auto
+    unfolding card_Diff_singleton[OF \<open>a\<in>s\<close>] by auto
   finally show ?thesis
     apply (subst insert_Diff[OF \<open>a\<in>s\<close>, symmetric])
     apply (rule dependent_imp_affine_dependent)
@@ -821,9 +821,7 @@
     using \<open>a\<in>S\<close> by (auto simp: span_base span_diff intro: subset_le_dim)
   also have "\<dots> < dim S + 1" by auto
   also have "\<dots> \<le> card (S - {a})"
-    using assms
-    using card_Diff_singleton[OF assms(1) \<open>a\<in>S\<close>]
-    by auto
+    using assms card_Diff_singleton[OF \<open>a\<in>S\<close>] by auto
   finally show ?thesis
     apply (subst insert_Diff[OF \<open>a\<in>S\<close>, symmetric])
     apply (rule dependent_imp_affine_dependent)
diff -r 527088d4a89b -r e04ec2b9ed97 src/HOL/Quotient_Examples/Quotient_FSet.thy
--- a/src/HOL/Quotient_Examples/Quotient_FSet.thy	Fri Sep 03 18:20:13 2021 +0100
+++ b/src/HOL/Quotient_Examples/Quotient_FSet.thy	Fri Sep 03 22:52:51 2021 +0100
@@ -819,8 +819,7 @@
 
 lemma card_remove_fset_le1: 
   shows "card_fset (remove_fset x xs) \<le> card_fset xs"
-  unfolding remove_fset card_fset
-  by (rule card_Diff1_le[OF finite_fset])
+  by simp
 
 lemma card_psubset_fset: 
   shows "ys |\<subseteq>| xs \<Longrightarrow> card_fset ys < card_fset xs \<Longrightarrow> ys |\<subset>| xs"
@@ -835,21 +834,17 @@
 lemma card_minus_insert_fset[simp]:
   assumes "a |\<in>| A" and "a |\<notin>| B"
   shows "card_fset (A - insert_fset a B) = card_fset (A - B) - 1"
-  using assms 
-  unfolding in_fset card_fset minus_fset
-  by (simp add: card_Diff_insert[OF finite_fset])
+  using assms  by (simp add: in_fset card_fset)
 
 lemma card_minus_subset_fset:
   assumes "B |\<subseteq>| A"
   shows "card_fset (A - B) = card_fset A - card_fset B"
   using assms 
-  unfolding subset_fset card_fset minus_fset
-  by (rule card_Diff_subset[OF finite_fset])
+  by (simp add: subset_fset card_fset card_Diff_subset)
 
 lemma card_minus_fset:
   shows "card_fset (A - B) = card_fset A - card_fset (A |\<inter>| B)"
-  unfolding inter_fset card_fset minus_fset
-  by (rule card_Diff_subset_Int) (simp)
+  by (simp add: card_fset card_Diff_subset_Int)
 
 
 subsection \<open>concat_fset\<close>