src/HOL/IntDiv.thy
changeset 23306 cdb027d0637e
parent 23164 69e55066dbca
child 23307 2fe3345035c7
     1.1 --- a/src/HOL/IntDiv.thy	Mon Jun 11 02:24:39 2007 +0200
     1.2 +++ b/src/HOL/IntDiv.thy	Mon Jun 11 02:25:55 2007 +0200
     1.3 @@ -1238,9 +1238,11 @@
     1.4    apply simp
     1.5    done
     1.6  
     1.7 -theorem zdvd_int: "(x dvd y) = (int x dvd int y)"
     1.8 -  apply (simp only: dvd_def ex_nat int_int_eq [symmetric] zmult_int [symmetric]
     1.9 -    nat_0_le cong add: conj_cong)
    1.10 +theorem zdvd_int_of_nat: "(x dvd y) = (int_of_nat x dvd int_of_nat y)"
    1.11 +  unfolding dvd_def
    1.12 +  apply (rule_tac s="\<exists>k. int_of_nat y = int_of_nat x * int_of_nat k" in trans)
    1.13 +  apply (simp only: of_nat_mult [symmetric] of_nat_eq_iff)
    1.14 +  apply (simp add: ex_nat cong add: conj_cong)
    1.15    apply (rule iffI)
    1.16    apply iprover
    1.17    apply (erule exE)
    1.18 @@ -1250,11 +1252,14 @@
    1.19    apply (case_tac "0 \<le> k")
    1.20    apply iprover
    1.21    apply (simp add: linorder_not_le)
    1.22 -  apply (drule mult_strict_left_mono_neg [OF iffD2 [OF zero_less_int_conv]])
    1.23 +  apply (drule mult_strict_left_mono_neg [OF iffD2 [OF of_nat_0_less_iff]])
    1.24    apply assumption
    1.25    apply (simp add: mult_ac)
    1.26    done
    1.27  
    1.28 +theorem zdvd_int: "(x dvd y) = (int x dvd int y)"
    1.29 +  unfolding int_eq_of_nat by (rule zdvd_int_of_nat)
    1.30 +
    1.31  lemma zdvd1_eq[simp]: "(x::int) dvd 1 = ( \<bar>x\<bar> = 1)"
    1.32  proof
    1.33    assume d: "x dvd 1" hence "int (nat \<bar>x\<bar>) dvd int (nat 1)" by (simp add: zdvd_abs1)
    1.34 @@ -1275,31 +1280,40 @@
    1.35    from zdvd_mult_cancel[OF H2 mp] show "\<bar>n\<bar> = 1" by (simp only: zdvd1_eq)
    1.36  qed
    1.37  
    1.38 -lemma int_dvd_iff: "(int m dvd z) = (m dvd nat (abs z))"
    1.39 +lemma int_of_nat_dvd_iff: "(int_of_nat m dvd z) = (m dvd nat (abs z))"
    1.40    apply (auto simp add: dvd_def nat_abs_mult_distrib)
    1.41 -  apply (auto simp add: nat_eq_iff abs_if split add: split_if_asm)
    1.42 -   apply (rule_tac x = "-(int k)" in exI)
    1.43 -  apply (auto simp add: int_mult)
    1.44 +  apply (auto simp add: nat_eq_iff' abs_if split add: split_if_asm)
    1.45 +   apply (rule_tac x = "-(int_of_nat k)" in exI)
    1.46 +  apply auto
    1.47 +  done
    1.48 +
    1.49 +lemma int_dvd_iff: "(int m dvd z) = (m dvd nat (abs z))"
    1.50 +  unfolding int_eq_of_nat by (rule int_of_nat_dvd_iff)
    1.51 +
    1.52 +lemma dvd_int_of_nat_iff: "(z dvd int_of_nat m) = (nat (abs z) dvd m)"
    1.53 +  apply (auto simp add: dvd_def abs_if)
    1.54 +    apply (rule_tac [3] x = "nat k" in exI)
    1.55 +    apply (rule_tac [2] x = "-(int_of_nat k)" in exI)
    1.56 +    apply (rule_tac x = "nat (-k)" in exI)
    1.57 +    apply (cut_tac [3] m = m and 'a=int in of_nat_less_0_iff)
    1.58 +    apply (cut_tac m = m and 'a=int in of_nat_less_0_iff)
    1.59 +    apply (auto simp add: zero_le_mult_iff mult_less_0_iff
    1.60 +      nat_mult_distrib [symmetric] nat_eq_iff2')
    1.61    done
    1.62  
    1.63  lemma dvd_int_iff: "(z dvd int m) = (nat (abs z) dvd m)"
    1.64 -  apply (auto simp add: dvd_def abs_if int_mult)
    1.65 -    apply (rule_tac [3] x = "nat k" in exI)
    1.66 -    apply (rule_tac [2] x = "-(int k)" in exI)
    1.67 -    apply (rule_tac x = "nat (-k)" in exI)
    1.68 -    apply (cut_tac [3] k = m in int_less_0_conv)
    1.69 -    apply (cut_tac k = m in int_less_0_conv)
    1.70 -    apply (auto simp add: zero_le_mult_iff mult_less_0_iff
    1.71 -      nat_mult_distrib [symmetric] nat_eq_iff2)
    1.72 +  unfolding int_eq_of_nat by (rule dvd_int_of_nat_iff)
    1.73 +
    1.74 +lemma nat_dvd_iff': "(nat z dvd m) = (if 0 \<le> z then (z dvd int_of_nat m) else m = 0)"
    1.75 +  apply (auto simp add: dvd_def)
    1.76 +  apply (rule_tac x = "nat k" in exI)
    1.77 +  apply (cut_tac m = m and 'a=int in of_nat_less_0_iff)
    1.78 +  apply (auto simp add: zero_le_mult_iff mult_less_0_iff
    1.79 +    nat_mult_distrib [symmetric] nat_eq_iff2')
    1.80    done
    1.81  
    1.82  lemma nat_dvd_iff: "(nat z dvd m) = (if 0 \<le> z then (z dvd int m) else m = 0)"
    1.83 -  apply (auto simp add: dvd_def int_mult)
    1.84 -  apply (rule_tac x = "nat k" in exI)
    1.85 -  apply (cut_tac k = m in int_less_0_conv)
    1.86 -  apply (auto simp add: zero_le_mult_iff mult_less_0_iff
    1.87 -    nat_mult_distrib [symmetric] nat_eq_iff2)
    1.88 -  done
    1.89 +  unfolding int_eq_of_nat by (rule nat_dvd_iff')
    1.90  
    1.91  lemma zminus_dvd_iff [iff]: "(-z dvd w) = (z dvd (w::int))"
    1.92    apply (auto simp add: dvd_def)
    1.93 @@ -1368,20 +1382,28 @@
    1.94  text{*Compatibility binding*}
    1.95  lemmas zpower_int = int_power [symmetric]
    1.96  
    1.97 -lemma zdiv_int: "int (a div b) = (int a) div (int b)"
    1.98 +lemma int_of_nat_div:
    1.99 +  "int_of_nat (a div b) = (int_of_nat a) div (int_of_nat b)"
   1.100  apply (subst split_div, auto)
   1.101  apply (subst split_zdiv, auto)
   1.102 -apply (rule_tac a="int (b * i) + int j" and b="int b" and r="int j" and r'=ja in IntDiv.unique_quotient)
   1.103 -apply (auto simp add: IntDiv.quorem_def int_eq_of_nat)
   1.104 +apply (rule_tac a="int_of_nat (b * i) + int_of_nat j" and b="int_of_nat b" and r="int_of_nat j" and r'=ja in IntDiv.unique_quotient)
   1.105 +apply (auto simp add: IntDiv.quorem_def)
   1.106 +done
   1.107 +
   1.108 +lemma zdiv_int: "int (a div b) = (int a) div (int b)"
   1.109 +  unfolding int_eq_of_nat by (rule int_of_nat_div)
   1.110 +
   1.111 +lemma int_of_nat_mod:
   1.112 +  "int_of_nat (a mod b) = (int_of_nat a) mod (int_of_nat b)"
   1.113 +apply (subst split_mod, auto)
   1.114 +apply (subst split_zmod, auto)
   1.115 +apply (rule_tac a="int_of_nat (b * i) + int_of_nat j" and b="int_of_nat b" and q="int_of_nat i" and q'=ia 
   1.116 +       in unique_remainder)
   1.117 +apply (auto simp add: IntDiv.quorem_def)
   1.118  done
   1.119  
   1.120  lemma zmod_int: "int (a mod b) = (int a) mod (int b)"
   1.121 -apply (subst split_mod, auto)
   1.122 -apply (subst split_zmod, auto)
   1.123 -apply (rule_tac a="int (b * i) + int j" and b="int b" and q="int i" and q'=ia 
   1.124 -       in unique_remainder)
   1.125 -apply (auto simp add: IntDiv.quorem_def int_eq_of_nat)
   1.126 -done
   1.127 +  unfolding int_eq_of_nat by (rule int_of_nat_mod)
   1.128  
   1.129  text{*Suggested by Matthias Daum*}
   1.130  lemma int_power_div_base: