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

author | wenzelm |

Wed, 05 Jan 2000 12:02:24 +0100 | |

changeset 8104 | d9b3a224c0e6 |

parent 8103 | 86f94a8116a9 |

child 8105 | 2dda3e88d23f |

tuned;

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

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

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