doc-src/IsarRef/isar-ref.tex
author wenzelm
Sat Oct 30 20:13:16 1999 +0200 (1999-10-30)
changeset 7981 5120a2a15d06
parent 7974 34245feb6e82
child 7988 feea893b47c7
permissions -rw-r--r--
tuned;
     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 proper
    58   document constructors, or improper auxiliary commands (for diagnostics,
    59   exploration etc.).  Proof texts consisting of proper document constructors
    60   only, admit a purely static reading, thus being intelligible later without
    61   requiring dynamic replay that is so typical for traditional proof scripts.
    62   Any of the Isabelle/Isar commands may be executed in single-steps, so
    63   basically the interpreter has a proof text 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}