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