# HG changeset patch
# User wenzelm
# Date 1315774526 -7200
# Node ID 7ca82df6e951619f5f92b65f10f105107418d5dd
# Parent  6ca299d29bdd28b4e0337090845c7ff4561755a6
misc tuning and clarification;

diff -r 6ca299d29bdd -r 7ca82df6e951 src/HOL/Hahn_Banach/Bounds.thy
--- a/src/HOL/Hahn_Banach/Bounds.thy	Sun Sep 11 21:35:35 2011 +0200
+++ b/src/HOL/Hahn_Banach/Bounds.thy	Sun Sep 11 22:55:26 2011 +0200
@@ -15,9 +15,8 @@
 
 lemmas [elim?] = lub.least lub.upper
 
-definition
-  the_lub :: "'a::order set \<Rightarrow> 'a" where
-  "the_lub A = The (lub A)"
+definition the_lub :: "'a::order set \<Rightarrow> 'a"
+  where "the_lub A = The (lub A)"
 
 notation (xsymbols)
   the_lub  ("\<Squnion>_" [90] 90)
diff -r 6ca299d29bdd -r 7ca82df6e951 src/HOL/Hahn_Banach/Function_Norm.thy
--- a/src/HOL/Hahn_Banach/Function_Norm.thy	Sun Sep 11 21:35:35 2011 +0200
+++ b/src/HOL/Hahn_Banach/Function_Norm.thy	Sun Sep 11 22:55:26 2011 +0200
@@ -143,7 +143,7 @@
           also
           from gt have "\<parallel>x\<parallel> \<noteq> 0" by simp
           then have "\<parallel>x\<parallel> * inverse \<parallel>x\<parallel> = 1" by simp 
-          also have "c * 1 \<le> b" by (simp add: b_def le_maxI1)
+          also have "c * 1 \<le> b" by (simp add: b_def)
           finally show "y \<le> b" .
         qed
       qed
diff -r 6ca299d29bdd -r 7ca82df6e951 src/HOL/Hahn_Banach/Function_Order.thy
--- a/src/HOL/Hahn_Banach/Function_Order.thy	Sun Sep 11 21:35:35 2011 +0200
+++ b/src/HOL/Hahn_Banach/Function_Order.thy	Sun Sep 11 22:55:26 2011 +0200
@@ -23,9 +23,8 @@
 
 type_synonym 'a graph = "('a \<times> real) set"
 
-definition
-  graph :: "'a set \<Rightarrow> ('a \<Rightarrow> real) \<Rightarrow> 'a graph" where
-  "graph F f = {(x, f x) | x. x \<in> F}"
+definition graph :: "'a set \<Rightarrow> ('a \<Rightarrow> real) \<Rightarrow> 'a graph"
+  where "graph F f = {(x, f x) | x. x \<in> F}"
 
 lemma graphI [intro]: "x \<in> F \<Longrightarrow> (x, f x) \<in> graph F f"
   unfolding graph_def by blast
@@ -34,8 +33,9 @@
   unfolding graph_def by blast
 
 lemma graphE [elim?]:
-    "(x, y) \<in> graph F f \<Longrightarrow> (x \<in> F \<Longrightarrow> y = f x \<Longrightarrow> C) \<Longrightarrow> C"
-  unfolding graph_def by blast
+  assumes "(x, y) \<in> graph F f"
+  obtains "x \<in> F" and "y = f x"
+  using assms unfolding graph_def by blast
 
 
 subsection {* Functions ordered by domain extension *}
@@ -50,12 +50,10 @@
     \<Longrightarrow> graph H h \<subseteq> graph H' h'"
   unfolding graph_def by blast
 
-lemma graph_extD1 [dest?]:
-  "graph H h \<subseteq> graph H' h' \<Longrightarrow> x \<in> H \<Longrightarrow> h x = h' x"
+lemma graph_extD1 [dest?]: "graph H h \<subseteq> graph H' h' \<Longrightarrow> x \<in> H \<Longrightarrow> h x = h' x"
   unfolding graph_def by blast
 
