update to Isabelle 2023

camkes/cdl-refine/Eval_CAMKES_CDL.thy

@@ -211,7 +211,7 @@ lemma Collect_asid_high__eval_helper:
 section \<open>Assorted helpers\<close>
 lemma fun_upds_to_map_of[THEN eq_reflection]:
   "Map.empty = map_of []"
-  "(map_of xs(k \<mapsto> v)) = map_of ((k, v) # xs)"
+  "((map_of xs)(k \<mapsto> v)) = map_of ((k, v) # xs)"
   by auto
 
 lemma subst_eqn_helper:

lib/Eisbach_Tools/Apply_Debug.thy

@@ -484,14 +484,14 @@ fun maybe_bind st (_,[tok]) ctxt =
 
       val local_facts = Facts.dest_static true [(Proof_Context.facts_of target)] local_facts;
 
-      val _ = Token.assign (SOME (Token.Declaration (fn phi =>
-      Data.put (SOME (phi,ctxt, {private_dyn_facts = private_dyns, local_facts = local_facts}))))) tok;
+      val _ = Token.assign (SOME (Token.Declaration (Morphism.entity (fn phi =>
+      Data.put (SOME (phi,ctxt, {private_dyn_facts = private_dyns, local_facts = local_facts})))))) tok;
 
    in ctxt end
   else
     let
       val SOME (Token.Declaration decl) = Token.get_value tok;
-      val dummy_ctxt = decl Morphism.identity (Context.Proof ctxt);
+      val dummy_ctxt = Morphism.form decl (Context.Proof ctxt);
       val SOME (phi,static_ctxt,{private_dyn_facts, local_facts}) = Data.get dummy_ctxt;
 
       val old_facts = Proof_Context.facts_of static_ctxt;

lib/Eisbach_Tools/Apply_Trace.thy

@@ -225,7 +225,7 @@ let
 
   val deps = case query of SOME (raw_query,pos) =>
     let
-      val pos' = perhaps (try (Position.advance_offsets 1)) pos;
+      val pos' = perhaps (try (Position.shift_offsets {remove_id = false} 1)) pos;
       val q = Find_Theorems.read_query pos' raw_query;
       val results = Find_Theorems.find_theorems_cmd ctxt (SOME thm) (SOME 1000000000) false q
                     |> snd

lib/Lib.thy

@@ -2237,7 +2237,7 @@ lemma map_of_zip_is_index:
 
 lemma map_of_zip_take_update:
   "\<lbrakk>i < length xs; length xs \<le> length ys; distinct xs\<rbrakk>
-  \<Longrightarrow> map_of (zip (take i xs) ys)(xs ! i \<mapsto> (ys ! i)) = map_of (zip (take (Suc i) xs) ys)"
+  \<Longrightarrow> (map_of (zip (take i xs) ys)) (xs ! i \<mapsto> ys ! i) = map_of (zip (take (Suc i) xs) ys)"
   apply (rule ext, rename_tac x)
   apply (case_tac "x=xs ! i"; clarsimp)
    apply (rule map_of_is_SomeI[symmetric])

lib/ML_Goal.thy

@@ -109,7 +109,7 @@ fun begin_proof ((name, attrs): Attrib.binding, ml_block: Input.source) ctxt =
             val ((res_name, res), ctxt') =
                 Local_Theory.note (binding, thms) ctxt;
             val _ =
-                Proof_Display.print_results true start_pos ctxt'
+                Proof_Display.print_results { interactive = true, pos = start_pos, proof_state = true } ctxt'
                   (("theorem", res_name), [("", res)])
           in ctxt' end
     in

lib/Qualify.thy

@@ -110,7 +110,7 @@ val _ =
           Toplevel.theory (set_global_qualify {name = str, target_name = case target of SOME (nm, _) => nm | _ => str})));
 
 fun syntax_alias global_alias local_alias b name =
