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.

(*  Title:	IntPrimes.thy
    ID:         $Id$
    Author:	Thomas M. Rasmussen
    Copyright	2000  University of Cambridge
*)

IntPrimes = Primes +

consts
  xzgcda   :: "int*int*int*int*int*int*int*int => int*int*int"
  xzgcd    :: "[int,int] => int*int*int" 
  zprime   :: int set
  zcong    :: [int,int,int] => bool     ("(1[_ = _] '(mod _'))")
  
recdef xzgcda 
       "measure ((%(m,n,r',r,s',s,t',t).(nat r))
                 ::int*int*int*int*int*int*int*int=>nat)"
        simpset "simpset() addsimps [pos_mod_bound]"
       "xzgcda (m,n,r',r,s',s,t',t) = 
          (if r<=#0 then (r',s',t') else  
           xzgcda(m,n,r,r' mod r,s,s'-(r' div r)*s,t,t'-(r' div r)*t))"

constdefs
  zgcd     :: "int*int => int"              
      "zgcd == %(x,y). int (gcd(nat (abs x), nat (abs y)))"

defs
  xzgcd_def    "xzgcd m n == xzgcda (m,n,m,n,#1,#0,#0,#1)"

  zprime_def   "zprime == {p. #1<p & (ALL m. m dvd p --> m=#1 | m=p)}"

  zcong_def    "[a=b] (mod m) == m dvd (a-b)"

end