equal
deleted
inserted
replaced
82 primrec |
82 primrec |
83 "map_of [] = empty" |
83 "map_of [] = empty" |
84 "map_of (p#ps) = (map_of ps)(fst p |-> snd p)" |
84 "map_of (p#ps) = (map_of ps)(fst p |-> snd p)" |
85 |
85 |
86 defs |
86 defs |
87 map_upds_def: "m(xs [|->] ys) == m ++ map_of (rev(zip xs ys))" |
87 map_upds_def [code func]: "m(xs [|->] ys) == m ++ map_of (rev(zip xs ys))" |
88 |
88 |
89 |
89 |
90 subsection {* @{term [source] empty} *} |
90 subsection {* @{term [source] empty} *} |
91 |
91 |
92 lemma empty_upd_none [simp]: "empty(x := None) = empty" |
92 lemma empty_upd_none [simp]: "empty(x := None) = empty" |