Updated files to work with Isabelle 2023

Author: tdardinier

BoogieLang/Semantics.thy

@@ -111,8 +111,8 @@ should not happen).\<close>
 definition update_var :: "var_context \<Rightarrow> 'a nstate \<Rightarrow> vname \<Rightarrow> 'a val \<Rightarrow>  'a nstate"
   where 
    "update_var \<Lambda> n_s x v =
-            (case (map_of (snd \<Lambda>) x) of Some res \<Rightarrow> n_s\<lparr>local_state := local_state(n_s)(x \<mapsto> v)\<rparr>  |
-                                 None \<Rightarrow> n_s\<lparr>global_state := global_state(n_s)(x \<mapsto> v) \<rparr>)"
+            (case (map_of (snd \<Lambda>) x) of Some res \<Rightarrow> n_s\<lparr>local_state := (local_state(n_s))(x \<mapsto> v) \<rparr>  |
+                                 None \<Rightarrow> n_s\<lparr>global_state := (global_state(n_s))(x \<mapsto> v) \<rparr>)"
 
 definition update_var_opt :: "var_context \<Rightarrow> 'a nstate \<Rightarrow> vname \<Rightarrow> 'a val option \<Rightarrow>  'a nstate"
   where 

BoogieLang/Util.thy

@@ -393,27 +393,27 @@ lemma update_var_same_state:
   using assms update_var_def lookup_var_def
 proof (cases "map_of (snd \<Lambda>) x")
   case None
-  hence update_global:"?ns' = ns\<lparr>global_state := global_state(ns)(x \<mapsto> v)\<rparr>"
+  hence update_global:"?ns' = ns\<lparr>global_state := (global_state(ns))(x \<mapsto> v)\<rparr>"
     by (simp add: update_var_def)
 
   from assms have global_ns:"global_state ns x = Some v"
     by (metis None lookup_var_global prod.collapse)
 
-  have "global_state(ns)(x \<mapsto> v) = global_state ns"
+  have "(global_state(ns))(x \<mapsto> v) = global_state ns"
     apply (rule HOL.ext)
     by (simp add: global_ns)
   then show ?thesis 
     using update_global
     by simp
 next
   case (Some a)
-  hence update_local:"?ns' = ns\<lparr>local_state := local_state(ns)(x \<mapsto> v)\<rparr>"
+  hence update_local:"?ns' = ns\<lparr>local_state := (local_state(ns))(x \<mapsto> v)\<rparr>"
     by (simp add: update_var_def)
 
   from assms have local_ns:"local_state ns x = Some v"
     by (metis Some lookup_var_local prod.collapse)
 
-  have "local_state(ns)(x \<mapsto> v) = local_state ns"
+  have "(local_state(ns))(x \<mapsto> v) = local_state ns"
     apply (rule HOL.ext)
     by (simp add: local_ns)
   then show ?thesis