| author | paulson |
| Mon, 31 Mar 2003 12:29:26 +0200 | |
| changeset 13887 | 54a0c675c423 |
| parent 13871 | 26e5f5e624f6 |
| child 14271 | 8ed6989228bb |
| permissions | -rw-r--r-- |
|
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
11368
diff
changeset
|
1 |
(* Title: HOL/NumberTheory/ROOT.ML |
|
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
11368
diff
changeset
|
2 |
ID: $Id$ |
|
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
11368
diff
changeset
|
3 |
Author: Lawrence C Paulson |
|
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
11368
diff
changeset
|
4 |
Copyright 2003 University of Cambridge |
|
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
11368
diff
changeset
|
5 |
|
|
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
11368
diff
changeset
|
6 |
This directory contains formalized proofs of Wilson's Theorem (by Thomas M |
| 13887 | 7 |
Rasmussen) and of Gauss's law of quadratic reciprocity (by Avigad, Gray and |
8 |
Kramer). |
|
9 |
||
10 |
The quadratic reciprocity formalization follows Eisenstein's proof, which is |
|
11 |
the one most commonly found in introductory textbooks, and also uses a trick |
|
12 |
used David Russinoff with the Boyer-Moore theorem prover. See his "A |
|
13 |
mechanical proof of quadratic reciprocity," Journal of Automated Reasoning |
|
14 |
8:3-21, 1992.*) |
|
|
9508
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
15 |
|
|
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
16 |
no_document use_thy "Permutation"; |
| 11368 | 17 |
no_document use_thy "Primes"; |
|
9508
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
18 |
|
|
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
19 |
use_thy "Fib"; |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
20 |
use_thy "Factorization"; |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
21 |
use_thy "Chinese"; |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
22 |
use_thy "EulerFermat"; |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
23 |
use_thy "WilsonRuss"; |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
24 |
use_thy "WilsonBij"; |
|
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
11368
diff
changeset
|
25 |
use_thy "Quadratic_Reciprocity"; |