src/HOL/NumberTheory/Chinese.thy
 author paulson Tue Jun 28 15:27:45 2005 +0200 (2005-06-28) changeset 16587 b34c8aa657a5 parent 16417 9bc16273c2d4 child 19670 2e4a143c73c5 permissions -rw-r--r--
Constant "If" is now local
```     1 (*  Title:      HOL/NumberTheory/Chinese.thy
```
```     2     ID:         \$Id\$
```
```     3     Author:     Thomas M. Rasmussen
```
```     4     Copyright   2000  University of Cambridge
```
```     5 *)
```
```     6
```
```     7 header {* The Chinese Remainder Theorem *}
```
```     8
```
```     9 theory Chinese imports IntPrimes begin
```
```    10
```
```    11 text {*
```
```    12   The Chinese Remainder Theorem for an arbitrary finite number of
```
```    13   equations.  (The one-equation case is included in theory @{text
```
```    14   IntPrimes}.  Uses functions for indexing.\footnote{Maybe @{term
```
```    15   funprod} and @{term funsum} should be based on general @{term fold}
```
```    16   on indices?}
```
```    17 *}
```
```    18
```
```    19
```
```    20 subsection {* Definitions *}
```
```    21
```
```    22 consts
```
```    23   funprod :: "(nat => int) => nat => nat => int"
```
```    24   funsum :: "(nat => int) => nat => nat => int"
```
```    25
```
```    26 primrec
```
```    27   "funprod f i 0 = f i"
```
```    28   "funprod f i (Suc n) = f (Suc (i + n)) * funprod f i n"
```
```    29
```
```    30 primrec
```
```    31   "funsum f i 0 = f i"
```
```    32   "funsum f i (Suc n) = f (Suc (i + n)) + funsum f i n"
```
```    33
```
```    34 consts
```
```    35   m_cond :: "nat => (nat => int) => bool"
```
```    36   km_cond :: "nat => (nat => int) => (nat => int) => bool"
```
```    37   lincong_sol ::
```
```    38     "nat => (nat => int) => (nat => int) => (nat => int) => int => bool"
```
```    39
```
```    40   mhf :: "(nat => int) => nat => nat => int"
```
```    41   xilin_sol ::
```
```    42     "nat => nat => (nat => int) => (nat => int) => (nat => int) => int"
```
```    43   x_sol :: "nat => (nat => int) => (nat => int) => (nat => int) => int"
```
```    44
```
```    45 defs
```
```    46   m_cond_def:
```
```    47     "m_cond n mf ==
```
```    48       (\<forall>i. i \<le> n --> 0 < mf i) \<and>
```
```    49       (\<forall>i j. i \<le> n \<and> j \<le> n \<and> i \<noteq> j --> zgcd (mf i, mf j) = 1)"
```
```    50
```
```    51   km_cond_def:
```
```    52     "km_cond n kf mf == \<forall>i. i \<le> n --> zgcd (kf i, mf i) = 1"
```
```    53
```
```    54   lincong_sol_def:
```
```    55     "lincong_sol n kf bf mf x == \<forall>i. i \<le> n --> zcong (kf i * x) (bf i) (mf i)"
```
```    56
```
```    57   mhf_def:
```
```    58     "mhf mf n i ==
```
```    59       if i = 0 then funprod mf (Suc 0) (n - Suc 0)
```
```    60       else if i = n then funprod mf 0 (n - Suc 0)
```
```    61       else funprod mf 0 (i - Suc 0) * funprod mf (Suc i) (n - Suc 0 - i)"
```
```    62
```
```    63   xilin_sol_def:
```
```    64     "xilin_sol i n kf bf mf ==
```
```    65       if 0 < n \<and> i \<le> n \<and> m_cond n mf \<and> km_cond n kf mf then
```
```    66         (SOME x. 0 \<le> x \<and> x < mf i \<and> zcong (kf i * mhf mf n i * x) (bf i) (mf i))
```
```    67       else 0"
```
```    68
```
```    69   x_sol_def:
```
```    70     "x_sol n kf bf mf == funsum (\<lambda>i. xilin_sol i n kf bf mf * mhf mf n i) 0 n"
```
```    71
```
```    72
```
```    73 text {* \medskip @{term funprod} and @{term funsum} *}
```
```    74
```
```    75 lemma funprod_pos: "(\<forall>i. i \<le> n --> 0 < mf i) ==> 0 < funprod mf 0 n"
```
```    76   apply (induct n)
```
```    77    apply auto
```
```    78   apply (simp add: zero_less_mult_iff)
```
```    79   done
```
```    80
```
```    81 lemma funprod_zgcd [rule_format (no_asm)]:
```
```    82   "(\<forall>i. k \<le> i \<and> i \<le> k + l --> zgcd (mf i, mf m) = 1) -->
```
```    83     zgcd (funprod mf k l, mf m) = 1"
```
```    84   apply (induct l)
```
```    85    apply simp_all
```
```    86   apply (rule impI)+
```
```    87   apply (subst zgcd_zmult_cancel)
```
```    88   apply auto
```
```    89   done
```
```    90
```
```    91 lemma funprod_zdvd [rule_format]:
```
```    92     "k \<le> i --> i \<le> k + l --> mf i dvd funprod mf k l"
```
```    93   apply (induct l)
```
```    94    apply auto
```
```    95     apply (rule_tac [1] zdvd_zmult2)
```
```    96     apply (rule_tac [2] zdvd_zmult)
```
```    97     apply (subgoal_tac "i = Suc (k + l)")
```
```    98     apply (simp_all (no_asm_simp))
```
```    99   done
```
```   100
```
```   101 lemma funsum_mod:
```
```   102     "funsum f k l mod m = funsum (\<lambda>i. (f i) mod m) k l mod m"
```
```   103   apply (induct l)
```
```   104    apply auto
```
```   105   apply (rule trans)
```
```   106    apply (rule zmod_zadd1_eq)
```
```   107   apply simp
```
```   108   apply (rule zmod_zadd_right_eq [symmetric])
```
```   109   done
```
```   110
```
```   111 lemma funsum_zero [rule_format (no_asm)]:
```
```   112     "(\<forall>i. k \<le> i \<and> i \<le> k + l --> f i = 0) --> (funsum f k l) = 0"
```
```   113   apply (induct l)
```
```   114    apply auto
```
```   115   done
```
```   116
```
```   117 lemma funsum_oneelem [rule_format (no_asm)]:
```
```   118   "k \<le> j --> j \<le> k + l -->
```
```   119     (\<forall>i. k \<le> i \<and> i \<le> k + l \<and> i \<noteq> j --> f i = 0) -->
```
```   120     funsum f k l = f j"
```
```   121   apply (induct l)
```
```   122    prefer 2
```
```   123    apply clarify
```
```   124    defer
```
```   125    apply clarify
```
```   126    apply (subgoal_tac "k = j")
```
```   127     apply (simp_all (no_asm_simp))
```
```   128   apply (case_tac "Suc (k + l) = j")
```
```   129    apply (subgoal_tac "funsum f k l = 0")
```
```   130     apply (rule_tac [2] funsum_zero)
```
```   131     apply (subgoal_tac [3] "f (Suc (k + l)) = 0")
```
```   132      apply (subgoal_tac [3] "j \<le> k + l")
```
```   133       prefer 4
```
```   134       apply arith
```
```   135      apply auto
```
```   136   done
```
```   137
```
```   138
```
```   139 subsection {* Chinese: uniqueness *}
```
```   140
```
```   141 lemma zcong_funprod_aux:
```
```   142   "m_cond n mf ==> km_cond n kf mf
```
```   143     ==> lincong_sol n kf bf mf x ==> lincong_sol n kf bf mf y
```
```   144     ==> [x = y] (mod mf n)"
```
```   145   apply (unfold m_cond_def km_cond_def lincong_sol_def)
```
```   146   apply (rule iffD1)
```
```   147    apply (rule_tac k = "kf n" in zcong_cancel2)
```
```   148     apply (rule_tac [3] b = "bf n" in zcong_trans)
```
```   149      prefer 4
```
```   150      apply (subst zcong_sym)
```
```   151      defer
```
```   152      apply (rule order_less_imp_le)
```
```   153      apply simp_all
```
```   154   done
```
```   155
```
```   156 lemma zcong_funprod [rule_format]:
```
```   157   "m_cond n mf --> km_cond n kf mf -->
```
```   158     lincong_sol n kf bf mf x --> lincong_sol n kf bf mf y -->
```
```   159     [x = y] (mod funprod mf 0 n)"
```
```   160   apply (induct n)
```
```   161    apply (simp_all (no_asm))
```
```   162    apply (blast intro: zcong_funprod_aux)
```
```   163   apply (rule impI)+
```
```   164   apply (rule zcong_zgcd_zmult_zmod)
```
```   165     apply (blast intro: zcong_funprod_aux)
```
```   166     prefer 2
```
```   167     apply (subst zgcd_commute)
```
```   168     apply (rule funprod_zgcd)
```
```   169    apply (auto simp add: m_cond_def km_cond_def lincong_sol_def)
```
```   170   done
```
```   171
```
```   172
```
```   173 subsection {* Chinese: existence *}
```
```   174
```
```   175 lemma unique_xi_sol:
```
```   176   "0 < n ==> i \<le> n ==> m_cond n mf ==> km_cond n kf mf
```
```   177     ==> \<exists>!x. 0 \<le> x \<and> x < mf i \<and> [kf i * mhf mf n i * x = bf i] (mod mf i)"
```
```   178   apply (rule zcong_lineq_unique)
```
```   179    apply (tactic {* stac (thm "zgcd_zmult_cancel") 2 *})
```
```   180     apply (unfold m_cond_def km_cond_def mhf_def)
```
```   181     apply (simp_all (no_asm_simp))
```
```   182   apply safe
```
```   183     apply (tactic {* stac (thm "zgcd_zmult_cancel") 3 *})
```
```   184      apply (rule_tac [!] funprod_zgcd)
```
```   185      apply safe
```
```   186      apply simp_all
```
```   187    apply (subgoal_tac "i<n")
```
```   188     prefer 2
```
```   189     apply arith
```
```   190    apply (case_tac [2] i)
```
```   191     apply simp_all
```
```   192   done
```
```   193
```
```   194 lemma x_sol_lin_aux:
```
```   195     "0 < n ==> i \<le> n ==> j \<le> n ==> j \<noteq> i ==> mf j dvd mhf mf n i"
```
```   196   apply (unfold mhf_def)
```
```   197   apply (case_tac "i = 0")
```
```   198    apply (case_tac [2] "i = n")
```
```   199     apply (simp_all (no_asm_simp))
```
```   200     apply (case_tac [3] "j < i")
```
```   201      apply (rule_tac [3] zdvd_zmult2)
```
```   202      apply (rule_tac [4] zdvd_zmult)
```
```   203      apply (rule_tac [!] funprod_zdvd)
```
```   204           apply arith+
```
```   205   done
```
```   206
```
```   207 lemma x_sol_lin:
```
```   208   "0 < n ==> i \<le> n
```
```   209     ==> x_sol n kf bf mf mod mf i =
```
```   210       xilin_sol i n kf bf mf * mhf mf n i mod mf i"
```
```   211   apply (unfold x_sol_def)
```
```   212   apply (subst funsum_mod)
```
```   213   apply (subst funsum_oneelem)
```
```   214      apply auto
```
```   215   apply (subst zdvd_iff_zmod_eq_0 [symmetric])
```
```   216   apply (rule zdvd_zmult)
```
```   217   apply (rule x_sol_lin_aux)
```
```   218   apply auto
```
```   219   done
```
```   220
```
```   221
```
```   222 subsection {* Chinese *}
```
```   223
```
```   224 lemma chinese_remainder:
```
```   225   "0 < n ==> m_cond n mf ==> km_cond n kf mf
```
```   226     ==> \<exists>!x. 0 \<le> x \<and> x < funprod mf 0 n \<and> lincong_sol n kf bf mf x"
```
```   227   apply safe
```
```   228    apply (rule_tac [2] m = "funprod mf 0 n" in zcong_zless_imp_eq)
```
```   229        apply (rule_tac [6] zcong_funprod)
```
```   230           apply auto
```
```   231   apply (rule_tac x = "x_sol n kf bf mf mod funprod mf 0 n" in exI)
```
```   232   apply (unfold lincong_sol_def)
```
```   233   apply safe
```
```   234     apply (tactic {* stac (thm "zcong_zmod") 3 *})
```
```   235     apply (tactic {* stac (thm "zmod_zmult_distrib") 3 *})
```
```   236     apply (tactic {* stac (thm "zmod_zdvd_zmod") 3 *})
```
```   237       apply (tactic {* stac (thm "x_sol_lin") 5 *})
```
```   238         apply (tactic {* stac (thm "zmod_zmult_distrib" RS sym) 7 *})
```
```   239         apply (tactic {* stac (thm "zcong_zmod" RS sym) 7 *})
```
```   240         apply (subgoal_tac [7]
```
```   241           "0 \<le> xilin_sol i n kf bf mf \<and> xilin_sol i n kf bf mf < mf i
```
```   242           \<and> [kf i * mhf mf n i * xilin_sol i n kf bf mf = bf i] (mod mf i)")
```
```   243          prefer 7
```
```   244          apply (simp add: zmult_ac)
```
```   245         apply (unfold xilin_sol_def)
```
```   246         apply (tactic {* Asm_simp_tac 7 *})
```
```   247         apply (rule_tac [7] ex1_implies_ex [THEN someI_ex])
```
```   248         apply (rule_tac [7] unique_xi_sol)
```
```   249            apply (rule_tac [4] funprod_zdvd)
```
```   250             apply (unfold m_cond_def)
```
```   251             apply (rule funprod_pos [THEN pos_mod_sign])
```
```   252             apply (rule_tac [2] funprod_pos [THEN pos_mod_bound])
```
```   253             apply auto
```
```   254   done
```
```   255
```
```   256 end
```