-lemma graph_extD2 [dest?]:
-  "graph H h \<subseteq> graph H' h' \<Longrightarrow> H \<subseteq> H'"
+lemma graph_extD2 [dest?]: "graph H h \<subseteq> graph H' h' \<Longrightarrow> H \<subseteq> H'"
   unfolding graph_def by blast
 
 
@@ -66,13 +64,11 @@
   funct}.
 *}
 
-definition
-  "domain" :: "'a graph \<Rightarrow> 'a set" where
-  "domain g = {x. \<exists>y. (x, y) \<in> g}"
+definition domain :: "'a graph \<Rightarrow> 'a set"
+  where "domain g = {x. \<exists>y. (x, y) \<in> g}"
 
-definition
-  funct :: "'a graph \<Rightarrow> ('a \<Rightarrow> real)" where
-  "funct g = (\<lambda>x. (SOME y. (x, y) \<in> g))"
+definition funct :: "'a graph \<Rightarrow> ('a \<Rightarrow> real)"
+  where "funct g = (\<lambda>x. (SOME y. (x, y) \<in> g))"
 
 text {*
   The following lemma states that @{text g} is the graph of a function
@@ -107,21 +103,26 @@
 definition
   norm_pres_extensions ::
     "'a::{plus, minus, uminus, zero} set \<Rightarrow> ('a \<Rightarrow> real) \<Rightarrow> 'a set \<Rightarrow> ('a \<Rightarrow> real)
-      \<Rightarrow> 'a graph set" where
-    "norm_pres_extensions E p F f
-      = {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)}"
+      \<Rightarrow> 'a graph set"
+where
+  "norm_pres_extensions E p F f
+    = {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_extensionE [elim]:
-  "g \<in> norm_pres_extensions E p F f
-  \<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"
-  unfolding norm_pres_extensions_def by blast
+  assumes "g \<in> norm_pres_extensions E p F f"
+  obtains H h
+    where "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"
+  using assms unfolding norm_pres_extensions_def by blast
 
 lemma norm_pres_extensionI2 [intro]:
   "linearform H h \<Longrightarrow> H \<unlhd> E \<Longrightarrow> F \<unlhd> H
diff -r 6ca299d29bdd -r 7ca82df6e951 src/HOL/Hahn_Banach/Hahn_Banach_Sup_Lemmas.thy
--- a/src/HOL/Hahn_Banach/Hahn_Banach_Sup_Lemmas.thy	Sun Sep 11 21:35:35 2011 +0200
+++ b/src/HOL/Hahn_Banach/Hahn_Banach_Sup_Lemmas.thy	Sun Sep 11 22:55:26 2011 +0200
@@ -334,7 +334,7 @@
   proof
     fix x assume "x \<in> H"
     with M cM graph
-    obtain H' h' where x: "x \<in> H'" and H'E: "H' \<unlhd> E"
+    obtain 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" ..
diff -r 6ca299d29bdd -r 7ca82df6e951 src/HOL/Hahn_Banach/Normed_Space.thy
--- a/src/HOL/Hahn_Banach/Normed_Space.thy	Sun Sep 11 21:35:35 2011 +0200
+++ b/src/HOL/Hahn_Banach/Normed_Space.thy	Sun Sep 11 22:55:26 2011 +0200
@@ -50,8 +50,7 @@
   interpret vectorspace V by fact
   assume x: "x \<in> V"
   then have "- 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 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
@@ -80,13 +79,13 @@
 declare normed_vectorspace.intro [intro?]
 
 lemma (in normed_vectorspace) gt_zero [intro?]:
-  "x \<in> V \<Longrightarrow> x \<noteq> 0 \<Longrightarrow> 0 < \<parallel>x\<parallel>"
+  assumes x: "x \<in> V" and neq: "x \<noteq> 0"
+  shows "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"
+  also have "0 \<noteq> \<parallel>x\<parallel>"
   proof
-    assume "\<parallel>x\<parallel> = 0"
+    assume "0 = \<parallel>x\<parallel>"
     with x have "x = 0" by simp
     with neq show False by contradiction
   qed
diff -r 6ca299d29bdd -r 7ca82df6e951 src/HOL/Hahn_Banach/Subspace.thy
--- a/src/HOL/Hahn_Banach/Subspace.thy	Sun Sep 11 21:35:35 2011 +0200
+++ b/src/HOL/Hahn_Banach/Subspace.thy	Sun Sep 11 22:55:26 2011 +0200
@@ -110,6 +110,7 @@
 proof
   show "V \<noteq> {}" ..
   show "V \<subseteq> V" ..
+next
   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
@@ -142,9 +143,8 @@
   scalar multiples of @{text x}.
 *}
 
