47 |
47 |
48 definition |
48 definition |
49 map_le :: "('a \<rightharpoonup> 'b) \<Rightarrow> ('a \<rightharpoonup> 'b) \<Rightarrow> bool" (infix "\<subseteq>\<^sub>m" 50) where |
49 map_le :: "('a \<rightharpoonup> 'b) \<Rightarrow> ('a \<rightharpoonup> 'b) \<Rightarrow> bool" (infix "\<subseteq>\<^sub>m" 50) where |
50 "(m\<^sub>1 \<subseteq>\<^sub>m m\<^sub>2) \<longleftrightarrow> (\<forall>a \<in> dom m\<^sub>1. m\<^sub>1 a = m\<^sub>2 a)" |
50 "(m\<^sub>1 \<subseteq>\<^sub>m m\<^sub>2) \<longleftrightarrow> (\<forall>a \<in> dom m\<^sub>1. m\<^sub>1 a = m\<^sub>2 a)" |
51 |
51 |
52 nonterminal maplets and maplet |
52 text \<open>Function update syntax \<open>f(x := y, \<dots>)\<close> is extended with \<open>x \<mapsto> y\<close>, which is short for |
|
53 \<open>x := Some y\<close>. \<open>:=\<close> and \<open>\<mapsto>\<close> can be mixed freely. |
|
54 The syntax \<open>[x \<mapsto> y, \<dots>]\<close> is short for \<open>Map.empty(x \<mapsto> y, \<dots>)\<close> |
|
55 but must only contain \<open>\<mapsto>\<close>, not \<open>:=\<close>, because \<open>[x:=y]\<close> clashes with the list update syntax \<open>xs[i:=x]\<close>.\<close> |
|
56 |
|
57 nonterminal maplet and maplets |
53 |
58 |
54 syntax |
59 syntax |
55 "_maplet" :: "['a, 'a] \<Rightarrow> maplet" ("_ /\<mapsto>/ _") |
60 "_maplet" :: "['a, 'a] \<Rightarrow> maplet" ("_ /\<mapsto>/ _") |
56 "_maplets" :: "['a, 'a] \<Rightarrow> maplet" ("_ /[\<mapsto>]/ _") |
61 "" :: "maplet \<Rightarrow> updbind" ("_") |
57 "" :: "maplet \<Rightarrow> maplets" ("_") |
62 "" :: "maplet \<Rightarrow> maplets" ("_") |
58 "_Maplets" :: "[maplet, maplets] \<Rightarrow> maplets" ("_,/ _") |
63 "_Maplets" :: "[maplet, maplets] \<Rightarrow> maplets" ("_,/ _") |
59 "_MapUpd" :: "['a \<rightharpoonup> 'b, maplets] \<Rightarrow> 'a \<rightharpoonup> 'b" ("_/'(_')" [1000, 0] 900) |
64 "_Map" :: "maplets \<Rightarrow> 'a \<rightharpoonup> 'b" ("(1[_])") |
60 "_Map" :: "maplets \<Rightarrow> 'a \<rightharpoonup> 'b" ("(1[_])") |
65 (* Syntax forbids \<open>[\<dots>, x := y, \<dots>]\<close> by introducing \<open>maplets\<close> in addition to \<open>updbinds\<close> *) |
61 |
66 |
62 syntax (ASCII) |
67 syntax (ASCII) |
63 "_maplet" :: "['a, 'a] \<Rightarrow> maplet" ("_ /|->/ _") |
68 "_maplet" :: "['a, 'a] \<Rightarrow> maplet" ("_ /|->/ _") |
64 "_maplets" :: "['a, 'a] \<Rightarrow> maplet" ("_ /[|->]/ _") |
|
65 |
69 |
66 translations |
70 translations |
67 "_MapUpd m (_Maplets xy ms)" \<rightleftharpoons> "_MapUpd (_MapUpd m xy) ms" |
71 "_Update f (_maplet x y)" \<rightleftharpoons> "f(x := CONST Some y)" |
68 "_MapUpd m (_maplet x y)" \<rightleftharpoons> "m(x := CONST Some y)" |
72 "_Maplets m ms" \<rightharpoonup> "_updbinds m ms" |
69 "_Map ms" \<rightleftharpoons> "_MapUpd (CONST empty) ms" |
73 "_Map ms" \<rightharpoonup> "_Update (CONST empty) ms" |
70 "_Map ms" \<leftharpoondown> "_MapUpd (\<lambda>x. CONST None) ms" \<comment>\<open>both are needed\<close> |
74 |
71 "_Map (_Maplets ms1 ms2)" \<leftharpoondown> "_MapUpd (_Map ms1) ms2" |
75 (* Printing must create \<open>_Map\<close> only for \<open>_maplet\<close> *) |
72 "_Maplets ms1 (_Maplets ms2 ms3)" \<leftharpoondown> "_Maplets (_Maplets ms1 ms2) ms3" |
76 "_Map (_maplet x y)" \<leftharpoondown> "_Update (\<lambda>u. CONST None) (_maplet x y)" |
73 |
77 "_Map (_updbinds m (_maplet x y))" \<leftharpoondown> "_Update (_Map m) (_maplet x y)" |
74 primrec map_of :: "('a \<times> 'b) list \<Rightarrow> 'a \<rightharpoonup> 'b" |
78 |
75 where |
79 text \<open>Updating with lists:\<close> |
|
80 |
|
81 primrec map_of :: "('a \<times> 'b) list \<Rightarrow> 'a \<rightharpoonup> 'b" where |
76 "map_of [] = empty" |
82 "map_of [] = empty" |
77 | "map_of (p # ps) = (map_of ps)(fst p \<mapsto> snd p)" |
83 | "map_of (p # ps) = (map_of ps)(fst p \<mapsto> snd p)" |
78 |
|
79 definition map_upds :: "('a \<rightharpoonup> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b list \<Rightarrow> 'a \<rightharpoonup> 'b" |
|
80 where "map_upds m xs ys = m ++ map_of (rev (zip xs ys))" |
|
81 translations |
|
82 "_MapUpd m (_maplets x y)" \<rightleftharpoons> "CONST map_upds m x y" |
|
83 |
84 |
84 lemma map_of_Cons_code [code]: |
85 lemma map_of_Cons_code [code]: |
85 "map_of [] k = None" |
86 "map_of [] k = None" |
86 "map_of ((l, v) # ps) k = (if l = k then Some v else map_of ps k)" |
87 "map_of ((l, v) # ps) k = (if l = k then Some v else map_of ps k)" |
87 by simp_all |
88 by simp_all |
|
89 |
|
90 definition map_upds :: "('a \<rightharpoonup> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b list \<Rightarrow> 'a \<rightharpoonup> 'b" where |
|
91 "map_upds m xs ys = m ++ map_of (rev (zip xs ys))" |
|
92 |
|
93 text \<open>There is also the more specialized update syntax \<open>xs [\<mapsto>] ys\<close> for lists \<open>xs\<close> and \<open>ys\<close>.\<close> |
|
94 |
|
95 syntax |
|
96 "_maplets" :: "['a, 'a] \<Rightarrow> maplet" ("_ /[\<mapsto>]/ _") |
|
97 |
|
98 syntax (ASCII) |
|
99 "_maplets" :: "['a, 'a] \<Rightarrow> maplet" ("_ /[|->]/ _") |
|
100 |
|
101 translations |
|
102 "_Update m (_maplets xs ys)" \<rightleftharpoons> "CONST map_upds m xs ys" |
|
103 |
|
104 "_Map (_maplets xs ys)" \<leftharpoondown> "_Update (\<lambda>u. CONST None) (_maplets xs ys)" |
|
105 "_Map (_updbinds m (_maplets xs ys))" \<leftharpoondown> "_Update (_Map m) (_maplets xs ys)" |
88 |
106 |
89 |
107 |
90 subsection \<open>@{term [source] empty}\<close> |
108 subsection \<open>@{term [source] empty}\<close> |
91 |
109 |
92 lemma empty_upd_none [simp]: "empty(x := None) = empty" |
110 lemma empty_upd_none [simp]: "empty(x := None) = empty" |