1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/doc-src/TutorialI/IsaMakefile Wed Apr 19 11:54:39 2000 +0200
1.3 @@ -0,0 +1,104 @@
1.4 +#
1.5 +# IsaMakefile for Tutorial
1.6 +#
1.7 +
1.8 +## targets
1.9 +
1.10 +default: styles HOL-ToyList HOL-Ifexpr HOL-CodeGen HOL-Trie HOL-Datatype HOL-Recdef HOL-Misc
1.11 +
1.12 +
1.13 +## global settings
1.14 +
1.15 +SRC = $(ISABELLE_HOME)/src
1.16 +OUT = $(ISABELLE_OUTPUT)
1.17 +LOG = $(OUT)/log
1.18 +
1.19 +
1.20 +## HOL
1.21 +
1.22 +HOL:
1.23 + @cd $(SRC)/HOL; $(ISATOOL) make HOL
1.24 +
1.25 +styles: isabelle.sty isabellesym.sty pdfsetup.sty
1.26 +
1.27 +isabelle.sty: $(ISABELLE_HOME)/lib/texinputs/isabelle.sty
1.28 + cp $(ISABELLE_HOME)/lib/texinputs/isabelle.sty .
1.29 +
1.30 +isabellesym.sty: $(ISABELLE_HOME)/lib/texinputs/isabellesym.sty
1.31 + cp $(ISABELLE_HOME)/lib/texinputs/isabellesym.sty .
1.32 +
1.33 +pdfsetup.sty: $(ISABELLE_HOME)/lib/texinputs/pdfsetup.sty
1.34 + cp $(ISABELLE_HOME)/lib/texinputs/pdfsetup.sty .
1.35 +
1.36 +
1.37 +## HOL-Ifexpr
1.38 +
1.39 +HOL-Ifexpr: HOL $(LOG)/HOL-Ifexpr.gz
1.40 +
1.41 +$(LOG)/HOL-Ifexpr.gz: $(OUT)/HOL Ifexpr/Ifexpr.thy Ifexpr/ROOT.ML
1.42 + @$(ISATOOL) usedir -i true -d dvi -D document $(OUT)/HOL Ifexpr
1.43 +
1.44 +
1.45 +## HOL-ToyList
1.46 +
1.47 +HOL-ToyList: HOL $(LOG)/HOL-ToyList.gz $(LOG)/HOL-ToyList2.gz
1.48 +
1.49 +ToyList2/ToyList.thy: ToyList2/ToyList1 ToyList2/ToyList2
1.50 + cat ToyList2/ToyList1 ToyList2/ToyList2 > ToyList2/ToyList.thy
1.51 +
1.52 +$(LOG)/HOL-ToyList2.gz: $(OUT)/HOL ToyList2/ToyList.thy ToyList2/ROOT.ML
1.53 + @$(ISATOOL) usedir -i true -d dvi -D document $(OUT)/HOL ToyList2
1.54 +
1.55 +$(LOG)/HOL-ToyList.gz: $(OUT)/HOL ToyList/ToyList.thy ToyList/ROOT.ML
1.56 + @$(ISATOOL) usedir -i true -d dvi -D document $(OUT)/HOL ToyList
1.57 +
1.58 +## HOL-CodeGen
1.59 +
1.60 +HOL-CodeGen: HOL $(LOG)/HOL-CodeGen.gz
1.61 +
1.62 +$(LOG)/HOL-CodeGen.gz: $(OUT)/HOL CodeGen/CodeGen.thy
1.63 + @$(ISATOOL) usedir -i true -d dvi -D document $(OUT)/HOL CodeGen
1.64 +
1.65 +
1.66 +## HOL-Datatype
1.67 +
1.68 +HOL-Datatype: HOL $(LOG)/HOL-Datatype.gz
1.69 +
1.70 +$(LOG)/HOL-Datatype.gz: $(OUT)/HOL Datatype/ROOT.ML Datatype/ABexpr.thy Datatype/Nested.thy \
1.71 + Datatype/Fundata.thy
1.72 + @$(ISATOOL) usedir -i true -d dvi -D document $(OUT)/HOL Datatype
1.73 +
1.74 +
1.75 +## HOL-Trie
1.76 +
1.77 +HOL-Trie: HOL $(LOG)/HOL-Trie.gz
1.78 +
1.79 +$(LOG)/HOL-Trie.gz: $(OUT)/HOL Trie/Option2.thy Trie/Trie.thy
1.80 + @$(ISATOOL) usedir -i true -d dvi -D document $(OUT)/HOL Trie
1.81 +
1.82 +
1.83 +## HOL-Recdef
1.84 +
1.85 +HOL-Recdef: HOL $(LOG)/HOL-Recdef.gz
1.86 +
1.87 +$(LOG)/HOL-Recdef.gz: $(OUT)/HOL Recdef/examples.thy Recdef/termination.thy \
1.88 + Recdef/simplification.thy Recdef/Induction.thy
1.89 + @$(ISATOOL) usedir -i true -d dvi -D document $(OUT)/HOL Recdef
1.90 +
1.91 +
1.92 +## HOL-Misc
1.93 +
1.94 +HOL-Misc: HOL $(LOG)/HOL-Misc.gz
1.95 +
1.96 +$(LOG)/HOL-Misc.gz: $(OUT)/HOL Misc/ROOT.ML Misc/Tree.thy Misc/cases.thy \
1.97 + Misc/fakenat.thy Misc/natsum.thy Misc/pairs.thy Misc/types.thy Misc/prime_def.thy \
1.98 + Misc/arith1.thy Misc/arith2.thy Misc/arith3.thy Misc/arith4.thy \
1.99 + Misc/def_rewr.thy Misc/let_rewr.thy Misc/cond_rewr.thy Misc/case_splits.thy \
1.100 + Misc/trace_simp.thy Misc/Itrev.thy Misc/asm_simp.thy
1.101 + @$(ISATOOL) usedir -i true -d dvi -D document $(OUT)/HOL Misc
1.102 +
1.103 +
1.104 +## clean
1.105 +
1.106 +clean:
1.107 + @rm -f $(LOG)/HOL-Ifexpr.gz $(LOG)/HOL-CodeGen.gz $(LOG)/HOL-Misc.gz $(LOG)/HOL-ToyList.gz $(LOG)/HOL-ToyList2.gz $(LOG)/HOL-Trie.gz $(LOG)/HOL-Datatype.gz $(LOG)/HOL-Recdef.gz
2.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
2.2 +++ b/doc-src/TutorialI/Makefile Wed Apr 19 11:54:39 2000 +0200
2.3 @@ -0,0 +1,39 @@
2.4 +#
2.5 +# $Id$
2.6 +#
2.7 +
2.8 +## targets
2.9 +
2.10 +default: dvi
2.11 +
2.12 +
2.13 +## dependencies
2.14 +
2.15 +include ../Makefile.in
2.16 +
2.17 +NAME = tutorial
2.18 +FILES = tutorial.tex basics.tex fp.tex appendix.tex \
2.19 + ../iman.sty ttbox.sty extra.sty
2.20 +
2.21 +dvi: $(NAME).dvi
2.22 +
2.23 +$(NAME).dvi: $(FILES) isabelle_hol.eps
2.24 + touch $(NAME).ind
2.25 + $(LATEX) $(NAME)
2.26 + $(BIBTEX) $(NAME)
2.27 + $(LATEX) $(NAME)
2.28 + $(LATEX) $(NAME)
2.29 + $(SEDINDEX) $(NAME)
2.30 + $(LATEX) $(NAME)
2.31 +
2.32 +pdf: $(NAME).pdf
2.33 +
2.34 +$(NAME).pdf: $(FILES) isabelle_hol.pdf
2.35 + touch $(NAME).ind
2.36 + $(PDFLATEX) $(NAME)
2.37 + $(BIBTEX) $(NAME)
2.38 + $(PDFLATEX) $(NAME)
2.39 + $(PDFLATEX) $(NAME)
2.40 + $(SEDINDEX) $(NAME)
2.41 + $(FIXBOOKMARKS) $(NAME).out
2.42 + $(PDFLATEX) $(NAME)
3.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
3.2 +++ b/doc-src/TutorialI/appendix.tex Wed Apr 19 11:54:39 2000 +0200
3.3 @@ -0,0 +1,162 @@
3.4 +\appendix
3.5 +
3.6 +\chapter{Appendix}
3.7 +\label{sec:Appendix}
3.8 +
3.9 +\begin{figure}[htbp]
3.10 +\begin{center}
3.11 +\begin{tabular}{|ccccccccccc|}
3.12 +\hline
3.13 +\indexboldpos{\isasymand}{$HOL0and} &
3.14 +\indexboldpos{\isasymor}{$HOL0or} &
3.15 +\indexboldpos{\isasymimp}{$HOL0imp} &
3.16 +\indexboldpos{\isasymnot}{$HOL0not} &
3.17 +\indexboldpos{\isasymnoteq}{$HOL0noteq} &
3.18 +\indexboldpos{\isasymforall}{$HOL0All} &
3.19 +\isasymforall &
3.20 +\indexboldpos{\isasymexists}{$HOL0Ex} &
3.21 +\isasymexists &
3.22 +\isasymuniqex\index{$HOL0ExU@\isasymuniqex|bold} &
3.23 +\isasymuniqex \\
3.24 +\texttt{\&}\indexbold{$HOL0and@{\texttt{\&}}} &
3.25 +\texttt{|}\index{$HOL0or@\ttor|bold} &
3.26 +\ttindexboldpos{-->}{$HOL0imp} &
3.27 +\verb$~$\index{$HOL0not@\verb$~$|bold} &
3.28 +\verb$~=$\index{$HOL0noteq@\verb$~=$|bold} &
3.29 +\ttindexbold{ALL} &
3.30 +\texttt{!}\index{$HOL0All@\ttall|bold} &
3.31 +\ttindexbold{EX} &
3.32 +\texttt{?}\index{$HOL0Ex@\texttt{?}|bold} &
3.33 +\ttEXU\index{EXX@\ttEXU|bold} &
3.34 +\ttuniquex\index{$HOL0ExU@\ttuniquex|bold}\\
3.35 +\hline\hline
3.36 +\indexboldpos{\isasymlbrakk}{$Isabrl} &
3.37 +\indexboldpos{\isasymrbrakk}{$Isabrr} &
3.38 +\indexboldpos{\isasymImp}{$IsaImp} &
3.39 +\indexboldpos{\isasymAnd}{$IsaAnd} &
3.40 +\indexboldpos{\isasymequiv}{$IsaEq} &
3.41 +\indexboldpos{\isasymlambda}{$Isalam} &
3.42 +\indexboldpos{\isasymFun}{$IsaFun}&
3.43 +&
3.44 +&
3.45 +&
3.46 +\\
3.47 +\texttt{[|}\index{$Isabrl@\ttlbr|bold} &
3.48 +\texttt{|]}\index{$Isabrr@\ttrbr|bold} &
3.49 +\ttindexboldpos{==>}{$IsaImp} &
3.50 +\texttt{!!}\index{$IsaAnd@\ttAnd|bold} &
3.51 +\ttindexboldpos{==}{$IsaEq} &
3.52 +\texttt{\%}\indexbold{$Isalam@\texttt{\%}} &
3.53 +\ttindexboldpos{=>}{$IsaFun}&
3.54 +&
3.55 +&
3.56 +&
3.57 + \\
3.58 +\hline\hline
3.59 +\indexboldpos{\isasymcirc}{$HOL1} &
3.60 +\indexboldpos{\isasymle}{$HOL2arithrel}&
3.61 +&
3.62 +&
3.63 +&
3.64 +&
3.65 +&
3.66 +&
3.67 +&
3.68 +&
3.69 + \\
3.70 +\ttindexbold{o} &
3.71 +\ttindexboldpos{<=}{$HOL2arithrel}&
3.72 +&
3.73 +&
3.74 +&
3.75 +&
3.76 +&
3.77 +&
3.78 +&
3.79 +&
3.80 +\\
3.81 +\hline
3.82 +\end{tabular}
3.83 +\end{center}
3.84 +\caption{Mathematical symbols and their ASCII-equivalents}
3.85 +\label{fig:ascii}
3.86 +\end{figure}
3.87 +
3.88 +\begin{figure}[htbp]
3.89 +\begin{center}
3.90 +\begin{tabular}{|lllll|}
3.91 +\hline
3.92 +\texttt{and} &
3.93 +\texttt{arities} &
3.94 +\texttt{assumes} &
3.95 +\texttt{axclass} &
3.96 +\texttt{binder} \\
3.97 +\texttt{classes} &
3.98 +\texttt{constdefs} &
3.99 +\texttt{consts} &
3.100 +\texttt{default} &
3.101 +\texttt{defines} \\
3.102 +\texttt{defs} &
3.103 +\texttt{end} &
3.104 +\texttt{fixes} &
3.105 +\texttt{global} &
3.106 +\texttt{inductive} \\
3.107 +\texttt{infixl} &
3.108 +\texttt{infixr} &
3.109 +\texttt{instance} &
3.110 +\texttt{local} &
3.111 +\texttt{locale} \\
3.112 +\texttt{mixfix} &
3.113 +\texttt{ML} &
3.114 +\texttt{MLtext} &
3.115 +\texttt{nonterminals} &
3.116 +\texttt{oracle} \\
3.117 +\texttt{output} &
3.118 +\texttt{path} &
3.119 +\texttt{primrec} &
3.120 +\texttt{rules} &
3.121 +\texttt{setup} \\
3.122 +\texttt{syntax} &
3.123 +\texttt{translations} &
3.124 +\texttt{typedef} &
3.125 +\texttt{types} &\\
3.126 +\hline
3.127 +\end{tabular}
3.128 +\end{center}
3.129 +\caption{Keywords in theory files}
3.130 +\label{fig:keywords}
3.131 +\end{figure}
3.132 +
3.133 +\begin{figure}[htbp]
3.134 +\begin{center}
3.135 +\begin{tabular}{|lllll|}
3.136 +\hline
3.137 +\texttt{ALL} &
3.138 +\texttt{case} &
3.139 +\texttt{div} &
3.140 +\texttt{dvd} &
3.141 +\texttt{else} \\
3.142 +\texttt{EX} &
3.143 +\texttt{if} &
3.144 +\texttt{in} &
3.145 +\texttt{INT} &
3.146 +\texttt{Int} \\
3.147 +\texttt{LEAST} &
3.148 +\texttt{let} &
3.149 +\texttt{mod} &
3.150 +\texttt{O} &
3.151 +\texttt{o} \\
3.152 +\texttt{of} &
3.153 +\texttt{op} &
3.154 +\texttt{PROP} &
3.155 +\texttt{SIGMA} &
3.156 +\texttt{then} \\
3.157 +\texttt{Times} &
3.158 +\texttt{UN} &
3.159 +\texttt{Un} &&\\
3.160 +\hline
3.161 +\end{tabular}
3.162 +\end{center}
3.163 +\caption{Reserved words in HOL}
3.164 +\label{fig:ReservedWords}
3.165 +\end{figure}
4.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
4.2 +++ b/doc-src/TutorialI/basics.tex Wed Apr 19 11:54:39 2000 +0200
4.3 @@ -0,0 +1,302 @@
4.4 +\chapter{Basic Concepts}
4.5 +
4.6 +\section{Introduction}
4.7 +
4.8 +This is a tutorial on how to use Isabelle/HOL as a specification and
4.9 +verification system. Isabelle is a generic system for implementing logical
4.10 +formalisms, and Isabelle/HOL is the specialization of Isabelle for
4.11 +HOL, which abbreviates Higher-Order Logic. We introduce HOL step by step
4.12 +following the equation
4.13 +\[ \mbox{HOL} = \mbox{Functional Programming} + \mbox{Logic}. \]
4.14 +We assume that the reader is familiar with the basic concepts of both fields.
4.15 +For excellent introductions to functional programming consult the textbooks
4.16 +by Bird and Wadler~\cite{Bird-Wadler} or Paulson~\cite{paulson-ml2}. Although
4.17 +this tutorial initially concentrates on functional programming, do not be
4.18 +misled: HOL can express most mathematical concepts, and functional
4.19 +programming is just one particularly simple and ubiquitous instance.
4.20 +
4.21 +This tutorial introduces HOL via Isabelle/Isar~\cite{isabelle-isar-ref},
4.22 +which is an extension of Isabelle~\cite{paulson-isa-book} with structured
4.23 +proofs.\footnote{Thus the full name of the system should be
4.24 + Isabelle/Isar/HOL, but that is a bit of a mouthful.} The most noticeable
4.25 +difference to classical Isabelle (which is the basis of another version of
4.26 +this tutorial) is the replacement of the ML level by a dedicated language for
4.27 +definitions and proofs.
4.28 +
4.29 +A tutorial is by definition incomplete. Currently the tutorial only
4.30 +introduces the rudiments of Isar's proof language. To fully exploit the power
4.31 +of Isar you need to consult the Isabelle/Isar Reference
4.32 +Manual~\cite{isabelle-isar-ref}. If you want to use Isabelle's ML level
4.33 +directly (for example for writing your own proof procedures) see the Isabelle
4.34 +Reference Manual~\cite{isabelle-ref}; for details relating to HOL see the
4.35 +Isabelle/HOL manual~\cite{isabelle-HOL}. All manuals have a comprehensive
4.36 +index.
4.37 +
4.38 +\section{Theories}
4.39 +\label{sec:Basic:Theories}
4.40 +
4.41 +Working with Isabelle means creating theories. Roughly speaking, a
4.42 +\bfindex{theory} is a named collection of types, functions, and theorems,
4.43 +much like a module in a programming language or a specification in a
4.44 +specification language. In fact, theories in HOL can be either. The general
4.45 +format of a theory \texttt{T} is
4.46 +\begin{ttbox}
4.47 +theory T = B\(@1\) + \(\cdots\) + B\(@n\):
4.48 +\(\textit{declarations, definitions, and proofs}\)
4.49 +end
4.50 +\end{ttbox}
4.51 +where \texttt{B}$@1$, \dots, \texttt{B}$@n$ are the names of existing
4.52 +theories that \texttt{T} is based on and \texttt{\textit{declarations,
4.53 + definitions, and proofs}} represents the newly introduced concepts
4.54 +(types, functions etc) and proofs about them. The \texttt{B}$@i$ are the
4.55 +direct \textbf{parent theories}\indexbold{parent theory} of \texttt{T}.
4.56 +Everything defined in the parent theories (and their parents \dots) is
4.57 +automatically visible. To avoid name clashes, identifiers can be
4.58 +\textbf{qualified} by theory names as in \texttt{T.f} and
4.59 +\texttt{B.f}.\indexbold{identifier!qualified} Each theory \texttt{T} must
4.60 +reside in a \indexbold{theory file} named \texttt{T.thy}.
4.61 +
4.62 +This tutorial is concerned with introducing you to the different linguistic
4.63 +constructs that can fill \textit{\texttt{declarations, definitions, and
4.64 + proofs}} in the above theory template. A complete grammar of the basic
4.65 +constructs is found in the Isabelle/Isar Reference Manual.
4.66 +
4.67 +HOL's theory library is available online at
4.68 +\begin{center}\small
4.69 + \url{http://isabelle.in.tum.de/library/}
4.70 +\end{center}
4.71 +and is recommended browsing.
4.72 +\begin{warn}
4.73 + HOL contains a theory \ttindexbold{Main}, the union of all the basic
4.74 + predefined theories like arithmetic, lists, sets, etc.\ (see the online
4.75 + library). Unless you know what you are doing, always include \texttt{Main}
4.76 + as a direct or indirect parent theory of all your theories.
4.77 +\end{warn}
4.78 +
4.79 +
4.80 +\section{Interaction and interfaces}
4.81 +
4.82 +Interaction with Isabelle can either occur at the shell level or through more
4.83 +advanced interfaces. To keep the tutorial independent of the interface we
4.84 +have phrased the description of the intraction in a neutral language. For
4.85 +example, the phrase ``to cancel a proof'' means to type \texttt{oops} at the
4.86 +shell level, which is explained the first time the phrase is used. Other
4.87 +interfaces perform the same act by cursor movements and/or mouse clicks.
4.88 +Although shell-based interaction is quite feasible for the kind of proof
4.89 +scripts currently presented in this tutorial, the recommended interface for
4.90 +Isabelle/Isar is the Emacs-based \bfindex{Proof
4.91 + General}~\cite{Aspinall:TACAS:2000,proofgeneral}.
4.92 +
4.93 +To improve readability some of the interfaces (including the shell level)
4.94 +offer special fonts with mathematical symbols. Therefore the usual
4.95 +mathematical symbols are used throughout the tutorial. Their
4.96 +ASCII-equivalents are shown in figure~\ref{fig:ascii} in the appendix.
4.97 +
4.98 +Finally, a word about semicolons.\indexbold{$Isar@\texttt{;}} Some interfaces,
4.99 +for example Proof General, require each command to be terminated by a
4.100 +semicolon, whereas others, for example the shell level, do not. But even at
4.101 +the shell level it is advisable to use semicolons to enforce that a command
4.102 +is executed immediately; otherwise Isabelle may wait for the next keyword
4.103 +before it knows that the command is complete. Note that for readibility
4.104 +reasons we often drop the final semicolon in the text.
4.105 +
4.106 +
4.107 +\section{Types, terms and formulae}
4.108 +\label{sec:TypesTermsForms}
4.109 +\indexbold{type}
4.110 +
4.111 +Embedded in the declarations of a theory are the types, terms and formulae of
4.112 +HOL. HOL is a typed logic whose type system resembles that of functional
4.113 +programming languages like ML or Haskell. Thus there are
4.114 +\begin{description}
4.115 +\item[base types,] in particular \ttindex{bool}, the type of truth values,
4.116 +and \ttindex{nat}, the type of natural numbers.
4.117 +\item[type constructors,] in particular \texttt{list}, the type of
4.118 +lists, and \texttt{set}, the type of sets. Type constructors are written
4.119 +postfix, e.g.\ \texttt{(nat)list} is the type of lists whose elements are
4.120 +natural numbers. Parentheses around single arguments can be dropped (as in
4.121 +\texttt{nat list}), multiple arguments are separated by commas (as in
4.122 +\texttt{(bool,nat)foo}).
4.123 +\item[function types,] denoted by \isasymFun\indexbold{$IsaFun@\isasymFun}.
4.124 + In HOL \isasymFun\ represents {\em total} functions only. As is customary,
4.125 + \texttt{$\tau@1$ \isasymFun~$\tau@2$ \isasymFun~$\tau@3$} means
4.126 + \texttt{$\tau@1$ \isasymFun~($\tau@2$ \isasymFun~$\tau@3$)}. Isabelle also
4.127 + supports the notation \texttt{[$\tau@1,\dots,\tau@n$] \isasymFun~$\tau$}
4.128 + which abbreviates \texttt{$\tau@1$ \isasymFun~$\cdots$ \isasymFun~$\tau@n$
4.129 + \isasymFun~$\tau$}.
4.130 +\item[type variables,] denoted by \texttt{'a}, \texttt{'b} etc, just like in
4.131 +ML. They give rise to polymorphic types like \texttt{'a \isasymFun~'a}, the
4.132 +type of the identity function.
4.133 +\end{description}
4.134 +\begin{warn}
4.135 + Types are extremely important because they prevent us from writing
4.136 + nonsense. Isabelle insists that all terms and formulae must be well-typed
4.137 + and will print an error message if a type mismatch is encountered. To
4.138 + reduce the amount of explicit type information that needs to be provided by
4.139 + the user, Isabelle infers the type of all variables automatically (this is
4.140 + called \bfindex{type inference}) and keeps quiet about it. Occasionally
4.141 + this may lead to misunderstandings between you and the system. If anything
4.142 + strange happens, we recommend to set the \rmindex{flag}
4.143 + \ttindexbold{show_types} that tells Isabelle to display type information
4.144 + that is usually suppressed: simply type
4.145 +\begin{ttbox}
4.146 +ML "set show_types"
4.147 +\end{ttbox}
4.148 +
4.149 +\noindent
4.150 +This can be reversed by \texttt{ML "reset show_types"}. Various other flags
4.151 +can be set and reset in the same manner.\bfindex{flag!(re)setting}
4.152 +\end{warn}
4.153 +
4.154 +
4.155 +\textbf{Terms}\indexbold{term} are formed as in functional programming by
4.156 +applying functions to arguments. If \texttt{f} is a function of type
4.157 +\texttt{$\tau@1$ \isasymFun~$\tau@2$} and \texttt{t} is a term of type
4.158 +$\tau@1$ then \texttt{f~t} is a term of type $\tau@2$. HOL also supports
4.159 +infix functions like \texttt{+} and some basic constructs from functional
4.160 +programming:
4.161 +\begin{description}
4.162 +\item[\texttt{if $b$ then $t@1$ else $t@2$}]\indexbold{*if}
4.163 +means what you think it means and requires that
4.164 +$b$ is of type \texttt{bool} and $t@1$ and $t@2$ are of the same type.
4.165 +\item[\texttt{let $x$ = $t$ in $u$}]\indexbold{*let}
4.166 +is equivalent to $u$ where all occurrences of $x$ have been replaced by
4.167 +$t$. For example,
4.168 +\texttt{let x = 0 in x+x} means \texttt{0+0}. Multiple bindings are separated
4.169 +by semicolons: \texttt{let $x@1$ = $t@1$; \dots; $x@n$ = $t@n$ in $u$}.
4.170 +\item[\texttt{case $e$ of $c@1$ \isasymFun~$e@1$ |~\dots~| $c@n$ \isasymFun~$e@n$}]
4.171 +\indexbold{*case}
4.172 +evaluates to $e@i$ if $e$ is of the form
4.173 +$c@i$. See~\S\ref{sec:case-expressions} for details.
4.174 +\end{description}
4.175 +
4.176 +Terms may also contain
4.177 +\isasymlambda-abstractions\indexbold{$Isalam@\isasymlambda}. For example,
4.178 +\texttt{\isasymlambda{}x.~x+1} is the function that takes an argument
4.179 +\texttt{x} and returns \texttt{x+1}. Instead of
4.180 +\texttt{\isasymlambda{}x.\isasymlambda{}y.\isasymlambda{}z.}~$t$ we can write
4.181 +\texttt{\isasymlambda{}x~y~z.}~$t$.
4.182 +
4.183 +\textbf{Formulae}\indexbold{formula}
4.184 +are terms of type \texttt{bool}. There are the basic
4.185 +constants \ttindexbold{True} and \ttindexbold{False} and the usual logical
4.186 +connectives (in decreasing order of priority):
4.187 +\indexboldpos{\isasymnot}{$HOL0not},
4.188 +\indexboldpos{\isasymand}{$HOL0and},
4.189 +\indexboldpos{\isasymor}{$HOL0or}, and
4.190 +\indexboldpos{\isasymimp}{$HOL0imp},
4.191 +all of which (except the unary \isasymnot) associate to the right. In
4.192 +particular \texttt{A \isasymimp~B \isasymimp~C} means
4.193 +\texttt{A \isasymimp~(B \isasymimp~C)} and is thus
4.194 +logically equivalent with \texttt{A \isasymand~B \isasymimp~C}
4.195 +(which is \texttt{(A \isasymand~B) \isasymimp~C}).
4.196 +
4.197 +Equality is available in the form of the infix function
4.198 +\texttt{=}\indexbold{$HOL0eq@\texttt{=}} of type \texttt{'a \isasymFun~'a
4.199 + \isasymFun~bool}. Thus \texttt{$t@1$ = $t@2$} is a formula provided $t@1$
4.200 +and $t@2$ are terms of the same type. In case $t@1$ and $t@2$ are of type
4.201 +\texttt{bool}, \texttt{=} acts as if-and-only-if. The formula
4.202 +$t@1$~\isasymnoteq~$t@2$ is merely an abbreviation for
4.203 +\texttt{\isasymnot($t@1$ = $t@2$)}.
4.204 +
4.205 +The syntax for quantifiers is
4.206 +\texttt{\isasymforall{}x.}~$P$\indexbold{$HOL0All@\isasymforall} and
4.207 +\texttt{\isasymexists{}x.}~$P$\indexbold{$HOL0Ex@\isasymexists}. There is
4.208 +even \texttt{\isasymuniqex{}x.}~$P$\index{$HOL0ExU@\isasymuniqex|bold}, which
4.209 +means that there exists exactly one \texttt{x} that satisfies $P$.
4.210 +Nested quantifications can be abbreviated:
4.211 +\texttt{\isasymforall{}x~y~z.}~$P$ means
4.212 +\texttt{\isasymforall{}x.\isasymforall{}y.\isasymforall{}z.}~$P$.
4.213 +
4.214 +Despite type inference, it is sometimes necessary to attach explicit
4.215 +\bfindex{type constraints} to a term. The syntax is \texttt{$t$::$\tau$} as
4.216 +in \texttt{x < (y::nat)}. Note that \ttindexboldpos{::}{$Isalamtc} binds weakly
4.217 +and should therefore be enclosed in parentheses: \texttt{x < y::nat} is
4.218 +ill-typed because it is interpreted as \texttt{(x < y)::nat}. The main reason
4.219 +for type constraints are overloaded functions like \texttt{+}, \texttt{*} and
4.220 +\texttt{<}. (See \S\ref{sec:TypeClasses} for a full discussion of
4.221 +overloading.)
4.222 +
4.223 +\begin{warn}
4.224 +In general, HOL's concrete syntax tries to follow the conventions of
4.225 +functional programming and mathematics. Below we list the main rules that you
4.226 +should be familiar with to avoid certain syntactic traps. A particular
4.227 +problem for novices can be the priority of operators. If you are unsure, use
4.228 +more rather than fewer parentheses. In those cases where Isabelle echoes your
4.229 +input, you can see which parentheses are dropped---they were superfluous. If
4.230 +you are unsure how to interpret Isabelle's output because you don't know
4.231 +where the (dropped) parentheses go, set (and possibly reset) the \rmindex{flag}
4.232 +\ttindexbold{show_brackets}:
4.233 +\begin{ttbox}
4.234 +ML "set show_brackets"; \(\dots\); ML "reset show_brackets";
4.235 +\end{ttbox}
4.236 +\end{warn}
4.237 +
4.238 +\begin{itemize}
4.239 +\item
4.240 +Remember that \texttt{f t u} means \texttt{(f t) u} and not \texttt{f(t u)}!
4.241 +\item
4.242 +Isabelle allows infix functions like \texttt{+}. The prefix form of function
4.243 +application binds more strongly than anything else and hence \texttt{f~x + y}
4.244 +means \texttt{(f~x)~+~y} and not \texttt{f(x+y)}.
4.245 +\item Remember that in HOL if-and-only-if is expressed using equality. But
4.246 + equality has a high priority, as befitting a relation, while if-and-only-if
4.247 + typically has the lowest priority. Thus, \texttt{\isasymnot~\isasymnot~P =
4.248 + P} means \texttt{\isasymnot\isasymnot(P = P)} and not
4.249 + \texttt{(\isasymnot\isasymnot P) = P}. When using \texttt{=} to mean
4.250 + logical equivalence, enclose both operands in parentheses, as in \texttt{(A
4.251 + \isasymand~B) = (B \isasymand~A)}.
4.252 +\item
4.253 +Constructs with an opening but without a closing delimiter bind very weakly
4.254 +and should therefore be enclosed in parentheses if they appear in subterms, as
4.255 +in \texttt{f = (\isasymlambda{}x.~x)}. This includes \ttindex{if},
4.256 +\ttindex{let}, \ttindex{case}, \isasymlambda, and quantifiers.
4.257 +\item
4.258 +Never write \texttt{\isasymlambda{}x.x} or \texttt{\isasymforall{}x.x=x}
4.259 +because \texttt{x.x} is always read as a single qualified identifier that
4.260 +refers to an item \texttt{x} in theory \texttt{x}. Write
4.261 +\texttt{\isasymlambda{}x.~x} and \texttt{\isasymforall{}x.~x=x} instead.
4.262 +\item Identifiers\indexbold{identifier} may contain \texttt{_} and \texttt{'}.
4.263 +\end{itemize}
4.264 +
4.265 +Remember that ASCII-equivalents of all mathematical symbols are
4.266 +given in figure~\ref{fig:ascii} in the appendix.
4.267 +
4.268 +\section{Variables}
4.269 +\label{sec:variables}
4.270 +\indexbold{variable}
4.271 +
4.272 +Isabelle distinguishes free and bound variables just as is customary. Bound
4.273 +variables are automatically renamed to avoid clashes with free variables. In
4.274 +addition, Isabelle has a third kind of variable, called a \bfindex{schematic
4.275 + variable}\indexbold{variable!schematic} or \bfindex{unknown}, which starts
4.276 +with a \texttt{?}. Logically, an unknown is a free variable. But it may be
4.277 +instantiated by another term during the proof process. For example, the
4.278 +mathematical theorem $x = x$ is represented in Isabelle as \texttt{?x = ?x},
4.279 +which means that Isabelle can instantiate it arbitrarily. This is in contrast
4.280 +to ordinary variables, which remain fixed. The programming language Prolog
4.281 +calls unknowns {\em logical\/} variables.
4.282 +
4.283 +Most of the time you can and should ignore unknowns and work with ordinary
4.284 +variables. Just don't be surprised that after you have finished the proof of
4.285 +a theorem, Isabelle will turn your free variables into unknowns: it merely
4.286 +indicates that Isabelle will automatically instantiate those unknowns
4.287 +suitably when the theorem is used in some other proof.
4.288 +\begin{warn}
4.289 + If you use \texttt{?}\index{$HOL0Ex@\texttt{?}} as an existential
4.290 + quantifier, it needs to be followed by a space. Otherwise \texttt{?x} is
4.291 + interpreted as a schematic variable.
4.292 +\end{warn}
4.293 +
4.294 +\section{Getting started}
4.295 +
4.296 +Assuming you have installed Isabelle, you start it by typing \texttt{isabelle
4.297 + -I HOL} in a shell window.\footnote{Simply executing \texttt{isabelle -I}
4.298 + starts the default logic, which usually is already \texttt{HOL}. This is
4.299 + controlled by the \texttt{ISABELLE_LOGIC} setting, see \emph{The Isabelle
4.300 + System Manual} for more details.} This presents you with Isabelle's most
4.301 +basic ASCII interface. In addition you need to open an editor window to
4.302 +create theory files. While you are developing a theory, we recommend to
4.303 +type each command into the file first and then enter it into Isabelle by
4.304 +copy-and-paste, thus ensuring that you have a complete record of your theory.
4.305 +As mentioned earlier, Proof General offers a much superior interface.
5.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
5.2 +++ b/doc-src/TutorialI/extra.sty Wed Apr 19 11:54:39 2000 +0200
5.3 @@ -0,0 +1,29 @@
5.4 +% extra.sty : Isabelle Manual extra macros for non-Springer version
5.5 +%
5.6 +\typeout{Document Style extra. Released 17 February 1994}
5.7 +
5.8 +%%Euro-style date: 20 September 1955
5.9 +\def\today{\number\day\space\ifcase\month\or
5.10 +January\or February\or March\or April\or May\or June\or
5.11 +July\or August\or September\or October\or November\or December\fi
5.12 +\space\number\year}
5.13 +
5.14 +%%Borrowed from alltt.sty, but leaves % as the comment character
5.15 +\def\docspecials{\do\ \do\$\do\&%
5.16 + \do\#\do\^\do\^^K\do\_\do\^^A\do\~}
5.17 +
5.18 +%%%Put first chapter on odd page, with arabic numbering; like \cleardoublepage
5.19 +\newcommand\clearfirst{\clearpage\ifodd\c@page\else
5.20 + \hbox{}\newpage\if@twocolumn\hbox{}\newpage\fi\fi
5.21 + \pagenumbering{arabic}}
5.22 +
5.23 +%%%Ruled chapter headings
5.24 +\def\@rulehead#1{\hrule height1pt \vskip 14pt \Huge \bf
5.25 + #1 \vskip 14pt\hrule height1pt}
5.26 +\def\@makechapterhead#1{ { \parindent 0pt
5.27 + \ifnum\c@secnumdepth >\m@ne \raggedleft\large\bf\@chapapp{} \thechapter \par
5.28 + \vskip 20pt \fi \raggedright \@rulehead{#1} \par \nobreak \vskip 40pt } }
5.29 +
5.30 +\def\@makeschapterhead#1{ { \parindent 0pt \raggedright
5.31 + \@rulehead{#1} \par \nobreak \vskip 40pt } }
5.32 +
6.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
6.2 +++ b/doc-src/TutorialI/fp.tex Wed Apr 19 11:54:39 2000 +0200
6.3 @@ -0,0 +1,841 @@
6.4 +\chapter{Functional Programming in HOL}
6.5 +
6.6 +Although on the surface this chapter is mainly concerned with how to write
6.7 +functional programs in HOL and how to verify them, most of the
6.8 +constructs and proof procedures introduced are general purpose and recur in
6.9 +any specification or verification task.
6.10 +
6.11 +The dedicated functional programmer should be warned: HOL offers only {\em
6.12 + total functional programming} --- all functions in HOL must be total; lazy
6.13 +data structures are not directly available. On the positive side, functions
6.14 +in HOL need not be computable: HOL is a specification language that goes well
6.15 +beyond what can be expressed as a program. However, for the time being we
6.16 +concentrate on the computable.
6.17 +
6.18 +\section{An introductory theory}
6.19 +\label{sec:intro-theory}
6.20 +
6.21 +Functional programming needs datatypes and functions. Both of them can be
6.22 +defined in a theory with a syntax reminiscent of languages like ML or
6.23 +Haskell. As an example consider the theory in figure~\ref{fig:ToyList}.
6.24 +We will now examine it line by line.
6.25 +
6.26 +\begin{figure}[htbp]
6.27 +\begin{ttbox}\makeatother
6.28 +\input{ToyList2/ToyList1}\end{ttbox}
6.29 +\caption{A theory of lists}
6.30 +\label{fig:ToyList}
6.31 +\end{figure}
6.32 +
6.33 +{\makeatother\input{ToyList/document/ToyList.tex}}
6.34 +
6.35 +The complete proof script is shown in figure~\ref{fig:ToyList-proofs}. The
6.36 +concatenation of figures \ref{fig:ToyList} and \ref{fig:ToyList-proofs}
6.37 +constitutes the complete theory \texttt{ToyList} and should reside in file
6.38 +\texttt{ToyList.thy}. It is good practice to present all declarations and
6.39 +definitions at the beginning of a theory to facilitate browsing.
6.40 +
6.41 +\begin{figure}[htbp]
6.42 +\begin{ttbox}\makeatother
6.43 +\input{ToyList2/ToyList2}\end{ttbox}
6.44 +\caption{Proofs about lists}
6.45 +\label{fig:ToyList-proofs}
6.46 +\end{figure}
6.47 +
6.48 +\subsubsection*{Review}
6.49 +
6.50 +This is the end of our toy proof. It should have familiarized you with
6.51 +\begin{itemize}
6.52 +\item the standard theorem proving procedure:
6.53 +state a goal (lemma or theorem); proceed with proof until a separate lemma is
6.54 +required; prove that lemma; come back to the original goal.
6.55 +\item a specific procedure that works well for functional programs:
6.56 +induction followed by all-out simplification via \isa{auto}.
6.57 +\item a basic repertoire of proof commands.
6.58 +\end{itemize}
6.59 +
6.60 +
6.61 +\section{Some helpful commands}
6.62 +\label{sec:commands-and-hints}
6.63 +
6.64 +This section discusses a few basic commands for manipulating the proof state
6.65 +and can be skipped by casual readers.
6.66 +
6.67 +There are two kinds of commands used during a proof: the actual proof
6.68 +commands and auxiliary commands for examining the proof state and controlling
6.69 +the display. Simple proof commands are of the form
6.70 +\isacommand{apply}\isa{(method)}\indexbold{apply} where \bfindex{method} is a
6.71 +synonym for ``theorem proving function''. Typical examples are
6.72 +\isa{induct_tac} and \isa{auto}. Further methods are introduced throughout
6.73 +the tutorial. Unless stated otherwise you may assume that a method attacks
6.74 +merely the first subgoal. An exception is \isa{auto} which tries to solve all
6.75 +subgoals.
6.76 +
6.77 +The most useful auxiliary commands are:
6.78 +\begin{description}
6.79 +\item[Undoing:] \isacommand{undo}\indexbold{*undo} undoes the effect of the
6.80 + last command; \isacommand{undo} can be undone by
6.81 + \isacommand{redo}\indexbold{*redo}. Both are only needed at the shell
6.82 + level and should not occur in the final theory.
6.83 +\item[Printing the current state:] \isacommand{pr}\indexbold{*pr} redisplays
6.84 + the current proof state, for example when it has disappeared off the
6.85 + screen.
6.86 +\item[Limiting the number of subgoals:] \isacommand{pr}~$n$ tells Isabelle to
6.87 + print only the first $n$ subgoals from now on and redisplays the current
6.88 + proof state. This is helpful when there are many subgoals.
6.89 +\item[Modifying the order of subgoals:]
6.90 +\isacommand{defer}\indexbold{*defer} moves the first subgoal to the end and
6.91 +\isacommand{prefer}\indexbold{*prefer}~$n$ moves subgoal $n$ to the front.
6.92 +\item[Printing theorems:]
6.93 + \isacommand{thm}\indexbold{*thm}~\textit{name}$@1$~\dots~\textit{name}$@n$
6.94 + prints the named theorems.
6.95 +\item[Displaying types:] We have already mentioned the flag
6.96 + \ttindex{show_types} above. It can also be useful for detecting typos in
6.97 + formulae early on. For example, if \texttt{show_types} is set and the goal
6.98 + \isa{rev(rev xs) = xs} is started, Isabelle prints the additional output
6.99 +\par\noindent
6.100 +\begin{isabelle}%
6.101 +Variables:\isanewline
6.102 +~~xs~::~'a~list
6.103 +\end{isabelle}%
6.104 +\par\noindent
6.105 +which tells us that Isabelle has correctly inferred that
6.106 +\isa{xs} is a variable of list type. On the other hand, had we
6.107 +made a typo as in \isa{rev(re xs) = xs}, the response
6.108 +\par\noindent
6.109 +\begin{isabelle}%
6.110 +Variables:\isanewline
6.111 +~~re~::~'a~list~{\isasymRightarrow}~'a~list\isanewline
6.112 +~~xs~::~'a~list%
6.113 +\end{isabelle}%
6.114 +\par\noindent
6.115 +would have alerted us because of the unexpected variable \isa{re}.
6.116 +\item[Reading terms and types:] \isacommand{term}\indexbold{*term}
6.117 + \textit{string} reads, type-checks and prints the given string as a term in
6.118 + the current context; the inferred type is output as well.
6.119 + \isacommand{typ}\indexbold{*typ} \textit{string} reads and prints the given
6.120 + string as a type in the current context.
6.121 +\item[(Re)loading theories:] When you start your interaction you must open a
6.122 + named theory with the line
6.123 + \isacommand{theory}\texttt{~T~=}~\dots~\texttt{:}. Isabelle automatically
6.124 + loads all the required parent theories from their respective files (which
6.125 + may take a moment, unless the theories are already loaded and the files
6.126 + have not been modified). The only time when you need to load a theory by
6.127 + hand is when you simply want to check if it loads successfully without
6.128 + wanting to make use of the theory itself. This you can do by typing
6.129 + \isacommand{use\_thy}\indexbold{*use_thy}~\texttt{"T"}.
6.130 +
6.131 + If you suddenly discover that you need to modify a parent theory of your
6.132 + current theory you must first abandon your current theory (at the shell
6.133 + level type \isacommand{kill}\indexbold{*kill}). After the parent theory has
6.134 + been modified you go back to your original theory. When its first line
6.135 + \isacommand{theory}\texttt{~T~=}~\dots~\texttt{:} is processed, the
6.136 + modified parent is reloaded automatically.
6.137 +\end{description}
6.138 +Further commands are found in the Isabelle/Isar Reference Manual.
6.139 +
6.140 +
6.141 +\section{Datatypes}
6.142 +\label{sec:datatype}
6.143 +
6.144 +Inductive datatypes are part of almost every non-trivial application of HOL.
6.145 +First we take another look at a very important example, the datatype of
6.146 +lists, before we turn to datatypes in general. The section closes with a
6.147 +case study.
6.148 +
6.149 +
6.150 +\subsection{Lists}
6.151 +\indexbold{*list}
6.152 +
6.153 +Lists are one of the essential datatypes in computing. Readers of this
6.154 +tutorial and users of HOL need to be familiar with their basic operations.
6.155 +Theory \texttt{ToyList} is only a small fragment of HOL's predefined theory
6.156 +\texttt{List}\footnote{\url{http://isabelle.in.tum.de/library/HOL/List.html}}.
6.157 +The latter contains many further operations. For example, the functions
6.158 +\isaindexbold{hd} (`head') and \isaindexbold{tl} (`tail') return the first
6.159 +element and the remainder of a list. (However, pattern-matching is usually
6.160 +preferable to \isa{hd} and \isa{tl}.) Theory \texttt{List} also contains
6.161 +more syntactic sugar: \isa{[}$x@1$\isa{,}\dots\isa{,}$x@n$\isa{]} abbreviates
6.162 +$x@1$\isa{\#}\dots\isa{\#}$x@n$\isa{\#[]}. In the rest of the tutorial we
6.163 +always use HOL's predefined lists.
6.164 +
6.165 +
6.166 +\subsection{The general format}
6.167 +\label{sec:general-datatype}
6.168 +
6.169 +The general HOL \isacommand{datatype} definition is of the form
6.170 +\[
6.171 +\isacommand{datatype}~(\alpha@1, \dots, \alpha@n) \, t ~=~
6.172 +C@1~\tau@{11}~\dots~\tau@{1k@1} ~\mid~ \dots ~\mid~
6.173 +C@m~\tau@{m1}~\dots~\tau@{mk@m}
6.174 +\]
6.175 +where $\alpha@i$ are type variables (the parameters), $C@i$ are distinct
6.176 +constructor names and $\tau@{ij}$ are types; it is customary to capitalize
6.177 +the first letter in constructor names. There are a number of
6.178 +restrictions (such as that the type should not be empty) detailed
6.179 +elsewhere~\cite{isabelle-HOL}. Isabelle notifies you if you violate them.
6.180 +
6.181 +Laws about datatypes, such as \isa{[] \isasymnoteq~x\#xs} and
6.182 +\isa{(x\#xs = y\#ys) = (x=y \isasymand~xs=ys)}, are used automatically
6.183 +during proofs by simplification. The same is true for the equations in
6.184 +primitive recursive function definitions.
6.185 +
6.186 +\subsection{Primitive recursion}
6.187 +
6.188 +Functions on datatypes are usually defined by recursion. In fact, most of the
6.189 +time they are defined by what is called \bfindex{primitive recursion}.
6.190 +The keyword \isacommand{primrec}\indexbold{*primrec} is followed by a list of
6.191 +equations
6.192 +\[ f \, x@1 \, \dots \, (C \, y@1 \, \dots \, y@k)\, \dots \, x@n = r \]
6.193 +such that $C$ is a constructor of the datatype $t$ and all recursive calls of
6.194 +$f$ in $r$ are of the form $f \, \dots \, y@i \, \dots$ for some $i$. Thus
6.195 +Isabelle immediately sees that $f$ terminates because one (fixed!) argument
6.196 +becomes smaller with every recursive call. There must be exactly one equation
6.197 +for each constructor. Their order is immaterial.
6.198 +A more general method for defining total recursive functions is explained in
6.199 +\S\ref{sec:recdef}.
6.200 +
6.201 +\begin{exercise}
6.202 +\input{Misc/document/Tree.tex}%
6.203 +\end{exercise}
6.204 +
6.205 +\subsection{Case expressions}
6.206 +\label{sec:case-expressions}
6.207 +
6.208 +HOL also features \isaindexbold{case}-expressions for analyzing
6.209 +elements of a datatype. For example,
6.210 +% case xs of [] => 0 | y#ys => y
6.211 +\begin{isabellepar}%
6.212 +~~~case~xs~of~[]~{\isasymRightarrow}~0~|~y~\#~ys~{\isasymRightarrow}~y
6.213 +\end{isabellepar}%
6.214 +evaluates to \isa{0} if \isa{xs} is \isa{[]} and to \isa{y} if
6.215 +\isa{xs} is \isa{y\#ys}. (Since the result in both branches must be of
6.216 +the same type, it follows that \isa{y::nat} and hence
6.217 +\isa{xs::(nat)list}.)
6.218 +
6.219 +In general, if $e$ is a term of the datatype $t$ defined in
6.220 +\S\ref{sec:general-datatype} above, the corresponding
6.221 +\isa{case}-expression analyzing $e$ is
6.222 +\[
6.223 +\begin{array}{rrcl}
6.224 +\isa{case}~e~\isa{of} & C@1~x@{11}~\dots~x@{1k@1} & \To & e@1 \\
6.225 + \vdots \\
6.226 + \mid & C@m~x@{m1}~\dots~x@{mk@m} & \To & e@m
6.227 +\end{array}
6.228 +\]
6.229 +
6.230 +\begin{warn}
6.231 +{\em All} constructors must be present, their order is fixed, and nested
6.232 +patterns are not supported. Violating these restrictions results in strange
6.233 +error messages.
6.234 +\end{warn}
6.235 +\noindent
6.236 +Nested patterns can be simulated by nested \isa{case}-expressions: instead
6.237 +of
6.238 +% case xs of [] => 0 | [x] => x | x#(y#zs) => y
6.239 +\begin{isabellepar}%
6.240 +~~~case~xs~of~[]~{\isasymRightarrow}~0~|~[x]~{\isasymRightarrow}~x~|~x~\#~y~\#~zs~{\isasymRightarrow}~y
6.241 +\end{isabellepar}%
6.242 +write
6.243 +% term(latex xsymbols symbols)"case xs of [] => 0 | x#ys => (case ys of [] => x | y#zs => y)";
6.244 +\begin{isabellepar}%
6.245 +~~~case~xs~of~[]~{\isasymRightarrow}~0~|~x~\#~ys~{\isasymRightarrow}~(case~ys~of~[]~{\isasymRightarrow}~x~|~y~\#~zs~{\isasymRightarrow}~y)%
6.246 +\end{isabellepar}%
6.247 +Note that \isa{case}-expressions should be enclosed in parentheses to
6.248 +indicate their scope.
6.249 +
6.250 +\subsection{Structural induction and case distinction}
6.251 +\indexbold{structural induction}
6.252 +\indexbold{induction!structural}
6.253 +\indexbold{case distinction}
6.254 +
6.255 +Almost all the basic laws about a datatype are applied automatically during
6.256 +simplification. Only induction is invoked by hand via \isaindex{induct_tac},
6.257 +which works for any datatype. In some cases, induction is overkill and a case
6.258 +distinction over all constructors of the datatype suffices. This is performed
6.259 +by \isaindexbold{case_tac}. A trivial example:
6.260 +
6.261 +\input{Misc/document/cases.tex}%
6.262 +
6.263 +Note that we do not need to give a lemma a name if we do not intend to refer
6.264 +to it explicitly in the future.
6.265 +
6.266 +\begin{warn}
6.267 + Induction is only allowed on free (or \isasymAnd-bound) variables that
6.268 + should not occur among the assumptions of the subgoal. Case distinction
6.269 + (\isa{case_tac}) works for arbitrary terms, which need to be
6.270 + quoted if they are non-atomic.
6.271 +\end{warn}
6.272 +
6.273 +
6.274 +\subsection{Case study: boolean expressions}
6.275 +\label{sec:boolex}
6.276 +
6.277 +The aim of this case study is twofold: it shows how to model boolean
6.278 +expressions and some algorithms for manipulating them, and it demonstrates
6.279 +the constructs introduced above.
6.280 +
6.281 +\input{Ifexpr/document/Ifexpr.tex}
6.282 +
6.283 +How does one come up with the required lemmas? Try to prove the main theorems
6.284 +without them and study carefully what \isa{auto} leaves unproved. This has
6.285 +to provide the clue. The necessity of universal quantification
6.286 +(\isa{\isasymforall{}t e}) in the two lemmas is explained in
6.287 +\S\ref{sec:InductionHeuristics}
6.288 +
6.289 +\begin{exercise}
6.290 + We strengthen the definition of a \isa{normal} If-expression as follows:
6.291 + the first argument of all \isa{IF}s must be a variable. Adapt the above
6.292 + development to this changed requirement. (Hint: you may need to formulate
6.293 + some of the goals as implications (\isasymimp) rather than equalities
6.294 + (\isa{=}).)
6.295 +\end{exercise}
6.296 +
6.297 +\section{Some basic types}
6.298 +
6.299 +
6.300 +\subsection{Natural numbers}
6.301 +\index{arithmetic|(}
6.302 +
6.303 +\input{Misc/document/fakenat.tex}
6.304 +\input{Misc/document/natsum.tex}
6.305 +
6.306 +The usual arithmetic operations \ttindexboldpos{+}{$HOL2arithfun},
6.307 +\ttindexboldpos{-}{$HOL2arithfun}, \ttindexboldpos{*}{$HOL2arithfun},
6.308 +\isaindexbold{div}, \isaindexbold{mod}, \isaindexbold{min} and
6.309 +\isaindexbold{max} are predefined, as are the relations
6.310 +\indexboldpos{\isasymle}{$HOL2arithrel} and
6.311 +\ttindexboldpos{<}{$HOL2arithrel}. There is even a least number operation
6.312 +\isaindexbold{LEAST}. For example, \isa{(LEAST n.$\,$1 < n) = 2}, although
6.313 +Isabelle does not prove this completely automatically. Note that \isa{1} and
6.314 +\isa{2} are available as abbreviations for the corresponding
6.315 +\isa{Suc}-expressions. If you need the full set of numerals,
6.316 +see~\S\ref{nat-numerals}.
6.317 +
6.318 +\begin{warn}
6.319 + The operations \ttindexboldpos{+}{$HOL2arithfun},
6.320 + \ttindexboldpos{-}{$HOL2arithfun}, \ttindexboldpos{*}{$HOL2arithfun},
6.321 + \isaindexbold{min}, \isaindexbold{max},
6.322 + \indexboldpos{\isasymle}{$HOL2arithrel} and
6.323 + \ttindexboldpos{<}{$HOL2arithrel} are overloaded, i.e.\ they are available
6.324 + not just for natural numbers but at other types as well (see
6.325 + \S\ref{sec:TypeClasses}). For example, given the goal \isa{x+y = y+x},
6.326 + there is nothing to indicate that you are talking about natural numbers.
6.327 + Hence Isabelle can only infer that \isa{x} and \isa{y} are of some
6.328 + arbitrary type where \isa{+} is declared. As a consequence, you will be
6.329 + unable to prove the goal (although it may take you some time to realize
6.330 + what has happened if \texttt{show_types} is not set). In this particular
6.331 + example, you need to include an explicit type constraint, for example
6.332 + \isa{x+y = y+(x::nat)}. If there is enough contextual information this may
6.333 + not be necessary: \isa{x+0 = x} automatically implies \isa{x::nat}.
6.334 +\end{warn}
6.335 +
6.336 +Simple arithmetic goals are proved automatically by both \isa{auto}
6.337 +and the simplification methods introduced in \S\ref{sec:Simplification}. For
6.338 +example,
6.339 +
6.340 +\input{Misc/document/arith1.tex}%
6.341 +is proved automatically. The main restriction is that only addition is taken
6.342 +into account; other arithmetic operations and quantified formulae are ignored.
6.343 +
6.344 +For more complex goals, there is the special method
6.345 +\isaindexbold{arith} (which attacks the first subgoal). It proves
6.346 +arithmetic goals involving the usual logical connectives (\isasymnot,
6.347 +\isasymand, \isasymor, \isasymimp), the relations \isasymle\ and \isa{<}, and
6.348 +the operations \isa{+}, \isa{-}, \isa{min} and \isa{max}. For example,
6.349 +
6.350 +\input{Misc/document/arith2.tex}%
6.351 +succeeds because \isa{k*k} can be treated as atomic.
6.352 +In contrast,
6.353 +
6.354 +\input{Misc/document/arith3.tex}%
6.355 +is not even proved by \isa{arith} because the proof relies essentially
6.356 +on properties of multiplication.
6.357 +
6.358 +\begin{warn}
6.359 + The running time of \isa{arith} is exponential in the number of occurrences
6.360 + of \ttindexboldpos{-}{$HOL2arithfun}, \isaindexbold{min} and
6.361 + \isaindexbold{max} because they are first eliminated by case distinctions.
6.362 +
6.363 + \isa{arith} is incomplete even for the restricted class of formulae
6.364 + described above (known as ``linear arithmetic''). If divisibility plays a
6.365 + role, it may fail to prove a valid formula, for example $m+m \neq n+n+1$.
6.366 + Fortunately, such examples are rare in practice.
6.367 +\end{warn}
6.368 +
6.369 +\index{arithmetic|)}
6.370 +
6.371 +
6.372 +\subsection{Products}
6.373 +
6.374 +HOL also has pairs: \isa{($a@1$,$a@2$)} is of type \texttt{$\tau@1$ *
6.375 + $\tau@2$} provided each $a@i$ is of type $\tau@i$. The components of a pair
6.376 +are extracted by \isa{fst} and \isa{snd}: \isa{fst($x$,$y$) = $x$} and
6.377 +\isa{snd($x$,$y$) = $y$}. Tuples are simulated by pairs nested to the right:
6.378 +\isa{($a@1$,$a@2$,$a@3$)} stands for \isa{($a@1$,($a@2$,$a@3$))} and
6.379 +\isa{$\tau@1$ * $\tau@2$ * $\tau@3$} for \isa{$\tau@1$ * ($\tau@2$ *
6.380 + $\tau@3$)}. Therefore we have \isa{fst(snd($a@1$,$a@2$,$a@3$)) = $a@2$}.
6.381 +
6.382 +It is possible to use (nested) tuples as patterns in abstractions, for
6.383 +example \isa{\isasymlambda(x,y,z).x+y+z} and
6.384 +\isa{\isasymlambda((x,y),z).x+y+z}.
6.385 +In addition to explicit $\lambda$-abstractions, tuple patterns can be used in
6.386 +most variable binding constructs. Typical examples are
6.387 +
6.388 +\input{Misc/document/pairs.tex}%
6.389 +Further important examples are quantifiers and sets (see~\S\ref{quant-pats}).
6.390 +
6.391 +%FIXME move stuff below into section on proofs about products?
6.392 +\begin{warn}
6.393 + Abstraction over pairs and tuples is merely a convenient shorthand for a
6.394 + more complex internal representation. Thus the internal and external form
6.395 + of a term may differ, which can affect proofs. If you want to avoid this
6.396 + complication, use \isa{fst} and \isa{snd}, i.e.\ write
6.397 + \isa{\isasymlambda{}p.~fst p + snd p} instead of
6.398 + \isa{\isasymlambda(x,y).~x + y}. See~\S\ref{proofs-about-products} for
6.399 + theorem proving with tuple patterns.
6.400 +\end{warn}
6.401 +
6.402 +Finally note that products, like natural numbers, are datatypes, which means
6.403 +in particular that \isa{induct_tac} and \isa{case_tac} are applicable to
6.404 +products (see \S\ref{proofs-about-products}).
6.405 +
6.406 +\section{Definitions}
6.407 +\label{sec:Definitions}
6.408 +
6.409 +A definition is simply an abbreviation, i.e.\ a new name for an existing
6.410 +construction. In particular, definitions cannot be recursive. Isabelle offers
6.411 +definitions on the level of types and terms. Those on the type level are
6.412 +called type synonyms, those on the term level are called (constant)
6.413 +definitions.
6.414 +
6.415 +
6.416 +\subsection{Type synonyms}
6.417 +\indexbold{type synonyms}
6.418 +
6.419 +Type synonyms are similar to those found in ML. Their syntax is fairly self
6.420 +explanatory:
6.421 +
6.422 +\input{Misc/document/types.tex}%
6.423 +
6.424 +Note that pattern-matching is not allowed, i.e.\ each definition must be of
6.425 +the form $f\,x@1\,\dots\,x@n~\isasymequiv~t$.
6.426 +
6.427 +Section~\S\ref{sec:Simplification} explains how definitions are used
6.428 +in proofs.
6.429 +
6.430 +\begin{warn}%
6.431 +A common mistake when writing definitions is to introduce extra free
6.432 +variables on the right-hand side as in the following fictitious definition:
6.433 +\input{Misc/document/prime_def.tex}%
6.434 +\end{warn}
6.435 +
6.436 +
6.437 +\chapter{More Functional Programming}
6.438 +
6.439 +The purpose of this chapter is to deepen the reader's understanding of the
6.440 +concepts encountered so far and to introduce an advanced forms of datatypes
6.441 +and recursive functions. The first two sections give a structured
6.442 +presentation of theorem proving by simplification
6.443 +(\S\ref{sec:Simplification}) and discuss important heuristics for induction
6.444 +(\S\ref{sec:InductionHeuristics}). They can be skipped by readers less
6.445 +interested in proofs. They are followed by a case study, a compiler for
6.446 +expressions (\S\ref{sec:ExprCompiler}). Advanced datatypes, including those
6.447 +involving function spaces, are covered in \S\ref{sec:advanced-datatypes},
6.448 +which closes with another case study, search trees (``tries''). Finally we
6.449 +introduce a very general form of recursive function definition which goes
6.450 +well beyond what \isacommand{primrec} allows (\S\ref{sec:recdef}).
6.451 +
6.452 +
6.453 +\section{Simplification}
6.454 +\label{sec:Simplification}
6.455 +\index{simplification|(}
6.456 +
6.457 +So far we have proved our theorems by \isa{auto}, which ``simplifies'' all
6.458 +subgoals. In fact, \isa{auto} can do much more than that, except that it
6.459 +did not need to so far. However, when you go beyond toy examples, you need to
6.460 +understand the ingredients of \isa{auto}. This section covers the method
6.461 +that \isa{auto} always applies first, namely simplification.
6.462 +
6.463 +Simplification is one of the central theorem proving tools in Isabelle and
6.464 +many other systems. The tool itself is called the \bfindex{simplifier}. The
6.465 +purpose of this section is twofold: to introduce the many features of the
6.466 +simplifier (\S\ref{sec:SimpFeatures}) and to explain a little bit how the
6.467 +simplifier works (\S\ref{sec:SimpHow}). Anybody intending to use HOL should
6.468 +read \S\ref{sec:SimpFeatures}, and the serious student should read
6.469 +\S\ref{sec:SimpHow} as well in order to understand what happened in case
6.470 +things do not simplify as expected.
6.471 +
6.472 +
6.473 +\subsection{Using the simplifier}
6.474 +\label{sec:SimpFeatures}
6.475 +
6.476 +In its most basic form, simplification means repeated application of
6.477 +equations from left to right. For example, taking the rules for \isa{\at}
6.478 +and applying them to the term \isa{[0,1] \at\ []} results in a sequence of
6.479 +simplification steps:
6.480 +\begin{ttbox}\makeatother
6.481 +(0#1#[]) @ [] \(\leadsto\) 0#((1#[]) @ []) \(\leadsto\) 0#(1#([] @ [])) \(\leadsto\) 0#1#[]
6.482 +\end{ttbox}
6.483 +This is also known as \bfindex{term rewriting} and the equations are referred
6.484 +to as \bfindex{rewrite rules}. This is more honest than ``simplification''
6.485 +because the terms do not necessarily become simpler in the process.
6.486 +
6.487 +\subsubsection{Simplification rules}
6.488 +\indexbold{simplification rules}
6.489 +
6.490 +To facilitate simplification, theorems can be declared to be simplification
6.491 +rules (with the help of the attribute \isa{[simp]}\index{*simp
6.492 + (attribute)}), in which case proofs by simplification make use of these
6.493 +rules by default. In addition the constructs \isacommand{datatype} and
6.494 +\isacommand{primrec} (and a few others) invisibly declare useful
6.495 +simplification rules. Explicit definitions are \emph{not} declared
6.496 +simplification rules automatically!
6.497 +
6.498 +Not merely equations but pretty much any theorem can become a simplification
6.499 +rule. The simplifier will try to make sense of it. For example, a theorem
6.500 +\isasymnot$P$ is automatically turned into \isa{$P$ = False}. The details
6.501 +are explained in \S\ref{sec:SimpHow}.
6.502 +
6.503 +The simplification attribute of theorems can be turned on and off as follows:
6.504 +\begin{ttbox}
6.505 +theorems [simp] = \(list of theorem names\);
6.506 +theorems [simp del] = \(list of theorem names\);
6.507 +\end{ttbox}
6.508 +As a rule of thumb, rules that really simplify (like \isa{rev(rev xs) =
6.509 + xs} and \mbox{\isa{xs \at\ [] = xs}}) should be made simplification
6.510 +rules. Those of a more specific nature (e.g.\ distributivity laws, which
6.511 +alter the structure of terms considerably) should only be used selectively,
6.512 +i.e.\ they should not be default simplification rules. Conversely, it may
6.513 +also happen that a simplification rule needs to be disabled in certain
6.514 +proofs. Frequent changes in the simplification status of a theorem may
6.515 +indicates a badly designed theory.
6.516 +\begin{warn}
6.517 + Simplification may not terminate, for example if both $f(x) = g(x)$ and
6.518 + $g(x) = f(x)$ are simplification rules. It is the user's responsibility not
6.519 + to include simplification rules that can lead to nontermination, either on
6.520 + their own or in combination with other simplification rules.
6.521 +\end{warn}
6.522 +
6.523 +\subsubsection{The simplification method}
6.524 +\index{*simp (method)|bold}
6.525 +
6.526 +The general format of the simplification method is
6.527 +\begin{ttbox}
6.528 +simp \(list of modifiers\)
6.529 +\end{ttbox}
6.530 +where the list of \emph{modifiers} helps to fine tune the behaviour and may
6.531 +be empty. Most if not all of the proofs seen so far could have been performed
6.532 +with \isa{simp} instead of \isa{auto}, except that \isa{simp} attacks
6.533 +only the first subgoal and may thus need to be repeated.
6.534 +Note that \isa{simp} fails if nothing changes.
6.535 +
6.536 +\subsubsection{Adding and deleting simplification rules}
6.537 +
6.538 +If a certain theorem is merely needed in a few proofs by simplification,
6.539 +we do not need to make it a global simplification rule. Instead we can modify
6.540 +the set of simplification rules used in a simplification step by adding rules
6.541 +to it and/or deleting rules from it. The two modifiers for this are
6.542 +\begin{ttbox}
6.543 +add: \(list of theorem names\)
6.544 +del: \(list of theorem names\)
6.545 +\end{ttbox}
6.546 +In case you want to use only a specific list of theorems and ignore all
6.547 +others:
6.548 +\begin{ttbox}
6.549 +only: \(list of theorem names\)
6.550 +\end{ttbox}
6.551 +
6.552 +
6.553 +\subsubsection{Assumptions}
6.554 +\index{simplification!with/of assumptions}
6.555 +
6.556 +{\makeatother\input{Misc/document/asm_simp.tex}}
6.557 +
6.558 +\subsubsection{Rewriting with definitions}
6.559 +\index{simplification!with definitions}
6.560 +
6.561 +\input{Misc/document/def_rewr.tex}
6.562 +
6.563 +\begin{warn}
6.564 + If you have defined $f\,x\,y~\isasymequiv~t$ then you can only expand
6.565 + occurrences of $f$ with at least two arguments. Thus it is safer to define
6.566 + $f$~\isasymequiv~\isasymlambda$x\,y.\;t$.
6.567 +\end{warn}
6.568 +
6.569 +\subsubsection{Simplifying let-expressions}
6.570 +\index{simplification!of let-expressions}
6.571 +
6.572 +Proving a goal containing \isaindex{let}-expressions almost invariably
6.573 +requires the \isa{let}-con\-structs to be expanded at some point. Since
6.574 +\isa{let}-\isa{in} is just syntactic sugar for a defined constant (called
6.575 +\isa{Let}), expanding \isa{let}-constructs means rewriting with
6.576 +\isa{Let_def}:
6.577 +
6.578 +{\makeatother\input{Misc/document/let_rewr.tex}}
6.579 +
6.580 +\subsubsection{Conditional equations}
6.581 +
6.582 +\input{Misc/document/cond_rewr.tex}
6.583 +
6.584 +
6.585 +\subsubsection{Automatic case splits}
6.586 +\indexbold{case splits}
6.587 +\index{*split|(}
6.588 +
6.589 +{\makeatother\input{Misc/document/case_splits.tex}}
6.590 +
6.591 +\index{*split|)}
6.592 +
6.593 +\begin{warn}
6.594 + The simplifier merely simplifies the condition of an \isa{if} but not the
6.595 + \isa{then} or \isa{else} parts. The latter are simplified only after the
6.596 + condition reduces to \isa{True} or \isa{False}, or after splitting. The
6.597 + same is true for \isaindex{case}-expressions: only the selector is
6.598 + simplified at first, until either the expression reduces to one of the
6.599 + cases or it is split.
6.600 +\end{warn}
6.601 +
6.602 +\subsubsection{Arithmetic}
6.603 +\index{arithmetic}
6.604 +
6.605 +The simplifier routinely solves a small class of linear arithmetic formulae
6.606 +(over types \isa{nat} and \isa{int}): it only takes into account
6.607 +assumptions and conclusions that are (possibly negated) (in)equalities
6.608 +(\isa{=}, \isasymle, \isa{<}) and it only knows about addition. Thus
6.609 +
6.610 +\input{Misc/document/arith1.tex}%
6.611 +is proved by simplification, whereas the only slightly more complex
6.612 +
6.613 +\input{Misc/document/arith4.tex}%
6.614 +is not proved by simplification and requires \isa{arith}.
6.615 +
6.616 +\subsubsection{Permutative rewrite rules}
6.617 +
6.618 +A rewrite rule is {\bf permutative} if the left-hand side and right-hand side
6.619 +are the same up to renaming of variables. The most common permutative rule
6.620 +is commutativity: $x+y = y+x$. Another example is $(x-y)-z = (x-z)-y$. Such
6.621 +rules are problematic because once they apply, they can be used forever.
6.622 +The simplifier is aware of this danger and treats permutative rules
6.623 +separately. For details see~\cite{isabelle-ref}.
6.624 +
6.625 +\subsubsection{Tracing}
6.626 +\indexbold{tracing the simplifier}
6.627 +
6.628 +{\makeatother\input{Misc/document/trace_simp.tex}}
6.629 +
6.630 +\subsection{How it works}
6.631 +\label{sec:SimpHow}
6.632 +
6.633 +\subsubsection{Higher-order patterns}
6.634 +
6.635 +\subsubsection{Local assumptions}
6.636 +
6.637 +\subsubsection{The preprocessor}
6.638 +
6.639 +\index{simplification|)}
6.640 +
6.641 +\section{Induction heuristics}
6.642 +\label{sec:InductionHeuristics}
6.643 +
6.644 +The purpose of this section is to illustrate some simple heuristics for
6.645 +inductive proofs. The first one we have already mentioned in our initial
6.646 +example:
6.647 +\begin{quote}
6.648 +{\em 1. Theorems about recursive functions are proved by induction.}
6.649 +\end{quote}
6.650 +In case the function has more than one argument
6.651 +\begin{quote}
6.652 +{\em 2. Do induction on argument number $i$ if the function is defined by
6.653 +recursion in argument number $i$.}
6.654 +\end{quote}
6.655 +When we look at the proof of {\makeatother\isa{(xs @ ys) @ zs = xs @ (ys @
6.656 + zs)}} in \S\ref{sec:intro-proof} we find (a) \isa{\at} is recursive in
6.657 +the first argument, (b) \isa{xs} occurs only as the first argument of
6.658 +\isa{\at}, and (c) both \isa{ys} and \isa{zs} occur at least once as
6.659 +the second argument of \isa{\at}. Hence it is natural to perform induction
6.660 +on \isa{xs}.
6.661 +
6.662 +The key heuristic, and the main point of this section, is to
6.663 +generalize the goal before induction. The reason is simple: if the goal is
6.664 +too specific, the induction hypothesis is too weak to allow the induction
6.665 +step to go through. Let us now illustrate the idea with an example.
6.666 +
6.667 +{\makeatother\input{Misc/document/Itrev.tex}}
6.668 +
6.669 +A final point worth mentioning is the orientation of the equation we just
6.670 +proved: the more complex notion (\isa{itrev}) is on the left-hand
6.671 +side, the simpler \isa{rev} on the right-hand side. This constitutes
6.672 +another, albeit weak heuristic that is not restricted to induction:
6.673 +\begin{quote}
6.674 + {\em 5. The right-hand side of an equation should (in some sense) be
6.675 + simpler than the left-hand side.}
6.676 +\end{quote}
6.677 +The heuristic is tricky to apply because it is not obvious that
6.678 +\isa{rev xs \at\ ys} is simpler than \isa{itrev xs ys}. But see what
6.679 +happens if you try to prove the symmetric equation!
6.680 +
6.681 +
6.682 +\section{Case study: compiling expressions}
6.683 +\label{sec:ExprCompiler}
6.684 +
6.685 +{\makeatother\input{CodeGen/document/CodeGen.tex}}
6.686 +
6.687 +
6.688 +\section{Advanced datatypes}
6.689 +\label{sec:advanced-datatypes}
6.690 +\index{*datatype|(}
6.691 +\index{*primrec|(}
6.692 +%|)
6.693 +
6.694 +This section presents advanced forms of \isacommand{datatype}s.
6.695 +
6.696 +\subsection{Mutual recursion}
6.697 +\label{sec:datatype-mut-rec}
6.698 +
6.699 +\input{Datatype/document/ABexpr.tex}
6.700 +
6.701 +\subsection{Nested recursion}
6.702 +
6.703 +\input{Datatype/document/Nested.tex}
6.704 +
6.705 +
6.706 +\subsection{The limits of nested recursion}
6.707 +
6.708 +How far can we push nested recursion? By the unfolding argument above, we can
6.709 +reduce nested to mutual recursion provided the nested recursion only involves
6.710 +previously defined datatypes. This does not include functions:
6.711 +\begin{ttbox}
6.712 +datatype t = C (t => bool)
6.713 +\end{ttbox}
6.714 +is a real can of worms: in HOL it must be ruled out because it requires a type
6.715 +\isa{t} such that \isa{t} and its power set \isa{t \isasymFun\ bool} have the
6.716 +same cardinality---an impossibility. For the same reason it is not possible
6.717 +to allow recursion involving the type \isa{set}, which is isomorphic to
6.718 +\isa{t \isasymFun\ bool}.
6.719 +
6.720 +Fortunately, a limited form of recursion
6.721 +involving function spaces is permitted: the recursive type may occur on the
6.722 +right of a function arrow, but never on the left. Hence the above can of worms
6.723 +is ruled out but the following example of a potentially infinitely branching tree is
6.724 +accepted:
6.725 +
6.726 +\input{Datatype/document/Fundata.tex}
6.727 +\bigskip
6.728 +
6.729 +If you need nested recursion on the left of a function arrow,
6.730 +there are alternatives to pure HOL: LCF~\cite{paulson87} is a logic where types like
6.731 +\begin{ttbox}
6.732 +datatype lam = C (lam -> lam)
6.733 +\end{ttbox}
6.734 +do indeed make sense (note the intentionally different arrow \isa{->}!).
6.735 +There is even a version of LCF on top of HOL, called
6.736 +HOLCF~\cite{MuellerNvOS99}.
6.737 +
6.738 +\index{*primrec|)}
6.739 +\index{*datatype|)}
6.740 +
6.741 +\subsection{Case study: Tries}
6.742 +
6.743 +Tries are a classic search tree data structure~\cite{Knuth3-75} for fast
6.744 +indexing with strings. Figure~\ref{fig:trie} gives a graphical example of a
6.745 +trie containing the words ``all'', ``an'', ``ape'', ``can'', ``car'' and
6.746 +``cat''. When searching a string in a trie, the letters of the string are
6.747 +examined sequentially. Each letter determines which subtrie to search next.
6.748 +In this case study we model tries as a datatype, define a lookup and an
6.749 +update function, and prove that they behave as expected.
6.750 +
6.751 +\begin{figure}[htbp]
6.752 +\begin{center}
6.753 +\unitlength1mm
6.754 +\begin{picture}(60,30)
6.755 +\put( 5, 0){\makebox(0,0)[b]{l}}
6.756 +\put(25, 0){\makebox(0,0)[b]{e}}
6.757 +\put(35, 0){\makebox(0,0)[b]{n}}
6.758 +\put(45, 0){\makebox(0,0)[b]{r}}
6.759 +\put(55, 0){\makebox(0,0)[b]{t}}
6.760 +%
6.761 +\put( 5, 9){\line(0,-1){5}}
6.762 +\put(25, 9){\line(0,-1){5}}
6.763 +\put(44, 9){\line(-3,-2){9}}
6.764 +\put(45, 9){\line(0,-1){5}}
6.765 +\put(46, 9){\line(3,-2){9}}
6.766 +%
6.767 +\put( 5,10){\makebox(0,0)[b]{l}}
6.768 +\put(15,10){\makebox(0,0)[b]{n}}
6.769 +\put(25,10){\makebox(0,0)[b]{p}}
6.770 +\put(45,10){\makebox(0,0)[b]{a}}
6.771 +%
6.772 +\put(14,19){\line(-3,-2){9}}
6.773 +\put(15,19){\line(0,-1){5}}
6.774 +\put(16,19){\line(3,-2){9}}
6.775 +\put(45,19){\line(0,-1){5}}
6.776 +%
6.777 +\put(15,20){\makebox(0,0)[b]{a}}
6.778 +\put(45,20){\makebox(0,0)[b]{c}}
6.779 +%
6.780 +\put(30,30){\line(-3,-2){13}}
6.781 +\put(30,30){\line(3,-2){13}}
6.782 +\end{picture}
6.783 +\end{center}
6.784 +\caption{A sample trie}
6.785 +\label{fig:trie}
6.786 +\end{figure}
6.787 +
6.788 +Proper tries associate some value with each string. Since the
6.789 +information is stored only in the final node associated with the string, many
6.790 +nodes do not carry any value. This distinction is captured by the
6.791 +following predefined datatype (from theory \texttt{Option}, which is a parent
6.792 +of \texttt{Main}):
6.793 +\input{Trie/document/Option2.tex}
6.794 +\indexbold{*option}\indexbold{*None}\indexbold{*Some}
6.795 +
6.796 +\input{Trie/document/Trie.tex}
6.797 +
6.798 +\begin{exercise}
6.799 + Write an improved version of \isa{update} that does not suffer from the
6.800 + space leak in the version above. Prove the main theorem for your improved
6.801 + \isa{update}.
6.802 +\end{exercise}
6.803 +
6.804 +\begin{exercise}
6.805 + Write a function to \emph{delete} entries from a trie. An easy solution is
6.806 + a clever modification of \isa{update} which allows both insertion and
6.807 + deletion with a single function. Prove (a modified version of) the main
6.808 + theorem above. Optimize you function such that it shrinks tries after
6.809 + deletion, if possible.
6.810 +\end{exercise}
6.811 +
6.812 +\section{Total recursive functions}
6.813 +\label{sec:recdef}
6.814 +\index{*recdef|(}
6.815 +
6.816 +Although many total functions have a natural primitive recursive definition,
6.817 +this is not always the case. Arbitrary total recursive functions can be
6.818 +defined by means of \isacommand{recdef}: you can use full pattern-matching,
6.819 +recursion need not involve datatypes, and termination is proved by showing
6.820 +that the arguments of all recursive calls are smaller in a suitable (user
6.821 +supplied) sense.
6.822 +
6.823 +\subsection{Defining recursive functions}
6.824 +
6.825 +\input{Recdef/document/examples.tex}
6.826 +
6.827 +\subsection{Proving termination}
6.828 +
6.829 +\input{Recdef/document/termination.tex}
6.830 +
6.831 +\subsection{Simplification with recdef}
6.832 +
6.833 +\input{Recdef/document/simplification.tex}
6.834 +
6.835 +
6.836 +\subsection{Induction}
6.837 +\index{induction!recursion|(}
6.838 +\index{recursion induction|(}
6.839 +
6.840 +\input{Recdef/document/Induction.tex}
6.841 +
6.842 +\index{induction!recursion|)}
6.843 +\index{recursion induction|)}
6.844 +\index{*recdef|)}
7.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
7.2 +++ b/doc-src/TutorialI/ttbox.sty Wed Apr 19 11:54:39 2000 +0200
7.3 @@ -0,0 +1,20 @@
7.4 +\ProvidesPackage{ttbox}[1997/06/25]
7.5 +\RequirePackage{alltt}
7.6 +
7.7 +%%%Boxed terminal sessions
7.8 +
7.9 +%Redefines \{ and \} to be in \tt font and \| to make a BACKSLASH
7.10 +\def\ttbraces{\chardef\{=`\{\chardef\}=`\}\chardef\|=`\\}
7.11 +
7.12 +%Restores % as the comment character (especially, to suppress line breaks)
7.13 +\newcommand\comments{\catcode`\%=14\relax}
7.14 +
7.15 +%alltt* environment: like alltt but smaller, and with \{ \} and \| as in ttbox
7.16 +\newenvironment{alltt*}{\begin{alltt}\footnotesize\ttbraces}{\end{alltt}}
7.17 +
7.18 +%Indented alltt* environment with small point size
7.19 +%NO LINE BREAKS are allowed unless \pagebreak appears at START of a line
7.20 +\newenvironment{ttbox}{\begin{quote}\samepage\begin{alltt*}}%
7.21 + {\end{alltt*}\end{quote}}
7.22 +
7.23 +\endinput
8.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
8.2 +++ b/doc-src/TutorialI/tutorial.tex Wed Apr 19 11:54:39 2000 +0200
8.3 @@ -0,0 +1,78 @@
8.4 +\documentclass[11pt,a4paper]{report}
8.5 +\usepackage{isabelle,isabellesym,pdfsetup}
8.6 +\usepackage{latexsym,verbatim,graphicx,../iman,extra,comment}
8.7 +
8.8 +\usepackage{ttbox}
8.9 +\newcommand\ttbreak{\vskip-10pt\pagebreak[0]}
8.10 +\newcommand\Out[1]{\texttt{\textsl{#1}}} %% for output from terminal sessions
8.11 +
8.12 +%\newtheorem{theorem}{Theorem}[section]
8.13 +\newtheorem{Exercise}{Exercise}[section]
8.14 +\newenvironment{exercise}{\begin{Exercise}\rm}{\end{Exercise}}
8.15 +\newcommand{\ttlbr}{\texttt{[|}}
8.16 +\newcommand{\ttrbr}{\texttt{|]}}
8.17 +\newcommand{\ttor}{\texttt{|}}
8.18 +\newcommand{\ttall}{\texttt{!}}
8.19 +\newcommand{\ttuniquex}{\texttt{?!}}
8.20 +\newcommand{\ttEXU}{\texttt{EX!}}
8.21 +\newcommand{\ttAnd}{\texttt{!!}}
8.22 +
8.23 +\newcommand{\isasymimp}{\isasymlongrightarrow}
8.24 +\newcommand{\isasymImp}{\isasymLongrightarrow}
8.25 +\newcommand{\isasymFun}{\isasymRightarrow}
8.26 +\newcommand{\isasymuniqex}{\emph{$\exists!\,$}}
8.27 +
8.28 +\newenvironment{isabellepar}%
8.29 +{\par\medskip\noindent\begin{isabelle}}{\end{isabelle}\medskip\par\noindent}
8.30 +
8.31 +\renewenvironment{isamarkuptxt}{\begin{isamarkuptext}}{\end{isamarkuptext}}
8.32 +
8.33 +%%% to index derived rls: ^\([a-zA-Z0-9][a-zA-Z0-9_]*\) \\tdx{\1}
8.34 +%%% to index rulenames: ^ *(\([a-zA-Z0-9][a-zA-Z0-9_]*\), \\tdx{\1}
8.35 +%%% to index constants: \\tt \([a-zA-Z0-9][a-zA-Z0-9_]*\) \\cdx{\1}
8.36 +%%% to deverbify: \\verb|\([^|]*\)| \\ttindex{\1}
8.37 +%% run ../sedindex logics to prepare index file
8.38 +
8.39 +\makeindex
8.40 +\newcommand{\indexboldpos}[2]{#1\indexbold{#2@#1}}
8.41 +\newcommand{\ttindexboldpos}[2]{\texttt{#1}\indexbold{#2@\texttt{#1}}}
8.42 +\newcommand{\isaindexbold}[1]{\isa{#1}\index{*#1|bold}}
8.43 +\newcommand{\isaindex}[1]{\isa{#1}\index{*#1}}
8.44 +
8.45 +\underscoreoff
8.46 +
8.47 +\setcounter{secnumdepth}{2} \setcounter{tocdepth}{2} %% {secnumdepth}{2}???
8.48 +
8.49 +\pagestyle{headings}
8.50 +%\sloppy
8.51 +%\binperiod %%%treat . like a binary operator
8.52 +
8.53 +\begin{document}
8.54 +\title{\includegraphics[scale=.8]{isabelle_hol}
8.55 + \\ \vspace{0.5cm} The Tutorial
8.56 + \\ --- DRAFT ---}
8.57 +\author{Tobias Nipkow\\
8.58 +Technische Universit\"at M\"unchen \\
8.59 +Institut f\"ur Informatik \\
8.60 +\url{http://www.in.tum.de/~nipkow/}}
8.61 +\maketitle
8.62 +
8.63 +\pagenumbering{roman}
8.64 +\tableofcontents
8.65 +
8.66 +\subsubsection*{Acknowledgements}
8.67 +This tutorial owes a lot to the constant discussions with and the valuable
8.68 +feedback from Larry Paulson and the Isabelle group at Munich: Olaf M\"uller,
8.69 +Wolfgang Naraschewski, David von Oheimb, Leonor Prensa Nieto, Cornelia Pusch
8.70 +and Markus Wenzel. Stefan Berghofer and Stephan Merz were also kind enough to
8.71 +read and comment on a draft version.
8.72 +\clearfirst
8.73 +
8.74 +\input{basics}
8.75 +\input{fp}
8.76 +\input{appendix}
8.77 +
8.78 +\bibliographystyle{plain}
8.79 +\bibliography{../manual}
8.80 +\input{tutorial.ind}
8.81 +\end{document}