src/HOL/Library/Multiset.thy
changeset 40606 af1a0b0c6202
parent 40347 429bf4388b2f
child 40950 a370b0fb6f09
     1.1 --- a/src/HOL/Library/Multiset.thy	Thu Nov 18 17:01:16 2010 +0100
     1.2 +++ b/src/HOL/Library/Multiset.thy	Thu Nov 18 17:01:16 2010 +0100
     1.3 @@ -1627,6 +1627,14 @@
     1.4    @{term "{#x+x|x:#M. x<c#}"}.
     1.5  *}
     1.6  
     1.7 +type_mapper image_mset proof -
     1.8 +  fix f g A show "image_mset f (image_mset g A) = image_mset (\<lambda>x. f (g x)) A"
     1.9 +    by (induct A) simp_all
    1.10 +next
    1.11 +  fix A show "image_mset (\<lambda>x. x) A = A"
    1.12 +    by (induct A) simp_all
    1.13 +qed
    1.14 +
    1.15  
    1.16  subsection {* Termination proofs with multiset orders *}
    1.17