src/HOL/Real/HahnBanach/HahnBanach_lemmas.thy
changeset 7566 c5a3f980a7af
parent 7535 599d3414b51d
child 7656 2f18c0ffc348
     1.1 --- a/src/HOL/Real/HahnBanach/HahnBanach_lemmas.thy	Tue Sep 21 17:30:55 1999 +0200
     1.2 +++ b/src/HOL/Real/HahnBanach/HahnBanach_lemmas.thy	Tue Sep 21 17:31:20 1999 +0200
     1.3 @@ -1,9 +1,10 @@
     1.4 -
     1.5 -theory HahnBanach_lemmas = FunctionOrder + NormedSpace + Zorn_Lemma + FunctionNorm + RComplete:;
     1.6 +(*  Title:      HOL/Real/HahnBanach/HahnBanach_lemmas.thy
     1.7 +    ID:         $Id$
     1.8 +    Author:     Gertrud Bauer, TU Munich
     1.9 +*)
    1.10  
    1.11 +theory HahnBanach_lemmas = FunctionNorm + Zorn_Lemma:;
    1.12  
    1.13 -theorems [dest!!] = subsetD;
    1.14 -theorems [intro!!] = subspace_subset; 
    1.15  
    1.16  lemma rabs_ineq: "[| is_subspace H E; is_vectorspace E; is_quasinorm E p; is_linearform H h |] \
    1.17   \ ==>  (ALL x:H. rabs (h x) <= p x)  = ( ALL x:H. h x <= p x)" (concl is "?L = ?R");
    1.18 @@ -17,7 +18,7 @@
    1.19      proof (intro ballI); 
    1.20        fix x; assume "x:H";
    1.21        have "h x <= rabs (h x)"; by (rule rabs_ge_self);
    1.22 -      also; have "rabs (h x) <= p x"; by fast;
    1.23 +      also; have "rabs (h x) <= p x"; by (fast!);
    1.24        finally; show "h x <= p x"; .;
    1.25      qed;
    1.26    next;
    1.27 @@ -34,15 +35,12 @@
    1.28  	  from H; have "- h x = h ([-] x)"; by (rule linearform_neg_linear [RS sym]);
    1.29  	  also; from r; have "... <= p ([-] x)"; 
    1.30  	  proof -; 
    1.31 -	    from H; have "[-] x : H"; by asm_simp;
    1.32 +	    from H; have "[-] x : H"; by (simp!);
    1.33              with r; show ?thesis; ..;
    1.34            qed;
    1.35  	  also; have "... = p x"; 
    1.36            proof (rule quasinorm_minus);
    1.37 -            show "x:E";
    1.38 -            proof (rule subsetD);
    1.39 -              show "H <= E"; ..; 
    1.40 -            qed;
    1.41 +            show "x:E"; ..;
    1.42            qed;
    1.43  	  finally; show "- h x <= p x"; .; 
    1.44  	qed;
    1.45 @@ -69,12 +67,12 @@
    1.46                      & (ALL x:H. h x <= p x)";
    1.47  
    1.48    have "EX t : (graph H h). t = (x, h x)"; 
    1.49 -    by (rule graph_lemma1);
    1.50 +    by (rule graphI2);
    1.51    thus ?thesis;
    1.52    proof (elim bexE); 
    1.53      fix t; assume "t : (graph H h)" and "t = (x, h x)";
    1.54      have ex1: "EX g:c. t:g";
    1.55 -      by (asm_simp only: Union_iff);
    1.56 +      by (simp! only: Union_iff);
    1.57      thus ?thesis;
    1.58      proof (elim bexE);
    1.59        fix g; assume "g:c" "t:g";
    1.60 @@ -85,9 +83,9 @@
    1.61        qed;
    1.62        have "EX H' h'. graph H' h' = g & ?P H' h'"; 
    1.63        proof (rule norm_prev_extension_D);
    1.64 -        from gM; show "g: norm_prev_extensions E p F f"; by asm_simp;
    1.65 +        from gM; show "g: norm_prev_extensions E p F f"; by (simp!);
    1.66        qed;
    1.67 -      thus ?thesis; by (elim exE conjE, intro exI conjI) (asm_simp+);
    1.68 +      thus ?thesis; by (elim exE conjE, intro exI conjI) (simp | simp!)+;
    1.69      qed;
    1.70    qed;
    1.71  qed;
    1.72 @@ -111,12 +109,13 @@
    1.73      assume "t : graph H h" "t = (x, h x)" "graph H' h' : c" "t : graph H' h'" 
    1.74             "is_linearform H' h'" "is_subspace H' E" "is_subspace F H'" 
    1.75             "graph F f <= graph H' h'" "ALL x:H'. h' x <= p x";
    1.76 -    show x: "x:H'"; by (asm_simp, rule graphD1);
    1.77 +    show x: "x:H'"; by (simp!, rule graphD1);
    1.78      show "graph H' h' <= graph H h";
    1.79 -      by (asm_simp only: chain_ball_Union_upper);
    1.80 +      by (simp! only: chain_ball_Union_upper);
    1.81    qed;
    1.82  qed;
    1.83  
    1.84 +theorems [trans] = subsetD [COMP swap_prems_rl];
    1.85  
    1.86  lemma some_H'h'2: 
    1.87    "[| M = norm_prev_extensions E p F f; c: chain M; graph H h = Union c; x:H; y:H|] 
    1.88 @@ -159,28 +158,33 @@
    1.89      proof; 
    1.90        assume "(graph H'' h'') <= (graph H' h')";
    1.91        show ?thesis;
    1.92 -      proof (intro exI conjI);
    1.93 -	have xh: "(x, h x): graph H' h'"; by (fast);
    1.94 +      proof (intro exI conjI); note [trans] = subsetD;
    1.95 +        have "(x, h x) : graph H'' h''"; by (simp!);
    1.96 +	also; have "... <= graph H' h'"; by (simp!); 
    1.97 +        finally; have xh: "(x, h x): graph H' h'"; .;
    1.98  	thus x: "x:H'"; by (rule graphD1);
    1.99 -	show y: "y:H'"; by (asm_simp, rule graphD1);
   1.100 +	show y: "y:H'"; by (simp!, rule graphD1);
   1.101  	show "(graph H' h') <= (graph H h)";
   1.102 -	  by (asm_simp only: chain_ball_Union_upper);
   1.103 +	  by (simp! only: chain_ball_Union_upper);
   1.104        qed;
   1.105      next;
   1.106        assume "(graph H' h') <= (graph H'' h'')";
   1.107        show ?thesis;
   1.108        proof (intro exI conjI);
   1.109 -	show x: "x:H''"; by (asm_simp, rule graphD1);
   1.110 -	have yh: "(y, h y): graph H'' h''"; by (fast);
   1.111 +	show x: "x:H''"; by (simp!, rule graphD1);
   1.112 +        have "(y, h y) : graph H' h'"; by (simp!);
   1.113 +        also; have "... <= graph H'' h''"; by (simp!);
   1.114 +	finally; have yh: "(y, h y): graph H'' h''"; .;
   1.115          thus y: "y:H''"; by (rule graphD1);
   1.116          show "(graph H'' h'') <= (graph H h)";
   1.117 -          by (asm_simp only: chain_ball_Union_upper);
   1.118 +          by (simp! only: chain_ball_Union_upper);
   1.119        qed;
   1.120      qed;
   1.121    qed;
   1.122  qed;
   1.123  
   1.124 -
   1.125 +lemmas chainE2 = chainD2 [elimify];
   1.126 +lemmas [intro!!] = subsetD chainD; 
   1.127  
   1.128  lemma sup_uniq: "[| is_vectorspace E; is_subspace F E; is_quasinorm E p; is_linearform F f;
   1.129         ALL x:F. f x <= p x; M == norm_prev_extensions E p F f; c : chain M;
   1.130 @@ -188,33 +192,33 @@
   1.131       ==> z = y";
   1.132  proof -;
   1.133    assume "M == norm_prev_extensions E p F f" "c : chain M" "(x, y) : Union c" " (x, z) : Union c";
   1.134 -  have "EX H h. (x, y) : graph H h & (x, z) : graph H h"; 
   1.135 -  proof (elim UnionE chainD2 [elimify]); 
   1.136 +  hence "EX H h. (x, y) : graph H h & (x, z) : graph H h"; 
   1.137 +  proof (elim UnionE chainE2); 
   1.138      fix G1 G2; assume "(x, y) : G1" "G1 : c" "(x, z) : G2" "G2 : c" "c <= M";
   1.139 -    have "G1 : M"; by (rule subsetD);
   1.140 +    have "G1 : M"; ..;
   1.141      hence e1: "EX H1 h1. graph H1 h1 = G1";  
   1.142 -      by (force dest: norm_prev_extension_D);
   1.143 -    have "G2 : M"; by (rule subsetD);
   1.144 +      by (force! dest: norm_prev_extension_D);
   1.145 +    have "G2 : M"; ..;
   1.146      hence e2: "EX H2 h2. graph H2 h2 = G2";  
   1.147 -      by (force dest: norm_prev_extension_D);
   1.148 +      by (force! dest: norm_prev_extension_D);
   1.149      from e1 e2; show ?thesis; 
   1.150      proof (elim exE);
   1.151        fix H1 h1 H2 h2; assume "graph H1 h1 = G1" "graph H2 h2 = G2";
   1.152 -      have "G1 <= G2 | G2 <= G1"; by (rule chainD);
   1.153 +      have "G1 <= G2 | G2 <= G1"; ..;
   1.154        thus ?thesis;
   1.155        proof;
   1.156          assume "G1 <= G2";
   1.157          thus ?thesis;
   1.158          proof (intro exI conjI);
   1.159 -          show "(x, y) : graph H2 h2"; by force;
   1.160 -          show "(x, z) : graph H2 h2"; by asm_simp;
   1.161 +          show "(x, y) : graph H2 h2"; by (force!);
   1.162 +          show "(x, z) : graph H2 h2"; by (simp!);
   1.163          qed;
   1.164        next;
   1.165          assume "G2 <= G1";
   1.166          thus ?thesis;
   1.167          proof (intro exI conjI);
   1.168 -          show "(x, y) : graph H1 h1"; by asm_simp;
   1.169 -          show "(x, z) : graph H1 h1"; by force; 
   1.170 +          show "(x, y) : graph H1 h1"; by (simp!);
   1.171 +          show "(x, z) : graph H1 h1"; by (force!);
   1.172          qed;
   1.173        qed;
   1.174      qed;
   1.175 @@ -222,8 +226,8 @@
   1.176    thus ?thesis; 
   1.177    proof (elim exE conjE);
   1.178      fix H h; assume "(x, y) : graph H h" "(x, z) : graph H h";
   1.179 -    have "y = h x"; by (rule graph_lemma2);
   1.180 -    also; have "h x = z"; by (rule graph_lemma2 [RS sym]);
   1.181 +    have "y = h x"; ..;
   1.182 +    also; have "... = z"; by (rule sym, rule);
   1.183      finally; show "z = y"; by (rule sym);
   1.184    qed;
   1.185  qed;
   1.186 @@ -254,17 +258,16 @@
   1.187          fix H' h'; assume "x:H'" "y:H'" 
   1.188            and b: "graph H' h' <= graph H h" 
   1.189            and "is_linearform H' h'" "is_subspace H' E";
   1.190 -        have h'x: "h' x = h x"; by (rule graph_lemma3); 
   1.191 -        have h'y: "h' y = h y"; by (rule graph_lemma3);
   1.192 +        have h'x: "h' x = h x"; ..;
   1.193 +        have h'y: "h' y = h y"; ..;
   1.194          have h'xy: "h' (x [+] y) = h' x + h' y"; by (rule linearform_add_linear);
   1.195          have "h' (x [+] y) = h (x [+] y)";  
   1.196          proof -;
   1.197 -          have "x [+] y : H'";
   1.198 -            by (rule subspace_add_closed);
   1.199 -          with b; show ?thesis; by (rule graph_lemma3);
   1.200 +          have "x [+] y : H'"; ..;
   1.201 +          with b; show ?thesis; ..;
   1.202          qed;
   1.203          with h'x h'y h'xy; show ?thesis;
   1.204 -          by asm_simp; 
   1.205 +          by (simp!); 
   1.206        qed;
   1.207      qed;
   1.208  
   1.209 @@ -281,16 +284,15 @@
   1.210  	fix H' h';
   1.211  	assume b: "graph H' h' <= graph H h";
   1.212  	assume "x:H'" "is_linearform H' h'" "is_subspace H' E";
   1.213 -	have h'x: "h' x = h x"; by (rule graph_lemma3);
   1.214 +	have h'x: "h' x = h x"; ..;
   1.215  	have h'ax: "h' (a [*] x) = a * h' x"; by (rule linearform_mult_linear);
   1.216  	have "h' (a [*] x) = h (a [*] x)";
   1.217  	proof -;
   1.218 -	  have "a [*] x : H'";
   1.219 -	    by (rule subspace_mult_closed);
   1.220 -	  with b; show ?thesis; by (rule graph_lemma3);
   1.221 +	  have "a [*] x : H'"; ..;
   1.222 +	  with b; show ?thesis; ..;
   1.223  	qed;
   1.224  	with h'x h'ax; show ?thesis;
   1.225 -	  by asm_simp;
   1.226 +	  by (simp!);
   1.227        qed;
   1.228      qed;
   1.229    qed;
   1.230 @@ -303,14 +305,14 @@
   1.231    assume "M = norm_prev_extensions E p F f" "c: chain M"  "graph H h = Union c"
   1.232      and  e: "EX x. x:c";
   1.233   
   1.234 -  show ?thesis; 
   1.235 +  thus ?thesis; 
   1.236    proof (elim exE);
   1.237      fix x; assume "x:c"; 
   1.238      show ?thesis;    
   1.239      proof -;
   1.240        have "x:norm_prev_extensions E p F f"; 
   1.241        proof (rule subsetD);
   1.242 -	show "c <= norm_prev_extensions E p F f"; by (asm_simp add: chainD2);
   1.243 +	show "c <= norm_prev_extensions E p F f"; by (simp! add: chainD2);
   1.244        qed;
   1.245   
   1.246        hence "(EX G g. graph G g = x
   1.247 @@ -319,15 +321,15 @@
   1.248                      & is_subspace F G
   1.249                      & (graph F f <= graph G g) 
   1.250                      & (ALL x:G. g x <= p x))";
   1.251 -	by (asm_simp add: norm_prev_extension_D);
   1.252 +	by (simp! add: norm_prev_extension_D);
   1.253  
   1.254        thus ?thesis; 
   1.255        proof (elim exE conjE); 
   1.256  	fix G g; assume "graph G g = x" "graph F f <= graph G g";
   1.257  	show ?thesis; 
   1.258          proof -; 
   1.259 -          have "graph F f <= graph G g"; by assumption;
   1.260 -          also; have "graph G g <= graph H h"; by (asm_simp, fast);
   1.261 +          have "graph F f <= graph G g"; .;
   1.262 +          also; have "graph G g <= graph H h"; by ((simp!), fast);
   1.263            finally; show ?thesis; .;
   1.264          qed;
   1.265        qed;
   1.266 @@ -343,22 +345,22 @@
   1.267      "is_subspace F E";
   1.268  
   1.269    show ?thesis; 
   1.270 -  proof (rule subspace_I);
   1.271 -    show "<0> : F"; by (rule zero_in_subspace); 
   1.272 +  proof (rule subspaceI);
   1.273 +    show "<0> : F"; ..;
   1.274      show "F <= H"; 
   1.275 -    proof (rule graph_lemma4);
   1.276 +    proof (rule graph_extD2);
   1.277        show "graph F f <= graph H h";
   1.278          by (rule sup_ext);
   1.279      qed;
   1.280      show "ALL x:F. ALL y:F. x [+] y : F"; 
   1.281      proof (intro ballI); 
   1.282        fix x y; assume "x:F" "y:F";
   1.283 -      show "x [+] y : F"; by asm_simp;
   1.284 +      show "x [+] y : F"; by (simp!);
   1.285      qed;
   1.286      show "ALL x:F. ALL a. a [*] x : F";
   1.287      proof (intro ballI allI);
   1.288        fix x a; assume "x:F";
   1.289 -      show "a [*] x : F"; by asm_simp;
   1.290 +      show "a [*] x : F"; by (simp!);
   1.291      qed;
   1.292    qed;
   1.293  qed;
   1.294 @@ -371,13 +373,13 @@
   1.295      "is_subspace F E";
   1.296  
   1.297    show ?thesis; 
   1.298 -  proof (rule subspace_I);
   1.299 +  proof;
   1.300  
   1.301      show "<0> : H"; 
   1.302      proof (rule subsetD [of F H]);
   1.303        have "is_subspace F H"; by (rule sup_supF);
   1.304 -      thus "F <= H"; by (rule subspace_subset);
   1.305 -      show  "<0> :F"; by (rule zero_in_subspace); 
   1.306 +      thus "F <= H"; ..;
   1.307 +      show  "<0> : F"; ..;
   1.308      qed;
   1.309  
   1.310      show "H <= E"; 
   1.311 @@ -394,8 +396,7 @@
   1.312  	  fix H' h'; assume "x:H'" "is_subspace H' E";
   1.313  	  show "x:E"; 
   1.314  	  proof (rule subsetD);
   1.315 -	    show "H' <= E";
   1.316 -	      by (rule subspace_subset);    
   1.317 +	    show "H' <= E"; ..;
   1.318  	  qed;
   1.319  	qed;
   1.320        qed;
   1.321 @@ -413,10 +414,10 @@
   1.322  	thus ?thesis;
   1.323  	proof (elim exE conjE); 
   1.324  	  fix H' h'; assume "x:H'" "y:H'" "is_subspace H' E" "graph H' h' <= graph H h";
   1.325 -	  have "H' <= H"; by (rule graph_lemma4);
   1.326 +	  have "H' <= H"; ..;
   1.327  	  thus ?thesis;
   1.328  	  proof (rule subsetD);
   1.329 -	    show "x [+] y : H'"; by (rule subspace_add_closed);
   1.330 +	    show "x [+] y : H'"; ..; 
   1.331  	  qed;
   1.332  	qed;
   1.333        qed;
   1.334 @@ -434,10 +435,10 @@
   1.335  	thus ?thesis;
   1.336  	proof (elim exE conjE);
   1.337  	  fix H' h'; assume "x:H'" "is_subspace H' E" "graph H' h' <= graph H h";
   1.338 -  	  have "H' <= H"; by (rule graph_lemma4);
   1.339 +  	  have "H' <= H"; ..;
   1.340  	  thus ?thesis;
   1.341  	  proof (rule subsetD);
   1.342 -	    show "a [*] x : H'"; by (rule subspace_mult_closed);
   1.343 +	    show "a [*] x : H'"; ..;
   1.344  	  qed;
   1.345  	qed;
   1.346        qed;
   1.347 @@ -461,8 +462,8 @@
   1.348      proof (elim exE conjE);
   1.349        fix H' h'; assume "x: H'" "graph H' h' <= graph H h" and a: "ALL x: H'. h' x <= p x" ;
   1.350        have "h x = h' x"; 
   1.351 -      proof(rule sym); 
   1.352 -        show "h' x = h x"; by (rule graph_lemma3);
   1.353 +      proof (rule sym); 
   1.354 +        show "h' x = h x"; ..;
   1.355        qed;
   1.356        also; from a; have "... <= p x "; ..;
   1.357        finally; show ?thesis; .;  
   1.358 @@ -471,4 +472,4 @@
   1.359  qed;
   1.360  
   1.361  
   1.362 -end;
   1.363 \ No newline at end of file
   1.364 +end;