src/HOL/GroupTheory/Exponent.ML

new theories from Jacques Fleuriot

(*  Title:      HOL/GroupTheory/Exponent
    ID:         $Id$
    Author:     Florian Kammueller, with new proofs by L C Paulson
    Copyright   2001  University of Cambridge
*)

(*** prime theorems ***)

val prime_def = thm "prime_def";

Goalw [prime_def] "p\\<in>prime ==> Suc 0 < p";
by (force_tac (claset(), simpset() addsimps []) 1); 
qed "prime_imp_one_less";

Goal "(p\\<in>prime) = (Suc 0 < 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);  
by Auto_tac; 
qed "prime_iff";

Goal "p\\<in>prime ==> 0 < p^a";
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 Auto_tac; 
qed "le_extend_mult";


Goal "0 < card(S) ==> S \\<noteq> {}";
by (force_tac (claset(), simpset() addsimps [card_empty]) 1); 
qed "card_nonempty";

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 ^ (Suc r) dvd n);  p^(a+r) dvd n*k |] \
\     ==> p ^ a dvd k";
by (dres_inst_tac [("a","Suc r"), ("b","a")] prime_power_dvd_cases 1);
by (assume_tac 1);  
by Auto_tac;  
qed "div_combine";

(*Lemma for power_dvd_bound*)
Goal "Suc 0 < 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;  Suc 0 < 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 (thm "Greatest_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")] (thm "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 (thm "Greatest_equality") 1); 
by (Asm_full_simp_tac 1);
by (asm_simp_tac (simpset() addsimps [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 Suc 0 < 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 (Suc 0) = 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","Suc 0")] 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 - Suc 0) choose (p^a - Suc 0)) = 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 (subgoal_tac "0 < p^a * m & p^a <= p^a * m" 1);
by (force_tac (claset(), simpset() addsimps [prime_iff]) 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_full_simp_tac (simpset() delsimps bad_Sucs
                         addsimps [exponent_mult_add, const_p_fac_right]) 1);
qed "const_p_fac";