src/HOL/Real/HahnBanach/HahnBanach.thy

     -- {* and @{text f} a linear form on @{text F} such that @{text f} is bounded by @{text p}, *}
     -- {* then @{text f} can be extended to a linear form @{text h} on @{text E} in a norm-preserving way. \skp *}
 proof -
   def M \<equiv> "norm_pres_extensions E p F f"
   hence M: "M = \<dots>" by (simp only:)
-  have E: "vectorspace E" .
-  have F: "vectorspace F" ..
+  note E = `vectorspace E`
+  then have F: "vectorspace F" ..
+  note FE = `F \<unlhd> E`
   {
     fix c assume cM: "c \<in> chain M" and ex: "\<exists>x. x \<in> c"
     have "\<Union>c \<in> M"
       -- {* Show that every non-empty chain @{text c} of @{text M} has an upper bound in @{text M}: *}
       -- {* @{text "\<Union>c"} is greater than any element of the chain @{text c}, so it suffices to show @{text "\<Union>c \<in> M"}. *}

         fix x y z assume "(x, y) \<in> \<Union>c" and "(x, z) \<in> \<Union>c"
         with M_def cM show "z = y" by (rule sup_definite)
       qed
       moreover from M cM a have "linearform ?H ?h"
         by (rule sup_lf)
-      moreover from a M cM ex have "?H \<unlhd> E"
+      moreover from a M cM ex FE E have "?H \<unlhd> E"
         by (rule sup_subE)
-      moreover from a M cM ex have "F \<unlhd> ?H"
+      moreover from a M cM ex FE have "F \<unlhd> ?H"
         by (rule sup_supF)
       moreover from a M cM ex have "graph F f \<subseteq> graph ?H ?h"
         by (rule sup_ext)
       moreover from a M cM have "\<forall>x \<in> ?H. ?h x \<le> p x"
         by (rule sup_norm_pres)

   -- {* With Zorn's Lemma we can conclude that there is a maximal element in @{text M}. \skp *}
   proof (rule Zorn's_Lemma)
       -- {* We show that @{text M} is non-empty: *}
     show "graph F f \<in> M"
     proof (unfold M_def, rule norm_pres_extensionI2)
-      show "linearform F f" .
-      show "F \<unlhd> E" .
+      show "linearform F f" by fact
+      show "F \<unlhd> E" by fact
       from F show "F \<unlhd> F" by (rule vectorspace.subspace_refl)
       show "graph F f \<subseteq> graph F f" ..
-      show "\<forall>x\<in>F. f x \<le> p x" .
-    qed
-  qed
-  then obtain g where gM: "g \<in> M" and "\<forall>x \<in> M. g \<subseteq> x \<longrightarrow> g = x"
+      show "\<forall>x\<in>F. f x \<le> p x" by fact
+    qed
+  qed
+  then obtain g where gM: "g \<in> M" and gx: "\<forall>x \<in> M. g \<subseteq> x \<longrightarrow> g = x"
     by blast
   from gM [unfolded M_def] obtain H h where
       g_rep: "g = graph H h"
     and linearform: "linearform H h"
     and HE: "H \<unlhd> E" and FH: "F \<unlhd> H"
     and graphs: "graph F f \<subseteq> graph H h"
     and hp: "\<forall>x \<in> H. h x \<le> p x" ..
       -- {* @{text g} is a norm-preserving extension of @{text f}, in other words: *}
       -- {* @{text g} is the graph of some linear form @{text h} defined on a subspace @{text H} of @{text E}, *}
       -- {* and @{text h} is an extension of @{text f} that is again bounded by @{text p}. \skp *}
-  from HE have H: "vectorspace H"
+  from HE E have H: "vectorspace H"
     by (rule subspace.vectorspace)
 
   have HE_eq: "H = E"
     -- {* We show that @{text h} is defined on whole @{text E} by classical contradiction. \skp *}
   proof (rule classical)

       proof
         show "x' \<noteq> 0"
         proof
           assume "x' = 0"
           with H have "x' \<in> H" by (simp only: vectorspace.zero)
-          then show False by contradiction
+          with `x' \<notin> H` show False by contradiction
         qed
       qed
 
       def H' \<equiv> "H + lin x'"
         -- {* Define @{text H'} as the direct sum of @{text H} and the linear closure of @{text x'}. \skp *}
       have HH': "H \<unlhd> H'"
       proof (unfold H'_def)
-        have "vectorspace (lin x')" ..
+        from x'E have "vectorspace (lin x')" ..
         with H show "H \<unlhd> H + lin x'" ..
       qed
 
       obtain xi where
-        "\<forall>y \<in> H. - p (y + x') - h y \<le> xi
+        xi: "\<forall>y \<in> H. - p (y + x') - h y \<le> xi
           \<and> xi \<le> p (y + x') - h y"
         -- {* Pick a real number @{text \<xi>} that fulfills certain inequations; this will *}
         -- {* be used to establish that @{text h'} is a norm-preserving extension of @{text h}.
            \label{ex-xi-use}\skp *}
       proof -

           also from x'E uE vE E have "p \<dots> \<le> p (v + x') + p (u + x')"
             by (simp add: diff_subadditive)
           finally have "h v - h u \<le> p (v + x') + p (u + x')" .
           then show "- p (u + x') - h u \<le> p (v + x') - h v" by simp
         qed
-        then show ?thesis ..
+        then show thesis by (blast intro: that)
       qed
 
       def h' \<equiv> "\<lambda>x. let (y, a) =
           SOME (y, a). x = y + a \<cdot> x' \<and> y \<in> H in h y + a * xi"
         -- {* Define the extension @{text h'} of @{text h} to @{text H'} using @{text \<xi>}. \skp *}

         show "g \<subseteq> graph H' h'"
         proof -
           have  "graph H h \<subseteq> graph H' h'"
           proof (rule graph_extI)
             fix t assume t: "t \<in> H"
-            have "(SOME (y, a). t = y + a \<cdot> x' \<and> y \<in> H) = (t, 0)"
-              by (rule decomp_H'_H)
+            from E HE t have "(SOME (y, a). t = y + a \<cdot> x' \<and> y \<in> H) = (t, 0)"
+	      using `x' \<notin> H` `x' \<in> E` `x' \<noteq> 0` by (rule decomp_H'_H)
             with h'_def show "h t = h' t" by (simp add: Let_def)
           next
             from HH' show "H \<subseteq> H'" ..
           qed
           with g_rep show ?thesis by (simp only:)

               from x'E show "x' = 0 + x'" by simp
             qed
             hence "(x', h' x') \<in> graph H' h'" ..
             with eq have "(x', h' x') \<in> graph H h" by (simp only:)
             hence "x' \<in> H" ..
-            thus False by contradiction
+            with `x' \<notin> H` show False by contradiction
           qed
           with g_rep show ?thesis by simp
         qed
       qed
       moreover have "graph H' h' \<in> M"
         -- {* and @{text h'} is norm-preserving. \skp *}
       proof (unfold M_def)
         show "graph H' h' \<in> norm_pres_extensions E p F f"
         proof (rule norm_pres_extensionI2)
-          show "linearform H' h'" by (rule h'_lf)
+          show "linearform H' h'"
+	    using h'_def H'_def HE linearform `x' \<notin> H` `x' \<in> E` `x' \<noteq> 0` E
+	    by (rule h'_lf)
           show "H' \<unlhd> E"
-          proof (unfold H'_def, rule)
-            show "H \<unlhd> E" .
-            show "vectorspace E" .
+	  unfolding H'_def
+          proof
+            show "H \<unlhd> E" by fact
+            show "vectorspace E" by fact
             from x'E show "lin x' \<unlhd> E" ..
           qed
-          have "F \<unlhd> H" .
-          from H this HH' show FH': "F \<unlhd> H'"
+          from H `F \<unlhd> H` HH' show FH': "F \<unlhd> H'"
             by (rule vectorspace.subspace_trans)
           show "graph F f \<subseteq> graph H' h'"
           proof (rule graph_extI)
             fix x assume x: "x \<in> F"
             with graphs have "f x = h x" ..
             also have "\<dots> = h x + 0 * xi" by simp
             also have "\<dots> = (let (y, a) = (x, 0) in h y + a * xi)"
               by (simp add: Let_def)
             also have "(x, 0) =
                 (SOME (y, a). x = y + a \<cdot> x' \<and> y \<in> H)"
+	    using E HE
             proof (rule decomp_H'_H [symmetric])
               from FH x show "x \<in> H" ..
               from x' show "x' \<noteq> 0" .
+	      show "x' \<notin> H" by fact
+	      show "x' \<in> E" by fact
             qed
             also have
               "(let (y, a) = (SOME (y, a). x = y + a \<cdot> x' \<and> y \<in> H)
               in h y + a * xi) = h' x" by (simp only: h'_def)
             finally show "f x = h' x" .
           next
             from FH' show "F \<subseteq> H'" ..
           qed
-          show "\<forall>x \<in> H'. h' x \<le> p x" by (rule h'_norm_pres)
+          show "\<forall>x \<in> H'. h' x \<le> p x"
+	    using h'_def H'_def `x' \<notin> H` `x' \<in> E` `x' \<noteq> 0` E HE
+	      `seminorm E p` linearform and hp xi
+	    by (rule h'_norm_pres)
         qed
       qed
       ultimately show ?thesis ..
     qed
     hence "\<not> (\<forall>x \<in> M. g \<subseteq> x \<longrightarrow> g = x)" by simp
       -- {* So the graph @{text g} of @{text h} cannot be maximal. Contradiction! \skp *}
-    then show "H = E" by contradiction
+    with gx show "H = E" by contradiction
   qed
 
   from HE_eq and linearform have "linearform E h"
     by (simp only:)
   moreover have "\<forall>x \<in> F. h x = f x"

   assumes fp: "\<forall>x \<in> F. \<bar>f x\<bar> \<le> p x"
   shows "\<exists>g. linearform E g
     \<and> (\<forall>x \<in> F. g x = f x)
     \<and> (\<forall>x \<in> E. \<bar>g x\<bar> \<le> p x)"
 proof -
-  have "\<exists>g. linearform E g \<and> (\<forall>x \<in> F. g x = f x)
-    \<and> (\<forall>x \<in> E. g x \<le> p x)"
+  note E = `vectorspace E`
+  note FE = `subspace F E`
+  note sn = `seminorm E p`
+  note lf = `linearform F f`
+  have "\<exists>g. linearform E g \<and> (\<forall>x \<in> F. g x = f x) \<and> (\<forall>x \<in> E. g x \<le> p x)"
+  using E FE sn lf
   proof (rule HahnBanach)
     show "\<forall>x \<in> F. f x \<le> p x"
-      by (rule abs_ineq_iff [THEN iffD1])
-  qed
-  then obtain g where * : "linearform E g"  "\<forall>x \<in> F. g x = f x"
-      and "\<forall>x \<in> E. g x \<le> p x" by blast
+      using FE E sn lf and fp by (rule abs_ineq_iff [THEN iffD1])
+  qed
+  then obtain g where lg: "linearform E g" and *: "\<forall>x \<in> F. g x = f x"
+      and **: "\<forall>x \<in> E. g x \<le> p x" by blast
   have "\<forall>x \<in> E. \<bar>g x\<bar> \<le> p x"
+  using _ E sn lg **
   proof (rule abs_ineq_iff [THEN iffD2])
     show "E \<unlhd> E" ..
   qed
-  with * show ?thesis by blast
+  with lg * show ?thesis by blast
 qed
 
 
 subsection {* The Hahn-Banach Theorem for normed spaces *}
 

      \<and> (\<forall>x \<in> F. g x = f x)
      \<and> \<parallel>g\<parallel>\<hyphen>E = \<parallel>f\<parallel>\<hyphen>F"
 proof -
   have E: "vectorspace E" by unfold_locales
   have E_norm: "normed_vectorspace E norm" by rule unfold_locales
-  have FE: "F \<unlhd> E" .
+  note FE = `F \<unlhd> E`
   have F: "vectorspace F" by rule unfold_locales
-  have linearform: "linearform F f" .
+  note linearform = `linearform F f`
   have F_norm: "normed_vectorspace F norm"
-    by (rule subspace_normed_vs)
+    using FE E_norm by (rule subspace_normed_vs)
   have ge_zero: "0 \<le> \<parallel>f\<parallel>\<hyphen>F"
     by (rule normed_vectorspace.fn_norm_ge_zero
-      [OF F_norm (* continuous.intro*), folded B_def fn_norm_def])
+      [OF F_norm `continuous F norm f`, folded B_def fn_norm_def])
   txt {* We define a function @{text p} on @{text E} as follows:
     @{text "p x = \<parallel>f\<parallel> \<cdot> \<parallel>x\<parallel>"} *}
   def p \<equiv> "\<lambda>x. \<parallel>f\<parallel>\<hyphen>F * \<parallel>x\<parallel>"
 
   txt {* @{text p} is a seminorm on @{text E}: *}

   txt {* @{text f} is bounded by @{text p}. *}
 
   have "\<forall>x \<in> F. \<bar>f x\<bar> \<le> p x"
   proof
     fix x assume "x \<in> F"
+    from this and `continuous F norm f`
     show "\<bar>f x\<bar> \<le> p x"
       by (unfold p_def) (rule normed_vectorspace.fn_norm_le_cong
         [OF F_norm, folded B_def fn_norm_def])
   qed
 

     show "\<parallel>f\<parallel>\<hyphen>F \<le> \<parallel>g\<parallel>\<hyphen>E"
     proof (rule normed_vectorspace.fn_norm_least [OF F_norm, folded B_def fn_norm_def])
       show "\<forall>x \<in> F. \<bar>f x\<bar> \<le> \<parallel>g\<parallel>\<hyphen>E * \<parallel>x\<parallel>"
       proof
 	fix x assume x: "x \<in> F"
-	from a have "g x = f x" ..
+	from a x have "g x = f x" ..
 	hence "\<bar>f x\<bar> = \<bar>g x\<bar>" by (simp only:)
 	also from g_cont
 	have "\<dots> \<le> \<parallel>g\<parallel>\<hyphen>E * \<parallel>x\<parallel>"
 	proof (rule fn_norm_le_cong [of g, folded B_def fn_norm_def])
 	  from FE x show "x \<in> E" ..

       qed
       show "0 \<le> \<parallel>g\<parallel>\<hyphen>E"
 	using g_cont
 	by (rule fn_norm_ge_zero [of g, folded B_def fn_norm_def])
     next
-      show "continuous F norm f" .
+      show "continuous F norm f" by fact
     qed
   qed
   with linearformE a g_cont show ?thesis by blast
 qed