# HG changeset patch
# User hoelzl
# Date 1354555149 -3600
# Node ID 9bd6b6b8a5544326a22c6d2c64adb90b0a9afe90
# Parent  25b1e8686ce076102d51bee674eec9556fd29186
weakened assumptions for lhopital_right_0

diff -r 25b1e8686ce0 -r 9bd6b6b8a554 src/HOL/Deriv.thy
--- a/src/HOL/Deriv.thy	Mon Dec 03 18:19:08 2012 +0100
+++ b/src/HOL/Deriv.thy	Mon Dec 03 18:19:09 2012 +0100
@@ -1607,26 +1607,90 @@
     by auto
 qed
 
+lemma DERIV_cong_ev: "x = y \<Longrightarrow> eventually (\<lambda>x. f x = g x) (nhds x) \<Longrightarrow> u = v \<Longrightarrow>
+    DERIV f x :> u \<longleftrightarrow> DERIV g y :> v"
+  unfolding DERIV_iff2
+proof (rule filterlim_cong)
+  assume "eventually (\<lambda>x. f x = g x) (nhds x)"
+  moreover then have "f x = g x" by (auto simp: eventually_nhds)
+  moreover assume "x = y" "u = v"
+  ultimately show "eventually (\<lambda>xa. (f xa - f x) / (xa - x) = (g xa - g y) / (xa - y)) (at x)"
+    by (auto simp: eventually_within at_def elim: eventually_elim1)
+qed simp_all
+
+lemma at_eq_sup_left_right: "at (x::real) = sup (at_left x) (at_right x)"
+  by (auto simp: eventually_within at_def filter_eq_iff eventually_sup 
+           elim: eventually_elim2 eventually_elim1)
+
+lemma filtermap_sup: "filtermap f (sup F1 F2) = sup (filtermap f F1) (filtermap f F2)"
+  by (auto simp: filter_eq_iff eventually_filtermap eventually_sup)
+
+lemma filterlim_filtermap: "filterlim f F1 (filtermap g F2) = filterlim (\<lambda>x. f (g x)) F1 F2"
+  unfolding filterlim_def filtermap_filtermap ..
+
+lemma filterlim_sup:
+  "filterlim f F F1 \<Longrightarrow> filterlim f F F2 \<Longrightarrow> filterlim f F (sup F1 F2)"
+  unfolding filterlim_def filtermap_sup by auto
+
+lemma filterlim_split_at_real:
+  "filterlim f F (at_left x) \<Longrightarrow> filterlim f F (at_right x) \<Longrightarrow> filterlim f F (at (x::real))"
+  by (subst at_eq_sup_left_right) (rule filterlim_sup)
+
 lemma lhopital_right_0:
-  fixes f g :: "real \<Rightarrow> real"
-  assumes f_0: "isCont f 0" "f 0 = 0"
-  assumes g_0: "isCont g 0" "g 0 = 0"
+  fixes f0 g0 :: "real \<Rightarrow> real"
+  assumes f_0: "(f0 ---> 0) (at_right 0)"
+  assumes g_0: "(g0 ---> 0) (at_right 0)"
   assumes ev:
-    "eventually (\<lambda>x. g x \<noteq> 0) (at_right 0)"
+    "eventually (\<lambda>x. g0 x \<noteq> 0) (at_right 0)"
     "eventually (\<lambda>x. g' x \<noteq> 0) (at_right 0)"
-    "eventually (\<lambda>x. DERIV f x :> f' x) (at_right 0)"
-    "eventually (\<lambda>x. DERIV g x :> g' x) (at_right 0)"
+    "eventually (\<lambda>x. DERIV f0 x :> f' x) (at_right 0)"
+    "eventually (\<lambda>x. DERIV g0 x :> g' x) (at_right 0)"
   assumes lim: "((\<lambda> x. (f' x / g' x)) ---> x) (at_right 0)"
-  shows "((\<lambda> x. f x / g x) ---> x) (at_right 0)"
+  shows "((\<lambda> x. f0 x / g0 x) ---> x) (at_right 0)"
 proof -
