author | wenzelm |

Thu Jun 14 00:22:45 2007 +0200 (2007-06-14) | |

changeset 23378 | 1d138d6bb461 |

parent 23377 | 197b6a39592c |

child 23379 | d0e3f790bd73 |

tuned proofs: avoid implicit prems;

1.1 --- a/src/HOL/Real/HahnBanach/FunctionNorm.thy Wed Jun 13 19:14:51 2007 +0200 1.2 +++ b/src/HOL/Real/HahnBanach/FunctionNorm.thy Thu Jun 14 00:22:45 2007 +0200 1.3 @@ -30,7 +30,7 @@ 1.4 assumes r: "\<And>x. x \<in> V \<Longrightarrow> \<bar>f x\<bar> \<le> c * \<parallel>x\<parallel>" 1.5 shows "continuous V norm f" 1.6 proof 1.7 - show "linearform V f" . 1.8 + show "linearform V f" by fact 1.9 from r have "\<exists>c. \<forall>x\<in>V. \<bar>f x\<bar> \<le> c * \<parallel>x\<parallel>" by blast 1.10 then show "continuous_axioms V norm f" .. 1.11 qed 1.12 @@ -138,7 +138,7 @@ 1.13 note y_rep 1.14 also have "\<bar>f x\<bar> * inverse \<parallel>x\<parallel> \<le> (c * \<parallel>x\<parallel>) * inverse \<parallel>x\<parallel>" 1.15 proof (rule mult_right_mono) 1.16 - from c show "\<bar>f x\<bar> \<le> c * \<parallel>x\<parallel>" .. 1.17 + from c x show "\<bar>f x\<bar> \<le> c * \<parallel>x\<parallel>" .. 1.18 from gt have "0 < inverse \<parallel>x\<parallel>" 1.19 by (rule positive_imp_inverse_positive) 1.20 thus "0 \<le> inverse \<parallel>x\<parallel>" by (rule order_less_imp_le) 1.21 @@ -164,7 +164,8 @@ 1.22 shows "b \<le> \<parallel>f\<parallel>\<hyphen>V" 1.23 proof - 1.24 have "lub (B V f) (\<parallel>f\<parallel>\<hyphen>V)" 1.25 - by (unfold B_def fn_norm_def) (rule fn_norm_works) 1.26 + unfolding B_def fn_norm_def 1.27 + using `continuous V norm f` by (rule fn_norm_works) 1.28 from this and b show ?thesis .. 1.29 qed 1.30 1.31 @@ -174,7 +175,8 @@ 1.32 shows "\<parallel>f\<parallel>\<hyphen>V \<le> y" 1.33 proof - 1.34 have "lub (B V f) (\<parallel>f\<parallel>\<hyphen>V)" 1.35 - by (unfold B_def fn_norm_def) (rule fn_norm_works) 1.36 + unfolding B_def fn_norm_def 1.37 + using `continuous V norm f` by (rule fn_norm_works) 1.38 from this and b show ?thesis .. 1.39 qed 1.40 1.41 @@ -188,7 +190,8 @@ 1.42 So it is @{text "\<ge> 0"} if all elements in @{text B} are @{text "\<ge> 1.43 0"}, provided the supremum exists and @{text B} is not empty. *} 1.44 have "lub (B V f) (\<parallel>f\<parallel>\<hyphen>V)" 1.45 - by (unfold B_def fn_norm_def) (rule fn_norm_works) 1.46 + unfolding B_def fn_norm_def 1.47 + using `continuous V norm f` by (rule fn_norm_works) 1.48 moreover have "0 \<in> B V f" .. 1.49 ultimately show ?thesis .. 1.50 qed 1.51 @@ -210,8 +213,9 @@ 1.52 also have "f 0 = 0" by rule unfold_locales 1.53 also have "\<bar>\<dots>\<bar> = 0" by simp 1.54 also have a: "0 \<le> \<parallel>f\<parallel>\<hyphen>V" 1.55 - by (unfold B_def fn_norm_def) (rule fn_norm_ge_zero) 1.56 - have "0 \<le> norm x" .. 1.57 + unfolding B_def fn_norm_def 1.58 + using `continuous V norm f` by (rule fn_norm_ge_zero) 1.59 + from x have "0 \<le> norm x" .. 1.60 with a have "0 \<le> \<parallel>f\<parallel>\<hyphen>V * \<parallel>x\<parallel>" by (simp add: zero_le_mult_iff) 1.61 finally show "\<bar>f x\<bar> \<le> \<parallel>f\<parallel>\<hyphen>V * \<parallel>x\<parallel>" . 1.62 next 1.63 @@ -223,8 +227,8 @@ 1.64 from x show "0 \<le> \<parallel>x\<parallel>" .. 1.65 from x and neq have "\<bar>f x\<bar> * inverse \<parallel>x\<parallel> \<in> B V f" 1.66 by (auto simp add: B_def real_divide_def) 1.67 - then show "\<bar>f x\<bar> * inverse \<parallel>x\<parallel> \<le> \<parallel>f\<parallel>\<hyphen>V" 1.68 - by (unfold B_def fn_norm_def) (rule fn_norm_ub) 1.69 + with `continuous V norm f` show "\<bar>f x\<bar> * inverse \<parallel>x\<parallel> \<le> \<parallel>f\<parallel>\<hyphen>V" 1.70 + unfolding B_def fn_norm_def by (rule fn_norm_ub) 1.71 qed 1.72 finally show ?thesis . 1.73 qed 1.74 @@ -255,7 +259,7 @@ 1.75 note b_rep 1.76 also have "\<bar>f x\<bar> * inverse \<parallel>x\<parallel> \<le> (c * \<parallel>x\<parallel>) * inverse \<parallel>x\<parallel>" 1.77 proof (rule mult_right_mono) 1.78 - have "0 < \<parallel>x\<parallel>" .. 1.79 + have "0 < \<parallel>x\<parallel>" using x x_neq .. 1.80 then show "0 \<le> inverse \<parallel>x\<parallel>" by simp 1.81 from ineq and x show "\<bar>f x\<bar> \<le> c * \<parallel>x\<parallel>" .. 1.82 qed

