author wenzelm
Wed Mar 25 11:39:52 2015 +0100 (2015-03-25)
changeset 59809 87641097d0f3
parent 58618 782f0b662cae
child 60286 410115884a92
permissions -rw-r--r--
tuned signature;
     1 theory Preface
     2 imports Base Main
     3 begin
     5 chapter \<open>Preface\<close>
     7 text \<open>
     8   The \emph{Isabelle} system essentially provides a generic
     9   infrastructure for building deductive systems (programmed in
    10   Standard ML), with a special focus on interactive theorem proving in
    11   higher-order logics.  Many years ago, even end-users would refer to
    12   certain ML functions (goal commands, tactics, tacticals etc.) to
    13   pursue their everyday theorem proving tasks.
    15   In contrast \emph{Isar} provides an interpreted language environment
    16   of its own, which has been specifically tailored for the needs of
    17   theory and proof development.  Compared to raw ML, the Isabelle/Isar
    18   top-level provides a more robust and comfortable development
    19   platform, with proper support for theory development graphs, managed
    20   transactions with unlimited undo etc.
    22   In its pioneering times, the Isabelle/Isar version of the
    23   \emph{Proof~General} user interface @{cite proofgeneral and
    24   "Aspinall:TACAS:2000"} has contributed to the
    25   success of for interactive theory and proof development in this
    26   advanced theorem proving environment, even though it was somewhat
    27   biased towards old-style proof scripts.  The more recent
    28   Isabelle/jEdit Prover IDE @{cite "Wenzel:2012"} emphasizes the
    29   document-oriented approach of Isabelle/Isar again more explicitly.
    31   \medskip Apart from the technical advances over bare-bones ML
    32   programming, the main purpose of the Isar language is to provide a
    33   conceptually different view on machine-checked proofs
    34   @{cite "Wenzel:1999:TPHOL" and "Wenzel-PhD"}.  \emph{Isar} stands for
    35   \emph{Intelligible semi-automated reasoning}.  Drawing from both the
    36   traditions of informal mathematical proof texts and high-level
    37   programming languages, Isar offers a versatile environment for
    38   structured formal proof documents.  Thus properly written Isar
    39   proofs become accessible to a broader audience than unstructured
    40   tactic scripts (which typically only provide operational information
    41   for the machine).  Writing human-readable proof texts certainly
    42   requires some additional efforts by the writer to achieve a good
    43   presentation, both of formal and informal parts of the text.  On the
    44   other hand, human-readable formal texts gain some value in their own
    45   right, independently of the mechanic proof-checking process.
    47   Despite its grand design of structured proof texts, Isar is able to
    48   assimilate the old tactical style as an ``improper'' sub-language.
    49   This provides an easy upgrade path for existing tactic scripts, as
    50   well as some means for interactive experimentation and debugging of
    51   structured proofs.  Isabelle/Isar supports a broad range of proof
    52   styles, both readable and unreadable ones.
    54   \medskip The generic Isabelle/Isar framework (see
    55   \chref{ch:isar-framework}) works reasonably well for any Isabelle
    56   object-logic that conforms to the natural deduction view of the
    57   Isabelle/Pure framework.  Specific language elements introduced by
    58   Isabelle/HOL are described in \partref{part:hol}.  Although the main
    59   language elements are already provided by the Isabelle/Pure
    60   framework, examples given in the generic parts will usually refer to
    61   Isabelle/HOL.
    63   \medskip Isar commands may be either \emph{proper} document
    64   constructors, or \emph{improper commands}.  Some proof methods and
    65   attributes introduced later are classified as improper as well.
    66   Improper Isar language elements, which are marked by ``@{text
    67   "\<^sup>*"}'' in the subsequent chapters; they are often helpful
    68   when developing proof documents, but their use is discouraged for
    69   the final human-readable outcome.  Typical examples are diagnostic
    70   commands that print terms or theorems according to the current
    71   context; other commands emulate old-style tactical theorem proving.
    72 \<close>
    74 end