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