# HG changeset patch
# User wenzelm
# Date 1436893720 -7200
# Node ID daf200e2d79ab2b30aed43b4668429b38a0fc55d
# Parent  c1b7793c23a31410736eae9d6ccfb7e8659ed7d0# Parent  4fce5d462afc432f00128f01bf378e06de026330
merged

diff -r 4fce5d462afc -r daf200e2d79a src/HOL/Filter.thy
--- a/src/HOL/Filter.thy	Tue Jul 14 19:08:27 2015 +0200
+++ b/src/HOL/Filter.thy	Tue Jul 14 19:08:40 2015 +0200
@@ -602,8 +602,10 @@
   finally show ?thesis .
 qed
 
-lemma eventually_gt_at_top:
-  "eventually (\<lambda>x. (c::_::unbounded_dense_linorder) < x) at_top"
+lemma eventually_at_top_not_equal: "eventually (\<lambda>x::'a::{no_top, linorder}. x \<noteq> c) at_top"
+  unfolding eventually_at_top_dense by auto
+
+lemma eventually_gt_at_top: "eventually (\<lambda>x. (c::_::{no_top, linorder}) < x) at_top"
   unfolding eventually_at_top_dense by auto
 
 definition at_bot :: "('a::order) filter"
@@ -631,6 +633,9 @@
   finally show ?thesis .
 qed
 
+lemma eventually_at_bot_not_equal: "eventually (\<lambda>x::'a::{no_bot, linorder}. x \<noteq> c) at_bot"
+  unfolding eventually_at_bot_dense by auto
+
 lemma eventually_gt_at_bot:
   "eventually (\<lambda>x. x < (c::_::unbounded_dense_linorder)) at_bot"
   unfolding eventually_at_bot_dense by auto
@@ -778,6 +783,21 @@
 lemma filtermap_eq_strong: "inj f \<Longrightarrow> filtermap f F = filtermap f G \<longleftrightarrow> F = G"
   by (simp add: filtermap_mono_strong eq_iff)
 
+lemma filtermap_fun_inverse:
+  assumes g: "filterlim g F G"
+  assumes f: "filterlim f G F"
+  assumes ev: "eventually (\<lambda>x. f (g x) = x) G"
+  shows "filtermap f F = G"
+proof (rule antisym)
+  show "filtermap f F \<le> G"
+    using f unfolding filterlim_def .
+  have "G = filtermap f (filtermap g G)"
+    using ev by (auto elim: eventually_elim2 simp: filter_eq_iff eventually_filtermap)
+  also have "\<dots> \<le> filtermap f F"
+    using g by (intro filtermap_mono) (simp add: filterlim_def)
+  finally show "G \<le> filtermap f F" .
+qed
+
 lemma filterlim_principal:
   "(LIM x F. f x :> principal S) \<longleftrightarrow> (eventually (\<lambda>x. f x \<in> S) F)"
   unfolding filterlim_def eventually_filtermap le_principal ..
diff -r 4fce5d462afc -r daf200e2d79a src/HOL/Library/Extended_Real.thy
--- a/src/HOL/Library/Extended_Real.thy	Tue Jul 14 19:08:27 2015 +0200
+++ b/src/HOL/Library/Extended_Real.thy	Tue Jul 14 19:08:40 2015 +0200
@@ -1697,6 +1697,7 @@
   show "\<exists>a b::ereal. a \<noteq> b"
     using zero_neq_one by blast
 qed
+
 subsubsection "Topological space"
 
 instantiation ereal :: linear_continuum_topology
@@ -1710,14 +1711,17 @@
 
 end
 
