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