src/HOL/Library/Extended_Real.thy

   shows "continuous (at_left x) f"
 proof cases
   assume "x = bot" then show ?thesis
     by (simp add: trivial_limit_at_left_bot)
 next
-  assume x: "x \<noteq> bot" 
+  assume x: "x \<noteq> bot"
   show ?thesis
     unfolding continuous_within
   proof (intro tendsto_at_left_sequentially[of bot])
     fix S :: "nat \<Rightarrow> 'a" assume S: "incseq S" and S_x: "S ----> x"
     from S_x have x_eq: "x = (SUP i. S i)"

 lemma sup_continuous_iff_at_left:
   fixes f :: "'a \<Rightarrow> 'a::{complete_linorder, linorder_topology, first_countable_topology}"
   shows "sup_continuous f \<longleftrightarrow> (\<forall>x. continuous (at_left x) f) \<and> mono f"
   using sup_continuous_at_left[of f] continuous_at_left_imp_sup_continuous[of f]
     sup_continuous_mono[of f] by auto
-  
+
 lemma continuous_at_right_imp_inf_continuous:
   fixes f :: "'a \<Rightarrow> 'a::{complete_linorder, linorder_topology}"
   assumes "mono f" "\<And>x. continuous (at_right x) f"
   shows "inf_continuous f"
   unfolding inf_continuous_def

   shows "continuous (at_right x) f"
 proof cases
   assume "x = top" then show ?thesis
     by (simp add: trivial_limit_at_right_top)
 next
-  assume x: "x \<noteq> top" 
+  assume x: "x \<noteq> top"
   show ?thesis
     unfolding continuous_within
   proof (intro tendsto_at_right_sequentially[of _ top])
     fix S :: "nat \<Rightarrow> 'a" assume S: "decseq S" and S_x: "S ----> x"
     from S_x have x_eq: "x = (INF i. S i)"

 
 lemma abs_ereal_pos[simp]: "0 \<le> \<bar>x :: ereal\<bar>"
   by (cases x) auto
 
 lemma ereal_abs_leI:
-  fixes x y :: ereal 
+  fixes x y :: ereal
   shows "\<lbrakk> x \<le> y; -x \<le> y \<rbrakk> \<Longrightarrow> \<bar>x\<bar> \<le> y"
 by(cases x y rule: ereal2_cases)(simp_all)
 
 lemma real_of_ereal_le_0[simp]: "real_of_ereal (x :: ereal) \<le> 0 \<longleftrightarrow> x \<le> 0 \<or> x = \<infinity>"
   by (cases x) auto

        (simp_all add: zero_ereal_def zero_less_mult_iff)
 qed
 
 end
 
-lemma [simp]: 
+lemma [simp]:
   shows ereal_1_times: "ereal 1 * x = x"
   and times_ereal_1: "x * ereal 1 = x"
 by(simp_all add: one_ereal_def[symmetric])
 
 lemma one_not_le_zero_ereal[simp]: "\<not> (1 \<le> (0::ereal))"

 lemma ereal_left_mult_cong:
   fixes a b c :: ereal
   shows  "c = d \<Longrightarrow> (d \<noteq> 0 \<Longrightarrow> a = b) \<Longrightarrow> a * c = b * d"
   by (cases "c = 0") simp_all
 
-lemma ereal_right_mult_cong: 
+lemma ereal_right_mult_cong:
   fixes a b c :: ereal
   shows "c = d \<Longrightarrow> (d \<noteq> 0 \<Longrightarrow> a = b) \<Longrightarrow> c * a = d * b"
   by (cases "c = 0") simp_all
 
 lemma ereal_distrib:

   fixes x y :: ereal
   shows "x - y = \<infinity> \<longleftrightarrow> y = -\<infinity> \<or> x = \<infinity>"
   by (cases x y rule: ereal2_cases) simp_all
 
 lemma ereal_diff_add_eq_diff_diff_swap:
-  fixes x y z :: ereal 
+  fixes x y z :: ereal
   shows "\<bar>y\<bar> \<noteq> \<infinity> \<Longrightarrow> x - (y + z) = x - y - z"
 by(cases x y z rule: ereal3_cases) simp_all
 
 lemma ereal_diff_add_assoc2:
   fixes x y z :: ereal

 by(cases x y z rule: ereal3_cases) simp_all
 
 lemma ereal_add_uminus_conv_diff: fixes x y z :: ereal shows "- x + y = y - x"
 by(cases x y rule: ereal2_cases) simp_all
 
-lemma ereal_minus_diff_eq: 
-  fixes x y :: ereal 
+lemma ereal_minus_diff_eq:
+  fixes x y :: ereal
   shows "\<lbrakk> x = \<infinity> \<longrightarrow> y \<noteq> \<infinity>; x = -\<infinity> \<longrightarrow> y \<noteq> - \<infinity> \<rbrakk> \<Longrightarrow> - (x - y) = y - x"
 by(cases x y rule: ereal2_cases) simp_all
 
 lemma ediff_le_self [simp]: "x - y \<le> (x :: enat)"
 by(cases x y rule: enat.exhaust[case_product enat.exhaust]) simp_all

 instance
   by standard (simp add: open_ereal_generated)
 
 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
