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

lib: OptionMonad: add more obind decomposition, oassert simps

This commit is contained in:
Rafal Kolanski 2019-03-07 17:07:25 +11:00
parent 014f351265
commit 66d87cd550
1 changed files with 12 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

12
lib/Monad_WP/OptionMonad.thy
View File

@ -188,6 +188,14 @@ lemma in_oassert_eq [simp]:
"(oassert P s = Some v) = P"
by (simp add: oassert_def)
lemma oassert_True [simp]:
"oassert True = oreturn ()"
by (simp add: oassert_def)
lemma oassert_False [simp]:
"oassert False = ofail"
by (simp add: oassert_def)
lemma oassertE:
"\<lbrakk> oassert P s = Some v; P \<Longrightarrow> Q \<rbrakk> \<Longrightarrow> Q"
by simp
@ -196,6 +204,10 @@ lemma in_obind_eq:
"((f |>> g) s = Some v) = (\<exists>v'. f s = Some v' \<and> g v' s = Some v)"
by (simp add: obind_def split: option.splits)
lemma obind_eqI:
"\<lbrakk> f s = f s' ; \<And>x. f s = Some x \<Longrightarrow> g x s = g' x s' \<rbrakk> \<Longrightarrow> obind f g s = obind f g' s'"
by (simp add: obind_def split: option.splits)
lemma obindE:
"\<lbrakk> (f |>> g) s = Some v;
\<And>v'. \<lbrakk>f s = Some v'; g v' s = Some v\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"