--- a/src/HOL/Real/HahnBanach/Aux.thy Fri Oct 08 16:18:51 1999 +0200
+++ b/src/HOL/Real/HahnBanach/Aux.thy Fri Oct 08 16:40:27 1999 +0200
@@ -3,12 +3,21 @@
Author: Gertrud Bauer, TU Munich
*)
+header {* Auxiliary theorems *};
+
theory Aux = Real + Zorn:;
lemmas [intro!!] = chainD;
lemmas chainE2 = chainD2 [elimify];
lemmas [intro!!] = isLub_isUb;
+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+);
+
+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+);
lemma le_max1: "x <= max x (y::'a::linorder)";
by (simp add: le_max_iff_disj[of x x y]);
@@ -25,160 +34,94 @@
lemma real_add_minus_eq: "x - y = 0r ==> x = y";
proof -;
assume "x - y = 0r";
- have "x + - y = x - y"; by simp;
- also; have "... = 0r"; .;
- finally; have "x + - y = 0r"; .;
+ have "x + - y = 0r"; by (simp!);
hence "x = - (- y)"; by (rule real_add_minus_eq_minus);
also; have "... = y"; by simp;
- finally; show "x = y"; .;
+ finally; show "?thesis"; .;
qed;
lemma rabs_minus_one: "rabs (- 1r) = 1r";
proof -;
- have "rabs (- 1r) = - (- 1r)";
- proof (rule rabs_minus_eqI2);
- show "-1r < 0r";
- by (rule real_minus_zero_less_iff[RS iffD1], simp, rule real_zero_less_one);
- qed;
+ have "-1r < 0r";
+ by (rule real_minus_zero_less_iff[RS iffD1], simp,
+ rule real_zero_less_one);
+ hence "rabs (- 1r) = - (- 1r)";
+ by (rule rabs_minus_eqI2);
also; have "... = 1r"; by simp;
- finally; show ?thesis; by simp;
+ finally; show ?thesis; .;
qed;
-lemma real_mult_le_le_mono2: "[| 0r <= z; x <= y |] ==> x * z <= y * z";
+lemma real_mult_le_le_mono2:
+ "[| 0r <= z; x <= y |] ==> x * z <= y * z";
proof -;
- assume gz: "0r <= z" and ineq: "x <= y";
+ assume "0r <= z" "x <= y";
hence "x < y | x = y"; by (force simp add: order_le_less);
thus ?thesis;
proof (elim disjE);
assume "x < y"; show ?thesis; by (rule real_mult_le_less_mono1);
next;
- assume "x = y";
- hence "x * z <= y * z"; by simp;
- thus ?thesis; by fast;
+ assume "x = y"; thus ?thesis;; by simp;
qed;
qed;
-lemma real_mult_less_le_anti: "[| z < 0r; x <= y |] ==> z * y <= z * x";
+lemma real_mult_less_le_anti:
+ "[| z < 0r; x <= y |] ==> z * y <= z * x";
proof -;
- assume lz: "z < 0r" and ineq: "x <= y";
+ assume "z < 0r" "x <= y";
hence "0r < - z"; by simp;
hence "0r <= - z"; by (rule real_less_imp_le);
- with ineq; have "(- z) * x <= (- z) * y"; by (simp add: real_mult_le_le_mono1);
- hence "- (z * x) <= - (z * y)"; by (simp add: real_minus_mult_eq1 [RS sym]);
+ hence "(- z) * x <= (- z) * y";
+ by (rule real_mult_le_le_mono1);
+ hence "- (z * x) <= - (z * y)";
+ by (simp only: real_minus_mult_eq1);
thus ?thesis; by simp;
qed;
-lemma real_mult_less_le_mono: "[| 0r < z; x <= y |] ==> z * x <= z * y";
+lemma real_mult_less_le_mono:
+ "[| 0r < z; x <= y |] ==> z * x <= z * y";
proof -;
- assume gt: "0r < z" and ineq: "x <= y";
- from gt; have "0r <= z"; by (rule real_less_imp_le);
+ assume "0r < z" "x <= y";
+ have "0r <= z"; by (rule real_less_imp_le);
thus ?thesis; by (rule real_mult_le_le_mono1);
qed;
-lemma real_mult_diff_distrib: "a * (- x - (y::real)) = - a * x - a * y";
+lemma real_mult_diff_distrib:
+ "a * (- x - (y::real)) = - a * x - a * y";
proof -;
- have "- x - (y::real) = - x + - y"; by simp;
- also; have "a * ... = a * - x + a * - y"; by (simp add: real_add_mult_distrib2);
+ have "- x - y = - x + - y"; by simp;
+ also; have "a * ... = a * - x + a * - y";
+ by (simp only: real_add_mult_distrib2);
also; have "... = - a * x - a * y";
- by (simp add: real_minus_mult_eq2 [RS sym] real_minus_mult_eq1 [RS sym]);
+ by (simp add: real_minus_mult_eq2 [RS sym] real_minus_mult_eq1);
finally; show ?thesis; .;
qed;
lemma real_mult_diff_distrib2: "a * (x - (y::real)) = a * x - a * y";
proof -;
- have "x - (y::real) = x + - y"; by simp;
- also; have "a * ... = a * x + a * - y"; by (simp add: real_add_mult_distrib2);
+ have "x - y = x + - y"; by simp;
+ also; have "a * ... = a * x + a * - y";
+ by (simp only: real_add_mult_distrib2);
also; have "... = a * x - a * y";
- by (simp add: real_minus_mult_eq2 [RS sym] real_minus_mult_eq1 [RS sym]);
+ by (simp add: real_minus_mult_eq2 [RS sym] real_minus_mult_eq1);
finally; show ?thesis; .;
qed;
-lemma le_noteq_imp_less: "[|x <= (r::'a::order); x ~= r |] ==> x < r";
+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 minus_le: "- (x::real) <= y ==> - y <= x";
-proof -;
- assume "- x <= y";
- hence "- x < y | - x = y"; by (rule order_le_less [RS iffD1]);
- thus "-y <= x";
- proof;
- assume "- x < y"; show ?thesis;
- proof -;
- have "- y < - (- x)"; by (rule real_less_swap_iff [RS iffD1]);
- hence "- y < x"; by simp;
- thus ?thesis; by (rule real_less_imp_le);
- qed;
- next;
- assume "- x = y"; thus ?thesis; by force;
- qed;
-qed;
+lemma real_minus_le: "- (x::real) <= y ==> - y <= x";
+ by simp;
-lemma rabs_interval_iff_1: "(rabs (x::real) <= r) = (-r <= x & x <= r)";
-proof (rule case_split [of "rabs x = r"]);
- assume a: "rabs x = r";
- show ?thesis;
- proof;
- assume "rabs x <= r";
- show "- r <= x & x <= r";
- proof;
- have "- x <= rabs x"; by (rule rabs_ge_minus_self);
- with a; have "- x <= r"; by simp;
- thus "- r <= x"; by (simp add : minus_le [of "x" "r"]);
- have "x <= rabs x"; by (rule rabs_ge_self);
- with a; show "x <= r"; by simp;
- qed;
- next;
- assume "- r <= x & x <= r";
- with a; show "rabs x <= r"; by fast;
- qed;
-next;
- assume "rabs x ~= r";
- show ?thesis;
- proof;
- assume "rabs x <= r";
- have "rabs x < r"; by (rule conjI [RS real_less_le [RS iffD2]]);
- hence "- r < x & x < r"; by (rule rabs_interval_iff [RS iffD1]);
- thus "- r <= x & x <= r";
- proof(elim conjE, intro conjI);
- assume "- r < x";
- show "- r <= x"; by (rule real_less_imp_le);
- assume "x < r";
- show "x <= r"; by (rule real_less_imp_le);
- qed;
- next;
- assume "- r <= x & x <= r";
- thus "rabs x <= r";
- proof;
- assume a: "- r <= x" and "x <= r";
- show ?thesis;
- proof (rule rabs_disj [RS disjE, of x]);
- assume "rabs x = x";
- thus ?thesis; by simp;
- next;
- assume "rabs x = - x";
- with a minus_le [of r x]; show ?thesis; by simp;
- qed;
- qed;
- qed;
-qed;
-
-
-lemma real_diff_ineq_swap: "(d::real) - b <= c + a ==> - a - b <= c - d";
-proof -;
- assume "d - b <= c + (a::real)";
- have "- a - b = d - b + (- d - a)"; by (simp!);
- also; have "... <= c + a + (- d - a)"; by (rule real_add_le_mono1);
- also; have "... = c - d"; by (simp!);
- finally; show "- a - b <= c - d"; .;
-qed;
-
+lemma real_diff_ineq_swap:
+ "(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;
+end;
\ No newline at end of file
--- a/src/HOL/Real/HahnBanach/Bounds.thy Fri Oct 08 16:18:51 1999 +0200
+++ b/src/HOL/Real/HahnBanach/Bounds.thy Fri Oct 08 16:40:27 1999 +0200
@@ -3,10 +3,12 @@
Author: Gertrud Bauer, TU Munich
*)
+header {* Bounds *};
+
theory Bounds = Main + Real:;
-section {* The sets of lower and upper bounds *};
+subsection {* The sets of lower and upper bounds *};
constdefs
is_LowerBound :: "('a::order) set => 'a set => 'a => bool"
@@ -22,10 +24,14 @@
"UpperBounds A B == Collect (is_UpperBound A B)";
syntax
- "_UPPERS" :: "[pttrn, 'a set, 'a => bool] => 'a set" ("(3UPPER'_BOUNDS _:_./ _)" 10)
- "_UPPERS_U" :: "[pttrn, 'a => bool] => 'a set" ("(3UPPER'_BOUNDS _./ _)" 10)
- "_LOWERS" :: "[pttrn, 'a set, 'a => bool] => 'a set" ("(3LOWER'_BOUNDS _:_./ _)" 10)
- "_LOWERS_U" :: "[pttrn, 'a => bool] => 'a set" ("(3LOWER'_BOUNDS _./ _)" 10);
+ "_UPPERS" :: "[pttrn, 'a set, 'a => bool] => 'a set"
+ ("(3UPPER'_BOUNDS _:_./ _)" 10)
+ "_UPPERS_U" :: "[pttrn, 'a => bool] => 'a set"
+ ("(3UPPER'_BOUNDS _./ _)" 10)
+ "_LOWERS" :: "[pttrn, 'a set, 'a => bool] => 'a set"
+ ("(3LOWER'_BOUNDS _:_./ _)" 10)
+ "_LOWERS_U" :: "[pttrn, 'a => bool] => 'a set"
+ ("(3LOWER'_BOUNDS _./ _)" 10);
translations
"UPPER_BOUNDS x:A. P" == "UpperBounds A (Collect (%x. P))"
@@ -34,7 +40,7 @@
"LOWER_BOUNDS x. P" == "LOWER_BOUNDS x:UNIV. P";
-section {* Least and greatest elements *};
+subsection {* Least and greatest elements *};
constdefs
is_Least :: "('a::order) set => 'a => bool"
@@ -50,15 +56,17 @@
"Greatest B == Eps (is_Greatest B)";
syntax
- "_LEAST" :: "[pttrn, 'a => bool] => 'a" ("(3LLEAST _./ _)" 10)
- "_GREATEST" :: "[pttrn, 'a => bool] => 'a" ("(3GREATEST _./ _)" 10);
+ "_LEAST" :: "[pttrn, 'a => bool] => 'a"
+ ("(3LLEAST _./ _)" 10)
+ "_GREATEST" :: "[pttrn, 'a => bool] => 'a"
+ ("(3GREATEST _./ _)" 10);
translations
"LLEAST x. P" == "Least {x. P}"
"GREATEST x. P" == "Greatest {x. P}";
-section {* Inf and Sup *};
+subsection {* Infimum and Supremum *};
constdefs
is_Sup :: "('a::order) set => 'a set => 'a => bool"
@@ -74,10 +82,14 @@
"Inf A B == Eps (is_Inf A B)";
syntax
- "_SUP" :: "[pttrn, 'a set, 'a => bool] => 'a set" ("(3SUP _:_./ _)" 10)
- "_SUP_U" :: "[pttrn, 'a => bool] => 'a set" ("(3SUP _./ _)" 10)
- "_INF" :: "[pttrn, 'a set, 'a => bool] => 'a set" ("(3INF _:_./ _)" 10)
- "_INF_U" :: "[pttrn, 'a => bool] => 'a set" ("(3INF _./ _)" 10);
+ "_SUP" :: "[pttrn, 'a set, 'a => bool] => 'a set"
+ ("(3SUP _:_./ _)" 10)
+ "_SUP_U" :: "[pttrn, 'a => bool] => 'a set"
+ ("(3SUP _./ _)" 10)
+ "_INF" :: "[pttrn, 'a set, 'a => bool] => 'a set"
+ ("(3INF _:_./ _)" 10)
+ "_INF_U" :: "[pttrn, 'a => bool] => 'a set"
+ ("(3INF _./ _)" 10);
translations
"SUP x:A. P" == "Sup A (Collect (%x. P))"
@@ -85,7 +97,6 @@
"INF x:A. P" == "Inf A (Collect (%x. P))"
"INF x. P" == "INF x:UNIV. P";
-
lemma sup_le_ub: "isUb A B y ==> is_Sup A B s ==> s <= y";
by (unfold is_Sup_def, rule isLub_le_isUb);
@@ -100,5 +111,4 @@
finally; show "a <= s"; .;
qed;
-
-end;
+end;
\ No newline at end of file
--- a/src/HOL/Real/HahnBanach/FunctionNorm.thy Fri Oct 08 16:18:51 1999 +0200
+++ b/src/HOL/Real/HahnBanach/FunctionNorm.thy Fri Oct 08 16:40:27 1999 +0200
@@ -3,13 +3,15 @@
Author: Gertrud Bauer, TU Munich
*)
+header {* The norm of a function *};
+
theory FunctionNorm = NormedSpace + FunctionOrder:;
constdefs
is_continous :: "['a 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_continous V norm f ==
+ (is_linearform V f & (EX c. ALL x:V. rabs (f x) <= c * norm x))";
lemma lipschitz_continousI [intro]:
"[| is_linearform V f; !! x. x:V ==> rabs (f x) <= c * norm x |]
@@ -19,7 +21,8 @@
fix x; assume "x:V"; show "rabs (f x) <= c * norm x"; by (rule r);
qed;
-lemma continous_linearform [intro!!]: "is_continous V norm f ==> is_linearform V f";
+lemma continous_linearform [intro!!]:
+ "is_continous V norm f ==> is_linearform V f";
by (unfold is_continous_def) force;
lemma continous_bounded [intro!!]:
@@ -28,7 +31,8 @@
constdefs
B:: "[ 'a set, 'a => real, 'a => real ] => real set"
- "B V norm f == {z. z = 0r | (EX x:V. x ~= <0> & z = rabs (f x) * rinv (norm (x)))}";
+ "B V norm f ==
+ {z. z = 0r | (EX x:V. x ~= <0> & z = rabs (f x) * rinv (norm (x)))}";
constdefs
function_norm :: " ['a set, 'a => real, 'a => real] => real"
@@ -46,10 +50,11 @@
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";
+ assume "is_linearform V f"
+ and e: "EX c. ALL x:V. rabs (f x) <= c * norm x";
show "EX a. is_Sup UNIV (B V norm f) a";
proof (unfold is_Sup_def, rule reals_complete);
show "EX X. X : B V norm f";
@@ -76,10 +81,12 @@
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; (*** or:
+ by (rule real_less_imp_le, rule real_rinv_gt_zero,
+ rule normed_vs_norm_gt_zero); ***)
qed;
- also; have "... = c * (norm x * rinv (norm x))"; by (rule real_mult_assoc);
+ 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";
@@ -88,8 +95,9 @@
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); ***)
+ qed; (*** or:
+ 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);
@@ -101,7 +109,8 @@
qed;
qed;
-lemma fnorm_ge_zero [intro!!]: "[| is_continous V norm f; is_normed_vectorspace V norm|]
+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";
@@ -126,13 +135,13 @@
qed;
qed;
qed (simp!);
- from ex_fnorm [OF n c]; show "is_Sup UNIV (B V norm f) (Sup UNIV (B V norm f))";
+ 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);
show "0r : B V norm f"; by (rule B_not_empty);
qed;
qed;
-
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";
@@ -184,9 +193,6 @@
qed;
qed;
-
-
-
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 |]
@@ -198,7 +204,8 @@
and "0r <= c";
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))";
+ 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 "isUb UNIV (B V norm f) c";
proof (intro isUbI setleI ballI);
@@ -217,7 +224,8 @@
from lt; have "0r < rinv (norm x)";
by (simp! add: real_rinv_gt_zero);
- then; have inv_leq: "0r <= rinv (norm x)"; by (rule real_less_imp_le);
+ then; have inv_leq: "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)";
@@ -235,6 +243,4 @@
qed;
qed;
-
-end;
-
+end;
\ No newline at end of file
--- a/src/HOL/Real/HahnBanach/FunctionOrder.thy Fri Oct 08 16:18:51 1999 +0200
+++ b/src/HOL/Real/HahnBanach/FunctionOrder.thy Fri Oct 08 16:40:27 1999 +0200
@@ -3,10 +3,14 @@
Author: Gertrud Bauer, TU Munich
*)
+header {* An Order on Functions *};
+
theory FunctionOrder = Subspace + Linearform:;
-section {* Order on functions *};
+
+subsection {* The graph of a function *}
+
types 'a graph = "('a * real) set";
@@ -34,17 +38,20 @@
lemma graphD2 [intro!!]: "(x, y): graph H h ==> y = h x";
by (unfold graph_def, elim CollectE exE) force;
-lemma graph_extD1 [intro!!]: "[| graph H h <= graph H' h'; x:H |] ==> h x = h' x";
+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'";
by (unfold graph_def, force);
-lemma graph_extI: "[| !! x. x: H ==> h x = h' x; H <= H'|] ==> graph H h <= graph H' 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_domain_funct:
- "(!!x y z. (x, y):g ==> (x, z):g ==> z = y) ==> graph (domain g) (funct g) = g";
+ "(!!x y z. (x, y):g ==> (x, z):g ==> z = y)
+ ==> graph (domain g) (funct g) = g";
proof (unfold domain_def, unfold funct_def, unfold graph_def, auto);
fix a b; assume "(a, b) : g";
show "(a, SOME y. (a, y) : g) : g"; by (rule selectI2);
@@ -56,6 +63,11 @@
qed;
qed;
+
+
+subsection {* The set of norm preserving extensions of a function *}
+
+
constdefs
norm_pres_extensions ::
"['a set, 'a => real, 'a set, 'a => real] => 'a graph set"
@@ -94,6 +106,5 @@
==> (g: norm_pres_extensions E p F f) ";
by (unfold norm_pres_extensions_def) force;
-
end;
--- a/src/HOL/Real/HahnBanach/HahnBanach.thy Fri Oct 08 16:18:51 1999 +0200
+++ b/src/HOL/Real/HahnBanach/HahnBanach.thy Fri Oct 08 16:40:27 1999 +0200
@@ -3,28 +3,29 @@
Author: Gertrud Bauer, TU Munich
*)
-(* The proof of two different versions of the Hahn-Banach theorem,
- following H. Heuser, Funktionalanalysis, p. 228 - 232.
-*)
+header {* The Hahn-Banach theorem *};
theory HahnBanach = HahnBanach_lemmas + HahnBanach_h0_lemmas:;
+text {*
+ The proof of two different versions of the Hahn-Banach theorem,
+ following \cite{Heuser}.
+*};
-section {* The Hahn-Banach theorem for general linear spaces,
- H. Heuser, Funktionalanalysis, p.231 *};
+subsection {* The Hahn-Banach theorem for 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 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 *};
theorem hahnbanach:
- "[| is_vectorspace E; is_subspace F E; is_quasinorm E p; is_linearform F f;
- ALL x:F. f x <= p x |]
+ "[| 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
& (ALL x:F. h x = f x)
& (ALL x:E. h x <= p x)";
proof -;
- assume "is_vectorspace E" "is_subspace F E" "is_quasinorm E p" "is_linearform F f"
- "ALL x:F. f x <= p x";
+ assume "is_vectorspace E" "is_subspace F E" "is_quasinorm E p"
+ "is_linearform F f" "ALL x:F. f x <= p x";
def M == "norm_pres_extensions E p F f";
@@ -36,13 +37,10 @@
qed;
qed (blast!)+;
+ subsubsect {* Existence of a supremum of the norm preserving functions *};
- sect {* Part I b of the proof of the Hahn-Banach Theorem,
- H. Heuser, Funktionalanalysis, p.231 *};
-
- txt {* Every chain of norm presenting functions has a supremum in M *};
-
- have "!! (c:: 'a graph set). c : chain M ==> EX x. x:c ==> (Union c) : M";
+ have "!! (c:: 'a graph set). 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";
@@ -53,7 +51,8 @@
& 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");
+ & (ALL x::'a:H. h x <= p x)"
+ (is "EX (H::'a set) h::'a => real. ?Q H h");
proof (intro exI conjI);
let ?H = "domain (Union c)";
let ?h = "funct (Union c)";
@@ -101,7 +100,8 @@
thus ?thesis;
proof (elim exE conjE);
fix H h;
- assume "graph H h = g" "is_linearform (H::'a set) h" "is_subspace H E" "is_subspace F 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";
@@ -110,203 +110,218 @@
have h: "is_vectorspace H"; ..;
have f: "is_vectorspace F"; ..;
- sect {* Part I a of the proof of the Hahn-Banach Theorem,
- H. Heuser, Funktionalanalysis, p.230 *};
-
- txt {* the maximal norm-preserving function is defined on whole E *};
+subsubsect {* The supremal norm-preserving function is defined on the
+ whole vectorspace *};
- have eq: "H = E";
- proof (rule classical);
-
- txt {* assume h is not defined on whole E *};
-
- assume "H ~= E";
- show ?thesis;
- proof -;
+have eq: "H = E";
+proof (rule classical);
- have "EX x:M. g <= x & g ~= x";
- proof -;
-
- txt {* h can be extended norm-preserving to H0 *};
+txt {* assume h is not defined on whole E *};
- 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";
+ assume "H ~= E";
+ show ?thesis;
+ proof -;
- have x0: "x0 ~= <0>";
- proof (rule classical);
- presume "x0 = <0>";
- with h; have "x0:H"; by simp;
- thus ?thesis; by contradiction;
- qed force;
+ have "EX x:M. g <= x & g ~= x";
+ proof -;
- 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 {* h can be extended norm-preserving to H0 *};
- 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 (simp! add: vs_add_minus_eq_diff);
- also; have "... = v [+] x0 [+] [-] (u [+] x0)"; by (simp!);
- also; have "... = (v [+] x0) [-] (u [+] x0)";
- by (simp! only: vs_add_minus_eq_diff);
- 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 "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 "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);
+ have x0: "x0 ~= <0>";
+ proof (rule classical);
+ presume "x0 = <0>";
+ with h; have "x0:H"; by simp;
+ thus ?thesis; by contradiction;
+ qed force;
- 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);
-
- 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 == "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);
- 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;
- qed;
- thus ?thesis; ..;
+ 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";
- thus ?thesis;
- by (elim exE conjE, intro bexI conjI);
- qed;
- hence "~ (ALL x:M. g <= x --> g = x)"; by force;
- thus ?thesis; by contradiction;
- qed;
- qed;
+ 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!)+;
+
+ show "is_subspace H0 E";
+ by (unfold H0_def, rule vs_sum_subspace,
+ rule lin_subspace);
- show "is_linearform E h & (ALL x:F. h x = f x) & (ALL x:E. h x <= p x)";
- proof (intro conjI);
- from eq; show "is_linearform E h"; by (simp!);
- show "ALL x:F. h x = f x";
- proof (intro ballI, rule sym);
- fix x; assume "x:F"; show "f x = h x "; ..;
+ 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!)+;
+
+ 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;
qed;
- from eq; show "ALL x:E. h x <= p x"; by (force!);
+ thus ?thesis; ..;
qed;
- qed;
- qed;
+ qed;
+
+ thus ?thesis;
+ by (elim exE conjE, intro bexI conjI);
+ qed;
+ hence "~ (ALL x:M. g <= x --> g = x)"; by force;
+ thus ?thesis; by contradiction;
qed;
+qed;
+
+show "is_linearform E h & (ALL x:F. h x = f x)
+ & (ALL x:E. h x <= p x)";
+proof (intro conjI);
+ from eq; show "is_linearform E h"; by (simp!);
+ show "ALL x:F. h x = f x";
+ proof (intro ballI, rule sym);
+ 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;
-
-section {* Part I (for real linear spaces) of the proof of the Hahn-banach Theorem,
- H. Heuser, Funktionalanalysis, p.229 *};
-
-text {* Alternative Formulation of the theorem *};
+subsection {* Alternative formulation of the theorem *};
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
- & (ALL x:F. g x = f x)
- & (ALL x:E. rabs (g x) <= p x)";
+ "[| 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
+ & (ALL x:F. g x = f x)
+ & (ALL x:E. rabs (g x) <= p x)";
proof -;
-
- assume e: "is_vectorspace E" and "is_subspace F E" "is_quasinorm E p" "is_linearform F f"
- "ALL x:F. rabs (f x) <= p x";
+ 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]);
- hence "EX g. is_linearform E g & (ALL x:F. g x = f x) & (ALL x:E. g x <= p x)";
+ 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);
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";
+ 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)+;
from e; show "ALL x:E. rabs (g x) <= p x";
@@ -316,8 +331,7 @@
qed;
-section {* The Hahn-Banach theorem for normd spaces,
- H. Heuser, Funktionalanalysis, p.232 *};
+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 *};
@@ -330,9 +344,7 @@
& (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");
-
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";
@@ -341,7 +353,8 @@
def p == "%x::'a. (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)";
+ let ?P' = "%g. is_linearform E g & (ALL x:F. g x = f x)
+ & (ALL x:E. rabs (g x) <= p x)";
have q: "is_quasinorm E p";
proof;
@@ -355,9 +368,12 @@
show "p (a [*] x) = (rabs a) * (p x)";
proof -;
- have "p (a [*] x) = (function_norm F norm f) * norm (a [*] x)"; by (simp!);
- also; have "norm (a [*] x) = rabs a * norm x"; by (rule normed_vs_norm_mult_distrib);
- also; have "(function_norm F norm f) * ... = rabs a * ((function_norm F norm f) * norm x)";
+ have "p (a [*] x) = (function_norm F norm f) * norm (a [*] x)";
+ by (simp!);
+ also; have "norm (a [*] x) = rabs a * norm x";
+ by (rule normed_vs_norm_mult_distrib);
+ also; have "(function_norm F norm f) * ...
+ = rabs a * ((function_norm F norm f) * norm x)";
by (simp! only: real_mult_left_commute);
also; have "... = (rabs a) * (p x)"; by (simp!);
finally; show ?thesis; .;
@@ -365,13 +381,15 @@
show "p (x [+] y) <= p x + p y";
proof -;
- 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)";
+ 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)";
proof (rule real_mult_le_le_mono1);
from _ f; 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;
@@ -380,7 +398,8 @@
have "ALL x:F. rabs (f x) <= p x";
proof;
fix x; assume "x:F";
- from f; show "rabs (f x) <= p x"; by (simp! add: norm_fx_le_norm_f_norm_x);
+ from f; 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";
@@ -389,7 +408,8 @@
thus "?thesis";
proof (elim exE conjE, intro exI conjI);
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";
+ 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";
@@ -398,7 +418,8 @@
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";
+ 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";
proof;
@@ -415,14 +436,16 @@
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";
+ 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;
- finally; show "rabs (f x) <= function_norm E norm g * norm x"; .;
+ 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"; ..;
@@ -431,6 +454,4 @@
qed;
qed;
-
-end;
-
+end;
\ No newline at end of file
--- a/src/HOL/Real/HahnBanach/HahnBanach_h0_lemmas.thy Fri Oct 08 16:18:51 1999 +0200
+++ b/src/HOL/Real/HahnBanach/HahnBanach_h0_lemmas.thy Fri Oct 08 16:40:27 1999 +0200
@@ -3,11 +3,14 @@
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)";
+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))";
@@ -74,17 +77,19 @@
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";
+ "[| 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";
+ 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);
@@ -101,7 +106,7 @@
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)";
+ 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";
@@ -116,9 +121,12 @@
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";
+ 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;
@@ -145,7 +153,8 @@
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)";
+ 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)";
@@ -162,7 +171,8 @@
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;
+ also; from vs y1'; have "... = c [*] y1 [+] (c * a1) [*] x0";
+ by simp;
finally; show ?thesis; by (rule sym);
qed;
show "c [*] y1: H"; ..;
@@ -184,28 +194,23 @@
qed;
qed;
-
-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+);
-
-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+);
-
-
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)|]
+ "[| 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";
+ 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";
@@ -227,10 +232,12 @@
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";
+ 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))";
+ 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);
@@ -257,12 +264,15 @@
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!);
+ 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))";
+ 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))";
+ 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))";
@@ -287,5 +297,4 @@
qed;
qed blast+;
-
end;
\ No newline at end of file
--- a/src/HOL/Real/HahnBanach/HahnBanach_lemmas.thy Fri Oct 08 16:18:51 1999 +0200
+++ b/src/HOL/Real/HahnBanach/HahnBanach_lemmas.thy Fri Oct 08 16:40:27 1999 +0200
@@ -3,13 +3,17 @@
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");
+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";
+ assume "is_subspace H E" "is_vectorspace E" "is_quasinorm E p"
+ "is_linearform H h";
have h: "is_vectorspace H"; ..;
show ?thesis;
proof;
@@ -30,12 +34,14 @@
show "rabs (h x) <= p x";
proof -;
show "!! r x. [| - r <= x; x <= r |] ==> rabs x <= r";
- by (simp add: rabs_interval_iff_1);
- show "- p x <= h x"; thm minus_le;
- proof (rule minus_le);
- from h; have "- h x = h ([-] x)"; by (rule linearform_neg_linear [RS sym]);
+ 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);
+ 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"; ..;
@@ -45,10 +51,12 @@
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)";
+ "[| 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";
@@ -72,16 +80,18 @@
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);
+ 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)";
+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";
@@ -100,25 +110,29 @@
& 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);
+ & (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);
+ 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' &
+ "[| 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";
+ 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
@@ -126,12 +140,12 @@
& (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'";
+ 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'";
+ 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;
@@ -147,7 +161,8 @@
"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'')";
+ have "(graph H'' h'') <= (graph H' h')
+ | (graph H' h') <= (graph H'' h'')";
by (rule chainD);
thus "?thesis";
proof;
@@ -179,15 +194,18 @@
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";
+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";
+ 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";
+ 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);
@@ -225,11 +243,12 @@
qed;
qed;
-
-lemma sup_lf: "[| M = norm_pres_extensions E p F f; c: chain M; graph H h = Union c|]
+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";
+ 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
@@ -242,9 +261,10 @@
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)";
+ 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);
@@ -253,7 +273,8 @@
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'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'"; ..;
@@ -263,14 +284,14 @@
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)";
+ 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);
@@ -278,7 +299,8 @@
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'ax: "h' (a [*] x) = a * h' x";
+ by (rule linearform_mult_linear);
have "h' (a [*] x) = h (a [*] x)";
proof -;
have "a [*] x : H'"; ..;
@@ -291,12 +313,13 @@
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";
+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";
+ 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);
@@ -331,10 +354,12 @@
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";
+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"
+ 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;
@@ -359,11 +384,12 @@
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";
+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";
+ 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;
@@ -380,9 +406,9 @@
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)";
+ 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);
@@ -400,13 +426,15 @@
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)";
+ 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";
+ 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);
@@ -427,7 +455,8 @@
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";
+ fix H' h';
+ assume "x:H'" "is_subspace H' E" "graph H' h' <= graph H h";
have "H' <= H"; ..;
thus ?thesis;
proof (rule subsetD);
@@ -439,21 +468,22 @@
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";
+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";
+ 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)";
+ 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" ;
+ 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"; ..;
@@ -464,5 +494,4 @@
qed;
qed;
-
-end;
+end;
\ No newline at end of file
--- a/src/HOL/Real/HahnBanach/LinearSpace.thy Fri Oct 08 16:18:51 1999 +0200
+++ b/src/HOL/Real/HahnBanach/LinearSpace.thy Fri Oct 08 16:40:27 1999 +0200
@@ -3,96 +3,107 @@
Author: Gertrud Bauer, TU Munich
*)
+header {* Linear Spaces *};
+
theory LinearSpace = Bounds + Aux:;
-
-section {* vector spaces *};
+subsection {* Signature *};
consts
- sum :: "['a, 'a] => 'a" (infixl "[+]" 65)
- prod :: "[real, 'a] => 'a" (infixr "[*]" 70)
- zero :: 'a ("<0>");
+ sum :: "['a, 'a] => 'a" (infixl "[+]" 65)
+ prod :: "[real, 'a] => 'a" (infixr "[*]" 70)
+ zero :: 'a ("<0>");
constdefs
- negate :: "'a => 'a" ("[-] _" [100] 100)
+ negate :: "'a => 'a" ("[-] _" [100] 100)
"[-] x == (- 1r) [*] x"
- diff :: "'a => 'a => 'a" (infixl "[-]" 68)
+ diff :: "'a => 'a => 'a" (infixl "[-]" 68)
"x [-] y == x [+] [-] y";
+subsection {* Vector space laws *}
+(***
constdefs
is_vectorspace :: "'a set => bool"
- "is_vectorspace V == <0>: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)";
-
-
-subsection {* neg, diff *};
-
-lemma vs_mult_minus_1: "(- 1r) [*] x = [-] x";
- by (simp add: negate_def);
-
-lemma vs_add_mult_minus_1_eq_diff: "x [+] (- 1r) [*] y = x [-] y";
- by (simp add: diff_def negate_def);
-
-lemma vs_add_minus_eq_diff: "x [+] [-] y = x [-] y";
- by (simp add: diff_def);
+ "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 a::real. 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::real. a [*] (x [+] y) = a [*] x [+] a [*] y; \
- \ ALL x: V. ALL a::real. ALL b::real. (a + b) [*] x = a [*] x [+] b [*] x; \
- \ ALL x: V. ALL a::real. ALL b::real. (a * b) [*] x = a [*] b [*] x; \
- \ ALL x: V. 1r [*] x = x |] ==> is_vectorspace 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 zero_in_vs [simp, intro]: "is_vectorspace V ==> <0>:V";
+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_not_empty [intro !!]: "is_vectorspace V ==> (V ~= {})";
- by (unfold is_vectorspace_def) fast;
-
-lemma vs_add_closed [simp, intro!!]: "[| is_vectorspace V; x: V; y: V|] ==> x [+] y: V";
+lemma vs_mult_closed [simp, intro!!]:
+ "[| is_vectorspace V; x: V |] ==> a [*] x: 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";
+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";
+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)";
+ "[| 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";
+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)";
+ "[| 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);
+ 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; .;
@@ -100,13 +111,30 @@
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>";
+lemma vs_diff_self [simp]:
+ "[| is_vectorspace V; x:V |] ==> x [-] x = <0>";
by (unfold is_vectorspace_def) simp;
-lemma vs_add_zero_left [simp]: "[| is_vectorspace V; x:V |] ==> <0> [+] x = x";
+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";
+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;
@@ -115,53 +143,67 @@
qed;
lemma vs_add_mult_distrib1:
- "[| is_vectorspace V; x:V; y:V |] ==> a [*] (x [+] y) = a [*] x [+] a [*] y";
+ "[| 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";
+ "[| 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_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";
+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";
+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";
+ "[| 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)";
+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)";
+ "[| 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);
+ 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>";
+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 "... = 1r [*] x [+] (- 1r) [*] x";
+ by (rule vs_add_mult_distrib2);
also; have "... = x [+] (- 1r) [*] x"; by (simp!);
- also; have "... = x [-] x"; by (rule vs_add_mult_minus_1_eq_diff);
+ 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)";
+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!);
@@ -171,38 +213,46 @@
finally; show ?thesis; .;
qed;
-lemma vs_minus_mult_cancel [simp]: "[| is_vectorspace V; x:V |] ==> (- a) [*] [-] x = a [*] x";
+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";
+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! only: vs_add_minus_eq_diff);
+ 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 (simp add: vs_add_minus_eq_diff);
+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 (simp add: vs_add_minus_eq_diff);
+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";
+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>";
+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");
+ "[| 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 (rule l [RS arg_cong] );
+ also; have "... = [-] <0>"; by (simp only: l);
also; have "... = <0>"; by (rule vs_minus_zero);
finally; show ?R; .;
next;
@@ -211,33 +261,41 @@
qed;
qed;
-lemma vs_add_minus_cancel [simp]: "[| is_vectorspace V; x:V; y:V|] ==> x [+] ([-] x [+] y) = y";
+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";
+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";
+ "[| 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";
+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";
+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)"
+ "[| 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 [+] 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 "... = [-] x [+] x [+] z";
+ by (rule vs_add_assoc [RS sym]) (simp!)+;
also; have "... = z"; by (simp!);
finally; show ?R;.;
next;
@@ -246,15 +304,18 @@
qed;
lemma vs_add_right_cancel:
- "[| is_vectorspace V; x:V; y:V; z:V |] ==> (y [+] x = z [+] x) = (y = z)";
+ "[| 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 |]
+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]);
+ 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";
+ "[| 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 :
@@ -271,14 +332,16 @@
qed;
lemma vs_mult_left_cancel:
- "[| is_vectorspace V; x:V; y:V; a ~= 0r |] ==> (a [*] x = a [*] y) = (x = y)"
+ "[| 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 [*] 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;.;
@@ -287,12 +350,27 @@
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;
+ assume l: ?L;
show "a = b";
proof (rule real_add_minus_eq);
show "a - b = 0r";
@@ -306,9 +384,11 @@
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)"
+ "[| 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";
@@ -316,60 +396,74 @@
proof;
assume l: ?L;
have "x [+] y = z [-] y [+] y"; by (simp add: l);
- also; have "... = z [+] [-] y [+] y"; by (simp only: vs_add_minus_eq_diff);
- 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; 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 (simp only: vs_add_minus_eq_diff);
- also; have "... = x [+] (y [+] [-] y)"; by (rule vs_add_assoc) (simp!)+;
+ 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";
+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 (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";
+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 "[-] 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";
+ "[| 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);
+ 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);
+ 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)"
+ "[| 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";
@@ -378,22 +472,26 @@
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 [+] (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 "... = [-] 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]);
+ 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)"
+ "[| 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";
@@ -404,7 +502,8 @@
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);
+ 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);
@@ -412,7 +511,8 @@
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 [+] ([-] z [+] z)";
+ by (simp! only: vs_add_left_commute);
also; have "... = y [+] <0>"; by (simp!);
also; have "... = y"; by (simp!);
finally; show ?L; .;
@@ -422,5 +522,4 @@
lemma it: "[| x = y; x' = y'|] ==> x [+] x' = y [+] y'";
by simp;
-
end;
\ No newline at end of file
--- a/src/HOL/Real/HahnBanach/Linearform.thy Fri Oct 08 16:18:51 1999 +0200
+++ b/src/HOL/Real/HahnBanach/Linearform.thy Fri Oct 08 16:40:27 1999 +0200
@@ -3,9 +3,9 @@
Author: Gertrud Bauer, TU Munich
*)
-theory Linearform = LinearSpace:;
+header {* Linearforms *};
-section {* linearforms *};
+theory Linearform = LinearSpace:;
constdefs
is_linearform :: "['a set, 'a => real] => bool"
@@ -13,7 +13,8 @@
(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;
+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 |]
==> is_linearform V f";
by (unfold is_linearform_def) force;
@@ -30,30 +31,33 @@
"[| is_vectorspace V; is_linearform V f; x:V|] ==> f ([-] x) = - f x";
proof -;
assume "is_linearform V f" "is_vectorspace V" "x:V";
- have "f ([-] x) = f ((- 1r) [*] x)"; by (simp! add: vs_mult_minus_1);
+ have "f ([-] x) = f ((- 1r) [*] x)"; by (unfold negate_def) simp;
also; have "... = (- 1r) * (f x)"; by (rule linearform_mult_linear);
also; have "... = - (f x)"; by (simp!);
finally; show ?thesis; .;
qed;
lemma linearform_diff_linear [intro!!]:
- "[| is_vectorspace V; is_linearform V f; x:V; y:V |] ==> f (x [-] y) = f x - f y";
+ "[| is_vectorspace V; is_linearform V f; x:V; y:V |]
+ ==> f (x [-] y) = f x - f y";
proof -;
assume "is_vectorspace V" "is_linearform V f" "x:V" "y:V";
have "f (x [-] y) = f (x [+] [-] y)"; by (simp only: diff_def);
- also; have "... = f x + f ([-] y)"; by (rule linearform_add_linear) (simp!)+;
+ 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!);
qed;
-lemma linearform_zero [intro!!, simp]: "[| is_vectorspace V; is_linearform V f |] ==> f <0> = 0r";
+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!);
- also; have "... = f <0> - f <0>"; by (rule linearform_diff_linear) (simp!)+;
+ also; have "... = f <0> - f <0>";
+ by (rule linearform_diff_linear) (simp!)+;
also; have "... = 0r"; by simp;
finally; show "f <0> = 0r"; .;
qed;
-end;
-
+end;
\ No newline at end of file
--- a/src/HOL/Real/HahnBanach/NormedSpace.thy Fri Oct 08 16:18:51 1999 +0200
+++ b/src/HOL/Real/HahnBanach/NormedSpace.thy Fri Oct 08 16:40:27 1999 +0200
@@ -3,12 +3,14 @@
Author: Gertrud Bauer, TU Munich
*)
+header {* Normed vector spaces *};
+
theory NormedSpace = Subspace:;
-section {* normed vector spaces *};
-subsection {* quasinorm *};
+subsection {* Quasinorms *};
+
constdefs
is_quasinorm :: "['a set, 'a => real] => bool"
@@ -17,7 +19,7 @@
& norm (a [*] x) = (rabs a) * (norm x)
& norm (x [+] y) <= norm x + norm y";
-lemma is_quasinormI[intro]:
+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 |]
@@ -29,36 +31,46 @@
by (unfold is_quasinorm_def, force);
lemma quasinorm_mult_distrib:
- "[| is_quasinorm V norm; x:V |] ==> norm (a [*] x) = (rabs a) * (norm x)";
+ "[| is_quasinorm V norm; x:V |]
+ ==> 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";
+ "[| is_quasinorm V norm; x:V; y:V |]
+ ==> 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";
+ "[| is_quasinorm V norm; x:V; y:V; is_vectorspace V |]
+ ==> norm (x [-] y) <= norm x + norm y";
proof -;
assume "is_quasinorm V norm" "x:V" "y:V" "is_vectorspace V";
- have "norm (x [-] y) = norm (x [+] - 1r [*] y)"; by (simp add: diff_def negate_def);
- also; have "... <= norm x + norm (- 1r [*] y)"; by (simp! add: quasinorm_triangle_ineq);
- also; have "norm (- 1r [*] y) = rabs (- 1r) * norm y"; by (rule quasinorm_mult_distrib);
+ have "norm (x [-] y) = norm (x [+] - 1r [*] y)";
+ by (simp add: diff_def negate_def);
+ also; have "... <= norm x + norm (- 1r [*] y)";
+ by (simp! add: quasinorm_triangle_ineq);
+ 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;
qed;
lemma quasinorm_minus:
- "[| is_quasinorm V norm; x:V; is_vectorspace V |] ==> norm ([-] x) = norm x";
+ "[| is_quasinorm V norm; x:V; is_vectorspace V |]
+ ==> norm ([-] x) = norm x";
proof -;
assume "is_quasinorm V norm" "x:V" "is_vectorspace V";
have "norm ([-] x) = norm (-1r [*] x)"; by (unfold negate_def) force;
- also; have "... = rabs (-1r) * norm x"; by (rule quasinorm_mult_distrib);
+ 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;
qed;
-subsection {* norm *};
+
+subsection {* Norms *};
+
constdefs
is_norm :: "['a set, 'a => real] => bool"
@@ -66,13 +78,16 @@
& (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";
+ "ALL x: V. is_quasinorm V norm & (norm x = 0r) = (x = <0>)
+ ==> is_norm V norm";
by (unfold is_norm_def, force);
-lemma norm_is_quasinorm [intro!!]: "[| is_norm V norm; x:V |] ==> is_quasinorm V norm";
+lemma norm_is_quasinorm [intro!!]:
+ "[| is_norm V norm; x:V |] ==> is_quasinorm V norm";
by (unfold is_norm_def, force);
-lemma norm_zero_iff: "[| is_norm V norm; x:V |] ==> (norm x = 0r) = (x = <0>)";
+lemma norm_zero_iff:
+ "[| is_norm V norm; x:V |] ==> (norm x = 0r) = (x = <0>)";
by (unfold is_norm_def, force);
lemma norm_ge_zero [intro!!]:
@@ -80,7 +95,8 @@
by (unfold is_norm_def is_quasinorm_def, force);
-subsection {* normed vector space *};
+subsection {* Normed vector spaces *};
+
constdefs
is_normed_vectorspace :: "['a set, 'a => real] => bool"
@@ -89,16 +105,20 @@
is_norm V norm";
lemma normed_vsI [intro]:
- "[| is_vectorspace V; is_norm V norm |] ==> is_normed_vectorspace V norm";
+ "[| is_vectorspace V; is_norm V norm |]
+ ==> is_normed_vectorspace V norm";
by (unfold is_normed_vectorspace_def) blast;
-lemma normed_vs_vs [intro!!]: "is_normed_vectorspace V norm ==> is_vectorspace V";
+lemma normed_vs_vs [intro!!]:
+ "is_normed_vectorspace V norm ==> is_vectorspace V";
by (unfold is_normed_vectorspace_def) force;
-lemma normed_vs_norm [intro!!]: "is_normed_vectorspace V norm ==> is_norm V norm";
+lemma normed_vs_norm [intro!!]:
+ "is_normed_vectorspace V norm ==> is_norm V norm";
by (unfold is_normed_vectorspace_def, elim conjE);
-lemma normed_vs_norm_ge_zero [intro!!]: "[| is_normed_vectorspace V norm; x:V |] ==> 0r <= norm x";
+lemma normed_vs_norm_ge_zero [intro!!]:
+ "[| is_normed_vectorspace V norm; x:V |] ==> 0r <= norm x";
by (unfold is_normed_vectorspace_def, rule, elim conjE);
lemma normed_vs_norm_gt_zero [intro!!]:
@@ -117,18 +137,23 @@
qed;
lemma normed_vs_norm_mult_distrib [intro!!]:
- "[| is_normed_vectorspace V norm; x:V |] ==> norm (a [*] x) = (rabs a) * (norm x)";
- by (rule quasinorm_mult_distrib, rule norm_is_quasinorm, rule normed_vs_norm);
+ "[| is_normed_vectorspace V norm; x:V |]
+ ==> 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";
- by (rule quasinorm_triangle_ineq, rule norm_is_quasinorm, rule normed_vs_norm);
+ "[| is_normed_vectorspace V norm; x:V; y:V |]
+ ==> norm (x [+] y) <= norm x + norm y";
+ by (rule quasinorm_triangle_ineq, rule norm_is_quasinorm,
+ rule normed_vs_norm);
lemma subspace_normed_vs [intro!!]:
"[| 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";
+ assume "is_subspace F E" "is_vectorspace E"
+ "is_normed_vectorspace E norm";
show "is_vectorspace F"; ..;
show "is_norm F norm";
proof (intro is_normI ballI conjI);
@@ -149,4 +174,4 @@
qed;
qed;
-end;
+end;
\ No newline at end of file
--- a/src/HOL/Real/HahnBanach/ROOT.ML Fri Oct 08 16:18:51 1999 +0200
+++ b/src/HOL/Real/HahnBanach/ROOT.ML Fri Oct 08 16:40:27 1999 +0200
@@ -5,4 +5,5 @@
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar).
*)
+time_use_thy "Bounds";
time_use_thy "HahnBanach";
--- a/src/HOL/Real/HahnBanach/Subspace.thy Fri Oct 08 16:18:51 1999 +0200
+++ b/src/HOL/Real/HahnBanach/Subspace.thy Fri Oct 08 16:40:27 1999 +0200
@@ -3,10 +3,13 @@
Author: Gertrud Bauer, TU Munich
*)
+
+header {* Subspaces *};
+
theory Subspace = LinearSpace:;
-section {* subspaces *};
+subsection {* Subspaces *};
constdefs
is_subspace :: "['a set, 'a set] => bool"
@@ -15,8 +18,9 @@
& 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 |]
- \ ==> is_subspace U V";
+ "[| <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;
lemma "is_subspace U V ==> U ~= {}";
@@ -28,23 +32,27 @@
lemma subspace_subset [intro !!]: "is_subspace U V ==> U <= V";
by (unfold is_subspace_def) simp;
-lemma subspace_subsetD [simp, intro!!]: "[| is_subspace U V; x:U |]==> x:V";
+lemma subspace_subsetD [simp, intro!!]:
+ "[| is_subspace U V; x:U |]==> x:V";
by (unfold is_subspace_def) force;
-lemma subspace_add_closed [simp, intro!!]: "[| is_subspace U V; x: U; y: U |] ==> x [+] y: U";
- by (unfold is_subspace_def) simp;
-
-lemma subspace_mult_closed [simp, intro!!]: "[| is_subspace U V; x: U |] ==> a [*] x: U";
+lemma subspace_add_closed [simp, intro!!]:
+ "[| is_subspace U V; x: U; y: U |] ==> x [+] y: U";
by (unfold is_subspace_def) simp;
-lemma subspace_diff_closed [simp, intro!!]: "[| is_subspace U V; x: U; y: U |] ==> x [-] y: U";
+lemma subspace_mult_closed [simp, intro!!]:
+ "[| 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;
-lemma subspace_neg_closed [simp, intro!!]: "[| is_subspace U V; x: U |] ==> [-] x: U";
- by (unfold negate_def) simp;
+lemma subspace_neg_closed [simp, intro!!]:
+ "[| is_subspace U V; x: U |] ==> [-] x: U";
+ by (unfold negate_def) simp;
-
-theorem subspace_vs [intro!!]:
+lemma subspace_vs [intro!!]:
"[| is_subspace U V; is_vectorspace V |] ==> is_vectorspace U";
proof -;
assume "is_subspace U V" "is_vectorspace V";
@@ -65,7 +73,8 @@
show "ALL x:V. ALL a. a [*] x : V"; by (simp!);
qed;
-lemma subspace_trans: "[| is_subspace U V; is_subspace V W |] ==> is_subspace U W";
+lemma subspace_trans:
+ "[| is_subspace U V; is_subspace V W |] ==> is_subspace U W";
proof;
assume "is_subspace U V" "is_subspace V W";
show "<0> : U"; ..;
@@ -88,7 +97,9 @@
qed;
-section {* linear closure *};
+
+subsection {* Linear closure *};
+
constdefs
lin :: "'a => 'a set"
@@ -106,7 +117,8 @@
show "x = 1r [*] x"; by (simp!);
qed;
-lemma lin_subspace [intro!!]: "[| is_vectorspace V; x:V |] ==> is_subspace (lin x) V";
+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";
@@ -126,7 +138,8 @@
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"; by (simp! add: vs_add_mult_distrib2);
+ show "x1 [+] x2 = (a1 + a2) [*] x";
+ by (simp! add: vs_add_mult_distrib2);
qed;
qed;
@@ -141,14 +154,17 @@
qed;
qed;
-
-lemma lin_vs [intro!!]: "[| is_vectorspace V; x:V |] ==> is_vectorspace (lin x)";
+lemma lin_vs [intro!!]:
+ "[| is_vectorspace V; x:V |] ==> is_vectorspace (lin x)";
proof (rule subspace_vs);
assume "is_vectorspace V" "x:V";
show "is_subspace (lin x) V"; ..;
qed;
-section {* sum of two vectorspaces *};
+
+
+subsection {* Sum of two vectorspaces *};
+
constdefs
vectorspace_sum :: "['a set, 'a set] => 'a set"
@@ -159,11 +175,14 @@
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";
+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);
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 (vectorspace_sum U V)";
proof;
assume "is_vectorspace U" "is_vectorspace V";
show "<0> : U"; ..;
@@ -188,7 +207,6 @@
==> is_subspace (vectorspace_sum U V) E";
proof;
assume "is_subspace U E" "is_subspace V E" and e: "is_vectorspace E";
-
show "<0> : vectorspace_sum U V";
proof (intro vs_sumI);
show "<0> : U"; ..;
@@ -202,24 +220,28 @@
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:vectorspace_sum U V. ALL y:vectorspace_sum U V.
+ x [+] y : vectorspace_sum 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";
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";
+ assume "ux : U" "vx : V" "x = ux [+] vx" "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:vectorspace_sum U V. ALL a.
+ a [*] x : vectorspace_sum U V";
proof (intro ballI allI);
fix x a; assume "x:vectorspace_sum U V";
thus "a [*] x : vectorspace_sum 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)"; by (simp! add: vs_add_mult_distrib1);
+ show "a [*] x = (a [*] u) [+] (a [*] v)";
+ by (simp! add: vs_add_mult_distrib1);
qed (simp!)+;
qed;
qed;
@@ -233,17 +255,25 @@
qed;
-section {* special case: direct sum of a vectorspace and a linear closure of a vector *};
+
+subsection {* A special case *}
+
-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 |]
+text {* direct sum of a vectorspace and a linear closure of a vector
+*};
+
+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";
+ 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;
+ 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);
@@ -256,8 +286,8 @@
qed (rule);
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 |]
+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 |]
==> y1 = y2 & a1 = a2";
proof;
assume "is_vectorspace E" and h: "is_subspace H E"
@@ -281,7 +311,8 @@
assume "a = 0r"; show ?thesis; by (simp!);
next;
assume "a ~= 0r";
- from h; have "(rinv a) [*] a [*] x0 : H"; by (rule subspace_mult_closed) (simp!);
+ from h; have "(rinv a) [*] a [*] x0 : H";
+ by (rule subspace_mult_closed) (simp!);
also; have "(rinv a) [*] a [*] x0 = x0"; by (simp!);
finally; have "x0 : H"; .;
thus ?thesis; by contradiction;
@@ -306,10 +337,11 @@
qed;
lemma decomp1:
- "[| is_vectorspace E; is_subspace H E; t:H; x0~:H; x0:E; x0 ~= <0> |]
+ "[| 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)";
proof (rule, unfold split_paired_all);
- assume "is_vectorspace E" "is_subspace H E" "t:H" "x0~:H" "x0:E" "x0 ~= <0>";
+ 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";
have "y = t & a = 0r";
@@ -320,17 +352,17 @@
lemma decomp3:
"[| 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> |]
+ 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>";
-
+ "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+;
+ 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)";
@@ -343,15 +375,17 @@
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"; by (force!);
- 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!)+);
+ have x: "x = (fst xa) [+] (snd xa) [*] x0 & (fst xa) : H";
+ by (force!);
+ 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!)+);
qed;
qed;
- hence eq: "(@ (y, a). (x = y [+] a [*] x0 & y:H)) = (y, a)"; by (rule select1_equality) (force!);
+ hence eq: "(@ (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;
-end;
-
-
+end;
\ No newline at end of file
--- a/src/HOL/Real/HahnBanach/Zorn_Lemma.thy Fri Oct 08 16:18:51 1999 +0200
+++ b/src/HOL/Real/HahnBanach/Zorn_Lemma.thy Fri Oct 08 16:40:27 1999 +0200
@@ -3,10 +3,12 @@
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) ==>
+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";
@@ -33,6 +35,4 @@
qed;
qed;
-
-
-end;
+end;
\ No newline at end of file
--- a/src/HOL/Real/HahnBanach/document/notation.tex Fri Oct 08 16:18:51 1999 +0200
+++ b/src/HOL/Real/HahnBanach/document/notation.tex Fri Oct 08 16:40:27 1999 +0200
@@ -0,0 +1,22 @@
+
+\renewcommand{\isamarkupheader}[1]{\section{#1}}
+\parindent 0pt \parskip 0.5ex
+
+\newcommand{\name}[1]{\textsf{#1}}
+
+\newcommand{\idt}[1]{{\mathord{\mathit{#1}}}}
+\newcommand{\var}[1]{{?\!#1}}
+\DeclareMathSymbol{\dshsym}{\mathalpha}{letters}{"2D}
+\newcommand{\dsh}{\dshsym}
+
+\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\;}
+
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "root"
+%%% End:
--- a/src/HOL/Real/HahnBanach/document/root.tex Fri Oct 08 16:18:51 1999 +0200
+++ b/src/HOL/Real/HahnBanach/document/root.tex Fri Oct 08 16:40:27 1999 +0200
@@ -2,12 +2,20 @@
\documentclass[11pt,a4paper]{article}
\usepackage{isabelle,pdfsetup}
+\input{notation}
+
\begin{document}
-\title{The Hahn-Banach theorem for real vectorspaces}
+\title{The Hahn-Banach Theorem for Real Vectorspaces}
\author{Gertrud Bauer}
\maketitle
+\begin{abstract}
+ FIXME
+\end{abstract}
+
+\tableofcontents
+
\input{session}
\end{document}