2022 |
2022 |
2023 To sum up this section, conversions are not as powerful as the simplifier |
2023 To sum up this section, conversions are not as powerful as the simplifier |
2024 and simprocs; the advantage of conversions, however, is that you never have |
2024 and simprocs; the advantage of conversions, however, is that you never have |
2025 to worry about non-termination. |
2025 to worry about non-termination. |
2026 |
2026 |
|
2027 (FIXME: explain @{ML Conv.try_conv}) |
|
2028 |
2027 \begin{exercise}\label{ex:addconversion} |
2029 \begin{exercise}\label{ex:addconversion} |
2028 Write a tactic that does the same as the simproc in exercise |
2030 Write a tactic that does the same as the simproc in exercise |
2029 \ref{ex:addsimproc}, but is based in conversions. That means replace terms |
2031 \ref{ex:addsimproc}, but is based in conversions. That means replace terms |
2030 of the form @{term "t\<^isub>1 + t\<^isub>2"} by their result. You can make |
2032 of the form @{term "t\<^isub>1 + t\<^isub>2"} by their result. You can make |
2031 the same assumptions as in \ref{ex:addsimproc}. FIXME: the current solution |
2033 the same assumptions as in \ref{ex:addsimproc}. |
2032 requires some additional functions. |
|
2033 \end{exercise} |
2034 \end{exercise} |
2034 |
2035 |
2035 \begin{exercise} |
2036 \begin{exercise} |
2036 Compare which way (either Exercise ~\ref{addsimproc} or \ref{ex:addconversion}) of |
2037 Compare which way (either Exercise ~\ref{addsimproc} or \ref{ex:addconversion}) of |
2037 rewriting such terms is faster. For this you might have to construct quite |
2038 rewriting such terms is faster. For this you might have to construct quite |