58 apply (simp add: gcd_non_0) |
58 apply (simp add: gcd_non_0) |
59 done |
59 done |
60 |
60 |
61 (*gcd(m,n) divides m and n. The conjunctions don't seem provable separately*) |
61 (*gcd(m,n) divides m and n. The conjunctions don't seem provable separately*) |
62 lemma gcd_dvd_both: "(gcd(m,n) dvd m) & (gcd(m,n) dvd n)" |
62 lemma gcd_dvd_both: "(gcd(m,n) dvd m) & (gcd(m,n) dvd n)" |
63 apply (rule_tac m="m" and n="n" in gcd_induct) |
63 apply (induct_tac m n rule: gcd_induct) |
64 apply (simp_all add: gcd_non_0) |
64 apply (simp_all add: gcd_non_0) |
65 apply (blast dest: dvd_mod_imp_dvd) |
65 apply (blast dest: dvd_mod_imp_dvd) |
66 done |
66 done |
67 |
67 |
68 lemmas gcd_dvd1 = gcd_dvd_both [THEN conjunct1]; |
68 lemmas gcd_dvd1 = gcd_dvd_both [THEN conjunct1]; |
70 |
70 |
71 |
71 |
72 (*Maximality: for all m,n,f naturals, |
72 (*Maximality: for all m,n,f naturals, |
73 if f divides m and f divides n then f divides gcd(m,n)*) |
73 if f divides m and f divides n then f divides gcd(m,n)*) |
74 lemma gcd_greatest [rulify]: "(f dvd m) --> (f dvd n) --> f dvd gcd(m,n)" |
74 lemma gcd_greatest [rulify]: "(f dvd m) --> (f dvd n) --> f dvd gcd(m,n)" |
75 apply (rule_tac m="m" and n="n" in gcd_induct) |
75 apply (induct_tac m n rule: gcd_induct) |
76 apply (simp_all add: gcd_non_0 dvd_mod); |
76 apply (simp_all add: gcd_non_0 dvd_mod); |
|
77 done; |
|
78 |
|
79 lemma gcd_greatest_iff [iff]: "f dvd gcd(m,n) = (f dvd m & f dvd n)" |
|
80 apply (blast intro!: gcd_dvd1 gcd_dvd2 intro: dvd_trans gcd_greatest); |
77 done; |
81 done; |
78 |
82 |
79 (*Function gcd yields the Greatest Common Divisor*) |
83 (*Function gcd yields the Greatest Common Divisor*) |
80 lemma is_gcd: "is_gcd (gcd(m,n)) m n" |
84 lemma is_gcd: "is_gcd (gcd(m,n)) m n" |
81 apply (simp add: is_gcd_def gcd_greatest gcd_dvd_both); |
85 apply (simp add: is_gcd_def gcd_greatest gcd_dvd_both); |
106 |
110 |
107 lemma gcd_assoc: "gcd(gcd(k,m),n) = gcd(k,gcd(m,n))" |
111 lemma gcd_assoc: "gcd(gcd(k,m),n) = gcd(k,gcd(m,n))" |
108 apply (rule is_gcd_unique) |
112 apply (rule is_gcd_unique) |
109 apply (rule is_gcd) |
113 apply (rule is_gcd) |
110 apply (simp add: is_gcd_def); |
114 apply (simp add: is_gcd_def); |
111 apply (blast intro!: gcd_dvd1 gcd_dvd2 intro: dvd_trans gcd_greatest); |
115 apply (blast intro!: gcd_dvd1 gcd_dvd2 intro: dvd_trans); |
112 done |
116 done |
113 |
117 |
114 lemma gcd_0_left [simp]: "gcd(0,m) = m" |
118 lemma gcd_0_left [simp]: "gcd(0,m) = m" |
115 apply (simp add: gcd_commute [of 0]) |
119 apply (simp add: gcd_commute [of 0]) |
116 done |
120 done |
122 |
126 |
123 (** Multiplication laws **) |
127 (** Multiplication laws **) |
124 |
128 |
125 (*Davenport, page 27*) |
129 (*Davenport, page 27*) |
126 lemma gcd_mult_distrib2: "k * gcd(m,n) = gcd(k*m, k*n)" |
130 lemma gcd_mult_distrib2: "k * gcd(m,n) = gcd(k*m, k*n)" |
127 apply (rule_tac m="m" and n="n" in gcd_induct) |
131 apply (induct_tac m n rule: gcd_induct) |
128 apply (simp) |
132 apply (simp) |
129 apply (case_tac "k=0") |
133 apply (case_tac "k=0") |
130 apply (simp_all add: mod_geq gcd_non_0 mod_mult_distrib2) |
134 apply (simp_all add: mod_geq gcd_non_0 mod_mult_distrib2) |
131 done |
135 done |
132 |
136 |
147 note gcd_mult_distrib2 [of k 1 n, simplify, THEN sym]; |
151 note gcd_mult_distrib2 [of k 1 n, simplify, THEN sym]; |
148 thus ?thesis; by assumption; qed; *) |
152 thus ?thesis; by assumption; qed; *) |
149 done |
153 done |
150 |
154 |
151 lemma relprime_dvd_mult: "[| gcd(k,n)=1; k dvd (m*n) |] ==> k dvd m"; |
155 lemma relprime_dvd_mult: "[| gcd(k,n)=1; k dvd (m*n) |] ==> k dvd m"; |
152 apply (subgoal_tac "k dvd gcd(m*k, m*n)") |
|
153 apply (subgoal_tac "gcd(m*k, m*n) = m") |
156 apply (subgoal_tac "gcd(m*k, m*n) = m") |
154 apply (simp) |
157 apply (erule_tac t="m" in subst); |
|
158 apply (simp) |
155 apply (simp add: gcd_mult_distrib2 [THEN sym]); |
159 apply (simp add: gcd_mult_distrib2 [THEN sym]); |
156 apply (rule gcd_greatest) |
160 done |
157 apply (simp_all) |
161 |
|
162 lemma relprime_dvd_mult_iff: "gcd(k,n)=1 \<Longrightarrow> k dvd (m*n) = k dvd m"; |
|
163 apply (blast intro: relprime_dvd_mult dvd_trans) |
158 done |
164 done |
159 |
165 |
160 lemma prime_imp_relprime: "[| p: prime; ~ p dvd n |] ==> gcd (p, n) = 1" |
166 lemma prime_imp_relprime: "[| p: prime; ~ p dvd n |] ==> gcd (p, n) = 1" |
161 apply (simp add: prime_def); |
167 apply (simp add: prime_def); |
162 apply (cut_tac m="p" and n="n" in gcd_dvd_both) |
168 apply (cut_tac m="p" and n="n" in gcd_dvd_both) |
194 apply (simp_all add: gcd_add2 add_assoc) |
200 apply (simp_all add: gcd_add2 add_assoc) |
195 done |
201 done |
196 |
202 |
197 |
203 |
198 (** More multiplication laws **) |
204 (** More multiplication laws **) |
199 |
|
200 lemma gcd_dvd_gcd_mult: "gcd(m,n) dvd gcd(k*m, n)" |
|
201 apply (blast intro: gcd_dvd2 gcd_dvd1 dvd_trans gcd_greatest); |
|
202 done |
|
203 |
205 |
204 lemma gcd_mult_cancel: "gcd(k,n) = 1 ==> gcd(k*m, n) = gcd(m,n)" |
206 lemma gcd_mult_cancel: "gcd(k,n) = 1 ==> gcd(k*m, n) = gcd(m,n)" |
205 apply (rule dvd_anti_sym) |
207 apply (rule dvd_anti_sym) |
206 apply (rule gcd_greatest) |
208 apply (rule gcd_greatest) |
207 apply (rule_tac n="k" in relprime_dvd_mult) |
209 apply (rule_tac n="k" in relprime_dvd_mult) |
208 apply (simp add: gcd_assoc) |
210 apply (simp add: gcd_assoc) |
209 apply (simp add: gcd_commute) |
211 apply (simp add: gcd_commute) |
210 apply (simp_all add: mult_commute gcd_dvd1 gcd_dvd2 gcd_dvd_gcd_mult) |
212 apply (simp_all add: mult_commute gcd_dvd1 gcd_dvd2) |
|
213 apply (blast intro: gcd_dvd1 dvd_trans); |
211 done |
214 done |
212 |
215 |
213 end |
216 end |