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.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;
```