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