added theorem chg_map_other
authoroheimb
Mon Apr 12 19:54:09 2004 +0200 (2004-04-12)
changeset 14537e95ba267e3d5
parent 14536 43e436a4f293
child 14538 1d9d75a8efae
added theorem chg_map_other
src/HOL/Map.thy
     1.1 --- a/src/HOL/Map.thy	Mon Apr 12 12:52:08 2004 +0200
     1.2 +++ b/src/HOL/Map.thy	Mon Apr 12 19:54:09 2004 +0200
     1.3 @@ -161,6 +161,9 @@
     1.4  lemma chg_map_upd[simp]: "m a = Some b ==> chg_map f a m = m(a|->f b)"
     1.5  by (unfold chg_map_def, auto)
     1.6  
     1.7 +lemma chg_map_other [simp]: "a \<noteq> b \<Longrightarrow> chg_map f a m b = m b"
     1.8 +by (auto simp: chg_map_def split add: option.split)
     1.9 +
    1.10  
    1.11  subsection {* @{term map_of} *}
    1.12