65 |
65 |
66 \underscoreoff |
66 \underscoreoff |
67 |
67 |
68 \maketitle |
68 \maketitle |
69 |
69 |
70 \begin{abstract} |
|
71 \emph{Intelligible semi-automated reasoning} (\emph{Isar}) is a generic |
|
72 approach to readable formal proof documents. It sets out to bridge the |
|
73 semantic gap between any internal notions of proof based on primitive |
|
74 inferences and tactics, and an appropriate level of abstraction for |
|
75 user-level work. The Isar formal proof language has been designed to |
|
76 satisfy quite contradictory requirements, being both ``declarative'' and |
|
77 immediately ``executable'', by virtue of the \emph{Isar/VM} interpreter. |
|
78 |
|
79 The Isabelle/Isar system provides an interpreter for the Isar formal proof |
|
80 language. The input may consist either of proper document constructors, or |
|
81 improper auxiliary commands (for diagnostics, exploration etc.). Proof |
|
82 texts consisting of proper elements only admit a purely static reading, thus |
|
83 being intelligible later without requiring dynamic replay that is so typical |
|
84 for traditional proof scripts. Any of the Isabelle/Isar commands may be |
|
85 executed in single-steps, so basically the interpreter has a proof text |
|
86 debugger already built-in. |
|
87 |
|
88 Employing the Isar instantiation of \emph{Proof~General}, a generic Emacs |
|
89 interface for interactive proof assistants, we arrive at a reasonable |
|
90 environment for \emph{live document editing}. Thus proof texts may be |
|
91 developed incrementally by issuing proof commands, including forward and |
|
92 backward tracing of partial documents; intermediate states may be inspected |
|
93 by diagnostic commands. |
|
94 |
|
95 The Isar subsystem is tightly integrated into the Isabelle/Pure meta-logic |
|
96 implementation. Theories, theorems, proof procedures etc.\ may be used |
|
97 interchangeably between classic Isabelle proof scripts and Isabelle/Isar |
|
98 documents. Even more, Isar provides a set of emulation commands and methods |
|
99 for simulating traditional tactic scripts within new-style theory documents. |
|
100 |
|
101 The Isar framework is as generic as Isabelle, able to support a wide range |
|
102 of object-logics. Currently, the end-user working environment is most |
|
103 complete for Isabelle/HOL. |
|
104 \end{abstract} |
|
105 |
|
106 \pagenumbering{roman} \tableofcontents \clearfirst |
70 \pagenumbering{roman} \tableofcontents \clearfirst |
107 |
71 |
108 %FIXME |
72 %FIXME |
109 \nocite{Aspinall:2000:eProof} |
73 \nocite{Aspinall:2000:eProof} |
110 \nocite{Bauer-Wenzel:2000:HB} |
74 \nocite{Bauer-Wenzel:2000:HB} |