44 |
44 |
45 Goal "(r::real)^2 = r * r"; |
45 Goal "(r::real)^2 = r * r"; |
46 by (Simp_tac 1); |
46 by (Simp_tac 1); |
47 qed "realpow_two"; |
47 qed "realpow_two"; |
48 |
48 |
49 Goal "(#0::real) < r --> #0 <= r ^ n"; |
|
50 by (induct_tac "n" 1); |
|
51 by (auto_tac (claset() addDs [order_less_imp_le] |
|
52 addIs [rename_numerals real_le_mult_order], |
|
53 simpset())); |
|
54 qed_spec_mp "realpow_ge_zero"; |
|
55 |
|
56 Goal "(#0::real) < r --> #0 < r ^ n"; |
49 Goal "(#0::real) < r --> #0 < r ^ n"; |
57 by (induct_tac "n" 1); |
50 by (induct_tac "n" 1); |
58 by (auto_tac (claset() addIs [rename_numerals real_mult_order], |
51 by (auto_tac (claset() addIs [rename_numerals real_mult_order], |
59 simpset() addsimps [real_zero_less_one])); |
52 simpset() addsimps [real_zero_less_one])); |
60 qed_spec_mp "realpow_gt_zero"; |
53 qed_spec_mp "realpow_gt_zero"; |
61 |
54 |
62 Goal "(#0::real) <= r --> #0 <= r ^ n"; |
55 Goal "(#0::real) <= r --> #0 <= r ^ n"; |
63 by (induct_tac "n" 1); |
56 by (induct_tac "n" 1); |
64 by (auto_tac (claset() addIs [rename_numerals real_le_mult_order], |
57 by (auto_tac (claset(), simpset() addsimps [real_0_le_mult_iff])); |
65 simpset())); |
58 qed_spec_mp "realpow_ge_zero"; |
66 qed_spec_mp "realpow_ge_zero2"; |
59 |
67 |
60 Goal "(#0::real) <= x & x <= y --> x ^ n <= y ^ n"; |
68 Goal "(#0::real) < x & x <= y --> x ^ n <= y ^ n"; |
61 by (induct_tac "n" 1); |
69 by (induct_tac "n" 1); |
62 by (auto_tac (claset() addSIs [real_mult_le_mono], simpset())); |
70 by (auto_tac (claset() addSIs [real_mult_le_mono], |
|
71 simpset())); |
|
72 by (asm_simp_tac (simpset() addsimps [realpow_ge_zero]) 1); |
63 by (asm_simp_tac (simpset() addsimps [realpow_ge_zero]) 1); |
73 qed_spec_mp "realpow_le"; |
64 qed_spec_mp "realpow_le"; |
74 |
|
75 Goal "(#0::real) <= x & x <= y --> x ^ n <= y ^ n"; |
|
76 by (induct_tac "n" 1); |
|
77 by (auto_tac (claset() addSIs [real_mult_le_mono4], |
|
78 simpset())); |
|
79 by (asm_simp_tac (simpset() addsimps [realpow_ge_zero2]) 1); |
|
80 qed_spec_mp "realpow_le2"; |
|
81 |
65 |
82 Goal "(#0::real) < x & x < y & 0 < n --> x ^ n < y ^ n"; |
66 Goal "(#0::real) < x & x < y & 0 < n --> x ^ n < y ^ n"; |
83 by (induct_tac "n" 1); |
67 by (induct_tac "n" 1); |
84 by (auto_tac (claset() addIs [rename_numerals real_mult_less_mono, gr0I] |
68 by (auto_tac (claset() addIs [rename_numerals real_mult_less_mono, gr0I] |
85 addDs [realpow_gt_zero], |
69 addDs [realpow_gt_zero], |
203 by Auto_tac; |
187 by Auto_tac; |
204 qed "realpow_Suc_le3"; |
188 qed "realpow_Suc_le3"; |
205 |
189 |
206 Goal "#0 <= r & r < (#1::real) & n < N --> r ^ N <= r ^ n"; |
190 Goal "#0 <= r & r < (#1::real) & n < N --> r ^ N <= r ^ n"; |
207 by (induct_tac "N" 1); |
191 by (induct_tac "N" 1); |
208 by Auto_tac; |
192 by (ALLGOALS Asm_simp_tac); |
209 by (ALLGOALS(forw_inst_tac [("n","na")] realpow_ge_zero2)); |
193 by (Clarify_tac 1); |
210 by (ALLGOALS(dtac (rename_numerals real_mult_le_mono3))); |
194 by (subgoal_tac "r * r ^ na <= #1 * r ^ n" 1); |
211 by (REPEAT(assume_tac 1)); |
195 by (Asm_full_simp_tac 1); |
212 by (REPEAT(assume_tac 3)); |
196 by (rtac real_mult_le_mono 1); |
213 by (auto_tac (claset(),simpset() addsimps |
197 by (auto_tac (claset(), simpset() addsimps [realpow_ge_zero, less_Suc_eq])); |
214 [less_Suc_eq])); |
|
215 qed_spec_mp "realpow_less_le"; |
198 qed_spec_mp "realpow_less_le"; |
216 |
199 |
217 Goal "[| #0 <= r; r < (#1::real); n <= N |] ==> r ^ N <= r ^ n"; |
200 Goal "[| #0 <= r; r < (#1::real); n <= N |] ==> r ^ N <= r ^ n"; |
218 by (dres_inst_tac [("n","N")] le_imp_less_or_eq 1); |
201 by (dres_inst_tac [("n","N")] le_imp_less_or_eq 1); |
219 by (auto_tac (claset() addIs [realpow_less_le], |
202 by (auto_tac (claset() addIs [realpow_less_le], |