56 \isacommand{primrec}\isanewline |
56 \isacommand{primrec}\isanewline |
57 {\isachardoublequote}mc{\isacharparenleft}Atom\ a{\isacharparenright}\ \ {\isacharequal}\ {\isacharbraceleft}s{\isachardot}\ a\ {\isasymin}\ L\ s{\isacharbraceright}{\isachardoublequote}\isanewline |
57 {\isachardoublequote}mc{\isacharparenleft}Atom\ a{\isacharparenright}\ \ {\isacharequal}\ {\isacharbraceleft}s{\isachardot}\ a\ {\isasymin}\ L\ s{\isacharbraceright}{\isachardoublequote}\isanewline |
58 {\isachardoublequote}mc{\isacharparenleft}Neg\ f{\isacharparenright}\ \ \ {\isacharequal}\ {\isacharminus}mc\ f{\isachardoublequote}\isanewline |
58 {\isachardoublequote}mc{\isacharparenleft}Neg\ f{\isacharparenright}\ \ \ {\isacharequal}\ {\isacharminus}mc\ f{\isachardoublequote}\isanewline |
59 {\isachardoublequote}mc{\isacharparenleft}And\ f\ g{\isacharparenright}\ {\isacharequal}\ mc\ f\ {\isasyminter}\ mc\ g{\isachardoublequote}\isanewline |
59 {\isachardoublequote}mc{\isacharparenleft}And\ f\ g{\isacharparenright}\ {\isacharequal}\ mc\ f\ {\isasyminter}\ mc\ g{\isachardoublequote}\isanewline |
60 {\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}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 |
61 {\isachardoublequote}mc{\isacharparenleft}EF\ f{\isacharparenright}\ \ \ \ {\isacharequal}\ lfp{\isacharparenleft}{\isasymlambda}T{\isachardot}\ mc\ f\ {\isasymunion}\ M{\isasyminverse}\ {\isacharbackquote}{\isacharbackquote}{\isacharbackquote}\ T{\isacharparenright}{\isachardoublequote}% |
61 {\isachardoublequote}mc{\isacharparenleft}EF\ f{\isacharparenright}\ \ \ \ {\isacharequal}\ lfp{\isacharparenleft}{\isasymlambda}T{\isachardot}\ mc\ f\ {\isasymunion}\ M{\isasyminverse}\ {\isacharbackquote}{\isacharbackquote}\ T{\isacharparenright}{\isachardoublequote}% |
62 \begin{isamarkuptext}% |
62 \begin{isamarkuptext}% |
63 \noindent |
63 \noindent |
64 Only the equation for \isa{EF} deserves some comments. Remember that the |
64 Only the equation for \isa{EF} deserves some comments. Remember that the |
65 postfix \isa{{\isasyminverse}} and the infix \isa{{\isacharbackquote}{\isacharbackquote}{\isacharbackquote}} are predefined and denote the |
65 postfix \isa{{\isasyminverse}} and the infix \isa{{\isacharbackquote}{\isacharbackquote}} are predefined and denote the |
66 converse of a relation and the application of a relation to a set. Thus |
66 converse of a relation and the application of a relation to a set. Thus |
67 \isa{M{\isasyminverse}\ {\isacharbackquote}{\isacharbackquote}{\isacharbackquote}\ T} is the set of all predecessors of \isa{T} and the least |
67 \isa{M{\isasyminverse}\ {\isacharbackquote}{\isacharbackquote}\ T} is the set of all predecessors of \isa{T} and the least |
68 fixed point (\isa{lfp}) of \isa{{\isasymlambda}T{\isachardot}\ mc\ f\ {\isasymunion}\ M{\isasyminverse}\ {\isacharbackquote}{\isacharbackquote}{\isacharbackquote}\ T} is the least set |
68 fixed point (\isa{lfp}) of \isa{{\isasymlambda}T{\isachardot}\ mc\ f\ {\isasymunion}\ M{\isasyminverse}\ {\isacharbackquote}{\isacharbackquote}\ T} is the least set |
69 \isa{T} containing \isa{mc\ f} and all predecessors of \isa{T}. If you |
69 \isa{T} containing \isa{mc\ f} and all predecessors of \isa{T}. If you |
70 find it hard to see that \isa{mc\ {\isacharparenleft}EF\ f{\isacharparenright}} contains exactly those states from |
70 find it hard to see that \isa{mc\ {\isacharparenleft}EF\ f{\isacharparenright}} contains exactly those states from |
71 which there is a path to a state where \isa{f} is true, do not worry---that |
71 which there is a path to a state where \isa{f} is true, do not worry---that |
72 will be proved in a moment. |
72 will be proved in a moment. |
73 |
73 |
74 First we prove monotonicity of the function inside \isa{lfp}% |
74 First we prove monotonicity of the function inside \isa{lfp}% |
75 \end{isamarkuptext}% |
75 \end{isamarkuptext}% |
76 \isacommand{lemma}\ mono{\isacharunderscore}ef{\isacharcolon}\ {\isachardoublequote}mono{\isacharparenleft}{\isasymlambda}T{\isachardot}\ A\ {\isasymunion}\ M{\isasyminverse}\ {\isacharbackquote}{\isacharbackquote}{\isacharbackquote}\ T{\isacharparenright}{\isachardoublequote}\isanewline |
76 \isacommand{lemma}\ mono{\isacharunderscore}ef{\isacharcolon}\ {\isachardoublequote}mono{\isacharparenleft}{\isasymlambda}T{\isachardot}\ A\ {\isasymunion}\ M{\isasyminverse}\ {\isacharbackquote}{\isacharbackquote}\ T{\isacharparenright}{\isachardoublequote}\isanewline |
77 \isacommand{apply}{\isacharparenleft}rule\ monoI{\isacharparenright}\isanewline |
77 \isacommand{apply}{\isacharparenleft}rule\ monoI{\isacharparenright}\isanewline |
78 \isacommand{apply}\ blast\isanewline |
78 \isacommand{apply}\ blast\isanewline |
79 \isacommand{done}% |
79 \isacommand{done}% |
80 \begin{isamarkuptext}% |
80 \begin{isamarkuptext}% |
81 \noindent |
81 \noindent |
83 |
83 |
84 Now we can relate model checking and semantics. For the \isa{EF} case we need |
84 Now we can relate model checking and semantics. For the \isa{EF} case we need |
85 a separate lemma:% |
85 a separate lemma:% |
86 \end{isamarkuptext}% |
86 \end{isamarkuptext}% |
87 \isacommand{lemma}\ EF{\isacharunderscore}lemma{\isacharcolon}\isanewline |
87 \isacommand{lemma}\ EF{\isacharunderscore}lemma{\isacharcolon}\isanewline |
88 \ \ {\isachardoublequote}lfp{\isacharparenleft}{\isasymlambda}T{\isachardot}\ A\ {\isasymunion}\ M{\isasyminverse}\ {\isacharbackquote}{\isacharbackquote}{\isacharbackquote}\ T{\isacharparenright}\ {\isacharequal}\ {\isacharbraceleft}s{\isachardot}\ {\isasymexists}t{\isachardot}\ {\isacharparenleft}s{\isacharcomma}t{\isacharparenright}\ {\isasymin}\ M\isactrlsup {\isacharasterisk}\ {\isasymand}\ t\ {\isasymin}\ A{\isacharbraceright}{\isachardoublequote}% |
88 \ \ {\isachardoublequote}lfp{\isacharparenleft}{\isasymlambda}T{\isachardot}\ A\ {\isasymunion}\ M{\isasyminverse}\ {\isacharbackquote}{\isacharbackquote}\ T{\isacharparenright}\ {\isacharequal}\ {\isacharbraceleft}s{\isachardot}\ {\isasymexists}t{\isachardot}\ {\isacharparenleft}s{\isacharcomma}t{\isacharparenright}\ {\isasymin}\ M\isactrlsup {\isacharasterisk}\ {\isasymand}\ t\ {\isasymin}\ A{\isacharbraceright}{\isachardoublequote}% |
89 \begin{isamarkuptxt}% |
89 \begin{isamarkuptxt}% |
90 \noindent |
90 \noindent |
91 The equality is proved in the canonical fashion by proving that each set |
91 The equality is proved in the canonical fashion by proving that each set |
92 contains the other; the containment is shown pointwise:% |
92 contains the other; the containment is shown pointwise:% |
93 \end{isamarkuptxt}% |
93 \end{isamarkuptxt}% |
96 \ \isacommand{apply}{\isacharparenleft}simp{\isacharparenright}% |
96 \ \isacommand{apply}{\isacharparenleft}simp{\isacharparenright}% |
97 \begin{isamarkuptxt}% |
97 \begin{isamarkuptxt}% |
98 \noindent |
98 \noindent |
99 Simplification leaves us with the following first subgoal |
99 Simplification leaves us with the following first subgoal |
100 \begin{isabelle}% |
100 \begin{isabelle}% |
101 \ {\isadigit{1}}{\isachardot}\ {\isasymAnd}s{\isachardot}\ s\ {\isasymin}\ lfp\ {\isacharparenleft}{\isasymlambda}T{\isachardot}\ A\ {\isasymunion}\ M{\isasyminverse}\ {\isacharbackquote}{\isacharbackquote}{\isacharbackquote}\ T{\isacharparenright}\ {\isasymLongrightarrow}\ {\isasymexists}t{\isachardot}\ {\isacharparenleft}s{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\isactrlsup {\isacharasterisk}\ {\isasymand}\ t\ {\isasymin}\ A% |
101 \ {\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% |
102 \end{isabelle} |
102 \end{isabelle} |
103 which is proved by \isa{lfp}-induction:% |
103 which is proved by \isa{lfp}-induction:% |
104 \end{isamarkuptxt}% |
104 \end{isamarkuptxt}% |
105 \ \isacommand{apply}{\isacharparenleft}erule\ lfp{\isacharunderscore}induct{\isacharparenright}\isanewline |
105 \ \isacommand{apply}{\isacharparenleft}erule\ lfp{\isacharunderscore}induct{\isacharparenright}\isanewline |
106 \ \ \isacommand{apply}{\isacharparenleft}rule\ mono{\isacharunderscore}ef{\isacharparenright}\isanewline |
106 \ \ \isacommand{apply}{\isacharparenleft}rule\ mono{\isacharunderscore}ef{\isacharparenright}\isanewline |
125 \isacommand{apply}{\isacharparenleft}simp{\isacharcomma}\ clarify{\isacharparenright}% |
125 \isacommand{apply}{\isacharparenleft}simp{\isacharcomma}\ clarify{\isacharparenright}% |
126 \begin{isamarkuptxt}% |
126 \begin{isamarkuptxt}% |
127 \noindent |
127 \noindent |
128 After simplification and clarification we are left with |
128 After simplification and clarification we are left with |
129 \begin{isabelle}% |
129 \begin{isabelle}% |
130 \ {\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}{\isacharbackquote}\ T{\isacharparenright}% |
130 \ {\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}% |
131 \end{isabelle} |
131 \end{isabelle} |
132 This goal is proved by induction on \isa{{\isacharparenleft}s{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\isactrlsup {\isacharasterisk}}. But since the model |
132 This goal is proved by induction on \isa{{\isacharparenleft}s{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\isactrlsup {\isacharasterisk}}. But since the model |
133 checker works backwards (from \isa{t} to \isa{s}), we cannot use the |
133 checker works backwards (from \isa{t} to \isa{s}), we cannot use the |
134 induction theorem \isa{rtrancl{\isacharunderscore}induct} because it works in the |
134 induction theorem \isa{rtrancl{\isacharunderscore}induct} because it works in the |
135 forward direction. Fortunately the converse induction theorem |
135 forward direction. Fortunately the converse induction theorem |
146 \isacommand{apply}{\isacharparenleft}erule\ converse{\isacharunderscore}rtrancl{\isacharunderscore}induct{\isacharparenright}% |
146 \isacommand{apply}{\isacharparenleft}erule\ converse{\isacharunderscore}rtrancl{\isacharunderscore}induct{\isacharparenright}% |
147 \begin{isamarkuptxt}% |
147 \begin{isamarkuptxt}% |
148 \noindent |
148 \noindent |
149 The base case |
149 The base case |
150 \begin{isabelle}% |
150 \begin{isabelle}% |
151 \ {\isadigit{1}}{\isachardot}\ {\isasymAnd}x\ t{\isachardot}\ t\ {\isasymin}\ A\ {\isasymLongrightarrow}\ t\ {\isasymin}\ lfp\ {\isacharparenleft}{\isasymlambda}T{\isachardot}\ A\ {\isasymunion}\ M{\isasyminverse}\ {\isacharbackquote}{\isacharbackquote}{\isacharbackquote}\ T{\isacharparenright}% |
151 \ {\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}% |
152 \end{isabelle} |
152 \end{isabelle} |
153 is solved by unrolling \isa{lfp} once% |
153 is solved by unrolling \isa{lfp} once% |
154 \end{isamarkuptxt}% |
154 \end{isamarkuptxt}% |
155 \ \isacommand{apply}{\isacharparenleft}rule\ ssubst{\isacharbrackleft}OF\ lfp{\isacharunderscore}unfold{\isacharbrackleft}OF\ mono{\isacharunderscore}ef{\isacharbrackright}{\isacharbrackright}{\isacharparenright}% |
155 \ \isacommand{apply}{\isacharparenleft}rule\ ssubst{\isacharbrackleft}OF\ lfp{\isacharunderscore}unfold{\isacharbrackleft}OF\ mono{\isacharunderscore}ef{\isacharbrackright}{\isacharbrackright}{\isacharparenright}% |
156 \begin{isamarkuptxt}% |
156 \begin{isamarkuptxt}% |
157 \begin{isabelle}% |
157 \begin{isabelle}% |
158 \ {\isadigit{1}}{\isachardot}\ {\isasymAnd}x\ t{\isachardot}\ t\ {\isasymin}\ A\ {\isasymLongrightarrow}\ t\ {\isasymin}\ A\ {\isasymunion}\ M{\isasyminverse}\ {\isacharbackquote}{\isacharbackquote}{\isacharbackquote}\ lfp\ {\isacharparenleft}{\isasymlambda}T{\isachardot}\ A\ {\isasymunion}\ M{\isasyminverse}\ {\isacharbackquote}{\isacharbackquote}{\isacharbackquote}\ T{\isacharparenright}% |
158 \ {\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}% |
159 \end{isabelle} |
159 \end{isabelle} |
160 and disposing of the resulting trivial subgoal automatically:% |
160 and disposing of the resulting trivial subgoal automatically:% |
161 \end{isamarkuptxt}% |
161 \end{isamarkuptxt}% |
162 \ \isacommand{apply}{\isacharparenleft}blast{\isacharparenright}% |
162 \ \isacommand{apply}{\isacharparenleft}blast{\isacharparenright}% |
163 \begin{isamarkuptxt}% |
163 \begin{isamarkuptxt}% |