1.1 --- a/doc-src/TutorialI/Advanced/advanced.tex Mon Oct 09 17:40:47 2000 +0200
1.2 +++ b/doc-src/TutorialI/Advanced/advanced.tex Mon Oct 09 19:20:55 2000 +0200
1.3 @@ -1,5 +1,5 @@
1.4 -\chapter{Advanced Simplification, Recursion, and Induction}
1.5 -\markboth{}{CHAPTER 4: ADVANCED SIMPLIFICATION ...}
1.6 +\chapter{Advanced Simplification, Recursion and Induction}
1.7 +\markboth{}{CHAPTER 4: ADVANCED SIMPLIFICATION, RECURSION ...}
1.8
1.9 Although we have already learned a lot about simplification, recursion and
1.10 induction, there are some advanced proof techniques that we have not covered
2.1 --- a/doc-src/TutorialI/CTL/Base.thy Mon Oct 09 17:40:47 2000 +0200
2.2 +++ b/doc-src/TutorialI/CTL/Base.thy Mon Oct 09 19:20:55 2000 +0200
2.3 @@ -7,7 +7,7 @@
2.4 state systems (implementations) w.r.t.\ temporal logic formulae
2.5 (specifications) \cite{Clark}. Its foundations are completely set theoretic
2.6 and this section shall develop them in HOL. This is done in two steps: first
2.7 -we consider a very simple ``temporal'' logic called propositional dynamic
2.8 +we consider a simple modal logic called propositional dynamic
2.9 logic (PDL) which we then extend to the temporal logic CTL used in many real
2.10 model checkers. In each case we give both a traditional semantics (@{text \<Turnstile>}) and a
2.11 recursive function @{term mc} that maps a formula into the set of all states of
3.1 --- a/doc-src/TutorialI/CTL/CTL.thy Mon Oct 09 17:40:47 2000 +0200
3.2 +++ b/doc-src/TutorialI/CTL/CTL.thy Mon Oct 09 19:20:55 2000 +0200
3.3 @@ -117,8 +117,6 @@
3.4 (*ML"Pretty.setmargin 70";
3.5 pr(latex xsymbols symbols);*)
3.6 txt{*\noindent
3.7 -FIXME OF/of with undescore?
3.8 -
3.9 leads to the following somewhat involved proof state
3.10 \begin{isabelle}
3.11 \ \isadigit{1}{\isachardot}\ {\isasymAnd}p{\isachardot}\ {\isasymlbrakk}p\ \isadigit{0}\ {\isasymin}\ A\ {\isasymor}\isanewline
3.12 @@ -374,15 +372,19 @@
3.13
3.14 text{*
3.15 The above language is not quite CTL. The latter also includes an
3.16 -until-operator, usually written as an infix @{text U}. The formula
3.17 -@{term"f U g"} means ``@{term f} until @{term g}''.
3.18 +until-operator, which is the subject of the following exercise.
3.19 It is not definable in terms of the other operators!
3.20 \begin{exercise}
3.21 -Extend the datatype of formulae by the until operator with semantics
3.22 -@{text[display]"s \<Turnstile> f U g = (............)"}
3.23 +Extend the datatype of formulae by the binary until operator @{term"EU f g"} with semantics
3.24 +``there exist a path where @{term f} is true until @{term g} becomes true''
3.25 +@{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))"}
3.26 and model checking algorithm
3.27 -@{text[display]"mc(f U g) = (............)"}
3.28 -Prove that the equivalence between semantics and model checking still holds.
3.29 +@{text[display]"mc(EU f g) = lfp(\<lambda>T. mc g \<union> mc f \<inter> (M^-1 ^^ T))"}
3.30 +Prove the equivalence between semantics and model checking, i.e.\
3.31 +@{prop"mc(EU f g) = {s. s \<Turnstile> EU f g}"}.
3.32 +
3.33 +For readability you may want to equip @{term EU} with the following customary syntax:
3.34 +@{text"E[f U g]"}.
3.35 \end{exercise}
3.36
3.37 Let us close this section with a few words about the executability of @{term mc}.
4.1 --- a/doc-src/TutorialI/CTL/PDL.thy Mon Oct 09 17:40:47 2000 +0200
4.2 +++ b/doc-src/TutorialI/CTL/PDL.thy Mon Oct 09 19:20:55 2000 +0200
4.3 @@ -1,8 +1,8 @@
4.4 (*<*)theory PDL = Base:(*>*)
4.5
4.6 -subsection{*Propositional dynmic logic---PDL*}
4.7 +subsection{*Propositional dynamic logic---PDL*}
4.8
4.9 -text{*
4.10 +text{*\index{PDL|(}
4.11 The formulae of PDL are built up from atomic propositions via the customary
4.12 propositional connectives of negation and conjunction and the two temporal
4.13 connectives @{text AX} and @{text EF}. Since formulae are essentially
4.14 @@ -60,7 +60,6 @@
4.15 "mc(AX f) = {s. \<forall>t. (s,t) \<in> M \<longrightarrow> t \<in> mc f}"
4.16 "mc(EF f) = lfp(\<lambda>T. mc f \<union> M^-1 ^^ T)"
4.17
4.18 -
4.19 text{*\noindent
4.20 Only the equation for @{term EF} deserves some comments. Remember that the
4.21 postfix @{text"^-1"} and the infix @{text"^^"} are predefined and denote the
4.22 @@ -199,6 +198,7 @@
4.23 Show that the semantics for @{term EF} satisfies the following recursion equation:
4.24 @{prop[display]"(s \<Turnstile> EF f) = (s \<Turnstile> f | s \<Turnstile> EN(EF f))"}
4.25 \end{exercise}
4.26 +\index{PDL|)}
4.27 *}
4.28 (*<*)
4.29 theorem main: "mc f = {s. s \<Turnstile> f}";
5.1 --- a/doc-src/TutorialI/CTL/ctl.tex Mon Oct 09 17:40:47 2000 +0200
5.2 +++ b/doc-src/TutorialI/CTL/ctl.tex Mon Oct 09 19:20:55 2000 +0200
5.3 @@ -1,3 +1,6 @@
5.4 +\index{CTL|(}
5.5 +\index{lfp@{\texttt{lfp}}!applications of|see{CTL}}
5.6 \input{CTL/document/Base.tex}
5.7 \input{CTL/document/PDL.tex}
5.8 \input{CTL/document/CTL.tex}
5.9 +\index{CTL|)}
6.1 --- a/doc-src/TutorialI/CTL/document/Base.tex Mon Oct 09 17:40:47 2000 +0200
6.2 +++ b/doc-src/TutorialI/CTL/document/Base.tex Mon Oct 09 19:20:55 2000 +0200
6.3 @@ -9,7 +9,7 @@
6.4 state systems (implementations) w.r.t.\ temporal logic formulae
6.5 (specifications) \cite{Clark}. Its foundations are completely set theoretic
6.6 and this section shall develop them in HOL. This is done in two steps: first
6.7 -we consider a very simple ``temporal'' logic called propositional dynamic
6.8 +we consider a simple modal logic called propositional dynamic
6.9 logic (PDL) which we then extend to the temporal logic CTL used in many real
6.10 model checkers. In each case we give both a traditional semantics (\isa{{\isasymTurnstile}}) and a
6.11 recursive function \isa{mc} that maps a formula into the set of all states of
7.1 --- a/doc-src/TutorialI/CTL/document/CTL.tex Mon Oct 09 17:40:47 2000 +0200
7.2 +++ b/doc-src/TutorialI/CTL/document/CTL.tex Mon Oct 09 19:20:55 2000 +0200
7.3 @@ -66,8 +66,6 @@
7.4 \isacommand{apply}{\isacharparenleft}clarsimp\ simp\ add{\isacharcolon}\ af{\isacharunderscore}def\ Paths{\isacharunderscore}def{\isacharparenright}%
7.5 \begin{isamarkuptxt}%
7.6 \noindent
7.7 -FIXME OF/of with undescore?
7.8 -
7.9 leads to the following somewhat involved proof state
7.10 \begin{isabelle}
7.11 \ \isadigit{1}{\isachardot}\ {\isasymAnd}p{\isachardot}\ {\isasymlbrakk}p\ \isadigit{0}\ {\isasymin}\ A\ {\isasymor}\isanewline
7.12 @@ -273,19 +271,23 @@
7.13 \isacommand{done}%
7.14 \begin{isamarkuptext}%
7.15 The above language is not quite CTL. The latter also includes an
7.16 -until-operator, usually written as an infix \isa{U}. The formula
7.17 -\isa{f\ U\ g} means ``\isa{f} until \isa{g}''.
7.18 +until-operator, which is the subject of the following exercise.
7.19 It is not definable in terms of the other operators!
7.20 \begin{exercise}
7.21 -Extend the datatype of formulae by the until operator with semantics
7.22 +Extend the datatype of formulae by the binary until operator \isa{EU\ f\ g} with semantics
7.23 +``there exist a path where \isa{f} is true until \isa{g} becomes true''
7.24 \begin{isabelle}%
7.25 -\ \ \ \ \ s\ {\isasymTurnstile}\ f\ U\ g\ {\isacharequal}\ {\isacharparenleft}{\isachardot}{\isachardot}{\isachardot}{\isachardot}{\isachardot}{\isachardot}{\isachardot}{\isachardot}{\isachardot}{\isachardot}{\isachardot}{\isachardot}{\isacharparenright}%
7.26 +\ \ \ \ \ 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}%
7.27 \end{isabelle}
7.28 and model checking algorithm
7.29 \begin{isabelle}%
7.30 -\ \ \ \ \ mc{\isacharparenleft}f\ U\ g{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}{\isachardot}{\isachardot}{\isachardot}{\isachardot}{\isachardot}{\isachardot}{\isachardot}{\isachardot}{\isachardot}{\isachardot}{\isachardot}{\isachardot}{\isacharparenright}%
7.31 +\ \ \ \ \ 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}%
7.32 \end{isabelle}
7.33 -Prove that the equivalence between semantics and model checking still holds.
7.34 +Prove the equivalence between semantics and model checking, i.e.\
7.35 +\isa{mc\ {\isacharparenleft}EU\ f\ g{\isacharparenright}\ {\isacharequal}\ {\isacharbraceleft}s{\isachardot}\ s\ {\isasymTurnstile}\ EU\ f\ g{\isacharbraceright}}.
7.36 +
7.37 +For readability you may want to equip \isa{EU} with the following customary syntax:
7.38 +\isa{E{\isacharbrackleft}f\ U\ g{\isacharbrackright}}.
7.39 \end{exercise}
7.40
7.41 Let us close this section with a few words about the executability of \isa{mc}.
8.1 --- a/doc-src/TutorialI/CTL/document/PDL.tex Mon Oct 09 17:40:47 2000 +0200
8.2 +++ b/doc-src/TutorialI/CTL/document/PDL.tex Mon Oct 09 19:20:55 2000 +0200
8.3 @@ -2,9 +2,10 @@
8.4 \begin{isabellebody}%
8.5 \def\isabellecontext{PDL}%
8.6 %
8.7 -\isamarkupsubsection{Propositional dynmic logic---PDL}
8.8 +\isamarkupsubsection{Propositional dynamic logic---PDL}
8.9 %
8.10 \begin{isamarkuptext}%
8.11 +\index{PDL|(}
8.12 The formulae of PDL are built up from atomic propositions via the customary
8.13 propositional connectives of negation and conjunction and the two temporal
8.14 connectives \isa{AX} and \isa{EF}. Since formulae are essentially
8.15 @@ -188,7 +189,8 @@
8.16 \begin{isabelle}%
8.17 \ \ \ \ \ s\ {\isasymTurnstile}\ EF\ f\ {\isacharequal}\ {\isacharparenleft}s\ {\isasymTurnstile}\ f\ {\isasymor}\ s\ {\isasymTurnstile}\ EN\ {\isacharparenleft}EF\ f{\isacharparenright}{\isacharparenright}%
8.18 \end{isabelle}
8.19 -\end{exercise}%
8.20 +\end{exercise}
8.21 +\index{PDL|)}%
8.22 \end{isamarkuptext}%
8.23 \end{isabellebody}%
8.24 %%% Local Variables:
9.1 --- a/doc-src/TutorialI/Datatype/Nested.thy Mon Oct 09 17:40:47 2000 +0200
9.2 +++ b/doc-src/TutorialI/Datatype/Nested.thy Mon Oct 09 19:20:55 2000 +0200
9.3 @@ -78,9 +78,9 @@
9.4 \begin{exercise}
9.5 The fact that substitution distributes over composition can be expressed
9.6 roughly as follows:
9.7 -@{text[display]"subst (f o g) t = subst f (subst g t)"}
9.8 +@{text[display]"subst (f \<circ> g) t = subst f (subst g t)"}
9.9 Correct this statement (you will find that it does not type-check),
9.10 -strengthen it, and prove it. (Note: \isaindexbold{o} is function composition;
9.11 +strengthen it, and prove it. (Note: @{text"\<circ>"} is function composition;
9.12 its definition is found in theorem @{thm[source]o_def}).
9.13 \end{exercise}
9.14 \begin{exercise}\label{ex:trev-trev}
10.1 --- a/doc-src/TutorialI/Datatype/document/Nested.tex Mon Oct 09 17:40:47 2000 +0200
10.2 +++ b/doc-src/TutorialI/Datatype/document/Nested.tex Mon Oct 09 19:20:55 2000 +0200
10.3 @@ -75,10 +75,10 @@
10.4 The fact that substitution distributes over composition can be expressed
10.5 roughly as follows:
10.6 \begin{isabelle}%
10.7 -\ \ \ \ \ subst\ {\isacharparenleft}f\ o\ g{\isacharparenright}\ t\ {\isacharequal}\ subst\ f\ {\isacharparenleft}subst\ g\ t{\isacharparenright}%
10.8 +\ \ \ \ \ subst\ {\isacharparenleft}f\ {\isasymcirc}\ g{\isacharparenright}\ t\ {\isacharequal}\ subst\ f\ {\isacharparenleft}subst\ g\ t{\isacharparenright}%
10.9 \end{isabelle}
10.10 Correct this statement (you will find that it does not type-check),
10.11 -strengthen it, and prove it. (Note: \isaindexbold{o} is function composition;
10.12 +strengthen it, and prove it. (Note: \isa{{\isasymcirc}} is function composition;
10.13 its definition is found in theorem \isa{o{\isacharunderscore}def}).
10.14 \end{exercise}
10.15 \begin{exercise}\label{ex:trev-trev}
11.1 --- a/doc-src/TutorialI/Recdef/simplification.thy Mon Oct 09 17:40:47 2000 +0200
11.2 +++ b/doc-src/TutorialI/Recdef/simplification.thy Mon Oct 09 19:20:55 2000 +0200
11.3 @@ -60,7 +60,7 @@
11.4 may not be expressible by pattern matching.
11.5
11.6 A very simple alternative is to replace @{text if} by @{text case}, which
11.7 -is also available for @{typ"bool"} but is not split automatically:
11.8 +is also available for @{typ bool} but is not split automatically:
11.9 *}
11.10
11.11 consts gcd2 :: "nat\<times>nat \<Rightarrow> nat";
12.1 --- a/doc-src/TutorialI/appendix.tex Mon Oct 09 17:40:47 2000 +0200
12.2 +++ b/doc-src/TutorialI/appendix.tex Mon Oct 09 19:20:55 2000 +0200
12.3 @@ -54,10 +54,10 @@
12.4 \verb$\<exists>!$\\
12.5 \indexboldpos{\isasymepsilon}{$HOL0ExSome} &
12.6 \ttindexbold{SOME} &
12.7 -\verb$\<?>$\\
12.8 +\verb$\<epsilon>$\\
12.9 \indexboldpos{\isasymcirc}{$HOL1} &
12.10 \ttindexbold{o} &
12.11 -\verb$\<?>$\\
12.12 +\verb$\<circ>$\\
12.13 \indexboldpos{\isasymle}{$HOL2arithrel}&
12.14 \ttindexboldpos{<=}{$HOL2arithrel}&
12.15 \verb$\<le>$\\
13.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
13.2 +++ b/doc-src/TutorialI/sets.tex Mon Oct 09 19:20:55 2000 +0200
13.3 @@ -0,0 +1,3 @@
13.4 +\chapter{Sets, Functions and Relations}
13.5 +
13.6 +\input{CTL/ctl}
13.7 \ No newline at end of file
14.1 --- a/doc-src/TutorialI/tutorial.tex Mon Oct 09 17:40:47 2000 +0200
14.2 +++ b/doc-src/TutorialI/tutorial.tex Mon Oct 09 19:20:55 2000 +0200
14.3 @@ -47,8 +47,8 @@
14.4 \\ \vspace{0.5cm} The Tutorial
14.5 \\ --- DRAFT ---}
14.6 \author{Tobias Nipkow\\
14.7 -Technische Universit\"at M\"unchen \\
14.8 -Institut f\"ur Informatik \\
14.9 +Technische Universit{\"a}t M{\"u}nchen \\
14.10 +Institut f{\"u}r Informatik \\
14.11 \url{http://www.in.tum.de/~nipkow/}}
14.12 \maketitle
14.13
14.14 @@ -57,7 +57,7 @@
14.15
14.16 \subsubsection*{Acknowledgements}
14.17 This tutorial owes a lot to the constant discussions with and the valuable
14.18 -feedback from Larry Paulson and the Isabelle group at Munich: Olaf M\"uller,
14.19 +feedback from Larry Paulson and the Isabelle group at Munich: Olaf M{\"u}ller,
14.20 Wolfgang Naraschewski, David von Oheimb, Leonor Prensa Nieto, Cornelia Pusch
14.21 and Markus Wenzel. Stefan Berghofer and Stephan Merz were also kind enough to
14.22 read and comment on a draft version.
14.23 @@ -65,8 +65,15 @@
14.24
14.25 \input{basics}
14.26 \input{fp}
14.27 -\input{CTL/ctl}
14.28 +\chapter{The Rules of the Game}
14.29 +\input{sets}
14.30 +\chapter{Inductively Defined Sets}
14.31 \input{Advanced/advanced}
14.32 +\chapter{More about Types}
14.33 +\chapter{Theory Presentation}
14.34 +\chapter{Case Study: The Needhamd-Schroeder Protocol}
14.35 +\chapter{Structured Proofs}
14.36 +\chapter{Case Study: UNIX File-System Security}
14.37 %\chapter{The Tricks of the Trade}
14.38 \input{appendix}
14.39