--- a/src/HOL/IntDiv.thy Wed Jun 13 03:28:21 2007 +0200
+++ b/src/HOL/IntDiv.thy Wed Jun 13 03:31:11 2007 +0200
@@ -11,8 +11,6 @@
imports IntArith Divides FunDef
begin
-declare zless_nat_conj [simp]
-
constdefs
quorem :: "(int*int) * (int*int) => bool"
--{*definition of quotient and remainder*}
@@ -266,7 +264,7 @@
val trans = trans;
val prove_eq_sums =
let
- val simps = diff_int_def :: Int_Numeral_Simprocs.add_0s @ zadd_ac
+ val simps = @{thm diff_int_def} :: Int_Numeral_Simprocs.add_0s @ @{thms zadd_ac}
in NatArithUtils.prove_conv all_tac (NatArithUtils.simp_all_tac simps) end;
end)
@@ -1238,9 +1236,9 @@
apply simp
done
-theorem zdvd_int_of_nat: "(x dvd y) = (int_of_nat x dvd int_of_nat y)"
+theorem zdvd_int: "(x dvd y) = (int x dvd int y)"
unfolding dvd_def
- apply (rule_tac s="\<exists>k. int_of_nat y = int_of_nat x * int_of_nat k" in trans)
+ apply (rule_tac s="\<exists>k. int y = int x * int k" in trans)
apply (simp only: of_nat_mult [symmetric] of_nat_eq_iff)
apply (simp add: ex_nat cong add: conj_cong)
apply (rule iffI)
@@ -1257,9 +1255,6 @@
apply (simp add: mult_ac)
done
-theorem zdvd_int: "(x dvd y) = (int x dvd int y)"
- unfolding int_eq_of_nat by (rule zdvd_int_of_nat)
-
lemma zdvd1_eq[simp]: "(x::int) dvd 1 = ( \<bar>x\<bar> = 1)"
proof
assume d: "x dvd 1" hence "int (nat \<bar>x\<bar>) dvd int (nat 1)" by (simp add: zdvd_abs1)
@@ -1280,40 +1275,31 @@
from zdvd_mult_cancel[OF H2 mp] show "\<bar>n\<bar> = 1" by (simp only: zdvd1_eq)
qed
-lemma int_of_nat_dvd_iff: "(int_of_nat m dvd z) = (m dvd nat (abs z))"
+lemma int_dvd_iff: "(int m dvd z) = (m dvd nat (abs z))"
apply (auto simp add: dvd_def nat_abs_mult_distrib)
- apply (auto simp add: nat_eq_iff' abs_if split add: split_if_asm)
- apply (rule_tac x = "-(int_of_nat k)" in exI)
+ apply (auto simp add: nat_eq_iff abs_if split add: split_if_asm)
+ apply (rule_tac x = "-(int k)" in exI)
apply auto
done
-lemma int_dvd_iff: "(int m dvd z) = (m dvd nat (abs z))"
- unfolding int_eq_of_nat by (rule int_of_nat_dvd_iff)
-
-lemma dvd_int_of_nat_iff: "(z dvd int_of_nat m) = (nat (abs z) dvd m)"
+lemma dvd_int_iff: "(z dvd int m) = (nat (abs z) dvd m)"
apply (auto simp add: dvd_def abs_if)
apply (rule_tac [3] x = "nat k" in exI)
- apply (rule_tac [2] x = "-(int_of_nat k)" in exI)
+ apply (rule_tac [2] x = "-(int k)" in exI)
apply (rule_tac x = "nat (-k)" in exI)
- apply (cut_tac [3] m = m and 'a=int in of_nat_less_0_iff)
- apply (cut_tac m = m and 'a=int in of_nat_less_0_iff)
+ apply (cut_tac [3] m = m in int_less_0_conv)
+ apply (cut_tac m = m in int_less_0_conv)
apply (auto simp add: zero_le_mult_iff mult_less_0_iff
- nat_mult_distrib [symmetric] nat_eq_iff2')
- done
-
-lemma dvd_int_iff: "(z dvd int m) = (nat (abs z) dvd m)"
- unfolding int_eq_of_nat by (rule dvd_int_of_nat_iff)
-
-lemma nat_dvd_iff': "(nat z dvd m) = (if 0 \<le> z then (z dvd int_of_nat m) else m = 0)"
- apply (auto simp add: dvd_def)
- apply (rule_tac x = "nat k" in exI)
- apply (cut_tac m = m and 'a=int in of_nat_less_0_iff)
- apply (auto simp add: zero_le_mult_iff mult_less_0_iff
- nat_mult_distrib [symmetric] nat_eq_iff2')
+ nat_mult_distrib [symmetric] nat_eq_iff2)
done
lemma nat_dvd_iff: "(nat z dvd m) = (if 0 \<le> z then (z dvd int m) else m = 0)"
- unfolding int_eq_of_nat by (rule nat_dvd_iff')
+ apply (auto simp add: dvd_def)
+ apply (rule_tac x = "nat k" in exI)
+ apply (cut_tac m = m in int_less_0_conv)
+ apply (auto simp add: zero_le_mult_iff mult_less_0_iff
+ nat_mult_distrib [symmetric] nat_eq_iff2)
+ done
lemma zminus_dvd_iff [iff]: "(-z dvd w) = (z dvd (w::int))"
apply (auto simp add: dvd_def)
@@ -1327,9 +1313,9 @@
done
lemma zdvd_imp_le: "[| z dvd n; 0 < n |] ==> z \<le> (n::int)"
- apply (rule_tac z=n in int_cases')
- apply (auto simp add: dvd_int_of_nat_iff)
- apply (rule_tac z=z in int_cases')
+ apply (rule_tac z=n in int_cases)
+ apply (auto simp add: dvd_int_iff)
+ apply (rule_tac z=z in int_cases)
apply (auto simp add: dvd_imp_le)
done
@@ -1377,33 +1363,25 @@
done
lemma int_power: "int (m^n) = (int m) ^ n"
- by (induct n, simp_all add: int_mult)
+ by (rule of_nat_power)
text{*Compatibility binding*}
lemmas zpower_int = int_power [symmetric]
-lemma int_of_nat_div:
- "int_of_nat (a div b) = (int_of_nat a) div (int_of_nat b)"
+lemma zdiv_int: "int (a div b) = (int a) div (int b)"
apply (subst split_div, auto)
apply (subst split_zdiv, auto)
-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)
-apply (auto simp add: IntDiv.quorem_def)
-done
-
-lemma zdiv_int: "int (a div b) = (int a) div (int b)"
- unfolding int_eq_of_nat by (rule int_of_nat_div)
-
-lemma int_of_nat_mod:
- "int_of_nat (a mod b) = (int_of_nat a) mod (int_of_nat b)"
-apply (subst split_mod, auto)
-apply (subst split_zmod, auto)
-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
- in unique_remainder)
+apply (rule_tac a="int (b * i) + int j" and b="int b" and r="int j" and r'=ja in IntDiv.unique_quotient)
apply (auto simp add: IntDiv.quorem_def)
done
lemma zmod_int: "int (a mod b) = (int a) mod (int b)"
- unfolding int_eq_of_nat by (rule int_of_nat_mod)
+apply (subst split_mod, auto)
+apply (subst split_zmod, auto)
+apply (rule_tac a="int (b * i) + int j" and b="int b" and q="int i" and q'=ia
+ in unique_remainder)
+apply (auto simp add: IntDiv.quorem_def)
+done
text{*Suggested by Matthias Daum*}
lemma int_power_div_base: