spec proof: resolve_address_bits'.simps[simp del]

Remove resolve_address_bits'.simps from the simp set at the definition
site, instead of in the middle of the proofs.

Signed-off-by: Corey Lewis <Corey.Lewis@data61.csiro.au>

proof/access-control/CNode_AC.thy

@@ -141,8 +141,6 @@ where
   | CancelBadgedSendsCall cap \<Rightarrow> pas_cap_cur_auth aag cap
   | RevokeCall ptr \<Rightarrow> is_subject aag (fst ptr))"
 
-declare resolve_address_bits'.simps[simp del]
-
 lemma resolve_address_bits_authorised_aux:
   "s \<turnstile> \<lbrace>pas_refined aag and K (is_cnode_cap (fst (cap, cref))
                                \<longrightarrow> (\<forall>x \<in> obj_refs (fst (cap, cref)). is_subject aag x))\<rbrace>

proof/bisim/Separation.thy

@@ -89,7 +89,7 @@ lemma separate_cnode_cap_rab:
                                                                      (throwError (GuardMismatch (length cref) guard))
                                        | _ \<Rightarrow> throwError InvalidRoot)"
   unfolding separate_cnode_cap_def resolve_address_bits_def
-  by (auto simp: word_bits_def split: cap.split_asm)
+  by (auto simp: word_bits_def resolve_address_bits'.simps split: cap.split_asm)
 
 definition
   "separate_state s \<equiv> \<forall>p. tcb_at p s \<longrightarrow> separate_tcb p (caps_of_state s)"

proof/bisim/Syscall_S.thy

@@ -97,6 +97,7 @@ lemma bisim_rab:
                                 | _ \<Rightarrow> throwError undefined
                         odE)
                       (resolve_address_bits (cap, cref))"
+  using resolve_address_bits'.simps[simp]
   unfolding resolve_address_bits_def
   apply (cases "length cref < word_bits")
    apply (auto intro!: bisim_underlyingI

proof/refine/ARM/CSpace1_R.thy

@@ -526,8 +526,6 @@ lemma cap_table_at_gsCNodes:
   apply blast
   done
 
-declare resolve_address_bits'.simps[simp del]
-
 lemma getSlotCap_valid:
   "\<lbrace>\<lambda>s. valid_objs' s \<and> (cte_wp_at' (\<lambda>_. True) p s \<longrightarrow> (\<forall>cap. valid_cap' cap s \<longrightarrow> Q cap s))\<rbrace>
   getSlotCap p \<lbrace>Q\<rbrace>"

proof/refine/ARM_HYP/CSpace1_R.thy

@@ -530,8 +530,6 @@ lemma cap_table_at_gsCNodes:
   apply blast
   done
 
-declare resolve_address_bits'.simps[simp del]
-
 lemma getSlotCap_valid:
   "\<lbrace>\<lambda>s. valid_objs' s \<and> (cte_wp_at' (\<lambda>_. True) p s \<longrightarrow> (\<forall>cap. valid_cap' cap s \<longrightarrow> Q cap s))\<rbrace>
   getSlotCap p \<lbrace>Q\<rbrace>"

proof/refine/RISCV64/CSpace1_R.thy

@@ -523,8 +523,6 @@ lemma cap_table_at_gsCNodes:
   apply blast
   done
 
-declare resolve_address_bits'.simps[simp del]
-
 lemma rab_corres':
   "\<lbrakk> cap_relation (fst a) c'; drop (64-bits) (to_bl cref') = snd a;
      bits = length (snd a) \<rbrakk> \<Longrightarrow>

proof/refine/X64/CSpace1_R.thy

@@ -525,8 +525,6 @@ lemma cap_table_at_gsCNodes:
   apply blast
   done
 
-declare resolve_address_bits'.simps[simp del]
-
 lemma rab_corres':
   "\<lbrakk> cap_relation (fst a) c'; drop (64-bits) (to_bl cref') = snd a;
      bits = length (snd a) \<rbrakk> \<Longrightarrow>

spec/abstract/CSpace_A.thy

@@ -200,6 +200,8 @@ termination
   apply (auto simp: whenE_def returnOk_def return_def rab_termination)
   done
 
+declare resolve_address_bits'.simps[simp del]
+
 definition resolve_address_bits where
 "resolve_address_bits \<equiv> resolve_address_bits' TYPE('z::state_ext)"