# HG changeset patch # User wenzelm # Date 981311473 -3600 # Node ID 7eef34adb852563c173b2166f40a8ce46a4394b1 # Parent 2f4976370b7a3d960be3e28f012cae1c7db7e99a HOL-NumberTheory: converted to new-style format and proper document setup; diff -r 2f4976370b7a -r 7eef34adb852 src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Sat Feb 03 17:43:34 2001 +0100 +++ b/src/HOL/IsaMakefile Sun Feb 04 19:31:13 2001 +0100 @@ -180,7 +180,7 @@ $(LOG)/HOL-Library.gz: $(OUT)/HOL Library/Accessible_Part.thy \ Library/Library.thy Library/List_Prefix.thy Library/Multiset.thy \ - Library/Quotient.thy Library/Ring_and_Field.thy \ + Library/Permutation.thy Library/Quotient.thy Library/Ring_and_Field.thy \ Library/Ring_and_Field_Example.thy Library/README.html \ Library/Nested_Environment.thy Library/Rational_Numbers.thy Library/ROOT.ML \ Library/While_Combinator.thy @@ -205,8 +205,8 @@ $(LOG)/HOL-Induct.gz: $(OUT)/HOL \ Induct/Com.ML Induct/Com.thy Induct/Comb.ML Induct/Comb.thy \ Induct/Exp.ML Induct/Exp.thy Induct/LFilter.ML Induct/LFilter.thy \ - Induct/LList.ML Induct/LList.thy Induct/Mutil.thy Induct/Perm.ML \ - Induct/Perm.thy Induct/PropLog.ML Induct/PropLog.thy Induct/ROOT.ML \ + Induct/LList.ML Induct/LList.thy Induct/Mutil.thy \ + Induct/PropLog.ML Induct/PropLog.thy Induct/ROOT.ML \ Induct/Sexp.ML Induct/Sexp.thy Induct/Sigma_Algebra.thy \ Induct/SList.ML Induct/SList.thy Induct/ABexp.thy Induct/Term.thy \ Induct/Tree.thy Induct/document/root.tex @@ -239,15 +239,11 @@ HOL-NumberTheory: HOL $(LOG)/HOL-NumberTheory.gz $(LOG)/HOL-NumberTheory.gz: $(OUT)/HOL \ - NumberTheory/Fib.ML NumberTheory/Fib.thy NumberTheory/Primes.thy \ - NumberTheory/Factorization.ML NumberTheory/Factorization.thy \ - NumberTheory/BijectionRel.ML NumberTheory/BijectionRel.thy \ - NumberTheory/Chinese.ML NumberTheory/Chinese.thy \ - NumberTheory/EulerFermat.ML NumberTheory/EulerFermat.thy \ - NumberTheory/IntFact.ML NumberTheory/IntFact.thy \ - NumberTheory/IntPrimes.ML NumberTheory/IntPrimes.thy \ - NumberTheory/WilsonBij.ML NumberTheory/WilsonBij.thy \ - NumberTheory/WilsonRuss.ML NumberTheory/WilsonRuss.thy \ + Library/Permutation.thy NumberTheory/Fib.thy NumberTheory/Primes.thy \ + NumberTheory/Factorization.thy NumberTheory/BijectionRel.thy \ + NumberTheory/Chinese.thy NumberTheory/EulerFermat.thy \ + NumberTheory/IntFact.thy NumberTheory/IntPrimes.thy \ + NumberTheory/WilsonBij.thy NumberTheory/WilsonRuss.thy \ NumberTheory/ROOT.ML @$(ISATOOL) usedir $(OUT)/HOL NumberTheory diff -r 2f4976370b7a -r 7eef34adb852 src/HOL/NumberTheory/BijectionRel.ML --- a/src/HOL/NumberTheory/BijectionRel.ML Sat Feb 03 17:43:34 2001 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,182 +0,0 @@ -(* 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 2f4976370b7a -r 7eef34adb852 src/HOL/NumberTheory/BijectionRel.thy --- a/src/HOL/NumberTheory/BijectionRel.thy Sat Feb 03 17:43:34 2001 +0100 +++ b/src/HOL/NumberTheory/BijectionRel.thy Sun Feb 04 19:31:13 2001 +0100 @@ -1,46 +1,235 @@ -(* Title: BijectionRel.thy +(* Title: HOL/NumberTheory/BijectionRel.thy ID: $Id$ - Author: Thomas M. Rasmussen - Copyright 2000 University of Cambridge + Author: Thomas M. Rasmussen + Copyright 2000 University of Cambridge *) -BijectionRel = Main + +header {* Bijections between sets *} + +theory BijectionRel = Main: + +text {* + Inductive definitions of bijections between two different sets and + between the same set. Theorem for relating the two definitions. + + \bigskip +*} consts - bijR :: "(['a, 'b] => bool) => ('a set * 'b set) set" + 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" + intros + empty [simp]: "({}, {}) \ bijR P" + insert: "P a b ==> a \ A ==> b \ B ==> (A, B) \ bijR P + ==> (insert a A, insert b B) \ bijR P" + +text {* + Add extra condition to @{term insert}: @{term "\b \ B. \ P a b"} + (and similar for @{term A}). +*} -(* Add extra condition to insert: ALL b:B. ~(P a b) (and similar for A) *) +constdefs + bijP :: "('a => 'a => bool) => 'a set => bool" + "bijP P F == \a b. a \ F \ P a b --> b \ F" + + uniqP :: "('a => 'a => bool) => bool" + "uniqP P == \a b c d. P a b \ P c d --> (a = c) = (b = d)" + + symP :: "('a => 'a => bool) => bool" + "symP P == \a b. P a b = P b 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" + 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" + intros + empty [simp]: "{} \ 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" + + +text {* \medskip @{term bijR} *} + +lemma fin_bijRl: "(A, B) \ bijR P ==> finite A" + apply (erule bijR.induct) + apply auto + done + +lemma fin_bijRr: "(A, B) \ bijR P ==> finite B" + apply (erule bijR.induct) + apply auto + done + +lemma aux_induct: + "finite F ==> F \ A ==> P {} ==> + (!!F a. F \ A ==> a \ A ==> a \ F ==> P F ==> P (insert a F)) + ==> P F" +proof - + case antecedent + assume major: "finite F" + and subs: "F \ A" + show ?thesis + apply (rule subs [THEN rev_mp]) + apply (rule major [THEN finite_induct]) + apply (blast intro: antecedent)+ + done +qed + +lemma aux: "A \ B ==> a \ A ==> a \ B ==> inj_on f B ==> f a \ f ` A" + apply (unfold inj_on_def) + apply auto + done + +lemma aux: + "\a. a \ A --> P a (f a) ==> inj_on f A ==> finite A ==> F <= A + ==> (F, f ` F) \ bijR P" + apply (rule_tac F = F and A = A in aux_induct) + apply (rule finite_subset) + apply auto + apply (rule bijR.insert) + apply (rule_tac [3] aux) + apply auto + done + +lemma inj_func_bijR: + "\a. a \ A --> P a (f a) ==> inj_on f A ==> finite A + ==> (A, f ` A) \ bijR P" + apply (rule aux) + apply auto + done + + +text {* \medskip @{term bijER} *} + +lemma fin_bijER: "A \ bijER P ==> finite A" + apply (erule bijER.induct) + apply auto + done + +lemma aux1: + "a \ A ==> a \ B ==> F \ insert a A ==> F \ insert a B ==> a \ F + ==> \C. F = insert a C \ a \ C \ C <= A \ C <= B" + apply (rule_tac x = "F - {a}" in exI) + apply auto + done + +lemma aux2: "a \ b ==> a \ A ==> b \ B ==> a \ F ==> b \ F + ==> F \ insert a A ==> F \ insert b B + ==> \C. F = insert a (insert b C) \ a \ C \ b \ C \ C \ A \ C \ B" + apply (rule_tac x = "F - {a, b}" in exI) + apply auto + done + +lemma aux_uniq: "uniqP P ==> P a b ==> P c d ==> (a = c) = (b = d)" + apply (unfold uniqP_def) + apply auto + done + +lemma aux_sym: "symP P ==> P a b = P b a" + apply (unfold symP_def) + apply auto + done + +lemma aux_in1: + "uniqP P ==> b \ C ==> P b b ==> bijP P (insert b C) ==> bijP P C" + apply (unfold bijP_def) + apply auto + apply (subgoal_tac "b \ a") + prefer 2 + apply clarify + apply (simp add: aux_uniq) + apply auto + done + +lemma aux_in2: + "symP P ==> uniqP P ==> a \ C ==> b \ C ==> a \ b ==> P a b + ==> bijP P (insert a (insert b C)) ==> bijP P C" + apply (unfold bijP_def) + apply auto + apply (subgoal_tac "aa \ a") + prefer 2 + apply clarify + apply (subgoal_tac "aa \ b") + prefer 2 + apply clarify + apply (simp add: aux_uniq) + apply (subgoal_tac "ba \ a") + apply auto + apply (subgoal_tac "P a aa") + prefer 2 + apply (simp add: aux_sym) + apply (subgoal_tac "b = aa") + apply (rule_tac [2] iffD1) + apply (rule_tac [2] a = a and c = a and P = P in aux_uniq) + apply auto + done + +lemma aux: "\a b. Q a \ P a b --> R b ==> P a b ==> Q a ==> R b" + apply auto + done + +lemma aux_bij: "bijP P F ==> symP P ==> P a b ==> (a \ F) = (b \ F)" + apply (unfold bijP_def) + apply (rule iffI) + apply (erule_tac [!] aux) + apply simp_all + apply (rule iffD2) + apply (rule_tac P = P in aux_sym) + apply simp_all + done + + +lemma aux_bijRER: + "(A, B) \ bijR P ==> uniqP P ==> symP P + ==> \F. bijP P F \ F \ A \ F \ B --> F \ bijER P" + apply (erule bijR.induct) + apply simp + apply (case_tac "a = b") + apply clarify + apply (case_tac "b \ F") + prefer 2 + apply (rotate_tac -1) + apply (simp add: subset_insert) + apply (cut_tac F = F and a = b and A = A and B = B in aux1) + prefer 6 + apply clarify + apply (rule bijER.insert1) + apply simp_all + apply (subgoal_tac "bijP P C") + apply simp + apply (rule aux_in1) + apply simp_all + apply clarify + apply (case_tac "a \ F") + apply (case_tac [!] "b \ F") + apply (rotate_tac [2-4] -2) + apply (cut_tac F = F and a = a and b = b and A = A and B = B + in aux2) + apply (simp_all add: subset_insert) + apply clarify + apply (rule bijER.insert2) + apply simp_all + apply (subgoal_tac "bijP P C") + apply simp + apply (rule aux_in2) + apply simp_all + apply (subgoal_tac "b \ F") + apply (rule_tac [2] iffD1) + apply (rule_tac [2] a = a and F = F and P = P in aux_bij) + apply (simp_all (no_asm_simp)) + apply (subgoal_tac [2] "a \ F") + apply (rule_tac [3] iffD2) + apply (rule_tac [3] b = b and F = F and P = P in aux_bij) + apply auto + done + +lemma bijR_bijER: + "(A, A) \ bijR P ==> + bijP P A ==> uniqP P ==> symP P ==> A \ bijER P" + apply (cut_tac A = A and B = A and P = P in aux_bijRER) + apply auto + done end - diff -r 2f4976370b7a -r 7eef34adb852 src/HOL/NumberTheory/Chinese.ML --- a/src/HOL/NumberTheory/Chinese.ML Sat Feb 03 17:43:34 2001 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,180 +0,0 @@ -(* 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? -*) - - -(*** 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) --> \ -\ 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 Clarify_tac); -by (subgoal_tac "k=j" 1 THEN ALLGOALS Asm_simp_tac); -by (case_tac "Suc (k+n) = j" 1); -by (subgoal_tac "funsum f k n = #0" 1); -by (rtac funsum_zero 2); -by (subgoal_tac "f (Suc (k+n)) = #0" 3); -by (subgoal_tac "j<=k+n" 3); -by (arith_tac 4); -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 order_less_imp_le 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]) 1); -by (stac zgcd_commute 2); -by (rtac funprod_zgcd 2); -by (auto_tac (claset(), - simpset() addsimps [m_cond_def,km_cond_def,lincong_sol_def])); -qed_spec_mp "zcong_funprod"; - - -(* Chinese: Existence *) - -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 (ALLGOALS Asm_simp_tac); -by Safe_tac; -by (stac zgcd_zmult_cancel 3); -by (ALLGOALS (rtac funprod_zgcd)); -by Safe_tac; -by (ALLGOALS Asm_full_simp_tac); -by (subgoal_tac "ia<=n" 3); -by (arith_tac 4); -by (subgoal_tac "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 (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 "[| 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 (ex1_implies_ex RS someI_ex) 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 2f4976370b7a -r 7eef34adb852 src/HOL/NumberTheory/Chinese.thy --- a/src/HOL/NumberTheory/Chinese.thy Sat Feb 03 17:43:34 2001 +0100 +++ b/src/HOL/NumberTheory/Chinese.thy Sun Feb 04 19:31:13 2001 +0100 @@ -1,55 +1,260 @@ -(* Title: Chinese.thy +(* Title: HOL/NumberTheory/Chinese.thy ID: $Id$ - Author: Thomas M. Rasmussen - Copyright 2000 University of Cambridge + Author: Thomas M. Rasmussen + Copyright 2000 University of Cambridge *) -Chinese = IntPrimes + +header {* The Chinese Remainder Theorem *} + +theory Chinese = IntPrimes: + +text {* + The Chinese Remainder Theorem for an arbitrary finite number of + equations. (The one-equation case is included in theory @{text + IntPrimes}. Uses functions for indexing.\footnote{Maybe @{term + funprod} and @{term funsum} should be based on general @{term fold} + on indices?} +*} + + +subsection {* Definitions *} consts - funprod :: (nat => int) => nat => nat => int - funsum :: (nat => int) => nat => nat => int + 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)" + "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)" - + "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 + 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 + 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)" + m_cond_def: + "m_cond n mf == + (\i. i \ n --> #0 < mf i) \ + (\i j. i \ n \ j \ n \ i \ j --> zgcd (mf i, mf j) = #1)" + + km_cond_def: + "km_cond n kf mf == \i. i \ n --> zgcd (kf i, mf i) = #1" + + lincong_sol_def: + "lincong_sol n kf bf mf x == \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 + (SOME 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" + + +text {* \medskip @{term funprod} and @{term funsum} *} + +lemma funprod_pos: "(\i. i \ n --> #0 < mf i) ==> #0 < funprod mf 0 n" + apply (induct n) + apply auto + apply (simp add: int_0_less_mult_iff) + done + +lemma funprod_zgcd [rule_format (no_asm)]: + "(\i. k \ i \ i \ k + l --> zgcd (mf i, mf m) = #1) --> + zgcd (funprod mf k l, mf m) = #1" + apply (induct l) + apply simp_all + apply (rule impI)+ + apply (subst zgcd_zmult_cancel) + apply auto + done - km_cond_def "km_cond n kf mf == (ALL i. i<=n --> zgcd(kf i,mf i) = #1)" +lemma funprod_zdvd [rule_format]: + "k \ i --> i \ k + l --> mf i dvd funprod mf k l" + apply (induct l) + apply auto + apply (rule_tac [2] zdvd_zmult2) + apply (rule_tac [3] zdvd_zmult) + apply (subgoal_tac "i = k") + apply (subgoal_tac [3] "i = Suc (k + n)") + apply (simp_all (no_asm_simp)) + done + +lemma funsum_mod: + "funsum f k l mod m = funsum (\i. (f i) mod m) k l mod m" + apply (induct l) + apply auto + apply (rule trans) + apply (rule zmod_zadd1_eq) + apply simp + apply (rule zmod_zadd_right_eq [symmetric]) + done - lincong_sol_def "lincong_sol n kf bf mf x == - (ALL i. i<=n --> zcong ((kf i)*x) (bf i) (mf i))" +lemma funsum_zero [rule_format (no_asm)]: + "(\i. k \ i \ i \ k + l --> f i = #0) --> (funsum f k l) = #0" + apply (induct l) + apply auto + done + +lemma funsum_oneelem [rule_format (no_asm)]: + "k \ j --> j \ k + l --> + (\i. k \ i \ i \ k + l \ i \ j --> f i = #0) --> + funsum f k l = f j" + apply (induct l) + prefer 2 + apply clarify + defer + apply clarify + apply (subgoal_tac "k = j") + apply (simp_all (no_asm_simp)) + apply (case_tac "Suc (k + n) = j") + apply (subgoal_tac "funsum f k n = #0") + apply (rule_tac [2] funsum_zero) + apply (subgoal_tac [3] "f (Suc (k + n)) = #0") + apply (subgoal_tac [3] "j \ k + n") + prefer 4 + apply arith + apply auto + done + + +subsection {* Chinese: uniqueness *} - 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)))))" +lemma aux: + "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)" + apply (unfold m_cond_def km_cond_def lincong_sol_def) + apply (rule iffD1) + apply (rule_tac k = "kf n" in zcong_cancel2) + apply (rule_tac [3] b = "bf n" in zcong_trans) + prefer 4 + apply (subst zcong_sym) + defer + apply (rule order_less_imp_le) + apply simp_all + done + +lemma zcong_funprod [rule_format]: + "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)" + apply (induct n) + apply (simp_all (no_asm)) + apply (blast intro: aux) + apply (rule impI)+ + apply (rule zcong_zgcd_zmult_zmod) + apply (blast intro: aux) + prefer 2 + apply (subst zgcd_commute) + apply (rule funprod_zgcd) + apply (auto simp add: m_cond_def km_cond_def lincong_sol_def) + done + + +subsection {* Chinese: existence *} + +lemma unique_xi_sol: + "0 < n ==> i \ n ==> m_cond n mf ==> km_cond n kf mf + ==> \!x. #0 \ x \ x < mf i \ [kf i * mhf mf n i * x = bf i] (mod mf i)" + apply (rule zcong_lineq_unique) + apply (tactic {* stac (thm "zgcd_zmult_cancel") 2 *}) + apply (unfold m_cond_def km_cond_def mhf_def) + apply (simp_all (no_asm_simp)) + apply safe + apply (tactic {* stac (thm "zgcd_zmult_cancel") 3 *}) + apply (rule_tac [!] funprod_zgcd) + apply safe + apply simp_all + apply (subgoal_tac [3] "ia \ n") + prefer 4 + apply arith + apply (subgoal_tac "i i \ n ==> j \ n ==> j \ i ==> mf j dvd mhf mf n i" + apply (unfold mhf_def) + apply (case_tac "i = 0") + apply (case_tac [2] "i = n") + apply (simp_all (no_asm_simp)) + apply (case_tac [3] "j < i") + apply (rule_tac [3] zdvd_zmult2) + apply (rule_tac [4] zdvd_zmult) + apply (rule_tac [!] funprod_zdvd) + apply arith+ + done + +lemma x_sol_lin: + "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" + apply (unfold x_sol_def) + apply (subst funsum_mod) + apply (subst funsum_oneelem) + apply auto + apply (subst zdvd_iff_zmod_eq_0 [symmetric]) + apply (rule zdvd_zmult) + apply (rule aux) + apply auto + done + + +subsection {* Chinese *} - x_sol_def "x_sol n kf bf mf == - (funsum (%i. (xilin_sol i n kf bf mf)*(mhf mf n i)) 0 n)" +lemma chinese_remainder: + "0 < n ==> m_cond n mf ==> km_cond n kf mf + ==> \!x. #0 \ x \ x < funprod mf 0 n \ lincong_sol n kf bf mf x" + apply safe + apply (rule_tac [2] m = "funprod mf 0 n" in zcong_zless_imp_eq) + apply (rule_tac [6] zcong_funprod) + apply auto + apply (rule_tac x = "x_sol n kf bf mf mod funprod mf 0 n" in exI) + apply (unfold lincong_sol_def) + apply safe + apply (tactic {* stac (thm "zcong_zmod") 3 *}) + apply (tactic {* stac (thm "zmod_zmult_distrib") 3 *}) + apply (tactic {* stac (thm "zmod_zdvd_zmod") 3 *}) + apply (tactic {* stac (thm "x_sol_lin") 5 *}) + apply (tactic {* stac (thm "zmod_zmult_distrib" RS sym) 7 *}) + apply (tactic {* stac (thm "zcong_zmod" RS sym) 7 *}) + apply (subgoal_tac [7] + "#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)") + prefer 7 + apply (simp add: zmult_ac) + apply (unfold xilin_sol_def) + apply (tactic {* Asm_simp_tac 7 *}) + apply (rule_tac [7] ex1_implies_ex [THEN someI_ex]) + apply (rule_tac [7] unique_xi_sol) + apply (rule_tac [4] funprod_zdvd) + apply (unfold m_cond_def) + apply (rule funprod_pos [THEN pos_mod_sign]) + apply (rule_tac [2] funprod_pos [THEN pos_mod_bound]) + apply auto + done end diff -r 2f4976370b7a -r 7eef34adb852 src/HOL/NumberTheory/EulerFermat.thy --- a/src/HOL/NumberTheory/EulerFermat.thy Sat Feb 03 17:43:34 2001 +0100 +++ b/src/HOL/NumberTheory/EulerFermat.thy Sun Feb 04 19:31:13 2001 +0100 @@ -1,46 +1,381 @@ -(* Title: EulerFermat.thy +(* Title: HOL/NumberTheory/EulerFermat.thy ID: $Id$ - Author: Thomas M. Rasmussen - Copyright 2000 University of Cambridge + Author: Thomas M. Rasmussen + Copyright 2000 University of Cambridge *) -EulerFermat = BijectionRel + IntFact + +header {* Fermat's Little Theorem extended to Euler's Totient function *} + +theory EulerFermat = BijectionRel + IntFact: + +text {* + Fermat's Little Theorem extended to Euler's Totient function. More + abstract approach than Boyer-Moore (which seems necessary to achieve + the extended version). +*} + + +subsection {* Definitions and lemmas *} 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 + 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" + intros + empty [simp]: "{} \ RsetR m" + insert: "A \ RsetR m ==> zgcd (a, m) = #1 ==> + \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, 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)" + 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 + SOME b. zcong a b m \ b \ norRRset m + else #0)" + +constdefs + zcongm :: "int => int => int => bool" + "zcongm m == \a b. zcong a b m" + +lemma abs_eq_1_iff [iff]: "(abs z = (#1::int)) = (z = #1 \ z = #-1)" + -- {* LCP: not sure why this lemma is needed now *} + apply (auto simp add: zabs_def) + done + + +text {* \medskip @{text norRRset} *} + +declare BnorRset.simps [simp del] + +lemma BnorRset_induct: + "(!!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" +proof - + case antecedent + show ?thesis + apply (rule BnorRset.induct) + apply safe + apply (case_tac [2] "#0 < a") + apply (rule_tac [2] antecedent) + apply simp_all + apply (simp_all add: BnorRset.simps antecedent) + done +qed + +lemma Bnor_mem_zle [rule_format]: "b \ BnorRset (a, m) --> b \ a" + apply (induct a m rule: BnorRset_induct) + prefer 2 + apply (subst BnorRset.simps) + apply (unfold Let_def) + apply auto + done + +lemma Bnor_mem_zle_swap: "a < b ==> b \ BnorRset (a, m)" + apply (auto dest: Bnor_mem_zle) + done + +lemma Bnor_mem_zg [rule_format]: "b \ BnorRset (a, m) --> #0 < b" + apply (induct a m rule: BnorRset_induct) + prefer 2 + apply (subst BnorRset.simps) + apply (unfold Let_def) + apply auto + done + +lemma Bnor_mem_if [rule_format]: + "zgcd (b, m) = #1 --> #0 < b --> b \ a --> b \ BnorRset (a, m)" + apply (induct a m rule: BnorRset.induct) + apply auto + apply (case_tac "a = b") + prefer 2 + apply (simp add: order_less_le) + apply (simp (no_asm_simp)) + prefer 2 + apply (subst BnorRset.simps) + defer + apply (subst BnorRset.simps) + apply (unfold Let_def) + apply auto + done - noXRRset_def "noXRRset m x == (%a. a*x)`(norRRset m)" +lemma Bnor_in_RsetR [rule_format]: "a < m --> BnorRset (a, m) \ RsetR m" + apply (induct a m rule: BnorRset_induct) + apply simp + apply (subst BnorRset.simps) + apply (unfold Let_def) + apply auto + apply (rule RsetR.insert) + apply (rule_tac [3] allI) + apply (rule_tac [3] impI) + apply (rule_tac [3] zcong_not) + apply (subgoal_tac [6] "a' \ a - #1") + apply (rule_tac [7] Bnor_mem_zle) + apply (rule_tac [5] Bnor_mem_zg) + apply auto + done + +lemma Bnor_fin: "finite (BnorRset (a, m))" + apply (induct a m rule: BnorRset_induct) + prefer 2 + apply (subst BnorRset.simps) + apply (unfold Let_def) + apply auto + done + +lemma aux: "a \ b - #1 ==> a < (b::int)" + apply auto + done - phi_def "phi m == card (norRRset m)" +lemma norR_mem_unique: + "#1 < m ==> + zgcd (a, m) = #1 ==> \!b. [a = b] (mod m) \ b \ norRRset m" + apply (unfold norRRset_def) + apply (cut_tac a = a and m = m in zcong_zless_unique) + apply auto + apply (rule_tac [2] m = m in zcong_zless_imp_eq) + apply (auto intro: Bnor_mem_zle Bnor_mem_zg zcong_trans + order_less_imp_le aux simp add: zcong_sym) + apply (rule_tac "x" = "b" in exI) + apply safe + apply (rule Bnor_mem_if) + apply (case_tac [2] "b = #0") + apply (auto intro: order_less_le [THEN iffD2]) + prefer 2 + apply (simp only: zcong_def) + apply (subgoal_tac "zgcd (a, m) = m") + prefer 2 + apply (subst zdvd_iff_zgcd [symmetric]) + apply (rule_tac [4] zgcd_zcong_zgcd) + apply (simp_all add: zdvd_zminus_iff zcong_sym) + done + + +text {* \medskip @{term noXRRset} *} + +lemma RRset_gcd [rule_format]: + "is_RRset A m ==> a \ A --> zgcd (a, m) = #1" + apply (unfold is_RRset_def) + apply (rule RsetR.induct) + apply auto + done + +lemma RsetR_zmult_mono: + "A \ RsetR m ==> + #0 < m ==> zgcd (x, m) = #1 ==> (\a. a * x) ` A \ RsetR m" + apply (erule RsetR.induct) + apply simp_all + apply (rule RsetR.insert) + apply auto + apply (blast intro: zgcd_zgcd_zmult) + apply (simp add: zcong_cancel) + done + +lemma card_nor_eq_noX: + "#0 < m ==> + zgcd (x, m) = #1 ==> card (noXRRset m x) = card (norRRset m)" + apply (unfold norRRset_def noXRRset_def) + apply (rule card_image) + apply (auto simp add: inj_on_def Bnor_fin) + apply (simp add: BnorRset.simps) + done + +lemma noX_is_RRset: + "#0 < m ==> zgcd (x, m) = #1 ==> is_RRset (noXRRset m x) m" + apply (unfold is_RRset_def phi_def) + apply (auto simp add: card_nor_eq_noX) + apply (unfold noXRRset_def norRRset_def) + apply (rule RsetR_zmult_mono) + apply (rule Bnor_in_RsetR) + apply simp_all + done - is_RRset_def "is_RRset A m == (A : (RsetR m)) & card(A) = (phi m)" +lemma aux_some: + "#1 < m ==> is_RRset A m ==> a \ A + ==> zcong a (SOME b. [a = b] (mod m) \ b \ norRRset m) m \ + (SOME b. [a = b] (mod m) \ b \ norRRset m) \ norRRset m" + apply (rule norR_mem_unique [THEN ex1_implies_ex, THEN someI_ex]) + apply (rule_tac [2] RRset_gcd) + apply simp_all + done + +lemma RRset2norRR_correct: + "#1 < m ==> is_RRset A m ==> a \ A ==> + [a = RRset2norRR A m a] (mod m) \ RRset2norRR A m a \ norRRset m" + apply (unfold RRset2norRR_def) + apply simp + apply (rule aux_some) + apply simp_all + done + +lemmas RRset2norRR_correct1 = + RRset2norRR_correct [THEN conjunct1, standard] +lemmas RRset2norRR_correct2 = + RRset2norRR_correct [THEN conjunct2, standard] + +lemma RsetR_fin: "A \ RsetR m ==> finite A" + apply (erule RsetR.induct) + apply auto + done + +lemma RRset_zcong_eq [rule_format]: + "#1 < m ==> + is_RRset A m ==> [a = b] (mod m) ==> a \ A --> b \ A --> a = b" + apply (unfold is_RRset_def) + apply (rule RsetR.induct) + apply (auto simp add: zcong_sym) + done + +lemma aux: + "P (SOME a. P a) ==> Q (SOME a. Q a) ==> + (SOME a. P a) = (SOME a. Q a) ==> \a. P a \ Q a" + apply auto + done + +lemma RRset2norRR_inj: + "#1 < m ==> is_RRset A m ==> inj_on (RRset2norRR A m) A" + apply (unfold RRset2norRR_def inj_on_def) + apply auto + apply (subgoal_tac "\b. ([x = b] (mod m) \ b \ norRRset m) \ + ([y = b] (mod m) \ b \ norRRset m)") + apply (rule_tac [2] aux) + apply (rule_tac [3] aux_some) + apply (rule_tac [2] aux_some) + apply (rule RRset_zcong_eq) + apply auto + apply (rule_tac b = b in zcong_trans) + apply (simp_all add: zcong_sym) + done + +lemma RRset2norRR_eq_norR: + "#1 < m ==> is_RRset A m ==> RRset2norRR A m ` A = norRRset m" + apply (rule card_seteq) + prefer 3 + apply (subst card_image) + apply (rule_tac [2] RRset2norRR_inj) + apply auto + apply (rule_tac [4] RRset2norRR_correct2) + apply auto + apply (unfold is_RRset_def phi_def norRRset_def) + apply (auto simp add: RsetR_fin Bnor_fin) + done + + +lemma aux: "a \ A ==> inj f ==> f a \ f ` A" + apply (unfold inj_on_def) + apply auto + done - RRset2norRR_def "RRset2norRR A m a == - (if #1 #0 ==> a < m --> setprod ((\a. a * x) ` BnorRset (a, m)) = + setprod (BnorRset(a, m)) * x^card (BnorRset (a, m))" + apply (induct a m rule: BnorRset_induct) + prefer 2 + apply (subst BnorRset.simps) + apply (unfold Let_def) + apply auto + apply (simp add: Bnor_fin Bnor_mem_zle_swap) + apply (subst setprod_insert) + apply (rule_tac [2] aux) + apply (unfold inj_on_def) + apply (simp_all add: zmult_ac Bnor_fin finite_imageI + Bnor_mem_zle_swap) + done + + +subsection {* Fermat *} + +lemma bijzcong_zcong_prod: + "(A, B) \ bijR (zcongm m) ==> [setprod A = setprod B] (mod m)" + apply (unfold zcongm_def) + apply (erule bijR.induct) + apply (subgoal_tac [2] "a \ A \ b \ B \ finite A \ finite B") + apply (auto intro: fin_bijRl fin_bijRr zcong_zmult) + done + +lemma Bnor_prod_zgcd [rule_format]: + "a < m --> zgcd (setprod (BnorRset (a, m)), m) = #1" + apply (induct a m rule: BnorRset_induct) + prefer 2 + apply (subst BnorRset.simps) + apply (unfold Let_def) + apply auto + apply (simp add: Bnor_fin Bnor_mem_zle_swap) + apply (blast intro: zgcd_zgcd_zmult) + done -consts zcongm :: int => [int, int] => bool -defs zcongm_def "zcongm m == (%a b. zcong a b m)" +theorem Euler_Fermat: + "#0 < m ==> zgcd (x, m) = #1 ==> [x^(phi m) = #1] (mod m)" + apply (unfold norRRset_def phi_def) + apply (case_tac "x = #0") + apply (case_tac [2] "m = #1") + apply (rule_tac [3] iffD1) + apply (rule_tac [3] k = "setprod (BnorRset (m - #1, m))" + in zcong_cancel2) + prefer 5 + apply (subst Bnor_prod_power [symmetric]) + apply (rule_tac [7] Bnor_prod_zgcd) + apply simp_all + apply (rule bijzcong_zcong_prod) + apply (fold norRRset_def noXRRset_def) + apply (subst RRset2norRR_eq_norR [symmetric]) + apply (rule_tac [3] inj_func_bijR) + apply auto + apply (unfold zcongm_def) + apply (rule_tac [3] RRset2norRR_correct1) + apply (rule_tac [6] RRset2norRR_inj) + apply (auto intro: order_less_le [THEN iffD2] + simp add: noX_is_RRset) + apply (unfold noXRRset_def norRRset_def) + apply (rule finite_imageI) + apply (rule Bnor_fin) + done + +lemma Bnor_prime [rule_format (no_asm)]: + "p \ zprime ==> + a < p --> (\b. #0 < b \ b \ a --> zgcd (b, p) = #1) + --> card (BnorRset (a, p)) = nat a" + apply (unfold zprime_def) + apply (induct a p rule: BnorRset.induct) + apply (subst BnorRset.simps) + apply (unfold Let_def) + apply auto + done + +lemma phi_prime: "p \ zprime ==> phi p = nat (p - #1)" + apply (unfold phi_def norRRset_def) + apply (rule Bnor_prime) + apply auto + apply (erule zless_zprime_imp_zrelprime) + apply simp_all + done + +theorem Little_Fermat: + "p \ zprime ==> \ p dvd x ==> [x^(nat (p - #1)) = #1] (mod p)" + apply (subst phi_prime [symmetric]) + apply (rule_tac [2] Euler_Fermat) + apply (erule_tac [3] zprime_imp_zrelprime) + apply (unfold zprime_def) + apply auto + done end diff -r 2f4976370b7a -r 7eef34adb852 src/HOL/NumberTheory/Factorization.ML --- a/src/HOL/NumberTheory/Factorization.ML Sat Feb 03 17:43:34 2001 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,310 +0,0 @@ -(* Title: HOL/ex/Factorization.thy - ID: $Id$ - Author: Thomas Marthedal Rasmussen - Copyright 2000 University of Cambridge - -Fundamental Theorem of Arithmetic (unique factorization into primes) -*) - -val prime_def = thm "prime_def"; -val prime_dvd_mult = thm "prime_dvd_mult"; - - -(* --- Arithmetic --- *) - -Goal "!!m::nat. [| m ~= m*k; m ~= 1 |] ==> 1 1 n=m"; -by Auto_tac; -qed "mult_left_cancel"; - -Goal "!!m::nat. [| 0 n=1"; -by (case_tac "n" 1); -by Auto_tac; -qed "mn_eq_m_one"; - -Goal "!!m::nat. [| 0 1 m*n = k --> n x*prod xs = y*prod ys"; -by Auto_tac; -qed "prod_xy_prod"; - -Goalw [primel_def] "primel (xs @ ys) = (primel xs & primel ys)"; -by Auto_tac; -qed "primel_append"; - -Goalw [primel_def] "n:prime ==> primel [n] & prod [n] = n"; -by Auto_tac; -qed "prime_primel"; - -Goalw [prime_def,dvd_def] "p:prime ==> ~(p dvd 1)"; -by Auto_tac; -qed "prime_nd_one"; - -Goalw [dvd_def] "[| prod (x#xs) = prod ys |] ==> x dvd (prod ys)"; -by (rtac exI 1); -by (rtac sym 1); -by (Asm_full_simp_tac 1); -qed "hd_dvd_prod"; - -Goalw [primel_def] "primel (x#xs) ==> primel xs"; -by Auto_tac; -qed "primel_tl"; - -Goalw [primel_def] "(primel (x#xs)) = (x:prime & primel xs)"; -by Auto_tac; -qed "primel_hd_tl"; - -Goalw [prime_def] "[| p:prime; q:prime; p dvd q |] ==> p=q"; -by Auto_tac; -qed "primes_eq"; - -Goalw [primel_def,prime_def] "[| primel xs; prod xs = 1 |] ==> xs = []"; -by (case_tac "xs" 1); -by (ALLGOALS Asm_full_simp_tac); -qed "primel_one_empty"; - -Goalw [prime_def] "p:prime ==> 1 0 xs ~= [] --> 1 < prod xs"; -by (induct_tac "xs" 1); -by (auto_tac (claset() addEs [one_less_mult], simpset())); -qed_spec_mp "primel_nempty_g_one"; - -Goalw [primel_def,prime_def] "primel xs --> 0 < prod xs"; -by (induct_tac "xs" 1); -by Auto_tac; -qed_spec_mp "primel_prod_gz"; - - -(* --- Sorting --- *) - -Goal "nondec xs --> nondec (oinsert x xs)"; -by (induct_tac "xs" 1); -by (case_tac "list" 2); -by (ALLGOALS(asm_full_simp_tac (simpset()delcongs[thm"list.weak_case_cong"]))); -qed_spec_mp "nondec_oinsert"; - -Goal "nondec (sort xs)"; -by (induct_tac "xs" 1); -by (ALLGOALS (Asm_full_simp_tac)); -by (etac nondec_oinsert 1); -qed "nondec_sort"; - -Goal "[| x<=y; l=y#ys |] ==> x#l = oinsert x l"; -by (ALLGOALS Asm_full_simp_tac); -qed "x_less_y_oinsert"; - -Goal "nondec xs --> xs = sort xs"; -by (induct_tac "xs" 1); -by Safe_tac; -by (ALLGOALS Asm_full_simp_tac); -by (case_tac "list" 1); -by (ALLGOALS Asm_full_simp_tac); -by (case_tac "list" 1); -by (Asm_full_simp_tac 1); -by (res_inst_tac [("y","aa"),("ys","lista")] x_less_y_oinsert 1); -by (ALLGOALS Asm_full_simp_tac); -qed_spec_mp "nondec_sort_eq"; - -Goal "oinsert x (oinsert y l) = oinsert y (oinsert x l)"; -by (induct_tac "l" 1); -by Auto_tac; -qed "oinsert_x_y"; - - -(* --- Permutation --- *) - -Goalw [primel_def] "xs <~~> ys ==> primel xs --> primel ys"; -by (etac perm.induct 1); -by (ALLGOALS Asm_simp_tac); -qed_spec_mp "perm_primel"; - -Goal "xs <~~> ys ==> prod xs = prod ys"; -by (etac perm.induct 1); -by (ALLGOALS (asm_simp_tac (simpset() addsimps mult_ac))); -qed_spec_mp "perm_prod"; - -Goal "xs <~~> ys ==> oinsert a xs <~~> oinsert a ys"; -by (etac perm.induct 1); -by Auto_tac; -qed "perm_subst_oinsert"; - -Goal "x#xs <~~> oinsert x xs"; -by (induct_tac "xs" 1); -by Auto_tac; -qed "perm_oinsert"; - -Goal "xs <~~> sort xs"; -by (induct_tac "xs" 1); -by (auto_tac (claset() addIs [perm_oinsert] - addEs [perm_subst_oinsert], - simpset())); -qed "perm_sort"; - -Goal "xs <~~> ys ==> sort xs = sort ys"; -by (etac perm.induct 1); -by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [oinsert_x_y]))); -qed "perm_sort_eq"; - - -(* --- Existence --- *) - -Goal "primel xs ==> EX ys. primel ys & nondec ys & prod ys = prod xs"; -by (blast_tac (claset() addIs [nondec_sort, perm_prod,perm_primel,perm_sort, - perm_sym]) 1); -qed "ex_nondec_lemma"; - -Goalw [prime_def,dvd_def] - "1 (EX m k.1 EX l. primel l & prod l = prod xs * prod ys"; -by (rtac exI 1); -by Safe_tac; -by (rtac prod_append 2); -by (asm_simp_tac (simpset() addsimps [primel_append]) 1); -qed "split_primel"; - -Goal "1 (EX l. primel l & prod l = n)"; -by (induct_thm_tac nat_less_induct "n" 1); -by (rtac impI 1); -by (case_tac "n:prime" 1); -by (rtac exI 1); -by (etac prime_primel 1); -by (cut_inst_tac [("n","n")] not_prime_ex_mk 1); -by (auto_tac (claset() addSIs [split_primel], simpset())); -qed_spec_mp "factor_exists"; - -Goal "1 (EX l. primel l & nondec l & prod l = n)"; -by (etac (factor_exists RS exE) 1); -by (blast_tac (claset() addSIs [ex_nondec_lemma]) 1); -qed "nondec_factor_exists"; - - -(* --- Uniqueness --- *) - -Goal "p:prime ==> p dvd (prod xs) --> (EX m. m:set xs & p dvd m)"; -by (induct_tac "xs" 1); -by (ALLGOALS Asm_full_simp_tac); -by (etac prime_nd_one 1); -by (rtac impI 1); -by (dtac prime_dvd_mult 1); -by Auto_tac; -qed_spec_mp "prime_dvd_mult_list"; - -Goal "[| primel (x#xs); primel ys; prod (x#xs) = prod ys |] \ -\ ==> EX m. m :set ys & x dvd m"; -by (rtac prime_dvd_mult_list 1); -by (etac hd_dvd_prod 2); -by (asm_full_simp_tac (simpset() addsimps [primel_hd_tl]) 1); -qed "hd_xs_dvd_prod"; - -Goal "[| primel (x#xs); primel ys; m:set ys; x dvd m |] ==> x=m"; -by (rtac primes_eq 1); -by (auto_tac (claset(), simpset() addsimps [primel_def,primel_hd_tl])); -qed "prime_dvd_eq"; - -Goal "[| primel (x#xs); primel ys; prod (x#xs) = prod ys |] ==> x:set ys"; -by (ftac hd_xs_dvd_prod 1); -by Auto_tac; -by (dtac prime_dvd_eq 1); -by Auto_tac; -qed "hd_xs_eq_prod"; - -Goal "[| primel (x#xs); primel ys; prod (x#xs) = prod ys |] \ -\ ==> EX l. ys <~~> (x#l)"; -by (rtac exI 1); -by (rtac perm_remove 1); -by (etac hd_xs_eq_prod 1); -by (ALLGOALS assume_tac); -qed "perm_primel_ex"; - -Goal "[| primel (x#xs); primel ys; prod (x#xs) = prod ys |] \ -\ ==> prod xs < prod ys"; -by (auto_tac (claset() addIs [prod_mn_less_k,prime_g_one,primel_prod_gz], - simpset() addsimps [primel_hd_tl])); -qed "primel_prod_less"; - -Goal "[| primel xs; p*prod xs = p; p:prime |] ==> xs=[]"; -by (auto_tac (claset() addIs [primel_one_empty], - simpset() addsimps [prime_def])); -qed "prod_one_empty"; - -Goal "[| ALL m. m < prod ys --> (ALL xs ys. primel xs & primel ys & \ -\ prod xs = prod ys & prod xs = m --> xs <~~> ys); primel list; \ -\ primel x; prod list = prod x; prod x < prod ys |] ==> x <~~> list"; -by (Asm_full_simp_tac 1); -qed "uniq_ex_lemma"; - -Goal "ALL xs ys. (primel xs & primel ys & prod xs = prod ys & prod xs = n \ -\ --> xs <~~> ys)"; -by (induct_thm_tac nat_less_induct "n" 1); -by Safe_tac; -by (case_tac "xs" 1); -by (force_tac (claset() addIs [primel_one_empty], simpset()) 1); -by (rtac (perm_primel_ex RS exE) 1); -by (ALLGOALS Asm_full_simp_tac); -by (rtac (perm.trans RS perm_sym) 1); -by (assume_tac 1); -by (rtac perm.Cons 1); -by (case_tac "x=[]" 1); -by (asm_full_simp_tac (simpset() addsimps [perm_sing_eq,primel_hd_tl]) 1); -by (res_inst_tac [("p","a")] prod_one_empty 1); -by (ALLGOALS Asm_full_simp_tac); -by (etac uniq_ex_lemma 1); -by (auto_tac (claset() addIs [primel_tl,perm_primel], - simpset() addsimps [primel_hd_tl])); -by (res_inst_tac [("k","a"),("n","prod list"),("m","prod x")] mult_left_cancel 1); -by (res_inst_tac [("x","a")] primel_prod_less 3); -by (rtac prod_xy_prod 2); -by (res_inst_tac [("s","prod ys")] trans 2); -by (etac perm_prod 3); -by (etac (perm_prod RS sym) 5); -by (auto_tac (claset() addIs [perm_primel,prime_g_zero], simpset())); -qed_spec_mp "factor_unique"; - -Goal "[| xs <~~> ys; nondec xs; nondec ys |] ==> xs = ys"; -by (rtac trans 1); -by (rtac trans 1); -by (etac nondec_sort_eq 1); -by (etac perm_sort_eq 1); -by (etac (nondec_sort_eq RS sym) 1); -qed "perm_nondec_unique"; - -Goal "ALL n. 1 (EX! l. primel l & nondec l & prod l = n)"; -by Safe_tac; -by (etac nondec_factor_exists 1); -by (rtac perm_nondec_unique 1); -by (rtac factor_unique 1); -by (ALLGOALS Asm_full_simp_tac); -qed_spec_mp "unique_prime_factorization"; diff -r 2f4976370b7a -r 7eef34adb852 src/HOL/NumberTheory/Factorization.thy --- a/src/HOL/NumberTheory/Factorization.thy Sat Feb 03 17:43:34 2001 +0100 +++ b/src/HOL/NumberTheory/Factorization.thy Sun Feb 04 19:31:13 2001 +0100 @@ -1,38 +1,363 @@ -(* Title: HOL/ex/Factorization.thy +(* Title: HOL/NumberTheory/Factorization.thy ID: $Id$ Author: Thomas Marthedal Rasmussen Copyright 2000 University of Cambridge +*) -Fundamental Theorem of Arithmetic (unique factorization into primes) -*) +header {* Fundamental Theorem of Arithmetic (unique factorization into primes) *} + +theory Factorization = Primes + Permutation: -Factorization = Primes + Perm + +subsection {* Definitions *} consts - primel :: nat list => bool - nondec :: nat list => bool - prod :: nat list => nat - oinsert :: [nat, nat list] => nat list - sort :: nat list => nat list + primel :: "nat list => bool " + nondec :: "nat list => bool " + prod :: "nat list => nat" + oinsert :: "nat => nat list => nat list" + sort :: "nat list => nat list" defs - primel_def "primel xs == set xs <= prime" + primel_def: "primel xs == set xs \ prime" + +primrec + "nondec [] = True" + "nondec (x # xs) = (case xs of [] => True | y # ys => x \ y \ nondec xs)" primrec - "nondec [] = True" - "nondec (x#xs) = (case xs of [] => True | y#ys => x<=y & nondec xs)" + "prod [] = 1" + "prod (x # xs) = x * prod xs" + +primrec + "oinsert x [] = [x]" + "oinsert x (y # ys) = (if x \ y then x # y # ys else y # oinsert x ys)" primrec - "prod [] = 1" - "prod (x#xs) = x * prod xs" + "sort [] = []" + "sort (x # xs) = oinsert x (sort xs)" + + +subsection {* Arithmetic *} + +lemma one_less_m: "(m::nat) \ m * k ==> m \ 1 ==> 1 < m" + apply (case_tac m) + apply auto + done + +lemma one_less_k: "(m::nat) \ m * k ==> 1 < m * k ==> 1 < k" + apply (case_tac k) + apply auto + done + +lemma mult_left_cancel: "(0::nat) < k ==> k * n = k * m ==> n = m" + apply auto + done + +lemma mn_eq_m_one: "(0::nat) < m ==> m * n = m ==> n = 1" + apply (case_tac n) + apply auto + done + +lemma prod_mn_less_k: + "(0::nat) < n ==> 0 < k ==> 1 < m ==> m * n = k ==> n < k" + apply (induct m) + apply auto + done + + +subsection {* Prime list and product *} + +lemma prod_append: "prod (xs @ ys) = prod xs * prod ys" + apply (induct xs) + apply (simp_all add: mult_assoc) + done + +lemma prod_xy_prod: + "prod (x # xs) = prod (y # ys) ==> x * prod xs = y * prod ys" + apply auto + done + +lemma primel_append: "primel (xs @ ys) = (primel xs \ primel ys)" + apply (unfold primel_def) + apply auto + done + +lemma prime_primel: "n \ prime ==> primel [n] \ prod [n] = n" + apply (unfold primel_def) + apply auto + done + +lemma prime_nd_one: "p \ prime ==> \ p dvd 1" + apply (unfold prime_def dvd_def) + apply auto + done + +lemma hd_dvd_prod: "prod (x # xs) = prod ys ==> x dvd (prod ys)" + apply (unfold dvd_def) + apply (rule exI) + apply (rule sym) + apply simp + done + +lemma primel_tl: "primel (x # xs) ==> primel xs" + apply (unfold primel_def) + apply auto + done + +lemma primel_hd_tl: "(primel (x # xs)) = (x \ prime \ primel xs)" + apply (unfold primel_def) + apply auto + done + +lemma primes_eq: "p \ prime ==> q \ prime ==> p dvd q ==> p = q" + apply (unfold prime_def) + apply auto + done + +lemma primel_one_empty: "primel xs ==> prod xs = 1 ==> xs = []" + apply (unfold primel_def prime_def) + apply (case_tac xs) + apply simp_all + done + +lemma prime_g_one: "p \ prime ==> 1 < p" + apply (unfold prime_def) + apply auto + done + +lemma prime_g_zero: "p \ prime ==> 0 < p" + apply (unfold prime_def) + apply auto + done + +lemma primel_nempty_g_one [rule_format]: + "primel xs --> xs \ [] --> 1 < prod xs" + apply (unfold primel_def prime_def) + apply (induct xs) + apply (auto elim: one_less_mult) + done + +lemma primel_prod_gz: "primel xs ==> 0 < prod xs" + apply (unfold primel_def prime_def) + apply (induct xs) + apply auto + done + + +subsection {* Sorting *} + +lemma nondec_oinsert [rule_format]: "nondec xs --> nondec (oinsert x xs)" + apply (induct xs) + apply (case_tac [2] list) + apply (simp_all cong del: list.weak_case_cong) + done + +lemma nondec_sort: "nondec (sort xs)" + apply (induct xs) + apply simp_all + apply (erule nondec_oinsert) + done + +lemma x_less_y_oinsert: "x \ y ==> l = y # ys ==> x # l = oinsert x l" + apply simp_all + done + +lemma nondec_sort_eq [rule_format]: "nondec xs --> xs = sort xs" + apply (induct xs) + apply safe + apply simp_all + apply (case_tac list) + apply simp_all + apply (case_tac list) + apply simp + apply (rule_tac y = aa and ys = lista in x_less_y_oinsert) + apply simp_all + done + +lemma oinsert_x_y: "oinsert x (oinsert y l) = oinsert y (oinsert x l)" + apply (induct l) + apply auto + done + + +subsection {* Permutation *} + +lemma perm_primel [rule_format]: "xs <~~> ys ==> primel xs --> primel ys" + apply (unfold primel_def) + apply (erule perm.induct) + apply simp_all + done + +lemma perm_prod [rule_format]: "xs <~~> ys ==> prod xs = prod ys" + apply (erule perm.induct) + apply (simp_all add: mult_ac) + done -primrec - "oinsert x [] = [x]" - "oinsert x (y#ys) = (if x<=y then x#y#ys else y#oinsert x ys)" +lemma perm_subst_oinsert: "xs <~~> ys ==> oinsert a xs <~~> oinsert a ys" + apply (erule perm.induct) + apply auto + done + +lemma perm_oinsert: "x # xs <~~> oinsert x xs" + apply (induct xs) + apply auto + done + +lemma perm_sort: "xs <~~> sort xs" + apply (induct xs) + apply (auto intro: perm_oinsert elim: perm_subst_oinsert) + done + +lemma perm_sort_eq: "xs <~~> ys ==> sort xs = sort ys" + apply (erule perm.induct) + apply (simp_all add: oinsert_x_y) + done + + +subsection {* Existence *} + +lemma ex_nondec_lemma: + "primel xs ==> \ys. primel ys \ nondec ys \ prod ys = prod xs" + apply (blast intro: nondec_sort perm_prod perm_primel perm_sort perm_sym) + done + +lemma not_prime_ex_mk: + "1 < n \ n \ prime ==> + \m k. 1 < m \ 1 < k \ m < n \ k < n \ n = m * k" + apply (unfold prime_def dvd_def) + apply (auto intro: n_less_m_mult_n n_less_n_mult_m one_less_m one_less_k) + done + +lemma split_primel: + "primel xs ==> primel ys ==> \l. primel l \ prod l = prod xs * prod ys" + apply (rule exI) + apply safe + apply (rule_tac [2] prod_append) + apply (simp add: primel_append) + done + +lemma factor_exists [rule_format]: "1 < n --> (\l. primel l \ prod l = n)" + apply (induct n rule: nat_less_induct) + apply (rule impI) + apply (case_tac "n \ prime") + apply (rule exI) + apply (erule prime_primel) + apply (cut_tac n = n in not_prime_ex_mk) + apply (auto intro!: split_primel) + done + +lemma nondec_factor_exists: "1 < n ==> \l. primel l \ nondec l \ prod l = n" + apply (erule factor_exists [THEN exE]) + apply (blast intro!: ex_nondec_lemma) + done + + +subsection {* Uniqueness *} + +lemma prime_dvd_mult_list [rule_format]: + "p \ prime ==> p dvd (prod xs) --> (\m. m:set xs \ p dvd m)" + apply (induct xs) + apply simp_all + apply (erule prime_nd_one) + apply (rule impI) + apply (drule prime_dvd_mult) + apply auto + done + +lemma hd_xs_dvd_prod: + "primel (x # xs) ==> primel ys ==> prod (x # xs) = prod ys + ==> \m. m \ set ys \ x dvd m" + apply (rule prime_dvd_mult_list) + apply (simp add: primel_hd_tl) + apply (erule hd_dvd_prod) + done + +lemma prime_dvd_eq: "primel (x # xs) ==> primel ys ==> m \ set ys ==> x dvd m ==> x = m" + apply (rule primes_eq) + apply (auto simp add: primel_def primel_hd_tl) + done -primrec - "sort [] = []" - "sort (x#xs) = oinsert x (sort xs)" +lemma hd_xs_eq_prod: + "primel (x # xs) ==> + primel ys ==> prod (x # xs) = prod ys ==> x \ set ys" + apply (frule hd_xs_dvd_prod) + apply auto + apply (drule prime_dvd_eq) + apply auto + done + +lemma perm_primel_ex: + "primel (x # xs) ==> + primel ys ==> prod (x # xs) = prod ys ==> \l. ys <~~> (x # l)" + apply (rule exI) + apply (rule perm_remove) + apply (erule hd_xs_eq_prod) + apply simp_all + done + +lemma primel_prod_less: + "primel (x # xs) ==> + primel ys ==> prod (x # xs) = prod ys ==> prod xs < prod ys" + apply (auto intro: prod_mn_less_k prime_g_one primel_prod_gz simp add: primel_hd_tl) + done + +lemma prod_one_empty: + "primel xs ==> p * prod xs = p ==> p \ prime ==> xs = []" + apply (auto intro: primel_one_empty simp add: prime_def) + done + +lemma uniq_ex_aux: + "\m. m < prod ys --> (\xs ys. primel xs \ primel ys \ + prod xs = prod ys \ prod xs = m --> xs <~~> ys) ==> + primel list ==> primel x ==> prod list = prod x ==> prod x < prod ys + ==> x <~~> list" + apply simp + done -end \ No newline at end of file +lemma factor_unique [rule_format]: + "\xs ys. primel xs \ primel ys \ prod xs = prod ys \ prod xs = n + --> xs <~~> ys" + apply (induct n rule: nat_less_induct) + apply safe + apply (case_tac xs) + apply (force intro: primel_one_empty) + apply (rule perm_primel_ex [THEN exE]) + apply simp_all + apply (rule perm.trans [THEN perm_sym]) + apply assumption + apply (rule perm.Cons) + apply (case_tac "x = []") + apply (simp add: perm_sing_eq primel_hd_tl) + apply (rule_tac p = a in prod_one_empty) + apply simp_all + apply (erule uniq_ex_aux) + apply (auto intro: primel_tl perm_primel simp add: primel_hd_tl) + apply (rule_tac k = a and n = "prod list" and m = "prod x" in mult_left_cancel) + apply (rule_tac [3] x = a in primel_prod_less) + apply (rule_tac [2] prod_xy_prod) + apply (rule_tac [2] s = "prod ys" in HOL.trans) + apply (erule_tac [3] perm_prod) + apply (erule_tac [5] perm_prod [symmetric]) + apply (auto intro: perm_primel prime_g_zero) + done + +lemma perm_nondec_unique: + "xs <~~> ys ==> nondec xs ==> nondec ys ==> xs = ys" + apply (rule HOL.trans) + apply (rule HOL.trans) + apply (erule nondec_sort_eq) + apply (erule perm_sort_eq) + apply (erule nondec_sort_eq [symmetric]) + done + +lemma unique_prime_factorization [rule_format]: + "\n. 1 < n --> (\!l. primel l \ nondec l \ prod l = n)" + apply safe + apply (erule nondec_factor_exists) + apply (rule perm_nondec_unique) + apply (rule factor_unique) + apply simp_all + done + +end diff -r 2f4976370b7a -r 7eef34adb852 src/HOL/NumberTheory/Fib.ML --- a/src/HOL/NumberTheory/Fib.ML Sat Feb 03 17:43:34 2001 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,121 +0,0 @@ -(* Title: HOL/ex/Fib - ID: $Id$ - Author: Lawrence C Paulson - Copyright 1997 University of Cambridge - -Fibonacci numbers: proofs of laws taken from - - R. L. Graham, D. E. Knuth, O. Patashnik. - Concrete Mathematics. - (Addison-Wesley, 1989) -*) - - -(** The difficulty in these proofs is to ensure that the induction hypotheses - are applied before the definition of "fib". Towards this end, the - "fib" equations are not added to the simpset and are applied very - selectively at first. -**) - -Delsimps fib.Suc_Suc; - -val [fib_Suc_Suc] = fib.Suc_Suc; -val fib_Suc3 = read_instantiate [("x", "(Suc ?n)")] fib_Suc_Suc; - -(*Concrete Mathematics, page 280*) -Goal "fib (Suc (n + k)) = fib(Suc k) * fib(Suc n) + fib k * fib n"; -by (induct_thm_tac fib.induct "n" 1); -(*Simplify the LHS just enough to apply the induction hypotheses*) -by (asm_full_simp_tac - (simpset() addsimps [inst "x" "Suc(?m+?n)" fib_Suc_Suc]) 3); -by (ALLGOALS - (asm_simp_tac (simpset() addsimps - ([fib_Suc_Suc, add_mult_distrib, add_mult_distrib2])))); -qed "fib_add"; - - -Goal "fib (Suc n) ~= 0"; -by (induct_thm_tac fib.induct "n" 1); -by (ALLGOALS (asm_simp_tac (simpset() addsimps [fib_Suc_Suc]))); -qed "fib_Suc_neq_0"; - -(* Also add 0 < fib (Suc n) *) -Addsimps [fib_Suc_neq_0, [neq0_conv, fib_Suc_neq_0] MRS iffD1]; - -Goal "0 0 < fib n"; -by (rtac (not0_implies_Suc RS exE) 1); -by Auto_tac; -qed "fib_gr_0"; - -(*Concrete Mathematics, page 278: Cassini's identity. - It is much easier to prove using integers!*) -Goal "int (fib (Suc (Suc n)) * fib n) = \ -\ (if n mod #2 = 0 then int (fib(Suc n) * fib(Suc n)) - #1 \ -\ else int (fib(Suc n) * fib(Suc n)) + #1)"; -by (induct_thm_tac fib.induct "n" 1); -by (simp_tac (simpset() addsimps [fib_Suc_Suc, mod_Suc]) 2); -by (simp_tac (simpset() addsimps [fib_Suc_Suc]) 1); -by (asm_full_simp_tac - (simpset() addsimps [fib_Suc_Suc, add_mult_distrib, add_mult_distrib2, - mod_Suc, zmult_int RS sym] @ zmult_ac) 1); -qed "fib_Cassini"; - - - -(** Towards Law 6.111 of Concrete Mathematics **) - -val gcd_induct = thm "gcd_induct"; -val gcd_commute = thm "gcd_commute"; -val gcd_add2 = thm "gcd_add2"; -val gcd_non_0 = thm "gcd_non_0"; -val gcd_mult_cancel = thm "gcd_mult_cancel"; - - -Goal "gcd(fib n, fib (Suc n)) = 1"; -by (induct_thm_tac fib.induct "n" 1); -by (asm_simp_tac (simpset() addsimps [gcd_commute, fib_Suc3]) 3); -by (ALLGOALS (simp_tac (simpset() addsimps [fib_Suc_Suc]))); -qed "gcd_fib_Suc_eq_1"; - -val gcd_fib_commute = - read_instantiate_sg (sign_of thy) [("m", "fib m")] gcd_commute; - -Goal "gcd(fib m, fib (n+m)) = gcd(fib m, fib n)"; -by (simp_tac (simpset() addsimps [gcd_fib_commute]) 1); -by (case_tac "m=0" 1); -by (Asm_simp_tac 1); -by (clarify_tac (claset() addSDs [not0_implies_Suc]) 1); -by (simp_tac (simpset() addsimps [fib_add]) 1); -by (asm_simp_tac (simpset() addsimps [add_commute, gcd_non_0]) 1); -by (asm_simp_tac (simpset() addsimps [gcd_non_0 RS sym]) 1); -by (asm_simp_tac (simpset() addsimps [gcd_fib_Suc_eq_1, gcd_mult_cancel]) 1); -qed "gcd_fib_add"; - -Goal "m <= n ==> gcd(fib m, fib (n-m)) = gcd(fib m, fib n)"; -by (rtac (gcd_fib_add RS sym RS trans) 1); -by (Asm_simp_tac 1); -qed "gcd_fib_diff"; - -Goal "0 gcd (fib m, fib (n mod m)) = gcd (fib m, fib n)"; -by (induct_thm_tac nat_less_induct "n" 1); -by (stac mod_if 1); -by (Asm_simp_tac 1); -by (asm_simp_tac (simpset() addsimps [gcd_fib_diff, mod_geq, - not_less_iff_le, diff_less]) 1); -qed "gcd_fib_mod"; - -(*Law 6.111*) -Goal "fib(gcd(m,n)) = gcd(fib m, fib n)"; -by (induct_thm_tac gcd_induct "m n" 1); -by (Asm_simp_tac 1); -by (asm_full_simp_tac (simpset() addsimps [gcd_non_0]) 1); -by (asm_full_simp_tac (simpset() addsimps [gcd_commute, gcd_fib_mod]) 1); -qed "fib_gcd"; - -Goal "fib (Suc n) * fib n = setsum (%k. fib k * fib k) (atMost n)"; -by (induct_thm_tac fib.induct "n" 1); -by (auto_tac (claset(), simpset() addsimps [atMost_Suc, fib_Suc_Suc])); -by (asm_full_simp_tac - (simpset() addsimps [add_mult_distrib, add_mult_distrib2]) 1); -qed "fib_mult_eq_setsum"; - diff -r 2f4976370b7a -r 7eef34adb852 src/HOL/NumberTheory/Fib.thy --- a/src/HOL/NumberTheory/Fib.thy Sat Feb 03 17:43:34 2001 +0100 +++ b/src/HOL/NumberTheory/Fib.thy Sun Feb 04 19:31:13 2001 +0100 @@ -1,17 +1,125 @@ -(* Title: ex/Fib +(* Title: HOL/NumberTheory/Fib.thy ID: $Id$ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1997 University of Cambridge - -The Fibonacci function. Demonstrates the use of recdef. *) -Fib = Primes + +header {* The Fibonacci function *} + +theory Fib = Primes: + +text {* + Fibonacci numbers: proofs of laws taken from: + R. L. Graham, D. E. Knuth, O. Patashnik. Concrete Mathematics. + (Addison-Wesley, 1989) + + \bigskip +*} + +consts fib :: "nat => nat" +recdef fib less_than + zero: "fib 0 = 0" + one: "fib 1 = 1" + Suc_Suc: "fib (Suc (Suc x)) = fib x + fib (Suc x)" + +text {* + \medskip The difficulty in these proofs is to ensure that the + induction hypotheses are applied before the definition of @{term + fib}. Towards this end, the @{term fib} equations are not declared + to the Simplifier and are applied very selectively at first. +*} + +declare fib.Suc_Suc [simp del] + +lemma fib_Suc3: "fib (Suc (Suc (Suc n))) = fib (Suc n) + fib (Suc (Suc n))" + apply (rule fib.Suc_Suc) + done + + +text {* \medskip Concrete Mathematics, page 280 *} + +lemma fib_add: "fib (Suc (n + k)) = fib (Suc k) * fib (Suc n) + fib k * fib n" + apply (induct n rule: fib.induct) + prefer 3 + txt {* simplify the LHS just enough to apply the induction hypotheses *} + apply (simp add: fib.Suc_Suc [of "Suc (m + n)", standard]) + apply (simp_all (no_asm_simp) add: fib.Suc_Suc add_mult_distrib add_mult_distrib2) + done + +lemma fib_Suc_neq_0 [simp]: "fib (Suc n) \ 0" + apply (induct n rule: fib.induct) + apply (simp_all add: fib.Suc_Suc) + done + +lemma [simp]: "0 < fib (Suc n)" + apply (simp add: neq0_conv [symmetric]) + done + +lemma fib_gr_0: "0 < n ==> 0 < fib n" + apply (rule not0_implies_Suc [THEN exE]) + apply auto + done + -consts fib :: "nat => nat" -recdef fib "less_than" - zero "fib 0 = 0" - one "fib 1 = 1" - Suc_Suc "fib (Suc (Suc x)) = fib x + fib (Suc x)" +text {* + \medskip Concrete Mathematics, page 278: Cassini's identity. It is + much easier to prove using integers! +*} + +lemma fib_Cassini: "int (fib (Suc (Suc n)) * fib n) = + (if n mod #2 = 0 then int (fib (Suc n) * fib (Suc n)) - #1 + else int (fib (Suc n) * fib (Suc n)) + #1)" + apply (induct n rule: fib.induct) + apply (simp add: fib.Suc_Suc) + apply (simp add: fib.Suc_Suc mod_Suc) + apply (simp add: fib.Suc_Suc + add_mult_distrib add_mult_distrib2 mod_Suc zmult_int [symmetric] zmult_ac) + done + + +text {* \medskip Towards Law 6.111 of Concrete Mathematics *} + +lemma gcd_fib_Suc_eq_1: "gcd (fib n, fib (Suc n)) = 1" + apply (induct n rule: fib.induct) + prefer 3 + apply (simp add: gcd_commute fib_Suc3) + apply (simp_all add: fib.Suc_Suc) + done + +lemma gcd_fib_add: "gcd (fib m, fib (n + m)) = gcd (fib m, fib n)" + apply (simp (no_asm) add: gcd_commute [of "fib m"]) + apply (case_tac "m = 0") + apply simp + apply (clarify dest!: not0_implies_Suc) + apply (simp add: fib_add) + apply (simp add: add_commute gcd_non_0) + apply (simp add: gcd_non_0 [symmetric]) + apply (simp add: gcd_fib_Suc_eq_1 gcd_mult_cancel) + done + +lemma gcd_fib_diff: "m \ n ==> gcd (fib m, fib (n - m)) = gcd (fib m, fib n)" + apply (rule gcd_fib_add [symmetric, THEN trans]) + apply simp + done + +lemma gcd_fib_mod: "0 < m ==> gcd (fib m, fib (n mod m)) = gcd (fib m, fib n)" + apply (induct n rule: nat_less_induct) + apply (subst mod_if) + apply (simp add: gcd_fib_diff mod_geq not_less_iff_le diff_less) + done + +lemma fib_gcd: "fib (gcd (m, n)) = gcd (fib m, fib n)" -- {* Law 6.111 *} + apply (induct m n rule: gcd_induct) + apply simp + apply (simp add: gcd_non_0) + apply (simp add: gcd_commute gcd_fib_mod) + done + +lemma fib_mult_eq_setsum: + "fib (Suc n) * fib n = setsum (\k. fib k * fib k) (atMost n)" + apply (induct n rule: fib.induct) + apply (auto simp add: atMost_Suc fib.Suc_Suc) + apply (simp add: add_mult_distrib add_mult_distrib2) + done end diff -r 2f4976370b7a -r 7eef34adb852 src/HOL/NumberTheory/IntFact.ML --- a/src/HOL/NumberTheory/IntFact.ML Sat Feb 03 17:43:34 2001 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,85 +0,0 @@ -(* 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 (induct_thm_tac d22set_induct "a" 1); -by (stac d22set_eq 2); -by Auto_tac; -qed_spec_mp "d22set_le"; - -Goal "a b~:(d22set a)"; -by (auto_tac (claset() addDs [d22set_le], simpset())); -qed "d22set_le_swap"; - -Goal "#1 b<=a --> b:(d22set a)"; -by (induct_thm_tac d22set.induct "a" 1); -by Auto_tac; -by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [d22set_eq]))); -qed_spec_mp "d22set_mem"; - -Goal "finite (d22set a)"; -by (induct_thm_tac d22set_induct "a" 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 (induct_thm_tac d22set.induct "a" 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 + 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))" +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)" + 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 {})" + + +text {* \medskip @{term setprod} --- product of finite set *} + +lemma setprod_empty [simp]: "setprod {} = #1" + apply (simp add: setprod_def) + done + +lemma setprod_insert [simp]: + "finite A ==> a \ A ==> setprod (insert a A) = a * setprod A" + apply (unfold setprod_def) + apply (simp add: zmult_left_commute fold_insert [standard]) + done + + +text {* + \medskip @{term d22set} --- recursively defined set including all + integers from @{term 2} up to @{term a} +*} + +declare d22set.simps [simp del] + + +lemma d22set_induct: + "(!!a. P {} a) ==> + (!!a. #1 < (a::int) ==> P (d22set (a - #1)) (a - #1) + ==> P (d22set a) a) + ==> P (d22set u) u" +proof - + case antecedent + show ?thesis + apply (rule d22set.induct) + apply safe + apply (case_tac [2] "#1 < a") + apply (rule_tac [2] antecedent) + apply (simp_all (no_asm_simp)) + apply (simp_all (no_asm_simp) add: d22set.simps antecedent) + done +qed -recdef d22set "measure ((%a.(nat a)) ::int=>nat)" - "d22set a = (if #1 d22set a --> #1 < b" + apply (induct a rule: d22set_induct) + prefer 2 + apply (subst d22set.simps) + apply auto + done + +lemma d22set_le [rule_format]: "b \ d22set a --> b \ a" + apply (induct a rule: d22set_induct) + prefer 2 + apply (subst d22set.simps) + apply auto + done + +lemma d22set_le_swap: "a < b ==> b \ d22set a" + apply (auto dest: d22set_le) + done + +lemma d22set_mem [rule_format]: "#1 < b --> b \ a --> b \ d22set a" + apply (induct a rule: d22set.induct) + apply auto + apply (simp_all add: d22set.simps) + done -end \ No newline at end of file +lemma d22set_fin: "finite (d22set a)" + apply (induct a rule: d22set_induct) + prefer 2 + apply (subst d22set.simps) + apply auto + done + + +declare zfact.simps [simp del] + +lemma d22set_prod_zfact: "setprod (d22set a) = zfact a" + apply (induct a rule: d22set.induct) + apply safe + apply (simp add: d22set.simps zfact.simps) + apply (subst d22set.simps) + apply (subst zfact.simps) + apply (case_tac "#1 < a") + prefer 2 + apply (simp add: d22set.simps zfact.simps) + apply (simp add: d22set_fin d22set_le_swap) + done + +end diff -r 2f4976370b7a -r 7eef34adb852 src/HOL/NumberTheory/IntPrimes.ML --- a/src/HOL/NumberTheory/IntPrimes.ML Sat Feb 03 17:43:34 2001 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,789 +0,0 @@ -(* Title: IntPrimes.ML - ID: $Id$ - Author: Thomas M. Rasmussen & L C Paulson - 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. -*) - -eta_contract:=false; - - -Goal "(abs (z::int) = w) = (z=w & #0 <= z | z=-w & z < #0)"; -by (auto_tac (claset(), simpset() addsimps [zabs_def])); -qed "zabs_eq_iff"; - - -(** gcd lemmas **) - -val gcd_non_0 = thm "gcd_non_0"; -val gcd_add1 = thm "gcd_add1"; -val gcd_commute = thm "gcd_commute"; - -Goal "gcd (m+k, k) = gcd (m+k, m)"; -by (simp_tac (simpset() addsimps [gcd_commute]) 1); -qed "gcd_add1_eq"; - -Goal "m <= n ==> gcd (n, n - m) = gcd (n, m)"; -by (subgoal_tac "n = m + (n-m)" 1); -by (etac ssubst 1 THEN rtac gcd_add1_eq 1); -by (Asm_simp_tac 1); -qed "gcd_diff2"; - - -(************************************************) -(** 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"; -AddIffs [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 (auto_tac (claset(), simpset() addsimps [zmod_zmult_self2])); -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(m,n) = zgcd (n, m mod n)"; -by (forw_inst_tac [("b","n"), ("a","m")] pos_mod_sign 1); -by (asm_simp_tac (simpset() addsimps [zgcd_def, zabs_def, nat_mod_distrib]) 1); -by (cut_inst_tac [("a","-m"),("b","n")] zmod_zminus1_eq_if 1); -by (auto_tac (claset(), - simpset() addsimps [gcd_non_0, nat_mod_distrib RS sym, - zmod_zminus1_eq_if])); -by (forw_inst_tac [("a","m")] pos_mod_bound 1); -by (asm_simp_tac (simpset() addsimps [nat_diff_distrib]) 1); -by (rtac gcd_diff2 1); -by (asm_full_simp_tac (simpset() addsimps [nat_le_eq_zle]) 1); -qed "zgcd_non_0"; - -Goal "zgcd(m,n) = zgcd (n, m mod n)"; -by (zdiv_undefined_case_tac "n = #0" 1); -by (auto_tac - (claset(), - simpset() addsimps [linorder_neq_iff, zgcd_non_0])); -by (cut_inst_tac [("m","-m"),("n","-n")] zgcd_non_0 1); -by Auto_tac; -qed "zgcd_eq"; - -Goal "zgcd(m,#1) = #1"; -by (simp_tac (simpset() addsimps [zgcd_def, zabs_def]) 1); -qed "zgcd_1"; -Addsimps [zgcd_1]; - -Goal "(zgcd(#0,m) = #1) = (abs m = #1)"; -by (simp_tac (simpset() addsimps [zgcd_def, zabs_def]) 1); -qed "zgcd_0_1_iff"; -Addsimps [zgcd_0_1_iff]; - -Goal "zgcd(m,n) dvd m"; -by (simp_tac (simpset() addsimps [zgcd_def, zabs_def, int_dvd_iff]) 1); -qed "zgcd_zdvd1"; - -Goal "zgcd(m,n) dvd n"; -by (simp_tac (simpset() addsimps [zgcd_def, zabs_def, int_dvd_iff]) 1); -qed "zgcd_zdvd2"; -AddIffs [zgcd_zdvd1, zgcd_zdvd2]; - -Goal "k dvd zgcd(m,n) = (k dvd m & k dvd n)"; -by (simp_tac (simpset() addsimps [zgcd_def, zabs_def, int_dvd_iff, - dvd_int_iff, nat_dvd_iff]) 1); -qed "zgcd_greatest_iff"; - -Goal "zgcd(m,n) = zgcd(n,m)"; -by (simp_tac (simpset() addsimps [zgcd_def, thm"gcd_commute"]) 1); -qed "zgcd_commute"; - -Goal "zgcd(#1,m) = #1"; -by (simp_tac (simpset() addsimps [zgcd_def, thm"gcd_1_left"]) 1); -qed "zgcd_1_left"; -Addsimps [zgcd_1_left]; - -Goal "zgcd(zgcd(k,m),n) = zgcd(k,zgcd(m,n))"; -by (simp_tac (simpset() addsimps [zgcd_def, thm"gcd_assoc"]) 1); -qed "zgcd_assoc"; - -Goal "zgcd(k,zgcd(m,n)) = zgcd(m,zgcd(k,n))"; -by (rtac (zgcd_commute RS trans) 1); -by (rtac (zgcd_assoc RS trans) 1); -by (rtac (zgcd_commute RS arg_cong) 1); -qed "zgcd_left_commute"; - -(*Addition is an AC-operator*) -bind_thms ("zgcd_ac", [zgcd_assoc, zgcd_commute, zgcd_left_commute]); - -val gcd_mult_distrib2 = thm"gcd_mult_distrib2"; - -Goal "#0<=k ==> k * zgcd(m,n) = zgcd(k*m, k*n)"; -by (asm_simp_tac - (simpset() delsimps [zmult_zminus_right] - addsimps [zmult_zminus_right RS sym, - nat_mult_distrib, zgcd_def, zabs_def, - zmult_less_0_iff, gcd_mult_distrib2 RS sym, - zmult_int RS sym]) 1); -qed "zgcd_zmult_distrib2"; - -Goal "zgcd(k*m, k*n) = abs k * zgcd(m,n)"; -by (simp_tac (simpset() addsimps [zabs_def, zgcd_zmult_distrib2]) 1); -qed "zgcd_zmult_distrib2_abs"; - - -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 ==> 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 "[| zgcd(n,k)=#1; k dvd m*n; #0 <= m |] ==> k dvd m"; -by (subgoal_tac "m = zgcd(m*n, m*k)" 1); -by (etac ssubst 1 THEN rtac (zgcd_greatest_iff RS iffD2) 1); -by (ALLGOALS (asm_simp_tac (simpset() - addsimps [zgcd_zmult_distrib2 RS sym,int_0_le_mult_iff]))); -val lemma = result(); - -Goal "[| zgcd(n,k)=#1; k dvd m*n |] ==> k dvd m"; -by (case_tac "#0 <= m" 1); -by (blast_tac (claset() addIs [lemma]) 1); -by (subgoal_tac "k dvd -m" 1); -by (rtac lemma 2); -by Auto_tac; -qed "zrelprime_zdvd_zmult"; - -Goalw [zprime_def] "[| p:zprime; ~p dvd n |] ==> zgcd(n,p) = #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 1); -by Auto_tac; -qed "zprime_zdvd_zmult"; - -val gcd_add_mult = thm "gcd_add_mult"; - -Goal "zgcd(m + n*k, n) = zgcd(m,n)"; -by (rtac (zgcd_eq RS trans) 1); -by (simp_tac (simpset() addsimps [zmod_zadd1_eq]) 1); -by (rtac (zgcd_eq RS sym) 1); -qed "zgcd_zadd_zmult"; -Addsimps [zgcd_zadd_zmult]; - - -Goal "zgcd(m,n) dvd zgcd(k*m,n)"; -by (simp_tac (simpset() addsimps [zgcd_greatest_iff]) 1); -by (blast_tac (claset() addIs [zdvd_trans]) 1); -qed "zgcd_zdvd_zgcd_zmult"; - -Goal "zgcd(k,n) = #1 ==> zgcd(k*m,n) dvd zgcd(m,n)"; -by (simp_tac (simpset() addsimps [zgcd_greatest_iff]) 1); -by (res_inst_tac [("n","k")] zrelprime_zdvd_zmult 1); -by (simp_tac (simpset() addsimps [zmult_commute]) 2); -by (subgoal_tac "zgcd (k, zgcd (k * m, n)) = zgcd (k * m, zgcd (k, n))" 1); -by (Asm_full_simp_tac 1); -by (simp_tac (simpset() addsimps zgcd_ac) 1); -qed "zgcd_zmult_zdvd_zgcd"; - -val gcd_mult_cancel = thm "gcd_mult_cancel"; - -Goal "zgcd(k,n) = #1 ==> zgcd(k*m, n) = zgcd(m,n)"; -by (asm_full_simp_tac (simpset() addsimps [zgcd_def, - nat_abs_mult_distrib, gcd_mult_cancel]) 1); -qed "zgcd_zmult_cancel"; - -Goal "[| 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 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] - "[| [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 3); -by (asm_simp_tac (simpset() addsimps [zgcd_commute]) 3); -by (asm_full_simp_tac (simpset() addsimps [zmult_commute,zdvd_zminus_iff]) 3); -by (res_inst_tac [("n","n")] zrelprime_zdvd_zmult 2); -by (asm_simp_tac (simpset() addsimps [zgcd_commute]) 2); -by (asm_full_simp_tac (simpset() addsimps [zmult_commute]) 2); -by (auto_tac (claset(), simpset() addsimps [dvd_def])); -by (blast_tac (claset() addIs [sym]) 1); -qed "zcong_zgcd_zmult_zmod"; - -Goalw [zcong_def,dvd_def] - "[| #0<=a; a a = b"; -by Auto_tac; -by (dres_inst_tac [("f", "%z. z mod m")] arg_cong 1); -by (cut_inst_tac [("z","a"),("w","b")] zless_linear 1); -by Auto_tac; -by (subgoal_tac "(a - b) mod m = a-b" 2); -by (rtac mod_pos_pos_trivial 3); -by Auto_tac; -by (subgoal_tac "(m + (a - b)) mod m = m + (a - b)" 1); -by (rtac mod_pos_pos_trivial 2); -by Auto_tac; -qed "zcong_zless_imp_eq"; - -Goal "[| p:zprime; #0 a = #1 | a = p-#1"; -by (cut_inst_tac [("p","p"),("a","a")] zcong_square 1); -by (full_simp_tac (simpset() addsimps [zprime_def]) 1); -by (auto_tac (claset() addIs [zcong_zless_imp_eq], simpset())); -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"; - -Goal "[a = b] (mod -m) = [a = b] (mod m)"; -by (auto_tac (claset(), simpset() addsimps [zcong_def])); -qed "zcong_zminus"; -AddIffs [zcong_zminus]; - -Goal "[a = b] (mod #0) = (a = b)"; -by (auto_tac (claset(), simpset() addsimps [zcong_def])); -qed "zcong_zero"; -AddIffs [zcong_zero]; - -Goal "[a = b] (mod m) = (a mod m = b mod m)"; -by (zdiv_undefined_case_tac "m = #0" 1); -by (case_tac "#0 (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 --> #0 < r --> \ -\ (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; -by (case_tac "r' mod r = #0" 1); -by (forw_inst_tac [("a","r'")] pos_mod_sign 2); -by Auto_tac; -by (arith_tac 2); -by (rtac exI 1); -by (rtac exI 1); -by (stac xzgcda_eq 1); -by Auto_tac; -by (asm_full_simp_tac (simpset() addsimps [zabs_def]) 1); -val lemma1 = result(); - -Goal "(EX sn tn. xzgcda (m,n,r',r,s',s,t',t) = (k,sn,tn)) --> #0 < r --> \ -\ 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 (claset(), simpset() addsimps [linorder_not_le])); -by (case_tac "r' mod r = #0" 1); -by (forw_inst_tac [("a","r'")] pos_mod_sign 2); -by Auto_tac; -by (arith_tac 2); -by (eres_inst_tac [("P","xzgcda ?u = ?v")] rev_mp 1); -by (stac xzgcda_eq 1); -by Auto_tac; -by (asm_full_simp_tac (simpset() addsimps [zabs_def]) 1); -val lemma2 = result(); - -Goalw [xzgcd_def] "#0 < n ==> (zgcd(m,n) = k) = (EX s t. xzgcd m n = (k,s,t))"; -by (rtac iffI 1); -by (rtac (lemma2 RS mp RS mp) 2); -by (rtac (lemma1 RS mp RS mp) 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(); - -bind_thm ("order_le_neq_implies_less", [order_less_le, conjI] MRS iffD2); - -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 (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 order_le_neq_implies_less 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 (asm_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 int*int*int" - xzgcd :: "[int,int] => int*int*int" - zprime :: int set - zcong :: [int,int,int] => bool ("(1[_ = _] '(mod _'))") - -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))" + 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 xzgcda + "measure ((\(m, n, r', r, s', s, t', t). nat r) + :: int * int * int * int *int * int * int * int => nat)" + "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))" + (hints simp: pos_mod_bound) constdefs - zgcd :: "int*int => int" - "zgcd == %(x,y). int (gcd(nat (abs x), nat (abs y)))" + zgcd :: "int * int => int" + "zgcd == \(x,y). int (gcd (nat (abs x), nat (abs y)))" defs - xzgcd_def "xzgcd m n == xzgcda (m,n,m,n,#1,#0,#0,#1)" + xzgcd_def: "xzgcd m n == xzgcda (m, n, m, n, #1, #0, #0, #1)" + zprime_def: "zprime == {p. #1 < p \ (\m. m dvd p --> m = #1 \ m = p)}" + zcong_def: "[a = b] (mod m) == m dvd (a - b)" + + +lemma zabs_eq_iff: + "(abs (z::int) = w) = (z = w \ #0 <= z \ z = -w \ z < #0)" + apply (auto simp add: zabs_def) + done + + +text {* \medskip @{term gcd} lemmas *} + +lemma gcd_add1_eq: "gcd (m + k, k) = gcd (m + k, m)" + apply (simp add: gcd_commute) + done + +lemma gcd_diff2: "m \ n ==> gcd (n, n - m) = gcd (n, m)" + apply (subgoal_tac "n = m + (n - m)") + apply (erule ssubst, rule gcd_add1_eq) + apply simp + done + + +subsection {* Divides relation *} + +lemma zdvd_0_right [iff]: "(m::int) dvd #0" + apply (unfold dvd_def) + apply (blast intro: zmult_0_right [symmetric]) + done + +lemma zdvd_0_left [iff]: "(#0 dvd (m::int)) = (m = #0)" + apply (unfold dvd_def) + apply auto + done + +lemma zdvd_1_left [iff]: "#1 dvd (m::int)" + apply (unfold dvd_def) + apply simp + done + +lemma zdvd_refl [simp]: "m dvd (m::int)" + apply (unfold dvd_def) + apply (blast intro: zmult_1_right [symmetric]) + done + +lemma zdvd_trans: "m dvd n ==> n dvd k ==> m dvd (k::int)" + apply (unfold dvd_def) + apply (blast intro: zmult_assoc) + done + +lemma zdvd_zminus_iff: "(m dvd -n) = (m dvd (n::int))" + apply (unfold dvd_def) + apply auto + apply (rule_tac [!] x = "-k" in exI) + apply auto + done + +lemma zdvd_zminus2_iff: "(-m dvd n) = (m dvd (n::int))" + apply (unfold dvd_def) + apply auto + apply (rule_tac [!] x = "-k" in exI) + apply auto + done + +lemma zdvd_anti_sym: + "#0 < m ==> #0 < n ==> m dvd n ==> n dvd m ==> m = (n::int)" + apply (unfold dvd_def) + apply auto + apply (simp add: zmult_assoc zmult_eq_self_iff int_0_less_mult_iff zmult_eq_1_iff) + done + +lemma zdvd_zadd: "k dvd m ==> k dvd n ==> k dvd (m + n :: int)" + apply (unfold dvd_def) + apply (blast intro: zadd_zmult_distrib2 [symmetric]) + done + +lemma zdvd_zdiff: "k dvd m ==> k dvd n ==> k dvd (m - n :: int)" + apply (unfold dvd_def) + apply (blast intro: zdiff_zmult_distrib2 [symmetric]) + done + +lemma zdvd_zdiffD: "k dvd m - n ==> k dvd n ==> k dvd (m::int)" + apply (subgoal_tac "m = n + (m - n)") + apply (erule ssubst) + apply (blast intro: zdvd_zadd) + apply simp + done + +lemma zdvd_zmult: "k dvd (n::int) ==> k dvd m * n" + apply (unfold dvd_def) + apply (blast intro: zmult_left_commute) + done + +lemma zdvd_zmult2: "k dvd (m::int) ==> k dvd m * n" + apply (subst zmult_commute) + apply (erule zdvd_zmult) + done + +lemma [iff]: "(k::int) dvd m * k" + apply (rule zdvd_zmult) + apply (rule zdvd_refl) + done + +lemma [iff]: "(k::int) dvd k * m" + apply (rule zdvd_zmult2) + apply (rule zdvd_refl) + done + +lemma zdvd_zmultD2: "j * k dvd n ==> j dvd (n::int)" + apply (unfold dvd_def) + apply (simp add: zmult_assoc) + apply blast + done + +lemma zdvd_zmultD: "j * k dvd n ==> k dvd (n::int)" + apply (rule zdvd_zmultD2) + apply (subst zmult_commute) + apply assumption + done + +lemma zdvd_zmult_mono: "i dvd m ==> j dvd (n::int) ==> i * j dvd m * n" + apply (unfold dvd_def) + apply clarify + apply (rule_tac x = "k * ka" in exI) + apply (simp add: zmult_ac) + done + +lemma zdvd_reduce: "(k dvd n + k * m) = (k dvd (n::int))" + apply (rule iffI) + apply (erule_tac [2] zdvd_zadd) + apply (subgoal_tac "n = (n + k * m) - k * m") + apply (erule ssubst) + apply (erule zdvd_zdiff) + apply simp_all + done + +lemma zdvd_zmod: "f dvd m ==> f dvd (n::int) ==> f dvd m mod n" + apply (unfold dvd_def) + apply (auto simp add: zmod_zmult_zmult1) + done + +lemma zdvd_zmod_imp_zdvd: "k dvd m mod n ==> k dvd n ==> k dvd (m::int)" + apply (subgoal_tac "k dvd n * (m div n) + m mod n") + apply (simp add: zmod_zdiv_equality [symmetric]) + apply (simp add: zdvd_zadd zdvd_zmult2) + done + +lemma zdvd_iff_zmod_eq_0: "(k dvd n) = (n mod (k::int) = #0)" + apply (unfold dvd_def) + apply auto + done + +lemma zdvd_not_zless: "#0 < m ==> m < n ==> \ n dvd (m::int)" + apply (unfold dvd_def) + apply auto + apply (subgoal_tac "#0 < n") + prefer 2 + apply (blast intro: zless_trans) + apply (simp add: int_0_less_mult_iff) + apply (subgoal_tac "n * k < n * #1") + apply (drule zmult_zless_cancel1 [THEN iffD1]) + apply auto + done + +lemma int_dvd_iff: "(int m dvd z) = (m dvd nat (abs z))" + apply (auto simp add: dvd_def nat_abs_mult_distrib) + apply (auto simp add: nat_eq_iff zabs_eq_iff) + apply (rule_tac [2] x = "-(int k)" in exI) + apply (auto simp add: zmult_int [symmetric]) + done + +lemma dvd_int_iff: "(z dvd int m) = (nat (abs z) dvd m)" + apply (auto simp add: dvd_def zabs_def zmult_int [symmetric]) + apply (rule_tac [3] x = "nat k" in exI) + apply (rule_tac [2] x = "-(int k)" in exI) + apply (rule_tac x = "nat (-k)" in exI) + apply (cut_tac [3] k = m in int_less_0_conv) + apply (cut_tac k = m in int_less_0_conv) + apply (auto simp add: int_0_le_mult_iff zmult_less_0_iff + nat_mult_distrib [symmetric] nat_eq_iff2) + done + +lemma nat_dvd_iff: "(nat z dvd m) = (if #0 \ z then (z dvd int m) else m = 0)" + apply (auto simp add: dvd_def zmult_int [symmetric]) + apply (rule_tac x = "nat k" in exI) + apply (cut_tac k = m in int_less_0_conv) + apply (auto simp add: int_0_le_mult_iff zmult_less_0_iff + nat_mult_distrib [symmetric] nat_eq_iff2) + done + +lemma zminus_dvd_iff [iff]: "(-z dvd w) = (z dvd (w::int))" + apply (auto simp add: dvd_def) + apply (rule_tac [!] x = "-k" in exI) + apply auto + done + +lemma dvd_zminus_iff [iff]: "(z dvd -w) = (z dvd (w::int))" + apply (auto simp add: dvd_def) + apply (drule zminus_equation [THEN iffD1]) + apply (rule_tac [!] x = "-k" in exI) + apply auto + done + + +subsection {* Euclid's Algorithm and GCD *} + +lemma zgcd_0 [simp]: "zgcd (m, #0) = abs m" + apply (simp add: zgcd_def zabs_def) + done + +lemma zgcd_0_left [simp]: "zgcd (#0, m) = abs m" + apply (simp add: zgcd_def zabs_def) + done + +lemma zgcd_zminus [simp]: "zgcd (-m, n) = zgcd (m, n)" + apply (simp add: zgcd_def) + done + +lemma zgcd_zminus2 [simp]: "zgcd (m, -n) = zgcd (m, n)" + apply (simp add: zgcd_def) + done + +lemma zgcd_non_0: "#0 < n ==> zgcd (m, n) = zgcd (n, m mod n)" + apply (frule_tac b = n and a = m in pos_mod_sign) + apply (simp add: zgcd_def zabs_def nat_mod_distrib) + apply (cut_tac a = "-m" and b = n in zmod_zminus1_eq_if) + apply (auto simp add: gcd_non_0 nat_mod_distrib [symmetric] zmod_zminus1_eq_if) + apply (frule_tac a = m in pos_mod_bound) + apply (simp add: nat_diff_distrib) + apply (rule gcd_diff2) + apply (simp add: nat_le_eq_zle) + done + +lemma zgcd_eq: "zgcd (m, n) = zgcd (n, m mod n)" + apply (tactic {* zdiv_undefined_case_tac "n = #0" 1 *}) + apply (auto simp add: linorder_neq_iff zgcd_non_0) + apply (cut_tac m = "-m" and n = "-n" in zgcd_non_0) + apply auto + done + +lemma zgcd_1 [simp]: "zgcd (m, #1) = #1" + apply (simp add: zgcd_def zabs_def) + done + +lemma zgcd_0_1_iff [simp]: "(zgcd (#0, m) = #1) = (abs m = #1)" + apply (simp add: zgcd_def zabs_def) + done + +lemma zgcd_zdvd1 [iff]: "zgcd (m, n) dvd m" + apply (simp add: zgcd_def zabs_def int_dvd_iff) + done + +lemma zgcd_zdvd2 [iff]: "zgcd (m, n) dvd n" + apply (simp add: zgcd_def zabs_def int_dvd_iff) + done + +lemma zgcd_greatest_iff: "k dvd zgcd (m, n) = (k dvd m \ k dvd n)" + apply (simp add: zgcd_def zabs_def int_dvd_iff dvd_int_iff nat_dvd_iff) + done + +lemma zgcd_commute: "zgcd (m, n) = zgcd (n, m)" + apply (simp add: zgcd_def gcd_commute) + done + +lemma zgcd_1_left [simp]: "zgcd (#1, m) = #1" + apply (simp add: zgcd_def gcd_1_left) + done + +lemma zgcd_assoc: "zgcd (zgcd (k, m), n) = zgcd (k, zgcd (m, n))" + apply (simp add: zgcd_def gcd_assoc) + done + +lemma zgcd_left_commute: "zgcd (k, zgcd (m, n)) = zgcd (m, zgcd (k, n))" + apply (rule zgcd_commute [THEN trans]) + apply (rule zgcd_assoc [THEN trans]) + apply (rule zgcd_commute [THEN arg_cong]) + done + +lemmas zgcd_ac = zgcd_assoc zgcd_commute zgcd_left_commute + -- {* addition is an AC-operator *} + +lemma zgcd_zmult_distrib2: "#0 \ k ==> k * zgcd (m, n) = zgcd (k * m, k * n)" + apply (simp del: zmult_zminus_right + add: zmult_zminus_right [symmetric] nat_mult_distrib zgcd_def zabs_def + zmult_less_0_iff gcd_mult_distrib2 [symmetric] zmult_int [symmetric]) + done + +lemma zgcd_zmult_distrib2_abs: "zgcd (k * m, k * n) = abs k * zgcd (m, n)" + apply (simp add: zabs_def zgcd_zmult_distrib2) + done + +lemma zgcd_self [simp]: "#0 \ m ==> zgcd (m, m) = m" + apply (cut_tac k = m and m = "#1" and n = "#1" in zgcd_zmult_distrib2) + apply simp_all + done + +lemma zgcd_zmult_eq_self [simp]: "#0 \ k ==> zgcd (k, k * n) = k" + apply (cut_tac k = k and m = "#1" and n = n in zgcd_zmult_distrib2) + apply simp_all + done + +lemma zgcd_zmult_eq_self2 [simp]: "#0 \ k ==> zgcd (k * n, k) = k" + apply (cut_tac k = k and m = n and n = "#1" in zgcd_zmult_distrib2) + apply simp_all + done + +lemma aux: "zgcd (n, k) = #1 ==> k dvd m * n ==> #0 \ m ==> k dvd m" + apply (subgoal_tac "m = zgcd (m * n, m * k)") + apply (erule ssubst, rule zgcd_greatest_iff [THEN iffD2]) + apply (simp_all add: zgcd_zmult_distrib2 [symmetric] int_0_le_mult_iff) + done + +lemma zrelprime_zdvd_zmult: "zgcd (n, k) = #1 ==> k dvd m * n ==> k dvd m" + apply (case_tac "#0 \ m") + apply (blast intro: aux) + apply (subgoal_tac "k dvd -m") + apply (rule_tac [2] aux) + apply auto + done + +lemma zprime_imp_zrelprime: + "p \ zprime ==> \ p dvd n ==> zgcd (n, p) = #1" + apply (unfold zprime_def) + apply auto + done + +lemma zless_zprime_imp_zrelprime: + "p \ zprime ==> #0 < n ==> n < p ==> zgcd (n, p) = #1" + apply (erule zprime_imp_zrelprime) + apply (erule zdvd_not_zless) + apply assumption + done + +lemma zprime_zdvd_zmult: + "#0 \ (m::int) ==> p \ zprime ==> p dvd m * n ==> p dvd m \ p dvd n" + apply safe + apply (rule zrelprime_zdvd_zmult) + apply (rule zprime_imp_zrelprime) + apply auto + done + +lemma zgcd_zadd_zmult [simp]: "zgcd (m + n * k, n) = zgcd (m, n)" + apply (rule zgcd_eq [THEN trans]) + apply (simp add: zmod_zadd1_eq) + apply (rule zgcd_eq [symmetric]) + done + +lemma zgcd_zdvd_zgcd_zmult: "zgcd (m, n) dvd zgcd (k * m, n)" + apply (simp add: zgcd_greatest_iff) + apply (blast intro: zdvd_trans) + done + +lemma zgcd_zmult_zdvd_zgcd: + "zgcd (k, n) = #1 ==> zgcd (k * m, n) dvd zgcd (m, n)" + apply (simp add: zgcd_greatest_iff) + apply (rule_tac n = k in zrelprime_zdvd_zmult) + prefer 2 + apply (simp add: zmult_commute) + apply (subgoal_tac "zgcd (k, zgcd (k * m, n)) = zgcd (k * m, zgcd (k, n))") + apply simp + apply (simp (no_asm) add: zgcd_ac) + done + +lemma zgcd_zmult_cancel: "zgcd (k, n) = #1 ==> zgcd (k * m, n) = zgcd (m, n)" + apply (simp add: zgcd_def nat_abs_mult_distrib gcd_mult_cancel) + done + +lemma zgcd_zgcd_zmult: + "zgcd (k, m) = #1 ==> zgcd (n, m) = #1 ==> zgcd (k * n, m) = #1" + apply (simp (no_asm_simp) add: zgcd_zmult_cancel) + done + +lemma zdvd_iff_zgcd: "#0 < m ==> (m dvd n) = (zgcd (n, m) = m)" + apply safe + apply (rule_tac [2] n = "zgcd (n, m)" in zdvd_trans) + apply (rule_tac [3] zgcd_zdvd1) + apply simp_all + apply (unfold dvd_def) + apply auto + done + + +subsection {* Congruences *} + +lemma zcong_1 [simp]: "[a = b] (mod #1)" + apply (unfold zcong_def) + apply auto + done + +lemma zcong_refl [simp]: "[k = k] (mod m)" + apply (unfold zcong_def) + apply auto + done - zprime_def "zprime == {p. #1

