diff options
Diffstat (limited to 'lib/isabelle/Prompt_monad_lemmas.thy')
| -rw-r--r-- | lib/isabelle/Prompt_monad_lemmas.thy | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/lib/isabelle/Prompt_monad_lemmas.thy b/lib/isabelle/Prompt_monad_lemmas.thy index e883c2a0..7a3a108d 100644 --- a/lib/isabelle/Prompt_monad_lemmas.thy +++ b/lib/isabelle/Prompt_monad_lemmas.thy @@ -17,6 +17,7 @@ lemmas bind_induct[case_names Done Read_mem Write_memv Read_reg Excl_res Write_e lemma bind_return[simp]: "bind (return a) f = f a" by (auto simp: return_def) +lemma bind_return_right[simp]: "bind x return = x" by (induction x) (auto simp: return_def) lemma bind_assoc[simp]: "bind (bind m f) g = bind m (\<lambda>x. bind (f x) g)" by (induction m f arbitrary: g rule: bind.induct) auto |