4 \documentclass[12pt,a4paper,fleqn]{report}
5 \usepackage{latexsym,graphicx,../iman,../extra,../proof,../rail,../railsetup,../isar,../pdfsetup}
7 \title{\includegraphics[scale=0.5]{isabelle_isar} \\[4ex] The Isabelle/Isar Reference Manual}
8 \author{\emph{Markus Wenzel} \\ TU M\"unchen}
12 \railterm{percent,ppercent,underscore,lbrace,rbrace,llbrace,rrbrace}
13 \railterm{ident,longident,symident,var,textvar,typefree,typevar,nat,string,verbatim,keyword}
15 \railalias{name}{\railqtoken{name}}
16 \railalias{nameref}{\railqtoken{nameref}}
17 \railalias{text}{\railqtoken{text}}
18 \railalias{type}{\railqtoken{type}}
19 \railalias{term}{\railqtoken{term}}
20 \railalias{prop}{\railqtoken{prop}}
21 \railalias{atom}{\railqtoken{atom}}
23 \newcommand{\drv}{\mathrel{\vdash}}
24 \newcommand{\edrv}{\mathop{\drv}\nolimits}
25 \newcommand{\Or}{\mathrel{\;|\;}}
28 \setcounter{secnumdepth}{2} \setcounter{tocdepth}{2}
32 \binperiod %%%treat . like a binary operator
34 \renewcommand{\phi}{\varphi}
36 %\includeonly{generic,refcard}
46 \emph{Intelligible semi-automated reasoning} (\emph{Isar}) is a generic
47 approach to readable formal proof documents. It sets out to bridge the
48 semantic gap between any internal notions of proof based on primitive
49 inferences and tactics, and an appropriate level of abstraction for
50 user-level work. The Isar formal proof language has been designed to
51 satisfy quite contradictory requirements, being both ``declarative'' and
52 immediately ``executable'', by virtue of the \emph{Isar/VM} interpreter.
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
56 Isar formal proof document language. The input may consist either of proper
57 document constructors, or improper auxiliary commands (for diagnostics,
58 exploration etc.). Proof texts consisting of proper document constructors
59 only, admit a purely static reading, thus being intelligible later without
60 requiring dynamic replay that is so typical for traditional proof scripts.
61 Any of the Isabelle/Isar commands may be executed in single-steps, so
62 basically the interpreter has a proof text debugger already built-in.
64 Employing the Isar instantiation of \emph{Proof~General}, a generic Emacs
65 interface for interactive proof assistants, we arrive at a reasonable
66 environment for \emph{live document editing}. Thus proof texts may be
67 developed incrementally by issuing proper document constructors, including
68 forward and backward tracing of partial documents; intermediate states may
69 be inspected by diagnostic commands.
71 The Isar subsystem is tightly integrated into the Isabelle/Pure meta-logic
72 implementation. Theories, theorems, proof procedures etc.\ may be used
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
75 object-logics. Currently, the end-user working environment is most complete
79 \pagenumbering{roman} \tableofcontents \clearfirst
83 % - Freek Widijk's stuff
86 \nocite{Rudnicki:1992:MizarOverview}
87 \nocite{Harrison:1996:MizarHOL}
88 \nocite{Rudnicki:1992:MizarOverview}
89 \nocite{Trybulec:1993:MizarFeatures}
90 \nocite{Syme:1997:DECLARE}
91 \nocite{Syme:1998:thesis}
92 \nocite{Syme:1999:TPHOL}
93 \nocite{Zammit:1999:TPHOL}
106 \bibliographystyle{plain} \small\raggedright\frenchspacing
107 \bibliography{../manual}