--- 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
--- 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";
-
-
-
-
--- 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]: "({}, {}) \<in> bijR P"
+ insert: "P a b ==> a \<notin> A ==> b \<notin> B ==> (A, B) \<in> bijR P
+ ==> (insert a A, insert b B) \<in> bijR P"
+
+text {*
+ Add extra condition to @{term insert}: @{term "\<forall>b \<in> B. \<not> 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 == \<forall>a b. a \<in> F \<and> P a b --> b \<in> F"
+
+ uniqP :: "('a => 'a => bool) => bool"
+ "uniqP P == \<forall>a b c d. P a b \<and> P c d --> (a = c) = (b = d)"
+
+ symP :: "('a => 'a => bool) => bool"
+ "symP P == \<forall>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]: "{} \<in> bijER P"
+ insert1: "P a a ==> a \<notin> A ==> A \<in> bijER P ==> insert a A \<in> bijER P"
+ insert2: "P a b ==> a \<noteq> b ==> a \<notin> A ==> b \<notin> A ==> A \<in> bijER P
+ ==> insert a (insert b A) \<in> bijER P"
+
+
+text {* \medskip @{term bijR} *}
+
+lemma fin_bijRl: "(A, B) \<in> bijR P ==> finite A"
+ apply (erule bijR.induct)
+ apply auto
+ done
+
+lemma fin_bijRr: "(A, B) \<in> bijR P ==> finite B"
+ apply (erule bijR.induct)
+ apply auto
+ done
+
+lemma aux_induct:
+ "finite F ==> F \<subseteq> A ==> P {} ==>
+ (!!F a. F \<subseteq> A ==> a \<in> A ==> a \<notin> F ==> P F ==> P (insert a F))
+ ==> P F"
+proof -
+ case antecedent
+ assume major: "finite F"
+ and subs: "F \<subseteq> A"
+ show ?thesis
+ apply (rule subs [THEN rev_mp])
+ apply (rule major [THEN finite_induct])
+ apply (blast intro: antecedent)+
+ done
+qed
+
+lemma aux: "A \<subseteq> B ==> a \<notin> A ==> a \<in> B ==> inj_on f B ==> f a \<notin> f ` A"
+ apply (unfold inj_on_def)
+ apply auto
+ done
+
+lemma aux:
+ "\<forall>a. a \<in> A --> P a (f a) ==> inj_on f A ==> finite A ==> F <= A
+ ==> (F, f ` F) \<in> 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:
+ "\<forall>a. a \<in> A --> P a (f a) ==> inj_on f A ==> finite A
+ ==> (A, f ` A) \<in> bijR P"
+ apply (rule aux)
+ apply auto
+ done
+
+
+text {* \medskip @{term bijER} *}
+
+lemma fin_bijER: "A \<in> bijER P ==> finite A"
+ apply (erule bijER.induct)
+ apply auto
+ done
+
+lemma aux1:
+ "a \<notin> A ==> a \<notin> B ==> F \<subseteq> insert a A ==> F \<subseteq> insert a B ==> a \<in> F
+ ==> \<exists>C. F = insert a C \<and> a \<notin> C \<and> C <= A \<and> C <= B"
+ apply (rule_tac x = "F - {a}" in exI)
+ apply auto
+ done
+
+lemma aux2: "a \<noteq> b ==> a \<notin> A ==> b \<notin> B ==> a \<in> F ==> b \<in> F
+ ==> F \<subseteq> insert a A ==> F \<subseteq> insert b B
+ ==> \<exists>C. F = insert a (insert b C) \<and> a \<notin> C \<and> b \<notin> C \<and> C \<subseteq> A \<and> C \<subseteq> 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 \<notin> C ==> P b b ==> bijP P (insert b C) ==> bijP P C"
+ apply (unfold bijP_def)
+ apply auto
+ apply (subgoal_tac "b \<noteq> a")
+ prefer 2
+ apply clarify
+ apply (simp add: aux_uniq)
+ apply auto
+ done
+
+lemma aux_in2:
+ "symP P ==> uniqP P ==> a \<notin> C ==> b \<notin> C ==> a \<noteq> b ==> P a b
+ ==> bijP P (insert a (insert b C)) ==> bijP P C"
+ apply (unfold bijP_def)
+ apply auto
+ apply (subgoal_tac "aa \<noteq> a")
+ prefer 2
+ apply clarify
+ apply (subgoal_tac "aa \<noteq> b")
+ prefer 2
+ apply clarify
+ apply (simp add: aux_uniq)
+ apply (subgoal_tac "ba \<noteq> 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: "\<forall>a b. Q a \<and> 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 \<in> F) = (b \<in> 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) \<in> bijR P ==> uniqP P ==> symP P
+ ==> \<forall>F. bijP P F \<and> F \<subseteq> A \<and> F \<subseteq> B --> F \<in> bijER P"
+ apply (erule bijR.induct)
+ apply simp
+ apply (case_tac "a = b")
+ apply clarify
+ apply (case_tac "b \<in> 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 \<in> F")
+ apply (case_tac [!] "b \<in> 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 \<in> 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 \<in> 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) \<in> bijR P ==>
+ bijP P A ==> uniqP P ==> symP P ==> A \<in> bijER P"
+ apply (cut_tac A = A and B = A and P = P in aux_bijRER)
+ apply auto
+ done
end
-
--- 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<n; i<=n; m_cond n mf; km_cond n kf mf |] \
-\ ==> EX! x. #0<=x & x<(mf i) & \
-\ [(kf i)*(mhf mf n i)*x = bf i] (mod mf i)";
-by (rtac zcong_lineq_unique 1);
-by (stac zgcd_zmult_cancel 2);
-by (rewrite_goals_tac [m_cond_def,km_cond_def,mhf_def]);
-by (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<n" 1);
-by (arith_tac 2);
-by (case_tac "i" 2);
-by (ALLGOALS Asm_full_simp_tac);
-qed "unique_xi_sol";
-
-Goalw [mhf_def] "[| 0<n; i<=n; j<=n; j~=i |] ==> (mf j) dvd (mhf mf n i)";
-by (case_tac "i=0" 1);
-by (case_tac "i=n" 2);
-by (ALLGOALS Asm_simp_tac);
-by (case_tac "j<i" 3);
-by (rtac zdvd_zmult2 3);
-by (rtac zdvd_zmult 4);
-by (ALLGOALS (rtac funprod_zdvd));
-by (ALLGOALS arith_tac);
-val lemma = result();
-
-Goalw [x_sol_def]
- "[| 0<n; i<=n |] \
-\ ==> (x_sol n kf bf mf) mod (mf i) = \
-\ (xilin_sol i n kf bf mf)*(mhf mf n i) mod (mf i)";
-by (stac funsum_mod 1);
-by (stac funsum_oneelem 1);
-by Auto_tac;
-by (stac (zdvd_iff_zmod_eq_0 RS sym) 1);
-by (rtac zdvd_zmult 1);
-by (rtac lemma 1);
-by Auto_tac;
-qed "x_sol_lin";
-
-
-(* Chinese *)
-
-Goal "[| 0<n; m_cond n mf; km_cond n kf mf |] \
-\ ==> (EX! x. #0 <= x & x < (funprod mf 0 n) & \
-\ (lincong_sol n kf bf mf x))";
-by Safe_tac;
-by (res_inst_tac [("m","funprod mf 0 n")] zcong_zless_imp_eq 2);
-by (rtac zcong_funprod 6);
-by Auto_tac;
-by (res_inst_tac [("x","(x_sol n kf bf mf) mod (funprod mf 0 n)")] exI 1);
-by (rewtac lincong_sol_def);
-by Safe_tac;
-by (stac zcong_zmod 3);
-by (stac zmod_zmult_distrib 3);
-by (stac zmod_zdvd_zmod 3);
-by (stac x_sol_lin 5);
-by (stac (zmod_zmult_distrib RS sym) 7);
-by (stac (zcong_zmod RS sym) 7);
-by (subgoal_tac "#0<=(xilin_sol i n kf bf mf) & \
-\ (xilin_sol i n kf bf mf)<(mf i) & \
-\ [(kf i)*(mhf mf n i)*(xilin_sol i n kf bf mf) = bf i] \
-\ (mod mf i)" 7);
-by (asm_full_simp_tac (simpset() addsimps zmult_ac) 7);
-by (rewtac xilin_sol_def);
-by (Asm_simp_tac 7);
-by (rtac (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";
--- 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 ==
+ (\<forall>i. i \<le> n --> #0 < mf i) \<and>
+ (\<forall>i j. i \<le> n \<and> j \<le> n \<and> i \<noteq> j --> zgcd (mf i, mf j) = #1)"
+
+ km_cond_def:
+ "km_cond n kf mf == \<forall>i. i \<le> n --> zgcd (kf i, mf i) = #1"
+
+ lincong_sol_def:
+ "lincong_sol n kf bf mf x == \<forall>i. i \<le> 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 \<and> i \<le> n \<and> m_cond n mf \<and> km_cond n kf mf then
+ (SOME x. #0 \<le> x \<and> x < mf i \<and> zcong (kf i * mhf mf n i * x) (bf i) (mf i))
+ else #0"
+
+ x_sol_def:
+ "x_sol n kf bf mf == funsum (\<lambda>i. xilin_sol i n kf bf mf * mhf mf n i) 0 n"
+
+
+text {* \medskip @{term funprod} and @{term funsum} *}
+
+lemma funprod_pos: "(\<forall>i. i \<le> 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)]:
+ "(\<forall>i. k \<le> i \<and> i \<le> 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 \<le> i --> i \<le> 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 (\<lambda>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)]:
+ "(\<forall>i. k \<le> i \<and> i \<le> k + l --> f i = #0) --> (funsum f k l) = #0"
+ apply (induct l)
+ apply auto
+ done
+
+lemma funsum_oneelem [rule_format (no_asm)]:
+ "k \<le> j --> j \<le> k + l -->
+ (\<forall>i. k \<le> i \<and> i \<le> k + l \<and> i \<noteq> 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 \<le> 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 \<le> n ==> m_cond n mf ==> km_cond n kf mf
+ ==> \<exists>!x. #0 \<le> x \<and> x < mf i \<and> [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 \<le> n")
+ prefer 4
+ apply arith
+ apply (subgoal_tac "i<n")
+ prefer 2
+ apply arith
+ apply (case_tac [2] i)
+ apply simp_all
+ done
- xilin_sol_def "xilin_sol i n kf bf mf ==
- (if 0<n & i<=n & m_cond n mf & km_cond n kf mf then
- (@ x. #0<=x & x<(mf i) &
- zcong ((kf i)*(mhf mf n i)*x) (bf i) (mf i))
- else #0)"
+lemma aux:
+ "0 < n ==> i \<le> n ==> j \<le> n ==> j \<noteq> 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 \<le> 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
+ ==> \<exists>!x. #0 \<le> x \<and> x < funprod mf 0 n \<and> 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 \<le> xilin_sol i n kf bf mf \<and> xilin_sol i n kf bf mf < mf i
+ \<and> [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
--- 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]: "{} \<in> RsetR m"
+ insert: "A \<in> RsetR m ==> zgcd (a, m) = #1 ==>
+ \<forall>a'. a' \<in> A --> \<not> zcong a a' m ==> insert a A \<in> RsetR m"
-recdef BnorRset "measure ((% (a,m).(nat a)) ::int*int=>nat)"
- "BnorRset (a,m) = (if #0<a then let na = BnorRset (a-#1,m) in
- (if zgcd(a,m) = #1 then insert a na else na)
- else {})"
+recdef BnorRset
+ "measure ((\<lambda>(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 == (\<lambda>a. a * x) ` norRRset m"
+ phi_def: "phi m == card (norRRset m)"
+ is_RRset_def: "is_RRset A m == A \<in> RsetR m \<and> card A = phi m"
+ RRset2norRR_def:
+ "RRset2norRR A m a ==
+ (if #1 < m \<and> is_RRset A m \<and> a \<in> A then
+ SOME b. zcong a b m \<and> b \<in> norRRset m
+ else #0)"
+
+constdefs
+ zcongm :: "int => int => int => bool"
+ "zcongm m == \<lambda>a b. zcong a b m"
+
+lemma abs_eq_1_iff [iff]: "(abs z = (#1::int)) = (z = #1 \<or> 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 \<in> BnorRset (a, m) --> b \<le> 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 \<notin> BnorRset (a, m)"
+ apply (auto dest: Bnor_mem_zle)
+ done
+
+lemma Bnor_mem_zg [rule_format]: "b \<in> 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 \<le> a --> b \<in> 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) \<in> 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' \<le> 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 \<le> 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 ==> \<exists>!b. [a = b] (mod m) \<and> b \<in> 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 \<in> A --> zgcd (a, m) = #1"
+ apply (unfold is_RRset_def)
+ apply (rule RsetR.induct)
+ apply auto
+ done
+
+lemma RsetR_zmult_mono:
+ "A \<in> RsetR m ==>
+ #0 < m ==> zgcd (x, m) = #1 ==> (\<lambda>a. a * x) ` A \<in> 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 \<in> A
+ ==> zcong a (SOME b. [a = b] (mod m) \<and> b \<in> norRRset m) m \<and>
+ (SOME b. [a = b] (mod m) \<and> b \<in> norRRset m) \<in> 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 \<in> A ==>
+ [a = RRset2norRR A m a] (mod m) \<and> RRset2norRR A m a \<in> 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 \<in> 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 \<in> A --> b \<in> 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) ==> \<exists>a. P a \<and> 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 "\<exists>b. ([x = b] (mod m) \<and> b \<in> norRRset m) \<and>
+ ([y = b] (mod m) \<and> b \<in> 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 \<notin> A ==> inj f ==> f a \<notin> f ` A"
+ apply (unfold inj_on_def)
+ apply auto
+ done
- RRset2norRR_def "RRset2norRR A m a ==
- (if #1<m & (is_RRset A m) & a:A
- then @b. zcong a b m & b:(norRRset m) else #0)"
+lemma Bnor_prod_power [rule_format]:
+ "x \<noteq> #0 ==> a < m --> setprod ((\<lambda>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) \<in> bijR (zcongm m) ==> [setprod A = setprod B] (mod m)"
+ apply (unfold zcongm_def)
+ apply (erule bijR.induct)
+ apply (subgoal_tac [2] "a \<notin> A \<and> b \<notin> B \<and> finite A \<and> 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 \<in> zprime ==>
+ a < p --> (\<forall>b. #0 < b \<and> b \<le> 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 \<in> 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 \<in> zprime ==> \<not> 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
--- 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<m";
-by (case_tac "m" 1);
-by Auto_tac;
-qed "one_less_m";
-
-Goal "!!m::nat. [| m ~= m*k; 1<m*k |] ==> 1<k";
-by (case_tac "k" 1);
-by Auto_tac;
-qed "one_less_k";
-
-Goal "!!m::nat. [| 0<k; k*n=k*m |] ==> n=m";
-by Auto_tac;
-qed "mult_left_cancel";
-
-Goal "!!m::nat. [| 0<m; m*n = m |] ==> n=1";
-by (case_tac "n" 1);
-by Auto_tac;
-qed "mn_eq_m_one";
-
-Goal "!!m::nat. [| 0<n; 0<k |] ==> 1<m --> m*n = k --> n<k";
-by (induct_tac "m" 1);
-by Auto_tac;
-qed_spec_mp "prod_mn_less_k";
-
-
-(* --- Prime List & Product --- *)
-
-Goal "prod (xs @ ys) = prod xs * prod ys";
-by (induct_tac "xs" 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsimps [mult_assoc])));
-qed "prod_append";
-
-Goal "prod (x#xs) = prod (y#ys) ==> 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<p";
-by Auto_tac;
-qed "prime_g_one";
-
-Goalw [prime_def] "p:prime ==> 0<p";
-by Auto_tac;
-qed "prime_g_zero";
-
-Goalw [primel_def,prime_def] "primel xs --> 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<n & n~:prime --> (EX m k.1<m & 1<k & m<n & k<n & n=m*k)";
-by (auto_tac (claset() addIs [n_less_m_mult_n, n_less_n_mult_m,
- one_less_m, one_less_k],
- simpset()));
-qed_spec_mp "not_prime_ex_mk";
-
-Goal "[| primel xs; primel ys |] \
-\ ==> 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<n --> (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<n ==> (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<n --> (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";
--- 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 \<subseteq> prime"
+
+primrec
+ "nondec [] = True"
+ "nondec (x # xs) = (case xs of [] => True | y # ys => x \<le> y \<and> 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 \<le> 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) \<noteq> m * k ==> m \<noteq> 1 ==> 1 < m"
+ apply (case_tac m)
+ apply auto
+ done
+
+lemma one_less_k: "(m::nat) \<noteq> 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 \<and> primel ys)"
+ apply (unfold primel_def)
+ apply auto
+ done
+
+lemma prime_primel: "n \<in> prime ==> primel [n] \<and> prod [n] = n"
+ apply (unfold primel_def)
+ apply auto
+ done
+
+lemma prime_nd_one: "p \<in> prime ==> \<not> 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 \<in> prime \<and> primel xs)"
+ apply (unfold primel_def)
+ apply auto
+ done
+
+lemma primes_eq: "p \<in> prime ==> q \<in> 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 \<in> prime ==> 1 < p"
+ apply (unfold prime_def)
+ apply auto
+ done
+
+lemma prime_g_zero: "p \<in> prime ==> 0 < p"
+ apply (unfold prime_def)
+ apply auto
+ done
+
+lemma primel_nempty_g_one [rule_format]:
+ "primel xs --> xs \<noteq> [] --> 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 \<le> 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 ==> \<exists>ys. primel ys \<and> nondec ys \<and> 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 \<and> n \<notin> prime ==>
+ \<exists>m k. 1 < m \<and> 1 < k \<and> m < n \<and> k < n \<and> 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 ==> \<exists>l. primel l \<and> 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 --> (\<exists>l. primel l \<and> prod l = n)"
+ apply (induct n rule: nat_less_induct)
+ apply (rule impI)
+ apply (case_tac "n \<in> 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 ==> \<exists>l. primel l \<and> nondec l \<and> 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 \<in> prime ==> p dvd (prod xs) --> (\<exists>m. m:set xs \<and> 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
+ ==> \<exists>m. m \<in> set ys \<and> 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 \<in> 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 \<in> 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 ==> \<exists>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 \<in> prime ==> xs = []"
+ apply (auto intro: primel_one_empty simp add: prime_def)
+ done
+
+lemma uniq_ex_aux:
+ "\<forall>m. m < prod ys --> (\<forall>xs ys. primel xs \<and> primel ys \<and>
+ prod xs = prod ys \<and> 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]:
+ "\<forall>xs ys. primel xs \<and> primel ys \<and> prod xs = prod ys \<and> 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]:
+ "\<forall>n. 1 < n --> (\<exists>!l. primel l \<and> nondec l \<and> prod l = n)"
+ apply safe
+ apply (erule nondec_factor_exists)
+ apply (rule perm_nondec_unique)
+ apply (rule factor_unique)
+ apply simp_all
+ done
+
+end
--- 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<n ==> 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<m ==> 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";
-
--- 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) \<noteq> 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 \<le> 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 (\<lambda>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
--- 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<a" 2);
-by (rtac prem2 2);
-by (ALLGOALS Asm_simp_tac);
-by (ALLGOALS (asm_simp_tac (simpset() addsimps [d22set_eq,prem1])));
-qed "d22set_induct";
-
-Goal "b:(d22set a) --> #1<b";
-by (induct_thm_tac d22set_induct "a" 1);
-by (stac d22set_eq 2);
-by Auto_tac;
-qed_spec_mp "d22set_g_1";
-
-Goal "b:(d22set a) --> 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 ==> b~:(d22set a)";
-by (auto_tac (claset() addDs [d22set_le], simpset()));
-qed "d22set_le_swap";
-
-Goal "#1<b --> 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<a" 1);
-by (asm_full_simp_tac (simpset() addsimps [d22set_eq,zfact_eq]) 2);
-by (asm_full_simp_tac (simpset() addsimps [d22set_fin,d22set_le_swap]) 1);
-qed "d22set_prod_zfact";
-
--- a/src/HOL/NumberTheory/IntFact.thy Sat Feb 03 17:43:34 2001 +0100
+++ b/src/HOL/NumberTheory/IntFact.thy Sun Feb 04 19:31:13 2001 +0100
@@ -1,23 +1,118 @@
-(* Title: IntFact.thy
+(* Title: HOL/NumberTheory/IntFact.thy
ID: $Id$
- Author: Thomas M. Rasmussen
- Copyright 2000 University of Cambridge
+ Author: Thomas M. Rasmussen
+ Copyright 2000 University of Cambridge
*)
-IntFact = IntPrimes +
+header {* Factorial on integers *}
+
+theory IntFact = IntPrimes:
+
+text {*
+ Factorial on integers and recursively defined set including all
+ Integers from @{term 2} up to @{term a}. Plus definition of product
+ of finite set.
+
+ \bigskip
+*}
consts
- zfact :: int => 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 ((\<lambda>n. nat n) :: int => nat)"
+ "zfact n = (if n \<le> #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 ((\<lambda>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 \<notin> 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<a then insert a (d22set (a-#1)) else {})"
+lemma d22set_g_1 [rule_format]: "b \<in> 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 \<in> d22set a --> b \<le> a"
+ apply (induct a rule: d22set_induct)
+ prefer 2
+ apply (subst d22set.simps)
+ apply auto
+ done
+
+lemma d22set_le_swap: "a < b ==> b \<notin> d22set a"
+ apply (auto dest: d22set_le)
+ done
+
+lemma d22set_mem [rule_format]: "#1 < b --> b \<le> a --> b \<in> 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
--- 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; #0<n; m dvd n; n dvd m |] ==> m = (n::int)";
-by Auto_tac;
-by (asm_full_simp_tac
- (simpset() addsimps [zmult_assoc,zmult_eq_self_iff,
- int_0_less_mult_iff, zmult_eq_1_iff]) 1);
-qed "zdvd_anti_sym";
-
-Goalw [dvd_def] "[| k dvd m; k dvd n |] ==> k dvd (m+n :: int)";
-by (blast_tac (claset() addIs [zadd_zmult_distrib2 RS sym]) 1);
-qed "zdvd_zadd";
-
-Goalw [dvd_def] "[| k dvd m; k dvd n |] ==> k dvd (m-n :: int)";
-by (blast_tac (claset() addIs [zdiff_zmult_distrib2 RS sym]) 1);
-qed "zdvd_zdiff";
-
-Goal "[| k dvd m-n; k dvd n |] ==> k dvd (m::int)";
-by (subgoal_tac "m=n+(m-n)" 1);
-by (etac ssubst 1);
-by (blast_tac (claset() addIs [zdvd_zadd]) 1);
-by (Simp_tac 1);
-qed "zdvd_zdiffD";
-
-Goalw [dvd_def] "k dvd (n::int) ==> k dvd m*n";
-by (blast_tac (claset() addIs [zmult_left_commute]) 1);
-qed "zdvd_zmult";
-
-Goal "k dvd (m::int) ==> k dvd m*n";
-by (stac zmult_commute 1);
-by (etac zdvd_zmult 1);
-qed "zdvd_zmult2";
-
-(* k dvd m*k *)
-AddIffs [zdvd_refl RS zdvd_zmult, zdvd_refl RS zdvd_zmult2];
-
-Goalw [dvd_def] "j*k dvd n ==> j dvd (n::int)";
-by (full_simp_tac (simpset() addsimps [zmult_assoc]) 1);
-by (Blast_tac 1);
-qed "zdvd_zmultD2";
-
-Goal "j*k dvd n ==> k dvd (n::int)";
-by (rtac zdvd_zmultD2 1);
-by (stac zmult_commute 1);
-by (assume_tac 1);
-qed "zdvd_zmultD";
-
-Goalw [dvd_def] "[| i dvd m; j dvd (n::int) |] ==> i*j dvd m*n";
-by (Clarify_tac 1);
-by (res_inst_tac [("x","k*ka")] exI 1);
-by (asm_simp_tac (simpset() addsimps zmult_ac) 1);
-qed "zdvd_zmult_mono";
-
-Goal "(k dvd n + k*m) = (k dvd (n::int))";
-by (rtac iffI 1);
-by (etac zdvd_zadd 2);
-by (subgoal_tac "n = (n+k*m)-k*m" 1);
-by (etac ssubst 1);
-by (etac zdvd_zdiff 1);
-by (ALLGOALS Simp_tac);
-qed "zdvd_reduce";
-
-Goalw [dvd_def] "[| f dvd m; f dvd (n::int) |] ==> f dvd m mod n";
-by (auto_tac (claset(), simpset() addsimps [zmod_zmult_zmult1]));
-qed "zdvd_zmod";
-
-Goal "[| k dvd m mod n; k dvd n |] ==> k dvd (m::int)";
-by (subgoal_tac "k dvd n*(m div n) + m mod n" 1);
-by (asm_simp_tac (simpset() addsimps [zdvd_zadd, zdvd_zmult2]) 2);
-by (asm_full_simp_tac (simpset() addsimps [zmod_zdiv_equality RS sym]) 1);
-qed "zdvd_zmod_imp_zdvd";
-
-Goalw [dvd_def] "(k dvd n) = (n mod (k::int) = #0)";
-by (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<m; m<n |] ==> ~n dvd (m::int)";
-by Auto_tac;
-by (subgoal_tac "#0<n" 1);
-by (blast_tac (claset() addIs [zless_trans]) 2);
-by (asm_full_simp_tac (simpset() addsimps [int_0_less_mult_iff]) 1);
-by (subgoal_tac "n*k < n*#1" 1);
-by (dtac (zmult_zless_cancel1 RS iffD1) 1);
-by Auto_tac;
-qed "zdvd_not_zless";
-
-Goal "(int m dvd z) = (m dvd nat(abs z))";
-by (auto_tac (claset(),
- simpset() addsimps [dvd_def, nat_abs_mult_distrib]));
-by (auto_tac (claset(), simpset() addsimps [nat_eq_iff, zabs_eq_iff]));
-by (res_inst_tac [("x","-(int k)")] exI 2);
-by (auto_tac (claset(), simpset() addsimps [zmult_int RS sym]));
-qed "int_dvd_iff";
-
-Goal "(z dvd int m) = (nat(abs z) dvd m)";
-by (auto_tac (claset(),
- simpset() addsimps [dvd_def, zabs_def, zmult_int RS sym]));
-by (res_inst_tac [("x","nat k")] exI 3);
-by (res_inst_tac [("x","-(int k)")] exI 2);
-by (res_inst_tac [("x","nat (-k)")] exI 1);
-by (cut_inst_tac [("k","m")] int_less_0_conv 3);
-by (cut_inst_tac [("k","m")] int_less_0_conv 1);
-by (auto_tac (claset(),
- simpset() addsimps [int_0_le_mult_iff, zmult_less_0_iff,
- nat_mult_distrib RS sym, nat_eq_iff2]));
-qed "dvd_int_iff";
-
-Goal "(nat z dvd m) = (if #0 <= z then (z dvd int m) else m=0)";
-by (auto_tac (claset(), simpset() addsimps [dvd_def, zmult_int RS sym]));
-by (res_inst_tac [("x","nat k")] exI 1);
-by (cut_inst_tac [("k","m")] int_less_0_conv 1);
-by (auto_tac (claset(),
- simpset() addsimps [int_0_le_mult_iff, zmult_less_0_iff,
- nat_mult_distrib RS sym, nat_eq_iff2]));
-qed "nat_dvd_iff";
-
-Goal "(-z dvd w) = (z dvd (w::int))";
-by (auto_tac (claset(), simpset() addsimps [dvd_def]));
-by (ALLGOALS (res_inst_tac [("x","-k")] exI));
-by Auto_tac;
-qed "zminus_dvd_iff";
-
-Goal "(z dvd -w) = (z dvd (w::int))";
-by (auto_tac (claset(), simpset() addsimps [dvd_def]));
-by (dtac (zminus_equation RS iffD1) 1);
-by (ALLGOALS (res_inst_tac [("x","-k")] exI));
-by Auto_tac;
-qed "dvd_zminus_iff";
-AddIffs [zminus_dvd_iff, dvd_zminus_iff];
-
-
-(************************************************)
-(** Euclid's Algorithm and GCD **)
-(************************************************)
-
-Goal "zgcd(m,#0) = abs m";
-by (simp_tac (simpset() addsimps [zgcd_def, zabs_def]) 1);
-qed "zgcd_0";
-Addsimps [zgcd_0];
-
-Goal"zgcd(#0,m) = abs m";
-by (simp_tac (simpset() addsimps [zgcd_def, zabs_def]) 1);
-qed "zgcd_0_left";
-Addsimps [zgcd_0_left];
-
-Goal "zgcd(-m,n) = zgcd(m,n)";
-by (simp_tac (simpset() addsimps [zgcd_def]) 1);
-qed "zgcd_zminus";
-Addsimps [zgcd_zminus];
-
-Goal "zgcd(m,-n) = zgcd(m,n)";
-by (simp_tac (simpset() addsimps [zgcd_def]) 1);
-qed "zgcd_zminus2";
-Addsimps [zgcd_zminus2];
-
-Goal "#0<n ==> 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<n; n<p |] ==> zgcd(n,p) = #1";
-by (etac zprime_imp_zrelprime 1);
-by (etac zdvd_not_zless 1);
-by (assume_tac 1);
-qed "zless_zprime_imp_zrelprime";
-
-Goal "[| #0<=(m::int); p:zprime; p dvd m*n |] ==> p dvd m | p dvd n";
-by Safe_tac;
-by (rtac zrelprime_zdvd_zmult 1);
-by (rtac zprime_imp_zrelprime 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 ==> (m dvd n) = (zgcd(n,m) = m)";
-by Safe_tac;
-by (res_inst_tac [("n","zgcd(n,m)")] zdvd_trans 2);
-by (rtac zgcd_zdvd1 3);
-by (ALLGOALS Asm_simp_tac);
-by (rewtac dvd_def);
-by Auto_tac;
-qed "zdvd_iff_zgcd";
-
-
-(************************************************)
-(** Congruences **)
-(************************************************)
-
-Goalw [zcong_def] "[a=b](mod #1)";
-by Auto_tac;
-qed "zcong_1";
-Addsimps [zcong_1];
-
-Goalw [zcong_def] "[k = k] (mod m)";
-by Auto_tac;
-qed "zcong_refl";
-Addsimps [zcong_refl];
-
-Goalw [zcong_def,dvd_def] "[a = b](mod m) = [b = a](mod m)";
-by Auto_tac;
-by (ALLGOALS (res_inst_tac [("x","-k")] exI));
-by Auto_tac;
-qed "zcong_sym";
-
-Goalw [zcong_def]
- "[| [a = b] (mod m); [c = d] (mod m) |] ==> [a+c = b+d](mod m)";
-by (res_inst_tac [("s","(a-b)+(c-d)")] subst 1);
-by (rtac zdvd_zadd 2);
-by Auto_tac;
-qed "zcong_zadd";
-
-Goalw [zcong_def]
- "[| [a = b] (mod m); [c = d] (mod m) |] ==> [a-c = b-d](mod m)";
-by (res_inst_tac [("s","(a-b)-(c-d)")] subst 1);
-by (rtac zdvd_zdiff 2);
-by Auto_tac;
-qed "zcong_zdiff";
-
-Goalw [zcong_def,dvd_def]
- "[| [a = b](mod m); [b = c](mod m) |] ==> [a = c](mod m)";
-by Auto_tac;
-by (res_inst_tac [("x","k+ka")] exI 1);
-by (asm_full_simp_tac (simpset() addsimps zadd_ac@[zadd_zmult_distrib2]) 1);
-qed "zcong_trans";
-
-Goal "[| [a = b] (mod m); [c = d] (mod m) |] ==> [a*c = b*d](mod m)";
-by (res_inst_tac [("b","b*c")] zcong_trans 1);
-by (rewtac zcong_def);
-by (res_inst_tac [("s","c*(a-b)")] subst 1);
-by (res_inst_tac [("s","b*(c-d)")] subst 3);
-by (blast_tac (claset() addIs [zdvd_zmult]) 4);
-by (blast_tac (claset() addIs [zdvd_zmult]) 2);
-by (ALLGOALS (asm_simp_tac (simpset() addsimps [zdiff_zmult_distrib2,
- zmult_commute])));
-qed "zcong_zmult";
-
-Goal "[a = b] (mod m) ==> [a*k = b*k](mod m)";
-by (rtac zcong_zmult 1);
-by (ALLGOALS Asm_simp_tac);
-qed "zcong_scalar";
-
-Goal "[a = b] (mod m) ==> [k*a = k*b](mod m)";
-by (rtac zcong_zmult 1);
-by (ALLGOALS Asm_simp_tac);
-qed "zcong_scalar2";
-
-Goalw [zcong_def] "[a*m = b*m](mod m)";
-by (rtac zdvd_zdiff 1);
-by (ALLGOALS Simp_tac);
-qed "zcong_zmult_self";
-
-Goalw [zcong_def]
- "[| p:zprime; #0<a; [a*a = #1](mod p) |] \
-\ ==> [a=#1](mod p) | [a = p-#1](mod p)";
-by (rtac zprime_zdvd_zmult 1);
-by (res_inst_tac [("s","a*a - #1 + p*(#1-a)")] subst 3);
-by (simp_tac (simpset() addsimps [zdvd_reduce]) 4);
-by (ALLGOALS (asm_simp_tac (simpset()
- addsimps [zdiff_zmult_distrib,zmult_commute,zdiff_zmult_distrib2])));
-qed "zcong_square";
-
-Goal "[| #0<=m; zgcd(k,m) = #1 |] ==> [a*k = b*k](mod m) = [a = b](mod m)";
-by Safe_tac;
-by (blast_tac (claset() addIs [zcong_scalar]) 2);
-by (case_tac "b<a" 1);
-by (stac zcong_sym 2);
-by (rewrite_goals_tac [zcong_def]);
-by (ALLGOALS (rtac zrelprime_zdvd_zmult));
-by (ALLGOALS (asm_simp_tac (simpset() addsimps [zdiff_zmult_distrib])));
-by (subgoal_tac "m dvd (-(a*k - b*k))" 1);
-by (asm_full_simp_tac (simpset() addsimps [zminus_zdiff_eq]) 1);
-by (stac zdvd_zminus_iff 1);
-by (assume_tac 1);
-qed "zcong_cancel";
-
-Goal "[| #0<=m; zgcd(k,m) = #1 |] ==> [k*a = k*b](mod m) = [a = b](mod m)";
-by (asm_simp_tac (simpset() addsimps [zmult_commute,zcong_cancel]) 1);
-qed "zcong_cancel2";
-
-Goalw [zcong_def,dvd_def]
- "[| [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<m; #0<=b; b<m; [a = b] (mod m) |] ==> 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; a<p; [a*a = #1](mod p) |] ==> 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; a<m; #0<b; b<a |] ==> ~[a = b] (mod m) ";
-by (rtac zdvd_not_zless 1);
-by Auto_tac;
-qed "zcong_not";
-
-Goalw [zcong_def,dvd_def] "[| #0<=a; a<m; [a=#0](mod m) |] ==> a = #0";
-by Auto_tac;
-by (subgoal_tac "#0<m" 1);
-by (rotate_tac ~1 1);
-by (asm_full_simp_tac (simpset() addsimps [int_0_le_mult_iff]) 1);
-by (subgoal_tac "m*k<m*#1" 1);
-by (dtac (zmult_zless_cancel1 RS iffD1) 1);
-by (auto_tac (claset(), simpset() addsimps [linorder_neq_iff]));
-qed "zcong_zless_0";
-
-Goal "#0<m ==> (EX! b. #0<=b & b<m & [a = b] (mod m))";
-by Auto_tac;
-by (subgoal_tac "[b = y] (mod m)" 2);
-by (case_tac "b=#0" 2);
-by (case_tac "y=#0" 3);
-by (auto_tac (claset() addIs [zcong_trans,zcong_zless_0,
- zcong_zless_imp_eq,order_less_le],
- simpset() addsimps [zcong_sym]));
-by (rewrite_goals_tac [zcong_def,dvd_def]);
-by (res_inst_tac [("x","a mod m")] exI 1);
-by (auto_tac (claset(),simpset() addsimps [pos_mod_sign,pos_mod_bound]));
-by (res_inst_tac [("x","-(a div m)")] exI 1);
-by (cut_inst_tac [("a","a"),("b","m")] zmod_zdiv_equality 1);
-by Auto_tac;
-qed "zcong_zless_unique";
-
-Goalw [zcong_def,dvd_def] "([a = b] (mod m)) = (EX k. b = a + m*k)";
-by Auto_tac;
-by (ALLGOALS (res_inst_tac [("x","-k")] exI));
-by Auto_tac;
-qed "zcong_iff_lin";
-
-Goal "[| #0<m; zgcd(a,m) = #1; [a = b] (mod m) |] ==> zgcd(b,m) = #1";
-by (auto_tac (claset(),simpset() addsimps [zcong_iff_lin]));
-qed "zgcd_zcong_zgcd";
-
-Goal "[| a=c; b=d |] ==> a-b = c-(d::int)";
-by Auto_tac;
-val lemma = result();
-
-Goal "a - b = (m::int) * (a div m - b div m) + (a mod m - b mod m)";
-by (res_inst_tac [("s","(m * (a div m) + a mod m) - \
-\ (m * (b div m) + b mod m)")] trans 1);
-by (simp_tac (simpset() addsimps [zdiff_zmult_distrib2]) 2);
-by (rtac lemma 1);
-by (ALLGOALS (rtac zmod_zdiv_equality));
-val lemma = result();
-
-Goalw [zcong_def] "[a = b] (mod m) = [a mod m = b mod m](mod m)";
-by (res_inst_tac [("t","a-b")] ssubst 1);
-by (res_inst_tac [("m","m")] lemma 1);
-by (rtac trans 1);
-by (res_inst_tac [("k","m"),("m","a div m - b div m")] zdvd_reduce 2);
-by (simp_tac (simpset() addsimps [zadd_commute]) 1);
-qed "zcong_zmod";
-
-Goal "#0<m ==> [a = b] (mod m) = (a mod m = b mod m)";
-by Auto_tac;
-by (res_inst_tac [("m","m")] zcong_zless_imp_eq 1);
-by (stac (zcong_zmod RS sym) 5);
-by (ALLGOALS (asm_simp_tac (simpset() addsimps [pos_mod_bound,pos_mod_sign])));
-by (rewrite_goals_tac [zcong_def,dvd_def]);
-by (res_inst_tac [("x","a div m - b div m")] exI 1);
-by (res_inst_tac [("m1","m")] (lemma RS trans) 1);
-by Auto_tac;
-qed "zcong_zmod_eq";
-
-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<m" 1);
-by (asm_simp_tac (simpset() addsimps [zcong_zmod_eq]) 1);
-by (res_inst_tac [("t","m")] (zminus_zminus RS subst) 1);
-by (stac zcong_zminus 1);
-by (stac zcong_zmod_eq 1);
-by (arith_tac 1);
-(*FIXME: finish this proof?*)
-
-(************************************************)
-(** Modulo **)
-(************************************************)
-
-Goalw [dvd_def] "[| #0<(m::int); m dvd b |] ==> (a mod b mod m) = (a mod m)";
-by Auto_tac;
-by (stac (zcong_zmod_eq RS sym) 1);
-by (stac zcong_iff_lin 2);
-by (res_inst_tac [("x","k*(a div (m*k))")] exI 2);
-by (stac zadd_commute 2);
-by (stac (zmult_assoc RS sym) 2);
-by (rtac zmod_zdiv_equality 2);
-by (assume_tac 1);
-qed "zmod_zdvd_zmod";
-
-
-(************************************************)
-(** Extended GCD **)
-(************************************************)
-
-val [xzgcda_eq] = xzgcda.simps;
-Delsimps xzgcda.simps;
-
-Goal "zgcd(r',r) = k --> #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<r --> xzgcda(m,n,r',r,s',s,t',t) = (rn,sn,tn) \
-\ --> r' = s'*m + t'*n --> r = s*m + t*n --> rn = sn*m + tn*n";
-by (res_inst_tac [("u","m"),("v","n"),("w","r'"),("x","r"),
- ("y","s'"),("z","s"),("aa","t'"),("ab","t")]
- xzgcda.induct 1);
-by (stac xzgcda_eq 1);
-by (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<n; xzgcd m n = (r,s,t) |] ==> r = s*m + t*n";
-by (etac xzgcda_linear 1);
-by (assume_tac 1);
-by Auto_tac;
-qed "xzgcd_linear";
-
-Goal "[| #0<n; zgcd(m,n) = k |] ==> (EX s t. k = s*m + t*n)";
-by (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<n; zgcd(a,n) = #1 |] ==> EX x. [a*x = #1](mod n)";
-by (cut_inst_tac [("m","a"),("n","n"),("k","#1")] zgcd_ex_linear 1);
-by Safe_tac;
-by (res_inst_tac [("x","s")] exI 1);
-by (res_inst_tac [("b","s*a+t*n")] zcong_trans 1);
-by (Asm_simp_tac 2);
-by (rewtac zcong_def);
-by (simp_tac (simpset() addsimps [zmult_commute,zdvd_zminus_iff]) 1);
-qed "zcong_lineq_ex";
-
-Goal "[| #0<n; zgcd(a,n) = #1 |] ==> EX! x. #0<=x & x<n & [a*x = b](mod n)";
-by Auto_tac;
-by (rtac zcong_zless_imp_eq 2);
-by (stac (zcong_cancel2 RS sym) 6);
-by (rtac zcong_trans 8);
-by (ALLGOALS Asm_simp_tac);
-by (asm_full_simp_tac (simpset() addsimps [zcong_sym]) 2);
-by (cut_inst_tac [("a","a"),("n","n")] zcong_lineq_ex 1);
-by Auto_tac;
-by (res_inst_tac [("x","x*b mod n")] exI 1);
-by Safe_tac;
-by (ALLGOALS (asm_simp_tac (simpset() addsimps [pos_mod_bound,pos_mod_sign])));
-by (stac zcong_zmod 1);
-by (stac (zmod_zmult1_eq RS sym) 1);
-by (stac (zcong_zmod RS sym) 1);
-by (subgoal_tac "[a*x*b = #1*b](mod n)" 1);
-by (rtac zcong_zmult 2);
-by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [zmult_assoc])));
-qed "zcong_lineq_unique";
-
--- a/src/HOL/NumberTheory/IntPrimes.thy Sat Feb 03 17:43:34 2001 +0100
+++ b/src/HOL/NumberTheory/IntPrimes.thy Sun Feb 04 19:31:13 2001 +0100
@@ -1,34 +1,841 @@
-(* Title: IntPrimes.thy
+(* Title: HOL/NumberTheory/IntPrimes.thy
ID: $Id$
- Author: Thomas M. Rasmussen
- Copyright 2000 University of Cambridge
+ Author: Thomas M. Rasmussen
+ Copyright 2000 University of Cambridge
*)
-IntPrimes = Primes +
+header {* Divisibility and prime numbers (on integers) *}
+
+theory IntPrimes = Primes:
+
+text {*
+ The @{text dvd} relation, GCD, Euclid's extended algorithm, primes,
+ congruences (all on the Integers). Comparable to theory @{text
+ Primes}, but @{text dvd} is included here as it is not present in
+ main HOL. Also includes extended GCD and congruences not present in
+ @{text Primes}.
+*}
+
+
+subsection {* Definitions *}
consts
- 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)"
- 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 ((\<lambda>(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 \<le> #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 == \<lambda>(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 \<and> (\<forall>m. m dvd p --> m = #1 \<or> m = p)}"
+ zcong_def: "[a = b] (mod m) == m dvd (a - b)"
+
+
+lemma zabs_eq_iff:
+ "(abs (z::int) = w) = (z = w \<and> #0 <= z \<or> z = -w \<and> 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 \<le> 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 ==> \<not> 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 \<le> 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 \<and> 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 \<le> 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 \<le> 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 \<le> 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 \<le> 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 \<le> 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 \<le> m")
+ apply (blast intro: aux)
+ apply (subgoal_tac "k dvd -m")
+ apply (rule_tac [2] aux)
+ apply auto
+ done
+
+lemma zprime_imp_zrelprime:
+ "p \<in> zprime ==> \<not> p dvd n ==> zgcd (n, p) = #1"
+ apply (unfold zprime_def)
+ apply auto
+ done
+
+lemma zless_zprime_imp_zrelprime:
+ "p \<in> 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 \<le> (m::int) ==> p \<in> zprime ==> p dvd m * n ==> p dvd m \<or> 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<p & (ALL m. m dvd p --> 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 \<in> zprime ==> #0 < a ==> [a * a = #1] (mod p)
+ ==> [a = #1] (mod p) \<or> [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 \<le> 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 \<le> 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 \<le> 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 \<le> a ==>
+ a < m ==> #0 \<le> b ==> b < m ==> [a = b] (mod m) ==> a = b"
+ apply (unfold zcong_def dvd_def)
+ apply auto
+ apply (drule_tac f = "\<lambda>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 \<in> zprime ==> #0 < a ==> a < p ==>
+ [a * a = #1] (mod p) ==> a = #1 \<or> 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 ==> \<not> [a = b] (mod m)"
+ apply (unfold zcong_def)
+ apply (rule zdvd_not_zless)
+ apply auto
+ done
+
+lemma zcong_zless_0:
+ "#0 \<le> 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 ==> (\<exists>!b. #0 \<le> b \<and> b < m \<and> [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)) = (\<exists>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 -->
+ (\<exists>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:
+ "(\<exists>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) = (\<exists>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) \<le> y ==> x \<noteq> 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 ==> (\<exists>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 ==> \<exists>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 ==> \<exists>!x. #0 \<le> x \<and> x < n \<and> [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
--- 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 ((\<lambda>(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 \<and> p dvd n \<and>
+ (\<forall>d. d dvd m \<and> d dvd n --> d dvd p)"
- prime :: "nat set"
- "prime == {p. 1<p & (ALL m. m dvd p --> 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 \<and> (\<forall>m. m dvd p --> m = 1 \<or> m = p)}"
lemma gcd_induct:
- "[| !!m. P m 0;
- !!m n. [| 0<n; P n (m mod n) |] ==> 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<n ==> 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 \<and> 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 \<and> 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 \<in> prime ==> \<not> 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 \<in> prime ==> p dvd m * n ==> p dvd m \<or> 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
--- 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
--- 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";
--- 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<a; a<p |] \
-\ ==> #0 <= (inv p a) & (inv p a)<p & [a*(inv p a) = #1](mod p)";
-by (Asm_simp_tac 1);
-by (rtac (zcong_lineq_unique RS ex1_implies_ex RS someI_ex) 1);
-by (etac zless_zprime_imp_zrelprime 2);
-by (rewtac zprime_def);
-by Auto_tac;
-qed "inv_correct";
-
-bind_thm ("inv_ge",inv_correct RS conjunct1);
-bind_thm ("inv_less",(inv_correct RS conjunct2) RS conjunct1);
-bind_thm ("inv_is_inv",(inv_correct RS conjunct2) RS conjunct2);
-
-(* Same as WilsonRuss *)
-Goal "[| p:zprime; #1<a; a<p-#1 |] ==> (inv p a) ~= #0";
-by Safe_tac;
-by (cut_inst_tac [("a","a"),("p","p")] inv_is_inv 1);
-by (rewtac zcong_def);
-by Auto_tac;
-by (subgoal_tac "~p dvd #1" 1);
-by (rtac zdvd_not_zless 2);
-by (subgoal_tac "p dvd #1" 1);
-by (stac (zdvd_zminus_iff RS sym) 2);
-by Auto_tac;
-qed "inv_not_0";
-
-(* Same as WilsonRuss *)
-Goal "[| p:zprime; #1<a; a<p-#1 |] ==> (inv p a) ~= #1";
-by Safe_tac;
-by (cut_inst_tac [("a","a"),("p","p")] inv_is_inv 1);
-by (Asm_full_simp_tac 4);
-by (subgoal_tac "a = #1" 4);
-by (rtac zcong_zless_imp_eq 5);
-by Auto_tac;
-qed "inv_not_1";
-
-(* Same as WilsonRuss *)
-Goalw [zcong_def] "[a*(p-#1) = #1](mod p) = [a = p-#1](mod p)";
-by (simp_tac (simpset() addsimps [zdiff_zdiff_eq,zdiff_zdiff_eq2,
- zdiff_zmult_distrib2]) 1);
-by (res_inst_tac [("s","p dvd -((a+#1)+(p*(-a)))")] trans 1);
-by (simp_tac (simpset() addsimps [zmult_commute,zminus_zdiff_eq]) 1);
-by (stac zdvd_zminus_iff 1);
-by (stac zdvd_reduce 1);
-by (res_inst_tac [("s","p dvd (a+#1)+(p*(-#1))")] trans 1);
-by (stac zdvd_reduce 1);
-by Auto_tac;
-val lemma = result();
-
-(* Same as WilsonRuss *)
-Goal "[| p:zprime; #1<a; a<p-#1 |] ==> (inv p a) ~= p-#1";
-by Safe_tac;
-by (cut_inst_tac [("a","a"),("p","p")] inv_is_inv 1);
-by Auto_tac;
-by (asm_full_simp_tac (simpset() addsimps [lemma]) 1);
-by (subgoal_tac "a = p-#1" 1);
-by (rtac zcong_zless_imp_eq 2);
-by Auto_tac;
-qed "inv_not_p_minus_1";
-
-(* Below is slightly different as we don't expand
- inv but use 'correct'-theos *)
-Goal "[| p:zprime; #1<a; a<p-#1 |] ==> #1<(inv p a)";
-by (subgoal_tac "(inv p a) ~= #1" 1);
-by (subgoal_tac "(inv p a) ~= #0" 1);
-by (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<a; a<p-#1 |] ==> (inv p a)<p-#1";
-by (stac order_less_le 1);
-by (asm_full_simp_tac (simpset() addsimps [inv_not_p_minus_1, inv_less]) 1);
-qed "inv_less_p_minus_1";
-
-(************* Bijection *******************)
-
-Goal "#1<x ==> #0<=(x::int)";
-by Auto_tac;
-val l1 = result();
-
-Goal "#1<x ==> #0<(x::int)";
-by Auto_tac;
-val l2 = result();
-
-Goal "x<=p-#2 ==> x<(p::int)";
-by Auto_tac;
-val l3 = result();
-
-Goal "x<=p-#2 ==> x<(p::int)-#1";
-by Auto_tac;
-val l4 = result();
-
-Goalw [inj_on_def] "p : zprime ==> inj_on (inv p) (d22set (p-#2))";
-by Auto_tac;
-by (rtac zcong_zless_imp_eq 1);
-by (stac (zcong_cancel RS sym) 5);
-by (rtac zcong_trans 7);
-by (stac zcong_sym 8);
-by (etac inv_is_inv 7);
-by (Asm_simp_tac 9);
-by (etac inv_is_inv 9);
-by (rtac zless_zprime_imp_zrelprime 6);
-by (rtac inv_less 8);
-by (rtac (inv_g_1 RS l2) 7);
-by (rewtac zprime_def);
-by (auto_tac (claset() addIs [d22set_g_1,d22set_le,l1,l2,l3,l4],simpset()));
-qed "inv_inj";
-
-Goal "p : zprime ==> (inv p)`(d22set (p-#2)) = (d22set (p-#2))";
-by (rtac endo_inj_surj 1);
-by (rtac d22set_fin 1);
-by (etac inv_inj 2);
-by Auto_tac;
-by (rtac d22set_mem 1);
-by (etac inv_g_1 1);
-by (subgoal_tac "inv p xa < p - #1" 3);
-by (etac inv_less_p_minus_1 4);
-by (auto_tac (claset() addIs [d22set_g_1,d22set_le,l4],simpset()));
-qed "inv_d22set_d22set";
-
-Goalw [reciR_def] "p:zprime \
-\ ==> (d22set(p-#2),d22set(p-#2)) : (bijR (reciR p))";
-by (res_inst_tac [("s","(d22set(p-#2),(inv p)`(d22set(p-#2)))")] subst 1);
-by (asm_simp_tac (simpset() addsimps [inv_d22set_d22set]) 1);
-by (rtac inj_func_bijR 1);
-by (rtac d22set_fin 3);
-by (etac inv_inj 2);
-by Auto_tac;
-by (etac inv_is_inv 1);
-by (etac inv_g_1 5);
-by (etac inv_less_p_minus_1 7);
-by (auto_tac (claset() addIs [d22set_g_1,d22set_le,l2,l3,l4],simpset()));
-qed "d22set_d22set_bij";
-
-Goalw [reciR_def,bijP_def]
- "p:zprime ==> bijP (reciR p) (d22set(p-#2))";
-by Auto_tac;
-by (rtac d22set_mem 1);
-by Auto_tac;
-qed "reciP_bijP";
-
-Goalw [reciR_def,uniqP_def]
- "p:zprime ==> uniqP (reciR p)";
-by Auto_tac;
-by (rtac zcong_zless_imp_eq 1);
-by (stac (zcong_cancel2 RS sym) 5);
-by (rtac zcong_trans 7);
-by (stac zcong_sym 8);
-by (rtac zless_zprime_imp_zrelprime 6);
-by Auto_tac;
-by (rtac zcong_zless_imp_eq 1);
-by (stac (zcong_cancel RS sym) 5);
-by (rtac zcong_trans 7);
-by (stac zcong_sym 8);
-by (rtac zless_zprime_imp_zrelprime 6);
-by Auto_tac;
-qed "reciP_uniq";
-
-Goalw [reciR_def,symP_def]
- "p:zprime ==> symP (reciR p)";
-by (simp_tac (simpset() addsimps [zmult_commute]) 1);
-by Auto_tac;
-qed "reciP_sym";
-
-Goal "p:zprime ==> d22set(p-#2) : (bijER (reciR p))";
-by (rtac bijR_bijER 1);
-by (etac d22set_d22set_bij 1);
-by (etac reciP_bijP 1);
-by (etac reciP_uniq 1);
-by (etac reciP_sym 1);
-qed "bijER_d22set";
-
-(*********** Wilson **************)
-
-Goalw [reciR_def]
- "[| p:zprime; A : bijER (reciR p) |] ==> [setprod A = #1](mod p)";
-by (etac bijER.induct 1);
-by (subgoal_tac "a=#1 | a=p-#1" 2);
-by (rtac zcong_square_zless 3);
-by Auto_tac;
-by (stac setprod_insert 1);
-by (stac setprod_insert 3);
-by (auto_tac (claset(),simpset() addsimps [fin_bijER]));
-by (subgoal_tac "zcong ((a * b) * setprod A) (#1*#1) p" 1);
-by (asm_full_simp_tac (simpset() addsimps [zmult_assoc]) 1);
-by (rtac zcong_zmult 1);
-by Auto_tac;
-qed "bijER_zcong_prod_1";
-
-Goal "p:zprime ==> [zfact(p-#1) = #-1](mod p)";
-by (subgoal_tac "zcong ((p-#1)*zfact(p-#2)) (#-1*#1) p" 1);
-by (rtac zcong_zmult 2);
-by (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";
--- 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 ==
+ \<lambda>a b. zcong (a * b) #1 p \<and> #1 < a \<and> a < p - #1 \<and> #1 < b \<and> b < p - #1"
+ inv :: "int => int => int"
+ "inv p a ==
+ if p \<in> zprime \<and> #0 < a \<and> a < p then
+ (SOME x. #0 \<le> x \<and> x < p \<and> zcong (a * x) #1 p)
+ else #0"
+
+
+text {* \medskip Inverse *}
+
+lemma inv_correct:
+ "p \<in> zprime ==> #0 < a ==> a < p
+ ==> #0 \<le> inv p a \<and> inv p a < p \<and> [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 \<in> zprime ==> #1 < a ==> a < p - #1 ==> inv p a \<noteq> #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 "\<not> 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 \<in> zprime ==> #1 < a ==> a < p - #1 ==> inv p a \<noteq> #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 \<in> zprime ==> #1 < a ==> a < p - #1 ==> inv p a \<noteq> 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 \<in> zprime ==> #1 < a ==> a < p - #1 ==> #1 < inv p a"
+ apply (subgoal_tac "inv p a \<noteq> #1")
+ apply (subgoal_tac "inv p a \<noteq> #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 \<in> 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 \<le> (x::int)"
+ apply auto
+ done
-defs
- reciR_def "reciR p == (%a b. zcong (a*b) #1 p &
- #1<a & a<p-#1 & #1<b & b<p-#1)"
- inv_def "inv p a == (if p:zprime & #0<a & a<p then
- (@x. #0<=x & x<p & zcong (a*x) #1 p)
- else #0)"
+lemma aux2: "#1 < x ==> #0 < (x::int)"
+ apply auto
+ done
+
+lemma aux3: "x \<le> p - #2 ==> x < (p::int)"
+ apply auto
+ done
+
+lemma aux4: "x \<le> p - #2 ==> x < (p::int)-#1"
+ apply auto
+ done
+
+lemma inv_inj: "p \<in> 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 \<in> 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 \<in> zprime ==> (d22set (p - #2), d22set (p - #2)) \<in> 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 \<in> 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 \<in> 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 \<in> zprime ==> symP (reciR p)"
+ apply (unfold reciR_def symP_def)
+ apply (simp add: zmult_commute)
+ apply auto
+ done
+
+lemma bijER_d22set: "p \<in> zprime ==> d22set (p - #2) \<in> 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 \<in> zprime ==> A \<in> bijER (reciR p) ==> [setprod A = #1] (mod p)"
+ apply (unfold reciR_def)
+ apply (erule bijER.induct)
+ apply (subgoal_tac [2] "a = #1 \<or> 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 \<in> 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
--- 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<m ==> Suc(nat(m-#2)) = nat(m-#1)";
-by (stac (int_int_eq RS sym) 1);
-by Auto_tac;
-val lemma = result();
-
-Goalw [inv_def]
- "[| p:zprime; #0<a; a<p |] ==> [a*(inv p a) = #1] (mod p)";
-by (stac zcong_zmod 1);
-by (stac (zmod_zmult1_eq RS sym) 1);
-by (stac (zcong_zmod RS sym) 1);
-by (stac (power_Suc RS sym) 1);
-by (stac lemma 1);
-by (etac Little_Fermat 2);
-by (etac zdvd_not_zless 2);
-by (rewtac zprime_def);
-by Auto_tac;
-qed "inv_is_inv";
-
-Goal "[| p:zprime; #1<a; a<p-#1 |] ==> a ~= (inv p a)";
-by Safe_tac;
-by (cut_inst_tac [("a","a"),("p","p")] zcong_square 1);
-by (cut_inst_tac [("a","a"),("p","p")] inv_is_inv 3);
-by Auto_tac;
-by (subgoal_tac "a=#1" 1);
-by (res_inst_tac [("m","p")] zcong_zless_imp_eq 2);
-by (subgoal_tac "a=p-#1" 7);
-by (res_inst_tac [("m","p")] zcong_zless_imp_eq 8);
-by Auto_tac;
-qed "inv_distinct";
-
-Goal "[| p:zprime; #1<a; a<p-#1 |] ==> (inv p a) ~= #0";
-by Safe_tac;
-by (cut_inst_tac [("a","a"),("p","p")] inv_is_inv 1);
-by (rewtac zcong_def);
-by Auto_tac;
-by (subgoal_tac "~p dvd #1" 1);
-by (rtac zdvd_not_zless 2);
-by (subgoal_tac "p dvd #1" 1);
-by (stac (zdvd_zminus_iff RS sym) 2);
-by Auto_tac;
-qed "inv_not_0";
-
-Goal "[| p:zprime; #1<a; a<p-#1 |] ==> (inv p a) ~= #1";
-by Safe_tac;
-by (cut_inst_tac [("a","a"),("p","p")] inv_is_inv 1);
-by (Asm_full_simp_tac 4);
-by (subgoal_tac "a = #1" 4);
-by (rtac zcong_zless_imp_eq 5);
-by Auto_tac;
-qed "inv_not_1";
-
-Goalw [zcong_def] "[a*(p-#1) = #1](mod p) = [a = p-#1](mod p)";
-by (simp_tac (simpset() addsimps [zdiff_zdiff_eq,zdiff_zdiff_eq2,
- zdiff_zmult_distrib2]) 1);
-by (res_inst_tac [("s","p dvd -((a+#1)+(p*(-a)))")] trans 1);
-by (simp_tac (simpset() addsimps [zmult_commute,zminus_zdiff_eq]) 1);
-by (stac zdvd_zminus_iff 1);
-by (stac zdvd_reduce 1);
-by (res_inst_tac [("s","p dvd (a+#1)+(p*(-#1))")] trans 1);
-by (stac zdvd_reduce 1);
-by Auto_tac;
-val lemma = result();
-
-Goal "[| p:zprime; #1<a; a<p-#1 |] ==> (inv p a) ~= p-#1";
-by Safe_tac;
-by (cut_inst_tac [("a","a"),("p","p")] inv_is_inv 1);
-by Auto_tac;
-by (asm_full_simp_tac (simpset() addsimps [lemma]) 1);
-by (subgoal_tac "a = p-#1" 1);
-by (rtac zcong_zless_imp_eq 2);
-by Auto_tac;
-qed "inv_not_p_minus_1";
-
-Goal "[| p:zprime; #1<a; a<p-#1 |] ==> #1<(inv p a)";
-by (case_tac "#0<=(inv p a)" 1);
-by (subgoal_tac "(inv p a) ~= #1" 1);
-by (subgoal_tac "(inv p a) ~= #0" 1);
-by (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<a; a<p-#1 |] ==> (inv p a)<p-#1";
-by (case_tac "(inv p a)<p" 1);
-by (stac order_less_le 1);
-by (asm_full_simp_tac (simpset() addsimps [inv_not_p_minus_1]) 1);
-by Auto_tac;
-by (rewrite_goals_tac [inv_def,zprime_def]);
-by (asm_full_simp_tac (simpset() addsimps [pos_mod_bound]) 1);
-qed "inv_less_p_minus_1";
-
-Goal "#5<=p ==> nat(p-#2)*nat(p-#2) = Suc(nat(p-#1)*nat(p-#3))";
-by (stac (int_int_eq RS sym) 1);
-by (asm_simp_tac (simpset() addsimps [zmult_int RS sym]) 1);
-by (simp_tac (simpset() addsimps [zdiff_zmult_distrib,
- zdiff_zmult_distrib2]) 1);
-val lemma = result();
-
-Goal "[x^y = #1](mod p) --> [x^(y*z) = #1](mod p)";
-by (induct_tac "z" 1);
-by (auto_tac (claset(),simpset() addsimps [zpower_zadd_distrib]));
-by (subgoal_tac "zcong (x^y * x^(y*n)) (#1*#1) p" 1);
-by (rtac zcong_zmult 2);
-by (ALLGOALS Asm_full_simp_tac);
-qed_spec_mp "zcong_zpower_zmult";
-
-Goalw [inv_def] "[| p:zprime; #5<=p; #0<a; a<p |] ==> (inv p (inv p a)) = a";
-by (stac zpower_zmod 1);
-by (stac zpower_zpower 1);
-by (rtac zcong_zless_imp_eq 1);
-by (stac zcong_zmod 5);
-by (stac mod_mod_trivial 5);
-by (stac (zcong_zmod RS sym) 5);
-by (stac lemma 5);
-by (subgoal_tac "zcong (a * a^(nat (p - #1) * nat (p - #3))) (a*#1) p" 6);
-by (rtac zcong_zmult 7);
-by (rtac zcong_zpower_zmult 8);
-by (etac Little_Fermat 8);
-by (rtac zdvd_not_zless 8);
-by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [pos_mod_bound,
- pos_mod_sign])));
-qed "inv_inv";
-
-
-(************* wset *************)
-
-val [wset_eq] = wset.simps;
-Delsimps wset.simps;
-
-val [prem1,prem2] =
-Goal "[| !!a p. P {} a p; \
-\ !!a p. [| #1<(a::int); P (wset (a-#1,p)) (a-#1) p |] \
-\ ==> P (wset (a,p)) a p|] \
-\ ==> P (wset (u,v)) u v";
-by (rtac wset.induct 1);
-by Safe_tac;
-by (case_tac "#1<a" 2);
-by (rtac prem2 2);
-by (ALLGOALS Asm_simp_tac);
-by (ALLGOALS (asm_simp_tac (simpset() addsimps [wset_eq,prem1])));
-qed "wset_induct";
-
-Goal "[| #1<a; b~:(wset (a-#1,p)) |] \
-\ ==> b:(wset (a,p)) --> b=a | b = inv p a";
-by (stac wset_eq 1);
-by (rewtac Let_def);
-by (Asm_simp_tac 1);
-qed_spec_mp "wset_mem_imp_or";
-
-Goal "#1<a ==> a:(wset(a,p))";
-by (stac wset_eq 1);
-by (rewtac Let_def);
-by (Asm_simp_tac 1);
-qed "wset_mem_mem";
-Addsimps [wset_mem_mem];
-
-Goal "[| #1<a; b:wset(a-#1,p) |] ==> b:wset(a,p)";
-by (stac wset_eq 1);
-by (rewtac Let_def);
-by Auto_tac;
-qed "wset_subset";
-
-Goal "p:zprime --> a<p-#1 --> b:(wset(a,p)) --> #1<b";
-by (induct_thm_tac wset_induct "a p" 1);
-by Auto_tac;
-by (case_tac "b=a" 1);
-by (case_tac "b=inv p a" 2);
-by (subgoal_tac "b=a | b = inv p a" 3);
-by (rtac wset_mem_imp_or 4);
-by (Asm_simp_tac 2);
-by (rtac inv_g_1 2);
-by Auto_tac;
-qed_spec_mp "wset_g_1";
-
-Goal "p:zprime --> a<p-#1 --> b:(wset(a,p)) --> b<p-#1";
-by (induct_thm_tac wset_induct "a p" 1);
-by Auto_tac;
-by (case_tac "b=a" 1);
-by (case_tac "b=inv p a" 2);
-by (subgoal_tac "b=a | b = inv p a" 3);
-by (rtac wset_mem_imp_or 4);
-by (Asm_simp_tac 2);
-by (rtac inv_less_p_minus_1 2);
-by Auto_tac;
-qed_spec_mp "wset_less";
-
-Goal "p:zprime --> a<p-#1 --> #1<b --> b<=a --> b:(wset(a,p))";
-by (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<p-#1 --> 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<p-#1; #1<b; b<p-#1; (inv p b):(wset (a,p)) |] \
-\ ==> b:(wset (a,p))";
-by (res_inst_tac [("s","inv p (inv p b)"),("t","b")] subst 1);
-by (rtac wset_mem_inv_mem 2);
-by (rtac inv_inv 1);
-by (ALLGOALS (Asm_simp_tac));
-qed "wset_inv_mem_mem";
-
-Goal "finite (wset (a,p))";
-by (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<p-#1 --> [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";
--- 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 ((\<lambda>(a, p). nat a) :: int * int => nat)"
+ "wset (a, p) =
+ (if #1 < a then
+ let ws = wset (a - #1, p)
+ in (if a \<in> 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 \<in> zprime \<Longrightarrow> #0 < a \<Longrightarrow> 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 \<in> zprime \<Longrightarrow> #1 < a \<Longrightarrow> a < p - #1 ==> a \<noteq> 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 \<in> zprime \<Longrightarrow> #1 < a \<Longrightarrow> a < p - #1 ==> inv p a \<noteq> #0"
+ apply safe
+ apply (cut_tac a = a and p = p in inv_is_inv)
+ apply (unfold zcong_def)
+ apply auto
+ apply (subgoal_tac "\<not> 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 \<in> zprime \<Longrightarrow> #1 < a \<Longrightarrow> a < p - #1 ==> inv p a \<noteq> #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 \<in> zprime \<Longrightarrow> #1 < a \<Longrightarrow> a < p - #1 ==> inv p a \<noteq> 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 \<in> zprime \<Longrightarrow> #1 < a \<Longrightarrow> a < p - #1 ==> #1 < inv p a"
+ apply (case_tac "#0\<le> inv p a")
+ apply (subgoal_tac "inv p a \<noteq> #1")
+ apply (subgoal_tac "inv p a \<noteq> #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 \<in> zprime \<Longrightarrow> #1 < a \<Longrightarrow> 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 \<le> 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) \<Longrightarrow> [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 \<in> zprime \<Longrightarrow>
+ #5 \<le> p \<Longrightarrow> #0 < a \<Longrightarrow> 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 then let ws = wset (a-#1,p) in
- (if a:ws then ws else insert a (insert (inv p a) ws))
- else {})"
+lemma wset_induct:
+ "(!!a p. P {} a p) \<Longrightarrow>
+ (!!a p. #1 < (a::int) \<Longrightarrow> 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 \<Longrightarrow> b \<notin> wset (a - #1, p)
+ ==> b \<in> wset (a, p) --> b = a \<or> b = inv p a"
+ apply (subst wset.simps)
+ apply (unfold Let_def)
+ apply simp
+ done
+
+lemma wset_mem_mem [simp]: "#1 < a ==> a \<in> wset (a, p)"
+ apply (subst wset.simps)
+ apply (unfold Let_def)
+ apply simp
+ done
+
+lemma wset_subset: "#1 < a \<Longrightarrow> b \<in> wset (a - #1, p) ==> b \<in> wset (a, p)"
+ apply (subst wset.simps)
+ apply (unfold Let_def)
+ apply auto
+ done
+
+lemma wset_g_1 [rule_format]:
+ "p \<in> zprime --> a < p - #1 --> b \<in> 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 \<or> 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 \<in> zprime --> a < p - #1 --> b \<in> 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 \<or> 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 \<in> zprime -->
+ a < p - #1 --> #1 < b --> b \<le> a --> b \<in> 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 \<in> zprime --> #5 \<le> p --> a < p - #1 --> b \<in> wset (a, p)
+ --> inv p b \<in> 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 \<or> b = inv p a")
+ apply (rule_tac [7] wset_mem_imp_or)
+ apply auto
+ done
+
+lemma wset_inv_mem_mem:
+ "p \<in> zprime \<Longrightarrow> #5 \<le> p \<Longrightarrow> a < p - #1 \<Longrightarrow> #1 < b \<Longrightarrow> b < p - #1
+ \<Longrightarrow> inv p b \<in> wset (a, p) \<Longrightarrow> b \<in> 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 \<in> zprime -->
+ #5 \<le> 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 \<in> 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 \<in> 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 \<in> zprime \<Longrightarrow> p \<noteq> #2 \<Longrightarrow> p \<noteq> #3 ==> #5 \<le> 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 \<in> 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 \<le> 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