doc-src/IsarRef/intro.tex
changeset 12618 43a97a2155d0
parent 11041 e07b601e2b5a
child 12621 48cafea0684b
--- a/doc-src/IsarRef/intro.tex	Wed Jan 02 21:52:54 2002 +0100
+++ b/doc-src/IsarRef/intro.tex	Wed Jan 02 21:53:50 2002 +0100
@@ -1,6 +1,55 @@
 
 \chapter{Introduction}
 
+\section{Overview}
+
+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.  In the olden days even
+end-users would refer to certain ML functions (goal commands, tactics,
+tacticals etc.) to pursue their everyday theorem proving needs
+\cite{isabelle-intro,isabelle-ref}.
+  
+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, single-step evaluation with unlimited undo, etc.  The
+Isabelle/Isar version of the \emph{Proof~General} user interface
+\cite{proofgeneral,Aspinall:TACAS:2000} provides an adequate front-end for
+interactive theory and proof development.
+
+\medskip Apart from these technical advances over bare-bones ML programming,
+the main intention of Isar is to provide a conceptually different view on
+machine-checked proofs \cite{Wenzel:1999:TPHOL, Wenzel-PhD} --- ``Isar''
+stands for ``Intelligible semi-automated reasoning''.  Drawing from both the
+traditions of informal mathematical proof texts and high-level programming
+languages, Isar provides a versatile environment for structured formal proof
+documents.  Thus properly written Isar proof texts 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 in order
+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-style tactical as an ``improper'' sub-language.  This provides an easy
+upgrade path for existing tactic scripts, as well as additional means for
+experimentation and debugging of interactive proofs.  Isabelle/Isar freely
+supports a broad range of proof styles, including unreadable ones.
+
+\medskip The Isabelle/Isar framework generic and should work for reasonably
+well for any object-logic that directly conforms to the view of natural
+deduction according to the Isabelle/Pure framework.  Major Isabelle logics
+(HOL \cite{isabelle-HOL}, HOLCF, FOL \cite{isabelle-logics}, ZF
+\cite{isabelle-ZF}) have already been setup for immediate use by end-users.
+
+Note that much of the existing body of theories still consist of old-style
+theory files with accompanied ML code for proof scripts.  This legacy will be
+converted as time goes by.
+
+
 \section{Quick start}
 
 \subsection{Terminal sessions}