src/HOL/IntDiv.thy
 changeset 30930 11010e5f18f0 parent 30652 752329615264 child 30934 ed5377c2b0a3
```     1.1 --- a/src/HOL/IntDiv.thy	Wed Apr 15 15:52:37 2009 +0200
1.2 +++ b/src/HOL/IntDiv.thy	Thu Apr 16 10:11:34 2009 +0200
1.3 @@ -711,6 +711,26 @@
1.4    show "(a + c * b) div b = c + a div b"
1.5      unfolding zdiv_zadd1_eq [of a "c * b"] using not0
1.6        by (simp add: zmod_zmult1_eq zmod_zdiv_trivial zdiv_zmult1_eq)
1.7 +next
1.8 +  fix a b c :: int
1.9 +  assume "a \<noteq> 0"
1.10 +  then show "(a * b) div (a * c) = b div c"
1.11 +  proof (cases "b \<noteq> 0 \<and> c \<noteq> 0")
1.12 +    case False then show ?thesis by auto
1.13 +  next
1.14 +    case True then have "b \<noteq> 0" and "c \<noteq> 0" by auto
1.15 +    with `a \<noteq> 0`
1.16 +    have "\<And>q r. divmod_rel b c (q, r) \<Longrightarrow> divmod_rel (a * b) (a * c) (q, a * r)"
1.17 +      apply (auto simp add: divmod_rel_def)
1.18 +      apply (auto simp add: algebra_simps)
1.19 +      apply (auto simp add: zero_less_mult_iff zero_le_mult_iff mult_le_0_iff)
1.20 +      apply (simp_all add: mult_less_cancel_left_disj mult_commute [of _ a])
1.21 +      done
1.22 +    moreover with `c \<noteq> 0` divmod_rel_div_mod have "divmod_rel b c (b div c, b mod c)" by auto
1.23 +    ultimately have "divmod_rel (a * b) (a * c) (b div c, a * (b mod c))" .
1.24 +    moreover from  `a \<noteq> 0` `c \<noteq> 0` have "a * c \<noteq> 0" by simp
1.25 +    ultimately show ?thesis by (rule divmod_rel_div)
1.26 +  qed
1.27  qed auto
1.28
1.29  lemma posDivAlg_div_mod:
1.30 @@ -808,52 +828,6 @@
1.31  done
1.32
1.33
1.34 -subsection{*Cancellation of Common Factors in div*}
1.35 -
1.36 -lemma zdiv_zmult_zmult1_aux1:
1.37 -     "[| (0::int) < b;  c \<noteq> 0 |] ==> (c*a) div (c*b) = a div b"
1.38 -by (subst zdiv_zmult2_eq, auto)
1.39 -
1.40 -lemma zdiv_zmult_zmult1_aux2:
1.41 -     "[| b < (0::int);  c \<noteq> 0 |] ==> (c*a) div (c*b) = a div b"
1.42 -apply (subgoal_tac " (c * (-a)) div (c * (-b)) = (-a) div (-b) ")
1.43 -apply (rule_tac [2] zdiv_zmult_zmult1_aux1, auto)
1.44 -done
1.45 -
1.46 -lemma zdiv_zmult_zmult1: "c \<noteq> (0::int) ==> (c*a) div (c*b) = a div b"
1.47 -apply (case_tac "b = 0", simp)
1.48 -apply (auto simp add: linorder_neq_iff zdiv_zmult_zmult1_aux1 zdiv_zmult_zmult1_aux2)
1.49 -done
1.50 -
1.51 -lemma zdiv_zmult_zmult1_if[simp]:
1.52 -  "(k*m) div (k*n) = (if k = (0::int) then 0 else m div n)"
1.54 -
1.55 -
1.56 -subsection{*Distribution of Factors over mod*}
1.57 -
1.58 -lemma zmod_zmult_zmult1_aux1:
1.59 -     "[| (0::int) < b;  c \<noteq> 0 |] ==> (c*a) mod (c*b) = c * (a mod b)"
1.60 -by (subst zmod_zmult2_eq, auto)
1.61 -
1.62 -lemma zmod_zmult_zmult1_aux2:
1.63 -     "[| b < (0::int);  c \<noteq> 0 |] ==> (c*a) mod (c*b) = c * (a mod b)"
1.64 -apply (subgoal_tac " (c * (-a)) mod (c * (-b)) = c * ((-a) mod (-b))")
1.65 -apply (rule_tac [2] zmod_zmult_zmult1_aux1, auto)
1.66 -done
1.67 -
1.68 -lemma zmod_zmult_zmult1: "(c*a) mod (c*b) = (c::int) * (a mod b)"
1.69 -apply (case_tac "b = 0", simp)
1.70 -apply (case_tac "c = 0", simp)
1.71 -apply (auto simp add: linorder_neq_iff zmod_zmult_zmult1_aux1 zmod_zmult_zmult1_aux2)
1.72 -done
1.73 -
1.74 -lemma zmod_zmult_zmult2: "(a*c) mod (b*c) = (a mod b) * (c::int)"
1.75 -apply (cut_tac c = c in zmod_zmult_zmult1)
1.76 -apply (auto simp add: mult_commute)
1.77 -done
1.78 -
1.79 -
1.80  subsection {*Splitting Rules for div and mod*}
1.81
1.82  text{*The proofs of the two lemmas below are essentially identical*}
1.83 @@ -937,7 +911,7 @@
1.84                    right_distrib)
1.85    thus ?thesis
1.87 -        simp add: zdiv_zmult_zmult1 zmod_zmult_zmult1 one_less_a2
1.88 +        simp add: mod_mult_mult1 one_less_a2
1.89                    div_pos_pos_trivial)
1.90  qed
1.91
1.92 @@ -961,7 +935,7 @@
1.93             then number_of v div (number_of w)
1.94             else (number_of v + (1::int)) div (number_of w))"
1.95  apply (simp only: number_of_eq numeral_simps UNIV_I split: split_if)
1.98  done
1.99
1.100
1.101 @@ -977,7 +951,7 @@
1.103                        pos_mod_bound)
1.105 -apply (simp add: zmod_zmult_zmult2 mod_pos_pos_trivial)
1.106 +apply (simp add: mod_mult_mult2 mod_pos_pos_trivial)
1.107  apply (rule mod_pos_pos_trivial)
1.108  apply (auto simp add: mod_pos_pos_trivial ring_distribs)
1.109  apply (subgoal_tac "0 \<le> b mod a", arith, simp)
1.110 @@ -998,7 +972,7 @@
1.111       "number_of (Int.Bit0 v) mod number_of (Int.Bit0 w) =
1.112        (2::int) * (number_of v mod number_of w)"
1.113  apply (simp only: number_of_eq numeral_simps)
1.114 -apply (simp add: zmod_zmult_zmult1 pos_zmod_mult_2
1.115 +apply (simp add: mod_mult_mult1 pos_zmod_mult_2
1.117  done
1.118
1.119 @@ -1008,7 +982,7 @@
1.120                  then 2 * (number_of v mod number_of w) + 1
1.121                  else 2 * ((number_of v + (1::int)) mod number_of w) - 1)"
1.122  apply (simp only: number_of_eq numeral_simps)
1.123 -apply (simp add: zmod_zmult_zmult1 pos_zmod_mult_2
1.124 +apply (simp add: mod_mult_mult1 pos_zmod_mult_2
1.126  done
1.127
1.128 @@ -1090,9 +1064,7 @@
1.129  done
1.130
1.131  lemma zdvd_zmod: "f dvd m ==> f dvd (n::int) ==> f dvd m mod n"
1.132 -  apply (simp add: dvd_def)
1.133 -  apply (auto simp add: zmod_zmult_zmult1)
1.134 -  done
1.135 +  by (auto elim!: dvdE simp add: mod_mult_mult1)
1.136
1.137  lemma zdvd_zmod_imp_zdvd: "k dvd m mod n ==> k dvd n ==> k dvd (m::int)"
1.138    apply (subgoal_tac "k dvd n * (m div n) + m mod n")
1.139 @@ -1247,9 +1219,9 @@
1.140  lemmas zmod_simps =