summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | bauerg |

Thu, 06 Jul 2000 12:27:36 +0200 | |

changeset 9261 | 879e0f0cd047 |

parent 9260 | 678e718a5a86 |

child 9262 | 8baf94ddb345 |

removed sorry;

src/HOL/Real/HahnBanach/HahnBanach.thy | file | annotate | diff | comparison | revisions | |

src/HOL/Real/HahnBanach/HahnBanachSupLemmas.thy | file | annotate | diff | comparison | revisions |

--- 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