doc-src/IsarRef/isar-ref.tex
author wenzelm
Thu Oct 21 17:42:21 1999 +0200 (1999-10-21)
changeset 7895 7c492d8bc8e3
parent 7836 7a9270282fd3
child 7974 34245feb6e82
permissions -rw-r--r--
updated;
     1 
     2 %% $Id$
     3 
     4 \documentclass[12pt,a4paper,fleqn]{report}
     5 \usepackage{graphicx,../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 \newcommand{\drv}{\mathrel{\vdash}}
    24 \newcommand{\edrv}{\mathop{\drv}\nolimits}
    25 
    26 
    27 \setcounter{secnumdepth}{2} \setcounter{tocdepth}{2}
    28 
    29 \pagestyle{headings}
    30 \sloppy
    31 \binperiod     %%%treat . like a binary operator
    32 
    33 \renewcommand{\phi}{\varphi}
    34 
    35 %\includeonly{pure}
    36 
    37 
    38 
    39 \begin{document}
    40 
    41 \underscoreoff
    42 
    43 \maketitle 
    44 
    45 \begin{abstract}
    46   \emph{Intelligible semi-automated reasoning} (\emph{Isar}) is a generic
    47   approach to readable formal proof documents.  It sets out to bridge the
    48   semantic gap between any internal notions of proof based on primitive
    49   inferences and tactics, and an appropriate level of abstraction for
    50   user-level work.  The Isar formal proof language has been designed to
    51   satisfy quite contradictory requirements, being both ``declarative'' and
    52   immediately ``executable'', by virtue of the \emph{Isar/VM} interpreter.
    53   
    54   The current version of Isabelle offers Isar as an alternative proof language
    55   interface layer.  The Isabelle/Isar system provides an interpreter for the
    56   Isar formal proof document language.  The input may consist either of
    57   \emph{proper document constructors}, or \emph{improper auxiliary commands}
    58   (for diagnostics, exploration etc.).  Proof texts consisting of proper
    59   document constructors only, admit a purely static reading, thus being
    60   intelligible later without requiring dynamic replay that is so typical for
    61   traditional proof scripts.  Any of the Isabelle/Isar commands may be
    62   executed in single-steps, so basically the interpreter has a proof text
    63   debugger already built-in.
    64   
    65   Employing the Isar instantiation of \emph{Proof~General}, the generic Emacs
    66   interface for interactive proof assistants of LFCS Edinburgh, we arrive at a
    67   reasonable environment for \emph{live document editing}.  Thus proof texts
    68   may be developed incrementally by issuing proper document constructors,
    69   including forward and backward tracing of partial documents; intermediate
    70   states may be inspected by diagnostic commands.
    71   
    72   The Isar subsystem is tightly integrated into the Isabelle/Pure meta-logic
    73   implementation.  Theories, theorems, proof procedures etc.\ may be used
    74   interchangeably between classic Isabelle proof scripts and Isabelle/Isar
    75   documents.  Isar is as generic as Isabelle, able to support a wide range of
    76   object-logics.  Currently, the end-user working environment is most complete
    77   for Isabelle/HOL.
    78 \end{abstract}
    79 
    80 \pagenumbering{roman} \tableofcontents \clearfirst
    81 
    82 %FIXME
    83 \nocite{Rudnicki:1992:MizarOverview}
    84 \nocite{Harrison:1996:MizarHOL}
    85 \nocite{Rudnicki:1992:MizarOverview}
    86 \nocite{Trybulec:1993:MizarFeatures}
    87 \nocite{Syme:1997:DECLARE}
    88 \nocite{Syme:1998:thesis}
    89 \nocite{Syme:1999:TPHOL}
    90 
    91 \include{intro}
    92 \include{basics}
    93 \include{syntax}
    94 \include{pure}
    95 \include{generic}
    96 \include{hol}
    97 
    98 \appendix
    99 \include{refcard}
   100 
   101 \begingroup
   102   \bibliographystyle{plain} \small\raggedright\frenchspacing
   103   \bibliography{../manual}
   104 \endgroup
   105 
   106 \input{isar-ref.ind}
   107 
   108 \end{document}