-definition
-  lin :: "('a::{minus, plus, zero}) \<Rightarrow> 'a set" where
-  "lin x = {a \<cdot> x | a. True}"
+definition lin :: "('a::{minus, plus, zero}) \<Rightarrow> 'a set"
+  where "lin x = {a \<cdot> x | a. True}"
 
 lemma linI [intro]: "y = a \<cdot> x \<Longrightarrow> y \<in> lin x"
   unfolding lin_def by blast
@@ -175,16 +175,18 @@
 text {* Any linear closure is a subspace. *}
 
 lemma (in vectorspace) lin_subspace [intro]:
-  "x \<in> V \<Longrightarrow> lin x \<unlhd> V"
+  assumes x: "x \<in> V"
+  shows "lin x \<unlhd> V"
 proof
-  assume x: "x \<in> V"
-  then show "lin x \<noteq> {}" by (auto simp add: x_lin_x)
+  from x show "lin x \<noteq> {}" by auto
+next
   show "lin x \<subseteq> V"
   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
+next
   fix x' x'' assume x': "x' \<in> lin x" and x'': "x'' \<in> lin x"
   show "x' + x'' \<in> lin x"
   proof -
@@ -290,6 +292,7 @@
         "u \<in> U" and "v \<in> V" ..
       then show "x \<in> E" by simp
     qed
+  next
     fix x y assume x: "x \<in> U \<oplus> V" and y: "y \<in> U \<oplus> V"
     show "x + y \<in> U \<oplus> V"
     proof -
@@ -467,8 +470,9 @@
 lemma h'_definite:
   fixes 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)"
+    "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'"
   assumes "vectorspace E" "subspace H E"
   assumes y: "y \<in> H"
diff -r 6ca299d29bdd -r 7ca82df6e951 src/HOL/Hahn_Banach/Vector_Space.thy
--- a/src/HOL/Hahn_Banach/Vector_Space.thy	Sun Sep 11 21:35:35 2011 +0200
+++ b/src/HOL/Hahn_Banach/Vector_Space.thy	Sun Sep 11 22:55:26 2011 +0200
@@ -5,7 +5,7 @@
 header {* Vector spaces *}
 
 theory Vector_Space
-imports Real Bounds "~~/src/HOL/Library/Zorn"
+imports Complex_Main Bounds "~~/src/HOL/Library/Zorn"
 begin
 
 subsection {* Signature *}
@@ -54,24 +54,24 @@
     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"
+begin
 
-lemma (in vectorspace) negate_eq2: "x \<in> V \<Longrightarrow> (- 1) \<cdot> x = - x"
+lemma negate_eq2: "x \<in> V \<Longrightarrow> (- 1) \<cdot> x = - x"
   by (rule negate_eq1 [symmetric])
 
-lemma (in vectorspace) negate_eq2a: "x \<in> V \<Longrightarrow> -1 \<cdot> x = - x"
+lemma negate_eq2a: "x \<in> V \<Longrightarrow> -1 \<cdot> x = - x"
   by (simp add: negate_eq1)
 
-lemma (in vectorspace) diff_eq2: "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> x + - y = x - y"
+lemma diff_eq2: "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> x + - y = x - y"
   by (rule diff_eq1 [symmetric])
 
-lemma (in vectorspace) diff_closed [iff]: "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> x - y \<in> V"
+lemma diff_closed [iff]: "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> x - y \<in> V"
   by (simp add: diff_eq1 negate_eq1)
 
-lemma (in vectorspace) neg_closed [iff]: "x \<in> V \<Longrightarrow> - x \<in> V"
+lemma neg_closed [iff]: "x \<in> V \<Longrightarrow> - x \<in> V"
   by (simp add: negate_eq1)
 
-lemma (in vectorspace) add_left_commute:
-  "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> z \<in> V \<Longrightarrow> x + (y + z) = y + (x + z)"
+lemma add_left_commute: "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> z \<in> V \<Longrightarrow> x + (y + z) = y + (x + z)"
 proof -
   assume xyz: "x \<in> V"  "y \<in> V"  "z \<in> V"
   then have "x + (y + z) = (x + y) + z"
@@ -81,14 +81,13 @@
   finally show ?thesis .
 qed
 
-theorems (in vectorspace) add_ac =
-  add_assoc add_commute add_left_commute
+theorems add_ac = add_assoc add_commute add_left_commute
 
 
 text {* The existence of the zero element of a vector space
   follows from the non-emptiness of carrier set. *}
 
-lemma (in vectorspace) zero [iff]: "0 \<in> V"
+lemma zero [iff]: "0 \<in> V"
 proof -
   from non_empty obtain x where x: "x \<in> V" by blast
   then have "0 = x - x" by (rule diff_self [symmetric])
@@ -96,8 +95,7 @@
   finally show ?thesis .
 qed
 
-lemma (in vectorspace) add_zero_right [simp]:
-  "x \<in> V \<Longrightarrow>  x + 0 = x"
+lemma add_zero_right [simp]: "x \<in> V \<Longrightarrow>  x + 0 = x"
 proof -
   assume x: "x \<in> V"
   from this and zero have "x + 0 = 0 + x" by (rule add_commute)
@@ -105,16 +103,13 @@
   finally show ?thesis .
 qed
 
-lemma (in vectorspace) mult_assoc2:
-    "x \<in> V \<Longrightarrow> a \<cdot> b \<cdot> x = (a * b) \<cdot> x"
+lemma mult_assoc2: "x \<in> V \<Longrightarrow> a \<cdot> b \<cdot> x = (a * b) \<cdot> x"
   by (simp only: 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"
+lemma 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 (in vectorspace) diff_mult_distrib2:
-  "x \<in> V \<Longrightarrow> (a - b) \<cdot> x = a \<cdot> x - (b \<cdot> x)"
+lemma diff_mult_distrib2: "x \<in> V \<Longrightarrow> (a - b) \<cdot> x = a \<cdot> x - (b \<cdot> x)"
 proof -
   assume x: "x \<in> V"
   have " (a - b) \<cdot> x = (a + - b) \<cdot> x"
@@ -128,15 +123,14 @@
   finally show ?thesis .
 qed
 
-lemmas (in vectorspace) distrib =
+lemmas distrib =
   add_mult_distrib1 add_mult_distrib2
   diff_mult_distrib1 diff_mult_distrib2
 
 
 text {* \medskip Further derived laws: *}
 
-lemma (in vectorspace) mult_zero_left [simp]:
-  "x \<in> V \<Longrightarrow> 0 \<cdot> x = 0"
+lemma mult_zero_left [simp]: "x \<in> V \<Longrightarrow> 0 \<cdot> x = 0"
 proof -
   assume x: "x \<in> V"
   have "0 \<cdot> x = (1 - 1) \<cdot> x" by simp
@@ -150,8 +144,7 @@
   finally show ?thesis .
 qed
 
-lemma (in vectorspace) mult_zero_right [simp]:
-  "a \<cdot> 0 = (0::'a)"
+lemma mult_zero_right [simp]: "a \<cdot> 0 = (0::'a)"
 proof -
   have "a \<cdot> 0 = a \<cdot> (0 - (0::'a))" by simp
   also have "\<dots> =  a \<cdot> 0 - a \<cdot> 0"
@@ -160,12 +153,10 @@
   finally show ?thesis .
 qed
 
-lemma (in vectorspace) minus_mult_cancel [simp]:
-    "x \<in> V \<Longrightarrow> (- a) \<cdot> - x = a \<cdot> x"
+lemma minus_mult_cancel [simp]: "x \<in> V \<Longrightarrow> (- a) \<cdot> - x = a \<cdot> x"
   by (simp add: negate_eq1 mult_assoc2)
 
-lemma (in vectorspace) add_minus_left_eq_diff:
-  "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> - x + y = y - x"
+lemma add_minus_left_eq_diff: "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> - x + y = y - x"
 proof -
   assume xy: "x \<in> V"  "y \<in> V"
   then have "- x + y = y + - x" by (simp add: add_commute)
@@ -173,95 +164,78 @@
   finally show ?thesis .
 qed
 
-lemma (in vectorspace) add_minus [simp]:
-    "x \<in> V \<Longrightarrow> x + - x = 0"
+lemma add_minus [simp]: "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"
+lemma add_minus_left [simp]: "x \<in> V \<Longrightarrow> - x + x = 0"
   by (simp add: diff_eq2 add_commute)
 
-lemma (in vectorspace) minus_minus [simp]:
-    "x \<in> V \<Longrightarrow> - (- x) = x"
+lemma 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"
+lemma minus_zero [simp]: "- (0::'a) = 0"
   by (simp add: negate_eq1)
 
-lemma (in vectorspace) minus_zero_iff [simp]:
-  "x \<in> V \<Longrightarrow> (- x = 0) = (x = 0)"
+lemma minus_zero_iff [simp]:
+  assumes x: "x \<in> V"
+  shows "(- 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 "- \<dots> = 0" by (rule minus_zero)
-    finally show "x = 0" .
-  next
-    assume "x = 0"
-    then show "- x = 0" by simp
-  }
+  from x have "x = - (- x)" by simp
+  also assume "- x = 0"
+  also have "- \<dots> = 0" by (rule minus_zero)
+  finally show "x = 0" .
+next
+  assume "x = 0"
+  then show "- x = 0" by simp
 qed
 
