# HG changeset patch
# User nipkow
# Date 1194524643 -3600
# Node ID 68577e621ea87c4076d62bc18eeb9f48feb623c5
# Parent  ca3761e38a8706ad18ce5fc36d60fec388507639
added evaluation

diff -r ca3761e38a87 -r 68577e621ea8 doc-src/TutorialI/ToyList/ToyList.thy
--- a/doc-src/TutorialI/ToyList/ToyList.thy	Thu Nov 08 13:23:47 2007 +0100
+++ b/doc-src/TutorialI/ToyList/ToyList.thy	Thu Nov 08 13:24:03 2007 +0100
@@ -113,12 +113,41 @@
 When Isabelle prints a syntax error message, it refers to the HOL syntax as
 the \textbf{inner syntax} and the enclosing theory language as the \textbf{outer syntax}.
 
+\section{Evaluation}
+\index{evaluation}
+
+Assuming you have processed the declarations and definitions of
+\texttt{ToyList} presented so far, you may want to test your
+functions by running them. For example, what is the value of
+@{term"rev(True#False#[])"}? Command
+*}
+
+value "rev (True # False # [])"
+
+text{* \noindent yields the correct result @{term"False # True # []"}.
+But we can go beyond mere functional programming and evaluate terms with
+variables in them, executing functions symbolically: *}
+
+normal_form "rev (a # b # c # [])"
+
+text{*\noindent yields @{term"c # b # a # []"}.
+Command \commdx{normal\protect\_form} works for arbitrary terms
+but can be slower than command \commdx{value},
+which is restricted to variable-free terms and executable functions.
+To appreciate the subtleties of evaluating terms with variables,
+try this one:
+*}
+
+normal_form "rev (a # b # c # xs)"
+
+text{*
+\noindent Chances are that the result will at first puzzle you.
 
 \section{An Introductory Proof}
 \label{sec:intro-proof}
 
-Assuming you have processed the declarations and definitions of
-\texttt{ToyList} presented so far, we are ready to prove a few simple
+Having convinced ourselves (as well as one can by testing) that our
+definitions capture our intentions, we are ready to prove a few simple
 theorems. This will illustrate not just the basic proof commands but
 also the typical proof process.
 
diff -r ca3761e38a87 -r 68577e621ea8 doc-src/TutorialI/ToyList/document/ToyList.tex
--- a/doc-src/TutorialI/ToyList/document/ToyList.tex	Thu Nov 08 13:23:47 2007 +0100
+++ b/doc-src/TutorialI/ToyList/document/ToyList.tex	Thu Nov 08 13:24:03 2007 +0100
@@ -133,12 +133,44 @@
 When Isabelle prints a syntax error message, it refers to the HOL syntax as
 the \textbf{inner syntax} and the enclosing theory language as the \textbf{outer syntax}.
 
+\section{Evaluation}
+\index{evaluation}
+
+Assuming you have processed the declarations and definitions of
+\texttt{ToyList} presented so far, you may want to test your
+functions by running them. For example, what is the value of
+\isa{rev\ {\isacharparenleft}True\ {\isacharhash}\ False\ {\isacharhash}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}}? Command%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{value}\isamarkupfalse%
+\ {\isachardoublequoteopen}rev\ {\isacharparenleft}True\ {\isacharhash}\ False\ {\isacharhash}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}{\isachardoublequoteclose}%
+\begin{isamarkuptext}%
+\noindent yields the correct result \isa{False\ {\isacharhash}\ True\ {\isacharhash}\ {\isacharbrackleft}{\isacharbrackright}}.
+But we can go beyond mere functional programming and evaluate terms with
+variables in them, executing functions symbolically:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{normal{\isacharunderscore}form}\isamarkupfalse%
+\ {\isachardoublequoteopen}rev\ {\isacharparenleft}a\ {\isacharhash}\ b\ {\isacharhash}\ c\ {\isacharhash}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}{\isachardoublequoteclose}%
+\begin{isamarkuptext}%
+\noindent yields \isa{c\ {\isacharhash}\ b\ {\isacharhash}\ a\ {\isacharhash}\ {\isacharbrackleft}{\isacharbrackright}}.
+Command \commdx{normal\protect\_form} works for arbitrary terms
+but can be slower than command \commdx{value},
+which is restricted to variable-free terms and executable functions.
+To appreciate the subtleties of evaluating terms with variables,
+try this one:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{normal{\isacharunderscore}form}\isamarkupfalse%
+\ {\isachardoublequoteopen}rev\ {\isacharparenleft}a\ {\isacharhash}\ b\ {\isacharhash}\ c\ {\isacharhash}\ xs{\isacharparenright}{\isachardoublequoteclose}%
+\begin{isamarkuptext}%
+\noindent Chances are that the result will at first puzzle you.
 
 \section{An Introductory Proof}
 \label{sec:intro-proof}
 
-Assuming you have processed the declarations and definitions of
-\texttt{ToyList} presented so far, we are ready to prove a few simple
+Having convinced ourselves (as well as one can by testing) that our
+definitions capture our intentions, we are ready to prove a few simple
 theorems. This will illustrate not just the basic proof commands but
 also the typical proof process.