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