author bauerg Thu, 06 Jul 2000 12:27:36 +0200 changeset 9261 879e0f0cd047 parent 9260 678e718a5a86 child 9262 8baf94ddb345
removed sorry;
--- 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
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)"
+                also have "... <= p (v - u)"
+                  by (simp!)
+                also have "v - u = x' + - x' + v + - u"
+                also have "... = v + x' + - (u + x')"
+                  by (simp!)
+                also have "... = (v + x') - (u + x')"
+                also have "p ... <= p (v + x') + p (u + x')"
+                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" ..
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)"
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";
-      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"
+      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)";
+             & graph F f \\<subseteq> graph G g
+             & (\<forall> x\<in>G. g x \\<le> p x)"

-    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