src/HOL/NumberTheory/README
author nipkow
Fri, 24 Nov 2000 16:49:27 +0100
changeset 10519 ade64af4c57c
parent 9545 c1d9500e2927
permissions -rw-r--r--
hide many names from Datatype_Universe.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
9508
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
     1
IntPrimes	dvd relation, GCD, Euclid's extended algorithm, primes,
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
     2
                congruences (all on the Integers)
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
     3
                Comparable to 'Primes' theory but dvd is included here
9545
paulson
parents: 9508
diff changeset
     4
                as it is not present in 'IntDiv'.  Also includes extended
9508
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
     5
                GCD and congruences not present in 'Primes'. 
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
     6
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
     7
Chinese		The Chinese Remainder Theorem for an arbitrary finite
9545
paulson
parents: 9508
diff changeset
     8
                number of equations.  (The one-equation case is included
paulson
parents: 9508
diff changeset
     9
                in 'IntPrimes')  Uses functions for indexing. 
9508
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
    10
9545
paulson
parents: 9508
diff changeset
    11
IntFact         Factorial on integers and recursively defined set
paulson
parents: 9508
diff changeset
    12
                including all Integers from 2 up to a.  Plus definition 
paulson
parents: 9508
diff changeset
    13
		of product of finite set. 
9508
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
    14
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
    15
BijectionRel    Inductive definitions of bijections between two different
9545
paulson
parents: 9508
diff changeset
    16
                sets and between the same set.  Theorem for relating
9508
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
    17
                the two definitions
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
    18
9545
paulson
parents: 9508
diff changeset
    19
EulerFermat     Fermat's Little Theorem extended to Euler's Totient function. 
9508
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
    20
                More abstract approach than Boyer-Moore (which seems necessary
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
    21
                to achieve the extended version)
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
    22
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
    23
WilsonRuss      Wilson's Theorem following quite closely Russinoff's approach
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
    24
		using Boyer-Moore (using finite sets instead of lists, though)
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
    25
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
    26
WilsonBij	Wilson's Theorem using a more "abstract" approach based on
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
    27
		bijections between sets.  Does not use Fermat's Little Theorem
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
    28
                (unlike Russinoff)
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
    29
 
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
    30