--- a/src/HOL/Real/HahnBanach/FunctionOrder.thy Mon Jul 17 15:06:08 2000 +0200
+++ b/src/HOL/Real/HahnBanach/FunctionOrder.thy Mon Jul 17 18:17:54 2000 +0200
@@ -22,18 +22,18 @@
constdefs
graph :: "['a set, 'a => real] => 'a graph "
- "graph F f == {(x, f x) | x. x \<in> F}"
+ "graph F f == {(x, f x) | x. x \\<in> F}"
-lemma graphI [intro??]: "x \<in> F ==> (x, f x) \<in> graph F f"
+lemma graphI [intro??]: "x \\<in> F ==> (x, f x) \\<in> graph F f"
by (unfold graph_def, intro CollectI exI) force
-lemma graphI2 [intro??]: "x \<in> F ==> \<exists>t\<in> (graph F f). t = (x, f x)"
+lemma graphI2 [intro??]: "x \\<in> F ==> \\<exists>t\\<in> (graph F f). t = (x, f x)"
by (unfold graph_def, force)
-lemma graphD1 [intro??]: "(x, y) \<in> graph F f ==> x \<in> F"
+lemma graphD1 [intro??]: "(x, y) \\<in> graph F f ==> x \\<in> F"
by (unfold graph_def, elim CollectE exE) force
-lemma graphD2 [intro??]: "(x, y) \<in> graph H h ==> y = h x"
+lemma graphD2 [intro??]: "(x, y) \\<in> graph H h ==> y = h x"
by (unfold graph_def, elim CollectE exE) force
subsection {* Functions ordered by domain extension *}
@@ -42,12 +42,12 @@
$h$ is a subset of the graph of $h'$.*}
lemma graph_extI:
- "[| !! x. x \<in> H ==> h x = h' x; H <= H'|]
+ "[| !! x. x \\<in> H ==> h x = h' x; H <= H'|]
==> graph H h <= graph H' h'"
by (unfold graph_def, force)
lemma graph_extD1 [intro??]:
- "[| graph H h <= graph H' h'; x \<in> H |] ==> h x = h' x"
+ "[| graph H h <= graph H' h'; x \\<in> H |] ==> h x = h' x"
by (unfold graph_def, force)
lemma graph_extD2 [intro??]:
@@ -61,33 +61,26 @@
constdefs
domain :: "'a graph => 'a set"
- "domain g == {x. \<exists>y. (x, y) \<in> g}"
+ "domain g == {x. \\<exists>y. (x, y) \\<in> g}"
funct :: "'a graph => ('a => real)"
- "funct g == \<lambda>x. (SOME y. (x, y) \<in> g)"
+ "funct g == \\<lambda>x. (SOME y. (x, y) \\<in> g)"
-(*text{* The equations
-\begin{matharray}
-\idt{domain} graph F f = F {\rm and}\\
-\idt{funct} graph F f = f
-\end{matharray}
-hold, but are not proved here.
-*}*)
text {* The following lemma states that $g$ is the graph of a function
if the relation induced by $g$ is unique. *}
lemma graph_domain_funct:
- "(!!x y z. (x, y) \<in> g ==> (x, z) \<in> g ==> z = y)
+ "(!!x y z. (x, y) \\<in> g ==> (x, z) \\<in> g ==> z = y)
==> graph (domain g) (funct g) = g"
proof (unfold domain_def funct_def graph_def, auto)
- fix a b assume "(a, b) \<in> g"
- show "(a, SOME y. (a, y) \<in> g) \<in> g" by (rule selectI2)
- show "\<exists>y. (a, y) \<in> g" ..
- assume uniq: "!!x y z. (x, y) \<in> g ==> (x, z) \<in> g ==> z = y"
- show "b = (SOME y. (a, y) \<in> g)"
+ fix a b assume "(a, b) \\<in> g"
+ show "(a, SOME y. (a, y) \\<in> g) \\<in> g" by (rule selectI2)
+ show "\\<exists>y. (a, y) \\<in> g" ..
+ assume uniq: "!!x y z. (x, y) \\<in> g ==> (x, z) \\<in> g ==> z = y"
+ show "b = (SOME y. (a, y) \\<in> g)"
proof (rule select_equality [RS sym])
- fix y assume "(a, y) \<in> g" show "y = b" by (rule uniq)
+ fix y assume "(a, y) \\<in> g" show "y = b" by (rule uniq)
qed
qed
@@ -105,37 +98,37 @@
"['a::{plus, minus, zero} set, 'a => real, 'a set, 'a => real]
=> 'a graph set"
"norm_pres_extensions E p F f
- == {g. \<exists>H h. graph H h = g
- \<and> is_linearform H h
- \<and> is_subspace H E
- \<and> is_subspace F H
- \<and> graph F f <= graph H h
- \<and> (\<forall>x \<in> H. h x <= p x)}"
+ == {g. \\<exists>H h. graph H h = g
+ \\<and> is_linearform H h
+ \\<and> is_subspace H E
+ \\<and> is_subspace F H
+ \\<and> graph F f <= graph H h
+ \\<and> (\\<forall>x \\<in> H. h x <= p x)}"
lemma norm_pres_extension_D:
- "g \<in> norm_pres_extensions E p F f
- ==> \<exists>H h. graph H h = g
- \<and> is_linearform H h
- \<and> is_subspace H E
- \<and> is_subspace F H
- \<and> graph F f <= graph H h
- \<and> (\<forall>x \<in> H. h x <= p x)"
+ "g \\<in> norm_pres_extensions E p F f
+ ==> \\<exists>H h. graph H h = g
+ \\<and> is_linearform H h
+ \\<and> is_subspace H E
+ \\<and> is_subspace F H
+ \\<and> graph F f <= graph H h
+ \\<and> (\\<forall>x \\<in> H. h x <= p x)"
by (unfold norm_pres_extensions_def) force
lemma norm_pres_extensionI2 [intro]:
"[| is_linearform H h; is_subspace H E; is_subspace F H;
- graph F f <= graph H h; \<forall>x \<in> H. h x <= p x |]
- ==> (graph H h \<in> norm_pres_extensions E p F f)"
+ graph F f <= graph H h; \\<forall>x \\<in> H. h x <= p x |]
+ ==> (graph H h \\<in> norm_pres_extensions E p F f)"
by (unfold norm_pres_extensions_def) force
lemma norm_pres_extensionI [intro]:
- "\<exists>H h. graph H h = g
- \<and> is_linearform H h
- \<and> is_subspace H E
- \<and> is_subspace F H
- \<and> graph F f <= graph H h
- \<and> (\<forall>x \<in> H. h x <= p x)
- ==> g\<in> norm_pres_extensions E p F f"
+ "\\<exists>H h. graph H h = g
+ \\<and> is_linearform H h
+ \\<and> is_subspace H E
+ \\<and> is_subspace F H
+ \\<and> graph F f <= graph H h
+ \\<and> (\\<forall>x \\<in> H. h x <= p x)
+ ==> g \\<in> norm_pres_extensions E p F f"
by (unfold norm_pres_extensions_def) force
end
\ No newline at end of file