src/HOL/Real/HahnBanach/HahnBanach_lemmas.thy
changeset 7917 5e5b9813cce7
parent 7916 3cb310f40a3a
child 7918 2979b3b75dbd
     1.1 --- a/src/HOL/Real/HahnBanach/HahnBanach_lemmas.thy	Fri Oct 22 18:41:00 1999 +0200
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,497 +0,0 @@
     1.4 -(*  Title:      HOL/Real/HahnBanach/HahnBanach_lemmas.thy
     1.5 -    ID:         $Id$
     1.6 -    Author:     Gertrud Bauer, TU Munich
     1.7 -*)
     1.8 -
     1.9 -header {* Lemmas about the supremal function w.r.t.~the function order *};
    1.10 -
    1.11 -theory HahnBanach_lemmas = FunctionNorm + Zorn_Lemma:;
    1.12 -
    1.13 -lemma rabs_ineq: 
    1.14 -  "[| is_subspace H E; is_vectorspace E; is_quasinorm E p; is_linearform H h |] 
    1.15 -  ==>  (ALL x:H. rabs (h x) <= p x)  = ( ALL x:H. h x <= p x)" 
    1.16 -  (concl is "?L = ?R");
    1.17 -proof -;
    1.18 -  assume "is_subspace H E" "is_vectorspace E" "is_quasinorm E p" 
    1.19 -         "is_linearform H h";
    1.20 -  have h: "is_vectorspace H"; ..;
    1.21 -  show ?thesis;
    1.22 -  proof; 
    1.23 -    assume l: ?L;
    1.24 -    then; show ?R;
    1.25 -    proof (intro ballI); 
    1.26 -      fix x; assume x: "x:H";
    1.27 -      have "h x <= rabs (h x)"; by (rule rabs_ge_self);
    1.28 -      also; from l; have "... <= p x"; ..;
    1.29 -      finally; show "h x <= p x"; .;
    1.30 -    qed;
    1.31 -  next;
    1.32 -    assume r: ?R;
    1.33 -    then; show ?L;
    1.34 -    proof (intro ballI);
    1.35 -      fix x; assume "x:H";
    1.36 - 
    1.37 -      show "rabs (h x) <= p x"; 
    1.38 -      proof -; 
    1.39 -        show "!! r x. [| - r <= x; x <= r |] ==> rabs x <= r";
    1.40 -          by arith;
    1.41 -	show "- p x <= h x";
    1.42 -	proof (rule real_minus_le);
    1.43 -	  from h; have "- h x = h ([-] x)"; 
    1.44 -            by (rule linearform_neg_linear [RS sym]);
    1.45 -	  also; from r; have "... <= p ([-] x)"; by (simp!);
    1.46 -	  also; have "... = p x"; 
    1.47 -            by (rule quasinorm_minus, rule subspace_subsetD);
    1.48 -	  finally; show "- h x <= p x"; .; 
    1.49 -	qed;
    1.50 -	from r; show "h x <= p x"; ..; 
    1.51 -      qed;
    1.52 -    qed;
    1.53 -  qed;
    1.54 -qed;  
    1.55 -
    1.56 -lemma  some_H'h't:
    1.57 -  "[| M = norm_pres_extensions E p F f; c: chain M; graph H h = Union c; 
    1.58 -  x:H|]
    1.59 -   ==> EX H' h' t. t : (graph H h) & t = (x, h x) & (graph H' h'):c 
    1.60 -                 & t:graph H' h' & is_linearform H' h' & is_subspace H' E 
    1.61 -                 & is_subspace F H' & (graph F f <= graph H' h') 
    1.62 -                 & (ALL x:H'. h' x <= p x)";
    1.63 -proof -;
    1.64 -  assume m: "M = norm_pres_extensions E p F f" and cM: "c: chain M" 
    1.65 -     and u: "graph H h = Union c" "x:H";
    1.66 -
    1.67 -  let ?P = "%H h. is_linearform H h
    1.68 -                    & is_subspace H E
    1.69 -                    & is_subspace F H
    1.70 -                    & (graph F f <= graph H h)
    1.71 -                    & (ALL x:H. h x <= p x)";
    1.72 -
    1.73 -  have "EX t : (graph H h). t = (x, h x)"; 
    1.74 -    by (rule graphI2);
    1.75 -  thus ?thesis;
    1.76 -  proof (elim bexE); 
    1.77 -    fix t; assume t: "t : (graph H h)" "t = (x, h x)";
    1.78 -    with u; have ex1: "EX g:c. t:g";
    1.79 -      by (simp only: Union_iff);
    1.80 -    thus ?thesis;
    1.81 -    proof (elim bexE);
    1.82 -      fix g; assume g: "g:c" "t:g";
    1.83 -      from cM; have "c <= M"; by (rule chainD2);
    1.84 -      hence "g : M"; ..;
    1.85 -      hence "g : norm_pres_extensions E p F f"; by (simp only: m);
    1.86 -      hence "EX H' h'. graph H' h' = g & ?P H' h'"; 
    1.87 -        by (rule norm_pres_extension_D);
    1.88 -      thus ?thesis; by (elim exE conjE, intro exI conjI) (simp | simp!)+;
    1.89 -    qed;
    1.90 -  qed;
    1.91 -qed;
    1.92 -      
    1.93 -lemma some_H'h': "[| M = norm_pres_extensions E p F f; c: chain M; 
    1.94 -  graph H h = Union c; x:H|] 
    1.95 -  ==> EX H' h'. x:H' & (graph H' h' <= graph H h) & 
    1.96 -                is_linearform H' h' & is_subspace H' E & is_subspace F H' & 
    1.97 -                (graph F f <= graph H' h') & (ALL x:H'. h' x <= p x)"; 
    1.98 -proof -;
    1.99 -  assume m: "M = norm_pres_extensions E p F f" and cM: "c: chain M" 
   1.100 -     and u: "graph H h = Union c" "x:H";  
   1.101 -  have "(x, h x): graph H h"; by (rule graphI); 
   1.102 -  also; have "... = Union c"; .;
   1.103 -  finally; have "(x, h x) : Union c"; .;
   1.104 -  hence "EX g:c. (x, h x):g"; by (simp only: Union_iff);
   1.105 -  thus ?thesis; 
   1.106 -  proof (elim bexE);
   1.107 -    fix g; assume g: "g:c" "(x, h x):g";
   1.108 -    from cM; have "c <= M"; by (rule chainD2);
   1.109 -    hence "g : M"; ..;
   1.110 -    hence "g : norm_pres_extensions E p F f"; by (simp only: m);
   1.111 -    hence "EX H' h'. graph H' h' = g 
   1.112 -                   & is_linearform H' h'
   1.113 -                   & is_subspace H' E
   1.114 -                   & is_subspace F H'
   1.115 -                   & (graph F f <= graph H' h')
   1.116 -                   & (ALL x:H'. h' x <= p x)"; 
   1.117 -      by (rule norm_pres_extension_D);
   1.118 -    thus ?thesis; 
   1.119 -    proof (elim exE conjE, intro exI conjI);
   1.120 -      fix H' h'; assume g': "graph H' h' = g";
   1.121 -      with g; have "(x, h x): graph H' h'"; by simp;
   1.122 -      thus "x:H'"; by (rule graphD1);
   1.123 -      from g g'; have "graph H' h' : c"; by simp;
   1.124 -      with cM u; show "graph H' h' <= graph H h"; 
   1.125 -        by (simp only: chain_ball_Union_upper);
   1.126 -    qed simp+;
   1.127 -  qed;
   1.128 -qed;
   1.129 -
   1.130 -lemma some_H'h'2: 
   1.131 -  "[| M = norm_pres_extensions E p F f; c: chain M; graph H h = Union c; 
   1.132 -  x:H; y:H|] 
   1.133 -  ==> EX H' h'. x:H' & y:H' & (graph H' h' <= graph H h) 
   1.134 -  & is_linearform H' h' & is_subspace H' E & is_subspace F H' & 
   1.135 -                (graph F f <= graph H' h') & (ALL x:H'. h' x <= p x)"; 
   1.136 -proof -;
   1.137 -  assume "M = norm_pres_extensions E p F f" "c: chain M" 
   1.138 -         "graph H h = Union c";
   1.139 - 
   1.140 -  let ?P = "%H h. is_linearform H h 
   1.141 -                    & is_subspace H E 
   1.142 -                    & is_subspace F H
   1.143 -                    & (graph F f <= graph H h)
   1.144 -                    & (ALL x:H. h x <= p x)";
   1.145 -  assume "x:H";
   1.146 -  have e1: "EX H' h' t. t : (graph H h) & t = (x, h x) & (graph H' h'):c 
   1.147 -                      & t:graph H' h' & ?P H' h'";
   1.148 -    by (rule some_H'h't); 
   1.149 -  assume "y:H";
   1.150 -  have e2: "EX H' h' t. t : (graph H h) & t = (y, h y) & (graph H' h'):c 
   1.151 -                      & t:graph H' h' & ?P H' h'";
   1.152 -    by (rule some_H'h't); 
   1.153 -
   1.154 -  from e1 e2; show ?thesis; 
   1.155 -  proof (elim exE conjE);
   1.156 -    fix H' h' t' H'' h'' t''; 
   1.157 -    assume "t' : graph H h"             "t'' : graph H h" 
   1.158 -           "t' = (y, h y)"              "t'' = (x, h x)"
   1.159 -           "graph H' h' : c"            "graph H'' h'' : c"
   1.160 -           "t' : graph H' h'"           "t'' : graph H'' h''" 
   1.161 -           "is_linearform H' h'"        "is_linearform H'' h''"
   1.162 -           "is_subspace H' E"           "is_subspace H'' E"
   1.163 -           "is_subspace F H'"           "is_subspace F H''"
   1.164 -           "graph F f <= graph H' h'"   "graph F f <= graph H'' h''"
   1.165 -           "ALL x:H'. h' x <= p x"      "ALL x:H''. h'' x <= p x";
   1.166 -
   1.167 -    have "(graph H'' h'') <= (graph H' h') 
   1.168 -         | (graph H' h') <= (graph H'' h'')";
   1.169 -      by (rule chainD);
   1.170 -    thus "?thesis";
   1.171 -    proof; 
   1.172 -      assume "(graph H'' h'') <= (graph H' h')";
   1.173 -      show ?thesis;
   1.174 -      proof (intro exI conjI);
   1.175 -        note [trans] = subsetD;
   1.176 -        have "(x, h x) : graph H'' h''"; by (simp!);
   1.177 -	also; have "... <= graph H' h'"; .;
   1.178 -        finally; have xh: "(x, h x): graph H' h'"; .;
   1.179 -	thus x: "x:H'"; by (rule graphD1);
   1.180 -	show y: "y:H'"; by (simp!, rule graphD1);
   1.181 -	show "(graph H' h') <= (graph H h)";
   1.182 -	  by (simp! only: chain_ball_Union_upper);
   1.183 -      qed;
   1.184 -    next;
   1.185 -      assume "(graph H' h') <= (graph H'' h'')";
   1.186 -      show ?thesis;
   1.187 -      proof (intro exI conjI);
   1.188 -	show x: "x:H''"; by (simp!, rule graphD1);
   1.189 -        have "(y, h y) : graph H' h'"; by (simp!);
   1.190 -        also; have "... <= graph H'' h''"; .;
   1.191 -	finally; have yh: "(y, h y): graph H'' h''"; .;
   1.192 -        thus y: "y:H''"; by (rule graphD1);
   1.193 -        show "(graph H'' h'') <= (graph H h)";
   1.194 -          by (simp! only: chain_ball_Union_upper);
   1.195 -      qed;
   1.196 -    qed;
   1.197 -  qed;
   1.198 -qed;
   1.199 -
   1.200 -lemma sup_uniq: 
   1.201 -  "[| is_vectorspace E; is_subspace F E; is_quasinorm E p; 
   1.202 -  is_linearform F f; ALL x:F. f x <= p x; M == norm_pres_extensions E p F f;
   1.203 -   c : chain M; EX x. x : c; (x, y) : Union c; (x, z) : Union c |]
   1.204 -   ==> z = y";
   1.205 -proof -;
   1.206 -  assume "M == norm_pres_extensions E p F f" "c : chain M" 
   1.207 -         "(x, y) : Union c" " (x, z) : Union c";
   1.208 -  hence "EX H h. (x, y) : graph H h & (x, z) : graph H h"; 
   1.209 -  proof (elim UnionE chainE2); 
   1.210 -    fix G1 G2; 
   1.211 -    assume "(x, y) : G1" "G1 : c" "(x, z) : G2" "G2 : c" "c <= M";
   1.212 -    have "G1 : M"; ..;
   1.213 -    hence e1: "EX H1 h1. graph H1 h1 = G1";  
   1.214 -      by (force! dest: norm_pres_extension_D);
   1.215 -    have "G2 : M"; ..;
   1.216 -    hence e2: "EX H2 h2. graph H2 h2 = G2";  
   1.217 -      by (force! dest: norm_pres_extension_D);
   1.218 -    from e1 e2; show ?thesis; 
   1.219 -    proof (elim exE);
   1.220 -      fix H1 h1 H2 h2; assume "graph H1 h1 = G1" "graph H2 h2 = G2";
   1.221 -      have "G1 <= G2 | G2 <= G1"; ..;
   1.222 -      thus ?thesis;
   1.223 -      proof;
   1.224 -        assume "G1 <= G2";
   1.225 -        thus ?thesis;
   1.226 -        proof (intro exI conjI);
   1.227 -          show "(x, y) : graph H2 h2"; by (force!);
   1.228 -          show "(x, z) : graph H2 h2"; by (simp!);
   1.229 -        qed;
   1.230 -      next;
   1.231 -        assume "G2 <= G1";
   1.232 -        thus ?thesis;
   1.233 -        proof (intro exI conjI);
   1.234 -          show "(x, y) : graph H1 h1"; by (simp!);
   1.235 -          show "(x, z) : graph H1 h1"; by (force!);
   1.236 -        qed;
   1.237 -      qed;
   1.238 -    qed;
   1.239 -  qed;
   1.240 -  thus ?thesis; 
   1.241 -  proof (elim exE conjE);
   1.242 -    fix H h; assume "(x, y) : graph H h" "(x, z) : graph H h";
   1.243 -    have "y = h x"; ..;
   1.244 -    also; have "... = z"; by (rule sym, rule);
   1.245 -    finally; show "z = y"; by (rule sym);
   1.246 -  qed;
   1.247 -qed;
   1.248 -
   1.249 -lemma sup_lf: 
   1.250 -  "[| M = norm_pres_extensions E p F f; c: chain M; graph H h = Union c|] 
   1.251 -   ==> is_linearform H h";
   1.252 -proof -; 
   1.253 -  assume "M = norm_pres_extensions E p F f" "c: chain M"
   1.254 -         "graph H h = Union c";
   1.255 - 
   1.256 -  let ?P = "%H h. is_linearform H h 
   1.257 -                    & is_subspace H E 
   1.258 -                    & is_subspace F H
   1.259 -                    & (graph F f <= graph H h)
   1.260 -                    & (ALL x:H. h x <= p x)";
   1.261 -
   1.262 -  show "is_linearform H h";
   1.263 -  proof;
   1.264 -    fix x y; assume "x : H" "y : H"; 
   1.265 -    show "h (x [+] y) = h x + h y"; 
   1.266 -    proof -;
   1.267 -      have "EX H' h'. x:H' & y:H' & (graph H' h' <= graph H h) 
   1.268 -                    & is_linearform H' h' & is_subspace H' E 
   1.269 -                    & is_subspace F H' &  (graph F f <= graph H' h') 
   1.270 -                    & (ALL x:H'. h' x <= p x)";
   1.271 -        by (rule some_H'h'2);
   1.272 -      thus ?thesis; 
   1.273 -      proof (elim exE conjE);
   1.274 -        fix H' h'; assume "x:H'" "y:H'" 
   1.275 -          and b: "graph H' h' <= graph H h" 
   1.276 -          and "is_linearform H' h'" "is_subspace H' E";
   1.277 -        have h'x: "h' x = h x"; ..;
   1.278 -        have h'y: "h' y = h y"; ..;
   1.279 -        have h'xy: "h' (x [+] y) = h' x + h' y"; 
   1.280 -          by (rule linearform_add_linear);
   1.281 -        have "h' (x [+] y) = h (x [+] y)";  
   1.282 -        proof -;
   1.283 -          have "x [+] y : H'"; ..;
   1.284 -          with b; show ?thesis; ..;
   1.285 -        qed;
   1.286 -        with h'x h'y h'xy; show ?thesis;
   1.287 -          by (simp!); 
   1.288 -      qed;
   1.289 -    qed;
   1.290 -  next;  
   1.291 -    fix a x; assume  "x : H";
   1.292 -    show "h (a [*] x) = a * (h x)"; 
   1.293 -    proof -;
   1.294 -      have "EX H' h'. x:H' & (graph H' h' <= graph H h) 
   1.295 -                    & is_linearform H' h' & is_subspace H' E
   1.296 -                    & is_subspace F H' & (graph F f <= graph H' h') 
   1.297 -                    & (ALL x:H'. h' x <= p x)";
   1.298 -	by (rule some_H'h');
   1.299 -      thus ?thesis; 
   1.300 -      proof (elim exE conjE);
   1.301 -	fix H' h';
   1.302 -	assume b: "graph H' h' <= graph H h";
   1.303 -	assume "x:H'" "is_linearform H' h'" "is_subspace H' E";
   1.304 -	have h'x: "h' x = h x"; ..;
   1.305 -	have h'ax: "h' (a [*] x) = a * h' x"; 
   1.306 -          by (rule linearform_mult_linear);
   1.307 -	have "h' (a [*] x) = h (a [*] x)";
   1.308 -	proof -;
   1.309 -	  have "a [*] x : H'"; ..;
   1.310 -	  with b; show ?thesis; ..;
   1.311 -	qed;
   1.312 -	with h'x h'ax; show ?thesis;
   1.313 -	  by (simp!);
   1.314 -      qed;
   1.315 -    qed;
   1.316 -  qed;
   1.317 -qed;
   1.318 -
   1.319 -lemma sup_ext:
   1.320 -  "[| M = norm_pres_extensions E p F f; c: chain M; EX x. x:c; 
   1.321 -  graph H h = Union c|] ==> graph F f <= graph H h";
   1.322 -proof -;
   1.323 -  assume "M = norm_pres_extensions E p F f" "c: chain M" 
   1.324 -         "graph H h = Union c"
   1.325 -  and e: "EX x. x:c";
   1.326 - 
   1.327 -  thus ?thesis; 
   1.328 -  proof (elim exE);
   1.329 -    fix x; assume "x:c"; 
   1.330 -    show ?thesis;    
   1.331 -    proof -;
   1.332 -      have "x:norm_pres_extensions E p F f"; 
   1.333 -      proof (rule subsetD);
   1.334 -	show "c <= norm_pres_extensions E p F f"; by (simp! add: chainD2);
   1.335 -      qed;
   1.336 - 
   1.337 -      hence "(EX G g. graph G g = x
   1.338 -                    & is_linearform G g 
   1.339 -                    & is_subspace G E
   1.340 -                    & is_subspace F G
   1.341 -                    & (graph F f <= graph G g) 
   1.342 -                    & (ALL x:G. g x <= p x))";
   1.343 -	by (simp! add: norm_pres_extension_D);
   1.344 -
   1.345 -      thus ?thesis; 
   1.346 -      proof (elim exE conjE); 
   1.347 -	fix G g; assume "graph G g = x" "graph F f <= graph G g";
   1.348 -	show ?thesis; 
   1.349 -        proof -; 
   1.350 -          have "graph F f <= graph G g"; .;
   1.351 -          also; have "graph G g <= graph H h"; by ((simp!), fast);
   1.352 -          finally; show ?thesis; .;
   1.353 -        qed;
   1.354 -      qed;
   1.355 -    qed;
   1.356 -  qed;
   1.357 -qed;
   1.358 -
   1.359 -
   1.360 -lemma sup_supF: 
   1.361 -  "[| M = norm_pres_extensions E p F f; c: chain M; EX x. x:c;
   1.362 -  graph H h = Union c; is_subspace F E |] ==> is_subspace F H";
   1.363 -proof -; 
   1.364 -  assume "M = norm_pres_extensions E p F f" "c: chain M" "EX x. x:c" 
   1.365 -         "graph H h = Union c"
   1.366 -    "is_subspace F E";
   1.367 -
   1.368 -  show ?thesis; 
   1.369 -  proof (rule subspaceI);
   1.370 -    show "<0> : F"; ..;
   1.371 -    show "F <= H"; 
   1.372 -    proof (rule graph_extD2);
   1.373 -      show "graph F f <= graph H h";
   1.374 -        by (rule sup_ext);
   1.375 -    qed;
   1.376 -    show "ALL x:F. ALL y:F. x [+] y : F"; 
   1.377 -    proof (intro ballI); 
   1.378 -      fix x y; assume "x:F" "y:F";
   1.379 -      show "x [+] y : F"; by (simp!);
   1.380 -    qed;
   1.381 -    show "ALL x:F. ALL a. a [*] x : F";
   1.382 -    proof (intro ballI allI);
   1.383 -      fix x a; assume "x:F";
   1.384 -      show "a [*] x : F"; by (simp!);
   1.385 -    qed;
   1.386 -  qed;
   1.387 -qed;
   1.388 -
   1.389 -
   1.390 -lemma sup_subE: 
   1.391 -  "[| M = norm_pres_extensions E p F f; c: chain M; EX x. x:c; 
   1.392 -  graph H h = Union c; is_subspace F E|] ==> is_subspace H E";
   1.393 -proof -; 
   1.394 -  assume "M = norm_pres_extensions E p F f" "c: chain M" "EX x. x:c" 
   1.395 -         "graph H h = Union c" "is_subspace F E";
   1.396 -
   1.397 -  show ?thesis; 
   1.398 -  proof;
   1.399 -
   1.400 -    show "<0> : H"; 
   1.401 -    proof (rule subsetD [of F H]);
   1.402 -      have "is_subspace F H"; by (rule sup_supF);
   1.403 -      thus "F <= H"; ..;
   1.404 -      show  "<0> : F"; ..;
   1.405 -    qed;
   1.406 -
   1.407 -    show "H <= E"; 
   1.408 -    proof;
   1.409 -      fix x; assume "x:H";
   1.410 -      show "x:E";
   1.411 -      proof -;
   1.412 -	have "EX H' h'. x:H' & (graph H' h' <= graph H h) 
   1.413 -              & is_linearform H' h' & is_subspace H' E & is_subspace F H' 
   1.414 -              & (graph F f <= graph H' h') & (ALL x:H'. h' x <= p x)"; 
   1.415 -	  by (rule some_H'h');
   1.416 -	thus ?thesis;
   1.417 -	proof (elim exE conjE);
   1.418 -	  fix H' h'; assume "x:H'" "is_subspace H' E";
   1.419 -	  show "x:E"; 
   1.420 -	  proof (rule subsetD);
   1.421 -	    show "H' <= E"; ..;
   1.422 -	  qed;
   1.423 -	qed;
   1.424 -      qed;
   1.425 -    qed;
   1.426 -
   1.427 -    show "ALL x:H. ALL y:H. x [+] y : H"; 
   1.428 -    proof (intro ballI); 
   1.429 -      fix x y; assume "x:H" "y:H";
   1.430 -      show "x [+] y : H";   
   1.431 -      proof -;
   1.432 - 	have "EX H' h'. x:H' & y:H' & (graph H' h' <= graph H h) 
   1.433 -              & is_linearform H' h' & is_subspace H' E & is_subspace F H'
   1.434 -              & (graph F f <= graph H' h') & (ALL x:H'. h' x <= p x)"; 
   1.435 -	  by (rule some_H'h'2); 
   1.436 -	thus ?thesis;
   1.437 -	proof (elim exE conjE); 
   1.438 -	  fix H' h'; 
   1.439 -          assume "x:H'" "y:H'" "is_subspace H' E" 
   1.440 -                 "graph H' h' <= graph H h";
   1.441 -	  have "H' <= H"; ..;
   1.442 -	  thus ?thesis;
   1.443 -	  proof (rule subsetD);
   1.444 -	    show "x [+] y : H'"; ..; 
   1.445 -	  qed;
   1.446 -	qed;
   1.447 -      qed;
   1.448 -    qed;      
   1.449 -
   1.450 -    show "ALL x:H. ALL a. a [*] x : H"; 
   1.451 -    proof (intro ballI allI); 
   1.452 -      fix x and a::real; assume "x:H";
   1.453 -      show "a [*] x : H"; 
   1.454 -      proof -;
   1.455 -	have "EX H' h'. x:H' & (graph H' h' <= graph H h) & 
   1.456 -               is_linearform H' h' & is_subspace H' E & is_subspace F H' & 
   1.457 -               (graph F f <= graph H' h') & (ALL x:H'. h' x <= p x)"; 
   1.458 -	  by (rule some_H'h'); 
   1.459 -	thus ?thesis;
   1.460 -	proof (elim exE conjE);
   1.461 -	  fix H' h'; 
   1.462 -          assume "x:H'" "is_subspace H' E" "graph H' h' <= graph H h";
   1.463 -  	  have "H' <= H"; ..;
   1.464 -	  thus ?thesis;
   1.465 -	  proof (rule subsetD);
   1.466 -	    show "a [*] x : H'"; ..;
   1.467 -	  qed;
   1.468 -	qed;
   1.469 -      qed;
   1.470 -    qed;
   1.471 -  qed;
   1.472 -qed;
   1.473 -
   1.474 -lemma sup_norm_pres: "[| M = norm_pres_extensions E p F f; c: chain M; 
   1.475 -  graph H h = Union c|] ==> ALL x::'a:H. h x <= p x";
   1.476 -proof;
   1.477 -  assume "M = norm_pres_extensions E p F f" "c: chain M" 
   1.478 -         "graph H h = Union c";
   1.479 -  fix x; assume "x:H";
   1.480 -  show "h x <= p x"; 
   1.481 -  proof -; 
   1.482 -    have "EX H' h'. x:H' & (graph H' h' <= graph H h) 
   1.483 -                & is_linearform H' h' & is_subspace H' E & is_subspace F H'
   1.484 -                & (graph F f <= graph H' h') & (ALL x:H'. h' x <= p x)"; 
   1.485 -      by (rule some_H'h');
   1.486 -    thus ?thesis; 
   1.487 -    proof (elim exE conjE);
   1.488 -      fix H' h'; assume "x: H'" "graph H' h' <= graph H h" 
   1.489 -      and a: "ALL x: H'. h' x <= p x" ;
   1.490 -      have "h x = h' x"; 
   1.491 -      proof (rule sym); 
   1.492 -        show "h' x = h x"; ..;
   1.493 -      qed;
   1.494 -      also; from a; have "... <= p x "; ..;
   1.495 -      finally; show ?thesis; .;  
   1.496 -    qed;
   1.497 -  qed;
   1.498 -qed;
   1.499 -
   1.500 -end;
   1.501 \ No newline at end of file