checkpoint;
authorwenzelm
Tue Jul 20 18:50:46 1999 +0200 (1999-07-20)
changeset 7050c70d3402fef5
parent 7049 f59d33c6e1c7
child 7051 9b6bdced3dc6
checkpoint;
doc-src/IsarRef/Makefile
doc-src/IsarRef/isar-ref.tex
doc-src/IsarRef/syntax.tex
doc-src/isar.sty
     1.1 --- a/doc-src/IsarRef/Makefile	Tue Jul 20 10:34:17 1999 +0200
     1.2 +++ b/doc-src/IsarRef/Makefile	Tue Jul 20 18:50:46 1999 +0200
     1.3 @@ -14,7 +14,7 @@
     1.4  NAME = isar-ref
     1.5  
     1.6  FILES = isar-ref.tex intro.tex basics.tex syntax.tex pure.tex \
     1.7 -	simplifier.tex classical.tex hol.tex \
     1.8 +	simplifier.tex classical.tex hol.tex ../isar.sty \
     1.9  	../rail.sty ../proof.sty ../iman.sty ../extra.sty ../manual.bib
    1.10  
    1.11  dvi: $(NAME).dvi
     2.1 --- a/doc-src/IsarRef/isar-ref.tex	Tue Jul 20 10:34:17 1999 +0200
     2.2 +++ b/doc-src/IsarRef/isar-ref.tex	Tue Jul 20 18:50:46 1999 +0200
     2.3 @@ -2,11 +2,13 @@
     2.4  %% $Id$
     2.5  
     2.6  \documentclass[12pt]{report}
     2.7 -\usepackage{graphicx,a4,../iman,../extra,../proof,../rail,../pdfsetup}
     2.8 +\usepackage{graphicx,a4,../iman,../extra,../proof,../rail,../isar,../pdfsetup}
     2.9  
    2.10  \title{\includegraphics[scale=0.5]{isabelle_isar} \\[4ex] The Isabelle/Isar Reference Manual}
    2.11 +\author{\emph{Markus Wenzel} \\ TU M\"unchen}
    2.12  
    2.13 -\author{\emph{Markus Wenzel} \\ TU M\"unchen}
    2.14 +\makeindex
    2.15 +
    2.16  
    2.17  \setcounter{secnumdepth}{2} \setcounter{tocdepth}{2}
    2.18  
    2.19 @@ -19,7 +21,15 @@
    2.20  \railterm{lbrace,rbrace}
    2.21  
    2.22  \railterm{ident,longident,symident,var,textvar,typefree,typevar,nat,string,verbatim}
    2.23 +\railterm{name,nameref,text,type,term,prop,atom}
    2.24  
    2.25 +\makeatletter
    2.26 +\newcommand{\railtoken}[1]{{\rail@termfont{#1}}}
    2.27 +\newcommand{\railnonterm}[1]{{\rail@nontfont{#1}}}
    2.28 +\makeatother
    2.29 +
    2.30 +\newcommand\indexoutertoken[1]{\index{#1@\railtoken{#1} (outer syntax)|bold}}
    2.31 +\newcommand\indexouternonterm[1]{\index{#1@\railnonterm{#1} (outer syntax)|bold}}
    2.32  
    2.33  \begin{document}
    2.34  
     3.1 --- a/doc-src/IsarRef/syntax.tex	Tue Jul 20 10:34:17 1999 +0200
     3.2 +++ b/doc-src/IsarRef/syntax.tex	Tue Jul 20 18:50:46 1999 +0200
     3.3 @@ -1,28 +1,59 @@
     3.4 +
     3.5 +%FIXME
     3.6 +% - examples (!?)
     3.7 +
     3.8  
     3.9  \chapter{Isar document syntax}
    3.10  
    3.11 -\section{Inner versus outer syntax}
    3.12 +FIXME important note: inner versus outer syntax
    3.13  
    3.14  \section{Lexical matters}
    3.15  
    3.16  \section{Common syntax entities}
    3.17  
    3.18 -\subsection{Atoms}
    3.19 +The Isar proof and theory language syntax has been carefully designed with
    3.20 +orthogonality in mind.  Many common syntax entities such that those for names,
    3.21 +terms, types etc.\ have been factored out.  Some of these basic syntactic
    3.22 +entities usually represent the level of abstraction for error messages: e.g.\ 
    3.23 +some higher syntax element such as $\CONSTS$ referring to \railtoken{name} or
    3.24 +\railtoken{type}, would really report a missing \railtoken{name} or
    3.25 +\railtoken{type} rather than any of its constituent primitive tokens (as
    3.26 +defined below).  These quasi-tokens are represented in the syntax diagrams
    3.27 +below using the same font as actual tokens (such as \railtoken{string}).
    3.28  
    3.29 +
    3.30 +\subsection{Names}
    3.31 +
    3.32 +Entity \railtoken{name} usually refers to any name of types, constants,
    3.33 +theorems, etc.\ to be \emph{declared} or \emph{defined} (so qualified
    3.34 +identifiers are excluded).  Already existing objects are typically referenced
    3.35 +by \railtoken{nameref}.
    3.36 +
    3.37 +\indexoutertoken{name}\indexoutertoken{nameref}
    3.38  \begin{rail}
    3.39    name : ident | symident | string
    3.40    ;
    3.41 -
    3.42    nameref : name | longident
    3.43    ;
    3.44 -
    3.45 -  text : nameref | verbatim
    3.46 -  ;
    3.47  \end{rail}
    3.48  
    3.49 +
    3.50  \subsection{Comments}
    3.51  
    3.52 +Large chunks of verbatim \railtoken{text} are usually given
    3.53 +\railtoken{verbatim}, i.e.\ enclosed in \verb|{*|~\verb|*}|; for convenience,
    3.54 +any of the smaller text entities (\railtoken{ident}, \railtoken{string} etc.)
    3.55 +are admitted as well.  Almost any of the Isar commands may be annotated by a
    3.56 +marginal comment: \texttt{--} \railtoken{text}.  Note that this kind of
    3.57 +comment is actually part of the language, while source level comments
    3.58 +\verb|(*|~\verb|*)| are already stripped at the lexical level.  A few commands
    3.59 +such as $\PROOFNAME$ admit some parts to be mark with a ``level of interest'':
    3.60 +currently only \texttt{\%} for ``boring, don't read this''.
    3.61 +
    3.62 +\indexoutertoken{text}\indexouternonterm{comment}\indexouternonterm{interest}
    3.63  \begin{rail}
    3.64 +  text : verbatim | nameref
    3.65 +  ;
    3.66    comment : (() | '--' text)
    3.67    ;
    3.68    interest : (() | '\%')
    3.69 @@ -32,30 +63,141 @@
    3.70  
    3.71  \subsection{Sorts and arities}
    3.72  
    3.73 +The syntax of sorts and arities is given directly at the outer level.  Note
    3.74 +that this in contrast to that types and terms (see below).  Only few commands
    3.75 +ever refer to sorts or arities explicitly.
    3.76 +
    3.77 +\indexouternonterm{sort}\indexouternonterm{arity}\indexouternonterm{simplearity}
    3.78  \begin{rail}
    3.79    sort : nameref | lbrace (nameref * ',') rbrace
    3.80    ;
    3.81    arity : ( () | '(' (sort + ',') ')' ) sort
    3.82    ;
    3.83 -  simple\-arity : ( () | '(' (sort + ',') ')' ) nameref
    3.84 +  simplearity : ( () | '(' (sort + ',') ')' ) nameref
    3.85 +  ;
    3.86 +\end{rail}
    3.87 +
    3.88 +
    3.89 +\subsection{Types and terms}
    3.90 +
    3.91 +The actual inner Isabelle syntax, i.e.\ that of types and terms, is far too
    3.92 +flexible in order to be modeled explicitly at the outer theory level.
    3.93 +Basically, any such entity would have to be quoted at the outer level to turn
    3.94 +it into a single token, with the actual parsing deferred to some functions
    3.95 +that read and type-check terms etc.\ (note that \railtoken{prop}s will be
    3.96 +handled differently from plain \railtoken{term}s here).  For convenience, the
    3.97 +quotes may be omitted for any \emph{atomic} term or type (e.g.\ a single
    3.98 +variable).
    3.99 +
   3.100 +\indexoutertoken{type}\indexoutertoken{term}\indexoutertoken{prop}
   3.101 +\begin{rail}
   3.102 +  type : ident | longident | symident | typefree | typevar | string
   3.103 +  ;
   3.104 +  term : ident | longident | symident | var | textvar | nat | string
   3.105 +  ;
   3.106 +  prop : term
   3.107 +  ;
   3.108 +\end{rail}
   3.109 +
   3.110 +Type definitions etc.\ usually refer to \railnonterm{typespec} on the
   3.111 +left-hand side.  This models basic type constructor application at the outer
   3.112 +syntax level.  Note that only plain postfix notation is available here, but no
   3.113 +infixes.
   3.114 +
   3.115 +\indexouternonterm{typespec}
   3.116 +\begin{rail}
   3.117 +  typespec : (() | typefree | '(' ( typefree + ',' ) ')') name
   3.118 +  ;
   3.119 +\end{rail}
   3.120 +
   3.121 +
   3.122 +\subsection{Term patterns}
   3.123 +
   3.124 +Statements like $\SHOWNAME$ involve propositions, some others like $\DEFNAME$
   3.125 +plain terms.  Any of these usually admit automatic binding of schematic text
   3.126 +variables by giving (optional) patterns $\IS{p@1 \dots p@n}$.  For
   3.127 +\railtoken{prop}s the $\CONCLNAME$ part refers to the conclusion only, in case
   3.128 +actual rules are involved, rather than atomic propositions.
   3.129 +
   3.130 +\indexouternonterm{termpat}\indexouternonterm{proppat}
   3.131 +\begin{rail}
   3.132 +  termpat : '(' (term + 'is' ) ')'
   3.133 +  ;
   3.134 +  proppat : '(' (() | (prop + 'is' )) (() | 'concl' (prop + 'is' )) ')'
   3.135    ;
   3.136  \end{rail}
   3.137  
   3.138  
   3.139 -\subsection{Terms and Types}
   3.140 +\subsection{Mixfix annotations}
   3.141 +
   3.142 +Mixfix annotations specify concrete \emph{inner} syntax.  Some commands such
   3.143 +as $\TYPES$ admit infixes only, while $\CONSTS$ etc.\ support the full range
   3.144 +of general mixfixes and binders.
   3.145  
   3.146 +\indexouternonterm{infix}\indexouternonterm{mixfix}
   3.147  \begin{rail}
   3.148 -  
   3.149 +  infix : '(' ('infixl' | 'infixr') (() | string) nat ')'
   3.150 +  ;
   3.151 +
   3.152 +  mixfix : infix | string (() | '[' (nat + ',') ']') (() | nat) |
   3.153 +  'binder' string (() | '[' (nat + ',') ']') nat
   3.154 +  ;
   3.155  \end{rail}
   3.156  
   3.157 -\subsection{Mixfix annotations}
   3.158 +
   3.159 +\subsection{Attributes and theorem specifications}\label{sec:syn-att}
   3.160 +
   3.161 +Attributes (and proof methods, see \S\ref{sec:syn-meth}) have their own
   3.162 +``semi-inner'' syntax, which does not have to be atomic at the outer level
   3.163 +unlike that of types and terms.  Instead, the attribute argument
   3.164 +specifications may be any sequence of atomic entities (identifiers, strings
   3.165 +etc.), or properly bracketed argument lists.  Below \railtoken{atom} refers to
   3.166 +any atomic entity (\railtoken{ident}, \railtoken{longident},
   3.167 +\railtoken{symident} etc.), including keywords that conform to
   3.168 +\railtoken{symident}, but do not coincide with actual command names.
   3.169 +
   3.170 +\indexoutertoken{atom}\indexouternonterm{args}\indexouternonterm{attributes}
   3.171 +\begin{rail}
   3.172 +  args : (atom | '(' (args *) ')' | '[' (args *) ']' | lbrace (args *) rbrace) *
   3.173 +  ;
   3.174 +  attributes : '[' (name args + ',') ']'
   3.175 +  ;
   3.176 +\end{rail}
   3.177 +
   3.178 +Theorem specifications come in three flavours: \railnonterm{thmdecl} usually
   3.179 +refers to the result of a goal statement (such as $\SHOWNAME$),
   3.180 +\railnonterm{thmdef} collects lists of existing theorems (as in $\NOTENAME$),
   3.181 +\railnonterm{thmref} refers to any list of existing theorems (e.g.\ occurring
   3.182 +as proof method arguments).  Any of these may include lists of attributes,
   3.183 +which are applied to the preceding theorem or list of theorems.
   3.184 +
   3.185 +\indexouternonterm{thmdecl}\indexouternonterm{thmdef}\indexouternonterm{thmref}
   3.186 +\begin{rail}
   3.187 +  thmdecl : (() | name) (() | attributes) ':'
   3.188 +  ;
   3.189 +  thmdef : (() | name) (() | attributes) '='
   3.190 +  ;
   3.191 +  thmref : (name (() | attributes) +)
   3.192 +  ;
   3.193 +\end{rail}
   3.194  
   3.195  
   3.196 -\subsection{}
   3.197 +\subsection{Proof methods}\label{sec:syn-meth}
   3.198  
   3.199 -\subsection{}
   3.200 +Proof methods are either basic ones, or expressions composed of methods via
   3.201 +``\texttt{,}'' (sequential composition), ``\texttt{|}'' (alternatives),
   3.202 +``\texttt{?}'' (try), ``\texttt{*}'' (repeat, ${} \ge 0$ times),
   3.203 +``\texttt{+}'' (repeat, ${} > 0$ times).  In practice, proof methods are
   3.204 +typically just a comma separeted list of \railtoken{name}~\railtoken{args}
   3.205 +specifications.  Thus the syntax is similar to that of attributes, with plain
   3.206 +parentheses instead of square brackets (see also \S\ref{sec:syn-att}).  Note
   3.207 +that parentheses may be dropped for methods without arguments.
   3.208  
   3.209 -\subsection{}
   3.210 +\indexouternonterm{method}
   3.211 +\begin{rail}
   3.212 +  method : (name args | (name | '(' method ')') (() | '?' | '*' | '+')) + (',' | '|')
   3.213 +  ;
   3.214 +\end{rail}
   3.215  
   3.216  
   3.217  %%% Local Variables: 
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/doc-src/isar.sty	Tue Jul 20 18:50:46 1999 +0200
     4.3 @@ -0,0 +1,70 @@
     4.4 +
     4.5 +%% $Id$
     4.6 +
     4.7 +\usepackage{ifthen}
     4.8 +
     4.9 +%Isar language elements
    4.10 +\newcommand{\I@keyword}[1]{{\mathord{\mathbf{#1}}}}
    4.11 +\newcommand{\I@optname}[1]{\ifthenelse{\equal{}{#1}}{}{~#1\colon}}
    4.12 +\newcommand{\I@optoptname}[1]{\ifthenelse{\equal{}{#1}}{}{~[#1\colon]}}
    4.13 +\newcommand{\I@optmeth}[1]{\ifthenelse{\equal{}{#1}}{}{~(#1)}}
    4.14 +\newcommand{\I@optoptmeth}[1]{\ifthenelse{\equal{}{#1}}{}{~[(#1)]}}
    4.15 +
    4.16 +\newcommand{\LEMMANAME}{\I@keyword{lemma}}
    4.17 +\newcommand{\THEOREMNAME}{\I@keyword{theorem}}
    4.18 +\newcommand{\NOTENAME}{\I@keyword{note}}
    4.19 +\newcommand{\FROMNAME}{\I@keyword{from}}
    4.20 +\newcommand{\WITHNAME}{\I@keyword{with}}
    4.21 +\newcommand{\FIXNAME}{\I@keyword{fix}}
    4.22 +\newcommand{\ASSUMENAME}{\I@keyword{assume}}
    4.23 +\newcommand{\PRESUMENAME}{\I@keyword{presume}}
    4.24 +\newcommand{\HAVENAME}{\I@keyword{have}}
    4.25 +\newcommand{\SHOWNAME}{\I@keyword{show}}
    4.26 +\newcommand{\HENCENAME}{\I@keyword{hence}}
    4.27 +\newcommand{\THUSNAME}{\I@keyword{thus}}
    4.28 +\newcommand{\PROOFNAME}{\I@keyword{proof}}
    4.29 +\newcommand{\QEDNAME}{\I@keyword{qed}}
    4.30 +\newcommand{\BYNAME}{\I@keyword{by}}
    4.31 +\newcommand{\ISNAME}{\I@keyword{is}}
    4.32 +\newcommand{\CONCLNAME}{\I@keyword{concl}}
    4.33 +\newcommand{\LETNAME}{\I@keyword{let}}
    4.34 +\newcommand{\DEFNAME}{\I@keyword{def}}
    4.35 +\newcommand{\SUFFNAME}{\I@keyword{suffient}}
    4.36 +\newcommand{\CMTNAME}{\I@keyword{-{}-}}
    4.37 +
    4.38 +\newcommand{\TYPES}{\I@keyword{types}}
    4.39 +\newcommand{\CONSTS}{\I@keyword{consts}}
    4.40 +\newcommand{\DEFS}{\I@keyword{defs}}
    4.41 +\newcommand{\NOTE}[2]{\NOTENAME~#1=#2}
    4.42 +\newcommand{\FROM}[1]{\FROMNAME~#1}
    4.43 +\newcommand{\WITH}[1]{\WITHNAME~#1}
    4.44 +\newcommand{\FIX}[1]{\FIXNAME~#1}
    4.45 +\newcommand{\ASSUME}[2]{\ASSUMENAME\I@optname{#1}~#2}
    4.46 +\newcommand{\PRESUME}[2]{\PRESUMENAME\I@optname{#1}~#2}
    4.47 +\newcommand{\THEN}{\I@keyword{then}}
    4.48 +\newcommand{\BEGIN}{\I@keyword{begin}}
    4.49 +\newcommand{\END}{\I@keyword{end}}
    4.50 +\newcommand{\BG}{\lceil}
    4.51 +\newcommand{\EN}{\rfloor}
    4.52 +\newcommand{\HAVE}[2]{\I@keyword{have}\I@optname{#1}~#2}
    4.53 +\newcommand{\SHOW}[2]{\I@keyword{show}\I@optname{#1}~#2}
    4.54 +\newcommand{\HENCE}[2]{\I@keyword{hence}\I@optname{#1}~#2}
    4.55 +\newcommand{\THUS}[2]{\I@keyword{thus}\I@optname{#1}~#2}
    4.56 +\newcommand{\LEMMA}[2]{\LEMMANAME\I@optname{#1}~#2}
    4.57 +\newcommand{\THEOREM}[2]{\THEOREMNAME\I@optname{#1}~#2}
    4.58 +\newcommand{\PROOF}[1]{\PROOFNAME\I@optmeth{#1}}
    4.59 +\newcommand{\PPROOF}[1]{\PPROOFNAME\I@optmeth{#1}}
    4.60 +\newcommand{\QED}[1]{\QEDNAME\I@optmeth{#1}}
    4.61 +\newcommand{\BY}[1]{\BYNAME\I@optmeth{#1}}
    4.62 +\newcommand{\DOT}{\I@keyword{.}}
    4.63 +\newcommand{\DDOT}{\I@keyword{.\,.}}
    4.64 +\newcommand{\DDDOT}{\dots}
    4.65 +\newcommand{\IS}[1]{(\ISNAME~#1)}
    4.66 +\newcommand{\LET}[1]{\LETNAME~#1}
    4.67 +\newcommand{\LETT}[1]{\LETNAME~#1\dt\;}
    4.68 +\newcommand{\DEF}[2]{\DEFNAME\I@optname{#1}~#2}
    4.69 +\newcommand{\SUFF}[1]{\SUFFNAME~#1}
    4.70 +\newcommand{\ATT}[1]{\ap [#1]}
    4.71 +\newcommand{\CMT}[1]{\CMTNAME~\text{#1}}
    4.72 +\newcommand{\ALSO}{\I@keyword{also}}
    4.73 +\newcommand{\FINALLY}{\I@keyword{finally}}