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.104 -            by (asm_simp add: vs_add_mult_distrib2[of E]);
   1.105 +            by (simp! add: vs_add_mult_distrib2[of E]);
   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.120 -	by (asm_simp add: linearform_add_linear [of H] real_add_mult_distrib);
   1.121 -      also; have "... = (h y1 + a1 * xi) + (h y2 + a2 * xi)"; by asm_simp;
   1.122 +	by (simp! add: linearform_add_linear [of H] real_add_mult_distrib);
   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.158 -            by (asm_simp_tac add: vs_add_mult_distrib1);
   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.164 +            by (asm_simp_tac add: vs_add_mult_distrib1);  (* FIXME *)
   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.182 -	by (asm_simp add: linearform_mult_linear [of H] real_add_mult_distrib);
   1.183 +	by (simp! add: linearform_mult_linear [of H] real_add_mult_distrib);
   1.184        also; have "... = c * (h y1 + a1 * xi)"; 
   1.185 -	by (asm_simp add: real_add_mult_distrib2 real_mult_assoc);
   1.186 +	by (simp! add: real_add_mult_distrib2 real_mult_assoc);
   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;