# HG changeset patch
# User haftmann
# Date 1587017369 -7200
# Node ID 3d1f72d25fc33855dbedc84c1c3cf6e9597f4c00
# Parent  318695613bb7010468b18ccd120509bbf9b1ff60
more complete rules on numerals

diff -r 318695613bb7 -r 3d1f72d25fc3 src/HOL/Divides.thy
--- a/src/HOL/Divides.thy	Thu Apr 16 08:09:28 2020 +0200
+++ b/src/HOL/Divides.thy	Thu Apr 16 08:09:29 2020 +0200
@@ -889,9 +889,7 @@
 text \<open>The division rewrite proper -- first, trivial results involving \<open>1\<close>\<close>
 
 lemma divmod_trivial [simp]:
-  "divmod Num.One Num.One = (numeral Num.One, 0)"
-  "divmod (Num.Bit0 m) Num.One = (numeral (Num.Bit0 m), 0)"
-  "divmod (Num.Bit1 m) Num.One = (numeral (Num.Bit1 m), 0)"
+  "divmod m Num.One = (numeral m, 0)"
   "divmod num.One (num.Bit0 n) = (0, Numeral1)"
   "divmod num.One (num.Bit1 n) = (0, Numeral1)"
   using divmod_divmod_step [of "Num.One"] by (simp_all add: divmod_def)
@@ -1128,6 +1126,10 @@
 
 end
 
+lemma divmod_BitM_2_eq [simp]:
+  \<open>divmod (Num.BitM m) (Num.Bit0 Num.One) = (numeral m - 1, (1 :: int))\<close>
+  by (cases m) simp_all
+
 lemma div_positive_int:
   "k div l > 0" if "k \<ge> l" and "l > 0" for k l :: int
   using that div_positive [of l k] by blast
diff -r 318695613bb7 -r 3d1f72d25fc3 src/HOL/Word/Bits_Int.thy
--- a/src/HOL/Word/Bits_Int.thy	Thu Apr 16 08:09:28 2020 +0200
+++ b/src/HOL/Word/Bits_Int.thy	Thu Apr 16 08:09:29 2020 +0200
@@ -102,7 +102,7 @@
   "bin_last (numeral (Num.Bit1 w))"
   "\<not> bin_last (- numeral (Num.Bit0 w))"
   "bin_last (- numeral (Num.Bit1 w))"
-  by (simp_all add: bin_last_def zmod_zminus1_eq_if) (auto simp add: divmod_def)
+  by (simp_all add: bin_last_def zmod_zminus1_eq_if)
 
 lemma bin_rest_numeral_simps [simp]:
   "bin_rest 0 = 0"
@@ -113,7 +113,7 @@
   "bin_rest (numeral (Num.Bit1 w)) = numeral w"
   "bin_rest (- numeral (Num.Bit0 w)) = - numeral w"
   "bin_rest (- numeral (Num.Bit1 w)) = - numeral (w + Num.One)"
-  by (simp_all add: bin_rest_def zdiv_zminus1_eq_if) (auto simp add: divmod_def)
+  by (simp_all add: bin_rest_def zdiv_zminus1_eq_if)
 
 lemma less_Bits: "v BIT b < w BIT c \<longleftrightarrow> v < w \<or> v \<le> w \<and> \<not> b \<and> c"
   by (auto simp: Bit_def)