src/HOL/ex/Lagrange.ML
author nipkow
Fri, 24 Nov 2000 16:49:27 +0100
changeset 10519 ade64af4c57c
parent 5078 7b5ea59c0275
child 11375 a6730c90e753
permissions -rw-r--r--
hide many names from Datatype_Universe.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
5078
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
     1
(*  Title:      HOL/Integ/Lagrange.ML
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
     2
    ID:         $Id$
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
     3
    Author:     Tobias Nipkow
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
     4
    Copyright   1996 TU Muenchen
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
     5
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
     6
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
     7
The following lemma essentially shows that all composite natural numbers are
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
     8
sums of fours squares, provided all prime numbers are. However, this is an
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
     9
abstract thm about commutative rings and has a priori nothing to do with nat.
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    10
*)
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    11
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    12
Goalw [Lagrange.sq_def] "!!x1::'a::cring. \
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    13
\  (sq x1 + sq x2 + sq x3 + sq x4) * (sq y1 + sq y2 + sq y3 + sq y4) = \
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    14
\  sq(x1*y1 - x2*y2 - x3*y3 - x4*y4)  + \
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    15
\  sq(x1*y2 + x2*y1 + x3*y4 - x4*y3)  + \
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    16
\  sq(x1*y3 - x2*y4 + x3*y1 + x4*y2)  + \
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    17
\  sq(x1*y4 + x2*y3 - x3*y2 + x4*y1)";
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    18
(*Takes up to three minutes...*)
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    19
by (cring_tac 1);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    20
qed "Lagrange_lemma";
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    21
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    22
(* A challenge by John Harrison.
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    23
   Takes forever because of the naive bottom-up strategy of the rewriter.
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    24
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    25
Goalw [Lagrange.sq_def] "!!p1::'a::cring.\
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    26
\ (sq p1 + sq q1 + sq r1 + sq s1 + sq t1 + sq u1 + sq v1 + sq w1) * \
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    27
\ (sq p2 + sq q2 + sq r2 + sq s2 + sq t2 + sq u2 + sq v2 + sq w2) \
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    28
\  = sq (p1*p2 - q1*q2 - r1*r2 - s1*s2 - t1*t2 - u1*u2 - v1*v2 - w1*w2) + \
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    29
\    sq (p1*q2 + q1*p2 + r1*s2 - s1*r2 + t1*u2 - u1*t2 - v1*w2 + w1*v2) +\
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    30
\    sq (p1*r2 - q1*s2 + r1*p2 + s1*q2 + t1*v2 + u1*w2 - v1*t2 - w1*u2) +\
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    31
\    sq (p1*s2 + q1*r2 - r1*q2 + s1*p2 + t1*w2 - u1*v2 + v1*u2 - w1*t2) +\
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    32
\    sq (p1*t2 - q1*u2 - r1*v2 - s1*w2 + t1*p2 + u1*q2 + v1*r2 + w1*s2) +\
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    33
\    sq (p1*u2 + q1*t2 - r1*w2 + s1*v2 - t1*q2 + u1*p2 - v1*s2 + w1*r2) +\
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    34
\    sq (p1*v2 + q1*w2 + r1*t2 - s1*u2 - t1*r2 + u1*s2 + v1*p2 - w1*q2) +\
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    35
\    sq (p1*w2 - q1*v2 + r1*u2 + s1*t2 - t1*s2 - u1*r2 + v1*q2 + w1*p2)";
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    36
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    37
*)