squash: PR suggestions

Signed-off-by: Corey Lewis <corey.lewis@proofcraft.systems>

proof/invariant-abstract/KHeap_AI.thy

@@ -2697,16 +2697,21 @@ lemma update_reply_pred_tcb_at[wp]:
   "update_reply ptr update \<lbrace>\<lambda>s. P (pred_tcb_at proj f t s)\<rbrace>"
   by (wpsimp simp: update_reply_def set_object_def get_object_def pred_tcb_at_def obj_at_def)
 
-lemma update_reply_valid_replies[wp]:
-  "update_reply ptr f \<lbrace>valid_replies_pred P\<rbrace>"
-  apply (rule hoare_lift_Pf2[where f=replies_blocked, rotated])
-   apply (wp replies_blocked_lift)
-  apply (wp replies_with_sc_lift)
-   apply (wp update_reply_wp)
-   apply (clarsimp simp: sc_replies_sc_at_def obj_at_def )
+lemma update_reply_replies_blocked[wp]:
+  "update_reply ptr f \<lbrace>\<lambda>s. P (replies_blocked s)\<rbrace>"
+  by (wpsimp wp: replies_blocked_lift)
+
+lemma update_reply_replies_with_sc[wp]:
+  "update_reply ptr f \<lbrace>\<lambda>s. P (replies_with_sc s)\<rbrace>"
+  apply (wpsimp wp: replies_with_sc_lift update_reply_wp)
+   apply (clarsimp simp: sc_replies_sc_at_def obj_at_def)
   apply clarsimp
   done
 
+lemma update_reply_valid_replies[wp]:
+  "update_reply ptr f \<lbrace>valid_replies_pred P\<rbrace>"
+  by (wp_pre, wps, wpsimp+)
+
 lemma update_reply_can_grant_reply_tcb_reply_at[wp]:
   "update_reply ptr (reply_can_grant_update f) \<lbrace>\<lambda>s. P (reply_tcb_reply_at Q t s) \<rbrace>"
   by (wpsimp simp: update_reply_def reply_at_ppred_def obj_at_def

proof/refine/RISCV64/Ipc_R.thy

@@ -5353,12 +5353,7 @@ crunch ifCondRefillUnblockCheck
 lemma replyCanGrant_update_valid_replies'_sc_asrt[wp]:
   shows "updateReply ptr (replyCanGrant_update f) \<lbrace>valid_replies'_sc_asrt ptr\<rbrace>"
   apply (rule valid_replies'_sc_asrt_lift; wpsimp wp: updateReply_wp_all)
-    apply (subst opt_map_upd_triv)
-     apply (clarsimp simp: opt_map_def obj_at'_def)
-    apply clarsimp
-   apply (subst opt_map_upd_triv)
-    apply (clarsimp simp: opt_map_def obj_at'_def)
-   apply clarsimp
+    apply (subst opt_map_upd_triv; clarsimp simp: opt_map_def obj_at'_def)+
   apply (fastforce simp: pred_tcb_at'_def  obj_at'_def)
   done
 
@@ -5499,13 +5494,7 @@ lemma receiveIPC_corres:
                                     prefer 5 \<comment> \<open> defer wp until corres complete \<close>
                                     apply (rule corres_split[OF setThreadState_corres], simp)
                                       apply (rule possibleSwitchTo_corres, simp)
-                                     apply (wpsimp wp: set_thread_state_valid_sched_action)
-                                    apply wpsimp
-                                   apply wpsimp
-                                  apply (wpsimp wp: updateReply_valid_objs')
-                                 apply wpsimp
-                                apply wpsimp
-                               apply clarsimp
+                                     apply (wpsimp wp: set_thread_state_valid_sched_action updateReply_valid_objs')+
                                apply (frule valid_objs_valid_tcbs)
                                apply (frule pred_tcb_at_tcb_at)
                                apply (frule (1) valid_sched_scheduler_act_not_better[OF _ st_tcb_weakenE])

proof/refine/RISCV64/KHeap_R.thy

@@ -1475,7 +1475,8 @@ lemma reply_at'_cross:
               split: Structures_A.kernel_object.split_asm if_split_asm
                      arch_kernel_obj.split_asm)
 
-lemma set_reply_corres: (* for reply update that doesn't touch the reply stack *)
+(* for reply update that doesn't touch the reply stack *)
+lemma set_reply_corres:
   "reply_relation ae ae' \<Longrightarrow>
   corres dc \<top>
             (obj_at' (\<lambda>ko. replyPrev_same ae' ko) ptr)
@@ -4644,7 +4645,8 @@ lemma no_fail_updateReply [wp]:
   "no_fail (reply_at' rp) (updateReply rp f)"
   unfolding updateReply_def by wpsimp
 
-lemma setReply_replyPrev_same_corres: (* for reply update that doesn't touch the reply stack *)
+(* for reply update that doesn't touch the reply stack *)
+lemma setReply_replyPrev_same_corres:
   assumes R': "reply_relation reply reply'"
   shows
     "corres dc
@@ -4773,11 +4775,7 @@ lemma updateReply_corres_Q:
               simp?)
       apply (clarsimp simp: obj_at_def)
      apply fastforce
-    apply wpsimp
-    apply (clarsimp simp: obj_at'_def)
-   apply wpsimp
-  apply wpsimp
-  apply (clarsimp simp: obj_at'_def)
+    apply (wpsimp | normalise_obj_at' | erule obj_at'_weakenE)+
   done
 
 lemma updateReply_corres: