src/HOL/Hyperreal/Lim.thy

 *)
 
 header{*Limits, Continuity and Differentiation*}
 
 theory Lim
-imports SEQ RealDef
+imports SEQ
 begin
 
 text{*Standard and Nonstandard Definitions*}
 
 constdefs
   LIM :: "[real=>real,real,real] => bool"
 				("((_)/ -- (_)/ --> (_))" [60, 0, 60] 60)
   "f -- a --> L ==
-     \<forall>r. 0 < r -->
-	     (\<exists>s. 0 < s & (\<forall>x. (x \<noteq> a & (\<bar>x + -a\<bar> < s)
-			  --> \<bar>f x + -L\<bar> < r)))"
+     \<forall>r > 0. \<exists>s > 0. \<forall>x. x \<noteq> a & \<bar>x + -a\<bar> < s
+			  --> \<bar>f x + -L\<bar> < r"
 
   NSLIM :: "[real=>real,real,real] => bool"
 			      ("((_)/ -- (_)/ --NS> (_))" [60, 0, 60] 60)
   "f -- a --NS> L == (\<forall>x. (x \<noteq> hypreal_of_real a &
 		      x @= hypreal_of_real a -->

   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))"
 
   isUCont :: "(real=>real) => bool"
-  "isUCont f ==  (\<forall>r. 0 < r -->
-		      (\<exists>s. 0 < s & (\<forall>x y. \<bar>x + -y\<bar> < s
-			    --> \<bar>f x + -f y\<bar> < r)))"
+  "isUCont f ==  \<forall>r > 0. \<exists>s > 0. \<forall>x y. \<bar>x + -y\<bar> < s --> \<bar>f x + -f y\<bar> < r"
 
   isNSUCont :: "(real=>real) => bool"
   "isNSUCont f == (\<forall>x y. x @= y --> ( *f* f) x @= ( *f* f) y)"
 
 

 
 section{*Some Purely Standard Proofs*}
 
 lemma LIM_eq:
      "f -- a --> L =
-     (\<forall>r. 0<r --> (\<exists>s. 0 < s & (\<forall>x. x \<noteq> a & \<bar>x-a\<bar> < s --> \<bar>f x - L\<bar> < r)))"
+     (\<forall>r>0.\<exists>s>0.\<forall>x. x \<noteq> a & \<bar>x-a\<bar> < s --> \<bar>f x - L\<bar> < r)"
 by (simp add: LIM_def diff_minus)
 
 lemma LIM_D:
      "[| f -- a --> L; 0<r |]
-      ==> \<exists>s. 0 < s & (\<forall>x. x \<noteq> a & \<bar>x-a\<bar> < s --> \<bar>f x - L\<bar> < r)"
+      ==> \<exists>s>0.\<forall>x. x \<noteq> a & \<bar>x-a\<bar> < s --> \<bar>f x - L\<bar> < r"
 by (simp add: LIM_eq)
 
 lemma LIM_const [simp]: "(%x. k) -- x --> k"
 by (simp add: LIM_def)
 

   from LIM_D [OF g half_gt_zero [OF r]]
   obtain gs
     where gs:    "0 < gs"
       and gs_lt: "\<forall>x. x \<noteq> a & \<bar>x-a\<bar> < gs --> \<bar>g x - M\<bar> < r/2"
   by blast
-  show "\<exists>s. 0 < s \<and>
-            (\<forall>x. x \<noteq> a \<and> \<bar>x-a\<bar> < s \<longrightarrow> \<bar>f x + g x - (L + M)\<bar> < r)"
+  show "\<exists>s>0.\<forall>x. x \<noteq> a \<and> \<bar>x-a\<bar> < s \<longrightarrow> \<bar>f x + g x - (L + M)\<bar> < r"
   proof (intro exI conjI strip)
     show "0 < min fs gs"  by (simp add: fs gs)
     fix x :: real
     assume "x \<noteq> a \<and> \<bar>x-a\<bar> < min fs gs"
     with fs_lt gs_lt

 
 
 lemma LIM_const_not_eq: "k \<noteq> L ==> ~ ((%x. k) -- a --> L)"
 proof (simp add: linorder_neq_iff LIM_eq, elim disjE)
   assume k: "k < L"
-  show "\<exists>r. 0 < r \<and>
-        (\<forall>s. 0 < s \<longrightarrow> (\<exists>x. (x < a \<or> a < x) \<and> \<bar>x-a\<bar> < s) \<and> \<not> \<bar>k-L\<bar> < r)"
+  show "\<exists>r>0. \<forall>s>0. (\<exists>x. (x < a \<or> a < x) \<and> \<bar>x-a\<bar> < s) \<and> \<not> \<bar>k-L\<bar> < r"
   proof (intro exI conjI strip)
     show "0 < L-k" by (simp add: k compare_rls)
     fix s :: real
     assume s: "0<s"
     { from s show "s/2 + a < a \<or> a < s/2 + a" by arith

      next
       from s show "~ \<bar>k-L\<bar> < L-k" by (simp add: abs_if) }
   qed
 next
   assume k: "L < k"
-  show "\<exists>r. 0 < r \<and>
-        (\<forall>s. 0 < s \<longrightarrow> (\<exists>x. (x < a \<or> a < x) \<and> \<bar>x-a\<bar> < s) \<and> \<not> \<bar>k-L\<bar> < r)"
+  show "\<exists>r>0.\<forall>s>0. (\<exists>x. (x < a \<or> a < x) \<and> \<bar>x-a\<bar> < s) \<and> \<not> \<bar>k-L\<bar> < r"
   proof (intro exI conjI strip)
     show "0 < k-L" by (simp add: k compare_rls)
     fix s :: real
     assume s: "0<s"
     { from s show "s/2 + a < a \<or> a < s/2 + a" by arith

 done
 
 
 subsubsection{*Limit: The NS definition implies the standard definition.*}
 
-lemma lemma_LIM: "\<forall>s. 0 < s --> (\<exists>xa.  xa \<noteq> x &
-         \<bar>xa + - x\<bar> < s  & r \<le> \<bar>f xa + -L\<bar>)
+lemma lemma_LIM: "\<forall>s>0.\<exists>xa.  xa \<noteq> x &
+         \<bar>xa + - x\<bar> < s  & r \<le> \<bar>f xa + -L\<bar>
       ==> \<forall>n::nat. \<exists>xa.  xa \<noteq> x &
               \<bar>xa + -x\<bar> < inverse(real(Suc n)) & r \<le> \<bar>f xa + -L\<bar>"
 apply clarify
 apply (cut_tac n1 = n in real_of_nat_Suc_gt_zero [THEN positive_imp_inverse_positive], auto)
 done
 
 lemma lemma_skolemize_LIM2:
-     "\<forall>s. 0 < s --> (\<exists>xa.  xa \<noteq> x &
-         \<bar>xa + - x\<bar> < s  & r \<le> \<bar>f xa + -L\<bar>)
+     "\<forall>s>0.\<exists>xa.  xa \<noteq> x & \<bar>xa + - x\<bar> < s  & r \<le> \<bar>f xa + -L\<bar>
       ==> \<exists>X. \<forall>n::nat. X n \<noteq> x &
                 \<bar>X n + -x\<bar> < inverse(real(Suc n)) & r \<le> abs(f (X n) + -L)"
 apply (drule lemma_LIM)
 apply (drule choice, blast)
 done

 prefer 2 apply blast
 apply (erule_tac V = "\<forall>x y. \<bar>x + - y\<bar> < s --> \<bar>f x + - f y\<bar> < u" in thin_rl)
 apply (drule FreeUltrafilterNat_all, ultra)
 done
 
-lemma lemma_LIMu: "\<forall>s. 0 < s --> (\<exists>z y. \<bar>z + - y\<bar> < s & r \<le> \<bar>f z + -f y\<bar>)
-      ==> \<forall>n::nat. \<exists>z y.
-               \<bar>z + -y\<bar> < inverse(real(Suc n)) &
-               r \<le> \<bar>f z + -f y\<bar>"
+lemma lemma_LIMu: "\<forall>s>0.\<exists>z y. \<bar>z + - y\<bar> < s & r \<le> \<bar>f z + -f y\<bar>
+      ==> \<forall>n::nat. \<exists>z y. \<bar>z + -y\<bar> < inverse(real(Suc n)) & r \<le> \<bar>f z + -f y\<bar>"
 apply clarify
 apply (cut_tac n1 = n 
        in real_of_nat_Suc_gt_zero [THEN positive_imp_inverse_positive], auto)
 done
 
 lemma lemma_skolemize_LIM2u:
-     "\<forall>s. 0 < s --> (\<exists>z y. \<bar>z + - y\<bar> < s  & r \<le> \<bar>f z + -f y\<bar>)
+     "\<forall>s>0.\<exists>z y. \<bar>z + - y\<bar> < s  & r \<le> \<bar>f z + -f y\<bar>
       ==> \<exists>X Y. \<forall>n::nat.
                abs(X n + -(Y n)) < inverse(real(Suc n)) &
                r \<le> abs(f (X n) + -f (Y n))"
 apply (drule lemma_LIMu)
 apply (drule choice, safe)

 by (force simp add: NSdifferentiable_def)
 
 subsubsection{*Alternative definition for differentiability*}
 
 lemma LIM_I:
-     "(!!r. 0<r ==> (\<exists>s. 0 < s & (\<forall>x. x \<noteq> a & \<bar>x-a\<bar> < s --> \<bar>f x - L\<bar> < r)))
+     "(!!r. 0<r ==> \<exists>s>0.\<forall>x. x \<noteq> a & \<bar>x-a\<bar> < s --> \<bar>f x - L\<bar> < r)
       ==> f -- a --> L"
 by (simp add: LIM_eq)
 
 lemma DERIV_LIM_iff:
      "((%h. (f(a + h) - f(a)) / h) -- 0 --> D) =

  prefer 2
  apply simp
  apply (drule_tac P = "%d. 0<d --> ?P d" and x = 1 in spec, arith)
 apply (drule_tac x = x in spec)+
 apply simp
-apply (drule_tac P = "%r. ?P r --> (\<exists>s. 0<s & ?Q r s) " and x = "\<bar>y - f x\<bar>" in spec)
+apply (drule_tac P = "%r. ?P r --> (\<exists>s>0. ?Q r s) " and x = "\<bar>y - f x\<bar>" in spec)
 apply safe
 apply simp
 apply (drule_tac x = s in spec, clarify)
 apply (cut_tac x = "f x" and y = y in linorder_less_linear, safe)
 apply (drule_tac x = "ba-x" in spec)

 subsection{*If @{term "0 < f'(x)"} then @{term x} is Locally Strictly Increasing At The Right*}
 
 lemma DERIV_left_inc:
   assumes der: "DERIV f x :> l"
       and l:   "0 < l"
-  shows "\<exists>d. 0 < d & (\<forall>h. 0 < h & h < d --> f(x) < f(x + h))"
+  shows "\<exists>d > 0. \<forall>h > 0. h < d --> f(x) < f(x + h)"
 proof -
   from l der [THEN DERIV_D, THEN LIM_D [where r = "l"]]
-  have "\<exists>s. 0 < s \<and>
-              (\<forall>z. z \<noteq> 0 \<and> \<bar>z\<bar> < s \<longrightarrow> \<bar>(f(x+z) - f x) / z - l\<bar> < l)"
+  have "\<exists>s > 0. (\<forall>z. z \<noteq> 0 \<and> \<bar>z\<bar> < s \<longrightarrow> \<bar>(f(x+z) - f x) / z - l\<bar> < l)"
     by (simp add: diff_minus)
   then obtain s
         where s:   "0 < s"
           and all: "!!z. z \<noteq> 0 \<and> \<bar>z\<bar> < s \<longrightarrow> \<bar>(f(x+z) - f x) / z - l\<bar> < l"
     by auto
   thus ?thesis
   proof (intro exI conjI strip)
     show "0<s" .
     fix h::real
-    assume "0 < h \<and> h < s"
+    assume "0 < h" "h < s"
     with all [of h] show "f x < f (x+h)"
     proof (simp add: abs_if pos_less_divide_eq diff_minus [symmetric]
 		split add: split_if_asm)
       assume "~ (f (x+h) - f x) / h < l" and h: "0 < h"
       with l

 qed
 
 lemma DERIV_left_dec:
   assumes der: "DERIV f x :> l"
       and l:   "l < 0"
-  shows "\<exists>d. 0 < d & (\<forall>h. 0 < h & h < d --> f(x) < f(x-h))"
+  shows "\<exists>d > 0. \<forall>h > 0. h < d --> f(x) < f(x-h)"
 proof -
   from l der [THEN DERIV_D, THEN LIM_D [where r = "-l"]]
-  have "\<exists>s. 0 < s \<and>
-              (\<forall>z. z \<noteq> 0 \<and> \<bar>z\<bar> < s \<longrightarrow> \<bar>(f(x+z) - f x) / z - l\<bar> < -l)"
+  have "\<exists>s > 0. (\<forall>z. z \<noteq> 0 \<and> \<bar>z\<bar> < s \<longrightarrow> \<bar>(f(x+z) - f x) / z - l\<bar> < -l)"
     by (simp add: diff_minus)
   then obtain s
         where s:   "0 < s"
           and all: "!!z. z \<noteq> 0 \<and> \<bar>z\<bar> < s \<longrightarrow> \<bar>(f(x+z) - f x) / z - l\<bar> < -l"
     by auto
   thus ?thesis
   proof (intro exI conjI strip)
     show "0<s" .
     fix h::real
-    assume "0 < h \<and> h < s"
+    assume "0 < h" "h < s"
     with all [of "-h"] show "f x < f (x-h)"
     proof (simp add: abs_if pos_less_divide_eq diff_minus [symmetric]
 		split add: split_if_asm)
       assume " - ((f (x-h) - f x) / h) < l" and h: "0 < h"
       with l

   case equal show ?thesis .
 next
   case less
   from DERIV_left_dec [OF der less]
   obtain d' where d': "0 < d'"
-             and lt: "\<forall>h. 0 < h \<and> h < d' \<longrightarrow> f x < f (x-h)" by blast
+             and lt: "\<forall>h > 0. h < d' \<longrightarrow> f x < f (x-h)" by blast
   from real_lbound_gt_zero [OF d d']
   obtain e where "0 < e \<and> e < d \<and> e < d'" ..
   with lt le [THEN spec [where x="x-e"]]
   show ?thesis by (auto simp add: abs_if)
 next
   case greater
   from DERIV_left_inc [OF der greater]
   obtain d' where d': "0 < d'"
-             and lt: "\<forall>h. 0 < h \<and> h < d' \<longrightarrow> f x < f (x + h)" by blast
+             and lt: "\<forall>h > 0. h < d' \<longrightarrow> f x < f (x + h)" by blast
   from real_lbound_gt_zero [OF d d']
   obtain e where "0 < e \<and> e < d \<and> e < d'" ..
   with lt le [THEN spec [where x="x+e"]]
   show ?thesis by (auto simp add: abs_if)
 qed

 text{*A function is constant if its derivative is 0 over an interval.*}
 
 lemma DERIV_isconst_end: "[| a < b;
          \<forall>x. a \<le> x & x \<le> b --> isCont f x;
          \<forall>x. a < x & x < b --> DERIV f x :> 0 |]
-        ==> (f b = f a)"
+        ==> f b = f a"
 apply (drule MVT, assumption)
 apply (blast intro: differentiableI)
 apply (auto dest!: DERIV_unique simp add: diff_eq_eq)
 done
 

 
 lemma isCont_inj_range:
   assumes d: "0 < d"
       and inj: "\<forall>z. \<bar>z-x\<bar> \<le> d --> g(f z) = z"
       and cont: "\<forall>z. \<bar>z-x\<bar> \<le> d --> isCont f z"
-  shows "\<exists>e. 0<e & (\<forall>y. \<bar>y - f x\<bar> \<le> e --> (\<exists>z. \<bar>z-x\<bar> \<le> d & f z = y))"
+  shows "\<exists>e>0. \<forall>y. \<bar>y - f x\<bar> \<le> e --> (\<exists>z. \<bar>z-x\<bar> \<le> d & f z = y)"
 proof -
   have "x-d \<le> x+d" "\<forall>z. x-d \<le> z \<and> z \<le> x+d \<longrightarrow> isCont f z" using cont d
     by (auto simp add: abs_le_interval_iff)
   from isCont_Lb_Ub [OF this]
   obtain L M

       and inj: "\<forall>z. \<bar>z-x\<bar> \<le> d --> g(f z) = z"
       and cont: "\<forall>z. \<bar>z-x\<bar> \<le> d --> isCont f z"
   shows "isCont g (f x)"
 proof (simp add: isCont_iff LIM_eq)
   show "\<forall>r. 0 < r \<longrightarrow>
-         (\<exists>s. 0<s \<and> (\<forall>z. z\<noteq>0 \<and> \<bar>z\<bar> < s \<longrightarrow> \<bar>g(f x + z) - g(f x)\<bar> < r))"
+         (\<exists>s>0. \<forall>z. z\<noteq>0 \<and> \<bar>z\<bar> < s \<longrightarrow> \<bar>g(f x + z) - g(f x)\<bar> < r)"
   proof (intro strip)
     fix r::real
     assume r: "0<r"
     from real_lbound_gt_zero [OF r d]
     obtain e where e: "0 < e" and e_lt: "e < r \<and> e < d" by blast

                   "\<forall>z. \<bar>z-x\<bar> \<le> e --> isCont f z"   by auto
     from isCont_inj_range [OF e this]
     obtain e' where e': "0 < e'"
         and all: "\<forall>y. \<bar>y - f x\<bar> \<le> e' \<longrightarrow> (\<exists>z. \<bar>z - x\<bar> \<le> e \<and> f z = y)"
           by blast
-    show "\<exists>s. 0<s \<and> (\<forall>z. z\<noteq>0 \<and> \<bar>z\<bar> < s \<longrightarrow> \<bar>g(f x + z) - g(f x)\<bar> < r)"
+    show "\<exists>s>0. \<forall>z. z\<noteq>0 \<and> \<bar>z\<bar> < s \<longrightarrow> \<bar>g(f x + z) - g(f x)\<bar> < r"
     proof (intro exI conjI)
       show "0<e'" .
       show "\<forall>z. z \<noteq> 0 \<and> \<bar>z\<bar> < e' \<longrightarrow> \<bar>g (f x + z) - g (f x)\<bar> < r"
       proof (intro strip)
         fix z::real

 val isCont_inverse_function = thm "isCont_inverse_function";
 *}
 
 
 end
-