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

lib: faster proof

This commit is contained in:
Gerwin Klein 2017-03-10 21:59:50 +11:00 committed by Miki Tanaka
parent 727b7f74e5
commit 3005f25eb9
1 changed files with 1 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
lib/Monad_WP/NonDetMonadVCG.thy
View File

@ -1631,7 +1631,7 @@ lemma hoare_drop_imp:
lemma hoare_drop_impE:
"\<lbrakk>\<lbrace>P\<rbrace> f \<lbrace>\<lambda>r. Q\<rbrace>, \<lbrace>E\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>\<lambda>r s. R r s \<longrightarrow> Q s\<rbrace>, \<lbrace>E\<rbrace>"
by (metis (lifting, mono_tags) hoare_post_impErr')
by (simp add: validE_weaken)
lemma hoare_drop_impE_R:
"\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>,- \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>\<lambda>r s. R r s \<longrightarrow> Q r s\<rbrace>, -"