--- a/src/HOL/Real/HahnBanach/HahnBanach.thy Thu Jul 06 12:15:05 2000 +0200
+++ b/src/HOL/Real/HahnBanach/HahnBanach.thy Thu Jul 06 12:27:36 2000 +0200
@@ -19,19 +19,19 @@
txt {* Show that every non-empty chain $c$ of $M$ has an upper bound in $M$: *}
txt {* $\Union c$ is greater than any element of the chain $c$, so it suffices to show $\Union c \in M$. *}
proof (unfold M_def, rule norm_pres_extensionI)
- show "EX (H::'a set) h::'a => real. graph H h = Union c
+ show "\\<exists> H h. graph H h = \\<Union> c
& is_linearform H h
& is_subspace H E
& is_subspace F H
- & graph F f <= graph H h
- & (ALL x::'a:H. h x <= p x)"
+ & graph F f \\<subseteq> graph H h
+ & (\\<forall> x \\<in> H. h x \\<le> p x)"
proof (intro exI conjI)
- let ?H = "domain (Union c)"
- let ?h = "funct (Union c)"
+ let ?H = "domain (\\<Union> c)"
+ let ?h = "funct (\\<Union> c)"
- show a: "graph ?H ?h = Union c"
+ show a: "graph ?H ?h = \\<Union> c"
proof (rule graph_domain_funct)
- fix x y z assume "(x, y) : Union c" "(x, z) : Union c"
+ fix x y z assume "(x, y) \\<in> \\<Union> c" "(x, z) \\<in> \\<Union> c"
show "z = y" by (rule sup_definite)
qed
show "is_linearform ?H ?h"
@@ -42,10 +42,10 @@
show "is_subspace F ?H"
by (rule sup_supF [OF _ _ _ a]) (simp!)+
(* FIXME by (rule sup_supF, rule a) (simp!)+ *)
- show "graph F f <= graph ?H ?h"
+ show "graph F f \\<subseteq> graph ?H ?h"
by (rule sup_ext [OF _ _ _ a]) (simp!)+
(* FIXME by (rule sup_ext, rule a) (simp!)+*)
- show "ALL x::'a:?H. ?h x <= p x"
+ show "\\<forall>x \\<in> ?H. ?h x \\<le> p x"
by (rule sup_norm_pres [OF _ _ a]) (simp!)+
(* FIXME by (rule sup_norm_pres, rule a) (simp!)+ *)
qed
@@ -56,12 +56,12 @@
txt {* With Zorn's Lemma we can conclude that there is a maximal element in $M$.\skp *}
proof (rule Zorn's_Lemma)
txt {* We show that $M$ is non-empty: *}
- have "graph F f : norm_pres_extensions E p F f"
+ have "graph F f \\<in> norm_pres_extensions E p F f"
proof (rule norm_pres_extensionI2)
have "is_vectorspace F" ..
thus "is_subspace F F" ..
qed (blast!)+
- thus "graph F f : M" by (simp!)
+ thus "graph F f \\<in> M" by (simp!)
qed
thus ?thesis
proof
@@ -75,10 +75,10 @@
txt {* $g$ is the graph of some linear form $h$ defined on a subspace $H$ of $E$, *}
txt {* and $h$ is an extension of $f$ that is again bounded by $p$. \skp *}
proof -
- have "EX H h. graph H h = g & is_linearform H h
+ have "\\<exists> H h. graph H h = g & is_linearform H h
& is_subspace H E & is_subspace F H
- & graph F f <= graph H h
- & (ALL x:H. h x <= p x)" by (simp! add: norm_pres_extension_D)
+ & graph F f \\<subseteq> graph H h
+ & (\\<forall>x \\<in> H. h x \\<le> p x)" by (simp! add: norm_pres_extension_D)
thus ?thesis by (elim exE conjE) rule
qed
have h: "is_vectorspace H" ..
@@ -92,26 +92,52 @@
obtain x' where "x' \\<in> E" "x' \\<notin> H"
txt {* Pick $x' \in E \setminus H$. \skp *}
proof -
- have "EX x':E. x'~:H"
+ have "\\<exists>x' \\<in> E. x' \\<notin> H"
proof (rule set_less_imp_diff_not_empty)
- have "H <= E" ..
- thus "H < E" ..
+ have "H \\<subseteq> E" ..
+ thus "H \\<subset> E" ..
qed
thus ?thesis by blast
qed
- have x': "x' ~= \<zero>"
+ have x': "x' \\<noteq> \<zero>"
proof (rule classical)
presume "x' = \<zero>"
- with h have "x':H" by simp
+ with h have "x' \\<in> H" by simp
thus ?thesis by contradiction
qed blast
def H' == "H + lin x'"
-- {* Define $H'$ as the direct sum of $H$ and the linear closure of $x'$. \skp *}
show ?thesis
obtain xi where "\\<forall>y \\<in> H. - p (y + x') - h y \\<le> xi
- \\<and> xi \\<le> p (y + x') - h y" sorry
- -- {* Pick a real number $\xi$ that fulfills certain inequations; this will *}
- -- {* be used to establish that $h'$ is a norm-preserving extension of $h$. \skp *}
+ \\<and> xi \\<le> p (y + x') - h y"
+ txt {* Pick a real number $\xi$ that fulfills certain inequations; this will *}
+ txt {* be used to establish that $h'$ is a norm-preserving extension of $h$. \skp *}
+
+ proof -
+ from h have "EX xi. ALL y:H. - p (y + x') - h y <= xi
+ & xi <= p (y + x') - h y"
+ proof (rule ex_xi)
+ fix u v assume "u:H" "v:H"
+ from h have "h v - h u = h (v - u)"
+ by (simp! add: linearform_diff)
+ also have "... <= p (v - u)"
+ by (simp!)
+ also have "v - u = x' + - x' + v + - u"
+ by (simp! add: diff_eq1)
+ also have "... = v + x' + - (u + x')"
+ by (simp!)
+ also have "... = (v + x') - (u + x')"
+ by (simp! add: diff_eq1)
+ also have "p ... <= p (v + x') + p (u + x')"
+ by (rule seminorm_diff_subadditive) (simp!)+
+ finally have "h v - h u <= p (v + x') + p (u + x')" .
+
+ thus "- p (u + x') - h u <= p (v + x') - h v"
+ by (rule real_diff_ineq_swap)
+ qed
+ thus ?thesis by rule rule
+ qed
+
def h' == "\\<lambda>x. let (y,a) = \\<epsilon>(y,a). x = y + a \<prod> x' \\<and> y \\<in> H
in (h y) + a * xi"
-- {* Define the extension $h'$ of $h$ to $H'$ using $\xi$. \skp *}
@@ -120,17 +146,17 @@
show "g \\<subseteq> graph H' h' \\<and> g \\<noteq> graph H' h'"
txt {* Show that $h'$ is an extension of $h$ \dots \skp *}
proof
- show "g <= graph H' h'"
+ show "g \\<subseteq> graph H' h'"
proof -
- have "graph H h <= graph H' h'"
+ have "graph H h \\<subseteq> graph H' h'"
proof (rule graph_extI)
- fix t assume "t:H"
- have "(SOME (y, a). t = y + a \<prod> x' & y : H)
+ fix t assume "t \\<in> H"
+ have "(SOME (y, a). t = y + a \<prod> x' & y \\<in> H)
= (t, #0)"
by (rule decomp_H0_H [OF _ _ _ _ _ x'])
thus "h t = h' t" by (simp! add: Let_def)
next
- show "H <= H'"
+ show "H \\<subseteq> H'"
proof (rule subspace_subset)
show "is_subspace H H'"
proof (unfold H'_def, rule subspace_vs_sum1)
@@ -141,20 +167,20 @@
qed
thus ?thesis by (simp!)
qed
- show "g ~= graph H' h'"
+ show "g \\<noteq> graph H' h'"
proof -
- have "graph H h ~= graph H' h'"
+ have "graph H h \\<noteq> graph H' h'"
proof
assume e: "graph H h = graph H' h'"
- have "x' : H'"
+ have "x' \\<in> H'"
proof (unfold H'_def, rule vs_sumI)
show "x' = \<zero> + x'" by (simp!)
- from h show "\<zero> : H" ..
- show "x' : lin x'" by (rule x_lin_x)
+ from h show "\<zero> \\<in> H" ..
+ show "x' \\<in> lin x'" by (rule x_lin_x)
qed
- hence "(x', h' x') : graph H' h'" ..
- with e have "(x', h' x') : graph H h" by simp
- hence "x' : H" ..
+ hence "(x', h' x') \\<in> graph H' h'" ..
+ with e have "(x', h' x') \\<in> graph H h" by simp
+ hence "x' \\<in> H" ..
thus False by contradiction
qed
thus ?thesis by (simp!)
@@ -163,7 +189,7 @@
show "graph H' h' \\<in> M"
txt {* and $h'$ is norm-preserving. \skp *}
proof -
- have "graph H' h' : norm_pres_extensions E p F f"
+ have "graph H' h' \\<in> norm_pres_extensions E p F f"
proof (rule norm_pres_extensionI2)
show "is_linearform H' h'"
by (rule h0_lf [OF _ _ _ _ _ _ x']) (simp!)+
@@ -175,29 +201,29 @@
finally (subspace_trans [OF _ h])
show f_h': "is_subspace F H'" .
- show "graph F f <= graph H' h'"
+ show "graph F f \\<subseteq> graph H' h'"
proof (rule graph_extI)
- fix x assume "x:F"
+ fix x assume "x \\<in> F"
have "f x = h x" ..
also have " ... = h x + #0 * xi" by simp
also have "... = (let (y,a) = (x, #0) in h y + a * xi)"
by (simp add: Let_def)
also have
- "(x, #0) = (SOME (y, a). x = y + a (*) x' & y : H)"
+ "(x, #0) = (SOME (y, a). x = y + a (*) x' & y \\<in> H)"
by (rule decomp_H0_H [RS sym, OF _ _ _ _ _ x']) (simp!)+
also have
- "(let (y,a) = (SOME (y,a). x = y + a (*) x' & y : H)
+ "(let (y,a) = (SOME (y,a). x = y + a (*) x' & y \\<in> H)
in h y + a * xi)
= h' x" by (simp!)
finally show "f x = h' x" .
next
- from f_h' show "F <= H'" ..
+ from f_h' show "F \\<subseteq> H'" ..
qed
- show "ALL x:H'. h' x <= p x"
+ show "\\<forall>x \\<in> H'. h' x \\<le> p x"
by (rule h0_norm_pres [OF _ _ _ _ x'])
qed
- thus "graph H' h' : M" by (simp!)
+ thus "graph H' h' \\<in> M" by (simp!)
qed
qed
qed
@@ -211,11 +237,11 @@
proof (intro exI conjI)
assume eq: "H = E"
from eq show "is_linearform E h" by (simp!)
- show "ALL x:F. h x = f x"
+ show "\\<forall>x \\<in> F. h x = f x"
proof (intro ballI, rule sym)
- fix x assume "x:F" show "f x = h x " ..
+ fix x assume "x \\<in> F" show "f x = h x " ..
qed
- from eq show "ALL x:E. h x <= p x" by (force!)
+ from eq show "\\<forall>x \\<in> E. h x \\<le> p x" by (force!)
qed
qed
qed
--- a/src/HOL/Real/HahnBanach/HahnBanachSupLemmas.thy Thu Jul 06 12:15:05 2000 +0200
+++ b/src/HOL/Real/HahnBanach/HahnBanachSupLemmas.thy Thu Jul 06 12:27:36 2000 +0200
@@ -3,9 +3,9 @@
Author: Gertrud Bauer, TU Munich
*)
-header {* The supremum w.r.t.~the function order *};
+header {* The supremum w.r.t.~the function order *}
-theory HahnBanachSupLemmas = FunctionNorm + ZornLemma:;
+theory HahnBanachSupLemmas = FunctionNorm + ZornLemma:
@@ -18,622 +18,472 @@
$\Union c = \idt{graph}\ap H\ap h$.
We will show some properties about the limit function $h$,
i.e.\ the supremum of the chain $c$.
-*};
-
-(***
-lemma some_H'h't:
- "[| M = norm_pres_extensions E p F f; c: chain M;
- graph H h = Union c; x:H |]
- ==> EX H' h' t. t : graph H h & t = (x, h x) & graph H' h':c
- & t:graph H' h' & is_linearform H' h' & is_subspace H' E
- & is_subspace F H' & graph F f <= graph H' h'
- & (ALL x:H'. h' x <= p x)";
-proof -;
- assume m: "M = norm_pres_extensions E p F f" and cM: "c: chain M"
- and u: "graph H h = Union c" "x:H";
-
- let ?P = "\\<lambda>H h. is_linearform H h
- & is_subspace H E
- & is_subspace F H
- & graph F f <= graph H h
- & (ALL x:H. h x <= p x)";
+*}
- have "EX t : graph H h. t = (x, h x)";
- by (rule graphI2);
- thus ?thesis;
- proof (elim bexE);
- fix t; assume t: "t : graph H h" "t = (x, h x)";
- with u; have ex1: "EX g:c. t:g";
- by (simp only: Union_iff);
- thus ?thesis;
- proof (elim bexE);
- fix g; assume g: "g:c" "t:g";
- from cM; have "c <= M"; by (rule chainD2);
- hence "g : M"; ..;
- hence "g : norm_pres_extensions E p F f"; by (simp only: m);
- hence "EX H' h'. graph H' h' = g & ?P H' h'";
- by (rule norm_pres_extension_D);
- thus ?thesis;
- by (elim exE conjE, intro exI conjI) (simp | simp!)+;
- qed;
- qed;
-qed;
-***)
text{* Let $c$ be a chain of norm-preserving extensions of the
function $f$ and let $\idt{graph}\ap H\ap h$ be the supremum of $c$.
Every element in $H$ is member of
-one of the elements of the chain. *};
+one of the elements of the chain. *}
lemma some_H'h't:
- "[| M = norm_pres_extensions E p F f; c: chain M;
- graph H h = Union c; x:H |]
- ==> EX H' h'. graph H' h' : c & (x, h x) : graph H' h'
+ "[| M = norm_pres_extensions E p F f; c \<in> chain M;
+ graph H h = Union c; x \\<in> H |]
+ ==> \\<exists> H' h'. graph H' h' \<in> c & (x, h x) \<in> graph H' h'
& is_linearform H' h' & is_subspace H' E
- & is_subspace F H' & graph F f <= graph H' h'
- & (ALL x:H'. h' x <= p x)";
-proof -;
- assume m: "M = norm_pres_extensions E p F f" and "c: chain M"
- and u: "graph H h = Union c" "x:H";
+ & is_subspace F H' & graph F f \\<subseteq> graph H' h'
+ & (\\<forall>x \\<in> H'. h' x \\<le> p x)"
+proof -
+ assume m: "M = norm_pres_extensions E p F f" and "c \<in> chain M"
+ and u: "graph H h = Union c" "x \\<in> H"
- have h: "(x, h x) : graph H h"; ..;
- with u; have "(x, h x) : Union c"; by simp;
- hence ex1: "EX g:c. (x, h x) : g";
- by (simp only: Union_iff);
- thus ?thesis;
- proof (elim bexE);
- fix g; assume g: "g:c" "(x, h x) : g";
- have "c <= M"; by (rule chainD2);
- hence "g : M"; ..;
- hence "g : norm_pres_extensions E p F f"; by (simp only: m);
- hence "EX H' h'. graph H' h' = g
+ have h: "(x, h x) \<in> graph H h" ..
+ with u have "(x, h x) \<in> Union c" by simp
+ hence ex1: "\<exists> g \\<in> c. (x, h x) \<in> g"
+ by (simp only: Union_iff)
+ thus ?thesis
+ proof (elim bexE)
+ fix g assume g: "g \\<in> c" "(x, h x) \\<in> g"
+ have "c \\<subseteq> M" by (rule chainD2)
+ hence "g \\<in> M" ..
+ hence "g \<in> norm_pres_extensions E p F f" by (simp only: m)
+ hence "\<exists> H' h'. graph H' h' = g
& is_linearform H' h'
& is_subspace H' E
& is_subspace F H'
- & graph F f <= graph H' h'
- & (ALL x:H'. h' x <= p x)";
- by (rule norm_pres_extension_D);
- thus ?thesis;
- proof (elim exE conjE);
- fix H' h';
+ & graph F f \\<subseteq> graph H' h'
+ & (\<forall>x \\<in> H'. h' x \\<le> p x)"
+ by (rule norm_pres_extension_D)
+ thus ?thesis
+ proof (elim exE conjE)
+ fix H' h'
assume "graph H' h' = g" "is_linearform H' h'"
"is_subspace H' E" "is_subspace F H'"
- "graph F f <= graph H' h'" "ALL x:H'. h' x <= p x";
- show ?thesis;
- proof (intro exI conjI);
- show "graph H' h' : c"; by (simp!);
- show "(x, h x) : graph H' h'"; by (simp!);
- qed;
- qed;
- qed;
-qed;
+ "graph F f \\<subseteq> graph H' h'" "\<forall>x \\<in> H'. h' x \\<le> p x"
+ show ?thesis
+ proof (intro exI conjI)
+ show "graph H' h' \<in> c" by (simp!)
+ show "(x, h x) \<in> graph H' h'" by (simp!)
+ qed
+ qed
+ qed
+qed
text{* \medskip Let $c$ be a chain of norm-preserving extensions of the
function $f$ and let $\idt{graph}\ap H\ap h$ be the supremum of $c$.
Every element in the domain $H$ of the supremum function is member of
the domain $H'$ of some function $h'$, such that $h$ extends $h'$.
-*};
+*}
lemma some_H'h':
- "[| M = norm_pres_extensions E p F f; c: chain M;
- graph H h = Union c; x:H |]
- ==> EX H' h'. x:H' & graph H' h' <= graph H h
+ "[| M = norm_pres_extensions E p F f; c \<in> chain M;
+ graph H h = Union c; x \\<in> H |]
+ ==> \<exists> H' h'. x \\<in> H' & graph H' h' \\<subseteq> graph H h
& is_linearform H' h' & is_subspace H' E & is_subspace F H'
- & graph F f <= graph H' h' & (ALL x:H'. h' x <= p x)";
-proof -;
- assume "M = norm_pres_extensions E p F f" and cM: "c: chain M"
- and u: "graph H h = Union c" "x:H";
-
- have "EX H' h'. graph H' h' : c & (x, h x) : graph H' h'
- & is_linearform H' h' & is_subspace H' E
- & is_subspace F H' & graph F f <= graph H' h'
- & (ALL x:H'. h' x <= p x)";
- by (rule some_H'h't);
- thus ?thesis;
- proof (elim exE conjE);
- fix H' h'; assume "(x, h x) : graph H' h'" "graph H' h' : c"
- "is_linearform H' h'" "is_subspace H' E" "is_subspace F H'"
- "graph F f <= graph H' h'" "ALL x:H'. h' x <= p x";
- show ?thesis;
- proof (intro exI conjI);
- show "x:H'"; by (rule graphD1);
- from cM u; show "graph H' h' <= graph H h";
- by (simp! only: chain_ball_Union_upper);
- qed;
- qed;
-qed;
+ & graph F f \\<subseteq> graph H' h' & (\<forall>x \\<in> H'. h' x \\<le> p x)"
+proof -
+ assume "M = norm_pres_extensions E p F f" and cM: "c \<in> chain M"
+ and u: "graph H h = Union c" "x \\<in> H"
-(***
-lemma some_H'h':
- "[| M = norm_pres_extensions E p F f; c: chain M;
- graph H h = Union c; x:H |]
- ==> EX H' h'. x:H' & graph H' h' <= graph H h
- & is_linearform H' h' & is_subspace H' E & is_subspace F H'
- & graph F f <= graph H' h' & (ALL x:H'. h' x <= p x)";
-proof -;
- assume m: "M = norm_pres_extensions E p F f" and cM: "c: chain M"
- and u: "graph H h = Union c" "x:H";
- have "(x, h x): graph H h"; by (rule graphI);
- hence "(x, h x) : Union c"; by (simp!);
- hence "EX g:c. (x, h x):g"; by (simp only: Union_iff);
- thus ?thesis;
- proof (elim bexE);
- fix g; assume g: "g:c" "(x, h x):g";
- from cM; have "c <= M"; by (rule chainD2);
- hence "g : M"; ..;
- hence "g : norm_pres_extensions E p F f"; by (simp only: m);
- hence "EX H' h'. graph H' h' = g
- & is_linearform H' h'
- & is_subspace H' E
- & is_subspace F H'
- & graph F f <= graph H' h'
- & (ALL x:H'. h' x <= p x)";
- by (rule norm_pres_extension_D);
- thus ?thesis;
- proof (elim exE conjE, intro exI conjI);
- fix H' h'; assume g': "graph H' h' = g";
- with g; have "(x, h x): graph H' h'"; by simp;
- thus "x:H'"; by (rule graphD1);
- from g g'; have "graph H' h' : c"; by simp;
- with cM u; show "graph H' h' <= graph H h";
- by (simp only: chain_ball_Union_upper);
- qed simp+;
- qed;
-qed;
-***)
+ have "\<exists> H' h'. graph H' h' \<in> c & (x, h x) \<in> graph H' h'
+ & is_linearform H' h' & is_subspace H' E
+ & is_subspace F H' & graph F f \\<subseteq> graph H' h'
+ & (\<forall> x \\<in> H'. h' x \\<le> p x)"
+ by (rule some_H'h't)
+ thus ?thesis
+ proof (elim exE conjE)
+ fix H' h' assume "(x, h x) \<in> graph H' h'" "graph H' h' \<in> c"
+ "is_linearform H' h'" "is_subspace H' E" "is_subspace F H'"
+ "graph F f \\<subseteq> graph H' h'" "\<forall> x\<in>H'. h' x \\<le> p x"
+ show ?thesis
+ proof (intro exI conjI)
+ show "x\<in>H'" by (rule graphD1)
+ from cM u show "graph H' h' \\<subseteq> graph H h"
+ by (simp! only: chain_ball_Union_upper)
+ qed
+ qed
+qed
text{* \medskip Any two elements $x$ and $y$ in the domain $H$ of the
supremum function $h$ are both in the domain $H'$ of some function
-$h'$, such that $h$ extends $h'$. *};
+$h'$, such that $h$ extends $h'$. *}
lemma some_H'h'2:
- "[| M = norm_pres_extensions E p F f; c: chain M;
- graph H h = Union c; x:H; y:H |]
- ==> EX H' h'. x:H' & y:H' & graph H' h' <= graph H h
+ "[| M = norm_pres_extensions E p F f; c\<in> chain M;
+ graph H h = Union c; x\<in>H; y\<in>H |]
+ ==> \<exists> H' h'. x\<in>H' & y\<in>H' & graph H' h' \\<subseteq> graph H h
& is_linearform H' h' & is_subspace H' E & is_subspace F H'
- & graph F f <= graph H' h' & (ALL x:H'. h' x <= p x)";
-proof -;
- assume "M = norm_pres_extensions E p F f" "c: chain M"
- "graph H h = Union c" "x:H" "y:H";
+ & graph F f \\<subseteq> graph H' h' & (\<forall> x\<in>H'. h' x \\<le> p x)"
+proof -
+ assume "M = norm_pres_extensions E p F f" "c\<in> chain M"
+ "graph H h = Union c" "x\<in>H" "y\<in>H"
txt {* $x$ is in the domain $H'$ of some function $h'$,
- such that $h$ extends $h'$. *};
+ such that $h$ extends $h'$. *}
- have e1: "EX H' h'. graph H' h' : c & (x, h x) : graph H' h'
+ have e1: "\<exists> H' h'. graph H' h' \<in> c & (x, h x) \<in> graph H' h'
& is_linearform H' h' & is_subspace H' E
- & is_subspace F H' & graph F f <= graph H' h'
- & (ALL x:H'. h' x <= p x)";
- by (rule some_H'h't);
+ & is_subspace F H' & graph F f \\<subseteq> graph H' h'
+ & (\<forall> x\<in>H'. h' x \\<le> p x)"
+ by (rule some_H'h't)
txt {* $y$ is in the domain $H''$ of some function $h''$,
- such that $h$ extends $h''$. *};
+ such that $h$ extends $h''$. *}
- have e2: "EX H'' h''. graph H'' h'' : c & (y, h y) : graph H'' h''
+ have e2: "\<exists> H'' h''. graph H'' h'' \<in> c & (y, h y) \<in> graph H'' h''
& is_linearform H'' h'' & is_subspace H'' E
- & is_subspace F H'' & graph F f <= graph H'' h''
- & (ALL x:H''. h'' x <= p x)";
- by (rule some_H'h't);
+ & is_subspace F H'' & graph F f \\<subseteq> graph H'' h''
+ & (\<forall> x\<in>H''. h'' x \\<le> p x)"
+ by (rule some_H'h't)
- from e1 e2; show ?thesis;
- proof (elim exE conjE);
- fix H' h'; assume "(y, h y): graph H' h'" "graph H' h' : c"
+ from e1 e2 show ?thesis
+ proof (elim exE conjE)
+ fix H' h' assume "(y, h y)\<in> graph H' h'" "graph H' h' \<in> c"
"is_linearform H' h'" "is_subspace H' E" "is_subspace F H'"
- "graph F f <= graph H' h'" "ALL x:H'. h' x <= p x";
+ "graph F f \\<subseteq> graph H' h'" "\<forall> x\<in>H'. h' x \\<le> p x"
- fix H'' h''; assume "(x, h x): graph H'' h''" "graph H'' h'' : c"
+ fix H'' h'' assume "(x, h x)\<in> graph H'' h''" "graph H'' h'' \<in> c"
"is_linearform H'' h''" "is_subspace H'' E" "is_subspace F H''"
- "graph F f <= graph H'' h''" "ALL x:H''. h'' x <= p x";
+ "graph F f \\<subseteq> graph H'' h''" "\<forall> x\<in>H''. h'' x \\<le> p x"
txt {* Since both $h'$ and $h''$ are elements of the chain,
$h''$ is an extension of $h'$ or vice versa. Thus both
- $x$ and $y$ are contained in the greater one. \label{cases1}*};
-
- have "graph H'' h'' <= graph H' h' | graph H' h' <= graph H'' h''"
- (is "?case1 | ?case2");
- by (rule chainD);
- thus ?thesis;
- proof;
- assume ?case1;
- show ?thesis;
- proof (intro exI conjI);
- have "(x, h x) : graph H'' h''"; .;
- also; have "... <= graph H' h'"; .;
- finally; have xh: "(x, h x): graph H' h'"; .;
- thus x: "x:H'"; ..;
- show y: "y:H'"; ..;
- show "graph H' h' <= graph H h";
- by (simp! only: chain_ball_Union_upper);
- qed;
- next;
- assume ?case2;
- show ?thesis;
- proof (intro exI conjI);
- show x: "x:H''"; ..;
- have "(y, h y) : graph H' h'"; by (simp!);
- also; have "... <= graph H'' h''"; .;
- finally; have yh: "(y, h y): graph H'' h''"; .;
- thus y: "y:H''"; ..;
- show "graph H'' h'' <= graph H h";
- by (simp! only: chain_ball_Union_upper);
- qed;
- qed;
- qed;
-qed;
+ $x$ and $y$ are contained in the greater one. \label{cases1}*}
-(***
-lemma some_H'h'2:
- "[| M = norm_pres_extensions E p F f; c: chain M;
- graph H h = Union c; x:H; y:H |]
- ==> EX H' h'. x:H' & y:H' & graph H' h' <= graph H h
- & is_linearform H' h' & is_subspace H' E & is_subspace F H'
- & graph F f <= graph H' h' & (ALL x:H'. h' x <= p x)";
-proof -;
- assume "M = norm_pres_extensions E p F f" "c: chain M"
- "graph H h = Union c";
-
- let ?P = "\\<lambda>H h. is_linearform H h
- & is_subspace H E
- & is_subspace F H
- & graph F f <= graph H h
- & (ALL x:H. h x <= p x)";
- assume "x:H";
- have e1: "EX H' h' t. t : graph H h & t = (x, h x)
- & graph H' h' : c & t : graph H' h' & ?P H' h'";
- by (rule some_H'h't);
- assume "y:H";
- have e2: "EX H' h' t. t : graph H h & t = (y, h y)
- & graph H' h' : c & t:graph H' h' & ?P H' h'";
- by (rule some_H'h't);
+ have "graph H'' h'' \\<subseteq> graph H' h' | graph H' h' \\<subseteq> graph H'' h''"
+ (is "?case1 | ?case2")
+ by (rule chainD)
+ thus ?thesis
+ proof
+ assume ?case1
+ show ?thesis
+ proof (intro exI conjI)
+ have "(x, h x) \<in> graph H'' h''" .
+ also have "... \\<subseteq> graph H' h'" .
+ finally have xh:"(x, h x) \<in> graph H' h'" .
+ thus x: "x\<in>H'" ..
+ show y: "y\<in>H'" ..
+ show "graph H' h' \\<subseteq> graph H h"
+ by (simp! only: chain_ball_Union_upper)
+ qed
+ next
+ assume ?case2
+ show ?thesis
+ proof (intro exI conjI)
+ show x: "x\<in>H''" ..
+ have "(y, h y) \<in> graph H' h'" by (simp!)
+ also have "... \\<subseteq> graph H'' h''" .
+ finally have yh: "(y, h y)\<in> graph H'' h''" .
+ thus y: "y\<in>H''" ..
+ show "graph H'' h'' \\<subseteq> graph H h"
+ by (simp! only: chain_ball_Union_upper)
+ qed
+ qed
+ qed
+qed
- from e1 e2; show ?thesis;
- proof (elim exE conjE);
- fix H' h' t' H'' h'' t'';
- assume
- "t' : graph H h" "t'' : graph H h"
- "t' = (y, h y)" "t'' = (x, h x)"
- "graph H' h' : c" "graph H'' h'' : c"
- "t' : graph H' h'" "t'' : graph H'' h''"
- "is_linearform H' h'" "is_linearform H'' h''"
- "is_subspace H' E" "is_subspace H'' E"
- "is_subspace F H'" "is_subspace F H''"
- "graph F f <= graph H' h'" "graph F f <= graph H'' h''"
- "ALL x:H'. h' x <= p x" "ALL x:H''. h'' x <= p x";
- have "graph H'' h'' <= graph H' h'
- | graph H' h' <= graph H'' h''";
- by (rule chainD);
- thus "?thesis";
- proof;
- assume "graph H'' h'' <= graph H' h'";
- show ?thesis;
- proof (intro exI conjI);
- note [trans] = subsetD;
- have "(x, h x) : graph H'' h''"; by (simp!);
- also; have "... <= graph H' h'"; .;
- finally; have xh: "(x, h x): graph H' h'"; .;
- thus x: "x:H'"; by (rule graphD1);
- show y: "y:H'"; by (simp!, rule graphD1);
- show "graph H' h' <= graph H h";
- by (simp! only: chain_ball_Union_upper);
- qed;
- next;
- assume "graph H' h' <= graph H'' h''";
- show ?thesis;
- proof (intro exI conjI);
- show x: "x:H''"; by (simp!, rule graphD1);
- have "(y, h y) : graph H' h'"; by (simp!);
- also; have "... <= graph H'' h''"; .;
- finally; have yh: "(y, h y): graph H'' h''"; .;
- thus y: "y:H''"; by (rule graphD1);
- show "graph H'' h'' <= graph H h";
- by (simp! only: chain_ball_Union_upper);
- qed;
- qed;
- qed;
-qed;
-
-***)
text{* \medskip The relation induced by the graph of the supremum
-of a chain $c$ is definite, i.~e.~it is the graph of a function. *};
+of a chain $c$ is definite, i.~e.~it is the graph of a function. *}
lemma sup_definite:
- "[| M == norm_pres_extensions E p F f; c : chain M;
- (x, y) : Union c; (x, z) : Union c |] ==> z = y";
-proof -;
- assume "c:chain M" "M == norm_pres_extensions E p F f"
- "(x, y) : Union c" "(x, z) : Union c";
- thus ?thesis;
- proof (elim UnionE chainE2);
+ "[| M == norm_pres_extensions E p F f; c \<in> chain M;
+ (x, y) \<in> Union c; (x, z) \<in> Union c |] ==> z = y"
+proof -
+ assume "c\<in>chain M" "M == norm_pres_extensions E p F f"
+ "(x, y) \<in> Union c" "(x, z) \<in> Union c"
+ thus ?thesis
+ proof (elim UnionE chainE2)
txt{* Since both $(x, y) \in \Union c$ and $(x, z) \in \Union c$
they are members of some graphs $G_1$ and $G_2$, resp., such that
- both $G_1$ and $G_2$ are members of $c$.*};
+ both $G_1$ and $G_2$ are members of $c$.*}
- fix G1 G2; assume
- "(x, y) : G1" "G1 : c" "(x, z) : G2" "G2 : c" "c <= M";
+ fix G1 G2 assume
+ "(x, y) \<in> G1" "G1 \<in> c" "(x, z) \<in> G2" "G2 \<in> c" "c \\<subseteq> M"
- have "G1 : M"; ..;
- hence e1: "EX H1 h1. graph H1 h1 = G1";
- by (force! dest: norm_pres_extension_D);
- have "G2 : M"; ..;
- hence e2: "EX H2 h2. graph H2 h2 = G2";
- by (force! dest: norm_pres_extension_D);
- from e1 e2; show ?thesis;
- proof (elim exE);
- fix H1 h1 H2 h2;
- assume "graph H1 h1 = G1" "graph H2 h2 = G2";
+ have "G1 \<in> M" ..
+ hence e1: "\<exists> H1 h1. graph H1 h1 = G1"
+ by (force! dest: norm_pres_extension_D)
+ have "G2 \<in> M" ..
+ hence e2: "\<exists> H2 h2. graph H2 h2 = G2"
+ by (force! dest: norm_pres_extension_D)
+ from e1 e2 show ?thesis
+ proof (elim exE)
+ fix H1 h1 H2 h2
+ assume "graph H1 h1 = G1" "graph H2 h2 = G2"
txt{* $G_1$ is contained in $G_2$ or vice versa,
- since both $G_1$ and $G_2$ are members of $c$. \label{cases2}*};
+ since both $G_1$ and $G_2$ are members of $c$. \label{cases2}*}
- have "G1 <= G2 | G2 <= G1" (is "?case1 | ?case2"); ..;
- thus ?thesis;
- proof;
- assume ?case1;
- have "(x, y) : graph H2 h2"; by (force!);
- hence "y = h2 x"; ..;
- also; have "(x, z) : graph H2 h2"; by (simp!);
- hence "z = h2 x"; ..;
- finally; show ?thesis; .;
- next;
- assume ?case2;
- have "(x, y) : graph H1 h1"; by (simp!);
- hence "y = h1 x"; ..;
- also; have "(x, z) : graph H1 h1"; by (force!);
- hence "z = h1 x"; ..;
- finally; show ?thesis; .;
- qed;
- qed;
- qed;
-qed;
+ have "G1 \\<subseteq> G2 | G2 \\<subseteq> G1" (is "?case1 | ?case2") ..
+ thus ?thesis
+ proof
+ assume ?case1
+ have "(x, y) \<in> graph H2 h2" by (force!)
+ hence "y = h2 x" ..
+ also have "(x, z) \<in> graph H2 h2" by (simp!)
+ hence "z = h2 x" ..
+ finally show ?thesis .
+ next
+ assume ?case2
+ have "(x, y) \<in> graph H1 h1" by (simp!)
+ hence "y = h1 x" ..
+ also have "(x, z) \<in> graph H1 h1" by (force!)
+ hence "z = h1 x" ..
+ finally show ?thesis .
+ qed
+ qed
+ qed
+qed
text{* \medskip The limit function $h$ is linear. Every element $x$ in the
domain of $h$ is in the domain of a function $h'$ in the chain of norm
preserving extensions. Furthermore, $h$ is an extension of $h'$ so
the function values of $x$ are identical for $h'$ and $h$. Finally, the
-function $h'$ is linear by construction of $M$. *};
+function $h'$ is linear by construction of $M$. *}
lemma sup_lf:
- "[| M = norm_pres_extensions E p F f; c: chain M;
- graph H h = Union c |] ==> is_linearform H h";
-proof -;
- assume "M = norm_pres_extensions E p F f" "c: chain M"
- "graph H h = Union c";
+ "[| M = norm_pres_extensions E p F f; c\<in> chain M;
+ graph H h = Union c |] ==> is_linearform H h"
+proof -
+ assume "M = norm_pres_extensions E p F f" "c\<in> chain M"
+ "graph H h = Union c"
- show "is_linearform H h";
- proof;
- fix x y; assume "x : H" "y : H";
- have "EX H' h'. x:H' & y:H' & graph H' h' <= graph H h
+ show "is_linearform H h"
+ proof
+ fix x y assume "x \<in> H" "y \<in> H"
+ have "\<exists> H' h'. x\<in>H' & y\<in>H' & graph H' h' \\<subseteq> graph H h
& is_linearform H' h' & is_subspace H' E
- & is_subspace F H' & graph F f <= graph H' h'
- & (ALL x:H'. h' x <= p x)";
- by (rule some_H'h'2);
+ & is_subspace F H' & graph F f \\<subseteq> graph H' h'
+ & (\<forall> x\<in>H'. h' x \\<le> p x)"
+ by (rule some_H'h'2)
- txt {* We have to show that $h$ is additive. *};
+ txt {* We have to show that $h$ is additive. *}
- thus "h (x + y) = h x + h y";
- proof (elim exE conjE);
- fix H' h'; assume "x:H'" "y:H'"
- and b: "graph H' h' <= graph H h"
- and "is_linearform H' h'" "is_subspace H' E";
- have "h' (x + y) = h' x + h' y";
- by (rule linearform_add);
- also; have "h' x = h x"; ..;
- also; have "h' y = h y"; ..;
- also; have "x + y : H'"; ..;
- with b; have "h' (x + y) = h (x + y)"; ..;
- finally; show ?thesis; .;
- qed;
- next;
- fix a x; assume "x : H";
- have "EX H' h'. x:H' & graph H' h' <= graph H h
+ thus "h (x + y) = h x + h y"
+ proof (elim exE conjE)
+ fix H' h' assume "x\<in>H'" "y\<in>H'"
+ and b: "graph H' h' \\<subseteq> graph H h"
+ and "is_linearform H' h'" "is_subspace H' E"
+ have "h' (x + y) = h' x + h' y"
+ by (rule linearform_add)
+ also have "h' x = h x" ..
+ also have "h' y = h y" ..
+ also have "x + y \<in> H'" ..
+ with b have "h' (x + y) = h (x + y)" ..
+ finally show ?thesis .
+ qed
+ next
+ fix a x assume "x \<in> H"
+ have "\<exists> H' h'. x\<in>H' & graph H' h' \\<subseteq> graph H h
& is_linearform H' h' & is_subspace H' E
- & is_subspace F H' & graph F f <= graph H' h'
- & (ALL x:H'. h' x <= p x)";
- by (rule some_H'h');
+ & is_subspace F H' & graph F f \\<subseteq> graph H' h'
+ & (\<forall> x\<in>H'. h' x \\<le> p x)"
+ by (rule some_H'h')
- txt{* We have to show that $h$ is multiplicative. *};
+ txt{* We have to show that $h$ is multiplicative. *}
- thus "h (a \<prod> x) = a * h x";
- proof (elim exE conjE);
- fix H' h'; assume "x:H'"
- and b: "graph H' h' <= graph H h"
- and "is_linearform H' h'" "is_subspace H' E";
- have "h' (a \<prod> x) = a * h' x";
- by (rule linearform_mult);
- also; have "h' x = h x"; ..;
- also; have "a \<prod> x : H'"; ..;
- with b; have "h' (a \<prod> x) = h (a \<prod> x)"; ..;
- finally; show ?thesis; .;
- qed;
- qed;
-qed;
+ thus "h (a \<prod> x) = a * h x"
+ proof (elim exE conjE)
+ fix H' h' assume "x\<in>H'"
+ and b: "graph H' h' \\<subseteq> graph H h"
+ and "is_linearform H' h'" "is_subspace H' E"
+ have "h' (a \<prod> x) = a * h' x"
+ by (rule linearform_mult)
+ also have "h' x = h x" ..
+ also have "a \<prod> x \<in> H'" ..
+ with b have "h' (a \<prod> x) = h (a \<prod> x)" ..
+ finally show ?thesis .
+ qed
+ qed
+qed
text{* \medskip The limit of a non-empty chain of norm
preserving extensions of $f$ is an extension of $f$,
since every element of the chain is an extension
of $f$ and the supremum is an extension
-for every element of the chain.*};
+for every element of the chain.*}
lemma sup_ext:
- "[| M = norm_pres_extensions E p F f; c: chain M; EX x. x:c;
- graph H h = Union c |] ==> graph F f <= graph H h";
-proof -;
- assume "M = norm_pres_extensions E p F f" "c: chain M"
- "graph H h = Union c";
- assume "EX x. x:c";
- thus ?thesis;
- proof;
- fix x; assume "x:c";
- have "c <= M"; by (rule chainD2);
- hence "x:M"; ..;
- hence "x : norm_pres_extensions E p F f"; by (simp!);
+ "[| M = norm_pres_extensions E p F f; c\<in> chain M; \<exists> x. x\<in>c;
+ graph H h = Union c |] ==> graph F f \\<subseteq> graph H h"
+proof -
+ assume "M = norm_pres_extensions E p F f" "c\<in> chain M"
+ "graph H h = Union c"
+ assume "\<exists> x. x\<in>c"
+ thus ?thesis
+ proof
+ fix x assume "x\<in>c"
+ have "c \\<subseteq> M" by (rule chainD2)
+ hence "x\<in>M" ..
+ hence "x \<in> norm_pres_extensions E p F f" by (simp!)
- hence "EX G g. graph G g = x
+ hence "\<exists> G g. graph G g = x
& is_linearform G g
& is_subspace G E
& is_subspace F G
- & graph F f <= graph G g
- & (ALL x:G. g x <= p x)";
- by (simp! add: norm_pres_extension_D);
+ & graph F f \\<subseteq> graph G g
+ & (\<forall> x\<in>G. g x \\<le> p x)"
+ by (simp! add: norm_pres_extension_D)
- thus ?thesis;
- proof (elim exE conjE);
- fix G g; assume "graph F f <= graph G g";
- also; assume "graph G g = x";
- also; have "... : c"; .;
- hence "x <= Union c"; by fast;
- also; have [RS sym]: "graph H h = Union c"; .;
- finally; show ?thesis; .;
- qed;
- qed;
-qed;
+ thus ?thesis
+ proof (elim exE conjE)
+ fix G g assume "graph F f \\<subseteq> graph G g"
+ also assume "graph G g = x"
+ also have "... \<in> c" .
+ hence "x \\<subseteq> Union c" by fast
+ also have [RS sym]: "graph H h = Union c" .
+ finally show ?thesis .
+ qed
+ qed
+qed
text{* \medskip The domain $H$ of the limit function is a superspace of $F$,
since $F$ is a subset of $H$. The existence of the $\zero$ element in
$F$ and the closure properties follow from the fact that $F$ is a
-vector space. *};
+vector space. *}
lemma sup_supF:
- "[| M = norm_pres_extensions E p F f; c: chain M; EX x. x:c;
+ "[| M = norm_pres_extensions E p F f; c\<in> chain M; \<exists> x. x\<in>c;
graph H h = Union c; is_subspace F E; is_vectorspace E |]
- ==> is_subspace F H";
-proof -;
- assume "M = norm_pres_extensions E p F f" "c: chain M" "EX x. x:c"
- "graph H h = Union c" "is_subspace F E" "is_vectorspace E";
+ ==> is_subspace F H"
+proof -
+ assume "M = norm_pres_extensions E p F f" "c\<in> chain M" "\<exists> x. x\<in>c"
+ "graph H h = Union c" "is_subspace F E" "is_vectorspace E"
- show ?thesis;
- proof;
- show "\<zero> : F"; ..;
- show "F <= H";
- proof (rule graph_extD2);
- show "graph F f <= graph H h";
- by (rule sup_ext);
- qed;
- show "ALL x:F. ALL y:F. x + y : F";
- proof (intro ballI);
- fix x y; assume "x:F" "y:F";
- show "x + y : F"; by (simp!);
- qed;
- show "ALL x:F. ALL a. a \<prod> x : F";
- proof (intro ballI allI);
- fix x a; assume "x:F";
- show "a \<prod> x : F"; by (simp!);
- qed;
- qed;
-qed;
+ show ?thesis
+ proof
+ show "\<zero> \<in> F" ..
+ show "F \\<subseteq> H"
+ proof (rule graph_extD2)
+ show "graph F f \\<subseteq> graph H h"
+ by (rule sup_ext)
+ qed
+ show "\<forall> x\<in>F. \<forall> y\<in>F. x + y \<in> F"
+ proof (intro ballI)
+ fix x y assume "x\<in>F" "y\<in>F"
+ show "x + y \<in> F" by (simp!)
+ qed
+ show "\<forall> x\<in>F. \<forall> a. a \<prod> x \<in> F"
+ proof (intro ballI allI)
+ fix x a assume "x\<in>F"
+ show "a \<prod> x \<in> F" by (simp!)
+ qed
+ qed
+qed
text{* \medskip The domain $H$ of the limit function is a subspace
-of $E$. *};
+of $E$. *}
lemma sup_subE:
- "[| M = norm_pres_extensions E p F f; c: chain M; EX x. x:c;
+ "[| M = norm_pres_extensions E p F f; c\<in> chain M; \<exists> x. x\<in>c;
graph H h = Union c; is_subspace F E; is_vectorspace E |]
- ==> is_subspace H E";
-proof -;
- assume "M = norm_pres_extensions E p F f" "c: chain M" "EX x. x:c"
- "graph H h = Union c" "is_subspace F E" "is_vectorspace E";
- show ?thesis;
- proof;
+ ==> is_subspace H E"
+proof -
+ assume "M = norm_pres_extensions E p F f" "c\<in> chain M" "\<exists> x. x\<in>c"
+ "graph H h = Union c" "is_subspace F E" "is_vectorspace E"
+ show ?thesis
+ proof
txt {* The $\zero$ element is in $H$, as $F$ is a subset
- of $H$: *};
+ of $H$: *}
- have "\<zero> : F"; ..;
- also; have "is_subspace F H"; by (rule sup_supF);
- hence "F <= H"; ..;
- finally; show "\<zero> : H"; .;
+ have "\<zero> \<in> F" ..
+ also have "is_subspace F H" by (rule sup_supF)
+ hence "F \\<subseteq> H" ..
+ finally show "\<zero> \<in> H" .
- txt{* $H$ is a subset of $E$: *};
+ txt{* $H$ is a subset of $E$: *}
- show "H <= E";
- proof;
- fix x; assume "x:H";
- have "EX H' h'. x:H' & graph H' h' <= graph H h
+ show "H \\<subseteq> E"
+ proof
+ fix x assume "x\<in>H"
+ have "\<exists> H' h'. x\<in>H' & graph H' h' \\<subseteq> graph H h
& is_linearform H' h' & is_subspace H' E
- & is_subspace F H' & graph F f <= graph H' h'
- & (ALL x:H'. h' x <= p x)";
- by (rule some_H'h');
- thus "x:E";
- proof (elim exE conjE);
- fix H' h'; assume "x:H'" "is_subspace H' E";
- have "H' <= E"; ..;
- thus "x:E"; ..;
- qed;
- qed;
+ & is_subspace F H' & graph F f \\<subseteq> graph H' h'
+ & (\<forall> x\<in>H'. h' x \\<le> p x)"
+ by (rule some_H'h')
+ thus "x\<in>E"
+ proof (elim exE conjE)
+ fix H' h' assume "x\<in>H'" "is_subspace H' E"
+ have "H' \\<subseteq> E" ..
+ thus "x\<in>E" ..
+ qed
+ qed
- txt{* $H$ is closed under addition: *};
+ txt{* $H$ is closed under addition: *}
- show "ALL x:H. ALL y:H. x + y : H";
- proof (intro ballI);
- fix x y; assume "x:H" "y:H";
- have "EX H' h'. x:H' & y:H' & graph H' h' <= graph H h
+ show "\<forall> x\<in>H. \<forall> y\<in>H. x + y \<in> H"
+ proof (intro ballI)
+ fix x y assume "x\<in>H" "y\<in>H"
+ have "\<exists> H' h'. x\<in>H' & y\<in>H' & graph H' h' \\<subseteq> graph H h
& is_linearform H' h' & is_subspace H' E
- & is_subspace F H' & graph F f <= graph H' h'
- & (ALL x:H'. h' x <= p x)";
- by (rule some_H'h'2);
- thus "x + y : H";
- proof (elim exE conjE);
- fix H' h';
- assume "x:H'" "y:H'" "is_subspace H' E"
- "graph H' h' <= graph H h";
- have "x + y : H'"; ..;
- also; have "H' <= H"; ..;
- finally; show ?thesis; .;
- qed;
- qed;
+ & is_subspace F H' & graph F f \\<subseteq> graph H' h'
+ & (\<forall> x\<in>H'. h' x \\<le> p x)"
+ by (rule some_H'h'2)
+ thus "x + y \<in> H"
+ proof (elim exE conjE)
+ fix H' h'
+ assume "x\<in>H'" "y\<in>H'" "is_subspace H' E"
+ "graph H' h' \\<subseteq> graph H h"
+ have "x + y \<in> H'" ..
+ also have "H' \\<subseteq> H" ..
+ finally show ?thesis .
+ qed
+ qed
- txt{* $H$ is closed under scalar multiplication: *};
+ txt{* $H$ is closed under scalar multiplication: *}
- show "ALL x:H. ALL a. a \<prod> x : H";
- proof (intro ballI allI);
- fix x a; assume "x:H";
- have "EX H' h'. x:H' & graph H' h' <= graph H h
+ show "\<forall> x\<in>H. \<forall> a. a \<prod> x \<in> H"
+ proof (intro ballI allI)
+ fix x a assume "x\<in>H"
+ have "\<exists> H' h'. x\<in>H' & graph H' h' \\<subseteq> graph H h
& is_linearform H' h' & is_subspace H' E
- & is_subspace F H' & graph F f <= graph H' h'
- & (ALL x:H'. h' x <= p x)";
- by (rule some_H'h');
- thus "a \<prod> x : H";
- proof (elim exE conjE);
- fix H' h';
- assume "x:H'" "is_subspace H' E" "graph H' h' <= graph H h";
- have "a \<prod> x : H'"; ..;
- also; have "H' <= H"; ..;
- finally; show ?thesis; .;
- qed;
- qed;
- qed;
-qed;
+ & is_subspace F H' & graph F f \\<subseteq> graph H' h'
+ & (\<forall> x\<in>H'. h' x \\<le> p x)"
+ by (rule some_H'h')
+ thus "a \<prod> x \<in> H"
+ proof (elim exE conjE)
+ fix H' h'
+ assume "x\<in>H'" "is_subspace H' E" "graph H' h' \\<subseteq> graph H h"
+ have "a \<prod> x \<in> H'" ..
+ also have "H' \\<subseteq> H" ..
+ finally show ?thesis .
+ qed
+ qed
+ qed
+qed
text {* \medskip The limit function is bounded by
the norm $p$ as well, since all elements in the chain are
bounded by $p$.
-*};
+*}
-lemma sup_norm_pres:
- "[| M = norm_pres_extensions E p F f; c: chain M;
- graph H h = Union c |] ==> ALL x:H. h x <= p x";
-proof;
- assume "M = norm_pres_extensions E p F f" "c: chain M"
- "graph H h = Union c";
- fix x; assume "x:H";
- have "EX H' h'. x:H' & graph H' h' <= graph H h
+lemma sup_norm_pres:
+ "[| M = norm_pres_extensions E p F f; c\<in> chain M;
+ graph H h = Union c |] ==> \<forall> x\<in>H. h x \\<le> p x"
+proof
+ assume "M = norm_pres_extensions E p F f" "c\<in> chain M"
+ "graph H h = Union c"
+ fix x assume "x\<in>H"
+ have "\\<exists> H' h'. x\<in>H' & graph H' h' \\<subseteq> graph H h
& is_linearform H' h' & is_subspace H' E & is_subspace F H'
- & graph F f <= graph H' h' & (ALL x:H'. h' x <= p x)";
- by (rule some_H'h');
- thus "h x <= p x";
- proof (elim exE conjE);
- fix H' h';
- assume "x: H'" "graph H' h' <= graph H h"
- and a: "ALL x: H'. h' x <= p x";
- have [RS sym]: "h' x = h x"; ..;
- also; from a; have "h' x <= p x "; ..;
- finally; show ?thesis; .;
- qed;
-qed;
+ & graph F f \\<subseteq> graph H' h' & (\<forall> x\<in>H'. h' x \\<le> p x)"
+ by (rule some_H'h')
+ thus "h x \\<le> p x"
+ proof (elim exE conjE)
+ fix H' h'
+ assume "x\<in> H'" "graph H' h' \\<subseteq> graph H h"
+ and a: "\<forall> x\<in> H'. h' x \\<le> p x"
+ have [RS sym]: "h' x = h x" ..
+ also from a have "h' x \\<le> p x " ..
+ finally show ?thesis .
+ qed
+qed
text{* \medskip The following lemma is a property of linear forms on
@@ -644,47 +494,47 @@
\forall x\in H.\ap |h\ap x|\leq p\ap x& {\rm and}\\
\forall x\in H.\ap h\ap x\leq p\ap x\\
\end{matharray}
-*};
+*}
lemma abs_ineq_iff:
"[| is_subspace H E; is_vectorspace E; is_seminorm E p;
is_linearform H h |]
- ==> (ALL x:H. abs (h x) <= p x) = (ALL x:H. h x <= p x)"
- (concl is "?L = ?R");
-proof -;
+ ==> (\<forall> x\<in>H. abs (h x) \\<le> p x) = (\<forall> x\<in>H. h x \\<le> p x)"
+ (concl is "?L = ?R")
+proof -
assume "is_subspace H E" "is_vectorspace E" "is_seminorm E p"
- "is_linearform H h";
- have h: "is_vectorspace H"; ..;
- show ?thesis;
- proof;
- assume l: ?L;
- show ?R;
- proof;
- fix x; assume x: "x:H";
- have "h x <= abs (h x)"; by (rule abs_ge_self);
- also; from l; have "... <= p x"; ..;
- finally; show "h x <= p x"; .;
- qed;
- next;
- assume r: ?R;
- show ?L;
- proof;
- fix x; assume "x:H";
- show "!! a b :: real. [| - a <= b; b <= a |] ==> abs b <= a";
- by arith;
- show "- p x <= h x";
- proof (rule real_minus_le);
- from h; have "- h x = h (- x)";
- by (rule linearform_neg [RS sym]);
- also; from r; have "... <= p (- x)"; by (simp!);
- also; have "... = p x";
- by (rule seminorm_minus [OF _ subspace_subsetD]);
- finally; show "- h x <= p x"; .;
- qed;
- from r; show "h x <= p x"; ..;
- qed;
- qed;
-qed;
+ "is_linearform H h"
+ have h: "is_vectorspace H" ..
+ show ?thesis
+ proof
+ assume l: ?L
+ show ?R
+ proof
+ fix x assume x: "x\<in>H"
+ have "h x \\<le> abs (h x)" by (rule abs_ge_self)
+ also from l have "... \\<le> p x" ..
+ finally show "h x \\<le> p x" .
+ qed
+ next
+ assume r: ?R
+ show ?L
+ proof
+ fix x assume "x\<in>H"
+ show "!! a b :: real. [| - a \\<le> b; b \\<le> a |] ==> abs b \\<le> a"
+ by arith
+ show "- p x \\<le> h x"
+ proof (rule real_minus_le)
+ from h have "- h x = h (- x)"
+ by (rule linearform_neg [RS sym])
+ also from r have "... \\<le> p (- x)" by (simp!)
+ also have "... = p x"
+ by (rule seminorm_minus [OF _ subspace_subsetD])
+ finally show "- h x \\<le> p x" .
+ qed
+ from r show "h x \\<le> p x" ..
+ qed
+ qed
+qed
-end;
\ No newline at end of file
+end
\ No newline at end of file