# HG changeset patch
# User wenzelm
# Date 1433960158 -7200
# Node ID 92d9557fb78c2308ce02232ec551d6e21ec8baa9
# Parent  884f54e014278c4ff76370e0b30e0b7e5ebef211
misc tuning;

diff -r 884f54e01427 -r 92d9557fb78c src/HOL/Multivariate_Analysis/Bounded_Continuous_Function.thy
--- a/src/HOL/Multivariate_Analysis/Bounded_Continuous_Function.thy	Wed Jun 10 19:10:20 2015 +0200
+++ b/src/HOL/Multivariate_Analysis/Bounded_Continuous_Function.thy	Wed Jun 10 20:15:58 2015 +0200
@@ -1,14 +1,15 @@
 section \<open>Bounded Continuous Functions\<close>
+
 theory Bounded_Continuous_Function
 imports Integration
 begin
 
-subsection\<open>Definition\<close>
+subsection \<open>Definition\<close>
 
-definition "bcontfun = {f :: 'a::topological_space \<Rightarrow> 'b::metric_space. continuous_on UNIV f \<and> bounded (range f)}"
+definition bcontfun :: "('a::topological_space \<Rightarrow> 'b::metric_space) set"
+  where "bcontfun = {f. continuous_on UNIV f \<and> bounded (range f)}"
 
-typedef ('a, 'b) bcontfun =
-    "bcontfun :: ('a::topological_space \<Rightarrow> 'b::metric_space) set"
+typedef ('a, 'b) bcontfun = "bcontfun :: ('a::topological_space \<Rightarrow> 'b::metric_space) set"
   by (auto simp: bcontfun_def intro: continuous_intros simp: bounded_def)
 
 lemma bcontfunE:
@@ -23,13 +24,11 @@
   using assms bcontfunE
   by metis
 
-lemma bcontfunI:
-  "continuous_on UNIV f \<Longrightarrow> (\<And>x. dist (f x) u \<le> b) \<Longrightarrow> f \<in> bcontfun"
+lemma bcontfunI: "continuous_on UNIV f \<Longrightarrow> (\<And>x. dist (f x) u \<le> b) \<Longrightarrow> f \<in> bcontfun"
   unfolding bcontfun_def
   by (metis (lifting, no_types) bounded_def dist_commute mem_Collect_eq rangeE)
 
-lemma bcontfunI':
-  "continuous_on UNIV f \<Longrightarrow> (\<And>x. dist (f x) undefined \<le> b) \<Longrightarrow> f \<in> bcontfun"
+lemma bcontfunI': "continuous_on UNIV f \<Longrightarrow> (\<And>x. dist (f x) undefined \<le> b) \<Longrightarrow> f \<in> bcontfun"
   using bcontfunI by metis
 
 lemma continuous_on_Rep_bcontfun[intro, simp]: "continuous_on T (Rep_bcontfun x)"
@@ -39,45 +38,47 @@
 instantiation bcontfun :: (topological_space, metric_space) metric_space
 begin
 
-definition dist_bcontfun::"('a, 'b) bcontfun \<Rightarrow> ('a, 'b) bcontfun \<Rightarrow> real" where
-  "dist_bcontfun f g = (SUP x. dist (Rep_bcontfun f x) (Rep_bcontfun g x))"
+definition dist_bcontfun :: "('a, 'b) bcontfun \<Rightarrow> ('a, 'b) bcontfun \<Rightarrow> real"
+  where "dist_bcontfun f g = (SUP x. dist (Rep_bcontfun f x) (Rep_bcontfun g x))"
 
-definition
-  open_bcontfun::"('a, 'b) bcontfun set \<Rightarrow> bool" where
-  "open_bcontfun S = (\<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S)"
+definition open_bcontfun :: "('a, 'b) bcontfun set \<Rightarrow> bool"
+  where "open_bcontfun S = (\<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S)"
 
 lemma dist_bounded:
-  fixes f ::"('a, 'b) bcontfun"
+  fixes f :: "('a, 'b) bcontfun"
   shows "dist (Rep_bcontfun f x) (Rep_bcontfun g x) \<le> dist f g"
 proof -
-  have "Rep_bcontfun f \<in> bcontfun" using Rep_bcontfun .
+  have "Rep_bcontfun f \<in> bcontfun" by (rule Rep_bcontfun)
   from bcontfunE'[OF this] obtain y where y:
     "continuous_on UNIV (Rep_bcontfun f)"
     "\<And>x. dist (Rep_bcontfun f x) undefined \<le> y"
     by auto
