src/HOL/Real/HahnBanach/HahnBanachSupLemmas.thy

   This section contains some lemmas that will be used in the proof of
   the Hahn-Banach Theorem.  In this section the following context is
   presumed.  Let @{text E} be a real vector space with a seminorm
   @{text p} on @{text E}.  @{text F} is a subspace of @{text E} and
   @{text f} a linear form on @{text F}. We consider a chain @{text c}
-  of norm-preserving extensions of @{text f}, such that
-  @{text "\<Union>c = graph H h"}.  We will show some properties about the
-  limit function @{text h}, i.e.\ the supremum of the chain @{text c}.
-*}
-
-text {*
-  Let @{text c} be a chain of norm-preserving extensions of the
-  function @{text f} and let @{text "graph H h"} be the supremum of
-  @{text c}.  Every element in @{text H} is member of one of the
+  of norm-preserving extensions of @{text f}, such that @{text "\<Union>c =
+  graph H h"}.  We will show some properties about the limit function
+  @{text h}, i.e.\ the supremum of the chain @{text c}.
+
+  \medskip Let @{text c} be a chain of norm-preserving extensions of
+  the function @{text f} and let @{text "graph H h"} be the supremum
+  of @{text c}.  Every element in @{text H} is member of one of the
   elements of the chain.
 *}
 
 lemma some_H'h't:
-  "M = norm_pres_extensions E p F f \<Longrightarrow> c \<in> chain M \<Longrightarrow>
-  graph H h = \<Union>c \<Longrightarrow> x \<in> H
-   \<Longrightarrow> \<exists>H' h'. graph H' h' \<in> c \<and> (x, h x) \<in> graph H' h'
-       \<and> is_linearform H' h' \<and> is_subspace H' E
-       \<and> is_subspace F H' \<and> graph F f \<subseteq> graph H' h'
-       \<and> (\<forall>x \<in> H'. h' x \<le> p x)"
+  assumes M: "M = norm_pres_extensions E p F f"
+    and cM: "c \<in> chain M"
+    and u: "graph H h = \<Union>c"
+    and x: "x \<in> H"
+  shows "\<exists>H' h'. graph H' h' \<in> c
+    \<and> (x, h x) \<in> graph H' h'
+    \<and> linearform H' h' \<and> H' \<unlhd> E
+    \<and> F \<unlhd> H' \<and> graph F f \<subseteq> graph H' h'
+    \<and> (\<forall>x \<in> H'. h' x \<le> p x)"
 proof -
-  assume m: "M = norm_pres_extensions E p F f" and "c \<in> chain M"
-     and u: "graph H h = \<Union>c"  "x \<in> H"
-
-  have h: "(x, h x) \<in> graph H h" ..
-  with u have "(x, h x) \<in> \<Union>c" by simp
-  hence ex1: "\<exists>g \<in> c. (x, h x) \<in> g"
-    by (simp only: Union_iff)
-  thus ?thesis
-  proof (elim bexE)
-    fix g assume g: "g \<in> c"  "(x, h x) \<in> g"
-    have "c \<subseteq> M" by (rule chainD2)
-    hence "g \<in> M" ..
-    hence "g \<in> norm_pres_extensions E p F f" by (simp only: m)
-    hence "\<exists>H' h'. graph H' h' = g
-                  \<and> is_linearform H' h'
-                  \<and> is_subspace H' E
-                  \<and> is_subspace F H'
-                  \<and> graph F f \<subseteq> graph H' h'
-                  \<and> (\<forall>x \<in> H'. h' x \<le> p x)"
-      by (rule norm_pres_extension_D)
-    thus ?thesis
-    proof (elim exE conjE)
-      fix H' h'
-      assume "graph H' h' = g"  "is_linearform H' h'"
-        "is_subspace H' E"  "is_subspace F H'"
-        "graph F f \<subseteq> graph H' h'"  "\<forall>x \<in> H'. h' x \<le> p x"
-      show ?thesis
-      proof (intro exI conjI)
-        show "graph H' h' \<in> c" by (simp!)
-        show "(x, h x) \<in> graph H' h'" by (simp!)
-      qed
-    qed
-  qed
-qed
-
+  from x have "(x, h x) \<in> graph H h" ..
+  also from u have "\<dots> = \<Union>c" .
+  finally obtain g where gc: "g \<in> c" and gh: "(x, h x) \<in> g" by blast
+
+  from cM have "c \<subseteq> M" ..
+  with gc have "g \<in> M" ..
+  also from M have "\<dots> = norm_pres_extensions E p F f" .
+  finally obtain H' and h' where g: "g = graph H' h'"
+    and * : "linearform H' h'"  "H' \<unlhd> E"  "F \<unlhd> H'"
+      "graph F f \<subseteq> graph H' h'"  "\<forall>x \<in> H'. h' x \<le> p x" ..
+
+  from gc and g have "graph H' h' \<in> c" by (simp only:)
+  moreover from gh and g have "(x, h x) \<in> graph H' h'" by (simp only:)
+  ultimately show ?thesis using * by blast
+qed
 
 text {*
   \medskip Let @{text c} be a chain of norm-preserving extensions of
   the function @{text f} and let @{text "graph H h"} be the supremum
   of @{text c}.  Every element in the domain @{text H} of the supremum
   function is member of the domain @{text H'} of some function @{text
   h'}, such that @{text h} extends @{text h'}.
 *}
 
 lemma some_H'h':
-  "M = norm_pres_extensions E p F f \<Longrightarrow> c \<in> chain M \<Longrightarrow>
-  graph H h = \<Union>c \<Longrightarrow> x \<in> H
-  \<Longrightarrow> \<exists>H' h'. x \<in> H' \<and> graph H' h' \<subseteq> graph H h
-      \<and> is_linearform H' h' \<and> is_subspace H' E \<and> is_subspace F H'
-      \<and> graph F f \<subseteq> graph H' h' \<and> (\<forall>x \<in> H'. h' x \<le> p x)"
+  assumes M: "M = norm_pres_extensions E p F f"
+    and cM: "c \<in> chain M"
+    and u: "graph H h = \<Union>c"
+    and x: "x \<in> H"
+  shows "\<exists>H' h'. x \<in> H' \<and> graph H' h' \<subseteq> graph H h
+    \<and> linearform H' h' \<and> H' \<unlhd> E \<and> F \<unlhd> H'
+    \<and> graph F f \<subseteq> graph H' h' \<and> (\<forall>x \<in> H'. h' x \<le> p x)"
 proof -
-  assume "M = norm_pres_extensions E p F f" and cM: "c \<in> chain M"
-     and u: "graph H h = \<Union>c"  "x \<in> H"
-
-  have "\<exists>H' h'. graph H' h' \<in> c \<and> (x, h x) \<in> graph H' h'
-       \<and> is_linearform H' h' \<and> is_subspace H' E
-       \<and> is_subspace F H' \<and> graph F f \<subseteq> graph H' h'
-       \<and> (\<forall>x \<in> H'. h' x \<le> p x)"
-    by (rule some_H'h't)
-  thus ?thesis
-  proof (elim exE conjE)
-    fix H' h' assume "(x, h x) \<in> graph H' h'"  "graph H' h' \<in> c"
-      "is_linearform H' h'"  "is_subspace H' E"  "is_subspace F H'"
+  from M cM u x obtain H' h' where
+      x_hx: "(x, h x) \<in> graph H' h'"
+    and c: "graph H' h' \<in> c"
+    and * : "linearform H' h'"  "H' \<unlhd> E"  "F \<unlhd> H'"
       "graph F f \<subseteq> graph H' h'"  "\<forall>x \<in> H'. h' x \<le> p x"
-    show ?thesis
-    proof (intro exI conjI)
-      show "x \<in> H'" by (rule graphD1)
-      from cM u show "graph H' h' \<subseteq> graph H h"
-        by (simp! only: chain_ball_Union_upper)
-    qed
-  qed
-qed
-
+    by (rule some_H'h't [elim_format]) blast
+  from x_hx have "x \<in> H'" ..
+  moreover from cM u c have "graph H' h' \<subseteq> graph H h"
+    by (simp only: chain_ball_Union_upper)
+  ultimately show ?thesis using * by blast
+qed
 
 text {*
   \medskip Any two elements @{text x} and @{text y} in the domain
   @{text H} of the supremum function @{text h} are both in the domain
   @{text H'} of some function @{text h'}, such that @{text h} extends
   @{text h'}.
 *}
 
 lemma some_H'h'2:
-  "M = norm_pres_extensions E p F f \<Longrightarrow> c \<in> chain M \<Longrightarrow>
-  graph H h = \<Union>c \<Longrightarrow> x \<in> H \<Longrightarrow> y \<in> H
-  \<Longrightarrow> \<exists>H' h'. x \<in> H' \<and> y \<in> H' \<and> graph H' h' \<subseteq> graph H h
-      \<and> is_linearform H' h' \<and> is_subspace H' E \<and> is_subspace F H'
-      \<and> graph F f \<subseteq> graph H' h' \<and> (\<forall>x \<in> H'. h' x \<le> p x)"
+  assumes M: "M = norm_pres_extensions E p F f"
+    and cM: "c \<in> chain M"
+    and u: "graph H h = \<Union>c"
+    and x: "x \<in> H"
+    and y: "y \<in> H"
+  shows "\<exists>H' h'. x \<in> H' \<and> y \<in> H'
+    \<and> graph H' h' \<subseteq> graph H h
+    \<and> linearform H' h' \<and> H' \<unlhd> E \<and> F \<unlhd> H'
+    \<and> graph F f \<subseteq> graph H' h' \<and> (\<forall>x \<in> H'. h' x \<le> p x)"
 proof -
-  assume "M = norm_pres_extensions E p F f"  "c \<in> chain M"
-         "graph H h = \<Union>c"  "x \<in> H"  "y \<in> H"
-
-  txt {*
-    @{text x} is in the domain @{text H'} of some function @{text h'},
-    such that @{text h} extends @{text h'}. *}
-
-  have e1: "\<exists>H' h'. graph H' h' \<in> c \<and> (x, h x) \<in> graph H' h'
-       \<and> is_linearform H' h' \<and> is_subspace H' E
-       \<and> is_subspace F H' \<and> graph F f \<subseteq> graph H' h'
-       \<and> (\<forall>x \<in> H'. h' x \<le> p x)"
-    by (rule some_H'h't)
-
   txt {* @{text y} is in the domain @{text H''} of some function @{text h''},
   such that @{text h} extends @{text h''}. *}
 
-  have e2: "\<exists>H'' h''. graph H'' h'' \<in> c \<and> (y, h y) \<in> graph H'' h''
-       \<and> is_linearform H'' h'' \<and> is_subspace H'' E
-       \<and> is_subspace F H'' \<and> graph F f \<subseteq> graph H'' h''
-       \<and> (\<forall>x \<in> H''. h'' x \<le> p x)"
-    by (rule some_H'h't)
-
-  from e1 e2 show ?thesis
-  proof (elim exE conjE)
-    fix H' h' assume "(y, h y) \<in> graph H' h'"  "graph H' h' \<in> c"
-      "is_linearform H' h'"  "is_subspace H' E"  "is_subspace F H'"
+  from M cM u and y obtain H' h' where
+      y_hy: "(y, h y) \<in> graph H' h'"
+    and c': "graph H' h' \<in> c"
+    and * :
+      "linearform H' h'"  "H' \<unlhd> E"  "F \<unlhd> H'"
       "graph F f \<subseteq> graph H' h'"  "\<forall>x \<in> H'. h' x \<le> p x"
-
-    fix H'' h'' assume "(x, h x) \<in> graph H'' h''"  "graph H'' h'' \<in> c"
-      "is_linearform H'' h''"  "is_subspace H'' E"  "is_subspace F H''"
+    by (rule some_H'h't [elim_format]) blast
+
+  txt {* @{text x} is in the domain @{text H'} of some function @{text h'},
+    such that @{text h} extends @{text h'}. *}
+
+  from M cM u and x obtain H'' h'' where
+      x_hx: "(x, h x) \<in> graph H'' h''"
+    and c'': "graph H'' h'' \<in> c"
+    and ** :
+      "linearform H'' h''"  "H'' \<unlhd> E"  "F \<unlhd> H''"
       "graph F f \<subseteq> graph H'' h''"  "\<forall>x \<in> H''. h'' x \<le> p x"
-
-   txt {* Since both @{text h'} and @{text h''} are elements of the chain,
-   @{text h''} is an extension of @{text h'} or vice versa. Thus both
-   @{text x} and @{text y} are contained in the greater one. \label{cases1}*}
-
-    have "graph H'' h'' \<subseteq> graph H' h' \<or> graph H' h' \<subseteq> graph H'' h''"
-      (is "?case1 \<or> ?case2")
-      by (rule chainD)
-    thus ?thesis
-    proof
-      assume ?case1
-      show ?thesis
-      proof (intro exI conjI)
-        have "(x, h x) \<in> graph H'' h''" .
-        also have "... \<subseteq> graph H' h'" .
-        finally have xh:"(x, h x) \<in> graph H' h'" .
-        thus x: "x \<in> H'" ..
-        show y: "y \<in> H'" ..
-        show "graph H' h' \<subseteq> graph H h"
-          by (simp! only: chain_ball_Union_upper)
-      qed
-    next
-      assume ?case2
-      show ?thesis
-      proof (intro exI conjI)
-        show x: "x \<in> H''" ..
-        have "(y, h y) \<in> graph H' h'" by (simp!)
-        also have "... \<subseteq> graph H'' h''" .
-        finally have yh: "(y, h y) \<in> graph H'' h''" .
-        thus y: "y \<in> H''" ..
-        show "graph H'' h'' \<subseteq> graph H h"
-          by (simp! only: chain_ball_Union_upper)
-      qed
-    qed
-  qed
-qed
-
-
+    by (rule some_H'h't [elim_format]) blast
+
+  txt {* Since both @{text h'} and @{text h''} are elements of the chain,
+    @{text h''} is an extension of @{text h'} or vice versa. Thus both
+    @{text x} and @{text y} are contained in the greater
+    one. \label{cases1}*}
+
+  from cM have "graph H'' h'' \<subseteq> graph H' h' \<or> graph H' h' \<subseteq> graph H'' h''"
+    (is "?case1 \<or> ?case2") ..
+  then show ?thesis
+  proof
+    assume ?case1
+    have "(x, h x) \<in> graph H'' h''" .
+    also have "... \<subseteq> graph H' h'" .
+    finally have xh:"(x, h x) \<in> graph H' h'" .
+    then have "x \<in> H'" ..
+    moreover from y_hy have "y \<in> H'" ..
+    moreover from cM u and c' have "graph H' h' \<subseteq> graph H h"
+      by (simp only: chain_ball_Union_upper)
+    ultimately show ?thesis using * by blast
+  next
+    assume ?case2
+    from x_hx have "x \<in> H''" ..
+    moreover {
+      from y_hy have "(y, h y) \<in> graph H' h'" .
+      also have "\<dots> \<subseteq> graph H'' h''" .
+      finally have "(y, h y) \<in> graph H'' h''" .
+    } then have "y \<in> H''" ..
+    moreover from cM u and c'' have "graph H'' h'' \<subseteq> graph H h"
+      by (simp only: chain_ball_Union_upper)
+    ultimately show ?thesis using ** by blast
+  qed
+qed
 
 text {*
   \medskip The relation induced by the graph of the supremum of a
-  chain @{text c} is definite, i.~e.~t is the graph of a function. *}
+  chain @{text c} is definite, i.~e.~t is the graph of a function.
+*}
 
 lemma sup_definite:
-  "M \<equiv> norm_pres_extensions E p F f \<Longrightarrow> c \<in> chain M \<Longrightarrow>
-  (x, y) \<in> \<Union>c \<Longrightarrow> (x, z) \<in> \<Union>c \<Longrightarrow> z = y"
+  assumes M_def: "M \<equiv> norm_pres_extensions E p F f"
+    and cM: "c \<in> chain M"
+    and xy: "(x, y) \<in> \<Union>c"
+    and xz: "(x, z) \<in> \<Union>c"
+  shows "z = y"
 proof -
-  assume "c \<in> chain M"  "M \<equiv> norm_pres_extensions E p F f"
-    "(x, y) \<in> \<Union>c"  "(x, z) \<in> \<Union>c"
-  thus ?thesis
-  proof (elim UnionE chainE2)
-
-    txt {* Since both @{text "(x, y) \<in> \<Union>c"} and @{text "(x, z) \<in> \<Union>c"}
-    they are members of some graphs @{text "G\<^sub>1"} and @{text
-    "G\<^sub>2"}, resp., such that both @{text "G\<^sub>1"} and @{text
-    "G\<^sub>2"} are members of @{text c}.*}
-
-    fix G1 G2 assume
-      "(x, y) \<in> G1"  "G1 \<in> c"  "(x, z) \<in> G2"  "G2 \<in> c"  "c \<subseteq> M"
-
-    have "G1 \<in> M" ..
-    hence e1: "\<exists>H1 h1. graph H1 h1 = G1"
-      by (blast! dest: norm_pres_extension_D)
-    have "G2 \<in> M" ..
-    hence e2: "\<exists>H2 h2. graph H2 h2 = G2"
-      by (blast! dest: norm_pres_extension_D)
-    from e1 e2 show ?thesis
-    proof (elim exE)
-      fix H1 h1 H2 h2
-      assume "graph H1 h1 = G1"  "graph H2 h2 = G2"
-
-      txt {* @{text "G\<^sub>1"} is contained in @{text "G\<^sub>2"}
-      or vice versa, since both @{text "G\<^sub>1"} and @{text
-      "G\<^sub>2"} are members of @{text c}. \label{cases2}*}
-
-      have "G1 \<subseteq> G2 \<or> G2 \<subseteq> G1" (is "?case1 \<or> ?case2") ..
-      thus ?thesis
-      proof
-        assume ?case1
-        have "(x, y) \<in> graph H2 h2" by (blast!)
-        hence "y = h2 x" ..
-        also have "(x, z) \<in> graph H2 h2" by (simp!)
-        hence "z = h2 x" ..
-        finally show ?thesis .
-      next
-        assume ?case2
-        have "(x, y) \<in> graph H1 h1" by (simp!)
-        hence "y = h1 x" ..
-        also have "(x, z) \<in> graph H1 h1" by (blast!)
-        hence "z = h1 x" ..
-        finally show ?thesis .
-      qed
-    qed
+  from cM have c: "c \<subseteq> M" ..
+  from xy obtain G1 where xy': "(x, y) \<in> G1" and G1: "G1 \<in> c" ..
+  from xz obtain G2 where xz': "(x, z) \<in> G2" and G2: "G2 \<in> c" ..
+
+  from G1 c have "G1 \<in> M" ..
+  then obtain H1 h1 where G1_rep: "G1 = graph H1 h1"
+    by (unfold M_def) blast
+
+  from G2 c have "G2 \<in> M" ..
+  then obtain H2 h2 where G2_rep: "G2 = graph H2 h2"
+    by (unfold M_def) blast
+
+  txt {* @{text "G\<^sub>1"} is contained in @{text "G\<^sub>2"}
+    or vice versa, since both @{text "G\<^sub>1"} and @{text
+    "G\<^sub>2"} are members of @{text c}. \label{cases2}*}
+
+  from cM G1 G2 have "G1 \<subseteq> G2 \<or> G2 \<subseteq> G1" (is "?case1 \<or> ?case2") ..
+  then show ?thesis
+  proof
+    assume ?case1
+    with xy' G2_rep have "(x, y) \<in> graph H2 h2" by blast
+    hence "y = h2 x" ..
+    also
+    from xz' G2_rep have "(x, z) \<in> graph H2 h2" by (simp only:)
+    hence "z = h2 x" ..
+    finally show ?thesis .
+  next
+    assume ?case2
+    with xz' G1_rep have "(x, z) \<in> graph H1 h1" by blast
+    hence "z = h1 x" ..
+    also
+    from xy' G1_rep have "(x, y) \<in> graph H1 h1" by (simp only:)
+    hence "y = h1 x" ..
+    finally show ?thesis ..
   qed
 qed
 
 text {*
   \medskip The limit function @{text h} is linear. Every element

   @{text x} are identical for @{text h'} and @{text h}.  Finally, the
   function @{text h'} is linear by construction of @{text M}.
 *}
 
 lemma sup_lf:
-  "M = norm_pres_extensions E p F f \<Longrightarrow> c \<in> chain M \<Longrightarrow>
-  graph H h = \<Union>c \<Longrightarrow> is_linearform H h"
-proof -
-  assume "M = norm_pres_extensions E p F f"  "c \<in> chain M"
-         "graph H h = \<Union>c"
-
-  show "is_linearform H h"
-  proof
-    fix x y assume "x \<in> H"  "y \<in> H"
-    have "\<exists>H' h'. x \<in> H' \<and> y \<in> H' \<and> graph H' h' \<subseteq> graph H h
-            \<and> is_linearform H' h' \<and> is_subspace H' E
-            \<and> is_subspace F H' \<and> graph F f \<subseteq> graph H' h'
-            \<and> (\<forall>x \<in> H'. h' x \<le> p x)"
-      by (rule some_H'h'2)
-
-    txt {* We have to show that @{text h} is additive. *}
-
-    thus "h (x + y) = h x + h y"
-    proof (elim exE conjE)
-      fix H' h' assume "x \<in> H'"  "y \<in> H'"
-        and b: "graph H' h' \<subseteq> graph H h"
-        and "is_linearform H' h'"  "is_subspace H' E"
-      have "h' (x + y) = h' x + h' y"
-        by (rule linearform_add)
-      also have "h' x = h x" ..
-      also have "h' y = h y" ..
-      also have "x + y \<in> H'" ..
-      with b have "h' (x + y) = h (x + y)" ..
-      finally show ?thesis .
-    qed
-  next
-    fix a x assume "x \<in> H"
-    have "\<exists>H' h'. x \<in> H' \<and> graph H' h' \<subseteq> graph H h
-            \<and> is_linearform H' h' \<and> is_subspace H' E
-            \<and> is_subspace F H' \<and> graph F f \<subseteq> graph H' h'
-            \<and> (\<forall>x \<in> H'. h' x \<le> p x)"
-      by (rule some_H'h')
-
-    txt{* We have to show that @{text h} is multiplicative. *}
-
-    thus "h (a \<cdot> x) = a * h x"
-    proof (elim exE conjE)
-      fix H' h' assume "x \<in> H'"
-        and b: "graph H' h' \<subseteq> graph H h"
-        and "is_linearform H' h'"  "is_subspace H' E"
-      have "h' (a \<cdot> x) = a * h' x"
-        by (rule linearform_mult)
-      also have "h' x = h x" ..
-      also have "a \<cdot> x \<in> H'" ..
-      with b have "h' (a \<cdot> x) = h (a \<cdot> x)" ..
-      finally show ?thesis .
-    qed
+  assumes M: "M = norm_pres_extensions E p F f"
+    and cM: "c \<in> chain M"
+    and u: "graph H h = \<Union>c"
+  shows "linearform H h"
+proof
+  fix x y assume x: "x \<in> H" and y: "y \<in> H"
+  with M cM u obtain H' h' where
+        x': "x \<in> H'" and y': "y \<in> H'"
+      and b: "graph H' h' \<subseteq> graph H h"
+      and linearform: "linearform H' h'"
+      and subspace: "H' \<unlhd> E"
+    by (rule some_H'h'2 [elim_format]) blast
+
+  show "h (x + y) = h x + h y"
+  proof -
+    from linearform x' y' have "h' (x + y) = h' x + h' y"
+      by (rule linearform.add)
+    also from b x' have "h' x = h x" ..
+    also from b y' have "h' y = h y" ..
+    also from subspace x' y' have "x + y \<in> H'"
+      by (rule subspace.add_closed)
+    with b have "h' (x + y) = h (x + y)" ..
+    finally show ?thesis .
+  qed
+next
+  fix x a assume x: "x \<in> H"
+  with M cM u obtain H' h' where
+        x': "x \<in> H'"
+      and b: "graph H' h' \<subseteq> graph H h"
+      and linearform: "linearform H' h'"
+      and subspace: "H' \<unlhd> E"
+    by (rule some_H'h' [elim_format]) blast
+
+  show "h (a \<cdot> x) = a * h x"
+  proof -
+    from linearform x' have "h' (a \<cdot> x) = a * h' x"
+      by (rule linearform.mult)
+    also from b x' have "h' x = h x" ..
+    also from subspace x' have "a \<cdot> x \<in> H'"
+      by (rule subspace.mult_closed)
+    with b have "h' (a \<cdot> x) = h (a \<cdot> x)" ..
+    finally show ?thesis .
   qed
 qed
 
 text {*
   \medskip The limit of a non-empty chain of norm preserving

   element of the chain is an extension of @{text f} and the supremum
   is an extension for every element of the chain.
 *}
 
 lemma sup_ext:
-  "graph H h = \<Union>c \<Longrightarrow> M = norm_pres_extensions E p F f \<Longrightarrow>
-  c \<in> chain M \<Longrightarrow> \<exists>x. x \<in> c \<Longrightarrow> graph F f \<subseteq> graph H h"
+  assumes graph: "graph H h = \<Union>c"
+    and M: "M = norm_pres_extensions E p F f"
+    and cM: "c \<in> chain M"
+    and ex: "\<exists>x. x \<in> c"
+  shows "graph F f \<subseteq> graph H h"
 proof -
-  assume "M = norm_pres_extensions E p F f"  "c \<in> chain M"
-         "graph H h = \<Union>c"
-  assume "\<exists>x. x \<in> c"
-  thus ?thesis
-  proof
-    fix x assume "x \<in> c"
-    have "c \<subseteq> M" by (rule chainD2)
-    hence "x \<in> M" ..
-    hence "x \<in> norm_pres_extensions E p F f" by (simp!)
-
-    hence "\<exists>G g. graph G g = x
-             \<and> is_linearform G g
-             \<and> is_subspace G E
-             \<and> is_subspace F G
-             \<and> graph F f \<subseteq> graph G g
-             \<and> (\<forall>x \<in> G. g x \<le> p x)"
-      by (simp! add: norm_pres_extension_D)
-
-    thus ?thesis
-    proof (elim exE conjE)
-      fix G g assume "graph F f \<subseteq> graph G g"
-      also assume "graph G g = x"
-      also have "... \<in> c" .
-      hence "x \<subseteq> \<Union>c" by fast
-      also have [symmetric]: "graph H h = \<Union>c" .
-      finally show ?thesis .
-    qed
-  qed
+  from ex obtain x where xc: "x \<in> c" ..
+  from cM have "c \<subseteq> M" ..
+  with xc have "x \<in> M" ..
+  with M have "x \<in> norm_pres_extensions E p F f"
+    by (simp only:)
+  then obtain G g where "x = graph G g" and "graph F f \<subseteq> graph G g" ..
+  then have "graph F f \<subseteq> x" by (simp only:)
+  also from xc have "\<dots> \<subseteq> \<Union>c" by blast
+  also from graph have "\<dots> = graph H h" ..
+  finally show ?thesis .
 qed
 
 text {*
   \medskip The domain @{text H} of the limit function is a superspace
   of @{text F}, since @{text F} is a subset of @{text H}. The
   existence of the @{text 0} element in @{text F} and the closure
   properties follow from the fact that @{text F} is a vector space.
 *}
 
 lemma sup_supF:
-  "graph H h = \<Union>c \<Longrightarrow> M = norm_pres_extensions E p F f \<Longrightarrow>
-  c \<in> chain M \<Longrightarrow> \<exists>x. x \<in> c \<Longrightarrow> is_subspace F E \<Longrightarrow> is_vectorspace E
-  \<Longrightarrow> is_subspace F H"
-proof -
-  assume "M = norm_pres_extensions E p F f"  "c \<in> chain M"  "\<exists>x. x \<in> c"
-    "graph H h = \<Union>c"  "is_subspace F E"  "is_vectorspace E"
-
-  show ?thesis
-  proof
-    show "0 \<in> F" ..
-    show "F \<subseteq> H"
-    proof (rule graph_extD2)
-      show "graph F f \<subseteq> graph H h"
-        by (rule sup_ext)
-    qed
-    show "\<forall>x \<in> F. \<forall>y \<in> F. x + y \<in> F"
-    proof (intro ballI)
-      fix x y assume "x \<in> F"  "y \<in> F"
-      show "x + y \<in> F" by (simp!)
-    qed
-    show "\<forall>x \<in> F. \<forall>a. a \<cdot> x \<in> F"
-    proof (intro ballI allI)
-      fix x a assume "x\<in>F"
-      show "a \<cdot> x \<in> F" by (simp!)
-    qed
-  qed
+  assumes graph: "graph H h = \<Union>c"
+    and M: "M = norm_pres_extensions E p F f"
+    and cM: "c \<in> chain M"
+    and ex: "\<exists>x. x \<in> c"
+    and FE: "F \<unlhd> E"
+  shows "F \<unlhd> H"
+proof
+  from FE show "F \<noteq> {}" by (rule subspace.non_empty)
+  from graph M cM ex have "graph F f \<subseteq> graph H h" by (rule sup_ext)
+  then show "F \<subseteq> H" ..
+  fix x y assume "x \<in> F" and "y \<in> F"
+  with FE show "x + y \<in> F" by (rule subspace.add_closed)
+next
+  fix x a assume "x \<in> F"
+  with FE show "a \<cdot> x \<in> F" by (rule subspace.mult_closed)
 qed
 
 text {*
   \medskip The domain @{text H} of the limit function is a subspace of
   @{text E}.
 *}
 
 lemma sup_subE:
-  "graph H h = \<Union>c \<Longrightarrow> M = norm_pres_extensions E p F f \<Longrightarrow>
-  c \<in> chain M \<Longrightarrow> \<exists>x. x \<in> c \<Longrightarrow> is_subspace F E \<Longrightarrow> is_vectorspace E
-  \<Longrightarrow> is_subspace H E"
-proof -
-  assume "M = norm_pres_extensions E p F f"  "c \<in> chain M"  "\<exists>x. x \<in> c"
-    "graph H h = \<Union>c"  "is_subspace F E"  "is_vectorspace E"
-  show ?thesis
+  assumes graph: "graph H h = \<Union>c"
+    and M: "M = norm_pres_extensions E p F f"
+    and cM: "c \<in> chain M"
+    and ex: "\<exists>x. x \<in> c"
+    and FE: "F \<unlhd> E"
+    and E: "vectorspace E"
+  shows "H \<unlhd> E"
+proof
+  show "H \<noteq> {}"
+  proof -
+    from FE E have "0 \<in> F" by (rule subvectorspace.zero)
+    also from graph M cM ex FE have "F \<unlhd> H" by (rule sup_supF)
+    then have "F \<subseteq> H" ..
+    finally show ?thesis by blast
+  qed
+  show "H \<subseteq> E"
   proof
-
-    txt {* The @{text 0} element is in @{text H}, as @{text F} is a
-    subset of @{text H}: *}
-
-    have "0 \<in> F" ..
-    also have "is_subspace F H" by (rule sup_supF)
-    hence "F \<subseteq> H" ..
-    finally show "0 \<in> H" .
-
-    txt {* @{text H} is a subset of @{text E}: *}
-
-    show "H \<subseteq> E"
-    proof
-      fix x assume "x \<in> H"
-      have "\<exists>H' h'. x \<in> H' \<and> graph H' h' \<subseteq> graph H h
-              \<and> is_linearform H' h' \<and> is_subspace H' E
-              \<and> is_subspace F H' \<and> graph F f \<subseteq> graph H' h'
-              \<and> (\<forall>x \<in> H'. h' x \<le> p x)"
-        by (rule some_H'h')
-      thus "x \<in> E"
-      proof (elim exE conjE)
-        fix H' h' assume "x \<in> H'"  "is_subspace H' E"
-        have "H' \<subseteq> E" ..
-        thus "x \<in> E" ..
-      qed
-    qed
-
-    txt {* @{text H} is closed under addition: *}
-
-    show "\<forall>x \<in> H. \<forall>y \<in> H. x + y \<in> H"
-    proof (intro ballI)
-      fix x y assume "x \<in> H"  "y \<in> H"
-      have "\<exists>H' h'. x \<in> H' \<and> y \<in> H' \<and> graph H' h' \<subseteq> graph H h
-              \<and> is_linearform H' h' \<and> is_subspace H' E
-              \<and> is_subspace F H' \<and> graph F f \<subseteq> graph H' h'
-              \<and> (\<forall>x \<in> H'. h' x \<le> p x)"
-        by (rule some_H'h'2)
-      thus "x + y \<in> H"
-      proof (elim exE conjE)
-        fix H' h'
-        assume "x \<in> H'"  "y \<in> H'"  "is_subspace H' E"
-          "graph H' h' \<subseteq> graph H h"
-        have "x + y \<in> H'" ..
-        also have "H' \<subseteq> H" ..
-        finally show ?thesis .
-      qed
-    qed
-
-    txt {* @{text H} is closed under scalar multiplication: *}
-
-    show "\<forall>x \<in> H. \<forall>a. a \<cdot> x \<in> H"
-    proof (intro ballI allI)
-      fix x a assume "x \<in> H"
-      have "\<exists>H' h'. x \<in> H' \<and> graph H' h' \<subseteq> graph H h
-              \<and> is_linearform H' h' \<and> is_subspace H' E
-              \<and> is_subspace F H' \<and> graph F f \<subseteq> graph H' h'
-              \<and> (\<forall>x \<in> H'. h' x \<le> p x)"
-        by (rule some_H'h')
-      thus "a \<cdot> x \<in> H"
-      proof (elim exE conjE)
-        fix H' h'
-        assume "x \<in> H'"  "is_subspace H' E"  "graph H' h' \<subseteq> graph H h"
-        have "a \<cdot> x \<in> H'" ..
-        also have "H' \<subseteq> H" ..
-        finally show ?thesis .
-      qed
-    qed
+    fix x assume "x \<in> H"
+    with M cM graph
+    obtain H' h' where x: "x \<in> H'" and H'E: "H' \<unlhd> E"
+      by (rule some_H'h' [elim_format]) blast
+    from H'E have "H' \<subseteq> E" ..
+    with x show "x \<in> E" ..
+  qed
+  fix x y assume x: "x \<in> H" and y: "y \<in> H"
+  show "x + y \<in> H"
+  proof -
+    from M cM graph x y obtain H' h' where
+          x': "x \<in> H'" and y': "y \<in> H'" and H'E: "H' \<unlhd> E"
+        and graphs: "graph H' h' \<subseteq> graph H h"
+      by (rule some_H'h'2 [elim_format]) blast
+    from H'E x' y' have "x + y \<in> H'"
+      by (rule subspace.add_closed)
+    also from graphs have "H' \<subseteq> H" ..
+    finally show ?thesis .
+  qed
+next
+  fix x a assume x: "x \<in> H"
+  show "a \<cdot> x \<in> H"
+  proof -
+    from M cM graph x
+    obtain H' h' where x': "x \<in> H'" and H'E: "H' \<unlhd> E"
+        and graphs: "graph H' h' \<subseteq> graph H h"
+      by (rule some_H'h' [elim_format]) blast
+    from H'E x' have "a \<cdot> x \<in> H'" by (rule subspace.mult_closed)
+    also from graphs have "H' \<subseteq> H" ..
+    finally show ?thesis .
   qed
 qed
 
 text {*
   \medskip The limit function is bounded by the norm @{text p} as
   well, since all elements in the chain are bounded by @{text p}.
 *}
 
 lemma sup_norm_pres:
-  "graph H h = \<Union>c \<Longrightarrow> M = norm_pres_extensions E p F f \<Longrightarrow>
-  c \<in> chain M \<Longrightarrow> \<forall>x \<in> H. h x \<le> p x"
+  assumes graph: "graph H h = \<Union>c"
+    and M: "M = norm_pres_extensions E p F f"
+    and cM: "c \<in> chain M"
+  shows "\<forall>x \<in> H. h x \<le> p x"
 proof
-  assume "M = norm_pres_extensions E p F f"  "c \<in> chain M"
-         "graph H h = \<Union>c"
   fix x assume "x \<in> H"
-  have "\<exists>H' h'. x \<in> H' \<and> graph H' h' \<subseteq> graph H h
-          \<and> is_linearform H' h' \<and> is_subspace H' E \<and> is_subspace F H'
-          \<and> graph F f \<subseteq> graph H' h' \<and> (\<forall>x \<in> H'. h' x \<le> p x)"
-    by (rule some_H'h')
-  thus "h x \<le> p x"
-  proof (elim exE conjE)
-    fix H' h'
-    assume "x \<in> H'"  "graph H' h' \<subseteq> graph H h"
+  with M cM graph obtain H' h' where x': "x \<in> H'"
+      and graphs: "graph H' h' \<subseteq> graph H h"
       and a: "\<forall>x \<in> H'. h' x \<le> p x"
-    have [symmetric]: "h' x = h x" ..
-    also from a have "h' x \<le> p x " ..
-    finally show ?thesis .
-  qed
-qed
-
+    by (rule some_H'h' [elim_format]) blast
+  from graphs x' have [symmetric]: "h' x = h x" ..
+  also from a x' have "h' x \<le> p x " ..
+  finally show "h x \<le> p x" .
+qed
 
 text {*
   \medskip The following lemma is a property of linear forms on real
   vector spaces. It will be used for the lemma @{text abs_HahnBanach}
   (see page \pageref{abs-HahnBanach}). \label{abs-ineq-iff} For real

   \end{tabular}
   \end{center}
 *}
 
 lemma abs_ineq_iff:
-  "is_subspace H E \<Longrightarrow> is_vectorspace E \<Longrightarrow> is_seminorm E p \<Longrightarrow>
-  is_linearform H h
-  \<Longrightarrow> (\<forall>x \<in> H. \<bar>h x\<bar> \<le> p x) = (\<forall>x \<in> H. h x \<le> p x)"
-  (concl is "?L = ?R")
-proof -
-  assume "is_subspace H E"  "is_vectorspace E"  "is_seminorm E p"
-         "is_linearform H h"
-  have h: "is_vectorspace H" ..
-  show ?thesis
-  proof
+  includes subvectorspace H E + seminorm E p + linearform H h
+  shows "(\<forall>x \<in> H. \<bar>h x\<bar> \<le> p x) = (\<forall>x \<in> H. h x \<le> p x)" (is "?L = ?R")
+proof
+  have h: "vectorspace H" by (rule vectorspace)
+  {
     assume l: ?L
     show ?R
     proof
       fix x assume x: "x \<in> H"
-      have "h x \<le> \<bar>h x\<bar>" by (rule abs_ge_self)
-      also from l have "... \<le> p x" ..
+      have "h x \<le> \<bar>h x\<bar>" by arith
+      also from l x have "\<dots> \<le> p x" ..
       finally show "h x \<le> p x" .
     qed
   next
     assume r: ?R
     show ?L
     proof
-      fix x assume "x \<in> H"
+      fix x assume x: "x \<in> H"
       show "\<And>a b :: real. - a \<le> b \<Longrightarrow> b \<le> a \<Longrightarrow> \<bar>b\<bar> \<le> a"
         by arith
       show "- p x \<le> h x"
       proof (rule real_minus_le)
-        from h have "- h x = h (- x)"
-          by (rule linearform_neg [symmetric])
-        also from r have "... \<le> p (- x)" by (simp!)
-        also have "... = p x"
-        proof (rule seminorm_minus)
+        have "linearform H h" .
+        from h this x have "- h x = h (- x)"
+          by (rule vectorspace_linearform.neg [symmetric])
+        also from r x have "\<dots> \<le> p (- x)" by simp
+        also have "\<dots> = p x"
+        proof (rule seminorm_vectorspace.minus)
           show "x \<in> E" ..
         qed
         finally show "- h x \<le> p x" .
       qed
-      from r show "h x \<le> p x" ..
+      from r x show "h x \<le> p x" ..
     qed
-  qed
+  }
 qed
 
 end