equal
deleted
inserted
replaced
165 induction theorem \isa{rtrancl{\isacharunderscore}induct}: it works in the |
165 induction theorem \isa{rtrancl{\isacharunderscore}induct}: it works in the |
166 forward direction. Fortunately the converse induction theorem |
166 forward direction. Fortunately the converse induction theorem |
167 \isa{converse{\isacharunderscore}rtrancl{\isacharunderscore}induct} already exists: |
167 \isa{converse{\isacharunderscore}rtrancl{\isacharunderscore}induct} already exists: |
168 \begin{isabelle}% |
168 \begin{isabelle}% |
169 \ \ \ \ \ {\isasymlbrakk}{\isacharparenleft}a{\isacharcomma}\ b{\isacharparenright}\ {\isasymin}\ r\isactrlsup {\isacharasterisk}{\isacharsemicolon}\ P\ b{\isacharsemicolon}\isanewline |
169 \ \ \ \ \ {\isasymlbrakk}{\isacharparenleft}a{\isacharcomma}\ b{\isacharparenright}\ {\isasymin}\ r\isactrlsup {\isacharasterisk}{\isacharsemicolon}\ P\ b{\isacharsemicolon}\isanewline |
170 \isaindent{\ \ \ \ \ \ \ \ }{\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 |
170 \isaindent{\ \ \ \ \ \ }{\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 |
171 \isaindent{\ \ \ \ \ }{\isasymLongrightarrow}\ P\ a% |
171 \isaindent{\ \ \ \ \ }{\isasymLongrightarrow}\ P\ a% |
172 \end{isabelle} |
172 \end{isabelle} |
173 It says that if \isa{{\isacharparenleft}a{\isacharcomma}\ b{\isacharparenright}\ {\isasymin}\ r\isactrlsup {\isacharasterisk}} and we know \isa{P\ b} then we can infer |
173 It says that if \isa{{\isacharparenleft}a{\isacharcomma}\ b{\isacharparenright}\ {\isasymin}\ r\isactrlsup {\isacharasterisk}} and we know \isa{P\ b} then we can infer |
174 \isa{P\ a} provided each step backwards from a predecessor \isa{z} of |
174 \isa{P\ a} provided each step backwards from a predecessor \isa{z} of |
175 \isa{b} preserves \isa{P}.% |
175 \isa{b} preserves \isa{P}.% |