src/HOL/Library/Multiset.thy
changeset 57514 bdc2c6b40bf2
parent 57512 cc97b347b301
child 57518 2f640245fc6d
     1.1 --- a/src/HOL/Library/Multiset.thy	Sat Jul 05 10:09:01 2014 +0200
     1.2 +++ b/src/HOL/Library/Multiset.thy	Sat Jul 05 11:01:53 2014 +0200
     1.3 @@ -717,7 +717,7 @@
     1.4      by (blast dest: multi_member_split)
     1.5    have "A + {#b#} = A + {#b#} + {#c#} - {#c#}" by simp
     1.6    then have "A + {#b#} = A + {#c#} + {#b#} - {#c#}" 
     1.7 -    by (simp add: add_ac)
     1.8 +    by (simp add: ac_simps)
     1.9    then show ?thesis using B by simp
    1.10  qed
    1.11  
    1.12 @@ -817,7 +817,7 @@
    1.13  next
    1.14    case (add M x)
    1.15    have "M + {#x#} + N = (M + N) + {#x#}"
    1.16 -    by (simp add: add_ac)
    1.17 +    by (simp add: ac_simps)
    1.18    with add show ?case by (simp add: fold_mset_insert fold_mset_fun_left_comm)
    1.19  qed
    1.20  
    1.21 @@ -851,7 +851,7 @@
    1.22  lemma comp_fun_commute_mset_image:
    1.23    "comp_fun_commute (plus o single o f)"
    1.24  proof
    1.25 -qed (simp add: add_ac fun_eq_iff)
    1.26 +qed (simp add: ac_simps fun_eq_iff)
    1.27  
    1.28  lemma image_mset_empty [simp]: "image_mset f {#} = {#}"
    1.29    by (simp add: image_mset_def)
    1.30 @@ -868,7 +868,7 @@
    1.31  proof -
    1.32    interpret comp_fun_commute "plus o single o f"
    1.33      by (fact comp_fun_commute_mset_image)
    1.34 -  show ?thesis by (induct N) (simp_all add: image_mset_def add_ac)
    1.35 +  show ?thesis by (induct N) (simp_all add: image_mset_def ac_simps)
    1.36  qed
    1.37  
    1.38  corollary image_mset_insert:
    1.39 @@ -956,7 +956,7 @@
    1.40  
    1.41  lemma multiset_of_append [simp]:
    1.42    "multiset_of (xs @ ys) = multiset_of xs + multiset_of ys"
    1.43 -  by (induct xs arbitrary: ys) (auto simp: add_ac)
    1.44 +  by (induct xs arbitrary: ys) (auto simp: ac_simps)
    1.45  
    1.46  lemma multiset_of_filter:
    1.47    "multiset_of (filter P xs) = {#x :# multiset_of xs. P x #}"
    1.48 @@ -1008,7 +1008,7 @@
    1.49  
    1.50  lemma multiset_of_compl_union [simp]:
    1.51    "multiset_of [x\<leftarrow>xs. P x] + multiset_of [x\<leftarrow>xs. \<not>P x] = multiset_of xs"
    1.52 -  by (induct xs) (auto simp: add_ac)
    1.53 +  by (induct xs) (auto simp: ac_simps)
    1.54  
    1.55  lemma count_multiset_of_length_filter:
    1.56    "count (multiset_of xs) x = length (filter (\<lambda>y. x = y) xs)"
    1.57 @@ -1552,7 +1552,7 @@
    1.58      next
    1.59        fix K'
    1.60        assume "M0' = K' + {#a#}"
    1.61 -      with N have n: "N = K' + K + {#a#}" by (simp add: add_ac)
    1.62 +      with N have n: "N = K' + K + {#a#}" by (simp add: ac_simps)
    1.63  
    1.64        assume "M0 = K' + {#a'#}"
    1.65        with r have "?R (K' + K) M0" by blast
    1.66 @@ -1701,7 +1701,7 @@
    1.67  apply (simp add: mult1_def set_of_def)
    1.68  apply (rule_tac x = a in exI)
    1.69  apply (rule_tac x = "I + J'" in exI)
    1.70 -apply (simp add: add_ac)
    1.71 +apply (simp add: ac_simps)
    1.72  done
    1.73  
    1.74  lemma one_step_implies_mult:
    1.75 @@ -1840,14 +1840,14 @@
    1.76        "{#x#} + X = A + ({#y#}+Z) 
    1.77        \<and> {#y#} + Y = B + ({#y#}+Z)
    1.78        \<and> ((set_of A, set_of B) \<in> max_strict \<or> (B = {#} \<and> A = {#}))"
    1.79 -      by (auto simp: add_ac)
    1.80 +      by (auto simp: ac_simps)
    1.81      thus ?case by (intro exI)
    1.82    next
    1.83      assume A: "(x, y) \<in> pair_less"
    1.84      let ?A' = "{#x#} + A" and ?B' = "{#y#} + B"
    1.85      have "{#x#} + X = ?A' + Z"
    1.86        "{#y#} + Y = ?B' + Z"
    1.87 -      by (auto simp add: add_ac)
    1.88 +      by (auto simp add: ac_simps)
    1.89      moreover have 
    1.90        "(set_of ?A', set_of ?B') \<in> max_strict"
    1.91        using 1 A unfolding max_strict_def 
    1.92 @@ -1880,12 +1880,12 @@
    1.93        assume [simp]: "A' = {#} \<and> B' = {#}"
    1.94        show ?thesis by (rule smsI) (auto intro: max)
    1.95      qed
    1.96 -    thus "(Z + A, Z' + B) \<in> ms_strict" by (simp add:add_ac)
    1.97 +    thus "(Z + A, Z' + B) \<in> ms_strict" by (simp add:ac_simps)
    1.98      thus "(Z + A, Z' + B) \<in> ms_weak" by (simp add: ms_weak_def)
    1.99    }
   1.100    from mx_or_empty
   1.101    have "(Z'' + A', Z'' + B') \<in> ms_weak" by (rule wmsI)
   1.102 -  thus "(Z + {#}, Z' + {#}) \<in> ms_weak" by (simp add:add_ac)
   1.103 +  thus "(Z + {#}, Z' + {#}) \<in> ms_weak" by (simp add:ac_simps)
   1.104  qed
   1.105  
   1.106  lemma empty_neutral: "{#} + x = x" "x + {#} = x"
   1.107 @@ -1914,7 +1914,7 @@
   1.108  
   1.109    val regroup_munion_conv =
   1.110        Function_Lib.regroup_conv @{const_abbrev Mempty} @{const_name plus}
   1.111 -        (map (fn t => t RS eq_reflection) (@{thms add_ac} @ @{thms empty_neutral}))
   1.112 +        (map (fn t => t RS eq_reflection) (@{thms ac_simps} @ @{thms empty_neutral}))
   1.113  
   1.114    fun unfold_pwleq_tac i =
   1.115      (rtac @{thm pw_leq_step} i THEN (fn st => unfold_pwleq_tac (i + 1) st))