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}