author nipkow Wed, 19 Apr 2000 11:54:39 +0200 changeset 8743 3253c6046d57 parent 8742 8a5b3f58b944 child 8744 22fa8b16c3ae
I wonder if that's all?
 doc-src/TutorialI/IsaMakefile file | annotate | diff | comparison | revisions doc-src/TutorialI/Makefile file | annotate | diff | comparison | revisions doc-src/TutorialI/appendix.tex file | annotate | diff | comparison | revisions doc-src/TutorialI/basics.tex file | annotate | diff | comparison | revisions doc-src/TutorialI/extra.sty file | annotate | diff | comparison | revisions doc-src/TutorialI/fp.tex file | annotate | diff | comparison | revisions doc-src/TutorialI/ttbox.sty file | annotate | diff | comparison | revisions doc-src/TutorialI/tutorial.tex file | annotate | diff | comparison | revisions
--- /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 --- /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) --- /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}
--- /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
+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
+
+\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
+\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. --- /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}}
+
+\def\@rulehead#1{\hrule height1pt \vskip 14pt \Huge \bf
+   #1 \vskip 14pt\hrule height1pt}
+ \ifnum\c@secnumdepth >\m@ne \raggedleft\large\bf\@chapapp{} \thechapter \par
+ \vskip 20pt \fi \raggedright \@rulehead{#1} \par \nobreak \vskip 40pt } }
+
+ \@rulehead{#1} \par \nobreak \vskip 40pt } }
+
--- /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
+
+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}
+\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}
+
+
+\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}.
+  \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.
+  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
+
+\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}???
+
+%\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}