m=#1 | m=p)}" +lemma zcong_sym: "[a = b] (mod m) = [b = a] (mod m)" + apply (unfold zcong_def dvd_def) + apply auto + apply (rule_tac [!] x = "-k" in exI) + apply auto + done + +lemma zcong_zadd: + "[a = b] (mod m) ==> [c = d] (mod m) ==> [a + c = b + d] (mod m)" + apply (unfold zcong_def) + apply (rule_tac s = "(a - b) + (c - d)" in subst) + apply (rule_tac [2] zdvd_zadd) + apply auto + done + +lemma zcong_zdiff: + "[a = b] (mod m) ==> [c = d] (mod m) ==> [a - c = b - d] (mod m)" + apply (unfold zcong_def) + apply (rule_tac s = "(a - b) - (c - d)" in subst) + apply (rule_tac [2] zdvd_zdiff) + apply auto + done + +lemma zcong_trans: + "[a = b] (mod m) ==> [b = c] (mod m) ==> [a = c] (mod m)" + apply (unfold zcong_def dvd_def) + apply auto + apply (rule_tac x = "k + ka" in exI) + apply (simp add: zadd_ac zadd_zmult_distrib2) + done + +lemma zcong_zmult: + "[a = b] (mod m) ==> [c = d] (mod m) ==> [a * c = b * d] (mod m)" + apply (rule_tac b = "b * c" in zcong_trans) + apply (unfold zcong_def) + apply (rule_tac s = "c * (a - b)" in subst) + apply (rule_tac [3] s = "b * (c - d)" in subst) + prefer 4 + apply (blast intro: zdvd_zmult) + prefer 2 + apply (blast intro: zdvd_zmult) + apply (simp_all add: zdiff_zmult_distrib2 zmult_commute) + done + +lemma zcong_scalar: "[a = b] (mod m) ==> [a * k = b * k] (mod m)" + apply (rule zcong_zmult) + apply simp_all + done + +lemma zcong_scalar2: "[a = b] (mod m) ==> [k * a = k * b] (mod m)" + apply (rule zcong_zmult) + apply simp_all + done + +lemma zcong_zmult_self: "[a * m = b * m] (mod m)" + apply (unfold zcong_def) + apply (rule zdvd_zdiff) + apply simp_all + done + +lemma zcong_square: + "p \ zprime ==> #0 < a ==> [a * a = #1] (mod p) + ==> [a = #1] (mod p) \ [a = p - #1] (mod p)" + apply (unfold zcong_def) + apply (rule zprime_zdvd_zmult) + apply (rule_tac [3] s = "a * a - #1 + p * (#1 - a)" in subst) + prefer 4 + apply (simp add: zdvd_reduce) + apply (simp_all add: zdiff_zmult_distrib zmult_commute zdiff_zmult_distrib2) + done + +lemma zcong_cancel: + "#0 \ m ==> + zgcd (k, m) = #1 ==> [a * k = b * k] (mod m) = [a = b] (mod m)" + apply safe + prefer 2 + apply (blast intro: zcong_scalar) + apply (case_tac "b < a") + prefer 2 + apply (subst zcong_sym) + apply (unfold zcong_def) + apply (rule_tac [!] zrelprime_zdvd_zmult) + apply (simp_all add: zdiff_zmult_distrib) + apply (subgoal_tac "m dvd (-(a * k - b * k))") + apply (simp add: zminus_zdiff_eq) + apply (subst zdvd_zminus_iff) + apply assumption + done + +lemma zcong_cancel2: + "#0 \ m ==> + zgcd (k, m) = #1 ==> [k * a = k * b] (mod m) = [a = b] (mod m)" + apply (simp add: zmult_commute zcong_cancel) + done + +lemma zcong_zgcd_zmult_zmod: + "[a = b] (mod m) ==> [a = b] (mod n) ==> zgcd (m, n) = #1 + ==> [a = b] (mod m * n)" + apply (unfold zcong_def dvd_def) + apply auto + apply (subgoal_tac "m dvd n * ka") + apply (subgoal_tac "m dvd ka") + apply (case_tac [2] "#0 \ ka") + prefer 3 + apply (subst zdvd_zminus_iff [symmetric]) + apply (rule_tac n = n in zrelprime_zdvd_zmult) + apply (simp add: zgcd_commute) + apply (simp add: zmult_commute zdvd_zminus_iff) + prefer 2 + apply (rule_tac n = n in zrelprime_zdvd_zmult) + apply (simp add: zgcd_commute) + apply (simp add: zmult_commute) + apply (auto simp add: dvd_def) + apply (blast intro: sym) + done + +lemma zcong_zless_imp_eq: + "#0 \ a ==> + a < m ==> #0 \ b ==> b < m ==> [a = b] (mod m) ==> a = b" + apply (unfold zcong_def dvd_def) + apply auto + apply (drule_tac f = "\z. z mod m" in arg_cong) + apply (cut_tac z = a and w = b in zless_linear) + apply auto + apply (subgoal_tac [2] "(a - b) mod m = a - b") + apply (rule_tac [3] mod_pos_pos_trivial) + apply auto + apply (subgoal_tac "(m + (a - b)) mod m = m + (a - b)") + apply (rule_tac [2] mod_pos_pos_trivial) + apply auto + done + +lemma zcong_square_zless: + "p \ zprime ==> #0 < a ==> a < p ==> + [a * a = #1] (mod p) ==> a = #1 \ a = p - #1" + apply (cut_tac p = p and a = a in zcong_square) + apply (simp add: zprime_def) + apply (auto intro: zcong_zless_imp_eq) + done + +lemma zcong_not: + "#0 < a ==> a < m ==> #0 < b ==> b < a ==> \ [a = b] (mod m)" + apply (unfold zcong_def) + apply (rule zdvd_not_zless) + apply auto + done + +lemma zcong_zless_0: + "#0 \ a ==> a < m ==> [a = #0] (mod m) ==> a = #0" + apply (unfold zcong_def dvd_def) + apply auto + apply (subgoal_tac "#0 < m") + apply (rotate_tac -1) + apply (simp add: int_0_le_mult_iff) + apply (subgoal_tac "m * k < m * #1") + apply (drule zmult_zless_cancel1 [THEN iffD1]) + apply (auto simp add: linorder_neq_iff) + done + +lemma zcong_zless_unique: + "#0 < m ==> (\!b. #0 \ b \ b < m \ [a = b] (mod m))" + apply auto + apply (subgoal_tac [2] "[b = y] (mod m)") + apply (case_tac [2] "b = #0") + apply (case_tac [3] "y = #0") + apply (auto intro: zcong_trans zcong_zless_0 zcong_zless_imp_eq order_less_le + simp add: zcong_sym) + apply (unfold zcong_def dvd_def) + apply (rule_tac x = "a mod m" in exI) + apply (auto simp add: pos_mod_sign pos_mod_bound) + apply (rule_tac x = "-(a div m)" in exI) + apply (cut_tac a = a and b = m in zmod_zdiv_equality) + apply auto + done + +lemma zcong_iff_lin: "([a = b] (mod m)) = (\k. b = a + m * k)" + apply (unfold zcong_def dvd_def) + apply auto + apply (rule_tac [!] x = "-k" in exI) + apply auto + done + +lemma zgcd_zcong_zgcd: + "#0 < m ==> + zgcd (a, m) = #1 ==> [a = b] (mod m) ==> zgcd (b, m) = #1" + apply (auto simp add: zcong_iff_lin) + done + +lemma aux: "a = c ==> b = d ==> a - b = c - (d::int)" + apply auto + done + +lemma aux: "a - b = (m::int) * (a div m - b div m) + (a mod m - b mod m)" + apply (rule_tac "s" = "(m * (a div m) + a mod m) - (m * (b div m) + b mod m)" + in trans) + prefer 2 + apply (simp add: zdiff_zmult_distrib2) + apply (rule aux) + apply (rule_tac [!] zmod_zdiv_equality) + done - zcong_def "[a=b] (mod m) == m dvd (a-b)" +lemma zcong_zmod: "[a = b] (mod m) = [a mod m = b mod m] (mod m)" + apply (unfold zcong_def) + apply (rule_tac t = "a - b" in ssubst) + apply (rule_tac "m" = "m" in aux) + apply (rule trans) + apply (rule_tac [2] k = m and m = "a div m - b div m" in zdvd_reduce) + apply (simp add: zadd_commute) + done + +lemma zcong_zmod_eq: "#0 < m ==> [a = b] (mod m) = (a mod m = b mod m)" + apply auto + apply (rule_tac m = m in zcong_zless_imp_eq) + prefer 5 + apply (subst zcong_zmod [symmetric]) + apply (simp_all add: pos_mod_bound pos_mod_sign) + apply (unfold zcong_def dvd_def) + apply (rule_tac x = "a div m - b div m" in exI) + apply (rule_tac m1 = m in aux [THEN trans]) + apply auto + done + +lemma zcong_zminus [iff]: "[a = b] (mod -m) = [a = b] (mod m)" + apply (auto simp add: zcong_def) + done + +lemma zcong_zero [iff]: "[a = b] (mod #0) = (a = b)" + apply (auto simp add: zcong_def) + done + +lemma "[a = b] (mod m) = (a mod m = b mod m)" + apply (tactic {* zdiv_undefined_case_tac "m = #0" 1 *}) + apply (case_tac "#0 < m") + apply (simp add: zcong_zmod_eq) + apply (rule_tac t = m in zminus_zminus [THEN subst]) + apply (subst zcong_zminus) + apply (subst zcong_zmod_eq) + apply arith + oops -- {* FIXME: finish this proof? *} + + +subsection {* Modulo *} + +lemma zmod_zdvd_zmod: + "#0 < (m::int) ==> m dvd b ==> (a mod b mod m) = (a mod m)" + apply (unfold dvd_def) + apply auto + apply (subst zcong_zmod_eq [symmetric]) + prefer 2 + apply (subst zcong_iff_lin) + apply (rule_tac x = "k * (a div (m * k))" in exI) + apply (subst zadd_commute) + apply (subst zmult_assoc [symmetric]) + apply (rule_tac zmod_zdiv_equality) + apply assumption + done + + +subsection {* Extended GCD *} + +declare xzgcda.simps [simp del] + +lemma aux1: + "zgcd (r', r) = k --> #0 < r --> + (\sn tn. xzgcda (m, n, r', r, s', s, t', t) = (k, sn, tn))" + apply (rule_tac u = m and v = n and w = r' and x = r and y = s' and + z = s and aa = t' and ab = t in xzgcda.induct) + apply (subst zgcd_eq) + apply (subst xzgcda.simps) + apply auto + apply (case_tac "r' mod r = #0") + prefer 2 + apply (frule_tac a = "r'" in pos_mod_sign) + apply auto + apply arith + apply (rule exI) + apply (rule exI) + apply (subst xzgcda.simps) + apply auto + apply (simp add: zabs_def) + done + +lemma aux2: + "(\sn tn. xzgcda (m, n, r', r, s', s, t', t) = (k, sn, tn)) --> #0 < r --> + zgcd (r', r) = k" + apply (rule_tac u = m and v = n and w = r' and x = r and y = s' and + z = s and aa = t' and ab = t in xzgcda.induct) + apply (subst zgcd_eq) + apply (subst xzgcda.simps) + apply (auto simp add: linorder_not_le) + apply (case_tac "r' mod r = #0") + prefer 2 + apply (frule_tac a = "r'" in pos_mod_sign) + apply auto + apply arith + apply (erule_tac P = "xzgcda ?u = ?v" in rev_mp) + apply (subst xzgcda.simps) + apply auto + apply (simp add: zabs_def) + done + +lemma xzgcd_correct: + "#0 < n ==> (zgcd (m, n) = k) = (\s t. xzgcd m n = (k, s, t))" + apply (unfold xzgcd_def) + apply (rule iffI) + apply (rule_tac [2] aux2 [THEN mp, THEN mp]) + apply (rule aux1 [THEN mp, THEN mp]) + apply auto + done + + +text {* \medskip @{term xzgcd} linear *} + +lemma aux: + "(a - r * b) * m + (c - r * d) * (n::int) = + (a * m + c * n) - r * (b * m + d * n)" + apply (simp add: zdiff_zmult_distrib zadd_zmult_distrib2 zmult_assoc) + done + +lemma aux: + "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)" + apply (rule trans) + apply (rule_tac [2] aux [symmetric]) + apply simp + apply (subst eq_zdiff_eq) + apply (rule trans [symmetric]) + apply (rule_tac b = "s * m + t * n" in zmod_zdiv_equality) + apply (simp add: zmult_commute) + done + +lemma order_le_neq_implies_less: "(x::'a::order) \ y ==> x \ y ==> x < y" + by (rule iffD2 [OF order_less_le conjI]) + +lemma xzgcda_linear [rule_format]: + "#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" + apply (rule_tac u = m and v = n and w = r' and x = r and y = s' and + z = s and aa = t' and ab = t in xzgcda.induct) + apply (subst xzgcda.simps) + apply (simp (no_asm)) + apply (rule impI)+ + apply (case_tac "r' mod r = #0") + apply (simp add: xzgcda.simps) + apply clarify + apply (subgoal_tac "#0 < r' mod r") + apply (rule_tac [2] order_le_neq_implies_less) + apply (rule_tac [2] pos_mod_sign) + apply (cut_tac m = m and n = n and r' = r' and r = r and s' = s' and + s = s and t' = t' and t = t in aux) + apply auto + done + +lemma xzgcd_linear: + "#0 < n ==> xzgcd m n = (r, s, t) ==> r = s * m + t * n" + apply (unfold xzgcd_def) + apply (erule xzgcda_linear) + apply assumption + apply auto + done + +lemma zgcd_ex_linear: + "#0 < n ==> zgcd (m, n) = k ==> (\s t. k = s * m + t * n)" + apply (simp add: xzgcd_correct) + apply safe + apply (rule exI)+ + apply (erule xzgcd_linear) + apply auto + done + +lemma zcong_lineq_ex: + "#0 < n ==> zgcd (a, n) = #1 ==> \x. [a * x = #1] (mod n)" + apply (cut_tac m = a and n = n and k = "#1" in zgcd_ex_linear) + apply safe + apply (rule_tac x = s in exI) + apply (rule_tac b = "s * a + t * n" in zcong_trans) + prefer 2 + apply simp + apply (unfold zcong_def) + apply (simp (no_asm) add: zmult_commute zdvd_zminus_iff) + done + +lemma zcong_lineq_unique: + "#0 < n ==> + zgcd (a, n) = #1 ==> \!x. #0 \ x \ x < n \ [a * x = b] (mod n)" + apply auto + apply (rule_tac [2] zcong_zless_imp_eq) + apply (tactic {* stac (thm "zcong_cancel2" RS sym) 6 *}) + apply (rule_tac [8] zcong_trans) + apply (simp_all (no_asm_simp)) + prefer 2 + apply (simp add: zcong_sym) + apply (cut_tac a = a and n = n in zcong_lineq_ex) + apply auto + apply (rule_tac x = "x * b mod n" in exI) + apply safe + apply (simp_all (no_asm_simp) add: pos_mod_bound pos_mod_sign) + apply (subst zcong_zmod) + apply (subst zmod_zmult1_eq [symmetric]) + apply (subst zcong_zmod [symmetric]) + apply (subgoal_tac "[a * x * b = #1 * b] (mod n)") + apply (rule_tac [2] zcong_zmult) + apply (simp_all add: zmult_assoc) + done end diff -r 2f4976370b7a -r 7eef34adb852 src/HOL/NumberTheory/Primes.thy --- a/src/HOL/NumberTheory/Primes.thy Sat Feb 03 17:43:34 2001 +0100 +++ b/src/HOL/NumberTheory/Primes.thy Sun Feb 04 19:31:13 2001 +0100 @@ -2,207 +2,229 @@ ID: $Id$ Author: Christophe Tabacznyj and Lawrence C Paulson Copyright 1996 University of Cambridge - -The Greatest Common Divisor and Euclid's algorithm - -See H. Davenport, "The Higher Arithmetic". 6th edition. (CUP, 1992) *) +header {* The Greatest Common Divisor and Euclid's algorithm *} + theory Primes = Main: + +text {* + (See H. Davenport, "The Higher Arithmetic". 6th edition. (CUP, 1992)) + + \bigskip +*} + consts - gcd :: "nat*nat=>nat" (*Euclid's algorithm *) + gcd :: "nat * nat => nat" -- {* Euclid's algorithm *} -recdef gcd "measure ((%(m,n).n) ::nat*nat=>nat)" - "gcd (m, n) = (if n=0 then m else gcd(n, m mod n))" +recdef gcd "measure ((\(m, n). n) :: nat * nat => nat)" + "gcd (m, n) = (if n = 0 then m else gcd (n, m mod n))" constdefs - is_gcd :: "[nat,nat,nat]=>bool" (*gcd as a relation*) - "is_gcd p m n == p dvd m & p dvd n & - (ALL d. d dvd m & d dvd n --> d dvd p)" - - coprime :: "[nat,nat]=>bool" - "coprime m n == gcd(m,n) = 1" + is_gcd :: "nat => nat => nat => bool" -- {* @{term gcd} as a relation *} + "is_gcd p m n == p dvd m \ p dvd n \ + (\d. d dvd m \ d dvd n --> d dvd p)" - prime :: "nat set" - "prime == {p. 1

