doc-src/TutorialI/CTL/document/CTL.tex
author haftmann
Tue, 03 May 2005 15:37:41 +0200
changeset 15920 c79fa63504c8
parent 15904 a6fb4ddc05c7
child 16069 3f2a9f400168
permissions -rw-r--r--
make mkdir usable with cygwin
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
10123
9469c039ff57 *** empty log message ***
nipkow
parents:
diff changeset
     1
%
9469c039ff57 *** empty log message ***
nipkow
parents:
diff changeset
     2
\begin{isabellebody}%
9469c039ff57 *** empty log message ***
nipkow
parents:
diff changeset
     3
\def\isabellecontext{CTL}%
11866
fbd097aec213 updated;
wenzelm
parents: 11706
diff changeset
     4
\isamarkupfalse%
10133
e187dacd248f *** empty log message ***
nipkow
parents: 10123
diff changeset
     5
%
10971
6852682eaf16 *** empty log message ***
nipkow
parents: 10950
diff changeset
     6
\isamarkupsubsection{Computation Tree Logic --- CTL%
10395
7ef380745743 updated;
wenzelm
parents: 10363
diff changeset
     7
}
11866
fbd097aec213 updated;
wenzelm
parents: 11706
diff changeset
     8
\isamarkuptrue%
10149
7cfdf6a330a0 *** empty log message ***
nipkow
parents: 10133
diff changeset
     9
%
7cfdf6a330a0 *** empty log message ***
nipkow
parents: 10133
diff changeset
    10
\begin{isamarkuptext}%
10217
e61e7e1eacaf *** empty log message ***
nipkow
parents: 10212
diff changeset
    11
\label{sec:CTL}
11494
23a118849801 revisions and indexing
paulson
parents: 11231
diff changeset
    12
\index{CTL|(}%
10867
bda1701848cd lcp's suggestions for CTL
paulson
parents: 10866
diff changeset
    13
The semantics of PDL only needs reflexive transitive closure.
bda1701848cd lcp's suggestions for CTL
paulson
parents: 10866
diff changeset
    14
Let us be adventurous and introduce a more expressive temporal operator.
bda1701848cd lcp's suggestions for CTL
paulson
parents: 10866
diff changeset
    15
We extend the datatype
10149
7cfdf6a330a0 *** empty log message ***
nipkow
parents: 10133
diff changeset
    16
\isa{formula} by a new constructor%
7cfdf6a330a0 *** empty log message ***
nipkow
parents: 10133
diff changeset
    17
\end{isamarkuptext}%
11866
fbd097aec213 updated;
wenzelm
parents: 11706
diff changeset
    18
\isamarkuptrue%
fbd097aec213 updated;
wenzelm
parents: 11706
diff changeset
    19
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharbar}\ AF\ formula\isamarkupfalse%
fbd097aec213 updated;
wenzelm
parents: 11706
diff changeset
    20
%
10149
7cfdf6a330a0 *** empty log message ***
nipkow
parents: 10133
diff changeset
    21
\begin{isamarkuptext}%
7cfdf6a330a0 *** empty log message ***
nipkow
parents: 10133
diff changeset
    22
\noindent
10983
59961d32b1ae *** empty log message ***
nipkow
parents: 10971
diff changeset
    23
which stands for ``\emph{A}lways in the \emph{F}uture'':
59961d32b1ae *** empty log message ***
nipkow
parents: 10971
diff changeset
    24
on all infinite paths, at some point the formula holds.
59961d32b1ae *** empty log message ***
nipkow
parents: 10971
diff changeset
    25
Formalizing the notion of an infinite path is easy
10159
a72ddfdbfca0 *** empty log message ***
nipkow
parents: 10149
diff changeset
    26
in HOL: it is simply a function from \isa{nat} to \isa{state}.%
10149
7cfdf6a330a0 *** empty log message ***
nipkow
parents: 10133
diff changeset
    27
\end{isamarkuptext}%
11866
fbd097aec213 updated;
wenzelm
parents: 11706
diff changeset
    28
\isamarkuptrue%
10123
9469c039ff57 *** empty log message ***
nipkow
parents:
diff changeset
    29
\isacommand{constdefs}\ Paths\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}state\ {\isasymRightarrow}\ {\isacharparenleft}nat\ {\isasymRightarrow}\ state{\isacharparenright}set{\isachardoublequote}\isanewline
11866
fbd097aec213 updated;
wenzelm
parents: 11706
diff changeset
    30
\ \ \ \ \ \ \ \ \ {\isachardoublequote}Paths\ s\ {\isasymequiv}\ {\isacharbraceleft}p{\isachardot}\ s\ {\isacharequal}\ p\ {\isadigit{0}}\ {\isasymand}\ {\isacharparenleft}{\isasymforall}i{\isachardot}\ {\isacharparenleft}p\ i{\isacharcomma}\ p{\isacharparenleft}i{\isacharplus}{\isadigit{1}}{\isacharparenright}{\isacharparenright}\ {\isasymin}\ M{\isacharparenright}{\isacharbraceright}{\isachardoublequote}\isamarkupfalse%
fbd097aec213 updated;
wenzelm
parents: 11706
diff changeset
    31
%
10149
7cfdf6a330a0 *** empty log message ***
nipkow
parents: 10133
diff changeset
    32
\begin{isamarkuptext}%
7cfdf6a330a0 *** empty log message ***
nipkow
parents: 10133
diff changeset
    33
\noindent
11494
23a118849801 revisions and indexing
paulson
parents: 11231
diff changeset
    34
This definition allows a succinct statement of the semantics of \isa{AF}:
10867
bda1701848cd lcp's suggestions for CTL
paulson
parents: 10866
diff changeset
    35
\footnote{Do not be misled: neither datatypes nor recursive functions can be
10149
7cfdf6a330a0 *** empty log message ***
nipkow
parents: 10133
diff changeset
    36
extended by new constructors or equations. This is just a trick of the
12815
wenzelm
parents: 12699
diff changeset
    37
presentation (see \S\ref{sec:doc-prep-suppress}). In reality one has to define
wenzelm
parents: 12699
diff changeset
    38
a new datatype and a new function.}%
10149
7cfdf6a330a0 *** empty log message ***
nipkow
parents: 10133
diff changeset
    39
\end{isamarkuptext}%
11866
fbd097aec213 updated;
wenzelm
parents: 11706
diff changeset
    40
\isamarkuptrue%
fbd097aec213 updated;
wenzelm
parents: 11706
diff changeset
    41
