lib/monads: style cleanup in Empty_Fail
Mostly contraction and some refactoring. Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
This commit is contained in:
parent
e51723ce5a
commit
b93335745e
|
@ -55,23 +55,26 @@ lemma empty_fail_select_f [simp]:
|
||||||
|
|
||||||
lemma empty_fail_bind [simp]:
|
lemma empty_fail_bind [simp]:
|
||||||
"\<lbrakk> empty_fail a; \<And>x. empty_fail (b x) \<rbrakk> \<Longrightarrow> empty_fail (a >>= b)"
|
"\<lbrakk> empty_fail a; \<And>x. empty_fail (b x) \<rbrakk> \<Longrightarrow> empty_fail (a >>= b)"
|
||||||
apply (simp add: bind_def empty_fail_def split_def)
|
by (fastforce simp: bind_def empty_fail_def split_def)
|
||||||
apply clarsimp
|
|
||||||
apply (case_tac "fst (a s) = {}")
|
|
||||||
apply blast
|
|
||||||
apply (clarsimp simp: ex_in_conv [symmetric])
|
|
||||||
done
|
|
||||||
|
|
||||||
lemma empty_fail_return [simp, wp]:
|
lemma empty_fail_return [simp, wp]:
|
||||||
"empty_fail (return x)"
|
"empty_fail (return x)"
|
||||||
by (simp add: empty_fail_def return_def)
|
by (simp add: empty_fail_def return_def)
|
||||||
|
|
||||||
|
lemma empty_fail_error_bits[simp]:
|
||||||
|
"empty_fail (returnOk v)"
|
||||||
|
"empty_fail (throwError v)"
|
||||||
|
"empty_fail (liftE f) = empty_fail f"
|
||||||
|
by (fastforce simp: returnOk_def throwError_def liftE_def empty_fail_def bind_def return_def)+
|
||||||
|
|
||||||
|
lemma empty_fail_lift:
|
||||||
|
"\<lbrakk> \<And>x. empty_fail (f x) \<rbrakk> \<Longrightarrow> empty_fail (lift f x)"
|
||||||
|
unfolding lift_def
|
||||||
|
by (auto split: sum.split)
|
||||||
|
|
||||||
lemma empty_fail_bindE:
|
lemma empty_fail_bindE:
|
||||||
"\<lbrakk> empty_fail f; \<And>rv. empty_fail (g rv) \<rbrakk> \<Longrightarrow> empty_fail (f >>=E g)"
|
"\<lbrakk> empty_fail f; \<And>rv. empty_fail (g rv) \<rbrakk> \<Longrightarrow> empty_fail (f >>=E g)"
|
||||||
apply (simp add: bindE_def)
|
by (simp add: bindE_def empty_fail_lift)
|
||||||
apply (erule empty_fail_bind)
|
|
||||||
apply (simp add: lift_def throwError_def split: sum.split)
|
|
||||||
done
|
|
||||||
|
|
||||||
lemma empty_fail_If:
|
lemma empty_fail_If:
|
||||||
"\<lbrakk> P \<Longrightarrow> empty_fail f; \<not> P \<Longrightarrow> empty_fail g \<rbrakk> \<Longrightarrow> empty_fail (if P then f else g)"
|
"\<lbrakk> P \<Longrightarrow> empty_fail f; \<not> P \<Longrightarrow> empty_fail g \<rbrakk> \<Longrightarrow> empty_fail (if P then f else g)"
|
||||||
|
@ -111,12 +114,6 @@ lemma empty_fail_gets_map[simp]:
|
||||||
"empty_fail (gets_map f p)"
|
"empty_fail (gets_map f p)"
|
||||||
unfolding gets_map_def by simp
|
unfolding gets_map_def by simp
|
||||||
|
|
||||||
lemma empty_fail_error_bits[simp]:
|
|
||||||
"empty_fail (returnOk v)"
|
|
||||||
"empty_fail (throwError v)"
|
|
||||||
"empty_fail (liftE f) = empty_fail f"
|
|
||||||
by (fastforce simp: returnOk_def throwError_def liftE_def empty_fail_def bind_def return_def)+
|
|
||||||
|
|
||||||
lemma empty_fail_whenEs:
|
lemma empty_fail_whenEs:
|
||||||
"empty_fail f \<Longrightarrow> empty_fail (whenE P f)"
|
"empty_fail f \<Longrightarrow> empty_fail (whenE P f)"
|
||||||
"empty_fail f \<Longrightarrow> empty_fail (unlessE P f)"
|
"empty_fail f \<Longrightarrow> empty_fail (unlessE P f)"
|
||||||
|
|
Loading…
Reference in New Issue