m=1 | m=p)}" - + coprime :: "nat => nat => bool" + "coprime m n == gcd (m, n) = 1" -(************************************************) -(** Greatest Common Divisor **) -(************************************************) - -(*** Euclid's Algorithm ***) + prime :: "nat set" + "prime == {p. 1 < p \ (\m. m dvd p --> m = 1 \ m = p)}" lemma gcd_induct: - "[| !!m. P m 0; - !!m n. [| 0 P m n - |] ==> P (m::nat) (n::nat)" - apply (induct_tac m n rule: gcd.induct) - apply (case_tac "n=0") - apply (simp_all) + "(!!m. P m 0) ==> + (!!m n. 0 < n ==> P n (m mod n) ==> P m n) + ==> P (m::nat) (n::nat)" + apply (induct m n rule: gcd.induct) + apply (case_tac "n = 0") + apply simp_all done -lemma gcd_0 [simp]: "gcd(m,0) = m" - apply (simp); +lemma gcd_0 [simp]: "gcd (m, 0) = m" + apply simp done -lemma gcd_non_0: "0 gcd(m,n) = gcd (n, m mod n)" - apply (simp) - done; +lemma gcd_non_0: "0 < n ==> gcd (m, n) = gcd (n, m mod n)" + apply simp + done -declare gcd.simps [simp del]; +declare gcd.simps [simp del] -lemma gcd_1 [simp]: "gcd(m,1) = 1" +lemma gcd_1 [simp]: "gcd (m, 1) = 1" apply (simp add: gcd_non_0) done -(*gcd(m,n) divides m and n. The conjunctions don't seem provable separately*) -lemma gcd_dvd_both: "gcd(m,n) dvd m & gcd(m,n) dvd n" - apply (induct_tac m n rule: gcd_induct) - apply (simp_all add: gcd_non_0) +text {* + \medskip @{term "gcd (m, n)"} divides @{text m} and @{text n}. The + conjunctions don't seem provable separately. +*} + +lemma gcd_dvd_both: "gcd (m, n) dvd m \ gcd (m, n) dvd n" + apply (induct m n rule: gcd_induct) + apply (simp_all add: gcd_non_0) apply (blast dest: dvd_mod_imp_dvd) done -lemmas gcd_dvd1 [iff] = gcd_dvd_both [THEN conjunct1] -lemmas gcd_dvd2 [iff] = gcd_dvd_both [THEN conjunct2]; +lemmas gcd_dvd1 [iff] = gcd_dvd_both [THEN conjunct1, standard] +lemmas gcd_dvd2 [iff] = gcd_dvd_both [THEN conjunct2, standard] -(*Maximality: for all m,n,k naturals, - if k divides m and k divides n then k divides gcd(m,n)*) -lemma gcd_greatest [rule_format]: "k dvd m --> k dvd n --> k dvd gcd(m,n)" - apply (induct_tac m n rule: gcd_induct) - apply (simp_all add: gcd_non_0 dvd_mod); - done; +text {* + \medskip Maximality: for all @{term m}, @{term n}, @{term k} + naturals, if @{term k} divides @{term m} and @{term k} divides + @{term n} then @{term k} divides @{term "gcd (m, n)"}. +*} + +lemma gcd_greatest: "k dvd m ==> k dvd n ==> k dvd gcd (m, n)" + apply (induct m n rule: gcd_induct) + apply (simp_all add: gcd_non_0 dvd_mod) + done -lemma gcd_greatest_iff [iff]: "(k dvd gcd(m,n)) = (k dvd m & k dvd n)" - apply (blast intro!: gcd_greatest intro: dvd_trans); - done; +lemma gcd_greatest_iff [iff]: "(k dvd gcd (m, n)) = (k dvd m \ k dvd n)" + apply (blast intro!: gcd_greatest intro: dvd_trans) + done + -(*Function gcd yields the Greatest Common Divisor*) -lemma is_gcd: "is_gcd (gcd(m,n)) m n" +text {* + \medskip Function gcd yields the Greatest Common Divisor. +*} + +lemma is_gcd: "is_gcd (gcd (m, n)) m n" apply (simp add: is_gcd_def gcd_greatest) done -(*uniqueness of GCDs*) -lemma is_gcd_unique: "[| is_gcd m a b; is_gcd n a b |] ==> m=n" - apply (simp add: is_gcd_def); +text {* + \medskip Uniqueness of GCDs. +*} + +lemma is_gcd_unique: "is_gcd m a b ==> is_gcd n a b ==> m = n" + apply (simp add: is_gcd_def) apply (blast intro: dvd_anti_sym) done -lemma is_gcd_dvd: "[| is_gcd m a b; k dvd a; k dvd b |] ==> k dvd m" - apply (auto simp add: is_gcd_def); +lemma is_gcd_dvd: "is_gcd m a b ==> k dvd a ==> k dvd b ==> k dvd m" + apply (auto simp add: is_gcd_def) done -(** Commutativity **) + +text {* + \medskip Commutativity +*} lemma is_gcd_commute: "is_gcd k m n = is_gcd k n m" - apply (auto simp add: is_gcd_def); + apply (auto simp add: is_gcd_def) done -lemma gcd_commute: "gcd(m,n) = gcd(n,m)" +lemma gcd_commute: "gcd (m, n) = gcd (n, m)" apply (rule is_gcd_unique) - apply (rule is_gcd) + apply (rule is_gcd) apply (subst is_gcd_commute) apply (simp add: is_gcd) done -lemma gcd_assoc: "gcd(gcd(k,m),n) = gcd(k,gcd(m,n))" +lemma gcd_assoc: "gcd (gcd (k, m), n) = gcd (k, gcd (m, n))" apply (rule is_gcd_unique) - apply (rule is_gcd) - apply (simp add: is_gcd_def); - apply (blast intro: dvd_trans); - done + apply (rule is_gcd) + apply (simp add: is_gcd_def) + apply (blast intro: dvd_trans) + done -lemma gcd_0_left [simp]: "gcd(0,m) = m" +lemma gcd_0_left [simp]: "gcd (0, m) = m" apply (simp add: gcd_commute [of 0]) done -lemma gcd_1_left [simp]: "gcd(1,m) = 1" +lemma gcd_1_left [simp]: "gcd (1, m) = 1" apply (simp add: gcd_commute [of 1]) done -(** Multiplication laws **) +text {* + \medskip Multiplication laws +*} -(*Davenport, page 27*) -lemma gcd_mult_distrib2: "k * gcd(m,n) = gcd(k*m, k*n)" - apply (induct_tac m n rule: gcd_induct) - apply (simp) - apply (case_tac "k=0") - apply (simp_all add: mod_geq gcd_non_0 mod_mult_distrib2) +lemma gcd_mult_distrib2: "k * gcd (m, n) = gcd (k * m, k * n)" + -- {* Davenport, page 27 *} + apply (induct m n rule: gcd_induct) + apply simp + apply (case_tac "k = 0") + apply (simp_all add: mod_geq gcd_non_0 mod_mult_distrib2) done -lemma gcd_mult [simp]: "gcd(k, k*n) = k" - apply (rule gcd_mult_distrib2 [of k 1 n, simplified, THEN sym]) +lemma gcd_mult [simp]: "gcd (k, k * n) = k" + apply (rule gcd_mult_distrib2 [of k 1 n, simplified, symmetric]) done -lemma gcd_self [simp]: "gcd(k,k) = k" +lemma gcd_self [simp]: "gcd (k, k) = k" apply (rule gcd_mult [of k 1, simplified]) done -lemma relprime_dvd_mult: "[| gcd(k,n)=1; k dvd m*n |] ==> k dvd m"; +lemma relprime_dvd_mult: "gcd (k, n) = 1 ==> k dvd m * n ==> k dvd m" apply (insert gcd_mult_distrib2 [of m k n]) - apply (simp) - apply (erule_tac t="m" in ssubst); - apply (simp) + apply simp + apply (erule_tac t = m in ssubst) + apply simp done -lemma relprime_dvd_mult_iff: "gcd(k,n)=1 ==> (k dvd m*n) = (k dvd m)"; +lemma relprime_dvd_mult_iff: "gcd (k, n) = 1 ==> (k dvd m * n) = (k dvd m)" apply (blast intro: relprime_dvd_mult dvd_trans) done -lemma prime_imp_relprime: "[| p: prime; ~ p dvd n |] ==> gcd (p, n) = 1" +lemma prime_imp_relprime: "p \ prime ==> \ p dvd n ==> gcd (p, n) = 1" apply (auto simp add: prime_def) - apply (drule_tac x="gcd(p,n)" in spec) + apply (drule_tac x = "gcd (p, n)" in spec) apply auto apply (insert gcd_dvd2 [of p n]) - apply (simp) + apply simp done -(*This theorem leads immediately to a proof of the uniqueness of factorization. - If p divides a product of primes then it is one of those primes.*) -lemma prime_dvd_mult: "[| p: prime; p dvd m*n |] ==> p dvd m | p dvd n" +text {* + This theorem leads immediately to a proof of the uniqueness of + factorization. If @{term p} divides a product of primes then it is + one of those primes. +*} + +lemma prime_dvd_mult: "p \ prime ==> p dvd m * n ==> p dvd m \ p dvd n" apply (blast intro: relprime_dvd_mult prime_imp_relprime) done -(** Addition laws **) +text {* \medskip Addition laws *} -lemma gcd_add1 [simp]: "gcd(m+n, n) = gcd(m,n)" - apply (case_tac "n=0") - apply (simp_all add: gcd_non_0) +lemma gcd_add1 [simp]: "gcd (m + n, n) = gcd (m, n)" + apply (case_tac "n = 0") + apply (simp_all add: gcd_non_0) done -lemma gcd_add2 [simp]: "gcd(m, m+n) = gcd(m,n)" +lemma gcd_add2 [simp]: "gcd (m, m + n) = gcd (m, n)" apply (rule gcd_commute [THEN trans]) apply (subst add_commute) apply (simp add: gcd_add1) apply (rule gcd_commute) done -lemma gcd_add2' [simp]: "gcd(m, n+m) = gcd(m,n)" +lemma gcd_add2' [simp]: "gcd (m, n + m) = gcd (m, n)" apply (subst add_commute) apply (rule gcd_add2) done -lemma gcd_add_mult: "gcd(m, k*m+n) = gcd(m,n)" - apply (induct_tac "k") - apply (simp_all add: gcd_add2 add_assoc) +lemma gcd_add_mult: "gcd (m, k * m + n) = gcd (m, n)" + apply (induct k) + apply (simp_all add: gcd_add2 add_assoc) done -(** More multiplication laws **) +text {* \medskip More multiplication laws *} -lemma gcd_mult_cancel: "gcd(k,n) = 1 ==> gcd(k*m, n) = gcd(m,n)" +lemma gcd_mult_cancel: "gcd (k, n) = 1 ==> gcd (k * m, n) = gcd (m, n)" apply (rule dvd_anti_sym) apply (rule gcd_greatest) - apply (rule_tac n="k" in relprime_dvd_mult) + apply (rule_tac n = k in relprime_dvd_mult) apply (simp add: gcd_assoc) apply (simp add: gcd_commute) apply (simp_all add: mult_commute gcd_dvd1 gcd_dvd2) - apply (blast intro: gcd_dvd1 dvd_trans); + apply (blast intro: gcd_dvd1 dvd_trans) done end diff -r 2f4976370b7a -r 7eef34adb852 src/HOL/NumberTheory/README --- a/src/HOL/NumberTheory/README Sat Feb 03 17:43:34 2001 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,30 +0,0 @@ -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'. - -Chinese The Chinese Remainder Theorem for an arbitrary finite - number of equations. (The one-equation case is included - in 'IntPrimes') Uses functions for indexing. - -IntFact Factorial on integers and recursively defined set - including all Integers from 2 up to a. Plus definition - of product of finite set. - -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 2f4976370b7a -r 7eef34adb852 src/HOL/NumberTheory/ROOT.ML --- a/src/HOL/NumberTheory/ROOT.ML Sat Feb 03 17:43:34 2001 +0100 +++ b/src/HOL/NumberTheory/ROOT.ML Sun Feb 04 19:31:13 2001 +0100 @@ -1,15 +1,10 @@ -(* 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 -*) +no_document use_thy "Permutation"; -time_use_thy "Primes"; -time_use_thy "Fib"; -with_path "../Induct" time_use_thy "Factorization"; -time_use_thy "Chinese"; -time_use_thy "EulerFermat"; -time_use_thy "WilsonRuss"; -time_use_thy "WilsonBij"; +use_thy "Primes"; +use_thy "Fib"; +use_thy "Factorization"; +use_thy "Chinese"; +use_thy "EulerFermat"; +use_thy "WilsonRuss"; +use_thy "WilsonBij"; diff -r 2f4976370b7a -r 7eef34adb852 src/HOL/NumberTheory/WilsonBij.ML --- a/src/HOL/NumberTheory/WilsonBij.ML Sat Feb 03 17:43:34 2001 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,223 +0,0 @@ -(* 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 (stac order_less_le 1); -by (stac (zle_add1_eq_le RS sym) 1); -by (stac order_less_le 1); -by (rtac inv_not_0 2); -by (rtac inv_not_1 5); -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 (full_simp_tac (simpset() addsimps [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 (asm_simp_tac (simpset() addsimps [zcong_def]) 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 2f4976370b7a -r 7eef34adb852 src/HOL/NumberTheory/WilsonBij.thy --- a/src/HOL/NumberTheory/WilsonBij.thy Sat Feb 03 17:43:34 2001 +0100 +++ b/src/HOL/NumberTheory/WilsonBij.thy Sun Feb 04 19:31:13 2001 +0100 @@ -1,20 +1,262 @@ -(* Title: WilsonBij.thy +(* Title: HOL/NumberTheory/WilsonBij.thy ID: $Id$ - Author: Thomas M. Rasmussen - Copyright 2000 University of Cambridge + Author: Thomas M. Rasmussen + Copyright 2000 University of Cambridge *) -WilsonBij = BijectionRel + IntFact + +header {* Wilson's Theorem using a more abstract approach *} + +theory WilsonBij = BijectionRel + IntFact: + +text {* + Wilson's Theorem using a more ``abstract'' approach based on + bijections between sets. Does not use Fermat's Little Theorem + (unlike Russinoff). +*} + + +subsection {* Definitions and lemmas *} + +constdefs + reciR :: "int => int => int => bool" + "reciR p == + \a b. zcong (a * b) #1 p \ #1 < a \ a < p - #1 \ #1 < b \ b < p - #1" + inv :: "int => int => int" + "inv p a == + if p \ zprime \ #0 < a \ a < p then + (SOME x. #0 \ x \ x < p \ zcong (a * x) #1 p) + else #0" + + +text {* \medskip Inverse *} + +lemma inv_correct: + "p \ zprime ==> #0 < a ==> a < p + ==> #0 \ inv p a \ inv p a < p \ [a * inv p a = #1] (mod p)" + apply (unfold inv_def) + apply (simp (no_asm_simp)) + apply (rule zcong_lineq_unique [THEN ex1_implies_ex, THEN someI_ex]) + apply (erule_tac [2] zless_zprime_imp_zrelprime) + apply (unfold zprime_def) + apply auto + done + +lemmas inv_ge = inv_correct [THEN conjunct1, standard] +lemmas inv_less = inv_correct [THEN conjunct2, THEN conjunct1, standard] +lemmas inv_is_inv = inv_correct [THEN conjunct2, THEN conjunct2, standard] + +lemma inv_not_0: + "p \ zprime ==> #1 < a ==> a < p - #1 ==> inv p a \ #0" + -- {* same as @{text WilsonRuss} *} + apply safe + apply (cut_tac a = a and p = p in inv_is_inv) + apply (unfold zcong_def) + apply auto + apply (subgoal_tac "\ p dvd #1") + apply (rule_tac [2] zdvd_not_zless) + apply (subgoal_tac "p dvd #1") + prefer 2 + apply (subst zdvd_zminus_iff [symmetric]) + apply auto + done -consts - reciR :: "int => [int,int] => bool" - inv :: "[int,int] => int" +lemma inv_not_1: + "p \ zprime ==> #1 < a ==> a < p - #1 ==> inv p a \ #1" + -- {* same as @{text WilsonRuss} *} + apply safe + apply (cut_tac a = a and p = p in inv_is_inv) + prefer 4 + apply simp + apply (subgoal_tac "a = #1") + apply (rule_tac [2] zcong_zless_imp_eq) + apply auto + done + +lemma aux: "[a * (p - #1) = #1] (mod p) = [a = p - #1] (mod p)" + -- {* same as @{text WilsonRuss} *} + apply (unfold zcong_def) + apply (simp add: zdiff_zdiff_eq zdiff_zdiff_eq2 zdiff_zmult_distrib2) + apply (rule_tac s = "p dvd -((a + #1) + (p * -a))" in trans) + apply (simp add: zmult_commute zminus_zdiff_eq) + apply (subst zdvd_zminus_iff) + apply (subst zdvd_reduce) + apply (rule_tac s = "p dvd (a + #1) + (p * -#1)" in trans) + apply (subst zdvd_reduce) + apply auto + done + +lemma inv_not_p_minus_1: + "p \ zprime ==> #1 < a ==> a < p - #1 ==> inv p a \ p - #1" + -- {* same as @{text WilsonRuss} *} + apply safe + apply (cut_tac a = a and p = p in inv_is_inv) + apply auto + apply (simp add: aux) + apply (subgoal_tac "a = p - #1") + apply (rule_tac [2] zcong_zless_imp_eq) + apply auto + done + +text {* + Below is slightly different as we don't expand @{term [source] inv} + but use ``@{text correct}'' theorems. +*} + +lemma inv_g_1: "p \ zprime ==> #1 < a ==> a < p - #1 ==> #1 < inv p a" + apply (subgoal_tac "inv p a \ #1") + apply (subgoal_tac "inv p a \ #0") + apply (subst order_less_le) + apply (subst zle_add1_eq_le [symmetric]) + apply (subst order_less_le) + apply (rule_tac [2] inv_not_0) + apply (rule_tac [5] inv_not_1) + apply auto + apply (rule inv_ge) + apply auto + done + +lemma inv_less_p_minus_1: + "p \ zprime ==> #1 < a ==> a < p - #1 ==> inv p a < p - #1" + -- {* ditto *} + apply (subst order_less_le) + apply (simp add: inv_not_p_minus_1 inv_less) + done + + +text {* \medskip Bijection *} + +lemma aux1: "#1 < x ==> #0 \ (x::int)" + apply auto + done -defs - reciR_def "reciR p == (%a b. zcong (a*b) #1 p & - #1 #0 < (x::int)" + apply auto + done + +lemma aux3: "x \ p - #2 ==> x < (p::int)" + apply auto + done + +lemma aux4: "x \ p - #2 ==> x < (p::int)-#1" + apply auto + done + +lemma inv_inj: "p \ zprime ==> inj_on (inv p) (d22set (p - #2))" + apply (unfold inj_on_def) + apply auto + apply (rule zcong_zless_imp_eq) + apply (tactic {* stac (thm "zcong_cancel" RS sym) 5 *}) + apply (rule_tac [7] zcong_trans) + apply (tactic {* stac (thm "zcong_sym") 8 *}) + apply (erule_tac [7] inv_is_inv) + apply (tactic "Asm_simp_tac 9") + apply (erule_tac [9] inv_is_inv) + apply (rule_tac [6] zless_zprime_imp_zrelprime) + apply (rule_tac [8] inv_less) + apply (rule_tac [7] inv_g_1 [THEN aux2]) + apply (unfold zprime_def) + apply (auto intro: d22set_g_1 d22set_le + aux1 aux2 aux3 aux4) + done + +lemma inv_d22set_d22set: + "p \ zprime ==> inv p ` d22set (p - #2) = d22set (p - #2)" + apply (rule endo_inj_surj) + apply (rule d22set_fin) + apply (erule_tac [2] inv_inj) + apply auto + apply (rule d22set_mem) + apply (erule inv_g_1) + apply (subgoal_tac [3] "inv p xa < p - #1") + apply (erule_tac [4] inv_less_p_minus_1) + apply (auto intro: d22set_g_1 d22set_le aux4) + done + +lemma d22set_d22set_bij: + "p \ zprime ==> (d22set (p - #2), d22set (p - #2)) \ bijR (reciR p)" + apply (unfold reciR_def) + apply (rule_tac s = "(d22set (p - #2), inv p ` d22set (p - #2))" in subst) + apply (simp add: inv_d22set_d22set) + apply (rule inj_func_bijR) + apply (rule_tac [3] d22set_fin) + apply (erule_tac [2] inv_inj) + apply auto + apply (erule inv_is_inv) + apply (erule_tac [5] inv_g_1) + apply (erule_tac [7] inv_less_p_minus_1) + apply (auto intro: d22set_g_1 d22set_le aux2 aux3 aux4) + done + +lemma reciP_bijP: "p \ zprime ==> bijP (reciR p) (d22set (p - #2))" + apply (unfold reciR_def bijP_def) + apply auto + apply (rule d22set_mem) + apply auto + done + +lemma reciP_uniq: "p \ zprime ==> uniqP (reciR p)" + apply (unfold reciR_def uniqP_def) + apply auto + apply (rule zcong_zless_imp_eq) + apply (tactic {* stac (thm "zcong_cancel2" RS sym) 5 *}) + apply (rule_tac [7] zcong_trans) + apply (tactic {* stac (thm "zcong_sym") 8 *}) + apply (rule_tac [6] zless_zprime_imp_zrelprime) + apply auto + apply (rule zcong_zless_imp_eq) + apply (tactic {* stac (thm "zcong_cancel" RS sym) 5 *}) + apply (rule_tac [7] zcong_trans) + apply (tactic {* stac (thm "zcong_sym") 8 *}) + apply (rule_tac [6] zless_zprime_imp_zrelprime) + apply auto + done + +lemma reciP_sym: "p \ zprime ==> symP (reciR p)" + apply (unfold reciR_def symP_def) + apply (simp add: zmult_commute) + apply auto + done + +lemma bijER_d22set: "p \ zprime ==> d22set (p - #2) \ bijER (reciR p)" + apply (rule bijR_bijER) + apply (erule d22set_d22set_bij) + apply (erule reciP_bijP) + apply (erule reciP_uniq) + apply (erule reciP_sym) + done + + +subsection {* Wilson *} + +lemma bijER_zcong_prod_1: + "p \ zprime ==> A \ bijER (reciR p) ==> [setprod A = #1] (mod p)" + apply (unfold reciR_def) + apply (erule bijER.induct) + apply (subgoal_tac [2] "a = #1 \ a = p - #1") + apply (rule_tac [3] zcong_square_zless) + apply auto + apply (subst setprod_insert) + prefer 3 + apply (subst setprod_insert) + apply (auto simp add: fin_bijER) + apply (subgoal_tac "zcong ((a * b) * setprod A) (#1 * #1) p") + apply (simp add: zmult_assoc) + apply (rule zcong_zmult) + apply auto + done + +theorem Wilson_Bij: "p \ zprime ==> [zfact (p - #1) = #-1] (mod p)" + apply (subgoal_tac "zcong ((p - #1) * zfact (p - #2)) (#-1 * #1) p") + apply (rule_tac [2] zcong_zmult) + apply (simp add: zprime_def) + apply (subst zfact.simps) + apply (rule_tac t = "p - #1 - #1" and s = "p - #2" in subst) + apply auto + apply (simp add: zcong_def) + apply (subst d22set_prod_zfact [symmetric]) + apply (rule bijER_zcong_prod_1) + apply (rule_tac [2] bijER_d22set) + apply auto + done end diff -r 2f4976370b7a -r 7eef34adb852 src/HOL/NumberTheory/WilsonRuss.ML --- a/src/HOL/NumberTheory/WilsonRuss.ML Sat Feb 03 17:43:34 2001 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,310 +0,0 @@ -(* Title: WilsonRuss.ML - ID: $Id$ - Author: Thomas M. Rasmussen - Copyright 2000 University of Cambridge -*) - - -(************ Inverse **************) - -Goal "#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 (stac order_less_le 1); -by (stac (zle_add1_eq_le RS sym) 1); -by (stac order_less_le 1); -by (rtac inv_not_0 2); -by (rtac inv_not_1 5); -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 (induct_thm_tac wset.induct "a p" 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 (induct_thm_tac wset_induct "a p" 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 (induct_thm_tac wset_induct "a p" 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 (induct_thm_tac wset_induct "a p" 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 *************) - -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 (arith_tac 1); -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 2f4976370b7a -r 7eef34adb852 src/HOL/NumberTheory/WilsonRuss.thy --- a/src/HOL/NumberTheory/WilsonRuss.thy Sat Feb 03 17:43:34 2001 +0100 +++ b/src/HOL/NumberTheory/WilsonRuss.thy Sun Feb 04 19:31:13 2001 +0100 @@ -1,21 +1,372 @@ -(* Title: WilsonRuss.thy +(* Title: HOL/NumberTheory/WilsonRuss.thy ID: $Id$ - Author: Thomas M. Rasmussen - Copyright 2000 University of Cambridge + Author: Thomas M. Rasmussen + Copyright 2000 University of Cambridge *) -WilsonRuss = EulerFermat + +header {* Wilson's Theorem according to Russinoff *} + +theory WilsonRuss = EulerFermat: + +text {* + Wilson's Theorem following quite closely Russinoff's approach + using Boyer-Moore (using finite sets instead of lists, though). +*} + +subsection {* Definitions and lemmas *} consts - inv :: "[int,int] => int" - wset :: "int*int=>int set" + inv :: "int => int => int" + wset :: "int * int => int set" defs - inv_def "inv p a == (a ^ (nat (p - #2))) mod p" + 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 {})" + + +text {* \medskip @{term [source] inv} *} + +lemma aux: "#1 < m ==> Suc (nat (m - #2)) = nat (m - #1)" + apply (subst int_int_eq [symmetric]) + apply auto + done + +lemma inv_is_inv: + "p \ zprime \ #0 < a \ a < p ==> [a * inv p a = #1] (mod p)" + apply (unfold inv_def) + apply (subst zcong_zmod) + apply (subst zmod_zmult1_eq [symmetric]) + apply (subst zcong_zmod [symmetric]) + apply (subst power_Suc [symmetric]) + apply (subst aux) + apply (erule_tac [2] Little_Fermat) + apply (erule_tac [2] zdvd_not_zless) + apply (unfold zprime_def) + apply auto + done + +lemma inv_distinct: + "p \ zprime \ #1 < a \ a < p - #1 ==> a \ inv p a" + apply safe + apply (cut_tac a = a and p = p in zcong_square) + apply (cut_tac [3] a = a and p = p in inv_is_inv) + apply auto + apply (subgoal_tac "a = #1") + apply (rule_tac [2] m = p in zcong_zless_imp_eq) + apply (subgoal_tac [7] "a = p - #1") + apply (rule_tac [8] m = p in zcong_zless_imp_eq) + apply auto + done + +lemma inv_not_0: + "p \ zprime \ #1 < a \ a < p - #1 ==> inv p a \ #0" + apply safe + apply (cut_tac a = a and p = p in inv_is_inv) + apply (unfold zcong_def) + apply auto + apply (subgoal_tac "\ p dvd #1") + apply (rule_tac [2] zdvd_not_zless) + apply (subgoal_tac "p dvd #1") + prefer 2 + apply (subst zdvd_zminus_iff [symmetric]) + apply auto + done + +lemma inv_not_1: + "p \ zprime \ #1 < a \ a < p - #1 ==> inv p a \ #1" + apply safe + apply (cut_tac a = a and p = p in inv_is_inv) + prefer 4 + apply simp + apply (subgoal_tac "a = #1") + apply (rule_tac [2] zcong_zless_imp_eq) + apply auto + done + +lemma aux: "[a * (p - #1) = #1] (mod p) = [a = p - #1] (mod p)" + apply (unfold zcong_def) + apply (simp add: zdiff_zdiff_eq zdiff_zdiff_eq2 zdiff_zmult_distrib2) + apply (rule_tac s = "p dvd -((a + #1) + (p * -a))" in trans) + apply (simp add: zmult_commute zminus_zdiff_eq) + apply (subst zdvd_zminus_iff) + apply (subst zdvd_reduce) + apply (rule_tac s = "p dvd (a + #1) + (p * -#1)" in trans) + apply (subst zdvd_reduce) + apply auto + done + +lemma inv_not_p_minus_1: + "p \ zprime \ #1 < a \ a < p - #1 ==> inv p a \ p - #1" + apply safe + apply (cut_tac a = a and p = p in inv_is_inv) + apply auto + apply (simp add: aux) + apply (subgoal_tac "a = p - #1") + apply (rule_tac [2] zcong_zless_imp_eq) + apply auto + done + +lemma inv_g_1: + "p \ zprime \ #1 < a \ a < p - #1 ==> #1 < inv p a" + apply (case_tac "#0\ inv p a") + apply (subgoal_tac "inv p a \ #1") + apply (subgoal_tac "inv p a \ #0") + apply (subst order_less_le) + apply (subst zle_add1_eq_le [symmetric]) + apply (subst order_less_le) + apply (rule_tac [2] inv_not_0) + apply (rule_tac [5] inv_not_1) + apply auto + apply (unfold inv_def zprime_def) + apply (simp add: pos_mod_sign) + done + +lemma inv_less_p_minus_1: + "p \ zprime \ #1 < a \ a < p - #1 ==> inv p a < p - #1" + apply (case_tac "inv p a < p") + apply (subst order_less_le) + apply (simp add: inv_not_p_minus_1) + apply auto + apply (unfold inv_def zprime_def) + apply (simp add: pos_mod_bound) + done + +lemma aux: "#5 \ p ==> + nat (p - #2) * nat (p - #2) = Suc (nat (p - #1) * nat (p - #3))" + apply (subst int_int_eq [symmetric]) + apply (simp add: zmult_int [symmetric]) + apply (simp add: zdiff_zmult_distrib zdiff_zmult_distrib2) + done + +lemma zcong_zpower_zmult: + "[x^y = #1] (mod p) \ [x^(y * z) = #1] (mod p)" + apply (induct z) + apply (auto simp add: zpower_zadd_distrib) + apply (subgoal_tac "zcong (x^y * x^(y * n)) (#1 * #1) p") + apply (rule_tac [2] zcong_zmult) + apply simp_all + done + +lemma inv_inv: "p \ zprime \ + #5 \ p \ #0 < a \ a < p ==> inv p (inv p a) = a" + apply (unfold inv_def) + apply (subst zpower_zmod) + apply (subst zpower_zpower) + apply (rule zcong_zless_imp_eq) + prefer 5 + apply (subst zcong_zmod) + apply (subst mod_mod_trivial) + apply (subst zcong_zmod [symmetric]) + apply (subst aux) + apply (subgoal_tac [2] + "zcong (a * a^(nat (p - #1) * nat (p - #3))) (a * #1) p") + apply (rule_tac [3] zcong_zmult) + apply (rule_tac [4] zcong_zpower_zmult) + apply (erule_tac [4] Little_Fermat) + apply (rule_tac [4] zdvd_not_zless) + apply (simp_all add: pos_mod_bound pos_mod_sign) + done + + +text {* \medskip @{term wset} *} + +declare wset.simps [simp del] -recdef wset "measure ((%(a,p).(nat a)) ::int*int=>nat)" - "wset (a,p) = (if #1 + (!!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" +proof - + case antecedent + show ?thesis + apply (rule wset.induct) + apply safe + apply (case_tac [2] "#1 < a") + apply (rule_tac [2] antecedent) + apply simp_all + apply (simp_all add: wset.simps antecedent) + done +qed + +lemma wset_mem_imp_or [rule_format]: + "#1 < a \ b \ wset (a - #1, p) + ==> b \ wset (a, p) --> b = a \ b = inv p a" + apply (subst wset.simps) + apply (unfold Let_def) + apply simp + done + +lemma wset_mem_mem [simp]: "#1 < a ==> a \ wset (a, p)" + apply (subst wset.simps) + apply (unfold Let_def) + apply simp + done + +lemma wset_subset: "#1 < a \ b \ wset (a - #1, p) ==> b \ wset (a, p)" + apply (subst wset.simps) + apply (unfold Let_def) + apply auto + done + +lemma wset_g_1 [rule_format]: + "p \ zprime --> a < p - #1 --> b \ wset (a, p) --> #1 < b" + apply (induct a p rule: wset_induct) + apply auto + apply (case_tac "b = a") + apply (case_tac [2] "b = inv p a") + apply (subgoal_tac [3] "b = a \ b = inv p a") + apply (rule_tac [4] wset_mem_imp_or) + prefer 2 + apply simp + apply (rule inv_g_1) + apply auto + done + +lemma wset_less [rule_format]: + "p \ zprime --> a < p - #1 --> b \ wset (a, p) --> b < p - #1" + apply (induct a p rule: wset_induct) + apply auto + apply (case_tac "b = a") + apply (case_tac [2] "b = inv p a") + apply (subgoal_tac [3] "b = a \ b = inv p a") + apply (rule_tac [4] wset_mem_imp_or) + prefer 2 + apply simp + apply (rule inv_less_p_minus_1) + apply auto + done + +lemma wset_mem [rule_format]: + "p \ zprime --> + a < p - #1 --> #1 < b --> b \ a --> b \ wset (a, p)" + apply (induct a p rule: wset.induct) + apply auto + apply (subgoal_tac "b = a") + apply (rule_tac [2] zle_anti_sym) + apply (rule_tac [4] wset_subset) + apply (simp (no_asm_simp)) + apply auto + done + +lemma wset_mem_inv_mem [rule_format]: + "p \ zprime --> #5 \ p --> a < p - #1 --> b \ wset (a, p) + --> inv p b \ wset (a, p)" + apply (induct a p rule: wset_induct) + apply auto + apply (case_tac "b = a") + apply (subst wset.simps) + apply (unfold Let_def) + apply (rule_tac [3] wset_subset) + apply auto + apply (case_tac "b = inv p a") + apply (simp (no_asm_simp)) + apply (subst inv_inv) + apply (subgoal_tac [6] "b = a \ b = inv p a") + apply (rule_tac [7] wset_mem_imp_or) + apply auto + done + +lemma wset_inv_mem_mem: + "p \ zprime \ #5 \ p \ a < p - #1 \ #1 < b \ b < p - #1 + \ inv p b \ wset (a, p) \ b \ wset (a, p)" + apply (rule_tac s = "inv p (inv p b)" and t = b in subst) + apply (rule_tac [2] wset_mem_inv_mem) + apply (rule inv_inv) + apply simp_all + done + +lemma wset_fin: "finite (wset (a, p))" + apply (induct a p rule: wset_induct) + prefer 2 + apply (subst wset.simps) + apply (unfold Let_def) + apply auto + done + +lemma wset_zcong_prod_1 [rule_format]: + "p \ zprime --> + #5 \ p --> a < p - #1 --> [setprod (wset (a, p)) = #1] (mod p)" + apply (induct a p rule: wset_induct) + prefer 2 + apply (subst wset.simps) + apply (unfold Let_def) + apply auto + apply (subst setprod_insert) + apply (tactic {* stac (thm "setprod_insert") 3 *}) + apply (subgoal_tac [5] + "zcong (a * inv p a * setprod (wset (a - #1, p))) (#1 * #1) p") + prefer 5 + apply (simp add: zmult_assoc) + apply (rule_tac [5] zcong_zmult) + apply (rule_tac [5] inv_is_inv) + apply (tactic "Clarify_tac 4") + apply (subgoal_tac [4] "a \ wset (a - #1, p)") + apply (rule_tac [5] wset_inv_mem_mem) + apply (simp_all add: wset_fin) + apply (rule inv_distinct) + apply auto + done + +lemma d22set_eq_wset: "p \ zprime ==> d22set (p - #2) = wset (p - #2, p)" + apply safe + apply (erule wset_mem) + apply (rule_tac [2] d22set_g_1) + apply (rule_tac [3] d22set_le) + apply (rule_tac [4] d22set_mem) + apply (erule_tac [4] wset_g_1) + prefer 6 + apply (subst zle_add1_eq_le [symmetric]) + apply (subgoal_tac "p - #2 + #1 = p - #1") + apply (simp (no_asm_simp)) + apply (erule wset_less) + apply auto + done + + +subsection {* Wilson *} + +lemma prime_g_5: "p \ zprime \ p \ #2 \ p \ #3 ==> #5 \ p" + apply (unfold zprime_def dvd_def) + apply (case_tac "p = #4") + apply auto + apply (rule notE) + prefer 2 + apply assumption + apply (simp (no_asm)) + apply (rule_tac x = "#2" in exI) + apply safe + apply (rule_tac x = "#2" in exI) + apply auto + apply arith + done + +theorem Wilson_Russ: + "p \ zprime ==> [zfact (p - #1) = #-1] (mod p)" + apply (subgoal_tac "[(p - #1) * zfact (p - #2) = #-1 * #1] (mod p)") + apply (rule_tac [2] zcong_zmult) + apply (simp only: zprime_def) + apply (subst zfact.simps) + apply (rule_tac t = "p - #1 - #1" and s = "p - #2" in subst) + apply auto + apply (simp only: zcong_def) + apply (simp (no_asm_simp)) + apply (case_tac "p = #2") + apply (simp add: zfact.simps) + apply (case_tac "p = #3") + apply (simp add: zfact.simps) + apply (subgoal_tac "#5 \ p") + apply (erule_tac [2] prime_g_5) + apply (subst d22set_prod_zfact [symmetric]) + apply (subst d22set_eq_wset) + apply (rule_tac [2] wset_zcong_prod_1) + apply auto + done end