# HG changeset patch
# User fleury <Mathias.Fleury@mpi-inf.mpg.de>
# Date 1473083270 -7200
# Node ID bcec0534aeea61f54b95265758284ae96bdd3fdb
# Parent  e68a0b651eb540cdd83acebb5f63bcb7faea7067
clean argument of simp add

diff -r e68a0b651eb5 -r bcec0534aeea src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Mon Sep 05 15:47:50 2016 +0200
+++ b/src/HOL/Library/Multiset.thy	Mon Sep 05 15:47:50 2016 +0200
@@ -483,7 +483,7 @@
     by (blast dest: multi_member_split)
   have "add_mset b A = add_mset c (add_mset b A) - {#c#}" by simp
   then have "add_mset b A = add_mset b (add_mset c A) - {#c#}"
-    by (simp add: ac_simps \<open>b \<noteq> c\<close>)
+    by (simp add: \<open>b \<noteq> c\<close>)
   then show ?thesis using B by simp
 qed
 
@@ -1563,7 +1563,7 @@
 
 lemma comp_fun_commute_mset_image: "comp_fun_commute (add_mset \<circ> f)"
 proof
-qed (simp add: ac_simps fun_eq_iff)
+qed (simp add: fun_eq_iff)
 
 lemma image_mset_empty [simp]: "image_mset f {#} = {#}"
   by (simp add: image_mset_def)
@@ -1579,7 +1579,7 @@
 proof -
   interpret comp_fun_commute "add_mset \<circ> f"
     by (fact comp_fun_commute_mset_image)
-  show ?thesis by (induct N) (simp_all add: image_mset_def ac_simps)
+  show ?thesis by (induct N) (simp_all add: image_mset_def)
 qed
 
 corollary image_mset_add_mset [simp]:
@@ -1598,7 +1598,7 @@
 lemma image_mset_If:
   "image_mset (\<lambda>x. if P x then f x else g x) A =
      image_mset f (filter_mset P A) + image_mset g (filter_mset (\<lambda>x. \<not>P x) A)"
-  by (induction A) (auto simp: add_ac)
+  by (induction A) auto
 
 lemma image_mset_Diff:
   assumes "B \<subseteq># A"
@@ -1709,7 +1709,7 @@
   by (induct xs) simp_all
 
 lemma mset_append [simp]: "mset (xs @ ys) = mset xs + mset ys"
-  by (induct xs arbitrary: ys) (auto simp: ac_simps)
+  by (induct xs arbitrary: ys) auto
 
 lemma mset_filter: "mset (filter P xs) = {#x \<in># mset xs. P x #}"
   by (induct xs) simp_all
@@ -1769,7 +1769,7 @@
 done
 
 lemma mset_compl_union [simp]: "mset [x\<leftarrow>xs. P x] + mset [x\<leftarrow>xs. \<not>P x] = mset xs"
-  by (induct xs) (auto simp: ac_simps)
+  by (induct xs) auto
 
 lemma nth_mem_mset: "i < length ls \<Longrightarrow> (ls ! i) \<in># mset ls"
 proof (induct ls arbitrary: i)
@@ -1824,7 +1824,7 @@
 
 global_interpretation mset_set: folding add_mset "{#}"
   defines mset_set = "folding.F add_mset {#}"
-  by standard (simp add: fun_eq_iff ac_simps)
+  by standard (simp add: fun_eq_iff)
 
 lemma count_mset_set [simp]:
   "finite A \<Longrightarrow> x \<in> A \<Longrightarrow> count (mset_set A) x = 1" (is "PROP ?P")
@@ -1846,7 +1846,7 @@
 
 lemma mset_set_Union:
   "finite A \<Longrightarrow> finite B \<Longrightarrow> A \<inter> B = {} \<Longrightarrow> mset_set (A \<union> B) = mset_set A + mset_set B"
-  by (induction A rule: finite_induct) (auto simp: add_ac)
+  by (induction A rule: finite_induct) auto
 
 lemma filter_mset_mset_set [simp]:
   "finite A \<Longrightarrow> filter_mset P (mset_set A) = mset_set {x\<in>A. P x}"
@@ -1854,7 +1854,7 @@
   case (insert x A)
   from insert.hyps have "filter_mset P (mset_set (insert x A)) =
       filter_mset P (mset_set A) + mset_set (if P x then {x} else {})"
-    by (simp add: add_ac)
+    by simp
   also have "filter_mset P (mset_set A) = mset_set {x\<in>A. P x}"
     by (rule insert.IH)
   also from insert.hyps
@@ -1876,7 +1876,7 @@
 qed
 
 lemma mset_set_set: "distinct xs \<Longrightarrow> mset_set (set xs) = mset xs"
-  by (induction xs) (simp_all add: add_ac)
+  by (induction xs) simp_all
 
 context linorder
 begin
@@ -1930,10 +1930,10 @@
 
 lemma sorted_list_of_mset_set [simp]:
   "sorted_list_of_multiset (mset_set A) = sorted_list_of_set A"
-by (cases "finite A") (induct A rule: finite_induct, simp_all add: ac_simps)
+by (cases "finite A") (induct A rule: finite_induct, simp_all)
 
 lemma mset_upt [simp]: "mset [m..<n] = mset_set {m..<n}"
-  by (induction n) (simp_all add: atLeastLessThanSuc add_ac)
+  by (induction n) (simp_all add: atLeastLessThanSuc)
 
 lemma image_mset_map_of:
   "distinct (map fst xs) \<Longrightarrow> {#the (map_of xs i). i \<in># mset (map fst xs)#} = mset (map snd xs)"
