src/HOL/GCD.thy
changeset 60162 645058aa9d6f
parent 59977 ad2d1cd53877
child 60357 bc0827281dc1
     1.1 --- a/src/HOL/GCD.thy	Wed Apr 29 14:04:22 2015 +0100
     1.2 +++ b/src/HOL/GCD.thy	Thu Apr 30 15:28:01 2015 +0100
     1.3 @@ -755,24 +755,16 @@
     1.4  done
     1.5  
     1.6  lemma coprime_exp_nat: "coprime (d::nat) a \<Longrightarrow> coprime d (a^n)"
     1.7 -  by (induct n, simp_all add: coprime_mult_nat)
     1.8 +  by (induct n, simp_all add: power_Suc coprime_mult_nat)
     1.9  
    1.10  lemma coprime_exp_int: "coprime (d::int) a \<Longrightarrow> coprime d (a^n)"
    1.11 -  by (induct n, simp_all add: coprime_mult_int)
    1.12 +  by (induct n, simp_all add: power_Suc coprime_mult_int)
    1.13  
    1.14  lemma coprime_exp2_nat [intro]: "coprime (a::nat) b \<Longrightarrow> coprime (a^n) (b^m)"
    1.15 -  apply (rule coprime_exp_nat)
    1.16 -  apply (subst gcd_commute_nat)
    1.17 -  apply (rule coprime_exp_nat)
    1.18 -  apply (subst gcd_commute_nat, assumption)
    1.19 -done
    1.20 +  by (simp add: coprime_exp_nat gcd_nat.commute)
    1.21  
    1.22  lemma coprime_exp2_int [intro]: "coprime (a::int) b \<Longrightarrow> coprime (a^n) (b^m)"
    1.23 -  apply (rule coprime_exp_int)
    1.24 -  apply (subst gcd_commute_int)
    1.25 -  apply (rule coprime_exp_int)
    1.26 -  apply (subst gcd_commute_int, assumption)
    1.27 -done
    1.28 +  by (simp add: coprime_exp_int gcd_int.commute)
    1.29  
    1.30  lemma gcd_exp_nat: "gcd ((a::nat)^n) (b^n) = (gcd a b)^n"
    1.31  proof (cases)
    1.32 @@ -783,24 +775,11 @@
    1.33      by (auto simp:div_gcd_coprime_nat)
    1.34    hence "gcd ((a div gcd a b)^n * (gcd a b)^n)
    1.35        ((b div gcd a b)^n * (gcd a b)^n) = (gcd a b)^n"
    1.36 -    apply (subst (1 2) mult.commute)
    1.37 -    apply (subst gcd_mult_distrib_nat [symmetric])
    1.38 -    apply simp
    1.39 -    done
    1.40 +    by (metis gcd_mult_distrib_nat mult.commute mult.right_neutral)
    1.41    also have "(a div gcd a b)^n * (gcd a b)^n = a^n"
    1.42 -    apply (subst div_power)
    1.43 -    apply auto
    1.44 -    apply (rule dvd_div_mult_self)
    1.45 -    apply (rule dvd_power_same)
    1.46 -    apply auto
    1.47 -    done
    1.48 +    by (metis dvd_div_mult_self gcd_unique_nat power_mult_distrib)
    1.49    also have "(b div gcd a b)^n * (gcd a b)^n = b^n"
    1.50 -    apply (subst div_power)
    1.51 -    apply auto
    1.52 -    apply (rule dvd_div_mult_self)
    1.53 -    apply (rule dvd_power_same)
    1.54 -    apply auto
    1.55 -    done
    1.56 +    by (metis dvd_div_mult_self gcd_unique_nat power_mult_distrib)
    1.57    finally show ?thesis .
    1.58  qed
    1.59  
    1.60 @@ -908,7 +887,7 @@
    1.61      have "a' dvd a'^n" by (simp add: m)
    1.62      with th0 have "a' dvd b'^n"
    1.63        using dvd_trans[of a' "a'^n" "b'^n"] by simp
    1.64 -    hence th1: "a' dvd b'^m * b'" by (simp add: m mult.commute)
    1.65 +    hence th1: "a' dvd b'^m * b'" by (simp add: m mult.commute power_Suc)
    1.66      from coprime_dvd_mult_int[OF coprime_exp_int [OF ab'(3), of m]] th1
    1.67      have "a' dvd b'" by (subst (asm) mult.commute, blast)
    1.68      hence "a'*?g dvd b'*?g" by simp
    1.69 @@ -947,21 +926,13 @@
    1.70  qed
    1.71  
    1.72  lemma coprime_plus_one_nat [simp]: "coprime ((n::nat) + 1) n"
    1.73 -  apply (subgoal_tac "gcd (n + 1) n dvd (n + 1 - n)")
    1.74 -  apply force
    1.75 -  apply (rule dvd_diff_nat)
    1.76 -  apply auto
    1.77 -done
    1.78 +  by (simp add: gcd_nat.commute)
    1.79  
    1.80  lemma coprime_Suc_nat [simp]: "coprime (Suc n) n"
    1.81    using coprime_plus_one_nat by (simp add: One_nat_def)
    1.82  
    1.83  lemma coprime_plus_one_int [simp]: "coprime ((n::int) + 1) n"
    1.84 -  apply (subgoal_tac "gcd (n + 1) n dvd (n + 1 - n)")
    1.85 -  apply force
    1.86 -  apply (rule dvd_diff)
    1.87 -  apply auto
    1.88 -done
    1.89 +  by (simp add: gcd_int.commute)
    1.90  
    1.91  lemma coprime_minus_one_nat: "(n::nat) \<noteq> 0 \<Longrightarrow> coprime (n - 1) n"
    1.92    using coprime_plus_one_nat [of "n - 1"]
    1.93 @@ -985,36 +956,23 @@
    1.94    apply (auto simp add: gcd_mult_cancel_int)
    1.95  done
    1.96  
    1.97 -lemma coprime_common_divisor_nat: "coprime (a::nat) b \<Longrightarrow> x dvd a \<Longrightarrow>
    1.98 -    x dvd b \<Longrightarrow> x = 1"
    1.99 -  apply (subgoal_tac "x dvd gcd a b")
   1.100 -  apply simp
   1.101 -  apply (erule (1) gcd_greatest)
   1.102 -done
   1.103 +lemma coprime_common_divisor_nat: 
   1.104 +    "coprime (a::nat) b \<Longrightarrow> x dvd a \<Longrightarrow> x dvd b \<Longrightarrow> x = 1"
   1.105 +  by (metis gcd_greatest_iff_nat nat_dvd_1_iff_1)
   1.106  
   1.107 -lemma coprime_common_divisor_int: "coprime (a::int) b \<Longrightarrow> x dvd a \<Longrightarrow>
   1.108 -    x dvd b \<Longrightarrow> abs x = 1"
   1.109 -  apply (subgoal_tac "x dvd gcd a b")
   1.110 -  apply simp
   1.111 -  apply (erule (1) gcd_greatest)
   1.112 -done
   1.113 +lemma coprime_common_divisor_int:
   1.114 +    "coprime (a::int) b \<Longrightarrow> x dvd a \<Longrightarrow> x dvd b \<Longrightarrow> abs x = 1"
   1.115 +  using gcd_greatest by fastforce
   1.116  
   1.117 -lemma coprime_divisors_nat: "(d::int) dvd a \<Longrightarrow> e dvd b \<Longrightarrow> coprime a b \<Longrightarrow>
   1.118 -    coprime d e"
   1.119 -  apply (auto simp add: dvd_def)
   1.120 -  apply (frule coprime_lmult_int)
   1.121 -  apply (subst gcd_commute_int)
   1.122 -  apply (subst (asm) (2) gcd_commute_int)
   1.123 -  apply (erule coprime_lmult_int)
   1.124 -done
   1.125 +lemma coprime_divisors_nat:
   1.126 +    "(d::int) dvd a \<Longrightarrow> e dvd b \<Longrightarrow> coprime a b \<Longrightarrow> coprime d e"
   1.127 +  by (meson coprime_int dvd_trans gcd_dvd1 gcd_dvd2 gcd_ge_0_int)
   1.128  
   1.129  lemma invertible_coprime_nat: "(x::nat) * y mod m = 1 \<Longrightarrow> coprime x m"
   1.130 -apply (metis coprime_lmult_nat gcd_1_nat gcd_commute_nat gcd_red_nat)
   1.131 -done
   1.132 +by (metis coprime_lmult_nat gcd_1_nat gcd_commute_nat gcd_red_nat)
   1.133  
   1.134  lemma invertible_coprime_int: "(x::int) * y mod m = 1 \<Longrightarrow> coprime x m"
   1.135 -apply (metis coprime_lmult_int gcd_1_int gcd_commute_int gcd_red_int)
   1.136 -done
   1.137 +by (metis coprime_lmult_int gcd_1_int gcd_commute_int gcd_red_int)
   1.138  
   1.139  
   1.140  subsection {* Bezout's theorem *}