src/HOL/Real/HahnBanach/FunctionOrder.thy
 changeset 7566 c5a3f980a7af parent 7535 599d3414b51d child 7656 2f18c0ffc348
```     1.1 --- a/src/HOL/Real/HahnBanach/FunctionOrder.thy	Tue Sep 21 17:30:55 1999 +0200
1.2 +++ b/src/HOL/Real/HahnBanach/FunctionOrder.thy	Tue Sep 21 17:31:20 1999 +0200
1.3 @@ -1,3 +1,7 @@
1.4 +(*  Title:      HOL/Real/HahnBanach/FunctionOrder.thy
1.5 +    ID:         \$Id\$
1.6 +    Author:     Gertrud Bauer, TU Munich
1.7 +*)
1.8
1.9  theory FunctionOrder = Subspace + Linearform:;
1.10
1.11 @@ -18,14 +22,30 @@
1.12    funct :: "'a graph => ('a => real)"
1.13    "funct g == %x. (@ y. (x, y):g)";
1.14
1.15 -lemma graph_I: "x:F ==> (x, f x) : graph F f";
1.16 +lemma graphI [intro!!]: "x:F ==> (x, f x) : graph F f";
1.17    by (unfold graph_def, intro CollectI exI) force;
1.18
1.19 -lemma graphD1: "(x, y): graph F f ==> x:F";
1.20 -  by (unfold graph_def, elim CollectD [elimify] exE) force;
1.21 +lemma graphI2 [intro!!]: "x:F ==> EX t: (graph F f). t = (x, f x)";
1.22 +  by (unfold graph_def, force);
1.23 +
1.24 +lemma graphD1 [intro!!]: "(x, y): graph F f ==> x:F";
1.25 +  by (unfold graph_def, elim CollectE exE) force;
1.26 +
1.27 +lemma graphD2 [intro!!]: "(x, y): graph H h ==> y = h x";
1.28 +  by (unfold graph_def, elim CollectE exE) force;
1.29
1.30 -lemma graph_domain_funct: "(!!x y z. (x, y):g ==> (x, z):g ==> z = y) ==> graph (domain g) (funct g) = g";
1.31 -proof ( unfold domain_def, unfold funct_def, unfold graph_def, auto);
1.32 +lemma graph_extD1 [intro!!]: "[| graph H h <= graph H' h'; x:H |] ==> h x = h' x";
1.33 +  by (unfold graph_def, force);
1.34 +
1.35 +lemma graph_extD2 [intro!!]: "[| graph H h <= graph H' h' |] ==> H <= H'";
1.36 +  by (unfold graph_def, force);
1.37 +
1.38 +lemma graph_extI: "[| !! x. x: H ==> h x = h' x; H <= H'|] ==> graph H h <= graph H' h'";
1.39 +  by (unfold graph_def, force);
1.40 +
1.41 +lemma graph_domain_funct:
1.42 +  "(!!x y z. (x, y):g ==> (x, z):g ==> z = y) ==> graph (domain g) (funct g) = g";
1.43 +proof (unfold domain_def, unfold funct_def, unfold graph_def, auto);
1.44    fix a b; assume "(a, b) : g";
1.45    show "(a, SOME y. (a, y) : g) : g"; by (rule selectI2);
1.46    show "EX y. (a, y) : g"; ..;
1.47 @@ -36,22 +56,6 @@
1.48    qed;
1.49  qed;
1.50
1.51 -lemma graph_lemma1: "x:F ==> EX t: (graph F f). t = (x, f x)";
1.52 -  by (unfold graph_def, force);
1.53 -
1.54 -lemma graph_lemma2: "(x, y): graph H h ==> y = h x";
1.55 -  by (unfold graph_def, elim CollectD [elimify] exE) force;
1.56 -
1.57 -lemma graph_lemma3: "[| graph H h <= graph H' h'; x:H |] ==> h x = h' x";
1.58 -  by (unfold graph_def, force);
1.59 -
1.60 -lemma graph_lemma4: "[| graph H h <= graph H' h' |] ==> H <= H'";
1.61 -  by (unfold graph_def, force);
1.62 -
1.63 -lemma graph_lemma5: "[| !! x. x: H ==> h x = h' x; H <= H'|] ==> graph H h <= graph H' h'";
1.64 -  by (unfold graph_def, force);
1.65 -
1.66 -
1.67  constdefs
1.68    norm_prev_extensions ::
1.69     "['a set, 'a  => real, 'a set, 'a => real] => 'a graph set"
1.70 @@ -71,7 +75,7 @@
1.71                                                & (ALL x:H. h x <= p x))";
1.72   by (unfold norm_prev_extensions_def) force;
1.73
1.74 -lemma norm_prev_extension_I2 [intro]:
1.75 +lemma norm_prev_extensionI2 [intro]:
1.76     "[| is_linearform H h;
1.77         is_subspace H E;
1.78         is_subspace F H;
1.79 @@ -80,7 +84,7 @@
1.80     ==> (graph H h : norm_prev_extensions E p F f)";
1.81   by (unfold norm_prev_extensions_def) force;
1.82
1.83 -lemma norm_prev_extension_I [intro]:
1.84 +lemma norm_prev_extensionI [intro]:
1.85     "(EX H h. graph H h = g
1.86               & is_linearform H h
1.87               & is_subspace H E
```