-  have "Rep_bcontfun g \<in> bcontfun" using Rep_bcontfun .
+  have "Rep_bcontfun g \<in> bcontfun" by (rule Rep_bcontfun)
   from bcontfunE'[OF this] obtain z where z:
     "continuous_on UNIV (Rep_bcontfun g)"
     "\<And>x. dist (Rep_bcontfun g x) undefined \<le> z"
     by auto
-  show ?thesis unfolding dist_bcontfun_def
+  show ?thesis
+    unfolding dist_bcontfun_def
   proof (intro cSUP_upper bdd_aboveI2)
     fix x
-    have "dist (Rep_bcontfun f x) (Rep_bcontfun g x) \<le> dist (Rep_bcontfun f x) undefined + dist (Rep_bcontfun g x) undefined"
+    have "dist (Rep_bcontfun f x) (Rep_bcontfun g x) \<le>
+      dist (Rep_bcontfun f x) undefined + dist (Rep_bcontfun g x) undefined"
       by (rule dist_triangle2)
-    also have "\<dots> \<le> y + z" using y(2)[of x] z(2)[of x] by (rule add_mono)
+    also have "\<dots> \<le> y + z"
+      using y(2)[of x] z(2)[of x] by (rule add_mono)
     finally show "dist (Rep_bcontfun f x) (Rep_bcontfun g x) \<le> y + z" .
   qed simp
 qed
 
 lemma dist_bound:
-  fixes f ::"('a, 'b) bcontfun"
+  fixes f :: "('a, 'b) bcontfun"
   assumes "\<And>x. dist (Rep_bcontfun f x) (Rep_bcontfun g x) \<le> b"
   shows "dist f g \<le> b"
   using assms by (auto simp: dist_bcontfun_def intro: cSUP_least)
 
 lemma dist_bounded_Abs:
-  fixes f g ::"'a \<Rightarrow> 'b"
+  fixes f g :: "'a \<Rightarrow> 'b"
   assumes "f \<in> bcontfun" "g \<in> bcontfun"
   shows "dist (f x) (g x) \<le> dist (Abs_bcontfun f) (Abs_bcontfun g)"
   by (metis Abs_bcontfun_inverse assms dist_bounded)
@@ -93,39 +94,44 @@
 lemma dist_val_lt_imp_dist_fun_le:
   assumes "\<forall>x. dist (Rep_bcontfun f x) (Rep_bcontfun g x) < e"
   shows "dist f g \<le> e"
-unfolding dist_bcontfun_def
+  unfolding dist_bcontfun_def
 proof (intro cSUP_least)
   fix x
   show "dist (Rep_bcontfun f x) (Rep_bcontfun g x) \<le> e"
     using assms[THEN spec[where x=x]] by (simp add: dist_norm)
-qed (simp)
+qed simp
 
 instance
 proof
-  fix f g::"('a, 'b) bcontfun"
+  fix f g h :: "('a, 'b) bcontfun"
   show "dist f g = 0 \<longleftrightarrow> f = g"
   proof
-    have "\<And>x. dist (Rep_bcontfun f x) (Rep_bcontfun g x) \<le> dist f g" by (rule dist_bounded)
+    have "\<And>x. dist (Rep_bcontfun f x) (Rep_bcontfun g x) \<le> dist f g"
+      by (rule dist_bounded)
     also assume "dist f g = 0"
-    finally  show "f = g" by (auto simp: Rep_bcontfun_inject[symmetric] Abs_bcontfun_inverse)
+    finally show "f = g"
+      by (auto simp: Rep_bcontfun_inject[symmetric] Abs_bcontfun_inverse)
   qed (auto simp: dist_bcontfun_def SUP_def simp del: Sup_image_eq intro!: cSup_eq)
-next
-  fix f g h :: "('a, 'b) bcontfun"
   show "dist f g \<le> dist f h + dist g h"
   proof (subst dist_bcontfun_def, safe intro!: cSUP_least)
     fix x
     have "dist (Rep_bcontfun f x) (Rep_bcontfun g x) \<le>
       dist (Rep_bcontfun f x) (Rep_bcontfun h x) + dist (Rep_bcontfun g x) (Rep_bcontfun h x)"
       by (rule dist_triangle2)
