doc-src/IsarRef/Thy/Introduction.thy

-theory Introduction
-imports Base Main
-begin
-
-chapter {* Introduction *}
-
-section {* Overview *}
-
-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.  The Isabelle/Isar version of
-  the \emph{Proof~General} user interface
-  \cite{proofgeneral,Aspinall:TACAS:2000} provides a decent front-end
-  for interactive theory and proof development in this advanced
-  theorem proving environment, even though it is somewhat biased
-  towards old-style proof scripts.
-
-  \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
-  the major object-logics are described in \chref{ch:hol}
-  (Isabelle/HOL), \chref{ch:holcf} (Isabelle/HOLCF), and \chref{ch:zf}
-  (Isabelle/ZF).  The main language elements are already provided by
-  the Isabelle/Pure framework. Nevertheless, examples given in the
-  generic parts will usually refer to Isabelle/HOL as well.
-
-  \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