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.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.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.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.42 -   apply (rule_tac x = "-(int k)" in exI)
1.43 -  apply (auto simp add: int_mult)
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:
```