+lemma continuous_on_compose': 
+  "continuous_on s f \<Longrightarrow> continuous_on t g \<Longrightarrow> f`s \<subseteq> t \<Longrightarrow> continuous_on s (\<lambda>x. g (f x))"
+  using continuous_on_compose[of s f g] continuous_on_subset[of t g "f`s"] by auto
+
+lemma continuous_on_ereal[continuous_intros]:
+  assumes f: "continuous_on s f" shows "continuous_on s (\<lambda>x. ereal (f x))"
+  by (rule continuous_on_compose'[OF f continuous_onI_mono[of ereal UNIV]]) auto
+
 lemma tendsto_ereal[tendsto_intros, simp, intro]: "(f ---> x) F \<Longrightarrow> ((\<lambda>x. ereal (f x)) ---> ereal x) F"
-  apply (rule tendsto_compose[where g=ereal])
-  apply (auto intro!: order_tendstoI simp: eventually_at_topological)
-  apply (rule_tac x="case a of MInfty \<Rightarrow> UNIV | ereal x \<Rightarrow> {x <..} | PInfty \<Rightarrow> {}" in exI)
-  apply (auto split: ereal.split) []
-  apply (rule_tac x="case a of MInfty \<Rightarrow> {} | ereal x \<Rightarrow> {..< x} | PInfty \<Rightarrow> UNIV" in exI)
-  apply (auto split: ereal.split) []
-  done
+  using isCont_tendsto_compose[of x ereal f F] continuous_on_ereal[of UNIV "\<lambda>x. x"]
+  by (simp add: continuous_on_eq_continuous_at)
 
 lemma tendsto_uminus_ereal[tendsto_intros, simp, intro]: "(f ---> x) F \<Longrightarrow> ((\<lambda>x. - f x::ereal) ---> - x) F"
   apply (rule tendsto_compose[where g=uminus])
@@ -1808,9 +1812,6 @@
 lemma continuous_at_ereal[continuous_intros]: "continuous F f \<Longrightarrow> continuous F (\<lambda>x. ereal (f x))"
   unfolding continuous_def by auto
 
-lemma continuous_on_ereal[continuous_intros]: "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. ereal (f x))"
-  unfolding continuous_on_def by auto
-
 lemma ereal_Sup:
   assumes *: "\<bar>SUP a:A. ereal a\<bar> \<noteq> \<infinity>"
   shows "ereal (Sup A) = (SUP a:A. ereal a)"
diff -r 4fce5d462afc -r daf200e2d79a src/HOL/Limits.thy
--- a/src/HOL/Limits.thy	Tue Jul 14 19:08:27 2015 +0200
+++ b/src/HOL/Limits.thy	Tue Jul 14 19:08:40 2015 +0200
@@ -901,30 +901,13 @@
 
 lemmas filterlim_split_at_real = filterlim_split_at[where 'a=real]
 
-lemma filtermap_homeomorph:
-  assumes f: "continuous (at a) f"
-  assumes g: "continuous (at (f a)) g"
-  assumes bij1: "\<forall>x. f (g x) = x" and bij2: "\<forall>x. g (f x) = x"
-  shows "filtermap f (nhds a) = nhds (f a)"
-  unfolding filter_eq_iff eventually_filtermap eventually_nhds
-proof safe
-  fix P S assume S: "open S" "f a \<in> S" and P: "\<forall>x\<in>S. P x"
-  from continuous_within_topological[THEN iffD1, rule_format, OF f S] P
-  show "\<exists>S. open S \<and> a \<in> S \<and> (\<forall>x\<in>S. P (f x))" by auto
-next
-  fix P S assume S: "open S" "a \<in> S" and P: "\<forall>x\<in>S. P (f x)"
-  with continuous_within_topological[THEN iffD1, rule_format, OF g, of S] bij2
-  obtain A where "open A" "f a \<in> A" "(\<forall>y\<in>A. g y \<in> S)"
-    by (metis UNIV_I)
-  with P bij1 show "\<exists>S. open S \<and> f a \<in> S \<and> (\<forall>x\<in>S. P x)"
-    by (force intro!: exI[of _ A])
-qed
-
 lemma filtermap_nhds_shift: "filtermap (\<lambda>x. x - d) (nhds a) = nhds (a - d::'a::real_normed_vector)"
-  by (rule filtermap_homeomorph[where g="\<lambda>x. x + d"]) (auto intro: continuous_intros)
+  by (rule filtermap_fun_inverse[where g="\<lambda>x. x + d"])
+     (auto intro!: tendsto_eq_intros filterlim_ident)
 
 lemma filtermap_nhds_minus: "filtermap (\<lambda>x. - x) (nhds a) = nhds (- a::'a::real_normed_vector)"
-  by (rule filtermap_homeomorph[where g=uminus]) (auto intro: continuous_minus)
+  by (rule filtermap_fun_inverse[where g=uminus])
+     (auto intro!: tendsto_eq_intros filterlim_ident)
 
 lemma filtermap_at_shift: "filtermap (\<lambda>x. x - d) (at a) = at (a - d::'a::real_normed_vector)"
   by (simp add: filter_eq_iff eventually_filtermap eventually_at_filter filtermap_nhds_shift[symmetric])
@@ -960,9 +943,17 @@
   "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_uminus_at_top_at_bot: "LIM x at_bot. - x :: real :> at_top"
+  unfolding filterlim_at_top eventually_at_bot_dense
+  by (metis leI minus_less_iff order_less_asym)
+
+lemma filterlim_uminus_at_bot_at_top: "LIM x at_top. - x :: real :> at_bot"
+  unfolding filterlim_at_bot eventually_at_top_dense
+  by (metis leI less_minus_iff order_less_asym)
+
 lemma at_top_mirror: "at_top = filtermap uminus (at_bot :: real filter)"
-  unfolding filter_eq_iff eventually_filtermap eventually_at_top_linorder eventually_at_bot_linorder
-  by (metis le_minus_iff minus_minus)
+  by (rule filtermap_fun_inverse[symmetric, of uminus])
+     (auto intro: filterlim_uminus_at_bot_at_top filterlim_uminus_at_top_at_bot)
 
 lemma at_bot_mirror: "at_bot = filtermap uminus (at_top :: real filter)"
   unfolding at_top_mirror filtermap_filtermap by (simp add: filtermap_ident)
@@ -973,14 +964,6 @@
 lemma filterlim_at_bot_mirror: "(LIM x at_bot. f x :> F) \<longleftrightarrow> (LIM x at_top. f (-x::real) :> F)"
   unfolding filterlim_def at_bot_mirror filtermap_filtermap ..
 
-lemma filterlim_uminus_at_top_at_bot: "LIM x at_bot. - x :: real :> at_top"
-  unfolding filterlim_at_top eventually_at_bot_dense
-  by (metis leI minus_less_iff order_less_asym)
-
-lemma filterlim_uminus_at_bot_at_top: "LIM x at_top. - x :: real :> at_bot"
-  unfolding filterlim_at_bot eventually_at_top_dense
-  by (metis leI less_minus_iff order_less_asym)
-
 lemma filterlim_uminus_at_top: "(LIM x F. f x :> at_top) \<longleftrightarrow> (LIM x F. - (f x) :: real :> at_bot)"
   using filterlim_compose[OF filterlim_uminus_at_bot_at_top, of f F]
   using filterlim_compose[OF filterlim_uminus_at_top_at_bot, of "\<lambda>x. - f x" F]
@@ -999,20 +982,6 @@
     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_right])
