conversion rules for at, at_left and at_right; applied to l'Hopital's rules.

--- a/src/HOL/Deriv.thy	Mon Dec 03 18:19:09 2012 +0100
+++ b/src/HOL/Deriv.thy	Mon Dec 03 18:19:11 2012 +0100
@@ -1618,23 +1618,14 @@
     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 DERIV_shift:
+  "(DERIV f (x + z) :> y) \<longleftrightarrow> (DERIV (\<lambda>x. f (x + z)) x :> y)"
+  by (simp add: DERIV_iff field_simps)
 
-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 DERIV_mirror:
+  "(DERIV f (- x) :> y) \<longleftrightarrow> (DERIV (\<lambda>x. f (- x::real) :: real) x :> - y)"
+  by (simp add: deriv_def filterlim_at_split filterlim_at_left_to_right
+                tendsto_minus_cancel_left field_simps conj_commute)
 
 lemma lhopital_right_0:
   fixes f0 g0 :: "real \<Rightarrow> real"
@@ -1733,6 +1724,39 @@
   finally show ?thesis .
 qed
 
+lemma lhopital_right:
+  "((f::real \<Rightarrow> real) ---> 0) (at_right x) \<Longrightarrow> (g ---> 0) (at_right x) \<Longrightarrow>
+    eventually (\<lambda>x. g x \<noteq> 0) (at_right x) \<Longrightarrow>
+    eventually (\<lambda>x. g' x \<noteq> 0) (at_right x) \<Longrightarrow>
+    eventually (\<lambda>x. DERIV f x :> f' x) (at_right x) \<Longrightarrow>
+    eventually (\<lambda>x. DERIV g x :> g' x) (at_right x) \<Longrightarrow>
+    ((\<lambda> x. (f' x / g' x)) ---> y) (at_right x) \<Longrightarrow>
+  ((\<lambda> x. f x / g x) ---> y) (at_right x)"
+  unfolding eventually_at_right_to_0[of _ x] filterlim_at_right_to_0[of _ _ x] DERIV_shift
+  by (rule lhopital_right_0)
+
+lemma lhopital_left:
+  "((f::real \<Rightarrow> real) ---> 0) (at_left x) \<Longrightarrow> (g ---> 0) (at_left x) \<Longrightarrow>
+    eventually (\<lambda>x. g x \<noteq> 0) (at_left x) \<Longrightarrow>
+    eventually (\<lambda>x. g' x \<noteq> 0) (at_left x) \<Longrightarrow>
+    eventually (\<lambda>x. DERIV f x :> f' x) (at_left x) \<Longrightarrow>
+    eventually (\<lambda>x. DERIV g x :> g' x) (at_left x) \<Longrightarrow>
+    ((\<lambda> x. (f' x / g' x)) ---> y) (at_left x) \<Longrightarrow>
+  ((\<lambda> x. f x / g x) ---> y) (at_left x)"
+  unfolding eventually_at_left_to_right filterlim_at_left_to_right DERIV_mirror
+  by (rule lhopital_right[where f'="\<lambda>x. - f' (- x)"]) (auto simp: DERIV_mirror)
+
+lemma lhopital:
+  "((f::real \<Rightarrow> real) ---> 0) (at x) \<Longrightarrow> (g ---> 0) (at x) \<Longrightarrow>
+    eventually (\<lambda>x. g x \<noteq> 0) (at x) \<Longrightarrow>
+    eventually (\<lambda>x. g' x \<noteq> 0) (at x) \<Longrightarrow>
+    eventually (\<lambda>x. DERIV f x :> f' x) (at x) \<Longrightarrow>
+    eventually (\<lambda>x. DERIV g x :> g' x) (at x) \<Longrightarrow>
+    ((\<lambda> x. (f' x / g' x)) ---> y) (at x) \<Longrightarrow>
+  ((\<lambda> x. f x / g x) ---> y) (at x)"
+  unfolding eventually_at_split filterlim_at_split
+  by (auto intro!: lhopital_right[of f x g g' f'] lhopital_left[of f x g g' f'])
+
 lemma lhopital_right_0_at_top:
   fixes f g :: "real \<Rightarrow> real"
   assumes g_0: "LIM x at_right 0. g x :> at_top"
@@ -1811,4 +1835,34 @@
   qed
 qed
 
+lemma lhopital_right_at_top:
+  "LIM x at_right x. (g::real \<Rightarrow> real) x :> at_top \<Longrightarrow>
+    eventually (\<lambda>x. g' x \<noteq> 0) (at_right x) \<Longrightarrow>
+    eventually (\<lambda>x. DERIV f x :> f' x) (at_right x) \<Longrightarrow>
+    eventually (\<lambda>x. DERIV g x :> g' x) (at_right x) \<Longrightarrow>
+    ((\<lambda> x. (f' x / g' x)) ---> y) (at_right x) \<Longrightarrow>
+    ((\<lambda> x. f x / g x) ---> y) (at_right x)"
+  unfolding eventually_at_right_to_0[of _ x] filterlim_at_right_to_0[of _ _ x] DERIV_shift
+  by (rule lhopital_right_0_at_top)
+
+lemma lhopital_left_at_top:
+  "LIM x at_left x. (g::real \<Rightarrow> real) x :> at_top \<Longrightarrow>
+    eventually (\<lambda>x. g' x \<noteq> 0) (at_left x) \<Longrightarrow>
+    eventually (\<lambda>x. DERIV f x :> f' x) (at_left x) \<Longrightarrow>
+    eventually (\<lambda>x. DERIV g x :> g' x) (at_left x) \<Longrightarrow>
+    ((\<lambda> x. (f' x / g' x)) ---> y) (at_left x) \<Longrightarrow>
+    ((\<lambda> x. f x / g x) ---> y) (at_left x)"
+  unfolding eventually_at_left_to_right filterlim_at_left_to_right DERIV_mirror
+  by (rule lhopital_right_at_top[where f'="\<lambda>x. - f' (- x)"]) (auto simp: DERIV_mirror)
+
+lemma lhopital_at_top:
+  "LIM x at x. (g::real \<Rightarrow> real) x :> at_top \<Longrightarrow>
+    eventually (\<lambda>x. g' x \<noteq> 0) (at x) \<Longrightarrow>
+    eventually (\<lambda>x. DERIV f x :> f' x) (at x) \<Longrightarrow>
+    eventually (\<lambda>x. DERIV g x :> g' x) (at x) \<Longrightarrow>
+    ((\<lambda> x. (f' x / g' x)) ---> y) (at x) \<Longrightarrow>
+    ((\<lambda> x. f x / g x) ---> y) (at x)"
+  unfolding eventually_at_split filterlim_at_split
+  by (auto intro!: lhopital_right_at_top[of g x g' f f'] lhopital_left_at_top[of g x g' f f'])
+
 end

--- a/src/HOL/Limits.thy	Mon Dec 03 18:19:09 2012 +0100
+++ b/src/HOL/Limits.thy	Mon Dec 03 18:19:11 2012 +0100
@@ -280,6 +280,9 @@
 lemma filtermap_bot [simp]: "filtermap f bot = bot"
   by (simp add: filter_eq_iff eventually_filtermap)
 
+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)
+
 subsection {* Order filters *}
 
 definition at_top :: "('a::order) filter"
@@ -703,6 +706,13 @@
     by (auto simp: le_filter_def eventually_filtermap eventually_within elim!: allE[of _ "\<lambda>x. x \<in> S"])
 qed (auto intro: within_le order_trans simp: le_within_iff eventually_filtermap)
 
+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
+
 abbreviation (in topological_space)
   tendsto :: "('b \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'b filter \<Rightarrow> bool" (infixr "--->" 55) where
   "(f ---> l) F \<equiv> filterlim f (nhds l) F"
@@ -915,6 +925,11 @@
   shows "((\<lambda>x. - f x) ---> - a) F \<Longrightarrow> (f ---> a) F"
   by (drule tendsto_minus, simp)
 
+lemma tendsto_minus_cancel_left:
+    "(f ---> - (y::_::real_normed_vector)) F \<longleftrightarrow> ((\<lambda>x. - f x) ---> y) F"
+  using tendsto_minus_cancel[of f "- y" F]  tendsto_minus[of f "- y" F]
+  by auto
+
 lemma tendsto_diff [tendsto_intros]:
   fixes a b :: "'a::real_normed_vector"
   shows "\<lbrakk>(f ---> a) F; (g ---> b) F\<rbrakk> \<Longrightarrow> ((\<lambda>x. f x - g x) ---> a - b) F"
@@ -1367,5 +1382,79 @@
     by eventually_elim simp
 qed
 
+subsection {* Relate @{const at}, @{const at_left} and @{const at_right} *}
+
+text {*
+
+This lemmas are useful for conversion between @{term "at x"} to @{term "at_left x"} and
+@{term "at_right x"} and also @{term "at_right 0"}.
+
+*}
+
+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 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 filtermap_nhds_shift: "filtermap (\<lambda>x. x - d) (nhds a) = nhds (a - d::real)"
+  unfolding filter_eq_iff eventually_filtermap eventually_nhds_metric
+  by (intro allI ex_cong) (auto simp: dist_real_def field_simps)
+
+lemma filtermap_nhds_minus: "filtermap (\<lambda>x. - x) (nhds a) = nhds (- a::real)"
+  unfolding filter_eq_iff eventually_filtermap eventually_nhds_metric
+  apply (intro allI ex_cong)
+  apply (auto simp: dist_real_def field_simps)
+  apply (erule_tac x="-x" in allE)
+  apply simp
+  done
+
+lemma filtermap_at_shift: "filtermap (\<lambda>x. x - d) (at a) = at (a - d::real)"
+  unfolding at_def filtermap_nhds_shift[symmetric]
+  by (simp add: filter_eq_iff eventually_filtermap eventually_within)
+
+lemma filtermap_at_right_shift: "filtermap (\<lambda>x. x - d) (at_right a) = at_right (a - d::real)"
+  unfolding filtermap_at_shift[symmetric]
+  by (simp add: filter_eq_iff eventually_filtermap eventually_within)
+
+lemma at_right_to_0: "at_right (a::real) = filtermap (\<lambda>x. x + a) (at_right 0)"
+  using filtermap_at_right_shift[of "-a" 0] by simp
+
+lemma filterlim_at_right_to_0:
+  "filterlim f F (at_right (a::real)) \<longleftrightarrow> filterlim (\<lambda>x. f (x + a)) F (at_right 0)"
+  unfolding filterlim_def filtermap_filtermap at_right_to_0[of a] ..
+
+lemma eventually_at_right_to_0:
+  "eventually P (at_right (a::real)) \<longleftrightarrow> eventually (\<lambda>x. P (x + a)) (at_right 0)"
+  unfolding at_right_to_0[of a] by (simp add: eventually_filtermap)
+
+lemma filtermap_at_minus: "filtermap (\<lambda>x. - x) (at a) = at (- a::real)"
+  unfolding at_def filtermap_nhds_minus[symmetric]
+  by (simp add: filter_eq_iff eventually_filtermap eventually_within)
+
+lemma at_left_minus: "at_left (a::real) = filtermap (\<lambda>x. - x) (at_right (- a))"
+  by (simp add: filter_eq_iff eventually_filtermap eventually_within filtermap_at_minus[symmetric])
+
+lemma at_right_minus: "at_right (a::real) = filtermap (\<lambda>x. - x) (at_left (- a))"
+  by (simp add: filter_eq_iff eventually_filtermap eventually_within filtermap_at_minus[symmetric])
+
+lemma filterlim_at_left_to_right:
+  "filterlim f F (at_left (a::real)) \<longleftrightarrow> filterlim (\<lambda>x. f (- x)) F (at_right (-a))"
+  unfolding filterlim_def filtermap_filtermap at_left_minus[of a] ..
+
+lemma eventually_at_left_to_right:
+  "eventually P (at_left (a::real)) \<longleftrightarrow> eventually (\<lambda>x. P (- x)) (at_right (-a))"
+  unfolding at_left_minus[of a] by (simp add: eventually_filtermap)
+
+lemma filterlim_at_split:
+  "filterlim f F (at (x::real)) \<longleftrightarrow> filterlim f F (at_left x) \<and> filterlim f F (at_right x)"
+  by (subst at_eq_sup_left_right) (simp add: filterlim_def filtermap_sup)
+
+lemma eventually_at_split:
+  "eventually P (at (x::real)) \<longleftrightarrow> eventually P (at_left x) \<and> eventually P (at_right x)"
+  by (subst at_eq_sup_left_right) (simp add: eventually_sup)
+
 end