-    also have "dist (Rep_bcontfun f x) (Rep_bcontfun h x) \<le> dist f h" by (rule dist_bounded)
-    also have "dist (Rep_bcontfun g x) (Rep_bcontfun h x) \<le> dist g h" by (rule dist_bounded)
-    finally show "dist (Rep_bcontfun f x) (Rep_bcontfun g x) \<le> dist f h + dist g h" by simp
+    also have "dist (Rep_bcontfun f x) (Rep_bcontfun h x) \<le> dist f h"
+      by (rule dist_bounded)
+    also have "dist (Rep_bcontfun g x) (Rep_bcontfun h x) \<le> dist g h"
+      by (rule dist_bounded)
+    finally show "dist (Rep_bcontfun f x) (Rep_bcontfun g x) \<le> dist f h + dist g h"
+      by simp
   qed
 qed (simp add: open_bcontfun_def)
+
 end
 
 lemma closed_Pi_bcontfun:
-  fixes I::"'a::metric_space set" and X::"'a \<Rightarrow> 'b::complete_space set"
+  fixes I :: "'a::metric_space set"
+    and X :: "'a \<Rightarrow> 'b::complete_space set"
   assumes "\<And>i. i \<in> I \<Longrightarrow> closed (X i)"
   shows "closed (Abs_bcontfun ` (Pi I X \<inter> bcontfun))"
   unfolding closed_sequential_limits
@@ -134,12 +140,13 @@
   assume seq: "\<forall>n. f n \<in> Abs_bcontfun ` (Pi I X \<inter> bcontfun)" and lim: "f ----> l"
   have lim_fun: "\<forall>e>0. \<exists>N. \<forall>n\<ge>N. \<forall>x. dist (Rep_bcontfun (f n) x) (Rep_bcontfun l x) < e"
     using LIMSEQ_imp_Cauchy[OF lim, simplified Cauchy_def] metric_LIMSEQ_D[OF lim]
-    by (intro uniformly_cauchy_imp_uniformly_convergent[where P="%_. True", simplified])
+    by (intro uniformly_cauchy_imp_uniformly_convergent[where P="\<lambda>_. True", simplified])
       (metis dist_fun_lt_imp_dist_val_lt)+
   show "l \<in> Abs_bcontfun ` (Pi I X \<inter> bcontfun)"
   proof (rule, safe)
     fix x assume "x \<in> I"
-    hence "closed (X x)" using assms by simp
+    then have "closed (X x)"
+      using assms by simp
     moreover have "eventually (\<lambda>xa. Rep_bcontfun (f xa) x \<in> X x) sequentially"
     proof (rule always_eventually, safe)
       fix i
@@ -155,30 +162,32 @@
   qed (auto simp: Rep_bcontfun Rep_bcontfun_inverse)
 qed
 
+
 subsection \<open>Complete Space\<close>
 
 instance bcontfun :: (metric_space, complete_space) complete_space
 proof
-  fix f::"nat \<Rightarrow> ('a,'b) bcontfun"
-  assume "Cauchy f" --\<open>Cauchy equals uniform convergence\<close>
+  fix f :: "nat \<Rightarrow> ('a, 'b) bcontfun"
+  assume "Cauchy f"  -- \<open>Cauchy equals uniform convergence\<close>
   then obtain g where limit_function:
     "\<forall>e>0. \<exists>N. \<forall>n\<ge>N. \<forall>x. dist (Rep_bcontfun (f n) x) (g x) < e"
     using uniformly_convergent_eq_cauchy[of "\<lambda>_. True"
       "\<lambda>n. Rep_bcontfun (f n)"]
-    unfolding Cauchy_def by (metis dist_fun_lt_imp_dist_val_lt)
+    unfolding Cauchy_def
+    by (metis dist_fun_lt_imp_dist_val_lt)
 
-  then obtain N where fg_dist: --\<open>for an upper bound on g\<close>
+  then obtain N where fg_dist:  -- \<open>for an upper bound on @{term g}\<close>
     "\<forall>n\<ge>N. \<forall>x. dist (g x) ( Rep_bcontfun (f n) x) < 1"
     by (force simp add: dist_commute)
   from bcontfunE'[OF Rep_bcontfun, of "f N"] obtain b where
-    f_bound: "\<forall>x. dist (Rep_bcontfun (f N) x) undefined \<le> b" by force
-  have "g \<in> bcontfun" --\<open>The limit function is bounded and continuous\<close>
+    f_bound: "\<forall>x. dist (Rep_bcontfun (f N) x) undefined \<le> b"
+    by force
+  have "g \<in> bcontfun"  -- \<open>The limit function is bounded and continuous\<close>
   proof (intro bcontfunI)
     show "continuous_on UNIV g"
       using bcontfunE[OF Rep_bcontfun] limit_function
