# HG changeset patch # User huffman # Date 1159311250 -7200 # Node ID bf00c59354321f680da67ad7c043ff9bc068bf68 # Parent 4c4869e4ddb76e241b93cf6b0a1e413e23ea5c7e define new constant Standard = range star_of diff -r 4c4869e4ddb7 -r bf00c5935432 src/HOL/Hyperreal/StarClasses.thy --- 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 \ Standard" +by (simp add: star_zero_def) + +lemma Standard_one: "1 \ Standard" +by (simp add: star_one_def) + +lemma Standard_number_of: "number_of b \ Standard" +by (simp add: star_number_def) + +lemma Standard_add: "\x \ Standard; y \ Standard\ \ x + y \ Standard" +by (simp add: star_add_def) + +lemma Standard_diff: "\x \ Standard; y \ Standard\ \ x - y \ Standard" +by (simp add: star_diff_def) + +lemma Standard_minus: "x \ Standard \ - x \ Standard" +by (simp add: star_minus_def) + +lemma Standard_mult: "\x \ Standard; y \ Standard\ \ x * y \ Standard" +by (simp add: star_mult_def) + +lemma Standard_divide: "\x \ Standard; y \ Standard\ \ x / y \ Standard" +by (simp add: star_divide_def) + +lemma Standard_inverse: "x \ Standard \ inverse x \ Standard" +by (simp add: star_inverse_def) + +lemma Standard_abs: "x \ Standard \ abs x \ Standard" +by (simp add: star_abs_def) + +lemma Standard_div: "\x \ Standard; y \ Standard\ \ x div y \ Standard" +by (simp add: star_div_def) + +lemma Standard_mod: "\x \ Standard; y \ Standard\ \ x mod y \ Standard" +by (simp add: star_mod_def) + +lemma Standard_power: "x \ Standard \ x ^ n \ 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 {* diff -r 4c4869e4ddb7 -r bf00c5935432 src/HOL/Hyperreal/StarDef.thy --- 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 \ 'a star" "star_of x == star_n (\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 \ Standard" +by (simp add: Standard_def) + subsection {* Internal functions *} @@ -193,6 +200,10 @@ lemma Ifun_star_of [simp]: "star_of f \ star_of x = star_of (f x)" by (transfer, rule refl) +lemma Standard_Ifun [simp]: + "\f \ Standard; x \ Standard\ \ f \ x \ 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 \ Standard \ starfun f x \ Standard" +by (simp add: starfun_def) + +lemma Standard_starfun2 [simp]: + "\x \ Standard; y \ Standard\ \ starfun2 f x y \ Standard" +by (simp add: starfun2_def) + subsection {* Internal predicates *}