1 |
1 |
2 \chapter{Basic Concepts}\label{ch:basics} |
2 \chapter{Basic Concepts}\label{ch:basics} |
|
3 |
|
4 \section{Isabelle/Isar theories} |
3 |
5 |
4 Isabelle/Isar offers two main improvements over classic Isabelle: |
6 Isabelle/Isar offers two main improvements over classic Isabelle: |
5 \begin{enumerate} |
7 \begin{enumerate} |
6 \item A new \emph{theory format}, occasionally referred to as ``new-style |
8 \item A new \emph{theory format}, occasionally referred to as ``new-style |
7 theories'', supporting interactive development with unlimited undo |
9 theories'', supporting interactive development and unlimited undo operation. |
8 operation. |
10 \item A \emph{formal proof document language} designed to support intelligible |
9 \item A \emph{formal proof language} designed to support intelligible |
11 semi-automated reasoning. Instead of putting together unreadable tactic |
10 semi-automated reasoning. Rather than putting together tactic scripts, the |
12 scripts, the author is enabled to express the reasoning in way that is close |
11 author is enabled to express the reasoning in way that is close to |
13 to mathematical practice. |
12 mathematical practice. |
|
13 \end{enumerate} |
14 \end{enumerate} |
14 |
15 |
15 The Isar proof language is embedded into the new theory format as a proper |
16 The Isar proof language is embedded into the new theory format as a proper |
16 sub-language. Proof mode is entered by stating some $\THEOREMNAME$ or |
17 sub-language. Proof mode is entered by stating some $\THEOREMNAME$ or |
17 $\LEMMANAME$ at the theory level, and left with the conclusion of the proof |
18 $\LEMMANAME$ at the theory level, and left again with the final conclusion |
18 (via $\QEDNAME$ etc.). Some theory extension mechanisms require proof as |
19 (e.g.\ via $\QEDNAME$). A few theory extension mechanisms require proof as |
19 well, such as the HOL $\isarkeyword{typedef}$ which demands non-emptiness of |
20 well, such as the HOL $\isarkeyword{typedef}$ which demands non-emptiness of |
20 the representing sets. |
21 the representing sets. |
21 |
22 |
22 New-style theory files may still be associated with an ML file consisting of |
23 New-style theory files may still be associated with an ML file consisting of |
23 plain old tactic scripts. There is no longer any ML binding generated for the |
24 plain old tactic scripts. There is no longer any ML binding generated for the |
27 users may start to benefit from interactive theory development even before |
28 users may start to benefit from interactive theory development even before |
28 they have any idea of the Isar proof language. |
29 they have any idea of the Isar proof language. |
29 |
30 |
30 \begin{warn} |
31 \begin{warn} |
31 Currently Proof~General does \emph{not} support mixed interactive |
32 Currently Proof~General does \emph{not} support mixed interactive |
32 development of classic Isabelle theory files and tactic scripts together |
33 development of classic Isabelle theory files and tactic scripts, together |
33 with Isar documents at the same time. The ``\texttt{isa}'' and |
34 with Isar documents at the same time. The ``\texttt{isa}'' and |
34 ``\texttt{isar}'' versions of Proof~General are handled as two different |
35 ``\texttt{isar}'' versions of Proof~General are handled as two different |
35 theorem proving systems, only one may be active at the same time. |
36 theorem proving systems, only one of these may be active. |
36 \end{warn} |
37 \end{warn} |
37 |
38 |
38 Porting of existing tactic scripts is best done by running two separate |
39 Porting of existing tactic scripts is best done by running two separate |
39 Proof~General sessions, one for replaying the old script and the other for the |
40 Proof~General sessions, one for replaying the old script and the other for the |
40 emerging Isabelle/Isar document. |
41 emerging Isabelle/Isar document. |