define new constant Standard = range star_of

--- a/src/HOL/Hyperreal/StarClasses.thy	Wed Sep 27 00:52:59 2006 +0200
+++ b/src/HOL/Hyperreal/StarClasses.thy	Wed Sep 27 00:54:10 2006 +0200
@@ -46,6 +46,54 @@
   star_le_def       star_less_def     star_abs_def
   star_div_def      star_mod_def      star_power_def
 
+text {* Class operations preserve standard elements *}
+
+lemma Standard_zero: "0 \<in> Standard"
+by (simp add: star_zero_def)
+
+lemma Standard_one: "1 \<in> Standard"
+by (simp add: star_one_def)
+
+lemma Standard_number_of: "number_of b \<in> Standard"
+by (simp add: star_number_def)
+
+lemma Standard_add: "\<lbrakk>x \<in> Standard; y \<in> Standard\<rbrakk> \<Longrightarrow> x + y \<in> Standard"
+by (simp add: star_add_def)
+
+lemma Standard_diff: "\<lbrakk>x \<in> Standard; y \<in> Standard\<rbrakk> \<Longrightarrow> x - y \<in> Standard"
+by (simp add: star_diff_def)
+
+lemma Standard_minus: "x \<in> Standard \<Longrightarrow> - x \<in> Standard"
+by (simp add: star_minus_def)
+
+lemma Standard_mult: "\<lbrakk>x \<in> Standard; y \<in> Standard\<rbrakk> \<Longrightarrow> x * y \<in> Standard"
+by (simp add: star_mult_def)
+
+lemma Standard_divide: "\<lbrakk>x \<in> Standard; y \<in> Standard\<rbrakk> \<Longrightarrow> x / y \<in> Standard"
+by (simp add: star_divide_def)
+
+lemma Standard_inverse: "x \<in> Standard \<Longrightarrow> inverse x \<in> Standard"
+by (simp add: star_inverse_def)
+
+lemma Standard_abs: "x \<in> Standard \<Longrightarrow> abs x \<in> Standard"
+by (simp add: star_abs_def)
+
+lemma Standard_div: "\<lbrakk>x \<in> Standard; y \<in> Standard\<rbrakk> \<Longrightarrow> x div y \<in> Standard"
+by (simp add: star_div_def)
+
+lemma Standard_mod: "\<lbrakk>x \<in> Standard; y \<in> Standard\<rbrakk> \<Longrightarrow> x mod y \<in> Standard"
+by (simp add: star_mod_def)
+
+lemma Standard_power: "x \<in> Standard \<Longrightarrow> x ^ n \<in> Standard"
+by (simp add: star_power_def)
+
+lemmas Standard_simps [simp] =
+  Standard_zero  Standard_one  Standard_number_of
+  Standard_add  Standard_diff  Standard_minus
+  Standard_mult  Standard_divide  Standard_inverse
+  Standard_abs  Standard_div  Standard_mod
+  Standard_power
+
 text {* @{term star_of} preserves class operations *}
 
 lemma star_of_add: "star_of (x + y) = star_of x + star_of y"
@@ -163,7 +211,6 @@
 instance star :: (linorder) linorder
 by (intro_classes, transfer, rule linorder_linear)
 
-
 subsection {* Lattice ordering classes *}
 
 text {*

--- a/src/HOL/Hyperreal/StarDef.thy	Wed Sep 27 00:52:59 2006 +0200
+++ b/src/HOL/Hyperreal/StarDef.thy	Wed Sep 27 00:54:10 2006 +0200
@@ -160,13 +160,20 @@
   star_of :: "'a \<Rightarrow> 'a star"
   "star_of x == star_n (\<lambda>n. x)"
 
+  Standard :: "'a star set"
+  "Standard = range star_of"
+
 text {* Transfer tactic should remove occurrences of @{term star_of} *}
 setup {* Transfer.add_const "StarDef.star_of" *}
+
 declare star_of_def [transfer_intro]
 
 lemma star_of_inject: "(star_of x = star_of y) = (x = y)"
 by (transfer, rule refl)
 
+lemma Standard_star_of [simp]: "star_of x \<in> Standard"
+by (simp add: Standard_def)
+
 
 subsection {* Internal functions *}
 
@@ -193,6 +200,10 @@
 lemma Ifun_star_of [simp]: "star_of f \<star> star_of x = star_of (f x)"
 by (transfer, rule refl)
 
+lemma Standard_Ifun [simp]:
+  "\<lbrakk>f \<in> Standard; x \<in> Standard\<rbrakk> \<Longrightarrow> f \<star> x \<in> Standard"
+by (auto simp add: Standard_def)
+
 text {* Nonstandard extensions of functions *}
 
 definition
@@ -220,6 +231,13 @@
 lemma starfun2_star_of [simp]: "( *f2* f) (star_of x) = *f* f x"
 by (transfer, rule refl)
 
+lemma Standard_starfun [simp]: "x \<in> Standard \<Longrightarrow> starfun f x \<in> Standard"
+by (simp add: starfun_def)
+
+lemma Standard_starfun2 [simp]:
+  "\<lbrakk>x \<in> Standard; y \<in> Standard\<rbrakk> \<Longrightarrow> starfun2 f x y \<in> Standard"
+by (simp add: starfun2_def)
+
 
 subsection {* Internal predicates *}