# HG changeset patch # User nipkow # Date 956138079 -7200 # Node ID 3253c6046d57555f6488ad6c0fae0ff4fbbf2788 # Parent 8a5b3f58b944079d17eb234d9037916732bdfd6f I wonder if that's all? diff -r 8a5b3f58b944 -r 3253c6046d57 doc-src/TutorialI/IsaMakefile --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/doc-src/TutorialI/IsaMakefile Wed Apr 19 11:54:39 2000 +0200 @@ -0,0 +1,104 @@ +# +# IsaMakefile for Tutorial +# + +## targets + +default: styles HOL-ToyList HOL-Ifexpr HOL-CodeGen HOL-Trie HOL-Datatype HOL-Recdef HOL-Misc + + +## global settings + +SRC = $(ISABELLE_HOME)/src +OUT = $(ISABELLE_OUTPUT) +LOG = $(OUT)/log + + +## HOL + +HOL: + @cd $(SRC)/HOL; $(ISATOOL) make HOL + +styles: isabelle.sty isabellesym.sty pdfsetup.sty + +isabelle.sty: $(ISABELLE_HOME)/lib/texinputs/isabelle.sty + cp $(ISABELLE_HOME)/lib/texinputs/isabelle.sty . + +isabellesym.sty: $(ISABELLE_HOME)/lib/texinputs/isabellesym.sty + cp $(ISABELLE_HOME)/lib/texinputs/isabellesym.sty . + +pdfsetup.sty: $(ISABELLE_HOME)/lib/texinputs/pdfsetup.sty + cp $(ISABELLE_HOME)/lib/texinputs/pdfsetup.sty . + + +## HOL-Ifexpr + +HOL-Ifexpr: HOL $(LOG)/HOL-Ifexpr.gz + +$(LOG)/HOL-Ifexpr.gz: $(OUT)/HOL Ifexpr/Ifexpr.thy Ifexpr/ROOT.ML + @$(ISATOOL) usedir -i true -d dvi -D document $(OUT)/HOL Ifexpr + + +## HOL-ToyList + +HOL-ToyList: HOL $(LOG)/HOL-ToyList.gz $(LOG)/HOL-ToyList2.gz + +ToyList2/ToyList.thy: ToyList2/ToyList1 ToyList2/ToyList2 + cat ToyList2/ToyList1 ToyList2/ToyList2 > ToyList2/ToyList.thy + +$(LOG)/HOL-ToyList2.gz: $(OUT)/HOL ToyList2/ToyList.thy ToyList2/ROOT.ML + @$(ISATOOL) usedir -i true -d dvi -D document $(OUT)/HOL ToyList2 + +$(LOG)/HOL-ToyList.gz: $(OUT)/HOL ToyList/ToyList.thy ToyList/ROOT.ML + @$(ISATOOL) usedir -i true -d dvi -D document $(OUT)/HOL ToyList + +## HOL-CodeGen + +HOL-CodeGen: HOL $(LOG)/HOL-CodeGen.gz + +$(LOG)/HOL-CodeGen.gz: $(OUT)/HOL CodeGen/CodeGen.thy + @$(ISATOOL) usedir -i true -d dvi -D document $(OUT)/HOL CodeGen + + +## HOL-Datatype + +HOL-Datatype: HOL $(LOG)/HOL-Datatype.gz + +$(LOG)/HOL-Datatype.gz: $(OUT)/HOL Datatype/ROOT.ML Datatype/ABexpr.thy Datatype/Nested.thy \ + Datatype/Fundata.thy + @$(ISATOOL) usedir -i true -d dvi -D document $(OUT)/HOL Datatype + + +## HOL-Trie + +HOL-Trie: HOL $(LOG)/HOL-Trie.gz + +$(LOG)/HOL-Trie.gz: $(OUT)/HOL Trie/Option2.thy Trie/Trie.thy + @$(ISATOOL) usedir -i true -d dvi -D document $(OUT)/HOL Trie + + +## HOL-Recdef + +HOL-Recdef: HOL $(LOG)/HOL-Recdef.gz + +$(LOG)/HOL-Recdef.gz: $(OUT)/HOL Recdef/examples.thy Recdef/termination.thy \ + Recdef/simplification.thy Recdef/Induction.thy + @$(ISATOOL) usedir -i true -d dvi -D document $(OUT)/HOL Recdef + + +## HOL-Misc + +HOL-Misc: HOL $(LOG)/HOL-Misc.gz + +$(LOG)/HOL-Misc.gz: $(OUT)/HOL Misc/ROOT.ML Misc/Tree.thy Misc/cases.thy \ + Misc/fakenat.thy Misc/natsum.thy Misc/pairs.thy Misc/types.thy Misc/prime_def.thy \ + Misc/arith1.thy Misc/arith2.thy Misc/arith3.thy Misc/arith4.thy \ + Misc/def_rewr.thy Misc/let_rewr.thy Misc/cond_rewr.thy Misc/case_splits.thy \ + Misc/trace_simp.thy Misc/Itrev.thy Misc/asm_simp.thy + @$(ISATOOL) usedir -i true -d dvi -D document $(OUT)/HOL Misc + + +## clean + +clean: + @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 diff -r 8a5b3f58b944 -r 3253c6046d57 doc-src/TutorialI/Makefile --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/doc-src/TutorialI/Makefile Wed Apr 19 11:54:39 2000 +0200 @@ -0,0 +1,39 @@ +# +# $Id$ +# + +## targets + +default: dvi + + +## dependencies + +include ../Makefile.in + +NAME = tutorial +FILES = tutorial.tex basics.tex fp.tex appendix.tex \ + ../iman.sty ttbox.sty extra.sty + +dvi: $(NAME).dvi + +$(NAME).dvi: $(FILES) isabelle_hol.eps + touch $(NAME).ind + $(LATEX) $(NAME) + $(BIBTEX) $(NAME) + $(LATEX) $(NAME) + $(LATEX) $(NAME) + $(SEDINDEX) $(NAME) + $(LATEX) $(NAME) + +pdf: $(NAME).pdf + +$(NAME).pdf: $(FILES) isabelle_hol.pdf + touch $(NAME).ind + $(PDFLATEX) $(NAME) + $(BIBTEX) $(NAME) + $(PDFLATEX) $(NAME) + $(PDFLATEX) $(NAME) + $(SEDINDEX) $(NAME) + $(FIXBOOKMARKS) $(NAME).out + $(PDFLATEX) $(NAME) diff -r 8a5b3f58b944 -r 3253c6046d57 doc-src/TutorialI/appendix.tex --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/doc-src/TutorialI/appendix.tex Wed Apr 19 11:54:39 2000 +0200 @@ -0,0 +1,162 @@ +\appendix + +\chapter{Appendix} +\label{sec:Appendix} + +\begin{figure}[htbp] +\begin{center} +\begin{tabular}{|ccccccccccc|} +\hline +\indexboldpos{\isasymand}{$HOL0and} & +\indexboldpos{\isasymor}{$HOL0or} & +\indexboldpos{\isasymimp}{$HOL0imp} & +\indexboldpos{\isasymnot}{$HOL0not} & +\indexboldpos{\isasymnoteq}{$HOL0noteq} & +\indexboldpos{\isasymforall}{$HOL0All} & +\isasymforall & +\indexboldpos{\isasymexists}{$HOL0Ex} & +\isasymexists & +\isasymuniqex\index{$HOL0ExU@\isasymuniqex|bold} & +\isasymuniqex \\ +\texttt{\&}\indexbold{$HOL0and@{\texttt{\&}}} & +\texttt{|}\index{$HOL0or@\ttor|bold} & +\ttindexboldpos{-->}{$HOL0imp} & +\verb$~$\index{$HOL0not@\verb$~$|bold} & +\verb$~=$\index{$HOL0noteq@\verb$~=$|bold} & +\ttindexbold{ALL} & +\texttt{!}\index{$HOL0All@\ttall|bold} & +\ttindexbold{EX} & +\texttt{?}\index{$HOL0Ex@\texttt{?}|bold} & +\ttEXU\index{EXX@\ttEXU|bold} & +\ttuniquex\index{$HOL0ExU@\ttuniquex|bold}\\ +\hline\hline +\indexboldpos{\isasymlbrakk}{$Isabrl} & +\indexboldpos{\isasymrbrakk}{$Isabrr} & +\indexboldpos{\isasymImp}{$IsaImp} & +\indexboldpos{\isasymAnd}{$IsaAnd} & +\indexboldpos{\isasymequiv}{$IsaEq} & +\indexboldpos{\isasymlambda}{$Isalam} & +\indexboldpos{\isasymFun}{$IsaFun}& +& +& +& +\\ +\texttt{[|}\index{$Isabrl@\ttlbr|bold} & +\texttt{|]}\index{$Isabrr@\ttrbr|bold} & +\ttindexboldpos{==>}{$IsaImp} & +\texttt{!!}\index{$IsaAnd@\ttAnd|bold} & +\ttindexboldpos{==}{$IsaEq} & +\texttt{\%}\indexbold{$Isalam@\texttt{\%}} & +\ttindexboldpos{=>}{$IsaFun}& +& +& +& + \\ +\hline\hline +\indexboldpos{\isasymcirc}{$HOL1} & +\indexboldpos{\isasymle}{$HOL2arithrel}& +& +& +& +& +& +& +& +& + \\ +\ttindexbold{o} & +\ttindexboldpos{<=}{$HOL2arithrel}& +& +& +& +& +& +& +& +& +\\ +\hline +\end{tabular} +\end{center} +\caption{Mathematical symbols and their ASCII-equivalents} +\label{fig:ascii} +\end{figure} + +\begin{figure}[htbp] +\begin{center} +\begin{tabular}{|lllll|} +\hline +\texttt{and} & +\texttt{arities} & +\texttt{assumes} & +\texttt{axclass} & +\texttt{binder} \\ +\texttt{classes} & +\texttt{constdefs} & +\texttt{consts} & +\texttt{default} & +\texttt{defines} \\ +\texttt{defs} & +\texttt{end} & +\texttt{fixes} & +\texttt{global} & +\texttt{inductive} \\ +\texttt{infixl} & +\texttt{infixr} & +\texttt{instance} & +\texttt{local} & +\texttt{locale} \\ +\texttt{mixfix} & +\texttt{ML} & +\texttt{MLtext} & +\texttt{nonterminals} & +\texttt{oracle} \\ +\texttt{output} & +\texttt{path} & +\texttt{primrec} & +\texttt{rules} & +\texttt{setup} \\ +\texttt{syntax} & +\texttt{translations} & +\texttt{typedef} & +\texttt{types} &\\ +\hline +\end{tabular} +\end{center} +\caption{Keywords in theory files} +\label{fig:keywords} +\end{figure} + +\begin{figure}[htbp] +\begin{center} +\begin{tabular}{|lllll|} +\hline +\texttt{ALL} & +\texttt{case} & +\texttt{div} & +\texttt{dvd} & +\texttt{else} \\ +\texttt{EX} & +\texttt{if} & +\texttt{in} & +\texttt{INT} & +\texttt{Int} \\ +\texttt{LEAST} & +\texttt{let} & +\texttt{mod} & +\texttt{O} & +\texttt{o} \\ +\texttt{of} & +\texttt{op} & +\texttt{PROP} & +\texttt{SIGMA} & +\texttt{then} \\ +\texttt{Times} & +\texttt{UN} & +\texttt{Un} &&\\ +\hline +\end{tabular} +\end{center} +\caption{Reserved words in HOL} +\label{fig:ReservedWords} +\end{figure} diff -r 8a5b3f58b944 -r 3253c6046d57 doc-src/TutorialI/basics.tex --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/doc-src/TutorialI/basics.tex Wed Apr 19 11:54:39 2000 +0200 @@ -0,0 +1,302 @@ +\chapter{Basic Concepts} + +\section{Introduction} + +This is a tutorial on how to use Isabelle/HOL as a specification and +verification system. Isabelle is a generic system for implementing logical +formalisms, and Isabelle/HOL is the specialization of Isabelle for +HOL, which abbreviates Higher-Order Logic. We introduce HOL step by step +following the equation +\[ \mbox{HOL} = \mbox{Functional Programming} + \mbox{Logic}. \] +We assume that the reader is familiar with the basic concepts of both fields. +For excellent introductions to functional programming consult the textbooks +by Bird and Wadler~\cite{Bird-Wadler} or Paulson~\cite{paulson-ml2}. Although +this tutorial initially concentrates on functional programming, do not be +misled: HOL can express most mathematical concepts, and functional +programming is just one particularly simple and ubiquitous instance. + +This tutorial introduces HOL via Isabelle/Isar~\cite{isabelle-isar-ref}, +which is an extension of Isabelle~\cite{paulson-isa-book} with structured +proofs.\footnote{Thus the full name of the system should be + Isabelle/Isar/HOL, but that is a bit of a mouthful.} The most noticeable +difference to classical Isabelle (which is the basis of another version of +this tutorial) is the replacement of the ML level by a dedicated language for +definitions and proofs. + +A tutorial is by definition incomplete. Currently the tutorial only +introduces the rudiments of Isar's proof language. To fully exploit the power +of Isar you need to consult the Isabelle/Isar Reference +Manual~\cite{isabelle-isar-ref}. If you want to use Isabelle's ML level +directly (for example for writing your own proof procedures) see the Isabelle +Reference Manual~\cite{isabelle-ref}; for details relating to HOL see the +Isabelle/HOL manual~\cite{isabelle-HOL}. All manuals have a comprehensive +index. + +\section{Theories} +\label{sec:Basic:Theories} + +Working with Isabelle means creating theories. Roughly speaking, a +\bfindex{theory} is a named collection of types, functions, and theorems, +much like a module in a programming language or a specification in a +specification language. In fact, theories in HOL can be either. The general +format of a theory \texttt{T} is +\begin{ttbox} +theory T = B\(@1\) + \(\cdots\) + B\(@n\): +\(\textit{declarations, definitions, and proofs}\) +end +\end{ttbox} +where \texttt{B}$@1$, \dots, \texttt{B}$@n$ are the names of existing +theories that \texttt{T} is based on and \texttt{\textit{declarations, + definitions, and proofs}} represents the newly introduced concepts +(types, functions etc) and proofs about them. The \texttt{B}$@i$ are the +direct \textbf{parent theories}\indexbold{parent theory} of \texttt{T}. +Everything defined in the parent theories (and their parents \dots) is +automatically visible. To avoid name clashes, identifiers can be +\textbf{qualified} by theory names as in \texttt{T.f} and +\texttt{B.f}.\indexbold{identifier!qualified} Each theory \texttt{T} must +reside in a \indexbold{theory file} named \texttt{T.thy}. + +This tutorial is concerned with introducing you to the different linguistic +constructs that can fill \textit{\texttt{declarations, definitions, and + proofs}} in the above theory template. A complete grammar of the basic +constructs is found in the Isabelle/Isar Reference Manual. + +HOL's theory library is available online at +\begin{center}\small + \url{http://isabelle.in.tum.de/library/} +\end{center} +and is recommended browsing. +\begin{warn} + HOL contains a theory \ttindexbold{Main}, the union of all the basic + predefined theories like arithmetic, lists, sets, etc.\ (see the online + library). Unless you know what you are doing, always include \texttt{Main} + as a direct or indirect parent theory of all your theories. +\end{warn} + + +\section{Interaction and interfaces} + +Interaction with Isabelle can either occur at the shell level or through more +advanced interfaces. To keep the tutorial independent of the interface we +have phrased the description of the intraction in a neutral language. For +example, the phrase ``to cancel a proof'' means to type \texttt{oops} at the +shell level, which is explained the first time the phrase is used. Other +interfaces perform the same act by cursor movements and/or mouse clicks. +Although shell-based interaction is quite feasible for the kind of proof +scripts currently presented in this tutorial, the recommended interface for +Isabelle/Isar is the Emacs-based \bfindex{Proof + General}~\cite{Aspinall:TACAS:2000,proofgeneral}. + +To improve readability some of the interfaces (including the shell level) +offer special fonts with mathematical symbols. Therefore the usual +mathematical symbols are used throughout the tutorial. Their +ASCII-equivalents are shown in figure~\ref{fig:ascii} in the appendix. + +Finally, a word about semicolons.\indexbold{$Isar@\texttt{;}} Some interfaces, +for example Proof General, require each command to be terminated by a +semicolon, whereas others, for example the shell level, do not. But even at +the shell level it is advisable to use semicolons to enforce that a command +is executed immediately; otherwise Isabelle may wait for the next keyword +before it knows that the command is complete. Note that for readibility +reasons we often drop the final semicolon in the text. + + +\section{Types, terms and formulae} +\label{sec:TypesTermsForms} +\indexbold{type} + +Embedded in the declarations of a theory are the types, terms and formulae of +HOL. HOL is a typed logic whose type system resembles that of functional +programming languages like ML or Haskell. Thus there are +\begin{description} +\item[base types,] in particular \ttindex{bool}, the type of truth values, +and \ttindex{nat}, the type of natural numbers. +\item[type constructors,] in particular \texttt{list}, the type of +lists, and \texttt{set}, the type of sets. Type constructors are written +postfix, e.g.\ \texttt{(nat)list} is the type of lists whose elements are +natural numbers. Parentheses around single arguments can be dropped (as in +\texttt{nat list}), multiple arguments are separated by commas (as in +\texttt{(bool,nat)foo}). +\item[function types,] denoted by \isasymFun\indexbold{$IsaFun@\isasymFun}. + In HOL \isasymFun\ represents {\em total} functions only. As is customary, + \texttt{$\tau@1$ \isasymFun~$\tau@2$ \isasymFun~$\tau@3$} means + \texttt{$\tau@1$ \isasymFun~($\tau@2$ \isasymFun~$\tau@3$)}. Isabelle also + supports the notation \texttt{[$\tau@1,\dots,\tau@n$] \isasymFun~$\tau$} + which abbreviates \texttt{$\tau@1$ \isasymFun~$\cdots$ \isasymFun~$\tau@n$ + \isasymFun~$\tau$}. +\item[type variables,] denoted by \texttt{'a}, \texttt{'b} etc, just like in +ML. They give rise to polymorphic types like \texttt{'a \isasymFun~'a}, the +type of the identity function. +\end{description} +\begin{warn} + Types are extremely important because they prevent us from writing + nonsense. Isabelle insists that all terms and formulae must be well-typed + and will print an error message if a type mismatch is encountered. To + reduce the amount of explicit type information that needs to be provided by + the user, Isabelle infers the type of all variables automatically (this is + called \bfindex{type inference}) and keeps quiet about it. Occasionally + this may lead to misunderstandings between you and the system. If anything + strange happens, we recommend to set the \rmindex{flag} + \ttindexbold{show_types} that tells Isabelle to display type information + that is usually suppressed: simply type +\begin{ttbox} +ML "set show_types" +\end{ttbox} + +\noindent +This can be reversed by \texttt{ML "reset show_types"}. Various other flags +can be set and reset in the same manner.\bfindex{flag!(re)setting} +\end{warn} + + +\textbf{Terms}\indexbold{term} are formed as in functional programming by +applying functions to arguments. If \texttt{f} is a function of type +\texttt{$\tau@1$ \isasymFun~$\tau@2$} and \texttt{t} is a term of type +$\tau@1$ then \texttt{f~t} is a term of type $\tau@2$. HOL also supports +infix functions like \texttt{+} and some basic constructs from functional +programming: +\begin{description} +\item[\texttt{if $b$ then $t@1$ else $t@2$}]\indexbold{*if} +means what you think it means and requires that +$b$ is of type \texttt{bool} and $t@1$ and $t@2$ are of the same type. +\item[\texttt{let $x$ = $t$ in $u$}]\indexbold{*let} +is equivalent to $u$ where all occurrences of $x$ have been replaced by +$t$. For example, +\texttt{let x = 0 in x+x} means \texttt{0+0}. Multiple bindings are separated +by semicolons: \texttt{let $x@1$ = $t@1$; \dots; $x@n$ = $t@n$ in $u$}. +\item[\texttt{case $e$ of $c@1$ \isasymFun~$e@1$ |~\dots~| $c@n$ \isasymFun~$e@n$}] +\indexbold{*case} +evaluates to $e@i$ if $e$ is of the form +$c@i$. See~\S\ref{sec:case-expressions} for details. +\end{description} + +Terms may also contain +\isasymlambda-abstractions\indexbold{$Isalam@\isasymlambda}. For example, +\texttt{\isasymlambda{}x.~x+1} is the function that takes an argument +\texttt{x} and returns \texttt{x+1}. Instead of +\texttt{\isasymlambda{}x.\isasymlambda{}y.\isasymlambda{}z.}~$t$ we can write +\texttt{\isasymlambda{}x~y~z.}~$t$. + +\textbf{Formulae}\indexbold{formula} +are terms of type \texttt{bool}. There are the basic +constants \ttindexbold{True} and \ttindexbold{False} and the usual logical +connectives (in decreasing order of priority): +\indexboldpos{\isasymnot}{$HOL0not}, +\indexboldpos{\isasymand}{$HOL0and}, +\indexboldpos{\isasymor}{$HOL0or}, and +\indexboldpos{\isasymimp}{$HOL0imp}, +all of which (except the unary \isasymnot) associate to the right. In +particular \texttt{A \isasymimp~B \isasymimp~C} means +\texttt{A \isasymimp~(B \isasymimp~C)} and is thus +logically equivalent with \texttt{A \isasymand~B \isasymimp~C} +(which is \texttt{(A \isasymand~B) \isasymimp~C}). + +Equality is available in the form of the infix function +\texttt{=}\indexbold{$HOL0eq@\texttt{=}} of type \texttt{'a \isasymFun~'a + \isasymFun~bool}. Thus \texttt{$t@1$ = $t@2$} is a formula provided $t@1$ +and $t@2$ are terms of the same type. In case $t@1$ and $t@2$ are of type +\texttt{bool}, \texttt{=} acts as if-and-only-if. The formula +$t@1$~\isasymnoteq~$t@2$ is merely an abbreviation for +\texttt{\isasymnot($t@1$ = $t@2$)}. + +The syntax for quantifiers is +\texttt{\isasymforall{}x.}~$P$\indexbold{$HOL0All@\isasymforall} and +\texttt{\isasymexists{}x.}~$P$\indexbold{$HOL0Ex@\isasymexists}. There is +even \texttt{\isasymuniqex{}x.}~$P$\index{$HOL0ExU@\isasymuniqex|bold}, which +means that there exists exactly one \texttt{x} that satisfies $P$. +Nested quantifications can be abbreviated: +\texttt{\isasymforall{}x~y~z.}~$P$ means +\texttt{\isasymforall{}x.\isasymforall{}y.\isasymforall{}z.}~$P$. + +Despite type inference, it is sometimes necessary to attach explicit +\bfindex{type constraints} to a term. The syntax is \texttt{$t$::$\tau$} as +in \texttt{x < (y::nat)}. Note that \ttindexboldpos{::}{$Isalamtc} binds weakly +and should therefore be enclosed in parentheses: \texttt{x < y::nat} is +ill-typed because it is interpreted as \texttt{(x < y)::nat}. The main reason +for type constraints are overloaded functions like \texttt{+}, \texttt{*} and +\texttt{<}. (See \S\ref{sec:TypeClasses} for a full discussion of +overloading.) + +\begin{warn} +In general, HOL's concrete syntax tries to follow the conventions of +functional programming and mathematics. Below we list the main rules that you +should be familiar with to avoid certain syntactic traps. A particular +problem for novices can be the priority of operators. If you are unsure, use +more rather than fewer parentheses. In those cases where Isabelle echoes your +input, you can see which parentheses are dropped---they were superfluous. If +you are unsure how to interpret Isabelle's output because you don't know +where the (dropped) parentheses go, set (and possibly reset) the \rmindex{flag} +\ttindexbold{show_brackets}: +\begin{ttbox} +ML "set show_brackets"; \(\dots\); ML "reset show_brackets"; +\end{ttbox} +\end{warn} + +\begin{itemize} +\item +Remember that \texttt{f t u} means \texttt{(f t) u} and not \texttt{f(t u)}! +\item +Isabelle allows infix functions like \texttt{+}. The prefix form of function +application binds more strongly than anything else and hence \texttt{f~x + y} +means \texttt{(f~x)~+~y} and not \texttt{f(x+y)}. +\item Remember that in HOL if-and-only-if is expressed using equality. But + equality has a high priority, as befitting a relation, while if-and-only-if + typically has the lowest priority. Thus, \texttt{\isasymnot~\isasymnot~P = + P} means \texttt{\isasymnot\isasymnot(P = P)} and not + \texttt{(\isasymnot\isasymnot P) = P}. When using \texttt{=} to mean + logical equivalence, enclose both operands in parentheses, as in \texttt{(A + \isasymand~B) = (B \isasymand~A)}. +\item +Constructs with an opening but without a closing delimiter bind very weakly +and should therefore be enclosed in parentheses if they appear in subterms, as +in \texttt{f = (\isasymlambda{}x.~x)}. This includes \ttindex{if}, +\ttindex{let}, \ttindex{case}, \isasymlambda, and quantifiers. +\item +Never write \texttt{\isasymlambda{}x.x} or \texttt{\isasymforall{}x.x=x} +because \texttt{x.x} is always read as a single qualified identifier that +refers to an item \texttt{x} in theory \texttt{x}. Write +\texttt{\isasymlambda{}x.~x} and \texttt{\isasymforall{}x.~x=x} instead. +\item Identifiers\indexbold{identifier} may contain \texttt{_} and \texttt{'}. +\end{itemize} + +Remember that ASCII-equivalents of all mathematical symbols are +given in figure~\ref{fig:ascii} in the appendix. + +\section{Variables} +\label{sec:variables} +\indexbold{variable} + +Isabelle distinguishes free and bound variables just as is customary. Bound +variables are automatically renamed to avoid clashes with free variables. In +addition, Isabelle has a third kind of variable, called a \bfindex{schematic + variable}\indexbold{variable!schematic} or \bfindex{unknown}, which starts +with a \texttt{?}. Logically, an unknown is a free variable. But it may be +instantiated by another term during the proof process. For example, the +mathematical theorem $x = x$ is represented in Isabelle as \texttt{?x = ?x}, +which means that Isabelle can instantiate it arbitrarily. This is in contrast +to ordinary variables, which remain fixed. The programming language Prolog +calls unknowns {\em logical\/} variables. + +Most of the time you can and should ignore unknowns and work with ordinary +variables. Just don't be surprised that after you have finished the proof of +a theorem, Isabelle will turn your free variables into unknowns: it merely +indicates that Isabelle will automatically instantiate those unknowns +suitably when the theorem is used in some other proof. +\begin{warn} + If you use \texttt{?}\index{$HOL0Ex@\texttt{?}} as an existential + quantifier, it needs to be followed by a space. Otherwise \texttt{?x} is + interpreted as a schematic variable. +\end{warn} + +\section{Getting started} + +Assuming you have installed Isabelle, you start it by typing \texttt{isabelle + -I HOL} in a shell window.\footnote{Simply executing \texttt{isabelle -I} + starts the default logic, which usually is already \texttt{HOL}. This is + controlled by the \texttt{ISABELLE_LOGIC} setting, see \emph{The Isabelle + System Manual} for more details.} This presents you with Isabelle's most +basic ASCII interface. In addition you need to open an editor window to +create theory files. While you are developing a theory, we recommend to +type each command into the file first and then enter it into Isabelle by +copy-and-paste, thus ensuring that you have a complete record of your theory. +As mentioned earlier, Proof General offers a much superior interface. diff -r 8a5b3f58b944 -r 3253c6046d57 doc-src/TutorialI/extra.sty --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/doc-src/TutorialI/extra.sty Wed Apr 19 11:54:39 2000 +0200 @@ -0,0 +1,29 @@ +% extra.sty : Isabelle Manual extra macros for non-Springer version +% +\typeout{Document Style extra. Released 17 February 1994} + +%%Euro-style date: 20 September 1955 +\def\today{\number\day\space\ifcase\month\or +January\or February\or March\or April\or May\or June\or +July\or August\or September\or October\or November\or December\fi +\space\number\year} + +%%Borrowed from alltt.sty, but leaves % as the comment character +\def\docspecials{\do\ \do\$\do\&% + \do\#\do\^\do\^^K\do\_\do\^^A\do\~} + +%%%Put first chapter on odd page, with arabic numbering; like \cleardoublepage +\newcommand\clearfirst{\clearpage\ifodd\c@page\else + \hbox{}\newpage\if@twocolumn\hbox{}\newpage\fi\fi + \pagenumbering{arabic}} + +%%%Ruled chapter headings +\def\@rulehead#1{\hrule height1pt \vskip 14pt \Huge \bf + #1 \vskip 14pt\hrule height1pt} +\def\@makechapterhead#1{ { \parindent 0pt + \ifnum\c@secnumdepth >\m@ne \raggedleft\large\bf\@chapapp{} \thechapter \par + \vskip 20pt \fi \raggedright \@rulehead{#1} \par \nobreak \vskip 40pt } } + +\def\@makeschapterhead#1{ { \parindent 0pt \raggedright + \@rulehead{#1} \par \nobreak \vskip 40pt } } + diff -r 8a5b3f58b944 -r 3253c6046d57 doc-src/TutorialI/fp.tex --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/doc-src/TutorialI/fp.tex Wed Apr 19 11:54:39 2000 +0200 @@ -0,0 +1,841 @@ +\chapter{Functional Programming in HOL} + +Although on the surface this chapter is mainly concerned with how to write +functional programs in HOL and how to verify them, most of the +constructs and proof procedures introduced are general purpose and recur in +any specification or verification task. + +The dedicated functional programmer should be warned: HOL offers only {\em + total functional programming} --- all functions in HOL must be total; lazy +data structures are not directly available. On the positive side, functions +in HOL need not be computable: HOL is a specification language that goes well +beyond what can be expressed as a program. However, for the time being we +concentrate on the computable. + +\section{An introductory theory} +\label{sec:intro-theory} + +Functional programming needs datatypes and functions. Both of them can be +defined in a theory with a syntax reminiscent of languages like ML or +Haskell. As an example consider the theory in figure~\ref{fig:ToyList}. +We will now examine it line by line. + +\begin{figure}[htbp] +\begin{ttbox}\makeatother +\input{ToyList2/ToyList1}\end{ttbox} +\caption{A theory of lists} +\label{fig:ToyList} +\end{figure} + +{\makeatother\input{ToyList/document/ToyList.tex}} + +The complete proof script is shown in figure~\ref{fig:ToyList-proofs}. The +concatenation of figures \ref{fig:ToyList} and \ref{fig:ToyList-proofs} +constitutes the complete theory \texttt{ToyList} and should reside in file +\texttt{ToyList.thy}. It is good practice to present all declarations and +definitions at the beginning of a theory to facilitate browsing. + +\begin{figure}[htbp] +\begin{ttbox}\makeatother +\input{ToyList2/ToyList2}\end{ttbox} +\caption{Proofs about lists} +\label{fig:ToyList-proofs} +\end{figure} + +\subsubsection*{Review} + +This is the end of our toy proof. It should have familiarized you with +\begin{itemize} +\item the standard theorem proving procedure: +state a goal (lemma or theorem); proceed with proof until a separate lemma is +required; prove that lemma; come back to the original goal. +\item a specific procedure that works well for functional programs: +induction followed by all-out simplification via \isa{auto}. +\item a basic repertoire of proof commands. +\end{itemize} + + +\section{Some helpful commands} +\label{sec:commands-and-hints} + +This section discusses a few basic commands for manipulating the proof state +and can be skipped by casual readers. + +There are two kinds of commands used during a proof: the actual proof +commands and auxiliary commands for examining the proof state and controlling +the display. Simple proof commands are of the form +\isacommand{apply}\isa{(method)}\indexbold{apply} where \bfindex{method} is a +synonym for ``theorem proving function''. Typical examples are +\isa{induct_tac} and \isa{auto}. Further methods are introduced throughout +the tutorial. Unless stated otherwise you may assume that a method attacks +merely the first subgoal. An exception is \isa{auto} which tries to solve all +subgoals. + +The most useful auxiliary commands are: +\begin{description} +\item[Undoing:] \isacommand{undo}\indexbold{*undo} undoes the effect of the + last command; \isacommand{undo} can be undone by + \isacommand{redo}\indexbold{*redo}. Both are only needed at the shell + level and should not occur in the final theory. +\item[Printing the current state:] \isacommand{pr}\indexbold{*pr} redisplays + the current proof state, for example when it has disappeared off the + screen. +\item[Limiting the number of subgoals:] \isacommand{pr}~$n$ tells Isabelle to + print only the first $n$ subgoals from now on and redisplays the current + proof state. This is helpful when there are many subgoals. +\item[Modifying the order of subgoals:] +\isacommand{defer}\indexbold{*defer} moves the first subgoal to the end and +\isacommand{prefer}\indexbold{*prefer}~$n$ moves subgoal $n$ to the front. +\item[Printing theorems:] + \isacommand{thm}\indexbold{*thm}~\textit{name}$@1$~\dots~\textit{name}$@n$ + prints the named theorems. +\item[Displaying types:] We have already mentioned the flag + \ttindex{show_types} above. It can also be useful for detecting typos in + formulae early on. For example, if \texttt{show_types} is set and the goal + \isa{rev(rev xs) = xs} is started, Isabelle prints the additional output +\par\noindent +\begin{isabelle}% +Variables:\isanewline +~~xs~::~'a~list +\end{isabelle}% +\par\noindent +which tells us that Isabelle has correctly inferred that +\isa{xs} is a variable of list type. On the other hand, had we +made a typo as in \isa{rev(re xs) = xs}, the response +\par\noindent +\begin{isabelle}% +Variables:\isanewline +~~re~::~'a~list~{\isasymRightarrow}~'a~list\isanewline +~~xs~::~'a~list% +\end{isabelle}% +\par\noindent +would have alerted us because of the unexpected variable \isa{re}. +\item[Reading terms and types:] \isacommand{term}\indexbold{*term} + \textit{string} reads, type-checks and prints the given string as a term in + the current context; the inferred type is output as well. + \isacommand{typ}\indexbold{*typ} \textit{string} reads and prints the given + string as a type in the current context. +\item[(Re)loading theories:] When you start your interaction you must open a + named theory with the line + \isacommand{theory}\texttt{~T~=}~\dots~\texttt{:}. Isabelle automatically + loads all the required parent theories from their respective files (which + may take a moment, unless the theories are already loaded and the files + have not been modified). The only time when you need to load a theory by + hand is when you simply want to check if it loads successfully without + wanting to make use of the theory itself. This you can do by typing + \isacommand{use\_thy}\indexbold{*use_thy}~\texttt{"T"}. + + If you suddenly discover that you need to modify a parent theory of your + current theory you must first abandon your current theory (at the shell + level type \isacommand{kill}\indexbold{*kill}). After the parent theory has + been modified you go back to your original theory. When its first line + \isacommand{theory}\texttt{~T~=}~\dots~\texttt{:} is processed, the + modified parent is reloaded automatically. +\end{description} +Further commands are found in the Isabelle/Isar Reference Manual. + + +\section{Datatypes} +\label{sec:datatype} + +Inductive datatypes are part of almost every non-trivial application of HOL. +First we take another look at a very important example, the datatype of +lists, before we turn to datatypes in general. The section closes with a +case study. + + +\subsection{Lists} +\indexbold{*list} + +Lists are one of the essential datatypes in computing. Readers of this +tutorial and users of HOL need to be familiar with their basic operations. +Theory \texttt{ToyList} is only a small fragment of HOL's predefined theory +\texttt{List}\footnote{\url{http://isabelle.in.tum.de/library/HOL/List.html}}. +The latter contains many further operations. For example, the functions +\isaindexbold{hd} (`head') and \isaindexbold{tl} (`tail') return the first +element and the remainder of a list. (However, pattern-matching is usually +preferable to \isa{hd} and \isa{tl}.) Theory \texttt{List} also contains +more syntactic sugar: \isa{[}$x@1$\isa{,}\dots\isa{,}$x@n$\isa{]} abbreviates +$x@1$\isa{\#}\dots\isa{\#}$x@n$\isa{\#[]}. In the rest of the tutorial we +always use HOL's predefined lists. + + +\subsection{The general format} +\label{sec:general-datatype} + +The general HOL \isacommand{datatype} definition is of the form +\[ +\isacommand{datatype}~(\alpha@1, \dots, \alpha@n) \, t ~=~ +C@1~\tau@{11}~\dots~\tau@{1k@1} ~\mid~ \dots ~\mid~ +C@m~\tau@{m1}~\dots~\tau@{mk@m} +\] +where $\alpha@i$ are type variables (the parameters), $C@i$ are distinct +constructor names and $\tau@{ij}$ are types; it is customary to capitalize +the first letter in constructor names. There are a number of +restrictions (such as that the type should not be empty) detailed +elsewhere~\cite{isabelle-HOL}. Isabelle notifies you if you violate them. + +Laws about datatypes, such as \isa{[] \isasymnoteq~x\#xs} and +\isa{(x\#xs = y\#ys) = (x=y \isasymand~xs=ys)}, are used automatically +during proofs by simplification. The same is true for the equations in +primitive recursive function definitions. + +\subsection{Primitive recursion} + +Functions on datatypes are usually defined by recursion. In fact, most of the +time they are defined by what is called \bfindex{primitive recursion}. +The keyword \isacommand{primrec}\indexbold{*primrec} is followed by a list of +equations +\[ f \, x@1 \, \dots \, (C \, y@1 \, \dots \, y@k)\, \dots \, x@n = r \] +such that $C$ is a constructor of the datatype $t$ and all recursive calls of +$f$ in $r$ are of the form $f \, \dots \, y@i \, \dots$ for some $i$. Thus +Isabelle immediately sees that $f$ terminates because one (fixed!) argument +becomes smaller with every recursive call. There must be exactly one equation +for each constructor. Their order is immaterial. +A more general method for defining total recursive functions is explained in +\S\ref{sec:recdef}. + +\begin{exercise} +\input{Misc/document/Tree.tex}% +\end{exercise} + +\subsection{Case expressions} +\label{sec:case-expressions} + +HOL also features \isaindexbold{case}-expressions for analyzing +elements of a datatype. For example, +% case xs of [] => 0 | y#ys => y +\begin{isabellepar}% +~~~case~xs~of~[]~{\isasymRightarrow}~0~|~y~\#~ys~{\isasymRightarrow}~y +\end{isabellepar}% +evaluates to \isa{0} if \isa{xs} is \isa{[]} and to \isa{y} if +\isa{xs} is \isa{y\#ys}. (Since the result in both branches must be of +the same type, it follows that \isa{y::nat} and hence +\isa{xs::(nat)list}.) + +In general, if $e$ is a term of the datatype $t$ defined in +\S\ref{sec:general-datatype} above, the corresponding +\isa{case}-expression analyzing $e$ is +\[ +\begin{array}{rrcl} +\isa{case}~e~\isa{of} & C@1~x@{11}~\dots~x@{1k@1} & \To & e@1 \\ + \vdots \\ + \mid & C@m~x@{m1}~\dots~x@{mk@m} & \To & e@m +\end{array} +\] + +\begin{warn} +{\em All} constructors must be present, their order is fixed, and nested +patterns are not supported. Violating these restrictions results in strange +error messages. +\end{warn} +\noindent +Nested patterns can be simulated by nested \isa{case}-expressions: instead +of +% case xs of [] => 0 | [x] => x | x#(y#zs) => y +\begin{isabellepar}% +~~~case~xs~of~[]~{\isasymRightarrow}~0~|~[x]~{\isasymRightarrow}~x~|~x~\#~y~\#~zs~{\isasymRightarrow}~y +\end{isabellepar}% +write +% term(latex xsymbols symbols)"case xs of [] => 0 | x#ys => (case ys of [] => x | y#zs => y)"; +\begin{isabellepar}% +~~~case~xs~of~[]~{\isasymRightarrow}~0~|~x~\#~ys~{\isasymRightarrow}~(case~ys~of~[]~{\isasymRightarrow}~x~|~y~\#~zs~{\isasymRightarrow}~y)% +\end{isabellepar}% +Note that \isa{case}-expressions should be enclosed in parentheses to +indicate their scope. + +\subsection{Structural induction and case distinction} +\indexbold{structural induction} +\indexbold{induction!structural} +\indexbold{case distinction} + +Almost all the basic laws about a datatype are applied automatically during +simplification. Only induction is invoked by hand via \isaindex{induct_tac}, +which works for any datatype. In some cases, induction is overkill and a case +distinction over all constructors of the datatype suffices. This is performed +by \isaindexbold{case_tac}. A trivial example: + +\input{Misc/document/cases.tex}% + +Note that we do not need to give a lemma a name if we do not intend to refer +to it explicitly in the future. + +\begin{warn} + Induction is only allowed on free (or \isasymAnd-bound) variables that + should not occur among the assumptions of the subgoal. Case distinction + (\isa{case_tac}) works for arbitrary terms, which need to be + quoted if they are non-atomic. +\end{warn} + + +\subsection{Case study: boolean expressions} +\label{sec:boolex} + +The aim of this case study is twofold: it shows how to model boolean +expressions and some algorithms for manipulating them, and it demonstrates +the constructs introduced above. + +\input{Ifexpr/document/Ifexpr.tex} + +How does one come up with the required lemmas? Try to prove the main theorems +without them and study carefully what \isa{auto} leaves unproved. This has +to provide the clue. The necessity of universal quantification +(\isa{\isasymforall{}t e}) in the two lemmas is explained in +\S\ref{sec:InductionHeuristics} + +\begin{exercise} + We strengthen the definition of a \isa{normal} If-expression as follows: + the first argument of all \isa{IF}s must be a variable. Adapt the above + development to this changed requirement. (Hint: you may need to formulate + some of the goals as implications (\isasymimp) rather than equalities + (\isa{=}).) +\end{exercise} + +\section{Some basic types} + + +\subsection{Natural numbers} +\index{arithmetic|(} + +\input{Misc/document/fakenat.tex} +\input{Misc/document/natsum.tex} + +The usual arithmetic operations \ttindexboldpos{+}{$HOL2arithfun}, +\ttindexboldpos{-}{$HOL2arithfun}, \ttindexboldpos{*}{$HOL2arithfun}, +\isaindexbold{div}, \isaindexbold{mod}, \isaindexbold{min} and +\isaindexbold{max} are predefined, as are the relations +\indexboldpos{\isasymle}{$HOL2arithrel} and +\ttindexboldpos{<}{$HOL2arithrel}. There is even a least number operation +\isaindexbold{LEAST}. For example, \isa{(LEAST n.$\,$1 < n) = 2}, although +Isabelle does not prove this completely automatically. Note that \isa{1} and +\isa{2} are available as abbreviations for the corresponding +\isa{Suc}-expressions. If you need the full set of numerals, +see~\S\ref{nat-numerals}. + +\begin{warn} + The operations \ttindexboldpos{+}{$HOL2arithfun}, + \ttindexboldpos{-}{$HOL2arithfun}, \ttindexboldpos{*}{$HOL2arithfun}, + \isaindexbold{min}, \isaindexbold{max}, + \indexboldpos{\isasymle}{$HOL2arithrel} and + \ttindexboldpos{<}{$HOL2arithrel} are overloaded, i.e.\ they are available + not just for natural numbers but at other types as well (see + \S\ref{sec:TypeClasses}). For example, given the goal \isa{x+y = y+x}, + there is nothing to indicate that you are talking about natural numbers. + Hence Isabelle can only infer that \isa{x} and \isa{y} are of some + arbitrary type where \isa{+} is declared. As a consequence, you will be + unable to prove the goal (although it may take you some time to realize + what has happened if \texttt{show_types} is not set). In this particular + example, you need to include an explicit type constraint, for example + \isa{x+y = y+(x::nat)}. If there is enough contextual information this may + not be necessary: \isa{x+0 = x} automatically implies \isa{x::nat}. +\end{warn} + +Simple arithmetic goals are proved automatically by both \isa{auto} +and the simplification methods introduced in \S\ref{sec:Simplification}. For +example, + +\input{Misc/document/arith1.tex}% +is proved automatically. The main restriction is that only addition is taken +into account; other arithmetic operations and quantified formulae are ignored. + +For more complex goals, there is the special method +\isaindexbold{arith} (which attacks the first subgoal). It proves +arithmetic goals involving the usual logical connectives (\isasymnot, +\isasymand, \isasymor, \isasymimp), the relations \isasymle\ and \isa{<}, and +the operations \isa{+}, \isa{-}, \isa{min} and \isa{max}. For example, + +\input{Misc/document/arith2.tex}% +succeeds because \isa{k*k} can be treated as atomic. +In contrast, + +\input{Misc/document/arith3.tex}% +is not even proved by \isa{arith} because the proof relies essentially +on properties of multiplication. + +\begin{warn} + The running time of \isa{arith} is exponential in the number of occurrences + of \ttindexboldpos{-}{$HOL2arithfun}, \isaindexbold{min} and + \isaindexbold{max} because they are first eliminated by case distinctions. + + \isa{arith} is incomplete even for the restricted class of formulae + described above (known as ``linear arithmetic''). If divisibility plays a + role, it may fail to prove a valid formula, for example $m+m \neq n+n+1$. + Fortunately, such examples are rare in practice. +\end{warn} + +\index{arithmetic|)} + + +\subsection{Products} + +HOL also has pairs: \isa{($a@1$,$a@2$)} is of type \texttt{$\tau@1$ * + $\tau@2$} provided each $a@i$ is of type $\tau@i$. The components of a pair +are extracted by \isa{fst} and \isa{snd}: \isa{fst($x$,$y$) = $x$} and +\isa{snd($x$,$y$) = $y$}. Tuples are simulated by pairs nested to the right: +\isa{($a@1$,$a@2$,$a@3$)} stands for \isa{($a@1$,($a@2$,$a@3$))} and +\isa{$\tau@1$ * $\tau@2$ * $\tau@3$} for \isa{$\tau@1$ * ($\tau@2$ * + $\tau@3$)}. Therefore we have \isa{fst(snd($a@1$,$a@2$,$a@3$)) = $a@2$}. + +It is possible to use (nested) tuples as patterns in abstractions, for +example \isa{\isasymlambda(x,y,z).x+y+z} and +\isa{\isasymlambda((x,y),z).x+y+z}. +In addition to explicit $\lambda$-abstractions, tuple patterns can be used in +most variable binding constructs. Typical examples are + +\input{Misc/document/pairs.tex}% +Further important examples are quantifiers and sets (see~\S\ref{quant-pats}). + +%FIXME move stuff below into section on proofs about products? +\begin{warn} + Abstraction over pairs and tuples is merely a convenient shorthand for a + more complex internal representation. Thus the internal and external form + of a term may differ, which can affect proofs. If you want to avoid this + complication, use \isa{fst} and \isa{snd}, i.e.\ write + \isa{\isasymlambda{}p.~fst p + snd p} instead of + \isa{\isasymlambda(x,y).~x + y}. See~\S\ref{proofs-about-products} for + theorem proving with tuple patterns. +\end{warn} + +Finally note that products, like natural numbers, are datatypes, which means +in particular that \isa{induct_tac} and \isa{case_tac} are applicable to +products (see \S\ref{proofs-about-products}). + +\section{Definitions} +\label{sec:Definitions} + +A definition is simply an abbreviation, i.e.\ a new name for an existing +construction. In particular, definitions cannot be recursive. Isabelle offers +definitions on the level of types and terms. Those on the type level are +called type synonyms, those on the term level are called (constant) +definitions. + + +\subsection{Type synonyms} +\indexbold{type synonyms} + +Type synonyms are similar to those found in ML. Their syntax is fairly self +explanatory: + +\input{Misc/document/types.tex}% + +Note that pattern-matching is not allowed, i.e.\ each definition must be of +the form $f\,x@1\,\dots\,x@n~\isasymequiv~t$. + +Section~\S\ref{sec:Simplification} explains how definitions are used +in proofs. + +\begin{warn}% +A common mistake when writing definitions is to introduce extra free +variables on the right-hand side as in the following fictitious definition: +\input{Misc/document/prime_def.tex}% +\end{warn} + + +\chapter{More Functional Programming} + +The purpose of this chapter is to deepen the reader's understanding of the +concepts encountered so far and to introduce an advanced forms of datatypes +and recursive functions. The first two sections give a structured +presentation of theorem proving by simplification +(\S\ref{sec:Simplification}) and discuss important heuristics for induction +(\S\ref{sec:InductionHeuristics}). They can be skipped by readers less +interested in proofs. They are followed by a case study, a compiler for +expressions (\S\ref{sec:ExprCompiler}). Advanced datatypes, including those +involving function spaces, are covered in \S\ref{sec:advanced-datatypes}, +which closes with another case study, search trees (``tries''). Finally we +introduce a very general form of recursive function definition which goes +well beyond what \isacommand{primrec} allows (\S\ref{sec:recdef}). + + +\section{Simplification} +\label{sec:Simplification} +\index{simplification|(} + +So far we have proved our theorems by \isa{auto}, which ``simplifies'' all +subgoals. In fact, \isa{auto} can do much more than that, except that it +did not need to so far. However, when you go beyond toy examples, you need to +understand the ingredients of \isa{auto}. This section covers the method +that \isa{auto} always applies first, namely simplification. + +Simplification is one of the central theorem proving tools in Isabelle and +many other systems. The tool itself is called the \bfindex{simplifier}. The +purpose of this section is twofold: to introduce the many features of the +simplifier (\S\ref{sec:SimpFeatures}) and to explain a little bit how the +simplifier works (\S\ref{sec:SimpHow}). Anybody intending to use HOL should +read \S\ref{sec:SimpFeatures}, and the serious student should read +\S\ref{sec:SimpHow} as well in order to understand what happened in case +things do not simplify as expected. + + +\subsection{Using the simplifier} +\label{sec:SimpFeatures} + +In its most basic form, simplification means repeated application of +equations from left to right. For example, taking the rules for \isa{\at} +and applying them to the term \isa{[0,1] \at\ []} results in a sequence of +simplification steps: +\begin{ttbox}\makeatother +(0#1#[]) @ [] \(\leadsto\) 0#((1#[]) @ []) \(\leadsto\) 0#(1#([] @ [])) \(\leadsto\) 0#1#[] +\end{ttbox} +This is also known as \bfindex{term rewriting} and the equations are referred +to as \bfindex{rewrite rules}. This is more honest than ``simplification'' +because the terms do not necessarily become simpler in the process. + +\subsubsection{Simplification rules} +\indexbold{simplification rules} + +To facilitate simplification, theorems can be declared to be simplification +rules (with the help of the attribute \isa{[simp]}\index{*simp + (attribute)}), in which case proofs by simplification make use of these +rules by default. In addition the constructs \isacommand{datatype} and +\isacommand{primrec} (and a few others) invisibly declare useful +simplification rules. Explicit definitions are \emph{not} declared +simplification rules automatically! + +Not merely equations but pretty much any theorem can become a simplification +rule. The simplifier will try to make sense of it. For example, a theorem +\isasymnot$P$ is automatically turned into \isa{$P$ = False}. The details +are explained in \S\ref{sec:SimpHow}. + +The simplification attribute of theorems can be turned on and off as follows: +\begin{ttbox} +theorems [simp] = \(list of theorem names\); +theorems [simp del] = \(list of theorem names\); +\end{ttbox} +As a rule of thumb, rules that really simplify (like \isa{rev(rev xs) = + xs} and \mbox{\isa{xs \at\ [] = xs}}) should be made simplification +rules. Those of a more specific nature (e.g.\ distributivity laws, which +alter the structure of terms considerably) should only be used selectively, +i.e.\ they should not be default simplification rules. Conversely, it may +also happen that a simplification rule needs to be disabled in certain +proofs. Frequent changes in the simplification status of a theorem may +indicates a badly designed theory. +\begin{warn} + Simplification may not terminate, for example if both $f(x) = g(x)$ and + $g(x) = f(x)$ are simplification rules. It is the user's responsibility not + to include simplification rules that can lead to nontermination, either on + their own or in combination with other simplification rules. +\end{warn} + +\subsubsection{The simplification method} +\index{*simp (method)|bold} + +The general format of the simplification method is +\begin{ttbox} +simp \(list of modifiers\) +\end{ttbox} +where the list of \emph{modifiers} helps to fine tune the behaviour and may +be empty. Most if not all of the proofs seen so far could have been performed +with \isa{simp} instead of \isa{auto}, except that \isa{simp} attacks +only the first subgoal and may thus need to be repeated. +Note that \isa{simp} fails if nothing changes. + +\subsubsection{Adding and deleting simplification rules} + +If a certain theorem is merely needed in a few proofs by simplification, +we do not need to make it a global simplification rule. Instead we can modify +the set of simplification rules used in a simplification step by adding rules +to it and/or deleting rules from it. The two modifiers for this are +\begin{ttbox} +add: \(list of theorem names\) +del: \(list of theorem names\) +\end{ttbox} +In case you want to use only a specific list of theorems and ignore all +others: +\begin{ttbox} +only: \(list of theorem names\) +\end{ttbox} + + +\subsubsection{Assumptions} +\index{simplification!with/of assumptions} + +{\makeatother\input{Misc/document/asm_simp.tex}} + +\subsubsection{Rewriting with definitions} +\index{simplification!with definitions} + +\input{Misc/document/def_rewr.tex} + +\begin{warn} + If you have defined $f\,x\,y~\isasymequiv~t$ then you can only expand + occurrences of $f$ with at least two arguments. Thus it is safer to define + $f$~\isasymequiv~\isasymlambda$x\,y.\;t$. +\end{warn} + +\subsubsection{Simplifying let-expressions} +\index{simplification!of let-expressions} + +Proving a goal containing \isaindex{let}-expressions almost invariably +requires the \isa{let}-con\-structs to be expanded at some point. Since +\isa{let}-\isa{in} is just syntactic sugar for a defined constant (called +\isa{Let}), expanding \isa{let}-constructs means rewriting with +\isa{Let_def}: + +{\makeatother\input{Misc/document/let_rewr.tex}} + +\subsubsection{Conditional equations} + +\input{Misc/document/cond_rewr.tex} + + +\subsubsection{Automatic case splits} +\indexbold{case splits} +\index{*split|(} + +{\makeatother\input{Misc/document/case_splits.tex}} + +\index{*split|)} + +\begin{warn} + The simplifier merely simplifies the condition of an \isa{if} but not the + \isa{then} or \isa{else} parts. The latter are simplified only after the + condition reduces to \isa{True} or \isa{False}, or after splitting. The + same is true for \isaindex{case}-expressions: only the selector is + simplified at first, until either the expression reduces to one of the + cases or it is split. +\end{warn} + +\subsubsection{Arithmetic} +\index{arithmetic} + +The simplifier routinely solves a small class of linear arithmetic formulae +(over types \isa{nat} and \isa{int}): it only takes into account +assumptions and conclusions that are (possibly negated) (in)equalities +(\isa{=}, \isasymle, \isa{<}) and it only knows about addition. Thus + +\input{Misc/document/arith1.tex}% +is proved by simplification, whereas the only slightly more complex + +\input{Misc/document/arith4.tex}% +is not proved by simplification and requires \isa{arith}. + +\subsubsection{Permutative rewrite rules} + +A rewrite rule is {\bf permutative} if the left-hand side and right-hand side +are the same up to renaming of variables. The most common permutative rule +is commutativity: $x+y = y+x$. Another example is $(x-y)-z = (x-z)-y$. Such +rules are problematic because once they apply, they can be used forever. +The simplifier is aware of this danger and treats permutative rules +separately. For details see~\cite{isabelle-ref}. + +\subsubsection{Tracing} +\indexbold{tracing the simplifier} + +{\makeatother\input{Misc/document/trace_simp.tex}} + +\subsection{How it works} +\label{sec:SimpHow} + +\subsubsection{Higher-order patterns} + +\subsubsection{Local assumptions} + +\subsubsection{The preprocessor} + +\index{simplification|)} + +\section{Induction heuristics} +\label{sec:InductionHeuristics} + +The purpose of this section is to illustrate some simple heuristics for +inductive proofs. The first one we have already mentioned in our initial +example: +\begin{quote} +{\em 1. Theorems about recursive functions are proved by induction.} +\end{quote} +In case the function has more than one argument +\begin{quote} +{\em 2. Do induction on argument number $i$ if the function is defined by +recursion in argument number $i$.} +\end{quote} +When we look at the proof of {\makeatother\isa{(xs @ ys) @ zs = xs @ (ys @ + zs)}} in \S\ref{sec:intro-proof} we find (a) \isa{\at} is recursive in +the first argument, (b) \isa{xs} occurs only as the first argument of +\isa{\at}, and (c) both \isa{ys} and \isa{zs} occur at least once as +the second argument of \isa{\at}. Hence it is natural to perform induction +on \isa{xs}. + +The key heuristic, and the main point of this section, is to +generalize the goal before induction. The reason is simple: if the goal is +too specific, the induction hypothesis is too weak to allow the induction +step to go through. Let us now illustrate the idea with an example. + +{\makeatother\input{Misc/document/Itrev.tex}} + +A final point worth mentioning is the orientation of the equation we just +proved: the more complex notion (\isa{itrev}) is on the left-hand +side, the simpler \isa{rev} on the right-hand side. This constitutes +another, albeit weak heuristic that is not restricted to induction: +\begin{quote} + {\em 5. The right-hand side of an equation should (in some sense) be + simpler than the left-hand side.} +\end{quote} +The heuristic is tricky to apply because it is not obvious that +\isa{rev xs \at\ ys} is simpler than \isa{itrev xs ys}. But see what +happens if you try to prove the symmetric equation! + + +\section{Case study: compiling expressions} +\label{sec:ExprCompiler} + +{\makeatother\input{CodeGen/document/CodeGen.tex}} + + +\section{Advanced datatypes} +\label{sec:advanced-datatypes} +\index{*datatype|(} +\index{*primrec|(} +%|) + +This section presents advanced forms of \isacommand{datatype}s. + +\subsection{Mutual recursion} +\label{sec:datatype-mut-rec} + +\input{Datatype/document/ABexpr.tex} + +\subsection{Nested recursion} + +\input{Datatype/document/Nested.tex} + + +\subsection{The limits of nested recursion} + +How far can we push nested recursion? By the unfolding argument above, we can +reduce nested to mutual recursion provided the nested recursion only involves +previously defined datatypes. This does not include functions: +\begin{ttbox} +datatype t = C (t => bool) +\end{ttbox} +is a real can of worms: in HOL it must be ruled out because it requires a type +\isa{t} such that \isa{t} and its power set \isa{t \isasymFun\ bool} have the +same cardinality---an impossibility. For the same reason it is not possible +to allow recursion involving the type \isa{set}, which is isomorphic to +\isa{t \isasymFun\ bool}. + +Fortunately, a limited form of recursion +involving function spaces is permitted: the recursive type may occur on the +right of a function arrow, but never on the left. Hence the above can of worms +is ruled out but the following example of a potentially infinitely branching tree is +accepted: + +\input{Datatype/document/Fundata.tex} +\bigskip + +If you need nested recursion on the left of a function arrow, +there are alternatives to pure HOL: LCF~\cite{paulson87} is a logic where types like +\begin{ttbox} +datatype lam = C (lam -> lam) +\end{ttbox} +do indeed make sense (note the intentionally different arrow \isa{->}!). +There is even a version of LCF on top of HOL, called +HOLCF~\cite{MuellerNvOS99}. + +\index{*primrec|)} +\index{*datatype|)} + +\subsection{Case study: Tries} + +Tries are a classic search tree data structure~\cite{Knuth3-75} for fast +indexing with strings. Figure~\ref{fig:trie} gives a graphical example of a +trie containing the words ``all'', ``an'', ``ape'', ``can'', ``car'' and +``cat''. When searching a string in a trie, the letters of the string are +examined sequentially. Each letter determines which subtrie to search next. +In this case study we model tries as a datatype, define a lookup and an +update function, and prove that they behave as expected. + +\begin{figure}[htbp] +\begin{center} +\unitlength1mm +\begin{picture}(60,30) +\put( 5, 0){\makebox(0,0)[b]{l}} +\put(25, 0){\makebox(0,0)[b]{e}} +\put(35, 0){\makebox(0,0)[b]{n}} +\put(45, 0){\makebox(0,0)[b]{r}} +\put(55, 0){\makebox(0,0)[b]{t}} +% +\put( 5, 9){\line(0,-1){5}} +\put(25, 9){\line(0,-1){5}} +\put(44, 9){\line(-3,-2){9}} +\put(45, 9){\line(0,-1){5}} +\put(46, 9){\line(3,-2){9}} +% +\put( 5,10){\makebox(0,0)[b]{l}} +\put(15,10){\makebox(0,0)[b]{n}} +\put(25,10){\makebox(0,0)[b]{p}} +\put(45,10){\makebox(0,0)[b]{a}} +% +\put(14,19){\line(-3,-2){9}} +\put(15,19){\line(0,-1){5}} +\put(16,19){\line(3,-2){9}} +\put(45,19){\line(0,-1){5}} +% +\put(15,20){\makebox(0,0)[b]{a}} +\put(45,20){\makebox(0,0)[b]{c}} +% +\put(30,30){\line(-3,-2){13}} +\put(30,30){\line(3,-2){13}} +\end{picture} +\end{center} +\caption{A sample trie} +\label{fig:trie} +\end{figure} + +Proper tries associate some value with each string. Since the +information is stored only in the final node associated with the string, many +nodes do not carry any value. This distinction is captured by the +following predefined datatype (from theory \texttt{Option}, which is a parent +of \texttt{Main}): +\input{Trie/document/Option2.tex} +\indexbold{*option}\indexbold{*None}\indexbold{*Some} + +\input{Trie/document/Trie.tex} + +\begin{exercise} + Write an improved version of \isa{update} that does not suffer from the + space leak in the version above. Prove the main theorem for your improved + \isa{update}. +\end{exercise} + +\begin{exercise} + Write a function to \emph{delete} entries from a trie. An easy solution is + a clever modification of \isa{update} which allows both insertion and + deletion with a single function. Prove (a modified version of) the main + theorem above. Optimize you function such that it shrinks tries after + deletion, if possible. +\end{exercise} + +\section{Total recursive functions} +\label{sec:recdef} +\index{*recdef|(} + +Although many total functions have a natural primitive recursive definition, +this is not always the case. Arbitrary total recursive functions can be +defined by means of \isacommand{recdef}: you can use full pattern-matching, +recursion need not involve datatypes, and termination is proved by showing +that the arguments of all recursive calls are smaller in a suitable (user +supplied) sense. + +\subsection{Defining recursive functions} + +\input{Recdef/document/examples.tex} + +\subsection{Proving termination} + +\input{Recdef/document/termination.tex} + +\subsection{Simplification with recdef} + +\input{Recdef/document/simplification.tex} + + +\subsection{Induction} +\index{induction!recursion|(} +\index{recursion induction|(} + +\input{Recdef/document/Induction.tex} + +\index{induction!recursion|)} +\index{recursion induction|)} +\index{*recdef|)} diff -r 8a5b3f58b944 -r 3253c6046d57 doc-src/TutorialI/ttbox.sty --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/doc-src/TutorialI/ttbox.sty Wed Apr 19 11:54:39 2000 +0200 @@ -0,0 +1,20 @@ +\ProvidesPackage{ttbox}[1997/06/25] +\RequirePackage{alltt} + +%%%Boxed terminal sessions + +%Redefines \{ and \} to be in \tt font and \| to make a BACKSLASH +\def\ttbraces{\chardef\{=`\{\chardef\}=`\}\chardef\|=`\\} + +%Restores % as the comment character (especially, to suppress line breaks) +\newcommand\comments{\catcode`\%=14\relax} + +%alltt* environment: like alltt but smaller, and with \{ \} and \| as in ttbox +\newenvironment{alltt*}{\begin{alltt}\footnotesize\ttbraces}{\end{alltt}} + +%Indented alltt* environment with small point size +%NO LINE BREAKS are allowed unless \pagebreak appears at START of a line +\newenvironment{ttbox}{\begin{quote}\samepage\begin{alltt*}}% + {\end{alltt*}\end{quote}} + +\endinput diff -r 8a5b3f58b944 -r 3253c6046d57 doc-src/TutorialI/tutorial.tex --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/doc-src/TutorialI/tutorial.tex Wed Apr 19 11:54:39 2000 +0200 @@ -0,0 +1,78 @@ +\documentclass[11pt,a4paper]{report} +\usepackage{isabelle,isabellesym,pdfsetup} +\usepackage{latexsym,verbatim,graphicx,../iman,extra,comment} + +\usepackage{ttbox} +\newcommand\ttbreak{\vskip-10pt\pagebreak[0]} +\newcommand\Out[1]{\texttt{\textsl{#1}}} %% for output from terminal sessions + +%\newtheorem{theorem}{Theorem}[section] +\newtheorem{Exercise}{Exercise}[section] +\newenvironment{exercise}{\begin{Exercise}\rm}{\end{Exercise}} +\newcommand{\ttlbr}{\texttt{[|}} +\newcommand{\ttrbr}{\texttt{|]}} +\newcommand{\ttor}{\texttt{|}} +\newcommand{\ttall}{\texttt{!}} +\newcommand{\ttuniquex}{\texttt{?!}} +\newcommand{\ttEXU}{\texttt{EX!}} +\newcommand{\ttAnd}{\texttt{!!}} + +\newcommand{\isasymimp}{\isasymlongrightarrow} +\newcommand{\isasymImp}{\isasymLongrightarrow} +\newcommand{\isasymFun}{\isasymRightarrow} +\newcommand{\isasymuniqex}{\emph{$\exists!\,$}} + +\newenvironment{isabellepar}% +{\par\medskip\noindent\begin{isabelle}}{\end{isabelle}\medskip\par\noindent} + +\renewenvironment{isamarkuptxt}{\begin{isamarkuptext}}{\end{isamarkuptext}} + +%%% to index derived rls: ^\([a-zA-Z0-9][a-zA-Z0-9_]*\) \\tdx{\1} +%%% to index rulenames: ^ *(\([a-zA-Z0-9][a-zA-Z0-9_]*\), \\tdx{\1} +%%% to index constants: \\tt \([a-zA-Z0-9][a-zA-Z0-9_]*\) \\cdx{\1} +%%% to deverbify: \\verb|\([^|]*\)| \\ttindex{\1} +%% run ../sedindex logics to prepare index file + +\makeindex +\newcommand{\indexboldpos}[2]{#1\indexbold{#2@#1}} +\newcommand{\ttindexboldpos}[2]{\texttt{#1}\indexbold{#2@\texttt{#1}}} +\newcommand{\isaindexbold}[1]{\isa{#1}\index{*#1|bold}} +\newcommand{\isaindex}[1]{\isa{#1}\index{*#1}} + +\underscoreoff + +\setcounter{secnumdepth}{2} \setcounter{tocdepth}{2} %% {secnumdepth}{2}??? + +\pagestyle{headings} +%\sloppy +%\binperiod %%%treat . like a binary operator + +\begin{document} +\title{\includegraphics[scale=.8]{isabelle_hol} + \\ \vspace{0.5cm} The Tutorial + \\ --- DRAFT ---} +\author{Tobias Nipkow\\ +Technische Universit\"at M\"unchen \\ +Institut f\"ur Informatik \\ +\url{http://www.in.tum.de/~nipkow/}} +\maketitle + +\pagenumbering{roman} +\tableofcontents + +\subsubsection*{Acknowledgements} +This tutorial owes a lot to the constant discussions with and the valuable +feedback from Larry Paulson and the Isabelle group at Munich: Olaf M\"uller, +Wolfgang Naraschewski, David von Oheimb, Leonor Prensa Nieto, Cornelia Pusch +and Markus Wenzel. Stefan Berghofer and Stephan Merz were also kind enough to +read and comment on a draft version. +\clearfirst + +\input{basics} +\input{fp} +\input{appendix} + +\bibliographystyle{plain} +\bibliography{../manual} +\input{tutorial.ind} +\end{document}