rt crefine: respond to Gerwin's comments squash

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

proof/crefine/RISCV64/ADT_C.thy

@@ -1176,27 +1176,27 @@ lemma scRefills_unique:
   done
 
 lemma scSize_unique:
-  assumes "refill_buffer_relation (ksPSpace as) ch gs" "refill_buffer_relation (ksPSpace as') ch gs"
-      and "ksPSpace as p = Some (KOSchedContext sc)"
-      and "ksPSpace as' p = Some (KOSchedContext sc')"
+  assumes "refill_buffer_relation ah ch gs" "refill_buffer_relation ah' ch gs"
+      and "ah p = Some (KOSchedContext sc)"
+      and "ah' p = Some (KOSchedContext sc')"
   shows   "scSize sc = scSize sc'"
   apply (insert assms)
-  apply (frule refill_buffer_relation_size_eq[where ah="ksPSpace as"])
-  apply (frule refill_buffer_relation_size_eq[where ah="ksPSpace as'"])
+  apply (frule refill_buffer_relation_size_eq[where ah=ah])
+  apply (frule refill_buffer_relation_size_eq[where ah=ah'])
   apply (clarsimp simp: Let_def)
   apply (drule_tac x=p in spec)+
   by fastforce
 
 lemma
   assumes "pspace_aligned' as" "pspace_distinct' as" "valid_sched_context' asc as"
   shows tcb_at'_scTCB:
-    "bound (scTCB asc) \<longrightarrow> tcb_at' (the (scTCB asc)) as"
+    "\<forall>tcbPtr. scTCB asc = Some tcbPtr \<longrightarrow> tcb_at' tcbPtr as"
   and reply_at'_scReply:
-    "bound (scReply asc) \<longrightarrow> reply_at' (the (scReply asc)) as"
+    "\<forall>replyPtr. scReply asc = Some replyPtr \<longrightarrow> reply_at' replyPtr as"
   and ntfn_at'_scNtfn:
-    "bound (scNtfn asc) \<longrightarrow> ntfn_at' (the (scNtfn asc)) as"
+    "\<forall>ntfnPtr. scNtfn asc = Some ntfnPtr \<longrightarrow> ntfn_at' ntfnPtr as"
   and tcb_at'_scYieldFrom:
-    "scYieldFrom asc \<noteq> None \<longrightarrow> tcb_at' (the (scYieldFrom asc)) as"
+    "\<forall>tcbPtr. scYieldFrom asc = Some tcbPtr \<longrightarrow> tcb_at' tcbPtr as"
   using assms
   by (clarsimp simp: valid_sched_context'_def obj_at'_def)+
 
@@ -1249,7 +1249,7 @@ lemma cpspace_sched_context_relation_unique:
      apply force
     apply (force simp: obj_at'_def)
    apply force
-  apply (frule_tac p=p in scSize_unique[where as=as and as'=as'])
+  apply (frule_tac p=p in scSize_unique[where ah="ksPSpace as" and ah'="ksPSpace as'"])
      apply fastforce
     apply (force simp: obj_at'_def)
    apply (force simp: obj_at'_def)