--- a/src/HOL/NumberTheory/IntPrimes.thy Wed Sep 13 18:45:10 2000 +0200
+++ b/src/HOL/NumberTheory/IntPrimes.thy Wed Sep 13 18:46:09 2000 +0200
@@ -4,20 +4,14 @@
Copyright 2000 University of Cambridge
*)
-IntPrimes = Main + IntDiv +
+IntPrimes = Main + IntDiv + Primes +
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)"
@@ -26,12 +20,13 @@
(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)"
- 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)"