equal
deleted
inserted
replaced
1 (*<*) |
|
2 theory let_rewr = Main:; |
|
3 (*>*) |
|
4 |
|
5 subsubsection{*Simplifying let-expressions*} |
|
6 |
|
7 text{*\index{simplification!of let-expressions} |
|
8 Proving a goal containing \isaindex{let}-expressions almost invariably |
|
9 requires the @{text"let"}-con\-structs to be expanded at some point. Since |
|
10 @{text"let"}-@{text"in"} is just syntactic sugar for a predefined constant |
|
11 (called @{term"Let"}), expanding @{text"let"}-constructs means rewriting with |
|
12 @{thm[source]Let_def}: |
|
13 *} |
|
14 |
|
15 lemma "(let xs = [] in xs@ys@xs) = ys"; |
|
16 by(simp add: Let_def); |
|
17 |
|
18 text{* |
|
19 If, in a particular context, there is no danger of a combinatorial explosion |
|
20 of nested @{text"let"}s one could even add @{thm[source]Let_def} permanently: |
|
21 *} |
|
22 lemmas [simp] = Let_def; |
|
23 (*<*) |
|
24 end |
|
25 (*>*) |
|