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