author | nipkow |

Wed Apr 19 11:54:39 2000 +0200 (2000-04-19) | |

changeset 8743 | 3253c6046d57 |

parent 8742 | 8a5b3f58b944 |

child 8744 | 22fa8b16c3ae |

I wonder if that's all?

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}