rt riscv refine: add sym_refs_asrt_def to global [simp] set

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

proof/refine/RISCV64/Detype_R.thy

@@ -1859,7 +1859,6 @@ lemma deleteObjects_sym_refs':
    apply clarsimp
    apply (frule(2) delete_locale.intro, simp_all)[1]
     apply (simp add: valid_idle'_asrt_def)
-   apply (simp add: sym_refs_asrt_def)
    apply (rule subst[rotated, where P="\<lambda>s. sym_refs (state_refs_of' s)"],
           erule delete_locale.delete_sym_refs')
    apply (simp add: field_simps mask_def)

proof/refine/RISCV64/Finalise_R.thy

@@ -4110,30 +4110,26 @@ lemma schedContextUnbindNtfn_corres:
   apply (rule corres_cross[where Q' = "sc_at' sc", OF sc_at'_cross_rel])
    apply (simp add: invs_psp_aligned invs_distinct)
   apply add_sym_refs
-  apply (rule corres_stateAssert_implied[where P'=\<top>, simplified])
-   apply (simp add: get_sc_obj_ref_def)
-   apply (rule corres_guard_imp)
-     apply (rule corres_split[OF get_sc_corres])
-       apply (rule corres_option_split)
-         apply (simp add: sc_relation_def)
-        apply (rule corres_return_trivial)
-       apply (simp add: update_sk_obj_ref_def bind_assoc)
-       apply (rule corres_split[OF getNotification_corres])
-         apply (rule corres_split[OF setNotification_corres])
-            apply (clarsimp simp: ntfn_relation_def split: Structures_A.ntfn.splits)
-           apply (rule_tac f'="scNtfn_update (\<lambda>_. None)"
-                    in update_sc_no_reply_stack_update_ko_at'_corres)
-              apply (clarsimp simp: sc_relation_def objBits_def objBitsKO_def refillSize_def)+
-          apply wpsimp+
-    apply (frule invs_valid_objs)
-    apply (frule (1) valid_objs_ko_at)
-    apply (clarsimp simp: invs_psp_aligned valid_obj_def valid_sched_context_def
-                   split: option.splits)
-   apply (clarsimp split: option.splits)
-   apply (frule (1) scNtfn_sym_refsD[OF ko_at_obj_at', simplified])
-     apply clarsimp+
-  apply normalise_obj_at'
-  apply (clarsimp simp: sym_refs_asrt_def)
+  apply (rule corres_stateAssert_implied[where P'=\<top>, simplified, rotated], simp)
+  apply (simp add: get_sc_obj_ref_def)
+  apply (rule corres_guard_imp)
+    apply (rule corres_split[OF get_sc_corres])
+      apply (rule corres_option_split)
+        apply (simp add: sc_relation_def)
+       apply (rule corres_return_trivial)
+      apply (simp add: update_sk_obj_ref_def bind_assoc)
+      apply (rule corres_split[OF getNotification_corres])
+        apply (rule corres_split[OF setNotification_corres])
+           apply (clarsimp simp: ntfn_relation_def split: Structures_A.ntfn.splits)
+          apply (rule_tac f'="scNtfn_update (\<lambda>_. None)"
+                   in update_sc_no_reply_stack_update_ko_at'_corres)
+             apply (clarsimp simp: sc_relation_def objBits_def objBitsKO_def refillSize_def)+
+         apply wpsimp+
+   apply (frule invs_valid_objs)
+   apply (frule (1) valid_objs_ko_at)
+   apply (clarsimp simp: invs_psp_aligned valid_obj_def valid_sched_context_def
+                  split: option.splits)
+  apply (fastforce dest: scNtfn_sym_refsD[OF ko_at_obj_at', simplified] split: option.splits)
   done
 
 lemma sched_context_maybe_unbind_ntfn_corres:
@@ -4178,7 +4174,6 @@ lemma sched_context_maybe_unbind_ntfn_corres:
        apply (frule (1) ntfnSc_sym_refsD[OF ko_at_obj_at', simplified])
         apply clarsimp+
        apply normalise_obj_at'
-      apply (clarsimp simp: sym_refs_asrt_def)
      apply (wpsimp wp: get_simple_ko_wp getNotification_wp split: option.splits)+
   done
 

proof/refine/RISCV64/Invariants_H.thy

@@ -374,6 +374,8 @@ definition state_refs_of' :: "kernel_state \<Rightarrow> obj_ref \<Rightarrow> r
 defs sym_refs_asrt_def:
   "sym_refs_asrt \<equiv> \<lambda>s. sym_refs (state_refs_of' s)"
 
+declare sym_refs_asrt_def[simp]
+
 definition live_sc' :: "sched_context \<Rightarrow> bool" where
   "live_sc' sc \<equiv> bound (scTCB sc) \<and> scTCB sc \<noteq> Some idle_thread_ptr
                   \<or> bound (scYieldFrom sc) \<or> bound (scNtfn sc) \<or> scReply sc \<noteq> None"

proof/refine/RISCV64/Ipc_R.thy

@@ -4309,7 +4309,6 @@ lemma sendSignal_corres:
        defer
        apply (wp get_simple_ko_ko_at get_ntfn_ko')+
      apply (simp add: invs_valid_objs invs_valid_objs')+
-   apply (clarsimp simp: sym_refs_asrt_def)
   apply add_sym_refs
   apply (case_tac "ntfn_obj ntfn"; simp)
     \<comment> \<open>IdleNtfn\<close>
@@ -5181,14 +5180,13 @@ lemma maybeReturnSc_invs':
   apply (rule_tac x=tcb in exI)
   apply (clarsimp simp: invs'_def inQ_def comp_def eq_commute[where a="Some _"])
   apply (intro conjI impI allI; clarsimp?)
-      apply (clarsimp simp: untyped_ranges_zero_inv_def cteCaps_of_def comp_def)
-     apply (clarsimp simp: valid_idle'_def obj_at'_def sym_refs_asrt_def)
-     apply (drule_tac ko="tcb" and p=tptr in sym_refs_ko_atD'[rotated])
-      apply (fastforce simp: obj_at'_def)
-     apply (clarsimp simp: ko_wp_at'_def refs_of_rev')
-     apply (fastforce elim: if_live_then_nonz_capE' simp: ko_wp_at'_def live_sc'_def)
-    apply (fastforce simp: valid_pspace'_def valid_obj'_def valid_sched_context'_def refillSize_def)
-   apply (fastforce simp: valid_obj'_def valid_sched_context_size'_def objBits_def objBitsKO_def)
+     apply (clarsimp simp: untyped_ranges_zero_inv_def cteCaps_of_def comp_def)
+    apply (drule_tac ko="tcb" and p=tptr in sym_refs_ko_atD'[rotated])
+     apply (fastforce simp: obj_at'_def)
+    apply (clarsimp simp: ko_wp_at'_def refs_of_rev')
+    apply (fastforce elim: if_live_then_nonz_capE' simp: ko_wp_at'_def live_sc'_def)
+   apply (fastforce simp: valid_pspace'_def valid_obj'_def valid_sched_context'_def refillSize_def)
+  apply (fastforce simp: valid_obj'_def valid_sched_context_size'_def objBits_def objBitsKO_def)
   done
 
 crunch doIPCTransfer

proof/refine/RISCV64/Syscall_R.thy

@@ -443,9 +443,7 @@ lemma performInvocation_corres:
                   apply (rule corres_returnOkTT)
                   apply simp
                  apply wpsimp+
-             apply (clarsimp simp: sym_refs_asrt_def)
 
-            apply (clarsimp simp: liftE_bindE)
             apply (rule corres_guard_imp)
               apply (rule corres_split[OF getCurThread_corres])
                 apply simp