--- a/src/HOL/Map.thy Sun Aug 25 12:43:43 2024 +0200
+++ b/src/HOL/Map.thy Sun Aug 25 15:02:19 2024 +0200
@@ -67,6 +67,9 @@
syntax (ASCII)
"_maplet" :: "['a, 'a] \<Rightarrow> maplet" ("_ /|->/ _")
+syntax_consts
+ "_maplet" "_Maplets" "_Map" \<rightleftharpoons> fun_upd
+
translations
"_Update f (_maplet x y)" \<rightleftharpoons> "f(x := CONST Some y)"
"_Maplets m ms" \<rightharpoonup> "_updbinds m ms"
@@ -76,6 +79,7 @@
"_Map (_maplet x y)" \<leftharpoondown> "_Update (\<lambda>u. CONST None) (_maplet x y)"
"_Map (_updbinds m (_maplet x y))" \<leftharpoondown> "_Update (_Map m) (_maplet x y)"
+
text \<open>Updating with lists:\<close>
primrec map_of :: "('a \<times> 'b) list \<Rightarrow> 'a \<rightharpoonup> 'b" where
@@ -98,6 +102,9 @@
syntax (ASCII)
"_maplets" :: "['a, 'a] \<Rightarrow> maplet" ("_ /[|->]/ _")
+syntax_consts
+ "_maplets" \<rightleftharpoons> map_upds
+
translations
"_Update m (_maplets xs ys)" \<rightleftharpoons> "CONST map_upds m xs ys"