src/HOL/Real/HahnBanach/HahnBanach_h0_lemmas.thy
 changeset 7566 c5a3f980a7af parent 7535 599d3414b51d child 7656 2f18c0ffc348
```     1.1 --- a/src/HOL/Real/HahnBanach/HahnBanach_h0_lemmas.thy	Tue Sep 21 17:30:55 1999 +0200
1.2 +++ b/src/HOL/Real/HahnBanach/HahnBanach_h0_lemmas.thy	Tue Sep 21 17:31:20 1999 +0200
1.3 @@ -1,8 +1,12 @@
1.4 +(*  Title:      HOL/Real/HahnBanach/HahnBanach_h0_lemmas.thy
1.5 +    ID:         \$Id\$
1.6 +    Author:     Gertrud Bauer, TU Munich
1.7 +*)
1.8
1.9 -theory HahnBanach_h0_lemmas = FunctionOrder + NormedSpace + Zorn_Lemma + FunctionNorm + RComplete:;
1.10 +theory HahnBanach_h0_lemmas = FunctionNorm:;
1.11
1.12
1.13 -theorems [intro!!] = zero_in_vs isLub_isUb;
1.14 +theorems [intro!!] = isLub_isUb;
1.15
1.16  lemma ex_xi: "[| is_vectorspace F;  (!! u v. [| u:F; v:F |] ==> a u <= b v )|]
1.17         ==> EX xi::real. (ALL y:F. (a::'a => real) y <= xi) & (ALL y:F. xi <= b y)";
1.18 @@ -11,7 +15,7 @@
1.19    assume r: "(!! u v. [| u:F; v:F |] ==> a u <= (b v::real))";
1.20    have "EX t. isLub UNIV {s::real . EX u:F. s = a u} t";
1.21    proof (rule reals_complete);
1.22 -    have "a <0> : {s. EX u:F. s = a u}"; by force;
1.23 +    have "a <0> : {s. EX u:F. s = a u}"; by (force!);
1.24      thus "EX X. X : {s. EX u:F. s = a u}"; ..;
1.25
1.26      show "EX Y. isUb UNIV {s. EX u:F. s = a u} Y";
1.27 @@ -21,7 +25,7 @@
1.28          fix y; assume "y : {s. EX u:F. s = a u}";
1.29          show "y <= b <0>";
1.30          proof -;
1.31 -          have "EX u:F. y = a u"; by fast;
1.32 +          have "EX u:F. y = a u"; by (fast!);
1.33            thus ?thesis;
1.34            proof;
1.35              fix u; assume "u:F";
1.36 @@ -45,7 +49,7 @@
1.37        show "a y <= t";
1.38        proof (rule isUbD);
1.39          show"isUb UNIV {s. EX u:F. s = a u} t"; ..;
1.40 -      qed fast;
1.41 +      qed (fast!);
1.42      next;
1.43        fix y; assume "y:F";
1.44        show "t <= b y";
1.45 @@ -56,7 +60,7 @@
1.46            assume "au : {s. EX u:F. s = a u} ";
1.47            show "au <= b y";
1.48            proof -;
1.49 -            have "EX u:F. au = a u"; by fast;
1.50 +            have "EX u:F. au = a u"; by (fast!);
1.51              thus "au <= b y";
1.52              proof;
1.53                fix u; assume "u:F";
1.54 @@ -73,8 +77,6 @@
1.55  qed;
1.56
1.57
1.58 -theorems [dest!!] = vs_sumD linD;
1.59 -
1.60  lemma h0_lf:
1.61    "[| h0 = (%x. let (y, a) = @ (y, a). (x = y [+] a [*] x0 & y:H) in (h y) + a * xi);
1.62        H0 = vectorspace_sum H (lin x0); is_subspace H E; is_linearform H h; x0 ~: H;
1.63 @@ -87,7 +89,7 @@
1.64      and [simp]: "x0 : E" "is_vectorspace E";
1.65
1.66    have h0: "is_vectorspace H0";
1.67 -  proof (asm_simp, rule vs_sum_vs);
1.68 +  proof ((simp!), rule vs_sum_vs);
1.69      show "is_subspace (lin x0) E"; by (rule lin_subspace);
1.70    qed simp+;
1.71
1.72 @@ -98,11 +100,11 @@
1.73        by (rule vs_add_closed, rule h0);
1.74
1.75      have ex_x1: "? y1 a1. (x1 = y1 [+] a1 [*] x0  & y1 : H)";
1.76 -      by (asm_simp add: vectorspace_sum_def lin_def) blast;
1.77 +      by (simp! add: vectorspace_sum_def lin_def) blast;
1.78      have ex_x2: "? y2 a2. (x2 = y2 [+] a2 [*] x0 & y2 : H)";
1.79 -      by (asm_simp add: vectorspace_sum_def lin_def) blast;
1.80 +      by (simp! add: vectorspace_sum_def lin_def) blast;
1.81      from x1x2; have ex_x1x2: "? y a. (x1 [+] x2 = y [+] a [*] x0  & y : H)";
1.82 -      by (asm_simp add: vectorspace_sum_def lin_def) force;
1.83 +      by (simp! add: vectorspace_sum_def lin_def) force;
1.84      from ex_x1 ex_x2 ex_x1x2;
1.85      show "h0 (x1 [+] x2) = h0 x1 + h0 x2";
1.86      proof (elim exE conjE);
1.87 @@ -112,33 +114,33 @@
1.88               "x1 [+] x2 = y  [+] a  [*] x0" "y  : H";
1.89
1.90        have ya: "y1 [+] y2 = y & a1 + a2 = a";
1.91 -      proof (rule lemma4);
1.92 +      proof (rule decomp4);
1.93          show "y1 [+] y2 [+] (a1 + a2) [*] x0 = y [+] a [*] x0";
1.94          proof -;
1.95 -          have "y [+] a [*] x0 = x1 [+] x2"; by asm_simp;
1.96 -          also; have "... = y1 [+] a1 [*] x0 [+] (y2 [+] a2 [*] x0)"; by asm_simp;
1.97 -          also; have "... = y1 [+] y2 [+] (a1 [*] x0 [+] a2 [*] x0)";
1.98 -            by asm_simp_tac;
1.99 +          have "y [+] a [*] x0 = x1 [+] x2"; by (simp!);
1.100 +          also; have "... = y1 [+] a1 [*] x0 [+] (y2 [+] a2 [*] x0)"; by (simp!);
1.101 +          also; from prems; have "... = y1 [+] y2 [+] (a1 [*] x0 [+] a2 [*] x0)";
1.102 +	    by asm_simp_tac;   (* FIXME !?? *)
1.103           also; have "... = y1 [+] y2 [+] (a1 + a2) [*] x0";
1.106            finally; show ?thesis; by (rule sym);
1.107          qed;
1.108 -        show "y1 [+] y2 : H"; by (rule subspace_add_closed);
1.109 +        show "y1 [+] y2 : H"; ..;
1.110        qed;
1.111        have y: "y1 [+] y2 = y"; by (rule conjunct1 [OF ya]);
1.112        have a: "a1 + a2 = a";  by (rule conjunct2 [OF ya]);
1.113
1.114        have "h0 (x1 [+] x2) = h y + a * xi";
1.115 -	by (rule lemma3);
1.116 -      also; have "... = h (y1 [+] y2) + (a1 + a2) * xi"; by (asm_simp add: y a);
1.117 +	by (rule decomp3);
1.118 +      also; have "... = h (y1 [+] y2) + (a1 + a2) * xi"; by (simp! add: y a);
1.119        also; have  "... = h y1 + h y2 + a1 * xi + a2 * xi";
1.121 -      also; have "... = (h y1 + a1 * xi) + (h y2 + a2 * xi)"; by asm_simp;
1.123 +      also; have "... = (h y1 + a1 * xi) + (h y2 + a2 * xi)"; by (simp!);
1.124        also; have "... = h0 x1 + h0 x2";
1.125        proof -;
1.126 -        have x1: "h0 x1 = h y1 + a1 * xi"; by (rule lemma3);
1.127 -        have x2: "h0 x2 = h y2 + a2 * xi"; by (rule lemma3);
1.128 -        from x1 x2; show ?thesis; by asm_simp;
1.129 +        have x1: "h0 x1 = h y1 + a1 * xi"; by (rule decomp3);
1.130 +        have x2: "h0 x2 = h y2 + a2 * xi"; by (rule decomp3);
1.131 +        from x1 x2; show ?thesis; by (simp!);
1.132        qed;
1.133        finally; show ?thesis; .;
1.134      qed;
1.135 @@ -149,9 +151,9 @@
1.136      have ax1: "c [*] x1 : H0";
1.137        by (rule vs_mult_closed, rule h0);
1.138      have ex_x1: "? y1 a1. (x1 = y1 [+] a1 [*] x0 & y1 : H)";
1.139 -      by (asm_simp add: vectorspace_sum_def lin_def, fast);
1.140 +      by (simp! add: vectorspace_sum_def lin_def, fast);
1.141      have ex_x: "!! x. x: H0 ==> ? y a. (x = y [+] a [*] x0 & y : H)";
1.142 -      by (asm_simp add: vectorspace_sum_def lin_def, fast);
1.143 +      by (simp! add: vectorspace_sum_def lin_def, fast);
1.144      note ex_ax1 = ex_x [of "c [*] x1", OF ax1];
1.145      from ex_x1 ex_ax1; show "h0 (c [*] x1) = c * (h0 x1)";
1.146      proof (elim exE conjE);
1.147 @@ -160,34 +162,34 @@
1.148  	     "c [*] x1 = y  [+] a  [*] x0" "y  : H";
1.149
1.150        have ya: "c [*] y1 = y & c * a1 = a";
1.151 -      proof (rule lemma4);
1.152 +      proof (rule decomp4);
1.153  	show "c [*] y1 [+] (c * a1) [*] x0 = y [+] a [*] x0";
1.154  	proof -;
1.155 -          have "y [+] a [*] x0 = c [*] x1"; by asm_simp;
1.156 -          also; have "... = c [*] (y1 [+] a1 [*] x0)"; by asm_simp;
1.157 -          also; have "... = c [*] y1 [+] c [*] (a1 [*] x0)";
1.159 -          also; have "... = c [*] y1 [+] (c * a1) [*] x0";
1.160 -            by (asm_simp_tac);
1.161 +          have "y [+] a [*] x0 = c [*] x1"; by (simp!);
1.162 +          also; have "... = c [*] (y1 [+] a1 [*] x0)"; by (simp!);
1.163 +          also; from prems; have "... = c [*] y1 [+] c [*] (a1 [*] x0)";
1.165 +          also; from prems; have "... = c [*] y1 [+] (c * a1) [*] x0";
1.166 +            by asm_simp_tac;
1.167            finally; show ?thesis; by (rule sym);
1.168          qed;
1.169 -        show "c [*] y1: H"; by (rule subspace_mult_closed);
1.170 +        show "c [*] y1: H"; ..;
1.171        qed;
1.172        have y: "c [*] y1 = y"; by (rule conjunct1 [OF ya]);
1.173        have a: "c * a1 = a"; by (rule conjunct2 [OF ya]);
1.174
1.175        have "h0 (c [*] x1) = h y + a * xi";
1.176 -	by (rule lemma3);
1.177 +	by (rule decomp3);
1.178        also; have "... = h (c [*] y1) + (c * a1) * xi";
1.179 -        by (asm_simp add: y a);
1.180 +        by (simp! add: y a);
1.181        also; have  "... = c * h y1 + c * a1 * xi";
1.184        also; have "... = c * (h y1 + a1 * xi)";
1.187        also; have "... = c * (h0 x1)";
1.188        proof -;
1.189 -        have "h0 x1 = h y1 + a1 * xi"; by (rule lemma3);
1.190 -        thus ?thesis; by asm_simp;
1.191 +        have "h0 x1 = h y1 + a1 * xi"; by (rule decomp3);
1.192 +        thus ?thesis; by (simp!);
1.193        qed;
1.194        finally; show ?thesis; .;
1.195      qed;
1.196 @@ -211,7 +213,7 @@
1.197    show "h0 x <= p x";
1.198    proof -;
1.199      have ex_x: "!! x. x : H0 ==> ? y a. (x = y [+] a [*] x0 & y : H)";
1.200 -      by (asm_simp add: vectorspace_sum_def lin_def, fast);
1.201 +      by (simp! add: vectorspace_sum_def lin_def, fast);
1.202      have "? y a. (x = y [+] a [*] x0 & y : H)";
1.203        by (rule ex_x);
1.204      thus ?thesis;
1.205 @@ -220,16 +222,16 @@
1.206        show ?thesis;
1.207        proof -;
1.208          have "h0 x = h y + a * xi";
1.209 -          by (rule lemma3);
1.210 +          by (rule decomp3);
1.211          also; have "... <= p (y [+] a [*] x0)";
1.212 -        proof (rule real_linear [of a "0r", elimify], elim disjE); (* case distinction *)
1.213 +        proof (rule real_linear [of a "0r", elimify], elim disjE); (*** case distinction ***)
1.214            assume lz: "a < 0r";
1.215            hence nz: "a ~= 0r"; by force;
1.216            show ?thesis;
1.217            proof -;
1.218              from a1; have "- p (rinv a [*] y [+] x0) - h (rinv a [*] y) <= xi";
1.219              proof (rule bspec);
1.220 -              show "(rinv a) [*] y : H"; by (rule subspace_mult_closed);
1.221 +              show "(rinv a) [*] y : H"; ..;
1.222              qed;
1.223              with lz; have "a * xi <= a * (- p (rinv a [*] y [+] x0) - h (rinv a [*] y))";
1.224                by (rule real_mult_less_le_anti);
1.225 @@ -241,52 +243,46 @@
1.226                  by (rule rabs_minus_eqI2);
1.227                thus ?thesis; by simp;
1.228              qed;
1.229 -            also; have "... =  p (a [*] (rinv a [*] y [+] x0)) - a * (h (rinv a [*] y))";
1.230 -              by (asm_simp, asm_simp_tac add: quasinorm_mult_distrib);
1.231 +            also; from prems; have "... =  p (a [*] (rinv a [*] y [+] x0)) - a * (h (rinv a [*] y))";
1.232 +              by (simp!, asm_simp_tac add: quasinorm_mult_distrib);
1.233              also; have "... = p ((a * rinv a) [*] y [+] a [*] x0) - a * (h (rinv a [*] y))";
1.234              proof simp;
1.235                have "a [*] (rinv a [*] y [+] x0) = a [*] rinv a [*] y [+] a [*] x0";
1.236 -                by (rule vs_add_mult_distrib1) asm_simp+;
1.237 +                by (rule vs_add_mult_distrib1) (simp!)+;
1.238                also; have "... = (a * rinv a) [*] y [+] a [*] x0";
1.239 -                by asm_simp;
1.240 +                by (simp!);
1.241                finally; have "a [*] (rinv a [*] y [+] x0) = (a * rinv a) [*] y [+] a [*] x0";.;
1.242                thus "p (a [*] (rinv a [*] y [+] x0)) = p ((a * rinv a) [*] y [+] a [*] x0)";
1.243                  by simp;
1.244              qed;
1.245              also; from nz; have "... = p (y [+] a [*] x0) - (a * (h (rinv a [*] y)))";
1.246 -              by asm_simp;
1.247 -            also; from nz; have "... = p (y [+] a [*] x0) - (h y)";
1.248 -            proof asm_simp;
1.249 -              have "a * (h (rinv a [*] y)) = h (a [*] (rinv a [*] y))";
1.250 +              by (simp!);
1.251 +            also; have "a * (h (rinv a [*] y)) = h y";
1.252 +	    proof -;
1.253 +              from prems; have "a * (h (rinv a [*] y)) = h (a [*] (rinv a [*] y))";
1.254                  by (asm_simp_tac add: linearform_mult_linear [RS sym]);
1.255 -              also; have "... = h y";
1.256 -              proof -;
1.257 -                from nz; have "a [*] (rinv a [*] y) = y"; by asm_simp;
1.258 -                thus ?thesis; by simp;
1.259 -              qed;
1.260 -              finally; have "a * (h (rinv a [*] y)) = h y"; .;
1.261 -              thus "- (a * (h (rinv a [*] y))) = - (h y)"; by simp;
1.262 +	      also; from nz; have "a [*] (rinv a [*] y) = y"; by (simp!);
1.263 +              finally; show ?thesis; .;
1.264              qed;
1.265 -            finally; have "a * xi <= p (y [+] a [*] x0) - h y"; .;
1.266 +            finally; have "a * xi <= p (y [+] a [*] x0) - ..."; .;
1.267              hence "h y + a * xi <= h y + (p (y [+] a [*] x0) - h y)";
1.268                by (rule real_add_left_cancel_le [RS iffD2]); (* arith *)
1.269              thus ?thesis;
1.270                by force;
1.271 -          qed;
1.272 -
1.273 +	  qed;
1.274          next;
1.275            assume "a = 0r"; show ?thesis;
1.276            proof -;
1.277 -            have "h y + a * xi = h y"; by asm_simp;
1.278 +            have "h y + a * xi = h y"; by (simp!);
1.279              also; from a; have "... <= p y"; ..;
1.280              also; have "... = p (y [+] a [*] x0)";
1.281              proof -;
1.282 -              have "y = y [+] <0>"; by asm_simp;
1.283 +              have "y = y [+] <0>"; by (simp!);
1.284                also; have "... = y [+] a [*] x0";
1.285                proof -;
1.286                  have "<0> = 0r [*] x0";
1.287 -                  by asm_simp;
1.288 -                also; have "... = a [*] x0"; by asm_simp;
1.289 +                  by (simp!);
1.290 +                also; have "... = a [*] x0"; by (simp!);
1.291                  finally; have "<0> = a [*] x0";.;
1.292                  thus ?thesis; by simp;
1.293                qed;
1.294 @@ -302,7 +298,7 @@
1.295            proof -;
1.296              from a2; have "xi <= p (rinv a [*] y [+] x0) - h (rinv a [*] y)";
1.297              proof (rule bspec);
1.298 -              show "rinv a [*] y : H"; by (rule subspace_mult_closed);
1.299 +              show "rinv a [*] y : H"; ..;
1.300              qed;
1.301              with gz; have "a * xi <= a * (p (rinv a [*] y [+] x0) - h (rinv a [*] y))";
1.302                by (rule real_mult_less_le_mono);
1.303 @@ -314,27 +310,27 @@
1.304                  by (rule rabs_eqI2);
1.305                thus ?thesis; by simp;
1.306              qed;
1.307 -            also; have "... =  p (a [*] (rinv a [*] y [+] x0)) - a * (h (rinv a [*] y))";
1.308 -              by (asm_simp, asm_simp_tac add: quasinorm_mult_distrib);
1.309 +            also; from prems; have "... =  p (a [*] (rinv a [*] y [+] x0)) - a * (h (rinv a [*] y))";
1.310 +              by (simp, asm_simp_tac add: quasinorm_mult_distrib);
1.311              also; have "... = p ((a * rinv a) [*] y [+] a [*] x0) - a * (h (rinv a [*] y))";
1.312              proof simp;
1.313                have "a [*] (rinv a [*] y [+] x0) = a [*] rinv a [*] y [+] a [*] x0";
1.314 -                by (rule vs_add_mult_distrib1) asm_simp+;
1.315 +                by (rule vs_add_mult_distrib1) (simp!)+;
1.316                also; have "... = (a * rinv a) [*] y [+] a [*] x0";
1.317 -                by asm_simp;
1.318 +                by (simp!);
1.319                finally; have "a [*] (rinv a [*] y [+] x0) = (a * rinv a) [*] y [+] a [*] x0";.;
1.320                thus "p (a [*] (rinv a [*] y [+] x0)) = p ((a * rinv a) [*] y [+] a [*] x0)";
1.321                  by simp;
1.322              qed;
1.323              also; from nz; have "... = p (y [+] a [*] x0) - (a * (h (rinv a [*] y)))";
1.324 -              by asm_simp;
1.325 +              by (simp!);
1.326              also; from nz; have "... = p (y [+] a [*] x0) - (h y)";
1.327 -            proof asm_simp;
1.328 +            proof (simp!);
1.329                have "a * (h (rinv a [*] y)) = h (a [*] (rinv a [*] y))";
1.330 -                by (rule linearform_mult_linear [RS sym]) asm_simp+;
1.331 +                by (rule linearform_mult_linear [RS sym]) (simp!)+;
1.332                also; have "... = h y";
1.333                proof -;
1.334 -                from nz; have "a [*] (rinv a [*] y) = y"; by asm_simp;
1.335 +                from nz; have "a [*] (rinv a [*] y) = y"; by (simp!);
1.336                  thus ?thesis; by simp;
1.337                qed;
1.338                finally; have "a * (h (rinv a [*] y)) = h y"; .;
1.339 @@ -347,7 +343,7 @@
1.340                by force;
1.341            qed;
1.342          qed;
1.343 -        also; have "... = p x"; by asm_simp;
1.344 +        also; have "... = p x"; by (simp!);
1.345          finally; show ?thesis; .;
1.346        qed;
1.347      qed;
```