# HG changeset patch # User paulson # Date 965292361 -7200 # Node ID 4d01dbf6ded7b4f48b7d68b0ee6289429c76f379 # Parent 7903ca5fecf10ebc9db9f584df2adbbdb75c3457 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen diff -r 7903ca5fecf1 -r 4d01dbf6ded7 src/HOL/NumberTheory/BijectionRel.ML --- /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"; + + + + diff -r 7903ca5fecf1 -r 4d01dbf6ded7 src/HOL/NumberTheory/BijectionRel.thy --- /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 + diff -r 7903ca5fecf1 -r 4d01dbf6ded7 src/HOL/NumberTheory/Chinese.ML --- /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 [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 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 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 (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 (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 (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"; diff -r 7903ca5fecf1 -r 4d01dbf6ded7 src/HOL/NumberTheory/Chinese.thy --- /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 P (BnorRset(a,m)) a m) |] \ +\ ==> P (BnorRset(u,v)) u v"; +by (rtac BnorRset.induct 1); +by Safe_tac; +by (case_tac "#0 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~: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 #0 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 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 (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 a:A --> zgcd (a,m) = #1"; +by (rtac RsetR.induct 1); +by Auto_tac; +qed_spec_mp "RRset_gcd"; + +Goal "[| A : RsetR m; #0 (%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 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 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 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 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 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 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 (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 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 a 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 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

(ALL b. #0 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"; + diff -r 7903ca5fecf1 -r 4d01dbf6ded7 src/HOL/NumberTheory/EulerFermat.thy --- /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 [int, int] => bool +defs zcongm_def "zcongm m == (%a b. zcong a b m)" + +end diff -r 7903ca5fecf1 -r 4d01dbf6ded7 src/HOL/NumberTheory/IntFact.ML --- /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 #1 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~:(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<=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 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 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 = (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 ~n dvd (m::int)"; +by Auto_tac; +by (subgoal_tac "#0 zgcd(#0,m) = m"; +by (auto_tac (claset(), simpset() addsimps zgcd.simps)); +qed "zgcd_0_left"; +Addsimps [zgcd_0_left]; + +Goal "#0 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 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 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 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 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 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 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 zgcd(k*n,m) = #1"; +by (asm_simp_tac (simpset() addsimps [zgcd_zmult_cancel]) 1); +qed "zgcd_zgcd_zmult"; + +Goal "#0 (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=#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 [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 [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 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 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 = b] (mod m) "; +by (rtac zdvd_not_zless 1); +by Auto_tac; +qed "zcong_not"; + +Goalw [zcong_def,dvd_def] "[| #0<=a; a a = #0"; +by Auto_tac; +by (subgoal_tac "#0 (EX! b. #0<=b & b 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 [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 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 r = s*m + t*n"; +by (etac xzgcda_linear 1); +by (assume_tac 1); +by Auto_tac; +qed "xzgcd_linear"; + +Goal "[| #0 (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 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 EX! x. #0<=x & x 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

m=#1 | m=p)}" + + zcong_def "[a=b] (mod m) == m dvd (a-b)" + +end diff -r 7903ca5fecf1 -r 4d01dbf6ded7 src/HOL/NumberTheory/README --- /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 diff -r 7903ca5fecf1 -r 4d01dbf6ded7 src/HOL/NumberTheory/ROOT.ML --- /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"; diff -r 7903ca5fecf1 -r 4d01dbf6ded7 src/HOL/NumberTheory/WilsonBij.ML --- /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 #0 <= (inv p a) & (inv p a)

(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 (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 (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 #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 (inv p a) #0<=(x::int)"; +by Auto_tac; +val l1 = result(); + +Goal "#1 #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"; diff -r 7903ca5fecf1 -r 4d01dbf6ded7 src/HOL/NumberTheory/WilsonBij.thy --- /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 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*(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 ~= (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 (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 (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 (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 #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 (inv p a) 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 (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 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:(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 b:wset(a,p)"; +by (stac wset_eq 1); +by (rewtac Let_def); +by Auto_tac; +qed "wset_subset"; + +Goal "p:zprime --> a b:(wset(a,p)) --> #1 a b:(wset(a,p)) --> b a #1 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 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 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 [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"; diff -r 7903ca5fecf1 -r 4d01dbf6ded7 src/HOL/NumberTheory/WilsonRuss.thy --- /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