--- a/src/HOL/Isar_Examples/Hoare.thy Mon Nov 02 11:43:02 2015 +0100
+++ b/src/HOL/Isar_Examples/Hoare.thy Mon Nov 02 13:58:19 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)