--- a/src/HOL/Real/HahnBanach/Aux.thy Wed Sep 29 15:35:09 1999 +0200
+++ b/src/HOL/Real/HahnBanach/Aux.thy Wed Sep 29 16:41:52 1999 +0200
@@ -3,14 +3,12 @@
Author: Gertrud Bauer, TU Munich
*)
-theory Aux = Real:;
-
-theorems case = case_split_thm; (* FIXME tmp *);
+theory Aux = Real + Zorn:;
-lemmas CollectE = CollectD [elimify];
+lemmas [intro!!] = chainD;
+lemmas chainE2 = chainD2 [elimify];
+lemmas [intro!!] = isLub_isUb;
-theorem [trans]: "[| (x::'a::order) <= y; x ~= y |] ==> x < y"; (* <= ~= < *)
- by (simp! add: order_less_le);
lemma le_max1: "x <= max x (y::'a::linorder)";
by (simp add: le_max_iff_disj[of x x y]);
@@ -24,8 +22,6 @@
lemma Int_singletonD: "[| A Int B = {v}; x:A; x:B |] ==> x = v";
by (fast elim: equalityE);
-lemmas singletonE = singletonD[elimify];
-
lemma real_add_minus_eq: "x - y = 0r ==> x = y";
proof -;
assume "x - y = 0r";
@@ -33,7 +29,7 @@
also; have "... = 0r"; .;
finally; have "x + - y = 0r"; .;
hence "x = - (- y)"; by (rule real_add_minus_eq_minus);
- also; have "... = y"; by (simp!);
+ also; have "... = y"; by simp;
finally; show "x = y"; .;
qed;
@@ -44,31 +40,64 @@
show "-1r < 0r";
by (rule real_minus_zero_less_iff[RS iffD1], simp, rule real_zero_less_one);
qed;
- also; have "... = 1r"; by (simp!);
- finally; show ?thesis; by (simp!);
+ also; have "... = 1r"; by simp;
+ finally; show ?thesis; by simp;
+qed;
+
+lemma real_mult_le_le_mono2: "[| 0r <= z; x <= y |] ==> x * z <= y * z";
+proof -;
+ assume gz: "0r <= z" and ineq: "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;
+ qed;
qed;
-axioms real_mult_le_le_mono2: "[| 0r <= z; x <= y |] ==> x * z <= y * z";
+lemma real_mult_less_le_anti: "[| z < 0r; x <= y |] ==> z * y <= z * x";
+proof -;
+ assume lz: "z < 0r" and ineq: "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]);
+ thus ?thesis; by simp;
+qed;
-axioms real_mult_less_le_anti: "[| z < 0r; x <= y |] ==> z * y <= z * x";
-
-axioms 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);
+ thus ?thesis; by (rule real_mult_le_le_mono1);
+qed;
-axioms 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);
+ also; have "... = - a * x - a * y";
+ by (simp add: real_minus_mult_eq2 [RS sym] real_minus_mult_eq1 [RS sym]);
+ finally; show ?thesis; .;
+qed;
-axioms real_mult_diff_distrib2: "a * (x - (y::real)) = a * x - a * y";
-
-lemma less_imp_le: "(x::real) < y ==> x <= y";
- by (simp! only: real_less_imp_le);
+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);
+ also; have "... = a * x - a * y";
+ by (simp add: real_minus_mult_eq2 [RS sym] real_minus_mult_eq1 [RS sym]);
+ finally; show ?thesis; .;
+qed;
lemma le_noteq_imp_less: "[|x <= (r::'a::order); x ~= r |] ==> x < r";
proof -;
- assume "x <= (r::'a::order)";
- assume "x ~= r";
- then; have "x < r | x = r";
- by (simp! add: order_le_less);
- then; show ?thesis;
- by (simp!);
+ 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";
@@ -80,16 +109,16 @@
assume "- x < y"; show ?thesis;
proof -;
have "- y < - (- x)"; by (rule real_less_swap_iff [RS iffD1]);
- hence "- y < x"; by (simp!);
+ hence "- y < x"; by simp;
thus ?thesis; by (rule real_less_imp_le);
qed;
next;
- assume "- x = y"; show ?thesis; by (force!);
+ assume "- x = y"; thus ?thesis; by force;
qed;
qed;
lemma rabs_interval_iff_1: "(rabs (x::real) <= r) = (-r <= x & x <= r)";
-proof (rule case [of "rabs x = r"]);
+proof (rule case_split [of "rabs x = r"]);
assume a: "rabs x = r";
show ?thesis;
proof;
@@ -97,14 +126,14 @@
show "- r <= x & x <= r";
proof;
have "- x <= rabs x"; by (rule rabs_ge_minus_self);
- hence "- x <= r"; by (simp!);
- thus "- r <= x"; by (simp! add : minus_le [of "x" "r"]);
+ 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);
- thus "x <= r"; by (simp!);
+ with a; show "x <= r"; by simp;
qed;
next;
assume "- r <= x & x <= r";
- show "rabs x <= r"; by (fast!);
+ with a; show "rabs x <= r"; by fast;
qed;
next;
assume "rabs x ~= r";
@@ -124,26 +153,32 @@
assume "- r <= x & x <= r";
thus "rabs x <= r";
proof;
- assume "- r <= x" "x <= r";
+ assume a: "- r <= x" and "x <= r";
show ?thesis;
proof (rule rabs_disj [RS disjE, of x]);
- assume "rabs x = x";
- show ?thesis; by (simp!);
+ assume "rabs x = x";
+ thus ?thesis; by simp;
next;
assume "rabs x = - x";
- from minus_le [of r x]; show ?thesis; by (simp!);
+ with a minus_le [of r x]; show ?thesis; by simp;
qed;
qed;
qed;
qed;
-lemma set_less_imp_diff_not_empty: "H < E ==> EX x0:E. x0 ~: H";
-proof- ;
- assume "H < E ";
- have le: "H <= E"; by (rule conjunct1 [OF psubset_eq[RS iffD1]]);
- have ne: "H ~= E"; by (rule conjunct2 [OF psubset_eq[RS iffD1]]);
- with le; show ?thesis; by force;
+
+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;
-end;
\ No newline at end of file
+lemma set_less_imp_diff_not_empty: "H < E ==> EX x0:E. x0 ~: H";
+ by (force simp add: psubset_eq);
+
+
+end;
--- a/src/HOL/Real/HahnBanach/Bounds.thy Wed Sep 29 15:35:09 1999 +0200
+++ b/src/HOL/Real/HahnBanach/Bounds.thy Wed Sep 29 16:41:52 1999 +0200
@@ -86,7 +86,7 @@
"INF x. P" == "INF x:UNIV. P";
-lemma ub_ge_sup: "isUb A B y ==> is_Sup A B s ==> s <= y";
+lemma sup_le_ub: "isUb A B y ==> is_Sup A B s ==> s <= y";
by (unfold is_Sup_def, rule isLub_le_isUb);
lemma sup_ub: "y:B ==> is_Sup A B s ==> y <= s";
--- a/src/HOL/Real/HahnBanach/FunctionNorm.thy Wed Sep 29 15:35:09 1999 +0200
+++ b/src/HOL/Real/HahnBanach/FunctionNorm.thy Wed Sep 29 16:41:52 1999 +0200
@@ -71,13 +71,13 @@
also; from _ le; have "... <= c * norm x * rinv (norm x)";
proof (rule real_mult_le_le_mono2);
show "0r <= rinv (norm x)";
- proof (rule less_imp_le);
+ proof (rule real_less_imp_le);
show "0r < rinv (norm x)";
proof (rule real_rinv_gt_zero);
show "0r < norm x"; ..;
qed;
qed;
- (*** or: by (rule less_imp_le, rule real_rinv_gt_zero, rule normed_vs_norm_gt_zero); ***)
+ (*** 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 "(norm x * rinv (norm x)) = 1r";
@@ -118,7 +118,7 @@
proof (simp!, rule real_le_mult_order);
show "0r <= rabs (f x)"; by (simp! only: rabs_ge_zero);
show "0r <= rinv (norm x)";
- proof (rule less_imp_le);
+ proof (rule real_less_imp_le);
show "0r < rinv (norm x)";
proof (rule real_rinv_gt_zero);
show "0r < norm x"; ..;
@@ -141,7 +141,7 @@
have v: "is_vectorspace V"; ..;
assume "x:V";
show "?thesis";
- proof (rule case [of "x = <0>"]);
+ proof (rule case_split [of "x = <0>"]);
assume "x ~= <0>";
show "?thesis";
proof -;
@@ -197,7 +197,7 @@
assume fb: "ALL x:V. rabs (f x) <= c * norm x"
and "0r <= c";
show "Sup UNIV (B V norm f) <= c";
- proof (rule ub_ge_sup);
+ proof (rule sup_le_ub);
from ex_fnorm [OF _ c]; show "is_Sup UNIV (B V norm f) (Sup UNIV (B V norm f))";
by (simp! add: is_function_norm_def function_norm_def);
show "isUb UNIV (B V norm f) c";
@@ -217,7 +217,7 @@
from lt; have "0r < rinv (norm x)";
by (simp! add: real_rinv_gt_zero);
- then; have inv_leq: "0r <= rinv (norm x)"; by (rule 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)";
--- a/src/HOL/Real/HahnBanach/FunctionOrder.thy Wed Sep 29 15:35:09 1999 +0200
+++ b/src/HOL/Real/HahnBanach/FunctionOrder.thy Wed Sep 29 16:41:52 1999 +0200
@@ -57,42 +57,42 @@
qed;
constdefs
- norm_prev_extensions ::
+ norm_pres_extensions ::
"['a set, 'a => real, 'a set, 'a => real] => 'a graph set"
- "norm_prev_extensions E p F f == {g. EX H h. graph H h = g
+ "norm_pres_extensions E p F f == {g. EX H h. graph H h = g
& is_linearform H h
& is_subspace H E
& is_subspace F H
& (graph F f <= graph H h)
& (ALL x:H. h x <= p x)}";
-lemma norm_prev_extension_D:
- "(g: norm_prev_extensions E p F f) ==> (EX H h. graph H h = g
+lemma norm_pres_extension_D:
+ "(g: norm_pres_extensions E p F f) ==> (EX H h. graph H h = g
& is_linearform H h
& is_subspace H E
& is_subspace F H
& (graph F f <= graph H h)
& (ALL x:H. h x <= p x))";
- by (unfold norm_prev_extensions_def) force;
+ by (unfold norm_pres_extensions_def) force;
-lemma norm_prev_extensionI2 [intro]:
+lemma norm_pres_extensionI2 [intro]:
"[| is_linearform H h;
is_subspace H E;
is_subspace F H;
(graph F f <= graph H h);
(ALL x:H. h x <= p x) |]
- ==> (graph H h : norm_prev_extensions E p F f)";
- by (unfold norm_prev_extensions_def) force;
+ ==> (graph H h : norm_pres_extensions E p F f)";
+ by (unfold norm_pres_extensions_def) force;
-lemma norm_prev_extensionI [intro]:
+lemma norm_pres_extensionI [intro]:
"(EX H h. graph H h = g
& is_linearform H h
& is_subspace H E
& is_subspace F H
& (graph F f <= graph H h)
& (ALL x:H. h x <= p x))
- ==> (g: norm_prev_extensions E p F f) ";
- by (unfold norm_prev_extensions_def) force;
+ ==> (g: norm_pres_extensions E p F f) ";
+ by (unfold norm_pres_extensions_def) force;
end;
--- a/src/HOL/Real/HahnBanach/HahnBanach.thy Wed Sep 29 15:35:09 1999 +0200
+++ b/src/HOL/Real/HahnBanach/HahnBanach.thy Wed Sep 29 16:41:52 1999 +0200
@@ -3,10 +3,18 @@
Author: Gertrud Bauer, TU Munich
*)
+(* The proof of two different versions of the Hahn-Banach theorem,
+ following H. Heuser, Funktionalanalysis, p. 228 - 232.
+*)
+
theory HahnBanach = HahnBanach_lemmas + HahnBanach_h0_lemmas:;
-theorems [elim!!] = psubsetI;
+section {* The Hahn-Banach theorem for general linear spaces,
+ H. Heuser, Funktionalanalysis, p.231 *};
+
+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;
@@ -16,11 +24,12 @@
& (ALL x:E. h x <= p x)";
proof -;
assume "is_vectorspace E" "is_subspace F E" "is_quasinorm E p" "is_linearform F f"
- and "ALL x:F. f x <= p x";
- def M == "norm_prev_extensions E p F f";
+ "ALL x:F. f x <= p x";
+
+ def M == "norm_pres_extensions E p F f";
- have aM: "graph F f : norm_prev_extensions E p F f";
- proof (rule norm_prev_extensionI2);
+ have aM: "graph F f : norm_pres_extensions E p F f";
+ proof (rule norm_pres_extensionI2);
show "is_subspace F F";
proof;
show "is_vectorspace F"; ..;
@@ -28,58 +37,56 @@
qed (blast!)+;
- sect {* Part I a of the proof of the Hahn-Banach Theorem,
+ 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";
proof -;
fix c; assume "c:chain M"; assume "EX x. x:c";
show "(Union c) : M";
- proof (unfold M_def, rule norm_prev_extensionI);
+ proof (unfold M_def, rule norm_pres_extensionI);
show "EX (H::'a set) h::'a => real. graph H h = Union c
& is_linearform H h
& is_subspace H E
& is_subspace F H
& (graph F f <= graph H h)
& (ALL x::'a:H. h x <= p x)" (is "EX (H::'a set) h::'a => real. ?Q H h");
- proof;
+ proof (intro exI conjI);
let ?H = "domain (Union c)";
- show "EX h. ?Q ?H h";
- proof;
- let ?h = "funct (Union c)";
- show "?Q ?H ?h";
- proof (intro conjI);
- show a: "graph ?H ?h = Union c";
- proof (rule graph_domain_funct);
- fix x y z; assume "(x, y) : Union c" "(x, z) : Union c";
- show "z = y"; by (rule sup_uniq);
- qed;
+ let ?h = "funct (Union c)";
+
+ show a: "graph ?H ?h = Union c";
+ proof (rule graph_domain_funct);
+ fix x y z; assume "(x, y) : Union c" "(x, z) : Union c";
+ show "z = y"; by (rule sup_uniq);
+ qed;
- show "is_linearform ?H ?h";
- by (simp! add: sup_lf a);
-
- show "is_subspace ?H E";
- by (rule sup_subE, rule a) (simp!)+;
+ show "is_linearform ?H ?h";
+ by (simp! add: sup_lf a);
- show "is_subspace F ?H";
- by (rule sup_supF, rule a) (simp!)+;
+ show "is_subspace ?H E";
+ by (rule sup_subE, rule a) (simp!)+;
+
+ show "is_subspace F ?H";
+ by (rule sup_supF, rule a) (simp!)+;
- show "graph F f <= graph ?H ?h";
- by (rule sup_ext, rule a) (simp!)+;
+ show "graph F f <= graph ?H ?h";
+ by (rule sup_ext, rule a) (simp!)+;
- show "ALL x::'a:?H. ?h x <= p x";
- by (rule sup_norm_prev, rule a) (simp!)+;
- qed;
- qed;
+ show "ALL x::'a:?H. ?h x <= p x";
+ by (rule sup_norm_pres, rule a) (simp!)+;
qed;
qed;
qed;
-
+
+ txt {* there exists a maximal norm-preserving function g. *};
with aM; have bex_g: "EX g:M. ALL x:M. g <= x --> g = x";
by (simp! add: Zorn's_Lemma);
+
thus ?thesis;
proof;
fix g; assume g: "g:M" "ALL x:M. g <= x --> g = x";
@@ -90,28 +97,38 @@
& is_subspace F H
& (graph F f <= graph H h)
& (ALL x:H. h x <= p x) ";
- by (simp! add: norm_prev_extension_D);
+ by (simp! add: norm_pres_extension_D);
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"
- "(graph F f <= graph H h)"; assume h_bound: "ALL x:H. h x <= p x";
+ fix H h;
+ assume "graph H h = g" "is_linearform (H::'a set) h" "is_subspace H E" "is_subspace F H"
+ and h_ext: "(graph F f <= graph H h)"
+ and h_bound: "ALL x:H. h x <= p x";
+
show ?thesis;
proof;
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 *};
+
have eq: "H = E";
proof (rule classical);
+
+ txt {* assume h is not defined on whole E *};
+
assume "H ~= E";
show ?thesis;
proof -;
+
have "EX x:M. g <= x & g ~= x";
proof -;
+
+ txt {* h can be extended norm-preserving to H0 *};
+
have "EX H0 h0. g <= graph H0 h0 & g ~= graph H0 h0 & graph H0 h0 : M";
proof-;
have "H <= E"; ..;
@@ -120,11 +137,11 @@
thus ?thesis;
proof;
fix x0; assume "x0:E" "x0~:H";
+
have x0: "x0 ~= <0>";
proof (rule classical);
- presume "x0 = <0>";
- also; have "<0> : H"; ..;
- finally; have "x0 : H"; .;
+ presume "x0 = <0>";
+ with h; have "x0:H"; by simp;
thus ?thesis; by contradiction;
qed force;
@@ -136,29 +153,16 @@
proof (rule ex_xi);
fix u v; assume "u:H" "v:H";
show "- p (u [+] x0) - h u <= p (v [+] x0) - h v";
- proof -;
- show "!! a b c d::real. d - b <= c + a ==> - a - b <= c - d";
- proof -; (* arith *)
- fix a b c d; 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;
+ proof (rule real_diff_ineq_swap);
+
show "h v - h u <= p (v [+] x0) + p (u [+] x0)";
proof -;
from h; have "h v - h u = h (v [-] u)";
- by (rule linearform_diff_linear [RS sym]);
- also; have "... <= p (v [-] u)";
- proof -;
- from h; have "v [-] u : H"; by (simp!);
- with h_bound; show ?thesis; ..;
- qed;
- also; have "v [-] u = x0 [+] [-] x0 [+] 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!);
also; have "... = (v [+] x0) [-] (u [+] x0)";
by (simp! only: vs_add_minus_eq_diff);
also; have "p ... <= p (v [+] x0) + p (u [+] x0)";
@@ -198,79 +202,59 @@
have "graph H h ~= graph H0 h0";
proof;
- assume "graph H h = graph H0 h0";
- have x1: "(x0, h0 x0) : graph H0 h0";
- proof (rule graphI);
- show "x0:H0";
- proof (unfold H0_def, rule vs_sumI);
- from h; show "<0> : H"; ..;
- show "x0 : lin x0"; by (rule x_lin_x);
- show "x0 = <0> [+] x0"; by (simp!);
- qed;
+ 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;
- have "(x0, h0 x0) ~: graph H h";
- proof;
- assume "(x0, h0 x0) : graph H h";
- have "x0:H"; ..;
- thus "False"; by contradiction;
- qed;
- hence "(x0, h0 x0) ~: graph H0 h0"; by (simp!);
- with x1; show "False"; by contradiction;
+ 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_prev_extensions E p F f";
- proof (rule norm_prev_extensionI2);
+ 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";
- proof -;
- have "is_subspace (vectorspace_sum H (lin x0)) E";
- by (rule vs_sum_subspace, rule lin_subspace);
- thus ?thesis; by (simp!);
- qed;
+ 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))";
- by (rule subspace_vs_sum1);
- thus "is_subspace H H0"; by (simp!);
+ 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);
+ proof (rule graph_extI);
fix x; assume "x:F";
show "f x = h0 x";
proof -;
- have "x:H";
- proof (rule subsetD);
- show "F <= H"; ..;
- qed;
have eq: "(@ (y, a). x = y [+] a [*] x0 & y : H) = (x, 0r)";
by (rule decomp1, rule x0) (simp!)+;
-
- have "h0 x = (let (y,a) = @ (y,a). x = y [+] a [*] x0 & y : H
- in h y + a * xi)";
- by (simp!);
- also; from eq; have "... = (let (y,a) = (x, 0r) in h y + a * xi)";
- by simp;
- also; have " ... = h x + 0r * xi";
- by (simp! add: Let_def);
- also; have "... = h x"; by (simp!);
- also; have "... = f x";
- proof (rule sym);
- show "f x = h x"; ..;
- qed;
- finally; show ?thesis; by (rule sym);
+
+ 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_prev, rule x0) (assumption | (simp!))+;
+ by (rule h0_norm_pres, rule x0) (assumption | (simp!))+;
qed;
thus "graph H0 h0 : M"; by (simp!);
qed;
@@ -302,6 +286,11 @@
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 *};
+
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 |]
@@ -310,11 +299,8 @@
& (ALL x:E. rabs (g x) <= p x)";
proof -;
- sect {* Part I (for real linear spaces) of the proof of the Hahn-banach Theorem,
- H. Heuser, Funktionalanalysis, p.229 *};
-
- assume e: "is_vectorspace E";
- assume "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" and "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)";
by (simp! only: hahnbanach);
@@ -330,6 +316,12 @@
qed;
+section {* The Hahn-Banach theorem for normd spaces,
+ H. Heuser, Funktionalanalysis, p.232 *};
+
+text {* Every continous linear function f on a subspace of E,
+ can be extended to a continous function on E with the same norm *};
+
theorem norm_hahnbanach:
"[| is_normed_vectorspace E norm; is_subspace F E; is_linearform F f;
is_continous F norm f |]
@@ -340,15 +332,13 @@
(concl is "EX g::'a=>real. ?P g");
proof -;
-sect {* Proof of the Hahn-Banach Theorem for normed spaces,
- H. Heuser, Funktionalanalysis, p.232 *};
assume a: "is_normed_vectorspace E norm";
assume b: "is_subspace F E" "is_linearform F f";
assume c: "is_continous F norm f";
have e: "is_vectorspace E"; ..;
- from _ e;
- have f: "is_normed_vectorspace F norm"; ..;
+ from _ e; have f: "is_normed_vectorspace F norm"; ..;
+
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)";
--- a/src/HOL/Real/HahnBanach/HahnBanach_h0_lemmas.thy Wed Sep 29 15:35:09 1999 +0200
+++ b/src/HOL/Real/HahnBanach/HahnBanach_h0_lemmas.thy Wed Sep 29 16:41:52 1999 +0200
@@ -6,26 +6,24 @@
theory HahnBanach_h0_lemmas = FunctionNorm:;
-theorems [intro!!] = isLub_isUb;
-
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 "is_vectorspace F";
+ assume vs: "is_vectorspace F";
assume r: "(!! u v. [| u:F; v:F |] ==> a u <= (b v::real))";
have "EX t. isLub UNIV {s::real . EX u:F. s = a u} t";
proof (rule reals_complete);
- have "a <0> : {s. EX u:F. s = a u}"; by (force!);
+ from vs; have "a <0> : {s. EX u:F. s = a u}"; by (force);
thus "EX X. X : {s. EX u:F. s = a u}"; ..;
show "EX Y. isUb UNIV {s. EX u:F. s = a u} Y";
proof;
show "isUb UNIV {s. EX u:F. s = a u} (b <0>)";
proof (intro isUbI setleI ballI, fast);
- fix y; assume "y : {s. EX u:F. s = a u}";
+ fix y; assume y: "y : {s. EX u:F. s = a u}";
show "y <= b <0>";
proof -;
- have "EX u:F. y = a u"; by (fast!);
+ from y; have "EX u:F. y = a u"; by (fast);
thus ?thesis;
proof;
fix u; assume "u:F";
@@ -45,11 +43,11 @@
fix t; assume "isLub UNIV {s::real . EX u:F. s = a u} t";
show ?thesis;
proof (intro exI conjI ballI);
- fix y; assume "y:F";
+ fix y; assume y: "y:F";
show "a y <= t";
proof (rule isUbD);
show"isUb UNIV {s. EX u:F. s = a u} t"; ..;
- qed (fast!);
+ qed (force simp add: y);
next;
fix y; assume "y:F";
show "t <= b y";
@@ -57,10 +55,10 @@
show "ALL ya : {s. EX u:F. s = a u}. ya <= b y";
proof (intro ballI);
fix au;
- assume "au : {s. EX u:F. s = a u} ";
+ assume au: "au : {s. EX u:F. s = a u} ";
show "au <= b y";
proof -;
- have "EX u:F. au = a u"; by (fast!);
+ from au; have "EX u:F. au = a u"; by (fast);
thus "au <= b y";
proof;
fix u; assume "u:F";
@@ -85,44 +83,43 @@
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 [simp]: "is_subspace H E" "is_linearform H h" "x0 ~: H" "x0 ~= <0>"
- and [simp]: "x0 : E" "is_vectorspace E";
+ 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!), rule vs_sum_vs);
+ proof (simp only: H0_def, rule vs_sum_vs);
show "is_subspace (lin x0) E"; by (rule lin_subspace);
- qed simp+;
+ qed;
show ?thesis;
proof;
- fix x1 x2; assume "x1 : H0" "x2 : H0";
+ fix x1 x2; assume x1: "x1 : H0" and x2: "x2 : H0";
have x1x2: "x1 [+] x2 : H0";
by (rule vs_add_closed, rule h0);
- have ex_x1: "? y1 a1. (x1 = y1 [+] a1 [*] x0 & y1 : H)";
- by (simp! add: vectorspace_sum_def lin_def) blast;
- have ex_x2: "? y2 a2. (x2 = y2 [+] a2 [*] x0 & y2 : H)";
- by (simp! add: vectorspace_sum_def lin_def) blast;
+ from x1; have ex_x1: "? y1 a1. (x1 = y1 [+] a1 [*] x0 & y1 : H)";
+ by (simp add: H0_def vectorspace_sum_def lin_def) blast;
+ from x2; have ex_x2: "? y2 a2. (x2 = y2 [+] a2 [*] x0 & y2 : H)";
+ by (simp add: H0_def vectorspace_sum_def lin_def) blast;
from x1x2; have ex_x1x2: "? y a. (x1 [+] x2 = y [+] a [*] x0 & y : H)";
- by (simp! add: vectorspace_sum_def lin_def) force;
+ by (simp add: H0_def vectorspace_sum_def lin_def) force;
from ex_x1 ex_x2 ex_x1x2;
show "h0 (x1 [+] x2) = h0 x1 + h0 x2";
proof (elim exE conjE);
fix y1 y2 y a1 a2 a;
- assume "x1 = y1 [+] a1 [*] x0" "y1 : H"
- "x2 = y2 [+] a2 [*] x0" "y2 : H"
- "x1 [+] x2 = y [+] a [*] x0" "y : H";
+ assume y1: "x1 = y1 [+] a1 [*] x0" and y1': "y1 : H"
+ and y2: "x2 = y2 [+] a2 [*] x0" and y2': "y2 : H"
+ and y: "x1 [+] x2 = y [+] a [*] x0" and y': "y : H";
have ya: "y1 [+] y2 = y & a1 + a2 = a";
proof (rule decomp4);
show "y1 [+] y2 [+] (a1 + a2) [*] x0 = y [+] a [*] x0";
proof -;
- have "y [+] a [*] x0 = x1 [+] x2"; by (simp!);
- also; have "... = y1 [+] a1 [*] x0 [+] (y2 [+] a2 [*] x0)"; by (simp!);
- also; from prems; have "... = y1 [+] y2 [+] (a1 [*] x0 [+] a2 [*] x0)";
- by asm_simp_tac; (* FIXME !?? *)
- also; have "... = y1 [+] y2 [+] (a1 + a2) [*] x0";
- by (simp! add: vs_add_mult_distrib2[of E]);
+ have "y [+] a [*] x0 = x1 [+] x2"; by (rule sym);
+ also; from y1 y2; have "... = y1 [+] a1 [*] x0 [+] (y2 [+] a2 [*] x0)"; by simp;
+ also; from vs y1' y2'; have "... = y1 [+] y2 [+] (a1 [*] x0 [+] a2 [*] x0)"; by simp;
+ also; from vs y1' y2'; have "... = y1 [+] y2 [+] (a1 + a2) [*] x0";
+ by (simp add: vs_add_mult_distrib2[of E]);
finally; show ?thesis; by (rule sym);
qed;
show "y1 [+] y2 : H"; ..;
@@ -132,45 +129,40 @@
have "h0 (x1 [+] x2) = h y + a * xi";
by (rule decomp3);
- also; have "... = h (y1 [+] y2) + (a1 + a2) * xi"; by (simp! add: y a);
- also; have "... = h y1 + h y2 + a1 * xi + a2 * xi";
- by (simp! add: linearform_add_linear [of H] real_add_mult_distrib);
- also; have "... = (h y1 + a1 * xi) + (h y2 + a2 * xi)"; by (simp!);
- also; have "... = h0 x1 + h0 x2";
- proof -;
- have x1: "h0 x1 = h y1 + a1 * xi"; by (rule decomp3);
- have x2: "h0 x2 = h y2 + a2 * xi"; by (rule decomp3);
- from x1 x2; show ?thesis; by (simp!);
- qed;
+ also; have "... = h (y1 [+] y2) + (a1 + a2) * xi"; by (simp add: y a);
+ also; from vs y1' y2'; have "... = h y1 + h y2 + a1 * xi + a2 * xi";
+ by (simp add: linearform_add_linear [of H] real_add_mult_distrib);
+ also; have "... = (h y1 + a1 * xi) + (h y2 + a2 * xi)"; by (simp);
+ also; have "h y1 + a1 * xi = h0 x1"; by (rule decomp3 [RS sym]);
+ also; have "h y2 + a2 * xi = h0 x2"; by (rule decomp3 [RS sym]);
finally; show ?thesis; .;
qed;
next;
- fix c x1; assume "x1 : H0";
+ fix c x1; assume x1: "x1 : H0";
have ax1: "c [*] x1 : H0";
by (rule vs_mult_closed, rule h0);
- have ex_x1: "? y1 a1. (x1 = y1 [+] a1 [*] x0 & y1 : H)";
- by (simp! add: vectorspace_sum_def lin_def, fast);
- have ex_x: "!! x. x: H0 ==> ? y a. (x = y [+] a [*] x0 & y : H)";
- by (simp! add: vectorspace_sum_def lin_def, fast);
+ from x1; have ex_x1: "? y1 a1. (x1 = y1 [+] a1 [*] x0 & y1 : H)";
+ by (simp add: H0_def vectorspace_sum_def lin_def, fast);
+ from x1; have ex_x: "!! x. x: H0 ==> ? y a. (x = y [+] a [*] x0 & y : H)";
+ by (simp add: H0_def vectorspace_sum_def lin_def, fast);
note ex_ax1 = ex_x [of "c [*] x1", OF ax1];
from ex_x1 ex_ax1; show "h0 (c [*] x1) = c * (h0 x1)";
proof (elim exE conjE);
fix y1 y a1 a;
- assume "x1 = y1 [+] a1 [*] x0" "y1 : H"
- "c [*] x1 = y [+] a [*] x0" "y : H";
+ assume y1: "x1 = y1 [+] a1 [*] x0" and y1': "y1 : H"
+ and y: "c [*] x1 = y [+] a [*] x0" and y': "y : H";
have ya: "c [*] y1 = y & c * a1 = a";
proof (rule decomp4);
show "c [*] y1 [+] (c * a1) [*] x0 = y [+] a [*] x0";
proof -;
- have "y [+] a [*] x0 = c [*] x1"; by (simp!);
- also; have "... = c [*] (y1 [+] a1 [*] x0)"; by (simp!);
- also; from prems; have "... = c [*] y1 [+] c [*] (a1 [*] x0)";
- by (asm_simp_tac add: vs_add_mult_distrib1); (* FIXME *)
- also; from prems; have "... = c [*] y1 [+] (c * a1) [*] x0";
- by asm_simp_tac;
+ have "y [+] a [*] x0 = c [*] x1"; by (rule sym);
+ also; from y1; have "... = c [*] (y1 [+] a1 [*] x0)"; by simp;
+ also; from vs y1'; have "... = c [*] y1 [+] c [*] (a1 [*] x0)";
+ by (simp add: vs_add_mult_distrib1);
+ also; from vs y1'; have "... = c [*] y1 [+] (c * a1) [*] x0"; by simp;
finally; show ?thesis; by (rule sym);
qed;
show "c [*] y1: H"; ..;
@@ -181,169 +173,114 @@
have "h0 (c [*] x1) = h y + a * xi";
by (rule decomp3);
also; have "... = h (c [*] y1) + (c * a1) * xi";
- by (simp! add: y a);
- also; have "... = c * h y1 + c * a1 * xi";
- by (simp! add: linearform_mult_linear [of H] real_add_mult_distrib);
- also; have "... = c * (h y1 + a1 * xi)";
- by (simp! add: real_add_mult_distrib2 real_mult_assoc);
- also; have "... = c * (h0 x1)";
- proof -;
- have "h0 x1 = h y1 + a1 * xi"; by (rule decomp3);
- thus ?thesis; by (simp!);
- qed;
+ by (simp add: y a);
+ also; from vs y1'; have "... = c * h y1 + c * a1 * xi";
+ by (simp add: linearform_mult_linear [of H] real_add_mult_distrib);
+ also; from vs y1'; have "... = c * (h y1 + a1 * xi)";
+ by (simp add: real_add_mult_distrib2 real_mult_assoc);
+ also; have "h y1 + a1 * xi = h0 x1"; by (rule decomp3 [RS sym]);
finally; show ?thesis; .;
qed;
qed;
qed;
-lemma h0_norm_prev:
+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)|]
==> ALL x:H0. h0 x <= p x";
proof;
- assume "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" 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";
show "h0 x <= p x";
proof -;
have ex_x: "!! x. x : H0 ==> ? y a. (x = y [+] a [*] x0 & y : H)";
- by (simp! add: vectorspace_sum_def lin_def, fast);
+ by (simp add: H0_def vectorspace_sum_def lin_def, fast);
have "? y a. (x = y [+] a [*] x0 & y : H)";
by (rule ex_x);
thus ?thesis;
proof (elim exE conjE);
- fix y a; assume "x = y [+] a [*] x0" "y : H";
+ fix y a; assume x: "x = y [+] a [*] x0" and y: "y : H";
show ?thesis;
proof -;
have "h0 x = h y + a * xi";
by (rule decomp3);
also; have "... <= p (y [+] a [*] x0)";
- proof (rule real_linear [of a "0r", elimify], elim disjE); (*** case distinction ***)
- assume lz: "a < 0r";
- hence nz: "a ~= 0r"; by force;
+ proof (rule real_linear_split [of a "0r"]); (*** case analysis ***)
+ assume lz: "a < 0r"; hence nz: "a ~= 0r"; by force;
show ?thesis;
proof -;
from a1; have "- p (rinv a [*] y [+] x0) - h (rinv a [*] y) <= xi";
- proof (rule bspec);
- show "(rinv a) [*] y : H"; ..;
- qed;
+ by (rule bspec, simp!);
+
with lz; have "a * xi <= a * (- p (rinv a [*] y [+] x0) - h (rinv a [*] y))";
by (rule real_mult_less_le_anti);
also; have "... = - a * (p (rinv a [*] y [+] x0)) - a * (h (rinv a [*] y))";
by (rule real_mult_diff_distrib);
- also; have "... = (rabs a) * (p (rinv a [*] y [+] x0)) - a * (h (rinv a [*] y))";
- proof -;
- from lz; have "rabs a = - a";
- by (rule rabs_minus_eqI2);
- thus ?thesis; by simp;
- qed;
- also; from prems; have "... = p (a [*] (rinv a [*] y [+] x0)) - a * (h (rinv a [*] y))";
- by (simp!, asm_simp_tac add: quasinorm_mult_distrib);
- also; have "... = p ((a * rinv a) [*] y [+] a [*] x0) - a * (h (rinv a [*] y))";
- proof simp;
- have "a [*] (rinv a [*] y [+] x0) = a [*] rinv a [*] y [+] a [*] x0";
- by (rule vs_add_mult_distrib1) (simp!)+;
- also; have "... = (a * rinv a) [*] y [+] a [*] x0";
- by (simp!);
- finally; have "a [*] (rinv a [*] y [+] x0) = (a * rinv a) [*] y [+] a [*] x0";.;
- thus "p (a [*] (rinv a [*] y [+] x0)) = p ((a * rinv a) [*] y [+] a [*] x0)";
- by simp;
- qed;
- also; from nz; have "... = p (y [+] a [*] x0) - (a * (h (rinv a [*] y)))";
- by (simp!);
- also; have "a * (h (rinv a [*] y)) = h y";
- proof -;
- from prems; have "a * (h (rinv a [*] y)) = h (a [*] (rinv a [*] y))";
- by (asm_simp_tac add: linearform_mult_linear [RS sym]);
- also; from nz; have "a [*] (rinv a [*] y) = y"; by (simp!);
- finally; show ?thesis; .;
- qed;
- finally; have "a * xi <= p (y [+] a [*] x0) - ..."; .;
+ also; from lz vs y;
+ have "- a * (p (rinv a [*] y [+] x0)) = p (a [*] (rinv a [*] y [+] x0))";
+ by (simp add: quasinorm_mult_distrib rabs_minus_eqI2 [RS sym]);
+ also; from nz vs y; have "... = p (y [+] a [*] x0)";
+ by (simp add: vs_add_mult_distrib1);
+ also; from nz vs y; have "a * (h (rinv a [*] y)) = h y";
+ by (simp add: linearform_mult_linear [RS sym]);
+ finally; have "a * xi <= p (y [+] a [*] x0) - h y"; .;
+
hence "h y + a * xi <= h y + (p (y [+] a [*] x0) - h y)";
- by (rule real_add_left_cancel_le [RS iffD2]); (* arith *)
+ by (rule real_add_left_cancel_le [RS iffD2]);
thus ?thesis;
- by force;
+ by simp;
qed;
+
next;
- assume "a = 0r"; show ?thesis;
- proof -;
- have "h y + a * xi = h y"; by (simp!);
- also; from a; have "... <= p y"; ..;
- also; have "... = p (y [+] a [*] x0)";
- proof -;
- have "y = y [+] <0>"; by (simp!);
- also; have "... = y [+] a [*] x0";
- proof -;
- have "<0> = 0r [*] x0";
- by (simp!);
- also; have "... = a [*] x0"; by (simp!);
- finally; have "<0> = a [*] x0";.;
- thus ?thesis; by simp;
- qed;
- finally; have "y = y [+] a [*] x0"; by simp;
- thus ?thesis; by simp;
- qed;
- finally; show ?thesis; .;
- qed;
+ assume z: "a = 0r";
+ with vs y a; show ?thesis; by simp;
next;
assume gz: "0r < a"; hence nz: "a ~= 0r"; by force;
show ?thesis;
proof -;
from a2; have "xi <= p (rinv a [*] y [+] x0) - h (rinv a [*] y)";
- proof (rule bspec);
- show "rinv a [*] y : H"; ..;
- qed;
+ by (rule bspec, simp!);
+
with gz; have "a * xi <= a * (p (rinv a [*] y [+] x0) - h (rinv a [*] y))";
by (rule real_mult_less_le_mono);
also; have "... = a * (p (rinv a [*] y [+] x0)) - a * (h (rinv a [*] y))";
by (rule real_mult_diff_distrib2);
- also; have "... = (rabs a) * (p (rinv a [*] y [+] x0)) - a * (h (rinv a [*] y))";
- proof -;
- from gz; have "rabs a = a";
- by (rule rabs_eqI2);
- thus ?thesis; by simp;
- qed;
- also; from prems; have "... = p (a [*] (rinv a [*] y [+] x0)) - a * (h (rinv a [*] y))";
- by (simp, asm_simp_tac add: quasinorm_mult_distrib);
- also; have "... = p ((a * rinv a) [*] y [+] a [*] x0) - a * (h (rinv a [*] y))";
- proof simp;
- have "a [*] (rinv a [*] y [+] x0) = a [*] rinv a [*] y [+] a [*] x0";
- by (rule vs_add_mult_distrib1) (simp!)+;
- also; have "... = (a * rinv a) [*] y [+] a [*] x0";
- by (simp!);
- finally; have "a [*] (rinv a [*] y [+] x0) = (a * rinv a) [*] y [+] a [*] x0";.;
- thus "p (a [*] (rinv a [*] y [+] x0)) = p ((a * rinv a) [*] y [+] a [*] x0)";
- by simp;
- qed;
- also; from nz; have "... = p (y [+] a [*] x0) - (a * (h (rinv a [*] y)))";
- by (simp!);
- also; from nz; have "... = p (y [+] a [*] x0) - (h y)";
- proof (simp!);
- have "a * (h (rinv a [*] y)) = h (a [*] (rinv a [*] y))";
- by (rule linearform_mult_linear [RS sym]) (simp!)+;
- also; have "... = h y";
- proof -;
- from nz; have "a [*] (rinv a [*] y) = y"; by (simp!);
- thus ?thesis; by simp;
- qed;
- finally; have "a * (h (rinv a [*] y)) = h y"; .;
- thus "- (a * (h (rinv a [*] y))) = - (h y)"; by simp;
- qed;
+ also; from gz vs y;
+ have "a * (p (rinv a [*] y [+] x0)) = p (a [*] (rinv a [*] y [+] x0))";
+ by (simp add: quasinorm_mult_distrib rabs_eqI2);
+ also; from nz vs y;
+ have "... = p (y [+] a [*] x0)";
+ by (simp add: vs_add_mult_distrib1);
+ also; from nz vs y; have "a * (h (rinv a [*] y)) = h y";
+ by (simp add: linearform_mult_linear [RS sym]);
finally; have "a * xi <= p (y [+] a [*] x0) - h y"; .;
+
hence "h y + a * xi <= h y + (p (y [+] a [*] x0) - h y)";
- by (rule real_add_left_cancel_le [RS iffD2]); (* arith *)
+ by (rule real_add_left_cancel_le [RS iffD2]);
thus ?thesis;
- by force;
+ by simp;
qed;
qed;
- also; have "... = p x"; by (simp!);
+ also; from x; have "... = p x"; by (simp);
finally; show ?thesis; .;
qed;
qed;
--- a/src/HOL/Real/HahnBanach/HahnBanach_lemmas.thy Wed Sep 29 15:35:09 1999 +0200
+++ b/src/HOL/Real/HahnBanach/HahnBanach_lemmas.thy Wed Sep 29 16:41:52 1999 +0200
@@ -10,15 +10,15 @@
\ ==> (ALL x:H. rabs (h x) <= p x) = ( ALL x:H. h x <= p x)" (concl is "?L = ?R");
proof -;
assume "is_subspace H E" "is_vectorspace E" "is_quasinorm E p" "is_linearform H h";
- have H: "is_vectorspace H"; by (rule subspace_vs);
+ have h: "is_vectorspace H"; ..;
show ?thesis;
proof;
assume l: ?L;
then; show ?R;
proof (intro ballI);
- fix x; assume "x:H";
+ fix x; assume x: "x:H";
have "h x <= rabs (h x)"; by (rule rabs_ge_self);
- also; have "rabs (h x) <= p x"; by (fast!);
+ also; from l; have "... <= p x"; ..;
finally; show "h x <= p x"; .;
qed;
next;
@@ -26,22 +26,16 @@
then; show ?L;
proof (intro ballI);
fix x; assume "x:H";
- have lem: "!! r x. [| - r <= x; x <= r |] ==> rabs x <= r";
- by (rule conjI [RS rabs_interval_iff_1 [RS iffD2]]); (* arith *)
+
show "rabs (h x) <= p x";
- proof (rule lem);
- show "- p x <= h 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]);
- also; from r; have "... <= p ([-] x)";
- proof -;
- from H; have "[-] x : H"; by (simp!);
- with r; show ?thesis; ..;
- qed;
- also; have "... = p x";
- proof (rule quasinorm_minus);
- show "x:E"; ..;
- qed;
+ from h; have "- h x = h ([-] x)"; by (rule linearform_neg_linear [RS sym]);
+ also; from r; have "... <= p ([-] x)"; by (simp!);
+ also; have "... = p x"; by (rule quasinorm_minus, rule subspace_subsetD);
finally; show "- h x <= p x"; .;
qed;
from r; show "h x <= p x"; ..;
@@ -50,18 +44,17 @@
qed;
qed;
-
lemma some_H'h't:
- "[| M = norm_prev_extensions E p F f; c: chain M; graph H h = Union c; x:H|]
+ "[| 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 = norm_prev_extensions E p F f" and cM: "c: chain M"
- and "graph H h = Union c" "x:H";
+ assume m: "M = norm_pres_extensions E p F f" and cM: "c: chain M"
+ and u: "graph H h = Union c" "x:H";
- let ?P = "%H h. is_linearform H h
- & is_subspace H E
+ let ?P = "%H h. is_linearform H h
+ & is_subspace H E
& is_subspace F H
& (graph F f <= graph H h)
& (ALL x:H. h x <= p x)";
@@ -70,60 +63,62 @@
by (rule graphI2);
thus ?thesis;
proof (elim bexE);
- fix t; assume "t : (graph H h)" and "t = (x, h x)";
- have ex1: "EX g:c. t:g";
- by (simp! only: Union_iff);
+ fix t; assume t: "t : (graph H h)" "t = (x, h x)";
+ with u; have ex1: "EX g:c. t:g";
+ by (simp only: Union_iff);
thus ?thesis;
proof (elim bexE);
- fix g; assume "g:c" "t:g";
- have gM: "g:M";
- proof -;
- from cM; have "c <= M"; by (rule chainD2);
- thus ?thesis; ..;
- qed;
- have "EX H' h'. graph H' h' = g & ?P H' h'";
- proof (rule norm_prev_extension_D);
- from gM; show "g: norm_prev_extensions E p F f"; by (simp!);
- qed;
+ fix g; assume g: "g:c" "t:g";
+ from cM; have "c <= M"; by (rule chainD2);
+ hence "g : M"; ..;
+ hence "g : norm_pres_extensions E p F f"; by (simp only: m);
+ hence "EX H' h'. graph H' h' = g & ?P H' h'"; by (rule norm_pres_extension_D);
thus ?thesis; by (elim exE conjE, intro exI conjI) (simp | simp!)+;
qed;
qed;
qed;
-
-lemma some_H'h': "[| M = norm_prev_extensions E p F f; c: chain M; graph H h = Union c; x:H|]
+lemma some_H'h': "[| M = norm_pres_extensions E p F f; c: chain M; graph H h = Union c; x:H|]
==> EX H' h'. x:H' & (graph H' h' <= graph H h) &
is_linearform H' h' & is_subspace H' E & is_subspace F H' &
(graph F f <= graph H' h') & (ALL x:H'. h' x <= p x)";
proof -;
- assume "M = norm_prev_extensions E p F f" "c: chain M" "graph H h = Union c" "x:H";
-
- have "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)";
- by (rule some_H'h't);
-
+ assume m: "M = norm_pres_extensions E p F f" and cM: "c: chain M"
+ and u: "graph H h = Union c" "x:H";
+ have "(x, h x): graph H h"; by (rule graphI);
+ also; have "... = Union c"; .;
+ finally; have "(x, h x) : Union c"; .;
+ hence "EX g:c. (x, h x):g"; by (simp only: Union_iff);
thus ?thesis;
- proof (elim exE conjE, intro exI conjI);
- fix H' h' t;
- assume "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";
- show x: "x:H'"; by (simp!, rule graphD1);
- show "graph H' h' <= graph H h";
- by (simp! only: chain_ball_Union_upper);
+ proof (elim bexE);
+ fix g; assume g: "g:c" "(x, h x):g";
+ from cM; have "c <= M"; by (rule chainD2);
+ hence "g : M"; ..;
+ hence "g : norm_pres_extensions E p F f"; by (simp only: m);
+ hence "EX H' h'. graph H' h' = g
+ & is_linearform H' h'
+ & is_subspace H' E
+ & is_subspace F H'
+ & (graph F f <= graph H' h')
+ & (ALL x:H'. h' x <= p x)"; by (rule norm_pres_extension_D);
+ thus ?thesis;
+ proof (elim exE conjE, intro exI conjI);
+ fix H' h'; assume g': "graph H' h' = g";
+ with g; have "(x, h x): graph H' h'"; by simp;
+ thus "x:H'"; by (rule graphD1);
+ from g g'; have "graph H' h' : c"; by simp;
+ with cM u; show "graph H' h' <= graph H h"; by (simp only: chain_ball_Union_upper);
+ qed simp+;
qed;
qed;
-theorems [trans] = subsetD [COMP swap_prems_rl];
-
lemma some_H'h'2:
- "[| M = norm_prev_extensions E p F f; c: chain M; graph H h = Union c; x:H; y: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_prev_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
@@ -142,15 +137,15 @@
from e1 e2; show ?thesis;
proof (elim exE conjE);
fix H' h' t' H'' h'' t'';
- assume "t' : graph H h" "t'' : graph H h"
- "t' = (y, h y)" "t'' = (x, h x)"
- "graph H' h' : c" "graph H'' h'' : c"
- "t' : graph H' h'" "t'' : graph H'' h''"
- "is_linearform H' h'" "is_linearform H'' h''"
- "is_subspace H' E" "is_subspace H'' E"
- "is_subspace F H'" "is_subspace F H''"
- "graph F f <= graph H' h'" "graph F f <= graph H'' h''"
- "ALL x:H'. h' x <= p x" "ALL x:H''. h'' x <= p x";
+ assume "t' : graph H h" "t'' : graph H h"
+ "t' = (y, h y)" "t'' = (x, h x)"
+ "graph H' h' : c" "graph H'' h'' : c"
+ "t' : graph H' h'" "t'' : graph H'' h''"
+ "is_linearform H' h'" "is_linearform H'' h''"
+ "is_subspace H' E" "is_subspace H'' E"
+ "is_subspace F H'" "is_subspace F H''"
+ "graph F f <= graph H' h'" "graph F f <= graph H'' h''"
+ "ALL x:H'. h' x <= p x" "ALL x:H''. h'' x <= p x";
have "(graph H'' h'') <= (graph H' h') | (graph H' h') <= (graph H'' h'')";
by (rule chainD);
@@ -158,9 +153,10 @@
proof;
assume "(graph H'' h'') <= (graph H' h')";
show ?thesis;
- proof (intro exI conjI); note [trans] = subsetD;
+ proof (intro exI conjI);
+ note [trans] = subsetD;
have "(x, h x) : graph H'' h''"; by (simp!);
- also; have "... <= graph H' h'"; by (simp!);
+ also; have "... <= graph H' h'"; .;
finally; have xh: "(x, h x): graph H' h'"; .;
thus x: "x:H'"; by (rule graphD1);
show y: "y:H'"; by (simp!, rule graphD1);
@@ -173,7 +169,7 @@
proof (intro exI conjI);
show x: "x:H''"; by (simp!, rule graphD1);
have "(y, h y) : graph H' h'"; by (simp!);
- also; have "... <= graph H'' h''"; by (simp!);
+ also; have "... <= graph H'' h''"; .;
finally; have yh: "(y, h y): graph H'' h''"; .;
thus y: "y:H''"; by (rule graphD1);
show "(graph H'' h'') <= (graph H h)";
@@ -183,24 +179,21 @@
qed;
qed;
-lemmas chainE2 = chainD2 [elimify];
-lemmas [intro!!] = subsetD chainD;
-
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_prev_extensions E p F f; c : chain M;
+ 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_prev_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";
have "G1 : M"; ..;
hence e1: "EX H1 h1. graph H1 h1 = G1";
- by (force! dest: norm_prev_extension_D);
+ by (force! dest: norm_pres_extension_D);
have "G2 : M"; ..;
hence e2: "EX H2 h2. graph H2 h2 = G2";
- by (force! dest: norm_prev_extension_D);
+ by (force! dest: norm_pres_extension_D);
from e1 e2; show ?thesis;
proof (elim exE);
fix H1 h1 H2 h2; assume "graph H1 h1 = G1" "graph H2 h2 = G2";
@@ -233,10 +226,10 @@
qed;
-lemma sup_lf: "[| M = norm_prev_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_prev_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
@@ -299,10 +292,10 @@
qed;
-lemma sup_ext: "[| M = norm_prev_extensions E p F f; c: chain M; EX x. x:c; graph H h = Union c|]
+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_prev_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"
and e: "EX x. x:c";
thus ?thesis;
@@ -310,9 +303,9 @@
fix x; assume "x:c";
show ?thesis;
proof -;
- have "x:norm_prev_extensions E p F f";
+ have "x:norm_pres_extensions E p F f";
proof (rule subsetD);
- show "c <= norm_prev_extensions E p F f"; by (simp! add: chainD2);
+ show "c <= norm_pres_extensions E p F f"; by (simp! add: chainD2);
qed;
hence "(EX G g. graph G g = x
@@ -321,7 +314,7 @@
& is_subspace F G
& (graph F f <= graph G g)
& (ALL x:G. g x <= p x))";
- by (simp! add: norm_prev_extension_D);
+ by (simp! add: norm_pres_extension_D);
thus ?thesis;
proof (elim exE conjE);
@@ -338,10 +331,10 @@
qed;
-lemma sup_supF: "[| M = norm_prev_extensions E p F f; c: chain M; EX x. x:c; graph H h = Union c;
+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_prev_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;
@@ -366,10 +359,10 @@
qed;
-lemma sup_subE: "[| M = norm_prev_extensions E p F f; c: chain M; EX x. x:c; graph H h = Union c;
+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_prev_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;
@@ -447,10 +440,10 @@
qed;
-lemma sup_norm_prev: "[| M = norm_prev_extensions E p F f; c: chain M; graph H h = Union c|]
+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_prev_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 -;
--- a/src/HOL/Real/HahnBanach/LinearSpace.thy Wed Sep 29 15:35:09 1999 +0200
+++ b/src/HOL/Real/HahnBanach/LinearSpace.thy Wed Sep 29 16:41:52 1999 +0200
@@ -63,88 +63,80 @@
thus "x [+] y [+] z = x [+] (y [+] z)"; by (elim bspec[elimify]);
qed force+;
-
-
lemma zero_in_vs [simp, intro]: "is_vectorspace V ==> <0>:V";
- by (unfold is_vectorspace_def) (simp!);
+ 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";
- by (unfold is_vectorspace_def) (simp!);
+ 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!);
+ by (unfold is_vectorspace_def) simp;
lemma vs_diff_closed [simp, intro!!]: "[| is_vectorspace V; x: V; y: V|] ==> x [-] y: V";
- by (unfold diff_def negate_def) (simp!);
+ by (unfold diff_def negate_def) simp;
lemma vs_neg_closed [simp, intro!!]: "[| is_vectorspace V; x: V |] ==> [-] x: V";
- by (unfold negate_def) (simp!);
+ by (unfold negate_def) simp;
lemma vs_add_assoc [simp]:
"[| is_vectorspace V; x: V; y: V; z: V|] ==> x [+] y [+] z = x [+] (y [+] z)";
by (unfold is_vectorspace_def) fast;
lemma vs_add_commute [simp]: "[| is_vectorspace V; x:V; y:V |] ==> y [+] x = x [+] y";
- by (unfold is_vectorspace_def) (simp!);
+ by (unfold is_vectorspace_def) simp;
lemma vs_add_left_commute [simp]:
"[| is_vectorspace V; x:V; y:V; z:V |] ==> x [+] (y [+] z) = y [+] (x [+] z)";
proof -;
- assume vs: "is_vectorspace V" "x:V" "y:V" "z:V";
- have "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);
+ assume "is_vectorspace V" "x:V" "y:V" "z:V";
+ hence "x [+] (y [+] z) = (x [+] y) [+] z"; by (simp only: vs_add_assoc);
+ also; have "... = (y [+] x) [+] z"; by (simp! only: vs_add_commute);
+ also; have "... = y [+] (x [+] z)"; by (simp! only: vs_add_assoc);
finally; show ?thesis; .;
qed;
-
theorems vs_add_ac = vs_add_assoc vs_add_commute vs_add_left_commute;
lemma vs_diff_self [simp]: "[| is_vectorspace V; x:V |] ==> x [-] x = <0>";
- by (unfold is_vectorspace_def) (simp!);
+ by (unfold is_vectorspace_def) simp;
lemma vs_add_zero_left [simp]: "[| is_vectorspace V; x:V |] ==> <0> [+] x = x";
- by (unfold is_vectorspace_def) (simp!);
+ by (unfold is_vectorspace_def) simp;
lemma vs_add_zero_right [simp]: "[| is_vectorspace V; x:V |] ==> x [+] <0> = x";
proof -;
- assume vs: "is_vectorspace V" "x:V";
- have "x [+] <0> = <0> [+] x";
- by (simp!);
- also; have "... = x";
- by (simp!);
+ assume "is_vectorspace V" "x:V";
+ hence "x [+] <0> = <0> [+] x"; by simp;
+ also; have "... = x"; by (simp!);
finally; show ?thesis; .;
qed;
lemma vs_add_mult_distrib1:
"[| is_vectorspace V; x:V; y:V |] ==> a [*] (x [+] y) = a [*] x [+] a [*] y";
- by (unfold is_vectorspace_def) (simp!);
+ by (unfold is_vectorspace_def) simp;
lemma vs_add_mult_distrib2:
"[| is_vectorspace V; x:V |] ==> (a + b) [*] x = a [*] x [+] b [*] x";
- by (unfold is_vectorspace_def) (simp!);
+ 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!);
+ by (unfold is_vectorspace_def) simp;
lemma vs_mult_assoc2 [simp]: "[| is_vectorspace V; x:V |] ==> a [*] b [*] x = (a * b) [*] x";
- by (simp! only: vs_mult_assoc);
+ by (simp only: vs_mult_assoc);
lemma vs_mult_1 [simp]: "[| is_vectorspace V; x:V |] ==> 1r [*] x = x";
- by (unfold is_vectorspace_def) (simp!);
+ by (unfold is_vectorspace_def) simp;
lemma vs_diff_mult_distrib1:
"[| is_vectorspace V; x:V; y:V |] ==> a [*] (x [-] y) = a [*] x [-] a [*] y";
- by (simp! add: diff_def negate_def vs_add_mult_distrib1);
+ by (simp add: diff_def negate_def vs_add_mult_distrib1);
lemma vs_minus_eq: "[| is_vectorspace V; x:V |] ==> - b [*] x = [-] (b [*] x)";
- by (simp! add: negate_def);
+ by (simp add: negate_def);
lemma vs_diff_mult_distrib2:
"[| is_vectorspace V; x:V |] ==> (a - b) [*] x = a [*] x [-] (b [*] x)";
@@ -159,60 +151,48 @@
lemma vs_mult_zero_left [simp]: "[| is_vectorspace V; x: V|] ==> 0r [*] x = <0>";
proof -;
- assume vs: "is_vectorspace V" "x:V";
- have "0r [*] x = (1r - 1r) [*] x";
- by (simp! only: real_diff_self);
- also; have "... = (1r + - 1r) [*] x";
- by simp;
- also; have "... = 1r [*] x [+] (- 1r) [*] x";
- by (rule vs_add_mult_distrib2);
- also; have "... = x [+] (- 1r) [*] x";
- by (simp!);
- also; have "... = x [-] x";
- by (rule vs_add_mult_minus_1_eq_diff);
- also; have "... = <0>";
- by (simp!);
+ assume "is_vectorspace V" "x:V";
+ have "0r [*] x = (1r - 1r) [*] x"; by (simp only: real_diff_self);
+ also; have "... = (1r + - 1r) [*] x"; by simp;
+ also; have "... = 1r [*] x [+] (- 1r) [*] x"; by (rule vs_add_mult_distrib2);
+ also; have "... = x [+] (- 1r) [*] x"; by (simp!);
+ also; have "... = x [-] x"; by (rule vs_add_mult_minus_1_eq_diff);
+ also; have "... = <0>"; by (simp!);
finally; show ?thesis; .;
qed;
lemma vs_mult_zero_right [simp]: "[| is_vectorspace (V:: 'a set) |] ==> a [*] <0> = (<0>::'a)";
proof -;
- assume vs: "is_vectorspace V";
- have "a [*] <0> = a [*] (<0> [-] (<0>::'a))";
- by (simp!);
- also; from zero_in_vs [of V]; have "... = a [*] <0> [-] a [*] <0>";
- by (simp! only: vs_diff_mult_distrib1);
- also; have "... = <0>";
- by (simp!);
+ assume "is_vectorspace V";
+ have "a [*] <0> = a [*] (<0> [-] (<0>::'a))"; by (simp!);
+ also; have "... = a [*] <0> [-] a [*] <0>";
+ by (rule vs_diff_mult_distrib1) (simp!)+;
+ also; have "... = <0>"; by (simp!);
finally; show ?thesis; .;
qed;
lemma vs_minus_mult_cancel [simp]: "[| is_vectorspace V; x:V |] ==> (- a) [*] [-] x = a [*] x";
- by (unfold negate_def) (simp!);
+ by (unfold negate_def) simp;
lemma vs_add_minus_left_eq_diff: "[| is_vectorspace V; x:V; y:V |] ==> [-] x [+] y = y [-] x";
proof -;
- assume vs: "is_vectorspace V";
- assume x: "x:V"; hence nx: "[-] x:V"; by (simp!);
- assume y: "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);
+ 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);
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);
+ by (simp add: vs_add_minus_eq_diff);
lemma vs_add_minus_left [simp]: "[| is_vectorspace V; x:V |] ==> [-] x [+] x = <0>";
- by (simp! add: vs_add_minus_eq_diff);
+ by (simp add: vs_add_minus_eq_diff);
lemma vs_minus_minus [simp]: "[| is_vectorspace V; x:V|] ==> [-] [-] x = x";
- by (unfold negate_def) (simp!);
+ by (unfold negate_def) simp;
lemma vs_minus_zero [simp]: "[| is_vectorspace (V::'a set)|] ==> [-] (<0>::'a) = <0>";
- by (unfold negate_def) (simp!);
+ by (unfold negate_def) simp;
lemma vs_minus_zero_iff [simp]:
"[| is_vectorspace V; x:V|] ==> ([-] x = <0>) = (x = <0>)" (concl is "?L = ?R");
@@ -221,54 +201,44 @@
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 (rule vs_minus_zero);
+ have "x = [-] [-] x"; by (rule vs_minus_minus [RS sym]);
+ also; have "... = [-] <0>"; by (rule l [RS arg_cong] );
+ also; have "... = <0>"; by (rule vs_minus_zero);
finally; show ?R; .;
next;
assume ?R;
- with vs; show ?L;
- by simp;
+ with vs; show ?L; by simp;
qed;
qed;
lemma vs_add_minus_cancel [simp]: "[| is_vectorspace V; x:V; y:V|] ==> x [+] ([-] x [+] y) = y";
- by (simp! add: vs_add_assoc [RS sym] del: vs_add_commute);
+ by (simp add: vs_add_assoc [RS sym] del: vs_add_commute);
lemma vs_minus_add_cancel [simp]: "[| is_vectorspace V; x:V; y:V |] ==> [-] x [+] (x [+] y) = y";
- by (simp! add: vs_add_assoc [RS sym] del: vs_add_commute);
+ by (simp add: vs_add_assoc [RS sym] del: vs_add_commute);
lemma vs_minus_add_distrib [simp]:
"[| is_vectorspace V; x:V; y:V|] ==> [-] (x [+] y) = [-] x [+] [-] y";
- by (unfold negate_def, simp! add: vs_add_mult_distrib1);
+ by (unfold negate_def, simp add: vs_add_mult_distrib1);
lemma vs_diff_zero [simp]: "[| is_vectorspace V; x:V |] ==> x [-] <0> = x";
- by (unfold diff_def) (simp!);
+ by (unfold diff_def) simp;
lemma vs_diff_zero_right [simp]: "[| is_vectorspace V; x:V |] ==> <0> [-] x = [-] x";
- by (unfold diff_def) (simp!);
+ by (unfold diff_def) simp;
lemma vs_add_left_cancel:
"[|is_vectorspace V; x:V; y:V; z:V|] ==> (x [+] y = x [+] z) = (y = z)"
(concl is "?L = ?R");
proof;
- assume vs: "is_vectorspace V" and x: "x:V" and y: "y:V" and z: "z:V";
+ 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; from vs vs_neg_closed x y ; have "... = [-] x [+] (x [+] y)";
- by (rule vs_add_assoc);
- also; have "... = [-] x [+] (x [+] z)";
- by (simp! only: l);
- also; from vs vs_neg_closed x z; have "... = [-] x [+] x [+] z";
- by (rule vs_add_assoc [RS sym]);
- also; have "... = z";
- by (simp!);
+ have "y = <0> [+] y"; by (simp!);
+ also; have "... = [-] x [+] x [+] y"; by (simp!);
+ also; have "... = [-] x [+] (x [+] y)"; by (simp! only: vs_add_assoc vs_neg_closed);
+ also; have "... = [-] x [+] (x [+] z)"; by (simp only: l);
+ also; have "... = [-] x [+] x [+] z"; by (rule vs_add_assoc [RS sym]) (simp!)+;
+ also; have "... = z"; by (simp!);
finally; show ?R;.;
next;
assume ?R;
@@ -277,125 +247,15 @@
lemma vs_add_right_cancel:
"[| is_vectorspace V; x:V; y:V; z:V |] ==> (y [+] x = z [+] x) = (y = z)";
- by (simp! only: vs_add_commute vs_add_left_cancel);
+ by (simp only: vs_add_commute vs_add_left_cancel);
-lemma vs_add_assoc_cong [tag FIXME simp]: "[| is_vectorspace V; x:V; y:V; x':V; y':V; z:V |] \
-\ ==> x [+] y = x' [+] y' ==> x [+] (y [+] z) = x' [+] (y' [+] z)";
- by (simp! del: vs_add_commute vs_add_assoc add: vs_add_assoc [RS sym]);
+lemma vs_add_assoc_cong [tag FIXME simp]: "[| is_vectorspace V; x:V; y:V; x':V; y':V; z:V |]
+ ==> x [+] y = x' [+] y' ==> x [+] (y [+] z) = x' [+] (y' [+] z)";
+ by (simp del: vs_add_commute vs_add_assoc add: vs_add_assoc [RS sym]);
lemma vs_mult_left_commute:
"[| is_vectorspace V; x:V; y:V; z:V |] ==> x [*] y [*] z = y [*] x [*] z";
- by (simp! add: real_mult_commute);
-
-lemma vs_mult_left_cancel:
- "[| is_vectorspace V; x:V; y:V; a ~= 0r |] ==> (a [*] x = a [*] y) = (x = y)"
- (concl is "?L = ?R");
-proof;
- assume vs: "is_vectorspace V";
- assume x: "x:V";
- assume y: "y:V";
- assume a: "a ~= 0r";
- assume l: ?L;
- have "x = 1r [*] x";
- by (simp!);
- also; have "... = (rinv a * a) [*] x";
- by (simp!);
- also; have "... = rinv a [*] (a [*] x)";
- by (simp! only: vs_mult_assoc);
- also; have "... = rinv a [*] (a [*] y)";
- by (simp! only: l);
- also; have "... = y";
- by (simp!);
- finally; show ?R;.;
-next;
- assume ?R;
- show ?L;
- by (simp!);
-qed;
-
-lemma vs_eq_diff_eq:
- "[| is_vectorspace V; x:V; y:V; z:V |] ==> (x = z [-] y) = (x [+] y = z)"
- (concl is "?L = ?R" );
-proof -;
- assume vs: "is_vectorspace V";
- assume x: "x:V";
- assume y: "y:V"; hence n: "[-] y:V"; by (simp!);
- assume z: "z:V";
- show "?L = ?R";
- proof;
- assume l: ?L;
- have "x [+] y = z [-] y [+] y";
- by (simp! add: l);
- also; have "... = z [+] [-] y [+] y";
- by (simp! only: vs_add_minus_eq_diff);
- also; from vs z n y; have "... = z [+] ([-] y [+] y)";
- by (simp! only: vs_add_assoc);
- also; have "... = z [+] <0>";
- by (simp! only: vs_add_minus_left);
- also; 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; have "... = x [+] y [+] [-] y";
- by (simp! only: vs_add_minus_eq_diff);
- also; from vs x y n; have "... = x [+] (y [+] [-] y)";
- by (rule vs_add_assoc);
- also; have "... = x";
- by (simp!);
- finally; show ?L; by (rule sym);
- qed;
-qed;
-
-lemma vs_add_minus_eq_minus: "[| is_vectorspace V; x:V; y:V; <0> = x [+] y|] ==> y = [-] x";
-proof -;
- assume vs: "is_vectorspace V";
- assume x: "x:V"; hence n: "[-] x : V"; by (simp!);
- assume y: "y:V";
- assume xy: "<0> = x [+] y";
- from vs n; have "[-] x = [-] x [+] <0>";
- by (simp!);
- also; have "... = [-] x [+] (x [+] y)";
- by (simp!);
- also; from vs n x y; have "... = [-] x [+] x [+] y";
- by (rule vs_add_assoc [RS sym]);
- also; from vs x y; have "... = (x [+] [-] x) [+] y";
- by simp;
- also; from vs y; have "... = y";
- by (simp!);
- finally; show ?thesis;
- by (rule sym);
-qed;
-
-lemma vs_add_minus_eq: "[| is_vectorspace V; x:V; y:V; x [-] y = <0> |] ==> x = y";
-proof -;
- assume "is_vectorspace V" "x:V" "y:V" "x [-] y = <0>";
- have "x [+] [-] y = x [-] y"; by (unfold diff_def, simp);
- also; have "... = <0>"; .;
- finally; have e: "<0> = x [+] [-] y"; by (rule sym);
- have "x = [-] [-] x"; by (simp!);
- also; from _ _ _ e; have "[-] x = [-] y";
- by (rule vs_add_minus_eq_minus [RS sym, of V x "[-] y"]) (simp!)+;
- also; have "[-] ... = y"; by (simp!);
- finally; show "x = y"; .;
-qed;
-
-lemma vs_add_diff_swap:
- "[| is_vectorspace V; a:V; b:V; c:V; d:V; a [+] b = c [+] d|] ==> a [-] c = d [-] b";
-proof -;
- assume vs: "is_vectorspace V" "a:V" "b:V" "c:V" "d:V" and eq: "a [+] b = c [+] d";
- have "[-] c [+] (a [+] b) = [-] c [+] (c [+] d)"; by (simp! add: vs_add_left_cancel);
- also; have "... = d"; by (rule vs_minus_add_cancel);
- finally; have eq: "[-] c [+] (a [+] b) = d"; .;
- from vs; have "a [-] c = ([-] c [+] (a [+] b)) [+] [-] b";
- by (simp add: vs_add_ac diff_def);
- also; from eq; have "... = d [+] [-] b"; by (simp! add: vs_add_right_cancel);
- also; have "... = d [-] b"; by (simp add : diff_def);
- finally; show "a [-] c = d [-] b"; .;
-qed;
-
+ by (simp add: real_mult_commute);
lemma vs_mult_zero_uniq :
"[| is_vectorspace V; x:V; a [*] x = <0>; x ~= <0> |] ==> a = 0r";
@@ -410,39 +270,124 @@
thus "a = 0r"; by contradiction;
qed;
+lemma vs_mult_left_cancel:
+ "[| is_vectorspace V; x:V; y:V; a ~= 0r |] ==> (a [*] x = a [*] y) = (x = y)"
+ (concl is "?L = ?R");
+proof;
+ assume "is_vectorspace V" "x:V" "y:V" "a ~= 0r";
+ assume l: ?L;
+ have "x = 1r [*] x"; by (simp!);
+ also; have "... = (rinv a * a) [*] x"; by (simp!);
+ also; have "... = rinv a [*] (a [*] x)"; by (simp! only: vs_mult_assoc);
+ also; have "... = rinv a [*] (a [*] y)"; by (simp only: l);
+ also; have "... = y"; by (simp!);
+ finally; show ?R;.;
+next;
+ assume ?R;
+ thus ?L; by simp;
+qed;
+
+lemma vs_mult_right_cancel:
+ "[| is_vectorspace V; x:V; x ~= <0> |] ==> (a [*] x = b [*] x) = (a = b)"
+ (concl is "?L = ?R");
+proof;
+ assume "is_vectorspace V" "x:V" "x ~= <0>";
+ assume l: ?L;
+ show "a = b";
+ proof (rule real_add_minus_eq);
+ show "a - b = 0r";
+ proof (rule vs_mult_zero_uniq);
+ have "(a - b) [*] x = a [*] x [-] b [*] x"; by (simp! add: vs_diff_mult_distrib2);
+ also; from l; have "a [*] x [-] b [*] x = <0>"; by (simp!);
+ finally; show "(a - b) [*] x = <0>"; .;
+ qed;
+ qed;
+next;
+ assume ?R;
+ thus ?L; by simp;
+qed;
+
+lemma vs_eq_diff_eq:
+ "[| is_vectorspace V; x:V; y:V; z:V |] ==> (x = z [-] y) = (x [+] y = z)"
+ (concl is "?L = ?R" );
+proof -;
+ assume vs: "is_vectorspace V" "x:V" "y:V" "z:V";
+ show "?L = ?R";
+ proof;
+ assume l: ?L;
+ have "x [+] y = z [-] y [+] y"; by (simp add: l);
+ also; have "... = z [+] [-] y [+] y"; by (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; 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; have "... = x"; by (simp!);
+ finally; show ?L; by (rule sym);
+ qed;
+qed;
+
+lemma vs_add_minus_eq_minus: "[| is_vectorspace V; x:V; y:V; <0> = x [+] y|] ==> y = [-] x";
+proof -;
+ assume vs: "is_vectorspace V" "x:V" "y:V";
+ assume "<0> = x [+] y";
+ have "[-] x = [-] x [+] <0>"; by (simp!);
+ also; have "... = [-] x [+] (x [+] y)"; by (simp!);
+ also; have "... = [-] x [+] x [+] y"; by (rule vs_add_assoc [RS sym]) (simp!)+;
+ also; have "... = (x [+] [-] x) [+] y"; by (simp!);
+ also; have "... = y"; by (simp!);
+ finally; show ?thesis; by (rule sym);
+qed;
+
+lemma vs_add_minus_eq: "[| is_vectorspace V; x:V; y:V; x [-] y = <0> |] ==> x = y";
+proof -;
+ assume "is_vectorspace V" "x:V" "y:V" "x [-] y = <0>";
+ have "x [+] [-] y = x [-] y"; by (unfold diff_def, simp);
+ also; have "... = <0>"; .;
+ finally; have e: "<0> = x [+] [-] y"; by (rule sym);
+ have "x = [-] [-] x"; by (simp!);
+ also; have "[-] x = [-] y"; by (rule vs_add_minus_eq_minus [RS sym]) (simp! add: e)+;
+ also; have "[-] ... = y"; by (simp!);
+ finally; show "x = y"; .;
+qed;
+
+lemma vs_add_diff_swap:
+ "[| is_vectorspace V; a:V; b:V; c:V; d:V; a [+] b = c [+] d|] ==> a [-] c = d [-] b";
+proof -;
+ assume vs: "is_vectorspace V" "a:V" "b:V" "c:V" "d:V" and eq: "a [+] b = c [+] d";
+ have "[-] c [+] (a [+] b) = [-] c [+] (c [+] d)"; by (simp! add: vs_add_left_cancel);
+ also; have "... = d"; by (rule vs_minus_add_cancel);
+ finally; have eq: "[-] c [+] (a [+] b) = d"; .;
+ from vs; have "a [-] c = ([-] c [+] (a [+] b)) [+] [-] b"; by (simp add: vs_add_ac diff_def);
+ also; from eq; have "... = d [+] [-] b"; by (simp! add: vs_add_right_cancel);
+ also; have "... = d [-] b"; by (simp add : diff_def);
+ finally; show "a [-] c = d [-] b"; .;
+qed;
+
lemma vs_add_cancel_21:
"[| is_vectorspace V; x:V; y:V; z:V; u:V|] ==> (x [+] (y [+] z) = y [+] u) = ((x [+] z) = u)"
(concl is "?L = ?R" );
proof -;
- assume vs: "is_vectorspace V";
- assume x: "x:V";
- assume y: "y:V"; hence n: "[-] y:V"; by (simp!);
- assume z: "z:V"; hence xz: "x [+] z: V"; by (simp!);
- assume u: "u:V";
+ assume vs: "is_vectorspace V" "x:V" "y:V""z:V" "u:V";
show "?L = ?R";
proof;
assume l: ?L;
- from vs u; have "u = <0> [+] u";
- by (simp!);
- also; from vs y vs_neg_closed u; have "... = [-] y [+] y [+] u";
- by (simp!);
- also; from vs n y u; have "... = [-] y [+] (y [+] u)";
- by (simp! only: vs_add_assoc);
- also; have "... = [-] y [+] (x [+] (y [+] z))";
- by (simp! only: l);
- also; have "... = [-] y [+] (y [+] (x [+] z))";
- by (simp! only: vs_add_left_commute);
- also; from vs n y xz; have "... = [-] y [+] y [+] (x [+] z)";
- by (simp! only: vs_add_assoc);
- also; have "... = (x [+] z)";
- by (simp!);
+ have "u = <0> [+] u"; by (simp!);
+ also; have "... = [-] y [+] y [+] u"; by (simp!);
+ also; have "... = [-] y [+] (y [+] u)"; by (rule vs_add_assoc) (simp!)+;
+ also; have "... = [-] y [+] (x [+] (y [+] z))"; by (simp only: l);
+ also; have "... = [-] y [+] (y [+] (x [+] z))"; by (simp!);
+ also; have "... = [-] y [+] y [+] (x [+] z)"; by (rule vs_add_assoc [RS sym]) (simp!)+;
+ also; have "... = (x [+] z)"; by (simp!);
finally; show ?R; by (rule sym);
next;
assume r: ?R;
- have "x [+] (y [+] z) = y [+] (x [+] z)";
- by (simp! only: vs_add_left_commute [of V x y z]);
- also; have "... = y [+] u";
- by (simp! only: r);
+ have "x [+] (y [+] z) = y [+] (x [+] z)"; by (simp! only: vs_add_left_commute [of V x]);
+ also; have "... = y [+] u"; by (simp only: r);
finally; show ?L; .;
qed;
qed;
@@ -451,44 +396,31 @@
"[| 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";
- assume x: "x:V";
- assume y: "y:V";
- assume z: "z:V"; hence xz: "x [+] z: V"; by (simp!);
- hence nz: "[-] z: V"; by (simp!);
+ assume vs: "is_vectorspace V" "x:V" "y:V" "z:V";
show "?L = ?R";
proof;
assume l: ?L;
- have n: "<0>:V"; by (simp!);
- have "y [+] <0> = y";
- by (simp! only: vs_add_zero_right);
- also; have "... = x [+] (y [+] z)";
- by (simp! only: l);
- also; have "... = y [+] (x [+] z)";
- by (simp! only: vs_add_left_commute);
- finally; have "y [+] <0> = y [+] (x [+] z)"; .;
- with vs y n xz; have "<0> = x [+] z";
- by (rule vs_add_left_cancel [RS iffD1]);
- with vs x z; have "z = [-] x";
- by (simp! only: vs_add_minus_eq_minus);
- then; show ?R;
- by (simp!);
+ have "<0> = x [+] z";
+ proof (rule vs_add_left_cancel [RS iffD1]);
+ have "y [+] <0> = y"; by (simp! only: vs_add_zero_right);
+ also; have "... = x [+] (y [+] z)"; by (simp only: l);
+ also; have "... = y [+] (x [+] z)"; by (simp! only: vs_add_left_commute);
+ finally; show "y [+] <0> = y [+] (x [+] z)"; .;
+ qed (simp!)+;
+ hence "z = [-] x"; by (simp! only: vs_add_minus_eq_minus);
+ then; show ?R; by (simp!);
next;
assume r: ?R;
- have "x [+] (y [+] z) = [-] z [+] (y [+] z)";
- by (simp! only: r);
- also; from vs nz y z; have "... = y [+] ([-] z [+] z)";
- by (simp! only: vs_add_left_commute);
- also; have "... = y [+] <0>";
- by (simp!);
- also; have "... = y";
- by (simp!);
+ have "x [+] (y [+] z) = [-] z [+] (y [+] z)"; by (simp only: r);
+ also; have "... = y [+] ([-] z [+] z)"; by (simp! only: vs_add_left_commute);
+ also; have "... = y [+] <0>"; by (simp!);
+ also; have "... = y"; by (simp!);
finally; show ?L; .;
qed;
qed;
lemma it: "[| x = y; x' = y'|] ==> x [+] x' = y [+] y'";
- by (simp!);
+ by simp;
end;
\ No newline at end of file
--- a/src/HOL/Real/HahnBanach/Linearform.thy Wed Sep 29 15:35:09 1999 +0200
+++ b/src/HOL/Real/HahnBanach/Linearform.thy Wed Sep 29 16:41:52 1999 +0200
@@ -46,7 +46,7 @@
finally; show "f (x [-] y) = f x - f y"; by (simp!);
qed;
-lemma linearform_zero [intro!!]: "[| 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!);
--- a/src/HOL/Real/HahnBanach/Subspace.thy Wed Sep 29 15:35:09 1999 +0200
+++ b/src/HOL/Real/HahnBanach/Subspace.thy Wed Sep 29 16:41:52 1999 +0200
@@ -17,39 +17,37 @@
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";
- by (unfold is_subspace_def) (simp!);
+ by (unfold is_subspace_def) simp;
lemma "is_subspace U V ==> U ~= {}";
by (unfold is_subspace_def) force;
lemma zero_in_subspace [intro !!]: "is_subspace U V ==> <0>:U";
- by (unfold is_subspace_def) (simp!);;
+ by (unfold is_subspace_def) simp;;
lemma subspace_subset [intro !!]: "is_subspace U V ==> U <= V";
- by (unfold is_subspace_def) (simp!);
+ by (unfold is_subspace_def) simp;
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!);
+ by (unfold is_subspace_def) simp;
lemma subspace_mult_closed [simp, intro!!]: "[| is_subspace U V; x: U |] ==> a [*] x: U";
- by (unfold is_subspace_def) (simp!);
+ 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!);
+ 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!);
+ by (unfold negate_def) simp;
theorem subspace_vs [intro!!]:
"[| is_subspace U V; is_vectorspace V |] ==> is_vectorspace U";
proof -;
- assume "is_subspace U V";
- assume "is_vectorspace V";
- assume "is_subspace U V";
+ assume "is_subspace U V" "is_vectorspace V";
show ?thesis;
proof;
show "<0>:U"; ..;
@@ -71,14 +69,17 @@
proof;
assume "is_subspace U V" "is_subspace V W";
show "<0> : U"; ..;
+
have "U <= V"; ..;
also; have "V <= W"; ..;
finally; show "U <= W"; .;
+
show "ALL x:U. ALL y:U. x [+] y : U";
proof (intro ballI);
fix x y; assume "x:U" "y:U";
show "x [+] y : U"; by (simp!);
qed;
+
show "ALL x:U. ALL a. a [*] x : U";
proof (intro ballI allI);
fix x a; assume "x:U";
@@ -96,6 +97,9 @@
lemma linD: "x : lin v = (? a::real. x = a [*] v)";
by (unfold lin_def) force;
+lemma linI [intro!!]: "a [*] x0 : lin x0";
+ by (unfold lin_def) force;
+
lemma x_lin_x: "[| is_vectorspace V; x:V |] ==> x:lin x";
proof (unfold lin_def, intro CollectI exI);
assume "is_vectorspace V" "x:V";
@@ -151,7 +155,7 @@
"vectorspace_sum U V == {x. ? u:U. ? v:V. x = u [+] v}";
lemma vs_sumD: "x:vectorspace_sum U V = (? u:U. ? v:V. x = u [+] v)";
- by (unfold vectorspace_sum_def) (simp!);
+ by (unfold vectorspace_sum_def) simp;
lemmas vs_sumE = vs_sumD [RS iffD1, elimify];
@@ -189,8 +193,7 @@
proof (intro vs_sumI);
show "<0> : U"; ..;
show "<0> : V"; ..;
- show "(<0>::'a) = <0> [+] <0>";
- by (simp!);
+ show "(<0>::'a) = <0> [+] <0>"; by (simp!);
qed;
show "vectorspace_sum U V <= E";
@@ -232,69 +235,76 @@
section {* special case: 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";
+ have eq: "u1 [-] u2 = v2 [-] v1"; by (simp! add: vs_add_diff_swap);
+ have u: "u1 [-] u2 : U"; by (simp!); with eq; have v': "v2 [-] v1 : U"; by simp;
+ have v: "v2 [-] v1 : V"; by (simp!); with eq; have u': "u1 [-] u2 : V"; by simp;
+
+ show "u1 = u2";
+ proof (rule vs_add_minus_eq);
+ show "u1 [-] u2 = <0>"; by (rule Int_singletonD [OF _ u u']);
+ qed (rule);
+
+ show "v1 = v2";
+ proof (rule vs_add_minus_eq [RS sym]);
+ show "v2 [-] v1 = <0>"; by (rule Int_singletonD [OF _ v' v]);
+ 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 |]
==> y1 = y2 & a1 = a2";
proof;
- assume "is_vectorspace E" "is_subspace H E"
- "y1 : H" "y2 : H" "x0 ~: H" "x0 : E" "x0 ~= <0>"
+ assume "is_vectorspace E" and h: "is_subspace H E"
+ and "y1 : H" "y2 : H" "x0 ~: H" "x0 : E" "x0 ~= <0>"
"y1 [+] a1 [*] x0 = y2 [+] a2 [*] x0";
- have h: "is_vectorspace H"; ..;
- have "y1 [-] y2 = a2 [*] x0 [-] a1 [*] x0";
- by (simp! add: vs_add_diff_swap);
- also; have "... = (a2 - a1) [*] x0";
- by (rule vs_diff_mult_distrib2 [RS sym]);
- finally; have eq: "y1 [-] y2 = (a2 - a1) [*] x0"; .;
-
- have y: "y1 [-] y2 : H"; by (simp!);
- have x: "(a2 - a1) [*] x0 : lin x0"; by (simp! add: lin_def) force;
- from eq y x; have y': "y1 [-] y2 : lin x0"; by simp;
- from eq y x; have x': "(a2 - a1) [*] x0 : H"; by simp;
- have int: "H Int (lin x0) = {<0>}";
- proof;
- show "H Int lin x0 <= {<0>}";
- proof (intro subsetI, elim IntE, rule singleton_iff[RS iffD2]);
- fix x; assume "x:H" "x:lin x0";
- thus "x = <0>";
- proof (unfold lin_def, elim CollectE exE);
- fix a; assume "x = a [*] x0";
- show ?thesis;
- proof (rule case [of "a = 0r"]);
- assume "a = 0r"; show ?thesis; by (simp!);
- next;
- assume "a ~= 0r";
- have "(rinv a) [*] a [*] x0 : H";
- by (rule vs_mult_closed [OF h]) (simp!);
- also; have "(rinv a) [*] a [*] x0 = x0"; by (simp!);
- finally; have "x0 : H"; .;
- thus ?thesis; by contradiction;
- qed;
- qed;
+ have c: "y1 = y2 & a1 [*] x0 = a2 [*] x0";
+ proof (rule decomp);
+ show "a1 [*] x0 : lin x0"; ..;
+ show "a2 [*] x0 : lin x0"; ..;
+ show "H Int (lin x0) = {<0>}";
+ proof;
+ show "H Int lin x0 <= {<0>}";
+ proof (intro subsetI, elim IntE, rule singleton_iff[RS iffD2]);
+ fix x; assume "x:H" "x:lin x0";
+ thus "x = <0>";
+ proof (unfold lin_def, elim CollectE exE);
+ fix a; assume "x = a [*] x0";
+ show ?thesis;
+ proof (rule case_split [of "a = 0r"]);
+ 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!);
+ also; have "(rinv a) [*] a [*] x0 = x0"; by (simp!);
+ finally; have "x0 : H"; .;
+ thus ?thesis; by contradiction;
+ qed;
+ qed;
+ qed;
+ show "{<0>} <= H Int lin x0";
+ proof (intro subsetI, elim singletonE, intro IntI, simp+);
+ show "<0> : H"; ..;
+ from lin_vs; show "<0> : lin x0"; ..;
+ qed;
qed;
- show "{<0>} <= H Int lin x0";
- proof (intro subsetI, elim singletonE, intro IntI, simp+);
- show "<0> : H"; ..;
- from lin_vs; show "<0> : lin x0"; ..;
- qed;
+ show "is_subspace (lin x0) E"; ..;
qed;
-
- from h; show "y1 = y2";
- proof (rule vs_add_minus_eq);
- show "y1 [-] y2 = <0>";
- by (rule Int_singletonD [OF int y y']);
- qed;
-
- show "a1 = a2";
- proof (rule real_add_minus_eq [RS sym]);
- show "a2 - a1 = 0r";
- proof (rule vs_mult_zero_uniq);
- show "(a2 - a1) [*] x0 = <0>"; by (rule Int_singletonD [OF int x' x]);
- qed;
+
+ from c; show "y1 = y2"; by simp;
+
+ show "a1 = a2";
+ proof (rule vs_mult_right_cancel [RS iffD1]);
+ from c; show "a1 [*] x0 = a2 [*] x0"; by simp;
qed;
qed;
-
lemma decomp1:
"[| is_vectorspace E; is_subspace H E; t:H; x0~:H; x0:E; x0 ~= <0> |]
==> (@ (y, a). t = y [+] a [*] x0 & y : H) = (t, 0r)";
@@ -303,11 +313,10 @@
have h: "is_vectorspace H"; ..;
fix y a; presume t1: "t = y [+] a [*] x0" and "y : H";
have "y = t & a = 0r";
- by (rule decomp4) (assumption+, (simp!));
+ by (rule decomp4) (assumption | (simp!))+;
thus "(y, a) = (t, 0r)"; by (simp!);
qed (simp!)+;
-
lemma decomp3:
"[| h0 = (%x. let (y, a) = @ (y, a). (x = y [+] a [*] x0 & y:H)
in (h y) + a * xi);
@@ -316,14 +325,14 @@
==> 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)";
- assume "x = y [+] a [*] x0";
- assume "is_vectorspace E" "is_subspace H E" "y:H" "x0 ~: H" "x0:E" "x0 ~= <0>";
+ in (h y) + a * xi)"
+ "x = y [+] a [*] x0"
+ "is_vectorspace E" "is_subspace H E" "y:H" "x0 ~: H" "x0:E" "x0 ~= <0>";
have "x : vectorspace_sum H (lin x0)";
by (simp! add: vectorspace_sum_def lin_def, intro bexI exI conjI) force+;
have "EX! xa. ((%(y, a). x = y [+] a [*] x0 & y:H) xa)";
- proof;
+ proof%%;
show "EX xa. ((%(y, a). x = y [+] a [*] x0 & y:H) xa)";
by (force!);
next;
@@ -336,17 +345,13 @@
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!)+);
+ 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!);
- thus "h0 x = h y + a * xi";
- by (simp! add: Let_def);
+ 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;
--- a/src/HOL/Real/HahnBanach/Zorn_Lemma.thy Wed Sep 29 15:35:09 1999 +0200
+++ b/src/HOL/Real/HahnBanach/Zorn_Lemma.thy Wed Sep 29 16:41:52 1999 +0200
@@ -14,19 +14,20 @@
show "ALL c:chain S. EX y:S. ALL z:c. z <= y";
proof;
fix c; assume "c:chain S";
- have s: "EX x. x:c ==> Union c : S";
- by (rule r);
+
show "EX y:S. ALL z:c. z <= y";
- proof (rule case [of "c={}"]);
+ proof (rule case_split [of "c={}"]);
assume "c={}";
- show ?thesis; by (fast!);
+ with aS; show ?thesis; by fast;
next;
- assume "c~={}";
+ assume c: "c~={}";
show ?thesis;
- proof;
- have "EX x. x:c"; by (fast!);
- thus "Union c : S"; by (rule s);
+ proof;
show "ALL z:c. z <= Union c"; by fast;
+ show "Union c : S";
+ proof (rule r);
+ from c; show "EX x. x:c"; by fast;
+ qed;
qed;
qed;
qed;