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
```