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{\isasyminverse}\ {\isacharcircum}{\isacharcircum}\ T} is the set of all predecessors of \isa{T} and the least |
67 fixed point (\isa{lfp}) of \isa{{\isasymlambda}T{\isachardot}\ mc\ f\ {\isasymunion}\ M{\isacharcircum}{\isacharminus}{\isadigit{1}}\ {\isacharcircum}{\isacharcircum}\ T} is the least set |
67 fixed point (\isa{lfp}) of \isa{{\isasymlambda}T{\isachardot}\ mc\ f\ {\isasymunion}\ M{\isasyminverse}\ {\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 |
126 \noindent |
126 \noindent |
127 After simplification and clarification we are left with |
127 After simplification and clarification we are left with |
128 \begin{isabelle} |
128 \begin{isabelle} |
129 \ \isadigit{1}{\isachardot}\ {\isasymAnd}s\ t{\isachardot}\ {\isasymlbrakk}{\isacharparenleft}s{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M{\isacharcircum}{\isacharasterisk}{\isacharsemicolon}\ t\ {\isasymin}\ A{\isasymrbrakk}\ {\isasymLongrightarrow}\ s\ {\isasymin}\ lfp\ {\isacharparenleft}{\isasymlambda}T{\isachardot}\ A\ {\isasymunion}\ M{\isacharcircum}{\isacharminus}\isadigit{1}\ {\isacharcircum}{\isacharcircum}\ T{\isacharparenright} |
129 \ \isadigit{1}{\isachardot}\ {\isasymAnd}s\ t{\isachardot}\ {\isasymlbrakk}{\isacharparenleft}s{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M{\isacharcircum}{\isacharasterisk}{\isacharsemicolon}\ t\ {\isasymin}\ A{\isasymrbrakk}\ {\isasymLongrightarrow}\ s\ {\isasymin}\ lfp\ {\isacharparenleft}{\isasymlambda}T{\isachardot}\ A\ {\isasymunion}\ M{\isacharcircum}{\isacharminus}\isadigit{1}\ {\isacharcircum}{\isacharcircum}\ T{\isacharparenright} |
130 \end{isabelle} |
130 \end{isabelle} |
131 This goal is proved by induction on \isa{{\isacharparenleft}s{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M{\isacharcircum}{\isacharasterisk}}. But since the model |
131 This goal is proved by induction on \isa{{\isacharparenleft}s{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\isactrlsup {\isacharasterisk}}. But since the model |
132 checker works backwards (from \isa{t} to \isa{s}), we cannot use the |
132 checker works backwards (from \isa{t} to \isa{s}), we cannot use the |
133 induction theorem \isa{rtrancl{\isacharunderscore}induct} because it works in the |
133 induction theorem \isa{rtrancl{\isacharunderscore}induct} because it works in the |
134 forward direction. Fortunately the converse induction theorem |
134 forward direction. Fortunately the converse induction theorem |
135 \isa{converse{\isacharunderscore}rtrancl{\isacharunderscore}induct} already exists: |
135 \isa{converse{\isacharunderscore}rtrancl{\isacharunderscore}induct} already exists: |
136 \begin{isabelle}% |
136 \begin{isabelle}% |
137 \ \ \ \ \ {\isasymlbrakk}{\isacharparenleft}a{\isacharcomma}\ b{\isacharparenright}\ {\isasymin}\ r{\isacharcircum}{\isacharasterisk}{\isacharsemicolon}\ P\ b{\isacharsemicolon}\isanewline |
137 \ \ \ \ \ {\isasymlbrakk}{\isacharparenleft}a{\isacharcomma}\ b{\isacharparenright}\ {\isasymin}\ r\isactrlsup {\isacharasterisk}{\isacharsemicolon}\ P\ b{\isacharsemicolon}\isanewline |
138 \ \ \ \ \ \ \ \ {\isasymAnd}y\ z{\isachardot}\ {\isasymlbrakk}{\isacharparenleft}y{\isacharcomma}\ z{\isacharparenright}\ {\isasymin}\ r{\isacharsemicolon}\ {\isacharparenleft}z{\isacharcomma}\ b{\isacharparenright}\ {\isasymin}\ r{\isacharcircum}{\isacharasterisk}{\isacharsemicolon}\ P\ z{\isasymrbrakk}\ {\isasymLongrightarrow}\ P\ y{\isasymrbrakk}\isanewline |
138 \ \ \ \ \ \ \ \ {\isasymAnd}y\ z{\isachardot}\ {\isasymlbrakk}{\isacharparenleft}y{\isacharcomma}\ z{\isacharparenright}\ {\isasymin}\ r{\isacharsemicolon}\ {\isacharparenleft}z{\isacharcomma}\ b{\isacharparenright}\ {\isasymin}\ r\isactrlsup {\isacharasterisk}{\isacharsemicolon}\ P\ z{\isasymrbrakk}\ {\isasymLongrightarrow}\ P\ y{\isasymrbrakk}\isanewline |
139 \ \ \ \ \ {\isasymLongrightarrow}\ P\ a% |
139 \ \ \ \ \ {\isasymLongrightarrow}\ P\ a% |
140 \end{isabelle} |
140 \end{isabelle} |
141 It says that if \isa{{\isacharparenleft}a{\isacharcomma}\ b{\isacharparenright}\ {\isasymin}\ r{\isacharcircum}{\isacharasterisk}} and we know \isa{P\ b} then we can infer |
141 It says that if \isa{{\isacharparenleft}a{\isacharcomma}\ b{\isacharparenright}\ {\isasymin}\ r\isactrlsup {\isacharasterisk}} and we know \isa{P\ b} then we can infer |
142 \isa{P\ a} provided each step backwards from a predecessor \isa{z} of |
142 \isa{P\ a} provided each step backwards from a predecessor \isa{z} of |
143 \isa{b} preserves \isa{P}.% |
143 \isa{b} preserves \isa{P}.% |
144 \end{isamarkuptxt}% |
144 \end{isamarkuptxt}% |
145 \isacommand{apply}{\isacharparenleft}erule\ converse{\isacharunderscore}rtrancl{\isacharunderscore}induct{\isacharparenright}% |
145 \isacommand{apply}{\isacharparenleft}erule\ converse{\isacharunderscore}rtrancl{\isacharunderscore}induct{\isacharparenright}% |
146 \begin{isamarkuptxt}% |
146 \begin{isamarkuptxt}% |