equal
deleted
inserted
replaced
1 % |
1 % |
2 \begin{isabellebody}% |
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}% |
3 \isacommand{lemma}\ {\isachardoublequote}{\isacharparenleft}let\ xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ in\ xs{\isacharat}ys{\isacharat}xs{\isacharparenright}\ {\isacharequal}\ ys{\isachardoublequote}\isanewline |
14 \isacommand{lemma}\ {\isachardoublequote}{\isacharparenleft}let\ xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ in\ xs{\isacharat}ys{\isacharat}xs{\isacharparenright}\ {\isacharequal}\ ys{\isachardoublequote}\isanewline |
4 \isacommand{by}{\isacharparenleft}simp\ add{\isacharcolon}\ Let{\isacharunderscore}def{\isacharparenright}% |
15 \isacommand{by}{\isacharparenleft}simp\ add{\isacharcolon}\ Let{\isacharunderscore}def{\isacharparenright}% |
5 \begin{isamarkuptext}% |
16 \begin{isamarkuptext}% |
6 If, in a particular context, there is no danger of a combinatorial explosion |
17 If, in a particular context, there is no danger of a combinatorial explosion |
7 of nested \isa{let}s one could even add \isa{Let_def} permanently:% |
18 of nested \isa{let}s one could even add \isa{Let{\isacharunderscore}def} permanently:% |
8 \end{isamarkuptext}% |
19 \end{isamarkuptext}% |
9 \isacommand{lemmas}\ {\isacharbrackleft}simp{\isacharbrackright}\ {\isacharequal}\ Let{\isacharunderscore}def\end{isabellebody}% |
20 \isacommand{lemmas}\ {\isacharbrackleft}simp{\isacharbrackright}\ {\isacharequal}\ Let{\isacharunderscore}def\end{isabellebody}% |
10 %%% Local Variables: |
21 %%% Local Variables: |
11 %%% mode: latex |
22 %%% mode: latex |
12 %%% TeX-master: "root" |
23 %%% TeX-master: "root" |