1 % |
|
2 \begin{isabellebody}% |
|
3 \def\isabellecontext{PDL}% |
|
4 % |
|
5 \isadelimtheory |
|
6 % |
|
7 \endisadelimtheory |
|
8 % |
|
9 \isatagtheory |
|
10 % |
|
11 \endisatagtheory |
|
12 {\isafoldtheory}% |
|
13 % |
|
14 \isadelimtheory |
|
15 % |
|
16 \endisadelimtheory |
|
17 % |
|
18 \isamarkupsubsection{Propositional Dynamic Logic --- PDL% |
|
19 } |
|
20 \isamarkuptrue% |
|
21 % |
|
22 \begin{isamarkuptext}% |
|
23 \index{PDL|(} |
|
24 The formulae of PDL are built up from atomic propositions via |
|
25 negation and conjunction and the two temporal |
|
26 connectives \isa{AX} and \isa{EF}\@. Since formulae are essentially |
|
27 syntax trees, they are naturally modelled as a datatype:% |
|
28 \footnote{The customary definition of PDL |
|
29 \cite{HarelKT-DL} looks quite different from ours, but the two are easily |
|
30 shown to be equivalent.}% |
|
31 \end{isamarkuptext}% |
|
32 \isamarkuptrue% |
|
33 \isacommand{datatype}\isamarkupfalse% |
|
34 \ formula\ {\isaliteral{3D}{\isacharequal}}\ Atom\ {\isaliteral{22}{\isachardoublequoteopen}}atom{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
|
35 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{7C}{\isacharbar}}\ Neg\ formula\isanewline |
|
36 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{7C}{\isacharbar}}\ And\ formula\ formula\isanewline |
|
37 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{7C}{\isacharbar}}\ AX\ formula\isanewline |
|
38 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{7C}{\isacharbar}}\ EF\ formula% |
|
39 \begin{isamarkuptext}% |
|
40 \noindent |
|
41 This resembles the boolean expression case study in |
|
42 \S\ref{sec:boolex}. |
|
43 A validity relation between states and formulae specifies the semantics. |
|
44 The syntax annotation allows us to write \isa{s\ {\isaliteral{5C3C5475726E7374696C653E}{\isasymTurnstile}}\ f} instead of |
|
45 \hbox{\isa{valid\ s\ f}}. The definition is by recursion over the syntax:% |
|
46 \end{isamarkuptext}% |
|
47 \isamarkuptrue% |
|
48 \isacommand{primrec}\isamarkupfalse% |
|
49 \ valid\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}state\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ formula\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool{\isaliteral{22}{\isachardoublequoteclose}}\ \ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5F}{\isacharunderscore}}\ {\isaliteral{5C3C5475726E7374696C653E}{\isasymTurnstile}}\ {\isaliteral{5F}{\isacharunderscore}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isadigit{8}}{\isadigit{0}}{\isaliteral{2C}{\isacharcomma}}{\isadigit{8}}{\isadigit{0}}{\isaliteral{5D}{\isacharbrackright}}\ {\isadigit{8}}{\isadigit{0}}{\isaliteral{29}{\isacharparenright}}\isanewline |
|
50 \isakeyword{where}\isanewline |
|
51 {\isaliteral{22}{\isachardoublequoteopen}}s\ {\isaliteral{5C3C5475726E7374696C653E}{\isasymTurnstile}}\ Atom\ a\ \ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}a\ {\isaliteral{5C3C696E3E}{\isasymin}}\ L\ s{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\isanewline |
|
52 {\isaliteral{22}{\isachardoublequoteopen}}s\ {\isaliteral{5C3C5475726E7374696C653E}{\isasymTurnstile}}\ Neg\ f\ \ \ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6E6F743E}{\isasymnot}}{\isaliteral{28}{\isacharparenleft}}s\ {\isaliteral{5C3C5475726E7374696C653E}{\isasymTurnstile}}\ f{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\isanewline |
|
53 {\isaliteral{22}{\isachardoublequoteopen}}s\ {\isaliteral{5C3C5475726E7374696C653E}{\isasymTurnstile}}\ And\ f\ g\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}s\ {\isaliteral{5C3C5475726E7374696C653E}{\isasymTurnstile}}\ f\ {\isaliteral{5C3C616E643E}{\isasymand}}\ s\ {\isaliteral{5C3C5475726E7374696C653E}{\isasymTurnstile}}\ g{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\isanewline |
|
54 {\isaliteral{22}{\isachardoublequoteopen}}s\ {\isaliteral{5C3C5475726E7374696C653E}{\isasymTurnstile}}\ AX\ f\ \ \ \ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}t{\isaliteral{2E}{\isachardot}}\ {\isaliteral{28}{\isacharparenleft}}s{\isaliteral{2C}{\isacharcomma}}t{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ M\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ t\ {\isaliteral{5C3C5475726E7374696C653E}{\isasymTurnstile}}\ f{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\isanewline |
|
55 {\isaliteral{22}{\isachardoublequoteopen}}s\ {\isaliteral{5C3C5475726E7374696C653E}{\isasymTurnstile}}\ EF\ f\ \ \ \ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6578697374733E}{\isasymexists}}t{\isaliteral{2E}{\isachardot}}\ {\isaliteral{28}{\isacharparenleft}}s{\isaliteral{2C}{\isacharcomma}}t{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ M\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}\ {\isaliteral{5C3C616E643E}{\isasymand}}\ t\ {\isaliteral{5C3C5475726E7374696C653E}{\isasymTurnstile}}\ f{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}% |
|
56 \begin{isamarkuptext}% |
|
57 \noindent |
|
58 The first three equations should be self-explanatory. The temporal formula |
|
59 \isa{AX\ f} means that \isa{f} is true in \emph{A}ll ne\emph{X}t states whereas |
|
60 \isa{EF\ f} means that there \emph{E}xists some \emph{F}uture state in which \isa{f} is |
|
61 true. The future is expressed via \isa{\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}}, the reflexive transitive |
|
62 closure. Because of reflexivity, the future includes the present. |
|
63 |
|
64 Now we come to the model checker itself. It maps a formula into the |
|
65 set of states where the formula is true. It too is defined by |
|
66 recursion over the syntax:% |
|
67 \end{isamarkuptext}% |
|
68 \isamarkuptrue% |
|
69 \isacommand{primrec}\isamarkupfalse% |
|
70 \ mc\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}formula\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ state\ set{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{where}\isanewline |
|
71 {\isaliteral{22}{\isachardoublequoteopen}}mc{\isaliteral{28}{\isacharparenleft}}Atom\ a{\isaliteral{29}{\isacharparenright}}\ \ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{7B}{\isacharbraceleft}}s{\isaliteral{2E}{\isachardot}}\ a\ {\isaliteral{5C3C696E3E}{\isasymin}}\ L\ s{\isaliteral{7D}{\isacharbraceright}}{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\isanewline |
|
72 {\isaliteral{22}{\isachardoublequoteopen}}mc{\isaliteral{28}{\isacharparenleft}}Neg\ f{\isaliteral{29}{\isacharparenright}}\ \ \ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{2D}{\isacharminus}}mc\ f{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\isanewline |
|
73 {\isaliteral{22}{\isachardoublequoteopen}}mc{\isaliteral{28}{\isacharparenleft}}And\ f\ g{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ mc\ f\ {\isaliteral{5C3C696E7465723E}{\isasyminter}}\ mc\ g{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\isanewline |
|
74 {\isaliteral{22}{\isachardoublequoteopen}}mc{\isaliteral{28}{\isacharparenleft}}AX\ f{\isaliteral{29}{\isacharparenright}}\ \ \ \ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{7B}{\isacharbraceleft}}s{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}t{\isaliteral{2E}{\isachardot}}\ {\isaliteral{28}{\isacharparenleft}}s{\isaliteral{2C}{\isacharcomma}}t{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ M\ \ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ t\ {\isaliteral{5C3C696E3E}{\isasymin}}\ mc\ f{\isaliteral{7D}{\isacharbraceright}}{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\isanewline |
|
75 {\isaliteral{22}{\isachardoublequoteopen}}mc{\isaliteral{28}{\isacharparenleft}}EF\ f{\isaliteral{29}{\isacharparenright}}\ \ \ \ {\isaliteral{3D}{\isacharequal}}\ lfp{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}T{\isaliteral{2E}{\isachardot}}\ mc\ f\ {\isaliteral{5C3C756E696F6E3E}{\isasymunion}}\ {\isaliteral{28}{\isacharparenleft}}M{\isaliteral{5C3C696E76657273653E}{\isasyminverse}}\ {\isaliteral{60}{\isacharbackquote}}{\isaliteral{60}{\isacharbackquote}}\ T{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}% |
|
76 \begin{isamarkuptext}% |
|
77 \noindent |
|
78 Only the equation for \isa{EF} deserves some comments. Remember that the |
|
79 postfix \isa{{\isaliteral{5C3C696E76657273653E}{\isasyminverse}}} and the infix \isa{{\isaliteral{60}{\isacharbackquote}}{\isaliteral{60}{\isacharbackquote}}} are predefined and denote the |
|
80 converse of a relation and the image of a set under a relation. Thus |
|
81 \isa{M{\isaliteral{5C3C696E76657273653E}{\isasyminverse}}\ {\isaliteral{60}{\isacharbackquote}}{\isaliteral{60}{\isacharbackquote}}\ T} is the set of all predecessors of \isa{T} and the least |
|
82 fixed point (\isa{lfp}) of \isa{{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}T{\isaliteral{2E}{\isachardot}}\ mc\ f\ {\isaliteral{5C3C756E696F6E3E}{\isasymunion}}\ M{\isaliteral{5C3C696E76657273653E}{\isasyminverse}}\ {\isaliteral{60}{\isacharbackquote}}{\isaliteral{60}{\isacharbackquote}}\ T} is the least set |
|
83 \isa{T} containing \isa{mc\ f} and all predecessors of \isa{T}. If you |
|
84 find it hard to see that \isa{mc\ {\isaliteral{28}{\isacharparenleft}}EF\ f{\isaliteral{29}{\isacharparenright}}} contains exactly those states from |
|
85 which there is a path to a state where \isa{f} is true, do not worry --- this |
|
86 will be proved in a moment. |
|
87 |
|
88 First we prove monotonicity of the function inside \isa{lfp} |
|
89 in order to make sure it really has a least fixed point.% |
|
90 \end{isamarkuptext}% |
|
91 \isamarkuptrue% |
|
92 \isacommand{lemma}\isamarkupfalse% |
|
93 \ mono{\isaliteral{5F}{\isacharunderscore}}ef{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}mono{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}T{\isaliteral{2E}{\isachardot}}\ A\ {\isaliteral{5C3C756E696F6E3E}{\isasymunion}}\ {\isaliteral{28}{\isacharparenleft}}M{\isaliteral{5C3C696E76657273653E}{\isasyminverse}}\ {\isaliteral{60}{\isacharbackquote}}{\isaliteral{60}{\isacharbackquote}}\ T{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
|
94 % |
|
95 \isadelimproof |
|
96 % |
|
97 \endisadelimproof |
|
98 % |
|
99 \isatagproof |
|
100 \isacommand{apply}\isamarkupfalse% |
|
101 {\isaliteral{28}{\isacharparenleft}}rule\ monoI{\isaliteral{29}{\isacharparenright}}\isanewline |
|
102 \isacommand{apply}\isamarkupfalse% |
|
103 \ blast\isanewline |
|
104 \isacommand{done}\isamarkupfalse% |
|
105 % |
|
106 \endisatagproof |
|
107 {\isafoldproof}% |
|
108 % |
|
109 \isadelimproof |
|
110 % |
|
111 \endisadelimproof |
|
112 % |
|
113 \begin{isamarkuptext}% |
|
114 \noindent |
|
115 Now we can relate model checking and semantics. For the \isa{EF} case we need |
|
116 a separate lemma:% |
|
117 \end{isamarkuptext}% |
|
118 \isamarkuptrue% |
|
119 \isacommand{lemma}\isamarkupfalse% |
|
120 \ EF{\isaliteral{5F}{\isacharunderscore}}lemma{\isaliteral{3A}{\isacharcolon}}\isanewline |
|
121 \ \ {\isaliteral{22}{\isachardoublequoteopen}}lfp{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}T{\isaliteral{2E}{\isachardot}}\ A\ {\isaliteral{5C3C756E696F6E3E}{\isasymunion}}\ {\isaliteral{28}{\isacharparenleft}}M{\isaliteral{5C3C696E76657273653E}{\isasyminverse}}\ {\isaliteral{60}{\isacharbackquote}}{\isaliteral{60}{\isacharbackquote}}\ T{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{7B}{\isacharbraceleft}}s{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C6578697374733E}{\isasymexists}}t{\isaliteral{2E}{\isachardot}}\ {\isaliteral{28}{\isacharparenleft}}s{\isaliteral{2C}{\isacharcomma}}t{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ M\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}\ {\isaliteral{5C3C616E643E}{\isasymand}}\ t\ {\isaliteral{5C3C696E3E}{\isasymin}}\ A{\isaliteral{7D}{\isacharbraceright}}{\isaliteral{22}{\isachardoublequoteclose}}% |
|
122 \isadelimproof |
|
123 % |
|
124 \endisadelimproof |
|
125 % |
|
126 \isatagproof |
|
127 % |
|
128 \begin{isamarkuptxt}% |
|
129 \noindent |
|
130 The equality is proved in the canonical fashion by proving that each set |
|
131 includes the other; the inclusion is shown pointwise:% |
|
132 \end{isamarkuptxt}% |
|
133 \isamarkuptrue% |
|
134 \isacommand{apply}\isamarkupfalse% |
|
135 {\isaliteral{28}{\isacharparenleft}}rule\ equalityI{\isaliteral{29}{\isacharparenright}}\isanewline |
|
136 \ \isacommand{apply}\isamarkupfalse% |
|
137 {\isaliteral{28}{\isacharparenleft}}rule\ subsetI{\isaliteral{29}{\isacharparenright}}\isanewline |
|
138 \ \isacommand{apply}\isamarkupfalse% |
|
139 {\isaliteral{28}{\isacharparenleft}}simp{\isaliteral{29}{\isacharparenright}}% |
|
140 \begin{isamarkuptxt}% |
|
141 \noindent |
|
142 Simplification leaves us with the following first subgoal |
|
143 \begin{isabelle}% |
|
144 \ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C416E643E}{\isasymAnd}}s{\isaliteral{2E}{\isachardot}}\ s\ {\isaliteral{5C3C696E3E}{\isasymin}}\ lfp\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}T{\isaliteral{2E}{\isachardot}}\ A\ {\isaliteral{5C3C756E696F6E3E}{\isasymunion}}\ M{\isaliteral{5C3C696E76657273653E}{\isasyminverse}}\ {\isaliteral{60}{\isacharbackquote}}{\isaliteral{60}{\isacharbackquote}}\ T{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{5C3C6578697374733E}{\isasymexists}}t{\isaliteral{2E}{\isachardot}}\ {\isaliteral{28}{\isacharparenleft}}s{\isaliteral{2C}{\isacharcomma}}\ t{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ M\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}\ {\isaliteral{5C3C616E643E}{\isasymand}}\ t\ {\isaliteral{5C3C696E3E}{\isasymin}}\ A% |
|
145 \end{isabelle} |
|
146 which is proved by \isa{lfp}-induction:% |
|
147 \end{isamarkuptxt}% |
|
148 \isamarkuptrue% |
|
149 \ \isacommand{apply}\isamarkupfalse% |
|
150 {\isaliteral{28}{\isacharparenleft}}erule\ lfp{\isaliteral{5F}{\isacharunderscore}}induct{\isaliteral{5F}{\isacharunderscore}}set{\isaliteral{29}{\isacharparenright}}\isanewline |
|
151 \ \ \isacommand{apply}\isamarkupfalse% |
|
152 {\isaliteral{28}{\isacharparenleft}}rule\ mono{\isaliteral{5F}{\isacharunderscore}}ef{\isaliteral{29}{\isacharparenright}}\isanewline |
|
153 \ \isacommand{apply}\isamarkupfalse% |
|
154 {\isaliteral{28}{\isacharparenleft}}simp{\isaliteral{29}{\isacharparenright}}% |
|
155 \begin{isamarkuptxt}% |
|
156 \noindent |
|
157 Having disposed of the monotonicity subgoal, |
|
158 simplification leaves us with the following goal: |
|
159 \begin{isabelle} |
|
160 \ {\isadigit{1}}{\isachardot}\ {\isasymAnd}x{\isachardot}\ x\ {\isasymin}\ A\ {\isasymor}\isanewline |
|
161 \ \ \ \ \ \ \ \ \ x\ {\isasymin}\ M{\isasyminverse}\ {\isacharbackquote}{\isacharbackquote}\ {\isacharparenleft}lfp\ {\isacharparenleft}\dots{\isacharparenright}\ {\isasyminter}\ {\isacharbraceleft}x{\isachardot}\ {\isasymexists}t{\isachardot}\ {\isacharparenleft}x{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\isactrlsup {\isacharasterisk}\ {\isasymand}\ t\ {\isasymin}\ A{\isacharbraceright}{\isacharparenright}\isanewline |
|
162 \ \ \ \ \ \ \ \ {\isasymLongrightarrow}\ {\isasymexists}t{\isachardot}\ {\isacharparenleft}x{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\isactrlsup {\isacharasterisk}\ {\isasymand}\ t\ {\isasymin}\ A |
|
163 \end{isabelle} |
|
164 It is proved by \isa{blast}, using the transitivity of |
|
165 \isa{M\isactrlsup {\isacharasterisk}}.% |
|
166 \end{isamarkuptxt}% |
|
167 \isamarkuptrue% |
|
168 \ \isacommand{apply}\isamarkupfalse% |
|
169 {\isaliteral{28}{\isacharparenleft}}blast\ intro{\isaliteral{3A}{\isacharcolon}}\ rtrancl{\isaliteral{5F}{\isacharunderscore}}trans{\isaliteral{29}{\isacharparenright}}% |
|
170 \begin{isamarkuptxt}% |
|
171 We now return to the second set inclusion subgoal, which is again proved |
|
172 pointwise:% |
|
173 \end{isamarkuptxt}% |
|
174 \isamarkuptrue% |
|
175 \isacommand{apply}\isamarkupfalse% |
|
176 {\isaliteral{28}{\isacharparenleft}}rule\ subsetI{\isaliteral{29}{\isacharparenright}}\isanewline |
|
177 \isacommand{apply}\isamarkupfalse% |
|
178 {\isaliteral{28}{\isacharparenleft}}simp{\isaliteral{2C}{\isacharcomma}}\ clarify{\isaliteral{29}{\isacharparenright}}% |
|
179 \begin{isamarkuptxt}% |
|
180 \noindent |
|
181 After simplification and clarification we are left with |
|
182 \begin{isabelle}% |
|
183 \ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C416E643E}{\isasymAnd}}x\ t{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}{\isaliteral{28}{\isacharparenleft}}x{\isaliteral{2C}{\isacharcomma}}\ t{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ M\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{3B}{\isacharsemicolon}}\ t\ {\isaliteral{5C3C696E3E}{\isasymin}}\ A{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ lfp\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}T{\isaliteral{2E}{\isachardot}}\ A\ {\isaliteral{5C3C756E696F6E3E}{\isasymunion}}\ M{\isaliteral{5C3C696E76657273653E}{\isasyminverse}}\ {\isaliteral{60}{\isacharbackquote}}{\isaliteral{60}{\isacharbackquote}}\ T{\isaliteral{29}{\isacharparenright}}% |
|
184 \end{isabelle} |
|
185 This goal is proved by induction on \isa{{\isaliteral{28}{\isacharparenleft}}s{\isaliteral{2C}{\isacharcomma}}\ t{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ M\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}}. But since the model |
|
186 checker works backwards (from \isa{t} to \isa{s}), we cannot use the |
|
187 induction theorem \isa{rtrancl{\isaliteral{5F}{\isacharunderscore}}induct}: it works in the |
|
188 forward direction. Fortunately the converse induction theorem |
|
189 \isa{converse{\isaliteral{5F}{\isacharunderscore}}rtrancl{\isaliteral{5F}{\isacharunderscore}}induct} already exists: |
|
190 \begin{isabelle}% |
|
191 \ \ \ \ \ {\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}{\isaliteral{28}{\isacharparenleft}}a{\isaliteral{2C}{\isacharcomma}}\ b{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ r\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{3B}{\isacharsemicolon}}\ P\ b{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
|
192 \isaindent{\ \ \ \ \ \ }{\isaliteral{5C3C416E643E}{\isasymAnd}}y\ z{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}{\isaliteral{28}{\isacharparenleft}}y{\isaliteral{2C}{\isacharcomma}}\ z{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ r{\isaliteral{3B}{\isacharsemicolon}}\ {\isaliteral{28}{\isacharparenleft}}z{\isaliteral{2C}{\isacharcomma}}\ b{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ r\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{3B}{\isacharsemicolon}}\ P\ z{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P\ y{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\isanewline |
|
193 \isaindent{\ \ \ \ \ }{\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P\ a% |
|
194 \end{isabelle} |
|
195 It says that if \isa{{\isaliteral{28}{\isacharparenleft}}a{\isaliteral{2C}{\isacharcomma}}\ b{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ r\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}} and we know \isa{P\ b} then we can infer |
|
196 \isa{P\ a} provided each step backwards from a predecessor \isa{z} of |
|
197 \isa{b} preserves \isa{P}.% |
|
198 \end{isamarkuptxt}% |
|
199 \isamarkuptrue% |
|
200 \isacommand{apply}\isamarkupfalse% |
|
201 {\isaliteral{28}{\isacharparenleft}}erule\ converse{\isaliteral{5F}{\isacharunderscore}}rtrancl{\isaliteral{5F}{\isacharunderscore}}induct{\isaliteral{29}{\isacharparenright}}% |
|
202 \begin{isamarkuptxt}% |
|
203 \noindent |
|
204 The base case |
|
205 \begin{isabelle}% |
|
206 \ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C416E643E}{\isasymAnd}}x\ t{\isaliteral{2E}{\isachardot}}\ t\ {\isaliteral{5C3C696E3E}{\isasymin}}\ A\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ t\ {\isaliteral{5C3C696E3E}{\isasymin}}\ lfp\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}T{\isaliteral{2E}{\isachardot}}\ A\ {\isaliteral{5C3C756E696F6E3E}{\isasymunion}}\ M{\isaliteral{5C3C696E76657273653E}{\isasyminverse}}\ {\isaliteral{60}{\isacharbackquote}}{\isaliteral{60}{\isacharbackquote}}\ T{\isaliteral{29}{\isacharparenright}}% |
|
207 \end{isabelle} |
|
208 is solved by unrolling \isa{lfp} once% |
|
209 \end{isamarkuptxt}% |
|
210 \isamarkuptrue% |
|
211 \ \isacommand{apply}\isamarkupfalse% |
|
212 {\isaliteral{28}{\isacharparenleft}}subst\ lfp{\isaliteral{5F}{\isacharunderscore}}unfold{\isaliteral{5B}{\isacharbrackleft}}OF\ mono{\isaliteral{5F}{\isacharunderscore}}ef{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}% |
|
213 \begin{isamarkuptxt}% |
|
214 \begin{isabelle}% |
|
215 \ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C416E643E}{\isasymAnd}}x\ t{\isaliteral{2E}{\isachardot}}\ t\ {\isaliteral{5C3C696E3E}{\isasymin}}\ A\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ t\ {\isaliteral{5C3C696E3E}{\isasymin}}\ A\ {\isaliteral{5C3C756E696F6E3E}{\isasymunion}}\ M{\isaliteral{5C3C696E76657273653E}{\isasyminverse}}\ {\isaliteral{60}{\isacharbackquote}}{\isaliteral{60}{\isacharbackquote}}\ lfp\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}T{\isaliteral{2E}{\isachardot}}\ A\ {\isaliteral{5C3C756E696F6E3E}{\isasymunion}}\ M{\isaliteral{5C3C696E76657273653E}{\isasyminverse}}\ {\isaliteral{60}{\isacharbackquote}}{\isaliteral{60}{\isacharbackquote}}\ T{\isaliteral{29}{\isacharparenright}}% |
|
216 \end{isabelle} |
|
217 and disposing of the resulting trivial subgoal automatically:% |
|
218 \end{isamarkuptxt}% |
|
219 \isamarkuptrue% |
|
220 \ \isacommand{apply}\isamarkupfalse% |
|
221 {\isaliteral{28}{\isacharparenleft}}blast{\isaliteral{29}{\isacharparenright}}% |
|
222 \begin{isamarkuptxt}% |
|
223 \noindent |
|
224 The proof of the induction step is identical to the one for the base case:% |
|
225 \end{isamarkuptxt}% |
|
226 \isamarkuptrue% |
|
227 \isacommand{apply}\isamarkupfalse% |
|
228 {\isaliteral{28}{\isacharparenleft}}subst\ lfp{\isaliteral{5F}{\isacharunderscore}}unfold{\isaliteral{5B}{\isacharbrackleft}}OF\ mono{\isaliteral{5F}{\isacharunderscore}}ef{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}\isanewline |
|
229 \isacommand{apply}\isamarkupfalse% |
|
230 {\isaliteral{28}{\isacharparenleft}}blast{\isaliteral{29}{\isacharparenright}}\isanewline |
|
231 \isacommand{done}\isamarkupfalse% |
|
232 % |
|
233 \endisatagproof |
|
234 {\isafoldproof}% |
|
235 % |
|
236 \isadelimproof |
|
237 % |
|
238 \endisadelimproof |
|
239 % |
|
240 \begin{isamarkuptext}% |
|
241 The main theorem is proved in the familiar manner: induction followed by |
|
242 \isa{auto} augmented with the lemma as a simplification rule.% |
|
243 \end{isamarkuptext}% |
|
244 \isamarkuptrue% |
|
245 \isacommand{theorem}\isamarkupfalse% |
|
246 \ {\isaliteral{22}{\isachardoublequoteopen}}mc\ f\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{7B}{\isacharbraceleft}}s{\isaliteral{2E}{\isachardot}}\ s\ {\isaliteral{5C3C5475726E7374696C653E}{\isasymTurnstile}}\ f{\isaliteral{7D}{\isacharbraceright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
|
247 % |
|
248 \isadelimproof |
|
249 % |
|
250 \endisadelimproof |
|
251 % |
|
252 \isatagproof |
|
253 \isacommand{apply}\isamarkupfalse% |
|
254 {\isaliteral{28}{\isacharparenleft}}induct{\isaliteral{5F}{\isacharunderscore}}tac\ f{\isaliteral{29}{\isacharparenright}}\isanewline |
|
255 \isacommand{apply}\isamarkupfalse% |
|
256 {\isaliteral{28}{\isacharparenleft}}auto\ simp\ add{\isaliteral{3A}{\isacharcolon}}\ EF{\isaliteral{5F}{\isacharunderscore}}lemma{\isaliteral{29}{\isacharparenright}}\isanewline |
|
257 \isacommand{done}\isamarkupfalse% |
|
258 % |
|
259 \endisatagproof |
|
260 {\isafoldproof}% |
|
261 % |
|
262 \isadelimproof |
|
263 % |
|
264 \endisadelimproof |
|
265 % |
|
266 \begin{isamarkuptext}% |
|
267 \begin{exercise} |
|
268 \isa{AX} has a dual operator \isa{EN} |
|
269 (``there exists a next state such that'')% |
|
270 \footnote{We cannot use the customary \isa{EX}: it is reserved |
|
271 as the \textsc{ascii}-equivalent of \isa{{\isaliteral{5C3C6578697374733E}{\isasymexists}}}.} |
|
272 with the intended semantics |
|
273 \begin{isabelle}% |
|
274 \ \ \ \ \ s\ {\isaliteral{5C3C5475726E7374696C653E}{\isasymTurnstile}}\ EN\ f\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6578697374733E}{\isasymexists}}t{\isaliteral{2E}{\isachardot}}\ {\isaliteral{28}{\isacharparenleft}}s{\isaliteral{2C}{\isacharcomma}}\ t{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ M\ {\isaliteral{5C3C616E643E}{\isasymand}}\ t\ {\isaliteral{5C3C5475726E7374696C653E}{\isasymTurnstile}}\ f{\isaliteral{29}{\isacharparenright}}% |
|
275 \end{isabelle} |
|
276 Fortunately, \isa{EN\ f} can already be expressed as a PDL formula. How? |
|
277 |
|
278 Show that the semantics for \isa{EF} satisfies the following recursion equation: |
|
279 \begin{isabelle}% |
|
280 \ \ \ \ \ s\ {\isaliteral{5C3C5475726E7374696C653E}{\isasymTurnstile}}\ EF\ f\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}s\ {\isaliteral{5C3C5475726E7374696C653E}{\isasymTurnstile}}\ f\ {\isaliteral{5C3C6F723E}{\isasymor}}\ s\ {\isaliteral{5C3C5475726E7374696C653E}{\isasymTurnstile}}\ EN\ {\isaliteral{28}{\isacharparenleft}}EF\ f{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}% |
|
281 \end{isabelle} |
|
282 \end{exercise} |
|
283 \index{PDL|)}% |
|
284 \end{isamarkuptext}% |
|
285 \isamarkuptrue% |
|
286 % |
|
287 \isadelimproof |
|
288 % |
|
289 \endisadelimproof |
|
290 % |
|
291 \isatagproof |
|
292 % |
|
293 \endisatagproof |
|
294 {\isafoldproof}% |
|
295 % |
|
296 \isadelimproof |
|
297 % |
|
298 \endisadelimproof |
|
299 % |
|
300 \isadelimproof |
|
301 % |
|
302 \endisadelimproof |
|
303 % |
|
304 \isatagproof |
|
305 % |
|
306 \endisatagproof |
|
307 {\isafoldproof}% |
|
308 % |
|
309 \isadelimproof |
|
310 % |
|
311 \endisadelimproof |
|
312 % |
|
313 \isadelimproof |
|
314 % |
|
315 \endisadelimproof |
|
316 % |
|
317 \isatagproof |
|
318 % |
|
319 \endisatagproof |
|
320 {\isafoldproof}% |
|
321 % |
|
322 \isadelimproof |
|
323 % |
|
324 \endisadelimproof |
|
325 % |
|
326 \isadelimtheory |
|
327 % |
|
328 \endisadelimtheory |
|
329 % |
|
330 \isatagtheory |
|
331 % |
|
332 \endisatagtheory |
|
333 {\isafoldtheory}% |
|
334 % |
|
335 \isadelimtheory |
|
336 % |
|
337 \endisadelimtheory |
|
338 \end{isabellebody}% |
|
339 %%% Local Variables: |
|
340 %%% mode: latex |
|
341 %%% TeX-master: "root" |
|
342 %%% End: |
|