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