tidied
authorpaulson
Wed Jun 13 16:30:12 2001 +0200 (2001-06-13)
changeset 11375a6730c90e753
parent 11374 2badb9b2a8ec
child 11376 bf98ad1c22c6
tidied
src/HOL/ex/Lagrange.ML
src/HOL/ex/Lagrange.thy
     1.1 --- a/src/HOL/ex/Lagrange.ML	Wed Jun 13 16:29:51 2001 +0200
     1.2 +++ b/src/HOL/ex/Lagrange.ML	Wed Jun 13 16:30:12 2001 +0200
     1.3 @@ -4,21 +4,21 @@
     1.4      Copyright   1996 TU Muenchen
     1.5  
     1.6  
     1.7 -The following lemma essentially shows that all composite natural numbers are
     1.8 -sums of fours squares, provided all prime numbers are. However, this is an
     1.9 -abstract thm about commutative rings and has a priori nothing to do with nat.
    1.10 -*)
    1.11 +The following lemma essentially shows that every natural number is the sum of
    1.12 +four squares, provided all prime numbers are.  However, this is an abstract
    1.13 +theorem about commutative rings.  It has, a priori, nothing to do with nat.*)
    1.14  
    1.15 -Goalw [Lagrange.sq_def] "!!x1::'a::cring. \
    1.16 +Goalw [Lagrange.sq_def]
    1.17 + "!!x1::'a::cring. \
    1.18  \  (sq x1 + sq x2 + sq x3 + sq x4) * (sq y1 + sq y2 + sq y3 + sq y4) = \
    1.19  \  sq(x1*y1 - x2*y2 - x3*y3 - x4*y4)  + \
    1.20  \  sq(x1*y2 + x2*y1 + x3*y4 - x4*y3)  + \
    1.21  \  sq(x1*y3 - x2*y4 + x3*y1 + x4*y2)  + \
    1.22  \  sq(x1*y4 + x2*y3 - x3*y2 + x4*y1)";
    1.23 -(*Takes up to three minutes...*)
    1.24 -by (cring_tac 1);
    1.25 +by (cring_tac 1);  (*once a slow step, but now (2001) just three seconds!*)
    1.26  qed "Lagrange_lemma";
    1.27  
    1.28 +
    1.29  (* A challenge by John Harrison.
    1.30     Takes forever because of the naive bottom-up strategy of the rewriter.
    1.31  
    1.32 @@ -33,5 +33,5 @@
    1.33  \    sq (p1*u2 + q1*t2 - r1*w2 + s1*v2 - t1*q2 + u1*p2 - v1*s2 + w1*r2) +\
    1.34  \    sq (p1*v2 + q1*w2 + r1*t2 - s1*u2 - t1*r2 + u1*s2 + v1*p2 - w1*q2) +\
    1.35  \    sq (p1*w2 - q1*v2 + r1*u2 + s1*t2 - t1*s2 - u1*r2 + v1*q2 + w1*p2)";
    1.36 -
    1.37 +by (cring_tac 1);
    1.38  *)
     2.1 --- a/src/HOL/ex/Lagrange.thy	Wed Jun 13 16:29:51 2001 +0200
     2.2 +++ b/src/HOL/ex/Lagrange.thy	Wed Jun 13 16:30:12 2001 +0200
     2.3 @@ -1,14 +1,14 @@
     2.4 -(*  Title:      HOL/Integ/Lagrange.thy
     2.5 +(*  Title:      HOL/ex/Lagrange.thy
     2.6      ID:         $Id$
     2.7      Author:     Tobias Nipkow
     2.8      Copyright   1996 TU Muenchen
     2.9  
    2.10  
    2.11 -This theory only contains a single thm, which is a lemma in Lagrange's proof
    2.12 -that every natural number is the sum of 4 squares.  It's sole purpose is to
    2.13 -demonstrate ordered rewriting for commutative rings.
    2.14 +This theory only contains a single theorem, which is a lemma in Lagrange's
    2.15 +proof that every natural number is the sum of 4 squares.  Its sole purpose is
    2.16 +to demonstrate ordered rewriting for commutative rings.
    2.17  
    2.18 -The enterprising reader might consider proving all of Lagrange's thm.
    2.19 +The enterprising reader might consider proving all of Lagrange's theorem.
    2.20  *)
    2.21  Lagrange = Ring +
    2.22