author  nipkow 
Fri, 24 Nov 2000 16:49:27 +0100  
changeset 10519  ade64af4c57c 
parent 10147  178deaacb244 
child 11049  7eef34adb852 
permissions  rwrr 
9508
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

1 
(* Title: IntPrimes.thy 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

2 
ID: $Id$ 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

3 
Author: Thomas M. Rasmussen 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

4 
Copyright 2000 University of Cambridge 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

5 
*) 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

6 

10147  7 
IntPrimes = Primes + 
9508
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

8 

4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

9 
consts 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

10 
xzgcda :: "int*int*int*int*int*int*int*int => int*int*int" 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

11 
xzgcd :: "[int,int] => int*int*int" 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

12 
zprime :: int set 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

13 
zcong :: [int,int,int] => bool ("(1[_ = _] '(mod _'))") 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

14 

4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

15 
recdef xzgcda 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

16 
"measure ((%(m,n,r',r,s',s,t',t).(nat r)) 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

17 
::int*int*int*int*int*int*int*int=>nat)" 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

18 
simpset "simpset() addsimps [pos_mod_bound]" 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

19 
"xzgcda (m,n,r',r,s',s,t',t) = 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

20 
(if r<=#0 then (r',s',t') else 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

21 
xzgcda(m,n,r,r' mod r,s,s'(r' div r)*s,t,t'(r' div r)*t))" 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

22 

9943  23 
constdefs 
24 
zgcd :: "int*int => int" 

25 
"zgcd == %(x,y). int (gcd(nat (abs x), nat (abs y)))" 

26 

9508
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

27 
defs 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

28 
xzgcd_def "xzgcd m n == xzgcda (m,n,m,n,#1,#0,#0,#1)" 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

29 

4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

30 
zprime_def "zprime == {p. #1<p & (ALL m. m dvd p > m=#1  m=p)}" 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

31 

4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

32 
zcong_def "[a=b] (mod m) == m dvd (ab)" 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

33 

4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

34 
end 