-      by (intro continuous_uniform_limit[where
-        f="%n. Rep_bcontfun (f n)" and F="sequentially"]) (auto
-        simp add: eventually_sequentially trivial_limit_def dist_norm)
+      by (intro continuous_uniform_limit[where f="\<lambda>n. Rep_bcontfun (f n)" and F="sequentially"])
+        (auto simp add: eventually_sequentially trivial_limit_def dist_norm)
   next
     fix x
     from fg_dist have "dist (g x) (Rep_bcontfun (f N) x) < 1"
@@ -189,9 +198,10 @@
   qed
   show "convergent f"
   proof (rule convergentI, subst lim_sequentially, safe)
-    --\<open>The limit function converges according to its norm\<close>
-    fix e::real
-    assume "e > 0" hence "e/2 > 0" by simp
+    -- \<open>The limit function converges according to its norm\<close>
+    fix e :: real
+    assume "e > 0"
+    then have "e/2 > 0" by simp
     with limit_function[THEN spec, of"e/2"]
     have "\<exists>N. \<forall>n\<ge>N. \<forall>x. dist (Rep_bcontfun (f n) x) (g x) < e/2"
       by simp
@@ -208,7 +218,8 @@
   qed
 qed
 
-subsection\<open>Supremum norm for a normed vector space\<close>
+
+subsection \<open>Supremum norm for a normed vector space\<close>
 
 instantiation bcontfun :: (topological_space, real_normed_vector) real_vector
 begin
@@ -224,8 +235,9 @@
 definition "scaleR r f = Abs_bcontfun (\<lambda>x. r *\<^sub>R Rep_bcontfun f x)"
 
 lemma plus_cont:
-  fixes f g ::"'a \<Rightarrow> 'b"
-  assumes f: "f \<in> bcontfun" and g: "g \<in> bcontfun"
+  fixes f g :: "'a \<Rightarrow> 'b"
+  assumes f: "f \<in> bcontfun"
+    and g: "g \<in> bcontfun"
   shows "(\<lambda>x. f x + g x) \<in> bcontfun"
 proof -
   from bcontfunE'[OF f] obtain y where "continuous_on UNIV f" "\<And>x. dist (f x) undefined \<le> y"
@@ -236,13 +248,14 @@
   ultimately show ?thesis
   proof (intro bcontfunI)
     fix x
-    have "dist (f x + g x) 0 = dist (f x + g x) (0 + 0)" by simp
-    also have "\<dots> \<le> dist (f x) 0 + dist (g x) 0" by (rule dist_triangle_add)
+    have "dist (f x + g x) 0 = dist (f x + g x) (0 + 0)"
+      by simp
+    also have "\<dots> \<le> dist (f x) 0 + dist (g x) 0"
+      by (rule dist_triangle_add)
     also have "\<dots> \<le> dist (Abs_bcontfun f) 0 + dist (Abs_bcontfun g) 0"
       unfolding zero_bcontfun_def using assms
       by (auto intro!: add_mono dist_bounded_Abs const_bcontfun)
-    finally
-    show "dist (f x + g x) 0 <= dist (Abs_bcontfun f) 0 + dist (Abs_bcontfun g) 0" .
+    finally show "dist (f x + g x) 0 \<le> dist (Abs_bcontfun f) 0 + dist (Abs_bcontfun g) 0" .
   qed (simp add: continuous_on_add)
 qed
 
@@ -250,74 +263,80 @@
   by (simp add: plus_bcontfun_def Abs_bcontfun_inverse plus_cont Rep_bcontfun)
 
 lemma uminus_cont:
-  fixes f ::"'a \<Rightarrow> 'b"
+  fixes f :: "'a \<Rightarrow> 'b"
   assumes "f \<in> bcontfun"
   shows "(\<lambda>x. - f x) \<in> bcontfun"
 proof -
-  from bcontfunE[OF assms, of 0] obtain y where "continuous_on UNIV f" "\<And>x. dist (f x) 0 \<le> y"
+  from bcontfunE[OF assms, of 0] obtain y
+    where "continuous_on UNIV f" "\<And>x. dist (f x) 0 \<le> y"
     by auto
-  thus ?thesis
+  then show ?thesis
   proof (intro bcontfunI)
     fix x
     assume "\<And>x. dist (f x) 0 \<le> y"
