src/HOL/ex/Lagrange.thy
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.thy
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
This theory only contains a single thm, which is a lemma in Lagrange's proof
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
     8
that every natural number is the sum of 4 squares.  It's sole purpose is to
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
     9
demonstrate ordered rewriting for commutative rings.
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    10
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    11
The enterprising reader might consider proving all of Lagrange's thm.
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