added and renamed lemmas
authornipkow
Mon Sep 13 08:43:48 2010 +0200 (2010-09-13)
changeset 39301e1bd8a54c40f
parent 39298 5aefb5bc8a93
child 39302 d7728f65b353
added and renamed lemmas
NEWS
src/HOL/Library/Multiset.thy
     1.1 --- a/NEWS	Mon Sep 13 06:02:47 2010 +0200
     1.2 +++ b/NEWS	Mon Sep 13 08:43:48 2010 +0200
     1.3 @@ -182,6 +182,8 @@
     1.4  * List.thy: use various operations from the Haskell prelude when
     1.5  generating Haskell code.
     1.6  
     1.7 +* Multiset.thy: renamed empty_idemp -> empty_neutral
     1.8 +
     1.9  * code_simp.ML and method code_simp: simplification with rules determined
    1.10  by code generator.
    1.11  
     2.1 --- a/src/HOL/Library/Multiset.thy	Mon Sep 13 06:02:47 2010 +0200
     2.2 +++ b/src/HOL/Library/Multiset.thy	Mon Sep 13 08:43:48 2010 +0200
     2.3 @@ -324,6 +324,9 @@
     2.4    "B \<le> A \<Longrightarrow> (A::'a multiset) - B + C = A + C - B"
     2.5  by (simp add: multiset_ext_iff mset_le_def)
     2.6  
     2.7 +lemma diff_le_self[simp]: "(M::'a multiset) - N \<le> M"
     2.8 +by(simp add: mset_le_def)
     2.9 +
    2.10  lemma mset_lessD: "A < B \<Longrightarrow> x \<in># A \<Longrightarrow> x \<in># B"
    2.11  apply (clarsimp simp: mset_le_def mset_less_def)
    2.12  apply (erule_tac x=x in allE)
    2.13 @@ -1597,7 +1600,7 @@
    2.14    thus "(Z + {#}, Z' + {#}) \<in> ms_weak" by (simp add:add_ac)
    2.15  qed
    2.16  
    2.17 -lemma empty_idemp: "{#} + x = x" "x + {#} = x"
    2.18 +lemma empty_neutral: "{#} + x = x" "x + {#} = x"
    2.19  and nonempty_plus: "{# x #} + rs \<noteq> {#}"
    2.20  and nonempty_single: "{# x #} \<noteq> {#}"
    2.21  by auto
    2.22 @@ -1623,7 +1626,7 @@
    2.23  
    2.24    val regroup_munion_conv =
    2.25        Function_Lib.regroup_conv @{const_abbrev Mempty} @{const_name plus}
    2.26 -        (map (fn t => t RS eq_reflection) (@{thms add_ac} @ @{thms empty_idemp}))
    2.27 +        (map (fn t => t RS eq_reflection) (@{thms add_ac} @ @{thms empty_neutral}))
    2.28  
    2.29    fun unfold_pwleq_tac i =
    2.30      (rtac @{thm pw_leq_step} i THEN (fn st => unfold_pwleq_tac (i + 1) st))