# HG changeset patch
# User huffman
# Date 1313247415 25200
# Node ID fe55049849373a08e3b2e904980b7dad888c2207
# Parent  4a80017c733ff254053513f8636fbe8df2ee4ce6
HOL-Hahn_Banach: use Set_Algebras library

diff -r 4a80017c733f -r fe5504984937 src/HOL/Hahn_Banach/Hahn_Banach.thy
--- a/src/HOL/Hahn_Banach/Hahn_Banach.thy	Sat Aug 13 07:39:35 2011 -0700
+++ b/src/HOL/Hahn_Banach/Hahn_Banach.thy	Sat Aug 13 07:56:55 2011 -0700
@@ -151,12 +151,12 @@
         qed
       qed
 
-      def H' \<equiv> "H + lin x'"
+      def H' \<equiv> "H \<oplus> lin x'"
         -- {* Define @{text H'} as the direct sum of @{text H} and the linear closure of @{text x'}. \skp *}
       have HH': "H \<unlhd> H'"
       proof (unfold H'_def)
         from x'E have "vectorspace (lin x')" ..
-        with H show "H \<unlhd> H + lin x'" ..
+        with H show "H \<unlhd> H \<oplus> lin x'" ..
       qed
 
       obtain xi where
diff -r 4a80017c733f -r fe5504984937 src/HOL/Hahn_Banach/Hahn_Banach_Ext_Lemmas.thy
--- a/src/HOL/Hahn_Banach/Hahn_Banach_Ext_Lemmas.thy	Sat Aug 13 07:39:35 2011 -0700
+++ b/src/HOL/Hahn_Banach/Hahn_Banach_Ext_Lemmas.thy	Sat Aug 13 07:56:55 2011 -0700
@@ -90,7 +90,7 @@
 lemma h'_lf:
   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 H'_def: "H' \<equiv> H \<oplus> lin x0"
     and HE: "H \<unlhd> E"
   assumes "linearform H h"
   assumes x0: "x0 \<notin> H"  "x0 \<in> E"  "x0 \<noteq> 0"
