--- a/src/HOL/Hahn_Banach/Bounds.thy Tue Oct 21 10:53:24 2014 +0200
+++ b/src/HOL/Hahn_Banach/Bounds.thy Tue Oct 21 10:58:19 2014 +0200
@@ -2,7 +2,7 @@
Author: Gertrud Bauer, TU Munich
*)
-header {* Bounds *}
+header \<open>Bounds\<close>
theory Bounds
imports Main "~~/src/HOL/Library/ContNotDenum"
@@ -28,7 +28,7 @@
interpret lub A x by fact
show ?thesis
proof (unfold the_lub_def)
- from `lub A x` show "The (lub A) = x"
+ from \<open>lub A x\<close> show "The (lub A) = x"
proof
fix x' assume lub': "lub A x'"
show "x' = x"
--- a/src/HOL/Hahn_Banach/Function_Norm.thy Tue Oct 21 10:53:24 2014 +0200
+++ b/src/HOL/Hahn_Banach/Function_Norm.thy Tue Oct 21 10:58:19 2014 +0200
@@ -2,15 +2,15 @@
Author: Gertrud Bauer, TU Munich
*)
-header {* The norm of a function *}
+header \<open>The norm of a function\<close>
theory Function_Norm
imports Normed_Space Function_Order
begin
-subsection {* Continuous linear forms*}
+subsection \<open>Continuous linear forms\<close>
-text {*
+text \<open>
A linear form @{text f} on a normed vector space @{text "(V, \<parallel>\<cdot>\<parallel>)"}
is \emph{continuous}, iff it is bounded, i.e.
\begin{center}
@@ -19,7 +19,7 @@
In our application no other functions than linear forms are
considered, so we can define continuous linear forms as bounded
linear forms:
-*}
+\<close>
locale continuous = linearform +
fixes norm :: "_ \<Rightarrow> real" ("\<parallel>_\<parallel>")
@@ -39,9 +39,9 @@
qed
-subsection {* The norm of a linear form *}
+subsection \<open>The norm of a linear form\<close>
-text {*
+text \<open>
The least real number @{text c} for which holds
\begin{center}
@{text "\<forall>x \<in> V. \<bar>f x\<bar> \<le> c \<cdot> \<parallel>x\<parallel>"}
@@ -70,7 +70,7 @@
@{text fn_norm} is equal to the supremum of @{text B}, if the
supremum exists (otherwise it is undefined).
-*}
+\<close>
locale fn_norm =
fixes norm :: "_ \<Rightarrow> real" ("\<parallel>_\<parallel>")
@@ -83,34 +83,34 @@
lemma (in fn_norm) B_not_empty [intro]: "0 \<in> B V f"
by (simp add: B_def)
-text {*
+text \<open>
The following lemma states that every continuous linear form on a
normed space @{text "(V, \<parallel>\<cdot>\<parallel>)"} has a function norm.
-*}
+\<close>
lemma (in normed_vectorspace_with_fn_norm) fn_norm_works:
assumes "continuous V f norm"
shows "lub (B V f) (\<parallel>f\<parallel>\<hyphen>V)"
proof -
interpret continuous V f norm by fact
- txt {* The existence of the supremum is shown using the
+ txt \<open>The existence of the supremum is shown using the
completeness of the reals. Completeness means, that every
- non-empty bounded set of reals has a supremum. *}
+ non-empty bounded set of reals has a supremum.\<close>
have "\<exists>a. lub (B V f) a"
proof (rule real_complete)
- txt {* First we have to show that @{text B} is non-empty: *}
+ txt \<open>First we have to show that @{text B} is non-empty:\<close>
have "0 \<in> B V f" ..
then show "\<exists>x. x \<in> B V f" ..
- txt {* Then we have to show that @{text B} is bounded: *}
+ txt \<open>Then we have to show that @{text B} is bounded:\<close>
show "\<exists>c. \<forall>y \<in> B V f. y \<le> c"
proof -
- txt {* We know that @{text f} is bounded by some value @{text c}. *}
+ txt \<open>We know that @{text f} is bounded by some value @{text c}.\<close>
from bounded obtain c where c: "\<forall>x \<in> V. \<bar>f x\<bar> \<le> c * \<parallel>x\<parallel>" ..
- txt {* To prove the thesis, we have to show that there is some
+ txt \<open>To prove the thesis, we have to show that there is some
@{text b}, such that @{text "y \<le> b"} for all @{text "y \<in>
- B"}. Due to the definition of @{text B} there are two cases. *}
+ B"}. Due to the definition of @{text B} there are two cases.\<close>
def b \<equiv> "max c 0"
have "\<forall>y \<in> B V f. y \<le> b"
@@ -121,16 +121,16 @@
assume "y = 0"
then show ?thesis unfolding b_def by arith
next
- txt {* The second case is @{text "y = \<bar>f x\<bar> / \<parallel>x\<parallel>"} for some
- @{text "x \<in> V"} with @{text "x \<noteq> 0"}. *}
+ txt \<open>The second case is @{text "y = \<bar>f x\<bar> / \<parallel>x\<parallel>"} for some
+ @{text "x \<in> V"} with @{text "x \<noteq> 0"}.\<close>
assume "y \<noteq> 0"
with y obtain x where y_rep: "y = \<bar>f x\<bar> * inverse \<parallel>x\<parallel>"
and x: "x \<in> V" and neq: "x \<noteq> 0"
by (auto simp add: B_def divide_inverse)
from x neq have gt: "0 < \<parallel>x\<parallel>" ..
- txt {* The thesis follows by a short calculation using the
- fact that @{text f} is bounded. *}
+ txt \<open>The thesis follows by a short calculation using the
+ fact that @{text f} is bounded.\<close>
note y_rep
also have "\<bar>f x\<bar> * inverse \<parallel>x\<parallel> \<le> (c * \<parallel>x\<parallel>) * inverse \<parallel>x\<parallel>"
@@ -162,7 +162,7 @@
proof -
interpret continuous V f norm by fact
have "lub (B V f) (\<parallel>f\<parallel>\<hyphen>V)"
- using `continuous V f norm` by (rule fn_norm_works)
+ using \<open>continuous V f norm\<close> by (rule fn_norm_works)
from this and b show ?thesis ..
qed
@@ -173,32 +173,32 @@
proof -
interpret continuous V f norm by fact
have "lub (B V f) (\<parallel>f\<parallel>\<hyphen>V)"
- using `continuous V f norm` by (rule fn_norm_works)
+ using \<open>continuous V f norm\<close> by (rule fn_norm_works)
from this and b show ?thesis ..
qed
-text {* The norm of a continuous function is always @{text "\<ge> 0"}. *}
+text \<open>The norm of a continuous function is always @{text "\<ge> 0"}.\<close>
lemma (in normed_vectorspace_with_fn_norm) fn_norm_ge_zero [iff]:
assumes "continuous V f norm"
shows "0 \<le> \<parallel>f\<parallel>\<hyphen>V"
proof -
interpret continuous V f norm by fact
- txt {* The function norm is defined as the supremum of @{text B}.
+ txt \<open>The function norm is defined as the supremum of @{text B}.
So it is @{text "\<ge> 0"} if all elements in @{text B} are @{text "\<ge>
- 0"}, provided the supremum exists and @{text B} is not empty. *}
+ 0"}, provided the supremum exists and @{text B} is not empty.\<close>
have "lub (B V f) (\<parallel>f\<parallel>\<hyphen>V)"
- using `continuous V f norm` by (rule fn_norm_works)
+ using \<open>continuous V f norm\<close> by (rule fn_norm_works)
moreover have "0 \<in> B V f" ..
ultimately show ?thesis ..
qed
-text {*
+text \<open>
\medskip The fundamental property of function norms is:
\begin{center}
@{text "\<bar>f x\<bar> \<le> \<parallel>f\<parallel> \<cdot> \<parallel>x\<parallel>"}
\end{center}
-*}
+\<close>
lemma (in normed_vectorspace_with_fn_norm) fn_norm_le_cong:
assumes "continuous V f norm" "linearform V f"
@@ -214,7 +214,7 @@
also have "f 0 = 0" by rule unfold_locales
also have "\<bar>\<dots>\<bar> = 0" by simp
also have a: "0 \<le> \<parallel>f\<parallel>\<hyphen>V"
- using `continuous V f norm` by (rule fn_norm_ge_zero)
+ using \<open>continuous V f norm\<close> by (rule fn_norm_ge_zero)
from x have "0 \<le> norm x" ..
with a have "0 \<le> \<parallel>f\<parallel>\<hyphen>V * \<parallel>x\<parallel>" by (simp add: zero_le_mult_iff)
finally show "\<bar>f x\<bar> \<le> \<parallel>f\<parallel>\<hyphen>V * \<parallel>x\<parallel>" .
@@ -227,20 +227,20 @@
from x show "0 \<le> \<parallel>x\<parallel>" ..
from x and neq have "\<bar>f x\<bar> * inverse \<parallel>x\<parallel> \<in> B V f"
by (auto simp add: B_def divide_inverse)
- with `continuous V f norm` show "\<bar>f x\<bar> * inverse \<parallel>x\<parallel> \<le> \<parallel>f\<parallel>\<hyphen>V"
+ with \<open>continuous V f norm\<close> show "\<bar>f x\<bar> * inverse \<parallel>x\<parallel> \<le> \<parallel>f\<parallel>\<hyphen>V"
by (rule fn_norm_ub)
qed
finally show ?thesis .
qed
qed
-text {*
+text \<open>
\medskip The function norm is the least positive real number for
which the following inequation holds:
\begin{center}
@{text "\<bar>f x\<bar> \<le> c \<cdot> \<parallel>x\<parallel>"}
\end{center}
-*}
+\<close>
lemma (in normed_vectorspace_with_fn_norm) fn_norm_least [intro?]:
assumes "continuous V f norm"
@@ -274,7 +274,7 @@
qed
finally show ?thesis .
qed
- qed (insert `continuous V f norm`, simp_all add: continuous_def)
+ qed (insert \<open>continuous V f norm\<close>, simp_all add: continuous_def)
qed
end
--- a/src/HOL/Hahn_Banach/Function_Order.thy Tue Oct 21 10:53:24 2014 +0200
+++ b/src/HOL/Hahn_Banach/Function_Order.thy Tue Oct 21 10:58:19 2014 +0200
@@ -2,15 +2,15 @@
Author: Gertrud Bauer, TU Munich
*)
-header {* An order on functions *}
+header \<open>An order on functions\<close>
theory Function_Order
imports Subspace Linearform
begin
-subsection {* The graph of a function *}
+subsection \<open>The graph of a function\<close>
-text {*
+text \<open>
We define the \emph{graph} of a (real) function @{text f} with
domain @{text F} as the set
\begin{center}
@@ -19,7 +19,7 @@
So we are modeling partial functions by specifying the domain and
the mapping function. We use the term ``function'' also for its
graph.
-*}
+\<close>
type_synonym 'a graph = "('a \<times> real) set"
@@ -38,12 +38,12 @@
using assms unfolding graph_def by blast
-subsection {* Functions ordered by domain extension *}
+subsection \<open>Functions ordered by domain extension\<close>
-text {*
+text \<open>
A function @{text h'} is an extension of @{text h}, iff the graph of
@{text h} is a subset of the graph of @{text h'}.
-*}
+\<close>
lemma graph_extI:
"(\<And>x. x \<in> H \<Longrightarrow> h x = h' x) \<Longrightarrow> H \<subseteq> H'
@@ -57,12 +57,12 @@
unfolding graph_def by blast
-subsection {* Domain and function of a graph *}
+subsection \<open>Domain and function of a graph\<close>
-text {*
+text \<open>
The inverse functions to @{text graph} are @{text domain} and @{text
funct}.
-*}
+\<close>
definition domain :: "'a graph \<Rightarrow> 'a set"
where "domain g = {x. \<exists>y. (x, y) \<in> g}"
@@ -70,10 +70,10 @@
definition funct :: "'a graph \<Rightarrow> ('a \<Rightarrow> real)"
where "funct g = (\<lambda>x. (SOME y. (x, y) \<in> g))"
-text {*
+text \<open>
The following lemma states that @{text g} is the graph of a function
if the relation induced by @{text g} is unique.
-*}
+\<close>
lemma graph_domain_funct:
assumes uniq: "\<And>x y z. (x, y) \<in> g \<Longrightarrow> (x, z) \<in> g \<Longrightarrow> z = y"
@@ -91,14 +91,14 @@
qed
-subsection {* Norm-preserving extensions of a function *}
+subsection \<open>Norm-preserving extensions of a function\<close>
-text {*
+text \<open>
Given a linear form @{text f} on the space @{text F} and a seminorm
@{text p} on @{text E}. The set of all linear extensions of @{text
f}, to superspaces @{text H} of @{text F}, which are bounded by
@{text p}, is defined as follows.
-*}
+\<close>
definition
norm_pres_extensions ::
--- a/src/HOL/Hahn_Banach/Hahn_Banach.thy Tue Oct 21 10:53:24 2014 +0200
+++ b/src/HOL/Hahn_Banach/Hahn_Banach.thy Tue Oct 21 10:58:19 2014 +0200
@@ -2,20 +2,20 @@
Author: Gertrud Bauer, TU Munich
*)
-header {* The Hahn-Banach Theorem *}
+header \<open>The Hahn-Banach Theorem\<close>
theory Hahn_Banach
imports Hahn_Banach_Lemmas
begin
-text {*
+text \<open>
We present the proof of two different versions of the Hahn-Banach
Theorem, closely following @{cite \<open>\S36\<close> "Heuser:1986"}.
-*}
+\<close>
-subsection {* The Hahn-Banach Theorem for vector spaces *}
+subsection \<open>The Hahn-Banach Theorem for vector spaces\<close>
-text {*
+text \<open>
\textbf{Hahn-Banach Theorem.} Let @{text F} be a subspace of a real
vector space @{text E}, let @{text p} be a semi-norm on @{text E},
and @{text f} be a linear form defined on @{text F} such that @{text
@@ -51,16 +51,16 @@
\end{itemize}
\end{enumerate}
-*}
+\<close>
theorem Hahn_Banach:
assumes E: "vectorspace E" and "subspace F E"
and "seminorm E p" and "linearform F f"
assumes fp: "\<forall>x \<in> F. f x \<le> p x"
shows "\<exists>h. linearform E h \<and> (\<forall>x \<in> F. h x = f x) \<and> (\<forall>x \<in> E. h x \<le> p x)"
- -- {* Let @{text E} be a vector space, @{text F} a subspace of @{text E}, @{text p} a seminorm on @{text E}, *}
- -- {* and @{text f} a linear form on @{text F} such that @{text f} is bounded by @{text p}, *}
- -- {* then @{text f} can be extended to a linear form @{text h} on @{text E} in a norm-preserving way. \skp *}
+ -- \<open>Let @{text E} be a vector space, @{text F} a subspace of @{text E}, @{text p} a seminorm on @{text E},\<close>
+ -- \<open>and @{text f} a linear form on @{text F} such that @{text f} is bounded by @{text p},\<close>
+ -- \<open>then @{text f} can be extended to a linear form @{text h} on @{text E} in a norm-preserving way. \skp\<close>
proof -
interpret vectorspace E by fact
interpret subspace F E by fact
@@ -69,12 +69,12 @@
def M \<equiv> "norm_pres_extensions E p F f"
then have M: "M = \<dots>" by (simp only:)
from E have F: "vectorspace F" ..
- note FE = `F \<unlhd> E`
+ note FE = \<open>F \<unlhd> E\<close>
{
fix c assume cM: "c \<in> chains M" and ex: "\<exists>x. x \<in> c"
have "\<Union>c \<in> M"
- -- {* Show that every non-empty chain @{text c} of @{text M} has an upper bound in @{text M}: *}
- -- {* @{text "\<Union>c"} is greater than any element of the chain @{text c}, so it suffices to show @{text "\<Union>c \<in> M"}. *}
+ -- \<open>Show that every non-empty chain @{text c} of @{text M} has an upper bound in @{text M}:\<close>
+ -- \<open>@{text "\<Union>c"} is greater than any element of the chain @{text c}, so it suffices to show @{text "\<Union>c \<in> M"}.\<close>
unfolding M_def
proof (rule norm_pres_extensionI)
let ?H = "domain (\<Union>c)"
@@ -104,9 +104,9 @@
qed
}
then have "\<exists>g \<in> M. \<forall>x \<in> M. g \<subseteq> x \<longrightarrow> x = g"
- -- {* With Zorn's Lemma we can conclude that there is a maximal element in @{text M}. \skp *}
+ -- \<open>With Zorn's Lemma we can conclude that there is a maximal element in @{text M}. \skp\<close>
proof (rule Zorn's_Lemma)
- -- {* We show that @{text M} is non-empty: *}
+ -- \<open>We show that @{text M} is non-empty:\<close>
show "graph F f \<in> M"
unfolding M_def
proof (rule norm_pres_extensionI2)
@@ -125,18 +125,18 @@
and HE: "H \<unlhd> E" and FH: "F \<unlhd> H"
and graphs: "graph F f \<subseteq> graph H h"
and hp: "\<forall>x \<in> H. h x \<le> p x" unfolding M_def ..
- -- {* @{text g} is a norm-preserving extension of @{text f}, in other words: *}
- -- {* @{text g} is the graph of some linear form @{text h} defined on a subspace @{text H} of @{text E}, *}
- -- {* and @{text h} is an extension of @{text f} that is again bounded by @{text p}. \skp *}
+ -- \<open>@{text g} is a norm-preserving extension of @{text f}, in other words:\<close>
+ -- \<open>@{text g} is the graph of some linear form @{text h} defined on a subspace @{text H} of @{text E},\<close>
+ -- \<open>and @{text h} is an extension of @{text f} that is again bounded by @{text p}. \skp\<close>
from HE E have H: "vectorspace H"
by (rule subspace.vectorspace)
have HE_eq: "H = E"
- -- {* We show that @{text h} is defined on whole @{text E} by classical contradiction. \skp *}
+ -- \<open>We show that @{text h} is defined on whole @{text E} by classical contradiction. \skp\<close>
proof (rule classical)
assume neq: "H \<noteq> E"
- -- {* Assume @{text h} is not defined on whole @{text E}. Then show that @{text h} can be extended *}
- -- {* in a norm-preserving way to a function @{text h'} with the graph @{text g'}. \skp *}
+ -- \<open>Assume @{text h} is not defined on whole @{text E}. Then show that @{text h} can be extended\<close>
+ -- \<open>in a norm-preserving way to a function @{text h'} with the graph @{text g'}. \skp\<close>
have "\<exists>g' \<in> M. g \<subseteq> g' \<and> g \<noteq> g'"
proof -
from HE have "H \<subseteq> E" ..
@@ -147,12 +147,12 @@
proof
assume "x' = 0"
with H have "x' \<in> H" by (simp only: vectorspace.zero)
- with `x' \<notin> H` show False by contradiction
+ with \<open>x' \<notin> H\<close> show False by contradiction
qed
qed
def H' \<equiv> "H + lin x'"
- -- {* Define @{text H'} as the direct sum of @{text H} and the linear closure of @{text x'}. \skp *}
+ -- \<open>Define @{text H'} as the direct sum of @{text H} and the linear closure of @{text x'}. \skp\<close>
have HH': "H \<unlhd> H'"
proof (unfold H'_def)
from x'E have "vectorspace (lin x')" ..
@@ -162,9 +162,9 @@
obtain xi where
xi: "\<forall>y \<in> H. - p (y + x') - h y \<le> xi
\<and> xi \<le> p (y + x') - h y"
- -- {* Pick a real number @{text \<xi>} that fulfills certain inequations; this will *}
- -- {* be used to establish that @{text h'} is a norm-preserving extension of @{text h}.
- \label{ex-xi-use}\skp *}
+ -- \<open>Pick a real number @{text \<xi>} that fulfills certain inequations; this will\<close>
+ -- \<open>be used to establish that @{text h'} is a norm-preserving extension of @{text h}.
+ \label{ex-xi-use}\skp\<close>
proof -
from H have "\<exists>xi. \<forall>y \<in> H. - p (y + x') - h y \<le> xi
\<and> xi \<le> p (y + x') - h y"
@@ -191,10 +191,10 @@
def h' \<equiv> "\<lambda>x. let (y, a) =
SOME (y, a). x = y + a \<cdot> x' \<and> y \<in> H in h y + a * xi"
- -- {* Define the extension @{text h'} of @{text h} to @{text H'} using @{text \<xi>}. \skp *}
+ -- \<open>Define the extension @{text h'} of @{text h} to @{text H'} using @{text \<xi>}. \skp\<close>
have "g \<subseteq> graph H' h' \<and> g \<noteq> graph H' h'"
- -- {* @{text h'} is an extension of @{text h} \dots \skp *}
+ -- \<open>@{text h'} is an extension of @{text h} \dots \skp\<close>
proof
show "g \<subseteq> graph H' h'"
proof -
@@ -202,7 +202,7 @@
proof (rule graph_extI)
fix t assume t: "t \<in> H"
from E HE t have "(SOME (y, a). t = y + a \<cdot> x' \<and> y \<in> H) = (t, 0)"
- using `x' \<notin> H` `x' \<in> E` `x' \<noteq> 0` by (rule decomp_H'_H)
+ using \<open>x' \<notin> H\<close> \<open>x' \<in> E\<close> \<open>x' \<noteq> 0\<close> by (rule decomp_H'_H)
with h'_def show "h t = h' t" by (simp add: Let_def)
next
from HH' show "H \<subseteq> H'" ..
@@ -225,18 +225,18 @@
then have "(x', h' x') \<in> graph H' h'" ..
with eq have "(x', h' x') \<in> graph H h" by (simp only:)
then have "x' \<in> H" ..
- with `x' \<notin> H` show False by contradiction
+ with \<open>x' \<notin> H\<close> show False by contradiction
qed
with g_rep show ?thesis by simp
qed
qed
moreover have "graph H' h' \<in> M"
- -- {* and @{text h'} is norm-preserving. \skp *}
+ -- \<open>and @{text h'} is norm-preserving. \skp\<close>
proof (unfold M_def)
show "graph H' h' \<in> norm_pres_extensions E p F f"
proof (rule norm_pres_extensionI2)
show "linearform H' h'"
- using h'_def H'_def HE linearform `x' \<notin> H` `x' \<in> E` `x' \<noteq> 0` E
+ using h'_def H'_def HE linearform \<open>x' \<notin> H\<close> \<open>x' \<in> E\<close> \<open>x' \<noteq> 0\<close> E
by (rule h'_lf)
show "H' \<unlhd> E"
unfolding H'_def
@@ -245,7 +245,7 @@
show "vectorspace E" by fact
from x'E show "lin x' \<unlhd> E" ..
qed
- from H `F \<unlhd> H` HH' show FH': "F \<unlhd> H'"
+ from H \<open>F \<unlhd> H\<close> HH' show FH': "F \<unlhd> H'"
by (rule vectorspace.subspace_trans)
show "graph F f \<subseteq> graph H' h'"
proof (rule graph_extI)
@@ -271,15 +271,15 @@
from FH' show "F \<subseteq> H'" ..
qed
show "\<forall>x \<in> H'. h' x \<le> p x"
- using h'_def H'_def `x' \<notin> H` `x' \<in> E` `x' \<noteq> 0` E HE
- `seminorm E p` linearform and hp xi
+ using h'_def H'_def \<open>x' \<notin> H\<close> \<open>x' \<in> E\<close> \<open>x' \<noteq> 0\<close> E HE
+ \<open>seminorm E p\<close> linearform and hp xi
by (rule h'_norm_pres)
qed
qed
ultimately show ?thesis ..
qed
then have "\<not> (\<forall>x \<in> M. g \<subseteq> x \<longrightarrow> g = x)" by simp
- -- {* So the graph @{text g} of @{text h} cannot be maximal. Contradiction! \skp *}
+ -- \<open>So the graph @{text g} of @{text h} cannot be maximal. Contradiction! \skp\<close>
with gx show "H = E" by contradiction
qed
@@ -297,9 +297,9 @@
qed
-subsection {* Alternative formulation *}
+subsection \<open>Alternative formulation\<close>
-text {*
+text \<open>
The following alternative formulation of the Hahn-Banach
Theorem\label{abs-Hahn-Banach} uses the fact that for a real linear
form @{text f} and a seminorm @{text p} the following inequations
@@ -311,7 +311,7 @@
@{text "\<forall>x \<in> H. h x \<le> p x"} \\
\end{tabular}
\end{center}
-*}
+\<close>
theorem abs_Hahn_Banach:
assumes E: "vectorspace E" and FE: "subspace F E"
@@ -342,13 +342,13 @@
qed
-subsection {* The Hahn-Banach Theorem for normed spaces *}
+subsection \<open>The Hahn-Banach Theorem for normed spaces\<close>
-text {*
+text \<open>
Every continuous linear form @{text f} on a subspace @{text F} of a
norm space @{text E}, can be extended to a continuous linear form
@{text g} on @{text E} such that @{text "\<parallel>f\<parallel> = \<parallel>g\<parallel>"}.
-*}
+\<close>
theorem norm_Hahn_Banach:
fixes V and norm ("\<parallel>_\<parallel>")
@@ -375,23 +375,23 @@
have ge_zero: "0 \<le> \<parallel>f\<parallel>\<hyphen>F"
by (rule normed_vectorspace_with_fn_norm.fn_norm_ge_zero
[OF normed_vectorspace_with_fn_norm.intro,
- OF F_norm `continuous F f norm` , folded B_def fn_norm_def])
- txt {* We define a function @{text p} on @{text E} as follows:
- @{text "p x = \<parallel>f\<parallel> \<cdot> \<parallel>x\<parallel>"} *}
+ OF F_norm \<open>continuous F f norm\<close> , folded B_def fn_norm_def])
+ txt \<open>We define a function @{text p} on @{text E} as follows:
+ @{text "p x = \<parallel>f\<parallel> \<cdot> \<parallel>x\<parallel>"}\<close>
def p \<equiv> "\<lambda>x. \<parallel>f\<parallel>\<hyphen>F * \<parallel>x\<parallel>"
- txt {* @{text p} is a seminorm on @{text E}: *}
+ txt \<open>@{text p} is a seminorm on @{text E}:\<close>
have q: "seminorm E p"
proof
fix x y a assume x: "x \<in> E" and y: "y \<in> E"
- txt {* @{text p} is positive definite: *}
+ txt \<open>@{text p} is positive definite:\<close>
have "0 \<le> \<parallel>f\<parallel>\<hyphen>F" by (rule ge_zero)
moreover from x have "0 \<le> \<parallel>x\<parallel>" ..
ultimately show "0 \<le> p x"
by (simp add: p_def zero_le_mult_iff)
- txt {* @{text p} is absolutely homogeneous: *}
+ txt \<open>@{text p} is absolutely homogeneous:\<close>
show "p (a \<cdot> x) = \<bar>a\<bar> * p x"
proof -
@@ -402,7 +402,7 @@
finally show ?thesis .
qed
- txt {* Furthermore, @{text p} is subadditive: *}
+ txt \<open>Furthermore, @{text p} is subadditive:\<close>
show "p (x + y) \<le> p x + p y"
proof -
@@ -417,22 +417,22 @@
qed
qed
- txt {* @{text f} is bounded by @{text p}. *}
+ txt \<open>@{text f} is bounded by @{text p}.\<close>
have "\<forall>x \<in> F. \<bar>f x\<bar> \<le> p x"
proof
fix x assume "x \<in> F"
- with `continuous F f norm` and linearform
+ with \<open>continuous F f norm\<close> and linearform
show "\<bar>f x\<bar> \<le> p x"
unfolding p_def by (rule normed_vectorspace_with_fn_norm.fn_norm_le_cong
[OF normed_vectorspace_with_fn_norm.intro,
OF F_norm, folded B_def fn_norm_def])
qed
- txt {* Using the fact that @{text p} is a seminorm and @{text f} is bounded
+ txt \<open>Using the fact that @{text p} is a seminorm and @{text f} is bounded
by @{text p} we can apply the Hahn-Banach Theorem for real vector
spaces. So @{text f} can be extended in a norm-preserving way to
- some function @{text g} on the whole vector space @{text E}. *}
+ some function @{text g} on the whole vector space @{text E}.\<close>
with E FE linearform q obtain g where
linearformE: "linearform E g"
@@ -440,7 +440,7 @@
and b: "\<forall>x \<in> E. \<bar>g x\<bar> \<le> p x"
by (rule abs_Hahn_Banach [elim_format]) iprover
- txt {* We furthermore have to show that @{text g} is also continuous: *}
+ txt \<open>We furthermore have to show that @{text g} is also continuous:\<close>
have g_cont: "continuous E g norm" using linearformE
proof
@@ -449,11 +449,11 @@
by (simp only: p_def)
qed
- txt {* To complete the proof, we show that @{text "\<parallel>g\<parallel> = \<parallel>f\<parallel>"}. *}
+ txt \<open>To complete the proof, we show that @{text "\<parallel>g\<parallel> = \<parallel>f\<parallel>"}.\<close>
have "\<parallel>g\<parallel>\<hyphen>E = \<parallel>f\<parallel>\<hyphen>F"
proof (rule order_antisym)
- txt {*
+ txt \<open>
First we show @{text "\<parallel>g\<parallel> \<le> \<parallel>f\<parallel>"}. The function norm @{text
"\<parallel>g\<parallel>"} is defined as the smallest @{text "c \<in> \<real>"} such that
\begin{center}
@@ -467,7 +467,7 @@
@{text "\<forall>x \<in> E. \<bar>g x\<bar> \<le> \<parallel>f\<parallel> \<cdot> \<parallel>x\<parallel>"}
\end{tabular}
\end{center}
- *}
+\<close>
from g_cont _ ge_zero
show "\<parallel>g\<parallel>\<hyphen>E \<le> \<parallel>f\<parallel>\<hyphen>F"
@@ -477,7 +477,7 @@
by (simp only: p_def)
qed
- txt {* The other direction is achieved by a similar argument. *}
+ txt \<open>The other direction is achieved by a similar argument.\<close>
show "\<parallel>f\<parallel>\<hyphen>F \<le> \<parallel>g\<parallel>\<hyphen>E"
proof (rule normed_vectorspace_with_fn_norm.fn_norm_least
--- a/src/HOL/Hahn_Banach/Hahn_Banach_Ext_Lemmas.thy Tue Oct 21 10:53:24 2014 +0200
+++ b/src/HOL/Hahn_Banach/Hahn_Banach_Ext_Lemmas.thy Tue Oct 21 10:58:19 2014 +0200
@@ -2,13 +2,13 @@
Author: Gertrud Bauer, TU Munich
*)
-header {* Extending non-maximal functions *}
+header \<open>Extending non-maximal functions\<close>
theory Hahn_Banach_Ext_Lemmas
imports Function_Norm
begin
-text {*
+text \<open>
In this section the following context is presumed. Let @{text E} be
a real vector space with a seminorm @{text q} on @{text E}. @{text
F} is a subspace of @{text E} and @{text f} a linear function on
@@ -38,7 +38,7 @@
@{text "\<forall>u \<in> F. \<forall>v \<in> F. a u \<le> b v"}
\end{tabular}
\end{center}
-*}
+\<close>
lemma ex_xi:
assumes "vectorspace F"
@@ -46,9 +46,9 @@
shows "\<exists>xi::real. \<forall>y \<in> F. a y \<le> xi \<and> xi \<le> b y"
proof -
interpret vectorspace F by fact
- txt {* From the completeness of the reals follows:
+ txt \<open>From the completeness of the reals follows:
The set @{text "S = {a u. u \<in> F}"} has a supremum, if it is
- non-empty and has an upper bound. *}
+ non-empty and has an upper bound.\<close>
let ?S = "{a u | u. u \<in> F}"
have "\<exists>xi. lub ?S xi"
@@ -81,11 +81,11 @@
} ultimately show "\<exists>xi. \<forall>y \<in> F. a y \<le> xi \<and> xi \<le> b y" by blast
qed
-text {*
+text \<open>
\medskip The function @{text h'} is defined as a @{text "h' x = h y
+ a \<cdot> \<xi>"} where @{text "x = y + a \<cdot> \<xi>"} is a linear extension of
@{text h} to @{text H'}.
-*}
+\<close>
lemma h'_lf:
assumes h'_def: "h' \<equiv> \<lambda>x. let (y, a) =
@@ -101,10 +101,10 @@
interpret vectorspace E by fact
show ?thesis
proof
- note E = `vectorspace E`
+ note E = \<open>vectorspace E\<close>
have H': "vectorspace H'"
proof (unfold H'_def)
- from `x0 \<in> E`
+ from \<open>x0 \<in> E\<close>
have "lin x0 \<unlhd> E" ..
with HE show "vectorspace (H + lin x0)" using E ..
qed
@@ -121,7 +121,7 @@
unfolding H'_def sum_def lin_def by blast
have ya: "y1 + y2 = y \<and> a1 + a2 = a" using E HE _ y x0
- proof (rule decomp_H') txt_raw {* \label{decomp-H-use} *}
+ proof (rule decomp_H') txt_raw \<open>\label{decomp-H-use}\<close>
from HE y1 y2 show "y1 + y2 \<in> H"
by (rule subspace.add_closed)
from x0 and HE y y1 y2
@@ -188,8 +188,8 @@
qed
qed
-text {* \medskip The linear extension @{text h'} of @{text h}
- is bounded by the seminorm @{text p}. *}
+text \<open>\medskip The linear extension @{text h'} of @{text h}
+ is bounded by the seminorm @{text p}.\<close>
lemma h'_norm_pres:
assumes h'_def: "h' \<equiv> \<lambda>x. let (y, a) =
@@ -229,8 +229,8 @@
also from x0 y' z have "p y = p (y + a \<cdot> x0)" by simp
finally show ?thesis .
next
- txt {* In the case @{text "a < 0"}, we use @{text "a\<^sub>1"}
- with @{text ya} taken as @{text "y / a"}: *}
+ txt \<open>In the case @{text "a < 0"}, we use @{text "a\<^sub>1"}
+ with @{text ya} taken as @{text "y / a"}:\<close>
assume lz: "a < 0" then have nz: "a \<noteq> 0" by simp
from a1 ay
have "- p (inverse a \<cdot> y + x0) - h (inverse a \<cdot> y) \<le> xi" ..
@@ -251,8 +251,8 @@
finally have "a * xi \<le> p (y + a \<cdot> x0) - h y" .
then show ?thesis by simp
next
- txt {* In the case @{text "a > 0"}, we use @{text "a\<^sub>2"}
- with @{text ya} taken as @{text "y / a"}: *}
+ txt \<open>In the case @{text "a > 0"}, we use @{text "a\<^sub>2"}
+ with @{text ya} taken as @{text "y / a"}:\<close>
assume gz: "0 < a" then have nz: "a \<noteq> 0" by simp
from a2 ay
have "xi \<le> p (inverse a \<cdot> y + x0) - h (inverse a \<cdot> y)" ..
--- a/src/HOL/Hahn_Banach/Hahn_Banach_Sup_Lemmas.thy Tue Oct 21 10:53:24 2014 +0200
+++ b/src/HOL/Hahn_Banach/Hahn_Banach_Sup_Lemmas.thy Tue Oct 21 10:58:19 2014 +0200
@@ -2,13 +2,13 @@
Author: Gertrud Bauer, TU Munich
*)
-header {* The supremum w.r.t.~the function order *}
+header \<open>The supremum w.r.t.~the function order\<close>
theory Hahn_Banach_Sup_Lemmas
imports Function_Norm Zorn_Lemma
begin
-text {*
+text \<open>
This section contains some lemmas that will be used in the proof of
the Hahn-Banach Theorem. In this section the following context is
presumed. Let @{text E} be a real vector space with a seminorm
@@ -22,7 +22,7 @@
the function @{text f} and let @{text "graph H h"} be the supremum
of @{text c}. Every element in @{text H} is member of one of the
elements of the chain.
-*}
+\<close>
lemmas [dest?] = chainsD
lemmas chainsE2 [elim?] = chainsD2 [elim_format]
@@ -53,13 +53,13 @@
ultimately show ?thesis using * by blast
qed
-text {*
+text \<open>
\medskip Let @{text c} be a chain of norm-preserving extensions of
the function @{text f} and let @{text "graph H h"} be the supremum
of @{text c}. Every element in the domain @{text H} of the supremum
function is member of the domain @{text H'} of some function @{text
h'}, such that @{text h} extends @{text h'}.
-*}
+\<close>
lemma some_H'h':
assumes M: "M = norm_pres_extensions E p F f"
@@ -81,12 +81,12 @@
ultimately show ?thesis using * by blast
qed
-text {*
+text \<open>
\medskip Any two elements @{text x} and @{text y} in the domain
@{text H} of the supremum function @{text h} are both in the domain
@{text H'} of some function @{text h'}, such that @{text h} extends
@{text h'}.
-*}
+\<close>
lemma some_H'h'2:
assumes M: "M = norm_pres_extensions E p F f"
@@ -99,8 +99,8 @@
\<and> linearform H' h' \<and> H' \<unlhd> E \<and> F \<unlhd> H'
\<and> graph F f \<subseteq> graph H' h' \<and> (\<forall>x \<in> H'. h' x \<le> p x)"
proof -
- txt {* @{text y} is in the domain @{text H''} of some function @{text h''},
- such that @{text h} extends @{text h''}. *}
+ txt \<open>@{text y} is in the domain @{text H''} of some function @{text h''},
+ such that @{text h} extends @{text h''}.\<close>
from M cM u and y obtain H' h' where
y_hy: "(y, h y) \<in> graph H' h'"
@@ -110,8 +110,8 @@
"graph F f \<subseteq> graph H' h'" "\<forall>x \<in> H'. h' x \<le> p x"
by (rule some_H'h't [elim_format]) blast
- txt {* @{text x} is in the domain @{text H'} of some function @{text h'},
- such that @{text h} extends @{text h'}. *}
+ txt \<open>@{text x} is in the domain @{text H'} of some function @{text h'},
+ such that @{text h} extends @{text h'}.\<close>
from M cM u and x obtain H'' h'' where
x_hx: "(x, h x) \<in> graph H'' h''"
@@ -121,10 +121,10 @@
"graph F f \<subseteq> graph H'' h''" "\<forall>x \<in> H''. h'' x \<le> p x"
by (rule some_H'h't [elim_format]) blast
- txt {* Since both @{text h'} and @{text h''} are elements of the chain,
+ txt \<open>Since both @{text h'} and @{text h''} are elements of the chain,
@{text h''} is an extension of @{text h'} or vice versa. Thus both
@{text x} and @{text y} are contained in the greater
- one. \label{cases1}*}
+ one. \label{cases1}\<close>
from cM c'' c' have "graph H'' h'' \<subseteq> graph H' h' \<or> graph H' h' \<subseteq> graph H'' h''"
(is "?case1 \<or> ?case2") ..
@@ -151,10 +151,10 @@
qed
qed
-text {*
+text \<open>
\medskip The relation induced by the graph of the supremum of a
chain @{text c} is definite, i.~e.~t is the graph of a function.
-*}
+\<close>
lemma sup_definite:
assumes M_def: "M \<equiv> norm_pres_extensions E p F f"
@@ -175,9 +175,9 @@
then obtain H2 h2 where G2_rep: "G2 = graph H2 h2"
unfolding M_def by blast
- txt {* @{text "G\<^sub>1"} is contained in @{text "G\<^sub>2"}
+ txt \<open>@{text "G\<^sub>1"} is contained in @{text "G\<^sub>2"}
or vice versa, since both @{text "G\<^sub>1"} and @{text
- "G\<^sub>2"} are members of @{text c}. \label{cases2}*}
+ "G\<^sub>2"} are members of @{text c}. \label{cases2}\<close>
from cM G1 G2 have "G1 \<subseteq> G2 \<or> G2 \<subseteq> G1" (is "?case1 \<or> ?case2") ..
then show ?thesis
@@ -200,14 +200,14 @@
qed
qed
-text {*
+text \<open>
\medskip The limit function @{text h} is linear. Every element
@{text x} in the domain of @{text h} is in the domain of a function
@{text h'} in the chain of norm preserving extensions. Furthermore,
@{text h} is an extension of @{text h'} so the function values of
@{text x} are identical for @{text h'} and @{text h}. Finally, the
function @{text h'} is linear by construction of @{text M}.
-*}
+\<close>
lemma sup_lf:
assumes M: "M = norm_pres_extensions E p F f"
@@ -255,12 +255,12 @@
qed
qed
-text {*
+text \<open>
\medskip The limit of a non-empty chain of norm preserving
extensions of @{text f} is an extension of @{text f}, since every
element of the chain is an extension of @{text f} and the supremum
is an extension for every element of the chain.
-*}
+\<close>
lemma sup_ext:
assumes graph: "graph H h = \<Union>c"
@@ -281,12 +281,12 @@
finally show ?thesis .
qed
-text {*
+text \<open>
\medskip The domain @{text H} of the limit function is a superspace
of @{text F}, since @{text F} is a subset of @{text H}. The
existence of the @{text 0} element in @{text F} and the closure
properties follow from the fact that @{text F} is a vector space.
-*}
+\<close>
lemma sup_supF:
assumes graph: "graph H h = \<Union>c"
@@ -306,10 +306,10 @@
with FE show "a \<cdot> x \<in> F" by (rule subspace.mult_closed)
qed
-text {*
+text \<open>
\medskip The domain @{text H} of the limit function is a subspace of
@{text E}.
-*}
+\<close>
lemma sup_subE:
assumes graph: "graph H h = \<Union>c"
@@ -362,10 +362,10 @@
qed
qed
-text {*
+text \<open>
\medskip The limit function is bounded by the norm @{text p} as
well, since all elements in the chain are bounded by @{text p}.
-*}
+\<close>
lemma sup_norm_pres:
assumes graph: "graph H h = \<Union>c"
@@ -383,7 +383,7 @@
finally show "h x \<le> p x" .
qed
-text {*
+text \<open>
\medskip The following lemma is a property of linear forms on real
vector spaces. It will be used for the lemma @{text abs_Hahn_Banach}
(see page \pageref{abs-Hahn_Banach}). \label{abs-ineq-iff} For real
@@ -394,7 +394,7 @@
@{text "\<forall>x \<in> H. h x \<le> p x"} \\
\end{tabular}
\end{center}
-*}
+\<close>
lemma abs_ineq_iff:
assumes "subspace H E" and "vectorspace E" and "seminorm E p"
@@ -405,7 +405,7 @@
interpret vectorspace E by fact
interpret seminorm E p by fact
interpret linearform H h by fact
- have H: "vectorspace H" using `vectorspace E` ..
+ have H: "vectorspace H" using \<open>vectorspace E\<close> ..
{
assume l: ?L
show ?R
@@ -422,13 +422,13 @@
fix x assume x: "x \<in> H"
show "\<And>a b :: real. - a \<le> b \<Longrightarrow> b \<le> a \<Longrightarrow> \<bar>b\<bar> \<le> a"
by arith
- from `linearform H h` and H x
+ from \<open>linearform H h\<close> and H x
have "- h x = h (- x)" by (rule linearform.neg [symmetric])
also
from H x have "- x \<in> H" by (rule vectorspace.neg_closed)
with r have "h (- x) \<le> p (- x)" ..
also have "\<dots> = p x"
- using `seminorm E p` `vectorspace E`
+ using \<open>seminorm E p\<close> \<open>vectorspace E\<close>
proof (rule seminorm.minus)
from x show "x \<in> E" ..
qed
--- a/src/HOL/Hahn_Banach/Linearform.thy Tue Oct 21 10:53:24 2014 +0200
+++ b/src/HOL/Hahn_Banach/Linearform.thy Tue Oct 21 10:58:19 2014 +0200
@@ -2,16 +2,16 @@
Author: Gertrud Bauer, TU Munich
*)
-header {* Linearforms *}
+header \<open>Linearforms\<close>
theory Linearform
imports Vector_Space
begin
-text {*
+text \<open>
A \emph{linear form} is a function on a vector space into the reals
that is additive and multiplicative.
-*}
+\<close>
locale linearform =
fixes V :: "'a\<Colon>{minus, plus, zero, uminus} set" and f
@@ -40,11 +40,11 @@
assume x: "x \<in> V" and y: "y \<in> V"
then have "x - y = x + - y" by (rule diff_eq1)
also have "f \<dots> = f x + f (- y)" by (rule add) (simp_all add: x y)
- also have "f (- y) = - f y" using `vectorspace V` y by (rule neg)
+ also have "f (- y) = - f y" using \<open>vectorspace V\<close> y by (rule neg)
finally show ?thesis by simp
qed
-text {* Every linear form yields @{text 0} for the @{text 0} vector. *}
+text \<open>Every linear form yields @{text 0} for the @{text 0} vector.\<close>
lemma (in linearform) zero [iff]:
assumes "vectorspace V"
@@ -52,7 +52,7 @@
proof -
interpret vectorspace V by fact
have "f 0 = f (0 - 0)" by simp
- also have "\<dots> = f 0 - f 0" using `vectorspace V` by (rule diff) simp_all
+ also have "\<dots> = f 0 - f 0" using \<open>vectorspace V\<close> by (rule diff) simp_all
also have "\<dots> = 0" by simp
finally show ?thesis .
qed
--- a/src/HOL/Hahn_Banach/Normed_Space.thy Tue Oct 21 10:53:24 2014 +0200
+++ b/src/HOL/Hahn_Banach/Normed_Space.thy Tue Oct 21 10:58:19 2014 +0200
@@ -2,19 +2,19 @@
Author: Gertrud Bauer, TU Munich
*)
-header {* Normed vector spaces *}
+header \<open>Normed vector spaces\<close>
theory Normed_Space
imports Subspace
begin
-subsection {* Quasinorms *}
+subsection \<open>Quasinorms\<close>
-text {*
+text \<open>
A \emph{seminorm} @{text "\<parallel>\<cdot>\<parallel>"} is a function on a real vector space
into the reals that has the following properties: it is positive
definite, absolute homogeneous and subadditive.
-*}
+\<close>
locale seminorm =
fixes V :: "'a\<Colon>{minus, plus, zero, uminus} set"
@@ -54,23 +54,23 @@
qed
-subsection {* Norms *}
+subsection \<open>Norms\<close>
-text {*
+text \<open>
A \emph{norm} @{text "\<parallel>\<cdot>\<parallel>"} is a seminorm that maps only the
@{text 0} vector to @{text 0}.
-*}
+\<close>
locale norm = seminorm +
assumes zero_iff [iff]: "x \<in> V \<Longrightarrow> (\<parallel>x\<parallel> = 0) = (x = 0)"
-subsection {* Normed vector spaces *}
+subsection \<open>Normed vector spaces\<close>
-text {*
+text \<open>
A vector space together with a norm is called a \emph{normed
space}.
-*}
+\<close>
locale normed_vectorspace = vectorspace + norm
@@ -90,9 +90,9 @@
finally show ?thesis .
qed
-text {*
+text \<open>
Any subspace of a normed vector space is again a normed vectorspace.
-*}
+\<close>
lemma subspace_normed_vs [intro?]:
fixes F E norm
--- a/src/HOL/Hahn_Banach/Subspace.thy Tue Oct 21 10:53:24 2014 +0200
+++ b/src/HOL/Hahn_Banach/Subspace.thy Tue Oct 21 10:58:19 2014 +0200
@@ -2,19 +2,19 @@
Author: Gertrud Bauer, TU Munich
*)
-header {* Subspaces *}
+header \<open>Subspaces\<close>
theory Subspace
imports Vector_Space "~~/src/HOL/Library/Set_Algebras"
begin
-subsection {* Definition *}
+subsection \<open>Definition\<close>
-text {*
+text \<open>
A non-empty subset @{text U} of a vector space @{text V} is a
\emph{subspace} of @{text V}, iff @{text U} is closed under addition
and scalar multiplication.
-*}
+\<close>
locale subspace =
fixes U :: "'a\<Colon>{minus, plus, zero, uminus} set" and V
@@ -49,11 +49,11 @@
from x y show ?thesis by (simp add: diff_eq1 negate_eq1)
qed
-text {*
+text \<open>
\medskip Similar as for linear spaces, the existence of the zero
element in every subspace follows from the non-emptiness of the
carrier set and by vector space laws.
-*}
+\<close>
lemma (in subspace) zero [intro]:
assumes "vectorspace V"
@@ -63,7 +63,7 @@
have "U \<noteq> {}" by (rule non_empty)
then obtain x where x: "x \<in> U" by blast
then have "x \<in> V" .. then have "0 = x - x" by simp
- also from `vectorspace V` x x have "\<dots> \<in> U" by (rule diff_closed)
+ also from \<open>vectorspace V\<close> x x have "\<dots> \<in> U" by (rule diff_closed)
finally show ?thesis .
qed
@@ -76,7 +76,7 @@
from x show ?thesis by (simp add: negate_eq1)
qed
-text {* \medskip Further derived laws: every subspace is a vector space. *}
+text \<open>\medskip Further derived laws: every subspace is a vector space.\<close>
lemma (in subspace) vectorspace [iff]:
assumes "vectorspace V"
@@ -104,7 +104,7 @@
qed
-text {* The subspace relation is reflexive. *}
+text \<open>The subspace relation is reflexive.\<close>
lemma (in vectorspace) subspace_refl [intro]: "V \<unlhd> V"
proof
@@ -117,7 +117,7 @@
from x show "a \<cdot> x \<in> V" by simp
qed
-text {* The subspace relation is transitive. *}
+text \<open>The subspace relation is transitive.\<close>
lemma (in vectorspace) subspace_trans [trans]:
"U \<unlhd> V \<Longrightarrow> V \<unlhd> W \<Longrightarrow> U \<unlhd> W"
@@ -136,12 +136,12 @@
qed
-subsection {* Linear closure *}
+subsection \<open>Linear closure\<close>
-text {*
+text \<open>
The \emph{linear closure} of a vector @{text x} is the set of all
scalar multiples of @{text x}.
-*}
+\<close>
definition lin :: "('a::{minus, plus, zero}) \<Rightarrow> 'a set"
where "lin x = {a \<cdot> x | a. True}"
@@ -156,7 +156,7 @@
unfolding lin_def by blast
-text {* Every vector is contained in its linear closure. *}
+text \<open>Every vector is contained in its linear closure.\<close>
lemma (in vectorspace) x_lin_x [iff]: "x \<in> V \<Longrightarrow> x \<in> lin x"
proof -
@@ -172,7 +172,7 @@
then show "0 = 0 \<cdot> x" by simp
qed
-text {* Any linear closure is a subspace. *}
+text \<open>Any linear closure is a subspace.\<close>
lemma (in vectorspace) lin_subspace [intro]:
assumes x: "x \<in> V"
@@ -208,25 +208,25 @@
qed
-text {* Any linear closure is a vector space. *}
+text \<open>Any linear closure is a vector space.\<close>
lemma (in vectorspace) lin_vectorspace [intro]:
assumes "x \<in> V"
shows "vectorspace (lin x)"
proof -
- from `x \<in> V` have "subspace (lin x) V"
+ from \<open>x \<in> V\<close> have "subspace (lin x) V"
by (rule lin_subspace)
from this and vectorspace_axioms show ?thesis
by (rule subspace.vectorspace)
qed
-subsection {* Sum of two vectorspaces *}
+subsection \<open>Sum of two vectorspaces\<close>
-text {*
+text \<open>
The \emph{sum} of two vectorspaces @{text U} and @{text V} is the
set of all sums of elements from @{text U} and @{text V}.
-*}
+\<close>
lemma sum_def: "U + V = {u + v | u v. u \<in> U \<and> v \<in> V}"
unfolding set_plus_def by auto
@@ -243,7 +243,7 @@
"u \<in> U \<Longrightarrow> v \<in> V \<Longrightarrow> u + v \<in> U + V"
unfolding sum_def by blast
-text {* @{text U} is a subspace of @{text "U + V"}. *}
+text \<open>@{text U} is a subspace of @{text "U + V"}.\<close>
lemma subspace_sum1 [iff]:
assumes "vectorspace U" "vectorspace V"
@@ -267,7 +267,7 @@
qed
qed
-text {* The sum of two subspaces is again a subspace. *}
+text \<open>The sum of two subspaces is again a subspace.\<close>
lemma sum_subspace [intro?]:
assumes "subspace U E" "vectorspace E" "subspace V E"
@@ -280,8 +280,8 @@
proof
have "0 \<in> U + V"
proof
- show "0 \<in> U" using `vectorspace E` ..
- show "0 \<in> V" using `vectorspace E` ..
+ show "0 \<in> U" using \<open>vectorspace E\<close> ..
+ show "0 \<in> V" using \<open>vectorspace E\<close> ..
show "(0::'a) = 0 + 0" by simp
qed
then show "U + V \<noteq> {}" by blast
@@ -316,22 +316,22 @@
qed
qed
-text{* The sum of two subspaces is a vectorspace. *}
+text\<open>The sum of two subspaces is a vectorspace.\<close>
lemma sum_vs [intro?]:
"U \<unlhd> E \<Longrightarrow> V \<unlhd> E \<Longrightarrow> vectorspace E \<Longrightarrow> vectorspace (U + V)"
by (rule subspace.vectorspace) (rule sum_subspace)
-subsection {* Direct sums *}
+subsection \<open>Direct sums\<close>
-text {*
+text \<open>
The sum of @{text U} and @{text V} is called \emph{direct}, iff the
zero element is the only common element of @{text U} and @{text
V}. For every element @{text x} of the direct sum of @{text U} and
@{text V} the decomposition in @{text "x = u + v"} with
@{text "u \<in> U"} and @{text "v \<in> V"} is unique.
-*}
+\<close>
lemma decomp:
assumes "vectorspace E" "subspace U E" "subspace V E"
@@ -347,9 +347,9 @@
show ?thesis
proof
have U: "vectorspace U" (* FIXME: use interpret *)
- using `subspace U E` `vectorspace E` by (rule subspace.vectorspace)
+ using \<open>subspace U E\<close> \<open>vectorspace E\<close> by (rule subspace.vectorspace)
have V: "vectorspace V"
- using `subspace V E` `vectorspace E` by (rule subspace.vectorspace)
+ using \<open>subspace V E\<close> \<open>vectorspace E\<close> by (rule subspace.vectorspace)
from u1 u2 v1 v2 and sum have eq: "u1 - u2 = v2 - v1"
by (simp add: add_diff_swap)
from u1 u2 have u: "u1 - u2 \<in> U"
@@ -374,14 +374,14 @@
qed
qed
-text {*
+text \<open>
An application of the previous lemma will be used in the proof of
the Hahn-Banach Theorem (see page \pageref{decomp-H-use}): for any
element @{text "y + a \<cdot> x\<^sub>0"} of the direct sum of a
vectorspace @{text H} and the linear closure of @{text "x\<^sub>0"}
the components @{text "y \<in> H"} and @{text a} are uniquely
determined.
-*}
+\<close>
lemma decomp_H':
assumes "vectorspace E" "subspace H E"
@@ -414,31 +414,31 @@
from x have "x \<in> H" ..
with xx' have "inverse a \<cdot> a \<cdot> x' \<in> H" by simp
with a and x' have "x' \<in> H" by (simp add: mult_assoc2)
- with `x' \<notin> H` show ?thesis by contradiction
+ with \<open>x' \<notin> H\<close> show ?thesis by contradiction
qed
then show "x \<in> {0}" ..
qed
show "{0} \<subseteq> H \<inter> lin x'"
proof -
- have "0 \<in> H" using `vectorspace E` ..
- moreover have "0 \<in> lin x'" using `x' \<in> E` ..
+ have "0 \<in> H" using \<open>vectorspace E\<close> ..
+ moreover have "0 \<in> lin x'" using \<open>x' \<in> E\<close> ..
ultimately show ?thesis by blast
qed
qed
- show "lin x' \<unlhd> E" using `x' \<in> E` ..
- qed (rule `vectorspace E`, rule `subspace H E`, rule y1, rule y2, rule eq)
+ show "lin x' \<unlhd> E" using \<open>x' \<in> E\<close> ..
+ qed (rule \<open>vectorspace E\<close>, rule \<open>subspace H E\<close>, rule y1, rule y2, rule eq)
then show "y1 = y2" ..
from c have "a1 \<cdot> x' = a2 \<cdot> x'" ..
with x' show "a1 = a2" by (simp add: mult_right_cancel)
qed
qed
-text {*
+text \<open>
Since for any element @{text "y + a \<cdot> x'"} of the direct sum of a
vectorspace @{text H} and the linear closure of @{text x'} the
components @{text "y \<in> H"} and @{text a} are unique, it follows from
@{text "y \<in> H"} that @{text "a = 0"}.
-*}
+\<close>
lemma decomp_H'_H:
assumes "vectorspace E" "subspace H E"
@@ -456,16 +456,16 @@
proof (rule decomp_H')
from ya x' show "y + a \<cdot> x' = t + 0 \<cdot> x'" by simp
from ya show "y \<in> H" ..
- qed (rule `vectorspace E`, rule `subspace H E`, rule t, (rule x')+)
+ qed (rule \<open>vectorspace E\<close>, rule \<open>subspace H E\<close>, rule t, (rule x')+)
with t x' show "(y, a) = (y + a \<cdot> x', 0)" by simp
qed
qed
-text {*
+text \<open>
The components @{text "y \<in> H"} and @{text a} in @{text "y + a \<cdot> x'"}
are unique, so the function @{text h'} defined by
@{text "h' (y + a \<cdot> x') = h y + a \<cdot> \<xi>"} is definite.
-*}
+\<close>
lemma h'_definite:
fixes H
@@ -498,7 +498,7 @@
from xq show "fst q \<in> H" ..
from xp and xq show "fst p + snd p \<cdot> x' = fst q + snd q \<cdot> x'"
by simp
- qed (rule `vectorspace E`, rule `subspace H E`, (rule x')+)
+ qed (rule \<open>vectorspace E\<close>, rule \<open>subspace H E\<close>, (rule x')+)
then show ?thesis by (cases p, cases q) simp
qed
qed
--- a/src/HOL/Hahn_Banach/Vector_Space.thy Tue Oct 21 10:53:24 2014 +0200
+++ b/src/HOL/Hahn_Banach/Vector_Space.thy Tue Oct 21 10:58:19 2014 +0200
@@ -2,19 +2,19 @@
Author: Gertrud Bauer, TU Munich
*)
-header {* Vector spaces *}
+header \<open>Vector spaces\<close>
theory Vector_Space
imports Complex_Main Bounds
begin
-subsection {* Signature *}
+subsection \<open>Signature\<close>
-text {*
+text \<open>
For the definition of real vector spaces a type @{typ 'a} of the
sort @{text "{plus, minus, zero}"} is considered, on which a real
scalar multiplication @{text \<cdot>} is declared.
-*}
+\<close>
consts
prod :: "real \<Rightarrow> 'a::{plus, minus, zero} \<Rightarrow> 'a" (infixr "'(*')" 70)
@@ -25,9 +25,9 @@
prod (infixr "\<cdot>" 70)
-subsection {* Vector space laws *}
+subsection \<open>Vector space laws\<close>
-text {*
+text \<open>
A \emph{vector space} is a non-empty set @{text V} of elements from
@{typ 'a} with the following vector space laws: The set @{text V} is
closed under addition and scalar multiplication, addition is
@@ -36,7 +36,7 @@
addition. Addition and multiplication are distributive; scalar
multiplication is associative and the real number @{text "1"} is
the neutral element of scalar multiplication.
-*}
+\<close>
locale vectorspace =
fixes V
@@ -83,8 +83,8 @@
theorems add_ac = add_assoc add_commute add_left_commute
-text {* The existence of the zero element of a vector space
- follows from the non-emptiness of carrier set. *}
+text \<open>The existence of the zero element of a vector space
+ follows from the non-emptiness of carrier set.\<close>
lemma zero [iff]: "0 \<in> V"
proof -
@@ -127,7 +127,7 @@
diff_mult_distrib1 diff_mult_distrib2
-text {* \medskip Further derived laws: *}
+text \<open>\medskip Further derived laws:\<close>
lemma mult_zero_left [simp]: "x \<in> V \<Longrightarrow> 0 \<cdot> x = 0"
proof -
@@ -236,11 +236,11 @@
proof (rule classical)
assume a: "a \<noteq> 0"
from x a have "x = (inverse a * a) \<cdot> x" by simp
- also from `x \<in> V` have "\<dots> = inverse a \<cdot> (a \<cdot> x)" by (rule mult_assoc)
+ also from \<open>x \<in> V\<close> have "\<dots> = inverse a \<cdot> (a \<cdot> x)" by (rule mult_assoc)
also from ax have "\<dots> = inverse a \<cdot> 0" by simp
also have "\<dots> = 0" by simp
finally have "x = 0" .
- with `x \<noteq> 0` show "a = 0" by contradiction
+ with \<open>x \<noteq> 0\<close> show "a = 0" by contradiction
qed
lemma mult_left_cancel:
@@ -330,7 +330,7 @@
proof -
from assms have "- c + (a + b) = - c + (c + d)"
by (simp add: add_left_cancel)
- also have "\<dots> = d" using `c \<in> V` `d \<in> V` by (rule minus_add_cancel)
+ also have "\<dots> = d" using \<open>c \<in> V\<close> \<open>d \<in> V\<close> by (rule minus_add_cancel)
finally have eq: "- c + (a + b) = d" .
from vs have "a - c = (- c + (a + b)) + - b"
by (simp add: add_ac diff_eq1)
--- a/src/HOL/Hahn_Banach/Zorn_Lemma.thy Tue Oct 21 10:53:24 2014 +0200
+++ b/src/HOL/Hahn_Banach/Zorn_Lemma.thy Tue Oct 21 10:58:19 2014 +0200
@@ -2,13 +2,13 @@
Author: Gertrud Bauer, TU Munich
*)
-header {* Zorn's Lemma *}
+header \<open>Zorn's Lemma\<close>
theory Zorn_Lemma
imports Main
begin
-text {*
+text \<open>
Zorn's Lemmas states: if every linear ordered subset of an ordered
set @{text S} has an upper bound in @{text S}, then there exists a
maximal element in @{text S}. In our application, @{text S} is a
@@ -17,7 +17,7 @@
of Zorn's lemma can be modified: if @{text S} is non-empty, it
suffices to show that for every non-empty chain @{text c} in @{text
S} the union of @{text c} also lies in @{text S}.
-*}
+\<close>
theorem Zorn's_Lemma:
assumes r: "\<And>c. c \<in> chains S \<Longrightarrow> \<exists>x. x \<in> c \<Longrightarrow> \<Union>c \<in> S"
@@ -30,14 +30,14 @@
show "\<exists>y \<in> S. \<forall>z \<in> c. z \<subseteq> y"
proof cases
- txt {* If @{text c} is an empty chain, then every element in
- @{text S} is an upper bound of @{text c}. *}
+ txt \<open>If @{text c} is an empty chain, then every element in
+ @{text S} is an upper bound of @{text c}.\<close>
assume "c = {}"
with aS show ?thesis by fast
- txt {* If @{text c} is non-empty, then @{text "\<Union>c"} is an upper
- bound of @{text c}, lying in @{text S}. *}
+ txt \<open>If @{text c} is non-empty, then @{text "\<Union>c"} is an upper
+ bound of @{text c}, lying in @{text S}.\<close>
next
assume "c \<noteq> {}"
@@ -46,7 +46,7 @@
show "\<forall>z \<in> c. z \<subseteq> \<Union>c" by fast
show "\<Union>c \<in> S"
proof (rule r)
- from `c \<noteq> {}` show "\<exists>x. x \<in> c" by fast
+ from \<open>c \<noteq> {}\<close> show "\<exists>x. x \<in> c" by fast
show "c \<in> chains S" by fact
qed
qed