src/HOL/ex/Lagrange.thy
author wenzelm
Tue, 01 Jun 2004 12:33:50 +0200
changeset 14854 61bdf2ae4dc5
parent 14738 83f1a514dcb4
child 15069 0a0371b55a0f
permissions -rw-r--r--
removed obsolete sort 'logic';
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
11375
paulson
parents: 5078
diff changeset
     1
(*  Title:      HOL/ex/Lagrange.thy
5078
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
11375
paulson
parents: 5078
diff changeset
     7
This theory only contains a single theorem, which is a lemma in Lagrange's
paulson
parents: 5078
diff changeset
     8
proof that every natural number is the sum of 4 squares.  Its sole purpose is
paulson
parents: 5078
diff changeset
     9
to demonstrate ordered rewriting for commutative rings.
5078
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    10
11375
paulson
parents: 5078
diff changeset
    11
The enterprising reader might consider proving all of Lagrange's theorem.
5078
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    12
*)
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    13
14603
985eb6708207 Moved ring stuff from ex into Ring_and_Field.
nipkow
parents: 11375
diff changeset
    14
theory Lagrange = Main:
985eb6708207 Moved ring stuff from ex into Ring_and_Field.
nipkow
parents: 11375
diff changeset
    15
985eb6708207 Moved ring stuff from ex into Ring_and_Field.
nipkow
parents: 11375
diff changeset
    16
constdefs sq :: "'a::times => 'a"
5078
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    17
         "sq x == x*x"
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    18
14603
985eb6708207 Moved ring stuff from ex into Ring_and_Field.
nipkow
parents: 11375
diff changeset
    19
(* The following lemma essentially shows that every natural number is the sum
985eb6708207 Moved ring stuff from ex into Ring_and_Field.
nipkow
parents: 11375
diff changeset
    20
of four squares, provided all prime numbers are.  However, this is an
985eb6708207 Moved ring stuff from ex into Ring_and_Field.
nipkow
parents: 11375
diff changeset
    21
abstract theorem about commutative rings.  It has, a priori, nothing to do
985eb6708207 Moved ring stuff from ex into Ring_and_Field.
nipkow
parents: 11375
diff changeset
    22
with nat.*)
985eb6708207 Moved ring stuff from ex into Ring_and_Field.
nipkow
parents: 11375
diff changeset
    23
985eb6708207 Moved ring stuff from ex into Ring_and_Field.
nipkow
parents: 11375
diff changeset
    24
(*once a slow step, but now (2001) just three seconds!*)
985eb6708207 Moved ring stuff from ex into Ring_and_Field.
nipkow
parents: 11375
diff changeset
    25
lemma Lagrange_lemma:
14738
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents: 14603
diff changeset
    26
 "!!x1::'a::comm_ring_1.
14603
985eb6708207 Moved ring stuff from ex into Ring_and_Field.
nipkow
parents: 11375
diff changeset
    27
  (sq x1 + sq x2 + sq x3 + sq x4) * (sq y1 + sq y2 + sq y3 + sq y4) =
985eb6708207 Moved ring stuff from ex into Ring_and_Field.
nipkow
parents: 11375
diff changeset
    28
  sq(x1*y1 - x2*y2 - x3*y3 - x4*y4)  +
985eb6708207 Moved ring stuff from ex into Ring_and_Field.
nipkow
parents: 11375
diff changeset
    29
  sq(x1*y2 + x2*y1 + x3*y4 - x4*y3)  +
985eb6708207 Moved ring stuff from ex into Ring_and_Field.
nipkow
parents: 11375
diff changeset
    30
  sq(x1*y3 - x2*y4 + x3*y1 + x4*y2)  +
985eb6708207 Moved ring stuff from ex into Ring_and_Field.
nipkow
parents: 11375
diff changeset
    31
  sq(x1*y4 + x2*y3 - x3*y2 + x4*y1)"
985eb6708207 Moved ring stuff from ex into Ring_and_Field.
nipkow
parents: 11375
diff changeset
    32
