src/HOL/NumberTheory/Chinese.thy
changeset 11049 7eef34adb852
parent 9508 4d01dbf6ded7
child 11468 02cd5d5bc497
     1.1 --- a/src/HOL/NumberTheory/Chinese.thy	Sat Feb 03 17:43:34 2001 +0100
     1.2 +++ b/src/HOL/NumberTheory/Chinese.thy	Sun Feb 04 19:31:13 2001 +0100
     1.3 @@ -1,55 +1,260 @@
     1.4 -(*  Title:	Chinese.thy
     1.5 +(*  Title:      HOL/NumberTheory/Chinese.thy
     1.6      ID:         $Id$
     1.7 -    Author:	Thomas M. Rasmussen
     1.8 -    Copyright	2000  University of Cambridge
     1.9 +    Author:     Thomas M. Rasmussen
    1.10 +    Copyright   2000  University of Cambridge
    1.11  *)
    1.12  
    1.13 -Chinese = IntPrimes +
    1.14 +header {* The Chinese Remainder Theorem *}
    1.15 +
    1.16 +theory Chinese = IntPrimes:
    1.17 +
    1.18 +text {*
    1.19 +  The Chinese Remainder Theorem for an arbitrary finite number of
    1.20 +  equations.  (The one-equation case is included in theory @{text
    1.21 +  IntPrimes}.  Uses functions for indexing.\footnote{Maybe @{term
    1.22 +  funprod} and @{term funsum} should be based on general @{term fold}
    1.23 +  on indices?}
    1.24 +*}
    1.25 +
    1.26 +
    1.27 +subsection {* Definitions *}
    1.28  
    1.29  consts
    1.30 -  funprod     :: (nat => int) => nat => nat => int
    1.31 -  funsum      :: (nat => int) => nat => nat => int
    1.32 +  funprod :: "(nat => int) => nat => nat => int"
    1.33 +  funsum :: "(nat => int) => nat => nat => int"
    1.34  
    1.35  primrec
    1.36 -  "funprod f i 0        = f i"
    1.37 -  "funprod f i (Suc n)  = (f (Suc (i+n)))*(funprod f i n)" 
    1.38 +  "funprod f i 0 = f i"
    1.39 +  "funprod f i (Suc n) = f (Suc (i + n)) * funprod f i n"
    1.40  
    1.41  primrec
    1.42 -  "funsum f i 0         = f i"
    1.43 -  "funsum f i (Suc n)   = (f (Suc (i+n)))+(funsum f i n)" 
    1.44 -
    1.45 +  "funsum f i 0 = f i"
    1.46 +  "funsum f i (Suc n) = f (Suc (i + n)) + funsum f i n"
    1.47  
    1.48  consts
    1.49 -  m_cond      :: [nat,nat => int] => bool
    1.50 -  km_cond     :: [nat,nat => int,nat => int] => bool
    1.51 -  lincong_sol :: [nat,nat => int,nat => int,nat => int,int] => bool
    1.52 +  m_cond :: "nat => (nat => int) => bool"
    1.53 +  km_cond :: "nat => (nat => int) => (nat => int) => bool"
    1.54 +  lincong_sol ::
    1.55 +    "nat => (nat => int) => (nat => int) => (nat => int) => int => bool"
    1.56  
    1.57 -  mhf         :: (nat => int) => nat => nat => int
    1.58 -  xilin_sol   :: [nat,nat,nat => int,nat => int,nat => int] => int
    1.59 -  x_sol       :: [nat,nat => int,nat => int,nat => int] => int  
    1.60 +  mhf :: "(nat => int) => nat => nat => int"
    1.61 +  xilin_sol ::
    1.62 +    "nat => nat => (nat => int) => (nat => int) => (nat => int) => int"
    1.63 +  x_sol :: "nat => (nat => int) => (nat => int) => (nat => int) => int"
    1.64  
    1.65  defs
    1.66 -  m_cond_def   "m_cond n mf == 
    1.67 -                   (ALL i. i<=n --> #0 < mf i) & 
    1.68 -                   (ALL i j. i<=n & j<=n & i ~= j --> zgcd(mf i,mf j) = #1)"
    1.69 +  m_cond_def:
    1.70 +    "m_cond n mf ==
    1.71 +      (\<forall>i. i \<le> n --> #0 < mf i) \<and>
    1.72 +      (\<forall>i j. i \<le> n \<and> j \<le> n \<and> i \<noteq> j --> zgcd (mf i, mf j) = #1)"
    1.73 +
    1.74 +  km_cond_def:
    1.75 +    "km_cond n kf mf == \<forall>i. i \<le> n --> zgcd (kf i, mf i) = #1"
    1.76 +
    1.77 +  lincong_sol_def:
    1.78 +    "lincong_sol n kf bf mf x == \<forall>i. i \<le> n --> zcong (kf i * x) (bf i) (mf i)"
    1.79 +
    1.80 +  mhf_def:
    1.81 +    "mhf mf n i ==
    1.82 +      if i = 0 then funprod mf 1 (n - 1)
    1.83 +      else if i = n then funprod mf 0 (n - 1)
    1.84 +      else funprod mf 0 (i - 1) * funprod mf (i + 1) (n - 1 - i)"
    1.85 +
    1.86 +  xilin_sol_def:
    1.87 +    "xilin_sol i n kf bf mf ==
    1.88 +      if 0 < n \<and> i \<le> n \<and> m_cond n mf \<and> km_cond n kf mf then
    1.89 +        (SOME x. #0 \<le> x \<and> x < mf i \<and> zcong (kf i * mhf mf n i * x) (bf i) (mf i))
    1.90 +      else #0"
    1.91 +
    1.92 +  x_sol_def:
    1.93 +    "x_sol n kf bf mf == funsum (\<lambda>i. xilin_sol i n kf bf mf * mhf mf n i) 0 n"
    1.94 +
    1.95 +
    1.96 +text {* \medskip @{term funprod} and @{term funsum} *}
    1.97 +
    1.98 +lemma funprod_pos: "(\<forall>i. i \<le> n --> #0 < mf i) ==> #0 < funprod mf 0 n"
    1.99 +  apply (induct n)
   1.100 +   apply auto
   1.101 +  apply (simp add: int_0_less_mult_iff)
   1.102 +  done
   1.103 +
   1.104 +lemma funprod_zgcd [rule_format (no_asm)]:
   1.105 +  "(\<forall>i. k \<le> i \<and> i \<le> k + l --> zgcd (mf i, mf m) = #1) -->
   1.106 +    zgcd (funprod mf k l, mf m) = #1"
   1.107 +  apply (induct l)
   1.108 +   apply simp_all
   1.109 +  apply (rule impI)+
   1.110 +  apply (subst zgcd_zmult_cancel)
   1.111 +  apply auto
   1.112 +  done
   1.113  
   1.114 -  km_cond_def  "km_cond n kf mf == (ALL i. i<=n --> zgcd(kf i,mf i) = #1)"
   1.115 +lemma funprod_zdvd [rule_format]:
   1.116 +    "k \<le> i --> i \<le> k + l --> mf i dvd funprod mf k l"
   1.117 +  apply (induct l)
   1.118 +   apply auto
   1.119 +    apply (rule_tac [2] zdvd_zmult2)
   1.120 +    apply (rule_tac [3] zdvd_zmult)
   1.121 +    apply (subgoal_tac "i = k")
   1.122 +    apply (subgoal_tac [3] "i = Suc (k + n)")
   1.123 +    apply (simp_all (no_asm_simp))
   1.124 +  done
   1.125 +
   1.126 +lemma funsum_mod:
   1.127 +    "funsum f k l mod m = funsum (\<lambda>i. (f i) mod m) k l mod m"
   1.128 +  apply (induct l)
   1.129 +   apply auto
   1.130 +  apply (rule trans)
   1.131 +   apply (rule zmod_zadd1_eq)
   1.132 +  apply simp
   1.133 +  apply (rule zmod_zadd_right_eq [symmetric])
   1.134 +  done
   1.135  
   1.136 -  lincong_sol_def "lincong_sol n kf bf mf x == 
   1.137 -                   (ALL i. i<=n --> zcong ((kf i)*x) (bf i) (mf i))"
   1.138 +lemma funsum_zero [rule_format (no_asm)]:
   1.139 +    "(\<forall>i. k \<le> i \<and> i \<le> k + l --> f i = #0) --> (funsum f k l) = #0"
   1.140 +  apply (induct l)
   1.141 +   apply auto
   1.142 +  done
   1.143 +
   1.144 +lemma funsum_oneelem [rule_format (no_asm)]:
   1.145 +  "k \<le> j --> j \<le> k + l -->
   1.146 +    (\<forall>i. k \<le> i \<and> i \<le> k + l \<and> i \<noteq> j --> f i = #0) -->
   1.147 +    funsum f k l = f j"
   1.148 +  apply (induct l)
   1.149 +   prefer 2
   1.150 +   apply clarify
   1.151 +   defer
   1.152 +   apply clarify
   1.153 +   apply (subgoal_tac "k = j")
   1.154 +    apply (simp_all (no_asm_simp))
   1.155 +  apply (case_tac "Suc (k + n) = j")
   1.156 +   apply (subgoal_tac "funsum f k n = #0")
   1.157 +    apply (rule_tac [2] funsum_zero)
   1.158 +    apply (subgoal_tac [3] "f (Suc (k + n)) = #0")
   1.159 +     apply (subgoal_tac [3] "j \<le> k + n")
   1.160 +      prefer 4
   1.161 +      apply arith
   1.162 +     apply auto
   1.163 +  done
   1.164 +
   1.165 +
   1.166 +subsection {* Chinese: uniqueness *}
   1.167  
   1.168 -  mhf_def  "mhf mf n i == (if i=0 then (funprod mf 1 (n-1)) 
   1.169 -                           else (if i=n then (funprod mf 0 (n-1))
   1.170 -                           else ((funprod mf 0 (i-1)) * 
   1.171 -                                 (funprod mf (i+1) (n-1-i)))))"
   1.172 +lemma aux:
   1.173 +  "m_cond n mf ==> km_cond n kf mf
   1.174 +    ==> lincong_sol n kf bf mf x ==> lincong_sol n kf bf mf y
   1.175 +    ==> [x = y] (mod mf n)"
   1.176 +  apply (unfold m_cond_def km_cond_def lincong_sol_def)
   1.177 +  apply (rule iffD1)
   1.178 +   apply (rule_tac k = "kf n" in zcong_cancel2)
   1.179 +    apply (rule_tac [3] b = "bf n" in zcong_trans)
   1.180 +     prefer 4
   1.181 +     apply (subst zcong_sym)
   1.182 +     defer
   1.183 +     apply (rule order_less_imp_le)
   1.184 +     apply simp_all
   1.185 +  done
   1.186 +
   1.187 +lemma zcong_funprod [rule_format]:
   1.188 +  "m_cond n mf --> km_cond n kf mf -->
   1.189 +    lincong_sol n kf bf mf x --> lincong_sol n kf bf mf y -->
   1.190 +    [x = y] (mod funprod mf 0 n)"
   1.191 +  apply (induct n)
   1.192 +   apply (simp_all (no_asm))
   1.193 +   apply (blast intro: aux)
   1.194 +  apply (rule impI)+
   1.195 +  apply (rule zcong_zgcd_zmult_zmod)
   1.196 +    apply (blast intro: aux)
   1.197 +    prefer 2
   1.198 +    apply (subst zgcd_commute)
   1.199 +    apply (rule funprod_zgcd)
   1.200 +   apply (auto simp add: m_cond_def km_cond_def lincong_sol_def)
   1.201 +  done
   1.202 +
   1.203 +
   1.204 +subsection {* Chinese: existence *}
   1.205 +
   1.206 +lemma unique_xi_sol:
   1.207 +  "0 < n ==> i \<le> n ==> m_cond n mf ==> km_cond n kf mf
   1.208 +    ==> \<exists>!x. #0 \<le> x \<and> x < mf i \<and> [kf i * mhf mf n i * x = bf i] (mod mf i)"
   1.209 +  apply (rule zcong_lineq_unique)
   1.210 +   apply (tactic {* stac (thm "zgcd_zmult_cancel") 2 *})
   1.211 +    apply (unfold m_cond_def km_cond_def mhf_def)
   1.212 +    apply (simp_all (no_asm_simp))
   1.213 +  apply safe
   1.214 +    apply (tactic {* stac (thm "zgcd_zmult_cancel") 3 *})
   1.215 +     apply (rule_tac [!] funprod_zgcd)
   1.216 +     apply safe
   1.217 +     apply simp_all
   1.218 +    apply (subgoal_tac [3] "ia \<le> n")
   1.219 +     prefer 4
   1.220 +     apply arith
   1.221 +     apply (subgoal_tac "i<n")
   1.222 +     prefer 2
   1.223 +     apply arith
   1.224 +    apply (case_tac [2] i)
   1.225 +     apply simp_all
   1.226 +  done
   1.227  
   1.228 -  xilin_sol_def "xilin_sol i n kf bf mf ==
   1.229 -                  (if 0<n & i<=n & m_cond n mf & km_cond n kf mf then
   1.230 -                    (@ x. #0<=x & x<(mf i) & 
   1.231 -                          zcong ((kf i)*(mhf mf n i)*x) (bf i) (mf i))
   1.232 -                    else #0)"
   1.233 +lemma aux:
   1.234 +    "0 < n ==> i \<le> n ==> j \<le> n ==> j \<noteq> i ==> mf j dvd mhf mf n i"
   1.235 +  apply (unfold mhf_def)
   1.236 +  apply (case_tac "i = 0")
   1.237 +   apply (case_tac [2] "i = n")
   1.238 +    apply (simp_all (no_asm_simp))
   1.239 +    apply (case_tac [3] "j < i")
   1.240 +     apply (rule_tac [3] zdvd_zmult2)
   1.241 +     apply (rule_tac [4] zdvd_zmult)
   1.242 +     apply (rule_tac [!] funprod_zdvd)
   1.243 +          apply arith+
   1.244 +  done
   1.245 +
   1.246 +lemma x_sol_lin:
   1.247 +  "0 < n ==> i \<le> n
   1.248 +    ==> x_sol n kf bf mf mod mf i =
   1.249 +      xilin_sol i n kf bf mf * mhf mf n i mod mf i"
   1.250 +  apply (unfold x_sol_def)
   1.251 +  apply (subst funsum_mod)
   1.252 +  apply (subst funsum_oneelem)
   1.253 +     apply auto
   1.254 +  apply (subst zdvd_iff_zmod_eq_0 [symmetric])
   1.255 +  apply (rule zdvd_zmult)
   1.256 +  apply (rule aux)
   1.257 +  apply auto
   1.258 +  done
   1.259 +
   1.260 +
   1.261 +subsection {* Chinese *}
   1.262  
   1.263 -  x_sol_def "x_sol n kf bf mf ==
   1.264 -              (funsum (%i. (xilin_sol i n kf bf mf)*(mhf mf n i)) 0 n)"
   1.265 +lemma chinese_remainder:
   1.266 +  "0 < n ==> m_cond n mf ==> km_cond n kf mf
   1.267 +    ==> \<exists>!x. #0 \<le> x \<and> x < funprod mf 0 n \<and> lincong_sol n kf bf mf x"
   1.268 +  apply safe
   1.269 +   apply (rule_tac [2] m = "funprod mf 0 n" in zcong_zless_imp_eq)
   1.270 +       apply (rule_tac [6] zcong_funprod)
   1.271 +          apply auto
   1.272 +  apply (rule_tac x = "x_sol n kf bf mf mod funprod mf 0 n" in exI)
   1.273 +  apply (unfold lincong_sol_def)
   1.274 +  apply safe
   1.275 +    apply (tactic {* stac (thm "zcong_zmod") 3 *})
   1.276 +    apply (tactic {* stac (thm "zmod_zmult_distrib") 3 *})
   1.277 +    apply (tactic {* stac (thm "zmod_zdvd_zmod") 3 *})
   1.278 +      apply (tactic {* stac (thm "x_sol_lin") 5 *})
   1.279 +        apply (tactic {* stac (thm "zmod_zmult_distrib" RS sym) 7 *})
   1.280 +        apply (tactic {* stac (thm "zcong_zmod" RS sym) 7 *})
   1.281 +        apply (subgoal_tac [7]
   1.282 +          "#0 \<le> xilin_sol i n kf bf mf \<and> xilin_sol i n kf bf mf < mf i
   1.283 +          \<and> [kf i * mhf mf n i * xilin_sol i n kf bf mf = bf i] (mod mf i)")
   1.284 +         prefer 7
   1.285 +         apply (simp add: zmult_ac)
   1.286 +        apply (unfold xilin_sol_def)
   1.287 +        apply (tactic {* Asm_simp_tac 7 *})
   1.288 +        apply (rule_tac [7] ex1_implies_ex [THEN someI_ex])
   1.289 +        apply (rule_tac [7] unique_xi_sol)
   1.290 +           apply (rule_tac [4] funprod_zdvd)
   1.291 +            apply (unfold m_cond_def)
   1.292 +            apply (rule funprod_pos [THEN pos_mod_sign])
   1.293 +            apply (rule_tac [2] funprod_pos [THEN pos_mod_bound])
   1.294 +            apply auto
   1.295 +  done
   1.296  
   1.297  end