5 chapter {* Introduction *}
10 The \emph{Isabelle} system essentially provides a generic
11 infrastructure for building deductive systems (programmed in
12 Standard ML), with a special focus on interactive theorem proving in
13 higher-order logics. Many years ago, even end-users would refer to
14 certain ML functions (goal commands, tactics, tacticals etc.) to
15 pursue their everyday theorem proving tasks.
17 In contrast \emph{Isar} provides an interpreted language environment
18 of its own, which has been specifically tailored for the needs of
19 theory and proof development. Compared to raw ML, the Isabelle/Isar
20 top-level provides a more robust and comfortable development
21 platform, with proper support for theory development graphs, managed
22 transactions with unlimited undo etc. The Isabelle/Isar version of
23 the \emph{Proof~General} user interface
24 \cite{proofgeneral,Aspinall:TACAS:2000} provides a decent front-end
25 for interactive theory and proof development in this advanced
26 theorem proving environment, even though it is somewhat biased
27 towards old-style proof scripts.
29 \medskip Apart from the technical advances over bare-bones ML
30 programming, the main purpose of the Isar language is to provide a
31 conceptually different view on machine-checked proofs
32 \cite{Wenzel:1999:TPHOL,Wenzel-PhD}. \emph{Isar} stands for
33 \emph{Intelligible semi-automated reasoning}. Drawing from both the
34 traditions of informal mathematical proof texts and high-level
35 programming languages, Isar offers a versatile environment for
36 structured formal proof documents. Thus properly written Isar
37 proofs become accessible to a broader audience than unstructured
38 tactic scripts (which typically only provide operational information
39 for the machine). Writing human-readable proof texts certainly
40 requires some additional efforts by the writer to achieve a good
41 presentation, both of formal and informal parts of the text. On the
42 other hand, human-readable formal texts gain some value in their own
43 right, independently of the mechanic proof-checking process.
45 Despite its grand design of structured proof texts, Isar is able to
46 assimilate the old tactical style as an ``improper'' sub-language.
47 This provides an easy upgrade path for existing tactic scripts, as
48 well as some means for interactive experimentation and debugging of
49 structured proofs. Isabelle/Isar supports a broad range of proof
50 styles, both readable and unreadable ones.
52 \medskip The generic Isabelle/Isar framework (see
53 \chref{ch:isar-framework}) works reasonably well for any Isabelle
54 object-logic that conforms to the natural deduction view of the
55 Isabelle/Pure framework. Specific language elements introduced by
56 the major object-logics are described in \chref{ch:hol}
57 (Isabelle/HOL), \chref{ch:holcf} (Isabelle/HOLCF), and \chref{ch:zf}
58 (Isabelle/ZF). The main language elements are already provided by
59 the Isabelle/Pure framework. Nevertheless, examples given in the
60 generic parts will usually refer to Isabelle/HOL as well.
62 \medskip Isar commands may be either \emph{proper} document
63 constructors, or \emph{improper commands}. Some proof methods and
64 attributes introduced later are classified as improper as well.
65 Improper Isar language elements, which are marked by ``@{text
66 "\<^sup>*"}'' in the subsequent chapters; they are often helpful
67 when developing proof documents, but their use is discouraged for
68 the final human-readable outcome. Typical examples are diagnostic
69 commands that print terms or theorems according to the current
70 context; other commands emulate old-style tactical theorem proving.