# HG changeset patch # User wenzelm # Date 936977331 -7200 # Node ID 599d3414b51d6b760b21bc7e5159bf5454e234e7 # Parent 30344dde83abb88febc53c59f83c6278536b8dc3 The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar) (by Gertrud Bauer, TU Munich); diff -r 30344dde83ab -r 599d3414b51d src/HOL/IsaMakefile --- 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 diff -r 30344dde83ab -r 599d3414b51d src/HOL/Real/HahnBanach/Aux.thy --- /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 diff -r 30344dde83ab -r 599d3414b51d src/HOL/Real/HahnBanach/Bounds.thy --- /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; diff -r 30344dde83ab -r 599d3414b51d src/HOL/Real/HahnBanach/FunctionNorm.thy --- /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; + diff -r 30344dde83ab -r 599d3414b51d src/HOL/Real/HahnBanach/FunctionOrder.thy --- /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; + diff -r 30344dde83ab -r 599d3414b51d src/HOL/Real/HahnBanach/HahnBanach.thy --- /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; diff -r 30344dde83ab -r 599d3414b51d src/HOL/Real/HahnBanach/HahnBanach_h0_lemmas.thy --- /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 diff -r 30344dde83ab -r 599d3414b51d src/HOL/Real/HahnBanach/HahnBanach_lemmas.thy --- /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 diff -r 30344dde83ab -r 599d3414b51d src/HOL/Real/HahnBanach/LinearSpace.thy --- /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 diff -r 30344dde83ab -r 599d3414b51d src/HOL/Real/HahnBanach/Linearform.thy --- /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; + diff -r 30344dde83ab -r 599d3414b51d src/HOL/Real/HahnBanach/NormedSpace.thy --- /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; + diff -r 30344dde83ab -r 599d3414b51d src/HOL/Real/HahnBanach/ROOT.ML --- /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"; diff -r 30344dde83ab -r 599d3414b51d src/HOL/Real/HahnBanach/Subspace.thy --- /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; + + diff -r 30344dde83ab -r 599d3414b51d src/HOL/Real/HahnBanach/Zorn_Lemma.thy --- /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;