src/HOL/Hyperreal/Lim.ML
changeset 13810 c3fbfd472365
parent 13630 a013a9dd370f
child 14262 e7db45b74b3a
     1.1 --- a/src/HOL/Hyperreal/Lim.ML	Fri Feb 07 15:36:54 2003 +0100
     1.2 +++ b/src/HOL/Hyperreal/Lim.ML	Fri Feb 07 16:40:23 2003 +0100
     1.3 @@ -438,7 +438,7 @@
     1.4  
     1.5  Goalw [isNSCont_def] 
     1.6        "[| isNSCont f a; y \\<approx> hypreal_of_real a |] \
     1.7 -\           ==> (*f* f) y \\<approx> hypreal_of_real (f a)";
     1.8 +\           ==> ( *f* f) y \\<approx> hypreal_of_real (f a)";
     1.9  by (Blast_tac 1);
    1.10  qed "isNSContD";
    1.11  
    1.12 @@ -662,7 +662,7 @@
    1.13                          Uniform continuity
    1.14   ------------------------------------------------------------------*)
    1.15  Goalw [isNSUCont_def] 
    1.16 -      "[| isNSUCont f; x \\<approx> y|] ==> (*f* f) x \\<approx> (*f* f) y";
    1.17 +      "[| isNSUCont f; x \\<approx> y|] ==> ( *f* f) x \\<approx> ( *f* f) y";
    1.18  by (Blast_tac 1);
    1.19  qed "isNSUContD";
    1.20  
    1.21 @@ -859,7 +859,7 @@
    1.22       "(NSDERIV f x :> D) = \
    1.23  \     (\\<forall>xa. \
    1.24  \       xa \\<noteq> hypreal_of_real x & xa \\<approx> hypreal_of_real x --> \
    1.25 -\       (*f* (%z. (f z - f x) / (z - x))) xa \\<approx> hypreal_of_real D)";
    1.26 +\       ( *f* (%z. (f z - f x) / (z - x))) xa \\<approx> hypreal_of_real D)";
    1.27  by (auto_tac (claset(), simpset() addsimps [NSDERIV_NSLIM_iff2, NSLIM_def]));
    1.28  qed "NSDERIV_iff2";
    1.29  
    1.30 @@ -867,7 +867,7 @@
    1.31  Goal "(NSDERIV f x :> D) ==> \
    1.32  \    (\\<forall>u. \
    1.33  \       u \\<approx> hypreal_of_real x --> \
    1.34 -\       (*f* (%z. f z - f x)) u \\<approx> hypreal_of_real D * (u - hypreal_of_real x))";
    1.35 +\       ( *f* (%z. f z - f x)) u \\<approx> hypreal_of_real D * (u - hypreal_of_real x))";
    1.36  by (auto_tac (claset(), simpset() addsimps [NSDERIV_iff2]));
    1.37  by (case_tac "u = hypreal_of_real x" 1);
    1.38  by (auto_tac (claset(), simpset() addsimps [hypreal_diff_def]));
    1.39 @@ -876,7 +876,7 @@
    1.40  by (dres_inst_tac [("c","u - hypreal_of_real x"),("b","hypreal_of_real D")]
    1.41       approx_mult1 1);
    1.42  by (ALLGOALS(dtac (hypreal_not_eq_minus_iff RS iffD1)));
    1.43 -by (subgoal_tac "(*f* (%z. z - x)) u \\<noteq> (0::hypreal)" 2);
    1.44 +by (subgoal_tac "( *f* (%z. z - x)) u \\<noteq> (0::hypreal)" 2);
    1.45  by (auto_tac (claset(),
    1.46      simpset() addsimps [real_diff_def, hypreal_diff_def, 
    1.47  		(approx_minus_iff RS iffD1) RS (mem_infmal_iff RS iffD2),  
    1.48 @@ -885,7 +885,7 @@
    1.49  
    1.50  Goal "(NSDERIV f x :> D) ==> \
    1.51  \     (\\<forall>h \\<in> Infinitesimal. \
    1.52 -\              ((*f* f)(hypreal_of_real x + h) - \
    1.53 +\              (( *f* f)(hypreal_of_real x + h) - \
    1.54  \                hypreal_of_real (f x))\\<approx> (hypreal_of_real D) * h)";
    1.55  by (auto_tac (claset(),simpset() addsimps [nsderiv_def]));
    1.56  by (case_tac "h = (0::hypreal)" 1);
    1.57 @@ -898,7 +898,7 @@
    1.58  
    1.59  Goal "(NSDERIV f x :> D) ==> \
    1.60  \     (\\<forall>h \\<in> Infinitesimal - {0}. \
    1.61 -\              ((*f* f)(hypreal_of_real x + h) - \
    1.62 +\              (( *f* f)(hypreal_of_real x + h) - \
    1.63  \                hypreal_of_real (f x))\\<approx> (hypreal_of_real D) * h)";
    1.64  by (auto_tac (claset(),simpset() addsimps [nsderiv_def]));
    1.65  by (rtac ccontr 1 THEN dres_inst_tac [("x","h")] bspec 1);
    1.66 @@ -1114,13 +1114,13 @@
    1.67   ---------------------------------------------------------------*)
    1.68  Goalw [increment_def] 
    1.69        "f NSdifferentiable x ==> \
    1.70 -\     increment f x h = (*f* f) (hypreal_of_real(x) + h) + \
    1.71 +\     increment f x h = ( *f* f) (hypreal_of_real(x) + h) + \
    1.72  \     -hypreal_of_real (f x)";
    1.73  by (Blast_tac 1);
    1.74  qed "incrementI";
    1.75  
    1.76  Goal "NSDERIV f x :> D ==> \
    1.77 -\    increment f x h = (*f* f) (hypreal_of_real(x) + h) + \
    1.78 +\    increment f x h = ( *f* f) (hypreal_of_real(x) + h) + \
    1.79  \    -hypreal_of_real (f x)";
    1.80  by (etac (NSdifferentiableI RS incrementI) 1);
    1.81  qed "incrementI2";
    1.82 @@ -1133,7 +1133,7 @@
    1.83  by (dtac (bex_Infinitesimal_iff2 RS iffD2) 1 THEN Step_tac 1);
    1.84  by (forw_inst_tac [("b1","hypreal_of_real(D) + y")] 
    1.85      ((hypreal_mult_right_cancel RS iffD2)) 1);
    1.86 -by (thin_tac "((*f* f) (hypreal_of_real(x) + h) + \
    1.87 +by (thin_tac "(( *f* f) (hypreal_of_real(x) + h) + \
    1.88  \   - hypreal_of_real (f x)) / h = hypreal_of_real(D) + y" 2);
    1.89  by (assume_tac 1);
    1.90  by (asm_full_simp_tac (simpset() addsimps [hypreal_times_divide1_eq RS sym]
    1.91 @@ -1169,7 +1169,7 @@
    1.92  (* lemmas *)
    1.93  Goalw [nsderiv_def] 
    1.94        "[| NSDERIV g x :> D; \
    1.95 -\              (*f* g) (hypreal_of_real(x) + xa) = hypreal_of_real(g x);\
    1.96 +\              ( *f* g) (hypreal_of_real(x) + xa) = hypreal_of_real(g x);\
    1.97  \              xa \\<in> Infinitesimal;\
    1.98  \              xa \\<noteq> 0 \
    1.99  \           |] ==> D = 0";
   1.100 @@ -1180,7 +1180,7 @@
   1.101  (* can be proved differently using NSLIM_isCont_iff *)
   1.102  Goalw [nsderiv_def] 
   1.103       "[| NSDERIV f x :> D;  h \\<in> Infinitesimal;  h \\<noteq> 0 |]  \
   1.104 -\     ==> (*f* f) (hypreal_of_real(x) + h) + -hypreal_of_real(f x) \\<approx> 0";    
   1.105 +\     ==> ( *f* f) (hypreal_of_real(x) + h) + -hypreal_of_real(f x) \\<approx> 0";    
   1.106  by (asm_full_simp_tac (simpset() addsimps 
   1.107      [mem_infmal_iff RS sym]) 1);
   1.108  by (rtac Infinitesimal_ratio 1);
   1.109 @@ -1196,11 +1196,11 @@
   1.110                    x - a
   1.111   ---------------------------------------------------------------*)
   1.112  Goal "[| NSDERIV f (g x) :> Da; \
   1.113 -\        (*f* g) (hypreal_of_real(x) + xa) \\<noteq> hypreal_of_real (g x); \
   1.114 -\        (*f* g) (hypreal_of_real(x) + xa) \\<approx> hypreal_of_real (g x) \
   1.115 -\     |] ==> ((*f* f) ((*f* g) (hypreal_of_real(x) + xa)) \
   1.116 +\        ( *f* g) (hypreal_of_real(x) + xa) \\<noteq> hypreal_of_real (g x); \
   1.117 +\        ( *f* g) (hypreal_of_real(x) + xa) \\<approx> hypreal_of_real (g x) \
   1.118 +\     |] ==> (( *f* f) (( *f* g) (hypreal_of_real(x) + xa)) \
   1.119  \                  + - hypreal_of_real (f (g x))) \
   1.120 -\             / ((*f* g) (hypreal_of_real(x) + xa) + - hypreal_of_real (g x)) \
   1.121 +\             / (( *f* g) (hypreal_of_real(x) + xa) + - hypreal_of_real (g x)) \
   1.122  \            \\<approx> hypreal_of_real(Da)";
   1.123  by (auto_tac (claset(),
   1.124         simpset() addsimps [NSDERIV_NSLIM_iff2, NSLIM_def]));
   1.125 @@ -1214,7 +1214,7 @@
   1.126                         h
   1.127   --------------------------------------------------------------*)
   1.128  Goal "[| NSDERIV g x :> Db; xa \\<in> Infinitesimal; xa \\<noteq> 0 |] \
   1.129 -\     ==> ((*f* g) (hypreal_of_real(x) + xa) + - hypreal_of_real(g x)) / xa \
   1.130 +\     ==> (( *f* g) (hypreal_of_real(x) + xa) + - hypreal_of_real(g x)) / xa \
   1.131  \         \\<approx> hypreal_of_real(Db)";
   1.132  by (auto_tac (claset(),
   1.133      simpset() addsimps [NSDERIV_NSLIM_iff, NSLIM_def, 
   1.134 @@ -1235,10 +1235,10 @@
   1.135  by (forw_inst_tac [("f","g")] NSDERIV_approx 1);
   1.136  by (auto_tac (claset(),
   1.137                simpset() addsimps [starfun_lambda_cancel2, starfun_o RS sym]));
   1.138 -by (case_tac "(*f* g) (hypreal_of_real(x) + xa) = hypreal_of_real (g x)" 1);
   1.139 +by (case_tac "( *f* g) (hypreal_of_real(x) + xa) = hypreal_of_real (g x)" 1);
   1.140  by (dres_inst_tac [("g","g")] NSDERIV_zero 1);
   1.141  by (auto_tac (claset(), simpset() addsimps [hypreal_divide_def]));
   1.142 -by (res_inst_tac [("z1","(*f* g) (hypreal_of_real(x) + xa) + -hypreal_of_real (g x)"),
   1.143 +by (res_inst_tac [("z1","( *f* g) (hypreal_of_real(x) + xa) + -hypreal_of_real (g x)"),
   1.144      ("y1","inverse xa")] (lemma_chain RS ssubst) 1);
   1.145  by (etac (hypreal_not_eq_minus_iff RS iffD1) 1);
   1.146  by (rtac approx_mult_hypreal_of_real 1);