-  Local_Theory.declaration {syntax = true, pervasive = true} (fn phi =>
+  Local_Theory.declaration {syntax = true, pos = Position.none, pervasive = true} (fn phi =>
     let val b' = Morphism.binding phi b
     in Context.mapping (global_alias b' name) (local_alias b' name) end);
 

lib/Requalify.thy

@@ -49,7 +49,7 @@ in
 end
 
 fun syntax_alias global_alias local_alias b (name : string) =
-  Local_Theory.declaration {syntax = false, pervasive = true} (fn phi =>
+  Local_Theory.declaration {syntax = false, pos = Position.none, pervasive = true} (fn phi =>
     let val b' = Morphism.binding phi b
     in Context.mapping (global_alias b' name) (local_alias b' name) end);
 

lib/Word_Lib/Bitwise.thy

@@ -365,7 +365,7 @@ lemma upt_eq_list_intros:
   by (simp_all add: upt_eq_Cons_conv)
 
 
-subsection \<open>Tactic definition\<close>
+text \<open>Tactic definition\<close>
 
 lemma if_bool_simps:
   "If p True y = (p \<or> y) \<and> If p False y = (\<not> p \<and> y) \<and>

lib/Word_Lib/More_Word.thy

@@ -1872,14 +1872,14 @@ lemma nth_0: "\<not> bit (0 :: 'a::len word) n"
 lemma nth_minus1: "bit (-1 :: 'a::len word) n \<longleftrightarrow> n < LENGTH('a)"
   by transfer simp
 
-lemma nth_ucast:
+lemma nth_ucast_weak:
   "bit (ucast w::'a::len word) n = (bit w n \<and> n < LENGTH('a))"
   by transfer (simp add: bit_take_bit_iff ac_simps)
 
-lemma drop_bit_numeral_bit0_1 [simp]:
-  \<open>drop_bit (Suc 0) (numeral k) =
-    (word_of_int (drop_bit (Suc 0) (take_bit LENGTH('a) (numeral k))) :: 'a::len word)\<close>
-  by (metis Word_eq_word_of_int drop_bit_word.abs_eq of_int_numeral)
+lemma nth_ucast:
+  "bit (ucast (w::'a::len word)::'b::len word) n =
+   (bit w n \<and> n < min LENGTH('a) LENGTH('b))"
+  by (auto simp: not_le nth_ucast_weak dest: bit_imp_le_length)
 
 lemma nth_mask:
   \<open>bit (mask n :: 'a::len word) i \<longleftrightarrow> i < n \<and> i < size (mask n :: 'a word)\<close>

lib/Word_Lib/More_Word_Operations.thy

@@ -302,13 +302,21 @@ lemma alignUp_not_aligned_eq:
   and     sz: "n < LENGTH('a)"
   shows   "alignUp a n = (a div 2 ^ n + 1) * 2 ^ n"
 proof -
+  from \<open>n < LENGTH('a)\<close> have \<open>(2::int) ^ n < 2 ^ LENGTH('a)\<close>
+    by simp
+  with take_bit_int_less_exp [of n]
+    have *: \<open>take_bit n k < 2 ^ LENGTH('a)\<close> for k :: int
+    by (rule less_trans)
   have anz: "a mod 2 ^ n \<noteq> 0"
     by (rule not_aligned_mod_nz) fact+
-
-  then have um: "unat (a mod 2 ^ n - 1) div 2 ^ n = 0" using sz
-    by (meson Euclidean_Division.div_eq_0_iff le_m1_iff_lt measure_unat order_less_trans
-              unat_less_power word_less_sub_le word_mod_less_divisor)
-
+  then have um: "unat (a mod 2 ^ n - 1) div 2 ^ n = 0"
+    apply (transfer fixing: n) using sz
+    apply (simp flip: take_bit_eq_mod add: div_eq_0_iff)
+    apply (subst take_bit_int_eq_self)
+    using *
+     apply (auto simp add: diff_less_eq intro: less_imp_le)
+    apply (simp add: less_le)
+    done
   have "a + 2 ^ n - 1 = (a div 2 ^ n) * 2 ^ n + (a mod 2 ^ n) + 2 ^ n - 1"
     by (simp add: word_mod_div_equality)
   also have "\<dots> = (a mod 2 ^ n - 1) + (a div 2 ^ n + 1) * 2 ^ n"

lib/Word_Lib/Signed_Division_Word.thy

@@ -10,6 +10,12 @@ theory Signed_Division_Word
   imports "HOL-Library.Signed_Division" "HOL-Library.Word"
 begin
 
+text \<open>
+  The following specification of division follows ISO C99, which in turn adopted the typical
+  behavior of hardware modern in the beginning of the 1990ies.
+  The underlying integer division is named ``T-division'' in \cite{leijen01}.
+\<close>
+
 instantiation word :: (len) signed_division
 begin
 

lib/Word_Lib/Word_Lemmas.thy

@@ -153,8 +153,8 @@ lemma sshiftr_n1: "-1 >>> n = -1"
 
 lemma nth_sshiftr:
   "bit (w >>> m) n = (n < size w \<and> (if n + m \<ge> size w then bit w (size w - 1) else bit w (n + m)))"
-  apply (clarsimp simp add: bit_simps word_size ac_simps not_less)
-  apply (metis add.commute bit_imp_le_length bit_shiftr_word_iff le_diff_conv not_le)
+  apply (auto simp add: bit_simps word_size ac_simps not_less)
+  apply (meson bit_imp_le_length bit_shiftr_word_iff leD)
   done
 
 lemma sshiftr_numeral:
@@ -508,8 +508,9 @@ next
       also have \<open>\<dots> \<longleftrightarrow> unat x < 2 ^ n div 2 ^ y\<close>
         using * by (simp add: less_le)
       finally show ?thesis
-      using that \<open>x \<noteq> 0\<close> by (simp flip: push_bit_eq_mult drop_bit_eq_div
-        add: shiftr_def shiftl_def unat_drop_bit_eq word_less_iff_unsigned [where ?'a = nat])
+        using that \<open>x \<noteq> 0\<close>
+        by (simp flip: push_bit_eq_mult drop_bit_eq_div
+                 add: shiftr_def shiftl_def unat_drop_bit_eq word_less_iff_unsigned [where ?'a = nat])
     qed
   qed
 qed
@@ -716,7 +717,8 @@ lemma word_and_notzeroD:
 lemma shiftr_le_0:
   "unat (w::'a::len word) < 2 ^ n \<Longrightarrow> w >> n = (0::'a::len word)"
   by (auto simp add: take_bit_word_eq_self_iff word_less_nat_alt shiftr_def
-           simp flip: take_bit_eq_self_iff_drop_bit_eq_0 intro: ccontr)
+           simp flip: take_bit_eq_self_iff_drop_bit_eq_0
+           intro: ccontr)
 
 lemma of_nat_shiftl:
   "(of_nat x << n) = (of_nat (x * 2 ^ n) :: ('a::len) word)"
@@ -1466,9 +1468,9 @@ lemma mask_shift_sum:
   "\<lbrakk> a \<ge> b; unat n = unat (p AND mask b) \<rbrakk>
    \<Longrightarrow> (p AND NOT(mask a)) + (p AND mask a >> b) * (1 << b) + n = (p :: 'a :: len word)"
   apply (simp add: shiftl_def shiftr_def flip: push_bit_eq_mult take_bit_eq_mask word_unat_eq_iff)
-  apply (subst disjunctive_add, clarsimp simp add: bit_simps)+
+  apply (subst disjunctive_add, fastforce simp: bit_simps)+
   apply (rule bit_word_eqI)
-  apply (auto simp add: bit_simps)
+  apply (fastforce simp: bit_simps)[1]
   done
 
 lemma is_up_compose:
@@ -1583,10 +1585,7 @@ next
     apply (rule impI)
     apply (subst bit_eq_iff)
     apply (simp add: bit_take_bit_iff bit_signed_take_bit_iff min_def)
-    apply (auto simp add: Suc_le_eq)
-    using less_imp_le_nat apply blast
-    using less_imp_le_nat apply blast
-    done
+    by (auto simp add: Suc_le_eq) (meson dual_order.strict_iff_not)+
 qed
 
 lemma scast_ucast_mask_compare:
@@ -1820,11 +1819,7 @@ proof (rule classical)
      apply (insert sdiv_int_range [where a="sint a" and b="sint b"])[1]
      apply (clarsimp simp: word_size)
     apply (insert sdiv_int_range [where a="sint a" and b="sint b"])[1]
-    apply auto
-    apply (cases \<open>size a\<close>)
-     apply simp_all
-    apply (smt (z3) One_nat_def diff_Suc_1 signed_word_eqI sint_int_min sint_range_size wsst_TYs(3))
-    done
+    by (smt (verit, best) One_nat_def signed_word_eqI sint_greater_eq sint_int_min sint_less wsst_TYs(3))
 
   have result_range_simple: "(sint a sdiv sint b \<in> ?range) \<Longrightarrow> ?thesis"
     apply (insert sdiv_int_range [where a="sint a" and b="sint b"])

lib/Word_Lib/Word_Lib_Sumo.thy

@@ -131,10 +131,4 @@ notation (input)
 
 lemmas cast_simps = cast_simps ucast_down_bl
 
-(* shadows the slightly weaker Word.nth_ucast *)
-lemma nth_ucast:
-  "(ucast (w::'a::len word)::'b::len word) !! n =
-   (w !! n \<and> n < min LENGTH('a) LENGTH('b))"
-  by (auto simp: not_le dest: bit_imp_le_length)
-
 end

lib/clib/CCorresLemmas.thy

@@ -518,7 +518,7 @@ lemma lift_t_super_update:
   and    eu: "export_uinfo s = typ_uinfo_t TYPE('b)"
   and    lp: "lift_t g (h, d) p = Some v'"
   shows "lift_t g (heap_update (Ptr &(p\<rightarrow>f)) v h, d)
-  = lift_t g (h, d)(p \<mapsto> field_update (field_desc s) (to_bytes_p v) v')"
+         = (lift_t g (h, d)) (p \<mapsto> field_update (field_desc s) (to_bytes_p v) v')"
   using fl eu lp
   apply -
   apply (rule trans [OF lift_t_super_field_update super_field_update_lookup])

lib/defs.ML

@@ -29,7 +29,7 @@ val opt_unchecked_overloaded =
       @{keyword "overloaded"} >> K (false, true)) --| @{keyword ")"})) (false, false);
 
 fun syntax_alias global_alias local_alias b name =
-  Local_Theory.declaration {syntax = true, pervasive = true} (fn phi =>
+  Local_Theory.declaration {syntax = true, pos = Position.none, pervasive = true} (fn phi =>
     let val b' = Morphism.binding phi b
     in Context.mapping (global_alias b' name) (local_alias b' name) end);
 

misc/jedit/macros/goto-error.bsh

@@ -25,8 +25,8 @@ import isabelle.jedit.*;
 msg(s) { Macros.message(view, s); }
 
 // isabelle setup
-model = Document_Model.get(textArea.getBuffer());
-snapshot = model.get().snapshot();
+model = Document_Model.get_model(textArea.getBuffer());
+snapshot = Document_Model.snapshot(model.get());
 
 class FirstError {
     public int first_error_pos = -1;

proof/access-control/ARM/ArchAccess.thy

@@ -196,10 +196,10 @@ lemmas integrity_asids_kh_upds =
 declare integrity_asids_def[simp]
 
 lemma integrity_asids_kh_upds':
-  "integrity_asids aag subjects x a (s\<lparr>kheap := kheap s(p \<mapsto> CNode sz cs)\<rparr>) s"
-  "integrity_asids aag subjects x a (s\<lparr>kheap := kheap s(p \<mapsto> TCB tcb)\<rparr>) s"
-  "integrity_asids aag subjects x a (s\<lparr>kheap := kheap s(p \<mapsto> Endpoint ep)\<rparr>) s"
-  "integrity_asids aag subjects x a (s\<lparr>kheap := kheap s(p \<mapsto> Notification ntfn)\<rparr>) s"
+  "integrity_asids aag subjects x a (s\<lparr>kheap := (kheap s)(p \<mapsto> CNode sz cs)\<rparr>) s"
+  "integrity_asids aag subjects x a (s\<lparr>kheap := (kheap s)(p \<mapsto> TCB tcb)\<rparr>) s"
+  "integrity_asids aag subjects x a (s\<lparr>kheap := (kheap s)(p \<mapsto> Endpoint ep)\<rparr>) s"
+  "integrity_asids aag subjects x a (s\<lparr>kheap := (kheap s)(p \<mapsto> Notification ntfn)\<rparr>) s"
   by auto
 
 lemma integrity_asids_kh_update:

proof/access-control/ARM/ArchAccess_AC.thy

@@ -91,7 +91,7 @@ lemma integrity_asids_refl[Access_AC_assms, simp]:
 
 lemma integrity_asids_update_autarch[Access_AC_assms]:
   "\<lbrakk> \<forall>x a. integrity_asids aag subjects x a st s; is_subject aag ptr \<rbrakk>
-     \<Longrightarrow> \<forall>x a. integrity_asids aag subjects x a st (s\<lparr>kheap := kheap s(ptr \<mapsto> obj)\<rparr>)"
+     \<Longrightarrow> \<forall>x a. integrity_asids aag subjects x a st (s\<lparr>kheap := (kheap s)(ptr \<mapsto> obj)\<rparr>)"
   by simp
 
 end

proof/access-control/ARM/ArchCNode_AC.thy

@@ -78,14 +78,14 @@ crunches prepare_thread_delete, arch_finalise_cap
   (wp: crunch_wps hoare_vcg_if_lift2 simp: unless_def)
 
 lemma state_vrefs_tcb_upd[CNode_AC_assms]:
-  "tcb_at t s \<Longrightarrow> state_vrefs (s\<lparr>kheap := kheap s(t \<mapsto> TCB tcb)\<rparr>) = state_vrefs s"
+  "tcb_at t s \<Longrightarrow> state_vrefs (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB tcb)\<rparr>) = state_vrefs s"
   apply (rule ext)
   apply (auto simp: state_vrefs_def vs_refs_no_global_pts_def tcb_at_def dest!: get_tcb_SomeD)
   done
 
 lemma state_vrefs_simple_type_upd[CNode_AC_assms]:
   "\<lbrakk> ko_at ko ptr s; is_simple_type ko; a_type ko = a_type (f val) \<rbrakk>
-     \<Longrightarrow> state_vrefs (s\<lparr>kheap := kheap s(ptr \<mapsto> f val)\<rparr>) = state_vrefs s"
+     \<Longrightarrow> state_vrefs (s\<lparr>kheap := (kheap s)(ptr \<mapsto> f val)\<rparr>) = state_vrefs s"
   apply (rule ext)
   apply (auto simp: state_vrefs_def vs_refs_no_global_pts_def obj_at_def partial_inv_def a_type_def
              split: kernel_object.splits arch_kernel_obj.splits if_splits)

proof/access-control/ARM/ArchFinalise_AC.thy

@@ -93,7 +93,7 @@ proof (induct rule: cap_revoke.induct[where ?a1.0=s])
 qed
 
 lemma finalise_cap_caps_of_state_nullinv[Finalise_AC_assms]:
-  "\<lbrace>\<lambda>s. P (caps_of_state s) \<and> (\<forall>p. P (caps_of_state s(p \<mapsto> NullCap)))\<rbrace>
+  "\<lbrace>\<lambda>s. P (caps_of_state s) \<and> (\<forall>p. P ((caps_of_state s)(p \<mapsto> NullCap)))\<rbrace>
    finalise_cap cap final
    \<lbrace>\<lambda>_ s. P (caps_of_state s)\<rbrace>"
   by (cases cap;

proof/access-control/ARM/ArchIpc_AC.thy

@@ -175,7 +175,7 @@ lemma handle_arch_fault_reply_respects[Ipc_AC_assms]:
 lemma auth_ipc_buffers_kheap_update[Ipc_AC_assms]:
   "\<lbrakk> x \<in> auth_ipc_buffers st thread; kheap st thread = Some (TCB tcb);
      kheap s thread = Some (TCB tcb'); tcb_ipcframe tcb = tcb_ipcframe tcb' \<rbrakk>
-     \<Longrightarrow> x \<in> auth_ipc_buffers (s\<lparr>kheap := kheap s(thread \<mapsto> TCB tcb)\<rparr>) thread"
+     \<Longrightarrow> x \<in> auth_ipc_buffers (s\<lparr>kheap := (kheap s)(thread \<mapsto> TCB tcb)\<rparr>) thread"
   by (clarsimp simp: auth_ipc_buffers_member_def get_tcb_def caps_of_state_tcb)
 
 lemma auth_ipc_buffers_machine_state_update[Ipc_AC_assms, simp]:

proof/access-control/Access_AC.thy

@@ -208,17 +208,17 @@ lemmas state_objs_to_policy_cases
 
 lemma tcb_states_of_state_preserved:
   "\<lbrakk> get_tcb thread s = Some tcb; tcb_state tcb' = tcb_state tcb \<rbrakk>
-     \<Longrightarrow> tcb_states_of_state (s\<lparr>kheap := kheap s(thread \<mapsto> TCB tcb')\<rparr>) = tcb_states_of_state s"
+     \<Longrightarrow> tcb_states_of_state (s\<lparr>kheap := (kheap s)(thread \<mapsto> TCB tcb')\<rparr>) = tcb_states_of_state s"
   by (auto split: option.splits simp: tcb_states_of_state_def get_tcb_def)
 
 lemma thread_st_auth_preserved:
   "\<lbrakk> get_tcb thread s = Some tcb; tcb_state tcb' = tcb_state tcb \<rbrakk>
-     \<Longrightarrow> thread_st_auth (s\<lparr>kheap := kheap s(thread \<mapsto> TCB tcb')\<rparr>) = thread_st_auth s"
+     \<Longrightarrow> thread_st_auth (s\<lparr>kheap := (kheap s)(thread \<mapsto> TCB tcb')\<rparr>) = thread_st_auth s"
   by (simp add: tcb_states_of_state_preserved thread_st_auth_def)
 
 lemma thread_bound_ntfns_preserved:
   "\<lbrakk> get_tcb thread s = Some tcb; tcb_bound_notification tcb' = tcb_bound_notification tcb \<rbrakk>
-     \<Longrightarrow> thread_bound_ntfns (s\<lparr>kheap := kheap s(thread \<mapsto> TCB tcb')\<rparr>) = thread_bound_ntfns s"
+     \<Longrightarrow> thread_bound_ntfns (s\<lparr>kheap := (kheap s)(thread \<mapsto> TCB tcb')\<rparr>) = thread_bound_ntfns s"
   by (auto simp: thread_bound_ntfns_def get_tcb_def split: option.splits)
 
 lemma is_transferable_null_filter[simp]:
@@ -865,7 +865,7 @@ locale Access_AC_2 = Access_AC_1 +
        \<Longrightarrow> (\<forall>x a. integrity_asids aag subjects x a s s'')"
   and integrity_asids_update_autarch:
     "\<lbrakk> \<forall>x a. integrity_asids aag {pasSubject aag} x a s s'; is_subject aag ptr \<rbrakk>
-       \<Longrightarrow> \<forall>x a. integrity_asids aag {pasSubject aag} x a s (s'\<lparr>kheap := kheap s'(ptr \<mapsto> obj)\<rparr>)"
+       \<Longrightarrow> \<forall>x a. integrity_asids aag {pasSubject aag} x a s (s'\<lparr>kheap := (kheap s')(ptr \<mapsto> obj)\<rparr>)"
 begin
 
 section \<open>Generic AC stuff\<close>
@@ -980,7 +980,7 @@ lemma integrity_refl [simp]:
 
 lemma integrity_update_autarch:
   "\<lbrakk> integrity aag X st s; is_subject aag ptr \<rbrakk>
-     \<Longrightarrow> integrity aag X st (s\<lparr>kheap := kheap s(ptr \<mapsto> obj)\<rparr>)"
+     \<Longrightarrow> integrity aag X st (s\<lparr>kheap := (kheap s)(ptr \<mapsto> obj)\<rparr>)"
   unfolding integrity_subjects_def
   apply (intro conjI,simp_all)
     apply clarsimp

proof/access-control/CNode_AC.thy

@@ -56,11 +56,11 @@ locale CNode_AC_1 =
        \<Longrightarrow> state_asids_to_policy_arch aag (caps(ptr \<mapsto> cap, ptr' \<mapsto> cap')) as vrefs \<subseteq> pasPolicy aag"
   and state_vrefs_tcb_upd:
     "\<lbrakk> pspace_aligned s; valid_vspace_objs s; valid_arch_state s; tcb_at tptr s \<rbrakk>
-       \<Longrightarrow> state_vrefs (s\<lparr>kheap := kheap s(tptr \<mapsto> TCB tcb)\<rparr>) = state_vrefs s"
+       \<Longrightarrow> state_vrefs (s\<lparr>kheap := (kheap s)(tptr \<mapsto> TCB tcb)\<rparr>) = state_vrefs s"
   and state_vrefs_simple_type_upd:
     "\<lbrakk> pspace_aligned s; valid_vspace_objs s; valid_arch_state s;
        ko_at ko p s; is_simple_type ko; a_type ko = a_type (f (val :: 'b)) \<rbrakk>
-       \<Longrightarrow> state_vrefs (s\<lparr>kheap := kheap s(p \<mapsto> f val)\<rparr>) = state_vrefs s"
+       \<Longrightarrow> state_vrefs (s\<lparr>kheap := (kheap s)(p \<mapsto> f val)\<rparr>) = state_vrefs s"
   and a_type_arch_object_not_tcb[simp]:
     "a_type (ArchObj arch_kernel_obj) \<noteq> ATCB"
   and set_cap_state_vrefs:
@@ -969,10 +969,10 @@ lemma set_untyped_cap_as_full_is_transferable[wp]:
   using untyped_not_transferable max_free_index_update_preserve_untyped by simp
 
 lemma set_untyped_cap_as_full_is_transferable':
-  "\<lbrace>\<lambda>s. is_transferable ((caps_of_state s(slot2 \<mapsto> new_cap)) slot3) \<and>
+  "\<lbrace>\<lambda>s. is_transferable (((caps_of_state s)(slot2 \<mapsto> new_cap)) slot3) \<and>
         Some src_cap = (caps_of_state s slot)\<rbrace>
    set_untyped_cap_as_full src_cap new_cap slot
-   \<lbrace>\<lambda>_ s. is_transferable ((caps_of_state s(slot2 \<mapsto> new_cap)) slot3)\<rbrace>"
+   \<lbrace>\<lambda>_ s. is_transferable (((caps_of_state s)(slot2 \<mapsto> new_cap)) slot3)\<rbrace>"
   apply (clarsimp simp: set_untyped_cap_as_full_def)
   apply safe
   apply (wp,fastforce)+