From ee123e2876c4fa5ae000256caeb7eb810e8c05f8 Mon Sep 17 00:00:00 2001 From: Thomas Bauereiss Date: Mon, 26 Feb 2018 13:22:11 +0000 Subject: Rename some Isabelle theories The suffix _lemmas is more descriptive than _extras. --- lib/isabelle/Makefile | 6 +- lib/isabelle/Prompt_monad_extras.thy | 156 ---------------------------- lib/isabelle/Prompt_monad_lemmas.thy | 156 ++++++++++++++++++++++++++++ lib/isabelle/ROOT | 4 +- lib/isabelle/Sail_values_extras.thy | 52 ---------- lib/isabelle/Sail_values_lemmas.thy | 52 ++++++++++ lib/isabelle/State_extras.thy | 190 ----------------------------------- lib/isabelle/State_lemmas.thy | 190 +++++++++++++++++++++++++++++++++++ lib/isabelle/State_monad_extras.thy | 146 --------------------------- lib/isabelle/State_monad_lemmas.thy | 146 +++++++++++++++++++++++++++ 10 files changed, 549 insertions(+), 549 deletions(-) delete mode 100644 lib/isabelle/Prompt_monad_extras.thy create mode 100644 lib/isabelle/Prompt_monad_lemmas.thy delete mode 100644 lib/isabelle/Sail_values_extras.thy create mode 100644 lib/isabelle/Sail_values_lemmas.thy delete mode 100644 lib/isabelle/State_extras.thy create mode 100644 lib/isabelle/State_lemmas.thy delete mode 100644 lib/isabelle/State_monad_extras.thy create mode 100644 lib/isabelle/State_monad_lemmas.thy (limited to 'lib') diff --git a/lib/isabelle/Makefile b/lib/isabelle/Makefile index 1cff8f61..688dfa07 100644 --- a/lib/isabelle/Makefile +++ b/lib/isabelle/Makefile @@ -1,7 +1,7 @@ THYS = Sail_instr_kinds.thy Sail_values.thy Sail_operators.thy \ Sail_operators_mwords.thy Sail_operators_bitlists.thy \ State_monad.thy State.thy Prompt_monad.thy Prompt.thy -EXTRA_THYS = State_monad_extras.thy State_extras.thy Prompt_monad_extras.thy +EXTRA_THYS = State_monad_lemmas.thy State_lemmas.thy Prompt_monad_lemmas.thy .PHONY: all heap-img clean @@ -32,13 +32,13 @@ Sail_operators_bitlists.thy: ../../src/gen_lib/sail_operators_bitlists.lem Sail_ Prompt_monad.thy: ../../src/gen_lib/prompt_monad.lem Sail_values.thy lem -isa -outdir . -lib ../../src/lem_interp -lib ../../src/gen_lib $< -Prompt.thy: ../../src/gen_lib/prompt.lem Prompt_monad.thy Prompt_monad_extras.thy +Prompt.thy: ../../src/gen_lib/prompt.lem Prompt_monad.thy Prompt_monad_lemmas.thy lem -isa -outdir . -lib ../../src/lem_interp -lib ../../src/gen_lib $< State_monad.thy: ../../src/gen_lib/state_monad.lem Sail_values.thy lem -isa -outdir . -lib ../../src/lem_interp -lib ../../src/gen_lib $< -State.thy: ../../src/gen_lib/state.lem Prompt.thy State_monad.thy State_monad_extras.thy +State.thy: ../../src/gen_lib/state.lem Prompt.thy State_monad.thy State_monad_lemmas.thy lem -isa -outdir . -lib ../../src/lem_interp -lib ../../src/gen_lib $< clean: diff --git a/lib/isabelle/Prompt_monad_extras.thy b/lib/isabelle/Prompt_monad_extras.thy deleted file mode 100644 index 9d29f5a2..00000000 --- a/lib/isabelle/Prompt_monad_extras.thy +++ /dev/null @@ -1,156 +0,0 @@ -theory Prompt_monad_extras - imports - Prompt_monad - Sail_values_extras -begin - -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 - -lemma bind_return[simp]: "bind (return a) f = f a" - by (auto simp: return_def) - -lemma bind_assoc[simp]: "bind (bind m f) g = bind m (\x. bind (f x) g)" - by (induction m f arbitrary: g rule: bind.induct) auto - -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 - -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_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 *) - | e_read_reg string 'regval - (* Request to write register *) - | e_write_reg string 'regval - -inductive_set T :: "(('rv, 'a, 'e) monad \ 'rv event \ ('rv, 'a, 'e) monad) set" where - Read_mem: "((Read_mem rk addr sz k), e_read_mem rk addr sz v, k v) \ T" -| Read_tag: "((Read_tag addr k), e_read_tag addr v, k v) \ T" -| Write_ea: "((Write_ea wk addr sz k), e_write_ea wk addr sz, k) \ T" -| Excl_res: "((Excl_res k), e_excl_res r, k r) \ T" -| Write_memv: "((Write_memv v k), e_write_memv v r, k r) \ T" -| Write_tagv: "((Write_tagv v k), e_write_tagv v r, k r) \ T" -| Footprint: "((Footprint k), e_footprint, k) \ T" -| Barrier: "((Barrier bk k), e_barrier bk, k) \ T" -| Read_reg: "((Read_reg r k), e_read_reg r v, k v) \ T" -| Write_reg: "((Write_reg r v k), e_write_reg r v, k) \ T" - -inductive_set Traces :: "(('rv, 'a, 'e) monad \ 'rv event list \ ('rv, 'a, 'e) monad) set" where - Nil: "(s, [], s) \ Traces" -| Step: "\(s, e, s'') \ T; (s'', t, s') \ Traces\ \ (s, e # t, s') \ Traces" - -declare Traces.intros[intro] -declare T.intros[intro] - -declare prod.splits[split] - -lemmas Traces_ConsI = T.intros[THEN Step, rotated] - -inductive_cases Traces_NilE[elim]: "(s, [], s') \ Traces" -inductive_cases Traces_ConsE[elim]: "(s, e # t, s') \ Traces" - -lemma Traces_cases: - fixes m :: "('rv, 'a, 'e) monad" - assumes Run: "(m, t, m') \ 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') \ 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') \ 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') \ 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') \ Traces" - | (Barrier) bk k t' v where "m = Barrier bk k" and "t = e_barrier bk # t'" and "(k, t', m') \ 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') \ Traces" - | (Excl_res) k t' v where "m = Excl_res k" and "t = e_excl_res v # t'" and "(k v, t', m') \ 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') \ Traces" - | (Footprint) k t' where "m = Footprint k" and "t = e_footprint # t'" and "(k, t', m') \ 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') \ Traces" -proof (use Run in \cases m t m' set: Traces\) - case Nil - then show ?thesis by (auto intro: that(1)) -next - case (Step e m'' t') - from \(m, e, m'') \ T\ and \t = e # t'\ and \(m'', t', m') \ Traces\ - show ?thesis by (cases m e m'' rule: T.cases; elim that; blast) -qed - -abbreviation Run :: "('rv, 'a, 'e) monad \ 'rv event list \ 'a \ bool" - where "Run s t a \ (s, t, Done a) \ Traces" - -lemma Run_appendI: - assumes "(s, t1, s') \ Traces" - and "Run s' t2 a" - shows "Run s (t1 @ t2) a" -proof (use assms in \induction t1 arbitrary: s\) - case (Cons e t1) - then show ?case by (elim Traces_ConsE) auto -qed auto - -lemma bind_DoneE: - assumes "bind m f = Done a" - obtains a' where "m = Done a'" and "f a' = Done a" - using assms by (auto elim: bind.elims) - -lemma bind_T_cases: - assumes "(bind m f, e, s') \ T" - obtains (Done) a where "m = Done a" - | (Bind) m' where "s' = bind m' f" and "(m, e, m') \ T" - using assms by (cases; blast elim: bind.elims) - -lemma Run_bindE: - fixes m :: "('rv, 'b, 'e) monad" and a :: 'a - assumes "Run (bind m f) t a" - obtains tm am tf where "t = tm @ tf" and "Run m tm am" and "Run (f am) tf a" -proof (use assms in \induction "bind m f" t "Done a :: ('rv, 'a, 'e) monad" arbitrary: m rule: Traces.induct\) - case Nil - obtain am where "m = Done am" and "f am = Done a" using Nil(1) by (elim bind_DoneE) - then show ?case by (intro Nil(2)) auto -next - case (Step e s'' t m) - show thesis using Step(1) - proof (cases rule: bind_T_cases) - case (Done am) - then show ?thesis using Step(1,2) by (intro Step(4)[of "[]" "e # t" am]) auto - next - case (Bind m') - show ?thesis proof (rule Step(3)[OF Bind(1)]) - fix tm tf am - assume "t = tm @ tf" and "Run m' tm am" and "Run (f am) tf a" - then show thesis using Bind by (intro Step(4)[of "e # tm" tf am]) auto - qed - 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' \ t = [] \ a' = a" - by (auto elim: Run_DoneE) - -lemma bind_cong[fundef_cong]: - assumes m: "m1 = m2" - and f: "\t a. Run m2 t a \ f1 a = f2 a" - shows "bind m1 f1 = bind m2 f2" - unfolding m using f - by (induction m2 f1 arbitrary: f2 rule: bind.induct; unfold bind.simps; blast) - -end diff --git a/lib/isabelle/Prompt_monad_lemmas.thy b/lib/isabelle/Prompt_monad_lemmas.thy new file mode 100644 index 00000000..d2466764 --- /dev/null +++ b/lib/isabelle/Prompt_monad_lemmas.thy @@ -0,0 +1,156 @@ +theory Prompt_monad_lemmas + imports + Prompt_monad + Sail_values_lemmas +begin + +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 + +lemma bind_return[simp]: "bind (return a) f = f a" + by (auto simp: return_def) + +lemma bind_assoc[simp]: "bind (bind m f) g = bind m (\x. bind (f x) g)" + by (induction m f arbitrary: g rule: bind.induct) auto + +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 + +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_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 *) + | e_read_reg string 'regval + (* Request to write register *) + | e_write_reg string 'regval + +inductive_set T :: "(('rv, 'a, 'e) monad \ 'rv event \ ('rv, 'a, 'e) monad) set" where + Read_mem: "((Read_mem rk addr sz k), e_read_mem rk addr sz v, k v) \ T" +| Read_tag: "((Read_tag addr k), e_read_tag addr v, k v) \ T" +| Write_ea: "((Write_ea wk addr sz k), e_write_ea wk addr sz, k) \ T" +| Excl_res: "((Excl_res k), e_excl_res r, k r) \ T" +| Write_memv: "((Write_memv v k), e_write_memv v r, k r) \ T" +| Write_tagv: "((Write_tagv v k), e_write_tagv v r, k r) \ T" +| Footprint: "((Footprint k), e_footprint, k) \ T" +| Barrier: "((Barrier bk k), e_barrier bk, k) \ T" +| Read_reg: "((Read_reg r k), e_read_reg r v, k v) \ T" +| Write_reg: "((Write_reg r v k), e_write_reg r v, k) \ T" + +inductive_set Traces :: "(('rv, 'a, 'e) monad \ 'rv event list \ ('rv, 'a, 'e) monad) set" where + Nil: "(s, [], s) \ Traces" +| Step: "\(s, e, s'') \ T; (s'', t, s') \ Traces\ \ (s, e # t, s') \ Traces" + +declare Traces.intros[intro] +declare T.intros[intro] + +declare prod.splits[split] + +lemmas Traces_ConsI = T.intros[THEN Step, rotated] + +inductive_cases Traces_NilE[elim]: "(s, [], s') \ Traces" +inductive_cases Traces_ConsE[elim]: "(s, e # t, s') \ Traces" + +lemma Traces_cases: + fixes m :: "('rv, 'a, 'e) monad" + assumes Run: "(m, t, m') \ 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') \ 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') \ 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') \ 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') \ Traces" + | (Barrier) bk k t' v where "m = Barrier bk k" and "t = e_barrier bk # t'" and "(k, t', m') \ 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') \ Traces" + | (Excl_res) k t' v where "m = Excl_res k" and "t = e_excl_res v # t'" and "(k v, t', m') \ 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') \ Traces" + | (Footprint) k t' where "m = Footprint k" and "t = e_footprint # t'" and "(k, t', m') \ 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') \ Traces" +proof (use Run in \cases m t m' set: Traces\) + case Nil + then show ?thesis by (auto intro: that(1)) +next + case (Step e m'' t') + from \(m, e, m'') \ T\ and \t = e # t'\ and \(m'', t', m') \ Traces\ + show ?thesis by (cases m e m'' rule: T.cases; elim that; blast) +qed + +abbreviation Run :: "('rv, 'a, 'e) monad \ 'rv event list \ 'a \ bool" + where "Run s t a \ (s, t, Done a) \ Traces" + +lemma Run_appendI: + assumes "(s, t1, s') \ Traces" + and "Run s' t2 a" + shows "Run s (t1 @ t2) a" +proof (use assms in \induction t1 arbitrary: s\) + case (Cons e t1) + then show ?case by (elim Traces_ConsE) auto +qed auto + +lemma bind_DoneE: + assumes "bind m f = Done a" + obtains a' where "m = Done a'" and "f a' = Done a" + using assms by (auto elim: bind.elims) + +lemma bind_T_cases: + assumes "(bind m f, e, s') \ T" + obtains (Done) a where "m = Done a" + | (Bind) m' where "s' = bind m' f" and "(m, e, m') \ T" + using assms by (cases; blast elim: bind.elims) + +lemma Run_bindE: + fixes m :: "('rv, 'b, 'e) monad" and a :: 'a + assumes "Run (bind m f) t a" + obtains tm am tf where "t = tm @ tf" and "Run m tm am" and "Run (f am) tf a" +proof (use assms in \induction "bind m f" t "Done a :: ('rv, 'a, 'e) monad" arbitrary: m rule: Traces.induct\) + case Nil + obtain am where "m = Done am" and "f am = Done a" using Nil(1) by (elim bind_DoneE) + then show ?case by (intro Nil(2)) auto +next + case (Step e s'' t m) + show thesis using Step(1) + proof (cases rule: bind_T_cases) + case (Done am) + then show ?thesis using Step(1,2) by (intro Step(4)[of "[]" "e # t" am]) auto + next + case (Bind m') + show ?thesis proof (rule Step(3)[OF Bind(1)]) + fix tm tf am + assume "t = tm @ tf" and "Run m' tm am" and "Run (f am) tf a" + then show thesis using Bind by (intro Step(4)[of "e # tm" tf am]) auto + qed + 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' \ t = [] \ a' = a" + by (auto elim: Run_DoneE) + +lemma bind_cong[fundef_cong]: + assumes m: "m1 = m2" + and f: "\t a. Run m2 t a \ f1 a = f2 a" + shows "bind m1 f1 = bind m2 f2" + unfolding m using f + by (induction m2 f1 arbitrary: f2 rule: bind.induct; unfold bind.simps; blast) + +end diff --git a/lib/isabelle/ROOT b/lib/isabelle/ROOT index b07bc807..4c5079fe 100644 --- a/lib/isabelle/ROOT +++ b/lib/isabelle/ROOT @@ -1,9 +1,9 @@ session "Sail" = "LEM" + options [document = false] theories - Sail_values_extras + Sail_values_lemmas Prompt - State_extras + State_lemmas Sail_operators_mwords Sail_operators_bitlists diff --git a/lib/isabelle/Sail_values_extras.thy b/lib/isabelle/Sail_values_extras.thy deleted file mode 100644 index 66bcba48..00000000 --- a/lib/isabelle/Sail_values_extras.thy +++ /dev/null @@ -1,52 +0,0 @@ -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 (\(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 \ None \ set xs" - by (induction xs) (auto split: option.splits) - -lemma just_list_Some_iff[simp]: "just_list xs = Some ys \ 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 \ 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 \ 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 \ 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 \ {B0, B1}" - by (auto simp: bitU_of_bool_def split: if_splits) - -lemma bool_of_bitU_bitU_of_bool[simp]: "bool_of_bitU \ 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 \ {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 \induction acc bs rule: nat_of_bits_aux.induct\) - (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/Sail_values_lemmas.thy b/lib/isabelle/Sail_values_lemmas.thy new file mode 100644 index 00000000..2114d991 --- /dev/null +++ b/lib/isabelle/Sail_values_lemmas.thy @@ -0,0 +1,52 @@ +theory Sail_values_lemmas + imports Sail_values +begin + +termination reverse_endianness_list by (lexicographic_order simp add: drop_list_def) + +termination index_list + by (relation "measure (\(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 \ None \ set xs" + by (induction xs) (auto split: option.splits) + +lemma just_list_Some_iff[simp]: "just_list xs = Some ys \ 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 \ 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 \ 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 \ 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 \ {B0, B1}" + by (auto simp: bitU_of_bool_def split: if_splits) + +lemma bool_of_bitU_bitU_of_bool[simp]: "bool_of_bitU \ 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 \ {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 \induction acc bs rule: nat_of_bits_aux.induct\) + (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 deleted file mode 100644 index 924861b0..00000000 --- a/lib/isabelle/State_extras.thy +++ /dev/null @@ -1,190 +0,0 @@ -theory State_extras - imports State -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 \ 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') \ set (liftState r m s)" - obtains t where "Run m t a" - by (use assms in \induction r m arbitrary: s s' rule: liftState.induct\; - 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_try_catch[simp]: - "liftState r (try_catch m h) = try_catchS (liftState r m) (liftState r \ 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 \ 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_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 "\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) = readS (read_from reg \ 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" - using assms unfolding bind_eq_Some_conv by blast - then show "liftState (get_regval', set_regval') (read_reg reg) s = readS (read_from reg \ regstate) s" - by (auto simp: read_reg_def bindS_def returnS_def read_regS_def readS_def) -qed - -lemma liftState_write_reg_updateS: - assumes "\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 (\i x. liftState r (f i x)) xs" - by (induction i "\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 (\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 \ f) xs" - by (auto simp: iter_def iterS_def) - -lemma liftState_foreachM[simp]: - "liftState r (foreachM xs vars body) = foreachS xs vars (\x vars. liftState r (body x vars))" - by (induction xs vars "\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') \ set (cond vars s)" - and "(Value vars', s'') \ set (body vars s')" - shows "whileS_dom (vars', cond, body, s'')" - by (use assms in \induction vars cond body s arbitrary: vars' s' s'' rule: whileS.pinduct\) - (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 \induction vars cond body arbitrary: vars' t t' rule: whileM.pinduct\) - (auto intro: whileM.domintros) - -lemma whileM_dom_ex_step: - assumes "whileM_dom (vars, cond, body)" - and "\t. Run (cond vars) t True" - and "\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 \ cond, liftState r \ body, s)" - and "whileM_dom (vars, cond, body)" - shows "liftState r (whileM vars cond body) s = whileS vars (liftState r \ cond) (liftState r \ body) s" -proof (use assms in \induction vars "liftState r \ cond" "liftState r \ body" s rule: whileS.pinduct\) - 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 \ (\vars. whileM vars cond body)) s' = - bindS (liftState r (body vars)) (\vars. whileS vars (liftState r \ cond) (liftState r \ 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 "\t. Run (cond vars) t True" using while that by (auto elim: Value_liftState_Run) - show "\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 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 \induction vars cond body arbitrary: vars' t t' rule: untilM.pinduct\) - (auto intro: untilM.domintros) - -lemma untilM_dom_ex_step: - assumes "untilM_dom (vars, cond, body)" - and "\t. Run (body vars) t vars'" - and "\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 \ cond, liftState r \ body, s)" - and "untilM_dom (vars, cond, body)" - shows "liftState r (untilM vars cond body) s = untilS vars (liftState r \ cond) (liftState r \ body) s" -proof (use assms in \induction vars "liftState r \ cond" "liftState r \ body" s rule: untilS.pinduct\) - 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 "\a" - proof (rule untilM_dom_ex_step[OF domM]) - show "\t. Run (body vars) t vars'" using k by (auto elim: Value_liftState_Run) - show "\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_lemmas.thy b/lib/isabelle/State_lemmas.thy new file mode 100644 index 00000000..e230bd37 --- /dev/null +++ b/lib/isabelle/State_lemmas.thy @@ -0,0 +1,190 @@ +theory State_lemmas + imports State +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 \ 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') \ set (liftState r m s)" + obtains t where "Run m t a" + by (use assms in \induction r m arbitrary: s s' rule: liftState.induct\; + 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_try_catch[simp]: + "liftState r (try_catch m h) = try_catchS (liftState r m) (liftState r \ 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 \ 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_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 "\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) = readS (read_from reg \ 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" + using assms unfolding bind_eq_Some_conv by blast + then show "liftState (get_regval', set_regval') (read_reg reg) s = readS (read_from reg \ regstate) s" + by (auto simp: read_reg_def bindS_def returnS_def read_regS_def readS_def) +qed + +lemma liftState_write_reg_updateS: + assumes "\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 (\i x. liftState r (f i x)) xs" + by (induction i "\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 (\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 \ f) xs" + by (auto simp: iter_def iterS_def) + +lemma liftState_foreachM[simp]: + "liftState r (foreachM xs vars body) = foreachS xs vars (\x vars. liftState r (body x vars))" + by (induction xs vars "\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') \ set (cond vars s)" + and "(Value vars', s'') \ set (body vars s')" + shows "whileS_dom (vars', cond, body, s'')" + by (use assms in \induction vars cond body s arbitrary: vars' s' s'' rule: whileS.pinduct\) + (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 \induction vars cond body arbitrary: vars' t t' rule: whileM.pinduct\) + (auto intro: whileM.domintros) + +lemma whileM_dom_ex_step: + assumes "whileM_dom (vars, cond, body)" + and "\t. Run (cond vars) t True" + and "\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 \ cond, liftState r \ body, s)" + and "whileM_dom (vars, cond, body)" + shows "liftState r (whileM vars cond body) s = whileS vars (liftState r \ cond) (liftState r \ body) s" +proof (use assms in \induction vars "liftState r \ cond" "liftState r \ body" s rule: whileS.pinduct\) + 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 \ (\vars. whileM vars cond body)) s' = + bindS (liftState r (body vars)) (\vars. whileS vars (liftState r \ cond) (liftState r \ 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 "\t. Run (cond vars) t True" using while that by (auto elim: Value_liftState_Run) + show "\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 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 \induction vars cond body arbitrary: vars' t t' rule: untilM.pinduct\) + (auto intro: untilM.domintros) + +lemma untilM_dom_ex_step: + assumes "untilM_dom (vars, cond, body)" + and "\t. Run (body vars) t vars'" + and "\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 \ cond, liftState r \ body, s)" + and "untilM_dom (vars, cond, body)" + shows "liftState r (untilM vars cond body) s = untilS vars (liftState r \ cond) (liftState r \ body) s" +proof (use assms in \induction vars "liftState r \ cond" "liftState r \ body" s rule: untilS.pinduct\) + 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 "\a" + proof (rule untilM_dom_ex_step[OF domM]) + show "\t. Run (body vars) t vars'" using k by (auto elim: Value_liftState_Run) + show "\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 deleted file mode 100644 index 406aec79..00000000 --- a/lib/isabelle/State_monad_extras.thy +++ /dev/null @@ -1,146 +0,0 @@ -theory State_monad_extras - 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 \ (\r. case r of (Value a, s') \ f a s' | (Ex e, s') \ [(Ex e, s')])" -abbreviation "bindS_app ms f \ List.concat (List.map (bindS_aux f) ms)" - -lemma bindS_ext_cong[fundef_cong]: - assumes m: "m1 s = m2 s" - and f: "\a s'. (Value a, s') \ set (m2 s) \ f1 a s' = f2 a s'" - shows "bindS m1 f1 s = bindS m2 f2 s" -proof - - 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 - -lemma bindS_cong[fundef_cong]: - assumes m: "m1 = m2" - and f: "\s a s'. (Value a, s') \ set (m2 s) \ f1 a s' = f2 a s'" - shows "bindS m1 f1 = bindS m2 f2" - using assms by (blast intro: bindS_ext_cong) - -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 \ '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 = (\s. m (f s) s)" - by (auto simp: bindS_def) - -lemma bindS_updateS: "bindS (updateS f) m = (\s. m () (f s))" - by (auto simp: bindS_def) - -lemma bindS_assoc[simp]: "bindS (bindS m f) g = bindS m (\x. bindS (f x) g)" -proof - - have "List.concat (map (bindS_aux g) (List.concat (map (bindS_aux f) xs))) = - List.concat (map (bindS_aux (\x s. List.concat (map (bindS_aux g) (f x s)))) xs)" for xs - by (induction xs) (auto split: result.splits) - then show ?thesis unfolding bindS_def by auto -qed - -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') \ set (bindS m f s)" - obtains s'' a' where "(Value a', s'') \ set (m s)" and "(Value a, s') \ set (f a' s'')" - using assms by (auto simp: bindS_def; split result.splits; auto) - -abbreviation - "try_catchS_aux h r \ - (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 \ 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: try_catchS_def) - -lemma try_catchS_cong[cong]: - assumes "\s. m1 s = m2 s" 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 \ 's) list \ (('a, 'e2) result \ '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 \ ('r, 'a, 'e2) monadS" where - "ignore_throw m \ \s. ignore_throw_app (m s)" - -lemma [simp]: "ignore_throw_app ms = (Ex (Throw e), s) # ms' \ 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 \ 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 \ f)" - "ignore_throw (bindS m f) s = bindS (ignore_throw m) (ignore_throw \ 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: "\s. ignore_throw m1 s = m1 s" - and m2: "\s. ignore_throw m1 s = m2 s" - shows "try_catchS (bindS m1 f) h = bindS m2 (\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) (\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 (\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: - "\a. ignore_throw (returnS a) = returnS a" - "\BC rk a sz s. ignore_throw (read_mem_bytesS BC rk a sz) s = read_mem_bytesS BC rk a sz s" - "\BC a s. ignore_throw (read_tagS BC a) s = read_tagS BC a s" - "\BC wk a sz s. ignore_throw (write_mem_eaS BC wk a sz) s = write_mem_eaS BC wk a sz s" - "\v s. ignore_throw (write_mem_bytesS v) s = write_mem_bytesS v s" - "\BC v s. ignore_throw (write_mem_valS BC v) s = write_mem_valS BC v s" - "\t s. ignore_throw (write_tagS t) s = write_tagS t s" - "\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 diff --git a/lib/isabelle/State_monad_lemmas.thy b/lib/isabelle/State_monad_lemmas.thy new file mode 100644 index 00000000..fe827c66 --- /dev/null +++ b/lib/isabelle/State_monad_lemmas.thy @@ -0,0 +1,146 @@ +theory State_monad_lemmas + imports + State_monad + Sail_values_lemmas +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 \ (\r. case r of (Value a, s') \ f a s' | (Ex e, s') \ [(Ex e, s')])" +abbreviation "bindS_app ms f \ List.concat (List.map (bindS_aux f) ms)" + +lemma bindS_ext_cong[fundef_cong]: + assumes m: "m1 s = m2 s" + and f: "\a s'. (Value a, s') \ set (m2 s) \ f1 a s' = f2 a s'" + shows "bindS m1 f1 s = bindS m2 f2 s" +proof - + 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 + +lemma bindS_cong[fundef_cong]: + assumes m: "m1 = m2" + and f: "\s a s'. (Value a, s') \ set (m2 s) \ f1 a s' = f2 a s'" + shows "bindS m1 f1 = bindS m2 f2" + using assms by (blast intro: bindS_ext_cong) + +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 \ '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 = (\s. m (f s) s)" + by (auto simp: bindS_def) + +lemma bindS_updateS: "bindS (updateS f) m = (\s. m () (f s))" + by (auto simp: bindS_def) + +lemma bindS_assoc[simp]: "bindS (bindS m f) g = bindS m (\x. bindS (f x) g)" +proof - + have "List.concat (map (bindS_aux g) (List.concat (map (bindS_aux f) xs))) = + List.concat (map (bindS_aux (\x s. List.concat (map (bindS_aux g) (f x s)))) xs)" for xs + by (induction xs) (auto split: result.splits) + then show ?thesis unfolding bindS_def by auto +qed + +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') \ set (bindS m f s)" + obtains s'' a' where "(Value a', s'') \ set (m s)" and "(Value a, s') \ set (f a' s'')" + using assms by (auto simp: bindS_def; split result.splits; auto) + +abbreviation + "try_catchS_aux h r \ + (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 \ 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: try_catchS_def) + +lemma try_catchS_cong[cong]: + assumes "\s. m1 s = m2 s" 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 \ 's) list \ (('a, 'e2) result \ '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 \ ('r, 'a, 'e2) monadS" where + "ignore_throw m \ \s. ignore_throw_app (m s)" + +lemma [simp]: "ignore_throw_app ms = (Ex (Throw e), s) # ms' \ 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 \ 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 \ f)" + "ignore_throw (bindS m f) s = bindS (ignore_throw m) (ignore_throw \ 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: "\s. ignore_throw m1 s = m1 s" + and m2: "\s. ignore_throw m1 s = m2 s" + shows "try_catchS (bindS m1 f) h = bindS m2 (\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) (\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 (\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: + "\a. ignore_throw (returnS a) = returnS a" + "\BC rk a sz s. ignore_throw (read_mem_bytesS BC rk a sz) s = read_mem_bytesS BC rk a sz s" + "\BC a s. ignore_throw (read_tagS BC a) s = read_tagS BC a s" + "\BC wk a sz s. ignore_throw (write_mem_eaS BC wk a sz) s = write_mem_eaS BC wk a sz s" + "\v s. ignore_throw (write_mem_bytesS v) s = write_mem_bytesS v s" + "\BC v s. ignore_throw (write_mem_valS BC v) s = write_mem_valS BC v s" + "\t s. ignore_throw (write_tagS t) s = write_tagS t s" + "\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 -- cgit v1.2.3