src/HOL/NumberTheory/Chinese.ML
changeset 9572 bfee45ac5d38
parent 9508 4d01dbf6ded7
child 9943 55c82decf3f4
equal deleted inserted replaced
9571:c869d1886a32 9572:bfee45ac5d38
   122 
   122 
   123 
   123 
   124 (* Chinese: Existence *)
   124 (* Chinese: Existence *)
   125 
   125 
   126 Goal "[| 0<n; i<n |] ==> Suc (i+(n-Suc(i))) = n";
   126 Goal "[| 0<n; i<n |] ==> Suc (i+(n-Suc(i))) = n";
   127 by (subgoal_tac "Suc (i+(n-1-i)) = n" 1);
   127 by (arith_tac 1);
   128 by (stac le_add_diff_inverse 2);
       
   129 by (stac le_pred_eq 2);
       
   130 by Auto_tac;
       
   131 val suclemma = result();
   128 val suclemma = result();
   132 
   129 
   133 Goal "[| 0<n; i<=n; m_cond n mf; km_cond n kf mf |] \
   130 Goal "[| 0<n; i<=n; m_cond n mf; km_cond n kf mf |] \
   134 \     ==> EX! x. #0<=x & x<(mf i) & \
   131 \     ==> EX! x. #0<=x & x<(mf i) & \
   135 \                [(kf i)*(mhf mf n i)*x = bf i] (mod mf i)";
   132 \                [(kf i)*(mhf mf n i)*x = bf i] (mod mf i)";
   191 qed "x_sol_lin";
   188 qed "x_sol_lin";
   192 
   189 
   193 
   190 
   194 (* Chinese *)
   191 (* Chinese *)
   195 
   192 
   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 |] \
   193 Goal "[| 0<n; m_cond n mf; km_cond n kf mf |] \
   203 \     ==> (EX! x. #0 <= x & x < (funprod mf 0 n) & \
   194 \     ==> (EX! x. #0 <= x & x < (funprod mf 0 n) & \
   204 \                 (lincong_sol n kf bf mf x))";
   195 \                 (lincong_sol n kf bf mf x))";
   205 by Safe_tac;
   196 by Safe_tac;
   206 by (res_inst_tac [("m","funprod mf 0 n")] zcong_zless_imp_eq 2);
   197 by (res_inst_tac [("m","funprod mf 0 n")] zcong_zless_imp_eq 2);
   220 \                [(kf i)*(mhf mf n i)*(xilin_sol i n kf bf mf) = bf i] \
   211 \                [(kf i)*(mhf mf n i)*(xilin_sol i n kf bf mf) = bf i] \
   221 \                  (mod mf i)" 7);
   212 \                  (mod mf i)" 7);
   222 by (asm_full_simp_tac (simpset() addsimps zmult_ac) 7);
   213 by (asm_full_simp_tac (simpset() addsimps zmult_ac) 7);
   223 by (rewtac xilin_sol_def);
   214 by (rewtac xilin_sol_def);
   224 by (Asm_simp_tac 7);
   215 by (Asm_simp_tac 7);
   225 by (rtac delemma 7);
   216 by (rtac (ex1_implies_ex RS ex_someI) 7);
   226 by (rtac unique_xi_sol 7);
   217 by (rtac unique_xi_sol 7);
   227 by (rtac funprod_zdvd 4);
   218 by (rtac funprod_zdvd 4);
   228 by (rewtac m_cond_def);
   219 by (rewtac m_cond_def);
   229 by (rtac (funprod_pos RS pos_mod_sign) 1);
   220 by (rtac (funprod_pos RS pos_mod_sign) 1);
   230 by (rtac (funprod_pos RS pos_mod_bound) 2);
   221 by (rtac (funprod_pos RS pos_mod_bound) 2);