-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 add_minus_cancel [simp]: "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> x + (- x + y) = y"
+  by (simp add: add_assoc [symmetric])
 
-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 minus_add_cancel [simp]: "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> - x + (x + y) = y"
+  by (simp add: add_assoc [symmetric])
 
-lemma (in vectorspace) minus_add_distrib [simp]:
-    "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> - (x + y) = - x + - y"
+lemma 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 (in vectorspace) diff_zero [simp]:
-    "x \<in> V \<Longrightarrow> x - 0 = x"
+lemma 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"
+lemma diff_zero_right [simp]: "x \<in> V \<Longrightarrow> 0 - x = - x"
   by (simp add: diff_eq1)
 
-lemma (in vectorspace) add_left_cancel:
-  "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> z \<in> V \<Longrightarrow> (x + y = x + z) = (y = z)"
+lemma add_left_cancel:
+  assumes x: "x \<in> V" and y: "y \<in> V" and z: "z \<in> V"
+  shows "(x + y = x + z) = (y = z)"
 proof
-  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 "\<dots> = (- x + x) + y" by simp
-    also from x y have "\<dots> = - 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 "\<dots> = z" by simp
-    finally show "y = z" .
-  next
-    assume "y = z"
-    then show "x + y = x + z" by (simp only:)
-  }
+  from y have "y = 0 + y" by simp
+  also from x y have "\<dots> = (- x + x) + y" by simp
+  also from x y have "\<dots> = - x + (x + y)" by (simp add: add_assoc)
+  also assume "x + y = x + z"
+  also from x z have "- x + (x + z) = - x + x + z" by (simp add: add_assoc)
+  also from x z have "\<dots> = z" by simp
+  finally show "y = z" .
+next
+  assume "y = z"
+  then show "x + y = x + z" by (simp only:)
 qed
 
-lemma (in vectorspace) add_right_cancel:
-    "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> z \<in> V \<Longrightarrow> (y + x = z + x) = (y = z)"
+lemma 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 (in vectorspace) add_assoc_cong:
+lemma 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 (in vectorspace) mult_left_commute:
-    "x \<in> V \<Longrightarrow> a \<cdot> b \<cdot> x = b \<cdot> a \<cdot> x"
+lemma mult_left_commute: "x \<in> V \<Longrightarrow> a \<cdot> b \<cdot> x = b \<cdot> a \<cdot> x"
   by (simp add: mult_commute mult_assoc2)
 
-lemma (in vectorspace) mult_zero_uniq:
-  "x \<in> V \<Longrightarrow> x \<noteq> 0 \<Longrightarrow> a \<cdot> x = 0 \<Longrightarrow> a = 0"
+lemma mult_zero_uniq:
+  assumes x: "x \<in> V"  "x \<noteq> 0" and ax: "a \<cdot> x = 0"
+  shows "a = 0"
 proof (rule classical)
   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 from `x \<in> V` have "\<dots> = inverse a \<cdot> (a \<cdot> x)" by (rule mult_assoc)
   also from ax have "\<dots> = inverse a \<cdot> 0" by simp
@@ -270,10 +244,10 @@
   with `x \<noteq> 0` show "a = 0" by contradiction
 qed
 
-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)"
+lemma mult_left_cancel:
+  assumes x: "x \<in> V" and y: "y \<in> V" and a: "a \<noteq> 0"
+  shows "(a \<cdot> x = a \<cdot> y) = (x = y)"
 proof
-  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 "\<dots> = (inverse a * a) \<cdot> x" by simp
   also from x have "\<dots> = inverse a \<cdot> (a \<cdot> x)"
@@ -287,81 +261,75 @@
   then show "a \<cdot> x = a \<cdot> y" by (simp only:)
 qed
 
-lemma (in vectorspace) mult_right_cancel:
-  "x \<in> V \<Longrightarrow> x \<noteq> 0 \<Longrightarrow> (a \<cdot> x = b \<cdot> x) = (a = b)"
+lemma mult_right_cancel:
+  assumes x: "x \<in> V" and neq: "x \<noteq> 0"
+  shows "(a \<cdot> x = b \<cdot> x) = (a = b)"
 proof
-  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)
-    then show "a = b" by simp
-  next
-    assume "a = b"
-    then show "a \<cdot> x = b \<cdot> x" by (simp only:)
-  }
+  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)
+  then show "a = b" by simp
+next
+  assume "a = b"
+  then show "a \<cdot> x = b \<cdot> x" by (simp only:)
 qed
 
-lemma (in vectorspace) eq_diff_eq:
-  "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> z \<in> V \<Longrightarrow> (x = z - y) = (x + y = z)"
+lemma eq_diff_eq:
+  assumes x: "x \<in> V" and y: "y \<in> V" and z: "z \<in> V"
+  shows "(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"
-    then have "x + y = z - y + y" by simp
-    also from y z have "\<dots> = z + - y + y"
-      by (simp add: diff_eq1)
-    also have "\<dots> = z + (- y + y)"
-      by (rule add_assoc) (simp_all add: y z)
-    also from y z have "\<dots> = z + 0"
-      by (simp only: add_minus_left)
-    also from z have "\<dots> = z"
-      by (simp only: add_zero_right)
-    finally show "x + y = z" .
-  next
-    assume "x + y = z"
-    then have "z - y = (x + y) - y" by simp
-    also from x y have "\<dots> = x + y + - y"
-      by (simp add: diff_eq1)
-    also have "\<dots> = x + (y + - y)"
-      by (rule add_assoc) (simp_all add: x y)
-    also from x y have "\<dots> = x" by simp
-    finally show "x = z - y" ..
-  }
+  assume "x = z - y"
+  then have "x + y = z - y + y" by simp
+  also from y z have "\<dots> = z + - y + y"
+    by (simp add: diff_eq1)
+  also have "\<dots> = z + (- y + y)"
+    by (rule add_assoc) (simp_all add: y z)
+  also from y z have "\<dots> = z + 0"
+    by (simp only: add_minus_left)
+  also from z have "\<dots> = z"
+    by (simp only: add_zero_right)
+  finally show "x + y = z" .
+next
+  assume "x + y = z"
+  then have "z - y = (x + y) - y" by simp
+  also from x y have "\<dots> = x + y + - y"
+    by (simp add: diff_eq1)
+  also have "\<dots> = x + (y + - y)"
+    by (rule add_assoc) (simp_all add: x y)
+  also from x y have "\<dots> = x" by simp
+  finally show "x = z - y" ..
 qed
 
