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