-    thus "dist (- f x) 0 \<le> y" by (subst dist_minus[symmetric]) simp
+    then show "dist (- f x) 0 \<le> y"
+      by (subst dist_minus[symmetric]) simp
   qed (simp add: continuous_on_minus)
 qed
 
-lemma Rep_bcontfun_uminus[simp]:
-  "Rep_bcontfun (- f) x = - Rep_bcontfun f x"
+lemma Rep_bcontfun_uminus[simp]: "Rep_bcontfun (- f) x = - Rep_bcontfun f x"
   by (simp add: uminus_bcontfun_def Abs_bcontfun_inverse uminus_cont Rep_bcontfun)
 
 lemma minus_cont:
-  fixes f g ::"'a \<Rightarrow> 'b"
-  assumes f: "f \<in> bcontfun" and g: "g \<in> bcontfun"
+  fixes f g :: "'a \<Rightarrow> 'b"
+  assumes f: "f \<in> bcontfun"
+    and g: "g \<in> bcontfun"
   shows "(\<lambda>x. f x - g x) \<in> bcontfun"
-  using plus_cont [of f "- g"] assms by (simp add: uminus_cont fun_Compl_def)
+  using plus_cont [of f "- g"] assms
+  by (simp add: uminus_cont fun_Compl_def)
 
-lemma Rep_bcontfun_minus[simp]:
-  "Rep_bcontfun (f - g) x = Rep_bcontfun f x - Rep_bcontfun g x"
+lemma Rep_bcontfun_minus[simp]: "Rep_bcontfun (f - g) x = Rep_bcontfun f x - Rep_bcontfun g x"
   by (simp add: minus_bcontfun_def Abs_bcontfun_inverse minus_cont Rep_bcontfun)
 
 lemma scaleR_cont:
-  fixes a and f::"'a \<Rightarrow> 'b"
+  fixes a :: real
+    and f :: "'a \<Rightarrow> 'b"
   assumes "f \<in> bcontfun"
   shows " (\<lambda>x. a *\<^sub>R f x) \<in> bcontfun"
 proof -
-  from bcontfunE[OF assms, of 0] obtain y where "continuous_on UNIV f" "\<And>x. dist (f x) 0 \<le> y"
+  from bcontfunE[OF assms, of 0] obtain y
+    where "continuous_on UNIV f" "\<And>x. dist (f x) 0 \<le> y"
     by auto
-  thus ?thesis
+  then show ?thesis
   proof (intro bcontfunI)
-    fix x assume "\<And>x. dist (f x) 0 \<le> y"
+    fix x
+    assume "\<And>x. dist (f x) 0 \<le> y"
     then show "dist (a *\<^sub>R f x) 0 \<le> abs a * y"
       by (metis norm_cmul_rule_thm norm_conv_dist)
   qed (simp add: continuous_intros)
 qed
 
-lemma Rep_bcontfun_scaleR[simp]:
-   "Rep_bcontfun (a *\<^sub>R g) x = a *\<^sub>R Rep_bcontfun g x"
+lemma Rep_bcontfun_scaleR[simp]: "Rep_bcontfun (a *\<^sub>R g) x = a *\<^sub>R Rep_bcontfun g x"
   by (simp add: scaleR_bcontfun_def Abs_bcontfun_inverse scaleR_cont Rep_bcontfun)
 
 instance
-proof
-qed (simp_all add: plus_bcontfun_def zero_bcontfun_def minus_bcontfun_def scaleR_bcontfun_def
-    Abs_bcontfun_inverse Rep_bcontfun_inverse Rep_bcontfun algebra_simps
-    plus_cont const_bcontfun minus_cont scaleR_cont)
+  by default
+    (simp_all add: plus_bcontfun_def zero_bcontfun_def minus_bcontfun_def scaleR_bcontfun_def
+      Abs_bcontfun_inverse Rep_bcontfun_inverse Rep_bcontfun algebra_simps
+      plus_cont const_bcontfun minus_cont scaleR_cont)
+
 end
 
 instantiation bcontfun :: (topological_space, real_normed_vector) real_normed_vector
 begin
 
-definition norm_bcontfun::"('a, 'b) bcontfun \<Rightarrow> real" where
-  "norm_bcontfun f = dist f 0"
+definition norm_bcontfun :: "('a, 'b) bcontfun \<Rightarrow> real"
+  where "norm_bcontfun f = dist f 0"
 
 definition "sgn (f::('a,'b) bcontfun) = f /\<^sub>R norm f"
 
 instance
 proof
