new material from the Sylow proof

--- a/src/HOL/Divides.ML	Sat Jun 09 08:42:06 2001 +0200
+++ b/src/HOL/Divides.ML	Sat Jun 09 08:42:29 2001 +0200
@@ -505,6 +505,10 @@
 (** Divides Relation                           **)
 (************************************************)
 
+Goalw [dvd_def] "!!P. [|m dvd n;  !!k. n = m*k ==> P|] ==> P";
+by (Blast_tac 1); 
+qed "dvdE";
+
 Goalw [dvd_def] "m dvd (0::nat)";
 by (blast_tac (claset() addIs [mult_0_right RS sym]) 1);
 qed "dvd_0_right";
@@ -519,6 +523,11 @@
 qed "dvd_1_left";
 AddIffs [dvd_1_left];
 
+Goal "(m dvd 1) = (m = 1)";
+by (simp_tac (simpset() addsimps [dvd_def]) 1); 
+qed "dvd_1_iff_1";
+Addsimps [dvd_1_iff_1];
+
 Goalw [dvd_def] "m dvd (m::nat)";
 by (blast_tac (claset() addIs [mult_1_right RS sym]) 1);
 qed "dvd_refl";
@@ -546,6 +555,11 @@
 by (blast_tac (claset() addIs [dvd_add]) 1);
 qed "dvd_diffD";
 
+Goal "[| k dvd m-n; k dvd m; n<=m |] ==> k dvd (n::nat)";
+by (dres_inst_tac [("m","m")] dvd_diff 1);
+by Auto_tac;  
+qed "dvd_diffD1";
+
 Goalw [dvd_def] "k dvd n ==> k dvd (m*n :: nat)";
 by (blast_tac (claset() addIs [mult_left_commute]) 1);
 qed "dvd_mult";

--- a/src/HOL/Power.ML	Sat Jun 09 08:42:06 2001 +0200
+++ b/src/HOL/Power.ML	Sat Jun 09 08:42:29 2001 +0200
@@ -25,6 +25,11 @@
 qed "zero_less_power";
 Addsimps [zero_less_power];
 
+Goal "i^n = 0 ==> i = (0::nat)";
+by (etac contrapos_pp 1); 
+by Auto_tac;  
+qed "power_eq_0D";
+
 Goal "!!i::nat. 1 <= i ==> 1 <= i^n";
 by (induct_tac "n" 1);
 by Auto_tac;
@@ -44,6 +49,17 @@
 by (asm_simp_tac (simpset() addsimps [power_add]) 1);
 qed "le_imp_power_dvd";
 
+Goal "1 < i ==> \\<forall>n. i ^ m <= i ^ n --> m <= n";
+by (induct_tac "m" 1);
+by Auto_tac;  
+by (case_tac "na" 1); 
+by Auto_tac;
+by (subgoal_tac "2 * 1 <= i * i^n" 1);
+by (Asm_full_simp_tac 1); 
+by (rtac mult_le_mono 1);
+by Auto_tac;   
+qed_spec_mp "power_le_imp_le";
+
 Goal "!!i::nat. [| 0 < i; i^m < i^n |] ==> m < n";
 by (rtac ccontr 1);
 by (dtac (leI RS le_imp_power_dvd RS dvd_imp_le RS leD) 1);
@@ -57,6 +73,14 @@
 by (blast_tac (claset() addSDs [dvd_mult_right]) 1);
 qed_spec_mp "power_le_dvd";
 
+Goal "[|i^m dvd i^n;  1 < i|] ==> m <= n";
+by (rtac power_le_imp_le 1); 
+by (assume_tac 1); 
+by (etac dvd_imp_le 1); 
+by (Asm_full_simp_tac 1); 
+qed "power_dvd_imp_le";
+
+
 
 (*** Binomial Coefficients, following Andy Gordon and Florian Kammueller ***)
 
@@ -107,6 +131,17 @@
 by (ALLGOALS Asm_simp_tac);
 qed_spec_mp "zero_less_binomial";
 
+Goal "(n choose k = 0) = (n<k)";
+by (safe_tac (claset() addSIs [binomial_eq_0]));
+by (etac contrapos_pp 1);
+by (asm_full_simp_tac (simpset() addsimps [zero_less_binomial]) 1); 
+qed "binomial_eq_0_iff";
+
+Goal "(0 < n choose k) = (k<=n)";
+by (simp_tac (simpset() addsimps [linorder_not_less RS sym, 
+                                  binomial_eq_0_iff RS sym]) 1); 
+qed "zero_less_binomial_iff";
+
 (*Might be more useful if re-oriented*)
 Goal "ALL k. k <= n --> Suc n * (n choose k) = (Suc n choose Suc k) * Suc k";
 by (induct_tac "n" 1);
@@ -118,9 +153,18 @@
 				  le_Suc_eq, binomial_eq_0]));
 qed_spec_mp "Suc_times_binomial_eq";
 
+(*This is the well-known version, but it's harder to use because of the
+  need to reason about division.*)
 Goal "k <= n ==> (Suc n choose Suc k) = (Suc n * (n choose k)) div Suc k";
 by (asm_simp_tac
     (simpset_of NatDef.thy addsimps [Suc_times_binomial_eq, 
 				  div_mult_self_is_m]) 1);
 qed "binomial_Suc_Suc_eq_times";
 
+(*Another version, with -1 instead of Suc.*)
+Goal "[|k <= n;  0<k|] ==> (n choose k) * k = n * ((n-1) choose (k-1))";
+by (cut_inst_tac [("n","n-1"),("k","k-1")] Suc_times_binomial_eq 1);
+by (asm_full_simp_tac (simpset() addsplits [nat_diff_split]) 1); 
+by Auto_tac;  
+qed "times_binomial_minus1_eq";
+