7046

1 


2 
%% $Id$


3 

7134

4 
\documentclass[12pt,fleqn]{report}


5 
\usepackage{graphicx,a4,../iman,../extra,../proof,../rail,../railsetup,../isar,../pdfsetup}

7046

6 


7 
\title{\includegraphics[scale=0.5]{isabelle_isar} \\[4ex] The Isabelle/Isar Reference Manual}

7050

8 
\author{\emph{Markus Wenzel} \\ TU M\"unchen}

7046

9 

7050

10 
\makeindex


11 

7167

12 
\railterm{percent,ppercent,underscore,lbrace,rbrace,llbrace,rrbrace}


13 
\railterm{ident,longident,symident,var,textvar,typefree,typevar,nat,string,verbatim,keyword}

7134

14 


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}}


22 

7046

23 


24 
\setcounter{secnumdepth}{2} \setcounter{tocdepth}{2}


25 


26 
\pagestyle{headings}


27 
\sloppy


28 
\binperiod %%%treat . like a binary operator


29 

7134

30 
\renewcommand{\phi}{\varphi}

7046

31 


32 


33 
\begin{document}


34 


35 
\underscoreoff


36 


37 
\maketitle


38 


39 
\begin{abstract}

7167

40 
\emph{Intelligible semiautomated 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 
userlevel 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 singlesteps, so


57 
basically the interpreter has a proof text debugger already builtin.


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 
metalogic implementation. Theories, theorems, proof procedures etc.\ may


68 
be used interchangeably between Isabelleclassic proof scripts and


69 
Isabelle/Isar documents. Isar is as generic as Isabelle, able to support a


70 
wide range of objectlogics. The current enduser setup is mainly for


71 
Isabelle/HOL.

7046

72 
\end{abstract}


73 


74 
\pagenumbering{roman} \tableofcontents \clearfirst


75 


76 
%FIXME


77 
\nocite{Rudnicki:1992:MizarOverview}


78 
\nocite{Harrison:1996:MizarHOL}


79 
\nocite{Rudnicki:1992:MizarOverview}


80 
\nocite{Trybulec:1993:MizarFeatures}


81 
\nocite{Syme:1997:DECLARE}


82 
\nocite{Syme:1998:thesis}


83 
\nocite{Syme:1999:TPHOL}


84 
\nocite{Wenzel:1999:TPHOL}


85 


86 
\include{intro}


87 
\include{basics}


88 
\include{syntax}


89 
\include{pure}

7135

90 
\include{generic}

7046

91 
\include{hol}


92 


93 
\begingroup


94 
\bibliographystyle{plain} \small\raggedright\frenchspacing


95 
\bibliography{../manual}


96 
\endgroup


97 


98 
\input{isarref.ind}


99 


100 
\end{document}
