Remove duplicate of ko_at_kheap_upd_id

proof/invariant-abstract/IpcDet_AI.thy

@@ -56,11 +56,6 @@ lemmas replies_blocked_safe_kheap_updates[simp] =
        replies_blocked_kh_update_sc[where f="\<lambda>sc v. sc\<lparr>sc_consumed := v\<rparr>"]
        replies_blocked_kh_update_tcb[where f="\<lambda>sc v. sc\<lparr>tcb_arch := v\<rparr>", simplified]
 
-lemma ko_at_kheap_upd_id[simp]:
-  "ko_at ko p s \<Longrightarrow> (s\<lparr>kheap := (kheap s)(p \<mapsto> ko)\<rparr> = s)"
-  unfolding obj_at_def fun_upd_def
-  by (rule abstract_state.equality, rule ext; simp)
-
 crunch send_ipc
  for typ_at[wp]: "\<lambda>s. P (typ_at T p s)"
   (wp: hoare_drop_imps mapM_wp_inv maybeM_inv simp: crunch_simps)
@@ -1082,12 +1077,12 @@ lemma set_mrs_valid_replies[wp]:
   "set_mrs receiver recv_buffer x2 \<lbrace> valid_replies_pred P \<rbrace>"
   unfolding set_mrs_def
   by (wpsimp wp:zipWithM_x_inv' set_object_wp,
-      clarsimp dest!: get_tcb_SomeD simp: obj_at_def)
+      clarsimp dest!: get_tcb_SomeD simp: ko_at_kheap_upd_id obj_at_def)
 
 lemma sched_context_update_consumed_valid_replies[wp]:
   "sched_context_update_consumed p \<lbrace> valid_replies_pred P \<rbrace>"
   unfolding sched_context_update_consumed_def
-  by (wpsimp wp: update_sched_context_wp)
+  by (wpsimp wp: update_sched_context_wp simp: ko_at_kheap_upd_id)
 
 crunch do_ipc_transfer
  for valid_replies[wp]: "valid_replies_pred P"

proof/invariant-abstract/SchedContextInv_AI.thy

@@ -1249,21 +1249,21 @@ lemma shows
    update_sched_context p (\<lambda>_. sc\<lparr>sc_sporadic := f \<rparr>)
    \<lbrace>\<lambda>rv. valid_replies_pred P\<rbrace>"
   by (wpsimp wp: update_sched_context_wp,
-      fastforce dest: ko_at_obj_congD)+
+      fastforce simp: ko_at_kheap_upd_id dest: ko_at_obj_congD)+
 
 lemma update_sc_refills_period_refill_max_valid_replies:
   "\<lbrace>valid_replies_pred P and (\<lambda>s. (\<exists>n. ko_at (SchedContext sc n) p s))\<rbrace>
    update_sched_context p (\<lambda>_. sc\<lparr>sc_period := period, sc_refill_max := m, sc_refills := r, sc_budget := b\<rparr>)
    \<lbrace>\<lambda>rv. valid_replies_pred P\<rbrace>"
   by (wpsimp wp: update_sched_context_wp,
-      fastforce dest: ko_at_obj_congD)
+      fastforce simp: ko_at_kheap_upd_id dest: ko_at_obj_congD)
 
 lemma update_sc_refills_valid_replies[wp]:
   "\<lbrace>valid_replies_pred P and (\<lambda>s. (\<exists>n. ko_at (SchedContext sc n) p s))\<rbrace>
    update_sched_context p (\<lambda>_. sc\<lparr>sc_refills := r\<rparr>)
    \<lbrace>\<lambda>rv. valid_replies_pred P\<rbrace>"
   by (wpsimp wp: update_sched_context_wp,
-      fastforce dest: ko_at_obj_congD)
+      fastforce simp: ko_at_kheap_upd_id dest: ko_at_obj_congD)
 
 lemma shows
   update_sc_badge_cur_sc_tcb:
@@ -1431,10 +1431,8 @@ lemma update_sched_context_sc_refills_update_invs:
                    update_sched_context_refs_of_same)
 
 lemma sc_consumed_add_valid_replies:
-  "\<lbrace> valid_replies \<rbrace>
-   update_sched_context scp (\<lambda>sc. sc\<lparr>sc_consumed := sc_consumed sc + consumed\<rparr>)
-   \<lbrace> \<lambda>_. valid_replies \<rbrace>"
-  by (wpsimp wp: update_sched_context_wp)
+  "update_sched_context scp (\<lambda>sc. sc\<lparr>sc_consumed := sc_consumed sc + consumed\<rparr>) \<lbrace>valid_replies\<rbrace>"
+  by (wpsimp wp: update_sched_context_wp simp: ko_at_kheap_upd_id)
 
 lemma sc_consumed_add_invs:
   "\<lbrace>\<lambda>s. invs s\<rbrace>

proof/refine/RISCV64/Reply_R.thy

@@ -641,7 +641,7 @@ lemma set_reply_obj_ref_noop:
    (return ())
    (set_reply_obj_ref (K id) rptr x)"
   by (clarsimp simp: set_simple_ko_def monadic_rewrite_def exec_gets
-                     update_sk_obj_ref_def gets_the_def
+                     update_sk_obj_ref_def gets_the_def ko_at_kheap_upd_id
                      get_simple_ko_def partial_inv_inj_Some get_object_def bind_assoc obj_at_def
                      is_reply_def2 set_object_def exec_get put_id_return)