-     (simp add: filterlim_def eventually_filtermap eventually_elim1 at_within_def le_principal)
-
-lemma filterlim_inverse_at_bot_neg:
-  "LIM x (at_left (0::real)). inverse x :> at_bot"
-  by (simp add: filterlim_inverse_at_top_right filterlim_uminus_at_bot filterlim_at_left_to_right)
-
-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"
-  unfolding filterlim_uminus_at_bot inverse_minus_eq[symmetric]
-  by (rule filterlim_inverse_at_top) (simp_all add: tendsto_minus_cancel_left[symmetric])
-
 lemma tendsto_inverse_0:
   fixes x :: "_ \<Rightarrow> 'a\<Colon>real_normed_div_algebra"
   shows "(inverse ---> (0::'a)) at_infinity"
@@ -1029,18 +998,28 @@
   qed
 qed
 
+lemma filterlim_inverse_at_right_top: "LIM x at_top. inverse x :> at_right (0::real)"
+  unfolding filterlim_at
+  by (auto simp: eventually_at_top_dense)
+     (metis tendsto_inverse_0 filterlim_mono at_top_le_at_infinity order_refl)
+
+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_right])
+     (simp add: filterlim_def eventually_filtermap eventually_elim1 at_within_def le_principal)
+
+lemma filterlim_inverse_at_bot_neg:
+  "LIM x (at_left (0::real)). inverse x :> at_bot"
+  by (simp add: filterlim_inverse_at_top_right filterlim_uminus_at_bot filterlim_at_left_to_right)
+
+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"
+  unfolding filterlim_uminus_at_bot inverse_minus_eq[symmetric]
+  by (rule filterlim_inverse_at_top) (simp_all add: tendsto_minus_cancel_left[symmetric])
+
 lemma at_right_to_top: "(at_right (0::real)) = filtermap inverse at_top"
