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

lib/monads: move empty_fail_guard into NonDetMonadVCG 

So that it is available together with the other empty_fail lemmas.
Eventually, these should go into their own theory.

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
This commit is contained in:
Gerwin Klein 2023-01-23 18:36:22 +11:00
parent 238acb46bb
commit 0aa2914b84
No known key found for this signature in database
GPG Key ID: 20A847CE6AB7F5F3
2 changed files with 4 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

3
lib/Monad_Equations.thy
View File

@ -513,9 +513,6 @@ lemma bind_fail_propagates:
"empty_fail A \<Longrightarrow> A >>= (\<lambda>_. fail) = fail"
by (monad_eq simp: empty_fail_def) fastforce
lemma empty_fail_guard [simp]: "empty_fail (state_assert G)"
by (clarsimp simp: state_assert_def assert_def empty_fail_def get_def return_def bind_def)
lemma simple_bind_fail [simp]:
"(state_assert X >>= (\<lambda>_. fail)) = fail"
"(modify M >>= (\<lambda>_. fail)) = fail"

4
lib/Monad_WP/NonDetMonadVCG.thy
View File

@ -872,6 +872,10 @@ lemma empty_fail_select[simp]:
"empty_fail (select V) = (V \<noteq> {})"
by (clarsimp simp: select_def empty_fail_def)
lemma empty_fail_guard[simp]:
"empty_fail (state_assert G)"
by (clarsimp simp: state_assert_def empty_fail_get empty_fail_assert)
lemma empty_fail_not_snd:
"\<lbrakk> \<not> snd (m s); empty_fail m \<rbrakk> \<Longrightarrow> \<exists>v. v \<in> fst (m s)"
by (fastforce simp: empty_fail_def)