|
11375
|
1 |
(* Title: HOL/ex/Lagrange.thy
|
|
5078
|
2 |
ID: $Id$
|
|
|
3 |
Author: Tobias Nipkow
|
|
|
4 |
Copyright 1996 TU Muenchen
|
|
|
5 |
|
|
|
6 |
|
|
11375
|
7 |
This theory only contains a single theorem, which is a lemma in Lagrange's
|
|
|
8 |
proof that every natural number is the sum of 4 squares. Its sole purpose is
|
|
|
9 |
to demonstrate ordered rewriting for commutative rings.
|
|
5078
|
10 |
|
|
11375
|
11 |
The enterprising reader might consider proving all of Lagrange's theorem.
|
|
5078
|
12 |
*)
|
|
|
13 |
Lagrange = Ring +
|
|
|
14 |
|
|
|
15 |
constdefs sq :: 'a::times => 'a
|
|
|
16 |
"sq x == x*x"
|
|
|
17 |
|
|
|
18 |
end
|