author wenzelm Wed, 05 Jan 2000 12:02:24 +0100 changeset 8104 d9b3a224c0e6 parent 8103 86f94a8116a9 child 8105 2dda3e88d23f
tuned;
--- a/src/HOL/Real/HahnBanach/HahnBanach.thy	Wed Jan 05 12:01:14 2000 +0100
+++ b/src/HOL/Real/HahnBanach/HahnBanach.thy	Wed Jan 05 12:02:24 2000 +0100
@@ -86,15 +86,15 @@

txt {* With Zorn's Lemma we can conclude that there is a maximal element $g$ in $M$. *};

-  hence "EX g:M. ALL x:M. g <= x --> g = x";
+  hence "EX g:M. ALL x:M. g <= x --> g = x";
proof (rule Zorn's_Lemma);
-    txt{* We show that $M$ is non-empty: *};
+    txt {* We show that $M$ is non-empty: *};
have "graph F f : 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 : M"; by (simp!);
qed;
thus ?thesis;
proof;
@@ -104,7 +104,10 @@
fix g; assume "g:M" "ALL x:M. g <= x --> g = x";
show ?thesis;

-txt_raw {* \isamarkuptxt{$g$ is a norm-preserving extension of $f$, that is: $g$ is the graph of a linear form $h$, defined on a subspace $H$ of $E$, which is a superspace of $F$. $h$ is an extension of $f$ and $h$ is again bounded by $p$.}  *};
+      txt {* $g$ is a norm-preserving extension of $f$, that is: $g$
+      is the graph of a linear form $h$, defined on a subspace $H$ of
+      $E$, which is a superspace of $F$. $h$ is an extension of $f$
+      and $h$ is again bounded by $p$. *};

obtain H h in "graph H h = g" and "is_linearform H h"
"is_subspace H E" "is_subspace F H" "graph F f <= graph H h"
@@ -114,7 +117,7 @@
& 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);
-        thus ?thesis; by (elim exE conjE) (rule that);
+        thus ?thesis; by blast;
qed;
have h: "is_vectorspace H"; ..;

@@ -123,7 +126,7 @@
have "H = E";
proof (rule classical);

-txt_raw {* \isamarkuptxt{Assume $h$ is not defined on whole $E$.} *};
+	txt {* Assume $h$ is not defined on whole $E$. *};

assume "H ~= E";

@@ -131,7 +134,7 @@

have "EX g_h0 : M. g <= g_h0 & g ~= g_h0";

-txt_raw {* \isamarkuptxt{Take $x_0 \in E \setminus H$.} *};
+	  txt {* Consider $x_0 \in E \setminus H$. *};

obtain x0 in "x0:E" "x0~:H";
proof -;
@@ -140,7 +143,7 @@
have "H <= E"; ..;
thus "H < E"; ..;
qed;
-            thus ?thesis; by (elim bexE) (rule that);
+            thus ?thesis; by blast;
qed;
have x0: "x0 ~= <0>";
proof (rule classical);
@@ -154,7 +157,9 @@
def H0 == "H + lin x0";
show ?thesis;

-txt_raw {* \isamarkuptxt{Chose a real number $\xi$ that fulfills certain inequations, which will be used to establish that $h_0$ is a norm-preserving extension of $h$.} *};
+	    txt {* Pick a real number $\xi$ that fulfills certain
+	    inequations, which will be used to establish that $h_0$ is
+	    a norm-preserving extension of $h$. *};

obtain xi in "ALL y:H. - p (y + x0) - h y <= xi
& xi <= p (y + x0) - h y";
@@ -180,7 +185,7 @@
thus "- p (u + x0) - h u <= p (v + x0) - h v";
by (rule real_diff_ineq_swap);
qed;
-              thus ?thesis; by (elim exE) (rule that);
+              thus ?thesis; by blast;
qed;

txt {* Define the extension $h_0$ of $h$ to $H_0$ using $\xi$.  *};
--- a/src/HOL/Real/HahnBanach/ZornLemma.thy	Wed Jan 05 12:01:14 2000 +0100
+++ b/src/HOL/Real/HahnBanach/ZornLemma.thy	Wed Jan 05 12:02:24 2000 +0100
@@ -7,24 +7,22 @@

theory ZornLemma = Aux + Zorn:;

-text{*
-Zorn's Lemmas states: if every linear ordered subset of an ordered set
-$S$ has an upper bound in $S$, then there exists a maximal element in $S$.
-In our application, $S$ is a set of sets ordered by set inclusion. Since
-the union of a chain of sets is an upper bound for all elements of the
-chain, the conditions of Zorn's lemma can be modified:
-if $S$ is non-empty, it suffices to show that for every non-empty
-chain $c$ in $S$ the union of $c$ also lies in $S$.
-*};
+text {* Zorn's Lemmas states: if every linear ordered subset of an
+ordered set $S$ has an upper bound in $S$, then there exists a maximal
+element in $S$.  In our application, $S$ is a set of sets ordered by
+set inclusion. Since the union of a chain of sets is an upper bound
+for all elements of the chain, the conditions of Zorn's lemma can be
+modified: if $S$ is non-empty, it suffices to show that for every
+non-empty chain $c$ in $S$ the union of $c$ also lies in $S$. *};

theorem Zorn's_Lemma:
-  "a:S ==> (!!c. c: chain S ==> EX x. x:c ==> Union c : S)
+  "(!!c. c: chain S ==> EX x. x:c ==> Union c : S) ==> a:S
==>  EX y: S. ALL z: S. y <= z --> y = z";
proof (rule Zorn_Lemma2);
-  txt_raw{* \footnote{See
+  txt_raw {* \footnote{See
\url{http://isabelle.in.tum.de/library/HOL/HOL-Real/Zorn.html}}*};
+  assume r: "!!c. c: chain S ==> EX x. x:c ==> Union c : S";
assume aS: "a:S";
-  assume r: "!!c. c: chain S ==> EX x. x:c ==> Union c : S";
show "ALL c:chain S. EX y:S. ALL z:c. z <= y";
proof;
fix c; assume "c:chain S";