I wonder if that's all?
authornipkow
Wed Apr 19 11:54:39 2000 +0200 (2000-04-19)
changeset 87433253c6046d57
parent 8742 8a5b3f58b944
child 8744 22fa8b16c3ae
I wonder if that's all?
doc-src/TutorialI/IsaMakefile
doc-src/TutorialI/Makefile
doc-src/TutorialI/appendix.tex
doc-src/TutorialI/basics.tex
doc-src/TutorialI/extra.sty
doc-src/TutorialI/fp.tex
doc-src/TutorialI/ttbox.sty
doc-src/TutorialI/tutorial.tex
     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}