src/HOL/NumberTheory/IntPrimes.thy
author nipkow
Fri, 24 Nov 2000 16:49:27 +0100
changeset 10519 ade64af4c57c
parent 10147 178deaacb244
child 11049 7eef34adb852
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
(*  Title:	IntPrimes.thy
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
     2
    ID:         $Id$
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
     3
    Author:	Thomas M. Rasmussen
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
     4
    Copyright	2000  University of Cambridge
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
     5
*)
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
     6
10147
178deaacb244 tuned deps;
wenzelm
parents: 9943
diff changeset
     7
IntPrimes = Primes +
9508
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
     8
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
     9
consts
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
    10
  xzgcda   :: "int*int*int*int*int*int*int*int => int*int*int"
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
    11
  xzgcd    :: "[int,int] => int*int*int" 
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
    12
  zprime   :: int set
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
    13
  zcong    :: [int,int,int] => bool     ("(1[_ = _] '(mod _'))")
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
recdef xzgcda 
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
    16
       "measure ((%(m,n,r',r,s',s,t',t).(nat r))
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
    17
                 ::int*int*int*int*int*int*int*int=>nat)"
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
    18
        simpset "simpset() addsimps [pos_mod_bound]"
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
    19
       "xzgcda (m,n,r',r,s',s,t',t) = 
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
    20
          (if r<=#0 then (r',s',t') else  
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
    21
           xzgcda(m,n,r,r' mod r,s,s'-(r' div r)*s,t,t'-(r' div r)*t))"
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
    22
9943
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9508
diff changeset
    23
constdefs
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9508
diff changeset
    24
  zgcd     :: "int*int => int"              
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9508
diff changeset
    25
      "zgcd == %(x,y). int (gcd(nat (abs x), nat (abs y)))"
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9508
diff changeset
    26
9508
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
    27
defs
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
    28
  xzgcd_def    "xzgcd m n == xzgcda (m,n,m,n,#1,#0,#0,#1)"
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
  zprime_def   "zprime == {p. #1<p & (ALL m. m dvd p --> m=#1 | m=p)}"
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
    31
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
    32
  zcong_def    "[a=b] (mod m) == m dvd (a-b)"
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
    33
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
    34
end