# HG changeset patch
# User hoelzl
# Date 1354555141 -3600
# Node ID 3764d4620fb3dd70ba0e99ae75e169d25f46625d
# Parent  b06b95a5fda214567474a619edd8b3481a1775ca
add filterlim rules for unary minus and inverse

diff -r b06b95a5fda2 -r 3764d4620fb3 src/HOL/Limits.thy
--- a/src/HOL/Limits.thy	Mon Dec 03 18:18:59 2012 +0100
+++ b/src/HOL/Limits.thy	Mon Dec 03 18:19:01 2012 +0100
@@ -390,6 +390,12 @@
 lemma within_le: "F within S \<le> F"
   unfolding le_filter_def eventually_within by (auto elim: eventually_elim1)
 
+lemma le_withinI: "F \<le> F' \<Longrightarrow> eventually (\<lambda>x. x \<in> S) F \<Longrightarrow> F \<le> F' within S"
+  unfolding le_filter_def eventually_within by (auto elim: eventually_elim2)
+
+lemma le_within_iff: "eventually (\<lambda>x. x \<in> S) F \<Longrightarrow> F \<le> F' within S \<longleftrightarrow> F \<le> F'"
+  by (blast intro: within_le le_withinI order_trans)
+
 lemma eventually_nhds:
   "eventually P (nhds a) \<longleftrightarrow> (\<exists>S. open S \<and> a \<in> S \<and> (\<forall>x\<in>S. P x))"
 unfolding nhds_def
@@ -629,6 +635,14 @@
 lemma filterlimI: "(\<And>P. eventually P F2 \<Longrightarrow> eventually (\<lambda>x. P (f x)) F1) \<Longrightarrow> (LIM x F1. f x :> F2)"
   by (auto simp: filterlim_def eventually_filtermap le_filter_def)
 
+lemma filterlim_compose: 
+  "filterlim g F3 F2 \<Longrightarrow> filterlim f F2 F1 \<Longrightarrow> filterlim (\<lambda>x. g (f x)) F3 F1"
+  unfolding filterlim_def filtermap_filtermap[symmetric] by (metis filtermap_mono order_trans)
+
+lemma filterlim_mono: 
+  "filterlim f F2 F1 \<Longrightarrow> F2 \<le> F2' \<Longrightarrow> F1' \<le> F1 \<Longrightarrow> filterlim f F2' F1'"
+  unfolding filterlim_def by (metis filtermap_mono order_trans)
+
 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"
@@ -734,36 +748,24 @@
   assumes "\<not> trivial_limit F" shows "((\<lambda>x. a) ---> b) F \<longleftrightarrow> a = b"
   by (safe intro!: tendsto_const tendsto_unique [OF assms tendsto_const])
 
+lemma tendsto_at_iff_tendsto_nhds:
+  "(g ---> g l) (at l) \<longleftrightarrow> (g ---> g l) (nhds l)"
+  unfolding tendsto_def at_def eventually_within
+  by (intro ext all_cong imp_cong) (auto elim!: eventually_elim1)
+
 lemma tendsto_compose:
-  assumes g: "(g ---> g l) (at l)"
-  assumes f: "(f ---> l) F"
-  shows "((\<lambda>x. g (f x)) ---> g l) F"
-proof (rule topological_tendstoI)
-  fix B assume B: "open B" "g l \<in> B"
-  obtain A where A: "open A" "l \<in> A"
-    and gB: "\<forall>y. y \<in> A \<longrightarrow> g y \<in> B"
-    using topological_tendstoD [OF g B] B(2)
-    unfolding eventually_at_topological by fast
-  hence "\<forall>x. f x \<in> A \<longrightarrow> g (f x) \<in> B" by simp
-  from this topological_tendstoD [OF f A]
-  show "eventually (\<lambda>x. g (f x) \<in> B) F"
-    by (rule eventually_mono)
-qed
+  "(g ---> g l) (at l) \<Longrightarrow> (f ---> l) F \<Longrightarrow> ((\<lambda>x. g (f x)) ---> g l) F"
+  unfolding tendsto_at_iff_tendsto_nhds by (rule filterlim_compose[of g])
 
 lemma tendsto_compose_eventually:
   assumes g: "(g ---> m) (at l)"
   assumes f: "(f ---> l) F"
   assumes inj: "eventually (\<lambda>x. f x \<noteq> l) F"
   shows "((\<lambda>x. g (f x)) ---> m) F"
-proof (rule topological_tendstoI)
-  fix B assume B: "open B" "m \<in> B"
-  obtain A where A: "open A" "l \<in> A"
-    and gB: "\<And>y. y \<in> A \<Longrightarrow> y \<noteq> l \<Longrightarrow> g y \<in> B"
-    using topological_tendstoD [OF g B]
-    unfolding eventually_at_topological by fast
-  show "eventually (\<lambda>x. g (f x) \<in> B) F"
-    using topological_tendstoD [OF f A] inj
-    by (rule eventually_elim2) (simp add: gB)
+proof -
+  from f inj have "LIM x F. f x :> at l"
+    unfolding filterlim_def at_def by (simp add: le_within_iff eventually_filtermap)
+  from filterlim_compose[OF g this] show ?thesis .
 qed
 
 lemma metric_tendsto_imp_tendsto:
@@ -1081,12 +1083,34 @@
   by (safe elim!: filterlimE intro!: filterlimI)
      (auto simp: eventually_at_top_dense elim!: eventually_elim1)
 
