src/HOL/NumberTheory/IntPrimes.thy

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/NumberTheory/IntPrimes.thy	Thu Aug 03 10:46:01 2000 +0200
@@ -0,0 +1,39 @@
+(*  Title:	IntPrimes.thy
+    ID:         $Id$
+    Author:	Thomas M. Rasmussen
+    Copyright	2000  University of Cambridge
+*)
+
+IntPrimes = Main + IntDiv +
+
+consts
+  is_zgcd  :: [int,int,int] => bool         
+  zgcd     :: "int*int => int"              
+  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 zgcd "measure ((%(m,n).(nat n)) ::int*int=>nat)"
+    simpset "simpset() addsimps [pos_mod_bound]"
+    "zgcd (m, n) = (if n<=#0 then m else zgcd(n, m mod n))"
+
+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))"
+
+defs
+  xzgcd_def    "xzgcd m n == xzgcda (m,n,m,n,#1,#0,#0,#1)"
+
+  is_zgcd_def  "is_zgcd p m n == #0 < p  &  p dvd m  &  p dvd n  &
+                                 (ALL d. d dvd m & d dvd n --> d dvd p)"
+
+  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