src/HOL/Divides.thy
 author blanchet Tue Nov 07 15:16:42 2017 +0100 (19 months ago) changeset 67022 49309fe530fd parent 66886 960509bfd47e child 67083 6b2c0681ef28 permissions -rw-r--r--
more robust parsing for THF proofs (esp. polymorphic Leo-III proofs)
1 (*  Title:      HOL/Divides.thy
2     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
3     Copyright   1999  University of Cambridge
4 *)
6 section \<open>More on quotient and remainder\<close>
8 theory Divides
9 imports Parity
10 begin
12 subsection \<open>Numeral division with a pragmatic type class\<close>
14 text \<open>
15   The following type class contains everything necessary to formulate
16   a division algorithm in ring structures with numerals, restricted
17   to its positive segments.  This is its primary motivation, and it
18   could surely be formulated using a more fine-grained, more algebraic
19   and less technical class hierarchy.
20 \<close>
22 class unique_euclidean_semiring_numeral = semiring_parity + linordered_semidom +
23   assumes div_less: "0 \<le> a \<Longrightarrow> a < b \<Longrightarrow> a div b = 0"
24     and mod_less: " 0 \<le> a \<Longrightarrow> a < b \<Longrightarrow> a mod b = a"
25     and div_positive: "0 < b \<Longrightarrow> b \<le> a \<Longrightarrow> a div b > 0"
26     and mod_less_eq_dividend: "0 \<le> a \<Longrightarrow> a mod b \<le> a"
27     and pos_mod_bound: "0 < b \<Longrightarrow> a mod b < b"
28     and pos_mod_sign: "0 < b \<Longrightarrow> 0 \<le> a mod b"
29     and mod_mult2_eq: "0 \<le> c \<Longrightarrow> a mod (b * c) = b * (a div b mod c) + a mod b"
30     and div_mult2_eq: "0 \<le> c \<Longrightarrow> a div (b * c) = a div b div c"
31   assumes discrete: "a < b \<longleftrightarrow> a + 1 \<le> b"
32   fixes divmod :: "num \<Rightarrow> num \<Rightarrow> 'a \<times> 'a"
33     and divmod_step :: "num \<Rightarrow> 'a \<times> 'a \<Rightarrow> 'a \<times> 'a"
34   assumes divmod_def: "divmod m n = (numeral m div numeral n, numeral m mod numeral n)"
35     and divmod_step_def: "divmod_step l qr = (let (q, r) = qr
36     in if r \<ge> numeral l then (2 * q + 1, r - numeral l)
37     else (2 * q, r))"
38     \<comment> \<open>These are conceptually definitions but force generated code
39     to be monomorphic wrt. particular instances of this class which
40     yields a significant speedup.\<close>
41 begin
43 lemma divmod_digit_1:
44   assumes "0 \<le> a" "0 < b" and "b \<le> a mod (2 * b)"
45   shows "2 * (a div (2 * b)) + 1 = a div b" (is "?P")
46     and "a mod (2 * b) - b = a mod b" (is "?Q")
47 proof -
48   from assms mod_less_eq_dividend [of a "2 * b"] have "b \<le> a"
49     by (auto intro: trans)
50   with \<open>0 < b\<close> have "0 < a div b" by (auto intro: div_positive)
51   then have [simp]: "1 \<le> a div b" by (simp add: discrete)
52   with \<open>0 < b\<close> have mod_less: "a mod b < b" by (simp add: pos_mod_bound)
53   define w where "w = a div b mod 2"
54   then have w_exhaust: "w = 0 \<or> w = 1" by auto
55   have mod_w: "a mod (2 * b) = a mod b + b * w"
56     by (simp add: w_def mod_mult2_eq ac_simps)
57   from assms w_exhaust have "w = 1"
58     by (auto simp add: mod_w) (insert mod_less, auto)
59   with mod_w have mod: "a mod (2 * b) = a mod b + b" by simp
60   have "2 * (a div (2 * b)) = a div b - w"
61     by (simp add: w_def div_mult2_eq minus_mod_eq_mult_div ac_simps)
62   with \<open>w = 1\<close> have div: "2 * (a div (2 * b)) = a div b - 1" by simp
63   then show ?P and ?Q
65 qed
67 lemma divmod_digit_0:
68   assumes "0 < b" and "a mod (2 * b) < b"
69   shows "2 * (a div (2 * b)) = a div b" (is "?P")
70     and "a mod (2 * b) = a mod b" (is "?Q")
71 proof -
72   define w where "w = a div b mod 2"
73   then have w_exhaust: "w = 0 \<or> w = 1" by auto
74   have mod_w: "a mod (2 * b) = a mod b + b * w"
75     by (simp add: w_def mod_mult2_eq ac_simps)
76   moreover have "b \<le> a mod b + b"
77   proof -
78     from \<open>0 < b\<close> pos_mod_sign have "0 \<le> a mod b" by blast
79     then have "0 + b \<le> a mod b + b" by (rule add_right_mono)
80     then show ?thesis by simp
81   qed
82   moreover note assms w_exhaust
83   ultimately have "w = 0" by auto
84   with mod_w have mod: "a mod (2 * b) = a mod b" by simp
85   have "2 * (a div (2 * b)) = a div b - w"
86     by (simp add: w_def div_mult2_eq minus_mod_eq_mult_div ac_simps)
87   with \<open>w = 0\<close> have div: "2 * (a div (2 * b)) = a div b" by simp
88   then show ?P and ?Q
89     by (simp_all add: div mod)
90 qed
92 lemma fst_divmod:
93   "fst (divmod m n) = numeral m div numeral n"
96 lemma snd_divmod:
97   "snd (divmod m n) = numeral m mod numeral n"
100 text \<open>
101   This is a formulation of one step (referring to one digit position)
102   in school-method division: compare the dividend at the current
103   digit position with the remainder from previous division steps
104   and evaluate accordingly.
105 \<close>
107 lemma divmod_step_eq [simp]:
108   "divmod_step l (q, r) = (if numeral l \<le> r
109     then (2 * q + 1, r - numeral l) else (2 * q, r))"
112 text \<open>
113   This is a formulation of school-method division.
114   If the divisor is smaller than the dividend, terminate.
115   If not, shift the dividend to the right until termination
116   occurs and then reiterate single division steps in the
117   opposite direction.
118 \<close>
120 lemma divmod_divmod_step:
121   "divmod m n = (if m < n then (0, numeral m)
122     else divmod_step n (divmod m (Num.Bit0 n)))"
123 proof (cases "m < n")
124   case True then have "numeral m < numeral n" by simp
125   then show ?thesis
126     by (simp add: prod_eq_iff div_less mod_less fst_divmod snd_divmod)
127 next
128   case False
129   have "divmod m n =
130     divmod_step n (numeral m div (2 * numeral n),
131       numeral m mod (2 * numeral n))"
132   proof (cases "numeral n \<le> numeral m mod (2 * numeral n)")
133     case True
134     with divmod_step_eq
135       have "divmod_step n (numeral m div (2 * numeral n), numeral m mod (2 * numeral n)) =
136         (2 * (numeral m div (2 * numeral n)) + 1, numeral m mod (2 * numeral n) - numeral n)"
137         by simp
138     moreover from True divmod_digit_1 [of "numeral m" "numeral n"]
139       have "2 * (numeral m div (2 * numeral n)) + 1 = numeral m div numeral n"
140       and "numeral m mod (2 * numeral n) - numeral n = numeral m mod numeral n"
141       by simp_all
142     ultimately show ?thesis by (simp only: divmod_def)
143   next
144     case False then have *: "numeral m mod (2 * numeral n) < numeral n"
146     with divmod_step_eq
147       have "divmod_step n (numeral m div (2 * numeral n), numeral m mod (2 * numeral n)) =
148         (2 * (numeral m div (2 * numeral n)), numeral m mod (2 * numeral n))"
149         by auto
150     moreover from * divmod_digit_0 [of "numeral n" "numeral m"]
151       have "2 * (numeral m div (2 * numeral n)) = numeral m div numeral n"
152       and "numeral m mod (2 * numeral n) = numeral m mod numeral n"
153       by (simp_all only: zero_less_numeral)
154     ultimately show ?thesis by (simp only: divmod_def)
155   qed
156   then have "divmod m n =
157     divmod_step n (numeral m div numeral (Num.Bit0 n),
158       numeral m mod numeral (Num.Bit0 n))"
159     by (simp only: numeral.simps distrib mult_1)
160   then have "divmod m n = divmod_step n (divmod m (Num.Bit0 n))"
162   with False show ?thesis by simp
163 qed
165 text \<open>The division rewrite proper -- first, trivial results involving \<open>1\<close>\<close>
167 lemma divmod_trivial [simp]:
168   "divmod Num.One Num.One = (numeral Num.One, 0)"
169   "divmod (Num.Bit0 m) Num.One = (numeral (Num.Bit0 m), 0)"
170   "divmod (Num.Bit1 m) Num.One = (numeral (Num.Bit1 m), 0)"
171   "divmod num.One (num.Bit0 n) = (0, Numeral1)"
172   "divmod num.One (num.Bit1 n) = (0, Numeral1)"
173   using divmod_divmod_step [of "Num.One"] by (simp_all add: divmod_def)
175 text \<open>Division by an even number is a right-shift\<close>
177 lemma divmod_cancel [simp]:
178   "divmod (Num.Bit0 m) (Num.Bit0 n) = (case divmod m n of (q, r) \<Rightarrow> (q, 2 * r))" (is ?P)
179   "divmod (Num.Bit1 m) (Num.Bit0 n) = (case divmod m n of (q, r) \<Rightarrow> (q, 2 * r + 1))" (is ?Q)
180 proof -
181   have *: "\<And>q. numeral (Num.Bit0 q) = 2 * numeral q"
182     "\<And>q. numeral (Num.Bit1 q) = 2 * numeral q + 1"
183     by (simp_all only: numeral_mult numeral.simps distrib) simp_all
184   have "1 div 2 = 0" "1 mod 2 = 1" by (auto intro: div_less mod_less)
185   then show ?P and ?Q
186     by (simp_all add: fst_divmod snd_divmod prod_eq_iff split_def * [of m] * [of n] mod_mult_mult1
187       div_mult2_eq [of _ _ 2] mod_mult2_eq [of _ _ 2]
189 qed
191 text \<open>The really hard work\<close>
193 lemma divmod_steps [simp]:
194   "divmod (num.Bit0 m) (num.Bit1 n) =
195       (if m \<le> n then (0, numeral (num.Bit0 m))
196        else divmod_step (num.Bit1 n)
197              (divmod (num.Bit0 m)
198                (num.Bit0 (num.Bit1 n))))"
199   "divmod (num.Bit1 m) (num.Bit1 n) =
200       (if m < n then (0, numeral (num.Bit1 m))
201        else divmod_step (num.Bit1 n)
202              (divmod (num.Bit1 m)
203                (num.Bit0 (num.Bit1 n))))"
206 lemmas divmod_algorithm_code = divmod_step_eq divmod_trivial divmod_cancel divmod_steps
208 text \<open>Special case: divisibility\<close>
210 definition divides_aux :: "'a \<times> 'a \<Rightarrow> bool"
211 where
212   "divides_aux qr \<longleftrightarrow> snd qr = 0"
214 lemma divides_aux_eq [simp]:
215   "divides_aux (q, r) \<longleftrightarrow> r = 0"
218 lemma dvd_numeral_simp [simp]:
219   "numeral m dvd numeral n \<longleftrightarrow> divides_aux (divmod n m)"
220   by (simp add: divmod_def mod_eq_0_iff_dvd)
222 text \<open>Generic computation of quotient and remainder\<close>
224 lemma numeral_div_numeral [simp]:
225   "numeral k div numeral l = fst (divmod k l)"
228 lemma numeral_mod_numeral [simp]:
229   "numeral k mod numeral l = snd (divmod k l)"
232 lemma one_div_numeral [simp]:
233   "1 div numeral n = fst (divmod num.One n)"
236 lemma one_mod_numeral [simp]:
237   "1 mod numeral n = snd (divmod num.One n)"
240 text \<open>Computing congruences modulo \<open>2 ^ q\<close>\<close>
242 lemma cong_exp_iff_simps:
243   "numeral n mod numeral Num.One = 0
244     \<longleftrightarrow> True"
245   "numeral (Num.Bit0 n) mod numeral (Num.Bit0 q) = 0
246     \<longleftrightarrow> numeral n mod numeral q = 0"
247   "numeral (Num.Bit1 n) mod numeral (Num.Bit0 q) = 0
248     \<longleftrightarrow> False"
249   "numeral m mod numeral Num.One = (numeral n mod numeral Num.One)
250     \<longleftrightarrow> True"
251   "numeral Num.One mod numeral (Num.Bit0 q) = (numeral Num.One mod numeral (Num.Bit0 q))
252     \<longleftrightarrow> True"
253   "numeral Num.One mod numeral (Num.Bit0 q) = (numeral (Num.Bit0 n) mod numeral (Num.Bit0 q))
254     \<longleftrightarrow> False"
255   "numeral Num.One mod numeral (Num.Bit0 q) = (numeral (Num.Bit1 n) mod numeral (Num.Bit0 q))
256     \<longleftrightarrow> (numeral n mod numeral q) = 0"
257   "numeral (Num.Bit0 m) mod numeral (Num.Bit0 q) = (numeral Num.One mod numeral (Num.Bit0 q))
258     \<longleftrightarrow> False"
259   "numeral (Num.Bit0 m) mod numeral (Num.Bit0 q) = (numeral (Num.Bit0 n) mod numeral (Num.Bit0 q))
260     \<longleftrightarrow> numeral m mod numeral q = (numeral n mod numeral q)"
261   "numeral (Num.Bit0 m) mod numeral (Num.Bit0 q) = (numeral (Num.Bit1 n) mod numeral (Num.Bit0 q))
262     \<longleftrightarrow> False"
263   "numeral (Num.Bit1 m) mod numeral (Num.Bit0 q) = (numeral Num.One mod numeral (Num.Bit0 q))
264     \<longleftrightarrow> (numeral m mod numeral q) = 0"
265   "numeral (Num.Bit1 m) mod numeral (Num.Bit0 q) = (numeral (Num.Bit0 n) mod numeral (Num.Bit0 q))
266     \<longleftrightarrow> False"
267   "numeral (Num.Bit1 m) mod numeral (Num.Bit0 q) = (numeral (Num.Bit1 n) mod numeral (Num.Bit0 q))
268     \<longleftrightarrow> numeral m mod numeral q = (numeral n mod numeral q)"
269   by (auto simp add: case_prod_beta dest: arg_cong [of _ _ even])
271 end
273 hide_fact (open) div_less mod_less mod_less_eq_dividend mod_mult2_eq div_mult2_eq
276 subsection \<open>More on division\<close>
278 instantiation nat :: unique_euclidean_semiring_numeral
279 begin
281 definition divmod_nat :: "num \<Rightarrow> num \<Rightarrow> nat \<times> nat"
282 where
283   divmod'_nat_def: "divmod_nat m n = (numeral m div numeral n, numeral m mod numeral n)"
285 definition divmod_step_nat :: "num \<Rightarrow> nat \<times> nat \<Rightarrow> nat \<times> nat"
286 where
287   "divmod_step_nat l qr = (let (q, r) = qr
288     in if r \<ge> numeral l then (2 * q + 1, r - numeral l)
289     else (2 * q, r))"
291 instance by standard
292   (auto simp add: divmod'_nat_def divmod_step_nat_def div_greater_zero_iff div_mult2_eq mod_mult2_eq)
294 end
296 declare divmod_algorithm_code [where ?'a = nat, code]
298 lemma Suc_0_div_numeral [simp]:
299   fixes k l :: num
300   shows "Suc 0 div numeral k = fst (divmod Num.One k)"
303 lemma Suc_0_mod_numeral [simp]:
304   fixes k l :: num
305   shows "Suc 0 mod numeral k = snd (divmod Num.One k)"
308 definition divmod_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat \<times> nat"
309   where "divmod_nat m n = (m div n, m mod n)"
311 lemma fst_divmod_nat [simp]:
312   "fst (divmod_nat m n) = m div n"
315 lemma snd_divmod_nat [simp]:
316   "snd (divmod_nat m n) = m mod n"
319 lemma divmod_nat_if [code]:
320   "Divides.divmod_nat m n = (if n = 0 \<or> m < n then (0, m) else
321     let (q, r) = Divides.divmod_nat (m - n) n in (Suc q, r))"
322   by (simp add: prod_eq_iff case_prod_beta not_less le_div_geq le_mod_geq)
324 lemma [code]:
325   "m div n = fst (divmod_nat m n)"
326   "m mod n = snd (divmod_nat m n)"
327   by simp_all
329 inductive eucl_rel_int :: "int \<Rightarrow> int \<Rightarrow> int \<times> int \<Rightarrow> bool"
330   where eucl_rel_int_by0: "eucl_rel_int k 0 (0, k)"
331   | eucl_rel_int_dividesI: "l \<noteq> 0 \<Longrightarrow> k = q * l \<Longrightarrow> eucl_rel_int k l (q, 0)"
332   | eucl_rel_int_remainderI: "sgn r = sgn l \<Longrightarrow> \<bar>r\<bar> < \<bar>l\<bar>
333       \<Longrightarrow> k = q * l + r \<Longrightarrow> eucl_rel_int k l (q, r)"
335 lemma eucl_rel_int_iff:
336   "eucl_rel_int k l (q, r) \<longleftrightarrow>
337     k = l * q + r \<and>
338      (if 0 < l then 0 \<le> r \<and> r < l else if l < 0 then l < r \<and> r \<le> 0 else q = 0)"
339   by (cases "r = 0")
340     (auto elim!: eucl_rel_int.cases intro: eucl_rel_int_by0 eucl_rel_int_dividesI eucl_rel_int_remainderI
341     simp add: ac_simps sgn_1_pos sgn_1_neg)
343 lemma unique_quotient_lemma:
344   "b * q' + r' \<le> b * q + r \<Longrightarrow> 0 \<le> r' \<Longrightarrow> r' < b \<Longrightarrow> r < b \<Longrightarrow> q' \<le> (q::int)"
345 apply (subgoal_tac "r' + b * (q'-q) \<le> r")
346  prefer 2 apply (simp add: right_diff_distrib)
347 apply (subgoal_tac "0 < b * (1 + q - q') ")
348 apply (erule_tac [2] order_le_less_trans)
349  prefer 2 apply (simp add: right_diff_distrib distrib_left)
350 apply (subgoal_tac "b * q' < b * (1 + q) ")
351  prefer 2 apply (simp add: right_diff_distrib distrib_left)
353 done
355 lemma unique_quotient_lemma_neg:
356   "b * q' + r' \<le> b*q + r \<Longrightarrow> r \<le> 0 \<Longrightarrow> b < r \<Longrightarrow> b < r' \<Longrightarrow> q \<le> (q'::int)"
357   by (rule_tac b = "-b" and r = "-r'" and r' = "-r" in unique_quotient_lemma) auto
359 lemma unique_quotient:
360   "eucl_rel_int a b (q, r) \<Longrightarrow> eucl_rel_int a b (q', r') \<Longrightarrow> q = q'"
361   apply (simp add: eucl_rel_int_iff linorder_neq_iff split: if_split_asm)
362   apply (blast intro: order_antisym
363     dest: order_eq_refl [THEN unique_quotient_lemma]
364     order_eq_refl [THEN unique_quotient_lemma_neg] sym)+
365   done
367 lemma unique_remainder:
368   "eucl_rel_int a b (q, r) \<Longrightarrow> eucl_rel_int a b (q', r') \<Longrightarrow> r = r'"
369 apply (subgoal_tac "q = q'")
371 apply (blast intro: unique_quotient)
372 done
374 lemma eucl_rel_int:
375   "eucl_rel_int k l (k div l, k mod l)"
376 proof (cases k rule: int_cases3)
377   case zero
378   then show ?thesis
379     by (simp add: eucl_rel_int_iff divide_int_def modulo_int_def)
380 next
381   case (pos n)
382   then show ?thesis
383     using div_mult_mod_eq [of n]
384     by (cases l rule: int_cases3)
385       (auto simp del: of_nat_mult of_nat_add
387         eucl_rel_int_iff divide_int_def modulo_int_def int_dvd_iff)
388 next
389   case (neg n)
390   then show ?thesis
391     using div_mult_mod_eq [of n]
392     by (cases l rule: int_cases3)
393       (auto simp del: of_nat_mult of_nat_add
395         eucl_rel_int_iff divide_int_def modulo_int_def int_dvd_iff)
396 qed
398 lemma divmod_int_unique:
399   assumes "eucl_rel_int k l (q, r)"
400   shows div_int_unique: "k div l = q" and mod_int_unique: "k mod l = r"
401   using assms eucl_rel_int [of k l]
402   using unique_quotient [of k l] unique_remainder [of k l]
403   by auto
405 lemma div_abs_eq_div_nat:
406   "\<bar>k\<bar> div \<bar>l\<bar> = int (nat \<bar>k\<bar> div nat \<bar>l\<bar>)"
409 lemma mod_abs_eq_div_nat:
410   "\<bar>k\<bar> mod \<bar>l\<bar> = int (nat \<bar>k\<bar> mod nat \<bar>l\<bar>)"
413 lemma zdiv_int:
414   "int (a div b) = int a div int b"
415   by (simp add: divide_int_def sgn_1_pos)
417 lemma zmod_int:
418   "int (a mod b) = int a mod int b"
419   by (simp add: modulo_int_def sgn_1_pos)
421 lemma div_sgn_abs_cancel:
422   fixes k l v :: int
423   assumes "v \<noteq> 0"
424   shows "(sgn v * \<bar>k\<bar>) div (sgn v * \<bar>l\<bar>) = \<bar>k\<bar> div \<bar>l\<bar>"
425 proof -
426   from assms have "sgn v = - 1 \<or> sgn v = 1"
427     by (cases "v \<ge> 0") auto
428   then show ?thesis
429     using assms unfolding divide_int_def [of "sgn v * \<bar>k\<bar>" "sgn v * \<bar>l\<bar>"]
430     by (fastforce simp add: not_less div_abs_eq_div_nat)
431 qed
433 lemma div_eq_sgn_abs:
434   fixes k l v :: int
435   assumes "sgn k = sgn l"
436   shows "k div l = \<bar>k\<bar> div \<bar>l\<bar>"
437 proof (cases "l = 0")
438   case True
439   then show ?thesis
440     by simp
441 next
442   case False
443   with assms have "(sgn k * \<bar>k\<bar>) div (sgn l * \<bar>l\<bar>) = \<bar>k\<bar> div \<bar>l\<bar>"
444     using div_sgn_abs_cancel [of l k l] by simp
445   then show ?thesis
447 qed
449 lemma div_dvd_sgn_abs:
450   fixes k l :: int
451   assumes "l dvd k"
452   shows "k div l = (sgn k * sgn l) * (\<bar>k\<bar> div \<bar>l\<bar>)"
453 proof (cases "k = 0 \<or> l = 0")
454   case True
455   then show ?thesis
456     by auto
457 next
458   case False
459   then have "k \<noteq> 0" and "l \<noteq> 0"
460     by auto
461   show ?thesis
462   proof (cases "sgn l = sgn k")
463     case True
464     then show ?thesis
466   next
467     case False
468     with \<open>k \<noteq> 0\<close> \<open>l \<noteq> 0\<close>
469     have "sgn l * sgn k = - 1"
470       by (simp add: sgn_if split: if_splits)
471     with assms show ?thesis
472       unfolding divide_int_def [of k l]
473       by (auto simp add: zdiv_int ac_simps)
474   qed
475 qed
477 lemma div_noneq_sgn_abs:
478   fixes k l :: int
479   assumes "l \<noteq> 0"
480   assumes "sgn k \<noteq> sgn l"
481   shows "k div l = - (\<bar>k\<bar> div \<bar>l\<bar>) - of_bool (\<not> l dvd k)"
482   using assms
483   by (simp only: divide_int_def [of k l], auto simp add: not_less zdiv_int)
485 text\<open>Basic laws about division and remainder\<close>
487 lemma pos_mod_conj: "(0::int) < b \<Longrightarrow> 0 \<le> a mod b \<and> a mod b < b"
488   using eucl_rel_int [of a b]
489   by (auto simp add: eucl_rel_int_iff prod_eq_iff)
491 lemmas pos_mod_sign = pos_mod_conj [THEN conjunct1]
492    and pos_mod_bound = pos_mod_conj [THEN conjunct2]
494 lemma neg_mod_conj: "b < (0::int) \<Longrightarrow> a mod b \<le> 0 \<and> b < a mod b"
495   using eucl_rel_int [of a b]
496   by (auto simp add: eucl_rel_int_iff prod_eq_iff)
498 lemmas neg_mod_sign [simp] = neg_mod_conj [THEN conjunct1]
499    and neg_mod_bound [simp] = neg_mod_conj [THEN conjunct2]
502 subsubsection \<open>General Properties of div and mod\<close>
504 lemma div_pos_pos_trivial [simp]:
505   "k div l = 0" if "k \<ge> 0" and "k < l" for k l :: int
506   using that by (auto intro!: div_int_unique [of _ _ _ k] simp add: eucl_rel_int_iff)
508 lemma div_neg_neg_trivial [simp]:
509   "k div l = 0" if "k \<le> 0" and "l < k" for k l :: int
510   using that by (auto intro!: div_int_unique [of _ _ _ k] simp add: eucl_rel_int_iff)
512 lemma div_pos_neg_trivial: "[| (0::int) < a;  a+b \<le> 0 |] ==> a div b = -1"
513 apply (rule div_int_unique)
514 apply (auto simp add: eucl_rel_int_iff)
515 done
517 lemma div_positive_int:
518   "k div l > 0" if "k \<ge> l" and "l > 0" for k l :: int
519   using that by (simp add: divide_int_def div_positive)
521 (*There is no div_neg_pos_trivial because  0 div b = 0 would supersede it*)
523 lemma mod_pos_pos_trivial [simp]:
524   "k mod l = k" if "k \<ge> 0" and "k < l" for k l :: int
525   using that by (auto intro!: mod_int_unique [of _ _ 0] simp add: eucl_rel_int_iff)
527 lemma mod_neg_neg_trivial [simp]:
528   "k mod l = k" if "k \<le> 0" and "l < k" for k l :: int
529   using that by (auto intro!: mod_int_unique [of _ _ 0] simp add: eucl_rel_int_iff)
531 lemma mod_pos_neg_trivial: "[| (0::int) < a;  a+b \<le> 0 |] ==> a mod b = a+b"
532 apply (rule_tac q = "-1" in mod_int_unique)
533 apply (auto simp add: eucl_rel_int_iff)
534 done
536 text\<open>There is no \<open>mod_neg_pos_trivial\<close>.\<close>
539 subsubsection \<open>Laws for div and mod with Unary Minus\<close>
541 lemma zminus1_lemma:
542      "eucl_rel_int a b (q, r) ==> b \<noteq> 0
543       ==> eucl_rel_int (-a) b (if r=0 then -q else -q - 1,
544                           if r=0 then 0 else b-r)"
545 by (force simp add: eucl_rel_int_iff right_diff_distrib)
548 lemma zdiv_zminus1_eq_if:
549      "b \<noteq> (0::int)
550       ==> (-a) div b =
551           (if a mod b = 0 then - (a div b) else  - (a div b) - 1)"
552 by (blast intro: eucl_rel_int [THEN zminus1_lemma, THEN div_int_unique])
554 lemma zmod_zminus1_eq_if:
555      "(-a::int) mod b = (if a mod b = 0 then 0 else  b - (a mod b))"
556 apply (case_tac "b = 0", simp)
557 apply (blast intro: eucl_rel_int [THEN zminus1_lemma, THEN mod_int_unique])
558 done
560 lemma zmod_zminus1_not_zero:
561   fixes k l :: int
562   shows "- k mod l \<noteq> 0 \<Longrightarrow> k mod l \<noteq> 0"
565 lemma zmod_zminus2_not_zero:
566   fixes k l :: int
567   shows "k mod - l \<noteq> 0 \<Longrightarrow> k mod l \<noteq> 0"
570 lemma zdiv_zminus2_eq_if:
571   "b \<noteq> (0::int)
572       ==> a div (-b) =
573           (if a mod b = 0 then - (a div b) else  - (a div b) - 1)"
574   by (auto simp add: zdiv_zminus1_eq_if div_minus_right)
576 lemma zmod_zminus2_eq_if:
577   "a mod (-b::int) = (if a mod b = 0 then 0 else  (a mod b) - b)"
578   by (auto simp add: zmod_zminus1_eq_if mod_minus_right)
581 subsubsection \<open>Monotonicity in the First Argument (Dividend)\<close>
583 lemma zdiv_mono1: "[| a \<le> a';  0 < (b::int) |] ==> a div b \<le> a' div b"
584 using mult_div_mod_eq [symmetric, of a b]
585 using mult_div_mod_eq [symmetric, of a' b]
586 apply -
587 apply (rule unique_quotient_lemma)
588 apply (erule subst)
589 apply (erule subst, simp_all)
590 done
592 lemma zdiv_mono1_neg: "[| a \<le> a';  (b::int) < 0 |] ==> a' div b \<le> a div b"
593 using mult_div_mod_eq [symmetric, of a b]
594 using mult_div_mod_eq [symmetric, of a' b]
595 apply -
596 apply (rule unique_quotient_lemma_neg)
597 apply (erule subst)
598 apply (erule subst, simp_all)
599 done
602 subsubsection \<open>Monotonicity in the Second Argument (Divisor)\<close>
604 lemma q_pos_lemma:
605      "[| 0 \<le> b'*q' + r'; r' < b';  0 < b' |] ==> 0 \<le> (q'::int)"
606 apply (subgoal_tac "0 < b'* (q' + 1) ")
609 done
611 lemma zdiv_mono2_lemma:
612      "[| b*q + r = b'*q' + r';  0 \<le> b'*q' + r';
613          r' < b';  0 \<le> r;  0 < b';  b' \<le> b |]
614       ==> q \<le> (q'::int)"
615 apply (frule q_pos_lemma, assumption+)
616 apply (subgoal_tac "b*q < b* (q' + 1) ")
618 apply (subgoal_tac "b*q = r' - r + b'*q'")
619  prefer 2 apply simp
620 apply (simp (no_asm_simp) add: distrib_left)
622 apply (rule mult_right_mono, auto)
623 done
625 lemma zdiv_mono2:
626      "[| (0::int) \<le> a;  0 < b';  b' \<le> b |] ==> a div b \<le> a div b'"
627 apply (subgoal_tac "b \<noteq> 0")
628   prefer 2 apply arith
629 using mult_div_mod_eq [symmetric, of a b]
630 using mult_div_mod_eq [symmetric, of a b']
631 apply -
632 apply (rule zdiv_mono2_lemma)
633 apply (erule subst)
634 apply (erule subst, simp_all)
635 done
637 lemma q_neg_lemma:
638      "[| b'*q' + r' < 0;  0 \<le> r';  0 < b' |] ==> q' \<le> (0::int)"
639 apply (subgoal_tac "b'*q' < 0")
640  apply (simp add: mult_less_0_iff, arith)
641 done
643 lemma zdiv_mono2_neg_lemma:
644      "[| b*q + r = b'*q' + r';  b'*q' + r' < 0;
645          r < b;  0 \<le> r';  0 < b';  b' \<le> b |]
646       ==> q' \<le> (q::int)"
647 apply (frule q_neg_lemma, assumption+)
648 apply (subgoal_tac "b*q' < b* (q + 1) ")
651 apply (subgoal_tac "b*q' \<le> b'*q'")
652  prefer 2 apply (simp add: mult_right_mono_neg, arith)
653 done
655 lemma zdiv_mono2_neg:
656      "[| a < (0::int);  0 < b';  b' \<le> b |] ==> a div b' \<le> a div b"
657 using mult_div_mod_eq [symmetric, of a b]
658 using mult_div_mod_eq [symmetric, of a b']
659 apply -
660 apply (rule zdiv_mono2_neg_lemma)
661 apply (erule subst)
662 apply (erule subst, simp_all)
663 done
666 subsubsection \<open>More Algebraic Laws for div and mod\<close>
668 lemma zdiv_zmult1_eq: "(a*b) div c = a*(b div c) + a*(b mod c) div (c::int)"
669   by (fact div_mult1_eq)
671 (*NOT suitable for rewriting: the RHS has an instance of the LHS*)
673      "(a+b) div (c::int) = a div c + b div c + ((a mod c + b mod c) div c)"
676 lemma zmod_eq_0_iff: "(m mod d = 0) = (EX q::int. m = d*q)"
677 by (simp add: dvd_eq_mod_eq_0 [symmetric] dvd_def)
679 (* REVISIT: should this be generalized to all semiring_div types? *)
680 lemmas zmod_eq_0D [dest!] = zmod_eq_0_iff [THEN iffD1]
683 subsubsection \<open>Proving  @{term "a div (b * c) = (a div b) div c"}\<close>
685 (*The condition c>0 seems necessary.  Consider that 7 div ~6 = ~2 but
686   7 div 2 div ~3 = 3 div ~3 = ~1.  The subcase (a div b) mod c = 0 seems
687   to cause particular problems.*)
689 text\<open>first, four lemmas to bound the remainder for the cases b<0 and b>0\<close>
691 lemma zmult2_lemma_aux1: "[| (0::int) < c;  b < r;  r \<le> 0 |] ==> b * c < b * (q mod c) + r"
692 apply (subgoal_tac "b * (c - q mod c) < r * 1")
694 apply (rule order_le_less_trans)
695  apply (erule_tac [2] mult_strict_right_mono)
696  apply (rule mult_left_mono_neg)
698  apply (simp)
699 apply (simp)
700 done
702 lemma zmult2_lemma_aux2:
703      "[| (0::int) < c;   b < r;  r \<le> 0 |] ==> b * (q mod c) + r \<le> 0"
704 apply (subgoal_tac "b * (q mod c) \<le> 0")
705  apply arith
707 done
709 lemma zmult2_lemma_aux3: "[| (0::int) < c;  0 \<le> r;  r < b |] ==> 0 \<le> b * (q mod c) + r"
710 apply (subgoal_tac "0 \<le> b * (q mod c) ")
711 apply arith
713 done
715 lemma zmult2_lemma_aux4: "[| (0::int) < c; 0 \<le> r; r < b |] ==> b * (q mod c) + r < b * c"
716 apply (subgoal_tac "r * 1 < b * (c - q mod c) ")
718 apply (rule order_less_le_trans)
719  apply (erule mult_strict_right_mono)
720  apply (rule_tac [2] mult_left_mono)
721   apply simp
723 apply simp
724 done
726 lemma zmult2_lemma: "[| eucl_rel_int a b (q, r); 0 < c |]
727       ==> eucl_rel_int a (b * c) (q div c, b*(q mod c) + r)"
728 by (auto simp add: mult.assoc eucl_rel_int_iff linorder_neq_iff
729                    zero_less_mult_iff distrib_left [symmetric]
730                    zmult2_lemma_aux1 zmult2_lemma_aux2 zmult2_lemma_aux3 zmult2_lemma_aux4 mult_less_0_iff split: if_split_asm)
732 lemma zdiv_zmult2_eq:
733   fixes a b c :: int
734   shows "0 \<le> c \<Longrightarrow> a div (b * c) = (a div b) div c"
735 apply (case_tac "b = 0", simp)
736 apply (force simp add: le_less eucl_rel_int [THEN zmult2_lemma, THEN div_int_unique])
737 done
739 lemma zmod_zmult2_eq:
740   fixes a b c :: int
741   shows "0 \<le> c \<Longrightarrow> a mod (b * c) = b * (a div b mod c) + a mod b"
742 apply (case_tac "b = 0", simp)
743 apply (force simp add: le_less eucl_rel_int [THEN zmult2_lemma, THEN mod_int_unique])
744 done
746 lemma div_pos_geq:
747   fixes k l :: int
748   assumes "0 < l" and "l \<le> k"
749   shows "k div l = (k - l) div l + 1"
750 proof -
751   have "k = (k - l) + l" by simp
752   then obtain j where k: "k = j + l" ..
754 qed
756 lemma mod_pos_geq:
757   fixes k l :: int
758   assumes "0 < l" and "l \<le> k"
759   shows "k mod l = (k - l) mod l"
760 proof -
761   have "k = (k - l) + l" by simp
762   then obtain j where k: "k = j + l" ..
763   with assms show ?thesis by simp
764 qed
767 subsubsection \<open>Splitting Rules for div and mod\<close>
769 text\<open>The proofs of the two lemmas below are essentially identical\<close>
771 lemma split_pos_lemma:
772  "0<k ==>
773     P(n div k :: int)(n mod k) = (\<forall>i j. 0\<le>j & j<k & n = k*i + j --> P i j)"
774   by auto
776 lemma split_neg_lemma:
777  "k<0 ==>
778     P(n div k :: int)(n mod k) = (\<forall>i j. k<j & j\<le>0 & n = k*i + j --> P i j)"
779   by auto
781 lemma split_zdiv:
782  "P(n div k :: int) =
783   ((k = 0 --> P 0) &
784    (0<k --> (\<forall>i j. 0\<le>j & j<k & n = k*i + j --> P i)) &
785    (k<0 --> (\<forall>i j. k<j & j\<le>0 & n = k*i + j --> P i)))"
786   apply (cases "k = 0")
787   apply simp
788 apply (simp only: linorder_neq_iff)
789  apply (auto simp add: split_pos_lemma [of concl: "%x y. P x"]
790                       split_neg_lemma [of concl: "%x y. P x"])
791 done
793 lemma split_zmod:
794  "P(n mod k :: int) =
795   ((k = 0 --> P n) &
796    (0<k --> (\<forall>i j. 0\<le>j & j<k & n = k*i + j --> P j)) &
797    (k<0 --> (\<forall>i j. k<j & j\<le>0 & n = k*i + j --> P j)))"
798 apply (case_tac "k=0", simp)
799 apply (simp only: linorder_neq_iff)
800 apply (erule disjE)
801  apply (simp_all add: split_pos_lemma [of concl: "%x y. P y"]
802                       split_neg_lemma [of concl: "%x y. P y"])
803 done
805 text \<open>Enable (lin)arith to deal with @{const divide} and @{const modulo}
806   when these are applied to some constant that is of the form
807   @{term "numeral k"}:\<close>
808 declare split_zdiv [of _ _ "numeral k", arith_split] for k
809 declare split_zmod [of _ _ "numeral k", arith_split] for k
812 subsubsection \<open>Computing \<open>div\<close> and \<open>mod\<close> with shifting\<close>
814 lemma pos_eucl_rel_int_mult_2:
815   assumes "0 \<le> b"
816   assumes "eucl_rel_int a b (q, r)"
817   shows "eucl_rel_int (1 + 2*a) (2*b) (q, 1 + 2*r)"
818   using assms unfolding eucl_rel_int_iff by auto
820 lemma neg_eucl_rel_int_mult_2:
821   assumes "b \<le> 0"
822   assumes "eucl_rel_int (a + 1) b (q, r)"
823   shows "eucl_rel_int (1 + 2*a) (2*b) (q, 2*r - 1)"
824   using assms unfolding eucl_rel_int_iff by auto
826 text\<open>computing div by shifting\<close>
828 lemma pos_zdiv_mult_2: "(0::int) \<le> a ==> (1 + 2*b) div (2*a) = b div a"
829   using pos_eucl_rel_int_mult_2 [OF _ eucl_rel_int]
830   by (rule div_int_unique)
832 lemma neg_zdiv_mult_2:
833   assumes A: "a \<le> (0::int)" shows "(1 + 2*b) div (2*a) = (b+1) div a"
834   using neg_eucl_rel_int_mult_2 [OF A eucl_rel_int]
835   by (rule div_int_unique)
837 (* FIXME: add rules for negative numerals *)
838 lemma zdiv_numeral_Bit0 [simp]:
839   "numeral (Num.Bit0 v) div numeral (Num.Bit0 w) =
840     numeral v div (numeral w :: int)"
841   unfolding numeral.simps unfolding mult_2 [symmetric]
842   by (rule div_mult_mult1, simp)
844 lemma zdiv_numeral_Bit1 [simp]:
845   "numeral (Num.Bit1 v) div numeral (Num.Bit0 w) =
846     (numeral v div (numeral w :: int))"
847   unfolding numeral.simps
848   unfolding mult_2 [symmetric] add.commute [of _ 1]
849   by (rule pos_zdiv_mult_2, simp)
851 lemma pos_zmod_mult_2:
852   fixes a b :: int
853   assumes "0 \<le> a"
854   shows "(1 + 2 * b) mod (2 * a) = 1 + 2 * (b mod a)"
855   using pos_eucl_rel_int_mult_2 [OF assms eucl_rel_int]
856   by (rule mod_int_unique)
858 lemma neg_zmod_mult_2:
859   fixes a b :: int
860   assumes "a \<le> 0"
861   shows "(1 + 2 * b) mod (2 * a) = 2 * ((b + 1) mod a) - 1"
862   using neg_eucl_rel_int_mult_2 [OF assms eucl_rel_int]
863   by (rule mod_int_unique)
865 (* FIXME: add rules for negative numerals *)
866 lemma zmod_numeral_Bit0 [simp]:
867   "numeral (Num.Bit0 v) mod numeral (Num.Bit0 w) =
868     (2::int) * (numeral v mod numeral w)"
869   unfolding numeral_Bit0 [of v] numeral_Bit0 [of w]
870   unfolding mult_2 [symmetric] by (rule mod_mult_mult1)
872 lemma zmod_numeral_Bit1 [simp]:
873   "numeral (Num.Bit1 v) mod numeral (Num.Bit0 w) =
874     2 * (numeral v mod numeral w) + (1::int)"
875   unfolding numeral_Bit1 [of v] numeral_Bit0 [of w]
876   unfolding mult_2 [symmetric] add.commute [of _ 1]
877   by (rule pos_zmod_mult_2, simp)
879 lemma zdiv_eq_0_iff:
880   "i div k = 0 \<longleftrightarrow> k = 0 \<or> 0 \<le> i \<and> i < k \<or> i \<le> 0 \<and> k < i" (is "?L = ?R")
881   for i k :: int
882 proof
883   assume ?L
884   moreover have "?L \<longrightarrow> ?R"
885     by (rule split_zdiv [THEN iffD2]) simp
886   ultimately show ?R
887     by blast
888 next
889   assume ?R then show ?L
890     by auto
891 qed
893 lemma zmod_trival_iff:
894   fixes i k :: int
895   shows "i mod k = i \<longleftrightarrow> k = 0 \<or> 0 \<le> i \<and> i < k \<or> i \<le> 0 \<and> k < i"
896 proof -
897   have "i mod k = i \<longleftrightarrow> i div k = 0"
898     by safe (insert div_mult_mod_eq [of i k], auto)
899   with zdiv_eq_0_iff
900   show ?thesis
901     by simp
902 qed
905 subsubsection \<open>Quotients of Signs\<close>
907 lemma div_eq_minus1: "(0::int) < b ==> -1 div b = -1"
910 lemma zmod_minus1: "(0::int) < b ==> -1 mod b = b - 1"
913 lemma div_neg_pos_less0: "[| a < (0::int);  0 < b |] ==> a div b < 0"
914 apply (subgoal_tac "a div b \<le> -1", force)
915 apply (rule order_trans)
916 apply (rule_tac a' = "-1" in zdiv_mono1)
917 apply (auto simp add: div_eq_minus1)
918 done
920 lemma div_nonneg_neg_le0: "[| (0::int) \<le> a; b < 0 |] ==> a div b \<le> 0"
921 by (drule zdiv_mono1_neg, auto)
923 lemma div_nonpos_pos_le0: "[| (a::int) \<le> 0; b > 0 |] ==> a div b \<le> 0"
924 by (drule zdiv_mono1, auto)
926 text\<open>Now for some equivalences of the form \<open>a div b >=< 0 \<longleftrightarrow> \<dots>\<close>
927 conditional upon the sign of \<open>a\<close> or \<open>b\<close>. There are many more.
928 They should all be simp rules unless that causes too much search.\<close>
930 lemma pos_imp_zdiv_nonneg_iff: "(0::int) < b ==> (0 \<le> a div b) = (0 \<le> a)"
931 apply auto
932 apply (drule_tac [2] zdiv_mono1)
933 apply (auto simp add: linorder_neq_iff)
934 apply (simp (no_asm_use) add: linorder_not_less [symmetric])
935 apply (blast intro: div_neg_pos_less0)
936 done
938 lemma pos_imp_zdiv_pos_iff:
939   "0<k \<Longrightarrow> 0 < (i::int) div k \<longleftrightarrow> k \<le> i"
940 using pos_imp_zdiv_nonneg_iff[of k i] zdiv_eq_0_iff[of i k]
941 by arith
943 lemma neg_imp_zdiv_nonneg_iff:
944   "b < (0::int) ==> (0 \<le> a div b) = (a \<le> (0::int))"
945 apply (subst div_minus_minus [symmetric])
946 apply (subst pos_imp_zdiv_nonneg_iff, auto)
947 done
949 (*But not (a div b \<le> 0 iff a\<le>0); consider a=1, b=2 when a div b = 0.*)
950 lemma pos_imp_zdiv_neg_iff: "(0::int) < b ==> (a div b < 0) = (a < 0)"
951 by (simp add: linorder_not_le [symmetric] pos_imp_zdiv_nonneg_iff)
953 (*Again the law fails for \<le>: consider a = -1, b = -2 when a div b = 0*)
954 lemma neg_imp_zdiv_neg_iff: "b < (0::int) ==> (a div b < 0) = (0 < a)"
955 by (simp add: linorder_not_le [symmetric] neg_imp_zdiv_nonneg_iff)
957 lemma nonneg1_imp_zdiv_pos_iff:
958   "(0::int) <= a \<Longrightarrow> (a div b > 0) = (a >= b & b>0)"
959 apply rule
960  apply rule
961   using div_pos_pos_trivial[of a b]apply arith
962  apply(cases "b=0")apply simp
963  using div_nonneg_neg_le0[of a b]apply arith
964 using int_one_le_iff_zero_less[of "a div b"] zdiv_mono1[of b a b]apply simp
965 done
967 lemma zmod_le_nonneg_dividend: "(m::int) \<ge> 0 ==> m mod k \<le> m"
968 apply (rule split_zmod[THEN iffD2])
969 apply(fastforce dest: q_pos_lemma intro: split_mult_pos_le)
970 done
973 subsubsection \<open>Computation of Division and Remainder\<close>
975 instantiation int :: unique_euclidean_semiring_numeral
976 begin
978 definition divmod_int :: "num \<Rightarrow> num \<Rightarrow> int \<times> int"
979 where
980   "divmod_int m n = (numeral m div numeral n, numeral m mod numeral n)"
982 definition divmod_step_int :: "num \<Rightarrow> int \<times> int \<Rightarrow> int \<times> int"
983 where
984   "divmod_step_int l qr = (let (q, r) = qr
985     in if r \<ge> numeral l then (2 * q + 1, r - numeral l)
986     else (2 * q, r))"
988 instance
989   by standard (auto intro: zmod_le_nonneg_dividend simp add: divmod_int_def divmod_step_int_def
990     pos_imp_zdiv_pos_iff zmod_zmult2_eq zdiv_zmult2_eq)
992 end
994 declare divmod_algorithm_code [where ?'a = int, code]
996 context
997 begin
999 qualified definition adjust_div :: "int \<times> int \<Rightarrow> int"
1000 where
1001   "adjust_div qr = (let (q, r) = qr in q + of_bool (r \<noteq> 0))"
1003 qualified lemma adjust_div_eq [simp, code]:
1004   "adjust_div (q, r) = q + of_bool (r \<noteq> 0)"
1007 qualified definition adjust_mod :: "int \<Rightarrow> int \<Rightarrow> int"
1008 where
1009   [simp]: "adjust_mod l r = (if r = 0 then 0 else l - r)"
1011 lemma minus_numeral_div_numeral [simp]:
1012   "- numeral m div numeral n = - (adjust_div (divmod m n) :: int)"
1013 proof -
1014   have "int (fst (divmod m n)) = fst (divmod m n)"
1015     by (simp only: fst_divmod divide_int_def) auto
1016   then show ?thesis
1018 qed
1020 lemma minus_numeral_mod_numeral [simp]:
1021   "- numeral m mod numeral n = adjust_mod (numeral n) (snd (divmod m n) :: int)"
1022 proof (cases "snd (divmod m n) = (0::int)")
1023   case True
1024   then show ?thesis
1025     by (simp add: mod_eq_0_iff_dvd divides_aux_def)
1026 next
1027   case False
1028   then have "int (snd (divmod m n)) = snd (divmod m n)" if "snd (divmod m n) \<noteq> (0::int)"
1029     by (simp only: snd_divmod modulo_int_def) auto
1030   then show ?thesis
1033 qed
1035 lemma numeral_div_minus_numeral [simp]:
1036   "numeral m div - numeral n = - (adjust_div (divmod m n) :: int)"
1037 proof -
1038   have "int (fst (divmod m n)) = fst (divmod m n)"
1039     by (simp only: fst_divmod divide_int_def) auto
1040   then show ?thesis
1042 qed
1044 lemma numeral_mod_minus_numeral [simp]:
1045   "numeral m mod - numeral n = - adjust_mod (numeral n) (snd (divmod m n) :: int)"
1046 proof (cases "snd (divmod m n) = (0::int)")
1047   case True
1048   then show ?thesis
1049     by (simp add: mod_eq_0_iff_dvd divides_aux_def)
1050 next
1051   case False
1052   then have "int (snd (divmod m n)) = snd (divmod m n)" if "snd (divmod m n) \<noteq> (0::int)"
1053     by (simp only: snd_divmod modulo_int_def) auto
1054   then show ?thesis
1057 qed
1059 lemma minus_one_div_numeral [simp]:
1060   "- 1 div numeral n = - (adjust_div (divmod Num.One n) :: int)"
1061   using minus_numeral_div_numeral [of Num.One n] by simp
1063 lemma minus_one_mod_numeral [simp]:
1064   "- 1 mod numeral n = adjust_mod (numeral n) (snd (divmod Num.One n) :: int)"
1065   using minus_numeral_mod_numeral [of Num.One n] by simp
1067 lemma one_div_minus_numeral [simp]:
1068   "1 div - numeral n = - (adjust_div (divmod Num.One n) :: int)"
1069   using numeral_div_minus_numeral [of Num.One n] by simp
1071 lemma one_mod_minus_numeral [simp]:
1072   "1 mod - numeral n = - adjust_mod (numeral n) (snd (divmod Num.One n) :: int)"
1073   using numeral_mod_minus_numeral [of Num.One n] by simp
1075 end
1078 subsubsection \<open>Further properties\<close>
1080 lemma div_int_pos_iff:
1081   "k div l \<ge> 0 \<longleftrightarrow> k = 0 \<or> l = 0 \<or> k \<ge> 0 \<and> l \<ge> 0
1082     \<or> k < 0 \<and> l < 0"
1083   for k l :: int
1084   apply (cases "k = 0 \<or> l = 0")
1085    apply (auto simp add: pos_imp_zdiv_nonneg_iff neg_imp_zdiv_nonneg_iff)
1086   apply (rule ccontr)
1088   done
1090 lemma mod_int_pos_iff:
1091   "k mod l \<ge> 0 \<longleftrightarrow> l dvd k \<or> l = 0 \<and> k \<ge> 0 \<or> l > 0"
1092   for k l :: int
1093   apply (cases "l > 0")
1095   apply (use neg_mod_conj [of l k] in \<open>auto simp add: le_less not_less\<close>)
1096   done
1098 text \<open>Simplify expresions in which div and mod combine numerical constants\<close>
1100 lemma int_div_pos_eq: "\<lbrakk>(a::int) = b * q + r; 0 \<le> r; r < b\<rbrakk> \<Longrightarrow> a div b = q"
1101   by (rule div_int_unique [of a b q r]) (simp add: eucl_rel_int_iff)
1103 lemma int_div_neg_eq: "\<lbrakk>(a::int) = b * q + r; r \<le> 0; b < r\<rbrakk> \<Longrightarrow> a div b = q"
1104   by (rule div_int_unique [of a b q r],
1107 lemma int_mod_pos_eq: "\<lbrakk>(a::int) = b * q + r; 0 \<le> r; r < b\<rbrakk> \<Longrightarrow> a mod b = r"
1108   by (rule mod_int_unique [of a b q r],
1111 lemma int_mod_neg_eq: "\<lbrakk>(a::int) = b * q + r; r \<le> 0; b < r\<rbrakk> \<Longrightarrow> a mod b = r"
1112   by (rule mod_int_unique [of a b q r],
1115 lemma abs_div: "(y::int) dvd x \<Longrightarrow> \<bar>x div y\<bar> = \<bar>x\<bar> div \<bar>y\<bar>"
1116 by (unfold dvd_def, cases "y=0", auto simp add: abs_mult)
1118 text\<open>Suggested by Matthias Daum\<close>
1119 lemma int_power_div_base:
1120      "\<lbrakk>0 < m; 0 < k\<rbrakk> \<Longrightarrow> k ^ m div k = (k::int) ^ (m - Suc 0)"
1121 apply (subgoal_tac "k ^ m = k ^ ((m - Suc 0) + Suc 0)")
1122  apply (erule ssubst)
1124  apply simp_all
1125 done
1127 text \<open>Distributive laws for function \<open>nat\<close>.\<close>
1129 lemma nat_div_distrib: "0 \<le> x \<Longrightarrow> nat (x div y) = nat x div nat y"
1130 apply (rule linorder_cases [of y 0])
1132 apply simp
1133 apply (simp add: nat_eq_iff pos_imp_zdiv_nonneg_iff zdiv_int)
1134 done
1136 (*Fails if y<0: the LHS collapses to (nat z) but the RHS doesn't*)
1137 lemma nat_mod_distrib:
1138   "\<lbrakk>0 \<le> x; 0 \<le> y\<rbrakk> \<Longrightarrow> nat (x mod y) = nat x mod nat y"
1139 apply (case_tac "y = 0", simp)
1140 apply (simp add: nat_eq_iff zmod_int)
1141 done
1143 text\<open>Suggested by Matthias Daum\<close>
1144 lemma int_div_less_self: "\<lbrakk>0 < x; 1 < k\<rbrakk> \<Longrightarrow> x div k < (x::int)"
1145 apply (subgoal_tac "nat x div nat k < nat x")
1146  apply (simp add: nat_div_distrib [symmetric])
1147 apply (rule div_less_dividend, simp_all)
1148 done
1150 lemma mod_eq_dvd_iff_nat:
1151   "m mod q = n mod q \<longleftrightarrow> q dvd m - n" if "m \<ge> n" for m n q :: nat
1152 proof -
1153   have "int m mod int q = int n mod int q \<longleftrightarrow> int q dvd int m - int n"
1155   with that have "int (m mod q) = int (n mod q) \<longleftrightarrow> int q dvd int (m - n)"
1156     by (simp only: of_nat_mod of_nat_diff)
1157   then show ?thesis
1159 qed
1161 lemma mod_eq_nat1E:
1162   fixes m n q :: nat
1163   assumes "m mod q = n mod q" and "m \<ge> n"
1164   obtains s where "m = n + q * s"
1165 proof -
1166   from assms have "q dvd m - n"
1168   then obtain s where "m - n = q * s" ..
1169   with \<open>m \<ge> n\<close> have "m = n + q * s"
1170     by simp
1171   with that show thesis .
1172 qed
1174 lemma mod_eq_nat2E:
1175   fixes m n q :: nat
1176   assumes "m mod q = n mod q" and "n \<ge> m"
1177   obtains s where "n = m + q * s"
1178   using assms mod_eq_nat1E [of n q m] by (auto simp add: ac_simps)
1180 lemma nat_mod_eq_lemma:
1181   assumes "(x::nat) mod n = y mod n" and "y \<le> x"
1182   shows "\<exists>q. x = y + n * q"
1183   using assms by (rule mod_eq_nat1E) rule
1185 lemma nat_mod_eq_iff: "(x::nat) mod n = y mod n \<longleftrightarrow> (\<exists>q1 q2. x + n * q1 = y + n * q2)"
1186   (is "?lhs = ?rhs")
1187 proof
1188   assume H: "x mod n = y mod n"
1189   {assume xy: "x \<le> y"
1190     from H have th: "y mod n = x mod n" by simp
1191     from nat_mod_eq_lemma[OF th xy] have ?rhs
1192       apply clarify  apply (rule_tac x="q" in exI) by (rule exI[where x="0"], simp)}
1193   moreover
1194   {assume xy: "y \<le> x"
1195     from nat_mod_eq_lemma[OF H xy] have ?rhs
1196       apply clarify  apply (rule_tac x="0" in exI) by (rule_tac x="q" in exI, simp)}
1197   ultimately  show ?rhs using linear[of x y] by blast
1198 next
1199   assume ?rhs then obtain q1 q2 where q12: "x + n * q1 = y + n * q2" by blast
1200   hence "(x + n * q1) mod n = (y + n * q2) mod n" by simp
1201   thus  ?lhs by simp
1202 qed
1205 subsubsection \<open>Dedicated simproc for calculation\<close>
1207 text \<open>
1208   There is space for improvement here: the calculation itself
1209   could be carried out outside the logic, and a generic simproc
1210   (simplifier setup) for generic calculation would be helpful.
1211 \<close>
1213 simproc_setup numeral_divmod
1214   ("0 div 0 :: 'a :: unique_euclidean_semiring_numeral" | "0 mod 0 :: 'a :: unique_euclidean_semiring_numeral" |
1215    "0 div 1 :: 'a :: unique_euclidean_semiring_numeral" | "0 mod 1 :: 'a :: unique_euclidean_semiring_numeral" |
1216    "0 div - 1 :: int" | "0 mod - 1 :: int" |
1217    "0 div numeral b :: 'a :: unique_euclidean_semiring_numeral" | "0 mod numeral b :: 'a :: unique_euclidean_semiring_numeral" |
1218    "0 div - numeral b :: int" | "0 mod - numeral b :: int" |
1219    "1 div 0 :: 'a :: unique_euclidean_semiring_numeral" | "1 mod 0 :: 'a :: unique_euclidean_semiring_numeral" |
1220    "1 div 1 :: 'a :: unique_euclidean_semiring_numeral" | "1 mod 1 :: 'a :: unique_euclidean_semiring_numeral" |
1221    "1 div - 1 :: int" | "1 mod - 1 :: int" |
1222    "1 div numeral b :: 'a :: unique_euclidean_semiring_numeral" | "1 mod numeral b :: 'a :: unique_euclidean_semiring_numeral" |
1223    "1 div - numeral b :: int" |"1 mod - numeral b :: int" |
1224    "- 1 div 0 :: int" | "- 1 mod 0 :: int" | "- 1 div 1 :: int" | "- 1 mod 1 :: int" |
1225    "- 1 div - 1 :: int" | "- 1 mod - 1 :: int" | "- 1 div numeral b :: int" | "- 1 mod numeral b :: int" |
1226    "- 1 div - numeral b :: int" | "- 1 mod - numeral b :: int" |
1227    "numeral a div 0 :: 'a :: unique_euclidean_semiring_numeral" | "numeral a mod 0 :: 'a :: unique_euclidean_semiring_numeral" |
1228    "numeral a div 1 :: 'a :: unique_euclidean_semiring_numeral" | "numeral a mod 1 :: 'a :: unique_euclidean_semiring_numeral" |
1229    "numeral a div - 1 :: int" | "numeral a mod - 1 :: int" |
1230    "numeral a div numeral b :: 'a :: unique_euclidean_semiring_numeral" | "numeral a mod numeral b :: 'a :: unique_euclidean_semiring_numeral" |
1231    "numeral a div - numeral b :: int" | "numeral a mod - numeral b :: int" |
1232    "- numeral a div 0 :: int" | "- numeral a mod 0 :: int" |
1233    "- numeral a div 1 :: int" | "- numeral a mod 1 :: int" |
1234    "- numeral a div - 1 :: int" | "- numeral a mod - 1 :: int" |
1235    "- numeral a div numeral b :: int" | "- numeral a mod numeral b :: int" |
1236    "- numeral a div - numeral b :: int" | "- numeral a mod - numeral b :: int") =
1237 \<open> let
1238     val if_cong = the (Code.get_case_cong @{theory} @{const_name If});
1239     fun successful_rewrite ctxt ct =
1240       let
1241         val thm = Simplifier.rewrite ctxt ct
1242       in if Thm.is_reflexive thm then NONE else SOME thm end;
1243   in fn phi =>
1244     let
1245       val simps = Morphism.fact phi (@{thms div_0 mod_0 div_by_0 mod_by_0 div_by_1 mod_by_1
1246         one_div_numeral one_mod_numeral minus_one_div_numeral minus_one_mod_numeral
1247         one_div_minus_numeral one_mod_minus_numeral
1248         numeral_div_numeral numeral_mod_numeral minus_numeral_div_numeral minus_numeral_mod_numeral
1249         numeral_div_minus_numeral numeral_mod_minus_numeral
1250         div_minus_minus mod_minus_minus Divides.adjust_div_eq of_bool_eq one_neq_zero
1251         numeral_neq_zero neg_equal_0_iff_equal arith_simps arith_special divmod_trivial
1252         divmod_cancel divmod_steps divmod_step_eq fst_conv snd_conv numeral_One
1253         case_prod_beta rel_simps Divides.adjust_mod_def div_minus1_right mod_minus1_right
1254         minus_minus numeral_times_numeral mult_zero_right mult_1_right}
1255         @ [@{lemma "0 = 0 \<longleftrightarrow> True" by simp}]);
1256       fun prepare_simpset ctxt = HOL_ss |> Simplifier.simpset_map ctxt
1258     in fn ctxt => successful_rewrite (Simplifier.put_simpset (prepare_simpset ctxt) ctxt) end
1259   end;
1260 \<close>
1263 subsubsection \<open>Code generation\<close>
1265 lemma [code]:
1266   fixes k :: int
1267   shows
1268     "k div 0 = 0"
1269     "k mod 0 = k"
1270     "0 div k = 0"
1271     "0 mod k = 0"
1272     "k div Int.Pos Num.One = k"
1273     "k mod Int.Pos Num.One = 0"
1274     "k div Int.Neg Num.One = - k"
1275     "k mod Int.Neg Num.One = 0"
1276     "Int.Pos m div Int.Pos n = (fst (divmod m n) :: int)"
1277     "Int.Pos m mod Int.Pos n = (snd (divmod m n) :: int)"
1278     "Int.Neg m div Int.Pos n = - (Divides.adjust_div (divmod m n) :: int)"
1279     "Int.Neg m mod Int.Pos n = Divides.adjust_mod (Int.Pos n) (snd (divmod m n) :: int)"
1280     "Int.Pos m div Int.Neg n = - (Divides.adjust_div (divmod m n) :: int)"
1281     "Int.Pos m mod Int.Neg n = - Divides.adjust_mod (Int.Pos n) (snd (divmod m n) :: int)"
1282     "Int.Neg m div Int.Neg n = (fst (divmod m n) :: int)"
1283     "Int.Neg m mod Int.Neg n = - (snd (divmod m n) :: int)"
1284   by simp_all
1286 code_identifier
1287   code_module Divides \<rightharpoonup> (SML) Arith and (OCaml) Arith and (Haskell) Arith
1289 lemma dvd_eq_mod_eq_0_numeral:
1290   "numeral x dvd (numeral y :: 'a) \<longleftrightarrow> numeral y mod numeral x = (0 :: 'a::semidom_modulo)"
1291   by (fact dvd_eq_mod_eq_0)
1293 declare minus_div_mult_eq_mod [symmetric, nitpick_unfold]
1296 subsubsection \<open>Lemmas of doubtful value\<close>
1298 lemma mod_mult_self3':
1299   "Suc (k * n + m) mod n = Suc m mod n"
1300   by (fact Suc_mod_mult_self3)
1302 lemma mod_Suc_eq_Suc_mod:
1303   "Suc m mod n = Suc (m mod n) mod n"
1306 lemma div_geq:
1307   "m div n = Suc ((m - n) div n)" if "0 < n" and " \<not> m < n" for m n :: nat
1308   by (rule le_div_geq) (use that in \<open>simp_all add: not_less\<close>)
1310 lemma mod_geq:
1311   "m mod n = (m - n) mod n" if "\<not> m < n" for m n :: nat
1312   by (rule le_mod_geq) (use that in \<open>simp add: not_less\<close>)
1314 lemma mod_eq_0_iff: "(m mod d = 0) = (\<exists>q::nat. m = d*q)"
1315   by (auto simp add: dvd_eq_mod_eq_0 [symmetric] dvd_def)
1317 lemmas mod_eq_0D [dest!] = mod_eq_0_iff [THEN iffD1]
1319 (*Loses information, namely we also have r<d provided d is nonzero*)
1320 lemma mod_eqD:
1321   fixes m d r q :: nat
1322   assumes "m mod d = r"
1323   shows "\<exists>q. m = r + q * d"
1324 proof -
1325   from div_mult_mod_eq obtain q where "q * d + m mod d = m" by blast
1326   with assms have "m = r + q * d" by simp
1327   then show ?thesis ..
1328 qed
1330 lemmas even_times_iff = even_mult_iff -- \<open>FIXME duplicate\<close>
1332 lemma mod_2_not_eq_zero_eq_one_nat:
1333   fixes n :: nat
1334   shows "n mod 2 \<noteq> 0 \<longleftrightarrow> n mod 2 = 1"
1335   by (fact not_mod_2_eq_0_eq_1)
1337 lemma even_int_iff [simp]: "even (int n) \<longleftrightarrow> even n"
1338   by (fact even_of_nat)
1340 lemma is_unit_int:
1341   "is_unit (k::int) \<longleftrightarrow> k = 1 \<or> k = - 1"
1342   by auto
1344 end