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

autocorres-crefine: update another corres_UL that snuck in before rebasing.

This commit is contained in:
Japheth Lim 2016-01-28 14:29:35 +11:00
parent 3ede1a33b0
commit b9c23eaa74
1 changed files with 2 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
proof/refine/CSpace1_R.thy
View File

@ -503,9 +503,9 @@ lemma cap_relation_Null2 [simp]:
lemmas cnode_cap_case_if = cap_case_CNodeCap
lemma corres_stateAssert_assume_stronger:
"\<lbrakk> corres_underlying sr nf r P Q f (g ());
"\<lbrakk> corres_underlying sr nf nf' r P Q f (g ());
\<And>s s'. \<lbrakk> (s, s') \<in> sr; P s; Q s' \<rbrakk> \<Longrightarrow> P' s' \<rbrakk> \<Longrightarrow>
corres_underlying sr nf r P Q f (stateAssert P' [] >>= g)"
corres_underlying sr nf nf' r P Q f (stateAssert P' [] >>= g)"
apply (clarsimp simp: bind_assoc stateAssert_def)
apply (rule corres_symb_exec_r [OF _ get_sp])
apply (rule_tac F="P' x" in corres_req)