2.1 --- a/src/HOL/Real/HahnBanach/FunctionOrder.thy Wed Jun 13 19:14:51 2007 +0200 2.2 +++ b/src/HOL/Real/HahnBanach/FunctionOrder.thy Thu Jun 14 00:22:45 2007 +0200 2.3 @@ -82,13 +82,13 @@ 2.4 assumes uniq: "\<And>x y z. (x, y) \<in> g \<Longrightarrow> (x, z) \<in> g \<Longrightarrow> z = y" 2.5 shows "graph (domain g) (funct g) = g" 2.6 proof (unfold domain_def funct_def graph_def, auto) (* FIXME !? *) 2.7 - fix a b assume "(a, b) \<in> g" 2.8 - show "(a, SOME y. (a, y) \<in> g) \<in> g" by (rule someI2) 2.9 - show "\<exists>y. (a, y) \<in> g" .. 2.10 - show "b = (SOME y. (a, y) \<in> g)" 2.11 + fix a b assume g: "(a, b) \<in> g" 2.12 + from g show "(a, SOME y. (a, y) \<in> g) \<in> g" by (rule someI2) 2.13 + from g show "\<exists>y. (a, y) \<in> g" .. 2.14 + from g show "b = (SOME y. (a, y) \<in> g)" 2.15 proof (rule some_equality [symmetric]) 2.16 fix y assume "(a, y) \<in> g" 2.17 - show "y = b" by (rule uniq) 2.18 + with g show "y = b" by (rule uniq) 2.19 qed 2.20 qed 2.21