@@ -106,7 +106,7 @@
     proof (unfold H'_def)
       from `x0 \<in> E`
       have "lin x0 \<unlhd> E" ..
-      with HE show "vectorspace (H + lin x0)" using E ..
+      with HE show "vectorspace (H \<oplus> lin x0)" using E ..
     qed
     {
       fix x1 x2 assume x1: "x1 \<in> H'" and x2: "x2 \<in> H'"
@@ -194,7 +194,7 @@
 lemma h'_norm_pres:
   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 H'_def: "H' \<equiv> H \<oplus> lin x0"
     and x0: "x0 \<notin> H"  "x0 \<in> E"  "x0 \<noteq> 0"
   assumes E: "vectorspace E" and HE: "subspace H E"
     and "seminorm E p" and "linearform H h"
diff -r 4a80017c733f -r fe5504984937 src/HOL/Hahn_Banach/Subspace.thy
--- a/src/HOL/Hahn_Banach/Subspace.thy	Sat Aug 13 07:39:35 2011 -0700
+++ b/src/HOL/Hahn_Banach/Subspace.thy	Sat Aug 13 07:56:55 2011 -0700
@@ -5,7 +5,7 @@
 header {* Subspaces *}
 
 theory Subspace
-imports Vector_Space
+imports Vector_Space "~~/src/HOL/Library/Set_Algebras"
 begin
 
 subsection {* Definition *}
@@ -226,45 +226,38 @@
   set of all sums of elements from @{text U} and @{text V}.
 *}
 
-instantiation "fun" :: (type, type) plus
-begin
-
-definition
-  sum_def: "plus_fun U V = {u + v | u v. u \<in> U \<and> v \<in> V}"  (* FIXME not fully general!? *)
-
-instance ..
-
-end
+lemma sum_def: "U \<oplus> V = {u + v | u v. u \<in> U \<and> v \<in> V}"
+  unfolding set_plus_def by auto
 
 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"
+    "x \<in> U \<oplus> V \<Longrightarrow> (\<And>u v. x = u + v \<Longrightarrow> u \<in> U \<Longrightarrow> v \<in> V \<Longrightarrow> C) \<Longrightarrow> C"
   unfolding sum_def by blast
 
 lemma sumI [intro]:
-    "u \<in> U \<Longrightarrow> v \<in> V \<Longrightarrow> x = u + v \<Longrightarrow> x \<in> U + V"
+    "u \<in> U \<Longrightarrow> v \<in> V \<Longrightarrow> x = u + v \<Longrightarrow> x \<in> U \<oplus> V"
   unfolding sum_def by blast
 
 lemma sumI' [intro]:
-    "u \<in> U \<Longrightarrow> v \<in> V \<Longrightarrow> u + v \<in> U + V"
+    "u \<in> U \<Longrightarrow> v \<in> V \<Longrightarrow> u + v \<in> U \<oplus> V"
   unfolding sum_def by blast
 
-text {* @{text U} is a subspace of @{text "U + V"}. *}
+text {* @{text U} is a subspace of @{text "U \<oplus> V"}. *}
 
 lemma subspace_sum1 [iff]:
   assumes "vectorspace U" "vectorspace V"
-  shows "U \<unlhd> U + V"
+  shows "U \<unlhd> U \<oplus> V"
 proof -
   interpret vectorspace U by fact
   interpret vectorspace V by fact
   show ?thesis
   proof
     show "U \<noteq> {}" ..
-    show "U \<subseteq> U + V"
+    show "U \<subseteq> U \<oplus> V"
     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
+      ultimately have "x + 0 \<in> U \<oplus> V" ..
+      with x show "x \<in> U \<oplus> V" by simp
     qed
     fix x y assume x: "x \<in> U" and "y \<in> U"
     then show "x + y \<in> U" by simp
@@ -276,29 +269,29 @@
 
 lemma sum_subspace [intro?]:
   assumes "subspace U E" "vectorspace E" "subspace V E"
-  shows "U + V \<unlhd> E"
+  shows "U \<oplus> V \<unlhd> E"
 proof -
   interpret subspace U E by fact
   interpret vectorspace E by fact
   interpret subspace V E by fact
   show ?thesis
   proof
-    have "0 \<in> U + V"
+    have "0 \<in> U \<oplus> V"
     proof
       show "0 \<in> U" using `vectorspace E` ..
       show "0 \<in> V" using `vectorspace E` ..
       show "(0::'a) = 0 + 0" by simp
     qed
-    then show "U + V \<noteq> {}" by blast
-    show "U + V \<subseteq> E"
+    then show "U \<oplus> V \<noteq> {}" by blast
+    show "U \<oplus> V \<subseteq> E"
     proof
-      fix x assume "x \<in> U + V"
+      fix x assume "x \<in> U \<oplus> V"
       then obtain u v where "x = u + v" and
         "u \<in> U" and "v \<in> V" ..
       then show "x \<in> E" by simp
     qed
-    fix x y assume x: "x \<in> U + V" and y: "y \<in> U + V"
-    show "x + y \<in> U + V"
+    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 -
       from x obtain ux vx where "x = ux + vx" and "ux \<in> U" and "vx \<in> V" ..
       moreover
@@ -310,7 +303,7 @@
         using x y by (simp_all add: add_ac)
       then show ?thesis ..
     qed
-    fix a show "a \<cdot> x \<in> U + V"
+    fix a show "a \<cdot> x \<in> U \<oplus> V"
     proof -
       from x obtain u v where "x = u + v" and "u \<in> U" and "v \<in> V" ..
       then have "a \<cdot> u \<in> U" and "a \<cdot> v \<in> V"
@@ -323,7 +316,7 @@
 text{* The sum of two subspaces is a vectorspace. *}
 
 lemma sum_vs [intro?]:
-    "U \<unlhd> E \<Longrightarrow> V \<unlhd> E \<Longrightarrow> vectorspace E \<Longrightarrow> vectorspace (U + V)"
+    "U \<unlhd> E \<Longrightarrow> V \<unlhd> E \<Longrightarrow> vectorspace E \<Longrightarrow> vectorspace (U \<oplus> V)"
   by (rule subspace.vectorspace) (rule sum_subspace)
 
 
@@ -484,7 +477,7 @@
 proof -
   interpret vectorspace E by fact
   interpret subspace H E by fact
-  from x y x' have "x \<in> H + lin x'" by auto
+  from x y x' have "x \<in> H \<oplus> 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 (rule ex_ex1I)
     from x y show "\<exists>p. ?P p" by blast