--- 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
--- 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"
--- 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