src/HOL/Bali/Basis.thy
changeset 19323 ec5cd5b1804c
parent 18576 8d98b7711e47
child 21314 6d709b9bea1a
     1.1 --- a/src/HOL/Bali/Basis.thy	Thu Mar 23 18:14:06 2006 +0100
     1.2 +++ b/src/HOL/Bali/Basis.thy	Thu Mar 23 20:03:53 2006 +0100
     1.3 @@ -277,6 +277,23 @@
     1.4    "! x:A: P"    == "! x:o2s A. P"
     1.5    "? x:A: P"    == "? x:o2s A. P"
     1.6  
     1.7 +section "Special map update"
     1.8 +
     1.9 +text{* Deemed too special for theory Map. *}
    1.10 +
    1.11 +constdefs
    1.12 +  chg_map :: "('b => 'b) => 'a => ('a ~=> 'b) => ('a ~=> 'b)"
    1.13 + "chg_map f a m == case m a of None => m | Some b => m(a|->f b)"
    1.14 +
    1.15 +lemma chg_map_new[simp]: "m a = None   ==> chg_map f a m = m"
    1.16 +by (unfold chg_map_def, auto)
    1.17 +
    1.18 +lemma chg_map_upd[simp]: "m a = Some b ==> chg_map f a m = m(a|->f b)"
    1.19 +by (unfold chg_map_def, auto)
    1.20 +
    1.21 +lemma chg_map_other [simp]: "a \<noteq> b \<Longrightarrow> chg_map f a m b = m b"
    1.22 +by (auto simp: chg_map_def split add: option.split)
    1.23 +
    1.24  
    1.25  section "unique association lists"
    1.26