doc-src/IsarRef/isar-ref.tex
author wenzelm
Tue Aug 03 18:56:51 1999 +0200 (1999-08-03)
changeset 7167 0b2e3ef1d8f4
parent 7135 8eabfd7e6b9b
child 7297 c1eeeadbe80a
permissions -rw-r--r--
tuned;
much more material;
     1 
     2 %% $Id$
     3 
     4 \documentclass[12pt,fleqn]{report}
     5 \usepackage{graphicx,a4,../iman,../extra,../proof,../rail,../railsetup,../isar,../pdfsetup}
     6 
     7 \title{\includegraphics[scale=0.5]{isabelle_isar} \\[4ex] The Isabelle/Isar Reference Manual}
     8 \author{\emph{Markus Wenzel} \\ TU M\"unchen}
     9 
    10 \makeindex
    11 
    12 \railterm{percent,ppercent,underscore,lbrace,rbrace,llbrace,rrbrace}
    13 \railterm{ident,longident,symident,var,textvar,typefree,typevar,nat,string,verbatim,keyword}
    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 
    23 
    24 \setcounter{secnumdepth}{2} \setcounter{tocdepth}{2}
    25 
    26 \pagestyle{headings}
    27 \sloppy
    28 \binperiod     %%%treat . like a binary operator
    29 
    30 \renewcommand{\phi}{\varphi}
    31 
    32 
    33 \begin{document}
    34 
    35 \underscoreoff
    36 
    37 \maketitle 
    38 
    39 \begin{abstract}
    40   \emph{Intelligible semi-automated 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   user-level 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 single-steps, so
    57   basically the interpreter has a proof text debugger already built-in.
    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   meta-logic implementation.  Theories, theorems, proof procedures etc.\ may
    68   be used interchangeably between Isabelle-classic proof scripts and
    69   Isabelle/Isar documents.  Isar is as generic as Isabelle, able to support a
    70   wide range of object-logics.  The current end-user setup is mainly for
    71   Isabelle/HOL.
    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}
    90 \include{generic}
    91 \include{hol}
    92 
    93 \begingroup
    94   \bibliographystyle{plain} \small\raggedright\frenchspacing
    95   \bibliography{../manual}
    96 \endgroup
    97 
    98 \input{isar-ref.ind}
    99 
   100 \end{document}