src/HOL/Real/HahnBanach/HahnBanachExtLemmas.thy
changeset 27611 2c01c0bdb385
parent 23378 1d138d6bb461
child 27612 d3eb431db035
     1.1 --- a/src/HOL/Real/HahnBanach/HahnBanachExtLemmas.thy	Tue Jul 15 16:02:10 2008 +0200
     1.2 +++ b/src/HOL/Real/HahnBanach/HahnBanachExtLemmas.thy	Tue Jul 15 16:50:09 2008 +0200
     1.3 @@ -40,10 +40,11 @@
     1.4  *}
     1.5  
     1.6  lemma ex_xi:
     1.7 -  includes vectorspace F
     1.8 +  assumes "vectorspace F"
     1.9    assumes r: "\<And>u v. u \<in> F \<Longrightarrow> v \<in> F \<Longrightarrow> a u \<le> b v"
    1.10    shows "\<exists>xi::real. \<forall>y \<in> F. a y \<le> xi \<and> xi \<le> b y"
    1.11  proof -
    1.12 +  interpret vectorspace [F] by fact
    1.13    txt {* From the completeness of the reals follows:
    1.14      The set @{text "S = {a u. u \<in> F}"} has a supremum, if it is
    1.15      non-empty and has an upper bound. *}
    1.16 @@ -86,183 +87,190 @@
    1.17  *}
    1.18  
    1.19  lemma h'_lf:
    1.20 -  includes var H + var h + var E
    1.21    assumes h'_def: "h' \<equiv> \<lambda>x. let (y, a) =
    1.22        SOME (y, a). x = y + a \<cdot> x0 \<and> y \<in> H in h y + a * xi"
    1.23      and H'_def: "H' \<equiv> H + lin x0"
    1.24      and HE: "H \<unlhd> E"
    1.25 -  includes linearform H h
    1.26 +  assumes "linearform H h"
    1.27    assumes x0: "x0 \<notin> H"  "x0 \<in> E"  "x0 \<noteq> 0"
    1.28 -  includes vectorspace E
    1.29 +  assumes E: "vectorspace E"
    1.30    shows "linearform H' h'"
    1.31 -proof
    1.32 -  note E = `vectorspace E`
    1.33 -  have H': "vectorspace H'"
    1.34 -  proof (unfold H'_def)
    1.35 -    from `x0 \<in> E`
    1.36 -    have "lin x0 \<unlhd> E" ..
    1.37 -    with HE show "vectorspace (H + lin x0)" using E ..
    1.38 -  qed
    1.39 -  {
    1.40 -    fix x1 x2 assume x1: "x1 \<in> H'" and x2: "x2 \<in> H'"
    1.41 -    show "h' (x1 + x2) = h' x1 + h' x2"
    1.42 -    proof -
    1.43 -      from H' x1 x2 have "x1 + x2 \<in> H'"
    1.44 -        by (rule vectorspace.add_closed)
    1.45 -      with x1 x2 obtain y y1 y2 a a1 a2 where
    1.46 -            x1x2: "x1 + x2 = y + a \<cdot> x0" and y: "y \<in> H"
    1.47 +proof -
    1.48 +  interpret linearform [H h] by fact
    1.49 +  interpret vectorspace [E] by fact
    1.50 +  show ?thesis proof
    1.51 +    note E = `vectorspace E`
    1.52 +    have H': "vectorspace H'"
    1.53 +    proof (unfold H'_def)
    1.54 +      from `x0 \<in> E`
    1.55 +      have "lin x0 \<unlhd> E" ..
    1.56 +      with HE show "vectorspace (H + lin x0)" using E ..
    1.57 +    qed
    1.58 +    {
    1.59 +      fix x1 x2 assume x1: "x1 \<in> H'" and x2: "x2 \<in> H'"
    1.60 +      show "h' (x1 + x2) = h' x1 + h' x2"
    1.61 +      proof -
    1.62 +	from H' x1 x2 have "x1 + x2 \<in> H'"
    1.63 +          by (rule vectorspace.add_closed)
    1.64 +	with x1 x2 obtain y y1 y2 a a1 a2 where
    1.65 +          x1x2: "x1 + x2 = y + a \<cdot> x0" and y: "y \<in> H"
    1.66            and x1_rep: "x1 = y1 + a1 \<cdot> x0" and y1: "y1 \<in> H"
    1.67            and x2_rep: "x2 = y2 + a2 \<cdot> x0" and y2: "y2 \<in> H"
    1.68 -        by (unfold H'_def sum_def lin_def) blast
    1.69 -
    1.70 -      have ya: "y1 + y2 = y \<and> a1 + a2 = a" using E HE _ y x0
    1.71 -      proof (rule decomp_H') txt_raw {* \label{decomp-H-use} *}
    1.72 -        from HE y1 y2 show "y1 + y2 \<in> H"
    1.73 -          by (rule subspace.add_closed)
    1.74 -        from x0 and HE y y1 y2
    1.75 -        have "x0 \<in> E"  "y \<in> E"  "y1 \<in> E"  "y2 \<in> E" by auto
    1.76 -        with x1_rep x2_rep have "(y1 + y2) + (a1 + a2) \<cdot> x0 = x1 + x2"
    1.77 -          by (simp add: add_ac add_mult_distrib2)
    1.78 -        also note x1x2
    1.79 -        finally show "(y1 + y2) + (a1 + a2) \<cdot> x0 = y + a \<cdot> x0" .
    1.80 +          by (unfold H'_def sum_def lin_def) blast
    1.81 +	
    1.82 +	have ya: "y1 + y2 = y \<and> a1 + a2 = a" using E HE _ y x0
    1.83 +	proof (rule decomp_H') txt_raw {* \label{decomp-H-use} *}
    1.84 +          from HE y1 y2 show "y1 + y2 \<in> H"
    1.85 +            by (rule subspace.add_closed)
    1.86 +          from x0 and HE y y1 y2
    1.87 +          have "x0 \<in> E"  "y \<in> E"  "y1 \<in> E"  "y2 \<in> E" by auto
    1.88 +          with x1_rep x2_rep have "(y1 + y2) + (a1 + a2) \<cdot> x0 = x1 + x2"
    1.89 +            by (simp add: add_ac add_mult_distrib2)
    1.90 +          also note x1x2
    1.91 +          finally show "(y1 + y2) + (a1 + a2) \<cdot> x0 = y + a \<cdot> x0" .
    1.92 +	qed
    1.93 +	
    1.94 +	from h'_def x1x2 E HE y x0
    1.95 +	have "h' (x1 + x2) = h y + a * xi"
    1.96 +          by (rule h'_definite)
    1.97 +	also have "\<dots> = h (y1 + y2) + (a1 + a2) * xi"
    1.98 +          by (simp only: ya)
    1.99 +	also from y1 y2 have "h (y1 + y2) = h y1 + h y2"
   1.100 +          by simp
   1.101 +	also have "\<dots> + (a1 + a2) * xi = (h y1 + a1 * xi) + (h y2 + a2 * xi)"
   1.102 +          by (simp add: left_distrib)
   1.103 +	also from h'_def x1_rep E HE y1 x0
   1.104 +	have "h y1 + a1 * xi = h' x1"
   1.105 +          by (rule h'_definite [symmetric])
   1.106 +	also from h'_def x2_rep E HE y2 x0
   1.107 +	have "h y2 + a2 * xi = h' x2"
   1.108 +          by (rule h'_definite [symmetric])
   1.109 +	finally show ?thesis .
   1.110        qed
   1.111 -
   1.112 -      from h'_def x1x2 E HE y x0
   1.113 -      have "h' (x1 + x2) = h y + a * xi"
   1.114 -        by (rule h'_definite)
   1.115 -      also have "\<dots> = h (y1 + y2) + (a1 + a2) * xi"
   1.116 -        by (simp only: ya)
   1.117 -      also from y1 y2 have "h (y1 + y2) = h y1 + h y2"
   1.118 -        by simp
   1.119 -      also have "\<dots> + (a1 + a2) * xi = (h y1 + a1 * xi) + (h y2 + a2 * xi)"
   1.120 -        by (simp add: left_distrib)
   1.121 -      also from h'_def x1_rep E HE y1 x0
   1.122 -      have "h y1 + a1 * xi = h' x1"
   1.123 -        by (rule h'_definite [symmetric])
   1.124 -      also from h'_def x2_rep E HE y2 x0
   1.125 -      have "h y2 + a2 * xi = h' x2"
   1.126 -        by (rule h'_definite [symmetric])
   1.127 -      finally show ?thesis .
   1.128 -    qed
   1.129 -  next
   1.130 -    fix x1 c assume x1: "x1 \<in> H'"
   1.131 -    show "h' (c \<cdot> x1) = c * (h' x1)"
   1.132 -    proof -
   1.133 -      from H' x1 have ax1: "c \<cdot> x1 \<in> H'"
   1.134 -        by (rule vectorspace.mult_closed)
   1.135 -      with x1 obtain y a y1 a1 where
   1.136 -            cx1_rep: "c \<cdot> x1 = y + a \<cdot> x0" and y: "y \<in> H"
   1.137 +    next
   1.138 +      fix x1 c assume x1: "x1 \<in> H'"
   1.139 +      show "h' (c \<cdot> x1) = c * (h' x1)"
   1.140 +      proof -
   1.141 +	from H' x1 have ax1: "c \<cdot> x1 \<in> H'"
   1.142 +          by (rule vectorspace.mult_closed)
   1.143 +	with x1 obtain y a y1 a1 where
   1.144 +          cx1_rep: "c \<cdot> x1 = y + a \<cdot> x0" and y: "y \<in> H"
   1.145            and x1_rep: "x1 = y1 + a1 \<cdot> x0" and y1: "y1 \<in> H"
   1.146 -        by (unfold H'_def sum_def lin_def) blast
   1.147 -
   1.148 -      have ya: "c \<cdot> y1 = y \<and> c * a1 = a" using E HE _ y x0
   1.149 -      proof (rule decomp_H')
   1.150 -        from HE y1 show "c \<cdot> y1 \<in> H"
   1.151 -          by (rule subspace.mult_closed)
   1.152 -        from x0 and HE y y1
   1.153 -        have "x0 \<in> E"  "y \<in> E"  "y1 \<in> E" by auto
   1.154 -        with x1_rep have "c \<cdot> y1 + (c * a1) \<cdot> x0 = c \<cdot> x1"
   1.155 -          by (simp add: mult_assoc add_mult_distrib1)
   1.156 -        also note cx1_rep
   1.157 -        finally show "c \<cdot> y1 + (c * a1) \<cdot> x0 = y + a \<cdot> x0" .
   1.158 +          by (unfold H'_def sum_def lin_def) blast
   1.159 +	
   1.160 +	have ya: "c \<cdot> y1 = y \<and> c * a1 = a" using E HE _ y x0
   1.161 +	proof (rule decomp_H')
   1.162 +          from HE y1 show "c \<cdot> y1 \<in> H"
   1.163 +            by (rule subspace.mult_closed)
   1.164 +          from x0 and HE y y1
   1.165 +          have "x0 \<in> E"  "y \<in> E"  "y1 \<in> E" by auto
   1.166 +          with x1_rep have "c \<cdot> y1 + (c * a1) \<cdot> x0 = c \<cdot> x1"
   1.167 +            by (simp add: mult_assoc add_mult_distrib1)
   1.168 +          also note cx1_rep
   1.169 +          finally show "c \<cdot> y1 + (c * a1) \<cdot> x0 = y + a \<cdot> x0" .
   1.170 +	qed
   1.171 +	
   1.172 +	from h'_def cx1_rep E HE y x0 have "h' (c \<cdot> x1) = h y + a * xi"
   1.173 +          by (rule h'_definite)
   1.174 +	also have "\<dots> = h (c \<cdot> y1) + (c * a1) * xi"
   1.175 +          by (simp only: ya)
   1.176 +	also from y1 have "h (c \<cdot> y1) = c * h y1"
   1.177 +          by simp
   1.178 +	also have "\<dots> + (c * a1) * xi = c * (h y1 + a1 * xi)"
   1.179 +          by (simp only: right_distrib)
   1.180 +	also from h'_def x1_rep E HE y1 x0 have "h y1 + a1 * xi = h' x1"
   1.181 +          by (rule h'_definite [symmetric])
   1.182 +	finally show ?thesis .
   1.183        qed
   1.184 -
   1.185 -      from h'_def cx1_rep E HE y x0 have "h' (c \<cdot> x1) = h y + a * xi"
   1.186 -        by (rule h'_definite)
   1.187 -      also have "\<dots> = h (c \<cdot> y1) + (c * a1) * xi"
   1.188 -        by (simp only: ya)
   1.189 -      also from y1 have "h (c \<cdot> y1) = c * h y1"
   1.190 -        by simp
   1.191 -      also have "\<dots> + (c * a1) * xi = c * (h y1 + a1 * xi)"
   1.192 -        by (simp only: right_distrib)
   1.193 -      also from h'_def x1_rep E HE y1 x0 have "h y1 + a1 * xi = h' x1"
   1.194 -        by (rule h'_definite [symmetric])
   1.195 -      finally show ?thesis .
   1.196 -    qed
   1.197 -  }
   1.198 +    }
   1.199 +  qed
   1.200  qed
   1.201  
   1.202  text {* \medskip The linear extension @{text h'} of @{text h}
   1.203    is bounded by the seminorm @{text p}. *}
   1.204  
   1.205  lemma h'_norm_pres:
   1.206 -  includes var H + var h + var E
   1.207    assumes h'_def: "h' \<equiv> \<lambda>x. let (y, a) =
   1.208        SOME (y, a). x = y + a \<cdot> x0 \<and> y \<in> H in h y + a * xi"
   1.209      and H'_def: "H' \<equiv> H + lin x0"
   1.210      and x0: "x0 \<notin> H"  "x0 \<in> E"  "x0 \<noteq> 0"
   1.211 -  includes vectorspace E + subspace H E + seminorm E p + linearform H h
   1.212 +  assumes E: "vectorspace E" and HE: "subspace H E"
   1.213 +    and "seminorm E p" and "linearform H h"
   1.214    assumes a: "\<forall>y \<in> H. h y \<le> p y"
   1.215      and a': "\<forall>y \<in> H. - p (y + x0) - h y \<le> xi \<and> xi \<le> p (y + x0) - h y"
   1.216    shows "\<forall>x \<in> H'. h' x \<le> p x"
   1.217 -proof
   1.218 -  note E = `vectorspace E`
   1.219 -  note HE = `subspace H E`
   1.220 -  fix x assume x': "x \<in> H'"
   1.221 -  show "h' x \<le> p x"
   1.222 -  proof -
   1.223 -    from a' have a1: "\<forall>ya \<in> H. - p (ya + x0) - h ya \<le> xi"
   1.224 -      and a2: "\<forall>ya \<in> H. xi \<le> p (ya + x0) - h ya" by auto
   1.225 -    from x' obtain y a where
   1.226 +proof -
   1.227 +  interpret vectorspace [E] by fact
   1.228 +  interpret subspace [H E] by fact
   1.229 +  interpret seminorm [E p] by fact
   1.230 +  interpret linearform [H h] by fact
   1.231 +  show ?thesis proof
   1.232 +    fix x assume x': "x \<in> H'"
   1.233 +    show "h' x \<le> p x"
   1.234 +    proof -
   1.235 +      from a' have a1: "\<forall>ya \<in> H. - p (ya + x0) - h ya \<le> xi"
   1.236 +	and a2: "\<forall>ya \<in> H. xi \<le> p (ya + x0) - h ya" by auto
   1.237 +      from x' obtain y a where
   1.238          x_rep: "x = y + a \<cdot> x0" and y: "y \<in> H"
   1.239 -      by (unfold H'_def sum_def lin_def) blast
   1.240 -    from y have y': "y \<in> E" ..
   1.241 -    from y have ay: "inverse a \<cdot> y \<in> H" by simp
   1.242 -
   1.243 -    from h'_def x_rep E HE y x0 have "h' x = h y + a * xi"
   1.244 -      by (rule h'_definite)
   1.245 -    also have "\<dots> \<le> p (y + a \<cdot> x0)"
   1.246 -    proof (rule linorder_cases)
   1.247 -      assume z: "a = 0"
   1.248 -      then have "h y + a * xi = h y" by simp
   1.249 -      also from a y have "\<dots> \<le> p y" ..
   1.250 -      also from x0 y' z have "p y = p (y + a \<cdot> x0)" by simp
   1.251 -      finally show ?thesis .
   1.252 -    next
   1.253 -      txt {* In the case @{text "a < 0"}, we use @{text "a\<^sub>1"}
   1.254 -        with @{text ya} taken as @{text "y / a"}: *}
   1.255 -      assume lz: "a < 0" hence nz: "a \<noteq> 0" by simp
   1.256 -      from a1 ay
   1.257 -      have "- p (inverse a \<cdot> y + x0) - h (inverse a \<cdot> y) \<le> xi" ..
   1.258 -      with lz have "a * xi \<le>
   1.259 +	by (unfold H'_def sum_def lin_def) blast
   1.260 +      from y have y': "y \<in> E" ..
   1.261 +      from y have ay: "inverse a \<cdot> y \<in> H" by simp
   1.262 +      
   1.263 +      from h'_def x_rep E HE y x0 have "h' x = h y + a * xi"
   1.264 +	by (rule h'_definite)
   1.265 +      also have "\<dots> \<le> p (y + a \<cdot> x0)"
   1.266 +      proof (rule linorder_cases)
   1.267 +	assume z: "a = 0"
   1.268 +	then have "h y + a * xi = h y" by simp
   1.269 +	also from a y have "\<dots> \<le> p y" ..
   1.270 +	also from x0 y' z have "p y = p (y + a \<cdot> x0)" by simp
   1.271 +	finally show ?thesis .
   1.272 +      next
   1.273 +	txt {* In the case @{text "a < 0"}, we use @{text "a\<^sub>1"}
   1.274 +          with @{text ya} taken as @{text "y / a"}: *}
   1.275 +	assume lz: "a < 0" hence nz: "a \<noteq> 0" by simp
   1.276 +	from a1 ay
   1.277 +	have "- p (inverse a \<cdot> y + x0) - h (inverse a \<cdot> y) \<le> xi" ..
   1.278 +	with lz have "a * xi \<le>
   1.279            a * (- p (inverse a \<cdot> y + x0) - h (inverse a \<cdot> y))"
   1.280 -        by (simp add: mult_left_mono_neg order_less_imp_le)
   1.281 -
   1.282 -      also have "\<dots> =
   1.283 +          by (simp add: mult_left_mono_neg order_less_imp_le)
   1.284 +	
   1.285 +	also have "\<dots> =
   1.286            - a * (p (inverse a \<cdot> y + x0)) - a * (h (inverse a \<cdot> y))"
   1.287 -	by (simp add: right_diff_distrib)
   1.288 -      also from lz x0 y' have "- a * (p (inverse a \<cdot> y + x0)) =
   1.289 +	  by (simp add: right_diff_distrib)
   1.290 +	also from lz x0 y' have "- a * (p (inverse a \<cdot> y + x0)) =
   1.291            p (a \<cdot> (inverse a \<cdot> y + x0))"
   1.292 -        by (simp add: abs_homogenous)
   1.293 -      also from nz x0 y' have "\<dots> = p (y + a \<cdot> x0)"
   1.294 -        by (simp add: add_mult_distrib1 mult_assoc [symmetric])
   1.295 -      also from nz y have "a * (h (inverse a \<cdot> y)) =  h y"
   1.296 -        by simp
   1.297 -      finally have "a * xi \<le> p (y + a \<cdot> x0) - h y" .
   1.298 -      then show ?thesis by simp
   1.299 -    next
   1.300 -      txt {* In the case @{text "a > 0"}, we use @{text "a\<^sub>2"}
   1.301 -        with @{text ya} taken as @{text "y / a"}: *}
   1.302 -      assume gz: "0 < a" hence nz: "a \<noteq> 0" by simp
   1.303 -      from a2 ay
   1.304 -      have "xi \<le> p (inverse a \<cdot> y + x0) - h (inverse a \<cdot> y)" ..
   1.305 -      with gz have "a * xi \<le>
   1.306 +          by (simp add: abs_homogenous)
   1.307 +	also from nz x0 y' have "\<dots> = p (y + a \<cdot> x0)"
   1.308 +          by (simp add: add_mult_distrib1 mult_assoc [symmetric])
   1.309 +	also from nz y have "a * (h (inverse a \<cdot> y)) =  h y"
   1.310 +          by simp
   1.311 +	finally have "a * xi \<le> p (y + a \<cdot> x0) - h y" .
   1.312 +	then show ?thesis by simp
   1.313 +      next
   1.314 +	txt {* In the case @{text "a > 0"}, we use @{text "a\<^sub>2"}
   1.315 +          with @{text ya} taken as @{text "y / a"}: *}
   1.316 +	assume gz: "0 < a" hence nz: "a \<noteq> 0" by simp
   1.317 +	from a2 ay
   1.318 +	have "xi \<le> p (inverse a \<cdot> y + x0) - h (inverse a \<cdot> y)" ..
   1.319 +	with gz have "a * xi \<le>
   1.320            a * (p (inverse a \<cdot> y + x0) - h (inverse a \<cdot> y))"
   1.321 -        by simp
   1.322 -      also have "... = a * p (inverse a \<cdot> y + x0) - a * h (inverse a \<cdot> y)"
   1.323 -	by (simp add: right_diff_distrib)
   1.324 -      also from gz x0 y'
   1.325 -      have "a * p (inverse a \<cdot> y + x0) = p (a \<cdot> (inverse a \<cdot> y + x0))"
   1.326 -        by (simp add: abs_homogenous)
   1.327 -      also from nz x0 y' have "\<dots> = p (y + a \<cdot> x0)"
   1.328 -        by (simp add: add_mult_distrib1 mult_assoc [symmetric])
   1.329 -      also from nz y have "a * h (inverse a \<cdot> y) = h y"
   1.330 -        by simp
   1.331 -      finally have "a * xi \<le> p (y + a \<cdot> x0) - h y" .
   1.332 -      then show ?thesis by simp
   1.333 +          by simp
   1.334 +	also have "... = a * p (inverse a \<cdot> y + x0) - a * h (inverse a \<cdot> y)"
   1.335 +	  by (simp add: right_diff_distrib)
   1.336 +	also from gz x0 y'
   1.337 +	have "a * p (inverse a \<cdot> y + x0) = p (a \<cdot> (inverse a \<cdot> y + x0))"
   1.338 +          by (simp add: abs_homogenous)
   1.339 +	also from nz x0 y' have "\<dots> = p (y + a \<cdot> x0)"
   1.340 +          by (simp add: add_mult_distrib1 mult_assoc [symmetric])
   1.341 +	also from nz y have "a * h (inverse a \<cdot> y) = h y"
   1.342 +          by simp
   1.343 +	finally have "a * xi \<le> p (y + a \<cdot> x0) - h y" .
   1.344 +	then show ?thesis by simp
   1.345 +      qed
   1.346 +      also from x_rep have "\<dots> = p x" by (simp only:)
   1.347 +      finally show ?thesis .
   1.348      qed
   1.349 -    also from x_rep have "\<dots> = p x" by (simp only:)
   1.350 -    finally show ?thesis .
   1.351    qed
   1.352  qed
   1.353