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.73
1.74 @@ -268,7 +267,7 @@
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);
```