src/HOL/NumberTheory/IntPrimes.thy
changeset 9508 4d01dbf6ded7
child 9943 55c82decf3f4
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/NumberTheory/IntPrimes.thy	Thu Aug 03 10:46:01 2000 +0200
     1.3 @@ -0,0 +1,39 @@
     1.4 +(*  Title:	IntPrimes.thy
     1.5 +    ID:         $Id$
     1.6 +    Author:	Thomas M. Rasmussen
     1.7 +    Copyright	2000  University of Cambridge
     1.8 +*)
     1.9 +
    1.10 +IntPrimes = Main + IntDiv +
    1.11 +
    1.12 +consts
    1.13 +  is_zgcd  :: [int,int,int] => bool         
    1.14 +  zgcd     :: "int*int => int"              
    1.15 +  xzgcda   :: "int*int*int*int*int*int*int*int => int*int*int"
    1.16 +  xzgcd    :: "[int,int] => int*int*int" 
    1.17 +  zprime   :: int set
    1.18 +  zcong    :: [int,int,int] => bool     ("(1[_ = _] '(mod _'))")
    1.19 +  
    1.20 +recdef zgcd "measure ((%(m,n).(nat n)) ::int*int=>nat)"
    1.21 +    simpset "simpset() addsimps [pos_mod_bound]"
    1.22 +    "zgcd (m, n) = (if n<=#0 then m else zgcd(n, m mod n))"
    1.23 +
    1.24 +recdef xzgcda 
    1.25 +       "measure ((%(m,n,r',r,s',s,t',t).(nat r))
    1.26 +                 ::int*int*int*int*int*int*int*int=>nat)"
    1.27 +        simpset "simpset() addsimps [pos_mod_bound]"
    1.28 +       "xzgcda (m,n,r',r,s',s,t',t) = 
    1.29 +          (if r<=#0 then (r',s',t') else  
    1.30 +           xzgcda(m,n,r,r' mod r,s,s'-(r' div r)*s,t,t'-(r' div r)*t))"
    1.31 +
    1.32 +defs
    1.33 +  xzgcd_def    "xzgcd m n == xzgcda (m,n,m,n,#1,#0,#0,#1)"
    1.34 +
    1.35 +  is_zgcd_def  "is_zgcd p m n == #0 < p  &  p dvd m  &  p dvd n  &
    1.36 +                                 (ALL d. d dvd m & d dvd n --> d dvd p)"
    1.37 +
    1.38 +  zprime_def   "zprime == {p. #1<p & (ALL m. m dvd p --> m=#1 | m=p)}"
    1.39 +
    1.40 +  zcong_def    "[a=b] (mod m) == m dvd (a-b)"
    1.41 +
    1.42 +end