author  paulson 
Mon, 31 Mar 2003 12:29:26 +0200  
changeset 13887  54a0c675c423 
parent 13871  26e5f5e624f6 
child 14271  8ed6989228bb 
permissions  rwrr 
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 BoyerMoore theorem prover. See his "A 

13 
mechanical proof of quadratic reciprocity," Journal of Automated Reasoning 

14 
8:321, 1992.*) 

9508
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

15 

11049
7eef34adb852
HOLNumberTheory: converted to newstyle 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
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9944
diff
changeset

19 
use_thy "Fib"; 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9944
diff
changeset

20 
use_thy "Factorization"; 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9944
diff
changeset

21 
use_thy "Chinese"; 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9944
diff
changeset

22 
use_thy "EulerFermat"; 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9944
diff
changeset

23 
use_thy "WilsonRuss"; 
7eef34adb852
HOLNumberTheory: converted to newstyle 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"; 