--- 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
--- 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)