wenzelm@7046: 
wenzelm@7046: %% $Id$
wenzelm@7046: 
wenzelm@7836: \documentclass[12pt,a4paper,fleqn]{report}
wenzelm@9695: \usepackage{latexsym,graphicx,../iman,../extra,../ttbox,../proof,../rail,../railsetup,../isar,../pdfsetup}
wenzelm@7046: 
wenzelm@7046: \title{\includegraphics[scale=0.5]{isabelle_isar} \\[4ex] The Isabelle/Isar Reference Manual}
wenzelm@7050: \author{\emph{Markus Wenzel} \\ TU M\"unchen}
wenzelm@7046: 
wenzelm@7050: \makeindex
wenzelm@7050: 
wenzelm@9658: \newcommand{\isastyle}{\small\tt\slshape}
wenzelm@9658: \newcommand{\isa}[1]{\emph{\isastyle #1}}
wenzelm@10208: \newcommand{\isamath}[1]{\emph{$#1$}}
wenzelm@10208: \newcommand{\isasymColon}{\isamath{\mathrel{::}}}
wenzelm@10208: \newcommand{\isasymRightarrow}{\isamath{\Rightarrow}}
wenzelm@9204: 
wenzelm@9204: \railterm{percent,ppercent,underscore,lbrace,rbrace,atsign}
wenzelm@7167: \railterm{ident,longident,symident,var,textvar,typefree,typevar,nat,string,verbatim,keyword}
wenzelm@8596: \railterm{name,nameref,text,type,term,prop,atom}
wenzelm@7134: 
wenzelm@8594: \railalias{ident}{\railtoken{ident}}
wenzelm@8594: \railalias{longident}{\railtoken{longident}}
wenzelm@8594: \railalias{symident}{\railtoken{symident}}
wenzelm@8594: \railalias{var}{\railtoken{var}}
wenzelm@8594: \railalias{textvar}{\railtoken{textvar}}
wenzelm@8594: \railalias{typefree}{\railtoken{typefree}}
wenzelm@8594: \railalias{typevar}{\railtoken{typevar}}
wenzelm@8594: \railalias{nat}{\railtoken{nat}}
wenzelm@8594: \railalias{string}{\railtoken{string}}
wenzelm@8594: \railalias{verbatim}{\railtoken{verbatim}}
wenzelm@8594: \railalias{keyword}{\railtoken{keyword}}
wenzelm@8594: 
wenzelm@7134: \railalias{name}{\railqtoken{name}}
wenzelm@7134: \railalias{nameref}{\railqtoken{nameref}}
wenzelm@7134: \railalias{text}{\railqtoken{text}}
wenzelm@7134: \railalias{type}{\railqtoken{type}}
wenzelm@7134: \railalias{term}{\railqtoken{term}}
wenzelm@7134: \railalias{prop}{\railqtoken{prop}}
wenzelm@7134: \railalias{atom}{\railqtoken{atom}}
wenzelm@7134: 
wenzelm@7895: \newcommand{\drv}{\mathrel{\vdash}}
wenzelm@7895: \newcommand{\edrv}{\mathop{\drv}\nolimits}
wenzelm@7974: \newcommand{\Or}{\mathrel{\;|\;}}
wenzelm@7895: 
wenzelm@7046: 
wenzelm@7046: \setcounter{secnumdepth}{2} \setcounter{tocdepth}{2}
wenzelm@7046: 
wenzelm@7046: \pagestyle{headings}
wenzelm@7046: \sloppy
wenzelm@7046: \binperiod     %%%treat . like a binary operator
wenzelm@7046: 
wenzelm@7134: \renewcommand{\phi}{\varphi}
wenzelm@7046: 
wenzelm@8514: %\includeonly{generic,refcard}
wenzelm@7895: 
wenzelm@7046: 
wenzelm@7046: \begin{document}
wenzelm@7046: 
wenzelm@7046: \underscoreoff
wenzelm@7046: 
wenzelm@7046: \maketitle 
wenzelm@7046: 
wenzelm@7046: \begin{abstract}
wenzelm@7167:   \emph{Intelligible semi-automated reasoning} (\emph{Isar}) is a generic
wenzelm@7167:   approach to readable formal proof documents.  It sets out to bridge the
wenzelm@7167:   semantic gap between any internal notions of proof based on primitive
wenzelm@7167:   inferences and tactics, and an appropriate level of abstraction for
wenzelm@7167:   user-level work.  The Isar formal proof language has been designed to
wenzelm@7167:   satisfy quite contradictory requirements, being both ``declarative'' and
wenzelm@7167:   immediately ``executable'', by virtue of the \emph{Isar/VM} interpreter.
wenzelm@7167:   
wenzelm@10160:   The Isabelle/Isar system provides an interpreter for the Isar formal proof
wenzelm@10160:   language.  The input may consist either of proper document constructors, or
wenzelm@10160:   improper auxiliary commands (for diagnostics, exploration etc.).  Proof
wenzelm@10160:   texts consisting of proper elements only admit a purely static reading, thus
wenzelm@10160:   being intelligible later without requiring dynamic replay that is so typical
wenzelm@10160:   for traditional proof scripts.  Any of the Isabelle/Isar commands may be
wenzelm@10160:   executed in single-steps, so basically the interpreter has a proof text
wenzelm@10160:   debugger already built-in.
wenzelm@7167:   
wenzelm@8509:   Employing the Isar instantiation of \emph{Proof~General}, a generic Emacs
wenzelm@8509:   interface for interactive proof assistants, we arrive at a reasonable
wenzelm@8509:   environment for \emph{live document editing}.  Thus proof texts may be
wenzelm@8547:   developed incrementally by issuing proof commands, including forward and
wenzelm@8547:   backward tracing of partial documents; intermediate states may be inspected
wenzelm@8547:   by diagnostic commands.
wenzelm@7167:   
wenzelm@7335:   The Isar subsystem is tightly integrated into the Isabelle/Pure meta-logic
wenzelm@7335:   implementation.  Theories, theorems, proof procedures etc.\ may be used
wenzelm@7895:   interchangeably between classic Isabelle proof scripts and Isabelle/Isar
wenzelm@10160:   documents.  Even more, Isar provides a set of emulation commands and methods
wenzelm@10160:   for simulating traditional tactic scripts within new-style theory documents.
wenzelm@10160:   
wenzelm@10160:   The Isar framework is as generic as Isabelle, able to support a wide range
wenzelm@10160:   of object-logics.  Currently, the end-user working environment is most
wenzelm@10160:   complete for Isabelle/HOL.
wenzelm@7046: \end{abstract}
wenzelm@7046: 
wenzelm@7046: \pagenumbering{roman} \tableofcontents \clearfirst
wenzelm@7046: 
wenzelm@7046: %FIXME
wenzelm@9600: \nocite{Aspinall:2000:eProof}
wenzelm@9600: \nocite{Bauer-Wenzel:2000:HB}
wenzelm@9600: \nocite{Harrison:1996:MizarHOL}
wenzelm@9600: \nocite{Muzalewski:Mizar}
wenzelm@7046: \nocite{Rudnicki:1992:MizarOverview}
wenzelm@7046: \nocite{Rudnicki:1992:MizarOverview}
wenzelm@7046: \nocite{Syme:1997:DECLARE}
wenzelm@7046: \nocite{Syme:1998:thesis}
wenzelm@7046: \nocite{Syme:1999:TPHOL}
wenzelm@9600: \nocite{Trybulec:1993:MizarFeatures}
wenzelm@9600: \nocite{Wiedijk:1999:Mizar}
wenzelm@9600: \nocite{Wiedijk:2000:MV}
wenzelm@7988: \nocite{Zammit:1999:TPHOL}
wenzelm@7046: 
wenzelm@7046: \include{intro}
wenzelm@7046: \include{basics}
wenzelm@7046: \include{syntax}
wenzelm@7046: \include{pure}
wenzelm@7135: \include{generic}
wenzelm@7046: \include{hol}
wenzelm@7046: 
wenzelm@7895: \appendix
wenzelm@7895: \include{refcard}
wenzelm@9600: \include{conversion}
wenzelm@7895: 
wenzelm@7046: \begingroup
wenzelm@7046:   \bibliographystyle{plain} \small\raggedright\frenchspacing
wenzelm@7046:   \bibliography{../manual}
wenzelm@7046: \endgroup
wenzelm@7046: 
wenzelm@8828: \printindex
wenzelm@7046: 
wenzelm@7046: \end{document}