added Let_def
authornipkow
Fri Sep 07 13:27:41 2018 +0200 (9 months ago)
changeset 6892135ea237696cf
parent 68920 e50312982ba0
child 68932 e609c3dec6f8
added Let_def
src/Doc/Prog_Prove/Types_and_funs.thy
     1.1 --- a/src/Doc/Prog_Prove/Types_and_funs.thy	Thu Sep 06 16:50:16 2018 +0200
     1.2 +++ b/src/Doc/Prog_Prove/Types_and_funs.thy	Fri Sep 07 13:27:41 2018 +0200
     1.3 @@ -539,12 +539,16 @@
     1.4  @{text "split: if_splits"} or @{text "split: t.splits"}.
     1.5  
     1.6  \ifsem\else
     1.7 -\subsection{Converting Numerals to @{const Suc} Terms}
     1.8 +\subsection{Rewriting \<open>let\<close> and Numerals}
     1.9 +
    1.10 +Let-expressions (@{term "let x = s in t"}) can be expanded explicitly with the simplification rule
    1.11 +@{thm[source] Let_def}. The simplifier will not expand \<open>let\<close>s automatically in many cases.
    1.12  
    1.13 -Recursive functions on type @{typ nat} are often defined by pattern matching over @{text 0} and @{const Suc},
    1.14 -e.g. @{text "f 0 = ..."} and  @{text "f (Suc n) = ..."}. In order to simplify \<open>f 2\<close>, the \<open>2\<close>
    1.15 -needs to be converted to @{term "Suc(Suc 0)"} first. The simplification rule @{thm[source] numeral_eq_Suc}
    1.16 -converts all numerals to @{const Suc} terms.
    1.17 +Numerals of type @{typ nat} can be converted to @{const Suc} terms with the simplification rule
    1.18 +@{thm[source] numeral_eq_Suc}. This is required, for example, when a function that is defined
    1.19 +by pattern matching with @{const Suc} is applied to a numeral: if \<open>f\<close> is defined by
    1.20 +@{text "f 0 = ..."} and  @{text "f (Suc n) = ..."}, the simplifier cannot simplify \<open>f 2\<close> unless
    1.21 +\<open>2\<close> is converted to @{term "Suc(Suc 0)"} (via @{thm[source] numeral_eq_Suc}).
    1.22  \fi
    1.23  
    1.24  \subsection*{Exercises}