4 \documentclass[12pt,a4paper,fleqn]{report}
5 \usepackage{latexsym,graphicx,../iman,../extra,../ttbox,../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 \newcommand{\isastyle}{\small\tt\slshape}
13 \newcommand{\isa}[1]{\emph{\isastyle #1}}
14 \newcommand{\isamath}[1]{\emph{$#1$}}
15 \newcommand{\isasymColon}{\isamath{\mathrel{::}}}
16 \newcommand{\isasymRightarrow}{\isamath{\Rightarrow}}
17 \newcommand{\isasymleftharpoondown}{\isamath{\leftharpoondown}}
18 \newcommand{\isasymrightharpoonup}{\isamath{\rightharpoonup}}
19 \newcommand{\isasymrightleftharpoons}{\isamath{\rightleftharpoons}}
21 \railterm{percent,ppercent,underscore,lbrace,rbrace,atsign}
22 \railterm{ident,longident,symident,var,textvar,typefree,typevar,nat,string,verbatim,keyword}
23 \railterm{name,nameref,text,type,term,prop,atom}
25 \railalias{ident}{\railtoken{ident}}
26 \railalias{longident}{\railtoken{longident}}
27 \railalias{symident}{\railtoken{symident}}
28 \railalias{var}{\railtoken{var}}
29 \railalias{textvar}{\railtoken{textvar}}
30 \railalias{typefree}{\railtoken{typefree}}
31 \railalias{typevar}{\railtoken{typevar}}
32 \railalias{nat}{\railtoken{nat}}
33 \railalias{string}{\railtoken{string}}
34 \railalias{verbatim}{\railtoken{verbatim}}
35 \railalias{keyword}{\railtoken{keyword}}
37 \railalias{name}{\railqtoken{name}}
38 \railalias{nameref}{\railqtoken{nameref}}
39 \railalias{text}{\railqtoken{text}}
40 \railalias{type}{\railqtoken{type}}
41 \railalias{term}{\railqtoken{term}}
42 \railalias{prop}{\railqtoken{prop}}
43 \railalias{atom}{\railqtoken{atom}}
45 \newcommand{\drv}{\mathrel{\vdash}}
46 \newcommand{\edrv}{\mathop{\drv}\nolimits}
47 \newcommand{\Or}{\mathrel{\;|\;}}
50 \setcounter{secnumdepth}{2} \setcounter{tocdepth}{2}
54 \binperiod %%%treat . like a binary operator
56 \renewcommand{\phi}{\varphi}
68 \emph{Intelligible semi-automated reasoning} (\emph{Isar}) is a generic
69 approach to readable formal proof documents. It sets out to bridge the
70 semantic gap between any internal notions of proof based on primitive
71 inferences and tactics, and an appropriate level of abstraction for
72 user-level work. The Isar formal proof language has been designed to
73 satisfy quite contradictory requirements, being both ``declarative'' and
74 immediately ``executable'', by virtue of the \emph{Isar/VM} interpreter.
76 The Isabelle/Isar system provides an interpreter for the Isar formal proof
77 language. The input may consist either of proper document constructors, or
78 improper auxiliary commands (for diagnostics, exploration etc.). Proof
79 texts consisting of proper elements only admit a purely static reading, thus
80 being intelligible later without requiring dynamic replay that is so typical
81 for traditional proof scripts. Any of the Isabelle/Isar commands may be
82 executed in single-steps, so basically the interpreter has a proof text
83 debugger already built-in.
85 Employing the Isar instantiation of \emph{Proof~General}, a generic Emacs
86 interface for interactive proof assistants, we arrive at a reasonable
87 environment for \emph{live document editing}. Thus proof texts may be
88 developed incrementally by issuing proof commands, including forward and
89 backward tracing of partial documents; intermediate states may be inspected
90 by diagnostic commands.
92 The Isar subsystem is tightly integrated into the Isabelle/Pure meta-logic
93 implementation. Theories, theorems, proof procedures etc.\ may be used
94 interchangeably between classic Isabelle proof scripts and Isabelle/Isar
95 documents. Even more, Isar provides a set of emulation commands and methods
96 for simulating traditional tactic scripts within new-style theory documents.
98 The Isar framework is as generic as Isabelle, able to support a wide range
99 of object-logics. Currently, the end-user working environment is most
100 complete for Isabelle/HOL.
103 \pagenumbering{roman} \tableofcontents \clearfirst
106 \nocite{Aspinall:2000:eProof}
107 \nocite{Bauer-Wenzel:2000:HB}
108 \nocite{Harrison:1996:MizarHOL}
109 \nocite{Muzalewski:Mizar}
110 \nocite{Rudnicki:1992:MizarOverview}
111 \nocite{Rudnicki:1992:MizarOverview}
112 \nocite{Syme:1997:DECLARE}
113 \nocite{Syme:1998:thesis}
114 \nocite{Syme:1999:TPHOL}
115 \nocite{Trybulec:1993:MizarFeatures}
116 \nocite{Wiedijk:1999:Mizar}
117 \nocite{Wiedijk:2000:MV}
118 \nocite{Zammit:1999:TPHOL}
132 \bibliographystyle{plain} \small\raggedright\frenchspacing
133 \bibliography{../manual}