-  fix f g::"('a, 'b) bcontfun"
+  fix a :: real
+  fix f g :: "('a, 'b) bcontfun"
   show "dist f g = norm (f - g)"
     by (simp add: norm_bcontfun_def dist_bcontfun_def zero_bcontfun_def
-    Abs_bcontfun_inverse const_bcontfun norm_conv_dist[symmetric] dist_norm)
+      Abs_bcontfun_inverse const_bcontfun norm_conv_dist[symmetric] dist_norm)
   show "norm (f + g) \<le> norm f + norm g"
     unfolding norm_bcontfun_def
   proof (subst dist_bcontfun_def, safe intro!: cSUP_least)
@@ -333,8 +352,6 @@
       by (simp add: Abs_bcontfun_inverse const_bcontfun zero_bcontfun_def)
     finally show "dist (Rep_bcontfun (f + g) x) (Rep_bcontfun 0 x) \<le> dist f 0 + dist g 0" by simp
   qed
-next
-  fix a and f g:: "('a, 'b) bcontfun"
   show "norm (a *\<^sub>R f) = \<bar>a\<bar> * norm f"
   proof -
     have "\<bar>a\<bar> * Sup (range (\<lambda>x. dist (Rep_bcontfun f x) 0)) =
@@ -346,7 +363,7 @@
           const_bcontfun)
     qed (auto intro!: monoI mult_left_mono continuous_intros)
     moreover
