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.16 -      val simps = diff_int_def :: Int_Numeral_Simprocs.add_0s @ zadd_ac
    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.31    apply (simp add: ex_nat cong add: conj_cong)
    1.32    apply (rule iffI)
    1.33 @@ -1257,9 +1255,6 @@
    1.34    apply (simp add: mult_ac)
    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.50 -  apply (auto simp add: nat_eq_iff' abs_if split add: split_if_asm)
    1.51 -   apply (rule_tac x = "-(int_of_nat k)" in exI)
    1.52 +  apply (auto simp add: nat_eq_iff abs_if split add: split_if_asm)
    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: