src/HOL/IntDiv.thy
changeset 33318 ddd97d9dfbfb
parent 33296 a3924d1069e5
child 33340 a165b97f3658
     1.1 --- a/src/HOL/IntDiv.thy	Thu Oct 29 08:14:39 2009 +0100
     1.2 +++ b/src/HOL/IntDiv.thy	Thu Oct 29 11:41:36 2009 +0100
     1.3 @@ -1024,139 +1024,16 @@
     1.4  lemmas zdvd_iff_zmod_eq_0_number_of [simp] =
     1.5    dvd_eq_mod_eq_0 [of "number_of x::int" "number_of y::int", standard]
     1.6  
     1.7 -lemma zdvd_anti_sym:
     1.8 -    "0 < m ==> 0 < n ==> m dvd n ==> n dvd m ==> m = (n::int)"
     1.9 -  apply (simp add: dvd_def, auto)
    1.10 -  apply (simp add: mult_assoc zero_less_mult_iff zmult_eq_1_iff)
    1.11 -  done
    1.12 -
    1.13 -lemma zdvd_dvd_eq: assumes "a \<noteq> 0" and "(a::int) dvd b" and "b dvd a" 
    1.14 -  shows "\<bar>a\<bar> = \<bar>b\<bar>"
    1.15 -proof-
    1.16 -  from `a dvd b` obtain k where k:"b = a*k" unfolding dvd_def by blast 
    1.17 -  from `b dvd a` obtain k' where k':"a = b*k'" unfolding dvd_def by blast 
    1.18 -  from k k' have "a = a*k*k'" by simp
    1.19 -  with mult_cancel_left1[where c="a" and b="k*k'"]
    1.20 -  have kk':"k*k' = 1" using `a\<noteq>0` by (simp add: mult_assoc)
    1.21 -  hence "k = 1 \<and> k' = 1 \<or> k = -1 \<and> k' = -1" by (simp add: zmult_eq_1_iff)
    1.22 -  thus ?thesis using k k' by auto
    1.23 -qed
    1.24 -
    1.25 -lemma zdvd_zdiffD: "k dvd m - n ==> k dvd n ==> k dvd (m::int)"
    1.26 -  apply (subgoal_tac "m = n + (m - n)")
    1.27 -   apply (erule ssubst)
    1.28 -   apply (blast intro: dvd_add, simp)
    1.29 -  done
    1.30 -
    1.31 -lemma zdvd_reduce: "(k dvd n + k * m) = (k dvd (n::int))"
    1.32 -apply (rule iffI)
    1.33 - apply (erule_tac [2] dvd_add)
    1.34 - apply (subgoal_tac "n = (n + k * m) - k * m")
    1.35 -  apply (erule ssubst)
    1.36 -  apply (erule dvd_diff)
    1.37 -  apply(simp_all)
    1.38 -done
    1.39 -
    1.40  lemma zdvd_zmod: "f dvd m ==> f dvd (n::int) ==> f dvd m mod n"
    1.41    by (rule dvd_mod) (* TODO: remove *)
    1.42  
    1.43  lemma zdvd_zmod_imp_zdvd: "k dvd m mod n ==> k dvd n ==> k dvd (m::int)"
    1.44    by (rule dvd_mod_imp_dvd) (* TODO: remove *)
    1.45  
    1.46 -lemma dvd_imp_le_int: "(i::int) ~= 0 ==> d dvd i ==> abs d <= abs i"
    1.47 -apply(auto simp:abs_if)
    1.48 -   apply(clarsimp simp:dvd_def mult_less_0_iff)
    1.49 -  using mult_le_cancel_left_neg[of _ "-1::int"]
    1.50 -  apply(clarsimp simp:dvd_def mult_less_0_iff)
    1.51 - apply(clarsimp simp:dvd_def mult_less_0_iff
    1.52 -         minus_mult_right simp del: mult_minus_right)
    1.53 -apply(clarsimp simp:dvd_def mult_less_0_iff)
    1.54 -done
    1.55 -
    1.56 -lemma zdvd_not_zless: "0 < m ==> m < n ==> \<not> n dvd (m::int)"
    1.57 -  apply (auto elim!: dvdE)
    1.58 -  apply (subgoal_tac "0 < n")
    1.59 -   prefer 2
    1.60 -   apply (blast intro: order_less_trans)
    1.61 -  apply (simp add: zero_less_mult_iff)
    1.62 -  done
    1.63 -
    1.64  lemma zmult_div_cancel: "(n::int) * (m div n) = m - (m mod n)"
    1.65    using zmod_zdiv_equality[where a="m" and b="n"]
    1.66    by (simp add: algebra_simps)
    1.67  
    1.68 -lemma zdvd_mult_div_cancel:"(n::int) dvd m \<Longrightarrow> n * (m div n) = m"
    1.69 -apply (subgoal_tac "m mod n = 0")
    1.70 - apply (simp add: zmult_div_cancel)
    1.71 -apply (simp only: dvd_eq_mod_eq_0)
    1.72 -done
    1.73 -
    1.74 -lemma zdvd_mult_cancel: assumes d:"k * m dvd k * n" and kz:"k \<noteq> (0::int)"
    1.75 -  shows "m dvd n"
    1.76 -proof-
    1.77 -  from d obtain h where h: "k*n = k*m * h" unfolding dvd_def by blast
    1.78 -  {assume "n \<noteq> m*h" hence "k* n \<noteq> k* (m*h)" using kz by simp
    1.79 -    with h have False by (simp add: mult_assoc)}
    1.80 -  hence "n = m * h" by blast
    1.81 -  thus ?thesis by simp
    1.82 -qed
    1.83 -
    1.84 -theorem zdvd_int: "(x dvd y) = (int x dvd int y)"
    1.85 -proof -
    1.86 -  have "\<And>k. int y = int x * k \<Longrightarrow> x dvd y"
    1.87 -  proof -
    1.88 -    fix k
    1.89 -    assume A: "int y = int x * k"
    1.90 -    then show "x dvd y" proof (cases k)
    1.91 -      case (1 n) with A have "y = x * n" by (simp add: zmult_int)
    1.92 -      then show ?thesis ..
    1.93 -    next
    1.94 -      case (2 n) with A have "int y = int x * (- int (Suc n))" by simp
    1.95 -      also have "\<dots> = - (int x * int (Suc n))" by (simp only: mult_minus_right)
    1.96 -      also have "\<dots> = - int (x * Suc n)" by (simp only: zmult_int)
    1.97 -      finally have "- int (x * Suc n) = int y" ..
    1.98 -      then show ?thesis by (simp only: negative_eq_positive) auto
    1.99 -    qed
   1.100 -  qed
   1.101 -  then show ?thesis by (auto elim!: dvdE simp only: dvd_triv_left int_mult)
   1.102 -qed
   1.103 -
   1.104 -lemma zdvd1_eq[simp]: "(x::int) dvd 1 = ( \<bar>x\<bar> = 1)"
   1.105 -proof
   1.106 -  assume d: "x dvd 1" hence "int (nat \<bar>x\<bar>) dvd int (nat 1)" by simp
   1.107 -  hence "nat \<bar>x\<bar> dvd 1" by (simp add: zdvd_int)
   1.108 -  hence "nat \<bar>x\<bar> = 1"  by simp
   1.109 -  thus "\<bar>x\<bar> = 1" by (cases "x < 0", auto)
   1.110 -next
   1.111 -  assume "\<bar>x\<bar>=1" thus "x dvd 1" 
   1.112 -    by(cases "x < 0",simp_all add: minus_equation_iff dvd_eq_mod_eq_0)
   1.113 -qed
   1.114 -lemma zdvd_mult_cancel1: 
   1.115 -  assumes mp:"m \<noteq>(0::int)" shows "(m * n dvd m) = (\<bar>n\<bar> = 1)"
   1.116 -proof
   1.117 -  assume n1: "\<bar>n\<bar> = 1" thus "m * n dvd m" 
   1.118 -    by (cases "n >0", auto simp add: minus_dvd_iff minus_equation_iff)
   1.119 -next
   1.120 -  assume H: "m * n dvd m" hence H2: "m * n dvd m * 1" by simp
   1.121 -  from zdvd_mult_cancel[OF H2 mp] show "\<bar>n\<bar> = 1" by (simp only: zdvd1_eq)
   1.122 -qed
   1.123 -
   1.124 -lemma int_dvd_iff: "(int m dvd z) = (m dvd nat (abs z))"
   1.125 -  unfolding zdvd_int by (cases "z \<ge> 0") simp_all
   1.126 -
   1.127 -lemma dvd_int_iff: "(z dvd int m) = (nat (abs z) dvd m)"
   1.128 -  unfolding zdvd_int by (cases "z \<ge> 0") simp_all
   1.129 -
   1.130 -lemma nat_dvd_iff: "(nat z dvd m) = (if 0 \<le> z then (z dvd int m) else m = 0)"
   1.131 -  by (auto simp add: dvd_int_iff)
   1.132 -
   1.133 -lemma zdvd_imp_le: "[| z dvd n; 0 < n |] ==> z \<le> (n::int)"
   1.134 -  apply (rule_tac z=n in int_cases)
   1.135 -  apply (auto simp add: dvd_int_iff)
   1.136 -  apply (rule_tac z=z in int_cases)
   1.137 -  apply (auto simp add: dvd_imp_le)
   1.138 -  done
   1.139 -
   1.140  lemma zpower_zmod: "((x::int) mod m)^y mod m = x^y mod m"
   1.141  apply (induct "y", auto)
   1.142  apply (rule zmod_zmult1_eq [THEN trans])
   1.143 @@ -1182,6 +1059,12 @@
   1.144  lemma abs_div: "(y::int) dvd x \<Longrightarrow> abs (x div y) = abs x div abs y"
   1.145  by (unfold dvd_def, cases "y=0", auto simp add: abs_mult)
   1.146  
   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: dvd_eq_mod_eq_0)
   1.151 +done
   1.152 +
   1.153  text{*Suggested by Matthias Daum*}
   1.154  lemma int_power_div_base:
   1.155       "\<lbrakk>0 < m; 0 < k\<rbrakk> \<Longrightarrow> k ^ m div k = (k::int) ^ (m - Suc 0)"
   1.156 @@ -1349,6 +1232,43 @@
   1.157  declare dvd_eq_mod_eq_0_number_of [simp]
   1.158  
   1.159  
   1.160 +subsection {* Transfer setup *}
   1.161 +
   1.162 +lemma transfer_nat_int_functions:
   1.163 +    "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> (nat x) div (nat y) = nat (x div y)"
   1.164 +    "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> (nat x) mod (nat y) = nat (x mod y)"
   1.165 +  by (auto simp add: nat_div_distrib nat_mod_distrib)
   1.166 +
   1.167 +lemma transfer_nat_int_function_closures:
   1.168 +    "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> x div y >= 0"
   1.169 +    "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> x mod y >= 0"
   1.170 +  apply (cases "y = 0")
   1.171 +  apply (auto simp add: pos_imp_zdiv_nonneg_iff)
   1.172 +  apply (cases "y = 0")
   1.173 +  apply auto
   1.174 +done
   1.175 +
   1.176 +declare TransferMorphism_nat_int[transfer add return:
   1.177 +  transfer_nat_int_functions
   1.178 +  transfer_nat_int_function_closures
   1.179 +]
   1.180 +
   1.181 +lemma transfer_int_nat_functions:
   1.182 +    "(int x) div (int y) = int (x div y)"
   1.183 +    "(int x) mod (int y) = int (x mod y)"
   1.184 +  by (auto simp add: zdiv_int zmod_int)
   1.185 +
   1.186 +lemma transfer_int_nat_function_closures:
   1.187 +    "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> is_nat (x div y)"
   1.188 +    "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> is_nat (x mod y)"
   1.189 +  by (simp_all only: is_nat_def transfer_nat_int_function_closures)
   1.190 +
   1.191 +declare TransferMorphism_int_nat[transfer add return:
   1.192 +  transfer_int_nat_functions
   1.193 +  transfer_int_nat_function_closures
   1.194 +]
   1.195 +
   1.196 +
   1.197  subsection {* Code generation *}
   1.198  
   1.199  definition pdivmod :: "int \<Rightarrow> int \<Rightarrow> int \<times> int" where