src/HOL/NumberTheory/IntPrimes.thy
author paulson
Thu Aug 03 10:46:01 2000 +0200 (2000-08-03)
changeset 9508 4d01dbf6ded7
child 9943 55c82decf3f4
permissions -rw-r--r--
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson@9508
     1
(*  Title:	IntPrimes.thy
paulson@9508
     2
    ID:         $Id$
paulson@9508
     3
    Author:	Thomas M. Rasmussen
paulson@9508
     4
    Copyright	2000  University of Cambridge
paulson@9508
     5
*)
paulson@9508
     6
paulson@9508
     7
IntPrimes = Main + IntDiv +
paulson@9508
     8
paulson@9508
     9
consts
paulson@9508
    10
  is_zgcd  :: [int,int,int] => bool         
paulson@9508
    11
  zgcd     :: "int*int => int"              
paulson@9508
    12
  xzgcda   :: "int*int*int*int*int*int*int*int => int*int*int"
paulson@9508
    13
  xzgcd    :: "[int,int] => int*int*int" 
paulson@9508
    14
  zprime   :: int set
paulson@9508
    15
  zcong    :: [int,int,int] => bool     ("(1[_ = _] '(mod _'))")
paulson@9508
    16
  
paulson@9508
    17
recdef zgcd "measure ((%(m,n).(nat n)) ::int*int=>nat)"
paulson@9508
    18
    simpset "simpset() addsimps [pos_mod_bound]"
paulson@9508
    19
    "zgcd (m, n) = (if n<=#0 then m else zgcd(n, m mod n))"
paulson@9508
    20
paulson@9508
    21
recdef xzgcda 
paulson@9508
    22
       "measure ((%(m,n,r',r,s',s,t',t).(nat r))
paulson@9508
    23
                 ::int*int*int*int*int*int*int*int=>nat)"
paulson@9508
    24
        simpset "simpset() addsimps [pos_mod_bound]"
paulson@9508
    25
       "xzgcda (m,n,r',r,s',s,t',t) = 
paulson@9508
    26
          (if r<=#0 then (r',s',t') else  
paulson@9508
    27
           xzgcda(m,n,r,r' mod r,s,s'-(r' div r)*s,t,t'-(r' div r)*t))"
paulson@9508
    28
paulson@9508
    29
defs
paulson@9508
    30
  xzgcd_def    "xzgcd m n == xzgcda (m,n,m,n,#1,#0,#0,#1)"
paulson@9508
    31
paulson@9508
    32
  is_zgcd_def  "is_zgcd p m n == #0 < p  &  p dvd m  &  p dvd n  &
paulson@9508
    33
                                 (ALL d. d dvd m & d dvd n --> d dvd p)"
paulson@9508
    34
paulson@9508
    35
  zprime_def   "zprime == {p. #1<p & (ALL m. m dvd p --> m=#1 | m=p)}"
paulson@9508
    36
paulson@9508
    37
  zcong_def    "[a=b] (mod m) == m dvd (a-b)"
paulson@9508
    38
paulson@9508
    39
end