--- 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]));
--- 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";
--- 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 \\<approx> hypreal_of_real a |] \
-\ ==> (*f* f) y \\<approx> hypreal_of_real (f a)";
+\ ==> ( *f* f) y \\<approx> hypreal_of_real (f a)";
by (Blast_tac 1);
qed "isNSContD";
@@ -662,7 +662,7 @@
Uniform continuity
------------------------------------------------------------------*)
Goalw [isNSUCont_def]
- "[| isNSUCont f; x \\<approx> y|] ==> (*f* f) x \\<approx> (*f* f) y";
+ "[| isNSUCont f; x \\<approx> y|] ==> ( *f* f) x \\<approx> ( *f* f) y";
by (Blast_tac 1);
qed "isNSUContD";
@@ -859,7 +859,7 @@
"(NSDERIV f x :> D) = \
\ (\\<forall>xa. \
\ xa \\<noteq> hypreal_of_real x & xa \\<approx> hypreal_of_real x --> \
-\ (*f* (%z. (f z - f x) / (z - x))) xa \\<approx> hypreal_of_real D)";
+\ ( *f* (%z. (f z - f x) / (z - x))) xa \\<approx> 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) ==> \
\ (\\<forall>u. \
\ u \\<approx> hypreal_of_real x --> \
-\ (*f* (%z. f z - f x)) u \\<approx> hypreal_of_real D * (u - hypreal_of_real x))";
+\ ( *f* (%z. f z - f x)) u \\<approx> 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 \\<noteq> (0::hypreal)" 2);
+by (subgoal_tac "( *f* (%z. z - x)) u \\<noteq> (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) ==> \
\ (\\<forall>h \\<in> Infinitesimal. \
-\ ((*f* f)(hypreal_of_real x + h) - \
+\ (( *f* f)(hypreal_of_real x + h) - \
\ hypreal_of_real (f x))\\<approx> (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) ==> \
\ (\\<forall>h \\<in> Infinitesimal - {0}. \
-\ ((*f* f)(hypreal_of_real x + h) - \
+\ (( *f* f)(hypreal_of_real x + h) - \
\ hypreal_of_real (f x))\\<approx> (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 \\<in> Infinitesimal;\
\ xa \\<noteq> 0 \
\ |] ==> D = 0";
@@ -1180,7 +1180,7 @@
(* can be proved differently using NSLIM_isCont_iff *)
Goalw [nsderiv_def]
"[| NSDERIV f x :> D; h \\<in> Infinitesimal; h \\<noteq> 0 |] \
-\ ==> (*f* f) (hypreal_of_real(x) + h) + -hypreal_of_real(f x) \\<approx> 0";
+\ ==> ( *f* f) (hypreal_of_real(x) + h) + -hypreal_of_real(f x) \\<approx> 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) \\<noteq> hypreal_of_real (g x); \
-\ (*f* g) (hypreal_of_real(x) + xa) \\<approx> hypreal_of_real (g x) \
-\ |] ==> ((*f* f) ((*f* g) (hypreal_of_real(x) + xa)) \
+\ ( *f* g) (hypreal_of_real(x) + xa) \\<noteq> hypreal_of_real (g x); \
+\ ( *f* g) (hypreal_of_real(x) + xa) \\<approx> 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)) \
\ \\<approx> 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 \\<in> Infinitesimal; xa \\<noteq> 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 \
\ \\<approx> 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);
--- 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*)
--- 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);
--- 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";
--- 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
--- 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],