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

autocorres: solve a bad ":000" var name from L2Opt 

Not sure if this breaks the property in the rule's comment, but
we'll probably find out if it does.
This commit is contained in:
Japheth Lim 2019-06-13 16:06:41 +10:00
parent ec74efcb9e
commit fa0b62380a
1 changed files with 1 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
tools/autocorres/L2Opt.thy
View File

@ -121,7 +121,7 @@ lemma monad_equiv_guard:
* variables being expanded inside of guard statements. *)
lemma monad_equiv_guard' [L2flow]:
"\<lbrakk> \<And>s. simp_expr True (G s) (G' s) \<rbrakk> \<Longrightarrow>
monad_equiv P (L2_guard G) (L2_guard G') (\<lambda>r s. P s \<and> G' s \<and> r = ()) (\<lambda>_ _. False)"
monad_equiv P (L2_guard (\<lambda>s. G s)) (L2_guard (\<lambda>s. G' s)) (\<lambda>r s. P s \<and> G' s \<and> r = ()) (\<lambda>_ _. False)"
apply (rule monad_equiv_guard)
apply (rule simp_expr_weaken)
apply assumption