The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
(by Gertrud Bauer, TU Munich);
--- a/src/HOL/IsaMakefile Thu Sep 09 19:01:37 1999 +0200
+++ b/src/HOL/IsaMakefile Fri Sep 10 17:28:51 1999 +0200
@@ -12,7 +12,7 @@
HOL-Auth HOL-UNITY HOL-Modelcheck HOL-Lambda HOL-W0 HOL-MiniML \
HOL-IOA HOL-AxClasses-Group HOL-AxClasses-Lattice \
HOL-AxClasses-Tutorial HOL-Quot HOL-ex HOL-Isar_examples HOL-Real-ex \
- TLA-Inc TLA-Buffer TLA-Memory
+ HOL-Real-HahnBanach TLA-Inc TLA-Buffer TLA-Memory
all: images test
@@ -94,6 +94,21 @@
@cd Real; $(ISATOOL) usedir $(OUT)/HOL-Real ex
+## HOL-Real-HahnBanach
+
+HOL-Real-HahnBanach: HOL-Real $(LOG)/HOL-Real-HahnBanach.gz
+
+$(LOG)/HOL-Real-HahnBanach.gz: $(OUT)/HOL-Real Real/HahnBanach/Aux.thy \
+ Real/HahnBanach/Bounds.thy Real/HahnBanach/FunctionNorm.thy \
+ Real/HahnBanach/FunctionOrder.thy Real/HahnBanach/HahnBanach.thy \
+ Real/HahnBanach/HahnBanach_h0_lemmas.thy \
+ Real/HahnBanach/HahnBanach_lemmas.thy \
+ Real/HahnBanach/LinearSpace.thy Real/HahnBanach/Linearform.thy \
+ Real/HahnBanach/NormedSpace.thy Real/HahnBanach/ROOT.ML \
+ Real/HahnBanach/Subspace.thy Real/HahnBanach/Zorn_Lemma.thy
+ @cd Real; $(ISATOOL) usedir $(OUT)/HOL-Real HahnBanach
+
+
## HOL-Subst
HOL-Subst: HOL $(LOG)/HOL-Subst.gz
@@ -406,4 +421,5 @@
$(LOG)/HOL-AxClasses-Tutorial.gz $(LOG)/HOL-Quot.gz \
$(LOG)/HOL-ex.gz $(LOG)/HOL-Isar_examples.gz $(OUT)/TLA \
$(LOG)/TLA.gz $(LOG)/TLA-Inc.gz $(LOG)/TLA-Buffer.gz \
- $(LOG)/TLA-Memory.gz $(LOG)/HOL-Real-ex.gz
+ $(LOG)/TLA-Memory.gz $(LOG)/HOL-Real-ex.gz \
+ $(LOG)/HOL-Real-HahnBanach.gz
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Real/HahnBanach/Aux.thy Fri Sep 10 17:28:51 1999 +0200
@@ -0,0 +1,134 @@
+
+theory Aux = Main + Real:;
+
+
+theorem [trans]: "[| (x::'a::order) <= y; x ~= y |] ==> x < y"; (* <= ~= < *)
+ by (asm_simp add: order_less_le);
+
+lemma lt_imp_not_eq: "x < (y::'a::order) ==> x ~= y";
+ by (rule order_less_le[RS iffD1, RS conjunct2]);
+
+lemma Int_singeltonD: "[| A Int B = {v}; x:A; x:B |] ==> x = v";
+ by (fast elim: equalityE);
+
+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"; .;
+ hence "x = - (- y)"; by (rule real_add_minus_eq_minus);
+ also; have "... = y"; by asm_simp;
+ finally; show "x = y"; .;
+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;
+ also; have "... = 1r"; by asm_simp;
+ finally; show ?thesis; by asm_simp;
+qed;
+
+axioms real_mult_le_le_mono2: "[| 0r <= z; x <= y |] ==> x * z <= y * z";
+
+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";
+
+axioms real_mult_diff_distrib: "a * (- x - y) = - a * x - a * y";
+
+axioms real_mult_diff_distrib2: "a * (x - y) = a * x - a * y";
+
+lemma less_imp_le: "(x::real) < y ==> x <= y";
+ by (asm_simp only: real_less_imp_le);
+
+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 (asm_simp add: order_le_less);
+ then; show ?thesis;
+ by asm_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 asm_simp;
+ thus ?thesis; by (rule real_less_imp_le);
+ qed;
+ next;
+ assume "- x = y"; show ?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"]);
+ 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);
+ hence "- x <= r"; by asm_simp;
+ thus "- r <= x"; by (asm_simp add : minus_le [of "x" "r"]);
+ have "x <= rabs x"; by (rule rabs_ge_self);
+ thus "x <= r"; by asm_simp;
+ qed;
+ next;
+ assume "- r <= x & x <= r";
+ 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 "- r <= x" "x <= r";
+ show ?thesis;
+ proof (rule rabs_disj [RS disjE, of x]);
+ assume "rabs x = x";
+ show ?thesis; by asm_simp;
+ next;
+ assume "rabs x = - x";
+ from minus_le [of r x]; show ?thesis; by asm_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;
+qed;
+
+
+end;
\ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Real/HahnBanach/Bounds.thy Fri Sep 10 17:28:51 1999 +0200
@@ -0,0 +1,105 @@
+
+theory Bounds = Main + Real:;
+
+
+section {* The sets of lower and upper bounds *};
+
+constdefs
+ is_LowerBound :: "('a::order) set => 'a set => 'a => bool"
+ "is_LowerBound A B == %x. x:A & (ALL y:B. x <= y)"
+
+ LowerBounds :: "('a::order) set => 'a set => 'a set"
+ "LowerBounds A B == Collect (is_LowerBound A B)"
+
+ is_UpperBound :: "('a::order) set => 'a set => 'a => bool"
+ "is_UpperBound A B == %x. x:A & (ALL y:B. y <= x)"
+
+ UpperBounds :: "('a::order) set => 'a set => 'a set"
+ "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);
+
+translations
+ "UPPER_BOUNDS x:A. P" == "UpperBounds A (Collect (%x. P))"
+ "UPPER_BOUNDS x. P" == "UPPER_BOUNDS x:UNIV. P"
+ "LOWER_BOUNDS x:A. P" == "LowerBounds A (Collect (%x. P))"
+ "LOWER_BOUNDS x. P" == "LOWER_BOUNDS x:UNIV. P";
+
+
+section {* Least and greatest elements *};
+
+constdefs
+ is_Least :: "('a::order) set => 'a => bool"
+ "is_Least B == is_LowerBound B B"
+
+ Least :: "('a::order) set => 'a"
+ "Least B == Eps (is_Least B)"
+
+ is_Greatest :: "('a::order) set => 'a => bool"
+ "is_Greatest B == is_UpperBound B B"
+
+ Greatest :: "('a::order) set => 'a"
+ "Greatest B == Eps (is_Greatest B)";
+
+syntax
+ "_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 *};
+
+constdefs
+ is_Sup :: "('a::order) set => 'a set => 'a => bool"
+ "is_Sup A B x == isLub A B x"
+
+ (* was: x:A & is_Least (UpperBounds A B) x" *)
+
+ Sup :: "('a::order) set => 'a set => 'a"
+ "Sup A B == Eps (is_Sup A B)"
+
+ is_Inf :: "('a::order) set => 'a set => 'a => bool"
+ "is_Inf A B x == x:A & is_Greatest (LowerBounds A B) x"
+
+ Inf :: "('a::order) set => 'a set => 'a"
+ "Inf A B == Eps (is_Inf A B)";
+
+syntax
+ "_SUP" :: "[pttrn, 'a set, 'a => bool] => 'a set" ("(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))"
+ "SUP x. P" == "SUP x:UNIV. P"
+ "INF x:A. P" == "Inf A (Collect (%x. P))"
+ "INF x. P" == "INF x:UNIV. P";
+
+
+lemma [intro]: "[| x:A; !!y. y:B ==> y <= x |] ==> x: UpperBounds A B";
+ by (unfold UpperBounds_def is_UpperBound_def) force;
+
+lemma ub_ge_sup: "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";
+ by (unfold is_Sup_def, rule isLubD2);
+
+lemma sup_ub1: "ALL y:B. a <= y ==> is_Sup A B s ==> x:B ==> a <= s";
+proof -;
+ assume "ALL y:B. a <= y" "is_Sup A B s" "x:B";
+ have "a <= x"; by (rule bspec);
+ also; have "x <= s"; by (rule sup_ub);
+ finally; show "a <= s"; .;
+qed;
+
+
+end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Real/HahnBanach/FunctionNorm.thy Fri Sep 10 17:28:51 1999 +0200
@@ -0,0 +1,222 @@
+
+theory FunctionNorm = NormedSpace + FunctionOrder:;
+
+
+theorems [elim!!] = bspec;
+
+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))";
+
+lemma lipschitz_continous_I:
+ "[| is_linearform V f; !! x. x:V ==> rabs (f x) <= c * norm x |]
+ ==> is_continous V norm f";
+proof (unfold is_continous_def, intro exI conjI ballI);
+ assume r: "!! x. x:V ==> rabs (f x) <= c * norm x";
+ fix x; assume "x:V"; show "rabs (f x) <= c * norm x"; by (rule r);
+qed;
+
+lemma continous_linearform: "is_continous V norm f ==> is_linearform V f";
+ by (unfold is_continous_def) force;
+
+lemma continous_bounded: "is_continous V norm f ==> EX c. ALL x:V. rabs (f x) <= c * norm x";
+ by (unfold is_continous_def) force;
+
+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)))}";
+
+constdefs
+ function_norm :: " ['a set, 'a => real, 'a => real] => real"
+ "function_norm V norm f ==
+ Sup UNIV (B V norm f)";
+
+constdefs
+ is_function_norm :: " ['a set, 'a => real, 'a => real] => real => bool"
+ "is_function_norm V norm f fn ==
+ is_Sup UNIV (B V norm f) fn";
+
+lemma B_not_empty: "0r : B V norm f";
+ by (unfold B_def, force);
+
+lemma le_max1: "x <= max x (y::'a::linorder)";
+ by (simp add: le_max_iff_disj[of x x y]);
+
+lemma le_max2: "y <= max x (y::'a::linorder)";
+ by (simp add: le_max_iff_disj[of y x y]);
+
+lemma ex_fnorm:
+ "[| 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);
+ assume "is_normed_vectorspace V norm";
+ 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";
+ proof (intro exI);
+ show "0r : (B V norm f)"; by (unfold B_def, force);
+ qed;
+
+ from e; show "EX Y. isUb UNIV (B V norm f) Y";
+ proof;
+ fix c; assume a: "ALL x:V. rabs (f x) <= c * norm x";
+ def b == "max c 0r";
+
+ show "EX Y. isUb UNIV (B V norm f) Y";
+ proof (intro exI isUbI setleI ballI, unfold B_def,
+ elim CollectD [elimify] disjE bexE conjE);
+ fix x y; assume "x:V" "x ~= <0>" "y = rabs (f x) * rinv (norm x)";
+ from a; have le: "rabs (f x) <= c * norm x"; ..;
+ have "y = rabs (f x) * rinv (norm x)";.;
+ also; from _ le; have "... <= c * norm x * rinv (norm x)";
+ proof (rule real_mult_le_le_mono2);
+ show "0r <= rinv (norm x)";
+ by (rule 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";
+ proof (rule real_mult_inv_right);
+ show "norm x ~= 0r";
+ by (rule not_sym, rule lt_imp_not_eq, rule normed_vs_norm_gt_zero);
+ qed;
+ also; have "c * ... = c"; by asm_simp;
+ also; have "... <= b"; by (asm_simp add: le_max1);
+ finally; show "y <= b"; .;
+ next;
+ fix y; assume "y = 0r"; show "y <= b"; by (asm_simp add: le_max2);
+ qed simp;
+ qed;
+ qed;
+qed;
+
+lemma fnorm_ge_zero: "[| is_continous V norm f; is_normed_vectorspace V norm|]
+ ==> 0r <= function_norm V norm f";
+proof -;
+ assume c: "is_continous V norm f" and n: "is_normed_vectorspace V norm";
+ have "is_function_norm V norm f (function_norm V norm f)"; by (rule ex_fnorm);
+ hence s: "is_Sup UNIV (B V norm f) (function_norm V norm f)";
+ by (simp add: is_function_norm_def);
+ show ?thesis;
+ proof (unfold function_norm_def, rule sup_ub1);
+ show "ALL x:(B V norm f). 0r <= x";
+ proof (intro ballI, unfold B_def, elim CollectD [elimify] bexE conjE disjE);
+ fix x r; assume "is_normed_vectorspace V norm" "x : V" "x ~= <0>"
+ "r = rabs (f x) * rinv (norm x)";
+ show "0r <= r";
+ proof (asm_simp, rule real_le_mult_order);
+ show "0r <= rabs (f x)"; by (asm_simp only: rabs_ge_zero);
+ show "0r <= rinv (norm x)";
+ proof (rule less_imp_le);
+ show "0r < rinv (norm x)";
+ by (rule real_rinv_gt_zero, rule normed_vs_norm_gt_zero [of V norm]);
+ qed;
+ qed;
+ qed asm_simp;
+ from ex_fnorm [OF n c]; show "is_Sup UNIV (B V norm f) (Sup UNIV (B V norm f))";
+ by (asm_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";
+proof -;
+ assume "is_normed_vectorspace V norm" "x:V" and c: "is_continous V norm f";
+ have v: "is_vectorspace V"; by (rule normed_vs_vs);
+ assume "x:V";
+ show "?thesis";
+ proof (rule case [of "x = <0>"]);
+ assume "x ~= <0>";
+ show "?thesis";
+ proof -;
+ have n: "0r <= norm x"; by (rule normed_vs_norm_ge_zero);
+ have le: "rabs (f x) * rinv (norm x) <= function_norm V norm f";
+ proof (unfold function_norm_def, rule sup_ub);
+ from ex_fnorm [OF _ c]; show "is_Sup UNIV (B V norm f) (Sup UNIV (B V norm f))";
+ by (asm_simp add: is_function_norm_def function_norm_def);
+ show "rabs (f x) * rinv (norm x) : B V norm f";
+ by (unfold B_def, intro CollectI disjI2 bexI [of _ x] conjI, simp);
+ qed;
+ have "rabs (f x) = rabs (f x) * 1r"; by asm_simp;
+ also; have "1r = rinv (norm x) * norm x";
+ by (rule real_mult_inv_left [RS sym], rule lt_imp_not_eq[RS not_sym],
+ rule normed_vs_norm_gt_zero[of V norm]);
+ also; have "rabs (f x) * ... = rabs (f x) * rinv (norm x) * norm x";
+ by (asm_simp add: real_mult_assoc [of "rabs (f x)"]);
+ also; have "rabs (f x) * rinv (norm x) * norm x <= function_norm V norm f * norm x";
+ by (rule real_mult_le_le_mono2 [OF n le]);
+ finally; show "rabs (f x) <= function_norm V norm f * norm x"; .;
+ qed;
+ next;
+ assume "x = <0>";
+ then; show "?thesis";
+ proof -;
+ have "rabs (f x) = rabs (f <0>)"; by asm_simp;
+ also; have "f <0> = 0r"; by (rule linearform_zero [OF v continous_linearform]);
+ also; note rabs_zero;
+ also; have" 0r <= function_norm V norm f * norm x";
+ proof (rule real_le_mult_order);
+ show "0r <= function_norm V norm f"; by (rule fnorm_ge_zero);
+ show "0r <= norm x"; by (rule normed_vs_norm_ge_zero);
+ qed;
+ finally; show "rabs (f x) <= function_norm V norm f * norm x"; .;
+ qed;
+ 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 |]
+ ==> function_norm V norm f <= c";
+proof (unfold function_norm_def);
+ assume "is_normed_vectorspace V norm";
+ assume c: "is_continous V norm f";
+ assume 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);
+ from ex_fnorm [OF _ c]; show "is_Sup UNIV (B V norm f) (Sup UNIV (B V norm f))";
+ by (asm_simp add: is_function_norm_def function_norm_def);
+ show "isUb UNIV (B V norm f) c";
+ proof (intro isUbI setleI ballI);
+ fix y; assume "y: B V norm f";
+ show le: "y <= c";
+ proof (unfold B_def, elim CollectD [elimify] disjE bexE);
+ fix x; assume Px: "x ~= <0> & y = rabs (f x) * rinv (norm x)";
+ assume x: "x : V";
+ have lt: "0r < norm x";
+ by (asm_simp add: normed_vs_norm_gt_zero);
+ hence "0r ~= norm x"; by (asm_simp add: order_less_imp_not_eq);
+ hence neq: "norm x ~= 0r"; by (rule not_sym);
+
+ from lt; have "0r < rinv (norm x)";
+ by (asm_simp add: real_rinv_gt_zero);
+ then; have inv_leq: "0r <= rinv (norm x)"; by (rule less_imp_le);
+
+ from Px; have "y = rabs (f x) * rinv (norm x)"; ..;
+ also; from inv_leq; have "... <= c * norm x * rinv (norm x)";
+ proof (rule real_mult_le_le_mono2);
+ from fb x; show "rabs (f x) <= c * norm x"; ..;
+ qed;
+ also; have "... <= c";
+ by (simp add: neq real_mult_assoc);
+ finally; show ?thesis; .;
+ next;
+ assume "y = 0r";
+ show "y <= c"; by force;
+ qed;
+ qed force;
+ qed;
+qed;
+
+
+end;
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Real/HahnBanach/FunctionOrder.thy Fri Sep 10 17:28:51 1999 +0200
@@ -0,0 +1,95 @@
+
+theory FunctionOrder = Subspace + Linearform:;
+
+
+section {* Order on functions *};
+
+types 'a graph = "('a * real) set";
+
+constdefs
+ graph :: "['a set, 'a => real] => 'a graph "
+ "graph F f == {p. EX x. p = (x, f x) & x:F}"; (* == {(x, f x). x:F} *)
+
+constdefs
+ domain :: "'a graph => 'a set"
+ "domain g == {x. EX y. (x, y):g}";
+
+constdefs
+ funct :: "'a graph => ('a => real)"
+ "funct g == %x. (@ y. (x, y):g)";
+
+lemma graph_I: "x:F ==> (x, f x) : graph F f";
+ by (unfold graph_def, intro CollectI exI) force;
+
+lemma graphD1: "(x, y): graph F f ==> x:F";
+ by (unfold graph_def, elim CollectD [elimify] exE) force;
+
+lemma graph_domain_funct: "(!!x y z. (x, y):g ==> (x, z):g ==> z = y) ==> graph (domain g) (funct g) = g";
+proof ( unfold domain_def, unfold funct_def, unfold graph_def, auto);
+ fix a b; assume "(a, b) : g";
+ show "(a, SOME y. (a, y) : g) : g"; by (rule selectI2);
+ show "EX y. (a, y) : g"; ..;
+ assume uniq: "!!x y z. (x, y):g ==> (x, z):g ==> z = y";
+ show "b = (SOME y. (a, y) : g)";
+ proof (rule select_equality [RS sym]);
+ fix y; assume "(a, y):g"; show "y = b"; by (rule uniq);
+ qed;
+qed;
+
+lemma graph_lemma1: "x:F ==> EX t: (graph F f). t = (x, f x)";
+ by (unfold graph_def, force);
+
+lemma graph_lemma2: "(x, y): graph H h ==> y = h x";
+ by (unfold graph_def, elim CollectD [elimify] exE) force;
+
+lemma graph_lemma3: "[| graph H h <= graph H' h'; x:H |] ==> h x = h' x";
+ by (unfold graph_def, force);
+
+lemma graph_lemma4: "[| graph H h <= graph H' h' |] ==> H <= H'";
+ by (unfold graph_def, force);
+
+lemma graph_lemma5: "[| !! x. x: H ==> h x = h' x; H <= H'|] ==> graph H h <= graph H' h'";
+ by (unfold graph_def, force);
+
+
+constdefs
+ norm_prev_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
+ & 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
+ & 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;
+
+lemma norm_prev_extension_I2 [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;
+
+lemma norm_prev_extension_I [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;
+
+
+end;
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Real/HahnBanach/HahnBanach.thy Fri Sep 10 17:28:51 1999 +0200
@@ -0,0 +1,434 @@
+
+theory HahnBanach = HahnBanach_lemmas + HahnBanach_h0_lemmas:;
+
+
+theorems [elim!!] = psubsetI;
+
+
+theorem hahnbanach:
+ "[| is_vectorspace E; is_subspace F E; is_quasinorm E p; is_linearform F f;
+ ALL x:F. f x <= p x |]
+ ==> EX h. is_linearform E h
+ & (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"
+ and "ALL x:F. f x <= p x";
+ def M_def: M == "norm_prev_extensions E p F f";
+
+ have aM: "graph F f : norm_prev_extensions E p F f";
+ proof (rule norm_prev_extension_I2);
+ show "is_subspace F F"; by (rule subspace_refl, rule subspace_vs);
+ qed blast+;
+
+
+ sect {* Part I a of the proof of the Hahn-Banach Theorem,
+ H. Heuser, Funktionalanalysis, p.231 *};
+
+
+ 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_extension_I);
+ 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;
+ 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 "EX x. x : c" "(x, y) : Union c" "(x, z) : Union c";
+ show "z = y"; by (rule sup_uniq);
+ qed;
+
+ show "is_linearform ?H ?h";
+ by (asm_simp add: sup_lf a);
+
+ show "is_subspace ?H E";
+ by (rule sup_subE, rule a) asm_simp+;
+
+ show "is_subspace F ?H";
+ by (rule sup_supF, rule a) asm_simp+;
+
+ show "graph F f <= graph ?H ?h";
+ by (rule sup_ext, rule a) asm_simp+;
+
+ show "ALL x::'a:?H. ?h x <= p x";
+ by (rule sup_norm_prev, rule a) asm_simp+;
+ qed;
+ qed;
+ qed;
+ qed;
+ qed;
+
+
+ with aM; have bex_g: "EX g:M. ALL x:M. g <= x --> g = x";
+ by (asm_simp add: Zorn's_Lemma);
+ thus ?thesis;
+ proof;
+ fix g; assume g: "g:M" "ALL x:M. g <= x --> g = x";
+
+ have ex_Hh: "EX H h. graph H h = g
+ & is_linearform H h
+ & is_subspace H E
+ & is_subspace F H
+ & (graph F f <= graph H h)
+ & (ALL x:H. h x <= p x) ";
+ by (asm_simp add: norm_prev_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";
+ show ?thesis;
+ proof;
+ have h: "is_vectorspace H"; by (rule subspace_vs);
+ have f: "is_vectorspace F"; by (rule subspace_vs);
+
+
+ sect {* Part I a of the proof of the Hahn-Banach Theorem,
+ H. Heuser, Funktionalanalysis, p.230 *};
+
+ have eq: "H = E";
+ proof (rule classical);
+ assume "H ~= E";
+ show ?thesis;
+ proof -;
+ have "EX x:M. g <= x & g ~= x";
+ proof -;
+ have "EX H0 h0. g <= graph H0 h0 & g ~= graph H0 h0 & graph H0 h0 : M";
+ proof-;
+ from subspace_subset [of H E]; have "H <= E"; ..;
+ hence "H < E"; ..;
+ hence "EX x0:E. x0~:H"; by (rule set_less_imp_diff_not_empty);
+ thus ?thesis;
+ proof;
+ fix x0; assume "x0:E" "x0~:H";
+ have x0: "x0 ~= <0>";
+ proof (rule classical);
+ presume "x0 = <0>";
+ have "x0 : H"; by (asm_simp add: zero_in_vs [OF h]);
+ thus "x0 ~= <0>"; by contradiction;
+ qed force;
+
+ def H0_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 -;
+ 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 asm_simp;
+ also; have "... <= c + a + (- d - a)";
+ by (rule real_add_le_mono1);
+ also; have "... = c - d"; by asm_simp;
+ finally; show "- a - b <= c - d"; .;
+ qed;
+ 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 asm_simp;
+ with h_bound; show ?thesis; ..;
+ qed;
+ also; have "v [-] u = x0 [+] [-] x0 [+] v [+] [-] u";
+ by (asm_simp add: vs_add_minus_eq_diff);
+ also; have "... = v [+] x0 [+] [-] (u [+] x0)";
+ by asm_simp;
+ also; have "... = (v [+] x0) [-] (u [+] x0)";
+ by (asm_simp only: vs_add_minus_eq_diff);
+ also; have "p ... <= p (v [+] x0) + p (u [+] x0)";
+ by (rule quasinorm_diff_triangle_ineq) asm_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_def: h0 == "%x. let (y, a) = @ (y, a). (x = y [+] a [*] x0 & y:H )
+ in (h y) + a * xi";
+
+ have "graph H h <= graph H0 h0";
+ proof% (rule graph_lemma5);
+ fix t; assume "t:H";
+ show "h t = h0 t";
+ proof -;
+ have "(@ (y, a). t = y [+] a [*] x0 & y : H) = (t, 0r)";
+ by (rule lemma1, rule x0);
+ thus ?thesis; by (asm_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 asm_simp;
+
+ 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 graph_I);
+ show "x0:H0";
+ proof (unfold H0_def, rule vs_sum_I);
+ from h; show "<0> : H"; by (rule zero_in_vs);
+ show "x0 : lin x0"; by (rule x_lin_x);
+ show "x0 = <0> [+] x0"; by (rule vs_add_zero_left [RS sym]);
+ qed;
+ qed;
+ have "(x0, h0 x0) ~: graph H h";
+ proof;
+ assume "(x0, h0 x0) : graph H h";
+ have "x0:H"; by (rule graphD1);
+ thus "False"; by contradiction;
+ qed;
+ hence "(x0, h0 x0) ~: graph H0 h0"; by asm_simp;
+ with x1; show "False"; by contradiction;
+ qed;
+ thus "g ~= graph H0 h0"; by asm_simp;
+
+ have "graph H0 h0 : norm_prev_extensions E p F f";
+ proof (rule norm_prev_extension_I2);
+
+ show "is_linearform H0 h0";
+ by (rule h0_lf, rule x0) asm_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 asm_simp;
+ qed;
+
+ 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 asm_simp;
+ qed;
+
+ show "graph F f <= graph H0 h0";
+ proof(rule graph_lemma5);
+ fix x; assume "x:F";
+ show "f x = h0 x";
+ proof -;
+ have "x:H";
+ proof (rule subsetD);
+ show "F <= H"; by (rule subspace_subset);
+ qed;
+ have eq: "(@ (y, a). x = y [+] a [*] x0 & y : H) = (x, 0r)";
+ by (rule lemma1, rule x0) asm_simp+;
+
+ have "h0 x = (let (y,a) = @ (y,a). x = y [+] a [*] x0 & y : H
+ in h y + a * xi)";
+ by asm_simp;
+ also; from eq; have "... = (let (y,a) = (x, 0r) in h y + a * xi)";
+ by simp;
+ also; have " ... = h x + 0r * xi";
+ by (asm_simp add: Let_def);
+ also; have "... = h x"; by asm_simp;
+ also; have "... = f x"; by (rule graph_lemma3 [RS sym, of F f H h]);
+ finally; show ?thesis; by (rule sym);
+ qed;
+ next;
+ from f_h0; show "F <= H0"; by (rule subspace_subset);
+ qed;
+
+ show "ALL x:H0. h0 x <= p x";
+ by (rule h0_norm_prev, rule x0) (assumption | asm_simp)+;
+ qed;
+ thus "graph H0 h0 : M"; by asm_simp;
+ qed;
+ qed;
+ thus ?thesis; ..;
+ 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 asm_simp;
+ show "ALL x:F. h x = f x"; by (intro ballI, rule graph_lemma3 [RS sym]);
+ from eq; show "ALL x:E. h x <= p x"; by force;
+ qed;
+ qed;
+ qed;
+ qed;
+qed;
+
+
+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)";
+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";
+ have "ALL x:F. f x <= p x";
+ by (asm_simp only: rabs_ineq);
+ hence "EX g. is_linearform E g & (ALL x:F. g x = f x) & (ALL x:E. g x <= p x)";
+ by (asm_simp only: hahnbanach);
+ thus ?thesis;
+ proof (elim exE conjE);
+ fix g; assume "is_linearform E g" "ALL x:F. g x = f x" "ALL x:E. g x <= p x";
+ show ?thesis;
+ proof (intro exI conjI)+;
+ from e; show "ALL x:E. rabs (g x) <= p x";
+ by (asm_simp add: rabs_ineq [OF subspace_refl]);
+ qed;
+ qed;
+qed;
+
+
+theorem norm_hahnbanach:
+ "[| is_normed_vectorspace E norm; is_subspace F E; is_linearform F f;
+ is_continous F norm f |]
+ ==> EX g. is_linearform E g
+ & is_continous E norm g
+ & (ALL x:F. g x = f x)
+ & function_norm E norm g = function_norm F norm f"
+ (concl is "EX g::'a=>real. ?P g");
+
+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";
+ hence e: "is_vectorspace E"; by (asm_simp add: normed_vs_vs);
+ from _ e;
+ have f: "is_normed_vectorspace F norm"; by (rule subspace_normed_vs);
+ def p_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)";
+
+ have q: "is_quasinorm E p";
+ proof;
+ fix x y a; assume "x:E" "y:E";
+
+ show "0r <= p x";
+ proof (unfold p_def, rule real_le_mult_order);
+ from c f; show "0r <= function_norm F norm f";
+ by (rule fnorm_ge_zero);
+ from a; show "0r <= norm x"; by (rule normed_vs_norm_ge_zero);
+ qed;
+
+ show "p (a [*] x) = (rabs a) * (p x)";
+ proof -;
+ have "p (a [*] x) = (function_norm F norm f) * norm (a [*] x)"; by asm_simp;
+ also; from a; 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 (asm_simp only: real_mult_left_commute);
+ also; have "... = (rabs a) * (p x)"; by asm_simp;
+ finally; show ?thesis; .;
+ qed;
+
+ show "p (x [+] y) <= p x + p y";
+ proof -;
+ have "p (x [+] y) = (function_norm F norm f) * norm (x [+] y)"; by asm_simp;
+ also; have "... <= (function_norm F norm f) * (norm x + norm y)";
+ proof (rule real_mult_le_le_mono1);
+ from c f; show "0r <= function_norm F norm f"; by (rule fnorm_ge_zero);
+ show "norm (x [+] y) <= norm x + norm y"; by (rule normed_vs_norm_triangle_ineq);
+ qed;
+ also; have "... = (function_norm F norm f) * (norm x) + (function_norm F norm f) * (norm y)";
+ by (asm_simp only: real_add_mult_distrib2);
+ finally; show ?thesis; by asm_simp;
+ qed;
+ qed;
+
+ have "ALL x:F. rabs (f x) <= p x";
+ proof;
+ fix x; assume "x:F";
+ from f; show "rabs (f x) <= p x"; by (asm_simp add: norm_fx_le_norm_f_norm_x);
+ qed;
+
+ with e b q; have "EX g. ?P' g";
+ by (asm_simp add: rabs_hahnbanach);
+
+ 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";
+ show ce: "is_continous E norm g";
+ proof (rule lipschitz_continous_I);
+ fix x; assume "x:E";
+ show "rabs (g x) <= function_norm F norm f * norm x";
+ by (rule bspec [of _ _ x], asm_simp);
+ qed;
+ show "function_norm E norm g = function_norm F norm f";
+ proof (rule order_antisym);
+ from _ ce; show "function_norm E norm g <= function_norm F norm f";
+ proof (rule fnorm_le_ub);
+ show "ALL x:E. rabs (g x) <= function_norm F norm f * norm x";
+ proof;
+ fix x; assume "x:E";
+ show "rabs (g x) <= function_norm F norm f * norm x";
+ by (rule bspec [of _ _ x], asm_simp);
+ qed;
+ from c f; show "0r <= function_norm F norm f"; by (rule fnorm_ge_zero);
+ qed;
+ show "function_norm F norm f <= function_norm E norm g";
+ proof (rule fnorm_le_ub);
+ show "ALL x:F. rabs (f x) <= function_norm E norm g * norm x";
+ proof;
+ fix x; assume "x:F";
+ from a; have "f x = g x"; by (rule bspec [of _ _ x, RS sym]);
+ hence "rabs (f x) = rabs (g x)"; by simp;
+ also; from _ _ ce; have "... <= function_norm E norm g * norm x";
+ proof (rule norm_fx_le_norm_f_norm_x);
+ show "x:E";
+ proof (rule subsetD);
+ show "F<=E"; by (rule subspace_subset);
+ qed;
+ qed;
+ finally; show "rabs (f x) <= function_norm E norm g * norm x"; .;
+ qed;
+ from _ e; show "is_normed_vectorspace F norm"; by (rule subspace_normed_vs);
+ from ce; show "0r <= function_norm E norm g"; by (rule fnorm_ge_zero);
+ qed;
+ qed;
+ qed;
+qed;
+
+
+end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Real/HahnBanach/HahnBanach_h0_lemmas.thy Fri Sep 10 17:28:51 1999 +0200
@@ -0,0 +1,358 @@
+
+theory HahnBanach_h0_lemmas = FunctionOrder + NormedSpace + Zorn_Lemma + FunctionNorm + RComplete:;
+
+
+theorems [intro!!] = zero_in_vs 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 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;
+ 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}";
+ show "y <= b <0>";
+ proof -;
+ have "EX u:F. y = a u"; by fast;
+ thus ?thesis;
+ proof;
+ fix u; assume "u:F";
+ assume "y = a u";
+ also; have "a u <= b <0>";
+ proof (rule r);
+ show "<0> : F"; ..;
+ qed;
+ finally; show ?thesis;.;
+ qed;
+ qed;
+ qed;
+ qed;
+ qed;
+ thus "EX xi. (ALL y:F. a y <= xi) & (ALL y:F. xi <= b y)";
+ proof (elim exE);
+ fix t; assume "isLub UNIV {s::real . EX u:F. s = a u} t";
+ show ?thesis;
+ proof (intro exI conjI ballI);
+ fix y; assume "y:F";
+ show "a y <= t";
+ proof (rule isUbD);
+ show"isUb UNIV {s. EX u:F. s = a u} t"; ..;
+ qed fast;
+ next;
+ fix y; assume "y:F";
+ show "t <= b y";
+ proof (intro isLub_le_isUb isUbI setleI);
+ show "ALL ya : {s. EX u:F. s = a u}. ya <= b y";
+ proof (intro ballI);
+ fix au;
+ assume "au : {s. EX u:F. s = a u} ";
+ show "au <= b y";
+ proof -;
+ have "EX u:F. au = a u"; by fast;
+ thus "au <= b y";
+ proof;
+ fix u; assume "u:F";
+ assume "au = a u";
+ also; have "... <= b y"; by (rule r);
+ finally; show ?thesis; .;
+ qed;
+ qed;
+ qed;
+ show "b y : UNIV"; by fast;
+ qed;
+ qed;
+ qed;
+qed;
+
+
+theorems [dest!!] = vs_sumD linD;
+
+lemma h0_lf:
+ "[| h0 = (%x. let (y, a) = @ (y, a). (x = y [+] a [*] x0 & y:H) in (h y) + a * xi);
+ H0 = vectorspace_sum H (lin x0); is_subspace H E; is_linearform H h; x0 ~: H;
+ x0 : E; x0 ~= <0>; is_vectorspace E |]
+ ==> is_linearform H0 h0";
+proof -;
+ assume h0_def: "h0 = (%x. let (y, a) = @ (y, a). (x = y [+] a [*] x0 & y:H) in (h y) + a * xi)"
+ and H0_def: "H0 = vectorspace_sum H (lin x0)"
+ and [simp]: "is_subspace H E" "is_linearform H h" "x0 ~: H" "x0 ~= <0>"
+ and [simp]: "x0 : E" "is_vectorspace E";
+
+ have h0: "is_vectorspace H0";
+ proof (asm_simp, rule vs_sum_vs);
+ show "is_subspace (lin x0) E"; by (rule lin_subspace);
+ qed simp+;
+
+ show ?thesis;
+ proof;
+ fix x1 x2; assume "x1 : H0" "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 (asm_simp add: vectorspace_sum_def lin_def) blast;
+ have ex_x2: "? y2 a2. (x2 = y2 [+] a2 [*] x0 & y2 : H)";
+ by (asm_simp add: vectorspace_sum_def lin_def) blast;
+ from x1x2; have ex_x1x2: "? y a. (x1 [+] x2 = y [+] a [*] x0 & y : H)";
+ by (asm_simp add: 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";
+
+ have ya: "y1 [+] y2 = y & a1 + a2 = a";
+ proof (rule lemma4);
+ show "y1 [+] y2 [+] (a1 + a2) [*] x0 = y [+] a [*] x0";
+ proof -;
+ have "y [+] a [*] x0 = x1 [+] x2"; by asm_simp;
+ also; have "... = y1 [+] a1 [*] x0 [+] (y2 [+] a2 [*] x0)"; by asm_simp;
+ also; have "... = y1 [+] y2 [+] (a1 [*] x0 [+] a2 [*] x0)";
+ by asm_simp_tac;
+ also; have "... = y1 [+] y2 [+] (a1 + a2) [*] x0";
+ by (asm_simp add: vs_add_mult_distrib2[of E]);
+ finally; show ?thesis; by (rule sym);
+ qed;
+ show "y1 [+] y2 : H"; by (rule subspace_add_closed);
+ qed;
+ have y: "y1 [+] y2 = y"; by (rule conjunct1 [OF ya]);
+ have a: "a1 + a2 = a"; by (rule conjunct2 [OF ya]);
+
+ have "h0 (x1 [+] x2) = h y + a * xi";
+ by (rule lemma3);
+ also; have "... = h (y1 [+] y2) + (a1 + a2) * xi"; by (asm_simp add: y a);
+ also; have "... = h y1 + h y2 + a1 * xi + a2 * xi";
+ by (asm_simp add: linearform_add_linear [of H] real_add_mult_distrib);
+ also; have "... = (h y1 + a1 * xi) + (h y2 + a2 * xi)"; by asm_simp;
+ also; have "... = h0 x1 + h0 x2";
+ proof -;
+ have x1: "h0 x1 = h y1 + a1 * xi"; by (rule lemma3);
+ have x2: "h0 x2 = h y2 + a2 * xi"; by (rule lemma3);
+ from x1 x2; show ?thesis; by asm_simp;
+ qed;
+ finally; show ?thesis; .;
+ qed;
+
+ next;
+ fix c x1; assume "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 (asm_simp add: vectorspace_sum_def lin_def, fast);
+ have ex_x: "!! x. x: H0 ==> ? y a. (x = y [+] a [*] x0 & y : H)";
+ by (asm_simp add: 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";
+
+ have ya: "c [*] y1 = y & c * a1 = a";
+ proof (rule lemma4);
+ show "c [*] y1 [+] (c * a1) [*] x0 = y [+] a [*] x0";
+ proof -;
+ have "y [+] a [*] x0 = c [*] x1"; by asm_simp;
+ also; have "... = c [*] (y1 [+] a1 [*] x0)"; by asm_simp;
+ also; have "... = c [*] y1 [+] c [*] (a1 [*] x0)";
+ by (asm_simp_tac add: vs_add_mult_distrib1);
+ also; have "... = c [*] y1 [+] (c * a1) [*] x0";
+ by (asm_simp_tac);
+ finally; show ?thesis; by (rule sym);
+ qed;
+ show "c [*] y1: H"; by (rule subspace_mult_closed);
+ qed;
+ have y: "c [*] y1 = y"; by (rule conjunct1 [OF ya]);
+ have a: "c * a1 = a"; by (rule conjunct2 [OF ya]);
+
+ have "h0 (c [*] x1) = h y + a * xi";
+ by (rule lemma3);
+ also; have "... = h (c [*] y1) + (c * a1) * xi";
+ by (asm_simp add: y a);
+ also; have "... = c * h y1 + c * a1 * xi";
+ by (asm_simp add: linearform_mult_linear [of H] real_add_mult_distrib);
+ also; have "... = c * (h y1 + a1 * xi)";
+ by (asm_simp add: real_add_mult_distrib2 real_mult_assoc);
+ also; have "... = c * (h0 x1)";
+ proof -;
+ have "h0 x1 = h y1 + a1 * xi"; by (rule lemma3);
+ thus ?thesis; by asm_simp;
+ qed;
+ finally; show ?thesis; .;
+ qed;
+ qed;
+qed;
+
+
+lemma h0_norm_prev:
+ "[| 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";
+ 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 (asm_simp add: 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";
+ show ?thesis;
+ proof -;
+ have "h0 x = h y + a * xi";
+ by (rule lemma3);
+ 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;
+ show ?thesis;
+ proof -;
+ from a1; have "- p (rinv a [*] y [+] x0) - h (rinv a [*] y) <= xi";
+ proof (rule bspec);
+ show "(rinv a) [*] y : H"; by (rule subspace_mult_closed);
+ qed;
+ 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; have "... = p (a [*] (rinv a [*] y [+] x0)) - a * (h (rinv a [*] y))";
+ by (asm_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) asm_simp+;
+ also; have "... = (a * rinv a) [*] y [+] a [*] x0";
+ by asm_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 asm_simp;
+ also; from nz; have "... = p (y [+] a [*] x0) - (h y)";
+ proof asm_simp;
+ have "a * (h (rinv a [*] y)) = h (a [*] (rinv a [*] y))";
+ by (asm_simp_tac add: linearform_mult_linear [RS sym]);
+ also; have "... = h y";
+ proof -;
+ from nz; have "a [*] (rinv a [*] y) = y"; by asm_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;
+ 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 *)
+ thus ?thesis;
+ by force;
+ qed;
+
+ next;
+ assume "a = 0r"; show ?thesis;
+ proof -;
+ have "h y + a * xi = h y"; by asm_simp;
+ also; from a; have "... <= p y"; ..;
+ also; have "... = p (y [+] a [*] x0)";
+ proof -;
+ have "y = y [+] <0>"; by asm_simp;
+ also; have "... = y [+] a [*] x0";
+ proof -;
+ have "<0> = 0r [*] x0";
+ by asm_simp;
+ also; have "... = a [*] x0"; by asm_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;
+
+ 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"; by (rule subspace_mult_closed);
+ qed;
+ 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; have "... = p (a [*] (rinv a [*] y [+] x0)) - a * (h (rinv a [*] y))";
+ by (asm_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) asm_simp+;
+ also; have "... = (a * rinv a) [*] y [+] a [*] x0";
+ by asm_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 asm_simp;
+ also; from nz; have "... = p (y [+] a [*] x0) - (h y)";
+ proof asm_simp;
+ have "a * (h (rinv a [*] y)) = h (a [*] (rinv a [*] y))";
+ by (rule linearform_mult_linear [RS sym]) asm_simp+;
+ also; have "... = h y";
+ proof -;
+ from nz; have "a [*] (rinv a [*] y) = y"; by asm_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;
+ 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 *)
+ thus ?thesis;
+ by force;
+ qed;
+ qed;
+ also; have "... = p x"; by asm_simp;
+ finally; show ?thesis; .;
+ qed;
+ qed;
+ qed;
+qed blast+;
+
+
+end;
\ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Real/HahnBanach/HahnBanach_lemmas.thy Fri Sep 10 17:28:51 1999 +0200
@@ -0,0 +1,474 @@
+
+theory HahnBanach_lemmas = FunctionOrder + NormedSpace + Zorn_Lemma + FunctionNorm + RComplete:;
+
+
+theorems [dest!!] = subsetD;
+theorems [intro!!] = subspace_subset;
+
+lemma rabs_ineq: "[| is_subspace H E; is_vectorspace E; is_quasinorm E p; is_linearform H h |] \
+ \ ==> (ALL x:H. rabs (h x) <= p x) = ( ALL x:H. h x <= p x)" (concl is "?L = ?R");
+proof -;
+ assume "is_subspace H E" "is_vectorspace E" "is_quasinorm E p" "is_linearform H h";
+ have H: "is_vectorspace H"; by (rule subspace_vs);
+ show ?thesis;
+ proof;
+ assume l: ?L;
+ then; show ?R;
+ proof (intro ballI);
+ fix x; assume "x:H";
+ have "h x <= rabs (h x)"; by (rule rabs_ge_self);
+ also; have "rabs (h x) <= p x"; by fast;
+ finally; show "h x <= p x"; .;
+ qed;
+ next;
+ assume r: ?R;
+ 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 (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 asm_simp;
+ with r; show ?thesis; ..;
+ qed;
+ also; have "... = p x";
+ proof (rule quasinorm_minus);
+ show "x:E";
+ proof (rule subsetD);
+ show "H <= E"; ..;
+ qed;
+ qed;
+ finally; show "- h x <= p x"; .;
+ qed;
+ from r; show "h x <= p x"; ..;
+ qed;
+ qed;
+ qed;
+qed;
+
+
+lemma some_H'h't:
+ "[| M = norm_prev_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";
+
+ let ?P = "%H h. is_linearform H h
+ & is_subspace H E
+ & is_subspace F H
+ & (graph F f <= graph H h)
+ & (ALL x:H. h x <= p x)";
+
+ have "EX t : (graph H h). t = (x, h x)";
+ by (rule graph_lemma1);
+ 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 (asm_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 asm_simp;
+ qed;
+ thus ?thesis; by (elim exE conjE, intro exI conjI) (asm_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|]
+ ==> 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);
+
+ 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 (asm_simp, rule graphD1);
+ show "graph H' h' <= graph H h";
+ by (asm_simp only: chain_ball_Union_upper);
+ qed;
+qed;
+
+
+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|]
+ ==> 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";
+
+ let ?P = "%H h. is_linearform H h
+ & is_subspace H E
+ & is_subspace F H
+ & (graph F f <= graph H h)
+ & (ALL x:H. h x <= p x)";
+ assume "x:H";
+ have e1: "EX H' h' t. t : (graph H h) & t = (x, h x) & (graph H' h'):c & t:graph H' h' &
+ ?P H' h'";
+ by (rule some_H'h't);
+ assume "y:H";
+ have e2: "EX H' h' t. t : (graph H h) & t = (y, h y) & (graph H' h'):c & t:graph H' h' &
+ ?P H' h'";
+ by (rule some_H'h't);
+
+ from e1 e2; show ?thesis;
+ proof (elim exE conjE);
+ fix H' h' t' H'' h'' t'';
+ assume "t' : graph H h" "t'' : graph H h"
+ "t' = (y, h y)" "t'' = (x, h x)"
+ "graph H' h' : c" "graph H'' h'' : c"
+ "t' : graph H' h'" "t'' : graph H'' h''"
+ "is_linearform H' h'" "is_linearform H'' h''"
+ "is_subspace H' E" "is_subspace H'' E"
+ "is_subspace F H'" "is_subspace F H''"
+ "graph F f <= graph H' h'" "graph F f <= graph H'' h''"
+ "ALL x:H'. h' x <= p x" "ALL x:H''. h'' x <= p x";
+
+ have "(graph H'' h'') <= (graph H' h') | (graph H' h') <= (graph H'' h'')";
+ by (rule chainD);
+ thus "?thesis";
+ proof;
+ assume "(graph H'' h'') <= (graph H' h')";
+ show ?thesis;
+ proof (intro exI conjI);
+ have xh: "(x, h x): graph H' h'"; by (fast);
+ thus x: "x:H'"; by (rule graphD1);
+ show y: "y:H'"; by (asm_simp, rule graphD1);
+ show "(graph H' h') <= (graph H h)";
+ by (asm_simp only: chain_ball_Union_upper);
+ qed;
+ next;
+ assume "(graph H' h') <= (graph H'' h'')";
+ show ?thesis;
+ proof (intro exI conjI);
+ show x: "x:H''"; by (asm_simp, rule graphD1);
+ have yh: "(y, h y): graph H'' h''"; by (fast);
+ thus y: "y:H''"; by (rule graphD1);
+ show "(graph H'' h'') <= (graph H h)";
+ by (asm_simp only: chain_ball_Union_upper);
+ qed;
+ qed;
+ qed;
+qed;
+
+
+
+lemma sup_uniq: "[| is_vectorspace E; is_subspace F E; is_quasinorm E p; is_linearform F f;
+ ALL x:F. f x <= p x; M == norm_prev_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";
+ have "EX H h. (x, y) : graph H h & (x, z) : graph H h";
+ proof (elim UnionE chainD2 [elimify]);
+ fix G1 G2; assume "(x, y) : G1" "G1 : c" "(x, z) : G2" "G2 : c" "c <= M";
+ have "G1 : M"; by (rule subsetD);
+ hence e1: "EX H1 h1. graph H1 h1 = G1";
+ by (force dest: norm_prev_extension_D);
+ have "G2 : M"; by (rule subsetD);
+ hence e2: "EX H2 h2. graph H2 h2 = G2";
+ by (force dest: norm_prev_extension_D);
+ from e1 e2; show ?thesis;
+ proof (elim exE);
+ fix H1 h1 H2 h2; assume "graph H1 h1 = G1" "graph H2 h2 = G2";
+ have "G1 <= G2 | G2 <= G1"; by (rule chainD);
+ thus ?thesis;
+ proof;
+ assume "G1 <= G2";
+ thus ?thesis;
+ proof (intro exI conjI);
+ show "(x, y) : graph H2 h2"; by force;
+ show "(x, z) : graph H2 h2"; by asm_simp;
+ qed;
+ next;
+ assume "G2 <= G1";
+ thus ?thesis;
+ proof (intro exI conjI);
+ show "(x, y) : graph H1 h1"; by asm_simp;
+ show "(x, z) : graph H1 h1"; by force;
+ qed;
+ qed;
+ qed;
+ qed;
+ thus ?thesis;
+ proof (elim exE conjE);
+ fix H h; assume "(x, y) : graph H h" "(x, z) : graph H h";
+ have "y = h x"; by (rule graph_lemma2);
+ also; have "h x = z"; by (rule graph_lemma2 [RS sym]);
+ finally; show "z = y"; by (rule sym);
+ qed;
+qed;
+
+
+lemma sup_lf: "[| M = norm_prev_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";
+
+ let ?P = "%H h. is_linearform H h
+ & is_subspace H E
+ & is_subspace F H
+ & (graph F f <= graph H h)
+ & (ALL x:H. h x <= p x)";
+
+ show "is_linearform H h";
+ proof;
+ fix x y; assume "x : H" "y : H";
+ show "h (x [+] y) = h x + h y";
+ proof -;
+ have "EX H' h'. x:H' & y:H' & (graph H' h' <= graph H h) &
+ is_linearform H' h' & is_subspace H' E & is_subspace F H' &
+ (graph F f <= graph H' h') & (ALL x:H'. h' x <= p x)";
+ by (rule some_H'h'2);
+ thus ?thesis;
+ proof (elim exE conjE);
+ fix H' h'; assume "x:H'" "y:H'"
+ and b: "graph H' h' <= graph H h"
+ and "is_linearform H' h'" "is_subspace H' E";
+ have h'x: "h' x = h x"; by (rule graph_lemma3);
+ have h'y: "h' y = h y"; by (rule graph_lemma3);
+ 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'";
+ by (rule subspace_add_closed);
+ with b; show ?thesis; by (rule graph_lemma3);
+ qed;
+ with h'x h'y h'xy; show ?thesis;
+ by asm_simp;
+ qed;
+ qed;
+
+ next;
+ fix a x; assume "x : H";
+ show "h (a [*] x) = a * (h x)";
+ proof -;
+ have "EX H' h'. x:H' & (graph H' h' <= graph H h) &
+ is_linearform H' h' & is_subspace H' E & is_subspace F H' &
+ (graph F f <= graph H' h') & (ALL x:H'. h' x <= p x)";
+ by (rule some_H'h');
+ thus ?thesis;
+ proof (elim exE conjE);
+ fix H' h';
+ assume b: "graph H' h' <= graph H h";
+ assume "x:H'" "is_linearform H' h'" "is_subspace H' E";
+ have h'x: "h' x = h x"; by (rule graph_lemma3);
+ 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'";
+ by (rule subspace_mult_closed);
+ with b; show ?thesis; by (rule graph_lemma3);
+ qed;
+ with h'x h'ax; show ?thesis;
+ by asm_simp;
+ qed;
+ qed;
+ qed;
+qed;
+
+
+lemma sup_ext: "[| M = norm_prev_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"
+ and e: "EX x. x:c";
+
+ show ?thesis;
+ proof (elim exE);
+ fix x; assume "x:c";
+ show ?thesis;
+ proof -;
+ have "x:norm_prev_extensions E p F f";
+ proof (rule subsetD);
+ show "c <= norm_prev_extensions E p F f"; by (asm_simp add: chainD2);
+ qed;
+
+ hence "(EX G g. graph G g = x
+ & is_linearform G g
+ & is_subspace G E
+ & is_subspace F G
+ & (graph F f <= graph G g)
+ & (ALL x:G. g x <= p x))";
+ by (asm_simp add: norm_prev_extension_D);
+
+ thus ?thesis;
+ proof (elim exE conjE);
+ fix G g; assume "graph G g = x" "graph F f <= graph G g";
+ show ?thesis;
+ proof -;
+ have "graph F f <= graph G g"; by assumption;
+ also; have "graph G g <= graph H h"; by (asm_simp, fast);
+ finally; show ?thesis; .;
+ qed;
+ qed;
+ qed;
+ qed;
+qed;
+
+
+lemma sup_supF: "[| M = norm_prev_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"
+ "is_subspace F E";
+
+ show ?thesis;
+ proof (rule subspace_I);
+ show "<0> : F"; by (rule zero_in_subspace);
+ show "F <= H";
+ proof (rule graph_lemma4);
+ show "graph F f <= graph H h";
+ by (rule sup_ext);
+ qed;
+ show "ALL x:F. ALL y:F. x [+] y : F";
+ proof (intro ballI);
+ fix x y; assume "x:F" "y:F";
+ show "x [+] y : F"; by asm_simp;
+ qed;
+ show "ALL x:F. ALL a. a [*] x : F";
+ proof (intro ballI allI);
+ fix x a; assume "x:F";
+ show "a [*] x : F"; by asm_simp;
+ qed;
+ qed;
+qed;
+
+
+lemma sup_subE: "[| M = norm_prev_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"
+ "is_subspace F E";
+
+ show ?thesis;
+ proof (rule subspace_I);
+
+ show "<0> : H";
+ proof (rule subsetD [of F H]);
+ have "is_subspace F H"; by (rule sup_supF);
+ thus "F <= H"; by (rule subspace_subset);
+ show "<0> :F"; by (rule zero_in_subspace);
+ qed;
+
+ show "H <= E";
+ proof;
+ fix x; assume "x:H";
+ show "x:E";
+ proof -;
+ have "EX H' h'. x:H' & (graph H' h' <= graph H h) &
+ is_linearform H' h' & is_subspace H' E & is_subspace F H' &
+ (graph F f <= graph H' h') & (ALL x:H'. h' x <= p x)";
+ by (rule some_H'h');
+ thus ?thesis;
+ proof (elim exE conjE);
+ fix H' h'; assume "x:H'" "is_subspace H' E";
+ show "x:E";
+ proof (rule subsetD);
+ show "H' <= E";
+ by (rule subspace_subset);
+ qed;
+ qed;
+ qed;
+ qed;
+
+ show "ALL x:H. ALL y:H. x [+] y : H";
+ proof (intro ballI);
+ fix x y; assume "x:H" "y:H";
+ show "x [+] y : H";
+ proof -;
+ have "EX H' h'. x:H' & y:H' & (graph H' h' <= graph H h) &
+ is_linearform H' h' & is_subspace H' E & is_subspace F H' &
+ (graph F f <= graph H' h') & (ALL x:H'. h' x <= p x)";
+ by (rule some_H'h'2);
+ thus ?thesis;
+ proof (elim exE conjE);
+ fix H' h'; assume "x:H'" "y:H'" "is_subspace H' E" "graph H' h' <= graph H h";
+ have "H' <= H"; by (rule graph_lemma4);
+ thus ?thesis;
+ proof (rule subsetD);
+ show "x [+] y : H'"; by (rule subspace_add_closed);
+ qed;
+ qed;
+ qed;
+ qed;
+
+ show "ALL x:H. ALL a. a [*] x : H";
+ proof (intro ballI allI);
+ fix x and a::real; assume "x:H";
+ show "a [*] x : H";
+ proof -;
+ have "EX H' h'. x:H' & (graph H' h' <= graph H h) &
+ is_linearform H' h' & is_subspace H' E & is_subspace F H' &
+ (graph F f <= graph H' h') & (ALL x:H'. h' x <= p x)";
+ by (rule some_H'h');
+ thus ?thesis;
+ proof (elim exE conjE);
+ fix H' h'; assume "x:H'" "is_subspace H' E" "graph H' h' <= graph H h";
+ have "H' <= H"; by (rule graph_lemma4);
+ thus ?thesis;
+ proof (rule subsetD);
+ show "a [*] x : H'"; by (rule subspace_mult_closed);
+ qed;
+ qed;
+ qed;
+ qed;
+ qed;
+qed;
+
+
+lemma sup_norm_prev: "[| M = norm_prev_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";
+ fix x; assume "x:H";
+ show "h x <= p x";
+ proof -;
+ have "EX H' h'. x:H' & (graph H' h' <= graph H h) &
+ is_linearform H' h' & is_subspace H' E & is_subspace F H' &
+ (graph F f <= graph H' h') & (ALL x:H'. h' x <= p x)";
+ by (rule some_H'h');
+ thus ?thesis;
+ proof (elim exE conjE);
+ fix H' h'; assume "x: H'" "graph H' h' <= graph H h" and a: "ALL x: H'. h' x <= p x" ;
+ have "h x = h' x";
+ proof(rule sym);
+ show "h' x = h x"; by (rule graph_lemma3);
+ qed;
+ also; from a; have "... <= p x "; ..;
+ finally; show ?thesis; .;
+ qed;
+ qed;
+qed;
+
+
+end;
\ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Real/HahnBanach/LinearSpace.thy Fri Sep 10 17:28:51 1999 +0200
@@ -0,0 +1,485 @@
+
+theory LinearSpace = Main + RealAbs + Bounds + Aux:;
+
+
+section {* vector spaces *};
+
+consts
+ sum :: "['a, 'a] => 'a" (infixl "[+]" 65)
+ prod :: "[real, 'a] => 'a" (infixr "[*]" 70)
+ zero :: "'a" ("<0>");
+
+constdefs
+ negate :: "'a => 'a" ("[-] _" [100] 100)
+ "[-] x == (- 1r) [*] x"
+ diff :: "'a => 'a => 'a" (infixl "[-]" 68)
+ "x [-] y == x [+] [-] y";
+
+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);
+
+lemma vs_I:
+ "[| <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";
+ by (unfold is_vectorspace_def) auto;
+
+lemma zero_in_vs [simp, dest]: "is_vectorspace V ==> <0>:V";
+ by (unfold is_vectorspace_def) asm_simp;
+
+lemma vs_not_empty: "is_vectorspace V ==> (V ~= {})";
+ by (unfold is_vectorspace_def) fast;
+
+lemma vs_add_closed [simp]: "[| is_vectorspace V; x: V; y: V|] ==> x [+] y: V";
+ by (unfold is_vectorspace_def) asm_simp;
+
+lemma vs_mult_closed [simp]: "[| is_vectorspace V; x: V |] ==> a [*] x: V";
+ by (unfold is_vectorspace_def) asm_simp;
+
+lemma vs_diff_closed [simp]: "[| is_vectorspace V; x: V; y: V|] ==> x [-] y: V";
+ by (unfold diff_def negate_def) asm_simp;
+
+lemma vs_neg_closed [simp]: "[| is_vectorspace V; x: V |] ==> [-] x: V";
+ by (unfold negate_def) asm_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) asm_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 (asm_simp only: vs_add_assoc);
+ also; have "... = (y [+] x) [+] z";
+ by (asm_simp only: vs_add_commute);
+ also; have "... = y [+] (x [+] z)";
+ by (asm_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) asm_simp;
+
+lemma vs_add_zero_left [simp]: "[| is_vectorspace V; x:V |] ==> <0> [+] x = x";
+ by (unfold is_vectorspace_def) asm_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 asm_simp;
+ also; have "... = x";
+ by asm_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) asm_simp;
+
+lemma vs_add_mult_distrib2:
+ "[| is_vectorspace V; x:V |] ==> (a + b) [*] x = a [*] x [+] b [*] x";
+ by (unfold is_vectorspace_def) asm_simp;
+
+lemma vs_mult_assoc: "[| is_vectorspace V; x:V |] ==> (a * b) [*] x = a [*] (b [*] x)";
+ by (unfold is_vectorspace_def) asm_simp;
+
+lemma vs_mult_assoc2 [simp]: "[| is_vectorspace V; x:V |] ==> a [*] b [*] x = (a * b) [*] x";
+ by (asm_simp only: vs_mult_assoc);
+
+lemma vs_mult_1 [simp]: "[| is_vectorspace V; x:V |] ==> 1r [*] x = x";
+ by (unfold is_vectorspace_def) asm_simp;
+
+lemma vs_diff_mult_distrib1:
+ "[| is_vectorspace V; x:V; y:V |] ==> a [*] (x [-] y) = a [*] x [-] a [*] y";
+ by (asm_simp add: diff_def negate_def vs_add_mult_distrib1);
+
+lemma vs_minus_eq: "[| is_vectorspace V; x:V |] ==> - b [*] x = [-] (b [*] x)";
+ by (asm_simp add: negate_def);
+
+lemma vs_diff_mult_distrib2:
+ "[| is_vectorspace V; x:V |] ==> (a - b) [*] x = a [*] x [-] (b [*] x)";
+proof -;
+ assume "is_vectorspace V" "x:V";
+ have " (a - b) [*] x = (a + - b ) [*] x"; by (unfold real_diff_def, simp);
+ also; have "... = a [*] x [+] (- b) [*] x"; by (rule vs_add_mult_distrib2);
+ also; have "... = a [*] x [+] [-] (b [*] x)"; by (asm_simp add: vs_minus_eq);
+ also; have "... = a [*] x [-] (b [*] x)"; by (unfold diff_def, simp);
+ finally; show ?thesis; .;
+qed;
+
+lemma vs_mult_zero_left [simp]: "[| is_vectorspace V; x: V|] ==> 0r [*] x = <0>";
+proof -;
+ assume vs: "is_vectorspace V" "x:V";
+ have "0r [*] x = (1r - 1r) [*] x";
+ by (asm_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 asm_simp;
+ also; have "... = x [-] x";
+ by (rule vs_add_mult_minus_1_eq_diff);
+ also; have "... = <0>";
+ by asm_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 (asm_simp);
+ also; from zero_in_vs [of V]; have "... = a [*] <0> [-] a [*] <0>";
+ by (asm_simp only: vs_diff_mult_distrib1);
+ also; have "... = <0>";
+ by asm_simp;
+ finally; show ?thesis; .;
+qed;
+
+lemma vs_minus_mult_cancel [simp]: "[| is_vectorspace V; x:V |] ==> (- a) [*] [-] x = a [*] x";
+ by (unfold negate_def) asm_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 asm_simp;
+ assume y: "y:V";
+ have "[-] x [+] y = y [+] [-] x";
+ by (asm_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 (asm_simp add: vs_add_minus_eq_diff);
+
+lemma vs_add_minus_left [simp]: "[| is_vectorspace V; x:V |] ==> [-] x [+] x = <0>";
+ by (asm_simp add: vs_add_minus_eq_diff);
+
+lemma vs_minus_minus [simp]: "[| is_vectorspace V; x:V|] ==> [-] [-] x = x";
+ by (unfold negate_def) asm_simp;
+
+lemma vs_minus_zero [simp]: "[| is_vectorspace (V::'a set)|] ==> [-] (<0>::'a) = <0>";
+ by (unfold negate_def) asm_simp;
+
+lemma vs_minus_zero_iff [simp]:
+ "[| is_vectorspace V; x:V|] ==> ([-] x = <0>) = (x = <0>)" (concl is "?L = ?R");
+proof -;
+ assume vs: "is_vectorspace V" "x:V";
+ show "?L = ?R";
+ proof;
+ assume l: ?L;
+ have "x = [-] [-] x";
+ by (rule vs_minus_minus [RS sym]);
+ also; have "... = [-] <0>";
+ by (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;
+ qed;
+qed;
+
+lemma vs_add_minus_cancel [simp]: "[| is_vectorspace V; x:V; y:V|] ==> x [+] ([-] x [+] y) = y";
+ by (asm_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 (asm_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, asm_simp add: vs_add_mult_distrib1);
+
+lemma vs_diff_zero [simp]: "[| is_vectorspace V; x:V |] ==> x [-] <0> = x";
+ by (unfold diff_def) asm_simp;
+
+lemma vs_diff_zero_right [simp]: "[| is_vectorspace V; x:V |] ==> <0> [-] x = [-] x";
+ by (unfold diff_def) asm_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 l: ?L;
+ have "y = <0> [+] y";
+ by asm_simp;
+ also; have "... = [-] x [+] x [+] y";
+ by asm_simp;
+ also; from vs vs_neg_closed x y ; have "... = [-] x [+] (x [+] y)";
+ by (rule vs_add_assoc);
+ also; have "... = [-] x [+] (x [+] z)";
+ by (asm_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 asm_simp;
+ finally; show ?R;.;
+next;
+ assume ?R;
+ show ?L;
+ by force;
+qed;
+
+lemma vs_add_right_cancel:
+ "[| is_vectorspace V; x:V; y:V; z:V |] ==> (y [+] x = z [+] x) = (y = z)";
+ by (asm_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 (asm_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 (asm_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 (asm_simp);
+ also; have "... = (rinv a * a) [*] x";
+ by (asm_simp);
+ also; have "... = rinv a [*] (a [*] x)";
+ by (asm_simp only: vs_mult_assoc);
+ also; have "... = rinv a [*] (a [*] y)";
+ by (asm_simp only: l);
+ also; have "... = y";
+ by (asm_simp);
+ finally; show ?R;.;
+next;
+ assume ?R;
+ show ?L;
+ by (asm_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 asm_simp;
+ assume z: "z:V";
+ show "?L = ?R";
+ proof;
+ assume l: ?L;
+ have "x [+] y = z [-] y [+] y";
+ by (asm_simp add: l);
+ also; have "... = z [+] [-] y [+] y";
+ by (asm_simp only: vs_add_minus_eq_diff);
+ also; from vs z n y; have "... = z [+] ([-] y [+] y)";
+ by (asm_simp only: vs_add_assoc);
+ also; have "... = z [+] <0>";
+ by (asm_simp only: vs_add_minus_left);
+ also; have "... = z";
+ by (asm_simp only: vs_add_zero_right);
+ finally; show ?R;.;
+ next;
+ assume r: ?R;
+ have "z [-] y = (x [+] y) [-] y";
+ by (asm_simp only: r);
+ also; have "... = x [+] y [+] [-] y";
+ by (asm_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 (asm_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 (asm_simp);
+ assume y: "y:V";
+ assume xy: "<0> = x [+] y";
+ from vs n; have "[-] x = [-] x [+] <0>";
+ by asm_simp;
+ also; have "... = [-] x [+] (x [+] y)";
+ by (asm_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 (asm_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 asm_simp;
+ also; from _ _ _ e; have "[-] x = [-] y";
+ by (rule vs_add_minus_eq_minus [RS sym, of V x "[-] y"]) asm_simp+;
+ also; have "[-] ... = y"; by asm_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 (asm_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 (asm_simp add: vs_add_right_cancel);
+ also; have "... = d [-] b"; by (simp add : diff_def);
+ finally; show "a [-] c = d [-] b"; .;
+qed;
+
+
+lemma vs_mult_zero_uniq :
+ "[| is_vectorspace V; x:V; a [*] x = <0>; x ~= <0> |] ==> a = 0r";
+proof (rule classical);
+ assume "is_vectorspace V" "x:V" "a [*] x = <0>" "x ~= <0>";
+ assume "a ~= 0r";
+ have "x = (rinv a * a) [*] x"; by asm_simp;
+ also; have "... = (rinv a) [*] (a [*] x)"; by (rule vs_mult_assoc);
+ also; have "... = (rinv a) [*] <0>"; by asm_simp;
+ also; have "... = <0>"; by asm_simp;
+ finally; have "x = <0>"; .;
+ thus "a = 0r"; by contradiction;
+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 (asm_simp);
+ assume z: "z:V"; hence xz: "x [+] z: V"; by (asm_simp);
+ assume u: "u:V";
+ show "?L = ?R";
+ proof;
+ assume l: ?L;
+ from vs u; have "u = <0> [+] u";
+ by asm_simp;
+ also; from vs y vs_neg_closed u; have "... = [-] y [+] y [+] u";
+ by asm_simp;
+ also; from vs n y u; have "... = [-] y [+] (y [+] u)";
+ by (asm_simp only: vs_add_assoc);
+ also; have "... = [-] y [+] (x [+] (y [+] z))";
+ by (asm_simp only: l);
+ also; have "... = [-] y [+] (y [+] (x [+] z))";
+ by (asm_simp only: vs_add_left_commute);
+ also; from vs n y xz; have "... = [-] y [+] y [+] (x [+] z)";
+ by (asm_simp only: vs_add_assoc);
+ also; have "... = (x [+] z)";
+ by (asm_simp);
+ finally; show ?R; by (rule sym);
+ next;
+ assume r: ?R;
+ have "x [+] (y [+] z) = y [+] (x [+] z)";
+ by (asm_simp only: vs_add_left_commute [of V x y z]);
+ also; have "... = y [+] u";
+ by (asm_simp only: r);
+ finally; show ?L; .;
+ qed;
+qed;
+
+lemma vs_add_cancel_end:
+ "[| is_vectorspace V; x:V; y:V; z:V |] ==> (x [+] (y [+] z) = y) = (x = [-] z)"
+ (concl is "?L = ?R" );
+proof -;
+ assume vs: "is_vectorspace V";
+ assume x: "x:V";
+ assume y: "y:V";
+ assume z: "z:V"; hence xz: "x [+] z: V"; by (asm_simp);
+ hence nz: "[-] z: V"; by (asm_simp);
+ show "?L = ?R";
+ proof;
+ assume l: ?L;
+ have n: "<0>:V"; by (asm_simp);
+ have "y [+] <0> = y";
+ by (asm_simp only: vs_add_zero_right);
+ also; have "... = x [+] (y [+] z)";
+ by (asm_simp only: l);
+ also; have "... = y [+] (x [+] z)";
+ by (asm_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 (asm_simp only: vs_add_minus_eq_minus);
+ then; show ?R;
+ by (asm_simp);
+ next;
+ assume r: ?R;
+ have "x [+] (y [+] z) = [-] z [+] (y [+] z)";
+ by (asm_simp only: r);
+ also; from vs nz y z; have "... = y [+] ([-] z [+] z)";
+ by (asm_simp only: vs_add_left_commute);
+ also; have "... = y [+] <0>";
+ by (asm_simp);
+ also; have "... = y";
+ by (asm_simp);
+ finally; show ?L; .;
+ qed;
+qed;
+
+lemma it: "[| x = y; x' = y'|] ==> x [+] x' = y [+] y'";
+ by (asm_simp);
+
+
+end;
\ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Real/HahnBanach/Linearform.thy Fri Sep 10 17:28:51 1999 +0200
@@ -0,0 +1,53 @@
+
+theory Linearform = LinearSpace:;
+
+section {* linearforms *};
+
+constdefs
+ is_linearform :: "['a set, 'a => real] => bool"
+ "is_linearform V f ==
+ (ALL x: V. ALL y: V. f (x [+] y) = f x + f y) &
+ (ALL x: V. ALL a. f (a [*] x) = a * (f x))";
+
+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);
+
+lemma linearform_add_linear: "[| is_linearform V f; x:V; y:V |] ==> f (x [+] y) = f x + f y";
+ by (unfold is_linearform_def, auto);
+
+lemma linearform_mult_linear: "[| is_linearform V f; x:V |] ==> f (a [*] x) = a * (f x)";
+ by (unfold is_linearform_def, auto);
+
+lemma linearform_neg_linear:
+ "[| 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 (asm_simp add: vs_mult_minus_1);
+ also; have "... = (- 1r) * (f x)"; by (rule linearform_mult_linear);
+ also; have "... = - (f x)"; by asm_simp;
+ finally; show ?thesis; .;
+qed;
+
+lemma linearform_diff_linear:
+ "[| 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) (asm_simp+);
+ also; have "f ([-] y) = - f y"; by (rule linearform_neg_linear);
+ finally; show "f (x [-] y) = f x - f y"; by asm_simp;
+qed;
+
+lemma linearform_zero: "[| 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 asm_simp;
+ also; have "... = f <0> - f <0>"; by (rule linearform_diff_linear) asm_simp+;
+ also; have "... = 0r"; by simp;
+ finally; show "f <0> = 0r"; .;
+qed;
+
+end;
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Real/HahnBanach/NormedSpace.thy Fri Sep 10 17:28:51 1999 +0200
@@ -0,0 +1,142 @@
+
+theory NormedSpace = Subspace:;
+
+
+section {* normed vector spaces *};
+
+subsection {* quasinorm *};
+
+constdefs
+ is_quasinorm :: "['a set, 'a => real] => bool"
+ "is_quasinorm V norm == ALL x: V. ALL y:V. ALL a.
+ 0r <= norm x
+ & norm (a [*] x) = (rabs a) * (norm x)
+ & norm (x [+] y) <= norm x + norm y";
+
+lemma is_quasinormI[intro]:
+ "[| !! x y a. [| x:V; y:V|] ==> 0r <= norm x;
+ !! x a. x:V ==> norm (a [*] x) = (rabs a) * (norm x);
+ !! x y. [|x:V; y:V |] ==> norm (x [+] y) <= norm x + norm y |]
+ ==> is_quasinorm V norm";
+ by (unfold is_quasinorm_def, force);
+
+lemma quasinorm_ge_zero:
+ "[|is_quasinorm V norm; x:V |] ==> 0r <= norm x";
+ by (unfold is_quasinorm_def, force);
+
+lemma quasinorm_mult_distrib:
+ "[|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";
+ 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";
+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 (rule quasinorm_triangle_ineq, asm_simp+);
+ 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";
+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) = 1r"; by (rule rabs_minus_one);
+ finally; show "norm ([-] x) = norm x"; by simp;
+qed;
+
+
+subsection {* norm *};
+
+constdefs
+ is_norm :: "['a set, 'a => real] => bool"
+ "is_norm V norm == ALL x: V. is_quasinorm V norm
+ & (norm x = 0r) = (x = <0>)";
+
+lemma is_norm_I: "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: "[| 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>)";
+ by (unfold is_norm_def, force);
+
+lemma norm_ge_zero:
+ "[|is_norm V norm; x:V |] ==> 0r <= norm x";
+ by (unfold is_norm_def, unfold is_quasinorm_def, force);
+
+
+subsection {* normed vector space *};
+
+constdefs
+ is_normed_vectorspace :: "['a set, 'a => real] => bool"
+ "is_normed_vectorspace V norm ==
+ is_vectorspace V &
+ is_norm V norm";
+
+lemma normed_vsI: "[| is_vectorspace V; is_norm V norm |] ==> is_normed_vectorspace V norm";
+ by (unfold is_normed_vectorspace_def, intro conjI);
+
+lemma normed_vs_vs: "is_normed_vectorspace V norm ==> is_vectorspace V";
+ by (unfold is_normed_vectorspace_def, force);
+
+lemma normed_vs_norm: "is_normed_vectorspace V norm ==> is_norm V norm";
+ by (unfold is_normed_vectorspace_def, force);
+
+lemma normed_vs_norm_ge_zero: "[| is_normed_vectorspace V norm; x:V |] ==> 0r <= norm x";
+ by (unfold is_normed_vectorspace_def, elim conjE, rule norm_ge_zero);
+
+lemma normed_vs_norm_gt_zero:
+ "[| is_normed_vectorspace V norm; x:V; x ~= <0> |] ==> 0r < norm x";
+proof (unfold is_normed_vectorspace_def, elim conjE);
+ assume "x : V" "x ~= <0>" "is_vectorspace V" "is_norm V norm";
+ have "0r <= norm x"; by (rule norm_ge_zero);
+ also; have "0r ~= norm x";
+ proof;
+ presume "norm x = 0r";
+ have "x = <0>"; by (asm_simp add: norm_zero_iff);
+ thus "False"; by contradiction;
+ qed (rule sym);
+ finally; show "0r < norm x"; .;
+qed;
+
+lemma normed_vs_norm_mult_distrib:
+ "[| is_normed_vectorspace V norm; x:V |] ==> norm (a [*] x) = (rabs a) * (norm x)";
+ by (unfold is_normed_vectorspace_def, elim conjE,
+ rule quasinorm_mult_distrib, rule norm_is_quasinorm);
+
+lemma normed_vs_norm_triangle_ineq:
+ "[| is_normed_vectorspace V norm; x:V; y:V |] ==> norm (x [+] y) <= norm x + norm y";
+ by (unfold is_normed_vectorspace_def, elim conjE,
+ rule quasinorm_triangle_ineq, rule norm_is_quasinorm);
+
+lemma subspace_normed_vs:
+ "[| 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";
+ show "is_vectorspace F"; by (rule subspace_vs);
+ show "is_norm F norm";
+ proof (intro is_norm_I ballI conjI);
+ show "is_quasinorm F norm";
+ proof (rule is_quasinormI, rule normed_vs_norm_ge_zero [of E norm],
+ rule normed_vs_norm_mult_distrib [of E norm], rule normed_vs_norm_triangle_ineq);
+ qed ( rule subsetD [OF subspace_subset], assumption+)+;
+
+ fix x; assume "x : F";
+ have n: "is_norm E norm"; by (unfold is_normed_vectorspace_def, asm_simp);
+ have "x:E"; by (rule subsetD [OF subspace_subset]);
+ from n this; show "(norm x = 0r) = (x = <0>)"; by (rule norm_zero_iff);
+ qed;
+qed;
+
+end;
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Real/HahnBanach/ROOT.ML Fri Sep 10 17:28:51 1999 +0200
@@ -0,0 +1,8 @@
+(* Title: HOL/Real/HahnBanach/ROOT.ML
+ ID: $Id$
+ Author: Gertrud Bauer, TU Munich
+
+The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar).
+*)
+
+time_use_thy "HahnBanach";
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Real/HahnBanach/Subspace.thy Fri Sep 10 17:28:51 1999 +0200
@@ -0,0 +1,319 @@
+
+theory Subspace = LinearSpace:;
+
+
+section {* subspaces *};
+
+constdefs
+ is_subspace :: "['a set, 'a set] => bool"
+ "is_subspace U V == <0>:U & U <= V
+ & (ALL x:U. ALL y:U. ALL a. x [+] y : U
+ & a [*] x : U)";
+
+lemma subspace_I:
+ "[| <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) blast;
+
+lemma "is_subspace U V ==> U ~= {}";
+ by (unfold is_subspace_def) force;
+
+lemma zero_in_subspace: "is_subspace U V ==> <0>:U";
+ by (unfold is_subspace_def) force;
+
+lemma subspace_subset: "is_subspace U V ==> U <= V";
+ by (unfold is_subspace_def) fast;
+
+lemma subspace_subset2 [simp]: "[| is_subspace U V; x:U |]==> x:V";
+ by (unfold is_subspace_def) fast;
+
+lemma subspace_add_closed [simp]: "[| is_subspace U V; x: U; y: U |] ==> x [+] y: U";
+ by (unfold is_subspace_def) asm_simp;
+
+lemma subspace_mult_closed [simp]: "[| is_subspace U V; x: U |] ==> a [*] x: U";
+ by (unfold is_subspace_def) asm_simp;
+
+lemma subspace_diff_closed [simp]: "[| is_subspace U V; x: U; y: U |] ==> x [-] y: U";
+ by (unfold diff_def negate_def) asm_simp;
+
+lemma subspace_neg_closed [simp]: "[| is_subspace U V; x: U |] ==> [-] x: U";
+ by (unfold negate_def) asm_simp;
+
+theorem subspace_vs [intro!!]:
+ "[| is_subspace U V; is_vectorspace V |] ==> is_vectorspace U";
+proof -;
+ presume "U <= V";
+ assume "is_vectorspace V";
+ assume "is_subspace U V";
+ show ?thesis;
+ proof (rule vs_I);
+ show "<0>:U"; by (rule zero_in_subspace);
+ show "ALL x:U. ALL a. a [*] x : U"; by asm_simp;
+ show "ALL x:U. ALL y:U. x [+] y : U"; by asm_simp;
+ qed (asm_simp add: vs_add_mult_distrib1 vs_add_mult_distrib2)+;
+next;
+ assume "is_subspace U V";
+ show "U <= V"; by (rule subspace_subset);
+qed;
+
+lemma subspace_refl: "is_vectorspace V ==> is_subspace V V";
+proof (unfold is_subspace_def, intro conjI);
+ assume "is_vectorspace V";
+ show "<0> : V"; by (rule zero_in_vs [of V], assumption);
+ show "V <= V"; by (simp);
+ show "ALL x::'a:V. ALL y::'a:V. ALL a::real. x [+] y : V & a [*] x : V"; by (asm_simp);
+qed;
+
+lemma subspace_trans: "[| is_subspace U V; is_subspace V W |] ==> is_subspace U W";
+proof (rule subspace_I);
+ assume "is_subspace U V" "is_subspace V W";
+ show "<0> : U"; by (rule zero_in_subspace);;
+ from subspace_subset [of U] subspace_subset [of V]; show uw: "U <= W"; by force;
+ 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 (rule subspace_add_closed);
+ qed;
+ show "ALL x:U. ALL a. a [*] x : U";
+ proof (intro ballI allI);
+ fix x a; assume "x:U";
+ show "a [*] x : U"; by (rule subspace_mult_closed);
+ qed;
+qed;
+
+
+section {* linear closure *};
+
+constdefs
+ lin :: "'a => 'a set"
+ "lin x == {y. ? a. y = a [*] x}";
+
+lemma linD: "x : lin v = (? a::real. x = a [*] v)";
+ by (unfold lin_def) fast;
+
+lemma x_lin_x: "[| is_vectorspace V; x:V |] ==> x:lin x";
+proof (unfold lin_def, intro CollectI exI);
+ assume "is_vectorspace V" "x:V";
+ show "x = 1r [*] x"; by (asm_simp);
+qed;
+
+lemma lin_subspace: "[| is_vectorspace V; x:V |] ==> is_subspace (lin x) V";
+proof (rule subspace_I);
+ assume "is_vectorspace V" "x:V";
+ show "<0> : lin x";
+ proof (unfold lin_def, intro CollectI exI);
+ show "<0> = 0r [*] x"; by asm_simp;
+ qed;
+ show "lin x <= V";
+ proof (unfold lin_def, intro subsetI, elim CollectD [elimify] exE);
+ fix xa a; assume "xa = a [*] x"; show "xa:V"; by asm_simp;
+ qed;
+ show "ALL x1 : lin x. ALL x2 : lin x. x1 [+] x2 : lin x";
+ proof (intro ballI);
+ fix x1 x2; assume "x1 : lin x" "x2 : lin x"; show "x1 [+] x2 : lin x";
+ proof (unfold lin_def, elim CollectD [elimify] exE, intro CollectI exI);
+ fix a1 a2; assume "x1 = a1 [*] x" "x2 = a2 [*] x";
+ show "x1 [+] x2 = (a1 + a2) [*] x"; by (asm_simp add: vs_add_mult_distrib2);
+ qed;
+ qed;
+ show "ALL xa:lin x. ALL a. a [*] xa : lin x";
+ proof (intro ballI allI);
+ fix x1 a; assume "x1 : lin x"; show "a [*] x1 : lin x";
+ proof (unfold lin_def, elim CollectD [elimify] exE, intro CollectI exI);
+ fix a1; assume "x1 = a1 [*] x";
+ show "a [*] x1 = (a * a1) [*] x"; by asm_simp;
+ qed;
+ qed;
+qed;
+
+
+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"; by (rule lin_subspace);
+qed;
+
+section {* sum of two vectorspaces *};
+
+constdefs
+ vectorspace_sum :: "['a set, 'a set] => 'a set"
+ "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) fast;
+
+lemma vs_sum_I: "[| 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)";
+proof (rule subspace_I);
+ assume "is_vectorspace U" "is_vectorspace V";
+ show "<0> : U"; by (rule zero_in_vs);
+ show "U <= vectorspace_sum U V";
+ proof (intro subsetI vs_sum_I);
+ fix x; assume "x:U";
+ show "x = x [+] <0>"; by asm_simp;
+ show "<0> : V"; by asm_simp;
+ qed;
+ 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 asm_simp;
+ qed;
+ show "ALL x:U. ALL a. a [*] x : U";
+ proof (intro ballI allI);
+ fix x a; assume "x:U"; show "a [*] x : U"; by asm_simp;
+ qed;
+qed;
+
+lemma vs_sum_subspace:
+ "[| is_subspace U E; is_subspace V E; is_vectorspace E |] ==> is_subspace (vectorspace_sum U V) E";
+proof (rule subspace_I);
+ assume u: "is_subspace U E" and v: "is_subspace V E" and e: "is_vectorspace E";
+
+ show "<0> : vectorspace_sum U V";
+ by (intro vs_sum_I, rule vs_add_zero_left [RS sym],
+ rule zero_in_subspace, rule zero_in_subspace, rule zero_in_vs);
+
+ show "vectorspace_sum U V <= E";
+ proof (intro subsetI, elim vs_sumD [RS iffD1, elimify] bexE);
+ fix x u v; assume "u : U" "v : V" "x = u [+] v";
+ show "x:E"; by (asm_simp);
+ qed;
+
+ show "ALL x:vectorspace_sum U V. ALL y:vectorspace_sum U V. x [+] y : vectorspace_sum U V";
+ proof (intro ballI, elim vs_sumD [RS iffD1, elimify] bexE, intro vs_sum_I);
+ fix x y ux vx uy vy; assume "ux : U" "vx : V" "x = ux [+] vx" "uy : U" "vy : V" "y = uy [+] vy";
+ show "x [+] y = (ux [+] uy) [+] (vx [+] vy)"; by asm_simp;
+ qed asm_simp+;
+
+ show "ALL x:vectorspace_sum U V. ALL a. a [*] x : vectorspace_sum U V";
+ proof (intro ballI allI, elim vs_sumD [RS iffD1, elimify] bexE, intro vs_sum_I);
+ fix a x u v; assume "u : U" "v : V" "x = u [+] v";
+ show "a [*] x = (a [*] u) [+] (a [*] v)"; by (asm_simp add: vs_add_mult_distrib1 [OF e]);
+ qed asm_simp+;
+qed;
+
+lemma vs_sum_vs:
+ "[| is_subspace U E; is_subspace V E; is_vectorspace E |] ==> is_vectorspace (vectorspace_sum U V)";
+ by (rule subspace_vs [OF vs_sum_subspace]);
+
+
+section {* special case: direct sum of a vectorspace and a linear closure of a vector *};
+
+
+lemma lemma4: "[| 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>"
+ "y1 [+] a1 [*] x0 = y2 [+] a2 [*] x0";
+ have h: "is_vectorspace H"; by (rule subspace_vs);
+ have "y1 [-] y2 = a2 [*] x0 [-] a1 [*] x0";
+ by (rule vs_add_diff_swap) asm_simp+;
+ 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 asm_simp;
+ have x: "(a2 - a1) [*] x0 : lin x0"; by (asm_simp add: lin_def) force;
+ from y; have y': "y1 [-] y2 : lin x0"; by (simp only: eq x);
+ from x; have x': "(a2 - a1) [*] x0 : H"; by (simp only: eq [RS sym] y);
+
+ have int: "H Int (lin x0) = {<0>}";
+ proof;
+ show "H Int lin x0 <= {<0>}";
+ proof (intro subsetI, unfold lin_def, elim IntE CollectD[elimify] exE,
+ rule singleton_iff[RS iffD2]);
+ fix x a; assume "x : H" and ax0: "x = a [*] x0";
+ show "x = <0>";
+ proof (rule case [of "a=0r"]);
+ assume "a = 0r"; show ?thesis; by asm_simp;
+ next;
+ assume "a ~= 0r";
+ have "(rinv a) [*] a [*] x0 : H";
+ by (rule vs_mult_closed [OF h]) asm_simp;
+ also; have "(rinv a) [*] a [*] x0 = x0"; by asm_simp;
+ finally; have "x0 : H"; .;
+ thus ?thesis; by contradiction;
+ qed;
+ qed;
+ show "{<0>} <= H Int lin x0";
+ proof (intro subsetI, elim singletonD[elimify], intro IntI, asm_simp+);
+ show "<0> : H"; by (rule zero_in_vs [OF h]);
+ show "<0> : lin x0"; by (rule zero_in_vs [OF lin_vs]);
+ qed;
+ qed;
+
+ from h; show "y1 = y2";
+ proof (rule vs_add_minus_eq);
+ show "y1 [-] y2 = <0>";
+ by (rule Int_singeltonD [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_singeltonD [OF int x' x]);
+ qed;
+ qed;
+qed;
+
+
+lemma lemma1:
+ "[| 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>";
+ have h: "is_vectorspace H"; by (rule subspace_vs);
+ fix y a; presume t1: "t = y [+] a [*] x0" and "y : H";
+ have "y = t & a = 0r";
+ by (rule lemma4) (assumption+, asm_simp);
+ thus "(y, a) = (t, 0r)"; by asm_simp;
+qed asm_simp+;
+
+
+lemma lemma3: "!! x0 h xi x y a H. [| 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> |]
+ ==> h0 x = h y + a * xi";
+proof -;
+ fix x0 h xi x y a H;
+ 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>";
+
+ have "x : vectorspace_sum H (lin x0)";
+ by (asm_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)";
+ by (asm_simp, rule exI, force);
+ next;
+ fix xa ya;
+ assume "(%(y,a). x = y [+] a [*] x0 & y : H) xa"
+ "(%(y,a). x = y [+] a [*] x0 & y : H) ya";
+ show "xa = ya"; ;
+ proof -;
+ show "fst xa = fst ya & snd xa = snd ya ==> xa = ya";
+ by(rule Pair_fst_snd_eq [RS iffD2]);
+ have x: "x = (fst xa) [+] (snd xa) [*] x0 & (fst xa) : H"; 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 lemma4, asm_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 (asm_simp add: Let_def);
+qed;
+
+
+end;
+
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Real/HahnBanach/Zorn_Lemma.thy Fri Sep 10 17:28:51 1999 +0200
@@ -0,0 +1,33 @@
+
+theory Zorn_Lemma = Zorn:;
+
+
+lemma Zorn's_Lemma: "a:S ==> (!!c. c: chain S ==> EX x. x:c ==> Union c : S) ==>
+ EX y: S. ALL z: S. y <= z --> y = z";
+proof (rule Zorn_Lemma2);
+ assume aS: "a:S";
+ assume r: "!!c. c: chain S ==> EX x. x:c ==> Union c : S";
+ show "ALL c:chain S. EX y:S. ALL z:c. z <= y";
+ proof;
+ fix c; assume "c:chain S";
+ 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={}"]);
+ assume "c={}";
+ show ?thesis; by fast;
+ next;
+ assume "c~={}";
+ show ?thesis;
+ proof;
+ have "EX x. x:c"; by fast;
+ thus "Union c : S"; by (rule s);
+ show "ALL z:c. z <= Union c"; by fast;
+ qed;
+ qed;
+ qed;
+qed;
+
+
+
+end;