--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/NumberTheory/BijectionRel.ML Thu Aug 03 10:46:01 2000 +0200
@@ -0,0 +1,182 @@
+(* Title: BijectionRel.ML
+ ID: $Id$
+ Author: Thomas M. Rasmussen
+ Copyright 2000 University of Cambridge
+
+Inductive definitions of bijections between two different sets and
+ between the same set.
+Theorem for relating the two definitions
+*)
+
+
+(***** bijR *****)
+
+Addsimps [bijR.empty];
+
+Goal "(A,B) : (bijR P) ==> finite A";
+by (etac bijR.induct 1);
+by Auto_tac;
+qed "fin_bijRl";
+
+Goal "(A,B) : (bijR P) ==> finite B";
+by (etac bijR.induct 1);
+by Auto_tac;
+qed "fin_bijRr";
+
+val major::subs::prems =
+Goal "[| finite F; F <= A; P({}); \
+\ !!F a. [| F <= A; a:A; a ~: F; P(F) |] ==> P(insert a F) |] \
+\ ==> P(F)";
+by (rtac (subs RS rev_mp) 1);
+by (rtac (major RS finite_induct) 1);
+by (ALLGOALS (blast_tac (claset() addIs prems)));
+val lemma_induct = result();
+
+Goalw [inj_on_def]
+ "[| A <= B; a ~: A ; a : B; inj_on f B |] ==> (f a) ~: f``A";
+by Auto_tac;
+val lemma = result();
+
+Goal "[| ALL a. a:A --> P a (f a); inj_on f A; finite A; F <= A |] \
+\ ==> (F,f``F) : bijR P";
+by (res_inst_tac [("F","F"),("A","A")] lemma_induct 1);
+by (rtac finite_subset 1);
+by Auto_tac;
+by (rtac bijR.insert 1);
+by (rtac lemma 3);
+by Auto_tac;
+val lemma = result();
+
+Goal "[| ALL a. a:A --> P a (f a); inj_on f A; finite A |] \
+\ ==> (A,f``A) : bijR P";
+by (rtac lemma 1);
+by Auto_tac;
+qed "inj_func_bijR";
+
+
+(***** bijER *****)
+
+Addsimps [bijER.empty];
+
+Goal "A : bijER P ==> finite A";
+by (etac bijER.induct 1);
+by Auto_tac;
+qed "fin_bijER";
+
+Goal "[| a ~: A; a ~: B; F <= insert a A; F <= insert a B; a : F |] \
+\ ==> (EX C. F = insert a C & a ~: C & C <= A & C <= B)";
+by (res_inst_tac [("x","F-{a}")] exI 1);
+by Auto_tac;
+val lemma1 = result();
+
+Goal "[| a ~= b; a ~: A; b ~: B; a : F; b : F; \
+\ F <= insert a A; F <= insert b B |] \
+\ ==> (EX C. F = insert a (insert b C) & a ~: C & b ~: C & \
+\ C <= A & C <= B)";
+by (res_inst_tac [("x","F-{a,b}")] exI 1);
+by Auto_tac;
+val lemma2 = result();
+
+Goalw [uniqP_def] "[| uniqP P; P a b; P c d |] ==> (a=c) = (b=d)";
+by Auto_tac;
+val lemma_uniq = result();
+
+Goalw [symP_def] "symP P ==> (P a b) = (P b a)";
+by Auto_tac;
+val lemma_sym = result();
+
+Goalw [bijP_def]
+ "[| uniqP P; b ~: C; P b b; bijP P (insert b C) |] ==> bijP P C";
+by Auto_tac;
+by (subgoal_tac "b~=a" 1);
+by (Clarify_tac 2);
+by (asm_full_simp_tac (simpset() addsimps [lemma_uniq]) 1);
+by Auto_tac;
+val lemma_in1 = result();
+
+Goalw [bijP_def]
+ "[| symP P; uniqP P; a ~: C; b ~: C; a ~= b; P a b; \
+\ bijP P (insert a (insert b C)) |] ==> bijP P C";
+by Auto_tac;
+by (subgoal_tac "aa~=a" 1);
+by (Clarify_tac 2);
+by (subgoal_tac "aa~=b" 1);
+by (Clarify_tac 2);
+by (asm_full_simp_tac (simpset() addsimps [lemma_uniq]) 1);
+by (subgoal_tac "ba~=a" 1);
+by Auto_tac;
+by (subgoal_tac "P a aa" 1);
+by (asm_simp_tac (simpset() addsimps [lemma_sym]) 2);
+by (subgoal_tac "b=aa" 1);
+by (rtac iffD1 2);
+by (res_inst_tac [("a","a"),("c","a"),("P","P")] lemma_uniq 2);
+by Auto_tac;
+val lemma_in2 = result();
+
+Goal "[| ALL a b. Q a & P a b --> R b; P a b; Q a |] ==> R b";
+by Auto_tac;
+val lemma = result();
+
+Goalw [bijP_def] "[| bijP P F; symP P; P a b |] ==> (a:F) = (b:F)";
+by (rtac iffI 1);
+by (ALLGOALS (etac lemma));
+by (ALLGOALS Asm_simp_tac);
+by (rtac iffD2 1);
+by (res_inst_tac [("P","P")] lemma_sym 1);
+by (ALLGOALS Asm_simp_tac);
+val lemma_bij = result();
+
+Goal "[| (A,B) : bijR P; uniqP P; symP P |] \
+\ ==> (ALL F. (bijP P F) & F<=A & F<=B --> F : bijER P)";
+by (etac bijR.induct 1);
+by (Simp_tac 1);
+by (case_tac "a=b" 1);
+by (Clarify_tac 1);
+by (case_tac "b:F" 1);
+by (rotate_tac ~1 2);
+by (asm_full_simp_tac (simpset() addsimps [subset_insert]) 2);
+by (cut_inst_tac [("F","F"),("a","b"),("A","A"),("B","B")] lemma1 1);
+by (Clarify_tac 6);
+by (rtac bijER.insert1 6);
+by (ALLGOALS Asm_full_simp_tac);
+by (subgoal_tac "bijP P C" 1);
+by (Asm_full_simp_tac 1);
+by (rtac lemma_in1 1);
+by (ALLGOALS Asm_simp_tac);
+by (Clarify_tac 1);
+by (case_tac "a:F" 1);
+by (ALLGOALS (case_tac "b:F"));
+by (rotate_tac ~2 4);
+by (asm_full_simp_tac (simpset() addsimps [subset_insert]) 4);
+by (rotate_tac ~2 3);
+by (asm_full_simp_tac (simpset() addsimps [subset_insert]) 3);
+by (rotate_tac ~2 2);
+by (asm_full_simp_tac (simpset() addsimps [subset_insert]) 2);
+by (cut_inst_tac [("F","F"),("a","a"),("b","b"),("A","A"),("B","B")]
+ lemma2 1);
+by (ALLGOALS Asm_simp_tac);
+by (Clarify_tac 1);
+by (rtac bijER.insert2 1);
+by (ALLGOALS Asm_simp_tac);
+by (subgoal_tac "bijP P C" 1);
+by (Asm_full_simp_tac 1);
+by (rtac lemma_in2 1);
+by (ALLGOALS Asm_simp_tac);
+by (subgoal_tac "b:F" 1);
+by (rtac iffD1 2);
+by (res_inst_tac [("a","a"),("F","F"),("P","P")] lemma_bij 2);
+by (ALLGOALS Asm_simp_tac);
+by (subgoal_tac "a:F" 2);
+by (rtac iffD2 3);
+by (res_inst_tac [("b","b"),("F","F"),("P","P")] lemma_bij 3);
+by Auto_tac;
+val lemma_bijRER = result();
+
+Goal "[| (A,A) : bijR P; (bijP P A); uniqP P; symP P |] ==> A : bijER P";
+by (cut_inst_tac [("A","A"),("B","A"),("P","P")] lemma_bijRER 1);
+by Auto_tac;
+qed "bijR_bijER";
+
+
+
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/NumberTheory/BijectionRel.thy Thu Aug 03 10:46:01 2000 +0200
@@ -0,0 +1,46 @@
+(* Title: BijectionRel.thy
+ ID: $Id$
+ Author: Thomas M. Rasmussen
+ Copyright 2000 University of Cambridge
+*)
+
+BijectionRel = Main +
+
+consts
+ bijR :: "(['a, 'b] => bool) => ('a set * 'b set) set"
+
+inductive "bijR P"
+intrs
+ empty "({},{}) : bijR P"
+ insert "[| P a b; a ~: A; b ~: B; (A,B) : bijR P |] \
+\ ==> (insert a A, insert b B) : bijR P"
+
+(* Add extra condition to insert: ALL b:B. ~(P a b) (and similar for A) *)
+
+consts
+ bijP :: "(['a, 'a] => bool) => 'a set => bool"
+
+defs
+ bijP_def "bijP P F == (ALL a b. a:F & P a b --> b:F)"
+
+consts
+ uniqP :: "(['a, 'a] => bool) => bool"
+ symP :: "(['a, 'a] => bool) => bool"
+
+defs
+ uniqP_def "uniqP P == (ALL a b c d. P a b & P c d --> (a=c) = (b=d))"
+ symP_def "symP P == (ALL a b. (P a b) = (P b a))"
+
+consts
+ bijER :: "(['a, 'a] => bool) => 'a set set"
+
+inductive "bijER P"
+intrs
+ empty "{} : bijER P"
+ insert1 "[| P a a; a ~: A; A : bijER P |] \
+\ ==> (insert a A) : bijER P"
+ insert2 "[| P a b; a ~= b; a ~: A; b ~: A; A : bijER P |] \
+\ ==> (insert a (insert b A)) : bijER P"
+
+end
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/NumberTheory/Chinese.ML Thu Aug 03 10:46:01 2000 +0200
@@ -0,0 +1,232 @@
+(* Title: Chinese.ML
+ ID: $Id$
+ Author: Thomas M. Rasmussen
+ Copyright 2000 University of Cambridge
+
+The Chinese Remainder Theorem for an arbitrary finite number of equations.
+(The one-equation case is included in 'IntPrimes')
+
+Uses functions for indexing. Maybe 'funprod' and 'funsum'
+should be based on general 'fold' on indices?
+*)
+
+
+(*** extra nat theorems ***)
+
+Goal "[| k <= i; i <= k |] ==> i = (k::nat)";
+by (rtac diffs0_imp_equal 1);
+by (ALLGOALS (stac diff_is_0_eq));
+by Auto_tac;
+qed "le_le_imp_eq";
+
+Goal "m~=n --> m<=n --> m<(n::nat)";
+by (induct_tac "n" 1);
+by Auto_tac;
+by (subgoal_tac "m = Suc n" 1);
+by (rtac le_le_imp_eq 2);
+by Auto_tac;
+qed_spec_mp "neq_le_imp_less";
+
+
+(*** funprod and funsum ***)
+
+Goal "(ALL i. i <= n --> #0 < mf i) --> #0 < funprod mf 0 n";
+by (induct_tac "n" 1);
+by Auto_tac;
+by (asm_full_simp_tac (simpset() addsimps [int_0_less_mult_iff]) 1);
+qed_spec_mp "funprod_pos";
+
+Goal "(ALL i. k<=i & i<=(k+l) --> zgcd (mf i, mf m) = #1) --> \
+\ #0 < mf m --> zgcd (funprod mf k l, mf m) = #1";
+by (induct_tac "l" 1);
+by (ALLGOALS Simp_tac);
+by (REPEAT (rtac impI 1));
+by (stac zgcd_zmult_cancel 1);
+by Auto_tac;
+qed_spec_mp "funprod_zgcd";
+
+Goal "k<=i --> i<=(k+l) --> (mf i) dvd (funprod mf k l)";
+by (induct_tac "l" 1);
+by Auto_tac;
+by (rtac zdvd_zmult2 2);
+by (rtac zdvd_zmult 3);
+by (subgoal_tac "i=k" 1);
+by (subgoal_tac "i=Suc (k + n)" 3);
+by (ALLGOALS Asm_simp_tac);
+qed_spec_mp "funprod_zdvd";
+
+Goal "(funsum f k l) mod m = (funsum (%i. (f i) mod m) k l) mod m";
+by (induct_tac "l" 1);
+by Auto_tac;
+by (rtac trans 1);
+by (rtac zmod_zadd1_eq 1);
+by (Asm_simp_tac 1);
+by (rtac (zmod_zadd_right_eq RS sym) 1);
+qed "funsum_mod";
+
+Goal "(ALL i. k<=i & i<=(k+l) --> (f i) = #0) --> (funsum f k l) = #0";
+by (induct_tac "l" 1);
+by Auto_tac;
+qed_spec_mp "funsum_zero";
+
+Goal "k<=j --> j<=(k+l) --> \
+\ (ALL i. k<=i & i<=(k+l) & i~=j --> (f i) = #0) --> \
+\ (funsum f k l) = (f j)";
+by (induct_tac "l" 1);
+by (ALLGOALS Simp_tac);
+by (ALLGOALS (REPEAT o (rtac impI)));
+by (case_tac "Suc (k+n) = j" 2);
+by (subgoal_tac "funsum f k n = #0" 2);
+by (rtac funsum_zero 3);
+by (subgoal_tac "f (Suc (k+n)) = #0" 4);
+by (subgoal_tac "k=j" 1);
+by (Clarify_tac 4);
+by (subgoal_tac "j<=k+n" 5);
+by (subgoal_tac "j<Suc (k+n)" 6);
+by (rtac neq_le_imp_less 7);
+by (ALLGOALS Asm_simp_tac);
+by Auto_tac;
+qed_spec_mp "funsum_oneelem";
+
+
+(*** Chinese: Uniqueness ***)
+
+Goalw [m_cond_def,km_cond_def,lincong_sol_def]
+ "[| m_cond n mf; km_cond n kf mf; \
+\ lincong_sol n kf bf mf x; lincong_sol n kf bf mf y |] \
+\ ==> [x=y] (mod mf n)";
+by (rtac iffD1 1);
+by (res_inst_tac [("k","kf n")] zcong_cancel2 1);
+by (res_inst_tac [("b","bf n")] zcong_trans 3);
+by (stac zcong_sym 4);
+by (rtac zless_imp_zle 1);
+by (ALLGOALS Asm_simp_tac);
+val lemma = result();
+
+Goal "m_cond n mf --> km_cond n kf mf --> \
+\ lincong_sol n kf bf mf x --> lincong_sol n kf bf mf y --> \
+\ [x=y] (mod funprod mf 0 n)";
+by (induct_tac "n" 1);
+by (ALLGOALS Simp_tac);
+by (blast_tac (claset() addIs [lemma]) 1);
+by (REPEAT (rtac impI 1));
+by (rtac zcong_zgcd_zmult_zmod 1);
+by (blast_tac (claset() addIs [lemma]) 3);
+by (stac zgcd_commute 4);
+by (rtac funprod_zgcd 6);
+by (rtac funprod_pos 5);
+by (rtac funprod_pos 2);
+by (rewrite_goals_tac [m_cond_def,km_cond_def,lincong_sol_def]);
+by Auto_tac;
+qed_spec_mp "zcong_funprod";
+
+
+(* Chinese: Existence *)
+
+Goal "[| 0<n; i<n |] ==> Suc (i+(n-Suc(i))) = n";
+by (subgoal_tac "Suc (i+(n-1-i)) = n" 1);
+by (stac le_add_diff_inverse 2);
+by (stac le_pred_eq 2);
+by Auto_tac;
+val suclemma = result();
+
+Goal "[| 0<n; i<=n; m_cond n mf; km_cond n kf mf |] \
+\ ==> EX! x. #0<=x & x<(mf i) & \
+\ [(kf i)*(mhf mf n i)*x = bf i] (mod mf i)";
+by (rtac zcong_lineq_unique 1);
+by (stac zgcd_zmult_cancel 2);
+by (rewrite_goals_tac [m_cond_def,km_cond_def,mhf_def]);
+by (case_tac "i=0" 4);
+by (case_tac "i=n" 5);
+by (ALLGOALS Asm_simp_tac);
+by (stac zgcd_zmult_cancel 3);
+by (Asm_simp_tac 3);
+by (ALLGOALS (rtac funprod_zgcd));
+by Safe_tac;
+by (ALLGOALS Asm_full_simp_tac);
+by (subgoal_tac "i<=n" 1);
+by (res_inst_tac [("j","n-1")] le_trans 2);
+by (subgoal_tac "i~=n" 1);
+by (subgoal_tac "ia<=n" 5);
+by (res_inst_tac [("j","i-1")] le_trans 6);
+by (res_inst_tac [("j","n-1")] le_trans 7);
+by (subgoal_tac "ia~=i" 5);
+by (subgoal_tac "ia<=n" 10);
+by (stac (suclemma RS sym) 11);
+by (assume_tac 13);
+by (rtac neq_le_imp_less 12);
+by (rtac diff_le_mono 8);
+by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [le_pred_eq])));
+qed "unique_xi_sol";
+
+Goalw [mhf_def] "[| 0<n; i<=n; j<=n; j~=i |] ==> (mf j) dvd (mhf mf n i)";
+by (case_tac "i=0" 1);
+by (case_tac "i=n" 2);
+by (ALLGOALS Asm_simp_tac);
+by (case_tac "j<i" 3);
+by (rtac zdvd_zmult2 3);
+by (rtac zdvd_zmult 4);
+by (ALLGOALS (rtac funprod_zdvd));
+by Auto_tac;
+by (stac suclemma 4);
+by (stac le_pred_eq 2);
+by (stac le_pred_eq 1);
+by (rtac neq_le_imp_less 2);
+by (rtac neq_le_imp_less 8);
+by (rtac pred_less_imp_le 6);
+by (rtac neq_le_imp_less 6);
+by Auto_tac;
+val lemma = result();
+
+Goalw [x_sol_def] "[| 0<n; i<=n |] \
+\ ==> (x_sol n kf bf mf) mod (mf i) = \
+\ (xilin_sol i n kf bf mf)*(mhf mf n i) mod (mf i)";
+by (stac funsum_mod 1);
+by (stac funsum_oneelem 1);
+by Auto_tac;
+by (stac (zdvd_iff_zmod_eq_0 RS sym) 1);
+by (rtac zdvd_zmult 1);
+by (rtac lemma 1);
+by Auto_tac;
+qed "x_sol_lin";
+
+
+(* Chinese *)
+
+Goal "EX! a. P a ==> P (@ a. P a)";
+by Auto_tac;
+by (stac select_equality 1);
+by Auto_tac;
+val delemma = result();
+
+Goal "[| 0<n; m_cond n mf; km_cond n kf mf |] \
+\ ==> (EX! x. #0 <= x & x < (funprod mf 0 n) & \
+\ (lincong_sol n kf bf mf x))";
+by Safe_tac;
+by (res_inst_tac [("m","funprod mf 0 n")] zcong_zless_imp_eq 2);
+by (rtac zcong_funprod 6);
+by Auto_tac;
+by (res_inst_tac [("x","(x_sol n kf bf mf) mod (funprod mf 0 n)")] exI 1);
+by (rewtac lincong_sol_def);
+by Safe_tac;
+by (stac zcong_zmod 3);
+by (stac zmod_zmult_distrib 3);
+by (stac zmod_zdvd_zmod 3);
+by (stac x_sol_lin 5);
+by (stac (zmod_zmult_distrib RS sym) 7);
+by (stac (zcong_zmod RS sym) 7);
+by (subgoal_tac "#0<=(xilin_sol i n kf bf mf) & \
+\ (xilin_sol i n kf bf mf)<(mf i) & \
+\ [(kf i)*(mhf mf n i)*(xilin_sol i n kf bf mf) = bf i] \
+\ (mod mf i)" 7);
+by (asm_full_simp_tac (simpset() addsimps zmult_ac) 7);
+by (rewtac xilin_sol_def);
+by (Asm_simp_tac 7);
+by (rtac delemma 7);
+by (rtac unique_xi_sol 7);
+by (rtac funprod_zdvd 4);
+by (rewtac m_cond_def);
+by (rtac (funprod_pos RS pos_mod_sign) 1);
+by (rtac (funprod_pos RS pos_mod_bound) 2);
+by Auto_tac;
+qed "chinese_remainder";
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/NumberTheory/Chinese.thy Thu Aug 03 10:46:01 2000 +0200
@@ -0,0 +1,55 @@
+(* Title: Chinese.thy
+ ID: $Id$
+ Author: Thomas M. Rasmussen
+ Copyright 2000 University of Cambridge
+*)
+
+Chinese = IntPrimes +
+
+consts
+ funprod :: (nat => int) => nat => nat => int
+ funsum :: (nat => int) => nat => nat => int
+
+primrec
+ "funprod f i 0 = f i"
+ "funprod f i (Suc n) = (f (Suc (i+n)))*(funprod f i n)"
+
+primrec
+ "funsum f i 0 = f i"
+ "funsum f i (Suc n) = (f (Suc (i+n)))+(funsum f i n)"
+
+
+consts
+ m_cond :: [nat,nat => int] => bool
+ km_cond :: [nat,nat => int,nat => int] => bool
+ lincong_sol :: [nat,nat => int,nat => int,nat => int,int] => bool
+
+ mhf :: (nat => int) => nat => nat => int
+ xilin_sol :: [nat,nat,nat => int,nat => int,nat => int] => int
+ x_sol :: [nat,nat => int,nat => int,nat => int] => int
+
+defs
+ m_cond_def "m_cond n mf ==
+ (ALL i. i<=n --> #0 < mf i) &
+ (ALL i j. i<=n & j<=n & i ~= j --> zgcd(mf i,mf j) = #1)"
+
+ km_cond_def "km_cond n kf mf == (ALL i. i<=n --> zgcd(kf i,mf i) = #1)"
+
+ lincong_sol_def "lincong_sol n kf bf mf x ==
+ (ALL i. i<=n --> zcong ((kf i)*x) (bf i) (mf i))"
+
+ mhf_def "mhf mf n i == (if i=0 then (funprod mf 1 (n-1))
+ else (if i=n then (funprod mf 0 (n-1))
+ else ((funprod mf 0 (i-1)) *
+ (funprod mf (i+1) (n-1-i)))))"
+
+ xilin_sol_def "xilin_sol i n kf bf mf ==
+ (if 0<n & i<=n & m_cond n mf & km_cond n kf mf then
+ (@ x. #0<=x & x<(mf i) &
+ zcong ((kf i)*(mhf mf n i)*x) (bf i) (mf i))
+ else #0)"
+
+ x_sol_def "x_sol n kf bf mf ==
+ (funsum (%i. (xilin_sol i n kf bf mf)*(mhf mf n i)) 0 n)"
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/NumberTheory/EulerFermat.ML Thu Aug 03 10:46:01 2000 +0200
@@ -0,0 +1,308 @@
+(* Title: EulerFermat.ML
+ ID: $Id$
+ Author: Thomas M. Rasmussen
+ Copyright 2000 University of Cambridge
+
+Fermat's Little Theorem extended to Euler's Totient function.
+More abstract approach than Boyer-Moore (which seems necessary
+to achieve the extended version)
+*)
+
+
+(*** norRRset ***)
+
+Addsimps [RsetR.empty];
+
+val [BnorRset_eq] = BnorRset.simps;
+Delsimps BnorRset.simps;
+
+val [prem1,prem2] =
+Goal "[| !! a m. P {} a m; \
+\ (!!a m. [| #0 < (a::int); P (BnorRset(a-#1,m::int)) (a-#1) m |] \
+\ ==> P (BnorRset(a,m)) a m) |] \
+\ ==> P (BnorRset(u,v)) u v";
+by (rtac BnorRset.induct 1);
+by Safe_tac;
+by (case_tac "#0<a" 2);
+by (rtac prem2 2);
+by (ALLGOALS Asm_simp_tac);
+by (ALLGOALS (asm_simp_tac (simpset() addsimps [BnorRset_eq,prem1])));
+qed "BnorRset_induct";
+
+Goal "b:BnorRset(a,m) --> b<=a";
+by (res_inst_tac [("u","a"),("v","m")] BnorRset_induct 1);
+by (stac BnorRset_eq 2);
+by (rewtac Let_def);
+by Auto_tac;
+qed_spec_mp "Bnor_mem_zle";
+
+Goal "a<b ==> b~:BnorRset(a,m)";
+by (res_inst_tac [("Pa","b<=a")] swap 1);
+by (rtac Bnor_mem_zle 2);
+by Auto_tac;
+qed "Bnor_mem_zle_swap";
+
+Goal "b:BnorRset(a,m) --> #0<b";
+by (res_inst_tac [("u","a"),("v","m")] BnorRset_induct 1);
+by (stac BnorRset_eq 2);
+by (rewtac Let_def);
+by Auto_tac;
+qed_spec_mp "Bnor_mem_zg";
+
+Goal "zgcd(b,m) = #1 --> #0<b --> b<=a --> b:BnorRset(a,m)";
+by (res_inst_tac [("u","a"),("v","m")] BnorRset.induct 1);
+by Auto_tac;
+by (case_tac "a=b" 1);
+by (asm_full_simp_tac (simpset() addsimps [zle_neq_implies_zless]) 2);
+by (Asm_simp_tac 1);
+by (ALLGOALS (stac BnorRset_eq));
+by (rewtac Let_def);
+by Auto_tac;
+qed_spec_mp "Bnor_mem_if";
+
+Goal "a<m --> BnorRset (a,m) : RsetR m";
+by (res_inst_tac [("u","a"),("v","m")] BnorRset_induct 1);
+by (Simp_tac 1);
+by (stac BnorRset_eq 1);
+by (rewtac Let_def);
+by Auto_tac;
+by (rtac RsetR.insert 1);
+by (rtac allI 3);
+by (rtac impI 3);
+by (rtac zcong_not 3);
+by (subgoal_tac "a' <= a-#1" 6);
+by (rtac Bnor_mem_zle 7);
+by (rtac Bnor_mem_zg 5);
+by Auto_tac;
+qed_spec_mp "Bnor_in_RsetR";
+
+Goal "finite (BnorRset (a,m))";
+by (res_inst_tac [("u","a"),("v","m")] BnorRset_induct 1);
+by (stac BnorRset_eq 2);
+by (rewtac Let_def);
+by Auto_tac;
+qed "Bnor_fin";
+
+Goal "a <= b - #1 ==> a < (b::int)";
+by Auto_tac;
+val lemma = result();
+
+Goalw [norRRset_def]
+ "[| #1<m; zgcd(a,m) = #1 |] ==> (EX! b. [a = b](mod m) & b:(norRRset m))";
+by (cut_inst_tac [("a","a"),("m","m")] zcong_zless_unique 1);
+by Auto_tac;
+by (res_inst_tac [("m","m")] zcong_zless_imp_eq 2);
+by (auto_tac (claset() addIs [Bnor_mem_zle,Bnor_mem_zg,zcong_trans,
+ zless_imp_zle,lemma],
+ simpset() addsimps [zcong_sym]));
+by (res_inst_tac [("x","b")] exI 1);
+by Safe_tac;
+by (rtac Bnor_mem_if 1);
+by (case_tac "b=#0" 2);
+by (auto_tac (claset() addIs [zle_neq_implies_zless], simpset()));
+by (SELECT_GOAL (rewtac zcong_def) 2);
+by (subgoal_tac "zgcd(a,m) = m" 2);
+by (stac (zdvd_iff_zgcd RS sym) 3);
+by (rtac zgcd_zcong_zgcd 1);
+by (ALLGOALS (asm_full_simp_tac (simpset()
+ addsimps [zdvd_zminus_iff,zcong_sym])));
+qed "norR_mem_unique";
+
+
+(*** noXRRset ***)
+
+Goalw [is_RRset_def]
+ "[| #0<m; is_RRset A m; #0<m |] ==> a:A --> zgcd (a,m) = #1";
+by (rtac RsetR.induct 1);
+by Auto_tac;
+qed_spec_mp "RRset_gcd";
+
+Goal "[| A : RsetR m; #0<m; zgcd (x, m) = #1 |] ==> (%a. a*x)``A : RsetR m";
+by (etac RsetR.induct 1);
+by (ALLGOALS Simp_tac);
+by (rtac RsetR.insert 1);
+by Auto_tac;
+by (asm_full_simp_tac (simpset() addsimps [zcong_cancel]) 2);
+by (blast_tac (claset() addIs [zgcd_zgcd_zmult]) 1);
+qed "RsetR_zmult_mono";
+
+Goalw [norRRset_def,noXRRset_def]
+ "[| #0<m; zgcd(x,m) = #1 |] \
+\ ==> card (noXRRset m x) = card (norRRset m)";
+by (rtac card_image 1);
+by (rewtac inj_on_def);
+by (auto_tac (claset(),simpset() addsimps [Bnor_fin]));
+by (case_tac "x=#0" 1);
+by (asm_full_simp_tac (simpset() addsimps [BnorRset_eq]) 1);
+by (stac (zmult_cancel2 RS sym) 1);
+by (ALLGOALS Asm_simp_tac);
+qed "card_nor_eq_noX";
+
+Goalw [is_RRset_def,phi_def]
+ "[| #0<m; zgcd(x,m) = #1 |] ==> is_RRset (noXRRset m x) m";
+by (auto_tac (claset(),simpset() addsimps [card_nor_eq_noX]));
+by (rewrite_goals_tac [noXRRset_def,norRRset_def]);
+by (rtac RsetR_zmult_mono 1);
+by (rtac Bnor_in_RsetR 1);
+by (ALLGOALS Asm_simp_tac);
+qed "noX_is_RRset";
+
+Goal "EX! a. P a ==> P (@ a. P a)";
+by Auto_tac;
+by (stac select_equality 1);
+by Auto_tac;
+val lemma = result();
+
+Goal "[| #1<m; is_RRset A m; a:A |] \
+\ ==> zcong a (@ b. [a = b](mod m) & b : norRRset m) m & \
+\ (@ b. [a = b](mod m) & b : norRRset m) : norRRset m";
+by (rtac lemma 1);
+by (rtac norR_mem_unique 1);
+by (rtac RRset_gcd 2);
+by (ALLGOALS Asm_simp_tac);
+val lemma_some = result();
+
+Goalw [RRset2norRR_def]
+ "[| #1<m; is_RRset A m; a:A |] \
+\ ==> zcong a (RRset2norRR A m a) m & \
+\ (RRset2norRR A m a):(norRRset m)";
+by (Asm_simp_tac 1);
+by (rtac lemma_some 1);
+by (ALLGOALS Asm_simp_tac);
+qed "RRset2norRR_correct";
+
+bind_thm ("RRset2norRR_correct1", RRset2norRR_correct RS conjunct1);
+bind_thm ("RRset2norRR_correct2", RRset2norRR_correct RS conjunct2);
+
+Goal "A : (RsetR m) ==> finite A";
+by (etac RsetR.induct 1);
+by Auto_tac;
+qed "RsetR_fin";
+
+Goalw [is_RRset_def]
+ "[| #1<m; is_RRset A m; [a = b](mod m) |] ==> a:A --> b:A --> a = b";
+by (rtac RsetR.induct 1);
+by (auto_tac (claset(), simpset() addsimps [zcong_sym]));
+qed_spec_mp "RRset_zcong_eq";
+
+Goal "[| P (@ a. P a); Q (@ a. Q a); (@ a. P a) = (@ a. Q a) |] \
+\ ==> (EX a. P a & Q a)";
+by Auto_tac;
+val lemma = result();
+
+Goalw [RRset2norRR_def,inj_on_def]
+ "[| #1<m; is_RRset A m |] ==> inj_on (RRset2norRR A m) A";
+by Auto_tac;
+by (subgoal_tac "(EX b. ([x = b](mod m) & b : norRRset m) & \
+\ ([y = b](mod m) & b : norRRset m))" 1);
+by (rtac lemma 2);
+by (rtac lemma_some 3);
+by (rtac lemma_some 2);
+by (rtac RRset_zcong_eq 1);
+by Auto_tac;
+by (res_inst_tac [("b","b")] zcong_trans 1);
+by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [zcong_sym])));
+qed "RRset2norRR_inj";
+
+Goal "[| #1<m; is_RRset A m |] ==> (RRset2norRR A m)``A = (norRRset m)";
+by (rtac card_seteq 1);
+by (stac card_image 3);
+by (rtac RRset2norRR_inj 4);
+by Auto_tac;
+by (rtac RRset2norRR_correct2 2);
+by Auto_tac;
+by (rewrite_goals_tac [is_RRset_def,phi_def,norRRset_def]);
+by (auto_tac (claset(),simpset() addsimps [RsetR_fin,Bnor_fin]));
+qed "RRset2norRR_eq_norR";
+
+Goalw [inj_on_def] "[| a ~: A ; inj f |] ==> (f a) ~: f``A";
+by Auto_tac;
+val lemma = result();
+
+Goal "x~=#0 ==> a<m --> setprod ((%a. a*x) `` BnorRset(a,m)) = \
+\ setprod (BnorRset(a,m)) * x^card(BnorRset(a,m))";
+by (res_inst_tac [("u","a"),("v","m")] BnorRset_induct 1);
+by (stac BnorRset_eq 2);
+by (rewtac Let_def);
+by Auto_tac;
+by (asm_simp_tac (simpset() addsimps [Bnor_fin,Bnor_mem_zle_swap]) 1);
+by (stac setprod_insert 1);
+by (rtac lemma 2);
+by (rewtac inj_on_def);
+by (ALLGOALS (asm_full_simp_tac (simpset()
+ addsimps zmult_ac@[Bnor_fin,finite_imageI,Bnor_mem_zle_swap])));
+qed_spec_mp "Bnor_prod_power";
+
+
+(*** Fermat ***)
+
+Goalw [zcongm_def]
+ "(A,B) : bijR (zcongm m) ==> [setprod A = setprod B](mod m)";
+by (etac bijR.induct 1);
+by (subgoal_tac "a~:A & b~:B & finite A & finite B" 2);
+by (auto_tac (claset() addIs [fin_bijRl,fin_bijRr,zcong_zmult],
+ simpset()));
+qed "bijzcong_zcong_prod";
+
+Goalw [norRRset_def,phi_def]
+ "#0<m --> a<m --> zgcd (setprod (BnorRset (a,m)),m) = #1";
+by (res_inst_tac [("u","a"),("v","m")] BnorRset_induct 1);
+by (stac BnorRset_eq 2);
+by (rewtac Let_def);
+by Auto_tac;
+by (asm_simp_tac (simpset() addsimps [Bnor_fin,Bnor_mem_zle_swap]) 1);
+by (blast_tac (claset() addIs [zgcd_zgcd_zmult]) 1);
+qed_spec_mp "Bnor_prod_zgcd";
+
+Goalw [norRRset_def,phi_def]
+ "[| #0<m; zgcd(x,m) = #1 |] ==> zcong (x^phi(m)) #1 m";
+by (case_tac "x=#0" 1);
+by (case_tac "m=#1" 2);
+by (rtac iffD1 3);
+by (res_inst_tac [("k","setprod (BnorRset (m-#1,m))")] zcong_cancel2 3);
+by (stac (Bnor_prod_power RS sym) 5);
+by (rtac Bnor_prod_zgcd 4);
+by (ALLGOALS Asm_full_simp_tac);
+by (rtac bijzcong_zcong_prod 1);
+by (fold_goals_tac [norRRset_def,noXRRset_def]);
+by (stac (RRset2norRR_eq_norR RS sym) 1);
+by (rtac inj_func_bijR 3);
+by Auto_tac;
+by (rewtac zcongm_def);
+by (rtac RRset2norRR_correct1 3);
+by (rtac RRset2norRR_inj 6);
+by (auto_tac (claset() addIs [zle_neq_implies_zless],
+ simpset() addsimps [noX_is_RRset]));
+by (rewrite_goals_tac [noXRRset_def,norRRset_def]);
+by (rtac finite_imageI 1);
+by (rtac Bnor_fin 1);
+qed "EulerFermatTheorem";
+
+Goalw [zprime_def]
+ "p:zprime ==> a<p --> (ALL b. #0<b & b<=a --> zgcd(b,p) = #1) \
+\ --> card (BnorRset(a, p)) = nat a";
+by (res_inst_tac [("u","a"),("v","p")] BnorRset.induct 1);
+by (stac BnorRset_eq 1);
+by (rewtac Let_def);
+by Auto_tac;
+by (asm_simp_tac (simpset() addsimps [Bnor_mem_zle_swap,Bnor_fin]) 1);
+by (stac (int_int_eq RS sym) 1);
+by Auto_tac;
+qed_spec_mp "Bnor_prime";
+
+Goalw [phi_def,norRRset_def]
+ "p:zprime ==> phi(p) = nat (p-#1)";
+by (rtac Bnor_prime 1);
+by Auto_tac;
+by (etac zless_zprime_imp_zrelprime 1);
+by (ALLGOALS Asm_simp_tac);
+qed "phi_prime";
+
+Goal "[| p:zprime; ~p dvd x |] ==> zcong (x^(nat (p-#1))) #1 p";
+by (stac (phi_prime RS sym) 1);
+by (rtac EulerFermatTheorem 2);
+by (etac zprime_imp_zrelprime 3);
+by (rewtac zprime_def);
+by Auto_tac;
+qed "Little_Fermat";
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/NumberTheory/EulerFermat.thy Thu Aug 03 10:46:01 2000 +0200
@@ -0,0 +1,46 @@
+(* Title: EulerFermat.thy
+ ID: $Id$
+ Author: Thomas M. Rasmussen
+ Copyright 2000 University of Cambridge
+*)
+
+EulerFermat = BijectionRel + IntFact +
+
+consts
+ RsetR :: "int => int set set"
+ BnorRset :: "int*int=>int set"
+ norRRset :: int => int set
+ noXRRset :: [int, int] => int set
+ phi :: int => nat
+ is_RRset :: [int set, int] => bool
+ RRset2norRR :: [int set, int, int] => int
+
+inductive "RsetR m"
+intrs
+ empty "{} : RsetR m"
+ insert "[| A : RsetR m; zgcd(a,m) = #1; \
+\ ALL a'. a':A --> ~ zcong a a' m |] \
+\ ==> insert a A : RsetR m"
+
+recdef BnorRset "measure ((% (a,m).(nat a)) ::int*int=>nat)"
+ "BnorRset (a,m) = (if #0<a then let na = BnorRset (a-#1,m) in
+ (if zgcd(a,m) = #1 then insert a na else na)
+ else {})"
+
+defs
+ norRRset_def "norRRset m == BnorRset (m-#1,m)"
+
+ noXRRset_def "noXRRset m x == (%a. a*x)``(norRRset m)"
+
+ phi_def "phi m == card (norRRset m)"
+
+ is_RRset_def "is_RRset A m == (A : (RsetR m)) & card(A) = (phi m)"
+
+ RRset2norRR_def "RRset2norRR A m a ==
+ (if #1<m & (is_RRset A m) & a:A
+ then @b. zcong a b m & b:(norRRset m) else #0)"
+
+consts zcongm :: int => [int, int] => bool
+defs zcongm_def "zcongm m == (%a b. zcong a b m)"
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/NumberTheory/IntFact.ML Thu Aug 03 10:46:01 2000 +0200
@@ -0,0 +1,87 @@
+(* Title: IntPowerFact.ML
+ ID: $Id$
+ Author: Thomas M. Rasmussen
+ Copyright 2000 University of Cambridge
+
+Factorial on integers.
+Product of finite set.
+Recursively defined set including all Integers from 2 up to a.
+*)
+
+
+(*---- setprod ----*)
+
+Goalw [setprod_def] "setprod {} = #1";
+by (Simp_tac 1);
+qed "setprod_empty";
+Addsimps [setprod_empty];
+
+Goalw [setprod_def]
+ "[| finite A; a ~: A |] ==> setprod (insert a A) = a * setprod A";
+by (asm_simp_tac (simpset() addsimps [zmult_left_commute,
+ export fold_insert]) 1);
+qed "setprod_insert";
+Addsimps [setprod_insert];
+
+(*---- IntFact ----*)
+
+val [d22set_eq] = d22set.simps;
+Delsimps d22set.simps;
+
+val [prem1,prem2] =
+Goal "[| !!a. P {} a; \
+\ !!a. [| #1<(a::int); P (d22set (a-#1)) (a-#1) |] \
+\ ==> P (d22set a) a |] \
+\ ==> P (d22set u) u";
+by (rtac d22set.induct 1);
+by Safe_tac;
+by (case_tac "#1<a" 2);
+by (rtac prem2 2);
+by (ALLGOALS Asm_simp_tac);
+by (ALLGOALS (asm_simp_tac (simpset() addsimps [d22set_eq,prem1])));
+qed "d22set_induct";
+
+Goal "b:(d22set a) --> #1<b";
+by (res_inst_tac [("u","a")] d22set_induct 1);
+by (stac d22set_eq 2);
+by Auto_tac;
+qed_spec_mp "d22set_g_1";
+
+Goal "b:(d22set a) --> b<=a";
+by (res_inst_tac [("u","a")] d22set_induct 1);
+by (stac d22set_eq 2);
+by Auto_tac;
+qed_spec_mp "d22set_le";
+
+Goal "a<b ==> b~:(d22set a)";
+by (res_inst_tac [("Pa","b<=a")] swap 1);
+by (rtac d22set_le 2);
+by Auto_tac;
+qed "d22set_le_swap";
+
+Goal "#1<b --> b<=a --> b:(d22set a)";
+by (res_inst_tac [("u","a")] d22set.induct 1);
+by Auto_tac;
+by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [d22set_eq])));
+qed_spec_mp "d22set_mem";
+
+Goal "finite (d22set a)";
+by (res_inst_tac [("u","a")] d22set_induct 1);
+by (stac d22set_eq 2);
+by Auto_tac;
+qed "d22set_fin";
+
+val [zfact_eq] = zfact.simps;
+Delsimps zfact.simps;
+
+Goal "setprod(d22set a) = zfact a";
+by (res_inst_tac [("u","a")] d22set.induct 1);
+by Safe_tac;
+by (asm_full_simp_tac (simpset() addsimps [d22set_eq,zfact_eq]) 1);
+by (stac d22set_eq 1);
+by (stac zfact_eq 1);
+by (case_tac "#1<a" 1);
+by (asm_full_simp_tac (simpset() addsimps [d22set_eq,zfact_eq]) 2);
+by (asm_full_simp_tac (simpset() addsimps [d22set_fin,d22set_le_swap]) 1);
+qed "d22set_prod_zfact";
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/NumberTheory/IntFact.thy Thu Aug 03 10:46:01 2000 +0200
@@ -0,0 +1,23 @@
+(* Title: IntFact.thy
+ ID: $Id$
+ Author: Thomas M. Rasmussen
+ Copyright 2000 University of Cambridge
+*)
+
+IntFact = IntPrimes +
+
+consts
+ zfact :: int => int
+ setprod :: int set => int
+ d22set :: int => int set
+
+recdef zfact "measure ((% n.(nat n)) ::int=>nat)"
+ "zfact n = (if n<=#0 then #1 else n*zfact(n-#1))"
+
+defs
+ setprod_def "setprod A == (if finite A then fold (op*) #1 A else #1)"
+
+recdef d22set "measure ((%a.(nat a)) ::int=>nat)"
+ "d22set a = (if #1<a then insert a (d22set (a-#1)) else {})"
+
+end
\ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/NumberTheory/IntPrimes.ML Thu Aug 03 10:46:01 2000 +0200
@@ -0,0 +1,741 @@
+(* Title: IntPrimes.ML
+ ID: $Id$
+ Author: Thomas M. Rasmussen
+ Copyright 2000 University of Cambridge
+
+dvd relation, GCD, Euclid's extended algorithm, primes, congruences
+(all on the Integers)
+
+Comparable to 'Primes' theory but dvd is included here as it is not present in
+'IntDiv'. Also includes extended GCD and congruences not
+present in 'Primes'. Also a few extra theorems concerning 'mod'
+*)
+
+eta_contract:=false;
+
+
+(************************************************)
+(** Divides relation 'dvd' **)
+(************************************************)
+
+Goalw [dvd_def] "(m::int) dvd #0";
+by (blast_tac (claset() addIs [zmult_0_right RS sym]) 1);
+qed "zdvd_0_right";
+AddIffs [zdvd_0_right];
+
+Goalw [dvd_def] "#0 dvd (m::int) ==> m = #0";
+by Auto_tac;
+qed "zdvd_0_left";
+
+Goalw [dvd_def] "#1 dvd (m::int)";
+by (Simp_tac 1);
+qed "zdvd_1_left";
+AddIffs [zdvd_1_left];
+
+Goalw [dvd_def] "m dvd (m::int)";
+by (blast_tac (claset() addIs [zmult_1_right RS sym]) 1);
+qed "zdvd_refl";
+Addsimps [zdvd_refl];
+
+Goalw [dvd_def] "[| m dvd n; n dvd k |] ==> m dvd (k::int)";
+by (blast_tac (claset() addIs [zmult_assoc] ) 1);
+qed "zdvd_trans";
+
+Goalw [dvd_def] "(m dvd -n) = (m dvd (n::int))";
+by Auto_tac;
+by (ALLGOALS (res_inst_tac [("x","-k")] exI));
+by Auto_tac;
+qed "zdvd_zminus_iff";
+
+Goalw [dvd_def] "(-m dvd n) = (m dvd (n::int))";
+by Auto_tac;
+by (ALLGOALS (res_inst_tac [("x","-k")] exI));
+by Auto_tac;
+qed "zdvd_zminus2_iff";
+
+Goalw [dvd_def] "[| #0<m; #0<n; m dvd n; n dvd m |] ==> m = (n::int)";
+by Auto_tac;
+by (asm_full_simp_tac
+ (simpset() addsimps [zmult_assoc,zmult_eq_self_iff,
+ int_0_less_mult_iff, zmult_eq_1_iff]) 1);
+qed "zdvd_anti_sym";
+
+Goalw [dvd_def] "[| k dvd m; k dvd n |] ==> k dvd (m+n :: int)";
+by (blast_tac (claset() addIs [zadd_zmult_distrib2 RS sym]) 1);
+qed "zdvd_zadd";
+
+Goalw [dvd_def] "[| k dvd m; k dvd n |] ==> k dvd (m-n :: int)";
+by (blast_tac (claset() addIs [zdiff_zmult_distrib2 RS sym]) 1);
+qed "zdvd_zdiff";
+
+Goal "[| k dvd (m-n); k dvd n |] ==> k dvd (m::int)";
+by (subgoal_tac "m=n+(m-n)" 1);
+by (etac ssubst 1);
+by (blast_tac (claset() addIs [zdvd_zadd]) 1);
+by (Simp_tac 1);
+qed "zdvd_zdiffD";
+
+Goalw [dvd_def] "k dvd (n::int) ==> k dvd (m*n)";
+by (blast_tac (claset() addIs [zmult_left_commute]) 1);
+qed "zdvd_zmult";
+
+Goal "k dvd (m::int) ==> k dvd (m*n)";
+by (stac zmult_commute 1);
+by (etac zdvd_zmult 1);
+qed "zdvd_zmult2";
+
+(* k dvd (m*k) *)
+AddIffs [zdvd_refl RS zdvd_zmult, zdvd_refl RS zdvd_zmult2];
+
+Goalw [dvd_def] "(j*k) dvd n ==> j dvd (n::int)";
+by (full_simp_tac (simpset() addsimps [zmult_assoc]) 1);
+by (Blast_tac 1);
+qed "zdvd_zmultD2";
+
+Goal "(j*k) dvd n ==> k dvd (n::int)";
+by (rtac zdvd_zmultD2 1);
+by (stac zmult_commute 1);
+by (assume_tac 1);
+qed "zdvd_zmultD";
+
+Goalw [dvd_def] "[| i dvd m; j dvd (n::int) |] ==> (i*j) dvd (m*n)";
+by (Clarify_tac 1);
+by (res_inst_tac [("x","k*ka")] exI 1);
+by (asm_simp_tac (simpset() addsimps zmult_ac) 1);
+qed "zdvd_zmult_mono";
+
+Goal "k dvd (n + k*m) = k dvd (n::int)";
+by (rtac iffI 1);
+by (etac zdvd_zadd 2);
+by (subgoal_tac "n = (n+k*m)-k*m" 1);
+by (etac ssubst 1);
+by (etac zdvd_zdiff 1);
+by (ALLGOALS Simp_tac);
+qed "zdvd_reduce";
+
+Goalw [dvd_def] "[| f dvd m; f dvd (n::int) |] ==> f dvd (m mod n)";
+by (auto_tac (claset(), simpset() addsimps [zmod_zmult_zmult1]));
+qed "zdvd_zmod";
+
+Goal "[| k dvd (m mod n); k dvd n |] ==> k dvd (m::int)";
+by (subgoal_tac "k dvd (n*(m div n) + m mod n)" 1);
+by (asm_simp_tac (simpset() addsimps [zdvd_zadd, zdvd_zmult2]) 2);
+by (asm_full_simp_tac (simpset() addsimps [zmod_zdiv_equality RS sym]) 1);
+qed "zdvd_zmod_imp_zdvd";
+
+Goalw [dvd_def] "(k dvd n) = (n mod (k::int) = #0)";
+by (zdiv_undefined_case_tac "k=#0" 1);
+by Safe_tac;
+by (res_inst_tac [("x","n div k")] exI 2);
+by (rtac trans 2);
+by (res_inst_tac [("b","k")] zmod_zdiv_equality 2);
+by (ALLGOALS Asm_simp_tac);
+qed "zdvd_iff_zmod_eq_0";
+
+Goal "[| ~k<#0; k~=#0 |] ==> #0<(k::int)";
+by (arith_tac 1);
+val lemma = result();
+
+Goalw [dvd_def] "[| #0<m; m<n |] ==> ~n dvd (m::int)";
+by Auto_tac;
+by (subgoal_tac "#0<n" 1);
+by (blast_tac (claset() addIs [zless_trans]) 2);
+by (case_tac "k<#0" 1);
+by (rotate_tac ~2 1);
+by (asm_full_simp_tac (simpset() addsimps [int_0_less_mult_iff]) 1);
+by (case_tac "k=#0" 1);
+by (subgoal_tac "n*k < n*#1" 2);
+by (asm_full_simp_tac (simpset() delsimps [zmult_1_right]) 2);
+by (subgoal_tac "#0<k" 2);
+by (rtac lemma 3);
+by (ALLGOALS Asm_full_simp_tac);
+qed "zdvd_not_zless";
+
+
+(************************************************)
+(** Euclid's Algorithm and GCD **)
+(************************************************)
+
+val [zgcd_eq] = zgcd.simps;
+Delsimps zgcd.simps;
+
+Goal "zgcd(m,#0) = m";
+by (rtac (zgcd_eq RS trans) 1);
+by (Simp_tac 1);
+qed "zgcd_0";
+Addsimps [zgcd_0];
+
+Goal"#0<(m::int) ==> zgcd(#0,m) = m";
+by (auto_tac (claset(), simpset() addsimps zgcd.simps));
+qed "zgcd_0_left";
+Addsimps [zgcd_0_left];
+
+Goal "#0<n ==> zgcd(m,n) = zgcd (n, m mod n)";
+by (rtac (zgcd_eq RS trans) 1);
+by (Asm_simp_tac 1);
+qed "zgcd_non_0";
+
+Goal "zgcd(m,#1) = #1";
+by (simp_tac (simpset() addsimps [zgcd_non_0]) 1);
+qed "zgcd_1";
+Addsimps [zgcd_1];
+
+Goal "(zgcd(#0,m) = #1) = (m = #1)";
+by (auto_tac (claset(),simpset() addsimps zgcd.simps));
+qed "zgcd_0_1_iff";
+Addsimps [zgcd_0_1_iff];
+
+Goal "#0<=(n::int) --> (zgcd(m,n) dvd m) & (zgcd(m,n) dvd n)";
+by (res_inst_tac [("u","m"),("v","n")] zgcd.induct 1);
+by (case_tac "n=#0" 1);
+by (auto_tac (claset() addDs [zdvd_zmod_imp_zdvd],
+ simpset() addsimps [zle_neq_implies_zless,neq_commute,
+ pos_mod_sign,zgcd_non_0]));
+by (ALLGOALS (rotate_tac 1));
+by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [zle_anti_sym])));
+qed_spec_mp "zgcd_zdvd_both";
+
+bind_thm ("zgcd_zdvd1", zgcd_zdvd_both RS conjunct1);
+bind_thm ("zgcd_zdvd2", zgcd_zdvd_both RS conjunct2);
+
+Goal "[| (n::int) <= #0; #0 <= n; #0 ~= n |] ==> False";
+by (asm_full_simp_tac (simpset() addsimps [zle_anti_sym]) 1);
+val lemma_false = result();
+
+Goal "#0<=(n::int) --> (f dvd m) --> (f dvd n) --> f dvd zgcd(m,n)";
+by (res_inst_tac [("u","m"),("v","n")] zgcd.induct 1);
+by (case_tac "n=#0" 1);
+by (auto_tac (claset() addDs [lemma_false] addIs [pos_mod_sign,zdvd_zmod],
+ simpset() addsimps [zgcd_non_0,neq_commute,zle_neq_implies_zless]));
+qed_spec_mp "zgcd_greatest";
+
+Goal "#0 < (n::int) --> #0 < zgcd (m, n)";
+by (res_inst_tac [("u","m"),("v","n")] zgcd.induct 1);
+by (auto_tac (claset(), simpset() addsimps zgcd.simps));
+qed_spec_mp "zgcd_zless";
+
+Goalw [is_zgcd_def] "#0<(n::int) ==> is_zgcd (zgcd(m,n)) m n";
+by (asm_simp_tac (simpset() addsimps
+ [zgcd_greatest,zgcd_zdvd_both,zgcd_zless]) 1);
+qed "is_zgcd";
+
+Goalw [is_zgcd_def] "[| is_zgcd m a b; is_zgcd n a b |] ==> m=n";
+by (blast_tac (claset() addIs [zdvd_anti_sym]) 1);
+qed "is_zgcd_unique";
+
+Goalw [is_zgcd_def] "[| is_zgcd m a b; k dvd a; k dvd b |] ==> k dvd m";
+by (Blast_tac 1);
+qed "is_zgcd_zdvd";
+
+Goalw [is_zgcd_def] "is_zgcd k m n = is_zgcd k n m";
+by (Blast_tac 1);
+qed "is_zgcd_commute";
+
+Goalw [is_zgcd_def] "is_zgcd k (-m) n = is_zgcd k m n";
+by (asm_full_simp_tac (simpset() addsimps [zdvd_zminus_iff]) 1);
+qed "is_zgcd_zminus";
+
+Goal "#0<(n::int) ==> zgcd(-m,n) = zgcd(m,n)";
+by (rtac is_zgcd_unique 1);
+by (rtac is_zgcd 1);
+by (asm_simp_tac (simpset() addsimps [is_zgcd,is_zgcd_zminus]) 2);
+by (assume_tac 1);
+qed "zgcd_zminus";
+
+Goal "[| #0<(m::int); #0<n |] ==> zgcd(m,n) = zgcd(n,m)";
+by (rtac is_zgcd_unique 1);
+by (rtac is_zgcd 2);
+by (asm_simp_tac (simpset() addsimps [is_zgcd,is_zgcd_commute]) 1);
+by (assume_tac 1);
+qed "zgcd_commute";
+
+Goal "#0<=(m::int) ==> zgcd(#1,m) = #1";
+by (case_tac "m=#0" 1);
+by (stac zgcd_commute 2);
+by (ALLGOALS (asm_full_simp_tac (simpset()
+ addsimps [zle_neq_implies_zless,neq_commute])));
+qed "zgcd_1_left";
+Addsimps [zgcd_1_left];
+
+Goal "[| #0<(m::int); #0<n |] ==> zgcd(zgcd(k,m),n) = zgcd(k,zgcd(m,n))";
+by (rtac is_zgcd_unique 1);
+by (rtac is_zgcd 2);
+by (rewrite_goals_tac [is_zgcd_def]);
+by Auto_tac;
+by (rtac zgcd_greatest 3);
+by (res_inst_tac [("n","zgcd (k,m)")] zdvd_trans 2);
+by (res_inst_tac [("n","zgcd (k,m)")] zdvd_trans 5);
+by (rtac zgcd_greatest 8);
+by (rtac zgcd_greatest 9);
+by (res_inst_tac [("n","zgcd (m,n)")] zdvd_trans 12);
+by (res_inst_tac [("n","zgcd (m,n)")] zdvd_trans 11);
+by (ALLGOALS (asm_simp_tac (simpset()
+ addsimps [zgcd_zdvd1,zgcd_zdvd2,zgcd_zless])));
+qed "zgcd_assoc";
+
+Goal "#0<=(n::int) --> #0<=k --> k * zgcd(m,n) = zgcd(k*m, k*n)";
+by (res_inst_tac [("u","m"),("v","n")] zgcd.induct 1);
+by (case_tac "n=#0" 1);
+by (auto_tac (claset() addDs [lemma_false],
+ simpset() addsimps [zle_neq_implies_zless,pos_mod_sign,
+ zgcd_non_0,neq_commute]));
+by (case_tac "k=#0" 1);
+by (ALLGOALS (asm_full_simp_tac (simpset()
+ addsimps [zle_neq_implies_zless,zgcd_non_0,zmod_zmult_zmult1,
+ int_0_less_mult_iff,neq_commute])));
+qed_spec_mp "zgcd_zmult_distrib2";
+
+Goal "#0<=m ==> zgcd(m,m) = m";
+by (cut_inst_tac [("k","m"),("m","#1"),("n","#1")] zgcd_zmult_distrib2 1);
+by (ALLGOALS Asm_full_simp_tac);
+qed "zgcd_self";
+Addsimps [zgcd_self];
+
+Goal "[| #0<=k; #0<=n |] ==> zgcd(k, k*n) = k";
+by (cut_inst_tac [("k","k"),("m","#1"),("n","n")] zgcd_zmult_distrib2 1);
+by (ALLGOALS Asm_full_simp_tac);
+qed "zgcd_zmult_eq_self";
+Addsimps [zgcd_zmult_eq_self];
+
+Goal "#0<=k ==> zgcd(k*n, k) = k";
+by (cut_inst_tac [("k","k"),("m","n"),("n","#1")] zgcd_zmult_distrib2 1);
+by (ALLGOALS Asm_full_simp_tac);
+qed "zgcd_zmult_eq_self2";
+Addsimps [zgcd_zmult_eq_self2];
+
+Goal "[| #0<=(m::int); #0<=k; zgcd(n,k)=#1; k dvd (m*n) |] ==> k dvd m";
+by (subgoal_tac "m = zgcd(m*n, m*k)" 1);
+by (etac ssubst 1 THEN rtac zgcd_greatest 1);
+by (ALLGOALS (asm_simp_tac (simpset()
+ addsimps [zgcd_zmult_distrib2 RS sym,int_0_le_mult_iff])));
+qed "zrelprime_zdvd_zmult";
+
+Goalw [zprime_def] "[| p:zprime; ~p dvd n |] ==> zgcd(n,p) = #1";
+by (cut_inst_tac [("m","n"),("n","p")] zgcd_zdvd_both 1);
+by Auto_tac;
+qed "zprime_imp_zrelprime";
+
+Goal "[| p:zprime; #0<n; n<p |] ==> zgcd(n,p) = #1";
+by (etac zprime_imp_zrelprime 1);
+by (etac zdvd_not_zless 1);
+by (assume_tac 1);
+qed "zless_zprime_imp_zrelprime";
+
+Goal "[| #0<=(m::int); p:zprime; p dvd (m*n) |] ==> p dvd m | p dvd n";
+by Safe_tac;
+by (rtac zrelprime_zdvd_zmult 1);
+by (rtac zprime_imp_zrelprime 3);
+by (SELECT_GOAL (rewrite_goals_tac [zprime_def]) 2);
+by Auto_tac;
+qed "zprime_zdvd_zmult";
+
+Goal "#0<n ==> zgcd(m+n*k,n) = zgcd(m,n)";
+by (rtac (zgcd_eq RS trans) 1);
+by Auto_tac;
+by (simp_tac (simpset() addsimps [zmod_zadd1_eq]) 1);
+by (rtac trans 1);
+by (rtac (zgcd_eq RS sym) 2);
+by Auto_tac;
+qed "zgcd_zadd_zmult";
+Addsimps [zgcd_zadd_zmult];
+
+Goal "#0<=n ==> zgcd(m,n) dvd zgcd(k*m,n)";
+by (rtac zgcd_greatest 1);
+by (rtac zdvd_trans 2);
+by (rtac zgcd_zdvd1 2);
+by (rtac zgcd_zdvd2 4);
+by (ALLGOALS Asm_simp_tac);
+qed "zgcd_zdvd_zgcd_zmult";
+
+Goal "[| #0<k; #0<m; #0<n; zgcd(k,n) = #1 |] ==> zgcd(k*m,n) dvd zgcd(m,n)";
+by (rtac zgcd_greatest 1);
+by (res_inst_tac [("n","k")] zrelprime_zdvd_zmult 2);
+by (stac zmult_commute 5);
+by (stac (zgcd_assoc RS sym) 4);
+by (rtac zless_imp_zle 3);
+by (ALLGOALS (asm_simp_tac (simpset()
+ addsimps [zgcd_zdvd1,zgcd_zdvd2,zgcd_zless,int_0_less_mult_iff])));
+qed "zgcd_zmult_zdvd_zgcd";
+
+Goal "[| #0<n; zgcd(k,n) = #1 |] ==> zgcd(k*m, n) = zgcd(m,n)";
+by (rtac zdvd_anti_sym 1);
+by (rtac zgcd_zdvd_zgcd_zmult 4);
+by (case_tac "m=#0" 3);
+by (case_tac "k=#0" 4);
+by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [zgcd_zless])));
+by (case_tac "#0<k" 1);
+by (ALLGOALS (case_tac "#0<m"));
+by (rtac zgcd_zmult_zdvd_zgcd 1);
+by (subgoal_tac "zgcd (k*(-m),n) dvd zgcd (-m,n)" 5);
+by (rtac zgcd_zmult_zdvd_zgcd 6);
+by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [zgcd_zminus])));
+by (subgoal_tac "zgcd ((-k)*m,n) dvd zgcd (m,n)" 2);
+by (rtac zgcd_zmult_zdvd_zgcd 3);
+by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [zgcd_zminus])));
+by (subgoal_tac "zgcd ((-k)*(-m),n) dvd zgcd (-m,n)" 3);
+by (rtac zgcd_zmult_zdvd_zgcd 4);
+by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [zgcd_zminus])));
+by (auto_tac (claset() addIs [zle_neq_implies_zless], simpset()));
+qed "zgcd_zmult_cancel";
+
+Goal "[| #0<m; zgcd(k,m) = #1; zgcd(n,m) = #1 |] ==> zgcd(k*n,m) = #1";
+by (asm_simp_tac (simpset() addsimps [zgcd_zmult_cancel]) 1);
+qed "zgcd_zgcd_zmult";
+
+Goal "#0<m ==> (m dvd n) = (zgcd(n,m) = m)";
+by Safe_tac;
+by (res_inst_tac [("n","zgcd(n,m)")] zdvd_trans 2);
+by (rtac zgcd_zdvd1 3);
+by (ALLGOALS Asm_simp_tac);
+by (rewtac dvd_def);
+by Auto_tac;
+qed "zdvd_iff_zgcd";
+
+
+(************************************************)
+(** Congruences **)
+(************************************************)
+
+Goalw [zcong_def] "[a=b](mod #1)";
+by Auto_tac;
+qed "zcong_1";
+Addsimps [zcong_1];
+
+Goalw [zcong_def] "[k = k] (mod m)";
+by Auto_tac;
+qed "zcong_refl";
+Addsimps [zcong_refl];
+
+Goalw [zcong_def,dvd_def] "[a = b](mod m) = [b = a](mod m)";
+by Auto_tac;
+by (ALLGOALS (res_inst_tac [("x","-k")] exI));
+by Auto_tac;
+qed "zcong_sym";
+
+Goalw [zcong_def]
+ "[| [a = b] (mod m); [c = d] (mod m) |] ==> [a+c = b+d](mod m)";
+by (res_inst_tac [("s","(a-b)+(c-d)")] subst 1);
+by (rtac zdvd_zadd 2);
+by Auto_tac;
+qed "zcong_zadd";
+
+Goalw [zcong_def]
+ "[| [a = b] (mod m); [c = d] (mod m) |] ==> [a-c = b-d](mod m)";
+by (res_inst_tac [("s","(a-b)-(c-d)")] subst 1);
+by (rtac zdvd_zdiff 2);
+by Auto_tac;
+qed "zcong_zdiff";
+
+Goalw [zcong_def,dvd_def]
+ "[| [a = b](mod m); [b = c](mod m) |] ==> [a = c](mod m)";
+by Auto_tac;
+by (res_inst_tac [("x","k+ka")] exI 1);
+by (asm_full_simp_tac (simpset() addsimps zadd_ac@[zadd_zmult_distrib2]) 1);
+qed "zcong_trans";
+
+Goal "[| [a = b] (mod m); [c = d] (mod m) |] ==> [a*c = b*d](mod m)";
+by (res_inst_tac [("b","b*c")] zcong_trans 1);
+by (rewtac zcong_def);
+by (res_inst_tac [("s","c*(a-b)")] subst 1);
+by (res_inst_tac [("s","b*(c-d)")] subst 3);
+by (blast_tac (claset() addIs [zdvd_zmult]) 4);
+by (blast_tac (claset() addIs [zdvd_zmult]) 2);
+by (ALLGOALS (asm_simp_tac (simpset() addsimps [zdiff_zmult_distrib2,
+ zmult_commute])));
+qed "zcong_zmult";
+
+Goal "[a = b] (mod m) ==> [a*k = b*k](mod m)";
+by (rtac zcong_zmult 1);
+by (ALLGOALS Asm_simp_tac);
+qed "zcong_scalar";
+
+Goal "[a = b] (mod m) ==> [k*a = k*b](mod m)";
+by (rtac zcong_zmult 1);
+by (ALLGOALS Asm_simp_tac);
+qed "zcong_scalar2";
+
+Goalw [zcong_def] "[a*m = b*m](mod m)";
+by (rtac zdvd_zdiff 1);
+by (ALLGOALS Simp_tac);
+qed "zcong_zmult_self";
+
+Goalw [zcong_def]
+ "[| p:zprime; #0<a; [a*a = #1](mod p) |] \
+\ ==> [a=#1](mod p) | [a = p-#1](mod p)";
+by (rtac zprime_zdvd_zmult 1);
+by (res_inst_tac [("s","a*a - #1 + p*(#1-a)")] subst 3);
+by (simp_tac (simpset() addsimps [zdvd_reduce]) 4);
+by (ALLGOALS (asm_simp_tac (simpset()
+ addsimps [zdiff_zmult_distrib,zmult_commute,zdiff_zmult_distrib2])));
+qed "zcong_square";
+
+Goal "[| #0<=m; zgcd(k,m) = #1 |] ==> [a*k = b*k](mod m) = [a = b](mod m)";
+by Safe_tac;
+by (blast_tac (claset() addIs [zcong_scalar]) 2);
+by (case_tac "b<a" 1);
+by (stac zcong_sym 2);
+by (rewrite_goals_tac [zcong_def]);
+by (ALLGOALS (rtac zrelprime_zdvd_zmult));
+by (ALLGOALS (asm_simp_tac (simpset() addsimps [zdiff_zmult_distrib])));
+by (subgoal_tac "m dvd (-(a*k - b*k))" 1);
+by (asm_full_simp_tac (simpset() addsimps [zminus_zdiff_eq]) 1);
+by (stac zdvd_zminus_iff 1);
+by (assume_tac 1);
+qed "zcong_cancel";
+
+Goal "[| #0<=m; zgcd(k,m) = #1 |] ==> [k*a = k*b](mod m) = [a = b](mod m)";
+by (asm_simp_tac (simpset() addsimps [zmult_commute,zcong_cancel]) 1);
+qed "zcong_cancel2";
+
+Goalw [zcong_def,dvd_def]
+ "[| #0<m; #0<n; [a = b] (mod m); [a = b] (mod n); zgcd(m,n) = #1 |] \
+\ ==> [a=b](mod m*n)";
+by Auto_tac;
+by (subgoal_tac "m dvd (n*ka)" 1);
+by (subgoal_tac "m dvd ka" 1);
+by (case_tac "#0<=ka" 2);
+by (stac (zdvd_zminus_iff RS sym) 3);
+by (res_inst_tac [("n","n")] zrelprime_zdvd_zmult 2);
+by (asm_simp_tac (simpset() addsimps [zgcd_commute]) 4);
+by (asm_full_simp_tac (simpset() addsimps [zmult_commute]) 4);
+by (res_inst_tac [("n","n")] zrelprime_zdvd_zmult 4);
+by (asm_simp_tac (simpset() addsimps [zgcd_commute]) 6);
+by (asm_full_simp_tac (simpset() addsimps [zmult_commute,zdvd_zminus_iff]) 6);
+by (ALLGOALS Asm_simp_tac);
+by (rewtac dvd_def);
+by Safe_tac;
+by (res_inst_tac [("x","kc")] exI 1);
+by (res_inst_tac [("x","k")] exI 2);
+by (simp_tac (simpset() addsimps zmult_ac) 1);
+by Auto_tac;
+qed "zcong_zgcd_zmult_zmod";
+
+Goalw [zcong_def,dvd_def]
+ "[| #0<=a; a<m; #0<=b; b<m; [a = b] (mod m) |] ==> a = b";
+by (rtac (eq_iff_zdiff_eq_0 RS iffD2) 1);
+by Auto_tac;
+by (subgoal_tac "k=#0" 1);
+by (subgoal_tac "#-1<k & k<#1" 2);
+by Auto_tac;
+by (ALLGOALS (rtac iffD1));
+by (res_inst_tac [("k","m")] zmult_zless_cancel1 3);
+by (res_inst_tac [("k","m")] zmult_zless_cancel1 1);
+by Auto_tac;
+qed "zcong_zless_imp_eq";
+
+Goal "[| p:zprime; #0<a; a<p; [a*a = #1](mod p) |] ==> a = #1 | a = p-#1";
+by (cut_inst_tac [("p","p"),("a","a")] zcong_square 1);
+by Safe_tac;
+by (res_inst_tac [("Pa","a=p-#1")] swap 2);
+by (rtac zcong_zless_imp_eq 1);
+by (rtac zcong_zless_imp_eq 7);
+by (rewtac zprime_def);
+by Auto_tac;
+qed "zcong_square_zless";
+
+Goalw [zcong_def] "[| #0<a; a<m; #0<b; b<a |] ==> ~[a = b] (mod m) ";
+by (rtac zdvd_not_zless 1);
+by Auto_tac;
+qed "zcong_not";
+
+Goalw [zcong_def,dvd_def] "[| #0<=a; a<m; [a=#0](mod m) |] ==> a = #0";
+by Auto_tac;
+by (subgoal_tac "#0<m" 1);
+by (rotate_tac ~1 1);
+by (asm_full_simp_tac (simpset() addsimps [int_0_le_mult_iff]) 1);
+by (subgoal_tac "m*k<m*#1" 1);
+by (asm_full_simp_tac (simpset() delsimps [zmult_1_right]) 1);
+by (ALLGOALS Asm_full_simp_tac);
+qed "zcong_zless_0";
+
+Goal "#0<m ==> (EX! b. #0<=b & b<m & [a = b] (mod m))";
+by Auto_tac;
+by (subgoal_tac "[b = y] (mod m)" 2);
+by (case_tac "b=#0" 2);
+by (case_tac "y=#0" 3);
+by (auto_tac (claset() addIs [zcong_trans,zcong_zless_0,
+ zcong_zless_imp_eq,zle_neq_implies_zless],
+ simpset() addsimps [zcong_sym]));
+by (rewrite_goals_tac [zcong_def,dvd_def]);
+by (res_inst_tac [("x","a mod m")] exI 1);
+by (auto_tac (claset(),simpset() addsimps [pos_mod_sign,pos_mod_bound]));
+by (res_inst_tac [("x","-(a div m)")] exI 1);
+by (cut_inst_tac [("a","a"),("b","m")] zmod_zdiv_equality 1);
+by Auto_tac;
+qed "zcong_zless_unique";
+
+Goalw [zcong_def,dvd_def] "([a = b] (mod m)) = (EX k. b = a + m*k)";
+by Auto_tac;
+by (ALLGOALS (res_inst_tac [("x","-k")] exI));
+by Auto_tac;
+qed "zcong_iff_lin";
+
+Goal "[| #0<m; zgcd(a,m) = #1; [a = b] (mod m) |] ==> zgcd(b,m) = #1";
+by (auto_tac (claset(),simpset() addsimps [zcong_iff_lin]));
+qed "zgcd_zcong_zgcd";
+
+Goal "[| a=c; b=d |] ==> a-b = c-(d::int)";
+by Auto_tac;
+val lemma = result();
+
+Goal "a - b = (m::int) * (a div m - b div m) + (a mod m - b mod m)";
+by (res_inst_tac [("s","(m * (a div m) + a mod m) - \
+\ (m * (b div m) + b mod m)")] trans 1);
+by (simp_tac (simpset() addsimps [zdiff_zmult_distrib2]) 2);
+by (rtac lemma 1);
+by (ALLGOALS (rtac zmod_zdiv_equality));
+val lemma = result();
+
+Goalw [zcong_def] "[a = b] (mod m) = [a mod m = b mod m](mod m)";
+by (res_inst_tac [("t","a-b")] ssubst 1);
+by (res_inst_tac [("m","m")] lemma 1);
+by (rtac trans 1);
+by (res_inst_tac [("k","m"),("m","a div m - b div m")] zdvd_reduce 2);
+by (simp_tac (simpset() addsimps [zadd_commute]) 1);
+qed "zcong_zmod";
+
+Goal "#0<m ==> [a = b] (mod m) = (a mod m = b mod m)";
+by Auto_tac;
+by (res_inst_tac [("m","m")] zcong_zless_imp_eq 1);
+by (stac (zcong_zmod RS sym) 5);
+by (ALLGOALS (asm_simp_tac (simpset() addsimps [pos_mod_bound,pos_mod_sign])));
+by (rewrite_goals_tac [zcong_def,dvd_def]);
+by (res_inst_tac [("x","a div m - b div m")] exI 1);
+by (res_inst_tac [("m1","m")] (lemma RS trans) 1);
+by Auto_tac;
+qed "zcong_zmod_eq";
+
+
+(************************************************)
+(** Modulo **)
+(************************************************)
+
+Goalw [dvd_def] "[| #0<(m::int); m dvd b |] ==> (a mod b mod m) = (a mod m)";
+by Auto_tac;
+by (stac (zcong_zmod_eq RS sym) 1);
+by (stac zcong_iff_lin 2);
+by (res_inst_tac [("x","k*(a div (m*k))")] exI 2);
+by (stac zadd_commute 2);
+by (stac (zmult_assoc RS sym) 2);
+by (rtac zmod_zdiv_equality 2);
+by (assume_tac 1);
+qed "zmod_zdvd_zmod";
+
+(************************************************)
+(** Extended GCD **)
+(************************************************)
+
+val [xzgcda_eq] = xzgcda.simps;
+Delsimps xzgcda.simps;
+
+Goal "zgcd(r',r) = k --> \
+\ (EX sn tn. xzgcda (m,n,r',r,s',s,t',t) = (k,sn,tn))";
+by (res_inst_tac [("u","m"),("v","n"),("w","r'"),("x","r"),
+ ("y","s'"),("z","s"),("aa","t'"),("ab","t")]
+ xzgcda.induct 1);
+by (stac zgcd_eq 1);
+by (stac xzgcda_eq 1);
+by Auto_tac;
+val lemma1 = result();
+
+Goal "(EX sn tn. xzgcda (m,n,r',r,s',s,t',t) = (k,sn,tn)) --> \
+\ zgcd(r',r) = k";
+by (res_inst_tac [("u","m"),("v","n"),("w","r'"),("x","r"),
+ ("y","s'"),("z","s"),("aa","t'"),("ab","t")]
+ xzgcda.induct 1);
+by (stac zgcd_eq 1);
+by (stac xzgcda_eq 1);
+by Auto_tac;
+val lemma2 = result();
+
+Goalw [xzgcd_def] "(zgcd(m,n) = k) = (EX s t. xzgcd m n = (k,s,t))";
+by (rtac iffI 1);
+by (ALLGOALS (rtac mp));
+by (rtac lemma2 3);
+by (rtac lemma1 1);
+by Auto_tac;
+qed "xzgcd_correct";
+
+(* xzgcd linear *)
+
+Goal "(a-r*b)*m + (c-r*d)*(n::int) = (a*m + c*n) - r*(b*m + d*n)";
+by (simp_tac (simpset() addsimps [zdiff_zmult_distrib,zadd_zmult_distrib2,
+ zmult_assoc]) 1);
+val lemma = result();
+
+Goal "[| r' = s'*m + t'*n; r = s*m + t*n |] \
+\ ==> (r' mod r) = (s' - (r' div r)*s)*m + (t' - (r' div r)*t)*(n::int)";
+by (rtac trans 1);
+by (rtac (lemma RS sym) 2);
+by (Asm_simp_tac 1);
+by (stac eq_zdiff_eq 1);
+by (rtac (trans RS sym) 1);
+by (res_inst_tac [("b","s*m + t*n")] zmod_zdiv_equality 1);
+by (simp_tac (simpset() addsimps [zmult_commute]) 1);
+val lemma = result();
+
+Goal "#0<r --> xzgcda(m,n,r',r,s',s,t',t) = (rn,sn,tn) \
+\ --> r' = s'*m + t'*n --> r = s*m + t*n --> rn = sn*m + tn*n";
+by (res_inst_tac [("u","m"),("v","n"),("w","r'"),("x","r"),
+ ("y","s'"),("z","s"),("aa","t'"),("ab","t")]
+ xzgcda.induct 1);
+by (stac xzgcda_eq 1);
+by (rewtac Let_def);
+by (Simp_tac 1);
+by (REPEAT (rtac impI 1));
+by (case_tac "r' mod r = #0" 1);
+by (asm_full_simp_tac (simpset() addsimps [xzgcda_eq]) 1);
+by (SELECT_GOAL Safe_tac 1);
+by (subgoal_tac "#0 < r' mod r" 1);
+by (rtac zle_neq_implies_zless 2);
+by (rtac pos_mod_sign 2);
+by (cut_inst_tac [("m","m"),("n","n"),("r'","r'"),("r","r"),
+ ("s'","s'"),("s","s"),("t'","t'"),("t","t")]
+ lemma 1);
+by Auto_tac;
+qed_spec_mp "xzgcda_linear";
+
+Goalw [xzgcd_def] "[| #0<n; xzgcd m n = (r,s,t) |] ==> r = s*m + t*n";
+by (etac xzgcda_linear 1);
+by (assume_tac 1);
+by Auto_tac;
+qed "xzgcd_linear";
+
+Goal "[| #0<n; zgcd(m,n) = k |] ==> (EX s t. k = s*m + t*n)";
+by (full_simp_tac (simpset() addsimps [xzgcd_correct]) 1);
+by Safe_tac;
+by (REPEAT (rtac exI 1));
+by (etac xzgcd_linear 1);
+by Auto_tac;
+qed "zgcd_ex_linear";
+
+Goal "[| #0<n; zgcd(a,n) = #1 |] ==> EX x. [a*x = #1](mod n)";
+by (cut_inst_tac [("m","a"),("n","n"),("k","#1")] zgcd_ex_linear 1);
+by Safe_tac;
+by (res_inst_tac [("x","s")] exI 1);
+by (res_inst_tac [("b","s*a+t*n")] zcong_trans 1);
+by (Asm_simp_tac 2);
+by (rewtac zcong_def);
+by (simp_tac (simpset() addsimps [zmult_commute,zdvd_zminus_iff]) 1);
+qed "zcong_lineq_ex";
+
+Goal "[| #0<n; zgcd(a,n) = #1 |] ==> EX! x. #0<=x & x<n & [a*x = b](mod n)";
+by Auto_tac;
+by (rtac zcong_zless_imp_eq 2);
+by (stac (zcong_cancel2 RS sym) 6);
+by (rtac zcong_trans 8);
+by (ALLGOALS Asm_simp_tac);
+by (asm_full_simp_tac (simpset() addsimps [zcong_sym]) 2);
+by (cut_inst_tac [("a","a"),("n","n")] zcong_lineq_ex 1);
+by Auto_tac;
+by (res_inst_tac [("x","x*b mod n")] exI 1);
+by Safe_tac;
+by (ALLGOALS (asm_simp_tac (simpset() addsimps [pos_mod_bound,pos_mod_sign])));
+by (stac zcong_zmod 1);
+by (stac (zmod_zmult1_eq RS sym) 1);
+by (stac (zcong_zmod RS sym) 1);
+by (subgoal_tac "[a*x*b = #1*b](mod n)" 1);
+by (rtac zcong_zmult 2);
+by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [zmult_assoc])));
+qed "zcong_lineq_unique";
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/NumberTheory/IntPrimes.thy Thu Aug 03 10:46:01 2000 +0200
@@ -0,0 +1,39 @@
+(* Title: IntPrimes.thy
+ ID: $Id$
+ Author: Thomas M. Rasmussen
+ Copyright 2000 University of Cambridge
+*)
+
+IntPrimes = Main + IntDiv +
+
+consts
+ is_zgcd :: [int,int,int] => bool
+ zgcd :: "int*int => int"
+ xzgcda :: "int*int*int*int*int*int*int*int => int*int*int"
+ xzgcd :: "[int,int] => int*int*int"
+ zprime :: int set
+ zcong :: [int,int,int] => bool ("(1[_ = _] '(mod _'))")
+
+recdef zgcd "measure ((%(m,n).(nat n)) ::int*int=>nat)"
+ simpset "simpset() addsimps [pos_mod_bound]"
+ "zgcd (m, n) = (if n<=#0 then m else zgcd(n, m mod n))"
+
+recdef xzgcda
+ "measure ((%(m,n,r',r,s',s,t',t).(nat r))
+ ::int*int*int*int*int*int*int*int=>nat)"
+ simpset "simpset() addsimps [pos_mod_bound]"
+ "xzgcda (m,n,r',r,s',s,t',t) =
+ (if r<=#0 then (r',s',t') else
+ xzgcda(m,n,r,r' mod r,s,s'-(r' div r)*s,t,t'-(r' div r)*t))"
+
+defs
+ xzgcd_def "xzgcd m n == xzgcda (m,n,m,n,#1,#0,#0,#1)"
+
+ is_zgcd_def "is_zgcd p m n == #0 < p & p dvd m & p dvd n &
+ (ALL d. d dvd m & d dvd n --> d dvd p)"
+
+ zprime_def "zprime == {p. #1<p & (ALL m. m dvd p --> m=#1 | m=p)}"
+
+ zcong_def "[a=b] (mod m) == m dvd (a-b)"
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/NumberTheory/README Thu Aug 03 10:46:01 2000 +0200
@@ -0,0 +1,37 @@
+IntPrimes dvd relation, GCD, Euclid's extended algorithm, primes,
+ congruences (all on the Integers)
+ Comparable to 'Primes' theory but dvd is included here
+ as it is not present in 'IntDiv'. Also includes extended
+ GCD and congruences not present in 'Primes'.
+ Also a few extra theorems concerning 'mod'
+ Maybe it should be split/merged - at least given another
+ name?
+
+Chinese The Chinese Remainder Theorem for an arbitrary finite
+ number of equations. (The one-equation case is included
+ in 'IntPrimes')
+ Uses functions for indicing. Maybe 'funprod' and 'funsum'
+ should be based on general 'fold' on indices?
+
+IntPowerFact Power function on Integers (exponent is still Nat),
+ Factorial on integers and recursively defined set
+ including all Integers from 2 up to a. Plus definition
+ of product of finite set.
+ Should probably be split/merged with other theories?
+
+BijectionRel Inductive definitions of bijections between two different
+ sets and between the same set. Theorem for relating
+ the two definitions
+
+EulerFermat Fermat's Little Theorem extended to Euler's Totient function.
+ More abstract approach than Boyer-Moore (which seems necessary
+ to achieve the extended version)
+
+WilsonRuss Wilson's Theorem following quite closely Russinoff's approach
+ using Boyer-Moore (using finite sets instead of lists, though)
+
+WilsonBij Wilson's Theorem using a more "abstract" approach based on
+ bijections between sets. Does not use Fermat's Little Theorem
+ (unlike Russinoff)
+
+
\ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/NumberTheory/ROOT.ML Thu Aug 03 10:46:01 2000 +0200
@@ -0,0 +1,12 @@
+(* Title: HOL/NumberTheory/ROOT
+ ID: $Id$
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Copyright 2000 University of Cambridge
+
+Number theory developments by Thomas M Rasmussen
+*)
+
+use_thy "Chinese";
+use_thy "EulerFermat";
+use_thy "WilsonRuss";
+use_thy "WilsonBij";
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/NumberTheory/WilsonBij.ML Thu Aug 03 10:46:01 2000 +0200
@@ -0,0 +1,227 @@
+(* Title: WilsonBij.ML
+ ID: $Id$
+ Author: Thomas M. Rasmussen
+ Copyright 2000 University of Cambridge
+
+Wilson's Theorem using a more "abstract" approach based on
+bijections between sets. Does not use Fermat's Little Theorem
+(unlike Russinoff)
+ *)
+
+
+(************ Inverse **************)
+
+Goalw [inv_def]
+ "[| p:zprime; #0<a; a<p |] \
+\ ==> #0 <= (inv p a) & (inv p a)<p & [a*(inv p a) = #1](mod p)";
+by (Asm_simp_tac 1);
+by (rtac (zcong_lineq_unique RS ex1_implies_ex RS ex_someI) 1);
+by (etac zless_zprime_imp_zrelprime 2);
+by (rewtac zprime_def);
+by Auto_tac;
+qed "inv_correct";
+
+bind_thm ("inv_ge",inv_correct RS conjunct1);
+bind_thm ("inv_less",(inv_correct RS conjunct2) RS conjunct1);
+bind_thm ("inv_is_inv",(inv_correct RS conjunct2) RS conjunct2);
+
+(* Same as WilsonRuss *)
+Goal "[| p:zprime; #1<a; a<p-#1 |] ==> (inv p a) ~= #0";
+by Safe_tac;
+by (cut_inst_tac [("a","a"),("p","p")] inv_is_inv 1);
+by (rewtac zcong_def);
+by Auto_tac;
+by (subgoal_tac "~p dvd #1" 1);
+by (rtac zdvd_not_zless 2);
+by (subgoal_tac "p dvd #1" 1);
+by (stac (zdvd_zminus_iff RS sym) 2);
+by Auto_tac;
+qed "inv_not_0";
+
+(* Same as WilsonRuss *)
+Goal "[| p:zprime; #1<a; a<p-#1 |] ==> (inv p a) ~= #1";
+by Safe_tac;
+by (cut_inst_tac [("a","a"),("p","p")] inv_is_inv 1);
+by (Asm_full_simp_tac 4);
+by (subgoal_tac "a = #1" 4);
+by (rtac zcong_zless_imp_eq 5);
+by Auto_tac;
+qed "inv_not_1";
+
+(* Same as WilsonRuss *)
+Goalw [zcong_def] "[a*(p-#1) = #1](mod p) = [a = p-#1](mod p)";
+by (simp_tac (simpset() addsimps [zdiff_zdiff_eq,zdiff_zdiff_eq2,
+ zdiff_zmult_distrib2]) 1);
+by (res_inst_tac [("s","p dvd -((a+#1)+(p*(-a)))")] trans 1);
+by (simp_tac (simpset() addsimps [zmult_commute,zminus_zdiff_eq]) 1);
+by (stac zdvd_zminus_iff 1);
+by (stac zdvd_reduce 1);
+by (res_inst_tac [("s","p dvd ((a+#1)+(p*(-#1)))")] trans 1);
+by (stac zdvd_reduce 1);
+by Auto_tac;
+val lemma = result();
+
+(* Same as WilsonRuss *)
+Goal "[| p:zprime; #1<a; a<p-#1 |] ==> (inv p a) ~= p-#1";
+by Safe_tac;
+by (cut_inst_tac [("a","a"),("p","p")] inv_is_inv 1);
+by Auto_tac;
+by (asm_full_simp_tac (simpset() addsimps [lemma]) 1);
+by (subgoal_tac "a = p-#1" 1);
+by (rtac zcong_zless_imp_eq 2);
+by Auto_tac;
+qed "inv_not_p_minus_1";
+
+(* Below is slightly different as we don't expand
+ inv but use 'correct'-theos *)
+Goal "[| p:zprime; #1<a; a<p-#1 |] ==> #1<(inv p a)";
+by (subgoal_tac "(inv p a) ~= #1" 1);
+by (subgoal_tac "(inv p a) ~= #0" 1);
+by (rtac zle_neq_implies_zless 1);
+by (stac (zle_add1_eq_le RS sym) 1);
+by (rtac zle_neq_implies_zless 1);
+by (rtac inv_not_0 4);
+by (rtac inv_not_1 7);
+by Auto_tac;
+by (rtac inv_ge 1);
+by Auto_tac;
+qed "inv_g_1";
+
+(* ditto *)
+Goal "[| p:zprime; #1<a; a<p-#1 |] ==> (inv p a)<p-#1";
+by (rtac zle_neq_implies_zless 1);
+by (rtac inv_not_p_minus_1 2);
+by Auto_tac;
+by (rtac inv_less 1);
+by Auto_tac;
+qed "inv_less_p_minus_1";
+
+(************* Bijection *******************)
+
+Goal "#1<x ==> #0<=(x::int)";
+by Auto_tac;
+val l1 = result();
+
+Goal "#1<x ==> #0<(x::int)";
+by Auto_tac;
+val l2 = result();
+
+Goal "x<=p-#2 ==> x<(p::int)";
+by Auto_tac;
+val l3 = result();
+
+Goal "x<=p-#2 ==> x<(p::int)-#1";
+by Auto_tac;
+val l4 = result();
+
+Goalw [inj_on_def] "p : zprime ==> inj_on (inv p) (d22set (p-#2))";
+by Auto_tac;
+by (rtac zcong_zless_imp_eq 1);
+by (stac (zcong_cancel RS sym) 5);
+by (rtac zcong_trans 7);
+by (stac zcong_sym 8);
+by (etac inv_is_inv 7);
+by (Asm_simp_tac 9);
+by (etac inv_is_inv 9);
+by (rtac zless_zprime_imp_zrelprime 6);
+by (rtac inv_less 8);
+by (rtac (inv_g_1 RS l2) 7);
+by (rewtac zprime_def);
+by (auto_tac (claset() addIs [d22set_g_1,d22set_le,l1,l2,l3,l4],simpset()));
+qed "inv_inj";
+
+Goal "p : zprime ==> (inv p)``(d22set (p-#2)) = (d22set (p-#2))";
+by (rtac endo_inj_surj 1);
+by (rtac d22set_fin 1);
+by (etac inv_inj 2);
+by Auto_tac;
+by (rtac d22set_mem 1);
+by (etac inv_g_1 1);
+by (subgoal_tac "inv p xa < p - #1" 3);
+by (etac inv_less_p_minus_1 4);
+by (auto_tac (claset() addIs [d22set_g_1,d22set_le,l4],simpset()));
+qed "inv_d22set_d22set";
+
+Goalw [reciR_def] "p:zprime \
+\ ==> (d22set(p-#2),d22set(p-#2)) : (bijR (reciR p))";
+by (res_inst_tac [("s","(d22set(p-#2),(inv p)``(d22set(p-#2)))")] subst 1);
+by (asm_simp_tac (simpset() addsimps [inv_d22set_d22set]) 1);
+by (rtac inj_func_bijR 1);
+by (rtac d22set_fin 3);
+by (etac inv_inj 2);
+by Auto_tac;
+by (etac inv_is_inv 1);
+by (etac inv_g_1 5);
+by (etac inv_less_p_minus_1 7);
+by (auto_tac (claset() addIs [d22set_g_1,d22set_le,l2,l3,l4],simpset()));
+qed "d22set_d22set_bij";
+
+Goalw [reciR_def,bijP_def]
+ "p:zprime ==> bijP (reciR p) (d22set(p-#2))";
+by Auto_tac;
+by (rtac d22set_mem 1);
+by Auto_tac;
+qed "reciP_bijP";
+
+Goalw [reciR_def,uniqP_def]
+ "p:zprime ==> uniqP (reciR p)";
+by Auto_tac;
+by (rtac zcong_zless_imp_eq 1);
+by (stac (zcong_cancel2 RS sym) 5);
+by (rtac zcong_trans 7);
+by (stac zcong_sym 8);
+by (rtac zless_zprime_imp_zrelprime 6);
+by Auto_tac;
+by (rtac zcong_zless_imp_eq 1);
+by (stac (zcong_cancel RS sym) 5);
+by (rtac zcong_trans 7);
+by (stac zcong_sym 8);
+by (rtac zless_zprime_imp_zrelprime 6);
+by Auto_tac;
+qed "reciP_uniq";
+
+Goalw [reciR_def,symP_def]
+ "p:zprime ==> symP (reciR p)";
+by (simp_tac (simpset() addsimps [zmult_commute]) 1);
+by Auto_tac;
+qed "reciP_sym";
+
+Goal "p:zprime ==> d22set(p-#2) : (bijER (reciR p))";
+by (rtac bijR_bijER 1);
+by (etac d22set_d22set_bij 1);
+by (etac reciP_bijP 1);
+by (etac reciP_uniq 1);
+by (etac reciP_sym 1);
+qed "bijER_d22set";
+
+(*********** Wilson **************)
+
+Goalw [reciR_def]
+ "[| p:zprime; A : bijER (reciR p) |] ==> [setprod A = #1](mod p)";
+by (etac bijER.induct 1);
+by (subgoal_tac "a=#1 | a=p-#1" 2);
+by (rtac zcong_square_zless 3);
+by Auto_tac;
+by (stac setprod_insert 1);
+by (stac setprod_insert 3);
+by (auto_tac (claset(),simpset() addsimps [fin_bijER]));
+by (subgoal_tac "zcong ((a * b) * setprod A) (#1*#1) p" 1);
+by (asm_full_simp_tac (simpset() addsimps [zmult_assoc]) 1);
+by (rtac zcong_zmult 1);
+by Auto_tac;
+qed "bijER_zcong_prod_1";
+
+Goal "p:zprime ==> [zfact(p-#1) = #-1](mod p)";
+by (subgoal_tac "zcong ((p-#1)*zfact(p-#2)) (#-1*#1) p" 1);
+by (rtac zcong_zmult 2);
+by (SELECT_GOAL (rewtac zprime_def) 1);
+by (stac zfact_eq 1);
+by (res_inst_tac [("t","p-#1-#1"),("s","p-#2")] subst 1);
+by Auto_tac;
+by (SELECT_GOAL (rewtac zcong_def) 1);
+by (Asm_simp_tac 1);
+by (stac (d22set_prod_zfact RS sym) 1);
+by (rtac bijER_zcong_prod_1 1);
+by (rtac bijER_d22set 2);
+by Auto_tac;
+qed "WilsonBij";
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/NumberTheory/WilsonBij.thy Thu Aug 03 10:46:01 2000 +0200
@@ -0,0 +1,20 @@
+(* Title: WilsonBij.thy
+ ID: $Id$
+ Author: Thomas M. Rasmussen
+ Copyright 2000 University of Cambridge
+*)
+
+WilsonBij = BijectionRel + IntFact +
+
+consts
+ reciR :: "int => [int,int] => bool"
+ inv :: "[int,int] => int"
+
+defs
+ reciR_def "reciR p == (%a b. zcong (a*b) #1 p &
+ #1<a & a<p-#1 & #1<b & b<p-#1)"
+ inv_def "inv p a == (if p:zprime & #0<a & a<p then
+ (@x. #0<=x & x<p & zcong (a*x) #1 p)
+ else #0)"
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/NumberTheory/WilsonRuss.ML Thu Aug 03 10:46:01 2000 +0200
@@ -0,0 +1,319 @@
+(* Title: WilsonRuss.ML
+ ID: $Id$
+ Author: Thomas M. Rasmussen
+ Copyright 2000 University of Cambridge
+*)
+
+
+(************ Inverse **************)
+
+Goal "#1<m ==> Suc(nat(m-#2)) = nat(m-#1)";
+by (stac (int_int_eq RS sym) 1);
+by Auto_tac;
+val lemma = result();
+
+Goalw [inv_def]
+ "[| p:zprime; #0<a; a<p |] ==> [a*(inv p a) = #1] (mod p)";
+by (stac zcong_zmod 1);
+by (stac (zmod_zmult1_eq RS sym) 1);
+by (stac (zcong_zmod RS sym) 1);
+by (stac (power_Suc RS sym) 1);
+by (stac lemma 1);
+by (etac Little_Fermat 2);
+by (etac zdvd_not_zless 2);
+by (rewtac zprime_def);
+by Auto_tac;
+qed "inv_is_inv";
+
+Goal "[| p:zprime; #1<a; a<p-#1 |] ==> a ~= (inv p a)";
+by Safe_tac;
+by (cut_inst_tac [("a","a"),("p","p")] zcong_square 1);
+by (cut_inst_tac [("a","a"),("p","p")] inv_is_inv 3);
+by Auto_tac;
+by (subgoal_tac "a=#1" 1);
+by (res_inst_tac [("m","p")] zcong_zless_imp_eq 2);
+by (subgoal_tac "a=p-#1" 7);
+by (res_inst_tac [("m","p")] zcong_zless_imp_eq 8);
+by Auto_tac;
+qed "inv_distinct";
+
+Goal "[| p:zprime; #1<a; a<p-#1 |] ==> (inv p a) ~= #0";
+by Safe_tac;
+by (cut_inst_tac [("a","a"),("p","p")] inv_is_inv 1);
+by (rewtac zcong_def);
+by Auto_tac;
+by (subgoal_tac "~p dvd #1" 1);
+by (rtac zdvd_not_zless 2);
+by (subgoal_tac "p dvd #1" 1);
+by (stac (zdvd_zminus_iff RS sym) 2);
+by Auto_tac;
+qed "inv_not_0";
+
+Goal "[| p:zprime; #1<a; a<p-#1 |] ==> (inv p a) ~= #1";
+by Safe_tac;
+by (cut_inst_tac [("a","a"),("p","p")] inv_is_inv 1);
+by (Asm_full_simp_tac 4);
+by (subgoal_tac "a = #1" 4);
+by (rtac zcong_zless_imp_eq 5);
+by Auto_tac;
+qed "inv_not_1";
+
+Goalw [zcong_def] "[a*(p-#1) = #1](mod p) = [a = p-#1](mod p)";
+by (simp_tac (simpset() addsimps [zdiff_zdiff_eq,zdiff_zdiff_eq2,
+ zdiff_zmult_distrib2]) 1);
+by (res_inst_tac [("s","p dvd -((a+#1)+(p*(-a)))")] trans 1);
+by (simp_tac (simpset() addsimps [zmult_commute,zminus_zdiff_eq]) 1);
+by (stac zdvd_zminus_iff 1);
+by (stac zdvd_reduce 1);
+by (res_inst_tac [("s","p dvd ((a+#1)+(p*(-#1)))")] trans 1);
+by (stac zdvd_reduce 1);
+by Auto_tac;
+val lemma = result();
+
+Goal "[| p:zprime; #1<a; a<p-#1 |] ==> (inv p a) ~= p-#1";
+by Safe_tac;
+by (cut_inst_tac [("a","a"),("p","p")] inv_is_inv 1);
+by Auto_tac;
+by (asm_full_simp_tac (simpset() addsimps [lemma]) 1);
+by (subgoal_tac "a = p-#1" 1);
+by (rtac zcong_zless_imp_eq 2);
+by Auto_tac;
+qed "inv_not_p_minus_1";
+
+Goal "[| p:zprime; #1<a; a<p-#1 |] ==> #1<(inv p a)";
+by (case_tac "#0<=(inv p a)" 1);
+by (subgoal_tac "(inv p a) ~= #1" 1);
+by (subgoal_tac "(inv p a) ~= #0" 1);
+by (rtac zle_neq_implies_zless 1);
+by (stac (zle_add1_eq_le RS sym) 1);
+by (rtac zle_neq_implies_zless 1);
+by (rtac inv_not_0 4);
+by (rtac inv_not_1 7);
+by Auto_tac;
+by (rewrite_goals_tac [inv_def,zprime_def]);
+by (asm_full_simp_tac (simpset() addsimps [pos_mod_sign]) 1);
+qed "inv_g_1";
+
+Goal "[| p:zprime; #1<a; a<p-#1 |] ==> (inv p a)<p-#1";
+by (case_tac "(inv p a)<p" 1);
+by (rtac zle_neq_implies_zless 1);
+by (rtac inv_not_p_minus_1 2);
+by Auto_tac;
+by (rewrite_goals_tac [inv_def,zprime_def]);
+by (asm_full_simp_tac (simpset() addsimps [pos_mod_bound]) 1);
+qed "inv_less_p_minus_1";
+
+Goal "#5<=p ==> nat(p-#2)*nat(p-#2) = Suc(nat(p-#1)*nat(p-#3))";
+by (stac (int_int_eq RS sym) 1);
+by (asm_simp_tac (simpset() addsimps [zmult_int RS sym]) 1);
+by (simp_tac (simpset() addsimps [zdiff_zmult_distrib,
+ zdiff_zmult_distrib2]) 1);
+val lemma = result();
+
+Goal "[x^y = #1](mod p) --> [x^(y*z) = #1](mod p)";
+by (induct_tac "z" 1);
+by (auto_tac (claset(),simpset() addsimps [zpower_zadd_distrib]));
+by (subgoal_tac "zcong (x^y * x^(y*n)) (#1*#1) p" 1);
+by (rtac zcong_zmult 2);
+by (ALLGOALS Asm_full_simp_tac);
+qed_spec_mp "zcong_zpower_zmult";
+
+Goalw [inv_def] "[| p:zprime; #5<=p; #0<a; a<p |] ==> (inv p (inv p a)) = a";
+by (stac zpower_zmod 1);
+by (stac zpower_zpower 1);
+by (rtac zcong_zless_imp_eq 1);
+by (stac zcong_zmod 5);
+by (stac mod_mod_trivial 5);
+by (stac (zcong_zmod RS sym) 5);
+by (stac lemma 5);
+by (subgoal_tac "zcong (a * a^(nat (p - #1) * nat (p - #3))) (a*#1) p" 6);
+by (rtac zcong_zmult 7);
+by (rtac zcong_zpower_zmult 8);
+by (etac Little_Fermat 8);
+by (rtac zdvd_not_zless 8);
+by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [pos_mod_bound,
+ pos_mod_sign])));
+qed "inv_inv";
+
+
+(************* wset *************)
+
+val [wset_eq] = wset.simps;
+Delsimps wset.simps;
+
+val [prem1,prem2] =
+Goal "[| !!a p. P {} a p; \
+\ !!a p. [| #1<(a::int); P (wset (a-#1,p)) (a-#1) p |] \
+\ ==> P (wset (a,p)) a p|] \
+\ ==> P (wset (u,v)) u v";
+by (rtac wset.induct 1);
+by Safe_tac;
+by (case_tac "#1<a" 2);
+by (rtac prem2 2);
+by (ALLGOALS Asm_simp_tac);
+by (ALLGOALS (asm_simp_tac (simpset() addsimps [wset_eq,prem1])));
+qed "wset_induct";
+
+Goal "[| #1<a; b~:(wset (a-#1,p)) |] \
+\ ==> b:(wset (a,p)) --> b=a | b = inv p a";
+by (stac wset_eq 1);
+by (rewtac Let_def);
+by (Asm_simp_tac 1);
+qed_spec_mp "wset_mem_imp_or";
+
+Goal "#1<a ==> a:(wset(a,p))";
+by (stac wset_eq 1);
+by (rewtac Let_def);
+by (Asm_simp_tac 1);
+qed "wset_mem_mem";
+Addsimps [wset_mem_mem];
+
+Goal "[| #1<a; b:wset(a-#1,p) |] ==> b:wset(a,p)";
+by (stac wset_eq 1);
+by (rewtac Let_def);
+by Auto_tac;
+qed "wset_subset";
+
+Goal "p:zprime --> a<p-#1 --> b:(wset(a,p)) --> #1<b";
+by (res_inst_tac [("u","a"),("v","p")] wset_induct 1);
+by Auto_tac;
+by (case_tac "b=a" 1);
+by (case_tac "b=inv p a" 2);
+by (subgoal_tac "b=a | b = inv p a" 3);
+by (rtac wset_mem_imp_or 4);
+by (Asm_simp_tac 2);
+by (rtac inv_g_1 2);
+by Auto_tac;
+qed_spec_mp "wset_g_1";
+
+Goal "p:zprime --> a<p-#1 --> b:(wset(a,p)) --> b<p-#1";
+by (res_inst_tac [("u","a"),("v","p")] wset_induct 1);
+by Auto_tac;
+by (case_tac "b=a" 1);
+by (case_tac "b=inv p a" 2);
+by (subgoal_tac "b=a | b = inv p a" 3);
+by (rtac wset_mem_imp_or 4);
+by (Asm_simp_tac 2);
+by (rtac inv_less_p_minus_1 2);
+by Auto_tac;
+qed_spec_mp "wset_less";
+
+Goal "p:zprime --> a<p-#1 --> #1<b --> b<=a --> b:(wset(a,p))";
+by (res_inst_tac [("u","a"),("v","p")] wset.induct 1);
+by Auto_tac;
+by (subgoal_tac "b=a" 1);
+by (rtac zle_anti_sym 2);
+by (rtac wset_subset 4);
+by (Asm_simp_tac 1);
+by Auto_tac;
+qed_spec_mp "wset_mem";
+
+Goal "p:zprime --> #5<=p --> a<p-#1 --> b:(wset (a,p)) \
+\ --> (inv p b):(wset (a,p))";
+by (res_inst_tac [("u","a"),("v","p")] wset_induct 1);
+by Auto_tac;
+by (case_tac "b=a" 1);
+by (stac wset_eq 1);
+by (rewtac Let_def);
+by (rtac wset_subset 3);
+by Auto_tac;
+by (case_tac "b = inv p a" 1);
+by (Asm_simp_tac 1);
+by (stac inv_inv 1);
+by (subgoal_tac "b=a | b = inv p a" 6);
+by (rtac wset_mem_imp_or 7);
+by Auto_tac;
+qed_spec_mp "wset_mem_inv_mem";
+
+Goal "[| p:zprime; #5<=p; a<p-#1; #1<b; b<p-#1; (inv p b):(wset (a,p)) |] \
+\ ==> b:(wset (a,p))";
+by (res_inst_tac [("s","inv p (inv p b)"),("t","b")] subst 1);
+by (rtac wset_mem_inv_mem 2);
+by (rtac inv_inv 1);
+by (ALLGOALS (Asm_simp_tac));
+qed "wset_inv_mem_mem";
+
+Goal "finite (wset (a,p))";
+by (res_inst_tac [("u","a"),("v","p")] wset_induct 1);
+by (stac wset_eq 2);
+by (rewtac Let_def);
+by Auto_tac;
+qed "wset_fin";
+
+Goal "p:zprime --> #5<=p --> a<p-#1 --> [setprod (wset (a,p)) = #1](mod p)";
+by (res_inst_tac [("u","a"),("v","p")] wset_induct 1);
+by (stac wset_eq 2);
+by (rewtac Let_def);
+by Auto_tac;
+by (stac setprod_insert 1);
+by (stac setprod_insert 3);
+by (subgoal_tac "zcong (a * (inv p a) * setprod(wset(a-#1,p))) (#1*#1) p" 5);
+by (asm_full_simp_tac (simpset() addsimps [zmult_assoc]) 5);
+by (rtac zcong_zmult 5);
+by (rtac inv_is_inv 5);
+by (Clarify_tac 4);
+by (subgoal_tac "a:wset(a-#1,p)" 4);
+by (rtac wset_inv_mem_mem 5);
+by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [wset_fin])));
+by (rtac inv_distinct 1);
+by Auto_tac;
+qed_spec_mp "wset_zcong_prod_1";
+
+Goal "p:zprime ==> d22set(p-#2) = wset(p-#2,p)";
+by Safe_tac;
+by (etac wset_mem 1);
+by (rtac d22set_g_1 2);
+by (rtac d22set_le 3);
+by (rtac d22set_mem 4);
+by (etac wset_g_1 4);
+by (stac (zle_add1_eq_le RS sym) 6);
+by (subgoal_tac "p-#2+#1 = p-#1" 6);
+by (Asm_simp_tac 6);
+by (etac wset_less 6);
+by Auto_tac;
+qed "d22set_eq_wset";
+
+(********** Wilson *************)
+
+Goal "[| z-#1<=w; z-#1~=w |] ==> z<=(w::int)";
+by (stac (zle_add1_eq_le RS sym) 1);
+by (rtac zle_neq_implies_zless 1);
+by Auto_tac;
+val lemma = result();
+
+Goalw [zprime_def,dvd_def] "[| p : zprime; p ~= #2; p ~= #3 |] ==> #5<=p";
+by (case_tac "p=#4" 1);
+by Auto_tac;
+by (rtac notE 1);
+by (assume_tac 2);
+by (Simp_tac 1);
+by (res_inst_tac [("x","#2")] exI 1);
+by Safe_tac;
+by (res_inst_tac [("x","#2")] exI 1);
+by Auto_tac;
+by (rtac lemma 1);
+by (rtac lemma 1);
+by (rtac lemma 1);
+by Auto_tac;
+qed "prime_g_5";
+
+Goal "p:zprime ==> [zfact(p-#1) = #-1] (mod p)";
+by (subgoal_tac "[(p-#1)*zfact(p-#2) = #-1*#1] (mod p)" 1);
+by (rtac zcong_zmult 2);
+by (SELECT_GOAL (rewtac zprime_def) 1);
+by (stac zfact_eq 1);
+by (res_inst_tac [("t","p-#1-#1"),("s","p-#2")] subst 1);
+by Auto_tac;
+by (SELECT_GOAL (rewtac zcong_def) 1);
+by (Asm_simp_tac 1);
+by (case_tac "p=#2" 1);
+by (asm_full_simp_tac (simpset() addsimps [zfact_eq]) 1);
+by (case_tac "p=#3" 1);
+by (asm_full_simp_tac (simpset() addsimps [zfact_eq]) 1);
+by (subgoal_tac "#5<=p" 1);
+by (etac prime_g_5 2);
+by (stac (d22set_prod_zfact RS sym) 1);
+by (stac d22set_eq_wset 1);
+by (rtac wset_zcong_prod_1 2);
+by Auto_tac;
+qed "WilsonRuss";
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/NumberTheory/WilsonRuss.thy Thu Aug 03 10:46:01 2000 +0200
@@ -0,0 +1,21 @@
+(* Title: WilsonRuss.thy
+ ID: $Id$
+ Author: Thomas M. Rasmussen
+ Copyright 2000 University of Cambridge
+*)
+
+WilsonRuss = EulerFermat +
+
+consts
+ inv :: "[int,int] => int"
+ wset :: "int*int=>int set"
+
+defs
+ inv_def "inv p a == (a ^ (nat (p - #2))) mod p"
+
+recdef wset "measure ((%(a,p).(nat a)) ::int*int=>nat)"
+ "wset (a,p) = (if #1<a then let ws = wset (a-#1,p) in
+ (if a:ws then ws else insert a (insert (inv p a) ws))
+ else {})"
+
+end