2281
|
1 |
(* Title: HOL/Integ/Lagrange.ML
|
|
2 |
ID: $Id$
|
|
3 |
Author: Tobias Nipkow
|
|
4 |
Copyright 1996 TU Muenchen
|
|
5 |
|
|
6 |
|
|
7 |
The following lemma essentially shows that all composite natural numbers are
|
|
8 |
sums of fours squares, provided all prime numbers are. However, this is an
|
|
9 |
abstract thm about commutative rings and has a priori nothing to do with nat.
|
|
10 |
*)
|
|
11 |
|
|
12 |
goalw Lagrange.thy [Lagrange.sq_def] "!!x1::'a::cring. \
|
|
13 |
\ (sq x1 + sq x2 + sq x3 + sq x4) * (sq y1 + sq y2 + sq y3 + sq y4) = \
|
|
14 |
\ sq(x1*y1 - x2*y2 - x3*y3 - x4*y4) + \
|
|
15 |
\ sq(x1*y2 + x2*y1 + x3*y4 - x4*y3) + \
|
|
16 |
\ sq(x1*y3 - x2*y4 + x3*y1 + x4*y2) + \
|
|
17 |
\ sq(x1*y4 + x2*y3 - x3*y2 + x4*y1)";
|
3239
|
18 |
(*Takes up to three minutes...*)
|
|
19 |
by (cring_simp 1);
|
2281
|
20 |
qed "Lagrange_lemma";
|