# HG changeset patch
# User paulson
# Date 1046366569 -3600
# Node ID 8dd150d36c6536e9ab208a160b263e314efb459e
# Parent  6d0392fc6dc5d2902dde1fb68bf54541d7b6f209
Reorganized, moving many results about the integer dvd relation from IntPrimes
to main HOL (IntDiv)

diff -r 6d0392fc6dc5 -r 8dd150d36c65 src/HOL/Integ/IntArith.ML
--- a/src/HOL/Integ/IntArith.ML	Thu Feb 27 18:21:42 2003 +0100
+++ b/src/HOL/Integ/IntArith.ML	Thu Feb 27 18:22:49 2003 +0100
@@ -185,3 +185,37 @@
 by Auto_tac;  
 qed "zmult_eq_1_iff";
 
+
+(*** More about nat ***)
+
+Goal "[| (0::int) <= z;  0 <= z' |] ==> nat (z+z') = nat z + nat z'";
+by (rtac (inj_int RS injD) 1);
+by (asm_simp_tac (simpset() addsimps [zadd_int RS sym]) 1);
+qed "nat_add_distrib";
+
+Goal "[| (0::int) <= z';  z' <= z |] ==> nat (z-z') = nat z - nat z'";
+by (rtac (inj_int RS injD) 1);
+by (asm_simp_tac (simpset() addsimps [zdiff_int RS sym, nat_le_eq_zle]) 1);
+qed "nat_diff_distrib";
+
+Goal "(0::int) <= z ==> nat (z*z') = nat z * nat z'";
+by (case_tac "0 <= z'" 1);
+by (asm_full_simp_tac (simpset() addsimps [zmult_le_0_iff]) 2);
+by (rtac (inj_int RS injD) 1);
+by (asm_simp_tac (simpset() addsimps [zmult_int RS sym,
+				      int_0_le_mult_iff]) 1);
+qed "nat_mult_distrib";
+
+Goal "z <= (0::int) ==> nat(z*z') = nat(-z) * nat(-z')"; 
+by (rtac trans 1); 
+by (rtac nat_mult_distrib 2); 
+by Auto_tac;  
+qed "nat_mult_distrib_neg";
+
+Goal "nat (abs (w * z)) = nat (abs w) * nat (abs z)";
+by (case_tac "z=0 | w=0" 1);
+by Auto_tac;  
+by (simp_tac (simpset() addsimps [zabs_def, nat_mult_distrib RS sym, 
+                          nat_mult_distrib_neg RS sym, zmult_less_0_iff]) 1);
+by (arith_tac 1);
+qed "nat_abs_mult_distrib";
diff -r 6d0392fc6dc5 -r 8dd150d36c65 src/HOL/Integ/IntArith.thy
--- a/src/HOL/Integ/IntArith.thy	Thu Feb 27 18:21:42 2003 +0100
+++ b/src/HOL/Integ/IntArith.thy	Thu Feb 27 18:22:49 2003 +0100
@@ -7,8 +7,13 @@
 use "int_arith1.ML"
 setup int_arith_setup
 use "int_arith2.ML"
+
 declare zabs_split [arith_split]
 
+lemma zabs_eq_iff:
+    "(abs (z::int) = w) = (z = w \<and> 0 <= z \<or> z = -w \<and> z < 0)"
+  by (auto simp add: zabs_def)
+
 lemma split_nat[arith_split]:
   "P(nat(i::int)) = ((ALL n. i = int n \<longrightarrow> P n) & (i < 0 \<longrightarrow> P 0))"
   (is "?P = (?L & ?R)")
diff -r 6d0392fc6dc5 -r 8dd150d36c65 src/HOL/Integ/IntDiv.thy
--- a/src/HOL/Integ/IntDiv.thy	Thu Feb 27 18:21:42 2003 +0100
+++ b/src/HOL/Integ/IntDiv.thy	Thu Feb 27 18:22:49 2003 +0100
@@ -628,9 +628,6 @@
 
 declare zmod_eq_0_iff [THEN iffD1, dest!]
 
