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: