# HG changeset patch
# User wenzelm
# Date 1030042183 -7200
# Node ID a6a7025fd7e83fb3474ac70b52f22fcb2f0d34fd
# Parent  cc3bbaf1b8d3c8faae21e0bcd3a40699588acf2b
updated to use locales (still some rough edges);

diff -r cc3bbaf1b8d3 -r a6a7025fd7e8 src/HOL/Real/HahnBanach/Aux.thy
--- a/src/HOL/Real/HahnBanach/Aux.thy	Thu Aug 22 12:28:41 2002 +0200
+++ b/src/HOL/Real/HahnBanach/Aux.thy	Thu Aug 22 20:49:43 2002 +0200
@@ -3,25 +3,15 @@
     Author:     Gertrud Bauer, TU Munich
 *)
 
-header {* Auxiliary theorems *}
+header {* Auxiliary theorems *}  (* FIXME clean *)
 
-theory Aux = Real + Zorn:
+theory Aux = Real + Bounds + Zorn:
 
 text {* Some existing theorems are declared as extra introduction
 or elimination rules, respectively. *}
 
-lemmas [intro?] = isLub_isUb
-lemmas [intro?] = chainD
-lemmas chainE2 = chainD2 [elim_format, standard]
-
-
-text {* \medskip Lemmas about sets. *}
-
-lemma Int_singletonD: "A \<inter> B = {v} \<Longrightarrow> x \<in> A \<Longrightarrow> x \<in> B \<Longrightarrow> x = v"
-  by (fast elim: equalityE)
-
-lemma set_less_imp_diff_not_empty: "H < E \<Longrightarrow> \<exists>x0 \<in> E. x0 \<notin> H"
-  by (auto simp add: psubset_eq)
+lemmas [dest?] = chainD
+lemmas chainE2 [elim?] = chainD2 [elim_format, standard]
 
 
 text{* \medskip Some lemmas about orders. *}
diff -r cc3bbaf1b8d3 -r a6a7025fd7e8 src/HOL/Real/HahnBanach/Bounds.thy
--- a/src/HOL/Real/HahnBanach/Bounds.thy	Thu Aug 22 12:28:41 2002 +0200
+++ b/src/HOL/Real/HahnBanach/Bounds.thy	Thu Aug 22 20:49:43 2002 +0200
@@ -7,47 +7,71 @@
 
 theory Bounds = Main + Real:
 
-text {*
-  A supremum\footnote{The definition of the supremum is based on one
-  in \url{http://isabelle.in.tum.de/library/HOL/HOL-Real/Lubs.html}}
-  of an ordered set @{text B} w.~r.~t. @{text A} is defined as a least
-  upper bound of @{text B}, which lies in @{text A}.
-*}
-   
-text {*
-  If a supremum exists, then @{text "Sup A B"} is equal to the
-  supremum. *}
+locale lub =
+  fixes A and x
+  assumes least [intro?]: "(\<And>a. a \<in> A \<Longrightarrow> a \<le> b) \<Longrightarrow> x \<le> b"
+    and upper [intro?]: "a \<in> A \<Longrightarrow> a \<le> x"
+
+lemmas [elim?] = lub.least lub.upper
+
+syntax (xsymbols)
+  the_lub :: "'a::order set \<Rightarrow> 'a"    ("\<Squnion>_" [90] 90)
 
 constdefs
-  is_Sup :: "('a::order) set \<Rightarrow> 'a set \<Rightarrow> 'a \<Rightarrow> bool"
-  "is_Sup A B x \<equiv> isLub A B x"
-
-  Sup :: "('a::order) set \<Rightarrow> 'a set \<Rightarrow> 'a"
-  "Sup A B \<equiv> Eps (is_Sup A B)"
+  the_lub :: "'a::order set \<Rightarrow> 'a"
+  "\<Squnion>A \<equiv> The (lub A)"
 
-text {*
-  The supremum of @{text B} is less than any upper bound of
-  @{text B}. *}
-
-lemma sup_le_ub: "isUb A B y \<Longrightarrow> is_Sup A B s \<Longrightarrow> s \<le> y"
-  by (unfold is_Sup_def, rule isLub_le_isUb)
-
-text {* The supremum @{text B} is an upper bound for @{text B}. *}
+lemma the_lub_equality [elim?]:
+  includes lub
+  shows "\<Squnion>A = (x::'a::order)"
+proof (unfold the_lub_def)
+  from lub_axioms show "The (lub A) = x"
+  proof
+    fix x' assume lub': "lub A x'"
+    show "x' = x"
+    proof (rule order_antisym)
+      from lub' show "x' \<le> x"
+      proof
+        fix a assume "a \<in> A"
+        then show "a \<le> x" ..
+      qed
+      show "x \<le> x'"
+      proof
+        fix a assume "a \<in> A"
+        with lub' show "a \<le> x'" ..
+      qed
+    qed
+  qed
+qed
 
-lemma sup_ub: "y \<in> B \<Longrightarrow> is_Sup A B s \<Longrightarrow> y \<le> s"
-  by (unfold is_Sup_def, rule isLubD2)
-
-text {*
-  The supremum of a non-empty set @{text B} is greater than a lower
-  bound of @{text B}. *}
+lemma the_lubI_ex:
+  assumes ex: "\<exists>x. lub A x"
+  shows "lub A (\<Squnion>A)"
+proof -
+  from ex obtain x where x: "lub A x" ..
+  also from x have [symmetric]: "\<Squnion>A = x" ..
+  finally show ?thesis .
+qed
 
-lemma sup_ub1: 
-  "\<forall>y \<in> B. a \<le> y \<Longrightarrow> is_Sup A B s \<Longrightarrow> x \<in> B \<Longrightarrow> a \<le> s"
-proof - 
-  assume "\<forall>y \<in> B. a \<le> y"  "is_Sup A B s"  "x \<in> B"
-  have "a \<le> x" by (rule bspec)
-  also have "x \<le> s" by (rule sup_ub)
-  finally show "a \<le> s" .
+lemma lub_compat: "lub A x = isLub UNIV A x"
+proof -
+  have "isUb UNIV A = (\<lambda>x. A *<= x \<and> x \<in> UNIV)"
+    by (rule ext) (simp only: isUb_def)
+  then show ?thesis
+    by (simp only: lub_def isLub_def leastP_def setge_def setle_def) blast
 qed
-  
+
+lemma real_complete:
+  fixes A :: "real set"
+  assumes nonempty: "\<exists>a. a \<in> A"
+    and ex_upper: "\<exists>y. \<forall>a \<in> A. a \<le> y"
+  shows "\<exists>x. lub A x"
+proof -
+  from ex_upper have "\<exists>y. isUb UNIV A y"
+    by (unfold isUb_def setle_def) blast
+  with nonempty have "\<exists>x. isLub UNIV A x"
+    by (rule reals_complete)
+  then show ?thesis by (simp only: lub_compat)
+qed
+
 end
diff -r cc3bbaf1b8d3 -r a6a7025fd7e8 src/HOL/Real/HahnBanach/FunctionNorm.thy
--- a/src/HOL/Real/HahnBanach/FunctionNorm.thy	Thu Aug 22 12:28:41 2002 +0200
+++ b/src/HOL/Real/HahnBanach/FunctionNorm.thy	Thu Aug 22 20:49:43 2002 +0200
@@ -11,7 +11,7 @@
 
 text {*
   A linear form @{text f} on a normed vector space @{text "(V, \<parallel>\<cdot>\<parallel>)"}
-  is \emph{continuous}, iff it is bounded, i.~e.
+  is \emph{continuous}, iff it is bounded, i.e.
   \begin{center}
   @{text "\<exists>c \<in> R. \<forall>x \<in> V. \<bar>f x\<bar> \<le> c \<cdot> \<parallel>x\<parallel>"}
   \end{center}
@@ -20,28 +20,21 @@
   linear forms:
 *}
 
-constdefs
-  is_continuous ::
-  "'a::{plus, minus, zero} set \<Rightarrow> ('a \<Rightarrow> real) \<Rightarrow> ('a \<Rightarrow> real) \<Rightarrow> bool"
-  "is_continuous V norm f \<equiv>
-    is_linearform V f \<and> (\<exists>c. \<forall>x \<in> V. \<bar>f x\<bar> \<le> c * norm x)"
+locale continuous = var V + norm_syntax + linearform +
+  assumes bounded: "\<exists>c. \<forall>x \<in> V. \<bar>f x\<bar> \<le> c * \<parallel>x\<parallel>"
 
 lemma continuousI [intro]:
-  "is_linearform V f \<Longrightarrow> (\<And>x. x \<in> V \<Longrightarrow> \<bar>f x\<bar> \<le> c * norm x)
-  \<Longrightarrow> is_continuous V norm f"
-  by (unfold is_continuous_def) blast
-
-lemma continuous_linearform [intro?]:
-  "is_continuous V norm f \<Longrightarrow> is_linearform V f"
-  by (unfold is_continuous_def) blast
-
-lemma continuous_bounded [intro?]:
-  "is_continuous V norm f
-  \<Longrightarrow> \<exists>c. \<forall>x \<in> V. \<bar>f x\<bar> \<le> c * norm x"
-  by (unfold is_continuous_def) blast
+  includes norm_syntax + linearform
+  assumes r: "\<And>x. x \<in> V \<Longrightarrow> \<bar>f x\<bar> \<le> c * \<parallel>x\<parallel>"
+  shows "continuous V norm f"
+proof
+  show "linearform V f" .
+  from r have "\<exists>c. \<forall>x\<in>V. \<bar>f x\<bar> \<le> c * \<parallel>x\<parallel>" by blast
+  then show "continuous_axioms V norm f" ..
+qed
 
 
-subsection{* The norm of a linear form *}
+subsection {* The norm of a linear form *}
 
 text {*
   The least real number @{text c} for which holds
@@ -62,174 +55,133 @@
   element in this set. This element must be @{text "{} \<ge> 0"} so that
   @{text function_norm} has the norm properties. Furthermore
   it does not have to change the norm in all other cases, so it must
-  be @{text 0}, as all other elements of are @{text "{} \<ge> 0"}.
+  be @{text 0}, as all other elements are @{text "{} \<ge> 0"}.
 
-  Thus we define the set @{text B} the supremum is taken from as
+  Thus we define the set @{text B} where the supremum is taken from as
+  follows:
   \begin{center}
   @{text "{0} \<union> {\<bar>f x\<bar> / \<parallel>x\<parallel>. x \<noteq> 0 \<and> x \<in> F}"}
   \end{center}
-*}
 
-constdefs
-  B :: "'a set \<Rightarrow> ('a \<Rightarrow> real) \<Rightarrow> ('a::{plus, minus, zero} \<Rightarrow> real) \<Rightarrow> real set"
-  "B V norm f \<equiv>
-  {0} \<union> {\<bar>f x\<bar> * inverse (norm x) | x. x \<noteq> 0 \<and> x \<in> V}"
-
-text {*
-  @{text n} is the function norm of @{text f}, iff @{text n} is the
-  supremum of @{text B}.
+  @{text function_norm} is equal to the supremum of @{text B}, if the
+  supremum exists (otherwise it is undefined).
 *}
 
-constdefs
-  is_function_norm ::
-  "('a::{minus,plus,zero} \<Rightarrow> real) \<Rightarrow> 'a set \<Rightarrow> ('a \<Rightarrow> real) \<Rightarrow> real \<Rightarrow> bool"
-  "is_function_norm f V norm fn \<equiv> is_Sup UNIV (B V norm f) fn"
-
-text {*
-  @{text function_norm} is equal to the supremum of @{text B}, if the
-  supremum exists. Otherwise it is undefined.
-*}
+locale function_norm = norm_syntax +
+  fixes B
+  defines "B V f \<equiv> {0} \<union> {\<bar>f x\<bar> / \<parallel>x\<parallel> | x. x \<noteq> 0 \<and> x \<in> V}"
+  fixes function_norm ("\<parallel>_\<parallel>\<hyphen>_" [0, 1000] 999)
+  defines "\<parallel>f\<parallel>\<hyphen>V \<equiv> \<Squnion>(B V f)"
 
-constdefs
-  function_norm :: "('a::{minus,plus,zero} \<Rightarrow> real) \<Rightarrow> 'a set \<Rightarrow> ('a \<Rightarrow> real) \<Rightarrow> real"
-  "function_norm f V norm \<equiv> Sup UNIV (B V norm f)"
+lemma (in function_norm) B_not_empty [intro]: "0 \<in> B V f"
+  by (unfold B_def) simp
 
-syntax
-  function_norm :: "('a \<Rightarrow> real) \<Rightarrow> 'a set \<Rightarrow> ('a \<Rightarrow> real) \<Rightarrow> real"  ("\<parallel>_\<parallel>_,_")
-
-lemma B_not_empty: "0 \<in> B V norm f"
-  by (unfold B_def) blast
+locale (open) functional_vectorspace =
+    normed_vectorspace + function_norm +
+  fixes cont
+  defines "cont f \<equiv> continuous V norm f"
 
 text {*
   The following lemma states that every continuous linear form on a
   normed space @{text "(V, \<parallel>\<cdot>\<parallel>)"} has a function norm.
 *}
 
-lemma ex_fnorm [intro?]:
-  "is_normed_vectorspace V norm \<Longrightarrow> is_continuous V norm f
-     \<Longrightarrow> is_function_norm f V norm \<parallel>f\<parallel>V,norm"
-proof (unfold function_norm_def is_function_norm_def
-  is_continuous_def Sup_def, elim conjE, rule someI2_ex)
-  assume "is_normed_vectorspace V norm"
-  assume "is_linearform V f"
-  and e: "\<exists>c. \<forall>x \<in> V. \<bar>f x\<bar> \<le> c * norm x"
-
+lemma (in functional_vectorspace) function_norm_works:
+  includes continuous
+  shows "lub (B V f) (\<parallel>f\<parallel>\<hyphen>V)"
+proof -
   txt {* The existence of the supremum is shown using the
-  completeness of the reals. Completeness means, that
-  every non-empty bounded set of reals has a
-  supremum. *}
-  show  "\<exists>a. is_Sup UNIV (B V norm f) a"
-  proof (unfold is_Sup_def, rule reals_complete)
-
+    completeness of the reals. Completeness means, that every
+    non-empty bounded set of reals has a supremum. *}
+  have "\<exists>a. lub (B V f) a"
+  proof (rule real_complete)
     txt {* First we have to show that @{text B} is non-empty: *}
-
-    show "\<exists>X. X \<in> B V norm f"
-    proof
-      show "0 \<in> (B V norm f)" by (unfold B_def) blast
-    qed
+    have "0 \<in> B V f" ..
+    thus "\<exists>x. x \<in> B V f" ..
 
     txt {* Then we have to show that @{text B} is bounded: *}
-
-    from e show "\<exists>Y. isUb UNIV (B V norm f) Y"
-    proof
-
+    show "\<exists>c. \<forall>y \<in> B V f. y \<le> c"
+    proof -
       txt {* We know that @{text f} is bounded by some value @{text c}. *}
-
-      fix c assume a: "\<forall>x \<in> V. \<bar>f x\<bar> \<le> c * norm x"
-      def b \<equiv> "max c 0"
+      from bounded obtain c where c: "\<forall>x \<in> V. \<bar>f x\<bar> \<le> c * \<parallel>x\<parallel>" ..
 
-      show "?thesis"
-      proof (intro exI isUbI setleI ballI, unfold B_def,
-        elim UnE CollectE exE conjE singletonE)
-
-        txt {* To proof the thesis, we have to show that there is some
-        constant @{text b}, such that @{text "y \<le> b"} for all
-        @{text "y \<in> B"}. Due to the definition of @{text B} there are
-        two cases for @{text "y \<in> B"}.  If @{text "y = 0"} then
-        @{text "y \<le> max c 0"}: *}
-
-        fix y assume "y = (0::real)"
-        show "y \<le> b" by (simp! add: le_maxI2)
-
-        txt {* The second case is @{text "y = \<bar>f x\<bar> / \<parallel>x\<parallel>"} for some
-        @{text "x \<in> V"} with @{text "x \<noteq> 0"}. *}
+      txt {* To prove the thesis, we have to show that there is some
+        @{text b}, such that @{text "y \<le> b"} for all @{text "y \<in>
+        B"}. Due to the definition of @{text B} there are two cases. *}
 
-      next
-        fix x y
-        assume "x \<in> V"  "x \<noteq> 0"
-
-        txt {* The thesis follows by a short calculation using the
-        fact that @{text f} is bounded. *}
+      def b \<equiv> "max c 0"
+      have "\<forall>y \<in> B V f. y \<le> b"
+      proof
+        fix y assume y: "y \<in> B V f"
+        show "y \<le> b"
+        proof cases
+          assume "y = 0"
+          thus ?thesis by (unfold b_def) arith
+        next
+          txt {* The second case is @{text "y = \<bar>f x\<bar> / \<parallel>x\<parallel>"} for some
+            @{text "x \<in> V"} with @{text "x \<noteq> 0"}. *}
+          assume "y \<noteq> 0"
+          with y obtain x where y_rep: "y = \<bar>f x\<bar> * inverse \<parallel>x\<parallel>"
+              and x: "x \<in> V" and neq: "x \<noteq> 0"
+            by (auto simp add: B_def real_divide_def)
+          from x neq have gt: "0 < \<parallel>x\<parallel>" ..
 
-        assume "y = \<bar>f x\<bar> * inverse (norm x)"
-        also have "... \<le> c * norm x * inverse (norm x)"
-        proof (rule real_mult_le_le_mono2)
-          show "0 \<le> inverse (norm x)"
-            by (rule order_less_imp_le, rule real_inverse_gt_0,
-                rule normed_vs_norm_gt_zero)
-          from a show "\<bar>f x\<bar> \<le> c * norm x" ..
+          txt {* The thesis follows by a short calculation using the
+            fact that @{text f} is bounded. *}
+
+          note y_rep
+          also have "\<bar>f x\<bar> * inverse \<parallel>x\<parallel> \<le> (c * \<parallel>x\<parallel>) * inverse \<parallel>x\<parallel>"
+          proof (rule real_mult_le_le_mono2)
+            from c show "\<bar>f x\<bar> \<le> c * \<parallel>x\<parallel>" ..
+            from gt have "0 < inverse \<parallel>x\<parallel>" by (rule real_inverse_gt_0)
+            thus "0 \<le> inverse \<parallel>x\<parallel>" by (rule order_less_imp_le)
+          qed
+          also have "\<dots> = c * (\<parallel>x\<parallel> * inverse \<parallel>x\<parallel>)"
+            by (rule real_mult_assoc)
+          also
+          from gt have "\<parallel>x\<parallel> \<noteq> 0" by simp
+          hence "\<parallel>x\<parallel> * inverse \<parallel>x\<parallel> = 1" by (simp add: real_mult_inv_right1)
+          also have "c * 1 \<le> b" by (simp add: b_def le_maxI1)
+          finally show "y \<le> b" .
         qed
-        also have "... = c * (norm x * inverse (norm x))"
-          by (rule real_mult_assoc)
-        also have "(norm x * inverse (norm x)) = (1::real)"
-        proof (rule real_mult_inv_right1)
-          show nz: "norm x \<noteq> 0"
-            by (rule not_sym, rule lt_imp_not_eq,
-              rule normed_vs_norm_gt_zero)
-        qed
-        also have "c * ... \<le> b " by (simp! add: le_maxI1)
-        finally show "y \<le> b" .
-      qed simp
+      qed
+      thus ?thesis ..
     qed
   qed
+  then show ?thesis
+    by (unfold function_norm_def) (rule the_lubI_ex)
+qed
+
+lemma (in functional_vectorspace) function_norm_ub [intro?]:
+  includes continuous
+  assumes b: "b \<in> B V f"
+  shows "b \<le> \<parallel>f\<parallel>\<hyphen>V"
+proof -
+  have "lub (B V f) (\<parallel>f\<parallel>\<hyphen>V)" by (rule function_norm_works)
+  from this and b show ?thesis ..
+qed
+
+lemma (in functional_vectorspace) function_norm_least [intro?]:
+  includes continuous
+  assumes b: "\<And>b. b \<in> B V f \<Longrightarrow> b \<le> y"
+  shows "\<parallel>f\<parallel>\<hyphen>V \<le> y"
+proof -
+  have "lub (B V f) (\<parallel>f\<parallel>\<hyphen>V)" by (rule function_norm_works)
+  from this and b show ?thesis ..
 qed
 
 text {* The norm of a continuous function is always @{text "\<ge> 0"}. *}
 
-lemma fnorm_ge_zero [intro?]:
-  "is_continuous V norm f \<Longrightarrow> is_normed_vectorspace V norm
-   \<Longrightarrow> 0 \<le> \<parallel>f\<parallel>V,norm"
+lemma (in functional_vectorspace) function_norm_ge_zero [iff]:
+  includes continuous
+  shows "0 \<le> \<parallel>f\<parallel>\<hyphen>V"
 proof -
-  assume c: "is_continuous V norm f"
-     and n: "is_normed_vectorspace V norm"
-
   txt {* The function norm is defined as the supremum of @{text B}.
-  So it is @{text "\<ge> 0"} if all elements in @{text B} are
-  @{text "\<ge> 0"}, provided the supremum exists and @{text B} is not
-  empty. *}
-
-  show ?thesis
-  proof (unfold function_norm_def, rule sup_ub1)
-    show "\<forall>x \<in> (B V norm f). 0 \<le> x"
-    proof (intro ballI, unfold B_def,
-           elim UnE singletonE CollectE exE conjE)
-      fix x r
-      assume "x \<in> V"  "x \<noteq> 0"
-        and r: "r = \<bar>f x\<bar> * inverse (norm x)"
-
-      have ge: "0 \<le> \<bar>f x\<bar>" by (simp! only: abs_ge_zero)
-      have "0 \<le> inverse (norm x)"
-        by (rule order_less_imp_le, rule real_inverse_gt_0, rule)(***
-        proof (rule order_less_imp_le);
-          show "0 < inverse (norm x)";
-          proof (rule real_inverse_gt_zero);
-            show "0 < norm x"; ..;
-          qed;
-        qed; ***)
-      with ge show "0 \<le> r"
-       by (simp only: r, rule real_le_mult_order1a)
-    qed (simp!)
-
-    txt {* Since @{text f} is continuous the function norm exists: *}
-
-    have "is_function_norm f V norm \<parallel>f\<parallel>V,norm" ..
-    thus "is_Sup UNIV (B V norm f) (Sup UNIV (B V norm f))"
-      by (unfold is_function_norm_def function_norm_def)
-
-    txt {* @{text B} is non-empty by construction: *}
-
-    show "0 \<in> B V norm f" by (rule B_not_empty)
-  qed
+    So it is @{text "\<ge> 0"} if all elements in @{text B} are @{text "\<ge>
+    0"}, provided the supremum exists and @{text B} is not empty. *}
+  have "lub (B V f) (\<parallel>f\<parallel>\<hyphen>V)" by (rule function_norm_works)
+  moreover have "0 \<in> B V f" ..
+  ultimately show ?thesis ..
 qed
 
 text {*
@@ -239,141 +191,79 @@
   \end{center}
 *}
 
-lemma norm_fx_le_norm_f_norm_x:
-  "is_continuous V norm f \<Longrightarrow> is_normed_vectorspace V norm \<Longrightarrow> x \<in> V
-    \<Longrightarrow> \<bar>f x\<bar> \<le> \<parallel>f\<parallel>V,norm * norm x"
-proof -
-  assume "is_normed_vectorspace V norm"  "x \<in> V"
-  and c: "is_continuous V norm f"
-  have v: "is_vectorspace V" ..
-
- txt{* The proof is by case analysis on @{text x}. *}
-
-  show ?thesis
-  proof cases
-
-    txt {* For the case @{text "x = 0"} the thesis follows from the
-    linearity of @{text f}: for every linear function holds
-    @{text "f 0 = 0"}. *}
-
-    assume "x = 0"
-    have "\<bar>f x\<bar> = \<bar>f 0\<bar>" by (simp!)
-    also from v continuous_linearform have "f 0 = 0" ..
-    also note abs_zero
-    also have "0 \<le> \<parallel>f\<parallel>V,norm * norm x"
-    proof (rule real_le_mult_order1a)
-      show "0 \<le> \<parallel>f\<parallel>V,norm" ..
-      show "0 \<le> norm x" ..
+lemma (in functional_vectorspace) function_norm_le_cong:
+  includes continuous + vectorspace_linearform
+  assumes x: "x \<in> V"
+  shows "\<bar>f x\<bar> \<le> \<parallel>f\<parallel>\<hyphen>V * \<parallel>x\<parallel>"
+proof cases
+  assume "x = 0"
+  then have "\<bar>f x\<bar> = \<bar>f 0\<bar>" by simp
+  also have "f 0 = 0" ..
+  also have "\<bar>\<dots>\<bar> = 0" by simp
+  also have "\<dots> \<le> \<parallel>f\<parallel>\<hyphen>V * \<parallel>x\<parallel>"
+  proof (rule real_le_mult_order1a)
+    show "0 \<le> \<parallel>f\<parallel>\<hyphen>V" ..
+    show "0 \<le> norm x" ..
+  qed
+  finally show "\<bar>f x\<bar> \<le> \<parallel>f\<parallel>\<hyphen>V * \<parallel>x\<parallel>" .
+next
+  assume "x \<noteq> 0"
+  with x have neq: "\<parallel>x\<parallel> \<noteq> 0" by simp
+  then have "\<bar>f x\<bar> = (\<bar>f x\<bar> * inverse \<parallel>x\<parallel>) * \<parallel>x\<parallel>" by simp
+  also have "\<dots> \<le>  \<parallel>f\<parallel>\<hyphen>V * \<parallel>x\<parallel>"
+  proof (rule real_mult_le_le_mono2)
+    from x show "0 \<le> \<parallel>x\<parallel>" ..
+    show "\<bar>f x\<bar> * inverse \<parallel>x\<parallel> \<le> \<parallel>f\<parallel>\<hyphen>V"
+    proof
+      from x and neq show "\<bar>f x\<bar> * inverse \<parallel>x\<parallel> \<in> B V f"
+        by (auto simp add: B_def real_divide_def)
     qed
-    finally
-    show "\<bar>f x\<bar> \<le> \<parallel>f\<parallel>V,norm * norm x" .
-
-  next
-    assume "x \<noteq> 0"
-    have n: "0 < norm x" ..
-    hence nz: "norm x \<noteq> 0"
-      by (simp only: lt_imp_not_eq)
-
-    txt {* For the case @{text "x \<noteq> 0"} we derive the following fact
-    from the definition of the function norm:*}
-
-    have l: "\<bar>f x\<bar> * inverse (norm x) \<le> \<parallel>f\<parallel>V,norm"
-    proof (unfold function_norm_def, rule sup_ub)
-      from ex_fnorm [OF _ c]
-      show "is_Sup UNIV (B V norm f) (Sup UNIV (B V norm f))"
-         by (simp! add: is_function_norm_def function_norm_def)
-      show "\<bar>f x\<bar> * inverse (norm x) \<in> B V norm f"
-        by (unfold B_def, intro UnI2 CollectI exI [of _ x]
-            conjI, simp)
-    qed
-
-    txt {* The thesis now follows by a short calculation: *}
-
-    have "\<bar>f x\<bar> = \<bar>f x\<bar> * 1" by (simp!)
-    also from nz have "1 = inverse (norm x) * norm x"
-      by (simp add: real_mult_inv_left1)
-    also have "\<bar>f x\<bar> * ... = \<bar>f x\<bar> * inverse (norm x) * norm x"
-      by (simp! add: real_mult_assoc)
-    also from n l have "... \<le> \<parallel>f\<parallel>V,norm * norm x"
-      by (simp add: real_mult_le_le_mono2)
-    finally show "\<bar>f x\<bar> \<le> \<parallel>f\<parallel>V,norm * norm x" .
   qed
+  finally show ?thesis .
 qed
 
 text {*
   \medskip The function norm is the least positive real number for
   which the following inequation holds:
   \begin{center}
-  @{text "\<bar>f x\<bar> \<le> c \<cdot> \<parallel>x\<parallel>"}
+    @{text "\<bar>f x\<bar> \<le> c \<cdot> \<parallel>x\<parallel>"}
   \end{center}
 *}
 
-lemma fnorm_le_ub:
-  "is_continuous V norm f \<Longrightarrow> is_normed_vectorspace V norm \<Longrightarrow>
-     \<forall>x \<in> V. \<bar>f x\<bar> \<le> c * norm x \<Longrightarrow> 0 \<le> c
-  \<Longrightarrow> \<parallel>f\<parallel>V,norm \<le> c"
-proof (unfold function_norm_def)
-  assume "is_normed_vectorspace V norm"
-  assume c: "is_continuous V norm f"
-  assume fb: "\<forall>x \<in> V. \<bar>f x\<bar> \<le> c * norm x"
-    and "0 \<le> c"
-
-  txt {* Suppose the inequation holds for some @{text "c \<ge> 0"}.  If
-  @{text c} is an upper bound of @{text B}, then @{text c} is greater
-  than the function norm since the function norm is the least upper
-  bound.  *}
-
-  show "Sup UNIV (B V norm f) \<le> c"
-  proof (rule sup_le_ub)
-    from ex_fnorm [OF _ c]
-    show "is_Sup UNIV (B V norm f) (Sup UNIV (B V norm f))"
-      by (simp! add: is_function_norm_def function_norm_def)
-
-    txt {* @{text c} is an upper bound of @{text B}, i.e. every
-    @{text "y \<in> B"} is less than @{text c}. *}
-
-    show "isUb UNIV (B V norm f) c"
-    proof (intro isUbI setleI ballI)
-      fix y assume "y \<in> B V norm f"
-      thus le: "y \<le> c"
-      proof (unfold B_def, elim UnE CollectE exE conjE singletonE)
-
-       txt {* The first case for @{text "y \<in> B"} is @{text "y = 0"}. *}
-
-        assume "y = 0"
-        show "y \<le> c" by (blast!)
-
-        txt{* The second case is @{text "y = \<bar>f x\<bar> / \<parallel>x\<parallel>"} for some
-        @{text "x \<in> V"} with @{text "x \<noteq> 0"}. *}
-
-      next
-        fix x
-        assume "x \<in> V"  "x \<noteq> 0"
-
-        have lz: "0 < norm x"
-          by (simp! add: normed_vs_norm_gt_zero)
-
-        have nz: "norm x \<noteq> 0"
-        proof (rule not_sym)
-          from lz show "0 \<noteq> norm x"
-            by (simp! add: order_less_imp_not_eq)
-        qed
-
-        from lz have "0 < inverse (norm x)"
-          by (simp! add: real_inverse_gt_0)
-        hence inverse_gez: "0 \<le> inverse (norm x)"
-          by (rule order_less_imp_le)
-
-        assume "y = \<bar>f x\<bar> * inverse (norm x)"
-        also from inverse_gez have "... \<le> c * norm x * inverse (norm x)"
-          proof (rule real_mult_le_le_mono2)
-            show "\<bar>f x\<bar> \<le> c * norm x" by (rule bspec)
-          qed
-        also have "... \<le> c" by (simp add: nz real_mult_assoc)
-        finally show ?thesis .
-      qed
-    qed blast
+lemma (in functional_vectorspace) function_norm_least [intro?]:
+  includes continuous
+  assumes ineq: "\<forall>x \<in> V. \<bar>f x\<bar> \<le> c * \<parallel>x\<parallel>" and ge: "0 \<le> c"
+  shows "\<parallel>f\<parallel>\<hyphen>V \<le> c"
+proof (rule function_norm_least)
+  fix b assume b: "b \<in> B V f"
+  show "b \<le> c"
+  proof cases
+    assume "b = 0"
+    with ge show ?thesis by simp
+  next
+    assume "b \<noteq> 0"
+    with b obtain x where b_rep: "b = \<bar>f x\<bar> * inverse \<parallel>x\<parallel>"
+        and x_neq: "x \<noteq> 0" and x: "x \<in> V"
+      by (auto simp add: B_def real_divide_def)
+    note b_rep
+    also have "\<bar>f x\<bar> * inverse \<parallel>x\<parallel> \<le> (c * \<parallel>x\<parallel>) * inverse \<parallel>x\<parallel>"
+    proof (rule real_mult_le_le_mono2)
+      have "0 < \<parallel>x\<parallel>" ..
+      then show "0 \<le> inverse \<parallel>x\<parallel>" by simp
+      from ineq and x show "\<bar>f x\<bar> \<le> c * \<parallel>x\<parallel>" ..
+    qed
+    also have "\<dots> = c"
+    proof -
+      from x_neq and x have "\<parallel>x\<parallel> \<noteq> 0" by simp
+      then show ?thesis by simp
+    qed
+    finally show ?thesis .
   qed
 qed
 
+lemmas [iff?] =
+  functional_vectorspace.function_norm_ge_zero
+  functional_vectorspace.function_norm_le_cong
+  functional_vectorspace.function_norm_least
+
 end
diff -r cc3bbaf1b8d3 -r a6a7025fd7e8 src/HOL/Real/HahnBanach/FunctionOrder.thy
--- a/src/HOL/Real/HahnBanach/FunctionOrder.thy	Thu Aug 22 12:28:41 2002 +0200
+++ b/src/HOL/Real/HahnBanach/FunctionOrder.thy	Thu Aug 22 20:49:43 2002 +0200
@@ -20,79 +20,78 @@
   graph.
 *}
 
-types 'a graph = "('a * real) set"
+types 'a graph = "('a \<times> real) set"
 
 constdefs
-  graph :: "'a set \<Rightarrow> ('a \<Rightarrow> real) \<Rightarrow> 'a graph "
+  graph :: "'a set \<Rightarrow> ('a \<Rightarrow> real) \<Rightarrow> 'a graph"
   "graph F f \<equiv> {(x, f x) | x. x \<in> F}"
 
-lemma graphI [intro?]: "x \<in> F \<Longrightarrow> (x, f x) \<in> graph F f"
+lemma graphI [intro]: "x \<in> F \<Longrightarrow> (x, f x) \<in> graph F f"
   by (unfold graph_def) blast
 
-lemma graphI2 [intro?]: "x \<in> F \<Longrightarrow> \<exists>t\<in> (graph F f). t = (x, f x)"
+lemma graphI2 [intro?]: "x \<in> F \<Longrightarrow> \<exists>t \<in> graph F f. t = (x, f x)"
   by (unfold graph_def) blast
 
-lemma graphD1 [intro?]: "(x, y) \<in> graph F f \<Longrightarrow> x \<in> F"
-  by (unfold graph_def) blast
-
-lemma graphD2 [intro?]: "(x, y) \<in> graph H h \<Longrightarrow> y = h x"
+lemma graphE [elim?]:
+    "(x, y) \<in> graph F f \<Longrightarrow> (x \<in> F \<Longrightarrow> y = f x \<Longrightarrow> C) \<Longrightarrow> C"
   by (unfold graph_def) blast
 
 
 subsection {* Functions ordered by domain extension *}
 
-text {* A function @{text h'} is an extension of @{text h}, iff the
-  graph of @{text h} is a subset of the graph of @{text h'}. *}
+text {*
+  A function @{text h'} is an extension of @{text h}, iff the graph of
+  @{text h} is a subset of the graph of @{text h'}.
+*}
 
 lemma graph_extI:
   "(\<And>x. x \<in> H \<Longrightarrow> h x = h' x) \<Longrightarrow> H \<subseteq> H'
-  \<Longrightarrow> graph H h \<subseteq> graph H' h'"
+    \<Longrightarrow> graph H h \<subseteq> graph H' h'"
   by (unfold graph_def) blast
 
-lemma graph_extD1 [intro?]:
+lemma graph_extD1 [dest?]:
   "graph H h \<subseteq> graph H' h' \<Longrightarrow> x \<in> H \<Longrightarrow> h x = h' x"
   by (unfold graph_def) blast
 
-lemma graph_extD2 [intro?]:
+lemma graph_extD2 [dest?]:
   "graph H h \<subseteq> graph H' h' \<Longrightarrow> H \<subseteq> H'"
   by (unfold graph_def) blast
 
+
 subsection {* Domain and function of a graph *}
 
 text {*
-  The inverse functions to @{text graph} are @{text domain} and
-  @{text funct}.
+  The inverse functions to @{text graph} are @{text domain} and @{text
+  funct}.
 *}
 
 constdefs
-  domain :: "'a graph \<Rightarrow> 'a set"
+  "domain" :: "'a graph \<Rightarrow> 'a set"
   "domain g \<equiv> {x. \<exists>y. (x, y) \<in> g}"
 
   funct :: "'a graph \<Rightarrow> ('a \<Rightarrow> real)"
   "funct g \<equiv> \<lambda>x. (SOME y. (x, y) \<in> g)"
 
-
 text {*
   The following lemma states that @{text g} is the graph of a function
   if the relation induced by @{text g} is unique.
 *}
 
 lemma graph_domain_funct:
-  "(\<And>x y z. (x, y) \<in> g \<Longrightarrow> (x, z) \<in> g \<Longrightarrow> z = y)
-  \<Longrightarrow> graph (domain g) (funct g) = g"
-proof (unfold domain_def funct_def graph_def, auto)
+  assumes uniq: "\<And>x y z. (x, y) \<in> g \<Longrightarrow> (x, z) \<in> g \<Longrightarrow> z = y"
+  shows "graph (domain g) (funct g) = g"
+proof (unfold domain_def funct_def graph_def, auto)  (* FIXME !? *)
   fix a b assume "(a, b) \<in> g"
   show "(a, SOME y. (a, y) \<in> g) \<in> g" by (rule someI2)
   show "\<exists>y. (a, y) \<in> g" ..
-  assume uniq: "\<And>x y z. (x, y) \<in> g \<Longrightarrow> (x, z) \<in> g \<Longrightarrow> z = y"
   show "b = (SOME y. (a, y) \<in> g)"
   proof (rule some_equality [symmetric])
-    fix y assume "(a, y) \<in> g" show "y = b" by (rule uniq)
+    fix y assume "(a, y) \<in> g"
+    show "y = b" by (rule uniq)
   qed
 qed
 
 
-
 subsection {* Norm-preserving extensions of a function *}
 
 text {*
@@ -105,39 +104,35 @@
 constdefs
   norm_pres_extensions ::
     "'a::{plus, minus, zero} set \<Rightarrow> ('a \<Rightarrow> real) \<Rightarrow> 'a set \<Rightarrow> ('a \<Rightarrow> real)
-    \<Rightarrow> 'a graph set"
+      \<Rightarrow> 'a graph set"
     "norm_pres_extensions E p F f
-    \<equiv> {g. \<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)}"
+      \<equiv> {g. \<exists>H h. g = 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)}"
 
-lemma norm_pres_extension_D:
+lemma norm_pres_extensionE [elim]:
   "g \<in> norm_pres_extensions E p F f
-  \<Longrightarrow> \<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)"
+  \<Longrightarrow> (\<And>H h. g = graph H h \<Longrightarrow> linearform H h
+        \<Longrightarrow> H \<unlhd> E \<Longrightarrow> F \<unlhd> H \<Longrightarrow> graph F f \<subseteq> graph H h
+        \<Longrightarrow> \<forall>x \<in> H. h x \<le> p x \<Longrightarrow> C) \<Longrightarrow> C"
   by (unfold norm_pres_extensions_def) blast
 
 lemma norm_pres_extensionI2 [intro]:
-  "is_linearform H h \<Longrightarrow> is_subspace H E \<Longrightarrow> is_subspace F H \<Longrightarrow>
-  graph F f \<subseteq> graph H h \<Longrightarrow> \<forall>x \<in> H. h x \<le> p x
-  \<Longrightarrow> (graph H h \<in> norm_pres_extensions E p F f)"
- by (unfold norm_pres_extensions_def) blast
+  "linearform H h \<Longrightarrow> H \<unlhd> E \<Longrightarrow> F \<unlhd> H
+    \<Longrightarrow> graph F f \<subseteq> graph H h \<Longrightarrow> \<forall>x \<in> H. h x \<le> p x
+    \<Longrightarrow> graph H h \<in> norm_pres_extensions E p F f"
+  by (unfold norm_pres_extensions_def) blast
 
-lemma norm_pres_extensionI [intro]:
-  "\<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)
-  \<Longrightarrow> g \<in> norm_pres_extensions E p F f"
+lemma norm_pres_extensionI:  (* FIXME ? *)
+  "\<exists>H h. g = 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) \<Longrightarrow> g \<in> norm_pres_extensions E p F f"
   by (unfold norm_pres_extensions_def) blast
 
 end
diff -r cc3bbaf1b8d3 -r a6a7025fd7e8 src/HOL/Real/HahnBanach/HahnBanach.thy
--- a/src/HOL/Real/HahnBanach/HahnBanach.thy	Thu Aug 22 12:28:41 2002 +0200
+++ b/src/HOL/Real/HahnBanach/HahnBanach.thy	Thu Aug 22 20:49:43 2002 +0200
@@ -49,251 +49,235 @@
   \item Thus @{text g} can not be maximal. Contradiction!
 
   \end{itemize}
-
   \end{enumerate}
 *}
 
 theorem HahnBanach:
-  "is_vectorspace E \<Longrightarrow> is_subspace F E \<Longrightarrow> is_seminorm E p
-  \<Longrightarrow> is_linearform F f \<Longrightarrow> \<forall>x \<in> F. f x \<le> p x
-  \<Longrightarrow> \<exists>h. is_linearform E h \<and> (\<forall>x \<in> F. h x = f x) \<and> (\<forall>x \<in> E. h x \<le> p x)"
+  includes vectorspace E + subvectorspace F E +
+    seminorm_vectorspace E p + linearform F f
+  assumes fp: "\<forall>x \<in> F. f x \<le> p x"
+  shows "\<exists>h. linearform E h \<and> (\<forall>x \<in> F. h x = f x) \<and> (\<forall>x \<in> E. h x \<le> p x)"
     -- {* Let @{text E} be a vector space, @{text F} a subspace of @{text E}, @{text p} a seminorm on @{text E}, *}
     -- {* 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 -
-  assume "is_vectorspace E"  "is_subspace F E"  "is_seminorm E p"
-   and "is_linearform F f"  "\<forall>x \<in> F. f x \<le> p x"
-  -- {* Assume the context of the theorem. \skp *}
   def M \<equiv> "norm_pres_extensions E p F f"
-  -- {* Define @{text M} as the set of all norm-preserving extensions of @{text F}. \skp *}
+  hence M: "M = \<dots>" by (simp only:)
+  have F: "vectorspace F" ..
   {
-    fix c assume "c \<in> chain M"  "\<exists>x. x \<in> c"
+    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"}. *}
+      -- {* 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"}. *}
     proof (unfold M_def, rule norm_pres_extensionI)
-      show "\<exists>H h. graph H h = \<Union>c
-              \<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)"
-      proof (intro exI conjI)
-        let ?H = "domain (\<Union>c)"
-        let ?h = "funct (\<Union>c)"
+      let ?H = "domain (\<Union>c)"
+      let ?h = "funct (\<Union>c)"
 
-        show a: "graph ?H ?h = \<Union>c"
-        proof (rule graph_domain_funct)
-          fix x y z assume "(x, y) \<in> \<Union>c"  "(x, z) \<in> \<Union>c"
-          show "z = y" by (rule sup_definite)
-        qed
-        show "is_linearform ?H ?h"
-          by (simp! add: sup_lf a)
-        show "is_subspace ?H E"
-          by (rule sup_subE, rule a) (simp!)+
-        show "is_subspace F ?H"
-          by (rule sup_supF, rule a) (simp!)+
-        show "graph F f \<subseteq> graph ?H ?h"
-          by (rule sup_ext, rule a) (simp!)+
-        show "\<forall>x \<in> ?H. ?h x \<le> p x"
-          by (rule sup_norm_pres, rule a) (simp!)+
+      have a: "graph ?H ?h = \<Union>c"
+      proof (rule graph_domain_funct)
+        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"
+        by (rule sup_subE)
+      moreover from a M cM ex 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)
+      ultimately show "\<exists>H h. \<Union>c = 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)" by blast
     qed
-
   }
   hence "\<exists>g \<in> M. \<forall>x \<in> M. g \<subseteq> x \<longrightarrow> g = x"
   -- {* 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: *}
-    have "graph F f \<in> norm_pres_extensions E p F f"
-    proof (rule norm_pres_extensionI2)
-      have "is_vectorspace F" ..
-      thus "is_subspace F F" ..
-    qed (blast!)+
-    thus "graph F f \<in> M" by (simp!)
+      -- {* 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" .
+      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
-  thus ?thesis
-  proof
-    fix g assume "g \<in> M"  "\<forall>x \<in> M. g \<subseteq> x \<longrightarrow> g = x"
-    -- {* We consider such a maximal element @{text "g \<in> M"}. \skp *}
-    obtain H h where "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"
+  then obtain g where gM: "g \<in> M" and "\<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 *}
-    proof -
-      have "\<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 (simp! add: norm_pres_extension_D)
-      with that show ?thesis by blast
-    qed
-    have h: "is_vectorspace H" ..
-    have "H = E"
+  from HE have H: "vectorspace H"
+    by (rule subvectorspace.vectorspace)
+
+  have HE_eq: "H = E"
     -- {* We show that @{text h} is defined on whole @{text E} by classical contradiction. \skp *}
-    proof (rule classical)
-      assume "H \<noteq> E"
+  proof (rule classical)
+    assume neq: "H \<noteq> E"
       -- {* Assume @{text h} is not defined on whole @{text E}. Then show that @{text h} can be extended *}
       -- {* in a norm-preserving way to a function @{text h'} with the graph @{text g'}. \skp *}
-      have "\<exists>g' \<in> M. g \<subseteq> g' \<and> g \<noteq> g'"
-      proof -
-        obtain x' where "x' \<in> E"  "x' \<notin> H"
-        -- {* Pick @{text "x' \<in> E - H"}. \skp *}
-        proof -
-          have "\<exists>x' \<in> E. x' \<notin> H"
-          proof (rule set_less_imp_diff_not_empty)
-            have "H \<subseteq> E" ..
-            thus "H \<subset> E" ..
-          qed
-          with that show ?thesis by blast
+    have "\<exists>g' \<in> M. g \<subseteq> g' \<and> g \<noteq> g'"
+    proof -
+      from HE have "H \<subseteq> E" ..
+      with neq obtain x' where x'E: "x' \<in> E" and "x' \<notin> H" by blast
+      obtain x': "x' \<noteq> 0"
+      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
         qed
-        have x': "x' \<noteq> 0"
-        proof (rule classical)
-          presume "x' = 0"
-          with h have "x' \<in> H" by simp
-          thus ?thesis by contradiction
-        qed blast
-        def H' \<equiv> "H + lin x'"
+      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 *}
-        obtain xi where "\<forall>y \<in> H. - p (y + x') - h y \<le> xi
-                          \<and> xi \<le> p (y + x') - h y"
+      have HH': "H \<unlhd> H'"
+      proof (unfold H'_def)
+        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
+          \<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 -
+        from H have "\<exists>xi. \<forall>y \<in> H. - p (y + x') - h y \<le> xi
+            \<and> xi \<le> p (y + x') - h y"
+        proof (rule ex_xi)
+          fix u v assume u: "u \<in> H" and v: "v \<in> H"
+          with HE have uE: "u \<in> E" and vE: "v \<in> E" by auto
+          from H u v linearform have "h v - h u = h (v - u)"
+            by (simp add: vectorspace_linearform.diff)
+          also from hp and H u v have "\<dots> \<le> p (v - u)"
+            by (simp only: vectorspace.diff_closed)
+          also from x'E uE vE have "v - u = x' + - x' + v + - u"
+            by (simp add: diff_eq1)
+          also from x'E uE vE have "\<dots> = v + x' + - (u + x')"
+            by (simp add: add_ac)
+          also from x'E uE vE have "\<dots> = (v + x') - (u + x')"
+            by (simp add: diff_eq1)
+          also from x'E uE vE 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 ..
+      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 *}
+
+      have "g \<subseteq> graph H' h' \<and> g \<noteq> graph H' h'"
+        -- {* @{text h'} is an extension of @{text h} \dots \skp *}
+      proof
+        show "g \<subseteq> graph H' h'"
         proof -
-          from h have "\<exists>xi. \<forall>y \<in> H. - p (y + x') - h y \<le> xi
-                          \<and> xi \<le> p (y + x') - h y"
-          proof (rule ex_xi)
-            fix u v assume "u \<in> H"  "v \<in> H"
-            from h have "h v - h u = h (v - u)"
-              by (simp! add: linearform_diff)
-            also have "... \<le> p (v - u)"
-              by (simp!)
-            also have "v - u = x' + - x' + v + - u"
-              by (simp! add: diff_eq1)
-            also have "... = v + x' + - (u + x')"
-              by (simp!)
-            also have "... = (v + x') - (u + x')"
-              by (simp! add: diff_eq1)
-            also have "p ... \<le> p (v + x') + p (u + x')"
-              by (rule seminorm_diff_subadditive) (simp_all!)
-            finally have "h v - h u \<le> p (v + x') + p (u + x')" .
-
-            thus "- p (u + x') - h u \<le> p (v + x') - h v"
-              by (rule real_diff_ineq_swap)
+          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)
+            with h'_def show "h t = h' t" by (simp add: Let_def)
+          next
+            from HH' show "H \<subseteq> H'" ..
           qed
-          thus ?thesis ..
+          with g_rep show ?thesis by (simp only:)
         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 ?thesis
-        proof
-          show "g \<subseteq> graph H' h' \<and> g \<noteq> graph H' h'"
-          -- {* Show that @{text h'} is an extension of @{text h} \dots \skp *}
+        show "g \<noteq> graph H' h'"
+        proof -
+          have "graph H h \<noteq> graph H' h'"
           proof
-            show "g \<subseteq> graph H' h'"
-            proof -
-              have  "graph H h \<subseteq> graph H' h'"
-              proof (rule graph_extI)
-                fix t assume "t \<in> H"
-                have "(SOME (y, a). t = y + a \<cdot> x' \<and> y \<in> H)
-                     = (t, 0)"
-                  by (rule decomp_H'_H) (assumption+, rule x')
-                thus "h t = h' t" by (simp! add: Let_def)
-              next
-                show "H \<subseteq> H'"
-                proof (rule subspace_subset)
-                  show "is_subspace H H'"
-                  proof (unfold H'_def, rule subspace_vs_sum1)
-                    show "is_vectorspace H" ..
-                    show "is_vectorspace (lin x')" ..
-                  qed
-                qed
-              qed
-              thus ?thesis by (simp!)
+            assume eq: "graph H h = graph H' h'"
+            have "x' \<in> H'"
+            proof (unfold H'_def, rule)
+              from H show "0 \<in> H" by (rule vectorspace.zero)
+              from x'E show "x' \<in> lin x'" by (rule x_lin_x)
+              from x'E show "x' = 0 + x'" by simp
             qed
-            show "g \<noteq> graph H' h'"
-            proof -
-              have "graph H h \<noteq> graph H' h'"
-              proof
-                assume e: "graph H h = graph H' h'"
-                have "x' \<in> H'"
-                proof (unfold H'_def, rule vs_sumI)
-                  show "x' = 0 + x'" by (simp!)
-                  from h show "0 \<in> H" ..
-                  show "x' \<in> lin x'" by (rule x_lin_x)
-                qed
-                hence "(x', h' x') \<in> graph H' h'" ..
-                with e have "(x', h' x') \<in> graph H h" by simp
-                hence "x' \<in> H" ..
-                thus False by contradiction
-              qed
-              thus ?thesis 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
           qed
-          show "graph H' h' \<in> M"
-          -- {* and @{text h'} is norm-preserving. \skp *}
-          proof -
-            have "graph H' h' \<in> norm_pres_extensions E p F f"
-            proof (rule norm_pres_extensionI2)
-              show "is_linearform H' h'"
-                by (rule h'_lf) (simp! add: x')+
-              show "is_subspace H' E"
-                by (unfold H'_def)
-                  (rule vs_sum_subspace [OF _ lin_subspace])
-              have "is_subspace F H" .
-              also from h lin_vs
-              have [folded H'_def]: "is_subspace H (H + lin x')" ..
-              finally (subspace_trans [OF _ h])
-              show f_h': "is_subspace F H'" .
-
-              show "graph F f \<subseteq> graph H' h'"
-              proof (rule graph_extI)
-                fix x assume "x \<in> F"
-                have "f x = h x" ..
-                also have " ... = h x + 0 * xi" by simp
-                also
-                have "... = (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)"
-                  by (rule decomp_H'_H [symmetric]) (simp! add: x')+
-                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!)
-                finally show "f x = h' x" .
-              next
-                from f_h' show "F \<subseteq> H'" ..
-              qed
-
-              show "\<forall>x \<in> H'. h' x \<le> p x"
-                by (rule h'_norm_pres) (assumption+, rule x')
-            qed
-            thus "graph H' h' \<in> M" by (simp!)
-          qed
+          with g_rep show ?thesis by simp
         qed
       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 *}
-      thus "H = E" by contradiction
+      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 "H' \<unlhd> E"
+          proof (unfold H'_def, rule)
+            show "H \<unlhd> E" .
+            show "vectorspace E" .
+            from x'E show "lin x' \<unlhd> E" ..
+          qed
+          have "F \<unlhd> H" .
+          from H this 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)"
+            proof (rule decomp_H'_H [symmetric])
+              from FH x show "x \<in> H" ..
+              from x' show "x' \<noteq> 0" .
+            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)
+        qed
+      qed
+      ultimately show ?thesis ..
     qed
-    thus "\<exists>h. is_linearform E h \<and> (\<forall>x \<in> F. h x = f x)
-      \<and> (\<forall>x \<in> E. h x \<le> p x)"
-    proof (intro exI conjI)
-      assume eq: "H = E"
-      from eq show "is_linearform E h" by (simp!)
-      show "\<forall>x \<in> F. h x = f x"
-      proof
-        fix x assume "x \<in> F" have "f x = h x " ..
-        thus "h x = f x" ..
-      qed
-      from eq show "\<forall>x \<in> E. h x \<le> p x" by (blast!)
-    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
   qed
+
+  from HE_eq and linearform have "linearform E h"
+    by (simp only:)
+  moreover have "\<forall>x \<in> F. h x = f x"
+  proof
+    fix x assume "x \<in> F"
+    with graphs have "f x = h x" ..
+    then show "h x = f x" ..
+  qed
+  moreover from HE_eq and hp have "\<forall>x \<in> E. h x \<le> p x"
+    by (simp only:)
+  ultimately show ?thesis by blast
 qed
 
 
@@ -314,26 +298,28 @@
 *}
 
 theorem abs_HahnBanach:
-  "is_vectorspace E \<Longrightarrow> is_subspace F E \<Longrightarrow> is_linearform F f
-  \<Longrightarrow> is_seminorm E p \<Longrightarrow> \<forall>x \<in> F. \<bar>f x\<bar> \<le> p x
-  \<Longrightarrow> \<exists>g. is_linearform E g \<and> (\<forall>x \<in> F. g x = f x)
+  includes vectorspace E + subvectorspace F E +
+    linearform F f + seminorm_vectorspace E p
+  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 -
-assume "is_vectorspace E"  "is_subspace F E"  "is_seminorm E p"
-"is_linearform F f"  "\<forall>x \<in> F. \<bar>f x\<bar> \<le> p x"
-have "\<forall>x \<in> F. f x \<le> p x"  by (rule abs_ineq_iff [THEN iffD1])
-hence "\<exists>g. is_linearform E g \<and> (\<forall>x \<in> F. g x = f x)
-          \<and> (\<forall>x \<in> E. g x \<le> p x)"
-by (simp! only: HahnBanach)
-thus ?thesis
-proof (elim exE conjE)
-fix g assume "is_linearform E g"  "\<forall>x \<in> F. g x = f x"
-              "\<forall>x \<in> E. g x \<le> p x"
-hence "\<forall>x \<in> E. \<bar>g x\<bar> \<le> p x"
-  by (simp! add: abs_ineq_iff [OF subspace_refl])
-thus ?thesis by (intro exI conjI)
+  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)"
+  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
+  have "\<forall>x \<in> E. \<bar>g x\<bar> \<le> p x"
+  proof (rule abs_ineq_iff [THEN iffD2])
+    show "E \<unlhd> E" ..
+  qed
+  with * show ?thesis by blast
 qed
-qed
+
 
 subsection {* The Hahn-Banach Theorem for normed spaces *}
 
@@ -344,126 +330,108 @@
 *}
 
 theorem norm_HahnBanach:
-  "is_normed_vectorspace E norm \<Longrightarrow> is_subspace F E
-  \<Longrightarrow> is_linearform F f \<Longrightarrow> is_continuous F norm f
-  \<Longrightarrow> \<exists>g. is_linearform E g
-     \<and> is_continuous E norm g
+  includes functional_vectorspace E + subvectorspace F E +
+    linearform F f + continuous F norm f
+  shows "\<exists>g. linearform E g
+     \<and> continuous E norm g
      \<and> (\<forall>x \<in> F. g x = f x)
-     \<and> \<parallel>g\<parallel>E,norm = \<parallel>f\<parallel>F,norm"
-proof -
-assume e_norm: "is_normed_vectorspace E norm"
-assume f: "is_subspace F E"  "is_linearform F f"
-assume f_cont: "is_continuous F norm f"
-have e: "is_vectorspace E" ..
-hence f_norm: "is_normed_vectorspace F norm" ..
-
-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>F,norm * norm x"
-
-txt {* @{text p} is a seminorm on @{text E}: *}
-
-have q: "is_seminorm E p"
-proof
-fix x y a assume "x \<in> E"  "y \<in> E"
-
-txt {* @{text p} is positive definite: *}
-
-show "0 \<le> p x"
-proof (unfold p_def, rule real_le_mult_order1a)
-  from f_cont f_norm show "0 \<le> \<parallel>f\<parallel>F,norm" ..
-  show "0 \<le> norm x" ..
-qed
-
-txt {* @{text p} is absolutely homogenous: *}
-
-show "p (a \<cdot> x) = \<bar>a\<bar> * p x"
-proof -
-  have "p (a \<cdot> x) = \<parallel>f\<parallel>F,norm * norm (a \<cdot> x)"
-    by (simp!)
-  also have "norm (a \<cdot> x) = \<bar>a\<bar> * norm x"
-    by (rule normed_vs_norm_abs_homogenous)
-  also have "\<parallel>f\<parallel>F,norm * (\<bar>a\<bar> * norm x )
-    = \<bar>a\<bar> * (\<parallel>f\<parallel>F,norm * norm x)"
-    by (simp! only: real_mult_left_commute)
-  also have "... = \<bar>a\<bar> * p x" by (simp!)
-  finally show ?thesis .
-qed
-
-txt {* Furthermore, @{text p} is subadditive: *}
-
-show "p (x + y) \<le> p x + p y"
+     \<and> \<parallel>g\<parallel>\<hyphen>E = \<parallel>f\<parallel>\<hyphen>F"
 proof -
-  have "p (x + y) = \<parallel>f\<parallel>F,norm * norm (x + y)"
-    by (simp!)
-  also
-  have "... \<le> \<parallel>f\<parallel>F,norm * (norm x + norm y)"
-  proof (rule real_mult_le_le_mono1a)
-    from f_cont f_norm show "0 \<le> \<parallel>f\<parallel>F,norm" ..
-    show "norm (x + y) \<le> norm x + norm y" ..
-  qed
-  also have "... = \<parallel>f\<parallel>F,norm * norm x
-                    + \<parallel>f\<parallel>F,norm * norm y"
-    by (simp! only: real_add_mult_distrib2)
-  finally show ?thesis by (simp!)
-qed
-qed
+  have E: "vectorspace E" .
+  have E_norm: "normed_vectorspace E norm" ..
+  have FE: "F \<unlhd> E" .
+  have F: "vectorspace F" ..
+  have linearform: "linearform F f" .
+  have F_norm: "normed_vectorspace F norm" ..
+
+  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}: *}
+  have q: "seminorm E p"
+  proof
+    fix x y a assume x: "x \<in> E" and y: "y \<in> E"
 
-txt {* @{text f} is bounded by @{text p}. *}
+    txt {* @{text p} is positive definite: *}
+    show "0 \<le> p x"
+    proof (unfold p_def, rule real_le_mult_order1a)
+      show "0 \<le> \<parallel>f\<parallel>\<hyphen>F"
+        apply (unfold function_norm_def B_def)
+        using normed_vectorspace.axioms [OF F_norm] ..
+      from x show "0 \<le> \<parallel>x\<parallel>" ..
+    qed
+
+    txt {* @{text p} is absolutely homogenous: *}
 
-have "\<forall>x \<in> F. \<bar>f x\<bar> \<le> p x"
-proof
-fix x assume "x \<in> F"
- from f_norm show "\<bar>f x\<bar> \<le> p x"
-   by (simp! add: norm_fx_le_norm_f_norm_x)
-qed
+    show "p (a \<cdot> x) = \<bar>a\<bar> * p x"
+    proof -
+      have "p (a \<cdot> x) = \<parallel>f\<parallel>\<hyphen>F * \<parallel>a \<cdot> x\<parallel>"
+        by (simp only: p_def)
+      also from x have "\<parallel>a \<cdot> x\<parallel> = \<bar>a\<bar> * \<parallel>x\<parallel>"
+        by (rule abs_homogenous)
+      also have "\<parallel>f\<parallel>\<hyphen>F * (\<bar>a\<bar> * \<parallel>x\<parallel>) = \<bar>a\<bar> * (\<parallel>f\<parallel>\<hyphen>F * \<parallel>x\<parallel>)"
+        by simp
+      also have "\<dots> = \<bar>a\<bar> * p x"
+        by (simp only: p_def)
+      finally show ?thesis .
+    qed
+
+    txt {* Furthermore, @{text p} is subadditive: *}
 
-txt {*
-  Using the fact that @{text p} is a seminorm and @{text f} is bounded
-  by @{text p} we can apply the Hahn-Banach Theorem for real vector
-  spaces. So @{text f} can be extended in a norm-preserving way to
-  some function @{text g} on the whole vector space @{text E}.
-*}
+    show "p (x + y) \<le> p x + p y"
+    proof -
+      have "p (x + y) = \<parallel>f\<parallel>\<hyphen>F * \<parallel>x + y\<parallel>"
+        by (simp only: p_def)
+      also have "\<dots> \<le> \<parallel>f\<parallel>\<hyphen>F * (\<parallel>x\<parallel> + \<parallel>y\<parallel>)"
+      proof (rule real_mult_le_le_mono1a)
+        show "0 \<le> \<parallel>f\<parallel>\<hyphen>F"
+          apply (unfold function_norm_def B_def)
+          using normed_vectorspace.axioms [OF F_norm] ..  (* FIXME *)
+        from x y show "\<parallel>x + y\<parallel> \<le> \<parallel>x\<parallel> + \<parallel>y\<parallel>" ..
+      qed
+      also have "\<dots> = \<parallel>f\<parallel>\<hyphen>F * \<parallel>x\<parallel> + \<parallel>f\<parallel>\<hyphen>F * \<parallel>y\<parallel>"
+        by (simp only: real_add_mult_distrib2)
+      also have "\<dots> = p x + p y"
+        by (simp only: p_def)
+      finally show ?thesis .
+    qed
+  qed
 
-with e f q
-have "\<exists>g. is_linearform E g \<and> (\<forall>x \<in> F. g x = f x)
-        \<and> (\<forall>x \<in> E. \<bar>g x\<bar> \<le> p x)"
-by (simp! add: abs_HahnBanach)
+  txt {* @{text f} is bounded by @{text p}. *}
 
-thus ?thesis
-proof (elim exE conjE)
-fix g
-assume "is_linearform E g" and a: "\<forall>x \<in> F. g x = f x"
-   and b: "\<forall>x \<in> E. \<bar>g x\<bar> \<le> p x"
+  have "\<forall>x \<in> F. \<bar>f x\<bar> \<le> p x"
+  proof
+    fix x assume "x \<in> F"
+    show "\<bar>f x\<bar> \<le> p x"
+      apply (unfold p_def function_norm_def B_def)
+      using normed_vectorspace.axioms [OF F_norm] .. (* FIXME *)
+  qed
 
-show "\<exists>g. is_linearform E g
-        \<and> is_continuous E norm g
-        \<and> (\<forall>x \<in> F. g x = f x)
-        \<and> \<parallel>g\<parallel>E,norm = \<parallel>f\<parallel>F,norm"
-proof (intro exI conjI)
+  txt {* Using the fact that @{text p} is a seminorm and @{text f} is bounded
+    by @{text p} we can apply the Hahn-Banach Theorem for real vector
+    spaces. So @{text f} can be extended in a norm-preserving way to
+    some function @{text g} on the whole vector space @{text E}. *}
 
-txt {*
-  We furthermore have to show that @{text g} is also continuous:
-*}
+  with E FE linearform q obtain g where
+        linearformE: "linearform E g"
+      and a: "\<forall>x \<in> F. g x = f x"
+      and b: "\<forall>x \<in> E. \<bar>g x\<bar> \<le> p x"
+    by (rule abs_HahnBanach [elim_format]) rules
 
-  show g_cont: "is_continuous E norm g"
+  txt {* We furthermore have to show that @{text g} is also continuous: *}
+
+  have g_cont: "continuous E norm g" using linearformE
   proof
     fix x assume "x \<in> E"
-    with b show "\<bar>g x\<bar> \<le> \<parallel>f\<parallel>F,norm * norm x"
-      by (simp add: p_def)
+    with b show "\<bar>g x\<bar> \<le> \<parallel>f\<parallel>\<hyphen>F * \<parallel>x\<parallel>"
+      by (simp only: p_def)
   qed
 
-  txt {*
-    To complete the proof, we show that
-    @{text "\<parallel>g\<parallel> = \<parallel>f\<parallel>"}. \label{order_antisym} *}
+  txt {* To complete the proof, we show that @{text "\<parallel>g\<parallel> = \<parallel>f\<parallel>"}. *}
 
-  show "\<parallel>g\<parallel>E,norm = \<parallel>f\<parallel>F,norm"
-    (is "?L = ?R")
+  have "\<parallel>g\<parallel>\<hyphen>E = \<parallel>f\<parallel>\<hyphen>F"
   proof (rule order_antisym)
-
     txt {*
       First we show @{text "\<parallel>g\<parallel> \<le> \<parallel>f\<parallel>"}.  The function norm @{text
       "\<parallel>g\<parallel>"} is defined as the smallest @{text "c \<in> \<real>"} such that
@@ -480,40 +448,51 @@
       \end{center}
     *}
 
-    have "\<forall>x \<in> E. \<bar>g x\<bar> \<le> \<parallel>f\<parallel>F,norm * norm x"
+    have "\<forall>x \<in> E. \<bar>g x\<bar> \<le> \<parallel>f\<parallel>\<hyphen>F * \<parallel>x\<parallel>"
     proof
       fix x assume "x \<in> E"
-      show "\<bar>g x\<bar> \<le> \<parallel>f\<parallel>F,norm * norm x"
-        by (simp!)
-    qed
-
-    with g_cont e_norm show "?L \<le> ?R"
-    proof (rule fnorm_le_ub)
-      from f_cont f_norm show "0 \<le> \<parallel>f\<parallel>F,norm" ..
+      with b show "\<bar>g x\<bar> \<le> \<parallel>f\<parallel>\<hyphen>F * \<parallel>x\<parallel>"
+        by (simp only: p_def)
     qed
-
-    txt{* The other direction is achieved by a similar
-    argument. *}
+    show "\<parallel>g\<parallel>\<hyphen>E \<le> \<parallel>f\<parallel>\<hyphen>F"
+      apply (unfold function_norm_def B_def)
+      apply rule
+      apply (rule normed_vectorspace.axioms [OF E_norm])+
+      apply (rule continuous.axioms [OF g_cont])+
+      apply (rule b [unfolded p_def function_norm_def B_def])
+      using normed_vectorspace.axioms [OF F_norm] ..  (* FIXME *)
 
-    have "\<forall>x \<in> F. \<bar>f x\<bar> \<le> \<parallel>g\<parallel>E,norm * norm x"
+    txt {* The other direction is achieved by a similar argument. *}
+
+    have ** : "\<forall>x \<in> F. \<bar>f x\<bar> \<le> \<parallel>g\<parallel>\<hyphen>E * \<parallel>x\<parallel>"
     proof
-      fix x assume "x \<in> F"
+      fix x assume x: "x \<in> F"
       from a have "g x = f x" ..
-      hence "\<bar>f x\<bar> = \<bar>g x\<bar>" by simp
-      also from g_cont
-      have "... \<le> \<parallel>g\<parallel>E,norm * norm x"
-      proof (rule norm_fx_le_norm_f_norm_x)
-        show "x \<in> E" ..
+      hence "\<bar>f x\<bar> = \<bar>g x\<bar>" by (simp only:)
+      also have "\<dots> \<le> \<parallel>g\<parallel>\<hyphen>E * \<parallel>x\<parallel>"
+        apply (unfold function_norm_def B_def)
+        apply rule
+        apply (rule normed_vectorspace.axioms [OF E_norm])+
+        apply (rule continuous.axioms [OF g_cont])+
+      proof -
+        from FE x show "x \<in> E" ..
       qed
-      finally show "\<bar>f x\<bar> \<le> \<parallel>g\<parallel>E,norm * norm x" .
+      finally show "\<bar>f x\<bar> \<le> \<parallel>g\<parallel>\<hyphen>E * \<parallel>x\<parallel>" .
     qed
-    thus "?R \<le> ?L"
-    proof (rule fnorm_le_ub [OF f_cont f_norm])
-      from g_cont show "0 \<le> \<parallel>g\<parallel>E,norm" ..
-    qed
+    show "\<parallel>f\<parallel>\<hyphen>F \<le> \<parallel>g\<parallel>\<hyphen>E"
+      apply (unfold function_norm_def B_def)
+      apply rule
+      apply (rule normed_vectorspace.axioms [OF F_norm])+
+      apply assumption+
+      apply (rule ** [unfolded function_norm_def B_def])
+      apply rule
+      apply assumption+
+      apply (rule continuous.axioms [OF g_cont])+
+      done  (* FIXME *)
   qed
-qed
-qed
+
+  with linearformE a g_cont show ?thesis
+    by blast
 qed
 
 end
diff -r cc3bbaf1b8d3 -r a6a7025fd7e8 src/HOL/Real/HahnBanach/HahnBanachExtLemmas.thy
--- a/src/HOL/Real/HahnBanach/HahnBanachExtLemmas.thy	Thu Aug 22 12:28:41 2002 +0200
+++ b/src/HOL/Real/HahnBanach/HahnBanachExtLemmas.thy	Thu Aug 22 20:49:43 2002 +0200
@@ -17,17 +17,15 @@
   an element in @{text "E - H"}.  @{text H} is extended to the direct
   sum @{text "H' = H + lin x\<^sub>0"}, so for any @{text "x \<in> H'"}
   the decomposition of @{text "x = y + a \<cdot> x"} with @{text "y \<in> H"} is
-  unique. @{text h'} is defined on @{text H'} by
-  @{text "h' x = h y + a \<cdot> \<xi>"} for a certain @{text \<xi>}.
+  unique. @{text h'} is defined on @{text H'} by @{text "h' x = h y +
+  a \<cdot> \<xi>"} for a certain @{text \<xi>}.
 
   Subsequently we show some properties of this extension @{text h'} of
   @{text h}.
-*}
 
-text {*
-  This lemma will be used to show the existence of a linear extension
-  of @{text f} (see page \pageref{ex-xi-use}). It is a consequence of
-  the completeness of @{text \<real>}. To show
+  \medskip This lemma will be used to show the existence of a linear
+  extension of @{text f} (see page \pageref{ex-xi-use}). It is a
+  consequence of the completeness of @{text \<real>}. To show
   \begin{center}
   \begin{tabular}{l}
   @{text "\<exists>\<xi>. \<forall>y \<in> F. a y \<le> \<xi> \<and> \<xi> \<le> b y"}
@@ -42,307 +40,227 @@
 *}
 
 lemma ex_xi:
-  "is_vectorspace F \<Longrightarrow> (\<And>u v. u \<in> F \<Longrightarrow> v \<in> F \<Longrightarrow> a u \<le> b v)
-  \<Longrightarrow> \<exists>xi::real. \<forall>y \<in> F. a y \<le> xi \<and> xi \<le> b y"
+  includes vectorspace F
+  assumes r: "\<And>u v. u \<in> F \<Longrightarrow> v \<in> F \<Longrightarrow> a u \<le> b v"
+  shows "\<exists>xi::real. \<forall>y \<in> F. a y \<le> xi \<and> xi \<le> b y"
 proof -
-  assume vs: "is_vectorspace F"
-  assume r: "(\<And>u v. u \<in> F \<Longrightarrow> v \<in> F \<Longrightarrow> a u \<le> (b v::real))"
-
   txt {* From the completeness of the reals follows:
-  The set @{text "S = {a u. u \<in> F}"} has a supremum, if
-  it is non-empty and has an upper bound. *}
-
-  let ?S = "{a u :: real | u. u \<in> F}"
-
-  have "\<exists>xi. isLub UNIV ?S xi"
-  proof (rule reals_complete)
-
-    txt {* The set @{text S} is non-empty, since @{text "a 0 \<in> S"}: *}
-
-    from vs have "a 0 \<in> ?S" by blast
-    thus "\<exists>X. X \<in> ?S" ..
-
-    txt {* @{text "b 0"} is an upper bound of @{text S}: *}
-
-    show "\<exists>Y. isUb UNIV ?S Y"
-    proof
-      show "isUb UNIV ?S (b 0)"
-      proof (intro isUbI setleI ballI)
-        show "b 0 \<in> UNIV" ..
-      next
-
-        txt {* Every element @{text "y \<in> S"} is less than @{text "b 0"}: *}
+    The set @{text "S = {a u. u \<in> F}"} has a supremum, if it is
+    non-empty and has an upper bound. *}
 
-        fix y assume y: "y \<in> ?S"
-        from y have "\<exists>u \<in> F. y = a u" by fast
-        thus "y \<le> b 0"
-        proof
-          fix u assume "u \<in> F"
-          assume "y = a u"
-          also have "a u \<le> b 0" by (rule r) (simp!)+
-          finally show ?thesis .
-        qed
-      qed
+  let ?S = "{a u | u. u \<in> F}"
+  have "\<exists>xi. lub ?S xi"
+  proof (rule real_complete)
+    have "a 0 \<in> ?S" by blast
+    then show "\<exists>X. X \<in> ?S" ..
+    have "\<forall>y \<in> ?S. y \<le> b 0"
+    proof
+      fix y assume y: "y \<in> ?S"
+      then obtain u where u: "u \<in> F" and y: "y = a u" by blast
+      from u and zero have "a u \<le> b 0" by (rule r)
+      with y show "y \<le> b 0" by (simp only:)
     qed
+    then show "\<exists>u. \<forall>y \<in> ?S. y \<le> u" ..
   qed
-
-  thus "\<exists>xi. \<forall>y \<in> F. a y \<le> xi \<and> xi \<le> b y"
-  proof (elim exE)
-    fix xi assume "isLub UNIV ?S xi"
-    show ?thesis
-    proof (intro exI conjI ballI)
-
-      txt {* For all @{text "y \<in> F"} holds @{text "a y \<le> \<xi>"}: *}
-
-      fix y assume y: "y \<in> F"
-      show "a y \<le> xi"
-      proof (rule isUbD)
-        show "isUb UNIV ?S xi" ..
-      qed (blast!)
-    next
-
-      txt {* For all @{text "y \<in> F"} holds @{text "\<xi> \<le> b y"}: *}
-
-      fix y assume "y \<in> F"
-      show "xi \<le> b y"
-      proof (intro isLub_le_isUb isUbI setleI)
-        show "b y \<in> UNIV" ..
-        show "\<forall>ya \<in> ?S. ya \<le> b y"
-        proof
-          fix au assume au: "au \<in> ?S "
-          hence "\<exists>u \<in> F. au = a u" by fast
-          thus "au \<le> b y"
-          proof
-            fix u assume "u \<in> F" assume "au = a u"
-            also have "... \<le> b y" by (rule r)
-            finally show ?thesis .
-          qed
-        qed
-      qed
+  then obtain xi where xi: "lub ?S xi" ..
+  {
+    fix y assume "y \<in> F"
+    then have "a y \<in> ?S" by blast
+    with xi have "a y \<le> xi" by (rule lub.upper)
+  } moreover {
+    fix y assume y: "y \<in> F"
+    from xi have "xi \<le> b y"
+    proof (rule lub.least)
+      fix au assume "au \<in> ?S"
+      then obtain u where u: "u \<in> F" and au: "au = a u" by blast
+      from u y have "a u \<le> b y" by (rule r)
+      with au show "au \<le> b y" by (simp only:)
     qed
-  qed
+  } ultimately show "\<exists>xi. \<forall>y \<in> F. a y \<le> xi \<and> xi \<le> b y" by blast
 qed
 
 text {*
-  \medskip The function @{text h'} is defined as a
-  @{text "h' x = h y + a \<cdot> \<xi>"} where @{text "x = y + a \<cdot> \<xi>"} is a
-  linear extension of @{text h} to @{text H'}. *}
+  \medskip The function @{text h'} is defined as a @{text "h' x = h y
+  + a \<cdot> \<xi>"} where @{text "x = y + a \<cdot> \<xi>"} is a linear extension of
+  @{text h} to @{text H'}.
+*}
 
 lemma h'_lf:
-  "h' \<equiv> \<lambda>x. let (y, a) = SOME (y, a). x = y + a \<cdot> x0 \<and> y \<in> H in h y + a * xi
-  \<Longrightarrow> H' \<equiv> H + lin x0 \<Longrightarrow> is_subspace H E \<Longrightarrow> is_linearform H h \<Longrightarrow> x0 \<notin> H
-  \<Longrightarrow> x0 \<in> E \<Longrightarrow> x0 \<noteq> 0 \<Longrightarrow> is_vectorspace E
-  \<Longrightarrow> is_linearform H' h'"
-proof -
-  assume h'_def:
-    "h' \<equiv> (\<lambda>x. let (y, a) = SOME (y, a). x = y + a \<cdot> x0 \<and> y \<in> H
-               in h y + a * xi)"
+  includes var H + var h + var E
+  assumes h'_def: "h' \<equiv> \<lambda>x. let (y, a) =
+      SOME (y, a). x = y + a \<cdot> x0 \<and> y \<in> H in h y + a * xi"
     and H'_def: "H' \<equiv> H + lin x0"
-    and vs: "is_subspace H E"  "is_linearform H h"  "x0 \<notin> H"
-      "x0 \<noteq> 0"  "x0 \<in> E"  "is_vectorspace E"
-
-  have h': "is_vectorspace H'"
-  proof (unfold H'_def, rule vs_sum_vs)
-    show "is_subspace (lin x0) E" ..
+    and HE: "H \<unlhd> E"
+  includes linearform H h
+  assumes x0: "x0 \<notin> H"  "x0 \<in> E"  "x0 \<noteq> 0"
+  includes vectorspace E
+  shows "linearform H' h'"
+proof
+  have H': "vectorspace H'"
+  proof (unfold H'_def)
+    have "x0 \<in> E" .
+    then have "lin x0 \<unlhd> E" ..
+    with HE show "vectorspace (H + lin x0)" ..
   qed
-
-  show ?thesis
-  proof
+  {
     fix x1 x2 assume x1: "x1 \<in> H'" and x2: "x2 \<in> H'"
-
-    txt {* We now have to show that @{text h'} is additive, i.~e.\
-      @{text "h' (x\<^sub>1 + x\<^sub>2) = h' x\<^sub>1 + h' x\<^sub>2"} for
-      @{text "x\<^sub>1, x\<^sub>2 \<in> H"}. *}
+    show "h' (x1 + x2) = h' x1 + h' x2"
+    proof -
+      from H' x1 x2 have "x1 + x2 \<in> H'"
+        by (rule vectorspace.add_closed)
+      with x1 x2 obtain y y1 y2 a a1 a2 where
+            x1x2: "x1 + x2 = y + a \<cdot> x0" and y: "y \<in> H"
+          and x1_rep: "x1 = y1 + a1 \<cdot> x0" and y1: "y1 \<in> H"
+          and x2_rep: "x2 = y2 + a2 \<cdot> x0" and y2: "y2 \<in> H"
+        by (unfold H'_def sum_def lin_def) blast
 
-    have x1x2: "x1 + x2 \<in> H'"
-      by (rule vs_add_closed, rule h')
-    from x1
-    have ex_x1: "\<exists>y1 a1. x1 = y1 + a1 \<cdot> x0  \<and> y1 \<in> H"
-      by (unfold H'_def vs_sum_def lin_def) fast
-    from x2
-    have ex_x2: "\<exists>y2 a2. x2 = y2 + a2 \<cdot> x0 \<and> y2 \<in> H"
-      by (unfold H'_def vs_sum_def lin_def) fast
-    from x1x2
-    have ex_x1x2: "\<exists>y a. x1 + x2 = y + a \<cdot> x0 \<and> y \<in> H"
-      by (unfold H'_def vs_sum_def lin_def) fast
-
-    from ex_x1 ex_x2 ex_x1x2
-    show "h' (x1 + x2) = h' x1 + h' x2"
-    proof (elim exE conjE)
-      fix y1 y2 y a1 a2 a
-      assume y1: "x1 = y1 + a1 \<cdot> x0"     and y1': "y1 \<in> H"
-         and y2: "x2 = y2 + a2 \<cdot> x0"     and y2': "y2 \<in> H"
-         and y: "x1 + x2 = y + a \<cdot> x0"   and y':  "y  \<in> H"
-      txt {* \label{decomp-H-use}*}
-      have ya: "y1 + y2 = y \<and> a1 + a2 = a"
-      proof (rule decomp_H')
-        show "y1 + y2 + (a1 + a2) \<cdot> x0 = y + a \<cdot> x0"
-          by (simp! add: vs_add_mult_distrib2 [of E])
-        show "y1 + y2 \<in> H" ..
+      have ya: "y1 + y2 = y \<and> a1 + a2 = a" using _ HE _ y x0
+      proof (rule decomp_H') txt_raw {* \label{decomp-H-use} *}
+        from HE y1 y2 show "y1 + y2 \<in> H"
+          by (rule subspace.add_closed)
+        from x0 and HE y y1 y2
+        have "x0 \<in> E"  "y \<in> E"  "y1 \<in> E"  "y2 \<in> E" by auto
+        with x1_rep x2_rep have "(y1 + y2) + (a1 + a2) \<cdot> x0 = x1 + x2"
+          by (simp add: add_ac add_mult_distrib2)
+        also note x1x2
+        finally show "(y1 + y2) + (a1 + a2) \<cdot> x0 = y + a \<cdot> x0" .
       qed
 
+      from h'_def x1x2 _ HE y x0
       have "h' (x1 + x2) = h y + a * xi"
         by (rule h'_definite)
-      also have "... = h (y1 + y2) + (a1 + a2) * xi"
-        by (simp add: ya)
-      also from vs y1' y2'
-      have "... = h y1 + h y2 + a1 * xi + a2 * xi"
-        by (simp add: linearform_add [of H]
-                      real_add_mult_distrib)
-      also have "... = (h y1 + a1 * xi) + (h y2 + a2 * xi)"
+      also have "\<dots> = h (y1 + y2) + (a1 + a2) * xi"
+        by (simp only: ya)
+      also from y1 y2 have "h (y1 + y2) = h y1 + h y2"
         by simp
-      also have "h y1 + a1 * xi = h' x1"
+      also have "\<dots> + (a1 + a2) * xi = (h y1 + a1 * xi) + (h y2 + a2 * xi)"
+        by (simp add: real_add_mult_distrib)
+      also from h'_def x1_rep _ HE y1 x0
+      have "h y1 + a1 * xi = h' x1"
         by (rule h'_definite [symmetric])
-      also have "h y2 + a2 * xi = h' x2"
+      also from h'_def x2_rep _ HE y2 x0
+      have "h y2 + a2 * xi = h' x2"
         by (rule h'_definite [symmetric])
       finally show ?thesis .
     qed
-
-    txt {* We further have to show that @{text h'} is multiplicative,
-    i.~e.\ @{text "h' (c \<cdot> x\<^sub>1) = c \<cdot> h' x\<^sub>1"} for @{text "x \<in> H"}
-    and @{text "c \<in> \<real>"}. *}
-
   next
-    fix c x1 assume x1: "x1 \<in> H'"
-    have ax1: "c \<cdot> x1 \<in> H'"
-      by (rule vs_mult_closed, rule h')
-    from x1
-    have ex_x: "\<And>x. x\<in> H' \<Longrightarrow> \<exists>y a. x = y + a \<cdot> x0 \<and> y \<in> H"
-      by (unfold H'_def vs_sum_def lin_def) fast
+    fix x1 c assume x1: "x1 \<in> H'"
+    show "h' (c \<cdot> x1) = c * (h' x1)"
+    proof -
+      from H' x1 have ax1: "c \<cdot> x1 \<in> H'"
+        by (rule vectorspace.mult_closed)
+      with x1 obtain y a y1 a1 where
+            cx1_rep: "c \<cdot> x1 = y + a \<cdot> x0" and y: "y \<in> H"
+          and x1_rep: "x1 = y1 + a1 \<cdot> x0" and y1: "y1 \<in> H"
+        by (unfold H'_def sum_def lin_def) blast
 
-    from x1 have ex_x1: "\<exists>y1 a1. x1 = y1 + a1 \<cdot> x0 \<and> y1 \<in> H"
-      by (unfold H'_def vs_sum_def lin_def) fast
-    with ex_x [of "c \<cdot> x1", OF ax1]
-    show "h' (c \<cdot> x1) = c * (h' x1)"
-    proof (elim exE conjE)
-      fix y1 y a1 a
-      assume y1: "x1 = y1 + a1 \<cdot> x0"     and y1': "y1 \<in> H"
-        and y: "c \<cdot> x1 = y  + a \<cdot> x0"    and y': "y \<in> H"
-
-      have ya: "c \<cdot> y1 = y \<and> c * a1 = a"
+      have ya: "c \<cdot> y1 = y \<and> c * a1 = a" using _ HE _ y x0
       proof (rule decomp_H')
-        show "c \<cdot> y1 + (c * a1) \<cdot> x0 = y + a \<cdot> x0"
-          by (simp! add: vs_add_mult_distrib1)
-        show "c \<cdot> y1 \<in> H" ..
+        from HE y1 show "c \<cdot> y1 \<in> H"
+          by (rule subspace.mult_closed)
+        from x0 and HE y y1
+        have "x0 \<in> E"  "y \<in> E"  "y1 \<in> E" by auto
+        with x1_rep have "c \<cdot> y1 + (c * a1) \<cdot> x0 = c \<cdot> x1"
+          by (simp add: mult_assoc add_mult_distrib1)
+        also note cx1_rep
+        finally show "c \<cdot> y1 + (c * a1) \<cdot> x0 = y + a \<cdot> x0" .
       qed
 
-      have "h' (c \<cdot> x1) = h y + a * xi"
+      from h'_def cx1_rep _ HE y x0 have "h' (c \<cdot> x1) = h y + a * xi"
         by (rule h'_definite)
-      also have "... = h (c \<cdot> y1) + (c * a1) * xi"
-        by (simp add: ya)
-      also from vs y1' have "... = c * h y1 + c * a1 * xi"
-        by (simp add: linearform_mult [of H])
-      also from vs y1' have "... = c * (h y1 + a1 * xi)"
-        by (simp add: real_add_mult_distrib2 real_mult_assoc)
-      also have "h y1 + a1 * xi = h' x1"
+      also have "\<dots> = h (c \<cdot> y1) + (c * a1) * xi"
+        by (simp only: ya)
+      also from y1 have "h (c \<cdot> y1) = c * h y1"
+        by simp
+      also have "\<dots> + (c * a1) * xi = c * (h y1 + a1 * xi)"
+        by (simp only: real_add_mult_distrib2)
+      also from h'_def x1_rep _ HE y1 x0 have "h y1 + a1 * xi = h' x1"
         by (rule h'_definite [symmetric])
       finally show ?thesis .
     qed
-  qed
+  }
 qed
 
 text {* \medskip The linear extension @{text h'} of @{text h}
-is bounded by the seminorm @{text p}. *}
+  is bounded by the seminorm @{text p}. *}
 
 lemma h'_norm_pres:
-  "h' \<equiv> \<lambda>x. let (y, a) = SOME (y, a). x = y + a \<cdot> x0 \<and> y \<in> H in h y + a * xi
-  \<Longrightarrow> H' \<equiv> H + lin x0 \<Longrightarrow> x0 \<notin> H \<Longrightarrow> x0 \<in> E \<Longrightarrow> x0 \<noteq> 0 \<Longrightarrow> is_vectorspace E
-  \<Longrightarrow> is_subspace H E \<Longrightarrow> is_seminorm E p \<Longrightarrow> is_linearform H h
-  \<Longrightarrow> \<forall>y \<in> H. h y \<le> p y
-  \<Longrightarrow> \<forall>y \<in> H. - p (y + x0) - h y \<le> xi \<and> xi \<le> p (y + x0) - h y
-  \<Longrightarrow> \<forall>x \<in> H'. h' x \<le> p x"
-proof
-  assume h'_def:
-    "h' \<equiv> (\<lambda>x. let (y, a) = SOME (y, a). x = y + a \<cdot> x0 \<and> y \<in> H
-               in (h y) + a * xi)"
+  includes var H + var h + var E
+  assumes h'_def: "h' \<equiv> \<lambda>x. let (y, a) =
+      SOME (y, a). x = y + a \<cdot> x0 \<and> y \<in> H in h y + a * xi"
     and H'_def: "H' \<equiv> H + lin x0"
-    and vs: "x0 \<notin> H"  "x0 \<in> E"  "x0 \<noteq> 0"  "is_vectorspace E"
-            "is_subspace H E"  "is_seminorm E p"  "is_linearform H h"
-    and a: "\<forall>y \<in> H. h y \<le> p y"
-  presume a1: "\<forall>ya \<in> H. - p (ya + x0) - h ya \<le> xi"
-  presume a2: "\<forall>ya \<in> H. xi \<le> p (ya + x0) - h ya"
-  fix x assume "x \<in> H'"
-  have ex_x:
-    "\<And>x. x \<in> H' \<Longrightarrow> \<exists>y a. x = y + a \<cdot> x0 \<and> y \<in> H"
-    by (unfold H'_def vs_sum_def lin_def) fast
-  have "\<exists>y a. x = y + a \<cdot> x0 \<and> y \<in> H"
-    by (rule ex_x)
-  thus "h' x \<le> p x"
-  proof (elim exE conjE)
-    fix y a assume x: "x = y + a \<cdot> x0" and y: "y \<in> H"
-    have "h' x = h y + a * xi"
+    and x0: "x0 \<notin> H"  "x0 \<in> E"  "x0 \<noteq> 0"
+  includes vectorspace E + subvectorspace H E +
+    seminorm E p + linearform H h
+  assumes a: "\<forall>y \<in> H. h y \<le> p y"
+    and a': "\<forall>y \<in> H. - p (y + x0) - h y \<le> xi \<and> xi \<le> p (y + x0) - h y"
+  shows "\<forall>x \<in> H'. h' x \<le> p x"
+proof
+  fix x assume x': "x \<in> H'"
+  show "h' x \<le> p x"
+  proof -
+    from a' have a1: "\<forall>ya \<in> H. - p (ya + x0) - h ya \<le> xi"
+      and a2: "\<forall>ya \<in> H. xi \<le> p (ya + x0) - h ya" by auto
+    from x' obtain y a where
+        x_rep: "x = y + a \<cdot> x0" and y: "y \<in> H"
+      by (unfold H'_def sum_def lin_def) blast
+    from y have y': "y \<in> E" ..
+    from y have ay: "inverse a \<cdot> y \<in> H" by simp
+
+    from h'_def x_rep _ _ y x0 have "h' x = h y + a * xi"
       by (rule h'_definite)
-
-    txt {* Now we show @{text "h y + a \<cdot> \<xi> \<le> p (y + a \<cdot> x\<^sub>0)"}
-    by case analysis on @{text a}. *}
-
-    also have "... \<le> p (y + a \<cdot> x0)"
+    also have "\<dots> \<le> p (y + a \<cdot> x0)"
     proof (rule linorder_cases)
-
       assume z: "a = 0"
-      with vs y a show ?thesis by simp
-
-    txt {* In the case @{text "a < 0"}, we use @{text "a\<^sub>1"}
-    with @{text ya} taken as @{text "y / a"}: *}
-
+      then have "h y + a * xi = h y" by simp
+      also from a y have "\<dots> \<le> p y" ..
+      also from x0 y' z have "p y = p (y + a \<cdot> x0)" by simp
+      finally show ?thesis .
     next
+      txt {* In the case @{text "a < 0"}, we use @{text "a\<^sub>1"}
+        with @{text ya} taken as @{text "y / a"}: *}
       assume lz: "a < 0" hence nz: "a \<noteq> 0" by simp
-      from a1
-      have "- p (inverse a \<cdot> y + x0) - h (inverse a \<cdot> y) \<le> xi"
-        by (rule bspec) (simp!)
-
-      txt {* The thesis for this case now follows by a short
-      calculation. *}
-      hence "a * xi \<le> a * (- p (inverse a \<cdot> y + x0) - h (inverse a \<cdot> y))"
-        by (rule real_mult_less_le_anti [OF lz])
-      also
-      have "... = - a * (p (inverse a \<cdot> y + x0)) - a * (h (inverse a \<cdot> y))"
+      from a1 ay
+      have "- p (inverse a \<cdot> y + x0) - h (inverse a \<cdot> y) \<le> xi" ..
+      with lz have "a * xi \<le>
+          a * (- p (inverse a \<cdot> y + x0) - h (inverse a \<cdot> y))"
+        by (rule real_mult_less_le_anti)
+      also have "\<dots> =
+          - a * (p (inverse a \<cdot> y + x0)) - a * (h (inverse a \<cdot> y))"
         by (rule real_mult_diff_distrib)
-      also from lz vs y
-      have "- a * (p (inverse a \<cdot> y + x0)) = p (a \<cdot> (inverse a \<cdot> y + x0))"
-        by (simp add: seminorm_abs_homogenous abs_minus_eqI2)
-      also from nz vs y have "... = p (y + a \<cdot> x0)"
-        by (simp add: vs_add_mult_distrib1)
-      also from nz vs y have "a * (h (inverse a \<cdot> y)) =  h y"
-        by (simp add: linearform_mult [symmetric])
+      also from lz x0 y' have "- a * (p (inverse a \<cdot> y + x0)) =
+          p (a \<cdot> (inverse a \<cdot> y + x0))"
+        by (simp add: abs_homogenous abs_minus_eqI2)
+      also from nz x0 y' have "\<dots> = p (y + a \<cdot> x0)"
+        by (simp add: add_mult_distrib1 mult_assoc [symmetric])
+      also from nz y have "a * (h (inverse a \<cdot> y)) =  h y"
+        by simp
       finally have "a * xi \<le> p (y + a \<cdot> x0) - h y" .
-
-      hence "h y + a * xi \<le> h y + p (y + a \<cdot> x0) - h y"
-        by (simp add: real_add_left_cancel_le)
-      thus ?thesis by simp
-
+      then show ?thesis by simp
+    next
       txt {* In the case @{text "a > 0"}, we use @{text "a\<^sub>2"}
         with @{text ya} taken as @{text "y / a"}: *}
-
-    next
       assume gz: "0 < a" hence nz: "a \<noteq> 0" by simp
-      from a2 have "xi \<le> p (inverse a \<cdot> y + x0) - h (inverse a \<cdot> y)"
-        by (rule bspec) (simp!)
-
-      txt {* The thesis for this case follows by a short
-      calculation: *}
-
-      with gz
-      have "a * xi \<le> a * (p (inverse a \<cdot> y + x0) - h (inverse a \<cdot> y))"
+      from a2 ay
+      have "xi \<le> p (inverse a \<cdot> y + x0) - h (inverse a \<cdot> y)" ..
+      with gz have "a * xi \<le>
+          a * (p (inverse a \<cdot> y + x0) - h (inverse a \<cdot> y))"
         by (rule real_mult_less_le_mono)
       also have "... = a * p (inverse a \<cdot> y + x0) - a * h (inverse a \<cdot> y)"
         by (rule real_mult_diff_distrib2)
-      also from gz vs y
+      also from gz x0 y'
       have "a * p (inverse a \<cdot> y + x0) = p (a \<cdot> (inverse a \<cdot> y + x0))"
-        by (simp add: seminorm_abs_homogenous abs_eqI2)
-      also from nz vs y have "... = p (y + a \<cdot> x0)"
-        by (simp add: vs_add_mult_distrib1)
-      also from nz vs y have "a * h (inverse a \<cdot> y) = h y"
-        by (simp add: linearform_mult [symmetric])
+        by (simp add: abs_homogenous abs_eqI2)
+      also from nz x0 y' have "\<dots> = p (y + a \<cdot> x0)"
+        by (simp add: add_mult_distrib1 mult_assoc [symmetric])
+      also from nz y have "a * h (inverse a \<cdot> y) = h y"
+        by simp
       finally have "a * xi \<le> p (y + a \<cdot> x0) - h y" .
-
-      hence "h y + a * xi \<le> h y + (p (y + a \<cdot> x0) - h y)"
-        by (simp add: real_add_left_cancel_le)
-      thus ?thesis by simp
+      then show ?thesis by simp
     qed
-    also from x have "... = p x" by simp
+    also from x_rep have "\<dots> = p x" by (simp only:)
     finally show ?thesis .
   qed
-qed blast+
+qed
 
 end
diff -r cc3bbaf1b8d3 -r a6a7025fd7e8 src/HOL/Real/HahnBanach/HahnBanachSupLemmas.thy
--- a/src/HOL/Real/HahnBanach/HahnBanachSupLemmas.thy	Thu Aug 22 12:28:41 2002 +0200
+++ b/src/HOL/Real/HahnBanach/HahnBanachSupLemmas.thy	Thu Aug 22 20:49:43 2002 +0200
@@ -13,62 +13,43 @@
   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}.
-*}
+  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
+  \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"
+  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
 
-  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
+  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
@@ -78,35 +59,26 @@
 *}
 
 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
+    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
@@ -115,136 +87,116 @@
 *}
 
 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 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"
+    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 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'"
-      "graph F f \<subseteq> graph H' h'"  "\<forall>x \<in> H'. h' x \<le> p x"
+  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"
+    by (rule some_H'h't [elim_format]) blast
 
-    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''"
-      "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}*}
+  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
+  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)
+  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" ..
 
-    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}.*}
+  from G1 c have "G1 \<in> M" ..
+  then obtain H1 h1 where G1_rep: "G1 = graph H1 h1"
+    by (unfold M_def) blast
 
-    fix G1 G2 assume
-      "(x, y) \<in> G1"  "G1 \<in> c"  "(x, z) \<in> G2"  "G2 \<in> c"  "c \<subseteq> M"
+  from G2 c have "G2 \<in> M" ..
+  then obtain H2 h2 where G2_rep: "G2 = graph H2 h2"
+    by (unfold M_def) blast
 
-    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}*}
+  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 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
 
@@ -258,58 +210,48 @@
 *}
 
 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. *}
+  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
 
-    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')
+  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
 
-    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
+  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
 
@@ -321,37 +263,22 @@
 *}
 
 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 {*
@@ -362,32 +289,21 @@
 *}
 
 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 {*
@@ -396,81 +312,53 @@
 *}
 
 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
 
@@ -480,28 +368,21 @@
 *}
 
 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
+    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}
@@ -516,45 +397,41 @@
 *}
 
 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
diff -r cc3bbaf1b8d3 -r a6a7025fd7e8 src/HOL/Real/HahnBanach/Linearform.thy
--- a/src/HOL/Real/HahnBanach/Linearform.thy	Thu Aug 22 12:28:41 2002 +0200
+++ b/src/HOL/Real/HahnBanach/Linearform.thy	Thu Aug 22 20:49:43 2002 +0200
@@ -12,60 +12,43 @@
   that is additive and multiplicative.
 *}
 
-constdefs
-  is_linearform :: "'a::{plus, minus, zero} set \<Rightarrow> ('a \<Rightarrow> real) \<Rightarrow> bool"
-  "is_linearform V f \<equiv>
-      (\<forall>x \<in> V. \<forall>y \<in> V. f (x + y) = f x + f y) \<and>
-      (\<forall>x \<in> V. \<forall>a. f (a \<cdot> x) = a * (f x))"
+locale linearform = var V + var f +
+  assumes add [iff]: "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> f (x + y) = f x + f y"
+    and mult [iff]: "x \<in> V \<Longrightarrow> f (a \<cdot> x) = a * f x"
 
-lemma is_linearformI [intro]:
-  "(\<And>x y. x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> f (x + y) = f x + f y) \<Longrightarrow>
-    (\<And>x c. x \<in> V \<Longrightarrow> f (c \<cdot> x) = c * f x)
- \<Longrightarrow> is_linearform V f"
- by (unfold is_linearform_def) blast
+locale (open) vectorspace_linearform =
+  vectorspace + linearform
 
-lemma linearform_add [intro?]:
-  "is_linearform V f \<Longrightarrow> x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> f (x + y) = f x + f y"
-  by (unfold is_linearform_def) blast
-
-lemma linearform_mult [intro?]:
-  "is_linearform V f \<Longrightarrow> x \<in> V \<Longrightarrow>  f (a \<cdot> x) = a * (f x)"
-  by (unfold is_linearform_def) blast
-
-lemma linearform_neg [intro?]:
-  "is_vectorspace V \<Longrightarrow> is_linearform V f \<Longrightarrow> x \<in> V
-  \<Longrightarrow> f (- x) = - f x"
+lemma (in vectorspace_linearform) neg [iff]:
+  "x \<in> V \<Longrightarrow> f (- x) = - f x"
 proof -
-  assume "is_linearform V f"  "is_vectorspace V"  "x \<in> V"
-  have "f (- x) = f ((- 1) \<cdot> x)" by (simp! add: negate_eq1)
-  also have "... = (- 1) * (f x)" by (rule linearform_mult)
-  also have "... = - (f x)" by (simp!)
+  assume x: "x \<in> V"
+  hence "f (- x) = f ((- 1) \<cdot> x)" by (simp add: negate_eq1)
+  also from x have "... = (- 1) * (f x)" by (rule mult)
+  also from x have "... = - (f x)" by simp
   finally show ?thesis .
 qed
 
-lemma linearform_diff [intro?]:
-  "is_vectorspace V \<Longrightarrow> is_linearform V f \<Longrightarrow> x \<in> V \<Longrightarrow> y \<in> V
-  \<Longrightarrow> f (x - y) = f x - f y"
+lemma (in vectorspace_linearform) diff [iff]:
+  "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> f (x - y) = f x - f y"
 proof -
-  assume "is_vectorspace V"  "is_linearform V f"  "x \<in> V"  "y \<in> V"
-  have "f (x - y) = f (x + - y)" by (simp! only: diff_eq1)
-  also have "... = f x + f (- y)"
-    by (rule linearform_add) (simp!)+
-  also have "f (- y) = - f y" by (rule linearform_neg)
-  finally show "f (x - y) = f x - f y" by (simp!)
+  assume x: "x \<in> V" and y: "y \<in> V"
+  hence "x - y = x + - y" by (rule diff_eq1)
+  also have "f ... = f x + f (- y)"
+    by (rule add) (simp_all add: x y)
+  also from y have "f (- y) = - f y" by (rule neg)
+  finally show ?thesis by simp
 qed
 
 text {* Every linear form yields @{text 0} for the @{text 0} vector. *}
 
-lemma linearform_zero [intro?, simp]:
-  "is_vectorspace V \<Longrightarrow> is_linearform V f \<Longrightarrow> f 0 = 0"
+lemma (in vectorspace_linearform) linearform_zero [iff]:
+  "f 0 = 0"
 proof -
-  assume "is_vectorspace V"  "is_linearform V f"
-  have "f 0 = f (0 - 0)" by (simp!)
-  also have "... = f 0 - f 0"
-    by (rule linearform_diff) (simp!)+
-  also have "... = 0" by simp
-  finally show "f 0 = 0" .
+  have "f 0 = f (0 - 0)" by simp
+  also have "\<dots> = f 0 - f 0" by (rule diff) simp_all
+  also have "\<dots> = 0" by simp
+  finally show ?thesis .
 qed
 
 end
diff -r cc3bbaf1b8d3 -r a6a7025fd7e8 src/HOL/Real/HahnBanach/NormedSpace.thy
--- a/src/HOL/Real/HahnBanach/NormedSpace.thy	Thu Aug 22 12:28:41 2002 +0200
+++ b/src/HOL/Real/HahnBanach/NormedSpace.thy	Thu Aug 22 20:49:43 2002 +0200
@@ -15,59 +15,40 @@
   definite, absolute homogenous and subadditive.
 *}
 
-constdefs
-  is_seminorm :: "'a::{plus, minus, zero} set \<Rightarrow> ('a \<Rightarrow> real) \<Rightarrow> bool"
-  "is_seminorm V norm \<equiv> \<forall>x \<in> V. \<forall>y \<in> V. \<forall>a.
-        0 \<le> norm x
-      \<and> norm (a \<cdot> x) = \<bar>a\<bar> * norm x
-      \<and> norm (x + y) \<le> norm x + norm y"
+locale norm_syntax =
+  fixes norm :: "'a \<Rightarrow> real"    ("\<parallel>_\<parallel>")
 
-lemma is_seminormI [intro]:
-  "(\<And>x y a. x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> 0 \<le> norm x) \<Longrightarrow>
-  (\<And>x a. x \<in> V \<Longrightarrow> norm (a \<cdot> x) = \<bar>a\<bar> * norm x) \<Longrightarrow>
-  (\<And>x y. x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> norm (x + y) \<le> norm x + norm y)
-  \<Longrightarrow> is_seminorm V norm"
-  by (unfold is_seminorm_def) auto
+locale seminorm = var V + norm_syntax +
+  assumes ge_zero [iff?]: "x \<in> V \<Longrightarrow> 0 \<le> \<parallel>x\<parallel>"
+    and abs_homogenous [iff?]: "x \<in> V \<Longrightarrow> \<parallel>a \<cdot> x\<parallel> = \<bar>a\<bar> * \<parallel>x\<parallel>"
+    and subadditive [iff?]: "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> \<parallel>x + y\<parallel> \<le> \<parallel>x\<parallel> + \<parallel>y\<parallel>"
 
-lemma seminorm_ge_zero [intro?]:
-  "is_seminorm V norm \<Longrightarrow> x \<in> V \<Longrightarrow> 0 \<le> norm x"
-  by (unfold is_seminorm_def) blast
+locale (open) seminorm_vectorspace =
+  seminorm + vectorspace
 
-lemma seminorm_abs_homogenous:
-  "is_seminorm V norm \<Longrightarrow> x \<in> V
-  \<Longrightarrow> norm (a \<cdot> x) = \<bar>a\<bar> * norm x"
-  by (unfold is_seminorm_def) blast
-
-lemma seminorm_subadditive:
-  "is_seminorm V norm \<Longrightarrow> x \<in> V \<Longrightarrow> y \<in> V
-  \<Longrightarrow> norm (x + y) \<le> norm x + norm y"
-  by (unfold is_seminorm_def) blast
-
-lemma seminorm_diff_subadditive:
-  "is_seminorm V norm \<Longrightarrow> x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> is_vectorspace V
-  \<Longrightarrow> norm (x - y) \<le> norm x + norm y"
+lemma (in seminorm_vectorspace) diff_subadditive:
+  "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> \<parallel>x - y\<parallel> \<le> \<parallel>x\<parallel> + \<parallel>y\<parallel>"
 proof -
-  assume "is_seminorm V norm"  "x \<in> V"  "y \<in> V"  "is_vectorspace V"
-  have "norm (x - y) = norm (x + - 1 \<cdot> y)"
-    by (simp! add: diff_eq2 negate_eq2a)
-  also have "... \<le> norm x + norm  (- 1 \<cdot> y)"
-    by (simp! add: seminorm_subadditive)
-  also have "norm (- 1 \<cdot> y) = \<bar>- 1\<bar> * norm y"
-    by (rule seminorm_abs_homogenous)
-  also have "\<bar>- 1\<bar> = (1::real)" by (rule abs_minus_one)
-  finally show "norm (x - y) \<le> norm x + norm y" by simp
+  assume x: "x \<in> V" and y: "y \<in> V"
+  hence "x - y = x + - 1 \<cdot> y"
+    by (simp add: diff_eq2 negate_eq2a)
+  also from x y have "\<parallel>\<dots>\<parallel> \<le> \<parallel>x\<parallel> + \<parallel>- 1 \<cdot> y\<parallel>"
+    by (simp add: subadditive)
+  also from y have "\<parallel>- 1 \<cdot> y\<parallel> = \<bar>- 1\<bar> * \<parallel>y\<parallel>"
+    by (rule abs_homogenous)
+  also have "\<dots> = \<parallel>y\<parallel>" by simp
+  finally show ?thesis .
 qed
 
-lemma seminorm_minus:
-  "is_seminorm V norm \<Longrightarrow> x \<in> V \<Longrightarrow> is_vectorspace V
-  \<Longrightarrow> norm (- x) = norm x"
+lemma (in seminorm_vectorspace) minus:
+  "x \<in> V \<Longrightarrow> \<parallel>- x\<parallel> = \<parallel>x\<parallel>"
 proof -
-  assume "is_seminorm V norm"  "x \<in> V"  "is_vectorspace V"
-  have "norm (- x) = norm (- 1 \<cdot> x)" by (simp! only: negate_eq1)
-  also have "... = \<bar>- 1\<bar> * norm x"
-    by (rule seminorm_abs_homogenous)
-  also have "\<bar>- 1\<bar> = (1::real)" by (rule abs_minus_one)
-  finally show "norm (- x) = norm x" by simp
+  assume x: "x \<in> V"
+  hence "- x = - 1 \<cdot> x" by (simp only: negate_eq1)
+  also from x have "\<parallel>\<dots>\<parallel> = \<bar>- 1\<bar> * \<parallel>x\<parallel>"
+    by (rule abs_homogenous)
+  also have "\<dots> = \<parallel>x\<parallel>" by simp
+  finally show ?thesis .
 qed
 
 
@@ -78,110 +59,46 @@
   @{text 0} vector to @{text 0}.
 *}
 
-constdefs
-  is_norm :: "'a::{plus, minus, zero} set \<Rightarrow> ('a \<Rightarrow> real) \<Rightarrow> bool"
-  "is_norm V norm \<equiv> \<forall>x \<in> V. is_seminorm V norm
-      \<and> (norm x = 0) = (x = 0)"
-
-lemma is_normI [intro]:
-  "\<forall>x \<in> V.  is_seminorm V norm  \<and> (norm x = 0) = (x = 0)
-  \<Longrightarrow> is_norm V norm" by (simp only: is_norm_def)
-
-lemma norm_is_seminorm [intro?]:
-  "is_norm V norm \<Longrightarrow> x \<in> V \<Longrightarrow> is_seminorm V norm"
-  by (unfold is_norm_def) blast
-
-lemma norm_zero_iff:
-  "is_norm V norm \<Longrightarrow> x \<in> V \<Longrightarrow> (norm x = 0) = (x = 0)"
-  by (unfold is_norm_def) blast
-
-lemma norm_ge_zero [intro?]:
-  "is_norm V norm \<Longrightarrow> x \<in> V \<Longrightarrow> 0 \<le> norm x"
-  by (unfold is_norm_def is_seminorm_def) blast
+locale norm = seminorm +
+  assumes zero_iff [iff]: "x \<in> V \<Longrightarrow> (\<parallel>x\<parallel> = 0) = (x = 0)"
 
 
 subsection {* Normed vector spaces *}
 
-text{* A vector space together with a norm is called
-a \emph{normed space}. *}
-
-constdefs
-  is_normed_vectorspace ::
-  "'a::{plus, minus, zero} set \<Rightarrow> ('a \<Rightarrow> real) \<Rightarrow> bool"
-  "is_normed_vectorspace V norm \<equiv>
-      is_vectorspace V \<and> is_norm V norm"
+text {*
+  A vector space together with a norm is called a \emph{normed
+  space}.
+*}
 
-lemma normed_vsI [intro]:
-  "is_vectorspace V \<Longrightarrow> is_norm V norm
-  \<Longrightarrow> is_normed_vectorspace V norm"
-  by (unfold is_normed_vectorspace_def) blast
-
-lemma normed_vs_vs [intro?]:
-  "is_normed_vectorspace V norm \<Longrightarrow> is_vectorspace V"
-  by (unfold is_normed_vectorspace_def) blast
+locale normed_vectorspace = vectorspace + seminorm_vectorspace + norm
 
-lemma normed_vs_norm [intro?]:
-  "is_normed_vectorspace V norm \<Longrightarrow> is_norm V norm"
-  by (unfold is_normed_vectorspace_def) blast
-
-lemma normed_vs_norm_ge_zero [intro?]:
-  "is_normed_vectorspace V norm \<Longrightarrow> x \<in> V \<Longrightarrow> 0 \<le> norm x"
-  by (unfold is_normed_vectorspace_def) (fast elim: norm_ge_zero)
-
-lemma normed_vs_norm_gt_zero [intro?]:
-  "is_normed_vectorspace V norm \<Longrightarrow> x \<in> V \<Longrightarrow> x \<noteq> 0 \<Longrightarrow> 0 < norm x"
-proof (unfold is_normed_vectorspace_def, elim conjE)
-  assume "x \<in> V"  "x \<noteq> 0"  "is_vectorspace V"  "is_norm V norm"
-  have "0 \<le> norm x" ..
-  also have "0 \<noteq> norm x"
+lemma (in normed_vectorspace) gt_zero [intro?]:
+  "x \<in> V \<Longrightarrow> x \<noteq> 0 \<Longrightarrow> 0 < \<parallel>x\<parallel>"
+proof -
+  assume x: "x \<in> V" and neq: "x \<noteq> 0"
+  from x have "0 \<le> \<parallel>x\<parallel>" ..
+  also have [symmetric]: "\<dots> \<noteq> 0"
   proof
-    presume "norm x = 0"
-    also have "?this = (x = 0)" by (rule norm_zero_iff)
-    finally have "x = 0" .
-    thus "False" by contradiction
-  qed (rule sym)
-  finally show "0 < norm x" .
+    assume "\<parallel>x\<parallel> = 0"
+    with x have "x = 0" by simp
+    with neq show False by contradiction
+  qed
+  finally show ?thesis .
 qed
 
-lemma normed_vs_norm_abs_homogenous [intro?]:
-  "is_normed_vectorspace V norm \<Longrightarrow> x \<in> V
-  \<Longrightarrow> norm (a \<cdot> x) = \<bar>a\<bar> * norm x"
-  by (rule seminorm_abs_homogenous, rule norm_is_seminorm,
-      rule normed_vs_norm)
-
-lemma normed_vs_norm_subadditive [intro?]:
-  "is_normed_vectorspace V norm \<Longrightarrow> x \<in> V \<Longrightarrow> y \<in> V
-  \<Longrightarrow> norm (x + y) \<le> norm x + norm y"
-  by (rule seminorm_subadditive, rule norm_is_seminorm,
-     rule normed_vs_norm)
-
-text{* Any subspace of a normed vector space is again a
-normed vectorspace.*}
+text {*
+  Any subspace of a normed vector space is again a normed vectorspace.
+*}
 
 lemma subspace_normed_vs [intro?]:
-  "is_vectorspace E \<Longrightarrow> is_subspace F E \<Longrightarrow>
-  is_normed_vectorspace E norm \<Longrightarrow> is_normed_vectorspace F norm"
-proof (rule normed_vsI)
-  assume "is_subspace F E"  "is_vectorspace E"
-         "is_normed_vectorspace E norm"
-  show "is_vectorspace F" ..
-  show "is_norm F norm"
-  proof (intro is_normI ballI conjI)
-    show "is_seminorm F norm"
-    proof
-      fix x y a presume "x \<in> E"
-      show "0 \<le> norm x" ..
-      show "norm (a \<cdot> x) = \<bar>a\<bar> * norm x" ..
-      presume "y \<in> E"
-      show "norm (x + y) \<le> norm x + norm y" ..
-    qed (simp!)+
-
-    fix x assume "x \<in> F"
-    show "(norm x = 0) = (x = 0)"
-    proof (rule norm_zero_iff)
-      show "is_norm E norm" ..
-    qed (simp!)
-  qed
+  includes subvectorspace F E + normed_vectorspace E
+  shows "normed_vectorspace F norm"
+proof
+  show "vectorspace F" by (rule vectorspace)
+  have "seminorm E norm" . with subset show "seminorm F norm"
+    by (simp add: seminorm_def)
+  have "norm_axioms E norm" . with subset show "norm_axioms F norm"
+    by (simp add: norm_axioms_def)
 qed
 
 end
diff -r cc3bbaf1b8d3 -r a6a7025fd7e8 src/HOL/Real/HahnBanach/Subspace.thy
--- a/src/HOL/Real/HahnBanach/Subspace.thy	Thu Aug 22 12:28:41 2002 +0200
+++ b/src/HOL/Real/HahnBanach/Subspace.thy	Thu Aug 22 20:49:43 2002 +0200
@@ -16,122 +16,109 @@
   and scalar multiplication.
 *}
 
-constdefs
-  is_subspace ::  "'a::{plus, minus, zero} set \<Rightarrow> 'a set \<Rightarrow> bool"
-  "is_subspace U V \<equiv> U \<noteq> {} \<and> U \<subseteq> V
-     \<and> (\<forall>x \<in> U. \<forall>y \<in> U. \<forall>a. x + y \<in> U \<and> a \<cdot> x \<in> U)"
+locale subspace = var U + var V +
+  assumes non_empty [iff, intro]: "U \<noteq> {}"
+    and subset [iff]: "U \<subseteq> V"
+    and add_closed [iff]: "x \<in> U \<Longrightarrow> y \<in> U \<Longrightarrow> x + y \<in> U"
+    and mult_closed [iff]: "x \<in> U \<Longrightarrow> a \<cdot> x \<in> U"
 
-lemma subspaceI [intro]:
-  "0 \<in> U \<Longrightarrow> U \<subseteq> V \<Longrightarrow> \<forall>x \<in> U. \<forall>y \<in> U. (x + y \<in> U) \<Longrightarrow>
-  \<forall>x \<in> U. \<forall>a. a \<cdot> x \<in> U
-  \<Longrightarrow> is_subspace U V"
-proof (unfold is_subspace_def, intro conjI)
-  assume "0 \<in> U" thus "U \<noteq> {}" by fast
-qed (simp+)
+syntax (symbols)
+  subspace :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool"    (infix "\<unlhd>" 50)
 
-lemma subspace_not_empty [intro?]: "is_subspace U V \<Longrightarrow> U \<noteq> {}"
-  by (unfold is_subspace_def) blast
+lemma subspace_subset [elim]: "U \<unlhd> V \<Longrightarrow> U \<subseteq> V"
+  by (rule subspace.subset)
 
-lemma subspace_subset [intro?]: "is_subspace U V \<Longrightarrow> U \<subseteq> V"
-  by (unfold is_subspace_def) blast
+lemma (in subspace) subsetD [iff]: "x \<in> U \<Longrightarrow> x \<in> V"
+  using subset by blast
 
-lemma subspace_subsetD [simp, intro?]:
-  "is_subspace U V \<Longrightarrow> x \<in> U \<Longrightarrow> x \<in> V"
-  by (unfold is_subspace_def) blast
+lemma subspaceD [elim]: "U \<unlhd> V \<Longrightarrow> x \<in> U \<Longrightarrow> x \<in> V"
+  by (rule subspace.subsetD)
 
-lemma subspace_add_closed [simp, intro?]:
-  "is_subspace U V \<Longrightarrow> x \<in> U \<Longrightarrow> y \<in> U \<Longrightarrow> x + y \<in> U"
-  by (unfold is_subspace_def) blast
+lemma rev_subspaceD [elim?]: "x \<in> U \<Longrightarrow> U \<unlhd> V \<Longrightarrow> x \<in> V"
+  by (rule subspace.subsetD)
+
 
-lemma subspace_mult_closed [simp, intro?]:
-  "is_subspace U V \<Longrightarrow> x \<in> U \<Longrightarrow> a \<cdot> x \<in> U"
-  by (unfold is_subspace_def) blast
+locale (open) subvectorspace =
+  subspace + vectorspace
 
-lemma subspace_diff_closed [simp, intro?]:
-  "is_subspace U V \<Longrightarrow> is_vectorspace V \<Longrightarrow> x \<in> U \<Longrightarrow> y \<in> U
-  \<Longrightarrow> x - y \<in> U"
+lemma (in subvectorspace) diff_closed [iff]:
+    "x \<in> U \<Longrightarrow> y \<in> U \<Longrightarrow> x - y \<in> U"
   by (simp add: diff_eq1 negate_eq1)
 
-text {* Similar as for linear spaces, the existence of the
-zero element in every subspace follows from the non-emptiness
-of the carrier set and by vector space laws.*}
 
-lemma zero_in_subspace [intro?]:
-  "is_subspace U V \<Longrightarrow> is_vectorspace V \<Longrightarrow> 0 \<in> U"
+text {*
+  \medskip Similar as for linear spaces, the existence of the zero
+  element in every subspace follows from the non-emptiness of the
+  carrier set and by vector space laws.
+*}
+
+lemma (in subvectorspace) zero [intro]: "0 \<in> U"
 proof -
-  assume "is_subspace U V" and v: "is_vectorspace V"
-  have "U \<noteq> {}" ..
-  hence "\<exists>x. x \<in> U" by blast
-  thus ?thesis
-  proof
-    fix x assume u: "x \<in> U"
-    hence "x \<in> V" by (simp!)
-    with v have "0 = x - x" by (simp!)
-    also have "... \<in> U" by (rule subspace_diff_closed)
-    finally show ?thesis .
-  qed
+  have "U \<noteq> {}" by (rule U_V.non_empty)
+  then obtain x where x: "x \<in> U" by blast
+  hence "x \<in> V" .. hence "0 = x - x" by simp
+  also have "... \<in> U" by (rule U_V.diff_closed)
+  finally show ?thesis .
 qed
 
-lemma subspace_neg_closed [simp, intro?]:
-  "is_subspace U V \<Longrightarrow> is_vectorspace V \<Longrightarrow> x \<in> U \<Longrightarrow> - x \<in> U"
+lemma (in subvectorspace) neg_closed [iff]: "x \<in> U \<Longrightarrow> - x \<in> U"
   by (simp add: negate_eq1)
 
+
 text {* \medskip Further derived laws: every subspace is a vector space. *}
 
-lemma subspace_vs [intro?]:
-  "is_subspace U V \<Longrightarrow> is_vectorspace V \<Longrightarrow> is_vectorspace U"
-proof -
-  assume "is_subspace U V"  "is_vectorspace V"
-  show ?thesis
-  proof
-    show "0 \<in> U" ..
-    show "\<forall>x \<in> U. \<forall>a. a \<cdot> x \<in> U" by (simp!)
-    show "\<forall>x \<in> U. \<forall>y \<in> U. x + y \<in> U" by (simp!)
-    show "\<forall>x \<in> U. - x = - 1 \<cdot> x" by (simp! add: negate_eq1)
-    show "\<forall>x \<in> U. \<forall>y \<in> U. x - y =  x + - y"
-      by (simp! add: diff_eq1)
-  qed (simp! add: vs_add_mult_distrib1 vs_add_mult_distrib2)+
+lemma (in subvectorspace) vectorspace [iff]:
+  "vectorspace U"
+proof
+  show "U \<noteq> {}" ..
+  fix x y z assume x: "x \<in> U" and y: "y \<in> U" and z: "z \<in> U"
+  fix a b :: real
+  from x y show "x + y \<in> U" by simp
+  from x show "a \<cdot> x \<in> U" by simp
+  from x y z show "(x + y) + z = x + (y + z)" by (simp add: add_ac)
+  from x y show "x + y = y + x" by (simp add: add_ac)
+  from x show "x - x = 0" by simp
+  from x show "0 + x = x" by simp
+  from x y show "a \<cdot> (x + y) = a \<cdot> x + a \<cdot> y" by (simp add: distrib)
+  from x show "(a + b) \<cdot> x = a \<cdot> x + b \<cdot> x" by (simp add: distrib)
+  from x show "(a * b) \<cdot> x = a \<cdot> b \<cdot> x" by (simp add: mult_assoc)
+  from x show "1 \<cdot> x = x" by simp
+  from x show "- x = - 1 \<cdot> x" by (simp add: negate_eq1)
+  from x y show "x - y = x + - y" by (simp add: diff_eq1)
 qed
 
+
 text {* The subspace relation is reflexive. *}
 
-lemma subspace_refl [intro]: "is_vectorspace V \<Longrightarrow> is_subspace V V"
+lemma (in vectorspace) subspace_refl [intro]: "V \<unlhd> V"
 proof
-  assume "is_vectorspace V"
-  show "0 \<in> V" ..
+  show "V \<noteq> {}" ..
   show "V \<subseteq> V" ..
-  show "\<forall>x \<in> V. \<forall>y \<in> V. x + y \<in> V" by (simp!)
-  show "\<forall>x \<in> V. \<forall>a. a \<cdot> x \<in> V" by (simp!)
+  fix x y assume x: "x \<in> V" and y: "y \<in> V"
+  fix a :: real
+  from x y show "x + y \<in> V" by simp
+  from x show "a \<cdot> x \<in> V" by simp
 qed
 
 text {* The subspace relation is transitive. *}
 
-lemma subspace_trans:
-  "is_subspace U V \<Longrightarrow> is_vectorspace V \<Longrightarrow> is_subspace V W
-  \<Longrightarrow> is_subspace U W"
+lemma (in vectorspace) subspace_trans [trans]:
+  "U \<unlhd> V \<Longrightarrow> V \<unlhd> W \<Longrightarrow> U \<unlhd> W"
 proof
-  assume "is_subspace U V"  "is_subspace V W"  "is_vectorspace V"
-  show "0 \<in> U" ..
-
-  have "U \<subseteq> V" ..
-  also have "V \<subseteq> W" ..
-  finally show "U \<subseteq> W" .
-
-  show "\<forall>x \<in> U. \<forall>y \<in> U. x + y \<in> U"
-  proof (intro ballI)
-    fix x y assume "x \<in> U"  "y \<in> U"
-    show "x + y \<in> U" by (simp!)
+  assume uv: "U \<unlhd> V" and vw: "V \<unlhd> W"
+  from uv show "U \<noteq> {}" by (rule subspace.non_empty)
+  show "U \<subseteq> W"
+  proof -
+    from uv have "U \<subseteq> V" by (rule subspace.subset)
+    also from vw have "V \<subseteq> W" by (rule subspace.subset)
+    finally show ?thesis .
   qed
-
-  show "\<forall>x \<in> U. \<forall>a. a \<cdot> x \<in> U"
-  proof (intro ballI allI)
-    fix x a assume "x \<in> U"
-    show "a \<cdot> x \<in> U" by (simp!)
-  qed
+  fix x y assume x: "x \<in> U" and y: "y \<in> U"
+  from uv and x y show "x + y \<in> U" by (rule subspace.add_closed)
+  from uv and x show "\<And>a. a \<cdot> x \<in> U" by (rule subspace.mult_closed)
 qed
 
 
-
 subsection {* Linear closure *}
 
 text {*
@@ -140,73 +127,75 @@
 *}
 
 constdefs
-  lin :: "('a::{minus,plus,zero}) \<Rightarrow> 'a set"
+  lin :: "('a::{minus, plus, zero}) \<Rightarrow> 'a set"
   "lin x \<equiv> {a \<cdot> x | a. True}"
 
-lemma linD: "(x \<in> lin v) = (\<exists>a::real. x = a \<cdot> v)"
-  by (unfold lin_def) fast
+lemma linI [intro]: "y = a \<cdot> x \<Longrightarrow> y \<in> lin x"
+  by (unfold lin_def) blast
 
-lemma linI [intro?]: "a \<cdot> x0 \<in> lin x0"
-  by (unfold lin_def) fast
+lemma linI' [iff]: "a \<cdot> x \<in> lin x"
+  by (unfold lin_def) blast
+
+lemma linE [elim]:
+    "x \<in> lin v \<Longrightarrow> (\<And>a::real. x = a \<cdot> v \<Longrightarrow> C) \<Longrightarrow> C"
+  by (unfold lin_def) blast
+
 
 text {* Every vector is contained in its linear closure. *}
 
-lemma x_lin_x: "is_vectorspace V \<Longrightarrow> x \<in> V \<Longrightarrow> x \<in> lin x"
-proof (unfold lin_def, intro CollectI exI conjI)
-  assume "is_vectorspace V"  "x \<in> V"
-  show "x = 1 \<cdot> x" by (simp!)
-qed simp
+lemma (in vectorspace) x_lin_x [iff]: "x \<in> V \<Longrightarrow> x \<in> lin x"
+proof -
+  assume "x \<in> V"
+  hence "x = 1 \<cdot> x" by simp
+  also have "\<dots> \<in> lin x" ..
+  finally show ?thesis .
+qed
+
+lemma (in vectorspace) "0_lin_x" [iff]: "x \<in> V \<Longrightarrow> 0 \<in> lin x"
+proof
+  assume "x \<in> V"
+  thus "0 = 0 \<cdot> x" by simp
+qed
 
 text {* Any linear closure is a subspace. *}
 
-lemma lin_subspace [intro?]:
-  "is_vectorspace V \<Longrightarrow> x \<in> V \<Longrightarrow> is_subspace (lin x) V"
+lemma (in vectorspace) lin_subspace [intro]:
+  "x \<in> V \<Longrightarrow> lin x \<unlhd> V"
 proof
-  assume "is_vectorspace V"  "x \<in> V"
-  show "0 \<in> lin x"
-  proof (unfold lin_def, intro CollectI exI conjI)
-    show "0 = (0::real) \<cdot> x" by (simp!)
-  qed simp
-
+  assume x: "x \<in> V"
+  thus "lin x \<noteq> {}" by (auto simp add: x_lin_x)
   show "lin x \<subseteq> V"
-  proof (unfold lin_def, intro subsetI, elim CollectE exE conjE)
-    fix xa a assume "xa = a \<cdot> x"
-    show "xa \<in> V" by (simp!)
+  proof
+    fix x' assume "x' \<in> lin x"
+    then obtain a where "x' = a \<cdot> x" ..
+    with x show "x' \<in> V" by simp
   qed
-
-  show "\<forall>x1 \<in> lin x. \<forall>x2 \<in> lin x. x1 + x2 \<in> lin x"
-  proof (intro ballI)
-    fix x1 x2 assume "x1 \<in> lin x"  "x2 \<in> lin x"
-    thus "x1 + x2 \<in> lin x"
-    proof (unfold lin_def, elim CollectE exE conjE,
-      intro CollectI exI conjI)
-      fix a1 a2 assume "x1 = a1 \<cdot> x"  "x2 = a2 \<cdot> x"
-      show "x1 + x2 = (a1 + a2) \<cdot> x"
-        by (simp! add: vs_add_mult_distrib2)
-    qed simp
+  fix x' x'' assume x': "x' \<in> lin x" and x'': "x'' \<in> lin x"
+  show "x' + x'' \<in> lin x"
+  proof -
+    from x' obtain a' where "x' = a' \<cdot> x" ..
+    moreover from x'' obtain a'' where "x'' = a'' \<cdot> x" ..
+    ultimately have "x' + x'' = (a' + a'') \<cdot> x"
+      using x by (simp add: distrib)
+    also have "\<dots> \<in> lin x" ..
+    finally show ?thesis .
   qed
-
-  show "\<forall>xa \<in> lin x. \<forall>a. a \<cdot> xa \<in> lin x"
-  proof (intro ballI allI)
-    fix x1 a assume "x1 \<in> lin x"
-    thus "a \<cdot> x1 \<in> lin x"
-    proof (unfold lin_def, elim CollectE exE conjE,
-      intro CollectI exI conjI)
-      fix a1 assume "x1 = a1 \<cdot> x"
-      show "a \<cdot> x1 = (a * a1) \<cdot> x" by (simp!)
-    qed simp
+  fix a :: real
+  show "a \<cdot> x' \<in> lin x"
+  proof -
+    from x' obtain a' where "x' = a' \<cdot> x" ..
+    with x have "a \<cdot> x' = (a * a') \<cdot> x" by (simp add: mult_assoc)
+    also have "\<dots> \<in> lin x" ..
+    finally show ?thesis .
   qed
 qed
 
+
 text {* Any linear closure is a vector space. *}
 
-lemma lin_vs [intro?]:
-  "is_vectorspace V \<Longrightarrow> x \<in> V \<Longrightarrow> is_vectorspace (lin x)"
-proof (rule subspace_vs)
-  assume "is_vectorspace V"  "x \<in> V"
-  show "is_subspace (lin x) V" ..
-qed
-
+lemma (in vectorspace) lin_vectorspace [intro]:
+    "x \<in> V \<Longrightarrow> vectorspace (lin x)"
+  by (rule subvectorspace.vectorspace) (rule lin_subspace)
 
 
 subsection {* Sum of two vectorspaces *}
@@ -219,101 +208,92 @@
 instance set :: (plus) plus ..
 
 defs (overloaded)
-  vs_sum_def: "U + V \<equiv> {u + v | u v. u \<in> U \<and> v \<in> V}"
+  sum_def: "U + V \<equiv> {u + v | u v. u \<in> U \<and> v \<in> V}"
 
-lemma vs_sumD:
-  "(x \<in> U + V) = (\<exists>u \<in> U. \<exists>v \<in> V. x = u + v)"
-    by (unfold vs_sum_def) fast
+lemma sumE [elim]:
+    "x \<in> U + V \<Longrightarrow> (\<And>u v. x = u + v \<Longrightarrow> u \<in> U \<Longrightarrow> v \<in> V \<Longrightarrow> C) \<Longrightarrow> C"
+  by (unfold sum_def) blast
 
-lemmas vs_sumE = vs_sumD [THEN iffD1, elim_format, standard]
+lemma sumI [intro]:
+    "u \<in> U \<Longrightarrow> v \<in> V \<Longrightarrow> x = u + v \<Longrightarrow> x \<in> U + V"
+  by (unfold sum_def) blast
 
-lemma vs_sumI [intro?]:
-  "x \<in> U \<Longrightarrow> y \<in> V \<Longrightarrow> t = x + y \<Longrightarrow> t \<in> U + V"
-  by (unfold vs_sum_def) fast
+lemma sumI' [intro]:
+    "u \<in> U \<Longrightarrow> v \<in> V \<Longrightarrow> u + v \<in> U + V"
+  by (unfold sum_def) blast
 
 text {* @{text U} is a subspace of @{text "U + V"}. *}
 
-lemma subspace_vs_sum1 [intro?]:
-  "is_vectorspace U \<Longrightarrow> is_vectorspace V
-  \<Longrightarrow> is_subspace U (U + V)"
+lemma subspace_sum1 [iff]:
+  includes vectorspace U + vectorspace V
+  shows "U \<unlhd> U + V"
 proof
-  assume "is_vectorspace U"  "is_vectorspace V"
-  show "0 \<in> U" ..
+  show "U \<noteq> {}" ..
   show "U \<subseteq> U + V"
-  proof (intro subsetI vs_sumI)
-  fix x assume "x \<in> U"
-    show "x = x + 0" by (simp!)
-    show "0 \<in> V" by (simp!)
+  proof
+    fix x assume x: "x \<in> U"
+    moreover have "0 \<in> V" ..
+    ultimately have "x + 0 \<in> U + V" ..
+    with x show "x \<in> U + V" by simp
   qed
-  show "\<forall>x \<in> U. \<forall>y \<in> U. x + y \<in> U"
-  proof (intro ballI)
-    fix x y assume "x \<in> U"  "y \<in> U" show "x + y \<in> U" by (simp!)
-  qed
-  show "\<forall>x \<in> U. \<forall>a. a \<cdot> x \<in> U"
-  proof (intro ballI allI)
-    fix x a assume "x \<in> U" show "a \<cdot> x \<in> U" by (simp!)
-  qed
+  fix x y assume x: "x \<in> U" and "y \<in> U"
+  thus "x + y \<in> U" by simp
+  from x show "\<And>a. a \<cdot> x \<in> U" by simp
 qed
 
-text{* The sum of two subspaces is again a subspace.*}
+text {* The sum of two subspaces is again a subspace. *}
 
-lemma vs_sum_subspace [intro?]:
-  "is_subspace U E \<Longrightarrow> is_subspace V E \<Longrightarrow> is_vectorspace E
-  \<Longrightarrow> is_subspace (U + V) E"
+lemma sum_subspace [intro?]:
+  includes subvectorspace U E + subvectorspace V E
+  shows "U + V \<unlhd> E"
 proof
-  assume "is_subspace U E"  "is_subspace V E"  "is_vectorspace E"
-  show "0 \<in> U + V"
-  proof (intro vs_sumI)
+  have "0 \<in> U + V"
+  proof
     show "0 \<in> U" ..
     show "0 \<in> V" ..
-    show "(0::'a) = 0 + 0" by (simp!)
+    show "(0::'a) = 0 + 0" by simp
   qed
-
+  thus "U + V \<noteq> {}" by blast
   show "U + V \<subseteq> E"
-  proof (intro subsetI, elim vs_sumE bexE)
-    fix x u v assume "u \<in> U"  "v \<in> V"  "x = u + v"
-    show "x \<in> E" by (simp!)
+  proof
+    fix x assume "x \<in> U + V"
+    then obtain u v where x: "x = u + v" and
+      u: "u \<in> U" and v: "v \<in> V" ..
+    have "U \<unlhd> E" . with u have "u \<in> E" ..
+    moreover have "V \<unlhd> E" . with v have "v \<in> E" ..
+    ultimately show "x \<in> E" using x by simp
   qed
-
-  show "\<forall>x \<in> U + V. \<forall>y \<in> U + V. x + y \<in> U + V"
-  proof (intro ballI)
-    fix x y assume "x \<in> U + V"  "y \<in> U + V"
-    thus "x + y \<in> U + V"
-    proof (elim vs_sumE bexE, intro vs_sumI)
-      fix ux vx uy vy
-      assume "ux \<in> U"  "vx \<in> V"  "x = ux + vx"
-        and "uy \<in> U"  "vy \<in> V"  "y = uy + vy"
-      show "x + y = (ux + uy) + (vx + vy)" by (simp!)
-    qed (simp_all!)
+  fix x y assume x: "x \<in> U + V" and y: "y \<in> U + V"
+  show "x + y \<in> U + V"
+  proof -
+    from x obtain ux vx where "x = ux + vx" and "ux \<in> U" and "vx \<in> V" ..
+    moreover
+    from y obtain uy vy where "y = uy + vy" and "uy \<in> U" and "vy \<in> V" ..
+    ultimately
+    have "ux + uy \<in> U"
+      and "vx + vy \<in> V"
+      and "x + y = (ux + uy) + (vx + vy)"
+      using x y by (simp_all add: add_ac)
+    thus ?thesis ..
   qed
-
-  show "\<forall>x \<in> U + V. \<forall>a. a \<cdot> x \<in> U + V"
-  proof (intro ballI allI)
-    fix x a assume "x \<in> U + V"
-    thus "a \<cdot> x \<in> U + V"
-    proof (elim vs_sumE bexE, intro vs_sumI)
-      fix a x u v assume "u \<in> U"  "v \<in> V"  "x = u + v"
-      show "a \<cdot> x = (a \<cdot> u) + (a \<cdot> v)"
-        by (simp! add: vs_add_mult_distrib1)
-    qed (simp_all!)
+  fix a show "a \<cdot> x \<in> U + V"
+  proof -
+    from x obtain u v where "x = u + v" and "u \<in> U" and "v \<in> V" ..
+    hence "a \<cdot> u \<in> U" and "a \<cdot> v \<in> V"
+      and "a \<cdot> x = (a \<cdot> u) + (a \<cdot> v)" by (simp_all add: distrib)
+    thus ?thesis ..
   qed
 qed
 
 text{* The sum of two subspaces is a vectorspace. *}
 
-lemma vs_sum_vs [intro?]:
-  "is_subspace U E \<Longrightarrow> is_subspace V E \<Longrightarrow> is_vectorspace E
-  \<Longrightarrow> is_vectorspace (U + V)"
-proof (rule subspace_vs)
-  assume "is_subspace U E"  "is_subspace V E"  "is_vectorspace E"
-  show "is_subspace (U + V) E" ..
-qed
-
+lemma sum_vs [intro?]:
+    "U \<unlhd> E \<Longrightarrow> V \<unlhd> E \<Longrightarrow> vectorspace E \<Longrightarrow> vectorspace (U + V)"
+  by (rule subvectorspace.vectorspace) (rule sum_subspace)
 
 
 subsection {* Direct sums *}
 
-
 text {*
   The sum of @{text U} and @{text V} is called \emph{direct}, iff the
   zero element is the only common element of @{text U} and @{text
@@ -323,31 +303,35 @@
 *}
 
 lemma decomp:
-  "is_vectorspace E \<Longrightarrow> is_subspace U E \<Longrightarrow> is_subspace V E \<Longrightarrow>
-  U \<inter> V = {0} \<Longrightarrow> u1 \<in> U \<Longrightarrow> u2 \<in> U \<Longrightarrow> v1 \<in> V \<Longrightarrow> v2 \<in> V \<Longrightarrow>
-  u1 + v1 = u2 + v2 \<Longrightarrow> u1 = u2 \<and> v1 = v2"
+  includes vectorspace E + subspace U E + subspace V E
+  assumes direct: "U \<inter> V = {0}"
+    and u1: "u1 \<in> U" and u2: "u2 \<in> U"
+    and v1: "v1 \<in> V" and v2: "v2 \<in> V"
+    and sum: "u1 + v1 = u2 + v2"
+  shows "u1 = u2 \<and> v1 = v2"
 proof
-  assume "is_vectorspace E"  "is_subspace U E"  "is_subspace V E"
-    "U \<inter> V = {0}"  "u1 \<in> U"  "u2 \<in> U"  "v1 \<in> V"  "v2 \<in> V"
-    "u1 + v1 = u2 + v2"
-  have eq: "u1 - u2 = v2 - v1" by (simp! add: vs_add_diff_swap)
-  have u: "u1 - u2 \<in> U" by (simp!)
-  with eq have v': "v2 - v1 \<in> U" by simp
-  have v: "v2 - v1 \<in> V" by (simp!)
-  with eq have u': "u1 - u2 \<in> V" by simp
+  have U: "vectorspace U" by (rule subvectorspace.vectorspace)
+  have V: "vectorspace V" by (rule subvectorspace.vectorspace)
+  from u1 u2 v1 v2 and sum have eq: "u1 - u2 = v2 - v1"
+    by (simp add: add_diff_swap)
+  from u1 u2 have u: "u1 - u2 \<in> U"
+    by (rule vectorspace.diff_closed [OF U])
+  with eq have v': "v2 - v1 \<in> U" by (simp only:)
+  from v2 v1 have v: "v2 - v1 \<in> V"
+    by (rule vectorspace.diff_closed [OF V])
+  with eq have u': " u1 - u2 \<in> V" by (simp only:)
 
   show "u1 = u2"
-  proof (rule vs_add_minus_eq)
-    show "u1 - u2 = 0" by (rule Int_singletonD [OF _ u u'])
+  proof (rule add_minus_eq)
     show "u1 \<in> E" ..
     show "u2 \<in> E" ..
+    from u u' and direct show "u1 - u2 = 0" by blast
   qed
-
   show "v1 = v2"
-  proof (rule vs_add_minus_eq [symmetric])
-    show "v2 - v1 = 0" by (rule Int_singletonD [OF _ v' v])
+  proof (rule add_minus_eq [symmetric])
     show "v1 \<in> E" ..
     show "v2 \<in> E" ..
+    from v v' and direct show "v2 - v1 = 0" by blast
   qed
 qed
 
@@ -361,58 +345,48 @@
 *}
 
 lemma decomp_H':
-  "is_vectorspace E \<Longrightarrow> is_subspace H E \<Longrightarrow> y1 \<in> H \<Longrightarrow> y2 \<in> H \<Longrightarrow>
-  x' \<notin> H \<Longrightarrow> x' \<in> E \<Longrightarrow> x' \<noteq> 0 \<Longrightarrow> y1 + a1 \<cdot> x' = y2 + a2 \<cdot> x'
-  \<Longrightarrow> y1 = y2 \<and> a1 = a2"
+  includes vectorspace E + subvectorspace H E
+  assumes y1: "y1 \<in> H" and y2: "y2 \<in> H"
+    and x': "x' \<notin> H"  "x' \<in> E"  "x' \<noteq> 0"
+    and eq: "y1 + a1 \<cdot> x' = y2 + a2 \<cdot> x'"
+  shows "y1 = y2 \<and> a1 = a2"
 proof
-  assume "is_vectorspace E" and h: "is_subspace H E"
-     and "y1 \<in> H"  "y2 \<in> H"  "x' \<notin> H"  "x' \<in> E"  "x' \<noteq> 0"
-         "y1 + a1 \<cdot> x' = y2 + a2 \<cdot> x'"
-
   have c: "y1 = y2 \<and> a1 \<cdot> x' = a2 \<cdot> x'"
   proof (rule decomp)
     show "a1 \<cdot> x' \<in> lin x'" ..
     show "a2 \<cdot> x' \<in> lin x'" ..
-    show "H \<inter> (lin x') = {0}"
+    show "H \<inter> lin x' = {0}"
     proof
       show "H \<inter> lin x' \<subseteq> {0}"
-      proof (intro subsetI, elim IntE, rule singleton_iff [THEN iffD2])
-        fix x assume "x \<in> H"  "x \<in> lin x'"
-        thus "x = 0"
-        proof (unfold lin_def, elim CollectE exE conjE)
-          fix a assume "x = a \<cdot> x'"
-          show ?thesis
-          proof cases
-            assume "a = (0::real)" show ?thesis by (simp!)
-          next
-            assume "a \<noteq> (0::real)"
-            from h have "inverse a \<cdot> a \<cdot> x' \<in> H"
-              by (rule subspace_mult_closed) (simp!)
-            also have "inverse a \<cdot> a \<cdot> x' = x'" by (simp!)
-            finally have "x' \<in> H" .
-            thus ?thesis by contradiction
-          qed
-       qed
+      proof
+        fix x assume x: "x \<in> H \<inter> lin x'"
+        then obtain a where xx': "x = a \<cdot> x'"
+          by blast
+        have "x = 0"
+        proof cases
+          assume "a = 0"
+          with xx' and x' show ?thesis by simp
+        next
+          assume a: "a \<noteq> 0"
+          from x have "x \<in> H" ..
+          with xx' have "inverse a \<cdot> a \<cdot> x' \<in> H" by simp
+          with a and x' have "x' \<in> H" by (simp add: mult_assoc2)
+          thus ?thesis by contradiction
+        qed
+        thus "x \<in> {0}" ..
       qed
       show "{0} \<subseteq> H \<inter> lin x'"
       proof -
-        have "0 \<in> H \<inter> lin x'"
-        proof (rule IntI)
-          show "0 \<in> H" ..
-          from lin_vs show "0 \<in> lin x'" ..
-        qed
-        thus ?thesis by simp
+        have "0 \<in> H" ..
+        moreover have "0 \<in> lin x'" ..
+        ultimately show ?thesis by blast
       qed
     qed
-    show "is_subspace (lin x') E" ..
+    show "lin x' \<unlhd> E" ..
   qed
-
-  from c show "y1 = y2" by simp
-
-  show  "a1 = a2"
-  proof (rule vs_mult_right_cancel [THEN iffD1])
-    from c show "a1 \<cdot> x' = a2 \<cdot> x'" by simp
-  qed
+  thus "y1 = y2" ..
+  from c have "a1 \<cdot> x' = a2 \<cdot> x'" ..
+  with x' show "a1 = a2" by (simp add: mult_right_cancel)
 qed
 
 text {*
@@ -423,18 +397,20 @@
 *}
 
 lemma decomp_H'_H:
-  "is_vectorspace E \<Longrightarrow> is_subspace H E \<Longrightarrow> t \<in> H \<Longrightarrow> x' \<notin> H \<Longrightarrow> x' \<in> E
-  \<Longrightarrow> x' \<noteq> 0
-  \<Longrightarrow> (SOME (y, a). t = y + a \<cdot> x' \<and> y \<in> H) = (t, (0::real))"
-proof (rule, unfold split_tupled_all)
-  assume "is_vectorspace E"  "is_subspace H E"  "t \<in> H"  "x' \<notin> H"  "x' \<in> E"
-    "x' \<noteq> 0"
-  have h: "is_vectorspace H" ..
-  fix y a presume t1: "t = y + a \<cdot> x'" and "y \<in> H"
-  have "y = t \<and> a = (0::real)"
-    by (rule decomp_H') (auto!)
-  thus "(y, a) = (t, (0::real))" by (simp!)
-qed (simp_all!)
+  includes vectorspace E + subvectorspace H E
+  assumes t: "t \<in> H"
+    and x': "x' \<notin> H"  "x' \<in> E"  "x' \<noteq> 0"
+  shows "(SOME (y, a). t = y + a \<cdot> x' \<and> y \<in> H) = (t, 0)"
+proof (rule, simp_all only: split_paired_all split_conv)
+  from t x' show "t = t + 0 \<cdot> x' \<and> t \<in> H" by simp
+  fix y and a assume ya: "t = y + a \<cdot> x' \<and> y \<in> H"
+  have "y = t \<and> a = 0"
+  proof (rule decomp_H')
+    from ya x' show "y + a \<cdot> x' = t + 0 \<cdot> x'" by simp
+    from ya show "y \<in> H" ..
+  qed
+  with t x' show "(y, a) = (y + a \<cdot> x', 0)" by simp
+qed
 
 text {*
   The components @{text "y \<in> H"} and @{text a} in @{text "y + a \<cdot> x'"}
@@ -443,42 +419,41 @@
 *}
 
 lemma h'_definite:
-  "h' \<equiv> (\<lambda>x. let (y, a) = SOME (y, a). (x = y + a \<cdot> x' \<and> y \<in> H)
-                in (h y) + a * xi) \<Longrightarrow>
-  x = y + a \<cdot> x' \<Longrightarrow> is_vectorspace E \<Longrightarrow> is_subspace H E \<Longrightarrow>
-  y \<in> H \<Longrightarrow> x' \<notin> H \<Longrightarrow> x' \<in> E \<Longrightarrow> x' \<noteq> 0
-  \<Longrightarrow> h' x = h y + a * xi"
+  includes var H
+  assumes h'_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)"
+    and x: "x = y + a \<cdot> x'"
+  includes vectorspace E + subvectorspace H E
+  assumes y: "y \<in> H"
+    and x': "x' \<notin> H"  "x' \<in> E"  "x' \<noteq> 0"
+  shows "h' x = h y + a * xi"
 proof -
-  assume
-    "h' \<equiv> (\<lambda>x. let (y, a) = SOME (y, a). (x = y + a \<cdot> x' \<and> y \<in> H)
-               in (h y) + a * xi)"
-    "x = y + a \<cdot> x'"  "is_vectorspace E"  "is_subspace H E"
-    "y \<in> H"  "x' \<notin> H"  "x' \<in> E"  "x' \<noteq> 0"
-  hence "x \<in> H + (lin x')"
-    by (auto simp add: vs_sum_def lin_def)
-  have "\<exists>! xa. ((\<lambda>(y, a). x = y + a \<cdot> x' \<and> y \<in> H) xa)"
+  from x y x' have "x \<in> H + lin x'" by auto
+  have "\<exists>!p. (\<lambda>(y, a). x = y + a \<cdot> x' \<and> y \<in> H) p" (is "\<exists>!p. ?P p")
   proof
-    show "\<exists>xa. ((\<lambda>(y, a). x = y + a \<cdot> x' \<and> y \<in> H) xa)"
-      by (blast!)
-  next
-    fix xa ya
-    assume "(\<lambda>(y,a). x = y + a \<cdot> x' \<and> y \<in> H) xa"
-           "(\<lambda>(y,a). x = y + a \<cdot> x' \<and> y \<in> H) ya"
-    show "xa = ya"
+    from x y show "\<exists>p. ?P p" by blast
+    fix p q assume p: "?P p" and q: "?P q"
+    show "p = q"
     proof -
-      show "fst xa = fst ya \<and> snd xa = snd ya \<Longrightarrow> xa = ya"
-        by (simp add: Pair_fst_snd_eq)
-      have x: "x = fst xa + snd xa \<cdot> x' \<and> fst xa \<in> H"
-        by (auto!)
-      have y: "x = fst ya + snd ya \<cdot> x' \<and> fst ya \<in> H"
-        by (auto!)
-      from x y show "fst xa = fst ya \<and> snd xa = snd ya"
-        by (elim conjE) (rule decomp_H', (simp!)+)
+      from p have xp: "x = fst p + snd p \<cdot> x' \<and> fst p \<in> H"
+        by (cases p) simp
+      from q have xq: "x = fst q + snd q \<cdot> x' \<and> fst q \<in> H"
+        by (cases q) simp
+      have "fst p = fst q \<and> snd p = snd q"
+      proof (rule decomp_H')
+        from xp show "fst p \<in> H" ..
+        from xq show "fst q \<in> H" ..
+        from xp and xq show "fst p + snd p \<cdot> x' = fst q + snd q \<cdot> x'"
+          by simp
+        apply_end assumption+
+      qed
+      thus ?thesis by (cases p, cases q) simp
     qed
   qed
   hence eq: "(SOME (y, a). x = y + a \<cdot> x' \<and> y \<in> H) = (y, a)"
-    by (rule some1_equality) (blast!)
-  thus "h' x = h y + a * xi" by (simp! add: Let_def)
+    by (rule some1_equality) (simp add: x y)
+  with h'_def show "h' x = h y + a * xi" by (simp add: Let_def)
 qed
 
 end
diff -r cc3bbaf1b8d3 -r a6a7025fd7e8 src/HOL/Real/HahnBanach/VectorSpace.thy
--- a/src/HOL/Real/HahnBanach/VectorSpace.thy	Thu Aug 22 12:28:41 2002 +0200
+++ b/src/HOL/Real/HahnBanach/VectorSpace.thy	Thu Aug 22 20:49:43 2002 +0200
@@ -5,7 +5,7 @@
 
 header {* Vector spaces *}
 
-theory VectorSpace = Bounds + Aux:
+theory VectorSpace = Aux:
 
 subsection {* Signature *}
 
@@ -35,459 +35,379 @@
   the neutral element of scalar multiplication.
 *}
 
-constdefs
-  is_vectorspace :: "('a::{plus, minus, zero}) set \<Rightarrow> bool"
-  "is_vectorspace V \<equiv> V \<noteq> {}
-   \<and> (\<forall>x \<in> V. \<forall>y \<in> V. \<forall>z \<in> V. \<forall>a b.
-        x + y \<in> V
-      \<and> a \<cdot> x \<in> V
-      \<and> (x + y) + z = x + (y + z)
-      \<and> x + y = y + x
-      \<and> x - x = 0
-      \<and> 0 + x = x
-      \<and> a \<cdot> (x + y) = a \<cdot> x + a \<cdot> y
-      \<and> (a + b) \<cdot> x = a \<cdot> x + b \<cdot> x
-      \<and> (a * b) \<cdot> x = a \<cdot> b \<cdot> x
-      \<and> 1 \<cdot> x = x
-      \<and> - x = (- 1) \<cdot> x
-      \<and> x - y = x + - y)"
-
-
-text {* \medskip The corresponding introduction rule is:*}
-
-lemma vsI [intro]:
-  "0 \<in> V \<Longrightarrow>
-  \<forall>x \<in> V. \<forall>y \<in> V. x + y \<in> V \<Longrightarrow>
-  \<forall>x \<in> V. \<forall>a. a \<cdot> x \<in> V \<Longrightarrow>
-  \<forall>x \<in> V. \<forall>y \<in> V. \<forall>z \<in> V. (x + y) + z = x + (y + z) \<Longrightarrow>
-  \<forall>x \<in> V. \<forall>y \<in> V. x + y = y + x \<Longrightarrow>
-  \<forall>x \<in> V. x - x = 0 \<Longrightarrow>
-  \<forall>x \<in> V. 0 + x = x \<Longrightarrow>
-  \<forall>x \<in> V. \<forall>y \<in> V. \<forall>a. a \<cdot> (x + y) = a \<cdot> x + a \<cdot> y \<Longrightarrow>
-  \<forall>x \<in> V. \<forall>a b. (a + b) \<cdot> x = a \<cdot> x + b \<cdot> x \<Longrightarrow>
-  \<forall>x \<in> V. \<forall>a b. (a * b) \<cdot> x = a \<cdot> b \<cdot> x \<Longrightarrow>
-  \<forall>x \<in> V. 1 \<cdot> x = x \<Longrightarrow>
-  \<forall>x \<in> V. - x = (- 1) \<cdot> x \<Longrightarrow>
-  \<forall>x \<in> V. \<forall>y \<in> V. x - y = x + - y \<Longrightarrow> is_vectorspace V"
-  by (unfold is_vectorspace_def) auto
+locale vectorspace = var V +
+  assumes non_empty [iff, intro?]: "V \<noteq> {}"
+    and add_closed [iff]: "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> x + y \<in> V"
+    and mult_closed [iff]: "x \<in> V \<Longrightarrow> a \<cdot> x \<in> V"
+    and add_assoc: "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> z \<in> V \<Longrightarrow> (x + y) + z = x + (y + z)"
+    and add_commute: "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> x + y = y + x"
+    and diff_self [simp]: "x \<in> V \<Longrightarrow> x - x = 0"
+    and add_zero_left [simp]: "x \<in> V \<Longrightarrow> 0 + x = x"
+    and add_mult_distrib1: "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> a \<cdot> (x + y) = a \<cdot> x + a \<cdot> y"
+    and add_mult_distrib2: "x \<in> V \<Longrightarrow> (a + b) \<cdot> x = a \<cdot> x + b \<cdot> x"
+    and mult_assoc: "x \<in> V \<Longrightarrow> (a * b) \<cdot> x = a \<cdot> (b \<cdot> x)"
+    and mult_1 [simp]: "x \<in> V \<Longrightarrow> 1 \<cdot> x = x"
+    and negate_eq1: "x \<in> V \<Longrightarrow> - x = (- 1) \<cdot> x"
+    and diff_eq1: "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> x - y = x + - y"
 
-text {* \medskip The corresponding destruction rules are: *}
-
-lemma negate_eq1:
-  "is_vectorspace V \<Longrightarrow> x \<in> V \<Longrightarrow> - x = (- 1) \<cdot> x"
-  by (unfold is_vectorspace_def) simp
-
-lemma diff_eq1:
-  "is_vectorspace V \<Longrightarrow> x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> x - y = x + - y"
-  by (unfold is_vectorspace_def) simp
-
-lemma negate_eq2:
-  "is_vectorspace V \<Longrightarrow> x \<in> V \<Longrightarrow> (- 1) \<cdot> x = - x"
-  by (unfold is_vectorspace_def) simp
-
-lemma negate_eq2a:
-  "is_vectorspace V \<Longrightarrow> x \<in> V \<Longrightarrow> -1 \<cdot> x = - x"
-  by (unfold is_vectorspace_def) simp
+lemma (in vectorspace) negate_eq2: "x \<in> V \<Longrightarrow> (- 1) \<cdot> x = - x"
+  by (rule negate_eq1 [symmetric])
 
-lemma diff_eq2:
-  "is_vectorspace V \<Longrightarrow> x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> x + - y = x - y"
-  by (unfold is_vectorspace_def) simp
-
-lemma vs_not_empty [intro?]: "is_vectorspace V \<Longrightarrow> (V \<noteq> {})"
-  by (unfold is_vectorspace_def) simp
+lemma (in vectorspace) negate_eq2a: "x \<in> V \<Longrightarrow> -1 \<cdot> x = - x"
+  by (simp add: negate_eq1)
 
-lemma vs_add_closed [simp, intro?]:
-  "is_vectorspace V \<Longrightarrow> x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> x + y \<in> V"
-  by (unfold is_vectorspace_def) simp
+lemma (in vectorspace) diff_eq2: "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> x + - y = x - y"
+  by (rule diff_eq1 [symmetric])
 
-lemma vs_mult_closed [simp, intro?]:
-  "is_vectorspace V \<Longrightarrow> x \<in> V \<Longrightarrow> a \<cdot> x \<in> V"
-  by (unfold is_vectorspace_def) simp
-
-lemma vs_diff_closed [simp, intro?]:
- "is_vectorspace V \<Longrightarrow> x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> x - y \<in> V"
+lemma (in vectorspace) diff_closed [iff]: "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> x - y \<in> V"
   by (simp add: diff_eq1 negate_eq1)
 
-lemma vs_neg_closed  [simp, intro?]:
-  "is_vectorspace V \<Longrightarrow> x \<in> V \<Longrightarrow> - x \<in> V"
+lemma (in vectorspace) neg_closed [iff]: "x \<in> V \<Longrightarrow> - x \<in> V"
   by (simp add: negate_eq1)
 
-lemma vs_add_assoc [simp]:
-  "is_vectorspace V \<Longrightarrow> x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> z \<in> V
-   \<Longrightarrow> (x + y) + z = x + (y + z)"
-  by (unfold is_vectorspace_def) blast
-
-lemma vs_add_commute [simp]:
-  "is_vectorspace V \<Longrightarrow> x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> y + x = x + y"
-  by (unfold is_vectorspace_def) blast
-
-lemma vs_add_left_commute [simp]:
-  "is_vectorspace V \<Longrightarrow> x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> z \<in> V
-  \<Longrightarrow> x + (y + z) = y + (x + z)"
+lemma (in vectorspace) add_left_commute:
+  "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> z \<in> V \<Longrightarrow> x + (y + z) = y + (x + z)"
 proof -
-  assume "is_vectorspace V"  "x \<in> V"  "y \<in> V"  "z \<in> V"
+  assume xyz: "x \<in> V"  "y \<in> V"  "z \<in> V"
   hence "x + (y + z) = (x + y) + z"
-    by (simp only: vs_add_assoc)
-  also have "... = (y + x) + z" by (simp! only: vs_add_commute)
-  also have "... = y + (x + z)" by (simp! only: vs_add_assoc)
+    by (simp only: add_assoc)
+  also from xyz have "... = (y + x) + z" by (simp only: add_commute)
+  also from xyz have "... = y + (x + z)" by (simp only: add_assoc)
   finally show ?thesis .
 qed
 
-theorems vs_add_ac = vs_add_assoc vs_add_commute vs_add_left_commute
+theorems (in vectorspace) add_ac =
+  add_assoc add_commute add_left_commute
 
-lemma vs_diff_self [simp]:
-  "is_vectorspace V \<Longrightarrow> x \<in> V \<Longrightarrow> x - x = 0"
-  by (unfold is_vectorspace_def) simp
 
 text {* The existence of the zero element of a vector space
-follows from the non-emptiness of carrier set. *}
+  follows from the non-emptiness of carrier set. *}
 
-lemma zero_in_vs [simp, intro]: "is_vectorspace V \<Longrightarrow> 0 \<in> V"
+lemma (in vectorspace) zero [iff]: "0 \<in> V"
 proof -
-  assume "is_vectorspace V"
-  have "V \<noteq> {}" ..
-  then obtain x where "x \<in> V" by blast
-  have "0 = x - x" by (simp!)
-  also have "... \<in> V" by (simp! only: vs_diff_closed)
+  from non_empty obtain x where x: "x \<in> V" by blast
+  then have "0 = x - x" by (rule diff_self [symmetric])
+  also from x have "... \<in> V" by (rule diff_closed)
   finally show ?thesis .
 qed
 
-lemma vs_add_zero_left [simp]:
-  "is_vectorspace V \<Longrightarrow> x \<in> V \<Longrightarrow>  0 + x = x"
-  by (unfold is_vectorspace_def) simp
-
-lemma vs_add_zero_right [simp]:
-  "is_vectorspace V \<Longrightarrow> x \<in> V \<Longrightarrow>  x + 0 = x"
+lemma (in vectorspace) add_zero_right [simp]:
+  "x \<in> V \<Longrightarrow>  x + 0 = x"
 proof -
-  assume "is_vectorspace V"  "x \<in> V"
-  hence "x + 0 = 0 + x" by simp
-  also have "... = x" by (simp!)
+  assume x: "x \<in> V"
+  from this and zero have "x + 0 = 0 + x" by (rule add_commute)
+  also from x have "... = x" by (rule add_zero_left)
   finally show ?thesis .
 qed
 
-lemma vs_add_mult_distrib1:
-  "is_vectorspace V \<Longrightarrow> x \<in> V \<Longrightarrow> y \<in> V
-  \<Longrightarrow> a \<cdot> (x + y) = a \<cdot> x + a \<cdot> y"
-  by (unfold is_vectorspace_def) simp
+lemma (in vectorspace) mult_assoc2:
+    "x \<in> V \<Longrightarrow> a \<cdot> b \<cdot> x = (a * b) \<cdot> x"
+  by (simp only: mult_assoc)
 
-lemma vs_add_mult_distrib2:
-  "is_vectorspace V \<Longrightarrow> x \<in> V
-  \<Longrightarrow> (a + b) \<cdot> x = a \<cdot> x + b \<cdot> x"
-  by (unfold is_vectorspace_def) simp
-
-lemma vs_mult_assoc:
-  "is_vectorspace V \<Longrightarrow> x \<in> V \<Longrightarrow> (a * b) \<cdot> x = a \<cdot> (b \<cdot> x)"
-  by (unfold is_vectorspace_def) simp
-
-lemma vs_mult_assoc2 [simp]:
- "is_vectorspace V \<Longrightarrow> x \<in> V \<Longrightarrow> a \<cdot> b \<cdot> x = (a * b) \<cdot> x"
-  by (simp only: vs_mult_assoc)
+lemma (in vectorspace) diff_mult_distrib1:
+    "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> a \<cdot> (x - y) = a \<cdot> x - a \<cdot> y"
+  by (simp add: diff_eq1 negate_eq1 add_mult_distrib1 mult_assoc2)
 
-lemma vs_mult_1 [simp]:
-  "is_vectorspace V \<Longrightarrow> x \<in> V \<Longrightarrow> 1 \<cdot> x = x"
-  by (unfold is_vectorspace_def) simp
-
-lemma vs_diff_mult_distrib1:
-  "is_vectorspace V \<Longrightarrow> x \<in> V \<Longrightarrow> y \<in> V
-  \<Longrightarrow> a \<cdot> (x - y) = a \<cdot> x - a \<cdot> y"
-  by (simp add: diff_eq1 negate_eq1 vs_add_mult_distrib1)
-
-lemma vs_diff_mult_distrib2:
-  "is_vectorspace V \<Longrightarrow> x \<in> V
-  \<Longrightarrow> (a - b) \<cdot> x = a \<cdot> x - (b \<cdot> x)"
+lemma (in vectorspace) diff_mult_distrib2:
+  "x \<in> V \<Longrightarrow> (a - b) \<cdot> x = a \<cdot> x - (b \<cdot> x)"
 proof -
-  assume "is_vectorspace V"  "x \<in> V"
+  assume x: "x \<in> V"
   have " (a - b) \<cdot> x = (a + - b) \<cdot> x"
-    by (unfold real_diff_def, simp)
+    by (simp add: real_diff_def)
   also have "... = a \<cdot> x + (- b) \<cdot> x"
-    by (rule vs_add_mult_distrib2)
-  also have "... = a \<cdot> x + - (b \<cdot> x)"
-    by (simp! add: negate_eq1)
-  also have "... = a \<cdot> x - (b \<cdot> x)"
-    by (simp! add: diff_eq1)
+    by (rule add_mult_distrib2)
+  also from x have "... = a \<cdot> x + - (b \<cdot> x)"
+    by (simp add: negate_eq1 mult_assoc2)
+  also from x have "... = a \<cdot> x - (b \<cdot> x)"
+    by (simp add: diff_eq1)
   finally show ?thesis .
 qed
 
+lemmas (in vectorspace) distrib =
+  add_mult_distrib1 add_mult_distrib2
+  diff_mult_distrib1 diff_mult_distrib2
+
 
 text {* \medskip Further derived laws: *}
 
-lemma vs_mult_zero_left [simp]:
-  "is_vectorspace V \<Longrightarrow> x \<in> V \<Longrightarrow> 0 \<cdot> x = 0"
+lemma (in vectorspace) mult_zero_left [simp]:
+  "x \<in> V \<Longrightarrow> 0 \<cdot> x = 0"
 proof -
-  assume "is_vectorspace V"  "x \<in> V"
-  have  "0 \<cdot> x = (1 - 1) \<cdot> x" by simp
+  assume x: "x \<in> V"
+  have "0 \<cdot> x = (1 - 1) \<cdot> x" by simp
   also have "... = (1 + - 1) \<cdot> x" by simp
   also have "... =  1 \<cdot> x + (- 1) \<cdot> x"
-    by (rule vs_add_mult_distrib2)
-  also have "... = x + (- 1) \<cdot> x" by (simp!)
-  also have "... = x + - x" by (simp! add: negate_eq2a)
-  also have "... = x - x" by (simp! add: diff_eq2)
-  also have "... = 0" by (simp!)
+    by (rule add_mult_distrib2)
+  also from x have "... = x + (- 1) \<cdot> x" by simp
+  also from x have "... = x + - x" by (simp add: negate_eq2a)
+  also from x have "... = x - x" by (simp add: diff_eq2)
+  also from x have "... = 0" by simp
   finally show ?thesis .
 qed
 
-lemma vs_mult_zero_right [simp]:
-  "is_vectorspace (V:: 'a::{plus, minus, zero} set)
-  \<Longrightarrow> a \<cdot> 0 = (0::'a)"
+lemma (in vectorspace) mult_zero_right [simp]:
+  "a \<cdot> 0 = (0::'a)"
 proof -
-  assume "is_vectorspace V"
-  have "a \<cdot> 0 = a \<cdot> (0 - (0::'a))" by (simp!)
+  have "a \<cdot> 0 = a \<cdot> (0 - (0::'a))" by simp
   also have "... =  a \<cdot> 0 - a \<cdot> 0"
-     by (rule vs_diff_mult_distrib1) (simp!)+
-  also have "... = 0" by (simp!)
+    by (rule diff_mult_distrib1) simp_all
+  also have "... = 0" by simp
   finally show ?thesis .
 qed
 
-lemma vs_minus_mult_cancel [simp]:
-  "is_vectorspace V \<Longrightarrow> x \<in> V \<Longrightarrow> (- a) \<cdot> - x = a \<cdot> x"
-  by (simp add: negate_eq1)
+lemma (in vectorspace) minus_mult_cancel [simp]:
+    "x \<in> V \<Longrightarrow> (- a) \<cdot> - x = a \<cdot> x"
+  by (simp add: negate_eq1 mult_assoc2)
 
-lemma vs_add_minus_left_eq_diff:
-  "is_vectorspace V \<Longrightarrow> x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> - x + y = y - x"
+lemma (in vectorspace) add_minus_left_eq_diff:
+  "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> - x + y = y - x"
 proof -
-  assume "is_vectorspace V"  "x \<in> V"  "y \<in> V"
-  hence "- x + y = y + - x"
-    by (simp add: vs_add_commute)
-  also have "... = y - x" by (simp! add: diff_eq1)
+  assume xy: "x \<in> V"  "y \<in> V"
+  hence "- x + y = y + - x" by (simp add: add_commute)
+  also from xy have "... = y - x" by (simp add: diff_eq1)
   finally show ?thesis .
 qed
 
-lemma vs_add_minus [simp]:
-  "is_vectorspace V \<Longrightarrow> x \<in> V \<Longrightarrow> x + - x = 0"
-  by (simp! add: diff_eq2)
+lemma (in vectorspace) add_minus [simp]:
+    "x \<in> V \<Longrightarrow> x + - x = 0"
+  by (simp add: diff_eq2)
 
-lemma vs_add_minus_left [simp]:
-  "is_vectorspace V \<Longrightarrow> x \<in> V \<Longrightarrow> - x + x = 0"
-  by (simp! add: diff_eq2)
+lemma (in vectorspace) add_minus_left [simp]:
+    "x \<in> V \<Longrightarrow> - x + x = 0"
+  by (simp add: diff_eq2 add_commute)
 
-lemma vs_minus_minus [simp]:
-  "is_vectorspace V \<Longrightarrow> x \<in> V \<Longrightarrow> - (- x) = x"
+lemma (in vectorspace) minus_minus [simp]:
+    "x \<in> V \<Longrightarrow> - (- x) = x"
+  by (simp add: negate_eq1 mult_assoc2)
+
+lemma (in vectorspace) minus_zero [simp]:
+    "- (0::'a) = 0"
   by (simp add: negate_eq1)
 
-lemma vs_minus_zero [simp]:
-  "is_vectorspace (V::'a::{plus, minus, zero} set) \<Longrightarrow> - (0::'a) = 0"
-  by (simp add: negate_eq1)
-
-lemma vs_minus_zero_iff [simp]:
-  "is_vectorspace V \<Longrightarrow> x \<in> V \<Longrightarrow> (- x = 0) = (x = 0)"
-  (concl is "?L = ?R")
-proof -
-  assume "is_vectorspace V"  "x \<in> V"
-  show "?L = ?R"
-  proof
-    have "x = - (- x)" by (simp! add: vs_minus_minus)
-    also assume ?L
-    also have "- ... = 0" by (rule vs_minus_zero)
-    finally show ?R .
-  qed (simp!)
+lemma (in vectorspace) minus_zero_iff [simp]:
+  "x \<in> V \<Longrightarrow> (- x = 0) = (x = 0)"
+proof
+  assume x: "x \<in> V"
+  {
+    from x have "x = - (- x)" by (simp add: minus_minus)
+    also assume "- x = 0"
+    also have "- ... = 0" by (rule minus_zero)
+    finally show "x = 0" .
+  next
+    assume "x = 0"
+    then show "- x = 0" by simp
+  }
 qed
 
-lemma vs_add_minus_cancel [simp]:
-  "is_vectorspace V \<Longrightarrow> x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> x + (- x + y) = y"
-  by (simp add: vs_add_assoc [symmetric] del: vs_add_commute)
+lemma (in vectorspace) add_minus_cancel [simp]:
+    "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> x + (- x + y) = y"
+  by (simp add: add_assoc [symmetric] del: add_commute)
 
-lemma vs_minus_add_cancel [simp]:
-  "is_vectorspace V \<Longrightarrow> x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> - x + (x + y) = y"
-  by (simp add: vs_add_assoc [symmetric] del: vs_add_commute)
+lemma (in vectorspace) minus_add_cancel [simp]:
+    "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> - x + (x + y) = y"
+  by (simp add: add_assoc [symmetric] del: add_commute)
 
-lemma vs_minus_add_distrib [simp]:
-  "is_vectorspace V \<Longrightarrow> x \<in> V \<Longrightarrow> y \<in> V
-  \<Longrightarrow> - (x + y) = - x + - y"
-  by (simp add: negate_eq1 vs_add_mult_distrib1)
+lemma (in vectorspace) minus_add_distrib [simp]:
+    "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> - (x + y) = - x + - y"
+  by (simp add: negate_eq1 add_mult_distrib1)
 
-lemma vs_diff_zero [simp]:
-  "is_vectorspace V \<Longrightarrow> x \<in> V \<Longrightarrow> x - 0 = x"
+lemma (in vectorspace) diff_zero [simp]:
+    "x \<in> V \<Longrightarrow> x - 0 = x"
+  by (simp add: diff_eq1)
+
+lemma (in vectorspace) diff_zero_right [simp]:
+    "x \<in> V \<Longrightarrow> 0 - x = - x"
   by (simp add: diff_eq1)
 
-lemma vs_diff_zero_right [simp]:
-  "is_vectorspace V \<Longrightarrow> x \<in> V \<Longrightarrow> 0 - x = - x"
-  by (simp add:diff_eq1)
-
-lemma vs_add_left_cancel:
-  "is_vectorspace V \<Longrightarrow> x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> z \<in> V
-   \<Longrightarrow> (x + y = x + z) = (y = z)"
-  (concl is "?L = ?R")
+lemma (in vectorspace) add_left_cancel:
+  "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> z \<in> V \<Longrightarrow> (x + y = x + z) = (y = z)"
 proof
-  assume "is_vectorspace V"  "x \<in> V"  "y \<in> V"  "z \<in> V"
-  have "y = 0 + y" by (simp!)
-  also have "... = - x + x + y" by (simp!)
-  also have "... = - x + (x + y)"
-    by (simp! only: vs_add_assoc vs_neg_closed)
-  also assume "x + y = x + z"
-  also have "- x + (x + z) = - x + x + z"
-    by (simp! only: vs_add_assoc [symmetric] vs_neg_closed)
-  also have "... = z" by (simp!)
-  finally show ?R .
-qed blast
+  assume x: "x \<in> V" and y: "y \<in> V" and z: "z \<in> V"
+  {
+    from y have "y = 0 + y" by simp
+    also from x y have "... = (- x + x) + y" by simp
+    also from x y have "... = - x + (x + y)"
+      by (simp add: add_assoc neg_closed)
+    also assume "x + y = x + z"
+    also from x z have "- x + (x + z) = - x + x + z"
+      by (simp add: add_assoc [symmetric] neg_closed)
+    also from x z have "... = z" by simp
+    finally show "y = z" .
+  next
+    assume "y = z"
+    then show "x + y = x + z" by (simp only:)
+  }
+qed
 
-lemma vs_add_right_cancel:
-  "is_vectorspace V \<Longrightarrow> x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> z \<in> V
-  \<Longrightarrow> (y + x = z + x) = (y = z)"
-  by (simp only: vs_add_commute vs_add_left_cancel)
+lemma (in vectorspace) add_right_cancel:
+    "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> z \<in> V \<Longrightarrow> (y + x = z + x) = (y = z)"
+  by (simp only: add_commute add_left_cancel)
 
-lemma vs_add_assoc_cong:
-  "is_vectorspace V \<Longrightarrow> x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> x' \<in> V \<Longrightarrow> y' \<in> V \<Longrightarrow> z \<in> V
-  \<Longrightarrow> x + y = x' + y' \<Longrightarrow> x + (y + z) = x' + (y' + z)"
-  by (simp only: vs_add_assoc [symmetric])
+lemma (in vectorspace) add_assoc_cong:
+  "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> x' \<in> V \<Longrightarrow> y' \<in> V \<Longrightarrow> z \<in> V
+    \<Longrightarrow> x + y = x' + y' \<Longrightarrow> x + (y + z) = x' + (y' + z)"
+  by (simp only: add_assoc [symmetric])
 
-lemma vs_mult_left_commute:
-  "is_vectorspace V \<Longrightarrow> x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> z \<in> V
-  \<Longrightarrow> x \<cdot> y \<cdot> z = y \<cdot> x \<cdot> z"
-  by (simp add: real_mult_commute)
+lemma (in vectorspace) mult_left_commute:
+    "x \<in> V \<Longrightarrow> a \<cdot> b \<cdot> x = b \<cdot> a \<cdot> x"
+  by (simp add: real_mult_commute mult_assoc2)
 
-lemma vs_mult_zero_uniq:
-  "is_vectorspace V \<Longrightarrow> x \<in> V \<Longrightarrow> x \<noteq> 0 \<Longrightarrow> a \<cdot> x = 0 \<Longrightarrow> a = 0"
+lemma (in vectorspace) mult_zero_uniq:
+  "x \<in> V \<Longrightarrow> x \<noteq> 0 \<Longrightarrow> a \<cdot> x = 0 \<Longrightarrow> a = 0"
 proof (rule classical)
-  assume "is_vectorspace V"  "x \<in> V"  "a \<cdot> x = 0"  "x \<noteq> 0"
-  assume "a \<noteq> 0"
-  have "x = (inverse a * a) \<cdot> x" by (simp!)
-  also have "... = inverse a \<cdot> (a \<cdot> x)" by (rule vs_mult_assoc)
-  also have "... = inverse a \<cdot> 0" by (simp!)
-  also have "... = 0" by (simp!)
+  assume a: "a \<noteq> 0"
+  assume x: "x \<in> V"  "x \<noteq> 0" and ax: "a \<cdot> x = 0"
+  from x a have "x = (inverse a * a) \<cdot> x" by simp
+  also have "... = inverse a \<cdot> (a \<cdot> x)" by (rule mult_assoc)
+  also from ax have "... = inverse a \<cdot> 0" by simp
+  also have "... = 0" by simp
   finally have "x = 0" .
   thus "a = 0" by contradiction
 qed
 
-lemma vs_mult_left_cancel:
-  "is_vectorspace V \<Longrightarrow> x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> a \<noteq> 0 \<Longrightarrow>
-  (a \<cdot> x = a \<cdot> y) = (x = y)"
-  (concl is "?L = ?R")
+lemma (in vectorspace) mult_left_cancel:
+  "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> a \<noteq> 0 \<Longrightarrow> (a \<cdot> x = a \<cdot> y) = (x = y)"
 proof
-  assume "is_vectorspace V"  "x \<in> V"  "y \<in> V"  "a \<noteq> 0"
-  have "x = 1 \<cdot> x" by (simp!)
-  also have "... = (inverse a * a) \<cdot> x" by (simp!)
-  also have "... = inverse a \<cdot> (a \<cdot> x)"
-    by (simp! only: vs_mult_assoc)
-  also assume ?L
-  also have "inverse a \<cdot> ... = y" by (simp!)
-  finally show ?R .
-qed simp
+  assume x: "x \<in> V" and y: "y \<in> V" and a: "a \<noteq> 0"
+  from x have "x = 1 \<cdot> x" by simp
+  also from a have "... = (inverse a * a) \<cdot> x" by simp
+  also from x have "... = inverse a \<cdot> (a \<cdot> x)"
+    by (simp only: mult_assoc)
+  also assume "a \<cdot> x = a \<cdot> y"
+  also from a y have "inverse a \<cdot> ... = y"
+    by (simp add: mult_assoc2)
+  finally show "x = y" .
+next
+  assume "x = y"
+  then show "a \<cdot> x = a \<cdot> y" by (simp only:)
+qed
 
-lemma vs_mult_right_cancel: (*** forward ***)
-  "is_vectorspace V \<Longrightarrow> x \<in> V \<Longrightarrow> x \<noteq> 0
-  \<Longrightarrow> (a \<cdot> x = b \<cdot> x) = (a = b)" (concl is "?L = ?R")
+lemma (in vectorspace) mult_right_cancel:
+  "x \<in> V \<Longrightarrow> x \<noteq> 0 \<Longrightarrow> (a \<cdot> x = b \<cdot> x) = (a = b)"
 proof
-  assume v: "is_vectorspace V"  "x \<in> V"  "x \<noteq> 0"
-  have "(a - b) \<cdot> x = a \<cdot> x - b \<cdot> x"
-    by (simp! add: vs_diff_mult_distrib2)
-  also assume ?L hence "a \<cdot> x - b \<cdot> x = 0" by (simp!)
-  finally have "(a - b) \<cdot> x = 0" .
-  from v this have "a - b = 0" by (rule vs_mult_zero_uniq)
-  thus "a = b" by simp
-qed simp
+  assume x: "x \<in> V" and neq: "x \<noteq> 0"
+  {
+    from x have "(a - b) \<cdot> x = a \<cdot> x - b \<cdot> x"
+      by (simp add: diff_mult_distrib2)
+    also assume "a \<cdot> x = b \<cdot> x"
+    with x have "a \<cdot> x - b \<cdot> x = 0" by simp
+    finally have "(a - b) \<cdot> x = 0" .
+    with x neq have "a - b = 0" by (rule mult_zero_uniq)
+    thus "a = b" by simp
+  next
+    assume "a = b"
+    then show "a \<cdot> x = b \<cdot> x" by (simp only:)
+  }
+qed
 
-lemma vs_eq_diff_eq:
-  "is_vectorspace V \<Longrightarrow> x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> z \<in> V \<Longrightarrow>
-  (x = z - y) = (x + y = z)"
-  (concl is "?L = ?R" )
-proof -
-  assume vs: "is_vectorspace V"  "x \<in> V"  "y \<in> V"  "z \<in> V"
-  show "?L = ?R"
-  proof
-    assume ?L
+lemma (in vectorspace) eq_diff_eq:
+  "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> z \<in> V \<Longrightarrow> (x = z - y) = (x + y = z)"
+proof
+  assume x: "x \<in> V" and y: "y \<in> V" and z: "z \<in> V"
+  {
+    assume "x = z - y"
     hence "x + y = z - y + y" by simp
-    also have "... = z + - y + y" by (simp! add: diff_eq1)
+    also from y z have "... = z + - y + y"
+      by (simp add: diff_eq1)
     also have "... = z + (- y + y)"
-      by (rule vs_add_assoc) (simp!)+
-    also from vs have "... = z + 0"
-      by (simp only: vs_add_minus_left)
-    also from vs have "... = z" by (simp only: vs_add_zero_right)
-    finally show ?R .
+      by (rule add_assoc) (simp_all add: y z)
+    also from y z have "... = z + 0"
+      by (simp only: add_minus_left)
+    also from z have "... = z"
+      by (simp only: add_zero_right)
+    finally show "x + y = z" .
   next
-    assume ?R
+    assume "x + y = z"
     hence "z - y = (x + y) - y" by simp
-    also from vs have "... = x + y + - y"
+    also from x y have "... = x + y + - y"
       by (simp add: diff_eq1)
     also have "... = x + (y + - y)"
-      by (rule vs_add_assoc) (simp!)+
-    also have "... = x" by (simp!)
-    finally show ?L by (rule sym)
-  qed
+      by (rule add_assoc) (simp_all add: x y)
+    also from x y have "... = x" by simp
+    finally show "x = z - y" ..
+  }
 qed
 
-lemma vs_add_minus_eq_minus:
-  "is_vectorspace V \<Longrightarrow> x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> x + y = 0 \<Longrightarrow> x = - y"
+lemma (in vectorspace) add_minus_eq_minus:
+  "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> x + y = 0 \<Longrightarrow> x = - y"
 proof -
-  assume "is_vectorspace V"  "x \<in> V"  "y \<in> V"
-  have "x = (- y + y) + x" by (simp!)
-  also have "... = - y + (x + y)" by (simp!)
+  assume x: "x \<in> V" and y: "y \<in> V"
+  from x y have "x = (- y + y) + x" by simp
+  also from x y have "... = - y + (x + y)" by (simp add: add_ac)
   also assume "x + y = 0"
-  also have "- y + 0 = - y" by (simp!)
+  also from y have "- y + 0 = - y" by simp
   finally show "x = - y" .
 qed
 
-lemma vs_add_minus_eq:
-  "is_vectorspace V \<Longrightarrow> x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> x - y = 0 \<Longrightarrow> x = y"
+lemma (in vectorspace) add_minus_eq:
+  "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> x - y = 0 \<Longrightarrow> x = y"
 proof -
-  assume "is_vectorspace V"  "x \<in> V"  "y \<in> V"  "x - y = 0"
+  assume x: "x \<in> V" and y: "y \<in> V"
   assume "x - y = 0"
-  hence e: "x + - y = 0" by (simp! add: diff_eq1)
-  with _ _ _ have "x = - (- y)"
-    by (rule vs_add_minus_eq_minus) (simp!)+
-  thus "x = y" by (simp!)
+  with x y have eq: "x + - y = 0" by (simp add: diff_eq1)
+  with _ _ have "x = - (- y)"
+    by (rule add_minus_eq_minus) (simp_all add: x y)
+  with x y show "x = y" by simp
 qed
 
-lemma vs_add_diff_swap:
-  "is_vectorspace V \<Longrightarrow> a \<in> V \<Longrightarrow> b \<in> V \<Longrightarrow> c \<in> V \<Longrightarrow> d \<in> V \<Longrightarrow> a + b = c + d
-  \<Longrightarrow> a - c = d - b"
+lemma (in vectorspace) add_diff_swap:
+  "a \<in> V \<Longrightarrow> b \<in> V \<Longrightarrow> c \<in> V \<Longrightarrow> d \<in> V \<Longrightarrow> a + b = c + d
+    \<Longrightarrow> a - c = d - b"
 proof -
-  assume vs: "is_vectorspace V"  "a \<in> V"  "b \<in> V"  "c \<in> V"  "d \<in> V"
+  assume vs: "a \<in> V"  "b \<in> V"  "c \<in> V"  "d \<in> V"
     and eq: "a + b = c + d"
-  have "- c + (a + b) = - c + (c + d)"
-    by (simp! add: vs_add_left_cancel)
-  also have "... = d" by (rule vs_minus_add_cancel)
+  then have "- c + (a + b) = - c + (c + d)"
+    by (simp add: add_left_cancel)
+  also have "... = d" by (rule minus_add_cancel)
   finally have eq: "- c + (a + b) = d" .
   from vs have "a - c = (- c + (a + b)) + - b"
-    by (simp add: vs_add_ac diff_eq1)
-  also from eq have "...  = d + - b"
-    by (simp! add: vs_add_right_cancel)
-  also have "... = d - b" by (simp! add: diff_eq2)
+    by (simp add: add_ac diff_eq1)
+  also from vs eq have "...  = d + - b"
+    by (simp add: add_right_cancel)
+  also from vs have "... = d - b" by (simp add: diff_eq2)
   finally show "a - c = d - b" .
 qed
 
-lemma vs_add_cancel_21:
-  "is_vectorspace V \<Longrightarrow> x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> z \<in> V \<Longrightarrow> u \<in> V
-  \<Longrightarrow> (x + (y + z) = y + u) = ((x + z) = u)"
-  (concl is "?L = ?R")
-proof -
-  assume "is_vectorspace V"  "x \<in> V"  "y \<in> V"  "z \<in> V"  "u \<in> V"
-  show "?L = ?R"
-  proof
-    have "x + z = - y + y + (x + z)" by (simp!)
+lemma (in vectorspace) vs_add_cancel_21:
+  "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> z \<in> V \<Longrightarrow> u \<in> V
+    \<Longrightarrow> (x + (y + z) = y + u) = (x + z = u)"
+proof
+  assume vs: "x \<in> V"  "y \<in> V"  "z \<in> V"  "u \<in> V"
+  {
+    from vs have "x + z = - y + y + (x + z)" by simp
     also have "... = - y + (y + (x + z))"
-      by (rule vs_add_assoc) (simp!)+
-    also have "y + (x + z) = x + (y + z)" by (simp!)
-    also assume ?L
-    also have "- y + (y + u) = u" by (simp!)
-    finally show ?R .
-  qed (simp! only: vs_add_left_commute [of V x])
+      by (rule add_assoc) (simp_all add: vs)
+    also from vs have "y + (x + z) = x + (y + z)"
+      by (simp add: add_ac)
+    also assume "x + (y + z) = y + u"
+    also from vs have "- y + (y + u) = u" by simp
+    finally show "x + z = u" .
+  next
+    assume "x + z = u"
+    with vs show "x + (y + z) = y + u"
+      by (simp only: add_left_commute [of x])
+  }
 qed
 
-lemma vs_add_cancel_end:
-  "is_vectorspace V \<Longrightarrow> x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> z \<in> V
-  \<Longrightarrow> (x + (y + z) = y) = (x = - z)"
-  (concl is "?L = ?R" )
-proof -
-  assume "is_vectorspace V"  "x \<in> V"  "y \<in> V"  "z \<in> V"
-  show "?L = ?R"
-  proof
-    assume l: ?L
-    have "x + z = 0"
-    proof (rule vs_add_left_cancel [THEN iffD1])
-      have "y + (x + z) = x + (y + z)" by (simp!)
-      also note l
-      also have "y = y + 0" by (simp!)
-      finally show "y + (x + z) = y + 0" .
-    qed (simp!)+
-    thus "x = - z" by (simp! add: vs_add_minus_eq_minus)
+lemma (in vectorspace) add_cancel_end:
+  "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> z \<in> V \<Longrightarrow> (x + (y + z) = y) = (x = - z)"
+proof
+  assume vs: "x \<in> V"  "y \<in> V"  "z \<in> V"
+  {
+    assume "x + (y + z) = y"
+    with vs have "(x + z) + y = 0 + y"
+      by (simp add: add_ac)
+    with vs have "x + z = 0"
+      by (simp only: add_right_cancel add_closed zero)
+    with vs show "x = - z" by (simp add: add_minus_eq_minus)
   next
-    assume r: ?R
+    assume eq: "x = - z"
     hence "x + (y + z) = - z + (y + z)" by simp
     also have "... = y + (- z + z)"
-      by (simp! only: vs_add_left_commute)
-    also have "... = y"  by (simp!)
-    finally show ?L .
-  qed
+      by (rule add_left_commute) (simp_all add: vs)
+    also from vs have "... = y"  by simp
+    finally show "x + (y + z) = y" .
+  }
 qed
 
 end
diff -r cc3bbaf1b8d3 -r a6a7025fd7e8 src/HOL/Real/HahnBanach/ZornLemma.thy
--- a/src/HOL/Real/HahnBanach/ZornLemma.thy	Thu Aug 22 12:28:41 2002 +0200
+++ b/src/HOL/Real/HahnBanach/ZornLemma.thy	Thu Aug 22 20:49:43 2002 +0200
@@ -19,23 +19,22 @@
 *}
 
 theorem Zorn's_Lemma:
-  "(\<And>c. c \<in> chain S \<Longrightarrow> \<exists>x. x \<in> c \<Longrightarrow> \<Union>c \<in> S) \<Longrightarrow> a \<in> S
-  \<Longrightarrow> \<exists>y \<in> S. \<forall>z \<in> S. y \<subseteq> z \<longrightarrow> y = z"
+  assumes r: "\<And>c. c \<in> chain S \<Longrightarrow> \<exists>x. x \<in> c \<Longrightarrow> \<Union>c \<in> S"
+    and aS: "a \<in> S"
+  shows "\<exists>y \<in> S. \<forall>z \<in> S. y \<subseteq> z \<longrightarrow> y = z"
 proof (rule Zorn_Lemma2)
   txt_raw {* \footnote{See
   \url{http://isabelle.in.tum.de/library/HOL/HOL-Real/Zorn.html}} \isanewline *}
-  assume r: "\<And>c. c \<in> chain S \<Longrightarrow> \<exists>x. x \<in> c \<Longrightarrow> \<Union>c \<in> S"
-  assume aS: "a \<in> S"
   show "\<forall>c \<in> chain S. \<exists>y \<in> S. \<forall>z \<in> c. z \<subseteq> y"
   proof
     fix c assume "c \<in> chain S"
     show "\<exists>y \<in> S. \<forall>z \<in> c. z \<subseteq> y"
     proof cases
- 
+
       txt {* If @{text c} is an empty chain, then every element in
       @{text S} is an upper bound of @{text c}. *}
 
-      assume "c = {}" 
+      assume "c = {}"
       with aS show ?thesis by fast
 
       txt {* If @{text c} is non-empty, then @{text "\<Union>c"} is an upper
@@ -43,12 +42,12 @@
 
     next
       assume c: "c \<noteq> {}"
-      show ?thesis 
-      proof 
+      show ?thesis
+      proof
         show "\<forall>z \<in> c. z \<subseteq> \<Union>c" by fast
-        show "\<Union>c \<in> S" 
+        show "\<Union>c \<in> S"
         proof (rule r)
-          from c show "\<exists>x. x \<in> c" by fast  
+          from c show "\<exists>x. x \<in> c" by fast
         qed
       qed
     qed