51 satisfy quite contradictory requirements, being both ``declarative'' and |
51 satisfy quite contradictory requirements, being both ``declarative'' and |
52 immediately ``executable'', by virtue of the \emph{Isar/VM} interpreter. |
52 immediately ``executable'', by virtue of the \emph{Isar/VM} interpreter. |
53 |
53 |
54 The current version of Isabelle offers Isar as an alternative proof language |
54 The current version of Isabelle offers Isar as an alternative proof language |
55 interface layer. The Isabelle/Isar system provides an interpreter for the |
55 interface layer. The Isabelle/Isar system provides an interpreter for the |
56 Isar formal proof document language. The input may consist either of proper |
56 Isar formal proof language. The input may consist either of proper document |
57 document constructors, or improper auxiliary commands (for diagnostics, |
57 constructors, or improper auxiliary commands (for diagnostics, exploration |
58 exploration etc.). Proof texts consisting of proper document constructors |
58 etc.). Proof texts consisting of proper elements only, admit a purely |
59 only, admit a purely static reading, thus being intelligible later without |
59 static reading, thus being intelligible later without requiring dynamic |
60 requiring dynamic replay that is so typical for traditional proof scripts. |
60 replay that is so typical for traditional proof scripts. Any of the |
61 Any of the Isabelle/Isar commands may be executed in single-steps, so |
61 Isabelle/Isar commands may be executed in single-steps, so basically the |
62 basically the interpreter has a proof text debugger already built-in. |
62 interpreter has a proof text debugger already built-in. |
63 |
63 |
64 Employing the Isar instantiation of \emph{Proof~General}, a generic Emacs |
64 Employing the Isar instantiation of \emph{Proof~General}, a generic Emacs |
65 interface for interactive proof assistants, we arrive at a reasonable |
65 interface for interactive proof assistants, we arrive at a reasonable |
66 environment for \emph{live document editing}. Thus proof texts may be |
66 environment for \emph{live document editing}. Thus proof texts may be |
67 developed incrementally by issuing proper document constructors, including |
67 developed incrementally by issuing proof commands, including forward and |
68 forward and backward tracing of partial documents; intermediate states may |
68 backward tracing of partial documents; intermediate states may be inspected |
69 be inspected by diagnostic commands. |
69 by diagnostic commands. |
70 |
70 |
71 The Isar subsystem is tightly integrated into the Isabelle/Pure meta-logic |
71 The Isar subsystem is tightly integrated into the Isabelle/Pure meta-logic |
72 implementation. Theories, theorems, proof procedures etc.\ may be used |
72 implementation. Theories, theorems, proof procedures etc.\ may be used |
73 interchangeably between classic Isabelle proof scripts and Isabelle/Isar |
73 interchangeably between classic Isabelle proof scripts and Isabelle/Isar |
74 documents. Isar is as generic as Isabelle, able to support a wide range of |
74 documents. Isar is as generic as Isabelle, able to support a wide range of |