more thorough treatment of division, particularly signed division on int and word

--- a/NEWS	Wed Sep 23 08:52:41 2020 +0000
+++ b/NEWS	Wed Sep 23 11:14:38 2020 +0000
@@ -78,6 +78,9 @@
 
 * Library theory "Bit_Operations" with generic bit operations.
 
+* Library theory "Signed_Division" provides operations for signed
+division, instantiated for type int.
+
 * Session HOL-Word: Type word is restricted to bit strings consisting
 of at least one bit.  INCOMPATIBILITY.
 

--- a/src/HOL/Library/Bit_Operations.thy	Wed Sep 23 08:52:41 2020 +0000
+++ b/src/HOL/Library/Bit_Operations.thy	Wed Sep 23 11:14:38 2020 +0000
@@ -159,6 +159,10 @@
   by (rule bit_eqI)
     (auto simp add: bit_take_bit_iff bit_and_iff bit_mask_iff)
 
+lemma or_eq_0_iff:
+  \<open>a OR b = 0 \<longleftrightarrow> a = 0 \<and> b = 0\<close>
+	by (auto simp add: bit_eq_iff bit_or_iff)
+
 lemma disjunctive_add:
   \<open>a + b = a OR b\<close> if \<open>\<And>n. \<not> bit a n \<or> \<not> bit b n\<close>
   by (rule bit_eqI) (use that in \<open>simp add: bit_disjunctive_add_iff bit_or_iff\<close>)
@@ -249,6 +253,30 @@
   \<open>NOT (a - b) = NOT a + b\<close>
   using not_add_distrib [of a \<open>- b\<close>] by simp
 
+lemma (in ring_bit_operations) and_eq_minus_1_iff:
+  \<open>a AND b = - 1 \<longleftrightarrow> a = - 1 \<and> b = - 1\<close>
+proof
+  assume \<open>a = - 1 \<and> b = - 1\<close>
+  then show \<open>a AND b = - 1\<close>
+	by simp
+next
+  assume \<open>a AND b = - 1\<close>
+  have *: \<open>bit a n\<close> \<open>bit b n\<close> if \<open>2 ^ n \<noteq> 0\<close> for n
+  proof -
+    from \<open>a AND b = - 1\<close>
+    have \<open>bit (a AND b) n = bit (- 1) n\<close>
+      by (simp add: bit_eq_iff)
+    then show \<open>bit a n\<close> \<open>bit b n\<close>
+	    using that by (simp_all add: bit_and_iff)
+  qed
+  have \<open>a = - 1\<close>
+    by (rule bit_eqI) (simp add: *)
+  moreover have \<open>b = - 1\<close>
+    by (rule bit_eqI) (simp add: *)
+  ultimately show \<open>a = - 1 \<and> b = - 1\<close>
+    by simp
+qed
+
 lemma disjunctive_diff:
   \<open>a - b = a AND NOT b\<close> if \<open>\<And>n. bit b n \<Longrightarrow> bit a n\<close>
 proof -

--- a/src/HOL/Library/Library.thy	Wed Sep 23 08:52:41 2020 +0000
+++ b/src/HOL/Library/Library.thy	Wed Sep 23 11:14:38 2020 +0000
@@ -86,6 +86,7 @@
   Saturated
   Set_Algebras
   Set_Idioms
+  Signed_Division
   State_Monad
   Stirling
   Stream

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/Signed_Division.thy	Wed Sep 23 11:14:38 2020 +0000
@@ -0,0 +1,27 @@
+(*  Author:  Stefan Berghofer et al.
+*)
+
+subsection \<open>Signed division: negative results rounded towards zero rather than minus infinity.\<close>
+
+theory Signed_Division
+  imports Main
+begin
+
+class signed_division =
+  fixes signed_divide :: \<open>'a \<Rightarrow> 'a \<Rightarrow> 'a\<close> (infixl "sdiv" 70)
+  and signed_modulo :: \<open>'a \<Rightarrow> 'a \<Rightarrow> 'a\<close> (infixl "smod" 70)
+
+instantiation int :: signed_division
+begin
+
+definition signed_divide_int :: \<open>int \<Rightarrow> int \<Rightarrow> int\<close>
+  where \<open>k sdiv l = sgn k * sgn l * (\<bar>k\<bar> div \<bar>l\<bar>)\<close> for k l :: int
+
+definition signed_modulo_int :: \<open>int \<Rightarrow> int \<Rightarrow> int\<close>
+  where \<open>k smod l = k - (k sdiv l) * l\<close> for k l :: int
+
+instance ..
+
+end
+
+end

--- a/src/HOL/Library/Type_Length.thy	Wed Sep 23 08:52:41 2020 +0000
+++ b/src/HOL/Library/Type_Length.thy	Wed Sep 23 11:14:38 2020 +0000
@@ -117,4 +117,12 @@
 
 end
 