-  from eventually_conj[OF eventually_conj[OF ev(1) ev(2)] eventually_conj[OF ev(3) ev(4)]]
-  obtain a where [arith]: "0 < a"
-    and g_neq_0: "\<And>x. 0 < x \<Longrightarrow> x < a \<Longrightarrow> g x \<noteq> 0"
+  def f \<equiv> "\<lambda>x. if x \<le> 0 then 0 else f0 x"
+  then have "f 0 = 0" by simp
+
+  def g \<equiv> "\<lambda>x. if x \<le> 0 then 0 else g0 x"
+  then have "g 0 = 0" by simp
+
+  have "eventually (\<lambda>x. g0 x \<noteq> 0 \<and> g' x \<noteq> 0 \<and>
+      DERIV f0 x :> (f' x) \<and> DERIV g0 x :> (g' x)) (at_right 0)"
+    using ev by eventually_elim auto
+  then obtain a where [arith]: "0 < a"
+    and g0_neq_0: "\<And>x. 0 < x \<Longrightarrow> x < a \<Longrightarrow> g0 x \<noteq> 0"
     and g'_neq_0: "\<And>x. 0 < x \<Longrightarrow> x < a \<Longrightarrow> g' x \<noteq> 0"
-    and f: "\<And>x. 0 < x \<Longrightarrow> x < a \<Longrightarrow> DERIV f x :> (f' x)"
-    and g: "\<And>x. 0 < x \<Longrightarrow> x < a \<Longrightarrow> DERIV g x :> (g' x)"
+    and f0: "\<And>x. 0 < x \<Longrightarrow> x < a \<Longrightarrow> DERIV f0 x :> (f' x)"
+    and g0: "\<And>x. 0 < x \<Longrightarrow> x < a \<Longrightarrow> DERIV g0 x :> (g' x)"
     unfolding eventually_within eventually_at by (auto simp: dist_real_def)
 
+  have g_neq_0: "\<And>x. 0 < x \<Longrightarrow> x < a \<Longrightarrow> g x \<noteq> 0"
+    using g0_neq_0 by (simp add: g_def)
+
+  { fix x assume x: "0 < x" "x < a" then have "DERIV f x :> (f' x)"
+      by (intro DERIV_cong_ev[THEN iffD1, OF _ _ _ f0[OF x]])
+         (auto simp: f_def eventually_nhds_metric dist_real_def intro!: exI[of _ x]) }
+  note f = this
+
+  { fix x assume x: "0 < x" "x < a" then have "DERIV g x :> (g' x)"
+      by (intro DERIV_cong_ev[THEN iffD1, OF _ _ _ g0[OF x]])
+         (auto simp: g_def eventually_nhds_metric dist_real_def intro!: exI[of _ x]) }
+  note g = this
+
+  have "isCont f 0"
+    using tendsto_const[of "0::real" "at 0"] f_0
+    unfolding isCont_def f_def
+    by (intro filterlim_split_at_real)
+       (auto elim: eventually_elim1
+             simp add: filterlim_def le_filter_def eventually_within eventually_filtermap)
+    
+  have "isCont g 0"
+    using tendsto_const[of "0::real" "at 0"] g_0
+    unfolding isCont_def g_def
+    by (intro filterlim_split_at_real)
+       (auto elim: eventually_elim1
+             simp add: filterlim_def le_filter_def eventually_within eventually_filtermap)
+
   have "\<exists>\<zeta>. \<forall>x\<in>{0 <..< a}. 0 < \<zeta> x \<and> \<zeta> x < x \<and> f x / g x = f' (\<zeta> x) / g' (\<zeta> x)"
   proof (rule bchoice, rule)
     fix x assume "x \<in> {0 <..< a}"
@@ -1661,9 +1725,12 @@
     by (auto elim!: eventually_elim1 simp: filterlim_within filterlim_at)
   from this lim have "((\<lambda>t. f' (\<zeta> t) / g' (\<zeta> t)) ---> x) (at_right 0)"
     by (rule_tac filterlim_compose[of _ _ _ \<zeta>])
-  ultimately show "((\<lambda>t. f t / g t) ---> x) (at_right 0)"
+  ultimately have "((\<lambda>t. f t / g t) ---> x) (at_right 0)" (is ?P)
     by (rule_tac filterlim_cong[THEN iffD1, OF refl refl])
        (auto elim: eventually_elim1)
+  also have "?P \<longleftrightarrow> ?thesis"
+    by (rule filterlim_cong) (auto simp: f_def g_def eventually_within)
+  finally show ?thesis .
 qed
 
 lemma lhopital_right_0_at_top: