lib: add ifM_to_top_of_bind
Signed-off-by: Michael McInerney <michael.mcinerney@proofcraft.systems>
This commit is contained in:
parent
3c9065f0da
commit
0cdce52f0b
|
@ -543,4 +543,8 @@ lemma notM_corres:
|
||||||
apply wpsimp+
|
apply wpsimp+
|
||||||
done
|
done
|
||||||
|
|
||||||
|
lemma ifM_to_top_of_bind:
|
||||||
|
"((ifM test true false) >>= z) = ifM test (true >>= z) (false >>= z)"
|
||||||
|
by (force simp: ifM_def bind_def split: if_splits)
|
||||||
|
|
||||||
end
|
end
|
||||||
|
|
Loading…
Reference in New Issue