From 2005eb7c190f8d28d6499df3dd77cf65a87e60cb Mon Sep 17 00:00:00 2001 From: Thomas Bauereiss Date: Thu, 21 Jun 2018 17:50:54 +0100 Subject: Follow Sail2 renaming in Isabelle library --- lib/isabelle/Hoare.thy | 2 +- lib/isabelle/Makefile | 36 ++-- lib/isabelle/Prompt_monad_lemmas.thy | 171 --------------- lib/isabelle/ROOT | 11 +- lib/isabelle/Sail2_operators_mwords_lemmas.thy | 112 ++++++++++ lib/isabelle/Sail2_prompt_monad_lemmas.thy | 171 +++++++++++++++ lib/isabelle/Sail2_state_lemmas.thy | 276 +++++++++++++++++++++++++ lib/isabelle/Sail2_state_monad_lemmas.thy | 232 +++++++++++++++++++++ lib/isabelle/Sail2_values_lemmas.thy | 206 ++++++++++++++++++ lib/isabelle/Sail_operators_mwords_lemmas.thy | 112 ---------- lib/isabelle/Sail_values_lemmas.thy | 206 ------------------ lib/isabelle/State_lemmas.thy | 260 ----------------------- lib/isabelle/State_monad_lemmas.thy | 232 --------------------- lib/isabelle/manual/Manual.thy | 18 +- src/gen_lib/sail2_prompt.lem | 2 +- src/gen_lib/sail2_string.lem | 14 +- 16 files changed, 1042 insertions(+), 1019 deletions(-) delete mode 100644 lib/isabelle/Prompt_monad_lemmas.thy create mode 100644 lib/isabelle/Sail2_operators_mwords_lemmas.thy create mode 100644 lib/isabelle/Sail2_prompt_monad_lemmas.thy create mode 100644 lib/isabelle/Sail2_state_lemmas.thy create mode 100644 lib/isabelle/Sail2_state_monad_lemmas.thy create mode 100644 lib/isabelle/Sail2_values_lemmas.thy delete mode 100644 lib/isabelle/Sail_operators_mwords_lemmas.thy delete mode 100644 lib/isabelle/Sail_values_lemmas.thy delete mode 100644 lib/isabelle/State_lemmas.thy delete mode 100644 lib/isabelle/State_monad_lemmas.thy diff --git a/lib/isabelle/Hoare.thy b/lib/isabelle/Hoare.thy index 9271e2fa..5c77c5e7 100644 --- a/lib/isabelle/Hoare.thy +++ b/lib/isabelle/Hoare.thy @@ -1,6 +1,6 @@ theory Hoare imports - State_lemmas + Sail2_state_lemmas "HOL-Eisbach.Eisbach_Tools" begin diff --git a/lib/isabelle/Makefile b/lib/isabelle/Makefile index b10dde78..56591140 100644 --- a/lib/isabelle/Makefile +++ b/lib/isabelle/Makefile @@ -1,8 +1,11 @@ -THYS = Sail_instr_kinds.thy Sail_values.thy Sail_operators.thy \ - Sail_operators_mwords.thy Sail_operators_bitlists.thy \ - State_monad.thy State.thy State_lifting.thy Prompt_monad.thy Prompt.thy -EXTRA_THYS = State_monad_lemmas.thy State_lemmas.thy Prompt_monad_lemmas.thy \ - Sail_operators_mwords_lemmas.thy Hoare.thy +THYS = Sail2_instr_kinds.thy Sail2_values.thy Sail2_operators.thy \ + Sail2_operators_mwords.thy Sail2_operators_bitlists.thy \ + Sail2_state_monad.thy Sail2_state.thy Sail2_state_lifting.thy \ + Sail2_prompt_monad.thy Sail2_prompt.thy \ + Sail2_string.thy +EXTRA_THYS = Sail2_state_monad_lemmas.thy Sail2_state_lemmas.thy \ + Sail2_prompt_monad_lemmas.thy \ + Sail2_operators_mwords_lemmas.thy Hoare.thy RISCV_DIR = ../../riscv @@ -24,34 +27,37 @@ manual: heap-img manual/Manual.thy manual/ROOT manual/document/root.tex make -C $(RISCV_DIR) Riscv_duopod.thy isabelle build -d manual Sail-Manual -Sail_instr_kinds.thy: ../../src/lem_interp/sail_instr_kinds.lem +Sail2_instr_kinds.thy: ../../src/lem_interp/sail2_instr_kinds.lem lem -isa -outdir . -auxiliary_level none -lib ../../src/lem_interp -lib ../../src/gen_lib $< -Sail_values.thy: ../../src/gen_lib/sail_values.lem Sail_instr_kinds.thy +Sail2_values.thy: ../../src/gen_lib/sail2_values.lem Sail2_instr_kinds.thy lem -isa -outdir . -auxiliary_level none -lib ../../src/lem_interp -lib ../../src/gen_lib $< -Sail_operators.thy: ../../src/gen_lib/sail_operators.lem Sail_values.thy +Sail2_operators.thy: ../../src/gen_lib/sail2_operators.lem Sail2_values.thy lem -isa -outdir . -auxiliary_level none -lib ../../src/lem_interp -lib ../../src/gen_lib $< -Sail_operators_mwords.thy: ../../src/gen_lib/sail_operators_mwords.lem Sail_operators.thy Prompt.thy +Sail2_operators_mwords.thy: ../../src/gen_lib/sail2_operators_mwords.lem Sail2_operators.thy Sail2_prompt.thy lem -isa -outdir . -auxiliary_level none -lib ../../src/lem_interp -lib ../../src/gen_lib $< -Sail_operators_bitlists.thy: ../../src/gen_lib/sail_operators_bitlists.lem Sail_operators.thy Prompt.thy +Sail2_operators_bitlists.thy: ../../src/gen_lib/sail2_operators_bitlists.lem Sail2_operators.thy Sail2_prompt.thy lem -isa -outdir . -auxiliary_level none -lib ../../src/lem_interp -lib ../../src/gen_lib $< -Prompt_monad.thy: ../../src/gen_lib/prompt_monad.lem Sail_values.thy +Sail2_prompt_monad.thy: ../../src/gen_lib/sail2_prompt_monad.lem Sail2_values.thy lem -isa -outdir . -auxiliary_level none -lib ../../src/lem_interp -lib ../../src/gen_lib $< -Prompt.thy: ../../src/gen_lib/prompt.lem Prompt_monad.thy Prompt_monad_lemmas.thy +Sail2_prompt.thy: ../../src/gen_lib/sail2_prompt.lem Sail2_prompt_monad.thy Sail2_prompt_monad_lemmas.thy lem -isa -outdir . -auxiliary_level none -lib ../../src/lem_interp -lib ../../src/gen_lib $< -State_monad.thy: ../../src/gen_lib/state_monad.lem Sail_values.thy +Sail2_state_monad.thy: ../../src/gen_lib/sail2_state_monad.lem Sail2_values.thy lem -isa -outdir . -auxiliary_level none -lib ../../src/lem_interp -lib ../../src/gen_lib $< -State.thy: ../../src/gen_lib/state.lem Prompt.thy State_monad.thy State_monad_lemmas.thy +Sail2_state.thy: ../../src/gen_lib/sail2_state.lem Sail2_prompt.thy Sail2_state_monad.thy Sail2_state_monad_lemmas.thy lem -isa -outdir . -auxiliary_level none -lib ../../src/lem_interp -lib ../../src/gen_lib $< -State_lifting.thy: ../../src/gen_lib/state_lifting.lem Prompt.thy State.thy +Sail2_state_lifting.thy: ../../src/gen_lib/sail2_state_lifting.lem Sail2_prompt.thy Sail2_state.thy + lem -isa -outdir . -auxiliary_level none -lib ../../src/lem_interp -lib ../../src/gen_lib $< + +Sail2_string.thy: ../../src/gen_lib/sail2_string.lem Sail2_operators_mwords.thy lem -isa -outdir . -auxiliary_level none -lib ../../src/lem_interp -lib ../../src/gen_lib $< clean: diff --git a/lib/isabelle/Prompt_monad_lemmas.thy b/lib/isabelle/Prompt_monad_lemmas.thy deleted file mode 100644 index 7a3a108d..00000000 --- a/lib/isabelle/Prompt_monad_lemmas.thy +++ /dev/null @@ -1,171 +0,0 @@ -theory Prompt_monad_lemmas - imports - Prompt_monad - Sail_values_lemmas -begin - -notation bind (infixr "\" 54) - -abbreviation seq :: "('rv,unit,'e)monad \ ('rv,'b,'e)monad \('rv,'b,'e)monad" (infixr "\" 54) where - "m \ n \ m \ (\_. n)" - -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 Exception] = bind.induct - -lemma bind_return[simp]: "bind (return a) f = f a" - by (auto simp: return_def) -lemma bind_return_right[simp]: "bind x return = x" by (induction x) (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 bind_assert_True[simp]: "bind (assert_exp True msg) f = f ()" - by (auto simp: assert_exp_def) - -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 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 \ '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_tag: "((Write_tag a v k), e_write_tag a 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" -| Undefined : "((Undefined k), e_undefined v, k v) \ T" -| Print: "((Print msg k), e_print msg, 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_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') \ 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" - | (Undefined) v k t' where "m = Undefined k" and "t = e_undefined v # t'" and "(k v, t', m') \ Traces" - | (Print) msg k t' where "m = Print msg k" and "t = e_print msg # 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 1f3ba3ff..545e47c4 100644 --- a/lib/isabelle/ROOT +++ b/lib/isabelle/ROOT @@ -3,10 +3,11 @@ session "Sail" = "LEM" + sessions "HOL-Eisbach" theories [document = false] - Sail_values_lemmas - Prompt - State_lemmas - Sail_operators_mwords_lemmas - Sail_operators_bitlists + Sail2_values_lemmas + Sail2_prompt + Sail2_state_lemmas + Sail2_operators_mwords_lemmas + Sail2_operators_bitlists + Sail2_string Hoare document_files "root.tex" diff --git a/lib/isabelle/Sail2_operators_mwords_lemmas.thy b/lib/isabelle/Sail2_operators_mwords_lemmas.thy new file mode 100644 index 00000000..ae8802f2 --- /dev/null +++ b/lib/isabelle/Sail2_operators_mwords_lemmas.thy @@ -0,0 +1,112 @@ +theory Sail2_operators_mwords_lemmas + imports Sail2_operators_mwords +begin + +lemmas uint_simps[simp] = uint_maybe_def uint_fail_def uint_oracle_def +lemmas sint_simps[simp] = sint_maybe_def sint_fail_def sint_oracle_def + +lemma bools_of_bits_oracle_just_list[simp]: + assumes "just_list (map bool_of_bitU bus) = Some bs" + shows "bools_of_bits_oracle bus = return bs" +proof - + have f: "foreachM bus bools (\b bools. bool_of_bitU_oracle b \ (\b. return (bools @ [b]))) = return (bools @ bs)" + if "just_list (map bool_of_bitU bus) = Some bs" for bus bs bools + proof (use that in \induction bus arbitrary: bs bools\) + case (Cons bu bus bs) + obtain b bs' where bs: "bs = b # bs'" and bu: "bool_of_bitU bu = Some b" + using Cons.prems by (cases bu) (auto split: option.splits) + then show ?case + using Cons.prems Cons.IH[where bs = bs' and bools = "bools @ [b]"] + by (cases bu) (auto simp: bool_of_bitU_oracle_def split: option.splits) + qed auto + then show ?thesis using f[OF assms, of "[]"] unfolding bools_of_bits_oracle_def + by auto +qed + +lemma of_bits_mword_return_of_bl[simp]: + assumes "just_list (map bool_of_bitU bus) = Some bs" + shows "of_bits_oracle BC_mword bus = return (of_bl bs)" + and "of_bits_fail BC_mword bus = return (of_bl bs)" + by (auto simp: of_bits_oracle_def of_bits_fail_def maybe_fail_def assms BC_mword_defs) + +lemma vec_of_bits_of_bl[simp]: + assumes "just_list (map bool_of_bitU bus) = Some bs" + shows "vec_of_bits_maybe bus = Some (of_bl bs)" + and "vec_of_bits_fail bus = return (of_bl bs)" + and "vec_of_bits_oracle bus = return (of_bl bs)" + and "vec_of_bits_failwith bus = of_bl bs" + and "vec_of_bits bus = of_bl bs" + unfolding vec_of_bits_maybe_def vec_of_bits_fail_def vec_of_bits_oracle_def + vec_of_bits_failwith_def vec_of_bits_def + by (auto simp: assms) + +lemmas access_vec_dec_test_bit[simp] = access_bv_dec_mword[folded access_vec_dec_def] + +lemma access_vec_inc_test_bit[simp]: + fixes w :: "('a::len) word" + assumes "n \ 0" and "nat n < LENGTH('a)" + shows "access_vec_inc w n = bitU_of_bool (w !! (LENGTH('a) - 1 - nat n))" + using assms + by (auto simp: access_vec_inc_def access_bv_inc_def access_list_def BC_mword_defs rev_nth test_bit_bl) + +lemma bool_of_bitU_monadic_simps[simp]: + "bool_of_bitU_fail B0 = return False" + "bool_of_bitU_fail B1 = return True" + "bool_of_bitU_fail BU = Fail ''bool_of_bitU''" + "bool_of_bitU_oracle B0 = return False" + "bool_of_bitU_oracle B1 = return True" + "bool_of_bitU_oracle BU = undefined_bool ()" + unfolding bool_of_bitU_fail_def bool_of_bitU_oracle_def + by auto + +lemma update_vec_dec_simps[simp]: + "update_vec_dec_maybe w i B0 = Some (set_bit w (nat i) False)" + "update_vec_dec_maybe w i B1 = Some (set_bit w (nat i) True)" + "update_vec_dec_maybe w i BU = None" + "update_vec_dec_fail w i B0 = return (set_bit w (nat i) False)" + "update_vec_dec_fail w i B1 = return (set_bit w (nat i) True)" + "update_vec_dec_fail w i BU = Fail ''bool_of_bitU''" + "update_vec_dec_oracle w i B0 = return (set_bit w (nat i) False)" + "update_vec_dec_oracle w i B1 = return (set_bit w (nat i) True)" + "update_vec_dec_oracle w i BU = undefined_bool () \ (\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_oracle_def update_vec_dec_def + by (auto simp: update_mword_dec_def update_mword_bool_dec_def maybe_failwith_def) + +lemma len_of_minus_One_minus_nonneg_lt_len_of[simp]: + "n \ 0 \ nat (int LENGTH('a::len) - 1 - n) < LENGTH('a)" + by (metis diff_mono diff_zero len_gt_0 nat_eq_iff2 nat_less_iff order_refl zle_diff1_eq) + +declare extz_vec_def[simp] +declare exts_vec_def[simp] +declare concat_vec_def[simp] + +lemma msb_Bits_msb[simp]: + "msb w = bitU_of_bool (Bits.msb w)" + by (auto simp: msb_def most_significant_def BC_mword_defs word_msb_alt split: list.splits) + +declare and_vec_def[simp] +declare or_vec_def[simp] +declare xor_vec_def[simp] +declare not_vec_def[simp] + +lemma arith_vec_simps[simp]: + "add_vec l r = l + r" + "sub_vec l r = l - r" + "mult_vec l r = (ucast l) * (ucast r)" + unfolding add_vec_def sub_vec_def mult_vec_def + by (auto simp: int_of_mword_def word_add_def word_sub_wi word_mult_def) + +declare adds_vec_def[simp] +declare subs_vec_def[simp] +declare mults_vec_def[simp] + +lemma arith_vec_int_simps[simp]: + "add_vec_int l r = l + (word_of_int r)" + "sub_vec_int l r = l - (word_of_int r)" + "mult_vec_int l r = (ucast l) * (word_of_int r)" + unfolding add_vec_int_def sub_vec_int_def mult_vec_int_def + by (auto simp: arith_op_bv_int_def BC_mword_defs word_add_def word_sub_wi word_mult_def) + +end diff --git a/lib/isabelle/Sail2_prompt_monad_lemmas.thy b/lib/isabelle/Sail2_prompt_monad_lemmas.thy new file mode 100644 index 00000000..08c9b33c --- /dev/null +++ b/lib/isabelle/Sail2_prompt_monad_lemmas.thy @@ -0,0 +1,171 @@ +theory Sail2_prompt_monad_lemmas + imports + Sail2_prompt_monad + Sail2_values_lemmas +begin + +notation bind (infixr "\" 54) + +abbreviation seq :: "('rv,unit,'e)monad \ ('rv,'b,'e)monad \('rv,'b,'e)monad" (infixr "\" 54) where + "m \ n \ m \ (\_. n)" + +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 Exception] = bind.induct + +lemma bind_return[simp]: "bind (return a) f = f a" + by (auto simp: return_def) +lemma bind_return_right[simp]: "bind x return = x" by (induction x) (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 bind_assert_True[simp]: "bind (assert_exp True msg) f = f ()" + by (auto simp: assert_exp_def) + +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 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 \ '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_tag: "((Write_tag a v k), e_write_tag a 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" +| Undefined : "((Undefined k), e_undefined v, k v) \ T" +| Print: "((Print msg k), e_print msg, 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_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') \ 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" + | (Undefined) v k t' where "m = Undefined k" and "t = e_undefined v # t'" and "(k v, t', m') \ Traces" + | (Print) msg k t' where "m = Print msg k" and "t = e_print msg # 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/Sail2_state_lemmas.thy b/lib/isabelle/Sail2_state_lemmas.thy new file mode 100644 index 00000000..124722ab --- /dev/null +++ b/lib/isabelle/Sail2_state_lemmas.thy @@ -0,0 +1,276 @@ +theory Sail2_state_lemmas + imports Sail2_state Sail2_state_lifting +begin + +lemma All_liftState_dom: "liftState_dom (r, m)" + by (induction m) (auto intro: liftState.domintros) +termination liftState using All_liftState_dom by auto + +named_theorems liftState_simp + +lemma liftState_bind[liftState_simp]: + "liftState r (bind m f) = bindS (liftState r m) (liftState r \ f)" + by (induction m f rule: bind.induct) auto + +lemma liftState_return[liftState_simp]: "liftState r (return a) = returnS a" by (auto simp: return_def) + +lemma Value_liftState_Run: + assumes "(Value a, s') \ 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) + +lemmas liftState_if_distrib[liftState_simp] = if_distrib[where f = "liftState ra" for ra] + +lemma liftState_throw[liftState_simp]: "liftState r (throw e) = throwS e" + by (auto simp: throw_def) +lemma liftState_assert[liftState_simp]: "liftState r (assert_exp c msg) = assert_expS c msg" + by (auto simp: assert_exp_def assert_expS_def) +lemma liftState_exit[liftState_simp]: "liftState r (exit0 ()) = exitS ()" + by (auto simp: exit0_def exitS_def) +lemma liftState_exclResult[liftState_simp]: "liftState r (excl_result ()) = excl_resultS ()" + by (auto simp: excl_result_def liftState_simp) +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_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" + by (auto simp: maybe_fail_def maybe_failS_def liftState_simp split: option.splits) +lemma liftState_and_boolM[liftState_simp]: + "liftState r (and_boolM x y) = and_boolS (liftState r x) (liftState r y)" + by (auto simp: and_boolM_def and_boolS_def liftState_simp cong: bindS_cong if_cong) +lemma liftState_or_boolM[liftState_simp]: + "liftState r (or_boolM x y) = or_boolS (liftState r x) (liftState r y)" + by (auto simp: or_boolM_def or_boolS_def liftState_simp cong: bindS_cong if_cong) + +lemma liftState_try_catch[liftState_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[liftState_simp]: + "liftState r (early_return r) = early_returnS r" + by (auto simp: early_return_def early_returnS_def liftState_simp) + +lemma liftState_catch_early_return[liftState_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 liftState_simp cong: sum.case_cong) + +lemma liftState_liftR[liftState_simp]: + "liftState r (liftR m) = liftRS (liftState r m)" + by (auto simp: liftR_def liftRS_def liftState_simp) + +lemma liftState_try_catchR[liftState_simp]: + "liftState r (try_catchR m h) = try_catchRS (liftState r m) (liftState r \ h)" + by (auto simp: try_catchR_def try_catchRS_def sum.case_distrib liftState_simp cong: sum.case_cong) + +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_mem[liftState_simp]: + "\a. liftState r (read_mem BC_mword BC_mword rk a sz) = read_memS BC_mword BC_mword rk a sz" + "\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) + +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) + +lemma liftState_write_mem_ea[liftState_simp]: + "\a. liftState r (write_mem_ea BC_mword rk a sz) = write_mem_eaS BC_mword rk a (nat sz)" + "\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_val: + "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 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 updateS_def returnS_def bindS_readS) + +lemma liftState_iter_aux[liftState_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 simp: liftState_simp cong: bindS_cong) + +lemma liftState_iteri[liftState_simp]: + "liftState r (iteri f xs) = iteriS (\i x. liftState r (f i x)) xs" + by (auto simp: iteri_def iteriS_def liftState_simp) + +lemma liftState_iter[liftState_simp]: + "liftState r (iter f xs) = iterS (liftState r \ f) xs" + by (auto simp: iter_def iterS_def liftState_simp) + +lemma liftState_foreachM[liftState_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 simp: liftState_simp cong: bindS_cong) + +lemma whileS_dom_step: + assumes "whileS_dom (vars, cond, body, s)" + and "(Value True, s') \ cond vars s" + and "(Value vars', s'') \ 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 IH by auto + qed auto + then show ?case by (auto simp: liftState_simp) + 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 liftState_simp) + qed auto + qed auto +qed + +(* Simplification rules for monadic Boolean connectives *) + +lemma if_return_return[simp]: "(if a then return True else return False) = return a" by auto + +lemma and_boolM_simps[simp]: + "and_boolM (return b) (return c) = return (b \ c)" + "and_boolM x (return True) = x" + "and_boolM x (return False) = x \ (\_. return False)" + "\x y z. and_boolM (x \ y) z = (x \ (\r. and_boolM (y r) z))" + by (auto simp: and_boolM_def) + +lemma and_boolM_return_if: + "and_boolM (return b) y = (if b then y else return False)" + by (auto simp: and_boolM_def) + +lemmas and_boolM_if_distrib[simp] = if_distrib[where f = "\x. and_boolM x y" for y] + +lemma or_boolM_simps[simp]: + "or_boolM (return b) (return c) = return (b \ c)" + "or_boolM x (return True) = x \ (\_. return True)" + "or_boolM x (return False) = x" + "\x y z. or_boolM (x \ y) z = (x \ (\r. or_boolM (y r) z))" + by (auto simp: or_boolM_def) + +lemma or_boolM_return_if: + "or_boolM (return b) y = (if b then return True else y)" + by (auto simp: or_boolM_def) + +lemmas or_boolM_if_distrib[simp] = if_distrib[where f = "\x. or_boolM x y" for y] + +lemma if_returnS_returnS[simp]: "(if a then returnS True else returnS False) = returnS a" by auto + +lemma and_boolS_simps[simp]: + "and_boolS (returnS b) (returnS c) = returnS (b \ c)" + "and_boolS x (returnS True) = x" + "and_boolS x (returnS False) = bindS x (\_. returnS False)" + "\x y z. and_boolS (bindS x y) z = (bindS x (\r. and_boolS (y r) z))" + by (auto simp: and_boolS_def) + +lemma and_boolS_returnS_if: + "and_boolS (returnS b) y = (if b then y else returnS False)" + by (auto simp: and_boolS_def) + +lemmas and_boolS_if_distrib[simp] = if_distrib[where f = "\x. and_boolS x y" for y] + +lemma or_boolS_simps[simp]: + "or_boolS (returnS b) (returnS c) = returnS (b \ c)" + "or_boolS x (returnS True) = bindS x (\_. returnS True)" + "or_boolS x (returnS False) = x" + "\x y z. or_boolS (bindS x y) z = (bindS x (\r. or_boolS (y r) z))" + by (auto simp: or_boolS_def) + +lemma or_boolS_returnS_if: + "or_boolS (returnS b) y = (if b then returnS True else y)" + by (auto simp: or_boolS_def) + +lemmas or_boolS_if_distrib[simp] = if_distrib[where f = "\x. or_boolS x y" for y] + +end diff --git a/lib/isabelle/Sail2_state_monad_lemmas.thy b/lib/isabelle/Sail2_state_monad_lemmas.thy new file mode 100644 index 00000000..b705de4c --- /dev/null +++ b/lib/isabelle/Sail2_state_monad_lemmas.thy @@ -0,0 +1,232 @@ +theory Sail2_state_monad_lemmas + imports + Sail2_state_monad + Sail2_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*) + +lemma bindS_ext_cong[fundef_cong]: + assumes m: "m1 s = m2 s" + and f: "\a s'. (Value a, s') \ (m2 s) \ f1 a s' = f2 a s'" + shows "bindS m1 f1 s = bindS m2 f2 s" + using assms unfolding bindS_def by (auto split: result.splits) + +lemma bindS_cong[fundef_cong]: + assumes m: "m1 = m2" + and f: "\s a s'. (Value a, s') \ (m2 s) \ f1 a s' = f2 a s'" + shows "bindS m1 f1 = bindS m2 f2" + using assms by (intro ext bindS_ext_cong; blast) + +lemma bindS_returnS_left[simp]: "bindS (returnS x) f = f x" + by (auto simp add: bindS_def returnS_def) + +lemma bindS_returnS_right[simp]: "bindS m returnS = (m :: ('regs, 'a, 'e) monadS)" + by (intro ext) (auto simp: bindS_def returnS_def split: result.splits) + +lemma bindS_readS: "bindS (readS f) m = (\s. m (f s) s)" + by (auto simp: bindS_def readS_def returnS_def) + +lemma bindS_updateS: "bindS (updateS f) m = (\s. m () (f s))" + by (auto simp: bindS_def updateS_def returnS_def) + +lemma bindS_assertS_True[simp]: "bindS (assert_expS True msg) f = f ()" + by (auto simp: assert_expS_def) + + +lemma result_cases: + fixes r :: "('a, 'e) result" + obtains (Value) a where "r = Value a" + | (Throw) e where "r = Ex (Throw e)" + | (Failure) msg where "r = Ex (Failure msg)" +proof (cases r) + case (Ex ex) then show ?thesis by (cases ex; auto intro: that) +qed + +lemma result_state_cases: + fixes rs :: "('a, 'e) result \ 's" + obtains (Value) a s where "rs = (Value a, s)" + | (Throw) e s where "rs = (Ex (Throw e), s)" + | (Failure) msg s where "rs = (Ex (Failure msg), s)" +proof - + obtain r s where rs: "rs = (r, s)" by (cases rs) + then show thesis by (cases r rule: result_cases) (auto intro: that) +qed + +lemma monadS_ext_eqI: + fixes m m' :: "('regs, 'a, 'e) monadS" + assumes "\a s'. (Value a, s') \ m s \ (Value a, s') \ m' s" + and "\e s'. (Ex (Throw e), s') \ m s \ (Ex (Throw e), s') \ m' s" + and "\msg s'. (Ex (Failure msg), s') \ m s \ (Ex (Failure msg), s') \ m' s" + shows "m s = m' s" +proof (intro set_eqI) + fix x + show "x \ m s \ x \ m' s" using assms by (cases x rule: result_state_cases) auto +qed + +lemma monadS_eqI: + fixes m m' :: "('regs, 'a, 'e) monadS" + assumes "\s a s'. (Value a, s') \ m s \ (Value a, s') \ m' s" + and "\s e s'. (Ex (Throw e), s') \ m s \ (Ex (Throw e), s') \ m' s" + and "\s msg s'. (Ex (Failure msg), s') \ m s \ (Ex (Failure msg), s') \ m' s" + shows "m = m'" + using assms by (intro ext monadS_ext_eqI) + +lemma bindS_cases: + assumes "(r, s') \ bindS m f s" + obtains (Value) a a' s'' where "r = Value a" and "(Value a', s'') \ m s" and "(Value a, s') \ f a' s''" + | (Ex_Left) e where "r = Ex e" and "(Ex e, s') \ m s" + | (Ex_Right) e a s'' where "r = Ex e" and "(Value a, s'') \ m s" and "(Ex e, s') \ f a s''" + using assms by (cases r; auto simp: bindS_def split: result.splits) + +lemma bindS_intros: + "\m f s a s' a' s''. (Value a', s'') \ m s \ (Value a, s') \ f a' s'' \ (Value a, s') \ bindS m f s" + "\m f s e s'. (Ex e, s') \ m s \ (Ex e, s') \ bindS m f s" + "\m f s e s' a s''. (Ex e, s') \ f a s'' \ (Value a, s'') \ m s \ (Ex e, s') \ bindS m f s" + by (auto simp: bindS_def intro: bexI[rotated]) + +lemma bindS_assoc[simp]: "bindS (bindS m f) g = bindS m (\x. bindS (f x) g)" + by (auto elim!: bindS_cases intro: bindS_intros monadS_eqI) + +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) +declare seqS_def[simp] + +lemma Value_bindS_elim: + assumes "(Value a, s') \ bindS m f s" + obtains s'' a' where "(Value a', s'') \ m s" and "(Value a, s') \ f a' s''" + using assms by (auto elim: bindS_cases) + +lemma Ex_bindS_elim: + assumes "(Ex e, s') \ bindS m f s" + obtains (Left) "(Ex e, s') \ m s" + | (Right) s'' a' where "(Value a', s'') \ m s" and "(Ex e, s') \ f a' s''" + using assms by (auto elim: bindS_cases) + +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 returnS_def failS_def throwS_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 + +lemma try_catchS_cases: + assumes "(r, s') \ try_catchS m h s" + obtains (Value) a where "r = Value a" and "(Value a, s') \ m s" + | (Fail) msg where "r = Ex (Failure msg)" and "(Ex (Failure msg), s') \ m s" + | (h) e s'' where "(Ex (Throw e), s'') \ m s" and "(r, s') \ h e s''" + using assms + by (cases r rule: result_cases) (auto simp: try_catchS_def returnS_def split: result.splits ex.splits) + +lemma try_catchS_intros: + "\m h s a s'. (Value a, s') \ m s \ (Value a, s') \ try_catchS m h s" + "\m h s msg s'. (Ex (Failure msg), s') \ m s \ (Ex (Failure msg), s') \ try_catchS m h s" + "\m h s e s'' r s'. (Ex (Throw e), s'') \ m s \ (r, s') \ h e s'' \ (r, s') \ try_catchS m h s" + by (auto simp: try_catchS_def returnS_def intro: bexI[rotated]) + +lemma no_Ex_basic_builtins[simp]: + "\s e s' a. (Ex e, s') \ returnS a s \ False" + "\s e s' f. (Ex e, s') \ readS f s \ False" + "\s e s' f. (Ex e, s') \ updateS f s \ False" + "\s e s' xs. (Ex e, s') \ chooseS xs s \ False" + by (auto simp: readS_def updateS_def returnS_def chooseS_def) + +fun ignore_throw_aux :: "(('a, 'e1) result \ 's) \ (('a, 'e2) result \ 's) set" where + "ignore_throw_aux (Value a, s') = {(Value a, s')}" +| "ignore_throw_aux (Ex (Throw e), s') = {}" +| "ignore_throw_aux (Ex (Failure msg), s') = {(Ex (Failure msg), s')}" +definition "ignore_throw m s \ \(ignore_throw_aux ` m s)" + +lemma ignore_throw_cong: + assumes "\s. m1 s = m2 s" + shows "ignore_throw m1 = ignore_throw m2" + using assms by (auto simp: ignore_throw_def) + +lemma ignore_throw_aux_member_simps[simp]: + "(Value a, s') \ ignore_throw_aux ms \ ms = (Value a, s')" + "(Ex (Throw e), s') \ ignore_throw_aux ms \ False" + "(Ex (Failure msg), s') \ ignore_throw_aux ms \ ms = (Ex (Failure msg), s')" + by (cases ms rule: result_state_cases; auto)+ + +lemma ignore_throw_member_simps[simp]: + "(Value a, s') \ ignore_throw m s \ (Value a, s') \ m s" + "(Value a, s') \ ignore_throw m s \ (Value a, s') \ m s" + "(Ex (Throw e), s') \ ignore_throw m s \ False" + "(Ex (Failure msg), s') \ ignore_throw m s \ (Ex (Failure msg), s') \ m s" + by (auto simp: ignore_throw_def) + +lemma ignore_throw_cases: + assumes no_throw: "ignore_throw m s = m s" + and r: "(r, s') \ m s" + obtains (Value) a where "r = Value a" + | (Failure) msg where "r = Ex (Failure msg)" + using r unfolding no_throw[symmetric] + by (cases r rule: result_cases) (auto simp: ignore_throw_def) + +lemma ignore_throw_bindS[simp]: + "ignore_throw (bindS m f) = bindS (ignore_throw m) (ignore_throw \ f)" + by (intro monadS_eqI) (auto simp: ignore_throw_def elim!: bindS_cases intro: bindS_intros) + +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 "try_catchS (bindS m1 f) h s = bindS (ignore_throw m1) (\a. try_catchS (f a) h) s" + by (intro monadS_ext_eqI; + auto elim!: bindS_cases try_catchS_cases elim: ignore_throw_cases[OF m1]; + auto simp: ignore_throw_def intro: bindS_intros try_catchS_intros) + also have "\ = bindS m2 (\a. try_catchS (f a) h) s" using m2 by (intro bindS_ext_cong) auto + finally show "try_catchS (bindS m1 f) h s = bindS m2 (\a. try_catchS (f a) h) s" . +qed + +lemma no_throw_basic_builtins[simp]: + "ignore_throw (returnS a) = returnS a" + "\f. ignore_throw (readS f) = readS f" + "\f. ignore_throw (updateS f) = updateS f" + "ignore_throw (chooseS xs) = chooseS xs" + "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 + by (intro ext; auto split: option.splits)+ + +lemmas ignore_throw_option_case_distrib = + option.case_distrib[where h = "\c. ignore_throw c s" and option = "c s" for c s] + +lemma no_throw_mem_builtins: + "\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" + "\BC a t s. ignore_throw (write_tagS BC a t) s = write_tagS BC a t s" + "\s. ignore_throw (excl_resultS ()) s = excl_resultS () s" + "\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 + 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) + +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) + +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: 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 + +(* end *) + +end diff --git a/lib/isabelle/Sail2_values_lemmas.thy b/lib/isabelle/Sail2_values_lemmas.thy new file mode 100644 index 00000000..b50d8942 --- /dev/null +++ b/lib/isabelle/Sail2_values_lemmas.thy @@ -0,0 +1,206 @@ +theory Sail2_values_lemmas + imports Sail2_values +begin + +lemma nat_of_int_nat_simps[simp]: "nat_of_int = nat" by (auto simp: nat_of_int_def) + +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 + +lemma repeat_singleton_replicate[simp]: + "repeat [x] n = replicate (nat n) x" +proof (induction n) + case (nonneg n) + have "nat (1 + int m) = Suc m" for m by auto + then show ?case by (induction n) auto +next + case (neg n) + then show ?case by auto +qed + +lemma bool_of_bitU_simps[simp]: + "bool_of_bitU B0 = Some False" + "bool_of_bitU B1 = Some True" + "bool_of_bitU BU = None" + by (auto simp: bool_of_bitU_def) + +lemma bitops_bitU_of_bool[simp]: + "and_bit (bitU_of_bool x) (bitU_of_bool y) = bitU_of_bool (x \ y)" + "or_bit (bitU_of_bool x) (bitU_of_bool y) = bitU_of_bool (x \ y)" + "xor_bit (bitU_of_bool x) (bitU_of_bool y) = bitU_of_bool ((x \ y) \ \(x \ y))" + "not_bit (bitU_of_bool x) = bitU_of_bool (\x)" + "not_bit \ bitU_of_bool = bitU_of_bool \ Not" + by (auto simp: bitU_of_bool_def not_bit_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 = Some" + "bool_of_bitU \ (bitU_of_bool \ f) = Some \ f" + "bool_of_bitU (bitU_of_bool x) = Some x" + by (intro ext, auto simp: bool_of_bitU_def bitU_of_bool_def)+ + +abbreviation "BC_bitU_list \ instance_Sail2_values_Bitvector_list_dict instance_Sail2_values_BitU_Sail2_values_bitU_dict" +lemmas BC_bitU_list_def = instance_Sail2_values_Bitvector_list_dict_def instance_Sail2_values_BitU_Sail2_values_bitU_dict_def +abbreviation "BC_mword \ instance_Sail2_values_Bitvector_Machine_word_mword_dict" +lemmas BC_mword_defs = instance_Sail2_values_Bitvector_Machine_word_mword_dict_def + access_mword_def access_mword_inc_def access_mword_dec_def + (*update_mword_def update_mword_inc_def update_mword_dec_def*) + subrange_list_def subrange_list_inc_def subrange_list_dec_def + update_subrange_list_def update_subrange_list_inc_def update_subrange_list_dec_def + +declare size_itself_int_def[simp] +declare size_itself_def[simp] +declare word_size[simp] + +lemma int_of_mword_simps[simp]: + "int_of_mword False w = uint w" + "int_of_mword True w = sint w" + "int_of_bv BC_mword False w = Some (uint w)" + "int_of_bv BC_mword True w = Some (sint w)" + by (auto simp: int_of_mword_def int_of_bv_def BC_mword_defs) + +lemma BC_mword_simps[simp]: + "unsigned_method BC_mword a = Some (uint a)" + "signed_method BC_mword a = Some (sint a)" + "length_method BC_mword (a :: ('a :: len) word) = int (LENGTH('a))" + by (auto simp: BC_mword_defs) + +lemma of_bits_mword_of_bl[simp]: + assumes "just_list (map bool_of_bitU bus) = Some bs" + shows "of_bits_method BC_mword bus = Some (of_bl bs)" + and "of_bits_failwith BC_mword bus = of_bl bs" + using assms by (auto simp: BC_mword_defs of_bits_failwith_def maybe_failwith_def) + +lemma nat_of_bits_aux_bl_to_bin_aux: + "nat_of_bools_aux acc bs = nat (bl_to_bin_aux bs (int acc))" + by (induction acc bs rule: nat_of_bools_aux.induct) + (auto simp: Bit_def intro!: arg_cong[where f = nat] arg_cong2[where f = bl_to_bin_aux] split: if_splits) + +lemma nat_of_bits_bl_to_bin[simp]: + "nat_of_bools bs = nat (bl_to_bin bs)" + by (auto simp: nat_of_bools_def bl_to_bin_def nat_of_bits_aux_bl_to_bin_aux) + +lemma unsigned_bits_of_mword[simp]: + "unsigned_method BC_bitU_list (bits_of_method BC_mword a) = Some (uint a)" + by (auto simp: BC_bitU_list_def BC_mword_defs unsigned_of_bits_def unsigned_of_bools_def) + +lemma bits_of_bitU_list[simp]: + "bits_of_method BC_bitU_list v = v" + "of_bits_method BC_bitU_list v = Some v" + by (auto simp: BC_bitU_list_def) + +lemma subrange_list_inc_drop_take: + "subrange_list_inc xs i j = drop (nat i) (take (nat (j + 1)) xs)" + by (auto simp: subrange_list_inc_def split_at_def) + +lemma subrange_list_dec_drop_take: + assumes "i \ 0" and "j \ 0" + shows "subrange_list_dec xs i j = drop (length xs - nat (i + 1)) (take (length xs - nat j) xs)" + using assms unfolding subrange_list_dec_def + by (auto simp: subrange_list_inc_drop_take add.commute diff_diff_add nat_minus_as_int) + +lemma update_subrange_list_inc_drop_take: + assumes "i \ 0" and "j \ i" + shows "update_subrange_list_inc xs i j xs' = take (nat i) xs @ xs' @ drop (nat (j + 1)) xs" + using assms unfolding update_subrange_list_inc_def + by (auto simp: split_at_def min_def) + +lemma update_subrange_list_dec_drop_take: + assumes "j \ 0" and "i \ j" + shows "update_subrange_list_dec xs i j xs' = take (length xs - nat (i + 1)) xs @ xs' @ drop (length xs - nat j) xs" + using assms unfolding update_subrange_list_dec_def update_subrange_list_inc_def + by (auto simp: split_at_def min_def Let_def add.commute diff_diff_add nat_minus_as_int) + +declare access_list_inc_def[simp] + +lemma access_list_dec_rev_nth: + assumes "0 \ i" and "nat i < length xs" + shows "access_list_dec xs i = rev xs ! (nat i)" + using assms + by (auto simp: access_list_dec_def rev_nth intro!: arg_cong2[where f = List.nth]) + +lemma access_bv_dec_mword[simp]: + fixes w :: "('a::len) word" + assumes "0 \ n" and "nat n < LENGTH('a)" + shows "access_bv_dec BC_mword w n = bitU_of_bool (w !! (nat n))" + using assms unfolding access_bv_dec_def access_list_def + by (auto simp: access_list_dec_rev_nth BC_mword_defs rev_map test_bit_bl) + +lemma access_list_dec_nth[simp]: + assumes "0 \ i" + shows "access_list_dec xs i = xs ! (length xs - nat (i + 1))" + using assms + by (auto simp: access_list_dec_def add.commute diff_diff_add nat_minus_as_int) + +lemma update_list_inc_update[simp]: + "update_list_inc xs n x = xs[nat n := x]" + by (auto simp: update_list_inc_def) + +lemma update_list_dec_update[simp]: + "update_list_dec xs n x = xs[length xs - nat (n + 1) := x]" + by (auto simp: update_list_dec_def add.commute diff_diff_add nat_minus_as_int) + +lemma bools_of_nat_aux_simps[simp]: + "\len. len \ 0 \ bools_of_nat_aux len x acc = acc" + "\len. bools_of_nat_aux (int (Suc len)) x acc = + bools_of_nat_aux (int len) (x div 2) ((if x mod 2 = 1 then True else False) # acc)" + by auto +declare bools_of_nat_aux.simps[simp del] + +lemma bools_of_nat_aux_bin_to_bl_aux: + "bools_of_nat_aux len n acc = bin_to_bl_aux (nat len) (int n) acc" +proof (cases len) + case (nonneg len') + show ?thesis unfolding nonneg + proof (induction len' arbitrary: n acc) + case (Suc len'' n acc) + then show ?case + using zmod_int[of n 2] + by (auto simp del: of_nat_simps simp add: bin_rest_def bin_last_def zdiv_int) + qed auto +qed auto + +lemma bools_of_nat_bin_to_bl[simp]: + "bools_of_nat len n = bin_to_bl (nat len) (int n)" + by (auto simp: bools_of_nat_def bools_of_nat_aux_bin_to_bl_aux) + +lemma add_one_bool_ignore_overflow_aux_rbl_succ[simp]: + "add_one_bool_ignore_overflow_aux xs = rbl_succ xs" + by (induction xs) auto + +lemma add_one_bool_ignore_overflow_rbl_succ[simp]: + "add_one_bool_ignore_overflow xs = rev (rbl_succ (rev xs))" + unfolding add_one_bool_ignore_overflow_def by auto + +lemma map_Not_bin_to_bl: + "map Not (bin_to_bl_aux len n acc) = bin_to_bl_aux len (-n - 1) (map Not acc)" +proof (induction len arbitrary: n acc) + case (Suc len n acc) + moreover have "(- (n div 2) - 1) = ((-n - 1) div 2)" by auto + moreover have "(n mod 2 = 0) = ((- n - 1) mod 2 = 1)" by presburger + ultimately show ?case by (auto simp: bin_rest_def bin_last_def) +qed auto + +lemma bools_of_int_bin_to_bl[simp]: + "bools_of_int (int len) n = bin_to_bl len n" + by (auto simp: bools_of_int_def Let_def map_Not_bin_to_bl rbl_succ[unfolded bin_to_bl_def]) + +end diff --git a/lib/isabelle/Sail_operators_mwords_lemmas.thy b/lib/isabelle/Sail_operators_mwords_lemmas.thy deleted file mode 100644 index 22c35e1f..00000000 --- a/lib/isabelle/Sail_operators_mwords_lemmas.thy +++ /dev/null @@ -1,112 +0,0 @@ -theory "Sail_operators_mwords_lemmas" - imports Sail_operators_mwords -begin - -lemmas uint_simps[simp] = uint_maybe_def uint_fail_def uint_oracle_def -lemmas sint_simps[simp] = sint_maybe_def sint_fail_def sint_oracle_def - -lemma bools_of_bits_oracle_just_list[simp]: - assumes "just_list (map bool_of_bitU bus) = Some bs" - shows "bools_of_bits_oracle bus = return bs" -proof - - have f: "foreachM bus bools (\b bools. bool_of_bitU_oracle b \ (\b. return (bools @ [b]))) = return (bools @ bs)" - if "just_list (map bool_of_bitU bus) = Some bs" for bus bs bools - proof (use that in \induction bus arbitrary: bs bools\) - case (Cons bu bus bs) - obtain b bs' where bs: "bs = b # bs'" and bu: "bool_of_bitU bu = Some b" - using Cons.prems by (cases bu) (auto split: option.splits) - then show ?case - using Cons.prems Cons.IH[where bs = bs' and bools = "bools @ [b]"] - by (cases bu) (auto simp: bool_of_bitU_oracle_def split: option.splits) - qed auto - then show ?thesis using f[OF assms, of "[]"] unfolding bools_of_bits_oracle_def - by auto -qed - -lemma of_bits_mword_return_of_bl[simp]: - assumes "just_list (map bool_of_bitU bus) = Some bs" - shows "of_bits_oracle BC_mword bus = return (of_bl bs)" - and "of_bits_fail BC_mword bus = return (of_bl bs)" - by (auto simp: of_bits_oracle_def of_bits_fail_def maybe_fail_def assms BC_mword_defs) - -lemma vec_of_bits_of_bl[simp]: - assumes "just_list (map bool_of_bitU bus) = Some bs" - shows "vec_of_bits_maybe bus = Some (of_bl bs)" - and "vec_of_bits_fail bus = return (of_bl bs)" - and "vec_of_bits_oracle bus = return (of_bl bs)" - and "vec_of_bits_failwith bus = of_bl bs" - and "vec_of_bits bus = of_bl bs" - unfolding vec_of_bits_maybe_def vec_of_bits_fail_def vec_of_bits_oracle_def - vec_of_bits_failwith_def vec_of_bits_def - by (auto simp: assms) - -lemmas access_vec_dec_test_bit[simp] = access_bv_dec_mword[folded access_vec_dec_def] - -lemma access_vec_inc_test_bit[simp]: - fixes w :: "('a::len) word" - assumes "n \ 0" and "nat n < LENGTH('a)" - shows "access_vec_inc w n = bitU_of_bool (w !! (LENGTH('a) - 1 - nat n))" - using assms - by (auto simp: access_vec_inc_def access_bv_inc_def access_list_def BC_mword_defs rev_nth test_bit_bl) - -lemma bool_of_bitU_monadic_simps[simp]: - "bool_of_bitU_fail B0 = return False" - "bool_of_bitU_fail B1 = return True" - "bool_of_bitU_fail BU = Fail ''bool_of_bitU''" - "bool_of_bitU_oracle B0 = return False" - "bool_of_bitU_oracle B1 = return True" - "bool_of_bitU_oracle BU = undefined_bool ()" - unfolding bool_of_bitU_fail_def bool_of_bitU_oracle_def - by auto - -lemma update_vec_dec_simps[simp]: - "update_vec_dec_maybe w i B0 = Some (set_bit w (nat i) False)" - "update_vec_dec_maybe w i B1 = Some (set_bit w (nat i) True)" - "update_vec_dec_maybe w i BU = None" - "update_vec_dec_fail w i B0 = return (set_bit w (nat i) False)" - "update_vec_dec_fail w i B1 = return (set_bit w (nat i) True)" - "update_vec_dec_fail w i BU = Fail ''bool_of_bitU''" - "update_vec_dec_oracle w i B0 = return (set_bit w (nat i) False)" - "update_vec_dec_oracle w i B1 = return (set_bit w (nat i) True)" - "update_vec_dec_oracle w i BU = undefined_bool () \ (\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_oracle_def update_vec_dec_def - by (auto simp: update_mword_dec_def update_mword_bool_dec_def maybe_failwith_def) - -lemma len_of_minus_One_minus_nonneg_lt_len_of[simp]: - "n \ 0 \ nat (int LENGTH('a::len) - 1 - n) < LENGTH('a)" - by (metis diff_mono diff_zero len_gt_0 nat_eq_iff2 nat_less_iff order_refl zle_diff1_eq) - -declare extz_vec_def[simp] -declare exts_vec_def[simp] -declare concat_vec_def[simp] - -lemma msb_Bits_msb[simp]: - "msb w = bitU_of_bool (Bits.msb w)" - by (auto simp: msb_def most_significant_def BC_mword_defs word_msb_alt split: list.splits) - -declare and_vec_def[simp] -declare or_vec_def[simp] -declare xor_vec_def[simp] -declare not_vec_def[simp] - -lemma arith_vec_simps[simp]: - "add_vec l r = l + r" - "sub_vec l r = l - r" - "mult_vec l r = (ucast l) * (ucast r)" - unfolding add_vec_def sub_vec_def mult_vec_def - by (auto simp: int_of_mword_def word_add_def word_sub_wi word_mult_def) - -declare adds_vec_def[simp] -declare subs_vec_def[simp] -declare mults_vec_def[simp] - -lemma arith_vec_int_simps[simp]: - "add_vec_int l r = l + (word_of_int r)" - "sub_vec_int l r = l - (word_of_int r)" - "mult_vec_int l r = (ucast l) * (word_of_int r)" - unfolding add_vec_int_def sub_vec_int_def mult_vec_int_def - by (auto simp: arith_op_bv_int_def BC_mword_defs word_add_def word_sub_wi word_mult_def) - -end diff --git a/lib/isabelle/Sail_values_lemmas.thy b/lib/isabelle/Sail_values_lemmas.thy deleted file mode 100644 index dd008695..00000000 --- a/lib/isabelle/Sail_values_lemmas.thy +++ /dev/null @@ -1,206 +0,0 @@ -theory Sail_values_lemmas - imports Sail_values -begin - -lemma nat_of_int_nat_simps[simp]: "nat_of_int = nat" by (auto simp: nat_of_int_def) - -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 - -lemma repeat_singleton_replicate[simp]: - "repeat [x] n = replicate (nat n) x" -proof (induction n) - case (nonneg n) - have "nat (1 + int m) = Suc m" for m by auto - then show ?case by (induction n) auto -next - case (neg n) - then show ?case by auto -qed - -lemma bool_of_bitU_simps[simp]: - "bool_of_bitU B0 = Some False" - "bool_of_bitU B1 = Some True" - "bool_of_bitU BU = None" - by (auto simp: bool_of_bitU_def) - -lemma bitops_bitU_of_bool[simp]: - "and_bit (bitU_of_bool x) (bitU_of_bool y) = bitU_of_bool (x \ y)" - "or_bit (bitU_of_bool x) (bitU_of_bool y) = bitU_of_bool (x \ y)" - "xor_bit (bitU_of_bool x) (bitU_of_bool y) = bitU_of_bool ((x \ y) \ \(x \ y))" - "not_bit (bitU_of_bool x) = bitU_of_bool (\x)" - "not_bit \ bitU_of_bool = bitU_of_bool \ Not" - by (auto simp: bitU_of_bool_def not_bit_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 = Some" - "bool_of_bitU \ (bitU_of_bool \ f) = Some \ f" - "bool_of_bitU (bitU_of_bool x) = Some x" - by (intro ext, auto simp: bool_of_bitU_def bitU_of_bool_def)+ - -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_defs = instance_Sail_values_Bitvector_Machine_word_mword_dict_def - access_mword_def access_mword_inc_def access_mword_dec_def - (*update_mword_def update_mword_inc_def update_mword_dec_def*) - subrange_list_def subrange_list_inc_def subrange_list_dec_def - update_subrange_list_def update_subrange_list_inc_def update_subrange_list_dec_def - -declare size_itself_int_def[simp] -declare size_itself_def[simp] -declare word_size[simp] - -lemma int_of_mword_simps[simp]: - "int_of_mword False w = uint w" - "int_of_mword True w = sint w" - "int_of_bv BC_mword False w = Some (uint w)" - "int_of_bv BC_mword True w = Some (sint w)" - by (auto simp: int_of_mword_def int_of_bv_def BC_mword_defs) - -lemma BC_mword_simps[simp]: - "unsigned_method BC_mword a = Some (uint a)" - "signed_method BC_mword a = Some (sint a)" - "length_method BC_mword (a :: ('a :: len) word) = int (LENGTH('a))" - by (auto simp: BC_mword_defs) - -lemma of_bits_mword_of_bl[simp]: - assumes "just_list (map bool_of_bitU bus) = Some bs" - shows "of_bits_method BC_mword bus = Some (of_bl bs)" - and "of_bits_failwith BC_mword bus = of_bl bs" - using assms by (auto simp: BC_mword_defs of_bits_failwith_def maybe_failwith_def) - -lemma nat_of_bits_aux_bl_to_bin_aux: - "nat_of_bools_aux acc bs = nat (bl_to_bin_aux bs (int acc))" - by (induction acc bs rule: nat_of_bools_aux.induct) - (auto simp: Bit_def intro!: arg_cong[where f = nat] arg_cong2[where f = bl_to_bin_aux] split: if_splits) - -lemma nat_of_bits_bl_to_bin[simp]: - "nat_of_bools bs = nat (bl_to_bin bs)" - by (auto simp: nat_of_bools_def bl_to_bin_def nat_of_bits_aux_bl_to_bin_aux) - -lemma unsigned_bits_of_mword[simp]: - "unsigned_method BC_bitU_list (bits_of_method BC_mword a) = Some (uint a)" - by (auto simp: BC_bitU_list_def BC_mword_defs unsigned_of_bits_def unsigned_of_bools_def) - -lemma bits_of_bitU_list[simp]: - "bits_of_method BC_bitU_list v = v" - "of_bits_method BC_bitU_list v = Some v" - by (auto simp: BC_bitU_list_def) - -lemma subrange_list_inc_drop_take: - "subrange_list_inc xs i j = drop (nat i) (take (nat (j + 1)) xs)" - by (auto simp: subrange_list_inc_def split_at_def) - -lemma subrange_list_dec_drop_take: - assumes "i \ 0" and "j \ 0" - shows "subrange_list_dec xs i j = drop (length xs - nat (i + 1)) (take (length xs - nat j) xs)" - using assms unfolding subrange_list_dec_def - by (auto simp: subrange_list_inc_drop_take add.commute diff_diff_add nat_minus_as_int) - -lemma update_subrange_list_inc_drop_take: - assumes "i \ 0" and "j \ i" - shows "update_subrange_list_inc xs i j xs' = take (nat i) xs @ xs' @ drop (nat (j + 1)) xs" - using assms unfolding update_subrange_list_inc_def - by (auto simp: split_at_def min_def) - -lemma update_subrange_list_dec_drop_take: - assumes "j \ 0" and "i \ j" - shows "update_subrange_list_dec xs i j xs' = take (length xs - nat (i + 1)) xs @ xs' @ drop (length xs - nat j) xs" - using assms unfolding update_subrange_list_dec_def update_subrange_list_inc_def - by (auto simp: split_at_def min_def Let_def add.commute diff_diff_add nat_minus_as_int) - -declare access_list_inc_def[simp] - -lemma access_list_dec_rev_nth: - assumes "0 \ i" and "nat i < length xs" - shows "access_list_dec xs i = rev xs ! (nat i)" - using assms - by (auto simp: access_list_dec_def rev_nth intro!: arg_cong2[where f = List.nth]) - -lemma access_bv_dec_mword[simp]: - fixes w :: "('a::len) word" - assumes "0 \ n" and "nat n < LENGTH('a)" - shows "access_bv_dec BC_mword w n = bitU_of_bool (w !! (nat n))" - using assms unfolding access_bv_dec_def access_list_def - by (auto simp: access_list_dec_rev_nth BC_mword_defs rev_map test_bit_bl) - -lemma access_list_dec_nth[simp]: - assumes "0 \ i" - shows "access_list_dec xs i = xs ! (length xs - nat (i + 1))" - using assms - by (auto simp: access_list_dec_def add.commute diff_diff_add nat_minus_as_int) - -lemma update_list_inc_update[simp]: - "update_list_inc xs n x = xs[nat n := x]" - by (auto simp: update_list_inc_def) - -lemma update_list_dec_update[simp]: - "update_list_dec xs n x = xs[length xs - nat (n + 1) := x]" - by (auto simp: update_list_dec_def add.commute diff_diff_add nat_minus_as_int) - -lemma bools_of_nat_aux_simps[simp]: - "\len. len \ 0 \ bools_of_nat_aux len x acc = acc" - "\len. bools_of_nat_aux (int (Suc len)) x acc = - bools_of_nat_aux (int len) (x div 2) ((if x mod 2 = 1 then True else False) # acc)" - by auto -declare bools_of_nat_aux.simps[simp del] - -lemma bools_of_nat_aux_bin_to_bl_aux: - "bools_of_nat_aux len n acc = bin_to_bl_aux (nat len) (int n) acc" -proof (cases len) - case (nonneg len') - show ?thesis unfolding nonneg - proof (induction len' arbitrary: n acc) - case (Suc len'' n acc) - then show ?case - using zmod_int[of n 2] - by (auto simp del: of_nat_simps simp add: bin_rest_def bin_last_def zdiv_int) - qed auto -qed auto - -lemma bools_of_nat_bin_to_bl[simp]: - "bools_of_nat len n = bin_to_bl (nat len) (int n)" - by (auto simp: bools_of_nat_def bools_of_nat_aux_bin_to_bl_aux) - -lemma add_one_bool_ignore_overflow_aux_rbl_succ[simp]: - "add_one_bool_ignore_overflow_aux xs = rbl_succ xs" - by (induction xs) auto - -lemma add_one_bool_ignore_overflow_rbl_succ[simp]: - "add_one_bool_ignore_overflow xs = rev (rbl_succ (rev xs))" - unfolding add_one_bool_ignore_overflow_def by auto - -lemma map_Not_bin_to_bl: - "map Not (bin_to_bl_aux len n acc) = bin_to_bl_aux len (-n - 1) (map Not acc)" -proof (induction len arbitrary: n acc) - case (Suc len n acc) - moreover have "(- (n div 2) - 1) = ((-n - 1) div 2)" by auto - moreover have "(n mod 2 = 0) = ((- n - 1) mod 2 = 1)" by presburger - ultimately show ?case by (auto simp: bin_rest_def bin_last_def) -qed auto - -lemma bools_of_int_bin_to_bl[simp]: - "bools_of_int (int len) n = bin_to_bl len n" - by (auto simp: bools_of_int_def Let_def map_Not_bin_to_bl rbl_succ[unfolded bin_to_bl_def]) - -end diff --git a/lib/isabelle/State_lemmas.thy b/lib/isabelle/State_lemmas.thy deleted file mode 100644 index cf5e4dbf..00000000 --- a/lib/isabelle/State_lemmas.thy +++ /dev/null @@ -1,260 +0,0 @@ -theory State_lemmas - imports State State_lifting -begin - -lemma All_liftState_dom: "liftState_dom (r, m)" - by (induction m) (auto intro: liftState.domintros) -termination liftState using All_liftState_dom by auto - -named_theorems liftState_simp - -lemma liftState_bind[liftState_simp]: - "liftState r (bind m f) = bindS (liftState r m) (liftState r \ f)" - by (induction m f rule: bind.induct) auto - -lemma liftState_return[liftState_simp]: "liftState r (return a) = returnS a" by (auto simp: return_def) - -lemma Value_liftState_Run: - assumes "(Value a, s') \ 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) - -lemmas liftState_if_distrib[liftState_simp] = if_distrib[where f = "liftState ra" for ra] - -lemma liftState_throw[liftState_simp]: "liftState r (throw e) = throwS e" - by (auto simp: throw_def) -lemma liftState_assert[liftState_simp]: "liftState r (assert_exp c msg) = assert_expS c msg" - by (auto simp: assert_exp_def assert_expS_def) -lemma liftState_exit[liftState_simp]: "liftState r (exit0 ()) = exitS ()" - by (auto simp: exit0_def exitS_def) -lemma liftState_exclResult[liftState_simp]: "liftState r (excl_result ()) = excl_resultS ()" - by (auto simp: excl_result_def liftState_simp) -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_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" - by (auto simp: maybe_fail_def maybe_failS_def liftState_simp split: option.splits) -lemma liftState_and_boolM[liftState_simp]: - "liftState r (and_boolM x y) = and_boolS (liftState r x) (liftState r y)" - by (auto simp: and_boolM_def and_boolS_def liftState_simp cong: bindS_cong if_cong) -lemma liftState_or_boolM[liftState_simp]: - "liftState r (or_boolM x y) = or_boolS (liftState r x) (liftState r y)" - by (auto simp: or_boolM_def or_boolS_def liftState_simp cong: bindS_cong if_cong) - -lemma liftState_try_catch[liftState_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[liftState_simp]: - "liftState r (early_return r) = early_returnS r" - by (auto simp: early_return_def early_returnS_def liftState_simp) - -lemma liftState_catch_early_return[liftState_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 liftState_simp cong: sum.case_cong) - -lemma liftState_liftR[liftState_simp]: - "liftState r (liftR m) = liftRS (liftState r m)" - by (auto simp: liftR_def liftRS_def liftState_simp) - -lemma liftState_try_catchR[liftState_simp]: - "liftState r (try_catchR m h) = try_catchRS (liftState r m) (liftState r \ h)" - by (auto simp: try_catchR_def try_catchRS_def sum.case_distrib liftState_simp cong: sum.case_cong) - -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_mem[liftState_simp]: - "\a. liftState r (read_mem BC_mword BC_mword rk a sz) = read_memS BC_mword BC_mword rk a sz" - "\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) - -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) - -lemma liftState_write_mem_ea[liftState_simp]: - "\a. liftState r (write_mem_ea BC_mword rk a sz) = write_mem_eaS BC_mword rk a (nat sz)" - "\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_val: - "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 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 updateS_def returnS_def bindS_readS) - -lemma liftState_iter_aux[liftState_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 simp: liftState_simp cong: bindS_cong) - -lemma liftState_iteri[liftState_simp]: - "liftState r (iteri f xs) = iteriS (\i x. liftState r (f i x)) xs" - by (auto simp: iteri_def iteriS_def liftState_simp) - -lemma liftState_iter[liftState_simp]: - "liftState r (iter f xs) = iterS (liftState r \ f) xs" - by (auto simp: iter_def iterS_def liftState_simp) - -lemma liftState_foreachM[liftState_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 simp: liftState_simp cong: bindS_cong) - -lemma whileS_dom_step: - assumes "whileS_dom (vars, cond, body, s)" - and "(Value True, s') \ cond vars s" - and "(Value vars', s'') \ 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 IH by auto - qed auto - then show ?case by (auto simp: liftState_simp) - 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 liftState_simp) - qed auto - qed auto -qed - -(* Simplification rules for monadic Boolean connectives *) - -lemma if_return_return[simp]: "(if a then return True else return False) = return a" by auto - -lemma and_boolM_simps[simp]: - "and_boolM (return b) y = (if b then y else return False)" - "and_boolM x (return True) = x" - "and_boolM x (return False) = x \ (\_. return False)" - "\x y z. and_boolM (x \ y) z = (x \ (\r. and_boolM (y r) z))" - by (auto simp: and_boolM_def) - -lemmas and_boolM_if_distrib[simp] = if_distrib[where f = "\x. and_boolM x y" for y] - -lemma or_boolM_simps[simp]: - "or_boolM (return b) y = (if b then return True else y)" - "or_boolM x (return True) = x \ (\_. return True)" - "or_boolM x (return False) = x" - "\x y z. or_boolM (x \ y) z = (x \ (\r. or_boolM (y r) z))" - by (auto simp: or_boolM_def) - -lemmas or_boolM_if_distrib[simp] = if_distrib[where f = "\x. or_boolM x y" for y] - -lemma if_returnS_returnS[simp]: "(if a then returnS True else returnS False) = returnS a" by auto - -lemma and_boolS_simps[simp]: - "and_boolS (returnS b) y = (if b then y else returnS False)" - "and_boolS x (returnS True) = x" - "and_boolS x (returnS False) = bindS x (\_. returnS False)" - "\x y z. and_boolS (bindS x y) z = (bindS x (\r. and_boolS (y r) z))" - by (auto simp: and_boolS_def) - -lemmas and_boolS_if_distrib[simp] = if_distrib[where f = "\x. and_boolS x y" for y] - -lemma or_boolS_simps[simp]: - "or_boolS (returnS b) y = (if b then returnS True else y)" - "or_boolS x (returnS True) = bindS x (\_. returnS True)" - "or_boolS x (returnS False) = x" - "\x y z. or_boolS (bindS x y) z = (bindS x (\r. or_boolS (y r) z))" - by (auto simp: or_boolS_def) - -lemmas or_boolS_if_distrib[simp] = if_distrib[where f = "\x. or_boolS x y" for y] - -end diff --git a/lib/isabelle/State_monad_lemmas.thy b/lib/isabelle/State_monad_lemmas.thy deleted file mode 100644 index e0d684ba..00000000 --- a/lib/isabelle/State_monad_lemmas.thy +++ /dev/null @@ -1,232 +0,0 @@ -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*) - -lemma bindS_ext_cong[fundef_cong]: - assumes m: "m1 s = m2 s" - and f: "\a s'. (Value a, s') \ (m2 s) \ f1 a s' = f2 a s'" - shows "bindS m1 f1 s = bindS m2 f2 s" - using assms unfolding bindS_def by (auto split: result.splits) - -lemma bindS_cong[fundef_cong]: - assumes m: "m1 = m2" - and f: "\s a s'. (Value a, s') \ (m2 s) \ f1 a s' = f2 a s'" - shows "bindS m1 f1 = bindS m2 f2" - using assms by (intro ext bindS_ext_cong; blast) - -lemma bindS_returnS_left[simp]: "bindS (returnS x) f = f x" - by (auto simp add: bindS_def returnS_def) - -lemma bindS_returnS_right[simp]: "bindS m returnS = (m :: ('regs, 'a, 'e) monadS)" - by (intro ext) (auto simp: bindS_def returnS_def split: result.splits) - -lemma bindS_readS: "bindS (readS f) m = (\s. m (f s) s)" - by (auto simp: bindS_def readS_def returnS_def) - -lemma bindS_updateS: "bindS (updateS f) m = (\s. m () (f s))" - by (auto simp: bindS_def updateS_def returnS_def) - -lemma bindS_assertS_True[simp]: "bindS (assert_expS True msg) f = f ()" - by (auto simp: assert_expS_def) - - -lemma result_cases: - fixes r :: "('a, 'e) result" - obtains (Value) a where "r = Value a" - | (Throw) e where "r = Ex (Throw e)" - | (Failure) msg where "r = Ex (Failure msg)" -proof (cases r) - case (Ex ex) then show ?thesis by (cases ex; auto intro: that) -qed - -lemma result_state_cases: - fixes rs :: "('a, 'e) result \ 's" - obtains (Value) a s where "rs = (Value a, s)" - | (Throw) e s where "rs = (Ex (Throw e), s)" - | (Failure) msg s where "rs = (Ex (Failure msg), s)" -proof - - obtain r s where rs: "rs = (r, s)" by (cases rs) - then show thesis by (cases r rule: result_cases) (auto intro: that) -qed - -lemma monadS_ext_eqI: - fixes m m' :: "('regs, 'a, 'e) monadS" - assumes "\a s'. (Value a, s') \ m s \ (Value a, s') \ m' s" - and "\e s'. (Ex (Throw e), s') \ m s \ (Ex (Throw e), s') \ m' s" - and "\msg s'. (Ex (Failure msg), s') \ m s \ (Ex (Failure msg), s') \ m' s" - shows "m s = m' s" -proof (intro set_eqI) - fix x - show "x \ m s \ x \ m' s" using assms by (cases x rule: result_state_cases) auto -qed - -lemma monadS_eqI: - fixes m m' :: "('regs, 'a, 'e) monadS" - assumes "\s a s'. (Value a, s') \ m s \ (Value a, s') \ m' s" - and "\s e s'. (Ex (Throw e), s') \ m s \ (Ex (Throw e), s') \ m' s" - and "\s msg s'. (Ex (Failure msg), s') \ m s \ (Ex (Failure msg), s') \ m' s" - shows "m = m'" - using assms by (intro ext monadS_ext_eqI) - -lemma bindS_cases: - assumes "(r, s') \ bindS m f s" - obtains (Value) a a' s'' where "r = Value a" and "(Value a', s'') \ m s" and "(Value a, s') \ f a' s''" - | (Ex_Left) e where "r = Ex e" and "(Ex e, s') \ m s" - | (Ex_Right) e a s'' where "r = Ex e" and "(Value a, s'') \ m s" and "(Ex e, s') \ f a s''" - using assms by (cases r; auto simp: bindS_def split: result.splits) - -lemma bindS_intros: - "\m f s a s' a' s''. (Value a', s'') \ m s \ (Value a, s') \ f a' s'' \ (Value a, s') \ bindS m f s" - "\m f s e s'. (Ex e, s') \ m s \ (Ex e, s') \ bindS m f s" - "\m f s e s' a s''. (Ex e, s') \ f a s'' \ (Value a, s'') \ m s \ (Ex e, s') \ bindS m f s" - by (auto simp: bindS_def intro: bexI[rotated]) - -lemma bindS_assoc[simp]: "bindS (bindS m f) g = bindS m (\x. bindS (f x) g)" - by (auto elim!: bindS_cases intro: bindS_intros monadS_eqI) - -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) -declare seqS_def[simp] - -lemma Value_bindS_elim: - assumes "(Value a, s') \ bindS m f s" - obtains s'' a' where "(Value a', s'') \ m s" and "(Value a, s') \ f a' s''" - using assms by (auto elim: bindS_cases) - -lemma Ex_bindS_elim: - assumes "(Ex e, s') \ bindS m f s" - obtains (Left) "(Ex e, s') \ m s" - | (Right) s'' a' where "(Value a', s'') \ m s" and "(Ex e, s') \ f a' s''" - using assms by (auto elim: bindS_cases) - -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 returnS_def failS_def throwS_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 - -lemma try_catchS_cases: - assumes "(r, s') \ try_catchS m h s" - obtains (Value) a where "r = Value a" and "(Value a, s') \ m s" - | (Fail) msg where "r = Ex (Failure msg)" and "(Ex (Failure msg), s') \ m s" - | (h) e s'' where "(Ex (Throw e), s'') \ m s" and "(r, s') \ h e s''" - using assms - by (cases r rule: result_cases) (auto simp: try_catchS_def returnS_def split: result.splits ex.splits) - -lemma try_catchS_intros: - "\m h s a s'. (Value a, s') \ m s \ (Value a, s') \ try_catchS m h s" - "\m h s msg s'. (Ex (Failure msg), s') \ m s \ (Ex (Failure msg), s') \ try_catchS m h s" - "\m h s e s'' r s'. (Ex (Throw e), s'') \ m s \ (r, s') \ h e s'' \ (r, s') \ try_catchS m h s" - by (auto simp: try_catchS_def returnS_def intro: bexI[rotated]) - -lemma no_Ex_basic_builtins[simp]: - "\s e s' a. (Ex e, s') \ returnS a s \ False" - "\s e s' f. (Ex e, s') \ readS f s \ False" - "\s e s' f. (Ex e, s') \ updateS f s \ False" - "\s e s' xs. (Ex e, s') \ chooseS xs s \ False" - by (auto simp: readS_def updateS_def returnS_def chooseS_def) - -fun ignore_throw_aux :: "(('a, 'e1) result \ 's) \ (('a, 'e2) result \ 's) set" where - "ignore_throw_aux (Value a, s') = {(Value a, s')}" -| "ignore_throw_aux (Ex (Throw e), s') = {}" -| "ignore_throw_aux (Ex (Failure msg), s') = {(Ex (Failure msg), s')}" -definition "ignore_throw m s \ \(ignore_throw_aux ` m s)" - -lemma ignore_throw_cong: - assumes "\s. m1 s = m2 s" - shows "ignore_throw m1 = ignore_throw m2" - using assms by (auto simp: ignore_throw_def) - -lemma ignore_throw_aux_member_simps[simp]: - "(Value a, s') \ ignore_throw_aux ms \ ms = (Value a, s')" - "(Ex (Throw e), s') \ ignore_throw_aux ms \ False" - "(Ex (Failure msg), s') \ ignore_throw_aux ms \ ms = (Ex (Failure msg), s')" - by (cases ms rule: result_state_cases; auto)+ - -lemma ignore_throw_member_simps[simp]: - "(Value a, s') \ ignore_throw m s \ (Value a, s') \ m s" - "(Value a, s') \ ignore_throw m s \ (Value a, s') \ m s" - "(Ex (Throw e), s') \ ignore_throw m s \ False" - "(Ex (Failure msg), s') \ ignore_throw m s \ (Ex (Failure msg), s') \ m s" - by (auto simp: ignore_throw_def) - -lemma ignore_throw_cases: - assumes no_throw: "ignore_throw m s = m s" - and r: "(r, s') \ m s" - obtains (Value) a where "r = Value a" - | (Failure) msg where "r = Ex (Failure msg)" - using r unfolding no_throw[symmetric] - by (cases r rule: result_cases) (auto simp: ignore_throw_def) - -lemma ignore_throw_bindS[simp]: - "ignore_throw (bindS m f) = bindS (ignore_throw m) (ignore_throw \ f)" - by (intro monadS_eqI) (auto simp: ignore_throw_def elim!: bindS_cases intro: bindS_intros) - -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 "try_catchS (bindS m1 f) h s = bindS (ignore_throw m1) (\a. try_catchS (f a) h) s" - by (intro monadS_ext_eqI; - auto elim!: bindS_cases try_catchS_cases elim: ignore_throw_cases[OF m1]; - auto simp: ignore_throw_def intro: bindS_intros try_catchS_intros) - also have "\ = bindS m2 (\a. try_catchS (f a) h) s" using m2 by (intro bindS_ext_cong) auto - finally show "try_catchS (bindS m1 f) h s = bindS m2 (\a. try_catchS (f a) h) s" . -qed - -lemma no_throw_basic_builtins[simp]: - "ignore_throw (returnS a) = returnS a" - "\f. ignore_throw (readS f) = readS f" - "\f. ignore_throw (updateS f) = updateS f" - "ignore_throw (chooseS xs) = chooseS xs" - "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 - by (intro ext; auto split: option.splits)+ - -lemmas ignore_throw_option_case_distrib = - option.case_distrib[where h = "\c. ignore_throw c s" and option = "c s" for c s] - -lemma no_throw_mem_builtins: - "\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" - "\BC a t s. ignore_throw (write_tagS BC a t) s = write_tagS BC a t s" - "\s. ignore_throw (excl_resultS ()) s = excl_resultS () s" - "\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 - 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) - -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) - -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: 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 - -(* end *) - -end diff --git a/lib/isabelle/manual/Manual.thy b/lib/isabelle/manual/Manual.thy index 0c83ebea..6cd90a9a 100644 --- a/lib/isabelle/manual/Manual.thy +++ b/lib/isabelle/manual/Manual.thy @@ -1,8 +1,8 @@ (*<*) theory Manual imports - Sail.State_lemmas - Sail.Sail_operators_mwords_lemmas + Sail.Sail2_state_lemmas + Sail.Sail2_operators_mwords_lemmas Sail.Hoare Riscv_duopod.Riscv_duopod_lemmas begin @@ -183,7 +183,7 @@ Vectors in Sail are mapped to lists in Isabelle, except for bitvectors, which ar Both increasing and decreasing indexing order are supported by having two versions for each operation that involves indexing, such as @{term update_list_inc} and @{term update_list_dec}, or @{term subrange_list_inc} and @{term subrange_list_dec}. These operations are defined in the -theory @{theory Sail_values}, while @{theory Sail_values_lemmas} provides simplification rules +theory @{theory Sail2_values}, while @{theory Sail2_values_lemmas} provides simplification rules such as @{lemma "access_list_inc xs i = xs ! nat i" by auto} \\ @@ -209,7 +209,7 @@ into multiple clauses with concrete bitvector lengths. This is not enabled by d so Sail generates Lem definitions using bit lists unless the @{verbatim "-lem_mwords"} command line flag is used. -The theory @{theory Sail_values} defines a (Lem) typeclass @{verbatim Bitvector}, which provides +The theory @{theory Sail2_values} defines a (Lem) typeclass @{verbatim Bitvector}, which provides an interface to some basic bitvector operations and has instantiations for both bit lists and machine words. It is mainly intended for internal use in the Sail library,\<^footnote>\Lem typeclasses are not very convenient to use in Isabelle, as they get translated to dictionaries that have to be passed to functions @@ -219,7 +219,7 @@ representations. For use in Sail specifications, wrappers are defined in the th right theory is automatically added to the generated files, depending on which bitvector representation is used. Hence, bitvector operations can be referred to in the Sail source code using uniform names, e.g.~@{term add_vec}, @{term update_vec_dec}, or @{term subrange_vec_inc}. -The theory @{theory Sail_operators_mwords_lemmas} sets up simplification rules that relate these +The theory @{theory Sail2_operators_mwords_lemmas} sets up simplification rules that relate these operations to the native operations in Isabelle, e.g. @{lemma "add_vec l r = l + r" by simp} \\ @@ -235,8 +235,8 @@ for integration with relaxed memory models. For the sequential case, we use a s exceptions and nondeterminism). The generated definitions use the free monad, and the sequential case is supported via a lifting -to the state monad defined in the theory @{theory State}. Simplification rules are set up in the -theory @{theory State_lemmas}, allowing seamless reasoning about the generated definitions in terms +to the state monad defined in the theory @{theory Sail2_state}. Simplification rules are set up in the +theory @{theory Sail2_state_lemmas}, allowing seamless reasoning about the generated definitions in terms of the state monad.\ subsubsection \State Monad \label{sec:state-monad}\ @@ -308,7 +308,7 @@ instances.\ subsubsection \Free Monad \label{sec:free-monad}\ -text \In addition to the state monad, the theory @{theory Prompt_monad} defines a free monad of an +text \In addition to the state monad, the theory @{theory Sail2_prompt_monad} defines a free monad of an effect datatype. A monadic expression either returns a pure value @{term a}, denoted @{term "Done a"}, or it has an effect. The latter can be a failure or an exception, or an effect together with a continuation. For example, @{term \Read_reg ''PC'' k\} represents a request to @@ -383,7 +383,7 @@ register state record: Sail aims to generate Isabelle definitions that can be used with either the state or the free monad. To achieve this, the definitions are generated using the free monad, and a lifting to the state monad is provided together with simplification rules. These include generic simplification rules -(proved in the theory @{theory State_lemmas}) such as +(proved in the theory @{theory Sail2_state_lemmas}) such as @{thm [display] liftState_return[where r = "(get_regval, set_regval)"] liftState_bind[where r = "(get_regval, set_regval)"] diff --git a/src/gen_lib/sail2_prompt.lem b/src/gen_lib/sail2_prompt.lem index 434df843..08a47052 100644 --- a/src/gen_lib/sail2_prompt.lem +++ b/src/gen_lib/sail2_prompt.lem @@ -2,7 +2,7 @@ open import Pervasives_extra (*open import Sail_impl_base*) open import Sail2_values open import Sail2_prompt_monad -open import {isabelle} `Prompt_monad_lemmas` +open import {isabelle} `Sail2_prompt_monad_lemmas` val (>>=) : forall 'rv 'a 'b 'e. monad 'rv 'a 'e -> ('a -> monad 'rv 'b 'e) -> monad 'rv 'b 'e declare isabelle target_rep function (>>=) = infix `\` diff --git a/src/gen_lib/sail2_string.lem b/src/gen_lib/sail2_string.lem index a54ffa65..3374d800 100644 --- a/src/gen_lib/sail2_string.lem +++ b/src/gen_lib/sail2_string.lem @@ -30,10 +30,8 @@ let string_append = stringAppend ***********************************************) val maybeIntegerOfString : string -> maybe integer - +let maybeIntegerOfString _ = Nothing (* TODO FIXME *) declare ocaml target_rep function maybeIntegerOfString = `(fun s -> match int_of_string_opt s with None -> None | Some i -> Some (Nat_big_num.of_int i))` -declare isabelle target_rep function maybeIntegerOfString = `maybeIntegerOfString` (* TODO FIXME *) -declare hol target_rep function maybeIntegerOfString = `maybeIntegerOfString` (* TODO FIXME *) (*********************************************** * end stuff that should be in Lem Num_extra * @@ -65,10 +63,12 @@ let rec n_leading_spaces s = (* match len with * (\* | 0 -> 0 *\) * (\* | 1 -> *\) - * | len -> *) match nth s 0 with - | #' ' -> 1 + (n_leading_spaces (string_sub s 1 (len - 1))) - | _ -> 0 - end + * | len -> *) + (* Isabelle generation for pattern matching on characters + is currently broken, so use an if-expression *) + if nth s 0 = #' ' + then 1 + (n_leading_spaces (string_sub s 1 (len - 1))) + else 0 (* end *) let opt_spc_matches_prefix s = -- cgit v1.2.3