diff options
Diffstat (limited to 'lib/isabelle/Sail2_prompt_monad_lemmas.thy')
| -rw-r--r-- | lib/isabelle/Sail2_prompt_monad_lemmas.thy | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/lib/isabelle/Sail2_prompt_monad_lemmas.thy b/lib/isabelle/Sail2_prompt_monad_lemmas.thy index c59fc62f..54f58fad 100644 --- a/lib/isabelle/Sail2_prompt_monad_lemmas.thy +++ b/lib/isabelle/Sail2_prompt_monad_lemmas.thy @@ -40,7 +40,7 @@ inductive_set T :: "(('rv, 'a, 'e) monad \<times> 'rv event \<times> ('rv, 'a, ' | Barrier: "((Barrier bk k), E_barrier bk, k) \<in> T" | Read_reg: "((Read_reg r k), E_read_reg r v, k v) \<in> T" | Write_reg: "((Write_reg r v k), E_write_reg r v, k) \<in> T" -| Undefined: "((Undefined k), E_undefined v, k v) \<in> T" +| Choose: "((Choose descr k), E_choose descr v, k v) \<in> T" | Print: "((Print msg k), E_print msg, k) \<in> T" inductive_set Traces :: "(('rv, 'a, 'e) monad \<times> 'rv event list \<times> ('rv, 'a, 'e) monad) set" where @@ -70,7 +70,7 @@ lemma Traces_cases: | (Write_ea) wk addr s k t' where "m = Write_ea wk addr s k" and "t = E_write_ea wk addr s # t'" and "(k, t', m') \<in> Traces" | (Footprint) k t' where "m = Footprint k" and "t = E_footprint # t'" and "(k, t', m') \<in> Traces" | (Write_reg) reg v k t' where "m = Write_reg reg v k" and "t = E_write_reg reg v # t'" and "(k, t', m') \<in> Traces" - | (Undefined) xs v k t' where "m = Undefined k" and "t = E_undefined v # t'" and "(k v, t', m') \<in> Traces" + | (Choose) descr v k t' where "m = Choose descr k" and "t = E_choose descr v # t'" and "(k v, t', m') \<in> Traces" | (Print) msg k t' where "m = Print msg k" and "t = E_print msg # t'" and "(k, t', m') \<in> Traces" proof (use Run in \<open>cases m t m' set: Traces\<close>) case Nil @@ -185,8 +185,10 @@ lemma bind_cong[fundef_cong]: lemma liftR_read_reg[simp]: "liftR (read_reg reg) = read_reg reg" by (auto simp: read_reg_def liftR_def split: option.splits) lemma try_catch_return[simp]: "try_catch (return x) h = return x" by (auto simp: return_def) +lemma try_catch_choose_bool[simp]: "try_catch (choose_bool descr) h = choose_bool descr" by (auto simp: choose_bool_def) +lemma liftR_choose_bool[simp]: "liftR (choose_bool descr) = choose_bool descr" by (auto simp: choose_bool_def liftR_def) lemma liftR_return[simp]: "liftR (return x) = return x" by (auto simp: liftR_def) -lemma liftR_undefined_bool[simp]: "liftR (undefined_bool ()) = undefined_bool ()" by (auto simp: undefined_bool_def liftR_def) +lemma liftR_undefined_bool[simp]: "liftR (undefined_bool ()) = undefined_bool ()" by (auto simp: undefined_bool_def) lemma assert_exp_True_return[simp]: "assert_exp True msg = return ()" by (auto simp: assert_exp_def return_def) end |