\isamarkupfalse%
fbd097aec213 updated;
wenzelm
parents: 11706
diff changeset
    42
{\isachardoublequote}s\ {\isasymTurnstile}\ AF\ f\ \ \ \ {\isacharequal}\ {\isacharparenleft}{\isasymforall}p\ {\isasymin}\ Paths\ s{\isachardot}\ {\isasymexists}i{\isachardot}\ p\ i\ {\isasymTurnstile}\ f{\isacharparenright}{\isachardoublequote}\isamarkupfalse%
fbd097aec213 updated;
wenzelm
parents: 11706
diff changeset
    43
%
10149
7cfdf6a330a0 *** empty log message ***
nipkow
parents: 10133
diff changeset
    44
\begin{isamarkuptext}%
7cfdf6a330a0 *** empty log message ***
nipkow
parents: 10133
diff changeset
    45
\noindent
7cfdf6a330a0 *** empty log message ***
nipkow
parents: 10133
diff changeset
    46
Model checking \isa{AF} involves a function which
10159
a72ddfdbfca0 *** empty log message ***
nipkow
parents: 10149
diff changeset
    47
is just complicated enough to warrant a separate definition:%
10149
7cfdf6a330a0 *** empty log message ***
nipkow
parents: 10133
diff changeset
    48
\end{isamarkuptext}%
11866
fbd097aec213 updated;
wenzelm
parents: 11706
diff changeset
    49
\isamarkuptrue%
10123
9469c039ff57 *** empty log message ***
nipkow
parents:
diff changeset
    50
\isacommand{constdefs}\ af\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}state\ set\ {\isasymRightarrow}\ state\ set\ {\isasymRightarrow}\ state\ set{\isachardoublequote}\isanewline
11866
fbd097aec213 updated;
wenzelm
parents: 11706
diff changeset
    51
