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