src/Doc/Isar_Ref/Preface.thy
 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

     4

     5 chapter \<open>Preface\<close>

     6

     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.

    14

    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.

    21

    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.

    30

    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.

    46

    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.

    53

    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.

    62

    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>

    73

    74 end