22 |
22 |
23 constdefs |
23 constdefs |
24 graph :: "['a set, 'a => real] => 'a graph " |
24 graph :: "['a set, 'a => real] => 'a graph " |
25 "graph F f == {(x, f x) | x. x \\<in> F}" |
25 "graph F f == {(x, f x) | x. x \\<in> F}" |
26 |
26 |
27 lemma graphI [intro??]: "x \\<in> F ==> (x, f x) \\<in> graph F f" |
27 lemma graphI [intro?]: "x \\<in> F ==> (x, f x) \\<in> graph F f" |
28 by (unfold graph_def, intro CollectI exI) force |
28 by (unfold graph_def, intro CollectI exI) force |
29 |
29 |
30 lemma graphI2 [intro??]: "x \\<in> F ==> \\<exists>t\\<in> (graph F f). t = (x, f x)" |
30 lemma graphI2 [intro?]: "x \\<in> F ==> \\<exists>t\\<in> (graph F f). t = (x, f x)" |
31 by (unfold graph_def, force) |
31 by (unfold graph_def, force) |
32 |
32 |
33 lemma graphD1 [intro??]: "(x, y) \\<in> graph F f ==> x \\<in> F" |
33 lemma graphD1 [intro?]: "(x, y) \\<in> graph F f ==> x \\<in> F" |
34 by (unfold graph_def, elim CollectE exE) force |
34 by (unfold graph_def, elim CollectE exE) force |
35 |
35 |
36 lemma graphD2 [intro??]: "(x, y) \\<in> graph H h ==> y = h x" |
36 lemma graphD2 [intro?]: "(x, y) \\<in> graph H h ==> y = h x" |
37 by (unfold graph_def, elim CollectE exE) force |
37 by (unfold graph_def, elim CollectE exE) force |
38 |
38 |
39 subsection {* Functions ordered by domain extension *} |
39 subsection {* Functions ordered by domain extension *} |
40 |
40 |
41 text{* A function $h'$ is an extension of $h$, iff the graph of |
41 text{* A function $h'$ is an extension of $h$, iff the graph of |
44 lemma graph_extI: |
44 lemma graph_extI: |
45 "[| !! x. x \\<in> H ==> h x = h' x; H <= H'|] |
45 "[| !! x. x \\<in> H ==> h x = h' x; H <= H'|] |
46 ==> graph H h <= graph H' h'" |
46 ==> graph H h <= graph H' h'" |
47 by (unfold graph_def, force) |
47 by (unfold graph_def, force) |
48 |
48 |
49 lemma graph_extD1 [intro??]: |
49 lemma graph_extD1 [intro?]: |
50 "[| graph H h <= graph H' h'; x \\<in> H |] ==> h x = h' x" |
50 "[| graph H h <= graph H' h'; x \\<in> H |] ==> h x = h' x" |
51 by (unfold graph_def, force) |
51 by (unfold graph_def, force) |
52 |
52 |
53 lemma graph_extD2 [intro??]: |
53 lemma graph_extD2 [intro?]: |
54 "[| graph H h <= graph H' h' |] ==> H <= H'" |
54 "[| graph H h <= graph H' h' |] ==> H <= H'" |
55 by (unfold graph_def, force) |
55 by (unfold graph_def, force) |
56 |
56 |
57 subsection {* Domain and function of a graph *} |
57 subsection {* Domain and function of a graph *} |
58 |
58 |