diff --git a/proof/crefine/AARCH64/Fastpath_C.thy b/proof/crefine/AARCH64/Fastpath_C.thy index 5495d4a19e..116b590486 100644 --- a/proof/crefine/AARCH64/Fastpath_C.thy +++ b/proof/crefine/AARCH64/Fastpath_C.thy @@ -54,7 +54,7 @@ lemma setCTE_tcbContext: apply (rule setObject_cte_obj_at_tcb', simp_all) done -lemma seThreadState_tcbContext: +lemma setThreadState_tcbContext: "\obj_at' (\tcb. P ((atcbContextGet o tcbArch) tcb)) t\ setThreadState a b \\_. obj_at' (\tcb. P ((atcbContextGet o tcbArch) tcb)) t\" @@ -73,7 +73,7 @@ lemma setBoundNotification_tcbContext: declare comp_apply [simp del] crunch tcbContext[wp]: deleteCallerCap "obj_at' (\tcb. P ((atcbContextGet o tcbArch) tcb)) t" (wp: setEndpoint_obj_at_tcb' setBoundNotification_tcbContext - setNotification_tcb crunch_wps seThreadState_tcbContext + setNotification_tcb crunch_wps setThreadState_tcbContext simp: crunch_simps unless_def) declare comp_apply [simp] diff --git a/proof/crefine/AARCH64/Fastpath_Equiv.thy b/proof/crefine/AARCH64/Fastpath_Equiv.thy index 0cb9028902..b005190e93 100644 --- a/proof/crefine/AARCH64/Fastpath_Equiv.thy +++ b/proof/crefine/AARCH64/Fastpath_Equiv.thy @@ -49,7 +49,7 @@ lemma setCTE_tcbContext: context begin interpretation Arch . (*FIXME: arch_split*) -lemma seThreadState_tcbContext: +lemma setThreadState_tcbContext: "\obj_at' (\tcb. P ((atcbContextGet o tcbArch) tcb)) t\ setThreadState a b \\_. obj_at' (\tcb. P ((atcbContextGet o tcbArch) tcb)) t\" @@ -68,7 +68,7 @@ lemma setBoundNotification_tcbContext: declare comp_apply [simp del] crunch tcbContext[wp]: deleteCallerCap "obj_at' (\tcb. P ((atcbContextGet o tcbArch) tcb)) t" (wp: setEndpoint_obj_at_tcb' setBoundNotification_tcbContext - setNotification_tcb crunch_wps seThreadState_tcbContext + setNotification_tcb crunch_wps setThreadState_tcbContext simp: crunch_simps unless_def) declare comp_apply [simp] @@ -1697,7 +1697,7 @@ lemma fastpath_callKernel_SysReplyRecv_corres: fastpathBestSwitchCandidate_lift[where f="threadSet f t" for f t] | wps)+)[3] apply (simp cong: rev_conj_cong) - apply (wpsimp wp: seThreadState_tcbContext[simplified comp_apply] + apply (wpsimp wp: setThreadState_tcbContext[simplified comp_apply] setThreadState_oa_queued user_getreg_rv setThreadState_no_sch_change setThreadState_obj_at_unchanged sts_st_tcb_at'_cases sts_bound_tcb_at' diff --git a/proof/crefine/ARM/Fastpath_C.thy b/proof/crefine/ARM/Fastpath_C.thy index 09be1b557b..cd2f746a82 100644 --- a/proof/crefine/ARM/Fastpath_C.thy +++ b/proof/crefine/ARM/Fastpath_C.thy @@ -54,7 +54,7 @@ lemma setCTE_tcbContext: apply (rule setObject_cte_obj_at_tcb', simp_all) done -lemma seThreadState_tcbContext: +lemma setThreadState_tcbContext: "\obj_at' (\tcb. P ((atcbContextGet o tcbArch) tcb)) t\ setThreadState a b \\_. obj_at' (\tcb. P ((atcbContextGet o tcbArch) tcb)) t\" @@ -73,7 +73,7 @@ lemma setBoundNotification_tcbContext: declare comp_apply [simp del] crunch tcbContext[wp]: deleteCallerCap "obj_at' (\tcb. P ((atcbContextGet o tcbArch) tcb)) t" (wp: setEndpoint_obj_at_tcb' setBoundNotification_tcbContext - setNotification_tcb crunch_wps seThreadState_tcbContext + setNotification_tcb crunch_wps setThreadState_tcbContext simp: crunch_simps unless_def) declare comp_apply [simp] diff --git a/proof/crefine/ARM/Fastpath_Equiv.thy b/proof/crefine/ARM/Fastpath_Equiv.thy index e39857801f..e4fedded83 100644 --- a/proof/crefine/ARM/Fastpath_Equiv.thy +++ b/proof/crefine/ARM/Fastpath_Equiv.thy @@ -49,7 +49,7 @@ lemma setCTE_tcbContext: context begin interpretation Arch . (*FIXME: arch_split*) -lemma seThreadState_tcbContext: +lemma setThreadState_tcbContext: "\obj_at' (\tcb. P ((atcbContextGet o tcbArch) tcb)) t\ setThreadState a b \\_. obj_at' (\tcb. P ((atcbContextGet o tcbArch) tcb)) t\" @@ -68,7 +68,7 @@ lemma setBoundNotification_tcbContext: declare comp_apply [simp del] crunch tcbContext[wp]: deleteCallerCap "obj_at' (\tcb. P ((atcbContextGet o tcbArch) tcb)) t" (wp: setEndpoint_obj_at_tcb' setBoundNotification_tcbContext - setNotification_tcb crunch_wps seThreadState_tcbContext + setNotification_tcb crunch_wps setThreadState_tcbContext simp: crunch_simps unless_def) declare comp_apply [simp] @@ -1558,7 +1558,7 @@ lemma fastpath_callKernel_SysReplyRecv_corres: fastpathBestSwitchCandidate_lift[where f="threadSet f t" for f t] | wps)+)[3] apply (simp cong: rev_conj_cong) - apply (wpsimp wp: seThreadState_tcbContext[simplified comp_apply] + apply (wpsimp wp: setThreadState_tcbContext[simplified comp_apply] setThreadState_oa_queued user_getreg_rv setThreadState_no_sch_change setThreadState_obj_at_unchanged sts_st_tcb_at'_cases sts_bound_tcb_at' diff --git a/proof/crefine/ARM_HYP/Fastpath_C.thy b/proof/crefine/ARM_HYP/Fastpath_C.thy index 3660f4cc75..117979ae1a 100644 --- a/proof/crefine/ARM_HYP/Fastpath_C.thy +++ b/proof/crefine/ARM_HYP/Fastpath_C.thy @@ -54,7 +54,7 @@ lemma setCTE_tcbContext: apply (rule setObject_cte_obj_at_tcb', simp_all) done -lemma seThreadState_tcbContext: +lemma setThreadState_tcbContext: "\obj_at' (\tcb. P ((atcbContextGet o tcbArch) tcb)) t\ setThreadState a b \\_. obj_at' (\tcb. P ((atcbContextGet o tcbArch) tcb)) t\" @@ -73,7 +73,7 @@ lemma setBoundNotification_tcbContext: declare comp_apply [simp del] crunch tcbContext[wp]: deleteCallerCap "obj_at' (\tcb. P ((atcbContextGet o tcbArch) tcb)) t" (wp: setEndpoint_obj_at_tcb' setBoundNotification_tcbContext - setNotification_tcb crunch_wps seThreadState_tcbContext + setNotification_tcb crunch_wps setThreadState_tcbContext simp: crunch_simps unless_def) declare comp_apply [simp] diff --git a/proof/crefine/ARM_HYP/Fastpath_Equiv.thy b/proof/crefine/ARM_HYP/Fastpath_Equiv.thy index 2ade2f9356..7bfd4520e8 100644 --- a/proof/crefine/ARM_HYP/Fastpath_Equiv.thy +++ b/proof/crefine/ARM_HYP/Fastpath_Equiv.thy @@ -49,7 +49,7 @@ lemma setCTE_tcbContext: context begin interpretation Arch . (*FIXME: arch_split*) -lemma seThreadState_tcbContext: +lemma setThreadState_tcbContext: "\obj_at' (\tcb. P ((atcbContextGet o tcbArch) tcb)) t\ setThreadState a b \\_. obj_at' (\tcb. P ((atcbContextGet o tcbArch) tcb)) t\" @@ -68,7 +68,7 @@ lemma setBoundNotification_tcbContext: declare comp_apply [simp del] crunch tcbContext[wp]: deleteCallerCap "obj_at' (\tcb. P ((atcbContextGet o tcbArch) tcb)) t" (wp: setEndpoint_obj_at_tcb' setBoundNotification_tcbContext - setNotification_tcb crunch_wps seThreadState_tcbContext + setNotification_tcb crunch_wps setThreadState_tcbContext simp: crunch_simps unless_def) declare comp_apply [simp] @@ -1561,7 +1561,7 @@ lemma fastpath_callKernel_SysReplyRecv_corres: fastpathBestSwitchCandidate_lift[where f="threadSet f t" for f t] | wps)+)[3] apply (simp cong: rev_conj_cong) - apply (wpsimp wp: seThreadState_tcbContext[simplified comp_apply] + apply (wpsimp wp: setThreadState_tcbContext[simplified comp_apply] setThreadState_oa_queued user_getreg_rv setThreadState_no_sch_change setThreadState_obj_at_unchanged sts_st_tcb_at'_cases sts_bound_tcb_at'