src/HOL/NumberTheory/IntPrimes.thy
author wenzelm
Tue Oct 03 22:37:16 2000 +0200 (2000-10-03)
changeset 10147 178deaacb244
parent 9943 55c82decf3f4
child 11049 7eef34adb852
permissions -rw-r--r--
tuned deps;
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
wenzelm@10147
     7
IntPrimes = Primes +
paulson@9508
     8
paulson@9508
     9
consts
paulson@9508
    10
  xzgcda   :: "int*int*int*int*int*int*int*int => int*int*int"
paulson@9508
    11
  xzgcd    :: "[int,int] => int*int*int" 
paulson@9508
    12
  zprime   :: int set
paulson@9508
    13
  zcong    :: [int,int,int] => bool     ("(1[_ = _] '(mod _'))")
paulson@9508
    14
  
paulson@9508
    15
recdef xzgcda 
paulson@9508
    16
       "measure ((%(m,n,r',r,s',s,t',t).(nat r))
paulson@9508
    17
                 ::int*int*int*int*int*int*int*int=>nat)"
paulson@9508
    18
        simpset "simpset() addsimps [pos_mod_bound]"
paulson@9508
    19
       "xzgcda (m,n,r',r,s',s,t',t) = 
paulson@9508
    20
          (if r<=#0 then (r',s',t') else  
paulson@9508
    21
           xzgcda(m,n,r,r' mod r,s,s'-(r' div r)*s,t,t'-(r' div r)*t))"
paulson@9508
    22
paulson@9943
    23
constdefs
paulson@9943
    24
  zgcd     :: "int*int => int"              
paulson@9943
    25
      "zgcd == %(x,y). int (gcd(nat (abs x), nat (abs y)))"
paulson@9943
    26
paulson@9508
    27
defs
paulson@9508
    28
  xzgcd_def    "xzgcd m n == xzgcda (m,n,m,n,#1,#0,#0,#1)"
paulson@9508
    29
paulson@9508
    30
  zprime_def   "zprime == {p. #1<p & (ALL m. m dvd p --> m=#1 | m=p)}"
paulson@9508
    31
paulson@9508
    32
  zcong_def    "[a=b] (mod m) == m dvd (a-b)"
paulson@9508
    33
paulson@9508
    34
end