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