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