aarch64 refine: move lemmas internally

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>

proof/refine/AARCH64/Detype_R.thy

@@ -1697,12 +1697,6 @@ lemma valid_untyped_no_overlap:
    apply (fastforce simp: mask_def add_diff_eq)+
   done
 
-(* FIXME AARCH64: move to InvariantUpdates_H *)
-lemma pspace_no_overlap'_ksArchState_update[simp]:
-  "pspace_no_overlap' p n (ksArchState_update f s) =
-   pspace_no_overlap' p n s"
-  by (simp add: pspace_no_overlap'_def)
-
 lemma deleteObject_no_overlap[wp]:
   "\<lbrace>valid_cap' (UntypedCap d ptr bits idx) and valid_pspace'\<rbrace>
      deleteObjects ptr bits

proof/refine/AARCH64/InvariantUpdates_H.thy

@@ -74,6 +74,11 @@ lemma pspace_no_overlap'_ksSchedulerAction[simp]:
    pspace_no_overlap' a b s"
   by (simp add: pspace_no_overlap'_def)
 
+lemma pspace_no_overlap'_ksArchState_update[simp]:
+  "pspace_no_overlap' p n (ksArchState_update f s) =
+   pspace_no_overlap' p n s"
+  by (simp add: pspace_no_overlap'_def)
+
 lemma ksReadyQueues_update_id[simp]:
   "ksReadyQueues_update id s = s"
   by simp

proof/refine/AARCH64/TcbAcc_R.thy

@@ -1356,6 +1356,10 @@ lemma threadSet_valid_objs':
   apply (clarsimp elim!: obj_at'_weakenE)
   done
 
+lemma atcbVCPUPtr_atcbContextSet_id[simp]:
+  "atcbVCPUPtr (atcbContextSet f (tcbArch tcb)) = atcbVCPUPtr (tcbArch tcb)"
+  by (simp add: atcbContextSet_def)
+
 lemma asUser_corres':
   assumes y: "corres_underlying Id False True r \<top> \<top> f g"
   shows      "corres r (tcb_at t and pspace_aligned and pspace_distinct) \<top>
@@ -1463,11 +1467,6 @@ lemma asUser_typ_at' [wp]:
 
 lemmas asUser_typ_ats[wp] = typ_at_lifts [OF asUser_typ_at']
 
-(* FIXME AARCH64: move *)
-lemma atcbVCPUPtr_atcbContextSet_id[simp]:
-  "atcbVCPUPtr (atcbContextSet f (tcbArch tcb)) = atcbVCPUPtr (tcbArch tcb)"
-  by (simp add: atcbContextSet_def)
-
 lemma asUser_invs[wp]:
   "\<lbrace>invs' and tcb_at' t\<rbrace> asUser t m \<lbrace>\<lambda>rv. invs'\<rbrace>"
   apply (simp add: asUser_def split_def)