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