adbrucker
/
lh-l4v
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

arm orphanage: Isabelle2020 update 

Signed-off-by: Gerwin Klein <gerwin.klein@data61.csiro.au>
This commit is contained in:
Gerwin Klein 2020-03-29 12:34:37 +08:00 committed by Gerwin Klein
parent bbacd7079f
commit 6719ec050b
1 changed files with 2 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
proof/refine/ARM/orphanage/Orphanage.thy
View File

@ -1090,6 +1090,7 @@ proof -
show ?thesis
unfolding schedule_def
supply if_weak_cong[cong]
apply (wp, wpc)
\<comment> \<open>action = ResumeCurrentThread\<close>
apply (wp)[1]
@ -1965,6 +1966,7 @@ lemma copyreg_no_orphans:
invokeTCB (tcbinvocation.CopyRegisters dest src susp resume frames ints arch)
\<lbrace> \<lambda>rv s. no_orphans s \<rbrace>"
unfolding invokeTCB_def performTransfer_def postModifyRegisters_def
supply if_weak_cong[cong]
apply simp
apply (wp hoare_vcg_if_lift static_imp_wp)
apply (wp hoare_vcg_imp_lift' mapM_x_wp' asUser_no_orphans