src/HOL/ex/Lagrange.thy
 author obua Mon Apr 10 16:00:34 2006 +0200 (2006-04-10) changeset 19404 9bf2cdc9e8e8 parent 17388 495c799df31d child 19736 d8d0f8f51d69 permissions -rw-r--r--
Moved stuff from Ring_and_Field to Matrix
 paulson@11375 1 (* Title: HOL/ex/Lagrange.thy paulson@5078 2 ID: \$Id\$ paulson@5078 3 Author: Tobias Nipkow paulson@5078 4 Copyright 1996 TU Muenchen paulson@5078 5 *) paulson@5078 6 wenzelm@17388 7 header {* A lemma for Lagrange's theorem *} wenzelm@17388 8 haftmann@16417 9 theory Lagrange imports Main begin nipkow@14603 10 wenzelm@17388 11 text {* This theory only contains a single theorem, which is a lemma wenzelm@17388 12 in Lagrange's proof that every natural number is the sum of 4 squares. wenzelm@17388 13 Its sole purpose is to demonstrate ordered rewriting for commutative wenzelm@17388 14 rings. wenzelm@17388 15 wenzelm@17388 16 The enterprising reader might consider proving all of Lagrange's wenzelm@17388 17 theorem. *} wenzelm@17388 18 nipkow@14603 19 constdefs sq :: "'a::times => 'a" paulson@5078 20 "sq x == x*x" paulson@5078 21 wenzelm@17388 22 text {* The following lemma essentially shows that every natural wenzelm@17388 23 number is the sum of four squares, provided all prime numbers are. wenzelm@17388 24 However, this is an abstract theorem about commutative rings. It has, wenzelm@17388 25 a priori, nothing to do with nat. *} nipkow@14603 26 nipkow@16568 27 ML"Delsimprocs[ab_group_add_cancel.sum_conv, ab_group_add_cancel.rel_conv]" nipkow@16568 28 wenzelm@17388 29 -- {* once a slow step, but now (2001) just three seconds! *} nipkow@14603 30 lemma Lagrange_lemma: nipkow@15069 31 "!!x1::'a::comm_ring. nipkow@14603 32 (sq x1 + sq x2 + sq x3 + sq x4) * (sq y1 + sq y2 + sq y3 + sq y4) = nipkow@14603 33 sq(x1*y1 - x2*y2 - x3*y3 - x4*y4) + nipkow@14603 34 sq(x1*y2 + x2*y1 + x3*y4 - x4*y3) + nipkow@14603 35 sq(x1*y3 - x2*y4 + x3*y1 + x4*y2) + nipkow@14603 36 sq(x1*y4 + x2*y3 - x3*y2 + x4*y1)" nipkow@14603 37 by(simp add: sq_def ring_eq_simps) nipkow@14603 38 nipkow@14603 39 paulson@16740 40 text{*A challenge by John Harrison. Takes about 74s on a 2.5GHz Apple G5.*} nipkow@14603 41 nipkow@15069 42 lemma "!!p1::'a::comm_ring. nipkow@14603 43 (sq p1 + sq q1 + sq r1 + sq s1 + sq t1 + sq u1 + sq v1 + sq w1) * nipkow@14603 44 (sq p2 + sq q2 + sq r2 + sq s2 + sq t2 + sq u2 + sq v2 + sq w2) nipkow@14603 45 = sq (p1*p2 - q1*q2 - r1*r2 - s1*s2 - t1*t2 - u1*u2 - v1*v2 - w1*w2) + nipkow@14603 46 sq (p1*q2 + q1*p2 + r1*s2 - s1*r2 + t1*u2 - u1*t2 - v1*w2 + w1*v2) + nipkow@14603 47 sq (p1*r2 - q1*s2 + r1*p2 + s1*q2 + t1*v2 + u1*w2 - v1*t2 - w1*u2) + nipkow@14603 48 sq (p1*s2 + q1*r2 - r1*q2 + s1*p2 + t1*w2 - u1*v2 + v1*u2 - w1*t2) + nipkow@14603 49 sq (p1*t2 - q1*u2 - r1*v2 - s1*w2 + t1*p2 + u1*q2 + v1*r2 + w1*s2) + nipkow@14603 50 sq (p1*u2 + q1*t2 - r1*w2 + s1*v2 - t1*q2 + u1*p2 - v1*s2 + w1*r2) + nipkow@14603 51 sq (p1*v2 + q1*w2 + r1*t2 - s1*u2 - t1*r2 + u1*s2 + v1*p2 - w1*q2) + nipkow@14603 52 sq (p1*w2 - q1*v2 + r1*u2 + s1*t2 - t1*s2 - u1*r2 + v1*q2 + w1*p2)" wenzelm@17388 53 oops wenzelm@17388 54 (* nipkow@14603 55 by(simp add: sq_def ring_eq_simps) nipkow@14603 56 *) nipkow@14603 57 paulson@5078 58 end