src/HOL/NumberTheory/Chinese.thy
changeset 19670 2e4a143c73c5
parent 16417 9bc16273c2d4
child 20272 0ca998e83447
     1.1 --- a/src/HOL/NumberTheory/Chinese.thy	Wed May 17 01:23:40 2006 +0200
     1.2 +++ b/src/HOL/NumberTheory/Chinese.thy	Wed May 17 01:23:41 2006 +0200
     1.3 @@ -31,43 +31,34 @@
     1.4    "funsum f i 0 = f i"
     1.5    "funsum f i (Suc n) = f (Suc (i + n)) + funsum f i n"
     1.6  
     1.7 -consts
     1.8 +definition
     1.9    m_cond :: "nat => (nat => int) => bool"
    1.10 +  "m_cond n mf =
    1.11 +    ((\<forall>i. i \<le> n --> 0 < mf i) \<and>
    1.12 +      (\<forall>i j. i \<le> n \<and> j \<le> n \<and> i \<noteq> j --> zgcd (mf i, mf j) = 1))"
    1.13 +
    1.14    km_cond :: "nat => (nat => int) => (nat => int) => bool"
    1.15 +  "km_cond n kf mf = (\<forall>i. i \<le> n --> zgcd (kf i, mf i) = 1)"
    1.16 +
    1.17    lincong_sol ::
    1.18      "nat => (nat => int) => (nat => int) => (nat => int) => int => bool"
    1.19 +  "lincong_sol n kf bf mf x = (\<forall>i. i \<le> n --> zcong (kf i * x) (bf i) (mf i))"
    1.20  
    1.21    mhf :: "(nat => int) => nat => nat => int"
    1.22 +  "mhf mf n i =
    1.23 +    (if i = 0 then funprod mf (Suc 0) (n - Suc 0)
    1.24 +     else if i = n then funprod mf 0 (n - Suc 0)
    1.25 +     else funprod mf 0 (i - Suc 0) * funprod mf (Suc i) (n - Suc 0 - i))"
    1.26 +
    1.27    xilin_sol ::
    1.28      "nat => nat => (nat => int) => (nat => int) => (nat => int) => int"
    1.29 -  x_sol :: "nat => (nat => int) => (nat => int) => (nat => int) => int"
    1.30 -
    1.31 -defs
    1.32 -  m_cond_def:
    1.33 -    "m_cond n mf ==
    1.34 -      (\<forall>i. i \<le> n --> 0 < mf i) \<and>
    1.35 -      (\<forall>i j. i \<le> n \<and> j \<le> n \<and> i \<noteq> j --> zgcd (mf i, mf j) = 1)"
    1.36 -
    1.37 -  km_cond_def:
    1.38 -    "km_cond n kf mf == \<forall>i. i \<le> n --> zgcd (kf i, mf i) = 1"
    1.39 -
    1.40 -  lincong_sol_def:
    1.41 -    "lincong_sol n kf bf mf x == \<forall>i. i \<le> n --> zcong (kf i * x) (bf i) (mf i)"
    1.42 +  "xilin_sol i n kf bf mf =
    1.43 +    (if 0 < n \<and> i \<le> n \<and> m_cond n mf \<and> km_cond n kf mf then
    1.44 +        (SOME x. 0 \<le> x \<and> x < mf i \<and> zcong (kf i * mhf mf n i * x) (bf i) (mf i))
    1.45 +     else 0)"
    1.46  
    1.47 -  mhf_def:
    1.48 -    "mhf mf n i ==
    1.49 -      if i = 0 then funprod mf (Suc 0) (n - Suc 0)
    1.50 -      else if i = n then funprod mf 0 (n - Suc 0)
    1.51 -      else funprod mf 0 (i - Suc 0) * funprod mf (Suc i) (n - Suc 0 - i)"
    1.52 -
    1.53 -  xilin_sol_def:
    1.54 -    "xilin_sol i n kf bf mf ==
    1.55 -      if 0 < n \<and> i \<le> n \<and> m_cond n mf \<and> km_cond n kf mf then
    1.56 -        (SOME x. 0 \<le> x \<and> x < mf i \<and> zcong (kf i * mhf mf n i * x) (bf i) (mf i))
    1.57 -      else 0"
    1.58 -
    1.59 -  x_sol_def:
    1.60 -    "x_sol n kf bf mf == funsum (\<lambda>i. xilin_sol i n kf bf mf * mhf mf n i) 0 n"
    1.61 +  x_sol :: "nat => (nat => int) => (nat => int) => (nat => int) => int"
    1.62 +  "x_sol n kf bf mf = funsum (\<lambda>i. xilin_sol i n kf bf mf * mhf mf n i) 0 n"
    1.63  
    1.64  
    1.65  text {* \medskip @{term funprod} and @{term funsum} *}