@@ -2117,7 +2117,7 @@
 
 lemma msetprod_replicate_mset [simp]:
   "msetprod (replicate_mset n a) = a ^ n"
-  by (induct n) (simp_all add: ac_simps)
+  by (induct n) simp_all
 
 lemma setprod_unfold_msetprod:
   "setprod f A = msetprod (image_mset f (mset_set A))"
@@ -2128,10 +2128,10 @@
   by (simp add: fold_mset_def setprod.eq_fold msetprod.eq_fold funpow_times_power comp_def)
 
 lemma msetprod_delta: "msetprod (image_mset (\<lambda>x. if x = y then c else 1) A) = c ^ count A y"
-  by (induction A) (simp_all add: mult_ac)
+  by (induction A) simp_all
 
 lemma msetprod_delta': "msetprod (image_mset (\<lambda>x. if y = x then c else 1) A) = c ^ count A y"
-  by (induction A) (simp_all add: mult_ac)
+  by (induction A) simp_all
 
 end
 
@@ -2188,7 +2188,7 @@
 
 lemma mset_sort [simp]:
   "mset (sort_key k xs) = mset xs"
-  by (induct xs) (simp_all add: ac_simps)
+  by (induct xs) simp_all
 
 text \<open>
   This lemma shows which properties suffice to show that a function
@@ -2443,7 +2443,7 @@
       then show ?thesis ..
     next
       case 2
-      from N 2(2) have n: "N = add_mset a (K' + K)" by (simp add: ac_simps)
+      from N 2(2) have n: "N = add_mset a (K' + K)" by simp
       with r 2(1) have "?R (K' + K) M0" by blast
       with n have ?case1 by (simp add: mult1_def)
       then show ?thesis ..
@@ -2592,7 +2592,7 @@
 apply (simp add: mult1_def)
 apply (rule_tac x = a in exI)
 apply (rule_tac x = "I + J'" in exI)
-apply (simp add: ac_simps)
+apply simp
 done
 
 lemma one_step_implies_mult:
@@ -2681,7 +2681,7 @@
     } note [dest!] = this
     assume ?R thus ?L
       using mult_implies_one_step[OF assms(2), of "N - M #\<inter> N" "M - M #\<inter> N"]
-        mult_cancel_max[OF assms(2,1), of "N" "M"] * by (auto simp: multp_def ac_simps)
+        mult_cancel_max[OF assms(2,1), of "N" "M"] * by (auto simp: multp_def)
   qed
 qed
 
@@ -2844,14 +2844,14 @@
     case [simp]: 1
     have "{#x#} + X = A + ({#y#}+Z) \<and> {#y#} + Y = B + ({#y#}+Z) \<and>
       ((set_mset A, set_mset B) \<in> max_strict \<or> (B = {#} \<and> A = {#}))"
-      by (auto simp: ac_simps)
+      by auto
     thus ?thesis by blast
   next
     case 2
     let ?A' = "{#x#} + A" and ?B' = "{#y#} + B"
     have "{#x#} + X = ?A' + Z"
       "{#y#} + Y = ?B' + Z"
-      by (auto simp add: ac_simps)
+      by auto
     moreover have
       "(set_mset ?A', set_mset ?B') \<in> max_strict"
       using 1 2 unfolding max_strict_def
@@ -2889,7 +2889,7 @@
   }
   from mx_or_empty
   have "(Z'' + A', Z'' + B') \<in> ms_weak" by (rule wmsI)
-  thus "(Z + {#}, Z' + {#}) \<in> ms_weak" by (simp add:ac_simps)
+  thus "(Z + {#}, Z' + {#}) \<in> ms_weak" by (simp add: ac_simps)
 qed
 
 lemma empty_neutral: "{#} + x = x" "x + {#} = x"
@@ -3088,7 +3088,7 @@
   apply (cases "finite A")
   apply simp_all
   apply (induct A rule: finite_induct)
-  apply (simp_all add: add.commute)
+  apply simp_all
   done
 
 declare size_mset [code]
@@ -3128,7 +3128,7 @@
     note Some = Some[unfolded res]
     from extract_SomeE[OF Some] have "ys = ys1 @ x # ys2" by simp
     hence id: "mset ys = add_mset x (mset (ys1 @ ys2))"
-      by (auto simp: ac_simps)
+      by auto
     show ?thesis unfolding subset_eq_mset_impl.simps
       unfolding Some option.simps split
       unfolding id
@@ -3158,7 +3158,7 @@
 end
 
 lemma [code]: "msetsum (mset xs) = listsum xs"
-  by (induct xs) (simp_all add: add.commute)
+  by (induct xs) simp_all
 
 lemma [code]: "msetprod (mset xs) = fold times xs 1"
 proof -
@@ -3240,7 +3240,7 @@
       add_mset (x,y) (mset (zip xs ys))"
       by (rule Cons.hyps(2))
     thus ?thesis
-      unfolding k by (auto simp: add.commute union_lcomm)
+      unfolding k by auto
   qed
 qed
 
@@ -3282,7 +3282,7 @@
   moreover have "mset (zip xs' ys') = mset (zip (x # xs) (y # ys))"
     unfolding xs' ys'_def
     by (rule trans[OF mset_zip_take_Cons_drop_twice])
-      (auto simp: len_a ms_a j_len' add.commute)
+      (auto simp: len_a ms_a j_len')
   ultimately show ?case
     by blast
 qed