src/HOL/IntDiv.thy
changeset 30042 31039ee583fa
parent 30034 60f64f112174
child 30079 293b896b9c25
     1.1 --- a/src/HOL/IntDiv.thy	Sat Feb 21 09:58:45 2009 +0100
     1.2 +++ b/src/HOL/IntDiv.thy	Sat Feb 21 20:52:30 2009 +0100
     1.3 @@ -836,13 +836,6 @@
     1.4    "(k*m) div (k*n) = (if k = (0::int) then 0 else m div n)"
     1.5  by (simp add:zdiv_zmult_zmult1)
     1.6  
     1.7 -(*
     1.8 -lemma zdiv_zmult_zmult2: "c \<noteq> (0::int) ==> (a*c) div (b*c) = a div b"
     1.9 -apply (drule zdiv_zmult_zmult1)
    1.10 -apply (auto simp add: mult_commute)
    1.11 -done
    1.12 -*)
    1.13 -
    1.14  
    1.15  subsection{*Distribution of Factors over mod*}
    1.16  
    1.17 @@ -1001,7 +994,7 @@
    1.18  apply (subgoal_tac "(1 + 2* (-b - 1)) mod (2* (-a)) = 
    1.19                      1 + 2* ((-b - 1) mod (-a))")
    1.20  apply (rule_tac [2] pos_zmod_mult_2)
    1.21 -apply (auto simp add: minus_mult_right [symmetric] right_diff_distrib)
    1.22 +apply (auto simp add: right_diff_distrib)
    1.23  apply (subgoal_tac " (-1 - (2 * b)) = - (1 + (2 * b))")
    1.24   prefer 2 apply simp 
    1.25  apply (simp only: zmod_zminus_zminus diff_minus minus_add_distrib [symmetric])
    1.26 @@ -1063,38 +1056,8 @@
    1.27  
    1.28  subsection {* The Divides Relation *}
    1.29  
    1.30 -lemma zdvd_iff_zmod_eq_0: "(m dvd n) = (n mod m = (0::int))"
    1.31 -  by (rule dvd_eq_mod_eq_0)
    1.32 -
    1.33  lemmas zdvd_iff_zmod_eq_0_number_of [simp] =
    1.34 -  zdvd_iff_zmod_eq_0 [of "number_of x" "number_of y", standard]
    1.35 -
    1.36 -lemma zdvd_0_right: "(m::int) dvd 0"
    1.37 -  by (rule dvd_0_right) (* already declared [iff] *)
    1.38 -
    1.39 -lemma zdvd_0_left: "(0 dvd (m::int)) = (m = 0)"
    1.40 -  by (rule dvd_0_left_iff) (* already declared [noatp,simp] *)
    1.41 -
    1.42 -lemma zdvd_1_left: "1 dvd (m::int)"
    1.43 -  by (rule one_dvd) (* already declared [simp] *)
    1.44 -
    1.45 -lemma zdvd_refl: "m dvd (m::int)"
    1.46 -  by (rule dvd_refl) (* already declared [simp] *)
    1.47 -
    1.48 -lemma zdvd_trans: "m dvd n ==> n dvd k ==> m dvd (k::int)"
    1.49 -  by (rule dvd_trans)
    1.50 -
    1.51 -lemma zdvd_zminus_iff: "m dvd -n \<longleftrightarrow> m dvd (n::int)"
    1.52 -  by (rule dvd_minus_iff) (* already declared [simp] *)
    1.53 -
    1.54 -lemma zdvd_zminus2_iff: "-m dvd n \<longleftrightarrow> m dvd (n::int)"
    1.55 -  by (rule minus_dvd_iff) (* already declared [simp] *)
    1.56 -
    1.57 -lemma zdvd_abs1: "( \<bar>i::int\<bar> dvd j) = (i dvd j)"
    1.58 -  by (rule abs_dvd_iff) (* already declared [simp] *)
    1.59 -
    1.60 -lemma zdvd_abs2: "( (i::int) dvd \<bar>j\<bar>) = (i dvd j)" 
    1.61 -  by (rule dvd_abs_iff) (* already declared [simp] *)
    1.62 +  dvd_eq_mod_eq_0 [of "number_of x::int" "number_of y::int", standard]
    1.63  
    1.64  lemma zdvd_anti_sym:
    1.65      "0 < m ==> 0 < n ==> m dvd n ==> n dvd m ==> m = (n::int)"
    1.66 @@ -1102,58 +1065,32 @@
    1.67    apply (simp add: mult_assoc zero_less_mult_iff zmult_eq_1_iff)
    1.68    done
    1.69  
    1.70 -lemma zdvd_zadd: "k dvd m ==> k dvd n ==> k dvd (m + n :: int)"
    1.71 -  by (rule dvd_add)
    1.72 -
    1.73 -lemma zdvd_dvd_eq: assumes anz:"a \<noteq> 0" and ab: "(a::int) dvd b" and ba:"b dvd a" 
    1.74 +lemma zdvd_dvd_eq: assumes "a \<noteq> 0" and "(a::int) dvd b" and "b dvd a" 
    1.75    shows "\<bar>a\<bar> = \<bar>b\<bar>"
    1.76  proof-
    1.77 -  from ab obtain k where k:"b = a*k" unfolding dvd_def by blast 
    1.78 -  from ba obtain k' where k':"a = b*k'" unfolding dvd_def by blast 
    1.79 +  from `a dvd b` obtain k where k:"b = a*k" unfolding dvd_def by blast 
    1.80 +  from `b dvd a` obtain k' where k':"a = b*k'" unfolding dvd_def by blast 
    1.81    from k k' have "a = a*k*k'" by simp
    1.82    with mult_cancel_left1[where c="a" and b="k*k'"]
    1.83 -  have kk':"k*k' = 1" using anz by (simp add: mult_assoc)
    1.84 +  have kk':"k*k' = 1" using `a\<noteq>0` by (simp add: mult_assoc)
    1.85    hence "k = 1 \<and> k' = 1 \<or> k = -1 \<and> k' = -1" by (simp add: zmult_eq_1_iff)
    1.86    thus ?thesis using k k' by auto
    1.87  qed
    1.88  
    1.89 -lemma zdvd_zdiff: "k dvd m ==> k dvd n ==> k dvd (m - n :: int)"
    1.90 -  by (rule Ring_and_Field.dvd_diff)
    1.91 -
    1.92  lemma zdvd_zdiffD: "k dvd m - n ==> k dvd n ==> k dvd (m::int)"
    1.93    apply (subgoal_tac "m = n + (m - n)")
    1.94     apply (erule ssubst)
    1.95 -   apply (blast intro: zdvd_zadd, simp)
    1.96 +   apply (blast intro: dvd_add, simp)
    1.97    done
    1.98  
    1.99 -lemma zdvd_zmult: "k dvd (n::int) ==> k dvd m * n"
   1.100 -  by (rule dvd_mult)
   1.101 -
   1.102 -lemma zdvd_zmult2: "k dvd (m::int) ==> k dvd m * n"
   1.103 -  by (rule dvd_mult2)
   1.104 -
   1.105 -lemma zdvd_triv_right: "(k::int) dvd m * k"
   1.106 -  by (rule dvd_triv_right) (* already declared [simp] *)
   1.107 -
   1.108 -lemma zdvd_triv_left: "(k::int) dvd k * m"
   1.109 -  by (rule dvd_triv_left) (* already declared [simp] *)
   1.110 -
   1.111 -lemma zdvd_zmultD2: "j * k dvd n ==> j dvd (n::int)"
   1.112 -  by (rule dvd_mult_left)
   1.113 -
   1.114 -lemma zdvd_zmultD: "j * k dvd n ==> k dvd (n::int)"
   1.115 -  by (rule dvd_mult_right)
   1.116 -
   1.117 -lemma zdvd_zmult_mono: "i dvd m ==> j dvd (n::int) ==> i * j dvd m * n"
   1.118 -  by (rule mult_dvd_mono)
   1.119 -
   1.120  lemma zdvd_reduce: "(k dvd n + k * m) = (k dvd (n::int))"
   1.121 -  apply (rule iffI)
   1.122 -   apply (erule_tac [2] zdvd_zadd)
   1.123 -   apply (subgoal_tac "n = (n + k * m) - k * m")
   1.124 -    apply (erule ssubst)
   1.125 -    apply (erule zdvd_zdiff, simp_all)
   1.126 -  done
   1.127 +apply (rule iffI)
   1.128 + apply (erule_tac [2] dvd_add)
   1.129 + apply (subgoal_tac "n = (n + k * m) - k * m")
   1.130 +  apply (erule ssubst)
   1.131 +  apply (erule dvd_diff)
   1.132 +  apply(simp_all)
   1.133 +done
   1.134  
   1.135  lemma zdvd_zmod: "f dvd m ==> f dvd (n::int) ==> f dvd m mod n"
   1.136    apply (simp add: dvd_def)
   1.137 @@ -1163,7 +1100,7 @@
   1.138  lemma zdvd_zmod_imp_zdvd: "k dvd m mod n ==> k dvd n ==> k dvd (m::int)"
   1.139    apply (subgoal_tac "k dvd n * (m div n) + m mod n")
   1.140     apply (simp add: zmod_zdiv_equality [symmetric])
   1.141 -  apply (simp only: zdvd_zadd zdvd_zmult2)
   1.142 +  apply (simp only: dvd_add dvd_mult2)
   1.143    done
   1.144  
   1.145  lemma zdvd_not_zless: "0 < m ==> m < n ==> \<not> n dvd (m::int)"
   1.146 @@ -1183,7 +1120,7 @@
   1.147  lemma zdvd_mult_div_cancel:"(n::int) dvd m \<Longrightarrow> n * (m div n) = m"
   1.148  apply (subgoal_tac "m mod n = 0")
   1.149   apply (simp add: zmult_div_cancel)
   1.150 -apply (simp only: zdvd_iff_zmod_eq_0)
   1.151 +apply (simp only: dvd_eq_mod_eq_0)
   1.152  done
   1.153  
   1.154  lemma zdvd_mult_cancel: assumes d:"k * m dvd k * n" and kz:"k \<noteq> (0::int)"
   1.155 @@ -1196,10 +1133,6 @@
   1.156    thus ?thesis by simp
   1.157  qed
   1.158  
   1.159 -lemma zdvd_zmult_cancel_disj:
   1.160 -  "(k*m) dvd (k*n) = (k=0 | m dvd (n::int))"
   1.161 -by (rule dvd_mult_cancel_left) (* already declared [simp] *)
   1.162 -
   1.163  
   1.164  theorem ex_nat: "(\<exists>x::nat. P x) = (\<exists>x::int. 0 <= x \<and> P (nat x))"
   1.165  apply (simp split add: split_nat)
   1.166 @@ -1231,44 +1164,38 @@
   1.167        then show ?thesis by (simp only: negative_eq_positive) auto
   1.168      qed
   1.169    qed
   1.170 -  then show ?thesis by (auto elim!: dvdE simp only: zdvd_triv_left int_mult)
   1.171 +  then show ?thesis by (auto elim!: dvdE simp only: dvd_triv_left int_mult)
   1.172  qed
   1.173  
   1.174  lemma zdvd1_eq[simp]: "(x::int) dvd 1 = ( \<bar>x\<bar> = 1)"
   1.175  proof
   1.176 -  assume d: "x dvd 1" hence "int (nat \<bar>x\<bar>) dvd int (nat 1)" by (simp add: zdvd_abs1)
   1.177 +  assume d: "x dvd 1" hence "int (nat \<bar>x\<bar>) dvd int (nat 1)" by simp
   1.178    hence "nat \<bar>x\<bar> dvd 1" by (simp add: zdvd_int)
   1.179    hence "nat \<bar>x\<bar> = 1"  by simp
   1.180    thus "\<bar>x\<bar> = 1" by (cases "x < 0", auto)
   1.181  next
   1.182    assume "\<bar>x\<bar>=1" thus "x dvd 1" 
   1.183 -    by(cases "x < 0",simp_all add: minus_equation_iff zdvd_iff_zmod_eq_0)
   1.184 +    by(cases "x < 0",simp_all add: minus_equation_iff dvd_eq_mod_eq_0)
   1.185  qed
   1.186  lemma zdvd_mult_cancel1: 
   1.187    assumes mp:"m \<noteq>(0::int)" shows "(m * n dvd m) = (\<bar>n\<bar> = 1)"
   1.188  proof
   1.189    assume n1: "\<bar>n\<bar> = 1" thus "m * n dvd m" 
   1.190 -    by (cases "n >0", auto simp add: zdvd_zminus2_iff minus_equation_iff)
   1.191 +    by (cases "n >0", auto simp add: minus_dvd_iff minus_equation_iff)
   1.192  next
   1.193    assume H: "m * n dvd m" hence H2: "m * n dvd m * 1" by simp
   1.194    from zdvd_mult_cancel[OF H2 mp] show "\<bar>n\<bar> = 1" by (simp only: zdvd1_eq)
   1.195  qed
   1.196  
   1.197  lemma int_dvd_iff: "(int m dvd z) = (m dvd nat (abs z))"
   1.198 -  unfolding zdvd_int by (cases "z \<ge> 0") (simp_all add: zdvd_zminus_iff)
   1.199 +  unfolding zdvd_int by (cases "z \<ge> 0") simp_all
   1.200  
   1.201  lemma dvd_int_iff: "(z dvd int m) = (nat (abs z) dvd m)"
   1.202 -  unfolding zdvd_int by (cases "z \<ge> 0") (simp_all add: zdvd_zminus2_iff)
   1.203 +  unfolding zdvd_int by (cases "z \<ge> 0") simp_all
   1.204  
   1.205  lemma nat_dvd_iff: "(nat z dvd m) = (if 0 \<le> z then (z dvd int m) else m = 0)"
   1.206    by (auto simp add: dvd_int_iff)
   1.207  
   1.208 -lemma zminus_dvd_iff [iff]: "(-z dvd w) = (z dvd (w::int))"
   1.209 -  by (rule minus_dvd_iff)
   1.210 -
   1.211 -lemma dvd_zminus_iff [iff]: "(z dvd -w) = (z dvd (w::int))"
   1.212 -  by (rule dvd_minus_iff)
   1.213 -
   1.214  lemma zdvd_imp_le: "[| z dvd n; 0 < n |] ==> z \<le> (n::int)"
   1.215    apply (rule_tac z=n in int_cases)
   1.216    apply (auto simp add: dvd_int_iff)
   1.217 @@ -1395,7 +1322,7 @@
   1.218    hence "x mod n - y mod n = 0" by simp
   1.219    hence "(x mod n - y mod n) mod n = 0" by simp 
   1.220    hence "(x - y) mod n = 0" by (simp add: mod_diff_eq[symmetric])
   1.221 -  thus "n dvd x - y" by (simp add: zdvd_iff_zmod_eq_0)
   1.222 +  thus "n dvd x - y" by (simp add: dvd_eq_mod_eq_0)
   1.223  next
   1.224    assume H: "n dvd x - y"
   1.225    then obtain k where k: "x-y = n*k" unfolding dvd_def by blast