author  wenzelm 
Fri, 20 Mar 2009 09:52:32 +0100  
changeset 30601  febd9234abdd 
parent 29667  53103fc8ffa3 
child 36350  bc7982c54e37 
permissions  rwrr 
11375  1 
(* Title: HOL/ex/Lagrange.thy 
5078  2 
Author: Tobias Nipkow 
3 
Copyright 1996 TU Muenchen 

4 
*) 

5 

17388  6 
header {* A lemma for Lagrange's theorem *} 
7 

16417  8 
theory Lagrange imports Main begin 
14603  9 

17388  10 
text {* This theory only contains a single theorem, which is a lemma 
11 
in Lagrange's proof that every natural number is the sum of 4 squares. 

12 
Its sole purpose is to demonstrate ordered rewriting for commutative 

13 
rings. 

14 

15 
The enterprising reader might consider proving all of Lagrange's 

16 
theorem. *} 

17 

23477
f4b83f03cac9
tuned and renamed group_eq_simps and ring_eq_simps
nipkow
parents:
22173
diff
changeset

18 
definition sq :: "'a::times => 'a" where "sq x == x*x" 
5078  19 

17388  20 
text {* The following lemma essentially shows that every natural 
21 
number is the sum of four squares, provided all prime numbers are. 

22 
However, this is an abstract theorem about commutative rings. It has, 

23 
a priori, nothing to do with nat. *} 

14603  24 

23477
f4b83f03cac9
tuned and renamed group_eq_simps and ring_eq_simps
nipkow
parents:
22173
diff
changeset

25 
(* These two simprocs are even less efficient than ordered rewriting 
f4b83f03cac9
tuned and renamed group_eq_simps and ring_eq_simps
nipkow
parents:
22173
diff
changeset

26 
and kill the second example: *) 
26480  27 
ML {* 
20807  28 
Delsimprocs [ab_group_add_cancel.sum_conv, ab_group_add_cancel.rel_conv] 
29 
*} 

16568  30 

23477
f4b83f03cac9
tuned and renamed group_eq_simps and ring_eq_simps
nipkow
parents:
22173
diff
changeset

31 
lemma Lagrange_lemma: fixes x1 :: "'a::comm_ring" shows 
20807  32 
"(sq x1 + sq x2 + sq x3 + sq x4) * (sq y1 + sq y2 + sq y3 + sq y4) = 
23477
f4b83f03cac9
tuned and renamed group_eq_simps and ring_eq_simps
nipkow
parents:
22173
diff
changeset

33 
sq (x1*y1  x2*y2  x3*y3  x4*y4) + 
f4b83f03cac9
tuned and renamed group_eq_simps and ring_eq_simps
nipkow
parents:
22173
diff
changeset

34 
sq (x1*y2 + x2*y1 + x3*y4  x4*y3) + 
f4b83f03cac9
tuned and renamed group_eq_simps and ring_eq_simps
nipkow
parents:
22173
diff
changeset

35 
sq (x1*y3  x2*y4 + x3*y1 + x4*y2) + 
f4b83f03cac9
tuned and renamed group_eq_simps and ring_eq_simps
nipkow
parents:
22173
diff
changeset

36 
sq (x1*y4 + x2*y3  x3*y2 + x4*y1)" 
30601
febd9234abdd
considerable speedup of benchmarks by using minimal simpset;
wenzelm
parents:
29667
diff
changeset

37 
by (simp only: sq_def ring_simps) 
14603  38 

39 

25475
d5a382ccb5cc
challenge by John Harrison: down to 12s (was 17s, was 75s);
wenzelm
parents:
23477
diff
changeset

40 
text {* A challenge by John Harrison. Takes about 12s on a 1.6GHz machine. *} 
14603  41 

23477
f4b83f03cac9
tuned and renamed group_eq_simps and ring_eq_simps
nipkow
parents:
22173
diff
changeset

42 
lemma fixes p1 :: "'a::comm_ring" shows 
20807  43 
"(sq p1 + sq q1 + sq r1 + sq s1 + sq t1 + sq u1 + sq v1 + sq w1) * 
44 
(sq p2 + sq q2 + sq r2 + sq s2 + sq t2 + sq u2 + sq v2 + sq w2) 

45 
= sq (p1*p2  q1*q2  r1*r2  s1*s2  t1*t2  u1*u2  v1*v2  w1*w2) + 

46 
sq (p1*q2 + q1*p2 + r1*s2  s1*r2 + t1*u2  u1*t2  v1*w2 + w1*v2) + 

47 
sq (p1*r2  q1*s2 + r1*p2 + s1*q2 + t1*v2 + u1*w2  v1*t2  w1*u2) + 

48 
sq (p1*s2 + q1*r2  r1*q2 + s1*p2 + t1*w2  u1*v2 + v1*u2  w1*t2) + 

49 
sq (p1*t2  q1*u2  r1*v2  s1*w2 + t1*p2 + u1*q2 + v1*r2 + w1*s2) + 

50 
sq (p1*u2 + q1*t2  r1*w2 + s1*v2  t1*q2 + u1*p2  v1*s2 + w1*r2) + 

51 
sq (p1*v2 + q1*w2 + r1*t2  s1*u2  t1*r2 + u1*s2 + v1*p2  w1*q2) + 

52 
sq (p1*w2  q1*v2 + r1*u2 + s1*t2  t1*s2  u1*r2 + v1*q2 + w1*p2)" 

30601
febd9234abdd
considerable speedup of benchmarks by using minimal simpset;
wenzelm
parents:
29667
diff
changeset

53 
by (simp only: sq_def ring_simps) 
14603  54 

5078  55 
end 