equal
deleted
inserted
replaced
69 |
69 |
70 @{thm[display] sym} |
70 @{thm[display] sym} |
71 \rulename{sym} |
71 \rulename{sym} |
72 *}; |
72 *}; |
73 |
73 |
74 lemmas gcd_mult = gcd_mult_1 [THEN sym]; |
74 lemmas gcd_mult0 = gcd_mult_1 [THEN sym]; |
75 |
75 (*not quite right: we need ?k but this gives k*) |
76 lemmas gcd_mult = gcd_mult_distrib2 [of k 1, simplified, THEN sym]; |
76 |
|
77 lemmas gcd_mult0' = gcd_mult_distrib2 [of k 1, simplified, THEN sym]; |
77 (*better in one step!*) |
78 (*better in one step!*) |
78 |
79 |
79 text {* |
80 text {* |
80 more legible |
81 more legible, and variables properly generalized |
81 *}; |
82 *}; |
82 |
83 |
83 lemma gcd_mult [simp]: "gcd(k, k*n) = k" |
84 lemma gcd_mult [simp]: "gcd(k, k*n) = k" |
84 by (rule gcd_mult_distrib2 [of k 1, simplified, THEN sym]) |
85 by (rule gcd_mult_distrib2 [of k 1, simplified, THEN sym]) |
85 |
86 |
86 |
87 |
87 lemmas gcd_self = gcd_mult [of k 1, simplified]; |
88 lemmas gcd_self0 = gcd_mult [of k 1, simplified]; |
88 |
89 |
89 |
90 |
90 text {* |
91 text {* |
91 Rules handy with THEN |
92 Rules handy with THEN |
92 |
93 |
97 \rulename{iffD2} |
98 \rulename{iffD2} |
98 *}; |
99 *}; |
99 |
100 |
100 |
101 |
101 text {* |
102 text {* |
102 again: more legible |
103 again: more legible, and variables properly generalized |
103 *}; |
104 *}; |
104 |
105 |
105 lemma gcd_self [simp]: "gcd(k,k) = k" |
106 lemma gcd_self [simp]: "gcd(k,k) = k" |
106 by (rule gcd_mult [of k 1, simplified]) |
107 by (rule gcd_mult [of k 1, simplified]) |
107 |
108 |