--- a/src/HOL/IsaMakefile Fri Oct 22 18:41:00 1999 +0200
+++ b/src/HOL/IsaMakefile Fri Oct 22 20:14:31 1999 +0200
@@ -101,12 +101,12 @@
$(LOG)/HOL-Real-HahnBanach.gz: $(OUT)/HOL-Real Real/HahnBanach/Aux.thy \
Real/HahnBanach/Bounds.thy Real/HahnBanach/FunctionNorm.thy \
Real/HahnBanach/FunctionOrder.thy Real/HahnBanach/HahnBanach.thy \
- Real/HahnBanach/HahnBanach_h0_lemmas.thy \
- Real/HahnBanach/HahnBanach_lemmas.thy \
- Real/HahnBanach/LinearSpace.thy Real/HahnBanach/Linearform.thy \
- Real/HahnBanach/NormedSpace.thy Real/HahnBanach/ROOT.ML \
- Real/HahnBanach/Subspace.thy Real/HahnBanach/Zorn_Lemma.thy \
- Real/HahnBanach/document/notation.tex \
+ Real/HahnBanach/HahnBanachExtLemmas.thy \
+ Real/HahnBanach/HahnBanachSupLemmas.thy \
+ Real/HahnBanach/Linearform.thy Real/HahnBanach/NormedSpace.thy \
+ Real/HahnBanach/README.html Real/HahnBanach/ROOT.ML \
+ Real/HahnBanach/Subspace.thy Real/HahnBanach/VectorSpace.thy \
+ Real/HahnBanach/ZornLemma.thy Real/HahnBanach/document/notation.tex \
Real/HahnBanach/document/root.tex
@cd Real; $(ISATOOL) usedir $(OUT)/HOL-Real HahnBanach
--- a/src/HOL/Real/HahnBanach/Aux.thy Fri Oct 22 18:41:00 1999 +0200
+++ b/src/HOL/Real/HahnBanach/Aux.thy Fri Oct 22 20:14:31 1999 +0200
@@ -7,17 +7,42 @@
theory Aux = Real + Zorn:;
+text {* Some existing theorems are declared as extra introduction
+or elimination rules, respectively. *};
+
+lemmas [intro!!] = isLub_isUb;
lemmas [intro!!] = chainD;
lemmas chainE2 = chainD2 [elimify];
-lemmas [intro!!] = isLub_isUb;
+
+text_raw {* \medskip *};
+text{* Lemmas about sets: *};
+
+lemma Int_singletonD: "[| A Int B = {v}; x:A; x:B |] ==> x = v";
+ by (fast elim: equalityE);
+
+lemma set_less_imp_diff_not_empty: "H < E ==> EX x0:E. x0 ~: H";
+ by (force simp add: psubset_eq);
+
+text_raw {* \medskip *};
+text{* Some lemmas about orders: *};
-theorem real_linear_split:
- "[| x < a ==> Q; x = a ==> Q; a < (x::real) ==> Q |] ==> Q";
- by (rule real_linear [of x a, elimify], elim disjE, force+);
+lemma lt_imp_not_eq: "x < (y::'a::order) ==> x ~= y";
+ by (rule order_less_le[RS iffD1, RS conjunct2]);
+
+lemma le_noteq_imp_less:
+ "[| x <= (r::'a::order); x ~= r |] ==> x < r";
+proof -;
+ assume "x <= (r::'a::order)" and ne:"x ~= r";
+ hence "x < r | x = r"; by (simp add: order_le_less);
+ with ne; show ?thesis; by simp;
+qed;
+
+text_raw {* \medskip *};
+text {* Some lemmas about linear orders. *};
theorem linorder_linear_split:
"[| x < a ==> Q; x = a ==> Q; a < (x::'a::linorder) ==> Q |] ==> Q";
- by (rule linorder_less_linear [of x a, elimify], elim disjE, force+);
+ by (rule linorder_less_linear [of x a, elimify]) force+;
lemma le_max1: "x <= max x (y::'a::linorder)";
by (simp add: le_max_iff_disj[of x x y]);
@@ -25,11 +50,8 @@
lemma le_max2: "y <= max x (y::'a::linorder)";
by (simp add: le_max_iff_disj[of y x y]);
-lemma lt_imp_not_eq: "x < (y::'a::order) ==> x ~= y";
- by (rule order_less_le[RS iffD1, RS conjunct2]);
-
-lemma Int_singletonD: "[| A Int B = {v}; x:A; x:B |] ==> x = v";
- by (fast elim: equalityE);
+text_raw {* \medskip *};
+text{* Some lemmas for the reals. *};
lemma real_add_minus_eq: "x - y = 0r ==> x = y";
proof -;
@@ -106,14 +128,6 @@
finally; show ?thesis; .;
qed;
-lemma le_noteq_imp_less:
- "[| x <= (r::'a::order); x ~= r |] ==> x < r";
-proof -;
- assume "x <= (r::'a::order)" and ne:"x ~= r";
- then; have "x < r | x = r"; by (simp add: order_le_less);
- with ne; show ?thesis; by simp;
-qed;
-
lemma real_minus_le: "- (x::real) <= y ==> - y <= x";
by simp;
@@ -121,7 +135,4 @@
"(d::real) - b <= c + a ==> - a - b <= c - d";
by simp;
-lemma set_less_imp_diff_not_empty: "H < E ==> EX x0:E. x0 ~: H";
- by (force simp add: psubset_eq);
-
end;
\ No newline at end of file
--- a/src/HOL/Real/HahnBanach/Bounds.thy Fri Oct 22 18:41:00 1999 +0200
+++ b/src/HOL/Real/HahnBanach/Bounds.thy Fri Oct 22 20:14:31 1999 +0200
@@ -7,18 +7,19 @@
theory Bounds = Main + Real:;
+text_raw {* \begin{comment} *};
subsection {* The sets of lower and upper bounds *};
constdefs
is_LowerBound :: "('a::order) set => 'a set => 'a => bool"
- "is_LowerBound A B == %x. x:A & (ALL y:B. x <= y)"
+ "is_LowerBound A B == \<lambda>x. x:A & (ALL y:B. x <= y)"
LowerBounds :: "('a::order) set => 'a set => 'a set"
"LowerBounds A B == Collect (is_LowerBound A B)"
is_UpperBound :: "('a::order) set => 'a set => 'a => bool"
- "is_UpperBound A B == %x. x:A & (ALL y:B. y <= x)"
+ "is_UpperBound A B == \<lambda>x. x:A & (ALL y:B. y <= x)"
UpperBounds :: "('a::order) set => 'a set => 'a set"
"UpperBounds A B == Collect (is_UpperBound A B)";
@@ -34,9 +35,9 @@
("(3LOWER'_BOUNDS _./ _)" 10);
translations
- "UPPER_BOUNDS x:A. P" == "UpperBounds A (Collect (%x. P))"
+ "UPPER_BOUNDS x:A. P" == "UpperBounds A (Collect (\<lambda>x. P))"
"UPPER_BOUNDS x. P" == "UPPER_BOUNDS x:UNIV. P"
- "LOWER_BOUNDS x:A. P" == "LowerBounds A (Collect (%x. P))"
+ "LOWER_BOUNDS x:A. P" == "LowerBounds A (Collect (\<lambda>x. P))"
"LOWER_BOUNDS x. P" == "LOWER_BOUNDS x:UNIV. P";
@@ -68,42 +69,67 @@
subsection {* Infimum and Supremum *};
+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{* If a supremum exists, then $\idt{Sup}\ap A\ap B$
+is equal to the supremum. *};
+
constdefs
is_Sup :: "('a::order) set => 'a set => 'a => bool"
"is_Sup A B x == isLub A B x"
-
+
Sup :: "('a::order) set => 'a set => 'a"
- "Sup A B == Eps (is_Sup A B)"
+ "Sup A B == Eps (is_Sup A B)";
+;
+text_raw {* \begin{comment} *};
- is_Inf :: "('a::order) set => 'a set => 'a => bool"
+constdefs
+ is_Inf :: "('a::order) set => 'a set => 'a => bool"
"is_Inf A B x == x:A & is_Greatest (LowerBounds A B) x"
Inf :: "('a::order) set => 'a set => 'a"
"Inf A B == Eps (is_Inf A B)";
syntax
- "_SUP" :: "[pttrn, 'a set, 'a => bool] => 'a set"
+ "_SUP" :: "[pttrn, 'a set, 'a => bool] => 'a set"
("(3SUP _:_./ _)" 10)
- "_SUP_U" :: "[pttrn, 'a => bool] => 'a set"
+ "_SUP_U" :: "[pttrn, 'a => bool] => 'a set"
("(3SUP _./ _)" 10)
- "_INF" :: "[pttrn, 'a set, 'a => bool] => 'a set"
+ "_INF" :: "[pttrn, 'a set, 'a => bool] => 'a set"
("(3INF _:_./ _)" 10)
- "_INF_U" :: "[pttrn, 'a => bool] => 'a set"
+ "_INF_U" :: "[pttrn, 'a => bool] => 'a set"
("(3INF _./ _)" 10);
translations
- "SUP x:A. P" == "Sup A (Collect (%x. P))"
+ "SUP x:A. P" == "Sup A (Collect (\<lambda>x. P))"
"SUP x. P" == "SUP x:UNIV. P"
- "INF x:A. P" == "Inf A (Collect (%x. P))"
+ "INF x:A. P" == "Inf A (Collect (\<lambda>x. P))"
"INF x. P" == "INF x:UNIV. P";
+text_raw {* \end{comment} *};
+;
+
+text{* The supremum of $B$ is less than every 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$. *};
+
lemma sup_ub: "y:B ==> is_Sup A B s ==> y <= s";
by (unfold is_Sup_def, rule isLubD2);
-lemma sup_ub1: "ALL y:B. a <= y ==> is_Sup A B s ==> x:B ==> a <= s";
+text{* The supremum of a non-empty set $B$ is greater
+than a lower bound of $B$. *};
+
+lemma sup_ub1:
+ "[| ALL y:B. a <= y; is_Sup A B s; x:B |] ==> a <= s";
proof -;
assume "ALL y:B. a <= y" "is_Sup A B s" "x:B";
have "a <= x"; by (rule bspec);
--- a/src/HOL/Real/HahnBanach/FunctionNorm.thy Fri Oct 22 18:41:00 1999 +0200
+++ b/src/HOL/Real/HahnBanach/FunctionNorm.thy Fri Oct 22 20:14:31 1999 +0200
@@ -7,13 +7,23 @@
theory FunctionNorm = NormedSpace + FunctionOrder:;
+subsection {* Continous linearforms*};
+
+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:
+*};
constdefs
- is_continous :: "['a set, 'a => real, 'a => real] => bool"
+ is_continous ::
+ "['a::{minus, plus} set, 'a => real, 'a => real] => bool"
"is_continous V norm f ==
- (is_linearform V f & (EX c. ALL x:V. rabs (f x) <= c * norm x))";
+ is_linearform V f & (EX c. ALL x:V. rabs (f x) <= c * norm x)";
-lemma lipschitz_continousI [intro]:
+lemma continousI [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);
@@ -26,173 +36,283 @@
by (unfold is_continous_def) force;
lemma continous_bounded [intro!!]:
- "is_continous V norm f ==> EX c. ALL x:V. rabs (f x) <= c * norm x";
+ "is_continous V norm f
+ ==> EX c. ALL x:V. rabs (f x) <= c * norm x";
by (unfold is_continous_def) force;
+subsection{* The norm of a linearform *};
+
+
+text{* The least real number $c$ for which holds
+\[\forall\ap x\in V.\ap |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
+\[\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
+set, 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 greater or equal $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 greater or equal $0$.
+
+Thus $B$ is defined as follows.
+*};
+
constdefs
- B:: "[ 'a set, 'a => real, 'a => real ] => real set"
+ 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)))}";
+ {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. *};
constdefs
function_norm :: " ['a set, 'a => real, 'a => real] => real"
- "function_norm V norm f ==
- Sup UNIV (B V norm f)";
+ "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 .*};
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";
+ 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";
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. *};
+
lemma ex_fnorm [intro!!]:
"[| is_normed_vectorspace V norm; is_continous 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);
+proof (unfold function_norm_def is_function_norm_def
+ is_continous_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
+ 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. *};
+
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. *};
+
from e; show "EX Y. isUb UNIV (B V norm f) Y";
proof;
+
+ txt {* We know that $f$ is bounded by some value $c$. *};
+
fix c; assume a: "ALL x:V. rabs (f x) <= c * norm x";
def b == "max c 0r";
- show "EX Y. isUb UNIV (B V norm f) Y";
+ show "?thesis";
proof (intro exI isUbI setleI ballI, unfold B_def,
elim CollectE disjE bexE conjE);
- fix x y; assume "x:V" "x ~= <0>" "y = rabs (f x) * rinv (norm x)";
- from a; have le: "rabs (f x) <= c * norm x"; ..;
- have "y = rabs (f x) * rinv (norm x)";.;
- also; from _ le; have "... <= c * norm x * rinv (norm x)";
- proof (rule real_mult_le_le_mono2);
- show "0r <= rinv (norm x)";
+
+ txt{* To proof the thesis, we have to show that there is
+ some constant b, which is greater than every $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$: *};
+
+ 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
+ $x\in V$ with $x \neq \zero$. *};
+
+ next;
+ fix x y;
+ assume "x:V" "x ~= <0>"; (***
+
+ have ge: "0r <= rinv (norm x)";
+ by (rule real_less_imp_le, rule real_rinv_gt_zero,
+ rule normed_vs_norm_gt_zero); (***
proof (rule real_less_imp_le);
show "0r < rinv (norm x)";
proof (rule real_rinv_gt_zero);
show "0r < norm x"; ..;
qed;
- qed; (*** or:
- by (rule real_less_imp_le, rule real_rinv_gt_zero,
- rule normed_vs_norm_gt_zero); ***)
+ qed; ***)
+ have nz: "norm x ~= 0r";
+ by (rule not_sym, rule lt_imp_not_eq,
+ rule normed_vs_norm_gt_zero); (***
+ proof (rule not_sym);
+ show "0r ~= norm x";
+ proof (rule lt_imp_not_eq);
+ show "0r < norm x"; ..;
+ qed;
+ qed; ***)***)
+
+ txt {* The thesis follows by a short calculation using the
+ fact that $f$ is bounded. *};
+
+ assume "y = rabs (f x) * rinv (norm x)";
+ also; have "... <= c * norm x * rinv (norm x)";
+ proof (rule real_mult_le_le_mono2);
+ show "0r <= rinv (norm x)";
+ by (rule real_less_imp_le, rule real_rinv_gt_zero,
+ rule normed_vs_norm_gt_zero);
+ from a; show "rabs (f x) <= c * norm x"; ..;
qed;
also; have "... = c * (norm x * rinv (norm x))";
by (rule real_mult_assoc);
also; have "(norm x * rinv (norm x)) = 1r";
proof (rule real_mult_inv_right);
- show "norm x ~= 0r";
- proof (rule not_sym);
- show "0r ~= norm x";
- proof (rule lt_imp_not_eq);
- show "0r < norm x"; ..;
- qed;
- qed; (*** or:
- by (rule not_sym, rule lt_imp_not_eq,
- rule normed_vs_norm_gt_zero); ***)
+ show nz: "norm x ~= 0r";
+ by (rule not_sym, rule lt_imp_not_eq,
+ rule normed_vs_norm_gt_zero);
qed;
- also; have "c * ... = c"; by (simp!);
- also; have "... <= b"; by (simp! add: le_max1);
+ also; have "c * ... <= b "; by (simp! add: le_max1);
finally; show "y <= b"; .;
- next;
- fix y; assume "y = 0r"; show "y <= b"; by (simp! add: le_max2);
qed simp;
qed;
qed;
qed;
+text {* The norm of a continous function is always $\geq 0$. *};
+
lemma fnorm_ge_zero [intro!!]:
"[| is_continous V norm f; is_normed_vectorspace V norm|]
==> 0r <= function_norm V norm f";
proof -;
- assume c: "is_continous V norm f" and n: "is_normed_vectorspace V norm";
- have "is_function_norm V norm f (function_norm V norm f)"; ..;
- hence s: "is_Sup UNIV (B V norm f) (function_norm V norm f)";
- by (simp add: is_function_norm_def);
+ assume c: "is_continous V norm f"
+ and n: "is_normed_vectorspace V norm";
+
+ txt {* The function norm is defined as the supremum of $B$.
+ So it is $\geq 0$ if all elements in $B$ are $\geq 0$, provided
+ the supremum exists and $B$ is not empty. *};
+
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; assume "x : V" "x ~= <0>"
- "r = rabs (f x) * rinv (norm x)";
- show "0r <= r";
- proof (simp!, rule real_le_mult_order);
- show "0r <= rabs (f x)"; by (simp! only: rabs_ge_zero);
- show "0r <= rinv (norm x)";
+ proof (intro ballI, unfold B_def,
+ elim CollectE bexE conjE disjE);
+ fix x r;
+ assume "x : V" "x ~= <0>"
+ and r: "r = rabs (f x) * rinv (norm x)";
+
+ have ge: "0r <= rabs (f x)"; by (simp! only: rabs_ge_zero);
+ have "0r <= rinv (norm x)";
+ by (rule real_less_imp_le, rule real_rinv_gt_zero, rule);(***
proof (rule real_less_imp_le);
show "0r < rinv (norm x)";
proof (rule real_rinv_gt_zero);
show "0r < norm x"; ..;
qed;
- qed;
- qed;
+ qed; ***)
+ with ge; show "0r <= r";
+ by (simp only: r,rule real_le_mult_order);
qed (simp!);
- from ex_fnorm [OF n c];
- show "is_Sup UNIV (B V norm f) (Sup UNIV (B V norm f))";
- by (simp! add: is_function_norm_def function_norm_def);
+
+ txt {* Since $f$ is continous 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);
+
+ 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:
+\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";
proof -;
- assume "is_normed_vectorspace V norm" "x:V" and c: "is_continous V norm f";
+ assume "is_normed_vectorspace V norm" "x:V"
+ and c: "is_continous V norm f";
have v: "is_vectorspace V"; ..;
assume "x:V";
+
+ txt{* The proof is by case analysis on $x$. *};
+
show "?thesis";
- proof (rule case_split [of "x = <0>"]);
+ proof (rule case_split);
+
+ txt {* For the case $x = \zero$ the thesis follows
+ from the linearity of $f$: for every linear function
+ holds $f\ap \zero = 0$. *};
+
+ assume "x = <0>";
+ have "rabs (f x) = rabs (f <0>)"; by (simp!);
+ also; from v continous_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);
+ show "0r <= function_norm V norm f"; ..;
+ show "0r <= norm x"; ..;
+ qed;
+ finally;
+ show "rabs (f x) <= function_norm V norm f * norm x"; .;
+
+ next;
assume "x ~= <0>";
- show "?thesis";
- proof -;
- have n: "0r <= norm x"; ..;
- have le: "rabs (f x) * rinv (norm x) <= function_norm V norm f";
- proof (unfold function_norm_def, rule sup_ub);
- from ex_fnorm [OF _ c]; 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] conjI, simp);
- qed;
- have "rabs (f x) = rabs (f x) * 1r"; by (simp!);
- also; have "1r = rinv (norm x) * norm x";
- proof (rule real_mult_inv_left [RS sym]);
- show "norm x ~= 0r";
- proof (rule lt_imp_not_eq[RS not_sym]);
- show "0r < norm x"; ..;
- qed;
- qed;
- also; have "rabs (f x) * ... = rabs (f x) * rinv (norm x) * norm x";
- by (simp! add: real_mult_assoc [of "rabs (f x)"]);
- also; have "rabs (f x) * rinv (norm x) * norm x <= function_norm V norm f * norm x";
- by (rule real_mult_le_le_mono2 [OF n le]);
- finally; show "rabs (f x) <= function_norm V norm f * norm x"; .;
+ have n: "0r <= norm x"; ..;
+ have nz: "norm x ~= 0r";
+ proof (rule lt_imp_not_eq [RS not_sym]);
+ show "0r < norm x"; ..;
qed;
- next;
- assume "x = <0>";
- then; show "?thesis";
- proof -;
- have "rabs (f x) = rabs (f <0>)"; by (simp!);
- also; from v continous_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);
- show "0r <= function_norm V norm f"; ..;
- show "0r <= norm x"; ..;
- qed;
- finally; show "rabs (f x) <= function_norm V norm f * norm x"; .;
+
+ txt {* For the case $x\neq \zero$ we derive the following
+ fact from the definition of the function norm:*};
+
+ have l: "rabs (f x) * rinv (norm x) <= function_norm V norm f";
+ proof (unfold function_norm_def, rule sup_ub);
+ from ex_fnorm [OF _ c];
+ 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]
+ conjI, simp);
qed;
+
+ txt {* The thesis 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";
+ by (rule real_mult_inv_left [RS sym]);
+ also;
+ have "rabs (f x) * ... = rabs (f x) * rinv (norm x) * norm x";
+ by (simp! add: real_mult_assoc [of "rabs (f x)"]);
+ also; have "... <= function_norm V norm f * norm x";
+ by (rule real_mult_le_le_mono2 [OF n l]);
+ finally;
+ show "rabs (f x) <= function_norm V norm f * norm x"; .;
qed;
qed;
+text{* The function norm is the least positive real number for
+which the inequation
+\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;
ALL x:V. rabs (f x) <= c * norm x; 0r <= c |]
@@ -202,42 +322,62 @@
assume c: "is_continous V norm f";
assume fb: "ALL x:V. rabs (f x) <= c * norm x"
and "0r <= c";
+
+ txt {* Suppose the inequation holds for some $c\geq 0$.
+ If $c$ is an upper bound of $B$, then $c$ is greater
+ than the function norm since the function norm is the
+ least upper bound.
+ *};
+
show "Sup UNIV (B V norm f) <= c";
proof (rule sup_le_ub);
from ex_fnorm [OF _ c];
show "is_Sup UNIV (B V norm f) (Sup UNIV (B V norm f))";
by (simp! add: is_function_norm_def function_norm_def);
+
+ txt {* $c$ is an upper bound of $B$, i.~e.~every
+ $y\in B$ is less than $c$. *};
+
show "isUb UNIV (B V norm f) c";
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);
- fix x; assume Px: "x ~= <0> & y = rabs (f x) * rinv (norm x)";
- assume x: "x : V";
- have lt: "0r < norm x"; by (simp! add: normed_vs_norm_gt_zero);
+ proof (unfold B_def, elim CollectE disjE bexE conjE);
+
+ txt {* The first case for $y\in B$ is $y=0$. *};
+
+ assume "y = 0r";
+ show "y <= c"; by (force!);
+
+ txt{* The second case is
+ $y = \frac{|f\ap x|}{\norm x}$ for some
+ $x\in V$ with $x \neq \zero$. *};
+
+ next;
+ fix x;
+ assume "x : V" "x ~= <0>";
+
+ have lz: "0r < norm x";
+ by (simp! add: normed_vs_norm_gt_zero);
- have neq: "norm x ~= 0r";
+ have nz: "norm x ~= 0r";
proof (rule not_sym);
- from lt; show "0r ~= norm x";
- by (simp! add: order_less_imp_not_eq);
+ from lz; show "0r ~= norm x";
+ by (simp! add: order_less_imp_not_eq);
qed;
- from lt; have "0r < rinv (norm x)";
+ from lz; have "0r < rinv (norm x)";
by (simp! add: real_rinv_gt_zero);
- then; have inv_leq: "0r <= rinv (norm x)";
+ hence rinv_gez: "0r <= rinv (norm x)";
by (rule real_less_imp_le);
- from Px; have "y = rabs (f x) * rinv (norm x)"; ..;
- also; from inv_leq; have "... <= c * norm x * rinv (norm x)";
+ assume "y = rabs (f x) * rinv (norm x)";
+ also; from rinv_gez; have "... <= c * norm x * rinv (norm x)";
proof (rule real_mult_le_le_mono2);
- from fb x; show "rabs (f x) <= c * norm x"; ..;
+ show "rabs (f x) <= c * norm x"; by (rule bspec);
qed;
- also; have "... <= c";
- by (simp add: neq real_mult_assoc);
+ also; have "... <= c"; by (simp add: nz real_mult_assoc);
finally; show ?thesis; .;
- next;
- assume "y = 0r";
- show "y <= c"; by (force!);
qed;
qed force;
qed;
--- a/src/HOL/Real/HahnBanach/FunctionOrder.thy Fri Oct 22 18:41:00 1999 +0200
+++ b/src/HOL/Real/HahnBanach/FunctionOrder.thy Fri Oct 22 20:14:31 1999 +0200
@@ -3,28 +3,29 @@
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 *}
+subsection {* The graph of a function *};
+text{* We define the \emph{graph} of a (real) function $f$ with the
+domain $F$ as the set
+\begin{matharray}{l}
+\{(x, f\ap x). \ap x:F\}.
+\end{matharray}
+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.
+*};
-types 'a graph = "('a * real) set";
+types 'a graph = "('a::{minus, plus} * 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} *)
-
-constdefs
- domain :: "'a graph => 'a set"
- "domain g == {x. EX y. (x, y):g}";
-
-constdefs
- funct :: "'a graph => ('a => real)"
- "funct g == %x. (@ y. (x, y):g)";
+ "graph F f == {p. EX x. p = (x, f x) & x:F}"; (*
+ == {(x, f x). x:F} *)
lemma graphI [intro!!]: "x:F ==> (x, f x) : graph F f";
by (unfold graph_def, intro CollectI exI) force;
@@ -38,16 +39,46 @@
lemma graphD2 [intro!!]: "(x, y): graph H h ==> y = h x";
by (unfold graph_def, elim CollectE exE) force;
+subsection {* Functions ordered by domain extension *};
+
+text{* The function $h'$ is an extension of $h$, iff the graph of
+$h$ is a subset of the graph of $h'$.*};
+
+lemma graph_extI:
+ "[| !! x. x: H ==> h x = h' x; H <= H'|]
+ ==> graph H h <= graph H' h'";
+ by (unfold graph_def, force);
+
lemma graph_extD1 [intro!!]:
"[| graph H h <= graph H' h'; x:H |] ==> h x = h' x";
by (unfold graph_def, force);
-lemma graph_extD2 [intro!!]: "[| graph H h <= graph H' h' |] ==> H <= H'";
+lemma graph_extD2 [intro!!]:
+ "[| graph H h <= graph H' h' |] ==> H <= H'";
by (unfold graph_def, force);
-lemma graph_extI:
- "[| !! x. x: H ==> h x = h' x; H <= H'|] ==> graph H h <= graph H' h'";
- by (unfold graph_def, force);
+subsection {* Domain and function of a graph *};
+
+text{* The inverse functions to $\idt{graph}$ are $\idt{domain}$ and
+$\idt{funct}$.*};
+
+constdefs
+ domain :: "'a graph => 'a set"
+ "domain g == {x. EX y. (x, y):g}"
+
+ funct :: "'a graph => ('a => real)"
+ "funct g == \<lambda>x. (SOME y. (x, y):g)";
+
+(*text{* The equations
+\begin{matharray}
+\idt{domain} graph F f = F {\rm and}\\
+\idt{funct} graph F f = f
+\end{matharray}
+hold, but are not proved here.
+*};*)
+
+text {* The following lemma states that $g$ is the graph of a function
+if the relation induced by $g$ is unique. *};
lemma graph_domain_funct:
"(!!x y z. (x, y):g ==> (x, z):g ==> z = y)
@@ -65,46 +96,50 @@
-subsection {* The set of 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
+$E$. The set of all linear extensions of $f$, to superspaces $H$ of
+$F$, which are bounded by $p$, is defined as follows. *};
constdefs
norm_pres_extensions ::
- "['a set, 'a => real, 'a set, 'a => real] => 'a graph set"
- "norm_pres_extensions E p F f == {g. EX H h. graph H h = g
- & 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)}";
+ "['a::{minus, plus} set, 'a => real, 'a set, 'a => real]
+ => 'a graph set"
+ "norm_pres_extensions E p F f
+ == {g. EX H h. graph H h = g
+ & 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)}";
lemma norm_pres_extension_D:
- "(g: norm_pres_extensions E p F f) ==> (EX H h. graph H h = g
- & 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))";
- by (unfold norm_pres_extensions_def) force;
+ "g : norm_pres_extensions E p F f
+ ==> EX H h. graph H h = g
+ & 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)";
+ by (unfold norm_pres_extensions_def) force;
lemma norm_pres_extensionI2 [intro]:
- "[| 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) |]
- ==> (graph H h : norm_pres_extensions E p F f)";
+ "[| 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 |]
+ ==> (graph H h : norm_pres_extensions E p F f)";
by (unfold norm_pres_extensions_def) force;
lemma norm_pres_extensionI [intro]:
- "(EX H h. graph H h = g
- & 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))
- ==> (g: norm_pres_extensions E p F f) ";
- by (unfold norm_pres_extensions_def) force;
+ "EX H h. graph H h = g
+ & 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)
+ ==> g: norm_pres_extensions E p F f";
+ by (unfold norm_pres_extensions_def) force;
end;
--- a/src/HOL/Real/HahnBanach/HahnBanach.thy Fri Oct 22 18:41:00 1999 +0200
+++ b/src/HOL/Real/HahnBanach/HahnBanach.thy Fri Oct 22 20:14:31 1999 +0200
@@ -1,23 +1,25 @@
(* Title: HOL/Real/HahnBanach/HahnBanach.thy
ID: $Id$
- Author: Gertrud Bauer, TU Munich
+ Author: Gertrud Baueer, TU Munich
*)
-header {* The Hahn-Banach theorem *};
+header {* The Hahn-Banach Theorem *};
-theory HahnBanach = HahnBanach_lemmas + HahnBanach_h0_lemmas:;
+theory HahnBanach
+ = HahnBanachSupLemmas + HahnBanachExtLemmas + ZornLemma:;
text {*
- The proof of two different versions of the Hahn-Banach theorem,
- following \cite{Heuser}.
+ We present the proof of two different versions of the Hahn-Banach
+ Theorem, closely following \cite{Heuser:1986}.
*};
-subsection {* The Hahn-Banach theorem for general linear spaces *};
+subsection {* The case of general linear spaces *};
-text {* Every linear function f on a subspace of E, which is bounded by a
- quasinorm on E, can be extended norm preserving to a function on E *};
+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. *};
-theorem hahnbanach:
+theorem HahnBanach:
"[| is_vectorspace E; is_subspace F E; is_quasinorm E p;
is_linearform F f; ALL x:F. f x <= p x |]
==> EX h. is_linearform E h
@@ -27,52 +29,60 @@
assume "is_vectorspace E" "is_subspace F E" "is_quasinorm 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
+ of $f$ to superspaces of $F$, which are bounded by $p$. *};
+
def M == "norm_pres_extensions E p F f";
+
+ txt{* We show that $M$ is non-empty: *};
have aM: "graph F f : norm_pres_extensions E p F f";
proof (rule norm_pres_extensionI2);
- show "is_subspace F F";
- proof;
- show "is_vectorspace F"; ..;
- qed;
+ have "is_vectorspace F"; ..;
+ thus "is_subspace F F"; ..;
qed (blast!)+;
- subsubsect {* Existence of a supremum of the norm preserving functions *};
+ subsubsect {* Existence of a limit function of the norm preserving
+ extensions *};
- have "!! (c:: 'a graph set). c : chain M ==> EX x. x:c
- ==> (Union c) : M";
+ 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.
+ It is even the least upper bound, because every upper bound of $M$
+ is also an upper bound for $\cup\; c$.) *};
+
+ have "!! c. [| c : chain M; EX x. x:c |] ==> Union c : M";
proof -;
- fix c; assume "c:chain M"; assume "EX x. x:c";
- show "(Union c) : M";
+ fix c; assume "c:chain M" "EX x. x:c";
+ show "Union c : M";
proof (unfold M_def, rule norm_pres_extensionI);
show "EX (H::'a set) h::'a => real. graph H h = Union c
& is_linearform H h
& is_subspace H E
& is_subspace F H
- & (graph F f <= graph H h)
- & (ALL x::'a:H. h x <= p x)"
- (is "EX (H::'a set) h::'a => real. ?Q H h");
+ & graph F f <= graph H h
+ & (ALL x::'a:H. h x <= p x)";
proof (intro exI conjI);
let ?H = "domain (Union c)";
let ?h = "funct (Union c)";
- show a: "graph ?H ?h = Union c";
+ show a [simp]: "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_uniq);
+ show "z = y"; by (rule sup_definite);
qed;
- show "is_linearform ?H ?h";
- by (simp! add: sup_lf a);
+ show "is_linearform ?H ?h";
+ by (simp! add: sup_lf a);
- show "is_subspace ?H E";
+ show "is_subspace ?H E";
by (rule sup_subE, rule a) (simp!)+;
- show "is_subspace F ?H";
+ show "is_subspace F ?H";
by (rule sup_supF, rule a) (simp!)+;
- show "graph F f <= graph ?H ?h";
+ show "graph F f <= graph ?H ?h";
by (rule sup_ext, rule a) (simp!)+;
show "ALL x::'a:?H. ?h x <= p x";
@@ -81,7 +91,8 @@
qed;
qed;
- txt {* there exists a maximal norm-preserving function g. *};
+ txt {* According to Zorn's Lemma there exists
+ a maximal norm-preserving extension $g\in M$. *};
with aM; have bex_g: "EX g:M. ALL x:M. g <= x --> g = x";
by (simp! add: Zorn's_Lemma);
@@ -90,204 +101,200 @@
proof;
fix g; assume g: "g:M" "ALL x:M. g <= x --> g = x";
- have ex_Hh: "EX H h. graph H h = g
- & 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) ";
+ have ex_Hh:
+ "EX H h. graph H h = g
+ & 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) ";
by (simp! add: norm_pres_extension_D);
thus ?thesis;
- proof (elim exE conjE);
+ proof (elim exE conjE, intro exI);
fix H h;
assume "graph H h = g" "is_linearform (H::'a set) h"
"is_subspace H E" "is_subspace F H"
- and h_ext: "(graph F f <= graph H h)"
- and h_bound: "ALL x:H. h x <= p x";
+ and h_ext: "graph F f <= graph H h"
+ and h_bound: "ALL x:H. h x <= p x";
- show ?thesis;
- proof;
- have h: "is_vectorspace H"; ..;
- have f: "is_vectorspace F"; ..;
+ have h: "is_vectorspace H"; ..;
+ have f: "is_vectorspace F"; ..;
-subsubsect {* The supremal norm-preserving function is defined on the
- whole vectorspace *};
+subsubsect {* The domain of the limit function. *};
have eq: "H = E";
proof (rule classical);
-txt {* assume h is not defined on whole E *};
-
+txt {* Assume the domain of the supremum is not $E$. *};
+;
assume "H ~= E";
- show ?thesis;
- proof -;
-
- have "EX x:M. g <= x & g ~= x";
- proof -;
-
- txt {* h can be extended norm-preserving to H0 *};
+ have "H <= E"; ..;
+ hence "H < E"; ..;
+
+ txt{* Then there exists an element $x_0$ in
+ the difference of $E$ and $H$. *};
- have "EX H0 h0. g <= graph H0 h0 & g ~= graph H0 h0
- & graph H0 h0 : M";
- proof-;
- have "H <= E"; ..;
- hence "H < E"; ..;
- hence "EX x0:E. x0~:H";
- by (rule set_less_imp_diff_not_empty);
- thus ?thesis;
- proof;
- fix x0; assume "x0:E" "x0~:H";
-
- have x0: "x0 ~= <0>";
- proof (rule classical);
- presume "x0 = <0>";
- with h; have "x0:H"; by simp;
- thus ?thesis; by contradiction;
- qed force;
+ hence "EX x0:E. x0~:H";
+ by (rule set_less_imp_diff_not_empty);
- def H0 == "vectorspace_sum H (lin x0)";
- have "EX h0. g <= graph H0 h0 & g ~= graph H0 h0
- & graph H0 h0 : M";
- proof -;
- from h;
- have xi: "EX xi. (ALL y:H. - p (y [+] x0) - h y <= xi)
- & (ALL y:H. xi <= p (y [+] x0) - h y)";
- proof (rule ex_xi);
- fix u v; assume "u:H" "v:H";
- show "- p (u [+] x0) - h u <= p (v [+] x0) - h v";
- proof (rule real_diff_ineq_swap);
+ txt {* We get that $h$ can be extended in a
+ norm-preserving way to some $H_0$. *};
+;
+ hence "EX H0 h0. g <= graph H0 h0 & g ~= graph H0 h0
+ & graph H0 h0 : M";
+ proof;
+ fix x0; assume "x0:E" "x0~:H";
- show "h v - h u <= p (v [+] x0) + p (u [+] x0)";
- proof -;
- from h; have "h v - h u = h (v [-] u)";
- by (simp! add: linearform_diff_linear);
- also; from h_bound; have "... <= p (v [-] u)";
- by (simp!);
- also;
- have "v [-] u = x0 [+] [-] x0 [+] v [+] [-] u";
- by (unfold diff_def) (simp!);
- also; have "... = v [+] x0 [+] [-] (u [+] x0)";
- by (simp!);
- also; have "... = (v [+] x0) [-] (u [+] x0)";
- by (unfold diff_def) (simp!);
- also; have "p ... <= p (v [+] x0) + p (u [+] x0)";
- by (rule quasinorm_diff_triangle_ineq)
- (simp!)+;
- finally; show ?thesis; .;
- qed;
- qed;
- qed;
-
- thus ?thesis;
- 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)";
- def h0 ==
- "%x. let (y,a) = @(y,a). (x = y [+] a [*] x0 & y:H )
- in (h y) + a * xi";
+ have x0: "x0 ~= <0>";
+ proof (rule classical);
+ presume "x0 = <0>";
+ with h; have "x0:H"; by simp;
+ thus ?thesis; by contradiction;
+ qed blast;
+
+ txt {* Define $H_0$ as the (direct) sum of H and the
+ linear closure of $x_0$.*};
+
+ def H0 == "H + lin x0";
- have "graph H h <= graph H0 h0";
- proof (rule graph_extI);
- fix t; assume "t:H";
- show "h t = h0 t";
- proof -;
- have "(@ (y, a). t = y [+] a [*] x0 & y : H)
- = (t,0r)";
- by (rule decomp1, rule x0);
- thus ?thesis; by (simp! add: Let_def);
- qed;
- next;
- show "H <= H0";
- proof (rule subspace_subset);
- show "is_subspace H H0";
- proof (unfold H0_def, rule subspace_vs_sum1);
- show "is_vectorspace H"; ..;
- show "is_vectorspace (lin x0)"; ..;
- qed;
- qed;
- qed;
- thus "g <= graph H0 h0"; by (simp!);
-
- have "graph H h ~= graph H0 h0";
- proof;
- assume e: "graph H h = graph H0 h0";
- have "x0:H0";
- proof (unfold H0_def, rule vs_sumI);
- show "x0 = <0> [+] x0"; by (simp!);
- show "x0 :lin x0"; by (rule x_lin_x);
- from h; show "<0> : H"; ..;
- qed;
- hence "(x0, h0 x0) : graph H0 h0"; by (rule graphI);
- with e; have "(x0, h0 x0) : graph H h"; by simp;
- hence "x0 : H"; ..;
- thus "False"; by contradiction;
- qed;
- thus "g ~= graph H0 h0"; by (simp!);
-
- 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!)+;
+ from h; have xi: "EX xi. (ALL y:H. - p (y + x0) - h y <= xi)
+ & (ALL y:H. 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);
+ also; from h_bound; have "... <= p (v - u)";
+ by (simp!);
+ also; have "v - u = x0 + - x0 + v + - u";
+ by (simp! add: diff_eq1);
+ also; have "... = v + x0 + - (u + x0)";
+ by (simp!);
+ 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!)+;
+ finally; have "h v - h u <= p (v + x0) + p (u + x0)"; .;
- show "is_subspace H0 E";
- by (unfold H0_def, rule vs_sum_subspace,
- rule lin_subspace);
+ thus "- p (u + x0) - h u <= p (v + x0) - h v";
+ by (rule real_diff_ineq_swap);
+ qed;
+ hence "EX h0. g <= graph H0 h0 & g ~= graph H0 h0
+ & 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)";
+
+ txt {* Define $h_0$ as the linear extension of $h$ on $H_0$:*};
- show f_h0: "is_subspace F H0";
- proof (rule subspace_trans [of F H H0]);
- from h lin_vs;
- have "is_subspace H (vectorspace_sum H (lin x0))";
- ..;
- thus "is_subspace H H0"; by (unfold H0_def);
- qed;
-
- show "graph F f <= graph H0 h0";
- proof (rule graph_extI);
- fix x; assume "x:F";
- show "f x = h0 x";
- proof -;
- have eq:
- "(@(y, a). x = y [+] a [*] x0 & y : H)
- = (x, 0r)";
- by (rule decomp1, rule x0) (simp!)+;
+ def h0 ==
+ "\<lambda>x. let (y,a) = SOME (y, a). (x = y + a <*> x0 & y:H)
+ in (h y) + a * xi";
- have "f x = h x"; ..;
- also; have " ... = h x + 0r * xi"; by simp;
- also; have
- "... = (let (y,a) = (x, 0r) in h y + a * xi)";
- by (simp add: Let_def);
- also; from eq; have
- "... = (let (y,a) = @ (y,a).
- x = y [+] a [*] x0 & y : H
- in h y + a * xi)"; by simp;
- also; have "... = h0 x"; by (simp!);
- finally; show ?thesis; .;
- qed;
- next;
- from f_h0; show "F <= H0"; ..;
- qed;
-
- show "ALL x:H0. h0 x <= p x";
- by (rule h0_norm_pres, rule x0)
- (assumption | (simp!))+;
- qed;
- thus "graph H0 h0 : M"; by (simp!);
- qed;
+ txt {* We get that the graph of $h_0$ extend that of
+ $h$. *};
+
+ have "graph H h <= graph H0 h0";
+ proof (rule graph_extI);
+ fix t; assume "t:H";
+ have "(SOME (y, a). t = y + a <*> x0 & y : H) = (t,0r)";
+ by (rule decomp_H0_H, rule x0);
+ thus "h t = h0 t"; by (simp! add: Let_def);
+ next;
+ show "H <= H0";
+ proof (rule subspace_subset);
+ show "is_subspace H H0";
+ proof (unfold H0_def, rule subspace_vs_sum1);
+ show "is_vectorspace H"; ..;
+ show "is_vectorspace (lin x0)"; ..;
qed;
- thus ?thesis; ..;
qed;
qed;
+ thus "g <= graph H0 h0"; by (simp!);
- thus ?thesis;
- by (elim exE conjE, intro bexI conjI);
+ txt {* Apparently $h_0$ is not equal to $h$. *};
+
+ have "graph H h ~= graph H0 h0";
+ proof;
+ assume e: "graph H h = graph H0 h0";
+ have "x0 : H0";
+ proof (unfold H0_def, rule vs_sumI);
+ show "x0 = <0> + x0"; by (simp!);
+ from h; show "<0> : H"; ..;
+ show "x0 : lin x0"; by (rule x_lin_x);
+ qed;
+ hence "(x0, h0 x0) : graph H0 h0"; ..;
+ with e; have "(x0, h0 x0) : graph H h"; by simp;
+ hence "x0 : H"; ..;
+ thus False; by contradiction;
+ qed;
+ thus "g ~= graph H0 h0"; by (simp!);
+
+ 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);
+
+ have "is_subspace F H"; .;
+ also; from h lin_vs;
+ have [fold H0_def]: "is_subspace H (H + lin x0)"; ..;
+ finally (subspace_trans [OF _ h]);
+ show f_h0: "is_subspace F H0"; .; (***
+ backwards:
+ show f_h0: "is_subspace F H0"; .;
+ proof (rule subspace_trans [of F H H0]);
+ from h lin_vs;
+ have "is_subspace H (H + lin x0)"; ..;
+ thus "is_subspace H H0"; by (unfold H0_def);
+ qed; ***)
+
+ show "graph F f <= graph H0 h0";
+ proof (rule graph_extI);
+ fix x; assume "x:F";
+ have "f x = h x"; ..;
+ also; have " ... = h x + 0r * xi"; by simp;
+ also; have "... = (let (y,a) = (x, 0r) in h y + a * xi)";
+ by (simp add: Let_def);
+ also; have
+ "(x, 0r) = (SOME (y, a). x = y + a <*> x0 & y : H)";
+ by (rule decomp_H0_H [RS sym], rule x0) (simp!)+;
+ also; have
+ "(let (y,a) = (SOME (y,a). x = y + a <*> x0 & y : H)
+ in h y + a * xi)
+ = h0 x"; by (simp!);
+ finally; show "f x = h0 x"; .;
+ next;
+ from f_h0; show "F <= H0"; ..;
+ qed;
+
+ show "ALL x:H0. h0 x <= p x";
+ by (rule h0_norm_pres, rule x0) (assumption | (simp!))+;
+ qed;
+ thus "graph H0 h0 : M"; by (simp!);
qed;
- hence "~ (ALL x:M. g <= x --> g = x)"; by force;
- thus ?thesis; by contradiction;
+ thus ?thesis; ..;
qed;
+
+ txt {* We have shown, that $h$ can still be extended to
+ some $h_0$, in contradiction to the assumption that
+ $h$ is a maximal element. *};
+
+ hence "EX x:M. g <= x & g ~= x";
+ by (elim exE conjE, intro bexI conjI);
+ hence "~ (ALL x:M. g <= x --> g = x)"; by simp;
+ thus ?thesis; by contradiction;
qed;
+txt{* It follows $H = E$ and the thesis can be shown. *};
+
show "is_linearform E h & (ALL x:F. h x = f x)
& (ALL x:E. h x <= p x)";
proof (intro conjI);
@@ -297,15 +304,26 @@
fix x; assume "x:F"; show "f x = h x "; ..;
qed;
from eq; show "ALL x:E. h x <= p x"; by (force!);
-qed;
-qed;
-qed;
-qed;
+qed;
+
+qed;
+qed;
qed;
-subsection {* Alternative formulation of the theorem *};
+
+
+subsection {* An alternative formulation of the theorem *};
-theorem rabs_hahnbanach:
+text {* The following alternative formulation of the
+Hahn-Banach Theorem uses the fact that for
+real numbers the following inequations are equivalent:
+\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_linearform F f; ALL x:F. rabs (f x) <= p x |]
==> EX g. is_linearform E g
@@ -314,141 +332,191 @@
proof -;
assume e: "is_vectorspace E" "is_subspace F E" "is_quasinorm 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 [RS iffD1]);
+ have "ALL x:F. f x <= p x";
+ by (rule rabs_ineq_iff [RS iffD1]);
hence "EX g. is_linearform E g & (ALL x:F. g x = f x)
& (ALL x:E. g x <= p x)";
- by (simp! only: hahnbanach);
+ by (simp! only: HahnBanach);
thus ?thesis;
proof (elim exE conjE);
fix g; assume "is_linearform E g" "ALL x:F. g x = f x"
"ALL x:E. g x <= p x";
show ?thesis;
- proof (intro exI conjI)+;
+ proof (intro exI conjI);
from e; show "ALL x:E. rabs (g x) <= p x";
- by (simp! add: rabs_ineq [OF subspace_refl]);
+ by (simp! add: rabs_ineq_iff [OF subspace_refl]);
qed;
qed;
qed;
-subsection {* The Hahn-Banach theorem for normed spaces *};
+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 norm *};
+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. *};
-theorem norm_hahnbanach:
- "[| is_normed_vectorspace E norm; is_subspace F E; is_linearform F f;
- is_continous F norm f |]
+theorem norm_HahnBanach:
+ "[| is_normed_vectorspace E norm; is_subspace F E;
+ is_linearform F f; is_continous F norm f |]
==> EX g. is_linearform E g
& is_continous E norm g
& (ALL x:F. g x = f x)
- & function_norm E norm g = function_norm F norm f"
- (concl is "EX g::'a=>real. ?P g");
+ & function_norm E norm g = function_norm F norm f";
proof -;
- assume a: "is_normed_vectorspace E norm";
- assume b: "is_subspace F E" "is_linearform F f";
- assume c: "is_continous F norm f";
+ 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";
have e: "is_vectorspace E"; ..;
- from _ e; have f: "is_normed_vectorspace F norm"; ..;
+ with _; have f_norm: "is_normed_vectorspace F norm"; ..;
- def p == "%x::'a. (function_norm F norm f) * norm x";
+ txt{* We define the function $p$ on $E$ as follows:
+ \begin{matharray}{l}
+ p\ap x = \fnorm f * \norm x\\
+ % p\ap x = \fnorm f * \fnorm x.\\
+ \end{matharray}
+ *};
+
+ def p == "\<lambda>x. function_norm F norm f * norm x";
- let ?P' = "%g. is_linearform E g & (ALL x:F. g x = f x)
- & (ALL x:E. rabs (g x) <= p x)";
+ txt{* $p$ is a quasinorm on $E$: *};
have q: "is_quasinorm E p";
proof;
fix x y a; assume "x:E" "y:E";
+ txt{* $p$ is positive definite: *};
+
show "0r <= p x";
proof (unfold p_def, rule real_le_mult_order);
- from _ f; show "0r <= function_norm F norm f"; ..;
+ from _ f_norm; show "0r <= function_norm F norm f"; ..;
show "0r <= norm x"; ..;
qed;
- show "p (a [*] x) = (rabs a) * (p x)";
+ txt{* $p$ is multiplicative: *};
+
+ show "p (a <*> x) = rabs a * p x";
proof -;
- have "p (a [*] x) = (function_norm F norm f) * norm (a [*] x)";
+ have "p (a <*> x) = function_norm F norm f * norm (a <*> x)";
by (simp!);
- also; have "norm (a [*] x) = rabs a * norm x";
+ also; have "norm (a <*> x) = rabs a * norm x";
by (rule normed_vs_norm_mult_distrib);
- also; have "(function_norm F norm f) * ...
- = rabs a * ((function_norm F norm f) * norm x)";
+ 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);
- also; have "... = (rabs a) * (p x)"; by (simp!);
+ also; have "... = rabs a * p x"; by (simp!);
finally; show ?thesis; .;
qed;
- show "p (x [+] y) <= p x + p y";
+ txt{* Furthermore $p$ obeys the triangle inequation: *};
+
+ show "p (x + y) <= p x + p y";
proof -;
- have "p (x [+] y) = (function_norm F norm f) * norm (x [+] y)";
+ have "p (x + y) = function_norm F norm f * norm (x + y)";
by (simp!);
- also; have "... <= (function_norm F norm f) * (norm x + norm y)";
+ also;
+ have "... <= function_norm F norm f * (norm x + norm y)";
proof (rule real_mult_le_le_mono1);
- from _ f; show "0r <= function_norm F norm f"; ..;
- show "norm (x [+] y) <= norm x + norm y"; ..;
+ from _ f_norm; show "0r <= function_norm F norm f"; ..;
+ show "norm (x + y) <= norm x + norm y"; ..;
qed;
- also; have "... = (function_norm F norm f) * (norm x)
- + (function_norm F norm f) * (norm y)";
+ also; have "... = function_norm F norm f * norm x
+ + function_norm F norm f * norm y";
by (simp! only: real_add_mult_distrib2);
finally; show ?thesis; by (simp!);
qed;
qed;
-
+
+ txt{* $f$ is bounded by $p$. *};
+
have "ALL x:F. rabs (f x) <= p x";
proof;
fix x; assume "x:F";
- from f; show "rabs (f x) <= p x";
+ from f_norm; show "rabs (f x) <= p x";
by (simp! add: norm_fx_le_norm_f_norm_x);
qed;
- with e b q; have "EX g. ?P' g";
- by (simp! add: rabs_hahnbanach);
+ 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
+ $g$ on the whole vector space $E$. *};
- thus "?thesis";
- proof (elim exE conjE, intro exI conjI);
+ with e f q;
+ have "EX g. is_linearform E g & (ALL x:F. g x = f x)
+ & (ALL x:E. rabs (g x) <= p x)";
+ by (simp! add: rabs_HahnBanach);
+
+ thus ?thesis;
+ 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";
- show ce: "is_continous E norm g";
- proof (rule lipschitz_continousI);
- fix x; assume "x:E";
- show "rabs (g x) <= function_norm F norm f * norm x";
- by (rule bspec [of _ _ x], (simp!));
- qed;
- show "function_norm E norm g = function_norm F norm f";
- proof (rule order_antisym);
- from _ ce;
- show "function_norm E norm g <= function_norm F norm f";
- proof (rule fnorm_le_ub);
- show "ALL x:E. rabs (g x) <= function_norm F norm f * norm x";
+
+ show "EX g. is_linearform E g
+ & is_continous 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$. *};
+
+ show g_cont: "is_continous E norm g";
+ proof;
+ fix x; assume "x:E";
+ show "rabs (g x) <= function_norm F norm f * norm x";
+ by (rule bspec [of _ _ x], (simp!));
+ qed;
+
+ 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
+ \begin{matharray}{l}
+ \forall\ap x\in E.\ap |g\ap x| \leq c * \norm x.
+ \end{matharray} *};
+
+ have "ALL x:E. rabs (g x) <= function_norm F norm f * norm x";
proof;
fix x; assume "x:E";
show "rabs (g x) <= function_norm F norm f * norm x";
- by (rule bspec [of _ _ x], (simp!));
+ by (simp!);
qed;
- from c f; show "0r <= function_norm F norm f"; ..;
- qed;
- show "function_norm F norm f <= function_norm E norm g";
- proof (rule fnorm_le_ub);
- show "ALL x:F. rabs (f x) <= function_norm E norm g * norm x";
+
+ 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";
+ proof (rule fnorm_le_ub);
+ from f_cont f_norm; show "0r <= function_norm F norm f"; ..;
+ qed;
+
+ txt{* The other direction is achieved by a similar
+ argument. *};
+
+ have "ALL x:F. rabs (f x) <= function_norm E norm g * norm x";
proof;
fix x; assume "x : F";
from a; have "g x = f x"; ..;
hence "rabs (f x) = rabs (g x)"; by simp;
- also; from _ _ ce;
- have "... <= function_norm E norm g * norm x";
- proof (rule norm_fx_le_norm_f_norm_x);
- show "x : E";
- proof (rule subsetD);
- show "F <= E"; ..;
- qed;
- qed;
+ also; from _ _ g_cont;
+ have "... <= function_norm E norm g * norm x";
+ by (rule norm_fx_le_norm_f_norm_x) (simp!)+;
finally;
show "rabs (f x) <= function_norm E norm g * norm x"; .;
qed;
- from _ e; show "is_normed_vectorspace F norm"; ..;
- from ce; show "0r <= function_norm E norm g"; ..;
+
+ with f_norm f_cont; show "?R <= ?L";
+ proof (rule fnorm_le_ub);
+ from g_cont; show "0r <= function_norm E norm g"; ..;
+ qed;
qed;
qed;
qed;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Real/HahnBanach/HahnBanachExtLemmas.thy Fri Oct 22 20:14:31 1999 +0200
@@ -0,0 +1,346 @@
+(* Title: HOL/Real/HahnBanach/HahnBanachExtLemmas.thy
+ ID: $Id$
+ Author: Gertrud Bauer, TU Munich
+*)
+
+header {* Extending a non-ma\-xi\-mal function *};
+
+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
+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
+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$.
+
+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
+\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}
+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}
+*};
+
+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)";
+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. *};
+
+ let ?S = "{s::real. EX u:F. s = a u}";
+
+ have "EX xi. isLub UNIV ?S xi";
+ proof (rule reals_complete);
+
+ 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$. *};
+
+ show "EX Y. isUb UNIV ?S Y";
+ proof;
+ show "isUb UNIV ?S (b <0>)";
+ proof (intro isUbI setleI ballI);
+
+ 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"; ..;
+ thus "y <= b <0>";
+ proof;
+ 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)";
+ proof (elim exE);
+ fix xi; assume "isLub UNIV ?S xi";
+ show ?thesis;
+ proof (intro exI conjI ballI);
+
+ txt {* For all $y\in F$ is $a\ap y \leq \xi$. *};
+
+ fix y; assume y: "y:F";
+ show "a y <= xi";
+ proof (rule isUbD);
+ show "isUb UNIV ?S xi"; ..;
+ qed (force!);
+ next;
+
+ txt {* For all $y\in F$ is $\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 "ALL ya : ?S. ya <= b y";
+ proof;
+ fix au; assume au: "au : ?S ";
+ hence "EX u:F. au = a u"; ..;
+ thus "au <= b y";
+ proof;
+ fix u; assume "u:F"; assume "au = a u";
+ also; have "... <= b y"; by (rule r);
+ finally; show ?thesis; .;
+ qed;
+ qed;
+ qed;
+ qed;
+ qed;
+qed;
+
+text{* The function $h_0$ is defined as a linear extension of $h$
+to $H_0$. $h_0$ is linear. *};
+
+lemma h0_lf:
+ "[| 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;
+ 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
+ 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";
+
+ have h0: "is_vectorspace H0";
+ proof (simp only: H0_def, rule vs_sum_vs);
+ show "is_subspace (lin x0) E"; ..;
+ qed;
+
+ show ?thesis;
+ 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.~
+ $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$. *};
+
+ have x1x2: "x1 + x2 : H0";
+ 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;
+ 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;
+ 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;
+
+ from ex_x1 ex_x2 ex_x1x2;
+ show "h0 (x1 + x2) = h0 x1 + h0 x2";
+ proof (elim exE conjE);
+ fix y1 y2 y a1 a2 a;
+ assume y1: "x1 = y1 + a1 <*> x0" and y1': "y1 : H"
+ and y2: "x2 = y2 + a2 <*> x0" and y2': "y2 : H"
+ and y: "x1 + x2 = y + a <*> x0" and y': "y : H";
+
+ have ya: "y1 + y2 = y & a1 + a2 = a";
+ proof (rule decomp_H0);
+ show "y1 + y2 + (a1 + a2) <*> x0 = y + a <*> x0";
+ by (simp! add: vs_add_mult_distrib2 [of E]);
+ show "y1 + y2 : H"; ..;
+ qed;
+
+ have "h0 (x1 + x2) = h y + a * xi";
+ by (rule h0_definite);
+ also; have "... = h (y1 + y2) + (a1 + a2) * xi";
+ 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]
+ real_add_mult_distrib);
+ also; have "... = (h y1 + a1 * xi) + (h y2 + a2 * xi)";
+ by simp;
+ also; have "h y1 + a1 * xi = h0 x1";
+ by (rule h0_definite [RS sym]);
+ also; have "h y2 + a2 * xi = h0 x2";
+ by (rule h0_definite [RS sym]);
+ finally; show ?thesis; .;
+ qed;
+
+ txt{* We further have to show that $h_0$ is linear
+ w.~r.~t.~scalar multiplication,
+ i.~e.~ $c\in real$ $h_0\ap (c \mult x_1) = c \cdot h_0\ap x_1$
+ for $x\in H$ and real $c$.
+ *};
+
+ 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];
+
+ with ex_x1; 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"
+ and y: "c <*> x1 = y + a <*> x0" and y': "y : H";
+
+ have ya: "c <*> y1 = y & c * a1 = a";
+ proof (rule decomp_H0);
+ show "c <*> y1 + (c * a1) <*> x0 = y + a <*> x0";
+ by (simp! add: add: vs_add_mult_distrib1);
+ show "c <*> y1 : H"; ..;
+ qed;
+
+ have "h0 (c <*> x1) = h y + a * xi";
+ by (rule h0_definite);
+ 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]);
+ 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";
+ by (rule h0_definite [RS sym]);
+ finally; show ?thesis; .;
+ qed;
+ qed;
+qed;
+
+text{* $h_0$ is bounded by the quasinorm $p$. *};
+
+lemma h0_norm_pres:
+ "[| 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;
+ 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
+ in (h y) + a * xi)"
+ 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";
+ 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;
+ have "EX y a. x = y + a <*> x0 & y : H";
+ by (rule ex_x);
+ thus "h0 x <= p x";
+ proof (elim exE conjE);
+ fix y a; assume x: "x = y + a <*> x0" and y: "y : H";
+ have "h0 x = h y + a * xi";
+ by (rule h0_definite);
+
+ txt{* Now we show
+ $h\ap y + a * xi\leq p\ap (y\plus a \mult x_0)$
+ by case analysis on $a$. *};
+
+ also; have "... <= p (y + a <*> x0)";
+ proof (rule linorder_linear_split);
+
+ 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
+ $\frac{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. *};
+
+ hence "a * xi
+ <= a * (- p (rinv a <*> y + x0) - h (rinv a <*> y))";
+ by (rule real_mult_less_le_anti [OF lz]);
+ also; have "... = - a * (p (rinv a <*> y + x0))
+ - a * (h (rinv a <*> y))";
+ 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);
+ 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]);
+ 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 $\frac{y}{a}$. *};
+ next;
+ assume gz: "0r < a"; hence nz: "a ~= 0r"; by simp;
+ have "xi <= p (rinv a <*> y + x0) - h (rinv a <*> y)";
+ by (rule bspec [OF a2]) (simp!);
+
+ txt {* The thesis follows by a short calculation. *};
+
+ with gz; have "a * xi
+ <= a * (p (rinv a <*> y + x0) - h (rinv a <*> y))";
+ by (rule real_mult_less_le_mono);
+ also; have "... = a * p (rinv a <*> y + x0)
+ - a * h (rinv a <*> y)";
+ by (rule real_mult_diff_distrib2);
+ 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);
+ 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]);
+ 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;
+ qed;
+ also; from x; have "... = p x"; by simp;
+ finally; show ?thesis; .;
+ qed;
+qed blast+;
+
+
+end;
\ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Real/HahnBanach/HahnBanachSupLemmas.thy Fri Oct 22 20:14:31 1999 +0200
@@ -0,0 +1,692 @@
+(* Title: HOL/Real/HahnBanach/HahnBanachSupLemmas.thy
+ ID: $Id$
+ Author: Gertrud Bauer, TU Munich
+*)
+
+header {* The supremum w.r.t.~the function order *};
+
+theory HahnBanachSupLemmas = FunctionNorm + ZornLemma:;
+
+
+
+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 $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
+$\cup\; 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$.
+*};
+
+(***
+lemma some_H'h't:
+ "[| M = norm_pres_extensions E p F f; c: chain M;
+ 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'
+ & (ALL x:H'. h' x <= p x)";
+proof -;
+ assume m: "M = norm_pres_extensions E p F f" and cM: "c: chain M"
+ and u: "graph H h = Union c" "x:H";
+
+ let ?P = "\<lambda>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)";
+
+ have "EX t : graph H h. t = (x, h x)";
+ by (rule graphI2);
+ thus ?thesis;
+ proof (elim bexE);
+ fix t; assume t: "t : graph H h" "t = (x, h x)";
+ with u; have ex1: "EX g:c. t:g";
+ by (simp only: Union_iff);
+ thus ?thesis;
+ proof (elim bexE);
+ fix g; assume g: "g:c" "t:g";
+ from cM; have "c <= M"; by (rule chainD2);
+ hence "g : M"; ..;
+ hence "g : norm_pres_extensions E p F f"; by (simp only: m);
+ hence "EX H' h'. graph H' h' = g & ?P H' h'";
+ by (rule norm_pres_extension_D);
+ thus ?thesis;
+ by (elim exE conjE, intro exI conjI) (simp | simp!)+;
+ qed;
+ qed;
+qed;
+***)
+
+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|]
+ ==> 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'
+ & (ALL x:H'. h' x <= p x)";
+proof -;
+ assume m: "M = norm_pres_extensions E p F f" and "c: chain M"
+ and u: "graph H h = Union c" "x:H";
+
+ have h: "(x, h x) : graph H h"; ..;
+ with u; have "(x, h x) : Union c"; by simp;
+ hence ex1: "EX g:c. (x, h x) : g";
+ by (simp only: Union_iff);
+ thus ?thesis;
+ proof (elim bexE);
+ fix g; assume g: "g:c" "(x, h x) : g";
+ have "c <= M"; by (rule chainD2);
+ hence "g : M"; ..;
+ hence "g : norm_pres_extensions E p F f"; by (simp only: m);
+ hence "EX H' h'. graph H' h' = g
+ & 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)";
+ by (rule norm_pres_extension_D);
+ thus ?thesis;
+ proof (elim exE conjE);
+ fix H' h';
+ assume "graph H' h' = g" "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";
+ show ?thesis;
+ proof (intro exI conjI);
+ show "graph H' h' : c"; by (simp!);
+ show "(x, h x) : graph H' h'"; by (simp!);
+ qed;
+ qed;
+ qed;
+qed;
+
+
+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'$.
+*};
+
+lemma some_H'h':
+ "[| M = norm_pres_extensions E p F f; c: chain M;
+ 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)";
+proof -;
+ assume "M = norm_pres_extensions E p F f" and cM: "c: chain M"
+ and u: "graph H h = Union c" "x:H";
+
+ have "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'
+ & (ALL x:H'. h' x <= p x)";
+ by (rule some_H'h't);
+ thus ?thesis;
+ proof (elim exE conjE);
+ fix H' h'; assume "(x, h x) : graph H' h'" "graph H' h' : c"
+ "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";
+ show ?thesis;
+ proof (intro exI conjI);
+ show "x:H'"; by (rule graphD1);
+ from cM u; show "graph H' h' <= graph H h";
+ by (simp! only: chain_ball_Union_upper);
+ qed;
+ qed;
+qed;
+
+(***
+lemma some_H'h':
+ "[| M = norm_pres_extensions E p F f; c: chain M;
+ 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)";
+proof -;
+ assume m: "M = norm_pres_extensions E p F f" and cM: "c: chain M"
+ and u: "graph H h = Union c" "x:H";
+ have "(x, h x): graph H h"; by (rule graphI);
+ hence "(x, h x) : Union c"; by (simp!);
+ hence "EX g:c. (x, h x):g"; by (simp only: Union_iff);
+ thus ?thesis;
+ proof (elim bexE);
+ fix g; assume g: "g:c" "(x, h x):g";
+ from cM; have "c <= M"; by (rule chainD2);
+ hence "g : M"; ..;
+ hence "g : norm_pres_extensions E p F f"; by (simp only: m);
+ hence "EX H' h'. graph H' h' = g
+ & 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)";
+ by (rule norm_pres_extension_D);
+ thus ?thesis;
+ proof (elim exE conjE, intro exI conjI);
+ fix H' h'; assume g': "graph H' h' = g";
+ with g; have "(x, h x): graph H' h'"; by simp;
+ thus "x:H'"; by (rule graphD1);
+ from g g'; have "graph H' h' : c"; by simp;
+ with cM u; show "graph H' h' <= graph H h";
+ by (simp only: chain_ball_Union_upper);
+ qed simp+;
+ qed;
+qed;
+***)
+
+
+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
+$h'$, such that $h$ extends $h'$. *};
+
+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 |]
+ ==> 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)";
+proof -;
+ assume "M = norm_pres_extensions E p F f" "c: chain M"
+ "graph H h = Union c" "x:H" "y:H";
+
+ txt {* $x$ is in the domain $H'$ of some function $h'$,
+ such that $h$ extends $h'$. *};
+
+ have e1: "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'
+ & (ALL x:H'. h' x <= p x)";
+ by (rule some_H'h't);
+
+ txt {* $y$ is in the domain $H''$ of some function $h''$,
+ such that $h$ extends $h''$. *};
+
+ have e2: "EX H'' h''. graph H'' h'' : c & (y, h y) : 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)";
+ by (rule some_H'h't);
+
+ from e1 e2; show ?thesis;
+ proof (elim exE conjE);
+ fix H' h'; assume "(y, h y): graph H' h'" "graph H' h' : c"
+ "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";
+
+ fix H'' h''; assume "(x, h x): graph H'' h''" "graph H'' h'' : c"
+ "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";
+
+ txt {* Since both $h'$ and $h''$ are elements of the chain,
+ $h''$ is an extension of $h'$ or vice versa. Thus both
+ $x$ and $y$ are contained in the greater one. *};
+
+ have "graph H'' h'' <= graph H' h' | graph H' h' <= graph H'' h''"
+ (is "?case1 | ?case2");
+ by (rule chainD);
+ thus ?thesis;
+ proof;
+ assume ?case1;
+ show ?thesis;
+ proof (intro exI conjI);
+ have "(x, h x) : graph H'' h''"; .;
+ also; have "... <= graph H' h'"; .;
+ finally; have xh: "(x, h x): graph H' h'"; .;
+ thus x: "x:H'"; ..;
+ show y: "y:H'"; ..;
+ show "graph H' h' <= graph H h";
+ by (simp! only: chain_ball_Union_upper);
+ qed;
+ next;
+ assume ?case2;
+ show ?thesis;
+ proof (intro exI conjI);
+ show x: "x:H''"; ..;
+ have "(y, h y) : graph H' h'"; by (simp!);
+ also; have "... <= graph H'' h''"; .;
+ finally; have yh: "(y, h y): graph H'' h''"; .;
+ thus y: "y:H''"; ..;
+ show "graph H'' h'' <= graph H h";
+ by (simp! only: chain_ball_Union_upper);
+ qed;
+ qed;
+ qed;
+qed;
+
+(***
+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|]
+ ==> 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)";
+proof -;
+ assume "M = norm_pres_extensions E p F f" "c: chain M"
+ "graph H h = Union c";
+
+ let ?P = "\<lambda>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)";
+ assume "x:H";
+ have e1: "EX H' h' t. t : graph H h & t = (x, h x)
+ & graph H' h' : c & t : graph H' h' & ?P H' h'";
+ by (rule some_H'h't);
+ assume "y:H";
+ have e2: "EX H' h' t. t : graph H h & t = (y, h y)
+ & graph H' h' : c & t:graph H' h' & ?P H' h'";
+ by (rule some_H'h't);
+
+ from e1 e2; show ?thesis;
+ proof (elim exE conjE);
+ fix H' h' t' H'' h'' t'';
+ assume
+ "t' : graph H h" "t'' : graph H h"
+ "t' = (y, h y)" "t'' = (x, h x)"
+ "graph H' h' : c" "graph H'' h'' : c"
+ "t' : graph H' h'" "t'' : graph H'' h''"
+ "is_linearform H' h'" "is_linearform H'' h''"
+ "is_subspace H' E" "is_subspace H'' E"
+ "is_subspace F H'" "is_subspace F H''"
+ "graph F f <= graph H' h'" "graph F f <= graph H'' h''"
+ "ALL x:H'. h' x <= p x" "ALL x:H''. h'' x <= p x";
+
+ have "graph H'' h'' <= graph H' h'
+ | graph H' h' <= graph H'' h''";
+ by (rule chainD);
+ thus "?thesis";
+ proof;
+ assume "graph H'' h'' <= graph H' h'";
+ show ?thesis;
+ proof (intro exI conjI);
+ note [trans] = subsetD;
+ have "(x, h x) : graph H'' h''"; by (simp!);
+ also; have "... <= graph H' h'"; .;
+ finally; have xh: "(x, h x): graph H' h'"; .;
+ thus x: "x:H'"; by (rule graphD1);
+ show y: "y:H'"; by (simp!, rule graphD1);
+ show "graph H' h' <= graph H h";
+ by (simp! only: chain_ball_Union_upper);
+ qed;
+ next;
+ assume "graph H' h' <= graph H'' h''";
+ show ?thesis;
+ proof (intro exI conjI);
+ show x: "x:H''"; by (simp!, rule graphD1);
+ have "(y, h y) : graph H' h'"; by (simp!);
+ also; have "... <= graph H'' h''"; .;
+ finally; have yh: "(y, h y): graph H'' h''"; .;
+ thus y: "y:H''"; by (rule graphD1);
+ show "graph H'' h'' <= graph H h";
+ by (simp! only: chain_ball_Union_upper);
+ qed;
+ qed;
+ qed;
+qed;
+
+***)
+
+text{* The relation induced by the graph of the supremum
+of a chain $c$ is definite, i.~e.~it is the graph of a function. *};
+
+lemma sup_definite:
+ "[| M == norm_pres_extensions E p F f; c : chain M;
+ (x, y) : Union c; (x, z) : Union c |] ==> z = y";
+proof -;
+ assume "c:chain M" "M == norm_pres_extensions E p F f"
+ "(x, y) : Union c" "(x, z) : Union c";
+ thus ?thesis;
+ proof (elim UnionE chainE2);
+
+ txt{* Since both $(x, y) \in \cup\; c$ and $(x, z) \in cup c$
+ they are menbers of some graphs $G_1$ and $G_2$, resp.~, such that
+ 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";
+
+ have "G1 : M"; ..;
+ hence e1: "EX H1 h1. graph H1 h1 = G1";
+ by (force! dest: norm_pres_extension_D);
+ have "G2 : M"; ..;
+ hence e2: "EX H2 h2. graph H2 h2 = G2";
+ by (force! dest: norm_pres_extension_D);
+ from e1 e2; show ?thesis;
+ proof (elim exE);
+ 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. *};
+
+ have "G1 <= G2 | G2 <= G1" (is "?case1 | ?case2"); ..;
+ thus ?thesis;
+ proof;
+ assume ?case1;
+ have "(x, y) : graph H2 h2"; by (force!);
+ hence "y = h2 x"; ..;
+ also; have "(x, z) : graph H2 h2"; by (simp!);
+ hence "z = h2 x"; ..;
+ finally; show ?thesis; .;
+ next;
+ assume ?case2;
+ have "(x, y) : graph H1 h1"; by (simp!);
+ hence "y = h1 x"; ..;
+ also; have "(x, z) : graph H1 h1"; by (force!);
+ hence "z = h1 x"; ..;
+ finally; show ?thesis; .;
+ qed;
+ qed;
+ qed;
+qed;
+
+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.
+Futher $h$ is an extension of $h'$ so the value
+of $x$ are identical for $h'$ and $h$.
+Finally, the function $h'$ is linear by construction of $M$.
+*};
+
+lemma sup_lf:
+ "[| M = norm_pres_extensions E p F f; c: chain M;
+ graph H h = Union c |] ==> is_linearform H h";
+proof -;
+ assume "M = norm_pres_extensions E p F f" "c: chain M"
+ "graph H h = Union c";
+
+ show "is_linearform H h";
+ proof;
+ fix x y; assume "x : H" "y : H";
+ have "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)";
+ by (rule some_H'h'2);
+
+ txt {* We have to show that h is linear w.~r.~t.
+ addition. *};
+
+ thus "h (x + y) = h x + h y";
+ proof (elim exE conjE);
+ fix H' h'; assume "x:H'" "y:H'"
+ 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);
+ also; have "h' x = h x"; ..;
+ also; have "h' y = h y"; ..;
+ also; have "x + y : H'"; ..;
+ with b; have "h' (x + y) = h (x + y)"; ..;
+ finally; show ?thesis; .;
+ qed;
+ next;
+ fix a x; assume "x : H";
+ have "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)";
+ by (rule some_H'h');
+
+ txt{* We have to show that h is linear w.~r.~t.
+ skalar multiplication. *};
+
+ thus "h (a <*> x) = a * h x";
+ proof (elim exE conjE);
+ fix H' h'; assume "x:H'"
+ 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);
+ also; have "h' x = h x"; ..;
+ also; have "a <*> x : H'"; ..;
+ with b; have "h' (a <*> x) = h (a <*> x)"; ..;
+ finally; show ?thesis; .;
+ qed;
+ qed;
+qed;
+
+text{* The limit of a non-empty chain of norm
+preserving extensions of $f$ is an extension of $f$,
+since every element of the chain is an extension
+of $f$ and the supremum is an extension
+for every element of the chain.*};
+
+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";
+proof -;
+ assume "M = norm_pres_extensions E p F f" "c: chain M"
+ "graph H h = Union c";
+ assume "EX x. x:c";
+ thus ?thesis;
+ proof;
+ fix x; assume "x:c";
+ have "c <= M"; by (rule chainD2);
+ hence "x:M"; ..;
+ hence "x : norm_pres_extensions E p F f"; by (simp!);
+
+ hence "EX G g. graph G g = x
+ & is_linearform G g
+ & is_subspace G E
+ & is_subspace F G
+ & graph F f <= graph G g
+ & (ALL x:G. g x <= p x)";
+ by (simp! add: norm_pres_extension_D);
+
+ 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);
+ finally; show ?thesis; .;
+ qed;
+ qed;
+qed;
+
+text{* The domain $H$ of the limit function is a superspace
+of $F$, since $F$ is a subset of $H$. The existence of
+the $\zero$ element in $F$ and the closeness properties
+follow from the fact that $F$ is a vectorspace. *};
+
+lemma sup_supF:
+ "[| M = norm_pres_extensions E p F f; c: chain M; EX x. x:c;
+ graph H h = Union c; is_subspace F E; is_vectorspace E |]
+ ==> is_subspace F H";
+proof -;
+ assume "M = norm_pres_extensions E p F f" "c: chain M" "EX x. x:c"
+ "graph H h = Union c" "is_subspace F E" "is_vectorspace E";
+
+ show ?thesis;
+ proof;
+ show "<0> : F"; ..;
+ show "F <= H";
+ proof (rule graph_extD2);
+ show "graph F f <= graph H h";
+ by (rule sup_ext);
+ qed;
+ show "ALL x:F. ALL y:F. x + y : F";
+ proof (intro ballI);
+ fix x y; assume "x:F" "y:F";
+ show "x + y : F"; by (simp!);
+ qed;
+ show "ALL x:F. ALL a. a <*> x : F";
+ proof (intro ballI allI);
+ fix x a; assume "x:F";
+ show "a <*> x : F"; by (simp!);
+ qed;
+ qed;
+qed;
+
+text{* The domain $H$ of the limt function is a subspace
+of $E$. *};
+
+lemma sup_subE:
+ "[| M = norm_pres_extensions E p F f; c: chain M; EX x. x:c;
+ graph H h = Union c; is_subspace F E; is_vectorspace E |]
+ ==> is_subspace H E";
+proof -;
+ assume "M = norm_pres_extensions E p F f" "c: chain M" "EX x. x:c"
+ "graph H h = Union c" "is_subspace F E" "is_vectorspace E";
+ show ?thesis;
+ proof;
+
+ txt {* The $\zero$ element lies 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$. *};
+
+ show "H <= E";
+ proof;
+ fix x; assume "x:H";
+ have "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)";
+ by (rule some_H'h');
+ thus "x:E";
+ proof (elim exE conjE);
+ fix H' h'; assume "x:H'" "is_subspace H' E";
+ have "H' <= E"; ..;
+ thus "x:E"; ..;
+ qed;
+ qed;
+
+ txt{* $H$ is closed under addition. *};
+
+ show "ALL x:H. ALL y:H. x + y : H";
+ proof (intro ballI);
+ fix x y; assume "x:H" "y:H";
+ have "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)";
+ by (rule some_H'h'2);
+ thus "x + y : H";
+ proof (elim exE conjE);
+ fix H' h';
+ assume "x:H'" "y:H'" "is_subspace H' E"
+ "graph H' h' <= graph H h";
+ have "x + y : H'"; ..;
+ also; have "H' <= H"; ..;
+ finally; show ?thesis; .;
+ qed;
+ qed;
+
+ txt{* $H$ is closed under skalar multiplication. *};
+
+ show "ALL x:H. ALL a. a <*> x : H";
+ proof (intro ballI allI);
+ fix x a; assume "x:H";
+ have "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)";
+ by (rule some_H'h');
+ thus "a <*> x : H";
+ proof (elim exE conjE);
+ fix H' h';
+ assume "x:H'" "is_subspace H' E" "graph H' h' <= graph H h";
+ have "a <*> x : H'"; ..;
+ also; have "H' <= H"; ..;
+ finally; show ?thesis; .;
+ qed;
+ qed;
+ qed;
+qed;
+
+text {* The limit functon is bounded by
+the norm $p$ as well, simce all elements in the chain are norm preserving.
+*};
+
+lemma sup_norm_pres:
+ "[| M = norm_pres_extensions E p F f; c: chain M;
+ graph H h = Union c |] ==> ALL x:H. h x <= p x";
+proof;
+ assume "M = norm_pres_extensions E p F f" "c: chain M"
+ "graph H h = Union c";
+ fix x; assume "x:H";
+ have "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)";
+ by (rule some_H'h');
+ thus "h x <= p x";
+ proof (elim exE conjE);
+ fix H' h';
+ assume "x: H'" "graph H' h' <= graph H h"
+ and a: "ALL x: H'. h' x <= p x";
+ have [RS sym]: "h' x = h x"; ..;
+ also; from a; have "h' x <= p x "; ..;
+ finally; show ?thesis; .;
+ qed;
+qed;
+
+
+text_raw{* \medskip *}
+text{* The following lemma is a property of real linearforms on
+real vector spaces. It will be used for the lemma
+$\idt{rabs{\dsh}HahnBanach}$.
+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}\\
+\forall x\in H.\ap h\ap x\leq p\ap x\\
+\end{matharray}
+*};
+
+lemma rabs_ineq_iff:
+ "[| is_subspace H E; is_vectorspace E; is_quasinorm 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"
+ "is_linearform H h";
+ have h: "is_vectorspace H"; ..;
+ show ?thesis;
+ proof;
+ assume l: ?L;
+ show ?R;
+ proof;
+ fix x; assume x: "x:H";
+ have "h x <= rabs (h x)"; by (rule rabs_ge_self);
+ also; from l; have "... <= p x"; ..;
+ finally; show "h x <= p x"; .;
+ qed;
+ next;
+ assume r: ?R;
+ show ?L;
+ proof;
+ fix x; assume "x:H";
+ show "!! a b. [| - a <= b; b <= a |] ==> rabs b <= a";
+ by arith;
+ show "- p x <= h x";
+ proof (rule real_minus_le);
+ from h; have "- h x = h (- x)";
+ by (rule linearform_neg_linear [RS sym]);
+ also; from r; have "... <= p (- x)"; by (simp!);
+ also; have "... = p x";
+ by (rule quasinorm_minus, rule subspace_subsetD);
+ finally; show "- h x <= p x"; .;
+ qed;
+ from r; show "h x <= p x"; ..;
+ qed;
+ qed;
+qed;
+
+
+end;
\ No newline at end of file
--- a/src/HOL/Real/HahnBanach/HahnBanach_h0_lemmas.thy Fri Oct 22 18:41:00 1999 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,300 +0,0 @@
-(* Title: HOL/Real/HahnBanach/HahnBanach_h0_lemmas.thy
- ID: $Id$
- Author: Gertrud Bauer, TU Munich
-*)
-
-header {* Lemmas about the extension of a non-maximal function *};
-
-theory HahnBanach_h0_lemmas = FunctionNorm:;
-
-lemma ex_xi:
- "[| is_vectorspace F; (!! u v. [| u:F; v:F |] ==> a u <= b v )|]
- ==> EX xi::real. (ALL y:F. (a::'a => real) y <= xi)
- & (ALL y:F. xi <= b y)";
-proof -;
- assume vs: "is_vectorspace F";
- assume r: "(!! u v. [| u:F; v:F |] ==> a u <= (b v::real))";
- have "EX t. isLub UNIV {s::real . EX u:F. s = a u} t";
- proof (rule reals_complete);
- from vs; have "a <0> : {s. EX u:F. s = a u}"; by (force);
- thus "EX X. X : {s. EX u:F. s = a u}"; ..;
-
- show "EX Y. isUb UNIV {s. EX u:F. s = a u} Y";
- proof;
- show "isUb UNIV {s. EX u:F. s = a u} (b <0>)";
- proof (intro isUbI setleI ballI, fast);
- fix y; assume y: "y : {s. EX u:F. s = a u}";
- show "y <= b <0>";
- proof -;
- from y; have "EX u:F. y = a u"; by (fast);
- thus ?thesis;
- proof;
- fix u; assume "u:F";
- assume "y = a u";
- also; have "a u <= b <0>";
- proof (rule r);
- show "<0> : F"; ..;
- qed;
- finally; show ?thesis;.;
- qed;
- qed;
- qed;
- qed;
- qed;
- thus "EX xi. (ALL y:F. a y <= xi) & (ALL y:F. xi <= b y)";
- proof (elim exE);
- fix t; assume "isLub UNIV {s::real . EX u:F. s = a u} t";
- show ?thesis;
- proof (intro exI conjI ballI);
- fix y; assume y: "y:F";
- show "a y <= t";
- proof (rule isUbD);
- show"isUb UNIV {s. EX u:F. s = a u} t"; ..;
- qed (force simp add: y);
- next;
- fix y; assume "y:F";
- show "t <= b y";
- proof (intro isLub_le_isUb isUbI setleI);
- show "ALL ya : {s. EX u:F. s = a u}. ya <= b y";
- proof (intro ballI);
- fix au;
- assume au: "au : {s. EX u:F. s = a u} ";
- show "au <= b y";
- proof -;
- from au; have "EX u:F. au = a u"; by (fast);
- thus "au <= b y";
- proof;
- fix u; assume "u:F";
- assume "au = a u";
- also; have "... <= b y"; by (rule r);
- finally; show ?thesis; .;
- qed;
- qed;
- qed;
- show "b y : UNIV"; by fast;
- qed;
- qed;
- qed;
-qed;
-
-lemma h0_lf:
- "[| h0 = (%x. let (y, a) = @ (y, a). (x = y [+] a [*] x0 & y:H)
- in (h y) + a * xi);
- H0 = vectorspace_sum 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 = (%x. let (y, a) = @ (y, a). (x = y [+] a [*] x0 & y:H)
- in (h y) + a * xi)"
- and H0_def: "H0 = vectorspace_sum 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);
- show "is_subspace (lin x0) E"; by (rule lin_subspace);
- qed;
-
- show ?thesis;
- proof;
- fix x1 x2; assume x1: "x1 : H0" and x2: "x2 : H0";
- have x1x2: "x1 [+] x2 : H0";
- by (rule vs_add_closed, rule h0);
-
- from x1; have ex_x1: "? y1 a1. (x1 = y1 [+] a1 [*] x0 & y1 : H)";
- by (simp add: H0_def vectorspace_sum_def lin_def) blast;
- from x2; have ex_x2: "? y2 a2. (x2 = y2 [+] a2 [*] x0 & y2 : H)";
- by (simp add: H0_def vectorspace_sum_def lin_def) blast;
- from x1x2; have ex_x1x2: "? y a. (x1 [+] x2 = y [+] a [*] x0 & y : H)";
- by (simp add: H0_def vectorspace_sum_def lin_def) force;
- from ex_x1 ex_x2 ex_x1x2;
- show "h0 (x1 [+] x2) = h0 x1 + h0 x2";
- proof (elim exE conjE);
- fix y1 y2 y a1 a2 a;
- assume y1: "x1 = y1 [+] a1 [*] x0" and y1': "y1 : H"
- and y2: "x2 = y2 [+] a2 [*] x0" and y2': "y2 : H"
- and y: "x1 [+] x2 = y [+] a [*] x0" and y': "y : H";
-
- have ya: "y1 [+] y2 = y & a1 + a2 = a";
- proof (rule decomp4);
- show "y1 [+] y2 [+] (a1 + a2) [*] x0 = y [+] a [*] x0";
- proof -;
- have "y [+] a [*] x0 = x1 [+] x2"; by (rule sym);
- also; from y1 y2;
- have "... = y1 [+] a1 [*] x0 [+] (y2 [+] a2 [*] x0)"; by simp;
- also; from vs y1' y2';
- have "... = y1 [+] y2 [+] (a1 [*] x0 [+] a2 [*] x0)"; by simp;
- also; from vs y1' y2';
- have "... = y1 [+] y2 [+] (a1 + a2) [*] x0";
- by (simp add: vs_add_mult_distrib2[of E]);
- finally; show ?thesis; by (rule sym);
- qed;
- show "y1 [+] y2 : H"; ..;
- qed;
- have y: "y1 [+] y2 = y"; by (rule conjunct1 [OF ya]);
- have a: "a1 + a2 = a"; by (rule conjunct2 [OF ya]);
-
- have "h0 (x1 [+] x2) = h y + a * xi";
- by (rule decomp3);
- also; have "... = h (y1 [+] y2) + (a1 + a2) * xi"; by (simp add: y a);
- also; from vs y1' y2'; have "... = h y1 + h y2 + a1 * xi + a2 * xi";
- by (simp add: linearform_add_linear [of H] real_add_mult_distrib);
- also; have "... = (h y1 + a1 * xi) + (h y2 + a2 * xi)"; by (simp);
- also; have "h y1 + a1 * xi = h0 x1"; by (rule decomp3 [RS sym]);
- also; have "h y2 + a2 * xi = h0 x2"; by (rule decomp3 [RS sym]);
- finally; show ?thesis; .;
- qed;
-
- 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: "? y1 a1. (x1 = y1 [+] a1 [*] x0 & y1 : H)";
- by (simp add: H0_def vectorspace_sum_def lin_def, fast);
- from x1;
- have ex_x: "!! x. x: H0 ==> ? y a. (x = y [+] a [*] x0 & y : H)";
- by (simp add: H0_def vectorspace_sum_def lin_def, fast);
- note ex_ax1 = ex_x [of "c [*] x1", OF ax1];
- from ex_x1 ex_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"
- and y: "c [*] x1 = y [+] a [*] x0" and y': "y : H";
-
- have ya: "c [*] y1 = y & c * a1 = a";
- proof (rule decomp4);
- show "c [*] y1 [+] (c * a1) [*] x0 = y [+] a [*] x0";
- proof -;
- have "y [+] a [*] x0 = c [*] x1"; by (rule sym);
- also; from y1; have "... = c [*] (y1 [+] a1 [*] x0)"; by simp;
- also; from vs y1'; have "... = c [*] y1 [+] c [*] (a1 [*] x0)";
- by (simp add: vs_add_mult_distrib1);
- also; from vs y1'; have "... = c [*] y1 [+] (c * a1) [*] x0";
- by simp;
- finally; show ?thesis; by (rule sym);
- qed;
- show "c [*] y1: H"; ..;
- qed;
- have y: "c [*] y1 = y"; by (rule conjunct1 [OF ya]);
- have a: "c * a1 = a"; by (rule conjunct2 [OF ya]);
-
- have "h0 (c [*] x1) = h y + a * xi";
- by (rule decomp3);
- also; have "... = h (c [*] y1) + (c * a1) * xi";
- by (simp add: y a);
- also; from vs y1'; have "... = c * h y1 + c * a1 * xi";
- by (simp add: linearform_mult_linear [of H] real_add_mult_distrib);
- 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"; by (rule decomp3 [RS sym]);
- finally; show ?thesis; .;
- qed;
- qed;
-qed;
-
-lemma h0_norm_pres:
- "[| h0 = (%x. let (y, a) = @ (y, a). (x = y [+] a [*] x0 & y:H)
- in (h y) + a * xi);
- H0 = vectorspace_sum H (lin x0); x0 ~: H; x0 : E; x0 ~= <0>;
- is_vectorspace E; is_subspace H E; is_quasinorm 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 = (%x. let (y, a) = @ (y, a). (x = y [+] a [*] x0 & y:H)
- in (h y) + a * xi)"
- and H0_def: "H0 = vectorspace_sum 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)";
- fix x; assume "x : H0";
- show "h0 x <= p x";
- proof -;
- have ex_x: "!! x. x : H0 ==> ? y a. (x = y [+] a [*] x0 & y : H)";
- by (simp add: H0_def vectorspace_sum_def lin_def, fast);
- have "? y a. (x = y [+] a [*] x0 & y : H)";
- by (rule ex_x);
- thus ?thesis;
- proof (elim exE conjE);
- fix y a; assume x: "x = y [+] a [*] x0" and y: "y : H";
- show ?thesis;
- proof -;
- have "h0 x = h y + a * xi";
- by (rule decomp3);
- also; have "... <= p (y [+] a [*] x0)";
- proof (rule real_linear_split [of a "0r"]); (*** case analysis ***)
- assume lz: "a < 0r"; hence nz: "a ~= 0r"; by force;
- show ?thesis;
- proof -;
- from a1;
- have "- p (rinv a [*] y [+] x0) - h (rinv a [*] y) <= xi";
- by (rule bspec, simp!);
-
- with lz;
- have "a * xi <= a * (- p (rinv a [*] y [+] x0) - h (rinv a [*] y))";
- by (rule real_mult_less_le_anti);
- also; have "... = - a * (p (rinv a [*] y [+] x0)) - a * (h (rinv a [*] y))";
- 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 [RS sym]);
- 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]);
- finally; have "a * xi <= p (y [+] a [*] x0) - h y"; .;
-
- hence "h y + a * xi <= h y + (p (y [+] a [*] x0) - h y)";
- by (rule real_add_left_cancel_le [RS iffD2]);
- thus ?thesis;
- by simp;
- qed;
-
- next;
- assume z: "a = 0r";
- with vs y a; show ?thesis; by simp;
-
- next;
- assume gz: "0r < a"; hence nz: "a ~= 0r"; by force;
- show ?thesis;
- proof -;
- from a2;
- have "xi <= p (rinv a [*] y [+] x0) - h (rinv a [*] y)";
- by (rule bspec, simp!);
-
- with gz;
- have "a * xi <= a * (p (rinv a [*] y [+] x0) - h (rinv a [*] y))";
- by (rule real_mult_less_le_mono);
- also;
- have "... = a * (p (rinv a [*] y [+] x0)) - a * (h (rinv a [*] y))";
- by (rule real_mult_diff_distrib2);
- 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);
- 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]);
- finally; have "a * xi <= p (y [+] a [*] x0) - h y"; .;
-
- hence "h y + a * xi <= h y + (p (y [+] a [*] x0) - h y)";
- by (rule real_add_left_cancel_le [RS iffD2]);
- thus ?thesis;
- by simp;
- qed;
- qed;
- also; from x; have "... = p x"; by (simp);
- finally; show ?thesis; .;
- qed;
- qed;
- qed;
-qed blast+;
-
-end;
\ No newline at end of file
--- a/src/HOL/Real/HahnBanach/HahnBanach_lemmas.thy Fri Oct 22 18:41:00 1999 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,497 +0,0 @@
-(* Title: HOL/Real/HahnBanach/HahnBanach_lemmas.thy
- ID: $Id$
- Author: Gertrud Bauer, TU Munich
-*)
-
-header {* Lemmas about the supremal function w.r.t.~the function order *};
-
-theory HahnBanach_lemmas = FunctionNorm + Zorn_Lemma:;
-
-lemma rabs_ineq:
- "[| is_subspace H E; is_vectorspace E; is_quasinorm 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"
- "is_linearform H h";
- have h: "is_vectorspace H"; ..;
- show ?thesis;
- proof;
- assume l: ?L;
- then; show ?R;
- proof (intro ballI);
- fix x; assume x: "x:H";
- have "h x <= rabs (h x)"; by (rule rabs_ge_self);
- also; from l; have "... <= p x"; ..;
- finally; show "h x <= p x"; .;
- qed;
- next;
- assume r: ?R;
- then; show ?L;
- proof (intro ballI);
- fix x; assume "x:H";
-
- show "rabs (h x) <= p x";
- proof -;
- show "!! r x. [| - r <= x; x <= r |] ==> rabs x <= r";
- by arith;
- show "- p x <= h x";
- proof (rule real_minus_le);
- from h; have "- h x = h ([-] x)";
- by (rule linearform_neg_linear [RS sym]);
- also; from r; have "... <= p ([-] x)"; by (simp!);
- also; have "... = p x";
- by (rule quasinorm_minus, rule subspace_subsetD);
- finally; show "- h x <= p x"; .;
- qed;
- from r; show "h x <= p x"; ..;
- qed;
- qed;
- qed;
-qed;
-
-lemma some_H'h't:
- "[| M = norm_pres_extensions E p F f; c: chain M; 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')
- & (ALL x:H'. h' x <= p x)";
-proof -;
- assume m: "M = norm_pres_extensions E p F f" and cM: "c: chain M"
- and u: "graph H h = Union c" "x:H";
-
- let ?P = "%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)";
-
- have "EX t : (graph H h). t = (x, h x)";
- by (rule graphI2);
- thus ?thesis;
- proof (elim bexE);
- fix t; assume t: "t : (graph H h)" "t = (x, h x)";
- with u; have ex1: "EX g:c. t:g";
- by (simp only: Union_iff);
- thus ?thesis;
- proof (elim bexE);
- fix g; assume g: "g:c" "t:g";
- from cM; have "c <= M"; by (rule chainD2);
- hence "g : M"; ..;
- hence "g : norm_pres_extensions E p F f"; by (simp only: m);
- hence "EX H' h'. graph H' h' = g & ?P H' h'";
- by (rule norm_pres_extension_D);
- thus ?thesis; by (elim exE conjE, intro exI conjI) (simp | simp!)+;
- qed;
- qed;
-qed;
-
-lemma some_H'h': "[| M = norm_pres_extensions E p F f; c: chain M;
- 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)";
-proof -;
- assume m: "M = norm_pres_extensions E p F f" and cM: "c: chain M"
- and u: "graph H h = Union c" "x:H";
- have "(x, h x): graph H h"; by (rule graphI);
- also; have "... = Union c"; .;
- finally; have "(x, h x) : Union c"; .;
- hence "EX g:c. (x, h x):g"; by (simp only: Union_iff);
- thus ?thesis;
- proof (elim bexE);
- fix g; assume g: "g:c" "(x, h x):g";
- from cM; have "c <= M"; by (rule chainD2);
- hence "g : M"; ..;
- hence "g : norm_pres_extensions E p F f"; by (simp only: m);
- hence "EX H' h'. graph H' h' = g
- & 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)";
- by (rule norm_pres_extension_D);
- thus ?thesis;
- proof (elim exE conjE, intro exI conjI);
- fix H' h'; assume g': "graph H' h' = g";
- with g; have "(x, h x): graph H' h'"; by simp;
- thus "x:H'"; by (rule graphD1);
- from g g'; have "graph H' h' : c"; by simp;
- with cM u; show "graph H' h' <= graph H h";
- by (simp only: chain_ball_Union_upper);
- qed simp+;
- qed;
-qed;
-
-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|]
- ==> 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)";
-proof -;
- assume "M = norm_pres_extensions E p F f" "c: chain M"
- "graph H h = Union c";
-
- let ?P = "%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)";
- assume "x:H";
- have e1: "EX H' h' t. t : (graph H h) & t = (x, h x) & (graph H' h'):c
- & t:graph H' h' & ?P H' h'";
- by (rule some_H'h't);
- assume "y:H";
- have e2: "EX H' h' t. t : (graph H h) & t = (y, h y) & (graph H' h'):c
- & t:graph H' h' & ?P H' h'";
- by (rule some_H'h't);
-
- from e1 e2; show ?thesis;
- proof (elim exE conjE);
- fix H' h' t' H'' h'' t'';
- assume "t' : graph H h" "t'' : graph H h"
- "t' = (y, h y)" "t'' = (x, h x)"
- "graph H' h' : c" "graph H'' h'' : c"
- "t' : graph H' h'" "t'' : graph H'' h''"
- "is_linearform H' h'" "is_linearform H'' h''"
- "is_subspace H' E" "is_subspace H'' E"
- "is_subspace F H'" "is_subspace F H''"
- "graph F f <= graph H' h'" "graph F f <= graph H'' h''"
- "ALL x:H'. h' x <= p x" "ALL x:H''. h'' x <= p x";
-
- have "(graph H'' h'') <= (graph H' h')
- | (graph H' h') <= (graph H'' h'')";
- by (rule chainD);
- thus "?thesis";
- proof;
- assume "(graph H'' h'') <= (graph H' h')";
- show ?thesis;
- proof (intro exI conjI);
- note [trans] = subsetD;
- have "(x, h x) : graph H'' h''"; by (simp!);
- also; have "... <= graph H' h'"; .;
- finally; have xh: "(x, h x): graph H' h'"; .;
- thus x: "x:H'"; by (rule graphD1);
- show y: "y:H'"; by (simp!, rule graphD1);
- show "(graph H' h') <= (graph H h)";
- by (simp! only: chain_ball_Union_upper);
- qed;
- next;
- assume "(graph H' h') <= (graph H'' h'')";
- show ?thesis;
- proof (intro exI conjI);
- show x: "x:H''"; by (simp!, rule graphD1);
- have "(y, h y) : graph H' h'"; by (simp!);
- also; have "... <= graph H'' h''"; .;
- finally; have yh: "(y, h y): graph H'' h''"; .;
- thus y: "y:H''"; by (rule graphD1);
- show "(graph H'' h'') <= (graph H h)";
- by (simp! only: chain_ball_Union_upper);
- qed;
- qed;
- qed;
-qed;
-
-lemma sup_uniq:
- "[| is_vectorspace E; is_subspace F E; is_quasinorm E p;
- is_linearform F f; ALL x:F. f x <= p x; M == norm_pres_extensions E p F f;
- c : chain M; EX x. x : c; (x, y) : Union c; (x, z) : Union c |]
- ==> z = y";
-proof -;
- assume "M == norm_pres_extensions E p F f" "c : chain M"
- "(x, y) : Union c" " (x, z) : Union c";
- hence "EX H h. (x, y) : graph H h & (x, z) : graph H h";
- proof (elim UnionE chainE2);
- fix G1 G2;
- assume "(x, y) : G1" "G1 : c" "(x, z) : G2" "G2 : c" "c <= M";
- have "G1 : M"; ..;
- hence e1: "EX H1 h1. graph H1 h1 = G1";
- by (force! dest: norm_pres_extension_D);
- have "G2 : M"; ..;
- hence e2: "EX H2 h2. graph H2 h2 = G2";
- by (force! dest: norm_pres_extension_D);
- from e1 e2; show ?thesis;
- proof (elim exE);
- fix H1 h1 H2 h2; assume "graph H1 h1 = G1" "graph H2 h2 = G2";
- have "G1 <= G2 | G2 <= G1"; ..;
- thus ?thesis;
- proof;
- assume "G1 <= G2";
- thus ?thesis;
- proof (intro exI conjI);
- show "(x, y) : graph H2 h2"; by (force!);
- show "(x, z) : graph H2 h2"; by (simp!);
- qed;
- next;
- assume "G2 <= G1";
- thus ?thesis;
- proof (intro exI conjI);
- show "(x, y) : graph H1 h1"; by (simp!);
- show "(x, z) : graph H1 h1"; by (force!);
- qed;
- qed;
- qed;
- qed;
- thus ?thesis;
- proof (elim exE conjE);
- fix H h; assume "(x, y) : graph H h" "(x, z) : graph H h";
- have "y = h x"; ..;
- also; have "... = z"; by (rule sym, rule);
- finally; show "z = y"; by (rule sym);
- qed;
-qed;
-
-lemma sup_lf:
- "[| M = norm_pres_extensions E p F f; c: chain M; graph H h = Union c|]
- ==> is_linearform H h";
-proof -;
- assume "M = norm_pres_extensions E p F f" "c: chain M"
- "graph H h = Union c";
-
- let ?P = "%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)";
-
- show "is_linearform H h";
- proof;
- fix x y; assume "x : H" "y : H";
- show "h (x [+] y) = h x + h y";
- proof -;
- have "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)";
- by (rule some_H'h'2);
- thus ?thesis;
- proof (elim exE conjE);
- fix H' h'; assume "x:H'" "y:H'"
- and b: "graph H' h' <= graph H h"
- and "is_linearform H' h'" "is_subspace H' E";
- have h'x: "h' x = h x"; ..;
- have h'y: "h' y = h y"; ..;
- have h'xy: "h' (x [+] y) = h' x + h' y";
- by (rule linearform_add_linear);
- have "h' (x [+] y) = h (x [+] y)";
- proof -;
- have "x [+] y : H'"; ..;
- with b; show ?thesis; ..;
- qed;
- with h'x h'y h'xy; show ?thesis;
- by (simp!);
- qed;
- qed;
- next;
- fix a x; assume "x : H";
- show "h (a [*] x) = a * (h x)";
- proof -;
- have "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)";
- by (rule some_H'h');
- thus ?thesis;
- proof (elim exE conjE);
- fix H' h';
- assume b: "graph H' h' <= graph H h";
- assume "x:H'" "is_linearform H' h'" "is_subspace H' E";
- have h'x: "h' x = h x"; ..;
- have h'ax: "h' (a [*] x) = a * h' x";
- by (rule linearform_mult_linear);
- have "h' (a [*] x) = h (a [*] x)";
- proof -;
- have "a [*] x : H'"; ..;
- with b; show ?thesis; ..;
- qed;
- with h'x h'ax; show ?thesis;
- by (simp!);
- qed;
- qed;
- qed;
-qed;
-
-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";
-proof -;
- assume "M = norm_pres_extensions E p F f" "c: chain M"
- "graph H h = Union c"
- and e: "EX x. x:c";
-
- thus ?thesis;
- proof (elim exE);
- fix x; assume "x:c";
- show ?thesis;
- proof -;
- have "x:norm_pres_extensions E p F f";
- proof (rule subsetD);
- show "c <= norm_pres_extensions E p F f"; by (simp! add: chainD2);
- qed;
-
- hence "(EX G g. graph G g = x
- & is_linearform G g
- & is_subspace G E
- & is_subspace F G
- & (graph F f <= graph G g)
- & (ALL x:G. g x <= p x))";
- by (simp! add: norm_pres_extension_D);
-
- thus ?thesis;
- proof (elim exE conjE);
- fix G g; assume "graph G g = x" "graph F f <= graph G g";
- show ?thesis;
- proof -;
- have "graph F f <= graph G g"; .;
- also; have "graph G g <= graph H h"; by ((simp!), fast);
- finally; show ?thesis; .;
- qed;
- qed;
- qed;
- qed;
-qed;
-
-
-lemma sup_supF:
- "[| M = norm_pres_extensions E p F f; c: chain M; EX x. x:c;
- graph H h = Union c; is_subspace F E |] ==> is_subspace F H";
-proof -;
- assume "M = norm_pres_extensions E p F f" "c: chain M" "EX x. x:c"
- "graph H h = Union c"
- "is_subspace F E";
-
- show ?thesis;
- proof (rule subspaceI);
- show "<0> : F"; ..;
- show "F <= H";
- proof (rule graph_extD2);
- show "graph F f <= graph H h";
- by (rule sup_ext);
- qed;
- show "ALL x:F. ALL y:F. x [+] y : F";
- proof (intro ballI);
- fix x y; assume "x:F" "y:F";
- show "x [+] y : F"; by (simp!);
- qed;
- show "ALL x:F. ALL a. a [*] x : F";
- proof (intro ballI allI);
- fix x a; assume "x:F";
- show "a [*] x : F"; by (simp!);
- qed;
- qed;
-qed;
-
-
-lemma sup_subE:
- "[| M = norm_pres_extensions E p F f; c: chain M; EX x. x:c;
- graph H h = Union c; is_subspace F E|] ==> is_subspace H E";
-proof -;
- assume "M = norm_pres_extensions E p F f" "c: chain M" "EX x. x:c"
- "graph H h = Union c" "is_subspace F E";
-
- show ?thesis;
- proof;
-
- show "<0> : H";
- proof (rule subsetD [of F H]);
- have "is_subspace F H"; by (rule sup_supF);
- thus "F <= H"; ..;
- show "<0> : F"; ..;
- qed;
-
- show "H <= E";
- proof;
- fix x; assume "x:H";
- show "x:E";
- proof -;
- have "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)";
- by (rule some_H'h');
- thus ?thesis;
- proof (elim exE conjE);
- fix H' h'; assume "x:H'" "is_subspace H' E";
- show "x:E";
- proof (rule subsetD);
- show "H' <= E"; ..;
- qed;
- qed;
- qed;
- qed;
-
- show "ALL x:H. ALL y:H. x [+] y : H";
- proof (intro ballI);
- fix x y; assume "x:H" "y:H";
- show "x [+] y : H";
- proof -;
- have "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)";
- by (rule some_H'h'2);
- thus ?thesis;
- proof (elim exE conjE);
- fix H' h';
- assume "x:H'" "y:H'" "is_subspace H' E"
- "graph H' h' <= graph H h";
- have "H' <= H"; ..;
- thus ?thesis;
- proof (rule subsetD);
- show "x [+] y : H'"; ..;
- qed;
- qed;
- qed;
- qed;
-
- show "ALL x:H. ALL a. a [*] x : H";
- proof (intro ballI allI);
- fix x and a::real; assume "x:H";
- show "a [*] x : H";
- proof -;
- have "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)";
- by (rule some_H'h');
- thus ?thesis;
- proof (elim exE conjE);
- fix H' h';
- assume "x:H'" "is_subspace H' E" "graph H' h' <= graph H h";
- have "H' <= H"; ..;
- thus ?thesis;
- proof (rule subsetD);
- show "a [*] x : H'"; ..;
- qed;
- qed;
- qed;
- qed;
- qed;
-qed;
-
-lemma sup_norm_pres: "[| M = norm_pres_extensions E p F f; c: chain M;
- graph H h = Union c|] ==> ALL x::'a:H. h x <= p x";
-proof;
- assume "M = norm_pres_extensions E p F f" "c: chain M"
- "graph H h = Union c";
- fix x; assume "x:H";
- show "h x <= p x";
- proof -;
- have "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)";
- by (rule some_H'h');
- thus ?thesis;
- proof (elim exE conjE);
- fix H' h'; assume "x: H'" "graph H' h' <= graph H h"
- and a: "ALL x: H'. h' x <= p x" ;
- have "h x = h' x";
- proof (rule sym);
- show "h' x = h x"; ..;
- qed;
- also; from a; have "... <= p x "; ..;
- finally; show ?thesis; .;
- qed;
- qed;
-qed;
-
-end;
\ No newline at end of file
--- a/src/HOL/Real/HahnBanach/LinearSpace.thy Fri Oct 22 18:41:00 1999 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,525 +0,0 @@
-(* Title: HOL/Real/HahnBanach/LinearSpace.thy
- ID: $Id$
- Author: Gertrud Bauer, TU Munich
-*)
-
-header {* Linear Spaces *};
-
-theory LinearSpace = Bounds + Aux:;
-
-subsection {* Signature *};
-
-consts
- sum :: "['a, 'a] => 'a" (infixl "[+]" 65)
- prod :: "[real, 'a] => 'a" (infixr "[*]" 70)
- zero :: 'a ("<0>");
-
-constdefs
- negate :: "'a => 'a" ("[-] _" [100] 100)
- "[-] x == (- 1r) [*] x"
- diff :: "'a => 'a => 'a" (infixl "[-]" 68)
- "x [-] y == x [+] [-] y";
-
-subsection {* Vector space laws *}
-(***
-constdefs
- is_vectorspace :: "'a set => bool"
- "is_vectorspace V == V ~= {}
- & (ALL x: V. ALL a. a [*] x: V)
- & (ALL x: V. ALL y: V. x [+] y = y [+] x)
- & (ALL x: V. ALL y: V. ALL z: V. x [+] y [+] z = x [+] (y [+] z))
- & (ALL x: V. ALL y: V. x [+] y: V)
- & (ALL x: V. x [-] x = <0>)
- & (ALL x: V. <0> [+] x = x)
- & (ALL x: V. ALL y: V. ALL a. a [*] (x [+] y) = a [*] x [+] a [*] y)
- & (ALL x: V. ALL a b. (a + b) [*] x = a [*] x [+] b [*] x)
- & (ALL x: V. ALL a b. (a * b) [*] x = a [*] b [*] x)
- & (ALL x: V. 1r [*] x = x)";
-***)
-constdefs
- is_vectorspace :: "'a set => bool"
- "is_vectorspace V == V ~= {}
- & (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 = y [+] x
- & x [-] x = <0>
- & <0> [+] x = x
- & a [*] (x [+] y) = a [*] x [+] a [*] y
- & (a + b) [*] x = a [*] x [+] b [*] x
- & (a * b) [*] x = a [*] b [*] x
- & 1r [*] x = x)";
-
-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 y: V. x [+] y = y [+] x;
- ALL x: V. x [-] x = <0>;
- ALL x: V. <0> [+] x = x;
- ALL x: V. ALL y: V. ALL a. a [*] (x [+] y) = a [*] x [+] a [*] y;
- ALL x: V. ALL a b. (a + b) [*] x = a [*] x [+] b [*] x;
- ALL x: V. ALL a b. (a * b) [*] x = a [*] b [*] x; \
- ALL x: V. 1r [*] x = x |] ==> is_vectorspace V";
-proof (unfold is_vectorspace_def, intro conjI ballI allI);
- fix x y z; assume "x:V" "y:V" "z:V";
- assume "ALL x: V. ALL y: V. ALL z: V. x [+] y [+] z = x [+] (y [+] z)";
- thus "x [+] y [+] z = x [+] (y [+] z)"; by (elim bspec[elimify]);
-qed force+;
-
-lemma vs_not_empty [intro !!]: "is_vectorspace V ==> (V ~= {})";
- by (unfold is_vectorspace_def) simp;
-
-lemma vs_add_closed [simp, intro!!]:
- "[| is_vectorspace V; x: V; y: V|] ==> x [+] y: V";
- by (unfold is_vectorspace_def) simp;
-
-lemma vs_mult_closed [simp, intro!!]:
- "[| is_vectorspace V; x: V |] ==> a [*] x: V";
- by (unfold is_vectorspace_def) simp;
-
-lemma vs_diff_closed [simp, intro!!]:
- "[| is_vectorspace V; x: V; y: V|] ==> x [-] y: V";
- by (unfold diff_def negate_def) simp;
-
-lemma vs_neg_closed [simp, intro!!]:
- "[| is_vectorspace V; x: V |] ==> [-] x: V";
- by (unfold negate_def) simp;
-
-lemma vs_add_assoc [simp]:
- "[| 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]:
- "[| is_vectorspace V; x:V; y:V |] ==> y [+] x = x [+] y";
- by (unfold is_vectorspace_def) simp;
-
-lemma vs_add_left_commute [simp]:
- "[| is_vectorspace V; x:V; y:V; z:V |]
- ==> x [+] (y [+] z) = y [+] (x [+] z)";
-proof -;
- assume "is_vectorspace V" "x:V" "y:V" "z:V";
- hence "x [+] (y [+] z) = (x [+] y) [+] z";
- by (simp only: vs_add_assoc);
- also; have "... = (y [+] x) [+] z"; by (simp! only: vs_add_commute);
- also; have "... = y [+] (x [+] z)"; by (simp! only: vs_add_assoc);
- finally; show ?thesis; .;
-qed;
-
-theorems vs_add_ac = vs_add_assoc vs_add_commute vs_add_left_commute;
-
-lemma vs_diff_self [simp]:
- "[| is_vectorspace V; x:V |] ==> x [-] x = <0>";
- by (unfold is_vectorspace_def) simp;
-
-lemma zero_in_vs [simp, intro]: "is_vectorspace V ==> <0>:V";
-proof -;
- assume "is_vectorspace V";
- have "V ~= {}"; ..;
- hence "EX x. x:V"; by force;
- thus ?thesis;
- proof;
- fix x; assume "x:V";
- have "<0> = x [-] x"; by (simp!);
- also; have "... : V"; by (simp! only: vs_diff_closed);
- finally; show ?thesis; .;
- qed;
-qed;
-
-lemma vs_add_zero_left [simp]:
- "[| is_vectorspace V; x:V |] ==> <0> [+] x = x";
- by (unfold is_vectorspace_def) simp;
-
-lemma vs_add_zero_right [simp]:
- "[| is_vectorspace V; x:V |] ==> x [+] <0> = x";
-proof -;
- assume "is_vectorspace V" "x:V";
- hence "x [+] <0> = <0> [+] x"; by simp;
- also; have "... = x"; by (simp!);
- finally; show ?thesis; .;
-qed;
-
-lemma vs_add_mult_distrib1:
- "[| is_vectorspace V; x:V; y:V |]
- ==> a [*] (x [+] y) = a [*] x [+] a [*] y";
- by (unfold is_vectorspace_def) simp;
-
-lemma vs_add_mult_distrib2:
- "[| is_vectorspace V; x:V |] ==> (a + b) [*] x = a [*] x [+] b [*] x";
- by (unfold is_vectorspace_def) simp;
-
-lemma vs_mult_assoc:
- "[| is_vectorspace V; x:V |] ==> (a * b) [*] x = a [*] (b [*] x)";
- by (unfold is_vectorspace_def) simp;
-
-lemma vs_mult_assoc2 [simp]:
- "[| is_vectorspace V; x:V |] ==> a [*] b [*] x = (a * b) [*] x";
- by (simp only: vs_mult_assoc);
-
-lemma vs_mult_1 [simp]:
- "[| is_vectorspace V; x:V |] ==> 1r [*] x = x";
- by (unfold is_vectorspace_def) simp;
-
-lemma vs_diff_mult_distrib1:
- "[| is_vectorspace V; x:V; y:V |]
- ==> a [*] (x [-] y) = a [*] x [-] a [*] y";
- by (simp add: diff_def negate_def vs_add_mult_distrib1);
-
-lemma vs_minus_eq: "[| is_vectorspace V; x:V |]
- ==> - b [*] x = [-] (b [*] x)";
- by (simp add: negate_def);
-
-lemma vs_diff_mult_distrib2:
- "[| is_vectorspace V; x:V |]
- ==> (a - b) [*] x = a [*] x [-] (b [*] x)";
-proof -;
- assume "is_vectorspace V" "x:V";
- have " (a - b) [*] x = (a + - b ) [*] x";
- by (unfold real_diff_def, simp);
- also; have "... = a [*] x [+] (- b) [*] x";
- by (rule vs_add_mult_distrib2);
- also; have "... = a [*] x [+] [-] (b [*] x)";
- by (simp! add: vs_minus_eq);
- also; have "... = a [*] x [-] (b [*] x)"; by (unfold diff_def, simp);
- finally; show ?thesis; .;
-qed;
-
-lemma vs_mult_zero_left [simp]:
- "[| 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);
- also; have "... = (1r + - 1r) [*] x"; by simp;
- also; have "... = 1r [*] x [+] (- 1r) [*] x";
- by (rule vs_add_mult_distrib2);
- also; have "... = x [+] (- 1r) [*] x"; by (simp!);
- also; have "... = x [+] [-] x"; by (fold negate_def) simp;
- also; have "... = x [-] x"; by (fold diff_def) simp;
- also; have "... = <0>"; by (simp!);
- finally; show ?thesis; .;
-qed;
-
-lemma vs_mult_zero_right [simp]:
- "[| is_vectorspace (V:: 'a set) |] ==> a [*] <0> = (<0>::'a)";
-proof -;
- assume "is_vectorspace V";
- have "a [*] <0> = a [*] (<0> [-] (<0>::'a))"; by (simp!);
- also; have "... = a [*] <0> [-] a [*] <0>";
- by (rule vs_diff_mult_distrib1) (simp!)+;
- also; have "... = <0>"; by (simp!);
- finally; show ?thesis; .;
-qed;
-
-lemma vs_minus_mult_cancel [simp]:
- "[| is_vectorspace V; x:V |] ==> (- a) [*] [-] x = a [*] x";
- by (unfold negate_def) simp;
-
-lemma vs_add_minus_left_eq_diff:
- "[| is_vectorspace V; x:V; y:V |] ==> [-] x [+] y = y [-] x";
-proof -;
- assume "is_vectorspace V" "x:V" "y:V";
- have "[-] x [+] y = y [+] [-] x";
- by (simp! add: vs_add_commute [RS sym, of V "[-] x"]);
- also; have "... = y [-] x"; by (unfold diff_def) simp;
- finally; show ?thesis; .;
-qed;
-
-lemma vs_add_minus [simp]:
- "[| is_vectorspace V; x:V|] ==> x [+] [-] x = <0>";
- by (fold diff_def) simp;
-
-lemma vs_add_minus_left [simp]:
- "[| is_vectorspace V; x:V |] ==> [-] x [+] x = <0>";
- by (fold diff_def) simp;
-
-lemma vs_minus_minus [simp]:
- "[| is_vectorspace V; x:V|] ==> [-] [-] x = x";
- by (unfold negate_def) simp;
-
-lemma vs_minus_zero [simp]:
- "[| is_vectorspace (V::'a set)|] ==> [-] (<0>::'a) = <0>";
- by (unfold negate_def) simp;
-
-lemma vs_minus_zero_iff [simp]:
- "[| is_vectorspace V; x:V|] ==> ([-] x = <0>) = (x = <0>)"
- (concl is "?L = ?R");
-proof -;
- assume vs: "is_vectorspace V" "x:V";
- show "?L = ?R";
- proof;
- assume l: ?L;
- have "x = [-] [-] x"; by (rule vs_minus_minus [RS sym]);
- also; have "... = [-] <0>"; by (simp only: l);
- also; have "... = <0>"; by (rule vs_minus_zero);
- finally; show ?R; .;
- next;
- assume ?R;
- with vs; show ?L; by simp;
- qed;
-qed;
-
-lemma vs_add_minus_cancel [simp]:
- "[| 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";
- by (simp add: vs_add_assoc [RS sym] del: vs_add_commute);
-
-lemma vs_minus_add_distrib [simp]:
- "[| is_vectorspace V; x:V; y:V|]
- ==> [-] (x [+] y) = [-] x [+] [-] y";
- by (unfold negate_def, simp add: vs_add_mult_distrib1);
-
-lemma vs_diff_zero [simp]:
- "[| is_vectorspace V; x:V |] ==> x [-] <0> = x";
- by (unfold diff_def) simp;
-
-lemma vs_diff_zero_right [simp]:
- "[| is_vectorspace V; x:V |] ==> <0> [-] x = [-] x";
- by (unfold diff_def) simp;
-
-lemma vs_add_left_cancel:
- "[| is_vectorspace V; x:V; y:V; z:V|]
- ==> (x [+] y = x [+] z) = (y = z)"
- (concl is "?L = ?R");
-proof;
- assume "is_vectorspace V" "x:V" "y:V" "z:V";
- assume l: ?L;
- have "y = <0> [+] y"; by (simp!);
- also; have "... = [-] x [+] x [+] y"; by (simp!);
- also; have "... = [-] x [+] (x [+] y)";
- by (simp! only: vs_add_assoc vs_neg_closed);
- also; have "... = [-] x [+] (x [+] z)"; by (simp only: l);
- also; have "... = [-] x [+] x [+] z";
- by (rule vs_add_assoc [RS sym]) (simp!)+;
- also; have "... = z"; by (simp!);
- finally; show ?R;.;
-next;
- assume ?R;
- thus ?L; by force;
-qed;
-
-lemma vs_add_right_cancel:
- "[| is_vectorspace V; x:V; y:V; z:V |]
- ==> (y [+] x = z [+] x) = (y = z)";
- by (simp only: vs_add_commute vs_add_left_cancel);
-
-lemma vs_add_assoc_cong [tag FIXME simp]:
- "[| is_vectorspace V; x:V; y:V; x':V; y':V; z:V |]
- ==> x [+] y = x' [+] y' ==> x [+] (y [+] z) = x' [+] (y' [+] z)";
- by (simp del: vs_add_commute vs_add_assoc add: vs_add_assoc [RS sym]);
-
-lemma vs_mult_left_commute:
- "[| is_vectorspace V; x:V; y:V; z:V |]
- ==> x [*] y [*] z = y [*] x [*] z";
- by (simp add: real_mult_commute);
-
-lemma vs_mult_zero_uniq :
- "[| is_vectorspace V; x:V; a [*] x = <0>; x ~= <0> |] ==> a = 0r";
-proof (rule classical);
- assume "is_vectorspace V" "x:V" "a [*] x = <0>" "x ~= <0>";
- assume "a ~= 0r";
- have "x = (rinv a * a) [*] x"; by (simp!);
- also; have "... = (rinv a) [*] (a [*] x)"; by (rule vs_mult_assoc);
- also; have "... = (rinv a) [*] <0>"; by (simp!);
- also; have "... = <0>"; by (simp!);
- finally; have "x = <0>"; .;
- thus "a = 0r"; by contradiction;
-qed;
-
-lemma vs_mult_left_cancel:
- "[| is_vectorspace V; x:V; y:V; a ~= 0r |] ==>
- (a [*] x = a [*] y) = (x = y)"
- (concl is "?L = ?R");
-proof;
- assume "is_vectorspace V" "x:V" "y:V" "a ~= 0r";
- assume l: ?L;
- have "x = 1r [*] x"; by (simp!);
- also; have "... = (rinv a * a) [*] x"; by (simp!);
- also; have "... = rinv a [*] (a [*] x)";
- by (simp! only: vs_mult_assoc);
- also; have "... = rinv a [*] (a [*] y)"; by (simp only: l);
- also; have "... = y"; by (simp!);
- finally; show ?R;.;
-next;
- assume ?R;
- thus ?L; by simp;
-qed;
-
-lemma vs_mult_right_cancel: (*** forward ***)
- "[| is_vectorspace V; x:V; x ~= <0> |] ==> (a [*] x = b [*] x) = (a = b)"
- (concl is "?L = ?R");
-proof;
- assume "is_vectorspace V" "x:V" "x ~= <0>";
- assume l: ?L;
- have "(a - b) [*] x = a [*] x [-] b [*] x"; by (simp! add: vs_diff_mult_distrib2);
- also; from l; have "a [*] x [-] b [*] x = <0>"; by (simp!);
- finally; have "(a - b) [*] x = <0>"; .;
- hence "a - b = 0r"; by (simp! add: vs_mult_zero_uniq);
- thus "a = b"; by (rule real_add_minus_eq);
-next;
- assume ?R;
- thus ?L; by simp;
-qed; (*** backward :
-lemma vs_mult_right_cancel:
- "[| is_vectorspace V; x:V; x ~= <0> |] ==> (a [*] x = b [*] x) = (a = b)"
- (concl is "?L = ?R");
-proof;
- assume "is_vectorspace V" "x:V" "x ~= <0>";
- assume l: ?L;
- show "a = b";
- proof (rule real_add_minus_eq);
- show "a - b = 0r";
- proof (rule vs_mult_zero_uniq);
- have "(a - b) [*] x = a [*] x [-] b [*] x"; by (simp! add: vs_diff_mult_distrib2);
- also; from l; have "a [*] x [-] b [*] x = <0>"; by (simp!);
- finally; show "(a - b) [*] x = <0>"; .;
- qed;
- qed;
-next;
- assume ?R;
- thus ?L; by simp;
-qed;
-**)
-
-lemma vs_eq_diff_eq:
- "[| is_vectorspace V; x:V; y:V; z:V |] ==>
- (x = z [-] y) = (x [+] y = z)"
- (concl is "?L = ?R" );
-proof -;
- assume vs: "is_vectorspace V" "x:V" "y:V" "z:V";
- show "?L = ?R";
- proof;
- assume l: ?L;
- have "x [+] y = z [-] y [+] y"; by (simp add: l);
- also; have "... = z [+] [-] y [+] y"; by (unfold diff_def) simp;
- also; have "... = z [+] ([-] y [+] y)";
- by (rule vs_add_assoc) (simp!)+;
- 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;.;
- next;
- assume r: ?R;
- have "z [-] y = (x [+] y) [-] y"; by (simp only: r);
- also; from vs; have "... = x [+] y [+] [-] y";
- by (unfold diff_def) simp;
- also; have "... = x [+] (y [+] [-] y)";
- by (rule vs_add_assoc) (simp!)+;
- also; have "... = x"; by (simp!);
- finally; show ?L; by (rule sym);
- qed;
-qed;
-
-lemma vs_add_minus_eq_minus:
- "[| is_vectorspace V; x:V; y:V; <0> = x [+] y|] ==> y = [-] x";
-proof -;
- assume vs: "is_vectorspace V" "x:V" "y:V";
- assume "<0> = x [+] y";
- have "[-] x = [-] x [+] <0>"; by (simp!);
- also; have "... = [-] x [+] (x [+] y)"; by (simp!);
- also; have "... = [-] x [+] x [+] y";
- by (rule vs_add_assoc [RS sym]) (simp!)+;
- also; have "... = (x [+] [-] x) [+] y"; by (simp!);
- also; have "... = y"; by (simp!);
- finally; show ?thesis; by (rule sym);
-qed;
-
-lemma vs_add_minus_eq:
- "[| is_vectorspace V; x:V; y:V; x [-] y = <0> |] ==> x = y";
-proof -;
- assume "is_vectorspace V" "x:V" "y:V" "x [-] y = <0>";
- have "x [+] [-] y = x [-] y"; by (unfold diff_def, simp);
- also; have "... = <0>"; .;
- finally; have e: "<0> = x [+] [-] y"; by (rule sym);
- have "x = [-] [-] x"; by (simp!);
- also; have "[-] x = [-] y";
- by (rule vs_add_minus_eq_minus [RS sym]) (simp! add: e)+;
- also; have "[-] ... = y"; by (simp!);
- finally; show "x = y"; .;
-qed;
-
-lemma vs_add_diff_swap:
- "[| 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";
- have "[-] c [+] (a [+] b) = [-] c [+] (c [+] d)";
- by (simp! add: vs_add_left_cancel);
- also; have "... = d"; by (rule vs_minus_add_cancel);
- finally; have eq: "[-] c [+] (a [+] b) = d"; .;
- from vs; have "a [-] c = ([-] c [+] (a [+] b)) [+] [-] b";
- by (simp add: vs_add_ac diff_def);
- also; from eq; have "... = d [+] [-] b";
- by (simp! add: vs_add_right_cancel);
- also; have "... = d [-] b"; by (simp add : diff_def);
- finally; show "a [-] c = d [-] b"; .;
-qed;
-
-lemma vs_add_cancel_21:
- "[| is_vectorspace V; x:V; y:V; z:V; u:V|]
- ==> (x [+] (y [+] z) = y [+] u) = ((x [+] z) = u)"
- (concl is "?L = ?R" );
-proof -;
- assume vs: "is_vectorspace V" "x:V" "y:V""z:V" "u:V";
- show "?L = ?R";
- proof;
- assume l: ?L;
- have "u = <0> [+] u"; by (simp!);
- also; have "... = [-] y [+] y [+] u"; by (simp!);
- also; have "... = [-] y [+] (y [+] u)";
- by (rule vs_add_assoc) (simp!)+;
- also; have "... = [-] y [+] (x [+] (y [+] z))"; by (simp only: l);
- also; have "... = [-] y [+] (y [+] (x [+] z))"; by (simp!);
- also; have "... = [-] y [+] y [+] (x [+] z)";
- by (rule vs_add_assoc [RS sym]) (simp!)+;
- also; have "... = (x [+] z)"; by (simp!);
- finally; show ?R; by (rule sym);
- next;
- assume r: ?R;
- have "x [+] (y [+] z) = y [+] (x [+] z)";
- by (simp! only: vs_add_left_commute [of V x]);
- also; have "... = y [+] u"; by (simp only: r);
- finally; show ?L; .;
- qed;
-qed;
-
-lemma vs_add_cancel_end:
- "[| is_vectorspace V; x:V; y:V; z:V |]
- ==> (x [+] (y [+] z) = y) = (x = [-] z)"
- (concl is "?L = ?R" );
-proof -;
- assume vs: "is_vectorspace V" "x:V" "y:V" "z:V";
- show "?L = ?R";
- proof;
- assume l: ?L;
- have "<0> = x [+] z";
- proof (rule vs_add_left_cancel [RS iffD1]);
- have "y [+] <0> = y"; by (simp! only: vs_add_zero_right);
- also; have "... = x [+] (y [+] z)"; by (simp only: l);
- also; have "... = y [+] (x [+] z)";
- by (simp! only: vs_add_left_commute);
- finally; show "y [+] <0> = y [+] (x [+] z)"; .;
- qed (simp!)+;
- hence "z = [-] x"; by (simp! only: vs_add_minus_eq_minus);
- then; show ?R; by (simp!);
- next;
- assume r: ?R;
- have "x [+] (y [+] z) = [-] z [+] (y [+] z)"; by (simp only: r);
- also; have "... = y [+] ([-] z [+] z)";
- by (simp! only: vs_add_left_commute);
- also; have "... = y [+] <0>"; by (simp!);
- also; have "... = y"; by (simp!);
- finally; show ?L; .;
- qed;
-qed;
-
-lemma it: "[| x = y; x' = y'|] ==> x [+] x' = y [+] y'";
- by simp;
-
-end;
\ No newline at end of file
--- a/src/HOL/Real/HahnBanach/Linearform.thy Fri Oct 22 18:41:00 1999 +0200
+++ b/src/HOL/Real/HahnBanach/Linearform.thy Fri Oct 22 20:14:31 1999 +0200
@@ -5,33 +5,38 @@
header {* Linearforms *};
-theory Linearform = LinearSpace:;
+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. *};
constdefs
- is_linearform :: "['a set, 'a => real] => bool"
+ is_linearform :: "['a::{minus, plus} set, 'a => real] => bool"
"is_linearform V f ==
- (ALL x: V. ALL y: V. f (x [+] y) = f x + f y) &
- (ALL x: V. ALL a. f (a [*] x) = a * (f x))";
+ (ALL x: V. ALL y: V. f (x + y) = f x + f y) &
+ (ALL x: V. ALL a. f (a <*> x) = a * (f x))";
lemma is_linearformI [intro]:
- "[| !! x y. [| x : V; y : V |] ==> f (x [+] y) = f x + f y;
- !! x c. x : V ==> f (c [*] x) = c * f x |]
+ "[| !! x y. [| x : V; y : V |] ==> f (x + y) = f x + f y;
+ !! x c. x : V ==> f (c <*> x) = c * f x |]
==> is_linearform V f";
by (unfold is_linearform_def) force;
lemma linearform_add_linear [intro!!]:
- "[| is_linearform V f; x:V; y:V |] ==> f (x [+] y) = f x + f y";
- by (unfold is_linearform_def) auto;
+ "[| 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!!]:
- "[| is_linearform V f; x:V |] ==> f (a [*] x) = a * (f x)";
- by (unfold is_linearform_def) auto;
+ "[| is_linearform V f; x:V |] ==> f (a <*> x) = a * (f x)";
+ by (unfold is_linearform_def) fast;
lemma linearform_neg_linear [intro!!]:
- "[| is_vectorspace V; is_linearform V f; x:V|] ==> f ([-] x) = - f x";
+ "[| 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 (unfold negate_def) simp;
+ have "f (- x) = f ((- 1r) <*> x)"; by (simp! add: negate_eq1);
also; have "... = (- 1r) * (f x)"; by (rule linearform_mult_linear);
also; have "... = - (f x)"; by (simp!);
finally; show ?thesis; .;
@@ -39,21 +44,23 @@
lemma linearform_diff_linear [intro!!]:
"[| is_vectorspace V; is_linearform V f; x:V; y:V |]
- ==> f (x [-] y) = f x - f y";
+ ==> 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_def);
- also; have "... = f x + f ([-] y)";
+ 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);
- finally; show "f (x [-] y) = f x - f y"; by (simp!);
+ also; have "f (- y) = - f y"; by (rule linearform_neg_linear);
+ finally; show "f (x - y) = f x - f y"; by (simp!);
qed;
+text{* Every linearform yields $0$ for the $\zero$ vector.*};
+
lemma linearform_zero [intro!!, simp]:
"[| is_vectorspace V; is_linearform V f |] ==> f <0> = 0r";
proof -;
assume "is_vectorspace V" "is_linearform V f";
- have "f <0> = f (<0> [-] <0>)"; by (simp!);
+ have "f <0> = f (<0> - <0>)"; by (simp!);
also; have "... = f <0> - f <0>";
by (rule linearform_diff_linear) (simp!)+;
also; have "... = 0r"; by simp;
--- a/src/HOL/Real/HahnBanach/NormedSpace.thy Fri Oct 22 18:41:00 1999 +0200
+++ b/src/HOL/Real/HahnBanach/NormedSpace.thy Fri Oct 22 20:14:31 1999 +0200
@@ -11,19 +11,21 @@
subsection {* Quasinorms *};
+text{* A \emph{quasinorm} $\norm{\cdot}$ is a function on a real vector space into the reals
+that has the following properties: *};
constdefs
- is_quasinorm :: "['a set, 'a => real] => bool"
+ is_quasinorm :: "['a::{plus, minus} set, 'a => real] => bool"
"is_quasinorm 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";
+ & 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;
- !! 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";
+ !! 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);
lemma quasinorm_ge_zero [intro!!]:
@@ -32,55 +34,54 @@
lemma quasinorm_mult_distrib:
"[| is_quasinorm V norm; x:V |]
- ==> norm (a [*] x) = (rabs a) * (norm x)";
+ ==> norm (a <*> x) = (rabs a) * (norm x)";
by (unfold is_quasinorm_def, force);
lemma quasinorm_triangle_ineq:
"[| is_quasinorm V norm; x:V; y:V |]
- ==> norm (x [+] y) <= norm x + norm y";
+ ==> norm (x + y) <= norm x + norm y";
by (unfold is_quasinorm_def, force);
lemma quasinorm_diff_triangle_ineq:
"[| is_quasinorm V norm; x:V; y:V; is_vectorspace V |]
- ==> norm (x [-] y) <= norm x + norm y";
+ ==> norm (x - y) <= norm x + norm y";
proof -;
assume "is_quasinorm V norm" "x:V" "y:V" "is_vectorspace V";
- have "norm (x [-] y) = norm (x [+] - 1r [*] y)";
- by (simp add: diff_def negate_def);
- also; have "... <= norm x + norm (- 1r [*] y)";
+ 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);
- also; have "norm (- 1r [*] y) = rabs (- 1r) * norm y";
+ also; have "norm (- 1r <*> y) = rabs (- 1r) * norm y";
by (rule quasinorm_mult_distrib);
also; have "rabs (- 1r) = 1r"; by (rule rabs_minus_one);
- finally; show "norm (x [-] y) <= norm x + norm y"; by simp;
+ finally; show "norm (x - y) <= norm x + norm y"; by simp;
qed;
lemma quasinorm_minus:
"[| is_quasinorm V norm; x:V; is_vectorspace V |]
- ==> norm ([-] x) = norm x";
+ ==> norm (- x) = norm x";
proof -;
assume "is_quasinorm V norm" "x:V" "is_vectorspace V";
- have "norm ([-] x) = norm (-1r [*] x)"; by (unfold negate_def) force;
+ have "norm (- x) = norm (-1r <*> x)"; by (simp! only: negate_eq1);
also; have "... = rabs (-1r) * norm x";
by (rule quasinorm_mult_distrib);
also; have "rabs (- 1r) = 1r"; by (rule rabs_minus_one);
- finally; show "norm ([-] x) = norm x"; by simp;
+ finally; show "norm (- x) = norm x"; by simp;
qed;
-
subsection {* Norms *};
+text{* A \emph{norm} $\norm{\cdot}$ is a quasinorm that maps only $\zero$ to $0$. *};
constdefs
- is_norm :: "['a set, 'a => real] => bool"
+ is_norm :: "['a::{minus, plus} set, 'a => real] => bool"
"is_norm V norm == ALL x: V. is_quasinorm V norm
& (norm x = 0r) = (x = <0>)";
lemma is_normI [intro]:
"ALL x: V. is_quasinorm V norm & (norm x = 0r) = (x = <0>)
- ==> is_norm V norm";
- by (unfold is_norm_def, force);
+ ==> 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";
@@ -97,9 +98,12 @@
subsection {* Normed vector spaces *};
+text{* A vector space together with a norm is called
+a \emph{normed space}. *};
constdefs
- is_normed_vectorspace :: "['a set, 'a => real] => bool"
+ is_normed_vectorspace ::
+ "['a::{plus, minus} set, 'a => real] => bool"
"is_normed_vectorspace V norm ==
is_vectorspace V &
is_norm V norm";
@@ -138,19 +142,22 @@
lemma normed_vs_norm_mult_distrib [intro!!]:
"[| is_normed_vectorspace V norm; x:V |]
- ==> norm (a [*] x) = (rabs a) * (norm x)";
+ ==> norm (a <*> x) = (rabs a) * (norm x)";
by (rule quasinorm_mult_distrib, rule norm_is_quasinorm,
rule normed_vs_norm);
lemma normed_vs_norm_triangle_ineq [intro!!]:
"[| is_normed_vectorspace V norm; x:V; y:V |]
- ==> norm (x [+] y) <= norm x + norm y";
+ ==> norm (x + y) <= norm x + norm y";
by (rule quasinorm_triangle_ineq, rule norm_is_quasinorm,
rule normed_vs_norm);
+text{* Any subspace of a normed vector space is again a
+normed vectorspace.*};
+
lemma subspace_normed_vs [intro!!]:
- "[| is_subspace F E; is_vectorspace E; is_normed_vectorspace E norm |]
- ==> is_normed_vectorspace F norm";
+ "[| is_subspace F E; is_vectorspace E;
+ is_normed_vectorspace E norm |] ==> is_normed_vectorspace F norm";
proof (rule normed_vsI);
assume "is_subspace F E" "is_vectorspace E"
"is_normed_vectorspace E norm";
@@ -161,9 +168,9 @@
proof;
fix x y a; presume "x : E";
show "0r <= norm x"; ..;
- show "norm (a [*] x) = rabs a * norm x"; ..;
+ show "norm (a <*> x) = rabs a * norm x"; ..;
presume "y : E";
- show "norm (x [+] y) <= norm x + norm y"; ..;
+ show "norm (x + y) <= norm x + norm y"; ..;
qed (simp!)+;
fix x; assume "x : F";
--- a/src/HOL/Real/HahnBanach/Subspace.thy Fri Oct 22 18:41:00 1999 +0200
+++ b/src/HOL/Real/HahnBanach/Subspace.thy Fri Oct 22 20:14:31 1999 +0200
@@ -6,28 +6,30 @@
header {* Subspaces *};
-theory Subspace = LinearSpace:;
+theory Subspace = VectorSpace:;
-subsection {* Subspaces *};
+subsection {* Definition *};
-constdefs
- is_subspace :: "['a set, 'a set] => bool"
- "is_subspace U V == <0>:U & U <= V
- & (ALL x:U. ALL y:U. ALL a. x [+] y : U
- & a [*] x : U)";
+text {* A non-empty subset $U$ of a vector space $V$ is a
+\emph{subspace} of $V$, iff $U$ is closed under addition and
+scalar multiplication. *};
+
+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)";
lemma subspaceI [intro]:
- "[| <0>:U; U <= V; ALL x:U. ALL y:U. (x [+] y : U);
- ALL x:U. ALL a. a [*] x : 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";
- by (unfold is_subspace_def) simp;
+proof (unfold is_subspace_def, intro conjI);
+ assume "<0>:U"; thus "U ~= {}"; by fast;
+qed (simp+);
-lemma "is_subspace U V ==> U ~= {}";
- by (unfold is_subspace_def) force;
-
-lemma zero_in_subspace [intro !!]: "is_subspace U V ==> <0>:U";
- by (unfold is_subspace_def) simp;;
+lemma subspace_not_empty [intro!!]: "is_subspace U V ==> U ~= {}";
+ by (unfold is_subspace_def) simp;
lemma subspace_subset [intro !!]: "is_subspace U V ==> U <= V";
by (unfold is_subspace_def) simp;
@@ -37,20 +39,44 @@
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; x: U; y: U |] ==> x [-] y: U";
- by (unfold diff_def negate_def) simp;
+ "[| 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.*};
+
+lemma zero_in_subspace [intro !!]:
+ "[| is_subspace U V; is_vectorspace V |] ==> <0>:U";
+proof -;
+ assume "is_subspace U V" and v: "is_vectorspace V";
+ have "U ~= {}"; ..;
+ hence "EX x. x:U"; by force;
+ thus ?thesis;
+ proof;
+ fix x; assume u: "x:U";
+ hence "x:V"; by (simp!);
+ with v; have "<0> = x - x"; by (simp!);
+ also; have "... : U"; by (rule subspace_diff_closed);
+ finally; show ?thesis; .;
+ qed;
+qed;
lemma subspace_neg_closed [simp, intro!!]:
- "[| is_subspace U V; x: U |] ==> [-] x: U";
- by (unfold negate_def) simp;
+ "[| 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. *};
lemma subspace_vs [intro!!]:
"[| is_subspace U V; is_vectorspace V |] ==> is_vectorspace U";
@@ -59,40 +85,48 @@
show ?thesis;
proof;
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. 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);
+ show "ALL x:U. ALL y:U. x - y = x + - y";
+ by (simp! add: diff_eq1);
qed (simp! add: vs_add_mult_distrib1 vs_add_mult_distrib2)+;
qed;
+text {* The subspace relation is reflexive. *};
+
lemma subspace_refl [intro]: "is_vectorspace V ==> is_subspace V V";
proof;
assume "is_vectorspace V";
show "<0> : V"; ..;
show "V <= V"; ..;
- show "ALL x:V. ALL y:V. x [+] y : V"; by (simp!);
- show "ALL x:V. ALL a. a [*] x : V"; by (simp!);
+ show "ALL x:V. ALL y:V. x + y : V"; by (simp!);
+ show "ALL x:V. ALL a. a <*> x : V"; by (simp!);
qed;
+text {* The subspace relation is transitive. *};
+
lemma subspace_trans:
- "[| is_subspace U V; is_subspace V W |] ==> is_subspace U W";
+ "[| is_subspace U V; is_vectorspace V; is_subspace V W |]
+ ==> is_subspace U W";
proof;
- assume "is_subspace U V" "is_subspace V W";
+ assume "is_subspace U V" "is_subspace V W" "is_vectorspace V";
show "<0> : U"; ..;
have "U <= V"; ..;
also; have "V <= W"; ..;
finally; show "U <= W"; .;
- show "ALL x:U. ALL y:U. x [+] y : U";
+ show "ALL x:U. ALL y:U. x + y : U";
proof (intro ballI);
fix x y; assume "x:U" "y:U";
- show "x [+] y : U"; by (simp!);
+ show "x + y : U"; by (simp!);
qed;
- show "ALL x:U. ALL a. a [*] x : U";
+ show "ALL x:U. ALL a. a <*> x : U";
proof (intro ballI allI);
fix x a; assume "x:U";
- show "a [*] x : U"; by (simp!);
+ show "a <*> x : U"; by (simp!);
qed;
qed;
@@ -100,60 +134,68 @@
subsection {* Linear closure *};
+text {* The \emph{linear closure} of a vector $x$ is the set of all
+multiples of $x$. *};
constdefs
lin :: "'a => 'a set"
- "lin x == {y. ? a. y = a [*] x}";
+ "lin x == {y. EX a. y = a <*> x}";
-lemma linD: "x : lin v = (? a::real. x = a [*] v)";
+lemma linD: "x : lin v = (EX a::real. x = a <*> v)";
by (unfold lin_def) force;
-lemma linI [intro!!]: "a [*] x0 : lin x0";
+lemma linI [intro!!]: "a <*> x0 : lin x0";
by (unfold lin_def) force;
+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);
assume "is_vectorspace V" "x:V";
- show "x = 1r [*] x"; by (simp!);
+ show "x = 1r <*> x"; by (simp!);
qed;
+text {* Any linear closure is a subspace. *};
+
lemma lin_subspace [intro!!]:
"[| is_vectorspace V; x:V |] ==> is_subspace (lin x) V";
proof;
assume "is_vectorspace V" "x:V";
show "<0> : lin x";
proof (unfold lin_def, intro CollectI exI);
- show "<0> = 0r [*] x"; by (simp!);
+ show "<0> = 0r <*> x"; by (simp!);
qed;
show "lin x <= V";
proof (unfold lin_def, intro subsetI, elim CollectE exE);
- fix xa a; assume "xa = a [*] x";
+ fix xa a; assume "xa = a <*> x";
show "xa:V"; by (simp!);
qed;
- show "ALL x1 : lin x. ALL x2 : lin x. x1 [+] x2 : lin x";
+ show "ALL x1 : lin x. ALL x2 : lin x. x1 + x2 : lin x";
proof (intro ballI);
fix x1 x2; assume "x1 : lin x" "x2 : lin x";
- thus "x1 [+] x2 : lin x";
+ thus "x1 + x2 : lin x";
proof (unfold lin_def, elim CollectE exE, intro CollectI exI);
- fix a1 a2; assume "x1 = a1 [*] x" "x2 = a2 [*] x";
- show "x1 [+] x2 = (a1 + a2) [*] x";
+ 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;
- show "ALL xa:lin x. ALL a. a [*] xa : lin x";
+ 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";
+ thus "a <*> x1 : lin x";
proof (unfold lin_def, elim CollectE exE, intro CollectI exI);
- fix a1; assume "x1 = a1 [*] x";
- show "a [*] x1 = (a * a1) [*] x"; by (simp!);
+ fix a1; assume "x1 = a1 <*> x";
+ show "a <*> x1 = (a * a1) <*> x"; by (simp!);
qed;
qed;
qed;
+text {* Any linear closure is a vector space. *};
+
lemma lin_vs [intro!!]:
"[| is_vectorspace V; x:V |] ==> is_vectorspace (lin x)";
proof (rule subspace_vs);
@@ -165,139 +207,166 @@
subsection {* Sum of two vectorspaces *};
+text {* The \emph{sum} of two vectorspaces $U$ and $V$ is the set of
+all sums of elements from $U$ and $V$. *};
+instance set :: (plus) plus; by intro_classes;
+
+defs vs_sum_def:
+ "U + V == {x. EX u:U. EX v:V. x = u + v}";
+
+(***
constdefs
- vectorspace_sum :: "['a set, 'a set] => 'a set"
- "vectorspace_sum U V == {x. ? u:U. ? v:V. x = u [+] v}";
+ vs_sum ::
+ "['a::{minus, plus} set, 'a set] => 'a set" (infixl "+" 65)
+ "vs_sum U V == {x. EX u:U. EX v:V. x = u + v}";
+***)
-lemma vs_sumD: "x:vectorspace_sum U V = (? u:U. ? v:V. x = u [+] v)";
- by (unfold vectorspace_sum_def) simp;
+lemma vs_sumD:
+ "x: U + V = (EX u:U. EX v:V. x = u + v)";
+ by (unfold vs_sum_def) simp;
lemmas vs_sumE = vs_sumD [RS iffD1, elimify];
lemma vs_sumI [intro!!]:
- "[| x: U; y:V; (t::'a) = x [+] y |]
- ==> (t::'a) : vectorspace_sum U V";
- by (unfold vectorspace_sum_def, intro CollectI bexI);
+ "[| x:U; y:V; t= x + y |] ==> t : U + V";
+ by (unfold vs_sum_def, intro CollectI bexI);
+
+text{* $U$ is a subspace of $U + V$. *};
lemma subspace_vs_sum1 [intro!!]:
- "[| is_vectorspace U; is_vectorspace V |]
- ==> is_subspace U (vectorspace_sum U V)";
+ "[| is_vectorspace U; is_vectorspace V |]
+ ==> is_subspace U (U + V)";
proof;
assume "is_vectorspace U" "is_vectorspace V";
show "<0> : U"; ..;
- show "U <= vectorspace_sum U V";
+ show "U <= U + V";
proof (intro subsetI vs_sumI);
fix x; assume "x:U";
- show "x = x [+] <0>"; by (simp!);
+ show "x = x + <0>"; by (simp!);
show "<0> : V"; by (simp!);
qed;
- show "ALL x:U. ALL y:U. x [+] y : U";
+ show "ALL x:U. ALL y:U. x + y : U";
proof (intro ballI);
- fix x y; assume "x:U" "y:U"; show "x [+] y : U"; by (simp!);
+ fix x y; assume "x:U" "y:U"; show "x + y : U"; by (simp!);
qed;
- show "ALL x:U. ALL a. a [*] x : U";
+ show "ALL x:U. ALL a. a <*> x : U";
proof (intro ballI allI);
- fix x a; assume "x:U"; show "a [*] x : U"; by (simp!);
+ fix x a; assume "x:U"; show "a <*> x : U"; by (simp!);
qed;
qed;
+text{* The sum of two subspaces is again a subspace.*};
+
lemma vs_sum_subspace [intro!!]:
"[| is_subspace U E; is_subspace V E; is_vectorspace E |]
- ==> is_subspace (vectorspace_sum U V) E";
+ ==> is_subspace (U + V) E";
proof;
- assume "is_subspace U E" "is_subspace V E" and e: "is_vectorspace E";
- show "<0> : vectorspace_sum U V";
+ assume "is_subspace U E" "is_subspace V E" "is_vectorspace E";
+ show "<0> : U + V";
proof (intro vs_sumI);
show "<0> : U"; ..;
show "<0> : V"; ..;
- show "(<0>::'a) = <0> [+] <0>"; by (simp!);
+ show "(<0>::'a) = <0> + <0>"; by (simp!);
qed;
- show "vectorspace_sum U V <= E";
+ show "U + V <= E";
proof (intro subsetI, elim vs_sumE bexE);
- fix x u v; assume "u : U" "v : V" "x = u [+] v";
+ fix x u v; assume "u : U" "v : V" "x = u + v";
show "x:E"; by (simp!);
qed;
- show "ALL x:vectorspace_sum U V. ALL y:vectorspace_sum U V.
- x [+] y : vectorspace_sum U V";
+ show "ALL x: U + V. ALL y: U + V. x + y : U + V";
proof (intro ballI);
- fix x y; assume "x:vectorspace_sum U V" "y:vectorspace_sum U V";
- thus "x [+] y : vectorspace_sum U V";
+ fix x y; assume "x : U + V" "y : U + V";
+ thus "x + y : U + V";
proof (elim vs_sumE bexE, intro vs_sumI);
fix ux vx uy vy;
- assume "ux : U" "vx : V" "x = ux [+] vx" "uy : U" "vy : V"
- "y = uy [+] vy";
- show "x [+] y = (ux [+] uy) [+] (vx [+] vy)"; by (simp!);
+ assume "ux : U" "vx : V" "x = ux + vx"
+ and "uy : U" "vy : V" "y = uy + vy";
+ show "x + y = (ux + uy) + (vx + vy)"; by (simp!);
qed (simp!)+;
qed;
- show "ALL x:vectorspace_sum U V. ALL a.
- a [*] x : vectorspace_sum U V";
+ show "ALL x: U + V. ALL a. a <*> x : U + V";
proof (intro ballI allI);
- fix x a; assume "x:vectorspace_sum U V";
- thus "a [*] x : vectorspace_sum U V";
+ fix x a; assume "x : U + V";
+ thus "a <*> x : U + V";
proof (elim vs_sumE bexE, intro vs_sumI);
- fix a x u v; assume "u : U" "v : V" "x = u [+] v";
- show "a [*] x = (a [*] u) [+] (a [*] v)";
+ fix a x u v; assume "u : U" "v : V" "x = u + v";
+ show "a <*> x = (a <*> u) + (a <*> v)";
by (simp! add: vs_add_mult_distrib1);
qed (simp!)+;
qed;
qed;
+text{* The sum of two subspaces is a vectorspace. *};
+
lemma vs_sum_vs [intro!!]:
"[| is_subspace U E; is_subspace V E; is_vectorspace E |]
- ==> is_vectorspace (vectorspace_sum U V)";
+ ==> is_vectorspace (U + V)";
proof (rule subspace_vs);
assume "is_subspace U E" "is_subspace V E" "is_vectorspace E";
- show "is_subspace (vectorspace_sum U V) E"; ..;
+ show "is_subspace (U + V) E"; ..;
qed;
-subsection {* A special case *}
+subsection {* Direct sums *};
-text {* direct sum of a vectorspace and a linear closure of a vector
-*};
+text {* The sum of $U$ and $V$ is called \emph{direct}, iff the zero
+element is the only common element of $U$ and $V$. For every element
+$x$ of the direct sum of $U$ and $V$ the decomposition in
+$x = u + v$ with $u:U$ and $v:V$ is unique.*};
-lemma decomp: "[| is_vectorspace E; is_subspace U E; is_subspace V E;
- U Int V = {<0>}; u1:U; u2:U; v1:V; v2:V; u1 [+] v1 = u2 [+] v2 |]
+lemma decomp:
+ "[| is_vectorspace E; is_subspace U E; is_subspace V E;
+ U Int V = {<0>}; u1:U; u2:U; v1:V; v2:V; u1 + v1 = u2 + v2 |]
==> u1 = u2 & v1 = v2";
proof;
assume "is_vectorspace E" "is_subspace U E" "is_subspace V E"
"U Int V = {<0>}" "u1:U" "u2:U" "v1:V" "v2:V"
- "u1 [+] v1 = u2 [+] v2";
- have eq: "u1 [-] u2 = v2 [-] v1"; by (simp! add: vs_add_diff_swap);
- have u: "u1 [-] u2 : U"; by (simp!);
- with eq; have v': "v2 [-] v1 : U"; by simp;
- have v: "v2 [-] v1 : V"; by (simp!);
- with eq; have u': "u1 [-] u2 : V"; by simp;
+ "u1 + v1 = u2 + v2";
+ have eq: "u1 - u2 = v2 - v1"; by (simp! add: vs_add_diff_swap);
+ have u: "u1 - u2 : U"; by (simp!);
+ with eq; have v': "v2 - v1 : U"; by simp;
+ have v: "v2 - v1 : V"; by (simp!);
+ with eq; have u': "u1 - u2 : V"; by simp;
show "u1 = u2";
proof (rule vs_add_minus_eq);
- show "u1 [-] u2 = <0>"; by (rule Int_singletonD [OF _ u u']);
- qed (rule);
+ show "u1 - u2 = <0>"; by (rule Int_singletonD [OF _ u u']);
+ show "u1 : E"; ..;
+ show "u2 : E"; ..;
+ qed;
show "v1 = v2";
proof (rule vs_add_minus_eq [RS sym]);
- show "v2 [-] v1 = <0>"; by (rule Int_singletonD [OF _ v' v]);
- qed (rule);
+ show "v2 - v1 = <0>"; by (rule Int_singletonD [OF _ v' v]);
+ show "v1 : E"; ..;
+ show "v2 : E"; ..;
+ qed;
qed;
-lemma decomp4: "[| is_vectorspace E; is_subspace H E; y1 : H; y2 : H;
- x0 ~: H; x0 :E; x0 ~= <0>; y1 [+] a1 [*] x0 = y2 [+] a2 [*] x0 |]
+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:H$ and $a$ are unique. *};
+
+lemma decomp_H0:
+ "[| is_vectorspace E; is_subspace H E; y1 : H; y2 : H;
+ x0 ~: H; x0 : E; x0 ~= <0>; y1 + a1 <*> x0 = y2 + a2 <*> x0 |]
==> y1 = y2 & a1 = a2";
proof;
assume "is_vectorspace E" and h: "is_subspace H E"
and "y1 : H" "y2 : H" "x0 ~: H" "x0 : E" "x0 ~= <0>"
- "y1 [+] a1 [*] x0 = y2 [+] a2 [*] x0";
+ "y1 + a1 <*> x0 = y2 + a2 <*> x0";
- have c: "y1 = y2 & a1 [*] x0 = a2 [*] x0";
+ have c: "y1 = y2 & a1 <*> x0 = a2 <*> x0";
proof (rule decomp);
- show "a1 [*] x0 : lin x0"; ..;
- show "a2 [*] x0 : lin x0"; ..;
+ show "a1 <*> x0 : lin x0"; ..;
+ show "a2 <*> x0 : lin x0"; ..;
show "H Int (lin x0) = {<0>}";
proof;
show "H Int lin x0 <= {<0>}";
@@ -305,15 +374,15 @@
fix x; assume "x:H" "x:lin x0";
thus "x = <0>";
proof (unfold lin_def, elim CollectE exE);
- fix a; assume "x = a [*] x0";
+ fix a; assume "x = a <*> x0";
show ?thesis;
- proof (rule case_split [of "a = 0r"]);
+ proof (rule case_split);
assume "a = 0r"; show ?thesis; by (simp!);
next;
assume "a ~= 0r";
- from h; have "(rinv a) [*] a [*] x0 : H";
+ from h; have "rinv a <*> a <*> x0 : H";
by (rule subspace_mult_closed) (simp!);
- also; have "(rinv a) [*] a [*] x0 = x0"; by (simp!);
+ also; have "rinv a <*> a <*> x0 = x0"; by (simp!);
finally; have "x0 : H"; .;
thus ?thesis; by contradiction;
qed;
@@ -332,58 +401,68 @@
show "a1 = a2";
proof (rule vs_mult_right_cancel [RS iffD1]);
- from c; show "a1 [*] x0 = a2 [*] x0"; by simp;
+ from c; show "a1 <*> x0 = a2 <*> x0"; by simp;
qed;
qed;
-lemma decomp1:
- "[| is_vectorspace E; is_subspace H E; t:H; x0~:H; x0:E; x0 ~= <0> |]
- ==> (@ (y, a). t = y [+] a [*] x0 & y : H) = (t, 0r)";
+text {* Since 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, follows from $y\in H$ the fact that
+$a = 0$.*};
+
+lemma decomp_H0_H:
+ "[| 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 decomp4) (assumption | (simp!))+;
+ by (rule decomp_H0) (assumption | (simp!))+;
thus "(y, a) = (t, 0r)"; by (simp!);
qed (simp!)+;
-lemma decomp3:
- "[| h0 = (%x. let (y, a) = @ (y, a). (x = y [+] a [*] x0 & y:H)
+text {* The components $y\in H$ and $a$ in $y \plus a \mult x_0$
+are unique, so the function $h_0$ defined by
+$h_0 (y \plus a \mult x_0) = h y + a * xi$ is definite. *};
+
+lemma h0_definite:
+ "[| 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;
+ 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 = (%x. let (y, a) = @ (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>";
- have "x : vectorspace_sum H (lin x0)";
- by (simp! add: vectorspace_sum_def lin_def, intro bexI exI conjI)
- force+;
- have "EX! xa. ((%(y, a). x = y [+] a [*] x0 & y:H) xa)";
- proof%%;
- show "EX xa. ((%(y, a). x = y [+] a [*] x0 & y:H) xa)";
+ assume
+ "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>";
+ have "x : H + (lin x0)";
+ 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)";
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 "(%(y,a). x = y + a <*> x0 & y : H) xa"
+ "(%(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 decomp4, (simp!)+);
+ by (elim conjE) (rule decomp_H0, (simp!)+);
qed;
qed;
- hence eq: "(@ (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;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Real/HahnBanach/VectorSpace.thy Fri Oct 22 20:14:31 1999 +0200
@@ -0,0 +1,537 @@
+(* Title: HOL/Real/HahnBanach/VectorSpace.thy
+ ID: $Id$
+ Author: Gertrud Bauer, TU Munich
+*)
+
+header {* Vector spaces *};
+
+theory VectorSpace = Bounds + Aux:;
+
+subsection {* Signature *};
+
+text {* For the definition of real vector spaces a type $\alpha$ is
+considered, on which the operations addition and real scalar
+multiplication are defined, and which has an zero element.*};
+
+consts
+(***
+ sum :: "['a, 'a] => 'a" (infixl "+" 65)
+***)
+ prod :: "[real, 'a] => 'a" (infixr "<*>" 70)
+ zero :: 'a ("<0>");
+
+syntax (symbols)
+ prod :: "[real, 'a] => 'a" (infixr "\<prod>" 70)
+ zero :: 'a ("\<zero>");
+
+text {* The unary and binary minus can be considered as
+abbreviations: *};
+
+(***
+constdefs
+ negate :: "'a => 'a" ("- _" [100] 100)
+ "- x == (- 1r) <*> x"
+ diff :: "'a => 'a => 'a" (infixl "-" 68)
+ "x - y == x + - y";
+***)
+
+subsection {* Vector space laws *};
+
+text {* A \emph{vector space} is a non-empty set $V$ of elements
+from $\alpha$ with the following vector space laws:
+The set $V$ is closed under addition and scalar multiplication,
+addition is associative 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 multiplication.
+*};
+
+constdefs
+ is_vectorspace :: "('a::{plus,minus}) set => bool"
+ "is_vectorspace V == V ~= {}
+ & (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 = y + x
+ & x - x = <0>
+ & <0> + x = x
+ & a <*> (x + y) = a <*> x + a <*> y
+ & (a + b) <*> x = a <*> x + b <*> x
+ & (a * b) <*> x = a <*> b <*> x
+ & 1r <*> x = x
+ & - x = (- 1r) <*> x
+ & x - y = x + - y)";
+
+text_raw {* \medskip *};
+text {* The corresponding introduction rule is:*};
+
+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 y:V. x + y = y + x;
+ ALL x:V. x - x = <0>;
+ ALL x:V. <0> + x = x;
+ ALL x:V. ALL y:V. ALL a. a <*> (x + y) = a <*> x + a <*> y;
+ ALL x:V. ALL a b. (a + b) <*> x = a <*> x + b <*> x;
+ 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";
+proof (unfold is_vectorspace_def, intro conjI ballI allI);
+ fix x y z;
+ assume "x:V" "y:V" "z:V"
+ "ALL x:V. ALL y:V. ALL z:V. x + y + z = x + (y + z)";
+ thus "x + y + z = x + (y + z)"; by (elim bspec[elimify]);
+qed force+;
+
+text_raw {* \medskip *};
+text {* The corresponding destruction rules are: *};
+
+lemma negate_eq1:
+ "[| is_vectorspace V; x:V |] ==> - x = (- 1r) <*> x";
+ by (unfold is_vectorspace_def) simp;
+
+lemma diff_eq1:
+ "[| is_vectorspace V; x:V; y:V |] ==> x - y = x + - y";
+ by (unfold is_vectorspace_def) simp;
+
+lemma negate_eq2:
+ "[| is_vectorspace V; x:V |] ==> (- 1r) <*> x = - x";
+ by (unfold is_vectorspace_def) simp;
+
+lemma diff_eq2:
+ "[| is_vectorspace V; x:V; y:V |] ==> x + - y = x - y";
+ by (unfold is_vectorspace_def) simp;
+
+lemma vs_not_empty [intro !!]: "is_vectorspace V ==> (V ~= {})";
+ by (unfold is_vectorspace_def) simp;
+
+lemma vs_add_closed [simp, intro!!]:
+ "[| is_vectorspace V; x:V; y:V|] ==> x + y : V";
+ by (unfold is_vectorspace_def) simp;
+
+lemma vs_mult_closed [simp, intro!!]:
+ "[| is_vectorspace V; x:V |] ==> a <*> x : V";
+ by (unfold is_vectorspace_def) simp;
+
+lemma vs_diff_closed [simp, intro!!]:
+ "[| is_vectorspace V; x:V; y:V|] ==> x - y : V";
+ by (simp add: diff_eq1 negate_eq1);
+
+lemma vs_neg_closed [simp, intro!!]:
+ "[| is_vectorspace V; x:V |] ==> - x : V";
+ 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)";
+ by (unfold is_vectorspace_def) fast;
+
+lemma vs_add_commute [simp]:
+ "[| is_vectorspace V; x:V; y:V |] ==> y + x = x + y";
+ by (unfold is_vectorspace_def) simp;
+
+lemma vs_add_left_commute [simp]:
+ "[| is_vectorspace V; x:V; y:V; z:V |]
+ ==> x + (y + z) = y + (x + z)";
+proof -;
+ assume "is_vectorspace V" "x:V" "y:V" "z:V";
+ hence "x + (y + z) = (x + y) + z";
+ by (simp only: vs_add_assoc);
+ also; have "... = (y + x) + z"; by (simp! only: vs_add_commute);
+ also; have "... = y + (x + z)"; by (simp! only: vs_add_assoc);
+ finally; show ?thesis; .;
+qed;
+
+theorems vs_add_ac = vs_add_assoc vs_add_commute vs_add_left_commute;
+
+lemma vs_diff_self [simp]:
+ "[| 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. *};
+
+lemma zero_in_vs [simp, intro]: "is_vectorspace V ==> <0>:V";
+proof -;
+ assume "is_vectorspace V";
+ have "V ~= {}"; ..;
+ hence "EX x. x:V"; by force;
+ thus ?thesis;
+ proof;
+ fix x; assume "x:V";
+ have "<0> = x - x"; by (simp!);
+ also; have "... : V"; by (simp! only: vs_diff_closed);
+ finally; show ?thesis; .;
+ qed;
+qed;
+
+lemma vs_add_zero_left [simp]:
+ "[| is_vectorspace V; x:V |] ==> <0> + x = x";
+ by (unfold is_vectorspace_def) simp;
+
+lemma vs_add_zero_right [simp]:
+ "[| is_vectorspace V; x:V |] ==> x + <0> = x";
+proof -;
+ assume "is_vectorspace V" "x:V";
+ hence "x + <0> = <0> + x"; by simp;
+ also; have "... = x"; by (simp!);
+ finally; show ?thesis; .;
+qed;
+
+lemma vs_add_mult_distrib1:
+ "[| is_vectorspace V; x:V; y:V |]
+ ==> a <*> (x + y) = a <*> x + a <*> y";
+ by (unfold is_vectorspace_def) simp;
+
+lemma vs_add_mult_distrib2:
+ "[| is_vectorspace V; x:V |]
+ ==> (a + b) <*> x = a <*> x + b <*> x";
+ by (unfold is_vectorspace_def) simp;
+
+lemma vs_mult_assoc:
+ "[| is_vectorspace V; x:V |] ==> (a * b) <*> x = a <*> (b <*> x)";
+ by (unfold is_vectorspace_def) simp;
+
+lemma vs_mult_assoc2 [simp]:
+ "[| is_vectorspace V; x:V |] ==> a <*> b <*> x = (a * b) <*> x";
+ by (simp only: vs_mult_assoc);
+
+lemma vs_mult_1 [simp]:
+ "[| is_vectorspace V; x:V |] ==> 1r <*> x = x";
+ by (unfold is_vectorspace_def) simp;
+
+lemma vs_diff_mult_distrib1:
+ "[| is_vectorspace V; x:V; y:V |]
+ ==> a <*> (x - y) = a <*> x - a <*> y";
+ by (simp add: diff_eq1 negate_eq1 vs_add_mult_distrib1);
+
+lemma vs_diff_mult_distrib2:
+ "[| is_vectorspace V; x:V |]
+ ==> (a - b) <*> x = a <*> x - (b <*> x)";
+proof -;
+ assume "is_vectorspace V" "x:V";
+ have " (a - b) <*> x = (a + - b ) <*> x";
+ by (unfold real_diff_def, simp);
+ also; have "... = a <*> x + (- b) <*> x";
+ by (rule vs_add_mult_distrib2);
+ also; have "... = a <*> x + - (b <*> x)";
+ by (simp! add: negate_eq1);
+ also; have "... = a <*> x - (b <*> x)";
+ by (simp! add: diff_eq1);
+ finally; show ?thesis; .;
+qed;
+
+(*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>";
+proof -;
+ assume "is_vectorspace V" "x:V";
+ have "0r <*> x = (1r - 1r) <*> x"; by (simp only: real_diff_self);
+ also; have "... = (1r + - 1r) <*> x"; by simp;
+ also; have "... = 1r <*> x + (- 1r) <*> x";
+ by (rule vs_add_mult_distrib2);
+ also; have "... = x + (- 1r) <*> x"; by (simp!);
+ also; have "... = x + - x"; by (simp! add: negate_eq2);;
+ also; have "... = x - x"; by (simp! add: diff_eq2);
+ also; have "... = <0>"; by (simp!);
+ finally; show ?thesis; .;
+qed;
+
+lemma vs_mult_zero_right [simp]:
+ "[| is_vectorspace (V:: 'a::{plus, minus} set) |]
+ ==> a <*> <0> = (<0>::'a)";
+proof -;
+ assume "is_vectorspace V";
+ have "a <*> <0> = a <*> (<0> - (<0>::'a))"; by (simp!);
+ also; have "... = a <*> <0> - a <*> <0>";
+ by (rule vs_diff_mult_distrib1) (simp!)+;
+ also; have "... = <0>"; by (simp!);
+ finally; show ?thesis; .;
+qed;
+
+lemma vs_minus_mult_cancel [simp]:
+ "[| is_vectorspace V; x:V |] ==> (- a) <*> - x = a <*> x";
+ by (simp add: negate_eq1);
+
+lemma vs_add_minus_left_eq_diff:
+ "[| is_vectorspace V; x:V; y:V |] ==> - x + y = y - x";
+proof -;
+ assume "is_vectorspace V" "x:V" "y:V";
+ have "- x + y = y + - x";
+ by (simp! add: vs_add_commute [RS sym, of V "- x"]);
+ also; have "... = y - x"; by (simp! add: diff_eq1);
+ finally; show ?thesis; .;
+qed;
+
+lemma vs_add_minus [simp]:
+ "[| is_vectorspace V; x:V |] ==> x + - x = <0>";
+ by (simp! add: diff_eq2);
+
+lemma vs_add_minus_left [simp]:
+ "[| is_vectorspace V; x:V |] ==> - x + x = <0>";
+ by (simp! add: diff_eq2);
+
+lemma vs_minus_minus [simp]:
+ "[| is_vectorspace V; x:V |] ==> - (- x) = x";
+ by (simp add: negate_eq1);
+
+lemma vs_minus_zero [simp]:
+ "is_vectorspace (V::'a::{minus, plus} set) ==> - (<0>::'a) = <0>";
+ by (simp add: negate_eq1);
+
+lemma vs_minus_zero_iff [simp]:
+ "[| is_vectorspace V; x:V |] ==> (- x = <0>) = (x = <0>)"
+ (concl is "?L = ?R");
+proof -;
+ assume "is_vectorspace V" "x:V";
+ show "?L = ?R";
+ proof;
+ have "x = - (- x)"; by (rule vs_minus_minus [RS sym]);
+ also; assume ?L;
+ also; have "- ... = <0>"; by (rule vs_minus_zero);
+ finally; show ?R; .;
+ qed (simp!);
+qed;
+
+lemma vs_add_minus_cancel [simp]:
+ "[| 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";
+ by (simp add: vs_add_assoc [RS sym] del: vs_add_commute);
+
+lemma vs_minus_add_distrib [simp]:
+ "[| is_vectorspace V; x:V; y:V |]
+ ==> - (x + y) = - x + - y";
+ by (simp add: negate_eq1 vs_add_mult_distrib1);
+
+lemma vs_diff_zero [simp]:
+ "[| is_vectorspace V; x:V |] ==> x - <0> = x";
+ by (simp add: diff_eq1);
+
+lemma vs_diff_zero_right [simp]:
+ "[| is_vectorspace V; x:V |] ==> <0> - x = - x";
+ by (simp add:diff_eq1);
+
+lemma vs_add_left_cancel:
+ "[| is_vectorspace V; x:V; y:V; z:V|]
+ ==> (x + y = x + z) = (y = z)"
+ (concl is "?L = ?R");
+proof;
+ assume "is_vectorspace V" "x:V" "y:V" "z:V";
+ have "y = <0> + y"; by (simp!);
+ also; have "... = - x + x + y"; by (simp!);
+ also; have "... = - x + (x + y)";
+ by (simp! only: vs_add_assoc vs_neg_closed);
+ also; assume ?L;
+ also; have "- x + ... = - x + x + z";
+ by (rule vs_add_assoc [RS sym]) (simp!)+;
+ also; have "... = z"; by (simp!);
+ finally; show ?R;.;
+qed force;
+
+lemma vs_add_right_cancel:
+ "[| is_vectorspace V; x:V; y:V; z:V |]
+ ==> (y + x = z + x) = (y = z)";
+ by (simp only: vs_add_commute vs_add_left_cancel);
+
+lemma vs_add_assoc_cong:
+ "[| is_vectorspace V; x:V; y:V; x':V; y':V; z:V |]
+ ==> x + y = x' + y' ==> x + (y + z) = x' + (y' + z)";
+ by (simp only: vs_add_assoc [RS sym]);
+
+lemma vs_mult_left_commute:
+ "[| is_vectorspace V; x:V; y:V; z:V |]
+ ==> x <*> y <*> z = y <*> x <*> z";
+ by (simp add: real_mult_commute);
+
+lemma vs_mult_zero_uniq :
+ "[| is_vectorspace V; x:V; a <*> x = <0>; x ~= <0> |] ==> a = 0r";
+proof (rule classical);
+ assume "is_vectorspace V" "x:V" "a <*> x = <0>" "x ~= <0>";
+ assume "a ~= 0r";
+ have "x = (rinv a * a) <*> x"; by (simp!);
+ also; have "... = rinv a <*> (a <*> x)"; by (rule vs_mult_assoc);
+ also; have "... = rinv a <*> <0>"; by (simp!);
+ also; have "... = <0>"; by (simp!);
+ finally; have "x = <0>"; .;
+ thus "a = 0r"; by contradiction;
+qed;
+
+lemma vs_mult_left_cancel:
+ "[| is_vectorspace V; x:V; y:V; a ~= 0r |] ==>
+ (a <*> x = a <*> y) = (x = y)"
+ (concl is "?L = ?R");
+proof;
+ assume "is_vectorspace V" "x:V" "y:V" "a ~= 0r";
+ have "x = 1r <*> x"; by (simp!);
+ also; have "... = (rinv a * a) <*> x"; by (simp!);
+ also; have "... = rinv a <*> (a <*> x)";
+ by (simp! only: vs_mult_assoc);
+ also; assume ?L;
+ also; have "rinv a <*> ... = y"; by (simp!);
+ finally; show ?R;.;
+qed simp;
+
+lemma vs_mult_right_cancel: (*** forward ***)
+ "[| is_vectorspace V; x:V; x ~= <0> |]
+ ==> (a <*> x = b <*> x) = (a = b)" (concl is "?L = ?R");
+proof;
+ assume "is_vectorspace V" "x:V" "x ~= <0>";
+ have "(a - b) <*> x = a <*> x - b <*> x";
+ by (simp! add: vs_diff_mult_distrib2);
+ also; assume ?L; hence "a <*> x - b <*> x = <0>"; by (simp!);
+ finally; have "(a - b) <*> x = <0>"; .;
+ hence "a - b = 0r"; by (simp! add: vs_mult_zero_uniq);
+ thus "a = b"; by (rule real_add_minus_eq);
+qed simp; (***
+
+backward :
+lemma vs_mult_right_cancel:
+ "[| is_vectorspace V; x:V; x ~= <0> |] ==>
+ (a <*> x = b <*> x) = (a = b)"
+ (concl is "?L = ?R");
+proof;
+ assume "is_vectorspace V" "x:V" "x ~= <0>";
+ assume l: ?L;
+ show "a = b";
+ proof (rule real_add_minus_eq);
+ show "a - b = 0r";
+ proof (rule vs_mult_zero_uniq);
+ have "(a - b) <*> x = a <*> x - b <*> x";
+ by (simp! add: vs_diff_mult_distrib2);
+ also; from l; have "a <*> x - b <*> x = <0>"; by (simp!);
+ finally; show "(a - b) <*> x = <0>"; .;
+ qed;
+ qed;
+next;
+ assume ?R;
+ thus ?L; by simp;
+qed;
+**)
+
+lemma vs_eq_diff_eq:
+ "[| is_vectorspace V; x:V; y:V; z:V |] ==>
+ (x = z - y) = (x + y = z)"
+ (concl is "?L = ?R" );
+proof -;
+ assume vs: "is_vectorspace V" "x:V" "y:V" "z:V";
+ show "?L = ?R";
+ proof;
+ assume ?L;
+ hence "x + y = z - y + y"; by simp;
+ also; have "... = z + - y + y"; by (simp! add: diff_eq1);
+ also; have "... = z + (- y + y)";
+ by (rule vs_add_assoc) (simp!)+;
+ 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;.;
+ next;
+ assume ?R;
+ hence "z - y = (x + y) - y"; by simp;
+ also; from vs; have "... = x + y + - y";
+ by (simp add: diff_eq1);
+ also; have "... = x + (y + - y)";
+ by (rule vs_add_assoc) (simp!)+;
+ also; have "... = x"; by (simp!);
+ finally; show ?L; by (rule sym);
+ qed;
+qed;
+
+lemma vs_add_minus_eq_minus:
+ "[| 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!);
+ also; have "... = - y + (x + y)"; by (simp!);
+ also; assume "x + y = <0>";
+ also; have "- y + <0> = - y"; by (simp!);
+ finally; show "x = - y"; .;
+qed;
+
+lemma vs_add_minus_eq:
+ "[| is_vectorspace V; x:V; y:V; x - y = <0> |] ==> x = y";
+proof -;
+ assume "is_vectorspace V" "x:V" "y:V" "x - y = <0>";
+ assume "x - y = <0>";
+ hence e: "x + - y = <0>"; by (simp! add: diff_eq1);
+ with _ _ _; have "x = - (- y)";
+ by (rule vs_add_minus_eq_minus) (simp!)+;
+ thus "x = y"; by (simp!);
+qed;
+
+lemma vs_add_diff_swap:
+ "[| 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";
+ have "- c + (a + b) = - c + (c + d)";
+ by (simp! add: vs_add_left_cancel);
+ also; have "... = d"; by (rule vs_minus_add_cancel);
+ finally; have eq: "- c + (a + b) = d"; .;
+ from vs; have "a - c = (- c + (a + b)) + - b";
+ by (simp add: vs_add_ac diff_eq1);
+ also; from eq; have "... = d + - b";
+ by (simp! add: vs_add_right_cancel);
+ also; have "... = d - b"; by (simp! add : diff_eq2);
+ finally; show "a - c = d - b"; .;
+qed;
+
+lemma vs_add_cancel_21:
+ "[| is_vectorspace V; x:V; y:V; z:V; u:V|]
+ ==> (x + (y + z) = y + u) = ((x + z) = u)"
+ (concl is "?L = ?R" );
+proof -;
+ assume "is_vectorspace V" "x:V" "y:V""z:V" "u:V";
+ show "?L = ?R";
+ proof;
+ have "x + z = - y + y + (x + z)"; by (simp!);
+ also; have "... = - y + (y + (x + z))";
+ by (rule vs_add_assoc) (simp!)+;
+ also; have "y + (x + z) = x + (y + z)"; by (simp!);
+ also; assume ?L;
+ also; have "- y + (y + u) = u"; by (simp!);
+ finally; show ?R; .;
+ qed (simp! only: vs_add_left_commute [of V x]);
+qed;
+
+lemma vs_add_cancel_end:
+ "[| is_vectorspace V; x:V; y:V; z:V |]
+ ==> (x + (y + z) = y) = (x = - z)"
+ (concl is "?L = ?R" );
+proof -;
+ assume "is_vectorspace V" "x:V" "y:V" "z:V";
+ show "?L = ?R";
+ proof;
+ assume l: ?L;
+ have "x + z = <0>";
+ proof (rule vs_add_left_cancel [RS iffD1]);
+ have "y + (x + z) = x + (y + z)"; by (simp!);
+ also; note l;
+ also; have "y = y + <0>"; by (simp!);
+ finally; show "y + (x + z) = y + <0>"; .;
+ qed (simp!)+;
+ thus "x = - z"; by (simp! add: vs_add_minus_eq_minus);
+ next;
+ assume r: ?R;
+ hence "x + (y + z) = - z + (y + z)"; by simp;
+ also; have "... = y + (- z + z)";
+ by (simp! only: vs_add_left_commute);
+ also; have "... = y"; by (simp!);
+ finally; show ?L; .;
+ qed;
+qed;
+
+end;
\ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Real/HahnBanach/ZornLemma.thy Fri Oct 22 20:14:31 1999 +0200
@@ -0,0 +1,55 @@
+(* Title: HOL/Real/HahnBanach/ZornLemma.thy
+ ID: $Id$
+ Author: Gertrud Bauer, TU Munich
+*)
+
+header {* Zorn's Lemma *};
+
+theory ZornLemma = Aux + Zorn:;
+
+text{*
+Zorn's Lemmas says: 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
+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$:
+*};
+
+theorem Zorn's_Lemma:
+ "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);
+ 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";
+ proof;
+ fix c; assume "c:chain S";
+ show "EX y:S. ALL z:c. z <= y";
+ proof (rule case_split);
+
+ txt{* If $c$ is an empty chain, then every element
+ in $S$ is an upperbound of $c$. *};
+
+ assume "c={}";
+ with aS; show ?thesis; by fast;
+
+ txt{* If $c$ is non-empty, then $\cup\; c$
+ is an upperbound of $c$, that lies in $S$. *};
+
+ next;
+ assume c: "c~={}";
+ show ?thesis;
+ proof;
+ show "ALL z:c. z <= Union c"; by fast;
+ show "Union c : S";
+ proof (rule r);
+ from c; show "EX x. x:c"; by fast;
+ qed;
+ qed;
+ qed;
+ qed;
+qed;
+
+end;
--- a/src/HOL/Real/HahnBanach/Zorn_Lemma.thy Fri Oct 22 18:41:00 1999 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,38 +0,0 @@
-(* Title: HOL/Real/HahnBanach/Zorn_Lemma.thy
- ID: $Id$
- Author: Gertrud Bauer, TU Munich
-*)
-
-header {* Zorn's Lemma *};
-
-theory Zorn_Lemma = Aux + Zorn:;
-
-lemma Zorn's_Lemma:
- "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);
- 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";
- proof;
- fix c; assume "c:chain S";
-
- show "EX y:S. ALL z:c. z <= y";
- proof (rule case_split [of "c={}"]);
- assume "c={}";
- with aS; show ?thesis; by fast;
- next;
- assume c: "c~={}";
- show ?thesis;
- proof;
- show "ALL z:c. z <= Union c"; by fast;
- show "Union c : S";
- proof (rule r);
- from c; show "EX x. x:c"; by fast;
- qed;
- qed;
- qed;
- qed;
-qed;
-
-end;
\ No newline at end of file
--- a/src/HOL/Real/HahnBanach/document/notation.tex Fri Oct 22 18:41:00 1999 +0200
+++ b/src/HOL/Real/HahnBanach/document/notation.tex Fri Oct 22 20:14:31 1999 +0200
@@ -1,5 +1,7 @@
\renewcommand{\isamarkupheader}[1]{\section{#1}}
+\newcommand{\isasymbollambda}{${\mathtt{\lambda}}$}
+
\parindent 0pt \parskip 0.5ex
\newcommand{\name}[1]{\textsf{#1}}
@@ -9,12 +11,50 @@
\DeclareMathSymbol{\dshsym}{\mathalpha}{letters}{"2D}
\newcommand{\dsh}{\dshsym}
+\newenvironment{matharray}[1]{\[\begin{array}{#1}}{\end{array}\]}
+
+\newcommand{\ty}{{\mathbin{:\,}}}
\newcommand{\To}{\to}
\newcommand{\dt}{{\mathpunct.}}
-\newcommand{\ap}{\mathbin{\!}}
-\newcommand{\lam}[1]{\mathop{\lambda} #1\dt\;}
\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{\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{\norm}[1]{\|\, #1\,\|}
+\newcommand{\fnorm}[1]{\|\, #1\,\|}
+\newcommand{\zero}{{\mathord{\mathbf {0}}}}
+\newcommand{\plus}{{\mathbin{\;\mathtt {+}\;}}}
+\newcommand{\minus}{{\mathbin{\;\mathtt {-}\;}}}
+\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:
%%% mode: latex
--- a/src/HOL/Real/HahnBanach/document/root.tex Fri Oct 22 18:41:00 1999 +0200
+++ b/src/HOL/Real/HahnBanach/document/root.tex Fri Oct 22 20:14:31 1999 +0200
@@ -1,21 +1,63 @@
-\documentclass[11pt,a4paper]{article}
-\usepackage{isabelle,pdfsetup}
+\documentclass[11pt,a4paper,twoside]{article}
+
+\usepackage{comment}
+\usepackage{latexsym,theorem}
+\usepackage{isabelle,pdfsetup} %last one!
\input{notation}
\begin{document}
+\pagestyle{headings}
+\pagenumbering{arabic}
+
\title{The Hahn-Banach Theorem for Real Vectorspaces}
\author{Gertrud Bauer}
\maketitle
\begin{abstract}
- FIXME
+The Hahn-Banach theorem is one of the most important theorems
+of functional analysis. We present the fully formal proof of two versions of
+the theorem, one for general linear spaces and one for normed spaces
+as a corollary of the first.
+
+The first part contains the definition of basic notions of
+linear algebra, such as vector spaces, subspaces, normed spaces,
+continous linearforms, 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 the extension of a non-maximal function,
+which are needed for the proof of the main theorem.
+
+The third part is the proof of the theorem in its two different versions.
+
\end{abstract}
\tableofcontents
-\input{session}
+\part {Basic notions}
+
+\input{Bounds.tex}
+\input{Aux.tex}
+\input{VectorSpace.tex}
+\input{Subspace.tex}
+\input{NormedSpace.tex}
+\input{Linearform.tex}
+\input{FunctionOrder.tex}
+\input{FunctionNorm.tex}
+\input{ZornLemma.tex}
+
+\part {Lemmas for the proof}
+
+\input{HahnBanachSupLemmas.tex}
+\input{HahnBanachExtLemmas.tex}
+
+\part {The proof}
+
+\input{HahnBanach.tex}
+\bibliographystyle{abbrv}
+\bibliography{bib}
\end{document}