+lemma less_eq_decr_length_iff [simp]:
+  \<open>n \<le> LENGTH('a::len) - Suc 0 \<longleftrightarrow> n < LENGTH('a)\<close>
+  by (cases \<open>LENGTH('a)\<close>) (simp_all add: less_Suc_eq le_less)
+
+lemma decr_length_less_iff [simp]:
+  \<open>LENGTH('a::len) - Suc 0 < n \<longleftrightarrow> LENGTH('a) \<le> n\<close>
+  by (cases \<open>LENGTH('a)\<close>) auto
+
 end

--- a/src/HOL/Parity.thy	Wed Sep 23 08:52:41 2020 +0000
+++ b/src/HOL/Parity.thy	Wed Sep 23 11:14:38 2020 +0000
@@ -1193,6 +1193,10 @@
 context semiring_bits
 begin
 
+lemma bit_of_bool_iff:
+  \<open>bit (of_bool b) n \<longleftrightarrow> b \<and> n = 0\<close>
+	by (simp add: bit_1_iff)
+
 lemma even_of_nat_iff:
   \<open>even (of_nat n) \<longleftrightarrow> even n\<close>
   by (induction n rule: nat_bit_induct) simp_all

--- a/src/HOL/Word/Word.thy	Wed Sep 23 08:52:41 2020 +0000
+++ b/src/HOL/Word/Word.thy	Wed Sep 23 11:14:38 2020 +0000
@@ -75,7 +75,6 @@
     transfer_rule_numeral [transfer_rule]
     transfer_rule_of_nat [transfer_rule]
     transfer_rule_of_int [transfer_rule]
-
 begin
 
 lemma power_transfer_word [transfer_rule]:
@@ -275,6 +274,10 @@
   \<open>v = w \<longleftrightarrow> unsigned v = unsigned w\<close>
   by (auto intro: unsigned_word_eqI)
 
+lemma (in semiring_char_0) unsigned_eq_0_iff:
+  \<open>unsigned w = 0 \<longleftrightarrow> w = 0\<close>
+  using word_eq_iff_unsigned [of w 0] by simp
+
 end
 
 context ring_1
@@ -326,6 +329,10 @@
   \<open>v = w \<longleftrightarrow> signed v = signed w\<close>
   by (auto intro: signed_word_eqI)
 
+lemma signed_eq_0_iff:
+  \<open>signed w = 0 \<longleftrightarrow> w = 0\<close>
+  using word_eq_iff_signed [of w 0] by simp
+
 end
 
 abbreviation unat :: \<open>'a::len word \<Rightarrow> nat\<close>
@@ -403,6 +410,10 @@
   \<open>nat (uint w) = unat w\<close>
   by transfer simp
 
+lemma sgn_uint_eq [simp]:
+  \<open>sgn (uint w) = of_bool (w \<noteq> 0)\<close>
+  by transfer (simp add: less_le)
+
 text \<open>Aliasses only for code generation\<close>
 
 context
@@ -2930,7 +2941,7 @@
 lemma udvd_imp_dvd:
   \<open>v dvd w\<close> if \<open>v udvd w\<close> for v w :: \<open>'a::len word\<close>
 proof -
-  from that obtain u :: \<open>'a word\<close> where w: \<open>unat w = unat v * unat u\<close> ..
+  from that obtain u :: \<open>'a word\<close> where \<open>unat w = unat v * unat u\<close> ..
   then have \<open>(word_of_nat (unat w) :: 'a word) = word_of_nat (unat v * unat u)\<close>
     by simp
   then have \<open>w = v * u\<close>
@@ -2938,6 +2949,20 @@
   then show \<open>v dvd w\<close> ..
 qed
 
+lemma exp_dvd_iff_exp_udvd:
+  \<open>2 ^ n dvd w \<longleftrightarrow> 2 ^ n udvd w\<close> for v w :: \<open>'a::len word\<close>
+proof
+  assume \<open>2 ^ n udvd w\<close> then show \<open>2 ^ n dvd w\<close>
+    by (rule udvd_imp_dvd) 
+next
+  assume \<open>2 ^ n dvd w\<close>
+  then obtain u :: \<open>'a word\<close> where \<open>w = 2 ^ n * u\<close> ..
+  then have \<open>w = push_bit n u\<close>
+    by (simp add: push_bit_eq_mult)
+  then show \<open>2 ^ n udvd w\<close>
+    by transfer (simp add: take_bit_push_bit dvd_eq_mod_eq_0 flip: take_bit_eq_mod)
+qed
+
 lemma udvd_nat_alt:
   \<open>a udvd b \<longleftrightarrow> (\<exists>n. unat b = n * unat a)\<close>
   by (auto simp add: udvd_iff_dvd)