squash arm access: PR suggestion

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

proof/access-control/Access.thy

@@ -246,7 +246,6 @@ unauthorised subjects (see integrity_ready_queues).
 
 \<close>
 
-\<comment> \<open>FIXME: should this be etcbs_of instead of kheap?\<close>
 inductive_set domains_of_state_aux for etcbs_of where
   domtcbs:
     "\<lbrakk> etcbs_of ptr = Some tcb; d = etcb_domain tcb \<rbrakk> \<Longrightarrow> (ptr, d) \<in> domains_of_state_aux etcbs_of"

proof/access-control/Retype_AC.thy

@@ -422,14 +422,11 @@ context retype_region_proofs' begin
 lemma tcb_domain_map_wellformed:
   "\<lbrakk>tcb_domain_map_wellformed aag s; pas_cur_domain aag s; \<forall>x\<in> set (retype_addrs ptr ty n us). is_subject aag x\<rbrakk>
    \<Longrightarrow> tcb_domain_map_wellformed aag s'"
-  unfolding s'_def ps_def
-  apply (clarsimp simp: tcb_domain_map_wellformed_aux_def)
-  apply (erule domains_of_state_aux.cases)
-  apply (clarsimp simp: etcbs_of'_def split: if_split_asm kernel_object.splits)
-   apply (clarsimp simp: default_object_def default_tcb_def tyunt split: apiobject_type.splits)
-   defer
-  apply (force intro: domtcbs)
-  done
+  by (force simp: s'_def ps_def tcb_domain_map_wellformed_aux_def etcbs_of'_def
+                  default_object_def default_tcb_def tyunt
+           split: if_split_asm kernel_object.splits apiobject_type.splits
+            elim: domains_of_state_aux.cases
+           intro: domtcbs)
 
 (* FIXME MOVE next to cte_at_pres *)
 lemma cte_wp_at_pres: