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} *}
```