--- a/src/HOL/Library/Bit_Operations.thy Sat Oct 17 11:32:03 2020 +0100
+++ b/src/HOL/Library/Bit_Operations.thy Sat Oct 17 18:36:08 2020 +0100
@@ -9,6 +9,41 @@
Main
begin
+lemma sub_BitM_One_eq:
+ \<open>(Num.sub (Num.BitM n) num.One) = 2 * (Num.sub n Num.One :: int)\<close>
+ by (cases n) simp_all
+
+lemma bit_not_int_iff':
+ \<open>bit (- k - 1) n \<longleftrightarrow> \<not> bit k n\<close>
+ for k :: int
+proof (induction n arbitrary: k)
+ case 0
+ show ?case
+ by simp
+next
+ case (Suc n)
+ have \<open>(- k - 1) div 2 = - (k div 2) - 1\<close>
+ by simp
+ with Suc show ?case
+ by (simp add: bit_Suc)
+qed
+
+lemma bit_minus_int_iff:
+ \<open>bit (- k) n \<longleftrightarrow> \<not> bit (k - 1) n\<close>
+ for k :: int
+ using bit_not_int_iff' [of \<open>k - 1\<close>] by simp
+
+lemma bit_numeral_int_simps [simp]:
+ \<open>bit (1 :: int) (numeral n) \<longleftrightarrow> bit (0 :: int) (pred_numeral n)\<close>
+ \<open>bit (numeral (num.Bit0 w) :: int) (numeral n) \<longleftrightarrow> bit (numeral w :: int) (pred_numeral n)\<close>
+ \<open>bit (numeral (num.Bit1 w) :: int) (numeral n) \<longleftrightarrow> bit (numeral w :: int) (pred_numeral n)\<close>
+ \<open>bit (numeral (Num.BitM w) :: int) (numeral n) \<longleftrightarrow> \<not> bit (- numeral w :: int) (pred_numeral n)\<close>
+ \<open>bit (- numeral (num.Bit0 w) :: int) (numeral n) \<longleftrightarrow> bit (- numeral w :: int) (pred_numeral n)\<close>
+ \<open>bit (- numeral (num.Bit1 w) :: int) (numeral n) \<longleftrightarrow> \<not> bit (numeral w :: int) (pred_numeral n)\<close>
+ \<open>bit (- numeral (Num.BitM w) :: int) (numeral n) \<longleftrightarrow> bit (- (numeral w) :: int) (pred_numeral n)\<close>
+ by (simp_all add: bit_1_iff numeral_eq_Suc bit_Suc add_One sub_inc_One_eq bit_minus_int_iff)
+
+
subsection \<open>Bit operations\<close>
class semiring_bit_operations = semiring_bit_shifts +
@@ -574,8 +609,8 @@
lemma bit_not_int_iff:
\<open>bit (NOT k) n \<longleftrightarrow> \<not> bit k n\<close>
- for k :: int
- by (induction n arbitrary: k) (simp_all add: not_int_div_2 even_not_iff_int bit_Suc)
+ for k :: int
+ by (simp add: bit_not_int_iff' not_int_def)
function and_int :: \<open>int \<Rightarrow> int \<Rightarrow> int\<close>
where \<open>(k::int) AND l = (if k \<in> {0, - 1} \<and> l \<in> {0, - 1}
@@ -771,6 +806,112 @@
\<open>k XOR l < 0 \<longleftrightarrow> (k < 0) \<noteq> (l < 0)\<close> for k l :: int
by (subst Not_eq_iff [symmetric]) (auto simp add: not_less)
+lemma OR_upper: \<^marker>\<open>contributor \<open>Stefan Berghofer\<close>\<close>
+ fixes x y :: int
+ assumes "0 \<le> x" "x < 2 ^ n" "y < 2 ^ n"
+ shows "x OR y < 2 ^ n"
+using assms proof (induction x arbitrary: y n rule: int_bit_induct)
+ case zero
+ then show ?case
+ by simp
+next
+ case minus
+ then show ?case
+ by simp
+next
+ case (even x)
+ from even.IH [of \<open>n - 1\<close> \<open>y div 2\<close>] even.prems even.hyps
+ show ?case
+ by (cases n) (auto simp add: or_int_rec [of \<open>_ * 2\<close>] elim: oddE)
+next
+ case (odd x)
+ from odd.IH [of \<open>n - 1\<close> \<open>y div 2\<close>] odd.prems odd.hyps
+ show ?case
+ by (cases n) (auto simp add: or_int_rec [of \<open>1 + _ * 2\<close>], linarith)
+qed
+
+lemma XOR_upper: \<^marker>\<open>contributor \<open>Stefan Berghofer\<close>\<close>
+ fixes x y :: int
+ assumes "0 \<le> x" "x < 2 ^ n" "y < 2 ^ n"
+ shows "x XOR y < 2 ^ n"
+using assms proof (induction x arbitrary: y n rule: int_bit_induct)
+ case zero
+ then show ?case
+ by simp
+next
+ case minus
+ then show ?case
+ by simp
+next
+ case (even x)
+ from even.IH [of \<open>n - 1\<close> \<open>y div 2\<close>] even.prems even.hyps
+ show ?case
+ by (cases n) (auto simp add: xor_int_rec [of \<open>_ * 2\<close>] elim: oddE)
+next
+ case (odd x)
+ from odd.IH [of \<open>n - 1\<close> \<open>y div 2\<close>] odd.prems odd.hyps
+ show ?case
+ by (cases n) (auto simp add: xor_int_rec [of \<open>1 + _ * 2\<close>])
+qed
+
+lemma AND_lower [simp]: \<^marker>\<open>contributor \<open>Stefan Berghofer\<close>\<close>
+ fixes x y :: int
+ assumes "0 \<le> x"
+ shows "0 \<le> x AND y"
+ using assms by simp
+
+lemma OR_lower [simp]: \<^marker>\<open>contributor \<open>Stefan Berghofer\<close>\<close>
+ fixes x y :: int
+ assumes "0 \<le> x" "0 \<le> y"
+ shows "0 \<le> x OR y"
+ using assms by simp
+
+lemma XOR_lower [simp]: \<^marker>\<open>contributor \<open>Stefan Berghofer\<close>\<close>
+ fixes x y :: int
+ assumes "0 \<le> x" "0 \<le> y"
+ shows "0 \<le> x XOR y"
+ using assms by simp
+
+lemma AND_upper1 [simp]: \<^marker>\<open>contributor \<open>Stefan Berghofer\<close>\<close>
+ fixes x y :: int
+ assumes "0 \<le> x"
+ shows "x AND y \<le> x"
+ using assms by (induction x arbitrary: y rule: int_bit_induct)
+ (simp_all add: and_int_rec [of \<open>_ * 2\<close>] and_int_rec [of \<open>1 + _ * 2\<close>] add_increasing)
+
+lemmas AND_upper1' [simp] = order_trans [OF AND_upper1] \<^marker>\<open>contributor \<open>Stefan Berghofer\<close>\<close>
+lemmas AND_upper1'' [simp] = order_le_less_trans [OF AND_upper1] \<^marker>\<open>contributor \<open>Stefan Berghofer\<close>\<close>
+
+lemma AND_upper2 [simp]: \<^marker>\<open>contributor \<open>Stefan Berghofer\<close>\<close>
+ fixes x y :: int
+ assumes "0 \<le> y"
+ shows "x AND y \<le> y"
+ using assms AND_upper1 [of y x] by (simp add: ac_simps)
+
+lemmas AND_upper2' [simp] = order_trans [OF AND_upper2] \<^marker>\<open>contributor \<open>Stefan Berghofer\<close>\<close>
+lemmas AND_upper2'' [simp] = order_le_less_trans [OF AND_upper2] \<^marker>\<open>contributor \<open>Stefan Berghofer\<close>\<close>
+
+lemma plus_and_or: \<open>(x AND y) + (x OR y) = x + y\<close> for x y :: int
+proof (induction x arbitrary: y rule: int_bit_induct)
+ case zero
+ then show ?case
+ by simp
+next
+ case minus
+ then show ?case
+ by simp
+next
+ case (even x)
+ from even.IH [of \<open>y div 2\<close>]
+ show ?case
+ by (auto simp add: and_int_rec [of _ y] or_int_rec [of _ y] elim: oddE)
+next
+ case (odd x)
+ from odd.IH [of \<open>y div 2\<close>]
+ show ?case
+ by (auto simp add: and_int_rec [of _ y] or_int_rec [of _ y] elim: oddE)
+qed
+
lemma set_bit_nonnegative_int_iff [simp]:
\<open>set_bit n k \<ge> 0 \<longleftrightarrow> k \<ge> 0\<close> for k :: int
by (simp add: set_bit_def)
@@ -926,6 +1067,114 @@
end
+text \<open>FIXME: The rule sets below are very large (24 rules for each
+ operator). Is there a simpler way to do this?\<close>
+
+context
+begin
+
+private lemma eqI:
+ \<open>k = l\<close>
+ if num: \<open>\<And>n. bit k (numeral n) \<longleftrightarrow> bit l (numeral n)\<close>
+ and even: \<open>even k \<longleftrightarrow> even l\<close>
+ for k l :: int
+proof (rule bit_eqI)
+ fix n
+ show \<open>bit k n \<longleftrightarrow> bit l n\<close>
+ proof (cases n)
+ case 0
+ with even show ?thesis
+ by simp
+ next
+ case (Suc n)
+ with num [of \<open>num_of_nat (Suc n)\<close>] show ?thesis
+ by (simp only: numeral_num_of_nat)
+ qed
+qed
+
+lemma int_and_numerals [simp]:
+ "numeral (Num.Bit0 x) AND numeral (Num.Bit0 y) = (2 :: int) * (numeral x AND numeral y)"
+ "numeral (Num.Bit0 x) AND numeral (Num.Bit1 y) = (2 :: int) * (numeral x AND numeral y)"
+ "numeral (Num.Bit1 x) AND numeral (Num.Bit0 y) = (2 :: int) * (numeral x AND numeral y)"
+ "numeral (Num.Bit1 x) AND numeral (Num.Bit1 y) = 1 + (2 :: int) * (numeral x AND numeral y)"
+ "numeral (Num.Bit0 x) AND - numeral (Num.Bit0 y) = (2 :: int) * (numeral x AND - numeral y)"
+ "numeral (Num.Bit0 x) AND - numeral (Num.Bit1 y) = (2 :: int) * (numeral x AND - numeral (y + Num.One))"
+ "numeral (Num.Bit1 x) AND - numeral (Num.Bit0 y) = (2 :: int) * (numeral x AND - numeral y)"
+ "numeral (Num.Bit1 x) AND - numeral (Num.Bit1 y) = 1 + (2 :: int) * (numeral x AND - numeral (y + Num.One))"
+ "- numeral (Num.Bit0 x) AND numeral (Num.Bit0 y) = (2 :: int) * (- numeral x AND numeral y)"
+ "- numeral (Num.Bit0 x) AND numeral (Num.Bit1 y) = (2 :: int) * (- numeral x AND numeral y)"
+ "- numeral (Num.Bit1 x) AND numeral (Num.Bit0 y) = (2 :: int) * (- numeral (x + Num.One) AND numeral y)"
+ "- numeral (Num.Bit1 x) AND numeral (Num.Bit1 y) = 1 + (2 :: int) * (- numeral (x + Num.One) AND numeral y)"
+ "- numeral (Num.Bit0 x) AND - numeral (Num.Bit0 y) = (2 :: int) * (- numeral x AND - numeral y)"
+ "- numeral (Num.Bit0 x) AND - numeral (Num.Bit1 y) = (2 :: int) * (- numeral x AND - numeral (y + Num.One))"
+ "- numeral (Num.Bit1 x) AND - numeral (Num.Bit0 y) = (2 :: int) * (- numeral (x + Num.One) AND - numeral y)"
+ "- numeral (Num.Bit1 x) AND - numeral (Num.Bit1 y) = 1 + (2 :: int) * (- numeral (x + Num.One) AND - numeral (y + Num.One))"
+ "(1::int) AND numeral (Num.Bit0 y) = 0"
+ "(1::int) AND numeral (Num.Bit1 y) = 1"
+ "(1::int) AND - numeral (Num.Bit0 y) = 0"
+ "(1::int) AND - numeral (Num.Bit1 y) = 1"
+ "numeral (Num.Bit0 x) AND (1::int) = 0"
+ "numeral (Num.Bit1 x) AND (1::int) = 1"
+ "- numeral (Num.Bit0 x) AND (1::int) = 0"
+ "- numeral (Num.Bit1 x) AND (1::int) = 1"
+ by (auto simp add: bit_and_iff bit_minus_iff even_and_iff bit_double_iff even_bit_succ_iff add_One sub_inc_One_eq intro: eqI)
+
+lemma int_or_numerals [simp]:
+ "numeral (Num.Bit0 x) OR numeral (Num.Bit0 y) = (2 :: int) * (numeral x OR numeral y)"
+ "numeral (Num.Bit0 x) OR numeral (Num.Bit1 y) = 1 + (2 :: int) * (numeral x OR numeral y)"
+ "numeral (Num.Bit1 x) OR numeral (Num.Bit0 y) = 1 + (2 :: int) * (numeral x OR numeral y)"
+ "numeral (Num.Bit1 x) OR numeral (Num.Bit1 y) = 1 + (2 :: int) * (numeral x OR numeral y)"
+ "numeral (Num.Bit0 x) OR - numeral (Num.Bit0 y) = (2 :: int) * (numeral x OR - numeral y)"
+ "numeral (Num.Bit0 x) OR - numeral (Num.Bit1 y) = 1 + (2 :: int) * (numeral x OR - numeral (y + Num.One))"
+ "numeral (Num.Bit1 x) OR - numeral (Num.Bit0 y) = 1 + (2 :: int) * (numeral x OR - numeral y)"
+ "numeral (Num.Bit1 x) OR - numeral (Num.Bit1 y) = 1 + (2 :: int) * (numeral x OR - numeral (y + Num.One))"
+ "- numeral (Num.Bit0 x) OR numeral (Num.Bit0 y) = (2 :: int) * (- numeral x OR numeral y)"
+ "- numeral (Num.Bit0 x) OR numeral (Num.Bit1 y) = 1 + (2 :: int) * (- numeral x OR numeral y)"
+ "- numeral (Num.Bit1 x) OR numeral (Num.Bit0 y) = 1 + (2 :: int) * (- numeral (x + Num.One) OR numeral y)"
+ "- numeral (Num.Bit1 x) OR numeral (Num.Bit1 y) = 1 + (2 :: int) * (- numeral (x + Num.One) OR numeral y)"
+ "- numeral (Num.Bit0 x) OR - numeral (Num.Bit0 y) = (2 :: int) * (- numeral x OR - numeral y)"
+ "- numeral (Num.Bit0 x) OR - numeral (Num.Bit1 y) = 1 + (2 :: int) * (- numeral x OR - numeral (y + Num.One))"
+ "- numeral (Num.Bit1 x) OR - numeral (Num.Bit0 y) = 1 + (2 :: int) * (- numeral (x + Num.One) OR - numeral y)"
+ "- numeral (Num.Bit1 x) OR - numeral (Num.Bit1 y) = 1 + (2 :: int) * (- numeral (x + Num.One) OR - numeral (y + Num.One))"
+ "(1::int) OR numeral (Num.Bit0 y) = numeral (Num.Bit1 y)"
+ "(1::int) OR numeral (Num.Bit1 y) = numeral (Num.Bit1 y)"
+ "(1::int) OR - numeral (Num.Bit0 y) = - numeral (Num.BitM y)"
+ "(1::int) OR - numeral (Num.Bit1 y) = - numeral (Num.Bit1 y)"
+ "numeral (Num.Bit0 x) OR (1::int) = numeral (Num.Bit1 x)"
+ "numeral (Num.Bit1 x) OR (1::int) = numeral (Num.Bit1 x)"
+ "- numeral (Num.Bit0 x) OR (1::int) = - numeral (Num.BitM x)"
+ "- numeral (Num.Bit1 x) OR (1::int) = - numeral (Num.Bit1 x)"
+ by (auto simp add: bit_or_iff bit_minus_iff even_or_iff bit_double_iff even_bit_succ_iff add_One sub_inc_One_eq sub_BitM_One_eq intro: eqI)
+
+lemma int_xor_numerals [simp]:
+ "numeral (Num.Bit0 x) XOR numeral (Num.Bit0 y) = (2 :: int) * (numeral x XOR numeral y)"
+ "numeral (Num.Bit0 x) XOR numeral (Num.Bit1 y) = 1 + (2 :: int) * (numeral x XOR numeral y)"
+ "numeral (Num.Bit1 x) XOR numeral (Num.Bit0 y) = 1 + (2 :: int) * (numeral x XOR numeral y)"
+ "numeral (Num.Bit1 x) XOR numeral (Num.Bit1 y) = (2 :: int) * (numeral x XOR numeral y)"
+ "numeral (Num.Bit0 x) XOR - numeral (Num.Bit0 y) = (2 :: int) * (numeral x XOR - numeral y)"
+ "numeral (Num.Bit0 x) XOR - numeral (Num.Bit1 y) = 1 + (2 :: int) * (numeral x XOR - numeral (y + Num.One))"
+ "numeral (Num.Bit1 x) XOR - numeral (Num.Bit0 y) = 1 + (2 :: int) * (numeral x XOR - numeral y)"
+ "numeral (Num.Bit1 x) XOR - numeral (Num.Bit1 y) = (2 :: int) * (numeral x XOR - numeral (y + Num.One))"
+ "- numeral (Num.Bit0 x) XOR numeral (Num.Bit0 y) = (2 :: int) * (- numeral x XOR numeral y)"
+ "- numeral (Num.Bit0 x) XOR numeral (Num.Bit1 y) = 1 + (2 :: int) * (- numeral x XOR numeral y)"
+ "- numeral (Num.Bit1 x) XOR numeral (Num.Bit0 y) = 1 + (2 :: int) * (- numeral (x + Num.One) XOR numeral y)"
+ "- numeral (Num.Bit1 x) XOR numeral (Num.Bit1 y) = (2 :: int) * (- numeral (x + Num.One) XOR numeral y)"
+ "- numeral (Num.Bit0 x) XOR - numeral (Num.Bit0 y) = (2 :: int) * (- numeral x XOR - numeral y)"
+ "- numeral (Num.Bit0 x) XOR - numeral (Num.Bit1 y) = 1 + (2 :: int) * (- numeral x XOR - numeral (y + Num.One))"
+ "- numeral (Num.Bit1 x) XOR - numeral (Num.Bit0 y) = 1 + (2 :: int) * (- numeral (x + Num.One) XOR - numeral y)"
+ "- numeral (Num.Bit1 x) XOR - numeral (Num.Bit1 y) = (2 :: int) * (- numeral (x + Num.One) XOR - numeral (y + Num.One))"
+ "(1::int) XOR numeral (Num.Bit0 y) = numeral (Num.Bit1 y)"
+ "(1::int) XOR numeral (Num.Bit1 y) = numeral (Num.Bit0 y)"
+ "(1::int) XOR - numeral (Num.Bit0 y) = - numeral (Num.BitM y)"
+ "(1::int) XOR - numeral (Num.Bit1 y) = - numeral (Num.Bit0 (y + Num.One))"
+ "numeral (Num.Bit0 x) XOR (1::int) = numeral (Num.Bit1 x)"
+ "numeral (Num.Bit1 x) XOR (1::int) = numeral (Num.Bit0 x)"
+ "- numeral (Num.Bit0 x) XOR (1::int) = - numeral (Num.BitM x)"
+ "- numeral (Num.Bit1 x) XOR (1::int) = - numeral (Num.Bit0 (x + Num.One))"
+ by (auto simp add: bit_xor_iff bit_minus_iff even_xor_iff bit_double_iff even_bit_succ_iff add_One sub_inc_One_eq sub_BitM_One_eq intro: eqI)
+
+end
+
subsection \<open>Bit concatenation\<close>
@@ -1009,6 +1258,10 @@
by (rule bit_eqI)
(auto simp add: bit_take_bit_iff bit_concat_bit_iff min_def)
+lemma concat_bit_take_bit_eq:
+ \<open>concat_bit n (take_bit n b) = concat_bit n b\<close>
+ by (simp add: concat_bit_def [abs_def])
+
subsection \<open>Taking bits with sign propagation\<close>
--- a/src/HOL/SPARK/Manual/Reference.thy Sat Oct 17 11:32:03 2020 +0100
+++ b/src/HOL/SPARK/Manual/Reference.thy Sat Oct 17 18:36:08 2020 +0100
@@ -1,6 +1,6 @@
(*<*)
theory Reference
-imports "HOL-SPARK.SPARK"
+imports "HOL-SPARK.SPARK" "HOL-Word.Bits_Int"
begin
syntax (my_constrain output)
--- a/src/HOL/SPARK/SPARK.thy Sat Oct 17 11:32:03 2020 +0100
+++ b/src/HOL/SPARK/SPARK.thy Sat Oct 17 18:36:08 2020 +0100
@@ -39,13 +39,7 @@
lemma bit_not_spark_eq:
"NOT (word_of_int x :: ('a::len) word) =
word_of_int (2 ^ LENGTH('a) - 1 - x)"
-proof -
- have "word_of_int x + NOT (word_of_int x) =
- word_of_int x + (word_of_int (2 ^ LENGTH('a) - 1 - x)::'a word)"
- by (simp only: bwsimps bin_add_not Min_def)
- (simp add: word_of_int_hom_syms word_of_int_2p_len)
- then show ?thesis by (rule add_left_imp_eq)
-qed
+ by (simp flip: mask_eq_exp_minus_1 add: of_int_mask_eq not_eq_complement)
lemmas [simp] =
bit_not_spark_eq [where 'a=8, simplified]
--- a/src/HOL/Word/Bit_Comprehension.thy Sat Oct 17 11:32:03 2020 +0100
+++ b/src/HOL/Word/Bit_Comprehension.thy Sat Oct 17 18:36:08 2020 +0100
@@ -47,7 +47,8 @@
apply simp
apply (rule bit_eqI)
apply (simp add: bit_signed_take_bit_iff min_def)
- using "*" by blast
+ apply (auto simp add: not_le bit_take_bit_iff dest: *)
+ done
qed
end
@@ -223,15 +224,15 @@
qed
lemma bin_last_set_bits [simp]:
- "bin_last (set_bits f) = f 0"
+ "odd (set_bits f :: int) = f 0"
by (subst int_set_bits_unfold_BIT) simp_all
lemma bin_rest_set_bits [simp]:
- "bin_rest (set_bits f) = set_bits (f \<circ> Suc)"
+ "set_bits f div (2 :: int) = set_bits (f \<circ> Suc)"
by (subst int_set_bits_unfold_BIT) simp_all
lemma bin_nth_set_bits [simp]:
- "bin_nth (set_bits f) m = f m"
+ "bit (set_bits f :: int) m \<longleftrightarrow> f m"
using wff proof (induction m arbitrary: f)
case 0
then show ?case
--- a/src/HOL/Word/Bits_Int.thy Sat Oct 17 11:32:03 2020 +0100
+++ b/src/HOL/Word/Bits_Int.thy Sat Oct 17 18:36:08 2020 +0100
@@ -8,15 +8,9 @@
imports
"HOL-Library.Bit_Operations"
Traditional_Syntax
+ Word
begin
-subsection \<open>Generic auxiliary\<close>
-
-lemma int_mod_ge: "a < n \<Longrightarrow> 0 < n \<Longrightarrow> a \<le> a mod n"
- for a n :: int
- by (metis dual_order.trans le_cases mod_pos_pos_trivial pos_mod_conj)
-
-
subsection \<open>Implicit bit representation of \<^typ>\<open>int\<close>\<close>
abbreviation (input) bin_last :: "int \<Rightarrow> bool"
@@ -511,6 +505,8 @@
definition bin_rsplit :: "nat \<Rightarrow> nat \<times> int \<Rightarrow> int list"
where "bin_rsplit n w = bin_rsplit_aux n (fst w) (snd w) []"
+value \<open>bin_rsplit 1705 (3, 88)\<close>
+
fun bin_rsplitl_aux :: "nat \<Rightarrow> nat \<Rightarrow> int \<Rightarrow> int list \<Rightarrow> int list"
where "bin_rsplitl_aux n m c bs =
(if m = 0 \<or> n = 0 then bs
@@ -1112,114 +1108,9 @@
"bin_last (- numeral (Num.BitM w))"
by simp
-(* FIXME: The rule sets below are very large (24 rules for each
- operator). Is there a simpler way to do this? *)
-
-lemma int_and_numerals [simp]:
- "numeral (Num.Bit0 x) AND numeral (Num.Bit0 y) = (2 :: int) * (numeral x AND numeral y)"
- "numeral (Num.Bit0 x) AND numeral (Num.Bit1 y) = (2 :: int) * (numeral x AND numeral y)"
- "numeral (Num.Bit1 x) AND numeral (Num.Bit0 y) = (2 :: int) * (numeral x AND numeral y)"
- "numeral (Num.Bit1 x) AND numeral (Num.Bit1 y) = 1 + (2 :: int) * (numeral x AND numeral y)"
- "numeral (Num.Bit0 x) AND - numeral (Num.Bit0 y) = (2 :: int) * (numeral x AND - numeral y)"
- "numeral (Num.Bit0 x) AND - numeral (Num.Bit1 y) = (2 :: int) * (numeral x AND - numeral (y + Num.One))"
- "numeral (Num.Bit1 x) AND - numeral (Num.Bit0 y) = (2 :: int) * (numeral x AND - numeral y)"
- "numeral (Num.Bit1 x) AND - numeral (Num.Bit1 y) = 1 + (2 :: int) * (numeral x AND - numeral (y + Num.One))"
- "- numeral (Num.Bit0 x) AND numeral (Num.Bit0 y) = (2 :: int) * (- numeral x AND numeral y)"
- "- numeral (Num.Bit0 x) AND numeral (Num.Bit1 y) = (2 :: int) * (- numeral x AND numeral y)"
- "- numeral (Num.Bit1 x) AND numeral (Num.Bit0 y) = (2 :: int) * (- numeral (x + Num.One) AND numeral y)"
- "- numeral (Num.Bit1 x) AND numeral (Num.Bit1 y) = 1 + (2 :: int) * (- numeral (x + Num.One) AND numeral y)"
- "- numeral (Num.Bit0 x) AND - numeral (Num.Bit0 y) = (2 :: int) * (- numeral x AND - numeral y)"
- "- numeral (Num.Bit0 x) AND - numeral (Num.Bit1 y) = (2 :: int) * (- numeral x AND - numeral (y + Num.One))"
- "- numeral (Num.Bit1 x) AND - numeral (Num.Bit0 y) = (2 :: int) * (- numeral (x + Num.One) AND - numeral y)"
- "- numeral (Num.Bit1 x) AND - numeral (Num.Bit1 y) = 1 + (2 :: int) * (- numeral (x + Num.One) AND - numeral (y + Num.One))"
- "(1::int) AND numeral (Num.Bit0 y) = 0"
- "(1::int) AND numeral (Num.Bit1 y) = 1"
- "(1::int) AND - numeral (Num.Bit0 y) = 0"
- "(1::int) AND - numeral (Num.Bit1 y) = 1"
- "numeral (Num.Bit0 x) AND (1::int) = 0"
- "numeral (Num.Bit1 x) AND (1::int) = 1"
- "- numeral (Num.Bit0 x) AND (1::int) = 0"
- "- numeral (Num.Bit1 x) AND (1::int) = 1"
- by (rule bin_rl_eqI; simp)+
-
-lemma int_or_numerals [simp]:
- "numeral (Num.Bit0 x) OR numeral (Num.Bit0 y) = (2 :: int) * (numeral x OR numeral y)"
- "numeral (Num.Bit0 x) OR numeral (Num.Bit1 y) = 1 + (2 :: int) * (numeral x OR numeral y)"
- "numeral (Num.Bit1 x) OR numeral (Num.Bit0 y) = 1 + (2 :: int) * (numeral x OR numeral y)"
- "numeral (Num.Bit1 x) OR numeral (Num.Bit1 y) = 1 + (2 :: int) * (numeral x OR numeral y)"
- "numeral (Num.Bit0 x) OR - numeral (Num.Bit0 y) = (2 :: int) * (numeral x OR - numeral y)"
- "numeral (Num.Bit0 x) OR - numeral (Num.Bit1 y) = 1 + (2 :: int) * (numeral x OR - numeral (y + Num.One))"
- "numeral (Num.Bit1 x) OR - numeral (Num.Bit0 y) = 1 + (2 :: int) * (numeral x OR - numeral y)"
- "numeral (Num.Bit1 x) OR - numeral (Num.Bit1 y) = 1 + (2 :: int) * (numeral x OR - numeral (y + Num.One))"
- "- numeral (Num.Bit0 x) OR numeral (Num.Bit0 y) = (2 :: int) * (- numeral x OR numeral y)"
- "- numeral (Num.Bit0 x) OR numeral (Num.Bit1 y) = 1 + (2 :: int) * (- numeral x OR numeral y)"
- "- numeral (Num.Bit1 x) OR numeral (Num.Bit0 y) = 1 + (2 :: int) * (- numeral (x + Num.One) OR numeral y)"
- "- numeral (Num.Bit1 x) OR numeral (Num.Bit1 y) = 1 + (2 :: int) * (- numeral (x + Num.One) OR numeral y)"
- "- numeral (Num.Bit0 x) OR - numeral (Num.Bit0 y) = (2 :: int) * (- numeral x OR - numeral y)"
- "- numeral (Num.Bit0 x) OR - numeral (Num.Bit1 y) = 1 + (2 :: int) * (- numeral x OR - numeral (y + Num.One))"
- "- numeral (Num.Bit1 x) OR - numeral (Num.Bit0 y) = 1 + (2 :: int) * (- numeral (x + Num.One) OR - numeral y)"
- "- numeral (Num.Bit1 x) OR - numeral (Num.Bit1 y) = 1 + (2 :: int) * (- numeral (x + Num.One) OR - numeral (y + Num.One))"
- "(1::int) OR numeral (Num.Bit0 y) = numeral (Num.Bit1 y)"
- "(1::int) OR numeral (Num.Bit1 y) = numeral (Num.Bit1 y)"
- "(1::int) OR - numeral (Num.Bit0 y) = - numeral (Num.BitM y)"
- "(1::int) OR - numeral (Num.Bit1 y) = - numeral (Num.Bit1 y)"
- "numeral (Num.Bit0 x) OR (1::int) = numeral (Num.Bit1 x)"
- "numeral (Num.Bit1 x) OR (1::int) = numeral (Num.Bit1 x)"
- "- numeral (Num.Bit0 x) OR (1::int) = - numeral (Num.BitM x)"
- "- numeral (Num.Bit1 x) OR (1::int) = - numeral (Num.Bit1 x)"
- by (rule bin_rl_eqI; simp)+
-
-lemma int_xor_numerals [simp]:
- "numeral (Num.Bit0 x) XOR numeral (Num.Bit0 y) = (2 :: int) * (numeral x XOR numeral y)"
- "numeral (Num.Bit0 x) XOR numeral (Num.Bit1 y) = 1 + (2 :: int) * (numeral x XOR numeral y)"
- "numeral (Num.Bit1 x) XOR numeral (Num.Bit0 y) = 1 + (2 :: int) * (numeral x XOR numeral y)"
- "numeral (Num.Bit1 x) XOR numeral (Num.Bit1 y) = (2 :: int) * (numeral x XOR numeral y)"
- "numeral (Num.Bit0 x) XOR - numeral (Num.Bit0 y) = (2 :: int) * (numeral x XOR - numeral y)"
- "numeral (Num.Bit0 x) XOR - numeral (Num.Bit1 y) = 1 + (2 :: int) * (numeral x XOR - numeral (y + Num.One))"
- "numeral (Num.Bit1 x) XOR - numeral (Num.Bit0 y) = 1 + (2 :: int) * (numeral x XOR - numeral y)"
- "numeral (Num.Bit1 x) XOR - numeral (Num.Bit1 y) = (2 :: int) * (numeral x XOR - numeral (y + Num.One))"
- "- numeral (Num.Bit0 x) XOR numeral (Num.Bit0 y) = (2 :: int) * (- numeral x XOR numeral y)"
- "- numeral (Num.Bit0 x) XOR numeral (Num.Bit1 y) = 1 + (2 :: int) * (- numeral x XOR numeral y)"
- "- numeral (Num.Bit1 x) XOR numeral (Num.Bit0 y) = 1 + (2 :: int) * (- numeral (x + Num.One) XOR numeral y)"
- "- numeral (Num.Bit1 x) XOR numeral (Num.Bit1 y) = (2 :: int) * (- numeral (x + Num.One) XOR numeral y)"
- "- numeral (Num.Bit0 x) XOR - numeral (Num.Bit0 y) = (2 :: int) * (- numeral x XOR - numeral y)"
- "- numeral (Num.Bit0 x) XOR - numeral (Num.Bit1 y) = 1 + (2 :: int) * (- numeral x XOR - numeral (y + Num.One))"
- "- numeral (Num.Bit1 x) XOR - numeral (Num.Bit0 y) = 1 + (2 :: int) * (- numeral (x + Num.One) XOR - numeral y)"
- "- numeral (Num.Bit1 x) XOR - numeral (Num.Bit1 y) = (2 :: int) * (- numeral (x + Num.One) XOR - numeral (y + Num.One))"
- "(1::int) XOR numeral (Num.Bit0 y) = numeral (Num.Bit1 y)"
- "(1::int) XOR numeral (Num.Bit1 y) = numeral (Num.Bit0 y)"
- "(1::int) XOR - numeral (Num.Bit0 y) = - numeral (Num.BitM y)"
- "(1::int) XOR - numeral (Num.Bit1 y) = - numeral (Num.Bit0 (y + Num.One))"
- "numeral (Num.Bit0 x) XOR (1::int) = numeral (Num.Bit1 x)"
- "numeral (Num.Bit1 x) XOR (1::int) = numeral (Num.Bit0 x)"
- "- numeral (Num.Bit0 x) XOR (1::int) = - numeral (Num.BitM x)"
- "- numeral (Num.Bit1 x) XOR (1::int) = - numeral (Num.Bit0 (x + Num.One))"
- by (rule bin_rl_eqI; simp)+
-
subsubsection \<open>Interactions with arithmetic\<close>
-lemma plus_and_or: "(x AND y) + (x OR y) = x + y" for x y :: int
-proof (induction x arbitrary: y rule: int_bit_induct)
- case zero
- then show ?case
- by simp
-next
- case minus
- then show ?case
- by simp
-next
- case (even x)
- from even.IH [of \<open>y div 2\<close>]
- show ?case
- by (auto simp add: and_int_rec [of _ y] or_int_rec [of _ y] elim: oddE)
-next
- case (odd x)
- from odd.IH [of \<open>y div 2\<close>]
- show ?case
- by (auto simp add: and_int_rec [of _ y] or_int_rec [of _ y] elim: oddE)
-qed
-
lemma le_int_or: "bin_sign y = 0 \<Longrightarrow> x \<le> x OR y"
for x y :: int
by (simp add: bin_sign_def or_greater_eq split: if_splits)
@@ -1236,106 +1127,18 @@
by (simp flip: take_bit_eq_mod add: take_bit_eq_mask mask_eq_exp_minus_1)
-subsubsection \<open>Comparison\<close>
-
-lemma AND_lower [simp]: \<^marker>\<open>contributor \<open>Stefan Berghofer\<close>\<close>
- fixes x y :: int
- assumes "0 \<le> x"
- shows "0 \<le> x AND y"
- using assms by simp
-
-lemma OR_lower [simp]: \<^marker>\<open>contributor \<open>Stefan Berghofer\<close>\<close>
- fixes x y :: int
- assumes "0 \<le> x" "0 \<le> y"
- shows "0 \<le> x OR y"
- using assms by simp
-
-lemma XOR_lower [simp]: \<^marker>\<open>contributor \<open>Stefan Berghofer\<close>\<close>
- fixes x y :: int
- assumes "0 \<le> x" "0 \<le> y"
- shows "0 \<le> x XOR y"
- using assms by simp
-
-lemma AND_upper1 [simp]: \<^marker>\<open>contributor \<open>Stefan Berghofer\<close>\<close>
- fixes x y :: int
- assumes "0 \<le> x"
- shows "x AND y \<le> x"
- using assms by (induction x arbitrary: y rule: int_bit_induct)
- (simp_all add: and_int_rec [of \<open>_ * 2\<close>] and_int_rec [of \<open>1 + _ * 2\<close>] add_increasing)
-
-lemmas AND_upper1' [simp] = order_trans [OF AND_upper1] \<^marker>\<open>contributor \<open>Stefan Berghofer\<close>\<close>
-lemmas AND_upper1'' [simp] = order_le_less_trans [OF AND_upper1] \<^marker>\<open>contributor \<open>Stefan Berghofer\<close>\<close>
-
-lemma AND_upper2 [simp]: \<^marker>\<open>contributor \<open>Stefan Berghofer\<close>\<close>
- fixes x y :: int
- assumes "0 \<le> y"
- shows "x AND y \<le> y"
- using assms AND_upper1 [of y x] by (simp add: ac_simps)
-
-lemmas AND_upper2' [simp] = order_trans [OF AND_upper2] \<^marker>\<open>contributor \<open>Stefan Berghofer\<close>\<close>
-lemmas AND_upper2'' [simp] = order_le_less_trans [OF AND_upper2] \<^marker>\<open>contributor \<open>Stefan Berghofer\<close>\<close>
-
-lemma OR_upper: \<^marker>\<open>contributor \<open>Stefan Berghofer\<close>\<close>
- fixes x y :: int
- assumes "0 \<le> x" "x < 2 ^ n" "y < 2 ^ n"
- shows "x OR y < 2 ^ n"
-using assms proof (induction x arbitrary: y n rule: int_bit_induct)
- case zero
- then show ?case
- by simp
-next
- case minus
- then show ?case
- by simp
-next
- case (even x)
- from even.IH [of \<open>n - 1\<close> \<open>y div 2\<close>] even.prems even.hyps
- show ?case
- by (cases n) (auto simp add: or_int_rec [of \<open>_ * 2\<close>] elim: oddE)
-next
- case (odd x)
- from odd.IH [of \<open>n - 1\<close> \<open>y div 2\<close>] odd.prems odd.hyps
- show ?case
- by (cases n) (auto simp add: or_int_rec [of \<open>1 + _ * 2\<close>], linarith)
-qed
-
-lemma XOR_upper: \<^marker>\<open>contributor \<open>Stefan Berghofer\<close>\<close>
- fixes x y :: int
- assumes "0 \<le> x" "x < 2 ^ n" "y < 2 ^ n"
- shows "x XOR y < 2 ^ n"
-using assms proof (induction x arbitrary: y n rule: int_bit_induct)
- case zero
- then show ?case
- by simp
-next
- case minus
- then show ?case
- by simp
-next
- case (even x)
- from even.IH [of \<open>n - 1\<close> \<open>y div 2\<close>] even.prems even.hyps
- show ?case
- by (cases n) (auto simp add: xor_int_rec [of \<open>_ * 2\<close>] elim: oddE)
-next
- case (odd x)
- from odd.IH [of \<open>n - 1\<close> \<open>y div 2\<close>] odd.prems odd.hyps
- show ?case
- by (cases n) (auto simp add: xor_int_rec [of \<open>1 + _ * 2\<close>])
-qed
-
-
subsubsection \<open>Truncating results of bit-wise operations\<close>
lemma bin_trunc_ao:
"bintrunc n x AND bintrunc n y = bintrunc n (x AND y)"
"bintrunc n x OR bintrunc n y = bintrunc n (x OR y)"
- by (auto simp add: bin_eq_iff bin_nth_ops nth_bintr)
+ by simp_all
lemma bin_trunc_xor: "bintrunc n (bintrunc n x XOR bintrunc n y) = bintrunc n (x XOR y)"
- by (auto simp add: bin_eq_iff bin_nth_ops nth_bintr)
+ by simp
lemma bin_trunc_not: "bintrunc n (NOT (bintrunc n x)) = bintrunc n (NOT x)"
- by (auto simp add: bin_eq_iff bin_nth_ops nth_bintr)
+ by (fact take_bit_not_take_bit)
text \<open>Want theorems of the form of \<open>bin_trunc_xor\<close>.\<close>
lemma bintr_bintr_i: "x = bintrunc n y \<Longrightarrow> bintrunc n x = bintrunc n y"
@@ -1545,4 +1348,62 @@
"bin_sc n True i = i OR (1 << n)"
by (induct n arbitrary: i) (rule bin_rl_eqI; simp)+
+
+subsection \<open>More lemmas on words\<close>
+
+lemma word_rcat_eq:
+ \<open>word_rcat ws = word_of_int (bin_rcat (LENGTH('a::len)) (map uint ws))\<close>
+ for ws :: \<open>'a::len word list\<close>
+ apply (simp add: word_rcat_def bin_rcat_def rev_map)
+ apply transfer
+ apply (simp add: horner_sum_foldr foldr_map comp_def)
+ done
+
+lemma sign_uint_Pls [simp]: "bin_sign (uint x) = 0"
+ by (simp add: sign_Pls_ge_0)
+
+lemmas bin_log_bintrs = bin_trunc_not bin_trunc_xor bin_trunc_and bin_trunc_or
+
+\<comment> \<open>following definitions require both arithmetic and bit-wise word operations\<close>
+
+\<comment> \<open>to get \<open>word_no_log_defs\<close> from \<open>word_log_defs\<close>, using \<open>bin_log_bintrs\<close>\<close>
+lemmas wils1 = bin_log_bintrs [THEN word_of_int_eq_iff [THEN iffD2],
+ folded uint_word_of_int_eq, THEN eq_reflection]
+
+\<comment> \<open>the binary operations only\<close> (* BH: why is this needed? *)
+lemmas word_log_binary_defs =
+ word_and_def word_or_def word_xor_def
+
+lemma setBit_no [simp]: "setBit (numeral bin) n = word_of_int (bin_sc n True (numeral bin))"
+ by transfer (simp add: bin_sc_eq)
+
+lemma clearBit_no [simp]:
+ "clearBit (numeral bin) n = word_of_int (bin_sc n False (numeral bin))"
+ by transfer (simp add: bin_sc_eq)
+
+lemma eq_mod_iff: "0 < n \<Longrightarrow> b = b mod n \<longleftrightarrow> 0 \<le> b \<and> b < n"
+ for b n :: int
+ by auto (metis pos_mod_conj)+
+
+lemma split_uint_lem: "bin_split n (uint w) = (a, b) \<Longrightarrow>
+ a = take_bit (LENGTH('a) - n) a \<and> b = take_bit (LENGTH('a)) b"
+ for w :: "'a::len word"
+ by transfer (simp add: drop_bit_take_bit ac_simps)
+
+\<comment> \<open>limited hom result\<close>
+lemma word_cat_hom:
+ "LENGTH('a::len) \<le> LENGTH('b::len) + LENGTH('c::len) \<Longrightarrow>
+ (word_cat (word_of_int w :: 'b word) (b :: 'c word) :: 'a word) =
+ word_of_int (bin_cat w (size b) (uint b))"
+ by transfer (simp add: take_bit_concat_bit_eq)
+
+lemma bintrunc_shiftl:
+ "take_bit n (m << i) = take_bit (n - i) m << i"
+ for m :: int
+ by (rule bit_eqI) (auto simp add: bit_take_bit_iff)
+
+lemma uint_shiftl:
+ "uint (n << i) = take_bit (size n) (uint n << i)"
+ by transfer (simp add: push_bit_take_bit shiftl_eq_push_bit)
+
end
--- a/src/HOL/Word/Misc_Typedef.thy Sat Oct 17 11:32:03 2020 +0100
+++ b/src/HOL/Word/Misc_Typedef.thy Sat Oct 17 18:36:08 2020 +0100
@@ -7,7 +7,7 @@
section \<open>Type Definition Theorems\<close>
theory Misc_Typedef
- imports Main Word Bit_Comprehension
+ imports Main Word Bit_Comprehension Bits_Int
begin
subsection "More lemmas about normal type definitions"
--- a/src/HOL/Word/More_Word.thy Sat Oct 17 11:32:03 2020 +0100
+++ b/src/HOL/Word/More_Word.thy Sat Oct 17 18:36:08 2020 +0100
@@ -15,6 +15,7 @@
Misc_set_bit
Misc_lsb
Misc_Typedef
+ Word_rsplit
begin
declare signed_take_bit_Suc [simp]
--- a/src/HOL/Word/Reversed_Bit_Lists.thy Sat Oct 17 11:32:03 2020 +0100
+++ b/src/HOL/Word/Reversed_Bit_Lists.thy Sat Oct 17 18:36:08 2020 +0100
@@ -1684,7 +1684,7 @@
apply (simp add: word_split_def)
apply transfer
apply (cases \<open>LENGTH('b) \<le> LENGTH('a)\<close>)
- apply (auto simp add: drop_bit_take_bit drop_bin2bl bin_to_bl_drop_bit [symmetric, of \<open>LENGTH('a)\<close> \<open>LENGTH('a) - LENGTH('b)\<close> \<open>LENGTH('b)\<close>])
+ apply (auto simp add: drop_bit_take_bit drop_bin2bl bin_to_bl_drop_bit [symmetric, of \<open>LENGTH('a)\<close> \<open>LENGTH('a) - LENGTH('b)\<close> \<open>LENGTH('b)\<close>] min_absorb2)
done
lemma word_split_bl: "std = size c - size b \<Longrightarrow>
--- a/src/HOL/Word/Tools/smt_word.ML Sat Oct 17 11:32:03 2020 +0100
+++ b/src/HOL/Word/Tools/smt_word.ML Sat Oct 17 18:36:08 2020 +0100
@@ -51,13 +51,25 @@
val mk_nat = HOLogic.mk_number \<^typ>\<open>nat\<close>
- fun mk_shift c [t, u] = Const c $ t $ mk_nat (snd (HOLogic.dest_number u))
+ fun mk_shift' c [t, u] = Const c $ t $ mk_nat (snd (HOLogic.dest_number u))
+ | mk_shift' c ts = raise TERM ("bad arguments", Const c :: ts)
+
+ fun shift' m n T ts =
+ let val U = Term.domain_type T
+ in
+ (case (can dest_wordT U, try (snd o HOLogic.dest_number o hd o tl) ts) of
+ (true, SOME i) =>
+ SOME (n, 2, [hd ts, HOLogic.mk_number U i], mk_shift' (m, T))
+ | _ => NONE) (* FIXME: also support non-numerical shifts *)
+ end
+
+ fun mk_shift c [u, t] = Const c $ mk_nat (snd (HOLogic.dest_number u)) $ t
| mk_shift c ts = raise TERM ("bad arguments", Const c :: ts)
fun shift m n T ts =
let val U = Term.domain_type T
in
- (case (can dest_wordT U, try (snd o HOLogic.dest_number o hd o tl) ts) of
+ (case (can dest_wordT U, try (snd o HOLogic.dest_number o hd) ts) of
(true, SOME i) =>
SOME (n, 2, [hd ts, HOLogic.mk_number U i], mk_shift (m, T))
| _ => NONE) (* FIXME: also support non-numerical shifts *)
@@ -110,6 +122,10 @@
(\<^term>\<open>(XOR) :: 'a::len word \<Rightarrow> _\<close>, "bvxor"),
(\<^term>\<open>word_cat :: 'a::len word \<Rightarrow> _\<close>, "concat") ] #>
fold (add_word_fun shift) [
+ (\<^term>\<open>push_bit :: nat \<Rightarrow> 'a::len word \<Rightarrow> _ \<close>, "bvshl"),
+ (\<^term>\<open>drop_bit :: nat \<Rightarrow> 'a::len word \<Rightarrow> _\<close>, "bvlshr"),
+ (\<^term>\<open>signed_drop_bit :: nat \<Rightarrow> 'a::len word \<Rightarrow> _\<close>, "bvashr") ] #>
+ fold (add_word_fun shift') [
(\<^term>\<open>shiftl :: 'a::len word \<Rightarrow> _ \<close>, "bvshl"),
(\<^term>\<open>shiftr :: 'a::len word \<Rightarrow> _\<close>, "bvlshr"),
(\<^term>\<open>sshiftr :: 'a::len word \<Rightarrow> _\<close>, "bvashr") ] #>
--- a/src/HOL/Word/Word.thy Sat Oct 17 11:32:03 2020 +0100
+++ b/src/HOL/Word/Word.thy Sat Oct 17 18:36:08 2020 +0100
@@ -9,7 +9,6 @@
"HOL-Library.Type_Length"
"HOL-Library.Boolean_Algebra"
"HOL-Library.Bit_Operations"
- Bits_Int
Traditional_Syntax
begin
@@ -131,6 +130,11 @@
by transfer simp
+subsubsection \<open>Basic tool setup\<close>
+
+ML_file \<open>Tools/word_lib.ML\<close>
+
+
subsubsection \<open>Basic code generation setup\<close>
context
@@ -295,8 +299,7 @@
lemma signed_1 [simp]:
\<open>signed (1 :: 'b::len word) = (if LENGTH('b) = 1 then - 1 else 1)\<close>
- by (transfer fixing: uminus; cases \<open>LENGTH('b)\<close>)
- (simp_all add: sbintrunc_minus_simps)
+ by (transfer fixing: uminus; cases \<open>LENGTH('b)\<close>) (auto dest: gr0_implies_Suc)
lemma signed_minus_1 [simp]:
\<open>signed (- 1 :: 'b::len word) = - 1\<close>
@@ -476,7 +479,7 @@
lemma [code]:
\<open>Word.the_signed_int w = signed_take_bit (LENGTH('a) - Suc 0) (Word.the_int w)\<close>
for w :: \<open>'a::len word\<close>
- by transfer simp
+ by transfer (simp add: signed_take_bit_take_bit)
lemma [code_abbrev, simp]:
\<open>Word.the_signed_int = sint\<close>
@@ -1658,7 +1661,7 @@
by (fact word_coorder.extremum)
lemma word_m1_ge [simp] : "word_pred 0 \<ge> y" (* FIXME: delete *)
- by transfer (simp add: take_bit_minus_one_eq_mask mask_eq_exp_minus_1 bintr_lt2p)
+ by transfer (simp add: take_bit_minus_one_eq_mask mask_eq_exp_minus_1 )
lemma word_n1_ge [simp]: "y \<le> -1"
for y :: "'a::len word"
@@ -1766,7 +1769,8 @@
lift_definition shiftr1 :: \<open>'a::len word \<Rightarrow> 'a word\<close>
\<comment> \<open>shift right as unsigned or as signed, ie logical or arithmetic\<close>
- is \<open>\<lambda>k. take_bit LENGTH('a) k div 2\<close> by simp
+ is \<open>\<lambda>k. take_bit LENGTH('a) k div 2\<close>
+ by simp
lemma shiftr1_eq_div_2:
\<open>shiftr1 w = w div 2\<close>
@@ -1884,14 +1888,14 @@
lemma shiftr_def:
\<open>w >> n = (shiftr1 ^^ n) w\<close>
proof -
- have \<open>drop_bit n = (((\<lambda>k::int. k div 2) ^^ n))\<close> for n
- by (rule sym, induction n)
- (simp_all add: fun_eq_iff drop_bit_Suc flip: drop_bit_half)
+ have \<open>shiftr1 ^^ n = (drop_bit n :: 'a word \<Rightarrow> 'a word)\<close>
+ apply (induction n)
+ apply simp
+ apply (simp only: shiftr1_eq_div_2 [abs_def] drop_bit_eq_div [abs_def] funpow_Suc_right)
+ apply (use div_exp_eq [of _ 1, where ?'a = \<open>'a word\<close>] in simp)
+ done
then show ?thesis
- apply transfer
- apply simp
- apply (metis bintrunc_bintrunc rco_bintr)
- done
+ by (simp add: shiftr_word_eq)
qed
lemma bit_shiftl_word_iff:
@@ -2029,9 +2033,18 @@
apply (metis le_antisym less_eq_decr_length_iff)
done
+lemma signed_drop_bit_signed_drop_bit [simp]:
+ \<open>signed_drop_bit m (signed_drop_bit n w) = signed_drop_bit (m + n) w\<close>
+ for w :: \<open>'a::len word\<close>
+ apply (cases \<open>LENGTH('a)\<close>)
+ apply simp_all
+ apply (rule bit_word_eqI)
+ apply (auto simp add: bit_signed_drop_bit_iff not_le less_diff_conv ac_simps)
+ done
+
lemma signed_drop_bit_0 [simp]:
\<open>signed_drop_bit 0 w = w\<close>
- by transfer simp
+ by transfer (simp add: take_bit_signed_take_bit)
lemma sint_signed_drop_bit_eq:
\<open>sint (signed_drop_bit n w) = drop_bit n (sint w)\<close>
@@ -2041,42 +2054,37 @@
apply (auto simp add: bit_sint_iff bit_drop_bit_eq bit_signed_drop_bit_iff dest: bit_imp_le_length)
done
-lift_definition sshiftr1 :: \<open>'a::len word \<Rightarrow> 'a word\<close>
- is \<open>\<lambda>k. take_bit LENGTH('a) (signed_take_bit (LENGTH('a) - 1) k div 2)\<close>
+lift_definition sshiftr :: \<open>'a::len word \<Rightarrow> nat \<Rightarrow> 'a word\<close> (infixl \<open>>>>\<close> 55)
+ is \<open>\<lambda>k n. take_bit LENGTH('a) (drop_bit n (signed_take_bit (LENGTH('a) - Suc 0) k))\<close>
by (simp flip: signed_take_bit_decr_length_iff)
-
-lift_definition sshiftr :: \<open>'a::len word \<Rightarrow> nat \<Rightarrow> 'a word\<close> (infixl \<open>>>>\<close> 55)
- is \<open>\<lambda>k n. take_bit LENGTH('a) (drop_bit n (signed_take_bit (LENGTH('a) - 1) k))\<close>
+
+lift_definition sshiftr1 :: \<open>'a::len word \<Rightarrow> 'a word\<close>
+ is \<open>\<lambda>k. take_bit LENGTH('a) (signed_take_bit (LENGTH('a) - Suc 0) k div 2)\<close>
by (simp flip: signed_take_bit_decr_length_iff)
lift_definition bshiftr1 :: \<open>bool \<Rightarrow> 'a::len word \<Rightarrow> 'a word\<close>
is \<open>\<lambda>b k. take_bit LENGTH('a) k div 2 + of_bool b * 2 ^ (LENGTH('a) - Suc 0)\<close>
by (fact arg_cong)
+lemma sshiftr_eq:
+ \<open>w >>> n = signed_drop_bit n w\<close>
+ by transfer simp
+
+lemma sshiftr1_eq_signed_drop_bit_Suc_0:
+ \<open>sshiftr1 = signed_drop_bit (Suc 0)\<close>
+ by (rule ext) (transfer, simp add: drop_bit_Suc)
+
lemma sshiftr1_eq:
\<open>sshiftr1 w = word_of_int (sint w div 2)\<close>
by transfer simp
lemma sshiftr_eq_funpow_sshiftr1:
\<open>w >>> n = (sshiftr1 ^^ n) w\<close>
-proof -
- have *: \<open>(\<lambda>k::int. take_bit LENGTH('a) (signed_take_bit (LENGTH('a) - Suc 0) k div 2)) ^^ Suc n =
- take_bit LENGTH('a) \<circ> drop_bit (Suc n) \<circ> signed_take_bit (LENGTH('a) - Suc 0)\<close>
- for n
- apply (induction n)
- apply (auto simp add: fun_eq_iff drop_bit_Suc)
- apply (metis (no_types, lifting) Suc_pred funpow_swap1 len_gt_0 sbintrunc_bintrunc sbintrunc_rest)
- done
- show ?thesis
- apply transfer
- apply simp
- subgoal for k n
- apply (cases n)
- apply (simp_all only: *)
- apply simp_all
- done
- done
-qed
+ apply (rule sym)
+ apply (simp add: sshiftr1_eq_signed_drop_bit_Suc_0 sshiftr_eq)
+ apply (induction n)
+ apply simp_all
+ done
lemma mask_eq:
\<open>mask n = (1 << n) - (1 :: 'a::len word)\<close>
@@ -2260,32 +2268,20 @@
lemma word_cat_eq' [code]:
\<open>word_cat a b = word_of_int (concat_bit LENGTH('b) (uint b) (uint a))\<close>
for a :: \<open>'a::len word\<close> and b :: \<open>'b::len word\<close>
- by transfer simp
+ by transfer (simp add: concat_bit_take_bit_eq)
lemma bit_word_cat_iff:
\<open>bit (word_cat v w :: 'c::len word) n \<longleftrightarrow> n < LENGTH('c) \<and> (if n < LENGTH('b) then bit w n else bit v (n - LENGTH('b)))\<close>
for v :: \<open>'a::len word\<close> and w :: \<open>'b::len word\<close>
by transfer (simp add: bit_concat_bit_iff bit_take_bit_iff)
-definition word_split :: "'a::len word \<Rightarrow> 'b::len word \<times> 'c::len word"
- where "word_split a =
- (case bin_split (LENGTH('c)) (uint a) of
- (u, v) \<Rightarrow> (word_of_int u, word_of_int v))"
+definition word_split :: \<open>'a::len word \<Rightarrow> 'b::len word \<times> 'c::len word\<close>
+ where \<open>word_split w =
+ (ucast (drop_bit LENGTH('c) w) :: 'b::len word, ucast w :: 'c::len word)\<close>
definition word_rcat :: \<open>'a::len word list \<Rightarrow> 'b::len word\<close>
where \<open>word_rcat = word_of_int \<circ> horner_sum uint (2 ^ LENGTH('a)) \<circ> rev\<close>
-lemma word_rcat_eq:
- \<open>word_rcat ws = word_of_int (bin_rcat (LENGTH('a::len)) (map uint ws))\<close>
- for ws :: \<open>'a::len word list\<close>
- apply (simp add: word_rcat_def bin_rcat_def rev_map)
- apply transfer
- apply (simp add: horner_sum_foldr foldr_map comp_def)
- done
-
-definition word_rsplit :: "'a::len word \<Rightarrow> 'b::len word list"
- where "word_rsplit w = map word_of_int (bin_rsplit (LENGTH('b)) (LENGTH('a), uint w))"
-
abbreviation (input) max_word :: \<open>'a::len word\<close>
\<comment> \<open>Largest representable machine integer.\<close>
where "max_word \<equiv> - 1"
@@ -2295,14 +2291,14 @@
lemma int_word_sint:
\<open>sint (word_of_int x :: 'a::len word) = (x + 2 ^ (LENGTH('a) - 1)) mod 2 ^ LENGTH('a) - 2 ^ (LENGTH('a) - 1)\<close>
- by transfer (simp add: no_sbintr_alt2)
+ by transfer (simp flip: take_bit_eq_mod add: signed_take_bit_eq_take_bit_shift)
lemma sint_sbintrunc': "sint (word_of_int bin :: 'a word) = signed_take_bit (LENGTH('a::len) - 1) bin"
by simp
-lemma uint_sint: "uint w = take_bit (LENGTH('a)) (sint w)"
+lemma uint_sint: "uint w = take_bit LENGTH('a) (sint w)"
for w :: "'a::len word"
- by transfer simp
+ by transfer (simp add: take_bit_signed_take_bit)
lemma bintr_uint: "LENGTH('a) \<le> n \<Longrightarrow> take_bit n (uint w) = uint w"
for w :: "'a::len word"
@@ -2367,9 +2363,6 @@
for x :: "'a::len word"
using sint_less [of x] by simp
-lemma sign_uint_Pls [simp]: "bin_sign (uint x) = 0"
- by (simp add: sign_Pls_ge_0)
-
lemma uint_m2p_neg: "uint x - 2 ^ LENGTH('a) < 0"
for x :: "'a::len word"
by (simp only: diff_less_0_iff_less uint_lt2p)
@@ -2380,7 +2373,7 @@
lemma lt2p_lem: "LENGTH('a) \<le> n \<Longrightarrow> uint w < 2 ^ n"
for w :: "'a::len word"
- by (metis bintr_lt2p bintr_uint)
+ using uint_bounded [of w] by (rule less_le_trans) simp
lemma uint_le_0_iff [simp]: "uint x \<le> 0 \<longleftrightarrow> uint x = 0"
by (fact uint_ge_0 [THEN leD, THEN antisym_conv1])
@@ -2439,7 +2432,7 @@
by transfer simp
lemma sint_range_size: "- (2 ^ (size w - Suc 0)) \<le> sint w \<and> sint w < 2 ^ (size w - Suc 0)"
- by transfer (use sbintr_ge sbintr_lt in blast)
+ by (simp add: word_size sint_greater_eq sint_less)
lemma sint_above_size: "2 ^ (size w - 1) \<le> x \<Longrightarrow> sint w < x"
for w :: "'a::len word"
@@ -2472,18 +2465,18 @@
for u v :: "'a::len word"
by simp
-lemma test_bit_bin': "w !! n \<longleftrightarrow> n < size w \<and> bin_nth (uint w) n"
+lemma test_bit_bin': "w !! n \<longleftrightarrow> n < size w \<and> bit (uint w) n"
by transfer (simp add: bit_take_bit_iff)
lemmas test_bit_bin = test_bit_bin' [unfolded word_size]
-lemma bin_nth_uint_imp: "bin_nth (uint w) n \<Longrightarrow> n < LENGTH('a)"
+lemma bin_nth_uint_imp: "bit (uint w) n \<Longrightarrow> n < LENGTH('a)"
for w :: "'a::len word"
by transfer (simp add: bit_take_bit_iff)
lemma bin_nth_sint:
"LENGTH('a) \<le> n \<Longrightarrow>
- bin_nth (sint w) n = bin_nth (sint w) (LENGTH('a) - 1)"
+ bit (sint w) n = bit (sint w) (LENGTH('a) - 1)"
for w :: "'a::len word"
by (transfer fixing: n) (simp add: bit_signed_take_bit_iff le_diff_conv min_def)
@@ -2506,7 +2499,7 @@
then have \<open>take_bit LENGTH('a) (signed_take_bit (LENGTH('a) - 1) (numeral a :: int)) = take_bit LENGTH('a) (numeral b)\<close>
by simp
then show \<open>take_bit LENGTH('a) (numeral a :: int) = take_bit LENGTH('a) (numeral b)\<close>
- by simp
+ by (simp add: take_bit_signed_take_bit)
qed
lemma num_abs_bintr:
@@ -2517,7 +2510,7 @@
lemma num_abs_sbintr:
"(numeral x :: 'a word) =
word_of_int (signed_take_bit (LENGTH('a::len) - 1) (numeral x))"
- by transfer simp
+ by transfer (simp add: take_bit_signed_take_bit)
text \<open>
\<open>cast\<close> -- note, no arg for new length, as it's determined by type of result,
@@ -2532,7 +2525,7 @@
by transfer simp
lemma scast_id [simp]: "scast w = w"
- by transfer simp
+ by transfer (simp add: take_bit_signed_take_bit)
lemma nth_ucast: "(ucast w::'a::len word) !! n = (w !! n \<and> n < LENGTH('a))"
by transfer (simp add: bit_take_bit_iff ac_simps)
@@ -2746,16 +2739,13 @@
and "sint (word_pred a) = signed_take_bit (LENGTH('a) - 1) (sint a - 1)"
and "sint (0 :: 'a word) = signed_take_bit (LENGTH('a) - 1) 0"
and "sint (1 :: 'a word) = signed_take_bit (LENGTH('a) - 1) 1"
- prefer 8
- apply (simp add: Suc_lessI sbintrunc_minus_simps(3))
- prefer 7
- apply simp
- apply transfer apply (simp add: signed_take_bit_add)
- apply transfer apply (simp add: signed_take_bit_diff)
- apply transfer apply (simp add: signed_take_bit_mult)
- apply transfer apply (simp add: signed_take_bit_minus)
- apply (metis One_nat_def id_apply of_int_eq_id sbintrunc_sbintrunc signed.rep_eq signed_word_eqI sint_sbintrunc' wi_hom_succ)
- apply (metis (no_types, lifting) One_nat_def signed_take_bit_decr_length_iff sint_uint uint_sint uint_word_of_int_eq wi_hom_pred word_of_int_uint)
+ apply transfer apply (simp add: signed_take_bit_add)
+ apply transfer apply (simp add: signed_take_bit_diff)
+ apply transfer apply (simp add: signed_take_bit_mult)
+ apply transfer apply (simp add: signed_take_bit_minus)
+ apply (metis of_int_sint scast_id sint_sbintrunc' wi_hom_succ)
+ apply (metis of_int_sint scast_id sint_sbintrunc' wi_hom_pred)
+ apply (simp_all add: sint_uint)
done
lemma word_pred_0_n1: "word_pred 0 = word_of_int (- 1)"
@@ -2940,18 +2930,31 @@
unfolding uint_word_ariths by (simp add: zmod_le_nonneg_dividend)
lemma uint_sub_ge: "uint (x - y) \<ge> uint x - uint y"
- unfolding uint_word_ariths by (simp add: int_mod_ge)
-
+ unfolding uint_word_ariths
+ by (simp flip: take_bit_eq_mod add: take_bit_int_greater_eq_self_iff)
+
+lemma int_mod_ge: \<open>a \<le> a mod n\<close> if \<open>a < n\<close> \<open>0 < n\<close>
+ for a n :: int
+proof (cases \<open>a < 0\<close>)
+ case True
+ with \<open>0 < n\<close> show ?thesis
+ by (metis less_trans not_less pos_mod_conj)
+
+next
+ case False
+ with \<open>a < n\<close> show ?thesis
+ by simp
+qed
+
lemma mod_add_if_z:
"x < z \<Longrightarrow> y < z \<Longrightarrow> 0 \<le> y \<Longrightarrow> 0 \<le> x \<Longrightarrow> 0 \<le> z \<Longrightarrow>
(x + y) mod z = (if x + y < z then x + y else x + y - z)"
for x y z :: int
apply (auto simp add: not_less)
apply (rule antisym)
- apply (metis diff_ge_0_iff_ge minus_mod_self2 zmod_le_nonneg_dividend)
- apply (simp only: flip: minus_mod_self2 [of \<open>x + y\<close> z])
- apply (rule int_mod_ge)
- apply simp_all
+ apply (metis diff_ge_0_iff_ge minus_mod_self2 zmod_le_nonneg_dividend)
+ apply (simp only: flip: minus_mod_self2 [of \<open>x + y\<close> z])
+ apply (metis add.commute add_less_cancel_left add_mono_thms_linordered_field(5) diff_add_cancel diff_ge_0_iff_ge mod_pos_pos_trivial order_refl)
done
lemma uint_plus_if':
@@ -3596,16 +3599,13 @@
by (fact inj_unsigned)
lemma range_uint: \<open>range (uint :: 'a word \<Rightarrow> int) = {0..<2 ^ LENGTH('a::len)}\<close>
- by transfer (auto simp add: bintr_lt2p range_bintrunc)
+ apply transfer
+ apply (auto simp add: image_iff)
+ apply (metis take_bit_int_eq_self_iff)
+ done
lemma UNIV_eq: \<open>(UNIV :: 'a word set) = word_of_int ` {0..<2 ^ LENGTH('a::len)}\<close>
-proof -
- have \<open>uint ` (UNIV :: 'a word set) = uint ` (word_of_int :: int \<Rightarrow> 'a word) ` {0..<2 ^ LENGTH('a::len)}\<close>
- by transfer (simp add: range_bintrunc, auto simp add: take_bit_eq_mod)
- then show ?thesis
- using inj_image_eq_iff [of \<open>uint :: 'a word \<Rightarrow> int\<close> \<open>UNIV :: 'a word set\<close> \<open>word_of_int ` {0..<2 ^ LENGTH('a)} :: 'a word set\<close>, OF inj_uint]
- by simp
-qed
+ by (auto simp add: image_iff) (metis atLeastLessThan_iff linorder_not_le uint_split)
lemma card_word: "CARD('a word) = 2 ^ LENGTH('a::len)"
by (simp add: UNIV_eq card_image inj_on_word_of_int)
@@ -3620,18 +3620,6 @@
subsection \<open>Bitwise Operations on Words\<close>
-lemmas bin_log_bintrs = bin_trunc_not bin_trunc_xor bin_trunc_and bin_trunc_or
-
-\<comment> \<open>following definitions require both arithmetic and bit-wise word operations\<close>
-
-\<comment> \<open>to get \<open>word_no_log_defs\<close> from \<open>word_log_defs\<close>, using \<open>bin_log_bintrs\<close>\<close>
-lemmas wils1 = bin_log_bintrs [THEN word_of_int_eq_iff [THEN iffD2],
- folded uint_word_of_int_eq, THEN eq_reflection]
-
-\<comment> \<open>the binary operations only\<close> (* BH: why is this needed? *)
-lemmas word_log_binary_defs =
- word_and_def word_or_def word_xor_def
-
lemma word_wi_log_defs:
"NOT (word_of_int a) = word_of_int (NOT a)"
"word_of_int a AND word_of_int b = word_of_int (a AND b)"
@@ -3704,7 +3692,7 @@
by (simp only: test_bit_eq_bit) transfer_prover
lemma test_bit_wi [simp]:
- "(word_of_int x :: 'a::len word) !! n \<longleftrightarrow> n < LENGTH('a) \<and> bin_nth x n"
+ "(word_of_int x :: 'a::len word) !! n \<longleftrightarrow> n < LENGTH('a) \<and> bit x n"
by transfer simp
lemma word_ops_nth_size:
@@ -3714,29 +3702,29 @@
(x XOR y) !! n = (x !! n \<noteq> y !! n) \<and>
(NOT x) !! n = (\<not> x !! n)"
for x :: "'a::len word"
- unfolding word_size by transfer (simp add: bin_nth_ops)
+ by transfer (simp add: bit_or_iff bit_and_iff bit_xor_iff bit_not_iff)
lemma word_ao_nth:
"(x OR y) !! n = (x !! n | y !! n) \<and>
(x AND y) !! n = (x !! n \<and> y !! n)"
for x :: "'a::len word"
- by transfer (auto simp add: bin_nth_ops)
+ by transfer (auto simp add: bit_or_iff bit_and_iff)
lemmas msb0 = len_gt_0 [THEN diff_Suc_less, THEN word_ops_nth_size [unfolded word_size]]
lemmas msb1 = msb0 [where i = 0]
lemma test_bit_numeral [simp]:
"(numeral w :: 'a::len word) !! n \<longleftrightarrow>
- n < LENGTH('a) \<and> bin_nth (numeral w) n"
+ n < LENGTH('a) \<and> bit (numeral w :: int) n"
by transfer (rule refl)
lemma test_bit_neg_numeral [simp]:
"(- numeral w :: 'a::len word) !! n \<longleftrightarrow>
- n < LENGTH('a) \<and> bin_nth (- numeral w) n"
+ n < LENGTH('a) \<and> bit (- numeral w :: int) n"
by transfer (rule refl)
lemma test_bit_1 [simp]: "(1 :: 'a::len word) !! n \<longleftrightarrow> n = 0"
- by transfer auto
+ by transfer (auto simp add: bit_1_iff)
lemma nth_0 [simp]: "\<not> (0 :: 'a::len word) !! n"
by transfer simp
@@ -3825,7 +3813,7 @@
lemma word_add_not [simp]: "x + NOT x = -1"
for x :: "'a::len word"
- by transfer (simp add: bin_add_not)
+ by transfer (simp add: not_int_def)
lemma word_plus_and_or [simp]: "(x AND y) + (x OR y) = x + y"
for x :: "'a::len word"
@@ -3845,7 +3833,7 @@
lemma le_word_or2: "x \<le> x OR y"
for x y :: "'a::len word"
- by (auto simp: word_le_def uint_or intro: le_int_or)
+ by (simp add: or_greater_eq uint_or word_le_def)
lemmas le_word_or1 = xtrans(3) [OF word_bw_comms (2) le_word_or2]
lemmas word_and_le1 = xtrans(3) [OF word_ao_absorbs (4) [symmetric] le_word_or2]
@@ -3880,16 +3868,9 @@
lemma nth_sint:
fixes w :: "'a::len word"
defines "l \<equiv> LENGTH('a)"
- shows "bin_nth (sint w) n = (if n < l - 1 then w !! n else w !! (l - 1))"
+ shows "bit (sint w) n = (if n < l - 1 then w !! n else w !! (l - 1))"
unfolding sint_uint l_def
- by (auto simp: nth_sbintr word_test_bit_def [symmetric])
-
-lemma setBit_no [simp]: "setBit (numeral bin) n = word_of_int (bin_sc n True (numeral bin))"
- by transfer (simp add: bin_sc_eq)
-
-lemma clearBit_no [simp]:
- "clearBit (numeral bin) n = word_of_int (bin_sc n False (numeral bin))"
- by transfer (simp add: bin_sc_eq)
+ by (auto simp: bit_signed_take_bit_iff word_test_bit_def not_less min_def)
lemma test_bit_2p: "(word_of_int (2 ^ n)::'a::len word) !! m \<longleftrightarrow> m = n \<and> m < LENGTH('a)"
by transfer (auto simp add: bit_exp_iff)
@@ -3976,12 +3957,13 @@
text \<open>
see paper page 10, (1), (2), \<open>shiftr1_def\<close> is of the form of (1),
- where \<open>f\<close> (ie \<open>bin_rest\<close>) takes normal arguments to normal results,
+ where \<open>f\<close> (ie \<open>_ div 2\<close>) takes normal arguments to normal results,
thus we get (2) from (1)
\<close>
-lemma uint_shiftr1: "uint (shiftr1 w) = bin_rest (uint w)"
- by transfer simp
+lemma uint_shiftr1: "uint (shiftr1 w) = uint w div 2"
+ using uint_shiftr_eq [of w 1]
+ by (simp add: shiftr1_code)
lemma bit_sshiftr1_iff:
\<open>bit (sshiftr1 w) n \<longleftrightarrow> bit w (if n = LENGTH('a) - 1 then LENGTH('a) - 1 else Suc n)\<close>
@@ -4001,10 +3983,6 @@
using le_less_Suc_eq apply fastforce
done
-lemma sshiftr_eq:
- \<open>w >>> m = signed_drop_bit m w\<close>
- by (rule bit_eqI) (simp add: bit_signed_drop_bit_iff bit_sshiftr_word_iff)
-
lemma nth_sshiftr1: "sshiftr1 w !! n = (if n = size w - 1 then w !! n else w !! Suc n)"
apply transfer
apply (auto simp add: bit_take_bit_iff bit_signed_take_bit_iff min_def simp flip: bit_Suc)
@@ -4025,20 +4003,15 @@
by (fact uint_shiftr1)
lemma sshiftr1_div_2: "sint (sshiftr1 w) = sint w div 2"
- by transfer simp
+ using sint_signed_drop_bit_eq [of 1 w]
+ by (simp add: drop_bit_Suc sshiftr1_eq_signed_drop_bit_Suc_0)
lemma shiftr_div_2n: "uint (shiftr w n) = uint w div 2 ^ n"
- apply (unfold shiftr_def)
- apply (induct n)
- apply simp
- apply (simp add: shiftr1_div_2 mult.commute zdiv_zmult2_eq [symmetric])
- done
+ by (fact uint_shiftr_eq)
lemma sshiftr_div_2n: "sint (sshiftr w n) = sint w div 2 ^ n"
- apply transfer
- apply (rule bit_eqI)
- apply (simp add: bit_signed_take_bit_iff bit_drop_bit_eq min_def flip: drop_bit_eq_div)
- done
+ using sint_signed_drop_bit_eq [of n w]
+ by (simp add: drop_bit_eq_div sshiftr_eq)
lemma bit_bshiftr1_iff:
\<open>bit (bshiftr1 b w) n \<longleftrightarrow> b \<and> n = LENGTH('a) - 1 \<or> bit w (Suc n)\<close>
@@ -4095,12 +4068,12 @@
lemma shiftr1_bintr [simp]:
"(shiftr1 (numeral w) :: 'a::len word) =
- word_of_int (bin_rest (take_bit (LENGTH('a)) (numeral w)))"
+ word_of_int (take_bit LENGTH('a) (numeral w) div 2)"
by transfer simp
lemma sshiftr1_sbintr [simp]:
"(sshiftr1 (numeral w) :: 'a::len word) =
- word_of_int (bin_rest (signed_take_bit (LENGTH('a) - 1) (numeral w)))"
+ word_of_int (signed_take_bit (LENGTH('a) - 1) (numeral w) div 2)"
by transfer simp
text \<open>TODO: rules for \<^term>\<open>- (numeral n)\<close>\<close>
@@ -4119,7 +4092,7 @@
word_of_int (drop_bit (numeral n) (signed_take_bit (LENGTH('a) - 1) (numeral k)))\<close>
apply (rule word_eqI)
apply (cases \<open>LENGTH('a)\<close>)
- apply (simp_all add: word_size bit_drop_bit_eq nth_sshiftr nth_sbintr not_le not_less less_Suc_eq_le ac_simps)
+ apply (simp_all add: word_size bit_drop_bit_eq nth_sshiftr bit_signed_take_bit_iff min_def not_le not_less less_Suc_eq_le ac_simps)
done
lemma zip_replicate: "n \<ge> length ys \<Longrightarrow> zip (replicate n x) ys = map (\<lambda>y. (x, y)) ys"
@@ -4188,20 +4161,17 @@
by (auto simp add: test_bit_word_eq word_size Word.bit_mask_iff)
lemma mask_bin: "mask n = word_of_int (take_bit n (- 1))"
- by (auto simp add: nth_bintr word_size intro: word_eqI)
+ by transfer (simp add: take_bit_minus_one_eq_mask)
lemma and_mask_bintr: "w AND mask n = word_of_int (take_bit n (uint w))"
- apply (rule word_eqI)
- apply (simp add: nth_bintr word_size word_ops_nth_size)
- apply (auto simp add: test_bit_bin)
- done
+ by transfer (simp add: ac_simps take_bit_eq_mask)
lemma and_mask_wi: "word_of_int i AND mask n = word_of_int (take_bit n i)"
- by (auto simp add: nth_bintr word_size word_ops_nth_size word_eq_iff)
+ by (auto simp add: and_mask_bintr min_def not_le wi_bintr)
lemma and_mask_wi':
"word_of_int i AND mask n = (word_of_int (take_bit (min LENGTH('a) n) i) :: 'a::len word)"
- by (auto simp add: nth_bintr word_size word_ops_nth_size word_eq_iff)
+ by (auto simp add: and_mask_wi min_def wi_bintr)
lemma and_mask_no: "numeral i AND mask n = word_of_int (take_bit n (numeral i))"
unfolding word_numeral_alt by (rule and_mask_wi)
@@ -4214,16 +4184,10 @@
by transfer simp
lemma and_mask_lt_2p: "uint (w AND mask n) < 2 ^ n"
- apply (simp add: uint_and uint_mask_eq)
- apply (rule AND_upper2'')
- apply simp
- apply (auto simp add: mask_eq_exp_minus_1 min_def power_add algebra_simps dest!: le_Suc_ex)
- apply (metis add_minus_cancel le_add2 one_le_numeral power_add power_increasing uminus_add_conv_diff zle_diff1_eq)
- done
-
-lemma eq_mod_iff: "0 < n \<Longrightarrow> b = b mod n \<longleftrightarrow> 0 \<le> b \<and> b < n"
- for b n :: int
- by auto (metis pos_mod_conj)+
+ apply (simp flip: take_bit_eq_mask)
+ apply transfer
+ apply (auto simp add: min_def)
+ using antisym_conv take_bit_int_eq_self_iff by fastforce
lemma mask_eq_iff: "w AND mask n = w \<longleftrightarrow> uint w < 2 ^ n"
apply (auto simp flip: take_bit_eq_mask)
@@ -4243,11 +4207,11 @@
lemma less_mask_eq: "x < 2 ^ n \<Longrightarrow> x AND mask n = x"
for x :: "'a::len word"
- apply (simp add: and_mask_bintr)
+ apply (cases \<open>n < LENGTH('a)\<close>)
+ apply (simp_all add: not_less flip: take_bit_eq_mask exp_eq_zero_iff)
apply transfer
- apply (simp add: ac_simps)
- apply (auto simp add: min_def)
- apply (metis bintrunc_bintrunc_ge mod_pos_pos_trivial mult.commute mult.left_neutral mult_zero_left not_le of_bool_def take_bit_eq_mod take_bit_nonnegative)
+ apply (simp add: min_def)
+ apply (metis min_def nat_less_le take_bit_int_eq_self_iff take_bit_take_bit)
done
lemmas mask_eq_iff_w2p = trans [OF mask_eq_iff word_2p_lem [symmetric]]
@@ -4540,15 +4504,6 @@
lemmas word_split_bin' = word_split_def
lemmas word_cat_bin' = word_cat_eq
-lemma word_rsplit_no:
- "(word_rsplit (numeral bin :: 'b::len word) :: 'a word list) =
- map word_of_int (bin_rsplit (LENGTH('a::len))
- (LENGTH('b), take_bit (LENGTH('b)) (numeral bin)))"
- by (simp add: word_rsplit_def of_nat_take_bit)
-
-lemmas word_rsplit_no_cl [simp] = word_rsplit_no
- [unfolded bin_rsplitl_def bin_rsplit_l [symmetric]]
-
lemma test_bit_cat [OF refl]:
"wc = word_cat a b \<Longrightarrow> wc !! n = (n < size wc \<and>
(if n < size b then b !! n else a !! (n - size b)))"
@@ -4556,27 +4511,15 @@
apply (auto simp add: bit_concat_bit_iff bit_take_bit_iff)
done
-lemma split_uint_lem: "bin_split n (uint w) = (a, b) \<Longrightarrow>
- a = take_bit (LENGTH('a) - n) a \<and> b = take_bit (LENGTH('a)) b"
- for w :: "'a::len word"
- by transfer (simp add: drop_bit_take_bit ac_simps)
-
\<comment> \<open>keep quantifiers for use in simplification\<close>
lemma test_bit_split':
"word_split c = (a, b) \<longrightarrow>
(\<forall>n m.
b !! n = (n < size b \<and> c !! n) \<and>
a !! m = (m < size a \<and> c !! (m + size b)))"
- apply (unfold word_split_bin' test_bit_bin)
- apply (clarify)
- apply simp
- apply (erule conjE)
- apply (drule sym)
- apply (drule sym)
- apply (simp add: bit_take_bit_iff bit_drop_bit_eq)
- apply transfer
- apply (simp add: bit_take_bit_iff ac_simps)
- done
+ by (auto simp add: word_split_bin' test_bit_bin bit_unsigned_iff word_size
+ bit_drop_bit_eq ac_simps exp_eq_zero_iff
+ dest: bit_imp_le_length)
lemma test_bit_split:
"word_split c = (a, b) \<Longrightarrow>
@@ -4602,15 +4545,7 @@
result to the length given by the result type\<close>
lemma word_cat_id: "word_cat a b = b"
- by transfer simp
-
-\<comment> \<open>limited hom result\<close>
-lemma word_cat_hom:
- "LENGTH('a::len) \<le> LENGTH('b::len) + LENGTH('c::len) \<Longrightarrow>
- (word_cat (word_of_int w :: 'b word) (b :: 'c word) :: 'a word) =
- word_of_int (bin_cat w (size b) (uint b))"
- apply transfer
- using bintr_cat by auto
+ by transfer (simp add: take_bit_concat_bit_eq)
lemma word_cat_split_alt: "size w \<le> size u + size v \<Longrightarrow> word_split w = (u, v) \<Longrightarrow> word_cat u v = w"
apply (rule word_eqI)
@@ -4659,40 +4594,6 @@
apply (rule word_eqI, clarsimp simp: test_bit_cat word_size)+
done
-text \<open>
- This odd result arises from the fact that the statement of the
- result implies that the decoded words are of the same type,
- and therefore of the same length, as the original word.\<close>
-
-lemma word_rsplit_same: "word_rsplit w = [w]"
- apply (simp add: word_rsplit_def bin_rsplit_all)
- apply transfer
- apply simp
- done
-
-lemma word_rsplit_empty_iff_size: "word_rsplit w = [] \<longleftrightarrow> size w = 0"
- by (simp add: word_rsplit_def bin_rsplit_def word_size bin_rsplit_aux_simp_alt Let_def
- split: prod.split)
-
-lemma test_bit_rsplit:
- "sw = word_rsplit w \<Longrightarrow> m < size (hd sw) \<Longrightarrow>
- k < length sw \<Longrightarrow> (rev sw ! k) !! m = w !! (k * size (hd sw) + m)"
- for sw :: "'a::len word list"
- apply (unfold word_rsplit_def word_test_bit_def)
- apply (rule trans)
- apply (rule_tac f = "\<lambda>x. bin_nth x m" in arg_cong)
- apply (rule nth_map [symmetric])
- apply simp
- apply (rule bin_nth_rsplit)
- apply simp_all
- apply (simp add : word_size rev_map)
- apply (rule trans)
- defer
- apply (rule map_ident [THEN fun_cong])
- apply (rule refl [THEN map_cong])
- apply simp
- using bin_rsplit_size_sign take_bit_int_eq_self_iff by blast
-
lemma horner_sum_uint_exp_Cons_eq:
\<open>horner_sum uint (2 ^ LENGTH('a)) (w # ws) =
concat_bit LENGTH('a) (uint w) (horner_sum uint (2 ^ LENGTH('a)) ws)\<close>
@@ -4721,105 +4622,11 @@
"sw = size (hd wl) \<Longrightarrow> rc = word_rcat wl \<Longrightarrow> rc !! n =
(n < size rc \<and> n div sw < size wl \<and> (rev wl) ! (n div sw) !! (n mod sw))"
for wl :: "'a::len word list"
- by (simp add: word_size word_rcat_def bin_rcat_def foldl_map rev_map bit_horner_sum_uint_exp_iff)
+ by (simp add: word_size word_rcat_def foldl_map rev_map bit_horner_sum_uint_exp_iff)
(simp add: test_bit_eq_bit)
lemmas test_bit_cong = arg_cong [where f = "test_bit", THEN fun_cong]
-lemma test_bit_rsplit_alt:
- \<open>(word_rsplit w :: 'b::len word list) ! i !! m \<longleftrightarrow>
- w !! ((length (word_rsplit w :: 'b::len word list) - Suc i) * size (hd (word_rsplit w :: 'b::len word list)) + m)\<close>
- if \<open>i < length (word_rsplit w :: 'b::len word list)\<close> \<open>m < size (hd (word_rsplit w :: 'b::len word list))\<close> \<open>0 < length (word_rsplit w :: 'b::len word list)\<close>
- for w :: \<open>'a::len word\<close>
- apply (rule trans)
- apply (rule test_bit_cong)
- apply (rule rev_nth [of _ \<open>rev (word_rsplit w)\<close>, simplified rev_rev_ident])
- apply simp
- apply (rule that(1))
- apply simp
- apply (rule test_bit_rsplit)
- apply (rule refl)
- apply (rule asm_rl)
- apply (rule that(2))
- apply (rule diff_Suc_less)
- apply (rule that(3))
- done
-
-lemma word_rsplit_len_indep [OF refl refl refl refl]:
- "[u,v] = p \<Longrightarrow> [su,sv] = q \<Longrightarrow> word_rsplit u = su \<Longrightarrow>
- word_rsplit v = sv \<Longrightarrow> length su = length sv"
- by (auto simp: word_rsplit_def bin_rsplit_len_indep)
-
-lemma length_word_rsplit_size:
- "n = LENGTH('a::len) \<Longrightarrow>
- length (word_rsplit w :: 'a word list) \<le> m \<longleftrightarrow> size w \<le> m * n"
- by (auto simp: word_rsplit_def word_size bin_rsplit_len_le)
-
-lemmas length_word_rsplit_lt_size =
- length_word_rsplit_size [unfolded Not_eq_iff linorder_not_less [symmetric]]
-
-lemma length_word_rsplit_exp_size:
- "n = LENGTH('a::len) \<Longrightarrow>
- length (word_rsplit w :: 'a word list) = (size w + n - 1) div n"
- by (auto simp: word_rsplit_def word_size bin_rsplit_len)
-
-lemma length_word_rsplit_even_size:
- "n = LENGTH('a::len) \<Longrightarrow> size w = m * n \<Longrightarrow>
- length (word_rsplit w :: 'a word list) = m"
- by (cases \<open>LENGTH('a)\<close>) (simp_all add: length_word_rsplit_exp_size div_nat_eqI)
-
-lemmas length_word_rsplit_exp_size' = refl [THEN length_word_rsplit_exp_size]
-
-\<comment> \<open>alternative proof of \<open>word_rcat_rsplit\<close>\<close>
-lemmas tdle = times_div_less_eq_dividend
-lemmas dtle = xtrans(4) [OF tdle mult.commute]
-
-lemma word_rcat_rsplit: "word_rcat (word_rsplit w) = w"
- apply (rule word_eqI)
- apply (clarsimp simp: test_bit_rcat word_size)
- apply (subst refl [THEN test_bit_rsplit])
- apply (simp_all add: word_size
- refl [THEN length_word_rsplit_size [simplified not_less [symmetric], simplified]])
- apply safe
- apply (erule xtrans(7), rule dtle)+
- done
-
-lemma size_word_rsplit_rcat_size:
- "word_rcat ws = frcw \<Longrightarrow> size frcw = length ws * LENGTH('a)
- \<Longrightarrow> length (word_rsplit frcw::'a word list) = length ws"
- for ws :: "'a::len word list" and frcw :: "'b::len word"
- by (cases \<open>LENGTH('a)\<close>) (simp_all add: word_size length_word_rsplit_exp_size' div_nat_eqI)
-
-lemma msrevs:
- "0 < n \<Longrightarrow> (k * n + m) div n = m div n + k"
- "(k * n + m) mod n = m mod n"
- for n :: nat
- by (auto simp: add.commute)
-
-lemma word_rsplit_rcat_size [OF refl]:
- "word_rcat ws = frcw \<Longrightarrow>
- size frcw = length ws * LENGTH('a) \<Longrightarrow> word_rsplit frcw = ws"
- for ws :: "'a::len word list"
- apply (frule size_word_rsplit_rcat_size, assumption)
- apply (clarsimp simp add : word_size)
- apply (rule nth_equalityI, assumption)
- apply clarsimp
- apply (rule word_eqI [rule_format])
- apply (rule trans)
- apply (rule test_bit_rsplit_alt)
- apply (clarsimp simp: word_size)+
- apply (rule trans)
- apply (rule test_bit_rcat [OF refl refl])
- apply (simp add: word_size)
- apply (subst rev_nth)
- apply arith
- apply (simp add: le0 [THEN [2] xtrans(7), THEN diff_Suc_less])
- apply safe
- apply (simp add: diff_mult_distrib)
- apply (cases "size ws")
- apply simp_all
- done
-
subsection \<open>Rotation\<close>
@@ -5072,11 +4879,11 @@
by transfer simp
with that show ?thesis
apply transfer
- apply simp
+ apply simp
apply (subst take_bit_diff [symmetric])
apply (subst nat_take_bit_eq)
- apply (simp add: nat_le_eq_zle)
- apply (simp add: nat_diff_distrib take_bit_nat_eq_self_iff less_imp_diff_less bintr_lt2p)
+ apply (simp add: nat_le_eq_zle)
+ apply (simp add: nat_diff_distrib take_bit_nat_eq_self_iff less_imp_diff_less)
done
qed
@@ -5285,26 +5092,16 @@
lemma mask_Suc_0: "mask (Suc 0) = 1"
using mask_1 by simp
-lemma bin_last_bintrunc: "bin_last (take_bit l n) = (l > 0 \<and> bin_last n)"
+lemma bin_last_bintrunc: "odd (take_bit l n) \<longleftrightarrow> l > 0 \<and> odd n"
by simp
lemma word_and_1:
"n AND 1 = (if n !! 0 then 1 else 0)" for n :: "_ word"
by (rule bit_word_eqI) (auto simp add: bit_and_iff test_bit_eq_bit bit_1_iff intro: gr0I)
-lemma bintrunc_shiftl:
- "take_bit n (m << i) = take_bit (n - i) m << i"
- for m :: int
- by (rule bit_eqI) (auto simp add: bit_take_bit_iff)
-
-lemma uint_shiftl:
- "uint (n << i) = take_bit (size n) (uint n << i)"
- by transfer (simp add: push_bit_take_bit shiftl_eq_push_bit)
-
-
-subsection \<open>Misc\<close>
-
-ML_file \<open>Tools/word_lib.ML\<close>
+
+subsection \<open>SMT support\<close>
+
ML_file \<open>Tools/smt_word.ML\<close>
end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Word/Word_rsplit.thy Sat Oct 17 18:36:08 2020 +0100
@@ -0,0 +1,149 @@
+(* Title: HOL/Word/Word_rsplit.thy
+ Author: Jeremy Dawson and Gerwin Klein, NICTA
+*)
+
+theory Word_rsplit
+ imports Bits_Int Word
+begin
+
+definition word_rsplit :: "'a::len word \<Rightarrow> 'b::len word list"
+ where "word_rsplit w = map word_of_int (bin_rsplit (LENGTH('b)) (LENGTH('a), uint w))"
+
+lemma word_rsplit_no:
+ "(word_rsplit (numeral bin :: 'b::len word) :: 'a word list) =
+ map word_of_int (bin_rsplit (LENGTH('a::len))
+ (LENGTH('b), take_bit (LENGTH('b)) (numeral bin)))"
+ by (simp add: word_rsplit_def of_nat_take_bit)
+
+lemmas word_rsplit_no_cl [simp] = word_rsplit_no
+ [unfolded bin_rsplitl_def bin_rsplit_l [symmetric]]
+
+text \<open>
+ This odd result arises from the fact that the statement of the
+ result implies that the decoded words are of the same type,
+ and therefore of the same length, as the original word.\<close>
+
+lemma word_rsplit_same: "word_rsplit w = [w]"
+ apply (simp add: word_rsplit_def bin_rsplit_all)
+ apply transfer
+ apply simp
+ done
+
+lemma word_rsplit_empty_iff_size: "word_rsplit w = [] \<longleftrightarrow> size w = 0"
+ by (simp add: word_rsplit_def bin_rsplit_def word_size bin_rsplit_aux_simp_alt Let_def
+ split: prod.split)
+
+lemma test_bit_rsplit:
+ "sw = word_rsplit w \<Longrightarrow> m < size (hd sw) \<Longrightarrow>
+ k < length sw \<Longrightarrow> (rev sw ! k) !! m = w !! (k * size (hd sw) + m)"
+ for sw :: "'a::len word list"
+ apply (unfold word_rsplit_def word_test_bit_def)
+ apply (rule trans)
+ apply (rule_tac f = "\<lambda>x. bin_nth x m" in arg_cong)
+ apply (rule nth_map [symmetric])
+ apply simp
+ apply (rule bin_nth_rsplit)
+ apply simp_all
+ apply (simp add : word_size rev_map)
+ apply (rule trans)
+ defer
+ apply (rule map_ident [THEN fun_cong])
+ apply (rule refl [THEN map_cong])
+ apply simp
+ using bin_rsplit_size_sign take_bit_int_eq_self_iff by blast
+
+lemma test_bit_rsplit_alt:
+ \<open>(word_rsplit w :: 'b::len word list) ! i !! m \<longleftrightarrow>
+ w !! ((length (word_rsplit w :: 'b::len word list) - Suc i) * size (hd (word_rsplit w :: 'b::len word list)) + m)\<close>
+ if \<open>i < length (word_rsplit w :: 'b::len word list)\<close> \<open>m < size (hd (word_rsplit w :: 'b::len word list))\<close> \<open>0 < length (word_rsplit w :: 'b::len word list)\<close>
+ for w :: \<open>'a::len word\<close>
+ apply (rule trans)
+ apply (rule test_bit_cong)
+ apply (rule rev_nth [of _ \<open>rev (word_rsplit w)\<close>, simplified rev_rev_ident])
+ apply simp
+ apply (rule that(1))
+ apply simp
+ apply (rule test_bit_rsplit)
+ apply (rule refl)
+ apply (rule asm_rl)
+ apply (rule that(2))
+ apply (rule diff_Suc_less)
+ apply (rule that(3))
+ done
+
+lemma word_rsplit_len_indep [OF refl refl refl refl]:
+ "[u,v] = p \<Longrightarrow> [su,sv] = q \<Longrightarrow> word_rsplit u = su \<Longrightarrow>
+ word_rsplit v = sv \<Longrightarrow> length su = length sv"
+ by (auto simp: word_rsplit_def bin_rsplit_len_indep)
+
+lemma length_word_rsplit_size:
+ "n = LENGTH('a::len) \<Longrightarrow>
+ length (word_rsplit w :: 'a word list) \<le> m \<longleftrightarrow> size w \<le> m * n"
+ by (auto simp: word_rsplit_def word_size bin_rsplit_len_le)
+
+lemmas length_word_rsplit_lt_size =
+ length_word_rsplit_size [unfolded Not_eq_iff linorder_not_less [symmetric]]
+
+lemma length_word_rsplit_exp_size:
+ "n = LENGTH('a::len) \<Longrightarrow>
+ length (word_rsplit w :: 'a word list) = (size w + n - 1) div n"
+ by (auto simp: word_rsplit_def word_size bin_rsplit_len)
+
+lemma length_word_rsplit_even_size:
+ "n = LENGTH('a::len) \<Longrightarrow> size w = m * n \<Longrightarrow>
+ length (word_rsplit w :: 'a word list) = m"
+ by (cases \<open>LENGTH('a)\<close>) (simp_all add: length_word_rsplit_exp_size div_nat_eqI)
+
+lemmas length_word_rsplit_exp_size' = refl [THEN length_word_rsplit_exp_size]
+
+\<comment> \<open>alternative proof of \<open>word_rcat_rsplit\<close>\<close>
+lemmas tdle = times_div_less_eq_dividend
+lemmas dtle = xtrans(4) [OF tdle mult.commute]
+
+lemma word_rcat_rsplit: "word_rcat (word_rsplit w) = w"
+ apply (rule word_eqI)
+ apply (clarsimp simp: test_bit_rcat word_size)
+ apply (subst refl [THEN test_bit_rsplit])
+ apply (simp_all add: word_size
+ refl [THEN length_word_rsplit_size [simplified not_less [symmetric], simplified]])
+ apply safe
+ apply (erule xtrans(7), rule dtle)+
+ done
+
+lemma size_word_rsplit_rcat_size:
+ "word_rcat ws = frcw \<Longrightarrow> size frcw = length ws * LENGTH('a)
+ \<Longrightarrow> length (word_rsplit frcw::'a word list) = length ws"
+ for ws :: "'a::len word list" and frcw :: "'b::len word"
+ by (cases \<open>LENGTH('a)\<close>) (simp_all add: word_size length_word_rsplit_exp_size' div_nat_eqI)
+
+lemma msrevs:
+ "0 < n \<Longrightarrow> (k * n + m) div n = m div n + k"
+ "(k * n + m) mod n = m mod n"
+ for n :: nat
+ by (auto simp: add.commute)
+
+lemma word_rsplit_rcat_size [OF refl]:
+ "word_rcat ws = frcw \<Longrightarrow>
+ size frcw = length ws * LENGTH('a) \<Longrightarrow> word_rsplit frcw = ws"
+ for ws :: "'a::len word list"
+ apply (frule size_word_rsplit_rcat_size, assumption)
+ apply (clarsimp simp add : word_size)
+ apply (rule nth_equalityI, assumption)
+ apply clarsimp
+ apply (rule word_eqI [rule_format])
+ apply (rule trans)
+ apply (rule test_bit_rsplit_alt)
+ apply (clarsimp simp: word_size)+
+ apply (rule trans)
+ apply (rule test_bit_rcat [OF refl refl])
+ apply (simp add: word_size)
+ apply (subst rev_nth)
+ apply arith
+ apply (simp add: le0 [THEN [2] xtrans(7), THEN diff_Suc_less])
+ apply safe
+ apply (simp add: diff_mult_distrib)
+ apply (cases "size ws")
+ apply simp_all
+ done
+
+end
\ No newline at end of file