# HG changeset patch
# User wenzelm
# Date 1448135844 -3600
# Node ID 2b775b88889714b65714337ed35d3045e313e4dc
# Parent  30d4ccd5486144e375b6178410c373090653a2e2
tuned proofs;

diff -r 30d4ccd54861 -r 2b775b888897 src/HOL/Library/Liminf_Limsup.thy
--- a/src/HOL/Library/Liminf_Limsup.thy	Sat Nov 21 20:19:20 2015 +0100
+++ b/src/HOL/Library/Liminf_Limsup.thy	Sat Nov 21 20:57:24 2015 +0100
@@ -43,12 +43,12 @@
 abbreviation "limsup \<equiv> Limsup sequentially"
 
 lemma Liminf_eqI:
-  "(\<And>P. eventually P F \<Longrightarrow> INFIMUM (Collect P) f \<le> x) \<Longrightarrow>  
+  "(\<And>P. eventually P F \<Longrightarrow> INFIMUM (Collect P) f \<le> x) \<Longrightarrow>
     (\<And>y. (\<And>P. eventually P F \<Longrightarrow> INFIMUM (Collect P) f \<le> y) \<Longrightarrow> x \<le> y) \<Longrightarrow> Liminf F f = x"
   unfolding Liminf_def by (auto intro!: SUP_eqI)
 
 lemma Limsup_eqI:
-  "(\<And>P. eventually P F \<Longrightarrow> x \<le> SUPREMUM (Collect P) f) \<Longrightarrow>  
+  "(\<And>P. eventually P F \<Longrightarrow> x \<le> SUPREMUM (Collect P) f) \<Longrightarrow>
     (\<And>y. (\<And>P. eventually P F \<Longrightarrow> y \<le> SUPREMUM (Collect P) f) \<Longrightarrow> y \<le> x) \<Longrightarrow> Limsup F f = x"
   unfolding Limsup_def by (auto intro!: INF_eqI)
 
@@ -60,7 +60,7 @@
   unfolding Limsup_def eventually_sequentially
   by (rule INF_eq) (auto simp: atLeast_def intro!: SUP_mono)
 
-lemma Limsup_const: 
+lemma Limsup_const:
   assumes ntriv: "\<not> trivial_limit F"
   shows "Limsup F (\<lambda>x. c) = c"
 proof -
@@ -157,7 +157,7 @@
   have "l = Limsup F (\<lambda>x. l)"
     using F by (simp add: Limsup_const)
   also have "\<dots> \<le> Limsup F f"
-    by (intro Limsup_mono x) 
+    by (intro Limsup_mono x)
   finally show ?thesis .
 qed
 
@@ -165,32 +165,32 @@
   fixes X :: "_ \<Rightarrow> _ :: complete_linorder"
   shows "C \<le> Liminf F X \<longleftrightarrow> (\<forall>y<C. eventually (\<lambda>x. y < X x) F)"
 proof -
-  { fix y P assume "eventually P F" "y < INFIMUM (Collect P) X"
-    then have "eventually (\<lambda>x. y < X x) F"
-      by (auto elim!: eventually_elim1 dest: less_INF_D) }
+  have "eventually (\<lambda>x. y < X x) F"
+    if "eventually P F" "y < INFIMUM (Collect P) X" for y P
+    using that by (auto elim!: eventually_elim1 dest: less_INF_D)
   moreover
-  { fix y P assume "y < C" and y: "\<forall>y<C. eventually (\<lambda>x. y < X x) F"
-    have "\<exists>P. eventually P F \<and> y < INFIMUM (Collect P) X"
-    proof (cases "\<exists>z. y < z \<and> z < C")
-      case True
-      then obtain z where z: "y < z \<and> z < C" ..
-      moreover from z have "z \<le> INFIMUM {x. z < X x} X"
-        by (auto intro!: INF_greatest)
-      ultimately show ?thesis
-        using y by (intro exI[of _ "\<lambda>x. z < X x"]) auto
-    next
-      case False
-      then have "C \<le> INFIMUM {x. y < X x} X"
-        by (intro INF_greatest) auto
-      with \<open>y < C\<close> show ?thesis
-        using y by (intro exI[of _ "\<lambda>x. y < X x"]) auto
-    qed }
+  have "\<exists>P. eventually P F \<and> y < INFIMUM (Collect P) X"
+    if "y < C" and y: "\<forall>y<C. eventually (\<lambda>x. y < X x) F" for y P
+  proof (cases "\<exists>z. y < z \<and> z < C")
+    case True
+    then obtain z where z: "y < z \<and> z < C" ..
+    moreover from z have "z \<le> INFIMUM {x. z < X x} X"
+      by (auto intro!: INF_greatest)
+    ultimately show ?thesis
+      using y by (intro exI[of _ "\<lambda>x. z < X x"]) auto
+  next
+    case False
+    then have "C \<le> INFIMUM {x. y < X x} X"
+      by (intro INF_greatest) auto
+    with \<open>y < C\<close> show ?thesis
+      using y by (intro exI[of _ "\<lambda>x. y < X x"]) auto
+  qed
   ultimately show ?thesis
     unfolding Liminf_def le_SUP_iff by auto
 qed
 
 lemma lim_imp_Liminf:
