# HG changeset patch # User nipkow # Date 971112055 -7200 # Node ID aecb5bf6f76f1d5e21a7ec2e744b02c21c7b4827 # Parent 383b0a1837a91fcf4e0cd9099b8476c174f8279e *** empty log message *** diff -r 383b0a1837a9 -r aecb5bf6f76f doc-src/TutorialI/Advanced/advanced.tex --- 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 diff -r 383b0a1837a9 -r aecb5bf6f76f doc-src/TutorialI/CTL/Base.thy --- 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 \}) and a recursive function @{term mc} that maps a formula into the set of all states of diff -r 383b0a1837a9 -r aecb5bf6f76f doc-src/TutorialI/CTL/CTL.thy --- 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 \ 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 \ EU f g = (\p\Paths s. \j. p j \ g \ (\i < j. p i \ 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(\T. mc g \ mc f \ (M^-1 ^^ T))"} +Prove the equivalence between semantics and model checking, i.e.\ +@{prop"mc(EU f g) = {s. s \ 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}. diff -r 383b0a1837a9 -r aecb5bf6f76f doc-src/TutorialI/CTL/PDL.thy --- 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. \t. (s,t) \ M \ t \ mc f}" "mc(EF f) = lfp(\T. mc f \ 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 \ EF f) = (s \ f | s \ EN(EF f))"} \end{exercise} +\index{PDL|)} *} (*<*) theorem main: "mc f = {s. s \ f}"; diff -r 383b0a1837a9 -r aecb5bf6f76f doc-src/TutorialI/CTL/ctl.tex --- 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|)} diff -r 383b0a1837a9 -r aecb5bf6f76f doc-src/TutorialI/CTL/document/Base.tex --- 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 diff -r 383b0a1837a9 -r aecb5bf6f76f doc-src/TutorialI/CTL/document/CTL.tex --- 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}. diff -r 383b0a1837a9 -r aecb5bf6f76f doc-src/TutorialI/CTL/document/PDL.tex --- 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: diff -r 383b0a1837a9 -r aecb5bf6f76f doc-src/TutorialI/Datatype/Nested.thy --- 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 \ 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"\"} is function composition; its definition is found in theorem @{thm[source]o_def}). \end{exercise} \begin{exercise}\label{ex:trev-trev} diff -r 383b0a1837a9 -r aecb5bf6f76f doc-src/TutorialI/Datatype/document/Nested.tex --- 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} diff -r 383b0a1837a9 -r aecb5bf6f76f doc-src/TutorialI/Recdef/simplification.thy --- 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\nat \ nat"; diff -r 383b0a1837a9 -r aecb5bf6f76f doc-src/TutorialI/appendix.tex --- 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$\!$\\ \indexboldpos{\isasymepsilon}{$HOL0ExSome} & \ttindexbold{SOME} & -\verb$\$\\ +\verb$\$\\ \indexboldpos{\isasymcirc}{$HOL1} & \ttindexbold{o} & -\verb$\$\\ +\verb$\$\\ \indexboldpos{\isasymle}{$HOL2arithrel}& \ttindexboldpos{<=}{$HOL2arithrel}& \verb$\$\\ diff -r 383b0a1837a9 -r aecb5bf6f76f doc-src/TutorialI/sets.tex --- /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 diff -r 383b0a1837a9 -r aecb5bf6f76f doc-src/TutorialI/tutorial.tex --- 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}