-    have "range (\<lambda>x. dist (Rep_bcontfun (a *\<^sub>R f) x) 0) = 
+    have "range (\<lambda>x. dist (Rep_bcontfun (a *\<^sub>R f) x) 0) =
       (\<lambda>x. \<bar>a\<bar> * x) ` (range (\<lambda>x. dist (Rep_bcontfun f x) 0))"
       by (auto simp: norm_conv_dist[symmetric])
     ultimately
@@ -358,38 +375,38 @@
 
 end
 
-lemma bcontfun_normI:
-  "continuous_on UNIV f \<Longrightarrow> (\<And>x. norm (f x) \<le> b) \<Longrightarrow> f \<in> bcontfun"
+lemma bcontfun_normI: "continuous_on UNIV f \<Longrightarrow> (\<And>x. norm (f x) \<le> b) \<Longrightarrow> f \<in> bcontfun"
   unfolding norm_conv_dist
   by (auto intro: bcontfunI)
 
 lemma norm_bounded:
-  fixes f ::"('a::topological_space, 'b::real_normed_vector) bcontfun"
+  fixes f :: "('a::topological_space, 'b::real_normed_vector) bcontfun"
   shows "norm (Rep_bcontfun f x) \<le> norm f"
   using dist_bounded[of f x 0]
   by (simp add: norm_bcontfun_def norm_conv_dist Abs_bcontfun_inverse zero_bcontfun_def
     const_bcontfun)
 
 lemma norm_bound:
-  fixes f ::"('a::topological_space, 'b::real_normed_vector) bcontfun"
+  fixes f :: "('a::topological_space, 'b::real_normed_vector) bcontfun"
   assumes "\<And>x. norm (Rep_bcontfun f x) \<le> b"
   shows "norm f \<le> b"
   using dist_bound[of f 0 b] assms
   by (simp add: norm_bcontfun_def norm_conv_dist Abs_bcontfun_inverse zero_bcontfun_def
     const_bcontfun)
 
-subsection\<open>Continuously Extended Functions\<close>
 
-definition clamp::"'a::euclidean_space \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a" where
+subsection \<open>Continuously Extended Functions\<close>
+
+definition clamp :: "'a::euclidean_space \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a" where
   "clamp a b x = (\<Sum>i\<in>Basis. (if x\<bullet>i < a\<bullet>i then a\<bullet>i else if x\<bullet>i \<le> b\<bullet>i then x\<bullet>i else b\<bullet>i) *\<^sub>R i)"
 
-definition ext_cont::"('a::euclidean_space \<Rightarrow> 'b::real_normed_vector) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> ('a, 'b) bcontfun"
+definition ext_cont :: "('a::euclidean_space \<Rightarrow> 'b::real_normed_vector) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> ('a, 'b) bcontfun"
   where "ext_cont f a b = Abs_bcontfun ((\<lambda>x. f (clamp a b x)))"
 
 lemma ext_cont_def':
   "ext_cont f a b = Abs_bcontfun (\<lambda>x.
     f (\<Sum>i\<in>Basis. (if x\<bullet>i < a\<bullet>i then a\<bullet>i else if x\<bullet>i \<le> b\<bullet>i then x\<bullet>i else b\<bullet>i) *\<^sub>R i))"
-unfolding ext_cont_def clamp_def ..
+  unfolding ext_cont_def clamp_def ..
 
 lemma clamp_in_interval:
   assumes "\<And>i. i \<in> Basis \<Longrightarrow> a \<bullet> i \<le> b \<bullet> i"
@@ -398,35 +415,34 @@
   using box_ne_empty(1)[of a b] assms by (auto simp: cbox_def)
 
 lemma dist_clamps_le_dist_args:
-  fixes x::"'a::euclidean_space"
+  fixes x :: "'a::euclidean_space"
   assumes "\<And>i. i \<in> Basis \<Longrightarrow> a \<bullet> i \<le> b \<bullet> i"
   shows "dist (clamp a b y) (clamp a b x) \<le> dist y x"
 proof -
-    from box_ne_empty(1)[of a b] assms have "(\<forall>i\<in>Basis. a \<bullet> i \<le> b \<bullet> i)"
-      by (simp add: cbox_def)
-    hence "(\<Sum>i\<in>Basis. (dist (clamp a b y \<bullet> i) (clamp a b x \<bullet> i))\<^sup>2)
-        \<le> (\<Sum>i\<in>Basis. (dist (y \<bullet> i) (x \<bullet> i))\<^sup>2)"
-      by (auto intro!: setsum_mono
-        simp add: clamp_def dist_real_def abs_le_square_iff[symmetric])
-    thus ?thesis
-      by (auto intro: real_sqrt_le_mono
-        simp add: euclidean_dist_l2[where y=x] euclidean_dist_l2[where y="clamp a b x"] setL2_def)
+  from box_ne_empty(1)[of a b] assms have "(\<forall>i\<in>Basis. a \<bullet> i \<le> b \<bullet> i)"
+    by (simp add: cbox_def)
+  then have "(\<Sum>i\<in>Basis. (dist (clamp a b y \<bullet> i) (clamp a b x \<bullet> i))\<^sup>2) \<le>
+    (\<Sum>i\<in>Basis. (dist (y \<bullet> i) (x \<bullet> i))\<^sup>2)"
+    by (auto intro!: setsum_mono simp: clamp_def dist_real_def abs_le_square_iff[symmetric])
+  then show ?thesis
+    by (auto intro: real_sqrt_le_mono
+      simp: euclidean_dist_l2[where y=x] euclidean_dist_l2[where y="clamp a b x"] setL2_def)
 qed
 
 lemma clamp_continuous_at:
-  fixes f::"'a::euclidean_space \<Rightarrow> 'b::metric_space"
-  fixes x
+  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::metric_space"
+    and x :: 'a
   assumes "\<And>i. i \<in> Basis \<Longrightarrow> a \<bullet> i \<le> b \<bullet> i"
-  assumes f_cont: "continuous_on (cbox a b) f"
+    and f_cont: "continuous_on (cbox a b) f"
   shows "continuous (at x) (\<lambda>x. f (clamp a b x))"
-unfolding continuous_at_eps_delta
-proof (safe)
-  fix x::'a and e::real
-  assume "0 < e"
-  moreover
-  have "clamp a b x \<in> cbox a b" by (simp add: clamp_in_interval assms)
-  moreover
-  note f_cont[simplified continuous_on_iff]
+  unfolding continuous_at_eps_delta
+proof safe
+  fix x :: 'a
+  fix e :: real
+  assume "e > 0"
+  moreover have "clamp a b x \<in> cbox a b"
+    by (simp add: clamp_in_interval assms)
+  moreover note f_cont[simplified continuous_on_iff]
   ultimately
   obtain d where d: "0 < d"
     "\<And>x'. x' \<in> cbox a b \<Longrightarrow> dist x' (clamp a b x) < d \<Longrightarrow> dist (f x') (f (clamp a b x)) < e"
@@ -437,27 +453,29 @@
 qed
 
 lemma clamp_continuous_on:
-  fixes f::"'a::euclidean_space \<Rightarrow> 'b::metric_space"
+  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::metric_space"
   assumes "\<And>i. i \<in> Basis \<Longrightarrow> a \<bullet> i \<le> b \<bullet> i"
-  assumes f_cont: "continuous_on (cbox a b) f"
+    and f_cont: "continuous_on (cbox a b) f"
   shows "continuous_on UNIV (\<lambda>x. f (clamp a b x))"
   using assms
   by (auto intro: continuous_at_imp_continuous_on clamp_continuous_at)
 
 lemma clamp_bcontfun:
-  fixes f::"'a::euclidean_space \<Rightarrow> 'b::real_normed_vector"
+  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::real_normed_vector"
   assumes "\<And>i. i \<in> Basis \<Longrightarrow> a \<bullet> i \<le> b \<bullet> i"
-  assumes continuous: "continuous_on (cbox a b) f"
+    and continuous: "continuous_on (cbox a b) f"
   shows "(\<lambda>x. f (clamp a b x)) \<in> bcontfun"
 proof -
-  from compact_continuous_image[OF continuous compact_cbox[of a b], THEN compact_imp_bounded]
-  have "bounded (f ` (cbox a b))" .
-  then obtain c where f_bound: "\<forall>x\<in>f ` cbox a b. norm x \<le> c" by (auto simp add: bounded_pos)
+  have "bounded (f ` (cbox a b))"
+    by (rule compact_continuous_image[OF continuous compact_cbox[of a b], THEN compact_imp_bounded])
+  then obtain c where f_bound: "\<forall>x\<in>f ` cbox a b. norm x \<le> c"
+    by (auto simp add: bounded_pos)
   show "(\<lambda>x. f (clamp a b x)) \<in> bcontfun"
   proof (intro bcontfun_normI)
     fix x
-    from clamp_in_interval[OF assms(1), of x] f_bound
-    show "norm (f (clamp a b x)) \<le> c" by (simp add: ext_cont_def)
+    show "norm (f (clamp a b x)) \<le> c"
+      using clamp_in_interval[OF assms(1), of x] f_bound
+      by (simp add: ext_cont_def)
   qed (simp add: clamp_continuous_on assms)
 qed
 
@@ -470,9 +488,9 @@
 declare [[coercion Rep_bcontfun]]
 
 lemma ext_cont_cancel[simp]:
-  fixes x a b::"'a::euclidean_space"
+  fixes x a b :: "'a::euclidean_space"
   assumes x: "x \<in> cbox a b"
-  assumes "continuous_on (cbox a b) f"
+    and "continuous_on (cbox a b) f"
   shows "ext_cont f a b x = f x"
   using assms
   unfolding ext_cont_def
@@ -484,11 +502,11 @@
 
 lemma ext_cont_cong:
   assumes "t0 = s0"
-  assumes "t1 = s1"
-  assumes "\<And>t. t \<in> (cbox t0 t1) \<Longrightarrow> f t = g t"
-  assumes "continuous_on (cbox t0 t1) f"
-  assumes "continuous_on (cbox s0 s1) g"
-  assumes ord: "\<And>i. i \<in> Basis \<Longrightarrow> t0 \<bullet> i \<le> t1 \<bullet> i"
+    and "t1 = s1"
+    and "\<And>t. t \<in> (cbox t0 t1) \<Longrightarrow> f t = g t"
+    and "continuous_on (cbox t0 t1) f"
+    and "continuous_on (cbox s0 s1) g"
+    and ord: "\<And>i. i \<in> Basis \<Longrightarrow> t0 \<bullet> i \<le> t1 \<bullet> i"
   shows "ext_cont f t0 t1 = ext_cont g s0 s1"
   unfolding assms ext_cont_def
   using assms clamp_in_interval[OF ord]
diff -r 884f54e01427 -r 92d9557fb78c src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy
--- a/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy	Wed Jun 10 19:10:20 2015 +0200
+++ b/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy	Wed Jun 10 20:15:58 2015 +0200
@@ -189,11 +189,11 @@
   show "finite ?F"
     using \<open>finite simplices\<close> unfolding F_eq by auto
 
-  { fix f assume "f \<in> ?F" "bnd f" then show "card {s \<in> simplices. face f s} = 1"
-      using bnd by auto }
+  show "card {s \<in> simplices. face f s} = 1" if "f \<in> ?F" "bnd f" for f
+    using bnd prems by auto
 
-  { fix f assume "f \<in> ?F" "\<not> bnd f" then show "card {s \<in> simplices. face f s} = 2"
-      using nbnd by auto }
+  show "card {s \<in> simplices. face f s} = 2" if "f \<in> ?F" "\<not> bnd f" for f
+    using nbnd prems by auto
 
   show "odd (card {f \<in> {f. \<exists>s\<in>simplices. face f s}. rl ` f = {..n} \<and> bnd f})"
     using odd_card by simp