# HG changeset patch # User wenzelm # Date 940616071 -7200 # Node ID 5e5b9813cce741b3ca1937c62a609613b59886e5 # Parent 3cb310f40a3a193476c11c791a4c6342cda361e8 HahnBanach update by Gertrud Bauer; diff -r 3cb310f40a3a -r 5e5b9813cce7 src/HOL/IsaMakefile --- 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 diff -r 3cb310f40a3a -r 5e5b9813cce7 src/HOL/Real/HahnBanach/Aux.thy --- 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 diff -r 3cb310f40a3a -r 5e5b9813cce7 src/HOL/Real/HahnBanach/Bounds.thy --- 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 == \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 == \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 (\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 (\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 (\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 (\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); diff -r 3cb310f40a3a -r 5e5b9813cce7 src/HOL/Real/HahnBanach/FunctionNorm.thy --- 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; diff -r 3cb310f40a3a -r 5e5b9813cce7 src/HOL/Real/HahnBanach/FunctionOrder.thy --- 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 == \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; diff -r 3cb310f40a3a -r 5e5b9813cce7 src/HOL/Real/HahnBanach/HahnBanach.thy --- 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 == + "\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 == "\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; diff -r 3cb310f40a3a -r 5e5b9813cce7 src/HOL/Real/HahnBanach/HahnBanachExtLemmas.thy --- /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 = (\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 = (\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 = (\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 = (\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 diff -r 3cb310f40a3a -r 5e5b9813cce7 src/HOL/Real/HahnBanach/HahnBanachSupLemmas.thy --- /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 = "\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 = "\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 diff -r 3cb310f40a3a -r 5e5b9813cce7 src/HOL/Real/HahnBanach/HahnBanach_h0_lemmas.thy --- 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 diff -r 3cb310f40a3a -r 5e5b9813cce7 src/HOL/Real/HahnBanach/HahnBanach_lemmas.thy --- 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 diff -r 3cb310f40a3a -r 5e5b9813cce7 src/HOL/Real/HahnBanach/LinearSpace.thy --- 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 diff -r 3cb310f40a3a -r 5e5b9813cce7 src/HOL/Real/HahnBanach/Linearform.thy --- 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; diff -r 3cb310f40a3a -r 5e5b9813cce7 src/HOL/Real/HahnBanach/NormedSpace.thy --- 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"; diff -r 3cb310f40a3a -r 5e5b9813cce7 src/HOL/Real/HahnBanach/Subspace.thy --- 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 = (\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 = (\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. ((\(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; diff -r 3cb310f40a3a -r 5e5b9813cce7 src/HOL/Real/HahnBanach/VectorSpace.thy --- /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 "\" 70) + zero :: 'a ("\"); + +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 diff -r 3cb310f40a3a -r 5e5b9813cce7 src/HOL/Real/HahnBanach/ZornLemma.thy --- /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; diff -r 3cb310f40a3a -r 5e5b9813cce7 src/HOL/Real/HahnBanach/Zorn_Lemma.thy --- 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 diff -r 3cb310f40a3a -r 5e5b9813cce7 src/HOL/Real/HahnBanach/document/notation.tex --- 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 diff -r 3cb310f40a3a -r 5e5b9813cce7 src/HOL/Real/HahnBanach/document/root.tex --- 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}