doc-src/Tutorial/basics.tex
 changeset 6606 94b638b3827c parent 6584 5569f2672662 child 6628 12ed4f748f7c
equal inserted replaced
6605:c2754409919b 6606:94b638b3827c
     8 HOL, which abbreviates Higher-Order Logic. We introduce HOL step by step
     8 HOL, which abbreviates Higher-Order Logic. We introduce HOL step by step
     9 following the equation
     9 following the equation
    10 $\mbox{HOL} = \mbox{Functional Programming} + \mbox{Logic}.$
    10 $\mbox{HOL} = \mbox{Functional Programming} + \mbox{Logic}.$
    11 We assume that the reader is familiar with the basic concepts of both fields.
    11 We assume that the reader is familiar with the basic concepts of both fields.
    12 For excellent introductions to functional programming consult the textbooks
    12 For excellent introductions to functional programming consult the textbooks
    13 by Bird and Wadler~\cite{Bird-Wadler} or Paulson~\cite{Paulson-ML}.  Although
    13 by Bird and Wadler~\cite{Bird-Wadler} or Paulson~\cite{paulson-ml2}.  Although
    14 this tutorial initially concentrates on functional programming, do not be
    14 this tutorial initially concentrates on functional programming, do not be
    15 misled: HOL can express most mathematical concepts, and functional
    15 misled: HOL can express most mathematical concepts, and functional
    16 programming is just one particularly simple and ubiquitous instance.
    16 programming is just one particularly simple and ubiquitous instance.
    17
    17
    18 A tutorial is by definition incomplete. To fully exploit the power of the
    18 A tutorial is by definition incomplete. To fully exploit the power of the
    19 system you need to consult the Isabelle Reference Manual~\cite{Isa-Ref-Man}
    19 system you need to consult the Isabelle Reference Manual~\cite{isabelle-ref}
    20 for details about Isabelle and the HOL chapter of the Logics
    20 for details about Isabelle and the Isabelle/HOL manual~\cite{isabelle-HOL}
    21 manual~\cite{Isa-Logics-Man} for details relating to HOL. Both manuals have a
    21 for details relating to HOL. Both manuals have a comprehensive index.
    22 comprehensive index.

    23
    22
    24 \section{Theories, proofs and interaction}
    23 \section{Theories, proofs and interaction}
    25 \label{sec:Basic:Theories}
    24 \label{sec:Basic:Theories}
    26
    25
    27 Working with Isabelle means creating two different kinds of documents:
    26 Working with Isabelle means creating two different kinds of documents:
    56 \end{warn}
    55 \end{warn}
    57
    56
    58 This tutorial is concerned with introducing you to the different linguistic
    57 This tutorial is concerned with introducing you to the different linguistic
    59 constructs that can fill ${\langle}declarations{\rangle}$ in the above theory template.
    58 constructs that can fill ${\langle}declarations{\rangle}$ in the above theory template.
    60 A complete grammar of the basic constructs is found in Appendix~A
    59 A complete grammar of the basic constructs is found in Appendix~A
    61 of~\cite{Isa-Ref-Man}, for reference in times of doubt.
    60 of~\cite{isabelle-ref}, for reference in times of doubt.
    62
    61
    63 The tutorial is also concerned with showing you how to prove theorems about
    62 The tutorial is also concerned with showing you how to prove theorems about
    64 the concepts in a theory. This involves invoking predefined theorem proving
    63 the concepts in a theory. This involves invoking predefined theorem proving
    65 commands. Because Isabelle is written in the programming language
    64 commands. Because Isabelle is written in the programming language
    66 ML,\footnote{Many concepts in HOL and ML are similar. Make sure you do not
    65 ML,\footnote{Many concepts in HOL and ML are similar. Make sure you do not