summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | wenzelm |

Wed, 24 Jun 2009 21:46:54 +0200 | |

changeset 31795 | be3e1cc5005c |

parent 31794 | 71af1fd6a5e4 |

child 31796 | 117300d72398 |

child 31799 | 294b955d0e80 |

standard naming conventions for session and theories;

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