src/Doc/Isar_Ref/Preface.thy

Merged

(*:maxLineLen=78:*)

theory Preface
imports Base Main
begin

text \<open>
  The \<^emph>\<open>Isabelle\<close> system essentially provides a generic
  infrastructure for building deductive systems (programmed in
  Standard ML), with a special focus on interactive theorem proving in
  higher-order logics.  Many years ago, even end-users would refer to
  certain ML functions (goal commands, tactics, tacticals etc.) to
  pursue their everyday theorem proving tasks.
  
  In contrast \<^emph>\<open>Isar\<close> provides an interpreted language environment
  of its own, which has been specifically tailored for the needs of
  theory and proof development.  Compared to raw ML, the Isabelle/Isar
  top-level provides a more robust and comfortable development
  platform, with proper support for theory development graphs, managed
  transactions with unlimited undo etc.

  In its pioneering times, the Isabelle/Isar version of the
  \<^emph>\<open>Proof~General\<close> user interface @{cite proofgeneral and
  "Aspinall:TACAS:2000"} has contributed to the
  success of for interactive theory and proof development in this
  advanced theorem proving environment, even though it was somewhat
  biased towards old-style proof scripts.  The more recent
  Isabelle/jEdit Prover IDE @{cite "Wenzel:2012"} emphasizes the
  document-oriented approach of Isabelle/Isar again more explicitly.

  \<^medskip>
  Apart from the technical advances over bare-bones ML
  programming, the main purpose of the Isar language is to provide a
  conceptually different view on machine-checked proofs
  @{cite "Wenzel:1999:TPHOL" and "Wenzel-PhD"}.  \<^emph>\<open>Isar\<close> stands for
  \<^emph>\<open>Intelligible semi-automated reasoning\<close>.  Drawing from both the
  traditions of informal mathematical proof texts and high-level
  programming languages, Isar offers a versatile environment for
  structured formal proof documents.  Thus properly written Isar
  proofs become accessible to a broader audience than unstructured
  tactic scripts (which typically only provide operational information
  for the machine).  Writing human-readable proof texts certainly
  requires some additional efforts by the writer to achieve a good
  presentation, both of formal and informal parts of the text.  On the
  other hand, human-readable formal texts gain some value in their own
  right, independently of the mechanic proof-checking process.

  Despite its grand design of structured proof texts, Isar is able to
  assimilate the old tactical style as an ``improper'' sub-language.
  This provides an easy upgrade path for existing tactic scripts, as
  well as some means for interactive experimentation and debugging of
  structured proofs.  Isabelle/Isar supports a broad range of proof
  styles, both readable and unreadable ones.

  \<^medskip>
  The generic Isabelle/Isar framework (see
  \chref{ch:isar-framework}) works reasonably well for any Isabelle
  object-logic that conforms to the natural deduction view of the
  Isabelle/Pure framework.  Specific language elements introduced by
  Isabelle/HOL are described in \partref{part:hol}.  Although the main
  language elements are already provided by the Isabelle/Pure
  framework, examples given in the generic parts will usually refer to
  Isabelle/HOL.

  \<^medskip>
  Isar commands may be either \<^emph>\<open>proper\<close> document
  constructors, or \<^emph>\<open>improper commands\<close>.  Some proof methods and
  attributes introduced later are classified as improper as well.
  Improper Isar language elements, which are marked by ``\<open>\<^sup>*\<close>'' in the subsequent chapters; they are often helpful
  when developing proof documents, but their use is discouraged for
  the final human-readable outcome.  Typical examples are diagnostic
  commands that print terms or theorems according to the current
  context; other commands emulate old-style tactical theorem proving.
\<close>

end