1 |
1 |
2 %% $Id$ |
2 %% $Id$ |
3 |
|
4 % FIXME TODO |
|
5 % |
|
6 % - update Proof General and X-symbol installation notes; |
|
7 % - update tactic emulation (including refcard); |
|
8 % - proof script conversion guide; |
|
9 |
|
10 |
3 |
11 \documentclass[12pt,a4paper,fleqn]{report} |
4 \documentclass[12pt,a4paper,fleqn]{report} |
12 \usepackage{latexsym,graphicx,../iman,../extra,../ttbox,../proof,../rail,../railsetup,../isar,../pdfsetup} |
5 \usepackage{latexsym,graphicx,../iman,../extra,../ttbox,../proof,../rail,../railsetup,../isar,../pdfsetup} |
13 |
6 |
14 \title{\includegraphics[scale=0.5]{isabelle_isar} \\[4ex] The Isabelle/Isar Reference Manual} |
7 \title{\includegraphics[scale=0.5]{isabelle_isar} \\[4ex] The Isabelle/Isar Reference Manual} |
74 inferences and tactics, and an appropriate level of abstraction for |
67 inferences and tactics, and an appropriate level of abstraction for |
75 user-level work. The Isar formal proof language has been designed to |
68 user-level work. The Isar formal proof language has been designed to |
76 satisfy quite contradictory requirements, being both ``declarative'' and |
69 satisfy quite contradictory requirements, being both ``declarative'' and |
77 immediately ``executable'', by virtue of the \emph{Isar/VM} interpreter. |
70 immediately ``executable'', by virtue of the \emph{Isar/VM} interpreter. |
78 |
71 |
79 The current version of Isabelle offers Isar as an alternative proof language |
72 The Isabelle/Isar system provides an interpreter for the Isar formal proof |
80 interface layer. The Isabelle/Isar system provides an interpreter for the |
73 language. The input may consist either of proper document constructors, or |
81 Isar formal proof language. The input may consist either of proper document |
74 improper auxiliary commands (for diagnostics, exploration etc.). Proof |
82 constructors, or improper auxiliary commands (for diagnostics, exploration |
75 texts consisting of proper elements only admit a purely static reading, thus |
83 etc.). Proof texts consisting of proper elements only, admit a purely |
76 being intelligible later without requiring dynamic replay that is so typical |
84 static reading, thus being intelligible later without requiring dynamic |
77 for traditional proof scripts. Any of the Isabelle/Isar commands may be |
85 replay that is so typical for traditional proof scripts. Any of the |
78 executed in single-steps, so basically the interpreter has a proof text |
86 Isabelle/Isar commands may be executed in single-steps, so basically the |
79 debugger already built-in. |
87 interpreter has a proof text debugger already built-in. |
|
88 |
80 |
89 Employing the Isar instantiation of \emph{Proof~General}, a generic Emacs |
81 Employing the Isar instantiation of \emph{Proof~General}, a generic Emacs |
90 interface for interactive proof assistants, we arrive at a reasonable |
82 interface for interactive proof assistants, we arrive at a reasonable |
91 environment for \emph{live document editing}. Thus proof texts may be |
83 environment for \emph{live document editing}. Thus proof texts may be |
92 developed incrementally by issuing proof commands, including forward and |
84 developed incrementally by issuing proof commands, including forward and |
94 by diagnostic commands. |
86 by diagnostic commands. |
95 |
87 |
96 The Isar subsystem is tightly integrated into the Isabelle/Pure meta-logic |
88 The Isar subsystem is tightly integrated into the Isabelle/Pure meta-logic |
97 implementation. Theories, theorems, proof procedures etc.\ may be used |
89 implementation. Theories, theorems, proof procedures etc.\ may be used |
98 interchangeably between classic Isabelle proof scripts and Isabelle/Isar |
90 interchangeably between classic Isabelle proof scripts and Isabelle/Isar |
99 documents. Isar is as generic as Isabelle, able to support a wide range of |
91 documents. Even more, Isar provides a set of emulation commands and methods |
100 object-logics. Currently, the end-user working environment is most complete |
92 for simulating traditional tactic scripts within new-style theory documents. |
101 for Isabelle/HOL. |
93 |
|
94 The Isar framework is as generic as Isabelle, able to support a wide range |
|
95 of object-logics. Currently, the end-user working environment is most |
|
96 complete for Isabelle/HOL. |
102 \end{abstract} |
97 \end{abstract} |
103 |
98 |
104 \pagenumbering{roman} \tableofcontents \clearfirst |
99 \pagenumbering{roman} \tableofcontents \clearfirst |
105 |
100 |
106 %FIXME |
101 %FIXME |