src/HOL/NumberTheory/Chinese.thy
 author paulson Thu, 03 Aug 2000 10:46:01 +0200 changeset 9508 4d01dbf6ded7 child 11049 7eef34adb852 permissions -rw-r--r--
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
```
(*  Title:	Chinese.thy
ID:         \$Id\$
Author:	Thomas M. Rasmussen
Copyright	2000  University of Cambridge
*)

Chinese = IntPrimes +

consts
funprod     :: (nat => int) => nat => nat => int
funsum      :: (nat => int) => nat => nat => int

primrec
"funprod f i 0        = f i"
"funprod f i (Suc n)  = (f (Suc (i+n)))*(funprod f i n)"

primrec
"funsum f i 0         = f i"
"funsum f i (Suc n)   = (f (Suc (i+n)))+(funsum f i n)"

consts
m_cond      :: [nat,nat => int] => bool
km_cond     :: [nat,nat => int,nat => int] => bool
lincong_sol :: [nat,nat => int,nat => int,nat => int,int] => bool

mhf         :: (nat => int) => nat => nat => int
xilin_sol   :: [nat,nat,nat => int,nat => int,nat => int] => int
x_sol       :: [nat,nat => int,nat => int,nat => int] => int

defs
m_cond_def   "m_cond n mf ==
(ALL i. i<=n --> #0 < mf i) &
(ALL i j. i<=n & j<=n & i ~= j --> zgcd(mf i,mf j) = #1)"

km_cond_def  "km_cond n kf mf == (ALL i. i<=n --> zgcd(kf i,mf i) = #1)"

lincong_sol_def "lincong_sol n kf bf mf x ==
(ALL i. i<=n --> zcong ((kf i)*x) (bf i) (mf i))"

mhf_def  "mhf mf n i == (if i=0 then (funprod mf 1 (n-1))
else (if i=n then (funprod mf 0 (n-1))
else ((funprod mf 0 (i-1)) *
(funprod mf (i+1) (n-1-i)))))"

xilin_sol_def "xilin_sol i n kf bf mf ==
(if 0<n & i<=n & m_cond n mf & km_cond n kf mf then
(@ x. #0<=x & x<(mf i) &
zcong ((kf i)*(mhf mf n i)*x) (bf i) (mf i))
else #0)"

x_sol_def "x_sol n kf bf mf ==
(funsum (%i. (xilin_sol i n kf bf mf)*(mhf mf n i)) 0 n)"

end
```