-proof (rule antisym)
-  have "(inverse ---> (0::real)) at_top"
-    by (metis tendsto_inverse_0 filterlim_mono at_top_le_at_infinity order_refl)
-  then show "filtermap inverse at_top \<le> at_right (0::real)"
-    by (simp add: le_principal eventually_filtermap eventually_gt_at_top filterlim_def at_within_def)
-next
-  have "filtermap inverse (filtermap inverse (at_right (0::real))) \<le> filtermap inverse at_top"
-    using filterlim_inverse_at_top_right unfolding filterlim_def by (rule filtermap_mono)
-  then show "at_right (0::real) \<le> filtermap inverse at_top"
-    by (simp add: filtermap_ident filtermap_filtermap)
-qed
+  by (intro filtermap_fun_inverse[symmetric, where g=inverse])
+     (auto intro: filterlim_inverse_at_top_right filterlim_inverse_at_right_top)
 
 lemma eventually_at_right_to_top:
   "eventually P (at_right (0::real)) \<longleftrightarrow> eventually (\<lambda>x. P (inverse x)) at_top"
diff -r 4fce5d462afc -r daf200e2d79a src/HOL/Topological_Spaces.thy
--- a/src/HOL/Topological_Spaces.thy	Tue Jul 14 19:08:27 2015 +0200
+++ b/src/HOL/Topological_Spaces.thy	Tue Jul 14 19:08:40 2015 +0200
@@ -1423,6 +1423,61 @@
   "continuous_on t g \<Longrightarrow> continuous_on s f \<Longrightarrow> t = f ` s \<Longrightarrow> continuous_on s (\<lambda>x. g (f x))"
   using continuous_on_compose[of s f g] by (simp add: comp_def)
 
