diff options
Diffstat (limited to 'lib/isabelle')
| -rw-r--r-- | lib/isabelle/Hoare.thy | 22 | ||||
| -rw-r--r-- | lib/isabelle/Makefile | 2 | ||||
| -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 | 304 | ||||
| -rw-r--r-- | lib/isabelle/Sail2_state_lemmas.thy | 189 | ||||
| -rw-r--r-- | lib/isabelle/Sail2_state_monad_lemmas.thy | 37 | ||||
| -rw-r--r-- | lib/isabelle/Sail2_values_lemmas.thy | 28 |
8 files changed, 475 insertions, 113 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/Makefile b/lib/isabelle/Makefile index 039a81f1..465b4c36 100644 --- a/lib/isabelle/Makefile +++ b/lib/isabelle/Makefile @@ -21,7 +21,7 @@ heap-img: thys $(EXTRA_THYS) ROOT ifeq ($(wildcard $(LEM_ISA_LIB)/ROOT),) $(error isabelle-lib directory of Lem not found. Please set the LEM_ISA_LIB environment variable) endif - isabelle build -d $(LEM_ISA_LIB) -D . + isabelle build -b -d $(LEM_ISA_LIB) -D . manual: heap-img manual/Manual.thy manual/ROOT manual/document/root.tex cp output/document/session_graph.pdf manual/document/Sail_session_graph.pdf 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 25eb9f52..1fde3287 100644 --- a/lib/isabelle/Sail2_prompt_monad_lemmas.thy +++ b/lib/isabelle/Sail2_prompt_monad_lemmas.thy @@ -30,42 +30,22 @@ lemma All_try_catch_dom: "try_catch_dom (m, h)" 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 Exception] = try_catch.induct -datatype 'regval event = - (* Request to read memory *) - e_read_mem read_kind "bitU list" nat "memory_byte list" - | e_read_tag "bitU list" bitU - (* Write is imminent, at address lifted, of size nat *) - | e_write_ea write_kind "bitU list" nat - (* Request the result of store-exclusive *) - | e_excl_res bool - (* Request to write memory at last signalled address. Memory value should be 8 - times the size given in ea signal *) - | e_write_memv "memory_byte list" bool - | e_write_tag "bitU list" bitU bool - (* Tell the system to dynamically recalculate dependency footprint *) - | e_footprint - (* Request a memory barrier *) - | e_barrier " barrier_kind " - (* Request to read register *) - | e_read_reg string 'regval - (* Request to write register *) - | e_write_reg string 'regval - | e_undefined bool - | e_print string - inductive_set T :: "(('rv, 'a, 'e) monad \<times> 'rv event \<times> ('rv, 'a, 'e) monad) set" where - Read_mem: "((Read_mem rk addr sz k), e_read_mem rk addr sz v, k v) \<in> T" -| Read_tag: "((Read_tag addr k), e_read_tag addr v, k v) \<in> T" -| Write_ea: "((Write_ea wk addr sz k), e_write_ea wk addr sz, k) \<in> T" -| Excl_res: "((Excl_res k), e_excl_res r, k r) \<in> T" -| Write_memv: "((Write_memv v k), e_write_memv v r, k r) \<in> T" -| Write_tag: "((Write_tag a v k), e_write_tag a v r, k r) \<in> T" -| Footprint: "((Footprint k), e_footprint, k) \<in> T" -| 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" -| Print: "((Print msg k), e_print msg, k) \<in> T" + Read_mem: "((Read_mem rk addr sz k), E_read_mem rk addr sz v, k v) \<in> T" +| Read_memt: "((Read_memt rk addr sz k), E_read_memt rk addr sz v, k v) \<in> T" +| Write_ea: "((Write_ea wk addr sz k), E_write_ea wk addr sz, k) \<in> T" +| Excl_res: "((Excl_res k), E_excl_res r, k r) \<in> T" +| Write_mem: "((Write_mem wk addr sz v k), E_write_mem wk addr sz v r, k r) \<in> T" +| Write_memt: "((Write_memt wk addr sz v t k), E_write_memt wk addr sz v t r, k r) \<in> T" +| Footprint: "((Footprint k), E_footprint, k) \<in> T" +| 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" +| Choose: "((Choose descr k), E_choose descr v, k v) \<in> T" +| Print: "((Print msg k), E_print msg, k) \<in> T" + +lemma emitEvent_iff_T: "emitEvent m e = Some m' \<longleftrightarrow> (m, e, m') \<in> T" + by (cases e) (auto simp: emitEvent_def elim: T.cases intro: T.intros split: monad.splits) inductive_set Traces :: "(('rv, 'a, 'e) monad \<times> 'rv event list \<times> ('rv, 'a, 'e) monad) set" where Nil: "(s, [], s) \<in> Traces" @@ -81,38 +61,68 @@ lemmas Traces_ConsI = T.intros[THEN Step, rotated] inductive_cases Traces_NilE[elim]: "(s, [], s') \<in> Traces" inductive_cases Traces_ConsE[elim]: "(s, e # t, s') \<in> Traces" +lemma runTrace_iff_Traces: "runTrace t m = Some m' \<longleftrightarrow> (m, t, m') \<in> Traces" + by (induction t m rule: runTrace.induct; fastforce simp: bind_eq_Some_conv emitEvent_iff_T) + +lemma hasTrace_iff_Traces_final: "hasTrace t m \<longleftrightarrow> (\<exists>m'. (m, t, m') \<in> Traces \<and> final m')" + by (auto simp: hasTrace_def runTrace_iff_Traces[symmetric] split: option.splits) + lemma Traces_cases: fixes m :: "('rv, 'a, 'e) monad" assumes Run: "(m, t, m') \<in> Traces" obtains (Nil) a where "m = m'" and "t = []" - | (Read_mem) rk addr s k t' v where "m = Read_mem rk addr s k" and "t = e_read_mem rk addr s v # t'" and "(k v, t', m') \<in> Traces" - | (Read_tag) addr k t' v where "m = Read_tag addr k" and "t = e_read_tag addr v # t'" and "(k v, t', m') \<in> Traces" - | (Write_memv) val k t' v where "m = Write_memv val k" and "t = e_write_memv val v # t'" and "(k v, t', m') \<in> Traces" - | (Write_tag) a val k t' v where "m = Write_tag a val k" and "t = e_write_tag a val v # t'" and "(k v, t', m') \<in> Traces" - | (Barrier) bk k t' v where "m = Barrier bk k" and "t = e_barrier bk # t'" and "(k, t', m') \<in> Traces" - | (Read_reg) reg k t' v where "m = Read_reg reg k" and "t = e_read_reg reg v # t'" and "(k v, t', m') \<in> Traces" - | (Excl_res) k t' v where "m = Excl_res k" and "t = e_excl_res v # t'" and "(k v, t', m') \<in> Traces" - | (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" - | (Print) msg k t' where "m = Print msg k" and "t = e_print msg # t'" and "(k, t', m') \<in> Traces" + | (Read_mem) rk addr s k t' v where "m = Read_mem rk addr s k" and "t = E_read_mem rk addr s v # t'" and "(k v, t', m') \<in> Traces" + | (Read_memt) rk addr s k t' v tag where "m = Read_memt rk addr s k" and "t = E_read_memt rk addr s (v, tag) # t'" and "(k (v, tag), t', m') \<in> Traces" + | (Write_mem) wk addr sz val k v t' where "m = Write_mem wk addr sz val k" and "t = E_write_mem wk addr sz val v # t'" and "(k v, t', m') \<in> Traces" + | (Write_memt) wk addr sz val tag k t' v where "m = Write_memt wk addr sz val tag k" and "t = E_write_memt wk addr sz val tag v # t'" and "(k v, t', m') \<in> Traces" + | (Barrier) bk k t' v where "m = Barrier bk k" and "t = E_barrier bk # t'" and "(k, t', m') \<in> Traces" + | (Read_reg) reg k t' v where "m = Read_reg reg k" and "t = E_read_reg reg v # t'" and "(k v, t', m') \<in> Traces" + | (Excl_res) k t' v where "m = Excl_res k" and "t = E_excl_res v # t'" and "(k v, t', m') \<in> Traces" + | (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" + | (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 then show ?thesis by (auto intro: that(1)) next case (Step e m'' t') - from \<open>(m, e, m'') \<in> T\<close> and \<open>t = e # t'\<close> and \<open>(m'', t', m') \<in> Traces\<close> - show ?thesis by (cases m e m'' rule: T.cases; elim that; blast) + note t = \<open>t = e # t'\<close> + note m' = \<open>(m'', t', m') \<in> Traces\<close> + from \<open>(m, e, m'') \<in> T\<close> and t and m' + show ?thesis proof (cases m e m'' rule: T.cases) + case (Read_memt rk addr sz k v) + then show ?thesis using t m' by (cases v; elim that; blast) + qed (elim that; blast)+ qed abbreviation Run :: "('rv, 'a, 'e) monad \<Rightarrow> 'rv event list \<Rightarrow> 'a \<Rightarrow> bool" where "Run s t a \<equiv> (s, t, Done a) \<in> Traces" -lemma Run_appendI: +lemma final_cases: + assumes "final m" + obtains (Done) a where "m = Done a" | (Fail) f where "m = Fail f" | (Ex) e where "m = Exception e" + using assms by (cases m) (auto simp: final_def) + +lemma hasTraces_elim: + assumes "hasTrace t m" + obtains m' where "(m, t, m') \<in> Traces" and "final m'" + using assms + unfolding hasTrace_iff_Traces_final + by blast + +lemma hasTrace_cases: + assumes "hasTrace t m" + obtains (Run) a where "Run m t a" + | (Fail) f where "(m, t, Fail f) \<in> Traces" + | (Ex) e where "(m, t, Exception e) \<in> Traces" + using assms by (elim hasTraces_elim final_cases) auto + +lemma Traces_appendI: assumes "(s, t1, s') \<in> Traces" - and "Run s' t2 a" - shows "Run s (t1 @ t2) a" + and "(s', t2, s'') \<in> Traces" + shows "(s, t1 @ t2, s'') \<in> Traces" proof (use assms in \<open>induction t1 arbitrary: s\<close>) case (Cons e t1) then show ?case by (elim Traces_ConsE) auto @@ -125,20 +135,188 @@ lemma bind_DoneE: lemma bind_T_cases: assumes "(bind m f, e, s') \<in> T" - obtains (Done) a where "m = Done a" + obtains (Done) a where "m = Done a" and "(f a, e, s') \<in> T" | (Bind) m' where "s' = bind m' f" and "(m, e, m') \<in> T" - using assms by (cases; blast elim: bind.elims) + using assms by (cases; fastforce elim: bind.elims) -lemma Run_bindI: +lemma Traces_bindI: fixes m :: "('r, 'a, 'e) monad" assumes "Run m t1 a1" - and "Run (f a1) t2 a2" - shows "Run (m \<bind> f) (t1 @ t2) a2" + and "(f a1, t2, m') \<in> Traces" + shows "(m \<bind> f, t1 @ t2, m') \<in> Traces" proof (use assms in \<open>induction m t1 "Done a1 :: ('r, 'a, 'e) monad" rule: Traces.induct\<close>) case (Step s e s'' t) then show ?case by (elim T.cases) auto qed auto +lemma Run_DoneE: + assumes "Run (Done a) t a'" + obtains "t = []" and "a' = a" + using assms by (auto elim: Traces.cases T.cases) + +lemma Run_Done_iff_Nil[simp]: "Run (Done a) t a' \<longleftrightarrow> t = [] \<and> a' = a" + by (auto elim: Run_DoneE) + +lemma Run_Nil_iff_Done: "Run m [] a \<longleftrightarrow> m = Done a" + by auto + +lemma Traces_Nil_iff: "(m, [], m') \<in> Traces \<longleftrightarrow> m' = m" + by auto + +lemma bind_Traces_cases: + assumes "(m \<bind> f, t, m') \<in> Traces" + obtains (Left) m'' where "(m, t, m'') \<in> Traces" and "m' = m'' \<bind> f" + | (Bind) tm am tf where "t = tm @ tf" and "Run m tm am" and "(f am, tf, m') \<in> Traces" +proof (use assms in \<open>induction "bind m f" t m' arbitrary: m rule: Traces.induct\<close>) + case Nil + then show ?case by (auto simp: Traces_Nil_iff) +next + case (Step e s'' t s') + note IH = Step(3) + note Left' = Step(4) + note Bind' = Step(5) + show thesis + proof (use \<open>(m \<bind> f, e, s'') \<in> T\<close> in \<open>cases rule: bind_T_cases\<close>) + case (Done a) + then show ?thesis using \<open>(s'', t, s') \<in> Traces\<close> Step(5)[of "[]" "e # t" a] by auto + next + case (Bind m') + show ?thesis + proof (rule IH) + show "s'' = m' \<bind> f" using Bind by blast + next + fix m'' + assume "(m', t, m'') \<in> Traces" and "s' = m'' \<bind> f" + then show thesis using \<open>(m, e, m') \<in> T\<close> Left'[of m''] by auto + next + fix tm tf am + assume "t = tm @ tf" and "Run m' tm am" and "(f am, tf, s') \<in> Traces" + then show thesis using \<open>(m, e, m') \<in> T\<close> Bind'[of "e # tm" tf am] by auto + qed + qed +qed + +lemma final_bind_cases: + assumes "final (m \<bind> f)" + obtains (Done) a where "m = Done a" and "final (f a)" + | (Fail) msg where "m = Fail msg" + | (Ex) e where "m = Exception e" + using assms by (cases m) (auto simp: final_def) + +lemma hasFailure_iff_Traces_Fail: "hasFailure t m \<longleftrightarrow> (\<exists>msg. (m, t, Fail msg) \<in> Traces)" + by (auto simp: hasFailure_def runTrace_iff_Traces[symmetric] split: option.splits monad.splits) + +lemma hasException_iff_Traces_Exception: "hasException t m \<longleftrightarrow> (\<exists>e. (m, t, Exception e) \<in> Traces)" + by (auto simp: hasException_def runTrace_iff_Traces[symmetric] split: option.splits monad.splits) + +lemma hasTrace_bind_cases: + assumes "hasTrace t (m \<bind> f)" + obtains (Bind) tm am tf where "t = tm @ tf" and "Run m tm am" and "hasTrace tf (f am)" + | (Fail) "hasFailure t m" + | (Ex) "hasException t m" +proof - + from assms obtain m' where t: "(m \<bind> f, t, m') \<in> Traces" and m': "final m'" + by (auto simp: hasTrace_iff_Traces_final) + note [simp] = hasTrace_iff_Traces_final hasFailure_iff_Traces_Fail hasException_iff_Traces_Exception + from t show thesis + proof (cases rule: bind_Traces_cases) + case (Left m'') + then show ?thesis + using m' Fail Ex Bind[of t "[]"] + by (fastforce elim!: final_bind_cases) + next + case (Bind tm am tf) + then show ?thesis + using m' that + by fastforce + qed +qed + +lemma try_catch_T_cases: + assumes "(try_catch m h, e, m') \<in> T" + obtains (NoEx) m'' where "(m, e, m'') \<in> T" and "m' = try_catch m'' h" + | (Ex) ex where "m = Exception ex" and "(h ex, e, m') \<in> T" + using assms + by (cases m) (auto elim!: T.cases) + +lemma try_catch_Traces_cases: + assumes "(try_catch m h, t, mtc) \<in> Traces" + obtains (NoEx) m' where "(m, t, m') \<in> Traces" and "mtc = try_catch m' h" + | (Ex) tm ex th where "(m, tm, Exception ex) \<in> Traces" and "(h ex, th, mtc) \<in> Traces" and "t = tm @ th" +proof (use assms in \<open>induction "try_catch m h" t mtc arbitrary: m rule: Traces.induct\<close>) + case Nil + then show ?case by auto +next + case (Step e mtc' t mtc) + note e = \<open>(try_catch m h, e, mtc') \<in> T\<close> + note t = \<open>(mtc', t, mtc) \<in> Traces\<close> + note IH = Step(3) + note NoEx_ConsE = Step(4) + note Ex_ConsE = Step(5) + show ?case + proof (use e in \<open>cases rule: try_catch_T_cases\<close>) + case (NoEx m1) + show ?thesis + proof (rule IH) + show "mtc' = try_catch m1 h" using NoEx by auto + next + fix m' + assume "(m1, t, m') \<in> Traces" and "mtc = try_catch m' h" + then show ?thesis + using NoEx NoEx_ConsE[of m'] + by auto + next + fix tm ex th + assume "(m1, tm, Exception ex) \<in> Traces" and "(h ex, th, mtc) \<in> Traces" and "t = tm @ th" + then show ?thesis + using NoEx Ex_ConsE[of "e # tm" ex th] + by auto + qed + next + case (Ex ex) + then show ?thesis + using t Ex_ConsE[of "[]" ex "e # t"] + by auto + qed +qed + +lemma Done_Traces_iff[simp]: "(Done a, t, m') \<in> Traces \<longleftrightarrow> t = [] \<and> m' = Done a" + by (auto elim: Traces_cases) + +lemma Fail_Traces_iff[simp]: "(Fail msg, t, m') \<in> Traces \<longleftrightarrow> t = [] \<and> m' = Fail msg" + by (auto elim: Traces_cases) + +lemma Exception_Traces_iff[simp]: "(Exception e, t, m') \<in> Traces \<longleftrightarrow> t = [] \<and> m' = Exception e" + by (auto elim: Traces_cases) + +lemma Read_reg_TracesE: + assumes "(Read_reg r k, t, m') \<in> Traces" + obtains (Nil) "t = []" and "m' = Read_reg r k" + | (Cons) v t' where "t = E_read_reg r v # t'" and "(k v, t', m') \<in> Traces" + using assms + by (auto elim: Traces_cases) + +lemma Write_reg_TracesE: + assumes "(Write_reg r v k, t, m') \<in> Traces" + obtains (Nil) "t = []" and "m' = Write_reg r v k" + | (Cons) t' where "t = E_write_reg r v # t'" and "(k, t', m') \<in> Traces" + using assms + by (auto elim: Traces_cases) + +lemma Write_ea_TracesE: + assumes "(Write_ea wk addr sz k, t, m') \<in> Traces" + obtains (Nil) "t = []" and "m' = Write_ea wk addr sz k" + | (Cons) t' where "t = E_write_ea wk addr sz # t'" and "(k, t', m') \<in> Traces" + using assms + by (auto elim: Traces_cases) + +lemma Write_memt_TracesE: + assumes "(Write_memt wk addr sz v tag k, t, m') \<in> Traces" + obtains (Nil) "t = []" and "m' = Write_memt wk addr sz v tag k" + | (Cons) t' r where "t = E_write_memt wk addr sz v tag r # t'" and "(k r, t', m') \<in> Traces" + using assms + by (auto elim: Traces_cases) + lemma Run_bindE: fixes m :: "('rv, 'b, 'e) monad" and a :: 'a assumes "Run (bind m f) t a" @@ -163,14 +341,6 @@ next qed qed -lemma Run_DoneE: - assumes "Run (Done a) t a'" - obtains "t = []" and "a' = a" - using assms by (auto elim: Traces.cases T.cases) - -lemma Run_Done_iff_Nil[simp]: "Run (Done a) t a' \<longleftrightarrow> t = [] \<and> a' = a" - by (auto elim: Run_DoneE) - lemma Run_bindE_ignore_trace: assumes "Run (m \<bind> f) t a" obtains tm tf am where "Run m tm am" and "Run (f am) tf a" @@ -205,8 +375,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 ba69d0d8..8b189f7a 100644 --- a/lib/isabelle/Sail2_state_lemmas.thy +++ b/lib/isabelle/Sail2_state_lemmas.thy @@ -2,6 +2,8 @@ theory Sail2_state_lemmas imports Sail2_state Sail2_state_lifting begin +text \<open>Monad lifting\<close> + lemma All_liftState_dom: "liftState_dom (r, m)" by (induction m) (auto intro: liftState.domintros) termination liftState using All_liftState_dom by auto @@ -18,7 +20,7 @@ lemma Value_liftState_Run: assumes "(Value a, s') \<in> liftState r m s" obtains t where "Run m t a" by (use assms in \<open>induction r m arbitrary: s s' rule: liftState.induct\<close>; - auto simp add: failS_def throwS_def returnS_def simp del: read_regvalS.simps; + simp add: failS_def throwS_def returnS_def del: read_regvalS.simps; blast elim: Value_bindS_elim) lemmas liftState_if_distrib[liftState_simp] = if_distrib[where f = "liftState ra" for ra] @@ -43,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" @@ -78,30 +83,44 @@ lemma liftState_bool_of_bitU_nondet[liftState_simp]: "liftState r (bool_of_bitU_nondet b) = bool_of_bitU_nondetS b" by (cases b; auto simp: bool_of_bitU_nondet_def bool_of_bitU_nondetS_def liftState_simp) -lemma liftState_read_mem_BC: - assumes "unsigned_method BC_bitU_list (bits_of_method BCa a) = unsigned_method BCa a" - shows "liftState r (read_mem BCa BCb rk a sz) = read_memS BCa BCb rk a sz" - using assms - by (auto simp: read_mem_def read_mem_bytes_def read_memS_def read_mem_bytesS_def maybe_failS_def liftState_simp split: option.splits) +lemma liftState_read_memt[liftState_simp]: + shows "liftState r (read_memt BCa BCb rk a sz) = read_memtS BCa BCb rk a sz" + by (auto simp: read_memt_def read_memt_bytes_def maybe_failS_def read_memtS_def + prod.case_distrib option.case_distrib[where h = "liftState r"] + option.case_distrib[where h = "\<lambda>c. c \<bind>\<^sub>S f" for f] liftState_simp + split: option.splits intro: bindS_cong) lemma liftState_read_mem[liftState_simp]: - "\<And>a. liftState r (read_mem BC_mword BC_mword rk a sz) = read_memS BC_mword BC_mword rk a sz" - "\<And>a. liftState r (read_mem BC_bitU_list BC_bitU_list rk a sz) = read_memS BC_bitU_list BC_bitU_list rk a sz" - by (auto simp: liftState_read_mem_BC) + shows "liftState r (read_mem BCa BCb rk a sz) = read_memS BCa BCb rk a sz" + by (auto simp: read_mem_def read_mem_bytes_def read_memS_def read_mem_bytesS_def maybe_failS_def + read_memtS_def + prod.case_distrib option.case_distrib[where h = "liftState r"] + option.case_distrib[where h = "\<lambda>c. c \<bind>\<^sub>S f" for f] liftState_simp + split: option.splits intro: bindS_cong) lemma liftState_write_mem_ea_BC: - assumes "unsigned_method BC_bitU_list (bits_of_method BCa a) = unsigned_method BCa a" - shows "liftState r (write_mem_ea BCa rk a sz) = write_mem_eaS BCa rk a (nat sz)" - using assms by (auto simp: write_mem_ea_def write_mem_eaS_def) + assumes "unsigned_method BCa a = Some a'" + shows "liftState r (write_mem_ea BCa rk a sz) = returnS ()" + using assms by (auto simp: write_mem_ea_def nat_of_bv_def maybe_fail_def) -lemma liftState_write_mem_ea[liftState_simp]: - "\<And>a. liftState r (write_mem_ea BC_mword rk a sz) = write_mem_eaS BC_mword rk a (nat sz)" - "\<And>a. liftState r (write_mem_ea BC_bitU_list rk a sz) = write_mem_eaS BC_bitU_list rk a (nat sz)" - by (auto simp: liftState_write_mem_ea_BC) +(*lemma liftState_write_mem_ea[liftState_simp]: + "\<And>a. liftState r (write_mem_ea BC_mword rk a sz) = returnS ()" + "\<And>a. liftState r (write_mem_ea BC_bitU_list rk a sz) = returnS ()" + by (auto simp: liftState_write_mem_ea_BC)*) -lemma liftState_write_mem_val[liftState_simp]: - "liftState r (write_mem_val BC v) = write_mem_valS BC v" - by (auto simp: write_mem_val_def write_mem_valS_def liftState_simp split: option.splits) +(*lemma write_mem_bytesS_def_BC_bitU_list_BC_mword[simp]: + "write_mem_bytesS BC_bitU_list wk (bits_of_method BC_mword addr) sz v t = + write_mem_bytesS BC_mword wk addr sz v t" + by (auto simp: write_mem_bytesS_def)*) + +lemma liftState_write_memt[liftState_simp]: + "liftState r (write_memt BCa BCv wk addr sz v t) = write_memtS BCa BCv wk addr sz v t" + by (auto simp: write_memt_def write_memtS_def liftState_simp split: option.splits) + +lemma liftState_write_mem[liftState_simp]: + "liftState r (write_mem BCa BCv wk addr sz v) = write_memS BCa BCv wk addr sz v" + by (auto simp: write_mem_def write_memS_def write_memtS_def write_mem_bytesS_def liftState_simp + split: option.splits) lemma liftState_read_reg_readS: assumes "\<And>s. Option.bind (get_regval' (name reg) s) (of_regval reg) = Some (read_from reg s)" @@ -138,6 +157,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 @@ -146,6 +173,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) @@ -301,7 +329,7 @@ proof (use assms in \<open>induction vars "liftState r \<circ> cond" "liftState qed auto qed -(* Simplification rules for monadic Boolean connectives *) +text \<open>Simplification rules for monadic Boolean connectives\<close> lemma if_return_return[simp]: "(if a then return True else return False) = return a" by auto @@ -384,4 +412,125 @@ lemma Run_and_boolM_E: lemma maybe_failS_Some[simp]: "maybe_failS msg (Some v) = returnS v" by (auto simp: maybe_failS_def) +text \<open>Event traces\<close> + +lemma Some_eq_bind_conv: "Some x = Option.bind f g \<longleftrightarrow> (\<exists>y. f = Some y \<and> g y = Some x)" + unfolding bind_eq_Some_conv[symmetric] by auto + +lemma if_then_Some_eq_Some_iff: "((if b then Some x else None) = Some y) \<longleftrightarrow> (b \<and> y = x)" + by auto + +lemma Some_eq_if_then_Some_iff: "(Some y = (if b then Some x else None)) \<longleftrightarrow> (b \<and> y = x)" + by auto + +lemma emitEventS_update_cases: + assumes "emitEventS ra e s = Some s'" + obtains + (Write_mem) wk addr sz v tag r + where "e = E_write_memt wk addr sz v tag r \<or> (e = E_write_mem wk addr sz v r \<and> tag = B0)" + and "s' = put_mem_bytes addr sz v tag s" + | (Write_reg) r v rs' + where "e = E_write_reg r v" and "(snd ra) r v (regstate s) = Some rs'" + and "s' = s\<lparr>regstate := rs'\<rparr>" + | (Read) "s' = s" + using assms + by (elim emitEventS.elims) + (auto simp: Some_eq_bind_conv bind_eq_Some_conv if_then_Some_eq_Some_iff Some_eq_if_then_Some_iff) + +lemma runTraceS_singleton[simp]: "runTraceS ra [e] s = emitEventS ra e s" + by (cases "emitEventS ra e s"; auto) + +lemma runTraceS_ConsE: + assumes "runTraceS ra (e # t) s = Some s'" + obtains s'' where "emitEventS ra e s = Some s''" and "runTraceS ra t s'' = Some s'" + using assms by (auto simp: bind_eq_Some_conv) + +lemma runTraceS_ConsI: + assumes "emitEventS ra e s = Some s'" and "runTraceS ra t s' = Some s''" + shows "runTraceS ra (e # t) s = Some s''" + using assms by auto + +lemma runTraceS_Cons_tl: + assumes "emitEventS ra e s = Some s'" + shows "runTraceS ra (e # t) s = runTraceS ra t s'" + using assms by (elim emitEventS.elims) (auto simp: Some_eq_bind_conv bind_eq_Some_conv) + +lemma runTraceS_appendE: + assumes "runTraceS ra (t @ t') s = Some s'" + obtains s'' where "runTraceS ra t s = Some s''" and "runTraceS ra t' s'' = Some s'" +proof - + have "\<exists>s''. runTraceS ra t s = Some s'' \<and> runTraceS ra t' s'' = Some s'" + proof (use assms in \<open>induction t arbitrary: s\<close>) + case (Cons e t) + from Cons.prems + obtain s_e where "emitEventS ra e s = Some s_e" and "runTraceS ra (t @ t') s_e = Some s'" + by (auto elim: runTraceS_ConsE simp: bind_eq_Some_conv) + with Cons.IH[of s_e] show ?case by (auto intro: runTraceS_ConsI) + qed auto + then show ?thesis using that by blast +qed + +lemma runTraceS_nth_split: + assumes "runTraceS ra t s = Some s'" and n: "n < length t" + obtains s1 s2 where "runTraceS ra (take n t) s = Some s1" + and "emitEventS ra (t ! n) s1 = Some s2" + and "runTraceS ra (drop (Suc n) t) s2 = Some s'" +proof - + have "runTraceS ra (take n t @ t ! n # drop (Suc n) t) s = Some s'" + using assms + by (auto simp: id_take_nth_drop[OF n, symmetric]) + then show thesis by (blast elim: runTraceS_appendE runTraceS_ConsE intro: that) +qed + +text \<open>Memory accesses\<close> + +lemma get_mem_bytes_put_mem_bytes_same_addr: + assumes "length v = sz" + shows "get_mem_bytes addr sz (put_mem_bytes addr sz v tag s) = Some (v, if sz > 0 then tag else B1)" +proof (unfold assms[symmetric], induction v rule: rev_induct) + case Nil + then show ?case by (auto simp: get_mem_bytes_def) +next + case (snoc x xs) + then show ?case + by (cases tag) + (auto simp: get_mem_bytes_def put_mem_bytes_def Let_def and_bit_eq_iff foldl_and_bit_eq_iff + cong: option.case_cong split: if_splits option.splits) +qed + +lemma memstate_put_mem_bytes: + assumes "length v = sz" + shows "memstate (put_mem_bytes addr sz v tag s) addr' = + (if addr' \<in> {addr..<addr+sz} then Some (v ! (addr' - addr)) else memstate s addr')" + unfolding assms[symmetric] + by (induction v rule: rev_induct) (auto simp: put_mem_bytes_def nth_Cons nth_append Let_def) + +lemma tagstate_put_mem_bytes: + assumes "length v = sz" + shows "tagstate (put_mem_bytes addr sz v tag s) addr' = + (if addr' \<in> {addr..<addr+sz} then Some tag else tagstate s addr')" + unfolding assms[symmetric] + by (induction v rule: rev_induct) (auto simp: put_mem_bytes_def nth_Cons nth_append Let_def) + +lemma get_mem_bytes_cong: + assumes "\<forall>addr'. addr \<le> addr' \<and> addr' < addr + sz \<longrightarrow> + (memstate s' addr' = memstate s addr' \<and> tagstate s' addr' = tagstate s addr')" + shows "get_mem_bytes addr sz s' = get_mem_bytes addr sz s" +proof (use assms in \<open>induction sz\<close>) + case 0 + then show ?case by (auto simp: get_mem_bytes_def) +next + case (Suc sz) + then show ?case + by (auto simp: get_mem_bytes_def Let_def + intro!: map_option_cong map_cong foldl_cong + arg_cong[where f = just_list] arg_cong2[where f = and_bit]) +qed + +lemma get_mem_bytes_tagged_tagstate: + assumes "get_mem_bytes addr sz s = Some (v, B1)" + shows "\<forall>addr' \<in> {addr..<addr + sz}. tagstate s addr' = Some B1" + using assms + by (auto simp: get_mem_bytes_def foldl_and_bit_eq_iff Let_def split: option.splits) + end diff --git a/lib/isabelle/Sail2_state_monad_lemmas.thy b/lib/isabelle/Sail2_state_monad_lemmas.thy index 3a286c10..1e9f50cc 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,31 +197,37 @@ 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 = option.case_distrib[where h = "\<lambda>c. ignore_throw c s" and option = "c s" for c s] + option.case_distrib[where h = "\<lambda>c. ignore_throw c" and option = "c" for c] + +lemma ignore_throw_let_distrib: "ignore_throw (let x = y in f x) = (let x = y in ignore_throw (f x))" + by auto lemma no_throw_mem_builtins: - "\<And>BC rk a sz s. ignore_throw (read_mem_bytesS BC rk a sz) s = read_mem_bytesS BC rk a sz s" + "\<And>rk a sz s. ignore_throw (read_mem_bytesS rk a sz) s = read_mem_bytesS rk a sz s" + "\<And>rk a sz s. ignore_throw (read_memt_bytesS rk a sz) s = read_memt_bytesS rk a sz s" "\<And>BC a s. ignore_throw (read_tagS BC a) s = read_tagS BC a s" - "\<And>BC wk a sz s. ignore_throw (write_mem_eaS BC wk a sz) s = write_mem_eaS BC wk a sz s" - "\<And>v s. ignore_throw (write_mem_bytesS v) s = write_mem_bytesS v s" - "\<And>BC v s. ignore_throw (write_mem_valS BC v) s = write_mem_valS BC v s" - "\<And>BC a t s. ignore_throw (write_tagS BC a t) s = write_tagS BC a t s" + "\<And>BCa BCv rk a sz s. ignore_throw (read_memS BCa BCv rk a sz) s = read_memS BCa BCv rk a sz s" + "\<And>BCa BCv rk a sz s. ignore_throw (read_memtS BCa BCv rk a sz) s = read_memtS BCa BCv rk a sz s" + "\<And>BC wk addr sz v s. ignore_throw (write_mem_bytesS wk addr sz v) s = write_mem_bytesS wk addr sz v s" + "\<And>BC wk addr sz v t s. ignore_throw (write_memt_bytesS wk addr sz v t) s = write_memt_bytesS wk addr sz v t s" + "\<And>BCa BCv wk addr sz v s. ignore_throw (write_memS BCa BCv wk addr sz v) s = write_memS BCa BCv wk addr sz v s" + "\<And>BCa BCv wk addr sz v t s. ignore_throw (write_memtS BCa BCv wk addr sz v t) s = write_memtS BCa BCv wk addr sz v t s" "\<And>s. ignore_throw (excl_resultS ()) s = excl_resultS () s" "\<And>s. ignore_throw (undefined_boolS ()) s = undefined_boolS () s" - unfolding read_mem_bytesS_def read_memS_def read_tagS_def write_mem_eaS_def - unfolding write_mem_valS_def write_mem_bytesS_def write_tagS_def - unfolding excl_resultS_def undefined_boolS_def + unfolding read_mem_bytesS_def read_memt_bytesS_def read_memtS_def read_memS_def read_tagS_def + unfolding write_memS_def write_memtS_def write_mem_bytesS_def write_memt_bytesS_def + unfolding excl_resultS_def undefined_boolS_def maybe_failS_def + unfolding ignore_throw_bindS by (auto cong: bindS_cong bindS_ext_cong ignore_throw_cong option.case_cong - simp: option.case_distrib prod.case_distrib ignore_throw_option_case_distrib comp_def) - -lemma no_throw_read_memS: "ignore_throw (read_memS BCa BCb rk a sz) s = read_memS BCa BCb rk a sz s" - by (auto simp: read_memS_def no_throw_mem_builtins cong: bindS_ext_cong) + simp: prod.case_distrib ignore_throw_option_case_distrib ignore_throw_let_distrib comp_def) lemma no_throw_read_regvalS: "ignore_throw (read_regvalS r reg_name) s = read_regvalS r reg_name s" by (cases r) (auto simp: option.case_distrib cong: bindS_cong option.case_cong) @@ -231,7 +236,7 @@ lemma no_throw_write_regvalS: "ignore_throw (write_regvalS r reg_name v) s = wri by (cases r) (auto simp: option.case_distrib cong: bindS_cong option.case_cong) lemmas no_throw_builtins[simp] = - no_throw_mem_builtins no_throw_read_regvalS no_throw_write_regvalS no_throw_read_memS + no_throw_mem_builtins no_throw_read_regvalS no_throw_write_regvalS (* end *) diff --git a/lib/isabelle/Sail2_values_lemmas.thy b/lib/isabelle/Sail2_values_lemmas.thy index 576cd8ea..27a6952f 100644 --- a/lib/isabelle/Sail2_values_lemmas.thy +++ b/lib/isabelle/Sail2_values_lemmas.thy @@ -123,6 +123,9 @@ lemma nth_upto[simp]: "i + int n \<le> j \<Longrightarrow> [i..j] ! n = i + int declare index_list.simps[simp del] +lemma genlist_add_upt[simp]: "genlist ((+) start) len = [start..<start + len]" + by (auto simp: genlist_def map_add_upt add.commute cong: map_cong) + lemma just_list_map_Some[simp]: "just_list (map Some v) = Some v" by (induction v) auto lemma just_list_None_iff[simp]: "just_list xs = None \<longleftrightarrow> None \<in> set xs" @@ -151,6 +154,31 @@ next then show ?case by (auto simp: repeat.simps) qed +lemma and_bit_B1[simp]: "and_bit B1 b = b" + by (cases b) auto + +lemma and_bit_idem[simp]: "and_bit b b = b" + by (cases b) auto + +lemma and_bit_eq_iff: + "and_bit b b' = B0 \<longleftrightarrow> (b = B0 \<or> b' = B0)" + "and_bit b b' = BU \<longleftrightarrow> (b = BU \<or> b' = BU) \<and> b \<noteq> B0 \<and> b' \<noteq> B0" + "and_bit b b' = B1 \<longleftrightarrow> (b = B1 \<and> b' = B1)" + by (cases b; cases b'; auto)+ + +lemma foldl_and_bit_eq_iff: + shows "foldl and_bit b bs = B0 \<longleftrightarrow> (b = B0 \<or> B0 \<in> set bs)" (is ?B0) + and "foldl and_bit b bs = B1 \<longleftrightarrow> (b = B1 \<and> set bs \<subseteq> {B1})" (is ?B1) + and "foldl and_bit b bs = BU \<longleftrightarrow> (b = BU \<or> BU \<in> set bs) \<and> b \<noteq> B0 \<and> B0 \<notin> set bs" (is ?BU) +proof - + have "?B0 \<and> ?B1 \<and> ?BU" + proof (induction bs arbitrary: b) + case (Cons b' bs) + show ?case using Cons.IH by (cases b; cases b') auto + qed auto + then show ?B0 and ?B1 and ?BU by auto +qed + lemma bool_of_bitU_simps[simp]: "bool_of_bitU B0 = Some False" "bool_of_bitU B1 = Some True" |