author | paulson |

Wed Jun 13 16:30:12 2001 +0200 (2001-06-13) | |

changeset 11375 | a6730c90e753 |

parent 11374 | 2badb9b2a8ec |

child 11376 | bf98ad1c22c6 |

tidied

src/HOL/ex/Lagrange.ML | file | annotate | diff | revisions | |

src/HOL/ex/Lagrange.thy | file | annotate | diff | revisions |

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