|
wenzelm@7046
|
1 |
|
|
wenzelm@7297
|
2 |
\chapter{Basic Concepts}\label{ch:basics}
|
|
wenzelm@7046
|
3 |
|
|
wenzelm@7895
|
4 |
\section{Isabelle/Isar theories}
|
|
wenzelm@7895
|
5 |
|
|
wenzelm@7297
|
6 |
Isabelle/Isar offers two main improvements over classic Isabelle:
|
|
wenzelm@7297
|
7 |
\begin{enumerate}
|
|
wenzelm@7466
|
8 |
\item A new \emph{theory format}, occasionally referred to as ``new-style
|
|
wenzelm@7895
|
9 |
theories'', supporting interactive development and unlimited undo operation.
|
|
wenzelm@7895
|
10 |
\item A \emph{formal proof document language} designed to support intelligible
|
|
wenzelm@7895
|
11 |
semi-automated reasoning. Instead of putting together unreadable tactic
|
|
wenzelm@7895
|
12 |
scripts, the author is enabled to express the reasoning in way that is close
|
|
wenzelm@7895
|
13 |
to mathematical practice.
|
|
wenzelm@7297
|
14 |
\end{enumerate}
|
|
wenzelm@7297
|
15 |
|
|
wenzelm@7297
|
16 |
The Isar proof language is embedded into the new theory format as a proper
|
|
wenzelm@7297
|
17 |
sub-language. Proof mode is entered by stating some $\THEOREMNAME$ or
|
|
wenzelm@7895
|
18 |
$\LEMMANAME$ at the theory level, and left again with the final conclusion
|
|
wenzelm@7895
|
19 |
(e.g.\ via $\QEDNAME$). A few theory extension mechanisms require proof as
|
|
wenzelm@7466
|
20 |
well, such as the HOL $\isarkeyword{typedef}$ which demands non-emptiness of
|
|
wenzelm@7466
|
21 |
the representing sets.
|
|
wenzelm@7297
|
22 |
|
|
wenzelm@7297
|
23 |
New-style theory files may still be associated with an ML file consisting of
|
|
wenzelm@7315
|
24 |
plain old tactic scripts. There is no longer any ML binding generated for the
|
|
wenzelm@7466
|
25 |
theory and theorems, though. ML functions \texttt{theory}, \texttt{thm}, and
|
|
wenzelm@7466
|
26 |
\texttt{thms} retrieve this information \cite{isabelle-ref}. Nevertheless,
|
|
wenzelm@7466
|
27 |
migration between classic Isabelle and Isabelle/Isar is relatively easy. Thus
|
|
wenzelm@7466
|
28 |
users may start to benefit from interactive theory development even before
|
|
wenzelm@7466
|
29 |
they have any idea of the Isar proof language.
|
|
wenzelm@7315
|
30 |
|
|
wenzelm@7315
|
31 |
\begin{warn}
|
|
wenzelm@7466
|
32 |
Currently Proof~General does \emph{not} support mixed interactive
|
|
wenzelm@7895
|
33 |
development of classic Isabelle theory files and tactic scripts, together
|
|
wenzelm@7466
|
34 |
with Isar documents at the same time. The ``\texttt{isa}'' and
|
|
wenzelm@7466
|
35 |
``\texttt{isar}'' versions of Proof~General are handled as two different
|
|
wenzelm@7895
|
36 |
theorem proving systems, only one of these may be active.
|
|
wenzelm@7315
|
37 |
\end{warn}
|
|
wenzelm@7297
|
38 |
|
|
wenzelm@7466
|
39 |
Porting of existing tactic scripts is best done by running two separate
|
|
wenzelm@7466
|
40 |
Proof~General sessions, one for replaying the old script and the other for the
|
|
wenzelm@7466
|
41 |
emerging Isabelle/Isar document.
|
|
wenzelm@7466
|
42 |
|
|
wenzelm@7046
|
43 |
|
|
wenzelm@7046
|
44 |
\section{The Isar proof language}
|
|
wenzelm@7046
|
45 |
|
|
wenzelm@7466
|
46 |
Sorry, this important section has not been written yet! Refer to
|
|
wenzelm@7297
|
47 |
\cite{Wenzel:1999:TPHOL} for the time being.
|
|
wenzelm@7297
|
48 |
|
|
wenzelm@7297
|
49 |
\subsection{Commands}
|
|
wenzelm@7297
|
50 |
|
|
wenzelm@7297
|
51 |
\subsubsection{Isar primitives}
|
|
wenzelm@7297
|
52 |
|
|
wenzelm@7297
|
53 |
\subsubsection{Derived elements}
|
|
wenzelm@7297
|
54 |
|
|
wenzelm@7135
|
55 |
|
|
wenzelm@7135
|
56 |
\subsection{Methods}
|
|
wenzelm@7046
|
57 |
|
|
wenzelm@7046
|
58 |
\subsection{Attributes}
|
|
wenzelm@7046
|
59 |
|
|
wenzelm@7046
|
60 |
%%% Local Variables:
|
|
wenzelm@7046
|
61 |
%%% mode: latex
|
|
wenzelm@7046
|
62 |
%%% TeX-master: "isar-ref"
|
|
wenzelm@7046
|
63 |
%%% End:
|