equal
deleted
inserted
replaced
142 usually known as mathematical induction. There is also \textbf{complete} |
142 usually known as mathematical induction. There is also \textbf{complete} |
143 \index{induction!complete}% |
143 \index{induction!complete}% |
144 induction, where you prove $P(n)$ under the assumption that $P(m)$ |
144 induction, where you prove $P(n)$ under the assumption that $P(m)$ |
145 holds for all $m<n$. In Isabelle, this is the theorem \tdx{nat_less_induct}: |
145 holds for all $m<n$. In Isabelle, this is the theorem \tdx{nat_less_induct}: |
146 \begin{isabelle}% |
146 \begin{isabelle}% |
147 \ \ \ \ \ {\isacharparenleft}{\isasymAnd}n{\isachardot}\ {\isasymforall}m{\isachardot}\ m\ {\isacharless}\ n\ {\isasymlongrightarrow}\ P\ m\ {\isasymLongrightarrow}\ P\ n{\isacharparenright}\ {\isasymLongrightarrow}\ P\ n% |
147 \ \ \ \ \ {\isacharparenleft}{\isasymAnd}n{\isachardot}\ {\isasymforall}m{\isacharless}n{\isachardot}\ P\ m\ {\isasymLongrightarrow}\ P\ n{\isacharparenright}\ {\isasymLongrightarrow}\ P\ n% |
148 \end{isabelle} |
148 \end{isabelle} |
149 As an application, we prove a property of the following |
149 As an application, we prove a property of the following |
150 function:% |
150 function:% |
151 \end{isamarkuptext}% |
151 \end{isamarkuptext}% |
152 \isamarkuptrue% |
152 \isamarkuptrue% |
182 % |
182 % |
183 \begin{isamarkuptxt}% |
183 \begin{isamarkuptxt}% |
184 \noindent |
184 \noindent |
185 We get the following proof state: |
185 We get the following proof state: |
186 \begin{isabelle}% |
186 \begin{isabelle}% |
187 \ {\isadigit{1}}{\isachardot}\ {\isasymAnd}n{\isachardot}\ {\isasymforall}m{\isachardot}\ m\ {\isacharless}\ n\ {\isasymlongrightarrow}\ {\isacharparenleft}{\isasymforall}i{\isachardot}\ m\ {\isacharequal}\ f\ i\ {\isasymlongrightarrow}\ i\ {\isasymle}\ f\ i{\isacharparenright}\ {\isasymLongrightarrow}\isanewline |
187 \ {\isadigit{1}}{\isachardot}\ {\isasymAnd}n{\isachardot}\ {\isasymforall}m{\isacharless}n{\isachardot}\ {\isasymforall}i{\isachardot}\ m\ {\isacharequal}\ f\ i\ {\isasymlongrightarrow}\ i\ {\isasymle}\ f\ i\ {\isasymLongrightarrow}\ {\isasymforall}i{\isachardot}\ n\ {\isacharequal}\ f\ i\ {\isasymlongrightarrow}\ i\ {\isasymle}\ f\ i% |
188 \isaindent{\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}n{\isachardot}\ }{\isasymforall}i{\isachardot}\ n\ {\isacharequal}\ f\ i\ {\isasymlongrightarrow}\ i\ {\isasymle}\ f\ i% |
|
189 \end{isabelle} |
188 \end{isabelle} |
190 After stripping the \isa{{\isasymforall}i}, the proof continues with a case |
189 After stripping the \isa{{\isasymforall}i}, the proof continues with a case |
191 distinction on \isa{i}. The case \isa{i\ {\isacharequal}\ {\isadigit{0}}} is trivial and we focus on |
190 distinction on \isa{i}. The case \isa{i\ {\isacharequal}\ {\isadigit{0}}} is trivial and we focus on |
192 the other case:% |
191 the other case:% |
193 \end{isamarkuptxt}% |
192 \end{isamarkuptxt}% |
199 \isacommand{apply}{\isacharparenleft}simp{\isacharparenright}\isamarkupfalse% |
198 \isacommand{apply}{\isacharparenleft}simp{\isacharparenright}\isamarkupfalse% |
200 % |
199 % |
201 \begin{isamarkuptxt}% |
200 \begin{isamarkuptxt}% |
202 \begin{isabelle}% |
201 \begin{isabelle}% |
203 \ {\isadigit{1}}{\isachardot}\ {\isasymAnd}n\ i\ nat{\isachardot}\isanewline |
202 \ {\isadigit{1}}{\isachardot}\ {\isasymAnd}n\ i\ nat{\isachardot}\isanewline |
204 \isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ }{\isasymlbrakk}{\isasymforall}m{\isachardot}\ m\ {\isacharless}\ n\ {\isasymlongrightarrow}\ {\isacharparenleft}{\isasymforall}i{\isachardot}\ m\ {\isacharequal}\ f\ i\ {\isasymlongrightarrow}\ i\ {\isasymle}\ f\ i{\isacharparenright}{\isacharsemicolon}\ i\ {\isacharequal}\ Suc\ nat{\isasymrbrakk}\isanewline |
203 \isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ }{\isasymlbrakk}{\isasymforall}m{\isacharless}n{\isachardot}\ {\isasymforall}i{\isachardot}\ m\ {\isacharequal}\ f\ i\ {\isasymlongrightarrow}\ i\ {\isasymle}\ f\ i{\isacharsemicolon}\ i\ {\isacharequal}\ Suc\ nat{\isasymrbrakk}\ {\isasymLongrightarrow}\ n\ {\isacharequal}\ f\ i\ {\isasymlongrightarrow}\ i\ {\isasymle}\ f\ i% |
205 \isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ }{\isasymLongrightarrow}\ n\ {\isacharequal}\ f\ i\ {\isasymlongrightarrow}\ i\ {\isasymle}\ f\ i% |
|
206 \end{isabelle}% |
204 \end{isabelle}% |
207 \end{isamarkuptxt}% |
205 \end{isamarkuptxt}% |
208 \isamarkuptrue% |
206 \isamarkuptrue% |
209 \isacommand{by}{\isacharparenleft}blast\ intro{\isacharbang}{\isacharcolon}\ f{\isacharunderscore}ax\ Suc{\isacharunderscore}leI\ intro{\isacharcolon}\ le{\isacharunderscore}less{\isacharunderscore}trans{\isacharparenright}\isamarkupfalse% |
207 \isacommand{by}{\isacharparenleft}blast\ intro{\isacharbang}{\isacharcolon}\ f{\isacharunderscore}ax\ Suc{\isacharunderscore}leI\ intro{\isacharcolon}\ le{\isacharunderscore}less{\isacharunderscore}trans{\isacharparenright}\isamarkupfalse% |
210 % |
208 % |