--- a/doc-src/TutorialI/Advanced/advanced.tex Mon Oct 09 17:40:47 2000 +0200
+++ b/doc-src/TutorialI/Advanced/advanced.tex Mon Oct 09 19:20:55 2000 +0200
@@ -1,5 +1,5 @@
-\chapter{Advanced Simplification, Recursion, and Induction}
-\markboth{}{CHAPTER 4: ADVANCED SIMPLIFICATION ...}
+\chapter{Advanced Simplification, Recursion and Induction}
+\markboth{}{CHAPTER 4: ADVANCED SIMPLIFICATION, RECURSION ...}
Although we have already learned a lot about simplification, recursion and
induction, there are some advanced proof techniques that we have not covered
--- a/doc-src/TutorialI/CTL/Base.thy Mon Oct 09 17:40:47 2000 +0200
+++ b/doc-src/TutorialI/CTL/Base.thy Mon Oct 09 19:20:55 2000 +0200
@@ -7,7 +7,7 @@
state systems (implementations) w.r.t.\ temporal logic formulae
(specifications) \cite{Clark}. Its foundations are completely set theoretic
and this section shall develop them in HOL. This is done in two steps: first
-we consider a very simple ``temporal'' logic called propositional dynamic
+we consider a simple modal logic called propositional dynamic
logic (PDL) which we then extend to the temporal logic CTL 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
--- a/doc-src/TutorialI/CTL/CTL.thy Mon Oct 09 17:40:47 2000 +0200
+++ b/doc-src/TutorialI/CTL/CTL.thy Mon Oct 09 19:20:55 2000 +0200
@@ -117,8 +117,6 @@
(*ML"Pretty.setmargin 70";
pr(latex xsymbols symbols);*)
txt{*\noindent
-FIXME OF/of with undescore?
-
leads to the following somewhat involved proof state
\begin{isabelle}
\ \isadigit{1}{\isachardot}\ {\isasymAnd}p{\isachardot}\ {\isasymlbrakk}p\ \isadigit{0}\ {\isasymin}\ A\ {\isasymor}\isanewline
@@ -374,15 +372,19 @@
text{*
The above language is not quite CTL. The latter also includes an
-until-operator, usually written as an infix @{text U}. The formula
-@{term"f U g"} means ``@{term f} until @{term g}''.
+until-operator, which is the subject of the following exercise.
It is not definable in terms of the other operators!
\begin{exercise}
-Extend the datatype of formulae by the until operator with semantics
-@{text[display]"s \<Turnstile> f U g = (............)"}
+Extend the datatype of formulae by the binary until operator @{term"EU f g"} with semantics
+``there exist a path where @{term f} is true until @{term g} becomes true''
+@{text[display]"s \<Turnstile> EU f g = (\<exists>p\<in>Paths s. \<exists>j. p j \<Turnstile> g \<and> (\<exists>i < j. p i \<Turnstile> f))"}
and model checking algorithm
-@{text[display]"mc(f U g) = (............)"}
-Prove that the equivalence between semantics and model checking still holds.
+@{text[display]"mc(EU f g) = lfp(\<lambda>T. mc g \<union> mc f \<inter> (M^-1 ^^ T))"}
+Prove the equivalence between semantics and model checking, i.e.\
+@{prop"mc(EU f g) = {s. s \<Turnstile> EU f g}"}.
+
+For readability you may want to equip @{term EU} with the following customary syntax:
+@{text"E[f U g]"}.
\end{exercise}
Let us close this section with a few words about the executability of @{term mc}.
--- a/doc-src/TutorialI/CTL/PDL.thy Mon Oct 09 17:40:47 2000 +0200
+++ b/doc-src/TutorialI/CTL/PDL.thy Mon Oct 09 19:20:55 2000 +0200
@@ -1,8 +1,8 @@
(*<*)theory PDL = Base:(*>*)
-subsection{*Propositional dynmic logic---PDL*}
+subsection{*Propositional dynamic logic---PDL*}
-text{*
+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
@@ -60,7 +60,6 @@
"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^-1 ^^ T)"
-
text{*\noindent
Only the equation for @{term EF} deserves some comments. Remember that the
postfix @{text"^-1"} and the infix @{text"^^"} are predefined and denote the
@@ -199,6 +198,7 @@
Show that the semantics for @{term EF} satisfies the following recursion equation:
@{prop[display]"(s \<Turnstile> EF f) = (s \<Turnstile> f | s \<Turnstile> EN(EF f))"}
\end{exercise}
+\index{PDL|)}
*}
(*<*)
theorem main: "mc f = {s. s \<Turnstile> f}";
--- a/doc-src/TutorialI/CTL/ctl.tex Mon Oct 09 17:40:47 2000 +0200
+++ b/doc-src/TutorialI/CTL/ctl.tex Mon Oct 09 19:20:55 2000 +0200
@@ -1,3 +1,6 @@
+\index{CTL|(}
+\index{lfp@{\texttt{lfp}}!applications of|see{CTL}}
\input{CTL/document/Base.tex}
\input{CTL/document/PDL.tex}
\input{CTL/document/CTL.tex}
+\index{CTL|)}
--- a/doc-src/TutorialI/CTL/document/Base.tex Mon Oct 09 17:40:47 2000 +0200
+++ b/doc-src/TutorialI/CTL/document/Base.tex Mon Oct 09 19:20:55 2000 +0200
@@ -9,7 +9,7 @@
state systems (implementations) w.r.t.\ temporal logic formulae
(specifications) \cite{Clark}. Its foundations are completely set theoretic
and this section shall develop them in HOL. This is done in two steps: first
-we consider a very simple ``temporal'' logic called propositional dynamic
+we consider a simple modal logic called propositional dynamic
logic (PDL) which we then extend to the temporal logic CTL 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
--- a/doc-src/TutorialI/CTL/document/CTL.tex Mon Oct 09 17:40:47 2000 +0200
+++ b/doc-src/TutorialI/CTL/document/CTL.tex Mon Oct 09 19:20:55 2000 +0200
@@ -66,8 +66,6 @@
\isacommand{apply}{\isacharparenleft}clarsimp\ simp\ add{\isacharcolon}\ af{\isacharunderscore}def\ Paths{\isacharunderscore}def{\isacharparenright}%
\begin{isamarkuptxt}%
\noindent
-FIXME OF/of with undescore?
-
leads to the following somewhat involved proof state
\begin{isabelle}
\ \isadigit{1}{\isachardot}\ {\isasymAnd}p{\isachardot}\ {\isasymlbrakk}p\ \isadigit{0}\ {\isasymin}\ A\ {\isasymor}\isanewline
@@ -273,19 +271,23 @@
\isacommand{done}%
\begin{isamarkuptext}%
The above language is not quite CTL. The latter also includes an
-until-operator, usually written as an infix \isa{U}. The formula
-\isa{f\ U\ g} means ``\isa{f} until \isa{g}''.
+until-operator, which is the subject of the following exercise.
It is not definable in terms of the other operators!
\begin{exercise}
-Extend the datatype of formulae by the until operator with semantics
+Extend the datatype of formulae by the binary until operator \isa{EU\ f\ g} with semantics
+``there exist a path where \isa{f} is true until \isa{g} becomes true''
\begin{isabelle}%
-\ \ \ \ \ s\ {\isasymTurnstile}\ f\ U\ g\ {\isacharequal}\ {\isacharparenleft}{\isachardot}{\isachardot}{\isachardot}{\isachardot}{\isachardot}{\isachardot}{\isachardot}{\isachardot}{\isachardot}{\isachardot}{\isachardot}{\isachardot}{\isacharparenright}%
+\ \ \ \ \ s\ {\isasymTurnstile}\ EU\ f\ g\ {\isacharequal}\ {\isacharparenleft}{\isasymexists}p{\isasymin}Paths\ s{\isachardot}\ {\isasymexists}j{\isachardot}\ p\ j\ {\isasymTurnstile}\ g\ {\isasymand}\ {\isacharparenleft}{\isasymexists}i\ {\isacharless}\ j{\isachardot}\ p\ i\ {\isasymTurnstile}\ f{\isacharparenright}{\isacharparenright}%
\end{isabelle}
and model checking algorithm
\begin{isabelle}%
-\ \ \ \ \ mc{\isacharparenleft}f\ U\ g{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}{\isachardot}{\isachardot}{\isachardot}{\isachardot}{\isachardot}{\isachardot}{\isachardot}{\isachardot}{\isachardot}{\isachardot}{\isachardot}{\isachardot}{\isacharparenright}%
+\ \ \ \ \ mc{\isacharparenleft}EU\ f\ g{\isacharparenright}\ {\isacharequal}\ lfp{\isacharparenleft}{\isasymlambda}T{\isachardot}\ mc\ g\ {\isasymunion}\ mc\ f\ {\isasyminter}\ {\isacharparenleft}M{\isacharcircum}{\isacharminus}\isadigit{1}\ {\isacharcircum}{\isacharcircum}\ T{\isacharparenright}{\isacharparenright}%
\end{isabelle}
-Prove that the equivalence between semantics and model checking still holds.
+Prove the equivalence between semantics and model checking, i.e.\
+\isa{mc\ {\isacharparenleft}EU\ f\ g{\isacharparenright}\ {\isacharequal}\ {\isacharbraceleft}s{\isachardot}\ s\ {\isasymTurnstile}\ EU\ f\ g{\isacharbraceright}}.
+
+For readability you may want to equip \isa{EU} with the following customary syntax:
+\isa{E{\isacharbrackleft}f\ U\ g{\isacharbrackright}}.
\end{exercise}
Let us close this section with a few words about the executability of \isa{mc}.
--- a/doc-src/TutorialI/CTL/document/PDL.tex Mon Oct 09 17:40:47 2000 +0200
+++ b/doc-src/TutorialI/CTL/document/PDL.tex Mon Oct 09 19:20:55 2000 +0200
@@ -2,9 +2,10 @@
\begin{isabellebody}%
\def\isabellecontext{PDL}%
%
-\isamarkupsubsection{Propositional dynmic logic---PDL}
+\isamarkupsubsection{Propositional dynamic logic---PDL}
%
\begin{isamarkuptext}%
+\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 \isa{AX} and \isa{EF}. Since formulae are essentially
@@ -188,7 +189,8 @@
\begin{isabelle}%
\ \ \ \ \ s\ {\isasymTurnstile}\ EF\ f\ {\isacharequal}\ {\isacharparenleft}s\ {\isasymTurnstile}\ f\ {\isasymor}\ s\ {\isasymTurnstile}\ EN\ {\isacharparenleft}EF\ f{\isacharparenright}{\isacharparenright}%
\end{isabelle}
-\end{exercise}%
+\end{exercise}
+\index{PDL|)}%
\end{isamarkuptext}%
\end{isabellebody}%
%%% Local Variables:
--- a/doc-src/TutorialI/Datatype/Nested.thy Mon Oct 09 17:40:47 2000 +0200
+++ b/doc-src/TutorialI/Datatype/Nested.thy Mon Oct 09 19:20:55 2000 +0200
@@ -78,9 +78,9 @@
\begin{exercise}
The fact that substitution distributes over composition can be expressed
roughly as follows:
-@{text[display]"subst (f o g) t = subst f (subst g t)"}
+@{text[display]"subst (f \<circ> g) t = subst f (subst g t)"}
Correct this statement (you will find that it does not type-check),
-strengthen it, and prove it. (Note: \isaindexbold{o} is function composition;
+strengthen it, and prove it. (Note: @{text"\<circ>"} is function composition;
its definition is found in theorem @{thm[source]o_def}).
\end{exercise}
\begin{exercise}\label{ex:trev-trev}
--- a/doc-src/TutorialI/Datatype/document/Nested.tex Mon Oct 09 17:40:47 2000 +0200
+++ b/doc-src/TutorialI/Datatype/document/Nested.tex Mon Oct 09 19:20:55 2000 +0200
@@ -75,10 +75,10 @@
The fact that substitution distributes over composition can be expressed
roughly as follows:
\begin{isabelle}%
-\ \ \ \ \ subst\ {\isacharparenleft}f\ o\ g{\isacharparenright}\ t\ {\isacharequal}\ subst\ f\ {\isacharparenleft}subst\ g\ t{\isacharparenright}%
+\ \ \ \ \ subst\ {\isacharparenleft}f\ {\isasymcirc}\ g{\isacharparenright}\ t\ {\isacharequal}\ subst\ f\ {\isacharparenleft}subst\ g\ t{\isacharparenright}%
\end{isabelle}
Correct this statement (you will find that it does not type-check),
-strengthen it, and prove it. (Note: \isaindexbold{o} is function composition;
+strengthen it, and prove it. (Note: \isa{{\isasymcirc}} is function composition;
its definition is found in theorem \isa{o{\isacharunderscore}def}).
\end{exercise}
\begin{exercise}\label{ex:trev-trev}
--- a/doc-src/TutorialI/Recdef/simplification.thy Mon Oct 09 17:40:47 2000 +0200
+++ b/doc-src/TutorialI/Recdef/simplification.thy Mon Oct 09 19:20:55 2000 +0200
@@ -60,7 +60,7 @@
may not be expressible by pattern matching.
A very simple alternative is to replace @{text if} by @{text case}, which
-is also available for @{typ"bool"} but is not split automatically:
+is also available for @{typ bool} but is not split automatically:
*}
consts gcd2 :: "nat\<times>nat \<Rightarrow> nat";
--- a/doc-src/TutorialI/appendix.tex Mon Oct 09 17:40:47 2000 +0200
+++ b/doc-src/TutorialI/appendix.tex Mon Oct 09 19:20:55 2000 +0200
@@ -54,10 +54,10 @@
\verb$\<exists>!$\\
\indexboldpos{\isasymepsilon}{$HOL0ExSome} &
\ttindexbold{SOME} &
-\verb$\<?>$\\
+\verb$\<epsilon>$\\
\indexboldpos{\isasymcirc}{$HOL1} &
\ttindexbold{o} &
-\verb$\<?>$\\
+\verb$\<circ>$\\
\indexboldpos{\isasymle}{$HOL2arithrel}&
\ttindexboldpos{<=}{$HOL2arithrel}&
\verb$\<le>$\\
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/TutorialI/sets.tex Mon Oct 09 19:20:55 2000 +0200
@@ -0,0 +1,3 @@
+\chapter{Sets, Functions and Relations}
+
+\input{CTL/ctl}
\ No newline at end of file
--- a/doc-src/TutorialI/tutorial.tex Mon Oct 09 17:40:47 2000 +0200
+++ b/doc-src/TutorialI/tutorial.tex Mon Oct 09 19:20:55 2000 +0200
@@ -47,8 +47,8 @@
\\ \vspace{0.5cm} The Tutorial
\\ --- DRAFT ---}
\author{Tobias Nipkow\\
-Technische Universit\"at M\"unchen \\
-Institut f\"ur Informatik \\
+Technische Universit{\"a}t M{\"u}nchen \\
+Institut f{\"u}r Informatik \\
\url{http://www.in.tum.de/~nipkow/}}
\maketitle
@@ -57,7 +57,7 @@
\subsubsection*{Acknowledgements}
This tutorial owes a lot to the constant discussions with and the valuable
-feedback from Larry Paulson and the Isabelle group at Munich: Olaf M\"uller,
+feedback from Larry Paulson and the Isabelle group at Munich: Olaf M{\"u}ller,
Wolfgang Naraschewski, David von Oheimb, Leonor Prensa Nieto, Cornelia Pusch
and Markus Wenzel. Stefan Berghofer and Stephan Merz were also kind enough to
read and comment on a draft version.
@@ -65,8 +65,15 @@
\input{basics}
\input{fp}
-\input{CTL/ctl}
+\chapter{The Rules of the Game}
+\input{sets}
+\chapter{Inductively Defined Sets}
\input{Advanced/advanced}
+\chapter{More about Types}
+\chapter{Theory Presentation}
+\chapter{Case Study: The Needhamd-Schroeder Protocol}
+\chapter{Structured Proofs}
+\chapter{Case Study: UNIX File-System Security}
%\chapter{The Tricks of the Trade}
\input{appendix}