*** empty log message ***
authornipkow
Wed May 14 11:15:18 2003 +0200 (2003-05-14)
changeset 1402768d247b7b14b
parent 14026 c031a330a03f
child 14028 ff6eb32b30a1
*** empty log message ***
src/HOL/Map.thy
     1.1 --- a/src/HOL/Map.thy	Wed May 14 10:33:52 2003 +0200
     1.2 +++ b/src/HOL/Map.thy	Wed May 14 11:15:18 2003 +0200
     1.3 @@ -201,11 +201,6 @@
     1.4  apply(simp add: map_add_def split:option.split)
     1.5  done
     1.6  
     1.7 -lemma map_add_comm: "dom m1 \<inter> dom m2 = {} \<Longrightarrow> m1++m2 = m2++m1"
     1.8 -apply(rule ext)
     1.9 -apply(fastsimp simp:map_add_def split:option.split)
    1.10 -done
    1.11 -
    1.12  lemma map_add_Some_iff: 
    1.13   "((m ++ n) k = Some x) = (n k = Some x | n k = None & m k = Some x)"
    1.14  apply (unfold map_add_def)
    1.15 @@ -340,6 +335,11 @@
    1.16   "dom(f(g|A)) = (dom f  - {a. a : A - dom g}) Un {a. a : A Int dom g}"
    1.17  by(auto simp add: dom_def overwrite_def)
    1.18  
    1.19 +lemma map_add_comm: "dom m1 \<inter> dom m2 = {} \<Longrightarrow> m1++m2 = m2++m1"
    1.20 +apply(rule ext)
    1.21 +apply(fastsimp simp:map_add_def split:option.split)
    1.22 +done
    1.23 +
    1.24  subsection {* ran *}
    1.25  
    1.26  lemma ran_empty[simp]: "ran empty = {}"