# HG changeset patch # User nipkow # Date 1245908052 -7200 # Node ID fe9a3043d36c13f7fd5a53e5bd8b460aac602fc0 # Parent d5a6096b94ade986781d0da1148b9d43ed58398e Cleaned up GCD diff -r d5a6096b94ad -r fe9a3043d36c src/HOL/GCD.thy --- a/src/HOL/GCD.thy Wed Jun 24 17:50:49 2009 +0200 +++ b/src/HOL/GCD.thy Thu Jun 25 07:34:12 2009 +0200 @@ -1,6 +1,6 @@ (* Title: GCD.thy Authors: Christophe Tabacznyj, Lawrence C. Paulson, Amine Chaieb, - Thomas M. Rasmussen, Jeremy Avigad + Thomas M. Rasmussen, Jeremy Avigad, Tobias Nipkow This file deals with the functions gcd and lcm, and properties of @@ -20,6 +20,7 @@ the congruence relations on the integers. The notion was extended to the natural numbers by Chiaeb. +Tobias Nipkow cleaned up a lot. *) @@ -247,11 +248,11 @@ lemma int_gcd_1 [simp]: "gcd (m::int) 1 = 1" by (simp add: gcd_int_def) -lemma nat_gcd_self [simp]: "gcd (x::nat) x = x" - by simp +lemma nat_gcd_idem: "gcd (x::nat) x = x" +by simp -lemma int_gcd_def [simp]: "gcd (x::int) x = abs x" - by (subst int_gcd_abs, auto simp add: gcd_int_def) +lemma int_gcd_idem: "gcd (x::int) x = abs x" +by (subst int_gcd_abs, auto simp add: gcd_int_def) declare gcd_nat.simps [simp del] @@ -267,8 +268,6 @@ apply (blast dest: dvd_mod_imp_dvd) done -thm nat_gcd_dvd1 [transferred] - lemma int_gcd_dvd1 [iff]: "gcd (x::int) y dvd x" apply (subst int_gcd_abs) apply (rule dvd_trans) @@ -308,7 +307,7 @@ by (rule zdvd_imp_le, auto) lemma nat_gcd_greatest: "(k::nat) dvd m \ k dvd n \ k dvd gcd m n" - by (induct m n rule: nat_gcd_induct) (simp_all add: nat_gcd_non_0 dvd_mod) +by (induct m n rule: nat_gcd_induct) (simp_all add: nat_gcd_non_0 dvd_mod) lemma int_gcd_greatest: assumes "(k::int) dvd m" and "k dvd n" @@ -364,15 +363,6 @@ lemmas int_gcd_ac = int_gcd_assoc int_gcd_commute int_gcd_left_commute -lemma nat_gcd_1_left [simp]: "gcd (1::nat) m = 1" - by (subst nat_gcd_commute, simp) - -lemma nat_gcd_Suc_0_left [simp]: "gcd (Suc 0) m = Suc 0" - by (subst nat_gcd_commute, simp add: One_nat_def) - -lemma int_gcd_1_left [simp]: "gcd (1::int) m = 1" - by (subst int_gcd_commute, simp) - lemma nat_gcd_unique: "(d::nat) dvd a \ d dvd b \ (\e. e dvd a \ e dvd b \ e dvd d) \ d = gcd a b" apply auto @@ -395,6 +385,19 @@ apply (auto intro: int_gcd_greatest) done +lemma gcd_proj1_if_dvd_nat [simp]: "(x::nat) dvd y \ gcd x y = x" +by (metis dvd.eq_iff nat_gcd_unique) + +lemma gcd_proj2_if_dvd_nat [simp]: "(y::nat) dvd x \ gcd x y = y" +by (metis dvd.eq_iff nat_gcd_unique) + +lemma gcd_proj1_if_dvd_int[simp]: "x dvd y \ gcd (x::int) y = abs x" +by (metis abs_dvd_iff abs_eq_0 int_gcd_0_left int_gcd_abs int_gcd_unique) + +lemma gcd_proj2_if_dvd_int[simp]: "y dvd x \ gcd (x::int) y = abs y" +by (metis gcd_proj1_if_dvd_int int_gcd_commute) + + text {* \medskip Multiplication laws *} @@ -414,12 +417,6 @@ apply auto done -lemma nat_gcd_mult [simp]: "gcd (k::nat) (k * n) = k" - by (rule nat_gcd_mult_distrib [of k 1 n, simplified, symmetric]) - -lemma int_gcd_mult [simp]: "gcd (k::int) (k * n) = abs k" - by (rule int_gcd_mult_distrib [of k 1 n, simplified, symmetric]) - lemma nat_coprime_dvd_mult: "coprime (k::nat) n \ k dvd m * n \ k dvd m" apply (insert nat_gcd_mult_distrib [of m k n]) apply simp @@ -517,42 +514,22 @@ done lemma int_gcd_add1 [simp]: "gcd ((m::int) + n) n = gcd m n" - apply (case_tac "n = 0", force) - apply (subst (1 2) int_gcd_red) - apply auto -done +by (metis int_gcd_red mod_add_self1 zadd_commute) lemma int_gcd_add2 [simp]: "gcd m ((m::int) + n) = gcd m n" - apply (subst int_gcd_commute) - apply (subst add_commute) - apply (subst int_gcd_add1) - apply (subst int_gcd_commute) - apply (rule refl) -done +by (metis int_gcd_add1 int_gcd_commute zadd_commute) lemma nat_gcd_add_mult: "gcd (m::nat) (k * m + n) = gcd m n" - by (induct k, simp_all add: ring_simps) +by (metis mod_mult_self3 nat_gcd_commute nat_gcd_red) lemma int_gcd_add_mult: "gcd (m::int) (k * m + n) = gcd m n" - apply (subgoal_tac "ALL s. ALL m. ALL n. - gcd m (int (s::nat) * m + n) = gcd m n") - apply (case_tac "k >= 0") - apply (drule_tac x = "nat k" in spec, force) - apply (subst (1 2) int_gcd_neg2 [symmetric]) - apply (drule_tac x = "nat (- k)" in spec) - apply (drule_tac x = "m" in spec) - apply (drule_tac x = "-n" in spec) - apply auto - apply (rule nat_induct) - apply auto - apply (auto simp add: left_distrib) - apply (subst add_assoc) - apply simp -done +by (metis int_gcd_commute int_gcd_red mod_mult_self1 zadd_commute) + (* to do: differences, and all variations of addition rules as simplification rules for nat and int *) +(* FIXME remove iff *) lemma nat_gcd_dvd_prod [iff]: "gcd (m::nat) n dvd k * n" using mult_dvd_mono [of 1] by auto @@ -714,20 +691,20 @@ qed lemma int_coprime_lmult: - assumes dab: "coprime (d::int) (a * b)" shows "coprime d a" + assumes "coprime (d::int) (a * b)" shows "coprime d a" proof - have "gcd d a dvd gcd d (a * b)" by (rule int_gcd_greatest, auto) - with dab show ?thesis + with assms show ?thesis by auto qed lemma nat_coprime_rmult: - assumes dab: "coprime (d::nat) (a * b)" shows "coprime d b" + assumes "coprime (d::nat) (a * b)" shows "coprime d b" proof - have "gcd d b dvd gcd d (a * b)" by (rule nat_gcd_greatest, auto intro: dvd_mult) - with dab show ?thesis + with assms show ?thesis by auto qed @@ -937,6 +914,7 @@ ultimately show ?thesis by blast qed +(* FIXME move to Divides(?) *) lemma nat_pow_divides_eq [simp]: "n ~= 0 \ ((a::nat)^n dvd b^n) = (a dvd b)" by (auto intro: nat_pow_divides_pow dvd_power_same) @@ -1316,30 +1294,12 @@ lemma int_lcm_0 [simp]: "lcm (m::int) 0 = 0" unfolding lcm_int_def by simp -lemma nat_lcm_1 [simp]: "lcm (m::nat) 1 = m" - unfolding lcm_nat_def by simp - -lemma nat_lcm_Suc_0 [simp]: "lcm (m::nat) (Suc 0) = m" - unfolding lcm_nat_def by (simp add: One_nat_def) - -lemma int_lcm_1 [simp]: "lcm (m::int) 1 = abs m" - unfolding lcm_int_def by simp - lemma nat_lcm_0_left [simp]: "lcm (0::nat) n = 0" unfolding lcm_nat_def by simp lemma int_lcm_0_left [simp]: "lcm (0::int) n = 0" unfolding lcm_int_def by simp -lemma nat_lcm_1_left [simp]: "lcm (1::nat) m = m" - unfolding lcm_nat_def by simp - -lemma nat_lcm_Suc_0_left [simp]: "lcm (Suc 0) m = m" - unfolding lcm_nat_def by (simp add: One_nat_def) - -lemma int_lcm_1_left [simp]: "lcm (1::int) m = abs m" - unfolding lcm_int_def by simp - lemma nat_lcm_commute: "lcm (m::nat) n = lcm n m" unfolding lcm_nat_def by (simp add: nat_gcd_commute ring_simps) @@ -1348,34 +1308,14 @@ lemma nat_lcm_pos: - assumes mpos: "(m::nat) > 0" - and npos: "n>0" - shows "lcm m n > 0" -proof(rule ccontr, simp add: lcm_nat_def nat_gcd_zero) - assume h:"m*n div gcd m n = 0" - from mpos npos have "gcd m n \ 0" using nat_gcd_zero by simp - hence gcdp: "gcd m n > 0" by simp - with h - have "m*n < gcd m n" - by (cases "m * n < gcd m n") - (auto simp add: div_if[OF gcdp, where m="m*n"]) - moreover - have "gcd m n dvd m" by simp - with mpos dvd_imp_le have t1:"gcd m n \ m" by simp - with npos have t1:"gcd m n*n \ m*n" by simp - have "gcd m n \ gcd m n*n" using npos by simp - with t1 have "gcd m n \ m*n" by arith - ultimately show "False" by simp -qed + "(m::nat) > 0 \ n>0 \ lcm m n > 0" +by (metis gr0I mult_is_0 nat_prod_gcd_lcm) lemma int_lcm_pos: - assumes mneq0: "(m::int) ~= 0" - and npos: "n ~= 0" - shows "lcm m n > 0" - + "(m::int) ~= 0 \ n ~= 0 \ lcm m n > 0" apply (subst int_lcm_abs) apply (rule nat_lcm_pos [transferred]) - using prems apply auto + apply auto done lemma nat_dvd_pos: @@ -1417,13 +1357,11 @@ qed lemma int_lcm_least: - assumes "(m::int) dvd k" and "n dvd k" - shows "lcm m n dvd k" - - apply (subst int_lcm_abs) - apply (rule dvd_trans) - apply (rule nat_lcm_least [transferred, of _ "abs k" _]) - using prems apply auto + "(m::int) dvd k \ n dvd k \ lcm m n dvd k" +apply (subst int_lcm_abs) +apply (rule dvd_trans) +apply (rule nat_lcm_least [transferred, of _ "abs k" _]) +apply auto done lemma nat_lcm_dvd1: "(m::nat) dvd lcm m n" @@ -1481,23 +1419,23 @@ (\e. a dvd e \ b dvd e \ d dvd e) \ d = lcm a b" by (auto intro: dvd_anti_sym [transferred] int_lcm_least) -lemma nat_lcm_dvd_eq [simp]: "(x::nat) dvd y \ lcm x y = y" +lemma lcm_proj2_if_dvd_nat [simp]: "(x::nat) dvd y \ lcm x y = y" apply (rule sym) apply (subst nat_lcm_unique [symmetric]) apply auto done -lemma int_lcm_dvd_eq [simp]: "0 <= y \ (x::int) dvd y \ lcm x y = y" +lemma lcm_proj2_if_dvd_int [simp]: "(x::int) dvd y \ lcm x y = abs y" apply (rule sym) apply (subst int_lcm_unique [symmetric]) apply auto done -lemma nat_lcm_dvd_eq' [simp]: "(x::nat) dvd y \ lcm y x = y" - by (subst nat_lcm_commute, erule nat_lcm_dvd_eq) +lemma lcm_proj1_if_dvd_nat [simp]: "(x::nat) dvd y \ lcm y x = y" +by (subst nat_lcm_commute, erule lcm_proj2_if_dvd_nat) -lemma int_lcm_dvd_eq' [simp]: "y >= 0 \ (x::int) dvd y \ lcm y x = y" - by (subst int_lcm_commute, erule (1) int_lcm_dvd_eq) +lemma lcm_proj1_if_dvd_int [simp]: "(x::int) dvd y \ lcm y x = abs y" +by (subst int_lcm_commute, erule lcm_proj2_if_dvd_int) lemma lcm_assoc_nat: "lcm (lcm n m) (p::nat) = lcm n (lcm m p)" diff -r d5a6096b94ad -r fe9a3043d36c src/HOL/NewNumberTheory/Residues.thy --- a/src/HOL/NewNumberTheory/Residues.thy Wed Jun 24 17:50:49 2009 +0200 +++ b/src/HOL/NewNumberTheory/Residues.thy Thu Jun 25 07:34:12 2009 +0200 @@ -202,9 +202,6 @@ apply (subgoal_tac "a mod m ~= 0") apply arith apply auto - apply (subst (asm) int_gcd_commute) - apply (subst (asm) int_gcd_mult) - apply auto apply (subst (asm) int_gcd_red) apply (subst int_gcd_commute, assumption) done