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