author | blanchet |
Fri, 24 Feb 2012 11:23:34 +0100 | |
changeset 46641 | 8801a24f9e9a |
parent 42915 | f35aae36cad0 |
child 48957 | c04001b3a753 |
permissions | -rw-r--r-- |
27035 | 1 |
% |
2 |
\begin{isabellebody}% |
|
42915
f35aae36cad0
turned "Overview" into "Preface" (similar to doc-src/Intro/intro.tex);
wenzelm
parents:
42651
diff
changeset
|
3 |
\def\isabellecontext{Preface}% |
27035 | 4 |
% |
5 |
\isadelimtheory |
|
6 |
% |
|
7 |
\endisadelimtheory |
|
8 |
% |
|
9 |
\isatagtheory |
|
10 |
\isacommand{theory}\isamarkupfalse% |
|
42915
f35aae36cad0
turned "Overview" into "Preface" (similar to doc-src/Intro/intro.tex);
wenzelm
parents:
42651
diff
changeset
|
11 |
\ Preface\isanewline |
42651 | 12 |
\isakeyword{imports}\ Base\ Main\isanewline |
27035 | 13 |
\isakeyword{begin}% |
14 |
\endisatagtheory |
|
15 |
{\isafoldtheory}% |
|
16 |
% |
|
17 |
\isadelimtheory |
|
18 |
% |
|
19 |
\endisadelimtheory |
|
20 |
% |
|
42915
f35aae36cad0
turned "Overview" into "Preface" (similar to doc-src/Intro/intro.tex);
wenzelm
parents:
42651
diff
changeset
|
21 |
\isamarkupchapter{Preface% |
27035 | 22 |
} |
23 |
\isamarkuptrue% |
|
24 |
% |
|
25 |
\begin{isamarkuptext}% |
|
26 |
The \emph{Isabelle} system essentially provides a generic |
|
27 |
infrastructure for building deductive systems (programmed in |
|
28 |
Standard ML), with a special focus on interactive theorem proving in |
|
29746 | 29 |
higher-order logics. Many years ago, even end-users would refer to |
30 |
certain ML functions (goal commands, tactics, tacticals etc.) to |
|
31 |
pursue their everyday theorem proving tasks. |
|
27035 | 32 |
|
33 |
In contrast \emph{Isar} provides an interpreted language environment |
|
34 |
of its own, which has been specifically tailored for the needs of |
|
35 |
theory and proof development. Compared to raw ML, the Isabelle/Isar |
|
36 |
top-level provides a more robust and comfortable development |
|
29746 | 37 |
platform, with proper support for theory development graphs, managed |
38 |
transactions with unlimited undo etc. The Isabelle/Isar version of |
|
39 |
the \emph{Proof~General} user interface |
|
40 |
\cite{proofgeneral,Aspinall:TACAS:2000} provides a decent front-end |
|
41 |
for interactive theory and proof development in this advanced |
|
42 |
theorem proving environment, even though it is somewhat biased |
|
43 |
towards old-style proof scripts. |
|
27035 | 44 |
|
45 |
\medskip Apart from the technical advances over bare-bones ML |
|
46 |
programming, the main purpose of the Isar language is to provide a |
|
47 |
conceptually different view on machine-checked proofs |
|
29746 | 48 |
\cite{Wenzel:1999:TPHOL,Wenzel-PhD}. \emph{Isar} stands for |
49 |
\emph{Intelligible semi-automated reasoning}. Drawing from both the |
|
27035 | 50 |
traditions of informal mathematical proof texts and high-level |
51 |
programming languages, Isar offers a versatile environment for |
|
52 |
structured formal proof documents. Thus properly written Isar |
|
53 |
proofs become accessible to a broader audience than unstructured |
|
54 |
tactic scripts (which typically only provide operational information |
|
55 |
for the machine). Writing human-readable proof texts certainly |
|
56 |
requires some additional efforts by the writer to achieve a good |
|
57 |
presentation, both of formal and informal parts of the text. On the |
|
58 |
other hand, human-readable formal texts gain some value in their own |
|
59 |
right, independently of the mechanic proof-checking process. |
|
60 |
||
61 |
Despite its grand design of structured proof texts, Isar is able to |
|
62 |
assimilate the old tactical style as an ``improper'' sub-language. |
|
63 |
This provides an easy upgrade path for existing tactic scripts, as |
|
29746 | 64 |
well as some means for interactive experimentation and debugging of |
65 |
structured proofs. Isabelle/Isar supports a broad range of proof |
|
66 |
styles, both readable and unreadable ones. |
|
27035 | 67 |
|
29717 | 68 |
\medskip The generic Isabelle/Isar framework (see |
29746 | 69 |
\chref{ch:isar-framework}) works reasonably well for any Isabelle |
70 |
object-logic that conforms to the natural deduction view of the |
|
71 |
Isabelle/Pure framework. Specific language elements introduced by |
|
72 |
the major object-logics are described in \chref{ch:hol} |
|
27057 | 73 |
(Isabelle/HOL), \chref{ch:holcf} (Isabelle/HOLCF), and \chref{ch:zf} |
74 |
(Isabelle/ZF). The main language elements are already provided by |
|
75 |
the Isabelle/Pure framework. Nevertheless, examples given in the |
|
76 |
generic parts will usually refer to Isabelle/HOL as well. |
|
27042 | 77 |
|
78 |
\medskip Isar commands may be either \emph{proper} document |
|
79 |
constructors, or \emph{improper commands}. Some proof methods and |
|
80 |
attributes introduced later are classified as improper as well. |
|
40406 | 81 |
Improper Isar language elements, which are marked by ``\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}}'' in the subsequent chapters; they are often helpful |
27042 | 82 |
when developing proof documents, but their use is discouraged for |
83 |
the final human-readable outcome. Typical examples are diagnostic |
|
84 |
commands that print terms or theorems according to the current |
|
85 |
context; other commands emulate old-style tactical theorem proving.% |
|
27035 | 86 |
\end{isamarkuptext}% |
87 |
\isamarkuptrue% |
|
88 |
% |
|
89 |
\isadelimtheory |
|
90 |
% |
|
91 |
\endisadelimtheory |
|
92 |
% |
|
93 |
\isatagtheory |
|
94 |
\isacommand{end}\isamarkupfalse% |
|
95 |
% |
|
96 |
\endisatagtheory |
|
97 |
{\isafoldtheory}% |
|
98 |
% |
|
99 |
\isadelimtheory |
|
100 |
% |
|
101 |
\endisadelimtheory |
|
102 |
\isanewline |
|
103 |
\end{isabellebody}% |
|
104 |
%%% Local Variables: |
|
105 |
%%% mode: latex |
|
106 |
%%% TeX-master: "root" |
|
107 |
%%% End: |