23 called \isa{formula{\isachardot}Atom}. |
23 called \isa{formula{\isachardot}Atom}. |
24 |
24 |
25 The meaning of these formulae is given by saying which formula is true in |
25 The meaning of these formulae is given by saying which formula is true in |
26 which state:% |
26 which state:% |
27 \end{isamarkuptext}% |
27 \end{isamarkuptext}% |
28 \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}% |
28 \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}% |
29 \begin{isamarkuptext}% |
29 \begin{isamarkuptext}% |
30 \noindent |
30 \noindent |
31 The concrete syntax annotation allows us to write \isa{s\ {\isasymTurnstile}\ f} instead of |
31 The concrete syntax annotation allows us to write \isa{s\ {\isasymTurnstile}\ f} instead of |
32 \isa{valid\ s\ f}. |
32 \isa{valid\ s\ f}. |
33 |
33 |
55 \isacommand{primrec}\isanewline |
55 \isacommand{primrec}\isanewline |
56 {\isachardoublequote}mc{\isacharparenleft}Atom\ a{\isacharparenright}\ \ {\isacharequal}\ {\isacharbraceleft}s{\isachardot}\ a\ {\isasymin}\ L\ s{\isacharbraceright}{\isachardoublequote}\isanewline |
56 {\isachardoublequote}mc{\isacharparenleft}Atom\ a{\isacharparenright}\ \ {\isacharequal}\ {\isacharbraceleft}s{\isachardot}\ a\ {\isasymin}\ L\ s{\isacharbraceright}{\isachardoublequote}\isanewline |
57 {\isachardoublequote}mc{\isacharparenleft}Neg\ f{\isacharparenright}\ \ \ {\isacharequal}\ {\isacharminus}mc\ f{\isachardoublequote}\isanewline |
57 {\isachardoublequote}mc{\isacharparenleft}Neg\ f{\isacharparenright}\ \ \ {\isacharequal}\ {\isacharminus}mc\ f{\isachardoublequote}\isanewline |
58 {\isachardoublequote}mc{\isacharparenleft}And\ f\ g{\isacharparenright}\ {\isacharequal}\ mc\ f\ {\isasyminter}\ mc\ g{\isachardoublequote}\isanewline |
58 {\isachardoublequote}mc{\isacharparenleft}And\ f\ g{\isacharparenright}\ {\isacharequal}\ mc\ f\ {\isasyminter}\ mc\ g{\isachardoublequote}\isanewline |
59 {\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 |
59 {\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 |
60 {\isachardoublequote}mc{\isacharparenleft}EF\ f{\isacharparenright}\ \ \ \ {\isacharequal}\ lfp{\isacharparenleft}{\isasymlambda}T{\isachardot}\ mc\ f\ {\isasymunion}\ M{\isacharcircum}{\isacharminus}\isadigit{1}\ {\isacharcircum}{\isacharcircum}\ T{\isacharparenright}{\isachardoublequote}% |
60 {\isachardoublequote}mc{\isacharparenleft}EF\ f{\isacharparenright}\ \ \ \ {\isacharequal}\ lfp{\isacharparenleft}{\isasymlambda}T{\isachardot}\ mc\ f\ {\isasymunion}\ M{\isacharcircum}{\isacharminus}{\isadigit{1}}\ {\isacharcircum}{\isacharcircum}\ T{\isacharparenright}{\isachardoublequote}% |
61 \begin{isamarkuptext}% |
61 \begin{isamarkuptext}% |
62 \noindent |
62 \noindent |
63 Only the equation for \isa{EF} deserves some comments. Remember that the |
63 Only the equation for \isa{EF} deserves some comments. Remember that the |
64 postfix \isa{{\isacharcircum}{\isacharminus}\isadigit{1}} and the infix \isa{{\isacharcircum}{\isacharcircum}} are predefined and denote the |
64 postfix \isa{{\isacharcircum}{\isacharminus}{\isadigit{1}}} and the infix \isa{{\isacharcircum}{\isacharcircum}} are predefined and denote the |
65 converse of a relation and the application of a relation to a set. Thus |
65 converse of a relation and the application of a relation to a set. Thus |
66 \isa{M{\isacharcircum}{\isacharminus}\isadigit{1}\ {\isacharcircum}{\isacharcircum}\ T} is the set of all predecessors of \isa{T} and the least |
66 \isa{M{\isacharcircum}{\isacharminus}{\isadigit{1}}\ {\isacharcircum}{\isacharcircum}\ T} is the set of all predecessors of \isa{T} and the least |
67 fixpoint (\isa{lfp}) of \isa{{\isasymlambda}T{\isachardot}\ mc\ f\ {\isasymunion}\ M{\isacharcircum}{\isacharminus}\isadigit{1}\ {\isacharcircum}{\isacharcircum}\ T} is the least set |
67 fixpoint (\isa{lfp}) of \isa{{\isasymlambda}T{\isachardot}\ mc\ f\ {\isasymunion}\ M{\isacharcircum}{\isacharminus}{\isadigit{1}}\ {\isacharcircum}{\isacharcircum}\ T} is the least set |
68 \isa{T} containing \isa{mc\ f} and all predecessors of \isa{T}. If you |
68 \isa{T} containing \isa{mc\ f} and all predecessors of \isa{T}. If you |
69 find it hard to see that \isa{mc\ {\isacharparenleft}EF\ f{\isacharparenright}} contains exactly those states from |
69 find it hard to see that \isa{mc\ {\isacharparenleft}EF\ f{\isacharparenright}} contains exactly those states from |
70 which there is a path to a state where \isa{f} is true, do not worry---that |
70 which there is a path to a state where \isa{f} is true, do not worry---that |
71 will be proved in a moment. |
71 will be proved in a moment. |
72 |
72 |
73 First we prove monotonicity of the function inside \isa{lfp}% |
73 First we prove monotonicity of the function inside \isa{lfp}% |
74 \end{isamarkuptext}% |
74 \end{isamarkuptext}% |
75 \isacommand{lemma}\ mono{\isacharunderscore}ef{\isacharcolon}\ {\isachardoublequote}mono{\isacharparenleft}{\isasymlambda}T{\isachardot}\ A\ {\isasymunion}\ M{\isacharcircum}{\isacharminus}\isadigit{1}\ {\isacharcircum}{\isacharcircum}\ T{\isacharparenright}{\isachardoublequote}\isanewline |
75 \isacommand{lemma}\ mono{\isacharunderscore}ef{\isacharcolon}\ {\isachardoublequote}mono{\isacharparenleft}{\isasymlambda}T{\isachardot}\ A\ {\isasymunion}\ M{\isacharcircum}{\isacharminus}{\isadigit{1}}\ {\isacharcircum}{\isacharcircum}\ T{\isacharparenright}{\isachardoublequote}\isanewline |
76 \isacommand{apply}{\isacharparenleft}rule\ monoI{\isacharparenright}\isanewline |
76 \isacommand{apply}{\isacharparenleft}rule\ monoI{\isacharparenright}\isanewline |
77 \isacommand{apply}\ blast\isanewline |
77 \isacommand{apply}\ blast\isanewline |
78 \isacommand{done}% |
78 \isacommand{done}% |
79 \begin{isamarkuptext}% |
79 \begin{isamarkuptext}% |
80 \noindent |
80 \noindent |
82 |
82 |
83 Now we can relate model checking and semantics. For the \isa{EF} case we need |
83 Now we can relate model checking and semantics. For the \isa{EF} case we need |
84 a separate lemma:% |
84 a separate lemma:% |
85 \end{isamarkuptext}% |
85 \end{isamarkuptext}% |
86 \isacommand{lemma}\ EF{\isacharunderscore}lemma{\isacharcolon}\isanewline |
86 \isacommand{lemma}\ EF{\isacharunderscore}lemma{\isacharcolon}\isanewline |
87 \ \ {\isachardoublequote}lfp{\isacharparenleft}{\isasymlambda}T{\isachardot}\ A\ {\isasymunion}\ M{\isacharcircum}{\isacharminus}\isadigit{1}\ {\isacharcircum}{\isacharcircum}\ T{\isacharparenright}\ {\isacharequal}\ {\isacharbraceleft}s{\isachardot}\ {\isasymexists}t{\isachardot}\ {\isacharparenleft}s{\isacharcomma}t{\isacharparenright}\ {\isasymin}\ M{\isacharcircum}{\isacharasterisk}\ {\isasymand}\ t\ {\isasymin}\ A{\isacharbraceright}{\isachardoublequote}% |
87 \ \ {\isachardoublequote}lfp{\isacharparenleft}{\isasymlambda}T{\isachardot}\ A\ {\isasymunion}\ M{\isacharcircum}{\isacharminus}{\isadigit{1}}\ {\isacharcircum}{\isacharcircum}\ T{\isacharparenright}\ {\isacharequal}\ {\isacharbraceleft}s{\isachardot}\ {\isasymexists}t{\isachardot}\ {\isacharparenleft}s{\isacharcomma}t{\isacharparenright}\ {\isasymin}\ M{\isacharcircum}{\isacharasterisk}\ {\isasymand}\ t\ {\isasymin}\ A{\isacharbraceright}{\isachardoublequote}% |
88 \begin{isamarkuptxt}% |
88 \begin{isamarkuptxt}% |
89 \noindent |
89 \noindent |
90 The equality is proved in the canonical fashion by proving that each set |
90 The equality is proved in the canonical fashion by proving that each set |
91 contains the other; the containment is shown pointwise:% |
91 contains the other; the containment is shown pointwise:% |
92 \end{isamarkuptxt}% |
92 \end{isamarkuptxt}% |