diff options
| author | Thomas Bauereiss | 2018-05-18 12:08:05 +0100 |
|---|---|---|
| committer | Thomas Bauereiss | 2018-05-18 20:11:24 +0100 |
| commit | 1644cf140a58b53ebfaebd90559d5a449df9e270 (patch) | |
| tree | 722b40b2fd2f4d657f50adc754e9a2466a1a2a13 /lib/isabelle/Prompt_monad_lemmas.thy | |
| parent | 6889366c61144d6dd0f9c37a0eb7a6c9f8ab2258 (diff) | |
Add lemmas about monadic Boolean connectives
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 |