172 termination rears its ugly head again. Here is |
172 termination rears its ugly head again. Here is |
173 \isa{while{\isacharunderscore}rule}, the well known proof rule for total |
173 \isa{while{\isacharunderscore}rule}, the well known proof rule for total |
174 correctness of loops expressed with \isa{while}: |
174 correctness of loops expressed with \isa{while}: |
175 \begin{isabelle}% |
175 \begin{isabelle}% |
176 \ \ \ \ \ {\isasymlbrakk}P\ s{\isacharsemicolon}\ {\isasymAnd}s{\isachardot}\ {\isasymlbrakk}P\ s{\isacharsemicolon}\ b\ s{\isasymrbrakk}\ {\isasymLongrightarrow}\ P\ {\isacharparenleft}c\ s{\isacharparenright}{\isacharsemicolon}\isanewline |
176 \ \ \ \ \ {\isasymlbrakk}P\ s{\isacharsemicolon}\ {\isasymAnd}s{\isachardot}\ {\isasymlbrakk}P\ s{\isacharsemicolon}\ b\ s{\isasymrbrakk}\ {\isasymLongrightarrow}\ P\ {\isacharparenleft}c\ s{\isacharparenright}{\isacharsemicolon}\isanewline |
177 \ \ \ \ \ \ \ \ {\isasymAnd}s{\isachardot}\ {\isasymlbrakk}P\ s{\isacharsemicolon}\ {\isasymnot}\ b\ s{\isasymrbrakk}\ {\isasymLongrightarrow}\ Q\ s{\isacharsemicolon}\ wf\ r{\isacharsemicolon}\isanewline |
177 \isaindent{\ \ \ \ \ \ \ \ }{\isasymAnd}s{\isachardot}\ {\isasymlbrakk}P\ s{\isacharsemicolon}\ {\isasymnot}\ b\ s{\isasymrbrakk}\ {\isasymLongrightarrow}\ Q\ s{\isacharsemicolon}\ wf\ r{\isacharsemicolon}\isanewline |
178 \ \ \ \ \ \ \ \ {\isasymAnd}s{\isachardot}\ {\isasymlbrakk}P\ s{\isacharsemicolon}\ b\ s{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharparenleft}c\ s{\isacharcomma}\ s{\isacharparenright}\ {\isasymin}\ r{\isasymrbrakk}\isanewline |
178 \isaindent{\ \ \ \ \ \ \ \ }{\isasymAnd}s{\isachardot}\ {\isasymlbrakk}P\ s{\isacharsemicolon}\ b\ s{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharparenleft}c\ s{\isacharcomma}\ s{\isacharparenright}\ {\isasymin}\ r{\isasymrbrakk}\isanewline |
179 \ \ \ \ \ {\isasymLongrightarrow}\ Q\ {\isacharparenleft}while\ b\ c\ s{\isacharparenright}% |
179 \isaindent{\ \ \ \ \ }{\isasymLongrightarrow}\ Q\ {\isacharparenleft}while\ b\ c\ s{\isacharparenright}% |
180 \end{isabelle} \isa{P} needs to be |
180 \end{isabelle} \isa{P} needs to be |
181 true of the initial state \isa{s} and invariant under \isa{c} |
181 true of the initial state \isa{s} and invariant under \isa{c} |
182 (premises 1 and~2). The post-condition \isa{Q} must become true when |
182 (premises 1 and~2). The post-condition \isa{Q} must become true when |
183 leaving the loop (premise~3). And each loop iteration must descend |
183 leaving the loop (premise~3). And each loop iteration must descend |
184 along a well-founded relation \isa{r} (premises 4 and~5). |
184 along a well-founded relation \isa{r} (premises 4 and~5). |