src/HOL/Library/Multiset.thy
changeset 39301 e1bd8a54c40f
parent 39198 f967a16dfcdd
child 39302 d7728f65b353
     1.1 --- a/src/HOL/Library/Multiset.thy	Mon Sep 13 06:02:47 2010 +0200
     1.2 +++ b/src/HOL/Library/Multiset.thy	Mon Sep 13 08:43:48 2010 +0200
     1.3 @@ -324,6 +324,9 @@
     1.4    "B \<le> A \<Longrightarrow> (A::'a multiset) - B + C = A + C - B"
     1.5  by (simp add: multiset_ext_iff mset_le_def)
     1.6  
     1.7 +lemma diff_le_self[simp]: "(M::'a multiset) - N \<le> M"
     1.8 +by(simp add: mset_le_def)
     1.9 +
    1.10  lemma mset_lessD: "A < B \<Longrightarrow> x \<in># A \<Longrightarrow> x \<in># B"
    1.11  apply (clarsimp simp: mset_le_def mset_less_def)
    1.12  apply (erule_tac x=x in allE)
    1.13 @@ -1597,7 +1600,7 @@
    1.14    thus "(Z + {#}, Z' + {#}) \<in> ms_weak" by (simp add:add_ac)
    1.15  qed
    1.16  
    1.17 -lemma empty_idemp: "{#} + x = x" "x + {#} = x"
    1.18 +lemma empty_neutral: "{#} + x = x" "x + {#} = x"
    1.19  and nonempty_plus: "{# x #} + rs \<noteq> {#}"
    1.20  and nonempty_single: "{# x #} \<noteq> {#}"
    1.21  by auto
    1.22 @@ -1623,7 +1626,7 @@
    1.23  
    1.24    val regroup_munion_conv =
    1.25        Function_Lib.regroup_conv @{const_abbrev Mempty} @{const_name plus}
    1.26 -        (map (fn t => t RS eq_reflection) (@{thms add_ac} @ @{thms empty_idemp}))
    1.27 +        (map (fn t => t RS eq_reflection) (@{thms add_ac} @ @{thms empty_neutral}))
    1.28  
    1.29    fun unfold_pwleq_tac i =
    1.30      (rtac @{thm pw_leq_step} i THEN (fn st => unfold_pwleq_tac (i + 1) st))