--- a/src/HOL/Library/Bit_Operations.thy Sat Aug 29 16:30:33 2020 +0100
+++ b/src/HOL/Library/Bit_Operations.thy Sun Aug 30 15:15:28 2020 +0000
@@ -737,15 +737,92 @@
qed
qed
+context ring_bit_operations
+begin
+
+lemma even_of_int_iff:
+ \<open>even (of_int k) \<longleftrightarrow> even k\<close>
+ by (induction k rule: int_bit_induct) simp_all
+
+lemma bit_of_int_iff:
+ \<open>bit (of_int k) n \<longleftrightarrow> (2::'a) ^ n \<noteq> 0 \<and> bit k n\<close>
+proof (cases \<open>(2::'a) ^ n = 0\<close>)
+ case True
+ then show ?thesis
+ by (simp add: exp_eq_0_imp_not_bit)
+next
+ case False
+ then have \<open>bit (of_int k) n \<longleftrightarrow> bit k n\<close>
+ proof (induction k arbitrary: n rule: int_bit_induct)
+ case zero
+ then show ?case
+ by simp
+ next
+ case minus
+ then show ?case
+ by simp
+ next
+ case (even k)
+ then show ?case
+ using bit_double_iff [of \<open>of_int k\<close> n] Parity.bit_double_iff [of k n]
+ by (cases n) (auto simp add: ac_simps dest: mult_not_zero)
+ next
+ case (odd k)
+ then show ?case
+ using bit_double_iff [of \<open>of_int k\<close> n]
+ by (cases n) (auto simp add: ac_simps bit_double_iff even_bit_succ_iff Parity.bit_Suc dest: mult_not_zero)
+ qed
+ with False show ?thesis
+ by simp
+qed
+
+lemma push_bit_of_int:
+ \<open>push_bit n (of_int k) = of_int (push_bit n k)\<close>
+ by (simp add: push_bit_eq_mult semiring_bit_shifts_class.push_bit_eq_mult)
+
+lemma of_int_push_bit:
+ \<open>of_int (push_bit n k) = push_bit n (of_int k)\<close>
+ by (simp add: push_bit_eq_mult semiring_bit_shifts_class.push_bit_eq_mult)
+
+lemma take_bit_of_int:
+ \<open>take_bit n (of_int k) = of_int (take_bit n k)\<close>
+ by (rule bit_eqI) (simp add: bit_take_bit_iff Parity.bit_take_bit_iff bit_of_int_iff)
+
+lemma of_int_take_bit:
+ \<open>of_int (take_bit n k) = take_bit n (of_int k)\<close>
+ by (rule bit_eqI) (simp add: bit_take_bit_iff Parity.bit_take_bit_iff bit_of_int_iff)
+
+lemma of_int_not_eq:
+ \<open>of_int (NOT k) = NOT (of_int k)\<close>
+ by (rule bit_eqI) (simp add: bit_not_iff Bit_Operations.bit_not_iff bit_of_int_iff)
+
+lemma of_int_and_eq:
+ \<open>of_int (k AND l) = of_int k AND of_int l\<close>
+ by (rule bit_eqI) (simp add: bit_of_int_iff bit_and_iff Bit_Operations.bit_and_iff)
+
+lemma of_int_or_eq:
+ \<open>of_int (k OR l) = of_int k OR of_int l\<close>
+ by (rule bit_eqI) (simp add: bit_of_int_iff bit_or_iff Bit_Operations.bit_or_iff)
+
+lemma of_int_xor_eq:
+ \<open>of_int (k XOR l) = of_int k XOR of_int l\<close>
+ by (rule bit_eqI) (simp add: bit_of_int_iff bit_xor_iff Bit_Operations.bit_xor_iff)
+
+lemma of_int_mask_eq:
+ \<open>of_int (mask n) = mask n\<close>
+ by (induction n) (simp_all add: mask_Suc_double Bit_Operations.mask_Suc_double of_int_or_eq)
+
+end
+
subsection \<open>Bit concatenation\<close>
definition concat_bit :: \<open>nat \<Rightarrow> int \<Rightarrow> int \<Rightarrow> int\<close>
- where \<open>concat_bit n k l = (k AND mask n) OR push_bit n l\<close>
+ where \<open>concat_bit n k l = take_bit n k OR push_bit n l\<close>
lemma bit_concat_bit_iff:
\<open>bit (concat_bit m k l) n \<longleftrightarrow> n < m \<and> bit k n \<or> m \<le> n \<and> bit l (n - m)\<close>
- by (simp add: concat_bit_def bit_or_iff bit_and_iff bit_mask_iff bit_push_bit_iff ac_simps)
+ by (simp add: concat_bit_def bit_or_iff bit_and_iff bit_take_bit_iff bit_push_bit_iff ac_simps)
lemma concat_bit_eq:
\<open>concat_bit n k l = take_bit n k + push_bit n l\<close>
@@ -784,12 +861,52 @@
\<open>concat_bit m (concat_bit n k l) r = concat_bit (min m n) k (concat_bit (m - n) l r)\<close>
by (rule bit_eqI) (auto simp add: bit_concat_bit_iff ac_simps min_def)
+lemma concat_bit_eq_iff:
+ \<open>concat_bit n k l = concat_bit n r s
+ \<longleftrightarrow> take_bit n k = take_bit n r \<and> l = s\<close> (is \<open>?P \<longleftrightarrow> ?Q\<close>)
+proof
+ assume ?Q
+ then show ?P
+ by (simp add: concat_bit_def)
+next
+ assume ?P
+ then have *: \<open>bit (concat_bit n k l) m = bit (concat_bit n r s) m\<close> for m
+ by (simp add: bit_eq_iff)
+ have \<open>take_bit n k = take_bit n r\<close>
+ proof (rule bit_eqI)
+ fix m
+ from * [of m]
+ show \<open>bit (take_bit n k) m \<longleftrightarrow> bit (take_bit n r) m\<close>
+ by (auto simp add: bit_take_bit_iff bit_concat_bit_iff)
+ qed
+ moreover have \<open>push_bit n l = push_bit n s\<close>
+ proof (rule bit_eqI)
+ fix m
+ from * [of m]
+ show \<open>bit (push_bit n l) m \<longleftrightarrow> bit (push_bit n s) m\<close>
+ by (auto simp add: bit_push_bit_iff bit_concat_bit_iff)
+ qed
+ then have \<open>l = s\<close>
+ by (simp add: push_bit_eq_mult)
+ ultimately show ?Q
+ by (simp add: concat_bit_def)
+qed
+
+lemma take_bit_concat_bit_eq:
+ \<open>take_bit m (concat_bit n k l) = concat_bit (min m n) k (take_bit (m - n) l)\<close>
+ by (rule bit_eqI)
+ (auto simp add: bit_take_bit_iff bit_concat_bit_iff min_def)
+
subsection \<open>Taking bit with sign propagation\<close>
definition signed_take_bit :: \<open>nat \<Rightarrow> int \<Rightarrow> int\<close>
where \<open>signed_take_bit n k = concat_bit n k (- of_bool (bit k n))\<close>
+lemma signed_take_bit_unfold:
+ \<open>signed_take_bit n k = take_bit n k OR (of_bool (bit k n) * NOT (mask n))\<close>
+ by (simp add: signed_take_bit_def concat_bit_def push_bit_minus_one_eq_not_mask)
+
lemma signed_take_bit_eq:
\<open>signed_take_bit n k = take_bit n k\<close> if \<open>\<not> bit k n\<close>
using that by (simp add: signed_take_bit_def)
@@ -1044,11 +1161,11 @@
instance proof
fix m n q :: nat
show \<open>bit (m AND n) q \<longleftrightarrow> bit m q \<and> bit n q\<close>
- by (auto simp add: and_nat_def bit_and_iff less_le bit_eq_iff)
+ by (auto simp add: bit_nat_iff and_nat_def bit_and_iff less_le bit_eq_iff)
show \<open>bit (m OR n) q \<longleftrightarrow> bit m q \<or> bit n q\<close>
- by (auto simp add: or_nat_def bit_or_iff less_le bit_eq_iff)
+ by (auto simp add: bit_nat_iff or_nat_def bit_or_iff less_le bit_eq_iff)
show \<open>bit (m XOR n) q \<longleftrightarrow> bit m q \<noteq> bit n q\<close>
- by (auto simp add: xor_nat_def bit_xor_iff less_le bit_eq_iff)
+ by (auto simp add: bit_nat_iff xor_nat_def bit_xor_iff less_le bit_eq_iff)
qed (simp add: mask_nat_def)
end
@@ -1089,6 +1206,32 @@
\<open>n XOR Suc 0 = n + of_bool (even n) - of_bool (odd n)\<close>
using xor_one_eq [of n] by simp
+context semiring_bit_operations
+begin
+
+lemma of_nat_and_eq:
+ \<open>of_nat (m AND n) = of_nat m AND of_nat n\<close>
+ by (rule bit_eqI) (simp add: bit_of_nat_iff bit_and_iff Bit_Operations.bit_and_iff)
+
+lemma of_nat_or_eq:
+ \<open>of_nat (m OR n) = of_nat m OR of_nat n\<close>
+ by (rule bit_eqI) (simp add: bit_of_nat_iff bit_or_iff Bit_Operations.bit_or_iff)
+
+lemma of_nat_xor_eq:
+ \<open>of_nat (m XOR n) = of_nat m XOR of_nat n\<close>
+ by (rule bit_eqI) (simp add: bit_of_nat_iff bit_xor_iff Bit_Operations.bit_xor_iff)
+
+end
+
+context ring_bit_operations
+begin
+
+lemma of_nat_mask_eq:
+ \<open>of_nat (mask n) = mask n\<close>
+ by (induction n) (simp_all add: mask_Suc_double Bit_Operations.mask_Suc_double of_nat_or_eq)
+
+end
+
subsection \<open>Instances for \<^typ>\<open>integer\<close> and \<^typ>\<open>natural\<close>\<close>
@@ -1224,4 +1367,33 @@
\<^item> (Bounded) conversion from and to a list of bits: @{thm horner_sum_bit_eq_take_bit [where ?'a = int, no_vars]}
\<close>
+context semiring_bit_operations
+begin
+
+lemma push_bit_and [simp]:
+ \<open>push_bit n (a AND b) = push_bit n a AND push_bit n b\<close>
+ by (rule bit_eqI) (auto simp add: bit_push_bit_iff bit_and_iff)
+
+lemma push_bit_or [simp]:
+ \<open>push_bit n (a OR b) = push_bit n a OR push_bit n b\<close>
+ by (rule bit_eqI) (auto simp add: bit_push_bit_iff bit_or_iff)
+
+lemma push_bit_xor [simp]:
+ \<open>push_bit n (a XOR b) = push_bit n a XOR push_bit n b\<close>
+ by (rule bit_eqI) (auto simp add: bit_push_bit_iff bit_xor_iff)
+
+lemma drop_bit_and [simp]:
+ \<open>drop_bit n (a AND b) = drop_bit n a AND drop_bit n b\<close>
+ by (rule bit_eqI) (auto simp add: bit_drop_bit_eq bit_and_iff)
+
+lemma drop_bit_or [simp]:
+ \<open>drop_bit n (a OR b) = drop_bit n a OR drop_bit n b\<close>
+ by (rule bit_eqI) (auto simp add: bit_drop_bit_eq bit_or_iff)
+
+lemma drop_bit_xor [simp]:
+ \<open>drop_bit n (a XOR b) = drop_bit n a XOR drop_bit n b\<close>
+ by (rule bit_eqI) (auto simp add: bit_drop_bit_eq bit_xor_iff)
+
end
+
+end
--- a/src/HOL/Parity.thy Sat Aug 29 16:30:33 2020 +0100
+++ b/src/HOL/Parity.thy Sun Aug 30 15:15:28 2020 +0000
@@ -976,6 +976,20 @@
\<open>bit (numeral Num.One) n \<longleftrightarrow> n = 0\<close>
by (simp add: bit_rec)
+lemma exp_add_not_zero_imp:
+ \<open>2 ^ m \<noteq> 0\<close> and \<open>2 ^ n \<noteq> 0\<close> if \<open>2 ^ (m + n) \<noteq> 0\<close>
+proof -
+ have \<open>\<not> (2 ^ m = 0 \<or> 2 ^ n = 0)\<close>
+ proof (rule notI)
+ assume \<open>2 ^ m = 0 \<or> 2 ^ n = 0\<close>
+ then have \<open>2 ^ (m + n) = 0\<close>
+ by (rule disjE) (simp_all add: power_add)
+ with that show False ..
+ qed
+ then show \<open>2 ^ m \<noteq> 0\<close> and \<open>2 ^ n \<noteq> 0\<close>
+ by simp_all
+qed
+
end
lemma nat_bit_induct [case_names zero even odd]:
@@ -1111,6 +1125,43 @@
qed
qed
+context semiring_bits
+begin
+
+lemma even_of_nat_iff:
+ \<open>even (of_nat n) \<longleftrightarrow> even n\<close>
+ by (induction n rule: nat_bit_induct) simp_all
+
+lemma bit_of_nat_iff:
+ \<open>bit (of_nat m) n \<longleftrightarrow> (2::'a) ^ n \<noteq> 0 \<and> bit m n\<close>
+proof (cases \<open>(2::'a) ^ n = 0\<close>)
+ case True
+ then show ?thesis
+ by (simp add: exp_eq_0_imp_not_bit)
+next
+ case False
+ then have \<open>bit (of_nat m) n \<longleftrightarrow> bit m n\<close>
+ proof (induction m arbitrary: n rule: nat_bit_induct)
+ case zero
+ then show ?case
+ by simp
+ next
+ case (even m)
+ then show ?case
+ by (cases n)
+ (auto simp add: bit_double_iff Parity.bit_double_iff dest: mult_not_zero)
+ next
+ case (odd m)
+ then show ?case
+ by (cases n)
+ (auto simp add: bit_double_iff even_bit_succ_iff Parity.bit_Suc dest: mult_not_zero)
+ qed
+ with False show ?thesis
+ by simp
+qed
+
+end
+
instantiation int :: semiring_bits
begin
@@ -1453,6 +1504,27 @@
end
+context semiring_bit_shifts
+begin
+
+lemma push_bit_of_nat:
+ \<open>push_bit n (of_nat m) = of_nat (push_bit n m)\<close>
+ by (simp add: push_bit_eq_mult semiring_bit_shifts_class.push_bit_eq_mult)
+
+lemma of_nat_push_bit:
+ \<open>of_nat (push_bit m n) = push_bit m (of_nat n)\<close>
+ by (simp add: push_bit_eq_mult semiring_bit_shifts_class.push_bit_eq_mult)
+
+lemma take_bit_of_nat:
+ \<open>take_bit n (of_nat m) = of_nat (take_bit n m)\<close>
+ by (rule bit_eqI) (simp add: bit_take_bit_iff Parity.bit_take_bit_iff bit_of_nat_iff)
+
+lemma of_nat_take_bit:
+ \<open>of_nat (take_bit n m) = take_bit n (of_nat m)\<close>
+ by (rule bit_eqI) (simp add: bit_take_bit_iff Parity.bit_take_bit_iff bit_of_nat_iff)
+
+end
+
instantiation int :: semiring_bit_shifts
begin
@@ -1498,10 +1570,6 @@
"push_bit n a = 0 \<longleftrightarrow> a = 0"
by (simp add: push_bit_eq_mult)
-lemma push_bit_of_nat:
- "push_bit n (of_nat m) = of_nat (push_bit n m)"
- by (simp add: push_bit_eq_mult Parity.push_bit_eq_mult)
-
lemma take_bit_add:
"take_bit n (take_bit n a + take_bit n b) = take_bit n (a + b)"
by (simp add: take_bit_eq_mod mod_simps)
@@ -1534,10 +1602,6 @@
\<open>take_bit (numeral l) (numeral (Num.Bit1 k)) = take_bit (pred_numeral l) (numeral k) * 2 + 1\<close>
by (simp add: take_bit_rec numeral_Bit1_div_2 mod_2_eq_odd)
-lemma take_bit_of_nat:
- "take_bit n (of_nat m) = of_nat (take_bit n m)"
- by (simp add: take_bit_eq_mod Parity.take_bit_eq_mod of_nat_mod [of m "2 ^ n"])
-
lemma drop_bit_Suc_bit0 [simp]:
\<open>drop_bit (Suc n) (numeral (Num.Bit0 k)) = drop_bit n (numeral k)\<close>
by (simp add: drop_bit_Suc numeral_Bit0_div_2)
@@ -1569,18 +1633,10 @@
by (simp add: bit_iff_odd semiring_bits_class.bit_iff_odd)
qed
-lemma of_nat_push_bit:
- \<open>of_nat (push_bit m n) = push_bit m (of_nat n)\<close>
- by (simp add: push_bit_eq_mult semiring_bit_shifts_class.push_bit_eq_mult)
-
lemma of_nat_drop_bit:
\<open>of_nat (drop_bit m n) = drop_bit m (of_nat n)\<close>
by (simp add: drop_bit_eq_div semiring_bit_shifts_class.drop_bit_eq_div of_nat_div)
-lemma of_nat_take_bit:
- \<open>of_nat (take_bit m n) = take_bit m (of_nat n)\<close>
- by (simp add: take_bit_eq_mod semiring_bit_shifts_class.take_bit_eq_mod of_nat_mod)
-
lemma bit_push_bit_iff_of_nat_iff:
\<open>bit (push_bit m (of_nat r)) n \<longleftrightarrow> m \<le> n \<and> bit (of_nat r) (n - m)\<close>
by (auto simp add: bit_push_bit_iff)
@@ -1591,9 +1647,9 @@
instance int :: unique_euclidean_semiring_with_bit_shifts ..
-lemma bit_nat_iff [simp]:
- \<open>bit (nat k) n \<longleftrightarrow> k > 0 \<and> bit k n\<close>
-proof (cases \<open>k > 0\<close>)
+lemma bit_nat_iff:
+ \<open>bit (nat k) n \<longleftrightarrow> k \<ge> 0 \<and> bit k n\<close>
+proof (cases \<open>k \<ge> 0\<close>)
case True
moreover define m where \<open>m = nat k\<close>
ultimately have \<open>k = int m\<close>
@@ -1606,6 +1662,21 @@
by simp
qed
+lemma push_bit_nat_eq:
+ \<open>push_bit n (nat k) = nat (push_bit n k)\<close>
+ by (cases \<open>k \<ge> 0\<close>) (simp_all add: push_bit_eq_mult nat_mult_distrib not_le mult_nonneg_nonpos2)
+
+lemma drop_bit_nat_eq:
+ \<open>drop_bit n (nat k) = nat (drop_bit n k)\<close>
+ apply (cases \<open>k \<ge> 0\<close>)
+ apply (simp_all add: drop_bit_eq_div nat_div_distrib nat_power_eq not_le)
+ apply (simp add: divide_int_def)
+ done
+
+lemma take_bit_nat_eq:
+ \<open>take_bit n (nat k) = nat (take_bit n k)\<close> if \<open>k \<ge> 0\<close>
+ using that by (simp add: take_bit_eq_mod nat_mod_distrib nat_power_eq)
+
lemma nat_take_bit_eq:
\<open>nat (take_bit n k) = take_bit n (nat k)\<close>
if \<open>k \<ge> 0\<close>
--- a/src/HOL/Word/Conversions.thy Sat Aug 29 16:30:33 2020 +0100
+++ b/src/HOL/Word/Conversions.thy Sun Aug 30 15:15:28 2020 +0000
@@ -13,7 +13,8 @@
hide_const (open) unat uint sint word_of_int ucast scast
-subsection \<open>Conversions to words\<close>
+
+subsection \<open>Conversions to word\<close>
abbreviation word_of_nat :: \<open>nat \<Rightarrow> 'a::len word\<close>
where \<open>word_of_nat \<equiv> of_nat\<close>
@@ -57,81 +58,10 @@
\<open>word_of_int k = (0 :: 'a::len word) \<longleftrightarrow> 2 ^ LENGTH('a) dvd k\<close>
using of_int_word_eq_iff [where ?'a = 'a, of k 0] by (simp add: take_bit_eq_0_iff)
-lemma int_AND_eq:
- \<open>int (m AND n) = int m AND int n\<close>
- by (rule bit_eqI) (simp add: bit_and_iff)
-
-lemma int_OR_eq:
- \<open>int (m OR n) = int m OR int n\<close>
- by (rule bit_eqI) (simp add: bit_or_iff)
-
-lemma int_XOR_eq:
- \<open>int (m XOR n) = int m XOR int n\<close>
- by (rule bit_eqI) (simp add: bit_xor_iff)
-
-context semiring_bit_operations
-begin
-
-lemma push_bit_and [simp]:
- \<open>push_bit n (a AND b) = push_bit n a AND push_bit n b\<close>
- by (rule bit_eqI) (auto simp add: bit_push_bit_iff bit_and_iff)
-
-lemma push_bit_or [simp]:
- \<open>push_bit n (a OR b) = push_bit n a OR push_bit n b\<close>
- by (rule bit_eqI) (auto simp add: bit_push_bit_iff bit_or_iff)
-
-lemma push_bit_xor [simp]:
- \<open>push_bit n (a XOR b) = push_bit n a XOR push_bit n b\<close>
- by (rule bit_eqI) (auto simp add: bit_push_bit_iff bit_xor_iff)
-
-lemma drop_bit_and [simp]:
- \<open>drop_bit n (a AND b) = drop_bit n a AND drop_bit n b\<close>
- by (rule bit_eqI) (auto simp add: bit_drop_bit_eq bit_and_iff)
-
-lemma drop_bit_or [simp]:
- \<open>drop_bit n (a OR b) = drop_bit n a OR drop_bit n b\<close>
- by (rule bit_eqI) (auto simp add: bit_drop_bit_eq bit_or_iff)
-lemma drop_bit_xor [simp]:
- \<open>drop_bit n (a XOR b) = drop_bit n a XOR drop_bit n b\<close>
- by (rule bit_eqI) (auto simp add: bit_drop_bit_eq bit_xor_iff)
-
-end
-
-lemma bit_word_of_nat_iff:
- \<open>bit (word_of_nat m :: 'a::len word) n \<longleftrightarrow> n < LENGTH('a) \<and> bit m n\<close>
- by transfer simp
-
-lemma bit_word_of_int_iff:
- \<open>bit (word_of_int k :: 'a::len word) n \<longleftrightarrow> n < LENGTH('a) \<and> bit k n\<close>
- by transfer simp
-
-lemma word_of_nat_AND_eq:
- \<open>word_of_nat (m AND n) = word_of_nat m AND word_of_nat n\<close>
- by (rule bit_eqI) (auto simp add: bit_word_of_nat_iff bit_and_iff)
+subsection \<open>Conversion from word\<close>
-lemma word_of_int_AND_eq:
- \<open>word_of_int (k AND l) = word_of_int k AND word_of_int l\<close>
- by (rule bit_eqI) (auto simp add: bit_word_of_int_iff bit_and_iff)
-
-lemma word_of_nat_OR_eq:
- \<open>word_of_nat (m OR n) = word_of_nat m OR word_of_nat n\<close>
- by (rule bit_eqI) (auto simp add: bit_word_of_nat_iff bit_or_iff)
-
-lemma word_of_int_OR_eq:
- \<open>word_of_int (k OR l) = word_of_int k OR word_of_int l\<close>
- by (rule bit_eqI) (auto simp add: bit_word_of_int_iff bit_or_iff)
-
-lemma word_of_nat_XOR_eq:
- \<open>word_of_nat (m XOR n) = word_of_nat m XOR word_of_nat n\<close>
- by (rule bit_eqI) (auto simp add: bit_word_of_nat_iff bit_xor_iff)
-
-lemma word_of_int_XOR_eq:
- \<open>word_of_int (k XOR l) = word_of_int k XOR word_of_int l\<close>
- by (rule bit_eqI) (auto simp add: bit_word_of_int_iff bit_xor_iff)
-
-
-subsection \<open>Conversion from words\<close>
+subsubsection \<open>Generic unsigned conversion\<close>
context semiring_1
begin
@@ -163,6 +93,114 @@
end
+context semiring_bits
+begin
+
+lemma bit_unsigned_iff:
+ \<open>bit (unsigned w) n \<longleftrightarrow> 2 ^ n \<noteq> 0 \<and> bit w n\<close>
+ for w :: \<open>'b::len word\<close>
+ by (transfer fixing: bit) (simp add: bit_of_nat_iff bit_nat_iff bit_take_bit_iff)
+
+end
+
+context semiring_bit_shifts
+begin
+
+lemma unsigned_push_bit_eq:
+ \<open>unsigned (push_bit n w) = take_bit LENGTH('b) (push_bit n (unsigned w))\<close>
+ for w :: \<open>'b::len word\<close>
+proof (rule bit_eqI)
+ fix m
+ assume \<open>2 ^ m \<noteq> 0\<close>
+ show \<open>bit (unsigned (push_bit n w)) m = bit (take_bit LENGTH('b) (push_bit n (unsigned w))) m\<close>
+ proof (cases \<open>n \<le> m\<close>)
+ case True
+ with \<open>2 ^ m \<noteq> 0\<close> have \<open>2 ^ (m - n) \<noteq> 0\<close>
+ by (metis (full_types) diff_add exp_add_not_zero_imp)
+ with True show ?thesis
+ by (simp add: bit_unsigned_iff bit_push_bit_iff Parity.bit_push_bit_iff bit_take_bit_iff ac_simps exp_eq_zero_iff not_le)
+ next
+ case False
+ then show ?thesis
+ by (simp add: not_le bit_unsigned_iff bit_push_bit_iff Parity.bit_push_bit_iff bit_take_bit_iff)
+ qed
+qed
+
+lemma unsigned_take_bit_eq:
+ \<open>unsigned (take_bit n w) = take_bit n (unsigned w)\<close>
+ for w :: \<open>'b::len word\<close>
+ by (rule bit_eqI) (simp add: bit_unsigned_iff bit_take_bit_iff Parity.bit_take_bit_iff)
+
+end
+
+context semiring_bit_operations
+begin
+
+lemma unsigned_and_eq:
+ \<open>unsigned (v AND w) = unsigned v AND unsigned w\<close>
+ for v w :: \<open>'b::len word\<close>
+ by (rule bit_eqI) (simp add: bit_unsigned_iff bit_and_iff Bit_Operations.bit_and_iff)
+
+lemma unsigned_or_eq:
+ \<open>unsigned (v OR w) = unsigned v OR unsigned w\<close>
+ for v w :: \<open>'b::len word\<close>
+ by (rule bit_eqI) (simp add: bit_unsigned_iff bit_or_iff Bit_Operations.bit_or_iff)
+
+lemma unsigned_xor_eq:
+ \<open>unsigned (v XOR w) = unsigned v XOR unsigned w\<close>
+ for v w :: \<open>'b::len word\<close>
+ by (rule bit_eqI) (simp add: bit_unsigned_iff bit_xor_iff Bit_Operations.bit_xor_iff)
+
+end
+
+context ring_bit_operations
+begin
+
+lemma unsigned_not_eq:
+ \<open>unsigned (NOT w) = take_bit LENGTH('b) (NOT (unsigned w))\<close>
+ for w :: \<open>'b::len word\<close>
+ by (rule bit_eqI)
+ (simp add: bit_unsigned_iff bit_take_bit_iff bit_not_iff Bit_Operations.bit_not_iff exp_eq_zero_iff not_le)
+
+end
+
+lemma unsigned_of_nat [simp]:
+ \<open>unsigned (word_of_nat n :: 'a::len word) = of_nat (take_bit LENGTH('a) n)\<close>
+ by transfer (simp add: nat_eq_iff take_bit_of_nat)
+
+lemma unsigned_of_int [simp]:
+ \<open>unsigned (word_of_int n :: 'a::len word) = of_int (take_bit LENGTH('a) n)\<close>
+ by transfer (simp add: nat_eq_iff take_bit_of_nat)
+
+context unique_euclidean_semiring_numeral
+begin
+
+lemma unsigned_greater_eq:
+ \<open>0 \<le> unsigned w\<close> for w :: \<open>'b::len word\<close>
+ by (transfer fixing: less_eq) simp
+
+lemma unsigned_less:
+ \<open>unsigned w < 2 ^ LENGTH('b)\<close> for w :: \<open>'b::len word\<close>
+ by (transfer fixing: less) (simp add: take_bit_int_less_exp)
+
+end
+
+context linordered_semidom
+begin
+
+lemma word_less_eq_iff_unsigned:
+ "a \<le> b \<longleftrightarrow> unsigned a \<le> unsigned b"
+ by (transfer fixing: less_eq) (simp add: nat_le_eq_zle)
+
+lemma word_less_iff_unsigned:
+ "a < b \<longleftrightarrow> unsigned a < unsigned b"
+ by (transfer fixing: less) (auto dest: preorder_class.le_less_trans [OF take_bit_nonnegative])
+
+end
+
+
+subsubsection \<open>Generic signed conversion\<close>
+
context ring_1
begin
@@ -198,6 +236,99 @@
end
+context ring_bit_operations
+begin
+
+lemma bit_signed_iff:
+ \<open>bit (signed w) n \<longleftrightarrow> 2 ^ n \<noteq> 0 \<and> bit w (min (LENGTH('b) - Suc 0) n)\<close>
+ for w :: \<open>'b::len word\<close>
+ by (transfer fixing: bit) (auto simp add: bit_of_int_iff bit_signed_take_bit_iff min_def)
+
+lemma signed_push_bit_eq:
+ \<open>signed (push_bit n w) = take_bit (LENGTH('b) - Suc 0) (push_bit n (signed w))
+ OR of_bool (n < LENGTH('b) \<and> bit w (LENGTH('b) - Suc n)) * NOT (mask (LENGTH('b) - Suc 0))\<close>
+ for w :: \<open>'b::len word\<close>
+proof (rule bit_eqI)
+ fix m
+ assume \<open>2 ^ m \<noteq> 0\<close>
+ define q where \<open>q = LENGTH('b) - Suc 0\<close>
+ then have *: \<open>LENGTH('b) = Suc q\<close>
+ by simp
+ show \<open>bit (signed (push_bit n w)) m \<longleftrightarrow>
+ bit (take_bit (LENGTH('b) - Suc 0) (push_bit n (signed w)) OR
+ of_bool (n < LENGTH('b) \<and> bit w (LENGTH('b) - Suc n)) * NOT (mask (LENGTH('b) - Suc 0))) m\<close>
+ proof (cases \<open>n \<le> m\<close>)
+ case True
+ with \<open>2 ^ m \<noteq> 0\<close> have \<open>2 ^ (m - n) \<noteq> 0\<close>
+ by (metis (full_types) diff_add exp_add_not_zero_imp)
+ with True show ?thesis
+ by (auto simp add: * bit_signed_iff bit_push_bit_iff Parity.bit_push_bit_iff bit_or_iff bit_take_bit_iff bit_not_iff bit_mask_iff exp_eq_zero_iff min_def)
+ next
+ case False
+ then show ?thesis
+ by (simp add: * bit_signed_iff bit_push_bit_iff Parity.bit_push_bit_iff bit_or_iff bit_take_bit_iff bit_not_iff bit_mask_iff)
+ qed
+qed
+
+lemma signed_take_bit_eq:
+ \<open>signed (take_bit n w) = (if n < LENGTH('b) then take_bit n (signed w) else signed w)\<close>
+ for w :: \<open>'b::len word\<close>
+ by (transfer fixing: take_bit; cases \<open>LENGTH('b)\<close>)
+ (auto simp add: signed_take_bit_take_bit take_bit_signed_take_bit take_bit_of_int min_def)
+
+lemma signed_not_eq:
+ \<open>signed (NOT w) = take_bit LENGTH('b) (NOT (signed w)) OR of_bool (bit (NOT (signed w)) LENGTH('b)) * NOT (mask LENGTH('b))\<close>
+ for w :: \<open>'b::len word\<close>
+proof (rule bit_eqI)
+ fix n
+ assume \<open>2 ^ n \<noteq> 0\<close>
+ show \<open>bit (signed (NOT w)) n \<longleftrightarrow>
+ bit (take_bit LENGTH('b) (NOT (signed w)) OR
+ of_bool (bit (NOT (signed w)) LENGTH('b)) * NOT (mask LENGTH('b))) n\<close>
+ proof (cases \<open>LENGTH('b) \<le> n\<close>)
+ case False
+ then show ?thesis
+ by (auto simp add: bit_signed_iff bit_not_iff bit_or_iff bit_take_bit_iff bit_mask_iff Bit_Operations.bit_not_iff exp_eq_zero_iff)
+ next
+ case True
+ moreover define q where \<open>q = n - LENGTH('b)\<close>
+ ultimately have \<open>n = LENGTH('b) + q\<close>
+ by simp
+ with \<open>2 ^ n \<noteq> 0\<close> have \<open>2 ^ q \<noteq> 0\<close> \<open>2 ^ LENGTH('b) \<noteq> 0\<close>
+ by (simp_all add: power_add) (use mult_not_zero in blast)+
+ then show ?thesis
+ by (simp add: bit_signed_iff bit_not_iff bit_or_iff bit_take_bit_iff bit_mask_iff Bit_Operations.bit_not_iff exp_eq_zero_iff min_def not_le not_less le_diff_conv le_Suc_eq)
+ qed
+qed
+
+lemma signed_and_eq:
+ \<open>signed (v AND w) = signed v AND signed w\<close>
+ for v w :: \<open>'b::len word\<close>
+ by (rule bit_eqI) (simp add: bit_signed_iff bit_and_iff Bit_Operations.bit_and_iff)
+
+lemma signed_or_eq:
+ \<open>signed (v OR w) = signed v OR signed w\<close>
+ for v w :: \<open>'b::len word\<close>
+ by (rule bit_eqI) (simp add: bit_signed_iff bit_or_iff Bit_Operations.bit_or_iff)
+
+lemma signed_xor_eq:
+ \<open>signed (v XOR w) = signed v XOR signed w\<close>
+ for v w :: \<open>'b::len word\<close>
+ by (rule bit_eqI) (simp add: bit_signed_iff bit_xor_iff Bit_Operations.bit_xor_iff)
+
+end
+
+lemma signed_of_nat [simp]:
+ \<open>signed (word_of_nat n :: 'a::len word) = of_int (signed_take_bit (LENGTH('a) - Suc 0) (int n))\<close>
+ by transfer simp
+
+lemma signed_of_int [simp]:
+ \<open>signed (word_of_int n :: 'a::len word) = of_int (signed_take_bit (LENGTH('a) - Suc 0) n)\<close>
+ by transfer simp
+
+
+subsubsection \<open>Important special cases\<close>
+
abbreviation unat :: \<open>'a::len word \<Rightarrow> nat\<close>
where \<open>unat \<equiv> unsigned\<close>
@@ -257,10 +388,6 @@
end
-lemma unsigned_of_nat [simp]:
- \<open>unsigned (of_nat n :: 'a::len word) = of_nat (take_bit LENGTH('a) n)\<close>
- by transfer (simp add: nat_eq_iff take_bit_of_nat)
-
lemma of_nat_unat [simp]:
\<open>of_nat (unat w) = unsigned w\<close>
by transfer simp
@@ -269,40 +396,66 @@
\<open>of_int (uint w) = unsigned w\<close>
by transfer simp
-context unique_euclidean_semiring_numeral
-begin
-
-lemma unsigned_greater_eq:
- \<open>0 \<le> unsigned w\<close> for w :: \<open>'b::len word\<close>
- by (transfer fixing: less_eq) simp
-
-lemma unsigned_less:
- \<open>unsigned w < 2 ^ LENGTH('b)\<close> for w :: \<open>'b::len word\<close>
- by (transfer fixing: less) (simp add: take_bit_int_less_exp)
-
-end
+lemma unat_div_distrib:
+ \<open>unat (v div w) = unat v div unat w\<close>
+proof transfer
+ fix k l
+ have \<open>nat (take_bit LENGTH('a) k) div nat (take_bit LENGTH('a) l) \<le> nat (take_bit LENGTH('a) k)\<close>
+ by (rule div_le_dividend)
+ also have \<open>nat (take_bit LENGTH('a) k) < 2 ^ LENGTH('a)\<close>
+ by (simp add: nat_less_iff take_bit_int_less_exp)
+ finally show \<open>(nat \<circ> take_bit LENGTH('a)) (take_bit LENGTH('a) k div take_bit LENGTH('a) l) =
+ (nat \<circ> take_bit LENGTH('a)) k div (nat \<circ> take_bit LENGTH('a)) l\<close>
+ by (simp add: nat_take_bit_eq div_int_pos_iff nat_div_distrib take_bit_eq_self)
+qed
-context linordered_semidom
-begin
-
-lemma word_less_eq_iff_unsigned:
- "a \<le> b \<longleftrightarrow> unsigned a \<le> unsigned b"
- by (transfer fixing: less_eq) (simp add: nat_le_eq_zle)
+lemma unat_mod_distrib:
+ \<open>unat (v mod w) = unat v mod unat w\<close>
+proof transfer
+ fix k l
+ have \<open>nat (take_bit LENGTH('a) k) mod nat (take_bit LENGTH('a) l) \<le> nat (take_bit LENGTH('a) k)\<close>
+ by (rule mod_less_eq_dividend)
+ also have \<open>nat (take_bit LENGTH('a) k) < 2 ^ LENGTH('a)\<close>
+ by (simp add: nat_less_iff take_bit_int_less_exp)
+ finally show \<open>(nat \<circ> take_bit LENGTH('a)) (take_bit LENGTH('a) k mod take_bit LENGTH('a) l) =
+ (nat \<circ> take_bit LENGTH('a)) k mod (nat \<circ> take_bit LENGTH('a)) l\<close>
+ by (simp add: nat_take_bit_eq mod_int_pos_iff less_le nat_mod_distrib take_bit_eq_self)
+qed
-lemma word_less_iff_unsigned:
- "a < b \<longleftrightarrow> unsigned a < unsigned b"
- by (transfer fixing: less) (auto dest: preorder_class.le_less_trans [OF take_bit_nonnegative])
+lemma uint_div_distrib:
+ \<open>uint (v div w) = uint v div uint w\<close>
+proof -
+ have \<open>int (unat (v div w)) = int (unat v div unat w)\<close>
+ by (simp add: unat_div_distrib)
+ then show ?thesis
+ by (simp add: of_nat_div)
+qed
-end
-
-lemma signed_of_int [simp]:
- \<open>signed (word_of_int k :: 'a::len word) = of_int (signed_take_bit (LENGTH('a) - 1) k)\<close>
- by transfer simp
+lemma uint_mod_distrib:
+ \<open>uint (v mod w) = uint v mod uint w\<close>
+proof -
+ have \<open>int (unat (v mod w)) = int (unat v mod unat w)\<close>
+ by (simp add: unat_mod_distrib)
+ then show ?thesis
+ by (simp add: of_nat_mod)
+qed
lemma of_int_sint [simp]:
\<open>of_int (sint a) = signed a\<close>
by transfer (simp_all add: take_bit_signed_take_bit)
+lemma sint_not_eq:
+ \<open>sint (NOT w) = signed_take_bit LENGTH('a) (NOT (sint w))\<close>
+ for w :: \<open>'a::len word\<close>
+ by (simp add: signed_not_eq signed_take_bit_unfold)
+
+lemma sint_push_bit_eq:
+ \<open>signed (push_bit n w) = signed_take_bit (LENGTH('a) - 1) (push_bit n (signed w))\<close>
+ for w :: \<open>'a::len word\<close>
+ by (transfer fixing: n; cases \<open>LENGTH('a)\<close>)
+ (auto simp add: signed_take_bit_def bit_concat_bit_iff bit_push_bit_iff bit_take_bit_iff bit_or_iff le_diff_conv2,
+ auto simp add: take_bit_push_bit not_less concat_bit_eq_iff take_bit_concat_bit_eq le_diff_conv2)
+
lemma sint_greater_eq:
\<open>- (2 ^ (LENGTH('a) - 1)) \<le> sint w\<close> for w :: \<open>'a::len word\<close>
proof (cases \<open>bit w (LENGTH('a) - 1)\<close>)
@@ -320,6 +473,6 @@
lemma sint_less:
\<open>sint w < 2 ^ (LENGTH('a) - 1)\<close> for w :: \<open>'a::len word\<close>
by (cases \<open>bit w (LENGTH('a) - 1)\<close>; transfer)
- (simp_all add: signed_take_bit_eq signed_take_bit_eq_or take_bit_int_less_exp not_eq_complement mask_eq_exp_minus_1 OR_upper)
+ (simp_all add: signed_take_bit_eq signed_take_bit_unfold take_bit_int_less_exp not_eq_complement mask_eq_exp_minus_1 OR_upper)
end
--- a/src/HOL/Word/Word.thy Sat Aug 29 16:30:33 2020 +0100
+++ b/src/HOL/Word/Word.thy Sun Aug 30 15:15:28 2020 +0000
@@ -931,9 +931,13 @@
\<open>uint (take_bit n w) = take_bit n (uint w)\<close>
by transfer (simp add: ac_simps)
+lemma take_bit_word_eq_self:
+ \<open>take_bit n w = w\<close> if \<open>LENGTH('a) \<le> n\<close> for w :: \<open>'a::len word\<close>
+ using that by transfer simp
+
lemma take_bit_length_eq [simp]:
\<open>take_bit LENGTH('a) w = w\<close> for w :: \<open>'a::len word\<close>
- by transfer simp
+ by (rule take_bit_word_eq_self) simp
lemma bit_word_of_int_iff:
\<open>bit (word_of_int k :: 'a::len word) n \<longleftrightarrow> n < LENGTH('a) \<and> bit k n\<close>
@@ -3865,7 +3869,7 @@
apply (auto simp add: signed_take_bit_eq_take_bit_minus take_bit_Suc_from_most n not_less intro!: *)
done
then show ?thesis
- apply (simp add: word_size shiftr_word_eq drop_bit_eq_zero_iff_not_bit_last bit_and_iff bit_xor_iff)
+ apply (simp only: One_nat_def word_size shiftr_word_eq drop_bit_eq_zero_iff_not_bit_last bit_and_iff bit_xor_iff)
apply (simp add: bit_last_iff)
done
qed