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