src/HOL/Divides.thy
 changeset 64246 15d1ee6e847b parent 64244 e7102c40783c child 64250 0cde0b4d4cb5
```     1.1 --- a/src/HOL/Divides.thy	Sun Oct 16 09:31:05 2016 +0200
1.2 +++ b/src/HOL/Divides.thy	Sun Oct 16 09:31:06 2016 +0200
1.3 @@ -565,17 +565,6 @@
1.4
1.5  begin
1.6
1.7 -lemma mult_div_cancel:
1.8 -  "b * (a div b) = a - a mod b"
1.9 -proof -
1.10 -  have "b * (a div b) + a mod b = a"
1.11 -    using div_mult_mod_eq [of a b] by (simp add: ac_simps)
1.12 -  then have "b * (a div b) + a mod b - a mod b = a - a mod b"
1.13 -    by simp
1.14 -  then show ?thesis
1.15 -    by simp
1.16 -qed
1.17 -
1.18  subclass semiring_div_parity
1.19  proof
1.20    fix a
1.21 @@ -617,7 +606,7 @@
1.22      by (auto simp add: mod_w) (insert mod_less, auto)
1.23    with mod_w have mod: "a mod (2 * b) = a mod b + b" by simp
1.24    have "2 * (a div (2 * b)) = a div b - w"
1.25 -    by (simp add: w_def div_mult2_eq mult_div_cancel ac_simps)
1.26 +    by (simp add: w_def div_mult2_eq minus_mod_eq_mult_div ac_simps)
1.27    with \<open>w = 1\<close> have div: "2 * (a div (2 * b)) = a div b - 1" by simp
1.28    then show ?P and ?Q
1.30 @@ -642,7 +631,7 @@
1.31    ultimately have "w = 0" by auto
1.32    with mod_w have mod: "a mod (2 * b) = a mod b" by simp
1.33    have "2 * (a div (2 * b)) = a div b - w"
1.34 -    by (simp add: w_def div_mult2_eq mult_div_cancel ac_simps)
1.35 +    by (simp add: w_def div_mult2_eq minus_mod_eq_mult_div ac_simps)
1.36    with \<open>w = 0\<close> have div: "2 * (a div (2 * b)) = a div b" by simp
1.37    then show ?P and ?Q
1.38      by (simp_all add: div mod)
1.39 @@ -1120,10 +1109,6 @@
1.40  lemma mod_by_Suc_0 [simp]: "m mod Suc 0 = 0"
1.41  by (induct m) (simp_all add: mod_geq)
1.42
1.43 -(* a simple rearrangement of div_mult_mod_eq: *)
1.44 -lemma mult_div_cancel: "(n::nat) * (m div n) = m - (m mod n)"
1.45 -  using mult_div_mod_eq [of n m] by arith
1.46 -
1.47  lemma mod_le_divisor[simp]: "0 < n \<Longrightarrow> m mod n \<le> (n::nat)"
1.48    apply (drule mod_less_divisor [where m = m])
1.49    apply simp
1.50 @@ -1329,7 +1314,7 @@
1.51    shows "n * q \<le> m \<and> m < n * Suc q \<longleftrightarrow> q = ((m::nat) div n)" (is "?lhs \<longleftrightarrow> ?rhs")
1.52  proof
1.53    assume ?rhs
1.54 -  with mult_div_cancel have nq: "n * q = m - (m mod n)" by simp
1.55 +  with minus_mod_eq_mult_div [symmetric] have nq: "n * q = m - (m mod n)" by simp
1.56    then have A: "n * q \<le> m" by simp
1.57    have "n - (m mod n) > 0" using mod_less_divisor assms by auto
1.58    then have "m < m + (n - (m mod n))" by simp
1.59 @@ -1387,8 +1372,6 @@
1.60    qed
1.61  qed
1.62
1.63 -declare minus_div_mult_eq_mod [symmetric, where ?'a = nat, nitpick_unfold]
1.64 -
1.65  lemma div_eq_dividend_iff: "a \<noteq> 0 \<Longrightarrow> (a :: nat) div b = a \<longleftrightarrow> b = 1"
1.66    apply rule
1.67    apply (cases "b = 0")
1.68 @@ -1806,9 +1789,6 @@
1.69
1.70  text\<open>Basic laws about division and remainder\<close>
1.71
1.72 -lemma zmod_zdiv_equality: "(a::int) = b * (a div b) + (a mod b)"
1.73 -  by (fact mult_div_mod_eq [symmetric])
1.74 -
1.75  lemma zdiv_int: "int (a div b) = int a div int b"
1.77
1.78 @@ -1932,16 +1912,18 @@
1.79  subsubsection \<open>Monotonicity in the First Argument (Dividend)\<close>
1.80
1.81  lemma zdiv_mono1: "[| a \<le> a';  0 < (b::int) |] ==> a div b \<le> a' div b"
1.82 -apply (cut_tac a = a and b = b in zmod_zdiv_equality)
1.83 -apply (cut_tac a = a' and b = b in zmod_zdiv_equality)
1.84 +using mult_div_mod_eq [symmetric, of a b]
1.85 +using mult_div_mod_eq [symmetric, of a' b]
1.86 +apply -
1.87  apply (rule unique_quotient_lemma)
1.88  apply (erule subst)
1.89  apply (erule subst, simp_all)
1.90  done
1.91
1.92  lemma zdiv_mono1_neg: "[| a \<le> a';  (b::int) < 0 |] ==> a' div b \<le> a div b"
1.93 -apply (cut_tac a = a and b = b in zmod_zdiv_equality)
1.94 -apply (cut_tac a = a' and b = b in zmod_zdiv_equality)
1.95 +using mult_div_mod_eq [symmetric, of a b]
1.96 +using mult_div_mod_eq [symmetric, of a' b]
1.97 +apply -
1.98  apply (rule unique_quotient_lemma_neg)
1.99  apply (erule subst)
1.100  apply (erule subst, simp_all)
1.101 @@ -1974,9 +1956,10 @@
1.102  lemma zdiv_mono2:
1.103       "[| (0::int) \<le> a;  0 < b';  b' \<le> b |] ==> a div b \<le> a div b'"
1.104  apply (subgoal_tac "b \<noteq> 0")
1.105 - prefer 2 apply arith
1.106 -apply (cut_tac a = a and b = b in zmod_zdiv_equality)
1.107 -apply (cut_tac a = a and b = b' in zmod_zdiv_equality)
1.108 +  prefer 2 apply arith
1.109 +using mult_div_mod_eq [symmetric, of a b]
1.110 +using mult_div_mod_eq [symmetric, of a b']
1.111 +apply -
1.112  apply (rule zdiv_mono2_lemma)
1.113  apply (erule subst)
1.114  apply (erule subst, simp_all)
1.115 @@ -2002,8 +1985,9 @@
1.116
1.117  lemma zdiv_mono2_neg:
1.118       "[| a < (0::int);  0 < b';  b' \<le> b |] ==> a div b' \<le> a div b"
1.119 -apply (cut_tac a = a and b = b in zmod_zdiv_equality)
1.120 -apply (cut_tac a = a and b = b' in zmod_zdiv_equality)
1.121 +using mult_div_mod_eq [symmetric, of a b]
1.122 +using mult_div_mod_eq [symmetric, of a b']
1.123 +apply -
1.124  apply (rule zdiv_mono2_neg_lemma)
1.125  apply (erule subst)
1.126  apply (erule subst, simp_all)
1.127 @@ -2044,10 +2028,6 @@
1.128  (* REVISIT: should this be generalized to all semiring_div types? *)
1.129  lemmas zmod_eq_0D [dest!] = zmod_eq_0_iff [THEN iffD1]
1.130
1.131 -lemma zmod_zdiv_equality' [nitpick_unfold]:
1.132 -  "(m::int) mod n = m - (m div n) * n"
1.133 -  using div_mult_mod_eq [of m n] by arith
1.134 -
1.135
1.136  subsubsection \<open>Proving  @{term "a div (b * c) = (a div b) div c"}\<close>
1.137
1.138 @@ -2350,11 +2330,6 @@
1.139  apply(fastforce dest: q_pos_lemma intro: split_mult_pos_le)
1.140  done
1.141
1.142 -lemma zmult_div_cancel:
1.143 -  "(n::int) * (m div n) = m - (m mod n)"
1.144 -  using zmod_zdiv_equality [where a="m" and b="n"]
1.145 -  by (simp add: algebra_simps) (* FIXME: generalize *)
1.146 -
1.147
1.148  subsubsection \<open>Computation of Division and Remainder\<close>
1.149
1.150 @@ -2690,6 +2665,8 @@
1.151    "numeral x dvd (numeral y :: 'a) \<longleftrightarrow> numeral y mod numeral x = (0 :: 'a::semiring_div)"
1.152    by (fact dvd_eq_mod_eq_0)
1.153
1.154 +declare minus_div_mult_eq_mod [symmetric, nitpick_unfold]
1.155 +
1.156  hide_fact (open) div_0 div_by_0
1.157
1.158  end
```