diff options
Diffstat (limited to 'lib/isabelle/Sail2_operators_mwords_lemmas.thy')
| -rw-r--r-- | lib/isabelle/Sail2_operators_mwords_lemmas.thy | 95 |
1 files changed, 76 insertions, 19 deletions
diff --git a/lib/isabelle/Sail2_operators_mwords_lemmas.thy b/lib/isabelle/Sail2_operators_mwords_lemmas.thy index ae8802f2..fd54c93a 100644 --- a/lib/isabelle/Sail2_operators_mwords_lemmas.thy +++ b/lib/isabelle/Sail2_operators_mwords_lemmas.thy @@ -2,14 +2,14 @@ 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 +lemmas uint_simps[simp] = uint_maybe_def uint_fail_def uint_nondet_def +lemmas sint_simps[simp] = sint_maybe_def sint_fail_def sint_nondet_def -lemma bools_of_bits_oracle_just_list[simp]: +lemma bools_of_bits_nondet_just_list[simp]: assumes "just_list (map bool_of_bitU bus) = Some bs" - shows "bools_of_bits_oracle bus = return bs" + shows "bools_of_bits_nondet bus = return bs" proof - - have f: "foreachM bus bools (\<lambda>b bools. bool_of_bitU_oracle b \<bind> (\<lambda>b. return (bools @ [b]))) = return (bools @ bs)" + have f: "foreachM bus bools (\<lambda>b bools. bool_of_bitU_nondet b \<bind> (\<lambda>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 \<open>induction bus arbitrary: bs bools\<close>) case (Cons bu bus bs) @@ -17,26 +17,26 @@ proof - 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) + by (cases bu) (auto simp: bool_of_bitU_nondet_def split: option.splits) qed auto - then show ?thesis using f[OF assms, of "[]"] unfolding bools_of_bits_oracle_def + then show ?thesis using f[OF assms, of "[]"] unfolding bools_of_bits_nondet_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)" + shows "of_bits_nondet 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) + by (auto simp: of_bits_nondet_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_nondet 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 + unfolding vec_of_bits_maybe_def vec_of_bits_fail_def vec_of_bits_nondet_def vec_of_bits_failwith_def vec_of_bits_def by (auto simp: assms) @@ -53,10 +53,10 @@ 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 + "bool_of_bitU_nondet B0 = return False" + "bool_of_bitU_nondet B1 = return True" + "bool_of_bitU_nondet BU = undefined_bool ()" + unfolding bool_of_bitU_fail_def bool_of_bitU_nondet_def by auto lemma update_vec_dec_simps[simp]: @@ -66,18 +66,69 @@ lemma update_vec_dec_simps[simp]: "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 () \<bind> (\<lambda>b. return (set_bit w (nat i) b))" + "update_vec_dec_nondet w i B0 = return (set_bit w (nat i) False)" + "update_vec_dec_nondet w i B1 = return (set_bit w (nat i) True)" + "update_vec_dec_nondet w i BU = undefined_bool () \<bind> (\<lambda>b. return (set_bit w (nat i) b))" "update_vec_dec 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 + unfolding update_vec_dec_maybe_def update_vec_dec_fail_def update_vec_dec_nondet_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 \<ge> 0 \<Longrightarrow> 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 subrange_vec_dec_def[simp] + +lemma update_subrange_vec_dec_update_subrange_list_dec: + assumes "0 \<le> j" and "j \<le> i" and "i < int LENGTH('a)" + shows "update_subrange_vec_dec (w :: 'a::len word) i j w' = + of_bl (update_subrange_list_dec (to_bl w) i j (to_bl w'))" + using assms + unfolding update_subrange_vec_dec_def update_subrange_list_dec_def update_subrange_list_inc_def + by (auto simp: word_update_def split_at_def Let_def nat_diff_distrib min_def) + +lemma subrange_vec_dec_subrange_list_dec: + assumes "0 \<le> j" and "j \<le> i" and "i < int LENGTH('a)" and "int LENGTH('b) = i - j + 1" + shows "subrange_vec_dec (w :: 'a::len word) i j = (of_bl (subrange_list_dec (to_bl w) i j) :: 'b::len word)" + using assms unfolding subrange_vec_dec_def + by (auto simp: subrange_list_dec_drop_take slice_take of_bl_drop') + +lemma slice_simp[simp]: "slice w lo len = Word.slice (nat lo) w" + by (auto simp: slice_def) + +declare slice_id[simp] + +lemma of_bools_of_bl[simp]: "of_bools_method BC_mword = of_bl" + by (auto simp: BC_mword_defs) + +lemma of_bl_bin_word_of_int: + "len = LENGTH('a) \<Longrightarrow> of_bl (bin_to_bl_aux len n []) = (word_of_int n :: ('a::len) word)" + by (auto simp: of_bl_def bin_bl_bin') + +lemma get_slice_int_0_bin_to_bl[simp]: + "len > 0 \<Longrightarrow> get_slice_int len n 0 = of_bl (bin_to_bl (nat len) n)" + unfolding get_slice_int_def get_slice_int_bv_def subrange_list_def + by (auto simp: subrange_list_dec_drop_take len_bin_to_bl_aux) + +lemma to_bl_of_bl[simp]: + fixes bl :: "bool list" + defines w: "w \<equiv> of_bl bl :: 'a::len word" + assumes len: "length bl = LENGTH('a)" + shows "to_bl w = bl" + using len unfolding w by (intro word_bl.Abs_inverse) auto + +lemma reverse_endianness_byte[simp]: + "LENGTH('a) = 8 \<Longrightarrow> reverse_endianness (w :: 'a::len word) = w" + unfolding reverse_endianness_def by (auto simp: reverse_endianness_list_simps) + +lemma reverse_reverse_endianness[simp]: + "8 dvd LENGTH('a) \<Longrightarrow> reverse_endianness (reverse_endianness w) = (w :: 'a::len word)" + unfolding reverse_endianness_def by (simp) + +lemma replicate_bits_zero[simp]: "replicate_bits 0 n = 0" + by (intro word_eqI) (auto simp: replicate_bits_def test_bit_of_bl rev_nth nth_repeat simp del: repeat.simps) + declare extz_vec_def[simp] declare exts_vec_def[simp] declare concat_vec_def[simp] @@ -109,4 +160,10 @@ lemma arith_vec_int_simps[simp]: 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) +lemma shiftl_simp[simp]: "shiftl w l = w << (nat l)" + by (auto simp: shiftl_def shiftl_mword_def) + +lemma shiftr_simp[simp]: "shiftr w l = w >> (nat l)" + by (auto simp: shiftr_def shiftr_mword_def) + end |