6 % - update Proof General and X-symbol installation notes;
7 % - update tactic emulation (including refcard);
8 % - proof script conversion guide;
11 \documentclass[12pt,a4paper,fleqn]{report}
12 \usepackage{latexsym,graphicx,../iman,../extra,../proof,../rail,../railsetup,../isar,../pdfsetup}
14 \title{\includegraphics[scale=0.5]{isabelle_isar} \\[4ex] The Isabelle/Isar Reference Manual}
15 \author{\emph{Markus Wenzel} \\ TU M\"unchen}
19 \newcommand{\isastyle}{\small\tt\slshape}
20 \newcommand{\isa}[1]{\emph{\isastyle #1}}
21 \newcommand{\isasymColon}{\emph{$\mathrel{::}$}}
22 \newcommand{\isasymRightarrow}{\emph{$\Rightarrow$}}
24 \railterm{percent,ppercent,underscore,lbrace,rbrace,atsign}
25 \railterm{ident,longident,symident,var,textvar,typefree,typevar,nat,string,verbatim,keyword}
26 \railterm{name,nameref,text,type,term,prop,atom}
28 \railalias{ident}{\railtoken{ident}}
29 \railalias{longident}{\railtoken{longident}}
30 \railalias{symident}{\railtoken{symident}}
31 \railalias{var}{\railtoken{var}}
32 \railalias{textvar}{\railtoken{textvar}}
33 \railalias{typefree}{\railtoken{typefree}}
34 \railalias{typevar}{\railtoken{typevar}}
35 \railalias{nat}{\railtoken{nat}}
36 \railalias{string}{\railtoken{string}}
37 \railalias{verbatim}{\railtoken{verbatim}}
38 \railalias{keyword}{\railtoken{keyword}}
40 \railalias{name}{\railqtoken{name}}
41 \railalias{nameref}{\railqtoken{nameref}}
42 \railalias{text}{\railqtoken{text}}
43 \railalias{type}{\railqtoken{type}}
44 \railalias{term}{\railqtoken{term}}
45 \railalias{prop}{\railqtoken{prop}}
46 \railalias{atom}{\railqtoken{atom}}
48 \newcommand{\drv}{\mathrel{\vdash}}
49 \newcommand{\edrv}{\mathop{\drv}\nolimits}
50 \newcommand{\Or}{\mathrel{\;|\;}}
53 \setcounter{secnumdepth}{2} \setcounter{tocdepth}{2}
57 \binperiod %%%treat . like a binary operator
59 \renewcommand{\phi}{\varphi}
61 %\includeonly{generic,refcard}
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.
79 The current version of Isabelle offers Isar as an alternative proof language
80 interface layer. The Isabelle/Isar system provides an interpreter for the
81 Isar formal proof language. The input may consist either of proper document
82 constructors, or improper auxiliary commands (for diagnostics, exploration
83 etc.). Proof texts consisting of proper elements only, admit a purely
84 static reading, thus being intelligible later without requiring dynamic
85 replay that is so typical for traditional proof scripts. Any of the
86 Isabelle/Isar commands may be executed in single-steps, so basically the
87 interpreter has a proof text debugger already built-in.
89 Employing the Isar instantiation of \emph{Proof~General}, a generic Emacs
90 interface for interactive proof assistants, we arrive at a reasonable
91 environment for \emph{live document editing}. Thus proof texts may be
92 developed incrementally by issuing proof commands, including forward and
93 backward tracing of partial documents; intermediate states may be inspected
94 by diagnostic commands.
96 The Isar subsystem is tightly integrated into the Isabelle/Pure meta-logic
97 implementation. Theories, theorems, proof procedures etc.\ may be used
98 interchangeably between classic Isabelle proof scripts and Isabelle/Isar
99 documents. Isar is as generic as Isabelle, able to support a wide range of
100 object-logics. Currently, the end-user working environment is most complete
104 \pagenumbering{roman} \tableofcontents \clearfirst
107 \nocite{Aspinall:2000:eProof}
108 \nocite{Bauer-Wenzel:2000:HB}
109 \nocite{Harrison:1996:MizarHOL}
110 \nocite{Muzalewski:Mizar}
111 \nocite{Rudnicki:1992:MizarOverview}
112 \nocite{Rudnicki:1992:MizarOverview}
113 \nocite{Syme:1997:DECLARE}
114 \nocite{Syme:1998:thesis}
115 \nocite{Syme:1999:TPHOL}
116 \nocite{Trybulec:1993:MizarFeatures}
117 \nocite{Wiedijk:1999:Mizar}
118 \nocite{Wiedijk:2000:MV}
119 \nocite{Zammit:1999:TPHOL}
133 \bibliographystyle{plain} \small\raggedright\frenchspacing
134 \bibliography{../manual}