*** empty log message ***
authornipkow
Mon Oct 09 19:20:55 2000 +0200 (2000-10-09)
changeset 10178aecb5bf6f76f
parent 10177 383b0a1837a9
child 10179 9d5678e6bf34
*** empty log message ***
doc-src/TutorialI/Advanced/advanced.tex
doc-src/TutorialI/CTL/Base.thy
doc-src/TutorialI/CTL/CTL.thy
doc-src/TutorialI/CTL/PDL.thy
doc-src/TutorialI/CTL/ctl.tex
doc-src/TutorialI/CTL/document/Base.tex
doc-src/TutorialI/CTL/document/CTL.tex
doc-src/TutorialI/CTL/document/PDL.tex
doc-src/TutorialI/Datatype/Nested.thy
doc-src/TutorialI/Datatype/document/Nested.tex
doc-src/TutorialI/Recdef/simplification.thy
doc-src/TutorialI/appendix.tex
doc-src/TutorialI/sets.tex
doc-src/TutorialI/tutorial.tex
     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