summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | nipkow |

Thu, 08 Nov 2007 13:24:03 +0100 | |

changeset 25342 | 68577e621ea8 |

parent 25341 | ca3761e38a87 |

child 25343 | 31c55418de5a |

added evaluation

doc-src/TutorialI/ToyList/ToyList.thy | file | annotate | diff | comparison | revisions | |

doc-src/TutorialI/ToyList/document/ToyList.tex | file | annotate | diff | comparison | revisions |

--- 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.

--- 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.