new GroupTheory example, e.g. the Sylow theorem (preliminary version)
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/GroupTheory/Exponent.ML Sun Jun 10 08:03:35 2001 +0200
@@ -0,0 +1,495 @@
+(* Title: HOL/GroupTheory/Exponent
+ ID: $Id$
+ Author: Florian Kammueller, with new proofs by L C Paulson
+ Copyright 2001 University of Cambridge
+*)
+
+(*??Two more for Divides.ML *)
+Goal "0<m ==> (m*n dvd m) = (n=1)";
+by Auto_tac;
+by (subgoal_tac "m*n dvd m*1" 1);
+by (dtac dvd_mult_cancel 1);
+by Auto_tac;
+qed "dvd_mult_cancel1";
+
+Goal "0<m ==> (n*m dvd m) = (n=1)";
+by (stac mult_commute 1);
+by (etac dvd_mult_cancel1 1);
+qed "dvd_mult_cancel2";
+
+
+(*** prime theorems ***)
+
+val prime_def = thm "prime_def";
+
+Goalw [prime_def] "p\\<in>prime ==> 1 < p";
+by (Blast_tac 1);
+qed "prime_imp_one_less";
+
+Goal "(p\\<in>prime) = (1<p & (\\<forall>a b. p dvd a*b --> (p dvd a) | (p dvd b)))";
+by (auto_tac (claset(), simpset() addsimps [prime_imp_one_less]));
+by (blast_tac (claset() addSDs [thm "prime_dvd_mult"]) 1);
+by (auto_tac (claset(), simpset() addsimps [prime_def]));
+by (etac dvdE 1);
+by (case_tac "k=0" 1);
+by (Asm_full_simp_tac 1);
+by (dres_inst_tac [("x","m")] spec 1);
+by (dres_inst_tac [("x","k")] spec 1);
+by (asm_full_simp_tac
+ (simpset() addsimps [dvd_mult_cancel1, dvd_mult_cancel2]) 1);
+qed "prime_iff";
+
+Goal "p\\<in>prime ==> 0 < p^a";
+by (rtac zero_less_power 1);
+by (force_tac (claset(), simpset() addsimps [prime_iff]) 1);
+qed "zero_less_prime_power";
+
+
+(*First some things about HOL and sets *)
+val [p1] = goal (the_context()) "(P x y) ==> ( (x, y)\\<in>{(a,b). P a b})";
+by (rtac CollectI 1);
+by (rewrite_goals_tac [split RS eq_reflection]);
+by (rtac p1 1);
+qed "CollectI_prod";
+
+val [p1] = goal (the_context()) "( (x, y)\\<in>{(a,b). P a b}) ==> (P x y)";
+by (res_inst_tac [("c1","P")] (split RS subst) 1);
+by (res_inst_tac [("a","(x,y)")] CollectD 1);
+by (rtac p1 1);
+qed "CollectD_prod";
+
+val [p1] = goal (the_context()) "(P x y z v) ==> ( (x, y, z, v)\\<in>{(a,b,c,d). P a b c d})";
+by (rtac CollectI_prod 1);
+by (rewrite_goals_tac [split RS eq_reflection]);
+by (rtac p1 1);
+qed "CollectI_prod4";
+
+Goal "( (x, y, z, v)\\<in>{(a,b,c,d). P a b c d}) ==> (P x y z v)";
+by Auto_tac;
+qed "CollectD_prod4";
+
+
+
+val [p1] = goal (the_context()) "x\\<in>{y. P(y) & Q(y)} ==> P(x)";
+by (res_inst_tac [("Q","Q x"),("P", "P x")] conjE 1);
+by (assume_tac 2);
+by (res_inst_tac [("a", "x")] CollectD 1);
+by (rtac p1 1);
+qed "subset_lemma1";
+
+val [p1,p2] = goal (the_context()) "[|P == Q; P|] ==> Q";
+by (fold_goals_tac [p1]);
+by (rtac p2 1);
+qed "apply_def";
+
+Goal "S \\<noteq> {} ==> \\<exists>x. x\\<in>S";
+by Auto_tac;
+qed "NotEmpty_ExEl";
+
+Goal "\\<exists>x. x: S ==> S \\<noteq> {}";
+by Auto_tac;
+qed "ExEl_NotEmpty";
+
+
+(* The following lemmas are needed for existsM1inM *)
+
+Goal "[| {} \\<notin> A; M\\<in>A |] ==> M \\<noteq> {}";
+by Auto_tac;
+qed "MnotEqempty";
+
+val [p1] = goal (the_context()) "\\<exists>g \\<in> A. x = P(g) ==> \\<exists>g \\<in> A. P(g) = x";
+by (rtac bexE 1);
+by (rtac p1 1);
+by (rtac bexI 1);
+by (rtac sym 1);
+by (assume_tac 1);
+by (assume_tac 1);
+qed "bex_sym";
+
+Goalw [equiv_def,quotient_def,sym_def,trans_def]
+ "[| equiv A r; C\\<in>A // r |] ==> \\<forall>x \\<in> C. \\<forall>y \\<in> C. (x,y)\\<in>r";
+by (Blast_tac 1);
+qed "ElemClassEquiv";
+
+Goalw [equiv_def,quotient_def,sym_def,trans_def]
+ "[|equiv A r; M\\<in>A // r; M1\\<in>M; (M1, M2)\\<in>r |] ==> M2\\<in>M";
+by (Blast_tac 1);
+qed "EquivElemClass";
+
+Goal "[| 0 < c; a <= b |] ==> a <= b * (c::nat)";
+by (res_inst_tac [("P","%x. x <= b * c")] subst 1);
+by (rtac mult_1_right 1);
+by (rtac mult_le_mono 1);
+by (assume_tac 1);
+by (stac Suc_le_eq 1);
+by (assume_tac 1);
+qed "le_extend_mult";
+
+
+(* card_inj lemma: F. Kammueller, 4.9. 96
+
+The sequel contains a proof of the lemma "card_inj" used in the
+plus preparations. The provable form here differs from the
+one used in Group in that it contains the additional neccessary assumptions
+"finite A" and "finite B" *)
+
+Goal "0 < card(S) ==> S \\<noteq> {}";
+by (force_tac (claset(), simpset() addsimps [card_empty]) 1);
+qed "card_nonempty";
+
+Goal "[| finite(A); finite(B); f \\<in> A -> B; inj_on f A |] ==> card A <= card B";
+bw funcset_def;
+by (rtac card_inj_on_le 1);
+by (assume_tac 4);
+by Auto_tac;
+qed "card_inj";
+
+Goal "[| x \\<notin> F; \
+\ \\<forall>c1\\<in>insert x F. \\<forall>c2 \\<in> insert x F. c1 \\<noteq> c2 --> c1 \\<inter> c2 = {}|]\
+\ ==> x \\<inter> \\<Union> F = {}";
+by Auto_tac;
+qed "insert_partition";
+
+(* main cardinality theorem *)
+Goal "finite C ==> \
+\ finite (\\<Union> C) --> \
+\ (\\<forall>c\\<in>C. card c = k) --> \
+\ (\\<forall>c1 \\<in> C. \\<forall>c2 \\<in> C. c1 \\<noteq> c2 --> c1 \\<inter> c2 = {}) --> \
+\ k * card(C) = card (\\<Union> C)";
+by (etac finite_induct 1);
+by (Asm_full_simp_tac 1);
+by (asm_full_simp_tac
+ (simpset() addsimps [card_insert_disjoint, card_Un_disjoint,
+ insert_partition, inst "B" "\\<Union>(insert x F)" finite_subset]) 1);
+qed_spec_mp "card_partition";
+
+Goal "[| finite S; S \\<noteq> {} |] ==> 0 < card(S)";
+by (swap_res_tac [card_0_eq RS iffD1] 1);
+by Auto_tac;
+qed "zero_less_card_empty";
+
+
+Goal "[| p*k dvd m*n; p\\<in>prime |] \
+\ ==> (\\<exists>x. k dvd x*n & m = p*x) | (\\<exists>y. k dvd m*y & n = p*y)";
+by (asm_full_simp_tac (simpset() addsimps [prime_iff]) 1);
+by (ftac dvd_mult_left 1);
+by (subgoal_tac "p dvd m | p dvd n" 1);
+by (Blast_tac 2);
+by (etac disjE 1);
+by (rtac disjI1 1);
+by (rtac disjI2 2);
+by (eres_inst_tac [("n","m")] dvdE 1);
+by (eres_inst_tac [("n","n")] dvdE 2);
+by Auto_tac;
+by (res_inst_tac [("k","p")] dvd_mult_cancel 2);
+by (res_inst_tac [("k","p")] dvd_mult_cancel 1);
+by (ALLGOALS (asm_full_simp_tac (simpset() addsimps mult_ac)));
+qed "prime_dvd_cases";
+
+
+Goal "p\\<in>prime \
+\ ==> \\<forall>m n. p^c dvd m*n --> \
+\ (\\<forall>a b. a+b = Suc c --> p^a dvd m | p^b dvd n)";
+by (induct_tac "c" 1);
+ by (Clarify_tac 1);
+ by (case_tac "a" 1);
+ by (Asm_full_simp_tac 1);
+ by (Asm_full_simp_tac 1);
+(*inductive step*)
+by (Asm_full_simp_tac 1);
+by (Clarify_tac 1);
+by (etac (prime_dvd_cases RS disjE) 1);
+by (assume_tac 1);
+by Auto_tac;
+(*case 1: p dvd m*)
+ by (case_tac "a" 1);
+ by (Asm_full_simp_tac 1);
+ by (Clarify_tac 1);
+ by (dtac spec 1 THEN dtac spec 1 THEN mp_tac 1);
+ by (dres_inst_tac [("x","nat")] spec 1);
+ by (dres_inst_tac [("x","b")] spec 1);
+ by (Asm_full_simp_tac 1);
+ by (blast_tac (claset() addIs [dvd_refl, mult_dvd_mono]) 1);
+(*case 2: p dvd n*)
+by (case_tac "b" 1);
+ by (Asm_full_simp_tac 1);
+by (Clarify_tac 1);
+by (dtac spec 1 THEN dtac spec 1 THEN mp_tac 1);
+by (dres_inst_tac [("x","a")] spec 1);
+by (dres_inst_tac [("x","nat")] spec 1);
+by (Asm_full_simp_tac 1);
+by (blast_tac (claset() addIs [dvd_refl, mult_dvd_mono]) 1);
+qed_spec_mp "prime_power_dvd_cases";
+
+(*needed in this form in Sylow.ML*)
+Goal "[| p\\<in>prime; ~(p ^ (r+1) dvd n); p ^ (a+r) dvd n * k |] \
+\ ==> p ^ a dvd k";
+by (dres_inst_tac [("a","r+1"), ("b","a")] prime_power_dvd_cases 1);
+by (assume_tac 1);
+by Auto_tac;
+qed "div_combine";
+
+(*Lemma for power_dvd_bound*)
+Goal "1 < p ==> Suc n <= p^n";
+by (induct_tac "n" 1);
+by (Asm_simp_tac 1);
+by (Asm_full_simp_tac 1);
+by (subgoal_tac "2*n + #2 <= p * p^n" 1);
+by (Asm_full_simp_tac 1);
+by (subgoal_tac "#2 * p^n <= p * p^n" 1);
+(*?arith_tac should handle all of this!*)
+by (rtac order_trans 1);
+by (assume_tac 2);
+by (dres_inst_tac [("k","#2")] mult_le_mono2 1);
+by (Asm_full_simp_tac 1);
+by (rtac mult_le_mono1 1);
+by (Asm_full_simp_tac 1);
+qed "Suc_le_power";
+
+(*An upper bound for the n such that p^n dvd a: needed for GREATEST to exist*)
+Goal "[|p^n dvd a; 1 < p; 0 < a|] ==> n < a";
+by (dtac dvd_imp_le 1);
+by (dres_inst_tac [("n","n")] Suc_le_power 2);
+by Auto_tac;
+qed "power_dvd_bound";
+
+
+(*** exponent theorems ***)
+
+Goal "[|p^k dvd n; p\\<in>prime; 0<n|] ==> k <= exponent p n";
+by (asm_full_simp_tac (simpset() addsimps [exponent_def]) 1);
+by (etac GreatestM_nat_le 1);
+by (blast_tac (claset() addDs [prime_imp_one_less, power_dvd_bound]) 1);
+qed_spec_mp "exponent_ge";
+
+Goal "0<s ==> (p ^ exponent p s) dvd s";
+by (simp_tac (simpset() addsimps [exponent_def]) 1);
+by (Clarify_tac 1);
+by (res_inst_tac [("k","0")] GreatestI 1);
+by (blast_tac (claset() addDs [prime_imp_one_less, power_dvd_bound]) 2);
+by (Asm_full_simp_tac 1);
+qed "power_exponent_dvd";
+
+Goal "[|(p * p ^ exponent p s) dvd s; p\\<in>prime |] ==> s=0";
+by (subgoal_tac "p ^ Suc(exponent p s) dvd s" 1);
+by (Asm_full_simp_tac 2);
+by (rtac ccontr 1);
+by (dtac exponent_ge 1);
+by Auto_tac;
+qed "power_Suc_exponent_Not_dvd";
+
+Goal "p\\<in>prime ==> exponent p (p^a) = a";
+by (asm_simp_tac (simpset() addsimps [exponent_def]) 1);
+by (rtac Greatest_equality 1);
+by (Asm_full_simp_tac 1);
+by (blast_tac (claset() addIs [prime_imp_one_less, power_dvd_imp_le]) 1);
+qed "exponent_power_eq";
+Addsimps [exponent_power_eq];
+
+Goal "!r::nat. (p^r dvd a) = (p^r dvd b) ==> exponent p a = exponent p b";
+by (asm_simp_tac (simpset() addsimps [exponent_def]) 1);
+qed "exponent_equalityI";
+
+Goal "p \\<notin> prime ==> exponent p s = 0";
+by (asm_simp_tac (simpset() addsimps [exponent_def]) 1);
+qed "exponent_eq_0";
+Addsimps [exponent_eq_0];
+
+
+(* exponent_mult_add, easy inclusion. Could weaken p\\<in>prime to 1<p *)
+Goal "[| 0 < a; 0 < b |] \
+\ ==> (exponent p a) + (exponent p b) <= exponent p (a * b)";
+by (case_tac "p \\<in> prime" 1);
+by (rtac exponent_ge 1);
+by (auto_tac (claset(), simpset() addsimps [power_add]));
+by (blast_tac (claset() addIs [prime_imp_one_less, power_exponent_dvd,
+ mult_dvd_mono]) 1);
+qed "exponent_mult_add1";
+
+(* exponent_mult_add, opposite inclusion *)
+Goal "[| 0 < a; 0 < b |] \
+\ ==> exponent p (a * b) <= (exponent p a) + (exponent p b)";
+by (case_tac "p\\<in>prime" 1);
+by (rtac leI 1);
+by (Clarify_tac 1);
+by (cut_inst_tac [("p","p"),("s","a*b")] power_exponent_dvd 1);
+by Auto_tac;
+by (subgoal_tac "p ^ (Suc (exponent p a + exponent p b)) dvd a * b" 1);
+by (rtac (le_imp_power_dvd RS dvd_trans) 2);
+ by (assume_tac 3);
+ by (Asm_full_simp_tac 2);
+by (forw_inst_tac [("a","Suc (exponent p a)"), ("b","Suc (exponent p b)")]
+ prime_power_dvd_cases 1);
+ by (assume_tac 1 THEN Force_tac 1);
+by (Asm_full_simp_tac 1);
+by (blast_tac (claset() addDs [power_Suc_exponent_Not_dvd]) 1);
+qed "exponent_mult_add2";
+
+Goal "[| 0 < a; 0 < b |] \
+\ ==> exponent p (a * b) = (exponent p a) + (exponent p b)";
+by (blast_tac (claset() addIs [exponent_mult_add1, exponent_mult_add2,
+ order_antisym]) 1);
+qed "exponent_mult_add";
+
+
+Goal "~ (p dvd n) ==> exponent p n = 0";
+by (case_tac "exponent p n" 1);
+by (Asm_full_simp_tac 1);
+by (case_tac "n" 1);
+by (Asm_full_simp_tac 1);
+by (cut_inst_tac [("s","n"),("p","p")] power_exponent_dvd 1);
+by (auto_tac (claset() addDs [dvd_mult_left], simpset()));
+qed "not_divides_exponent_0";
+
+Goal "exponent p 1 = 0";
+by (case_tac "p \\<in> prime" 1);
+by (auto_tac (claset(),
+ simpset() addsimps [prime_iff, not_divides_exponent_0]));
+qed "exponent_1_eq_0";
+Addsimps [exponent_1_eq_0];
+
+
+(*** Lemmas for the main combinatorial argument ***)
+
+Goal "[| 0 < (m::nat); 0<k; k < p^a; (p^r) dvd (p^a)* m - k |] ==> r <= a";
+by (rtac notnotD 1);
+by (rtac notI 1);
+by (dtac (leI RSN (2, contrapos_nn) RS notnotD) 1);
+by (assume_tac 1);
+by (dres_inst_tac [("m","a")] less_imp_le 1);
+by (dtac le_imp_power_dvd 1);
+by (dres_inst_tac [("n","p ^ r")] dvd_trans 1);
+by (assume_tac 1);
+by (forw_inst_tac [("m","k")] less_imp_le 1);
+by (dres_inst_tac [("c","m")] le_extend_mult 1);
+by (assume_tac 1);
+by (dres_inst_tac [("k","p ^ a"),("m","(p ^ a) * m")] dvd_diffD1 1);
+by (assume_tac 2);
+by (rtac (dvd_refl RS dvd_mult2) 1);
+by (dres_inst_tac [("n","k")] dvd_imp_le 1);
+by Auto_tac;
+qed "p_fac_forw_lemma";
+
+Goal "[| 0 < (m::nat); 0<k; k < p^a; (p^r) dvd (p^a)* m - k |] \
+\ ==> (p^r) dvd (p^a) - k";
+by (forw_inst_tac [("k1","k"),("i","p")]
+ (p_fac_forw_lemma RS le_imp_power_dvd) 1);
+by Auto_tac;
+by (subgoal_tac "p^r dvd p^a*m" 1);
+ by (blast_tac (claset() addIs [dvd_mult2]) 2);
+by (dtac dvd_diffD1 1);
+ by (assume_tac 1);
+ by (blast_tac (claset() addIs [dvd_diff]) 2);
+by (dtac less_imp_Suc_add 1);
+by Auto_tac;
+qed "p_fac_forw";
+
+
+Goal "[| 0 < (k::nat); k < p^a; 0 < p; (p^r) dvd (p^a) - k |] ==> r <= a";
+by (res_inst_tac [("m","1")] p_fac_forw_lemma 1);
+by Auto_tac;
+qed "r_le_a_forw";
+
+Goal "[| 0<m; 0<k; 0 < (p::nat); k < p^a; (p^r) dvd p^a - k |] \
+\ ==> (p^r) dvd (p^a)*m - k";
+by (forw_inst_tac [("k1","k"),("i","p")] (r_le_a_forw RS le_imp_power_dvd) 1);
+by Auto_tac;
+by (subgoal_tac "p^r dvd p^a*m" 1);
+ by (blast_tac (claset() addIs [dvd_mult2]) 2);
+by (dtac dvd_diffD1 1);
+ by (assume_tac 1);
+ by (blast_tac (claset() addIs [dvd_diff]) 2);
+by (dtac less_imp_Suc_add 1);
+by Auto_tac;
+qed "p_fac_backw";
+
+Goal "[| 0<m; 0<k; 0 < (p::nat); k < p^a |] \
+\ ==> exponent p (p^a * m - k) = exponent p (p^a - k)";
+by (blast_tac (claset() addIs [exponent_equalityI, p_fac_forw,
+ p_fac_backw]) 1);
+qed "exponent_p_a_m_k_equation";
+
+(*Suc rules that we have to delete from the simpset*)
+val bad_Sucs = [binomial_Suc_Suc, mult_Suc, mult_Suc_right];
+
+(*The bound K is needed; otherwise it's too weak to be used.*)
+Goal "[| \\<forall>i. Suc i < K --> exponent p (Suc i) = exponent p (Suc(j+i))|] \
+\ ==> k<K --> exponent p ((j+k) choose k) = 0";
+by (case_tac "p \\<in> prime" 1);
+by (Asm_simp_tac 2);
+by (induct_tac "k" 1);
+by (Simp_tac 1);
+(*induction step*)
+by (subgoal_tac "0 < (Suc(j+n) choose Suc n)" 1);
+ by (simp_tac (simpset() addsimps [zero_less_binomial_iff]) 2);
+by (Clarify_tac 1);
+by (subgoal_tac
+ "exponent p ((Suc(j+n) choose Suc n) * Suc n) = exponent p (Suc n)" 1);
+(*First, use the assumed equation. We simplify the LHS to
+ exponent p (Suc (j + n) choose Suc n) + exponent p (Suc n);
+ the common terms cancel, proving the conclusion.*)
+ by (asm_full_simp_tac (simpset() delsimps bad_Sucs
+ addsimps [exponent_mult_add]) 1);
+(*Establishing the equation requires first applying Suc_times_binomial_eq...*)
+by (asm_full_simp_tac (simpset() delsimps bad_Sucs
+ addsimps [Suc_times_binomial_eq RS sym]) 1);
+(*...then exponent_mult_add and the quantified premise.*)
+by (asm_full_simp_tac (simpset() delsimps bad_Sucs
+ addsimps [zero_less_binomial_iff, exponent_mult_add]) 1);
+qed_spec_mp "p_not_div_choose_lemma";
+
+(*The lemma above, with two changes of variables*)
+Goal "[| k<K; k<=n; \
+\ \\<forall>j. 0<j & j<K --> exponent p (n - k + (K - j)) = exponent p (K - j)|] \
+\ ==> exponent p (n choose k) = 0";
+by (cut_inst_tac [("j","n-k"),("k","k"),("p","p")] p_not_div_choose_lemma 1);
+by (assume_tac 2);
+by (Asm_full_simp_tac 2);
+by (Clarify_tac 1);
+by (dres_inst_tac [("x","K - Suc i")] spec 1);
+by (asm_full_simp_tac (simpset() addsimps [Suc_diff_le]) 1);
+qed "p_not_div_choose";
+
+
+Goal "0 < m ==> exponent p ((p^a * m - 1) choose (p^a - 1)) = 0";
+by (case_tac "p \\<in> prime" 1);
+by (Asm_simp_tac 2);
+by (forw_inst_tac [("a","a")] zero_less_prime_power 1);
+by (res_inst_tac [("K","p^a")] p_not_div_choose 1);
+ by (Asm_full_simp_tac 1);
+ by (Asm_full_simp_tac 1);
+ by (case_tac "m" 1);
+ by (case_tac "p^a" 2);
+ by Auto_tac;
+(*now the hard case, simplified to
+ exponent p (Suc (p ^ a * m + i - p ^ a)) = exponent p (Suc i) *)
+by (subgoal_tac "0<p" 1);
+ by (force_tac (claset() addSDs [prime_imp_one_less], simpset()) 2);
+by (stac exponent_p_a_m_k_equation 1);
+by Auto_tac;
+qed "const_p_fac_right";
+
+Goal "0 < m ==> exponent p (((p^a) * m) choose p^a) = exponent p m";
+by (case_tac "p \\<in> prime" 1);
+by (Asm_simp_tac 2);
+by (forw_inst_tac [("a","a")] zero_less_prime_power 1);
+by (subgoal_tac "0 < p^a * m & p^a <= p^a * m" 1);
+by (Asm_full_simp_tac 2);
+(*A similar trick to the one used in p_not_div_choose_lemma:
+ insert an equation; use exponent_mult_add on the LHS; on the RHS, first
+ transform the binomial coefficient, then use exponent_mult_add.*)
+by (subgoal_tac
+ "exponent p ((((p^a) * m) choose p^a) * p^a) = a + exponent p m" 1);
+by (asm_full_simp_tac (simpset() delsimps bad_Sucs
+ addsimps [zero_less_binomial_iff, exponent_mult_add, prime_iff]) 1);
+(*one subgoal left!*)
+by (stac times_binomial_minus1_eq 1);
+by (Asm_full_simp_tac 1);
+by (Asm_full_simp_tac 1);
+by (stac exponent_mult_add 1);
+by (Asm_full_simp_tac 1);
+by (asm_simp_tac (simpset() addsimps [zero_less_binomial_iff]) 1);
+by (arith_tac 1);
+by (asm_simp_tac (simpset() delsimps bad_Sucs
+ addsimps [exponent_mult_add, const_p_fac_right]) 1);
+qed "const_p_fac";
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/GroupTheory/Exponent.thy Sun Jun 10 08:03:35 2001 +0200
@@ -0,0 +1,18 @@
+(* Title: HOL/GroupTheory/Exponent
+ ID: $Id$
+ Author: Florian Kammueller, with new proofs by L C Paulson
+ Copyright 2001 University of Cambridge
+*)
+
+Exponent = Main + Primes +
+
+constdefs
+
+ (*??use the one in Fun.thy?*)
+ funcset :: "['a set, 'b set] => ('a => 'b) set" ("_ -> _" [91,90]90)
+ "A -> B == {f. \\<forall>x \\<in> A. f(x) \\<in> B}"
+
+ exponent :: "[nat, nat] => nat"
+ "exponent p s == if p \\<in> prime then (GREATEST r. p ^ r dvd s) else 0"
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/GroupTheory/Group.ML Sun Jun 10 08:03:35 2001 +0200
@@ -0,0 +1,849 @@
+(* Title: HOL/GroupTheory/Group
+ ID: $Id$
+ Author: Florian Kammueller, with new proofs by L C Paulson
+ Copyright 2001 University of Cambridge
+*)
+
+(* Proof of the first theorem of Sylow, building on Group.thy
+F. Kammueller 4.9.96.
+The proofs are not using any simplification tacticals or alike, they are very
+basic stepwise derivations. Thus, they are very long.
+The reason for doing it that way is that I wanted to learn about reasoning in
+HOL and Group.thy.*)
+
+(* general *)
+val [p1] = goal (the_context()) "f\\<in>A -> B ==> \\<forall>x\\<in>A. f x\\<in>B";
+by (res_inst_tac [("a","f")] CollectD 1);
+by (fold_goals_tac [funcset_def]);
+by (rtac p1 1);
+qed "funcsetE";
+
+val [p1] = goal (the_context()) "\\<forall>x\\<in>A. f x\\<in>B ==> f\\<in>A -> B";
+by (rewtac funcset_def);
+by (rtac CollectI 1);
+by (rtac p1 1);
+qed "funcsetI";
+
+
+val [p1] = goal (the_context()) "f\\<in>A -> B -> C ==> \\<forall>x\\<in>A. \\<forall> y\\<in>B. f x y\\<in>C";
+by (rtac ballI 1);
+by (res_inst_tac [("a","f x")] CollectD 1);
+by (res_inst_tac [("A","A")] bspec 1);
+by (assume_tac 2);
+by (res_inst_tac [("a","f")] CollectD 1);
+by (fold_goals_tac [funcset_def]);
+by (rtac p1 1);
+qed "funcsetE2";
+
+val [p1] = goal (the_context()) "\\<forall>x\\<in>A. \\<forall> y\\<in>B. f x y\\<in>C ==> f\\<in>A -> B -> C";
+by (rewtac funcset_def);
+by (rtac CollectI 1);
+by (rtac ballI 1);
+by (rtac CollectI 1);
+by (res_inst_tac [("A","A")] bspec 1);
+by (assume_tac 2);
+by (rtac p1 1);
+qed "funcsetI2";
+
+
+val [p1,p2,p3,p4] = goal (the_context())
+ "[| finite A; finite B; \
+\ \\<exists>f \\<in> A -> B. inj_on f A; \\<exists>g \\<in> B -> A. inj_on g B |] ==> card(A) = card(B)";
+by (rtac le_anti_sym 1);
+by (rtac bexE 1);
+by (rtac p3 1);
+by (rtac (p2 RS (p1 RS card_inj)) 1);
+by (assume_tac 1);
+by (assume_tac 1);
+by (rtac bexE 1);
+by (rtac p4 1);
+by (rtac (p1 RS (p2 RS card_inj)) 1);
+by (assume_tac 1);
+by (assume_tac 1);
+qed "card_bij";
+
+Goal "order(G) = card(carrier G)";
+by (simp_tac (simpset() addsimps [order_def,carrier_def]) 1);
+qed "order_eq";
+
+
+(* Basic group properties *)
+goal (the_context()) "bin_op (H, bin_op G, invers G, unity G) = bin_op G";
+by (rewtac bin_op_def);
+by (rewrite_goals_tac [snd_conv RS eq_reflection]);
+by (rewrite_goals_tac [fst_conv RS eq_reflection]);
+by (rtac refl 1);
+qed "bin_op_conv";
+
+goal (the_context()) "carrier (H, bin_op G, invers G, unity G) = H";
+by (rewtac carrier_def);
+by (rewrite_goals_tac [fst_conv RS eq_reflection]);
+by (rtac refl 1);
+qed "carrier_conv";
+
+goal (the_context()) "invers (H, bin_op G, invers G, unity G) = invers G";
+by (rewtac invers_def);
+by (rewrite_goals_tac [snd_conv RS eq_reflection]);
+by (rewrite_goals_tac [fst_conv RS eq_reflection]);
+by (rtac refl 1);
+qed "invers_conv";
+
+goal (the_context()) "G\\<in>Group ==> (carrier G, bin_op G, invers G, unity G) = G";
+by (rewrite_goals_tac [carrier_def,invers_def,unity_def,bin_op_def]);
+by (rtac (surjective_pairing RS subst) 1);
+by (rtac (surjective_pairing RS subst) 1);
+by (rtac (surjective_pairing RS subst) 1);
+by (rtac refl 1);
+qed "G_conv";
+
+(* Derivations of the Group definitions *)
+val [q1] = goal (the_context()) "G\\<in>Group ==> unity G\\<in>carrier G";
+by (rtac (q1 RSN(2,mp)) 1);
+by (res_inst_tac [("P","%x. x\\<in>Group --> unity G\\<in>carrier G")] subst 1);
+by (rtac (q1 RS G_conv) 1);
+by (rtac impI 1);
+by (rewtac Group_def);
+by (dtac CollectD_prod4 1);
+by (Fast_tac 1);
+qed "unity_closed";
+
+(* second part is identical to previous proof *)
+val [q1,q2,q3] = goal (the_context()) "[| G\\<in>Group; a\\<in>carrier G; b\\<in>carrier G |] ==> bin_op G a b\\<in>carrier G";
+by (res_inst_tac [("x","b")] bspec 1);
+by (rtac q3 2);
+by (res_inst_tac [("x","a")] bspec 1);
+by (rtac q2 2);
+by (rtac funcsetE2 1);
+by (rtac (q1 RSN(2,mp)) 1);
+by (res_inst_tac [("P","%x. x\\<in>Group --> bin_op G\\<in>carrier G -> carrier G -> carrier G")] subst 1);
+by (rtac (q1 RS G_conv) 1);
+by (rtac impI 1);
+by (rewtac Group_def);
+by (dtac CollectD_prod4 1);
+by (Fast_tac 1);
+qed "bin_op_closed";
+
+val [q1,q2] = goal (the_context()) "[| G\\<in>Group; a\\<in>carrier G |] ==> invers G a\\<in>carrier G";
+by (res_inst_tac [("x","a")] bspec 1);
+by (rtac q2 2);
+by (rtac funcsetE 1);
+by (rtac (q1 RSN(2,mp)) 1);
+by (res_inst_tac [("P","%x. x\\<in>Group --> invers G\\<in>carrier G -> carrier G")] subst 1);
+by (rtac (q1 RS G_conv) 1);
+by (rtac impI 1);
+by (rewtac Group_def);
+by (dtac CollectD_prod4 1);
+by (Fast_tac 1);
+qed "invers_closed";
+
+val [q1,q2] = goal (the_context()) "[| G\\<in>Group; a\\<in>carrier G |] ==> bin_op G (unity G) a = a";
+by (rtac (q1 RSN(2,mp)) 1);
+by (res_inst_tac [("P","%x. x\\<in>Group --> bin_op G (unity G) a = a")] subst 1);
+by (rtac (q1 RS G_conv) 1);
+by (rtac impI 1);
+by (rewtac Group_def);
+by (dtac CollectD_prod4 1);
+by (dtac conjunct2 1);
+by (dtac conjunct2 1);
+by (dtac conjunct2 1);
+by (dtac bspec 1);
+by (rtac q2 1);
+by (dtac bspec 1);
+by (rtac q2 1);
+by (dtac bspec 1);
+by (rtac q2 1);
+by (Fast_tac 1);
+qed "unity_ax1";
+
+(* Apart from the instantiation in third line identical to last proof ! *)
+val [q1,q2] = goal (the_context()) "[| G\\<in>Group; a\\<in>carrier G |] ==> bin_op G (invers G a) a = unity G";
+by (rtac (q1 RSN(2,mp)) 1);
+by (res_inst_tac [("P","%x. x\\<in>Group --> bin_op G (invers G a) a = unity G")] subst 1);
+by (rtac (q1 RS G_conv) 1);
+by (rtac impI 1);
+by (rewtac Group_def);
+by (dtac CollectD_prod4 1);
+by (dtac conjunct2 1);
+by (dtac conjunct2 1);
+by (dtac conjunct2 1);
+by (dtac bspec 1);
+by (rtac q2 1);
+by (dtac bspec 1);
+by (rtac q2 1);
+by (dtac bspec 1);
+by (rtac q2 1);
+by (Fast_tac 1);
+qed "invers_ax2";
+
+(* again similar, different instantiation also in bspec's later *)
+val [q1,q2,q3,q4] = goal (the_context()) "[| G\\<in>Group; a\\<in>carrier G; b\\<in>carrier G; c\\<in>carrier G |] \
+\ ==> bin_op G (bin_op G a b) c = bin_op G a (bin_op G b c)";
+by (rtac (q1 RSN(2,mp)) 1);
+by (res_inst_tac [("P","%x. x\\<in>Group --> bin_op G (bin_op G a b) c = bin_op G a (bin_op G b c)")] subst 1);
+by (rtac (q1 RS G_conv) 1);
+by (rtac impI 1);
+by (rewtac Group_def);
+by (dtac CollectD_prod4 1);
+by (dtac conjunct2 1);
+by (dtac conjunct2 1);
+by (dtac conjunct2 1);
+by (dtac bspec 1);
+by (rtac q2 1);
+by (dtac bspec 1);
+by (rtac q3 1);
+by (dtac bspec 1);
+by (rtac q4 1);
+by (Fast_tac 1);
+qed "bin_op_assoc";
+
+val [p1,p2,p3,p4,p5] = goal (the_context()) "[| G\\<in>Group; x\\<in>carrier G; y\\<in>carrier G;\
+\ z\\<in>carrier G; bin_op G x y = bin_op G x z |] ==> y = z";
+by (res_inst_tac [("P","%r. r = z")] (unity_ax1 RS subst) 1);
+by (rtac p1 1);
+by (rtac p3 1);
+by (res_inst_tac [("P","%r. bin_op G r y = z")] subst 1);
+by (res_inst_tac [("a","x")] invers_ax2 1);
+by (rtac p1 1);
+by (rtac p2 1);
+by (stac bin_op_assoc 1);
+by (rtac p1 1);
+by (rtac invers_closed 1);
+by (rtac p1 1);
+by (rtac p2 1);
+by (rtac p2 1);
+by (rtac p3 1);
+by (stac p5 1);
+by (rtac (bin_op_assoc RS subst) 1);
+by (rtac p1 1);
+by (rtac invers_closed 1);
+by (rtac p1 1);
+by (rtac p2 1);
+by (rtac p2 1);
+by (rtac p4 1);
+by (stac invers_ax2 1);
+by (rtac p1 1);
+by (rtac p2 1);
+by (stac unity_ax1 1);
+by (rtac p1 1);
+by (rtac p4 1);
+by (rtac refl 1);
+qed "left_cancellation";
+
+(* here all other directions of basic lemmas, they need a cancellation *)
+(* to be able to show the other directions of inverse and unity axiom we need:*)
+val [q1,q2] = goal (the_context()) "[| G\\<in>Group; a\\<in>carrier G |] ==> bin_op G a (unity G) = a";
+by (res_inst_tac [("x","invers G a")] left_cancellation 1);
+by (rtac q1 1);
+by (rtac (q2 RS (q1 RS invers_closed)) 1);
+by (rtac (q2 RS (q1 RS bin_op_closed)) 1);
+by (rtac (q1 RS unity_closed) 1);
+by (rtac q2 1);
+by (rtac (q1 RS bin_op_assoc RS subst) 1);
+by (rtac (q2 RS (q1 RS invers_closed)) 1);
+by (rtac q2 1);
+by (rtac (q1 RS unity_closed) 1);
+by (rtac (q1 RS invers_ax2 RS ssubst) 1);
+by (rtac q2 1);
+by (rtac (q1 RS unity_ax1 RS ssubst) 1);
+by (rtac (q1 RS unity_closed) 1);
+by (rtac refl 1);
+qed "unity_ax2";
+
+val [q1,q2,q3] = goal (the_context()) "[| G \\<in> Group; a\\<in>carrier G; bin_op G a a = a |] ==> a = unity G";
+by (rtac (q3 RSN(2,mp)) 1);
+by (res_inst_tac [("P","%x. bin_op G a a = x --> a = unity G")] subst 1);
+by (rtac (q2 RS (q1 RS unity_ax2)) 1);
+by (rtac impI 1);
+by (res_inst_tac [("x","a")] left_cancellation 1);
+by (assume_tac 5);
+by (rtac q1 1);
+by (rtac q2 1);
+by (rtac q2 1);
+by (rtac (q1 RS unity_closed) 1);
+qed "idempotent_e";
+
+val [q1,q2] = goal (the_context()) "[| G\\<in>Group; a\\<in>carrier G |] ==> bin_op G a (invers G a) = unity G";
+by (rtac (q1 RS idempotent_e) 1);
+by (rtac (q1 RS bin_op_closed) 1);
+by (rtac q2 1);
+by (rtac (q2 RS (q1 RS invers_closed)) 1);
+by (rtac (q1 RS bin_op_assoc RS ssubst) 1);
+by (rtac q2 1);
+by (rtac (q2 RS (q1 RS invers_closed)) 1);
+by (rtac (q2 RS (q1 RS bin_op_closed)) 1);
+by (rtac (q2 RS (q1 RS invers_closed)) 1);
+by (res_inst_tac [("t","bin_op G (invers G a) (bin_op G a (invers G a))")] subst 1);
+by (rtac (q1 RS bin_op_assoc) 1);
+by (rtac (q2 RS (q1 RS invers_closed)) 1);
+by (rtac q2 1);
+by (rtac (q2 RS (q1 RS invers_closed)) 1);
+by (rtac (q2 RS (q1 RS invers_ax2) RS ssubst) 1);
+by (rtac (q1 RS unity_ax1 RS ssubst) 1);
+by (rtac (q2 RS (q1 RS invers_closed)) 1);
+by (rtac refl 1);
+qed "invers_ax1";
+
+val [p1,p2,p3] = goal (the_context()) "[|(P==>Q); (Q==>R); P |] ==> R";
+by (rtac p2 1);
+by (rtac p1 1);
+by (rtac p3 1);
+qed "trans_meta";
+
+val [p1,p2,p3,p4] = goal (the_context()) "[| G\\<in>Group; M <= carrier G; g\\<in>carrier G; h\\<in>carrier G |] \
+\ ==> r_coset G (r_coset G M g) h = r_coset G M (bin_op G g h)";
+by (rewtac r_coset_def);
+by (rtac equalityI 1);
+by (rtac subsetI 1);
+by (rtac CollectI 1);
+by (rtac trans_meta 1);
+by (assume_tac 3);
+by (etac CollectD 1);
+by (rtac bexE 1);
+by (assume_tac 1);
+by (etac subst 1);
+by (rtac trans_meta 1);
+by (assume_tac 3);
+by (res_inst_tac [("a","xa")] CollectD 1);
+by (assume_tac 1);
+by (res_inst_tac [("A","M")] bexE 1);
+by (assume_tac 1);
+by (etac subst 1);
+by (res_inst_tac [("x","xb")] bexI 1);
+by (rtac (bin_op_assoc RS subst) 1);
+by (rtac refl 5);
+by (assume_tac 5);
+by (rtac p4 4);
+by (rtac p3 3);
+by (rtac p1 1);
+by (rtac subsetD 1);
+by (assume_tac 2);
+by (rtac p2 1);
+(* end of first <= obligation *)
+by (rtac subsetI 1);
+by (rtac CollectI 1);
+by (rtac trans_meta 1);
+by (assume_tac 3);
+by (etac CollectD 1);
+by (rtac bexE 1);
+by (assume_tac 1);
+by (etac subst 1);
+by (res_inst_tac [("x","bin_op G xa g")] bexI 1);
+by (rtac CollectI 2);
+by (res_inst_tac [("x","xa")] bexI 2);
+by (assume_tac 3);
+by (rtac refl 2);
+by (rtac (bin_op_assoc RS subst) 1);
+by (rtac p1 1);
+by (rtac subsetD 1);
+by (assume_tac 2);
+by (rtac p2 1);
+by (rtac p3 1);
+by (rtac p4 1);
+by (rtac refl 1);
+qed "coset_mul_assoc";
+
+val [q1,q2] = goal (the_context()) "[| G \\<in> Group; M <= carrier G |] ==> r_coset G M (unity G) = M";
+by (rewtac r_coset_def);
+by (rtac equalityI 1);
+by (rtac subsetI 1);
+by (dtac CollectD 1);
+by (etac bexE 1);
+by (etac subst 1);
+by (stac unity_ax2 1);
+by (rtac q1 1);
+by (assume_tac 2);
+by (etac (q2 RS subsetD) 1);
+(* one direction <= finished *)
+by (rtac subsetI 1);
+by (rtac CollectI 1);
+by (rtac bexI 1);
+by (assume_tac 2);
+by (rtac unity_ax2 1);
+by (rtac q1 1);
+by (etac (q2 RS subsetD) 1);
+qed "coset_mul_unity";
+
+
+val [q1,q2,q3,q4] = goal (the_context()) "[| G \\<in> Group; x\\<in>carrier G; H <<= G;\
+\ x\\<in>H |] ==> r_coset G H x = H";
+by (rewtac r_coset_def);
+by (rtac equalityI 1);
+by (rtac subsetI 1);
+by (dtac CollectD 1);
+by (etac bexE 1);
+by (etac subst 1);
+by (rtac (bin_op_conv RS subst) 1);
+by (rtac (carrier_conv RS subst) 1);
+val l1 = q3 RS (subgroup_def RS apply_def) RS conjunct2;
+by (rtac (l1 RS bin_op_closed) 1);
+by (stac carrier_conv 1);
+by (assume_tac 1);
+by (stac carrier_conv 1);
+by (rtac q4 1);
+(* first <= finished *)
+by (rtac subsetI 1);
+by (rtac CollectI 1);
+by (res_inst_tac [("x","bin_op G xa (invers G x)")] bexI 1);
+by (stac bin_op_assoc 1);
+by (rtac q1 1);
+by (rtac q2 3);
+val l3 = q3 RS (subgroup_def RS apply_def) RS conjunct1;
+by (rtac subsetD 1);
+by (rtac l3 1);
+by (assume_tac 1);
+by (rtac invers_closed 1);
+by (rtac q1 1);
+by (rtac q2 1);
+by (stac invers_ax2 1);
+by (rtac q1 1);
+by (rtac q2 1);
+by (rtac unity_ax2 1);
+by (rtac q1 1);
+by (rtac subsetD 1);
+by (rtac l3 1);
+by (assume_tac 1);
+by (rtac (bin_op_conv RS subst) 1);
+by (rtac (carrier_conv RS subst) 1);
+by (rtac (l1 RS bin_op_closed) 1);
+by (rewrite_goals_tac [carrier_conv RS eq_reflection]);
+by (assume_tac 1);
+by (rtac (invers_conv RS subst) 1);
+by (rtac (carrier_conv RS subst) 1);
+by (rtac (l1 RS invers_closed) 1);
+by (stac carrier_conv 1);
+by (rtac q4 1);
+qed "coset_join2";
+
+val [q1,q2,q3,q4,q5] = goal (the_context()) "[| G \\<in> Group; x\\<in>carrier G; y\\<in>carrier G;\
+\ M <= carrier G; r_coset G M (bin_op G x (invers G y)) = M |] ==> r_coset G M x = r_coset G M y";
+by (res_inst_tac [("P","%z. r_coset G M x = r_coset G z y")] (q5 RS subst) 1);
+by (stac coset_mul_assoc 1);
+by (rtac q1 1);
+by (rtac q4 1);
+by (rtac bin_op_closed 1);
+by (rtac q1 1);
+by (rtac q2 1);
+by (rtac (q3 RS (q1 RS invers_closed)) 1);
+by (rtac q3 1);
+by (rtac (q1 RS bin_op_assoc RS ssubst) 1);
+by (rtac q2 1);
+by (rtac (q3 RS (q1 RS invers_closed)) 1);
+by (rtac q3 1);
+by (rtac (q1 RS invers_ax2 RS ssubst) 1);
+by (rtac q3 1);
+by (rtac (q1 RS unity_ax2 RS ssubst) 1);
+by (rtac q2 1);
+by (rtac refl 1);
+qed "coset_mul_invers1";
+
+val [q1,q2,q3,q4,q5] = goal (the_context()) "[| G \\<in> Group; x\\<in>carrier G; y\\<in>carrier G;\
+\ M <= carrier G; r_coset G M x = r_coset G M y|] ==> r_coset G M (bin_op G x (invers G y)) = M ";
+by (rtac (coset_mul_assoc RS subst) 1);
+by (rtac q1 1);
+by (rtac q4 1);
+by (rtac q2 1);
+by (rtac (q3 RS (q1 RS invers_closed)) 1);
+by (stac q5 1);
+by (rtac (q1 RS coset_mul_assoc RS ssubst) 1);
+by (rtac q4 1);
+by (rtac q3 1);
+by (rtac (q3 RS (q1 RS invers_closed)) 1);
+by (stac invers_ax1 1);
+by (rtac q1 1);
+by (rtac q3 1);
+by (rtac (q4 RS (q1 RS coset_mul_unity)) 1);
+qed "coset_mul_invers2";
+
+
+val [q1,q2] = goal (the_context()) "[|G\\<in>Group; H <<= G|] ==> unity G\\<in>H";
+by (rtac (q2 RSN(2,mp)) 1);
+by (rtac impI 1);
+by (dtac (subgroup_def RS apply_def RS conjunct2) 1);
+by (rewtac Group_def);
+by (dtac CollectD_prod4 1);
+by (Fast_tac 1);
+qed "SG_unity";
+
+
+val [q1,q2,q3,q4] = goal (the_context()) "[| G \\<in> Group; x\\<in>carrier G; H <<= G;\
+\ r_coset G H x = H |] ==> x\\<in>H";
+by (rtac (q4 RS subst) 1);
+by (rewtac r_coset_def);
+by (rtac CollectI 1);
+by (res_inst_tac [("x", "unity G")] bexI 1);
+by (rtac unity_ax1 1);
+by (rtac q1 1);
+by (rtac q2 1);
+by (rtac SG_unity 1);
+by (rtac q1 1);
+by (rtac q3 1);
+qed "coset_join1";
+
+
+val [q1,q2,q3] = goal (the_context()) "[| G \\<in> Group; finite(carrier G); H <<= G |] ==> 0 < card(H)";
+by (rtac zero_less_card_empty 1);
+by (rtac ExEl_NotEmpty 2);
+by (res_inst_tac [("x","unity G")] exI 2);
+by (rtac finite_subset 1);
+by (rtac (q3 RS (subgroup_def RS apply_def) RS conjunct1) 1);
+by (rtac q2 1);
+by (rtac SG_unity 1);
+by (rtac q1 1);
+by (rtac q3 1);
+qed "SG_card1";
+
+
+(* subgroupI: a characterization of subgroups *)
+val [p1,p2,p3,p4,p5] = goal (the_context()) "[|G\\<in>Group; H <= carrier G; H \\<noteq> {}; \\<forall> a \\<in> H. invers G a\\<in>H;\
+\ \\<forall> a\\<in>H. \\<forall> b\\<in>H. bin_op G a b\\<in>H|] ==> H <<= G";
+by (rewtac subgroup_def);
+by (rtac conjI 1);
+by (rtac p2 1);
+by (rewtac Group_def);
+by (rtac CollectI_prod4 1);
+by (rtac conjI 1);
+by (rtac conjI 2);
+by (rtac conjI 3);
+by (rtac funcsetI2 1);
+by (rtac p5 1);
+by (rtac funcsetI 1);
+by (rtac p4 1);
+by (rtac exE 1);
+by (rtac (p3 RS NotEmpty_ExEl) 1);
+by (rtac (invers_ax1 RS subst) 1);
+by (etac (p2 RS subsetD) 2);
+by (rtac p1 1);
+by (rtac (p5 RS bspec RS bspec) 1);
+by (assume_tac 1);
+by (etac (p4 RS bspec) 1);
+by (REPEAT (rtac ballI 1));
+by (rtac conjI 1);
+by (rtac conjI 2);
+by (rtac (p1 RS bin_op_assoc) 3);
+by (REPEAT (etac (p2 RS subsetD) 3));
+by (rtac (p1 RS unity_ax1) 2);
+by (etac (p2 RS subsetD) 2);
+by (rtac (p1 RS invers_ax2) 1);
+by (etac (p2 RS subsetD) 1);
+qed "subgroupI";
+
+
+val [p1,p2,p3,p4,p5] = goal (the_context()) "[| G\\<in>Group; x\\<in>carrier G; y\\<in>carrier G;\
+\ z\\<in>carrier G; bin_op G y x = bin_op G z x|] ==> y = z";
+by (res_inst_tac [("P","%r. r = z")] (unity_ax2 RS subst) 1);
+by (rtac p1 1);
+by (rtac p3 1);
+by (res_inst_tac [("P","%r. bin_op G y r = z")] subst 1);
+by (res_inst_tac [("a","x")] invers_ax1 1);
+by (rtac p1 1);
+by (rtac p2 1);
+by (rtac (bin_op_assoc RS subst) 1);
+by (rtac p1 1);
+by (rtac p3 1);
+by (rtac p2 1);
+by (rtac invers_closed 1);
+by (rtac p1 1);
+by (rtac p2 1);
+by (stac p5 1);
+by (stac bin_op_assoc 1);
+by (rtac p1 1);
+by (rtac p4 1);
+by (rtac p2 1);
+by (rtac invers_closed 1);
+by (rtac p1 1);
+by (rtac p2 1);
+by (stac invers_ax1 1);
+by (rtac p1 1);
+by (rtac p2 1);
+by (stac unity_ax2 1);
+by (rtac p1 1);
+by (rtac p4 1);
+by (rtac refl 1);
+qed "right_cancellation";
+
+
+(* further general theorems necessary for Lagrange *)
+val [p1,p2] = goal (the_context()) "[| G \\<in> Group; H <<= G|]\
+\ ==> \\<Union> (set_r_cos G H) = carrier G";
+by (rtac equalityI 1);
+by (rtac subsetI 1);
+by (etac UnionE 1);
+by (SELECT_GOAL (rewtac set_r_cos_def) 1);
+by (dtac CollectD 1);
+by (etac bexE 1);
+by (SELECT_GOAL (rewtac r_coset_def) 1);
+by (rtac subsetD 1);
+by (assume_tac 2);
+by (etac ssubst 1);
+by (rtac subsetI 1);
+by (dtac CollectD 1);
+by (etac bexE 1);
+by (etac subst 1);
+by (rtac (p1 RS bin_op_closed) 1);
+by (assume_tac 2);
+by (rtac subsetD 1);
+by (assume_tac 2);
+by (rtac (p2 RS (subgroup_def RS apply_def) RS conjunct1) 1);
+by (rtac subsetI 1);
+by (res_inst_tac [("X","r_coset G H x")] UnionI 1);
+by (rewtac set_r_cos_def);
+by (rtac CollectI 1);
+by (rtac bexI 1);
+by (assume_tac 2);
+by (rtac refl 1);
+by (rewtac r_coset_def);
+by (rtac CollectI 1);
+by (rtac bexI 1);
+by (etac (p1 RS unity_ax1) 1);
+by (rtac (p2 RS (p1 RS SG_unity)) 1);
+qed "set_r_cos_part_G";
+
+
+val [p1,p2,p3] = goal (the_context()) "[| G \\<in> Group; H <= carrier G; a\\<in>carrier G |]\
+\ ==> r_coset G H a <= carrier G";
+by (rtac subsetI 1);
+by (rewtac r_coset_def);
+by (dtac CollectD 1);
+by (etac bexE 1);
+by (etac subst 1);
+by (rtac (p1 RS bin_op_closed) 1);
+by (etac (p2 RS subsetD) 1);
+by (rtac p3 1);
+qed "rcosetGHa_subset_G";
+
+val [p1,p2,p3] = goal (the_context()) "[|G\\<in>Group; H <= carrier G; finite(carrier G) |]\
+\ ==> \\<forall> c \\<in> set_r_cos G H. card c = card H";
+by (rtac ballI 1);
+by (rewtac set_r_cos_def);
+by (dtac CollectD 1);
+by (etac bexE 1);
+by (etac ssubst 1);
+by (rtac card_bij 1); (*use card_bij_eq??*)
+by (rtac finite_subset 1);
+by (rtac p3 2);
+by (etac (p2 RS (p1 RS rcosetGHa_subset_G)) 1);
+by (rtac (p3 RS (p2 RS finite_subset)) 1);
+(* injective maps *)
+by (res_inst_tac [("x","%y. bin_op G y (invers G a)")] bexI 1);
+by (SELECT_GOAL (rewtac funcset_def) 2);
+by (rtac CollectI 2);
+by (rtac ballI 2);
+by (SELECT_GOAL (rewtac r_coset_def) 2);
+by (dtac CollectD 2);
+by (etac bexE 2);
+by (etac subst 2);
+by (rtac (p1 RS bin_op_assoc RS ssubst) 2);
+by (etac (p2 RS subsetD) 2);
+by (assume_tac 2);
+by (etac (p1 RS invers_closed) 2);
+by (etac (p1 RS invers_ax1 RS ssubst) 2);
+by (rtac (p1 RS unity_ax2 RS ssubst) 2);
+by (assume_tac 3);
+by (etac (p2 RS subsetD) 2);
+by (rtac inj_onI 1);
+by (rtac (p1 RS right_cancellation) 1);
+by (rtac (p1 RS invers_closed) 1);
+by (assume_tac 1);
+by (rtac (rcosetGHa_subset_G RS subsetD) 1);
+by (rtac p1 1);
+by (rtac p2 1);
+by (assume_tac 1);
+by (assume_tac 1);
+by (rtac (rcosetGHa_subset_G RS subsetD) 1);
+by (rtac p1 1);
+by (rtac p2 1);
+by (assume_tac 1);
+by (assume_tac 1);
+by (assume_tac 1);
+(* f finished *)
+by (res_inst_tac [("x","%y. bin_op G y a")] bexI 1);
+by (SELECT_GOAL (rewtac funcset_def) 2);
+by (rtac CollectI 2);
+by (rtac ballI 2);
+by (SELECT_GOAL (rewtac r_coset_def) 2);
+by (rtac CollectI 2);
+by (rtac bexI 2);
+by (rtac refl 2);
+by (assume_tac 2);
+by (rtac inj_onI 1);
+by (rtac (p1 RS right_cancellation) 1);
+by (assume_tac 1);
+by (etac (p2 RS subsetD) 1);
+by (etac (p2 RS subsetD) 1);
+by (assume_tac 1);
+qed "card_cosets_equal";
+
+
+val prems = goal (the_context()) "[| G \\<in> Group; x \\<in> carrier G; y \\<in> carrier G;\
+\ z\\<in>carrier G; bin_op G x y = z|] ==> y = bin_op G (invers G x) z";
+by (res_inst_tac [("x","x")] left_cancellation 1);
+by (REPEAT (ares_tac prems 1));
+by (rtac bin_op_closed 1);
+by (rtac invers_closed 2);
+by (REPEAT (ares_tac prems 1));
+by (rtac (bin_op_assoc RS subst) 1);
+by (rtac invers_closed 3);
+by (REPEAT (ares_tac prems 1));
+by (stac invers_ax1 1);
+by (stac unity_ax1 3);
+by (REPEAT (ares_tac prems 1));
+qed "transpose_invers";
+
+val [p1,p2,p3,p4] = goal (the_context()) "[| G \\<in> Group; H <<= G; h1 \\<in> H; h2 \\<in> H|]\
+\ ==> bin_op G h1 h2\\<in>H";
+by (rtac (bin_op_conv RS subst) 1);
+val l1 = (p2 RS (subgroup_def RS apply_def) RS conjunct2);
+by (rtac (carrier_conv RS subst) 1);
+by (rtac (l1 RS bin_op_closed) 1);
+by (rewrite_goals_tac [carrier_conv RS eq_reflection]);
+by (rtac p3 1);
+by (rtac p4 1);
+qed "SG_bin_op_closed";
+
+
+val [p1,p2,p3] = goal (the_context()) "[| G \\<in> Group; H <<= G; h1 \\<in> H|]\
+\ ==> invers G h1\\<in>H";
+by (rtac (invers_conv RS subst) 1);
+by (rtac (carrier_conv RS subst) 1);
+val l1 = (p2 RS (subgroup_def RS apply_def) RS conjunct2);
+by (rtac (l1 RS invers_closed) 1);
+by (stac carrier_conv 1);
+by (rtac p3 1);
+qed "SG_invers_closed";
+
+val [p1] = goal (the_context()) "x = y ==> bin_op G z x = bin_op G z y";
+by (res_inst_tac [("t","y")] subst 1);
+by (rtac refl 2);
+by (rtac p1 1);
+qed "left_extend";
+
+val [p1,p2] = goal (the_context()) "[| G \\<in> Group; H <<= G |]\
+\ ==> \\<forall> c1 \\<in> set_r_cos G H. \\<forall> c2 \\<in> set_r_cos G H. c1 \\<noteq> c2 --> c1 \\<inter> c2 = {}";
+val l1 = (p2 RS (subgroup_def RS apply_def) RS conjunct1);
+val l2 = l1 RS (p1 RS rcosetGHa_subset_G) RS subsetD;
+by (rtac ballI 1);
+by (rtac ballI 1);
+by (rtac impI 1);
+by (rtac notnotD 1);
+by (etac contrapos_nn 1);
+by (dtac NotEmpty_ExEl 1);
+by (etac exE 1);
+by (ftac IntD1 1);
+by (dtac IntD2 1);
+by (rewtac set_r_cos_def);
+by (dtac CollectD 1);
+by (dtac CollectD 1);
+by (etac bexE 1);
+by (etac bexE 1);
+by (hyp_subst_tac 1);
+by (hyp_subst_tac 1);
+by (rewtac r_coset_def);
+(* Level 17 *)
+by (rtac equalityI 1);
+by (rtac subsetI 1);
+by (rtac subsetI 2);
+by (rtac CollectI 1);
+by (rtac CollectI 2);
+by (dtac CollectD 1);
+by (dtac CollectD 2);
+by (ftac CollectD 1);
+by (ftac CollectD 2);
+by (dres_inst_tac [("a","xa")] CollectD 1);
+by (dres_inst_tac [("a","xa")] CollectD 2);
+by (fold_goals_tac [r_coset_def]);
+by (REPEAT (etac bexE 1));
+by (REPEAT (etac bexE 2));
+(* first solve 1 *)
+by (res_inst_tac [("x","bin_op G hb (bin_op G (invers G h) ha)")] bexI 1);
+by (stac bin_op_assoc 1);
+val G_closed_rules = [(p1 RS invers_closed),(p1 RS bin_op_closed),(p2 RS (p1 RS SG_invers_closed))
+ ,(p2 RS (p1 RS SG_bin_op_closed)),(l1 RS subsetD)];
+by (rtac p1 1);
+by (REPEAT (ares_tac G_closed_rules 1));
+by (REPEAT (ares_tac G_closed_rules 2));
+by (eres_inst_tac [("t","xa")] subst 1);
+by (rtac left_extend 1);
+by (stac bin_op_assoc 1);
+by (rtac p1 1);
+by (REPEAT (ares_tac G_closed_rules 1));
+by (eres_inst_tac [("t","bin_op G ha aa")] ssubst 1);
+by (rtac (p1 RS transpose_invers RS ssubst) 1);
+by (rtac refl 5);
+by (rtac l2 3);
+by (assume_tac 4);
+by (REPEAT (ares_tac G_closed_rules 1));
+(* second thing, level 47 *)
+by (res_inst_tac [("x","bin_op G hb (bin_op G (invers G ha) h)")] bexI 1);
+by (REPEAT (ares_tac G_closed_rules 2));
+by (stac bin_op_assoc 1);
+by (rtac p1 1);
+by (REPEAT (ares_tac G_closed_rules 1));
+by (eres_inst_tac [("t","xa")] subst 1);
+by (rtac left_extend 1);
+by (stac bin_op_assoc 1);
+by (rtac p1 1);
+by (REPEAT (ares_tac G_closed_rules 1));
+by (etac ssubst 1);
+by (rtac (p1 RS transpose_invers RS ssubst) 1);
+by (rtac refl 5);
+by (rtac l2 3);
+by (assume_tac 4);
+by (REPEAT (ares_tac G_closed_rules 1));
+qed "r_coset_disjunct";
+
+
+val [p1,p2] = goal (the_context()) "[| G \\<in> Group; H <<= G |]\
+\ ==> set_r_cos G H <= Pow( carrier G)";
+by (rewtac set_r_cos_def);
+by (rtac subsetI 1);
+by (dtac CollectD 1);
+by (etac bexE 1);
+by (etac ssubst 1);
+by (rtac PowI 1);
+by (rtac subsetI 1);
+by (rewtac r_coset_def);
+by (dtac CollectD 1);
+by (etac bexE 1);
+by (etac subst 1);
+by (rtac bin_op_closed 1);
+by (rtac p1 1);
+by (assume_tac 2);
+by (etac (p2 RS (subgroup_def RS apply_def) RS conjunct1 RS subsetD) 1);
+qed "set_r_cos_subset_PowG";
+
+val [p1,p2,p3] = goal (the_context()) "[| G \\<in> Group; finite(carrier G); H <<= G |]\
+\ ==> card(set_r_cos G H) * card(H) = order(G)";
+by (simp_tac (simpset() addsimps [order_eq]) 1);
+by (rtac (p3 RS (p1 RS set_r_cos_part_G) RS subst) 1);
+by (rtac (mult_commute RS subst) 1);
+by (rtac card_partition 1);
+by (rtac finite_subset 1);
+by (rtac (p3 RS (p1 RS set_r_cos_subset_PowG)) 1);
+by (simp_tac (simpset() addsimps [finite_Pow_iff]) 1);
+by (rtac p2 1);
+by (rtac (p3 RS (p1 RS set_r_cos_part_G) RS ssubst) 1);
+by (rtac p2 1);
+val l1 = (p3 RS (subgroup_def RS apply_def) RS conjunct1);
+by (rtac (l1 RS (p1 RS card_cosets_equal)) 1);
+by (rtac p2 1);
+by (rtac (p3 RS (p1 RS r_coset_disjunct)) 1);
+qed "Lagrange"; (*original version: closer to locales??*)
+
+ (*version using "Goal" but no locales...
+ Goal "[| G \\<in> Group; finite(carrier G); H <<= G |] \
+ \ ==> card(set_r_cos G H) * card(H) = order(G)";
+ by (asm_simp_tac (simpset() addsimps [order_eq, set_r_cos_part_G RS sym]) 1);
+ by (stac mult_commute 1);
+ by (rtac card_partition 1);
+ by (rtac finite_subset 1);
+ by (rtac set_r_cos_subset_PowG 1);
+ by (assume_tac 1); by (assume_tac 1);
+ by (simp_tac (simpset() addsimps [finite_Pow_iff]) 1);
+ by (asm_full_simp_tac (simpset() addsimps [set_r_cos_part_G]) 1);
+ by (rtac card_cosets_equal 1);
+ by (rtac r_coset_disjunct 4);
+ by Auto_tac;
+ by (asm_full_simp_tac (simpset() addsimps [subgroup_def]) 1);
+ by (blast_tac (claset() addIs []) 1);
+ qed "Lagrange";
+ *)
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/GroupTheory/Group.thy Sun Jun 10 08:03:35 2001 +0200
@@ -0,0 +1,60 @@
+(* Title: HOL/GroupTheory/Group
+ ID: $Id$
+ Author: Florian Kammueller, with new proofs by L C Paulson
+ Copyright 2001 University of Cambridge
+*)
+
+(* Theory of Groups, for Sylow's theorem. F. Kammueller, 11.10.96
+Step 1: Use two separate .thy files for groups and Sylow's thm, respectively:
+
+Besides the formalization of groups as polymorphic sets of quadruples this
+theory file contains a bunch of declarations and axioms of number theory
+because it is meant to be the basis for a proof experiment of the theorem of
+Sylow. This theorem uses various kinds of theoretical domains. To improve the
+syntactical form I have deleted here in contrast to the first almost complete
+version of the proof (8exp/Group.* or presently results/AllgGroup/Group.* )
+all definitions which are specific for Sylow's theorem. They are now contained
+in the file Sylow.thy.
+*)
+
+Group = Exponent +
+
+
+constdefs
+
+ carrier :: "('a set * (['a, 'a] => 'a) * ('a => 'a) * 'a) => 'a set"
+ "carrier(G) == fst(G)"
+
+ bin_op :: "('a set * (['a, 'a] => 'a) * ('a => 'a) * 'a) => (['a, 'a] => 'a)"
+ "bin_op(G) == fst(snd(G))"
+
+ invers :: "('a set * (['a, 'a] => 'a) * ('a => 'a) * 'a) => ('a => 'a)"
+"invers(G) == fst(snd(snd(G)))"
+
+ unity :: "('a set * (['a, 'a] => 'a) * ('a => 'a) * 'a) => 'a"
+ "unity(G) == snd(snd(snd(G)))"
+
+ order :: "('a set * (['a, 'a] => 'a) * ('a => 'a) * 'a) => nat"
+ "order(G) == card(fst(G))"
+
+ r_coset :: "[('a set * (['a, 'a] => 'a) * ('a => 'a) * 'a), 'a set, 'a] => 'a set"
+ "r_coset G H a == {b . ? h : H. bin_op G h a = b}"
+
+ set_r_cos :: "[('a set * (['a, 'a] => 'a) * ('a => 'a) * 'a), 'a set] => 'a set set"
+
+ "set_r_cos G H == {C . ? a : carrier G. C = r_coset G H a}"
+
+ subgroup :: "['a set,('a set * (['a, 'a] => 'a) * ('a => 'a) * 'a)] => bool"
+ ("_ <<= _" [51,50]50)
+
+ "H <<= G == H <= carrier(G) & (H,bin_op(G),invers(G),unity(G)) : Group"
+
+ Group :: "'a set"
+
+ "Group == {(G,f,inv,e). f : G -> G -> G & inv : G -> G & e : G &\
+\ (! x: G. ! y: G. !z: G.\
+\ (f (inv x) x = e) & (f e x = x) &
+ (f (f x y) z = f (x) (f y z)))}"
+
+end
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/GroupTheory/ROOT.ML Sun Jun 10 08:03:35 2001 +0200
@@ -0,0 +1,4 @@
+
+no_document use_thy "Primes";
+
+use_thy "Sylow";
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/GroupTheory/Sylow.ML Sun Jun 10 08:03:35 2001 +0200
@@ -0,0 +1,720 @@
+(* Title: HOL/GroupTheory/Group
+ ID: $Id$
+ Author: Florian Kammueller, with new proofs by L C Paulson
+ Copyright 2001 University of Cambridge
+*)
+
+(* The clean version, no comments, more tacticals*)
+
+AddIffs [p1 RS prime_imp_one_less];
+
+val [q1,q2,q3] = goal Sylow.thy "[|M <= carrier G; g\\<in>carrier G; h\\<in>carrier G |]\
+\ ==> (M #> g) #> h = M #> (g ## h)";
+by (rewrite_goals_tac [r_coset_abbr, bin_op_abbr]);
+by (rtac coset_mul_assoc 1);
+by (rtac p2 1);
+by (rtac q1 1);
+by (rtac q2 1);
+by (rtac q3 1);
+qed "Icoset_mul_assoc";
+
+val [q1] = goal Sylow.thy "[| M <= carrier G |] ==> M #> e = M";
+by (rewrite_goals_tac [r_coset_abbr,e_def]);
+by (rtac coset_mul_unity 1);
+by (rtac p2 1);
+by (rtac q1 1);
+qed "Icoset_mul_unity";
+
+val [q1,q2,q3,q4] = goal Sylow.thy "[| x\\<in>carrier G; y\\<in>carrier G;\
+\ M <= carrier G; M #> (x ## inv y) = M |] ==> M #> x = M #> y";
+by (rewtac r_coset_abbr);
+by (rtac coset_mul_invers1 1);
+by (rtac p2 1);
+by (rtac q1 1);
+by (rtac q2 1);
+by (rtac q3 1);
+by (fold_goals_tac [r_coset_abbr, bin_op_abbr,inv_def]);
+by (rtac q4 1);
+qed "Icoset_mul_invers1";
+
+val [q1,q2,q3,q4] = goal Sylow.thy "[| x\\<in>carrier G; y\\<in>carrier G;\
+\ M <= carrier G; M #> x = M #> y|] ==> M #> (x ## inv y) = M ";
+by (rewrite_goals_tac [r_coset_abbr,inv_def,bin_op_abbr]);
+by (rtac coset_mul_invers2 1);
+by (rtac p2 1);
+by (rtac q1 1);
+by (rtac q2 1);
+by (rtac q3 1);
+by (fold_goals_tac [r_coset_abbr]);
+by (rtac q4 1);
+qed "Icoset_mul_invers2";
+
+val [q1,q2,q3] = goal Sylow.thy "[| x\\<in>carrier G; H <<= G;\
+\ H #> x = H |] ==> x\\<in>H";
+by (rtac coset_join1 1);
+by (rtac p2 1);
+by (rtac q1 1);
+by (rtac q2 1);
+by (fold_goals_tac [r_coset_abbr]);
+by (rtac q3 1);
+qed "Icoset_join1";
+
+val [q1,q2,q3] = goal Sylow.thy "[| x\\<in>carrier G; H <<= G;\
+\ x\\<in>H |] ==> H #> x = H";
+by (rewtac r_coset_abbr);
+by (rtac coset_join2 1);
+by (rtac p2 1);
+by (rtac q1 1);
+by (rtac q2 1);
+by (rtac q3 1);
+qed "Icoset_join2";
+
+val [q1,q2,q3,q4] = goal Sylow.thy "[| x\\<in>carrier G; y\\<in>carrier G;\
+\ z\\<in>carrier G; x ## y = x ## z |] ==> y = z";
+by (rtac left_cancellation 1);
+by (rtac p2 1);
+by (fold_goals_tac [bin_op_abbr]);
+by (rtac q1 1);
+by (rtac q2 1);
+by (rtac q3 1);
+by (rtac q4 1);
+qed "Ileft_cancellation";
+
+val [q1,q2,q3,q4] = goal Sylow.thy "[| x\\<in>carrier G; y\\<in>carrier G;\
+\ z\\<in>carrier G; y ## x = z ## x |] ==> y = z";
+by (rtac right_cancellation 1);
+by (rtac p2 1);
+by (fold_goals_tac [bin_op_abbr]);
+by (rtac q1 1);
+by (rtac q2 1);
+by (rtac q3 1);
+by (rtac q4 1);
+qed "Iright_cancellation";
+
+goal Sylow.thy "e\\<in>carrier G";
+by (rewtac e_def);
+by (rtac (p2 RS unity_closed) 1);
+qed "Iunity_closed";
+
+val [q1,q2] = goal Sylow.thy "[|x\\<in>carrier G; y\\<in>carrier G |]\
+\ ==> x ## y\\<in>carrier G";
+by (rewtac bin_op_abbr);
+by (rtac bin_op_closed 1);
+by (rtac p2 1);
+by (rtac q1 1);
+by (rtac q2 1);
+qed "Ibin_op_closed";
+
+val [q1] = goal Sylow.thy "[|x\\<in>carrier G |] ==> inv x\\<in>carrier G";
+by (rewtac inv_def);
+by (rtac invers_closed 1);
+by (rtac p2 1);
+by (rtac q1 1);
+qed "Iinvers_closed";
+
+val [q1] = goal Sylow.thy "[| x\\<in>carrier G |] ==> e ## x = x";
+by (rewrite_goals_tac [e_def,bin_op_abbr]);
+by (rtac unity_ax1 1);
+by (rtac p2 1);
+by (rtac q1 1);
+qed "Iunity_ax1";
+
+val [q1] = goal Sylow.thy "[| x\\<in>carrier G |] ==> x ## e = x";
+by (rewrite_goals_tac [e_def,bin_op_abbr]);
+by (rtac unity_ax2 1);
+by (rtac p2 1);
+by (rtac q1 1);
+qed "Iunity_ax2";
+
+val [q1] = goal Sylow.thy "[| x\\<in>carrier G |] ==> x ## inv x = e";
+by (rewrite_goals_tac [e_def,inv_def,bin_op_abbr]);
+by (rtac invers_ax1 1);
+by (rtac p2 1);
+by (rtac q1 1);
+qed "Iinvers_ax1";
+
+val [q1] = goal Sylow.thy "[| x\\<in>carrier G |] ==> inv x ## x = e";
+by (rewrite_goals_tac [e_def,inv_def,bin_op_abbr]);
+by (rtac invers_ax2 1);
+by (rtac p2 1);
+by (rtac q1 1);
+qed "Iinvers_ax2";
+
+val [q1,q2,q3] = goal Sylow.thy "[| x\\<in>carrier G; y\\<in>carrier G; z\\<in>carrier G |] \
+\ ==> (x ## y)## z = x ##(y ## z)";
+by (rewtac bin_op_abbr);
+by (rtac bin_op_assoc 1);
+by (rtac p2 1);
+by (rtac q1 1);
+by (rtac q2 1);
+by (rtac q3 1);
+qed "Ibin_op_assoc";
+
+val [q1] = goal Sylow.thy "H <<= G ==> e\\<in>H";
+by (rewtac e_def);
+by (rtac SG_unity 1);
+by (rtac p2 1);
+by (rtac q1 1);
+qed "ISG_unity";
+
+val prems = goal Sylow.thy "[| H <= carrier G; H \\<noteq> {};\
+\ \\<forall> x \\<in> H. inv x \\<in> H; \\<forall> x \\<in> H. \\<forall> y \\<in> H. x ## y \\<in> H |] ==> H <<= G";
+by (rtac subgroupI 1);
+by (fold_goals_tac [bin_op_abbr, inv_def]);
+by (REPEAT (ares_tac (p2 :: prems) 1));
+qed "IsubgroupI";
+
+goal Sylow.thy "equiv calM RelM";
+by (rewtac equiv_def);
+by (Step_tac 1);
+by (rewrite_goals_tac [refl_def,RelM_def]);
+by (rtac conjI 1);
+by (Step_tac 1);
+by (res_inst_tac [("x","e")] bexI 1);
+by (rtac Iunity_closed 2);
+by (rtac (Icoset_mul_unity RS sym) 1);
+by (SELECT_GOAL (rewtac calM_def) 1);
+by (Fast_tac 1);
+by (rewtac sym_def);
+by (Step_tac 1);
+by (res_inst_tac [("x","inv g")] bexI 1);
+by (etac Iinvers_closed 2);
+by (stac Icoset_mul_assoc 1);
+by (etac Iinvers_closed 3);
+by (assume_tac 2);
+by (SELECT_GOAL (rewtac calM_def) 1);
+by (Fast_tac 1);
+by (etac (Iinvers_ax1 RS ssubst) 1);
+by (stac Icoset_mul_unity 1);
+by (SELECT_GOAL (rewtac calM_def) 1);
+by (Fast_tac 1);
+by (rtac refl 1);
+by (rewtac trans_def);
+by (Step_tac 1);
+by (res_inst_tac [("x","ga ## g")] bexI 1);
+by (rtac Icoset_mul_assoc 1);
+by (rewtac calM_def);
+by (rotate_tac 4 1);
+by (Fast_tac 1);
+by (assume_tac 1);
+by (assume_tac 1);
+by (etac Ibin_op_closed 1);
+by (assume_tac 1);
+qed "RelM_equiv";
+
+
+val [q1] = goal Sylow.thy
+" M\\<in>calM // RelM ==> M <= calM";
+by (rtac quotientE 1);
+by (rtac q1 1);
+by (etac ssubst 1);
+by (rewrite_goals_tac [Image_def, RelM_def,subset_def]);
+by (rtac ballI 1);
+by (dtac CollectD 1);
+(* change *)
+by (etac bexE 1);
+by (dtac CollectD_prod 1);
+by (dtac conjunct1 1);
+by (etac SigmaD2 1);
+qed "M_subset_calM_prep";
+
+val [q1] = goal Sylow.thy
+" M\\<in>calM // RelM & ~(p ^ ((exponent p m)+ 1) dvd card(M)) ==> M <= calM";
+by (rtac M_subset_calM_prep 1);
+by (rtac (q1 RS conjunct1) 1);
+qed "M_subset_calM";
+
+val [q1,q2] = goal Sylow.thy "[|M\\<in>calM // RelM & ~(p ^ ((exponent p m)+ 1) dvd card(M));\
+\ M1\\<in>M|] ==> card(M1) = p ^ a";
+by (res_inst_tac [("P", "M1 <= carrier G")] conjunct2 1);
+by (res_inst_tac [("a","M1")] CollectD 1);
+by (fold_goals_tac [calM_def]);
+by (rtac (q2 RSN(2, subsetD)) 1);
+by (rtac (q1 RS M_subset_calM) 1);
+qed "card_M1";
+
+val [q1,q2] = goal Sylow.thy
+ "[|M\\<in>calM // RelM & ~(p ^ ((exponent p m)+ 1) dvd card(M));\
+\ M1\\<in>M|] ==> \\<exists>x. x\\<in>M1";
+by (rtac NotEmpty_ExEl 1);
+by (rtac card_nonempty 1);
+by (rtac (q2 RS (q1 RS card_M1) RS ssubst) 1);
+by (rtac zero_less_prime_power 1);
+by (rtac p1 1);
+qed "exists_x_in_M1";
+
+val [q1,q2] = goal Sylow.thy "[| M\\<in>calM // RelM & ~(p ^ ((exponent p m)+ 1) dvd card(M));\
+\ M1\\<in>M|] ==> M1 <= carrier G";
+by (rtac PowD 1);
+by (rtac subsetD 1);
+by (rtac q2 2);
+by (rtac subset_trans 1);
+by (rtac (q1 RS M_subset_calM) 1);
+by (rewtac calM_def);
+by (rtac subsetI 1);
+by (rtac PowI 1);
+by (rtac conjunct1 1);
+by (etac CollectD 1);
+qed "M1_subset_G";
+
+val [q1,q2] = goal Sylow.thy
+"[| M\\<in>calM // RelM & ~(p ^ ((exponent p m)+ 1) dvd card(M)); M1\\<in>M|] ==> \
+\ \\<exists>f \\<in> {g. g\\<in>carrier G & M1 #> g = M1} -> M1. inj_on f {g. g\\<in>carrier G & M1 #> g = M1}";
+by (rtac exE 1);
+by (rtac (q2 RS (q1 RS exists_x_in_M1)) 1);
+by (res_inst_tac [("x", "% z. x ## z")] bexI 1);
+by (rewtac funcset_def);
+by (rtac CollectI 2);
+by (rtac ballI 2);
+by (dtac CollectD 2);
+by (ftac conjunct2 2);
+by (SELECT_GOAL (rewrite_goals_tac [r_coset_abbr, r_coset_def]) 2);
+by (dtac equalityD1 2);
+by (rewtac subset_def);
+by (fold_goals_tac [bin_op_abbr]);
+by (res_inst_tac [("P","%z. z\\<in>M1")] bspec 2);
+by (assume_tac 2);
+by (rtac CollectI 2);
+by (rtac bexI 2);
+by (assume_tac 3);
+by (rtac refl 2);
+by (rtac inj_onI 1);
+by (rtac Ileft_cancellation 1);
+by (assume_tac 4);
+by (dres_inst_tac [("a","y")] CollectD 3);
+by (etac conjunct1 3);
+by (dtac CollectD 2);
+by (etac conjunct1 2);
+by (etac (q2 RS (q1 RS M1_subset_G) RS subsetD) 1);
+val M1_inj_H = result();
+
+val [q1,q2] = goal Sylow.thy "[| {} = RelM `` {x}; x\\<in>calM |] ==> False";
+by (res_inst_tac [("a","x")] emptyE 1);
+by (stac q1 1);
+by (rtac (q2 RS(RelM_equiv RS equiv_class_self)) 1);
+qed "RangeNotEmpty";
+
+goal Sylow.thy "{} \\<notin> calM // RelM";
+by (rtac notI 1);
+by (rtac (RangeNotEmpty RSN (2, quotientE)) 1);
+by (assume_tac 1);
+by (assume_tac 1);
+by (assume_tac 1);
+qed "EmptyNotInEquivSet";
+
+val [q1] = goal Sylow.thy
+"M\\<in>calM // RelM & ~(p ^ ((exponent p m)+ 1) dvd card(M))==> \\<exists>M1. M1\\<in>M";
+by (rtac NotEmpty_ExEl 1);
+by (rtac (q1 RS conjunct1 RSN (2, MnotEqempty)) 1);
+by (rtac EmptyNotInEquivSet 1);
+qed "existsM1inM";
+
+goal Sylow.thy "0 < order(G)";
+by (rewtac order_def);
+by (fold_goals_tac [carrier_def]);
+by (rtac zero_less_card_empty 1);
+by (rtac p4 1);
+by (rtac ExEl_NotEmpty 1);
+by (res_inst_tac [("x","e")] exI 1);
+by (rtac Iunity_closed 1);
+qed "zero_less_o_G";
+
+goal Sylow.thy "0 < m";
+by (res_inst_tac [("P","0 < p ^ a")] conjunct2 1);
+by (rtac (zero_less_mult_iff RS subst) 1);
+by (rtac (p3 RS subst) 1);
+by (rtac zero_less_o_G 1);
+qed "zero_less_m";
+
+goal Sylow.thy "card(calM) = ((p ^ a) * m choose p ^ a)";
+by (simp_tac
+ (simpset() addsimps [calM_def, p3 RS sym, order_eq, n_subsets, p4]) 1);
+qed "card_calM";
+
+Goal "0 < card calM";
+by (asm_full_simp_tac (simpset() addsimps [card_calM]) 1);
+by (rtac zero_less_binomial 1);
+by (rtac le_extend_mult 1);
+by (rtac le_refl 2);
+by (rtac zero_less_m 1);
+qed "zero_less_card_calM";
+
+Goal "~ (p ^ ((exponent p m)+ 1) dvd card(calM))";
+by (subgoal_tac "exponent p m = exponent p (card calM)" 1);
+ by (asm_full_simp_tac (simpset() addsimps [card_calM,
+ zero_less_m RS const_p_fac]) 2);
+by (cut_facts_tac [zero_less_card_calM, p1] 1);
+by (force_tac (claset() addDs [power_Suc_exponent_Not_dvd], simpset()) 1);
+qed "max_p_div_calM";
+
+goal Sylow.thy "finite calM";
+by (rtac finite_subset 1);
+by (rtac (finite_Pow_iff RS iffD2) 2);
+by (rtac p4 2);
+by (rtac subsetI 1);
+by (rtac PowI 1);
+by (SELECT_GOAL (rewtac calM_def) 1);
+by (dtac CollectD 1);
+by (etac conjunct1 1);
+qed "finite_calM";
+
+
+
+Goal "~(\\<forall> x\\<in>M. P x) ==> \\<exists>x\\<in>M. ~P x";
+by (blast_tac (claset() addIs []) 1);
+qed "Set_NotAll_ExNot";
+
+
+goal Sylow.thy "\\<exists>M. M\\<in>calM // RelM & ~(p ^ ((exponent p m)+ 1) dvd card(M))";
+by (fold_goals_tac [Bex_def]);
+by (rtac Set_NotAll_ExNot 1);
+by (rtac contrapos_nn 1);
+by (rtac max_p_div_calM 1);
+by (rtac (RelM_equiv RSN(2, equiv_imp_dvd_card)) 1);
+by (rtac finite_calM 1);
+by (assume_tac 1);
+qed "lemma_A1";
+
+val [q1,q2,q3,q4] = goal Sylow.thy "[| M\\<in>calM // RelM & ~(p ^ ((exponent p m)+ 1) dvd card(M));\
+\ M1\\<in>M; x\\<in>{g. g\\<in>carrier G & M1 #> g = M1}; xa\\<in>{g. g\\<in>carrier G & M1 #> g = M1}|]\
+\ ==> x ## xa\\<in>{g. g\\<in>carrier G & M1 #> g = M1}";
+val l1 = q3 RS CollectD RS conjunct2;
+val l2 = q4 RS CollectD RS conjunct2;
+val l3 = q3 RS CollectD RS conjunct1;
+val l4 = q4 RS CollectD RS conjunct1;
+by (rtac CollectI 1);
+by (rtac conjI 1);
+by (rtac Ibin_op_closed 1);
+by (rtac l3 1);
+by (rtac l4 1);
+by (rtac (Icoset_mul_assoc RS subst) 1);
+by (rtac l3 2);
+by (rtac l4 2);
+by (rtac (q2 RS (q1 RS M1_subset_G)) 1);
+by (stac l1 1);
+by (stac l2 1);
+by (rtac refl 1);
+qed "bin_op_closed_lemma";
+
+val [q1,q2] = goal Sylow.thy "[|M\\<in>calM // RelM & ~(p ^ ((exponent p m)+ 1) dvd card(M));\
+\ M1\\<in>M |] ==> {g. g\\<in>carrier G & M1 #> g = M1} <<= G";
+by (rtac IsubgroupI 1);
+by (rtac subsetI 1);
+by (etac subset_lemma1 1);
+by (rtac ExEl_NotEmpty 1);
+by (res_inst_tac [("x","e")] exI 1);
+by (rtac CollectI 1);
+by (rtac conjI 1);
+by (rtac Iunity_closed 1);
+by (rtac Icoset_mul_unity 1);
+by (rtac (q2 RS (q1 RS M1_subset_G)) 1);
+by (rtac ballI 1);
+by (rtac CollectI 1);
+by (dtac CollectD 1);
+by (rtac conjI 1);
+by (rtac Iinvers_closed 1);
+by (etac conjunct1 1);
+by (ftac conjunct2 1);
+by (eres_inst_tac [("P","%z. z #> inv x = M1")] subst 1);
+by (stac Icoset_mul_assoc 1);
+by (rtac (q2 RS (q1 RS M1_subset_G)) 1);
+by (etac conjunct1 1);
+by (rtac Iinvers_closed 1);
+by (etac conjunct1 1);
+by (stac Iinvers_ax1 1);
+by (etac conjunct1 1);
+by (rtac Icoset_mul_unity 1);
+by (rtac (q2 RS (q1 RS M1_subset_G)) 1);
+by (rtac ballI 1);
+by (rtac ballI 1);
+by (rtac (q2 RS( q1 RS bin_op_closed_lemma)) 1);
+by (assume_tac 1);
+by (assume_tac 1);
+qed "H_is_SG";
+
+val [q1,q2,q3] = goal Sylow.thy "[| M\\<in>calM // RelM & ~(p ^ ((exponent p m)+ 1) dvd card(M));\
+\ M1 \\<in> M; M2 \\<in> M|] ==> \\<exists>g \\<in> carrier G. M1 #> g = M2";
+val l1 = (q1 RS conjunct1) RS (RelM_equiv RS ElemClassEquiv);
+val l2 = q2 RS ((q3 RS (l1 RS bspec)) RS bspec);
+by (rtac bex_sym 1);
+by (res_inst_tac [("P","(M2, M1)\\<in>calM <*> calM")] conjunct2 1);
+by (res_inst_tac [("x","M2"),("y","M1")] CollectD_prod 1);
+by (fold_goals_tac [RelM_def]);
+by (rtac l2 1);
+qed "M_elem_map";
+
+val [q1,q2,q3] = goal Sylow.thy "[|M\\<in>calM // RelM & ~(p ^ ((exponent p m)+ 1) dvd card(M));\
+\ M1 \\<in> M; H\\<in>set_r_cos G {g. g\\<in>carrier G & M1 #> g = M1} |] ==>\
+\ \\<exists>g \\<in> carrier G. {g. g\\<in>carrier G & M1 #> g = M1} #> g = H";
+by (rtac bex_sym 1);
+by (res_inst_tac [("a","H")] CollectD 1);
+by (rewtac r_coset_abbr);
+by (fold_goals_tac [set_r_cos_def]);
+by (fold_goals_tac [r_coset_abbr]);
+by (rtac q3 1);
+qed "H_elem_map";
+
+val [q1,q2,q3,q4] = goal Sylow.thy "[| M\\<in>calM // RelM & ~(p ^ ((exponent p m)+ 1) dvd card(M));\
+\ M1 \\<in> M; g\\<in>carrier G; x\\<in>M1 #> g |] ==> x\\<in>carrier G";
+by (rtac (q4 RSN(2, mp)) 1);
+by (rtac impI 1);
+by (rewrite_goals_tac [r_coset_abbr,r_coset_def]);
+by (fold_goals_tac [bin_op_abbr]);
+by (dtac CollectD 1);
+by (etac bexE 1);
+by (etac subst 1);
+by (rtac Ibin_op_closed 1);
+by (rtac q3 2);
+by (etac (q2 RS( q1 RS M1_subset_G) RS subsetD) 1);
+qed "rcosetGM1g_subset_G";
+
+val [q1,q2] = goal Sylow.thy "[|M\\<in>calM // RelM & ~(p ^ ((exponent p m)+ 1) dvd card(M));\
+\ M1 \\<in> M|] ==> finite M1";
+by (rtac finite_subset 1);
+by (rtac (q2 RS (q1 RS M1_subset_G)) 1);
+by (rtac p4 1);
+qed "finite_M1";
+
+val [q1,q2,q3] = goal Sylow.thy "[|M\\<in>calM // RelM & ~(p ^ ((exponent p m)+ 1) dvd card(M));\
+\ M1 \\<in> M; g\\<in>carrier G|] ==> finite (M1 #> g)";
+by (rtac finite_subset 1);
+by (rtac subsetI 1);
+by (etac (q3 RS( q2 RS (q1 RS rcosetGM1g_subset_G))) 1);
+by (rtac p4 1);
+qed "finite_rcosetGM1g";
+
+val [q1,q2,q3] = goal Sylow.thy "[| M\\<in>calM // RelM & ~(p ^ ((exponent p m)+ 1) dvd card(M));\
+\ M1 \\<in> M; g\\<in>carrier G|] ==> card(M1) = card(M1 #> g)";
+by (rewtac r_coset_abbr);
+by (rtac sym 1);
+by (rtac (p2 RS card_cosets_equal RS bspec) 1);
+by (rtac (q2 RS (q1 RS M1_subset_G)) 1);
+by (rtac p4 1);
+by (rewtac set_r_cos_def);
+by (Step_tac 1);
+by (rtac bexI 1);
+by (rtac refl 1);
+by (rtac q3 1);
+qed "M1_cardeq_rcosetGM1g";
+
+val [q1,q2,q3] = goal Sylow.thy "[| M\\<in>calM // RelM & ~(p ^ ((exponent p m)+ 1) dvd card(M));\
+\ M1 \\<in> M; g\\<in>carrier G|] ==> (M1, M1 #> g)\\<in>RelM";
+val l1 = (q2 RS (q1 RS M1_subset_G));
+val l2 = q3 RS (q2 RS (q1 RS rcosetGM1g_subset_G));
+by (rewtac RelM_def);
+by (rtac CollectI_prod 1);
+by (rtac conjI 1);
+by (rtac SigmaI 1);
+by (SELECT_GOAL (rewtac calM_def) 1);
+by (rtac CollectI 1);
+by (rtac conjI 1);
+by (rtac (q2 RS (q1 RS card_M1)) 2);
+by (rtac l1 1);
+
+by (rewtac calM_def);
+by (rtac CollectI 1);
+by (rtac conjI 1);
+by (rtac (q3 RS (q2 RS (q1 RS M1_cardeq_rcosetGM1g)) RS subst) 2);
+by (rtac (q2 RS (q1 RS card_M1)) 2);
+by (rtac subsetI 1);
+by (etac l2 1);
+by (res_inst_tac [("x","inv g")] bexI 1);
+by (stac Icoset_mul_assoc 1);
+by (rtac l1 1);
+by (rtac q3 1);
+by (rtac (q3 RS Iinvers_closed) 1);
+by (stac Iinvers_ax1 1);
+by (rtac q3 1);
+by (rtac (Icoset_mul_unity RS sym) 1);
+by (rtac l1 1);
+by (rtac (q3 RS Iinvers_closed) 1);
+qed "M1_RelM_rcosetGM1g";
+
+val [q1,q2] = goal Sylow.thy "[| M\\<in>calM // RelM & ~(p ^ ((exponent p m)+ 1) dvd card(M));\
+\ M1\\<in>M|] ==> (\\<exists>f \\<in> M -> set_r_cos G {g. g\\<in>carrier G & M1 #> g = M1}. inj_on f M )\
+\ & (\\<exists>g \\<in> (set_r_cos G {g. g\\<in>carrier G & M1 #> g = M1}) -> M. \
+\ inj_on g (set_r_cos G {g. g\\<in>carrier G & M1 #> g = M1}))";
+by (rtac conjI 1);
+by (res_inst_tac
+[("x","% M. {g. g\\<in>carrier G & M1 #> g = M1} #> (@ g. g\\<in>carrier G & M1 #> g = M)")]
+bexI 1);
+by (SELECT_GOAL (rewtac funcset_def) 2);
+by (rtac CollectI 2);
+by (rtac ballI 2);
+by (SELECT_GOAL (rewtac set_r_cos_def) 2);
+by (fold_goals_tac [r_coset_abbr]);
+by (rtac CollectI 2);
+by (rtac bexI 2);
+by (rtac refl 2);
+val l1 = (q2 RS(q1 RS M_elem_map)) RS (Bex_def RS apply_def) RS (Ex_def RS apply_def);
+by (rtac (l1 RS conjunct1) 2);
+by (assume_tac 2);
+by (rtac inj_onI 1);
+by (rtac ((l1 RS conjunct2) RS subst) 1);
+by (assume_tac 1);
+by (res_inst_tac [("P","% z. z = M1 #> (@ x. x\\<in>carrier G & M1 #> x = y)")] subst 1);
+by (rtac (l1 RS conjunct2) 1);
+by (assume_tac 1);
+by (rtac Icoset_mul_invers1 1);
+by (etac (l1 RS conjunct1) 1);
+by (etac (l1 RS conjunct1) 1);
+by (rtac (q2 RS (q1 RS M1_subset_G)) 1);
+by (res_inst_tac
+[("P","(@ xa. xa\\<in>carrier G & M1 #> xa = x) ## (inv (@ x. x\\<in>carrier G & M1 #> x = y))\\<in>carrier G")]
+conjunct2 1);
+by (res_inst_tac
+[("a","(@ xa. xa\\<in>carrier G & M1 #> xa = x) ## (inv (@ x. x\\<in>carrier G & M1 #> x = y))")]
+CollectD 1);
+by (rtac (H_is_SG RSN(2, Icoset_join1)) 1);
+by (rtac Ibin_op_closed 1);
+by (etac (l1 RS conjunct1) 1);
+by (rtac Iinvers_closed 1);
+by (etac (l1 RS conjunct1) 1);
+by (rtac q1 1);
+by (rtac q2 1);
+by (rtac Icoset_mul_invers2 1);
+by (etac (l1 RS conjunct1) 1);
+by (etac (l1 RS conjunct1) 1);
+by (rtac subsetI 1);
+by (dtac CollectD 1);
+by (etac conjunct1 1);
+by (assume_tac 1);
+by (res_inst_tac [("x","% C. M1 #> (@g. g\\<in>carrier G &\
+\ {g. g \\<in> carrier G & M1 #> g = M1} #> g = C)")] bexI 1);
+by (rewtac funcset_def);
+by (rtac CollectI 2);
+by (rtac ballI 2);
+by (rtac ((q2 RS (q1 RS M1_RelM_rcosetGM1g)) RSN (4, EquivElemClass)) 2);
+by (rtac RelM_equiv 2);
+by (rtac (q1 RS conjunct1) 2);
+by (rtac q2 2);
+by (SELECT_GOAL (rewtac set_r_cos_def) 2);
+by (dtac CollectD 2);
+by (dtac bex_sym 2);
+by (fold_goals_tac [r_coset_abbr]);
+by (rewrite_goals_tac [Bex_def,Ex_def]);
+by (etac conjunct1 2);
+by (rtac inj_onI 1);
+val l1 = (q2 RS (q1 RS H_elem_map)) RS (Bex_def RS apply_def) RS (Ex_def RS apply_def);
+by (rtac (l1 RS conjunct2 RS subst) 1);
+by (assume_tac 1);
+by (res_inst_tac [("t","x")] (l1 RS conjunct2 RS subst) 1);
+by (assume_tac 1);
+by (rtac Icoset_mul_invers1 1);
+by (etac (l1 RS conjunct1) 1);
+by (etac (l1 RS conjunct1) 1);
+val l2 = (q2 RS (q1 RS H_is_SG));
+by (rtac (l2 RS (subgroup_def RS apply_def) RS conjunct1) 1);
+by (rtac Icoset_join2 1);
+by (rtac Ibin_op_closed 1);
+by (etac (l1 RS conjunct1) 1);
+by (rtac Iinvers_closed 1);
+by (etac (l1 RS conjunct1) 1);
+by (rtac l2 1);
+by (rtac CollectI 1);
+by (rtac conjI 1);
+by (rtac Ibin_op_closed 1);
+by (etac (l1 RS conjunct1) 1);
+by (rtac Iinvers_closed 1);
+by (etac (l1 RS conjunct1) 1);
+by (rtac Icoset_mul_invers2 1);
+by (assume_tac 4);
+by (etac (l1 RS conjunct1) 1);
+by (etac (l1 RS conjunct1) 1);
+by (rtac (q2 RS (q1 RS M1_subset_G)) 1);
+qed "bij_M_GmodH";
+
+goal Sylow.thy "calM <= Pow(carrier G)";
+by (rtac subsetI 1);
+by (rtac PowI 1);
+by (rewtac calM_def);
+by (dtac CollectD 1);
+by (etac conjunct1 1);
+qed "calM_subset_PowG";
+
+val [q1] = goal Sylow.thy "M\\<in>calM // RelM & ~(p ^ ((exponent p m)+ 1) dvd card(M)) ==> finite M";
+by (rtac finite_subset 1);
+by (rtac (q1 RS M_subset_calM RS subset_trans) 1);
+by (rtac calM_subset_PowG 1);
+by (rtac (p4 RS (finite_Pow_iff RS iffD2)) 1);
+qed "finite_M";
+
+val [q1,q2] = goal Sylow.thy "[| M\\<in>calM // RelM & ~(p ^ ((exponent p m)+ 1) dvd card(M));\
+\ M1\\<in>M|] ==> card(M) = card(set_r_cos G {g. g\\<in>carrier G & M1 #> g = M1})";
+by (rtac card_bij 1);
+by (rtac (q1 RS finite_M) 1);
+by (rtac finite_subset 1);
+by (rtac (p2 RS set_r_cos_subset_PowG) 1);
+by (rtac (q2 RS( q1 RS H_is_SG)) 1);
+by (rtac (p4 RS (finite_Pow_iff RS iffD2)) 1);
+val l1 = (q2 RS (q1 RS bij_M_GmodH));
+by (rtac (l1 RS conjunct1) 1);
+by (rtac (l1 RS conjunct2) 1);
+qed "cardMeqIndexH";
+
+val [q1,q2] = goal Sylow.thy "[| M\\<in>calM // RelM & ~(p ^ ((exponent p m)+ 1) dvd card(M));\
+\ M1\\<in>M|] ==> (card(M) * card({g. g\\<in>carrier G & M1 #> g = M1})) = order(G)";
+by (rtac ((q2 RS( q1 RS cardMeqIndexH)) RS ssubst) 1);
+by (rtac Lagrange 1);
+by (rtac p2 1);
+by (rtac p4 1);
+by (rtac (q2 RS (q1 RS H_is_SG)) 1);
+qed "index_lem";
+
+val [q1,q2] = goal Sylow.thy
+ "[| M\\<in>calM // RelM & ~(p ^ ((exponent p m)+ 1) dvd card(M));\
+\ M1\\<in>M |] \
+\ ==> p ^ a <= card({g. g\\<in>carrier G & M1 #> g = M1})";
+by (rtac dvd_imp_le 1);
+by (res_inst_tac [("r","exponent p m"),("n", "card(M)")] div_combine 1);
+by (rtac p1 1);
+by (rtac SG_card1 3);
+by (rtac p2 3);
+by (rtac p4 3);
+by (rtac (q2 RS (q1 RS H_is_SG)) 3);
+by (rtac (q1 RS conjunct2) 1);
+by (rtac (q2 RS (q1 RS index_lem) RS ssubst) 1);
+by (stac p3 1);
+by (stac power_add 1);
+by (rtac mult_dvd_mono 1);
+by (rtac dvd_refl 1);
+by (rtac power_exponent_dvd 1);
+by (rtac zero_less_m 1);
+qed "lemma_leq1";
+
+val [q1,q2] = goal Sylow.thy "[| M\\<in>calM // RelM & ~(p ^ ((exponent p m)+ 1) dvd card(M));\
+\ M1\\<in>M |] ==> card({g. g\\<in>carrier G & M1 #> g = M1}) <= p ^ a";
+by (rtac (q2 RS (q1 RS card_M1) RS subst) 1);
+by (rtac bexE 1);
+by (rtac (q2 RS (q1 RS M1_inj_H)) 1);
+by (rtac card_inj 1);
+by (assume_tac 3);
+by (assume_tac 3);
+by (rtac finite_subset 2);
+by (rtac p4 3);
+by (rtac (q2 RS (q1 RS M1_subset_G)) 2);
+by (rtac finite_subset 1);
+by (rtac p4 2);
+by (rtac subsetI 1);
+by (etac subset_lemma1 1);
+qed "lemma_leq2";
+
+val [q1,q2] = goal Sylow.thy "[| M\\<in>calM // RelM & ~(p ^ ((exponent p m)+ 1) dvd card(M));\
+\ M1\\<in>M|] ==> {g. g\\<in>carrier G & M1 #> g = M1} <<= G & \
+\ card({g. g\\<in>carrier G & M1 #> g = M1}) = p ^ a";
+by (rtac conjI 1);
+by (rtac le_anti_sym 2);
+by (rtac (q2 RS( q1 RS H_is_SG)) 1);
+by (rtac (q2 RS( q1 RS lemma_leq2)) 1);
+by (rtac (q2 RS( q1 RS lemma_leq1)) 1);
+qed "main_proof";
+
+goal Sylow.thy "\\<exists>H. H <<= G & card(H) = p ^ a";
+by (rtac exE 1);
+by (rtac lemma_A1 1);
+by (rtac exE 1);
+by (etac existsM1inM 1);
+by (dtac main_proof 1);
+by (assume_tac 1);
+by (etac exI 1);
+qed "Sylow1";
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/GroupTheory/Sylow.thy Sun Jun 10 08:03:35 2001 +0200
@@ -0,0 +1,45 @@
+(* Title: HOL/GroupTheory/Group
+ ID: $Id$
+ Author: Florian Kammueller, with new proofs by L C Paulson
+ Copyright 2001 University of Cambridge
+*)
+
+(* Theory file for the proof of Sylow's theorem. F. Kammueller 11.10.96
+Step 1: Use two separate .thy files for groups and Sylow's thm, respectively:
+
+I.e. here are the definitions which are specific for Sylow's theorem.
+*)
+
+Sylow = Group +
+
+types i
+arities i::term
+
+consts
+ G :: "i set * ([i, i] => i) * (i => i) * i"
+(* overloading for the carrier of G does not work because "duplicate declaration" : G :: "i set" *)
+ p, a, m :: "nat"
+ r_cos :: "[i set, i] => i set" ("_ #> _" [60,61]60)
+ "##" :: "[i, i] => i" (infixl 60)
+
+ (* coset and bin_op short forms *)
+defs
+ r_coset_abbr "H #> x == r_coset G H x"
+ bin_op_abbr "x ## y == bin_op G x y"
+
+constdefs
+ e :: "i" "e == unity G"
+ inv :: "i => i" "inv == invers G"
+ calM :: "i set set"
+ "calM == {s. s <= carrier(G) & card(s) = (p ^ a)}"
+ RelM :: "(i set * i set)set"
+ "RelM == {(N1,N2).(N1,N2): calM <*> calM & (? g: carrier(G). N1 = (N2 #> g) )}"
+
+rules
+(* specific rules modeling the section mechanism *)
+p1 "p : prime"
+p2 "G : Group"
+p3 "order(G) = (p ^ a) * m"
+p4 "finite (carrier G)"
+
+end
--- a/src/HOL/IsaMakefile Sat Jun 09 14:22:08 2001 +0200
+++ b/src/HOL/IsaMakefile Sun Jun 10 08:03:35 2001 +0200
@@ -18,6 +18,7 @@
HOL-CTL \
HOL-Real-HahnBanach \
HOL-Real-ex \
+ HOL-GroupTheory \
HOL-Hoare \
HOL-IMP \
HOL-IMPP \
@@ -251,6 +252,18 @@
@$(ISATOOL) usedir $(OUT)/HOL NumberTheory
+## HOL-GroupTheory
+
+HOL-GroupTheory: HOL $(LOG)/HOL-GroupTheory.gz
+
+$(LOG)/HOL-GroupTheory.gz: $(OUT)/HOL \
+ Library/Primes.thy \
+ GroupTheory/Exponent.thy GroupTheory/Exponent.ML GroupTheory/Group.thy\
+ GroupTheory/Group.ML GroupTheory/Sylow.thy GroupTheory/Sylow.ML\
+ GroupTheory/ROOT.ML
+ @$(ISATOOL) usedir $(OUT)/HOL GroupTheory
+
+
## HOL-Hoare
HOL-Hoare: HOL $(LOG)/HOL-Hoare.gz