--- a/doc-src/TutorialI/CTL/Base.thy Thu Jan 11 11:47:57 2001 +0100
+++ b/doc-src/TutorialI/CTL/Base.thy Thu Jan 11 12:12:01 2001 +0100
@@ -1,19 +1,22 @@
(*<*)theory Base = Main:(*>*)
-section{*Case study: Verified model checking*}
+section{*Case Study: Verified Model Checking*}
text{*\label{sec:VMC}
-Model checking is a very popular technique for the verification of finite
+This chapter ends with a case study concerning model checking for
+Computation Tree Logic (CTL), a temporal logic.
+Model checking is a popular technique for the verification of finite
state systems (implementations) with respect to temporal logic formulae
-(specifications) \cite{ClarkeGP-book,Huth-Ryan-book}. Its foundations are completely set theoretic
-and this section will explore them a little in HOL\@. This is done in two steps: first
+(specifications) \cite{ClarkeGP-book,Huth-Ryan-book}. Its foundations are set theoretic
+and this section will explore them in HOL\@. This is done in two steps. First
we consider a simple modal logic called propositional dynamic
-logic (PDL) which we then extend to the temporal logic CTL used in many real
+logic (PDL), which we then extend to the temporal logic CTL, which is
+used in many real
model checkers. In each case we give both a traditional semantics (@{text \<Turnstile>}) and a
recursive function @{term mc} that maps a formula into the set of all states of
the system where the formula is valid. If the system has a finite number of
-states, @{term mc} is directly executable, i.e.\ a model checker, albeit not a
-very efficient one. The main proof obligation is to show that the semantics
+states, @{term mc} is directly executable: it is a model checker, albeit an
+inefficient one. The main proof obligation is to show that the semantics
and the model checker agree.
\underscoreon
@@ -63,7 +66,7 @@
course it would have been more generic to make @{typ state} a type
parameter of everything but declaring @{typ state} globally as above
reduces clutter. Similarly we declare an arbitrary but fixed
-transition system, i.e.\ relation between states:
+transition system, i.e.\ a relation between states:
*}
consts M :: "(state \<times> state)set";
--- a/doc-src/TutorialI/CTL/CTL.thy Thu Jan 11 11:47:57 2001 +0100
+++ b/doc-src/TutorialI/CTL/CTL.thy Thu Jan 11 12:12:01 2001 +0100
@@ -1,11 +1,11 @@
(*<*)theory CTL = Base:;(*>*)
-subsection{*Computation tree logic---CTL*};
+subsection{*Computation Tree Logic---CTL*};
text{*\label{sec:CTL}
-The semantics of PDL only needs transitive reflexive closure.
-Let us now be a bit more adventurous and introduce a new temporal operator
-that goes beyond transitive reflexive closure. We extend the datatype
+The semantics of PDL only needs reflexive transitive closure.
+Let us be adventurous and introduce a more expressive temporal operator.
+We extend the datatype
@{text formula} by a new constructor
*};
(*<*)
@@ -27,7 +27,7 @@
text{*\noindent
This definition allows a very succinct statement of the semantics of @{term AF}:
-\footnote{Do not be mislead: neither datatypes nor recursive functions can be
+\footnote{Do not be misled: neither datatypes nor recursive functions can be
extended by new constructors or equations. This is just a trick of the
presentation. In reality one has to define a new datatype and a new function.}
*};
@@ -52,7 +52,7 @@
"af A T \<equiv> A \<union> {s. \<forall>t. (s, t) \<in> M \<longrightarrow> t \<in> T}";
text{*\noindent
-Now we define @{term "mc(AF f)"} as the least set @{term T} that contains
+Now we define @{term "mc(AF f)"} as the least set @{term T} that includes
@{term"mc f"} and all states all of whose direct successors are in @{term T}:
*};
(*<*)
@@ -97,9 +97,9 @@
by(blast);
(*>*)
text{*
-All we need to prove now is that @{term mc} and @{text"\<Turnstile>"}
-agree for @{term AF}, i.e.\ that @{prop"mc(AF f) = {s. s \<Turnstile>
-AF f}"}. This time we prove the two containments separately, starting
+All we need to prove now is @{prop"mc(AF f) = {s. s \<Turnstile> AF f}"}, which states
+that @{term mc} and @{text"\<Turnstile>"} agree for @{term AF}\@.
+This time we prove the two inclusions separately, starting
with the easy one:
*};
@@ -145,7 +145,7 @@
text{*
-The opposite containment is proved by contradiction: if some state
+The opposite inclusion is proved by contradiction: if some state
@{term s} is not in @{term"lfp(af A)"}, then we can construct an
infinite @{term A}-avoiding path starting from @{term s}. The reason is
that by unfolding @{term lfp} we find that if @{term s} is not in
@@ -154,7 +154,8 @@
A)"}. Iterating this argument yields the promised infinite
@{term A}-avoiding path. Let us formalize this sketch.
-The one-step argument in the above sketch
+The one-step argument in the sketch above
+is proved by a variant of contraposition:
*};
lemma not_in_lfp_afD:
@@ -165,8 +166,7 @@
done;
text{*\noindent
-is proved by a variant of contraposition:
-assume the negation of the conclusion and prove @{term"s : lfp(af A)"}.
+We assume the negation of the conclusion and prove @{term"s : lfp(af A)"}.
Unfolding @{term lfp} once and
simplifying with the definition of @{term af} finishes the proof.
@@ -183,8 +183,8 @@
Element @{term"n+1"} on this path is some arbitrary successor
@{term t} of element @{term n} such that @{term"P t"} holds. Remember that @{text"SOME t. R t"}
is some arbitrary but fixed @{term t} such that @{prop"R t"} holds (see \S\ref{sec:SOME}). Of
-course, such a @{term t} may in general not exist, but that is of no
-concern to us since we will only use @{term path} in such cases where a
+course, such a @{term t} need not exist, but that is of no
+concern to us since we will only use @{term path} when a
suitable @{term t} does exist.
Let us show that if each state @{term s} that satisfies @{term P}
@@ -266,15 +266,14 @@
done;
text{*
-Function @{term path} has fulfilled its purpose now and can be forgotten
-about. It was merely defined to provide the witness in the proof of the
+Function @{term path} has fulfilled its purpose now and can be forgotten.
+It was merely defined to provide the witness in the proof of the
@{thm[source]infinity_lemma}. Aficionados of minimal proofs might like to know
that we could have given the witness without having to define a new function:
the term
@{term[display]"nat_rec s (\<lambda>n t. SOME u. (t,u)\<in>M \<and> P u)"}
is extensionally equal to @{term"path s P"},
-where @{term nat_rec} is the predefined primitive recursor on @{typ nat}, whose defining
-equations we omit.
+where @{term nat_rec} is the predefined primitive recursor on @{typ nat}.
*};
(*<*)
lemma infinity_lemma:
@@ -329,8 +328,8 @@
done;
text{*
-If you found the above proofs somewhat complicated we recommend you read
-\S\ref{sec:CTL-revisited} where we shown how inductive definitions lead to
+If you find these proofs too complicated, we recommend that you read
+\S\ref{sec:CTL-revisited}, where we show how inductive definitions lead to
simpler arguments.
The main theorem is proved as for PDL, except that we also derive the
@@ -345,8 +344,8 @@
text{*
-The above language is not quite CTL\@. The latter also includes an
-until-operator @{term"EU f g"} with semantics ``there exist a path
+The language defined above is not quite CTL\@. The latter also includes an
+until-operator @{term"EU f g"} with semantics ``there exists a path
where @{term f} is true until @{term g} becomes true''. With the help
of an auxiliary function
*}
@@ -375,7 +374,7 @@
%{text[display]"| EU formula formula E[_ U _]"}
%which enables you to read and write {text"E[f U g]"} instead of {term"EU f g"}.
\end{exercise}
-For more CTL exercises see, for example, \cite{Huth-Ryan-book}.
+For more CTL exercises see, for example, Huth and Ryan \cite{Huth-Ryan-book}.
*}
(*<*)
@@ -457,8 +456,11 @@
Let us close this section with a few words about the executability of our model checkers.
It is clear that if all sets are finite, they can be represented as lists and the usual
set operations are easily implemented. Only @{term lfp} requires a little thought.
-Fortunately the HOL library proves that in the case of finite sets and a monotone @{term F},
-@{term"lfp F"} can be computed by iterated application of @{term F} to @{term"{}"} until
+\REMARK{you had `in the library' but I assume you meant it was a
+built in lemma. Do we give its name?}
+Fortunately, Isabelle/HOL provides a theorem stating that
+in the case of finite sets and a monotone @{term F},
+the value of @{term"lfp F"} can be computed by iterated application of @{term F} to~@{term"{}"} until
a fixed point is reached. It is actually possible to generate executable functional programs
from HOL definitions, but that is beyond the scope of the tutorial.
*}
--- a/doc-src/TutorialI/CTL/PDL.thy Thu Jan 11 11:47:57 2001 +0100
+++ b/doc-src/TutorialI/CTL/PDL.thy Thu Jan 11 12:12:01 2001 +0100
@@ -1,12 +1,12 @@
(*<*)theory PDL = Base:(*>*)
-subsection{*Propositional dynamic logic---PDL*}
+subsection{*Propositional Dynamic Logic---PDL*}
text{*\index{PDL|(}
The formulae of PDL are built up from atomic propositions via the customary
propositional connectives of negation and conjunction and the two temporal
connectives @{text AX} and @{text EF}. Since formulae are essentially
-(syntax) trees, they are naturally modelled as a datatype:
+syntax trees, they are naturally modelled as a datatype:
*}
datatype formula = Atom atom
@@ -17,8 +17,7 @@
text{*\noindent
This is almost the same as in the boolean expression case study in
-\S\ref{sec:boolex}, except that what used to be called @{text Var} is now
-called @{term Atom}.
+\S\ref{sec:boolex}.
The meaning of these formulae is given by saying which formula is true in
which state:
@@ -27,9 +26,10 @@
consts valid :: "state \<Rightarrow> formula \<Rightarrow> bool" ("(_ \<Turnstile> _)" [80,80] 80)
text{*\noindent
-The concrete syntax annotation allows us to write @{term"s \<Turnstile> f"} instead of
-@{text"valid s f"}.
+The syntax annotation allows us to write @{term"s \<Turnstile> f"} instead of
+\hbox{@{text"valid s f"}}.
+\smallskip
The definition of @{text"\<Turnstile>"} is by recursion over the syntax:
*}
@@ -44,7 +44,7 @@
The first three equations should be self-explanatory. The temporal formula
@{term"AX f"} means that @{term f} is true in all next states whereas
@{term"EF f"} means that there exists some future state in which @{term f} is
-true. The future is expressed via @{text"\<^sup>*"}, the transitive reflexive
+true. The future is expressed via @{text"\<^sup>*"}, the reflexive transitive
closure. Because of reflexivity, the future includes the present.
Now we come to the model checker itself. It maps a formula into the set of
@@ -58,12 +58,12 @@
"mc(Neg f) = -mc f"
"mc(And f g) = mc f \<inter> mc g"
"mc(AX f) = {s. \<forall>t. (s,t) \<in> M \<longrightarrow> t \<in> mc f}"
-"mc(EF f) = lfp(\<lambda>T. mc f \<union> M\<inverse> `` T)"
+"mc(EF f) = lfp(\<lambda>T. mc f \<union> (M\<inverse> `` T))"
text{*\noindent
Only the equation for @{term EF} deserves some comments. Remember that the
postfix @{text"\<inverse>"} and the infix @{text"``"} are predefined and denote the
-converse of a relation and the application of a relation to a set. Thus
+converse of a relation and the image of a set under a relation. Thus
@{term "M\<inverse> `` T"} is the set of all predecessors of @{term T} and the least
fixed point (@{term lfp}) of @{term"\<lambda>T. mc f \<union> M\<inverse> `` T"} is the least set
@{term T} containing @{term"mc f"} and all predecessors of @{term T}. If you
@@ -72,26 +72,25 @@
will be proved in a moment.
First we prove monotonicity of the function inside @{term lfp}
+in order to make sure it really has a least fixed point.
*}
-lemma mono_ef: "mono(\<lambda>T. A \<union> M\<inverse> `` T)"
+lemma mono_ef: "mono(\<lambda>T. A \<union> (M\<inverse> `` T))"
apply(rule monoI)
apply blast
done
text{*\noindent
-in order to make sure it really has a least fixed point.
-
Now we can relate model checking and semantics. For the @{text EF} case we need
a separate lemma:
*}
lemma EF_lemma:
- "lfp(\<lambda>T. A \<union> M\<inverse> `` T) = {s. \<exists>t. (s,t) \<in> M\<^sup>* \<and> t \<in> A}"
+ "lfp(\<lambda>T. A \<union> (M\<inverse> `` T)) = {s. \<exists>t. (s,t) \<in> M\<^sup>* \<and> t \<in> A}"
txt{*\noindent
The equality is proved in the canonical fashion by proving that each set
-contains the other; the containment is shown pointwise:
+includes the other; the inclusion is shown pointwise:
*}
apply(rule equalityI);
@@ -122,7 +121,7 @@
apply(blast intro: rtrancl_trans);
txt{*
-We now return to the second set containment subgoal, which is again proved
+We now return to the second set inclusion subgoal, which is again proved
pointwise:
*}
--- a/doc-src/TutorialI/CTL/document/Base.tex Thu Jan 11 11:47:57 2001 +0100
+++ b/doc-src/TutorialI/CTL/document/Base.tex Thu Jan 11 12:12:01 2001 +0100
@@ -2,22 +2,25 @@
\begin{isabellebody}%
\def\isabellecontext{Base}%
%
-\isamarkupsection{Case study: Verified model checking%
+\isamarkupsection{Case Study: Verified Model Checking%
}
%
\begin{isamarkuptext}%
\label{sec:VMC}
-Model checking is a very popular technique for the verification of finite
+This chapter ends with a case study concerning model checking for
+Computation Tree Logic (CTL), a temporal logic.
+Model checking is a popular technique for the verification of finite
state systems (implementations) with respect to temporal logic formulae
-(specifications) \cite{ClarkeGP-book,Huth-Ryan-book}. Its foundations are completely set theoretic
-and this section will explore them a little in HOL\@. This is done in two steps: first
+(specifications) \cite{ClarkeGP-book,Huth-Ryan-book}. Its foundations are set theoretic
+and this section will explore them in HOL\@. This is done in two steps. First
we consider a simple modal logic called propositional dynamic
-logic (PDL) which we then extend to the temporal logic CTL used in many real
+logic (PDL), which we then extend to the temporal logic CTL, which is
+used in many real
model checkers. In each case we give both a traditional semantics (\isa{{\isasymTurnstile}}) and a
recursive function \isa{mc} that maps a formula into the set of all states of
the system where the formula is valid. If the system has a finite number of
-states, \isa{mc} is directly executable, i.e.\ a model checker, albeit not a
-very efficient one. The main proof obligation is to show that the semantics
+states, \isa{mc} is directly executable: it is a model checker, albeit an
+inefficient one. The main proof obligation is to show that the semantics
and the model checker agree.
\underscoreon
@@ -66,7 +69,7 @@
course it would have been more generic to make \isa{state} a type
parameter of everything but declaring \isa{state} globally as above
reduces clutter. Similarly we declare an arbitrary but fixed
-transition system, i.e.\ relation between states:%
+transition system, i.e.\ a relation between states:%
\end{isamarkuptext}%
\isacommand{consts}\ M\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}state\ {\isasymtimes}\ state{\isacharparenright}set{\isachardoublequote}%
\begin{isamarkuptext}%
--- a/doc-src/TutorialI/CTL/document/CTL.tex Thu Jan 11 11:47:57 2001 +0100
+++ b/doc-src/TutorialI/CTL/document/CTL.tex Thu Jan 11 12:12:01 2001 +0100
@@ -2,14 +2,14 @@
\begin{isabellebody}%
\def\isabellecontext{CTL}%
%
-\isamarkupsubsection{Computation tree logic---CTL%
+\isamarkupsubsection{Computation Tree Logic---CTL%
}
%
\begin{isamarkuptext}%
\label{sec:CTL}
-The semantics of PDL only needs transitive reflexive closure.
-Let us now be a bit more adventurous and introduce a new temporal operator
-that goes beyond transitive reflexive closure. We extend the datatype
+The semantics of PDL only needs reflexive transitive closure.
+Let us be adventurous and introduce a more expressive temporal operator.
+We extend the datatype
\isa{formula} by a new constructor%
\end{isamarkuptext}%
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharbar}\ AF\ formula%
@@ -24,7 +24,7 @@
\begin{isamarkuptext}%
\noindent
This definition allows a very succinct statement of the semantics of \isa{AF}:
-\footnote{Do not be mislead: neither datatypes nor recursive functions can be
+\footnote{Do not be misled: neither datatypes nor recursive functions can be
extended by new constructors or equations. This is just a trick of the
presentation. In reality one has to define a new datatype and a new function.}%
\end{isamarkuptext}%
@@ -38,7 +38,7 @@
\ \ \ \ \ \ \ \ \ {\isachardoublequote}af\ A\ T\ {\isasymequiv}\ A\ {\isasymunion}\ {\isacharbraceleft}s{\isachardot}\ {\isasymforall}t{\isachardot}\ {\isacharparenleft}s{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\ {\isasymlongrightarrow}\ t\ {\isasymin}\ T{\isacharbraceright}{\isachardoublequote}%
\begin{isamarkuptext}%
\noindent
-Now we define \isa{mc\ {\isacharparenleft}AF\ f{\isacharparenright}} as the least set \isa{T} that contains
+Now we define \isa{mc\ {\isacharparenleft}AF\ f{\isacharparenright}} as the least set \isa{T} that includes
\isa{mc\ f} and all states all of whose direct successors are in \isa{T}:%
\end{isamarkuptext}%
{\isachardoublequote}mc{\isacharparenleft}AF\ f{\isacharparenright}\ \ \ \ {\isacharequal}\ lfp{\isacharparenleft}af{\isacharparenleft}mc\ f{\isacharparenright}{\isacharparenright}{\isachardoublequote}%
@@ -52,8 +52,9 @@
\isacommand{apply}\ blast\isanewline
\isacommand{done}%
\begin{isamarkuptext}%
-All we need to prove now is that \isa{mc} and \isa{{\isasymTurnstile}}
-agree for \isa{AF}, i.e.\ that \isa{mc\ {\isacharparenleft}AF\ f{\isacharparenright}\ {\isacharequal}\ {\isacharbraceleft}s{\isachardot}\ s\ {\isasymTurnstile}\ AF\ f{\isacharbraceright}}. This time we prove the two containments separately, starting
+All we need to prove now is \isa{mc\ {\isacharparenleft}AF\ f{\isacharparenright}\ {\isacharequal}\ {\isacharbraceleft}s{\isachardot}\ s\ {\isasymTurnstile}\ AF\ f{\isacharbraceright}}, which states
+that \isa{mc} and \isa{{\isasymTurnstile}} agree for \isa{AF}\@.
+This time we prove the two inclusions separately, starting
with the easy one:%
\end{isamarkuptext}%
\isacommand{theorem}\ AF{\isacharunderscore}lemma{\isadigit{1}}{\isacharcolon}\isanewline
@@ -105,7 +106,7 @@
\isacommand{apply}\ blast\isanewline
\isacommand{done}%
\begin{isamarkuptext}%
-The opposite containment is proved by contradiction: if some state
+The opposite inclusion is proved by contradiction: if some state
\isa{s} is not in \isa{lfp\ {\isacharparenleft}af\ A{\isacharparenright}}, then we can construct an
infinite \isa{A}-avoiding path starting from \isa{s}. The reason is
that by unfolding \isa{lfp} we find that if \isa{s} is not in
@@ -113,7 +114,8 @@
direct successor of \isa{s} that is again not in \isa{lfp\ {\isacharparenleft}af\ A{\isacharparenright}}. Iterating this argument yields the promised infinite
\isa{A}-avoiding path. Let us formalize this sketch.
-The one-step argument in the above sketch%
+The one-step argument in the sketch above
+is proved by a variant of contraposition:%
\end{isamarkuptext}%
\isacommand{lemma}\ not{\isacharunderscore}in{\isacharunderscore}lfp{\isacharunderscore}afD{\isacharcolon}\isanewline
\ {\isachardoublequote}s\ {\isasymnotin}\ lfp{\isacharparenleft}af\ A{\isacharparenright}\ {\isasymLongrightarrow}\ s\ {\isasymnotin}\ A\ {\isasymand}\ {\isacharparenleft}{\isasymexists}\ t{\isachardot}\ {\isacharparenleft}s{\isacharcomma}t{\isacharparenright}{\isasymin}M\ {\isasymand}\ t\ {\isasymnotin}\ lfp{\isacharparenleft}af\ A{\isacharparenright}{\isacharparenright}{\isachardoublequote}\isanewline
@@ -123,8 +125,7 @@
\isacommand{done}%
\begin{isamarkuptext}%
\noindent
-is proved by a variant of contraposition:
-assume the negation of the conclusion and prove \isa{s\ {\isasymin}\ lfp\ {\isacharparenleft}af\ A{\isacharparenright}}.
+We assume the negation of the conclusion and prove \isa{s\ {\isasymin}\ lfp\ {\isacharparenleft}af\ A{\isacharparenright}}.
Unfolding \isa{lfp} once and
simplifying with the definition of \isa{af} finishes the proof.
@@ -140,8 +141,8 @@
Element \isa{n\ {\isacharplus}\ {\isadigit{1}}} on this path is some arbitrary successor
\isa{t} of element \isa{n} such that \isa{P\ t} holds. Remember that \isa{SOME\ t{\isachardot}\ R\ t}
is some arbitrary but fixed \isa{t} such that \isa{R\ t} holds (see \S\ref{sec:SOME}). Of
-course, such a \isa{t} may in general not exist, but that is of no
-concern to us since we will only use \isa{path} in such cases where a
+course, such a \isa{t} need not exist, but that is of no
+concern to us since we will only use \isa{path} when a
suitable \isa{t} does exist.
Let us show that if each state \isa{s} that satisfies \isa{P}
@@ -224,8 +225,8 @@
\isacommand{apply}{\isacharparenleft}blast{\isacharparenright}\isanewline
\isacommand{done}%
\begin{isamarkuptext}%
-Function \isa{path} has fulfilled its purpose now and can be forgotten
-about. It was merely defined to provide the witness in the proof of the
+Function \isa{path} has fulfilled its purpose now and can be forgotten.
+It was merely defined to provide the witness in the proof of the
\isa{infinity{\isacharunderscore}lemma}. Aficionados of minimal proofs might like to know
that we could have given the witness without having to define a new function:
the term
@@ -233,8 +234,7 @@
\ \ \ \ \ nat{\isacharunderscore}rec\ s\ {\isacharparenleft}{\isasymlambda}n\ t{\isachardot}\ SOME\ u{\isachardot}\ {\isacharparenleft}t{\isacharcomma}\ u{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ P\ u{\isacharparenright}%
\end{isabelle}
is extensionally equal to \isa{path\ s\ P},
-where \isa{nat{\isacharunderscore}rec} is the predefined primitive recursor on \isa{nat}, whose defining
-equations we omit.%
+where \isa{nat{\isacharunderscore}rec} is the predefined primitive recursor on \isa{nat}.%
\end{isamarkuptext}%
%
\begin{isamarkuptext}%
@@ -267,8 +267,8 @@
\ \isacommand{apply}{\isacharparenleft}auto\ dest{\isacharcolon}not{\isacharunderscore}in{\isacharunderscore}lfp{\isacharunderscore}afD{\isacharparenright}\isanewline
\isacommand{done}%
\begin{isamarkuptext}%
-If you found the above proofs somewhat complicated we recommend you read
-\S\ref{sec:CTL-revisited} where we shown how inductive definitions lead to
+If you find these proofs too complicated, we recommend that you read
+\S\ref{sec:CTL-revisited}, where we show how inductive definitions lead to
simpler arguments.
The main theorem is proved as for PDL, except that we also derive the
@@ -280,8 +280,8 @@
\isacommand{apply}{\isacharparenleft}auto\ simp\ add{\isacharcolon}\ EF{\isacharunderscore}lemma\ equalityI{\isacharbrackleft}OF\ AF{\isacharunderscore}lemma{\isadigit{1}}\ AF{\isacharunderscore}lemma{\isadigit{2}}{\isacharbrackright}{\isacharparenright}\isanewline
\isacommand{done}%
\begin{isamarkuptext}%
-The above language is not quite CTL\@. The latter also includes an
-until-operator \isa{EU\ f\ g} with semantics ``there exist a path
+The language defined above is not quite CTL\@. The latter also includes an
+until-operator \isa{EU\ f\ g} with semantics ``there exists a path
where \isa{f} is true until \isa{g} becomes true''. With the help
of an auxiliary function%
\end{isamarkuptext}%
@@ -312,15 +312,18 @@
%{text[display]"| EU formula formula E[_ U _]"}
%which enables you to read and write {text"E[f U g]"} instead of {term"EU f g"}.
\end{exercise}
-For more CTL exercises see, for example, \cite{Huth-Ryan-book}.%
+For more CTL exercises see, for example, Huth and Ryan \cite{Huth-Ryan-book}.%
\end{isamarkuptext}%
%
\begin{isamarkuptext}%
Let us close this section with a few words about the executability of our model checkers.
It is clear that if all sets are finite, they can be represented as lists and the usual
set operations are easily implemented. Only \isa{lfp} requires a little thought.
-Fortunately the HOL library proves that in the case of finite sets and a monotone \isa{F},
-\isa{lfp\ F} can be computed by iterated application of \isa{F} to \isa{{\isacharbraceleft}{\isacharbraceright}} until
+\REMARK{you had `in the library' but I assume you meant it was a
+built in lemma. Do we give its name?}
+Fortunately, Isabelle/HOL provides a theorem stating that
+in the case of finite sets and a monotone \isa{F},
+the value of \isa{lfp\ F} can be computed by iterated application of \isa{F} to~\isa{{\isacharbraceleft}{\isacharbraceright}} until
a fixed point is reached. It is actually possible to generate executable functional programs
from HOL definitions, but that is beyond the scope of the tutorial.%
\end{isamarkuptext}%
--- a/doc-src/TutorialI/CTL/document/PDL.tex Thu Jan 11 11:47:57 2001 +0100
+++ b/doc-src/TutorialI/CTL/document/PDL.tex Thu Jan 11 12:12:01 2001 +0100
@@ -2,7 +2,7 @@
\begin{isabellebody}%
\def\isabellecontext{PDL}%
%
-\isamarkupsubsection{Propositional dynamic logic---PDL%
+\isamarkupsubsection{Propositional Dynamic Logic---PDL%
}
%
\begin{isamarkuptext}%
@@ -10,7 +10,7 @@
The formulae of PDL are built up from atomic propositions via the customary
propositional connectives of negation and conjunction and the two temporal
connectives \isa{AX} and \isa{EF}. Since formulae are essentially
-(syntax) trees, they are naturally modelled as a datatype:%
+syntax trees, they are naturally modelled as a datatype:%
\end{isamarkuptext}%
\isacommand{datatype}\ formula\ {\isacharequal}\ Atom\ atom\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharbar}\ Neg\ formula\isanewline
@@ -20,8 +20,7 @@
\begin{isamarkuptext}%
\noindent
This is almost the same as in the boolean expression case study in
-\S\ref{sec:boolex}, except that what used to be called \isa{Var} is now
-called \isa{Atom}.
+\S\ref{sec:boolex}.
The meaning of these formulae is given by saying which formula is true in
which state:%
@@ -29,9 +28,10 @@
\isacommand{consts}\ valid\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}state\ {\isasymRightarrow}\ formula\ {\isasymRightarrow}\ bool{\isachardoublequote}\ \ \ {\isacharparenleft}{\isachardoublequote}{\isacharparenleft}{\isacharunderscore}\ {\isasymTurnstile}\ {\isacharunderscore}{\isacharparenright}{\isachardoublequote}\ {\isacharbrackleft}{\isadigit{8}}{\isadigit{0}}{\isacharcomma}{\isadigit{8}}{\isadigit{0}}{\isacharbrackright}\ {\isadigit{8}}{\isadigit{0}}{\isacharparenright}%
\begin{isamarkuptext}%
\noindent
-The concrete syntax annotation allows us to write \isa{s\ {\isasymTurnstile}\ f} instead of
-\isa{valid\ s\ f}.
+The syntax annotation allows us to write \isa{s\ {\isasymTurnstile}\ f} instead of
+\hbox{\isa{valid\ s\ f}}.
+\smallskip
The definition of \isa{{\isasymTurnstile}} is by recursion over the syntax:%
\end{isamarkuptext}%
\isacommand{primrec}\isanewline
@@ -45,7 +45,7 @@
The first three equations should be self-explanatory. The temporal formula
\isa{AX\ f} means that \isa{f} is true in all next states whereas
\isa{EF\ f} means that there exists some future state in which \isa{f} is
-true. The future is expressed via \isa{\isactrlsup {\isacharasterisk}}, the transitive reflexive
+true. The future is expressed via \isa{\isactrlsup {\isacharasterisk}}, the reflexive transitive
closure. Because of reflexivity, the future includes the present.
Now we come to the model checker itself. It maps a formula into the set of
@@ -58,12 +58,12 @@
{\isachardoublequote}mc{\isacharparenleft}Neg\ f{\isacharparenright}\ \ \ {\isacharequal}\ {\isacharminus}mc\ f{\isachardoublequote}\isanewline
{\isachardoublequote}mc{\isacharparenleft}And\ f\ g{\isacharparenright}\ {\isacharequal}\ mc\ f\ {\isasyminter}\ mc\ g{\isachardoublequote}\isanewline
{\isachardoublequote}mc{\isacharparenleft}AX\ f{\isacharparenright}\ \ \ \ {\isacharequal}\ {\isacharbraceleft}s{\isachardot}\ {\isasymforall}t{\isachardot}\ {\isacharparenleft}s{\isacharcomma}t{\isacharparenright}\ {\isasymin}\ M\ \ {\isasymlongrightarrow}\ t\ {\isasymin}\ mc\ f{\isacharbraceright}{\isachardoublequote}\isanewline
-{\isachardoublequote}mc{\isacharparenleft}EF\ f{\isacharparenright}\ \ \ \ {\isacharequal}\ lfp{\isacharparenleft}{\isasymlambda}T{\isachardot}\ mc\ f\ {\isasymunion}\ M{\isasyminverse}\ {\isacharbackquote}{\isacharbackquote}\ T{\isacharparenright}{\isachardoublequote}%
+{\isachardoublequote}mc{\isacharparenleft}EF\ f{\isacharparenright}\ \ \ \ {\isacharequal}\ lfp{\isacharparenleft}{\isasymlambda}T{\isachardot}\ mc\ f\ {\isasymunion}\ {\isacharparenleft}M{\isasyminverse}\ {\isacharbackquote}{\isacharbackquote}\ T{\isacharparenright}{\isacharparenright}{\isachardoublequote}%
\begin{isamarkuptext}%
\noindent
Only the equation for \isa{EF} deserves some comments. Remember that the
postfix \isa{{\isasyminverse}} and the infix \isa{{\isacharbackquote}{\isacharbackquote}} are predefined and denote the
-converse of a relation and the application of a relation to a set. Thus
+converse of a relation and the image of a set under a relation. Thus
\isa{M{\isasyminverse}\ {\isacharbackquote}{\isacharbackquote}\ T} is the set of all predecessors of \isa{T} and the least
fixed point (\isa{lfp}) of \isa{{\isasymlambda}T{\isachardot}\ mc\ f\ {\isasymunion}\ M{\isasyminverse}\ {\isacharbackquote}{\isacharbackquote}\ T} is the least set
\isa{T} containing \isa{mc\ f} and all predecessors of \isa{T}. If you
@@ -71,25 +71,24 @@
which there is a path to a state where \isa{f} is true, do not worry---that
will be proved in a moment.
-First we prove monotonicity of the function inside \isa{lfp}%
+First we prove monotonicity of the function inside \isa{lfp}
+in order to make sure it really has a least fixed point.%
\end{isamarkuptext}%
-\isacommand{lemma}\ mono{\isacharunderscore}ef{\isacharcolon}\ {\isachardoublequote}mono{\isacharparenleft}{\isasymlambda}T{\isachardot}\ A\ {\isasymunion}\ M{\isasyminverse}\ {\isacharbackquote}{\isacharbackquote}\ T{\isacharparenright}{\isachardoublequote}\isanewline
+\isacommand{lemma}\ mono{\isacharunderscore}ef{\isacharcolon}\ {\isachardoublequote}mono{\isacharparenleft}{\isasymlambda}T{\isachardot}\ A\ {\isasymunion}\ {\isacharparenleft}M{\isasyminverse}\ {\isacharbackquote}{\isacharbackquote}\ T{\isacharparenright}{\isacharparenright}{\isachardoublequote}\isanewline
\isacommand{apply}{\isacharparenleft}rule\ monoI{\isacharparenright}\isanewline
\isacommand{apply}\ blast\isanewline
\isacommand{done}%
\begin{isamarkuptext}%
\noindent
-in order to make sure it really has a least fixed point.
-
Now we can relate model checking and semantics. For the \isa{EF} case we need
a separate lemma:%
\end{isamarkuptext}%
\isacommand{lemma}\ EF{\isacharunderscore}lemma{\isacharcolon}\isanewline
-\ \ {\isachardoublequote}lfp{\isacharparenleft}{\isasymlambda}T{\isachardot}\ A\ {\isasymunion}\ M{\isasyminverse}\ {\isacharbackquote}{\isacharbackquote}\ T{\isacharparenright}\ {\isacharequal}\ {\isacharbraceleft}s{\isachardot}\ {\isasymexists}t{\isachardot}\ {\isacharparenleft}s{\isacharcomma}t{\isacharparenright}\ {\isasymin}\ M\isactrlsup {\isacharasterisk}\ {\isasymand}\ t\ {\isasymin}\ A{\isacharbraceright}{\isachardoublequote}%
+\ \ {\isachardoublequote}lfp{\isacharparenleft}{\isasymlambda}T{\isachardot}\ A\ {\isasymunion}\ {\isacharparenleft}M{\isasyminverse}\ {\isacharbackquote}{\isacharbackquote}\ T{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ {\isacharbraceleft}s{\isachardot}\ {\isasymexists}t{\isachardot}\ {\isacharparenleft}s{\isacharcomma}t{\isacharparenright}\ {\isasymin}\ M\isactrlsup {\isacharasterisk}\ {\isasymand}\ t\ {\isasymin}\ A{\isacharbraceright}{\isachardoublequote}%
\begin{isamarkuptxt}%
\noindent
The equality is proved in the canonical fashion by proving that each set
-contains the other; the containment is shown pointwise:%
+includes the other; the inclusion is shown pointwise:%
\end{isamarkuptxt}%
\isacommand{apply}{\isacharparenleft}rule\ equalityI{\isacharparenright}\isanewline
\ \isacommand{apply}{\isacharparenleft}rule\ subsetI{\isacharparenright}\isanewline
@@ -118,7 +117,7 @@
\end{isamarkuptxt}%
\ \isacommand{apply}{\isacharparenleft}blast\ intro{\isacharcolon}\ rtrancl{\isacharunderscore}trans{\isacharparenright}%
\begin{isamarkuptxt}%
-We now return to the second set containment subgoal, which is again proved
+We now return to the second set inclusion subgoal, which is again proved
pointwise:%
\end{isamarkuptxt}%
\isacommand{apply}{\isacharparenleft}rule\ subsetI{\isacharparenright}\isanewline