src/Doc/Isar_Ref/Preface.thy
author wenzelm
Mon Oct 09 21:12:22 2017 +0200 (23 months ago)
changeset 66822 4642cf4a7ebb
parent 63531 847eefdca90d
permissions -rw-r--r--
tuned signature;
     1 (*:maxLineLen=78:*)
     2 
     3 theory Preface
     4   imports Main Base
     5 begin
     6 
     7 text \<open>
     8   The \<^emph>\<open>Isabelle\<close> 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>\<open>Isar\<close> 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>\<open>Proof~General\<close> 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>
    32   Apart from the technical advances over bare-bones ML
    33   programming, the main purpose of the Isar language is to provide a
    34   conceptually different view on machine-checked proofs
    35   @{cite "Wenzel:1999:TPHOL" and "Wenzel-PhD"}.  \<^emph>\<open>Isar\<close> stands for
    36   \<^emph>\<open>Intelligible semi-automated reasoning\<close>.  Drawing from both the
    37   traditions of informal mathematical proof texts and high-level
    38   programming languages, Isar offers a versatile environment for
    39   structured formal proof documents.  Thus properly written Isar
    40   proofs become accessible to a broader audience than unstructured
    41   tactic scripts (which typically only provide operational information
    42   for the machine).  Writing human-readable proof texts certainly
    43   requires some additional efforts by the writer to achieve a good
    44   presentation, both of formal and informal parts of the text.  On the
    45   other hand, human-readable formal texts gain some value in their own
    46   right, independently of the mechanic proof-checking process.
    47 
    48   Despite its grand design of structured proof texts, Isar is able to
    49   assimilate the old tactical style as an ``improper'' sub-language.
    50   This provides an easy upgrade path for existing tactic scripts, as
    51   well as some means for interactive experimentation and debugging of
    52   structured proofs.  Isabelle/Isar supports a broad range of proof
    53   styles, both readable and unreadable ones.
    54 
    55   \<^medskip>
    56   The generic Isabelle/Isar framework (see
    57   \chref{ch:isar-framework}) works reasonably well for any Isabelle
    58   object-logic that conforms to the natural deduction view of the
    59   Isabelle/Pure framework.  Specific language elements introduced by
    60   Isabelle/HOL are described in \partref{part:hol}.  Although the main
    61   language elements are already provided by the Isabelle/Pure
    62   framework, examples given in the generic parts will usually refer to
    63   Isabelle/HOL.
    64 
    65   \<^medskip>
    66   Isar commands may be either \<^emph>\<open>proper\<close> document
    67   constructors, or \<^emph>\<open>improper commands\<close>.  Some proof methods and
    68   attributes introduced later are classified as improper as well.
    69   Improper Isar language elements, which are marked by ``\<open>\<^sup>*\<close>'' in the subsequent chapters; they are often helpful
    70   when developing proof documents, but their use is discouraged for
    71   the final human-readable outcome.  Typical examples are diagnostic
    72   commands that print terms or theorems according to the current
    73   context; other commands emulate old-style tactical theorem proving.
    74 \<close>
    75 
    76 end