doc-src/IsarRef/Thy/document/Introduction.tex
author wenzelm
Fri Oct 29 11:49:56 2010 +0200 (2010-10-29)
changeset 40255 9ffbc25e1606
parent 30242 aea5d7fa7ef5
child 40406 313a24b66a8d
permissions -rw-r--r--
eliminated obsolete \_ escapes in rail environments;
     1 %
     2 \begin{isabellebody}%
     3 \def\isabellecontext{Introduction}%
     4 %
     5 \isadelimtheory
     6 %
     7 \endisadelimtheory
     8 %
     9 \isatagtheory
    10 \isacommand{theory}\isamarkupfalse%
    11 \ Introduction\isanewline
    12 \isakeyword{imports}\ Main\isanewline
    13 \isakeyword{begin}%
    14 \endisatagtheory
    15 {\isafoldtheory}%
    16 %
    17 \isadelimtheory
    18 %
    19 \endisadelimtheory
    20 %
    21 \isamarkupchapter{Introduction%
    22 }
    23 \isamarkuptrue%
    24 %
    25 \isamarkupsection{Overview%
    26 }
    27 \isamarkuptrue%
    28 %
    29 \begin{isamarkuptext}%
    30 The \emph{Isabelle} system essentially provides a generic
    31   infrastructure for building deductive systems (programmed in
    32   Standard ML), with a special focus on interactive theorem proving in
    33   higher-order logics.  Many years ago, even end-users would refer to
    34   certain ML functions (goal commands, tactics, tacticals etc.) to
    35   pursue their everyday theorem proving tasks.
    36   
    37   In contrast \emph{Isar} provides an interpreted language environment
    38   of its own, which has been specifically tailored for the needs of
    39   theory and proof development.  Compared to raw ML, the Isabelle/Isar
    40   top-level provides a more robust and comfortable development
    41   platform, with proper support for theory development graphs, managed
    42   transactions with unlimited undo etc.  The Isabelle/Isar version of
    43   the \emph{Proof~General} user interface
    44   \cite{proofgeneral,Aspinall:TACAS:2000} provides a decent front-end
    45   for interactive theory and proof development in this advanced
    46   theorem proving environment, even though it is somewhat biased
    47   towards old-style proof scripts.
    48 
    49   \medskip Apart from the technical advances over bare-bones ML
    50   programming, the main purpose of the Isar language is to provide a
    51   conceptually different view on machine-checked proofs
    52   \cite{Wenzel:1999:TPHOL,Wenzel-PhD}.  \emph{Isar} stands for
    53   \emph{Intelligible semi-automated reasoning}.  Drawing from both the
    54   traditions of informal mathematical proof texts and high-level
    55   programming languages, Isar offers a versatile environment for
    56   structured formal proof documents.  Thus properly written Isar
    57   proofs become accessible to a broader audience than unstructured
    58   tactic scripts (which typically only provide operational information
    59   for the machine).  Writing human-readable proof texts certainly
    60   requires some additional efforts by the writer to achieve a good
    61   presentation, both of formal and informal parts of the text.  On the
    62   other hand, human-readable formal texts gain some value in their own
    63   right, independently of the mechanic proof-checking process.
    64 
    65   Despite its grand design of structured proof texts, Isar is able to
    66   assimilate the old tactical style as an ``improper'' sub-language.
    67   This provides an easy upgrade path for existing tactic scripts, as
    68   well as some means for interactive experimentation and debugging of
    69   structured proofs.  Isabelle/Isar supports a broad range of proof
    70   styles, both readable and unreadable ones.
    71 
    72   \medskip The generic Isabelle/Isar framework (see
    73   \chref{ch:isar-framework}) works reasonably well for any Isabelle
    74   object-logic that conforms to the natural deduction view of the
    75   Isabelle/Pure framework.  Specific language elements introduced by
    76   the major object-logics are described in \chref{ch:hol}
    77   (Isabelle/HOL), \chref{ch:holcf} (Isabelle/HOLCF), and \chref{ch:zf}
    78   (Isabelle/ZF).  The main language elements are already provided by
    79   the Isabelle/Pure framework. Nevertheless, examples given in the
    80   generic parts will usually refer to Isabelle/HOL as well.
    81 
    82   \medskip Isar commands may be either \emph{proper} document
    83   constructors, or \emph{improper commands}.  Some proof methods and
    84   attributes introduced later are classified as improper as well.
    85   Improper Isar language elements, which are marked by ``\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}}'' in the subsequent chapters; they are often helpful
    86   when developing proof documents, but their use is discouraged for
    87   the final human-readable outcome.  Typical examples are diagnostic
    88   commands that print terms or theorems according to the current
    89   context; other commands emulate old-style tactical theorem proving.%
    90 \end{isamarkuptext}%
    91 \isamarkuptrue%
    92 %
    93 \isadelimtheory
    94 %
    95 \endisadelimtheory
    96 %
    97 \isatagtheory
    98 \isacommand{end}\isamarkupfalse%
    99 %
   100 \endisatagtheory
   101 {\isafoldtheory}%
   102 %
   103 \isadelimtheory
   104 %
   105 \endisadelimtheory
   106 \isanewline
   107 \end{isabellebody}%
   108 %%% Local Variables:
   109 %%% mode: latex
   110 %%% TeX-master: "root"
   111 %%% End: