diff options
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/isabelle/Hoare.thy | 22 | ||||
| -rw-r--r-- | lib/isabelle/ROOT | 2 | ||||
| -rw-r--r-- | lib/isabelle/Sail2_operators_mwords_lemmas.thy | 4 | ||||
| -rw-r--r-- | lib/isabelle/Sail2_prompt_monad_lemmas.thy | 8 | ||||
| -rw-r--r-- | lib/isabelle/Sail2_state_lemmas.thy | 12 | ||||
| -rw-r--r-- | lib/isabelle/Sail2_state_monad_lemmas.thy | 6 |
6 files changed, 38 insertions, 16 deletions
diff --git a/lib/isabelle/Hoare.thy b/lib/isabelle/Hoare.thy index 76750117..98b7d077 100644 --- a/lib/isabelle/Hoare.thy +++ b/lib/isabelle/Hoare.thy @@ -164,7 +164,7 @@ qed lemma PrePost_assert_expS[intro, PrePost_atomI]: "PrePost (if c then P (Value ()) else P (Ex (Failure m))) (assert_expS c m) P" unfolding PrePost_def assert_expS_def by (auto simp: returnS_def failS_def) -lemma PrePost_chooseS[intro, PrePost_atomI]: "PrePost (\<lambda>s. \<forall>x \<in> xs. Q (Value x) s) (chooseS xs) Q" +lemma PrePost_chooseS[intro, PrePost_atomI]: "PrePost (\<lambda>s. \<forall>x \<in> set xs. Q (Value x) s) (chooseS xs) Q" by (auto simp: PrePost_def chooseS_def) lemma PrePost_failS[intro, PrePost_atomI]: "PrePost (Q (Ex (Failure msg))) (failS msg) Q" @@ -381,7 +381,7 @@ lemma PrePostE_exitS[PrePostE_atomI, intro]: "PrePostE (E (Failure ''exit'')) (e unfolding exitS_def PrePostE_def PrePost_def failS_def by auto lemma PrePostE_chooseS[intro, PrePostE_atomI]: - "PrePostE (\<lambda>s. \<forall>x \<in> xs. Q x s) (chooseS xs) Q E" + "PrePostE (\<lambda>s. \<forall>x \<in> set xs. Q x s) (chooseS xs) Q E" unfolding PrePostE_def by (auto intro: PrePost_strengthen_pre) lemma PrePostE_throwS[PrePostE_atomI]: "PrePostE (E (Throw e)) (throwS e) Q E" @@ -488,11 +488,11 @@ lemma PrePostE_liftState_untilM_pure_cond: shows "PrePostE (Inv Q vars) (liftState r (untilM vars (return \<circ> cond) body)) Q E" using assms by (intro PrePostE_liftState_untilM) (auto simp: comp_def liftState_simp) -lemma PrePostE_undefined_boolS[PrePostE_atomI]: +lemma PrePostE_choose_boolS_any[PrePostE_atomI]: "PrePostE (\<lambda>s. \<forall>b. Q b s) - (undefined_boolS unit) Q E" - unfolding undefined_boolS_def seqS_def - by (auto intro: PrePostE_strengthen_pre PrePostE_chooseS) + (choose_boolS unit) Q E" + unfolding choose_boolS_def seqS_def + by (auto intro: PrePostE_strengthen_pre) lemma PrePostE_bool_of_bitU_nondetS_any: "PrePostE (\<lambda>s. \<forall>b. Q b s) (bool_of_bitU_nondetS b) Q E" @@ -507,11 +507,19 @@ lemma PrePostE_bools_of_bits_nondetS_any: PrePostE_bool_of_bitU_nondetS_any)+) auto +lemma PrePostE_choose_boolsS_any: + "PrePostE (\<lambda>s. \<forall>bs. Q bs s) (choose_boolsS n) Q E" + unfolding choose_boolsS_def genlistS_def Let_def + by (rule PrePostE_weaken_post[where B = "\<lambda>_ s. \<forall>bs. Q bs s"], rule PrePostE_strengthen_pre, + (rule PrePostE_foreachS_invariant[OF PrePostE_strengthen_pre] PrePostE_bindS PrePostE_returnS + PrePostE_choose_boolS_any)+) + auto + lemma PrePostE_internal_pick: "xs \<noteq> [] \<Longrightarrow> PrePostE (\<lambda>s. \<forall>x \<in> set xs. Q x s) (internal_pickS xs) Q E" unfolding internal_pickS_def Let_def by (rule PrePostE_strengthen_pre, - (rule PrePostE_compositeI PrePostE_atomI PrePostE_bools_of_bits_nondetS_any)+) + (rule PrePostE_compositeI PrePostE_atomI PrePostE_choose_boolsS_any)+) (auto split: option.splits) end diff --git a/lib/isabelle/ROOT b/lib/isabelle/ROOT index 545e47c4..fb73a673 100644 --- a/lib/isabelle/ROOT +++ b/lib/isabelle/ROOT @@ -2,7 +2,7 @@ session "Sail" = "LEM" + options [browser_info, document = pdf, document_output = "output"] sessions "HOL-Eisbach" - theories [document = false] + theories Sail2_values_lemmas Sail2_prompt Sail2_state_lemmas diff --git a/lib/isabelle/Sail2_operators_mwords_lemmas.thy b/lib/isabelle/Sail2_operators_mwords_lemmas.thy index fd54c93a..3e8dcb2f 100644 --- a/lib/isabelle/Sail2_operators_mwords_lemmas.thy +++ b/lib/isabelle/Sail2_operators_mwords_lemmas.thy @@ -55,7 +55,7 @@ lemma bool_of_bitU_monadic_simps[simp]: "bool_of_bitU_fail BU = Fail ''bool_of_bitU''" "bool_of_bitU_nondet B0 = return False" "bool_of_bitU_nondet B1 = return True" - "bool_of_bitU_nondet BU = undefined_bool ()" + "bool_of_bitU_nondet BU = choose_bool ''bool_of_bitU''" unfolding bool_of_bitU_fail_def bool_of_bitU_nondet_def by auto @@ -68,7 +68,7 @@ lemma update_vec_dec_simps[simp]: "update_vec_dec_fail w i BU = Fail ''bool_of_bitU''" "update_vec_dec_nondet w i B0 = return (set_bit w (nat i) False)" "update_vec_dec_nondet w i B1 = return (set_bit w (nat i) True)" - "update_vec_dec_nondet w i BU = undefined_bool () \<bind> (\<lambda>b. return (set_bit w (nat i) b))" + "update_vec_dec_nondet w i BU = choose_bool ''bool_of_bitU'' \<bind> (\<lambda>b. return (set_bit w (nat i) b))" "update_vec_dec w i B0 = set_bit w (nat i) False" "update_vec_dec w i B1 = set_bit w (nat i) True" unfolding update_vec_dec_maybe_def update_vec_dec_fail_def update_vec_dec_nondet_def update_vec_dec_def 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 diff --git a/lib/isabelle/Sail2_state_lemmas.thy b/lib/isabelle/Sail2_state_lemmas.thy index 77f4ac5a..d99dfc85 100644 --- a/lib/isabelle/Sail2_state_lemmas.thy +++ b/lib/isabelle/Sail2_state_lemmas.thy @@ -45,6 +45,9 @@ lemma liftState_barrier[liftState_simp]: "liftState r (barrier bk) = returnS ()" by (auto simp: barrier_def) lemma liftState_footprint[liftState_simp]: "liftState r (footprint ()) = returnS ()" by (auto simp: footprint_def) +lemma liftState_choose_bool[liftState_simp]: "liftState r (choose_bool descr) = choose_boolS ()" + by (auto simp: choose_bool_def liftState_simp) +declare undefined_boolS_def[simp] lemma liftState_undefined[liftState_simp]: "liftState r (undefined_bool ()) = undefined_boolS ()" by (auto simp: undefined_bool_def liftState_simp) lemma liftState_maybe_fail[liftState_simp]: "liftState r (maybe_fail msg x) = maybe_failS msg x" @@ -149,6 +152,14 @@ lemma liftState_foreachM[liftState_simp]: by (induction xs vars "\<lambda>x vars. liftState r (body x vars)" rule: foreachS.induct) (auto simp: liftState_simp cong: bindS_cong) +lemma liftState_genlistM[liftState_simp]: + "liftState r (genlistM f n) = genlistS (liftState r \<circ> f) n" + by (auto simp: genlistM_def genlistS_def liftState_simp cong: bindS_cong) + +lemma liftState_choose_bools[liftState_simp]: + "liftState r (choose_bools descr n) = choose_boolsS n" + by (auto simp: choose_bools_def choose_boolsS_def liftState_simp comp_def) + lemma liftState_bools_of_bits_nondet[liftState_simp]: "liftState r (bools_of_bits_nondet bs) = bools_of_bits_nondetS bs" unfolding bools_of_bits_nondet_def bools_of_bits_nondetS_def @@ -157,6 +168,7 @@ lemma liftState_bools_of_bits_nondet[liftState_simp]: lemma liftState_internal_pick[liftState_simp]: "liftState r (internal_pick xs) = internal_pickS xs" by (auto simp: internal_pick_def internal_pickS_def liftState_simp comp_def + chooseM_def option.case_distrib[where h = "liftState r"] simp del: repeat.simps cong: option.case_cong) diff --git a/lib/isabelle/Sail2_state_monad_lemmas.thy b/lib/isabelle/Sail2_state_monad_lemmas.thy index 12452ca4..ca7e5751 100644 --- a/lib/isabelle/Sail2_state_monad_lemmas.thy +++ b/lib/isabelle/Sail2_state_monad_lemmas.thy @@ -38,10 +38,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)" +lemma bindS_chooseS_returnS[simp]: "bindS (chooseS xs) (\<lambda>x. returnS (f x)) = chooseS (map f xs)" by (intro ext) (auto simp: bindS_def chooseS_def returnS_def) - lemma result_cases: fixes r :: "('a, 'e) result" obtains (Value) a where "r = Value a" @@ -198,9 +197,10 @@ lemma no_throw_basic_builtins[simp]: "\<And>f. ignore_throw (readS f) = readS f" "\<And>f. ignore_throw (updateS f) = updateS f" "ignore_throw (chooseS xs) = chooseS xs" + "ignore_throw (choose_boolS ()) = choose_boolS ()" "ignore_throw (failS msg) = failS msg" "ignore_throw (maybe_failS msg x) = maybe_failS msg x" - unfolding ignore_throw_def returnS_def chooseS_def maybe_failS_def failS_def readS_def updateS_def + unfolding ignore_throw_def returnS_def chooseS_def maybe_failS_def failS_def readS_def updateS_def choose_boolS_def by (intro ext; auto split: option.splits)+ lemmas ignore_throw_option_case_distrib = |