28 syntax trees, they are naturally modelled as a datatype:% |
28 syntax trees, they are naturally modelled as a datatype:% |
29 \footnote{The customary definition of PDL |
29 \footnote{The customary definition of PDL |
30 \cite{HarelKT-DL} looks quite different from ours, but the two are easily |
30 \cite{HarelKT-DL} looks quite different from ours, but the two are easily |
31 shown to be equivalent.}% |
31 shown to be equivalent.}% |
32 \end{isamarkuptext}% |
32 \end{isamarkuptext}% |
33 \isamarkupfalse% |
33 \isamarkuptrue% |
34 \isacommand{datatype}\ formula\ {\isacharequal}\ Atom\ atom\isanewline |
34 \isacommand{datatype}\isamarkupfalse% |
|
35 \ formula\ {\isacharequal}\ Atom\ atom\isanewline |
35 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharbar}\ Neg\ formula\isanewline |
36 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharbar}\ Neg\ formula\isanewline |
36 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharbar}\ And\ formula\ formula\isanewline |
37 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharbar}\ And\ formula\ formula\isanewline |
37 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharbar}\ AX\ formula\isanewline |
38 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharbar}\ AX\ formula\isanewline |
38 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharbar}\ EF\ formula\isamarkuptrue% |
39 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharbar}\ EF\ formula% |
39 % |
|
40 \begin{isamarkuptext}% |
40 \begin{isamarkuptext}% |
41 \noindent |
41 \noindent |
42 This resembles the boolean expression case study in |
42 This resembles the boolean expression case study in |
43 \S\ref{sec:boolex}. |
43 \S\ref{sec:boolex}. |
44 A validity relation between |
44 A validity relation between |
45 states and formulae specifies the semantics:% |
45 states and formulae specifies the semantics:% |
46 \end{isamarkuptext}% |
46 \end{isamarkuptext}% |
47 \isamarkupfalse% |
47 \isamarkuptrue% |
48 \isacommand{consts}\ valid\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}state\ {\isasymRightarrow}\ formula\ {\isasymRightarrow}\ bool{\isachardoublequote}\ \ \ {\isacharparenleft}{\isachardoublequote}{\isacharparenleft}{\isacharunderscore}\ {\isasymTurnstile}\ {\isacharunderscore}{\isacharparenright}{\isachardoublequote}\ {\isacharbrackleft}{\isadigit{8}}{\isadigit{0}}{\isacharcomma}{\isadigit{8}}{\isadigit{0}}{\isacharbrackright}\ {\isadigit{8}}{\isadigit{0}}{\isacharparenright}\isamarkuptrue% |
48 \isacommand{consts}\isamarkupfalse% |
49 % |
49 \ valid\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}state\ {\isasymRightarrow}\ formula\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\ \ \ {\isacharparenleft}{\isachardoublequoteopen}{\isacharparenleft}{\isacharunderscore}\ {\isasymTurnstile}\ {\isacharunderscore}{\isacharparenright}{\isachardoublequoteclose}\ {\isacharbrackleft}{\isadigit{8}}{\isadigit{0}}{\isacharcomma}{\isadigit{8}}{\isadigit{0}}{\isacharbrackright}\ {\isadigit{8}}{\isadigit{0}}{\isacharparenright}% |
50 \begin{isamarkuptext}% |
50 \begin{isamarkuptext}% |
51 \noindent |
51 \noindent |
52 The syntax annotation allows us to write \isa{s\ {\isasymTurnstile}\ f} instead of |
52 The syntax annotation allows us to write \isa{s\ {\isasymTurnstile}\ f} instead of |
53 \hbox{\isa{valid\ s\ f}}. |
53 \hbox{\isa{valid\ s\ f}}. |
54 The definition of \isa{{\isasymTurnstile}} is by recursion over the syntax:% |
54 The definition of \isa{{\isasymTurnstile}} is by recursion over the syntax:% |
55 \end{isamarkuptext}% |
55 \end{isamarkuptext}% |
56 \isamarkupfalse% |
56 \isamarkuptrue% |
57 \isacommand{primrec}\isanewline |
57 \isacommand{primrec}\isamarkupfalse% |
58 {\isachardoublequote}s\ {\isasymTurnstile}\ Atom\ a\ \ {\isacharequal}\ {\isacharparenleft}a\ {\isasymin}\ L\ s{\isacharparenright}{\isachardoublequote}\isanewline |
58 \isanewline |
59 {\isachardoublequote}s\ {\isasymTurnstile}\ Neg\ f\ \ \ {\isacharequal}\ {\isacharparenleft}{\isasymnot}{\isacharparenleft}s\ {\isasymTurnstile}\ f{\isacharparenright}{\isacharparenright}{\isachardoublequote}\isanewline |
59 {\isachardoublequoteopen}s\ {\isasymTurnstile}\ Atom\ a\ \ {\isacharequal}\ {\isacharparenleft}a\ {\isasymin}\ L\ s{\isacharparenright}{\isachardoublequoteclose}\isanewline |
60 {\isachardoublequote}s\ {\isasymTurnstile}\ And\ f\ g\ {\isacharequal}\ {\isacharparenleft}s\ {\isasymTurnstile}\ f\ {\isasymand}\ s\ {\isasymTurnstile}\ g{\isacharparenright}{\isachardoublequote}\isanewline |
60 {\isachardoublequoteopen}s\ {\isasymTurnstile}\ Neg\ f\ \ \ {\isacharequal}\ {\isacharparenleft}{\isasymnot}{\isacharparenleft}s\ {\isasymTurnstile}\ f{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline |
61 {\isachardoublequote}s\ {\isasymTurnstile}\ AX\ f\ \ \ \ {\isacharequal}\ {\isacharparenleft}{\isasymforall}t{\isachardot}\ {\isacharparenleft}s{\isacharcomma}t{\isacharparenright}\ {\isasymin}\ M\ {\isasymlongrightarrow}\ t\ {\isasymTurnstile}\ f{\isacharparenright}{\isachardoublequote}\isanewline |
61 {\isachardoublequoteopen}s\ {\isasymTurnstile}\ And\ f\ g\ {\isacharequal}\ {\isacharparenleft}s\ {\isasymTurnstile}\ f\ {\isasymand}\ s\ {\isasymTurnstile}\ g{\isacharparenright}{\isachardoublequoteclose}\isanewline |
62 {\isachardoublequote}s\ {\isasymTurnstile}\ EF\ f\ \ \ \ {\isacharequal}\ {\isacharparenleft}{\isasymexists}t{\isachardot}\ {\isacharparenleft}s{\isacharcomma}t{\isacharparenright}\ {\isasymin}\ M\isactrlsup {\isacharasterisk}\ {\isasymand}\ t\ {\isasymTurnstile}\ f{\isacharparenright}{\isachardoublequote}\isamarkuptrue% |
62 {\isachardoublequoteopen}s\ {\isasymTurnstile}\ AX\ f\ \ \ \ {\isacharequal}\ {\isacharparenleft}{\isasymforall}t{\isachardot}\ {\isacharparenleft}s{\isacharcomma}t{\isacharparenright}\ {\isasymin}\ M\ {\isasymlongrightarrow}\ t\ {\isasymTurnstile}\ f{\isacharparenright}{\isachardoublequoteclose}\isanewline |
63 % |
63 {\isachardoublequoteopen}s\ {\isasymTurnstile}\ EF\ f\ \ \ \ {\isacharequal}\ {\isacharparenleft}{\isasymexists}t{\isachardot}\ {\isacharparenleft}s{\isacharcomma}t{\isacharparenright}\ {\isasymin}\ M\isactrlsup {\isacharasterisk}\ {\isasymand}\ t\ {\isasymTurnstile}\ f{\isacharparenright}{\isachardoublequoteclose}% |
64 \begin{isamarkuptext}% |
64 \begin{isamarkuptext}% |
65 \noindent |
65 \noindent |
66 The first three equations should be self-explanatory. The temporal formula |
66 The first three equations should be self-explanatory. The temporal formula |
67 \isa{AX\ f} means that \isa{f} is true in \emph{A}ll ne\emph{X}t states whereas |
67 \isa{AX\ f} means that \isa{f} is true in \emph{A}ll ne\emph{X}t states whereas |
68 \isa{EF\ f} means that there \emph{E}xists some \emph{F}uture state in which \isa{f} is |
68 \isa{EF\ f} means that there \emph{E}xists some \emph{F}uture state in which \isa{f} is |
70 closure. Because of reflexivity, the future includes the present. |
70 closure. Because of reflexivity, the future includes the present. |
71 |
71 |
72 Now we come to the model checker itself. It maps a formula into the set of |
72 Now we come to the model checker itself. It maps a formula into the set of |
73 states where the formula is true. It too is defined by recursion over the syntax:% |
73 states where the formula is true. It too is defined by recursion over the syntax:% |
74 \end{isamarkuptext}% |
74 \end{isamarkuptext}% |
75 \isamarkupfalse% |
75 \isamarkuptrue% |
76 \isacommand{consts}\ mc\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}formula\ {\isasymRightarrow}\ state\ set{\isachardoublequote}\isanewline |
76 \isacommand{consts}\isamarkupfalse% |
77 \isamarkupfalse% |
77 \ mc\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}formula\ {\isasymRightarrow}\ state\ set{\isachardoublequoteclose}\isanewline |
78 \isacommand{primrec}\isanewline |
78 \isacommand{primrec}\isamarkupfalse% |
79 {\isachardoublequote}mc{\isacharparenleft}Atom\ a{\isacharparenright}\ \ {\isacharequal}\ {\isacharbraceleft}s{\isachardot}\ a\ {\isasymin}\ L\ s{\isacharbraceright}{\isachardoublequote}\isanewline |
79 \isanewline |
80 {\isachardoublequote}mc{\isacharparenleft}Neg\ f{\isacharparenright}\ \ \ {\isacharequal}\ {\isacharminus}mc\ f{\isachardoublequote}\isanewline |
80 {\isachardoublequoteopen}mc{\isacharparenleft}Atom\ a{\isacharparenright}\ \ {\isacharequal}\ {\isacharbraceleft}s{\isachardot}\ a\ {\isasymin}\ L\ s{\isacharbraceright}{\isachardoublequoteclose}\isanewline |
81 {\isachardoublequote}mc{\isacharparenleft}And\ f\ g{\isacharparenright}\ {\isacharequal}\ mc\ f\ {\isasyminter}\ mc\ g{\isachardoublequote}\isanewline |
81 {\isachardoublequoteopen}mc{\isacharparenleft}Neg\ f{\isacharparenright}\ \ \ {\isacharequal}\ {\isacharminus}mc\ f{\isachardoublequoteclose}\isanewline |
82 {\isachardoublequote}mc{\isacharparenleft}AX\ f{\isacharparenright}\ \ \ \ {\isacharequal}\ {\isacharbraceleft}s{\isachardot}\ {\isasymforall}t{\isachardot}\ {\isacharparenleft}s{\isacharcomma}t{\isacharparenright}\ {\isasymin}\ M\ \ {\isasymlongrightarrow}\ t\ {\isasymin}\ mc\ f{\isacharbraceright}{\isachardoublequote}\isanewline |
82 {\isachardoublequoteopen}mc{\isacharparenleft}And\ f\ g{\isacharparenright}\ {\isacharequal}\ mc\ f\ {\isasyminter}\ mc\ g{\isachardoublequoteclose}\isanewline |
83 {\isachardoublequote}mc{\isacharparenleft}EF\ f{\isacharparenright}\ \ \ \ {\isacharequal}\ lfp{\isacharparenleft}{\isasymlambda}T{\isachardot}\ mc\ f\ {\isasymunion}\ {\isacharparenleft}M{\isasyminverse}\ {\isacharbackquote}{\isacharbackquote}\ T{\isacharparenright}{\isacharparenright}{\isachardoublequote}\isamarkuptrue% |
83 {\isachardoublequoteopen}mc{\isacharparenleft}AX\ f{\isacharparenright}\ \ \ \ {\isacharequal}\ {\isacharbraceleft}s{\isachardot}\ {\isasymforall}t{\isachardot}\ {\isacharparenleft}s{\isacharcomma}t{\isacharparenright}\ {\isasymin}\ M\ \ {\isasymlongrightarrow}\ t\ {\isasymin}\ mc\ f{\isacharbraceright}{\isachardoublequoteclose}\isanewline |
84 % |
84 {\isachardoublequoteopen}mc{\isacharparenleft}EF\ f{\isacharparenright}\ \ \ \ {\isacharequal}\ lfp{\isacharparenleft}{\isasymlambda}T{\isachardot}\ mc\ f\ {\isasymunion}\ {\isacharparenleft}M{\isasyminverse}\ {\isacharbackquote}{\isacharbackquote}\ T{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}% |
85 \begin{isamarkuptext}% |
85 \begin{isamarkuptext}% |
86 \noindent |
86 \noindent |
87 Only the equation for \isa{EF} deserves some comments. Remember that the |
87 Only the equation for \isa{EF} deserves some comments. Remember that the |
88 postfix \isa{{\isasyminverse}} and the infix \isa{{\isacharbackquote}{\isacharbackquote}} are predefined and denote the |
88 postfix \isa{{\isasyminverse}} and the infix \isa{{\isacharbackquote}{\isacharbackquote}} are predefined and denote the |
89 converse of a relation and the image of a set under a relation. Thus |
89 converse of a relation and the image of a set under a relation. Thus |
95 will be proved in a moment. |
95 will be proved in a moment. |
96 |
96 |
97 First we prove monotonicity of the function inside \isa{lfp} |
97 First we prove monotonicity of the function inside \isa{lfp} |
98 in order to make sure it really has a least fixed point.% |
98 in order to make sure it really has a least fixed point.% |
99 \end{isamarkuptext}% |
99 \end{isamarkuptext}% |
100 \isamarkupfalse% |
100 \isamarkuptrue% |
101 \isacommand{lemma}\ mono{\isacharunderscore}ef{\isacharcolon}\ {\isachardoublequote}mono{\isacharparenleft}{\isasymlambda}T{\isachardot}\ A\ {\isasymunion}\ {\isacharparenleft}M{\isasyminverse}\ {\isacharbackquote}{\isacharbackquote}\ T{\isacharparenright}{\isacharparenright}{\isachardoublequote}\isanewline |
101 \isacommand{lemma}\isamarkupfalse% |
102 % |
102 \ mono{\isacharunderscore}ef{\isacharcolon}\ {\isachardoublequoteopen}mono{\isacharparenleft}{\isasymlambda}T{\isachardot}\ A\ {\isasymunion}\ {\isacharparenleft}M{\isasyminverse}\ {\isacharbackquote}{\isacharbackquote}\ T{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline |
103 \isadelimproof |
103 % |
104 % |
104 \isadelimproof |
105 \endisadelimproof |
105 % |
106 % |
106 \endisadelimproof |
107 \isatagproof |
107 % |
108 \isamarkupfalse% |
108 \isatagproof |
109 \isacommand{apply}{\isacharparenleft}rule\ monoI{\isacharparenright}\isanewline |
109 \isacommand{apply}\isamarkupfalse% |
110 \isamarkupfalse% |
110 {\isacharparenleft}rule\ monoI{\isacharparenright}\isanewline |
111 \isacommand{apply}\ blast\isanewline |
111 \isacommand{apply}\isamarkupfalse% |
112 \isamarkupfalse% |
112 \ blast\isanewline |
113 \isacommand{done}% |
113 \isacommand{done}\isamarkupfalse% |
114 \endisatagproof |
114 % |
115 {\isafoldproof}% |
115 \endisatagproof |
116 % |
116 {\isafoldproof}% |
117 \isadelimproof |
117 % |
118 % |
118 \isadelimproof |
119 \endisadelimproof |
119 % |
120 \isamarkuptrue% |
120 \endisadelimproof |
121 % |
121 % |
122 \begin{isamarkuptext}% |
122 \begin{isamarkuptext}% |
123 \noindent |
123 \noindent |
124 Now we can relate model checking and semantics. For the \isa{EF} case we need |
124 Now we can relate model checking and semantics. For the \isa{EF} case we need |
125 a separate lemma:% |
125 a separate lemma:% |
126 \end{isamarkuptext}% |
126 \end{isamarkuptext}% |
127 \isamarkupfalse% |
127 \isamarkuptrue% |
128 \isacommand{lemma}\ EF{\isacharunderscore}lemma{\isacharcolon}\isanewline |
128 \isacommand{lemma}\isamarkupfalse% |
129 \ \ {\isachardoublequote}lfp{\isacharparenleft}{\isasymlambda}T{\isachardot}\ A\ {\isasymunion}\ {\isacharparenleft}M{\isasyminverse}\ {\isacharbackquote}{\isacharbackquote}\ T{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ {\isacharbraceleft}s{\isachardot}\ {\isasymexists}t{\isachardot}\ {\isacharparenleft}s{\isacharcomma}t{\isacharparenright}\ {\isasymin}\ M\isactrlsup {\isacharasterisk}\ {\isasymand}\ t\ {\isasymin}\ A{\isacharbraceright}{\isachardoublequote}% |
129 \ EF{\isacharunderscore}lemma{\isacharcolon}\isanewline |
130 \isadelimproof |
130 \ \ {\isachardoublequoteopen}lfp{\isacharparenleft}{\isasymlambda}T{\isachardot}\ A\ {\isasymunion}\ {\isacharparenleft}M{\isasyminverse}\ {\isacharbackquote}{\isacharbackquote}\ T{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ {\isacharbraceleft}s{\isachardot}\ {\isasymexists}t{\isachardot}\ {\isacharparenleft}s{\isacharcomma}t{\isacharparenright}\ {\isasymin}\ M\isactrlsup {\isacharasterisk}\ {\isasymand}\ t\ {\isasymin}\ A{\isacharbraceright}{\isachardoublequoteclose}% |
131 % |
131 \isadelimproof |
132 \endisadelimproof |
132 % |
133 % |
133 \endisadelimproof |
134 \isatagproof |
134 % |
135 \isamarkuptrue% |
135 \isatagproof |
136 % |
136 % |
137 \begin{isamarkuptxt}% |
137 \begin{isamarkuptxt}% |
138 \noindent |
138 \noindent |
139 The equality is proved in the canonical fashion by proving that each set |
139 The equality is proved in the canonical fashion by proving that each set |
140 includes the other; the inclusion is shown pointwise:% |
140 includes the other; the inclusion is shown pointwise:% |
141 \end{isamarkuptxt}% |
141 \end{isamarkuptxt}% |
142 \isamarkupfalse% |
142 \isamarkuptrue% |
143 \isacommand{apply}{\isacharparenleft}rule\ equalityI{\isacharparenright}\isanewline |
143 \isacommand{apply}\isamarkupfalse% |
144 \ \isamarkupfalse% |
144 {\isacharparenleft}rule\ equalityI{\isacharparenright}\isanewline |
145 \isacommand{apply}{\isacharparenleft}rule\ subsetI{\isacharparenright}\isanewline |
145 \ \isacommand{apply}\isamarkupfalse% |
146 \ \isamarkupfalse% |
146 {\isacharparenleft}rule\ subsetI{\isacharparenright}\isanewline |
147 \isacommand{apply}{\isacharparenleft}simp{\isacharparenright}\isamarkuptrue% |
147 \ \isacommand{apply}\isamarkupfalse% |
|
148 {\isacharparenleft}simp{\isacharparenright}\isamarkupfalse% |
148 % |
149 % |
149 \begin{isamarkuptxt}% |
150 \begin{isamarkuptxt}% |
150 \noindent |
151 \noindent |
151 Simplification leaves us with the following first subgoal |
152 Simplification leaves us with the following first subgoal |
152 \begin{isabelle}% |
153 \begin{isabelle}% |
153 \ {\isadigit{1}}{\isachardot}\ {\isasymAnd}s{\isachardot}\ s\ {\isasymin}\ lfp\ {\isacharparenleft}{\isasymlambda}T{\isachardot}\ A\ {\isasymunion}\ M{\isasyminverse}\ {\isacharbackquote}{\isacharbackquote}\ T{\isacharparenright}\ {\isasymLongrightarrow}\ {\isasymexists}t{\isachardot}\ {\isacharparenleft}s{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\isactrlsup {\isacharasterisk}\ {\isasymand}\ t\ {\isasymin}\ A% |
154 \ {\isadigit{1}}{\isachardot}\ {\isasymAnd}s{\isachardot}\ s\ {\isasymin}\ lfp\ {\isacharparenleft}{\isasymlambda}T{\isachardot}\ A\ {\isasymunion}\ M{\isasyminverse}\ {\isacharbackquote}{\isacharbackquote}\ T{\isacharparenright}\ {\isasymLongrightarrow}\ {\isasymexists}t{\isachardot}\ {\isacharparenleft}s{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\isactrlsup {\isacharasterisk}\ {\isasymand}\ t\ {\isasymin}\ A% |
154 \end{isabelle} |
155 \end{isabelle} |
155 which is proved by \isa{lfp}-induction:% |
156 which is proved by \isa{lfp}-induction:% |
156 \end{isamarkuptxt}% |
157 \end{isamarkuptxt}% |
157 \ \isamarkupfalse% |
158 \isamarkuptrue% |
158 \isacommand{apply}{\isacharparenleft}erule\ lfp{\isacharunderscore}induct{\isacharparenright}\isanewline |
159 \ \isacommand{apply}\isamarkupfalse% |
159 \ \ \isamarkupfalse% |
160 {\isacharparenleft}erule\ lfp{\isacharunderscore}induct{\isacharparenright}\isanewline |
160 \isacommand{apply}{\isacharparenleft}rule\ mono{\isacharunderscore}ef{\isacharparenright}\isanewline |
161 \ \ \isacommand{apply}\isamarkupfalse% |
161 \ \isamarkupfalse% |
162 {\isacharparenleft}rule\ mono{\isacharunderscore}ef{\isacharparenright}\isanewline |
162 \isacommand{apply}{\isacharparenleft}simp{\isacharparenright}\isamarkuptrue% |
163 \ \isacommand{apply}\isamarkupfalse% |
163 % |
164 {\isacharparenleft}simp{\isacharparenright}% |
164 \begin{isamarkuptxt}% |
165 \begin{isamarkuptxt}% |
165 \noindent |
166 \noindent |
166 Having disposed of the monotonicity subgoal, |
167 Having disposed of the monotonicity subgoal, |
167 simplification leaves us with the following goal: |
168 simplification leaves us with the following goal: |
168 \begin{isabelle} |
169 \begin{isabelle} |
171 \ \ \ \ \ \ \ \ {\isasymLongrightarrow}\ {\isasymexists}t{\isachardot}\ {\isacharparenleft}x{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\isactrlsup {\isacharasterisk}\ {\isasymand}\ t\ {\isasymin}\ A |
172 \ \ \ \ \ \ \ \ {\isasymLongrightarrow}\ {\isasymexists}t{\isachardot}\ {\isacharparenleft}x{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\isactrlsup {\isacharasterisk}\ {\isasymand}\ t\ {\isasymin}\ A |
172 \end{isabelle} |
173 \end{isabelle} |
173 It is proved by \isa{blast}, using the transitivity of |
174 It is proved by \isa{blast}, using the transitivity of |
174 \isa{M\isactrlsup {\isacharasterisk}}.% |
175 \isa{M\isactrlsup {\isacharasterisk}}.% |
175 \end{isamarkuptxt}% |
176 \end{isamarkuptxt}% |
176 \ \isamarkupfalse% |
177 \isamarkuptrue% |
177 \isacommand{apply}{\isacharparenleft}blast\ intro{\isacharcolon}\ rtrancl{\isacharunderscore}trans{\isacharparenright}\isamarkuptrue% |
178 \ \isacommand{apply}\isamarkupfalse% |
178 % |
179 {\isacharparenleft}blast\ intro{\isacharcolon}\ rtrancl{\isacharunderscore}trans{\isacharparenright}% |
179 \begin{isamarkuptxt}% |
180 \begin{isamarkuptxt}% |
180 We now return to the second set inclusion subgoal, which is again proved |
181 We now return to the second set inclusion subgoal, which is again proved |
181 pointwise:% |
182 pointwise:% |
182 \end{isamarkuptxt}% |
183 \end{isamarkuptxt}% |
183 \isamarkupfalse% |
184 \isamarkuptrue% |
184 \isacommand{apply}{\isacharparenleft}rule\ subsetI{\isacharparenright}\isanewline |
185 \isacommand{apply}\isamarkupfalse% |
185 \isamarkupfalse% |
186 {\isacharparenleft}rule\ subsetI{\isacharparenright}\isanewline |
186 \isacommand{apply}{\isacharparenleft}simp{\isacharcomma}\ clarify{\isacharparenright}\isamarkuptrue% |
187 \isacommand{apply}\isamarkupfalse% |
187 % |
188 {\isacharparenleft}simp{\isacharcomma}\ clarify{\isacharparenright}% |
188 \begin{isamarkuptxt}% |
189 \begin{isamarkuptxt}% |
189 \noindent |
190 \noindent |
190 After simplification and clarification we are left with |
191 After simplification and clarification we are left with |
191 \begin{isabelle}% |
192 \begin{isabelle}% |
192 \ {\isadigit{1}}{\isachardot}\ {\isasymAnd}x\ t{\isachardot}\ {\isasymlbrakk}{\isacharparenleft}x{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\isactrlsup {\isacharasterisk}{\isacharsemicolon}\ t\ {\isasymin}\ A{\isasymrbrakk}\ {\isasymLongrightarrow}\ x\ {\isasymin}\ lfp\ {\isacharparenleft}{\isasymlambda}T{\isachardot}\ A\ {\isasymunion}\ M{\isasyminverse}\ {\isacharbackquote}{\isacharbackquote}\ T{\isacharparenright}% |
193 \ {\isadigit{1}}{\isachardot}\ {\isasymAnd}x\ t{\isachardot}\ {\isasymlbrakk}{\isacharparenleft}x{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\isactrlsup {\isacharasterisk}{\isacharsemicolon}\ t\ {\isasymin}\ A{\isasymrbrakk}\ {\isasymLongrightarrow}\ x\ {\isasymin}\ lfp\ {\isacharparenleft}{\isasymlambda}T{\isachardot}\ A\ {\isasymunion}\ M{\isasyminverse}\ {\isacharbackquote}{\isacharbackquote}\ T{\isacharparenright}% |
203 \end{isabelle} |
204 \end{isabelle} |
204 It says that if \isa{{\isacharparenleft}a{\isacharcomma}\ b{\isacharparenright}\ {\isasymin}\ r\isactrlsup {\isacharasterisk}} and we know \isa{P\ b} then we can infer |
205 It says that if \isa{{\isacharparenleft}a{\isacharcomma}\ b{\isacharparenright}\ {\isasymin}\ r\isactrlsup {\isacharasterisk}} and we know \isa{P\ b} then we can infer |
205 \isa{P\ a} provided each step backwards from a predecessor \isa{z} of |
206 \isa{P\ a} provided each step backwards from a predecessor \isa{z} of |
206 \isa{b} preserves \isa{P}.% |
207 \isa{b} preserves \isa{P}.% |
207 \end{isamarkuptxt}% |
208 \end{isamarkuptxt}% |
208 \isamarkupfalse% |
209 \isamarkuptrue% |
209 \isacommand{apply}{\isacharparenleft}erule\ converse{\isacharunderscore}rtrancl{\isacharunderscore}induct{\isacharparenright}\isamarkuptrue% |
210 \isacommand{apply}\isamarkupfalse% |
210 % |
211 {\isacharparenleft}erule\ converse{\isacharunderscore}rtrancl{\isacharunderscore}induct{\isacharparenright}% |
211 \begin{isamarkuptxt}% |
212 \begin{isamarkuptxt}% |
212 \noindent |
213 \noindent |
213 The base case |
214 The base case |
214 \begin{isabelle}% |
215 \begin{isabelle}% |
215 \ {\isadigit{1}}{\isachardot}\ {\isasymAnd}x\ t{\isachardot}\ t\ {\isasymin}\ A\ {\isasymLongrightarrow}\ t\ {\isasymin}\ lfp\ {\isacharparenleft}{\isasymlambda}T{\isachardot}\ A\ {\isasymunion}\ M{\isasyminverse}\ {\isacharbackquote}{\isacharbackquote}\ T{\isacharparenright}% |
216 \ {\isadigit{1}}{\isachardot}\ {\isasymAnd}x\ t{\isachardot}\ t\ {\isasymin}\ A\ {\isasymLongrightarrow}\ t\ {\isasymin}\ lfp\ {\isacharparenleft}{\isasymlambda}T{\isachardot}\ A\ {\isasymunion}\ M{\isasyminverse}\ {\isacharbackquote}{\isacharbackquote}\ T{\isacharparenright}% |
216 \end{isabelle} |
217 \end{isabelle} |
217 is solved by unrolling \isa{lfp} once% |
218 is solved by unrolling \isa{lfp} once% |
218 \end{isamarkuptxt}% |
219 \end{isamarkuptxt}% |
219 \ \isamarkupfalse% |
220 \isamarkuptrue% |
220 \isacommand{apply}{\isacharparenleft}subst\ lfp{\isacharunderscore}unfold{\isacharbrackleft}OF\ mono{\isacharunderscore}ef{\isacharbrackright}{\isacharparenright}\isamarkuptrue% |
221 \ \isacommand{apply}\isamarkupfalse% |
221 % |
222 {\isacharparenleft}subst\ lfp{\isacharunderscore}unfold{\isacharbrackleft}OF\ mono{\isacharunderscore}ef{\isacharbrackright}{\isacharparenright}% |
222 \begin{isamarkuptxt}% |
223 \begin{isamarkuptxt}% |
223 \begin{isabelle}% |
224 \begin{isabelle}% |
224 \ {\isadigit{1}}{\isachardot}\ {\isasymAnd}x\ t{\isachardot}\ t\ {\isasymin}\ A\ {\isasymLongrightarrow}\ t\ {\isasymin}\ A\ {\isasymunion}\ M{\isasyminverse}\ {\isacharbackquote}{\isacharbackquote}\ lfp\ {\isacharparenleft}{\isasymlambda}T{\isachardot}\ A\ {\isasymunion}\ M{\isasyminverse}\ {\isacharbackquote}{\isacharbackquote}\ T{\isacharparenright}% |
225 \ {\isadigit{1}}{\isachardot}\ {\isasymAnd}x\ t{\isachardot}\ t\ {\isasymin}\ A\ {\isasymLongrightarrow}\ t\ {\isasymin}\ A\ {\isasymunion}\ M{\isasyminverse}\ {\isacharbackquote}{\isacharbackquote}\ lfp\ {\isacharparenleft}{\isasymlambda}T{\isachardot}\ A\ {\isasymunion}\ M{\isasyminverse}\ {\isacharbackquote}{\isacharbackquote}\ T{\isacharparenright}% |
225 \end{isabelle} |
226 \end{isabelle} |
226 and disposing of the resulting trivial subgoal automatically:% |
227 and disposing of the resulting trivial subgoal automatically:% |
227 \end{isamarkuptxt}% |
228 \end{isamarkuptxt}% |
228 \ \isamarkupfalse% |
229 \isamarkuptrue% |
229 \isacommand{apply}{\isacharparenleft}blast{\isacharparenright}\isamarkuptrue% |
230 \ \isacommand{apply}\isamarkupfalse% |
230 % |
231 {\isacharparenleft}blast{\isacharparenright}% |
231 \begin{isamarkuptxt}% |
232 \begin{isamarkuptxt}% |
232 \noindent |
233 \noindent |
233 The proof of the induction step is identical to the one for the base case:% |
234 The proof of the induction step is identical to the one for the base case:% |
234 \end{isamarkuptxt}% |
235 \end{isamarkuptxt}% |
235 \isamarkupfalse% |
236 \isamarkuptrue% |
236 \isacommand{apply}{\isacharparenleft}subst\ lfp{\isacharunderscore}unfold{\isacharbrackleft}OF\ mono{\isacharunderscore}ef{\isacharbrackright}{\isacharparenright}\isanewline |
237 \isacommand{apply}\isamarkupfalse% |
237 \isamarkupfalse% |
238 {\isacharparenleft}subst\ lfp{\isacharunderscore}unfold{\isacharbrackleft}OF\ mono{\isacharunderscore}ef{\isacharbrackright}{\isacharparenright}\isanewline |
238 \isacommand{apply}{\isacharparenleft}blast{\isacharparenright}\isanewline |
239 \isacommand{apply}\isamarkupfalse% |
239 \isamarkupfalse% |
240 {\isacharparenleft}blast{\isacharparenright}\isanewline |
240 \isacommand{done}% |
241 \isacommand{done}\isamarkupfalse% |
241 \endisatagproof |
242 % |
242 {\isafoldproof}% |
243 \endisatagproof |
243 % |
244 {\isafoldproof}% |
244 \isadelimproof |
245 % |
245 % |
246 \isadelimproof |
246 \endisadelimproof |
247 % |
247 \isamarkuptrue% |
248 \endisadelimproof |
248 % |
249 % |
249 \begin{isamarkuptext}% |
250 \begin{isamarkuptext}% |
250 The main theorem is proved in the familiar manner: induction followed by |
251 The main theorem is proved in the familiar manner: induction followed by |
251 \isa{auto} augmented with the lemma as a simplification rule.% |
252 \isa{auto} augmented with the lemma as a simplification rule.% |
252 \end{isamarkuptext}% |
253 \end{isamarkuptext}% |
253 \isamarkupfalse% |
254 \isamarkuptrue% |
254 \isacommand{theorem}\ {\isachardoublequote}mc\ f\ {\isacharequal}\ {\isacharbraceleft}s{\isachardot}\ s\ {\isasymTurnstile}\ f{\isacharbraceright}{\isachardoublequote}\isanewline |
255 \isacommand{theorem}\isamarkupfalse% |
255 % |
256 \ {\isachardoublequoteopen}mc\ f\ {\isacharequal}\ {\isacharbraceleft}s{\isachardot}\ s\ {\isasymTurnstile}\ f{\isacharbraceright}{\isachardoublequoteclose}\isanewline |
256 \isadelimproof |
257 % |
257 % |
258 \isadelimproof |
258 \endisadelimproof |
259 % |
259 % |
260 \endisadelimproof |
260 \isatagproof |
261 % |
261 \isamarkupfalse% |
262 \isatagproof |
262 \isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ f{\isacharparenright}\isanewline |
263 \isacommand{apply}\isamarkupfalse% |
263 \isamarkupfalse% |
264 {\isacharparenleft}induct{\isacharunderscore}tac\ f{\isacharparenright}\isanewline |
264 \isacommand{apply}{\isacharparenleft}auto\ simp\ add{\isacharcolon}\ EF{\isacharunderscore}lemma{\isacharparenright}\isanewline |
265 \isacommand{apply}\isamarkupfalse% |
265 \isamarkupfalse% |
266 {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ EF{\isacharunderscore}lemma{\isacharparenright}\isanewline |
266 \isacommand{done}% |
267 \isacommand{done}\isamarkupfalse% |
267 \endisatagproof |
268 % |
268 {\isafoldproof}% |
269 \endisatagproof |
269 % |
270 {\isafoldproof}% |
270 \isadelimproof |
271 % |
271 % |
272 \isadelimproof |
272 \endisadelimproof |
273 % |
273 \isamarkuptrue% |
274 \endisadelimproof |
274 % |
275 % |
275 \begin{isamarkuptext}% |
276 \begin{isamarkuptext}% |
276 \begin{exercise} |
277 \begin{exercise} |
277 \isa{AX} has a dual operator \isa{EN} |
278 \isa{AX} has a dual operator \isa{EN} |
278 (``there exists a next state such that'')% |
279 (``there exists a next state such that'')% |