3.1 --- a/src/HOL/Real/HahnBanach/HahnBanach.thy Wed Jun 13 19:14:51 2007 +0200 3.2 +++ b/src/HOL/Real/HahnBanach/HahnBanach.thy Thu Jun 14 00:22:45 2007 +0200 3.3 @@ -62,8 +62,9 @@ 3.4 proof - 3.5 def M \<equiv> "norm_pres_extensions E p F f" 3.6 hence M: "M = \<dots>" by (simp only:) 3.7 - have E: "vectorspace E" . 3.8 - have F: "vectorspace F" .. 3.9 + note E = `vectorspace E` 3.10 + then have F: "vectorspace F" .. 3.11 + note FE = `F \<unlhd> E` 3.12 { 3.13 fix c assume cM: "c \<in> chain M" and ex: "\<exists>x. x \<in> c" 3.14 have "\<Union>c \<in> M" 3.15 @@ -80,9 +81,9 @@ 3.16 qed 3.17 moreover from M cM a have "linearform ?H ?h" 3.18 by (rule sup_lf) 3.19 - moreover from a M cM ex have "?H \<unlhd> E" 3.20 + moreover from a M cM ex FE E have "?H \<unlhd> E" 3.21 by (rule sup_subE) 3.22 - moreover from a M cM ex have "F \<unlhd> ?H" 3.23 + moreover from a M cM ex FE have "F \<unlhd> ?H" 3.24 by (rule sup_supF) 3.25 moreover from a M cM ex have "graph F f \<subseteq> graph ?H ?h" 3.26 by (rule sup_ext) 3.27 @@ -102,14 +103,14 @@ 3.28 -- {* We show that @{text M} is non-empty: *} 3.29 show "graph F f \<in> M" 3.30 proof (unfold M_def, rule norm_pres_extensionI2) 3.31 - show "linearform F f" . 3.32 - show "F \<unlhd> E" . 3.33 + show "linearform F f" by fact 3.34 + show "F \<unlhd> E" by fact 3.35 from F show "F \<unlhd> F" by (rule vectorspace.subspace_refl) 3.36 show "graph F f \<subseteq> graph F f" .. 3.37 - show "\<forall>x\<in>F. f x \<le> p x" . 3.38 + show "\<forall>x\<in>F. f x \<le> p x" by fact 3.39 qed 3.40 qed 3.41 - then obtain g where gM: "g \<in> M" and "\<forall>x \<in> M. g \<subseteq> x \<longrightarrow> g = x" 3.42 + then obtain g where gM: "g \<in> M" and gx: "\<forall>x \<in> M. g \<subseteq> x \<longrightarrow> g = x" 3.43 by blast 3.44 from gM [unfolded M_def] obtain H h where 3.45 g_rep: "g = graph H h" 3.46 @@ -120,7 +121,7 @@ 3.47 -- {* @{text g} is a norm-preserving extension of @{text f}, in other words: *} 3.48 -- {* @{text g} is the graph of some linear form @{text h} defined on a subspace @{text H} of @{text E}, *} 3.49 -- {* and @{text h} is an extension of @{text f} that is again bounded by @{text p}. \skp *} 3.50 - from HE have H: "vectorspace H" 3.51 + from HE E have H: "vectorspace H" 3.52 by (rule subspace.vectorspace) 3.53 3.54 have HE_eq: "H = E" 3.55 @@ -139,7 +140,7 @@ 3.56 proof 3.57 assume "x' = 0" 3.58 with H have "x' \<in> H" by (simp only: vectorspace.zero) 3.59 - then show False by contradiction 3.60 + with `x' \<notin> H` show False by contradiction 3.61 qed 3.62 qed 3.63 3.64 @@ -147,12 +148,12 @@ 3.65 -- {* Define @{text H'} as the direct sum of @{text H} and the linear closure of @{text x'}. \skp *} 3.66 have HH': "H \<unlhd> H'" 3.67 proof (unfold H'_def) 3.68 - have "vectorspace (lin x')" .. 3.69 + from x'E have "vectorspace (lin x')" .. 3.70 with H show "H \<unlhd> H + lin x'" .. 3.71 qed 3.72 3.73 obtain xi where 3.74 - "\<forall>y \<in> H. - p (y + x') - h y \<le> xi 3.75 + xi: "\<forall>y \<in> H. - p (y + x') - h y \<le> xi 3.76 \<and> xi \<le> p (y + x') - h y" 3.77 -- {* Pick a real number @{text \<xi>} that fulfills certain inequations; this will *} 3.78 -- {* be used to establish that @{text h'} is a norm-preserving extension of @{text h}. 3.79 @@ -178,7 +179,7 @@ 3.80 finally have "h v - h u \<le> p (v + x') + p (u + x')" . 3.81 then show "- p (u + x') - h u \<le> p (v + x') - h v" by simp 3.82 qed 3.83 - then show ?thesis .. 3.84 + then show thesis by (blast intro: that) 3.85 qed 3.86 3.87 def h' \<equiv> "\<lambda>x. let (y, a) = 3.88 @@ -193,8 +194,8 @@ 3.89 have "graph H h \<subseteq> graph H' h'" 3.90 proof (rule graph_extI) 3.91 fix t assume t: "t \<in> H" 3.92 - have "(SOME (y, a). t = y + a \<cdot> x' \<and> y \<in> H) = (t, 0)" 3.93 - by (rule decomp_H'_H) 3.94 + from E HE t have "(SOME (y, a). t = y + a \<cdot> x' \<and> y \<in> H) = (t, 0)" 3.95 + using `x' \<notin> H` `x' \<in> E` `x' \<noteq> 0` by (rule decomp_H'_H) 3.96 with h'_def show "h t = h' t" by (simp add: Let_def) 3.97 next 3.98 from HH' show "H \<subseteq> H'" .. 3.99 @@ -216,7 +217,7 @@ 3.100 hence "(x', h' x') \<in> graph H' h'" .. 3.101 with eq have "(x', h' x') \<in> graph H h" by (simp only:) 3.102 hence "x' \<in> H" .. 3.103 - thus False by contradiction 3.104 + with `x' \<notin> H` show False by contradiction 3.105 qed 3.106 with g_rep show ?thesis by simp 3.107 qed 3.108 @@ -226,15 +227,17 @@ 3.109 proof (unfold M_def) 3.110 show "graph H' h' \<in> norm_pres_extensions E p F f" 3.111 proof (rule norm_pres_extensionI2) 3.112 - show "linearform H' h'" by (rule h'_lf) 3.113 + show "linearform H' h'" 3.114 + using h'_def H'_def HE linearform `x' \<notin> H` `x' \<in> E` `x' \<noteq> 0` E 3.115 + by (rule h'_lf) 3.116 show "H' \<unlhd> E" 3.117 - proof (unfold H'_def, rule) 3.118 - show "H \<unlhd> E" . 3.119 - show "vectorspace E" . 3.120 + unfolding H'_def 3.121 + proof 3.122 + show "H \<unlhd> E" by fact 3.123 + show "vectorspace E" by fact 3.124 from x'E show "lin x' \<unlhd> E" .. 3.125 qed 3.126 - have "F \<unlhd> H" . 3.127 - from H this HH' show FH': "F \<unlhd> H'" 3.128 + from H `F \<unlhd> H` HH' show FH': "F \<unlhd> H'" 3.129 by (rule vectorspace.subspace_trans) 3.130 show "graph F f \<subseteq> graph H' h'" 3.131 proof (rule graph_extI) 3.132 @@ -245,9 +248,12 @@ 3.133 by (simp add: Let_def) 3.134 also have "(x, 0) = 3.135 (SOME (y, a). x = y + a \<cdot> x' \<and> y \<in> H)" 3.136 + using E HE 3.137 proof (rule decomp_H'_H [symmetric]) 3.138 from FH x show "x \<in> H" .. 3.139 from x' show "x' \<noteq> 0" . 3.140 + show "x' \<notin> H" by fact 3.141 + show "x' \<in> E" by fact 3.142 qed 3.143 also have 3.144 "(let (y, a) = (SOME (y, a). x = y + a \<cdot> x' \<and> y \<in> H) 3.145 @@ -256,14 +262,17 @@ 3.146 next 3.147 from FH' show "F \<subseteq> H'" .. 3.148 qed 3.149 - show "\<forall>x \<in> H'. h' x \<le> p x" by (rule h'_norm_pres) 3.150 + show "\<forall>x \<in> H'. h' x \<le> p x" 3.151 + using h'_def H'_def `x' \<notin> H` `x' \<in> E` `x' \<noteq> 0` E HE 3.152 + `seminorm E p` linearform and hp xi 3.153 + by (rule h'_norm_pres) 3.154 qed 3.155 qed 3.156 ultimately show ?thesis .. 3.157 qed 3.158 hence "\<not> (\<forall>x \<in> M. g \<subseteq> x \<longrightarrow> g = x)" by simp 3.159 -- {* So the graph @{text g} of @{text h} cannot be maximal. Contradiction! \skp *} 3.160 - then show "H = E" by contradiction 3.161 + with gx show "H = E" by contradiction 3.162 qed 3.163 3.164 from HE_eq and linearform have "linearform E h" 3.165 @@ -303,19 +312,24 @@ 3.166 \<and> (\<forall>x \<in> F. g x = f x) 3.167 \<and> (\<forall>x \<in> E. \<bar>g x\<bar> \<le> p x)" 3.168 proof - 3.169 - have "\<exists>g. linearform E g \<and> (\<forall>x \<in> F. g x = f x) 3.170 - \<and> (\<forall>x \<in> E. g x \<le> p x)" 3.171 + note E = `vectorspace E` 3.172 + note FE = `subspace F E` 3.173 + note sn = `seminorm E p` 3.174 + note lf = `linearform F f` 3.175 + have "\<exists>g. linearform E g \<and> (\<forall>x \<in> F. g x = f x) \<and> (\<forall>x \<in> E. g x \<le> p x)" 3.176 + using E FE sn lf 3.177 proof (rule HahnBanach) 3.178 show "\<forall>x \<in> F. f x \<le> p x" 3.179 - by (rule abs_ineq_iff [THEN iffD1]) 3.180 + using FE E sn lf and fp by (rule abs_ineq_iff [THEN iffD1]) 3.181 qed 3.182 - then obtain g where * : "linearform E g" "\<forall>x \<in> F. g x = f x" 3.183 - and "\<forall>x \<in> E. g x \<le> p x" by blast 3.184 + then obtain g where lg: "linearform E g" and *: "\<forall>x \<in> F. g x = f x" 3.185 + and **: "\<forall>x \<in> E. g x \<le> p x" by blast 3.186 have "\<forall>x \<in> E. \<bar>g x\<bar> \<le> p x" 3.187 + using _ E sn lg ** 3.188 proof (rule abs_ineq_iff [THEN iffD2]) 3.189 show "E \<unlhd> E" .. 3.190 qed 3.191 - with * show ?thesis by blast 3.192 + with lg * show ?thesis by blast 3.193 qed 3.194 3.195 3.196 @@ -336,14 +350,14 @@ 3.197 proof - 3.198 have E: "vectorspace E" by unfold_locales 3.199 have E_norm: "normed_vectorspace E norm" by rule unfold_locales 3.200 - have FE: "F \<unlhd> E" . 3.201 + note FE = `F \<unlhd> E` 3.202 have F: "vectorspace F" by rule unfold_locales 3.203 - have linearform: "linearform F f" . 3.204 + note linearform = `linearform F f` 3.205 have F_norm: "normed_vectorspace F norm" 3.206 - by (rule subspace_normed_vs) 3.207 + using FE E_norm by (rule subspace_normed_vs) 3.208 have ge_zero: "0 \<le> \<parallel>f\<parallel>\<hyphen>F" 3.209 by (rule normed_vectorspace.fn_norm_ge_zero 3.210 - [OF F_norm (* continuous.intro*), folded B_def fn_norm_def]) 3.211 + [OF F_norm `continuous F norm f`, folded B_def fn_norm_def]) 3.212 txt {* We define a function @{text p} on @{text E} as follows: 3.213 @{text "p x = \<parallel>f\<parallel> \<cdot> \<parallel>x\<parallel>"} *} 3.214 def p \<equiv> "\<lambda>x. \<parallel>f\<parallel>\<hyphen>F * \<parallel>x\<parallel>" 3.215 @@ -390,6 +404,7 @@ 3.216 have "\<forall>x \<in> F. \<bar>f x\<bar> \<le> p x" 3.217 proof 3.218 fix x assume "x \<in> F" 3.219 + from this and `continuous F norm f` 3.220 show "\<bar>f x\<bar> \<le> p x" 3.221 by (unfold p_def) (rule normed_vectorspace.fn_norm_le_cong 3.222 [OF F_norm, folded B_def fn_norm_def]) 3.223 @@ -452,7 +467,7 @@ 3.224 show "\<forall>x \<in> F. \<bar>f x\<bar> \<le> \<parallel>g\<parallel>\<hyphen>E * \<parallel>x\<parallel>" 3.225 proof 3.226 fix x assume x: "x \<in> F" 3.227 - from a have "g x = f x" .. 3.228 + from a x have "g x = f x" .. 3.229 hence "\<bar>f x\<bar> = \<bar>g x\<bar>" by (simp only:) 3.230 also from g_cont 3.231 have "\<dots> \<le> \<parallel>g\<parallel>\<hyphen>E * \<parallel>x\<parallel>" 3.232 @@ -465,7 +480,7 @@ 3.233 using g_cont 3.234 by (rule fn_norm_ge_zero [of g, folded B_def fn_norm_def]) 3.235 next 3.236 - show "continuous F norm f" . 3.237 + show "continuous F norm f" by fact 3.238 qed 3.239 qed 3.240 with linearformE a g_cont show ?thesis by blast

4.1 --- a/src/HOL/Real/HahnBanach/HahnBanachExtLemmas.thy Wed Jun 13 19:14:51 2007 +0200 4.2 +++ b/src/HOL/Real/HahnBanach/HahnBanachExtLemmas.thy Thu Jun 14 00:22:45 2007 +0200 4.3 @@ -96,11 +96,12 @@ 4.4 includes vectorspace E 4.5 shows "linearform H' h'" 4.6 proof 4.7 + note E = `vectorspace E` 4.8 have H': "vectorspace H'" 4.9 proof (unfold H'_def) 4.10 - have "x0 \<in> E" . 4.11 - then have "lin x0 \<unlhd> E" .. 4.12 - with HE show "vectorspace (H + lin x0)" .. 4.13 + from `x0 \<in> E` 4.14 + have "lin x0 \<unlhd> E" .. 4.15 + with HE show "vectorspace (H + lin x0)" using E .. 4.16 qed 4.17 { 4.18 fix x1 x2 assume x1: "x1 \<in> H'" and x2: "x2 \<in> H'" 4.19 @@ -114,7 +115,7 @@ 4.20 and x2_rep: "x2 = y2 + a2 \<cdot> x0" and y2: "y2 \<in> H" 4.21 by (unfold H'_def sum_def lin_def) blast 4.22 4.23 - have ya: "y1 + y2 = y \<and> a1 + a2 = a" using _ HE _ y x0 4.24 + have ya: "y1 + y2 = y \<and> a1 + a2 = a" using E HE _ y x0 4.25 proof (rule decomp_H') txt_raw {* \label{decomp-H-use} *} 4.26 from HE y1 y2 show "y1 + y2 \<in> H" 4.27 by (rule subspace.add_closed) 4.28 @@ -126,7 +127,7 @@ 4.29 finally show "(y1 + y2) + (a1 + a2) \<cdot> x0 = y + a \<cdot> x0" . 4.30 qed 4.31 4.32 - from h'_def x1x2 _ HE y x0 4.33 + from h'_def x1x2 E HE y x0 4.34 have "h' (x1 + x2) = h y + a * xi" 4.35 by (rule h'_definite) 4.36 also have "\<dots> = h (y1 + y2) + (a1 + a2) * xi" 4.37 @@ -135,10 +136,10 @@ 4.38 by simp 4.39 also have "\<dots> + (a1 + a2) * xi = (h y1 + a1 * xi) + (h y2 + a2 * xi)" 4.40 by (simp add: left_distrib) 4.41 - also from h'_def x1_rep _ HE y1 x0 4.42 + also from h'_def x1_rep E HE y1 x0 4.43 have "h y1 + a1 * xi = h' x1" 4.44 by (rule h'_definite [symmetric]) 4.45 - also from h'_def x2_rep _ HE y2 x0 4.46 + also from h'_def x2_rep E HE y2 x0 4.47 have "h y2 + a2 * xi = h' x2" 4.48 by (rule h'_definite [symmetric]) 4.49 finally show ?thesis . 4.50 @@ -154,7 +155,7 @@ 4.51 and x1_rep: "x1 = y1 + a1 \<cdot> x0" and y1: "y1 \<in> H" 4.52 by (unfold H'_def sum_def lin_def) blast 4.53 4.54 - have ya: "c \<cdot> y1 = y \<and> c * a1 = a" using _ HE _ y x0 4.55 + have ya: "c \<cdot> y1 = y \<and> c * a1 = a" using E HE _ y x0 4.56 proof (rule decomp_H') 4.57 from HE y1 show "c \<cdot> y1 \<in> H" 4.58 by (rule subspace.mult_closed) 4.59 @@ -166,7 +167,7 @@ 4.60 finally show "c \<cdot> y1 + (c * a1) \<cdot> x0 = y + a \<cdot> x0" . 4.61 qed 4.62 4.63 - from h'_def cx1_rep _ HE y x0 have "h' (c \<cdot> x1) = h y + a * xi" 4.64 + from h'_def cx1_rep E HE y x0 have "h' (c \<cdot> x1) = h y + a * xi" 4.65 by (rule h'_definite) 4.66 also have "\<dots> = h (c \<cdot> y1) + (c * a1) * xi" 4.67 by (simp only: ya) 4.68 @@ -174,7 +175,7 @@ 4.69 by simp 4.70 also have "\<dots> + (c * a1) * xi = c * (h y1 + a1 * xi)" 4.71 by (simp only: right_distrib) 4.72 - also from h'_def x1_rep _ HE y1 x0 have "h y1 + a1 * xi = h' x1" 4.73 + also from h'_def x1_rep E HE y1 x0 have "h y1 + a1 * xi = h' x1" 4.74 by (rule h'_definite [symmetric]) 4.75 finally show ?thesis . 4.76 qed 4.77 @@ -195,6 +196,8 @@ 4.78 and a': "\<forall>y \<in> H. - p (y + x0) - h y \<le> xi \<and> xi \<le> p (y + x0) - h y" 4.79 shows "\<forall>x \<in> H'. h' x \<le> p x" 4.80 proof 4.81 + note E = `vectorspace E` 4.82 + note HE = `subspace H E` 4.83 fix x assume x': "x \<in> H'" 4.84 show "h' x \<le> p x" 4.85 proof - 4.86 @@ -206,7 +209,7 @@ 4.87 from y have y': "y \<in> E" .. 4.88 from y have ay: "inverse a \<cdot> y \<in> H" by simp 4.89 4.90 - from h'_def x_rep _ _ y x0 have "h' x = h y + a * xi" 4.91 + from h'_def x_rep E HE y x0 have "h' x = h y + a * xi" 4.92 by (rule h'_definite) 4.93 also have "\<dots> \<le> p (y + a \<cdot> x0)" 4.94 proof (rule linorder_cases)

5.1 --- a/src/HOL/Real/HahnBanach/HahnBanachSupLemmas.thy Wed Jun 13 19:14:51 2007 +0200 5.2 +++ b/src/HOL/Real/HahnBanach/HahnBanachSupLemmas.thy Thu Jun 14 00:22:45 2007 +0200 5.3 @@ -126,13 +126,13 @@ 5.4 @{text x} and @{text y} are contained in the greater 5.5 one. \label{cases1}*} 5.6 5.7 - from cM have "graph H'' h'' \<subseteq> graph H' h' \<or> graph H' h' \<subseteq> graph H'' h''" 5.8 + from cM c'' c' have "graph H'' h'' \<subseteq> graph H' h' \<or> graph H' h' \<subseteq> graph H'' h''" 5.9 (is "?case1 \<or> ?case2") .. 5.10 then show ?thesis 5.11 proof 5.12 assume ?case1 5.13 - have "(x, h x) \<in> graph H'' h''" . 5.14 - also have "... \<subseteq> graph H' h'" . 5.15 + have "(x, h x) \<in> graph H'' h''" by fact 5.16 + also have "... \<subseteq> graph H' h'" by fact 5.17 finally have xh:"(x, h x) \<in> graph H' h'" . 5.18 then have "x \<in> H'" .. 5.19 moreover from y_hy have "y \<in> H'" .. 5.20 @@ -143,8 +143,8 @@ 5.21 assume ?case2 5.22 from x_hx have "x \<in> H''" .. 5.23 moreover { 5.24 - from y_hy have "(y, h y) \<in> graph H' h'" . 5.25 - also have "\<dots> \<subseteq> graph H'' h''" . 5.26 + have "(y, h y) \<in> graph H' h'" by (rule y_hy) 5.27 + also have "\<dots> \<subseteq> graph H'' h''" by fact 5.28 finally have "(y, h y) \<in> graph H'' h''" . 5.29 } then have "y \<in> H''" .. 5.30 moreover from cM u and c'' have "graph H'' h'' \<subseteq> graph H h" 5.31 @@ -402,7 +402,7 @@ 5.32 includes subspace H E + vectorspace E + seminorm E p + linearform H h 5.33 shows "(\<forall>x \<in> H. \<bar>h x\<bar> \<le> p x) = (\<forall>x \<in> H. h x \<le> p x)" (is "?L = ?R") 5.34 proof 5.35 - have H: "vectorspace H" .. 5.36 + have H: "vectorspace H" using `vectorspace E` .. 5.37 { 5.38 assume l: ?L 5.39 show ?R 5.40 @@ -419,12 +419,13 @@ 5.41 fix x assume x: "x \<in> H" 5.42 show "\<And>a b :: real. - a \<le> b \<Longrightarrow> b \<le> a \<Longrightarrow> \<bar>b\<bar> \<le> a" 5.43 by arith 5.44 - have "linearform H h" . 5.45 - from this H x have "- h x = h (- x)" by (rule linearform.neg [symmetric]) 5.46 + from `linearform H h` and H x 5.47 + have "- h x = h (- x)" by (rule linearform.neg [symmetric]) 5.48 also 5.49 from H x have "- x \<in> H" by (rule vectorspace.neg_closed) 5.50 with r have "h (- x) \<le> p (- x)" .. 5.51 also have "\<dots> = p x" 5.52 + using `seminorm E p` `vectorspace E` 5.53 proof (rule seminorm.minus) 5.54 from x show "x \<in> E" .. 5.55 qed

6.1 --- a/src/HOL/Real/HahnBanach/Linearform.thy Wed Jun 13 19:14:51 2007 +0200 6.2 +++ b/src/HOL/Real/HahnBanach/Linearform.thy Thu Jun 14 00:22:45 2007 +0200 6.3 @@ -36,7 +36,7 @@ 6.4 assume x: "x \<in> V" and y: "y \<in> V" 6.5 hence "x - y = x + - y" by (rule diff_eq1) 6.6 also have "f ... = f x + f (- y)" by (rule add) (simp_all add: x y) 6.7 - also from _ y have "f (- y) = - f y" by (rule neg) 6.8 + also have "f (- y) = - f y" using `vectorspace V` y by (rule neg) 6.9 finally show ?thesis by simp 6.10 qed 6.11 6.12 @@ -47,7 +47,7 @@ 6.13 shows "f 0 = 0" 6.14 proof - 6.15 have "f 0 = f (0 - 0)" by simp 6.16 - also have "\<dots> = f 0 - f 0" by (rule diff) simp_all 6.17 + also have "\<dots> = f 0 - f 0" using `vectorspace V` by (rule diff) simp_all 6.18 also have "\<dots> = 0" by simp 6.19 finally show ?thesis . 6.20 qed

7.1 --- a/src/HOL/Real/HahnBanach/Subspace.thy Wed Jun 13 19:14:51 2007 +0200 7.2 +++ b/src/HOL/Real/HahnBanach/Subspace.thy Thu Jun 14 00:22:45 2007 +0200 7.3 @@ -58,7 +58,7 @@ 7.4 have "U \<noteq> {}" by (rule U_V.non_empty) 7.5 then obtain x where x: "x \<in> U" by blast 7.6 hence "x \<in> V" .. hence "0 = x - x" by simp 7.7 - also have "... \<in> U" by (rule U_V.diff_closed) 7.8 + also from `vectorspace V` x x have "... \<in> U" by (rule U_V.diff_closed) 7.9 finally show ?thesis . 7.10 qed 7.11 7.12 @@ -198,8 +198,14 @@ 7.13 text {* Any linear closure is a vector space. *} 7.14 7.15 lemma (in vectorspace) lin_vectorspace [intro]: 7.16 - "x \<in> V \<Longrightarrow> vectorspace (lin x)" 7.17 - by (rule subspace.vectorspace) (rule lin_subspace) 7.18 + assumes "x \<in> V" 7.19 + shows "vectorspace (lin x)" 7.20 +proof - 7.21 + from `x \<in> V` have "subspace (lin x) V" 7.22 + by (rule lin_subspace) 7.23 + from this and `vectorspace V` show ?thesis 7.24 + by (rule subspace.vectorspace) 7.25 +qed 7.26 7.27 7.28 subsection {* Sum of two vectorspaces *} 7.29 @@ -253,19 +259,17 @@ 7.30 proof 7.31 have "0 \<in> U + V" 7.32 proof 7.33 - show "0 \<in> U" .. 7.34 - show "0 \<in> V" .. 7.35 + show "0 \<in> U" using `vectorspace E` .. 7.36 + show "0 \<in> V" using `vectorspace E` .. 7.37 show "(0::'a) = 0 + 0" by simp 7.38 qed 7.39 thus "U + V \<noteq> {}" by blast 7.40 show "U + V \<subseteq> E" 7.41 proof 7.42 fix x assume "x \<in> U + V" 7.43 - then obtain u v where x: "x = u + v" and 7.44 - u: "u \<in> U" and v: "v \<in> V" .. 7.45 - have "U \<unlhd> E" . with u have "u \<in> E" .. 7.46 - moreover have "V \<unlhd> E" . with v have "v \<in> E" .. 7.47 - ultimately show "x \<in> E" using x by simp 7.48 + then obtain u v where "x = u + v" and 7.49 + "u \<in> U" and "v \<in> V" .. 7.50 + then show "x \<in> E" by simp 7.51 qed 7.52 fix x y assume x: "x \<in> U + V" and y: "y \<in> U + V" 7.53 show "x + y \<in> U + V" 7.54 @@ -314,8 +318,10 @@ 7.55 and sum: "u1 + v1 = u2 + v2" 7.56 shows "u1 = u2 \<and> v1 = v2" 7.57 proof 7.58 - have U: "vectorspace U" by (rule subspace.vectorspace) 7.59 - have V: "vectorspace V" by (rule subspace.vectorspace) 7.60 + have U: "vectorspace U" 7.61 + using `subspace U E` `vectorspace E` by (rule subspace.vectorspace) 7.62 + have V: "vectorspace V" 7.63 + using `subspace V E` `vectorspace E` by (rule subspace.vectorspace) 7.64 from u1 u2 v1 v2 and sum have eq: "u1 - u2 = v2 - v1" 7.65 by (simp add: add_diff_swap) 7.66 from u1 u2 have u: "u1 - u2 \<in> U" 7.67 @@ -327,15 +333,15 @@ 7.68 7.69 show "u1 = u2" 7.70 proof (rule add_minus_eq) 7.71 - show "u1 \<in> E" .. 7.72 - show "u2 \<in> E" .. 7.73 - from u u' and direct show "u1 - u2 = 0" by force 7.74 + from u1 show "u1 \<in> E" .. 7.75 + from u2 show "u2 \<in> E" .. 7.76 + from u u' and direct show "u1 - u2 = 0" by blast 7.77 qed 7.78 show "v1 = v2" 7.79 proof (rule add_minus_eq [symmetric]) 7.80 - show "v1 \<in> E" .. 7.81 - show "v2 \<in> E" .. 7.82 - from v v' and direct show "v2 - v1 = 0" by force 7.83 + from v1 show "v1 \<in> E" .. 7.84 + from v2 show "v2 \<in> E" .. 7.85 + from v v' and direct show "v2 - v1 = 0" by blast 7.86 qed 7.87 qed 7.88 7.89 @@ -375,19 +381,19 @@ 7.90 from x have "x \<in> H" .. 7.91 with xx' have "inverse a \<cdot> a \<cdot> x' \<in> H" by simp 7.92 with a and x' have "x' \<in> H" by (simp add: mult_assoc2) 7.93 - thus ?thesis by contradiction 7.94 + with `x' \<notin> H` show ?thesis by contradiction 7.95 qed 7.96 thus "x \<in> {0}" .. 7.97 qed 7.98 show "{0} \<subseteq> H \<inter> lin x'" 7.99 proof - 7.100 - have "0 \<in> H" .. 7.101 - moreover have "0 \<in> lin x'" .. 7.102 + have "0 \<in> H" using `vectorspace E` .. 7.103 + moreover have "0 \<in> lin x'" using `x' \<in> E` .. 7.104 ultimately show ?thesis by blast 7.105 qed 7.106 qed 7.107 - show "lin x' \<unlhd> E" .. 7.108 - qed 7.109 + show "lin x' \<unlhd> E" using `x' \<in> E` .. 7.110 + qed (rule `vectorspace E`, rule `subspace H E`, rule y1, rule y2, rule eq) 7.111 thus "y1 = y2" .. 7.112 from c have "a1 \<cdot> x' = a2 \<cdot> x'" .. 7.113 with x' show "a1 = a2" by (simp add: mult_right_cancel) 7.114 @@ -412,7 +418,7 @@ 7.115 proof (rule decomp_H') 7.116 from ya x' show "y + a \<cdot> x' = t + 0 \<cdot> x'" by simp 7.117 from ya show "y \<in> H" .. 7.118 - qed 7.119 + qed (rule `vectorspace E`, rule `subspace H E`, rule t, (rule x')+) 7.120 with t x' show "(y, a) = (y + a \<cdot> x', 0)" by simp 7.121 qed 7.122 7.123 @@ -450,7 +456,7 @@ 7.124 from xq show "fst q \<in> H" .. 7.125 from xp and xq show "fst p + snd p \<cdot> x' = fst q + snd q \<cdot> x'" 7.126 by simp 7.127 - qed 7.128 + qed (rule `vectorspace E`, rule `subspace H E`, (rule x')+) 7.129 thus ?thesis by (cases p, cases q) simp 7.130 qed 7.131 qed

8.1 --- a/src/HOL/Real/HahnBanach/VectorSpace.thy Wed Jun 13 19:14:51 2007 +0200 8.2 +++ b/src/HOL/Real/HahnBanach/VectorSpace.thy Thu Jun 14 00:22:45 2007 +0200 8.3 @@ -89,7 +89,7 @@ 8.4 proof - 8.5 from non_empty obtain x where x: "x \<in> V" by blast 8.6 then have "0 = x - x" by (rule diff_self [symmetric]) 8.7 - also from x have "... \<in> V" by (rule diff_closed) 8.8 + also from x x have "... \<in> V" by (rule diff_closed) 8.9 finally show ?thesis . 8.10 qed 8.11 8.12 @@ -116,7 +116,7 @@ 8.13 assume x: "x \<in> V" 8.14 have " (a - b) \<cdot> x = (a + - b) \<cdot> x" 8.15 by (simp add: real_diff_def) 8.16 - also have "... = a \<cdot> x + (- b) \<cdot> x" 8.17 + also from x have "... = a \<cdot> x + (- b) \<cdot> x" 8.18 by (rule add_mult_distrib2) 8.19 also from x have "... = a \<cdot> x + - (b \<cdot> x)" 8.20 by (simp add: negate_eq1 mult_assoc2) 8.21 @@ -138,7 +138,7 @@ 8.22 assume x: "x \<in> V" 8.23 have "0 \<cdot> x = (1 - 1) \<cdot> x" by simp 8.24 also have "... = (1 + - 1) \<cdot> x" by simp 8.25 - also have "... = 1 \<cdot> x + (- 1) \<cdot> x" 8.26 + also from x have "... = 1 \<cdot> x + (- 1) \<cdot> x" 8.27 by (rule add_mult_distrib2) 8.28 also from x have "... = x + (- 1) \<cdot> x" by simp 8.29 also from x have "... = x + - x" by (simp add: negate_eq2a) 8.30 @@ -260,11 +260,11 @@ 8.31 assume a: "a \<noteq> 0" 8.32 assume x: "x \<in> V" "x \<noteq> 0" and ax: "a \<cdot> x = 0" 8.33 from x a have "x = (inverse a * a) \<cdot> x" by simp 8.34 - also have "... = inverse a \<cdot> (a \<cdot> x)" by (rule mult_assoc) 8.35 + also from `x \<in> V` have "... = inverse a \<cdot> (a \<cdot> x)" by (rule mult_assoc) 8.36 also from ax have "... = inverse a \<cdot> 0" by simp 8.37 also have "... = 0" by simp 8.38 finally have "x = 0" . 8.39 - thus "a = 0" by contradiction 8.40 + with `x \<noteq> 0` show "a = 0" by contradiction 8.41 qed 8.42 8.43 lemma (in vectorspace) mult_left_cancel: 8.44 @@ -360,7 +360,7 @@ 8.45 and eq: "a + b = c + d" 8.46 then have "- c + (a + b) = - c + (c + d)" 8.47 by (simp add: add_left_cancel) 8.48 - also have "... = d" by (rule minus_add_cancel) 8.49 + also have "... = d" using `c \<in> V` `d \<in> V` by (rule minus_add_cancel) 8.50 finally have eq: "- c + (a + b) = d" . 8.51 from vs have "a - c = (- c + (a + b)) + - b" 8.52 by (simp add: add_ac diff_eq1)

9.1 --- a/src/HOL/Real/HahnBanach/ZornLemma.thy Wed Jun 13 19:14:51 2007 +0200 9.2 +++ b/src/HOL/Real/HahnBanach/ZornLemma.thy Thu Jun 14 00:22:45 2007 +0200 9.3 @@ -48,6 +48,7 @@ 9.4 show "\<Union>c \<in> S" 9.5 proof (rule r) 9.6 from c show "\<exists>x. x \<in> c" by fast 9.7 + show "c \<in> chain S" by fact 9.8 qed 9.9 qed 9.10 qed