1.1 --- a/src/HOL/Real/HahnBanach/HahnBanach.thy Wed Jan 05 12:01:14 2000 +0100
1.2 +++ b/src/HOL/Real/HahnBanach/HahnBanach.thy Wed Jan 05 12:02:24 2000 +0100
1.3 @@ -86,15 +86,15 @@
1.4
1.5 txt {* With Zorn's Lemma we can conclude that there is a maximal element $g$ in $M$. *};
1.6
1.7 - hence "EX g:M. ALL x:M. g <= x --> g = x";
1.8 + hence "EX g:M. ALL x:M. g <= x --> g = x";
1.9 proof (rule Zorn's_Lemma);
1.10 - txt{* We show that $M$ is non-empty: *};
1.11 + txt {* We show that $M$ is non-empty: *};
1.12 have "graph F f : norm_pres_extensions E p F f";
1.13 proof (rule norm_pres_extensionI2);
1.14 have "is_vectorspace F"; ..;
1.15 thus "is_subspace F F"; ..;
1.16 qed (blast!)+;
1.17 - thus "graph F f : M"; by (simp!);
1.18 + thus "graph F f : M"; by (simp!);
1.19 qed;
1.20 thus ?thesis;
1.21 proof;
1.22 @@ -104,7 +104,10 @@
1.23 fix g; assume "g:M" "ALL x:M. g <= x --> g = x";
1.24 show ?thesis;
1.25
1.26 -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$.} *};
1.27 + txt {* $g$ is a norm-preserving extension of $f$, that is: $g$
1.28 + is the graph of a linear form $h$, defined on a subspace $H$ of
1.29 + $E$, which is a superspace of $F$. $h$ is an extension of $f$
1.30 + and $h$ is again bounded by $p$. *};
1.31
1.32 obtain H h in "graph H h = g" and "is_linearform H h"
1.33 "is_subspace H E" "is_subspace F H" "graph F f <= graph H h"
1.34 @@ -114,7 +117,7 @@
1.35 & is_subspace H E & is_subspace F H
1.36 & graph F f <= graph H h
1.37 & (ALL x:H. h x <= p x)"; by (simp! add: norm_pres_extension_D);
1.38 - thus ?thesis; by (elim exE conjE) (rule that);
1.39 + thus ?thesis; by blast;
1.40 qed;
1.41 have h: "is_vectorspace H"; ..;
1.42
1.43 @@ -123,7 +126,7 @@
1.44 have "H = E";
1.45 proof (rule classical);
1.46
1.47 -txt_raw {* \isamarkuptxt{Assume $h$ is not defined on whole $E$.} *};
1.48 + txt {* Assume $h$ is not defined on whole $E$. *};
1.49
1.50 assume "H ~= E";
1.51
1.52 @@ -131,7 +134,7 @@
1.53
1.54 have "EX g_h0 : M. g <= g_h0 & g ~= g_h0";
1.55
1.56 -txt_raw {* \isamarkuptxt{Take $x_0 \in E \setminus H$.} *};
1.57 + txt {* Consider $x_0 \in E \setminus H$. *};
1.58
1.59 obtain x0 in "x0:E" "x0~:H";
1.60 proof -;
1.61 @@ -140,7 +143,7 @@
1.62 have "H <= E"; ..;
1.63 thus "H < E"; ..;
1.64 qed;
1.65 - thus ?thesis; by (elim bexE) (rule that);
1.66 + thus ?thesis; by blast;
1.67 qed;
1.68 have x0: "x0 ~= <0>";
1.69 proof (rule classical);
1.70 @@ -154,7 +157,9 @@
1.71 def H0 == "H + lin x0";
1.72 show ?thesis;
1.73
1.74 -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$.} *};
1.75 + txt {* Pick a real number $\xi$ that fulfills certain
1.76 + inequations, which will be used to establish that $h_0$ is
1.77 + a norm-preserving extension of $h$. *};
1.78
1.79 obtain xi in "ALL y:H. - p (y + x0) - h y <= xi
1.80 & xi <= p (y + x0) - h y";
1.81 @@ -180,7 +185,7 @@
1.82 thus "- p (u + x0) - h u <= p (v + x0) - h v";
1.83 by (rule real_diff_ineq_swap);
1.84 qed;
1.85 - thus ?thesis; by (elim exE) (rule that);
1.86 + thus ?thesis; by blast;
1.87 qed;
1.88
1.89 txt {* Define the extension $h_0$ of $h$ to $H_0$ using $\xi$. *};
2.1 --- a/src/HOL/Real/HahnBanach/ZornLemma.thy Wed Jan 05 12:01:14 2000 +0100
2.2 +++ b/src/HOL/Real/HahnBanach/ZornLemma.thy Wed Jan 05 12:02:24 2000 +0100
2.3 @@ -7,24 +7,22 @@
2.4
2.5 theory ZornLemma = Aux + Zorn:;
2.6
2.7 -text{*
2.8 -Zorn's Lemmas states: if every linear ordered subset of an ordered set
2.9 -$S$ has an upper bound in $S$, then there exists a maximal element in $S$.
2.10 -In our application, $S$ is a set of sets ordered by set inclusion. Since
2.11 -the union of a chain of sets is an upper bound for all elements of the
2.12 -chain, the conditions of Zorn's lemma can be modified:
2.13 -if $S$ is non-empty, it suffices to show that for every non-empty
2.14 -chain $c$ in $S$ the union of $c$ also lies in $S$.
2.15 -*};
2.16 +text {* Zorn's Lemmas states: if every linear ordered subset of an
2.17 +ordered set $S$ has an upper bound in $S$, then there exists a maximal
2.18 +element in $S$. In our application, $S$ is a set of sets ordered by
2.19 +set inclusion. Since the union of a chain of sets is an upper bound
2.20 +for all elements of the chain, the conditions of Zorn's lemma can be
2.21 +modified: if $S$ is non-empty, it suffices to show that for every
2.22 +non-empty chain $c$ in $S$ the union of $c$ also lies in $S$. *};
2.23
2.24 theorem Zorn's_Lemma:
2.25 - "a:S ==> (!!c. c: chain S ==> EX x. x:c ==> Union c : S)
2.26 + "(!!c. c: chain S ==> EX x. x:c ==> Union c : S) ==> a:S
2.27 ==> EX y: S. ALL z: S. y <= z --> y = z";
2.28 proof (rule Zorn_Lemma2);
2.29 - txt_raw{* \footnote{See
2.30 + txt_raw {* \footnote{See
2.31 \url{http://isabelle.in.tum.de/library/HOL/HOL-Real/Zorn.html}}*};
2.32 + assume r: "!!c. c: chain S ==> EX x. x:c ==> Union c : S";
2.33 assume aS: "a:S";
2.34 - assume r: "!!c. c: chain S ==> EX x. x:c ==> Union c : S";
2.35 show "ALL c:chain S. EX y:S. ALL z:c. z <= y";
2.36 proof;
2.37 fix c; assume "c:chain S";