\ \ \ \ \ \ \ \ \ {\isachardoublequote}af\ A\ T\ {\isasymequiv}\ A\ {\isasymunion}\ {\isacharbraceleft}s{\isachardot}\ {\isasymforall}t{\isachardot}\ {\isacharparenleft}s{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\ {\isasymlongrightarrow}\ t\ {\isasymin}\ T{\isacharbraceright}{\isachardoublequote}\isamarkupfalse%
fbd097aec213 updated;
wenzelm
parents: 11706
diff changeset
    52
%
10149
7cfdf6a330a0 *** empty log message ***
nipkow
parents: 10133
diff changeset
    53
\begin{isamarkuptext}%
7cfdf6a330a0 *** empty log message ***
nipkow
parents: 10133
diff changeset
    54
\noindent
10867
bda1701848cd lcp's suggestions for CTL
paulson
parents: 10866
diff changeset
    55
Now we define \isa{mc\ {\isacharparenleft}AF\ f{\isacharparenright}} as the least set \isa{T} that includes
10159
a72ddfdbfca0 *** empty log message ***
nipkow
parents: 10149
diff changeset
    56
\isa{mc\ f} and all states all of whose direct successors are in \isa{T}:%
a72ddfdbfca0 *** empty log message ***
nipkow
parents: 10149
diff changeset
    57
\end{isamarkuptext}%
11866
fbd097aec213 updated;
wenzelm
parents: 11706
diff changeset
    58
\isamarkuptrue%
fbd097aec213 updated;
wenzelm
parents: 11706
diff changeset
    59
\isamarkupfalse%
fbd097aec213 updated;
wenzelm
parents: 11706
diff changeset
    60
{\isachardoublequote}mc{\isacharparenleft}AF\ f{\isacharparenright}\ \ \ \ {\isacharequal}\ lfp{\isacharparenleft}af{\isacharparenleft}mc\ f{\isacharparenright}{\isacharparenright}{\isachardoublequote}\isamarkupfalse%
fbd097aec213 updated;
wenzelm
parents: 11706
diff changeset
    61
%
10159
a72ddfdbfca0 *** empty log message ***
nipkow
parents: 10149
diff changeset
    62
\begin{isamarkuptext}%
a72ddfdbfca0 *** empty log message ***
nipkow
parents: 10149
diff changeset
    63
\noindent
a72ddfdbfca0 *** empty log message ***
nipkow
parents: 10149
diff changeset
    64
Because \isa{af} is monotone in its second argument (and also its first, but
10983
59961d32b1ae *** empty log message ***
nipkow
parents: 10971
diff changeset
    65
that is irrelevant), \isa{af\ A} has a least fixed point:%
10149
7cfdf6a330a0 *** empty log message ***
nipkow
parents: 10133
diff changeset
    66
\end{isamarkuptext}%
11866
fbd097aec213 updated;
wenzelm
parents: 11706
diff changeset
    67
\isamarkuptrue%
10123
9469c039ff57 *** empty log message ***
nipkow
parents:
diff changeset
    68
\isacommand{lemma}\ mono{\isacharunderscore}af{\isacharcolon}\ {\isachardoublequote}mono{\isacharparenleft}af\ A{\isacharparenright}{\isachardoublequote}\isanewline
11866
fbd097aec213 updated;
wenzelm
parents: 11706
diff changeset
    69
\isamarkupfalse%
15488
7c638a46dcbb tidying of some subst/simplesubst proofs
paulson
parents: 15106
diff changeset
    70
\isamarkupfalse%
11866
fbd097aec213 updated;
wenzelm
parents: 11706
diff changeset
    71
\isamarkupfalse%
15904
a6fb4ddc05c7 introduced @{const ...} antiquotation
haftmann
parents: 15488
diff changeset
    72
\isanewline
a6fb4ddc05c7 introduced @{const ...} antiquotation
haftmann
parents: 15488
diff changeset
    73
\isamarkupfalse%
a6fb4ddc05c7 introduced @{const ...} antiquotation
haftmann
parents: 15488
diff changeset
    74
\isamarkupfalse%
a6fb4ddc05c7 introduced @{const ...} antiquotation
haftmann
parents: 15488
diff changeset
    75
\isamarkupfalse%
a6fb4ddc05c7 introduced @{const ...} antiquotation
haftmann
parents: 15488
diff changeset
    76
\isanewline
11866
fbd097aec213 updated;
wenzelm
parents: 11706
diff changeset
    77
\isamarkupfalse%
fbd097aec213 updated;
wenzelm
parents: 11706
diff changeset
    78
\isamarkupfalse%
fbd097aec213 updated;
wenzelm
parents: 11706
diff changeset
    79
\isamarkupfalse%
fbd097aec213 updated;
wenzelm
parents: 11706
diff changeset
    80
\isamarkupfalse%
fbd097aec213 updated;
wenzelm
parents: 11706
diff changeset
    81
\isamarkupfalse%
fbd097aec213 updated;
wenzelm
parents: 11706
diff changeset
    82
\isamarkupfalse%
fbd097aec213 updated;
wenzelm
parents: 11706
diff changeset
    83
\isamarkupfalse%
fbd097aec213 updated;
wenzelm
parents: 11706
diff changeset
    84
\isamarkupfalse%
fbd097aec213 updated;
wenzelm
parents: 11706
diff changeset
    85
\isamarkupfalse%
fbd097aec213 updated;
wenzelm
parents: 11706
diff changeset
    86
\isamarkupfalse%
fbd097aec213 updated;
wenzelm
parents: 11706
diff changeset
    87
\isamarkupfalse%
fbd097aec213 updated;
wenzelm
parents: 11706
diff changeset
    88
\isamarkupfalse%
fbd097aec213 updated;
wenzelm
parents: 11706
diff changeset
    89
\isamarkupfalse%
fbd097aec213 updated;
wenzelm
parents: 11706
diff changeset
    90
\isamarkupfalse%
fbd097aec213 updated;
wenzelm
parents: 11706
diff changeset
    91
\isamarkupfalse%
15904
a6fb4ddc05c7 introduced @{const ...} antiquotation
haftmann
parents: 15488
diff changeset
    92
\isanewline
11866
fbd097aec213 updated;
wenzelm
parents: 11706
diff changeset
    93
\isamarkupfalse%
fbd097aec213 updated;
wenzelm
parents: 11706
diff changeset
    94
%
10149
7cfdf6a330a0 *** empty log message ***
nipkow
parents: 10133
diff changeset
    95
\begin{isamarkuptext}%
10867
bda1701848cd lcp's suggestions for CTL
paulson
parents: 10866
diff changeset
    96
All we need to prove now is  \isa{mc\ {\isacharparenleft}AF\ f{\isacharparenright}\ {\isacharequal}\ {\isacharbraceleft}s{\isachardot}\ s\ {\isasymTurnstile}\ AF\ f{\isacharbraceright}}, which states
bda1701848cd lcp's suggestions for CTL
paulson
parents: 10866
diff changeset
    97
that \isa{mc} and \isa{{\isasymTurnstile}} agree for \isa{AF}\@.
bda1701848cd lcp's suggestions for CTL
paulson
parents: 10866
diff changeset
    98
This time we prove the two inclusions separately, starting
10159
a72ddfdbfca0 *** empty log message ***
nipkow
parents: 10149
diff changeset
    99
with the easy one:%
a72ddfdbfca0 *** empty log message ***
nipkow
parents: 10149
diff changeset
   100
\end{isamarkuptext}%
11866
fbd097aec213 updated;
wenzelm
parents: 11706
diff changeset
   101
\isamarkuptrue%
10187
0376cccd9118 *** empty log message ***
nipkow
parents: 10186
diff changeset
   102
\isacommand{theorem}\ AF{\isacharunderscore}lemma{\isadigit{1}}{\isacharcolon}\isanewline
12328
7c4ec77a8715 *** empty log message ***
nipkow
parents: 11866
diff changeset
   103
\ \ {\isachardoublequote}lfp{\isacharparenleft}af\ A{\isacharparenright}\ {\isasymsubseteq}\ {\isacharbraceleft}s{\isachardot}\ {\isasymforall}p\ {\isasymin}\ Paths\ s{\isachardot}\ {\isasymexists}i{\isachardot}\ p\ i\ {\isasymin}\ A{\isacharbraceright}{\isachardoublequote}\isamarkupfalse%
11866
fbd097aec213 updated;
wenzelm
parents: 11706
diff changeset
   104
\isamarkuptrue%
15488
7c638a46dcbb tidying of some subst/simplesubst proofs
paulson
parents: 15106
diff changeset
   105
\isamarkupfalse%
11866
fbd097aec213 updated;
wenzelm
parents: 11706
diff changeset
   106
\isamarkupfalse%
fbd097aec213 updated;
wenzelm
parents: 11706
diff changeset
   107
\isamarkuptrue%
15488
7c638a46dcbb tidying of some subst/simplesubst proofs
paulson
parents: 15106
diff changeset
   108
\isamarkupfalse%
11866
fbd097aec213 updated;
wenzelm
parents: 11706
diff changeset
   109
\isamarkupfalse%
fbd097aec213 updated;
wenzelm
parents: 11706
diff changeset
   110
\isamarkupfalse%
fbd097aec213 updated;
wenzelm
parents: 11706
diff changeset
   111
%
10123
9469c039ff57 *** empty log message ***
nipkow
parents:
diff changeset
   112
\begin{isamarkuptext}%
10867
bda1701848cd lcp's suggestions for CTL
paulson
parents: 10866
diff changeset
   113
The opposite inclusion is proved by contradiction: if some state
10159
a72ddfdbfca0 *** empty log message ***
nipkow
parents: 10149
diff changeset
   114
\isa{s} is not in \isa{lfp\ {\isacharparenleft}af\ A{\isacharparenright}}, then we can construct an
11494
23a118849801 revisions and indexing
paulson
parents: 11231
diff changeset
   115
infinite \isa{A}-avoiding path starting from~\isa{s}. The reason is
10123
9469c039ff57 *** empty log message ***
nipkow
parents:
diff changeset
   116
that by unfolding \isa{lfp} we find that if \isa{s} is not in
9469c039ff57 *** empty log message ***
nipkow
parents:
diff changeset
   117
\isa{lfp\ {\isacharparenleft}af\ A{\isacharparenright}}, then \isa{s} is not in \isa{A} and there is a
10983
59961d32b1ae *** empty log message ***
nipkow
parents: 10971
diff changeset
   118
direct successor of \isa{s} that is again not in \mbox{\isa{lfp\ {\isacharparenleft}af\ A{\isacharparenright}}}. Iterating this argument yields the promised infinite
10123
9469c039ff57 *** empty log message ***
nipkow
parents:
diff changeset
   119
\isa{A}-avoiding path. Let us formalize this sketch.
9469c039ff57 *** empty log message ***
nipkow
parents:
diff changeset
   120
10867
bda1701848cd lcp's suggestions for CTL
paulson
parents: 10866
diff changeset
   121
The one-step argument in the sketch above
bda1701848cd lcp's suggestions for CTL
paulson
parents: 10866
diff changeset
   122
is proved by a variant of contraposition:%
10123
9469c039ff57 *** empty log message ***
nipkow
parents:
diff changeset
   123
\end{isamarkuptext}%
11866
fbd097aec213 updated;
wenzelm
parents: 11706
diff changeset
   124
\isamarkuptrue%
10123
9469c039ff57 *** empty log message ***
nipkow
parents:
diff changeset
   125
\isacommand{lemma}\ not{\isacharunderscore}in{\isacharunderscore}lfp{\isacharunderscore}afD{\isacharcolon}\isanewline
10983
59961d32b1ae *** empty log message ***
nipkow
parents: 10971
diff changeset
   126
\ {\isachardoublequote}s\ {\isasymnotin}\ lfp{\isacharparenleft}af\ A{\isacharparenright}\ {\isasymLongrightarrow}\ s\ {\isasymnotin}\ A\ {\isasymand}\ {\isacharparenleft}{\isasymexists}\ t{\isachardot}\ {\isacharparenleft}s{\isacharcomma}t{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ t\ {\isasymnotin}\ lfp{\isacharparenleft}af\ A{\isacharparenright}{\isacharparenright}{\isachardoublequote}\isanewline
11866
fbd097aec213 updated;
wenzelm
parents: 11706
diff changeset
   127
\isamarkupfalse%
fbd097aec213 updated;
wenzelm
parents: 11706
diff changeset
   128
\isamarkupfalse%
fbd097aec213 updated;
wenzelm
parents: 11706
diff changeset
   129
\isamarkupfalse%
fbd097aec213 updated;
wenzelm
parents: 11706
diff changeset
   130
\isamarkupfalse%
15488
7c638a46dcbb tidying of some subst/simplesubst proofs
paulson
parents: 15106
diff changeset
   131
\isamarkupfalse%
11866
fbd097aec213 updated;
wenzelm
parents: 11706
diff changeset
   132
%
10123
9469c039ff57 *** empty log message ***
nipkow
parents:
diff changeset
   133
\begin{isamarkuptext}%
9469c039ff57 *** empty log message ***
nipkow
parents:
diff changeset
   134
\noindent
10867
bda1701848cd lcp's suggestions for CTL
paulson
parents: 10866
diff changeset
   135
We assume the negation of the conclusion and prove \isa{s\ {\isasymin}\ lfp\ {\isacharparenleft}af\ A{\isacharparenright}}.
10237
875bf54b5d74 *** empty log message ***
nipkow
parents: 10225
diff changeset
   136
Unfolding \isa{lfp} once and
10123
9469c039ff57 *** empty log message ***
nipkow
parents:
diff changeset
   137
simplifying with the definition of \isa{af} finishes the proof.
9469c039ff57 *** empty log message ***
nipkow
parents:
diff changeset
   138
9469c039ff57 *** empty log message ***
nipkow
parents:
diff changeset
   139
Now we iterate this process. The following construction of the desired
10895
79194f07d356 *** empty log message ***
nipkow
parents: 10878
diff changeset
   140
path is parameterized by a predicate \isa{Q} that should hold along the path:%
10123
9469c039ff57 *** empty log message ***
nipkow
parents:
diff changeset
   141
\end{isamarkuptext}%
11866
fbd097aec213 updated;
wenzelm
parents: 11706
diff changeset
   142
\isamarkuptrue%
10123
9469c039ff57 *** empty log message ***
nipkow
parents:
diff changeset
   143
\isacommand{consts}\ path\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}state\ {\isasymRightarrow}\ {\isacharparenleft}state\ {\isasymRightarrow}\ bool{\isacharparenright}\ {\isasymRightarrow}\ {\isacharparenleft}nat\ {\isasymRightarrow}\ state{\isacharparenright}{\isachardoublequote}\isanewline
11866
fbd097aec213 updated;
wenzelm
parents: 11706
diff changeset
   144
\isamarkupfalse%
10123
9469c039ff57 *** empty log message ***
nipkow
parents:
diff changeset
   145
\isacommand{primrec}\isanewline
10895
79194f07d356 *** empty log message ***
nipkow
parents: 10878
diff changeset
   146
{\isachardoublequote}path\ s\ Q\ {\isadigit{0}}\ {\isacharequal}\ s{\isachardoublequote}\isanewline
11866
fbd097aec213 updated;
wenzelm
parents: 11706
diff changeset
   147
{\isachardoublequote}path\ s\ Q\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}SOME\ t{\isachardot}\ {\isacharparenleft}path\ s\ Q\ n{\isacharcomma}t{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ Q\ t{\isacharparenright}{\isachardoublequote}\isamarkupfalse%
fbd097aec213 updated;
wenzelm
parents: 11706
diff changeset
   148
%
10123
9469c039ff57 *** empty log message ***
nipkow
parents:
diff changeset
   149
\begin{isamarkuptext}%
9469c039ff57 *** empty log message ***
nipkow
parents:
diff changeset
   150
\noindent
12699
deae80045527 *** empty log message ***
nipkow
parents: 12489
diff changeset
   151
Element \isa{n\ {\isacharplus}\ {\isadigit{1}}} on this path is some arbitrary successor
10895
79194f07d356 *** empty log message ***
nipkow
parents: 10878
diff changeset
   152
\isa{t} of element \isa{n} such that \isa{Q\ t} holds.  Remember that \isa{SOME\ t{\isachardot}\ R\ t}
10654
458068404143 *** empty log message ***
nipkow
parents: 10645
diff changeset
   153
is some arbitrary but fixed \isa{t} such that \isa{R\ t} holds (see \S\ref{sec:SOME}). Of
10867
bda1701848cd lcp's suggestions for CTL
paulson
parents: 10866
diff changeset
   154
course, such a \isa{t} need not exist, but that is of no
bda1701848cd lcp's suggestions for CTL
paulson
parents: 10866
diff changeset
   155
concern to us since we will only use \isa{path} when a
10123
9469c039ff57 *** empty log message ***
nipkow
parents:
diff changeset
   156
suitable \isa{t} does exist.
9469c039ff57 *** empty log message ***
nipkow
parents:
diff changeset
   157
10895
79194f07d356 *** empty log message ***
nipkow
parents: 10878
diff changeset
   158
Let us show that if each state \isa{s} that satisfies \isa{Q}
79194f07d356 *** empty log message ***
nipkow
parents: 10878
diff changeset
   159
has a successor that again satisfies \isa{Q}, then there exists an infinite \isa{Q}-path:%
10123
9469c039ff57 *** empty log message ***
nipkow
parents:
diff changeset
   160
\end{isamarkuptext}%
11866
fbd097aec213 updated;
wenzelm
parents: 11706
diff changeset
   161
\isamarkuptrue%
10159
a72ddfdbfca0 *** empty log message ***
nipkow
parents: 10149
diff changeset
   162
\isacommand{lemma}\ infinity{\isacharunderscore}lemma{\isacharcolon}\isanewline
10895
79194f07d356 *** empty log message ***
nipkow
parents: 10878
diff changeset
   163
\ \ {\isachardoublequote}{\isasymlbrakk}\ Q\ s{\isacharsemicolon}\ {\isasymforall}s{\isachardot}\ Q\ s\ {\isasymlongrightarrow}\ {\isacharparenleft}{\isasymexists}\ t{\isachardot}\ {\isacharparenleft}s{\isacharcomma}t{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ Q\ t{\isacharparenright}\ {\isasymrbrakk}\ {\isasymLongrightarrow}\isanewline
11866
fbd097aec213 updated;
wenzelm
parents: 11706
diff changeset
   164
\ \ \ {\isasymexists}p{\isasymin}Paths\ s{\isachardot}\ {\isasymforall}i{\isachardot}\ Q{\isacharparenleft}p\ i{\isacharparenright}{\isachardoublequote}\isamarkupfalse%
15488
7c638a46dcbb tidying of some subst/simplesubst proofs
paulson
parents: 15106
diff changeset
   165
\isamarkuptrue%
7c638a46dcbb tidying of some subst/simplesubst proofs
paulson
parents: 15106
diff changeset
   166
\isamarkupfalse%
11866
fbd097aec213 updated;
wenzelm
parents: 11706
diff changeset
   167
\isamarkuptrue%
15488
7c638a46dcbb tidying of some subst/simplesubst proofs
paulson
parents: 15106
diff changeset
   168
\isamarkupfalse%
11866
fbd097aec213 updated;
wenzelm
parents: 11706
diff changeset
   169
\isamarkuptrue%
fbd097aec213 updated;
wenzelm
parents: 11706
diff changeset
   170
\isamarkupfalse%
15488
7c638a46dcbb tidying of some subst/simplesubst proofs
paulson
parents: 15106
diff changeset
   171
\isamarkupfalse%
11866
fbd097aec213 updated;
wenzelm
parents: 11706
diff changeset
   172
\isamarkuptrue%
15488
7c638a46dcbb tidying of some subst/simplesubst proofs
paulson
parents: 15106
diff changeset
   173
\isamarkupfalse%
7c638a46dcbb tidying of some subst/simplesubst proofs
paulson
parents: 15106
diff changeset
   174
\isamarkupfalse%
7c638a46dcbb tidying of some subst/simplesubst proofs
paulson
parents: 15106
diff changeset
   175
\isamarkuptrue%
7c638a46dcbb tidying of some subst/simplesubst proofs
paulson
parents: 15106
diff changeset
   176
\isamarkupfalse%
11866
fbd097aec213 updated;
wenzelm
parents: 11706
diff changeset
   177
\isamarkuptrue%
15488
7c638a46dcbb tidying of some subst/simplesubst proofs
paulson
parents: 15106
diff changeset
   178
\isamarkupfalse%
11866
fbd097aec213 updated;
wenzelm
parents: 11706
diff changeset
   179
\isamarkupfalse%
15488
7c638a46dcbb tidying of some subst/simplesubst proofs
paulson
parents: 15106
diff changeset
   180
\isamarkupfalse%
11866
fbd097aec213 updated;
wenzelm
parents: 11706
diff changeset
   181
\isamarkupfalse%
15488
7c638a46dcbb tidying of some subst/simplesubst proofs
paulson
parents: 15106
diff changeset
   182
\isamarkupfalse%
11866
fbd097aec213 updated;
wenzelm
parents: 11706
diff changeset
   183
\isamarkupfalse%
fbd097aec213 updated;
wenzelm
parents: 11706
diff changeset
   184
\isamarkupfalse%
fbd097aec213 updated;
wenzelm
parents: 11706
diff changeset
   185
%
10159
a72ddfdbfca0 *** empty log message ***
nipkow
parents: 10149
diff changeset
   186
\begin{isamarkuptext}%
10867
bda1701848cd lcp's suggestions for CTL
paulson
parents: 10866
diff changeset
   187
Function \isa{path} has fulfilled its purpose now and can be forgotten.
bda1701848cd lcp's suggestions for CTL
paulson
parents: 10866
diff changeset
   188
It was merely defined to provide the witness in the proof of the
10171
59d6633835fa *** empty log message ***
nipkow
parents: 10159
diff changeset
   189
\isa{infinity{\isacharunderscore}lemma}. Aficionados of minimal proofs might like to know
10159
a72ddfdbfca0 *** empty log message ***
nipkow
parents: 10149
diff changeset
   190
that we could have given the witness without having to define a new function:
a72ddfdbfca0 *** empty log message ***
nipkow
parents: 10149
diff changeset
   191
the term
a72ddfdbfca0 *** empty log message ***
nipkow
parents: 10149
diff changeset
   192
\begin{isabelle}%
10895
79194f07d356 *** empty log message ***
nipkow
parents: 10878
diff changeset
   193
\ \ \ \ \ nat{\isacharunderscore}rec\ s\ {\isacharparenleft}{\isasymlambda}n\ t{\isachardot}\ SOME\ u{\isachardot}\ {\isacharparenleft}t{\isacharcomma}\ u{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ Q\ u{\isacharparenright}%
10159
a72ddfdbfca0 *** empty log message ***
nipkow
parents: 10149
diff changeset
   194
\end{isabelle}
10895
79194f07d356 *** empty log message ***
nipkow
parents: 10878
diff changeset
   195
is extensionally equal to \isa{path\ s\ Q},
10867
bda1701848cd lcp's suggestions for CTL
paulson
parents: 10866
diff changeset
   196
where \isa{nat{\isacharunderscore}rec} is the predefined primitive recursor on \isa{nat}.%
10159
a72ddfdbfca0 *** empty log message ***
nipkow
parents: 10149
diff changeset
   197
\end{isamarkuptext}%
11866
fbd097aec213 updated;
wenzelm
parents: 11706
diff changeset
   198
\isamarkuptrue%
fbd097aec213 updated;
wenzelm
parents: 11706
diff changeset
   199
\isamarkupfalse%
fbd097aec213 updated;
wenzelm
parents: 11706
diff changeset
   200
\isamarkupfalse%
fbd097aec213 updated;
wenzelm
parents: 11706
diff changeset
   201
\isamarkupfalse%
fbd097aec213 updated;
wenzelm
parents: 11706
diff changeset
   202
\isamarkupfalse%
fbd097aec213 updated;
wenzelm
parents: 11706
diff changeset
   203
\isamarkupfalse%
fbd097aec213 updated;
wenzelm
parents: 11706
diff changeset
   204
\isamarkupfalse%
fbd097aec213 updated;
wenzelm
parents: 11706
diff changeset
   205
\isamarkupfalse%
fbd097aec213 updated;
wenzelm
parents: 11706
diff changeset
   206
\isamarkupfalse%
fbd097aec213 updated;
wenzelm
parents: 11706
diff changeset
   207
\isamarkupfalse%
fbd097aec213 updated;
wenzelm
parents: 11706
diff changeset
   208
\isamarkupfalse%
fbd097aec213 updated;
wenzelm
parents: 11706
diff changeset
   209
\isamarkupfalse%
fbd097aec213 updated;
wenzelm
parents: 11706
diff changeset
   210
\isamarkupfalse%
fbd097aec213 updated;
wenzelm
parents: 11706
diff changeset
   211
\isamarkupfalse%
fbd097aec213 updated;
wenzelm
parents: 11706
diff changeset
   212
\isamarkupfalse%
fbd097aec213 updated;
wenzelm
parents: 11706
diff changeset
   213
\isamarkupfalse%
15904
a6fb4ddc05c7 introduced @{const ...} antiquotation
haftmann
parents: 15488
diff changeset
   214
\isanewline
11866
fbd097aec213 updated;
wenzelm
parents: 11706
diff changeset
   215
\isamarkupfalse%
10159
a72ddfdbfca0 *** empty log message ***
nipkow
parents: 10149
diff changeset
   216
%
a72ddfdbfca0 *** empty log message ***
nipkow
parents: 10149
diff changeset
   217
\begin{isamarkuptext}%
10187
0376cccd9118 *** empty log message ***
nipkow
parents: 10186
diff changeset
   218
At last we can prove the opposite direction of \isa{AF{\isacharunderscore}lemma{\isadigit{1}}}:%
10159
a72ddfdbfca0 *** empty log message ***
nipkow
parents: 10149
diff changeset
   219
\end{isamarkuptext}%
11866
fbd097aec213 updated;
wenzelm
parents: 11706
diff changeset
   220
\isamarkuptrue%
12328
7c4ec77a8715 *** empty log message ***
nipkow
parents: 11866
diff changeset
   221
\isacommand{theorem}\ AF{\isacharunderscore}lemma{\isadigit{2}}{\isacharcolon}\ {\isachardoublequote}{\isacharbraceleft}s{\isachardot}\ {\isasymforall}p\ {\isasymin}\ Paths\ s{\isachardot}\ {\isasymexists}i{\isachardot}\ p\ i\ {\isasymin}\ A{\isacharbraceright}\ {\isasymsubseteq}\ lfp{\isacharparenleft}af\ A{\isacharparenright}{\isachardoublequote}\isamarkupfalse%
11866
fbd097aec213 updated;
wenzelm
parents: 11706
diff changeset
   222
\isamarkuptrue%
fbd097aec213 updated;
wenzelm
parents: 11706
diff changeset
   223
\isamarkupfalse%
15488
7c638a46dcbb tidying of some subst/simplesubst proofs
paulson
parents: 15106
diff changeset
   224
\isamarkupfalse%
11866
fbd097aec213 updated;
wenzelm
parents: 11706
diff changeset
   225
\isamarkupfalse%
15488
7c638a46dcbb tidying of some subst/simplesubst proofs
paulson
parents: 15106
diff changeset
   226
\isamarkuptrue%
7c638a46dcbb tidying of some subst/simplesubst proofs
paulson
parents: 15106
diff changeset
   227
\isamarkupfalse%
11866
fbd097aec213 updated;
wenzelm
parents: 11706
diff changeset
   228
\isamarkuptrue%
fbd097aec213 updated;
wenzelm
parents: 11706
diff changeset
   229
\isamarkupfalse%
15488
7c638a46dcbb tidying of some subst/simplesubst proofs
paulson
parents: 15106
diff changeset
   230
\isamarkupfalse%
11866
fbd097aec213 updated;
wenzelm
parents: 11706
diff changeset
   231
%
10159
a72ddfdbfca0 *** empty log message ***
nipkow
parents: 10149
diff changeset
   232
\begin{isamarkuptext}%
10867
bda1701848cd lcp's suggestions for CTL
paulson
parents: 10866
diff changeset
   233
If you find these proofs too complicated, we recommend that you read
bda1701848cd lcp's suggestions for CTL
paulson
parents: 10866
diff changeset
   234
\S\ref{sec:CTL-revisited}, where we show how inductive definitions lead to
10217
e61e7e1eacaf *** empty log message ***
nipkow
parents: 10212
diff changeset
   235
simpler arguments.
e61e7e1eacaf *** empty log message ***
nipkow
parents: 10212
diff changeset
   236
e61e7e1eacaf *** empty log message ***
nipkow
parents: 10212
diff changeset
   237
The main theorem is proved as for PDL, except that we also derive the
e61e7e1eacaf *** empty log message ***
nipkow
parents: 10212
diff changeset
   238
necessary equality \isa{lfp{\isacharparenleft}af\ A{\isacharparenright}\ {\isacharequal}\ {\isachardot}{\isachardot}{\isachardot}} by combining
e61e7e1eacaf *** empty log message ***
nipkow
parents: 10212
diff changeset
   239
\isa{AF{\isacharunderscore}lemma{\isadigit{1}}} and \isa{AF{\isacharunderscore}lemma{\isadigit{2}}} on the spot:%
10159
a72ddfdbfca0 *** empty log message ***
nipkow
parents: 10149
diff changeset
   240
\end{isamarkuptext}%
11866
fbd097aec213 updated;
wenzelm
parents: 11706
diff changeset
   241
\isamarkuptrue%
10123
9469c039ff57 *** empty log message ***
nipkow
parents:
diff changeset
   242
\isacommand{theorem}\ {\isachardoublequote}mc\ f\ {\isacharequal}\ {\isacharbraceleft}s{\isachardot}\ s\ {\isasymTurnstile}\ f{\isacharbraceright}{\isachardoublequote}\isanewline
11866
fbd097aec213 updated;
wenzelm
parents: 11706
diff changeset
   243
\isamarkupfalse%
15488
7c638a46dcbb tidying of some subst/simplesubst proofs
paulson
parents: 15106
diff changeset
   244
\isamarkupfalse%
11866
fbd097aec213 updated;
wenzelm
parents: 11706
diff changeset
   245
\isamarkupfalse%
fbd097aec213 updated;
wenzelm
parents: 11706
diff changeset
   246
\isamarkupfalse%
fbd097aec213 updated;
wenzelm
parents: 11706
diff changeset
   247
%
10159
a72ddfdbfca0 *** empty log message ***
nipkow
parents: 10149
diff changeset
   248
\begin{isamarkuptext}%
10867
bda1701848cd lcp's suggestions for CTL
paulson
parents: 10866
diff changeset
   249
The language defined above is not quite CTL\@. The latter also includes an
10983
59961d32b1ae *** empty log message ***
nipkow
parents: 10971
diff changeset
   250
until-operator \isa{EU\ f\ g} with semantics ``there \emph{E}xists a path
11494
23a118849801 revisions and indexing
paulson
parents: 11231
diff changeset
   251
where \isa{f} is true \emph{U}ntil \isa{g} becomes true''.  We need
23a118849801 revisions and indexing
paulson
parents: 11231
diff changeset
   252
an auxiliary function:%
10281
9554ce1c2e54 *** empty log message ***
nipkow
parents: 10242
diff changeset
   253
\end{isamarkuptext}%
11866
fbd097aec213 updated;
wenzelm
parents: 11706
diff changeset
   254
\isamarkuptrue%
10281
9554ce1c2e54 *** empty log message ***
nipkow
parents: 10242
diff changeset
   255
\isacommand{consts}\ until{\isacharcolon}{\isacharcolon}\ {\isachardoublequote}state\ set\ {\isasymRightarrow}\ state\ set\ {\isasymRightarrow}\ state\ {\isasymRightarrow}\ state\ list\ {\isasymRightarrow}\ bool{\isachardoublequote}\isanewline
11866
fbd097aec213 updated;
wenzelm
parents: 11706
diff changeset
   256
\isamarkupfalse%
10281
9554ce1c2e54 *** empty log message ***
nipkow
parents: 10242
diff changeset
   257
\isacommand{primrec}\isanewline
9554ce1c2e54 *** empty log message ***
nipkow
parents: 10242
diff changeset
   258
{\isachardoublequote}until\ A\ B\ s\ {\isacharbrackleft}{\isacharbrackright}\ \ \ \ {\isacharequal}\ {\isacharparenleft}s\ {\isasymin}\ B{\isacharparenright}{\isachardoublequote}\isanewline
11866
fbd097aec213 updated;
wenzelm
parents: 11706
diff changeset
   259
{\isachardoublequote}until\ A\ B\ s\ {\isacharparenleft}t{\isacharhash}p{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}s\ {\isasymin}\ A\ {\isasymand}\ {\isacharparenleft}s{\isacharcomma}t{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ until\ A\ B\ t\ p{\isacharparenright}{\isachardoublequote}\isamarkupfalse%
fbd097aec213 updated;
wenzelm
parents: 11706
diff changeset
   260
\isamarkupfalse%
fbd097aec213 updated;
wenzelm
parents: 11706
diff changeset
   261
%
10281
9554ce1c2e54 *** empty log message ***
nipkow
parents: 10242
diff changeset
   262
\begin{isamarkuptext}%
9554ce1c2e54 *** empty log message ***
nipkow
parents: 10242
diff changeset
   263
\noindent
11494
23a118849801 revisions and indexing
paulson
parents: 11231
diff changeset
   264
Expressing the semantics of \isa{EU} is now straightforward:
10171
59d6633835fa *** empty log message ***
nipkow
parents: 10159
diff changeset
   265
\begin{isabelle}%
10983
59961d32b1ae *** empty log message ***
nipkow
parents: 10971
diff changeset
   266
\ \ \ \ \ s\ {\isasymTurnstile}\ EU\ f\ g\ {\isacharequal}\ {\isacharparenleft}{\isasymexists}p{\isachardot}\ until\ {\isacharbraceleft}t{\isachardot}\ t\ {\isasymTurnstile}\ f{\isacharbraceright}\ {\isacharbraceleft}t{\isachardot}\ t\ {\isasymTurnstile}\ g{\isacharbraceright}\ s\ p{\isacharparenright}%
10171
59d6633835fa *** empty log message ***
nipkow
parents: 10159
diff changeset
   267
\end{isabelle}
10281
9554ce1c2e54 *** empty log message ***
nipkow
parents: 10242
diff changeset
   268
Note that \isa{EU} is not definable in terms of the other operators!
9554ce1c2e54 *** empty log message ***
nipkow
parents: 10242
diff changeset
   269
9554ce1c2e54 *** empty log message ***
nipkow
parents: 10242
diff changeset
   270
Model checking \isa{EU} is again a least fixed point construction:
10171
59d6633835fa *** empty log message ***
nipkow
parents: 10159
diff changeset
   271
\begin{isabelle}%
10839
1f93f5a27de6 *** empty log message ***
nipkow
parents: 10801
diff changeset
   272
\ \ \ \ \ mc{\isacharparenleft}EU\ f\ g{\isacharparenright}\ {\isacharequal}\ lfp{\isacharparenleft}{\isasymlambda}T{\isachardot}\ mc\ g\ {\isasymunion}\ mc\ f\ {\isasyminter}\ {\isacharparenleft}M{\isasyminverse}\ {\isacharbackquote}{\isacharbackquote}\ T{\isacharparenright}{\isacharparenright}%
10171
59d6633835fa *** empty log message ***
nipkow
parents: 10159
diff changeset
   273
\end{isabelle}
10281
9554ce1c2e54 *** empty log message ***
nipkow
parents: 10242
diff changeset
   274
9554ce1c2e54 *** empty log message ***
nipkow
parents: 10242
diff changeset
   275
\begin{exercise}
9554ce1c2e54 *** empty log message ***
nipkow
parents: 10242
diff changeset
   276
Extend the datatype of formulae by the above until operator
9554ce1c2e54 *** empty log message ***
nipkow
parents: 10242
diff changeset
   277
and prove the equivalence between semantics and model checking, i.e.\ that
10186
499637e8f2c6 *** empty log message ***
nipkow
parents: 10178
diff changeset
   278
\begin{isabelle}%
499637e8f2c6 *** empty log message ***
nipkow
parents: 10178
diff changeset
   279
\ \ \ \ \ mc\ {\isacharparenleft}EU\ f\ g{\isacharparenright}\ {\isacharequal}\ {\isacharbraceleft}s{\isachardot}\ s\ {\isasymTurnstile}\ EU\ f\ g{\isacharbraceright}%
499637e8f2c6 *** empty log message ***
nipkow
parents: 10178
diff changeset
   280
\end{isabelle}
499637e8f2c6 *** empty log message ***
nipkow
parents: 10178
diff changeset
   281
%For readability you may want to annotate {term EU} with its customary syntax
499637e8f2c6 *** empty log message ***
nipkow
parents: 10178
diff changeset
   282
%{text[display]"| EU formula formula    E[_ U _]"}
499637e8f2c6 *** empty log message ***
nipkow
parents: 10178
diff changeset
   283
%which enables you to read and write {text"E[f U g]"} instead of {term"EU f g"}.
499637e8f2c6 *** empty log message ***
nipkow
parents: 10178
diff changeset
   284
\end{exercise}
10867
bda1701848cd lcp's suggestions for CTL
paulson
parents: 10866
diff changeset
   285
For more CTL exercises see, for example, Huth and Ryan \cite{Huth-Ryan-book}.%
10281
9554ce1c2e54 *** empty log message ***
nipkow
parents: 10242
diff changeset
   286
\end{isamarkuptext}%
11866
fbd097aec213 updated;
wenzelm
parents: 11706
diff changeset
   287
\isamarkuptrue%
fbd097aec213 updated;
wenzelm
parents: 11706
diff changeset
   288
\isamarkupfalse%
fbd097aec213 updated;
wenzelm
parents: 11706
diff changeset
   289
\isamarkupfalse%
fbd097aec213 updated;
wenzelm
parents: 11706
diff changeset
   290
\isamarkupfalse%
fbd097aec213 updated;
wenzelm
parents: 11706
diff changeset
   291
\isamarkupfalse%
fbd097aec213 updated;
wenzelm
parents: 11706
diff changeset
   292
\isamarkupfalse%
fbd097aec213 updated;
wenzelm
parents: 11706
diff changeset
   293
\isamarkupfalse%
fbd097aec213 updated;
wenzelm
parents: 11706
diff changeset
   294
\isamarkupfalse%
fbd097aec213 updated;
wenzelm
parents: 11706
diff changeset
   295
\isamarkupfalse%
15904
a6fb4ddc05c7 introduced @{const ...} antiquotation
haftmann
parents: 15488
diff changeset
   296
\isanewline
a6fb4ddc05c7 introduced @{const ...} antiquotation
haftmann
parents: 15488
diff changeset
   297
\isamarkupfalse%
a6fb4ddc05c7 introduced @{const ...} antiquotation
haftmann
parents: 15488
diff changeset
   298
\isamarkupfalse%
a6fb4ddc05c7 introduced @{const ...} antiquotation
haftmann
parents: 15488
diff changeset
   299
\isamarkupfalse%
a6fb4ddc05c7 introduced @{const ...} antiquotation
haftmann
parents: 15488
diff changeset
   300
\isamarkupfalse%
a6fb4ddc05c7 introduced @{const ...} antiquotation
haftmann
parents: 15488
diff changeset
   301
\isanewline
11866
fbd097aec213 updated;
wenzelm
parents: 11706
diff changeset
   302
\isamarkupfalse%
fbd097aec213 updated;
wenzelm
parents: 11706
diff changeset
   303
\isamarkupfalse%
fbd097aec213 updated;
wenzelm
parents: 11706
diff changeset
   304
\isamarkupfalse%
fbd097aec213 updated;
wenzelm
parents: 11706
diff changeset
   305
\isamarkupfalse%
fbd097aec213 updated;
wenzelm
parents: 11706
diff changeset
   306
\isamarkupfalse%
fbd097aec213 updated;
wenzelm
parents: 11706
diff changeset
   307
\isamarkupfalse%
fbd097aec213 updated;
wenzelm
parents: 11706
diff changeset
   308
\isamarkupfalse%
fbd097aec213 updated;
wenzelm
parents: 11706
diff changeset
   309
\isamarkupfalse%
fbd097aec213 updated;
wenzelm
parents: 11706
diff changeset
   310
\isamarkupfalse%
fbd097aec213 updated;
wenzelm
parents: 11706
diff changeset
   311
\isamarkupfalse%
fbd097aec213 updated;
wenzelm
parents: 11706
diff changeset
   312
\isamarkupfalse%
fbd097aec213 updated;
wenzelm
parents: 11706
diff changeset
   313
\isamarkupfalse%
15904
a6fb4ddc05c7 introduced @{const ...} antiquotation
haftmann
parents: 15488
diff changeset
   314
\isanewline
a6fb4ddc05c7 introduced @{const ...} antiquotation
haftmann
parents: 15488
diff changeset
   315
\isanewline
11866
fbd097aec213 updated;
wenzelm
parents: 11706
diff changeset
   316
\isamarkupfalse%
10281
9554ce1c2e54 *** empty log message ***
nipkow
parents: 10242
diff changeset
   317
%
9554ce1c2e54 *** empty log message ***
nipkow
parents: 10242
diff changeset
   318
\begin{isamarkuptext}%
12334
60bf75e157e4 *** empty log message ***
nipkow
parents: 12332
diff changeset
   319
Let us close this section with a few words about the executability of
60bf75e157e4 *** empty log message ***
nipkow
parents: 12332
diff changeset
   320
our model checkers.  It is clear that if all sets are finite, they can be
60bf75e157e4 *** empty log message ***
nipkow
parents: 12332
diff changeset
   321
represented as lists and the usual set operations are easily
60bf75e157e4 *** empty log message ***
nipkow
parents: 12332
diff changeset
   322
implemented. Only \isa{lfp} requires a little thought.  Fortunately, theory
12473
f41e477576b9 *** empty log message ***
nipkow
parents: 12334
diff changeset
   323
\isa{While{\isacharunderscore}Combinator} in the Library~\cite{HOL-Library} provides a
12334
60bf75e157e4 *** empty log message ***
nipkow
parents: 12332
diff changeset
   324
theorem stating that in the case of finite sets and a monotone
60bf75e157e4 *** empty log message ***
nipkow
parents: 12332
diff changeset
   325
function~\isa{F}, the value of \mbox{\isa{lfp\ F}} can be computed by
60bf75e157e4 *** empty log message ***
nipkow
parents: 12332
diff changeset
   326
iterated application of \isa{F} to~\isa{{\isacharbraceleft}{\isacharbraceright}} until a fixed point is
60bf75e157e4 *** empty log message ***
nipkow
parents: 12332
diff changeset
   327
reached. It is actually possible to generate executable functional programs
10159
a72ddfdbfca0 *** empty log message ***
nipkow
parents: 10149
diff changeset
   328
from HOL definitions, but that is beyond the scope of the tutorial.%
11494
23a118849801 revisions and indexing
paulson
parents: 11231
diff changeset
   329
\index{CTL|)}%
10159
a72ddfdbfca0 *** empty log message ***
nipkow
parents: 10149
diff changeset
   330
\end{isamarkuptext}%
11866
fbd097aec213 updated;
wenzelm
parents: 11706
diff changeset
   331
\isamarkuptrue%
fbd097aec213 updated;
wenzelm
parents: 11706
diff changeset
   332
\isamarkupfalse%
10123
9469c039ff57 *** empty log message ***
nipkow
parents:
diff changeset
   333
\end{isabellebody}%
9469c039ff57 *** empty log message ***
nipkow
parents:
diff changeset
   334
%%% Local Variables:
9469c039ff57 *** empty log message ***
nipkow
parents:
diff changeset
   335
%%% mode: latex
9469c039ff57 *** empty log message ***
nipkow
parents:
diff changeset
   336
%%% TeX-master: "root"
9469c039ff57 *** empty log message ***
nipkow
parents:
diff changeset
   337
%%% End: