diff options
Diffstat (limited to 'lib/isabelle/State_monad_lemmas.thy')
| -rw-r--r-- | lib/isabelle/State_monad_lemmas.thy | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/lib/isabelle/State_monad_lemmas.thy b/lib/isabelle/State_monad_lemmas.thy index e7286fcf..e0d684ba 100644 --- a/lib/isabelle/State_monad_lemmas.thy +++ b/lib/isabelle/State_monad_lemmas.thy @@ -32,6 +32,9 @@ lemma bindS_readS: "bindS (readS f) m = (\<lambda>s. m (f s) s)" lemma bindS_updateS: "bindS (updateS f) m = (\<lambda>s. m () (f s))" by (auto simp: bindS_def updateS_def returnS_def) +lemma bindS_assertS_True[simp]: "bindS (assert_expS True msg) f = f ()" + by (auto simp: assert_expS_def) + lemma result_cases: fixes r :: "('a, 'e) result" @@ -126,6 +129,13 @@ lemma try_catchS_intros: "\<And>m h s e s'' r s'. (Ex (Throw e), s'') \<in> m s \<Longrightarrow> (r, s') \<in> h e s'' \<Longrightarrow> (r, s') \<in> try_catchS m h s" by (auto simp: try_catchS_def returnS_def intro: bexI[rotated]) +lemma no_Ex_basic_builtins[simp]: + "\<And>s e s' a. (Ex e, s') \<in> returnS a s \<longleftrightarrow> False" + "\<And>s e s' f. (Ex e, s') \<in> readS f s \<longleftrightarrow> False" + "\<And>s e s' f. (Ex e, s') \<in> updateS f s \<longleftrightarrow> False" + "\<And>s e s' xs. (Ex e, s') \<in> chooseS xs s \<longleftrightarrow> False" + by (auto simp: readS_def updateS_def returnS_def chooseS_def) + fun ignore_throw_aux :: "(('a, 'e1) result \<times> 's) \<Rightarrow> (('a, 'e2) result \<times> 's) set" where "ignore_throw_aux (Value a, s') = {(Value a, s')}" | "ignore_throw_aux (Ex (Throw e), s') = {}" |