address more PR comments squash into main commit

Signed-off-by: Michael McInerney <[email protected]>

proof/crefine/RISCV64/IpcCancel_C.thy

@@ -2553,8 +2553,8 @@ lemma ep_ptr_set_queue_spec:
   oops
 
 lemma valid_ep_blockedD:
-  "\<lbrakk> valid_ep' ep s; (isSendEP ep \<or> isRecvEP ep) \<rbrakk>
-   \<Longrightarrow> (epQueue ep) \<noteq> [] \<and> (\<forall>t\<in>set (epQueue ep). tcb_at' t s)"
+  "\<lbrakk> valid_ep' ep s; isSendEP ep \<or> isRecvEP ep \<rbrakk>
+   \<Longrightarrow> epQueue ep \<noteq> [] \<and> (\<forall>t\<in>set (epQueue ep). tcb_at' t s)"
   unfolding valid_ep'_def isSendEP_def isRecvEP_def
   by (clarsimp split: endpoint.splits)
 

proof/crefine/RISCV64/SR_lemmas_C.thy

@@ -1212,7 +1212,7 @@ lemma ntfn_blocked_in_queueD:
 (* MOVE *)
 lemma valid_ntfn_isWaitingNtfnD:
   "\<lbrakk> valid_ntfn' ntfn s; isWaitingNtfn (ntfnObj ntfn) \<rbrakk>
-  \<Longrightarrow> (ntfnQueue (ntfnObj ntfn)) \<noteq> [] \<and> (\<forall>t\<in>set (ntfnQueue (ntfnObj ntfn)). tcb_at' t s)"
+  \<Longrightarrow> ntfnQueue (ntfnObj ntfn) \<noteq> [] \<and> (\<forall>t\<in>set (ntfnQueue (ntfnObj ntfn)). tcb_at' t s)"
   unfolding valid_ntfn'_def isWaitingNtfn_def
   by (clarsimp split: Structures_H.notification.splits ntfn.splits)
 

proof/invariant-abstract/IpcDet_AI.thy

@@ -93,34 +93,6 @@ lemma sfi_tcb_at [wp]:
     \<lbrace>\<lambda>_. tcb_at t\<rbrace>"
   by (wpsimp simp: send_fault_ipc_def)
 
-(* FIXME RT: move these wp and sp rules for mapM? *)
-lemma mapM_gets_the_wp:
-  "\<lbrace>\<lambda>s. \<forall>vs. map (\<lambda>t. f t s) ts = map Some vs \<longrightarrow> P vs s\<rbrace>
-   mapM (gets_the \<circ> f) ts
-   \<lbrace>P\<rbrace>"
-unfolding comp_def
-proof (induct ts arbitrary: P)
-  case Nil thus ?case by (wpsimp simp: mapM_Nil)
-next
-  case (Cons x xs) show ?case by (wpsimp simp: mapM_Cons wp: Cons)
-qed
-
-lemma mapM_gets_the_wp':
-  "\<lbrace>\<lambda>s. \<forall>vs. (\<forall>i < length vs. f (ts ! i) s = Some (vs ! i)) \<longrightarrow> P vs s\<rbrace>
-   mapM (gets_the \<circ> f) ts
-   \<lbrace>P\<rbrace>"
-  apply (wpsimp wp: mapM_gets_the_wp)
-  by (simp add: map_equality_iff)
-
-lemma mapM_gets_the_sp:
-  "\<lbrace>P\<rbrace> mapM (gets_the \<circ> f) ts \<lbrace>\<lambda>rv s. P s \<and> map (\<lambda>t. f t s) ts = map Some rv\<rbrace>"
-  by (wpsimp wp: mapM_gets_the_wp simp: comp_def)
-
-lemma mapM_gets_the_sp':
-  "\<lbrace>P\<rbrace> mapM (gets_the \<circ> f) ts \<lbrace>\<lambda>rv s. P s \<and> (\<forall>i < length rv. f (ts ! i) s = Some (rv ! i))\<rbrace>"
-  apply (wpsimp wp: mapM_gets_the_wp simp: comp_def)
-  by (simp add: map_equality_iff)
-
 lemma distinct_map_fst_filter_zip:
   "distinct list \<Longrightarrow> distinct (map fst (filter f (zip list zp)))"
   apply (induct list rule: length_induct)