equal
deleted
inserted
replaced
1 (*<*) |
1 (*<*) |
2 theory let_rewr = Main:; |
2 theory let_rewr = Main:; |
3 (*>*) |
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 |
4 lemma "(let xs = [] in xs@ys@xs) = ys"; |
15 lemma "(let xs = [] in xs@ys@xs) = ys"; |
5 by(simp add: Let_def); |
16 by(simp add: Let_def); |
6 |
17 |
7 text{* |
18 text{* |
8 If, in a particular context, there is no danger of a combinatorial explosion |
19 If, in a particular context, there is no danger of a combinatorial explosion |
9 of nested \isa{let}s one could even add \isa{Let_def} permanently: |
20 of nested @{text"let"}s one could even add @{thm[source]Let_def} permanently: |
10 *} |
21 *} |
11 lemmas [simp] = Let_def; |
22 lemmas [simp] = Let_def; |
12 (*<*) |
23 (*<*) |
13 end |
24 end |
14 (*>*) |
25 (*>*) |