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

lib: add ovalid_post_taut 

Signed-off-by: Michael McInerney <michael.mcinerney@proofcraft.systems>
This commit is contained in:
Michael McInerney 2024-01-09 19:47:51 +10:30 committed by Achim D. Brucker
parent be7ac0ee39
commit 92ad82ff79
1 changed files with 4 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
lib/Monads/reader_option/Reader_Option_VCG.thy
View File

@ -59,6 +59,10 @@ lemmas owhile_add_inv = owhile_inv_def[symmetric]
(* WP rules for ovalid. *)
lemma ovalid_post_taut[wp]:
"\<lblot>P\<rblot> f \<lblot>\<top>\<top>\<rblot>"
by (simp add: ovalid_def)
lemma ovalid_inv[wp]:
"ovalid P f (\<lambda>_. P)"
by (simp add: ovalid_def)