Add some lemmas about bitvectors

Also clean up some library functions a bit, and add some missing failure
handling variants of division operations on bitvectors.

1 files changed, 88 insertions, 9 deletions

diff --git a/lib/isabelle/Sail_values_lemmas.thy b/lib/isabelle/Sail_values_lemmas.thy
index 256e76d0..dd008695 100644
--- a/lib/isabelle/Sail_values_lemmas.thy
+++ b/lib/isabelle/Sail_values_lemmas.thy
@@ -23,6 +23,23 @@ lemma just_list_cases:
         | (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 \<and> y)"
   "or_bit (bitU_of_bool x) (bitU_of_bool y) = bitU_of_bool (x \<or> y)"
@@ -49,11 +66,28 @@ lemmas BC_mword_defs = instance_Sail_values_Bitvector_Machine_word_mword_dict_de
   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 word_size)
+  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))"
@@ -97,12 +131,6 @@ lemma update_subrange_list_dec_drop_take:
 
 declare access_list_inc_def[simp]
 
-lemma access_list_dec_nth:
-  assumes "0 \<le> 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 access_list_dec_rev_nth:
   assumes "0 \<le> i" and "nat i < length xs"
   shows "access_list_dec xs i = rev xs ! (nat i)"
@@ -114,14 +142,65 @@ lemma access_bv_dec_mword[simp]:
   assumes "0 \<le> 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 word_size)
+  by (auto simp: access_list_dec_rev_nth BC_mword_defs rev_map test_bit_bl)
+
+lemma access_list_dec_nth[simp]:
+  assumes "0 \<le> 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:
+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]:
+  "\<And>len. len \<le> 0 \<Longrightarrow> bools_of_nat_aux len x acc = acc"
+  "\<And>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