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