# HG changeset patch
# User nipkow
# Date 1678814350 -3600
# Node ID 7edbb16bc60fd39833f7cce9ee671348e65fbde3
# Parent  48b4e0cd94cd90050dac8b84b647e5e8ae500d87
Adjusted to new map update priorities

diff -r 48b4e0cd94cd -r 7edbb16bc60f src/HOL/Bali/AxSound.thy
--- a/src/HOL/Bali/AxSound.thy	Tue Mar 14 14:00:07 2023 +0100
+++ b/src/HOL/Bali/AxSound.thy	Tue Mar 14 18:19:10 2023 +0100
@@ -1468,7 +1468,7 @@
                        EName e
                        \<Rightarrow> (case e of 
                              VNam v 
-                             \<Rightarrow>(table_of (lcls (mbody (mthd dynM)))
+                             \<Rightarrow>((table_of (lcls (mbody (mthd dynM))))
                                 (pars (mthd dynM)[\<mapsto>]pTs')) v
                            | Res \<Rightarrow> Some (resTy dynM))
                      | This \<Rightarrow> if is_static statM 
diff -r 48b4e0cd94cd -r 7edbb16bc60f src/HOL/Bali/DefiniteAssignment.thy
--- a/src/HOL/Bali/DefiniteAssignment.thy	Tue Mar 14 14:00:07 2023 +0100
+++ b/src/HOL/Bali/DefiniteAssignment.thy	Tue Mar 14 18:19:10 2023 +0100
@@ -608,7 +608,7 @@
          \<Longrightarrow> Env\<turnstile> B \<guillemotright>\<langle>Throw e\<rangle>\<guillemotright> A"
 
 | Try:  "\<lbrakk>Env\<turnstile> B \<guillemotright>\<langle>c1\<rangle>\<guillemotright> C1; 
-          Env\<lparr>lcl := lcl Env(VName vn\<mapsto>Class C)\<rparr>\<turnstile> (B \<union> {VName vn}) \<guillemotright>\<langle>c2\<rangle>\<guillemotright> C2;  
+          Env\<lparr>lcl := (lcl Env)(VName vn\<mapsto>Class C)\<rparr>\<turnstile> (B \<union> {VName vn}) \<guillemotright>\<langle>c2\<rangle>\<guillemotright> C2;  
           nrm A = nrm C1 \<inter> nrm C2;
           brk A = brk C1 \<Rightarrow>\<inter> brk C2\<rbrakk> 
          \<Longrightarrow> Env\<turnstile> B \<guillemotright>\<langle>Try c1 Catch(C vn) c2\<rangle>\<guillemotright> A"
@@ -1170,7 +1170,7 @@
     from \<open>Env\<turnstile> B' \<guillemotright>\<langle>Try c1 Catch(C vn) c2\<rangle>\<guillemotright> A'\<close>
     obtain C1' C2'
       where da_c1': "Env\<turnstile> B' \<guillemotright>\<langle>c1\<rangle>\<guillemotright> C1'" and
-            da_c2': "Env\<lparr>lcl := lcl Env(VName vn\<mapsto>Class C)\<rparr>\<turnstile> B' \<union> {VName vn} 
+            da_c2': "Env\<lparr>lcl := (lcl Env)(VName vn\<mapsto>Class C)\<rparr>\<turnstile> B' \<union> {VName vn} 
                       \<guillemotright>\<langle>c2\<rangle>\<guillemotright> C2'" and
             A': "nrm A' = nrm C1' \<inter> nrm C2'"
                 "brk A' = brk C1' \<Rightarrow>\<inter>  brk C2'" 
@@ -1180,7 +1180,7 @@
     moreover note da_c1'
     ultimately obtain C1': "nrm C1 \<subseteq> nrm C1'" "(\<forall>l. brk C1 l \<subseteq> brk C1' l)"
       by blast
-    note \<open>PROP ?Hyp (Env\<lparr>lcl := lcl Env(VName vn\<mapsto>Class C)\<rparr>)
+    note \<open>PROP ?Hyp (Env\<lparr>lcl := (lcl Env)(VName vn\<mapsto>Class C)\<rparr>)
                     (B \<union> {VName vn}) \<langle>c2\<rangle> C2\<close>
     with B' da_c2'
     obtain "nrm C2 \<subseteq> nrm C2'" "(\<forall>l. brk C2 l \<subseteq> brk C2' l)"
@@ -1448,11 +1448,11 @@
     qed
     moreover
     obtain C2' where 
-      "Env\<lparr>lcl := lcl Env(VName vn\<mapsto>Class C)\<rparr>\<turnstile> B' \<union> {VName vn} \<guillemotright>\<langle>c2\<rangle>\<guillemotright> C2'"
+      "Env\<lparr>lcl := (lcl Env)(VName vn\<mapsto>Class C)\<rparr>\<turnstile> B' \<union> {VName vn} \<guillemotright>\<langle>c2\<rangle>\<guillemotright> C2'"
     proof -
       from B' have "B \<union> {VName vn} \<subseteq> B' \<union> {VName vn}" by blast
       moreover
-      have "PROP ?Hyp (Env\<lparr>lcl := lcl Env(VName vn\<mapsto>Class C)\<rparr>) 
+      have "PROP ?Hyp (Env\<lparr>lcl := (lcl Env)(VName vn\<mapsto>Class C)\<rparr>) 
                       (B \<union> {VName vn}) \<langle>c2\<rangle>" 
         by (rule Try.hyps)
       ultimately
diff -r 48b4e0cd94cd -r 7edbb16bc60f src/HOL/Bali/DefiniteAssignmentCorrect.thy
--- a/src/HOL/Bali/DefiniteAssignmentCorrect.thy	Tue Mar 14 14:00:07 2023 +0100
+++ b/src/HOL/Bali/DefiniteAssignmentCorrect.thy	Tue Mar 14 18:19:10 2023 +0100
@@ -494,7 +494,7 @@
     note G = \<open>prg Env = G\<close>
     from Try.prems obtain 
       wt_c1: "Env\<turnstile>c1\<Colon>\<surd>" and  
-      wt_c2: "Env\<lparr>lcl := lcl Env(VName vn\<mapsto>Class C)\<rparr>\<turnstile>c2\<Colon>\<surd>"
+      wt_c2: "Env\<lparr>lcl := (lcl Env)(VName vn\<mapsto>Class C)\<rparr>\<turnstile>c2\<Colon>\<surd>"
       by (elim wt_elim_cases)
     {
       fix j
@@ -531,7 +531,7 @@
           moreover have "jumpNestingOk jmps (In1r c2)" using jmpOk by simp
           moreover note wt_c2
           moreover from G 
-          have "prg (Env\<lparr>lcl := lcl Env(VName vn\<mapsto>Class C)\<rparr>) = G"
+          have "prg (Env\<lparr>lcl := (lcl Env)(VName vn\<mapsto>Class C)\<rparr>) = G"
             by simp
           moreover note jmp
           ultimately show ?thesis 
@@ -3170,13 +3170,13 @@
     from Try.prems obtain C1 C2 where
       da_c1: "Env\<turnstile> dom (locals (store ((Norm s0)::state))) \<guillemotright>\<langle>c1\<rangle>\<guillemotright> C1"  and
       da_c2:
-       "Env\<lparr>lcl := lcl Env(VName vn\<mapsto>Class C)\<rparr>
+       "Env\<lparr>lcl := (lcl Env)(VName vn\<mapsto>Class C)\<rparr>
         \<turnstile> (dom (locals (store ((Norm s0)::state))) \<union> {VName vn}) \<guillemotright>\<langle>c2\<rangle>\<guillemotright> C2" and
       A: "nrm A = nrm C1 \<inter> nrm C2" "brk A = brk C1 \<Rightarrow>\<inter> brk C2"
       by (elim da_elim_cases) simp
     from Try.prems obtain 
       wt_c1: "Env\<turnstile>c1\<Colon>\<surd>" and
-      wt_c2: "Env\<lparr>lcl := lcl Env(VName vn\<mapsto>Class C)\<rparr>\<turnstile>c2\<Colon>\<surd>"
+      wt_c2: "Env\<lparr>lcl := (lcl Env)(VName vn\<mapsto>Class C)\<rparr>\<turnstile>c2\<Colon>\<surd>"
       by (elim wt_elim_cases)
     have sxalloc: "prg Env\<turnstile>s1 \<midarrow>sxalloc\<rightarrow> s2" using Try.hyps G 
       by (simp (no_asm_simp))
@@ -3257,7 +3257,7 @@
           qed
           with da_c2 
           obtain C2' where
-            da_C2': "Env\<lparr>lcl := lcl Env(VName vn\<mapsto>Class C)\<rparr>
+            da_C2': "Env\<lparr>lcl := (lcl Env)(VName vn\<mapsto>Class C)\<rparr>
                      \<turnstile> dom (locals (store (new_xcpt_var vn s2))) \<guillemotright>\<langle>c2\<rangle>\<guillemotright> C2'"
            and nrm_C2': "nrm C2 \<subseteq> nrm C2'" 
            and brk_C2': "\<forall> l. brk C2 l \<subseteq> brk C2' l"
diff -r 48b4e0cd94cd -r 7edbb16bc60f src/HOL/Bali/Example.thy
--- a/src/HOL/Bali/Example.thy	Tue Mar 14 14:00:07 2023 +0100
+++ b/src/HOL/Bali/Example.thy	Tue Mar 14 18:19:10 2023 +0100
@@ -1208,12 +1208,11 @@
 
 abbreviation
   "obj_a == \<lparr>tag=Arr (PrimT Boolean) 2
-                ,values= Map.empty(Inr 0\<mapsto>Bool False)(Inr 1\<mapsto>Bool False)\<rparr>"
+                ,values= Map.empty(Inr 0\<mapsto>Bool False, Inr 1\<mapsto>Bool False)\<rparr>"
 
 abbreviation
   "obj_b == \<lparr>tag=CInst Ext
-                ,values=(Map.empty(Inl (vee, Base)\<mapsto>Null   )
-                              (Inl (vee, Ext )\<mapsto>Intg 0))\<rparr>"
+                ,values=(Map.empty(Inl (vee, Base)\<mapsto>Null, Inl (vee, Ext )\<mapsto>Intg 0))\<rparr>"
 
 abbreviation
   "obj_c == \<lparr>tag=CInst (SXcpt NullPointer),values=CONST Map.empty\<rparr>"
@@ -1222,15 +1221,15 @@
 abbreviation "arr_a == Map.empty(Inl (arr, Base)\<mapsto>Addr a)"
 
 abbreviation
-  "globs1 == Map.empty(Inr Ext   \<mapsto>\<lparr>tag=undefined, values=Map.empty\<rparr>)
-                     (Inr Base  \<mapsto>\<lparr>tag=undefined, values=arr_N\<rparr>)
-                     (Inr Object\<mapsto>\<lparr>tag=undefined, values=Map.empty\<rparr>)"
+  "globs1 == Map.empty(Inr Ext   \<mapsto>\<lparr>tag=undefined, values=Map.empty\<rparr>,
+                     Inr Base  \<mapsto>\<lparr>tag=undefined, values=arr_N\<rparr>,
+                     Inr Object\<mapsto>\<lparr>tag=undefined, values=Map.empty\<rparr>)"
 
 abbreviation
-  "globs2 == Map.empty(Inr Ext   \<mapsto>\<lparr>tag=undefined, values=Map.empty\<rparr>)
-                     (Inr Object\<mapsto>\<lparr>tag=undefined, values=Map.empty\<rparr>)
-                     (Inl a\<mapsto>obj_a)
-                     (Inr Base  \<mapsto>\<lparr>tag=undefined, values=arr_a\<rparr>)"
+  "globs2 == Map.empty(Inr Ext   \<mapsto>\<lparr>tag=undefined, values=Map.empty\<rparr>,
+                     Inr Object\<mapsto>\<lparr>tag=undefined, values=Map.empty\<rparr>,
+                     Inl a\<mapsto>obj_a,
+                     Inr Base  \<mapsto>\<lparr>tag=undefined, values=arr_a\<rparr>)"
 
 abbreviation "globs3 == globs2(Inl b\<mapsto>obj_b)"
 abbreviation "globs8 == globs3(Inl c\<mapsto>obj_c)"
diff -r 48b4e0cd94cd -r 7edbb16bc60f src/HOL/Bali/State.thy
--- a/src/HOL/Bali/State.thy	Tue Mar 14 14:00:07 2023 +0100
+++ b/src/HOL/Bali/State.thy	Tue Mar 14 18:19:10 2023 +0100
@@ -293,7 +293,7 @@
 
 lemma init_arr_comps_step [simp]: 
 "0 < j \<Longrightarrow> init_vals (arr_comps T  j    ) =  
-           init_vals (arr_comps T (j - 1))(j - 1\<mapsto>default_val T)"
+           (init_vals (arr_comps T (j - 1)))(j - 1\<mapsto>default_val T)"
 apply (unfold arr_comps_def in_bounds_def)
 apply (rule ext)
 apply auto
@@ -335,7 +335,7 @@
 apply (simp (no_asm))
 done
 
-lemma globs_gupd [simp]: "globs  (gupd(r\<mapsto>obj) s) = globs s(r\<mapsto>obj)"
+lemma globs_gupd [simp]: "globs  (gupd(r\<mapsto>obj) s) = (globs s)(r\<mapsto>obj)"
 apply (induct "s")
 by (simp add: gupd_def)
 
@@ -347,7 +347,7 @@
 apply (induct "s")
 by (simp add: gupd_def)
 
-lemma locals_lupd [simp]: "locals (lupd(vn\<mapsto>v ) s) = locals s(vn\<mapsto>v )"
+lemma locals_lupd [simp]: "locals (lupd(vn\<mapsto>v ) s) = (locals s)(vn\<mapsto>v )"
 apply (induct "s")
 by (simp add: lupd_def)
 
@@ -359,7 +359,7 @@
 done
 
 lemma globs_upd_gobj_upd [rule_format (no_asm), simp]: 
-"globs s r=Some obj\<longrightarrow> globs (upd_gobj r n v s) = globs s(r\<mapsto>upd_obj n v obj)"
+"globs s r=Some obj\<longrightarrow> globs (upd_gobj r n v s) = (globs s)(r\<mapsto>upd_obj n v obj)"
 apply (unfold upd_gobj_def)
 apply (induct "s")
 apply auto
@@ -390,7 +390,7 @@
 done
 
 lemma heap_heap_upd [simp]: 
-  "heap (st (g(Inl a\<mapsto>obj)) l) = heap (st g l)(a\<mapsto>obj)"
+  "heap (st (g(Inl a\<mapsto>obj)) l) = (heap (st g l))(a\<mapsto>obj)"
 apply (rule ext)
 apply (simp (no_asm))
 done
@@ -403,7 +403,7 @@
 apply (simp (no_asm))
 done
 
-lemma heap_gupd_Heap [simp]: "heap (gupd(Heap a\<mapsto>obj) s) = heap s(a\<mapsto>obj)"
+lemma heap_gupd_Heap [simp]: "heap (gupd(Heap a\<mapsto>obj) s) = (heap s)(a\<mapsto>obj)"
 apply (rule ext)
 apply (simp (no_asm))
 done
diff -r 48b4e0cd94cd -r 7edbb16bc60f src/HOL/Bali/TypeSafe.thy
--- a/src/HOL/Bali/TypeSafe.thy	Tue Mar 14 14:00:07 2023 +0100
+++ b/src/HOL/Bali/TypeSafe.thy	Tue Mar 14 18:19:10 2023 +0100
@@ -815,7 +815,7 @@
   wf_mhead G P sig mh;
   list_all2 (conf G s) pvs pTsa; G\<turnstile>pTsa[\<preceq>](parTs sig)\<rbrakk> \<Longrightarrow>  
   G,s\<turnstile>Map.empty (pars mh[\<mapsto>]pvs)
-      [\<sim>\<Colon>\<preceq>]table_of lvars(pars mh[\<mapsto>]parTs sig)"
+      [\<sim>\<Colon>\<preceq>](table_of lvars)(pars mh[\<mapsto>]parTs sig)"
 apply (unfold wf_mhead_def)
 apply clarify
 apply (erule (1) wlconf_empty_vals [THEN wlconf_ext_list])
@@ -895,7 +895,7 @@
                 (case k of
                    EName e \<Rightarrow> (case e of 
                                  VNam v 
-                                  \<Rightarrow> (table_of (lcls (mbody (mthd dm)))
+                                  \<Rightarrow> ((table_of (lcls (mbody (mthd dm))))
                                         (pars (mthd dm)[\<mapsto>]parTs sig)) v
                                | Res \<Rightarrow> Some (resTy (mthd dm)))
                  | This \<Rightarrow> if (is_static (mthd sm)) 
@@ -1180,7 +1180,7 @@
 
 lemma map_upds_upd_eq_length_simp:
   "\<And> tab qs x y. length ps = length qs 
-                  \<Longrightarrow> tab(ps[\<mapsto>]qs)(x\<mapsto>y) = tab(ps@[x][\<mapsto>]qs@[y])"
+                  \<Longrightarrow> tab(ps[\<mapsto>]qs, x\<mapsto>y) = tab(ps@[x][\<mapsto>]qs@[y])"
 proof (induct "ps")
   case Nil thus ?case by simp
 next
@@ -1189,7 +1189,7 @@
   obtain q qs' where qs: "qs=q#qs'" and eq_length: "length ps=length qs'"
     by (cases qs) auto
   from eq_length 
-  have "(tab(p\<mapsto>q))(ps[\<mapsto>]qs')(x\<mapsto>y) = (tab(p\<mapsto>q))(ps@[x][\<mapsto>]qs'@[y])"
+  have "(tab(p\<mapsto>q))(ps[\<mapsto>]qs', x\<mapsto>y) = (tab(p\<mapsto>q))(ps@[x][\<mapsto>]qs'@[y])"
     by (rule Cons.hyps)
   with qs show ?case
     by simp
@@ -1219,7 +1219,7 @@
     show ?thesis by simp
   next
     case (Cons y ys')
-    have "(tab(x\<mapsto>y)(xs[\<mapsto>]ys')) z = (tab'(x\<mapsto>y)(xs[\<mapsto>]ys')) z"
+    have "(tab(x\<mapsto>y, xs[\<mapsto>]ys')) z = (tab'(x\<mapsto>y, xs[\<mapsto>]ys')) z"
       by (iprover intro: Hyps map_upd_cong_ext)
     with Cons show ?thesis
       by simp
@@ -1230,7 +1230,7 @@
   by simp
 
 lemma map_upds_eq_length_suffix: "\<And> tab qs. 
-        length ps = length qs \<Longrightarrow> tab(ps@xs[\<mapsto>]qs) = tab(ps[\<mapsto>]qs)(xs[\<mapsto>][])"
+        length ps = length qs \<Longrightarrow> tab(ps@xs[\<mapsto>]qs) = tab(ps[\<mapsto>]qs, xs[\<mapsto>][])"
 proof (induct ps)
   case Nil thus ?case by simp
 next
@@ -1238,7 +1238,7 @@
   then obtain q qs' where qs: "qs=q#qs'" and eq_length: "length ps=length qs'"
     by (cases qs) auto
   from eq_length
-  have "tab(p\<mapsto>q)(ps @ xs[\<mapsto>]qs') = tab(p\<mapsto>q)(ps[\<mapsto>]qs')(xs[\<mapsto>][])"
+  have "tab(p\<mapsto>q, ps @ xs[\<mapsto>]qs') = tab(p\<mapsto>q, ps[\<mapsto>]qs', xs[\<mapsto>][])"
     by (rule Cons.hyps)
   with qs show ?case 
     by simp
@@ -1247,7 +1247,7 @@
   
 lemma map_upds_upds_eq_length_prefix_simp:
   "\<And> tab qs. length ps = length qs
-              \<Longrightarrow> tab(ps[\<mapsto>]qs)(xs[\<mapsto>]ys) = tab(ps@xs[\<mapsto>]qs@ys)"
+              \<Longrightarrow> tab(ps[\<mapsto>]qs, xs[\<mapsto>]ys) = tab(ps@xs[\<mapsto>]qs@ys)"
 proof (induct ps)
   case Nil thus ?case by simp
 next
@@ -1255,7 +1255,7 @@
   then obtain q qs' where qs: "qs=q#qs'" and eq_length: "length ps=length qs'"
     by (cases qs) auto
   from eq_length 
-  have "tab(p\<mapsto>q)(ps[\<mapsto>]qs')(xs[\<mapsto>]ys) = tab(p\<mapsto>q)(ps @ xs[\<mapsto>](qs' @ ys))"
+  have "tab(p\<mapsto>q, ps[\<mapsto>]qs', xs[\<mapsto>]ys) = tab(p\<mapsto>q, ps @ xs[\<mapsto>](qs' @ ys))"
     by (rule Cons.hyps)
   with qs 
   show ?case by simp
@@ -1297,11 +1297,11 @@
 
 
 lemma map_upd_Some_swap:
- "(tab(r\<mapsto>w)(u\<mapsto>v)) vn = Some z \<Longrightarrow> \<exists> z. (tab(u\<mapsto>v)(r\<mapsto>w)) vn = Some z"
+ "(tab(r\<mapsto>w, u\<mapsto>v)) vn = Some z \<Longrightarrow> \<exists> z. (tab(u\<mapsto>v, r\<mapsto>w)) vn = Some z"
 by (simp add: fun_upd_def)
 
 lemma map_upd_None_swap:
- "(tab(r\<mapsto>w)(u\<mapsto>v)) vn = None \<Longrightarrow> (tab(u\<mapsto>v)(r\<mapsto>w)) vn = None"
+ "(tab(r\<mapsto>w, u\<mapsto>v)) vn = None \<Longrightarrow> (tab(u\<mapsto>v, r\<mapsto>w)) vn = None"
 by (simp add: fun_upd_def)
 
 
@@ -1331,7 +1331,7 @@
     show ?thesis
     proof (cases "(tab(x\<mapsto>y)) vn \<noteq> Some z")
       case True
-      with some ys have "(tab'(x\<mapsto>y)(xs[\<mapsto>]tl)) vn = Some z"
+      with some ys have "(tab'(x\<mapsto>y, xs[\<mapsto>]tl)) vn = Some z"
         by (fastforce intro: Cons.hyps)
       with ys show ?thesis 
         by simp
@@ -1345,7 +1345,7 @@
       ultimately
       have "(tab(x\<mapsto>y)) vn =(tab'(x\<mapsto>y)) vn"
         by simp
-      hence "(tab(x\<mapsto>y)(xs[\<mapsto>]tl)) vn = (tab'(x\<mapsto>y)(xs[\<mapsto>]tl)) vn"
+      hence "(tab(x\<mapsto>y, xs[\<mapsto>]tl)) vn = (tab'(x\<mapsto>y, xs[\<mapsto>]tl)) vn"
         by (rule map_upds_cong_ext)
       with some ys
       show ?thesis 
@@ -1355,18 +1355,18 @@
 qed
    
 lemma map_upds_Some_swap: 
- assumes r_u: "(tab(r\<mapsto>w)(u\<mapsto>v)(xs[\<mapsto>]ys)) vn = Some z"
-    shows "\<exists> z. (tab(u\<mapsto>v)(r\<mapsto>w)(xs[\<mapsto>]ys)) vn = Some z"
-proof (cases "(tab(r\<mapsto>w)(u\<mapsto>v)) vn = Some z")
+ assumes r_u: "(tab(r\<mapsto>w, u\<mapsto>v, xs[\<mapsto>]ys)) vn = Some z"
+    shows "\<exists> z. (tab(u\<mapsto>v, r\<mapsto>w, xs[\<mapsto>]ys)) vn = Some z"
+proof (cases "(tab(r\<mapsto>w, u\<mapsto>v)) vn = Some z")
   case True
-  then obtain z' where "(tab(u\<mapsto>v)(r\<mapsto>w)) vn = Some z'"
+  then obtain z' where "(tab(u\<mapsto>v, r\<mapsto>w)) vn = Some z'"
     by (rule map_upd_Some_swap [elim_format]) blast
-  thus "\<exists> z. (tab(u\<mapsto>v)(r\<mapsto>w)(xs[\<mapsto>]ys)) vn = Some z"
+  thus "\<exists> z. (tab(u\<mapsto>v, r\<mapsto>w, xs[\<mapsto>]ys)) vn = Some z"
     by (rule map_upds_Some_expand)
 next
   case False
   with r_u
-  have "(tab(u\<mapsto>v)(r\<mapsto>w)(xs[\<mapsto>]ys)) vn = Some z"
+  have "(tab(u\<mapsto>v, r\<mapsto>w, xs[\<mapsto>]ys)) vn = Some z"
     by (rule map_upds_in_expansion_map_swap)
   thus ?thesis
     by simp
@@ -1374,7 +1374,7 @@
  
 lemma map_upds_Some_insert:
   assumes z: "(tab(xs[\<mapsto>]ys)) vn = Some z"
-    shows "\<exists> z. (tab(u\<mapsto>v)(xs[\<mapsto>]ys)) vn = Some z"
+    shows "\<exists> z. (tab(u\<mapsto>v, xs[\<mapsto>]ys)) vn = Some z"
 proof (cases "\<exists> z. tab vn = Some z")
   case True
   then obtain z' where "tab vn = Some z'" by blast
@@ -1386,7 +1386,7 @@
   case False
   hence "tab vn \<noteq> Some z" by simp
   with z
-  have "(tab(u\<mapsto>v)(xs[\<mapsto>]ys)) vn = Some z"
+  have "(tab(u\<mapsto>v, xs[\<mapsto>]ys)) vn = Some z"
     by (rule map_upds_in_expansion_map_swap)
   thus ?thesis ..
 qed
@@ -1425,7 +1425,7 @@
     have "(tab(x\<mapsto>y)) vn = Some el"
       by - (rule Cons.hyps,auto)
     moreover from tab'_vn ys
-    have "(tab'(x\<mapsto>y)(xs[\<mapsto>]tl)) vn = None" 
+    have "(tab'(x\<mapsto>y, xs[\<mapsto>]tl)) vn = None" 
       by simp
     hence "(tab'(x\<mapsto>y)) vn = None"
       by (rule map_upds_None_cut)
@@ -1436,7 +1436,7 @@
 
    
 lemma dom_vname_split:
- "dom (case_lname (case_ename (tab(x\<mapsto>y)(xs[\<mapsto>]ys)) a) b)
+ "dom (case_lname (case_ename (tab(x\<mapsto>y, xs[\<mapsto>]ys)) a) b)
    = dom (case_lname (case_ename (tab(x\<mapsto>y)) a) b) \<union> 
      dom (case_lname (case_ename (tab(xs[\<mapsto>]ys)) a) b)"
   (is "?List x xs y ys = ?Hd x y \<union> ?Tl xs ys")
@@ -1503,7 +1503,7 @@
     case Nil with len show ?thesis by simp
   next
     case (Cons y tl)
-    with len have "dom (tab(x\<mapsto>y)(xs[\<mapsto>]tl)) = dom (tab(x\<mapsto>y)) \<union> set xs"
+    with len have "dom (tab(x\<mapsto>y, xs[\<mapsto>]tl)) = dom (tab(x\<mapsto>y)) \<union> set xs"
       by - (rule Hyp,simp)
     moreover 
     have "dom (tab(x\<mapsto>hd ys)) = dom tab \<union> {x}"
@@ -3162,7 +3162,7 @@
                     EName e
                     \<Rightarrow> (case e of 
                           VNam v 
-                          \<Rightarrow>(table_of (lcls (mbody (mthd dynM)))
+                          \<Rightarrow>((table_of (lcls (mbody (mthd dynM))))
                              (pars (mthd dynM)[\<mapsto>]pTs')) v
                         | Res \<Rightarrow> Some (resTy dynM))
                   | This \<Rightarrow> if is_static statM 
diff -r 48b4e0cd94cd -r 7edbb16bc60f src/HOL/Bali/WellForm.thy
--- a/src/HOL/Bali/WellForm.thy	Tue Mar 14 14:00:07 2023 +0100
+++ b/src/HOL/Bali/WellForm.thy	Tue Mar 14 18:19:10 2023 +0100
@@ -85,7 +85,7 @@
             EName e 
             \<Rightarrow> (case e of 
                   VNam v 
-                  \<Rightarrow>(table_of (lcls (mbody m))((pars m)[\<mapsto>](parTs sig))) v
+                  \<Rightarrow>((table_of (lcls (mbody m)))(pars m [\<mapsto>] parTs sig)) v
                 | Res \<Rightarrow> Some (resTy m))
           | This \<Rightarrow> if is_static m then None else Some (Class C)))"
 
@@ -110,7 +110,7 @@
 
 lemma callee_lcl_VNam_simp [simp]:
 "callee_lcl C sig m (EName (VNam v)) 
-  = (table_of (lcls (mbody m))((pars m)[\<mapsto>](parTs sig))) v"
+  = ((table_of (lcls (mbody m)))(pars m [\<mapsto>] parTs sig)) v"
 by (simp add: callee_lcl_def)
  
 lemma callee_lcl_Res_simp [simp]:
diff -r 48b4e0cd94cd -r 7edbb16bc60f src/HOL/Bali/WellType.thy
--- a/src/HOL/Bali/WellType.thy	Tue Mar 14 14:00:07 2023 +0100
+++ b/src/HOL/Bali/WellType.thy	Tue Mar 14 18:19:10 2023 +0100
@@ -295,7 +295,7 @@
                                          E,dt\<Turnstile>Throw e\<Colon>\<surd>"
   \<comment> \<open>cf. 14.18\<close>
 | Try:  "\<lbrakk>E,dt\<Turnstile>c1\<Colon>\<surd>; prg E\<turnstile>tn\<preceq>\<^sub>C SXcpt Throwable;
-          lcl E (VName vn)=None; E \<lparr>lcl := lcl E(VName vn\<mapsto>Class tn)\<rparr>,dt\<Turnstile>c2\<Colon>\<surd>\<rbrakk>
+          lcl E (VName vn)=None; E \<lparr>lcl := (lcl E)(VName vn\<mapsto>Class tn)\<rparr>,dt\<Turnstile>c2\<Colon>\<surd>\<rbrakk>
           \<Longrightarrow>
                                          E,dt\<Turnstile>Try c1 Catch(tn vn) c2\<Colon>\<surd>"
 
diff -r 48b4e0cd94cd -r 7edbb16bc60f src/HOL/MicroJava/Comp/AuxLemmas.thy
--- a/src/HOL/MicroJava/Comp/AuxLemmas.thy	Tue Mar 14 14:00:07 2023 +0100
+++ b/src/HOL/MicroJava/Comp/AuxLemmas.thy	Tue Mar 14 18:19:10 2023 +0100
@@ -102,7 +102,7 @@
    apply fastforce+
   done
 
-lemma map_of_upds_SomeD: "(map_of m (xs[\<mapsto>]ys)) k = Some y 
+lemma map_of_upds_SomeD: "((map_of m) (xs[\<mapsto>]ys)) k = Some y 
   \<Longrightarrow> k \<in> (set (xs @ map fst m))"
   by (auto dest: map_upds_SomeD map_of_SomeD fst_in_set_lemma)
 
diff -r 48b4e0cd94cd -r 7edbb16bc60f src/HOL/MicroJava/Comp/CorrComp.thy
--- a/src/HOL/MicroJava/Comp/CorrComp.thy	Tue Mar 14 14:00:07 2023 +0100
+++ b/src/HOL/MicroJava/Comp/CorrComp.thy	Tue Mar 14 18:19:10 2023 +0100
@@ -266,7 +266,7 @@
   "env_of_jmb G C S == 
   (let (mn,pTs) = S;
        (D,rT,(pns,lvars,blk,res)) = the(method (G, C) S) in
-  (G,map_of lvars(pns[\<mapsto>]pTs)(This\<mapsto>Class C)))"
+  (G,(map_of lvars)(pns[\<mapsto>]pTs, This\<mapsto>Class C)))"
 
 lemma env_of_jmb_fst [simp]: "fst (env_of_jmb G C S) = G"
 by (simp add: env_of_jmb_def split_beta)
@@ -406,7 +406,7 @@
   wf_prog wf_java_mdecl G; is_class G D \<rbrakk>
  \<Longrightarrow> wtpd_stmt (env_of_jmb G D (md, pTs)) blk"
   apply (simp add: wtpd_stmt_def env_of_jmb_def)
-  apply (frule_tac P="%D (md, pTs) (rT, (pns, lvars, blk, res)). (G, map_of lvars(pns[\<mapsto>]pTs)(This\<mapsto>Class D)) \<turnstile> blk \<surd> " in method_preserves)
+  apply (frule_tac P="%D (md, pTs) (rT, (pns, lvars, blk, res)). (G, (map_of lvars)(pns[\<mapsto>]pTs, This\<mapsto>Class D)) \<turnstile> blk \<surd> " in method_preserves)
      apply (auto simp: wf_mdecl_def wf_java_mdecl_def)
   done
 
@@ -415,7 +415,7 @@
   wf_prog wf_java_mdecl G; is_class G D \<rbrakk>
  \<Longrightarrow> wtpd_expr (env_of_jmb G D (md, pTs)) res"
   apply (simp add: wtpd_expr_def env_of_jmb_def)
-  apply (frule_tac P="%D (md, pTs) (rT, (pns, lvars, blk, res)). \<exists>T. (G, map_of lvars(pns[\<mapsto>]pTs)(This\<mapsto>Class D)) \<turnstile> res :: T " in method_preserves)
+  apply (frule_tac P="%D (md, pTs) (rT, (pns, lvars, blk, res)). \<exists>T. (G, (map_of lvars)(pns[\<mapsto>]pTs, This\<mapsto>Class D)) \<turnstile> res :: T " in method_preserves)
      apply (auto simp: wf_mdecl_def wf_java_mdecl_def)
   done
 
@@ -539,7 +539,7 @@
    {cG, D, S} \<turnstile>
    {h, os, (a' # pvs @ lvals)}
    >- (compInitLvars (pns, lvars, blk, res) lvars) \<rightarrow>
-   {h, os, (locvars_xstate G C S (Norm (h, init_vars lvars(pns[\<mapsto>]pvs)(This\<mapsto>a'))))})"
+   {h, os, (locvars_xstate G C S (Norm (h, (init_vars lvars)(pns[\<mapsto>]pvs, This\<mapsto>a'))))})"
   apply (simp only: compInitLvars_def)
   apply (frule method_yields_wf_java_mdecl, assumption, assumption)
 
@@ -587,7 +587,7 @@
   method (G, dynT) (mn, pTs) = Some (md, rT, pns, lvars, blk, res);
   list_all2 (conf G h) pvs pTs; G,h \<turnstile> a' ::\<preceq> Class md\<rbrakk>
   \<Longrightarrow>
-  (np a' x, h, init_vars lvars(pns[\<mapsto>]pvs)(This\<mapsto>a'))::\<preceq>(env_of_jmb G md (mn, pTs))"
+  (np a' x, h, (init_vars lvars)(pns[\<mapsto>]pvs, This\<mapsto>a'))::\<preceq>(env_of_jmb G md (mn, pTs))"
   apply (frule wf_prog_ws_prog)
   apply (frule method_in_md [THEN conjunct2], assumption+)
   apply (frule method_yields_wf_java_mdecl, assumption, assumption)
@@ -1173,7 +1173,7 @@
            apply (simp (no_asm_simp))
 
           (* show s3::\<preceq>\<dots> *)
-          apply (rule_tac xs = "(np a' x, h, init_vars lvars(pns[\<mapsto>]pvs)(This\<mapsto>a'))" and st=blk in state_ok_exec)
+          apply (rule_tac xs = "(np a' x, h, (init_vars lvars)(pns[\<mapsto>]pvs, This\<mapsto>a'))" and st=blk in state_ok_exec)
              apply assumption
             apply (simp (no_asm_simp) only: env_of_jmb_fst)
            apply assumption
diff -r 48b4e0cd94cd -r 7edbb16bc60f src/HOL/MicroJava/Comp/CorrCompTp.thy
--- a/src/HOL/MicroJava/Comp/CorrCompTp.thy	Tue Mar 14 14:00:07 2023 +0100
+++ b/src/HOL/MicroJava/Comp/CorrCompTp.thy	Tue Mar 14 18:19:10 2023 +0100
@@ -20,7 +20,7 @@
 
 definition local_env :: "[java_mb prog, cname, sig, vname list,(vname \<times> ty) list] \<Rightarrow> java_mb env" where
   "local_env G C S pns lvars == 
-     let (mn, pTs) = S in (G,map_of lvars(pns[\<mapsto>]pTs)(This\<mapsto>Class C))"
+     let (mn, pTs) = S in (G,(map_of lvars)(pns[\<mapsto>]pTs, This\<mapsto>Class C))"
 
 lemma local_env_fst [simp]: "fst (local_env G C S pns lvars) = G"
   by (simp add: local_env_def split_beta)
@@ -42,7 +42,7 @@
 subsection "index"
 
 lemma local_env_snd:
-  "snd (local_env G C (mn, pTs) pns lvars) = map_of lvars(pns[\<mapsto>]pTs)(This\<mapsto>Class C)"
+  "snd (local_env G C (mn, pTs) pns lvars) = (map_of lvars)(pns[\<mapsto>]pTs, This\<mapsto>Class C)"
   by (simp add: local_env_def)
 
 
@@ -62,7 +62,7 @@
 
 
 lemma map_upds_append: 
-  "length k1s = length x1s \<Longrightarrow> m(k1s[\<mapsto>]x1s)(k2s[\<mapsto>]x2s) = m ((k1s@k2s)[\<mapsto>](x1s@x2s))"
+  "length k1s = length x1s \<Longrightarrow> m(k1s[\<mapsto>]x1s, k2s[\<mapsto>]x2s) = m ((k1s@k2s)[\<mapsto>](x1s@x2s))"
   apply (induct k1s arbitrary: x1s m)
    apply simp
   apply (subgoal_tac "\<exists>x xr. x1s = x # xr")
@@ -114,7 +114,7 @@
    apply (clarify)
    apply (drule_tac x=kr in spec)
    apply (simp only: rev.simps)
-   apply (subgoal_tac "(Map.empty(rev kr @ [k'][\<mapsto>]rev xs @ [a])) = Map.empty (rev kr[\<mapsto>]rev xs)([k'][\<mapsto>][a])")
+   apply (subgoal_tac "(Map.empty(rev kr @ [k'][\<mapsto>]rev xs @ [a])) = Map.empty (rev kr[\<mapsto>]rev xs, [k'][\<mapsto>][a])")
     apply (simp split:if_split_asm)
    apply (simp add: map_upds_append [symmetric])
   apply (case_tac ks)
diff -r 48b4e0cd94cd -r 7edbb16bc60f src/HOL/MicroJava/Comp/DefsComp.thy
--- a/src/HOL/MicroJava/Comp/DefsComp.thy	Tue Mar 14 14:00:07 2023 +0100
+++ b/src/HOL/MicroJava/Comp/DefsComp.thy	Tue Mar 14 18:19:10 2023 +0100
@@ -65,7 +65,7 @@
 
 definition locals_locvars :: "java_mb prog \<Rightarrow> cname \<Rightarrow> sig \<Rightarrow> locvars \<Rightarrow> State.locals" where
   "locals_locvars G C S lvs == 
-  Map.empty ((gjmb_plns (gmb G C S))[\<mapsto>](tl lvs)) (This\<mapsto>(hd lvs))"
+  Map.empty ((gjmb_plns (gmb G C S))[\<mapsto>](tl lvs), This\<mapsto>(hd lvs))"
 
 definition locvars_xstate :: "java_mb prog \<Rightarrow> cname \<Rightarrow> sig \<Rightarrow> xstate \<Rightarrow> locvars" where
   "locvars_xstate G C S xs == locvars_locals G C S (gl xs)"
diff -r 48b4e0cd94cd -r 7edbb16bc60f src/HOL/MicroJava/J/Eval.thy
--- a/src/HOL/MicroJava/J/Eval.thy	Tue Mar 14 14:00:07 2023 +0100
+++ b/src/HOL/MicroJava/J/Eval.thy	Tue Mar 14 18:19:10 2023 +0100
@@ -83,7 +83,7 @@
 | Call: "[| G\<turnstile>Norm s0 -e\<succ>a'-> s1; a = the_Addr a';
             G\<turnstile>s1 -ps[\<succ>]pvs-> (x,(h,l)); dynT = fst (the (h a));
             (md,rT,pns,lvars,blk,res) = the (method (G,dynT) (mn,pTs));
-            G\<turnstile>(np a' x,(h,(init_vars lvars)(pns[\<mapsto>]pvs)(This\<mapsto>a'))) -blk-> s3;
+            G\<turnstile>(np a' x,(h,(init_vars lvars)(pns[\<mapsto>]pvs, This\<mapsto>a'))) -blk-> s3;
             G\<turnstile> s3 -res\<succ>v -> (x4,s4) |] ==>
          G\<turnstile>Norm s0 -{C}e..mn({pTs}ps)\<succ>v-> (x4,(heap s4,l))"
 
@@ -135,7 +135,7 @@
 lemmas eval_evals_exec_induct = eval_evals_exec.induct [split_format (complete)]
 
 lemma NewCI: "[|new_Addr (heap s) = (a,x);  
-       s' = c_hupd (heap s(a\<mapsto>(C,init_vars (fields (G,C))))) (x,s)|] ==>  
+       s' = c_hupd ((heap s)(a\<mapsto>(C,init_vars (fields (G,C))))) (x,s)|] ==>  
        G\<turnstile>Norm s -NewC C\<succ>Addr a-> s'"
 apply simp
 apply (rule eval_evals_exec.NewC)
@@ -197,7 +197,7 @@
   "[| G\<turnstile>Norm s0 -e\<succ>a'-> s1; a = the_Addr a';
       G\<turnstile>s1 -ps[\<succ>]pvs-> (x,(h,l)); dynT = fst (the (h a));
       (md,rT,pns,lvars,blk,res) = the (method (G,dynT) (mn,pTs));
-      G\<turnstile>(np a' x,(h,(init_vars lvars)(pns[\<mapsto>]pvs)(This\<mapsto>a'))) -blk-> s3;
+      G\<turnstile>(np a' x,(h,(init_vars lvars)(pns[\<mapsto>]pvs, This\<mapsto>a'))) -blk-> s3;
       G\<turnstile> s3 -res\<succ>v -> (x4,(h4, l4)) |] ==>
    G\<turnstile>Norm s0 -{C}e..mn({pTs}ps)\<succ>v-> (x4,(h4,l))"
 using Call[of G s0 e a' s1 a ps pvs x h l dynT md rT pns lvars blk res mn pTs s3 v x4 "(h4, l4)" C]
diff -r 48b4e0cd94cd -r 7edbb16bc60f src/HOL/MicroJava/J/Example.thy
--- a/src/HOL/MicroJava/J/Example.thy	Tue Mar 14 14:00:07 2023 +0100
+++ b/src/HOL/MicroJava/J/Example.thy	Tue Mar 14 18:19:10 2023 +0100
@@ -120,11 +120,11 @@
 
 abbreviation
   obj1  :: obj where
-  "obj1 == (Ext, Map.empty((vee, Base)\<mapsto>Bool False) ((vee, Ext )\<mapsto>Intg 0))"
+  "obj1 == (Ext, Map.empty((vee, Base)\<mapsto>Bool False, (vee, Ext )\<mapsto>Intg 0))"
 
 abbreviation "s0 == Norm    (Map.empty, Map.empty)"
 abbreviation "s1 == Norm    (Map.empty(a\<mapsto>obj1),Map.empty(e\<mapsto>Addr a))"
-abbreviation "s2 == Norm    (Map.empty(a\<mapsto>obj1),Map.empty(x\<mapsto>Null)(This\<mapsto>Addr a))"
+abbreviation "s2 == Norm    (Map.empty(a\<mapsto>obj1),Map.empty(x\<mapsto>Null, This\<mapsto>Addr a))"
 abbreviation "s3 == (Some NP, Map.empty(a\<mapsto>obj1),Map.empty(e\<mapsto>Addr a))"
 
 lemmas map_of_Cons = map_of.simps(2)
diff -r 48b4e0cd94cd -r 7edbb16bc60f src/HOL/MicroJava/J/Exceptions.thy
--- a/src/HOL/MicroJava/J/Exceptions.thy	Tue Mar 14 14:00:07 2023 +0100
+++ b/src/HOL/MicroJava/J/Exceptions.thy	Tue Mar 14 18:19:10 2023 +0100
@@ -10,9 +10,9 @@
   "blank G C \<equiv> (C,init_vars (fields(G,C)))" 
 
 definition start_heap :: "'c prog \<Rightarrow> aheap" where
-  "start_heap G \<equiv> Map.empty (XcptRef NullPointer \<mapsto> blank G (Xcpt NullPointer))
-                        (XcptRef ClassCast \<mapsto> blank G (Xcpt ClassCast))
-                        (XcptRef OutOfMemory \<mapsto> blank G (Xcpt OutOfMemory))"
+  "start_heap G \<equiv> Map.empty (XcptRef NullPointer \<mapsto> blank G (Xcpt NullPointer),
+                        XcptRef ClassCast \<mapsto> blank G (Xcpt ClassCast),
+                        XcptRef OutOfMemory \<mapsto> blank G (Xcpt OutOfMemory))"
 
 
 abbreviation
diff -r 48b4e0cd94cd -r 7edbb16bc60f src/HOL/MicroJava/J/JTypeSafe.thy
--- a/src/HOL/MicroJava/J/JTypeSafe.thy	Tue Mar 14 14:00:07 2023 +0100
+++ b/src/HOL/MicroJava/J/JTypeSafe.thy	Tue Mar 14 18:19:10 2023 +0100
@@ -105,7 +105,7 @@
    list_all2 (\<lambda>T T'. G\<turnstile>T\<preceq>T') pTs pTs'; wf_mhead G (mn,pTs') rT;  
   length pTs' = length pns; distinct pns;  
   Ball (set lvars) (case_prod (\<lambda>vn. is_type G))  
-  |] ==> G,h\<turnstile>init_vars lvars(pns[\<mapsto>]pvs)[::\<preceq>]map_of lvars(pns[\<mapsto>]pTs')"
+  |] ==> G,h\<turnstile>(init_vars lvars)(pns[\<mapsto>]pvs)[::\<preceq>](map_of lvars)(pns[\<mapsto>]pTs')"
 apply (unfold wf_mhead_def)
 apply( clarsimp)
 apply( rule lconf_ext_list)
@@ -122,7 +122,7 @@
      list_all2 (conf G h) pvs pTsa; 
      (md, rT, pns, lvars, blk, res) =  
                the (method (G,fst (the (h (the_Addr a')))) (mn, pTs')); 
-  \<forall>lT. (np a' None, h, init_vars lvars(pns[\<mapsto>]pvs)(This\<mapsto>a'))::\<preceq>(G, lT) -->  
+  \<forall>lT. (np a' None, h, (init_vars lvars)(pns[\<mapsto>]pvs, This\<mapsto>a'))::\<preceq>(G, lT) -->  
   (G, lT)\<turnstile>blk\<surd> -->  h\<le>|xi \<and>  (xcptb, xi, xl)::\<preceq>(G, lT);  
   \<forall>lT. (xcptb,xi, xl)::\<preceq>(G, lT) --> (\<forall>T. (G, lT)\<turnstile>res::T -->  
           xi\<le>|h' \<and> (x',h', xj)::\<preceq>(G, lT) \<and> (x' = None --> G,h'\<turnstile>v::\<preceq>T));  
diff -r 48b4e0cd94cd -r 7edbb16bc60f src/HOL/MicroJava/J/WellType.thy
--- a/src/HOL/MicroJava/J/WellType.thy	Tue Mar 14 14:00:07 2023 +0100
+++ b/src/HOL/MicroJava/J/WellType.thy	Tue Mar 14 18:19:10 2023 +0100
@@ -194,7 +194,7 @@
         This \<notin> set pns \<and> This \<notin> set (map fst lvars) \<and> 
   (\<forall>pn\<in>set pns. map_of lvars pn = None) \<and>
   (\<forall>(vn,T)\<in>set lvars. is_type G T) &
-  (let E = (G,map_of lvars(pns[\<mapsto>]pTs)(This\<mapsto>Class C)) in
+  (let E = (G,(map_of lvars)(pns[\<mapsto>]pTs, This\<mapsto>Class C)) in
    E\<turnstile>blk\<surd> \<and> (\<exists>T. E\<turnstile>res::T \<and> G\<turnstile>T\<preceq>rT))"
 
 abbreviation "wf_java_prog == wf_prog wf_java_mdecl"