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.29      by (simp_all add: div mod add_implies_diff [symmetric])
    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.76    by (simp add: divide_int_def)
    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