src/HOL/ex/Lagrange.thy
author paulson
Wed, 13 Jun 2001 16:30:12 +0200
changeset 11375 a6730c90e753
parent 5078 7b5ea59c0275
child 14603 985eb6708207
permissions -rw-r--r--
tidied
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
Lagrange = Ring +
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    14
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    15
constdefs sq :: 'a::times => 'a
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    16
         "sq x == x*x"
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    17
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    18
end