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

lib/wp: Bundle to restore classic combinators. 

The previous combinator change is desirable, but some proofs are too
difficult to fix. This bundle restores the classic behaviour.
This commit is contained in:
Thomas Sewell 2018-01-15 16:46:02 +11:00
parent 652cbb966e
commit be45b71fd7
1 changed files with 13 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

13
lib/Monad_WP/NonDetMonadVCG.thy
View File

@ -1383,6 +1383,16 @@ lemmas hoare_wp_state_combsE =
hoare_vcg_E_elim[OF valid_validE_E]
hoare_vcg_E_conj[OF valid_validE_E]
lemmas hoare_classic_wp_combs
= hoare_post_comb_imp_conj hoare_vcg_precond_imp hoare_wp_combs
lemmas hoare_classic_wp_combsE
= hoare_vcg_precond_impE hoare_vcg_precond_impE_R hoare_wp_combsE
lemmas hoare_classic_wp_state_combsE
= hoare_vcg_precond_impE[OF valid_validE]
hoare_vcg_precond_impE_R[OF valid_validE_R] hoare_wp_state_combsE
lemmas all_classic_wp_combs =
hoare_classic_wp_state_combsE hoare_classic_wp_combsE hoare_classic_wp_combs
lemmas hoare_wp_splits [wp_split] =
hoare_seq_ext hoare_vcg_seqE handleE'_wp handleE_wp
validE_validE_R [OF hoare_vcg_seqE [OF validE_R_validE]]
@ -1489,6 +1499,9 @@ declare no_fail_pre [wp_pre]
bundle no_pre = hoare_pre [wp_pre del] no_fail_pre [wp_pre del]
bundle classic_wp_pre = hoare_pre [wp_pre del] no_fail_pre [wp_pre del]
all_classic_wp_combs[wp_comb del] all_classic_wp_combs[wp_comb]
text {* Miscellaneous lemmas on hoare triples *}
lemma hoare_vcg_mp: