--- a/src/HOL/NumberTheory/IntPrimes.thy Mon Jul 14 16:13:51 2008 +0200
+++ b/src/HOL/NumberTheory/IntPrimes.thy Mon Jul 14 16:13:55 2008 +0200
@@ -45,100 +45,12 @@
zcong :: "int => int => int => bool" ("(1[_ = _] '(mod _'))") where
"[a = b] (mod m) = (m dvd (a - b))"
-
-
-text {* \medskip @{term gcd} lemmas *}
-
-lemma gcd_add1_eq: "gcd (m + k) k = gcd (m + k) m"
- by (simp add: gcd_commute)
-
-lemma gcd_diff2: "m \<le> n ==> gcd n (n - m) = gcd n m"
- apply (subgoal_tac "n = m + (n - m)")
- apply (erule ssubst, rule gcd_add1_eq, simp)
- done
-
-
subsection {* Euclid's Algorithm and GCD *}
-lemma zgcd_0 [simp]: "zgcd m 0 = abs m"
- by (simp add: zgcd_def abs_if)
-
-lemma zgcd_0_left [simp]: "zgcd 0 m = abs m"
- by (simp add: zgcd_def abs_if)
-
-lemma zgcd_zminus [simp]: "zgcd (-m) n = zgcd m n"
- by (simp add: zgcd_def)
-
-lemma zgcd_zminus2 [simp]: "zgcd m (-n) = zgcd m n"
- by (simp add: zgcd_def)
-
-lemma zgcd_non_0: "0 < n ==> zgcd m n = zgcd n (m mod n)"
- apply (frule_tac b = n and a = m in pos_mod_sign)
- apply (simp del: pos_mod_sign add: zgcd_def abs_if nat_mod_distrib)
- apply (auto simp add: gcd_non_0 nat_mod_distrib [symmetric] zmod_zminus1_eq_if)
- apply (frule_tac a = m in pos_mod_bound)
- apply (simp del: pos_mod_bound add: nat_diff_distrib gcd_diff2 nat_le_eq_zle)
- done
-
-lemma zgcd_eq: "zgcd m n = zgcd n (m mod n)"
- apply (case_tac "n = 0", simp add: DIVISION_BY_ZERO)
- apply (auto simp add: linorder_neq_iff zgcd_non_0)
- apply (cut_tac m = "-m" and n = "-n" in zgcd_non_0, auto)
- done
-
-lemma zgcd_1 [simp]: "zgcd m 1 = 1"
- by (simp add: zgcd_def abs_if)
-
-lemma zgcd_0_1_iff [simp]: "zgcd 0 m = 1 \<longleftrightarrow> abs m = 1"
- by (simp add: zgcd_def abs_if)
-
-lemma zgcd_zdvd1 [iff]: "zgcd m n dvd m"
- by (simp add: zgcd_def abs_if int_dvd_iff)
-
-lemma zgcd_zdvd2 [iff]: "zgcd m n dvd n"
- by (simp add: zgcd_def abs_if int_dvd_iff)
-
-lemma zgcd_greatest_iff: "k dvd zgcd m n \<longleftrightarrow> k dvd m \<and> k dvd n"
- by (simp add: zgcd_def abs_if int_dvd_iff dvd_int_iff nat_dvd_iff)
-
-lemma zgcd_commute: "zgcd m n = zgcd n m"
- by (simp add: zgcd_def gcd_commute)
-
-lemma zgcd_1_left [simp]: "zgcd 1 m = 1"
- by (simp add: zgcd_def gcd_1_left)
-
-lemma zgcd_assoc: "zgcd (zgcd k m) n = zgcd k (zgcd m n)"
- by (simp add: zgcd_def gcd_assoc)
-
-lemma zgcd_left_commute: "zgcd k (zgcd m n) = zgcd m (zgcd k n)"
- apply (rule zgcd_commute [THEN trans])
- apply (rule zgcd_assoc [THEN trans])
- apply (rule zgcd_commute [THEN arg_cong])
- done
-
-lemmas zgcd_ac = zgcd_assoc zgcd_commute zgcd_left_commute
- -- {* addition is an AC-operator *}
-
-lemma zgcd_zmult_distrib2: "0 \<le> k ==> k * zgcd m n = zgcd (k * m) (k * n)"
- by (simp del: minus_mult_right [symmetric]
- add: minus_mult_right nat_mult_distrib zgcd_def abs_if
- mult_less_0_iff gcd_mult_distrib2 [symmetric] zmult_int [symmetric])
-
-lemma zgcd_zmult_distrib2_abs: "zgcd (k * m) (k * n) = abs k * zgcd m n"
- by (simp add: abs_if zgcd_zmult_distrib2)
-
-lemma zgcd_self [simp]: "0 \<le> m ==> zgcd m m = m"
- by (cut_tac k = m and m = 1 and n = 1 in zgcd_zmult_distrib2, simp_all)
-
-lemma zgcd_zmult_eq_self [simp]: "0 \<le> k ==> zgcd k (k * n) = k"
- by (cut_tac k = k and m = 1 and n = n in zgcd_zmult_distrib2, simp_all)
-
-lemma zgcd_zmult_eq_self2 [simp]: "0 \<le> k ==> zgcd (k * n) k = k"
- by (cut_tac k = k and m = n and n = 1 in zgcd_zmult_distrib2, simp_all)
lemma zrelprime_zdvd_zmult_aux:
"zgcd n k = 1 ==> k dvd m * n ==> 0 \<le> m ==> k dvd m"
- by (metis abs_of_nonneg zdvd_triv_right zgcd_greatest_iff zgcd_zmult_distrib2_abs zmult_1_right)
+ by (metis abs_of_nonneg zdvd_triv_right zgcd_greatest_iff zgcd_zmult_distrib2_abs zmult_1_right)
lemma zrelprime_zdvd_zmult: "zgcd n k = 1 ==> k dvd m * n ==> k dvd m"
apply (case_tac "0 \<le> m")
@@ -172,7 +84,7 @@
lemma zprime_zdvd_zmult:
"0 \<le> (m::int) ==> zprime p ==> p dvd m * n ==> p dvd m \<or> p dvd n"
- by (metis zgcd_dvd1 zgcd_dvd2 zgcd_pos zprime_def zrelprime_dvd_mult)
+ by (metis zgcd_zdvd1 zgcd_zdvd2 zgcd_pos zprime_def zrelprime_dvd_mult)
lemma zgcd_zadd_zmult [simp]: "zgcd (m + n * k) n = zgcd m n"
apply (rule zgcd_eq [THEN trans])
@@ -186,7 +98,7 @@
done
lemma zgcd_zmult_zdvd_zgcd:
- "zgcd k n = 1 ==> zgcd (k * m) n dvd zgcd m n"
+ "zgcd k n = 1 ==> zgcd (k * m) n dvd zgcd m n"
apply (simp add: zgcd_greatest_iff)
apply (rule_tac n = k in zrelprime_zdvd_zmult)
prefer 2
@@ -198,7 +110,7 @@
by (simp add: zgcd_def nat_abs_mult_distrib gcd_mult_cancel)
lemma zgcd_zgcd_zmult:
- "zgcd k m = 1 ==> zgcd n m = 1 ==> zgcd (k * n) m = 1"
+ "zgcd k m = 1 ==> zgcd n m = 1 ==> zgcd (k * n) m = 1"
by (simp add: zgcd_zmult_cancel)
lemma zdvd_iff_zgcd: "0 < m ==> m dvd n \<longleftrightarrow> zgcd n m = m"
@@ -437,7 +349,7 @@
done
lemma xzgcd_correct:
- "0 < n ==> zgcd m n = k \<longleftrightarrow> (\<exists>s t. xzgcd m n = (k, s, t))"
+ "0 < n ==> (zgcd m n = k) = (\<exists>s t. xzgcd m n = (k, s, t))"
apply (unfold xzgcd_def)
apply (rule iffI)
apply (rule_tac [2] xzgcd_correct_aux2 [THEN mp, THEN mp])