1 |
1 |
2 \chapter{Introduction} |
2 \chapter{Introduction} |
|
3 |
|
4 \section{Overview} |
|
5 |
|
6 The \emph{Isabelle} system essentially provides a generic infrastructure for |
|
7 building deductive systems (programmed in Standard ML), with a special focus |
|
8 on interactive theorem proving in higher-order logics. In the olden days even |
|
9 end-users would refer to certain ML functions (goal commands, tactics, |
|
10 tacticals etc.) to pursue their everyday theorem proving needs |
|
11 \cite{isabelle-intro,isabelle-ref}. |
|
12 |
|
13 In contrast \emph{Isar} provides an interpreted language environment of its |
|
14 own, which has been specifically tailored for the needs of theory and proof |
|
15 development. Compared to raw ML, the Isabelle/Isar top-level provides a more |
|
16 robust and comfortable development platform, with proper support for theory |
|
17 development graphs, single-step evaluation with unlimited undo, etc. The |
|
18 Isabelle/Isar version of the \emph{Proof~General} user interface |
|
19 \cite{proofgeneral,Aspinall:TACAS:2000} provides an adequate front-end for |
|
20 interactive theory and proof development. |
|
21 |
|
22 \medskip Apart from these technical advances over bare-bones ML programming, |
|
23 the main intention of Isar is to provide a conceptually different view on |
|
24 machine-checked proofs \cite{Wenzel:1999:TPHOL, Wenzel-PhD} --- ``Isar'' |
|
25 stands for ``Intelligible semi-automated reasoning''. Drawing from both the |
|
26 traditions of informal mathematical proof texts and high-level programming |
|
27 languages, Isar provides a versatile environment for structured formal proof |
|
28 documents. Thus properly written Isar proof texts become accessible to a |
|
29 broader audience than unstructured tactic scripts (which typically only |
|
30 provide operational information for the machine). Writing human-readable |
|
31 proof texts certainly requires some additional efforts by the writer in order |
|
32 to achieve a good presentation --- both of formal and informal parts of the |
|
33 text. On the other hand, human-readable formal texts gain some value in their |
|
34 own right, independently of the mechanic proof-checking process. |
|
35 |
|
36 Despite its grand design of structured proof texts, Isar is able to assimilate |
|
37 the old-style tactical as an ``improper'' sub-language. This provides an easy |
|
38 upgrade path for existing tactic scripts, as well as additional means for |
|
39 experimentation and debugging of interactive proofs. Isabelle/Isar freely |
|
40 supports a broad range of proof styles, including unreadable ones. |
|
41 |
|
42 \medskip The Isabelle/Isar framework generic and should work for reasonably |
|
43 well for any object-logic that directly conforms to the view of natural |
|
44 deduction according to the Isabelle/Pure framework. Major Isabelle logics |
|
45 (HOL \cite{isabelle-HOL}, HOLCF, FOL \cite{isabelle-logics}, ZF |
|
46 \cite{isabelle-ZF}) have already been setup for immediate use by end-users. |
|
47 |
|
48 Note that much of the existing body of theories still consist of old-style |
|
49 theory files with accompanied ML code for proof scripts. This legacy will be |
|
50 converted as time goes by. |
|
51 |
3 |
52 |
4 \section{Quick start} |
53 \section{Quick start} |
5 |
54 |
6 \subsection{Terminal sessions} |
55 \subsection{Terminal sessions} |
7 |
56 |