src/HOL/IntDiv.thy
changeset 27651 16a26996c30e
parent 26507 6da615cef733
child 27667 62500b980749
     1.1 --- a/src/HOL/IntDiv.thy	Fri Jul 18 17:09:48 2008 +0200
     1.2 +++ b/src/HOL/IntDiv.thy	Fri Jul 18 18:25:53 2008 +0200
     1.3 @@ -747,8 +747,49 @@
     1.4  lemma zdiv_zmult_self1 [simp]: "b \<noteq> (0::int) ==> (a*b) div b = a"
     1.5  by (simp add: zdiv_zmult1_eq)
     1.6  
     1.7 +lemma mod_div_trivial [simp]: "(a mod b) div b = (0::int)"
     1.8 +apply (case_tac "b = 0", simp)
     1.9 +apply (auto simp add: linorder_neq_iff div_pos_pos_trivial div_neg_neg_trivial)
    1.10 +done
    1.11 +
    1.12 +lemma mod_mod_trivial [simp]: "(a mod b) mod b = a mod (b::int)"
    1.13 +apply (case_tac "b = 0", simp)
    1.14 +apply (force simp add: linorder_neq_iff mod_pos_pos_trivial mod_neg_neg_trivial)
    1.15 +done
    1.16 +
    1.17 +text{*proving (a+b) div c = a div c + b div c + ((a mod c + b mod c) div c) *}
    1.18 +
    1.19 +lemma zadd1_lemma:
    1.20 +     "[| quorem((a,c),(aq,ar));  quorem((b,c),(bq,br));  c \<noteq> 0 |]  
    1.21 +      ==> quorem ((a+b, c), (aq + bq + (ar+br) div c, (ar+br) mod c))"
    1.22 +by (force simp add: split_ifs quorem_def linorder_neq_iff right_distrib)
    1.23 +
    1.24 +(*NOT suitable for rewriting: the RHS has an instance of the LHS*)
    1.25 +lemma zdiv_zadd1_eq:
    1.26 +     "(a+b) div (c::int) = a div c + b div c + ((a mod c + b mod c) div c)"
    1.27 +apply (case_tac "c = 0", simp)
    1.28 +apply (blast intro: zadd1_lemma [OF quorem_div_mod quorem_div_mod] quorem_div)
    1.29 +done
    1.30 +
    1.31 +lemma zmod_zadd1_eq: "(a+b) mod (c::int) = (a mod c + b mod c) mod c"
    1.32 +apply (case_tac "c = 0", simp)
    1.33 +apply (blast intro: zadd1_lemma [OF quorem_div_mod quorem_div_mod] quorem_mod)
    1.34 +done
    1.35 +
    1.36 +lemma zdiv_zadd_self1[simp]: "a \<noteq> (0::int) ==> (a+b) div a = b div a + 1"
    1.37 +by (simp add: zdiv_zadd1_eq)
    1.38 +
    1.39 +lemma zdiv_zadd_self2[simp]: "a \<noteq> (0::int) ==> (b+a) div a = b div a + 1"
    1.40 +by (simp add: zdiv_zadd1_eq)
    1.41 +
    1.42  instance int :: semiring_div
    1.43 -  by intro_classes auto
    1.44 +proof
    1.45 +  fix a b c :: int
    1.46 +  assume not0: "b \<noteq> 0"
    1.47 +  show "(a + c * b) div b = c + a div b"
    1.48 +    unfolding zdiv_zadd1_eq [of a "c * b"] using not0 
    1.49 +      by (simp add: zmod_zmult1_eq)
    1.50 +qed auto
    1.51  
    1.52  lemma zdiv_zmult_self2 [simp]: "b \<noteq> (0::int) ==> (b*a) div b = a"
    1.53  by (subst mult_commute, erule zdiv_zmult_self1)
    1.54 @@ -770,35 +811,6 @@
    1.55  
    1.56  lemmas zmod_eq_0D [dest!] = zmod_eq_0_iff [THEN iffD1]
    1.57  
    1.58 -text{*proving (a+b) div c = a div c + b div c + ((a mod c + b mod c) div c) *}
    1.59 -
    1.60 -lemma zadd1_lemma:
    1.61 -     "[| quorem((a,c),(aq,ar));  quorem((b,c),(bq,br));  c \<noteq> 0 |]  
    1.62 -      ==> quorem ((a+b, c), (aq + bq + (ar+br) div c, (ar+br) mod c))"
    1.63 -by (force simp add: split_ifs quorem_def linorder_neq_iff right_distrib)
    1.64 -
    1.65 -(*NOT suitable for rewriting: the RHS has an instance of the LHS*)
    1.66 -lemma zdiv_zadd1_eq:
    1.67 -     "(a+b) div (c::int) = a div c + b div c + ((a mod c + b mod c) div c)"
    1.68 -apply (case_tac "c = 0", simp)
    1.69 -apply (blast intro: zadd1_lemma [OF quorem_div_mod quorem_div_mod] quorem_div)
    1.70 -done
    1.71 -
    1.72 -lemma zmod_zadd1_eq: "(a+b) mod (c::int) = (a mod c + b mod c) mod c"
    1.73 -apply (case_tac "c = 0", simp)
    1.74 -apply (blast intro: zadd1_lemma [OF quorem_div_mod quorem_div_mod] quorem_mod)
    1.75 -done
    1.76 -
    1.77 -lemma mod_div_trivial [simp]: "(a mod b) div b = (0::int)"
    1.78 -apply (case_tac "b = 0", simp)
    1.79 -apply (auto simp add: linorder_neq_iff div_pos_pos_trivial div_neg_neg_trivial)
    1.80 -done
    1.81 -
    1.82 -lemma mod_mod_trivial [simp]: "(a mod b) mod b = a mod (b::int)"
    1.83 -apply (case_tac "b = 0", simp)
    1.84 -apply (force simp add: linorder_neq_iff mod_pos_pos_trivial mod_neg_neg_trivial)
    1.85 -done
    1.86 -
    1.87  lemma zmod_zadd_left_eq: "(a+b) mod (c::int) = ((a mod c) + b) mod c"
    1.88  apply (rule trans [symmetric])
    1.89  apply (rule zmod_zadd1_eq, simp)
    1.90 @@ -811,12 +823,6 @@
    1.91  apply (rule zmod_zadd1_eq [symmetric])
    1.92  done
    1.93  
    1.94 -lemma zdiv_zadd_self1[simp]: "a \<noteq> (0::int) ==> (a+b) div a = b div a + 1"
    1.95 -by (simp add: zdiv_zadd1_eq)
    1.96 -
    1.97 -lemma zdiv_zadd_self2[simp]: "a \<noteq> (0::int) ==> (b+a) div a = b div a + 1"
    1.98 -by (simp add: zdiv_zadd1_eq)
    1.99 -
   1.100  lemma zmod_zadd_self1[simp]: "(a+b) mod a = b mod (a::int)"
   1.101  apply (case_tac "a = 0", simp)
   1.102  apply (simp add: zmod_zadd1_eq)
   1.103 @@ -1183,33 +1189,36 @@
   1.104  lemma zdvd_trans: "m dvd n ==> n dvd k ==> m dvd (k::int)"
   1.105    by (auto simp add: dvd_def intro: mult_assoc)
   1.106  
   1.107 -lemma zdvd_zminus_iff: "(m dvd -n) = (m dvd (n::int))"
   1.108 -  apply (simp add: dvd_def, auto)
   1.109 -   apply (rule_tac [!] x = "-k" in exI, auto)
   1.110 -  done
   1.111 +lemma zdvd_zminus_iff: "m dvd -n \<longleftrightarrow> m dvd (n::int)"
   1.112 +proof
   1.113 +  assume "m dvd - n"
   1.114 +  then obtain k where "- n = m * k" ..
   1.115 +  then have "n = m * - k" by simp
   1.116 +  then show "m dvd n" ..
   1.117 +next
   1.118 +  assume "m dvd n"
   1.119 +  then have "m dvd n * -1" by (rule dvd_mult2)
   1.120 +  then show "m dvd - n" by simp
   1.121 +qed
   1.122  
   1.123 -lemma zdvd_zminus2_iff: "(-m dvd n) = (m dvd (n::int))"
   1.124 -  apply (simp add: dvd_def, auto)
   1.125 -   apply (rule_tac [!] x = "-k" in exI, auto)
   1.126 -  done
   1.127 +lemma zdvd_zminus2_iff: "-m dvd n \<longleftrightarrow> m dvd (n::int)"
   1.128 +proof
   1.129 +  assume "- m dvd n"
   1.130 +  then obtain k where "n = - m * k" ..
   1.131 +  then have "n = m * - k" by simp
   1.132 +  then show "m dvd n" ..
   1.133 +next
   1.134 +  assume "m dvd n"
   1.135 +  then obtain k where "n = m * k" ..
   1.136 +  then have "n = - m * - k" by simp
   1.137 +  then show "- m dvd n" ..
   1.138 +qed
   1.139 +
   1.140  lemma zdvd_abs1: "( \<bar>i::int\<bar> dvd j) = (i dvd j)" 
   1.141 -  apply (cases "i > 0", simp)
   1.142 -  apply (simp add: dvd_def)
   1.143 -  apply (rule iffI)
   1.144 -  apply (erule exE)
   1.145 -  apply (rule_tac x="- k" in exI, simp)
   1.146 -  apply (erule exE)
   1.147 -  apply (rule_tac x="- k" in exI, simp)
   1.148 -  done
   1.149 +  by (cases "i > 0") (simp_all add: zdvd_zminus2_iff)
   1.150 +
   1.151  lemma zdvd_abs2: "( (i::int) dvd \<bar>j\<bar>) = (i dvd j)" 
   1.152 -  apply (cases "j > 0", simp)
   1.153 -  apply (simp add: dvd_def)
   1.154 -  apply (rule iffI)
   1.155 -  apply (erule exE)
   1.156 -  apply (rule_tac x="- k" in exI, simp)
   1.157 -  apply (erule exE)
   1.158 -  apply (rule_tac x="- k" in exI, simp)
   1.159 -  done
   1.160 +  by (cases "j > 0") (simp_all add: zdvd_zminus_iff)
   1.161  
   1.162  lemma zdvd_anti_sym:
   1.163      "0 < m ==> 0 < n ==> m dvd n ==> n dvd m ==> m = (n::int)"
   1.164 @@ -1276,10 +1285,7 @@
   1.165    done
   1.166  
   1.167  lemma zdvd_zmult_mono: "i dvd m ==> j dvd (n::int) ==> i * j dvd m * n"
   1.168 -  apply (simp add: dvd_def, clarify)
   1.169 -  apply (rule_tac x = "k * ka" in exI)
   1.170 -  apply (simp add: mult_ac)
   1.171 -  done
   1.172 +  by (rule mult_dvd_mono)
   1.173  
   1.174  lemma zdvd_reduce: "(k dvd n + k * m) = (k dvd (n::int))"
   1.175    apply (rule iffI)
   1.176 @@ -1301,7 +1307,7 @@
   1.177    done
   1.178  
   1.179  lemma zdvd_not_zless: "0 < m ==> m < n ==> \<not> n dvd (m::int)"
   1.180 -  apply (simp add: dvd_def, auto)
   1.181 +  apply (auto elim!: dvdE)
   1.182    apply (subgoal_tac "0 < n")
   1.183     prefer 2
   1.184     apply (blast intro: order_less_trans)
   1.185 @@ -1309,6 +1315,7 @@
   1.186    apply (subgoal_tac "n * k < n * 1")
   1.187     apply (drule mult_less_cancel_left [THEN iffD1], auto)
   1.188    done
   1.189 +
   1.190  lemma zmult_div_cancel: "(n::int) * (m div n) = m - (m mod n)"
   1.191    using zmod_zdiv_equality[where a="m" and b="n"]
   1.192    by (simp add: ring_simps)
   1.193 @@ -1348,21 +1355,24 @@
   1.194  done
   1.195  
   1.196  theorem zdvd_int: "(x dvd y) = (int x dvd int y)"
   1.197 -apply (simp only: dvd_def ex_nat int_int_eq [symmetric] zmult_int [symmetric]
   1.198 -    nat_0_le cong add: conj_cong)
   1.199 -apply (rule iffI)
   1.200 -apply iprover
   1.201 -apply (erule exE)
   1.202 -apply (case_tac "x=0")
   1.203 -apply (rule_tac x=0 in exI)
   1.204 -apply simp
   1.205 -apply (case_tac "0 \<le> k")
   1.206 -apply iprover
   1.207 -apply (simp add: neq0_conv linorder_not_le)
   1.208 -apply (drule mult_strict_left_mono_neg [OF iffD2 [OF zero_less_int_conv]])
   1.209 -apply assumption
   1.210 -apply (simp add: mult_ac)
   1.211 -done
   1.212 +proof -
   1.213 +  have "\<And>k. int y = int x * k \<Longrightarrow> x dvd y"
   1.214 +  proof -
   1.215 +    fix k
   1.216 +    assume A: "int y = int x * k"
   1.217 +    then show "x dvd y" proof (cases k)
   1.218 +      case (1 n) with A have "y = x * n" by (simp add: zmult_int)
   1.219 +      then show ?thesis ..
   1.220 +    next
   1.221 +      case (2 n) with A have "int y = int x * (- int (Suc n))" by simp
   1.222 +      also have "\<dots> = - (int x * int (Suc n))" by (simp only: mult_minus_right)
   1.223 +      also have "\<dots> = - int (x * Suc n)" by (simp only: zmult_int)
   1.224 +      finally have "- int (x * Suc n) = int y" ..
   1.225 +      then show ?thesis by (simp only: negative_eq_positive) auto
   1.226 +    qed
   1.227 +  qed
   1.228 +  then show ?thesis by (auto elim!: dvdE simp only: zmult_int [symmetric])
   1.229 +qed 
   1.230  
   1.231  lemma zdvd1_eq[simp]: "(x::int) dvd 1 = ( \<bar>x\<bar> = 1)"
   1.232  proof
   1.233 @@ -1385,41 +1395,19 @@
   1.234  qed
   1.235  
   1.236  lemma int_dvd_iff: "(int m dvd z) = (m dvd nat (abs z))"
   1.237 -  apply (auto simp add: dvd_def nat_abs_mult_distrib)
   1.238 -  apply (auto simp add: nat_eq_iff abs_if split add: split_if_asm)
   1.239 -   apply (rule_tac x = "-(int k)" in exI)
   1.240 -  apply (auto simp add: int_mult)
   1.241 -  done
   1.242 +  unfolding zdvd_int by (cases "z \<ge> 0") (simp_all add: zdvd_zminus_iff)
   1.243  
   1.244  lemma dvd_int_iff: "(z dvd int m) = (nat (abs z) dvd m)"
   1.245 -  apply (auto simp add: dvd_def abs_if int_mult)
   1.246 -    apply (rule_tac [3] x = "nat k" in exI)
   1.247 -    apply (rule_tac [2] x = "-(int k)" in exI)
   1.248 -    apply (rule_tac x = "nat (-k)" in exI)
   1.249 -    apply (cut_tac [3] k = m in int_less_0_conv)
   1.250 -    apply (cut_tac k = m in int_less_0_conv)
   1.251 -    apply (auto simp add: zero_le_mult_iff mult_less_0_iff
   1.252 -      nat_mult_distrib [symmetric] nat_eq_iff2)
   1.253 -  done
   1.254 +  unfolding zdvd_int by (cases "z \<ge> 0") (simp_all add: zdvd_zminus2_iff)
   1.255  
   1.256  lemma nat_dvd_iff: "(nat z dvd m) = (if 0 \<le> z then (z dvd int m) else m = 0)"
   1.257 -  apply (auto simp add: dvd_def int_mult)
   1.258 -  apply (rule_tac x = "nat k" in exI)
   1.259 -  apply (cut_tac k = m in int_less_0_conv)
   1.260 -  apply (auto simp add: zero_le_mult_iff mult_less_0_iff
   1.261 -    nat_mult_distrib [symmetric] nat_eq_iff2)
   1.262 -  done
   1.263 +  by (auto simp add: dvd_int_iff)
   1.264  
   1.265  lemma zminus_dvd_iff [iff]: "(-z dvd w) = (z dvd (w::int))"
   1.266 -  apply (auto simp add: dvd_def)
   1.267 -   apply (rule_tac [!] x = "-k" in exI, auto)
   1.268 -  done
   1.269 +  by (simp add: zdvd_zminus2_iff)
   1.270  
   1.271  lemma dvd_zminus_iff [iff]: "(z dvd -w) = (z dvd (w::int))"
   1.272 -  apply (auto simp add: dvd_def)
   1.273 -   apply (drule minus_equation_iff [THEN iffD1])
   1.274 -   apply (rule_tac [!] x = "-k" in exI, auto)
   1.275 -  done
   1.276 +  by (simp add: zdvd_zminus_iff)
   1.277  
   1.278  lemma zdvd_imp_le: "[| z dvd n; 0 < n |] ==> z \<le> (n::int)"
   1.279    apply (rule_tac z=n in int_cases)