summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/HOL/GCD.thy

changeset 34915 | 7894c7dab132 |

parent 34223 | dce32a1e05fe |

child 34973 | ae634fad947e |

1.1 --- a/src/HOL/GCD.thy Sun Jan 10 18:41:07 2010 +0100 1.2 +++ b/src/HOL/GCD.thy Sun Jan 10 18:43:45 2010 +0100 1.3 @@ -16,7 +16,7 @@ 1.4 another extension of the notions to the integers, and added a number 1.5 of results to "Primes" and "GCD". IntPrimes also defined and developed 1.6 the congruence relations on the integers. The notion was extended to 1.7 -the natural numbers by Chiaeb. 1.8 +the natural numbers by Chaieb. 1.9 1.10 Jeremy Avigad combined all of these, made everything uniform for the 1.11 natural numbers and the integers, and added a number of new theorems. 1.12 @@ -25,7 +25,7 @@ 1.13 *) 1.14 1.15 1.16 -header {* Greates common divisor and least common multiple *} 1.17 +header {* Greatest common divisor and least common multiple *} 1.18 1.19 theory GCD 1.20 imports Fact Parity 1.21 @@ -1074,34 +1074,35 @@ 1.22 assumes c: " \<forall>a b. P (a::nat) b \<longleftrightarrow> P b a" and z: "\<forall>a. P a 0" 1.23 and add: "\<forall>a b. P a b \<longrightarrow> P a (a + b)" 1.24 shows "P a b" 1.25 -proof(induct n\<equiv>"a+b" arbitrary: a b rule: nat_less_induct) 1.26 - fix n a b 1.27 - assume H: "\<forall>m < n. \<forall>a b. m = a + b \<longrightarrow> P a b" "n = a + b" 1.28 +proof(induct "a + b" arbitrary: a b rule: less_induct) 1.29 + case less 1.30 have "a = b \<or> a < b \<or> b < a" by arith 1.31 moreover {assume eq: "a= b" 1.32 from add[rule_format, OF z[rule_format, of a]] have "P a b" using eq 1.33 by simp} 1.34 moreover 1.35 {assume lt: "a < b" 1.36 - hence "a + b - a < n \<or> a = 0" using H(2) by arith 1.37 + hence "a + b - a < a + b \<or> a = 0" by arith 1.38 moreover 1.39 {assume "a =0" with z c have "P a b" by blast } 1.40 moreover 1.41 - {assume ab: "a + b - a < n" 1.42 - have th0: "a + b - a = a + (b - a)" using lt by arith 1.43 - from add[rule_format, OF H(1)[rule_format, OF ab th0]] 1.44 - have "P a b" by (simp add: th0[symmetric])} 1.45 + {assume "a + b - a < a + b" 1.46 + also have th0: "a + b - a = a + (b - a)" using lt by arith 1.47 + finally have "a + (b - a) < a + b" . 1.48 + then have "P a (a + (b - a))" by (rule add[rule_format, OF less]) 1.49 + then have "P a b" by (simp add: th0[symmetric])} 1.50 ultimately have "P a b" by blast} 1.51 moreover 1.52 {assume lt: "a > b" 1.53 - hence "b + a - b < n \<or> b = 0" using H(2) by arith 1.54 + hence "b + a - b < a + b \<or> b = 0" by arith 1.55 moreover 1.56 {assume "b =0" with z c have "P a b" by blast } 1.57 moreover 1.58 - {assume ab: "b + a - b < n" 1.59 - have th0: "b + a - b = b + (a - b)" using lt by arith 1.60 - from add[rule_format, OF H(1)[rule_format, OF ab th0]] 1.61 - have "P b a" by (simp add: th0[symmetric]) 1.62 + {assume "b + a - b < a + b" 1.63 + also have th0: "b + a - b = b + (a - b)" using lt by arith 1.64 + finally have "b + (a - b) < a + b" . 1.65 + then have "P b (b + (a - b))" by (rule add[rule_format, OF less]) 1.66 + then have "P b a" by (simp add: th0[symmetric]) 1.67 hence "P a b" using c by blast } 1.68 ultimately have "P a b" by blast} 1.69 ultimately show "P a b" by blast