371 |
371 |
372 constdefs |
372 constdefs |
373 hypreal_of_hypnat :: "hypnat => hypreal" |
373 hypreal_of_hypnat :: "hypnat => hypreal" |
374 "hypreal_of_hypnat == *f* real" |
374 "hypreal_of_hypnat == *f* real" |
375 |
375 |
|
376 declare hypreal_of_hypnat_def [transfer_unfold] |
376 |
377 |
377 lemma HNat_hypreal_of_nat [simp]: "hypreal_of_nat N \<in> Nats" |
378 lemma HNat_hypreal_of_nat [simp]: "hypreal_of_nat N \<in> Nats" |
378 by (simp add: hypreal_of_nat_def) |
379 by (simp add: hypreal_of_nat_def) |
379 |
380 |
380 lemma hypreal_of_hypnat: |
381 lemma hypreal_of_hypnat: |
381 "hypreal_of_hypnat (star_n X) = star_n (%n. real (X n))" |
382 "hypreal_of_hypnat (star_n X) = star_n (%n. real (X n))" |
382 by (simp add: hypreal_of_hypnat_def starfun) |
383 by (simp add: hypreal_of_hypnat_def starfun) |
383 |
384 |
384 lemma hypreal_of_hypnat_inject [simp]: |
385 lemma hypreal_of_hypnat_inject [simp]: |
385 "!!m n. (hypreal_of_hypnat m = hypreal_of_hypnat n) = (m=n)" |
386 "!!m n. (hypreal_of_hypnat m = hypreal_of_hypnat n) = (m=n)" |
386 by (unfold hypreal_of_hypnat_def, transfer, simp) |
387 by (transfer, simp) |
387 |
388 |
388 lemma hypreal_of_hypnat_zero: "hypreal_of_hypnat 0 = 0" |
389 lemma hypreal_of_hypnat_zero: "hypreal_of_hypnat 0 = 0" |
389 by (simp add: star_n_zero_num hypreal_of_hypnat) |
390 by (simp add: star_n_zero_num hypreal_of_hypnat) |
390 |
391 |
391 lemma hypreal_of_hypnat_one: "hypreal_of_hypnat (1::hypnat) = 1" |
392 lemma hypreal_of_hypnat_one: "hypreal_of_hypnat (1::hypnat) = 1" |
392 by (simp add: star_n_one_num hypreal_of_hypnat) |
393 by (simp add: star_n_one_num hypreal_of_hypnat) |
393 |
394 |
394 lemma hypreal_of_hypnat_add [simp]: |
395 lemma hypreal_of_hypnat_add [simp]: |
395 "!!m n. hypreal_of_hypnat (m + n) = hypreal_of_hypnat m + hypreal_of_hypnat n" |
396 "!!m n. hypreal_of_hypnat (m + n) = hypreal_of_hypnat m + hypreal_of_hypnat n" |
396 by (unfold hypreal_of_hypnat_def, transfer, rule real_of_nat_add) |
397 by (transfer, rule real_of_nat_add) |
397 |
398 |
398 lemma hypreal_of_hypnat_mult [simp]: |
399 lemma hypreal_of_hypnat_mult [simp]: |
399 "!!m n. hypreal_of_hypnat (m * n) = hypreal_of_hypnat m * hypreal_of_hypnat n" |
400 "!!m n. hypreal_of_hypnat (m * n) = hypreal_of_hypnat m * hypreal_of_hypnat n" |
400 by (unfold hypreal_of_hypnat_def, transfer, rule real_of_nat_mult) |
401 by (transfer, rule real_of_nat_mult) |
401 |
402 |
402 lemma hypreal_of_hypnat_less_iff [simp]: |
403 lemma hypreal_of_hypnat_less_iff [simp]: |
403 "!!m n. (hypreal_of_hypnat n < hypreal_of_hypnat m) = (n < m)" |
404 "!!m n. (hypreal_of_hypnat n < hypreal_of_hypnat m) = (n < m)" |
404 by (unfold hypreal_of_hypnat_def, transfer, simp) |
405 by (transfer, simp) |
405 |
406 |
406 lemma hypreal_of_hypnat_eq_zero_iff: "(hypreal_of_hypnat N = 0) = (N = 0)" |
407 lemma hypreal_of_hypnat_eq_zero_iff: "(hypreal_of_hypnat N = 0) = (N = 0)" |
407 by (simp add: hypreal_of_hypnat_zero [symmetric]) |
408 by (simp add: hypreal_of_hypnat_zero [symmetric]) |
408 declare hypreal_of_hypnat_eq_zero_iff [simp] |
409 declare hypreal_of_hypnat_eq_zero_iff [simp] |
409 |
410 |
410 lemma hypreal_of_hypnat_ge_zero [simp]: "!!n. 0 \<le> hypreal_of_hypnat n" |
411 lemma hypreal_of_hypnat_ge_zero [simp]: "!!n. 0 \<le> hypreal_of_hypnat n" |
411 by (unfold hypreal_of_hypnat_def, transfer, simp) |
412 by (transfer, simp) |
412 |
413 |
413 lemma HNatInfinite_inverse_Infinitesimal [simp]: |
414 lemma HNatInfinite_inverse_Infinitesimal [simp]: |
414 "n \<in> HNatInfinite ==> inverse (hypreal_of_hypnat n) \<in> Infinitesimal" |
415 "n \<in> HNatInfinite ==> inverse (hypreal_of_hypnat n) \<in> Infinitesimal" |
415 apply (cases n) |
416 apply (cases n) |
416 apply (auto simp add: hypreal_of_hypnat star_n_inverse |
417 apply (auto simp add: hypreal_of_hypnat star_n_inverse |