-lemma zdvd_iff_zmod_eq_0: "(m dvd n) = (n mod m = (0::int))"
-by(simp add:dvd_def zmod_eq_0_iff)
-
 (** proving (a+b) div c = a div c + b div c + ((a mod c + b mod c) div c) **)
 
 lemma zadd1_lemma:
@@ -988,6 +985,175 @@
 lemma neg_imp_zdiv_neg_iff: "b < (0::int) ==> (a div b < 0) = (0 < a)"
 by (simp add: linorder_not_le [symmetric] neg_imp_zdiv_nonneg_iff)
 
+
+subsection {* Divides relation *}
+
+lemma zdvd_iff_zmod_eq_0: "(m dvd n) = (n mod m = (0::int))"
+by(simp add:dvd_def zmod_eq_0_iff)
+
+lemma zdvd_0_right [iff]: "(m::int) dvd 0"
+  apply (unfold dvd_def)
+  apply (blast intro: zmult_0_right [symmetric])
+  done
+
+lemma zdvd_0_left [iff]: "(0 dvd (m::int)) = (m = 0)"
+  by (unfold dvd_def, auto)
+
+lemma zdvd_1_left [iff]: "1 dvd (m::int)"
+  by (unfold dvd_def, simp)
+
+lemma zdvd_refl [simp]: "m dvd (m::int)"
+  apply (unfold dvd_def)
+  apply (blast intro: zmult_1_right [symmetric])
+  done
+
+lemma zdvd_trans: "m dvd n ==> n dvd k ==> m dvd (k::int)"
+  apply (unfold dvd_def)
+  apply (blast intro: zmult_assoc)
+  done
+
+lemma zdvd_zminus_iff: "(m dvd -n) = (m dvd (n::int))"
+  apply (unfold dvd_def, auto)
+   apply (rule_tac [!] x = "-k" in exI, auto)
+  done
+
+lemma zdvd_zminus2_iff: "(-m dvd n) = (m dvd (n::int))"
+  apply (unfold dvd_def, auto)
+   apply (rule_tac [!] x = "-k" in exI, auto)
+  done
+
+lemma zdvd_anti_sym:
+    "0 < m ==> 0 < n ==> m dvd n ==> n dvd m ==> m = (n::int)"
+  apply (unfold dvd_def, auto)
+  apply (simp add: zmult_assoc zmult_eq_self_iff int_0_less_mult_iff zmult_eq_1_iff)
+  done
+
+lemma zdvd_zadd: "k dvd m ==> k dvd n ==> k dvd (m + n :: int)"
+  apply (unfold dvd_def)
+  apply (blast intro: zadd_zmult_distrib2 [symmetric])
+  done
+
+lemma zdvd_zdiff: "k dvd m ==> k dvd n ==> k dvd (m - n :: int)"
+  apply (unfold dvd_def)
+  apply (blast intro: zdiff_zmult_distrib2 [symmetric])
+  done
+
+lemma zdvd_zdiffD: "k dvd m - n ==> k dvd n ==> k dvd (m::int)"
+  apply (subgoal_tac "m = n + (m - n)")
+   apply (erule ssubst)
+   apply (blast intro: zdvd_zadd, simp)
+  done
+
+lemma zdvd_zmult: "k dvd (n::int) ==> k dvd m * n"
+  apply (unfold dvd_def)
+  apply (blast intro: zmult_left_commute)
+  done
+
+lemma zdvd_zmult2: "k dvd (m::int) ==> k dvd m * n"
+  apply (subst zmult_commute)
+  apply (erule zdvd_zmult)
+  done
+
+lemma [iff]: "(k::int) dvd m * k"
+  apply (rule zdvd_zmult)
+  apply (rule zdvd_refl)
+  done
+
+lemma [iff]: "(k::int) dvd k * m"
+  apply (rule zdvd_zmult2)
+  apply (rule zdvd_refl)
+  done
+
+lemma zdvd_zmultD2: "j * k dvd n ==> j dvd (n::int)"
+  apply (unfold dvd_def)
+  apply (simp add: zmult_assoc, blast)
+  done
+
+lemma zdvd_zmultD: "j * k dvd n ==> k dvd (n::int)"
+  apply (rule zdvd_zmultD2)
+  apply (subst zmult_commute, assumption)
+  done
+
+lemma zdvd_zmult_mono: "i dvd m ==> j dvd (n::int) ==> i * j dvd m * n"
+  apply (unfold dvd_def, clarify)
+  apply (rule_tac x = "k * ka" in exI)
+  apply (simp add: zmult_ac)
+  done
+
+lemma zdvd_reduce: "(k dvd n + k * m) = (k dvd (n::int))"
+  apply (rule iffI)
+   apply (erule_tac [2] zdvd_zadd)
+   apply (subgoal_tac "n = (n + k * m) - k * m")
+    apply (erule ssubst)
+    apply (erule zdvd_zdiff, simp_all)
+  done
+
+lemma zdvd_zmod: "f dvd m ==> f dvd (n::int) ==> f dvd m mod n"
+  apply (unfold dvd_def)
+  apply (auto simp add: zmod_zmult_zmult1)
+  done
+
+lemma zdvd_zmod_imp_zdvd: "k dvd m mod n ==> k dvd n ==> k dvd (m::int)"
+  apply (subgoal_tac "k dvd n * (m div n) + m mod n")
+   apply (simp add: zmod_zdiv_equality [symmetric])
+  apply (simp only: zdvd_zadd zdvd_zmult2)
+  done
+
+lemma zdvd_not_zless: "0 < m ==> m < n ==> \<not> n dvd (m::int)"
+  apply (unfold dvd_def, auto)
+  apply (subgoal_tac "0 < n")
+   prefer 2
+   apply (blast intro: zless_trans)
+  apply (simp add: int_0_less_mult_iff)
+  apply (subgoal_tac "n * k < n * 1")
+   apply (drule zmult_zless_cancel1 [THEN iffD1], auto)
+  done
+
+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 zabs_eq_iff)
+   apply (rule_tac [2] x = "-(int k)" in exI)
+  apply (auto simp add: zmult_int [symmetric])
+  done
+
+lemma dvd_int_iff: "(z dvd int m) = (nat (abs z) dvd m)"
+  apply (auto simp add: dvd_def zabs_def zmult_int [symmetric])
+    apply (rule_tac [3] x = "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] k = m in int_less_0_conv)
+    apply (cut_tac k = m in int_less_0_conv)
+    apply (auto simp add: int_0_le_mult_iff zmult_less_0_iff
+      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)"
+  apply (auto simp add: dvd_def zmult_int [symmetric])
+  apply (rule_tac x = "nat k" in exI)
+  apply (cut_tac k = m in int_less_0_conv)
+  apply (auto simp add: int_0_le_mult_iff zmult_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)
+   apply (rule_tac [!] x = "-k" in exI, auto)
+  done
+
+lemma dvd_zminus_iff [iff]: "(z dvd -w) = (z dvd (w::int))"
+  apply (auto simp add: dvd_def)
+   apply (drule zminus_equation [THEN iffD1])
+   apply (rule_tac [!] x = "-k" in exI, auto)
+  done
+
+lemma zdvd_imp_le: "[| z dvd n; 0 < n |] ==> z <= (n::int)"
+  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
+
+
 ML
 {*
 val quorem_def = thm "quorem_def";
diff -r 6d0392fc6dc5 -r 8dd150d36c65 src/HOL/Integ/Int_lemmas.ML
--- a/src/HOL/Integ/Int_lemmas.ML	Thu Feb 27 18:21:42 2003 +0100
+++ b/src/HOL/Integ/Int_lemmas.ML	Thu Feb 27 18:22:49 2003 +0100
@@ -319,7 +319,7 @@
 qed "zle_iff_zadd";
 
 Goal "abs (int m) = int m";
-by (simp_tac (simpset() addsimps [zabs_def]) 1); 
+by (simp_tac (simpset() addsimps [Int.zabs_def]) 1); 
 qed "abs_int_eq";
 Addsimps [abs_int_eq];
 
@@ -394,7 +394,6 @@
 by (auto_tac (claset(), simpset() addsimps [lemma, linorder_not_less])); 
 qed "zless_nat_conj";
 
-
 (* a case theorem distinguishing non-negative and negative int *)  
 
 val prems = Goal
diff -r 6d0392fc6dc5 -r 8dd150d36c65 src/HOL/Integ/nat_bin.ML
--- a/src/HOL/Integ/nat_bin.ML	Thu Feb 27 18:21:42 2003 +0100
+++ b/src/HOL/Integ/nat_bin.ML	Thu Feb 27 18:22:49 2003 +0100
@@ -8,6 +8,7 @@
 
 val nat_number_of_def = thm "nat_number_of_def";
 
+
 (** nat (coercion from int to nat) **)
 
 Goal "nat (number_of w) = number_of w";
@@ -31,6 +32,50 @@
 by (rtac nat_2 1); 
 qed "numeral_2_eq_2";
 
+
+(** Distributive laws for "nat".  The others are in IntArith.ML, but these
+    require div and mod to be defined for type "int".  They also need 
+    some of the lemmas proved just above.**)
+
+Goal "(0::int) <= z ==> nat (z div z') = nat z div nat z'";
+by (case_tac "0 <= z'" 1);
+by (auto_tac (claset(), 
+	      simpset() addsimps [div_nonneg_neg_le0, DIVISION_BY_ZERO_DIV]));
+by (case_tac "z' = 0" 1 THEN asm_simp_tac (simpset() addsimps [DIVISION_BY_ZERO]) 1);
+ by (simp_tac (simpset() addsimps [numeral_0_eq_0, DIVISION_BY_ZERO_DIV]) 1);
+by (auto_tac (claset() addSEs [nonneg_eq_int], simpset()));
+by (rename_tac "m m'" 1);
+by (subgoal_tac "0 <= int m div int m'" 1);
+ by (asm_full_simp_tac 
+     (simpset() addsimps [numeral_0_eq_0, pos_imp_zdiv_nonneg_iff]) 2);
+by (rtac (inj_int RS injD) 1);
+by (Asm_simp_tac 1);
+by (res_inst_tac [("r", "int (m mod m')")] quorem_div 1);
+ by (Force_tac 2);
+by (asm_full_simp_tac 
+    (simpset() addsimps [nat_less_iff RS sym, quorem_def, 
+	                 numeral_0_eq_0, zadd_int, zmult_int]) 1);
+qed "nat_div_distrib";
+
+(*Fails if z'<0: the LHS collapses to (nat z) but the RHS doesn't*)
+Goal "[| (0::int) <= z;  0 <= z' |] ==> nat (z mod z') = nat z mod nat z'";
+by (case_tac "z' = 0" 1 THEN asm_simp_tac (simpset() addsimps [DIVISION_BY_ZERO]) 1);
+ by (simp_tac (simpset() addsimps [numeral_0_eq_0, DIVISION_BY_ZERO_MOD]) 1);
+by (auto_tac (claset() addSEs [nonneg_eq_int], simpset()));
+by (rename_tac "m m'" 1);
+by (subgoal_tac "0 <= int m mod int m'" 1);
+ by (asm_full_simp_tac 
+     (simpset() addsimps [nat_less_iff, numeral_0_eq_0, pos_mod_sign]) 2);
+by (rtac (inj_int RS injD) 1);
+by (Asm_simp_tac 1);
+by (res_inst_tac [("q", "int (m div m')")] quorem_mod 1);
+ by (Force_tac 2);
+by (asm_full_simp_tac 
+     (simpset() addsimps [nat_less_iff RS sym, quorem_def, 
+		          numeral_0_eq_0, zadd_int, zmult_int]) 1);
+qed "nat_mod_distrib";
+
+
 (** int (coercion from nat to int) **)
 
 (*"neg" is used in rewrite rules for binary comparisons*)
@@ -78,11 +123,6 @@
 
 (** Addition **)
 
-Goal "[| (0::int) <= z;  0 <= z' |] ==> nat (z+z') = nat z + nat z'";
-by (rtac (inj_int RS injD) 1);
-by (asm_simp_tac (simpset() addsimps [zadd_int RS sym]) 1);
-qed "nat_add_distrib";
-
 (*"neg" is used in rewrite rules for binary comparisons*)
 Goal "(number_of v :: nat) + number_of v' = \
 \        (if neg (number_of v) then number_of v' \
@@ -98,12 +138,6 @@
 
 (** Subtraction **)
 
-Goal "[| (0::int) <= z';  z' <= z |] ==> nat (z-z') = nat z - nat z'";
-by (rtac (inj_int RS injD) 1);
-by (asm_simp_tac (simpset() addsimps [zdiff_int RS sym, nat_le_eq_zle]) 1);
-qed "nat_diff_distrib";
-
-
 Goal "nat z - nat z' = \
 \       (if neg z' then nat z  \
 \        else let d = z-z' in    \
@@ -129,20 +163,6 @@
 
 (** Multiplication **)
 
-Goal "(0::int) <= z ==> nat (z*z') = nat z * nat z'";
-by (case_tac "0 <= z'" 1);
-by (asm_full_simp_tac (simpset() addsimps [zmult_le_0_iff]) 2);
-by (rtac (inj_int RS injD) 1);
-by (asm_simp_tac (simpset() addsimps [zmult_int RS sym,
-				      int_0_le_mult_iff]) 1);
-qed "nat_mult_distrib";
-
-Goal "z <= (0::int) ==> nat(z*z') = nat(-z) * nat(-z')"; 
-by (rtac trans 1); 
-by (rtac nat_mult_distrib 2); 
-by Auto_tac;  
-qed "nat_mult_distrib_neg";
-
 Goal "(number_of v :: nat) * number_of v' = \
 \      (if neg (number_of v) then 0 else number_of (bin_mult v v'))";
 by (simp_tac
@@ -156,26 +176,6 @@
 
 (** Quotient **)
 
-Goal "(0::int) <= z ==> nat (z div z') = nat z div nat z'";
-by (case_tac "0 <= z'" 1);
-by (auto_tac (claset(), 
-	      simpset() addsimps [div_nonneg_neg_le0, DIVISION_BY_ZERO_DIV]));
-by (case_tac "z' = 0" 1 THEN asm_simp_tac (simpset() addsimps [DIVISION_BY_ZERO]) 1);
- by (simp_tac (simpset() addsimps [numeral_0_eq_0, DIVISION_BY_ZERO_DIV]) 1);
-by (auto_tac (claset() addSEs [nonneg_eq_int], simpset()));
-by (rename_tac "m m'" 1);
-by (subgoal_tac "0 <= int m div int m'" 1);
- by (asm_full_simp_tac 
-     (simpset() addsimps [numeral_0_eq_0, pos_imp_zdiv_nonneg_iff]) 2);
-by (rtac (inj_int RS injD) 1);
-by (Asm_simp_tac 1);
-by (res_inst_tac [("r", "int (m mod m')")] quorem_div 1);
- by (Force_tac 2);
-by (asm_full_simp_tac 
-    (simpset() addsimps [nat_less_iff RS sym, quorem_def, 
-	                 numeral_0_eq_0, zadd_int, zmult_int]) 1);
-qed "nat_div_distrib";
-
 Goal "(number_of v :: nat)  div  number_of v' = \
 \         (if neg (number_of v) then 0 \
 \          else nat (number_of v div number_of v'))";
@@ -189,24 +189,6 @@
 
 (** Remainder **)
 
-(*Fails if z'<0: the LHS collapses to (nat z) but the RHS doesn't*)
-Goal "[| (0::int) <= z;  0 <= z' |] ==> nat (z mod z') = nat z mod nat z'";
-by (case_tac "z' = 0" 1 THEN asm_simp_tac (simpset() addsimps [DIVISION_BY_ZERO]) 1);
- by (simp_tac (simpset() addsimps [numeral_0_eq_0, DIVISION_BY_ZERO_MOD]) 1);
-by (auto_tac (claset() addSEs [nonneg_eq_int], simpset()));
-by (rename_tac "m m'" 1);
-by (subgoal_tac "0 <= int m mod int m'" 1);
- by (asm_full_simp_tac 
-     (simpset() addsimps [nat_less_iff, numeral_0_eq_0, pos_mod_sign]) 2);
-by (rtac (inj_int RS injD) 1);
-by (Asm_simp_tac 1);
-by (res_inst_tac [("q", "int (m div m')")] quorem_mod 1);
- by (Force_tac 2);
-by (asm_full_simp_tac 
-     (simpset() addsimps [nat_less_iff RS sym, quorem_def, 
-		          numeral_0_eq_0, zadd_int, zmult_int]) 1);
-qed "nat_mod_distrib";
-
 Goal "(number_of v :: nat)  mod  number_of v' = \
 \       (if neg (number_of v) then 0 \
 \        else if neg (number_of v') then number_of v \
@@ -471,16 +453,6 @@
 qed "eq_number_of_Pls_Min"; 
 
 
-(*** Further lemmas about "nat" ***)
-
-Goal "nat (abs (w * z)) = nat (abs w) * nat (abs z)";
-by (case_tac "z=0 | w=0" 1);
-by Auto_tac;  
-by (simp_tac (simpset() addsimps [zabs_def, nat_mult_distrib RS sym, 
-                          nat_mult_distrib_neg RS sym, zmult_less_0_iff]) 1);
-by (arith_tac 1);
-qed "nat_abs_mult_distrib";
-
 (*Distributive laws for literals*)
 Addsimps (map (inst "k" "number_of ?v")
 	  [add_mult_distrib, add_mult_distrib2,
diff -r 6d0392fc6dc5 -r 8dd150d36c65 src/HOL/MicroJava/Comp/CorrComp.thy
--- a/src/HOL/MicroJava/Comp/CorrComp.thy	Thu Feb 27 18:21:42 2003 +0100
+++ b/src/HOL/MicroJava/Comp/CorrComp.thy	Thu Feb 27 18:22:49 2003 +0100
@@ -465,7 +465,7 @@
 
 (* case v1 = v2 *)
 apply (rule_tac "instrs1.0" = "[LitPush (Bool True)]" in jump_fwd_progression)
-apply (auto simp: NatBin.nat_add_distrib)
+apply (auto simp: nat_add_distrib)
 apply (rule progression_one_step) apply simp
 
 (* case v1 \<noteq> v2 *)
@@ -474,7 +474,7 @@
 apply (rule progression_one_step [THEN HOL.refl [THEN progression_transitive], simplified]) 
 apply auto
 apply (rule_tac "instrs1.0" = "[]" in jump_fwd_progression)
-apply (auto simp: NatBin.nat_add_distrib intro: progression_refl)
+apply (auto simp: nat_add_distrib intro: progression_refl)
 done
 
 
@@ -1008,14 +1008,14 @@
 apply fast
 apply (rule_tac "instrs1.0" = "[]" in jump_fwd_progression)
 apply (simp, rule conjI, (rule HOL.refl)+)
-apply simp apply (rule conjI, simp) apply (simp add: NatBin.nat_add_distrib)
+apply simp apply (rule conjI, simp) apply (simp add: nat_add_distrib)
 apply (rule progression_refl)
 
  (* case b= False *)
 apply simp
 apply (rule_tac "instrs1.0" = "compStmt (gmb G CL S) c2" in jump_fwd_progression)
 apply (simp, rule conjI, (rule HOL.refl)+)
-apply (simp, rule conjI, rule HOL.refl, simp add: NatBin.nat_add_distrib)
+apply (simp, rule conjI, rule HOL.refl, simp add: nat_add_distrib)
 apply fast
 
 (* case exit Loop *)
@@ -1043,7 +1043,7 @@
 apply fast
 apply (rule_tac "instrs1.0" = "[]" in jump_fwd_progression)
 apply (simp, rule conjI, rule HOL.refl, rule HOL.refl)
-apply (simp, rule conjI, rule HOL.refl, simp add: NatBin.nat_add_distrib)
+apply (simp, rule conjI, rule HOL.refl, simp add: nat_add_distrib)
 apply (rule progression_refl)
 
 
diff -r 6d0392fc6dc5 -r 8dd150d36c65 src/HOL/NumberTheory/IntPrimes.thy
--- a/src/HOL/NumberTheory/IntPrimes.thy	Thu Feb 27 18:21:42 2003 +0100
+++ b/src/HOL/NumberTheory/IntPrimes.thy	Thu Feb 27 18:22:49 2003 +0100
@@ -50,10 +50,6 @@
   "[a = b] (mod m) == m dvd (a - b)"
 
 
-lemma zabs_eq_iff:
-    "(abs (z::int) = w) = (z = w \<and> 0 <= z \<or> z = -w \<and> z < 0)"
-  by (auto simp add: zabs_def)
-
 
 text {* \medskip @{term gcd} lemmas *}
 
@@ -66,167 +62,6 @@
   done
 
 
-subsection {* Divides relation *}
-
-lemma zdvd_0_right [iff]: "(m::int) dvd 0"
-  apply (unfold dvd_def)
-  apply (blast intro: zmult_0_right [symmetric])
-  done
-
-lemma zdvd_0_left [iff]: "(0 dvd (m::int)) = (m = 0)"
-  by (unfold dvd_def, auto)
-
-lemma zdvd_1_left [iff]: "1 dvd (m::int)"
-  by (unfold dvd_def, simp)
-
-lemma zdvd_refl [simp]: "m dvd (m::int)"
-  apply (unfold dvd_def)
-  apply (blast intro: zmult_1_right [symmetric])
-  done
-
-lemma zdvd_trans: "m dvd n ==> n dvd k ==> m dvd (k::int)"
-  apply (unfold dvd_def)
-  apply (blast intro: zmult_assoc)
-  done
-
-lemma zdvd_zminus_iff: "(m dvd -n) = (m dvd (n::int))"
-  apply (unfold dvd_def, auto)
-   apply (rule_tac [!] x = "-k" in exI, auto)
-  done
-
-lemma zdvd_zminus2_iff: "(-m dvd n) = (m dvd (n::int))"
-  apply (unfold dvd_def, auto)
-   apply (rule_tac [!] x = "-k" in exI, auto)
-  done
-
-lemma zdvd_anti_sym:
-    "0 < m ==> 0 < n ==> m dvd n ==> n dvd m ==> m = (n::int)"
-  apply (unfold dvd_def, auto)
-  apply (simp add: zmult_assoc zmult_eq_self_iff int_0_less_mult_iff zmult_eq_1_iff)
-  done
-
-lemma zdvd_zadd: "k dvd m ==> k dvd n ==> k dvd (m + n :: int)"
-  apply (unfold dvd_def)
-  apply (blast intro: zadd_zmult_distrib2 [symmetric])
-  done
-
-lemma zdvd_zdiff: "k dvd m ==> k dvd n ==> k dvd (m - n :: int)"
-  apply (unfold dvd_def)
-  apply (blast intro: zdiff_zmult_distrib2 [symmetric])
-  done
-
-lemma zdvd_zdiffD: "k dvd m - n ==> k dvd n ==> k dvd (m::int)"
-  apply (subgoal_tac "m = n + (m - n)")
-   apply (erule ssubst)
-   apply (blast intro: zdvd_zadd, simp)
-  done
-
-lemma zdvd_zmult: "k dvd (n::int) ==> k dvd m * n"
-  apply (unfold dvd_def)
-  apply (blast intro: zmult_left_commute)
-  done
-
-lemma zdvd_zmult2: "k dvd (m::int) ==> k dvd m * n"
-  apply (subst zmult_commute)
-  apply (erule zdvd_zmult)
-  done
-
-lemma [iff]: "(k::int) dvd m * k"
-  apply (rule zdvd_zmult)
-  apply (rule zdvd_refl)
-  done
-
-lemma [iff]: "(k::int) dvd k * m"
-  apply (rule zdvd_zmult2)
-  apply (rule zdvd_refl)
-  done
-
-lemma zdvd_zmultD2: "j * k dvd n ==> j dvd (n::int)"
-  apply (unfold dvd_def)
-  apply (simp add: zmult_assoc, blast)
-  done
-
-lemma zdvd_zmultD: "j * k dvd n ==> k dvd (n::int)"
-  apply (rule zdvd_zmultD2)
-  apply (subst zmult_commute, assumption)
-  done
-
-lemma zdvd_zmult_mono: "i dvd m ==> j dvd (n::int) ==> i * j dvd m * n"
-  apply (unfold dvd_def, clarify)
-  apply (rule_tac x = "k * ka" in exI)
-  apply (simp add: zmult_ac)
-  done
-
-lemma zdvd_reduce: "(k dvd n + k * m) = (k dvd (n::int))"
-  apply (rule iffI)
-   apply (erule_tac [2] zdvd_zadd)
-   apply (subgoal_tac "n = (n + k * m) - k * m")
-    apply (erule ssubst)
-    apply (erule zdvd_zdiff, simp_all)
-  done
-
-lemma zdvd_zmod: "f dvd m ==> f dvd (n::int) ==> f dvd m mod n"
-  apply (unfold dvd_def)
-  apply (auto simp add: zmod_zmult_zmult1)
-  done
-
-lemma zdvd_zmod_imp_zdvd: "k dvd m mod n ==> k dvd n ==> k dvd (m::int)"
-  apply (subgoal_tac "k dvd n * (m div n) + m mod n")
-   apply (simp add: zmod_zdiv_equality [symmetric])
-  apply (simp only: zdvd_zadd zdvd_zmult2)
-  done
-
-lemma zdvd_iff_zmod_eq_0: "(k dvd n) = (n mod (k::int) = 0)"
-  by (unfold dvd_def, auto)
-
-lemma zdvd_not_zless: "0 < m ==> m < n ==> \<not> n dvd (m::int)"
-  apply (unfold dvd_def, auto)
-  apply (subgoal_tac "0 < n")
-   prefer 2
-   apply (blast intro: zless_trans)
-  apply (simp add: int_0_less_mult_iff)
-  apply (subgoal_tac "n * k < n * 1")
-   apply (drule zmult_zless_cancel1 [THEN iffD1], auto)
-  done
-
-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 zabs_eq_iff)
-   apply (rule_tac [2] x = "-(int k)" in exI)
-  apply (auto simp add: zmult_int [symmetric])
-  done
-
-lemma dvd_int_iff: "(z dvd int m) = (nat (abs z) dvd m)"
-  apply (auto simp add: dvd_def zabs_def zmult_int [symmetric])
-    apply (rule_tac [3] x = "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] k = m in int_less_0_conv)
-    apply (cut_tac k = m in int_less_0_conv)
-    apply (auto simp add: int_0_le_mult_iff zmult_less_0_iff
-      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)"
-  apply (auto simp add: dvd_def zmult_int [symmetric])
-  apply (rule_tac x = "nat k" in exI)
-  apply (cut_tac k = m in int_less_0_conv)
-  apply (auto simp add: int_0_le_mult_iff zmult_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)
-   apply (rule_tac [!] x = "-k" in exI, auto)
-  done
-
-lemma dvd_zminus_iff [iff]: "(z dvd -w) = (z dvd (w::int))"
-  apply (auto simp add: dvd_def)
-   apply (drule zminus_equation [THEN iffD1])
-   apply (rule_tac [!] x = "-k" in exI, auto)
-  done
-
-
 subsection {* Euclid's Algorithm and GCD *}
 
 lemma zgcd_0 [simp]: "zgcd (m, 0) = abs m"
@@ -322,6 +157,14 @@
 lemma zgcd_geq_zero: "0 <= zgcd(x,y)"
   by (auto simp add: zgcd_def)
 
+text{*This is merely a sanity check on zprime, since the previous version
+      denoted the empty set.*}
+lemma "2 \<in> zprime"
+  apply (auto simp add: zprime_def) 
+  apply (frule zdvd_imp_le, simp) 
+  apply (auto simp add: order_le_less dvd_def) 
+  done
+
 lemma zprime_imp_zrelprime:
     "p \<in> zprime ==> \<not> p dvd n ==> zgcd (n, p) = 1"
   apply (auto simp add: zprime_def)
@@ -688,8 +531,7 @@
 lemma xzgcd_linear:
     "0 < n ==> xzgcd m n = (r, s, t) ==> r = s * m + t * n"
   apply (unfold xzgcd_def)
-  apply (erule xzgcda_linear, assumption)
-   apply auto
+  apply (erule xzgcda_linear, assumption, auto)
   done
 
 lemma zgcd_ex_linear: