202 ----------------------------------------------------------*) |
202 ----------------------------------------------------------*) |
203 Goalw [hypreal_of_real_def] |
203 Goalw [hypreal_of_real_def] |
204 "abs (hypreal_of_real r) = hypreal_of_real (abs r)"; |
204 "abs (hypreal_of_real r) = hypreal_of_real (abs r)"; |
205 by (auto_tac (claset(), simpset() addsimps [hypreal_hrabs])); |
205 by (auto_tac (claset(), simpset() addsimps [hypreal_hrabs])); |
206 qed "hypreal_of_real_hrabs"; |
206 qed "hypreal_of_real_hrabs"; |
|
207 |
|
208 |
|
209 (*---------------------------------------------------------------------------- |
|
210 Embedding of the naturals in the hyperreals |
|
211 ----------------------------------------------------------------------------*) |
|
212 |
|
213 Goalw [hypreal_of_nat_def] |
|
214 "hypreal_of_nat n1 + hypreal_of_nat n2 = hypreal_of_nat (n1 + n2)"; |
|
215 by (simp_tac (simpset() addsimps [hypreal_of_real_add, real_of_nat_add]) 1); |
|
216 qed "hypreal_of_nat_add"; |
|
217 |
|
218 Goalw [hypreal_of_nat_def] |
|
219 "(n < m) = (hypreal_of_nat n < hypreal_of_nat m)"; |
|
220 by (auto_tac (claset() addIs [hypreal_add_less_mono1], simpset())); |
|
221 qed "hypreal_of_nat_less_iff"; |
|
222 Addsimps [hypreal_of_nat_less_iff RS sym]; |
|
223 |
|
224 (*------------------------------------------------------------*) |
|
225 (* naturals embedded in hyperreals *) |
|
226 (* is a hyperreal c.f. NS extension *) |
|
227 (*------------------------------------------------------------*) |
|
228 |
|
229 Goalw [hypreal_of_nat_def, hypreal_of_real_def, real_of_nat_def] |
|
230 "hypreal_of_nat m = Abs_hypreal(hyprel^^{%n. real_of_nat m})"; |
|
231 by Auto_tac; |
|
232 qed "hypreal_of_nat_iff"; |
|
233 |
|
234 Goal "inj hypreal_of_nat"; |
|
235 by (simp_tac (simpset() addsimps [inj_on_def, hypreal_of_nat_def]) 1); |
|
236 qed "inj_hypreal_of_nat"; |
|
237 |
|
238 Goalw [hypreal_of_nat_def] |
|
239 "hypreal_of_nat (Suc n) = hypreal_of_nat n + 1hr"; |
|
240 by (simp_tac (simpset() addsimps [real_of_nat_Suc]) 1); |
|
241 qed "hypreal_of_nat_Suc"; |
|
242 |
|
243 (*"neg" is used in rewrite rules for binary comparisons*) |
|
244 Goal "hypreal_of_nat (number_of v :: nat) = \ |
|
245 \ (if neg (number_of v) then #0 \ |
|
246 \ else (number_of v :: hypreal))"; |
|
247 by (simp_tac (simpset() addsimps [hypreal_of_nat_def]) 1); |
|
248 qed "hypreal_of_nat_number_of"; |
|
249 Addsimps [hypreal_of_nat_number_of]; |
|
250 |
|
251 Goal "hypreal_of_nat 0 = #0"; |
|
252 by (simp_tac (simpset() delsimps [numeral_0_eq_0] |
|
253 addsimps [numeral_0_eq_0 RS sym]) 1); |
|
254 qed "hypreal_of_nat_zero"; |
|
255 Addsimps [hypreal_of_nat_zero]; |