+  by (rule continuous_on_compose2 [OF continuous_onI_mono[of ereal UNIV] f]) auto
 
 lemma tendsto_ereal[tendsto_intros, simp, intro]: "(f ---> x) F \<Longrightarrow> ((\<lambda>x. ereal (f x)) ---> ereal x) F"
   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)
 

     assume "- \<infinity> < c" "c < 0"
     then have "0 < - c" "- c < \<infinity>"
       by (auto simp: ereal_uminus_reorder ereal_less_uminus_reorder[of 0])
     then have "((\<lambda>x. (- c) * f x) ---> (- c) * x) F"
       by (rule *)
-    from tendsto_uminus_ereal[OF this] show ?thesis 
+    from tendsto_uminus_ereal[OF this] show ?thesis
       by simp
   qed (auto intro!: *)
 qed
 
 lemma tendsto_cmult_ereal_not_0[tendsto_intros, simp, intro]:

     by (subst continuous_at_Sup_mono[where f="\<lambda>x. c * x"])
        (auto simp: mono_def continuous_at continuous_at_imp_continuous_at_within \<open>I \<noteq> {}\<close>
              intro!: ereal_mult_left_mono c)
 qed
 
-lemma countable_approach: 
+lemma countable_approach:
   fixes x :: ereal
   assumes "x \<noteq> -\<infinity>"
   shows "\<exists>f. incseq f \<and> (\<forall>i::nat. f i < x) \<and> (f ----> x)"
 proof (cases x)
   case (real r)
   moreover have "(\<lambda>n. r - inverse (real (Suc n))) ----> r - 0"
     by (intro tendsto_intros LIMSEQ_inverse_real_of_nat)
   ultimately show ?thesis
     by (intro exI[of _ "\<lambda>n. x - inverse (Suc n)"]) (auto simp: incseq_def)
-next 
+next
   case PInf with LIMSEQ_SUP[of "\<lambda>n::nat. ereal (real n)"] show ?thesis
     by (intro exI[of _ "\<lambda>n. ereal (real n)"]) (auto simp: incseq_def SUP_nat_Infty)
 qed (simp add: assms)
 
 lemma Sup_countable_SUP:

       fix i assume "i \<in> I" then show "0 \<le> f n i" "0 \<le> (\<Sum>l\<in>N. f l i)"
         using insert by (auto intro!: setsum_nonneg nonneg)
     next
       fix i j assume "i \<in> I" "j \<in> I"
       from directed[OF \<open>insert n N \<subseteq> A\<close> this] guess k ..
-      then show "\<exists>k\<in>I. f n i + (\<Sum>l\<in>N. f l j) \<le> f n k + (\<Sum>l\<in>N. f l k)" 
+      then show "\<exists>k\<in>I. f n i + (\<Sum>l\<in>N. f l j) \<le> f n k + (\<Sum>l\<in>N. f l k)"
         by (intro bexI[of _ k]) (auto intro!: ereal_add_mono setsum_mono)
     qed
     ultimately show ?case
       by simp
   qed (simp_all add: SUP_constant \<open>I \<noteq> {}\<close>)

   fixes X :: "nat \<Rightarrow> real" and L :: real
   assumes 1: "limsup X \<le> L" and 2: "L \<le> liminf X"
   shows "X ----> L"
 proof -
   from 1 2 have "limsup X \<le> liminf X" by auto
-  hence 3: "limsup X = liminf X"  
+  hence 3: "limsup X = liminf X"
     apply (subst eq_iff, rule conjI)
     by (rule Liminf_le_Limsup, auto)
   hence 4: "convergent (\<lambda>n. ereal (X n))"
     by (subst convergent_ereal)
   hence "limsup X = lim (\<lambda>n. ereal(X n))"
     by (rule convergent_limsup_cl)
   also from 1 2 3 have "limsup X = L" by auto
   finally have "lim (\<lambda>n. ereal(X n)) = L" ..
   hence "(\<lambda>n. ereal (X n)) ----> L"
     apply (elim subst)
-    by (subst convergent_LIMSEQ_iff [symmetric], rule 4) 
+    by (subst convergent_LIMSEQ_iff [symmetric], rule 4)
   thus ?thesis by simp
 qed
 
 lemma liminf_PInfty:
   fixes X :: "nat \<Rightarrow> ereal"

 
 lemma inverse_infty_ereal_tendsto_0: "inverse -- \<infinity> --> (0::ereal)"
 proof -
   have **: "((\<lambda>x. ereal (inverse x)) ---> ereal 0) at_infinity"
     by (intro tendsto_intros tendsto_inverse_0)
-  
+
   show ?thesis
     by (simp add: at_infty_ereal_eq_at_top tendsto_compose_filtermap[symmetric] comp_def)
        (auto simp: eventually_at_top_linorder exI[of _ 1] zero_ereal_def at_top_le_at_infinity
              intro!: filterlim_mono_eventually[OF **])
 qed
 
-lemma inverse_ereal_tendsto_pos: 
+lemma inverse_ereal_tendsto_pos:
   fixes x :: ereal assumes "0 < x"
   shows "inverse -- x --> inverse x"
 proof (cases x)
   case (real r)
   with \<open>0 < x\<close> have **: "(\<lambda>x. ereal (inverse x)) -- r --> ereal (inverse r)"