--- a/src/HOL/Real/HahnBanach/Aux.thy Fri Oct 29 19:24:20 1999 +0200
+++ b/src/HOL/Real/HahnBanach/Aux.thy Fri Oct 29 20:18:34 1999 +0200
@@ -15,7 +15,7 @@
lemmas chainE2 = chainD2 [elimify];
text_raw {* \medskip *};
-text{* Lemmas about sets: *};
+text{* Lemmas about sets. *};
lemma Int_singletonD: "[| A Int B = {v}; x:A; x:B |] ==> x = v";
by (fast elim: equalityE);
@@ -24,7 +24,7 @@
by (force simp add: psubset_eq);
text_raw {* \medskip *};
-text{* Some lemmas about orders: *};
+text{* Some lemmas about orders. *};
lemma lt_imp_not_eq: "x < (y::'a::order) ==> x ~= y";
by (rule order_less_le[RS iffD1, RS conjunct2]);
--- a/src/HOL/Real/HahnBanach/Bounds.thy Fri Oct 29 19:24:20 1999 +0200
+++ b/src/HOL/Real/HahnBanach/Bounds.thy Fri Oct 29 20:18:34 1999 +0200
@@ -71,10 +71,12 @@
text_raw {* \end{comment} *};
-text {* A supremum of an ordered set $B$ w.~r.~t.~$A$
-is defined as a least upperbound of $B$, which lies in $A$.
-The definition of the supremum is based on the
-existing definition (see HOL/Real/Lubs.thy).*};
+text {*
+ A supremum\footnote{The definition of the supremum is based on one in
+ \url{http://isabelle.in.tum.de/library/HOL/HOL-Real/Lubs.html}} of
+ an ordered set $B$ w.~r.~t.~$A$ is defined as a least upper bound of
+ $B$, which lies in $A$.
+*};
text{* If a supremum exists, then $\idt{Sup}\ap A\ap B$
is equal to the supremum. *};
@@ -114,13 +116,13 @@
text_raw {* \end{comment} *};
;
-text{* The supremum of $B$ is less than every upper bound
+text{* The supremum of $B$ is less than any upper bound
of $B$.*};
lemma sup_le_ub: "isUb A B y ==> is_Sup A B s ==> s <= y";
by (unfold is_Sup_def, rule isLub_le_isUb);
-text {* The supremum $B$ is an upperbound for $B$. *};
+text {* The supremum $B$ is an upper bound for $B$. *};
lemma sup_ub: "y:B ==> is_Sup A B s ==> y <= s";
by (unfold is_Sup_def, rule isLubD2);
--- a/src/HOL/Real/HahnBanach/FunctionNorm.thy Fri Oct 29 19:24:20 1999 +0200
+++ b/src/HOL/Real/HahnBanach/FunctionNorm.thy Fri Oct 29 20:18:34 1999 +0200
@@ -7,110 +7,113 @@
theory FunctionNorm = NormedSpace + FunctionOrder:;
-subsection {* Continous linearforms*};
+subsection {* Continuous linear forms*};
-text{* A linearform $f$ on a normed vector space $(V, \norm{\cdot})$
-is \emph{continous}, iff it is bounded, i.~e.
-\[\exists\ap c\in R.\ap \forall\ap x\in V.\ap
-|f\ap x| \leq c \cdot \norm x\]
-In our application no other functions than linearforms are considered,
-so we can define continous linearforms as follows:
+text{* A linear form $f$ on a normed vector space $(V, \norm{\cdot})$
+is \emph{continuous}, iff it is bounded, i.~e.
+\[\Ex {c\in R}{\All {x\in V} {|f\ap x| \leq c \cdot \norm x}}\]
+In our application no other functions than linear forms are considered,
+so we can define continuous linear forms as bounded linear forms:
*};
constdefs
- is_continous ::
+ is_continuous ::
"['a::{minus, plus} set, 'a => real, 'a => real] => bool"
- "is_continous V norm f ==
+ "is_continuous V norm f ==
is_linearform V f & (EX c. ALL x:V. rabs (f x) <= c * norm x)";
-lemma continousI [intro]:
+lemma continuousI [intro]:
"[| is_linearform V f; !! x. x:V ==> rabs (f x) <= c * norm x |]
- ==> is_continous V norm f";
-proof (unfold is_continous_def, intro exI conjI ballI);
+ ==> is_continuous V norm f";
+proof (unfold is_continuous_def, intro exI conjI ballI);
assume r: "!! x. x:V ==> rabs (f x) <= c * norm x";
fix x; assume "x:V"; show "rabs (f x) <= c * norm x"; by (rule r);
qed;
-lemma continous_linearform [intro!!]:
- "is_continous V norm f ==> is_linearform V f";
- by (unfold is_continous_def) force;
+lemma continuous_linearform [intro!!]:
+ "is_continuous V norm f ==> is_linearform V f";
+ by (unfold is_continuous_def) force;
-lemma continous_bounded [intro!!]:
- "is_continous V norm f
+lemma continuous_bounded [intro!!]:
+ "is_continuous V norm f
==> EX c. ALL x:V. rabs (f x) <= c * norm x";
- by (unfold is_continous_def) force;
+ by (unfold is_continuous_def) force;
-subsection{* The norm of a linearform *};
+subsection{* The norm of a linear form *};
text{* The least real number $c$ for which holds
-\[\forall\ap x\in V.\ap |f\ap x| \leq c \cdot \norm x\]
+\[\All {x\in V}{|f\ap x| \leq c \cdot \norm x}\]
is called the \emph{norm} of $f$.
-For the non-trivial vector space $V$ the norm can be defined as
+For non-trivial vector spaces $V \neq \{\zero\}$ the norm can be defined as
\[\fnorm {f} =\sup_{x\neq\zero}\frac{|f\ap x|}{\norm x} \]
-For the case that the vector space $V$ contains only the $\zero$
-vector, the set $B$ this supremum is taken from would be empty, and
-any real number is a supremum of $B$. So it must be guarateed that
-there is an element in $B$. This element must be ${} \ge 0$ so that
+For the case $V = \{\zero\}$ the supremum would be taken from an
+empty set. Since $\bbbR$ 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 ${} \ge 0$ so that
$\idt{function{\dsh}norm}$ has the norm properties. Furthermore it
does not have to change the norm in all other cases, so it must be
-$0$, as all other elements of $B$ are ${} \ge 0$.
+$0$, as all other elements of are ${} \ge 0$.
-Thus $B$ is defined as follows.
+Thus we define the set $B$ the supremum is taken from as
+\[
+\{ 0 \} \Un \left\{ \frac{|f\ap x|}{\norm x} \dt x\neq \zero \And x\in F\right\}
+ \]
*};
constdefs
B :: "[ 'a set, 'a => real, 'a => real ] => real set"
"B V norm f ==
- {z. z = 0r | (EX x:V. x ~= <0> & z = rabs (f x) * rinv (norm x))}";
-
-text{* $\idt{function{\dsh}norm}$ is equal to the supremum of $B$,
-if there exists a supremum. *};
+ {0r} \Un {rabs (f x) * rinv (norm x) | x. x ~= <0> & x:V}";
-constdefs
- function_norm :: " ['a set, 'a => real, 'a => real] => real"
- "function_norm V norm f == Sup UNIV (B V norm f)";
-
-text{* $\idt{is{\dsh}function{\dsh}norm}$ also guarantees that there
-is a funciton norm .*};
+text{* $n$ is the function norm of $f$, iff
+$n$ is the supremum of $B$.
+*};
constdefs
is_function_norm ::
" ['a set, 'a => real, 'a => real] => real => bool"
"is_function_norm V norm f fn == is_Sup UNIV (B V norm f) fn";
+text{* $\idt{function{\dsh}norm}$ is equal to the supremum of $B$,
+if the supremum exists. Otherwise it is undefined. *};
+
+constdefs
+ function_norm :: " ['a set, 'a => real, 'a => real] => real"
+ "function_norm V norm f == Sup UNIV (B V norm f)";
+
lemma B_not_empty: "0r : B V norm f";
by (unfold B_def, force);
-text {* The following lemma states every continous linearform on a
-normed space $(V, \norm{\cdot})$ has a function norm. *};
+text {* The following lemma states that every continuous linear form
+on a normed space $(V, \norm{\cdot})$ has a function norm. *};
lemma ex_fnorm [intro!!]:
- "[| is_normed_vectorspace V norm; is_continous V norm f|]
+ "[| is_normed_vectorspace V norm; is_continuous V norm f|]
==> is_function_norm V norm f (function_norm V norm f)";
proof (unfold function_norm_def is_function_norm_def
- is_continous_def Sup_def, elim conjE, rule selectI2EX);
+ is_continuous_def Sup_def, elim conjE, rule selectI2EX);
assume "is_normed_vectorspace V norm";
assume "is_linearform V f"
and e: "EX c. ALL x:V. rabs (f x) <= c * norm x";
txt {* The existence of the supremum is shown using the
completeness of the reals. Completeness means, that
- for every non-empty and bounded set of reals there exists a
+ every non-empty bounded set of reals has a
supremum. *};
show "EX a. is_Sup UNIV (B V norm f) a";
proof (unfold is_Sup_def, rule reals_complete);
- txt {* First we have to show that $B$ is non-empty. *};
+ txt {* First we have to show that $B$ is non-empty: *};
show "EX X. X : B V norm f";
proof (intro exI);
show "0r : (B V norm f)"; by (unfold B_def, force);
qed;
- txt {* Then we have to show that $B$ is bounded. *};
+ txt {* Then we have to show that $B$ is bounded: *};
from e; show "EX Y. isUb UNIV (B V norm f) Y";
proof;
@@ -122,19 +125,18 @@
show "?thesis";
proof (intro exI isUbI setleI ballI, unfold B_def,
- elim CollectE disjE bexE conjE);
+ elim UnE CollectE exE conjE singletonE);
txt{* To proof the thesis, we have to show that there is
- some constant b, which is greater than every $y$ in $B$.
+ some constant $b$, such that $y \leq b$ for all $y\in B$.
Due to the definition of $B$ there are two cases for
- $y\in B$. If $y = 0$ then $y$ is less than
- $\idt{max}\ap c\ap 0$: *};
+ $y\in B$. If $y = 0$ then $y \leq idt{max}\ap c\ap 0$: *};
fix y; assume "y = 0r";
show "y <= b"; by (simp! add: le_max2);
txt{* The second case is
- $y = \frac{|f\ap x|}{\norm x}$ for some
+ $y = {|f\ap x|}/{\norm x}$ for some
$x\in V$ with $x \neq \zero$. *};
next;
@@ -186,13 +188,13 @@
qed;
qed;
-text {* The norm of a continous function is always $\geq 0$. *};
+text {* The norm of a continuous function is always $\geq 0$. *};
lemma fnorm_ge_zero [intro!!]:
- "[| is_continous V norm f; is_normed_vectorspace V norm|]
+ "[| is_continuous V norm f; is_normed_vectorspace V norm|]
==> 0r <= function_norm V norm f";
proof -;
- assume c: "is_continous V norm f"
+ assume c: "is_continuous V norm f"
and n: "is_normed_vectorspace V norm";
txt {* The function norm is defined as the supremum of $B$.
@@ -202,9 +204,9 @@
show ?thesis;
proof (unfold function_norm_def, rule sup_ub1);
show "ALL x:(B V norm f). 0r <= x";
- proof (intro ballI, unfold B_def,
- elim CollectE bexE conjE disjE);
- fix x r;
+ proof (intro ballI, unfold B_def,
+ elim UnE singletonE CollectE exE conjE);
+ fix x r;
assume "x : V" "x ~= <0>"
and r: "r = rabs (f x) * rinv (norm x)";
@@ -218,33 +220,33 @@
qed;
qed; ***)
with ge; show "0r <= r";
- by (simp only: r,rule real_le_mult_order);
+ by (simp only: r, rule real_le_mult_order);
qed (simp!);
- txt {* Since $f$ is continous the function norm exists. *};
+ txt {* Since $f$ is continuous the function norm exists: *};
have "is_function_norm V norm f (function_norm V norm f)"; ..;
thus "is_Sup UNIV (B V norm f) (Sup UNIV (B V norm f))";
- by (unfold is_function_norm_def, unfold function_norm_def);
+ by (unfold is_function_norm_def function_norm_def);
- txt {* $B$ is non-empty by construction. *};
+ txt {* $B$ is non-empty by construction: *};
show "0r : B V norm f"; by (rule B_not_empty);
qed;
qed;
-text{* The basic property of function norms is:
+text{* \medskip The fundamental property of function norms is:
\begin{matharray}{l}
| f\ap x | \leq {\fnorm {f}} \cdot {\norm x}
\end{matharray}
*};
lemma norm_fx_le_norm_f_norm_x:
- "[| is_normed_vectorspace V norm; x:V; is_continous V norm f |]
- ==> rabs (f x) <= (function_norm V norm f) * norm x";
+ "[| is_normed_vectorspace V norm; x:V; is_continuous V norm f |]
+ ==> rabs (f x) <= function_norm V norm f * norm x";
proof -;
assume "is_normed_vectorspace V norm" "x:V"
- and c: "is_continous V norm f";
+ and c: "is_continuous V norm f";
have v: "is_vectorspace V"; ..;
assume "x:V";
@@ -259,7 +261,7 @@
assume "x = <0>";
have "rabs (f x) = rabs (f <0>)"; by (simp!);
- also; from v continous_linearform; have "f <0> = 0r"; ..;
+ also; from v continuous_linearform; have "f <0> = 0r"; ..;
also; note rabs_zero;
also; have "0r <= function_norm V norm f * norm x";
proof (rule real_le_mult_order);
@@ -286,11 +288,11 @@
show "is_Sup UNIV (B V norm f) (Sup UNIV (B V norm f))";
by (simp! add: is_function_norm_def function_norm_def);
show "rabs (f x) * rinv (norm x) : B V norm f";
- by (unfold B_def, intro CollectI disjI2 bexI [of _ x]
+ by (unfold B_def, intro UnI2 CollectI exI [of _ x]
conjI, simp);
qed;
- txt {* The thesis follows by a short calculation: *};
+ txt {* The thesis now follows by a short calculation: *};
have "rabs (f x) = rabs (f x) * 1r"; by (simp!);
also; from nz; have "1r = rinv (norm x) * norm x";
@@ -305,21 +307,20 @@
qed;
qed;
-text{* The function norm is the least positive real number for
-which the inequation
+text{* \medskip The function norm is the least positive real number for
+which the following inequation holds:
\begin{matharray}{l}
| f\ap x | \leq c \cdot {\norm x}
\end{matharray}
-holds.
*};
lemma fnorm_le_ub:
- "[| is_normed_vectorspace V norm; is_continous V norm f;
+ "[| is_normed_vectorspace V norm; is_continuous V norm f;
ALL x:V. rabs (f x) <= c * norm x; 0r <= c |]
==> function_norm V norm f <= c";
proof (unfold function_norm_def);
assume "is_normed_vectorspace V norm";
- assume c: "is_continous V norm f";
+ assume c: "is_continuous V norm f";
assume fb: "ALL x:V. rabs (f x) <= c * norm x"
and "0r <= c";
@@ -342,7 +343,7 @@
proof (intro isUbI setleI ballI);
fix y; assume "y: B V norm f";
thus le: "y <= c";
- proof (unfold B_def, elim CollectE disjE bexE conjE);
+ proof (unfold B_def, elim UnE CollectE exE conjE singletonE);
txt {* The first case for $y\in B$ is $y=0$. *};
@@ -350,7 +351,7 @@
show "y <= c"; by (force!);
txt{* The second case is
- $y = \frac{|f\ap x|}{\norm x}$ for some
+ $y = {|f\ap x|}/{\norm x}$ for some
$x\in V$ with $x \neq \zero$. *};
next;
--- a/src/HOL/Real/HahnBanach/FunctionOrder.thy Fri Oct 29 19:24:20 1999 +0200
+++ b/src/HOL/Real/HahnBanach/FunctionOrder.thy Fri Oct 29 20:18:34 1999 +0200
@@ -3,29 +3,26 @@
Author: Gertrud Bauer, TU Munich
*)
-header {* An Order on functions *};
+header {* An order on functions *};
theory FunctionOrder = Subspace + Linearform:;
-
subsection {* The graph of a function *};
-text{* We define the \emph{graph} of a (real) function $f$ with the
+text{* We define the \emph{graph} of a (real) function $f$ with
domain $F$ as the set
\[
\{(x, f\ap x). \ap x:F\}
\]
-So we are modelling partial functions by specifying the domain and
-the mapping function. We use the notion ``function'' also for the graph
-of a function.
+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::{minus, plus} * real) set";
+types 'a graph = "('a * real) set";
constdefs
graph :: "['a set, 'a => real] => 'a graph "
- "graph F f == {p. EX x. p = (x, f x) & x:F}"; (*
- == {(x, f x). x:F} *)
+ "graph F f == {(x, f x) | x. x:F}";
lemma graphI [intro!!]: "x:F ==> (x, f x) : graph F f";
by (unfold graph_def, intro CollectI exI) force;
@@ -41,7 +38,7 @@
subsection {* Functions ordered by domain extension *};
-text{* The function $h'$ is an extension of $h$, iff the graph of
+text{* A function $h'$ is an extension of $h$, iff the graph of
$h$ is a subset of the graph of $h'$.*};
lemma graph_extI:
@@ -83,7 +80,7 @@
lemma graph_domain_funct:
"(!!x y z. (x, y):g ==> (x, z):g ==> z = y)
==> graph (domain g) (funct g) = g";
-proof (unfold domain_def, unfold funct_def, unfold graph_def, auto);
+proof (unfold domain_def funct_def graph_def, auto);
fix a b; assume "(a, b) : g";
show "(a, SOME y. (a, y) : g) : g"; by (rule selectI2);
show "EX y. (a, y) : g"; ..;
@@ -96,9 +93,9 @@
-subsection {* Norm preserving extensions of a function *};
+subsection {* Norm-preserving extensions of a function *};
-text {* Given a function $f$ on the space $F$ and a quasinorm $p$ on
+text {* Given a linear form $f$ on the space $F$ and a seminorm $p$ on
$E$. The set of all linear extensions of $f$, to superspaces $H$ of
$F$, which are bounded by $p$, is defined as follows. *};
--- a/src/HOL/Real/HahnBanach/HahnBanach.thy Fri Oct 29 19:24:20 1999 +0200
+++ b/src/HOL/Real/HahnBanach/HahnBanach.thy Fri Oct 29 20:18:34 1999 +0200
@@ -1,6 +1,6 @@
(* Title: HOL/Real/HahnBanach/HahnBanach.thy
ID: $Id$
- Author: Gertrud Baueer, TU Munich
+ Author: Gertrud Bauer, TU Munich
*)
header {* The Hahn-Banach Theorem *};
@@ -15,18 +15,19 @@
subsection {* The case of general linear spaces *};
-text {* Every linearform $f$ on a subspace $F$ of $E$, which is
- bounded by some quasinorm $q$ on $E$, can be extended
- to a function on $E$ in a norm preseving way. *};
+text {* Let $f$ be a linear form $f$ defined on a subspace $F$
+ of a norm vector space $E$. If $f$ is
+ bounded by some seminorm $q$ on $E$, it can be extended
+ to a function on $E$ in a norm-preserving way. *};
theorem HahnBanach:
- "[| is_vectorspace E; is_subspace F E; is_quasinorm E p;
+ "[| is_vectorspace E; is_subspace F E; is_seminorm E p;
is_linearform F f; ALL x:F. f x <= p x |]
==> EX h. is_linearform E h
& (ALL x:F. h x = f x)
& (ALL x:E. h x <= p x)";
proof -;
- assume "is_vectorspace E" "is_subspace F E" "is_quasinorm E p"
+ assume "is_vectorspace E" "is_subspace F E" "is_seminorm E p"
"is_linearform F f" "ALL x:F. f x <= p x";
txt{* We define $M$ to be the set of all linear extensions
@@ -42,19 +43,18 @@
thus "is_subspace F F"; ..;
qed (blast!)+;
- subsubsect {* Existence of a limit function of the norm preserving
+ subsubsect {* Existence of a limit function the norm-preserving
extensions *};
- txt {* For every non-empty chain of norm preserving functions
- the union of all functions in the chain is again a norm preserving
- function. (The union is an upper bound for all elements.
+ txt {* For every non-empty chain of norm-preserving extensions
+ the union of all functions in the chain is again a norm-preserving
+ extension. (The union is an upper bound for all elements.
It is even the least upper bound, because every upper bound of $M$
is also an upper bound for $\Union c$.) *};
- have "!! c. [| c : chain M; EX x. x:c |] ==> Union c : M";
- proof -;
+ {{;
fix c; assume "c:chain M" "EX x. x:c";
- show "Union c : M";
+ have "Union c : M";
proof (unfold M_def, rule norm_pres_extensionI);
show "EX (H::'a set) h::'a => real. graph H h = Union c
@@ -67,29 +67,25 @@
let ?H = "domain (Union c)";
let ?h = "funct (Union c)";
- show a [simp]: "graph ?H ?h = Union c";
+ show a: "graph ?H ?h = Union c";
proof (rule graph_domain_funct);
fix x y z; assume "(x, y) : Union c" "(x, z) : Union c";
show "z = y"; by (rule sup_definite);
qed;
- show "is_linearform ?H ?h";
+ show "is_linearform ?H ?h";
by (simp! add: sup_lf a);
-
show "is_subspace ?H E";
by (rule sup_subE, rule a) (simp!)+;
-
show "is_subspace F ?H";
by (rule sup_supF, rule a) (simp!)+;
-
show "graph F f <= graph ?H ?h";
by (rule sup_ext, rule a) (simp!)+;
-
show "ALL x::'a:?H. ?h x <= p x";
by (rule sup_norm_pres, rule a) (simp!)+;
qed;
qed;
- qed;
+ }};
txt {* According to Zorn's Lemma there is
a maximal norm-preserving extension $g\in M$. *};
@@ -120,19 +116,18 @@
have h: "is_vectorspace H"; ..;
have f: "is_vectorspace F"; ..;
-subsubsect {* The domain of the limit function. *};
+subsubsect {* The domain of the limit function *};
have eq: "H = E";
proof (rule classical);
-txt {* Assume the domain of the supremum is not $E$. *};
+txt {* Assume that the domain of the supremum is not $E$, *};
;
assume "H ~= E";
have "H <= E"; ..;
hence "H < E"; ..;
- txt{* Then there exists an element $x_0$ in
- the difference of $E$ and $H$. *};
+ txt{* then there exists an element $x_0$ in $E \ H$: *};
hence "EX x0:E. x0~:H";
by (rule set_less_imp_diff_not_empty);
@@ -153,16 +148,16 @@
qed blast;
txt {* Define $H_0$ as the (direct) sum of H and the
- linear closure of $x_0$.*};
+ linear closure of $x_0$. \label{ex-xi-use}*};
def H0 == "H + lin x0";
- from h; have xi: "EX xi. (ALL y:H. - p (y + x0) - h y <= xi)
- & (ALL y:H. xi <= p (y + x0) - h y)";
+ from h; have xi: "EX xi. ALL y:H. - p (y + x0) - h y <= xi
+ & xi <= p (y + x0) - h y";
proof (rule ex_xi);
fix u v; assume "u:H" "v:H";
from h; have "h v - h u = h (v - u)";
- by (simp! add: linearform_diff_linear);
+ by (simp! add: linearform_diff);
also; from h_bound; have "... <= p (v - u)";
by (simp!);
also; have "v - u = x0 + - x0 + v + - u";
@@ -172,7 +167,7 @@
also; have "... = (v + x0) - (u + x0)";
by (simp! add: diff_eq1);
also; have "p ... <= p (v + x0) + p (u + x0)";
- by (rule quasinorm_diff_triangle_ineq) (simp!)+;
+ by (rule seminorm_diff_subadditive) (simp!)+;
finally; have "h v - h u <= p (v + x0) + p (u + x0)"; .;
thus "- p (u + x0) - h u <= p (v + x0) - h v";
@@ -182,13 +177,14 @@
& graph H0 h0 : M";
proof (elim exE, intro exI conjI);
fix xi;
- assume a: "(ALL y:H. - p (y + x0) - h y <= xi)
- & (ALL y:H. xi <= p (y + x0) - h y)";
+ assume a: "ALL y:H. - p (y + x0) - h y <= xi
+ & xi <= p (y + x0) - h y";
- txt {* Define $h_0$ as the linear extension of $h$ on $H_0$:*};
+ txt {* Define $h_0$ as the canonical linear extension
+ of $h$ on $H_0$:*};
def h0 ==
- "\<lambda>x. let (y,a) = SOME (y, a). (x = y + a <*> x0 & y:H)
+ "\<lambda>x. let (y,a) = SOME (y, a). x = y + a <*> x0 & y:H
in (h y) + a * xi";
txt {* We get that the graph of $h_0$ extend that of
@@ -230,15 +226,13 @@
qed;
thus "g ~= graph H0 h0"; by (simp!);
- txt {* Furthermore $h_0$ is a norm preserving extension
+ txt {* Furthermore $h_0$ is a norm-preserving extension
of $f$. *};
have "graph H0 h0 : norm_pres_extensions E p F f";
proof (rule norm_pres_extensionI2);
-
show "is_linearform H0 h0";
by (rule h0_lf, rule x0) (simp!)+;
-
show "is_subspace H0 E";
by (unfold H0_def, rule vs_sum_subspace,
rule lin_subspace);
@@ -314,23 +308,24 @@
subsection {* An alternative formulation of the theorem *};
-text {* The following alternative formulation of the
-Hahn-Banach Theorem uses the fact that for
-real numbers the following inequations are equivalent:
+text {* The following alternative formulation of the Hahn-Banach
+Theorem\label{rabs-HahnBanach} uses the fact that for real numbers the
+following inequations are equivalent:\footnote{This was shown in lemma
+$\idt{rabs{\dsh}ineq{\dsh}iff}$ (see page \pageref{rabs-ineq-iff}).}
\begin{matharray}{ll}
\forall x\in H.\ap |h\ap x|\leq p\ap x& {\rm and}\\
\forall x\in H.\ap h\ap x\leq p\ap x\\
\end{matharray}
-(This was shown in lemma $\idt{rabs{\dsh}ineq}$.) *};
+*};
theorem rabs_HahnBanach:
- "[| is_vectorspace E; is_subspace F E; is_quasinorm E p;
+ "[| is_vectorspace E; is_subspace F E; is_seminorm E p;
is_linearform F f; ALL x:F. rabs (f x) <= p x |]
==> EX g. is_linearform E g
& (ALL x:F. g x = f x)
& (ALL x:E. rabs (g x) <= p x)";
proof -;
- assume e: "is_vectorspace E" "is_subspace F E" "is_quasinorm E p"
+ assume e: "is_vectorspace E" "is_subspace F E" "is_seminorm E p"
"is_linearform F f" "ALL x:F. rabs (f x) <= p x";
have "ALL x:F. f x <= p x";
by (rule rabs_ineq_iff [RS iffD1]);
@@ -352,36 +347,35 @@
subsection {* The Hahn-Banach Theorem for normed spaces *};
-text {* Every continous linear function $f$ on a subspace of $E$,
- can be extended to a continous function on $E$ with the same
- function norm. *};
+text {* Every continuous linear form $f$ on a subspace $F$ of a
+norm space $E$, can be extended to a continuous linear form $g$ on
+$E$ such that $\fnorm{f} = \fnorm {g}$. *};
theorem norm_HahnBanach:
"[| is_normed_vectorspace E norm; is_subspace F E;
- is_linearform F f; is_continous F norm f |]
+ is_linearform F f; is_continuous F norm f |]
==> EX g. is_linearform E g
- & is_continous E norm g
+ & is_continuous E norm g
& (ALL x:F. g x = f x)
& function_norm E norm g = function_norm F norm f";
proof -;
assume e_norm: "is_normed_vectorspace E norm";
assume f: "is_subspace F E" "is_linearform F f";
- assume f_cont: "is_continous F norm f";
+ assume f_cont: "is_continuous F norm f";
have e: "is_vectorspace E"; ..;
with _; have f_norm: "is_normed_vectorspace F norm"; ..;
txt{* We define the function $p$ on $E$ as follows:
\begin{matharray}{l}
- p\ap x = \fnorm f \cdot \norm x\\
- % p\ap x = \fnorm f \cdot \fnorm x\\
+ p \ap x = \fnorm f \cdot \norm x\\
\end{matharray}
*};
def p == "\<lambda>x. function_norm F norm f * norm x";
- txt{* $p$ is a quasinorm on $E$: *};
+ txt{* $p$ is a seminorm on $E$: *};
- have q: "is_quasinorm E p";
+ have q: "is_seminorm E p";
proof;
fix x y a; assume "x:E" "y:E";
@@ -393,14 +387,14 @@
show "0r <= norm x"; ..;
qed;
- txt{* $p$ is multiplicative: *};
+ txt{* $p$ is absolutely homogenous: *};
show "p (a <*> x) = rabs a * p x";
proof -;
have "p (a <*> x) = function_norm F norm f * norm (a <*> x)";
by (simp!);
also; have "norm (a <*> x) = rabs a * norm x";
- by (rule normed_vs_norm_mult_distrib);
+ by (rule normed_vs_norm_rabs_homogenous);
also; have "function_norm F norm f * (rabs a * norm x)
= rabs a * (function_norm F norm f * norm x)";
by (simp! only: real_mult_left_commute);
@@ -408,7 +402,7 @@
finally; show ?thesis; .;
qed;
- txt{* Furthermore, $p$ obeys the triangle inequation: *};
+ txt{* Furthermore, $p$ is subadditive: *};
show "p (x + y) <= p x + p y";
proof -;
@@ -436,10 +430,10 @@
by (simp! add: norm_fx_le_norm_f_norm_x);
qed;
- txt{* Using the facts that $p$ is a quasinorm and
- $f$ is bounded we can apply the Hahn-Banach Theorem for real
- vector spaces.
- So $f$ can be extended in a norm preserving way to some function
+ txt{* Using the fact that $p$ is a seminorm and
+ $f$ is bounded by $q$ we can apply the Hahn-Banach Theorem
+ for real vector spaces.
+ So $f$ can be extended in a norm-preserving way to some function
$g$ on the whole vector space $E$. *};
with e f q;
@@ -451,36 +445,43 @@
proof (elim exE conjE);
fix g;
assume "is_linearform E g" and a: "ALL x:F. g x = f x"
- and "ALL x:E. rabs (g x) <= p x";
+ and b: "ALL x:E. rabs (g x) <= p x";
show "EX g. is_linearform E g
- & is_continous E norm g
+ & is_continuous E norm g
& (ALL x:F. g x = f x)
& function_norm E norm g = function_norm F norm f";
proof (intro exI conjI);
- txt{* To complete the proof, we show that this function
- $g$ is also continous and has the same function norm as
- $f$. *};
+ txt{* We futhermore have to show that
+ $g$ is also continuous: *};
- show g_cont: "is_continous E norm g";
+ show g_cont: "is_continuous E norm g";
proof;
fix x; assume "x:E";
+ from b [RS bspec, OF this];
show "rabs (g x) <= function_norm F norm f * norm x";
- by (rule bspec [of _ _ x], (simp!));
+ by (unfold p_def);
qed;
+ txt {* To complete the proof, we show that
+ $\fnorm g = \fnorm f$. *};
+
show "function_norm E norm g = function_norm F norm f"
(is "?L = ?R");
proof (rule order_antisym);
- txt{* $\idt{function{\dsh}norm}\ap F\ap \idt{norm}\ap f$ is
- a solution
- for the inequation
+ txt{* First we show $\fnorm g \leq \fnorm f$. The function norm
+ $\fnorm g$ is defined as the smallest $c\in\bbbR$ such that
\begin{matharray}{l}
- \forall\ap x\in E.\ap |g\ap x| \leq c \cdot \norm x
- \end{matharray} *};
-
+ \All {x\in E} {|g\ap x| \leq c \cdot \norm x}
+ \end{matharray}
+ Furthermore holds
+ \begin{matharray}{l}
+ \All {x\in E} {|g\ap x| \leq \fnorm f \cdot \norm x}
+ \end{matharray}
+ *};
+
have "ALL x:E. rabs (g x) <= function_norm F norm f * norm x";
proof;
fix x; assume "x:E";
@@ -488,12 +489,7 @@
by (simp!);
qed;
- txt{* Since
- $\idt{function{\dsh}norm}\ap E\ap \idt{norm}\ap g$
- is the smallest solution for this inequation, we have: *};
-
- with _ g_cont;
- show "?L <= ?R";
+ with _ g_cont; show "?L <= ?R";
proof (rule fnorm_le_ub);
from f_cont f_norm; show "0r <= function_norm F norm f"; ..;
qed;
--- a/src/HOL/Real/HahnBanach/HahnBanachExtLemmas.thy Fri Oct 29 19:24:20 1999 +0200
+++ b/src/HOL/Real/HahnBanach/HahnBanachExtLemmas.thy Fri Oct 29 20:18:34 1999 +0200
@@ -3,88 +3,89 @@
Author: Gertrud Bauer, TU Munich
*)
-header {* Extending a non-maximal function *};
+header {* Extending non-maximal functions *};
theory HahnBanachExtLemmas = FunctionNorm:;
text{* In this section the following context is presumed.
Let $E$ be a real vector space with a
-quasinorm $q$ on $E$. $F$ is a subspace of $E$ and $f$ a linear
+seminorm $q$ on $E$. $F$ is a subspace of $E$ and $f$ a linear
function on $F$. We consider a subspace $H$ of $E$ that is a
-superspace of $F$ and a linearform $h$ on $H$. $H$ is a not equal
+superspace of $F$ and a linear form $h$ on $H$. $H$ is a not equal
to $E$ and $x_0$ is an element in $E \backslash H$.
$H$ is extended to the direct sum $H_0 = H + \idt{lin}\ap x_0$, so for
any $x\in H_0$ the decomposition of $x = y + a \mult x$
with $y\in H$ is unique. $h_0$ is defined on $H_0$ by
-$h_0 x = h y + a \cdot \xi$ for some $\xi$.
+$h_0\ap x = h\ap y + a \cdot \xi$ for a certain $\xi$.
Subsequently we show some properties of this extension $h_0$ of $h$.
*};
-text {* This lemma will be used to show the existence of a linear
-extension of $f$. It is a conclusion of the completenesss of the
-reals. To show
+text {* This lemma will be used to show the existence of a linear
+extension of $f$ (see page \pageref{ex-xi-use}).
+It is a consequence
+of the completeness of $\bbbR$. To show
\begin{matharray}{l}
-\exists \xi. \ap (\forall y\in F.\ap a\ap y \leq \xi) \land (\forall y\in F.\ap xi \leq b\ap y)
-\end{matharray}
+\Ex{\xi}{\All {y\in F}{a\ap y \leq \xi \land \xi \leq b\ap y}}
+\end{matharray}
it suffices to show that
-\begin{matharray}{l}
-\forall u\in F. \ap\forall v\in F. \ap a\ap u \leq b \ap v
-\end{matharray}
-*};
+\begin{matharray}{l} \All
+{u\in F}{\All {v\in F}{a\ap u \leq b \ap v}}
+\end{matharray} *};
lemma ex_xi:
"[| is_vectorspace F; !! u v. [| u:F; v:F |] ==> a u <= b v |]
- ==> EX (xi::real). (ALL y:F. a y <= xi) & (ALL y:F. xi <= b y)";
+ ==> EX (xi::real). ALL y:F. a y <= xi & xi <= b y";
proof -;
assume vs: "is_vectorspace F";
assume r: "(!! u v. [| u:F; v:F |] ==> a u <= (b v::real))";
txt {* From the completeness of the reals follows:
The set $S = \{a\ap u.\ap u\in F\}$ has a supremum, if
- it is non-empty and if it has an upperbound. *};
+ it is non-empty and has an upper bound. *};
- let ?S = "{s::real. EX u:F. s = a u}";
+ let ?S = "{a u :: real | u. u:F}";
have "EX xi. isLub UNIV ?S xi";
proof (rule reals_complete);
- txt {* The set $S$ is non-empty, since $a\ap\zero \in S$ *};
+ txt {* The set $S$ is non-empty, since $a\ap\zero \in S$: *};
from vs; have "a <0> : ?S"; by force;
thus "EX X. X : ?S"; ..;
- txt {* $b\ap \zero$ is an upperboud of $S$. *};
+ txt {* $b\ap \zero$ is an upper bound of $S$: *};
show "EX Y. isUb UNIV ?S Y";
proof;
show "isUb UNIV ?S (b <0>)";
proof (intro isUbI setleI ballI);
+ show "b <0> : UNIV"; ..;
+ next;
- txt {* Every element $y\in S$ is less than $b\ap \zero$ *};
+ txt {* Every element $y\in S$ is less than $b\ap \zero$: *};
fix y; assume y: "y : ?S";
- from y; have "EX u:F. y = a u"; ..;
+ from y; have "EX u:F. y = a u"; by fast;
thus "y <= b <0>";
proof;
- fix u; assume "u:F"; assume "y = a u";
+ fix u; assume "u:F";
+ assume "y = a u";
also; have "a u <= b <0>"; by (rule r) (simp!)+;
finally; show ?thesis; .;
qed;
- next;
- show "b <0> : UNIV"; by simp;
qed;
qed;
qed;
- thus "EX xi. (ALL y:F. a y <= xi) & (ALL y:F. xi <= b y)";
+ thus "EX xi. ALL y:F. a y <= xi & xi <= b y";
proof (elim exE);
fix xi; assume "isLub UNIV ?S xi";
show ?thesis;
proof (intro exI conjI ballI);
- txt {* For all $y\in F$ holds $a\ap y \leq \xi$. *};
+ txt {* For all $y\in F$ holds $a\ap y \leq \xi$: *};
fix y; assume y: "y:F";
show "a y <= xi";
@@ -93,16 +94,16 @@
qed (force!);
next;
- txt {* For all $y\in F$ holds $\xi\leq b\ap y$. *};
+ txt {* For all $y\in F$ holds $\xi\leq b\ap y$: *};
fix y; assume "y:F";
show "xi <= b y";
proof (intro isLub_le_isUb isUbI setleI);
- show "b y : UNIV"; by simp;
+ show "b y : UNIV"; ..;
show "ALL ya : ?S. ya <= b y";
proof;
fix au; assume au: "au : ?S ";
- hence "EX u:F. au = a u"; ..;
+ hence "EX u:F. au = a u"; by fast;
thus "au <= b y";
proof;
fix u; assume "u:F"; assume "au = a u";
@@ -115,25 +116,26 @@
qed;
qed;
-text{* The function $h_0$ is defined as a canonical linear extension
-of $h$ to $H_0$. *};
+text{* The function $h_0$ is defined as a
+$h_0\ap x = h\ap y + a\cdot \xi$ where $x = y + a\prod \xi$
+is a linear extension of $h$ to $H_0$. *};
lemma h0_lf:
- "[| h0 = (\<lambda>x. let (y, a) = SOME (y, a). x = y + a <*> x0 & y:H
+ "[| h0 == (\<lambda>x. let (y, a) = SOME (y, a). x = y + a <*> x0 & y:H
in h y + a * xi);
- H0 = H + lin x0; is_subspace H E; is_linearform H h; x0 ~: H;
+ H0 == H + lin x0; is_subspace H E; is_linearform H h; x0 ~: H;
x0 : E; x0 ~= <0>; is_vectorspace E |]
==> is_linearform H0 h0";
proof -;
assume h0_def:
- "h0 = (\<lambda>x. let (y, a) = SOME (y, a). x = y + a <*> x0 & y:H
+ "h0 == (\<lambda>x. let (y, a) = SOME (y, a). x = y + a <*> x0 & y:H
in h y + a * xi)"
- and H0_def: "H0 = H + lin x0"
- and vs: "is_subspace H E" "is_linearform H h" "x0 ~: H"
- "x0 ~= <0>" "x0 : E" "is_vectorspace E";
+ and H0_def: "H0 == H + lin x0"
+ and vs: "is_subspace H E" "is_linearform H h" "x0 ~: H"
+ "x0 ~= <0>" "x0 : E" "is_vectorspace E";
have h0: "is_vectorspace H0";
- proof (simp only: H0_def, rule vs_sum_vs);
+ proof (unfold H0_def, rule vs_sum_vs);
show "is_subspace (lin x0) E"; ..;
qed;
@@ -141,8 +143,7 @@
proof;
fix x1 x2; assume x1: "x1 : H0" and x2: "x2 : H0";
- txt{* We now have to show that $h_0$ is linear
- w.~r.~t.~addition, i.~e.\
+ txt{* We now have to show that $h_0$ is additive, i.~e.\
$h_0 \ap (x_1\plus x_2) = h_0\ap x_1 + h_0\ap x_2$
for $x_1, x_2\in H$. *};
@@ -150,13 +151,13 @@
by (rule vs_add_closed, rule h0);
from x1;
have ex_x1: "EX y1 a1. x1 = y1 + a1 <*> x0 & y1 : H";
- by (simp add: H0_def vs_sum_def lin_def) blast;
+ by (unfold H0_def vs_sum_def lin_def) fast;
from x2;
have ex_x2: "EX y2 a2. x2 = y2 + a2 <*> x0 & y2 : H";
- by (simp add: H0_def vs_sum_def lin_def) blast;
+ by (unfold H0_def vs_sum_def lin_def) fast;
from x1x2;
have ex_x1x2: "EX y a. x1 + x2 = y + a <*> x0 & y : H";
- by (simp add: H0_def vs_sum_def lin_def) force;
+ by (unfold H0_def vs_sum_def lin_def) fast;
from ex_x1 ex_x2 ex_x1x2;
show "h0 (x1 + x2) = h0 x1 + h0 x2";
@@ -167,7 +168,7 @@
and y: "x1 + x2 = y + a <*> x0" and y': "y : H";
have ya: "y1 + y2 = y & a1 + a2 = a";
- proof (rule decomp_H0);
+ proof (rule decomp_H0); txt{*\label{decomp-H0-use}*};
show "y1 + y2 + (a1 + a2) <*> x0 = y + a <*> x0";
by (simp! add: vs_add_mult_distrib2 [of E]);
show "y1 + y2 : H"; ..;
@@ -179,7 +180,7 @@
by (simp add: ya);
also; from vs y1' y2';
have "... = h y1 + h y2 + a1 * xi + a2 * xi";
- by (simp add: linearform_add_linear [of H]
+ by (simp add: linearform_add [of H]
real_add_mult_distrib);
also; have "... = (h y1 + a1 * xi) + (h y2 + a2 * xi)";
by simp;
@@ -190,24 +191,23 @@
finally; show ?thesis; .;
qed;
- txt{* We further have to show that $h_0$ is linear
- w.~r.~t.~scalar multiplication,
+ txt{* We further have to show that $h_0$ is multiplicative,
i.~e.\ $h_0\ap (c \mult x_1) = c \cdot h_0\ap x_1$
- for $x\in H$ and any real number $c$.
+ for $x\in H$ and $c\in \bbbR$.
*};
next;
fix c x1; assume x1: "x1 : H0";
have ax1: "c <*> x1 : H0";
by (rule vs_mult_closed, rule h0);
- from x1; have ex_x1: "EX y1 a1. x1 = y1 + a1 <*> x0 & y1 : H";
- by (simp add: H0_def vs_sum_def lin_def) fast;
from x1; have ex_x: "!! x. x: H0
==> EX y a. x = y + a <*> x0 & y : H";
- by (simp add: H0_def vs_sum_def lin_def) fast;
- note ex_ax1 = ex_x [of "c <*> x1", OF ax1];
+ by (unfold H0_def vs_sum_def lin_def) fast;
- with ex_x1; show "h0 (c <*> x1) = c * (h0 x1)";
+ from x1; have ex_x1: "EX y1 a1. x1 = y1 + a1 <*> x0 & y1 : H";
+ by (unfold H0_def vs_sum_def lin_def) fast;
+ with ex_x [of "c <*> x1", OF ax1];
+ show "h0 (c <*> x1) = c * (h0 x1)";
proof (elim exE conjE);
fix y1 y a1 a;
assume y1: "x1 = y1 + a1 <*> x0" and y1': "y1 : H"
@@ -225,7 +225,7 @@
also; have "... = h (c <*> y1) + (c * a1) * xi";
by (simp add: ya);
also; from vs y1'; have "... = c * h y1 + c * a1 * xi";
- by (simp add: linearform_mult_linear [of H]);
+ by (simp add: linearform_mult [of H]);
also; from vs y1'; have "... = c * (h y1 + a1 * xi)";
by (simp add: real_add_mult_distrib2 real_mult_assoc);
also; have "h y1 + a1 * xi = h0 x1";
@@ -235,30 +235,31 @@
qed;
qed;
-text{* $h_0$ is bounded by the quasinorm $p$. *};
+text{* The linear extension $h_0$ of $h$
+is bounded by the seminorm $p$. *};
lemma h0_norm_pres:
- "[| h0 = (\<lambda>x. let (y, a) = SOME (y, a). x = y + a <*> x0 & y:H
+ "[| h0 == (\<lambda>x. let (y, a) = SOME (y, a). x = y + a <*> x0 & y:H
in h y + a * xi);
- H0 = H + lin x0; x0 ~: H; x0 : E; x0 ~= <0>; is_vectorspace E;
- is_subspace H E; is_quasinorm E p; is_linearform H h;
+ H0 == H + lin x0; x0 ~: H; x0 : E; x0 ~= <0>; is_vectorspace E;
+ is_subspace H E; is_seminorm E p; is_linearform H h;
ALL y:H. h y <= p y; (ALL y:H. - p (y + x0) - h y <= xi)
& (ALL y:H. xi <= p (y + x0) - h y) |]
==> ALL x:H0. h0 x <= p x";
proof;
assume h0_def:
- "h0 = (\<lambda>x. let (y, a) = SOME (y, a). x = y + a <*> x0 & y:H
+ "h0 == (\<lambda>x. let (y, a) = SOME (y, a). x = y + a <*> x0 & y:H
in (h y) + a * xi)"
- and H0_def: "H0 = H + lin x0"
+ and H0_def: "H0 == H + lin x0"
and vs: "x0 ~: H" "x0 : E" "x0 ~= <0>" "is_vectorspace E"
- "is_subspace H E" "is_quasinorm E p" "is_linearform H h"
- and a: " ALL y:H. h y <= p y";
- presume a1: "ALL y:H. - p (y + x0) - h y <= xi";
- presume a2: "ALL y:H. xi <= p (y + x0) - h y";
+ "is_subspace H E" "is_seminorm E p" "is_linearform H h"
+ and a: "ALL y:H. h y <= p y";
+ presume a1: "ALL ya:H. - p (ya + x0) - h ya <= xi";
+ presume a2: "ALL ya:H. xi <= p (ya + x0) - h ya";
fix x; assume "x : H0";
have ex_x:
"!! x. x : H0 ==> EX y a. x = y + a <*> x0 & y : H";
- by (simp add: H0_def vs_sum_def lin_def) fast;
+ by (unfold H0_def vs_sum_def lin_def) fast;
have "EX y a. x = y + a <*> x0 & y : H";
by (rule ex_x);
thus "h0 x <= p x";
@@ -268,7 +269,7 @@
by (rule h0_definite);
txt{* Now we show
- $h\ap y + a \cdot xi\leq p\ap (y\plus a \mult x_0)$
+ $h\ap y + a \cdot \xi\leq p\ap (y\plus a \mult x_0)$
by case analysis on $a$. *};
also; have "... <= p (y + a <*> x0)";
@@ -277,17 +278,17 @@
assume z: "a = 0r";
with vs y a; show ?thesis; by simp;
- txt {* In the case $a < 0$ we use $a_1$ with $y$ taken as
- $y/a$. *};
+ txt {* In the case $a < 0$, we use $a_1$ with $\idt{ya}$
+ taken as $y/a$: *};
next;
assume lz: "a < 0r"; hence nz: "a ~= 0r"; by simp;
from a1;
have "- p (rinv a <*> y + x0) - h (rinv a <*> y) <= xi";
- by (rule bspec)(simp!);
-
- txt {* The thesis now follows by a short calculation. *};
+ by (rule bspec) (simp!);
+ txt {* The thesis for this case now follows by a short
+ calculation. *};
hence "a * xi
<= a * (- p (rinv a <*> y + x0) - h (rinv a <*> y))";
by (rule real_mult_less_le_anti [OF lz]);
@@ -296,25 +297,28 @@
by (rule real_mult_diff_distrib);
also; from lz vs y; have "- a * (p (rinv a <*> y + x0))
= p (a <*> (rinv a <*> y + x0))";
- by (simp add: quasinorm_mult_distrib rabs_minus_eqI2);
+ by (simp add: seminorm_rabs_homogenous rabs_minus_eqI2);
also; from nz vs y; have "... = p (y + a <*> x0)";
by (simp add: vs_add_mult_distrib1);
also; from nz vs y; have "a * (h (rinv a <*> y)) = h y";
- by (simp add: linearform_mult_linear [RS sym]);
+ by (simp add: linearform_mult [RS sym]);
finally; have "a * xi <= p (y + a <*> x0) - h y"; .;
hence "h y + a * xi <= h y + p (y + a <*> x0) - h y";
by (simp add: real_add_left_cancel_le);
thus ?thesis; by simp;
- txt {* In the case $a > 0$ we use $a_2$ with $y$ taken
- as $y/a$. *};
+ txt {* In the case $a > 0$, we use $a_2$ with $\idt{ya}$
+ taken as $y/a$: *};
+
next;
assume gz: "0r < a"; hence nz: "a ~= 0r"; by simp;
+ from a2;
have "xi <= p (rinv a <*> y + x0) - h (rinv a <*> y)";
- by (rule bspec [OF a2]) (simp!);
+ by (rule bspec) (simp!);
- txt {* The thesis follows by a short calculation. *};
+ txt {* The thesis for this case follows by a short
+ calculation: *};
with gz; have "a * xi
<= a * (p (rinv a <*> y + x0) - h (rinv a <*> y))";
@@ -325,12 +329,12 @@
also; from gz vs y;
have "a * p (rinv a <*> y + x0)
= p (a <*> (rinv a <*> y + x0))";
- by (simp add: quasinorm_mult_distrib rabs_eqI2);
+ by (simp add: seminorm_rabs_homogenous rabs_eqI2);
also; from nz vs y;
have "... = p (y + a <*> x0)";
by (simp add: vs_add_mult_distrib1);
also; from nz vs y; have "a * h (rinv a <*> y) = h y";
- by (simp add: linearform_mult_linear [RS sym]);
+ by (simp add: linearform_mult [RS sym]);
finally; have "a * xi <= p (y + a <*> x0) - h y"; .;
hence "h y + a * xi <= h y + (p (y + a <*> x0) - h y)";
@@ -342,5 +346,4 @@
qed;
qed blast+;
-
end;
\ No newline at end of file
--- a/src/HOL/Real/HahnBanach/HahnBanachSupLemmas.thy Fri Oct 29 19:24:20 1999 +0200
+++ b/src/HOL/Real/HahnBanach/HahnBanachSupLemmas.thy Fri Oct 29 20:18:34 1999 +0200
@@ -10,20 +10,20 @@
text{* This section contains some lemmas that will be used in the
-proof of the Hahn-Banach theorem.
+proof of the Hahn-Banach Theorem.
In this section the following context is presumed.
-Let $E$ be a real vector space with a quasinorm $q$ on $E$.
-$F$ is a subspace of $E$ and $f$ a linearform on $F$. We
-consider a chain $c$ of norm preserving extensions of $f$, such that
+Let $E$ be a real vector space with a seminorm $q$ on $E$.
+$F$ is a subspace of $E$ and $f$ a linear form on $F$. We
+consider a chain $c$ of norm-preserving extensions of $f$, such that
$\Union c = \idt{graph}\ap H\ap h$.
We will show some properties about the limit function $h$,
-i.~e.~the supremum of the chain $c$.
+i.e.\ the supremum of the chain $c$.
*};
(***
lemma some_H'h't:
"[| M = norm_pres_extensions E p F f; c: chain M;
- graph H h = Union c; x:H|]
+ graph H h = Union c; x:H |]
==> EX H' h' t. t : graph H h & t = (x, h x) & graph H' h':c
& t:graph H' h' & is_linearform H' h' & is_subspace H' E
& is_subspace F H' & graph F f <= graph H' h'
@@ -60,14 +60,14 @@
qed;
***)
-text{* Let $c$ be a chain of norm preserving extensions of the
+text{* Let $c$ be a chain of norm-preserving extensions of the
function $f$ and let $\idt{graph}\ap H\ap h$ be the supremum of $c$.
Every element in $H$ is member of
one of the elements of the chain. *};
lemma some_H'h't:
"[| M = norm_pres_extensions E p F f; c: chain M;
- graph H h = Union c; x:H|]
+ graph H h = Union c; x:H |]
==> EX H' h'. graph H' h' : c & (x, h x) : graph H' h'
& is_linearform H' h' & is_subspace H' E
& is_subspace F H' & graph F f <= graph H' h'
@@ -109,7 +109,7 @@
qed;
-text{* Let $c$ be a chain of norm preserving extensions of the
+text{* Let $c$ be a chain of norm-preserving extensions of the
function $f$ and let $\idt{graph}\ap H\ap h$ be the supremum of $c$.
Every element in the domain $H$ of the supremum function is member of
the domain $H'$ of some function $h'$, such that $h$ extends $h'$.
@@ -117,7 +117,7 @@
lemma some_H'h':
"[| M = norm_pres_extensions E p F f; c: chain M;
- graph H h = Union c; x:H|]
+ graph H h = Union c; x:H |]
==> EX H' h'. x:H' & graph H' h' <= graph H h
& is_linearform H' h' & is_subspace H' E & is_subspace F H'
& graph F f <= graph H' h' & (ALL x:H'. h' x <= p x)";
@@ -147,7 +147,7 @@
(***
lemma some_H'h':
"[| M = norm_pres_extensions E p F f; c: chain M;
- graph H h = Union c; x:H|]
+ graph H h = Union c; x:H |]
==> EX H' h'. x:H' & graph H' h' <= graph H h
& is_linearform H' h' & is_subspace H' E & is_subspace F H'
& graph F f <= graph H' h' & (ALL x:H'. h' x <= p x)";
@@ -185,7 +185,7 @@
text{* Any two elements $x$ and $y$ in the domain $H$ of the
-supremum function $h$ lie both in the domain $H'$ of some function
+supremum function $h$ are both in the domain $H'$ of some function
$h'$, such that $h$ extends $h'$. *};
lemma some_H'h'2:
@@ -265,7 +265,7 @@
(***
lemma some_H'h'2:
"[| M = norm_pres_extensions E p F f; c: chain M;
- graph H h = Union c; x:H; y:H|]
+ graph H h = Union c; x:H; y:H |]
==> EX H' h'. x:H' & y:H' & graph H' h' <= graph H h
& is_linearform H' h' & is_subspace H' E & is_subspace F H'
& graph F f <= graph H' h' & (ALL x:H'. h' x <= p x)";
@@ -350,7 +350,7 @@
txt{* Since both $(x, y) \in \Union c$ and $(x, z) \in \Union c$
they are members of some graphs $G_1$ and $G_2$, resp., such that
- both $G_1$ and $G_2$ are members of $c$*};
+ both $G_1$ and $G_2$ are members of $c$.*};
fix G1 G2; assume
"(x, y) : G1" "G1 : c" "(x, z) : G2" "G2 : c" "c <= M";
@@ -366,8 +366,8 @@
fix H1 h1 H2 h2;
assume "graph H1 h1 = G1" "graph H2 h2 = G2";
- txt{* Since both h $G_1$ and $G_2$ are members of $c$,
- $G_1$ is contained in $G_2$ or vice versa. *};
+ txt{* $G_1$ is contained in $G_2$ or vice versa,
+ since both $G_1$ and $G_2$ are members of $c$. *};
have "G1 <= G2 | G2 <= G1" (is "?case1 | ?case2"); ..;
thus ?thesis;
@@ -390,10 +390,10 @@
qed;
qed;
-text{* The limit function $h$ is linear: every element $x$ in the
+text{* The limit function $h$ is linear. Every element $x$ in the
domain of $h$ is in the domain of a function $h'$ in the chain of norm
preserving extensions. Furthermore, $h$ is an extension of $h'$ so
-the value of $x$ are identical for $h'$ and $h$. Finally, the
+the function values of $x$ are identical for $h'$ and $h$. Finally, the
function $h'$ is linear by construction of $M$. *};
lemma sup_lf:
@@ -412,8 +412,7 @@
& (ALL x:H'. h' x <= p x)";
by (rule some_H'h'2);
- txt {* We have to show that h is linear w.~r.~t.
- addition. *};
+ txt {* We have to show that $h$ is additive. *};
thus "h (x + y) = h x + h y";
proof (elim exE conjE);
@@ -421,7 +420,7 @@
and b: "graph H' h' <= graph H h"
and "is_linearform H' h'" "is_subspace H' E";
have "h' (x + y) = h' x + h' y";
- by (rule linearform_add_linear);
+ by (rule linearform_add);
also; have "h' x = h x"; ..;
also; have "h' y = h y"; ..;
also; have "x + y : H'"; ..;
@@ -436,8 +435,7 @@
& (ALL x:H'. h' x <= p x)";
by (rule some_H'h');
- txt{* We have to show that h is linear w.~r.~t.
- scalar multiplication. *};
+ txt{* We have to show that $h$ is multiplicative. *};
thus "h (a <*> x) = a * h x";
proof (elim exE conjE);
@@ -445,7 +443,7 @@
and b: "graph H' h' <= graph H h"
and "is_linearform H' h'" "is_subspace H' E";
have "h' (a <*> x) = a * h' x";
- by (rule linearform_mult_linear);
+ by (rule linearform_mult);
also; have "h' x = h x"; ..;
also; have "a <*> x : H'"; ..;
with b; have "h' (a <*> x) = h (a <*> x)"; ..;
@@ -462,7 +460,7 @@
lemma sup_ext:
"[| M = norm_pres_extensions E p F f; c: chain M; EX x. x:c;
- graph H h = Union c|] ==> graph F f <= graph H h";
+ graph H h = Union c |] ==> graph F f <= graph H h";
proof -;
assume "M = norm_pres_extensions E p F f" "c: chain M"
"graph H h = Union c";
@@ -484,9 +482,11 @@
thus ?thesis;
proof (elim exE conjE);
- fix G g; assume "graph G g = x" "graph F f <= graph G g";
- have "graph F f <= graph G g"; .;
- also; have "graph G g <= graph H h"; by (simp!, fast);
+ fix G g; assume "graph F f <= graph G g";
+ also; assume "graph G g = x";
+ also; have "... : c"; .;
+ hence "x <= Union c"; by fast;
+ also; have [RS sym]: "graph H h = Union c"; .;
finally; show ?thesis; .;
qed;
qed;
@@ -539,15 +539,15 @@
show ?thesis;
proof;
- txt {* The $\zero$ element lies in $H$, as $F$ is a subset
- of $H$. *};
+ txt {* The $\zero$ element is in $H$, as $F$ is a subset
+ of $H$: *};
have "<0> : F"; ..;
also; have "is_subspace F H"; by (rule sup_supF);
hence "F <= H"; ..;
finally; show "<0> : H"; .;
- txt{* $H$ is a subset of $E$. *};
+ txt{* $H$ is a subset of $E$: *};
show "H <= E";
proof;
@@ -565,7 +565,7 @@
qed;
qed;
- txt{* $H$ is closed under addition. *};
+ txt{* $H$ is closed under addition: *};
show "ALL x:H. ALL y:H. x + y : H";
proof (intro ballI);
@@ -586,7 +586,7 @@
qed;
qed;
- txt{* $H$ is closed under scalar multiplication. *};
+ txt{* $H$ is closed under scalar multiplication: *};
show "ALL x:H. ALL a. a <*> x : H";
proof (intro ballI allI);
@@ -609,7 +609,8 @@
qed;
text {* The limit function is bounded by
-the norm $p$ as well, since all elements in the chain are norm preserving.
+the norm $p$ as well, since all elements in the chain are
+bounded by $p$.
*};
lemma sup_norm_pres:
@@ -635,10 +636,10 @@
qed;
-text_raw{* \medskip *}
-text{* The following lemma is a property of real linearforms on
+text{* \medskip The following lemma is a property of linearforms on
real vector spaces. It will be used for the lemma
-$\idt{rabs{\dsh}HahnBanach}$.
+$\idt{rabs{\dsh}HahnBanach}$ (see page \pageref{rabs-HahnBanach}).
+\label{rabs-ineq-iff}
For real vector spaces the following inequations are equivalent:
\begin{matharray}{ll}
\forall x\in H.\ap |h\ap x|\leq p\ap x& {\rm and}\\
@@ -647,12 +648,12 @@
*};
lemma rabs_ineq_iff:
- "[| is_subspace H E; is_vectorspace E; is_quasinorm E p;
+ "[| is_subspace H E; is_vectorspace E; is_seminorm E p;
is_linearform H h |]
==> (ALL x:H. rabs (h x) <= p x) = (ALL x:H. h x <= p x)"
(concl is "?L = ?R");
proof -;
- assume "is_subspace H E" "is_vectorspace E" "is_quasinorm E p"
+ assume "is_subspace H E" "is_vectorspace E" "is_seminorm E p"
"is_linearform H h";
have h: "is_vectorspace H"; ..;
show ?thesis;
@@ -675,10 +676,10 @@
show "- p x <= h x";
proof (rule real_minus_le);
from h; have "- h x = h (- x)";
- by (rule linearform_neg_linear [RS sym]);
+ by (rule linearform_neg [RS sym]);
also; from r; have "... <= p (- x)"; by (simp!);
also; have "... = p x";
- by (rule quasinorm_minus, rule subspace_subsetD);
+ by (rule seminorm_minus, rule subspace_subsetD);
finally; show "- h x <= p x"; .;
qed;
from r; show "h x <= p x"; ..;
--- a/src/HOL/Real/HahnBanach/Linearform.thy Fri Oct 29 19:24:20 1999 +0200
+++ b/src/HOL/Real/HahnBanach/Linearform.thy Fri Oct 29 20:18:34 1999 +0200
@@ -7,9 +7,8 @@
theory Linearform = VectorSpace:;
-text{* A \emph{linearform} is a function on a vector
-space into the reals that is linear w.~r.~t.~addition and skalar
-multiplikation. *};
+text{* A \emph{linear form} is a function on a vector
+space into the reals that is additive and multiplicative. *};
constdefs
is_linearform :: "['a::{minus, plus} set, 'a => real] => bool"
@@ -23,38 +22,38 @@
==> is_linearform V f";
by (unfold is_linearform_def) force;
-lemma linearform_add_linear [intro!!]:
+lemma linearform_add [intro!!]:
"[| is_linearform V f; x:V; y:V |] ==> f (x + y) = f x + f y";
by (unfold is_linearform_def) fast;
-lemma linearform_mult_linear [intro!!]:
+lemma linearform_mult [intro!!]:
"[| is_linearform V f; x:V |] ==> f (a <*> x) = a * (f x)";
by (unfold is_linearform_def) fast;
-lemma linearform_neg_linear [intro!!]:
+lemma linearform_neg [intro!!]:
"[| is_vectorspace V; is_linearform V f; x:V|]
==> f (- x) = - f x";
proof -;
assume "is_linearform V f" "is_vectorspace V" "x:V";
have "f (- x) = f ((- 1r) <*> x)"; by (simp! add: negate_eq1);
- also; have "... = (- 1r) * (f x)"; by (rule linearform_mult_linear);
+ also; have "... = (- 1r) * (f x)"; by (rule linearform_mult);
also; have "... = - (f x)"; by (simp!);
finally; show ?thesis; .;
qed;
-lemma linearform_diff_linear [intro!!]:
+lemma linearform_diff [intro!!]:
"[| is_vectorspace V; is_linearform V f; x:V; y:V |]
==> f (x - y) = f x - f y";
proof -;
assume "is_vectorspace V" "is_linearform V f" "x:V" "y:V";
have "f (x - y) = f (x + - y)"; by (simp! only: diff_eq1);
also; have "... = f x + f (- y)";
- by (rule linearform_add_linear) (simp!)+;
- also; have "f (- y) = - f y"; by (rule linearform_neg_linear);
+ by (rule linearform_add) (simp!)+;
+ also; have "f (- y) = - f y"; by (rule linearform_neg);
finally; show "f (x - y) = f x - f y"; by (simp!);
qed;
-text{* Every linearform yields $0$ for the $\zero$ vector.*};
+text{* Every linear form yields $0$ for the $\zero$ vector.*};
lemma linearform_zero [intro!!, simp]:
"[| is_vectorspace V; is_linearform V f |] ==> f <0> = 0r";
@@ -62,7 +61,7 @@
assume "is_vectorspace V" "is_linearform V f";
have "f <0> = f (<0> - <0>)"; by (simp!);
also; have "... = f <0> - f <0>";
- by (rule linearform_diff_linear) (simp!)+;
+ by (rule linearform_diff) (simp!)+;
also; have "... = 0r"; by simp;
finally; show "f <0> = 0r"; .;
qed;
--- a/src/HOL/Real/HahnBanach/NormedSpace.thy Fri Oct 29 19:24:20 1999 +0200
+++ b/src/HOL/Real/HahnBanach/NormedSpace.thy Fri Oct 29 20:18:34 1999 +0200
@@ -11,60 +11,61 @@
subsection {* Quasinorms *};
-text{* A \emph{quasinorm} $\norm{\cdot}$ is a function on a real vector space into the reals
-that has the following properties: *};
+text{* A \emph{seminorm} $\norm{\cdot}$ is a function on a real vector
+space into the reals that has the following properties: It is positive
+definite, absolute homogenous and subadditive. *};
constdefs
- is_quasinorm :: "['a::{plus, minus} set, 'a => real] => bool"
- "is_quasinorm V norm == ALL x: V. ALL y:V. ALL a.
+ is_seminorm :: "['a::{plus, minus} set, 'a => real] => bool"
+ "is_seminorm V norm == ALL x: V. ALL y:V. ALL a.
0r <= norm x
& norm (a <*> x) = (rabs a) * (norm x)
& norm (x + y) <= norm x + norm y";
-lemma is_quasinormI [intro]:
- "[| !! x y a. [| x:V; y:V|] ==> 0r <= norm x;
+lemma is_seminormI [intro]:
+ "[| !! x y a. [| x:V; y:V|] ==> 0r <= norm x;
!! x a. x:V ==> norm (a <*> x) = (rabs a) * (norm x);
!! x y. [|x:V; y:V |] ==> norm (x + y) <= norm x + norm y |]
- ==> is_quasinorm V norm";
- by (unfold is_quasinorm_def, force);
+ ==> is_seminorm V norm";
+ by (unfold is_seminorm_def, force);
-lemma quasinorm_ge_zero [intro!!]:
- "[| is_quasinorm V norm; x:V |] ==> 0r <= norm x";
- by (unfold is_quasinorm_def, force);
+lemma seminorm_ge_zero [intro!!]:
+ "[| is_seminorm V norm; x:V |] ==> 0r <= norm x";
+ by (unfold is_seminorm_def, force);
-lemma quasinorm_mult_distrib:
- "[| is_quasinorm V norm; x:V |]
+lemma seminorm_rabs_homogenous:
+ "[| is_seminorm V norm; x:V |]
==> norm (a <*> x) = (rabs a) * (norm x)";
- by (unfold is_quasinorm_def, force);
+ by (unfold is_seminorm_def, force);
-lemma quasinorm_triangle_ineq:
- "[| is_quasinorm V norm; x:V; y:V |]
+lemma seminorm_subadditive:
+ "[| is_seminorm V norm; x:V; y:V |]
==> norm (x + y) <= norm x + norm y";
- by (unfold is_quasinorm_def, force);
+ by (unfold is_seminorm_def, force);
-lemma quasinorm_diff_triangle_ineq:
- "[| is_quasinorm V norm; x:V; y:V; is_vectorspace V |]
+lemma seminorm_diff_subadditive:
+ "[| is_seminorm V norm; x:V; y:V; is_vectorspace V |]
==> norm (x - y) <= norm x + norm y";
proof -;
- assume "is_quasinorm V norm" "x:V" "y:V" "is_vectorspace V";
+ assume "is_seminorm V norm" "x:V" "y:V" "is_vectorspace V";
have "norm (x - y) = norm (x + - 1r <*> y)";
by (simp! add: diff_eq2 negate_eq2);
also; have "... <= norm x + norm (- 1r <*> y)";
- by (simp! add: quasinorm_triangle_ineq);
+ by (simp! add: seminorm_subadditive);
also; have "norm (- 1r <*> y) = rabs (- 1r) * norm y";
- by (rule quasinorm_mult_distrib);
+ by (rule seminorm_rabs_homogenous);
also; have "rabs (- 1r) = 1r"; by (rule rabs_minus_one);
finally; show "norm (x - y) <= norm x + norm y"; by simp;
qed;
-lemma quasinorm_minus:
- "[| is_quasinorm V norm; x:V; is_vectorspace V |]
+lemma seminorm_minus:
+ "[| is_seminorm V norm; x:V; is_vectorspace V |]
==> norm (- x) = norm x";
proof -;
- assume "is_quasinorm V norm" "x:V" "is_vectorspace V";
- have "norm (- x) = norm (-1r <*> x)"; by (simp! only: negate_eq1);
- also; have "... = rabs (-1r) * norm x";
- by (rule quasinorm_mult_distrib);
+ assume "is_seminorm V norm" "x:V" "is_vectorspace V";
+ have "norm (- x) = norm (- 1r <*> x)"; by (simp! only: negate_eq1);
+ also; have "... = rabs (- 1r) * norm x";
+ by (rule seminorm_rabs_homogenous);
also; have "rabs (- 1r) = 1r"; by (rule rabs_minus_one);
finally; show "norm (- x) = norm x"; by simp;
qed;
@@ -72,20 +73,20 @@
subsection {* Norms *};
-text{* A \emph{norm} $\norm{\cdot}$ is a quasinorm that maps only the
+text{* A \emph{norm} $\norm{\cdot}$ is a seminorm that maps only the
$\zero$ vector to $0$. *};
constdefs
is_norm :: "['a::{minus, plus} set, 'a => real] => bool"
- "is_norm V norm == ALL x: V. is_quasinorm V norm
+ "is_norm V norm == ALL x: V. is_seminorm V norm
& (norm x = 0r) = (x = <0>)";
lemma is_normI [intro]:
- "ALL x: V. is_quasinorm V norm & (norm x = 0r) = (x = <0>)
+ "ALL x: V. is_seminorm V norm & (norm x = 0r) = (x = <0>)
==> is_norm V norm"; by (simp only: is_norm_def);
-lemma norm_is_quasinorm [intro!!]:
- "[| is_norm V norm; x:V |] ==> is_quasinorm V norm";
+lemma norm_is_seminorm [intro!!]:
+ "[| is_norm V norm; x:V |] ==> is_seminorm V norm";
by (unfold is_norm_def, force);
lemma norm_zero_iff:
@@ -94,7 +95,7 @@
lemma norm_ge_zero [intro!!]:
"[|is_norm V norm; x:V |] ==> 0r <= norm x";
- by (unfold is_norm_def is_quasinorm_def, force);
+ by (unfold is_norm_def is_seminorm_def, force);
subsection {* Normed vector spaces *};
@@ -141,16 +142,16 @@
finally; show "0r < norm x"; .;
qed;
-lemma normed_vs_norm_mult_distrib [intro!!]:
+lemma normed_vs_norm_rabs_homogenous [intro!!]:
"[| is_normed_vectorspace V norm; x:V |]
==> norm (a <*> x) = (rabs a) * (norm x)";
- by (rule quasinorm_mult_distrib, rule norm_is_quasinorm,
+ by (rule seminorm_rabs_homogenous, rule norm_is_seminorm,
rule normed_vs_norm);
-lemma normed_vs_norm_triangle_ineq [intro!!]:
+lemma normed_vs_norm_subadditive [intro!!]:
"[| is_normed_vectorspace V norm; x:V; y:V |]
==> norm (x + y) <= norm x + norm y";
- by (rule quasinorm_triangle_ineq, rule norm_is_quasinorm,
+ by (rule seminorm_subadditive, rule norm_is_seminorm,
rule normed_vs_norm);
text{* Any subspace of a normed vector space is again a
@@ -165,7 +166,7 @@
show "is_vectorspace F"; ..;
show "is_norm F norm";
proof (intro is_normI ballI conjI);
- show "is_quasinorm F norm";
+ show "is_seminorm F norm";
proof;
fix x y a; presume "x : E";
show "0r <= norm x"; ..;
--- a/src/HOL/Real/HahnBanach/ROOT.ML Fri Oct 29 19:24:20 1999 +0200
+++ b/src/HOL/Real/HahnBanach/ROOT.ML Fri Oct 29 20:18:34 1999 +0200
@@ -5,5 +5,4 @@
The Hahn-Banach theorem for real vector spaces (Isabelle/Isar).
*)
-time_use_thy "Bounds";
time_use_thy "HahnBanach";
--- a/src/HOL/Real/HahnBanach/Subspace.thy Fri Oct 29 19:24:20 1999 +0200
+++ b/src/HOL/Real/HahnBanach/Subspace.thy Fri Oct 29 20:18:34 1999 +0200
@@ -17,15 +17,15 @@
constdefs
is_subspace :: "['a::{minus, plus} set, 'a set] => bool"
- "is_subspace U V == U ~= {} & U <= V
- & (ALL x:U. ALL y:U. ALL a. x + y : U & a <*> x : U)";
+ "is_subspace U V == U ~= {} & U <= V
+ & (ALL x:U. ALL y:U. ALL a. x + y : U & a <*> x : U)";
lemma subspaceI [intro]:
- "[| <0>:U; U <= V; ALL x:U. ALL y:U. (x + y : U);
+ "[| <0> : U; U <= V; ALL x:U. ALL y:U. (x + y : U);
ALL x:U. ALL a. a <*> x : U |]
==> is_subspace U V";
proof (unfold is_subspace_def, intro conjI);
- assume "<0>:U"; thus "U ~= {}"; by fast;
+ assume "<0> : U"; thus "U ~= {}"; by fast;
qed (simp+);
lemma subspace_not_empty [intro!!]: "is_subspace U V ==> U ~= {}";
@@ -35,28 +35,28 @@
by (unfold is_subspace_def) simp;
lemma subspace_subsetD [simp, intro!!]:
- "[| is_subspace U V; x:U |]==> x:V";
+ "[| is_subspace U V; x:U |] ==> x:V";
by (unfold is_subspace_def) force;
lemma subspace_add_closed [simp, intro!!]:
- "[| is_subspace U V; x: U; y: U |] ==> x + y : U";
+ "[| is_subspace U V; x:U; y:U |] ==> x + y : U";
by (unfold is_subspace_def) simp;
lemma subspace_mult_closed [simp, intro!!]:
- "[| is_subspace U V; x: U |] ==> a <*> x: U";
+ "[| is_subspace U V; x:U |] ==> a <*> x : U";
by (unfold is_subspace_def) simp;
lemma subspace_diff_closed [simp, intro!!]:
- "[| is_subspace U V; is_vectorspace V; x: U; y: U |]
- ==> x - y: U";
+ "[| is_subspace U V; is_vectorspace V; x:U; y:U |]
+ ==> x - y : U";
by (simp! add: diff_eq1 negate_eq1);
text {* Similar as for linear spaces, the existence of the
-zero element in every subspace follws from the non-emptyness
-of the subspace and vector space laws.*};
+zero element in every subspace follows from the non-emptiness
+of the carrier set and by vector space laws.*};
lemma zero_in_subspace [intro !!]:
- "[| is_subspace U V; is_vectorspace V |] ==> <0>:U";
+ "[| is_subspace U V; is_vectorspace V |] ==> <0> : U";
proof -;
assume "is_subspace U V" and v: "is_vectorspace V";
have "U ~= {}"; ..;
@@ -72,11 +72,11 @@
qed;
lemma subspace_neg_closed [simp, intro!!]:
- "[| is_subspace U V; is_vectorspace V; x: U |] ==> - x: U";
+ "[| is_subspace U V; is_vectorspace V; x:U |] ==> - x : U";
by (simp add: negate_eq1);
text_raw {* \medskip *};
-text {* Further derived laws: Every subspace is a vector space. *};
+text {* Further derived laws: every subspace is a vector space. *};
lemma subspace_vs [intro!!]:
"[| is_subspace U V; is_vectorspace V |] ==> is_vectorspace U";
@@ -84,7 +84,7 @@
assume "is_subspace U V" "is_vectorspace V";
show ?thesis;
proof;
- show "<0>:U"; ..;
+ show "<0> : U"; ..;
show "ALL x:U. ALL a. a <*> x : U"; by (simp!);
show "ALL x:U. ALL y:U. x + y : U"; by (simp!);
show "ALL x:U. - x = -1r <*> x"; by (simp! add: negate_eq1);
@@ -134,26 +134,26 @@
subsection {* Linear closure *};
-text {* The \emph{linear closure} of a vector $x$ is the set of all
-multiples of $x$. *};
+text {* The \emph{linear closure} of a vector $x$ is the set of all
+scalar multiples of $x$. *};
constdefs
lin :: "'a => 'a set"
- "lin x == {y. EX a. y = a <*> x}";
+ "lin x == {a <*> x | a. True}";
lemma linD: "x : lin v = (EX a::real. x = a <*> v)";
- by (unfold lin_def) force;
+ by (unfold lin_def) fast;
lemma linI [intro!!]: "a <*> x0 : lin x0";
- by (unfold lin_def) force;
+ by (unfold lin_def) fast;
text {* Every vector is contained in its linear closure. *};
-lemma x_lin_x: "[| is_vectorspace V; x:V |] ==> x:lin x";
-proof (unfold lin_def, intro CollectI exI);
+lemma x_lin_x: "[| is_vectorspace V; x:V |] ==> x : lin x";
+proof (unfold lin_def, intro CollectI exI conjI);
assume "is_vectorspace V" "x:V";
show "x = 1r <*> x"; by (simp!);
-qed;
+qed simp;
text {* Any linear closure is a subspace. *};
@@ -162,12 +162,12 @@
proof;
assume "is_vectorspace V" "x:V";
show "<0> : lin x";
- proof (unfold lin_def, intro CollectI exI);
+ proof (unfold lin_def, intro CollectI exI conjI);
show "<0> = 0r <*> x"; by (simp!);
- qed;
+ qed simp;
show "lin x <= V";
- proof (unfold lin_def, intro subsetI, elim CollectE exE);
+ proof (unfold lin_def, intro subsetI, elim CollectE exE conjE);
fix xa a; assume "xa = a <*> x";
show "xa:V"; by (simp!);
qed;
@@ -176,21 +176,23 @@
proof (intro ballI);
fix x1 x2; assume "x1 : lin x" "x2 : lin x";
thus "x1 + x2 : lin x";
- proof (unfold lin_def, elim CollectE exE, intro CollectI exI);
+ proof (unfold lin_def, elim CollectE exE conjE,
+ intro CollectI exI conjI);
fix a1 a2; assume "x1 = a1 <*> x" "x2 = a2 <*> x";
show "x1 + x2 = (a1 + a2) <*> x";
by (simp! add: vs_add_mult_distrib2);
- qed;
+ qed simp;
qed;
show "ALL xa:lin x. ALL a. a <*> xa : lin x";
proof (intro ballI allI);
fix x1 a; assume "x1 : lin x";
thus "a <*> x1 : lin x";
- proof (unfold lin_def, elim CollectE exE, intro CollectI exI);
+ proof (unfold lin_def, elim CollectE exE conjE,
+ intro CollectI exI conjI);
fix a1; assume "x1 = a1 <*> x";
show "a <*> x1 = (a * a1) <*> x"; by (simp!);
- qed;
+ qed simp;
qed;
qed;
@@ -213,7 +215,7 @@
instance set :: (plus) plus; by intro_classes;
defs vs_sum_def:
- "U + V == {x. EX u:U. EX v:V. x = u + v}";(***
+ "U + V == {u + v | u v. u:U & v:V}"; (***
constdefs
vs_sum ::
@@ -223,13 +225,13 @@
lemma vs_sumD:
"x: U + V = (EX u:U. EX v:V. x = u + v)";
- by (unfold vs_sum_def) simp;
+ by (unfold vs_sum_def) fast;
lemmas vs_sumE = vs_sumD [RS iffD1, elimify];
lemma vs_sumI [intro!!]:
"[| x:U; y:V; t= x + y |] ==> t : U + V";
- by (unfold vs_sum_def, intro CollectI bexI);
+ by (unfold vs_sum_def) fast;
text{* $U$ is a subspace of $U + V$. *};
@@ -287,7 +289,7 @@
qed (simp!)+;
qed;
- show "ALL x: U + V. ALL a. a <*> x : U + V";
+ show "ALL x : U + V. ALL a. a <*> x : U + V";
proof (intro ballI allI);
fix x a; assume "x : U + V";
thus "a <*> x : U + V";
@@ -348,10 +350,11 @@
qed;
qed;
-text {* An application of the previous lemma will be used in the
-proof of the Hahn-Banach theorem: for an element $y + a \mult x_0$
-of the direct sum of a vectorspace $H$ and the linear closure of
-$x_0$ the components $y \in H$ and $a$ are unique. *};
+text {* An application of the previous lemma will be used in the proof
+of the Hahn-Banach Theorem (see page \pageref{decomp-H0-use}): for any
+element $y + a \mult x_0$ of the direct sum of a vectorspace $H$ and
+the linear closure of $x_0$ the components $y \in H$ and $a$ are
+uniquely determined. *};
lemma decomp_H0:
"[| is_vectorspace E; is_subspace H E; y1 : H; y2 : H;
@@ -370,9 +373,9 @@
proof;
show "H Int lin x0 <= {<0>}";
proof (intro subsetI, elim IntE, rule singleton_iff[RS iffD2]);
- fix x; assume "x:H" "x:lin x0";
+ fix x; assume "x:H" "x : lin x0";
thus "x = <0>";
- proof (unfold lin_def, elim CollectE exE);
+ proof (unfold lin_def, elim CollectE exE conjE);
fix a; assume "x = a <*> x0";
show ?thesis;
proof (rule case_split);
@@ -388,8 +391,9 @@
qed;
qed;
show "{<0>} <= H Int lin x0";
- proof (intro subsetI, elim singletonE, intro IntI, simp+);
- show "<0> : H"; ..;
+ proof (intro subsetI, elim singletonE, intro IntI,
+ (simp only:)+);
+ show "<0>:H"; ..;
from lin_vs; show "<0> : lin x0"; ..;
qed;
qed;
@@ -404,20 +408,20 @@
qed;
qed;
-text {* Since for an element $y + a \mult x_0$ of the direct sum
+text {* Since for any element $y + a \mult x_0$ of the direct sum
of a vectorspace $H$ and the linear closure of $x_0$ the components
-$y\in H$ and $a$ are unique, follows from $y\in H$ the fact that
+$y\in H$ and $a$ are unique, it follows from $y\in H$ that
$a = 0$.*};
lemma decomp_H0_H:
- "[| is_vectorspace E; is_subspace H E; t:H; x0~:H; x0:E;
+ "[| is_vectorspace E; is_subspace H E; t:H; x0 ~: H; x0:E;
x0 ~= <0> |]
==> (SOME (y, a). t = y + a <*> x0 & y : H) = (t, 0r)";
proof (rule, unfold split_paired_all);
- assume "is_vectorspace E" "is_subspace H E" "t:H" "x0~:H" "x0:E"
+ assume "is_vectorspace E" "is_subspace H E" "t:H" "x0 ~: H" "x0:E"
"x0 ~= <0>";
have h: "is_vectorspace H"; ..;
- fix y a; presume t1: "t = y + a <*> x0" and "y : H";
+ fix y a; presume t1: "t = y + a <*> x0" and "y:H";
have "y = t & a = 0r";
by (rule decomp_H0) (assumption | (simp!))+;
thus "(y, a) = (t, 0r)"; by (simp!);
@@ -428,14 +432,14 @@
$h_0 (y \plus a \mult x_0) = h y + a \cdot \xi$ is definite. *};
lemma h0_definite:
- "[| h0 = (\<lambda>x. let (y, a) = SOME (y, a). (x = y + a <*> x0 & y:H)
+ "[| h0 == (\<lambda>x. let (y, a) = SOME (y, a). (x = y + a <*> x0 & y:H)
in (h y) + a * xi);
x = y + a <*> x0; is_vectorspace E; is_subspace H E;
y:H; x0 ~: H; x0:E; x0 ~= <0> |]
==> h0 x = h y + a * xi";
proof -;
assume
- "h0 = (\<lambda>x. let (y, a) = SOME (y, a). (x = y + a <*> x0 & y:H)
+ "h0 == (\<lambda>x. let (y, a) = SOME (y, a). (x = y + a <*> x0 & y:H)
in (h y) + a * xi)"
"x = y + a <*> x0" "is_vectorspace E" "is_subspace H E"
"y:H" "x0 ~: H" "x0:E" "x0 ~= <0>";
@@ -443,25 +447,25 @@
by (simp! add: vs_sum_def lin_def) force+;
have "EX! xa. ((\<lambda>(y, a). x = y + a <*> x0 & y:H) xa)";
proof;
- show "EX xa. ((%(y, a). x = y + a <*> x0 & y:H) xa)";
+ show "EX xa. ((\<lambda>(y, a). x = y + a <*> x0 & y:H) xa)";
by (force!);
next;
fix xa ya;
- assume "(%(y,a). x = y + a <*> x0 & y : H) xa"
- "(%(y,a). x = y + a <*> x0 & y : H) ya";
+ assume "(\<lambda>(y,a). x = y + a <*> x0 & y : H) xa"
+ "(\<lambda>(y,a). x = y + a <*> x0 & y : H) ya";
show "xa = ya"; ;
proof -;
show "fst xa = fst ya & snd xa = snd ya ==> xa = ya";
by (rule Pair_fst_snd_eq [RS iffD2]);
- have x: "x = (fst xa) + (snd xa) <*> x0 & (fst xa) : H";
+ have x: "x = fst xa + snd xa <*> x0 & fst xa : H";
by (force!);
- have y: "x = (fst ya) + (snd ya) <*> x0 & (fst ya) : H";
+ have y: "x = fst ya + snd ya <*> x0 & fst ya : H";
by (force!);
from x y; show "fst xa = fst ya & snd xa = snd ya";
by (elim conjE) (rule decomp_H0, (simp!)+);
qed;
qed;
- hence eq: "(SOME (y, a). (x = y + a <*> x0 & y:H)) = (y, a)";
+ hence eq: "(SOME (y, a). x = y + a <*> x0 & y:H) = (y, a)";
by (rule select1_equality) (force!);
thus "h0 x = h y + a * xi"; by (simp! add: Let_def);
qed;
--- a/src/HOL/Real/HahnBanach/VectorSpace.thy Fri Oct 29 19:24:20 1999 +0200
+++ b/src/HOL/Real/HahnBanach/VectorSpace.thy Fri Oct 29 20:18:34 1999 +0200
@@ -10,14 +10,11 @@
subsection {* Signature *};
text {* For the definition of real vector spaces a type $\alpha$
-of the sort $\idt{plus}, \idt{minus}$ is considered, on which a
-real scalar multiplication $\mult$ is defined, and which has an zero
-element $\zero$.*};
+of the sort $\{ \idt{plus}, \idt{minus}\}$ is considered, on which a
+real scalar multiplication $\mult$, and a zero
+element $\zero$ is defined. *};
consts
-(***
- sum :: "['a, 'a] => 'a" (infixl "+" 65)
-***)
prod :: "[real, 'a] => 'a" (infixr "<*>" 70)
zero :: 'a ("<0>");
@@ -45,7 +42,7 @@
and commutative; $\minus x$ is the inverse of $x$ w.~r.~t.~addition
and $\zero$ is the neutral element of addition. Addition and
multiplication are distributive; scalar multiplication is
- associative and the real $1$ is the neutral element of scalar
+ associative and the real number $1$ is the neutral element of scalar
multiplication.
*};
@@ -55,7 +52,7 @@
& (ALL x:V. ALL y:V. ALL z:V. ALL a b.
x + y : V
& a <*> x : V
- & x + y + z = x + (y + z)
+ & (x + y) + z = x + (y + z)
& x + y = y + x
& x - x = <0>
& <0> + x = x
@@ -72,8 +69,8 @@
lemma vsI [intro]:
"[| <0>:V;
ALL x:V. ALL y:V. x + y : V;
- ALL x:V. ALL a. a <*> x : V;
- ALL x:V. ALL y:V. ALL z:V. x + y + z = x + (y + z);
+ ALL x:V. ALL a. a <*> x : V;
+ ALL x:V. ALL y:V. ALL z:V. (x + y) + z = x + (y + z);
ALL x:V. ALL y:V. x + y = y + x;
ALL x:V. x - x = <0>;
ALL x:V. <0> + x = x;
@@ -82,7 +79,7 @@
ALL x:V. ALL a b. (a * b) <*> x = a <*> b <*> x;
ALL x:V. 1r <*> x = x;
ALL x:V. - x = (- 1r) <*> x;
- ALL x:V. ALL y:V. x - y = x + - y|] ==> is_vectorspace V";
+ ALL x:V. ALL y:V. x - y = x + - y |] ==> is_vectorspace V";
proof (unfold is_vectorspace_def, intro conjI ballI allI);
fix x y z;
assume "x:V" "y:V" "z:V"
@@ -113,7 +110,7 @@
by (unfold is_vectorspace_def) simp;
lemma vs_add_closed [simp, intro!!]:
- "[| is_vectorspace V; x:V; y:V|] ==> x + y : V";
+ "[| is_vectorspace V; x:V; y:V |] ==> x + y : V";
by (unfold is_vectorspace_def) simp;
lemma vs_mult_closed [simp, intro!!]:
@@ -121,7 +118,7 @@
by (unfold is_vectorspace_def) simp;
lemma vs_diff_closed [simp, intro!!]:
- "[| is_vectorspace V; x:V; y:V|] ==> x - y : V";
+ "[| is_vectorspace V; x:V; y:V |] ==> x - y : V";
by (simp add: diff_eq1 negate_eq1);
lemma vs_neg_closed [simp, intro!!]:
@@ -129,8 +126,8 @@
by (simp add: negate_eq1);
lemma vs_add_assoc [simp]:
- "[| is_vectorspace V; x:V; y:V; z:V|]
- ==> x + y + z = x + (y + z)";
+ "[| is_vectorspace V; x:V; y:V; z:V |]
+ ==> (x + y) + z = x + (y + z)";
by (unfold is_vectorspace_def) fast;
lemma vs_add_commute [simp]:
@@ -155,8 +152,8 @@
"[| is_vectorspace V; x:V |] ==> x - x = <0>";
by (unfold is_vectorspace_def) simp;
-text {* The existence of the zero element a vector space
-follows from the non-emptyness of the vector space. *};
+text {* The existence of the zero element of a vector space
+follows from the non-emptiness of carrier set. *};
lemma zero_in_vs [simp, intro]: "is_vectorspace V ==> <0>:V";
proof -;
@@ -228,12 +225,12 @@
finally; show ?thesis; .;
qed;
-(*text_raw {* \paragraph {Further derived laws:} *};*)
+(*text_raw {* \paragraph {Further derived laws.} *};*)
text_raw {* \medskip *};
text{* Further derived laws: *};
lemma vs_mult_zero_left [simp]:
- "[| is_vectorspace V; x:V|] ==> 0r <*> x = <0>";
+ "[| is_vectorspace V; x:V |] ==> 0r <*> x = <0>";
proof -;
assume "is_vectorspace V" "x:V";
have "0r <*> x = (1r - 1r) <*> x"; by (simp only: real_diff_self);
@@ -304,11 +301,11 @@
qed;
lemma vs_add_minus_cancel [simp]:
- "[| is_vectorspace V; x:V; y:V |] ==> x + (- x + y) = y";
+ "[| is_vectorspace V; x:V; y:V |] ==> x + (- x + y) = y";
by (simp add: vs_add_assoc [RS sym] del: vs_add_commute);
lemma vs_minus_add_cancel [simp]:
- "[| is_vectorspace V; x:V; y:V |] ==> - x + (x + y) = y";
+ "[| is_vectorspace V; x:V; y:V |] ==> - x + (x + y) = y";
by (simp add: vs_add_assoc [RS sym] del: vs_add_commute);
lemma vs_minus_add_distrib [simp]:
@@ -325,7 +322,7 @@
by (simp add:diff_eq1);
lemma vs_add_left_cancel:
- "[| is_vectorspace V; x:V; y:V; z:V|]
+ "[| is_vectorspace V; x:V; y:V; z:V |]
==> (x + y = x + z) = (y = z)"
(concl is "?L = ?R");
proof;
@@ -338,7 +335,7 @@
also; have "- x + ... = - x + x + z";
by (rule vs_add_assoc [RS sym]) (simp!)+;
also; have "... = z"; by (simp!);
- finally; show ?R;.;
+ finally; show ?R; .;
qed force;
lemma vs_add_right_cancel:
@@ -381,7 +378,7 @@
by (simp! only: vs_mult_assoc);
also; assume ?L;
also; have "rinv a <*> ... = y"; by (simp!);
- finally; show ?R;.;
+ finally; show ?R; .;
qed simp;
lemma vs_mult_right_cancel: (*** forward ***)
@@ -437,7 +434,7 @@
also; from vs; have "... = z + <0>";
by (simp only: vs_add_minus_left);
also; from vs; have "... = z"; by (simp only: vs_add_zero_right);
- finally; show ?R;.;
+ finally; show ?R; .;
next;
assume ?R;
hence "z - y = (x + y) - y"; by simp;
@@ -451,7 +448,7 @@
qed;
lemma vs_add_minus_eq_minus:
- "[| is_vectorspace V; x:V; y:V; x + y = <0>|] ==> x = - y";
+ "[| is_vectorspace V; x:V; y:V; x + y = <0> |] ==> x = - y";
proof -;
assume "is_vectorspace V" "x:V" "y:V";
have "x = (- y + y) + x"; by (simp!);
@@ -473,11 +470,11 @@
qed;
lemma vs_add_diff_swap:
- "[| is_vectorspace V; a:V; b:V; c:V; d:V; a + b = c + d|]
+ "[| is_vectorspace V; a:V; b:V; c:V; d:V; a + b = c + d |]
==> a - c = d - b";
proof -;
assume vs: "is_vectorspace V" "a:V" "b:V" "c:V" "d:V"
- and eq: "a + b = c + d";
+ and eq: "a + b = c + d";
have "- c + (a + b) = - c + (c + d)";
by (simp! add: vs_add_left_cancel);
also; have "... = d"; by (rule vs_minus_add_cancel);
@@ -491,9 +488,9 @@
qed;
lemma vs_add_cancel_21:
- "[| is_vectorspace V; x:V; y:V; z:V; u:V|]
+ "[| is_vectorspace V; x:V; y:V; z:V; u:V |]
==> (x + (y + z) = y + u) = ((x + z) = u)"
- (concl is "?L = ?R" );
+ (concl is "?L = ?R");
proof -;
assume "is_vectorspace V" "x:V" "y:V""z:V" "u:V";
show "?L = ?R";
--- a/src/HOL/Real/HahnBanach/ZornLemma.thy Fri Oct 29 19:24:20 1999 +0200
+++ b/src/HOL/Real/HahnBanach/ZornLemma.thy Fri Oct 29 20:18:34 1999 +0200
@@ -8,10 +8,10 @@
theory ZornLemma = Aux + Zorn:;
text{*
-Zorn's Lemmas says: if every linear ordered subset of an ordered set
+Zorn's Lemmas states: if every linear ordered subset of an ordered set
$S$ has an upper bound in $S$, then there exists a maximal element in $S$.
-In our application $S$ is a set of sets, ordered by set inclusion. Since
-the union of a chain of sets is an upperbound for all elements of the
+In our application, $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 $S$ is non-empty, it suffices to show that for every non-empty
chain $c$ in $S$ the union of $c$ also lies in $S$.
@@ -21,6 +21,8 @@
"a:S ==> (!!c. c: chain S ==> EX x. x:c ==> Union c : S)
==> EX y: S. ALL z: S. y <= z --> y = z";
proof (rule Zorn_Lemma2);
+ txt_raw{* \footnote{See
+ \url{http://isabelle.in.tum.de/library/HOL/HOL-Real/Zorn.html}}*};
assume aS: "a:S";
assume r: "!!c. c: chain S ==> EX x. x:c ==> Union c : S";
show "ALL c:chain S. EX y:S. ALL z:c. z <= y";
@@ -30,13 +32,13 @@
proof (rule case_split);
txt{* If $c$ is an empty chain, then every element
- in $S$ is an upperbound of $c$. *};
+ in $S$ is an upper bound of $c$. *};
assume "c={}";
with aS; show ?thesis; by fast;
txt{* If $c$ is non-empty, then $\Union c$
- is an upperbound of $c$, that lies in $S$. *};
+ is an upper bound of $c$, lying in $S$. *};
next;
assume c: "c~={}";
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Real/HahnBanach/document/bbb.sty Fri Oct 29 20:18:34 1999 +0200
@@ -0,0 +1,25 @@
+% bbb.sty 10-Nov-1991, 27-Mar-1994
+%
+% blackboard-bold symbols: B C D E F G H I J K L M N O P Q R T U Z
+%
+
+\def\bbbB{{{\rm I}\mkern-3.8mu{\rm B}}}
+\def\bbbC{{{\rm C}\mkern-15mu{\phantom{\rm t}\vrule}\mkern9mu}}
+\def\bbbD{{{\rm I}\mkern-3.8mu{\rm D}}}
+\def\bbbE{{{\rm I}\mkern-3.8mu{\rm E}}}
+\def\bbbF{{{\rm I}\mkern-3.8mu{\rm F}}}
+\def\bbbG{{{\rm G}\mkern-16mu{\phantom{\rm t}\vrule}\mkern10mu}}
+\def\bbbH{{{\rm I}\mkern-3.8mu{\rm H}}}
+\def\bbbI{{{\rm I}\mkern-12mu{\phantom{\rm t}\vrule}\mkern6mu}}
+\def\bbbJ{{{\rm J}\mkern-12mu{\phantom{\rm t}\vrule}\mkern6mu}}
+\def\bbbK{{{\rm I}\mkern-3.8mu{\rm K}}}
+\def\bbbL{{{\rm I}\mkern-3.8mu{\rm L}}}
+\def\bbbM{{{\rm I}\mkern-3.8mu{\rm M}}}
+\def\bbbN{{{\rm I}\mkern-3.8mu{\rm N}}}
+\def\bbbO{{{\rm O}\mkern-16mu{\phantom{\rm t}\vrule}\mkern10mu}}
+\def\bbbP{{{\rm I}\mkern-3.8mu{\rm P}}}
+\def\bbbQ{{{\rm Q}\mkern-16mu{\phantom{\rm t}\vrule}\mkern10mu}}
+\def\bbbR{{{\rm I}\mkern-3.8mu{\rm R}}}
+\def\bbbT{{{\rm T}\mkern-16mu{\phantom{\rm t}\vrule}\mkern10mu}}
+\def\bbbU{{{\rm U}\mkern-15mu{\phantom{\rm t}\vrule}\mkern9mu}}
+\def\bbbZ{{{\sf Z}\mkern-7.5mu{\sf Z}}}
--- a/src/HOL/Real/HahnBanach/document/notation.tex Fri Oct 29 19:24:20 1999 +0200
+++ b/src/HOL/Real/HahnBanach/document/notation.tex Fri Oct 29 20:18:34 1999 +0200
@@ -1,11 +1,10 @@
\renewcommand{\isamarkupheader}[1]{\section{#1}}
-\newcommand{\isasymbollambda}{${\mathtt{\lambda}}$}
-
+\newcommand{\isasymlambda}{${\mathtt{\lambda}}$}
+\newcommand{\isasymprod}{\emph{$\mult$}}
+\newcommand{\isasymzero}{\emph{$\zero$}}
-\newcommand{\name}[1]{\textsf{#1}}
-
\newcommand{\idt}[1]{{\mathord{\mathit{#1}}}}
\newcommand{\var}[1]{{?\!#1}}
\DeclareMathSymbol{\dshsym}{\mathalpha}{letters}{"2D}
@@ -13,30 +12,22 @@
\newenvironment{matharray}[1]{\[\begin{array}{#1}}{\end{array}\]}
-\newcommand{\ty}{{\mathbin{:\,}}}
\newcommand{\To}{\to}
\newcommand{\dt}{{\mathpunct.}}
-\newcommand{\all}[1]{\forall #1\dt\;}
-\newcommand{\ex}[1]{\exists #1\dt\;}
-\newcommand{\EX}[1]{\exists #1\dt\;}
-\newcommand{\eps}[1]{\epsilon\; #1}
-%\newcommand{\Forall}{\mathop\bigwedge}
+\newcommand{\Ex}[1]{\exists #1\dt\;}
\newcommand{\Forall}{\forall}
\newcommand{\All}[1]{\Forall #1\dt\;}
-\newcommand{\ALL}[1]{\Forall #1\dt\;}
-\newcommand{\Eps}[1]{\Epsilon #1\dt\;}
\newcommand{\Eq}{\mathbin{\,\equiv\,}}
-\newcommand{\True}{\name{true}}
-\newcommand{\False}{\name{false}}
\newcommand{\Impl}{\Rightarrow}
\newcommand{\And}{\;\land\;}
\newcommand{\Or}{\;\lor\;}
\newcommand{\Le}{\le}
\newcommand{\Lt}{\lt}
\newcommand{\lam}[1]{\mathop{\lambda} #1\dt\;}
-\newcommand{\ap}{\mathbin{}}
+\newcommand{\ap}{\mathpalette{\mathbin{\!}}{\mathbin{\!}}{\mathbin{}}{\mathbin{}}}
\newcommand{\Union}{\bigcup}
-
+\newcommand{\Un}{\cup}
+\newcommand{\Int}{\cap}
\newcommand{\norm}[1]{\left\|#1\right\|}
\newcommand{\fnorm}[1]{\left\|#1\right\|}
@@ -44,20 +35,8 @@
\newcommand{\plus}{\mathbin{\mathbf +}}
\newcommand{\minus}{\mathbin{\mathbf -}}
\newcommand{\mult}{\mathbin{\mathbf\odot}}
-\newcommand{\1}{\mathord{\mathrm{1}}}
-%\newcommand{\zero}{{\mathord{\small\sl\tt {<0>}}}}
-%\newcommand{\plus}{{\mathbin{\;\small\sl\tt {[+]}\;}}}
-%\newcommand{\minus}{{\mathbin{\;\small\sl\tt {[-]}\;}}}
-%\newcommand{\mult}{{\mathbin{\;\small\sl\tt {[*]}\;}}}
-%\newcommand{\1}{{\mathord{\mathrb{1}}}}
-\newcommand{\fl}{{\mathord{\bf\underline{\phantom{i}}}}}
-\renewcommand{\times}{\;{\mathbin{\cdot}}\;}
-\newcommand{\qed}{\hfill~$\Box$}
-\newcommand{\isasymbolprod}{$\mult$}
-\newcommand{\isasymbolzero}{$\zero$}
-
-%%% Local Variables:
+%%% Local Variables:
%%% mode: latex
%%% TeX-master: "root"
-%%% End:
+%%% End:
--- a/src/HOL/Real/HahnBanach/document/root.tex Fri Oct 29 19:24:20 1999 +0200
+++ b/src/HOL/Real/HahnBanach/document/root.tex Fri Oct 29 20:18:34 1999 +0200
@@ -4,6 +4,7 @@
\usepackage{comment}
\usepackage{latexsym,theorem}
\usepackage{isabelle,pdfsetup} %last one!
+\usepackage{bbb}
\input{notation}
@@ -13,11 +14,13 @@
\pagenumbering{arabic}
\title{The Hahn-Banach Theorem for Real Vector Spaces}
-\author{Gertrud Bauer}
+
+\author{Gertrud Bauer \\ \url{http://www.in.tum.de/~bauerg/}}
+\maketitle
\maketitle
\begin{abstract}
- The Hahn-Banach theorem is one of the most fundamental results in functional
+ 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
@@ -31,11 +34,11 @@
\clearpage
\section{Preface}
-This is a fully formal proof of the Hahn-Banach theorem. It closely follows
+This is a fully formal proof of the Hahn-Banach Theorem. It closely follows
the informal presentation given in the 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 in \cite{Narici:1996}.
+Hahn-Banach Theorem is given in \cite{Narici:1996}.
\medskip The document is structured as follows. The first part contains
definitions of basic notions of linear algebra: vector spaces, subspaces,