-lemma (in vectorspace) add_minus_eq_minus:
-  "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> x + y = 0 \<Longrightarrow> x = - y"
+lemma add_minus_eq_minus:
+  assumes x: "x \<in> V" and y: "y \<in> V" and xy: "x + y = 0"
+  shows "x = - y"
 proof -
-  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 "\<dots> = - y + (x + y)" by (simp add: add_ac)
-  also assume "x + y = 0"
+  also note xy
   also from y have "- y + 0 = - y" by simp
   finally show "x = - y" .
 qed
 
-lemma (in vectorspace) add_minus_eq:
-  "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> x - y = 0 \<Longrightarrow> x = y"
+lemma add_minus_eq:
+  assumes x: "x \<in> V" and y: "y \<in> V" and xy: "x - y = 0"
+  shows "x = y"
 proof -
-  assume x: "x \<in> V" and y: "y \<in> V"
-  assume "x - y = 0"
-  with x y have eq: "x + - y = 0" by (simp add: diff_eq1)
+  from x y xy 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 (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"
+lemma add_diff_swap:
+  assumes vs: "a \<in> V"  "b \<in> V"  "c \<in> V"  "d \<in> V"
+    and eq: "a + b = c + d"
+  shows "a - c = d - b"
 proof -
-  assume vs: "a \<in> V"  "b \<in> V"  "c \<in> V"  "d \<in> V"
-    and eq: "a + b = c + d"
-  then have "- c + (a + b) = - c + (c + d)"
+  from assms have "- c + (a + b) = - c + (c + d)"
     by (simp add: add_left_cancel)
   also have "\<dots> = d" using `c \<in> V` `d \<in> V` by (rule minus_add_cancel)
   finally have eq: "- c + (a + b) = d" .
@@ -373,46 +341,41 @@
   finally show "a - c = d - b" .
 qed
 
-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)"
+lemma vs_add_cancel_21:
+  assumes vs: "x \<in> V"  "y \<in> V"  "z \<in> V"  "u \<in> V"
+  shows "(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 "\<dots> = - y + (y + (x + z))"
-      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])
-  }
+  from vs have "x + z = - y + y + (x + z)" by simp
+  also have "\<dots> = - y + (y + (x + z))"
+    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 (in vectorspace) add_cancel_end:
-  "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> z \<in> V \<Longrightarrow> (x + (y + z) = y) = (x = - z)"
+lemma add_cancel_end:
+  assumes vs: "x \<in> V"  "y \<in> V"  "z \<in> V"
+  shows "(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 eq: "x = - z"
-    then have "x + (y + z) = - z + (y + z)" by simp
-    also have "\<dots> = y + (- z + z)"
-      by (rule add_left_commute) (simp_all add: vs)
-    also from vs have "\<dots> = y"  by simp
-    finally show "x + (y + z) = y" .
-  }
+  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 eq: "x = - z"
+  then have "x + (y + z) = - z + (y + z)" by simp
+  also have "\<dots> = y + (- z + z)" by (rule add_left_commute) (simp_all add: vs)
+  also from vs have "\<dots> = y"  by simp
+  finally show "x + (y + z) = y" .
 qed
 
 end
+
+end
+
diff -r 6ca299d29bdd -r 7ca82df6e951 src/HOL/Hahn_Banach/Zorn_Lemma.thy
--- a/src/HOL/Hahn_Banach/Zorn_Lemma.thy	Sun Sep 11 21:35:35 2011 +0200
+++ b/src/HOL/Hahn_Banach/Zorn_Lemma.thy	Sun Sep 11 22:55:26 2011 +0200
@@ -5,7 +5,7 @@
 header {* Zorn's Lemma *}
 
 theory Zorn_Lemma
-imports Zorn
+imports "~~/src/HOL/Library/Zorn"
 begin
 
 text {*