Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
authorpaulson
Thu Aug 03 10:46:01 2000 +0200 (2000-08-03)
changeset 95084d01dbf6ded7
parent 9507 7903ca5fecf1
child 9509 0f3ee1f89ca8
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
src/HOL/NumberTheory/BijectionRel.ML
src/HOL/NumberTheory/BijectionRel.thy
src/HOL/NumberTheory/Chinese.ML
src/HOL/NumberTheory/Chinese.thy
src/HOL/NumberTheory/EulerFermat.ML
src/HOL/NumberTheory/EulerFermat.thy
src/HOL/NumberTheory/IntFact.ML
src/HOL/NumberTheory/IntFact.thy
src/HOL/NumberTheory/IntPrimes.ML
src/HOL/NumberTheory/IntPrimes.thy
src/HOL/NumberTheory/README
src/HOL/NumberTheory/ROOT.ML
src/HOL/NumberTheory/WilsonBij.ML
src/HOL/NumberTheory/WilsonBij.thy
src/HOL/NumberTheory/WilsonRuss.ML
src/HOL/NumberTheory/WilsonRuss.thy
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/NumberTheory/BijectionRel.ML	Thu Aug 03 10:46:01 2000 +0200
     1.3 @@ -0,0 +1,182 @@
     1.4 +(*  Title:	BijectionRel.ML
     1.5 +    ID:         $Id$
     1.6 +    Author:	Thomas M. Rasmussen
     1.7 +    Copyright	2000  University of Cambridge
     1.8 +
     1.9 +Inductive definitions of bijections between two different sets and
    1.10 +	between the same set. 
    1.11 +Theorem for relating the two definitions
    1.12 +*)
    1.13 +
    1.14 +
    1.15 +(***** bijR *****)
    1.16 +
    1.17 +Addsimps [bijR.empty];
    1.18 +
    1.19 +Goal "(A,B) : (bijR P) ==> finite A";
    1.20 +by (etac bijR.induct 1);
    1.21 +by Auto_tac;
    1.22 +qed "fin_bijRl";
    1.23 +
    1.24 +Goal "(A,B) : (bijR P) ==> finite B";
    1.25 +by (etac bijR.induct 1);
    1.26 +by Auto_tac;
    1.27 +qed "fin_bijRr";
    1.28 +
    1.29 +val major::subs::prems = 
    1.30 +Goal "[| finite F;  F <= A; P({}); \
    1.31 +\        !!F a. [| F <= A; a:A; a ~: F;  P(F) |] ==> P(insert a F) |] \
    1.32 +\     ==> P(F)";
    1.33 +by (rtac (subs RS rev_mp) 1);
    1.34 +by (rtac (major RS finite_induct) 1);
    1.35 +by (ALLGOALS (blast_tac (claset() addIs prems)));
    1.36 +val lemma_induct = result();
    1.37 +
    1.38 +Goalw [inj_on_def] 
    1.39 +      "[| A <= B; a ~: A ; a : B; inj_on f B |] ==> (f a) ~: f``A";
    1.40 +by Auto_tac;
    1.41 +val lemma = result();
    1.42 +
    1.43 +Goal "[| ALL a. a:A --> P a (f a); inj_on f A; finite A; F <= A |] \
    1.44 +\    ==> (F,f``F) : bijR P";
    1.45 +by (res_inst_tac [("F","F"),("A","A")] lemma_induct 1);
    1.46 +by (rtac finite_subset 1);
    1.47 +by Auto_tac;
    1.48 +by (rtac bijR.insert 1);
    1.49 +by (rtac lemma 3);
    1.50 +by Auto_tac;
    1.51 +val lemma = result();
    1.52 +
    1.53 +Goal "[| ALL a. a:A --> P a (f a); inj_on f A; finite A |] \
    1.54 +\    ==> (A,f``A) : bijR P";
    1.55 +by (rtac lemma 1);
    1.56 +by Auto_tac;
    1.57 +qed "inj_func_bijR";
    1.58 +
    1.59 +
    1.60 +(***** bijER *****)
    1.61 +
    1.62 +Addsimps [bijER.empty];
    1.63 +
    1.64 +Goal "A : bijER P ==> finite A";
    1.65 +by (etac bijER.induct 1);
    1.66 +by Auto_tac;
    1.67 +qed "fin_bijER";
    1.68 +
    1.69 +Goal "[| a ~: A; a ~: B; F <= insert a A; F <= insert a B; a : F |] \
    1.70 +\    ==> (EX C. F = insert a C & a ~: C & C <= A & C <= B)";
    1.71 +by (res_inst_tac [("x","F-{a}")] exI 1);
    1.72 +by Auto_tac;
    1.73 +val lemma1 = result();
    1.74 +
    1.75 +Goal "[| a ~= b; a ~: A; b ~: B; a : F; b : F; \
    1.76 +\        F <= insert a A; F <= insert b B |] \
    1.77 +\    ==> (EX C. F = insert a (insert b C) & a ~: C & b ~: C & \
    1.78 +\         C <= A & C <= B)";
    1.79 +by (res_inst_tac [("x","F-{a,b}")] exI 1);
    1.80 +by Auto_tac;
    1.81 +val lemma2 = result();
    1.82 +
    1.83 +Goalw [uniqP_def] "[| uniqP P; P a b; P c d |] ==> (a=c) = (b=d)";
    1.84 +by Auto_tac;
    1.85 +val lemma_uniq = result();
    1.86 +
    1.87 +Goalw [symP_def] "symP P ==> (P a b) = (P b a)";
    1.88 +by Auto_tac;
    1.89 +val lemma_sym = result();
    1.90 +
    1.91 +Goalw [bijP_def] 
    1.92 +      "[| uniqP P; b ~: C; P b b; bijP P (insert b C) |] ==> bijP P C";
    1.93 +by Auto_tac;
    1.94 +by (subgoal_tac "b~=a" 1);
    1.95 +by (Clarify_tac 2);
    1.96 +by (asm_full_simp_tac (simpset() addsimps [lemma_uniq]) 1);
    1.97 +by Auto_tac;
    1.98 +val lemma_in1 = result();
    1.99 +
   1.100 +Goalw [bijP_def] 
   1.101 +      "[| symP P; uniqP P; a ~: C; b ~: C; a ~= b; P a b; \
   1.102 +\         bijP P (insert a (insert b C)) |] ==> bijP P C";
   1.103 +by Auto_tac;
   1.104 +by (subgoal_tac "aa~=a" 1);
   1.105 +by (Clarify_tac 2);
   1.106 +by (subgoal_tac "aa~=b" 1);
   1.107 +by (Clarify_tac 2);
   1.108 +by (asm_full_simp_tac (simpset() addsimps [lemma_uniq]) 1);
   1.109 +by (subgoal_tac "ba~=a" 1);
   1.110 +by Auto_tac;
   1.111 +by (subgoal_tac "P a aa" 1);
   1.112 +by (asm_simp_tac (simpset() addsimps [lemma_sym]) 2);
   1.113 +by (subgoal_tac "b=aa" 1);
   1.114 +by (rtac iffD1 2);
   1.115 +by (res_inst_tac [("a","a"),("c","a"),("P","P")] lemma_uniq 2);
   1.116 +by Auto_tac;
   1.117 +val lemma_in2 = result();
   1.118 +
   1.119 +Goal "[| ALL a b. Q a & P a b --> R b; P a b; Q a |] ==> R b";
   1.120 +by Auto_tac;
   1.121 +val lemma = result();
   1.122 +
   1.123 +Goalw [bijP_def] "[| bijP P F; symP P; P a b |] ==> (a:F) = (b:F)";
   1.124 +by (rtac iffI 1);
   1.125 +by (ALLGOALS (etac lemma));
   1.126 +by (ALLGOALS Asm_simp_tac);
   1.127 +by (rtac iffD2 1);
   1.128 +by (res_inst_tac [("P","P")] lemma_sym 1);
   1.129 +by (ALLGOALS Asm_simp_tac);
   1.130 +val lemma_bij = result();
   1.131 +
   1.132 +Goal "[| (A,B) : bijR P; uniqP P; symP P |] \
   1.133 +\     ==> (ALL F. (bijP P F) & F<=A & F<=B --> F : bijER P)";
   1.134 +by (etac bijR.induct 1);
   1.135 +by (Simp_tac 1);
   1.136 +by (case_tac "a=b" 1);
   1.137 +by (Clarify_tac 1);
   1.138 +by (case_tac "b:F" 1);
   1.139 +by (rotate_tac ~1 2);
   1.140 +by (asm_full_simp_tac (simpset() addsimps [subset_insert]) 2);
   1.141 +by (cut_inst_tac [("F","F"),("a","b"),("A","A"),("B","B")] lemma1 1);
   1.142 +by (Clarify_tac 6);
   1.143 +by (rtac bijER.insert1 6);
   1.144 +by (ALLGOALS Asm_full_simp_tac);
   1.145 +by (subgoal_tac "bijP P C" 1);
   1.146 +by (Asm_full_simp_tac 1);
   1.147 +by (rtac lemma_in1 1);
   1.148 +by (ALLGOALS Asm_simp_tac);
   1.149 +by (Clarify_tac 1);
   1.150 +by (case_tac "a:F" 1);
   1.151 +by (ALLGOALS (case_tac "b:F"));
   1.152 +by (rotate_tac ~2 4);
   1.153 +by (asm_full_simp_tac (simpset() addsimps [subset_insert]) 4);
   1.154 +by (rotate_tac ~2 3);
   1.155 +by (asm_full_simp_tac (simpset() addsimps [subset_insert]) 3);
   1.156 +by (rotate_tac ~2 2);
   1.157 +by (asm_full_simp_tac (simpset() addsimps [subset_insert]) 2);
   1.158 +by (cut_inst_tac [("F","F"),("a","a"),("b","b"),("A","A"),("B","B")] 
   1.159 +                 lemma2 1);
   1.160 +by (ALLGOALS Asm_simp_tac);
   1.161 +by (Clarify_tac 1);
   1.162 +by (rtac bijER.insert2 1);
   1.163 +by (ALLGOALS Asm_simp_tac);
   1.164 +by (subgoal_tac "bijP P C" 1);
   1.165 +by (Asm_full_simp_tac 1);
   1.166 +by (rtac lemma_in2 1);
   1.167 +by (ALLGOALS Asm_simp_tac);
   1.168 +by (subgoal_tac "b:F" 1);
   1.169 +by (rtac iffD1 2);
   1.170 +by (res_inst_tac [("a","a"),("F","F"),("P","P")] lemma_bij 2);
   1.171 +by (ALLGOALS Asm_simp_tac);
   1.172 +by (subgoal_tac "a:F" 2);
   1.173 +by (rtac iffD2 3);
   1.174 +by (res_inst_tac [("b","b"),("F","F"),("P","P")] lemma_bij 3);
   1.175 +by Auto_tac;
   1.176 +val lemma_bijRER = result();
   1.177 +
   1.178 +Goal "[| (A,A) : bijR P; (bijP P A); uniqP P; symP P |] ==> A : bijER P";
   1.179 +by (cut_inst_tac [("A","A"),("B","A"),("P","P")] lemma_bijRER 1);
   1.180 +by Auto_tac;
   1.181 +qed "bijR_bijER";
   1.182 +
   1.183 +
   1.184 +
   1.185 +
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOL/NumberTheory/BijectionRel.thy	Thu Aug 03 10:46:01 2000 +0200
     2.3 @@ -0,0 +1,46 @@
     2.4 +(*  Title:	BijectionRel.thy
     2.5 +    ID:         $Id$
     2.6 +    Author:	Thomas M. Rasmussen
     2.7 +    Copyright	2000  University of Cambridge
     2.8 +*)
     2.9 +
    2.10 +BijectionRel = Main +
    2.11 +
    2.12 +consts
    2.13 +  bijR :: "(['a, 'b] => bool) => ('a set * 'b set) set"
    2.14 +
    2.15 +inductive "bijR P"
    2.16 +intrs
    2.17 +  empty  "({},{}) : bijR P"
    2.18 +  insert "[| P a b; a ~: A; b ~: B; (A,B) : bijR P |] \ 
    2.19 +\        ==> (insert a A, insert b B) : bijR P" 
    2.20 +
    2.21 +(* Add extra condition to insert: ALL b:B. ~(P a b) (and similar for A) *) 
    2.22 +
    2.23 +consts
    2.24 +  bijP :: "(['a, 'a] => bool) => 'a set => bool"
    2.25 +
    2.26 +defs
    2.27 +  bijP_def "bijP P F == (ALL a b. a:F & P a b --> b:F)" 
    2.28 +
    2.29 +consts
    2.30 +  uniqP :: "(['a, 'a] => bool) => bool"
    2.31 +  symP :: "(['a, 'a] => bool) => bool"
    2.32 +  
    2.33 +defs
    2.34 +  uniqP_def "uniqP P == (ALL a b c d. P a b & P c d --> (a=c) = (b=d))" 
    2.35 +  symP_def  "symP P  == (ALL a b. (P a b) = (P b a))" 
    2.36 +
    2.37 +consts
    2.38 +  bijER :: "(['a, 'a] => bool) => 'a set set"
    2.39 +
    2.40 +inductive "bijER P"
    2.41 +intrs
    2.42 +  empty   "{} : bijER P"
    2.43 +  insert1 "[| P a a; a ~: A; A : bijER P |] \ 
    2.44 +\         ==> (insert a A) : bijER P" 
    2.45 +  insert2 "[| P a b; a ~= b; a ~: A; b ~: A; A : bijER P |] \ 
    2.46 +\         ==> (insert a (insert b A)) : bijER P" 
    2.47 +
    2.48 +end
    2.49 +
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOL/NumberTheory/Chinese.ML	Thu Aug 03 10:46:01 2000 +0200
     3.3 @@ -0,0 +1,232 @@
     3.4 +(*  Title:	Chinese.ML
     3.5 +    ID:         $Id$
     3.6 +    Author:	Thomas M. Rasmussen
     3.7 +    Copyright	2000  University of Cambridge
     3.8 +
     3.9 +The Chinese Remainder Theorem for an arbitrary finite number of equations. 
    3.10 +(The one-equation case is included in 'IntPrimes')
    3.11 +
    3.12 +Uses functions for indexing. Maybe 'funprod' and 'funsum'
    3.13 +should be based on general 'fold' on indices?
    3.14 +*)
    3.15 +
    3.16 +
    3.17 +(*** extra nat theorems ***)
    3.18 +
    3.19 +Goal "[| k <= i; i <= k |] ==> i = (k::nat)";
    3.20 +by (rtac diffs0_imp_equal 1);
    3.21 +by (ALLGOALS (stac diff_is_0_eq)); 
    3.22 +by Auto_tac;
    3.23 +qed "le_le_imp_eq";
    3.24 +
    3.25 +Goal "m~=n --> m<=n --> m<(n::nat)";
    3.26 +by (induct_tac "n" 1);
    3.27 +by Auto_tac;
    3.28 +by (subgoal_tac "m = Suc n" 1);
    3.29 +by (rtac le_le_imp_eq 2);
    3.30 +by Auto_tac;
    3.31 +qed_spec_mp "neq_le_imp_less";
    3.32 +
    3.33 +
    3.34 +(*** funprod and funsum ***)
    3.35 +
    3.36 +Goal "(ALL i. i <= n --> #0 < mf i) --> #0 < funprod mf 0 n";
    3.37 +by (induct_tac "n" 1);
    3.38 +by Auto_tac;
    3.39 +by (asm_full_simp_tac (simpset() addsimps [int_0_less_mult_iff]) 1);
    3.40 +qed_spec_mp "funprod_pos";
    3.41 +
    3.42 +Goal "(ALL i. k<=i & i<=(k+l) --> zgcd (mf i, mf m) = #1) --> \
    3.43 +\      #0 < mf m --> zgcd (funprod mf k l, mf m) = #1";
    3.44 +by (induct_tac "l" 1);
    3.45 +by (ALLGOALS Simp_tac);
    3.46 +by (REPEAT (rtac impI 1));
    3.47 +by (stac zgcd_zmult_cancel 1);
    3.48 +by Auto_tac;
    3.49 +qed_spec_mp "funprod_zgcd";
    3.50 +
    3.51 +Goal "k<=i --> i<=(k+l) --> (mf i) dvd (funprod mf k l)";     
    3.52 +by (induct_tac "l" 1);
    3.53 +by Auto_tac;
    3.54 +by (rtac zdvd_zmult2 2);
    3.55 +by (rtac zdvd_zmult 3);
    3.56 +by (subgoal_tac "i=k" 1);
    3.57 +by (subgoal_tac "i=Suc (k + n)" 3);
    3.58 +by (ALLGOALS Asm_simp_tac);
    3.59 +qed_spec_mp "funprod_zdvd";
    3.60 +
    3.61 +Goal "(funsum f k l) mod m = (funsum (%i. (f i) mod m) k l) mod m";
    3.62 +by (induct_tac "l" 1);
    3.63 +by Auto_tac;
    3.64 +by (rtac trans 1);
    3.65 +by (rtac zmod_zadd1_eq 1);
    3.66 +by (Asm_simp_tac 1);
    3.67 +by (rtac (zmod_zadd_right_eq RS sym) 1);
    3.68 +qed "funsum_mod";
    3.69 +
    3.70 +Goal "(ALL i. k<=i & i<=(k+l) --> (f i) = #0) --> (funsum f k l) = #0";
    3.71 +by (induct_tac "l" 1);
    3.72 +by Auto_tac;
    3.73 +qed_spec_mp "funsum_zero";
    3.74 +
    3.75 +Goal "k<=j --> j<=(k+l) --> \
    3.76 +\     (ALL i. k<=i & i<=(k+l) & i~=j --> (f i) = #0) --> \
    3.77 +\     (funsum f k l) = (f j)";
    3.78 +by (induct_tac "l" 1);
    3.79 +by (ALLGOALS Simp_tac); 
    3.80 +by (ALLGOALS (REPEAT o (rtac impI)));
    3.81 +by (case_tac "Suc (k+n) = j" 2);
    3.82 +by (subgoal_tac "funsum f k n = #0" 2);
    3.83 +by (rtac funsum_zero 3);
    3.84 +by (subgoal_tac "f (Suc (k+n)) = #0" 4);
    3.85 +by (subgoal_tac "k=j" 1);
    3.86 +by (Clarify_tac 4);
    3.87 +by (subgoal_tac "j<=k+n" 5);
    3.88 +by (subgoal_tac "j<Suc (k+n)" 6);
    3.89 +by (rtac neq_le_imp_less 7);
    3.90 +by (ALLGOALS Asm_simp_tac); 
    3.91 +by Auto_tac;
    3.92 +qed_spec_mp "funsum_oneelem";
    3.93 +
    3.94 +
    3.95 +(*** Chinese: Uniqueness ***)
    3.96 +
    3.97 +Goalw [m_cond_def,km_cond_def,lincong_sol_def]
    3.98 +      "[| m_cond n mf; km_cond n kf mf; \
    3.99 +\         lincong_sol n kf bf mf x; lincong_sol n kf bf mf y |] \
   3.100 +\     ==>  [x=y] (mod mf n)";
   3.101 +by (rtac iffD1 1);
   3.102 +by (res_inst_tac [("k","kf n")] zcong_cancel2 1);
   3.103 +by (res_inst_tac [("b","bf n")] zcong_trans 3);
   3.104 +by (stac zcong_sym 4);
   3.105 +by (rtac zless_imp_zle 1);
   3.106 +by (ALLGOALS Asm_simp_tac);
   3.107 +val lemma = result();
   3.108 +
   3.109 +Goal "m_cond n mf --> km_cond n kf mf --> \
   3.110 +\     lincong_sol n kf bf mf x --> lincong_sol n kf bf mf y --> \
   3.111 +\     [x=y] (mod funprod mf 0 n)";
   3.112 +by (induct_tac "n" 1);
   3.113 +by (ALLGOALS Simp_tac);
   3.114 +by (blast_tac (claset() addIs [lemma]) 1);
   3.115 +by (REPEAT (rtac impI 1));
   3.116 +by (rtac zcong_zgcd_zmult_zmod 1);
   3.117 +by (blast_tac (claset() addIs [lemma]) 3);
   3.118 +by (stac zgcd_commute 4);
   3.119 +by (rtac funprod_zgcd 6);
   3.120 +by (rtac funprod_pos 5);
   3.121 +by (rtac funprod_pos 2);
   3.122 +by (rewrite_goals_tac [m_cond_def,km_cond_def,lincong_sol_def]);
   3.123 +by Auto_tac;
   3.124 +qed_spec_mp "zcong_funprod";
   3.125 +
   3.126 +
   3.127 +(* Chinese: Existence *)
   3.128 +
   3.129 +Goal "[| 0<n; i<n |] ==> Suc (i+(n-Suc(i))) = n";
   3.130 +by (subgoal_tac "Suc (i+(n-1-i)) = n" 1);
   3.131 +by (stac le_add_diff_inverse 2);
   3.132 +by (stac le_pred_eq 2);
   3.133 +by Auto_tac;
   3.134 +val suclemma = result();
   3.135 +
   3.136 +Goal "[| 0<n; i<=n; m_cond n mf; km_cond n kf mf |] \
   3.137 +\     ==> EX! x. #0<=x & x<(mf i) & \
   3.138 +\                [(kf i)*(mhf mf n i)*x = bf i] (mod mf i)";
   3.139 +by (rtac zcong_lineq_unique 1);
   3.140 +by (stac zgcd_zmult_cancel 2);
   3.141 +by (rewrite_goals_tac [m_cond_def,km_cond_def,mhf_def]);
   3.142 +by (case_tac "i=0" 4);
   3.143 +by (case_tac "i=n" 5);
   3.144 +by (ALLGOALS Asm_simp_tac);
   3.145 +by (stac zgcd_zmult_cancel 3);
   3.146 +by (Asm_simp_tac 3);
   3.147 +by (ALLGOALS (rtac funprod_zgcd));
   3.148 +by Safe_tac;
   3.149 +by (ALLGOALS Asm_full_simp_tac);
   3.150 +by (subgoal_tac "i<=n" 1);
   3.151 +by (res_inst_tac [("j","n-1")] le_trans 2);
   3.152 +by (subgoal_tac "i~=n" 1);
   3.153 +by (subgoal_tac "ia<=n" 5);
   3.154 +by (res_inst_tac [("j","i-1")] le_trans 6);
   3.155 +by (res_inst_tac [("j","n-1")] le_trans 7);
   3.156 +by (subgoal_tac "ia~=i" 5);
   3.157 +by (subgoal_tac "ia<=n" 10);
   3.158 +by (stac (suclemma RS sym) 11);
   3.159 +by (assume_tac 13);
   3.160 +by (rtac neq_le_imp_less 12);
   3.161 +by (rtac diff_le_mono 8);
   3.162 +by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [le_pred_eq])));
   3.163 +qed "unique_xi_sol";
   3.164 +
   3.165 +Goalw [mhf_def] "[| 0<n; i<=n; j<=n; j~=i |] ==> (mf j) dvd (mhf mf n i)";
   3.166 +by (case_tac "i=0" 1);
   3.167 +by (case_tac "i=n" 2);
   3.168 +by (ALLGOALS Asm_simp_tac);
   3.169 +by (case_tac "j<i" 3);
   3.170 +by (rtac zdvd_zmult2 3);
   3.171 +by (rtac zdvd_zmult 4);
   3.172 +by (ALLGOALS (rtac funprod_zdvd));
   3.173 +by Auto_tac;
   3.174 +by (stac suclemma 4);
   3.175 +by (stac le_pred_eq 2);
   3.176 +by (stac le_pred_eq 1);
   3.177 +by (rtac neq_le_imp_less 2);
   3.178 +by (rtac neq_le_imp_less 8);
   3.179 +by (rtac pred_less_imp_le 6);
   3.180 +by (rtac neq_le_imp_less 6);
   3.181 +by Auto_tac;
   3.182 +val lemma = result();
   3.183 +
   3.184 +Goalw [x_sol_def] "[| 0<n; i<=n |] \
   3.185 +\     ==> (x_sol n kf bf mf) mod (mf i) = \
   3.186 +\         (xilin_sol i n kf bf mf)*(mhf mf n i) mod (mf i)";
   3.187 +by (stac funsum_mod 1);
   3.188 +by (stac funsum_oneelem 1);
   3.189 +by Auto_tac;
   3.190 +by (stac (zdvd_iff_zmod_eq_0 RS sym) 1);
   3.191 +by (rtac zdvd_zmult 1);
   3.192 +by (rtac lemma 1);
   3.193 +by Auto_tac;
   3.194 +qed "x_sol_lin";
   3.195 +
   3.196 +
   3.197 +(* Chinese *)
   3.198 +
   3.199 +Goal "EX! a. P a ==> P (@ a. P a)";
   3.200 +by Auto_tac;
   3.201 +by (stac select_equality 1);
   3.202 +by Auto_tac;
   3.203 +val delemma = result();
   3.204 +
   3.205 +Goal "[| 0<n; m_cond n mf; km_cond n kf mf |] \
   3.206 +\     ==> (EX! x. #0 <= x & x < (funprod mf 0 n) & \
   3.207 +\                 (lincong_sol n kf bf mf x))";
   3.208 +by Safe_tac;
   3.209 +by (res_inst_tac [("m","funprod mf 0 n")] zcong_zless_imp_eq 2);
   3.210 +by (rtac zcong_funprod 6);
   3.211 +by Auto_tac;
   3.212 +by (res_inst_tac [("x","(x_sol n kf bf mf) mod (funprod mf 0 n)")] exI 1);
   3.213 +by (rewtac lincong_sol_def);
   3.214 +by Safe_tac;
   3.215 +by (stac zcong_zmod 3);
   3.216 +by (stac zmod_zmult_distrib 3);
   3.217 +by (stac zmod_zdvd_zmod 3);
   3.218 +by (stac x_sol_lin 5);
   3.219 +by (stac (zmod_zmult_distrib RS sym) 7);
   3.220 +by (stac (zcong_zmod RS sym) 7);
   3.221 +by (subgoal_tac "#0<=(xilin_sol i n kf bf mf) & \
   3.222 +\                (xilin_sol i n kf bf mf)<(mf i) & \
   3.223 +\                [(kf i)*(mhf mf n i)*(xilin_sol i n kf bf mf) = bf i] \
   3.224 +\                  (mod mf i)" 7);
   3.225 +by (asm_full_simp_tac (simpset() addsimps zmult_ac) 7);
   3.226 +by (rewtac xilin_sol_def);
   3.227 +by (Asm_simp_tac 7);
   3.228 +by (rtac delemma 7);
   3.229 +by (rtac unique_xi_sol 7);
   3.230 +by (rtac funprod_zdvd 4);
   3.231 +by (rewtac m_cond_def);
   3.232 +by (rtac (funprod_pos RS pos_mod_sign) 1);
   3.233 +by (rtac (funprod_pos RS pos_mod_bound) 2);
   3.234 +by Auto_tac;
   3.235 +qed "chinese_remainder";
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/HOL/NumberTheory/Chinese.thy	Thu Aug 03 10:46:01 2000 +0200
     4.3 @@ -0,0 +1,55 @@
     4.4 +(*  Title:	Chinese.thy
     4.5 +    ID:         $Id$
     4.6 +    Author:	Thomas M. Rasmussen
     4.7 +    Copyright	2000  University of Cambridge
     4.8 +*)
     4.9 +
    4.10 +Chinese = IntPrimes +
    4.11 +
    4.12 +consts
    4.13 +  funprod     :: (nat => int) => nat => nat => int
    4.14 +  funsum      :: (nat => int) => nat => nat => int
    4.15 +
    4.16 +primrec
    4.17 +  "funprod f i 0        = f i"
    4.18 +  "funprod f i (Suc n)  = (f (Suc (i+n)))*(funprod f i n)" 
    4.19 +
    4.20 +primrec
    4.21 +  "funsum f i 0         = f i"
    4.22 +  "funsum f i (Suc n)   = (f (Suc (i+n)))+(funsum f i n)" 
    4.23 +
    4.24 +
    4.25 +consts
    4.26 +  m_cond      :: [nat,nat => int] => bool
    4.27 +  km_cond     :: [nat,nat => int,nat => int] => bool
    4.28 +  lincong_sol :: [nat,nat => int,nat => int,nat => int,int] => bool
    4.29 +
    4.30 +  mhf         :: (nat => int) => nat => nat => int
    4.31 +  xilin_sol   :: [nat,nat,nat => int,nat => int,nat => int] => int
    4.32 +  x_sol       :: [nat,nat => int,nat => int,nat => int] => int  
    4.33 +
    4.34 +defs
    4.35 +  m_cond_def   "m_cond n mf == 
    4.36 +                   (ALL i. i<=n --> #0 < mf i) & 
    4.37 +                   (ALL i j. i<=n & j<=n & i ~= j --> zgcd(mf i,mf j) = #1)"
    4.38 +
    4.39 +  km_cond_def  "km_cond n kf mf == (ALL i. i<=n --> zgcd(kf i,mf i) = #1)"
    4.40 +
    4.41 +  lincong_sol_def "lincong_sol n kf bf mf x == 
    4.42 +                   (ALL i. i<=n --> zcong ((kf i)*x) (bf i) (mf i))"
    4.43 +
    4.44 +  mhf_def  "mhf mf n i == (if i=0 then (funprod mf 1 (n-1)) 
    4.45 +                           else (if i=n then (funprod mf 0 (n-1))
    4.46 +                           else ((funprod mf 0 (i-1)) * 
    4.47 +                                 (funprod mf (i+1) (n-1-i)))))"
    4.48 +
    4.49 +  xilin_sol_def "xilin_sol i n kf bf mf ==
    4.50 +                  (if 0<n & i<=n & m_cond n mf & km_cond n kf mf then
    4.51 +                    (@ x. #0<=x & x<(mf i) & 
    4.52 +                          zcong ((kf i)*(mhf mf n i)*x) (bf i) (mf i))
    4.53 +                    else #0)"
    4.54 +
    4.55 +  x_sol_def "x_sol n kf bf mf ==
    4.56 +              (funsum (%i. (xilin_sol i n kf bf mf)*(mhf mf n i)) 0 n)"
    4.57 +
    4.58 +end
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/src/HOL/NumberTheory/EulerFermat.ML	Thu Aug 03 10:46:01 2000 +0200
     5.3 @@ -0,0 +1,308 @@
     5.4 +(*  Title:	EulerFermat.ML
     5.5 +    ID:         $Id$
     5.6 +    Author:	Thomas M. Rasmussen
     5.7 +    Copyright	2000  University of Cambridge
     5.8 +
     5.9 +Fermat's Little Theorem extended to Euler's Totient function.
    5.10 +More abstract approach than Boyer-Moore (which seems necessary
    5.11 +to achieve the extended version)
    5.12 +*)
    5.13 +
    5.14 +
    5.15 +(***  norRRset  ***)
    5.16 +
    5.17 +Addsimps [RsetR.empty];
    5.18 +
    5.19 +val [BnorRset_eq] = BnorRset.simps;
    5.20 +Delsimps BnorRset.simps;
    5.21 +
    5.22 +val [prem1,prem2] =
    5.23 +Goal "[| !! a m. P {} a m; \
    5.24 +\       (!!a m. [| #0 < (a::int); P (BnorRset(a-#1,m::int)) (a-#1) m |] \
    5.25 +\               ==> P (BnorRset(a,m)) a m) |] \
    5.26 +\    ==> P (BnorRset(u,v)) u v";
    5.27 +by (rtac BnorRset.induct 1);
    5.28 +by Safe_tac;
    5.29 +by (case_tac "#0<a" 2);
    5.30 +by (rtac prem2 2);
    5.31 +by (ALLGOALS Asm_simp_tac);
    5.32 +by (ALLGOALS (asm_simp_tac (simpset() addsimps [BnorRset_eq,prem1])));
    5.33 +qed "BnorRset_induct";
    5.34 +
    5.35 +Goal "b:BnorRset(a,m) --> b<=a";
    5.36 +by (res_inst_tac [("u","a"),("v","m")] BnorRset_induct 1);
    5.37 +by (stac BnorRset_eq 2);
    5.38 +by (rewtac Let_def);
    5.39 +by Auto_tac;
    5.40 +qed_spec_mp "Bnor_mem_zle"; 
    5.41 +
    5.42 +Goal "a<b ==> b~:BnorRset(a,m)";
    5.43 +by (res_inst_tac [("Pa","b<=a")] swap 1);
    5.44 +by (rtac Bnor_mem_zle 2);
    5.45 +by Auto_tac;
    5.46 +qed "Bnor_mem_zle_swap";
    5.47 +
    5.48 +Goal "b:BnorRset(a,m) --> #0<b";
    5.49 +by (res_inst_tac [("u","a"),("v","m")] BnorRset_induct 1);
    5.50 +by (stac BnorRset_eq 2);
    5.51 +by (rewtac Let_def);
    5.52 +by Auto_tac;
    5.53 +qed_spec_mp "Bnor_mem_zg"; 
    5.54 +
    5.55 +Goal "zgcd(b,m) = #1 --> #0<b --> b<=a --> b:BnorRset(a,m)";
    5.56 +by (res_inst_tac [("u","a"),("v","m")] BnorRset.induct 1);
    5.57 +by Auto_tac;
    5.58 +by (case_tac "a=b" 1);
    5.59 +by (asm_full_simp_tac (simpset() addsimps [zle_neq_implies_zless]) 2);
    5.60 +by (Asm_simp_tac 1);
    5.61 +by (ALLGOALS (stac BnorRset_eq));
    5.62 +by (rewtac Let_def);
    5.63 +by Auto_tac;
    5.64 +qed_spec_mp "Bnor_mem_if";
    5.65 +
    5.66 +Goal "a<m --> BnorRset (a,m) : RsetR m";
    5.67 +by (res_inst_tac [("u","a"),("v","m")] BnorRset_induct 1);
    5.68 +by (Simp_tac 1);
    5.69 +by (stac BnorRset_eq 1);
    5.70 +by (rewtac Let_def);
    5.71 +by Auto_tac;
    5.72 +by (rtac RsetR.insert 1);
    5.73 +by (rtac allI 3);
    5.74 +by (rtac impI 3);
    5.75 +by (rtac zcong_not 3);
    5.76 +by (subgoal_tac "a' <= a-#1" 6);
    5.77 +by (rtac Bnor_mem_zle 7);
    5.78 +by (rtac Bnor_mem_zg 5);
    5.79 +by Auto_tac;
    5.80 +qed_spec_mp "Bnor_in_RsetR";
    5.81 +
    5.82 +Goal "finite (BnorRset (a,m))";
    5.83 +by (res_inst_tac [("u","a"),("v","m")] BnorRset_induct 1);
    5.84 +by (stac BnorRset_eq 2);
    5.85 +by (rewtac Let_def);
    5.86 +by Auto_tac;
    5.87 +qed "Bnor_fin";
    5.88 +
    5.89 +Goal "a <= b - #1 ==> a < (b::int)";
    5.90 +by Auto_tac;
    5.91 +val lemma = result();
    5.92 +
    5.93 +Goalw [norRRset_def]
    5.94 +      "[| #1<m; zgcd(a,m) = #1 |] ==> (EX! b. [a = b](mod m) & b:(norRRset m))";
    5.95 +by (cut_inst_tac [("a","a"),("m","m")] zcong_zless_unique 1);
    5.96 +by Auto_tac;
    5.97 +by (res_inst_tac [("m","m")] zcong_zless_imp_eq 2);
    5.98 +by (auto_tac (claset() addIs [Bnor_mem_zle,Bnor_mem_zg,zcong_trans,
    5.99 +                              zless_imp_zle,lemma],
   5.100 +              simpset() addsimps [zcong_sym]));
   5.101 +by (res_inst_tac [("x","b")] exI 1);
   5.102 +by Safe_tac;
   5.103 +by (rtac Bnor_mem_if 1);
   5.104 +by (case_tac "b=#0" 2);
   5.105 +by (auto_tac (claset() addIs [zle_neq_implies_zless], simpset()));
   5.106 +by (SELECT_GOAL (rewtac zcong_def) 2);
   5.107 +by (subgoal_tac "zgcd(a,m) = m" 2);
   5.108 +by (stac (zdvd_iff_zgcd RS sym) 3);
   5.109 +by (rtac zgcd_zcong_zgcd 1);
   5.110 +by (ALLGOALS (asm_full_simp_tac (simpset() 
   5.111 +      addsimps [zdvd_zminus_iff,zcong_sym])));
   5.112 +qed "norR_mem_unique";
   5.113 +
   5.114 +
   5.115 +(***  noXRRset  ***)
   5.116 +
   5.117 +Goalw [is_RRset_def] 
   5.118 +      "[| #0<m; is_RRset A m; #0<m |] ==> a:A --> zgcd (a,m) = #1";
   5.119 +by (rtac RsetR.induct 1);
   5.120 +by Auto_tac;
   5.121 +qed_spec_mp "RRset_gcd";
   5.122 +
   5.123 +Goal "[|  A : RsetR m; #0<m; zgcd (x, m) = #1 |] ==> (%a. a*x)``A : RsetR m";
   5.124 +by (etac RsetR.induct 1);
   5.125 +by (ALLGOALS Simp_tac);
   5.126 +by (rtac RsetR.insert 1);
   5.127 +by Auto_tac;
   5.128 +by (asm_full_simp_tac (simpset() addsimps [zcong_cancel]) 2);
   5.129 +by (blast_tac (claset() addIs [zgcd_zgcd_zmult]) 1);
   5.130 +qed "RsetR_zmult_mono";
   5.131 +
   5.132 +Goalw [norRRset_def,noXRRset_def]
   5.133 +      "[| #0<m; zgcd(x,m) = #1 |] \
   5.134 +\     ==> card (noXRRset m x) = card (norRRset m)";
   5.135 +by (rtac card_image 1);
   5.136 +by (rewtac inj_on_def);
   5.137 +by (auto_tac (claset(),simpset() addsimps [Bnor_fin]));
   5.138 +by (case_tac "x=#0" 1);
   5.139 +by (asm_full_simp_tac (simpset() addsimps [BnorRset_eq]) 1);
   5.140 +by (stac (zmult_cancel2 RS sym) 1);
   5.141 +by (ALLGOALS Asm_simp_tac);
   5.142 +qed "card_nor_eq_noX";
   5.143 +
   5.144 +Goalw [is_RRset_def,phi_def]
   5.145 +      "[| #0<m; zgcd(x,m) = #1 |] ==> is_RRset (noXRRset m x) m";
   5.146 +by (auto_tac (claset(),simpset() addsimps [card_nor_eq_noX]));
   5.147 +by (rewrite_goals_tac [noXRRset_def,norRRset_def]);
   5.148 +by (rtac RsetR_zmult_mono 1);
   5.149 +by (rtac Bnor_in_RsetR 1);
   5.150 +by (ALLGOALS Asm_simp_tac);
   5.151 +qed "noX_is_RRset";
   5.152 +
   5.153 +Goal "EX! a. P a ==> P (@ a. P a)";
   5.154 +by Auto_tac;
   5.155 +by (stac select_equality 1);
   5.156 +by Auto_tac;
   5.157 +val lemma = result();
   5.158 +
   5.159 +Goal "[| #1<m; is_RRset A m; a:A |] \
   5.160 +\    ==> zcong a (@ b. [a = b](mod m) & b : norRRset m) m & \
   5.161 +\        (@ b. [a = b](mod m) & b : norRRset m) : norRRset m";
   5.162 +by (rtac lemma 1);
   5.163 +by (rtac norR_mem_unique 1);
   5.164 +by (rtac RRset_gcd 2);
   5.165 +by (ALLGOALS Asm_simp_tac);
   5.166 +val lemma_some = result();
   5.167 +
   5.168 +Goalw [RRset2norRR_def]
   5.169 +      "[| #1<m; is_RRset A m; a:A |] \
   5.170 +\     ==> zcong a (RRset2norRR A m a) m & \
   5.171 +\         (RRset2norRR A m a):(norRRset m)";
   5.172 +by (Asm_simp_tac 1);
   5.173 +by (rtac lemma_some 1);
   5.174 +by (ALLGOALS Asm_simp_tac);
   5.175 +qed "RRset2norRR_correct";
   5.176 +
   5.177 +bind_thm ("RRset2norRR_correct1", RRset2norRR_correct RS conjunct1);
   5.178 +bind_thm ("RRset2norRR_correct2", RRset2norRR_correct RS conjunct2);
   5.179 +
   5.180 +Goal "A : (RsetR m) ==> finite A";
   5.181 +by (etac RsetR.induct 1);
   5.182 +by Auto_tac;
   5.183 +qed "RsetR_fin";
   5.184 +
   5.185 +Goalw [is_RRset_def] 
   5.186 +      "[| #1<m; is_RRset A m; [a = b](mod m) |] ==> a:A --> b:A --> a = b";
   5.187 +by (rtac RsetR.induct 1);
   5.188 +by (auto_tac (claset(), simpset() addsimps [zcong_sym]));
   5.189 +qed_spec_mp "RRset_zcong_eq";
   5.190 +
   5.191 +Goal "[| P (@ a. P a); Q (@ a. Q a); (@ a. P a) = (@ a. Q a) |] \
   5.192 +\    ==> (EX a. P a & Q a)";
   5.193 +by Auto_tac;
   5.194 +val lemma = result();
   5.195 +
   5.196 +Goalw [RRset2norRR_def,inj_on_def]
   5.197 +      "[| #1<m; is_RRset A m |] ==> inj_on (RRset2norRR A m) A";
   5.198 +by Auto_tac;
   5.199 +by (subgoal_tac "(EX b. ([x = b](mod m) & b : norRRset m) & \
   5.200 +\                       ([y = b](mod m) & b : norRRset m))" 1);
   5.201 +by (rtac lemma 2);
   5.202 +by (rtac lemma_some 3);
   5.203 +by (rtac lemma_some 2);
   5.204 +by (rtac RRset_zcong_eq 1);
   5.205 +by Auto_tac;
   5.206 +by (res_inst_tac [("b","b")] zcong_trans 1);
   5.207 +by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [zcong_sym])));
   5.208 +qed "RRset2norRR_inj";
   5.209 +
   5.210 +Goal "[| #1<m; is_RRset A m |] ==> (RRset2norRR A m)``A = (norRRset m)";
   5.211 +by (rtac card_seteq 1);
   5.212 +by (stac card_image 3);
   5.213 +by (rtac RRset2norRR_inj 4);
   5.214 +by Auto_tac;
   5.215 +by (rtac RRset2norRR_correct2 2);
   5.216 +by Auto_tac;
   5.217 +by (rewrite_goals_tac [is_RRset_def,phi_def,norRRset_def]);
   5.218 +by (auto_tac (claset(),simpset() addsimps [RsetR_fin,Bnor_fin]));
   5.219 +qed "RRset2norRR_eq_norR";
   5.220 +
   5.221 +Goalw [inj_on_def] "[| a ~: A ; inj f |] ==> (f a) ~: f``A";
   5.222 +by Auto_tac;
   5.223 +val lemma = result();
   5.224 +
   5.225 +Goal "x~=#0 ==> a<m --> setprod ((%a. a*x) `` BnorRset(a,m)) = \
   5.226 +\     setprod (BnorRset(a,m)) * x^card(BnorRset(a,m))";
   5.227 +by (res_inst_tac [("u","a"),("v","m")] BnorRset_induct 1);
   5.228 +by (stac BnorRset_eq 2);
   5.229 +by (rewtac Let_def);
   5.230 +by Auto_tac;
   5.231 +by (asm_simp_tac (simpset() addsimps [Bnor_fin,Bnor_mem_zle_swap]) 1);
   5.232 +by (stac setprod_insert 1);
   5.233 +by (rtac lemma 2);
   5.234 +by (rewtac inj_on_def);
   5.235 +by (ALLGOALS (asm_full_simp_tac (simpset() 
   5.236 +      addsimps zmult_ac@[Bnor_fin,finite_imageI,Bnor_mem_zle_swap])));
   5.237 +qed_spec_mp "Bnor_prod_power";
   5.238 +
   5.239 +
   5.240 +(***  Fermat  ***)
   5.241 +
   5.242 +Goalw [zcongm_def] 
   5.243 +      "(A,B) : bijR (zcongm m) ==> [setprod A = setprod B](mod m)";
   5.244 +by (etac bijR.induct 1);
   5.245 +by (subgoal_tac "a~:A & b~:B & finite A & finite B" 2); 
   5.246 +by (auto_tac (claset() addIs [fin_bijRl,fin_bijRr,zcong_zmult],
   5.247 +              simpset()));
   5.248 +qed "bijzcong_zcong_prod";
   5.249 +
   5.250 +Goalw [norRRset_def,phi_def]
   5.251 +      "#0<m --> a<m --> zgcd (setprod (BnorRset (a,m)),m) = #1";
   5.252 +by (res_inst_tac [("u","a"),("v","m")] BnorRset_induct 1);
   5.253 +by (stac BnorRset_eq 2);
   5.254 +by (rewtac Let_def);
   5.255 +by Auto_tac;
   5.256 +by (asm_simp_tac (simpset() addsimps [Bnor_fin,Bnor_mem_zle_swap]) 1);
   5.257 +by (blast_tac (claset() addIs [zgcd_zgcd_zmult]) 1);
   5.258 +qed_spec_mp "Bnor_prod_zgcd";
   5.259 +
   5.260 +Goalw [norRRset_def,phi_def]
   5.261 +      "[| #0<m; zgcd(x,m) = #1 |] ==> zcong (x^phi(m)) #1 m";
   5.262 +by (case_tac "x=#0" 1);
   5.263 +by (case_tac "m=#1" 2);
   5.264 +by (rtac iffD1 3);
   5.265 +by (res_inst_tac [("k","setprod (BnorRset (m-#1,m))")] zcong_cancel2 3);
   5.266 +by (stac (Bnor_prod_power RS sym) 5);
   5.267 +by (rtac Bnor_prod_zgcd 4);
   5.268 +by (ALLGOALS Asm_full_simp_tac);
   5.269 +by (rtac bijzcong_zcong_prod 1);
   5.270 +by (fold_goals_tac [norRRset_def,noXRRset_def]);
   5.271 +by (stac (RRset2norRR_eq_norR RS sym) 1);
   5.272 +by (rtac inj_func_bijR 3);
   5.273 +by Auto_tac;
   5.274 +by (rewtac zcongm_def);
   5.275 +by (rtac RRset2norRR_correct1 3);
   5.276 +by (rtac RRset2norRR_inj 6);
   5.277 +by (auto_tac (claset() addIs [zle_neq_implies_zless], 
   5.278 +              simpset() addsimps [noX_is_RRset]));
   5.279 +by (rewrite_goals_tac [noXRRset_def,norRRset_def]);
   5.280 +by (rtac finite_imageI 1);
   5.281 +by (rtac Bnor_fin 1);
   5.282 +qed "EulerFermatTheorem";
   5.283 +
   5.284 +Goalw [zprime_def] 
   5.285 +      "p:zprime ==> a<p --> (ALL b. #0<b & b<=a --> zgcd(b,p) = #1) \
   5.286 +\      --> card (BnorRset(a, p)) = nat a";
   5.287 +by (res_inst_tac [("u","a"),("v","p")] BnorRset.induct 1);
   5.288 +by (stac BnorRset_eq 1);
   5.289 +by (rewtac Let_def);
   5.290 +by Auto_tac;
   5.291 +by (asm_simp_tac (simpset() addsimps [Bnor_mem_zle_swap,Bnor_fin]) 1);
   5.292 +by (stac (int_int_eq RS sym) 1);
   5.293 +by Auto_tac;
   5.294 +qed_spec_mp "Bnor_prime";
   5.295 +
   5.296 +Goalw [phi_def,norRRset_def]
   5.297 +      "p:zprime ==> phi(p) = nat (p-#1)"; 
   5.298 +by (rtac Bnor_prime 1);
   5.299 +by Auto_tac;
   5.300 +by (etac zless_zprime_imp_zrelprime 1);
   5.301 +by (ALLGOALS Asm_simp_tac);
   5.302 +qed "phi_prime";
   5.303 +
   5.304 +Goal "[| p:zprime; ~p dvd x |] ==> zcong (x^(nat (p-#1))) #1 p";
   5.305 +by (stac (phi_prime RS sym) 1);
   5.306 +by (rtac EulerFermatTheorem 2);
   5.307 +by (etac zprime_imp_zrelprime 3);
   5.308 +by (rewtac zprime_def);
   5.309 +by Auto_tac;
   5.310 +qed "Little_Fermat";
   5.311 +
     6.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.2 +++ b/src/HOL/NumberTheory/EulerFermat.thy	Thu Aug 03 10:46:01 2000 +0200
     6.3 @@ -0,0 +1,46 @@
     6.4 +(*  Title:	EulerFermat.thy
     6.5 +    ID:         $Id$
     6.6 +    Author:	Thomas M. Rasmussen
     6.7 +    Copyright	2000  University of Cambridge
     6.8 +*)
     6.9 +
    6.10 +EulerFermat = BijectionRel + IntFact +
    6.11 +
    6.12 +consts
    6.13 +  RsetR        :: "int => int set set"
    6.14 +  BnorRset     :: "int*int=>int set" 
    6.15 +  norRRset     :: int => int set
    6.16 +  noXRRset     :: [int, int] => int set
    6.17 +  phi          :: int => nat
    6.18 +  is_RRset     :: [int set, int] => bool
    6.19 +  RRset2norRR  :: [int set, int, int] => int
    6.20 +
    6.21 +inductive "RsetR m"
    6.22 +intrs
    6.23 +  empty  "{} : RsetR m"
    6.24 +  insert "[| A : RsetR m; zgcd(a,m) = #1; \
    6.25 +\            ALL a'. a':A --> ~ zcong a a' m |] \
    6.26 +\        ==> insert a A : RsetR m"
    6.27 +
    6.28 +recdef BnorRset "measure ((% (a,m).(nat a)) ::int*int=>nat)"
    6.29 +    "BnorRset (a,m) = (if #0<a then let na = BnorRset (a-#1,m) in
    6.30 +                         (if zgcd(a,m) = #1 then insert a na else na) 
    6.31 +                       else {})"
    6.32 +
    6.33 +defs
    6.34 +  norRRset_def "norRRset m   == BnorRset (m-#1,m)"
    6.35 +
    6.36 +  noXRRset_def "noXRRset m x == (%a. a*x)``(norRRset m)"
    6.37 +
    6.38 +  phi_def      "phi m == card (norRRset m)"
    6.39 +
    6.40 +  is_RRset_def "is_RRset A m ==  (A : (RsetR m)) & card(A) = (phi m)"
    6.41 +
    6.42 +  RRset2norRR_def "RRset2norRR A m a == 
    6.43 +                     (if #1<m & (is_RRset A m) & a:A 
    6.44 +                      then @b. zcong a b m & b:(norRRset m) else #0)"
    6.45 +
    6.46 +consts zcongm :: int => [int, int] => bool
    6.47 +defs zcongm_def "zcongm m == (%a b. zcong a b m)"
    6.48 +
    6.49 +end
     7.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.2 +++ b/src/HOL/NumberTheory/IntFact.ML	Thu Aug 03 10:46:01 2000 +0200
     7.3 @@ -0,0 +1,87 @@
     7.4 +(*  Title:	IntPowerFact.ML
     7.5 +    ID:         $Id$
     7.6 +    Author:	Thomas M. Rasmussen
     7.7 +    Copyright	2000  University of Cambridge
     7.8 +
     7.9 +Factorial on integers.
    7.10 +Product of finite set.
    7.11 +Recursively defined set including all Integers from 2 up to a. 
    7.12 +*)
    7.13 +
    7.14 +
    7.15 +(*----  setprod  ----*)
    7.16 +
    7.17 +Goalw [setprod_def] "setprod {} = #1";
    7.18 +by (Simp_tac 1);
    7.19 +qed "setprod_empty";
    7.20 +Addsimps [setprod_empty];
    7.21 +
    7.22 +Goalw [setprod_def] 
    7.23 +      "[| finite A; a ~: A |] ==> setprod (insert a A) = a * setprod A";
    7.24 +by (asm_simp_tac (simpset() addsimps [zmult_left_commute,
    7.25 +                                      export fold_insert]) 1);
    7.26 +qed "setprod_insert";
    7.27 +Addsimps [setprod_insert];
    7.28 +
    7.29 +(*---- IntFact ----*)
    7.30 +
    7.31 +val [d22set_eq] = d22set.simps;
    7.32 +Delsimps d22set.simps;
    7.33 +
    7.34 +val [prem1,prem2] =
    7.35 +Goal "[| !!a. P {} a; \
    7.36 +\        !!a. [| #1<(a::int); P (d22set (a-#1)) (a-#1) |] \
    7.37 +\             ==> P (d22set a) a |] \
    7.38 +\    ==> P (d22set u) u";
    7.39 +by (rtac d22set.induct 1);
    7.40 +by Safe_tac;
    7.41 +by (case_tac "#1<a" 2);
    7.42 +by (rtac prem2 2);
    7.43 +by (ALLGOALS Asm_simp_tac);
    7.44 +by (ALLGOALS (asm_simp_tac (simpset() addsimps [d22set_eq,prem1])));
    7.45 +qed "d22set_induct";
    7.46 +
    7.47 +Goal "b:(d22set a) --> #1<b";
    7.48 +by (res_inst_tac [("u","a")] d22set_induct 1);
    7.49 +by (stac d22set_eq 2);
    7.50 +by Auto_tac;
    7.51 +qed_spec_mp "d22set_g_1";
    7.52 +
    7.53 +Goal "b:(d22set a) --> b<=a";
    7.54 +by (res_inst_tac [("u","a")] d22set_induct 1);
    7.55 +by (stac d22set_eq 2);
    7.56 +by Auto_tac;
    7.57 +qed_spec_mp "d22set_le";
    7.58 +
    7.59 +Goal "a<b ==> b~:(d22set a)";
    7.60 +by (res_inst_tac [("Pa","b<=a")] swap 1);
    7.61 +by (rtac d22set_le 2); 
    7.62 +by Auto_tac;
    7.63 +qed "d22set_le_swap";
    7.64 +
    7.65 +Goal "#1<b --> b<=a --> b:(d22set a)";
    7.66 +by (res_inst_tac [("u","a")] d22set.induct 1);
    7.67 +by Auto_tac;
    7.68 +by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [d22set_eq])));
    7.69 +qed_spec_mp "d22set_mem";
    7.70 +
    7.71 +Goal "finite (d22set a)";
    7.72 +by (res_inst_tac [("u","a")] d22set_induct 1);
    7.73 +by (stac d22set_eq 2);
    7.74 +by Auto_tac;
    7.75 +qed "d22set_fin";
    7.76 +
    7.77 +val [zfact_eq] = zfact.simps;
    7.78 +Delsimps zfact.simps; 
    7.79 +
    7.80 +Goal "setprod(d22set a) = zfact a";
    7.81 +by (res_inst_tac [("u","a")] d22set.induct 1);
    7.82 +by Safe_tac;
    7.83 +by (asm_full_simp_tac (simpset() addsimps [d22set_eq,zfact_eq]) 1);
    7.84 +by (stac d22set_eq 1);
    7.85 +by (stac zfact_eq 1);
    7.86 +by (case_tac "#1<a" 1);
    7.87 +by (asm_full_simp_tac (simpset() addsimps [d22set_eq,zfact_eq]) 2);
    7.88 +by (asm_full_simp_tac (simpset() addsimps [d22set_fin,d22set_le_swap]) 1);
    7.89 +qed "d22set_prod_zfact";
    7.90 +
     8.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     8.2 +++ b/src/HOL/NumberTheory/IntFact.thy	Thu Aug 03 10:46:01 2000 +0200
     8.3 @@ -0,0 +1,23 @@
     8.4 +(*  Title:	IntFact.thy
     8.5 +    ID:         $Id$
     8.6 +    Author:	Thomas M. Rasmussen
     8.7 +    Copyright	2000  University of Cambridge
     8.8 +*)
     8.9 +
    8.10 +IntFact = IntPrimes + 
    8.11 +
    8.12 +consts
    8.13 +  zfact    :: int => int
    8.14 +  setprod  :: int set => int
    8.15 +  d22set   :: int => int set
    8.16 +
    8.17 +recdef zfact "measure ((% n.(nat n)) ::int=>nat)"
    8.18 +    "zfact n = (if n<=#0 then #1 else n*zfact(n-#1))"
    8.19 +
    8.20 +defs
    8.21 +  setprod_def  "setprod A == (if finite A then fold (op*) #1 A else #1)"
    8.22 +
    8.23 +recdef d22set "measure ((%a.(nat a)) ::int=>nat)"
    8.24 +    "d22set a = (if #1<a then insert a (d22set (a-#1)) else {})"
    8.25 +
    8.26 +end
    8.27 \ No newline at end of file
     9.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     9.2 +++ b/src/HOL/NumberTheory/IntPrimes.ML	Thu Aug 03 10:46:01 2000 +0200
     9.3 @@ -0,0 +1,741 @@
     9.4 +(*  Title:	IntPrimes.ML
     9.5 +    ID:         $Id$
     9.6 +    Author:	Thomas M. Rasmussen
     9.7 +    Copyright	2000  University of Cambridge
     9.8 +
     9.9 +dvd relation, GCD, Euclid's extended algorithm, primes, congruences
    9.10 +(all on the Integers)
    9.11 +
    9.12 +Comparable to 'Primes' theory but dvd is included here as it is not present in
    9.13 +'IntDiv'. Also includes extended GCD and congruences not
    9.14 +present in 'Primes'.  Also a few extra theorems concerning 'mod'
    9.15 +*)
    9.16 +
    9.17 +eta_contract:=false;
    9.18 +
    9.19 +
    9.20 +(************************************************)
    9.21 +(** Divides relation 'dvd'                     **)
    9.22 +(************************************************)
    9.23 +
    9.24 +Goalw [dvd_def] "(m::int) dvd #0";
    9.25 +by (blast_tac (claset() addIs [zmult_0_right RS sym]) 1);
    9.26 +qed "zdvd_0_right";
    9.27 +AddIffs [zdvd_0_right];
    9.28 +
    9.29 +Goalw [dvd_def] "#0 dvd (m::int) ==> m = #0";
    9.30 +by Auto_tac;
    9.31 +qed "zdvd_0_left";
    9.32 +
    9.33 +Goalw [dvd_def] "#1 dvd (m::int)";
    9.34 +by (Simp_tac 1);
    9.35 +qed "zdvd_1_left";
    9.36 +AddIffs [zdvd_1_left];
    9.37 +
    9.38 +Goalw [dvd_def] "m dvd (m::int)";
    9.39 +by (blast_tac (claset() addIs [zmult_1_right RS sym]) 1);
    9.40 +qed "zdvd_refl";
    9.41 +Addsimps [zdvd_refl];
    9.42 +
    9.43 +Goalw [dvd_def] "[| m dvd n; n dvd k |] ==> m dvd (k::int)";
    9.44 +by (blast_tac (claset() addIs [zmult_assoc] ) 1);
    9.45 +qed "zdvd_trans";
    9.46 +
    9.47 +Goalw [dvd_def] "(m dvd -n) = (m dvd (n::int))";
    9.48 +by Auto_tac;
    9.49 +by (ALLGOALS (res_inst_tac [("x","-k")] exI));
    9.50 +by Auto_tac;
    9.51 +qed "zdvd_zminus_iff";  
    9.52 +
    9.53 +Goalw [dvd_def] "(-m dvd n) = (m dvd (n::int))";
    9.54 +by Auto_tac;
    9.55 +by (ALLGOALS (res_inst_tac [("x","-k")] exI));
    9.56 +by Auto_tac;
    9.57 +qed "zdvd_zminus2_iff";  
    9.58 +
    9.59 +Goalw [dvd_def] "[| #0<m; #0<n; m dvd n; n dvd m |] ==> m = (n::int)";
    9.60 +by Auto_tac;
    9.61 +by (asm_full_simp_tac
    9.62 +    (simpset() addsimps [zmult_assoc,zmult_eq_self_iff,
    9.63 +                         int_0_less_mult_iff, zmult_eq_1_iff]) 1);
    9.64 +qed "zdvd_anti_sym";
    9.65 +
    9.66 +Goalw [dvd_def] "[| k dvd m; k dvd n |] ==> k dvd (m+n :: int)";
    9.67 +by (blast_tac (claset() addIs [zadd_zmult_distrib2 RS sym]) 1);
    9.68 +qed "zdvd_zadd";
    9.69 +
    9.70 +Goalw [dvd_def] "[| k dvd m; k dvd n |] ==> k dvd (m-n :: int)";
    9.71 +by (blast_tac (claset() addIs [zdiff_zmult_distrib2 RS sym]) 1);
    9.72 +qed "zdvd_zdiff";
    9.73 +
    9.74 +Goal "[| k dvd (m-n); k dvd n |] ==> k dvd (m::int)";
    9.75 +by (subgoal_tac "m=n+(m-n)" 1);
    9.76 +by (etac ssubst 1);
    9.77 +by (blast_tac (claset() addIs [zdvd_zadd]) 1);
    9.78 +by (Simp_tac 1);
    9.79 +qed "zdvd_zdiffD";
    9.80 +
    9.81 +Goalw [dvd_def] "k dvd (n::int) ==> k dvd (m*n)";
    9.82 +by (blast_tac (claset() addIs [zmult_left_commute]) 1);
    9.83 +qed "zdvd_zmult";
    9.84 +
    9.85 +Goal "k dvd (m::int) ==> k dvd (m*n)";
    9.86 +by (stac zmult_commute 1);
    9.87 +by (etac zdvd_zmult 1);
    9.88 +qed "zdvd_zmult2";
    9.89 +
    9.90 +(* k dvd (m*k) *)
    9.91 +AddIffs [zdvd_refl RS zdvd_zmult, zdvd_refl RS zdvd_zmult2];
    9.92 +
    9.93 +Goalw [dvd_def] "(j*k) dvd n ==> j dvd (n::int)";
    9.94 +by (full_simp_tac (simpset() addsimps [zmult_assoc]) 1);
    9.95 +by (Blast_tac 1);
    9.96 +qed "zdvd_zmultD2";
    9.97 +
    9.98 +Goal "(j*k) dvd n ==> k dvd (n::int)";
    9.99 +by (rtac zdvd_zmultD2 1);
   9.100 +by (stac zmult_commute 1);
   9.101 +by (assume_tac 1);
   9.102 +qed "zdvd_zmultD";
   9.103 +
   9.104 +Goalw [dvd_def] "[| i dvd m; j dvd (n::int) |] ==> (i*j) dvd (m*n)";
   9.105 +by (Clarify_tac 1);
   9.106 +by (res_inst_tac [("x","k*ka")] exI 1);
   9.107 +by (asm_simp_tac (simpset() addsimps zmult_ac) 1);
   9.108 +qed "zdvd_zmult_mono";
   9.109 +
   9.110 +Goal "k dvd (n + k*m) = k dvd (n::int)";
   9.111 +by (rtac iffI 1);
   9.112 +by (etac zdvd_zadd 2);
   9.113 +by (subgoal_tac "n = (n+k*m)-k*m" 1);
   9.114 +by (etac ssubst 1);
   9.115 +by (etac zdvd_zdiff 1);
   9.116 +by (ALLGOALS Simp_tac);
   9.117 +qed "zdvd_reduce";
   9.118 +
   9.119 +Goalw [dvd_def] "[| f dvd m; f dvd (n::int) |] ==> f dvd (m mod n)";
   9.120 +by (auto_tac (claset(), simpset() addsimps [zmod_zmult_zmult1]));
   9.121 +qed "zdvd_zmod";
   9.122 +
   9.123 +Goal "[| k dvd (m mod n);  k dvd n |] ==> k dvd (m::int)";
   9.124 +by (subgoal_tac "k dvd (n*(m div n) + m mod n)" 1);
   9.125 +by (asm_simp_tac (simpset() addsimps [zdvd_zadd, zdvd_zmult2]) 2);
   9.126 +by (asm_full_simp_tac (simpset() addsimps [zmod_zdiv_equality RS sym]) 1);
   9.127 +qed "zdvd_zmod_imp_zdvd";
   9.128 +
   9.129 +Goalw [dvd_def] "(k dvd n) = (n mod (k::int) = #0)";
   9.130 +by (zdiv_undefined_case_tac "k=#0" 1);
   9.131 +by Safe_tac;
   9.132 +by (res_inst_tac [("x","n div k")] exI 2);
   9.133 +by (rtac trans 2);
   9.134 +by (res_inst_tac [("b","k")] zmod_zdiv_equality 2);
   9.135 +by (ALLGOALS Asm_simp_tac);
   9.136 +qed "zdvd_iff_zmod_eq_0";
   9.137 +
   9.138 +Goal "[| ~k<#0; k~=#0 |] ==> #0<(k::int)";
   9.139 +by (arith_tac 1);
   9.140 +val lemma = result();
   9.141 +
   9.142 +Goalw [dvd_def] "[| #0<m; m<n |] ==> ~n dvd (m::int)";
   9.143 +by Auto_tac;
   9.144 +by (subgoal_tac "#0<n" 1);
   9.145 +by (blast_tac (claset() addIs [zless_trans]) 2);
   9.146 +by (case_tac "k<#0" 1);
   9.147 +by (rotate_tac ~2 1);
   9.148 +by (asm_full_simp_tac (simpset() addsimps [int_0_less_mult_iff]) 1);
   9.149 +by (case_tac "k=#0" 1);
   9.150 +by (subgoal_tac "n*k < n*#1" 2);
   9.151 +by (asm_full_simp_tac (simpset() delsimps [zmult_1_right]) 2);
   9.152 +by (subgoal_tac "#0<k" 2);
   9.153 +by (rtac lemma 3);
   9.154 +by (ALLGOALS Asm_full_simp_tac);
   9.155 +qed "zdvd_not_zless";
   9.156 +
   9.157 +
   9.158 +(************************************************)
   9.159 +(** Euclid's Algorithm and GCD                 **)
   9.160 +(************************************************)
   9.161 +
   9.162 +val [zgcd_eq] = zgcd.simps;
   9.163 +Delsimps zgcd.simps;
   9.164 +
   9.165 +Goal "zgcd(m,#0) = m";
   9.166 +by (rtac (zgcd_eq RS trans) 1);
   9.167 +by (Simp_tac 1);
   9.168 +qed "zgcd_0";
   9.169 +Addsimps [zgcd_0];
   9.170 +
   9.171 +Goal"#0<(m::int) ==> zgcd(#0,m) = m";
   9.172 +by (auto_tac (claset(), simpset() addsimps zgcd.simps));
   9.173 +qed "zgcd_0_left";
   9.174 +Addsimps [zgcd_0_left];
   9.175 +
   9.176 +Goal "#0<n ==> zgcd(m,n) = zgcd (n, m mod n)";
   9.177 +by (rtac (zgcd_eq RS trans) 1);
   9.178 +by (Asm_simp_tac 1);
   9.179 +qed "zgcd_non_0";
   9.180 +
   9.181 +Goal "zgcd(m,#1) = #1";
   9.182 +by (simp_tac (simpset() addsimps [zgcd_non_0]) 1);
   9.183 +qed "zgcd_1";
   9.184 +Addsimps [zgcd_1];
   9.185 +
   9.186 +Goal "(zgcd(#0,m) = #1) = (m = #1)";
   9.187 +by (auto_tac (claset(),simpset() addsimps zgcd.simps));
   9.188 +qed "zgcd_0_1_iff";
   9.189 +Addsimps [zgcd_0_1_iff];
   9.190 +
   9.191 +Goal "#0<=(n::int) --> (zgcd(m,n) dvd m) & (zgcd(m,n) dvd n)";
   9.192 +by (res_inst_tac [("u","m"),("v","n")] zgcd.induct 1);
   9.193 +by (case_tac "n=#0" 1);
   9.194 +by (auto_tac (claset() addDs [zdvd_zmod_imp_zdvd],
   9.195 +              simpset() addsimps [zle_neq_implies_zless,neq_commute,
   9.196 +                                  pos_mod_sign,zgcd_non_0]));
   9.197 +by (ALLGOALS (rotate_tac 1));
   9.198 +by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [zle_anti_sym])));
   9.199 +qed_spec_mp "zgcd_zdvd_both";
   9.200 +
   9.201 +bind_thm ("zgcd_zdvd1", zgcd_zdvd_both RS conjunct1);
   9.202 +bind_thm ("zgcd_zdvd2", zgcd_zdvd_both RS conjunct2);
   9.203 +
   9.204 +Goal "[| (n::int) <= #0;  #0 <= n; #0 ~= n |] ==> False";
   9.205 +by (asm_full_simp_tac (simpset() addsimps [zle_anti_sym]) 1);
   9.206 +val lemma_false = result();
   9.207 +
   9.208 +Goal "#0<=(n::int) --> (f dvd m) --> (f dvd n) --> f dvd zgcd(m,n)";
   9.209 +by (res_inst_tac [("u","m"),("v","n")] zgcd.induct 1);
   9.210 +by (case_tac "n=#0" 1);
   9.211 +by (auto_tac (claset() addDs [lemma_false] addIs [pos_mod_sign,zdvd_zmod],
   9.212 +        simpset() addsimps [zgcd_non_0,neq_commute,zle_neq_implies_zless]));
   9.213 +qed_spec_mp "zgcd_greatest";
   9.214 +
   9.215 +Goal "#0 < (n::int) --> #0 < zgcd (m, n)";
   9.216 +by (res_inst_tac [("u","m"),("v","n")] zgcd.induct 1);
   9.217 +by (auto_tac (claset(), simpset() addsimps zgcd.simps));
   9.218 +qed_spec_mp "zgcd_zless";
   9.219 +
   9.220 +Goalw [is_zgcd_def] "#0<(n::int) ==> is_zgcd (zgcd(m,n)) m n";
   9.221 +by (asm_simp_tac (simpset() addsimps 
   9.222 +      [zgcd_greatest,zgcd_zdvd_both,zgcd_zless]) 1);
   9.223 +qed "is_zgcd";
   9.224 +
   9.225 +Goalw [is_zgcd_def] "[| is_zgcd m a b; is_zgcd n a b |] ==> m=n";
   9.226 +by (blast_tac (claset() addIs [zdvd_anti_sym]) 1);
   9.227 +qed "is_zgcd_unique";
   9.228 +
   9.229 +Goalw [is_zgcd_def] "[| is_zgcd m a b; k dvd a; k dvd b |] ==> k dvd m";
   9.230 +by (Blast_tac 1);
   9.231 +qed "is_zgcd_zdvd";
   9.232 +
   9.233 +Goalw [is_zgcd_def] "is_zgcd k m n = is_zgcd k n m";
   9.234 +by (Blast_tac 1);
   9.235 +qed "is_zgcd_commute";
   9.236 +
   9.237 +Goalw [is_zgcd_def] "is_zgcd k (-m) n = is_zgcd k m n";
   9.238 +by (asm_full_simp_tac (simpset() addsimps [zdvd_zminus_iff]) 1);
   9.239 +qed "is_zgcd_zminus";
   9.240 +
   9.241 +Goal "#0<(n::int) ==> zgcd(-m,n) = zgcd(m,n)";
   9.242 +by (rtac is_zgcd_unique 1);
   9.243 +by (rtac is_zgcd 1);
   9.244 +by (asm_simp_tac (simpset() addsimps [is_zgcd,is_zgcd_zminus]) 2);
   9.245 +by (assume_tac 1);
   9.246 +qed "zgcd_zminus";
   9.247 +
   9.248 +Goal "[| #0<(m::int); #0<n |] ==> zgcd(m,n) = zgcd(n,m)";
   9.249 +by (rtac is_zgcd_unique 1);
   9.250 +by (rtac is_zgcd 2);
   9.251 +by (asm_simp_tac (simpset() addsimps [is_zgcd,is_zgcd_commute]) 1);
   9.252 +by (assume_tac 1);
   9.253 +qed "zgcd_commute";
   9.254 +
   9.255 +Goal "#0<=(m::int) ==> zgcd(#1,m) = #1";
   9.256 +by (case_tac "m=#0" 1);
   9.257 +by (stac zgcd_commute 2);
   9.258 +by (ALLGOALS (asm_full_simp_tac (simpset() 
   9.259 +      addsimps [zle_neq_implies_zless,neq_commute])));
   9.260 +qed "zgcd_1_left";
   9.261 +Addsimps [zgcd_1_left];
   9.262 +
   9.263 +Goal "[| #0<(m::int); #0<n |] ==> zgcd(zgcd(k,m),n) = zgcd(k,zgcd(m,n))";
   9.264 +by (rtac is_zgcd_unique 1);
   9.265 +by (rtac is_zgcd 2);
   9.266 +by (rewrite_goals_tac [is_zgcd_def]);
   9.267 +by Auto_tac;
   9.268 +by (rtac zgcd_greatest 3);
   9.269 +by (res_inst_tac [("n","zgcd (k,m)")] zdvd_trans 2);
   9.270 +by (res_inst_tac [("n","zgcd (k,m)")] zdvd_trans 5);
   9.271 +by (rtac zgcd_greatest 8);
   9.272 +by (rtac zgcd_greatest 9);
   9.273 +by (res_inst_tac [("n","zgcd (m,n)")] zdvd_trans 12);
   9.274 +by (res_inst_tac [("n","zgcd (m,n)")] zdvd_trans 11);
   9.275 +by (ALLGOALS (asm_simp_tac (simpset() 
   9.276 +      addsimps [zgcd_zdvd1,zgcd_zdvd2,zgcd_zless])));
   9.277 +qed "zgcd_assoc";
   9.278 +
   9.279 +Goal "#0<=(n::int) --> #0<=k --> k * zgcd(m,n) = zgcd(k*m, k*n)";
   9.280 +by (res_inst_tac [("u","m"),("v","n")] zgcd.induct 1);
   9.281 +by (case_tac "n=#0" 1);
   9.282 +by (auto_tac (claset() addDs [lemma_false],
   9.283 +              simpset() addsimps [zle_neq_implies_zless,pos_mod_sign,
   9.284 +                                  zgcd_non_0,neq_commute]));
   9.285 +by (case_tac "k=#0" 1);
   9.286 +by (ALLGOALS (asm_full_simp_tac (simpset() 
   9.287 +      addsimps [zle_neq_implies_zless,zgcd_non_0,zmod_zmult_zmult1,
   9.288 +                int_0_less_mult_iff,neq_commute])));
   9.289 +qed_spec_mp "zgcd_zmult_distrib2";
   9.290 +
   9.291 +Goal "#0<=m ==> zgcd(m,m) = m";
   9.292 +by (cut_inst_tac [("k","m"),("m","#1"),("n","#1")] zgcd_zmult_distrib2 1);
   9.293 +by (ALLGOALS Asm_full_simp_tac);
   9.294 +qed "zgcd_self";
   9.295 +Addsimps [zgcd_self];
   9.296 +
   9.297 +Goal "[| #0<=k; #0<=n |] ==> zgcd(k, k*n) = k";
   9.298 +by (cut_inst_tac [("k","k"),("m","#1"),("n","n")] zgcd_zmult_distrib2 1);
   9.299 +by (ALLGOALS Asm_full_simp_tac);
   9.300 +qed "zgcd_zmult_eq_self";
   9.301 +Addsimps [zgcd_zmult_eq_self];
   9.302 +
   9.303 +Goal "#0<=k ==> zgcd(k*n, k) = k";
   9.304 +by (cut_inst_tac [("k","k"),("m","n"),("n","#1")] zgcd_zmult_distrib2 1);
   9.305 +by (ALLGOALS Asm_full_simp_tac);
   9.306 +qed "zgcd_zmult_eq_self2";
   9.307 +Addsimps [zgcd_zmult_eq_self2];
   9.308 +
   9.309 +Goal "[| #0<=(m::int); #0<=k; zgcd(n,k)=#1; k dvd (m*n) |] ==> k dvd m";
   9.310 +by (subgoal_tac "m = zgcd(m*n, m*k)" 1);
   9.311 +by (etac ssubst 1 THEN rtac zgcd_greatest 1);
   9.312 +by (ALLGOALS (asm_simp_tac (simpset() 
   9.313 +      addsimps [zgcd_zmult_distrib2 RS sym,int_0_le_mult_iff])));
   9.314 +qed "zrelprime_zdvd_zmult";
   9.315 +
   9.316 +Goalw [zprime_def] "[| p:zprime; ~p dvd n |] ==> zgcd(n,p) = #1";
   9.317 +by (cut_inst_tac [("m","n"),("n","p")] zgcd_zdvd_both 1);
   9.318 +by Auto_tac;
   9.319 +qed "zprime_imp_zrelprime";
   9.320 +
   9.321 +Goal "[| p:zprime; #0<n; n<p |] ==> zgcd(n,p) = #1";
   9.322 +by (etac zprime_imp_zrelprime 1);
   9.323 +by (etac zdvd_not_zless 1);
   9.324 +by (assume_tac 1);
   9.325 +qed "zless_zprime_imp_zrelprime";
   9.326 +
   9.327 +Goal "[| #0<=(m::int); p:zprime; p dvd (m*n) |] ==> p dvd m | p dvd n";
   9.328 +by Safe_tac;
   9.329 +by (rtac zrelprime_zdvd_zmult 1);
   9.330 +by (rtac zprime_imp_zrelprime 3);
   9.331 +by (SELECT_GOAL (rewrite_goals_tac [zprime_def]) 2);
   9.332 +by Auto_tac;
   9.333 +qed "zprime_zdvd_zmult";
   9.334 +
   9.335 +Goal "#0<n ==> zgcd(m+n*k,n) = zgcd(m,n)";
   9.336 +by (rtac (zgcd_eq RS trans) 1);
   9.337 +by Auto_tac;
   9.338 +by (simp_tac (simpset() addsimps [zmod_zadd1_eq]) 1);
   9.339 +by (rtac trans 1);
   9.340 +by (rtac (zgcd_eq RS sym) 2);
   9.341 +by Auto_tac;
   9.342 +qed "zgcd_zadd_zmult";
   9.343 +Addsimps [zgcd_zadd_zmult];
   9.344 +
   9.345 +Goal "#0<=n ==> zgcd(m,n) dvd zgcd(k*m,n)";
   9.346 +by (rtac zgcd_greatest 1);
   9.347 +by (rtac zdvd_trans 2);
   9.348 +by (rtac zgcd_zdvd1 2);
   9.349 +by (rtac zgcd_zdvd2 4);
   9.350 +by (ALLGOALS Asm_simp_tac);
   9.351 +qed "zgcd_zdvd_zgcd_zmult";
   9.352 +
   9.353 +Goal "[| #0<k; #0<m; #0<n; zgcd(k,n) = #1 |] ==> zgcd(k*m,n) dvd zgcd(m,n)";
   9.354 +by (rtac zgcd_greatest 1);
   9.355 +by (res_inst_tac [("n","k")] zrelprime_zdvd_zmult 2);
   9.356 +by (stac zmult_commute 5);
   9.357 +by (stac (zgcd_assoc RS sym) 4);
   9.358 +by (rtac zless_imp_zle 3);
   9.359 +by (ALLGOALS (asm_simp_tac (simpset() 
   9.360 +      addsimps [zgcd_zdvd1,zgcd_zdvd2,zgcd_zless,int_0_less_mult_iff])));
   9.361 +qed "zgcd_zmult_zdvd_zgcd";
   9.362 +
   9.363 +Goal "[| #0<n; zgcd(k,n) = #1 |] ==> zgcd(k*m, n) = zgcd(m,n)";
   9.364 +by (rtac zdvd_anti_sym 1);
   9.365 +by (rtac zgcd_zdvd_zgcd_zmult 4);
   9.366 +by (case_tac "m=#0" 3);
   9.367 +by (case_tac "k=#0" 4);
   9.368 +by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [zgcd_zless])));
   9.369 +by (case_tac "#0<k" 1);
   9.370 +by (ALLGOALS (case_tac "#0<m"));
   9.371 +by (rtac zgcd_zmult_zdvd_zgcd 1);
   9.372 +by (subgoal_tac "zgcd (k*(-m),n) dvd zgcd (-m,n)" 5);
   9.373 +by (rtac zgcd_zmult_zdvd_zgcd 6);
   9.374 +by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [zgcd_zminus])));
   9.375 +by (subgoal_tac "zgcd ((-k)*m,n) dvd zgcd (m,n)" 2);
   9.376 +by (rtac zgcd_zmult_zdvd_zgcd 3);
   9.377 +by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [zgcd_zminus])));
   9.378 +by (subgoal_tac "zgcd ((-k)*(-m),n) dvd zgcd (-m,n)" 3);
   9.379 +by (rtac zgcd_zmult_zdvd_zgcd 4);
   9.380 +by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [zgcd_zminus])));
   9.381 +by (auto_tac (claset() addIs [zle_neq_implies_zless], simpset()));
   9.382 +qed "zgcd_zmult_cancel";
   9.383 +
   9.384 +Goal "[| #0<m; zgcd(k,m) = #1; zgcd(n,m) = #1 |] ==> zgcd(k*n,m) = #1";
   9.385 +by (asm_simp_tac (simpset() addsimps [zgcd_zmult_cancel]) 1);
   9.386 +qed "zgcd_zgcd_zmult";
   9.387 +
   9.388 +Goal "#0<m ==> (m dvd n) = (zgcd(n,m) = m)";
   9.389 +by Safe_tac;
   9.390 +by (res_inst_tac [("n","zgcd(n,m)")] zdvd_trans 2);
   9.391 +by (rtac zgcd_zdvd1 3);
   9.392 +by (ALLGOALS Asm_simp_tac);
   9.393 +by (rewtac dvd_def);
   9.394 +by Auto_tac;
   9.395 +qed "zdvd_iff_zgcd";
   9.396 +
   9.397 +
   9.398 +(************************************************)
   9.399 +(** Congruences                                **)
   9.400 +(************************************************)
   9.401 +
   9.402 +Goalw [zcong_def] "[a=b](mod #1)";
   9.403 +by Auto_tac;
   9.404 +qed "zcong_1";
   9.405 +Addsimps [zcong_1];
   9.406 +
   9.407 +Goalw [zcong_def] "[k = k] (mod m)";
   9.408 +by Auto_tac;
   9.409 +qed "zcong_refl";
   9.410 +Addsimps [zcong_refl];
   9.411 +
   9.412 +Goalw [zcong_def,dvd_def] "[a = b](mod m) = [b = a](mod m)";
   9.413 +by Auto_tac;
   9.414 +by (ALLGOALS (res_inst_tac [("x","-k")] exI));
   9.415 +by Auto_tac;
   9.416 +qed "zcong_sym";
   9.417 +
   9.418 +Goalw [zcong_def]
   9.419 +     "[| [a = b] (mod m); [c = d] (mod m) |] ==> [a+c = b+d](mod m)";
   9.420 +by (res_inst_tac [("s","(a-b)+(c-d)")] subst 1);
   9.421 +by (rtac zdvd_zadd 2);
   9.422 +by Auto_tac;
   9.423 +qed "zcong_zadd";
   9.424 +
   9.425 +Goalw [zcong_def]
   9.426 +     "[| [a = b] (mod m); [c = d] (mod m) |] ==> [a-c = b-d](mod m)";
   9.427 +by (res_inst_tac [("s","(a-b)-(c-d)")] subst 1);
   9.428 +by (rtac zdvd_zdiff 2);
   9.429 +by Auto_tac;
   9.430 +qed "zcong_zdiff";
   9.431 +
   9.432 +Goalw [zcong_def,dvd_def]
   9.433 +     "[| [a = b](mod m); [b = c](mod m) |] ==> [a = c](mod m)";
   9.434 +by Auto_tac;
   9.435 +by (res_inst_tac [("x","k+ka")] exI 1);
   9.436 +by (asm_full_simp_tac (simpset() addsimps zadd_ac@[zadd_zmult_distrib2]) 1);
   9.437 +qed "zcong_trans";
   9.438 + 
   9.439 +Goal "[| [a = b] (mod m); [c = d] (mod m) |] ==> [a*c = b*d](mod m)";
   9.440 +by (res_inst_tac [("b","b*c")] zcong_trans 1);
   9.441 +by (rewtac zcong_def);
   9.442 +by (res_inst_tac [("s","c*(a-b)")] subst 1);
   9.443 +by (res_inst_tac [("s","b*(c-d)")] subst 3);
   9.444 +by (blast_tac (claset() addIs [zdvd_zmult]) 4);
   9.445 +by (blast_tac (claset() addIs [zdvd_zmult]) 2);
   9.446 +by (ALLGOALS (asm_simp_tac (simpset() addsimps [zdiff_zmult_distrib2,
   9.447 +                                                zmult_commute])));
   9.448 +qed "zcong_zmult";
   9.449 +
   9.450 +Goal "[a = b] (mod m) ==> [a*k = b*k](mod m)";
   9.451 +by (rtac zcong_zmult 1);
   9.452 +by (ALLGOALS Asm_simp_tac);
   9.453 +qed "zcong_scalar";
   9.454 +
   9.455 +Goal "[a = b] (mod m) ==> [k*a = k*b](mod m)";
   9.456 +by (rtac zcong_zmult 1);
   9.457 +by (ALLGOALS Asm_simp_tac);
   9.458 +qed "zcong_scalar2";
   9.459 +
   9.460 +Goalw [zcong_def] "[a*m = b*m](mod m)";
   9.461 +by (rtac zdvd_zdiff 1);
   9.462 +by (ALLGOALS Simp_tac);
   9.463 +qed "zcong_zmult_self";
   9.464 +
   9.465 +Goalw [zcong_def]
   9.466 +      "[| p:zprime; #0<a; [a*a = #1](mod p) |] \
   9.467 +\     ==> [a=#1](mod p) | [a = p-#1](mod p)";
   9.468 +by (rtac zprime_zdvd_zmult 1);
   9.469 +by (res_inst_tac [("s","a*a - #1 + p*(#1-a)")] subst 3);
   9.470 +by (simp_tac (simpset() addsimps [zdvd_reduce]) 4);
   9.471 +by (ALLGOALS (asm_simp_tac (simpset() 
   9.472 +      addsimps [zdiff_zmult_distrib,zmult_commute,zdiff_zmult_distrib2])));
   9.473 +qed "zcong_square";
   9.474 +
   9.475 +Goal "[| #0<=m; zgcd(k,m) = #1 |] ==> [a*k = b*k](mod m) = [a = b](mod m)";
   9.476 +by Safe_tac;
   9.477 +by (blast_tac (claset() addIs [zcong_scalar]) 2);
   9.478 +by (case_tac "b<a" 1);
   9.479 +by (stac zcong_sym 2);
   9.480 +by (rewrite_goals_tac [zcong_def]);
   9.481 +by (ALLGOALS (rtac zrelprime_zdvd_zmult));
   9.482 +by (ALLGOALS (asm_simp_tac (simpset() addsimps [zdiff_zmult_distrib])));
   9.483 +by (subgoal_tac "m dvd (-(a*k - b*k))" 1);
   9.484 +by (asm_full_simp_tac (simpset() addsimps [zminus_zdiff_eq]) 1);
   9.485 +by (stac zdvd_zminus_iff 1);
   9.486 +by (assume_tac 1);
   9.487 +qed "zcong_cancel";
   9.488 +
   9.489 +Goal "[| #0<=m; zgcd(k,m) = #1 |] ==> [k*a = k*b](mod m) = [a = b](mod m)";
   9.490 +by (asm_simp_tac (simpset() addsimps [zmult_commute,zcong_cancel]) 1);
   9.491 +qed "zcong_cancel2";
   9.492 +
   9.493 +Goalw [zcong_def,dvd_def]
   9.494 +      "[| #0<m; #0<n; [a = b] (mod m); [a = b] (mod n); zgcd(m,n) = #1 |] \
   9.495 +\     ==> [a=b](mod m*n)";
   9.496 +by Auto_tac;
   9.497 +by (subgoal_tac "m dvd (n*ka)" 1);
   9.498 +by (subgoal_tac "m dvd ka" 1);
   9.499 +by (case_tac "#0<=ka" 2);
   9.500 +by (stac (zdvd_zminus_iff RS sym) 3);
   9.501 +by (res_inst_tac [("n","n")] zrelprime_zdvd_zmult 2);
   9.502 +by (asm_simp_tac (simpset() addsimps [zgcd_commute]) 4);
   9.503 +by (asm_full_simp_tac (simpset() addsimps [zmult_commute]) 4);
   9.504 +by (res_inst_tac [("n","n")] zrelprime_zdvd_zmult 4);
   9.505 +by (asm_simp_tac (simpset() addsimps [zgcd_commute]) 6);
   9.506 +by (asm_full_simp_tac (simpset() addsimps [zmult_commute,zdvd_zminus_iff]) 6);
   9.507 +by (ALLGOALS Asm_simp_tac);
   9.508 +by (rewtac dvd_def);
   9.509 +by Safe_tac;
   9.510 +by (res_inst_tac [("x","kc")] exI 1);
   9.511 +by (res_inst_tac [("x","k")] exI 2);
   9.512 +by (simp_tac (simpset() addsimps zmult_ac) 1);
   9.513 +by Auto_tac;
   9.514 +qed "zcong_zgcd_zmult_zmod";
   9.515 +
   9.516 +Goalw [zcong_def,dvd_def] 
   9.517 +      "[| #0<=a; a<m; #0<=b; b<m; [a = b] (mod m) |] ==> a = b";
   9.518 +by (rtac (eq_iff_zdiff_eq_0 RS iffD2) 1);
   9.519 +by Auto_tac;
   9.520 +by (subgoal_tac "k=#0" 1);
   9.521 +by (subgoal_tac "#-1<k & k<#1" 2);
   9.522 +by Auto_tac;
   9.523 +by (ALLGOALS (rtac iffD1));
   9.524 +by (res_inst_tac [("k","m")] zmult_zless_cancel1 3);
   9.525 +by (res_inst_tac [("k","m")] zmult_zless_cancel1 1);
   9.526 +by Auto_tac;
   9.527 +qed "zcong_zless_imp_eq";
   9.528 +
   9.529 +Goal "[| p:zprime; #0<a; a<p; [a*a = #1](mod p) |] ==> a = #1 | a = p-#1";
   9.530 +by (cut_inst_tac [("p","p"),("a","a")] zcong_square 1);
   9.531 +by Safe_tac;
   9.532 +by (res_inst_tac [("Pa","a=p-#1")] swap 2);
   9.533 +by (rtac zcong_zless_imp_eq 1);
   9.534 +by (rtac zcong_zless_imp_eq 7);
   9.535 +by (rewtac zprime_def);
   9.536 +by Auto_tac;
   9.537 +qed "zcong_square_zless";
   9.538 +
   9.539 +Goalw [zcong_def] "[| #0<a; a<m; #0<b; b<a |] ==> ~[a = b] (mod m) ";
   9.540 +by (rtac zdvd_not_zless 1);
   9.541 +by Auto_tac;
   9.542 +qed "zcong_not";
   9.543 +
   9.544 +Goalw [zcong_def,dvd_def] "[| #0<=a; a<m; [a=#0](mod m) |] ==> a = #0";
   9.545 +by Auto_tac;
   9.546 +by (subgoal_tac "#0<m" 1);
   9.547 +by (rotate_tac ~1 1);
   9.548 +by (asm_full_simp_tac (simpset() addsimps [int_0_le_mult_iff]) 1);
   9.549 +by (subgoal_tac "m*k<m*#1" 1);
   9.550 +by (asm_full_simp_tac (simpset() delsimps [zmult_1_right]) 1);
   9.551 +by (ALLGOALS Asm_full_simp_tac);
   9.552 +qed "zcong_zless_0";
   9.553 +
   9.554 +Goal "#0<m ==> (EX! b. #0<=b & b<m & [a = b] (mod m))";
   9.555 +by Auto_tac;
   9.556 +by (subgoal_tac "[b = y] (mod m)" 2);
   9.557 +by (case_tac "b=#0" 2);
   9.558 +by (case_tac "y=#0" 3);
   9.559 +by (auto_tac (claset() addIs [zcong_trans,zcong_zless_0,
   9.560 +                              zcong_zless_imp_eq,zle_neq_implies_zless],
   9.561 +              simpset() addsimps [zcong_sym]));
   9.562 +by (rewrite_goals_tac [zcong_def,dvd_def]);
   9.563 +by (res_inst_tac [("x","a mod m")] exI 1);
   9.564 +by (auto_tac (claset(),simpset() addsimps [pos_mod_sign,pos_mod_bound]));
   9.565 +by (res_inst_tac [("x","-(a div m)")] exI 1);
   9.566 +by (cut_inst_tac [("a","a"),("b","m")] zmod_zdiv_equality 1);
   9.567 +by Auto_tac;
   9.568 +qed "zcong_zless_unique";
   9.569 +
   9.570 +Goalw [zcong_def,dvd_def] "([a = b] (mod m)) = (EX k. b = a + m*k)"; 
   9.571 +by Auto_tac;
   9.572 +by (ALLGOALS (res_inst_tac [("x","-k")] exI));
   9.573 +by Auto_tac;
   9.574 +qed "zcong_iff_lin";
   9.575 +
   9.576 +Goal "[| #0<m; zgcd(a,m) = #1; [a = b] (mod m) |] ==> zgcd(b,m) = #1";
   9.577 +by (auto_tac (claset(),simpset() addsimps [zcong_iff_lin]));
   9.578 +qed "zgcd_zcong_zgcd";
   9.579 +
   9.580 +Goal "[| a=c; b=d |] ==> a-b = c-(d::int)";
   9.581 +by Auto_tac;
   9.582 +val lemma = result();
   9.583 +
   9.584 +Goal "a - b = (m::int) * (a div m - b div m) + (a mod m - b mod m)";
   9.585 +by (res_inst_tac [("s","(m * (a div m) + a mod m) - \
   9.586 +\                 (m * (b div m) + b mod m)")] trans 1);
   9.587 +by (simp_tac (simpset() addsimps [zdiff_zmult_distrib2]) 2);
   9.588 +by (rtac lemma 1);
   9.589 +by (ALLGOALS (rtac zmod_zdiv_equality));
   9.590 +val lemma = result();
   9.591 +
   9.592 +Goalw [zcong_def] "[a = b] (mod m) = [a mod m = b mod m](mod m)";
   9.593 +by (res_inst_tac [("t","a-b")] ssubst 1);
   9.594 +by (res_inst_tac [("m","m")] lemma 1);
   9.595 +by (rtac trans 1);
   9.596 +by (res_inst_tac [("k","m"),("m","a div m - b div m")] zdvd_reduce 2);
   9.597 +by (simp_tac (simpset() addsimps [zadd_commute]) 1);
   9.598 +qed "zcong_zmod";
   9.599 +
   9.600 +Goal "#0<m ==> [a = b] (mod m) = (a mod m = b mod m)";
   9.601 +by Auto_tac;
   9.602 +by (res_inst_tac [("m","m")] zcong_zless_imp_eq 1);
   9.603 +by (stac (zcong_zmod RS sym) 5);
   9.604 +by (ALLGOALS (asm_simp_tac (simpset() addsimps [pos_mod_bound,pos_mod_sign])));
   9.605 +by (rewrite_goals_tac [zcong_def,dvd_def]);
   9.606 +by (res_inst_tac [("x","a div m - b div m")] exI 1);
   9.607 +by (res_inst_tac [("m1","m")] (lemma RS trans) 1);
   9.608 +by Auto_tac;
   9.609 +qed "zcong_zmod_eq";
   9.610 +
   9.611 +
   9.612 +(************************************************)
   9.613 +(** Modulo                                     **)
   9.614 +(************************************************)
   9.615 +
   9.616 +Goalw [dvd_def] "[| #0<(m::int); m dvd b |] ==> (a mod b mod m) = (a mod m)";
   9.617 +by Auto_tac;
   9.618 +by (stac (zcong_zmod_eq RS sym) 1);
   9.619 +by (stac zcong_iff_lin 2);
   9.620 +by (res_inst_tac [("x","k*(a div (m*k))")] exI 2);
   9.621 +by (stac zadd_commute 2);
   9.622 +by (stac (zmult_assoc RS sym) 2);
   9.623 +by (rtac zmod_zdiv_equality 2);
   9.624 +by (assume_tac 1);
   9.625 +qed "zmod_zdvd_zmod";
   9.626 +
   9.627 +(************************************************)
   9.628 +(** Extended GCD                               **)
   9.629 +(************************************************)
   9.630 +
   9.631 +val [xzgcda_eq] = xzgcda.simps;
   9.632 +Delsimps xzgcda.simps;
   9.633 +
   9.634 +Goal "zgcd(r',r) = k --> \
   9.635 +\     (EX sn tn. xzgcda (m,n,r',r,s',s,t',t) = (k,sn,tn))";
   9.636 +by (res_inst_tac [("u","m"),("v","n"),("w","r'"),("x","r"),
   9.637 +                  ("y","s'"),("z","s"),("aa","t'"),("ab","t")] 
   9.638 +                  xzgcda.induct 1);
   9.639 +by (stac zgcd_eq 1);
   9.640 +by (stac xzgcda_eq 1);
   9.641 +by Auto_tac;
   9.642 +val lemma1 = result();
   9.643 +
   9.644 +Goal "(EX sn tn. xzgcda (m,n,r',r,s',s,t',t) = (k,sn,tn)) --> \
   9.645 +\     zgcd(r',r) = k";
   9.646 +by (res_inst_tac [("u","m"),("v","n"),("w","r'"),("x","r"),
   9.647 +                  ("y","s'"),("z","s"),("aa","t'"),("ab","t")] 
   9.648 +                  xzgcda.induct 1);
   9.649 +by (stac zgcd_eq 1);
   9.650 +by (stac xzgcda_eq 1);
   9.651 +by Auto_tac;
   9.652 +val lemma2 = result();
   9.653 +
   9.654 +Goalw [xzgcd_def] "(zgcd(m,n) = k) = (EX s t. xzgcd m n = (k,s,t))"; 
   9.655 +by (rtac iffI 1);
   9.656 +by (ALLGOALS (rtac mp));
   9.657 +by (rtac lemma2 3);
   9.658 +by (rtac lemma1 1);
   9.659 +by Auto_tac;
   9.660 +qed "xzgcd_correct";
   9.661 +
   9.662 +(* xzgcd linear *)
   9.663 +
   9.664 +Goal "(a-r*b)*m + (c-r*d)*(n::int) = (a*m + c*n) - r*(b*m + d*n)";
   9.665 +by (simp_tac (simpset() addsimps [zdiff_zmult_distrib,zadd_zmult_distrib2,
   9.666 +                                  zmult_assoc]) 1);
   9.667 +val lemma = result();
   9.668 +
   9.669 +Goal "[| r' = s'*m + t'*n; r = s*m + t*n |] \
   9.670 +\    ==> (r' mod r) = (s' - (r' div r)*s)*m + (t' - (r' div r)*t)*(n::int)"; 
   9.671 +by (rtac trans 1);
   9.672 +by (rtac (lemma RS sym) 2);
   9.673 +by (Asm_simp_tac 1);
   9.674 +by (stac eq_zdiff_eq 1);
   9.675 +by (rtac (trans RS sym) 1);
   9.676 +by (res_inst_tac [("b","s*m + t*n")] zmod_zdiv_equality 1);
   9.677 +by (simp_tac (simpset() addsimps [zmult_commute]) 1);
   9.678 +val lemma = result();
   9.679 +
   9.680 +Goal "#0<r --> xzgcda(m,n,r',r,s',s,t',t) = (rn,sn,tn) \
   9.681 +\          --> r' = s'*m + t'*n -->  r = s*m + t*n --> rn = sn*m + tn*n";
   9.682 +by (res_inst_tac [("u","m"),("v","n"),("w","r'"),("x","r"),
   9.683 +                  ("y","s'"),("z","s"),("aa","t'"),("ab","t")] 
   9.684 +                  xzgcda.induct 1);
   9.685 +by (stac xzgcda_eq 1);
   9.686 +by (rewtac Let_def);
   9.687 +by (Simp_tac 1);
   9.688 +by (REPEAT (rtac impI 1));
   9.689 +by (case_tac "r' mod r = #0" 1);
   9.690 +by (asm_full_simp_tac (simpset() addsimps [xzgcda_eq]) 1);
   9.691 +by (SELECT_GOAL Safe_tac 1);
   9.692 +by (subgoal_tac "#0 < r' mod r" 1);
   9.693 +by (rtac zle_neq_implies_zless 2);
   9.694 +by (rtac pos_mod_sign 2);
   9.695 +by (cut_inst_tac [("m","m"),("n","n"),("r'","r'"),("r","r"),
   9.696 +                  ("s'","s'"),("s","s"),("t'","t'"),("t","t")] 
   9.697 +                 lemma 1);
   9.698 +by Auto_tac;
   9.699 +qed_spec_mp "xzgcda_linear";
   9.700 +
   9.701 +Goalw [xzgcd_def] "[| #0<n; xzgcd m n = (r,s,t) |] ==> r = s*m + t*n";
   9.702 +by (etac xzgcda_linear 1);
   9.703 +by (assume_tac 1);
   9.704 +by Auto_tac;
   9.705 +qed "xzgcd_linear";
   9.706 +
   9.707 +Goal "[| #0<n; zgcd(m,n) = k |] ==> (EX s t. k = s*m + t*n)";
   9.708 +by (full_simp_tac (simpset() addsimps [xzgcd_correct]) 1);
   9.709 +by Safe_tac;
   9.710 +by (REPEAT (rtac exI 1));
   9.711 +by (etac xzgcd_linear 1);
   9.712 +by Auto_tac;
   9.713 +qed "zgcd_ex_linear";
   9.714 +
   9.715 +Goal "[| #0<n; zgcd(a,n) = #1 |] ==> EX x. [a*x = #1](mod n)";
   9.716 +by (cut_inst_tac [("m","a"),("n","n"),("k","#1")] zgcd_ex_linear 1);
   9.717 +by Safe_tac;
   9.718 +by (res_inst_tac [("x","s")] exI 1);
   9.719 +by (res_inst_tac [("b","s*a+t*n")] zcong_trans 1);
   9.720 +by (Asm_simp_tac 2);
   9.721 +by (rewtac zcong_def);
   9.722 +by (simp_tac (simpset() addsimps [zmult_commute,zdvd_zminus_iff]) 1);
   9.723 +qed "zcong_lineq_ex";
   9.724 +
   9.725 +Goal "[| #0<n; zgcd(a,n) = #1 |] ==> EX! x. #0<=x & x<n & [a*x = b](mod n)";
   9.726 +by Auto_tac;
   9.727 +by (rtac zcong_zless_imp_eq 2);
   9.728 +by (stac (zcong_cancel2 RS sym) 6);
   9.729 +by (rtac zcong_trans 8);
   9.730 +by (ALLGOALS Asm_simp_tac);
   9.731 +by (asm_full_simp_tac (simpset() addsimps [zcong_sym]) 2);
   9.732 +by (cut_inst_tac [("a","a"),("n","n")] zcong_lineq_ex 1);
   9.733 +by Auto_tac;
   9.734 +by (res_inst_tac [("x","x*b mod n")] exI 1);
   9.735 +by Safe_tac;
   9.736 +by (ALLGOALS (asm_simp_tac (simpset() addsimps [pos_mod_bound,pos_mod_sign])));
   9.737 +by (stac zcong_zmod 1);
   9.738 +by (stac (zmod_zmult1_eq RS sym) 1);
   9.739 +by (stac (zcong_zmod RS sym) 1);
   9.740 +by (subgoal_tac "[a*x*b = #1*b](mod n)" 1);
   9.741 +by (rtac zcong_zmult 2);
   9.742 +by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [zmult_assoc])));
   9.743 +qed "zcong_lineq_unique";
   9.744 +
    10.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    10.2 +++ b/src/HOL/NumberTheory/IntPrimes.thy	Thu Aug 03 10:46:01 2000 +0200
    10.3 @@ -0,0 +1,39 @@
    10.4 +(*  Title:	IntPrimes.thy
    10.5 +    ID:         $Id$
    10.6 +    Author:	Thomas M. Rasmussen
    10.7 +    Copyright	2000  University of Cambridge
    10.8 +*)
    10.9 +
   10.10 +IntPrimes = Main + IntDiv +
   10.11 +
   10.12 +consts
   10.13 +  is_zgcd  :: [int,int,int] => bool         
   10.14 +  zgcd     :: "int*int => int"              
   10.15 +  xzgcda   :: "int*int*int*int*int*int*int*int => int*int*int"
   10.16 +  xzgcd    :: "[int,int] => int*int*int" 
   10.17 +  zprime   :: int set
   10.18 +  zcong    :: [int,int,int] => bool     ("(1[_ = _] '(mod _'))")
   10.19 +  
   10.20 +recdef zgcd "measure ((%(m,n).(nat n)) ::int*int=>nat)"
   10.21 +    simpset "simpset() addsimps [pos_mod_bound]"
   10.22 +    "zgcd (m, n) = (if n<=#0 then m else zgcd(n, m mod n))"
   10.23 +
   10.24 +recdef xzgcda 
   10.25 +       "measure ((%(m,n,r',r,s',s,t',t).(nat r))
   10.26 +                 ::int*int*int*int*int*int*int*int=>nat)"
   10.27 +        simpset "simpset() addsimps [pos_mod_bound]"
   10.28 +       "xzgcda (m,n,r',r,s',s,t',t) = 
   10.29 +          (if r<=#0 then (r',s',t') else  
   10.30 +           xzgcda(m,n,r,r' mod r,s,s'-(r' div r)*s,t,t'-(r' div r)*t))"
   10.31 +
   10.32 +defs
   10.33 +  xzgcd_def    "xzgcd m n == xzgcda (m,n,m,n,#1,#0,#0,#1)"
   10.34 +
   10.35 +  is_zgcd_def  "is_zgcd p m n == #0 < p  &  p dvd m  &  p dvd n  &
   10.36 +                                 (ALL d. d dvd m & d dvd n --> d dvd p)"
   10.37 +
   10.38 +  zprime_def   "zprime == {p. #1<p & (ALL m. m dvd p --> m=#1 | m=p)}"
   10.39 +
   10.40 +  zcong_def    "[a=b] (mod m) == m dvd (a-b)"
   10.41 +
   10.42 +end
    11.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    11.2 +++ b/src/HOL/NumberTheory/README	Thu Aug 03 10:46:01 2000 +0200
    11.3 @@ -0,0 +1,37 @@
    11.4 +IntPrimes	dvd relation, GCD, Euclid's extended algorithm, primes,
    11.5 +                congruences (all on the Integers)
    11.6 +                Comparable to 'Primes' theory but dvd is included here
    11.7 +                as it is not present in 'IntDiv'. Also includes extended
    11.8 +                GCD and congruences not present in 'Primes'. 
    11.9 +                Also a few extra theorems concerning 'mod'
   11.10 +                Maybe it should be split/merged - at least given another
   11.11 +                name?
   11.12 +
   11.13 +Chinese		The Chinese Remainder Theorem for an arbitrary finite
   11.14 +                number of equations. (The one-equation case is included
   11.15 +                in 'IntPrimes')
   11.16 +		Uses functions for indicing. Maybe 'funprod' and 'funsum'
   11.17 +                should be based on general 'fold' on indices?
   11.18 +
   11.19 +IntPowerFact    Power function on Integers (exponent is still Nat),
   11.20 +                Factorial on integers and recursively defined set
   11.21 +                including all Integers from 2 up to a. Plus definition 
   11.22 +		of product of finite set.
   11.23 +                Should probably be split/merged with other theories?
   11.24 +
   11.25 +BijectionRel    Inductive definitions of bijections between two different
   11.26 +                sets and between the same set. Theorem for relating
   11.27 +                the two definitions
   11.28 +
   11.29 +EulerFermat     Fermat's Little Theorem extended to Euler's Totient function.
   11.30 +                More abstract approach than Boyer-Moore (which seems necessary
   11.31 +                to achieve the extended version)
   11.32 +
   11.33 +WilsonRuss      Wilson's Theorem following quite closely Russinoff's approach
   11.34 +		using Boyer-Moore (using finite sets instead of lists, though)
   11.35 +
   11.36 +WilsonBij	Wilson's Theorem using a more "abstract" approach based on
   11.37 +		bijections between sets.  Does not use Fermat's Little Theorem
   11.38 +                (unlike Russinoff)
   11.39 + 
   11.40 +  
   11.41 \ No newline at end of file
    12.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    12.2 +++ b/src/HOL/NumberTheory/ROOT.ML	Thu Aug 03 10:46:01 2000 +0200
    12.3 @@ -0,0 +1,12 @@
    12.4 +(*  Title:      HOL/NumberTheory/ROOT
    12.5 +    ID:         $Id$
    12.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    12.7 +    Copyright   2000  University of Cambridge
    12.8 +
    12.9 +Number theory developments by Thomas M Rasmussen
   12.10 +*)
   12.11 +
   12.12 +use_thy "Chinese";
   12.13 +use_thy "EulerFermat";
   12.14 +use_thy "WilsonRuss";
   12.15 +use_thy "WilsonBij";
    13.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    13.2 +++ b/src/HOL/NumberTheory/WilsonBij.ML	Thu Aug 03 10:46:01 2000 +0200
    13.3 @@ -0,0 +1,227 @@
    13.4 +(*  Title:	WilsonBij.ML
    13.5 +    ID:         $Id$
    13.6 +    Author:	Thomas M. Rasmussen
    13.7 +    Copyright	2000  University of Cambridge
    13.8 +
    13.9 +Wilson's Theorem using a more "abstract" approach based on
   13.10 +bijections between sets.  Does not use Fermat's Little Theorem
   13.11 +(unlike Russinoff)
   13.12 + *)
   13.13 +
   13.14 +
   13.15 +(************  Inverse  **************)
   13.16 +
   13.17 +Goalw [inv_def] 
   13.18 +      "[| p:zprime; #0<a; a<p |] \ 
   13.19 +\     ==> #0 <= (inv p a) & (inv p a)<p & [a*(inv p a) = #1](mod p)";
   13.20 +by (Asm_simp_tac 1);
   13.21 +by (rtac (zcong_lineq_unique RS ex1_implies_ex RS ex_someI) 1);
   13.22 +by (etac zless_zprime_imp_zrelprime 2);
   13.23 +by (rewtac zprime_def);
   13.24 +by Auto_tac;
   13.25 +qed "inv_correct";
   13.26 +
   13.27 +bind_thm ("inv_ge",inv_correct RS conjunct1);
   13.28 +bind_thm ("inv_less",(inv_correct RS conjunct2) RS conjunct1);
   13.29 +bind_thm ("inv_is_inv",(inv_correct RS conjunct2) RS conjunct2);
   13.30 +
   13.31 +(* Same as WilsonRuss *)
   13.32 +Goal "[| p:zprime; #1<a; a<p-#1 |] ==> (inv p a) ~= #0";
   13.33 +by Safe_tac;
   13.34 +by (cut_inst_tac [("a","a"),("p","p")] inv_is_inv 1);
   13.35 +by (rewtac zcong_def);
   13.36 +by Auto_tac;
   13.37 +by (subgoal_tac "~p dvd #1" 1);
   13.38 +by (rtac zdvd_not_zless 2);
   13.39 +by (subgoal_tac "p dvd #1" 1);
   13.40 +by (stac (zdvd_zminus_iff RS sym) 2);
   13.41 +by Auto_tac;
   13.42 +qed "inv_not_0";
   13.43 +
   13.44 +(* Same as WilsonRuss *)
   13.45 +Goal "[| p:zprime; #1<a; a<p-#1 |] ==> (inv p a) ~= #1";
   13.46 +by Safe_tac;
   13.47 +by (cut_inst_tac [("a","a"),("p","p")] inv_is_inv 1);
   13.48 +by (Asm_full_simp_tac 4);
   13.49 +by (subgoal_tac "a = #1" 4);
   13.50 +by (rtac zcong_zless_imp_eq 5);
   13.51 +by Auto_tac;
   13.52 +qed "inv_not_1";
   13.53 +
   13.54 +(* Same as WilsonRuss *)
   13.55 +Goalw [zcong_def] "[a*(p-#1) = #1](mod p) = [a = p-#1](mod p)"; 
   13.56 +by (simp_tac (simpset() addsimps [zdiff_zdiff_eq,zdiff_zdiff_eq2,
   13.57 +                                  zdiff_zmult_distrib2]) 1);
   13.58 +by (res_inst_tac [("s","p dvd -((a+#1)+(p*(-a)))")] trans 1);
   13.59 +by (simp_tac (simpset() addsimps [zmult_commute,zminus_zdiff_eq]) 1);
   13.60 +by (stac zdvd_zminus_iff 1);
   13.61 +by (stac zdvd_reduce 1);
   13.62 +by (res_inst_tac [("s","p dvd ((a+#1)+(p*(-#1)))")] trans 1);
   13.63 +by (stac zdvd_reduce 1);
   13.64 +by Auto_tac;
   13.65 +val lemma = result();
   13.66 +
   13.67 +(* Same as WilsonRuss *)
   13.68 +Goal "[| p:zprime; #1<a; a<p-#1 |] ==> (inv p a) ~= p-#1";
   13.69 +by Safe_tac;
   13.70 +by (cut_inst_tac [("a","a"),("p","p")] inv_is_inv 1);
   13.71 +by Auto_tac;
   13.72 +by (asm_full_simp_tac (simpset() addsimps [lemma]) 1);
   13.73 +by (subgoal_tac "a = p-#1" 1);
   13.74 +by (rtac zcong_zless_imp_eq 2);
   13.75 +by Auto_tac;
   13.76 +qed "inv_not_p_minus_1";
   13.77 +
   13.78 +(* Below is slightly different as we don't expand 
   13.79 +   inv but use 'correct'-theos *)
   13.80 +Goal "[| p:zprime; #1<a; a<p-#1 |] ==> #1<(inv p a)";
   13.81 +by (subgoal_tac "(inv p a) ~= #1" 1);
   13.82 +by (subgoal_tac "(inv p a) ~= #0" 1);
   13.83 +by (rtac zle_neq_implies_zless 1);
   13.84 +by (stac (zle_add1_eq_le RS sym) 1);
   13.85 +by (rtac zle_neq_implies_zless 1);
   13.86 +by (rtac inv_not_0 4);
   13.87 +by (rtac inv_not_1 7);
   13.88 +by Auto_tac;
   13.89 +by (rtac inv_ge 1);
   13.90 +by Auto_tac;
   13.91 +qed "inv_g_1";
   13.92 +
   13.93 +(* ditto *)
   13.94 +Goal "[| p:zprime; #1<a; a<p-#1 |] ==> (inv p a)<p-#1";
   13.95 +by (rtac zle_neq_implies_zless 1);
   13.96 +by (rtac inv_not_p_minus_1 2);
   13.97 +by Auto_tac;
   13.98 +by (rtac inv_less 1);
   13.99 +by Auto_tac;
  13.100 +qed "inv_less_p_minus_1";
  13.101 +
  13.102 +(*************  Bijection  *******************)
  13.103 +
  13.104 +Goal "#1<x ==> #0<=(x::int)";
  13.105 +by Auto_tac;
  13.106 +val l1 = result();
  13.107 +
  13.108 +Goal "#1<x ==> #0<(x::int)";
  13.109 +by Auto_tac;
  13.110 +val l2 = result();
  13.111 +
  13.112 +Goal "x<=p-#2 ==> x<(p::int)";
  13.113 +by Auto_tac;
  13.114 +val l3 = result();
  13.115 +
  13.116 +Goal "x<=p-#2 ==> x<(p::int)-#1";
  13.117 +by Auto_tac;
  13.118 +val l4 = result();
  13.119 +
  13.120 +Goalw [inj_on_def] "p : zprime ==> inj_on (inv p) (d22set (p-#2))";
  13.121 +by Auto_tac;
  13.122 +by (rtac zcong_zless_imp_eq 1);
  13.123 +by (stac (zcong_cancel RS sym) 5);
  13.124 +by (rtac zcong_trans 7);
  13.125 +by (stac zcong_sym 8);
  13.126 +by (etac inv_is_inv 7);
  13.127 +by (Asm_simp_tac 9);
  13.128 +by (etac inv_is_inv 9);
  13.129 +by (rtac zless_zprime_imp_zrelprime 6);
  13.130 +by (rtac inv_less 8);
  13.131 +by (rtac (inv_g_1 RS l2) 7);
  13.132 +by (rewtac zprime_def);
  13.133 +by (auto_tac (claset() addIs [d22set_g_1,d22set_le,l1,l2,l3,l4],simpset()));
  13.134 +qed "inv_inj";
  13.135 +
  13.136 +Goal "p : zprime ==> (inv p)``(d22set (p-#2)) = (d22set (p-#2))";
  13.137 +by (rtac endo_inj_surj 1);
  13.138 +by (rtac d22set_fin 1);
  13.139 +by (etac inv_inj 2);
  13.140 +by Auto_tac;
  13.141 +by (rtac d22set_mem 1);
  13.142 +by (etac inv_g_1 1);
  13.143 +by (subgoal_tac "inv p xa < p - #1" 3);
  13.144 +by (etac inv_less_p_minus_1 4);
  13.145 +by (auto_tac (claset() addIs [d22set_g_1,d22set_le,l4],simpset()));
  13.146 +qed "inv_d22set_d22set";
  13.147 +
  13.148 +Goalw [reciR_def] "p:zprime \
  13.149 +\    ==> (d22set(p-#2),d22set(p-#2)) : (bijR (reciR p))";
  13.150 +by (res_inst_tac [("s","(d22set(p-#2),(inv p)``(d22set(p-#2)))")] subst 1);
  13.151 +by (asm_simp_tac (simpset() addsimps [inv_d22set_d22set]) 1);
  13.152 +by (rtac inj_func_bijR 1);
  13.153 +by (rtac d22set_fin 3);
  13.154 +by (etac inv_inj 2);
  13.155 +by Auto_tac;
  13.156 +by (etac inv_is_inv 1);
  13.157 +by (etac inv_g_1 5);
  13.158 +by (etac inv_less_p_minus_1 7);
  13.159 +by (auto_tac (claset() addIs [d22set_g_1,d22set_le,l2,l3,l4],simpset()));
  13.160 +qed "d22set_d22set_bij";
  13.161 +
  13.162 +Goalw [reciR_def,bijP_def] 
  13.163 +      "p:zprime ==>  bijP (reciR p) (d22set(p-#2))";
  13.164 +by Auto_tac;
  13.165 +by (rtac d22set_mem 1);
  13.166 +by Auto_tac;
  13.167 +qed "reciP_bijP";
  13.168 +
  13.169 +Goalw [reciR_def,uniqP_def] 
  13.170 +      "p:zprime ==> uniqP (reciR p)";
  13.171 +by Auto_tac;
  13.172 +by (rtac zcong_zless_imp_eq 1);
  13.173 +by (stac (zcong_cancel2 RS sym) 5);
  13.174 +by (rtac zcong_trans 7);
  13.175 +by (stac zcong_sym 8);
  13.176 +by (rtac zless_zprime_imp_zrelprime 6);
  13.177 +by Auto_tac;
  13.178 +by (rtac zcong_zless_imp_eq 1);
  13.179 +by (stac (zcong_cancel RS sym) 5);
  13.180 +by (rtac zcong_trans 7);
  13.181 +by (stac zcong_sym 8);
  13.182 +by (rtac zless_zprime_imp_zrelprime 6);
  13.183 +by Auto_tac;
  13.184 +qed "reciP_uniq";
  13.185 +
  13.186 +Goalw [reciR_def,symP_def] 
  13.187 +      "p:zprime ==> symP (reciR p)";
  13.188 +by (simp_tac (simpset() addsimps [zmult_commute]) 1);
  13.189 +by Auto_tac;
  13.190 +qed "reciP_sym";
  13.191 +
  13.192 +Goal "p:zprime ==> d22set(p-#2) : (bijER (reciR p))";
  13.193 +by (rtac bijR_bijER 1);
  13.194 +by (etac d22set_d22set_bij 1);
  13.195 +by (etac reciP_bijP 1);
  13.196 +by (etac reciP_uniq 1);
  13.197 +by (etac reciP_sym 1);
  13.198 +qed "bijER_d22set";
  13.199 +
  13.200 +(***********  Wilson  **************)
  13.201 +
  13.202 +Goalw [reciR_def] 
  13.203 +      "[| p:zprime; A : bijER (reciR p) |] ==> [setprod A = #1](mod p)";
  13.204 +by (etac bijER.induct 1);
  13.205 +by (subgoal_tac "a=#1 | a=p-#1" 2);
  13.206 +by (rtac zcong_square_zless 3);
  13.207 +by Auto_tac;
  13.208 +by (stac setprod_insert 1);
  13.209 +by (stac setprod_insert 3);
  13.210 +by (auto_tac (claset(),simpset() addsimps [fin_bijER]));
  13.211 +by (subgoal_tac "zcong ((a * b) * setprod A) (#1*#1) p" 1);
  13.212 +by (asm_full_simp_tac (simpset() addsimps [zmult_assoc]) 1);
  13.213 +by (rtac zcong_zmult 1); 
  13.214 +by Auto_tac;
  13.215 +qed "bijER_zcong_prod_1";
  13.216 +
  13.217 +Goal "p:zprime ==> [zfact(p-#1) = #-1](mod p)";
  13.218 +by (subgoal_tac "zcong ((p-#1)*zfact(p-#2)) (#-1*#1) p" 1);
  13.219 +by (rtac zcong_zmult 2);
  13.220 +by (SELECT_GOAL (rewtac zprime_def) 1);
  13.221 +by (stac zfact_eq 1);
  13.222 +by (res_inst_tac [("t","p-#1-#1"),("s","p-#2")] subst 1);
  13.223 +by Auto_tac;
  13.224 +by (SELECT_GOAL (rewtac zcong_def) 1);
  13.225 +by (Asm_simp_tac 1);
  13.226 +by (stac (d22set_prod_zfact RS sym) 1);
  13.227 +by (rtac bijER_zcong_prod_1 1);
  13.228 +by (rtac bijER_d22set 2);
  13.229 +by Auto_tac;
  13.230 +qed "WilsonBij";
    14.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    14.2 +++ b/src/HOL/NumberTheory/WilsonBij.thy	Thu Aug 03 10:46:01 2000 +0200
    14.3 @@ -0,0 +1,20 @@
    14.4 +(*  Title:	WilsonBij.thy
    14.5 +    ID:         $Id$
    14.6 +    Author:	Thomas M. Rasmussen
    14.7 +    Copyright	2000  University of Cambridge
    14.8 +*)
    14.9 +
   14.10 +WilsonBij = BijectionRel + IntFact +
   14.11 +
   14.12 +consts
   14.13 +  reciR  :: "int => [int,int] => bool"
   14.14 +  inv    :: "[int,int] => int"
   14.15 +
   14.16 +defs
   14.17 +  reciR_def "reciR p == (%a b. zcong (a*b) #1 p & 
   14.18 +                               #1<a & a<p-#1 & #1<b & b<p-#1)"
   14.19 +  inv_def   "inv p a == (if p:zprime & #0<a & a<p then
   14.20 +                           (@x. #0<=x & x<p & zcong (a*x) #1 p)
   14.21 +                         else #0)"
   14.22 +
   14.23 +end
    15.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    15.2 +++ b/src/HOL/NumberTheory/WilsonRuss.ML	Thu Aug 03 10:46:01 2000 +0200
    15.3 @@ -0,0 +1,319 @@
    15.4 +(*  Title:	WilsonRuss.ML
    15.5 +    ID:         $Id$
    15.6 +    Author:	Thomas M. Rasmussen
    15.7 +    Copyright	2000  University of Cambridge
    15.8 +*)
    15.9 +
   15.10 +
   15.11 +(************  Inverse  **************)
   15.12 +
   15.13 +Goal "#1<m ==> Suc(nat(m-#2)) = nat(m-#1)";
   15.14 +by (stac (int_int_eq RS sym) 1);
   15.15 +by Auto_tac;
   15.16 +val lemma = result();
   15.17 +
   15.18 +Goalw [inv_def]
   15.19 +      "[| p:zprime; #0<a; a<p |] ==> [a*(inv p a) = #1] (mod p)";
   15.20 +by (stac zcong_zmod 1);
   15.21 +by (stac (zmod_zmult1_eq RS sym) 1);
   15.22 +by (stac (zcong_zmod RS sym) 1);
   15.23 +by (stac (power_Suc RS sym) 1);
   15.24 +by (stac lemma 1);
   15.25 +by (etac Little_Fermat 2);
   15.26 +by (etac zdvd_not_zless 2);
   15.27 +by (rewtac zprime_def);
   15.28 +by Auto_tac;
   15.29 +qed "inv_is_inv";
   15.30 +
   15.31 +Goal "[| p:zprime; #1<a; a<p-#1 |] ==> a ~= (inv p a)";
   15.32 +by Safe_tac;
   15.33 +by (cut_inst_tac [("a","a"),("p","p")] zcong_square 1);
   15.34 +by (cut_inst_tac [("a","a"),("p","p")] inv_is_inv 3);
   15.35 +by Auto_tac;
   15.36 +by (subgoal_tac "a=#1" 1);
   15.37 +by (res_inst_tac [("m","p")] zcong_zless_imp_eq 2);
   15.38 +by (subgoal_tac "a=p-#1" 7);
   15.39 +by (res_inst_tac [("m","p")] zcong_zless_imp_eq 8);
   15.40 +by Auto_tac;
   15.41 +qed "inv_distinct";
   15.42 +
   15.43 +Goal "[| p:zprime; #1<a; a<p-#1 |] ==> (inv p a) ~= #0";
   15.44 +by Safe_tac;
   15.45 +by (cut_inst_tac [("a","a"),("p","p")] inv_is_inv 1);
   15.46 +by (rewtac zcong_def);
   15.47 +by Auto_tac;
   15.48 +by (subgoal_tac "~p dvd #1" 1);
   15.49 +by (rtac zdvd_not_zless 2);
   15.50 +by (subgoal_tac "p dvd #1" 1);
   15.51 +by (stac (zdvd_zminus_iff RS sym) 2);
   15.52 +by Auto_tac;
   15.53 +qed "inv_not_0";
   15.54 +
   15.55 +Goal "[| p:zprime; #1<a; a<p-#1 |] ==> (inv p a) ~= #1";
   15.56 +by Safe_tac;
   15.57 +by (cut_inst_tac [("a","a"),("p","p")] inv_is_inv 1);
   15.58 +by (Asm_full_simp_tac 4);
   15.59 +by (subgoal_tac "a = #1" 4);
   15.60 +by (rtac zcong_zless_imp_eq 5);
   15.61 +by Auto_tac;
   15.62 +qed "inv_not_1";
   15.63 +
   15.64 +Goalw [zcong_def] "[a*(p-#1) = #1](mod p) = [a = p-#1](mod p)"; 
   15.65 +by (simp_tac (simpset() addsimps [zdiff_zdiff_eq,zdiff_zdiff_eq2,
   15.66 +                                  zdiff_zmult_distrib2]) 1);
   15.67 +by (res_inst_tac [("s","p dvd -((a+#1)+(p*(-a)))")] trans 1);
   15.68 +by (simp_tac (simpset() addsimps [zmult_commute,zminus_zdiff_eq]) 1);
   15.69 +by (stac zdvd_zminus_iff 1);
   15.70 +by (stac zdvd_reduce 1);
   15.71 +by (res_inst_tac [("s","p dvd ((a+#1)+(p*(-#1)))")] trans 1);
   15.72 +by (stac zdvd_reduce 1);
   15.73 +by Auto_tac;
   15.74 +val lemma = result();
   15.75 +
   15.76 +Goal "[| p:zprime; #1<a; a<p-#1 |] ==> (inv p a) ~= p-#1";
   15.77 +by Safe_tac;
   15.78 +by (cut_inst_tac [("a","a"),("p","p")] inv_is_inv 1);
   15.79 +by Auto_tac;
   15.80 +by (asm_full_simp_tac (simpset() addsimps [lemma]) 1);
   15.81 +by (subgoal_tac "a = p-#1" 1);
   15.82 +by (rtac zcong_zless_imp_eq 2);
   15.83 +by Auto_tac;
   15.84 +qed "inv_not_p_minus_1";
   15.85 +
   15.86 +Goal "[| p:zprime; #1<a; a<p-#1 |] ==> #1<(inv p a)";
   15.87 +by (case_tac "#0<=(inv p a)" 1);
   15.88 +by (subgoal_tac "(inv p a) ~= #1" 1);
   15.89 +by (subgoal_tac "(inv p a) ~= #0" 1);
   15.90 +by (rtac zle_neq_implies_zless 1);
   15.91 +by (stac (zle_add1_eq_le RS sym) 1);
   15.92 +by (rtac zle_neq_implies_zless 1);
   15.93 +by (rtac inv_not_0 4);
   15.94 +by (rtac inv_not_1 7);
   15.95 +by Auto_tac;
   15.96 +by (rewrite_goals_tac [inv_def,zprime_def]);
   15.97 +by (asm_full_simp_tac (simpset() addsimps [pos_mod_sign]) 1);
   15.98 +qed "inv_g_1";
   15.99 +
  15.100 +Goal "[| p:zprime; #1<a; a<p-#1 |] ==> (inv p a)<p-#1";
  15.101 +by (case_tac "(inv p a)<p" 1);
  15.102 +by (rtac zle_neq_implies_zless 1);
  15.103 +by (rtac inv_not_p_minus_1 2);
  15.104 +by Auto_tac;
  15.105 +by (rewrite_goals_tac [inv_def,zprime_def]);
  15.106 +by (asm_full_simp_tac (simpset() addsimps [pos_mod_bound]) 1);
  15.107 +qed "inv_less_p_minus_1";
  15.108 +
  15.109 +Goal "#5<=p ==> nat(p-#2)*nat(p-#2) = Suc(nat(p-#1)*nat(p-#3))";
  15.110 +by (stac (int_int_eq RS sym) 1);
  15.111 +by (asm_simp_tac (simpset() addsimps [zmult_int RS sym]) 1);
  15.112 +by (simp_tac (simpset() addsimps [zdiff_zmult_distrib,
  15.113 +                                  zdiff_zmult_distrib2]) 1);
  15.114 +val lemma = result();
  15.115 +
  15.116 +Goal "[x^y = #1](mod p) --> [x^(y*z) = #1](mod p)";
  15.117 +by (induct_tac "z" 1);
  15.118 +by (auto_tac (claset(),simpset() addsimps [zpower_zadd_distrib]));
  15.119 +by (subgoal_tac "zcong (x^y * x^(y*n)) (#1*#1) p" 1);
  15.120 +by (rtac zcong_zmult 2);
  15.121 +by (ALLGOALS Asm_full_simp_tac);
  15.122 +qed_spec_mp "zcong_zpower_zmult";
  15.123 +
  15.124 +Goalw [inv_def] "[| p:zprime; #5<=p; #0<a; a<p |] ==> (inv p (inv p a)) = a";
  15.125 +by (stac zpower_zmod 1);
  15.126 +by (stac zpower_zpower 1);
  15.127 +by (rtac zcong_zless_imp_eq 1);
  15.128 +by (stac zcong_zmod 5); 
  15.129 +by (stac mod_mod_trivial 5);
  15.130 +by (stac (zcong_zmod RS sym) 5); 
  15.131 +by (stac lemma 5);
  15.132 +by (subgoal_tac "zcong (a * a^(nat (p - #1) * nat (p - #3))) (a*#1) p" 6);
  15.133 +by (rtac zcong_zmult 7);
  15.134 +by (rtac zcong_zpower_zmult 8);
  15.135 +by (etac Little_Fermat 8);
  15.136 +by (rtac zdvd_not_zless 8);
  15.137 +by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [pos_mod_bound,
  15.138 +                                                     pos_mod_sign])));
  15.139 +qed "inv_inv";
  15.140 +
  15.141 +
  15.142 +(*************  wset  *************)
  15.143 +
  15.144 +val [wset_eq] = wset.simps;
  15.145 +Delsimps wset.simps;
  15.146 +
  15.147 +val [prem1,prem2] =
  15.148 +Goal "[| !!a p. P {} a p; \
  15.149 +\        !!a p. [| #1<(a::int); P (wset (a-#1,p)) (a-#1) p |] \
  15.150 +\               ==> P (wset (a,p)) a p|] \
  15.151 +\    ==> P (wset (u,v)) u v";
  15.152 +by (rtac wset.induct 1);
  15.153 +by Safe_tac;
  15.154 +by (case_tac "#1<a" 2);
  15.155 +by (rtac prem2 2);
  15.156 +by (ALLGOALS Asm_simp_tac);
  15.157 +by (ALLGOALS (asm_simp_tac (simpset() addsimps [wset_eq,prem1])));
  15.158 +qed "wset_induct";
  15.159 +
  15.160 +Goal "[| #1<a; b~:(wset (a-#1,p)) |] \
  15.161 +\     ==> b:(wset (a,p)) --> b=a | b = inv p a";
  15.162 +by (stac wset_eq 1);
  15.163 +by (rewtac Let_def);
  15.164 +by (Asm_simp_tac 1);
  15.165 +qed_spec_mp "wset_mem_imp_or";
  15.166 +
  15.167 +Goal "#1<a ==> a:(wset(a,p))";
  15.168 +by (stac wset_eq 1);
  15.169 +by (rewtac Let_def);
  15.170 +by (Asm_simp_tac 1);
  15.171 +qed "wset_mem_mem";
  15.172 +Addsimps [wset_mem_mem];
  15.173 +
  15.174 +Goal "[| #1<a; b:wset(a-#1,p) |] ==> b:wset(a,p)";
  15.175 +by (stac wset_eq 1);
  15.176 +by (rewtac Let_def);
  15.177 +by Auto_tac;
  15.178 +qed "wset_subset";
  15.179 +
  15.180 +Goal "p:zprime --> a<p-#1 --> b:(wset(a,p)) --> #1<b";
  15.181 +by (res_inst_tac [("u","a"),("v","p")] wset_induct 1);
  15.182 +by Auto_tac;
  15.183 +by (case_tac "b=a" 1);
  15.184 +by (case_tac "b=inv p a" 2);
  15.185 +by (subgoal_tac "b=a | b = inv p a" 3);
  15.186 +by (rtac wset_mem_imp_or 4);
  15.187 +by (Asm_simp_tac 2);
  15.188 +by (rtac inv_g_1 2);
  15.189 +by Auto_tac;
  15.190 +qed_spec_mp "wset_g_1";
  15.191 +
  15.192 +Goal "p:zprime --> a<p-#1 --> b:(wset(a,p)) --> b<p-#1";
  15.193 +by (res_inst_tac [("u","a"),("v","p")] wset_induct 1);
  15.194 +by Auto_tac;
  15.195 +by (case_tac "b=a" 1);
  15.196 +by (case_tac "b=inv p a" 2);
  15.197 +by (subgoal_tac "b=a | b = inv p a" 3);
  15.198 +by (rtac wset_mem_imp_or 4);
  15.199 +by (Asm_simp_tac 2);
  15.200 +by (rtac inv_less_p_minus_1 2);
  15.201 +by Auto_tac;
  15.202 +qed_spec_mp "wset_less";
  15.203 +
  15.204 +Goal "p:zprime --> a<p-#1 --> #1<b --> b<=a --> b:(wset(a,p))"; 
  15.205 +by (res_inst_tac [("u","a"),("v","p")] wset.induct 1);
  15.206 +by Auto_tac;
  15.207 +by (subgoal_tac "b=a" 1);
  15.208 +by (rtac zle_anti_sym 2);
  15.209 +by (rtac wset_subset 4);
  15.210 +by (Asm_simp_tac 1);
  15.211 +by Auto_tac;
  15.212 +qed_spec_mp "wset_mem";
  15.213 +
  15.214 +Goal "p:zprime --> #5<=p --> a<p-#1 --> b:(wset (a,p)) \
  15.215 +\     --> (inv p b):(wset (a,p))";
  15.216 +by (res_inst_tac [("u","a"),("v","p")] wset_induct 1);
  15.217 +by Auto_tac;
  15.218 +by (case_tac "b=a" 1);
  15.219 +by (stac wset_eq 1);
  15.220 +by (rewtac Let_def);
  15.221 +by (rtac wset_subset 3);
  15.222 +by Auto_tac;
  15.223 +by (case_tac "b = inv p a" 1);
  15.224 +by (Asm_simp_tac 1);
  15.225 +by (stac inv_inv 1);
  15.226 +by (subgoal_tac "b=a | b = inv p a" 6);
  15.227 +by (rtac wset_mem_imp_or 7);
  15.228 +by Auto_tac;
  15.229 +qed_spec_mp "wset_mem_inv_mem";
  15.230 +
  15.231 +Goal "[| p:zprime; #5<=p; a<p-#1; #1<b; b<p-#1; (inv p b):(wset (a,p)) |] \
  15.232 +\    ==> b:(wset (a,p))";
  15.233 +by (res_inst_tac [("s","inv p (inv p b)"),("t","b")] subst 1);
  15.234 +by (rtac wset_mem_inv_mem 2);
  15.235 +by (rtac inv_inv 1);
  15.236 +by (ALLGOALS (Asm_simp_tac));
  15.237 +qed "wset_inv_mem_mem";
  15.238 +
  15.239 +Goal "finite (wset (a,p))";
  15.240 +by (res_inst_tac [("u","a"),("v","p")] wset_induct 1);
  15.241 +by (stac wset_eq 2);
  15.242 +by (rewtac Let_def);
  15.243 +by Auto_tac;
  15.244 +qed "wset_fin";
  15.245 +
  15.246 +Goal "p:zprime --> #5<=p --> a<p-#1 --> [setprod (wset (a,p)) = #1](mod p)";
  15.247 +by (res_inst_tac [("u","a"),("v","p")] wset_induct 1);
  15.248 +by (stac wset_eq 2);
  15.249 +by (rewtac Let_def);
  15.250 +by Auto_tac;
  15.251 +by (stac setprod_insert 1);
  15.252 +by (stac setprod_insert 3);
  15.253 +by (subgoal_tac "zcong (a * (inv p a) * setprod(wset(a-#1,p))) (#1*#1) p" 5);
  15.254 +by (asm_full_simp_tac (simpset() addsimps [zmult_assoc]) 5);
  15.255 +by (rtac zcong_zmult 5);
  15.256 +by (rtac inv_is_inv 5);
  15.257 +by (Clarify_tac 4);
  15.258 +by (subgoal_tac "a:wset(a-#1,p)" 4);
  15.259 +by (rtac wset_inv_mem_mem 5);
  15.260 +by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [wset_fin])));
  15.261 +by (rtac inv_distinct 1);
  15.262 +by Auto_tac;
  15.263 +qed_spec_mp "wset_zcong_prod_1";
  15.264 +
  15.265 +Goal "p:zprime ==> d22set(p-#2) = wset(p-#2,p)";
  15.266 +by Safe_tac;
  15.267 +by (etac wset_mem 1); 
  15.268 +by (rtac d22set_g_1 2);
  15.269 +by (rtac d22set_le 3);
  15.270 +by (rtac d22set_mem 4);
  15.271 +by (etac wset_g_1 4);
  15.272 +by (stac (zle_add1_eq_le RS sym) 6); 
  15.273 +by (subgoal_tac "p-#2+#1 = p-#1" 6);
  15.274 +by (Asm_simp_tac 6);
  15.275 +by (etac wset_less 6);
  15.276 +by Auto_tac;
  15.277 +qed "d22set_eq_wset";
  15.278 +
  15.279 +(**********  Wilson  *************)
  15.280 +
  15.281 +Goal "[| z-#1<=w; z-#1~=w |] ==> z<=(w::int)";
  15.282 +by (stac (zle_add1_eq_le RS sym) 1);
  15.283 +by (rtac zle_neq_implies_zless 1);
  15.284 +by Auto_tac;
  15.285 +val lemma = result();
  15.286 +
  15.287 +Goalw [zprime_def,dvd_def] "[| p : zprime; p ~= #2; p ~= #3 |] ==> #5<=p";
  15.288 +by (case_tac "p=#4" 1);
  15.289 +by Auto_tac;
  15.290 +by (rtac notE 1);
  15.291 +by (assume_tac 2);
  15.292 +by (Simp_tac 1);
  15.293 +by (res_inst_tac [("x","#2")] exI 1);
  15.294 +by Safe_tac;
  15.295 +by (res_inst_tac [("x","#2")] exI 1);
  15.296 +by Auto_tac;
  15.297 +by (rtac lemma 1);
  15.298 +by (rtac lemma 1);
  15.299 +by (rtac lemma 1);
  15.300 +by Auto_tac;
  15.301 +qed "prime_g_5";
  15.302 +
  15.303 +Goal "p:zprime ==> [zfact(p-#1) = #-1] (mod p)";
  15.304 +by (subgoal_tac "[(p-#1)*zfact(p-#2) = #-1*#1] (mod p)" 1);
  15.305 +by (rtac zcong_zmult 2);
  15.306 +by (SELECT_GOAL (rewtac zprime_def) 1);
  15.307 +by (stac zfact_eq 1);
  15.308 +by (res_inst_tac [("t","p-#1-#1"),("s","p-#2")] subst 1);
  15.309 +by Auto_tac;
  15.310 +by (SELECT_GOAL (rewtac zcong_def) 1);
  15.311 +by (Asm_simp_tac 1);
  15.312 +by (case_tac "p=#2" 1);
  15.313 +by (asm_full_simp_tac (simpset() addsimps [zfact_eq]) 1);
  15.314 +by (case_tac "p=#3" 1);
  15.315 +by (asm_full_simp_tac (simpset() addsimps [zfact_eq]) 1);
  15.316 +by (subgoal_tac "#5<=p" 1);
  15.317 +by (etac prime_g_5 2);
  15.318 +by (stac (d22set_prod_zfact RS sym) 1);
  15.319 +by (stac d22set_eq_wset 1);
  15.320 +by (rtac wset_zcong_prod_1 2);
  15.321 +by Auto_tac;
  15.322 +qed "WilsonRuss";
    16.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    16.2 +++ b/src/HOL/NumberTheory/WilsonRuss.thy	Thu Aug 03 10:46:01 2000 +0200
    16.3 @@ -0,0 +1,21 @@
    16.4 +(*  Title:	WilsonRuss.thy
    16.5 +    ID:         $Id$
    16.6 +    Author:	Thomas M. Rasmussen
    16.7 +    Copyright	2000  University of Cambridge
    16.8 +*)
    16.9 +
   16.10 +WilsonRuss = EulerFermat +
   16.11 +
   16.12 +consts
   16.13 +  inv    :: "[int,int] => int" 
   16.14 +  wset   :: "int*int=>int set"
   16.15 +
   16.16 +defs
   16.17 +  inv_def   "inv p a == (a ^ (nat (p - #2))) mod p"
   16.18 +
   16.19 +recdef wset "measure ((%(a,p).(nat a)) ::int*int=>nat)"
   16.20 +    "wset (a,p) = (if #1<a then let ws = wset (a-#1,p) in
   16.21 +                     (if a:ws then ws else insert a (insert (inv p a) ws))
   16.22 +                   else {})"
   16.23 +
   16.24 +end