diff options
| author | Thomas Bauereiss | 2018-04-18 16:03:26 +0100 |
|---|---|---|
| committer | Thomas Bauereiss | 2018-04-18 16:03:26 +0100 |
| commit | e1b2379f9058e858722f2bd9691c76d00c00dcaa (patch) | |
| tree | 635c9dfcf02772200796297f98aea114a118fda1 /lib/isabelle/Prompt_monad_lemmas.thy | |
| parent | 15f965c9e4bd39eb7fe97552b9ac9db51a3cdbfb (diff) | |
Add some lemmas about bitvectors
Also clean up some library functions a bit, and add some missing failure
handling variants of division operations on bitvectors.
Diffstat (limited to 'lib/isabelle/Prompt_monad_lemmas.thy')
| -rw-r--r-- | lib/isabelle/Prompt_monad_lemmas.thy | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/lib/isabelle/Prompt_monad_lemmas.thy b/lib/isabelle/Prompt_monad_lemmas.thy index 84f3333e..e883c2a0 100644 --- a/lib/isabelle/Prompt_monad_lemmas.thy +++ b/lib/isabelle/Prompt_monad_lemmas.thy @@ -13,7 +13,7 @@ lemma All_bind_dom: "bind_dom (m, f)" by (induction m) (auto intro: bind.domintros) termination bind using All_bind_dom by auto -lemmas bind_induct[case_names Done Read_mem Write_memv Read_reg Excl_res Write_ea Barrier Write_reg Fail Error Exception] = bind.induct +lemmas bind_induct[case_names Done Read_mem Write_memv Read_reg Excl_res Write_ea Barrier Write_reg Fail Exception] = bind.induct lemma bind_return[simp]: "bind (return a) f = f a" by (auto simp: return_def) @@ -21,10 +21,13 @@ lemma bind_return[simp]: "bind (return a) f = f a" 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 +lemma bind_assert_True[simp]: "bind (assert_exp True msg) f = f ()" + by (auto simp: assert_exp_def) + lemma All_try_catch_dom: "try_catch_dom (m, h)" by (induction m) (auto intro: try_catch.domintros) termination try_catch using All_try_catch_dom by auto -lemmas try_catch_induct[case_names Done Read_mem Write_memv Read_reg Excl_res Write_ea Barrier Write_reg Fail Error Exception] = try_catch.induct +lemmas try_catch_induct[case_names Done Read_mem Write_memv Read_reg Excl_res Write_ea Barrier Write_reg Fail Exception] = try_catch.induct datatype 'regval event = (* Request to read memory *) |