author | paulson |
Sat, 27 Dec 2003 21:02:14 +0100 | |
changeset 14331 | 8dbbb7cf3637 |
parent 14305 | f17ca9f6dc8c |
child 14334 | 6137d24eef79 |
permissions | -rw-r--r-- |
10751 | 1 |
(* Title : HyperPow.ML |
2 |
Author : Jacques D. Fleuriot |
|
3 |
Copyright : 1998 University of Cambridge |
|
4 |
Description : Natural Powers of hyperreals theory |
|
5 |
||
10778
2c6605049646
more tidying, especially to remove real_of_posnat
paulson
parents:
10751
diff
changeset
|
6 |
Exponentials on the hyperreals |
10751 | 7 |
*) |
8 |
||
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11713
diff
changeset
|
9 |
Goal "(0::hypreal) ^ (Suc n) = 0"; |
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11713
diff
changeset
|
10 |
by Auto_tac; |
10751 | 11 |
qed "hrealpow_zero"; |
12 |
Addsimps [hrealpow_zero]; |
|
13 |
||
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11713
diff
changeset
|
14 |
Goal "r ~= (0::hypreal) --> r ^ n ~= 0"; |
10751 | 15 |
by (induct_tac "n" 1); |
16 |
by Auto_tac; |
|
17 |
qed_spec_mp "hrealpow_not_zero"; |
|
18 |
||
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11713
diff
changeset
|
19 |
Goal "r ~= (0::hypreal) --> inverse(r ^ n) = (inverse r) ^ n"; |
10751 | 20 |
by (induct_tac "n" 1); |
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11713
diff
changeset
|
21 |
by Auto_tac; |
10751 | 22 |
qed_spec_mp "hrealpow_inverse"; |
23 |
||
24 |
Goal "abs (r::hypreal) ^ n = abs (r ^ n)"; |
|
25 |
by (induct_tac "n" 1); |
|
26 |
by (auto_tac (claset(), simpset() addsimps [hrabs_mult])); |
|
27 |
qed "hrealpow_hrabs"; |
|
28 |
||
29 |
Goal "(r::hypreal) ^ (n + m) = (r ^ n) * (r ^ m)"; |
|
30 |
by (induct_tac "n" 1); |
|
14331 | 31 |
by (auto_tac (claset(), simpset() addsimps mult_ac)); |
10751 | 32 |
qed "hrealpow_add"; |
33 |
||
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
11468
diff
changeset
|
34 |
Goal "(r::hypreal) ^ Suc 0 = r"; |
10751 | 35 |
by (Simp_tac 1); |
36 |
qed "hrealpow_one"; |
|
37 |
Addsimps [hrealpow_one]; |
|
38 |
||
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
11468
diff
changeset
|
39 |
Goal "(r::hypreal) ^ Suc (Suc 0) = r * r"; |
10751 | 40 |
by (Simp_tac 1); |
41 |
qed "hrealpow_two"; |
|
42 |
||
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11713
diff
changeset
|
43 |
Goal "(0::hypreal) <= r --> 0 <= r ^ n"; |
10751 | 44 |
by (induct_tac "n" 1); |
14331 | 45 |
by (auto_tac (claset(), simpset() addsimps [zero_le_mult_iff])); |
10751 | 46 |
qed_spec_mp "hrealpow_ge_zero"; |
47 |
||
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11713
diff
changeset
|
48 |
Goal "(0::hypreal) < r --> 0 < r ^ n"; |
10751 | 49 |
by (induct_tac "n" 1); |
14331 | 50 |
by (auto_tac (claset(), simpset() addsimps [zero_less_mult_iff])); |
10751 | 51 |
qed_spec_mp "hrealpow_gt_zero"; |
52 |
||
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11713
diff
changeset
|
53 |
Goal "x <= y & (0::hypreal) < x --> x ^ n <= y ^ n"; |
10751 | 54 |
by (induct_tac "n" 1); |
55 |
by (auto_tac (claset() addSIs [hypreal_mult_le_mono], simpset())); |
|
56 |
by (asm_simp_tac (simpset() addsimps [hrealpow_ge_zero]) 1); |
|
57 |
qed_spec_mp "hrealpow_le"; |
|
58 |
||
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11713
diff
changeset
|
59 |
Goal "x < y & (0::hypreal) < x & 0 < n --> x ^ n < y ^ n"; |
10751 | 60 |
by (induct_tac "n" 1); |
61 |
by (auto_tac (claset() addIs [hypreal_mult_less_mono,gr0I], |
|
62 |
simpset() addsimps [hrealpow_gt_zero])); |
|
63 |
qed "hrealpow_less"; |
|
64 |
||
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11713
diff
changeset
|
65 |
Goal "1 ^ n = (1::hypreal)"; |
10751 | 66 |
by (induct_tac "n" 1); |
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11713
diff
changeset
|
67 |
by Auto_tac; |
10751 | 68 |
qed "hrealpow_eq_one"; |
69 |
Addsimps [hrealpow_eq_one]; |
|
70 |
||
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11713
diff
changeset
|
71 |
Goal "abs(-(1 ^ n)) = (1::hypreal)"; |
10751 | 72 |
by Auto_tac; |
73 |
qed "hrabs_minus_hrealpow_one"; |
|
74 |
Addsimps [hrabs_minus_hrealpow_one]; |
|
75 |
||
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11713
diff
changeset
|
76 |
Goal "abs(-1 ^ n) = (1::hypreal)"; |
10751 | 77 |
by (induct_tac "n" 1); |
78 |
by Auto_tac; |
|
79 |
qed "hrabs_hrealpow_minus_one"; |
|
80 |
Addsimps [hrabs_hrealpow_minus_one]; |
|
81 |
||
82 |
Goal "((r::hypreal) * s) ^ n = (r ^ n) * (s ^ n)"; |
|
83 |
by (induct_tac "n" 1); |
|
14331 | 84 |
by (auto_tac (claset(), simpset() addsimps mult_ac)); |
10751 | 85 |
qed "hrealpow_mult"; |
86 |
||
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11713
diff
changeset
|
87 |
Goal "(0::hypreal) <= r ^ Suc (Suc 0)"; |
14331 | 88 |
by (auto_tac (claset(), simpset() addsimps [zero_le_mult_iff])); |
10751 | 89 |
qed "hrealpow_two_le"; |
90 |
Addsimps [hrealpow_two_le]; |
|
91 |
||
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11713
diff
changeset
|
92 |
Goal "(0::hypreal) <= u ^ Suc (Suc 0) + v ^ Suc (Suc 0)"; |
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11713
diff
changeset
|
93 |
by (simp_tac (HOL_ss addsimps [hrealpow_two_le, hypreal_le_add_order]) 1); |
10751 | 94 |
qed "hrealpow_two_le_add_order"; |
95 |
Addsimps [hrealpow_two_le_add_order]; |
|
96 |
||
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11713
diff
changeset
|
97 |
Goal "(0::hypreal) <= u ^ Suc (Suc 0) + v ^ Suc (Suc 0) + w ^ Suc (Suc 0)"; |
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11713
diff
changeset
|
98 |
by (simp_tac (HOL_ss addsimps [hrealpow_two_le, hypreal_le_add_order]) 1); |
10751 | 99 |
qed "hrealpow_two_le_add_order2"; |
100 |
Addsimps [hrealpow_two_le_add_order2]; |
|
101 |
||
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11713
diff
changeset
|
102 |
Goal "[| 0 <= x; 0 <= y |] ==> (x+y = 0) = (x = 0 & y = (0::hypreal))"; |
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11713
diff
changeset
|
103 |
by (auto_tac (claset() addIs [order_antisym], simpset())); |
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11713
diff
changeset
|
104 |
qed "hypreal_add_nonneg_eq_0_iff"; |
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11713
diff
changeset
|
105 |
|
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11713
diff
changeset
|
106 |
Goal "(x*x + y*y + z*z = 0) = (x = 0 & y = 0 & z = (0::hypreal))"; |
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11713
diff
changeset
|
107 |
by (simp_tac (HOL_ss addsimps [hypreal_le_square, hypreal_le_add_order, |
14305
f17ca9f6dc8c
tidying first part of HyperArith0.ML, using generic lemmas
paulson
parents:
14299
diff
changeset
|
108 |
hypreal_add_nonneg_eq_0_iff]) 1); |
f17ca9f6dc8c
tidying first part of HyperArith0.ML, using generic lemmas
paulson
parents:
14299
diff
changeset
|
109 |
by Auto_tac; |
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11713
diff
changeset
|
110 |
qed "hypreal_three_squares_add_zero_iff"; |
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11713
diff
changeset
|
111 |
|
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11713
diff
changeset
|
112 |
Goal "(x ^ Suc (Suc 0) + y ^ Suc (Suc 0) + z ^ Suc (Suc 0) = (0::hypreal)) = (x = 0 & y = 0 & z = 0)"; |
10751 | 113 |
by (simp_tac (HOL_ss addsimps |
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11713
diff
changeset
|
114 |
[hypreal_three_squares_add_zero_iff, hrealpow_two]) 1); |
10751 | 115 |
qed "hrealpow_three_squares_add_zero_iff"; |
116 |
Addsimps [hrealpow_three_squares_add_zero_iff]; |
|
117 |
||
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
11468
diff
changeset
|
118 |
Goal "abs(x ^ Suc (Suc 0)) = (x::hypreal) ^ Suc (Suc 0)"; |
10751 | 119 |
by (auto_tac (claset(), |
14331 | 120 |
simpset() addsimps [hrabs_def, zero_le_mult_iff])); |
10751 | 121 |
qed "hrabs_hrealpow_two"; |
122 |
Addsimps [hrabs_hrealpow_two]; |
|
123 |
||
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
11468
diff
changeset
|
124 |
Goal "abs(x) ^ Suc (Suc 0) = (x::hypreal) ^ Suc (Suc 0)"; |
10751 | 125 |
by (simp_tac (simpset() addsimps [hrealpow_hrabs, hrabs_eqI1] |
126 |
delsimps [hpowr_Suc]) 1); |
|
127 |
qed "hrealpow_two_hrabs"; |
|
128 |
Addsimps [hrealpow_two_hrabs]; |
|
129 |
||
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11713
diff
changeset
|
130 |
Goal "(1::hypreal) < r ==> 1 < r ^ Suc (Suc 0)"; |
10751 | 131 |
by (auto_tac (claset(), simpset() addsimps [hrealpow_two])); |
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11713
diff
changeset
|
132 |
by (res_inst_tac [("y","1*1")] order_le_less_trans 1); |
10751 | 133 |
by (rtac hypreal_mult_less_mono 2); |
134 |
by Auto_tac; |
|
135 |
qed "hrealpow_two_gt_one"; |
|
136 |
||
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11713
diff
changeset
|
137 |
Goal "(1::hypreal) <= r ==> 1 <= r ^ Suc (Suc 0)"; |
10751 | 138 |
by (etac (order_le_imp_less_or_eq RS disjE) 1); |
139 |
by (etac (hrealpow_two_gt_one RS order_less_imp_le) 1); |
|
140 |
by Auto_tac; |
|
141 |
qed "hrealpow_two_ge_one"; |
|
142 |
||
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11713
diff
changeset
|
143 |
Goal "(1::hypreal) <= 2 ^ n"; |
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11713
diff
changeset
|
144 |
by (res_inst_tac [("y","1 ^ n")] order_trans 1); |
10751 | 145 |
by (rtac hrealpow_le 2); |
10778
2c6605049646
more tidying, especially to remove real_of_posnat
paulson
parents:
10751
diff
changeset
|
146 |
by Auto_tac; |
10751 | 147 |
qed "two_hrealpow_ge_one"; |
148 |
||
11704
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
149 |
Goal "hypreal_of_nat n < 2 ^ n"; |
10751 | 150 |
by (induct_tac "n" 1); |
151 |
by (auto_tac (claset(), |
|
14331 | 152 |
simpset() addsimps [hypreal_of_nat_Suc, left_distrib])); |
10751 | 153 |
by (cut_inst_tac [("n","n")] two_hrealpow_ge_one 1); |
154 |
by (arith_tac 1); |
|
155 |
qed "two_hrealpow_gt"; |
|
156 |
Addsimps [two_hrealpow_gt,two_hrealpow_ge_one]; |
|
157 |
||
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11713
diff
changeset
|
158 |
Goal "-1 ^ (2*n) = (1::hypreal)"; |
10751 | 159 |
by (induct_tac "n" 1); |
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11713
diff
changeset
|
160 |
by Auto_tac; |
10751 | 161 |
qed "hrealpow_minus_one"; |
162 |
||
11704
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
163 |
Goal "n+n = (2*n::nat)"; |
11377
0f16ad464c62
Simprocs for type "nat" no longer introduce numerals unless they are already
paulson
parents:
10919
diff
changeset
|
164 |
by Auto_tac; |
0f16ad464c62
Simprocs for type "nat" no longer introduce numerals unless they are already
paulson
parents:
10919
diff
changeset
|
165 |
qed "double_lemma"; |
0f16ad464c62
Simprocs for type "nat" no longer introduce numerals unless they are already
paulson
parents:
10919
diff
changeset
|
166 |
|
0f16ad464c62
Simprocs for type "nat" no longer introduce numerals unless they are already
paulson
parents:
10919
diff
changeset
|
167 |
(*ugh: need to get rid fo the n+n*) |
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11713
diff
changeset
|
168 |
Goal "-1 ^ (n + n) = (1::hypreal)"; |
11377
0f16ad464c62
Simprocs for type "nat" no longer introduce numerals unless they are already
paulson
parents:
10919
diff
changeset
|
169 |
by (auto_tac (claset(), |
0f16ad464c62
Simprocs for type "nat" no longer introduce numerals unless they are already
paulson
parents:
10919
diff
changeset
|
170 |
simpset() addsimps [double_lemma, hrealpow_minus_one])); |
10751 | 171 |
qed "hrealpow_minus_one2"; |
172 |
Addsimps [hrealpow_minus_one2]; |
|
173 |
||
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
11468
diff
changeset
|
174 |
Goal "(-(x::hypreal)) ^ Suc (Suc 0) = x ^ Suc (Suc 0)"; |
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11713
diff
changeset
|
175 |
by Auto_tac; |
10751 | 176 |
qed "hrealpow_minus_two"; |
177 |
Addsimps [hrealpow_minus_two]; |
|
178 |
||
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11713
diff
changeset
|
179 |
Goal "(0::hypreal) < r & r < 1 --> r ^ Suc n < r ^ n"; |
10751 | 180 |
by (induct_tac "n" 1); |
181 |
by (auto_tac (claset(), |
|
182 |
simpset() addsimps [hypreal_mult_less_mono2])); |
|
183 |
qed_spec_mp "hrealpow_Suc_less"; |
|
184 |
||
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11713
diff
changeset
|
185 |
Goal "(0::hypreal) <= r & r < 1 --> r ^ Suc n <= r ^ n"; |
10751 | 186 |
by (induct_tac "n" 1); |
187 |
by (auto_tac (claset() addIs [order_less_imp_le] |
|
188 |
addSDs [order_le_imp_less_or_eq,hrealpow_Suc_less], |
|
189 |
simpset() addsimps [hypreal_mult_less_mono2])); |
|
190 |
qed_spec_mp "hrealpow_Suc_le"; |
|
191 |
||
10834 | 192 |
Goal "Abs_hypreal(hyprel``{%n. X n}) ^ m = Abs_hypreal(hyprel``{%n. (X n) ^ m})"; |
10751 | 193 |
by (induct_tac "m" 1); |
194 |
by (auto_tac (claset(), |
|
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11713
diff
changeset
|
195 |
simpset() addsimps [hypreal_one_def, hypreal_mult])); |
10751 | 196 |
qed "hrealpow"; |
197 |
||
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
11468
diff
changeset
|
198 |
Goal "(x + (y::hypreal)) ^ Suc (Suc 0) = \ |
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
11468
diff
changeset
|
199 |
\ x ^ Suc (Suc 0) + y ^ Suc (Suc 0) + (hypreal_of_nat (Suc (Suc 0)))*x*y"; |
10778
2c6605049646
more tidying, especially to remove real_of_posnat
paulson
parents:
10751
diff
changeset
|
200 |
by (simp_tac (simpset() addsimps |
14331 | 201 |
[right_distrib, left_distrib, |
10778
2c6605049646
more tidying, especially to remove real_of_posnat
paulson
parents:
10751
diff
changeset
|
202 |
hypreal_of_nat_zero, hypreal_of_nat_Suc]) 1); |
10751 | 203 |
qed "hrealpow_sum_square_expand"; |
204 |
||
12613
279facb4253a
Literal arithmetic: raising numbers to powers (nat, int, real, hypreal)
paulson
parents:
12330
diff
changeset
|
205 |
|
279facb4253a
Literal arithmetic: raising numbers to powers (nat, int, real, hypreal)
paulson
parents:
12330
diff
changeset
|
206 |
(*** Literal arithmetic involving powers, type hypreal ***) |
279facb4253a
Literal arithmetic: raising numbers to powers (nat, int, real, hypreal)
paulson
parents:
12330
diff
changeset
|
207 |
|
279facb4253a
Literal arithmetic: raising numbers to powers (nat, int, real, hypreal)
paulson
parents:
12330
diff
changeset
|
208 |
Goal "hypreal_of_real (x ^ n) = hypreal_of_real x ^ n"; |
279facb4253a
Literal arithmetic: raising numbers to powers (nat, int, real, hypreal)
paulson
parents:
12330
diff
changeset
|
209 |
by (induct_tac "n" 1); |
279facb4253a
Literal arithmetic: raising numbers to powers (nat, int, real, hypreal)
paulson
parents:
12330
diff
changeset
|
210 |
by (ALLGOALS (asm_simp_tac (simpset() addsimps [nat_mult_distrib]))); |
279facb4253a
Literal arithmetic: raising numbers to powers (nat, int, real, hypreal)
paulson
parents:
12330
diff
changeset
|
211 |
qed "hypreal_of_real_power"; |
279facb4253a
Literal arithmetic: raising numbers to powers (nat, int, real, hypreal)
paulson
parents:
12330
diff
changeset
|
212 |
Addsimps [hypreal_of_real_power]; |
279facb4253a
Literal arithmetic: raising numbers to powers (nat, int, real, hypreal)
paulson
parents:
12330
diff
changeset
|
213 |
|
279facb4253a
Literal arithmetic: raising numbers to powers (nat, int, real, hypreal)
paulson
parents:
12330
diff
changeset
|
214 |
Goal "(number_of v :: hypreal) ^ n = hypreal_of_real ((number_of v) ^ n)"; |
279facb4253a
Literal arithmetic: raising numbers to powers (nat, int, real, hypreal)
paulson
parents:
12330
diff
changeset
|
215 |
by (simp_tac (HOL_ss addsimps [hypreal_number_of_def, |
279facb4253a
Literal arithmetic: raising numbers to powers (nat, int, real, hypreal)
paulson
parents:
12330
diff
changeset
|
216 |
hypreal_of_real_power]) 1); |
279facb4253a
Literal arithmetic: raising numbers to powers (nat, int, real, hypreal)
paulson
parents:
12330
diff
changeset
|
217 |
qed "power_hypreal_of_real_number_of"; |
279facb4253a
Literal arithmetic: raising numbers to powers (nat, int, real, hypreal)
paulson
parents:
12330
diff
changeset
|
218 |
|
279facb4253a
Literal arithmetic: raising numbers to powers (nat, int, real, hypreal)
paulson
parents:
12330
diff
changeset
|
219 |
Addsimps [inst "n" "number_of ?w" power_hypreal_of_real_number_of]; |
279facb4253a
Literal arithmetic: raising numbers to powers (nat, int, real, hypreal)
paulson
parents:
12330
diff
changeset
|
220 |
|
10751 | 221 |
(*--------------------------------------------------------------- |
222 |
we'll prove the following theorem by going down to the |
|
223 |
level of the ultrafilter and relying on the analogous |
|
224 |
property for the real rather than prove it directly |
|
225 |
using induction: proof is much simpler this way! |
|
226 |
---------------------------------------------------------------*) |
|
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11713
diff
changeset
|
227 |
Goal "[|(0::hypreal) <= x; 0 <= y;x ^ Suc n <= y ^ Suc n |] ==> x <= y"; |
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11713
diff
changeset
|
228 |
by (full_simp_tac (simpset() addsimps [hypreal_zero_def]) 1); |
10751 | 229 |
by (res_inst_tac [("z","x")] eq_Abs_hypreal 1); |
230 |
by (res_inst_tac [("z","y")] eq_Abs_hypreal 1); |
|
231 |
by (auto_tac (claset(), |
|
232 |
simpset() addsimps [hrealpow,hypreal_le,hypreal_mult])); |
|
233 |
by (ultra_tac (claset() addIs [realpow_increasing], simpset()) 1); |
|
234 |
qed "hrealpow_increasing"; |
|
235 |
||
236 |
(*By antisymmetry with the above we conclude x=y, replacing the deleted |
|
237 |
theorem hrealpow_Suc_cancel_eq*) |
|
238 |
||
239 |
Goal "x : HFinite --> x ^ n : HFinite"; |
|
240 |
by (induct_tac "n" 1); |
|
241 |
by (auto_tac (claset() addIs [HFinite_mult], simpset())); |
|
242 |
qed_spec_mp "hrealpow_HFinite"; |
|
243 |
||
244 |
(*--------------------------------------------------------------- |
|
245 |
Hypernaturals Powers |
|
246 |
--------------------------------------------------------------*) |
|
247 |
Goalw [congruent_def] |
|
248 |
"congruent hyprel \ |
|
10834 | 249 |
\ (%X Y. hyprel``{%n. ((X::nat=>real) n ^ (Y::nat=>nat) n)})"; |
14299 | 250 |
by (auto_tac (claset() addSIs [ext], simpset())); |
10751 | 251 |
by (ALLGOALS(Fuf_tac)); |
252 |
qed "hyperpow_congruent"; |
|
253 |
||
254 |
Goalw [hyperpow_def] |
|
10834 | 255 |
"Abs_hypreal(hyprel``{%n. X n}) pow Abs_hypnat(hypnatrel``{%n. Y n}) = \ |
256 |
\ Abs_hypreal(hyprel``{%n. X n ^ Y n})"; |
|
10751 | 257 |
by (res_inst_tac [("f","Abs_hypreal")] arg_cong 1); |
258 |
by (auto_tac (claset() addSIs [lemma_hyprel_refl,bexI], |
|
259 |
simpset() addsimps [hyprel_in_hypreal RS |
|
260 |
Abs_hypreal_inverse,equiv_hyprel,hyperpow_congruent])); |
|
261 |
by (Fuf_tac 1); |
|
262 |
qed "hyperpow"; |
|
263 |
||
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11713
diff
changeset
|
264 |
Goalw [hypnat_one_def] "(0::hypreal) pow (n + (1::hypnat)) = 0"; |
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11713
diff
changeset
|
265 |
by (simp_tac (simpset() addsimps [hypreal_zero_def]) 1); |
10751 | 266 |
by (res_inst_tac [("z","n")] eq_Abs_hypnat 1); |
267 |
by (auto_tac (claset(), simpset() addsimps [hyperpow,hypnat_add])); |
|
268 |
qed "hyperpow_zero"; |
|
269 |
Addsimps [hyperpow_zero]; |
|
270 |
||
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11713
diff
changeset
|
271 |
Goal "r ~= (0::hypreal) --> r pow n ~= 0"; |
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11713
diff
changeset
|
272 |
by (simp_tac (simpset() addsimps [hypreal_zero_def]) 1); |
10751 | 273 |
by (res_inst_tac [("z","n")] eq_Abs_hypnat 1); |
274 |
by (res_inst_tac [("z","r")] eq_Abs_hypreal 1); |
|
275 |
by (auto_tac (claset(), simpset() addsimps [hyperpow])); |
|
276 |
by (dtac FreeUltrafilterNat_Compl_mem 1); |
|
277 |
by (fuf_empty_tac (claset() addIs [realpow_not_zero RS notE], |
|
278 |
simpset()) 1); |
|
279 |
qed_spec_mp "hyperpow_not_zero"; |
|
280 |
||
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11713
diff
changeset
|
281 |
Goal "r ~= (0::hypreal) --> inverse(r pow n) = (inverse r) pow n"; |
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11713
diff
changeset
|
282 |
by (simp_tac (simpset() addsimps [hypreal_zero_def]) 1); |
10751 | 283 |
by (res_inst_tac [("z","n")] eq_Abs_hypnat 1); |
284 |
by (res_inst_tac [("z","r")] eq_Abs_hypreal 1); |
|
285 |
by (auto_tac (claset() addSDs [FreeUltrafilterNat_Compl_mem], |
|
286 |
simpset() addsimps [hypreal_inverse,hyperpow])); |
|
287 |
by (rtac FreeUltrafilterNat_subset 1); |
|
288 |
by (auto_tac (claset() addDs [realpow_not_zero] |
|
289 |
addIs [realpow_inverse], |
|
290 |
simpset())); |
|
291 |
qed "hyperpow_inverse"; |
|
292 |
||
293 |
Goal "abs r pow n = abs (r pow n)"; |
|
294 |
by (res_inst_tac [("z","n")] eq_Abs_hypnat 1); |
|
295 |
by (res_inst_tac [("z","r")] eq_Abs_hypreal 1); |
|
296 |
by (auto_tac (claset(), |
|
12330 | 297 |
simpset() addsimps [hypreal_hrabs, hyperpow,realpow_abs RS sym])); |
10751 | 298 |
qed "hyperpow_hrabs"; |
299 |
||
300 |
Goal "r pow (n + m) = (r pow n) * (r pow m)"; |
|
301 |
by (res_inst_tac [("z","n")] eq_Abs_hypnat 1); |
|
302 |
by (res_inst_tac [("z","m")] eq_Abs_hypnat 1); |
|
303 |
by (res_inst_tac [("z","r")] eq_Abs_hypreal 1); |
|
304 |
by (auto_tac (claset(), |
|
305 |
simpset() addsimps [hyperpow,hypnat_add, hypreal_mult,realpow_add])); |
|
306 |
qed "hyperpow_add"; |
|
307 |
||
11713
883d559b0b8c
sane numerals (stage 3): provide generic "1" on all number types;
wenzelm
parents:
11704
diff
changeset
|
308 |
Goalw [hypnat_one_def] "r pow (1::hypnat) = r"; |
10751 | 309 |
by (res_inst_tac [("z","r")] eq_Abs_hypreal 1); |
310 |
by (auto_tac (claset(), simpset() addsimps [hyperpow])); |
|
311 |
qed "hyperpow_one"; |
|
312 |
Addsimps [hyperpow_one]; |
|
313 |
||
314 |
Goalw [hypnat_one_def] |
|
11713
883d559b0b8c
sane numerals (stage 3): provide generic "1" on all number types;
wenzelm
parents:
11704
diff
changeset
|
315 |
"r pow ((1::hypnat) + (1::hypnat)) = r * r"; |
10751 | 316 |
by (res_inst_tac [("z","r")] eq_Abs_hypreal 1); |
317 |
by (auto_tac (claset(), |
|
10784 | 318 |
simpset() addsimps [hyperpow,hypnat_add, hypreal_mult])); |
10751 | 319 |
qed "hyperpow_two"; |
320 |
||
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11713
diff
changeset
|
321 |
Goal "(0::hypreal) < r --> 0 < r pow n"; |
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11713
diff
changeset
|
322 |
by (simp_tac (simpset() addsimps [hypreal_zero_def]) 1); |
10751 | 323 |
by (res_inst_tac [("z","n")] eq_Abs_hypnat 1); |
324 |
by (res_inst_tac [("z","r")] eq_Abs_hypreal 1); |
|
325 |
by (auto_tac (claset() addSEs [FreeUltrafilterNat_subset, realpow_gt_zero], |
|
326 |
simpset() addsimps [hyperpow,hypreal_less, hypreal_le])); |
|
327 |
qed_spec_mp "hyperpow_gt_zero"; |
|
328 |
||
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11713
diff
changeset
|
329 |
Goal "(0::hypreal) <= r --> 0 <= r pow n"; |
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11713
diff
changeset
|
330 |
by (simp_tac (simpset() addsimps [hypreal_zero_def]) 1); |
10751 | 331 |
by (res_inst_tac [("z","n")] eq_Abs_hypnat 1); |
332 |
by (res_inst_tac [("z","r")] eq_Abs_hypreal 1); |
|
10784 | 333 |
by (auto_tac (claset() addSEs [FreeUltrafilterNat_subset, realpow_ge_zero], |
10751 | 334 |
simpset() addsimps [hyperpow,hypreal_le])); |
10784 | 335 |
qed "hyperpow_ge_zero"; |
10751 | 336 |
|
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11713
diff
changeset
|
337 |
Goal "(0::hypreal) < x & x <= y --> x pow n <= y pow n"; |
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11713
diff
changeset
|
338 |
by (full_simp_tac (simpset() addsimps [hypreal_zero_def]) 1); |
10751 | 339 |
by (res_inst_tac [("z","n")] eq_Abs_hypnat 1); |
340 |
by (res_inst_tac [("z","x")] eq_Abs_hypreal 1); |
|
341 |
by (res_inst_tac [("z","y")] eq_Abs_hypreal 1); |
|
10784 | 342 |
by (auto_tac (claset(), |
343 |
simpset() addsimps [hyperpow,hypreal_le,hypreal_less])); |
|
344 |
by (etac (FreeUltrafilterNat_Int RS FreeUltrafilterNat_subset) 1 |
|
345 |
THEN assume_tac 1); |
|
346 |
by (auto_tac (claset() addIs [realpow_le], simpset())); |
|
10751 | 347 |
qed_spec_mp "hyperpow_le"; |
348 |
||
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11713
diff
changeset
|
349 |
Goal "1 pow n = (1::hypreal)"; |
10751 | 350 |
by (res_inst_tac [("z","n")] eq_Abs_hypnat 1); |
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11713
diff
changeset
|
351 |
by (auto_tac (claset(), simpset() addsimps [hypreal_one_def, hyperpow])); |
10751 | 352 |
qed "hyperpow_eq_one"; |
353 |
Addsimps [hyperpow_eq_one]; |
|
354 |
||
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11713
diff
changeset
|
355 |
Goal "abs(-(1 pow n)) = (1::hypreal)"; |
10751 | 356 |
by (res_inst_tac [("z","n")] eq_Abs_hypnat 1); |
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11713
diff
changeset
|
357 |
by (auto_tac (claset(), |
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11713
diff
changeset
|
358 |
simpset() addsimps [hyperpow, hypreal_hrabs, hypreal_one_def])); |
10751 | 359 |
qed "hrabs_minus_hyperpow_one"; |
360 |
Addsimps [hrabs_minus_hyperpow_one]; |
|
361 |
||
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11713
diff
changeset
|
362 |
Goal "abs(-1 pow n) = (1::hypreal)"; |
11713
883d559b0b8c
sane numerals (stage 3): provide generic "1" on all number types;
wenzelm
parents:
11704
diff
changeset
|
363 |
by (subgoal_tac "abs((- (1::hypreal)) pow n) = (1::hypreal)" 1); |
10751 | 364 |
by (Asm_full_simp_tac 1); |
365 |
by (res_inst_tac [("z","n")] eq_Abs_hypnat 1); |
|
366 |
by (auto_tac (claset(), |
|
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11713
diff
changeset
|
367 |
simpset() addsimps [hypreal_one_def, hyperpow,hypreal_minus, |
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11713
diff
changeset
|
368 |
hypreal_hrabs])); |
10751 | 369 |
qed "hrabs_hyperpow_minus_one"; |
370 |
Addsimps [hrabs_hyperpow_minus_one]; |
|
371 |
||
372 |
Goal "(r * s) pow n = (r pow n) * (s pow n)"; |
|
373 |
by (res_inst_tac [("z","n")] eq_Abs_hypnat 1); |
|
374 |
by (res_inst_tac [("z","r")] eq_Abs_hypreal 1); |
|
375 |
by (res_inst_tac [("z","s")] eq_Abs_hypreal 1); |
|
376 |
by (auto_tac (claset(), |
|
377 |
simpset() addsimps [hyperpow, hypreal_mult,realpow_mult])); |
|
378 |
qed "hyperpow_mult"; |
|
379 |
||
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11713
diff
changeset
|
380 |
Goal "(0::hypreal) <= r pow ((1::hypnat) + (1::hypnat))"; |
10751 | 381 |
by (auto_tac (claset(), |
14331 | 382 |
simpset() addsimps [hyperpow_two, zero_le_mult_iff])); |
10751 | 383 |
qed "hyperpow_two_le"; |
384 |
Addsimps [hyperpow_two_le]; |
|
385 |
||
11713
883d559b0b8c
sane numerals (stage 3): provide generic "1" on all number types;
wenzelm
parents:
11704
diff
changeset
|
386 |
Goal "abs(x pow ((1::hypnat) + (1::hypnat))) = x pow ((1::hypnat) + (1::hypnat))"; |
10751 | 387 |
by (simp_tac (simpset() addsimps [hrabs_eqI1]) 1); |
388 |
qed "hrabs_hyperpow_two"; |
|
389 |
Addsimps [hrabs_hyperpow_two]; |
|
390 |
||
11713
883d559b0b8c
sane numerals (stage 3): provide generic "1" on all number types;
wenzelm
parents:
11704
diff
changeset
|
391 |
Goal "abs(x) pow ((1::hypnat) + (1::hypnat)) = x pow ((1::hypnat) + (1::hypnat))"; |
10751 | 392 |
by (simp_tac (simpset() addsimps [hyperpow_hrabs,hrabs_eqI1]) 1); |
393 |
qed "hyperpow_two_hrabs"; |
|
394 |
Addsimps [hyperpow_two_hrabs]; |
|
395 |
||
396 |
(*? very similar to hrealpow_two_gt_one *) |
|
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11713
diff
changeset
|
397 |
Goal "(1::hypreal) < r ==> 1 < r pow ((1::hypnat) + (1::hypnat))"; |
10751 | 398 |
by (auto_tac (claset(), simpset() addsimps [hyperpow_two])); |
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11713
diff
changeset
|
399 |
by (res_inst_tac [("y","1*1")] order_le_less_trans 1); |
10751 | 400 |
by (rtac hypreal_mult_less_mono 2); |
401 |
by Auto_tac; |
|
402 |
qed "hyperpow_two_gt_one"; |
|
403 |
||
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11713
diff
changeset
|
404 |
Goal "(1::hypreal) <= r ==> 1 <= r pow ((1::hypnat) + (1::hypnat))"; |
10751 | 405 |
by (auto_tac (claset() addSDs [order_le_imp_less_or_eq] |
406 |
addIs [hyperpow_two_gt_one,order_less_imp_le], |
|
407 |
simpset())); |
|
408 |
qed "hyperpow_two_ge_one"; |
|
409 |
||
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11713
diff
changeset
|
410 |
Goal "(1::hypreal) <= 2 pow n"; |
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11713
diff
changeset
|
411 |
by (res_inst_tac [("y","1 pow n")] order_trans 1); |
10751 | 412 |
by (rtac hyperpow_le 2); |
10778
2c6605049646
more tidying, especially to remove real_of_posnat
paulson
parents:
10751
diff
changeset
|
413 |
by Auto_tac; |
10751 | 414 |
qed "two_hyperpow_ge_one"; |
415 |
Addsimps [two_hyperpow_ge_one]; |
|
416 |
||
417 |
Addsimps [simplify (simpset()) realpow_minus_one]; |
|
418 |
||
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11713
diff
changeset
|
419 |
Goal "-1 pow (((1::hypnat) + (1::hypnat))*n) = (1::hypreal)"; |
11713
883d559b0b8c
sane numerals (stage 3): provide generic "1" on all number types;
wenzelm
parents:
11704
diff
changeset
|
420 |
by (subgoal_tac "(-((1::hypreal))) pow (((1::hypnat) + (1::hypnat))*n) = (1::hypreal)" 1); |
10751 | 421 |
by (Asm_full_simp_tac 1); |
422 |
by (simp_tac (HOL_ss addsimps [hypreal_one_def]) 1); |
|
423 |
by (res_inst_tac [("z","n")] eq_Abs_hypnat 1); |
|
424 |
by (auto_tac (claset(), |
|
11377
0f16ad464c62
Simprocs for type "nat" no longer introduce numerals unless they are already
paulson
parents:
10919
diff
changeset
|
425 |
simpset() addsimps [double_lemma, hyperpow, hypnat_add, |
0f16ad464c62
Simprocs for type "nat" no longer introduce numerals unless they are already
paulson
parents:
10919
diff
changeset
|
426 |
hypreal_minus])); |
10751 | 427 |
qed "hyperpow_minus_one2"; |
428 |
Addsimps [hyperpow_minus_one2]; |
|
429 |
||
430 |
Goalw [hypnat_one_def] |
|
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11713
diff
changeset
|
431 |
"(0::hypreal) < r & r < 1 --> r pow (n + (1::hypnat)) < r pow n"; |
10751 | 432 |
by (res_inst_tac [("z","n")] eq_Abs_hypnat 1); |
433 |
by (res_inst_tac [("z","r")] eq_Abs_hypreal 1); |
|
434 |
by (auto_tac (claset() addSDs [conjI RS realpow_Suc_less] |
|
435 |
addEs [FreeUltrafilterNat_Int RS FreeUltrafilterNat_subset], |
|
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11713
diff
changeset
|
436 |
simpset() addsimps [hypreal_zero_def, hypreal_one_def, |
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11713
diff
changeset
|
437 |
hyperpow, hypreal_less, hypnat_add])); |
10751 | 438 |
qed_spec_mp "hyperpow_Suc_less"; |
439 |
||
440 |
Goalw [hypnat_one_def] |
|
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11713
diff
changeset
|
441 |
"0 <= r & r < (1::hypreal) --> r pow (n + (1::hypnat)) <= r pow n"; |
10751 | 442 |
by (res_inst_tac [("z","n")] eq_Abs_hypnat 1); |
443 |
by (res_inst_tac [("z","r")] eq_Abs_hypreal 1); |
|
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11713
diff
changeset
|
444 |
by (auto_tac (claset() addSDs [conjI RS realpow_Suc_le] |
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11713
diff
changeset
|
445 |
addEs [FreeUltrafilterNat_Int RS FreeUltrafilterNat_subset], |
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11713
diff
changeset
|
446 |
simpset() addsimps [hypreal_zero_def, hypreal_one_def, hyperpow, |
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11713
diff
changeset
|
447 |
hypreal_le,hypnat_add, hypreal_less])); |
10751 | 448 |
qed_spec_mp "hyperpow_Suc_le"; |
449 |
||
450 |
Goalw [hypnat_one_def] |
|
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11713
diff
changeset
|
451 |
"(0::hypreal) <= r & r < 1 & n < N --> r pow N <= r pow n"; |
10751 | 452 |
by (res_inst_tac [("z","n")] eq_Abs_hypnat 1); |
453 |
by (res_inst_tac [("z","N")] eq_Abs_hypnat 1); |
|
454 |
by (res_inst_tac [("z","r")] eq_Abs_hypreal 1); |
|
455 |
by (auto_tac (claset(), |
|
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11713
diff
changeset
|
456 |
simpset() addsimps [hyperpow, hypreal_le,hypreal_less, |
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11713
diff
changeset
|
457 |
hypnat_less, hypreal_zero_def, hypreal_one_def])); |
10751 | 458 |
by (etac (FreeUltrafilterNat_Int RS FreeUltrafilterNat_subset) 1); |
459 |
by (etac FreeUltrafilterNat_Int 1); |
|
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11713
diff
changeset
|
460 |
by (auto_tac (claset() addSDs [conjI RS realpow_less_le], simpset())); |
10751 | 461 |
qed_spec_mp "hyperpow_less_le"; |
462 |
||
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11713
diff
changeset
|
463 |
Goal "[| (0::hypreal) <= r; r < 1 |] \ |
10751 | 464 |
\ ==> ALL N n. n < N --> r pow N <= r pow n"; |
465 |
by (blast_tac (claset() addSIs [hyperpow_less_le]) 1); |
|
466 |
qed "hyperpow_less_le2"; |
|
467 |
||
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11713
diff
changeset
|
468 |
Goal "[| 0 <= r; r < (1::hypreal); N : HNatInfinite |] \ |
10919
144ede948e58
renamings: real_of_nat, real_of_int -> (overloaded) real
paulson
parents:
10834
diff
changeset
|
469 |
\ ==> ALL n: Nats. r pow N <= r pow n"; |
10751 | 470 |
by (auto_tac (claset() addSIs [hyperpow_less_le], |
471 |
simpset() addsimps [HNatInfinite_iff])); |
|
472 |
qed "hyperpow_SHNat_le"; |
|
473 |
||
474 |
Goalw [hypreal_of_real_def,hypnat_of_nat_def] |
|
475 |
"(hypreal_of_real r) pow (hypnat_of_nat n) = hypreal_of_real (r ^ n)"; |
|
476 |
by (auto_tac (claset(), simpset() addsimps [hyperpow])); |
|
477 |
qed "hyperpow_realpow"; |
|
478 |
||
12613
279facb4253a
Literal arithmetic: raising numbers to powers (nat, int, real, hypreal)
paulson
parents:
12330
diff
changeset
|
479 |
Goalw [SReal_def] "(hypreal_of_real r) pow (hypnat_of_nat n) : Reals"; |
279facb4253a
Literal arithmetic: raising numbers to powers (nat, int, real, hypreal)
paulson
parents:
12330
diff
changeset
|
480 |
by (simp_tac (simpset() delsimps [hypreal_of_real_power] |
279facb4253a
Literal arithmetic: raising numbers to powers (nat, int, real, hypreal)
paulson
parents:
12330
diff
changeset
|
481 |
addsimps [hyperpow_realpow]) 1); |
10751 | 482 |
qed "hyperpow_SReal"; |
483 |
Addsimps [hyperpow_SReal]; |
|
484 |
||
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11713
diff
changeset
|
485 |
Goal "N : HNatInfinite ==> (0::hypreal) pow N = 0"; |
10751 | 486 |
by (dtac HNatInfinite_is_Suc 1); |
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11713
diff
changeset
|
487 |
by Auto_tac; |
10751 | 488 |
qed "hyperpow_zero_HNatInfinite"; |
489 |
Addsimps [hyperpow_zero_HNatInfinite]; |
|
490 |
||
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11713
diff
changeset
|
491 |
Goal "[| (0::hypreal) <= r; r < 1; n <= N |] ==> r pow N <= r pow n"; |
10751 | 492 |
by (dres_inst_tac [("y","N")] hypnat_le_imp_less_or_eq 1); |
493 |
by (auto_tac (claset() addIs [hyperpow_less_le], simpset())); |
|
494 |
qed "hyperpow_le_le"; |
|
495 |
||
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11713
diff
changeset
|
496 |
Goal "[| (0::hypreal) < r; r < 1 |] ==> r pow (n + (1::hypnat)) <= r"; |
11713
883d559b0b8c
sane numerals (stage 3): provide generic "1" on all number types;
wenzelm
parents:
11704
diff
changeset
|
497 |
by (dres_inst_tac [("n","(1::hypnat)")] (order_less_imp_le RS hyperpow_le_le) 1); |
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11713
diff
changeset
|
498 |
by Auto_tac; |
10751 | 499 |
qed "hyperpow_Suc_le_self"; |
500 |
||
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11713
diff
changeset
|
501 |
Goal "[| (0::hypreal) <= r; r < 1 |] ==> r pow (n + (1::hypnat)) <= r"; |
11713
883d559b0b8c
sane numerals (stage 3): provide generic "1" on all number types;
wenzelm
parents:
11704
diff
changeset
|
502 |
by (dres_inst_tac [("n","(1::hypnat)")] hyperpow_le_le 1); |
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11713
diff
changeset
|
503 |
by Auto_tac; |
10751 | 504 |
qed "hyperpow_Suc_le_self2"; |
505 |
||
506 |
Goalw [Infinitesimal_def] |
|
10778
2c6605049646
more tidying, especially to remove real_of_posnat
paulson
parents:
10751
diff
changeset
|
507 |
"[| x : Infinitesimal; 0 < N |] ==> abs (x pow N) <= abs x"; |
10751 | 508 |
by (auto_tac (claset() addSIs [hyperpow_Suc_le_self2], |
10778
2c6605049646
more tidying, especially to remove real_of_posnat
paulson
parents:
10751
diff
changeset
|
509 |
simpset() addsimps [hyperpow_hrabs RS sym, |
2c6605049646
more tidying, especially to remove real_of_posnat
paulson
parents:
10751
diff
changeset
|
510 |
hypnat_gt_zero_iff2, hrabs_ge_zero])); |
10751 | 511 |
qed "lemma_Infinitesimal_hyperpow"; |
512 |
||
513 |
Goal "[| x : Infinitesimal; 0 < N |] ==> x pow N : Infinitesimal"; |
|
514 |
by (rtac hrabs_le_Infinitesimal 1); |
|
10778
2c6605049646
more tidying, especially to remove real_of_posnat
paulson
parents:
10751
diff
changeset
|
515 |
by (rtac lemma_Infinitesimal_hyperpow 2); |
2c6605049646
more tidying, especially to remove real_of_posnat
paulson
parents:
10751
diff
changeset
|
516 |
by Auto_tac; |
10751 | 517 |
qed "Infinitesimal_hyperpow"; |
518 |
||
519 |
Goalw [hypnat_of_nat_def] |
|
520 |
"(x ^ n : Infinitesimal) = (x pow (hypnat_of_nat n) : Infinitesimal)"; |
|
521 |
by (res_inst_tac [("z","x")] eq_Abs_hypreal 1); |
|
522 |
by (auto_tac (claset(), simpset() addsimps [hrealpow, hyperpow])); |
|
523 |
qed "hrealpow_hyperpow_Infinitesimal_iff"; |
|
524 |
||
525 |
Goal "[| x : Infinitesimal; 0 < n |] ==> x ^ n : Infinitesimal"; |
|
526 |
by (auto_tac (claset() addSIs [Infinitesimal_hyperpow], |
|
527 |
simpset() addsimps [hrealpow_hyperpow_Infinitesimal_iff, |
|
528 |
hypnat_of_nat_less_iff,hypnat_of_nat_zero] |
|
529 |
delsimps [hypnat_of_nat_less_iff RS sym])); |
|
530 |
qed "Infinitesimal_hrealpow"; |
|
14268
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
12613
diff
changeset
|
531 |
|
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
12613
diff
changeset
|
532 |
(* MOVE UP *) |
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
12613
diff
changeset
|
533 |
Goal "(0::hypreal) <= x * x"; |
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
12613
diff
changeset
|
534 |
by (auto_tac (claset(),simpset() addsimps |
14331 | 535 |
[zero_le_mult_iff])); |
14268
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
12613
diff
changeset
|
536 |
qed "hypreal_mult_self_ge_zero"; |
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
12613
diff
changeset
|
537 |
Addsimps [hypreal_mult_self_ge_zero]; |
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
12613
diff
changeset
|
538 |
|
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
12613
diff
changeset
|
539 |
Goal "[|(0::hypreal) <= x; 0 <= y; x ^ Suc n = y ^ Suc n |] ==> x = y"; |
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
12613
diff
changeset
|
540 |
by (res_inst_tac [("z","x")] eq_Abs_hypreal 1); |
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
12613
diff
changeset
|
541 |
by (res_inst_tac [("z","y")] eq_Abs_hypreal 1); |
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
12613
diff
changeset
|
542 |
by (auto_tac (claset(),simpset() addsimps |
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
12613
diff
changeset
|
543 |
[hrealpow,hypreal_mult,hypreal_le,hypreal_zero_num])); |
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
12613
diff
changeset
|
544 |
by (ultra_tac (claset() addIs [realpow_Suc_cancel_eq], |
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
12613
diff
changeset
|
545 |
simpset()) 1); |
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
12613
diff
changeset
|
546 |
qed "hrealpow_Suc_cancel_eq"; |
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
12613
diff
changeset
|
547 |