doc-src/IsarRef/isar-ref.tex
author wenzelm
Mon Aug 28 13:52:38 2000 +0200 (2000-08-28)
changeset 9695 ec7d7f877712
parent 9658 97d6d0a72d35
child 10160 bb8f9412fec6
permissions -rw-r--r--
proper setup of iman.sty/extra.sty/ttbox.sty;
     1 
     2 %% $Id$
     3 
     4 % FIXME TODO
     5 %
     6 % - update Proof General and X-symbol installation notes;
     7 % - update tactic emulation (including refcard);
     8 % - proof script conversion guide;
     9 
    10 
    11 \documentclass[12pt,a4paper,fleqn]{report}
    12 \usepackage{latexsym,graphicx,../iman,../extra,../ttbox,../proof,../rail,../railsetup,../isar,../pdfsetup}
    13 
    14 \title{\includegraphics[scale=0.5]{isabelle_isar} \\[4ex] The Isabelle/Isar Reference Manual}
    15 \author{\emph{Markus Wenzel} \\ TU M\"unchen}
    16 
    17 \makeindex
    18 
    19 \newcommand{\isastyle}{\small\tt\slshape}
    20 \newcommand{\isa}[1]{\emph{\isastyle #1}}
    21 \newcommand{\isasymColon}{\emph{$\mathrel{::}$}}
    22 \newcommand{\isasymRightarrow}{\emph{$\Rightarrow$}}
    23 
    24 \railterm{percent,ppercent,underscore,lbrace,rbrace,atsign}
    25 \railterm{ident,longident,symident,var,textvar,typefree,typevar,nat,string,verbatim,keyword}
    26 \railterm{name,nameref,text,type,term,prop,atom}
    27 
    28 \railalias{ident}{\railtoken{ident}}
    29 \railalias{longident}{\railtoken{longident}}
    30 \railalias{symident}{\railtoken{symident}}
    31 \railalias{var}{\railtoken{var}}
    32 \railalias{textvar}{\railtoken{textvar}}
    33 \railalias{typefree}{\railtoken{typefree}}
    34 \railalias{typevar}{\railtoken{typevar}}
    35 \railalias{nat}{\railtoken{nat}}
    36 \railalias{string}{\railtoken{string}}
    37 \railalias{verbatim}{\railtoken{verbatim}}
    38 \railalias{keyword}{\railtoken{keyword}}
    39 
    40 \railalias{name}{\railqtoken{name}}
    41 \railalias{nameref}{\railqtoken{nameref}}
    42 \railalias{text}{\railqtoken{text}}
    43 \railalias{type}{\railqtoken{type}}
    44 \railalias{term}{\railqtoken{term}}
    45 \railalias{prop}{\railqtoken{prop}}
    46 \railalias{atom}{\railqtoken{atom}}
    47 
    48 \newcommand{\drv}{\mathrel{\vdash}}
    49 \newcommand{\edrv}{\mathop{\drv}\nolimits}
    50 \newcommand{\Or}{\mathrel{\;|\;}}
    51 
    52 
    53 \setcounter{secnumdepth}{2} \setcounter{tocdepth}{2}
    54 
    55 \pagestyle{headings}
    56 \sloppy
    57 \binperiod     %%%treat . like a binary operator
    58 
    59 \renewcommand{\phi}{\varphi}
    60 
    61 %\includeonly{generic,refcard}
    62 
    63 
    64 \begin{document}
    65 
    66 \underscoreoff
    67 
    68 \maketitle 
    69 
    70 \begin{abstract}
    71   \emph{Intelligible semi-automated reasoning} (\emph{Isar}) is a generic
    72   approach to readable formal proof documents.  It sets out to bridge the
    73   semantic gap between any internal notions of proof based on primitive
    74   inferences and tactics, and an appropriate level of abstraction for
    75   user-level work.  The Isar formal proof language has been designed to
    76   satisfy quite contradictory requirements, being both ``declarative'' and
    77   immediately ``executable'', by virtue of the \emph{Isar/VM} interpreter.
    78   
    79   The current version of Isabelle offers Isar as an alternative proof language
    80   interface layer.  The Isabelle/Isar system provides an interpreter for the
    81   Isar formal proof language.  The input may consist either of proper document
    82   constructors, or improper auxiliary commands (for diagnostics, exploration
    83   etc.).  Proof texts consisting of proper elements only, admit a purely
    84   static reading, thus being intelligible later without requiring dynamic
    85   replay that is so typical for traditional proof scripts.  Any of the
    86   Isabelle/Isar commands may be executed in single-steps, so basically the
    87   interpreter has a proof text debugger already built-in.
    88   
    89   Employing the Isar instantiation of \emph{Proof~General}, a generic Emacs
    90   interface for interactive proof assistants, we arrive at a reasonable
    91   environment for \emph{live document editing}.  Thus proof texts may be
    92   developed incrementally by issuing proof commands, including forward and
    93   backward tracing of partial documents; intermediate states may be inspected
    94   by diagnostic commands.
    95   
    96   The Isar subsystem is tightly integrated into the Isabelle/Pure meta-logic
    97   implementation.  Theories, theorems, proof procedures etc.\ may be used
    98   interchangeably between classic Isabelle proof scripts and Isabelle/Isar
    99   documents.  Isar is as generic as Isabelle, able to support a wide range of
   100   object-logics.  Currently, the end-user working environment is most complete
   101   for Isabelle/HOL.
   102 \end{abstract}
   103 
   104 \pagenumbering{roman} \tableofcontents \clearfirst
   105 
   106 %FIXME
   107 \nocite{Aspinall:2000:eProof}
   108 \nocite{Bauer-Wenzel:2000:HB}
   109 \nocite{Harrison:1996:MizarHOL}
   110 \nocite{Muzalewski:Mizar}
   111 \nocite{Rudnicki:1992:MizarOverview}
   112 \nocite{Rudnicki:1992:MizarOverview}
   113 \nocite{Syme:1997:DECLARE}
   114 \nocite{Syme:1998:thesis}
   115 \nocite{Syme:1999:TPHOL}
   116 \nocite{Trybulec:1993:MizarFeatures}
   117 \nocite{Wiedijk:1999:Mizar}
   118 \nocite{Wiedijk:2000:MV}
   119 \nocite{Zammit:1999:TPHOL}
   120 
   121 \include{intro}
   122 \include{basics}
   123 \include{syntax}
   124 \include{pure}
   125 \include{generic}
   126 \include{hol}
   127 
   128 \appendix
   129 \include{refcard}
   130 \include{conversion}
   131 
   132 \begingroup
   133   \bibliographystyle{plain} \small\raggedright\frenchspacing
   134   \bibliography{../manual}
   135 \endgroup
   136 
   137 \printindex
   138 
   139 \end{document}