# HG changeset patch # User chaieb # Date 1216044835 -7200 # Node ID c8419e8a2d83e95c9817ed46b2ee8eff9a959bcf # Parent 9949dc7a24de48743b163ad8288764bef0e0a9d1 Simple theorems about zgcd moved to GCD.thy diff -r 9949dc7a24de -r c8419e8a2d83 src/HOL/NumberTheory/IntPrimes.thy --- 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 \ 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 \ 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 \ k dvd m \ 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 \ 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 \ 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 \ 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 \ 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 \ 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 \ m") @@ -172,7 +84,7 @@ lemma zprime_zdvd_zmult: "0 \ (m::int) ==> zprime p ==> p dvd m * n ==> p dvd m \ 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 \ zgcd n m = m" @@ -437,7 +349,7 @@ done lemma xzgcd_correct: - "0 < n ==> zgcd m n = k \ (\s t. xzgcd m n = (k, s, t))" + "0 < n ==> (zgcd m n = k) = (\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])