by(simp add: sq_def ring_eq_simps)
985eb6708207 Moved ring stuff from ex into Ring_and_Field.
nipkow
parents: 11375
diff changeset
    33
985eb6708207 Moved ring stuff from ex into Ring_and_Field.
nipkow
parents: 11375
diff changeset
    34
985eb6708207 Moved ring stuff from ex into Ring_and_Field.
nipkow
parents: 11375
diff changeset
    35
(* A challenge by John Harrison. Takes about 4 mins on a 3GHz machine.
985eb6708207 Moved ring stuff from ex into Ring_and_Field.
nipkow
parents: 11375
diff changeset
    36
14738
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents: 14603
diff changeset
    37
lemma "!!p1::'a::comm_ring_1.
14603
985eb6708207 Moved ring stuff from ex into Ring_and_Field.
nipkow
parents: 11375
diff changeset
    38
 (sq p1 + sq q1 + sq r1 + sq s1 + sq t1 + sq u1 + sq v1 + sq w1) * 
985eb6708207 Moved ring stuff from ex into Ring_and_Field.
nipkow
parents: 11375
diff changeset
    39
 (sq p2 + sq q2 + sq r2 + sq s2 + sq t2 + sq u2 + sq v2 + sq w2) 
985eb6708207 Moved ring stuff from ex into Ring_and_Field.
nipkow
parents: 11375
diff changeset
    40
  = sq (p1*p2 - q1*q2 - r1*r2 - s1*s2 - t1*t2 - u1*u2 - v1*v2 - w1*w2) + 
985eb6708207 Moved ring stuff from ex into Ring_and_Field.
nipkow
parents: 11375
diff changeset
    41
    sq (p1*q2 + q1*p2 + r1*s2 - s1*r2 + t1*u2 - u1*t2 - v1*w2 + w1*v2) +
985eb6708207 Moved ring stuff from ex into Ring_and_Field.
nipkow
parents: 11375
diff changeset
    42
    sq (p1*r2 - q1*s2 + r1*p2 + s1*q2 + t1*v2 + u1*w2 - v1*t2 - w1*u2) +
985eb6708207 Moved ring stuff from ex into Ring_and_Field.
nipkow
parents: 11375
diff changeset
    43
    sq (p1*s2 + q1*r2 - r1*q2 + s1*p2 + t1*w2 - u1*v2 + v1*u2 - w1*t2) +
985eb6708207 Moved ring stuff from ex into Ring_and_Field.
nipkow
parents: 11375
diff changeset
    44
    sq (p1*t2 - q1*u2 - r1*v2 - s1*w2 + t1*p2 + u1*q2 + v1*r2 + w1*s2) +
985eb6708207 Moved ring stuff from ex into Ring_and_Field.
nipkow
parents: 11375
diff changeset
    45
    sq (p1*u2 + q1*t2 - r1*w2 + s1*v2 - t1*q2 + u1*p2 - v1*s2 + w1*r2) +
985eb6708207 Moved ring stuff from ex into Ring_and_Field.
nipkow
parents: 11375
diff changeset
    46
    sq (p1*v2 + q1*w2 + r1*t2 - s1*u2 - t1*r2 + u1*s2 + v1*p2 - w1*q2) +
985eb6708207 Moved ring stuff from ex into Ring_and_Field.
nipkow
parents: 11375
diff changeset
    47
    sq (p1*w2 - q1*v2 + r1*u2 + s1*t2 - t1*s2 - u1*r2 + v1*q2 + w1*p2)"
985eb6708207 Moved ring stuff from ex into Ring_and_Field.
nipkow
parents: 11375
diff changeset
    48
by(simp add: sq_def ring_eq_simps)
985eb6708207 Moved ring stuff from ex into Ring_and_Field.
nipkow
parents: 11375
diff changeset
    49
*)
985eb6708207 Moved ring stuff from ex into Ring_and_Field.
nipkow
parents: 11375
diff changeset
    50
5078
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    51
end