148 \end{isamarkuptext}% |
148 \end{isamarkuptext}% |
149 \isamarkuptrue% |
149 \isamarkuptrue% |
150 \isacommand{lemma}\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\isanewline |
150 \isacommand{lemma}\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\isanewline |
151 \ \ {\isachardoublequote}wf{\isacharparenleft}step{\isadigit{1}}\ f{\isacharparenright}\ {\isasymLongrightarrow}\ find{\isacharparenleft}f{\isacharcomma}x{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}if\ f\ x\ {\isacharequal}\ x\ then\ x\ else\ find{\isacharparenleft}f{\isacharcomma}\ f\ x{\isacharparenright}{\isacharparenright}{\isachardoublequote}\isanewline |
151 \ \ {\isachardoublequote}wf{\isacharparenleft}step{\isadigit{1}}\ f{\isacharparenright}\ {\isasymLongrightarrow}\ find{\isacharparenleft}f{\isacharcomma}x{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}if\ f\ x\ {\isacharequal}\ x\ then\ x\ else\ find{\isacharparenleft}f{\isacharcomma}\ f\ x{\isacharparenright}{\isacharparenright}{\isachardoublequote}\isanewline |
152 \isamarkupfalse% |
152 \isamarkupfalse% |
153 \isacommand{by}\ simp\isamarkupfalse% |
153 \isamarkupfalse% |
154 % |
154 % |
155 \begin{isamarkuptext}% |
155 \begin{isamarkuptext}% |
156 \noindent Then you should disable the original recursion equation:% |
156 \noindent Then you should disable the original recursion equation:% |
157 \end{isamarkuptext}% |
157 \end{isamarkuptext}% |
158 \isamarkuptrue% |
158 \isamarkuptrue% |
163 recursive functions. Here is a simple example of recursion induction:% |
163 recursive functions. Here is a simple example of recursion induction:% |
164 \end{isamarkuptext}% |
164 \end{isamarkuptext}% |
165 \isamarkuptrue% |
165 \isamarkuptrue% |
166 \isacommand{lemma}\ {\isachardoublequote}wf{\isacharparenleft}step{\isadigit{1}}\ f{\isacharparenright}\ {\isasymlongrightarrow}\ f{\isacharparenleft}find{\isacharparenleft}f{\isacharcomma}x{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ find{\isacharparenleft}f{\isacharcomma}x{\isacharparenright}{\isachardoublequote}\isanewline |
166 \isacommand{lemma}\ {\isachardoublequote}wf{\isacharparenleft}step{\isadigit{1}}\ f{\isacharparenright}\ {\isasymlongrightarrow}\ f{\isacharparenleft}find{\isacharparenleft}f{\isacharcomma}x{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ find{\isacharparenleft}f{\isacharcomma}x{\isacharparenright}{\isachardoublequote}\isanewline |
167 \isamarkupfalse% |
167 \isamarkupfalse% |
168 \isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ f\ x\ rule{\isacharcolon}\ find{\isachardot}induct{\isacharparenright}\isanewline |
168 \isamarkupfalse% |
169 \isamarkupfalse% |
169 \isamarkupfalse% |
170 \isacommand{apply}\ simp\isanewline |
170 \isamarkupfalse% |
171 \isamarkupfalse% |
|
172 \isacommand{done}\isamarkupfalse% |
|
173 % |
171 % |
174 \isamarkupsubsubsection{The {\tt\slshape while} Combinator% |
172 \isamarkupsubsubsection{The {\tt\slshape while} Combinator% |
175 } |
173 } |
176 \isamarkuptrue% |
174 \isamarkuptrue% |
177 % |
175 % |
229 \isamarkuptrue% |
227 \isamarkuptrue% |
230 \isacommand{lemma}\ lem{\isacharcolon}\ {\isachardoublequote}wf{\isacharparenleft}step{\isadigit{1}}\ f{\isacharparenright}\ {\isasymLongrightarrow}\isanewline |
228 \isacommand{lemma}\ lem{\isacharcolon}\ {\isachardoublequote}wf{\isacharparenleft}step{\isadigit{1}}\ f{\isacharparenright}\ {\isasymLongrightarrow}\isanewline |
231 \ \ {\isasymexists}y{\isachardot}\ while\ {\isacharparenleft}{\isasymlambda}{\isacharparenleft}x{\isacharcomma}x{\isacharprime}{\isacharparenright}{\isachardot}\ x{\isacharprime}\ {\isasymnoteq}\ x{\isacharparenright}\ {\isacharparenleft}{\isasymlambda}{\isacharparenleft}x{\isacharcomma}x{\isacharprime}{\isacharparenright}{\isachardot}\ {\isacharparenleft}x{\isacharprime}{\isacharcomma}f\ x{\isacharprime}{\isacharparenright}{\isacharparenright}\ {\isacharparenleft}x{\isacharcomma}f\ x{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}y{\isacharcomma}y{\isacharparenright}\ {\isasymand}\isanewline |
229 \ \ {\isasymexists}y{\isachardot}\ while\ {\isacharparenleft}{\isasymlambda}{\isacharparenleft}x{\isacharcomma}x{\isacharprime}{\isacharparenright}{\isachardot}\ x{\isacharprime}\ {\isasymnoteq}\ x{\isacharparenright}\ {\isacharparenleft}{\isasymlambda}{\isacharparenleft}x{\isacharcomma}x{\isacharprime}{\isacharparenright}{\isachardot}\ {\isacharparenleft}x{\isacharprime}{\isacharcomma}f\ x{\isacharprime}{\isacharparenright}{\isacharparenright}\ {\isacharparenleft}x{\isacharcomma}f\ x{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}y{\isacharcomma}y{\isacharparenright}\ {\isasymand}\isanewline |
232 \ \ \ \ \ \ \ f\ y\ {\isacharequal}\ y{\isachardoublequote}\isanewline |
230 \ \ \ \ \ \ \ f\ y\ {\isacharequal}\ y{\isachardoublequote}\isanewline |
233 \isamarkupfalse% |
231 \isamarkupfalse% |
234 \isacommand{apply}{\isacharparenleft}rule{\isacharunderscore}tac\ P\ {\isacharequal}\ {\isachardoublequote}{\isasymlambda}{\isacharparenleft}x{\isacharcomma}x{\isacharprime}{\isacharparenright}{\isachardot}\ x{\isacharprime}\ {\isacharequal}\ f\ x{\isachardoublequote}\ \isakeyword{and}\isanewline |
232 \isamarkupfalse% |
235 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ r\ {\isacharequal}\ {\isachardoublequote}inv{\isacharunderscore}image\ {\isacharparenleft}step{\isadigit{1}}\ f{\isacharparenright}\ fst{\isachardoublequote}\ \isakeyword{in}\ while{\isacharunderscore}rule{\isacharparenright}\isanewline |
233 \isamarkupfalse% |
236 \isamarkupfalse% |
234 \isamarkupfalse% |
237 \isacommand{apply}\ auto\isanewline |
235 \isamarkupfalse% |
238 \isamarkupfalse% |
|
239 \isacommand{apply}{\isacharparenleft}simp\ add{\isacharcolon}\ inv{\isacharunderscore}image{\isacharunderscore}def\ step{\isadigit{1}}{\isacharunderscore}def{\isacharparenright}\isanewline |
|
240 \isamarkupfalse% |
|
241 \isacommand{done}\isamarkupfalse% |
|
242 % |
236 % |
243 \begin{isamarkuptext}% |
237 \begin{isamarkuptext}% |
244 The theorem itself is a simple consequence of this lemma:% |
238 The theorem itself is a simple consequence of this lemma:% |
245 \end{isamarkuptext}% |
239 \end{isamarkuptext}% |
246 \isamarkuptrue% |
240 \isamarkuptrue% |
247 \isacommand{theorem}\ {\isachardoublequote}wf{\isacharparenleft}step{\isadigit{1}}\ f{\isacharparenright}\ {\isasymLongrightarrow}\ f{\isacharparenleft}find{\isadigit{2}}\ f\ x{\isacharparenright}\ {\isacharequal}\ find{\isadigit{2}}\ f\ x{\isachardoublequote}\isanewline |
241 \isacommand{theorem}\ {\isachardoublequote}wf{\isacharparenleft}step{\isadigit{1}}\ f{\isacharparenright}\ {\isasymLongrightarrow}\ f{\isacharparenleft}find{\isadigit{2}}\ f\ x{\isacharparenright}\ {\isacharequal}\ find{\isadigit{2}}\ f\ x{\isachardoublequote}\isanewline |
248 \isamarkupfalse% |
242 \isamarkupfalse% |
249 \isacommand{apply}{\isacharparenleft}drule{\isacharunderscore}tac\ x\ {\isacharequal}\ x\ \isakeyword{in}\ lem{\isacharparenright}\isanewline |
243 \isamarkupfalse% |
250 \isamarkupfalse% |
244 \isamarkupfalse% |
251 \isacommand{apply}{\isacharparenleft}auto\ simp\ add{\isacharcolon}\ find{\isadigit{2}}{\isacharunderscore}def{\isacharparenright}\isanewline |
245 \isamarkupfalse% |
252 \isamarkupfalse% |
|
253 \isacommand{done}\isamarkupfalse% |
|
254 % |
246 % |
255 \begin{isamarkuptext}% |
247 \begin{isamarkuptext}% |
256 Let us conclude this section on partial functions by a |
248 Let us conclude this section on partial functions by a |
257 discussion of the merits of the \isa{while} combinator. We have |
249 discussion of the merits of the \isa{while} combinator. We have |
258 already seen that the advantage of not having to |
250 already seen that the advantage of not having to |