7 \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} |
8 \author{\emph{Markus Wenzel} \\ TU M\"unchen} |
8 \author{\emph{Markus Wenzel} \\ TU M\"unchen} |
9 |
9 |
10 \makeindex |
10 \makeindex |
11 |
11 |
12 \railterm{lbrace,rbrace,llbrace,rrbrace} |
12 \railterm{percent,ppercent,underscore,lbrace,rbrace,llbrace,rrbrace} |
13 \railterm{ident,longident,symident,var,textvar,typefree,typevar,nat,string,verbatim} |
13 \railterm{ident,longident,symident,var,textvar,typefree,typevar,nat,string,verbatim,keyword} |
14 |
14 |
15 \railalias{name}{\railqtoken{name}} |
15 \railalias{name}{\railqtoken{name}} |
16 \railalias{nameref}{\railqtoken{nameref}} |
16 \railalias{nameref}{\railqtoken{nameref}} |
17 \railalias{text}{\railqtoken{text}} |
17 \railalias{text}{\railqtoken{text}} |
18 \railalias{type}{\railqtoken{type}} |
18 \railalias{type}{\railqtoken{type}} |
35 \underscoreoff |
35 \underscoreoff |
36 |
36 |
37 \maketitle |
37 \maketitle |
38 |
38 |
39 \begin{abstract} |
39 \begin{abstract} |
40 FIXME |
40 \emph{Intelligible semi-automated reasoning} (\emph{Isar}) is a generic |
|
41 approach to readable formal proof documents. It sets out to bridge the |
|
42 semantic gap between any internal notions of proof based on primitive |
|
43 inferences and tactics, and an appropriate level of abstraction for |
|
44 user-level work. The Isar formal proof language has been designed to |
|
45 satisfy quite contradictory requirements, being both ``declarative'' and |
|
46 immediately ``executable'', by virtue of the \emph{Isar/VM} interpreter. |
|
47 |
|
48 The current version of Isabelle offers Isar as an alternative proof language |
|
49 interface layer, beyond traditional tactic scripts. The Isabelle/Isar |
|
50 system provides an interpreter for the Isar formal proof document language. |
|
51 Isabelle/Isar input may consist either of \emph{proper document |
|
52 constructors}, or \emph{improper auxiliary commands} (for diagnostics, |
|
53 exploration etc.). Proof texts consisting of proper document constructors |
|
54 only admit a purely static reading, thus being intelligible later without |
|
55 requiring dynamic replay that is so typical for traditional proof scripts. |
|
56 Any of the Isabelle/Isar commands may be executed in single-steps, so |
|
57 basically the interpreter has a proof text debugger already built-in. |
|
58 |
|
59 Employing the \emph{ProofGeneral/isar} instantiation of the generic Emacs |
|
60 interface for interactive proof assistants of LFCS Edinburgh, we arrive at a |
|
61 reasonable environment for \emph{live document editing}. Thus proof texts |
|
62 may be developed incrementally by issuing proper document constructors, |
|
63 including forward and backward tracing of partial documents; intermediate |
|
64 states may be inspected by diagnostic commands. |
|
65 |
|
66 The Isar subsystem of Isabelle is tightly integrated into the Isabelle/Pure |
|
67 meta-logic implementation. Theories, theorems, proof procedures etc.\ may |
|
68 be used interchangeably between Isabelle-classic proof scripts and |
|
69 Isabelle/Isar documents. Isar is as generic as Isabelle, able to support a |
|
70 wide range of object-logics. The current end-user setup is mainly for |
|
71 Isabelle/HOL. |
41 \end{abstract} |
72 \end{abstract} |
42 |
73 |
43 \pagenumbering{roman} \tableofcontents \clearfirst |
74 \pagenumbering{roman} \tableofcontents \clearfirst |
44 |
75 |
45 %FIXME |
76 %FIXME |