src/Doc/Isar-Ref/Preface.thy

+theory Preface
+imports Base Main
+begin
+
+chapter {* Preface *}
+
+text {*
+  The \emph{Isabelle} 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{Isar} 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{Proof~General} user interface
+  \cite{proofgeneral,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,Wenzel-PhD}.  \emph{Isar} stands for
+  \emph{Intelligible semi-automated reasoning}.  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{proper} document
+  constructors, or \emph{improper commands}.  Some proof methods and
+  attributes introduced later are classified as improper as well.
+  Improper Isar language elements, which are marked by ``@{text
+  "\<^sup>*"}'' 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.
+*}
+
+end