src/Doc/Intro/document/root.tex
author haftmann
Sun Oct 08 22:28:22 2017 +0200 (23 months ago)
changeset 66816 212a3334e7da
parent 48985 5386df44a037
permissions -rw-r--r--
more fundamental definition of div and mod on int
     1 \documentclass[12pt,a4paper]{article}
     2 \usepackage{graphicx,iman,extra,ttbox,proof,pdfsetup}
     3 
     4 %% run    bibtex intro         to prepare bibliography
     5 %% run    ../sedindex intro    to prepare index file
     6 %prth *(\(.*\));          \1;      
     7 %{\\out \(.*\)}          {\\out val it = "\1" : thm}
     8 
     9 \title{\includegraphics[scale=0.5]{isabelle} \\[4ex] Old Introduction to Isabelle}   
    10 \author{{\em Lawrence C. Paulson}\\
    11         Computer Laboratory \\ University of Cambridge \\
    12         \texttt{lcp@cl.cam.ac.uk}\\[3ex] 
    13         With Contributions by Tobias Nipkow and Markus Wenzel
    14 }
    15 \makeindex
    16 
    17 \underscoreoff
    18 
    19 \setcounter{secnumdepth}{2} \setcounter{tocdepth}{2}
    20 
    21 \sloppy
    22 \binperiod     %%%treat . like a binary operator
    23 
    24 \newcommand\qeq{\stackrel{?}{\equiv}}  %for disagreement pairs in unification
    25 \newcommand{\nand}{\mathbin{\lnot\&}} 
    26 \newcommand{\xor}{\mathbin{\#}}
    27 
    28 \pagenumbering{roman} 
    29 \begin{document}
    30 \pagestyle{empty}
    31 \begin{titlepage}
    32 \maketitle 
    33 \emph{Note}: this document is part of the earlier Isabelle documentation, 
    34 which is largely superseded by the Isabelle/HOL
    35 \emph{Tutorial}~\cite{isa-tutorial}. It describes the old-style theory 
    36 syntax and shows how to conduct proofs using the 
    37 ML top level. This style of interaction is largely obsolete:
    38 most Isabelle proofs are now written using the Isar 
    39 language and the Proof General interface. However, this paper contains valuable 
    40 information that is not available elsewhere. Its examples are based 
    41 on first-order logic rather than higher-order logic.
    42 
    43 \thispagestyle{empty}
    44 \vfill
    45 {\small Copyright \copyright{} \number\year{} by Lawrence C. Paulson}
    46 \end{titlepage}
    47 
    48 \pagestyle{headings}
    49 \part*{Preface}
    50 \index{Isabelle!overview} \index{Isabelle!object-logics supported}
    51 Isabelle~\cite{paulson-natural,paulson-found,paulson700} is a generic theorem
    52 prover.  It has been instantiated to support reasoning in several
    53 object-logics:
    54 \begin{itemize}
    55 \item first-order logic, constructive and classical versions
    56 \item higher-order logic, similar to that of Gordon's {\sc
    57 hol}~\cite{mgordon-hol}
    58 \item Zermelo-Fraenkel set theory~\cite{suppes72}
    59 \item an extensional version of Martin-L\"of's Type Theory~\cite{nordstrom90}
    60 \item the classical first-order sequent calculus, {\sc lk}
    61 \item the modal logics $T$, $S4$, and $S43$
    62 \item the Logic for Computable Functions~\cite{paulson87}
    63 \end{itemize}
    64 A logic's syntax and inference rules are specified declaratively; this
    65 allows single-step proof construction.  Isabelle provides control
    66 structures for expressing search procedures.  Isabelle also provides
    67 several generic tools, such as simplifiers and classical theorem provers,
    68 which can be applied to object-logics.
    69 
    70 Isabelle is a large system, but beginners can get by with a small
    71 repertoire of commands and a basic knowledge of how Isabelle works.  
    72 The Isabelle/HOL \emph{Tutorial}~\cite{isa-tutorial} describes how to get started. Advanced Isabelle users will benefit from some
    73 knowledge of Standard~\ML{}, because Isabelle is written in \ML{};
    74 \index{ML}
    75 if you are prepared to writing \ML{}
    76 code, you can get Isabelle to do almost anything.  My book
    77 on~\ML{}~\cite{paulson-ml2} covers much material connected with Isabelle,
    78 including a simple theorem prover.  Users must be familiar with logic as
    79 used in computer science; there are many good
    80 texts~\cite{galton90,reeves90}.
    81 
    82 \index{LCF}
    83 {\sc lcf}, developed by Robin Milner and colleagues~\cite{mgordon79}, is an
    84 ancestor of {\sc hol}, Nuprl, and several other systems.  Isabelle borrows
    85 ideas from {\sc lcf}: formulae are~\ML{} values; theorems belong to an
    86 abstract type; tactics and tacticals support backward proof.  But {\sc lcf}
    87 represents object-level rules by functions, while Isabelle represents them
    88 by terms.  You may find my other writings~\cite{paulson87,paulson-handbook}
    89 helpful in understanding the relationship between {\sc lcf} and Isabelle.
    90 
    91 \index{Isabelle!release history} Isabelle was first distributed in 1986.
    92 The 1987 version introduced a higher-order meta-logic with an improved
    93 treatment of quantifiers.  The 1988 version added limited polymorphism and
    94 support for natural deduction.  The 1989 version included a parser and
    95 pretty printer generator.  The 1992 version introduced type classes, to
    96 support many-sorted and higher-order logics.  The 1994 version introduced
    97 greater support for theories.  The most important recent change is the
    98 introduction of the Isar proof language, thanks to Markus Wenzel.  
    99 Isabelle is still under
   100 development and will continue to change.
   101 
   102 \subsubsection*{Overview} 
   103 This manual consists of three parts.  Part~I discusses the Isabelle's
   104 foundations.  Part~II, presents simple on-line sessions, starting with
   105 forward proof.  It also covers basic tactics and tacticals, and some
   106 commands for invoking them.  Part~III contains further examples for users
   107 with a bit of experience.  It explains how to derive rules define theories,
   108 and concludes with an extended example: a Prolog interpreter.
   109 
   110 Isabelle's Reference Manual and Object-Logics manual contain more details.
   111 They assume familiarity with the concepts presented here.
   112 
   113 
   114 \subsubsection*{Acknowledgements} 
   115 Tobias Nipkow contributed most of the section on defining theories.
   116 Stefan Berghofer, Sara Kalvala and Viktor Kuncak suggested improvements.
   117 
   118 Tobias Nipkow has made immense contributions to Isabelle, including the parser
   119 generator, type classes, and the simplifier.  Carsten Clasohm and Markus
   120 Wenzel made major contributions; Sonia Mahjoub and Karin Nimmermann also
   121 helped.  Isabelle was developed using Dave Matthews's Standard~{\sc ml}
   122 compiler, Poly/{\sc ml}.  Many people have contributed to Isabelle's standard
   123 object-logics, including Martin Coen, Philippe de Groote, Philippe No\"el.
   124 The research has been funded by the EPSRC (grants GR/G53279, GR/H40570,
   125 GR/K57381, GR/K77051, GR/M75440) and by ESPRIT (projects 3245: Logical
   126 Frameworks, and 6453: Types), and by the DFG Schwerpunktprogramm
   127 \emph{Deduktion}.
   128 
   129 \newpage
   130 \pagestyle{plain} \tableofcontents 
   131 \newpage
   132 
   133 \newfont{\sanssi}{cmssi12}
   134 \vspace*{2.5cm}
   135 \begin{quote}
   136 \raggedleft
   137 {\sanssi
   138 You can only find truth with logic\\
   139 if you have already found truth without it.}\\
   140 \bigskip
   141 
   142 G.K. Chesterton, {\em The Man who was Orthodox}
   143 \end{quote}
   144 
   145 \clearfirst  \pagestyle{headings}
   146 \input{foundations}
   147 \input{getting}
   148 \input{advanced}
   149 
   150 \bibliographystyle{plain} \small\raggedright\frenchspacing
   151 \bibliography{manual}
   152 
   153 \printindex
   154 \end{document}