--- a/NEWS Mon Nov 02 18:35:41 2015 +0100
+++ b/NEWS Mon Nov 02 20:11:16 2015 +0100
@@ -79,6 +79,9 @@
standard Isabelle fonts provide glyphs to render important control
symbols, e.g. "\<^verbatim>", "\<^emph>", "\<^bold>".
+* System option "document_symbols" determines completion of Isabelle
+symbols within document source.
+
* Antiquotation @{cartouche} in Isabelle/Pure is the same as @{text}.
Consequently, \<open>...\<close> without any decoration prints literal quasi-formal
text. Command-line tool "isabelle update_cartouches -t" helps to update
--- a/etc/options Mon Nov 02 18:35:41 2015 +0100
+++ b/etc/options Mon Nov 02 20:11:16 2015 +0100
@@ -164,3 +164,5 @@
public option completion_limit : int = 40
-- "limit for completion within the formal context"
+public option document_symbols : bool = false
+ -- "completion of Isabelle symbols within document source"
--- a/src/HOL/Hahn_Banach/Function_Norm.thy Mon Nov 02 18:35:41 2015 +0100
+++ b/src/HOL/Hahn_Banach/Function_Norm.thy Mon Nov 02 20:11:16 2015 +0100
@@ -11,14 +11,13 @@
subsection \<open>Continuous linear forms\<close>
text \<open>
- A linear form @{text f} on a normed vector space @{text "(V, \<parallel>\<cdot>\<parallel>)"}
- is \<^emph>\<open>continuous\<close>, iff it is bounded, i.e.
+ A linear form \<open>f\<close> on a normed vector space \<open>(V, \<parallel>\<cdot>\<parallel>)\<close> is \<^emph>\<open>continuous\<close>,
+ iff it is bounded, i.e.
\begin{center}
- @{text "\<exists>c \<in> R. \<forall>x \<in> V. \<bar>f x\<bar> \<le> c \<cdot> \<parallel>x\<parallel>"}
+ \<open>\<exists>c \<in> R. \<forall>x \<in> V. \<bar>f x\<bar> \<le> c \<cdot> \<parallel>x\<parallel>\<close>
\end{center}
- In our application no other functions than linear forms are
- considered, so we can define continuous linear forms as bounded
- linear forms:
+ 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 +
@@ -42,34 +41,31 @@
subsection \<open>The norm of a linear form\<close>
text \<open>
- The least real number @{text c} for which holds
+ The least real number \<open>c\<close> for which holds
\begin{center}
- @{text "\<forall>x \<in> V. \<bar>f x\<bar> \<le> c \<cdot> \<parallel>x\<parallel>"}
+ \<open>\<forall>x \<in> V. \<bar>f x\<bar> \<le> c \<cdot> \<parallel>x\<parallel>\<close>
\end{center}
- is called the \<^emph>\<open>norm\<close> of @{text f}.
+ is called the \<^emph>\<open>norm\<close> of \<open>f\<close>.
- For non-trivial vector spaces @{text "V \<noteq> {0}"} the norm can be
- defined as
+ For non-trivial vector spaces \<open>V \<noteq> {0}\<close> the norm can be defined as
\begin{center}
- @{text "\<parallel>f\<parallel> = \<sup>x \<noteq> 0. \<bar>f x\<bar> / \<parallel>x\<parallel>"}
+ \<open>\<parallel>f\<parallel> = \<sup>x \<noteq> 0. \<bar>f x\<bar> / \<parallel>x\<parallel>\<close>
\end{center}
- For the case @{text "V = {0}"} the supremum would be taken from an
- empty set. Since @{text \<real>} is unbounded, there would be no supremum.
- To avoid this situation it must be guaranteed that there is an
- element in this set. This element must be @{text "{} \<ge> 0"} so that
- @{text fn_norm} has the norm properties. Furthermore it does not
- have to change the norm in all other cases, so it must be @{text 0},
- as all other elements are @{text "{} \<ge> 0"}.
+ For the case \<open>V = {0}\<close> the supremum would be taken from an empty set.
+ Since \<open>\<real>\<close> is unbounded, there would be no supremum. To avoid this
+ situation it must be guaranteed that there is an element in this set. This
+ element must be \<open>{} \<ge> 0\<close> so that \<open>fn_norm\<close> has the norm properties.
+ Furthermore it does not have to change the norm in all other cases, so it
+ must be \<open>0\<close>, as all other elements are \<open>{} \<ge> 0\<close>.
- Thus we define the set @{text B} where the supremum is taken from as
- follows:
+ Thus we define the set \<open>B\<close> where the supremum is taken from as follows:
\begin{center}
- @{text "{0} \<union> {\<bar>f x\<bar> / \<parallel>x\<parallel>. x \<noteq> 0 \<and> x \<in> F}"}
+ \<open>{0} \<union> {\<bar>f x\<bar> / \<parallel>x\<parallel>. x \<noteq> 0 \<and> x \<in> F}\<close>
\end{center}
- @{text fn_norm} is equal to the supremum of @{text B}, if the
- supremum exists (otherwise it is undefined).
+ \<open>fn_norm\<close> is equal to the supremum of \<open>B\<close>, if the supremum exists
+ (otherwise it is undefined).
\<close>
locale fn_norm =
@@ -84,8 +80,8 @@
by (simp add: B_def)
text \<open>
- The following lemma states that every continuous linear form on a
- normed space @{text "(V, \<parallel>\<cdot>\<parallel>)"} has a function norm.
+ The following lemma states that every continuous linear form on a normed
+ space \<open>(V, \<parallel>\<cdot>\<parallel>)\<close> has a function norm.
\<close>
lemma (in normed_vectorspace_with_fn_norm) fn_norm_works:
@@ -98,19 +94,19 @@
non-empty bounded set of reals has a supremum.\<close>
have "\<exists>a. lub (B V f) a"
proof (rule real_complete)
- txt \<open>First we have to show that @{text B} is non-empty:\<close>
+ txt \<open>First we have to show that \<open>B\<close> is non-empty:\<close>
have "0 \<in> B V f" ..
then show "\<exists>x. x \<in> B V f" ..
- txt \<open>Then we have to show that @{text B} is bounded:\<close>
+ txt \<open>Then we have to show that \<open>B\<close> is bounded:\<close>
show "\<exists>c. \<forall>y \<in> B V f. y \<le> c"
proof -
- txt \<open>We know that @{text f} is bounded by some value @{text c}.\<close>
+ txt \<open>We know that \<open>f\<close> is bounded by some value \<open>c\<close>.\<close>
from bounded obtain c where c: "\<forall>x \<in> V. \<bar>f x\<bar> \<le> c * \<parallel>x\<parallel>" ..
- 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.\<close>
+ txt \<open>To prove the thesis, we have to show that there is some \<open>b\<close>, such
+ that \<open>y \<le> b\<close> for all \<open>y \<in> B\<close>. Due to the definition of \<open>B\<close> there are
+ two cases.\<close>
def b \<equiv> "max c 0"
have "\<forall>y \<in> B V f. y \<le> b"
@@ -121,8 +117,8 @@
assume "y = 0"
then show ?thesis unfolding b_def by arith
next
- 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>
+ txt \<open>The second case is \<open>y = \<bar>f x\<bar> / \<parallel>x\<parallel>\<close> for some
+ \<open>x \<in> V\<close> with \<open>x \<noteq> 0\<close>.\<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"
@@ -130,7 +126,7 @@
from x neq have gt: "0 < \<parallel>x\<parallel>" ..
txt \<open>The thesis follows by a short calculation using the
- fact that @{text f} is bounded.\<close>
+ fact that \<open>f\<close> 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>"
@@ -177,16 +173,16 @@
from this and b show ?thesis ..
qed
-text \<open>The norm of a continuous function is always @{text "\<ge> 0"}.\<close>
+text \<open>The norm of a continuous function is always \<open>\<ge> 0\<close>.\<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 \<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.\<close>
+ txt \<open>The function norm is defined as the supremum of \<open>B\<close>.
+ So it is \<open>\<ge> 0\<close> if all elements in \<open>B\<close> are \<open>\<ge>
+ 0\<close>, provided the supremum exists and \<open>B\<close> is not empty.\<close>
have "lub (B V f) (\<parallel>f\<parallel>\<hyphen>V)"
using \<open>continuous V f norm\<close> by (rule fn_norm_works)
moreover have "0 \<in> B V f" ..
@@ -197,7 +193,7 @@
\<^medskip>
The fundamental property of function norms is:
\begin{center}
- @{text "\<bar>f x\<bar> \<le> \<parallel>f\<parallel> \<cdot> \<parallel>x\<parallel>"}
+ \<open>\<bar>f x\<bar> \<le> \<parallel>f\<parallel> \<cdot> \<parallel>x\<parallel>\<close>
\end{center}
\<close>
@@ -237,10 +233,10 @@
text \<open>
\<^medskip>
- The function norm is the least positive real number for
- which the following inequation holds:
+ The function norm is the least positive real number for which the
+ following inequality holds:
\begin{center}
- @{text "\<bar>f x\<bar> \<le> c \<cdot> \<parallel>x\<parallel>"}
+ \<open>\<bar>f x\<bar> \<le> c \<cdot> \<parallel>x\<parallel>\<close>
\end{center}
\<close>
--- a/src/HOL/Hahn_Banach/Function_Order.thy Mon Nov 02 18:35:41 2015 +0100
+++ b/src/HOL/Hahn_Banach/Function_Order.thy Mon Nov 02 20:11:16 2015 +0100
@@ -11,10 +11,10 @@
subsection \<open>The graph of a function\<close>
text \<open>
- We define the \<^emph>\<open>graph\<close> of a (real) function @{text f} with
- domain @{text F} as the set
+ We define the \<^emph>\<open>graph\<close> of a (real) function \<open>f\<close> with
+ domain \<open>F\<close> as the set
\begin{center}
- @{text "{(x, f x). x \<in> F}"}
+ \<open>{(x, f x). x \<in> F}\<close>
\end{center}
So we are modeling partial functions by specifying the domain and
the mapping function. We use the term ``function'' also for its
@@ -41,8 +41,8 @@
subsection \<open>Functions ordered by domain extension\<close>
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'}.
+ A function \<open>h'\<close> is an extension of \<open>h\<close>, iff the graph of
+ \<open>h\<close> is a subset of the graph of \<open>h'\<close>.
\<close>
lemma graph_extI:
@@ -60,8 +60,7 @@
subsection \<open>Domain and function of a graph\<close>
text \<open>
- The inverse functions to @{text graph} are @{text domain} and @{text
- funct}.
+ The inverse functions to \<open>graph\<close> are \<open>domain\<close> and \<open>funct\<close>.
\<close>
definition domain :: "'a graph \<Rightarrow> 'a set"
@@ -71,8 +70,8 @@
where "funct g = (\<lambda>x. (SOME y. (x, y) \<in> g))"
text \<open>
- The following lemma states that @{text g} is the graph of a function
- if the relation induced by @{text g} is unique.
+ The following lemma states that \<open>g\<close> is the graph of a function if the
+ relation induced by \<open>g\<close> is unique.
\<close>
lemma graph_domain_funct:
@@ -94,10 +93,9 @@
subsection \<open>Norm-preserving extensions of a function\<close>
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.
+ Given a linear form \<open>f\<close> on the space \<open>F\<close> and a seminorm \<open>p\<close> on \<open>E\<close>. The
+ set of all linear extensions of \<open>f\<close>, to superspaces \<open>H\<close> of \<open>F\<close>, which are
+ bounded by \<open>p\<close>, is defined as follows.
\<close>
definition
--- a/src/HOL/Hahn_Banach/Hahn_Banach.thy Mon Nov 02 18:35:41 2015 +0100
+++ b/src/HOL/Hahn_Banach/Hahn_Banach.thy Mon Nov 02 20:11:16 2015 +0100
@@ -9,42 +9,39 @@
begin
text \<open>
- We present the proof of two different versions of the Hahn-Banach
- Theorem, closely following @{cite \<open>\S36\<close> "Heuser:1986"}.
+ We present the proof of two different versions of the Hahn-Banach Theorem,
+ closely following @{cite \<open>\S36\<close> "Heuser:1986"}.
\<close>
+
subsection \<open>The Hahn-Banach Theorem for vector spaces\<close>
paragraph \<open>Hahn-Banach Theorem.\<close>
text \<open>
- 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 f} is bounded by @{text p}, i.e. @{text "\<forall>x \<in>
- F. f x \<le> p x"}. Then @{text f} can be extended to a linear form @{text h}
- on @{text E} such that @{text h} is norm-preserving, i.e. @{text h} is
- also bounded by @{text p}.
+ Let \<open>F\<close> be a subspace of a real vector space \<open>E\<close>, let \<open>p\<close> be a semi-norm
+ on \<open>E\<close>, and \<open>f\<close> be a linear form defined on \<open>F\<close> such that \<open>f\<close> is bounded
+ by \<open>p\<close>, i.e. \<open>\<forall>x \<in> F. f x \<le> p x\<close>. Then \<open>f\<close> can be extended to a linear
+ form \<open>h\<close> on \<open>E\<close> such that \<open>h\<close> is norm-preserving, i.e. \<open>h\<close> is also bounded
+ by \<open>p\<close>.
\<close>
paragraph \<open>Proof Sketch.\<close>
text \<open>
- \<^enum> Define @{text M} as the set of norm-preserving extensions of
- @{text f} to subspaces of @{text E}. The linear forms in @{text M}
- are ordered by domain extension.
+ \<^enum> Define \<open>M\<close> as the set of norm-preserving extensions of \<open>f\<close> to subspaces
+ of \<open>E\<close>. The linear forms in \<open>M\<close> are ordered by domain extension.
- \<^enum> We show that every non-empty chain in @{text M} has an upper
- bound in @{text M}.
+ \<^enum> We show that every non-empty chain in \<open>M\<close> has an upper bound in \<open>M\<close>.
+
+ \<^enum> With Zorn's Lemma we conclude that there is a maximal function \<open>g\<close> in
+ \<open>M\<close>.
- \<^enum> With Zorn's Lemma we conclude that there is a maximal function
- @{text g} in @{text M}.
-
- \<^enum> The domain @{text H} of @{text g} is the whole space @{text
- E}, as shown by classical contradiction:
+ \<^enum> The domain \<open>H\<close> of \<open>g\<close> is the whole space \<open>E\<close>, as shown by classical
+ contradiction:
- \<^item> Assuming @{text g} is not defined on whole @{text E}, it can
- still be extended in a norm-preserving way to a super-space @{text
- H'} of @{text H}.
+ \<^item> Assuming \<open>g\<close> is not defined on whole \<open>E\<close>, it can still be extended in
+ a norm-preserving way to a super-space \<open>H'\<close> of \<open>H\<close>.
- \<^item> Thus @{text g} can not be maximal. Contradiction!
+ \<^item> Thus \<open>g\<close> can not be maximal. Contradiction!
\<close>
theorem Hahn_Banach:
@@ -52,9 +49,9 @@
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)"
- -- \<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. \<^smallskip>\<close>
+ -- \<open>Let \<open>E\<close> be a vector space, \<open>F\<close> a subspace of \<open>E\<close>, \<open>p\<close> a seminorm on \<open>E\<close>,\<close>
+ -- \<open>and \<open>f\<close> a linear form on \<open>F\<close> such that \<open>f\<close> is bounded by \<open>p\<close>,\<close>
+ -- \<open>then \<open>f\<close> can be extended to a linear form \<open>h\<close> on \<open>E\<close> in a norm-preserving way. \<^smallskip>\<close>
proof -
interpret vectorspace E by fact
interpret subspace F E by fact
@@ -67,8 +64,8 @@
{
fix c assume cM: "c \<in> chains M" and ex: "\<exists>x. x \<in> c"
have "\<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>
+ -- \<open>Show that every non-empty chain \<open>c\<close> of \<open>M\<close> has an upper bound in \<open>M\<close>:\<close>
+ -- \<open>\<open>\<Union>c\<close> is greater than any element of the chain \<open>c\<close>, so it suffices to show \<open>\<Union>c \<in> M\<close>.\<close>
unfolding M_def
proof (rule norm_pres_extensionI)
let ?H = "domain (\<Union>c)"
@@ -98,9 +95,9 @@
qed
}
then have "\<exists>g \<in> M. \<forall>x \<in> M. g \<subseteq> x \<longrightarrow> x = g"
- -- \<open>With Zorn's Lemma we can conclude that there is a maximal element in @{text M}. \<^smallskip>\<close>
+ -- \<open>With Zorn's Lemma we can conclude that there is a maximal element in \<open>M\<close>. \<^smallskip>\<close>
proof (rule Zorn's_Lemma)
- -- \<open>We show that @{text M} is non-empty:\<close>
+ -- \<open>We show that \<open>M\<close> is non-empty:\<close>
show "graph F f \<in> M"
unfolding M_def
proof (rule norm_pres_extensionI2)
@@ -119,18 +116,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 ..
- -- \<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}. \<^smallskip>\<close>
+ -- \<open>\<open>g\<close> is a norm-preserving extension of \<open>f\<close>, in other words:\<close>
+ -- \<open>\<open>g\<close> is the graph of some linear form \<open>h\<close> defined on a subspace \<open>H\<close> of \<open>E\<close>,\<close>
+ -- \<open>and \<open>h\<close> is an extension of \<open>f\<close> that is again bounded by \<open>p\<close>. \<^smallskip>\<close>
from HE E have H: "vectorspace H"
by (rule subspace.vectorspace)
have HE_eq: "H = E"
- -- \<open>We show that @{text h} is defined on whole @{text E} by classical contradiction. \<^smallskip>\<close>
+ -- \<open>We show that \<open>h\<close> is defined on whole \<open>E\<close> by classical contradiction. \<^smallskip>\<close>
proof (rule classical)
assume neq: "H \<noteq> E"
- -- \<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'}. \<^smallskip>\<close>
+ -- \<open>Assume \<open>h\<close> is not defined on whole \<open>E\<close>. Then show that \<open>h\<close> can be extended\<close>
+ -- \<open>in a norm-preserving way to a function \<open>h'\<close> with the graph \<open>g'\<close>. \<^smallskip>\<close>
have "\<exists>g' \<in> M. g \<subseteq> g' \<and> g \<noteq> g'"
proof -
from HE have "H \<subseteq> E" ..
@@ -146,7 +143,7 @@
qed
def H' \<equiv> "H + lin x'"
- -- \<open>Define @{text H'} as the direct sum of @{text H} and the linear closure of @{text x'}. \<^smallskip>\<close>
+ -- \<open>Define \<open>H'\<close> as the direct sum of \<open>H\<close> and the linear closure of \<open>x'\<close>. \<^smallskip>\<close>
have HH': "H \<unlhd> H'"
proof (unfold H'_def)
from x'E have "vectorspace (lin x')" ..
@@ -156,8 +153,8 @@
obtain xi where
xi: "\<forall>y \<in> H. - p (y + x') - h y \<le> xi
\<and> xi \<le> p (y + x') - h y"
- -- \<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}.
+ -- \<open>Pick a real number \<open>\<xi>\<close> that fulfills certain inequality; this will\<close>
+ -- \<open>be used to establish that \<open>h'\<close> is a norm-preserving extension of \<open>h\<close>.
\label{ex-xi-use}\<^smallskip>\<close>
proof -
from H have "\<exists>xi. \<forall>y \<in> H. - p (y + x') - h y \<le> xi
@@ -185,10 +182,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"
- -- \<open>Define the extension @{text h'} of @{text h} to @{text H'} using @{text \<xi>}. \<^smallskip>\<close>
+ -- \<open>Define the extension \<open>h'\<close> of \<open>h\<close> to \<open>H'\<close> using \<open>\<xi>\<close>. \<^smallskip>\<close>
have "g \<subseteq> graph H' h' \<and> g \<noteq> graph H' h'"
- -- \<open>@{text h'} is an extension of @{text h} \dots \<^smallskip>\<close>
+ -- \<open>\<open>h'\<close> is an extension of \<open>h\<close> \dots \<^smallskip>\<close>
proof
show "g \<subseteq> graph H' h'"
proof -
@@ -225,7 +222,7 @@
qed
qed
moreover have "graph H' h' \<in> M"
- -- \<open>and @{text h'} is norm-preserving. \<^smallskip>\<close>
+ -- \<open>and \<open>h'\<close> is norm-preserving. \<^smallskip>\<close>
proof (unfold M_def)
show "graph H' h' \<in> norm_pres_extensions E p F f"
proof (rule norm_pres_extensionI2)
@@ -273,7 +270,7 @@
ultimately show ?thesis ..
qed
then have "\<not> (\<forall>x \<in> M. g \<subseteq> x \<longrightarrow> g = x)" by simp
- -- \<open>So the graph @{text g} of @{text h} cannot be maximal. Contradiction! \<^smallskip>\<close>
+ -- \<open>So the graph \<open>g\<close> of \<open>h\<close> cannot be maximal. Contradiction! \<^smallskip>\<close>
with gx show "H = E" by contradiction
qed
@@ -295,14 +292,14 @@
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
- are equivalent:\footnote{This was shown in lemma @{thm [source]
- abs_ineq_iff} (see page \pageref{abs-ineq-iff}).}
+ Theorem\label{abs-Hahn-Banach} uses the fact that for a real linear form
+ \<open>f\<close> and a seminorm \<open>p\<close> the following inequality are
+ equivalent:\footnote{This was shown in lemma @{thm [source] abs_ineq_iff}
+ (see page \pageref{abs-ineq-iff}).}
\begin{center}
\begin{tabular}{lll}
- @{text "\<forall>x \<in> H. \<bar>h x\<bar> \<le> p x"} & and &
- @{text "\<forall>x \<in> H. h x \<le> p x"} \\
+ \<open>\<forall>x \<in> H. \<bar>h x\<bar> \<le> p x\<close> & and &
+ \<open>\<forall>x \<in> H. h x \<le> p x\<close> \\
\end{tabular}
\end{center}
\<close>
@@ -339,9 +336,9 @@
subsection \<open>The Hahn-Banach Theorem for normed spaces\<close>
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>"}.
+ Every continuous linear form \<open>f\<close> on a subspace \<open>F\<close> of a norm space \<open>E\<close>,
+ can be extended to a continuous linear form \<open>g\<close> on \<open>E\<close> such that \<open>\<parallel>f\<parallel> =
+ \<parallel>g\<parallel>\<close>.
\<close>
theorem norm_Hahn_Banach:
@@ -370,22 +367,22 @@
by (rule normed_vectorspace_with_fn_norm.fn_norm_ge_zero
[OF normed_vectorspace_with_fn_norm.intro,
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>
+ txt \<open>We define a function \<open>p\<close> on \<open>E\<close> as follows:
+ \<open>p x = \<parallel>f\<parallel> \<cdot> \<parallel>x\<parallel>\<close>\<close>
def p \<equiv> "\<lambda>x. \<parallel>f\<parallel>\<hyphen>F * \<parallel>x\<parallel>"
- txt \<open>@{text p} is a seminorm on @{text E}:\<close>
+ txt \<open>\<open>p\<close> is a seminorm on \<open>E\<close>:\<close>
have q: "seminorm E p"
proof
fix x y a assume x: "x \<in> E" and y: "y \<in> E"
- txt \<open>@{text p} is positive definite:\<close>
+ txt \<open>\<open>p\<close> 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 \<open>@{text p} is absolutely homogeneous:\<close>
+ txt \<open>\<open>p\<close> is absolutely homogeneous:\<close>
show "p (a \<cdot> x) = \<bar>a\<bar> * p x"
proof -
@@ -396,7 +393,7 @@
finally show ?thesis .
qed
- txt \<open>Furthermore, @{text p} is subadditive:\<close>
+ txt \<open>Furthermore, \<open>p\<close> is subadditive:\<close>
show "p (x + y) \<le> p x + p y"
proof -
@@ -411,7 +408,7 @@
qed
qed
- txt \<open>@{text f} is bounded by @{text p}.\<close>
+ txt \<open>\<open>f\<close> is bounded by \<open>p\<close>.\<close>
have "\<forall>x \<in> F. \<bar>f x\<bar> \<le> p x"
proof
@@ -423,10 +420,10 @@
OF F_norm, folded B_def fn_norm_def])
qed
- 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}.\<close>
+ txt \<open>Using the fact that \<open>p\<close> is a seminorm and \<open>f\<close> is bounded by \<open>p\<close> we
+ can apply the Hahn-Banach Theorem for real vector spaces. So \<open>f\<close> can be
+ extended in a norm-preserving way to some function \<open>g\<close> on the whole
+ vector space \<open>E\<close>.\<close>
with E FE linearform q obtain g where
linearformE: "linearform E g"
@@ -434,7 +431,7 @@
and b: "\<forall>x \<in> E. \<bar>g x\<bar> \<le> p x"
by (rule abs_Hahn_Banach [elim_format]) iprover
- txt \<open>We furthermore have to show that @{text g} is also continuous:\<close>
+ txt \<open>We furthermore have to show that \<open>g\<close> is also continuous:\<close>
have g_cont: "continuous E g norm" using linearformE
proof
@@ -443,25 +440,25 @@
by (simp only: p_def)
qed
- txt \<open>To complete the proof, we show that @{text "\<parallel>g\<parallel> = \<parallel>f\<parallel>"}.\<close>
+ txt \<open>To complete the proof, we show that \<open>\<parallel>g\<parallel> = \<parallel>f\<parallel>\<close>.\<close>
have "\<parallel>g\<parallel>\<hyphen>E = \<parallel>f\<parallel>\<hyphen>F"
proof (rule order_antisym)
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
+ First we show \<open>\<parallel>g\<parallel> \<le> \<parallel>f\<parallel>\<close>. The function norm \<open>\<parallel>g\<parallel>\<close> is defined as the
+ smallest \<open>c \<in> \<real>\<close> such that
\begin{center}
\begin{tabular}{l}
- @{text "\<forall>x \<in> E. \<bar>g x\<bar> \<le> c \<cdot> \<parallel>x\<parallel>"}
+ \<open>\<forall>x \<in> E. \<bar>g x\<bar> \<le> c \<cdot> \<parallel>x\<parallel>\<close>
\end{tabular}
\end{center}
- \noindent Furthermore holds
+ \<^noindent> Furthermore holds
\begin{center}
\begin{tabular}{l}
- @{text "\<forall>x \<in> E. \<bar>g x\<bar> \<le> \<parallel>f\<parallel> \<cdot> \<parallel>x\<parallel>"}
+ \<open>\<forall>x \<in> E. \<bar>g x\<bar> \<le> \<parallel>f\<parallel> \<cdot> \<parallel>x\<parallel>\<close>
\end{tabular}
\end{center}
-\<close>
+ \<close>
from g_cont _ ge_zero
show "\<parallel>g\<parallel>\<hyphen>E \<le> \<parallel>f\<parallel>\<hyphen>F"
--- a/src/HOL/Hahn_Banach/Hahn_Banach_Ext_Lemmas.thy Mon Nov 02 18:35:41 2015 +0100
+++ b/src/HOL/Hahn_Banach/Hahn_Banach_Ext_Lemmas.thy Mon Nov 02 20:11:16 2015 +0100
@@ -9,34 +9,30 @@
begin
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
- @{text F}. We consider a subspace @{text H} of @{text E} that is a
- superspace of @{text F} and a linear form @{text h} on @{text
- H}. @{text H} is a not equal to @{text E} and @{text "x\<^sub>0"} is
- an element in @{text "E - H"}. @{text H} is extended to the direct
- sum @{text "H' = H + lin x\<^sub>0"}, so for any @{text "x \<in> H'"}
- the decomposition of @{text "x = y + a \<cdot> x"} with @{text "y \<in> H"} is
- unique. @{text h'} is defined on @{text H'} by @{text "h' x = h y +
- a \<cdot> \<xi>"} for a certain @{text \<xi>}.
+ In this section the following context is presumed. Let \<open>E\<close> be a real
+ vector space with a seminorm \<open>q\<close> on \<open>E\<close>. \<open>F\<close> is a subspace of \<open>E\<close> and \<open>f\<close>
+ a linear function on \<open>F\<close>. We consider a subspace \<open>H\<close> of \<open>E\<close> that is a
+ superspace of \<open>F\<close> and a linear form \<open>h\<close> on \<open>H\<close>. \<open>H\<close> is a not equal to \<open>E\<close>
+ and \<open>x\<^sub>0\<close> is an element in \<open>E - H\<close>. \<open>H\<close> is extended to the direct sum \<open>H'
+ = H + lin x\<^sub>0\<close>, so for any \<open>x \<in> H'\<close> the decomposition of \<open>x = y + a \<cdot> x\<close>
+ with \<open>y \<in> H\<close> is unique. \<open>h'\<close> is defined on \<open>H'\<close> by \<open>h' x = h y + a \<cdot> \<xi>\<close>
+ for a certain \<open>\<xi>\<close>.
- Subsequently we show some properties of this extension @{text h'} of
- @{text h}.
+ Subsequently we show some properties of this extension \<open>h'\<close> of \<open>h\<close>.
\<^medskip>
- This lemma will be used to show the existence of a linear
- extension of @{text f} (see page \pageref{ex-xi-use}). It is a
- consequence of the completeness of @{text \<real>}. To show
+ This lemma will be used to show the existence of a linear extension of \<open>f\<close>
+ (see page \pageref{ex-xi-use}). It is a consequence of the completeness of
+ \<open>\<real>\<close>. To show
\begin{center}
\begin{tabular}{l}
- @{text "\<exists>\<xi>. \<forall>y \<in> F. a y \<le> \<xi> \<and> \<xi> \<le> b y"}
+ \<open>\<exists>\<xi>. \<forall>y \<in> F. a y \<le> \<xi> \<and> \<xi> \<le> b y\<close>
\end{tabular}
\end{center}
- \noindent it suffices to show that
+ \<^noindent> it suffices to show that
\begin{center}
\begin{tabular}{l}
- @{text "\<forall>u \<in> F. \<forall>v \<in> F. a u \<le> b v"}
+ \<open>\<forall>u \<in> F. \<forall>v \<in> F. a u \<le> b v\<close>
\end{tabular}
\end{center}
\<close>
@@ -48,7 +44,7 @@
proof -
interpret vectorspace F by fact
txt \<open>From the completeness of the reals follows:
- The set @{text "S = {a u. u \<in> F}"} has a supremum, if it is
+ The set \<open>S = {a u. u \<in> F}\<close> has a supremum, if it is
non-empty and has an upper bound.\<close>
let ?S = "{a u | u. u \<in> F}"
@@ -86,9 +82,8 @@
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'}.
+ The function \<open>h'\<close> is defined as a \<open>h' x = h y + a \<cdot> \<xi>\<close> where
+ \<open>x = y + a \<cdot> \<xi>\<close> is a linear extension of \<open>h\<close> to \<open>H'\<close>.
\<close>
lemma h'_lf:
@@ -194,8 +189,8 @@
text \<open>
\<^medskip>
- The linear extension @{text h'} of @{text h}
- is bounded by the seminorm @{text p}.\<close>
+ The linear extension \<open>h'\<close> of \<open>h\<close> is bounded by the seminorm \<open>p\<close>.
+\<close>
lemma h'_norm_pres:
assumes h'_def: "h' \<equiv> \<lambda>x. let (y, a) =
@@ -235,8 +230,8 @@
also from x0 y' z have "p y = p (y + a \<cdot> x0)" by simp
finally show ?thesis .
next
- txt \<open>In the case @{text "a < 0"}, we use @{text "a\<^sub>1"}
- with @{text ya} taken as @{text "y / a"}:\<close>
+ txt \<open>In the case \<open>a < 0\<close>, we use \<open>a\<^sub>1\<close>
+ with \<open>ya\<close> taken as \<open>y / a\<close>:\<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" ..
@@ -257,8 +252,8 @@
finally have "a * xi \<le> p (y + a \<cdot> x0) - h y" .
then show ?thesis by simp
next
- txt \<open>In the case @{text "a > 0"}, we use @{text "a\<^sub>2"}
- with @{text ya} taken as @{text "y / a"}:\<close>
+ txt \<open>In the case \<open>a > 0\<close>, we use \<open>a\<^sub>2\<close>
+ with \<open>ya\<close> taken as \<open>y / a\<close>:\<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 Mon Nov 02 18:35:41 2015 +0100
+++ b/src/HOL/Hahn_Banach/Hahn_Banach_Sup_Lemmas.thy Mon Nov 02 20:11:16 2015 +0100
@@ -2,27 +2,25 @@
Author: Gertrud Bauer, TU Munich
*)
-section \<open>The supremum w.r.t.~the function order\<close>
+section \<open>The supremum wrt.\ the function order\<close>
theory Hahn_Banach_Sup_Lemmas
imports Function_Norm Zorn_Lemma
begin
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
- @{text p} on @{text E}. @{text F} is a subspace of @{text E} and
- @{text f} a linear form on @{text F}. We consider a chain @{text c}
- of norm-preserving extensions of @{text f}, such that @{text "\<Union>c =
- graph H h"}. We will show some properties about the limit function
- @{text h}, i.e.\ the supremum of the chain @{text c}.
+ 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 \<open>E\<close> be a real vector space with a seminorm \<open>p\<close> on \<open>E\<close>. \<open>F\<close> is a
+ subspace of \<open>E\<close> and \<open>f\<close> a linear form on \<open>F\<close>. We consider a chain \<open>c\<close> of
+ norm-preserving extensions of \<open>f\<close>, such that \<open>\<Union>c = graph H h\<close>. We will
+ show some properties about the limit function \<open>h\<close>, i.e.\ the supremum of
+ the chain \<open>c\<close>.
\<^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 @{text H} is member of one of the
- elements of the chain.
+ Let \<open>c\<close> be a chain of norm-preserving extensions of the function \<open>f\<close> and
+ let \<open>graph H h\<close> be the supremum of \<open>c\<close>. Every element in \<open>H\<close> is member of
+ one of the elements of the chain.
\<close>
lemmas [dest?] = chainsD
@@ -57,11 +55,10 @@
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'}.
+ Let \<open>c\<close> be a chain of norm-preserving extensions of the function \<open>f\<close> and
+ let \<open>graph H h\<close> be the supremum of \<open>c\<close>. Every element in the domain \<open>H\<close> of
+ the supremum function is member of the domain \<open>H'\<close> of some function \<open>h'\<close>,
+ such that \<open>h\<close> extends \<open>h'\<close>.
\<close>
lemma some_H'h':
@@ -86,10 +83,9 @@
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'}.
+ Any two elements \<open>x\<close> and \<open>y\<close> in the domain \<open>H\<close> of the supremum function
+ \<open>h\<close> are both in the domain \<open>H'\<close> of some function \<open>h'\<close>, such that \<open>h\<close>
+ extends \<open>h'\<close>.
\<close>
lemma some_H'h'2:
@@ -103,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 \<open>@{text y} is in the domain @{text H''} of some function @{text h''},
- such that @{text h} extends @{text h''}.\<close>
+ txt \<open>\<open>y\<close> is in the domain \<open>H''\<close> of some function \<open>h''\<close>,
+ such that \<open>h\<close> extends \<open>h''\<close>.\<close>
from M cM u and y obtain H' h' where
y_hy: "(y, h y) \<in> graph H' h'"
@@ -114,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 \<open>@{text x} is in the domain @{text H'} of some function @{text h'},
- such that @{text h} extends @{text h'}.\<close>
+ txt \<open>\<open>x\<close> is in the domain \<open>H'\<close> of some function \<open>h'\<close>,
+ such that \<open>h\<close> extends \<open>h'\<close>.\<close>
from M cM u and x obtain H'' h'' where
x_hx: "(x, h x) \<in> graph H'' h''"
@@ -125,9 +121,9 @@
"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 \<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
+ txt \<open>Since both \<open>h'\<close> and \<open>h''\<close> are elements of the chain,
+ \<open>h''\<close> is an extension of \<open>h'\<close> or vice versa. Thus both
+ \<open>x\<close> and \<open>y\<close> are contained in the greater
one. \label{cases1}\<close>
from cM c'' c' consider "graph H'' h'' \<subseteq> graph H' h'" | "graph H' h' \<subseteq> graph H'' h''"
@@ -159,8 +155,8 @@
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.
+ The relation induced by the graph of the supremum of a chain \<open>c\<close> is
+ definite, i.e.\ it is the graph of a function.
\<close>
lemma sup_definite:
@@ -182,9 +178,8 @@
then obtain H2 h2 where G2_rep: "G2 = graph H2 h2"
unfolding M_def by blast
- 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}\<close>
+ txt \<open>\<open>G\<^sub>1\<close> is contained in \<open>G\<^sub>2\<close> or vice versa, since both \<open>G\<^sub>1\<close> and \<open>G\<^sub>2\<close>
+ are members of \<open>c\<close>. \label{cases2}\<close>
from cM G1 G2 consider "G1 \<subseteq> G2" | "G2 \<subseteq> G1"
by (blast dest: chainsD)
@@ -210,12 +205,11 @@
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}.
+ The limit function \<open>h\<close> is linear. Every element \<open>x\<close> in the domain of \<open>h\<close>
+ is in the domain of a function \<open>h'\<close> in the chain of norm preserving
+ extensions. Furthermore, \<open>h\<close> is an extension of \<open>h'\<close> so the function
+ values of \<open>x\<close> are identical for \<open>h'\<close> and \<open>h\<close>. Finally, the function \<open>h'\<close>
+ is linear by construction of \<open>M\<close>.
\<close>
lemma sup_lf:
@@ -266,10 +260,9 @@
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.
+ The limit of a non-empty chain of norm preserving extensions of \<open>f\<close> is an
+ extension of \<open>f\<close>, since every element of the chain is an extension of \<open>f\<close>
+ and the supremum is an extension for every element of the chain.
\<close>
lemma sup_ext:
@@ -293,10 +286,9 @@
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.
+ The domain \<open>H\<close> of the limit function is a superspace of \<open>F\<close>, since \<open>F\<close> is
+ a subset of \<open>H\<close>. The existence of the \<open>0\<close> element in \<open>F\<close> and the closure
+ properties follow from the fact that \<open>F\<close> is a vector space.
\<close>
lemma sup_supF:
@@ -319,8 +311,7 @@
text \<open>
\<^medskip>
- The domain @{text H} of the limit function is a subspace of
- @{text E}.
+ The domain \<open>H\<close> of the limit function is a subspace of \<open>E\<close>.
\<close>
lemma sup_subE:
@@ -376,8 +367,8 @@
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}.
+ The limit function is bounded by the norm \<open>p\<close> as well, since all elements
+ in the chain are bounded by \<open>p\<close>.
\<close>
lemma sup_norm_pres:
@@ -398,14 +389,14 @@
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
- vector spaces the following inequations are equivalent:
+ The following lemma is a property of linear forms on real vector spaces.
+ It will be used for the lemma \<open>abs_Hahn_Banach\<close> (see page
+ \pageref{abs-Hahn-Banach}). \label{abs-ineq-iff} For real vector spaces
+ the following inequality are equivalent:
\begin{center}
\begin{tabular}{lll}
- @{text "\<forall>x \<in> H. \<bar>h x\<bar> \<le> p x"} & and &
- @{text "\<forall>x \<in> H. h x \<le> p x"} \\
+ \<open>\<forall>x \<in> H. \<bar>h x\<bar> \<le> p x\<close> & and &
+ \<open>\<forall>x \<in> H. h x \<le> p x\<close> \\
\end{tabular}
\end{center}
\<close>
--- a/src/HOL/Hahn_Banach/Linearform.thy Mon Nov 02 18:35:41 2015 +0100
+++ b/src/HOL/Hahn_Banach/Linearform.thy Mon Nov 02 20:11:16 2015 +0100
@@ -9,8 +9,8 @@
begin
text \<open>
- A \<^emph>\<open>linear form\<close> is a function on a vector space into the reals
- that is additive and multiplicative.
+ A \<^emph>\<open>linear form\<close> is a function on a vector space into the reals that is
+ additive and multiplicative.
\<close>
locale linearform =
@@ -44,7 +44,7 @@
finally show ?thesis by simp
qed
-text \<open>Every linear form yields @{text 0} for the @{text 0} vector.\<close>
+text \<open>Every linear form yields \<open>0\<close> for the \<open>0\<close> vector.\<close>
lemma (in linearform) zero [iff]:
assumes "vectorspace V"
--- a/src/HOL/Hahn_Banach/Normed_Space.thy Mon Nov 02 18:35:41 2015 +0100
+++ b/src/HOL/Hahn_Banach/Normed_Space.thy Mon Nov 02 20:11:16 2015 +0100
@@ -11,9 +11,9 @@
subsection \<open>Quasinorms\<close>
text \<open>
- A \<^emph>\<open>seminorm\<close> @{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.
+ A \<^emph>\<open>seminorm\<close> \<open>\<parallel>\<cdot>\<parallel>\<close> 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 =
@@ -57,8 +57,8 @@
subsection \<open>Norms\<close>
text \<open>
- A \<^emph>\<open>norm\<close> @{text "\<parallel>\<cdot>\<parallel>"} is a seminorm that maps only the
- @{text 0} vector to @{text 0}.
+ A \<^emph>\<open>norm\<close> \<open>\<parallel>\<cdot>\<parallel>\<close> is a seminorm that maps only the
+ \<open>0\<close> vector to \<open>0\<close>.
\<close>
locale norm = seminorm +
--- a/src/HOL/Hahn_Banach/Subspace.thy Mon Nov 02 18:35:41 2015 +0100
+++ b/src/HOL/Hahn_Banach/Subspace.thy Mon Nov 02 20:11:16 2015 +0100
@@ -11,9 +11,8 @@
subsection \<open>Definition\<close>
text \<open>
- A non-empty subset @{text U} of a vector space @{text V} is a
- \<^emph>\<open>subspace\<close> of @{text V}, iff @{text U} is closed under addition
- and scalar multiplication.
+ A non-empty subset \<open>U\<close> of a vector space \<open>V\<close> is a \<^emph>\<open>subspace\<close> of \<open>V\<close>, iff
+ \<open>U\<close> is closed under addition and scalar multiplication.
\<close>
locale subspace =
@@ -51,9 +50,9 @@
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.
+ 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]:
@@ -140,8 +139,8 @@
subsection \<open>Linear closure\<close>
text \<open>
- The \<^emph>\<open>linear closure\<close> of a vector @{text x} is the set of all
- scalar multiples of @{text x}.
+ The \<^emph>\<open>linear closure\<close> of a vector \<open>x\<close> is the set of all scalar multiples
+ of \<open>x\<close>.
\<close>
definition lin :: "('a::{minus,plus,zero}) \<Rightarrow> 'a set"
@@ -227,8 +226,8 @@
subsection \<open>Sum of two vectorspaces\<close>
text \<open>
- The \<^emph>\<open>sum\<close> of two vectorspaces @{text U} and @{text V} is the
- set of all sums of elements from @{text U} and @{text V}.
+ The \<^emph>\<open>sum\<close> of two vectorspaces \<open>U\<close> and \<open>V\<close> is the set of all sums of
+ elements from \<open>U\<close> and \<open>V\<close>.
\<close>
lemma sum_def: "U + V = {u + v | u v. u \<in> U \<and> v \<in> V}"
@@ -246,7 +245,7 @@
"u \<in> U \<Longrightarrow> v \<in> V \<Longrightarrow> u + v \<in> U + V"
unfolding sum_def by blast
-text \<open>@{text U} is a subspace of @{text "U + V"}.\<close>
+text \<open>\<open>U\<close> is a subspace of \<open>U + V\<close>.\<close>
lemma subspace_sum1 [iff]:
assumes "vectorspace U" "vectorspace V"
@@ -329,11 +328,10 @@
subsection \<open>Direct sums\<close>
text \<open>
- The sum of @{text U} and @{text V} is called \<^emph>\<open>direct\<close>, 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.
+ The sum of \<open>U\<close> and \<open>V\<close> is called \<^emph>\<open>direct\<close>, iff the zero element is the
+ only common element of \<open>U\<close> and \<open>V\<close>. For every element \<open>x\<close> of the direct
+ sum of \<open>U\<close> and \<open>V\<close> the decomposition in \<open>x = u + v\<close> with \<open>u \<in> U\<close> and
+ \<open>v \<in> V\<close> is unique.
\<close>
lemma decomp:
@@ -378,12 +376,10 @@
qed
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.
+ 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
+ \<open>y + a \<cdot> x\<^sub>0\<close> of the direct sum of a vectorspace \<open>H\<close> and the linear closure
+ of \<open>x\<^sub>0\<close> the components \<open>y \<in> H\<close> and \<open>a\<close> are uniquely determined.
\<close>
lemma decomp_H':
@@ -437,10 +433,9 @@
qed
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"}.
+ Since for any element \<open>y + a \<cdot> x'\<close> of the direct sum of a vectorspace \<open>H\<close>
+ and the linear closure of \<open>x'\<close> the components \<open>y \<in> H\<close> and \<open>a\<close> are unique,
+ it follows from \<open>y \<in> H\<close> that \<open>a = 0\<close>.
\<close>
lemma decomp_H'_H:
@@ -465,9 +460,8 @@
qed
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.
+ The components \<open>y \<in> H\<close> and \<open>a\<close> in \<open>y + a \<cdot> x'\<close> are unique, so the function
+ \<open>h'\<close> defined by \<open>h' (y + a \<cdot> x') = h y + a \<cdot> \<xi>\<close> is definite.
\<close>
lemma h'_definite:
--- a/src/HOL/Hahn_Banach/Vector_Space.thy Mon Nov 02 18:35:41 2015 +0100
+++ b/src/HOL/Hahn_Banach/Vector_Space.thy Mon Nov 02 20:11:16 2015 +0100
@@ -11,9 +11,9 @@
subsection \<open>Signature\<close>
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.
+ For the definition of real vector spaces a type @{typ 'a} of the sort
+ \<open>{plus, minus, zero}\<close> is considered, on which a real scalar multiplication
+ \<open>\<cdot>\<close> is declared.
\<close>
consts
@@ -23,14 +23,13 @@
subsection \<open>Vector space laws\<close>
text \<open>
- A \<^emph>\<open>vector space\<close> 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
- associative and commutative; @{text "- x"} is the inverse of @{text
- x} w.~r.~t.~addition and @{text 0} is the neutral element of
- addition. Addition and multiplication are distributive; scalar
- multiplication is associative and the real number @{text "1"} is
- the neutral element of scalar multiplication.
+ A \<^emph>\<open>vector space\<close> is a non-empty set \<open>V\<close> of elements from @{typ 'a} with
+ the following vector space laws: The set \<open>V\<close> is closed under addition and
+ scalar multiplication, addition is associative and commutative; \<open>- x\<close> is
+ the inverse of \<open>x\<close> wrt.\ addition and \<open>0\<close> is the neutral element of
+ addition. Addition and multiplication are distributive; scalar
+ multiplication is associative and the real number \<open>1\<close> is the neutral
+ element of scalar multiplication.
\<close>
locale vectorspace =
@@ -65,7 +64,8 @@
lemma neg_closed [iff]: "x \<in> V \<Longrightarrow> - x \<in> V"
by (simp add: negate_eq1)
-lemma add_left_commute: "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> z \<in> V \<Longrightarrow> x + (y + z) = y + (x + z)"
+lemma add_left_commute:
+ "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> z \<in> V \<Longrightarrow> x + (y + z) = y + (x + z)"
proof -
assume xyz: "x \<in> V" "y \<in> V" "z \<in> V"
then have "x + (y + z) = (x + y) + z"
@@ -78,8 +78,8 @@
lemmas add_ac = add_assoc add_commute add_left_commute
-text \<open>The existence of the zero element of a vector space
- follows from the non-emptiness of carrier set.\<close>
+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 -
@@ -214,7 +214,8 @@
then show "x + y = x + z" by (simp only:)
qed
-lemma add_right_cancel: "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> z \<in> V \<Longrightarrow> (y + x = z + x) = (y = z)"
+lemma add_right_cancel:
+ "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> z \<in> V \<Longrightarrow> (y + x = z + x) = (y = z)"
by (simp only: add_commute add_left_cancel)
lemma add_assoc_cong:
@@ -372,4 +373,3 @@
end
end
-
--- a/src/HOL/Hahn_Banach/Zorn_Lemma.thy Mon Nov 02 18:35:41 2015 +0100
+++ b/src/HOL/Hahn_Banach/Zorn_Lemma.thy Mon Nov 02 20:11:16 2015 +0100
@@ -10,13 +10,12 @@
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
+ set \<open>S\<close> has an upper bound in \<open>S\<close>, then there exists a
+ maximal element in \<open>S\<close>. In our application, \<open>S\<close> 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 @{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}.
+ of Zorn's lemma can be modified: if \<open>S\<close> is non-empty, it
+ suffices to show that for every non-empty chain \<open>c\<close> in \<open>S\<close> the union of \<open>c\<close> also lies in \<open>S\<close>.
\<close>
theorem Zorn's_Lemma:
@@ -30,14 +29,14 @@
show "\<exists>y \<in> S. \<forall>z \<in> c. z \<subseteq> y"
proof cases
- txt \<open>If @{text c} is an empty chain, then every element in
- @{text S} is an upper bound of @{text c}.\<close>
+ txt \<open>If \<open>c\<close> is an empty chain, then every element in
+ \<open>S\<close> is an upper bound of \<open>c\<close>.\<close>
assume "c = {}"
with aS show ?thesis by fast
- txt \<open>If @{text c} is non-empty, then @{text "\<Union>c"} is an upper
- bound of @{text c}, lying in @{text S}.\<close>
+ txt \<open>If \<open>c\<close> is non-empty, then \<open>\<Union>c\<close> is an upper
+ bound of \<open>c\<close>, lying in \<open>S\<close>.\<close>
next
assume "c \<noteq> {}"
--- a/src/HOL/Hahn_Banach/document/root.tex Mon Nov 02 18:35:41 2015 +0100
+++ b/src/HOL/Hahn_Banach/document/root.tex Mon Nov 02 20:11:16 2015 +0100
@@ -16,7 +16,7 @@
\pagenumbering{arabic}
\title{The Hahn-Banach Theorem \\ for Real Vector Spaces}
-\author{Gertrud Bauer \\ \url{http://www.in.tum.de/~bauerg/}}
+\author{Gertrud Bauer}
\maketitle
\begin{abstract}
--- a/src/HOL/Isar_Examples/Basic_Logic.thy Mon Nov 02 18:35:41 2015 +0100
+++ b/src/HOL/Isar_Examples/Basic_Logic.thy Mon Nov 02 20:11:16 2015 +0100
@@ -13,10 +13,9 @@
subsection \<open>Pure backward reasoning\<close>
-text \<open>In order to get a first idea of how Isabelle/Isar proof
- documents may look like, we consider the propositions @{text I},
- @{text K}, and @{text S}. The following (rather explicit) proofs
- should require little extra explanations.\<close>
+text \<open>In order to get a first idea of how Isabelle/Isar proof documents may
+ look like, we consider the propositions \<open>I\<close>, \<open>K\<close>, and \<open>S\<close>. The following
+ (rather explicit) proofs should require little extra explanations.\<close>
lemma I: "A \<longrightarrow> A"
proof
@@ -51,14 +50,12 @@
qed
qed
-text \<open>Isar provides several ways to fine-tune the reasoning,
- avoiding excessive detail. Several abbreviated language elements
- are available, enabling the writer to express proofs in a more
- concise way, even without referring to any automated proof tools
- yet.
+text \<open>Isar provides several ways to fine-tune the reasoning, avoiding
+ excessive detail. Several abbreviated language elements are available,
+ enabling the writer to express proofs in a more concise way, even without
+ referring to any automated proof tools yet.
- First of all, proof by assumption may be abbreviated as a single
- dot.\<close>
+ First of all, proof by assumption may be abbreviated as a single dot.\<close>
lemma "A \<longrightarrow> A"
proof
@@ -66,21 +63,21 @@
show A by fact+
qed
-text \<open>In fact, concluding any (sub-)proof already involves solving
- any remaining goals by assumption\footnote{This is not a completely
- trivial operation, as proof by assumption may involve full
- higher-order unification.}. Thus we may skip the rather vacuous
- body of the above proof as well.\<close>
+text \<open>In fact, concluding any (sub-)proof already involves solving any
+ remaining goals by assumption\footnote{This is not a completely trivial
+ operation, as proof by assumption may involve full higher-order
+ unification.}. Thus we may skip the rather vacuous body of the above proof
+ as well.\<close>
lemma "A \<longrightarrow> A"
proof
qed
-text \<open>Note that the \isacommand{proof} command refers to the @{text
- rule} method (without arguments) by default. Thus it implicitly
- applies a single rule, as determined from the syntactic form of the
- statements involved. The \isacommand{by} command abbreviates any
- proof with empty body, so the proof may be further pruned.\<close>
+text \<open>Note that the \isacommand{proof} command refers to the \<open>rule\<close> method
+ (without arguments) by default. Thus it implicitly applies a single rule,
+ as determined from the syntactic form of the statements involved. The
+ \isacommand{by} command abbreviates any proof with empty body, so the
+ proof may be further pruned.\<close>
lemma "A \<longrightarrow> A"
by rule
@@ -89,19 +86,18 @@
lemma "A \<longrightarrow> A" ..
-text \<open>Thus we have arrived at an adequate representation of the
- proof of a tautology that holds by a single standard
- rule.\footnote{Apparently, the rule here is implication
- introduction.}\<close>
+text \<open>Thus we have arrived at an adequate representation of the proof of a
+ tautology that holds by a single standard rule.\footnote{Apparently, the
+ rule here is implication introduction.}
-text \<open>Let us also reconsider @{text K}. Its statement is composed
- of iterated connectives. Basic decomposition is by a single rule at
- a time, which is why our first version above was by nesting two
- proofs.
+ \<^medskip>
+ Let us also reconsider \<open>K\<close>. Its statement is composed of iterated
+ connectives. Basic decomposition is by a single rule at a time, which is
+ why our first version above was by nesting two proofs.
- The @{text intro} proof method repeatedly decomposes a goal's
- conclusion.\footnote{The dual method is @{text elim}, acting on a
- goal's premises.}\<close>
+ The \<open>intro\<close> proof method repeatedly decomposes a goal's
+ conclusion.\footnote{The dual method is \<open>elim\<close>, acting on a goal's
+ premises.}\<close>
lemma "A \<longrightarrow> B \<longrightarrow> A"
proof (intro impI)
@@ -114,29 +110,27 @@
lemma "A \<longrightarrow> B \<longrightarrow> A"
by (intro impI)
-text \<open>Just like @{text rule}, the @{text intro} and @{text elim}
- proof methods pick standard structural rules, in case no explicit
- arguments are given. While implicit rules are usually just fine for
- single rule application, this may go too far with iteration. Thus
- in practice, @{text intro} and @{text elim} would be typically
- restricted to certain structures by giving a few rules only, e.g.\
- \isacommand{proof}~@{text "(intro impI allI)"} to strip implications
- and universal quantifiers.
+text \<open>Just like \<open>rule\<close>, the \<open>intro\<close> and \<open>elim\<close> proof methods pick standard
+ structural rules, in case no explicit arguments are given. While implicit
+ rules are usually just fine for single rule application, this may go too
+ far with iteration. Thus in practice, \<open>intro\<close> and \<open>elim\<close> would be
+ typically restricted to certain structures by giving a few rules only,
+ e.g.\ \isacommand{proof}~\<open>(intro impI allI)\<close> to strip implications and
+ universal quantifiers.
- Such well-tuned iterated decomposition of certain structures is the
- prime application of @{text intro} and @{text elim}. In contrast,
- terminal steps that solve a goal completely are usually performed by
- actual automated proof methods (such as \isacommand{by}~@{text
- blast}.\<close>
+ Such well-tuned iterated decomposition of certain structures is the prime
+ application of \<open>intro\<close> and \<open>elim\<close>. In contrast, terminal steps that solve
+ a goal completely are usually performed by actual automated proof methods
+ (such as \isacommand{by}~\<open>blast\<close>.\<close>
subsection \<open>Variations of backward vs.\ forward reasoning\<close>
-text \<open>Certainly, any proof may be performed in backward-style only.
- On the other hand, small steps of reasoning are often more naturally
- expressed in forward-style. Isar supports both backward and forward
- reasoning as a first-class concept. In order to demonstrate the
- difference, we consider several proofs of @{text "A \<and> B \<longrightarrow> B \<and> A"}.
+text \<open>Certainly, any proof may be performed in backward-style only. On the
+ other hand, small steps of reasoning are often more naturally expressed in
+ forward-style. Isar supports both backward and forward reasoning as a
+ first-class concept. In order to demonstrate the difference, we consider
+ several proofs of \<open>A \<and> B \<longrightarrow> B \<and> A\<close>.
The first version is purely backward.\<close>
@@ -150,13 +144,12 @@
qed
qed
-text \<open>Above, the @{text "conjunct_1/2"} projection rules had to be
- named explicitly, since the goals @{text B} and @{text A} did not
- provide any structural clue. This may be avoided using
- \isacommand{from} to focus on the @{text "A \<and> B"} assumption as the
- current facts, enabling the use of double-dot proofs. Note that
- \isacommand{from} already does forward-chaining, involving the
- @{text conjE} rule here.\<close>
+text \<open>Above, the projection rules \<open>conjunct1\<close> / \<open>conjunct2\<close> had to be named
+ explicitly, since the goals \<open>B\<close> and \<open>A\<close> did not provide any structural
+ clue. This may be avoided using \isacommand{from} to focus on the \<open>A \<and> B\<close>
+ assumption as the current facts, enabling the use of double-dot proofs.
+ Note that \isacommand{from} already does forward-chaining, involving the
+ \<open>conjE\<close> rule here.\<close>
lemma "A \<and> B \<longrightarrow> B \<and> A"
proof
@@ -168,27 +161,26 @@
qed
qed
-text \<open>In the next version, we move the forward step one level
- upwards. Forward-chaining from the most recent facts is indicated
- by the \isacommand{then} command. Thus the proof of @{text "B \<and> A"}
- from @{text "A \<and> B"} actually becomes an elimination, rather than an
- introduction. The resulting proof structure directly corresponds to
- that of the @{text conjE} rule, including the repeated goal
- proposition that is abbreviated as @{text ?thesis} below.\<close>
+text \<open>In the next version, we move the forward step one level upwards.
+ Forward-chaining from the most recent facts is indicated by the
+ \isacommand{then} command. Thus the proof of \<open>B \<and> A\<close> from \<open>A \<and> B\<close> actually
+ becomes an elimination, rather than an introduction. The resulting proof
+ structure directly corresponds to that of the \<open>conjE\<close> rule, including the
+ repeated goal proposition that is abbreviated as \<open>?thesis\<close> below.\<close>
lemma "A \<and> B \<longrightarrow> B \<and> A"
proof
assume "A \<and> B"
then show "B \<and> A"
- proof -- \<open>rule @{text conjE} of @{text "A \<and> B"}\<close>
+ proof -- \<open>rule \<open>conjE\<close> of \<open>A \<and> B\<close>\<close>
assume B A
- then show ?thesis .. -- \<open>rule @{text conjI} of @{text "B \<and> A"}\<close>
+ then show ?thesis .. -- \<open>rule \<open>conjI\<close> of \<open>B \<and> A\<close>\<close>
qed
qed
-text \<open>In the subsequent version we flatten the structure of the main
- body by doing forward reasoning all the time. Only the outermost
- decomposition step is left as backward.\<close>
+text \<open>In the subsequent version we flatten the structure of the main body by
+ doing forward reasoning all the time. Only the outermost decomposition
+ step is left as backward.\<close>
lemma "A \<and> B \<longrightarrow> B \<and> A"
proof
@@ -198,9 +190,9 @@
from \<open>B\<close> \<open>A\<close> show "B \<and> A" ..
qed
-text \<open>We can still push forward-reasoning a bit further, even at the
- risk of getting ridiculous. Note that we force the initial proof
- step to do nothing here, by referring to the ``-'' proof method.\<close>
+text \<open>We can still push forward-reasoning a bit further, even at the risk of
+ getting ridiculous. Note that we force the initial proof step to do
+ nothing here, by referring to the \<open>-\<close> proof method.\<close>
lemma "A \<and> B \<longrightarrow> B \<and> A"
proof -
@@ -210,27 +202,28 @@
from \<open>A \<and> B\<close> have B ..
from \<open>B\<close> \<open>A\<close> have "B \<and> A" ..
}
- then show ?thesis .. -- \<open>rule @{text impI}\<close>
+ then show ?thesis .. -- \<open>rule \<open>impI\<close>\<close>
qed
-text \<open>\medskip With these examples we have shifted through a whole
- range from purely backward to purely forward reasoning. Apparently,
- in the extreme ends we get slightly ill-structured proofs, which
- also require much explicit naming of either rules (backward) or
- local facts (forward).
+text \<open>
+ \<^medskip>
+ With these examples we have shifted through a whole range from purely
+ backward to purely forward reasoning. Apparently, in the extreme ends we
+ get slightly ill-structured proofs, which also require much explicit
+ naming of either rules (backward) or local facts (forward).
- The general lesson learned here is that good proof style would
- achieve just the \emph{right} balance of top-down backward
- decomposition, and bottom-up forward composition. In general, there
- is no single best way to arrange some pieces of formal reasoning, of
- course. Depending on the actual applications, the intended audience
- etc., rules (and methods) on the one hand vs.\ facts on the other
- hand have to be emphasized in an appropriate way. This requires the
- proof writer to develop good taste, and some practice, of course.\<close>
+ The general lesson learned here is that good proof style would achieve
+ just the \<^emph>\<open>right\<close> balance of top-down backward decomposition, and
+ bottom-up forward composition. In general, there is no single best way to
+ arrange some pieces of formal reasoning, of course. Depending on the
+ actual applications, the intended audience etc., rules (and methods) on
+ the one hand vs.\ facts on the other hand have to be emphasized in an
+ appropriate way. This requires the proof writer to develop good taste, and
+ some practice, of course.
-text \<open>For our example the most appropriate way of reasoning is
- probably the middle one, with conjunction introduction done after
- elimination.\<close>
+ \<^medskip>
+ For our example the most appropriate way of reasoning is probably the
+ middle one, with conjunction introduction done after elimination.\<close>
lemma "A \<and> B \<longrightarrow> B \<and> A"
proof
@@ -246,50 +239,48 @@
subsection \<open>A few examples from ``Introduction to Isabelle''\<close>
-text \<open>We rephrase some of the basic reasoning examples of
- @{cite "isabelle-intro"}, using HOL rather than FOL.\<close>
+text \<open>We rephrase some of the basic reasoning examples of @{cite
+ "isabelle-intro"}, using HOL rather than FOL.\<close>
subsubsection \<open>A propositional proof\<close>
-text \<open>We consider the proposition @{text "P \<or> P \<longrightarrow> P"}. The proof
- below involves forward-chaining from @{text "P \<or> P"}, followed by an
- explicit case-analysis on the two \emph{identical} cases.\<close>
+text \<open>We consider the proposition \<open>P \<or> P \<longrightarrow> P\<close>. The proof below involves
+ forward-chaining from \<open>P \<or> P\<close>, followed by an explicit case-analysis on
+ the two \<^emph>\<open>identical\<close> cases.\<close>
lemma "P \<or> P \<longrightarrow> P"
proof
assume "P \<or> P"
then show P
- proof -- \<open>
- rule @{text disjE}: \smash{$\infer{C}{A \disj B & \infer*{C}{[A]} & \infer*{C}{[B]}}$}
-\<close>
+ proof -- \<open>rule \<open>disjE\<close>: \smash{$\infer{\<open>C\<close>}{\<open>A \<or> B\<close> & \infer*{\<open>C\<close>}{[\<open>A\<close>]} & \infer*{\<open>C\<close>}{[\<open>B\<close>]}}$}\<close>
assume P show P by fact
next
assume P show P by fact
qed
qed
-text \<open>Case splits are \emph{not} hardwired into the Isar language as
- a special feature. The \isacommand{next} command used to separate
- the cases above is just a short form of managing block structure.
+text \<open>Case splits are \<^emph>\<open>not\<close> hardwired into the Isar language as a
+ special feature. The \isacommand{next} command used to separate the cases
+ above is just a short form of managing block structure.
- \medskip In general, applying proof methods may split up a goal into
- separate ``cases'', i.e.\ new subgoals with individual local
- assumptions. The corresponding proof text typically mimics this by
- establishing results in appropriate contexts, separated by blocks.
+ \<^medskip>
+ In general, applying proof methods may split up a goal into separate
+ ``cases'', i.e.\ new subgoals with individual local assumptions. The
+ corresponding proof text typically mimics this by establishing results in
+ appropriate contexts, separated by blocks.
In order to avoid too much explicit parentheses, the Isar system
implicitly opens an additional block for any new goal, the
- \isacommand{next} statement then closes one block level, opening a
- new one. The resulting behavior is what one would expect from
- separating cases, only that it is more flexible. E.g.\ an induction
- base case (which does not introduce local assumptions) would
- \emph{not} require \isacommand{next} to separate the subsequent step
- case.
+ \isacommand{next} statement then closes one block level, opening a new
+ one. The resulting behaviour is what one would expect from separating
+ cases, only that it is more flexible. E.g.\ an induction base case (which
+ does not introduce local assumptions) would \<^emph>\<open>not\<close> require
+ \isacommand{next} to separate the subsequent step case.
- \medskip In our example the situation is even simpler, since the two
- cases actually coincide. Consequently the proof may be rephrased as
- follows.\<close>
+ \<^medskip>
+ In our example the situation is even simpler, since the two cases actually
+ coincide. Consequently the proof may be rephrased as follows.\<close>
lemma "P \<or> P \<longrightarrow> P"
proof
@@ -316,37 +307,33 @@
subsubsection \<open>A quantifier proof\<close>
-text \<open>To illustrate quantifier reasoning, let us prove @{text
- "(\<exists>x. P (f x)) \<longrightarrow> (\<exists>y. P y)"}. Informally, this holds because any
- @{text a} with @{text "P (f a)"} may be taken as a witness for the
- second existential statement.
+text \<open>To illustrate quantifier reasoning, let us prove
+ \<open>(\<exists>x. P (f x)) \<longrightarrow> (\<exists>y. P y)\<close>. Informally, this holds because any \<open>a\<close> with
+ \<open>P (f a)\<close> may be taken as a witness for the second existential statement.
- The first proof is rather verbose, exhibiting quite a lot of
- (redundant) detail. It gives explicit rules, even with some
- instantiation. Furthermore, we encounter two new language elements:
- the \isacommand{fix} command augments the context by some new
- ``arbitrary, but fixed'' element; the \isacommand{is} annotation
- binds term abbreviations by higher-order pattern matching.\<close>
+ The first proof is rather verbose, exhibiting quite a lot of (redundant)
+ detail. It gives explicit rules, even with some instantiation.
+ Furthermore, we encounter two new language elements: the \isacommand{fix}
+ command augments the context by some new ``arbitrary, but fixed'' element;
+ the \isacommand{is} annotation binds term abbreviations by higher-order
+ pattern matching.\<close>
lemma "(\<exists>x. P (f x)) \<longrightarrow> (\<exists>y. P y)"
proof
assume "\<exists>x. P (f x)"
then show "\<exists>y. P y"
- proof (rule exE) -- \<open>
- rule @{text exE}: \smash{$\infer{B}{\ex x A(x) & \infer*{B}{[A(x)]_x}}$}
-\<close>
+ proof (rule exE) -- \<open>rule \<open>exE\<close>: \smash{$\infer{\<open>B\<close>}{\<open>\<exists>x. A(x)\<close> & \infer*{\<open>B\<close>}{[\<open>A(x)\<close>]_x}}$}\<close>
fix a
assume "P (f a)" (is "P ?witness")
then show ?thesis by (rule exI [of P ?witness])
qed
qed
-text \<open>While explicit rule instantiation may occasionally improve
- readability of certain aspects of reasoning, it is usually quite
- redundant. Above, the basic proof outline gives already enough
- structural clues for the system to infer both the rules and their
- instances (by higher-order unification). Thus we may as well prune
- the text as follows.\<close>
+text \<open>While explicit rule instantiation may occasionally improve readability
+ of certain aspects of reasoning, it is usually quite redundant. Above, the
+ basic proof outline gives already enough structural clues for the system
+ to infer both the rules and their instances (by higher-order unification).
+ Thus we may as well prune the text as follows.\<close>
lemma "(\<exists>x. P (f x)) \<longrightarrow> (\<exists>y. P y)"
proof
@@ -359,10 +346,9 @@
qed
qed
-text \<open>Explicit @{text \<exists>}-elimination as seen above can become quite
- cumbersome in practice. The derived Isar language element
- ``\isakeyword{obtain}'' provides a more handsome way to do
- generalized existence reasoning.\<close>
+text \<open>Explicit \<open>\<exists>\<close>-elimination as seen above can become quite cumbersome in
+ practice. The derived Isar language element ``\isakeyword{obtain}''
+ provides a more handsome way to do generalized existence reasoning.\<close>
lemma "(\<exists>x. P (f x)) \<longrightarrow> (\<exists>y. P y)"
proof
@@ -371,21 +357,19 @@
then show "\<exists>y. P y" ..
qed
-text \<open>Technically, \isakeyword{obtain} is similar to
- \isakeyword{fix} and \isakeyword{assume} together with a soundness
- proof of the elimination involved. Thus it behaves similar to any
- other forward proof element. Also note that due to the nature of
- general existence reasoning involved here, any result exported from
- the context of an \isakeyword{obtain} statement may \emph{not} refer
- to the parameters introduced there.\<close>
+text \<open>Technically, \isakeyword{obtain} is similar to \isakeyword{fix} and
+ \isakeyword{assume} together with a soundness proof of the elimination
+ involved. Thus it behaves similar to any other forward proof element. Also
+ note that due to the nature of general existence reasoning involved here,
+ any result exported from the context of an \isakeyword{obtain} statement
+ may \<^emph>\<open>not\<close> refer to the parameters introduced there.\<close>
subsubsection \<open>Deriving rules in Isabelle\<close>
-text \<open>We derive the conjunction elimination rule from the
- corresponding projections. The proof is quite straight-forward,
- since Isabelle/Isar supports non-atomic goals and assumptions fully
- transparently.\<close>
+text \<open>We derive the conjunction elimination rule from the corresponding
+ projections. The proof is quite straight-forward, since Isabelle/Isar
+ supports non-atomic goals and assumptions fully transparently.\<close>
theorem conjE: "A \<and> B \<Longrightarrow> (A \<Longrightarrow> B \<Longrightarrow> C) \<Longrightarrow> C"
proof -
--- a/src/HOL/Isar_Examples/Cantor.thy Mon Nov 02 18:35:41 2015 +0100
+++ b/src/HOL/Isar_Examples/Cantor.thy Mon Nov 02 20:11:16 2015 +0100
@@ -12,17 +12,17 @@
the Isabelle/HOL manual @{cite "isabelle-HOL"}.}\<close>
text \<open>Cantor's Theorem states that every set has more subsets than
- it has elements. It has become a favorite basic example in pure
- higher-order logic since it is so easily expressed: \[\all{f::\alpha
- \To \alpha \To \idt{bool}} \ex{S::\alpha \To \idt{bool}}
- \all{x::\alpha} f \ap x \not= S\]
+ it has elements. It has become a favourite basic example in pure
+ higher-order logic since it is so easily expressed:
+
+ @{text [display]
+ \<open>\<forall>f::\<alpha> \<Rightarrow> \<alpha> \<Rightarrow> bool. \<exists>S::\<alpha> \<Rightarrow> bool. \<forall>x::\<alpha>. f x \<noteq> S\<close>}
- Viewing types as sets, $\alpha \To \idt{bool}$ represents the
- powerset of $\alpha$. This version of the theorem states that for
- every function from $\alpha$ to its powerset, some subset is outside
- its range. The Isabelle/Isar proofs below uses HOL's set theory,
- with the type $\alpha \ap \idt{set}$ and the operator
- $\idt{range}::(\alpha \To \beta) \To \beta \ap \idt{set}$.\<close>
+ Viewing types as sets, \<open>\<alpha> \<Rightarrow> bool\<close> represents the powerset of \<open>\<alpha>\<close>. This
+ version of the theorem states that for every function from \<open>\<alpha>\<close> to its
+ powerset, some subset is outside its range. The Isabelle/Isar proofs below
+ uses HOL's set theory, with the type \<open>\<alpha> set\<close> and the operator
+ \<open>range :: (\<alpha> \<Rightarrow> \<beta>) \<Rightarrow> \<beta> set\<close>.\<close>
theorem "\<exists>S. S \<notin> range (f :: 'a \<Rightarrow> 'a set)"
proof
@@ -46,20 +46,19 @@
qed
qed
-text \<open>How much creativity is required? As it happens, Isabelle can
- prove this theorem automatically using best-first search.
- Depth-first search would diverge, but best-first search successfully
- navigates through the large search space. The context of Isabelle's
- classical prover contains rules for the relevant constructs of HOL's
- set theory.\<close>
+text \<open>How much creativity is required? As it happens, Isabelle can prove
+ this theorem automatically using best-first search. Depth-first search
+ would diverge, but best-first search successfully navigates through the
+ large search space. The context of Isabelle's classical prover contains
+ rules for the relevant constructs of HOL's set theory.\<close>
theorem "\<exists>S. S \<notin> range (f :: 'a \<Rightarrow> 'a set)"
by best
-text \<open>While this establishes the same theorem internally, we do not
- get any idea of how the proof actually works. There is currently no
- way to transform internal system-level representations of Isabelle
- proofs back into Isar text. Writing intelligible proof documents
- really is a creative process, after all.\<close>
+text \<open>While this establishes the same theorem internally, we do not get any
+ idea of how the proof actually works. There is currently no way to
+ transform internal system-level representations of Isabelle proofs back
+ into Isar text. Writing intelligible proof documents really is a creative
+ process, after all.\<close>
end
--- a/src/HOL/Isar_Examples/Drinker.thy Mon Nov 02 18:35:41 2015 +0100
+++ b/src/HOL/Isar_Examples/Drinker.thy Mon Nov 02 20:11:16 2015 +0100
@@ -9,8 +9,8 @@
begin
text \<open>Here is another example of classical reasoning: the Drinker's
- Principle says that for some person, if he is drunk, everybody else
- is drunk!
+ Principle says that for some person, if he is drunk, everybody else is
+ drunk!
We first prove a classical part of de-Morgan's law.\<close>
--- a/src/HOL/Isar_Examples/Expr_Compiler.thy Mon Nov 02 18:35:41 2015 +0100
+++ b/src/HOL/Isar_Examples/Expr_Compiler.thy Mon Nov 02 20:11:16 2015 +0100
@@ -10,17 +10,16 @@
imports Main
begin
-text \<open>This is a (rather trivial) example of program verification.
- We model a compiler for translating expressions to stack machine
- instructions, and prove its correctness wrt.\ some evaluation
- semantics.\<close>
+text \<open>This is a (rather trivial) example of program verification. We model a
+ compiler for translating expressions to stack machine instructions, and
+ prove its correctness wrt.\ some evaluation semantics.\<close>
subsection \<open>Binary operations\<close>
-text \<open>Binary operations are just functions over some type of values.
- This is both for abstract syntax and semantics, i.e.\ we use a
- ``shallow embedding'' here.\<close>
+text \<open>Binary operations are just functions over some type of values. This is
+ both for abstract syntax and semantics, i.e.\ we use a ``shallow
+ embedding'' here.\<close>
type_synonym 'val binop = "'val \<Rightarrow> 'val \<Rightarrow> 'val"
@@ -28,16 +27,15 @@
subsection \<open>Expressions\<close>
text \<open>The language of expressions is defined as an inductive type,
- consisting of variables, constants, and binary operations on
- expressions.\<close>
+ consisting of variables, constants, and binary operations on expressions.\<close>
datatype (dead 'adr, dead 'val) expr =
Variable 'adr
| Constant 'val
| Binop "'val binop" "('adr, 'val) expr" "('adr, 'val) expr"
-text \<open>Evaluation (wrt.\ some environment of variable assignments) is
- defined by primitive recursion over the structure of expressions.\<close>
+text \<open>Evaluation (wrt.\ some environment of variable assignments) is defined
+ by primitive recursion over the structure of expressions.\<close>
primrec eval :: "('adr, 'val) expr \<Rightarrow> ('adr \<Rightarrow> 'val) \<Rightarrow> 'val"
where
@@ -48,16 +46,15 @@
subsection \<open>Machine\<close>
-text \<open>Next we model a simple stack machine, with three
- instructions.\<close>
+text \<open>Next we model a simple stack machine, with three instructions.\<close>
datatype (dead 'adr, dead 'val) instr =
Const 'val
| Load 'adr
| Apply "'val binop"
-text \<open>Execution of a list of stack machine instructions is easily
- defined as follows.\<close>
+text \<open>Execution of a list of stack machine instructions is easily defined as
+ follows.\<close>
primrec exec :: "(('adr, 'val) instr) list \<Rightarrow> 'val list \<Rightarrow> ('adr \<Rightarrow> 'val) \<Rightarrow> 'val list"
where
@@ -75,8 +72,8 @@
subsection \<open>Compiler\<close>
-text \<open>We are ready to define the compilation function of expressions
- to lists of stack machine instructions.\<close>
+text \<open>We are ready to define the compilation function of expressions to
+ lists of stack machine instructions.\<close>
primrec compile :: "('adr, 'val) expr \<Rightarrow> (('adr, 'val) instr) list"
where
@@ -85,9 +82,8 @@
| "compile (Binop f e1 e2) = compile e2 @ compile e1 @ [Apply f]"
-text \<open>The main result of this development is the correctness theorem
- for @{text compile}. We first establish a lemma about @{text exec}
- and list append.\<close>
+text \<open>The main result of this development is the correctness theorem for
+ \<open>compile\<close>. We first establish a lemma about \<open>exec\<close> and list append.\<close>
lemma exec_append:
"exec (xs @ ys) stack env =
@@ -127,11 +123,14 @@
qed
-text \<open>\bigskip In the proofs above, the @{text simp} method does
- quite a lot of work behind the scenes (mostly ``functional program
- execution''). Subsequently, the same reasoning is elaborated in
- detail --- at most one recursive function definition is used at a
- time. Thus we get a better idea of what is actually going on.\<close>
+text \<open>
+ \<^bigskip>
+ In the proofs above, the \<open>simp\<close> method does quite a lot of work behind the
+ scenes (mostly ``functional program execution''). Subsequently, the same
+ reasoning is elaborated in detail --- at most one recursive function
+ definition is used at a time. Thus we get a better idea of what is
+ actually going on.
+\<close>
lemma exec_append':
"exec (xs @ ys) stack env = exec ys (exec xs stack env) env"
--- a/src/HOL/Isar_Examples/Group.thy Mon Nov 02 18:35:41 2015 +0100
+++ b/src/HOL/Isar_Examples/Group.thy Mon Nov 02 20:11:16 2015 +0100
@@ -10,18 +10,17 @@
subsection \<open>Groups and calculational reasoning\<close>
-text \<open>Groups over signature $({\times} :: \alpha \To \alpha \To
- \alpha, \idt{one} :: \alpha, \idt{inverse} :: \alpha \To \alpha)$
- are defined as an axiomatic type class as follows. Note that the
- parent class $\idt{times}$ is provided by the basic HOL theory.\<close>
+text \<open>Groups over signature \<open>(\<times> :: \<alpha> \<Rightarrow> \<alpha> \<Rightarrow> \<alpha>, one :: \<alpha>, inverse :: \<alpha> \<Rightarrow> \<alpha>)\<close>
+ are defined as an axiomatic type class as follows. Note that the parent
+ class \<open>\<times>\<close> is provided by the basic HOL theory.\<close>
class group = times + one + inverse +
assumes group_assoc: "(x * y) * z = x * (y * z)"
and group_left_one: "1 * x = x"
and group_left_inverse: "inverse x * x = 1"
-text \<open>The group axioms only state the properties of left one and
- inverse, the right versions may be derived as follows.\<close>
+text \<open>The group axioms only state the properties of left one and inverse,
+ the right versions may be derived as follows.\<close>
theorem (in group) group_right_inverse: "x * inverse x = 1"
proof -
@@ -44,9 +43,8 @@
finally show ?thesis .
qed
-text \<open>With \name{group-right-inverse} already available,
- \name{group-right-one}\label{thm:group-right-one} is now established
- much easier.\<close>
+text \<open>With \<open>group_right_inverse\<close> already available, \<open>group_right_one\<close>
+ \label{thm:group-right-one} is now established much easier.\<close>
theorem (in group) group_right_one: "x * 1 = x"
proof -
@@ -61,27 +59,27 @@
finally show ?thesis .
qed
-text \<open>\medskip The calculational proof style above follows typical
- presentations given in any introductory course on algebra. The
- basic technique is to form a transitive chain of equations, which in
- turn are established by simplifying with appropriate rules. The
- low-level logical details of equational reasoning are left implicit.
+text \<open>
+ \<^medskip>
+ The calculational proof style above follows typical presentations given in
+ any introductory course on algebra. The basic technique is to form a
+ transitive chain of equations, which in turn are established by
+ simplifying with appropriate rules. The low-level logical details of
+ equational reasoning are left implicit.
- Note that ``$\dots$'' is just a special term variable that is bound
- automatically to the argument\footnote{The argument of a curried
- infix expression happens to be its right-hand side.} of the last
- fact achieved by any local assumption or proven statement. In
- contrast to $\var{thesis}$, the ``$\dots$'' variable is bound
- \emph{after} the proof is finished, though.
+ Note that ``\<open>\<dots>\<close>'' is just a special term variable that is bound
+ automatically to the argument\footnote{The argument of a curried infix
+ expression happens to be its right-hand side.} of the last fact achieved
+ by any local assumption or proven statement. In contrast to \<open>?thesis\<close>, the
+ ``\<open>\<dots>\<close>'' variable is bound \<^emph>\<open>after\<close> the proof is finished.
There are only two separate Isar language elements for calculational
- proofs: ``\isakeyword{also}'' for initial or intermediate
- calculational steps, and ``\isakeyword{finally}'' for exhibiting the
- result of a calculation. These constructs are not hardwired into
- Isabelle/Isar, but defined on top of the basic Isar/VM interpreter.
- Expanding the \isakeyword{also} and \isakeyword{finally} derived
- language elements, calculations may be simulated by hand as
- demonstrated below.\<close>
+ proofs: ``\isakeyword{also}'' for initial or intermediate calculational
+ steps, and ``\isakeyword{finally}'' for exhibiting the result of a
+ calculation. These constructs are not hardwired into Isabelle/Isar, but
+ defined on top of the basic Isar/VM interpreter. Expanding the
+ \isakeyword{also} and \isakeyword{finally} derived language elements,
+ calculations may be simulated by hand as demonstrated below.\<close>
theorem (in group) "x * 1 = x"
proof -
@@ -114,51 +112,49 @@
show ?thesis .
qed
-text \<open>Note that this scheme of calculations is not restricted to
- plain transitivity. Rules like anti-symmetry, or even forward and
- backward substitution work as well. For the actual implementation
- of \isacommand{also} and \isacommand{finally}, Isabelle/Isar
- maintains separate context information of ``transitivity'' rules.
- Rule selection takes place automatically by higher-order
- unification.\<close>
+text \<open>Note that this scheme of calculations is not restricted to plain
+ transitivity. Rules like anti-symmetry, or even forward and backward
+ substitution work as well. For the actual implementation of
+ \isacommand{also} and \isacommand{finally}, Isabelle/Isar maintains
+ separate context information of ``transitivity'' rules. Rule selection
+ takes place automatically by higher-order unification.\<close>
subsection \<open>Groups as monoids\<close>
-text \<open>Monoids over signature $({\times} :: \alpha \To \alpha \To
- \alpha, \idt{one} :: \alpha)$ are defined like this.\<close>
+text \<open>Monoids over signature \<open>(\<times> :: \<alpha> \<Rightarrow> \<alpha> \<Rightarrow> \<alpha>, one :: \<alpha>)\<close> are defined like
+ this.\<close>
class monoid = times + one +
assumes monoid_assoc: "(x * y) * z = x * (y * z)"
and monoid_left_one: "1 * x = x"
and monoid_right_one: "x * 1 = x"
-text \<open>Groups are \emph{not} yet monoids directly from the
- definition. For monoids, \name{right-one} had to be included as an
- axiom, but for groups both \name{right-one} and \name{right-inverse}
- are derivable from the other axioms. With \name{group-right-one}
- derived as a theorem of group theory (see
+text \<open>Groups are \<^emph>\<open>not\<close> yet monoids directly from the definition. For
+ monoids, \<open>right_one\<close> had to be included as an axiom, but for groups both
+ \<open>right_one\<close> and \<open>right_inverse\<close> are derivable from the other axioms. With
+ \<open>group_right_one\<close> derived as a theorem of group theory (see
page~\pageref{thm:group-right-one}), we may still instantiate
- $\idt{group} \subseteq \idt{monoid}$ properly as follows.\<close>
+ \<open>group \<subseteq> monoid\<close> properly as follows.\<close>
-instance group < monoid
+instance group \<subseteq> monoid
by intro_classes
(rule group_assoc,
rule group_left_one,
rule group_right_one)
text \<open>The \isacommand{instance} command actually is a version of
- \isacommand{theorem}, setting up a goal that reflects the intended
- class relation (or type constructor arity). Thus any Isar proof
- language element may be involved to establish this statement. When
- concluding the proof, the result is transformed into the intended
- type signature extension behind the scenes.\<close>
+ \isacommand{theorem}, setting up a goal that reflects the intended class
+ relation (or type constructor arity). Thus any Isar proof language element
+ may be involved to establish this statement. When concluding the proof,
+ the result is transformed into the intended type signature extension
+ behind the scenes.\<close>
subsection \<open>More theorems of group theory\<close>
text \<open>The one element is already uniquely determined by preserving
- an \emph{arbitrary} group element.\<close>
+ an \<^emph>\<open>arbitrary\<close> group element.\<close>
theorem (in group) group_one_equality:
assumes eq: "e * x = x"
--- a/src/HOL/Isar_Examples/Hoare.thy Mon Nov 02 18:35:41 2015 +0100
+++ b/src/HOL/Isar_Examples/Hoare.thy Mon Nov 02 20:11:16 2015 +0100
@@ -12,11 +12,10 @@
subsection \<open>Abstract syntax and semantics\<close>
-text \<open>The following abstract syntax and semantics of Hoare Logic
- over \texttt{WHILE} programs closely follows the existing tradition
- in Isabelle/HOL of formalizing the presentation given in
- @{cite \<open>\S6\<close> "Winskel:1993"}. See also @{file "~~/src/HOL/Hoare"} and
- @{cite "Nipkow:1998:Winskel"}.\<close>
+text \<open>The following abstract syntax and semantics of Hoare Logic over
+ \<^verbatim>\<open>WHILE\<close> programs closely follows the existing tradition in Isabelle/HOL
+ of formalizing the presentation given in @{cite \<open>\S6\<close> "Winskel:1993"}. See
+ also @{file "~~/src/HOL/Hoare"} and @{cite "Nipkow:1998:Winskel"}.\<close>
type_synonym 'a bexp = "'a set"
type_synonym 'a assn = "'a set"
@@ -60,14 +59,15 @@
subsection \<open>Primitive Hoare rules\<close>
-text \<open>From the semantics defined above, we derive the standard set
- of primitive Hoare rules; e.g.\ see @{cite \<open>\S6\<close> "Winskel:1993"}.
- Usually, variant forms of these rules are applied in actual proof,
- see also \S\ref{sec:hoare-isar} and \S\ref{sec:hoare-vcg}.
+text \<open>From the semantics defined above, we derive the standard set of
+ primitive Hoare rules; e.g.\ see @{cite \<open>\S6\<close> "Winskel:1993"}. Usually,
+ variant forms of these rules are applied in actual proof, see also
+ \S\ref{sec:hoare-isar} and \S\ref{sec:hoare-vcg}.
- \medskip The \name{basic} rule represents any kind of atomic access
- to the state space. This subsumes the common rules of \name{skip}
- and \name{assign}, as formulated in \S\ref{sec:hoare-isar}.\<close>
+ \<^medskip>
+ The \<open>basic\<close> rule represents any kind of atomic access to the state space.
+ This subsumes the common rules of \<open>skip\<close> and \<open>assign\<close>, as formulated in
+ \S\ref{sec:hoare-isar}.\<close>
theorem basic: "\<turnstile> {s. f s \<in> P} (Basic f) P"
proof
@@ -79,7 +79,7 @@
qed
text \<open>The rules for sequential commands and semantic consequences are
- established in a straight forward manner as follows.\<close>
+ established in a straight forward manner as follows.\<close>
theorem seq: "\<turnstile> P c1 Q \<Longrightarrow> \<turnstile> Q c2 R \<Longrightarrow> \<turnstile> P (c1; c2) R"
proof
@@ -105,8 +105,8 @@
qed
text \<open>The rule for conditional commands is directly reflected by the
- corresponding semantics; in the proof we just have to look closely
- which cases apply.\<close>
+ corresponding semantics; in the proof we just have to look closely which
+ cases apply.\<close>
theorem cond:
assumes case_b: "\<turnstile> (P \<inter> b) c1 Q"
@@ -134,12 +134,11 @@
qed
qed
-text \<open>The @{text while} rule is slightly less trivial --- it is the
- only one based on recursion, which is expressed in the semantics by
- a Kleene-style least fixed-point construction. The auxiliary
- statement below, which is by induction on the number of iterations
- is the main point to be proven; the rest is by routine application
- of the semantics of \texttt{WHILE}.\<close>
+text \<open>The \<open>while\<close> rule is slightly less trivial --- it is the only one based
+ on recursion, which is expressed in the semantics by a Kleene-style least
+ fixed-point construction. The auxiliary statement below, which is by
+ induction on the number of iterations is the main point to be proven; the
+ rest is by routine application of the semantics of \<^verbatim>\<open>WHILE\<close>.\<close>
theorem while:
assumes body: "\<turnstile> (P \<inter> b) c P"
@@ -167,24 +166,23 @@
text \<open>We now introduce concrete syntax for describing commands (with
embedded expressions) and assertions. The basic technique is that of
- semantic ``quote-antiquote''. A \emph{quotation} is a syntactic
- entity delimited by an implicit abstraction, say over the state
- space. An \emph{antiquotation} is a marked expression within a
- quotation that refers the implicit argument; a typical antiquotation
- would select (or even update) components from the state.
+ semantic ``quote-antiquote''. A \<^emph>\<open>quotation\<close> is a syntactic entity
+ delimited by an implicit abstraction, say over the state space. An
+ \<^emph>\<open>antiquotation\<close> is a marked expression within a quotation that refers the
+ implicit argument; a typical antiquotation would select (or even update)
+ components from the state.
- We will see some examples later in the concrete rules and
- applications.\<close>
+ We will see some examples later in the concrete rules and applications.
-text \<open>The following specification of syntax and translations is for
- Isabelle experts only; feel free to ignore it.
+ \<^medskip>
+ The following specification of syntax and translations is for Isabelle
+ experts only; feel free to ignore it.
- While the first part is still a somewhat intelligible specification
- of the concrete syntactic representation of our Hoare language, the
- actual ``ML drivers'' is quite involved. Just note that the we
- re-use the basic quote/antiquote translations as already defined in
- Isabelle/Pure (see @{ML Syntax_Trans.quote_tr}, and
- @{ML Syntax_Trans.quote_tr'},).\<close>
+ While the first part is still a somewhat intelligible specification of the
+ concrete syntactic representation of our Hoare language, the actual ``ML
+ drivers'' is quite involved. Just note that the we re-use the basic
+ quote/antiquote translations as already defined in Isabelle/Pure (see @{ML
+ Syntax_Trans.quote_tr}, and @{ML Syntax_Trans.quote_tr'},).\<close>
syntax
"_quote" :: "'b \<Rightarrow> ('a \<Rightarrow> 'b)"
@@ -213,10 +211,9 @@
in [(@{syntax_const "_quote"}, K quote_tr)] end
\<close>
-text \<open>As usual in Isabelle syntax translations, the part for
- printing is more complicated --- we cannot express parts as macro
- rules as above. Don't look here, unless you have to do similar
- things for yourself.\<close>
+text \<open>As usual in Isabelle syntax translations, the part for printing is
+ more complicated --- we cannot express parts as macro rules as above.
+ Don't look here, unless you have to do similar things for yourself.\<close>
print_translation \<open>
let
@@ -245,13 +242,14 @@
subsection \<open>Rules for single-step proof \label{sec:hoare-isar}\<close>
-text \<open>We are now ready to introduce a set of Hoare rules to be used
- in single-step structured proofs in Isabelle/Isar. We refer to the
- concrete syntax introduce above.
+text \<open>We are now ready to introduce a set of Hoare rules to be used in
+ single-step structured proofs in Isabelle/Isar. We refer to the concrete
+ syntax introduce above.
- \medskip Assertions of Hoare Logic may be manipulated in
- calculational proofs, with the inclusion expressed in terms of sets
- or predicates. Reversed order is supported as well.\<close>
+ \<^medskip>
+ Assertions of Hoare Logic may be manipulated in calculational proofs, with
+ the inclusion expressed in terms of sets or predicates. Reversed order is
+ supported as well.\<close>
lemma [trans]: "\<turnstile> P c Q \<Longrightarrow> P' \<subseteq> P \<Longrightarrow> \<turnstile> P' c Q"
by (unfold Valid_def) blast
@@ -278,10 +276,10 @@
by (simp add: Valid_def)
-text \<open>Identity and basic assignments.\footnote{The $\idt{hoare}$
- method introduced in \S\ref{sec:hoare-vcg} is able to provide proper
- instances for any number of basic assignments, without producing
- additional verification conditions.}\<close>
+text \<open>Identity and basic assignments.\footnote{The \<open>hoare\<close> method introduced
+ in \S\ref{sec:hoare-vcg} is able to provide proper instances for any
+ number of basic assignments, without producing additional verification
+ conditions.}\<close>
lemma skip [intro?]: "\<turnstile> P SKIP P"
proof -
@@ -293,19 +291,19 @@
by (rule basic)
text \<open>Note that above formulation of assignment corresponds to our
- preferred way to model state spaces, using (extensible) record types
- in HOL @{cite "Naraschewski-Wenzel:1998:HOOL"}. For any record field
- $x$, Isabelle/HOL provides a functions $x$ (selector) and
- $\idt{x{\dsh}update}$ (update). Above, there is only a place-holder
- appearing for the latter kind of function: due to concrete syntax
- \isa{\'x := \'a} also contains \isa{x\_update}.\footnote{Note that
- due to the external nature of HOL record fields, we could not even
- state a general theorem relating selector and update functions (if
- this were required here); this would only work for any particular
- instance of record fields introduced so far.}\<close>
+ preferred way to model state spaces, using (extensible) record types in
+ HOL @{cite "Naraschewski-Wenzel:1998:HOOL"}. For any record field \<open>x\<close>,
+ Isabelle/HOL provides a functions \<open>x\<close> (selector) and \<open>x_update\<close> (update).
+ Above, there is only a place-holder appearing for the latter kind of
+ function: due to concrete syntax \<open>\<acute>x := \<acute>a\<close> also contains
+ \<open>x_update\<close>.\footnote{Note that due to the external nature of HOL record
+ fields, we could not even state a general theorem relating selector and
+ update functions (if this were required here); this would only work for
+ any particular instance of record fields introduced so far.}
-text \<open>Sequential composition --- normalizing with associativity
- achieves proper of chunks of code verified separately.\<close>
+ \<^medskip>
+ Sequential composition --- normalizing with associativity achieves proper
+ of chunks of code verified separately.\<close>
lemmas [trans, intro?] = seq
@@ -344,16 +342,15 @@
subsection \<open>Verification conditions \label{sec:hoare-vcg}\<close>
-text \<open>We now load the \emph{original} ML file for proof scripts and
- tactic definition for the Hoare Verification Condition Generator
- (see @{file "~~/src/HOL/Hoare/"}). As far as we
- are concerned here, the result is a proof method \name{hoare}, which
- may be applied to a Hoare Logic assertion to extract purely logical
- verification conditions. It is important to note that the method
- requires \texttt{WHILE} loops to be fully annotated with invariants
- beforehand. Furthermore, only \emph{concrete} pieces of code are
- handled --- the underlying tactic fails ungracefully if supplied
- with meta-variables or parameters, for example.\<close>
+text \<open>We now load the \<^emph>\<open>original\<close> ML file for proof scripts and tactic
+ definition for the Hoare Verification Condition Generator (see @{file
+ "~~/src/HOL/Hoare/"}). As far as we are concerned here, the result is a
+ proof method \<open>hoare\<close>, which may be applied to a Hoare Logic assertion to
+ extract purely logical verification conditions. It is important to note
+ that the method requires \<^verbatim>\<open>WHILE\<close> loops to be fully annotated with
+ invariants beforehand. Furthermore, only \<^emph>\<open>concrete\<close> pieces of code are
+ handled --- the underlying tactic fails ungracefully if supplied with
+ meta-variables or parameters, for example.\<close>
lemma SkipRule: "p \<subseteq> q \<Longrightarrow> Valid p (Basic id) q"
by (auto simp add: Valid_def)
--- a/src/HOL/Isar_Examples/Hoare_Ex.thy Mon Nov 02 18:35:41 2015 +0100
+++ b/src/HOL/Isar_Examples/Hoare_Ex.thy Mon Nov 02 20:11:16 2015 +0100
@@ -6,9 +6,9 @@
subsection \<open>State spaces\<close>
-text \<open>First of all we provide a store of program variables that
- occur in any of the programs considered later. Slightly unexpected
- things may happen when attempting to work with undeclared variables.\<close>
+text \<open>First of all we provide a store of program variables that occur in any
+ of the programs considered later. Slightly unexpected things may happen
+ when attempting to work with undeclared variables.\<close>
record vars =
I :: nat
@@ -16,29 +16,28 @@
N :: nat
S :: nat
-text \<open>While all of our variables happen to have the same type,
- nothing would prevent us from working with many-sorted programs as
- well, or even polymorphic ones. Also note that Isabelle/HOL's
- extensible record types even provides simple means to extend the
- state space later.\<close>
+text \<open>While all of our variables happen to have the same type, nothing would
+ prevent us from working with many-sorted programs as well, or even
+ polymorphic ones. Also note that Isabelle/HOL's extensible record types
+ even provides simple means to extend the state space later.\<close>
subsection \<open>Basic examples\<close>
-text \<open>We look at few trivialities involving assignment and
- sequential composition, in order to get an idea of how to work with
- our formulation of Hoare Logic.\<close>
+text \<open>We look at few trivialities involving assignment and sequential
+ composition, in order to get an idea of how to work with our formulation
+ of Hoare Logic.\<close>
-text \<open>Using the basic @{text assign} rule directly is a bit
+text \<open>Using the basic \<open>assign\<close> rule directly is a bit
cumbersome.\<close>
lemma "\<turnstile> \<lbrace>\<acute>(N_update (\<lambda>_. (2 * \<acute>N))) \<in> \<lbrace>\<acute>N = 10\<rbrace>\<rbrace> \<acute>N := 2 * \<acute>N \<lbrace>\<acute>N = 10\<rbrace>"
by (rule assign)
-text \<open>Certainly we want the state modification already done, e.g.\
- by simplification. The \name{hoare} method performs the basic state
- update for us; we may apply the Simplifier afterwards to achieve
- ``obvious'' consequences as well.\<close>
+text \<open>Certainly we want the state modification already done, e.g.\ by
+ simplification. The \<open>hoare\<close> method performs the basic state update for us;
+ we may apply the Simplifier afterwards to achieve ``obvious'' consequences
+ as well.\<close>
lemma "\<turnstile> \<lbrace>True\<rbrace> \<acute>N := 10 \<lbrace>\<acute>N = 10\<rbrace>"
by hoare
@@ -67,8 +66,8 @@
\<lbrace>\<acute>M = b \<and> \<acute>N = a\<rbrace>"
by hoare simp
-text \<open>It is important to note that statements like the following one
- can only be proven for each individual program variable. Due to the
+text \<open>It is important to note that statements like the following one can
+ only be proven for each individual program variable. Due to the
extra-logical nature of record fields, we cannot formulate a theorem
relating record selectors and updates schematically.\<close>
@@ -84,9 +83,9 @@
oops
-text \<open>In the following assignments we make use of the consequence
- rule in order to achieve the intended precondition. Certainly, the
- \name{hoare} method is able to handle this case, too.\<close>
+text \<open>In the following assignments we make use of the consequence rule in
+ order to achieve the intended precondition. Certainly, the \<open>hoare\<close> method
+ is able to handle this case, too.\<close>
lemma "\<turnstile> \<lbrace>\<acute>M = \<acute>N\<rbrace> \<acute>M := \<acute>M + 1 \<lbrace>\<acute>M \<noteq> \<acute>N\<rbrace>"
proof -
@@ -114,10 +113,10 @@
subsection \<open>Multiplication by addition\<close>
-text \<open>We now do some basic examples of actual \texttt{WHILE}
- programs. This one is a loop for calculating the product of two
- natural numbers, by iterated addition. We first give detailed
- structured proof based on single-step Hoare rules.\<close>
+text \<open>We now do some basic examples of actual \<^verbatim>\<open>WHILE\<close> programs. This one is
+ a loop for calculating the product of two natural numbers, by iterated
+ addition. We first give detailed structured proof based on single-step
+ Hoare rules.\<close>
lemma
"\<turnstile> \<lbrace>\<acute>M = 0 \<and> \<acute>S = 0\<rbrace>
@@ -141,10 +140,10 @@
finally show ?thesis .
qed
-text \<open>The subsequent version of the proof applies the @{text hoare}
- method to reduce the Hoare statement to a purely logical problem
- that can be solved fully automatically. Note that we have to
- specify the \texttt{WHILE} loop invariant in the original statement.\<close>
+text \<open>The subsequent version of the proof applies the \<open>hoare\<close> method to
+ reduce the Hoare statement to a purely logical problem that can be solved
+ fully automatically. Note that we have to specify the \<^verbatim>\<open>WHILE\<close> loop
+ invariant in the original statement.\<close>
lemma
"\<turnstile> \<lbrace>\<acute>M = 0 \<and> \<acute>S = 0\<rbrace>
@@ -157,15 +156,15 @@
subsection \<open>Summing natural numbers\<close>
-text \<open>We verify an imperative program to sum natural numbers up to a
- given limit. First some functional definition for proper
- specification of the problem.\<close>
+text \<open>We verify an imperative program to sum natural numbers up to a given
+ limit. First some functional definition for proper specification of the
+ problem.
-text \<open>The following proof is quite explicit in the individual steps
- taken, with the \name{hoare} method only applied locally to take
- care of assignment and sequential composition. Note that we express
- intermediate proof obligation in pure logic, without referring to
- the state space.\<close>
+ \<^medskip>
+ The following proof is quite explicit in the individual steps taken, with
+ the \<open>hoare\<close> method only applied locally to take care of assignment and
+ sequential composition. Note that we express intermediate proof obligation
+ in pure logic, without referring to the state space.\<close>
theorem
"\<turnstile> \<lbrace>True\<rbrace>
@@ -203,9 +202,8 @@
finally show ?thesis .
qed
-text \<open>The next version uses the @{text hoare} method, while still
- explaining the resulting proof obligations in an abstract,
- structured manner.\<close>
+text \<open>The next version uses the \<open>hoare\<close> method, while still explaining the
+ resulting proof obligations in an abstract, structured manner.\<close>
theorem
"\<turnstile> \<lbrace>True\<rbrace>
@@ -230,8 +228,8 @@
qed
qed
-text \<open>Certainly, this proof may be done fully automatic as well,
- provided that the invariant is given beforehand.\<close>
+text \<open>Certainly, this proof may be done fully automatic as well, provided
+ that the invariant is given beforehand.\<close>
theorem
"\<turnstile> \<lbrace>True\<rbrace>
@@ -248,8 +246,8 @@
subsection \<open>Time\<close>
-text \<open>A simple embedding of time in Hoare logic: function @{text
- timeit} inserts an extra variable to keep track of the elapsed time.\<close>
+text \<open>A simple embedding of time in Hoare logic: function \<open>timeit\<close> inserts
+ an extra variable to keep track of the elapsed time.\<close>
record tstate = time :: nat
--- a/src/HOL/Isar_Examples/Knaster_Tarski.thy Mon Nov 02 18:35:41 2015 +0100
+++ b/src/HOL/Isar_Examples/Knaster_Tarski.thy Mon Nov 02 20:11:16 2015 +0100
@@ -14,30 +14,27 @@
subsection \<open>Prose version\<close>
text \<open>According to the textbook @{cite \<open>pages 93--94\<close> "davey-priestley"},
- the Knaster-Tarski fixpoint theorem is as
- follows.\footnote{We have dualized the argument, and tuned the
- notation a little bit.}
-
- \textbf{The Knaster-Tarski Fixpoint Theorem.} Let @{text L} be a
- complete lattice and @{text "f: L \<rightarrow> L"} an order-preserving map.
- Then @{text "\<Sqinter>{x \<in> L | f(x) \<le> x}"} is a fixpoint of @{text f}.
+ the Knaster-Tarski fixpoint theorem is as follows.\footnote{We have
+ dualized the argument, and tuned the notation a little bit.}
- \textbf{Proof.} Let @{text "H = {x \<in> L | f(x) \<le> x}"} and @{text "a =
- \<Sqinter>H"}. For all @{text "x \<in> H"} we have @{text "a \<le> x"}, so @{text
- "f(a) \<le> f(x) \<le> x"}. Thus @{text "f(a)"} is a lower bound of @{text
- H}, whence @{text "f(a) \<le> a"}. We now use this inequality to prove
- the reverse one (!) and thereby complete the proof that @{text a} is
- a fixpoint. Since @{text f} is order-preserving, @{text "f(f(a)) \<le>
- f(a)"}. This says @{text "f(a) \<in> H"}, so @{text "a \<le> f(a)"}.\<close>
+ \<^bold>\<open>The Knaster-Tarski Fixpoint Theorem.\<close> Let \<open>L\<close> be a complete lattice and
+ \<open>f: L \<rightarrow> L\<close> an order-preserving map. Then \<open>\<Sqinter>{x \<in> L | f(x) \<le> x}\<close> is a
+ fixpoint of \<open>f\<close>.
+
+ \<^bold>\<open>Proof.\<close> Let \<open>H = {x \<in> L | f(x) \<le> x}\<close> and \<open>a = \<Sqinter>H\<close>. For all \<open>x \<in> H\<close> we
+ have \<open>a \<le> x\<close>, so \<open>f(a) \<le> f(x) \<le> x\<close>. Thus \<open>f(a)\<close> is a lower bound of \<open>H\<close>,
+ whence \<open>f(a) \<le> a\<close>. We now use this inequality to prove the reverse one (!)
+ and thereby complete the proof that \<open>a\<close> is a fixpoint. Since \<open>f\<close> is
+ order-preserving, \<open>f(f(a)) \<le> f(a)\<close>. This says \<open>f(a) \<in> H\<close>, so \<open>a \<le> f(a)\<close>.\<close>
subsection \<open>Formal versions\<close>
-text \<open>The Isar proof below closely follows the original
- presentation. Virtually all of the prose narration has been
- rephrased in terms of formal Isar language elements. Just as many
- textbook-style proofs, there is a strong bias towards forward proof,
- and several bends in the course of reasoning.\<close>
+text \<open>The Isar proof below closely follows the original presentation.
+ Virtually all of the prose narration has been rephrased in terms of formal
+ Isar language elements. Just as many textbook-style proofs, there is a
+ strong bias towards forward proof, and several bends in the course of
+ reasoning.\<close>
theorem Knaster_Tarski:
fixes f :: "'a::complete_lattice \<Rightarrow> 'a"
@@ -67,15 +64,15 @@
qed
qed
-text \<open>Above we have used several advanced Isar language elements,
- such as explicit block structure and weak assumptions. Thus we have
- mimicked the particular way of reasoning of the original text.
+text \<open>Above we have used several advanced Isar language elements, such as
+ explicit block structure and weak assumptions. Thus we have mimicked the
+ particular way of reasoning of the original text.
- In the subsequent version the order of reasoning is changed to
- achieve structured top-down decomposition of the problem at the
- outer level, while only the inner steps of reasoning are done in a
- forward manner. We are certainly more at ease here, requiring only
- the most basic features of the Isar language.\<close>
+ In the subsequent version the order of reasoning is changed to achieve
+ structured top-down decomposition of the problem at the outer level, while
+ only the inner steps of reasoning are done in a forward manner. We are
+ certainly more at ease here, requiring only the most basic features of the
+ Isar language.\<close>
theorem Knaster_Tarski':
fixes f :: "'a::complete_lattice \<Rightarrow> 'a"
--- a/src/HOL/Isar_Examples/Mutilated_Checkerboard.thy Mon Nov 02 18:35:41 2015 +0100
+++ b/src/HOL/Isar_Examples/Mutilated_Checkerboard.thy Mon Nov 02 20:11:16 2015 +0100
@@ -9,8 +9,8 @@
imports Main
begin
-text \<open>The Mutilated Checker Board Problem, formalized inductively.
- See @{cite "paulson-mutilated-board"} for the original tactic script version.\<close>
+text \<open>The Mutilated Checker Board Problem, formalized inductively. See @{cite
+ "paulson-mutilated-board"} for the original tactic script version.\<close>
subsection \<open>Tilings\<close>
--- a/src/HOL/Isar_Examples/Nested_Datatype.thy Mon Nov 02 18:35:41 2015 +0100
+++ b/src/HOL/Isar_Examples/Nested_Datatype.thy Mon Nov 02 20:11:16 2015 +0100
@@ -20,7 +20,7 @@
lemmas subst_simps = subst_term.simps subst_term_list.simps
-text \<open>\medskip A simple lemma about composition of substitutions.\<close>
+text \<open>\<^medskip> A simple lemma about composition of substitutions.\<close>
lemma
"subst_term (subst_term f1 \<circ> f2) t =
--- a/src/HOL/Isar_Examples/Peirce.thy Mon Nov 02 18:35:41 2015 +0100
+++ b/src/HOL/Isar_Examples/Peirce.thy Mon Nov 02 20:11:16 2015 +0100
@@ -8,16 +8,15 @@
imports Main
begin
-text \<open>We consider Peirce's Law: $((A \impl B) \impl A) \impl A$.
- This is an inherently non-intuitionistic statement, so its proof
- will certainly involve some form of classical contradiction.
+text \<open>We consider Peirce's Law: \<open>((A \<longrightarrow> B) \<longrightarrow> A) \<longrightarrow> A\<close>. This is an inherently
+ non-intuitionistic statement, so its proof will certainly involve some
+ form of classical contradiction.
- The first proof is again a well-balanced combination of plain
- backward and forward reasoning. The actual classical step is where
- the negated goal may be introduced as additional assumption. This
- eventually leads to a contradiction.\footnote{The rule involved
- there is negation elimination; it holds in intuitionistic logic as
- well.}\<close>
+ The first proof is again a well-balanced combination of plain backward and
+ forward reasoning. The actual classical step is where the negated goal may
+ be introduced as additional assumption. This eventually leads to a
+ contradiction.\footnote{The rule involved there is negation elimination;
+ it holds in intuitionistic logic as well.}\<close>
theorem "((A \<longrightarrow> B) \<longrightarrow> A) \<longrightarrow> A"
proof
@@ -34,19 +33,17 @@
qed
qed
-text \<open>In the subsequent version the reasoning is rearranged by means
- of ``weak assumptions'' (as introduced by \isacommand{presume}).
- Before assuming the negated goal $\neg A$, its intended consequence
- $A \impl B$ is put into place in order to solve the main problem.
- Nevertheless, we do not get anything for free, but have to establish
- $A \impl B$ later on. The overall effect is that of a logical
- \emph{cut}.
+text \<open>In the subsequent version the reasoning is rearranged by means of
+ ``weak assumptions'' (as introduced by \isacommand{presume}). Before
+ assuming the negated goal \<open>\<not> A\<close>, its intended consequence \<open>A \<longrightarrow> B\<close> is put
+ into place in order to solve the main problem. Nevertheless, we do not get
+ anything for free, but have to establish \<open>A \<longrightarrow> B\<close> later on. The overall
+ effect is that of a logical \<^emph>\<open>cut\<close>.
- Technically speaking, whenever some goal is solved by
- \isacommand{show} in the context of weak assumptions then the latter
- give rise to new subgoals, which may be established separately. In
- contrast, strong assumptions (as introduced by \isacommand{assume})
- are solved immediately.\<close>
+ Technically speaking, whenever some goal is solved by \isacommand{show} in
+ the context of weak assumptions then the latter give rise to new subgoals,
+ which may be established separately. In contrast, strong assumptions (as
+ introduced by \isacommand{assume}) are solved immediately.\<close>
theorem "((A \<longrightarrow> B) \<longrightarrow> A) \<longrightarrow> A"
proof
@@ -65,21 +62,20 @@
qed
qed
-text \<open>Note that the goals stemming from weak assumptions may be even
- left until qed time, where they get eventually solved ``by
- assumption'' as well. In that case there is really no fundamental
- difference between the two kinds of assumptions, apart from the
- order of reducing the individual parts of the proof configuration.
+text \<open>Note that the goals stemming from weak assumptions may be even left
+ until qed time, where they get eventually solved ``by assumption'' as
+ well. In that case there is really no fundamental difference between the
+ two kinds of assumptions, apart from the order of reducing the individual
+ parts of the proof configuration.
- Nevertheless, the ``strong'' mode of plain assumptions is quite
- important in practice to achieve robustness of proof text
- interpretation. By forcing both the conclusion \emph{and} the
- assumptions to unify with the pending goal to be solved, goal
- selection becomes quite deterministic. For example, decomposition
- with rules of the ``case-analysis'' type usually gives rise to
- several goals that only differ in there local contexts. With strong
- assumptions these may be still solved in any order in a predictable
- way, while weak ones would quickly lead to great confusion,
- eventually demanding even some backtracking.\<close>
+ Nevertheless, the ``strong'' mode of plain assumptions is quite important
+ in practice to achieve robustness of proof text interpretation. By forcing
+ both the conclusion \<^emph>\<open>and\<close> the assumptions to unify with the pending goal
+ to be solved, goal selection becomes quite deterministic. For example,
+ decomposition with rules of the ``case-analysis'' type usually gives rise
+ to several goals that only differ in there local contexts. With strong
+ assumptions these may be still solved in any order in a predictable way,
+ while weak ones would quickly lead to great confusion, eventually
+ demanding even some backtracking.\<close>
end
--- a/src/HOL/Isar_Examples/Puzzle.thy Mon Nov 02 18:35:41 2015 +0100
+++ b/src/HOL/Isar_Examples/Puzzle.thy Mon Nov 02 20:11:16 2015 +0100
@@ -8,9 +8,8 @@
Original pen-and-paper proof due to Herbert Ehler; Isabelle tactic
script by Tobias Nipkow.}\<close>
-text \<open>\textbf{Problem.} Given some function $f\colon \Nat \to \Nat$
- such that $f \ap (f \ap n) < f \ap (\idt{Suc} \ap n)$ for all $n$.
- Demonstrate that $f$ is the identity.\<close>
+text \<open>\<^bold>\<open>Problem.\<close> Given some function \<open>f: \<nat> \<rightarrow> \<nat>\<close> such that
+ \<open>f (f n) < f (Suc n)\<close> for all \<open>n\<close>. Demonstrate that \<open>f\<close> is the identity.\<close>
theorem
assumes f_ax: "\<And>n. f (f n) < f (Suc n)"
--- a/src/HOL/Isar_Examples/Summation.thy Mon Nov 02 18:35:41 2015 +0100
+++ b/src/HOL/Isar_Examples/Summation.thy Mon Nov 02 20:11:16 2015 +0100
@@ -9,16 +9,16 @@
begin
text \<open>Subsequently, we prove some summation laws of natural numbers
- (including odds, squares, and cubes). These examples demonstrate
- how plain natural deduction (including induction) may be combined
- with calculational proof.\<close>
+ (including odds, squares, and cubes). These examples demonstrate how plain
+ natural deduction (including induction) may be combined with calculational
+ proof.\<close>
subsection \<open>Summation laws\<close>
-text \<open>The sum of natural numbers $0 + \cdots + n$ equals $n \times
- (n + 1)/2$. Avoiding formal reasoning about division we prove this
- equation multiplied by $2$.\<close>
+text \<open>The sum of natural numbers \<open>0 + \<cdots> + n\<close> equals \<open>n \<times> (n + 1)/2\<close>.
+ Avoiding formal reasoning about division we prove this equation multiplied
+ by \<open>2\<close>.\<close>
theorem sum_of_naturals:
"2 * (\<Sum>i::nat=0..n. i) = n * (n + 1)"
@@ -35,47 +35,39 @@
by simp
qed
-text \<open>The above proof is a typical instance of mathematical
- induction. The main statement is viewed as some $\var{P} \ap n$
- that is split by the induction method into base case $\var{P} \ap
- 0$, and step case $\var{P} \ap n \Impl \var{P} \ap (\idt{Suc} \ap
- n)$ for arbitrary $n$.
+text \<open>The above proof is a typical instance of mathematical induction. The
+ main statement is viewed as some \<open>?P n\<close> that is split by the induction
+ method into base case \<open>?P 0\<close>, and step case \<open>?P n \<Longrightarrow> ?P (Suc n)\<close> for
+ arbitrary \<open>n\<close>.
- The step case is established by a short calculation in forward
- manner. Starting from the left-hand side $\var{S} \ap (n + 1)$ of
- the thesis, the final result is achieved by transformations
- involving basic arithmetic reasoning (using the Simplifier). The
- main point is where the induction hypothesis $\var{S} \ap n = n
- \times (n + 1)$ is introduced in order to replace a certain subterm.
- So the ``transitivity'' rule involved here is actual
- \emph{substitution}. Also note how the occurrence of ``\dots'' in
- the subsequent step documents the position where the right-hand side
- of the hypothesis got filled in.
+ The step case is established by a short calculation in forward manner.
+ Starting from the left-hand side \<open>?S (n + 1)\<close> of the thesis, the final
+ result is achieved by transformations involving basic arithmetic reasoning
+ (using the Simplifier). The main point is where the induction hypothesis
+ \<open>?S n = n \<times> (n + 1)\<close> is introduced in order to replace a certain subterm.
+ So the ``transitivity'' rule involved here is actual \<^emph>\<open>substitution\<close>. Also
+ note how the occurrence of ``\dots'' in the subsequent step documents the
+ position where the right-hand side of the hypothesis got filled in.
- \medskip A further notable point here is integration of calculations
- with plain natural deduction. This works so well in Isar for two
- reasons.
- \begin{enumerate}
-
- \item Facts involved in \isakeyword{also}~/ \isakeyword{finally}
- calculational chains may be just anything. There is nothing special
- about \isakeyword{have}, so the natural deduction element
- \isakeyword{assume} works just as well.
+ \<^medskip>
+ A further notable point here is integration of calculations with plain
+ natural deduction. This works so well in Isar for two reasons.
- \item There are two \emph{separate} primitives for building natural
- deduction contexts: \isakeyword{fix}~$x$ and
- \isakeyword{assume}~$A$. Thus it is possible to start reasoning
- with some new ``arbitrary, but fixed'' elements before bringing in
- the actual assumption. In contrast, natural deduction is
- occasionally formalized with basic context elements of the form
- $x:A$ instead.
+ \<^enum> Facts involved in \isakeyword{also}~/ \isakeyword{finally}
+ calculational chains may be just anything. There is nothing special
+ about \isakeyword{have}, so the natural deduction element
+ \isakeyword{assume} works just as well.
+
+ \<^enum> There are two \<^emph>\<open>separate\<close> primitives for building natural deduction
+ contexts: \isakeyword{fix}~\<open>x\<close> and \isakeyword{assume}~\<open>A\<close>. Thus it is
+ possible to start reasoning with some new ``arbitrary, but fixed''
+ elements before bringing in the actual assumption. In contrast, natural
+ deduction is occasionally formalized with basic context elements of the
+ form \<open>x:A\<close> instead.
- \end{enumerate}
-\<close>
-
-text \<open>\medskip We derive further summation laws for odds, squares,
- and cubes as follows. The basic technique of induction plus
- calculation is the same as before.\<close>
+ \<^medskip>
+ We derive further summation laws for odds, squares, and cubes as follows.
+ The basic technique of induction plus calculation is the same as before.\<close>
theorem sum_of_odds:
"(\<Sum>i::nat=0..<n. 2 * i + 1) = n^Suc (Suc 0)"
@@ -93,9 +85,8 @@
by simp
qed
-text \<open>Subsequently we require some additional tweaking of Isabelle
- built-in arithmetic simplifications, such as bringing in
- distributivity by hand.\<close>
+text \<open>Subsequently we require some additional tweaking of Isabelle built-in
+ arithmetic simplifications, such as bringing in distributivity by hand.\<close>
lemmas distrib = add_mult_distrib add_mult_distrib2
@@ -134,15 +125,13 @@
text \<open>Note that in contrast to older traditions of tactical proof
scripts, the structured proof applies induction on the original,
- unsimplified statement. This allows to state the induction cases
- robustly and conveniently. Simplification (or other automated)
- methods are then applied in terminal position to solve certain
- sub-problems completely.
+ unsimplified statement. This allows to state the induction cases robustly
+ and conveniently. Simplification (or other automated) methods are then
+ applied in terminal position to solve certain sub-problems completely.
- As a general rule of good proof style, automatic methods such as
- $\idt{simp}$ or $\idt{auto}$ should normally be never used as
- initial proof methods with a nested sub-proof to address the
- automatically produced situation, but only as terminal ones to solve
- sub-problems.\<close>
+ As a general rule of good proof style, automatic methods such as \<open>simp\<close> or
+ \<open>auto\<close> should normally be never used as initial proof methods with a
+ nested sub-proof to address the automatically produced situation, but only
+ as terminal ones to solve sub-problems.\<close>
end
--- a/src/HOL/Isar_Examples/document/root.tex Mon Nov 02 18:35:41 2015 +0100
+++ b/src/HOL/Isar_Examples/document/root.tex Mon Nov 02 20:11:16 2015 +0100
@@ -1,11 +1,22 @@
-\input{style}
+\documentclass[11pt,a4paper]{article}
+\usepackage[only,bigsqcap]{stmaryrd}
+\usepackage{ifthen,proof,amssymb,isabelle,isabellesym}
+\isabellestyle{it}
+\usepackage{pdfsetup}\urlstyle{rm}
+
+\renewcommand{\isacommand}[1]
+{\ifthenelse{\equal{sorry}{#1}}{$\;$\dummyproof}
+ {\ifthenelse{\equal{oops}{#1}}{$\vdots$}{\isakeyword{#1}}}}
+
+\newcommand{\DUMMYPROOF}{{\langle\mathit{proof}\rangle}}
+\newcommand{\dummyproof}{$\DUMMYPROOF$}
\hyphenation{Isabelle}
\begin{document}
\title{Miscellaneous Isabelle/Isar examples for Higher-Order Logic}
-\author{Markus Wenzel \\ \url{http://www.in.tum.de/~wenzelm/} \\[2ex]
+\author{Markus Wenzel \\[2ex]
With contributions by Gertrud Bauer and Tobias Nipkow}
\maketitle
--- a/src/HOL/Isar_Examples/document/style.tex Mon Nov 02 18:35:41 2015 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,38 +0,0 @@
-\documentclass[11pt,a4paper]{article}
-\usepackage[only,bigsqcap]{stmaryrd}
-\usepackage{ifthen,proof,amssymb,isabelle,isabellesym}
-\isabellestyle{it}
-\usepackage{pdfsetup}\urlstyle{rm}
-
-\renewcommand{\isacommand}[1]
-{\ifthenelse{\equal{sorry}{#1}}{$\;$\dummyproof}
- {\ifthenelse{\equal{oops}{#1}}{$\vdots$}{\isakeyword{#1}}}}
-
-\newcommand{\DUMMYPROOF}{{\langle\idt{proof}\rangle}}
-\newcommand{\dummyproof}{$\DUMMYPROOF$}
-
-\newcommand{\name}[1]{\textsl{#1}}
-
-\newcommand{\idt}[1]{{\mathord{\mathit{#1}}}}
-\newcommand{\var}[1]{{?\!\idt{#1}}}
-\DeclareMathSymbol{\dshsym}{\mathalpha}{letters}{"2D}
-\newcommand{\dsh}{\dshsym}
-
-\newcommand{\To}{\to}
-\newcommand{\dt}{{\mathpunct.}}
-\newcommand{\ap}{\mathbin{\!}}
-\newcommand{\lam}[1]{\mathop{\lambda} #1\dt\;}
-\newcommand{\all}[1]{\forall #1\dt\;}
-\newcommand{\ex}[1]{\exists #1\dt\;}
-\newcommand{\impl}{\to}
-\newcommand{\conj}{\land}
-\newcommand{\disj}{\lor}
-\newcommand{\Impl}{\Longrightarrow}
-
-\newcommand{\Nat}{\mathord{\mathrm{I}\mkern-3.8mu\mathrm{N}}}
-
-
-%%% Local Variables:
-%%% mode: latex
-%%% TeX-master: "root"
-%%% End:
--- a/src/HOL/Library/Lattice_Algebras.thy Mon Nov 02 18:35:41 2015 +0100
+++ b/src/HOL/Library/Lattice_Algebras.thy Mon Nov 02 20:11:16 2015 +0100
@@ -1,4 +1,4 @@
-(* Author: Steven Obua, TU Muenchen *)
+(* Author: Steven Obua, TU Muenchen *)
section \<open>Various algebraic structures combined with a lattice\<close>
@@ -224,7 +224,7 @@
proof -
from that have a: "inf (a + a) 0 = 0"
by (simp add: inf_commute inf_absorb1)
- have "inf a 0 + inf a 0 = inf (inf (a + a) 0) a" (is "?l=_")
+ have "inf a 0 + inf a 0 = inf (inf (a + a) 0) a" (is "?l = _")
by (simp add: add_sup_inf_distribs inf_aci)
then have "?l = 0 + inf a 0"
by (simp add: a, simp add: inf_commute)
@@ -619,4 +619,3 @@
qed
end
-
--- a/src/HOL/ROOT Mon Nov 02 18:35:41 2015 +0100
+++ b/src/HOL/ROOT Mon Nov 02 20:11:16 2015 +0100
@@ -647,7 +647,6 @@
document_files
"root.bib"
"root.tex"
- "style.tex"
session "HOL-Eisbach" in Eisbach = HOL +
description {*
--- a/src/Pure/PIDE/markup.ML Mon Nov 02 18:35:41 2015 +0100
+++ b/src/Pure/PIDE/markup.ML Mon Nov 02 20:11:16 2015 +0100
@@ -36,7 +36,7 @@
val language_prop: bool -> T
val language_ML: bool -> T
val language_SML: bool -> T
- val language_document: bool -> T
+ val language_document: {symbols: bool, delimited: bool} -> T
val language_antiquotation: T
val language_text: bool -> T
val language_rail: T
@@ -310,7 +310,8 @@
val language_prop = language' {name = "prop", symbols = true, antiquotes = false};
val language_ML = language' {name = "ML", symbols = false, antiquotes = true};
val language_SML = language' {name = "SML", symbols = false, antiquotes = false};
-val language_document = language' {name = "document", symbols = false, antiquotes = true};
+fun language_document {symbols, delimited} =
+ language' {name = "document", symbols = symbols, antiquotes = true} delimited;
val language_antiquotation =
language {name = "antiquotation", symbols = true, antiquotes = false, delimited = true};
val language_text = language' {name = "text", symbols = true, antiquotes = false};
--- a/src/Pure/PIDE/query_operation.scala Mon Nov 02 18:35:41 2015 +0100
+++ b/src/Pure/PIDE/query_operation.scala Mon Nov 02 20:11:16 2015 +0100
@@ -16,6 +16,26 @@
val RUNNING = Value("running")
val FINISHED = Value("finished")
}
+
+ object State
+ {
+ val empty: State = State()
+
+ def make(command: Command, query: List[String]): State =
+ State(instance = Document_ID.make().toString,
+ location = Some(command),
+ query = query,
+ status = Status.WAITING)
+ }
+
+ sealed case class State(
+ instance: String = Document_ID.none.toString,
+ location: Option[Command] = None,
+ query: List[String] = Nil,
+ update_pending: Boolean = false,
+ output: List[XML.Tree] = Nil,
+ status: Status.Value = Status.FINISHED,
+ exec_id: Document_ID.Exec = Document_ID.none)
}
class Query_Operation[Editor_Context](
@@ -26,37 +46,19 @@
consume_output: (Document.Snapshot, Command.Results, XML.Body) => Unit)
{
private val print_function = operation_name + "_query"
- private val instance = Document_ID.make().toString
/* implicit state -- owned by GUI thread */
- @volatile private var current_location: Option[Command] = None
- @volatile private var current_query: List[String] = Nil
- @volatile private var current_update_pending = false
- @volatile private var current_output: List[XML.Tree] = Nil
- @volatile private var current_status = Query_Operation.Status.FINISHED
- @volatile private var current_exec_id = Document_ID.none
-
- def get_location: Option[Command] = current_location
+ private val current_state = Synchronized(Query_Operation.State.empty)
- private def reset_state()
- {
- current_location = None
- current_query = Nil
- current_update_pending = false
- current_output = Nil
- current_status = Query_Operation.Status.FINISHED
- current_exec_id = Document_ID.none
- }
+ def get_location: Option[Command] = current_state.value.location
private def remove_overlay()
{
- current_location match {
- case None =>
- case Some(command) =>
- editor.remove_overlay(command, print_function, instance :: current_query)
- editor.flush()
+ val state = current_state.value
+ for (command <- state.location) {
+ editor.remove_overlay(command, print_function, state.instance :: state.query)
}
}
@@ -70,29 +72,31 @@
/* snapshot */
- val (snapshot, command_results, removed) =
- current_location match {
+ val state0 = current_state.value
+
+ val (snapshot, command_results, results, removed) =
+ state0.location match {
case Some(cmd) =>
val snapshot = editor.node_snapshot(cmd.node_name)
val command_results = snapshot.state.command_results(snapshot.version, cmd)
+ val results =
+ (for {
+ (_, elem @ XML.Elem(Markup(Markup.RESULT, props), _)) <- command_results.iterator
+ if props.contains((Markup.INSTANCE, state0.instance))
+ } yield elem).toList
val removed = !snapshot.version.nodes(cmd.node_name).commands.contains(cmd)
- (snapshot, command_results, removed)
+ (snapshot, command_results, results, removed)
case None =>
- (Document.Snapshot.init, Command.Results.empty, true)
+ (Document.Snapshot.init, Command.Results.empty, Nil, true)
}
- val results =
- (for {
- (_, elem @ XML.Elem(Markup(Markup.RESULT, props), _)) <- command_results.iterator
- if props.contains((Markup.INSTANCE, instance))
- } yield elem).toList
/* resolve sendback: static command id */
def resolve_sendback(body: XML.Body): XML.Body =
{
- current_location match {
+ state0.location match {
case None => body
case Some(command) =>
def resolve(body: XML.Body): XML.Body =
@@ -101,7 +105,7 @@
case XML.Elem(Markup(Markup.SENDBACK, props), b) =>
val props1 =
props.map({
- case (Markup.ID, Properties.Value.Long(id)) if id == current_exec_id =>
+ case (Markup.ID, Properties.Value.Long(id)) if id == state0.exec_id =>
(Markup.ID, Properties.Value.Long(command.id))
case p => p
})
@@ -137,27 +141,27 @@
get_status(Markup.RUNNING, Query_Operation.Status.RUNNING) getOrElse
Query_Operation.Status.WAITING
+
+ /* state update */
+
if (new_status == Query_Operation.Status.RUNNING)
results.collectFirst(
{
case XML.Elem(Markup(_, Position.Id(id)), List(elem: XML.Elem))
if elem.name == Markup.RUNNING => id
- }).foreach(id => current_exec_id = id)
-
-
- /* state update */
+ }).foreach(id => current_state.change(_.copy(exec_id = id)))
- if (current_output != new_output || current_status != new_status) {
+ if (state0.output != new_output || state0.status != new_status) {
if (snapshot.is_outdated)
- current_update_pending = true
+ current_state.change(_.copy(update_pending = true))
else {
- current_update_pending = false
- if (current_output != new_output && !removed) {
- current_output = new_output
+ current_state.change(_.copy(update_pending = false))
+ if (state0.output != new_output && !removed) {
+ current_state.change(_.copy(output = new_output))
consume_output(snapshot, command_results, new_output)
}
- if (current_status != new_status) {
- current_status = new_status
+ if (state0.status != new_status) {
+ current_state.change(_.copy(status = new_status))
consume_status(new_status)
if (new_status == Query_Operation.Status.FINISHED)
remove_overlay()
@@ -170,7 +174,7 @@
/* query operations */
def cancel_query(): Unit =
- GUI_Thread.require { editor.session.cancel_exec(current_exec_id) }
+ GUI_Thread.require { editor.session.cancel_exec(current_state.value.exec_id) }
def apply_query(query: List[String])
{
@@ -179,19 +183,18 @@
editor.current_node_snapshot(editor_context) match {
case Some(snapshot) =>
remove_overlay()
- reset_state()
+ current_state.change(_ => Query_Operation.State.empty)
consume_output(Document.Snapshot.init, Command.Results.empty, Nil)
if (!snapshot.is_outdated) {
editor.current_command(editor_context, snapshot) match {
case Some(command) =>
- current_location = Some(command)
- current_query = query
- current_status = Query_Operation.Status.WAITING
- editor.insert_overlay(command, print_function, instance :: query)
+ val state = Query_Operation.State.make(command, query)
+ current_state.change(_ => state)
+ editor.insert_overlay(command, print_function, state.instance :: query)
case None =>
}
}
- consume_status(current_status)
+ consume_status(current_state.value.status)
editor.flush()
case None =>
}
@@ -201,8 +204,9 @@
{
GUI_Thread.require {}
+ val state = current_state.value
for {
- command <- current_location
+ command <- state.location
snapshot = editor.node_snapshot(command.node_name)
link <- editor.hyperlink_command(true, snapshot, command)
} link.follow(editor_context)
@@ -214,10 +218,11 @@
private val main =
Session.Consumer[Session.Commands_Changed](getClass.getName) {
case changed =>
- current_location match {
+ val state = current_state.value
+ state.location match {
case Some(command)
- if current_update_pending ||
- (current_status != Query_Operation.Status.FINISHED &&
+ if state.update_pending ||
+ (state.status != Query_Operation.Status.FINISHED &&
changed.commands.contains(command)) =>
GUI_Thread.later { content_update() }
case _ =>
@@ -231,8 +236,8 @@
def deactivate() {
editor.session.commands_changed -= main
remove_overlay()
- reset_state()
+ current_state.change(_ => Query_Operation.State.empty)
consume_output(Document.Snapshot.init, Command.Results.empty, Nil)
- consume_status(current_status)
+ consume_status(Query_Operation.Status.FINISHED)
}
}
--- a/src/Pure/Thy/thy_info.scala Mon Nov 02 18:35:41 2015 +0100
+++ b/src/Pure/Thy/thy_info.scala Mon Nov 02 20:11:16 2015 +0100
@@ -35,23 +35,25 @@
object Dependencies
{
- val empty = new Dependencies(Nil, Nil, Multi_Map.empty, Multi_Map.empty)
+ val empty = new Dependencies(Nil, Nil, Set.empty, Multi_Map.empty, Multi_Map.empty)
}
final class Dependencies private(
rev_deps: List[Thy_Info.Dep],
val keywords: Thy_Header.Keywords,
+ val seen: Set[Document.Node.Name],
val seen_names: Multi_Map[String, Document.Node.Name],
val seen_positions: Multi_Map[String, Position.T])
{
def :: (dep: Thy_Info.Dep): Dependencies =
new Dependencies(dep :: rev_deps, dep.header.keywords ::: keywords,
- seen_names, seen_positions)
+ seen, seen_names, seen_positions)
def + (thy: (Document.Node.Name, Position.T)): Dependencies =
{
val (name, pos) = thy
new Dependencies(rev_deps, keywords,
+ seen + name,
seen_names + (name.theory -> name),
seen_positions + (name.theory -> pos))
}
@@ -102,15 +104,13 @@
required: Dependencies, thy: (Document.Node.Name, Position.T)): Dependencies =
{
val (name, require_pos) = thy
- val theory = name.theory
def message: String =
- "The error(s) above occurred for theory " + quote(theory) +
+ "The error(s) above occurred for theory " + quote(name.theory) +
required_by(initiators) + Position.here(require_pos)
val required1 = required + thy
- if (required.seen_names.isDefinedAt(theory) || resources.loaded_theories(theory))
- required1
+ if (required.seen(name) || resources.loaded_theories(name.theory)) required1
else {
try {
if (initiators.contains(name)) error(cycle_msg(initiators))
--- a/src/Pure/Thy/thy_output.ML Mon Nov 02 18:35:41 2015 +0100
+++ b/src/Pure/Thy/thy_output.ML Mon Nov 02 20:11:16 2015 +0100
@@ -196,7 +196,10 @@
fun output_text state {markdown} source =
let
val pos = Input.pos_of source;
- val _ = Position.report pos (Markup.language_document (Input.is_delimited source));
+ val _ =
+ Position.report pos
+ (Markup.language_document
+ {symbols = Options.default_bool "document_symbols", delimited = Input.is_delimited source});
val syms = Input.source_explode source;
val output_antiquote = eval_antiquote state #> Symbol.explode #> Latex.output_ctrl_symbols;
--- a/src/Tools/jEdit/src/document_model.scala Mon Nov 02 18:35:41 2015 +0100
+++ b/src/Tools/jEdit/src/document_model.scala Mon Nov 02 20:11:16 2015 +0100
@@ -255,6 +255,9 @@
reset_blob()
reset_bibtex()
+ for (doc_view <- PIDE.document_views(buffer))
+ doc_view.rich_text_area.active_reset()
+
if (clear) {
pending_clear = true
pending.clear
--- a/src/Tools/jEdit/src/jedit_editor.scala Mon Nov 02 18:35:41 2015 +0100
+++ b/src/Tools/jEdit/src/jedit_editor.scala Mon Nov 02 20:11:16 2015 +0100
@@ -41,7 +41,7 @@
name => (name, Document.Node.no_perspective_text))
val edits = models.flatMap(_.flushed_edits(doc_blobs)) ::: removed_perspective
- if (edits.nonEmpty) session.update(doc_blobs, edits)
+ session.update(doc_blobs, edits)
}
private val delay_flush =