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