# HG changeset patch
# User haftmann
# Date 1598800528 0
# Node ID 0f3d24dc197f144741b49d51719e3e5c7ad035c4
# Parent  5e26a4bca0c2d9f370c127213a159c6b87bd91d9
more on conversions

diff -r 5e26a4bca0c2 -r 0f3d24dc197f src/HOL/Library/Bit_Operations.thy
--- 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
diff -r 5e26a4bca0c2 -r 0f3d24dc197f src/HOL/Parity.thy
--- 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>
diff -r 5e26a4bca0c2 -r 0f3d24dc197f src/HOL/Word/Conversions.thy
--- 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
diff -r 5e26a4bca0c2 -r 0f3d24dc197f src/HOL/Word/Word.thy
--- 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