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