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