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