src/HOL/GroupTheory/Exponent.ML
changeset 11468 02cd5d5bc497
parent 11394 e88c2c89f98e
child 11506 244a02a2968b
     1.1 --- a/src/HOL/GroupTheory/Exponent.ML	Mon Aug 06 16:43:40 2001 +0200
     1.2 +++ b/src/HOL/GroupTheory/Exponent.ML	Tue Aug 07 16:36:52 2001 +0200
     1.3 @@ -8,11 +8,11 @@
     1.4  
     1.5  val prime_def = thm "prime_def";
     1.6  
     1.7 -Goalw [prime_def] "p\\<in>prime ==> 1 < p";
     1.8 -by (Blast_tac 1); 
     1.9 +Goalw [prime_def] "p\\<in>prime ==> 1' < p";
    1.10 +by (force_tac (claset(), simpset() addsimps []) 1); 
    1.11  qed "prime_imp_one_less";
    1.12  
    1.13 -Goal "(p\\<in>prime) = (1<p & (\\<forall>a b. p dvd a*b --> (p dvd a) | (p dvd b)))";
    1.14 +Goal "(p\\<in>prime) = (1'<p & (\\<forall>a b. p dvd a*b --> (p dvd a) | (p dvd b)))";
    1.15  by (auto_tac (claset(), simpset() addsimps [prime_imp_one_less]));  
    1.16  by (blast_tac (claset() addSDs [thm "prime_dvd_mult"]) 1);
    1.17  by (auto_tac (claset(), simpset() addsimps [prime_def]));  
    1.18 @@ -23,6 +23,7 @@
    1.19  by (dres_inst_tac [("x","k")] spec 1);
    1.20  by (asm_full_simp_tac
    1.21      (simpset() addsimps [dvd_mult_cancel1, dvd_mult_cancel2]) 1);  
    1.22 +by Auto_tac; 
    1.23  qed "prime_iff";
    1.24  
    1.25  Goal "p\\<in>prime ==> 0 < p^a";
    1.26 @@ -106,9 +107,7 @@
    1.27  by (res_inst_tac [("P","%x. x <= b * c")] subst 1);
    1.28  by (rtac mult_1_right 1);
    1.29  by (rtac mult_le_mono 1);
    1.30 -by (assume_tac 1);
    1.31 -by (stac Suc_le_eq 1);
    1.32 -by (assume_tac 1);
    1.33 +by Auto_tac; 
    1.34  qed "le_extend_mult";
    1.35  
    1.36  
    1.37 @@ -194,15 +193,15 @@
    1.38  qed_spec_mp "prime_power_dvd_cases";
    1.39  
    1.40  (*needed in this form in Sylow.ML*)
    1.41 -Goal "[| p\\<in>prime; ~(p ^ (r+1) dvd n); p ^ (a+r) dvd n * k |] \
    1.42 +Goal "[| p \\<in> prime; ~ (p ^ (Suc r) dvd n);  p^(a+r) dvd n*k |] \
    1.43  \     ==> p ^ a dvd k";
    1.44 -by (dres_inst_tac [("a","r+1"), ("b","a")] prime_power_dvd_cases 1);
    1.45 +by (dres_inst_tac [("a","Suc r"), ("b","a")] prime_power_dvd_cases 1);
    1.46  by (assume_tac 1);  
    1.47  by Auto_tac;  
    1.48  qed "div_combine";
    1.49  
    1.50  (*Lemma for power_dvd_bound*)
    1.51 -Goal "1 < p ==> Suc n <= p^n";
    1.52 +Goal "1' < p ==> Suc n <= p^n";
    1.53  by (induct_tac "n" 1);
    1.54  by (Asm_simp_tac 1); 
    1.55  by (Asm_full_simp_tac 1); 
    1.56 @@ -219,7 +218,7 @@
    1.57  qed "Suc_le_power";
    1.58  
    1.59  (*An upper bound for the n such that p^n dvd a: needed for GREATEST to exist*)
    1.60 -Goal "[|p^n dvd a;  1 < p;  0 < a|] ==> n < a";
    1.61 +Goal "[|p^n dvd a;  1' < p;  0 < a|] ==> n < a";
    1.62  by (dtac dvd_imp_le 1); 
    1.63  by (dres_inst_tac [("n","n")] Suc_le_power 2); 
    1.64  by Auto_tac;  
    1.65 @@ -254,7 +253,7 @@
    1.66  by (asm_simp_tac (simpset() addsimps [exponent_def]) 1);
    1.67  by (rtac Greatest_equality 1); 
    1.68  by (Asm_full_simp_tac 1);
    1.69 -by (blast_tac (claset() addIs [prime_imp_one_less, power_dvd_imp_le]) 1); 
    1.70 +by (asm_simp_tac (simpset() addsimps [prime_imp_one_less, power_dvd_imp_le]) 1); 
    1.71  qed "exponent_power_eq";
    1.72  Addsimps [exponent_power_eq];
    1.73  
    1.74 @@ -268,7 +267,7 @@
    1.75  Addsimps [exponent_eq_0];
    1.76  
    1.77  
    1.78 -(* exponent_mult_add, easy inclusion.  Could weaken p\\<in>prime to 1<p *)
    1.79 +(* exponent_mult_add, easy inclusion.  Could weaken p\\<in>prime to 1'<p *)
    1.80  Goal "[| 0 < a; 0 < b |]  \
    1.81  \     ==> (exponent p a) + (exponent p b) <= exponent p (a * b)";
    1.82  by (case_tac "p \\<in> prime" 1);
    1.83 @@ -313,7 +312,7 @@
    1.84  by (auto_tac (claset() addDs [dvd_mult_left], simpset()));  
    1.85  qed "not_divides_exponent_0";
    1.86  
    1.87 -Goal "exponent p 1 = 0";
    1.88 +Goal "exponent p 1' = 0";
    1.89  by (case_tac "p \\<in> prime" 1);
    1.90  by (auto_tac (claset(), 
    1.91                simpset() addsimps [prime_iff, not_divides_exponent_0]));
    1.92 @@ -358,7 +357,7 @@
    1.93  
    1.94  
    1.95  Goal "[| 0 < (k::nat); k < p^a; 0 < p; (p^r) dvd (p^a) - k |] ==> r <= a";
    1.96 -by (res_inst_tac [("m","1")] p_fac_forw_lemma 1);
    1.97 +by (res_inst_tac [("m","1'")] p_fac_forw_lemma 1);
    1.98  by Auto_tac;
    1.99  qed "r_le_a_forw";
   1.100  
   1.101 @@ -423,7 +422,7 @@
   1.102  qed "p_not_div_choose";
   1.103  
   1.104  
   1.105 -Goal "0 < m ==> exponent p ((p^a * m - 1) choose (p^a - 1)) = 0";
   1.106 +Goal "0 < m ==> exponent p ((p^a * m - 1') choose (p^a - 1')) = 0";
   1.107  by (case_tac "p \\<in> prime" 1);
   1.108  by (Asm_simp_tac 2);
   1.109  by (forw_inst_tac [("a","a")] zero_less_prime_power 1);