-  fixes f :: "'a \<Rightarrow> _ :: {complete_linorder, linorder_topology}"
+  fixes f :: "'a \<Rightarrow> _ :: {complete_linorder,linorder_topology}"
   assumes ntriv: "\<not> trivial_limit F"
   assumes lim: "(f ---> f0) F"
   shows "Liminf F f = f0"
@@ -229,7 +229,7 @@
 qed
 
 lemma lim_imp_Limsup:
-  fixes f :: "'a \<Rightarrow> _ :: {complete_linorder, linorder_topology}"
+  fixes f :: "'a \<Rightarrow> _ :: {complete_linorder,linorder_topology}"
   assumes ntriv: "\<not> trivial_limit F"
   assumes lim: "(f ---> f0) F"
   shows "Limsup F f = f0"
@@ -268,7 +268,7 @@
 qed
 
 lemma Liminf_eq_Limsup:
-  fixes f0 :: "'a :: {complete_linorder, linorder_topology}"
+  fixes f0 :: "'a :: {complete_linorder,linorder_topology}"
   assumes ntriv: "\<not> trivial_limit F"
     and lim: "Liminf F f = f0" "Limsup F f = f0"
   shows "(f ---> f0) F"
@@ -289,7 +289,7 @@
 qed
 
 lemma tendsto_iff_Liminf_eq_Limsup:
-  fixes f0 :: "'a :: {complete_linorder, linorder_topology}"
+  fixes f0 :: "'a :: {complete_linorder,linorder_topology}"
   shows "\<not> trivial_limit F \<Longrightarrow> (f ---> f0) F \<longleftrightarrow> (Liminf F f = f0 \<and> Limsup F f = f0)"
   by (metis Liminf_eq_Limsup lim_imp_Limsup lim_imp_Liminf)
 
@@ -311,32 +311,36 @@
   assumes "subseq r"
   shows "limsup (X \<circ> r) \<le> limsup X"
 proof-
-  have "\<And>n. (SUP m:{n..}. (X \<circ> r) m) \<le> (SUP m:{n..}. X m)"
+  have "(SUP m:{n..}. (X \<circ> r) m) \<le> (SUP m:{n..}. X m)" for n
   proof (safe intro!: SUP_mono)
-    fix n m :: nat assume "n \<le> m" then show "\<exists>ma\<in>{n..}. (X \<circ> r) m \<le> X ma"
+    fix m :: nat
+    assume "n \<le> m"
+    then show "\<exists>ma\<in>{n..}. (X \<circ> r) m \<le> X ma"
       using seq_suble[OF \<open>subseq r\<close>, of m] by (intro bexI[of _ "r m"]) auto
   qed
-  then show ?thesis by (auto intro!: INF_mono simp: limsup_INF_SUP comp_def)
+  then show ?thesis
+    by (auto intro!: INF_mono simp: limsup_INF_SUP comp_def)
 qed
 
-lemma continuous_on_imp_continuous_within: "continuous_on s f \<Longrightarrow> t \<subseteq> s \<Longrightarrow> x \<in> s \<Longrightarrow> continuous (at x within t) f"
-  unfolding continuous_on_eq_continuous_within by (auto simp: continuous_within intro: tendsto_within_subset)
+lemma continuous_on_imp_continuous_within:
+  "continuous_on s f \<Longrightarrow> t \<subseteq> s \<Longrightarrow> x \<in> s \<Longrightarrow> continuous (at x within t) f"
+  unfolding continuous_on_eq_continuous_within
+  by (auto simp: continuous_within intro: tendsto_within_subset)
 
 lemma Liminf_compose_continuous_antimono:
-  fixes f :: "'a::{complete_linorder, linorder_topology} \<Rightarrow> 'b::{complete_linorder, linorder_topology}"
-  assumes c: "continuous_on UNIV f" and am: "antimono f" and F: "F \<noteq> bot"
+  fixes f :: "'a::{complete_linorder,linorder_topology} \<Rightarrow> 'b::{complete_linorder,linorder_topology}"
+  assumes c: "continuous_on UNIV f"
+    and am: "antimono f"
+    and F: "F \<noteq> bot"
   shows "Liminf F (\<lambda>n. f (g n)) = f (Limsup F g)"
 proof -
-  { fix P assume "eventually P F"
-    have "\<exists>x. P x"
-    proof (rule ccontr)
-      assume "\<not> (\<exists>x. P x)" then have "P = (\<lambda>x. False)"
-        by auto
-      with \<open>eventually P F\<close> F show False
-        by auto
-    qed }
-  note * = this
-
+  have *: "\<exists>x. P x" if "eventually P F" for P
+  proof (rule ccontr)
+    assume "\<not> (\<exists>x. P x)" then have "P = (\<lambda>x. False)"
+      by auto
+    with \<open>eventually P F\<close> F show False
+      by auto
+  qed
   have "f (Limsup F g) = (SUP P : {P. eventually P F}. f (Sup (g ` Collect P)))"
     unfolding Limsup_def INF_def
     by (subst continuous_at_Inf_antimono[OF am continuous_on_imp_continuous_within[OF c]])