# HG changeset patch # User wenzelm # Date 1216143577 -7200 # Node ID d3eb431db03597ea61596b96c2564ea5105fafe4 # Parent 2c01c0bdb385303fca5891f3e31933e4cd5b4d0c modernized specifications and proofs; tuned document; diff -r 2c01c0bdb385 -r d3eb431db035 src/HOL/Real/HahnBanach/Bounds.thy --- a/src/HOL/Real/HahnBanach/Bounds.thy Tue Jul 15 16:50:09 2008 +0200 +++ b/src/HOL/Real/HahnBanach/Bounds.thy Tue Jul 15 19:39:37 2008 +0200 @@ -28,7 +28,8 @@ shows "\A = (x::'a::order)" proof - interpret lub [A x] by fact - show ?thesis proof (unfold the_lub_def) + show ?thesis + proof (unfold the_lub_def) from `lub A x` show "The (lub A) = x" proof fix x' assume lub': "lub A x'" @@ -73,7 +74,7 @@ shows "\x. lub A x" proof - from ex_upper have "\y. isUb UNIV A y" - by (unfold isUb_def setle_def) blast + unfolding isUb_def setle_def by blast with nonempty have "\x. isLub UNIV A x" by (rule reals_complete) then show ?thesis by (simp only: lub_compat) diff -r 2c01c0bdb385 -r d3eb431db035 src/HOL/Real/HahnBanach/FunctionNorm.thy --- a/src/HOL/Real/HahnBanach/FunctionNorm.thy Tue Jul 15 16:50:09 2008 +0200 +++ b/src/HOL/Real/HahnBanach/FunctionNorm.thy Tue Jul 15 19:39:37 2008 +0200 @@ -5,7 +5,9 @@ header {* The norm of a function *} -theory FunctionNorm imports NormedSpace FunctionOrder begin +theory FunctionNorm +imports NormedSpace FunctionOrder +begin subsection {* Continuous linear forms*} @@ -97,7 +99,7 @@ proof (rule real_complete) txt {* First we have to show that @{text B} is non-empty: *} have "0 \ B V f" .. - thus "\x. x \ B V f" .. + then show "\x. x \ B V f" .. txt {* Then we have to show that @{text B} is bounded: *} show "\c. \y \ B V f. y \ c" @@ -116,7 +118,7 @@ show "y \ b" proof cases assume "y = 0" - thus ?thesis by (unfold b_def) arith + then show ?thesis unfolding b_def by arith next txt {* The second case is @{text "y = \f x\ / \x\"} for some @{text "x \ V"} with @{text "x \ 0"}. *} @@ -135,21 +137,21 @@ 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) + then show "0 \ inverse \x\" by (rule order_less_imp_le) qed also have "\ = c * (\x\ * inverse \x\)" by (rule real_mult_assoc) also from gt have "\x\ \ 0" by simp - hence "\x\ * inverse \x\ = 1" by simp + then have "\x\ * inverse \x\ = 1" by simp also have "c * 1 \ b" by (simp add: b_def le_maxI1) finally show "y \ b" . qed qed - thus ?thesis .. + then show ?thesis .. qed qed - then show ?thesis by (unfold fn_norm_def) (rule the_lubI_ex) + then show ?thesis unfolding fn_norm_def by (rule the_lubI_ex) qed lemma (in normed_vectorspace_with_fn_norm) fn_norm_ub [iff?]: @@ -185,7 +187,6 @@ 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)" -(* 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 .. @@ -205,7 +206,8 @@ proof - interpret continuous [V norm f] by fact interpret linearform [V f] . - show ?thesis proof cases + show ?thesis + proof cases assume "x = 0" then have "\f x\ = \f 0\" by simp also have "f 0 = 0" by rule unfold_locales @@ -245,7 +247,8 @@ shows "\f\\V \ c" proof - interpret continuous [V norm f] by fact - show ?thesis proof (rule fn_norm_leastB [folded B_def fn_norm_def]) + show ?thesis + proof (rule fn_norm_leastB [folded B_def fn_norm_def]) fix b assume b: "b \ B V f" show "b \ c" proof cases diff -r 2c01c0bdb385 -r d3eb431db035 src/HOL/Real/HahnBanach/FunctionOrder.thy --- a/src/HOL/Real/HahnBanach/FunctionOrder.thy Tue Jul 15 16:50:09 2008 +0200 +++ b/src/HOL/Real/HahnBanach/FunctionOrder.thy Tue Jul 15 19:39:37 2008 +0200 @@ -5,7 +5,9 @@ header {* An order on functions *} -theory FunctionOrder imports Subspace Linearform begin +theory FunctionOrder +imports Subspace Linearform +begin subsection {* The graph of a function *} @@ -27,14 +29,14 @@ "graph F f = {(x, f x) | x. x \ F}" lemma graphI [intro]: "x \ F \ (x, f x) \ graph F f" - by (unfold graph_def) blast + unfolding graph_def by blast lemma graphI2 [intro?]: "x \ F \ \t \ graph F f. t = (x, f x)" - by (unfold graph_def) blast + unfolding graph_def by blast lemma graphE [elim?]: "(x, y) \ graph F f \ (x \ F \ y = f x \ C) \ C" - by (unfold graph_def) blast + unfolding graph_def by blast subsection {* Functions ordered by domain extension *} @@ -47,15 +49,15 @@ lemma graph_extI: "(\x. x \ H \ h x = h' x) \ H \ H' \ graph H h \ graph H' h'" - by (unfold graph_def) blast + unfolding graph_def by blast lemma graph_extD1 [dest?]: "graph H h \ graph H' h' \ x \ H \ h x = h' x" - by (unfold graph_def) blast + unfolding graph_def by blast lemma graph_extD2 [dest?]: "graph H h \ graph H' h' \ H \ H'" - by (unfold graph_def) blast + unfolding graph_def by blast subsection {* Domain and function of a graph *} @@ -81,7 +83,8 @@ lemma graph_domain_funct: 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 !? *) + unfolding domain_def funct_def graph_def +proof auto (* FIXME !? *) 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" .. @@ -119,13 +122,13 @@ \ (\H h. g = graph H h \ linearform H h \ H \ E \ F \ H \ graph F f \ graph H h \ \x \ H. h x \ p x \ C) \ C" - by (unfold norm_pres_extensions_def) blast + unfolding norm_pres_extensions_def by blast lemma norm_pres_extensionI2 [intro]: "linearform H h \ H \ E \ F \ H \ graph F f \ graph H h \ \x \ H. h x \ p x \ graph H h \ norm_pres_extensions E p F f" - by (unfold norm_pres_extensions_def) blast + unfolding norm_pres_extensions_def by blast lemma norm_pres_extensionI: (* FIXME ? *) "\H h. g = graph H h @@ -134,6 +137,6 @@ \ F \ H \ graph F f \ graph H h \ (\x \ H. h x \ p x) \ g \ norm_pres_extensions E p F f" - by (unfold norm_pres_extensions_def) blast + unfolding norm_pres_extensions_def by blast end diff -r 2c01c0bdb385 -r d3eb431db035 src/HOL/Real/HahnBanach/HahnBanach.thy --- a/src/HOL/Real/HahnBanach/HahnBanach.thy Tue Jul 15 16:50:09 2008 +0200 +++ b/src/HOL/Real/HahnBanach/HahnBanach.thy Tue Jul 15 19:39:37 2008 +0200 @@ -5,7 +5,9 @@ header {* The Hahn-Banach Theorem *} -theory HahnBanach imports HahnBanachLemmas begin +theory HahnBanach +imports HahnBanachLemmas +begin text {* We present the proof of two different versions of the Hahn-Banach @@ -66,7 +68,7 @@ interpret seminorm [E p] by fact interpret linearform [F f] by fact def M \ "norm_pres_extensions E p F f" - hence M: "M = \" by (simp only:) + then have M: "M = \" by (simp only:) from E have F: "vectorspace F" .. note FE = `F \ E` { @@ -74,7 +76,8 @@ have "\c \ M" -- {* Show that every non-empty chain @{text c} of @{text M} has an upper bound in @{text M}: *} -- {* @{text "\c"} is greater than any element of the chain @{text c}, so it suffices to show @{text "\c \ M"}. *} - proof (unfold M_def, rule norm_pres_extensionI) + unfolding M_def + proof (rule norm_pres_extensionI) let ?H = "domain (\c)" let ?h = "funct (\c)" @@ -101,12 +104,13 @@ \ (\x \ H. h x \ p x)" by blast qed } - hence "\g \ M. \x \ M. g \ x \ g = x" + then have "\g \ M. \x \ M. g \ x \ g = x" -- {* With Zorn's Lemma we can conclude that there is a maximal element in @{text M}. \skp *} proof (rule Zorn's_Lemma) -- {* We show that @{text M} is non-empty: *} show "graph F f \ M" - proof (unfold M_def, rule norm_pres_extensionI2) + unfolding M_def + proof (rule norm_pres_extensionI2) show "linearform F f" by fact show "F \ E" by fact from F show "F \ F" by (rule vectorspace.subspace_refl) @@ -116,12 +120,12 @@ qed 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 + from gM obtain H h where g_rep: "g = graph H h" and linearform: "linearform H h" and HE: "H \ E" and FH: "F \ H" and graphs: "graph F f \ graph H h" - and hp: "\x \ H. h x \ p x" .. + and hp: "\x \ H. h x \ p x" unfolding M_def .. -- {* @{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 *} @@ -213,14 +217,15 @@ proof assume eq: "graph H h = graph H' h'" have "x' \ H'" - proof (unfold H'_def, rule) + unfolding H'_def + proof from H show "0 \ H" by (rule vectorspace.zero) from x'E show "x' \ lin x'" by (rule x_lin_x) from x'E show "x' = 0 + x'" by simp qed - hence "(x', h' x') \ graph H' h'" .. + then have "(x', h' x') \ graph H' h'" .. with eq have "(x', h' x') \ graph H h" by (simp only:) - hence "x' \ H" .. + then have "x' \ H" .. with `x' \ H` show False by contradiction qed with g_rep show ?thesis by simp @@ -252,7 +257,7 @@ by (simp add: Let_def) also have "(x, 0) = (SOME (y, a). x = y + a \ x' \ y \ H)" - using E HE + using E HE proof (rule decomp_H'_H [symmetric]) from FH x show "x \ H" .. from x' show "x' \ 0" . @@ -274,7 +279,7 @@ qed ultimately show ?thesis .. qed - hence "\ (\x \ M. g \ x \ g = x)" by simp + then have "\ (\x \ M. g \ x \ g = x)" by simp -- {* So the graph @{text g} of @{text h} cannot be maximal. Contradiction! \skp *} with gx show "H = E" by contradiction qed @@ -321,12 +326,8 @@ interpret subspace [F E] by fact interpret linearform [F f] by fact interpret seminorm [E p] by fact -(* 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 + 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" using FE E sn lf and fp by (rule abs_ineq_iff [THEN iffD1]) @@ -334,7 +335,7 @@ 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 ** + using _ E sn lg ** proof (rule abs_ineq_iff [THEN iffD2]) show "E \ E" .. qed @@ -384,10 +385,10 @@ have q: "seminorm E p" proof fix x y a assume x: "x \ E" and y: "y \ E" - + txt {* @{text p} is positive definite: *} - have "0 \ \f\\F" by (rule ge_zero) - moreover from x have "0 \ \x\" .. + have "0 \ \f\\F" by (rule ge_zero) + moreover from x have "0 \ \x\" .. ultimately show "0 \ p x" by (simp add: p_def zero_le_mult_iff) @@ -422,9 +423,9 @@ have "\x \ F. \f x\ \ p x" proof fix x assume "x \ F" - from this and `continuous F norm f` + with `continuous F norm f` and linearform show "\f x\ \ p x" - by (unfold p_def) (rule normed_vectorspace_with_fn_norm.fn_norm_le_cong + unfolding p_def by (rule normed_vectorspace_with_fn_norm.fn_norm_le_cong [OF normed_vectorspace_with_fn_norm.intro, OF F_norm, folded B_def fn_norm_def]) qed @@ -435,9 +436,9 @@ some function @{text g} on the whole vector space @{text E}. *} with E FE linearform q obtain g where - linearformE: "linearform E g" - and a: "\x \ F. g x = f x" - and b: "\x \ E. \g x\ \ p x" + linearformE: "linearform E g" + and a: "\x \ F. g x = f x" + and b: "\x \ E. \g x\ \ p x" by (rule abs_HahnBanach [elim_format]) iprover txt {* We furthermore have to show that @{text g} is also continuous: *} @@ -489,7 +490,7 @@ proof fix x assume x: "x \ F" from a x have "g x = f x" .. - hence "\f x\ = \g x\" by (simp only:) + then have "\f x\ = \g x\" by (simp only:) also from g_cont have "\ \ \g\\E * \x\" proof (rule fn_norm_le_cong [of g, folded B_def fn_norm_def]) @@ -500,7 +501,6 @@ show "0 \ \g\\E" using g_cont by (rule fn_norm_ge_zero [of g, folded B_def fn_norm_def]) - next show "continuous F norm f" by fact qed qed diff -r 2c01c0bdb385 -r d3eb431db035 src/HOL/Real/HahnBanach/HahnBanachExtLemmas.thy --- a/src/HOL/Real/HahnBanach/HahnBanachExtLemmas.thy Tue Jul 15 16:50:09 2008 +0200 +++ b/src/HOL/Real/HahnBanach/HahnBanachExtLemmas.thy Tue Jul 15 19:39:37 2008 +0200 @@ -5,7 +5,9 @@ header {* Extending non-maximal functions *} -theory HahnBanachExtLemmas imports FunctionNorm begin +theory HahnBanachExtLemmas +imports FunctionNorm +begin text {* In this section the following context is presumed. Let @{text E} be @@ -98,7 +100,8 @@ proof - interpret linearform [H h] by fact interpret vectorspace [E] by fact - show ?thesis proof + show ?thesis + proof note E = `vectorspace E` have H': "vectorspace H'" proof (unfold H'_def) @@ -116,7 +119,7 @@ x1x2: "x1 + x2 = y + a \ x0" and y: "y \ H" and x1_rep: "x1 = y1 + a1 \ x0" and y1: "y1 \ H" and x2_rep: "x2 = y2 + a2 \ x0" and y2: "y2 \ H" - by (unfold H'_def sum_def lin_def) blast + unfolding H'_def sum_def lin_def by blast have ya: "y1 + y2 = y \ a1 + a2 = a" using E HE _ y x0 proof (rule decomp_H') txt_raw {* \label{decomp-H-use} *} @@ -154,9 +157,9 @@ from H' x1 have ax1: "c \ x1 \ H'" by (rule vectorspace.mult_closed) with x1 obtain y a y1 a1 where - cx1_rep: "c \ x1 = y + a \ x0" and y: "y \ H" + cx1_rep: "c \ x1 = y + a \ x0" and y: "y \ H" and x1_rep: "x1 = y1 + a1 \ x0" and y1: "y1 \ H" - by (unfold H'_def sum_def lin_def) blast + unfolding H'_def sum_def lin_def by blast have ya: "c \ y1 = y \ c * a1 = a" using E HE _ y x0 proof (rule decomp_H') @@ -204,15 +207,16 @@ interpret subspace [H E] by fact interpret seminorm [E p] by fact interpret linearform [H h] by fact - show ?thesis proof + show ?thesis + proof fix x assume x': "x \ H'" show "h' x \ p x" proof - from a' have a1: "\ya \ H. - p (ya + x0) - h ya \ xi" and a2: "\ya \ H. xi \ p (ya + x0) - h ya" by auto from x' obtain y a where - x_rep: "x = y + a \ x0" and y: "y \ H" - by (unfold H'_def sum_def lin_def) blast + x_rep: "x = y + a \ x0" and y: "y \ H" + unfolding H'_def sum_def lin_def by blast from y have y': "y \ E" .. from y have ay: "inverse a \ y \ H" by simp @@ -228,7 +232,7 @@ next txt {* In the case @{text "a < 0"}, we use @{text "a\<^sub>1"} with @{text ya} taken as @{text "y / a"}: *} - assume lz: "a < 0" hence nz: "a \ 0" by simp + assume lz: "a < 0" then have nz: "a \ 0" by simp from a1 ay have "- p (inverse a \ y + x0) - h (inverse a \ y) \ xi" .. with lz have "a * xi \ @@ -250,13 +254,13 @@ next txt {* In the case @{text "a > 0"}, we use @{text "a\<^sub>2"} with @{text ya} taken as @{text "y / a"}: *} - assume gz: "0 < a" hence nz: "a \ 0" by simp + assume gz: "0 < a" then have nz: "a \ 0" by simp from a2 ay have "xi \ p (inverse a \ y + x0) - h (inverse a \ y)" .. with gz have "a * xi \ a * (p (inverse a \ y + x0) - h (inverse a \ y))" by simp - also have "... = a * p (inverse a \ y + x0) - a * h (inverse a \ y)" + also have "\ = a * p (inverse a \ y + x0) - a * h (inverse a \ y)" by (simp add: right_diff_distrib) also from gz x0 y' have "a * p (inverse a \ y + x0) = p (a \ (inverse a \ y + x0))" diff -r 2c01c0bdb385 -r d3eb431db035 src/HOL/Real/HahnBanach/HahnBanachSupLemmas.thy --- a/src/HOL/Real/HahnBanach/HahnBanachSupLemmas.thy Tue Jul 15 16:50:09 2008 +0200 +++ b/src/HOL/Real/HahnBanach/HahnBanachSupLemmas.thy Tue Jul 15 19:39:37 2008 +0200 @@ -5,7 +5,9 @@ header {* The supremum w.r.t.~the function order *} -theory HahnBanachSupLemmas imports FunctionNorm ZornLemma begin +theory HahnBanachSupLemmas +imports FunctionNorm ZornLemma +begin text {* This section contains some lemmas that will be used in the proof of @@ -132,7 +134,7 @@ proof assume ?case1 have "(x, h x) \ graph H'' h''" by fact - also have "... \ graph H' h'" by fact + also have "\ \ graph H' h'" by fact finally have xh:"(x, h x) \ graph H' h'" . then have "x \ H'" .. moreover from y_hy have "y \ H'" .. @@ -171,11 +173,11 @@ from G1 c have "G1 \ M" .. then obtain H1 h1 where G1_rep: "G1 = graph H1 h1" - by (unfold M_def) blast + unfolding M_def by blast from G2 c have "G2 \ M" .. then obtain H2 h2 where G2_rep: "G2 = graph H2 h2" - by (unfold M_def) blast + unfolding M_def by blast txt {* @{text "G\<^sub>1"} is contained in @{text "G\<^sub>2"} or vice versa, since both @{text "G\<^sub>1"} and @{text @@ -186,18 +188,18 @@ proof assume ?case1 with xy' G2_rep have "(x, y) \ graph H2 h2" by blast - hence "y = h2 x" .. + then have "y = h2 x" .. also from xz' G2_rep have "(x, z) \ graph H2 h2" by (simp only:) - hence "z = h2 x" .. + then have "z = h2 x" .. finally show ?thesis . next assume ?case2 with xz' G1_rep have "(x, z) \ graph H1 h1" by blast - hence "z = h1 x" .. + then have "z = h1 x" .. also from xy' G1_rep have "(x, y) \ graph H1 h1" by (simp only:) - hence "y = h1 x" .. + then have "y = h1 x" .. finally show ?thesis .. qed qed diff -r 2c01c0bdb385 -r d3eb431db035 src/HOL/Real/HahnBanach/Linearform.thy --- a/src/HOL/Real/HahnBanach/Linearform.thy Tue Jul 15 16:50:09 2008 +0200 +++ b/src/HOL/Real/HahnBanach/Linearform.thy Tue Jul 15 19:39:37 2008 +0200 @@ -5,7 +5,9 @@ header {* Linearforms *} -theory Linearform imports VectorSpace begin +theory Linearform +imports VectorSpace +begin text {* A \emph{linear form} is a function on a vector space into the reals @@ -25,9 +27,9 @@ proof - interpret vectorspace [V] by fact assume x: "x \ V" - hence "f (- x) = f ((- 1) \ x)" by (simp add: negate_eq1) - also from x have "... = (- 1) * (f x)" by (rule mult) - also from x have "... = - (f x)" by simp + then have "f (- x) = f ((- 1) \ x)" by (simp add: negate_eq1) + also from x have "\ = (- 1) * (f x)" by (rule mult) + also from x have "\ = - (f x)" by simp finally show ?thesis . qed @@ -37,8 +39,8 @@ proof - interpret vectorspace [V] by fact assume x: "x \ V" and y: "y \ V" - hence "x - y = x + - y" by (rule diff_eq1) - also have "f ... = f x + f (- y)" by (rule add) (simp_all add: x y) + then have "x - y = x + - y" by (rule diff_eq1) + also have "f \ = f x + f (- y)" by (rule add) (simp_all add: x y) also have "f (- y) = - f y" using `vectorspace V` y by (rule neg) finally show ?thesis by simp qed diff -r 2c01c0bdb385 -r d3eb431db035 src/HOL/Real/HahnBanach/NormedSpace.thy --- a/src/HOL/Real/HahnBanach/NormedSpace.thy Tue Jul 15 16:50:09 2008 +0200 +++ b/src/HOL/Real/HahnBanach/NormedSpace.thy Tue Jul 15 19:39:37 2008 +0200 @@ -5,7 +5,9 @@ header {* Normed vector spaces *} -theory NormedSpace imports Subspace begin +theory NormedSpace +imports Subspace +begin subsection {* Quasinorms *} @@ -32,7 +34,7 @@ proof - interpret vectorspace [V] by fact assume x: "x \ V" and y: "y \ V" - hence "x - y = x + - 1 \ y" + then have "x - y = x + - 1 \ y" by (simp add: diff_eq2 negate_eq2a) also from x y have "\\\ \ \x\ + \- 1 \ y\" by (simp add: subadditive) @@ -48,7 +50,7 @@ proof - interpret vectorspace [V] by fact assume x: "x \ V" - hence "- x = - 1 \ x" by (simp only: negate_eq1) + then have "- x = - 1 \ x" by (simp only: negate_eq1) also from x have "\\\ = \- 1\ * \x\