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