# HG changeset patch # User huffman # Date 1126052163 -7200 # Node ID 25aab757672bc2c8ff2ce3b4a4b4eab70686ee77 # Parent 6c82a5c1007605a543a257b1412a9e5c965fc8bd generalized types diff -r 6c82a5c10076 -r 25aab757672b src/HOL/Hyperreal/Star.thy --- a/src/HOL/Hyperreal/Star.thy Wed Sep 07 02:13:24 2005 +0200 +++ b/src/HOL/Hyperreal/Star.thy Wed Sep 07 02:16:03 2005 +0200 @@ -12,30 +12,30 @@ constdefs (* nonstandard extension of sets *) - starset :: "real set => hypreal set" ("*s* _" [80] 80) + starset :: "'a set => 'a star set" ("*s* _" [80] 80) "*s* A == {x. \X \ Rep_star(x). {n::nat. X n \ A}: FreeUltrafilterNat}" (* internal sets *) - starset_n :: "(nat => real set) => hypreal set" ("*sn* _" [80] 80) + starset_n :: "(nat => 'a set) => 'a star set" ("*sn* _" [80] 80) "*sn* As == {x. \X \ Rep_star(x). {n::nat. X n : (As n)}: FreeUltrafilterNat}" - InternalSets :: "hypreal set set" + InternalSets :: "'a star set set" "InternalSets == {X. \As. X = *sn* As}" (* nonstandard extension of function *) - is_starext :: "[hypreal => hypreal, real => real] => bool" + is_starext :: "['a star => 'a star, 'a => 'a] => bool" "is_starext F f == (\x y. \X \ Rep_star(x). \Y \ Rep_star(y). ((y = (F x)) = ({n. Y n = f(X n)} : FreeUltrafilterNat)))" - starfun :: "(real => real) => hypreal => hypreal" ("*f* _" [80] 80) + starfun :: "('a => 'a) => 'a star => 'a star" ("*f* _" [80] 80) "*f* f == (%x. Abs_star(\X \ Rep_star(x). starrel``{%n. f(X n)}))" (* internal functions *) - starfun_n :: "(nat => (real => real)) => hypreal => hypreal" + starfun_n :: "(nat => ('a => 'a)) => 'a star => 'a star" ("*fn* _" [80] 80) "*fn* F == (%x. Abs_star(\X \ Rep_star(x). starrel``{%n. (F n)(X n)}))" - InternalFuns :: "(hypreal => hypreal) set" + InternalFuns :: "('a star => 'a star) set" "InternalFuns == {X. \F. X = *fn* F}" @@ -180,10 +180,9 @@ apply (rule_tac z = y in eq_Abs_star, auto) apply (rule bexI, rule_tac [2] lemma_starrel_refl) apply (rule bexI, rule_tac [2] lemma_starrel_refl) -apply (auto dest!: spec - simp add: hypreal_minus abs_if hypreal_zero_def - hypreal_le hypreal_less) -apply (arith | ultra)+ +apply (fold star_n_def) +apply (unfold star_abs_def Ifun_of_def star_of_def) +apply (simp add: Ifun_star_n star_n_eq_iff) done lemma Rep_star_FreeUltrafilterNat: @@ -247,7 +246,8 @@ lemma starfun_diff: "( *f* f) xa - ( *f* g) xa = ( *f* (%x. f x - g x)) xa" -apply (simp add: diff_minus) +apply (rule_tac z = xa in eq_Abs_star) +apply (simp add: starfun hypreal_diff) done declare starfun_diff [symmetric, simp] @@ -356,18 +356,26 @@ lemma starfun_inverse_inverse: "( *f* inverse) x = inverse(x)" apply (rule_tac z = x in eq_Abs_star) -apply (auto simp add: starfun hypreal_inverse hypreal_zero_def) +apply (simp add: starfun) +apply (fold star_n_def) +apply (unfold star_inverse_def Ifun_of_def star_of_def) +apply (simp add: Ifun_star_n) done declare starfun_inverse_inverse [simp] lemma starfun_inverse: "inverse (( *f* f) x) = ( *f* (%x. inverse (f x))) x" apply (rule_tac z = x in eq_Abs_star) -apply (auto simp add: starfun hypreal_inverse) +apply (auto simp add: starfun hypreal_inverse2) done declare starfun_inverse [symmetric, simp] lemma starfun_divide: "( *f* f) xa / ( *f* g) xa = ( *f* (%x. f x / g x)) xa" -by (simp add: divide_inverse) +apply (rule_tac z = xa in eq_Abs_star) +apply (simp add: starfun) +apply (fold star_n_def) +apply (unfold star_divide_def Ifun2_of_def star_of_def) +apply (simp add: Ifun_star_n) +done declare starfun_divide [symmetric, simp] lemma starfun_inverse2: "inverse (( *f* f) x) = ( *f* (%x. inverse (f x))) x"