+lemma continuous_on_generate_topology:
+  assumes *: "open = generate_topology X"
+  assumes **: "\<And>B. B \<in> X \<Longrightarrow> \<exists>C. open C \<and> C \<inter> A = f -` B \<inter> A"
+  shows "continuous_on A f"
+  unfolding continuous_on_open_invariant
+proof safe
+  fix B :: "'a set" assume "open B" then show "\<exists>C. open C \<and> C \<inter> A = f -` B \<inter> A"
+    unfolding *
+  proof induction
+    case (UN K)
+    then obtain C where "\<And>k. k \<in> K \<Longrightarrow> open (C k)" "\<And>k. k \<in> K \<Longrightarrow> C k \<inter> A = f -` k \<inter> A"
+      by metis
+    then show ?case
+      by (intro exI[of _ "\<Union>k\<in>K. C k"]) blast
+  qed (auto intro: **)
+qed
+
+lemma continuous_onI_mono:
+  fixes f :: "'a::linorder_topology \<Rightarrow> 'b::{dense_order, linorder_topology}"
+  assumes "open (f`A)"
+  assumes mono: "\<And>x y. x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> x \<le> y \<Longrightarrow> f x \<le> f y"
+  shows "continuous_on A f"
+proof (rule continuous_on_generate_topology[OF open_generated_order], safe)
+  have monoD: "\<And>x y. x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> f x < f y \<Longrightarrow> x < y"
+    by (auto simp: not_le[symmetric] mono)
+
+  { fix a b assume "a \<in> A" "f a < b"
+    moreover
+    with open_right[OF \<open>open (f`A)\<close>, of "f a" b] obtain y where "f a < y" "{f a ..< y} \<subseteq> f`A"
+      by auto
+    moreover then obtain z where "f a < z" "z < min b y"
+      using dense[of "f a" "min b y"] \<open>f a < y\<close> \<open>f a < b\<close> by auto
+    moreover then obtain c where "z = f c" "c \<in> A"
+      using \<open>{f a ..< y} \<subseteq> f`A\<close>[THEN subsetD, of z] by (auto simp: less_imp_le)
+    ultimately have "\<exists>x. x \<in> A \<and> f x < b \<and> a < x"
+      by (auto intro!: exI[of _ c] simp: monoD) }
+  then show "\<exists>C. open C \<and> C \<inter> A = f -` {..<b} \<inter> A" for b
+    by (intro exI[of _ "(\<Union>x\<in>{x\<in>A. f x < b}. {..< x})"])
+       (auto intro: le_less_trans[OF mono] less_imp_le)
+
+  { fix a b assume "a \<in> A" "b < f a"
+    moreover
+    with open_left[OF \<open>open (f`A)\<close>, of "f a" b] obtain y where "y < f a" "{y <.. f a} \<subseteq> f`A"
+      by auto
+    moreover then obtain z where "max b y < z" "z < f a"
+      using dense[of "max b y" "f a"] \<open>y < f a\<close> \<open>b < f a\<close> by auto
+    moreover then obtain c where "z = f c" "c \<in> A"
+      using \<open>{y <.. f a} \<subseteq> f`A\<close>[THEN subsetD, of z] by (auto simp: less_imp_le)
+    ultimately have "\<exists>x. x \<in> A \<and> b < f x \<and> x < a"
+      by (auto intro!: exI[of _ c] simp: monoD) }
+  then show "\<exists>C. open C \<and> C \<inter> A = f -` {b <..} \<inter> A" for b
+    by (intro exI[of _ "(\<Union>x\<in>{x\<in>A. b < f x}. {x <..})"])
+       (auto intro: less_le_trans[OF _ mono] less_imp_le)
+qed
+
 subsubsection {* Continuity at a point *}
 
 definition continuous :: "'a::t2_space filter \<Rightarrow> ('a \<Rightarrow> 'b::topological_space) \<Rightarrow> bool" where
diff -r 4fce5d462afc -r daf200e2d79a src/HOL/Transcendental.thy
--- a/src/HOL/Transcendental.thy	Tue Jul 14 19:08:27 2015 +0200
+++ b/src/HOL/Transcendental.thy	Tue Jul 14 19:08:40 2015 +0200
@@ -2016,6 +2016,13 @@
   by (rule filterlim_at_top_at_top[where Q="\<lambda>x. 0 < x" and P="\<lambda>x. True" and g="exp"])
      (auto intro: eventually_gt_at_top)
 
+lemma filtermap_ln_at_top: "filtermap (ln::real \<Rightarrow> real) at_top = at_top"
+  by (intro filtermap_fun_inverse[of exp] exp_at_top ln_at_top) auto
+
+lemma filtermap_exp_at_top: "filtermap (exp::real \<Rightarrow> real) at_top = at_top"
+  by (intro filtermap_fun_inverse[of ln] exp_at_top ln_at_top)
+     (auto simp: eventually_at_top_dense)
+
 lemma tendsto_power_div_exp_0: "((\<lambda>x. x ^ k / exp x) ---> (0::real)) at_top"
 proof (induct k)
   case 0