diff options
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/isabelle/Prompt_monad_extras.thy | 43 | ||||
| -rw-r--r-- | lib/isabelle/ROOT | 2 | ||||
| -rw-r--r-- | lib/isabelle/Sail_values_extras.thy | 52 | ||||
| -rw-r--r-- | lib/isabelle/State_extras.thy | 181 | ||||
| -rw-r--r-- | lib/isabelle/State_monad_extras.thy | 119 |
5 files changed, 367 insertions, 30 deletions
diff --git a/lib/isabelle/Prompt_monad_extras.thy b/lib/isabelle/Prompt_monad_extras.thy index e93c6052..9d29f5a2 100644 --- a/lib/isabelle/Prompt_monad_extras.thy +++ b/lib/isabelle/Prompt_monad_extras.thy @@ -1,5 +1,7 @@ theory Prompt_monad_extras - imports Prompt_monad + imports + Prompt_monad + Sail_values_extras begin lemma All_bind_dom: "bind_dom (m, f)" @@ -21,14 +23,18 @@ lemmas try_catch_induct[case_names Done Read_mem Write_memv Read_reg Excl_res Wr datatype 'regval event = (* Request to read memory *) - e_read_mem read_kind int int "memory_byte list" + 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 int int + | 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_tagv bitU bool + (* Tell the system to dynamically recalculate dependency footprint *) + | e_footprint (* Request a memory barrier *) | e_barrier " barrier_kind " (* Request to read register *) @@ -38,9 +44,12 @@ datatype 'regval event = 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_tagv: "((Write_tagv v k), e_write_tagv 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" @@ -59,6 +68,29 @@ 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 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_tagv) val k t' v where "m = Write_tagv val k" and "t = e_write_tagv 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" +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) +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" @@ -114,11 +146,6 @@ lemma Run_DoneE: lemma Run_Done_iff_Nil[simp]: "Run (Done a) t a' \<longleftrightarrow> t = [] \<and> a' = a" by (auto elim: Run_DoneE) -lemma Run_BarrierE[elim!]: - assumes "Run (Barrier bk k) t a" - obtains t' where "t = e_barrier bk # t'" and "Run k t' a" - using assms by cases (auto elim: T.cases) - lemma bind_cong[fundef_cong]: assumes m: "m1 = m2" and f: "\<And>t a. Run m2 t a \<Longrightarrow> f1 a = f2 a" diff --git a/lib/isabelle/ROOT b/lib/isabelle/ROOT index d826ea08..b07bc807 100644 --- a/lib/isabelle/ROOT +++ b/lib/isabelle/ROOT @@ -1,7 +1,7 @@ session "Sail" = "LEM" + options [document = false] theories - Sail_values + Sail_values_extras Prompt State_extras Sail_operators_mwords diff --git a/lib/isabelle/Sail_values_extras.thy b/lib/isabelle/Sail_values_extras.thy new file mode 100644 index 00000000..66bcba48 --- /dev/null +++ b/lib/isabelle/Sail_values_extras.thy @@ -0,0 +1,52 @@ +theory Sail_values_extras + imports Sail_values +begin + +termination reverse_endianness_list by (lexicographic_order simp add: drop_list_def) + +termination index_list + by (relation "measure (\<lambda>(i, j, step). nat ((j - i + step) * sgn step))") auto + +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" + by (induction xs) (auto split: option.splits) + +lemma just_list_Some_iff[simp]: "just_list xs = Some ys \<longleftrightarrow> xs = map Some ys" + by (induction xs arbitrary: ys) (auto split: option.splits) + +lemma just_list_cases: + assumes "just_list xs = y" + obtains (None) "None \<in> set xs" and "y = None" + | (Some) ys where "xs = map Some ys" and "y = Some ys" + using assms by (cases y) auto + +abbreviation "BC_bitU_list \<equiv> instance_Sail_values_Bitvector_list_dict instance_Sail_values_BitU_Sail_values_bitU_dict" +lemmas BC_bitU_list_def = instance_Sail_values_Bitvector_list_dict_def instance_Sail_values_BitU_Sail_values_bitU_dict_def +abbreviation "BC_mword \<equiv> instance_Sail_values_Bitvector_Machine_word_mword_dict" +lemmas BC_mword_def = instance_Sail_values_Bitvector_Machine_word_mword_dict_def + +lemma image_bitU_of_bool_B0_B1: "bitU_of_bool ` bs \<subseteq> {B0, B1}" + by (auto simp: bitU_of_bool_def split: if_splits) + +lemma bool_of_bitU_bitU_of_bool[simp]: "bool_of_bitU \<circ> bitU_of_bool = id" + by (intro ext) (auto simp: bool_of_bitU_def bitU_of_bool_def) + +lemma nat_of_bits_aux_bl_to_bin_aux: + assumes "set bs \<subseteq> {B0, B1}" + shows "nat_of_bits_aux acc bs = nat (bl_to_bin_aux (map bool_of_bitU bs) (int acc))" + by (use assms in \<open>induction acc bs rule: nat_of_bits_aux.induct\<close>) + (auto simp: Bit_def bool_of_bitU_def intro!: arg_cong[where f = nat] arg_cong2[where f = bl_to_bin_aux]) + +lemma nat_of_bits_bl_to_bin[simp]: "nat_of_bits (map bitU_of_bool bs) = nat (bl_to_bin bs)" + by (auto simp: nat_of_bits_def bl_to_bin_def nat_of_bits_aux_bl_to_bin_aux image_bitU_of_bool_B0_B1) + +lemma unsigned_bits_of_mword: + "unsigned_method BC_bitU_list (bits_of_method BC_mword a) = unsigned_method BC_mword a" + by (auto simp: BC_bitU_list_def BC_mword_def unsigned_of_bits_def) + +lemma unsigned_bits_of_bitU_list: + "unsigned_method BC_bitU_list (bits_of_method BC_bitU_list a) = unsigned_method BC_bitU_list a" + by (auto simp: BC_bitU_list_def) + +end diff --git a/lib/isabelle/State_extras.thy b/lib/isabelle/State_extras.thy index 096fb19b..924861b0 100644 --- a/lib/isabelle/State_extras.thy +++ b/lib/isabelle/State_extras.thy @@ -4,32 +4,187 @@ begin lemma All_liftState_dom: "liftState_dom (r, m)" by (induction m) (auto intro: liftState.domintros) - termination liftState using All_liftState_dom by auto +lemma liftState_bind[simp]: + "liftState r (bind m f) = bindS (liftState r m) (liftState r \<circ> f)" + by (induction m f rule: bind.induct) auto + lemma liftState_return[simp]: "liftState r (return a) = returnS a" by (auto simp: return_def) + +lemma Value_liftState_Run: + assumes "(Value a, s') \<in> set (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; + blast elim: Value_bindS_elim) + lemma liftState_throw[simp]: "liftState r (throw e) = throwS e" by (auto simp: throw_def) lemma liftState_assert[simp]: "liftState r (assert_exp c msg) = assert_expS c msg" by (auto simp: assert_exp_def assert_expS_def) +lemma liftState_exit[simp]: "liftState r (exit0 ()) = exitS ()" by (auto simp: exit0_def exitS_def) +lemma liftState_exclResult[simp]: "liftState r (excl_result ()) = excl_resultS ()" by (auto simp: excl_result_def) +lemma liftState_barrier[simp]: "liftState r (barrier bk) = returnS ()" by (auto simp: barrier_def) +lemma liftState_footprint[simp]: "liftState r (footprint ()) = returnS ()" by (auto simp: footprint_def) -lemma liftState_bind[simp]: - "liftState r (bind m f) = bindS (liftState r m) (liftState r \<circ> f)" - by (induction m f rule: bind.induct) auto +lemma liftState_try_catch[simp]: + "liftState r (try_catch m h) = try_catchS (liftState r m) (liftState r \<circ> h)" + by (induction m h rule: try_catch_induct) (auto simp: try_catchS_bindS_no_throw) + +lemma liftState_early_return[simp]: + "liftState r (early_return r) = early_returnS r" + by (auto simp: early_return_def early_returnS_def) + +lemma liftState_catch_early_return[simp]: + "liftState r (catch_early_return m) = catch_early_returnS (liftState r m)" + by (auto simp: catch_early_return_def catch_early_returnS_def sum.case_distrib cong: sum.case_cong) + +lemma liftState_liftR[simp]: + "liftState r (liftR m) = liftSR (liftState r m)" + by (auto simp: liftR_def liftSR_def) + +lemma liftState_try_catchR[simp]: + "liftState r (try_catchR m h) = try_catchSR (liftState r m) (liftState r \<circ> h)" + by (auto simp: try_catchR_def try_catchSR_def sum.case_distrib cong: sum.case_cong) + +lemma liftState_read_mem_BC[simp]: + 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_memS_def read_mem_bytesS_def) +lemmas liftState_read_mem[simp] = + liftState_read_mem_BC[OF unsigned_bits_of_mword] liftState_read_mem_BC[OF unsigned_bits_of_bitU_list] + +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 sz" + using assms by (auto simp: write_mem_ea_def write_mem_eaS_def) +lemmas liftState_write_mem_ea[simp] = + liftState_write_mem_ea_BC[OF unsigned_bits_of_mword] liftState_write_mem_ea_BC[OF unsigned_bits_of_bitU_list] -lemma liftState_read_reg[intro]: +lemma liftState_write_mem_val: + "liftState r (write_mem_val BC v) = write_mem_valS BC v" + by (auto simp: write_mem_val_def write_mem_valS_def 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)" - shows "liftState (get_regval', set_regval') (read_reg reg) = read_regS reg" + shows "liftState (get_regval', set_regval') (read_reg reg) = readS (read_from reg \<circ> regstate)" proof fix s :: "'a sequential_state" obtain rv v where "get_regval' (name reg) (regstate s) = Some rv" - and "of_regval reg rv = Some v" and "read_from reg (regstate s) = v" + and "of_regval reg rv \<equiv> Some v" and "read_from reg (regstate s) = v" using assms unfolding bind_eq_Some_conv by blast - then show "liftState (get_regval', set_regval') (read_reg reg) s = read_regS reg s" - by (auto simp: read_reg_def bindS_def returnS_def read_regS_def) + then show "liftState (get_regval', set_regval') (read_reg reg) s = readS (read_from reg \<circ> regstate) s" + by (auto simp: read_reg_def bindS_def returnS_def read_regS_def readS_def) +qed + +lemma liftState_write_reg_updateS: + assumes "\<And>s. set_regval' (name reg) (regval_of reg v) s = Some (write_to reg v s)" + shows "liftState (get_regval', set_regval') (write_reg reg v) = updateS (regstate_update (write_to reg v))" + using assms by (auto simp: write_reg_def bindS_readS updateS_def returnS_def) + +lemma liftState_iter_aux[simp]: + shows "liftState r (iter_aux i f xs) = iterS_aux i (\<lambda>i x. liftState r (f i x)) xs" + by (induction i "\<lambda>i x. liftState r (f i x)" xs rule: iterS_aux.induct) (auto cong: bindS_cong) + +lemma liftState_iteri[simp]: + "liftState r (iteri f xs) = iteriS (\<lambda>i x. liftState r (f i x)) xs" + by (auto simp: iteri_def iteriS_def) + +lemma liftState_iter[simp]: + "liftState r (iter f xs) = iterS (liftState r \<circ> f) xs" + by (auto simp: iter_def iterS_def) + +lemma liftState_foreachM[simp]: + "liftState r (foreachM xs vars body) = foreachS xs vars (\<lambda>x vars. liftState r (body x vars))" + by (induction xs vars "\<lambda>x vars. liftState r (body x vars)" rule: foreachS.induct) + (auto cong: bindS_cong) + +lemma whileS_dom_step: + assumes "whileS_dom (vars, cond, body, s)" + and "(Value True, s') \<in> set (cond vars s)" + and "(Value vars', s'') \<in> set (body vars s')" + shows "whileS_dom (vars', cond, body, s'')" + by (use assms in \<open>induction vars cond body s arbitrary: vars' s' s'' rule: whileS.pinduct\<close>) + (auto intro: whileS.domintros) + +lemma whileM_dom_step: + assumes "whileM_dom (vars, cond, body)" + and "Run (cond vars) t True" + and "Run (body vars) t' vars'" + shows "whileM_dom (vars', cond, body)" + by (use assms in \<open>induction vars cond body arbitrary: vars' t t' rule: whileM.pinduct\<close>) + (auto intro: whileM.domintros) + +lemma whileM_dom_ex_step: + assumes "whileM_dom (vars, cond, body)" + and "\<exists>t. Run (cond vars) t True" + and "\<exists>t'. Run (body vars) t' vars'" + shows "whileM_dom (vars', cond, body)" + using assms by (blast intro: whileM_dom_step) + +lemmas whileS_pinduct = whileS.pinduct[case_names Step] + +lemma liftState_whileM: + assumes "whileS_dom (vars, liftState r \<circ> cond, liftState r \<circ> body, s)" + and "whileM_dom (vars, cond, body)" + shows "liftState r (whileM vars cond body) s = whileS vars (liftState r \<circ> cond) (liftState r \<circ> body) s" +proof (use assms in \<open>induction vars "liftState r \<circ> cond" "liftState r \<circ> body" s rule: whileS.pinduct\<close>) + case Step: (1 vars s) + note domS = Step(1) and IH = Step(2) and domM = Step(3) + show ?case unfolding whileS.psimps[OF domS] whileM.psimps[OF domM] liftState_bind + proof (intro bindS_ext_cong, goal_cases cond while) + case (while a s') + have "bindS (liftState r (body vars)) (liftState r \<circ> (\<lambda>vars. whileM vars cond body)) s' = + bindS (liftState r (body vars)) (\<lambda>vars. whileS vars (liftState r \<circ> cond) (liftState r \<circ> body)) s'" + if "a" + proof (intro bindS_ext_cong, goal_cases body while') + case (while' vars' s'') + have "whileM_dom (vars', cond, body)" proof (rule whileM_dom_ex_step[OF domM]) + show "\<exists>t. Run (cond vars) t True" using while that by (auto elim: Value_liftState_Run) + show "\<exists>t'. Run (body vars) t' vars'" using while' that by (auto elim: Value_liftState_Run) + qed + then show ?case using while while' that by (auto intro: IH) + qed auto + then show ?case by auto + qed auto qed -lemma liftState_write_reg[intro]: - assumes "\<And>s. set_regval' (name reg) (regval_of reg v) s = Some (write_to reg s v)" - shows "liftState (get_regval', set_regval') (write_reg reg v) = write_regS reg v" - using assms by (auto simp: write_reg_def bindS_def returnS_def write_regS_def) + +lemma untilM_dom_step: + assumes "untilM_dom (vars, cond, body)" + and "Run (body vars) t vars'" + and "Run (cond vars') t' False" + shows "untilM_dom (vars', cond, body)" + by (use assms in \<open>induction vars cond body arbitrary: vars' t t' rule: untilM.pinduct\<close>) + (auto intro: untilM.domintros) + +lemma untilM_dom_ex_step: + assumes "untilM_dom (vars, cond, body)" + and "\<exists>t. Run (body vars) t vars'" + and "\<exists>t'. Run (cond vars') t' False" + shows "untilM_dom (vars', cond, body)" + using assms by (blast intro: untilM_dom_step) + +lemma liftState_untilM: + assumes "untilS_dom (vars, liftState r \<circ> cond, liftState r \<circ> body, s)" + and "untilM_dom (vars, cond, body)" + shows "liftState r (untilM vars cond body) s = untilS vars (liftState r \<circ> cond) (liftState r \<circ> body) s" +proof (use assms in \<open>induction vars "liftState r \<circ> cond" "liftState r \<circ> body" s rule: untilS.pinduct\<close>) + case Step: (1 vars s) + note domS = Step(1) and IH = Step(2) and domM = Step(3) + show ?case unfolding untilS.psimps[OF domS] untilM.psimps[OF domM] liftState_bind + proof (intro bindS_ext_cong, goal_cases body k) + case (k vars' s') + show ?case unfolding comp_def liftState_bind + proof (intro bindS_ext_cong, goal_cases cond until) + case (until a s'') + have "untilM_dom (vars', cond, body)" if "\<not>a" + proof (rule untilM_dom_ex_step[OF domM]) + show "\<exists>t. Run (body vars) t vars'" using k by (auto elim: Value_liftState_Run) + show "\<exists>t'. Run (cond vars') t' False" using until that by (auto elim: Value_liftState_Run) + qed + then show ?case using k until IH by (auto simp: comp_def) + qed auto + qed auto +qed end diff --git a/lib/isabelle/State_monad_extras.thy b/lib/isabelle/State_monad_extras.thy index eb8ed678..406aec79 100644 --- a/lib/isabelle/State_monad_extras.thy +++ b/lib/isabelle/State_monad_extras.thy @@ -1,15 +1,22 @@ theory State_monad_extras - imports State_monad + imports + State_monad + Sail_values_extras +begin + +context + notes returnS_def[simp] and failS_def[simp] and throwS_def[simp] and readS_def[simp] and updateS_def[simp] begin abbreviation "bindS_aux f \<equiv> (\<lambda>r. case r of (Value a, s') \<Rightarrow> f a s' | (Ex e, s') \<Rightarrow> [(Ex e, s')])" +abbreviation "bindS_app ms f \<equiv> List.concat (List.map (bindS_aux f) ms)" lemma bindS_ext_cong[fundef_cong]: assumes m: "m1 s = m2 s" and f: "\<And>a s'. (Value a, s') \<in> set (m2 s) \<Longrightarrow> f1 a s' = f2 a s'" - shows "(bindS m1 f1) s = (bindS m2 f2) s" + shows "bindS m1 f1 s = bindS m2 f2 s" proof - - have "List.concat (map (bindS_aux f1) (m2 s)) = List.concat (map (bindS_aux f2) (m2 s))" + have "bindS_app (m2 s) f1 = bindS_app (m2 s) f2" using f by (intro arg_cong[where f = List.concat]) (auto intro: map_ext split: result.splits) then show ?thesis using m by (auto simp: bindS_def) qed @@ -20,8 +27,21 @@ lemma bindS_cong[fundef_cong]: shows "bindS m1 f1 = bindS m2 f2" using assms by (blast intro: bindS_ext_cong) -lemma bindS_returnS[simp]: "bindS (returnS x) m = m x" - by (auto simp add: bindS_def returnS_def) +lemma bindS_returnS_left[simp]: "bindS (returnS x) f = f x" + by (auto simp add: bindS_def) + +lemma bindS_returnS_right[simp]: "bindS m returnS = (m :: ('regs, 'a, 'e) monadS)" +proof - + have "List.concat (map (bindS_aux returnS) ms) = ms" for ms :: "(('a, 'e) result \<times> 'regs sequential_state) list" + by (induction ms) (auto split: result.splits) + then show ?thesis unfolding bindS_def by blast +qed + +lemma bindS_readS: "bindS (readS f) m = (\<lambda>s. m (f s) s)" + by (auto simp: bindS_def) + +lemma bindS_updateS: "bindS (updateS f) m = (\<lambda>s. m () (f s))" + by (auto simp: bindS_def) lemma bindS_assoc[simp]: "bindS (bindS m f) g = bindS m (\<lambda>x. bindS (f x) g)" proof - @@ -31,13 +51,96 @@ proof - then show ?thesis unfolding bindS_def by auto qed -lemma bindS_failS[simp]: "bindS (failS msg) f = failS msg" by (auto simp: bindS_def failS_def) -lemma bindS_throwS[simp]: "bindS (throwS e) f = throwS e" by (auto simp: bindS_def throwS_def) +lemma bindS_failS[simp]: "bindS (failS msg) f = failS msg" by (auto simp: bindS_def) +lemma bindS_throwS[simp]: "bindS (throwS e) f = throwS e" by (auto simp: bindS_def) declare seqS_def[simp] +lemma Value_bindS_elim: + assumes "(Value a, s') \<in> set (bindS m f s)" + obtains s'' a' where "(Value a', s'') \<in> set (m s)" and "(Value a, s') \<in> set (f a' s'')" + using assms by (auto simp: bindS_def; split result.splits; auto) + +abbreviation + "try_catchS_aux h r \<equiv> + (case r of + (Value a, s') => returnS a s' + | (Ex (Throw e), s') => h e s' + | (Ex (Failure msg), s') => [(Ex (Failure msg), s')])" +abbreviation "try_catchS_app ms h \<equiv> List.concat (List.map (try_catchS_aux h) ms)" + lemma try_catchS_returnS[simp]: "try_catchS (returnS a) h = returnS a" and try_catchS_failS[simp]: "try_catchS (failS msg) h = failS msg" and try_catchS_throwS[simp]: "try_catchS (throwS e) h = h e" - by (auto simp: returnS_def failS_def throwS_def try_catchS_def) + by (auto simp: try_catchS_def) + +lemma try_catchS_cong[cong]: + assumes "\<And>s. m1 s = m2 s" and "\<And>e s. h1 e s = h2 e s" + shows "try_catchS m1 h1 = try_catchS m2 h2" + using assms by (intro arg_cong2[where f = try_catchS] ext) auto + +fun ignore_throw_app :: "(('a, 'e1) result \<times> 's) list \<Rightarrow> (('a, 'e2) result \<times> 's) list" where + "ignore_throw_app [] = []" +| "ignore_throw_app ((Value a, s) # ms) = (Value a, s) # ignore_throw_app ms" +| "ignore_throw_app ((Ex (Failure msg), s) # ms) = (Ex (Failure msg), s) # ignore_throw_app ms" +| "ignore_throw_app ((Ex (Throw e), s) # ms) = ignore_throw_app ms" +abbreviation ignore_throw :: "('r, 'a, 'e1) monadS \<Rightarrow> ('r, 'a, 'e2) monadS" where + "ignore_throw m \<equiv> \<lambda>s. ignore_throw_app (m s)" + +lemma [simp]: "ignore_throw_app ms = (Ex (Throw e), s) # ms' \<longleftrightarrow> False" + by (induction ms rule: ignore_throw_app.induct) auto + +lemma ignore_throw_app_append[simp]: + "ignore_throw_app (ms1 @ ms2) = ignore_throw_app ms1 @ ignore_throw_app ms2" + by (induction ms1 rule: ignore_throw_app.induct) auto + +lemma ignore_throw_app_bindS_app[simp]: + "ignore_throw_app (bindS_app ms f) = bindS_app (ignore_throw_app ms) (ignore_throw \<circ> f)" + by (induction ms rule: ignore_throw_app.induct) (auto split: result.splits) + +lemma ignore_throw_bindS[simp]: + "ignore_throw (bindS m f) = bindS (ignore_throw m) (ignore_throw \<circ> f)" + "ignore_throw (bindS m f) s = bindS (ignore_throw m) (ignore_throw \<circ> f) s" + unfolding bindS_def by auto + +lemma try_catchS_bindS_no_throw: + fixes m1 :: "('r, 'a, 'e1) monadS" and m2 :: "('r, 'a, 'e2) monadS" + assumes m1: "\<And>s. ignore_throw m1 s = m1 s" + and m2: "\<And>s. ignore_throw m1 s = m2 s" + shows "try_catchS (bindS m1 f) h = bindS m2 (\<lambda>a. try_catchS (f a) h)" +proof + fix s + have 1: "try_catchS_app (bindS_app ms f) h = + bindS_app (ignore_throw_app ms) (\<lambda>a s'. try_catchS_app (f a s') h)" + if "ignore_throw_app ms = ms" for ms + using that by (induction ms rule: ignore_throw_app.induct) auto + then show "try_catchS (bindS m1 f) h s = bindS m2 (\<lambda>a. try_catchS (f a) h) s" + using m1 unfolding try_catchS_def bindS_def m2[symmetric] by blast +qed + +lemma no_throw_mem_builtins: + "\<And>a. ignore_throw (returnS a) = returnS a" + "\<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>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>t s. ignore_throw (write_tagS t) s = write_tagS t s" + "\<And>s. ignore_throw (excl_resultS ()) s = excl_resultS () s" + unfolding read_mem_bytesS_def read_memS_def read_tagS_def write_mem_eaS_def write_mem_valS_def write_mem_bytesS_def write_tagS_def excl_resultS_def + by (auto simp: bindS_def chooseS_def Let_def split: option.splits)+ + +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_cong) + +lemma no_throw_read_regvalS: "ignore_throw (read_regvalS r reg_name) s = read_regvalS r reg_name s" + by (cases r) (auto simp: bindS_def split: option.splits) + +lemma no_throw_write_regvalS: "ignore_throw (write_regvalS r reg_name v) s = write_regvalS r reg_name v s" + by (cases r) (auto simp: bindS_def split: option.splits) + +lemmas no_throw_builtins[simp, intro] = + no_throw_mem_builtins no_throw_read_regvalS no_throw_write_regvalS no_throw_read_memS + +end end |