diff options
Diffstat (limited to 'lib/isabelle/Sail2_state_monad_lemmas.thy')
| -rw-r--r-- | lib/isabelle/Sail2_state_monad_lemmas.thy | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/lib/isabelle/Sail2_state_monad_lemmas.thy b/lib/isabelle/Sail2_state_monad_lemmas.thy index b705de4c..91e4c17e 100644 --- a/lib/isabelle/Sail2_state_monad_lemmas.thy +++ b/lib/isabelle/Sail2_state_monad_lemmas.thy @@ -35,6 +35,9 @@ lemma bindS_updateS: "bindS (updateS f) m = (\<lambda>s. m () (f s))" lemma bindS_assertS_True[simp]: "bindS (assert_expS True msg) f = f ()" by (auto simp: assert_expS_def) +lemma bindS_chooseS_returnS[simp]: "bindS (chooseS xs) (\<lambda>x. returnS (f x)) = chooseS (f ` xs)" + by (intro ext) (auto simp: bindS_def chooseS_def returnS_def) + lemma result_cases: fixes r :: "('a, 'e) result" |