src/HOL/NSA/NSA.thy
changeset 47108 2a1953f0d20d
parent 45541 934866fc776c
child 51521 36fa825e0ea7
     1.1 --- a/src/HOL/NSA/NSA.thy	Sat Mar 24 16:27:04 2012 +0100
     1.2 +++ b/src/HOL/NSA/NSA.thy	Sun Mar 25 20:15:39 2012 +0200
     1.3 @@ -190,7 +190,7 @@
     1.4  lemma SReal_hypreal_of_real [simp]: "hypreal_of_real x \<in> Reals"
     1.5  by (simp add: Reals_eq_Standard)
     1.6  
     1.7 -lemma SReal_divide_number_of: "r \<in> Reals ==> r/(number_of w::hypreal) \<in> Reals"
     1.8 +lemma SReal_divide_numeral: "r \<in> Reals ==> r/(numeral w::hypreal) \<in> Reals"
     1.9  by simp
    1.10  
    1.11  text{*epsilon is not in Reals because it is an infinitesimal*}
    1.12 @@ -290,8 +290,8 @@
    1.13    "(hnorm (x::hypreal) \<in> HFinite) = (x \<in> HFinite)"
    1.14  by (simp add: HFinite_def)
    1.15  
    1.16 -lemma HFinite_number_of [simp]: "number_of w \<in> HFinite"
    1.17 -unfolding star_number_def by (rule HFinite_star_of)
    1.18 +lemma HFinite_numeral [simp]: "numeral w \<in> HFinite"
    1.19 +unfolding star_numeral_def by (rule HFinite_star_of)
    1.20  
    1.21  (** As always with numerals, 0 and 1 are special cases **)
    1.22  
    1.23 @@ -347,7 +347,7 @@
    1.24  apply (rule InfinitesimalI)
    1.25  apply (rule hypreal_sum_of_halves [THEN subst])
    1.26  apply (drule half_gt_zero)
    1.27 -apply (blast intro: hnorm_add_less SReal_divide_number_of dest: InfinitesimalD)
    1.28 +apply (blast intro: hnorm_add_less SReal_divide_numeral dest: InfinitesimalD)
    1.29  done
    1.30  
    1.31  lemma Infinitesimal_minus_iff [simp]: "(-x:Infinitesimal) = (x:Infinitesimal)"
    1.32 @@ -652,7 +652,7 @@
    1.33  (*reorientation simplification procedure: reorients (polymorphic)
    1.34    0 = x, 1 = x, nnn = x provided x isn't 0, 1 or a numeral.*)
    1.35  simproc_setup approx_reorient_simproc
    1.36 -  ("0 @= x" | "1 @= y" | "number_of w @= z") =
    1.37 +  ("0 @= x" | "1 @= y" | "numeral w @= z" | "neg_numeral w @= r") =
    1.38  {*
    1.39    let val rule = @{thm approx_reorient} RS eq_reflection
    1.40        fun proc phi ss ct = case term_of ct of
    1.41 @@ -957,9 +957,9 @@
    1.42       "x \<noteq> 0 ==> star_of x \<in> HFinite - Infinitesimal"
    1.43  by simp
    1.44  
    1.45 -lemma number_of_not_Infinitesimal [simp]:
    1.46 -     "number_of w \<noteq> (0::hypreal) ==> (number_of w :: hypreal) \<notin> Infinitesimal"
    1.47 -by (fast dest: Reals_number_of [THEN SReal_Infinitesimal_zero])
    1.48 +lemma numeral_not_Infinitesimal [simp]:
    1.49 +     "numeral w \<noteq> (0::hypreal) ==> (numeral w :: hypreal) \<notin> Infinitesimal"
    1.50 +by (fast dest: Reals_numeral [THEN SReal_Infinitesimal_zero])
    1.51  
    1.52  (*again: 1 is a special case, but not 0 this time*)
    1.53  lemma one_not_Infinitesimal [simp]:
    1.54 @@ -1024,31 +1024,31 @@
    1.55  apply simp
    1.56  done
    1.57  
    1.58 -lemma number_of_approx_iff [simp]:
    1.59 -     "(number_of v @= (number_of w :: 'a::{number,real_normed_vector} star)) =
    1.60 -      (number_of v = (number_of w :: 'a))"
    1.61 -apply (unfold star_number_def)
    1.62 +lemma numeral_approx_iff [simp]:
    1.63 +     "(numeral v @= (numeral w :: 'a::{numeral,real_normed_vector} star)) =
    1.64 +      (numeral v = (numeral w :: 'a))"
    1.65 +apply (unfold star_numeral_def)
    1.66  apply (rule star_of_approx_iff)
    1.67  done
    1.68  
    1.69  (*And also for 0 @= #nn and 1 @= #nn, #nn @= 0 and #nn @= 1.*)
    1.70  lemma [simp]:
    1.71 -  "(number_of w @= (0::'a::{number,real_normed_vector} star)) =
    1.72 -   (number_of w = (0::'a))"
    1.73 -  "((0::'a::{number,real_normed_vector} star) @= number_of w) =
    1.74 -   (number_of w = (0::'a))"
    1.75 -  "(number_of w @= (1::'b::{number,one,real_normed_vector} star)) =
    1.76 -   (number_of w = (1::'b))"
    1.77 -  "((1::'b::{number,one,real_normed_vector} star) @= number_of w) =
    1.78 -   (number_of w = (1::'b))"
    1.79 +  "(numeral w @= (0::'a::{numeral,real_normed_vector} star)) =
    1.80 +   (numeral w = (0::'a))"
    1.81 +  "((0::'a::{numeral,real_normed_vector} star) @= numeral w) =
    1.82 +   (numeral w = (0::'a))"
    1.83 +  "(numeral w @= (1::'b::{numeral,one,real_normed_vector} star)) =
    1.84 +   (numeral w = (1::'b))"
    1.85 +  "((1::'b::{numeral,one,real_normed_vector} star) @= numeral w) =
    1.86 +   (numeral w = (1::'b))"
    1.87    "~ (0 @= (1::'c::{zero_neq_one,real_normed_vector} star))"
    1.88    "~ (1 @= (0::'c::{zero_neq_one,real_normed_vector} star))"
    1.89 -apply (unfold star_number_def star_zero_def star_one_def)
    1.90 +apply (unfold star_numeral_def star_zero_def star_one_def)
    1.91  apply (unfold star_of_approx_iff)
    1.92  by (auto intro: sym)
    1.93  
    1.94 -lemma star_of_approx_number_of_iff [simp]:
    1.95 -     "(star_of k @= number_of w) = (k = number_of w)"
    1.96 +lemma star_of_approx_numeral_iff [simp]:
    1.97 +     "(star_of k @= numeral w) = (k = numeral w)"
    1.98  by (subst star_of_approx_iff [symmetric], auto)
    1.99  
   1.100  lemma star_of_approx_zero_iff [simp]: "(star_of k @= 0) = (k = 0)"
   1.101 @@ -1843,8 +1843,11 @@
   1.102  lemma st_add: "\<lbrakk>x \<in> HFinite; y \<in> HFinite\<rbrakk> \<Longrightarrow> st (x + y) = st x + st y"
   1.103  by (simp add: st_unique st_SReal st_approx_self approx_add)
   1.104  
   1.105 -lemma st_number_of [simp]: "st (number_of w) = number_of w"
   1.106 -by (rule Reals_number_of [THEN st_SReal_eq])
   1.107 +lemma st_numeral [simp]: "st (numeral w) = numeral w"
   1.108 +by (rule Reals_numeral [THEN st_SReal_eq])
   1.109 +
   1.110 +lemma st_neg_numeral [simp]: "st (neg_numeral w) = neg_numeral w"
   1.111 +by (rule Reals_neg_numeral [THEN st_SReal_eq])
   1.112  
   1.113  lemma st_0 [simp]: "st 0 = 0"
   1.114  by (simp add: st_SReal_eq)