doc-src/Intro/intro.tex
 author lcp Tue Jul 25 16:52:08 1995 +0200 (1995-07-25) changeset 1186 906c32af858d parent 873 0cfc734e3dbd child 1866 a1a41b4b02e7 permissions -rw-r--r--
now uses proof209.sty
     1 \documentstyle[a4,12pt,proof209,iman,extra]{article}

     2 %% $Id$

     3 %% run    bibtex intro         to prepare bibliography

     4 %% run    ../sedindex intro    to prepare index file

     5 %prth *($$.*$$);          \1;

     6 %{\\out $$.*$$}          {\\out val it = "\1" : thm}

     7

     8 \title{Introduction to Isabelle}

     9 \author{{\em Lawrence C. Paulson}\\

    10         Computer Laboratory \\ University of Cambridge \\[2ex]

    11         {\small{\em Electronic mail\/}: {\tt lcp@cl.cam.ac.uk}}

    12 }

    13 \date{}

    14 \makeindex

    15

    16 \underscoreoff

    17

    18 \setcounter{secnumdepth}{2} \setcounter{tocdepth}{2}

    19

    20 \sloppy

    21 \binperiod     %%%treat . like a binary operator

    22

    23 \newcommand\qeq{\stackrel{?}{\equiv}}  %for disagreement pairs in unification

    24 \newcommand{\nand}{\mathbin{\lnot\&}}

    25 \newcommand{\xor}{\mathbin{\#}}

    26

    27 \pagenumbering{roman}

    28 \begin{document}

    29 \pagestyle{empty}

    30 \begin{titlepage}

    31 \maketitle

    32 \thispagestyle{empty}

    33 \vfill

    34 {\small Copyright \copyright{} \number\year{} by Lawrence C. Paulson}

    35 \end{titlepage}

    36

    37 \pagestyle{headings}

    38 \part*{Preface}

    39 \index{Isabelle!overview}

    40 \index{Isabelle!object-logics supported}

    41 Isabelle~\cite{paulson86,paulson89,paulson700} is a generic theorem prover.

    42 It has been instantiated to support reasoning in several object-logics:

    43 \begin{itemize}

    44 \item first-order logic, constructive and classical versions

    45 \item higher-order logic, similar to that of Gordon's {\sc

    46 hol}~\cite{mgordon-hol}

    47 \item Zermelo-Fraenkel set theory~\cite{suppes72}

    48 \item an extensional version of Martin-L\"of's Type Theory~\cite{nordstrom90}

    49 \item the classical first-order sequent calculus, {\sc lk}

    50 \item the modal logics $T$, $S4$, and $S43$

    51 \item the Logic for Computable Functions~\cite{paulson87}

    52 \end{itemize}

    53 A logic's syntax and inference rules are specified declaratively; this

    54 allows single-step proof construction.  Isabelle provides control

    55 structures for expressing search procedures.  Isabelle also provides

    56 several generic tools, such as simplifiers and classical theorem provers,

    57 which can be applied to object-logics.

    58

    59 \index{ML}

    60 Isabelle is a large system, but beginners can get by with a small

    61 repertoire of commands and a basic knowledge of how Isabelle works.  Some

    62 knowledge of Standard~\ML{} is essential, because \ML{} is Isabelle's user

    63 interface.  Advanced Isabelle theorem proving can involve writing \ML{}

    64 code, possibly with Isabelle's sources at hand.  My book

    65 on~\ML{}~\cite{paulson91} covers much material connected with Isabelle,

    66 including a simple theorem prover.  Users must be familiar with logic as

    67 used in computer science; there are many good

    68 texts~\cite{galton90,reeves90}.

    69

    70 \index{LCF}

    71 {\sc lcf}, developed by Robin Milner and colleagues~\cite{mgordon79}, is an

    72 ancestor of {\sc hol}, Nuprl, and several other systems.  Isabelle borrows

    73 ideas from {\sc lcf}: formulae are~\ML{} values; theorems belong to an

    74 abstract type; tactics and tacticals support backward proof.  But {\sc lcf}

    75 represents object-level rules by functions, while Isabelle represents them

    76 by terms.  You may find my other writings~\cite{paulson87,paulson-handbook}

    77 helpful in understanding the relationship between {\sc lcf} and Isabelle.

    78

    79 \index{Isabelle!release history} Isabelle was first distributed in 1986.

    80 The 1987 version introduced a higher-order meta-logic with an improved

    81 treatment of quantifiers.  The 1988 version added limited polymorphism and

    82 support for natural deduction.  The 1989 version included a parser and

    83 pretty printer generator.  The 1992 version introduced type classes, to

    84 support many-sorted and higher-order logics.  The current version provides

    85 greater support for theories and is much faster.  Isabelle is still under

    86 development and will continue to change.

    87

    88 \subsubsection*{Overview}

    89 This manual consists of three parts.  Part~I discusses the Isabelle's

    90 foundations.  Part~II, presents simple on-line sessions, starting with

    91 forward proof.  It also covers basic tactics and tacticals, and some

    92 commands for invoking them.  Part~III contains further examples for users

    93 with a bit of experience.  It explains how to derive rules define theories,

    94 and concludes with an extended example: a Prolog interpreter.

    95

    96 Isabelle's Reference Manual and Object-Logics manual contain more details.

    97 They assume familiarity with the concepts presented here.

    98

    99

   100 \subsubsection*{Acknowledgements}

   101 Tobias Nipkow contributed most of the section on defining theories.

   102 Sara Kalvala and Markus Wenzel suggested improvements.

   103

   104 Tobias Nipkow has made immense contributions to Isabelle, including the

   105 parser generator, type classes, and the simplifier.  Carsten Clasohm and

   106 Markus Wenzel made major contributions; Sonia Mahjoub and Karin Nimmermann

   107 also helped.  Isabelle was developed using Dave Matthews's Standard~{\sc

   108   ml} compiler, Poly/{\sc ml}.  Many people have contributed to Isabelle's

   109 standard object-logics, including Martin Coen, Philippe de Groote, Philippe

   110 No\"el.  The research has been funded by the SERC (grants GR/G53279,

   111 GR/H40570) and by ESPRIT (projects 3245: Logical Frameworks, and 6453:

   112 Types).

   113

   114 \newpage

   115 \pagestyle{plain} \tableofcontents

   116 \newpage

   117

   118 \newfont{\sanssi}{cmssi12}

   119 \vspace*{2.5cm}

   120 \begin{quote}

   121 \raggedleft

   122 {\sanssi

   123 You can only find truth with logic\\

   124 if you have already found truth without it.}\\

   125 \bigskip

   126

   127 G.K. Chesterton, {\em The Man who was Orthodox}

   128 \end{quote}

   129

   130 \clearfirst  \pagestyle{headings}

   131 \include{foundations}

   132 \include{getting}

   133 \include{advanced}

   134

   135 \bibliographystyle{plain} \small\raggedright\frenchspacing

   136 \bibliography{string,atp,funprog,general,logicprog,isabelle,theory,crossref}

   137

   138 \input{intro.ind}

   139 \end{document}
{"extraction_info": {"found_math": true, "script_math_tex": 0, "script_math_asciimath": 0, "math_annotations": 0, "math_alttext": 0, "mathml": 0, "mathjax_tag": 0, "mathjax_inline_tex": 1, "mathjax_display_tex": 1, "mathjax_asciimath": 1, "img_math": 0, "codecogs_latex": 0, "wp_latex": 0, "mimetex.cgi": 0, "/images/math/codecogs": 0, "mathtex.cgi": 0, "katex": 0, "math-container": 0, "wp-katex-eq": 0, "align": 0, "equation": 0, "x-ck12": 0, "texerror": 0, "math_score": 0.8703287243843079, "perplexity": 13088.783076398462}, "config": {"markdown_headings": true, "markdown_code": true, "boilerplate_config": {"ratio_threshold": 0.18, "absolute_threshold": 10, "end_threshold": 15, "enable": true}, "remove_buttons": true, "remove_image_figures": true, "remove_link_clusters": true, "table_config": {"min_rows": 2, "min_cols": 3, "format": "plain"}, "remove_chinese": true, "remove_edit_buttons": true, "extract_latex": true}, "warc_path": "s3://commoncrawl/crawl-data/CC-MAIN-2019-51/segments/1575540530857.12/warc/CC-MAIN-20191211103140-20191211131140-00438.warc.gz"}