--- a/src/HOL/HahnBanach/Bounds.thy Wed Jun 24 21:28:02 2009 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,82 +0,0 @@
-(* Title: HOL/Real/HahnBanach/Bounds.thy
- Author: Gertrud Bauer, TU Munich
-*)
-
-header {* Bounds *}
-
-theory Bounds
-imports Main ContNotDenum
-begin
-
-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
-
-definition
- the_lub :: "'a::order set \<Rightarrow> 'a" where
- "the_lub A = The (lub A)"
-
-notation (xsymbols)
- the_lub ("\<Squnion>_" [90] 90)
-
-lemma the_lub_equality [elim?]:
- assumes "lub A x"
- shows "\<Squnion>A = (x::'a::order)"
-proof -
- interpret lub A x by fact
- show ?thesis
- proof (unfold the_lub_def)
- from `lub A x` 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
-qed
-
-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 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"
- unfolding isUb_def setle_def by blast
- with nonempty have "\<exists>x. isLub UNIV A x"
- by (rule reals_complete)
- then show ?thesis by (simp only: lub_compat)
-qed
-
-end
--- a/src/HOL/HahnBanach/FunctionNorm.thy Wed Jun 24 21:28:02 2009 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,278 +0,0 @@
-(* Title: HOL/Real/HahnBanach/FunctionNorm.thy
- Author: Gertrud Bauer, TU Munich
-*)
-
-header {* The norm of a function *}
-
-theory FunctionNorm
-imports NormedSpace FunctionOrder
-begin
-
-subsection {* Continuous linear forms*}
-
-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.
- \begin{center}
- @{text "\<exists>c \<in> R. \<forall>x \<in> V. \<bar>f x\<bar> \<le> c \<cdot> \<parallel>x\<parallel>"}
- \end{center}
- In our application no other functions than linear forms are
- considered, so we can define continuous linear forms as bounded
- linear forms:
-*}
-
-locale continuous = var_V + norm_syntax + linearform +
- assumes bounded: "\<exists>c. \<forall>x \<in> V. \<bar>f x\<bar> \<le> c * \<parallel>x\<parallel>"
-
-declare continuous.intro [intro?] continuous_axioms.intro [intro?]
-
-lemma continuousI [intro]:
- fixes norm :: "_ \<Rightarrow> real" ("\<parallel>_\<parallel>")
- assumes "linearform V f"
- 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" by fact
- 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 *}
-
-text {*
- The least real number @{text c} for which holds
- \begin{center}
- @{text "\<forall>x \<in> V. \<bar>f x\<bar> \<le> c \<cdot> \<parallel>x\<parallel>"}
- \end{center}
- is called the \emph{norm} of @{text f}.
-
- For non-trivial vector spaces @{text "V \<noteq> {0}"} the norm can be
- defined as
- \begin{center}
- @{text "\<parallel>f\<parallel> = \<sup>x \<noteq> 0. \<bar>f x\<bar> / \<parallel>x\<parallel>"}
- \end{center}
-
- For the case @{text "V = {0}"} the supremum would be taken from an
- empty set. Since @{text \<real>} is unbounded, there would be no supremum.
- To avoid this situation it must be guaranteed that there is an
- element in this set. This element must be @{text "{} \<ge> 0"} so that
- @{text fn_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 are @{text "{} \<ge> 0"}.
-
- 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}
-
- @{text fn_norm} is equal to the supremum of @{text B}, if the
- supremum exists (otherwise it is undefined).
-*}
-
-locale fn_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 fn_norm ("\<parallel>_\<parallel>\<hyphen>_" [0, 1000] 999)
- defines "\<parallel>f\<parallel>\<hyphen>V \<equiv> \<Squnion>(B V f)"
-
-locale normed_vectorspace_with_fn_norm = normed_vectorspace + fn_norm
-
-lemma (in fn_norm) B_not_empty [intro]: "0 \<in> B V f"
- by (simp add: B_def)
-
-text {*
- The following lemma states that every continuous linear form on a
- normed space @{text "(V, \<parallel>\<cdot>\<parallel>)"} has a function norm.
-*}
-
-lemma (in normed_vectorspace_with_fn_norm) fn_norm_works:
- assumes "continuous V norm f"
- shows "lub (B V f) (\<parallel>f\<parallel>\<hyphen>V)"
-proof -
- interpret continuous V norm f by fact
- 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. *}
- have "\<exists>a. lub (B V f) a"
- proof (rule real_complete)
- txt {* First we have to show that @{text B} is non-empty: *}
- have "0 \<in> B V f" ..
- then show "\<exists>x. x \<in> B V f" ..
-
- txt {* Then we have to show that @{text B} is bounded: *}
- 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}. *}
- from bounded obtain c where c: "\<forall>x \<in> V. \<bar>f x\<bar> \<le> c * \<parallel>x\<parallel>" ..
-
- 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. *}
-
- 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"
- then show ?thesis unfolding b_def by 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>" ..
-
- 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 mult_right_mono)
- from c x show "\<bar>f x\<bar> \<le> c * \<parallel>x\<parallel>" ..
- from gt have "0 < inverse \<parallel>x\<parallel>"
- by (rule positive_imp_inverse_positive)
- then show "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
- 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)
- finally show "y \<le> b" .
- qed
- qed
- then show ?thesis ..
- qed
- qed
- then show ?thesis unfolding fn_norm_def by (rule the_lubI_ex)
-qed
-
-lemma (in normed_vectorspace_with_fn_norm) fn_norm_ub [iff?]:
- assumes "continuous V norm f"
- assumes b: "b \<in> B V f"
- shows "b \<le> \<parallel>f\<parallel>\<hyphen>V"
-proof -
- interpret continuous V norm f by fact
- have "lub (B V f) (\<parallel>f\<parallel>\<hyphen>V)"
- using `continuous V norm f` by (rule fn_norm_works)
- from this and b show ?thesis ..
-qed
-
-lemma (in normed_vectorspace_with_fn_norm) fn_norm_leastB:
- assumes "continuous V norm f"
- assumes b: "\<And>b. b \<in> B V f \<Longrightarrow> b \<le> y"
- shows "\<parallel>f\<parallel>\<hyphen>V \<le> y"
-proof -
- interpret continuous V norm f by fact
- have "lub (B V f) (\<parallel>f\<parallel>\<hyphen>V)"
- using `continuous V norm f` by (rule fn_norm_works)
- from this and b show ?thesis ..
-qed
-
-text {* The norm of a continuous function is always @{text "\<ge> 0"}. *}
-
-lemma (in normed_vectorspace_with_fn_norm) fn_norm_ge_zero [iff]:
- assumes "continuous V norm f"
- shows "0 \<le> \<parallel>f\<parallel>\<hyphen>V"
-proof -
- interpret continuous V norm f by fact
- 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. *}
- have "lub (B V f) (\<parallel>f\<parallel>\<hyphen>V)"
- using `continuous V norm f` by (rule fn_norm_works)
- moreover have "0 \<in> B V f" ..
- ultimately show ?thesis ..
-qed
-
-text {*
- \medskip The fundamental property of function norms is:
- \begin{center}
- @{text "\<bar>f x\<bar> \<le> \<parallel>f\<parallel> \<cdot> \<parallel>x\<parallel>"}
- \end{center}
-*}
-
-lemma (in normed_vectorspace_with_fn_norm) fn_norm_le_cong:
- assumes "continuous V norm f" "linearform V f"
- assumes x: "x \<in> V"
- shows "\<bar>f x\<bar> \<le> \<parallel>f\<parallel>\<hyphen>V * \<parallel>x\<parallel>"
-proof -
- interpret continuous V norm f by fact
- interpret linearform V f by fact
- show ?thesis
- proof cases
- assume "x = 0"
- then have "\<bar>f x\<bar> = \<bar>f 0\<bar>" by simp
- also have "f 0 = 0" by rule unfold_locales
- also have "\<bar>\<dots>\<bar> = 0" by simp
- also have a: "0 \<le> \<parallel>f\<parallel>\<hyphen>V"
- using `continuous V norm f` by (rule fn_norm_ge_zero)
- from x have "0 \<le> norm x" ..
- with a have "0 \<le> \<parallel>f\<parallel>\<hyphen>V * \<parallel>x\<parallel>" by (simp add: zero_le_mult_iff)
- 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 mult_right_mono)
- from x show "0 \<le> \<parallel>x\<parallel>" ..
- from x and neq have "\<bar>f x\<bar> * inverse \<parallel>x\<parallel> \<in> B V f"
- by (auto simp add: B_def real_divide_def)
- with `continuous V norm f` show "\<bar>f x\<bar> * inverse \<parallel>x\<parallel> \<le> \<parallel>f\<parallel>\<hyphen>V"
- by (rule fn_norm_ub)
- qed
- finally show ?thesis .
- qed
-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>"}
- \end{center}
-*}
-
-lemma (in normed_vectorspace_with_fn_norm) fn_norm_least [intro?]:
- assumes "continuous V norm f"
- 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 -
- interpret continuous V norm f by fact
- show ?thesis
- proof (rule fn_norm_leastB [folded B_def fn_norm_def])
- 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 mult_right_mono)
- have "0 < \<parallel>x\<parallel>" using x x_neq ..
- 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 (insert `continuous V norm f`, simp_all add: continuous_def)
-qed
-
-end
--- a/src/HOL/HahnBanach/FunctionOrder.thy Wed Jun 24 21:28:02 2009 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,142 +0,0 @@
-(* Title: HOL/Real/HahnBanach/FunctionOrder.thy
- ID: $Id$
- Author: Gertrud Bauer, TU Munich
-*)
-
-header {* An order on functions *}
-
-theory FunctionOrder
-imports Subspace Linearform
-begin
-
-subsection {* The graph of a function *}
-
-text {*
- We define the \emph{graph} of a (real) function @{text f} with
- domain @{text F} as the set
- \begin{center}
- @{text "{(x, f x). x \<in> F}"}
- \end{center}
- So we are modeling partial functions by specifying the domain and
- the mapping function. We use the term ``function'' also for its
- graph.
-*}
-
-types '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}"
-
-lemma graphI [intro]: "x \<in> F \<Longrightarrow> (x, f x) \<in> graph F f"
- unfolding graph_def by blast
-
-lemma graphI2 [intro?]: "x \<in> F \<Longrightarrow> \<exists>t \<in> graph F f. t = (x, f x)"
- 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
-
-
-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'}.
-*}
-
-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'"
- 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"
- unfolding graph_def by blast
-
-lemma graph_extD2 [dest?]:
- "graph H h \<subseteq> graph H' h' \<Longrightarrow> H \<subseteq> H'"
- unfolding graph_def by blast
-
-
-subsection {* Domain and function of a graph *}
-
-text {*
- The inverse functions to @{text graph} are @{text domain} and @{text
- funct}.
-*}
-
-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))"
-
-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:
- 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"
- unfolding domain_def funct_def graph_def
-proof auto (* FIXME !? *)
- fix a b assume g: "(a, b) \<in> g"
- from g show "(a, SOME y. (a, y) \<in> g) \<in> g" by (rule someI2)
- from g show "\<exists>y. (a, y) \<in> g" ..
- from g show "b = (SOME y. (a, y) \<in> g)"
- proof (rule some_equality [symmetric])
- fix y assume "(a, y) \<in> g"
- with g show "y = b" by (rule uniq)
- qed
-qed
-
-
-subsection {* Norm-preserving extensions of a function *}
-
-text {*
- Given a linear form @{text f} on the space @{text F} and a seminorm
- @{text p} on @{text E}. The set of all linear extensions of @{text
- f}, to superspaces @{text H} of @{text F}, which are bounded by
- @{text p}, is defined as follows.
-*}
-
-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)}"
-
-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
-
-lemma norm_pres_extensionI2 [intro]:
- "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"
- unfolding norm_pres_extensions_def by blast
-
-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"
- unfolding norm_pres_extensions_def by blast
-
-end
--- a/src/HOL/HahnBanach/HahnBanach.thy Wed Jun 24 21:28:02 2009 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,509 +0,0 @@
-(* Title: HOL/Real/HahnBanach/HahnBanach.thy
- Author: Gertrud Bauer, TU Munich
-*)
-
-header {* The Hahn-Banach Theorem *}
-
-theory HahnBanach
-imports HahnBanachLemmas
-begin
-
-text {*
- We present the proof of two different versions of the Hahn-Banach
- Theorem, closely following \cite[\S36]{Heuser:1986}.
-*}
-
-subsection {* The Hahn-Banach Theorem for vector spaces *}
-
-text {*
- \textbf{Hahn-Banach Theorem.} Let @{text F} be a subspace of a real
- vector space @{text E}, let @{text p} be a semi-norm on @{text E},
- and @{text f} be a linear form defined on @{text F} such that @{text
- f} is bounded by @{text p}, i.e. @{text "\<forall>x \<in> F. f x \<le> p x"}. Then
- @{text f} can be extended to a linear form @{text h} on @{text E}
- such that @{text h} is norm-preserving, i.e. @{text h} is also
- bounded by @{text p}.
-
- \bigskip
- \textbf{Proof Sketch.}
- \begin{enumerate}
-
- \item Define @{text M} as the set of norm-preserving extensions of
- @{text f} to subspaces of @{text E}. The linear forms in @{text M}
- are ordered by domain extension.
-
- \item We show that every non-empty chain in @{text M} has an upper
- bound in @{text M}.
-
- \item With Zorn's Lemma we conclude that there is a maximal function
- @{text g} in @{text M}.
-
- \item The domain @{text H} of @{text g} is the whole space @{text
- E}, as shown by classical contradiction:
-
- \begin{itemize}
-
- \item Assuming @{text g} is not defined on whole @{text E}, it can
- still be extended in a norm-preserving way to a super-space @{text
- H'} of @{text H}.
-
- \item Thus @{text g} can not be maximal. Contradiction!
-
- \end{itemize}
- \end{enumerate}
-*}
-
-theorem HahnBanach:
- assumes E: "vectorspace E" and "subspace F E"
- and "seminorm E p" and "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 -
- interpret vectorspace E by fact
- interpret subspace F E by fact
- interpret seminorm E p by fact
- interpret linearform F f by fact
- def M \<equiv> "norm_pres_extensions E p F f"
- then have M: "M = \<dots>" by (simp only:)
- from E have F: "vectorspace F" ..
- note FE = `F \<unlhd> E`
- {
- 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"}. *}
- unfolding M_def
- proof (rule norm_pres_extensionI)
- let ?H = "domain (\<Union>c)"
- let ?h = "funct (\<Union>c)"
-
- 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 FE E have "?H \<unlhd> E"
- by (rule sup_subE)
- moreover from a M cM ex FE 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
- }
- then have "\<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: *}
- show "graph F f \<in> M"
- unfolding M_def
- proof (rule norm_pres_extensionI2)
- show "linearform F f" by fact
- show "F \<unlhd> E" by fact
- 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" by fact
- qed
- qed
- then obtain g where gM: "g \<in> M" and gx: "\<forall>x \<in> M. g \<subseteq> x \<longrightarrow> g = x"
- by blast
- from gM 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" unfolding M_def ..
- -- {* @{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 *}
- from HE E have H: "vectorspace H"
- by (rule subspace.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 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 -
- 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)
- with `x' \<notin> H` show False by contradiction
- qed
- 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 *}
- have HH': "H \<unlhd> H'"
- proof (unfold H'_def)
- from x'E have "vectorspace (lin x')" ..
- with H show "H \<unlhd> H + lin x'" ..
- qed
-
- obtain xi where
- xi: "\<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: 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 E 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 by (blast intro: that)
- 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 -
- have "graph H h \<subseteq> graph H' h'"
- proof (rule graph_extI)
- fix t assume t: "t \<in> H"
- from E HE t have "(SOME (y, a). t = y + a \<cdot> x' \<and> y \<in> H) = (t, 0)"
- using `x' \<notin> H` `x' \<in> E` `x' \<noteq> 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
- with g_rep show ?thesis by (simp only:)
- qed
-
- show "g \<noteq> graph H' h'"
- proof -
- have "graph H h \<noteq> graph H' h'"
- proof
- assume eq: "graph H h = graph H' h'"
- have "x' \<in> H'"
- unfolding H'_def
- proof
- 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
- then have "(x', h' x') \<in> graph H' h'" ..
- with eq have "(x', h' x') \<in> graph H h" by (simp only:)
- then have "x' \<in> H" ..
- with `x' \<notin> H` show False by contradiction
- qed
- with g_rep show ?thesis by simp
- qed
- qed
- 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'"
- using h'_def H'_def HE linearform `x' \<notin> H` `x' \<in> E` `x' \<noteq> 0` E
- by (rule h'_lf)
- show "H' \<unlhd> E"
- unfolding H'_def
- proof
- show "H \<unlhd> E" by fact
- show "vectorspace E" by fact
- from x'E show "lin x' \<unlhd> E" ..
- qed
- from H `F \<unlhd> H` 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)"
- using E HE
- proof (rule decomp_H'_H [symmetric])
- from FH x show "x \<in> H" ..
- from x' show "x' \<noteq> 0" .
- show "x' \<notin> H" by fact
- show "x' \<in> E" by fact
- 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"
- using h'_def H'_def `x' \<notin> H` `x' \<in> E` `x' \<noteq> 0` E HE
- `seminorm E p` linearform and hp xi
- by (rule h'_norm_pres)
- qed
- qed
- ultimately show ?thesis ..
- qed
- then have "\<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 *}
- with gx 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
-
-
-subsection {* Alternative formulation *}
-
-text {*
- The following alternative formulation of the Hahn-Banach
- Theorem\label{abs-HahnBanach} uses the fact that for a real linear
- form @{text f} and a seminorm @{text p} the following inequations
- are equivalent:\footnote{This was shown in lemma @{thm [source]
- abs_ineq_iff} (see page \pageref{abs-ineq-iff}).}
- \begin{center}
- \begin{tabular}{lll}
- @{text "\<forall>x \<in> H. \<bar>h x\<bar> \<le> p x"} & and &
- @{text "\<forall>x \<in> H. h x \<le> p x"} \\
- \end{tabular}
- \end{center}
-*}
-
-theorem abs_HahnBanach:
- assumes E: "vectorspace E" and FE: "subspace F E"
- and lf: "linearform F f" and sn: "seminorm 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 -
- interpret vectorspace E by fact
- interpret subspace F E by fact
- interpret linearform F f by fact
- interpret seminorm E p by fact
- 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)"
- using E FE sn lf
- proof (rule HahnBanach)
- show "\<forall>x \<in> F. f x \<le> p x"
- using FE E sn lf and fp by (rule abs_ineq_iff [THEN iffD1])
- qed
- then obtain g where lg: "linearform E g" and *: "\<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"
- using _ E sn lg **
- proof (rule abs_ineq_iff [THEN iffD2])
- show "E \<unlhd> E" ..
- qed
- with lg * show ?thesis by blast
-qed
-
-
-subsection {* The Hahn-Banach Theorem for normed spaces *}
-
-text {*
- Every continuous linear form @{text f} on a subspace @{text F} of a
- norm space @{text E}, can be extended to a continuous linear form
- @{text g} on @{text E} such that @{text "\<parallel>f\<parallel> = \<parallel>g\<parallel>"}.
-*}
-
-theorem norm_HahnBanach:
- fixes V and norm ("\<parallel>_\<parallel>")
- fixes B defines "\<And>V f. B V f \<equiv> {0} \<union> {\<bar>f x\<bar> / \<parallel>x\<parallel> | x. x \<noteq> 0 \<and> x \<in> V}"
- fixes fn_norm ("\<parallel>_\<parallel>\<hyphen>_" [0, 1000] 999)
- defines "\<And>V f. \<parallel>f\<parallel>\<hyphen>V \<equiv> \<Squnion>(B V f)"
- assumes E_norm: "normed_vectorspace E norm" and FE: "subspace F E"
- and linearform: "linearform F f" and "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>\<hyphen>E = \<parallel>f\<parallel>\<hyphen>F"
-proof -
- interpret normed_vectorspace E norm by fact
- interpret normed_vectorspace_with_fn_norm E norm B fn_norm
- by (auto simp: B_def fn_norm_def) intro_locales
- interpret subspace F E by fact
- interpret linearform F f by fact
- interpret continuous F norm f by fact
- have E: "vectorspace E" by intro_locales
- have F: "vectorspace F" by rule intro_locales
- have F_norm: "normed_vectorspace F norm"
- using FE E_norm by (rule subspace_normed_vs)
- have ge_zero: "0 \<le> \<parallel>f\<parallel>\<hyphen>F"
- by (rule normed_vectorspace_with_fn_norm.fn_norm_ge_zero
- [OF normed_vectorspace_with_fn_norm.intro,
- OF F_norm `continuous F norm f` , folded B_def fn_norm_def])
- 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 p} is positive definite: *}
- have "0 \<le> \<parallel>f\<parallel>\<hyphen>F" by (rule ge_zero)
- moreover from x have "0 \<le> \<parallel>x\<parallel>" ..
- ultimately show "0 \<le> p x"
- by (simp add: p_def zero_le_mult_iff)
-
- 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>\<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: *}
-
- 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 a: "0 \<le> \<parallel>f\<parallel>\<hyphen>F" by (rule ge_zero)
- from x y have "\<parallel>x + y\<parallel> \<le> \<parallel>x\<parallel> + \<parallel>y\<parallel>" ..
- with a have " \<parallel>f\<parallel>\<hyphen>F * \<parallel>x + y\<parallel> \<le> \<parallel>f\<parallel>\<hyphen>F * (\<parallel>x\<parallel> + \<parallel>y\<parallel>)"
- by (simp add: mult_left_mono)
- also have "\<dots> = \<parallel>f\<parallel>\<hyphen>F * \<parallel>x\<parallel> + \<parallel>f\<parallel>\<hyphen>F * \<parallel>y\<parallel>" by (simp only: right_distrib)
- also have "\<dots> = p x + p y" by (simp only: p_def)
- finally show ?thesis .
- qed
- qed
-
- txt {* @{text f} is bounded by @{text p}. *}
-
- have "\<forall>x \<in> F. \<bar>f x\<bar> \<le> p x"
- proof
- fix x assume "x \<in> F"
- with `continuous F norm f` and linearform
- show "\<bar>f x\<bar> \<le> p x"
- unfolding p_def by (rule normed_vectorspace_with_fn_norm.fn_norm_le_cong
- [OF normed_vectorspace_with_fn_norm.intro,
- OF F_norm, folded B_def fn_norm_def])
- qed
-
- 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}. *}
-
- 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]) iprover
-
- 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>\<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>"}. *}
-
- 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
- \begin{center}
- \begin{tabular}{l}
- @{text "\<forall>x \<in> E. \<bar>g x\<bar> \<le> c \<cdot> \<parallel>x\<parallel>"}
- \end{tabular}
- \end{center}
- \noindent Furthermore holds
- \begin{center}
- \begin{tabular}{l}
- @{text "\<forall>x \<in> E. \<bar>g x\<bar> \<le> \<parallel>f\<parallel> \<cdot> \<parallel>x\<parallel>"}
- \end{tabular}
- \end{center}
- *}
-
- 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"
- with b show "\<bar>g x\<bar> \<le> \<parallel>f\<parallel>\<hyphen>F * \<parallel>x\<parallel>"
- by (simp only: p_def)
- qed
- from g_cont this ge_zero
- show "\<parallel>g\<parallel>\<hyphen>E \<le> \<parallel>f\<parallel>\<hyphen>F"
- by (rule fn_norm_least [of g, folded B_def fn_norm_def])
-
- txt {* The other direction is achieved by a similar argument. *}
-
- show "\<parallel>f\<parallel>\<hyphen>F \<le> \<parallel>g\<parallel>\<hyphen>E"
- proof (rule normed_vectorspace_with_fn_norm.fn_norm_least
- [OF normed_vectorspace_with_fn_norm.intro,
- OF F_norm, folded B_def fn_norm_def])
- show "\<forall>x \<in> F. \<bar>f x\<bar> \<le> \<parallel>g\<parallel>\<hyphen>E * \<parallel>x\<parallel>"
- proof
- fix x assume x: "x \<in> F"
- from a x have "g x = f x" ..
- then have "\<bar>f x\<bar> = \<bar>g x\<bar>" by (simp only:)
- also from g_cont
- have "\<dots> \<le> \<parallel>g\<parallel>\<hyphen>E * \<parallel>x\<parallel>"
- proof (rule fn_norm_le_cong [OF _ linearformE, folded B_def fn_norm_def])
- from FE x show "x \<in> E" ..
- qed
- finally show "\<bar>f x\<bar> \<le> \<parallel>g\<parallel>\<hyphen>E * \<parallel>x\<parallel>" .
- qed
- show "0 \<le> \<parallel>g\<parallel>\<hyphen>E"
- using g_cont
- by (rule fn_norm_ge_zero [of g, folded B_def fn_norm_def])
- show "continuous F norm f" by fact
- qed
- qed
- with linearformE a g_cont show ?thesis by blast
-qed
-
-end
--- a/src/HOL/HahnBanach/HahnBanachExtLemmas.thy Wed Jun 24 21:28:02 2009 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,280 +0,0 @@
-(* Title: HOL/Real/HahnBanach/HahnBanachExtLemmas.thy
- Author: Gertrud Bauer, TU Munich
-*)
-
-header {* Extending non-maximal functions *}
-
-theory HahnBanachExtLemmas
-imports FunctionNorm
-begin
-
-text {*
- In this section the following context is presumed. Let @{text E} be
- a real vector space with a seminorm @{text q} on @{text E}. @{text
- F} is a subspace of @{text E} and @{text f} a linear function on
- @{text F}. We consider a subspace @{text H} of @{text E} that is a
- superspace of @{text F} and a linear form @{text h} on @{text
- H}. @{text H} is a not equal to @{text E} and @{text "x\<^sub>0"} is
- 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>}.
-
- Subsequently we show some properties of this extension @{text h'} of
- @{text h}.
-
- \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"}
- \end{tabular}
- \end{center}
- \noindent it suffices to show that
- \begin{center}
- \begin{tabular}{l}
- @{text "\<forall>u \<in> F. \<forall>v \<in> F. a u \<le> b v"}
- \end{tabular}
- \end{center}
-*}
-
-lemma ex_xi:
- assumes "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 -
- interpret vectorspace F by fact
- 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 | 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
- 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
- } 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'}.
-*}
-
-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 HE: "H \<unlhd> E"
- assumes "linearform H h"
- assumes x0: "x0 \<notin> H" "x0 \<in> E" "x0 \<noteq> 0"
- assumes E: "vectorspace E"
- shows "linearform H' h'"
-proof -
- interpret linearform H h by fact
- interpret vectorspace E by fact
- show ?thesis
- proof
- note E = `vectorspace E`
- have H': "vectorspace H'"
- proof (unfold H'_def)
- from `x0 \<in> E`
- have "lin x0 \<unlhd> E" ..
- with HE show "vectorspace (H + lin x0)" using E ..
- qed
- {
- fix x1 x2 assume x1: "x1 \<in> H'" and x2: "x2 \<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"
- unfolding H'_def sum_def lin_def by blast
-
- have ya: "y1 + y2 = y \<and> a1 + a2 = a" using E 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 E HE y x0
- have "h' (x1 + x2) = h y + a * xi"
- by (rule h'_definite)
- 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 "\<dots> + (a1 + a2) * xi = (h y1 + a1 * xi) + (h y2 + a2 * xi)"
- by (simp add: left_distrib)
- also from h'_def x1_rep E HE y1 x0
- have "h y1 + a1 * xi = h' x1"
- by (rule h'_definite [symmetric])
- also from h'_def x2_rep E HE y2 x0
- have "h y2 + a2 * xi = h' x2"
- by (rule h'_definite [symmetric])
- finally show ?thesis .
- qed
- next
- 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"
- unfolding H'_def sum_def lin_def by blast
-
- have ya: "c \<cdot> y1 = y \<and> c * a1 = a" using E HE _ y x0
- proof (rule decomp_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
-
- from h'_def cx1_rep E HE y x0 have "h' (c \<cdot> x1) = h y + a * xi"
- by (rule h'_definite)
- 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: right_distrib)
- also from h'_def x1_rep E 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}. *}
-
-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 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"
- 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 -
- interpret vectorspace E by fact
- interpret subspace H E by fact
- interpret seminorm E p by fact
- interpret linearform H h by fact
- show ?thesis
- 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"
- unfolding H'_def sum_def lin_def by 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 E HE y x0 have "h' x = h y + a * xi"
- by (rule h'_definite)
- also have "\<dots> \<le> p (y + a \<cdot> x0)"
- proof (rule linorder_cases)
- assume z: "a = 0"
- 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" then have nz: "a \<noteq> 0" by simp
- 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 (simp add: mult_left_mono_neg order_less_imp_le)
-
- also have "\<dots> =
- - a * (p (inverse a \<cdot> y + x0)) - a * (h (inverse a \<cdot> y))"
- by (simp add: right_diff_distrib)
- 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)
- 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" .
- 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"}: *}
- assume gz: "0 < a" then have nz: "a \<noteq> 0" by simp
- 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 simp
- also have "\<dots> = a * p (inverse a \<cdot> y + x0) - a * h (inverse a \<cdot> y)"
- by (simp add: right_diff_distrib)
- also from gz x0 y'
- have "a * p (inverse a \<cdot> y + x0) = p (a \<cdot> (inverse a \<cdot> y + x0))"
- by (simp add: abs_homogenous)
- 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" .
- then show ?thesis by simp
- qed
- also from x_rep have "\<dots> = p x" by (simp only:)
- finally show ?thesis .
- qed
- qed
-qed
-
-end
--- a/src/HOL/HahnBanach/HahnBanachLemmas.thy Wed Jun 24 21:28:02 2009 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,4 +0,0 @@
-(*<*)
-theory HahnBanachLemmas imports HahnBanachSupLemmas HahnBanachExtLemmas begin
-end
-(*>*)
\ No newline at end of file
--- a/src/HOL/HahnBanach/HahnBanachSupLemmas.thy Wed Jun 24 21:28:02 2009 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,446 +0,0 @@
-(* Title: HOL/Real/HahnBanach/HahnBanachSupLemmas.thy
- ID: $Id$
- Author: Gertrud Bauer, TU Munich
-*)
-
-header {* The supremum w.r.t.~the function order *}
-
-theory HahnBanachSupLemmas
-imports FunctionNorm ZornLemma
-begin
-
-text {*
- This section contains some lemmas that will be used in the proof of
- the Hahn-Banach Theorem. In this section the following context is
- presumed. Let @{text E} be a real vector space with a seminorm
- @{text p} on @{text E}. @{text F} is a subspace of @{text E} and
- @{text f} a linear form on @{text F}. We consider a chain @{text c}
- of norm-preserving extensions of @{text f}, such that @{text "\<Union>c =
- graph H h"}. We will show some properties about the limit function
- @{text h}, i.e.\ the supremum of the chain @{text c}.
-
- \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.
-*}
-lemmas [dest?] = chainD
-lemmas chainE2 [elim?] = chainD2 [elim_format, standard]
-
-lemma some_H'h't:
- 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 -
- from x have "(x, h x) \<in> graph H h" ..
- also from u have "\<dots> = \<Union>c" .
- finally obtain g where gc: "g \<in> c" and gh: "(x, h x) \<in> g" by blast
-
- from cM have "c \<subseteq> M" ..
- with gc have "g \<in> M" ..
- also from M have "\<dots> = norm_pres_extensions E p F f" .
- finally obtain H' and h' where g: "g = graph H' h'"
- and * : "linearform H' h'" "H' \<unlhd> E" "F \<unlhd> H'"
- "graph F f \<subseteq> graph H' h'" "\<forall>x \<in> H'. h' x \<le> p x" ..
-
- from gc and g have "graph H' h' \<in> c" by (simp only:)
- moreover from gh and g have "(x, h x) \<in> graph H' h'" by (simp only:)
- ultimately show ?thesis using * by blast
-qed
-
-text {*
- \medskip Let @{text c} be a chain of norm-preserving extensions of
- the function @{text f} and let @{text "graph H h"} be the supremum
- of @{text c}. Every element in the domain @{text H} of the supremum
- function is member of the domain @{text H'} of some function @{text
- h'}, such that @{text h} extends @{text h'}.
-*}
-
-lemma some_H'h':
- 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 -
- 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"
- by (rule some_H'h't [elim_format]) blast
- from x_hx have "x \<in> H'" ..
- moreover from cM u c have "graph H' h' \<subseteq> graph H h"
- by (simp only: chain_ball_Union_upper)
- ultimately show ?thesis using * by blast
-qed
-
-text {*
- \medskip Any two elements @{text x} and @{text y} in the domain
- @{text H} of the supremum function @{text h} are both in the domain
- @{text H'} of some function @{text h'}, such that @{text h} extends
- @{text h'}.
-*}
-
-lemma some_H'h'2:
- 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 -
- txt {* @{text y} is in the domain @{text H''} of some function @{text h''},
- such that @{text h} extends @{text h''}. *}
-
- from M cM u and y obtain H' h' where
- y_hy: "(y, h y) \<in> graph H' h'"
- and c': "graph H' h' \<in> c"
- and * :
- "linearform H' h'" "H' \<unlhd> E" "F \<unlhd> H'"
- "graph F f \<subseteq> graph H' h'" "\<forall>x \<in> H'. h' x \<le> p x"
- by (rule some_H'h't [elim_format]) blast
-
- txt {* @{text x} is in the domain @{text H'} of some function @{text h'},
- such that @{text h} extends @{text h'}. *}
-
- from M cM u and x obtain H'' h'' where
- x_hx: "(x, h x) \<in> graph H'' h''"
- and c'': "graph H'' h'' \<in> c"
- and ** :
- "linearform H'' h''" "H'' \<unlhd> E" "F \<unlhd> H''"
- "graph F f \<subseteq> graph H'' h''" "\<forall>x \<in> H''. h'' x \<le> p x"
- by (rule some_H'h't [elim_format]) blast
-
- txt {* Since both @{text h'} and @{text h''} are elements of the chain,
- @{text h''} is an extension of @{text h'} or vice versa. Thus both
- @{text x} and @{text y} are contained in the greater
- one. \label{cases1}*}
-
- from cM c'' c' 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''" by fact
- also have "\<dots> \<subseteq> graph H' h'" by fact
- 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 {
- have "(y, h y) \<in> graph H' h'" by (rule y_hy)
- also have "\<dots> \<subseteq> graph H'' h''" by fact
- 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.
-*}
-
-lemma sup_definite:
- 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 -
- from cM have c: "c \<subseteq> M" ..
- from xy obtain G1 where xy': "(x, y) \<in> G1" and G1: "G1 \<in> c" ..
- from xz obtain G2 where xz': "(x, z) \<in> G2" and G2: "G2 \<in> c" ..
-
- from G1 c have "G1 \<in> M" ..
- then obtain H1 h1 where G1_rep: "G1 = graph H1 h1"
- unfolding M_def by blast
-
- from G2 c have "G2 \<in> M" ..
- then obtain H2 h2 where G2_rep: "G2 = graph H2 h2"
- unfolding M_def by blast
-
- txt {* @{text "G\<^sub>1"} is contained in @{text "G\<^sub>2"}
- or vice versa, since both @{text "G\<^sub>1"} and @{text
- "G\<^sub>2"} are members of @{text c}. \label{cases2}*}
-
- from cM G1 G2 have "G1 \<subseteq> G2 \<or> G2 \<subseteq> G1" (is "?case1 \<or> ?case2") ..
- then show ?thesis
- proof
- assume ?case1
- with xy' G2_rep have "(x, y) \<in> graph H2 h2" by blast
- then have "y = h2 x" ..
- also
- from xz' G2_rep have "(x, z) \<in> graph H2 h2" by (simp only:)
- then have "z = h2 x" ..
- finally show ?thesis .
- next
- assume ?case2
- with xz' G1_rep have "(x, z) \<in> graph H1 h1" by blast
- then have "z = h1 x" ..
- also
- from xy' G1_rep have "(x, y) \<in> graph H1 h1" by (simp only:)
- then have "y = h1 x" ..
- finally show ?thesis ..
- qed
-qed
-
-text {*
- \medskip The limit function @{text h} is linear. Every element
- @{text x} in the domain of @{text h} is in the domain of a function
- @{text h'} in the chain of norm preserving extensions. Furthermore,
- @{text h} is an extension of @{text h'} so the function values of
- @{text x} are identical for @{text h'} and @{text h}. Finally, the
- function @{text h'} is linear by construction of @{text M}.
-*}
-
-lemma sup_lf:
- assumes M: "M = norm_pres_extensions E p F f"
- and cM: "c \<in> chain M"
- and u: "graph H h = \<Union>c"
- shows "linearform H h"
-proof
- fix x y assume x: "x \<in> H" and y: "y \<in> H"
- with M cM u obtain H' h' where
- x': "x \<in> H'" and y': "y \<in> H'"
- and b: "graph H' h' \<subseteq> graph H h"
- and linearform: "linearform H' h'"
- and subspace: "H' \<unlhd> E"
- by (rule some_H'h'2 [elim_format]) blast
-
- show "h (x + y) = h x + h y"
- proof -
- from linearform x' y' have "h' (x + y) = h' x + h' y"
- by (rule linearform.add)
- also from b x' have "h' x = h x" ..
- also from b y' have "h' y = h y" ..
- also from subspace x' y' have "x + y \<in> H'"
- by (rule subspace.add_closed)
- with b have "h' (x + y) = h (x + y)" ..
- finally show ?thesis .
- qed
-next
- fix x a assume x: "x \<in> H"
- with M cM u obtain H' h' where
- x': "x \<in> H'"
- and b: "graph H' h' \<subseteq> graph H h"
- and linearform: "linearform H' h'"
- and subspace: "H' \<unlhd> E"
- by (rule some_H'h' [elim_format]) blast
-
- show "h (a \<cdot> x) = a * h x"
- proof -
- from linearform x' have "h' (a \<cdot> x) = a * h' x"
- by (rule linearform.mult)
- also from b x' have "h' x = h x" ..
- also from subspace x' have "a \<cdot> x \<in> H'"
- by (rule subspace.mult_closed)
- with b have "h' (a \<cdot> x) = h (a \<cdot> x)" ..
- finally show ?thesis .
- qed
-qed
-
-text {*
- \medskip The limit of a non-empty chain of norm preserving
- extensions of @{text f} is an extension of @{text f}, since every
- element of the chain is an extension of @{text f} and the supremum
- is an extension for every element of the chain.
-*}
-
-lemma sup_ext:
- 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 -
- from ex obtain x where xc: "x \<in> c" ..
- from cM have "c \<subseteq> M" ..
- with xc have "x \<in> M" ..
- with M have "x \<in> norm_pres_extensions E p F f"
- by (simp only:)
- then obtain G g where "x = graph G g" and "graph F f \<subseteq> graph G g" ..
- then have "graph F f \<subseteq> x" by (simp only:)
- also from xc have "\<dots> \<subseteq> \<Union>c" by blast
- also from graph have "\<dots> = graph H h" ..
- finally show ?thesis .
-qed
-
-text {*
- \medskip The domain @{text H} of the limit function is a superspace
- of @{text F}, since @{text F} is a subset of @{text H}. The
- existence of the @{text 0} element in @{text F} and the closure
- properties follow from the fact that @{text F} is a vector space.
-*}
-
-lemma sup_supF:
- assumes graph: "graph H h = \<Union>c"
- and M: "M = norm_pres_extensions E p F f"
- and cM: "c \<in> chain M"
- and ex: "\<exists>x. x \<in> c"
- and FE: "F \<unlhd> E"
- shows "F \<unlhd> H"
-proof
- from FE show "F \<noteq> {}" by (rule subspace.non_empty)
- from graph M cM ex have "graph F f \<subseteq> graph H h" by (rule sup_ext)
- then show "F \<subseteq> H" ..
- fix x y assume "x \<in> F" and "y \<in> F"
- with FE show "x + y \<in> F" by (rule subspace.add_closed)
-next
- fix x a assume "x \<in> F"
- with FE show "a \<cdot> x \<in> F" by (rule subspace.mult_closed)
-qed
-
-text {*
- \medskip The domain @{text H} of the limit function is a subspace of
- @{text E}.
-*}
-
-lemma sup_subE:
- 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 subspace.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
- fix x assume "x \<in> H"
- with M cM graph
- obtain H' h' where x: "x \<in> H'" and H'E: "H' \<unlhd> E"
- by (rule some_H'h' [elim_format]) blast
- from H'E have "H' \<subseteq> E" ..
- with x show "x \<in> E" ..
- qed
- fix x y assume x: "x \<in> H" and y: "y \<in> H"
- show "x + y \<in> H"
- proof -
- from M cM graph x y obtain H' h' where
- x': "x \<in> H'" and y': "y \<in> H'" and H'E: "H' \<unlhd> E"
- and graphs: "graph H' h' \<subseteq> graph H h"
- by (rule some_H'h'2 [elim_format]) blast
- from H'E x' y' have "x + y \<in> H'"
- by (rule subspace.add_closed)
- also from graphs have "H' \<subseteq> H" ..
- finally show ?thesis .
- qed
-next
- fix x a assume x: "x \<in> H"
- show "a \<cdot> x \<in> H"
- proof -
- from M cM graph x
- obtain H' h' where x': "x \<in> H'" and H'E: "H' \<unlhd> E"
- and graphs: "graph H' h' \<subseteq> graph H h"
- by (rule some_H'h' [elim_format]) blast
- from H'E x' have "a \<cdot> x \<in> H'" by (rule subspace.mult_closed)
- also from graphs have "H' \<subseteq> H" ..
- finally show ?thesis .
- qed
-qed
-
-text {*
- \medskip The limit function is bounded by the norm @{text p} as
- well, since all elements in the chain are bounded by @{text p}.
-*}
-
-lemma sup_norm_pres:
- 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
- fix x assume "x \<in> 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"
- by (rule some_H'h' [elim_format]) blast
- from graphs x' have [symmetric]: "h' x = h x" ..
- also from a x' have "h' x \<le> p x " ..
- finally show "h x \<le> p x" .
-qed
-
-text {*
- \medskip The following lemma is a property of linear forms on real
- vector spaces. It will be used for the lemma @{text abs_HahnBanach}
- (see page \pageref{abs-HahnBanach}). \label{abs-ineq-iff} For real
- vector spaces the following inequations are equivalent:
- \begin{center}
- \begin{tabular}{lll}
- @{text "\<forall>x \<in> H. \<bar>h x\<bar> \<le> p x"} & and &
- @{text "\<forall>x \<in> H. h x \<le> p x"} \\
- \end{tabular}
- \end{center}
-*}
-
-lemma abs_ineq_iff:
- assumes "subspace H E" and "vectorspace E" and "seminorm E p"
- and "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
- interpret subspace H E by fact
- interpret vectorspace E by fact
- interpret seminorm E p by fact
- interpret linearform H h by fact
- have H: "vectorspace H" using `vectorspace E` ..
- {
- assume l: ?L
- show ?R
- proof
- fix x assume x: "x \<in> H"
- 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: "x \<in> H"
- show "\<And>a b :: real. - a \<le> b \<Longrightarrow> b \<le> a \<Longrightarrow> \<bar>b\<bar> \<le> a"
- by arith
- from `linearform H h` and H x
- have "- h x = h (- x)" by (rule linearform.neg [symmetric])
- also
- from H x have "- x \<in> H" by (rule vectorspace.neg_closed)
- with r have "h (- x) \<le> p (- x)" ..
- also have "\<dots> = p x"
- using `seminorm E p` `vectorspace E`
- proof (rule seminorm.minus)
- from x show "x \<in> E" ..
- qed
- finally have "- h x \<le> p x" .
- then show "- p x \<le> h x" by simp
- from r x show "h x \<le> p x" ..
- qed
- }
-qed
-
-end
--- a/src/HOL/HahnBanach/Linearform.thy Wed Jun 24 21:28:02 2009 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,60 +0,0 @@
-(* Title: HOL/Real/HahnBanach/Linearform.thy
- Author: Gertrud Bauer, TU Munich
-*)
-
-header {* Linearforms *}
-
-theory Linearform
-imports VectorSpace
-begin
-
-text {*
- A \emph{linear form} is a function on a vector space into the reals
- that is additive and multiplicative.
-*}
-
-locale linearform =
- fixes V :: "'a\<Colon>{minus, plus, zero, uminus} set" and 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"
-
-declare linearform.intro [intro?]
-
-lemma (in linearform) neg [iff]:
- assumes "vectorspace V"
- shows "x \<in> V \<Longrightarrow> f (- x) = - f x"
-proof -
- interpret vectorspace V by fact
- assume x: "x \<in> V"
- then have "f (- x) = f ((- 1) \<cdot> x)" by (simp add: negate_eq1)
- also from x have "\<dots> = (- 1) * (f x)" by (rule mult)
- also from x have "\<dots> = - (f x)" by simp
- finally show ?thesis .
-qed
-
-lemma (in linearform) diff [iff]:
- assumes "vectorspace V"
- shows "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> f (x - y) = f x - f y"
-proof -
- interpret vectorspace V by fact
- assume x: "x \<in> V" and y: "y \<in> V"
- then have "x - y = x + - y" by (rule diff_eq1)
- also have "f \<dots> = f x + f (- y)" by (rule add) (simp_all add: x y)
- also have "f (- y) = - f y" using `vectorspace V` y by (rule neg)
- finally show ?thesis by simp
-qed
-
-text {* Every linear form yields @{text 0} for the @{text 0} vector. *}
-
-lemma (in linearform) zero [iff]:
- assumes "vectorspace V"
- shows "f 0 = 0"
-proof -
- interpret vectorspace V by fact
- have "f 0 = f (0 - 0)" by simp
- also have "\<dots> = f 0 - f 0" using `vectorspace V` by (rule diff) simp_all
- also have "\<dots> = 0" by simp
- finally show ?thesis .
-qed
-
-end
--- a/src/HOL/HahnBanach/NormedSpace.thy Wed Jun 24 21:28:02 2009 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,117 +0,0 @@
-(* Title: HOL/Real/HahnBanach/NormedSpace.thy
- Author: Gertrud Bauer, TU Munich
-*)
-
-header {* Normed vector spaces *}
-
-theory NormedSpace
-imports Subspace
-begin
-
-subsection {* Quasinorms *}
-
-text {*
- A \emph{seminorm} @{text "\<parallel>\<cdot>\<parallel>"} is a function on a real vector space
- into the reals that has the following properties: it is positive
- definite, absolute homogenous and subadditive.
-*}
-
-locale norm_syntax =
- fixes norm :: "'a \<Rightarrow> real" ("\<parallel>_\<parallel>")
-
-locale seminorm = var_V + norm_syntax +
- constrains V :: "'a\<Colon>{minus, plus, zero, uminus} set"
- 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>"
-
-declare seminorm.intro [intro?]
-
-lemma (in seminorm) diff_subadditive:
- assumes "vectorspace V"
- shows "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> \<parallel>x - y\<parallel> \<le> \<parallel>x\<parallel> + \<parallel>y\<parallel>"
-proof -
- interpret vectorspace V by fact
- assume x: "x \<in> V" and y: "y \<in> V"
- then have "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 (in seminorm) minus:
- assumes "vectorspace V"
- shows "x \<in> V \<Longrightarrow> \<parallel>- x\<parallel> = \<parallel>x\<parallel>"
-proof -
- 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 have "\<dots> = \<parallel>x\<parallel>" by simp
- finally show ?thesis .
-qed
-
-
-subsection {* Norms *}
-
-text {*
- A \emph{norm} @{text "\<parallel>\<cdot>\<parallel>"} is a seminorm that maps only the
- @{text 0} vector to @{text 0}.
-*}
-
-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}.
-*}
-
-locale normed_vectorspace = vectorspace + norm
-
-declare normed_vectorspace.intro [intro?]
-
-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
- assume "\<parallel>x\<parallel> = 0"
- with x have "x = 0" by simp
- with neq show False by contradiction
- qed
- finally show ?thesis .
-qed
-
-text {*
- Any subspace of a normed vector space is again a normed vectorspace.
-*}
-
-lemma subspace_normed_vs [intro?]:
- fixes F E norm
- assumes "subspace F E" "normed_vectorspace E norm"
- shows "normed_vectorspace F norm"
-proof -
- interpret subspace F E by fact
- interpret normed_vectorspace E norm by fact
- show ?thesis
- proof
- show "vectorspace F" by (rule vectorspace) unfold_locales
- next
- have "NormedSpace.norm E norm" ..
- with subset show "NormedSpace.norm F norm"
- by (simp add: norm_def seminorm_def norm_axioms_def)
- qed
-qed
-
-end
--- a/src/HOL/HahnBanach/README.html Wed Jun 24 21:28:02 2009 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,38 +0,0 @@
-<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
-
-<!-- $Id$ -->
-
-<HTML>
-
-<HEAD>
- <meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1">
- <TITLE>HOL/Real/HahnBanach/README</TITLE>
-</HEAD>
-
-<BODY>
-
-<H3>The Hahn-Banach Theorem for Real Vector Spaces (Isabelle/Isar)</H3>
-
-Author: Gertrud Bauer, Technische Universität München<P>
-
-This directory contains the proof of the Hahn-Banach theorem for real vectorspaces,
-following H. Heuser, Funktionalanalysis, p. 228 -232.
-The Hahn-Banach theorem is one of the fundamental theorems of functioal analysis.
-It is a conclusion of Zorn's lemma.<P>
-
-Two different formaulations of the theorem are presented, one for general real vectorspaces
-and its application to normed vectorspaces. <P>
-
-The theorem says, that every continous linearform, defined on arbitrary subspaces
-(not only one-dimensional subspaces), can be extended to a continous linearform on
-the whole vectorspace.
-
-
-<HR>
-
-<ADDRESS>
-<A NAME="bauerg@in.tum.de" HREF="mailto:bauerg@in.tum.de">bauerg@in.tum.de</A>
-</ADDRESS>
-
-</BODY>
-</HTML>
--- a/src/HOL/HahnBanach/ROOT.ML Wed Jun 24 21:28:02 2009 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,8 +0,0 @@
-(* Title: HOL/Real/HahnBanach/ROOT.ML
- ID: $Id$
- Author: Gertrud Bauer, TU Munich
-
-The Hahn-Banach theorem for real vector spaces (Isabelle/Isar).
-*)
-
-time_use_thy "HahnBanach";
--- a/src/HOL/HahnBanach/Subspace.thy Wed Jun 24 21:28:02 2009 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,513 +0,0 @@
-(* Title: HOL/Real/HahnBanach/Subspace.thy
- Author: Gertrud Bauer, TU Munich
-*)
-
-header {* Subspaces *}
-
-theory Subspace
-imports VectorSpace
-begin
-
-subsection {* Definition *}
-
-text {*
- A non-empty subset @{text U} of a vector space @{text V} is a
- \emph{subspace} of @{text V}, iff @{text U} is closed under addition
- and scalar multiplication.
-*}
-
-locale subspace =
- fixes U :: "'a\<Colon>{minus, plus, zero, uminus} set" and 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"
-
-notation (symbols)
- subspace (infix "\<unlhd>" 50)
-
-declare vectorspace.intro [intro?] subspace.intro [intro?]
-
-lemma subspace_subset [elim]: "U \<unlhd> V \<Longrightarrow> U \<subseteq> V"
- by (rule subspace.subset)
-
-lemma (in subspace) subsetD [iff]: "x \<in> U \<Longrightarrow> x \<in> V"
- using subset by blast
-
-lemma subspaceD [elim]: "U \<unlhd> V \<Longrightarrow> x \<in> U \<Longrightarrow> x \<in> V"
- by (rule subspace.subsetD)
-
-lemma rev_subspaceD [elim?]: "x \<in> U \<Longrightarrow> U \<unlhd> V \<Longrightarrow> x \<in> V"
- by (rule subspace.subsetD)
-
-lemma (in subspace) diff_closed [iff]:
- assumes "vectorspace V"
- assumes x: "x \<in> U" and y: "y \<in> U"
- shows "x - y \<in> U"
-proof -
- interpret vectorspace V by fact
- from x y show ?thesis by (simp add: diff_eq1 negate_eq1)
-qed
-
-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 subspace) zero [intro]:
- assumes "vectorspace V"
- shows "0 \<in> U"
-proof -
- interpret V: vectorspace V by fact
- have "U \<noteq> {}" by (rule non_empty)
- then obtain x where x: "x \<in> U" by blast
- then have "x \<in> V" .. then have "0 = x - x" by simp
- also from `vectorspace V` x x have "\<dots> \<in> U" by (rule diff_closed)
- finally show ?thesis .
-qed
-
-lemma (in subspace) neg_closed [iff]:
- assumes "vectorspace V"
- assumes x: "x \<in> U"
- shows "- x \<in> U"
-proof -
- interpret vectorspace V by fact
- from x show ?thesis by (simp add: negate_eq1)
-qed
-
-text {* \medskip Further derived laws: every subspace is a vector space. *}
-
-lemma (in subspace) vectorspace [iff]:
- assumes "vectorspace V"
- shows "vectorspace U"
-proof -
- interpret vectorspace V by fact
- show ?thesis
- 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
-qed
-
-
-text {* The subspace relation is reflexive. *}
-
-lemma (in vectorspace) subspace_refl [intro]: "V \<unlhd> V"
-proof
- show "V \<noteq> {}" ..
- show "V \<subseteq> V" ..
- 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 (in vectorspace) subspace_trans [trans]:
- "U \<unlhd> V \<Longrightarrow> V \<unlhd> W \<Longrightarrow> U \<unlhd> W"
-proof
- 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
- 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 {*
- The \emph{linear closure} of a vector @{text x} is the set of all
- scalar multiples of @{text x}.
-*}
-
-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
-
-lemma linI' [iff]: "a \<cdot> x \<in> lin x"
- unfolding lin_def by blast
-
-lemma linE [elim]: "x \<in> lin v \<Longrightarrow> (\<And>a::real. x = a \<cdot> v \<Longrightarrow> C) \<Longrightarrow> C"
- unfolding lin_def by blast
-
-
-text {* Every vector is contained in its linear closure. *}
-
-lemma (in vectorspace) x_lin_x [iff]: "x \<in> V \<Longrightarrow> x \<in> lin x"
-proof -
- assume "x \<in> V"
- then have "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"
- then show "0 = 0 \<cdot> x" by simp
-qed
-
-text {* Any linear closure is a subspace. *}
-
-lemma (in vectorspace) lin_subspace [intro]:
- "x \<in> V \<Longrightarrow> lin x \<unlhd> V"
-proof
- assume x: "x \<in> V"
- then show "lin x \<noteq> {}" by (auto simp add: x_lin_x)
- 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
- 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
- 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 (in vectorspace) lin_vectorspace [intro]:
- assumes "x \<in> V"
- shows "vectorspace (lin x)"
-proof -
- from `x \<in> V` have "subspace (lin x) V"
- by (rule lin_subspace)
- from this and vectorspace_axioms show ?thesis
- by (rule subspace.vectorspace)
-qed
-
-
-subsection {* Sum of two vectorspaces *}
-
-text {*
- The \emph{sum} of two vectorspaces @{text U} and @{text V} is the
- 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 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"
- unfolding sum_def by blast
-
-lemma sumI [intro]:
- "u \<in> U \<Longrightarrow> v \<in> V \<Longrightarrow> x = u + v \<Longrightarrow> x \<in> U + V"
- unfolding sum_def by blast
-
-lemma sumI' [intro]:
- "u \<in> U \<Longrightarrow> v \<in> V \<Longrightarrow> u + v \<in> U + V"
- unfolding sum_def by blast
-
-text {* @{text U} is a subspace of @{text "U + V"}. *}
-
-lemma subspace_sum1 [iff]:
- assumes "vectorspace U" "vectorspace V"
- shows "U \<unlhd> U + V"
-proof -
- interpret vectorspace U by fact
- interpret vectorspace V by fact
- show ?thesis
- proof
- show "U \<noteq> {}" ..
- show "U \<subseteq> U + 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
- qed
- fix x y assume x: "x \<in> U" and "y \<in> U"
- then show "x + y \<in> U" by simp
- from x show "\<And>a. a \<cdot> x \<in> U" by simp
- qed
-qed
-
-text {* The sum of two subspaces is again a subspace. *}
-
-lemma sum_subspace [intro?]:
- assumes "subspace U E" "vectorspace E" "subspace V E"
- shows "U + 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"
- 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"
- proof
- fix x assume "x \<in> U + 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"
- 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)
- then show ?thesis ..
- qed
- 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" ..
- then have "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)
- then show ?thesis ..
- qed
- qed
-qed
-
-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)"
- by (rule subspace.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
- V}. For every element @{text x} of the direct sum of @{text U} and
- @{text V} the decomposition in @{text "x = u + v"} with
- @{text "u \<in> U"} and @{text "v \<in> V"} is unique.
-*}
-
-lemma decomp:
- assumes "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 -
- interpret vectorspace E by fact
- interpret subspace U E by fact
- interpret subspace V E by fact
- show ?thesis
- proof
- have U: "vectorspace U" (* FIXME: use interpret *)
- using `subspace U E` `vectorspace E` by (rule subspace.vectorspace)
- have V: "vectorspace V"
- using `subspace V E` `vectorspace E` by (rule subspace.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 add_minus_eq)
- from u1 show "u1 \<in> E" ..
- from u2 show "u2 \<in> E" ..
- from u u' and direct show "u1 - u2 = 0" by blast
- qed
- show "v1 = v2"
- proof (rule add_minus_eq [symmetric])
- from v1 show "v1 \<in> E" ..
- from v2 show "v2 \<in> E" ..
- from v v' and direct show "v2 - v1 = 0" by blast
- qed
- qed
-qed
-
-text {*
- An application of the previous lemma will be used in the proof of
- the Hahn-Banach Theorem (see page \pageref{decomp-H-use}): for any
- element @{text "y + a \<cdot> x\<^sub>0"} of the direct sum of a
- vectorspace @{text H} and the linear closure of @{text "x\<^sub>0"}
- the components @{text "y \<in> H"} and @{text a} are uniquely
- determined.
-*}
-
-lemma decomp_H':
- assumes "vectorspace E" "subspace 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 -
- interpret vectorspace E by fact
- interpret subspace H E by fact
- show ?thesis
- proof
- 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}"
- proof
- show "H \<inter> lin x' \<subseteq> {0}"
- 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)
- with `x' \<notin> H` show ?thesis by contradiction
- qed
- then show "x \<in> {0}" ..
- qed
- show "{0} \<subseteq> H \<inter> lin x'"
- proof -
- have "0 \<in> H" using `vectorspace E` ..
- moreover have "0 \<in> lin x'" using `x' \<in> E` ..
- ultimately show ?thesis by blast
- qed
- qed
- show "lin x' \<unlhd> E" using `x' \<in> E` ..
- qed (rule `vectorspace E`, rule `subspace H E`, rule y1, rule y2, rule eq)
- then show "y1 = y2" ..
- from c have "a1 \<cdot> x' = a2 \<cdot> x'" ..
- with x' show "a1 = a2" by (simp add: mult_right_cancel)
- qed
-qed
-
-text {*
- Since for any element @{text "y + a \<cdot> x'"} of the direct sum of a
- vectorspace @{text H} and the linear closure of @{text x'} the
- components @{text "y \<in> H"} and @{text a} are unique, it follows from
- @{text "y \<in> H"} that @{text "a = 0"}.
-*}
-
-lemma decomp_H'_H:
- assumes "vectorspace E" "subspace 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 -
- interpret vectorspace E by fact
- interpret subspace H E by fact
- show ?thesis
- 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 (rule `vectorspace E`, rule `subspace H E`, rule t, (rule x')+)
- with t x' show "(y, a) = (y + a \<cdot> x', 0)" by simp
- qed
-qed
-
-text {*
- The components @{text "y \<in> H"} and @{text a} in @{text "y + a \<cdot> x'"}
- are unique, so the function @{text h'} defined by
- @{text "h' (y + a \<cdot> x') = h y + a \<cdot> \<xi>"} is definite.
-*}
-
-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)"
- and x: "x = y + a \<cdot> x'"
- assumes "vectorspace E" "subspace 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 -
- interpret vectorspace E by fact
- interpret subspace H E by fact
- 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 (rule ex_ex1I)
- 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 -
- 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
- qed (rule `vectorspace E`, rule `subspace H E`, (rule x')+)
- then show ?thesis by (cases p, cases q) simp
- qed
- qed
- then have eq: "(SOME (y, a). x = y + a \<cdot> x' \<and> y \<in> H) = (y, a)"
- 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
--- a/src/HOL/HahnBanach/VectorSpace.thy Wed Jun 24 21:28:02 2009 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,419 +0,0 @@
-(* Title: HOL/Real/HahnBanach/VectorSpace.thy
- ID: $Id$
- Author: Gertrud Bauer, TU Munich
-*)
-
-header {* Vector spaces *}
-
-theory VectorSpace
-imports Real Bounds Zorn
-begin
-
-subsection {* Signature *}
-
-text {*
- For the definition of real vector spaces a type @{typ 'a} of the
- sort @{text "{plus, minus, zero}"} is considered, on which a real
- scalar multiplication @{text \<cdot>} is declared.
-*}
-
-consts
- prod :: "real \<Rightarrow> 'a::{plus, minus, zero} \<Rightarrow> 'a" (infixr "'(*')" 70)
-
-notation (xsymbols)
- prod (infixr "\<cdot>" 70)
-notation (HTML output)
- prod (infixr "\<cdot>" 70)
-
-
-subsection {* Vector space laws *}
-
-text {*
- A \emph{vector space} is a non-empty set @{text V} of elements from
- @{typ 'a} with the following vector space laws: The set @{text V} is
- closed under addition and scalar multiplication, addition is
- associative and commutative; @{text "- x"} is the inverse of @{text
- x} w.~r.~t.~addition and @{text 0} is the neutral element of
- addition. Addition and multiplication are distributive; scalar
- multiplication is associative and the real number @{text "1"} is
- the neutral element of scalar multiplication.
-*}
-
-locale var_V = fixes V
-
-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"
-
-lemma (in vectorspace) 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"
- by (simp add: negate_eq1)
-
-lemma (in vectorspace) 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"
- by (simp add: diff_eq1 negate_eq1)
-
-lemma (in vectorspace) 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)"
-proof -
- assume xyz: "x \<in> V" "y \<in> V" "z \<in> V"
- then have "x + (y + z) = (x + y) + z"
- by (simp only: add_assoc)
- also from xyz have "\<dots> = (y + x) + z" by (simp only: add_commute)
- also from xyz have "\<dots> = y + (x + z)" by (simp only: add_assoc)
- finally show ?thesis .
-qed
-
-theorems (in vectorspace) 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"
-proof -
- 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 x have "\<dots> \<in> V" by (rule diff_closed)
- finally show ?thesis .
-qed
-
-lemma (in vectorspace) 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)
- also from x have "\<dots> = x" by (rule add_zero_left)
- finally show ?thesis .
-qed
-
-lemma (in vectorspace) 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"
- 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)"
-proof -
- assume x: "x \<in> V"
- have " (a - b) \<cdot> x = (a + - b) \<cdot> x"
- by (simp add: real_diff_def)
- also from x have "\<dots> = a \<cdot> x + (- b) \<cdot> x"
- by (rule add_mult_distrib2)
- also from x have "\<dots> = a \<cdot> x + - (b \<cdot> x)"
- by (simp add: negate_eq1 mult_assoc2)
- also from x have "\<dots> = 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 (in vectorspace) 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
- also have "\<dots> = (1 + - 1) \<cdot> x" by simp
- also from x have "\<dots> = 1 \<cdot> x + (- 1) \<cdot> x"
- by (rule add_mult_distrib2)
- also from x have "\<dots> = x + (- 1) \<cdot> x" by simp
- also from x have "\<dots> = x + - x" by (simp add: negate_eq2a)
- also from x have "\<dots> = x - x" by (simp add: diff_eq2)
- also from x have "\<dots> = 0" by simp
- finally show ?thesis .
-qed
-
-lemma (in vectorspace) 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"
- by (rule diff_mult_distrib1) simp_all
- also have "\<dots> = 0" by simp
- finally show ?thesis .
-qed
-
-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 (in vectorspace) 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)
- also from xy have "\<dots> = y - x" by (simp add: diff_eq1)
- finally show ?thesis .
-qed
-
-lemma (in vectorspace) 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"
- by (simp add: diff_eq2 add_commute)
-
-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 (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 "- \<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 (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 (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 (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 (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 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:)
- }
-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)"
- by (simp only: add_commute add_left_cancel)
-
-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 (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 (in vectorspace) mult_zero_uniq:
- "x \<in> V \<Longrightarrow> x \<noteq> 0 \<Longrightarrow> a \<cdot> x = 0 \<Longrightarrow> 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
- also have "\<dots> = 0" by simp
- finally have "x = 0" .
- 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)"
-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)"
- by (simp only: mult_assoc)
- also assume "a \<cdot> x = a \<cdot> y"
- also from a y have "inverse a \<cdot> \<dots> = 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 (in vectorspace) mult_right_cancel:
- "x \<in> V \<Longrightarrow> x \<noteq> 0 \<Longrightarrow> (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:)
- }
-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)"
-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" ..
- }
-qed
-
-lemma (in vectorspace) add_minus_eq_minus:
- "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> x + y = 0 \<Longrightarrow> 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 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"
-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)
- 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"
-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)"
- 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" .
- from vs have "a - c = (- c + (a + b)) + - b"
- by (simp add: add_ac diff_eq1)
- also from vs eq have "\<dots> = d + - b"
- by (simp add: add_right_cancel)
- also from vs have "\<dots> = d - b" by (simp add: diff_eq2)
- 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)"
-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])
- }
-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)"
-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" .
- }
-qed
-
-end
--- a/src/HOL/HahnBanach/ZornLemma.thy Wed Jun 24 21:28:02 2009 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,57 +0,0 @@
-(* Title: HOL/Real/HahnBanach/ZornLemma.thy
- Author: Gertrud Bauer, TU Munich
-*)
-
-header {* Zorn's Lemma *}
-
-theory ZornLemma
-imports Zorn
-begin
-
-text {*
- Zorn's Lemmas states: if every linear ordered subset of an ordered
- set @{text S} has an upper bound in @{text S}, then there exists a
- maximal element in @{text S}. In our application, @{text S} is a
- set of sets ordered by set inclusion. Since the union of a chain of
- sets is an upper bound for all elements of the chain, the conditions
- of Zorn's lemma can be modified: if @{text S} is non-empty, it
- suffices to show that for every non-empty chain @{text c} in @{text
- S} the union of @{text c} also lies in @{text S}.
-*}
-
-theorem Zorn's_Lemma:
- 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)
- 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 = {}"
- with aS show ?thesis by fast
-
- txt {* If @{text c} is non-empty, then @{text "\<Union>c"} is an upper
- bound of @{text c}, lying in @{text S}. *}
-
- next
- assume "c \<noteq> {}"
- show ?thesis
- proof
- show "\<forall>z \<in> c. z \<subseteq> \<Union>c" by fast
- show "\<Union>c \<in> S"
- proof (rule r)
- from `c \<noteq> {}` show "\<exists>x. x \<in> c" by fast
- show "c \<in> chain S" by fact
- qed
- qed
- qed
- qed
-qed
-
-end
--- a/src/HOL/HahnBanach/document/root.bib Wed Jun 24 21:28:02 2009 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,27 +0,0 @@
-
-@Book{Heuser:1986,
- author = {H. Heuser},
- title = {Funktionalanalysis: Theorie und Anwendung},
- publisher = {Teubner},
- year = 1986
-}
-
-@InCollection{Narici:1996,
- author = {L. Narici and E. Beckenstein},
- title = {The {Hahn-Banach Theorem}: The Life and Times},
- booktitle = {Topology Atlas},
- publisher = {York University, Toronto, Ontario, Canada},
- year = 1996,
- note = {\url{http://at.yorku.ca/topology/preprint.htm} and
- \url{http://at.yorku.ca/p/a/a/a/16.htm}}
-}
-
-@Article{Nowak:1993,
- author = {B. Nowak and A. Trybulec},
- title = {{Hahn-Banach} Theorem},
- journal = {Journal of Formalized Mathematics},
- year = {1993},
- volume = {5},
- institution = {University of Bialystok},
- note = {\url{http://mizar.uwb.edu.pl/JFM/Vol5/hahnban.html}}
-}
--- a/src/HOL/HahnBanach/document/root.tex Wed Jun 24 21:28:02 2009 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,83 +0,0 @@
-\documentclass[10pt,a4paper,twoside]{article}
-\usepackage{graphicx}
-\usepackage{latexsym,theorem}
-\usepackage{isabelle,isabellesym}
-\usepackage{pdfsetup} %last one!
-
-\isabellestyle{it}
-\urlstyle{rm}
-
-\newcommand{\isasymsup}{\isamath{\sup\,}}
-\newcommand{\skp}{\smallskip}
-
-
-\begin{document}
-
-\pagestyle{headings}
-\pagenumbering{arabic}
-
-\title{The Hahn-Banach Theorem \\ for Real Vector Spaces}
-\author{Gertrud Bauer \\ \url{http://www.in.tum.de/~bauerg/}}
-\maketitle
-
-\begin{abstract}
- The Hahn-Banach Theorem is one of the most fundamental results in functional
- analysis. We present a fully formal proof of two versions of the theorem,
- one for general linear spaces and another for normed spaces. This
- development is based on simply-typed classical set-theory, as provided by
- Isabelle/HOL.
-\end{abstract}
-
-
-\tableofcontents
-\parindent 0pt \parskip 0.5ex
-
-\clearpage
-\section{Preface}
-
-This is a fully formal proof of the Hahn-Banach Theorem. It closely follows
-the informal presentation given in Heuser's textbook \cite[{\S} 36]{Heuser:1986}.
-Another formal proof of the same theorem has been done in Mizar
-\cite{Nowak:1993}. A general overview of the relevance and history of the
-Hahn-Banach Theorem is given by Narici and Beckenstein \cite{Narici:1996}.
-
-\medskip The document is structured as follows. The first part contains
-definitions of basic notions of linear algebra: vector spaces, subspaces,
-normed spaces, continuous linear-forms, norm of functions and an order on
-functions by domain extension. The second part contains some lemmas about the
-supremum (w.r.t.\ the function order) and extension of non-maximal functions.
-With these preliminaries, the main proof of the theorem (in its two versions)
-is conducted in the third part. The dependencies of individual theories are
-as follows.
-
-\begin{center}
- \includegraphics[scale=0.5]{session_graph}
-\end{center}
-
-\clearpage
-\part {Basic Notions}
-
-\input{Bounds}
-\input{VectorSpace}
-\input{Subspace}
-\input{NormedSpace}
-\input{Linearform}
-\input{FunctionOrder}
-\input{FunctionNorm}
-\input{ZornLemma}
-
-\clearpage
-\part {Lemmas for the Proof}
-
-\input{HahnBanachSupLemmas}
-\input{HahnBanachExtLemmas}
-\input{HahnBanachLemmas}
-
-\clearpage
-\part {The Main Proof}
-
-\input{HahnBanach}
-\bibliographystyle{abbrv}
-\bibliography{root}
-
-\end{document}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Hahn_Banach/Bounds.thy Wed Jun 24 21:46:54 2009 +0200
@@ -0,0 +1,82 @@
+(* Title: HOL/Hahn_Banach/Bounds.thy
+ Author: Gertrud Bauer, TU Munich
+*)
+
+header {* Bounds *}
+
+theory Bounds
+imports Main ContNotDenum
+begin
+
+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
+
+definition
+ the_lub :: "'a::order set \<Rightarrow> 'a" where
+ "the_lub A = The (lub A)"
+
+notation (xsymbols)
+ the_lub ("\<Squnion>_" [90] 90)
+
+lemma the_lub_equality [elim?]:
+ assumes "lub A x"
+ shows "\<Squnion>A = (x::'a::order)"
+proof -
+ interpret lub A x by fact
+ show ?thesis
+ proof (unfold the_lub_def)
+ from `lub A x` 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
+qed
+
+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 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"
+ unfolding isUb_def setle_def by blast
+ with nonempty have "\<exists>x. isLub UNIV A x"
+ by (rule reals_complete)
+ then show ?thesis by (simp only: lub_compat)
+qed
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Hahn_Banach/Function_Norm.thy Wed Jun 24 21:46:54 2009 +0200
@@ -0,0 +1,278 @@
+(* Title: HOL/Hahn_Banach/Function_Norm.thy
+ Author: Gertrud Bauer, TU Munich
+*)
+
+header {* The norm of a function *}
+
+theory Function_Norm
+imports Normed_Space Function_Order
+begin
+
+subsection {* Continuous linear forms*}
+
+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.
+ \begin{center}
+ @{text "\<exists>c \<in> R. \<forall>x \<in> V. \<bar>f x\<bar> \<le> c \<cdot> \<parallel>x\<parallel>"}
+ \end{center}
+ In our application no other functions than linear forms are
+ considered, so we can define continuous linear forms as bounded
+ linear forms:
+*}
+
+locale continuous = var_V + norm_syntax + linearform +
+ assumes bounded: "\<exists>c. \<forall>x \<in> V. \<bar>f x\<bar> \<le> c * \<parallel>x\<parallel>"
+
+declare continuous.intro [intro?] continuous_axioms.intro [intro?]
+
+lemma continuousI [intro]:
+ fixes norm :: "_ \<Rightarrow> real" ("\<parallel>_\<parallel>")
+ assumes "linearform V f"
+ 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" by fact
+ 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 *}
+
+text {*
+ The least real number @{text c} for which holds
+ \begin{center}
+ @{text "\<forall>x \<in> V. \<bar>f x\<bar> \<le> c \<cdot> \<parallel>x\<parallel>"}
+ \end{center}
+ is called the \emph{norm} of @{text f}.
+
+ For non-trivial vector spaces @{text "V \<noteq> {0}"} the norm can be
+ defined as
+ \begin{center}
+ @{text "\<parallel>f\<parallel> = \<sup>x \<noteq> 0. \<bar>f x\<bar> / \<parallel>x\<parallel>"}
+ \end{center}
+
+ For the case @{text "V = {0}"} the supremum would be taken from an
+ empty set. Since @{text \<real>} is unbounded, there would be no supremum.
+ To avoid this situation it must be guaranteed that there is an
+ element in this set. This element must be @{text "{} \<ge> 0"} so that
+ @{text fn_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 are @{text "{} \<ge> 0"}.
+
+ 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}
+
+ @{text fn_norm} is equal to the supremum of @{text B}, if the
+ supremum exists (otherwise it is undefined).
+*}
+
+locale fn_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 fn_norm ("\<parallel>_\<parallel>\<hyphen>_" [0, 1000] 999)
+ defines "\<parallel>f\<parallel>\<hyphen>V \<equiv> \<Squnion>(B V f)"
+
+locale normed_vectorspace_with_fn_norm = normed_vectorspace + fn_norm
+
+lemma (in fn_norm) B_not_empty [intro]: "0 \<in> B V f"
+ by (simp add: B_def)
+
+text {*
+ The following lemma states that every continuous linear form on a
+ normed space @{text "(V, \<parallel>\<cdot>\<parallel>)"} has a function norm.
+*}
+
+lemma (in normed_vectorspace_with_fn_norm) fn_norm_works:
+ assumes "continuous V norm f"
+ shows "lub (B V f) (\<parallel>f\<parallel>\<hyphen>V)"
+proof -
+ interpret continuous V norm f by fact
+ 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. *}
+ have "\<exists>a. lub (B V f) a"
+ proof (rule real_complete)
+ txt {* First we have to show that @{text B} is non-empty: *}
+ have "0 \<in> B V f" ..
+ then show "\<exists>x. x \<in> B V f" ..
+
+ txt {* Then we have to show that @{text B} is bounded: *}
+ 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}. *}
+ from bounded obtain c where c: "\<forall>x \<in> V. \<bar>f x\<bar> \<le> c * \<parallel>x\<parallel>" ..
+
+ 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. *}
+
+ 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"
+ then show ?thesis unfolding b_def by 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>" ..
+
+ 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 mult_right_mono)
+ from c x show "\<bar>f x\<bar> \<le> c * \<parallel>x\<parallel>" ..
+ from gt have "0 < inverse \<parallel>x\<parallel>"
+ by (rule positive_imp_inverse_positive)
+ then show "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
+ 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)
+ finally show "y \<le> b" .
+ qed
+ qed
+ then show ?thesis ..
+ qed
+ qed
+ then show ?thesis unfolding fn_norm_def by (rule the_lubI_ex)
+qed
+
+lemma (in normed_vectorspace_with_fn_norm) fn_norm_ub [iff?]:
+ assumes "continuous V norm f"
+ assumes b: "b \<in> B V f"
+ shows "b \<le> \<parallel>f\<parallel>\<hyphen>V"
+proof -
+ interpret continuous V norm f by fact
+ have "lub (B V f) (\<parallel>f\<parallel>\<hyphen>V)"
+ using `continuous V norm f` by (rule fn_norm_works)
+ from this and b show ?thesis ..
+qed
+
+lemma (in normed_vectorspace_with_fn_norm) fn_norm_leastB:
+ assumes "continuous V norm f"
+ assumes b: "\<And>b. b \<in> B V f \<Longrightarrow> b \<le> y"
+ shows "\<parallel>f\<parallel>\<hyphen>V \<le> y"
+proof -
+ interpret continuous V norm f by fact
+ have "lub (B V f) (\<parallel>f\<parallel>\<hyphen>V)"
+ using `continuous V norm f` by (rule fn_norm_works)
+ from this and b show ?thesis ..
+qed
+
+text {* The norm of a continuous function is always @{text "\<ge> 0"}. *}
+
+lemma (in normed_vectorspace_with_fn_norm) fn_norm_ge_zero [iff]:
+ assumes "continuous V norm f"
+ shows "0 \<le> \<parallel>f\<parallel>\<hyphen>V"
+proof -
+ interpret continuous V norm f by fact
+ 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. *}
+ have "lub (B V f) (\<parallel>f\<parallel>\<hyphen>V)"
+ using `continuous V norm f` by (rule fn_norm_works)
+ moreover have "0 \<in> B V f" ..
+ ultimately show ?thesis ..
+qed
+
+text {*
+ \medskip The fundamental property of function norms is:
+ \begin{center}
+ @{text "\<bar>f x\<bar> \<le> \<parallel>f\<parallel> \<cdot> \<parallel>x\<parallel>"}
+ \end{center}
+*}
+
+lemma (in normed_vectorspace_with_fn_norm) fn_norm_le_cong:
+ assumes "continuous V norm f" "linearform V f"
+ assumes x: "x \<in> V"
+ shows "\<bar>f x\<bar> \<le> \<parallel>f\<parallel>\<hyphen>V * \<parallel>x\<parallel>"
+proof -
+ interpret continuous V norm f by fact
+ interpret linearform V f by fact
+ show ?thesis
+ proof cases
+ assume "x = 0"
+ then have "\<bar>f x\<bar> = \<bar>f 0\<bar>" by simp
+ also have "f 0 = 0" by rule unfold_locales
+ also have "\<bar>\<dots>\<bar> = 0" by simp
+ also have a: "0 \<le> \<parallel>f\<parallel>\<hyphen>V"
+ using `continuous V norm f` by (rule fn_norm_ge_zero)
+ from x have "0 \<le> norm x" ..
+ with a have "0 \<le> \<parallel>f\<parallel>\<hyphen>V * \<parallel>x\<parallel>" by (simp add: zero_le_mult_iff)
+ 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 mult_right_mono)
+ from x show "0 \<le> \<parallel>x\<parallel>" ..
+ from x and neq have "\<bar>f x\<bar> * inverse \<parallel>x\<parallel> \<in> B V f"
+ by (auto simp add: B_def real_divide_def)
+ with `continuous V norm f` show "\<bar>f x\<bar> * inverse \<parallel>x\<parallel> \<le> \<parallel>f\<parallel>\<hyphen>V"
+ by (rule fn_norm_ub)
+ qed
+ finally show ?thesis .
+ qed
+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>"}
+ \end{center}
+*}
+
+lemma (in normed_vectorspace_with_fn_norm) fn_norm_least [intro?]:
+ assumes "continuous V norm f"
+ 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 -
+ interpret continuous V norm f by fact
+ show ?thesis
+ proof (rule fn_norm_leastB [folded B_def fn_norm_def])
+ 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 mult_right_mono)
+ have "0 < \<parallel>x\<parallel>" using x x_neq ..
+ 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 (insert `continuous V norm f`, simp_all add: continuous_def)
+qed
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Hahn_Banach/Function_Order.thy Wed Jun 24 21:46:54 2009 +0200
@@ -0,0 +1,141 @@
+(* Title: HOL/Hahn_Banach/Function_Order.thy
+ Author: Gertrud Bauer, TU Munich
+*)
+
+header {* An order on functions *}
+
+theory Function_Order
+imports Subspace Linearform
+begin
+
+subsection {* The graph of a function *}
+
+text {*
+ We define the \emph{graph} of a (real) function @{text f} with
+ domain @{text F} as the set
+ \begin{center}
+ @{text "{(x, f x). x \<in> F}"}
+ \end{center}
+ So we are modeling partial functions by specifying the domain and
+ the mapping function. We use the term ``function'' also for its
+ graph.
+*}
+
+types '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}"
+
+lemma graphI [intro]: "x \<in> F \<Longrightarrow> (x, f x) \<in> graph F f"
+ unfolding graph_def by blast
+
+lemma graphI2 [intro?]: "x \<in> F \<Longrightarrow> \<exists>t \<in> graph F f. t = (x, f x)"
+ 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
+
+
+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'}.
+*}
+
+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'"
+ 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"
+ unfolding graph_def by blast
+
+lemma graph_extD2 [dest?]:
+ "graph H h \<subseteq> graph H' h' \<Longrightarrow> H \<subseteq> H'"
+ unfolding graph_def by blast
+
+
+subsection {* Domain and function of a graph *}
+
+text {*
+ The inverse functions to @{text graph} are @{text domain} and @{text
+ funct}.
+*}
+
+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))"
+
+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:
+ 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"
+ unfolding domain_def funct_def graph_def
+proof auto (* FIXME !? *)
+ fix a b assume g: "(a, b) \<in> g"
+ from g show "(a, SOME y. (a, y) \<in> g) \<in> g" by (rule someI2)
+ from g show "\<exists>y. (a, y) \<in> g" ..
+ from g show "b = (SOME y. (a, y) \<in> g)"
+ proof (rule some_equality [symmetric])
+ fix y assume "(a, y) \<in> g"
+ with g show "y = b" by (rule uniq)
+ qed
+qed
+
+
+subsection {* Norm-preserving extensions of a function *}
+
+text {*
+ Given a linear form @{text f} on the space @{text F} and a seminorm
+ @{text p} on @{text E}. The set of all linear extensions of @{text
+ f}, to superspaces @{text H} of @{text F}, which are bounded by
+ @{text p}, is defined as follows.
+*}
+
+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)}"
+
+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
+
+lemma norm_pres_extensionI2 [intro]:
+ "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"
+ unfolding norm_pres_extensions_def by blast
+
+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"
+ unfolding norm_pres_extensions_def by blast
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Hahn_Banach/Hahn_Banach.thy Wed Jun 24 21:46:54 2009 +0200
@@ -0,0 +1,509 @@
+(* Title: HOL/Hahn_Banach/Hahn_Banach.thy
+ Author: Gertrud Bauer, TU Munich
+*)
+
+header {* The Hahn-Banach Theorem *}
+
+theory Hahn_Banach
+imports Hahn_Banach_Lemmas
+begin
+
+text {*
+ We present the proof of two different versions of the Hahn-Banach
+ Theorem, closely following \cite[\S36]{Heuser:1986}.
+*}
+
+subsection {* The Hahn-Banach Theorem for vector spaces *}
+
+text {*
+ \textbf{Hahn-Banach Theorem.} Let @{text F} be a subspace of a real
+ vector space @{text E}, let @{text p} be a semi-norm on @{text E},
+ and @{text f} be a linear form defined on @{text F} such that @{text
+ f} is bounded by @{text p}, i.e. @{text "\<forall>x \<in> F. f x \<le> p x"}. Then
+ @{text f} can be extended to a linear form @{text h} on @{text E}
+ such that @{text h} is norm-preserving, i.e. @{text h} is also
+ bounded by @{text p}.
+
+ \bigskip
+ \textbf{Proof Sketch.}
+ \begin{enumerate}
+
+ \item Define @{text M} as the set of norm-preserving extensions of
+ @{text f} to subspaces of @{text E}. The linear forms in @{text M}
+ are ordered by domain extension.
+
+ \item We show that every non-empty chain in @{text M} has an upper
+ bound in @{text M}.
+
+ \item With Zorn's Lemma we conclude that there is a maximal function
+ @{text g} in @{text M}.
+
+ \item The domain @{text H} of @{text g} is the whole space @{text
+ E}, as shown by classical contradiction:
+
+ \begin{itemize}
+
+ \item Assuming @{text g} is not defined on whole @{text E}, it can
+ still be extended in a norm-preserving way to a super-space @{text
+ H'} of @{text H}.
+
+ \item Thus @{text g} can not be maximal. Contradiction!
+
+ \end{itemize}
+ \end{enumerate}
+*}
+
+theorem Hahn_Banach:
+ assumes E: "vectorspace E" and "subspace F E"
+ and "seminorm E p" and "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 -
+ interpret vectorspace E by fact
+ interpret subspace F E by fact
+ interpret seminorm E p by fact
+ interpret linearform F f by fact
+ def M \<equiv> "norm_pres_extensions E p F f"
+ then have M: "M = \<dots>" by (simp only:)
+ from E have F: "vectorspace F" ..
+ note FE = `F \<unlhd> E`
+ {
+ 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"}. *}
+ unfolding M_def
+ proof (rule norm_pres_extensionI)
+ let ?H = "domain (\<Union>c)"
+ let ?h = "funct (\<Union>c)"
+
+ 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 FE E have "?H \<unlhd> E"
+ by (rule sup_subE)
+ moreover from a M cM ex FE 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
+ }
+ then have "\<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: *}
+ show "graph F f \<in> M"
+ unfolding M_def
+ proof (rule norm_pres_extensionI2)
+ show "linearform F f" by fact
+ show "F \<unlhd> E" by fact
+ 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" by fact
+ qed
+ qed
+ then obtain g where gM: "g \<in> M" and gx: "\<forall>x \<in> M. g \<subseteq> x \<longrightarrow> g = x"
+ by blast
+ from gM 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" unfolding M_def ..
+ -- {* @{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 *}
+ from HE E have H: "vectorspace H"
+ by (rule subspace.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 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 -
+ 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)
+ with `x' \<notin> H` show False by contradiction
+ qed
+ 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 *}
+ have HH': "H \<unlhd> H'"
+ proof (unfold H'_def)
+ from x'E have "vectorspace (lin x')" ..
+ with H show "H \<unlhd> H + lin x'" ..
+ qed
+
+ obtain xi where
+ xi: "\<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: 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 E 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 by (blast intro: that)
+ 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 -
+ have "graph H h \<subseteq> graph H' h'"
+ proof (rule graph_extI)
+ fix t assume t: "t \<in> H"
+ from E HE t have "(SOME (y, a). t = y + a \<cdot> x' \<and> y \<in> H) = (t, 0)"
+ using `x' \<notin> H` `x' \<in> E` `x' \<noteq> 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
+ with g_rep show ?thesis by (simp only:)
+ qed
+
+ show "g \<noteq> graph H' h'"
+ proof -
+ have "graph H h \<noteq> graph H' h'"
+ proof
+ assume eq: "graph H h = graph H' h'"
+ have "x' \<in> H'"
+ unfolding H'_def
+ proof
+ 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
+ then have "(x', h' x') \<in> graph H' h'" ..
+ with eq have "(x', h' x') \<in> graph H h" by (simp only:)
+ then have "x' \<in> H" ..
+ with `x' \<notin> H` show False by contradiction
+ qed
+ with g_rep show ?thesis by simp
+ qed
+ qed
+ 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'"
+ using h'_def H'_def HE linearform `x' \<notin> H` `x' \<in> E` `x' \<noteq> 0` E
+ by (rule h'_lf)
+ show "H' \<unlhd> E"
+ unfolding H'_def
+ proof
+ show "H \<unlhd> E" by fact
+ show "vectorspace E" by fact
+ from x'E show "lin x' \<unlhd> E" ..
+ qed
+ from H `F \<unlhd> H` 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)"
+ using E HE
+ proof (rule decomp_H'_H [symmetric])
+ from FH x show "x \<in> H" ..
+ from x' show "x' \<noteq> 0" .
+ show "x' \<notin> H" by fact
+ show "x' \<in> E" by fact
+ 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"
+ using h'_def H'_def `x' \<notin> H` `x' \<in> E` `x' \<noteq> 0` E HE
+ `seminorm E p` linearform and hp xi
+ by (rule h'_norm_pres)
+ qed
+ qed
+ ultimately show ?thesis ..
+ qed
+ then have "\<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 *}
+ with gx 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
+
+
+subsection {* Alternative formulation *}
+
+text {*
+ The following alternative formulation of the Hahn-Banach
+ Theorem\label{abs-Hahn-Banach} uses the fact that for a real linear
+ form @{text f} and a seminorm @{text p} the following inequations
+ are equivalent:\footnote{This was shown in lemma @{thm [source]
+ abs_ineq_iff} (see page \pageref{abs-ineq-iff}).}
+ \begin{center}
+ \begin{tabular}{lll}
+ @{text "\<forall>x \<in> H. \<bar>h x\<bar> \<le> p x"} & and &
+ @{text "\<forall>x \<in> H. h x \<le> p x"} \\
+ \end{tabular}
+ \end{center}
+*}
+
+theorem abs_Hahn_Banach:
+ assumes E: "vectorspace E" and FE: "subspace F E"
+ and lf: "linearform F f" and sn: "seminorm 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 -
+ interpret vectorspace E by fact
+ interpret subspace F E by fact
+ interpret linearform F f by fact
+ interpret seminorm E p by fact
+ 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)"
+ using E FE sn lf
+ proof (rule Hahn_Banach)
+ show "\<forall>x \<in> F. f x \<le> p x"
+ using FE E sn lf and fp by (rule abs_ineq_iff [THEN iffD1])
+ qed
+ then obtain g where lg: "linearform E g" and *: "\<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"
+ using _ E sn lg **
+ proof (rule abs_ineq_iff [THEN iffD2])
+ show "E \<unlhd> E" ..
+ qed
+ with lg * show ?thesis by blast
+qed
+
+
+subsection {* The Hahn-Banach Theorem for normed spaces *}
+
+text {*
+ Every continuous linear form @{text f} on a subspace @{text F} of a
+ norm space @{text E}, can be extended to a continuous linear form
+ @{text g} on @{text E} such that @{text "\<parallel>f\<parallel> = \<parallel>g\<parallel>"}.
+*}
+
+theorem norm_Hahn_Banach:
+ fixes V and norm ("\<parallel>_\<parallel>")
+ fixes B defines "\<And>V f. B V f \<equiv> {0} \<union> {\<bar>f x\<bar> / \<parallel>x\<parallel> | x. x \<noteq> 0 \<and> x \<in> V}"
+ fixes fn_norm ("\<parallel>_\<parallel>\<hyphen>_" [0, 1000] 999)
+ defines "\<And>V f. \<parallel>f\<parallel>\<hyphen>V \<equiv> \<Squnion>(B V f)"
+ assumes E_norm: "normed_vectorspace E norm" and FE: "subspace F E"
+ and linearform: "linearform F f" and "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>\<hyphen>E = \<parallel>f\<parallel>\<hyphen>F"
+proof -
+ interpret normed_vectorspace E norm by fact
+ interpret normed_vectorspace_with_fn_norm E norm B fn_norm
+ by (auto simp: B_def fn_norm_def) intro_locales
+ interpret subspace F E by fact
+ interpret linearform F f by fact
+ interpret continuous F norm f by fact
+ have E: "vectorspace E" by intro_locales
+ have F: "vectorspace F" by rule intro_locales
+ have F_norm: "normed_vectorspace F norm"
+ using FE E_norm by (rule subspace_normed_vs)
+ have ge_zero: "0 \<le> \<parallel>f\<parallel>\<hyphen>F"
+ by (rule normed_vectorspace_with_fn_norm.fn_norm_ge_zero
+ [OF normed_vectorspace_with_fn_norm.intro,
+ OF F_norm `continuous F norm f` , folded B_def fn_norm_def])
+ 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 p} is positive definite: *}
+ have "0 \<le> \<parallel>f\<parallel>\<hyphen>F" by (rule ge_zero)
+ moreover from x have "0 \<le> \<parallel>x\<parallel>" ..
+ ultimately show "0 \<le> p x"
+ by (simp add: p_def zero_le_mult_iff)
+
+ 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>\<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: *}
+
+ 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 a: "0 \<le> \<parallel>f\<parallel>\<hyphen>F" by (rule ge_zero)
+ from x y have "\<parallel>x + y\<parallel> \<le> \<parallel>x\<parallel> + \<parallel>y\<parallel>" ..
+ with a have " \<parallel>f\<parallel>\<hyphen>F * \<parallel>x + y\<parallel> \<le> \<parallel>f\<parallel>\<hyphen>F * (\<parallel>x\<parallel> + \<parallel>y\<parallel>)"
+ by (simp add: mult_left_mono)
+ also have "\<dots> = \<parallel>f\<parallel>\<hyphen>F * \<parallel>x\<parallel> + \<parallel>f\<parallel>\<hyphen>F * \<parallel>y\<parallel>" by (simp only: right_distrib)
+ also have "\<dots> = p x + p y" by (simp only: p_def)
+ finally show ?thesis .
+ qed
+ qed
+
+ txt {* @{text f} is bounded by @{text p}. *}
+
+ have "\<forall>x \<in> F. \<bar>f x\<bar> \<le> p x"
+ proof
+ fix x assume "x \<in> F"
+ with `continuous F norm f` and linearform
+ show "\<bar>f x\<bar> \<le> p x"
+ unfolding p_def by (rule normed_vectorspace_with_fn_norm.fn_norm_le_cong
+ [OF normed_vectorspace_with_fn_norm.intro,
+ OF F_norm, folded B_def fn_norm_def])
+ qed
+
+ 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}. *}
+
+ 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_Hahn_Banach [elim_format]) iprover
+
+ 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>\<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>"}. *}
+
+ 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
+ \begin{center}
+ \begin{tabular}{l}
+ @{text "\<forall>x \<in> E. \<bar>g x\<bar> \<le> c \<cdot> \<parallel>x\<parallel>"}
+ \end{tabular}
+ \end{center}
+ \noindent Furthermore holds
+ \begin{center}
+ \begin{tabular}{l}
+ @{text "\<forall>x \<in> E. \<bar>g x\<bar> \<le> \<parallel>f\<parallel> \<cdot> \<parallel>x\<parallel>"}
+ \end{tabular}
+ \end{center}
+ *}
+
+ 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"
+ with b show "\<bar>g x\<bar> \<le> \<parallel>f\<parallel>\<hyphen>F * \<parallel>x\<parallel>"
+ by (simp only: p_def)
+ qed
+ from g_cont this ge_zero
+ show "\<parallel>g\<parallel>\<hyphen>E \<le> \<parallel>f\<parallel>\<hyphen>F"
+ by (rule fn_norm_least [of g, folded B_def fn_norm_def])
+
+ txt {* The other direction is achieved by a similar argument. *}
+
+ show "\<parallel>f\<parallel>\<hyphen>F \<le> \<parallel>g\<parallel>\<hyphen>E"
+ proof (rule normed_vectorspace_with_fn_norm.fn_norm_least
+ [OF normed_vectorspace_with_fn_norm.intro,
+ OF F_norm, folded B_def fn_norm_def])
+ show "\<forall>x \<in> F. \<bar>f x\<bar> \<le> \<parallel>g\<parallel>\<hyphen>E * \<parallel>x\<parallel>"
+ proof
+ fix x assume x: "x \<in> F"
+ from a x have "g x = f x" ..
+ then have "\<bar>f x\<bar> = \<bar>g x\<bar>" by (simp only:)
+ also from g_cont
+ have "\<dots> \<le> \<parallel>g\<parallel>\<hyphen>E * \<parallel>x\<parallel>"
+ proof (rule fn_norm_le_cong [OF _ linearformE, folded B_def fn_norm_def])
+ from FE x show "x \<in> E" ..
+ qed
+ finally show "\<bar>f x\<bar> \<le> \<parallel>g\<parallel>\<hyphen>E * \<parallel>x\<parallel>" .
+ qed
+ show "0 \<le> \<parallel>g\<parallel>\<hyphen>E"
+ using g_cont
+ by (rule fn_norm_ge_zero [of g, folded B_def fn_norm_def])
+ show "continuous F norm f" by fact
+ qed
+ qed
+ with linearformE a g_cont show ?thesis by blast
+qed
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Hahn_Banach/Hahn_Banach_Ext_Lemmas.thy Wed Jun 24 21:46:54 2009 +0200
@@ -0,0 +1,280 @@
+(* Title: HOL/Hahn_Banach/Hahn_Banach_Ext_Lemmas.thy
+ Author: Gertrud Bauer, TU Munich
+*)
+
+header {* Extending non-maximal functions *}
+
+theory Hahn_Banach_Ext_Lemmas
+imports Function_Norm
+begin
+
+text {*
+ In this section the following context is presumed. Let @{text E} be
+ a real vector space with a seminorm @{text q} on @{text E}. @{text
+ F} is a subspace of @{text E} and @{text f} a linear function on
+ @{text F}. We consider a subspace @{text H} of @{text E} that is a
+ superspace of @{text F} and a linear form @{text h} on @{text
+ H}. @{text H} is a not equal to @{text E} and @{text "x\<^sub>0"} is
+ 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>}.
+
+ Subsequently we show some properties of this extension @{text h'} of
+ @{text h}.
+
+ \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"}
+ \end{tabular}
+ \end{center}
+ \noindent it suffices to show that
+ \begin{center}
+ \begin{tabular}{l}
+ @{text "\<forall>u \<in> F. \<forall>v \<in> F. a u \<le> b v"}
+ \end{tabular}
+ \end{center}
+*}
+
+lemma ex_xi:
+ assumes "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 -
+ interpret vectorspace F by fact
+ 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 | 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
+ 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
+ } 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'}.
+*}
+
+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 HE: "H \<unlhd> E"
+ assumes "linearform H h"
+ assumes x0: "x0 \<notin> H" "x0 \<in> E" "x0 \<noteq> 0"
+ assumes E: "vectorspace E"
+ shows "linearform H' h'"
+proof -
+ interpret linearform H h by fact
+ interpret vectorspace E by fact
+ show ?thesis
+ proof
+ note E = `vectorspace E`
+ have H': "vectorspace H'"
+ proof (unfold H'_def)
+ from `x0 \<in> E`
+ have "lin x0 \<unlhd> E" ..
+ with HE show "vectorspace (H + lin x0)" using E ..
+ qed
+ {
+ fix x1 x2 assume x1: "x1 \<in> H'" and x2: "x2 \<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"
+ unfolding H'_def sum_def lin_def by blast
+
+ have ya: "y1 + y2 = y \<and> a1 + a2 = a" using E 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 E HE y x0
+ have "h' (x1 + x2) = h y + a * xi"
+ by (rule h'_definite)
+ 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 "\<dots> + (a1 + a2) * xi = (h y1 + a1 * xi) + (h y2 + a2 * xi)"
+ by (simp add: left_distrib)
+ also from h'_def x1_rep E HE y1 x0
+ have "h y1 + a1 * xi = h' x1"
+ by (rule h'_definite [symmetric])
+ also from h'_def x2_rep E HE y2 x0
+ have "h y2 + a2 * xi = h' x2"
+ by (rule h'_definite [symmetric])
+ finally show ?thesis .
+ qed
+ next
+ 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"
+ unfolding H'_def sum_def lin_def by blast
+
+ have ya: "c \<cdot> y1 = y \<and> c * a1 = a" using E HE _ y x0
+ proof (rule decomp_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
+
+ from h'_def cx1_rep E HE y x0 have "h' (c \<cdot> x1) = h y + a * xi"
+ by (rule h'_definite)
+ 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: right_distrib)
+ also from h'_def x1_rep E 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}. *}
+
+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 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"
+ 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 -
+ interpret vectorspace E by fact
+ interpret subspace H E by fact
+ interpret seminorm E p by fact
+ interpret linearform H h by fact
+ show ?thesis
+ 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"
+ unfolding H'_def sum_def lin_def by 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 E HE y x0 have "h' x = h y + a * xi"
+ by (rule h'_definite)
+ also have "\<dots> \<le> p (y + a \<cdot> x0)"
+ proof (rule linorder_cases)
+ assume z: "a = 0"
+ 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" then have nz: "a \<noteq> 0" by simp
+ 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 (simp add: mult_left_mono_neg order_less_imp_le)
+
+ also have "\<dots> =
+ - a * (p (inverse a \<cdot> y + x0)) - a * (h (inverse a \<cdot> y))"
+ by (simp add: right_diff_distrib)
+ 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)
+ 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" .
+ 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"}: *}
+ assume gz: "0 < a" then have nz: "a \<noteq> 0" by simp
+ 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 simp
+ also have "\<dots> = a * p (inverse a \<cdot> y + x0) - a * h (inverse a \<cdot> y)"
+ by (simp add: right_diff_distrib)
+ also from gz x0 y'
+ have "a * p (inverse a \<cdot> y + x0) = p (a \<cdot> (inverse a \<cdot> y + x0))"
+ by (simp add: abs_homogenous)
+ 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" .
+ then show ?thesis by simp
+ qed
+ also from x_rep have "\<dots> = p x" by (simp only:)
+ finally show ?thesis .
+ qed
+ qed
+qed
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Hahn_Banach/Hahn_Banach_Lemmas.thy Wed Jun 24 21:46:54 2009 +0200
@@ -0,0 +1,4 @@
+(*<*)
+theory Hahn_Banach_Lemmas imports Hahn_Banach_Sup_Lemmas Hahn_Banach_Ext_Lemmas begin
+end
+(*>*)
\ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Hahn_Banach/Hahn_Banach_Sup_Lemmas.thy Wed Jun 24 21:46:54 2009 +0200
@@ -0,0 +1,445 @@
+(* Title: HOL/Hahn_Banach/Hahn_Banach_Sup_Lemmas.thy
+ Author: Gertrud Bauer, TU Munich
+*)
+
+header {* The supremum w.r.t.~the function order *}
+
+theory Hahn_Banach_Sup_Lemmas
+imports Function_Norm Zorn_Lemma
+begin
+
+text {*
+ This section contains some lemmas that will be used in the proof of
+ the Hahn-Banach Theorem. In this section the following context is
+ presumed. Let @{text E} be a real vector space with a seminorm
+ @{text p} on @{text E}. @{text F} is a subspace of @{text E} and
+ @{text f} a linear form on @{text F}. We consider a chain @{text c}
+ of norm-preserving extensions of @{text f}, such that @{text "\<Union>c =
+ graph H h"}. We will show some properties about the limit function
+ @{text h}, i.e.\ the supremum of the chain @{text c}.
+
+ \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.
+*}
+lemmas [dest?] = chainD
+lemmas chainE2 [elim?] = chainD2 [elim_format, standard]
+
+lemma some_H'h't:
+ 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 -
+ from x have "(x, h x) \<in> graph H h" ..
+ also from u have "\<dots> = \<Union>c" .
+ finally obtain g where gc: "g \<in> c" and gh: "(x, h x) \<in> g" by blast
+
+ from cM have "c \<subseteq> M" ..
+ with gc have "g \<in> M" ..
+ also from M have "\<dots> = norm_pres_extensions E p F f" .
+ finally obtain H' and h' where g: "g = graph H' h'"
+ and * : "linearform H' h'" "H' \<unlhd> E" "F \<unlhd> H'"
+ "graph F f \<subseteq> graph H' h'" "\<forall>x \<in> H'. h' x \<le> p x" ..
+
+ from gc and g have "graph H' h' \<in> c" by (simp only:)
+ moreover from gh and g have "(x, h x) \<in> graph H' h'" by (simp only:)
+ ultimately show ?thesis using * by blast
+qed
+
+text {*
+ \medskip Let @{text c} be a chain of norm-preserving extensions of
+ the function @{text f} and let @{text "graph H h"} be the supremum
+ of @{text c}. Every element in the domain @{text H} of the supremum
+ function is member of the domain @{text H'} of some function @{text
+ h'}, such that @{text h} extends @{text h'}.
+*}
+
+lemma some_H'h':
+ 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 -
+ 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"
+ by (rule some_H'h't [elim_format]) blast
+ from x_hx have "x \<in> H'" ..
+ moreover from cM u c have "graph H' h' \<subseteq> graph H h"
+ by (simp only: chain_ball_Union_upper)
+ ultimately show ?thesis using * by blast
+qed
+
+text {*
+ \medskip Any two elements @{text x} and @{text y} in the domain
+ @{text H} of the supremum function @{text h} are both in the domain
+ @{text H'} of some function @{text h'}, such that @{text h} extends
+ @{text h'}.
+*}
+
+lemma some_H'h'2:
+ 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 -
+ txt {* @{text y} is in the domain @{text H''} of some function @{text h''},
+ such that @{text h} extends @{text h''}. *}
+
+ from M cM u and y obtain H' h' where
+ y_hy: "(y, h y) \<in> graph H' h'"
+ and c': "graph H' h' \<in> c"
+ and * :
+ "linearform H' h'" "H' \<unlhd> E" "F \<unlhd> H'"
+ "graph F f \<subseteq> graph H' h'" "\<forall>x \<in> H'. h' x \<le> p x"
+ by (rule some_H'h't [elim_format]) blast
+
+ txt {* @{text x} is in the domain @{text H'} of some function @{text h'},
+ such that @{text h} extends @{text h'}. *}
+
+ from M cM u and x obtain H'' h'' where
+ x_hx: "(x, h x) \<in> graph H'' h''"
+ and c'': "graph H'' h'' \<in> c"
+ and ** :
+ "linearform H'' h''" "H'' \<unlhd> E" "F \<unlhd> H''"
+ "graph F f \<subseteq> graph H'' h''" "\<forall>x \<in> H''. h'' x \<le> p x"
+ by (rule some_H'h't [elim_format]) blast
+
+ txt {* Since both @{text h'} and @{text h''} are elements of the chain,
+ @{text h''} is an extension of @{text h'} or vice versa. Thus both
+ @{text x} and @{text y} are contained in the greater
+ one. \label{cases1}*}
+
+ from cM c'' c' 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''" by fact
+ also have "\<dots> \<subseteq> graph H' h'" by fact
+ 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 {
+ have "(y, h y) \<in> graph H' h'" by (rule y_hy)
+ also have "\<dots> \<subseteq> graph H'' h''" by fact
+ 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.
+*}
+
+lemma sup_definite:
+ 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 -
+ from cM have c: "c \<subseteq> M" ..
+ from xy obtain G1 where xy': "(x, y) \<in> G1" and G1: "G1 \<in> c" ..
+ from xz obtain G2 where xz': "(x, z) \<in> G2" and G2: "G2 \<in> c" ..
+
+ from G1 c have "G1 \<in> M" ..
+ then obtain H1 h1 where G1_rep: "G1 = graph H1 h1"
+ unfolding M_def by blast
+
+ from G2 c have "G2 \<in> M" ..
+ then obtain H2 h2 where G2_rep: "G2 = graph H2 h2"
+ unfolding M_def by blast
+
+ txt {* @{text "G\<^sub>1"} is contained in @{text "G\<^sub>2"}
+ or vice versa, since both @{text "G\<^sub>1"} and @{text
+ "G\<^sub>2"} are members of @{text c}. \label{cases2}*}
+
+ from cM G1 G2 have "G1 \<subseteq> G2 \<or> G2 \<subseteq> G1" (is "?case1 \<or> ?case2") ..
+ then show ?thesis
+ proof
+ assume ?case1
+ with xy' G2_rep have "(x, y) \<in> graph H2 h2" by blast
+ then have "y = h2 x" ..
+ also
+ from xz' G2_rep have "(x, z) \<in> graph H2 h2" by (simp only:)
+ then have "z = h2 x" ..
+ finally show ?thesis .
+ next
+ assume ?case2
+ with xz' G1_rep have "(x, z) \<in> graph H1 h1" by blast
+ then have "z = h1 x" ..
+ also
+ from xy' G1_rep have "(x, y) \<in> graph H1 h1" by (simp only:)
+ then have "y = h1 x" ..
+ finally show ?thesis ..
+ qed
+qed
+
+text {*
+ \medskip The limit function @{text h} is linear. Every element
+ @{text x} in the domain of @{text h} is in the domain of a function
+ @{text h'} in the chain of norm preserving extensions. Furthermore,
+ @{text h} is an extension of @{text h'} so the function values of
+ @{text x} are identical for @{text h'} and @{text h}. Finally, the
+ function @{text h'} is linear by construction of @{text M}.
+*}
+
+lemma sup_lf:
+ assumes M: "M = norm_pres_extensions E p F f"
+ and cM: "c \<in> chain M"
+ and u: "graph H h = \<Union>c"
+ shows "linearform H h"
+proof
+ fix x y assume x: "x \<in> H" and y: "y \<in> H"
+ with M cM u obtain H' h' where
+ x': "x \<in> H'" and y': "y \<in> H'"
+ and b: "graph H' h' \<subseteq> graph H h"
+ and linearform: "linearform H' h'"
+ and subspace: "H' \<unlhd> E"
+ by (rule some_H'h'2 [elim_format]) blast
+
+ show "h (x + y) = h x + h y"
+ proof -
+ from linearform x' y' have "h' (x + y) = h' x + h' y"
+ by (rule linearform.add)
+ also from b x' have "h' x = h x" ..
+ also from b y' have "h' y = h y" ..
+ also from subspace x' y' have "x + y \<in> H'"
+ by (rule subspace.add_closed)
+ with b have "h' (x + y) = h (x + y)" ..
+ finally show ?thesis .
+ qed
+next
+ fix x a assume x: "x \<in> H"
+ with M cM u obtain H' h' where
+ x': "x \<in> H'"
+ and b: "graph H' h' \<subseteq> graph H h"
+ and linearform: "linearform H' h'"
+ and subspace: "H' \<unlhd> E"
+ by (rule some_H'h' [elim_format]) blast
+
+ show "h (a \<cdot> x) = a * h x"
+ proof -
+ from linearform x' have "h' (a \<cdot> x) = a * h' x"
+ by (rule linearform.mult)
+ also from b x' have "h' x = h x" ..
+ also from subspace x' have "a \<cdot> x \<in> H'"
+ by (rule subspace.mult_closed)
+ with b have "h' (a \<cdot> x) = h (a \<cdot> x)" ..
+ finally show ?thesis .
+ qed
+qed
+
+text {*
+ \medskip The limit of a non-empty chain of norm preserving
+ extensions of @{text f} is an extension of @{text f}, since every
+ element of the chain is an extension of @{text f} and the supremum
+ is an extension for every element of the chain.
+*}
+
+lemma sup_ext:
+ 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 -
+ from ex obtain x where xc: "x \<in> c" ..
+ from cM have "c \<subseteq> M" ..
+ with xc have "x \<in> M" ..
+ with M have "x \<in> norm_pres_extensions E p F f"
+ by (simp only:)
+ then obtain G g where "x = graph G g" and "graph F f \<subseteq> graph G g" ..
+ then have "graph F f \<subseteq> x" by (simp only:)
+ also from xc have "\<dots> \<subseteq> \<Union>c" by blast
+ also from graph have "\<dots> = graph H h" ..
+ finally show ?thesis .
+qed
+
+text {*
+ \medskip The domain @{text H} of the limit function is a superspace
+ of @{text F}, since @{text F} is a subset of @{text H}. The
+ existence of the @{text 0} element in @{text F} and the closure
+ properties follow from the fact that @{text F} is a vector space.
+*}
+
+lemma sup_supF:
+ assumes graph: "graph H h = \<Union>c"
+ and M: "M = norm_pres_extensions E p F f"
+ and cM: "c \<in> chain M"
+ and ex: "\<exists>x. x \<in> c"
+ and FE: "F \<unlhd> E"
+ shows "F \<unlhd> H"
+proof
+ from FE show "F \<noteq> {}" by (rule subspace.non_empty)
+ from graph M cM ex have "graph F f \<subseteq> graph H h" by (rule sup_ext)
+ then show "F \<subseteq> H" ..
+ fix x y assume "x \<in> F" and "y \<in> F"
+ with FE show "x + y \<in> F" by (rule subspace.add_closed)
+next
+ fix x a assume "x \<in> F"
+ with FE show "a \<cdot> x \<in> F" by (rule subspace.mult_closed)
+qed
+
+text {*
+ \medskip The domain @{text H} of the limit function is a subspace of
+ @{text E}.
+*}
+
+lemma sup_subE:
+ 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 subspace.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
+ fix x assume "x \<in> H"
+ with M cM graph
+ obtain H' h' where x: "x \<in> H'" and H'E: "H' \<unlhd> E"
+ by (rule some_H'h' [elim_format]) blast
+ from H'E have "H' \<subseteq> E" ..
+ with x show "x \<in> E" ..
+ qed
+ fix x y assume x: "x \<in> H" and y: "y \<in> H"
+ show "x + y \<in> H"
+ proof -
+ from M cM graph x y obtain H' h' where
+ x': "x \<in> H'" and y': "y \<in> H'" and H'E: "H' \<unlhd> E"
+ and graphs: "graph H' h' \<subseteq> graph H h"
+ by (rule some_H'h'2 [elim_format]) blast
+ from H'E x' y' have "x + y \<in> H'"
+ by (rule subspace.add_closed)
+ also from graphs have "H' \<subseteq> H" ..
+ finally show ?thesis .
+ qed
+next
+ fix x a assume x: "x \<in> H"
+ show "a \<cdot> x \<in> H"
+ proof -
+ from M cM graph x
+ obtain H' h' where x': "x \<in> H'" and H'E: "H' \<unlhd> E"
+ and graphs: "graph H' h' \<subseteq> graph H h"
+ by (rule some_H'h' [elim_format]) blast
+ from H'E x' have "a \<cdot> x \<in> H'" by (rule subspace.mult_closed)
+ also from graphs have "H' \<subseteq> H" ..
+ finally show ?thesis .
+ qed
+qed
+
+text {*
+ \medskip The limit function is bounded by the norm @{text p} as
+ well, since all elements in the chain are bounded by @{text p}.
+*}
+
+lemma sup_norm_pres:
+ 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
+ fix x assume "x \<in> 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"
+ 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_Hahn_Banach}
+ (see page \pageref{abs-Hahn_Banach}). \label{abs-ineq-iff} For real
+ vector spaces the following inequations are equivalent:
+ \begin{center}
+ \begin{tabular}{lll}
+ @{text "\<forall>x \<in> H. \<bar>h x\<bar> \<le> p x"} & and &
+ @{text "\<forall>x \<in> H. h x \<le> p x"} \\
+ \end{tabular}
+ \end{center}
+*}
+
+lemma abs_ineq_iff:
+ assumes "subspace H E" and "vectorspace E" and "seminorm E p"
+ and "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
+ interpret subspace H E by fact
+ interpret vectorspace E by fact
+ interpret seminorm E p by fact
+ interpret linearform H h by fact
+ have H: "vectorspace H" using `vectorspace E` ..
+ {
+ assume l: ?L
+ show ?R
+ proof
+ fix x assume x: "x \<in> H"
+ 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: "x \<in> H"
+ show "\<And>a b :: real. - a \<le> b \<Longrightarrow> b \<le> a \<Longrightarrow> \<bar>b\<bar> \<le> a"
+ by arith
+ from `linearform H h` and H x
+ have "- h x = h (- x)" by (rule linearform.neg [symmetric])
+ also
+ from H x have "- x \<in> H" by (rule vectorspace.neg_closed)
+ with r have "h (- x) \<le> p (- x)" ..
+ also have "\<dots> = p x"
+ using `seminorm E p` `vectorspace E`
+ proof (rule seminorm.minus)
+ from x show "x \<in> E" ..
+ qed
+ finally have "- h x \<le> p x" .
+ then show "- p x \<le> h x" by simp
+ from r x show "h x \<le> p x" ..
+ qed
+ }
+qed
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Hahn_Banach/Linearform.thy Wed Jun 24 21:46:54 2009 +0200
@@ -0,0 +1,60 @@
+(* Title: HOL/Hahn_Banach/Linearform.thy
+ Author: Gertrud Bauer, TU Munich
+*)
+
+header {* Linearforms *}
+
+theory Linearform
+imports Vector_Space
+begin
+
+text {*
+ A \emph{linear form} is a function on a vector space into the reals
+ that is additive and multiplicative.
+*}
+
+locale linearform =
+ fixes V :: "'a\<Colon>{minus, plus, zero, uminus} set" and 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"
+
+declare linearform.intro [intro?]
+
+lemma (in linearform) neg [iff]:
+ assumes "vectorspace V"
+ shows "x \<in> V \<Longrightarrow> f (- x) = - f x"
+proof -
+ interpret vectorspace V by fact
+ assume x: "x \<in> V"
+ then have "f (- x) = f ((- 1) \<cdot> x)" by (simp add: negate_eq1)
+ also from x have "\<dots> = (- 1) * (f x)" by (rule mult)
+ also from x have "\<dots> = - (f x)" by simp
+ finally show ?thesis .
+qed
+
+lemma (in linearform) diff [iff]:
+ assumes "vectorspace V"
+ shows "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> f (x - y) = f x - f y"
+proof -
+ interpret vectorspace V by fact
+ assume x: "x \<in> V" and y: "y \<in> V"
+ then have "x - y = x + - y" by (rule diff_eq1)
+ also have "f \<dots> = f x + f (- y)" by (rule add) (simp_all add: x y)
+ also have "f (- y) = - f y" using `vectorspace V` y by (rule neg)
+ finally show ?thesis by simp
+qed
+
+text {* Every linear form yields @{text 0} for the @{text 0} vector. *}
+
+lemma (in linearform) zero [iff]:
+ assumes "vectorspace V"
+ shows "f 0 = 0"
+proof -
+ interpret vectorspace V by fact
+ have "f 0 = f (0 - 0)" by simp
+ also have "\<dots> = f 0 - f 0" using `vectorspace V` by (rule diff) simp_all
+ also have "\<dots> = 0" by simp
+ finally show ?thesis .
+qed
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Hahn_Banach/Normed_Space.thy Wed Jun 24 21:46:54 2009 +0200
@@ -0,0 +1,117 @@
+(* Title: HOL/Hahn_Banach/Normed_Space.thy
+ Author: Gertrud Bauer, TU Munich
+*)
+
+header {* Normed vector spaces *}
+
+theory Normed_Space
+imports Subspace
+begin
+
+subsection {* Quasinorms *}
+
+text {*
+ A \emph{seminorm} @{text "\<parallel>\<cdot>\<parallel>"} is a function on a real vector space
+ into the reals that has the following properties: it is positive
+ definite, absolute homogenous and subadditive.
+*}
+
+locale norm_syntax =
+ fixes norm :: "'a \<Rightarrow> real" ("\<parallel>_\<parallel>")
+
+locale seminorm = var_V + norm_syntax +
+ constrains V :: "'a\<Colon>{minus, plus, zero, uminus} set"
+ 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>"
+
+declare seminorm.intro [intro?]
+
+lemma (in seminorm) diff_subadditive:
+ assumes "vectorspace V"
+ shows "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> \<parallel>x - y\<parallel> \<le> \<parallel>x\<parallel> + \<parallel>y\<parallel>"
+proof -
+ interpret vectorspace V by fact
+ assume x: "x \<in> V" and y: "y \<in> V"
+ then have "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 (in seminorm) minus:
+ assumes "vectorspace V"
+ shows "x \<in> V \<Longrightarrow> \<parallel>- x\<parallel> = \<parallel>x\<parallel>"
+proof -
+ 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 have "\<dots> = \<parallel>x\<parallel>" by simp
+ finally show ?thesis .
+qed
+
+
+subsection {* Norms *}
+
+text {*
+ A \emph{norm} @{text "\<parallel>\<cdot>\<parallel>"} is a seminorm that maps only the
+ @{text 0} vector to @{text 0}.
+*}
+
+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}.
+*}
+
+locale normed_vectorspace = vectorspace + norm
+
+declare normed_vectorspace.intro [intro?]
+
+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
+ assume "\<parallel>x\<parallel> = 0"
+ with x have "x = 0" by simp
+ with neq show False by contradiction
+ qed
+ finally show ?thesis .
+qed
+
+text {*
+ Any subspace of a normed vector space is again a normed vectorspace.
+*}
+
+lemma subspace_normed_vs [intro?]:
+ fixes F E norm
+ assumes "subspace F E" "normed_vectorspace E norm"
+ shows "normed_vectorspace F norm"
+proof -
+ interpret subspace F E by fact
+ interpret normed_vectorspace E norm by fact
+ show ?thesis
+ proof
+ show "vectorspace F" by (rule vectorspace) unfold_locales
+ next
+ have "Normed_Space.norm E norm" ..
+ with subset show "Normed_Space.norm F norm"
+ by (simp add: norm_def seminorm_def norm_axioms_def)
+ qed
+qed
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Hahn_Banach/README.html Wed Jun 24 21:46:54 2009 +0200
@@ -0,0 +1,38 @@
+<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
+
+<!-- $Id$ -->
+
+<HTML>
+
+<HEAD>
+ <meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1">
+ <TITLE>HOL/Hahn_Banach/README</TITLE>
+</HEAD>
+
+<BODY>
+
+<H3>The Hahn-Banach Theorem for Real Vector Spaces (Isabelle/Isar)</H3>
+
+Author: Gertrud Bauer, Technische Universität München<P>
+
+This directory contains the proof of the Hahn-Banach theorem for real vectorspaces,
+following H. Heuser, Funktionalanalysis, p. 228 -232.
+The Hahn-Banach theorem is one of the fundamental theorems of functioal analysis.
+It is a conclusion of Zorn's lemma.<P>
+
+Two different formaulations of the theorem are presented, one for general real vectorspaces
+and its application to normed vectorspaces. <P>
+
+The theorem says, that every continous linearform, defined on arbitrary subspaces
+(not only one-dimensional subspaces), can be extended to a continous linearform on
+the whole vectorspace.
+
+
+<HR>
+
+<ADDRESS>
+<A NAME="bauerg@in.tum.de" HREF="mailto:bauerg@in.tum.de">bauerg@in.tum.de</A>
+</ADDRESS>
+
+</BODY>
+</HTML>
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Hahn_Banach/ROOT.ML Wed Jun 24 21:46:54 2009 +0200
@@ -0,0 +1,7 @@
+(* Title: HOL/Hahn_Banach/ROOT.ML
+ Author: Gertrud Bauer, TU Munich
+
+The Hahn-Banach theorem for real vector spaces (Isabelle/Isar).
+*)
+
+use_thy "Hahn_Banach";
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Hahn_Banach/Subspace.thy Wed Jun 24 21:46:54 2009 +0200
@@ -0,0 +1,513 @@
+(* Title: HOL/Hahn_Banach/Subspace.thy
+ Author: Gertrud Bauer, TU Munich
+*)
+
+header {* Subspaces *}
+
+theory Subspace
+imports Vector_Space
+begin
+
+subsection {* Definition *}
+
+text {*
+ A non-empty subset @{text U} of a vector space @{text V} is a
+ \emph{subspace} of @{text V}, iff @{text U} is closed under addition
+ and scalar multiplication.
+*}
+
+locale subspace =
+ fixes U :: "'a\<Colon>{minus, plus, zero, uminus} set" and 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"
+
+notation (symbols)
+ subspace (infix "\<unlhd>" 50)
+
+declare vectorspace.intro [intro?] subspace.intro [intro?]
+
+lemma subspace_subset [elim]: "U \<unlhd> V \<Longrightarrow> U \<subseteq> V"
+ by (rule subspace.subset)
+
+lemma (in subspace) subsetD [iff]: "x \<in> U \<Longrightarrow> x \<in> V"
+ using subset by blast
+
+lemma subspaceD [elim]: "U \<unlhd> V \<Longrightarrow> x \<in> U \<Longrightarrow> x \<in> V"
+ by (rule subspace.subsetD)
+
+lemma rev_subspaceD [elim?]: "x \<in> U \<Longrightarrow> U \<unlhd> V \<Longrightarrow> x \<in> V"
+ by (rule subspace.subsetD)
+
+lemma (in subspace) diff_closed [iff]:
+ assumes "vectorspace V"
+ assumes x: "x \<in> U" and y: "y \<in> U"
+ shows "x - y \<in> U"
+proof -
+ interpret vectorspace V by fact
+ from x y show ?thesis by (simp add: diff_eq1 negate_eq1)
+qed
+
+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 subspace) zero [intro]:
+ assumes "vectorspace V"
+ shows "0 \<in> U"
+proof -
+ interpret V: vectorspace V by fact
+ have "U \<noteq> {}" by (rule non_empty)
+ then obtain x where x: "x \<in> U" by blast
+ then have "x \<in> V" .. then have "0 = x - x" by simp
+ also from `vectorspace V` x x have "\<dots> \<in> U" by (rule diff_closed)
+ finally show ?thesis .
+qed
+
+lemma (in subspace) neg_closed [iff]:
+ assumes "vectorspace V"
+ assumes x: "x \<in> U"
+ shows "- x \<in> U"
+proof -
+ interpret vectorspace V by fact
+ from x show ?thesis by (simp add: negate_eq1)
+qed
+
+text {* \medskip Further derived laws: every subspace is a vector space. *}
+
+lemma (in subspace) vectorspace [iff]:
+ assumes "vectorspace V"
+ shows "vectorspace U"
+proof -
+ interpret vectorspace V by fact
+ show ?thesis
+ 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
+qed
+
+
+text {* The subspace relation is reflexive. *}
+
+lemma (in vectorspace) subspace_refl [intro]: "V \<unlhd> V"
+proof
+ show "V \<noteq> {}" ..
+ show "V \<subseteq> V" ..
+ 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 (in vectorspace) subspace_trans [trans]:
+ "U \<unlhd> V \<Longrightarrow> V \<unlhd> W \<Longrightarrow> U \<unlhd> W"
+proof
+ 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
+ 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 {*
+ The \emph{linear closure} of a vector @{text x} is the set of all
+ scalar multiples of @{text x}.
+*}
+
+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
+
+lemma linI' [iff]: "a \<cdot> x \<in> lin x"
+ unfolding lin_def by blast
+
+lemma linE [elim]: "x \<in> lin v \<Longrightarrow> (\<And>a::real. x = a \<cdot> v \<Longrightarrow> C) \<Longrightarrow> C"
+ unfolding lin_def by blast
+
+
+text {* Every vector is contained in its linear closure. *}
+
+lemma (in vectorspace) x_lin_x [iff]: "x \<in> V \<Longrightarrow> x \<in> lin x"
+proof -
+ assume "x \<in> V"
+ then have "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"
+ then show "0 = 0 \<cdot> x" by simp
+qed
+
+text {* Any linear closure is a subspace. *}
+
+lemma (in vectorspace) lin_subspace [intro]:
+ "x \<in> V \<Longrightarrow> lin x \<unlhd> V"
+proof
+ assume x: "x \<in> V"
+ then show "lin x \<noteq> {}" by (auto simp add: x_lin_x)
+ 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
+ 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
+ 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 (in vectorspace) lin_vectorspace [intro]:
+ assumes "x \<in> V"
+ shows "vectorspace (lin x)"
+proof -
+ from `x \<in> V` have "subspace (lin x) V"
+ by (rule lin_subspace)
+ from this and vectorspace_axioms show ?thesis
+ by (rule subspace.vectorspace)
+qed
+
+
+subsection {* Sum of two vectorspaces *}
+
+text {*
+ The \emph{sum} of two vectorspaces @{text U} and @{text V} is the
+ 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 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"
+ unfolding sum_def by blast
+
+lemma sumI [intro]:
+ "u \<in> U \<Longrightarrow> v \<in> V \<Longrightarrow> x = u + v \<Longrightarrow> x \<in> U + V"
+ unfolding sum_def by blast
+
+lemma sumI' [intro]:
+ "u \<in> U \<Longrightarrow> v \<in> V \<Longrightarrow> u + v \<in> U + V"
+ unfolding sum_def by blast
+
+text {* @{text U} is a subspace of @{text "U + V"}. *}
+
+lemma subspace_sum1 [iff]:
+ assumes "vectorspace U" "vectorspace V"
+ shows "U \<unlhd> U + V"
+proof -
+ interpret vectorspace U by fact
+ interpret vectorspace V by fact
+ show ?thesis
+ proof
+ show "U \<noteq> {}" ..
+ show "U \<subseteq> U + 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
+ qed
+ fix x y assume x: "x \<in> U" and "y \<in> U"
+ then show "x + y \<in> U" by simp
+ from x show "\<And>a. a \<cdot> x \<in> U" by simp
+ qed
+qed
+
+text {* The sum of two subspaces is again a subspace. *}
+
+lemma sum_subspace [intro?]:
+ assumes "subspace U E" "vectorspace E" "subspace V E"
+ shows "U + 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"
+ 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"
+ proof
+ fix x assume "x \<in> U + 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"
+ 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)
+ then show ?thesis ..
+ qed
+ 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" ..
+ then have "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)
+ then show ?thesis ..
+ qed
+ qed
+qed
+
+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)"
+ by (rule subspace.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
+ V}. For every element @{text x} of the direct sum of @{text U} and
+ @{text V} the decomposition in @{text "x = u + v"} with
+ @{text "u \<in> U"} and @{text "v \<in> V"} is unique.
+*}
+
+lemma decomp:
+ assumes "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 -
+ interpret vectorspace E by fact
+ interpret subspace U E by fact
+ interpret subspace V E by fact
+ show ?thesis
+ proof
+ have U: "vectorspace U" (* FIXME: use interpret *)
+ using `subspace U E` `vectorspace E` by (rule subspace.vectorspace)
+ have V: "vectorspace V"
+ using `subspace V E` `vectorspace E` by (rule subspace.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 add_minus_eq)
+ from u1 show "u1 \<in> E" ..
+ from u2 show "u2 \<in> E" ..
+ from u u' and direct show "u1 - u2 = 0" by blast
+ qed
+ show "v1 = v2"
+ proof (rule add_minus_eq [symmetric])
+ from v1 show "v1 \<in> E" ..
+ from v2 show "v2 \<in> E" ..
+ from v v' and direct show "v2 - v1 = 0" by blast
+ qed
+ qed
+qed
+
+text {*
+ An application of the previous lemma will be used in the proof of
+ the Hahn-Banach Theorem (see page \pageref{decomp-H-use}): for any
+ element @{text "y + a \<cdot> x\<^sub>0"} of the direct sum of a
+ vectorspace @{text H} and the linear closure of @{text "x\<^sub>0"}
+ the components @{text "y \<in> H"} and @{text a} are uniquely
+ determined.
+*}
+
+lemma decomp_H':
+ assumes "vectorspace E" "subspace 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 -
+ interpret vectorspace E by fact
+ interpret subspace H E by fact
+ show ?thesis
+ proof
+ 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}"
+ proof
+ show "H \<inter> lin x' \<subseteq> {0}"
+ 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)
+ with `x' \<notin> H` show ?thesis by contradiction
+ qed
+ then show "x \<in> {0}" ..
+ qed
+ show "{0} \<subseteq> H \<inter> lin x'"
+ proof -
+ have "0 \<in> H" using `vectorspace E` ..
+ moreover have "0 \<in> lin x'" using `x' \<in> E` ..
+ ultimately show ?thesis by blast
+ qed
+ qed
+ show "lin x' \<unlhd> E" using `x' \<in> E` ..
+ qed (rule `vectorspace E`, rule `subspace H E`, rule y1, rule y2, rule eq)
+ then show "y1 = y2" ..
+ from c have "a1 \<cdot> x' = a2 \<cdot> x'" ..
+ with x' show "a1 = a2" by (simp add: mult_right_cancel)
+ qed
+qed
+
+text {*
+ Since for any element @{text "y + a \<cdot> x'"} of the direct sum of a
+ vectorspace @{text H} and the linear closure of @{text x'} the
+ components @{text "y \<in> H"} and @{text a} are unique, it follows from
+ @{text "y \<in> H"} that @{text "a = 0"}.
+*}
+
+lemma decomp_H'_H:
+ assumes "vectorspace E" "subspace 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 -
+ interpret vectorspace E by fact
+ interpret subspace H E by fact
+ show ?thesis
+ 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 (rule `vectorspace E`, rule `subspace H E`, rule t, (rule x')+)
+ with t x' show "(y, a) = (y + a \<cdot> x', 0)" by simp
+ qed
+qed
+
+text {*
+ The components @{text "y \<in> H"} and @{text a} in @{text "y + a \<cdot> x'"}
+ are unique, so the function @{text h'} defined by
+ @{text "h' (y + a \<cdot> x') = h y + a \<cdot> \<xi>"} is definite.
+*}
+
+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)"
+ and x: "x = y + a \<cdot> x'"
+ assumes "vectorspace E" "subspace 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 -
+ interpret vectorspace E by fact
+ interpret subspace H E by fact
+ 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 (rule ex_ex1I)
+ 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 -
+ 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
+ qed (rule `vectorspace E`, rule `subspace H E`, (rule x')+)
+ then show ?thesis by (cases p, cases q) simp
+ qed
+ qed
+ then have eq: "(SOME (y, a). x = y + a \<cdot> x' \<and> y \<in> H) = (y, a)"
+ 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
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Hahn_Banach/Vector_Space.thy Wed Jun 24 21:46:54 2009 +0200
@@ -0,0 +1,418 @@
+(* Title: HOL/Hahn_Banach/Vector_Space.thy
+ Author: Gertrud Bauer, TU Munich
+*)
+
+header {* Vector spaces *}
+
+theory Vector_Space
+imports Real Bounds Zorn
+begin
+
+subsection {* Signature *}
+
+text {*
+ For the definition of real vector spaces a type @{typ 'a} of the
+ sort @{text "{plus, minus, zero}"} is considered, on which a real
+ scalar multiplication @{text \<cdot>} is declared.
+*}
+
+consts
+ prod :: "real \<Rightarrow> 'a::{plus, minus, zero} \<Rightarrow> 'a" (infixr "'(*')" 70)
+
+notation (xsymbols)
+ prod (infixr "\<cdot>" 70)
+notation (HTML output)
+ prod (infixr "\<cdot>" 70)
+
+
+subsection {* Vector space laws *}
+
+text {*
+ A \emph{vector space} is a non-empty set @{text V} of elements from
+ @{typ 'a} with the following vector space laws: The set @{text V} is
+ closed under addition and scalar multiplication, addition is
+ associative and commutative; @{text "- x"} is the inverse of @{text
+ x} w.~r.~t.~addition and @{text 0} is the neutral element of
+ addition. Addition and multiplication are distributive; scalar
+ multiplication is associative and the real number @{text "1"} is
+ the neutral element of scalar multiplication.
+*}
+
+locale var_V = fixes V
+
+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"
+
+lemma (in vectorspace) 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"
+ by (simp add: negate_eq1)
+
+lemma (in vectorspace) 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"
+ by (simp add: diff_eq1 negate_eq1)
+
+lemma (in vectorspace) 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)"
+proof -
+ assume xyz: "x \<in> V" "y \<in> V" "z \<in> V"
+ then have "x + (y + z) = (x + y) + z"
+ by (simp only: add_assoc)
+ also from xyz have "\<dots> = (y + x) + z" by (simp only: add_commute)
+ also from xyz have "\<dots> = y + (x + z)" by (simp only: add_assoc)
+ finally show ?thesis .
+qed
+
+theorems (in vectorspace) 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"
+proof -
+ 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 x have "\<dots> \<in> V" by (rule diff_closed)
+ finally show ?thesis .
+qed
+
+lemma (in vectorspace) 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)
+ also from x have "\<dots> = x" by (rule add_zero_left)
+ finally show ?thesis .
+qed
+
+lemma (in vectorspace) 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"
+ 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)"
+proof -
+ assume x: "x \<in> V"
+ have " (a - b) \<cdot> x = (a + - b) \<cdot> x"
+ by (simp add: real_diff_def)
+ also from x have "\<dots> = a \<cdot> x + (- b) \<cdot> x"
+ by (rule add_mult_distrib2)
+ also from x have "\<dots> = a \<cdot> x + - (b \<cdot> x)"
+ by (simp add: negate_eq1 mult_assoc2)
+ also from x have "\<dots> = 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 (in vectorspace) 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
+ also have "\<dots> = (1 + - 1) \<cdot> x" by simp
+ also from x have "\<dots> = 1 \<cdot> x + (- 1) \<cdot> x"
+ by (rule add_mult_distrib2)
+ also from x have "\<dots> = x + (- 1) \<cdot> x" by simp
+ also from x have "\<dots> = x + - x" by (simp add: negate_eq2a)
+ also from x have "\<dots> = x - x" by (simp add: diff_eq2)
+ also from x have "\<dots> = 0" by simp
+ finally show ?thesis .
+qed
+
+lemma (in vectorspace) 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"
+ by (rule diff_mult_distrib1) simp_all
+ also have "\<dots> = 0" by simp
+ finally show ?thesis .
+qed
+
+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 (in vectorspace) 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)
+ also from xy have "\<dots> = y - x" by (simp add: diff_eq1)
+ finally show ?thesis .
+qed
+
+lemma (in vectorspace) 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"
+ by (simp add: diff_eq2 add_commute)
+
+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 (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 "- \<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 (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 (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 (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 (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 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:)
+ }
+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)"
+ by (simp only: add_commute add_left_cancel)
+
+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 (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 (in vectorspace) mult_zero_uniq:
+ "x \<in> V \<Longrightarrow> x \<noteq> 0 \<Longrightarrow> a \<cdot> x = 0 \<Longrightarrow> 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
+ also have "\<dots> = 0" by simp
+ finally have "x = 0" .
+ 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)"
+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)"
+ by (simp only: mult_assoc)
+ also assume "a \<cdot> x = a \<cdot> y"
+ also from a y have "inverse a \<cdot> \<dots> = 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 (in vectorspace) mult_right_cancel:
+ "x \<in> V \<Longrightarrow> x \<noteq> 0 \<Longrightarrow> (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:)
+ }
+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)"
+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" ..
+ }
+qed
+
+lemma (in vectorspace) add_minus_eq_minus:
+ "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> x + y = 0 \<Longrightarrow> 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 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"
+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)
+ 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"
+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)"
+ 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" .
+ from vs have "a - c = (- c + (a + b)) + - b"
+ by (simp add: add_ac diff_eq1)
+ also from vs eq have "\<dots> = d + - b"
+ by (simp add: add_right_cancel)
+ also from vs have "\<dots> = d - b" by (simp add: diff_eq2)
+ 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)"
+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])
+ }
+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)"
+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" .
+ }
+qed
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Hahn_Banach/Zorn_Lemma.thy Wed Jun 24 21:46:54 2009 +0200
@@ -0,0 +1,57 @@
+(* Title: HOL/Hahn_Banach/Zorn_Lemma.thy
+ Author: Gertrud Bauer, TU Munich
+*)
+
+header {* Zorn's Lemma *}
+
+theory Zorn_Lemma
+imports Zorn
+begin
+
+text {*
+ Zorn's Lemmas states: if every linear ordered subset of an ordered
+ set @{text S} has an upper bound in @{text S}, then there exists a
+ maximal element in @{text S}. In our application, @{text S} is a
+ set of sets ordered by set inclusion. Since the union of a chain of
+ sets is an upper bound for all elements of the chain, the conditions
+ of Zorn's lemma can be modified: if @{text S} is non-empty, it
+ suffices to show that for every non-empty chain @{text c} in @{text
+ S} the union of @{text c} also lies in @{text S}.
+*}
+
+theorem Zorn's_Lemma:
+ 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)
+ 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 = {}"
+ with aS show ?thesis by fast
+
+ txt {* If @{text c} is non-empty, then @{text "\<Union>c"} is an upper
+ bound of @{text c}, lying in @{text S}. *}
+
+ next
+ assume "c \<noteq> {}"
+ show ?thesis
+ proof
+ show "\<forall>z \<in> c. z \<subseteq> \<Union>c" by fast
+ show "\<Union>c \<in> S"
+ proof (rule r)
+ from `c \<noteq> {}` show "\<exists>x. x \<in> c" by fast
+ show "c \<in> chain S" by fact
+ qed
+ qed
+ qed
+ qed
+qed
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Hahn_Banach/document/root.bib Wed Jun 24 21:46:54 2009 +0200
@@ -0,0 +1,27 @@
+
+@Book{Heuser:1986,
+ author = {H. Heuser},
+ title = {Funktionalanalysis: Theorie und Anwendung},
+ publisher = {Teubner},
+ year = 1986
+}
+
+@InCollection{Narici:1996,
+ author = {L. Narici and E. Beckenstein},
+ title = {The {Hahn-Banach Theorem}: The Life and Times},
+ booktitle = {Topology Atlas},
+ publisher = {York University, Toronto, Ontario, Canada},
+ year = 1996,
+ note = {\url{http://at.yorku.ca/topology/preprint.htm} and
+ \url{http://at.yorku.ca/p/a/a/a/16.htm}}
+}
+
+@Article{Nowak:1993,
+ author = {B. Nowak and A. Trybulec},
+ title = {{Hahn-Banach} Theorem},
+ journal = {Journal of Formalized Mathematics},
+ year = {1993},
+ volume = {5},
+ institution = {University of Bialystok},
+ note = {\url{http://mizar.uwb.edu.pl/JFM/Vol5/hahnban.html}}
+}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Hahn_Banach/document/root.tex Wed Jun 24 21:46:54 2009 +0200
@@ -0,0 +1,83 @@
+\documentclass[10pt,a4paper,twoside]{article}
+\usepackage{graphicx}
+\usepackage{latexsym,theorem}
+\usepackage{isabelle,isabellesym}
+\usepackage{pdfsetup} %last one!
+
+\isabellestyle{it}
+\urlstyle{rm}
+
+\newcommand{\isasymsup}{\isamath{\sup\,}}
+\newcommand{\skp}{\smallskip}
+
+
+\begin{document}
+
+\pagestyle{headings}
+\pagenumbering{arabic}
+
+\title{The Hahn-Banach Theorem \\ for Real Vector Spaces}
+\author{Gertrud Bauer \\ \url{http://www.in.tum.de/~bauerg/}}
+\maketitle
+
+\begin{abstract}
+ The Hahn-Banach Theorem is one of the most fundamental results in functional
+ analysis. We present a fully formal proof of two versions of the theorem,
+ one for general linear spaces and another for normed spaces. This
+ development is based on simply-typed classical set-theory, as provided by
+ Isabelle/HOL.
+\end{abstract}
+
+
+\tableofcontents
+\parindent 0pt \parskip 0.5ex
+
+\clearpage
+\section{Preface}
+
+This is a fully formal proof of the Hahn-Banach Theorem. It closely follows
+the informal presentation given in Heuser's textbook \cite[{\S} 36]{Heuser:1986}.
+Another formal proof of the same theorem has been done in Mizar
+\cite{Nowak:1993}. A general overview of the relevance and history of the
+Hahn-Banach Theorem is given by Narici and Beckenstein \cite{Narici:1996}.
+
+\medskip The document is structured as follows. The first part contains
+definitions of basic notions of linear algebra: vector spaces, subspaces,
+normed spaces, continuous linear-forms, norm of functions and an order on
+functions by domain extension. The second part contains some lemmas about the
+supremum (w.r.t.\ the function order) and extension of non-maximal functions.
+With these preliminaries, the main proof of the theorem (in its two versions)
+is conducted in the third part. The dependencies of individual theories are
+as follows.
+
+\begin{center}
+ \includegraphics[scale=0.5]{session_graph}
+\end{center}
+
+\clearpage
+\part {Basic Notions}
+
+\input{Bounds}
+\input{Vector_Space}
+\input{Subspace}
+\input{Normed_Space}
+\input{Linearform}
+\input{Function_Order}
+\input{Function_Norm}
+\input{Zorn_Lemma}
+
+\clearpage
+\part {Lemmas for the Proof}
+
+\input{Hahn_Banach_Sup_Lemmas}
+\input{Hahn_Banach_Ext_Lemmas}
+\input{Hahn_Banach_Lemmas}
+
+\clearpage
+\part {The Main Proof}
+
+\input{Hahn_Banach}
+\bibliographystyle{abbrv}
+\bibliography{root}
+
+\end{document}
--- a/src/HOL/IsaMakefile Wed Jun 24 21:28:02 2009 +0200
+++ b/src/HOL/IsaMakefile Wed Jun 24 21:46:54 2009 +0200
@@ -16,7 +16,7 @@
HOL-Bali \
HOL-Decision_Procs \
HOL-Extraction \
- HOL-HahnBanach \
+ HOL-Hahn_Banach \
HOL-Hoare \
HOL-HoareParallel \
HOL-Import \
@@ -360,21 +360,19 @@
@cd Library; $(ISABELLE_TOOL) usedir $(OUT)/HOL Library
-## HOL-HahnBanach
+## HOL-Hahn_Banach
-HOL-HahnBanach: HOL $(LOG)/HOL-HahnBanach.gz
+HOL-Hahn_Banach: HOL $(LOG)/HOL-Hahn_Banach.gz
-$(LOG)/HOL-HahnBanach.gz: $(OUT)/HOL \
- HahnBanach/Bounds.thy HahnBanach/FunctionNorm.thy \
- HahnBanach/FunctionOrder.thy HahnBanach/HahnBanach.thy \
- HahnBanach/HahnBanachExtLemmas.thy \
- HahnBanach/HahnBanachSupLemmas.thy \
- HahnBanach/Linearform.thy HahnBanach/NormedSpace.thy \
- HahnBanach/README.html HahnBanach/ROOT.ML \
- HahnBanach/Subspace.thy HahnBanach/VectorSpace.thy \
- HahnBanach/ZornLemma.thy HahnBanach/document/root.bib \
- HahnBanach/document/root.tex
- @$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL HahnBanach
+$(LOG)/HOL-Hahn_Banach.gz: $(OUT)/HOL Hahn_Banach/Bounds.thy \
+ Hahn_Banach/Function_Norm.thy Hahn_Banach/Function_Order.thy \
+ Hahn_Banach/Hahn_Banach.thy Hahn_Banach/Hahn_Banach_Ext_Lemmas.thy \
+ Hahn_Banach/Hahn_Banach_Sup_Lemmas.thy Hahn_Banach/Linearform.thy \
+ Hahn_Banach/Normed_Space.thy Hahn_Banach/README.html \
+ Hahn_Banach/ROOT.ML Hahn_Banach/Subspace.thy \
+ Hahn_Banach/Vector_Space.thy Hahn_Banach/Zorn_Lemma.thy \
+ Hahn_Banach/document/root.bib Hahn_Banach/document/root.tex
+ @$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL Hahn_Banach
## HOL-Subst
@@ -1138,7 +1136,7 @@
$(LOG)/HOL-MicroJava.gz $(LOG)/HOL-NanoJava.gz \
$(LOG)/HOL-Nominal-Examples.gz $(LOG)/HOL-IOA.gz \
$(LOG)/HOL-Lattice $(LOG)/HOL-Matrix \
- $(LOG)/HOL-HahnBanach.gz $(LOG)/HOL-SET-Protocol.gz \
+ $(LOG)/HOL-Hahn_Banach.gz $(LOG)/HOL-SET-Protocol.gz \
$(LOG)/TLA-Inc.gz $(LOG)/TLA-Buffer.gz \
$(LOG)/TLA-Memory.gz $(LOG)/HOL-Library.gz \
$(LOG)/HOL-Unix.gz $(OUT)/HOL-Word $(LOG)/HOL-Word.gz \
--- a/src/HOL/README.html Wed Jun 24 21:28:02 2009 +0200
+++ b/src/HOL/README.html Wed Jun 24 21:46:54 2009 +0200
@@ -96,7 +96,7 @@
<dt>Real
<dd>the real numbers, part of Complex
-<dt>Real/HahnBanach
+<dt>Hahn_Banach
<dd>the Hahn-Banach theorem for real vector spaces (in Isabelle/Isar)
<dt>SET-Protocol