equal
deleted
inserted
replaced
1 % |
|
2 \begin{isabellebody}% |
|
3 % |
|
4 \isamarkupsubsubsection{Simplifying let-expressions} |
|
5 % |
|
6 \begin{isamarkuptext}% |
|
7 \index{simplification!of let-expressions} |
|
8 Proving a goal containing \isaindex{let}-expressions almost invariably |
|
9 requires the \isa{let}-con\-structs to be expanded at some point. Since |
|
10 \isa{let}-\isa{in} is just syntactic sugar for a predefined constant |
|
11 (called \isa{Let}), expanding \isa{let}-constructs means rewriting with |
|
12 \isa{Let{\isacharunderscore}def}:% |
|
13 \end{isamarkuptext}% |
|
14 \isacommand{lemma}\ {\isachardoublequote}{\isacharparenleft}let\ xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ in\ xs{\isacharat}ys{\isacharat}xs{\isacharparenright}\ {\isacharequal}\ ys{\isachardoublequote}\isanewline |
|
15 \isacommand{by}{\isacharparenleft}simp\ add{\isacharcolon}\ Let{\isacharunderscore}def{\isacharparenright}% |
|
16 \begin{isamarkuptext}% |
|
17 If, in a particular context, there is no danger of a combinatorial explosion |
|
18 of nested \isa{let}s one could even add \isa{Let{\isacharunderscore}def} permanently:% |
|
19 \end{isamarkuptext}% |
|
20 \isacommand{lemmas}\ {\isacharbrackleft}simp{\isacharbrackright}\ {\isacharequal}\ Let{\isacharunderscore}def\end{isabellebody}% |
|
21 %%% Local Variables: |
|
22 %%% mode: latex |
|
23 %%% TeX-master: "root" |
|
24 %%% End: |
|