--- 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);