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

lib: add ifME_liftE 

Signed-off-by: Michael McInerney <michael.mcinerney@proofcraft.systems>
This commit is contained in:
Michael McInerney 2023-03-09 20:33:39 +10:30 committed by michaelmcinerney
parent f4a9758d8b
commit adc7499aea
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/More_NonDetMonadVCG.thy
View File

@ -370,6 +370,10 @@ lemma ifM_throwError_returnOk:
validE_def bind_def
split: if_splits)
lemma ifME_liftE:
"ifME (liftE test) a b = ifM test a b"
by (simp add: ifME_def ifM_def liftE_bindE)
lemma gets_the_inv: "\<lbrace>P\<rbrace> gets_the V \<lbrace>\<lambda>rv. P\<rbrace>" by wpsimp
lemma select_f_inv: