20 Goal "!!i::nat. i ^ (j*k) = (i^j) ^ k"; |
20 Goal "!!i::nat. i ^ (j*k) = (i^j) ^ k"; |
21 by (induct_tac "k" 1); |
21 by (induct_tac "k" 1); |
22 by (ALLGOALS (asm_simp_tac (simpset() addsimps [power_add]))); |
22 by (ALLGOALS (asm_simp_tac (simpset() addsimps [power_add]))); |
23 qed "power_mult"; |
23 qed "power_mult"; |
24 |
24 |
25 Goal "!! i. 0 < i ==> 0 < i^n"; |
25 Goal "0 < i ==> 0 < i^n"; |
26 by (induct_tac "n" 1); |
26 by (induct_tac "n" 1); |
27 by (ALLGOALS (asm_simp_tac (simpset() addsimps [zero_less_mult_iff]))); |
27 by (ALLGOALS (asm_simp_tac (simpset() addsimps [zero_less_mult_iff]))); |
28 qed "zero_less_power"; |
28 qed "zero_less_power"; |
29 |
29 |
30 Goalw [dvd_def] "!!m::nat. m<=n ==> i^m dvd i^n"; |
30 Goalw [dvd_def] "!!m::nat. m<=n ==> i^m dvd i^n"; |
31 by (etac (not_less_iff_le RS iffD2 RS add_diff_inverse RS subst) 1); |
31 by (etac (not_less_iff_le RS iffD2 RS add_diff_inverse RS subst) 1); |
32 by (asm_simp_tac (simpset() addsimps [power_add]) 1); |
32 by (asm_simp_tac (simpset() addsimps [power_add]) 1); |
33 by (Blast_tac 1); |
33 by (Blast_tac 1); |
34 qed "le_imp_power_dvd"; |
34 qed "le_imp_power_dvd"; |
35 |
35 |
36 Goal "!! i r. [| 0 < i; i^m < i^n |] ==> m<n"; |
36 Goal "[| 0 < i; i^m < i^n |] ==> m<n"; |
37 by (rtac ccontr 1); |
37 by (rtac ccontr 1); |
38 by (dtac (leI RS le_imp_power_dvd RS dvd_imp_le RS leD) 1); |
38 by (dtac (leI RS le_imp_power_dvd RS dvd_imp_le RS leD) 1); |
39 by (etac zero_less_power 1); |
39 by (etac zero_less_power 1); |
40 by (contr_tac 1); |
40 by (contr_tac 1); |
41 qed "power_less_imp_less"; |
41 qed "power_less_imp_less"; |
42 |
42 |
43 Goal "!!n. k^j dvd n --> i<j --> k^i dvd n"; |
43 Goal "k^j dvd n --> i<j --> k^i dvd n"; |
44 by (induct_tac "j" 1); |
44 by (induct_tac "j" 1); |
45 by (ALLGOALS (simp_tac (simpset() addsimps [less_Suc_eq]))); |
45 by (ALLGOALS (simp_tac (simpset() addsimps [less_Suc_eq]))); |
46 by (stac mult_commute 1); |
46 by (stac mult_commute 1); |
47 by (blast_tac (claset() addSDs [dvd_mult_left]) 1); |
47 by (blast_tac (claset() addSDs [dvd_mult_left]) 1); |
48 qed_spec_mp "power_less_dvd"; |
48 qed_spec_mp "power_less_dvd"; |