src/HOL/NumberTheory/Chinese.ML
changeset 9508 4d01dbf6ded7
child 9572 bfee45ac5d38
equal deleted inserted replaced
9507:7903ca5fecf1 9508:4d01dbf6ded7
       
     1 (*  Title:	Chinese.ML
       
     2     ID:         $Id$
       
     3     Author:	Thomas M. Rasmussen
       
     4     Copyright	2000  University of Cambridge
       
     5 
       
     6 The Chinese Remainder Theorem for an arbitrary finite number of equations. 
       
     7 (The one-equation case is included in 'IntPrimes')
       
     8 
       
     9 Uses functions for indexing. Maybe 'funprod' and 'funsum'
       
    10 should be based on general 'fold' on indices?
       
    11 *)
       
    12 
       
    13 
       
    14 (*** extra nat theorems ***)
       
    15 
       
    16 Goal "[| k <= i; i <= k |] ==> i = (k::nat)";
       
    17 by (rtac diffs0_imp_equal 1);
       
    18 by (ALLGOALS (stac diff_is_0_eq)); 
       
    19 by Auto_tac;
       
    20 qed "le_le_imp_eq";
       
    21 
       
    22 Goal "m~=n --> m<=n --> m<(n::nat)";
       
    23 by (induct_tac "n" 1);
       
    24 by Auto_tac;
       
    25 by (subgoal_tac "m = Suc n" 1);
       
    26 by (rtac le_le_imp_eq 2);
       
    27 by Auto_tac;
       
    28 qed_spec_mp "neq_le_imp_less";
       
    29 
       
    30 
       
    31 (*** funprod and funsum ***)
       
    32 
       
    33 Goal "(ALL i. i <= n --> #0 < mf i) --> #0 < funprod mf 0 n";
       
    34 by (induct_tac "n" 1);
       
    35 by Auto_tac;
       
    36 by (asm_full_simp_tac (simpset() addsimps [int_0_less_mult_iff]) 1);
       
    37 qed_spec_mp "funprod_pos";
       
    38 
       
    39 Goal "(ALL i. k<=i & i<=(k+l) --> zgcd (mf i, mf m) = #1) --> \
       
    40 \      #0 < mf m --> zgcd (funprod mf k l, mf m) = #1";
       
    41 by (induct_tac "l" 1);
       
    42 by (ALLGOALS Simp_tac);
       
    43 by (REPEAT (rtac impI 1));
       
    44 by (stac zgcd_zmult_cancel 1);
       
    45 by Auto_tac;
       
    46 qed_spec_mp "funprod_zgcd";
       
    47 
       
    48 Goal "k<=i --> i<=(k+l) --> (mf i) dvd (funprod mf k l)";     
       
    49 by (induct_tac "l" 1);
       
    50 by Auto_tac;
       
    51 by (rtac zdvd_zmult2 2);
       
    52 by (rtac zdvd_zmult 3);
       
    53 by (subgoal_tac "i=k" 1);
       
    54 by (subgoal_tac "i=Suc (k + n)" 3);
       
    55 by (ALLGOALS Asm_simp_tac);
       
    56 qed_spec_mp "funprod_zdvd";
       
    57 
       
    58 Goal "(funsum f k l) mod m = (funsum (%i. (f i) mod m) k l) mod m";
       
    59 by (induct_tac "l" 1);
       
    60 by Auto_tac;
       
    61 by (rtac trans 1);
       
    62 by (rtac zmod_zadd1_eq 1);
       
    63 by (Asm_simp_tac 1);
       
    64 by (rtac (zmod_zadd_right_eq RS sym) 1);
       
    65 qed "funsum_mod";
       
    66 
       
    67 Goal "(ALL i. k<=i & i<=(k+l) --> (f i) = #0) --> (funsum f k l) = #0";
       
    68 by (induct_tac "l" 1);
       
    69 by Auto_tac;
       
    70 qed_spec_mp "funsum_zero";
       
    71 
       
    72 Goal "k<=j --> j<=(k+l) --> \
       
    73 \     (ALL i. k<=i & i<=(k+l) & i~=j --> (f i) = #0) --> \
       
    74 \     (funsum f k l) = (f j)";
       
    75 by (induct_tac "l" 1);
       
    76 by (ALLGOALS Simp_tac); 
       
    77 by (ALLGOALS (REPEAT o (rtac impI)));
       
    78 by (case_tac "Suc (k+n) = j" 2);
       
    79 by (subgoal_tac "funsum f k n = #0" 2);
       
    80 by (rtac funsum_zero 3);
       
    81 by (subgoal_tac "f (Suc (k+n)) = #0" 4);
       
    82 by (subgoal_tac "k=j" 1);
       
    83 by (Clarify_tac 4);
       
    84 by (subgoal_tac "j<=k+n" 5);
       
    85 by (subgoal_tac "j<Suc (k+n)" 6);
       
    86 by (rtac neq_le_imp_less 7);
       
    87 by (ALLGOALS Asm_simp_tac); 
       
    88 by Auto_tac;
       
    89 qed_spec_mp "funsum_oneelem";
       
    90 
       
    91 
       
    92 (*** Chinese: Uniqueness ***)
       
    93 
       
    94 Goalw [m_cond_def,km_cond_def,lincong_sol_def]
       
    95       "[| m_cond n mf; km_cond n kf mf; \
       
    96 \         lincong_sol n kf bf mf x; lincong_sol n kf bf mf y |] \
       
    97 \     ==>  [x=y] (mod mf n)";
       
    98 by (rtac iffD1 1);
       
    99 by (res_inst_tac [("k","kf n")] zcong_cancel2 1);
       
   100 by (res_inst_tac [("b","bf n")] zcong_trans 3);
       
   101 by (stac zcong_sym 4);
       
   102 by (rtac zless_imp_zle 1);
       
   103 by (ALLGOALS Asm_simp_tac);
       
   104 val lemma = result();
       
   105 
       
   106 Goal "m_cond n mf --> km_cond n kf mf --> \
       
   107 \     lincong_sol n kf bf mf x --> lincong_sol n kf bf mf y --> \
       
   108 \     [x=y] (mod funprod mf 0 n)";
       
   109 by (induct_tac "n" 1);
       
   110 by (ALLGOALS Simp_tac);
       
   111 by (blast_tac (claset() addIs [lemma]) 1);
       
   112 by (REPEAT (rtac impI 1));
       
   113 by (rtac zcong_zgcd_zmult_zmod 1);
       
   114 by (blast_tac (claset() addIs [lemma]) 3);
       
   115 by (stac zgcd_commute 4);
       
   116 by (rtac funprod_zgcd 6);
       
   117 by (rtac funprod_pos 5);
       
   118 by (rtac funprod_pos 2);
       
   119 by (rewrite_goals_tac [m_cond_def,km_cond_def,lincong_sol_def]);
       
   120 by Auto_tac;
       
   121 qed_spec_mp "zcong_funprod";
       
   122 
       
   123 
       
   124 (* Chinese: Existence *)
       
   125 
       
   126 Goal "[| 0<n; i<n |] ==> Suc (i+(n-Suc(i))) = n";
       
   127 by (subgoal_tac "Suc (i+(n-1-i)) = n" 1);
       
   128 by (stac le_add_diff_inverse 2);
       
   129 by (stac le_pred_eq 2);
       
   130 by Auto_tac;
       
   131 val suclemma = result();
       
   132 
       
   133 Goal "[| 0<n; i<=n; m_cond n mf; km_cond n kf mf |] \
       
   134 \     ==> EX! x. #0<=x & x<(mf i) & \
       
   135 \                [(kf i)*(mhf mf n i)*x = bf i] (mod mf i)";
       
   136 by (rtac zcong_lineq_unique 1);
       
   137 by (stac zgcd_zmult_cancel 2);
       
   138 by (rewrite_goals_tac [m_cond_def,km_cond_def,mhf_def]);
       
   139 by (case_tac "i=0" 4);
       
   140 by (case_tac "i=n" 5);
       
   141 by (ALLGOALS Asm_simp_tac);
       
   142 by (stac zgcd_zmult_cancel 3);
       
   143 by (Asm_simp_tac 3);
       
   144 by (ALLGOALS (rtac funprod_zgcd));
       
   145 by Safe_tac;
       
   146 by (ALLGOALS Asm_full_simp_tac);
       
   147 by (subgoal_tac "i<=n" 1);
       
   148 by (res_inst_tac [("j","n-1")] le_trans 2);
       
   149 by (subgoal_tac "i~=n" 1);
       
   150 by (subgoal_tac "ia<=n" 5);
       
   151 by (res_inst_tac [("j","i-1")] le_trans 6);
       
   152 by (res_inst_tac [("j","n-1")] le_trans 7);
       
   153 by (subgoal_tac "ia~=i" 5);
       
   154 by (subgoal_tac "ia<=n" 10);
       
   155 by (stac (suclemma RS sym) 11);
       
   156 by (assume_tac 13);
       
   157 by (rtac neq_le_imp_less 12);
       
   158 by (rtac diff_le_mono 8);
       
   159 by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [le_pred_eq])));
       
   160 qed "unique_xi_sol";
       
   161 
       
   162 Goalw [mhf_def] "[| 0<n; i<=n; j<=n; j~=i |] ==> (mf j) dvd (mhf mf n i)";
       
   163 by (case_tac "i=0" 1);
       
   164 by (case_tac "i=n" 2);
       
   165 by (ALLGOALS Asm_simp_tac);
       
   166 by (case_tac "j<i" 3);
       
   167 by (rtac zdvd_zmult2 3);
       
   168 by (rtac zdvd_zmult 4);
       
   169 by (ALLGOALS (rtac funprod_zdvd));
       
   170 by Auto_tac;
       
   171 by (stac suclemma 4);
       
   172 by (stac le_pred_eq 2);
       
   173 by (stac le_pred_eq 1);
       
   174 by (rtac neq_le_imp_less 2);
       
   175 by (rtac neq_le_imp_less 8);
       
   176 by (rtac pred_less_imp_le 6);
       
   177 by (rtac neq_le_imp_less 6);
       
   178 by Auto_tac;
       
   179 val lemma = result();
       
   180 
       
   181 Goalw [x_sol_def] "[| 0<n; i<=n |] \
       
   182 \     ==> (x_sol n kf bf mf) mod (mf i) = \
       
   183 \         (xilin_sol i n kf bf mf)*(mhf mf n i) mod (mf i)";
       
   184 by (stac funsum_mod 1);
       
   185 by (stac funsum_oneelem 1);
       
   186 by Auto_tac;
       
   187 by (stac (zdvd_iff_zmod_eq_0 RS sym) 1);
       
   188 by (rtac zdvd_zmult 1);
       
   189 by (rtac lemma 1);
       
   190 by Auto_tac;
       
   191 qed "x_sol_lin";
       
   192 
       
   193 
       
   194 (* Chinese *)
       
   195 
       
   196 Goal "EX! a. P a ==> P (@ a. P a)";
       
   197 by Auto_tac;
       
   198 by (stac select_equality 1);
       
   199 by Auto_tac;
       
   200 val delemma = result();
       
   201 
       
   202 Goal "[| 0<n; m_cond n mf; km_cond n kf mf |] \
       
   203 \     ==> (EX! x. #0 <= x & x < (funprod mf 0 n) & \
       
   204 \                 (lincong_sol n kf bf mf x))";
       
   205 by Safe_tac;
       
   206 by (res_inst_tac [("m","funprod mf 0 n")] zcong_zless_imp_eq 2);
       
   207 by (rtac zcong_funprod 6);
       
   208 by Auto_tac;
       
   209 by (res_inst_tac [("x","(x_sol n kf bf mf) mod (funprod mf 0 n)")] exI 1);
       
   210 by (rewtac lincong_sol_def);
       
   211 by Safe_tac;
       
   212 by (stac zcong_zmod 3);
       
   213 by (stac zmod_zmult_distrib 3);
       
   214 by (stac zmod_zdvd_zmod 3);
       
   215 by (stac x_sol_lin 5);
       
   216 by (stac (zmod_zmult_distrib RS sym) 7);
       
   217 by (stac (zcong_zmod RS sym) 7);
       
   218 by (subgoal_tac "#0<=(xilin_sol i n kf bf mf) & \
       
   219 \                (xilin_sol i n kf bf mf)<(mf i) & \
       
   220 \                [(kf i)*(mhf mf n i)*(xilin_sol i n kf bf mf) = bf i] \
       
   221 \                  (mod mf i)" 7);
       
   222 by (asm_full_simp_tac (simpset() addsimps zmult_ac) 7);
       
   223 by (rewtac xilin_sol_def);
       
   224 by (Asm_simp_tac 7);
       
   225 by (rtac delemma 7);
       
   226 by (rtac unique_xi_sol 7);
       
   227 by (rtac funprod_zdvd 4);
       
   228 by (rewtac m_cond_def);
       
   229 by (rtac (funprod_pos RS pos_mod_sign) 1);
       
   230 by (rtac (funprod_pos RS pos_mod_bound) 2);
       
   231 by Auto_tac;
       
   232 qed "chinese_remainder";