src/HOL/Hyperreal/NSA.thy
changeset 14378 69c4d5997669
parent 14371 c78c7da09519
child 14387 e96d5c42c4b0
     1.1 --- a/src/HOL/Hyperreal/NSA.thy	Thu Feb 05 10:45:28 2004 +0100
     1.2 +++ b/src/HOL/Hyperreal/NSA.thy	Tue Feb 10 12:02:11 2004 +0100
     1.3 @@ -33,7 +33,7 @@
     1.4     "x @= y       == (x + -y) \<in> Infinitesimal"
     1.5  
     1.6  
     1.7 -defs
     1.8 +defs (overloaded)
     1.9  
    1.10     (*standard real numbers as a subset of the hyperreals*)
    1.11     SReal_def:      "Reals == {x. \<exists>r. x = hypreal_of_real r}"
    1.12 @@ -47,7 +47,8 @@
    1.13       Closure laws for members of (embedded) set standard real Reals
    1.14   --------------------------------------------------------------------*)
    1.15  
    1.16 -lemma SReal_add: "[| (x::hypreal) \<in> Reals; y \<in> Reals |] ==> x + y \<in> Reals"
    1.17 +lemma SReal_add [simp]:
    1.18 +     "[| (x::hypreal) \<in> Reals; y \<in> Reals |] ==> x + y \<in> Reals"
    1.19  apply (auto simp add: SReal_def)
    1.20  apply (rule_tac x = "r + ra" in exI, simp)
    1.21  done
    1.22 @@ -1911,6 +1912,11 @@
    1.23  apply (blast dest!: reals_Archimedean intro: order_less_trans)
    1.24  done
    1.25  
    1.26 +lemma of_nat_in_Reals [simp]: "(of_nat n::hypreal) \<in> \<real>"
    1.27 +apply (induct n)
    1.28 +apply (simp_all add: SReal_add);
    1.29 +done 
    1.30 + 
    1.31  lemma lemma_Infinitesimal2: "(\<forall>r \<in> Reals. 0 < r --> x < r) =
    1.32        (\<forall>n. x < inverse(hypreal_of_nat (Suc n)))"
    1.33  apply safe
    1.34 @@ -1918,13 +1924,14 @@
    1.35  apply (simp (no_asm_use) add: SReal_inverse)
    1.36  apply (rule real_of_nat_Suc_gt_zero [THEN positive_imp_inverse_positive, THEN hypreal_of_real_less_iff [THEN iffD2], THEN [2] impE])
    1.37  prefer 2 apply assumption
    1.38 -apply (simp add: real_of_nat_Suc_gt_zero hypreal_of_nat_def)
    1.39 +apply (simp add: real_of_nat_Suc_gt_zero hypreal_of_nat_eq)
    1.40  apply (auto dest!: reals_Archimedean simp add: SReal_iff)
    1.41  apply (drule hypreal_of_real_less_iff [THEN iffD2])
    1.42 -apply (simp add: real_of_nat_Suc_gt_zero hypreal_of_nat_def)
    1.43 +apply (simp add: real_of_nat_Suc_gt_zero hypreal_of_nat_eq)
    1.44  apply (blast intro: order_less_trans)
    1.45  done
    1.46  
    1.47 +
    1.48  lemma Infinitesimal_hypreal_of_nat_iff:
    1.49       "Infinitesimal = {x. \<forall>n. abs x < inverse (hypreal_of_nat (Suc n))}"
    1.50  apply (simp add: Infinitesimal_def)