src/HOL/NumberTheory/Chinese.thy
author paulson
Thu Aug 03 10:46:01 2000 +0200 (2000-08-03)
changeset 9508 4d01dbf6ded7
child 11049 7eef34adb852
permissions -rw-r--r--
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
     1 (*  Title:	Chinese.thy
     2     ID:         $Id$
     3     Author:	Thomas M. Rasmussen
     4     Copyright	2000  University of Cambridge
     5 *)
     6 
     7 Chinese = IntPrimes +
     8 
     9 consts
    10   funprod     :: (nat => int) => nat => nat => int
    11   funsum      :: (nat => int) => nat => nat => int
    12 
    13 primrec
    14   "funprod f i 0        = f i"
    15   "funprod f i (Suc n)  = (f (Suc (i+n)))*(funprod f i n)" 
    16 
    17 primrec
    18   "funsum f i 0         = f i"
    19   "funsum f i (Suc n)   = (f (Suc (i+n)))+(funsum f i n)" 
    20 
    21 
    22 consts
    23   m_cond      :: [nat,nat => int] => bool
    24   km_cond     :: [nat,nat => int,nat => int] => bool
    25   lincong_sol :: [nat,nat => int,nat => int,nat => int,int] => bool
    26 
    27   mhf         :: (nat => int) => nat => nat => int
    28   xilin_sol   :: [nat,nat,nat => int,nat => int,nat => int] => int
    29   x_sol       :: [nat,nat => int,nat => int,nat => int] => int  
    30 
    31 defs
    32   m_cond_def   "m_cond n mf == 
    33                    (ALL i. i<=n --> #0 < mf i) & 
    34                    (ALL i j. i<=n & j<=n & i ~= j --> zgcd(mf i,mf j) = #1)"
    35 
    36   km_cond_def  "km_cond n kf mf == (ALL i. i<=n --> zgcd(kf i,mf i) = #1)"
    37 
    38   lincong_sol_def "lincong_sol n kf bf mf x == 
    39                    (ALL i. i<=n --> zcong ((kf i)*x) (bf i) (mf i))"
    40 
    41   mhf_def  "mhf mf n i == (if i=0 then (funprod mf 1 (n-1)) 
    42                            else (if i=n then (funprod mf 0 (n-1))
    43                            else ((funprod mf 0 (i-1)) * 
    44                                  (funprod mf (i+1) (n-1-i)))))"
    45 
    46   xilin_sol_def "xilin_sol i n kf bf mf ==
    47                   (if 0<n & i<=n & m_cond n mf & km_cond n kf mf then
    48                     (@ x. #0<=x & x<(mf i) & 
    49                           zcong ((kf i)*(mhf mf n i)*x) (bf i) (mf i))
    50                     else #0)"
    51 
    52   x_sol_def "x_sol n kf bf mf ==
    53               (funsum (%i. (xilin_sol i n kf bf mf)*(mhf mf n i)) 0 n)"
    54 
    55 end