diff -r 1fead823c7c6 -r 6e15de7dd871 doc-src/TutorialI/document/Base.tex
--- a/doc-src/TutorialI/document/Base.tex	Tue Aug 28 13:15:15 2012 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,130 +0,0 @@
-%
-\begin{isabellebody}%
-\def\isabellecontext{Base}%
-%
-\isadelimtheory
-%
-\endisadelimtheory
-%
-\isatagtheory
-%
-\endisatagtheory
-{\isafoldtheory}%
-%
-\isadelimtheory
-%
-\endisadelimtheory
-%
-\isamarkupsection{Case Study: Verified Model Checking%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-\label{sec:VMC}
-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 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)\@.  We then proceed to the temporal logic CTL, which is
-used in many real
-model checkers. In each case we give both a traditional semantics (\isa{{\isaliteral{5C3C5475726E7374696C653E}{\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: 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
-
-Our models are \emph{transition systems}:\index{transition systems}
-sets of \emph{states} with
-transitions between them.  Here is a simple example:
-\begin{center}
-\unitlength.5mm
-\thicklines
-\begin{picture}(100,60)
-\put(50,50){\circle{20}}
-\put(50,50){\makebox(0,0){$p,q$}}
-\put(61,55){\makebox(0,0)[l]{$s_0$}}
-\put(44,42){\vector(-1,-1){26}}
-\put(16,18){\vector(1,1){26}}
-\put(57,43){\vector(1,-1){26}}
-\put(10,10){\circle{20}}
-\put(10,10){\makebox(0,0){$q,r$}}
-\put(-1,15){\makebox(0,0)[r]{$s_1$}}
-\put(20,10){\vector(1,0){60}}
-\put(90,10){\circle{20}}
-\put(90,10){\makebox(0,0){$r$}}
-\put(98, 5){\line(1,0){10}}
-\put(108, 5){\line(0,1){10}}
-\put(108,15){\vector(-1,0){10}}
-\put(91,21){\makebox(0,0)[bl]{$s_2$}}
-\end{picture}
-\end{center}
-Each state has a unique name or number ($s_0,s_1,s_2$), and in each state
-certain \emph{atomic propositions} ($p,q,r$) hold.  The aim of temporal logic
-is to formalize statements such as ``there is no path starting from $s_2$
-leading to a state where $p$ or $q$ holds,'' which is true, and ``on all paths
-starting from $s_0$, $q$ always holds,'' which is false.
-
-Abstracting from this concrete example, we assume there is a type of
-states:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-\isacommand{typedecl}\isamarkupfalse%
-\ state%
-\begin{isamarkuptext}%
-\noindent
-Command \commdx{typedecl} merely declares a new type but without
-defining it (see \S\ref{sec:typedecl}). Thus we know nothing
-about the type other than its existence. That is exactly what we need
-because \isa{state} really is an implicit parameter of our model.  Of
-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.\ a relation between states:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-\isacommand{consts}\isamarkupfalse%
-\ M\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}state\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ state{\isaliteral{29}{\isacharparenright}}set{\isaliteral{22}{\isachardoublequoteclose}}%
-\begin{isamarkuptext}%
-\noindent
-This is Isabelle's way of declaring a constant without defining it.
-Finally we introduce a type of atomic propositions%
-\end{isamarkuptext}%
-\isamarkuptrue%
-\isacommand{typedecl}\isamarkupfalse%
-\ {\isaliteral{22}{\isachardoublequoteopen}}atom{\isaliteral{22}{\isachardoublequoteclose}}%
-\begin{isamarkuptext}%
-\noindent
-and a \emph{labelling function}%
-\end{isamarkuptext}%
-\isamarkuptrue%
-\isacommand{consts}\isamarkupfalse%
-\ L\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}state\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ atom\ set{\isaliteral{22}{\isachardoublequoteclose}}%
-\begin{isamarkuptext}%
-\noindent
-telling us which atomic propositions are true in each state.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isadelimtheory
-%
-\endisadelimtheory
-%
-\isatagtheory
-%
-\endisatagtheory
-{\isafoldtheory}%
-%
-\isadelimtheory
-%
-\endisadelimtheory
-\end{isabellebody}%
-%%% Local Variables:
-%%% mode: latex
-%%% TeX-master: "root"
-%%% End: