# HG changeset patch # User nipkow # Date 1044632423 -3600 # Node ID c3fbfd472365aad1305b3160a6fba642350efb98 # Parent a4cd9057d2eefd41855e3a2525dac34db8398648 (*f -> ( *f because of new comments diff -r a4cd9057d2ee -r c3fbfd472365 src/HOL/Hyperreal/ExtraThms2.ML --- a/src/HOL/Hyperreal/ExtraThms2.ML Fri Feb 07 15:36:54 2003 +0100 +++ b/src/HOL/Hyperreal/ExtraThms2.ML Fri Feb 07 16:40:23 2003 +0100 @@ -498,7 +498,7 @@ Addsimps [HNatInfinite_inverse_not_zero]; Goal "N : HNatInfinite \ -\ ==> (*fNat* (%x. inverse (real x))) N : Infinitesimal"; +\ ==> ( *fNat* (%x. inverse (real x))) N : Infinitesimal"; by (res_inst_tac [("f1","inverse")] (starfun_stafunNat_o2 RS subst) 1); by (subgoal_tac "hypreal_of_hypnat N ~= 0" 1); by (auto_tac (claset(),simpset() addsimps [starfunNat_real_of_nat])); diff -r a4cd9057d2ee -r c3fbfd472365 src/HOL/Hyperreal/HSeries.ML --- a/src/HOL/Hyperreal/HSeries.ML Fri Feb 07 15:36:54 2003 +0100 +++ b/src/HOL/Hyperreal/HSeries.ML Fri Feb 07 16:40:23 2003 +0100 @@ -45,7 +45,7 @@ (* Theorem corresponding to recursive case in def of sumr *) Goalw [hypnat_one_def] "sumhr(m,n+(1::hypnat),f) = (if n + (1::hypnat) <= m then 0 \ -\ else sumhr(m,n,f) + (*fNat* f) n)"; +\ else sumhr(m,n,f) + ( *fNat* f) n)"; by (res_inst_tac [("z","m")] eq_Abs_hypnat 1); by (res_inst_tac [("z","n")] eq_Abs_hypnat 1); by (auto_tac (claset(), @@ -68,7 +68,7 @@ Addsimps [sumhr_eq_bounds]; Goalw [hypnat_one_def] - "sumhr (m,m + (1::hypnat),f) = (*fNat* f) m"; + "sumhr (m,m + (1::hypnat),f) = ( *fNat* f) m"; by (res_inst_tac [("z","m")] eq_Abs_hypnat 1); by (auto_tac (claset(), simpset() addsimps [sumhr, hypnat_add,starfunNat])); @@ -206,7 +206,7 @@ qed "sumhr_interval_const"; Goalw [hypnat_zero_def] - "(*fNat* (%n. sumr 0 n f)) N = sumhr(0,N,f)"; + "( *fNat* (%n. sumr 0 n f)) N = sumhr(0,N,f)"; by (res_inst_tac [("z","N")] eq_Abs_hypnat 1); by (asm_full_simp_tac (simpset() addsimps [starfunNat,sumhr]) 1); qed "starfunNat_sumr"; diff -r a4cd9057d2ee -r c3fbfd472365 src/HOL/Hyperreal/Lim.ML --- a/src/HOL/Hyperreal/Lim.ML Fri Feb 07 15:36:54 2003 +0100 +++ b/src/HOL/Hyperreal/Lim.ML Fri Feb 07 16:40:23 2003 +0100 @@ -438,7 +438,7 @@ Goalw [isNSCont_def] "[| isNSCont f a; y \\ hypreal_of_real a |] \ -\ ==> (*f* f) y \\ hypreal_of_real (f a)"; +\ ==> ( *f* f) y \\ hypreal_of_real (f a)"; by (Blast_tac 1); qed "isNSContD"; @@ -662,7 +662,7 @@ Uniform continuity ------------------------------------------------------------------*) Goalw [isNSUCont_def] - "[| isNSUCont f; x \\ y|] ==> (*f* f) x \\ (*f* f) y"; + "[| isNSUCont f; x \\ y|] ==> ( *f* f) x \\ ( *f* f) y"; by (Blast_tac 1); qed "isNSUContD"; @@ -859,7 +859,7 @@ "(NSDERIV f x :> D) = \ \ (\\xa. \ \ xa \\ hypreal_of_real x & xa \\ hypreal_of_real x --> \ -\ (*f* (%z. (f z - f x) / (z - x))) xa \\ hypreal_of_real D)"; +\ ( *f* (%z. (f z - f x) / (z - x))) xa \\ hypreal_of_real D)"; by (auto_tac (claset(), simpset() addsimps [NSDERIV_NSLIM_iff2, NSLIM_def])); qed "NSDERIV_iff2"; @@ -867,7 +867,7 @@ Goal "(NSDERIV f x :> D) ==> \ \ (\\u. \ \ u \\ hypreal_of_real x --> \ -\ (*f* (%z. f z - f x)) u \\ hypreal_of_real D * (u - hypreal_of_real x))"; +\ ( *f* (%z. f z - f x)) u \\ hypreal_of_real D * (u - hypreal_of_real x))"; by (auto_tac (claset(), simpset() addsimps [NSDERIV_iff2])); by (case_tac "u = hypreal_of_real x" 1); by (auto_tac (claset(), simpset() addsimps [hypreal_diff_def])); @@ -876,7 +876,7 @@ by (dres_inst_tac [("c","u - hypreal_of_real x"),("b","hypreal_of_real D")] approx_mult1 1); by (ALLGOALS(dtac (hypreal_not_eq_minus_iff RS iffD1))); -by (subgoal_tac "(*f* (%z. z - x)) u \\ (0::hypreal)" 2); +by (subgoal_tac "( *f* (%z. z - x)) u \\ (0::hypreal)" 2); by (auto_tac (claset(), simpset() addsimps [real_diff_def, hypreal_diff_def, (approx_minus_iff RS iffD1) RS (mem_infmal_iff RS iffD2), @@ -885,7 +885,7 @@ Goal "(NSDERIV f x :> D) ==> \ \ (\\h \\ Infinitesimal. \ -\ ((*f* f)(hypreal_of_real x + h) - \ +\ (( *f* f)(hypreal_of_real x + h) - \ \ hypreal_of_real (f x))\\ (hypreal_of_real D) * h)"; by (auto_tac (claset(),simpset() addsimps [nsderiv_def])); by (case_tac "h = (0::hypreal)" 1); @@ -898,7 +898,7 @@ Goal "(NSDERIV f x :> D) ==> \ \ (\\h \\ Infinitesimal - {0}. \ -\ ((*f* f)(hypreal_of_real x + h) - \ +\ (( *f* f)(hypreal_of_real x + h) - \ \ hypreal_of_real (f x))\\ (hypreal_of_real D) * h)"; by (auto_tac (claset(),simpset() addsimps [nsderiv_def])); by (rtac ccontr 1 THEN dres_inst_tac [("x","h")] bspec 1); @@ -1114,13 +1114,13 @@ ---------------------------------------------------------------*) Goalw [increment_def] "f NSdifferentiable x ==> \ -\ increment f x h = (*f* f) (hypreal_of_real(x) + h) + \ +\ increment f x h = ( *f* f) (hypreal_of_real(x) + h) + \ \ -hypreal_of_real (f x)"; by (Blast_tac 1); qed "incrementI"; Goal "NSDERIV f x :> D ==> \ -\ increment f x h = (*f* f) (hypreal_of_real(x) + h) + \ +\ increment f x h = ( *f* f) (hypreal_of_real(x) + h) + \ \ -hypreal_of_real (f x)"; by (etac (NSdifferentiableI RS incrementI) 1); qed "incrementI2"; @@ -1133,7 +1133,7 @@ by (dtac (bex_Infinitesimal_iff2 RS iffD2) 1 THEN Step_tac 1); by (forw_inst_tac [("b1","hypreal_of_real(D) + y")] ((hypreal_mult_right_cancel RS iffD2)) 1); -by (thin_tac "((*f* f) (hypreal_of_real(x) + h) + \ +by (thin_tac "(( *f* f) (hypreal_of_real(x) + h) + \ \ - hypreal_of_real (f x)) / h = hypreal_of_real(D) + y" 2); by (assume_tac 1); by (asm_full_simp_tac (simpset() addsimps [hypreal_times_divide1_eq RS sym] @@ -1169,7 +1169,7 @@ (* lemmas *) Goalw [nsderiv_def] "[| NSDERIV g x :> D; \ -\ (*f* g) (hypreal_of_real(x) + xa) = hypreal_of_real(g x);\ +\ ( *f* g) (hypreal_of_real(x) + xa) = hypreal_of_real(g x);\ \ xa \\ Infinitesimal;\ \ xa \\ 0 \ \ |] ==> D = 0"; @@ -1180,7 +1180,7 @@ (* can be proved differently using NSLIM_isCont_iff *) Goalw [nsderiv_def] "[| NSDERIV f x :> D; h \\ Infinitesimal; h \\ 0 |] \ -\ ==> (*f* f) (hypreal_of_real(x) + h) + -hypreal_of_real(f x) \\ 0"; +\ ==> ( *f* f) (hypreal_of_real(x) + h) + -hypreal_of_real(f x) \\ 0"; by (asm_full_simp_tac (simpset() addsimps [mem_infmal_iff RS sym]) 1); by (rtac Infinitesimal_ratio 1); @@ -1196,11 +1196,11 @@ x - a ---------------------------------------------------------------*) Goal "[| NSDERIV f (g x) :> Da; \ -\ (*f* g) (hypreal_of_real(x) + xa) \\ hypreal_of_real (g x); \ -\ (*f* g) (hypreal_of_real(x) + xa) \\ hypreal_of_real (g x) \ -\ |] ==> ((*f* f) ((*f* g) (hypreal_of_real(x) + xa)) \ +\ ( *f* g) (hypreal_of_real(x) + xa) \\ hypreal_of_real (g x); \ +\ ( *f* g) (hypreal_of_real(x) + xa) \\ hypreal_of_real (g x) \ +\ |] ==> (( *f* f) (( *f* g) (hypreal_of_real(x) + xa)) \ \ + - hypreal_of_real (f (g x))) \ -\ / ((*f* g) (hypreal_of_real(x) + xa) + - hypreal_of_real (g x)) \ +\ / (( *f* g) (hypreal_of_real(x) + xa) + - hypreal_of_real (g x)) \ \ \\ hypreal_of_real(Da)"; by (auto_tac (claset(), simpset() addsimps [NSDERIV_NSLIM_iff2, NSLIM_def])); @@ -1214,7 +1214,7 @@ h --------------------------------------------------------------*) Goal "[| NSDERIV g x :> Db; xa \\ Infinitesimal; xa \\ 0 |] \ -\ ==> ((*f* g) (hypreal_of_real(x) + xa) + - hypreal_of_real(g x)) / xa \ +\ ==> (( *f* g) (hypreal_of_real(x) + xa) + - hypreal_of_real(g x)) / xa \ \ \\ hypreal_of_real(Db)"; by (auto_tac (claset(), simpset() addsimps [NSDERIV_NSLIM_iff, NSLIM_def, @@ -1235,10 +1235,10 @@ by (forw_inst_tac [("f","g")] NSDERIV_approx 1); by (auto_tac (claset(), simpset() addsimps [starfun_lambda_cancel2, starfun_o RS sym])); -by (case_tac "(*f* g) (hypreal_of_real(x) + xa) = hypreal_of_real (g x)" 1); +by (case_tac "( *f* g) (hypreal_of_real(x) + xa) = hypreal_of_real (g x)" 1); by (dres_inst_tac [("g","g")] NSDERIV_zero 1); by (auto_tac (claset(), simpset() addsimps [hypreal_divide_def])); -by (res_inst_tac [("z1","(*f* g) (hypreal_of_real(x) + xa) + -hypreal_of_real (g x)"), +by (res_inst_tac [("z1","( *f* g) (hypreal_of_real(x) + xa) + -hypreal_of_real (g x)"), ("y1","inverse xa")] (lemma_chain RS ssubst) 1); by (etac (hypreal_not_eq_minus_iff RS iffD1) 1); by (rtac approx_mult_hypreal_of_real 1); diff -r a4cd9057d2ee -r c3fbfd472365 src/HOL/Hyperreal/Lim.thy --- a/src/HOL/Hyperreal/Lim.thy Fri Feb 07 15:36:54 2003 +0100 +++ b/src/HOL/Hyperreal/Lim.thy Fri Feb 07 16:40:23 2003 +0100 @@ -23,7 +23,7 @@ ("((_)/ -- (_)/ --NS> (_))" [60, 0, 60] 60) "f -- a --NS> L == (ALL x. (x ~= hypreal_of_real a & x @= hypreal_of_real a --> - (*f* f) x @= hypreal_of_real L))" + ( *f* f) x @= hypreal_of_real L))" isCont :: [real=>real,real] => bool "isCont f a == (f -- a --> (f a))" @@ -31,7 +31,7 @@ (* NS definition dispenses with limit notions *) isNSCont :: [real=>real,real] => bool "isNSCont f a == (ALL y. y @= hypreal_of_real a --> - (*f* f) y @= hypreal_of_real (f a))" + ( *f* f) y @= hypreal_of_real (f a))" (* differentiation: D is derivative of function f at x *) deriv:: [real=>real,real,real] => bool @@ -41,7 +41,7 @@ nsderiv :: [real=>real,real,real] => bool ("(NSDERIV (_)/ (_)/ :> (_))" [60, 0, 60] 60) "NSDERIV f x :> D == (ALL h: Infinitesimal - {0}. - ((*f* f)(hypreal_of_real x + h) + + (( *f* f)(hypreal_of_real x + h) + - hypreal_of_real (f x))/h @= hypreal_of_real D)" differentiable :: [real=>real,real] => bool (infixl 60) @@ -52,7 +52,7 @@ increment :: [real=>real,real,hypreal] => hypreal "increment f x h == (@inc. f NSdifferentiable x & - inc = (*f* f)(hypreal_of_real x + h) + -hypreal_of_real (f x))" + inc = ( *f* f)(hypreal_of_real x + h) + -hypreal_of_real (f x))" isUCont :: (real=>real) => bool "isUCont f == (ALL r. 0 < r --> @@ -60,7 +60,7 @@ --> abs(f x + -f y) < r)))" isNSUCont :: (real=>real) => bool - "isNSUCont f == (ALL x y. x @= y --> (*f* f) x @= (*f* f) y)" + "isNSUCont f == (ALL x y. x @= y --> ( *f* f) x @= ( *f* f) y)" (*Used in the proof of the Bolzano theorem*) diff -r a4cd9057d2ee -r c3fbfd472365 src/HOL/Hyperreal/NatStar.ML --- a/src/HOL/Hyperreal/NatStar.ML Fri Feb 07 15:36:54 2003 +0100 +++ b/src/HOL/Hyperreal/NatStar.ML Fri Feb 07 16:40:23 2003 +0100 @@ -70,7 +70,7 @@ simpset() addsimps [starsetNat_n_Int RS sym])); qed "InternalNatSets_Int"; -Goalw [starsetNat_def] "*sNat* (-A) = -(*sNat* A)"; +Goalw [starsetNat_def] "*sNat* (-A) = -( *sNat* A)"; by (Auto_tac); by (res_inst_tac [("z","x")] eq_Abs_hypnat 1); by (res_inst_tac [("z","x")] eq_Abs_hypnat 2); @@ -78,7 +78,7 @@ by (TRYALL(Ultra_tac)); qed "NatStar_Compl"; -Goalw [starsetNat_n_def] "*sNatn* ((%n. - A n)) = -(*sNatn* A)"; +Goalw [starsetNat_n_def] "*sNatn* ((%n. - A n)) = -( *sNatn* A)"; by (Auto_tac); by (res_inst_tac [("z","x")] eq_Abs_hypnat 1); by (res_inst_tac [("z","x")] eq_Abs_hypnat 2); @@ -148,7 +148,7 @@ by Auto_tac; qed "starsetNat_starsetNat_n_eq"; -Goalw [InternalNatSets_def] "(*sNat* X) : InternalNatSets"; +Goalw [InternalNatSets_def] "( *sNat* X) : InternalNatSets"; by (auto_tac (claset(), simpset() addsimps [starsetNat_starsetNat_n_eq])); qed "InternalNatSets_starsetNat_n"; @@ -195,7 +195,7 @@ (* f::nat=>real *) Goalw [starfunNat_def] - "(*fNat* f) (Abs_hypnat(hypnatrel``{%n. X n})) = \ + "( *fNat* f) (Abs_hypnat(hypnatrel``{%n. X n})) = \ \ Abs_hypreal(hyprel `` {%n. f (X n)})"; by (res_inst_tac [("f","Abs_hypreal")] arg_cong 1); by (simp_tac (simpset() addsimps @@ -205,7 +205,7 @@ (* f::nat=>nat *) Goalw [starfunNat2_def] - "(*fNat2* f) (Abs_hypnat(hypnatrel``{%n. X n})) = \ + "( *fNat2* f) (Abs_hypnat(hypnatrel``{%n. X n})) = \ \ Abs_hypnat(hypnatrel `` {%n. f (X n)})"; by (res_inst_tac [("f","Abs_hypnat")] arg_cong 1); by (simp_tac (simpset() addsimps @@ -216,12 +216,12 @@ (*--------------------------------------------- multiplication: ( *f ) x ( *g ) = *(f x g) ---------------------------------------------*) -Goal "(*fNat* f) z * (*fNat* g) z = (*fNat* (%x. f x * g x)) z"; +Goal "( *fNat* f) z * ( *fNat* g) z = ( *fNat* (%x. f x * g x)) z"; by (res_inst_tac [("z","z")] eq_Abs_hypnat 1); by (auto_tac (claset(), simpset() addsimps [starfunNat,hypreal_mult])); qed "starfunNat_mult"; -Goal "(*fNat2* f) z * (*fNat2* g) z = (*fNat2* (%x. f x * g x)) z"; +Goal "( *fNat2* f) z * ( *fNat2* g) z = ( *fNat2* (%x. f x * g x)) z"; by (res_inst_tac [("z","z")] eq_Abs_hypnat 1); by (auto_tac (claset(), simpset() addsimps [starfunNat2,hypnat_mult])); qed "starfunNat2_mult"; @@ -229,17 +229,17 @@ (*--------------------------------------- addition: ( *f ) + ( *g ) = *(f + g) ---------------------------------------*) -Goal "(*fNat* f) z + (*fNat* g) z = (*fNat* (%x. f x + g x)) z"; +Goal "( *fNat* f) z + ( *fNat* g) z = ( *fNat* (%x. f x + g x)) z"; by (res_inst_tac [("z","z")] eq_Abs_hypnat 1); by (auto_tac (claset(), simpset() addsimps [starfunNat,hypreal_add])); qed "starfunNat_add"; -Goal "(*fNat2* f) z + (*fNat2* g) z = (*fNat2* (%x. f x + g x)) z"; +Goal "( *fNat2* f) z + ( *fNat2* g) z = ( *fNat2* (%x. f x + g x)) z"; by (res_inst_tac [("z","z")] eq_Abs_hypnat 1); by (auto_tac (claset(), simpset() addsimps [starfunNat2,hypnat_add])); qed "starfunNat2_add"; -Goal "(*fNat2* f) z - (*fNat2* g) z = (*fNat2* (%x. f x - g x)) z"; +Goal "( *fNat2* f) z - ( *fNat2* g) z = ( *fNat2* (%x. f x - g x)) z"; by (res_inst_tac [("z","z")] eq_Abs_hypnat 1); by (auto_tac (claset(), simpset() addsimps [starfunNat2, hypnat_minus])); qed "starfunNat2_minus"; @@ -249,18 +249,18 @@ ---------------------------------------*) (***** ( *f::nat=>real ) o ( *g::nat=>nat ) = *(f o g) *****) -Goal "(*fNat* f) o (*fNat2* g) = (*fNat* (f o g))"; +Goal "( *fNat* f) o ( *fNat2* g) = ( *fNat* (f o g))"; by (rtac ext 1); by (res_inst_tac [("z","x")] eq_Abs_hypnat 1); by (auto_tac (claset(), simpset() addsimps [starfunNat2, starfunNat])); qed "starfunNatNat2_o"; -Goal "(%x. (*fNat* f) ((*fNat2* g) x)) = (*fNat* (%x. f(g x)))"; +Goal "(%x. ( *fNat* f) (( *fNat2* g) x)) = ( *fNat* (%x. f(g x)))"; by (rtac ( simplify (simpset() addsimps [o_def]) starfunNatNat2_o) 1); qed "starfunNatNat2_o2"; (***** ( *f::nat=>nat ) o ( *g::nat=>nat ) = *(f o g) *****) -Goal "(*fNat2* f) o (*fNat2* g) = (*fNat2* (f o g))"; +Goal "( *fNat2* f) o ( *fNat2* g) = ( *fNat2* (f o g))"; by (rtac ext 1); by (res_inst_tac [("z","x")] eq_Abs_hypnat 1); by (auto_tac (claset(), simpset() addsimps [starfunNat2])); @@ -268,38 +268,38 @@ (***** ( *f::real=>real ) o ( *g::nat=>real ) = *(f o g) *****) -Goal "(*f* f) o (*fNat* g) = (*fNat* (f o g))"; +Goal "( *f* f) o ( *fNat* g) = ( *fNat* (f o g))"; by (rtac ext 1); by (res_inst_tac [("z","x")] eq_Abs_hypnat 1); by (auto_tac (claset(), simpset() addsimps [starfunNat,starfun])); qed "starfun_stafunNat_o"; -Goal "(%x. (*f* f) ((*fNat* g) x)) = (*fNat* (%x. f (g x)))"; +Goal "(%x. ( *f* f) (( *fNat* g) x)) = ( *fNat* (%x. f (g x)))"; by (rtac ( simplify (simpset() addsimps [o_def]) starfun_stafunNat_o) 1); qed "starfun_stafunNat_o2"; (*-------------------------------------- NS extension of constant function --------------------------------------*) -Goal "(*fNat* (%x. k)) z = hypreal_of_real k"; +Goal "( *fNat* (%x. k)) z = hypreal_of_real k"; by (res_inst_tac [("z","z")] eq_Abs_hypnat 1); by (auto_tac (claset(), simpset() addsimps [starfunNat, hypreal_of_real_def])); qed "starfunNat_const_fun"; Addsimps [starfunNat_const_fun]; -Goal "(*fNat2* (%x. k)) z = hypnat_of_nat k"; +Goal "( *fNat2* (%x. k)) z = hypnat_of_nat k"; by (res_inst_tac [("z","z")] eq_Abs_hypnat 1); by (auto_tac (claset(), simpset() addsimps [starfunNat2, hypnat_of_nat_def])); qed "starfunNat2_const_fun"; Addsimps [starfunNat2_const_fun]; -Goal "- (*fNat* f) x = (*fNat* (%x. - f x)) x"; +Goal "- ( *fNat* f) x = ( *fNat* (%x. - f x)) x"; by (res_inst_tac [("z","x")] eq_Abs_hypnat 1); by (auto_tac (claset(), simpset() addsimps [starfunNat, hypreal_minus])); qed "starfunNat_minus"; -Goal "inverse ((*fNat* f) x) = (*fNat* (%x. inverse (f x))) x"; +Goal "inverse (( *fNat* f) x) = ( *fNat* (%x. inverse (f x))) x"; by (res_inst_tac [("z","x")] eq_Abs_hypnat 1); by (auto_tac (claset(), simpset() addsimps [starfunNat, hypreal_inverse])); qed "starfunNat_inverse"; @@ -310,20 +310,20 @@ for all natural arguments (c.f. Hoskins pg. 107- SEQ) -------------------------------------------------------*) -Goal "(*fNat* f) (hypnat_of_nat a) = hypreal_of_real (f a)"; +Goal "( *fNat* f) (hypnat_of_nat a) = hypreal_of_real (f a)"; by (auto_tac (claset(), simpset() addsimps [starfunNat,hypnat_of_nat_def,hypreal_of_real_def])); qed "starfunNat_eq"; Addsimps [starfunNat_eq]; -Goal "(*fNat2* f) (hypnat_of_nat a) = hypnat_of_nat (f a)"; +Goal "( *fNat2* f) (hypnat_of_nat a) = hypnat_of_nat (f a)"; by (auto_tac (claset(), simpset() addsimps [starfunNat2,hypnat_of_nat_def])); qed "starfunNat2_eq"; Addsimps [starfunNat2_eq]; -Goal "(*fNat* f) (hypnat_of_nat a) @= hypreal_of_real (f a)"; +Goal "( *fNat* f) (hypnat_of_nat a) @= hypreal_of_real (f a)"; by (Auto_tac); qed "starfunNat_approx"; @@ -333,7 +333,7 @@ --- used for limit comparison of sequences ----------------------------------------------------------------*) Goal "ALL n. N <= n --> f n <= g n \ -\ ==> ALL n. hypnat_of_nat N <= n --> (*fNat* f) n <= (*fNat* g) n"; +\ ==> ALL n. hypnat_of_nat N <= n --> ( *fNat* f) n <= ( *fNat* g) n"; by (Step_tac 1); by (res_inst_tac [("z","n")] eq_Abs_hypnat 1); by (auto_tac (claset(), @@ -345,7 +345,7 @@ (*****----- and another -----*****) Goal "ALL n. N <= n --> f n < g n \ -\ ==> ALL n. hypnat_of_nat N <= n --> (*fNat* f) n < (*fNat* g) n"; +\ ==> ALL n. hypnat_of_nat N <= n --> ( *fNat* f) n < ( *fNat* g) n"; by (Step_tac 1); by (res_inst_tac [("z","n")] eq_Abs_hypnat 1); by (auto_tac (claset(), @@ -358,7 +358,7 @@ (*---------------------------------------------------------------- NS extension when we displace argument by one ---------------------------------------------------------------*) -Goal "(*fNat* (%n. f (Suc n))) N = (*fNat* f) (N + (1::hypnat))"; +Goal "( *fNat* (%n. f (Suc n))) N = ( *fNat* f) (N + (1::hypnat))"; by (res_inst_tac [("z","N")] eq_Abs_hypnat 1); by (auto_tac (claset(), simpset() addsimps [starfunNat, hypnat_one_def,hypnat_add])); @@ -367,7 +367,7 @@ (*---------------------------------------------------------------- NS extension with rabs ---------------------------------------------------------------*) -Goal "(*fNat* (%n. abs (f n))) N = abs((*fNat* f) N)"; +Goal "( *fNat* (%n. abs (f n))) N = abs(( *fNat* f) N)"; by (res_inst_tac [("z","N")] eq_Abs_hypnat 1); by (auto_tac (claset(), simpset() addsimps [starfunNat, hypreal_hrabs])); qed "starfunNat_rabs"; @@ -375,19 +375,19 @@ (*---------------------------------------------------------------- The hyperpow function as a NS extension of realpow ----------------------------------------------------------------*) -Goal "(*fNat* (%n. r ^ n)) N = (hypreal_of_real r) pow N"; +Goal "( *fNat* (%n. r ^ n)) N = (hypreal_of_real r) pow N"; by (res_inst_tac [("z","N")] eq_Abs_hypnat 1); by (auto_tac (claset(), simpset() addsimps [hyperpow, hypreal_of_real_def,starfunNat])); qed "starfunNat_pow"; -Goal "(*fNat* (%n. (X n) ^ m)) N = (*fNat* X) N pow hypnat_of_nat m"; +Goal "( *fNat* (%n. (X n) ^ m)) N = ( *fNat* X) N pow hypnat_of_nat m"; by (res_inst_tac [("z","N")] eq_Abs_hypnat 1); by (auto_tac (claset(), simpset() addsimps [hyperpow, hypnat_of_nat_def,starfunNat])); qed "starfunNat_pow2"; -Goalw [hypnat_of_nat_def] "(*f* (%r. r ^ n)) R = (R) pow hypnat_of_nat n"; +Goalw [hypnat_of_nat_def] "( *f* (%r. r ^ n)) R = (R) pow hypnat_of_nat n"; by (res_inst_tac [("z","R")] eq_Abs_hypreal 1); by (auto_tac (claset(), simpset() addsimps [hyperpow,starfun])); qed "starfun_pow"; @@ -395,14 +395,14 @@ (*----------------------------------------------------- hypreal_of_hypnat as NS extension of real (from "nat")! -------------------------------------------------------*) -Goal "(*fNat* real) = hypreal_of_hypnat"; +Goal "( *fNat* real) = hypreal_of_hypnat"; by (rtac ext 1); by (res_inst_tac [("z","x")] eq_Abs_hypnat 1); by (auto_tac (claset(), simpset() addsimps [hypreal_of_hypnat,starfunNat])); qed "starfunNat_real_of_nat"; Goal "N : HNatInfinite \ -\ ==> (*fNat* (%x::nat. inverse(real x))) N = inverse(hypreal_of_hypnat N)"; +\ ==> ( *fNat* (%x::nat. inverse(real x))) N = inverse(hypreal_of_hypnat N)"; by (res_inst_tac [("f1","inverse")] (starfun_stafunNat_o2 RS subst) 1); by (subgoal_tac "hypreal_of_hypnat N ~= 0" 1); by (auto_tac (claset(), @@ -419,7 +419,7 @@ qed "starfunNat_n_congruent"; Goalw [starfunNat_n_def] - "(*fNatn* f) (Abs_hypnat(hypnatrel``{%n. X n})) = \ + "( *fNatn* f) (Abs_hypnat(hypnatrel``{%n. X n})) = \ \ Abs_hypreal(hyprel `` {%n. f n (X n)})"; by (res_inst_tac [("f","Abs_hypreal")] arg_cong 1); by Auto_tac; @@ -429,7 +429,7 @@ (*------------------------------------------------- multiplication: ( *fn ) x ( *gn ) = *(fn x gn) -------------------------------------------------*) -Goal "(*fNatn* f) z * (*fNatn* g) z = (*fNatn* (% i x. f i x * g i x)) z"; +Goal "( *fNatn* f) z * ( *fNatn* g) z = ( *fNatn* (% i x. f i x * g i x)) z"; by (res_inst_tac [("z","z")] eq_Abs_hypnat 1); by (auto_tac (claset(), simpset() addsimps [starfunNat_n,hypreal_mult])); qed "starfunNat_n_mult"; @@ -437,7 +437,7 @@ (*----------------------------------------------- addition: ( *fn ) + ( *gn ) = *(fn + gn) -----------------------------------------------*) -Goal "(*fNatn* f) z + (*fNatn* g) z = (*fNatn* (%i x. f i x + g i x)) z"; +Goal "( *fNatn* f) z + ( *fNatn* g) z = ( *fNatn* (%i x. f i x + g i x)) z"; by (res_inst_tac [("z","z")] eq_Abs_hypnat 1); by (auto_tac (claset(), simpset() addsimps [starfunNat_n,hypreal_add])); qed "starfunNat_n_add"; @@ -445,7 +445,7 @@ (*------------------------------------------------- subtraction: ( *fn ) + -( *gn ) = *(fn + -gn) -------------------------------------------------*) -Goal "(*fNatn* f) z + -(*fNatn* g) z = (*fNatn* (%i x. f i x + -g i x)) z"; +Goal "( *fNatn* f) z + -( *fNatn* g) z = ( *fNatn* (%i x. f i x + -g i x)) z"; by (res_inst_tac [("z","z")] eq_Abs_hypnat 1); by (auto_tac (claset(), simpset() addsimps [starfunNat_n, hypreal_minus,hypreal_add])); @@ -455,7 +455,7 @@ composition: ( *fn ) o ( *gn ) = *(fn o gn) -------------------------------------------------*) -Goal "(*fNatn* (%i x. k)) z = hypreal_of_real k"; +Goal "( *fNatn* (%i x. k)) z = hypreal_of_real k"; by (res_inst_tac [("z","z")] eq_Abs_hypnat 1); by (auto_tac (claset(), simpset() addsimps [starfunNat_n, hypreal_of_real_def])); @@ -463,17 +463,17 @@ Addsimps [starfunNat_n_const_fun]; -Goal "- (*fNatn* f) x = (*fNatn* (%i x. - (f i) x)) x"; +Goal "- ( *fNatn* f) x = ( *fNatn* (%i x. - (f i) x)) x"; by (res_inst_tac [("z","x")] eq_Abs_hypnat 1); by (auto_tac (claset(), simpset() addsimps [starfunNat_n, hypreal_minus])); qed "starfunNat_n_minus"; -Goal "(*fNatn* f) (hypnat_of_nat n) = Abs_hypreal(hyprel `` {%i. f i n})"; +Goal "( *fNatn* f) (hypnat_of_nat n) = Abs_hypreal(hyprel `` {%i. f i n})"; by (auto_tac (claset(), simpset() addsimps [starfunNat_n,hypnat_of_nat_def])); qed "starfunNat_n_eq"; Addsimps [starfunNat_n_eq]; -Goal "((*fNat* f) = (*fNat* g)) = (f = g)"; +Goal "(( *fNat* f) = ( *fNat* g)) = (f = g)"; by Auto_tac; by (rtac ext 1 THEN rtac ccontr 1); by (dres_inst_tac [("x","hypnat_of_nat(x)")] fun_cong 1); diff -r a4cd9057d2ee -r c3fbfd472365 src/HOL/Hyperreal/SEQ.ML --- a/src/HOL/Hyperreal/SEQ.ML Fri Feb 07 15:36:54 2003 +0100 +++ b/src/HOL/Hyperreal/SEQ.ML Fri Feb 07 16:40:23 2003 +0100 @@ -11,7 +11,7 @@ -------------------------------------------------------------------------- *) Goalw [hypnat_omega_def] - "(*fNat* (%n::nat. inverse(real(Suc n)))) whn : Infinitesimal"; + "( *fNat* (%n::nat. inverse(real(Suc n)))) whn : Infinitesimal"; by (auto_tac (claset(), simpset() addsimps [Infinitesimal_FreeUltrafilterNat_iff,starfunNat])); by (rtac bexI 1 THEN rtac lemma_hyprel_refl 2); @@ -31,7 +31,7 @@ qed "LIMSEQ_iff"; Goalw [NSLIMSEQ_def] - "(X ----NS> L) = (ALL N: HNatInfinite. (*fNat* X) N @= hypreal_of_real L)"; + "(X ----NS> L) = (ALL N: HNatInfinite. ( *fNat* X) N @= hypreal_of_real L)"; by (Simp_tac 1); qed "NSLIMSEQ_iff"; @@ -121,7 +121,7 @@ val lemmaLIM2 = result(); Goal "[| 0 < r; ALL n. r <= abs (X (f n) + - L); \ -\ (*fNat* X) (Abs_hypnat (hypnatrel `` {f})) + \ +\ ( *fNat* X) (Abs_hypnat (hypnatrel `` {f})) + \ \ - hypreal_of_real L @= 0 |] ==> False"; by (auto_tac (claset(),simpset() addsimps [starfunNat, mem_infmal_iff RS sym,hypreal_of_real_def, @@ -419,12 +419,12 @@ qed "Bseq_iff1a"; Goalw [NSBseq_def] - "[| NSBseq X; N: HNatInfinite |] ==> (*fNat* X) N : HFinite"; + "[| NSBseq X; N: HNatInfinite |] ==> ( *fNat* X) N : HFinite"; by (Blast_tac 1); qed "NSBseqD"; Goalw [NSBseq_def] - "ALL N: HNatInfinite. (*fNat* X) N : HFinite ==> NSBseq X"; + "ALL N: HNatInfinite. ( *fNat* X) N : HFinite ==> NSBseq X"; by (assume_tac 1); qed "NSBseqI"; diff -r a4cd9057d2ee -r c3fbfd472365 src/HOL/Hyperreal/SEQ.thy --- a/src/HOL/Hyperreal/SEQ.thy Fri Feb 07 15:36:54 2003 +0100 +++ b/src/HOL/Hyperreal/SEQ.thy Fri Feb 07 16:40:23 2003 +0100 @@ -14,7 +14,7 @@ (* Nonstandard definition of convergence of sequence *) NSLIMSEQ :: [nat=>real,real] => bool ("((_)/ ----NS> (_))" [60, 60] 60) - "X ----NS> L == (ALL N: HNatInfinite. (*fNat* X) N @= hypreal_of_real L)" + "X ----NS> L == (ALL N: HNatInfinite. ( *fNat* X) N @= hypreal_of_real L)" (* define value of limit using choice operator*) lim :: (nat => real) => real @@ -37,7 +37,7 @@ (* Nonstandard definition for bounded sequence *) NSBseq :: (nat=>real) => bool - "NSBseq X == (ALL N: HNatInfinite. (*fNat* X) N : HFinite)" + "NSBseq X == (ALL N: HNatInfinite. ( *fNat* X) N : HFinite)" (* Definition for monotonicity *) monoseq :: (nat=>real)=>bool @@ -58,6 +58,6 @@ NSCauchy :: (nat => real) => bool "NSCauchy X == (ALL M: HNatInfinite. ALL N: HNatInfinite. - (*fNat* X) M @= (*fNat* X) N)" + ( *fNat* X) M @= ( *fNat* X) N)" end diff -r a4cd9057d2ee -r c3fbfd472365 src/HOL/Hyperreal/Star.ML --- a/src/HOL/Hyperreal/Star.ML Fri Feb 07 15:36:54 2003 +0100 +++ b/src/HOL/Hyperreal/Star.ML Fri Feb 07 16:40:23 2003 +0100 @@ -51,7 +51,7 @@ by (REPEAT(blast_tac (claset() addIs [FreeUltrafilterNat_subset]) 1)); qed "STAR_Int"; -Goalw [starset_def] "*s* -A = -(*s* A)"; +Goalw [starset_def] "*s* -A = -( *s* A)"; by (Auto_tac); by (res_inst_tac [("z","x")] eq_Abs_hypreal 1); by (res_inst_tac [("z","x")] eq_Abs_hypreal 2); @@ -198,7 +198,7 @@ qed "starfun_congruent"; Goalw [starfun_def] - "(*f* f) (Abs_hypreal(hyprel``{%n. X n})) = \ + "( *f* f) (Abs_hypreal(hyprel``{%n. X n})) = \ \ Abs_hypreal(hyprel `` {%n. f (X n)})"; by (res_inst_tac [("f","Abs_hypreal")] arg_cong 1); by (simp_tac (simpset() addsimps @@ -209,7 +209,7 @@ (*------------------------------------------- multiplication: ( *f ) x ( *g ) = *(f x g) ------------------------------------------*) -Goal "(*f* f) xa * (*f* g) xa = (*f* (%x. f x * g x)) xa"; +Goal "( *f* f) xa * ( *f* g) xa = ( *f* (%x. f x * g x)) xa"; by (res_inst_tac [("z","xa")] eq_Abs_hypreal 1); by (auto_tac (claset(),simpset() addsimps [starfun,hypreal_mult])); qed "starfun_mult"; @@ -218,7 +218,7 @@ (*--------------------------------------- addition: ( *f ) + ( *g ) = *(f + g) ---------------------------------------*) -Goal "(*f* f) xa + (*f* g) xa = (*f* (%x. f x + g x)) xa"; +Goal "( *f* f) xa + ( *f* g) xa = ( *f* (%x. f x + g x)) xa"; by (res_inst_tac [("z","xa")] eq_Abs_hypreal 1); by (auto_tac (claset(),simpset() addsimps [starfun,hypreal_add])); qed "starfun_add"; @@ -228,20 +228,20 @@ subtraction: ( *f ) + -( *g ) = *(f + -g) -------------------------------------------*) -Goal "- (*f* f) x = (*f* (%x. - f x)) x"; +Goal "- ( *f* f) x = ( *f* (%x. - f x)) x"; by (res_inst_tac [("z","x")] eq_Abs_hypreal 1); by (auto_tac (claset(),simpset() addsimps [starfun, hypreal_minus])); qed "starfun_minus"; Addsimps [starfun_minus RS sym]; (*FIXME: delete*) -Goal "(*f* f) xa + -(*f* g) xa = (*f* (%x. f x + -g x)) xa"; +Goal "( *f* f) xa + -( *f* g) xa = ( *f* (%x. f x + -g x)) xa"; by (Simp_tac 1); qed "starfun_add_minus"; Addsimps [starfun_add_minus RS sym]; Goalw [hypreal_diff_def,real_diff_def] - "(*f* f) xa - (*f* g) xa = (*f* (%x. f x - g x)) xa"; + "( *f* f) xa - ( *f* g) xa = ( *f* (%x. f x - g x)) xa"; by (rtac starfun_add_minus 1); qed "starfun_diff"; Addsimps [starfun_diff RS sym]; @@ -250,20 +250,20 @@ composition: ( *f ) o ( *g ) = *(f o g) ---------------------------------------*) -Goal "(%x. (*f* f) ((*f* g) x)) = *f* (%x. f (g x))"; +Goal "(%x. ( *f* f) (( *f* g) x)) = *f* (%x. f (g x))"; by (rtac ext 1); by (res_inst_tac [("z","x")] eq_Abs_hypreal 1); by (auto_tac (claset(),simpset() addsimps [starfun])); qed "starfun_o2"; -Goalw [o_def] "(*f* f) o (*f* g) = (*f* (f o g))"; +Goalw [o_def] "( *f* f) o ( *f* g) = ( *f* (f o g))"; by (simp_tac (simpset() addsimps [starfun_o2]) 1); qed "starfun_o"; (*-------------------------------------- NS extension of constant function --------------------------------------*) -Goal "(*f* (%x. k)) xa = hypreal_of_real k"; +Goal "( *f* (%x. k)) xa = hypreal_of_real k"; by (res_inst_tac [("z","xa")] eq_Abs_hypreal 1); by (auto_tac (claset(),simpset() addsimps [starfun, hypreal_of_real_def])); @@ -275,12 +275,12 @@ the NS extension of the identity function ----------------------------------------------------*) -Goal "x @= hypreal_of_real a ==> (*f* (%x. x)) x @= hypreal_of_real a"; +Goal "x @= hypreal_of_real a ==> ( *f* (%x. x)) x @= hypreal_of_real a"; by (res_inst_tac [("z","x")] eq_Abs_hypreal 1); by (auto_tac (claset(),simpset() addsimps [starfun])); qed "starfun_Idfun_approx"; -Goal "(*f* (%x. x)) x = x"; +Goal "( *f* (%x. x)) x = x"; by (res_inst_tac [("z","x")] eq_Abs_hypreal 1); by (auto_tac (claset(),simpset() addsimps [starfun])); qed "starfun_Id"; @@ -290,7 +290,7 @@ the *-function is a (nonstandard) extension of the function ----------------------------------------------------------------------*) -Goalw [is_starext_def] "is_starext (*f* f) f"; +Goalw [is_starext_def] "is_starext ( *f* f) f"; by (Auto_tac); by (res_inst_tac [("z","x")] eq_Abs_hypreal 1); by (res_inst_tac [("z","y")] eq_Abs_hypreal 1); @@ -305,7 +305,7 @@ by (rtac ext 1); by (res_inst_tac [("z","x")] eq_Abs_hypreal 1); by (dres_inst_tac [("x","x")] spec 1); -by (dres_inst_tac [("x","(*f* f) x")] spec 1); +by (dres_inst_tac [("x","( *f* f) x")] spec 1); by (auto_tac (claset() addSDs [FreeUltrafilterNat_Compl_mem], simpset() addsimps [starfun])); by (Fuf_empty_tac 1); @@ -320,41 +320,41 @@ version for real arguments. i.e they are the same for all real arguments -------------------------------------------------------*) -Goal "(*f* f) (hypreal_of_real a) = hypreal_of_real (f a)"; +Goal "( *f* f) (hypreal_of_real a) = hypreal_of_real (f a)"; by (auto_tac (claset(),simpset() addsimps [starfun,hypreal_of_real_def])); qed "starfun_eq"; Addsimps [starfun_eq]; -Goal "(*f* f) (hypreal_of_real a) @= hypreal_of_real (f a)"; +Goal "( *f* f) (hypreal_of_real a) @= hypreal_of_real (f a)"; by (Auto_tac); qed "starfun_approx"; (* useful for NS definition of derivatives *) -Goal "(*f* (%h. f (x + h))) xa = (*f* f) (hypreal_of_real x + xa)"; +Goal "( *f* (%h. f (x + h))) xa = ( *f* f) (hypreal_of_real x + xa)"; by (res_inst_tac [("z","xa")] eq_Abs_hypreal 1); by (auto_tac (claset(),simpset() addsimps [starfun, hypreal_of_real_def,hypreal_add])); qed "starfun_lambda_cancel"; -Goal "(*f* (%h. f(g(x + h)))) xa = (*f* (f o g)) (hypreal_of_real x + xa)"; +Goal "( *f* (%h. f(g(x + h)))) xa = ( *f* (f o g)) (hypreal_of_real x + xa)"; by (res_inst_tac [("z","xa")] eq_Abs_hypreal 1); by (auto_tac (claset(),simpset() addsimps [starfun, hypreal_of_real_def,hypreal_add])); qed "starfun_lambda_cancel2"; -Goal "[| (*f* f) xa @= l; (*f* g) xa @= m; \ +Goal "[| ( *f* f) xa @= l; ( *f* g) xa @= m; \ \ l: HFinite; m: HFinite \ -\ |] ==> (*f* (%x. f x * g x)) xa @= l * m"; +\ |] ==> ( *f* (%x. f x * g x)) xa @= l * m"; by (dtac approx_mult_HFinite 1); by (REPEAT(assume_tac 1)); by (auto_tac (claset() addIs [approx_sym RSN (2,approx_HFinite)], simpset())); qed "starfun_mult_HFinite_approx"; -Goal "[| (*f* f) xa @= l; (*f* g) xa @= m \ -\ |] ==> (*f* (%x. f x + g x)) xa @= l + m"; +Goal "[| ( *f* f) xa @= l; ( *f* g) xa @= m \ +\ |] ==> ( *f* (%x. f x + g x)) xa @= l + m"; by (auto_tac (claset() addIs [approx_add], simpset())); qed "starfun_add_approx"; @@ -372,14 +372,14 @@ (is_starext_starfun_iff RS iffD1) RS sym) 1); qed "starfun_rabs_hrabs"; -Goal "(*f* inverse) x = inverse(x)"; +Goal "( *f* inverse) x = inverse(x)"; by (res_inst_tac [("z","x")] eq_Abs_hypreal 1); by (auto_tac (claset(), simpset() addsimps [starfun, hypreal_inverse, hypreal_zero_def])); qed "starfun_inverse_inverse"; Addsimps [starfun_inverse_inverse]; -Goal "inverse ((*f* f) x) = (*f* (%x. inverse (f x))) x"; +Goal "inverse (( *f* f) x) = ( *f* (%x. inverse (f x))) x"; by (res_inst_tac [("z","x")] eq_Abs_hypreal 1); by (auto_tac (claset(), simpset() addsimps [starfun, hypreal_inverse])); @@ -387,12 +387,12 @@ Addsimps [starfun_inverse RS sym]; Goalw [hypreal_divide_def,real_divide_def] - "(*f* f) xa / (*f* g) xa = (*f* (%x. f x / g x)) xa"; + "( *f* f) xa / ( *f* g) xa = ( *f* (%x. f x / g x)) xa"; by Auto_tac; qed "starfun_divide"; Addsimps [starfun_divide RS sym]; -Goal "inverse ((*f* f) x) = (*f* (%x. inverse (f x))) x"; +Goal "inverse (( *f* f) x) = ( *f* (%x. inverse (f x))) x"; by (res_inst_tac [("z","x")] eq_Abs_hypreal 1); by (auto_tac (claset() addIs [FreeUltrafilterNat_subset] addSDs [FreeUltrafilterNat_Compl_mem], @@ -404,7 +404,7 @@ topology of the reals ------------------------------------------------------------*) Goalw [starset_def] - "(*f* f) x : *s* A ==> x : *s* {x. f x : A}"; + "( *f* f) x : *s* A ==> x : *s* {x. f x : A}"; by (res_inst_tac [("z","x")] eq_Abs_hypreal 1); by (auto_tac (claset(),simpset() addsimps [starfun])); by (dres_inst_tac [("x","%n. f (Xa n)")] bspec 1); @@ -440,7 +440,7 @@ Goalw [starset_def] "*s* {x. abs (f x + - y) < r} = \ -\ {x. abs((*f* f) x + -hypreal_of_real y) < hypreal_of_real r}"; +\ {x. abs(( *f* f) x + -hypreal_of_real y) < hypreal_of_real r}"; by (Step_tac 1); by (ALLGOALS(res_inst_tac [("z","x")] eq_Abs_hypreal)); by (auto_tac (claset() addSIs [exI] addSDs [bspec],