# HG changeset patch
# User nipkow
# Date 1678798807 -3600
# Node ID 48b4e0cd94cd90050dac8b84b647e5e8ae500d87
# Parent  4b688b8f1de33076a6c652cf5bb53881594ff66d
bring priority in line with ordinary function update notation

diff -r 4b688b8f1de3 -r 48b4e0cd94cd src/HOL/Map.thy
--- a/src/HOL/Map.thy	Tue Mar 14 10:35:10 2023 +0100
+++ b/src/HOL/Map.thy	Tue Mar 14 14:00:07 2023 +0100
@@ -56,7 +56,7 @@
   "_maplets" :: "['a, 'a] \<Rightarrow> maplet"             ("_ /[\<mapsto>]/ _")
   ""         :: "maplet \<Rightarrow> maplets"             ("_")
   "_Maplets" :: "[maplet, maplets] \<Rightarrow> maplets" ("_,/ _")
-  "_MapUpd"  :: "['a \<rightharpoonup> 'b, maplets] \<Rightarrow> 'a \<rightharpoonup> 'b" ("_/'(_')" [900, 0] 900)
+  "_MapUpd"  :: "['a \<rightharpoonup> 'b, maplets] \<Rightarrow> 'a \<rightharpoonup> 'b" ("_/'(_')" [1000, 0] 900)
   "_Map"     :: "maplets \<Rightarrow> 'a \<rightharpoonup> 'b"            ("(1[_])")
 
 syntax (ASCII)
@@ -177,7 +177,7 @@
   assumes "length ys = length xs"
     and "length zs = length xs"
     and "x \<notin> set xs"
-    and "map_of (zip xs ys)(x \<mapsto> y) = map_of (zip xs zs)(x \<mapsto> z)"
+    and "(map_of (zip xs ys))(x \<mapsto> y) = (map_of (zip xs zs))(x \<mapsto> z)"
   shows "map_of (zip xs ys) = map_of (zip xs zs)"
 proof
   fix x' :: 'a
@@ -191,7 +191,7 @@
     ultimately show ?thesis by simp
   next
     case False from assms
-      have "(map_of (zip xs ys)(x \<mapsto> y)) x' = (map_of (zip xs zs)(x \<mapsto> z)) x'" by auto
+      have "((map_of (zip xs ys))(x \<mapsto> y)) x' = ((map_of (zip xs zs))(x \<mapsto> z)) x'" by auto
     with False show ?thesis by simp
   qed
 qed
@@ -209,7 +209,7 @@
 next
   case (Cons y ys x xs z zs)
   from \<open>map_of (zip (x#xs) (y#ys)) = map_of (zip (x#xs) (z#zs))\<close>
-    have map_of: "map_of (zip xs ys)(x \<mapsto> y) = map_of (zip xs zs)(x \<mapsto> z)" by simp
+    have map_of: "(map_of (zip xs ys))(x \<mapsto> y) = (map_of (zip xs zs))(x \<mapsto> z)" by simp
   from Cons have "length ys = length xs" and "length zs = length xs"
     and "x \<notin> set xs" by simp_all
   then have "map_of (zip xs ys) = map_of (zip xs zs)" using map_of by (rule map_of_zip_upd)
@@ -435,7 +435,7 @@
   by (simp add:map_upds_def)
 
 lemma map_upds_append1 [simp]:
-  "size xs < size ys \<Longrightarrow> m(xs@[x] [\<mapsto>] ys) = m(xs [\<mapsto>] ys)(x \<mapsto> ys!size xs)"
+  "size xs < size ys \<Longrightarrow> m(xs@[x] [\<mapsto>] ys) = m(xs [\<mapsto>] ys, x \<mapsto> ys!size xs)"
 proof (induct xs arbitrary: ys m)
   case Nil
   then show ?case
@@ -478,7 +478,7 @@
 
 
 lemma map_upds_twist [simp]:
-  "a \<notin> set as \<Longrightarrow> m(a\<mapsto>b)(as[\<mapsto>]bs) = m(as[\<mapsto>]bs)(a\<mapsto>b)"
+  "a \<notin> set as \<Longrightarrow> m(a\<mapsto>b, as[\<mapsto>]bs) = m(as[\<mapsto>]bs, a\<mapsto>b)"
 using set_take_subset by (fastforce simp add: map_upd_upds_conv_if)
 
 lemma map_upds_apply_nontin [simp]:
@@ -876,7 +876,7 @@
   with Cons.prems have "k \<notin> dom (map_of xs)"
     by (simp add: dom_map_of_conv_image_fst)
   then have *: "insert (k, v) {(k, v). map_of xs k = Some v} =
-    {(k', v'). (map_of xs(k \<mapsto> v)) k' = Some v'}"
+    {(k', v'). ((map_of xs)(k \<mapsto> v)) k' = Some v'}"
     by (auto split: if_splits)
   from Cons have "set xs = {(k, v). map_of xs k = Some v}" by simp
   with * \<open>x = (k, v)\<close> show ?case by simp