src/HOL/IntDiv.thy
 changeset 23365 f31794033ae1 parent 23307 2fe3345035c7 child 23401 8c5532263ba9
```     1.1 --- a/src/HOL/IntDiv.thy	Wed Jun 13 03:28:21 2007 +0200
1.2 +++ b/src/HOL/IntDiv.thy	Wed Jun 13 03:31:11 2007 +0200
1.3 @@ -11,8 +11,6 @@
1.4  imports IntArith Divides FunDef
1.5  begin
1.6
1.7 -declare zless_nat_conj [simp]
1.8 -
1.9  constdefs
1.10    quorem :: "(int*int) * (int*int) => bool"
1.11      --{*definition of quotient and remainder*}
1.12 @@ -266,7 +264,7 @@
1.13    val trans = trans;
1.14    val prove_eq_sums =
1.15      let
1.17 +      val simps = @{thm diff_int_def} :: Int_Numeral_Simprocs.add_0s @ @{thms zadd_ac}
1.18      in NatArithUtils.prove_conv all_tac (NatArithUtils.simp_all_tac simps) end;
1.19  end)
1.20
1.21 @@ -1238,9 +1236,9 @@
1.22    apply simp
1.23    done
1.24
1.25 -theorem zdvd_int_of_nat: "(x dvd y) = (int_of_nat x dvd int_of_nat y)"
1.26 +theorem zdvd_int: "(x dvd y) = (int x dvd int y)"
1.27    unfolding dvd_def
1.28 -  apply (rule_tac s="\<exists>k. int_of_nat y = int_of_nat x * int_of_nat k" in trans)
1.29 +  apply (rule_tac s="\<exists>k. int y = int x * int k" in trans)
1.30    apply (simp only: of_nat_mult [symmetric] of_nat_eq_iff)
1.32    apply (rule iffI)
1.33 @@ -1257,9 +1255,6 @@
1.35    done
1.36
1.37 -theorem zdvd_int: "(x dvd y) = (int x dvd int y)"
1.38 -  unfolding int_eq_of_nat by (rule zdvd_int_of_nat)
1.39 -
1.40  lemma zdvd1_eq[simp]: "(x::int) dvd 1 = ( \<bar>x\<bar> = 1)"
1.41  proof
1.42    assume d: "x dvd 1" hence "int (nat \<bar>x\<bar>) dvd int (nat 1)" by (simp add: zdvd_abs1)
1.43 @@ -1280,40 +1275,31 @@
1.44    from zdvd_mult_cancel[OF H2 mp] show "\<bar>n\<bar> = 1" by (simp only: zdvd1_eq)
1.45  qed
1.46
1.47 -lemma int_of_nat_dvd_iff: "(int_of_nat m dvd z) = (m dvd nat (abs z))"
1.48 +lemma int_dvd_iff: "(int m dvd z) = (m dvd nat (abs z))"
1.49    apply (auto simp add: dvd_def nat_abs_mult_distrib)
1.51 -   apply (rule_tac x = "-(int_of_nat k)" in exI)
1.53 +   apply (rule_tac x = "-(int k)" in exI)
1.54    apply auto
1.55    done
1.56
1.57 -lemma int_dvd_iff: "(int m dvd z) = (m dvd nat (abs z))"
1.58 -  unfolding int_eq_of_nat by (rule int_of_nat_dvd_iff)
1.59 -
1.60 -lemma dvd_int_of_nat_iff: "(z dvd int_of_nat m) = (nat (abs z) dvd m)"
1.61 +lemma dvd_int_iff: "(z dvd int m) = (nat (abs z) dvd m)"
1.62    apply (auto simp add: dvd_def abs_if)
1.63      apply (rule_tac [3] x = "nat k" in exI)
1.64 -    apply (rule_tac [2] x = "-(int_of_nat k)" in exI)
1.65 +    apply (rule_tac [2] x = "-(int k)" in exI)
1.66      apply (rule_tac x = "nat (-k)" in exI)
1.67 -    apply (cut_tac [3] m = m and 'a=int in of_nat_less_0_iff)
1.68 -    apply (cut_tac m = m and 'a=int in of_nat_less_0_iff)
1.69 +    apply (cut_tac [3] m = m in int_less_0_conv)
1.70 +    apply (cut_tac m = m in int_less_0_conv)
1.71      apply (auto simp add: zero_le_mult_iff mult_less_0_iff
1.72 -      nat_mult_distrib [symmetric] nat_eq_iff2')
1.73 -  done
1.74 -
1.75 -lemma dvd_int_iff: "(z dvd int m) = (nat (abs z) dvd m)"
1.76 -  unfolding int_eq_of_nat by (rule dvd_int_of_nat_iff)
1.77 -
1.78 -lemma nat_dvd_iff': "(nat z dvd m) = (if 0 \<le> z then (z dvd int_of_nat m) else m = 0)"
1.79 -  apply (auto simp add: dvd_def)
1.80 -  apply (rule_tac x = "nat k" in exI)
1.81 -  apply (cut_tac m = m and 'a=int in of_nat_less_0_iff)
1.82 -  apply (auto simp add: zero_le_mult_iff mult_less_0_iff
1.83 -    nat_mult_distrib [symmetric] nat_eq_iff2')
1.84 +      nat_mult_distrib [symmetric] nat_eq_iff2)
1.85    done
1.86
1.87  lemma nat_dvd_iff: "(nat z dvd m) = (if 0 \<le> z then (z dvd int m) else m = 0)"
1.88 -  unfolding int_eq_of_nat by (rule nat_dvd_iff')
1.89 +  apply (auto simp add: dvd_def)
1.90 +  apply (rule_tac x = "nat k" in exI)
1.91 +  apply (cut_tac m = m in int_less_0_conv)
1.92 +  apply (auto simp add: zero_le_mult_iff mult_less_0_iff
1.93 +    nat_mult_distrib [symmetric] nat_eq_iff2)
1.94 +  done
1.95
1.96  lemma zminus_dvd_iff [iff]: "(-z dvd w) = (z dvd (w::int))"
1.97    apply (auto simp add: dvd_def)
1.98 @@ -1327,9 +1313,9 @@
1.99    done
1.100
1.101  lemma zdvd_imp_le: "[| z dvd n; 0 < n |] ==> z \<le> (n::int)"
1.102 -  apply (rule_tac z=n in int_cases')
1.103 -  apply (auto simp add: dvd_int_of_nat_iff)
1.104 -  apply (rule_tac z=z in int_cases')
1.105 +  apply (rule_tac z=n in int_cases)
1.106 +  apply (auto simp add: dvd_int_iff)
1.107 +  apply (rule_tac z=z in int_cases)
1.108    apply (auto simp add: dvd_imp_le)
1.109    done
1.110
1.111 @@ -1377,33 +1363,25 @@
1.112  done
1.113
1.114  lemma int_power: "int (m^n) = (int m) ^ n"
1.115 -  by (induct n, simp_all add: int_mult)
1.116 +  by (rule of_nat_power)
1.117
1.118  text{*Compatibility binding*}
1.119  lemmas zpower_int = int_power [symmetric]
1.120
1.121 -lemma int_of_nat_div:
1.122 -  "int_of_nat (a div b) = (int_of_nat a) div (int_of_nat b)"
1.123 +lemma zdiv_int: "int (a div b) = (int a) div (int b)"
1.124  apply (subst split_div, auto)
1.125  apply (subst split_zdiv, auto)
1.126 -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.127 -apply (auto simp add: IntDiv.quorem_def)
1.128 -done
1.129 -
1.130 -lemma zdiv_int: "int (a div b) = (int a) div (int b)"
1.131 -  unfolding int_eq_of_nat by (rule int_of_nat_div)
1.132 -
1.133 -lemma int_of_nat_mod:
1.134 -  "int_of_nat (a mod b) = (int_of_nat a) mod (int_of_nat b)"
1.135 -apply (subst split_mod, auto)
1.136 -apply (subst split_zmod, auto)
1.137 -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.138 -       in unique_remainder)
1.139 +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.140  apply (auto simp add: IntDiv.quorem_def)
1.141  done
1.142
1.143  lemma zmod_int: "int (a mod b) = (int a) mod (int b)"
1.144 -  unfolding int_eq_of_nat by (rule int_of_nat_mod)
1.145 +apply (subst split_mod, auto)
1.146 +apply (subst split_zmod, auto)
1.147 +apply (rule_tac a="int (b * i) + int j" and b="int b" and q="int i" and q'=ia
1.148 +       in unique_remainder)
1.149 +apply (auto simp add: IntDiv.quorem_def)
1.150 +done
1.151
1.152  text{*Suggested by Matthias Daum*}
1.153  lemma int_power_div_base:
```