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}\ {\isacharparenleft}x{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\isactrlsup {\isacharasterisk}\ {\isasymLongrightarrow}\ t\ {\isasymin}\ A\ {\isasymLongrightarrow}\ x\ {\isasymin}\ lfp\ {\isacharparenleft}{\isasymlambda}T{\isachardot}\ A\ {\isasymunion}\ M{\isasyminverse}\ {\isacharcircum}{\isacharcircum}\ 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}\ {\isacharcircum}{\isacharcircum}\ 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 |
136 \isa{converse{\isacharunderscore}rtrancl{\isacharunderscore}induct} already exists: |
136 \isa{converse{\isacharunderscore}rtrancl{\isacharunderscore}induct} already exists: |
137 \begin{isabelle}% |
137 \begin{isabelle}% |
138 \ \ \ \ \ {\isacharparenleft}a{\isacharcomma}\ b{\isacharparenright}\ {\isasymin}\ r\isactrlsup {\isacharasterisk}\ {\isasymLongrightarrow}\isanewline |
138 \ \ \ \ \ {\isasymlbrakk}{\isacharparenleft}a{\isacharcomma}\ b{\isacharparenright}\ {\isasymin}\ r\isactrlsup {\isacharasterisk}{\isacharsemicolon}\ P\ b{\isacharsemicolon}\isanewline |
139 \ \ \ \ \ P\ b\ {\isasymLongrightarrow}\isanewline |
139 \ \ \ \ \ \ \ \ {\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 |
140 \ \ \ \ \ {\isacharparenleft}{\isasymAnd}y\ z{\isachardot}\ {\isacharparenleft}y{\isacharcomma}\ z{\isacharparenright}\ {\isasymin}\ r\ {\isasymLongrightarrow}\ {\isacharparenleft}z{\isacharcomma}\ b{\isacharparenright}\ {\isasymin}\ r\isactrlsup {\isacharasterisk}\ {\isasymLongrightarrow}\ P\ z\ {\isasymLongrightarrow}\ P\ y{\isacharparenright}\ {\isasymLongrightarrow}\ P\ a% |
140 \ \ \ \ \ {\isasymLongrightarrow}\ P\ a% |
141 \end{isabelle} |
141 \end{isabelle} |
142 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 It says that if \isa{{\isacharparenleft}a{\isacharcomma}\ b{\isacharparenright}\ {\isasymin}\ r\isactrlsup {\isacharasterisk}} and we know \isa{P\ b} then we can infer |
143 \isa{P\ a} provided each step backwards from a predecessor \isa{z} of |
143 \isa{P\ a} provided each step backwards from a predecessor \isa{z} of |
144 \isa{b} preserves \isa{P}.% |
144 \isa{b} preserves \isa{P}.% |
145 \end{isamarkuptxt}% |
145 \end{isamarkuptxt}% |