src/HOL/ex/Lagrange.thy
 author nipkow Fri Mar 06 17:38:47 2009 +0100 (2009-03-06) changeset 30313 b2441b0c8d38 parent 29667 53103fc8ffa3 child 30601 febd9234abdd permissions -rw-r--r--
 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@23477 ` 19` ```definition sq :: "'a::times => 'a" where "sq x == x*x" ``` paulson@5078 ` 20` wenzelm@17388 ` 21` ```text {* The following lemma essentially shows that every natural ``` wenzelm@17388 ` 22` ```number is the sum of four squares, provided all prime numbers are. ``` wenzelm@17388 ` 23` ```However, this is an abstract theorem about commutative rings. It has, ``` wenzelm@17388 ` 24` ```a priori, nothing to do with nat. *} ``` nipkow@14603 ` 25` nipkow@23477 ` 26` ```(* These two simprocs are even less efficient than ordered rewriting ``` nipkow@23477 ` 27` ``` and kill the second example: *) ``` wenzelm@26480 ` 28` ```ML {* ``` wenzelm@20807 ` 29` ``` Delsimprocs [ab_group_add_cancel.sum_conv, ab_group_add_cancel.rel_conv] ``` wenzelm@20807 ` 30` ```*} ``` nipkow@16568 ` 31` nipkow@23477 ` 32` ```lemma Lagrange_lemma: fixes x1 :: "'a::comm_ring" shows ``` wenzelm@20807 ` 33` ``` "(sq x1 + sq x2 + sq x3 + sq x4) * (sq y1 + sq y2 + sq y3 + sq y4) = ``` nipkow@23477 ` 34` ``` sq (x1*y1 - x2*y2 - x3*y3 - x4*y4) + ``` nipkow@23477 ` 35` ``` sq (x1*y2 + x2*y1 + x3*y4 - x4*y3) + ``` nipkow@23477 ` 36` ``` sq (x1*y3 - x2*y4 + x3*y1 + x4*y2) + ``` nipkow@23477 ` 37` ``` sq (x1*y4 + x2*y3 - x3*y2 + x4*y1)" ``` nipkow@29667 ` 38` ```by (simp add: sq_def algebra_simps) ``` nipkow@14603 ` 39` nipkow@14603 ` 40` wenzelm@25475 ` 41` ```text {* A challenge by John Harrison. Takes about 12s on a 1.6GHz machine. *} ``` nipkow@14603 ` 42` nipkow@23477 ` 43` ```lemma fixes p1 :: "'a::comm_ring" shows ``` wenzelm@20807 ` 44` ``` "(sq p1 + sq q1 + sq r1 + sq s1 + sq t1 + sq u1 + sq v1 + sq w1) * ``` wenzelm@20807 ` 45` ``` (sq p2 + sq q2 + sq r2 + sq s2 + sq t2 + sq u2 + sq v2 + sq w2) ``` wenzelm@20807 ` 46` ``` = sq (p1*p2 - q1*q2 - r1*r2 - s1*s2 - t1*t2 - u1*u2 - v1*v2 - w1*w2) + ``` wenzelm@20807 ` 47` ``` sq (p1*q2 + q1*p2 + r1*s2 - s1*r2 + t1*u2 - u1*t2 - v1*w2 + w1*v2) + ``` wenzelm@20807 ` 48` ``` sq (p1*r2 - q1*s2 + r1*p2 + s1*q2 + t1*v2 + u1*w2 - v1*t2 - w1*u2) + ``` wenzelm@20807 ` 49` ``` sq (p1*s2 + q1*r2 - r1*q2 + s1*p2 + t1*w2 - u1*v2 + v1*u2 - w1*t2) + ``` wenzelm@20807 ` 50` ``` sq (p1*t2 - q1*u2 - r1*v2 - s1*w2 + t1*p2 + u1*q2 + v1*r2 + w1*s2) + ``` wenzelm@20807 ` 51` ``` sq (p1*u2 + q1*t2 - r1*w2 + s1*v2 - t1*q2 + u1*p2 - v1*s2 + w1*r2) + ``` wenzelm@20807 ` 52` ``` sq (p1*v2 + q1*w2 + r1*t2 - s1*u2 - t1*r2 + u1*s2 + v1*p2 - w1*q2) + ``` wenzelm@20807 ` 53` ``` sq (p1*w2 - q1*v2 + r1*u2 + s1*t2 - t1*s2 - u1*r2 + v1*q2 + w1*p2)" ``` nipkow@29667 ` 54` ```by (simp add: sq_def algebra_simps) ``` nipkow@14603 ` 55` paulson@5078 ` 56` ```end ```