1(*
2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
3 *
4 * SPDX-License-Identifier: BSD-2-Clause
5 *)
6
7section "More Lemmas on Division"
8
9theory More_Divides
10imports Main
11begin
12
13lemma div_mult_le:
14  "(a::nat) div b * b \<le> a"
15  by (fact div_times_less_eq_dividend)
16
17lemma diff_mod_le:
18  "\<lbrakk> (a::nat) < d; b dvd d \<rbrakk> \<Longrightarrow> a - a mod b \<le> d - b"
19  apply(subst minus_mod_eq_mult_div)
20  apply(clarsimp simp: dvd_def)
21  apply(case_tac "b = 0")
22   apply simp
23  apply(subgoal_tac "a div b \<le> k - 1")
24   prefer 2
25   apply(subgoal_tac "a div b < k")
26    apply(simp add: less_Suc_eq_le [symmetric])
27   apply(subgoal_tac "b * (a div b) < b * ((b * k) div b)")
28    apply clarsimp
29   apply(subst div_mult_self1_is_m)
30    apply arith
31   apply(rule le_less_trans)
32    apply simp
33    apply(subst mult.commute)
34    apply(rule div_mult_le)
35   apply assumption
36  apply clarsimp
37  apply(subgoal_tac "b * (a div b) \<le> b * (k - 1)")
38   apply(erule le_trans)
39   apply(simp add: diff_mult_distrib2)
40  apply simp
41  done
42
43lemma int_div_same_is_1 [simp]:
44  "0 < a \<Longrightarrow> ((a :: int) div b = a) = (b = 1)"
45  by (metis div_by_1 abs_ge_zero abs_of_pos int_div_less_self neq_iff
46            nonneg1_imp_zdiv_pos_iff zabs_less_one_iff)
47
48declare div_eq_dividend_iff [simp]
49
50lemma int_div_minus_is_minus1 [simp]:
51    "a < 0 \<Longrightarrow> ((a :: int) div b = -a) = (b = -1)"
52  by (metis div_minus_right equation_minus_iff int_div_same_is_1 neg_0_less_iff_less)
53
54end
55