# HG changeset patch # User wenzelm # Date 1181773365 -7200 # Node ID 1d138d6bb4613e5fb8974bc68773961c2373b2d7 # Parent 197b6a39592cc9bae6f4d362397af242520c2ab8 tuned proofs: avoid implicit prems; diff -r 197b6a39592c -r 1d138d6bb461 src/HOL/Real/HahnBanach/FunctionNorm.thy --- a/src/HOL/Real/HahnBanach/FunctionNorm.thy Wed Jun 13 19:14:51 2007 +0200 +++ b/src/HOL/Real/HahnBanach/FunctionNorm.thy Thu Jun 14 00:22:45 2007 +0200 @@ -30,7 +30,7 @@ assumes r: "\x. x \ V \ \f x\ \ c * \x\" shows "continuous V norm f" proof - show "linearform V f" . + show "linearform V f" by fact from r have "\c. \x\V. \f x\ \ c * \x\" by blast then show "continuous_axioms V norm f" .. qed @@ -138,7 +138,7 @@ note y_rep also have "\f x\ * inverse \x\ \ (c * \x\) * inverse \x\" proof (rule mult_right_mono) - from c show "\f x\ \ c * \x\" .. + from c x show "\f x\ \ c * \x\" .. from gt have "0 < inverse \x\" by (rule positive_imp_inverse_positive) thus "0 \ inverse \x\" by (rule order_less_imp_le) @@ -164,7 +164,8 @@ shows "b \ \f\\V" proof - have "lub (B V f) (\f\\V)" - by (unfold B_def fn_norm_def) (rule fn_norm_works) + unfolding B_def fn_norm_def + using `continuous V norm f` by (rule fn_norm_works) from this and b show ?thesis .. qed @@ -174,7 +175,8 @@ shows "\f\\V \ y" proof - have "lub (B V f) (\f\\V)" - by (unfold B_def fn_norm_def) (rule fn_norm_works) + unfolding B_def fn_norm_def + using `continuous V norm f` by (rule fn_norm_works) from this and b show ?thesis .. qed @@ -188,7 +190,8 @@ So it is @{text "\ 0"} if all elements in @{text B} are @{text "\ 0"}, provided the supremum exists and @{text B} is not empty. *} have "lub (B V f) (\f\\V)" - by (unfold B_def fn_norm_def) (rule fn_norm_works) + unfolding B_def fn_norm_def + using `continuous V norm f` by (rule fn_norm_works) moreover have "0 \ B V f" .. ultimately show ?thesis .. qed @@ -210,8 +213,9 @@ also have "f 0 = 0" by rule unfold_locales also have "\\\ = 0" by simp also have a: "0 \ \f\\V" - by (unfold B_def fn_norm_def) (rule fn_norm_ge_zero) - have "0 \ norm x" .. + unfolding B_def fn_norm_def + using `continuous V norm f` by (rule fn_norm_ge_zero) + from x have "0 \ norm x" .. with a have "0 \ \f\\V * \x\" by (simp add: zero_le_mult_iff) finally show "\f x\ \ \f\\V * \x\" . next @@ -223,8 +227,8 @@ from x show "0 \ \x\" .. from x and neq have "\f x\ * inverse \x\ \ B V f" by (auto simp add: B_def real_divide_def) - then show "\f x\ * inverse \x\ \ \f\\V" - by (unfold B_def fn_norm_def) (rule fn_norm_ub) + with `continuous V norm f` show "\f x\ * inverse \x\ \ \f\\V" + unfolding B_def fn_norm_def by (rule fn_norm_ub) qed finally show ?thesis . qed @@ -255,7 +259,7 @@ note b_rep also have "\f x\ * inverse \x\ \ (c * \x\) * inverse \x\" proof (rule mult_right_mono) - have "0 < \x\" .. + have "0 < \x\" using x x_neq .. then show "0 \ inverse \x\" by simp from ineq and x show "\f x\ \ c * \x\" .. qed diff -r 197b6a39592c -r 1d138d6bb461 src/HOL/Real/HahnBanach/FunctionOrder.thy --- a/src/HOL/Real/HahnBanach/FunctionOrder.thy Wed Jun 13 19:14:51 2007 +0200 +++ b/src/HOL/Real/HahnBanach/FunctionOrder.thy Thu Jun 14 00:22:45 2007 +0200 @@ -82,13 +82,13 @@ assumes uniq: "\x y z. (x, y) \ g \ (x, z) \ g \ z = y" shows "graph (domain g) (funct g) = g" proof (unfold domain_def funct_def graph_def, auto) (* FIXME !? *) - fix a b assume "(a, b) \ g" - show "(a, SOME y. (a, y) \ g) \ g" by (rule someI2) - show "\y. (a, y) \ g" .. - show "b = (SOME y. (a, y) \ g)" + fix a b assume g: "(a, b) \ g" + from g show "(a, SOME y. (a, y) \ g) \ g" by (rule someI2) + from g show "\y. (a, y) \ g" .. + from g show "b = (SOME y. (a, y) \ g)" proof (rule some_equality [symmetric]) fix y assume "(a, y) \ g" - show "y = b" by (rule uniq) + with g show "y = b" by (rule uniq) qed qed diff -r 197b6a39592c -r 1d138d6bb461 src/HOL/Real/HahnBanach/HahnBanach.thy --- a/src/HOL/Real/HahnBanach/HahnBanach.thy Wed Jun 13 19:14:51 2007 +0200 +++ b/src/HOL/Real/HahnBanach/HahnBanach.thy Thu Jun 14 00:22:45 2007 +0200 @@ -62,8 +62,9 @@ proof - def M \ "norm_pres_extensions E p F f" hence M: "M = \" by (simp only:) - have E: "vectorspace E" . - have F: "vectorspace F" .. + note E = `vectorspace E` + then have F: "vectorspace F" .. + note FE = `F \ E` { fix c assume cM: "c \ chain M" and ex: "\x. x \ c" have "\c \ M" @@ -80,9 +81,9 @@ qed moreover from M cM a have "linearform ?H ?h" by (rule sup_lf) - moreover from a M cM ex have "?H \ E" + moreover from a M cM ex FE E have "?H \ E" by (rule sup_subE) - moreover from a M cM ex have "F \ ?H" + moreover from a M cM ex FE have "F \ ?H" by (rule sup_supF) moreover from a M cM ex have "graph F f \ graph ?H ?h" by (rule sup_ext) @@ -102,14 +103,14 @@ -- {* We show that @{text M} is non-empty: *} show "graph F f \ M" proof (unfold M_def, rule norm_pres_extensionI2) - show "linearform F f" . - show "F \ E" . + show "linearform F f" by fact + show "F \ E" by fact from F show "F \ F" by (rule vectorspace.subspace_refl) show "graph F f \ graph F f" .. - show "\x\F. f x \ p x" . + show "\x\F. f x \ p x" by fact qed qed - then obtain g where gM: "g \ M" and "\x \ M. g \ x \ g = x" + then obtain g where gM: "g \ M" and gx: "\x \ M. g \ x \ g = x" by blast from gM [unfolded M_def] obtain H h where g_rep: "g = graph H h" @@ -120,7 +121,7 @@ -- {* @{text g} is a norm-preserving extension of @{text f}, in other words: *} -- {* @{text g} is the graph of some linear form @{text h} defined on a subspace @{text H} of @{text E}, *} -- {* and @{text h} is an extension of @{text f} that is again bounded by @{text p}. \skp *} - from HE have H: "vectorspace H" + from HE E have H: "vectorspace H" by (rule subspace.vectorspace) have HE_eq: "H = E" @@ -139,7 +140,7 @@ proof assume "x' = 0" with H have "x' \ H" by (simp only: vectorspace.zero) - then show False by contradiction + with `x' \ H` show False by contradiction qed qed @@ -147,12 +148,12 @@ -- {* Define @{text H'} as the direct sum of @{text H} and the linear closure of @{text x'}. \skp *} have HH': "H \ H'" proof (unfold H'_def) - have "vectorspace (lin x')" .. + from x'E have "vectorspace (lin x')" .. with H show "H \ H + lin x'" .. qed obtain xi where - "\y \ H. - p (y + x') - h y \ xi + xi: "\y \ H. - p (y + x') - h y \ xi \ xi \ p (y + x') - h y" -- {* Pick a real number @{text \} that fulfills certain inequations; this will *} -- {* be used to establish that @{text h'} is a norm-preserving extension of @{text h}. @@ -178,7 +179,7 @@ finally have "h v - h u \ p (v + x') + p (u + x')" . then show "- p (u + x') - h u \ p (v + x') - h v" by simp qed - then show ?thesis .. + then show thesis by (blast intro: that) qed def h' \ "\x. let (y, a) = @@ -193,8 +194,8 @@ have "graph H h \ graph H' h'" proof (rule graph_extI) fix t assume t: "t \ H" - have "(SOME (y, a). t = y + a \ x' \ y \ H) = (t, 0)" - by (rule decomp_H'_H) + from E HE t have "(SOME (y, a). t = y + a \ x' \ y \ H) = (t, 0)" + using `x' \ H` `x' \ E` `x' \ 0` by (rule decomp_H'_H) with h'_def show "h t = h' t" by (simp add: Let_def) next from HH' show "H \ H'" .. @@ -216,7 +217,7 @@ hence "(x', h' x') \ graph H' h'" .. with eq have "(x', h' x') \ graph H h" by (simp only:) hence "x' \ H" .. - thus False by contradiction + with `x' \ H` show False by contradiction qed with g_rep show ?thesis by simp qed @@ -226,15 +227,17 @@ proof (unfold M_def) show "graph H' h' \ norm_pres_extensions E p F f" proof (rule norm_pres_extensionI2) - show "linearform H' h'" by (rule h'_lf) + show "linearform H' h'" + using h'_def H'_def HE linearform `x' \ H` `x' \ E` `x' \ 0` E + by (rule h'_lf) show "H' \ E" - proof (unfold H'_def, rule) - show "H \ E" . - show "vectorspace E" . + unfolding H'_def + proof + show "H \ E" by fact + show "vectorspace E" by fact from x'E show "lin x' \ E" .. qed - have "F \ H" . - from H this HH' show FH': "F \ H'" + from H `F \ H` HH' show FH': "F \ H'" by (rule vectorspace.subspace_trans) show "graph F f \ graph H' h'" proof (rule graph_extI) @@ -245,9 +248,12 @@ by (simp add: Let_def) also have "(x, 0) = (SOME (y, a). x = y + a \ x' \ y \ H)" + using E HE proof (rule decomp_H'_H [symmetric]) from FH x show "x \ H" .. from x' show "x' \ 0" . + show "x' \ H" by fact + show "x' \ E" by fact qed also have "(let (y, a) = (SOME (y, a). x = y + a \ x' \ y \ H) @@ -256,14 +262,17 @@ next from FH' show "F \ H'" .. qed - show "\x \ H'. h' x \ p x" by (rule h'_norm_pres) + show "\x \ H'. h' x \ p x" + using h'_def H'_def `x' \ H` `x' \ E` `x' \ 0` E HE + `seminorm E p` linearform and hp xi + by (rule h'_norm_pres) qed qed ultimately show ?thesis .. qed hence "\ (\x \ M. g \ x \ g = x)" by simp -- {* So the graph @{text g} of @{text h} cannot be maximal. Contradiction! \skp *} - then show "H = E" by contradiction + with gx show "H = E" by contradiction qed from HE_eq and linearform have "linearform E h" @@ -303,19 +312,24 @@ \ (\x \ F. g x = f x) \ (\x \ E. \g x\ \ p x)" proof - - have "\g. linearform E g \ (\x \ F. g x = f x) - \ (\x \ E. g x \ p x)" + note E = `vectorspace E` + note FE = `subspace F E` + note sn = `seminorm E p` + note lf = `linearform F f` + have "\g. linearform E g \ (\x \ F. g x = f x) \ (\x \ E. g x \ p x)" + using E FE sn lf proof (rule HahnBanach) show "\x \ F. f x \ p x" - by (rule abs_ineq_iff [THEN iffD1]) + using FE E sn lf and fp by (rule abs_ineq_iff [THEN iffD1]) qed - then obtain g where * : "linearform E g" "\x \ F. g x = f x" - and "\x \ E. g x \ p x" by blast + then obtain g where lg: "linearform E g" and *: "\x \ F. g x = f x" + and **: "\x \ E. g x \ p x" by blast have "\x \ E. \g x\ \ p x" + using _ E sn lg ** proof (rule abs_ineq_iff [THEN iffD2]) show "E \ E" .. qed - with * show ?thesis by blast + with lg * show ?thesis by blast qed @@ -336,14 +350,14 @@ proof - have E: "vectorspace E" by unfold_locales have E_norm: "normed_vectorspace E norm" by rule unfold_locales - have FE: "F \ E" . + note FE = `F \ E` have F: "vectorspace F" by rule unfold_locales - have linearform: "linearform F f" . + note linearform = `linearform F f` have F_norm: "normed_vectorspace F norm" - by (rule subspace_normed_vs) + using FE E_norm by (rule subspace_normed_vs) have ge_zero: "0 \ \f\\F" by (rule normed_vectorspace.fn_norm_ge_zero - [OF F_norm (* continuous.intro*), folded B_def fn_norm_def]) + [OF F_norm `continuous F norm f`, folded B_def fn_norm_def]) txt {* We define a function @{text p} on @{text E} as follows: @{text "p x = \f\ \ \x\"} *} def p \ "\x. \f\\F * \x\" @@ -390,6 +404,7 @@ have "\x \ F. \f x\ \ p x" proof fix x assume "x \ F" + from this and `continuous F norm f` show "\f x\ \ p x" by (unfold p_def) (rule normed_vectorspace.fn_norm_le_cong [OF F_norm, folded B_def fn_norm_def]) @@ -452,7 +467,7 @@ show "\x \ F. \f x\ \ \g\\E * \x\" proof fix x assume x: "x \ F" - from a have "g x = f x" .. + from a x have "g x = f x" .. hence "\f x\ = \g x\" by (simp only:) also from g_cont have "\ \ \g\\E * \x\" @@ -465,7 +480,7 @@ using g_cont by (rule fn_norm_ge_zero [of g, folded B_def fn_norm_def]) next - show "continuous F norm f" . + show "continuous F norm f" by fact qed qed with linearformE a g_cont show ?thesis by blast diff -r 197b6a39592c -r 1d138d6bb461 src/HOL/Real/HahnBanach/HahnBanachExtLemmas.thy --- a/src/HOL/Real/HahnBanach/HahnBanachExtLemmas.thy Wed Jun 13 19:14:51 2007 +0200 +++ b/src/HOL/Real/HahnBanach/HahnBanachExtLemmas.thy Thu Jun 14 00:22:45 2007 +0200 @@ -96,11 +96,12 @@ includes vectorspace E shows "linearform H' h'" proof + note E = `vectorspace E` have H': "vectorspace H'" proof (unfold H'_def) - have "x0 \ E" . - then have "lin x0 \ E" .. - with HE show "vectorspace (H + lin x0)" .. + from `x0 \ E` + have "lin x0 \ E" .. + with HE show "vectorspace (H + lin x0)" using E .. qed { fix x1 x2 assume x1: "x1 \ H'" and x2: "x2 \ H'" @@ -114,7 +115,7 @@ and x2_rep: "x2 = y2 + a2 \ x0" and y2: "y2 \ H" by (unfold H'_def sum_def lin_def) blast - have ya: "y1 + y2 = y \ a1 + a2 = a" using _ HE _ y x0 + have ya: "y1 + y2 = y \ a1 + a2 = a" using E HE _ y x0 proof (rule decomp_H') txt_raw {* \label{decomp-H-use} *} from HE y1 y2 show "y1 + y2 \ H" by (rule subspace.add_closed) @@ -126,7 +127,7 @@ finally show "(y1 + y2) + (a1 + a2) \ x0 = y + a \ x0" . qed - from h'_def x1x2 _ HE y x0 + from h'_def x1x2 E HE y x0 have "h' (x1 + x2) = h y + a * xi" by (rule h'_definite) also have "\ = h (y1 + y2) + (a1 + a2) * xi" @@ -135,10 +136,10 @@ by simp also have "\ + (a1 + a2) * xi = (h y1 + a1 * xi) + (h y2 + a2 * xi)" by (simp add: left_distrib) - also from h'_def x1_rep _ HE y1 x0 + also from h'_def x1_rep E HE y1 x0 have "h y1 + a1 * xi = h' x1" by (rule h'_definite [symmetric]) - also from h'_def x2_rep _ HE y2 x0 + also from h'_def x2_rep E HE y2 x0 have "h y2 + a2 * xi = h' x2" by (rule h'_definite [symmetric]) finally show ?thesis . @@ -154,7 +155,7 @@ and x1_rep: "x1 = y1 + a1 \ x0" and y1: "y1 \ H" by (unfold H'_def sum_def lin_def) blast - have ya: "c \ y1 = y \ c * a1 = a" using _ HE _ y x0 + have ya: "c \ y1 = y \ c * a1 = a" using E HE _ y x0 proof (rule decomp_H') from HE y1 show "c \ y1 \ H" by (rule subspace.mult_closed) @@ -166,7 +167,7 @@ finally show "c \ y1 + (c * a1) \ x0 = y + a \ x0" . qed - from h'_def cx1_rep _ HE y x0 have "h' (c \ x1) = h y + a * xi" + from h'_def cx1_rep E HE y x0 have "h' (c \ x1) = h y + a * xi" by (rule h'_definite) also have "\ = h (c \ y1) + (c * a1) * xi" by (simp only: ya) @@ -174,7 +175,7 @@ by simp also have "\ + (c * a1) * xi = c * (h y1 + a1 * xi)" by (simp only: right_distrib) - also from h'_def x1_rep _ HE y1 x0 have "h y1 + a1 * xi = h' x1" + also from h'_def x1_rep E HE y1 x0 have "h y1 + a1 * xi = h' x1" by (rule h'_definite [symmetric]) finally show ?thesis . qed @@ -195,6 +196,8 @@ and a': "\y \ H. - p (y + x0) - h y \ xi \ xi \ p (y + x0) - h y" shows "\x \ H'. h' x \ p x" proof + note E = `vectorspace E` + note HE = `subspace H E` fix x assume x': "x \ H'" show "h' x \ p x" proof - @@ -206,7 +209,7 @@ from y have y': "y \ E" .. from y have ay: "inverse a \ y \ H" by simp - from h'_def x_rep _ _ y x0 have "h' x = h y + a * xi" + from h'_def x_rep E HE y x0 have "h' x = h y + a * xi" by (rule h'_definite) also have "\ \ p (y + a \ x0)" proof (rule linorder_cases) diff -r 197b6a39592c -r 1d138d6bb461 src/HOL/Real/HahnBanach/HahnBanachSupLemmas.thy --- a/src/HOL/Real/HahnBanach/HahnBanachSupLemmas.thy Wed Jun 13 19:14:51 2007 +0200 +++ b/src/HOL/Real/HahnBanach/HahnBanachSupLemmas.thy Thu Jun 14 00:22:45 2007 +0200 @@ -126,13 +126,13 @@ @{text x} and @{text y} are contained in the greater one. \label{cases1}*} - from cM have "graph H'' h'' \ graph H' h' \ graph H' h' \ graph H'' h''" + from cM c'' c' have "graph H'' h'' \ graph H' h' \ graph H' h' \ graph H'' h''" (is "?case1 \ ?case2") .. then show ?thesis proof assume ?case1 - have "(x, h x) \ graph H'' h''" . - also have "... \ graph H' h'" . + have "(x, h x) \