231 proof- |
231 proof- |
232 from H have "\<forall>d. d dvd x \<and> d dvd y \<longleftrightarrow> d dvd gcd u v" by simp |
232 from H have "\<forall>d. d dvd x \<and> d dvd y \<longleftrightarrow> d dvd gcd u v" by simp |
233 with gcd_unique[of "gcd u v" x y] show ?thesis by auto |
233 with gcd_unique[of "gcd u v" x y] show ?thesis by auto |
234 qed |
234 qed |
235 |
235 |
236 lemma ind_euclid: |
236 lemma ind_euclid: |
237 assumes c: " \<forall>a b. P (a::nat) b \<longleftrightarrow> P b a" and z: "\<forall>a. P a 0" |
237 assumes c: " \<forall>a b. P (a::nat) b \<longleftrightarrow> P b a" and z: "\<forall>a. P a 0" |
238 and add: "\<forall>a b. P a b \<longrightarrow> P a (a + b)" |
238 and add: "\<forall>a b. P a b \<longrightarrow> P a (a + b)" |
239 shows "P a b" |
239 shows "P a b" |
240 proof(induct n\<equiv>"a+b" arbitrary: a b rule: nat_less_induct) |
240 proof(induct "a + b" arbitrary: a b rule: less_induct) |
241 fix n a b |
241 case less |
242 assume H: "\<forall>m < n. \<forall>a b. m = a + b \<longrightarrow> P a b" "n = a + b" |
|
243 have "a = b \<or> a < b \<or> b < a" by arith |
242 have "a = b \<or> a < b \<or> b < a" by arith |
244 moreover {assume eq: "a= b" |
243 moreover {assume eq: "a= b" |
245 from add[rule_format, OF z[rule_format, of a]] have "P a b" using eq by simp} |
244 from add[rule_format, OF z[rule_format, of a]] have "P a b" using eq |
|
245 by simp} |
246 moreover |
246 moreover |
247 {assume lt: "a < b" |
247 {assume lt: "a < b" |
248 hence "a + b - a < n \<or> a = 0" using H(2) by arith |
248 hence "a + b - a < a + b \<or> a = 0" by arith |
249 moreover |
249 moreover |
250 {assume "a =0" with z c have "P a b" by blast } |
250 {assume "a =0" with z c have "P a b" by blast } |
251 moreover |
251 moreover |
252 {assume ab: "a + b - a < n" |
252 {assume "a + b - a < a + b" |
253 have th0: "a + b - a = a + (b - a)" using lt by arith |
253 also have th0: "a + b - a = a + (b - a)" using lt by arith |
254 from add[rule_format, OF H(1)[rule_format, OF ab th0]] |
254 finally have "a + (b - a) < a + b" . |
255 have "P a b" by (simp add: th0[symmetric])} |
255 then have "P a (a + (b - a))" by (rule add[rule_format, OF less]) |
|
256 then have "P a b" by (simp add: th0[symmetric])} |
256 ultimately have "P a b" by blast} |
257 ultimately have "P a b" by blast} |
257 moreover |
258 moreover |
258 {assume lt: "a > b" |
259 {assume lt: "a > b" |
259 hence "b + a - b < n \<or> b = 0" using H(2) by arith |
260 hence "b + a - b < a + b \<or> b = 0" by arith |
260 moreover |
261 moreover |
261 {assume "b =0" with z c have "P a b" by blast } |
262 {assume "b =0" with z c have "P a b" by blast } |
262 moreover |
263 moreover |
263 {assume ab: "b + a - b < n" |
264 {assume "b + a - b < a + b" |
264 have th0: "b + a - b = b + (a - b)" using lt by arith |
265 also have th0: "b + a - b = b + (a - b)" using lt by arith |
265 from add[rule_format, OF H(1)[rule_format, OF ab th0]] |
266 finally have "b + (a - b) < a + b" . |
266 have "P b a" by (simp add: th0[symmetric]) |
267 then have "P b (b + (a - b))" by (rule add[rule_format, OF less]) |
|
268 then have "P b a" by (simp add: th0[symmetric]) |
267 hence "P a b" using c by blast } |
269 hence "P a b" using c by blast } |
268 ultimately have "P a b" by blast} |
270 ultimately have "P a b" by blast} |
269 ultimately show "P a b" by blast |
271 ultimately show "P a b" by blast |
270 qed |
272 qed |
271 |
273 |