+lemma filterlim_at_top_gt:
+  fixes f :: "'a \<Rightarrow> ('b::dense_linorder)" and c :: "'b"
+  shows "(LIM x F. f x :> at_top) \<longleftrightarrow> (\<forall>Z>c. eventually (\<lambda>x. Z < f x) F)"
+  unfolding filterlim_at_top
+proof safe
+  fix Z assume *: "\<forall>Z>c. eventually (\<lambda>x. Z < f x) F"
+  from gt_ex[of "max Z c"] guess x ..
+  with *[THEN spec, of x] show "eventually (\<lambda>x. Z < f x) F"
+    by (auto elim!: eventually_elim1)
+qed simp
+
 lemma filterlim_at_bot: 
   fixes f :: "'a \<Rightarrow> ('b::dense_linorder)"
   shows "(LIM x F. f x :> at_bot) \<longleftrightarrow> (\<forall>Z. eventually (\<lambda>x. f x < Z) F)"
   by (safe elim!: filterlimE intro!: filterlimI)
      (auto simp: eventually_at_bot_dense elim!: eventually_elim1)
 
+lemma filterlim_at_bot_lt:
+  fixes f :: "'a \<Rightarrow> ('b::dense_linorder)" and c :: "'b"
+  shows "(LIM x F. f x :> at_bot) \<longleftrightarrow> (\<forall>Z<c. eventually (\<lambda>x. Z > f x) F)"
+  unfolding filterlim_at_bot
+proof safe
+  fix Z assume *: "\<forall>Z<c. eventually (\<lambda>x. Z > f x) F"
+  from lt_ex[of "min Z c"] guess x ..
+  with *[THEN spec, of x] show "eventually (\<lambda>x. Z > f x) F"
+    by (auto elim!: eventually_elim1)
+qed simp
+
 lemma filterlim_real_sequentially: "LIM x sequentially. real x :> at_top"
   unfolding filterlim_at_top
   apply (intro allI)
@@ -1094,4 +1118,50 @@
   apply (auto simp: natceiling_le_eq)
   done
 
+lemma filterlim_inverse_at_top_pos:
+  "LIM x (nhds 0 within {0::real <..}). inverse x :> at_top"
+  unfolding filterlim_at_top_gt[where c=0] eventually_within
+proof safe
+  fix Z :: real assume [arith]: "0 < Z"
+  then have "eventually (\<lambda>x. x < inverse Z) (nhds 0)"
+    by (auto simp add: eventually_nhds_metric dist_real_def intro!: exI[of _ "\<bar>inverse Z\<bar>"])
+  then show "eventually (\<lambda>x. x \<in> {0<..} \<longrightarrow> Z < inverse x) (nhds 0)"
+    by (auto elim!: eventually_elim1 simp: inverse_eq_divide field_simps)
+qed
+
+lemma filterlim_inverse_at_top:
+  "(f ---> (0 :: real)) F \<Longrightarrow> eventually (\<lambda>x. 0 < f x) F \<Longrightarrow> LIM x F. inverse (f x) :> at_top"
+  by (intro filterlim_compose[OF filterlim_inverse_at_top_pos])
+     (simp add: filterlim_def eventually_filtermap le_within_iff)
+
+lemma filterlim_inverse_at_bot_neg:
+  "LIM x (nhds 0 within {..< 0::real}). inverse x :> at_bot"
+  unfolding filterlim_at_bot_lt[where c=0] eventually_within
+proof safe
+  fix Z :: real assume [arith]: "Z < 0"
+  have "eventually (\<lambda>x. inverse Z < x) (nhds 0)"
+    by (auto simp add: eventually_nhds_metric dist_real_def intro!: exI[of _ "\<bar>inverse Z\<bar>"])
+  then show "eventually (\<lambda>x. x \<in> {..< 0} \<longrightarrow> inverse x < Z) (nhds 0)"
+    by (auto elim!: eventually_elim1 simp: inverse_eq_divide field_simps)
+qed
+
+lemma filterlim_inverse_at_bot:
+  "(f ---> (0 :: real)) F \<Longrightarrow> eventually (\<lambda>x. f x < 0) F \<Longrightarrow> LIM x F. inverse (f x) :> at_bot"
+  by (intro filterlim_compose[OF filterlim_inverse_at_bot_neg])
+     (simp add: filterlim_def eventually_filtermap le_within_iff)
+
+lemma filterlim_uminus_at_top_at_bot: "LIM x at_bot. - x :: real :> at_top"
+  unfolding filterlim_at_top eventually_at_bot_dense
+  by (blast intro: less_minus_iff[THEN iffD1])
+
+lemma filterlim_uminus_at_top: "LIM x F. f x :> at_bot \<Longrightarrow> LIM x F. - (f x) :: real :> at_top"
+  by (rule filterlim_compose[OF filterlim_uminus_at_top_at_bot])
+
+lemma filterlim_uminus_at_bot_at_top: "LIM x at_top. - x :: real :> at_bot"
+  unfolding filterlim_at_bot eventually_at_top_dense
+  by (blast intro: minus_less_iff[THEN iffD1])
+
+lemma filterlim_uminus_at_bot: "LIM x F. f x :> at_top \<Longrightarrow> LIM x F. - (f x) :: real :> at_bot"
+  by (rule filterlim_compose[OF filterlim_uminus_at_bot_at_top])
+
 end