Reorganized, moving many results about the integer dvd relation from IntPrimes
to main HOL (IntDiv)
--- 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";
--- 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)")
--- 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";
--- 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
--- 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,
--- 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)
--- 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: