sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
"num" syntax (still with "#"), Numeral0, Numeral1;
(* 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 (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 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 (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";