src/HOL/GCD.thy
changeset 30082 43c5b7bfc791
parent 30042 31039ee583fa
child 30242 aea5d7fa7ef5
     1.1 --- a/src/HOL/GCD.thy	Tue Feb 24 11:10:05 2009 -0800
     1.2 +++ b/src/HOL/GCD.thy	Tue Feb 24 11:12:58 2009 -0800
     1.3 @@ -60,9 +60,12 @@
     1.4  lemma gcd_non_0: "n > 0 \<Longrightarrow> gcd m n = gcd n (m mod n)"
     1.5    by simp
     1.6  
     1.7 -lemma gcd_1 [simp, algebra]: "gcd m (Suc 0) = 1"
     1.8 +lemma gcd_1 [simp, algebra]: "gcd m (Suc 0) = Suc 0"
     1.9    by simp
    1.10  
    1.11 +lemma nat_gcd_1_right [simp, algebra]: "gcd m 1 = 1"
    1.12 +  unfolding One_nat_def by (rule gcd_1)
    1.13 +
    1.14  declare gcd.simps [simp del]
    1.15  
    1.16  text {*
    1.17 @@ -116,9 +119,12 @@
    1.18    apply (blast intro: dvd_trans)
    1.19    done
    1.20  
    1.21 -lemma gcd_1_left [simp, algebra]: "gcd (Suc 0) m = 1"
    1.22 +lemma gcd_1_left [simp, algebra]: "gcd (Suc 0) m = Suc 0"
    1.23    by (simp add: gcd_commute)
    1.24  
    1.25 +lemma nat_gcd_1_left [simp, algebra]: "gcd 1 m = 1"
    1.26 +  unfolding One_nat_def by (rule gcd_1_left)
    1.27 +
    1.28  text {*
    1.29    \medskip Multiplication laws
    1.30  *}