doc-src/TutorialI/Misc/let_rewr.thy

*** empty log message ***

(*<*)
theory let_rewr = Main:;
(*>*)

subsubsection{*Simplifying let-expressions*}

text{*\index{simplification!of let-expressions}
Proving a goal containing \isaindex{let}-expressions almost invariably
requires the @{text"let"}-con\-structs to be expanded at some point. Since
@{text"let"}-@{text"in"} is just syntactic sugar for a predefined constant
(called @{term"Let"}), expanding @{text"let"}-constructs means rewriting with
@{thm[source]Let_def}:
*}

lemma "(let xs = [] in xs@ys@xs) = ys";
by(simp add: Let_def);

text{*
If, in a particular context, there is no danger of a combinatorial explosion
of nested @{text"let"}s one could even add @{thm[source]Let_def} permanently:
*}
lemmas [simp] = Let_def;
(*<*)
end
(*>*)