|
5078
|
1 |
(* Title: HOL/Integ/IntRing.ML
|
|
|
2 |
ID: $Id$
|
|
|
3 |
Author: Tobias Nipkow and Markus Wenzel
|
|
|
4 |
Copyright 1996 TU Muenchen
|
|
|
5 |
|
|
|
6 |
The instantiation of Lagrange's lemma for int.
|
|
|
7 |
*)
|
|
|
8 |
|
|
|
9 |
Goal "!!i1::int. \
|
|
|
10 |
\ (sq i1 + sq i2 + sq i3 + sq i4) * (sq j1 + sq j2 + sq j3 + sq j4) = \
|
|
|
11 |
\ sq(i1*j1 - i2*j2 - i3*j3 - i4*j4) + \
|
|
|
12 |
\ sq(i1*j2 + i2*j1 + i3*j4 - i4*j3) + \
|
|
|
13 |
\ sq(i1*j3 - i2*j4 + i3*j1 + i4*j2) + \
|
|
|
14 |
\ sq(i1*j4 + i2*j3 - i3*j2 + i4*j1)";
|
|
|
15 |
by (rtac Lagrange_lemma 1);
|
|
|
16 |
qed "Lagrange_lemma_int";
|