src/HOL/Library/Primes.thy
changeset 15628 9f912f8fd2df
parent 15140 322485b816ac
child 16663 13e9c402308b
     1.1 --- a/src/HOL/Library/Primes.thy	Fri Mar 25 14:14:01 2005 +0100
     1.2 +++ b/src/HOL/Library/Primes.thy	Fri Mar 25 16:20:57 2005 +0100
     1.3 @@ -210,11 +210,13 @@
     1.4    done
     1.5  
     1.6  lemma gcd_add2 [simp]: "gcd (m, m + n) = gcd (m, n)"
     1.7 -  apply (rule gcd_commute [THEN trans])
     1.8 -  apply (subst add_commute)
     1.9 -  apply (simp add: gcd_add1)
    1.10 -  apply (rule gcd_commute)
    1.11 -  done
    1.12 +proof -
    1.13 +  have "gcd (m, m + n) = gcd (m + n, m)" by (rule gcd_commute) 
    1.14 +  also have "... = gcd (n + m, m)" by (simp add: add_commute)
    1.15 +  also have "... = gcd (n, m)" by simp
    1.16 +  also have  "... = gcd (m, n)" by (rule gcd_commute) 
    1.17 +  finally show ?thesis .
    1.18 +qed
    1.19  
    1.20  lemma gcd_add2' [simp]: "gcd (m, n + m) = gcd (m, n)"
    1.21    apply (subst add_commute)
    1.22 @@ -223,7 +225,7 @@
    1.23  
    1.24  lemma gcd_add_mult: "gcd (m, k * m + n) = gcd (m, n)"
    1.25    apply (induct k)
    1.26 -   apply (simp_all add: gcd_add2 add_assoc)
    1.27 +   apply (simp_all add: add_assoc)
    1.28    done
    1.29  
    1.30  
    1.31 @@ -235,8 +237,8 @@
    1.32      apply (rule_tac n = k in relprime_dvd_mult)
    1.33       apply (simp add: gcd_assoc)
    1.34       apply (simp add: gcd_commute)
    1.35 -    apply (simp_all add: mult_commute gcd_dvd1 gcd_dvd2)
    1.36 -  apply (blast intro: gcd_dvd1 dvd_trans)
    1.37 +    apply (simp_all add: mult_commute)
    1.38 +  apply (blast intro: dvd_trans)
    1.39    done
    1.40  
    1.41  end