7046

1 


2 
%% $Id$


3 

7134

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

7509

5 
\usepackage{graphicx,a4,../url,../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

7335

54 
only, admit a purely static reading, thus being intelligible later without

7167

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 

7297

59 
Employing the Isar instantiation of \emph{Proof~General}, the generic Emacs

7167

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 

7335

66 
The Isar subsystem is tightly integrated into the Isabelle/Pure metalogic


67 
implementation. Theories, theorems, proof procedures etc.\ may be used


68 
interchangeably between Isabelleclassic proof scripts and Isabelle/Isar


69 
documents. Isar is as generic as Isabelle, able to support a wide range of

7466

70 
objectlogics. The current working environment for endusers is setup


71 
mainly for 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 


85 
\include{intro}


86 
\include{basics}


87 
\include{syntax}


88 
\include{pure}

7135

89 
\include{generic}

7046

90 
\include{hol}


91 


92 
\begingroup


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


94 
\bibliography{../manual}


95 
\endgroup


96 


97 
\input{isarref.ind}


98 


99 
\end{document}
