src/HOL/IntDiv.thy
changeset 30240 5b25fee0362c
parent 29951 a70bc5190534
child 30242 aea5d7fa7ef5
     1.1 --- a/src/HOL/IntDiv.thy	Wed Mar 04 10:43:39 2009 +0100
     1.2 +++ b/src/HOL/IntDiv.thy	Wed Mar 04 10:45:52 2009 +0100
     1.3 @@ -547,34 +547,6 @@
     1.4  simproc_setup binary_int_mod ("number_of m mod number_of n :: int") =
     1.5    {* K (divmod_proc (@{thm divmod_rel_mod_eq})) *}
     1.6  
     1.7 -(* The following 8 lemmas are made unnecessary by the above simprocs: *)
     1.8 -
     1.9 -lemmas div_pos_pos_number_of =
    1.10 -    div_pos_pos [of "number_of v" "number_of w", standard]
    1.11 -
    1.12 -lemmas div_neg_pos_number_of =
    1.13 -    div_neg_pos [of "number_of v" "number_of w", standard]
    1.14 -
    1.15 -lemmas div_pos_neg_number_of =
    1.16 -    div_pos_neg [of "number_of v" "number_of w", standard]
    1.17 -
    1.18 -lemmas div_neg_neg_number_of =
    1.19 -    div_neg_neg [of "number_of v" "number_of w", standard]
    1.20 -
    1.21 -
    1.22 -lemmas mod_pos_pos_number_of =
    1.23 -    mod_pos_pos [of "number_of v" "number_of w", standard]
    1.24 -
    1.25 -lemmas mod_neg_pos_number_of =
    1.26 -    mod_neg_pos [of "number_of v" "number_of w", standard]
    1.27 -
    1.28 -lemmas mod_pos_neg_number_of =
    1.29 -    mod_pos_neg [of "number_of v" "number_of w", standard]
    1.30 -
    1.31 -lemmas mod_neg_neg_number_of =
    1.32 -    mod_neg_neg [of "number_of v" "number_of w", standard]
    1.33 -
    1.34 -
    1.35  lemmas posDivAlg_eqn_number_of [simp] =
    1.36      posDivAlg_eqn [of "number_of v" "number_of w", standard]
    1.37  
    1.38 @@ -584,15 +556,6 @@
    1.39  
    1.40  text{*Special-case simplification *}
    1.41  
    1.42 -lemma zmod_1 [simp]: "a mod (1::int) = 0"
    1.43 -apply (cut_tac a = a and b = 1 in pos_mod_sign)
    1.44 -apply (cut_tac [2] a = a and b = 1 in pos_mod_bound)
    1.45 -apply (auto simp del:pos_mod_bound pos_mod_sign)
    1.46 -done
    1.47 -
    1.48 -lemma zdiv_1 [simp]: "a div (1::int) = a"
    1.49 -by (cut_tac a = a and b = 1 in zmod_zdiv_equality, auto)
    1.50 -
    1.51  lemma zmod_minus1_right [simp]: "a mod (-1::int) = 0"
    1.52  apply (cut_tac a = a and b = "-1" in neg_mod_sign)
    1.53  apply (cut_tac [2] a = a and b = "-1" in neg_mod_bound)
    1.54 @@ -726,9 +689,6 @@
    1.55  apply (blast intro: divmod_rel_div_mod [THEN zmult1_lemma, THEN divmod_rel_mod])
    1.56  done
    1.57  
    1.58 -lemma zdiv_zmult_self1 [simp]: "b \<noteq> (0::int) ==> (a*b) div b = a"
    1.59 -by (simp add: zdiv_zmult1_eq)
    1.60 -
    1.61  lemma zmod_zdiv_trivial: "(a mod b) div b = (0::int)"
    1.62  apply (case_tac "b = 0", simp)
    1.63  apply (auto simp add: linorder_neq_iff div_pos_pos_trivial div_neg_neg_trivial)
    1.64 @@ -754,7 +714,7 @@
    1.65    assume not0: "b \<noteq> 0"
    1.66    show "(a + c * b) div b = c + a div b"
    1.67      unfolding zdiv_zadd1_eq [of a "c * b"] using not0 
    1.68 -      by (simp add: zmod_zmult1_eq zmod_zdiv_trivial)
    1.69 +      by (simp add: zmod_zmult1_eq zmod_zdiv_trivial zdiv_zmult1_eq)
    1.70  qed auto
    1.71  
    1.72  lemma posDivAlg_div_mod:
    1.73 @@ -784,41 +744,12 @@
    1.74    show ?thesis by simp
    1.75  qed
    1.76  
    1.77 -lemma zdiv_zadd_self1: "a \<noteq> (0::int) ==> (a+b) div a = b div a + 1"
    1.78 -by (rule div_add_self1) (* already declared [simp] *)
    1.79 -
    1.80 -lemma zdiv_zadd_self2: "a \<noteq> (0::int) ==> (b+a) div a = b div a + 1"
    1.81 -by (rule div_add_self2) (* already declared [simp] *)
    1.82 -
    1.83 -lemma zdiv_zmult_self2: "b \<noteq> (0::int) ==> (b*a) div b = a"
    1.84 -by (rule div_mult_self1_is_id) (* already declared [simp] *)
    1.85 -
    1.86 -lemma zmod_zmult_self1: "(a*b) mod b = (0::int)"
    1.87 -by (rule mod_mult_self2_is_0) (* already declared [simp] *)
    1.88 -
    1.89 -lemma zmod_zmult_self2: "(b*a) mod b = (0::int)"
    1.90 -by (rule mod_mult_self1_is_0) (* already declared [simp] *)
    1.91 -
    1.92  lemma zmod_eq_0_iff: "(m mod d = 0) = (EX q::int. m = d*q)"
    1.93  by (simp add: dvd_eq_mod_eq_0 [symmetric] dvd_def)
    1.94  
    1.95  (* REVISIT: should this be generalized to all semiring_div types? *)
    1.96  lemmas zmod_eq_0D [dest!] = zmod_eq_0_iff [THEN iffD1]
    1.97  
    1.98 -lemma zmod_zadd_left_eq: "(a+b) mod (c::int) = ((a mod c) + b) mod c"
    1.99 -by (rule mod_add_left_eq)
   1.100 -
   1.101 -lemma zmod_zadd_right_eq: "(a+b) mod (c::int) = (a + (b mod c)) mod c"
   1.102 -by (rule mod_add_right_eq)
   1.103 -
   1.104 -lemma zmod_zadd_self1: "(a+b) mod a = b mod (a::int)"
   1.105 -by (rule mod_add_self1) (* already declared [simp] *)
   1.106 -
   1.107 -lemma zmod_zadd_self2: "(b+a) mod a = b mod (a::int)"
   1.108 -by (rule mod_add_self2) (* already declared [simp] *)
   1.109 -
   1.110 -lemma zmod_zdiff1_eq: "(a - b) mod c = (a mod c - b mod c) mod (c::int)"
   1.111 -by (rule mod_diff_eq)
   1.112  
   1.113  subsection{*Proving  @{term "a div (b*c) = (a div b) div c"} *}
   1.114  
   1.115 @@ -902,13 +833,6 @@
   1.116    "(k*m) div (k*n) = (if k = (0::int) then 0 else m div n)"
   1.117  by (simp add:zdiv_zmult_zmult1)
   1.118  
   1.119 -(*
   1.120 -lemma zdiv_zmult_zmult2: "c \<noteq> (0::int) ==> (a*c) div (b*c) = a div b"
   1.121 -apply (drule zdiv_zmult_zmult1)
   1.122 -apply (auto simp add: mult_commute)
   1.123 -done
   1.124 -*)
   1.125 -
   1.126  
   1.127  subsection{*Distribution of Factors over mod*}
   1.128  
   1.129 @@ -933,9 +857,6 @@
   1.130  apply (auto simp add: mult_commute)
   1.131  done
   1.132  
   1.133 -lemma zmod_zmod_cancel: "n dvd m \<Longrightarrow> (k::int) mod m mod n = k mod n"
   1.134 -by (rule mod_mod_cancel)
   1.135 -
   1.136  
   1.137  subsection {*Splitting Rules for div and mod*}
   1.138  
   1.139 @@ -1070,7 +991,7 @@
   1.140  apply (subgoal_tac "(1 + 2* (-b - 1)) mod (2* (-a)) = 
   1.141                      1 + 2* ((-b - 1) mod (-a))")
   1.142  apply (rule_tac [2] pos_zmod_mult_2)
   1.143 -apply (auto simp add: minus_mult_right [symmetric] right_diff_distrib)
   1.144 +apply (auto simp add: right_diff_distrib)
   1.145  apply (subgoal_tac " (-1 - (2 * b)) = - (1 + (2 * b))")
   1.146   prefer 2 apply simp 
   1.147  apply (simp only: zmod_zminus_zminus diff_minus minus_add_distrib [symmetric])
   1.148 @@ -1132,38 +1053,8 @@
   1.149  
   1.150  subsection {* The Divides Relation *}
   1.151  
   1.152 -lemma zdvd_iff_zmod_eq_0: "(m dvd n) = (n mod m = (0::int))"
   1.153 -  by (rule dvd_eq_mod_eq_0)
   1.154 -
   1.155  lemmas zdvd_iff_zmod_eq_0_number_of [simp] =
   1.156 -  zdvd_iff_zmod_eq_0 [of "number_of x" "number_of y", standard]
   1.157 -
   1.158 -lemma zdvd_0_right: "(m::int) dvd 0"
   1.159 -  by (rule dvd_0_right) (* already declared [iff] *)
   1.160 -
   1.161 -lemma zdvd_0_left: "(0 dvd (m::int)) = (m = 0)"
   1.162 -  by (rule dvd_0_left_iff) (* already declared [noatp,simp] *)
   1.163 -
   1.164 -lemma zdvd_1_left: "1 dvd (m::int)"
   1.165 -  by (rule one_dvd) (* already declared [simp] *)
   1.166 -
   1.167 -lemma zdvd_refl: "m dvd (m::int)"
   1.168 -  by (rule dvd_refl) (* already declared [simp] *)
   1.169 -
   1.170 -lemma zdvd_trans: "m dvd n ==> n dvd k ==> m dvd (k::int)"
   1.171 -  by (rule dvd_trans)
   1.172 -
   1.173 -lemma zdvd_zminus_iff: "m dvd -n \<longleftrightarrow> m dvd (n::int)"
   1.174 -  by (rule dvd_minus_iff) (* already declared [simp] *)
   1.175 -
   1.176 -lemma zdvd_zminus2_iff: "-m dvd n \<longleftrightarrow> m dvd (n::int)"
   1.177 -  by (rule minus_dvd_iff) (* already declared [simp] *)
   1.178 -
   1.179 -lemma zdvd_abs1: "( \<bar>i::int\<bar> dvd j) = (i dvd j)"
   1.180 -  by (rule abs_dvd_iff) (* already declared [simp] *)
   1.181 -
   1.182 -lemma zdvd_abs2: "( (i::int) dvd \<bar>j\<bar>) = (i dvd j)" 
   1.183 -  by (rule dvd_abs_iff) (* already declared [simp] *)
   1.184 +  dvd_eq_mod_eq_0 [of "number_of x::int" "number_of y::int", standard]
   1.185  
   1.186  lemma zdvd_anti_sym:
   1.187      "0 < m ==> 0 < n ==> m dvd n ==> n dvd m ==> m = (n::int)"
   1.188 @@ -1171,58 +1062,32 @@
   1.189    apply (simp add: mult_assoc zero_less_mult_iff zmult_eq_1_iff)
   1.190    done
   1.191  
   1.192 -lemma zdvd_zadd: "k dvd m ==> k dvd n ==> k dvd (m + n :: int)"
   1.193 -  by (rule dvd_add)
   1.194 -
   1.195 -lemma zdvd_dvd_eq: assumes anz:"a \<noteq> 0" and ab: "(a::int) dvd b" and ba:"b dvd a" 
   1.196 +lemma zdvd_dvd_eq: assumes "a \<noteq> 0" and "(a::int) dvd b" and "b dvd a" 
   1.197    shows "\<bar>a\<bar> = \<bar>b\<bar>"
   1.198  proof-
   1.199 -  from ab obtain k where k:"b = a*k" unfolding dvd_def by blast 
   1.200 -  from ba obtain k' where k':"a = b*k'" unfolding dvd_def by blast 
   1.201 +  from `a dvd b` obtain k where k:"b = a*k" unfolding dvd_def by blast 
   1.202 +  from `b dvd a` obtain k' where k':"a = b*k'" unfolding dvd_def by blast 
   1.203    from k k' have "a = a*k*k'" by simp
   1.204    with mult_cancel_left1[where c="a" and b="k*k'"]
   1.205 -  have kk':"k*k' = 1" using anz by (simp add: mult_assoc)
   1.206 +  have kk':"k*k' = 1" using `a\<noteq>0` by (simp add: mult_assoc)
   1.207    hence "k = 1 \<and> k' = 1 \<or> k = -1 \<and> k' = -1" by (simp add: zmult_eq_1_iff)
   1.208    thus ?thesis using k k' by auto
   1.209  qed
   1.210  
   1.211 -lemma zdvd_zdiff: "k dvd m ==> k dvd n ==> k dvd (m - n :: int)"
   1.212 -  by (rule Ring_and_Field.dvd_diff)
   1.213 -
   1.214  lemma zdvd_zdiffD: "k dvd m - n ==> k dvd n ==> k dvd (m::int)"
   1.215    apply (subgoal_tac "m = n + (m - n)")
   1.216     apply (erule ssubst)
   1.217 -   apply (blast intro: zdvd_zadd, simp)
   1.218 +   apply (blast intro: dvd_add, simp)
   1.219    done
   1.220  
   1.221 -lemma zdvd_zmult: "k dvd (n::int) ==> k dvd m * n"
   1.222 -  by (rule dvd_mult)
   1.223 -
   1.224 -lemma zdvd_zmult2: "k dvd (m::int) ==> k dvd m * n"
   1.225 -  by (rule dvd_mult2)
   1.226 -
   1.227 -lemma zdvd_triv_right: "(k::int) dvd m * k"
   1.228 -  by (rule dvd_triv_right) (* already declared [simp] *)
   1.229 -
   1.230 -lemma zdvd_triv_left: "(k::int) dvd k * m"
   1.231 -  by (rule dvd_triv_left) (* already declared [simp] *)
   1.232 -
   1.233 -lemma zdvd_zmultD2: "j * k dvd n ==> j dvd (n::int)"
   1.234 -  by (rule dvd_mult_left)
   1.235 -
   1.236 -lemma zdvd_zmultD: "j * k dvd n ==> k dvd (n::int)"
   1.237 -  by (rule dvd_mult_right)
   1.238 -
   1.239 -lemma zdvd_zmult_mono: "i dvd m ==> j dvd (n::int) ==> i * j dvd m * n"
   1.240 -  by (rule mult_dvd_mono)
   1.241 -
   1.242  lemma zdvd_reduce: "(k dvd n + k * m) = (k dvd (n::int))"
   1.243 -  apply (rule iffI)
   1.244 -   apply (erule_tac [2] zdvd_zadd)
   1.245 -   apply (subgoal_tac "n = (n + k * m) - k * m")
   1.246 -    apply (erule ssubst)
   1.247 -    apply (erule zdvd_zdiff, simp_all)
   1.248 -  done
   1.249 +apply (rule iffI)
   1.250 + apply (erule_tac [2] dvd_add)
   1.251 + apply (subgoal_tac "n = (n + k * m) - k * m")
   1.252 +  apply (erule ssubst)
   1.253 +  apply (erule dvd_diff)
   1.254 +  apply(simp_all)
   1.255 +done
   1.256  
   1.257  lemma zdvd_zmod: "f dvd m ==> f dvd (n::int) ==> f dvd m mod n"
   1.258    apply (simp add: dvd_def)
   1.259 @@ -1232,7 +1097,7 @@
   1.260  lemma zdvd_zmod_imp_zdvd: "k dvd m mod n ==> k dvd n ==> k dvd (m::int)"
   1.261    apply (subgoal_tac "k dvd n * (m div n) + m mod n")
   1.262     apply (simp add: zmod_zdiv_equality [symmetric])
   1.263 -  apply (simp only: zdvd_zadd zdvd_zmult2)
   1.264 +  apply (simp only: dvd_add dvd_mult2)
   1.265    done
   1.266  
   1.267  lemma zdvd_not_zless: "0 < m ==> m < n ==> \<not> n dvd (m::int)"
   1.268 @@ -1252,7 +1117,7 @@
   1.269  lemma zdvd_mult_div_cancel:"(n::int) dvd m \<Longrightarrow> n * (m div n) = m"
   1.270  apply (subgoal_tac "m mod n = 0")
   1.271   apply (simp add: zmult_div_cancel)
   1.272 -apply (simp only: zdvd_iff_zmod_eq_0)
   1.273 +apply (simp only: dvd_eq_mod_eq_0)
   1.274  done
   1.275  
   1.276  lemma zdvd_mult_cancel: assumes d:"k * m dvd k * n" and kz:"k \<noteq> (0::int)"
   1.277 @@ -1265,10 +1130,6 @@
   1.278    thus ?thesis by simp
   1.279  qed
   1.280  
   1.281 -lemma zdvd_zmult_cancel_disj[simp]:
   1.282 -  "(k*m) dvd (k*n) = (k=0 | m dvd (n::int))"
   1.283 -by (auto simp: zdvd_zmult_mono dest: zdvd_mult_cancel)
   1.284 -
   1.285  
   1.286  theorem ex_nat: "(\<exists>x::nat. P x) = (\<exists>x::int. 0 <= x \<and> P (nat x))"
   1.287  apply (simp split add: split_nat)
   1.288 @@ -1300,44 +1161,38 @@
   1.289        then show ?thesis by (simp only: negative_eq_positive) auto
   1.290      qed
   1.291    qed
   1.292 -  then show ?thesis by (auto elim!: dvdE simp only: zdvd_triv_left int_mult)
   1.293 +  then show ?thesis by (auto elim!: dvdE simp only: dvd_triv_left int_mult)
   1.294  qed
   1.295  
   1.296  lemma zdvd1_eq[simp]: "(x::int) dvd 1 = ( \<bar>x\<bar> = 1)"
   1.297  proof
   1.298 -  assume d: "x dvd 1" hence "int (nat \<bar>x\<bar>) dvd int (nat 1)" by (simp add: zdvd_abs1)
   1.299 +  assume d: "x dvd 1" hence "int (nat \<bar>x\<bar>) dvd int (nat 1)" by simp
   1.300    hence "nat \<bar>x\<bar> dvd 1" by (simp add: zdvd_int)
   1.301    hence "nat \<bar>x\<bar> = 1"  by simp
   1.302    thus "\<bar>x\<bar> = 1" by (cases "x < 0", auto)
   1.303  next
   1.304    assume "\<bar>x\<bar>=1" thus "x dvd 1" 
   1.305 -    by(cases "x < 0",simp_all add: minus_equation_iff zdvd_iff_zmod_eq_0)
   1.306 +    by(cases "x < 0",simp_all add: minus_equation_iff dvd_eq_mod_eq_0)
   1.307  qed
   1.308  lemma zdvd_mult_cancel1: 
   1.309    assumes mp:"m \<noteq>(0::int)" shows "(m * n dvd m) = (\<bar>n\<bar> = 1)"
   1.310  proof
   1.311    assume n1: "\<bar>n\<bar> = 1" thus "m * n dvd m" 
   1.312 -    by (cases "n >0", auto simp add: zdvd_zminus2_iff minus_equation_iff)
   1.313 +    by (cases "n >0", auto simp add: minus_dvd_iff minus_equation_iff)
   1.314  next
   1.315    assume H: "m * n dvd m" hence H2: "m * n dvd m * 1" by simp
   1.316    from zdvd_mult_cancel[OF H2 mp] show "\<bar>n\<bar> = 1" by (simp only: zdvd1_eq)
   1.317  qed
   1.318  
   1.319  lemma int_dvd_iff: "(int m dvd z) = (m dvd nat (abs z))"
   1.320 -  unfolding zdvd_int by (cases "z \<ge> 0") (simp_all add: zdvd_zminus_iff)
   1.321 +  unfolding zdvd_int by (cases "z \<ge> 0") simp_all
   1.322  
   1.323  lemma dvd_int_iff: "(z dvd int m) = (nat (abs z) dvd m)"
   1.324 -  unfolding zdvd_int by (cases "z \<ge> 0") (simp_all add: zdvd_zminus2_iff)
   1.325 +  unfolding zdvd_int by (cases "z \<ge> 0") simp_all
   1.326  
   1.327  lemma nat_dvd_iff: "(nat z dvd m) = (if 0 \<le> z then (z dvd int m) else m = 0)"
   1.328    by (auto simp add: dvd_int_iff)
   1.329  
   1.330 -lemma zminus_dvd_iff [iff]: "(-z dvd w) = (z dvd (w::int))"
   1.331 -  by (rule minus_dvd_iff)
   1.332 -
   1.333 -lemma dvd_zminus_iff [iff]: "(z dvd -w) = (z dvd (w::int))"
   1.334 -  by (rule dvd_minus_iff)
   1.335 -
   1.336  lemma zdvd_imp_le: "[| z dvd n; 0 < n |] ==> z \<le> (n::int)"
   1.337    apply (rule_tac z=n in int_cases)
   1.338    apply (auto simp add: dvd_int_iff)
   1.339 @@ -1367,10 +1222,13 @@
   1.340  apply (auto simp add: IntDiv.divmod_rel_def of_nat_mult)
   1.341  done
   1.342  
   1.343 +lemma abs_div: "(y::int) dvd x \<Longrightarrow> abs (x div y) = abs x div abs y"
   1.344 +by (unfold dvd_def, cases "y=0", auto simp add: abs_mult)
   1.345 +
   1.346  text{*Suggested by Matthias Daum*}
   1.347  lemma int_power_div_base:
   1.348       "\<lbrakk>0 < m; 0 < k\<rbrakk> \<Longrightarrow> k ^ m div k = (k::int) ^ (m - Suc 0)"
   1.349 -apply (subgoal_tac "k ^ m = k ^ ((m - 1) + 1)")
   1.350 +apply (subgoal_tac "k ^ m = k ^ ((m - Suc 0) + Suc 0)")
   1.351   apply (erule ssubst)
   1.352   apply (simp only: power_add)
   1.353   apply simp_all
   1.354 @@ -1387,8 +1245,8 @@
   1.355  by (rule mod_diff_right_eq [symmetric])
   1.356  
   1.357  lemmas zmod_simps =
   1.358 -  IntDiv.zmod_zadd_left_eq  [symmetric]
   1.359 -  IntDiv.zmod_zadd_right_eq [symmetric]
   1.360 +  mod_add_left_eq  [symmetric]
   1.361 +  mod_add_right_eq [symmetric]
   1.362    IntDiv.zmod_zmult1_eq     [symmetric]
   1.363    mod_mult_left_eq          [symmetric]
   1.364    IntDiv.zpower_zmod
   1.365 @@ -1463,14 +1321,14 @@
   1.366    assume H: "x mod n = y mod n"
   1.367    hence "x mod n - y mod n = 0" by simp
   1.368    hence "(x mod n - y mod n) mod n = 0" by simp 
   1.369 -  hence "(x - y) mod n = 0" by (simp add: zmod_zdiff1_eq[symmetric])
   1.370 -  thus "n dvd x - y" by (simp add: zdvd_iff_zmod_eq_0)
   1.371 +  hence "(x - y) mod n = 0" by (simp add: mod_diff_eq[symmetric])
   1.372 +  thus "n dvd x - y" by (simp add: dvd_eq_mod_eq_0)
   1.373  next
   1.374    assume H: "n dvd x - y"
   1.375    then obtain k where k: "x-y = n*k" unfolding dvd_def by blast
   1.376    hence "x = n*k + y" by simp
   1.377    hence "x mod n = (n*k + y) mod n" by simp
   1.378 -  thus "x mod n = y mod n" by (simp add: zmod_zadd_left_eq)
   1.379 +  thus "x mod n = y mod n" by (simp add: mod_add_left_eq)
   1.380  qed
   1.381  
   1.382  lemma nat_mod_eq_lemma: assumes xyn: "(x::nat) mod n = y  mod n" and xy:"y \<le> x"