summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

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;