equal
deleted
inserted
replaced
81 |
81 |
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 declare map_of.simps [code del] |
|
87 |
|
88 lemma map_of_Cons_code [code]: |
|
89 "map_of [] k = None" |
|
90 "map_of ((l, v) # ps) k = (if l = k then Some v else map_of ps k)" |
|
91 by simp_all |
|
92 |
86 defs |
93 defs |
87 map_upds_def [code func]: "m(xs [|->] ys) == m ++ map_of (rev(zip xs ys))" |
94 map_upds_def [code func]: "m(xs [|->] ys) == m ++ map_of (rev(zip xs ys))" |
88 |
95 |
89 |
96 |
90 subsection {* @{term [source] empty} *} |
97 subsection {* @{term [source] empty} *} |