# HG changeset patch # User wenzelm # Date 932489446 -7200 # Node ID c70d3402fef57e1d71877b02d42ad1209a26b7e0 # Parent f59d33c6e1c7951123d4031d03fb6e6f572623b6 checkpoint; diff -r f59d33c6e1c7 -r c70d3402fef5 doc-src/IsarRef/Makefile --- a/doc-src/IsarRef/Makefile Tue Jul 20 10:34:17 1999 +0200 +++ b/doc-src/IsarRef/Makefile Tue Jul 20 18:50:46 1999 +0200 @@ -14,7 +14,7 @@ NAME = isar-ref FILES = isar-ref.tex intro.tex basics.tex syntax.tex pure.tex \ - simplifier.tex classical.tex hol.tex \ + simplifier.tex classical.tex hol.tex ../isar.sty \ ../rail.sty ../proof.sty ../iman.sty ../extra.sty ../manual.bib dvi: $(NAME).dvi diff -r f59d33c6e1c7 -r c70d3402fef5 doc-src/IsarRef/isar-ref.tex --- a/doc-src/IsarRef/isar-ref.tex Tue Jul 20 10:34:17 1999 +0200 +++ b/doc-src/IsarRef/isar-ref.tex Tue Jul 20 18:50:46 1999 +0200 @@ -2,11 +2,13 @@ %% $Id$ \documentclass[12pt]{report} -\usepackage{graphicx,a4,../iman,../extra,../proof,../rail,../pdfsetup} +\usepackage{graphicx,a4,../iman,../extra,../proof,../rail,../isar,../pdfsetup} \title{\includegraphics[scale=0.5]{isabelle_isar} \\[4ex] The Isabelle/Isar Reference Manual} +\author{\emph{Markus Wenzel} \\ TU M\"unchen} -\author{\emph{Markus Wenzel} \\ TU M\"unchen} +\makeindex + \setcounter{secnumdepth}{2} \setcounter{tocdepth}{2} @@ -19,7 +21,15 @@ \railterm{lbrace,rbrace} \railterm{ident,longident,symident,var,textvar,typefree,typevar,nat,string,verbatim} +\railterm{name,nameref,text,type,term,prop,atom} +\makeatletter +\newcommand{\railtoken}[1]{{\rail@termfont{#1}}} +\newcommand{\railnonterm}[1]{{\rail@nontfont{#1}}} +\makeatother + +\newcommand\indexoutertoken[1]{\index{#1@\railtoken{#1} (outer syntax)|bold}} +\newcommand\indexouternonterm[1]{\index{#1@\railnonterm{#1} (outer syntax)|bold}} \begin{document} diff -r f59d33c6e1c7 -r c70d3402fef5 doc-src/IsarRef/syntax.tex --- a/doc-src/IsarRef/syntax.tex Tue Jul 20 10:34:17 1999 +0200 +++ b/doc-src/IsarRef/syntax.tex Tue Jul 20 18:50:46 1999 +0200 @@ -1,28 +1,59 @@ + +%FIXME +% - examples (!?) + \chapter{Isar document syntax} -\section{Inner versus outer syntax} +FIXME important note: inner versus outer syntax \section{Lexical matters} \section{Common syntax entities} -\subsection{Atoms} +The Isar proof and theory language syntax has been carefully designed with +orthogonality in mind. Many common syntax entities such that those for names, +terms, types etc.\ have been factored out. Some of these basic syntactic +entities usually represent the level of abstraction for error messages: e.g.\ +some higher syntax element such as $\CONSTS$ referring to \railtoken{name} or +\railtoken{type}, would really report a missing \railtoken{name} or +\railtoken{type} rather than any of its constituent primitive tokens (as +defined below). These quasi-tokens are represented in the syntax diagrams +below using the same font as actual tokens (such as \railtoken{string}). + +\subsection{Names} + +Entity \railtoken{name} usually refers to any name of types, constants, +theorems, etc.\ to be \emph{declared} or \emph{defined} (so qualified +identifiers are excluded). Already existing objects are typically referenced +by \railtoken{nameref}. + +\indexoutertoken{name}\indexoutertoken{nameref} \begin{rail} name : ident | symident | string ; - nameref : name | longident ; - - text : nameref | verbatim - ; \end{rail} + \subsection{Comments} +Large chunks of verbatim \railtoken{text} are usually given +\railtoken{verbatim}, i.e.\ enclosed in \verb|{*|~\verb|*}|; for convenience, +any of the smaller text entities (\railtoken{ident}, \railtoken{string} etc.) +are admitted as well. Almost any of the Isar commands may be annotated by a +marginal comment: \texttt{--} \railtoken{text}. Note that this kind of +comment is actually part of the language, while source level comments +\verb|(*|~\verb|*)| are already stripped at the lexical level. A few commands +such as $\PROOFNAME$ admit some parts to be mark with a ``level of interest'': +currently only \texttt{\%} for ``boring, don't read this''. + +\indexoutertoken{text}\indexouternonterm{comment}\indexouternonterm{interest} \begin{rail} + text : verbatim | nameref + ; comment : (() | '--' text) ; interest : (() | '\%') @@ -32,30 +63,141 @@ \subsection{Sorts and arities} +The syntax of sorts and arities is given directly at the outer level. Note +that this in contrast to that types and terms (see below). Only few commands +ever refer to sorts or arities explicitly. + +\indexouternonterm{sort}\indexouternonterm{arity}\indexouternonterm{simplearity} \begin{rail} sort : nameref | lbrace (nameref * ',') rbrace ; arity : ( () | '(' (sort + ',') ')' ) sort ; - simple\-arity : ( () | '(' (sort + ',') ')' ) nameref + simplearity : ( () | '(' (sort + ',') ')' ) nameref + ; +\end{rail} + + +\subsection{Types and terms} + +The actual inner Isabelle syntax, i.e.\ that of types and terms, is far too +flexible in order to be modeled explicitly at the outer theory level. +Basically, any such entity would have to be quoted at the outer level to turn +it into a single token, with the actual parsing deferred to some functions +that read and type-check terms etc.\ (note that \railtoken{prop}s will be +handled differently from plain \railtoken{term}s here). For convenience, the +quotes may be omitted for any \emph{atomic} term or type (e.g.\ a single +variable). + +\indexoutertoken{type}\indexoutertoken{term}\indexoutertoken{prop} +\begin{rail} + type : ident | longident | symident | typefree | typevar | string + ; + term : ident | longident | symident | var | textvar | nat | string + ; + prop : term + ; +\end{rail} + +Type definitions etc.\ usually refer to \railnonterm{typespec} on the +left-hand side. This models basic type constructor application at the outer +syntax level. Note that only plain postfix notation is available here, but no +infixes. + +\indexouternonterm{typespec} +\begin{rail} + typespec : (() | typefree | '(' ( typefree + ',' ) ')') name + ; +\end{rail} + + +\subsection{Term patterns} + +Statements like $\SHOWNAME$ involve propositions, some others like $\DEFNAME$ +plain terms. Any of these usually admit automatic binding of schematic text +variables by giving (optional) patterns $\IS{p@1 \dots p@n}$. For +\railtoken{prop}s the $\CONCLNAME$ part refers to the conclusion only, in case +actual rules are involved, rather than atomic propositions. + +\indexouternonterm{termpat}\indexouternonterm{proppat} +\begin{rail} + termpat : '(' (term + 'is' ) ')' + ; + proppat : '(' (() | (prop + 'is' )) (() | 'concl' (prop + 'is' )) ')' ; \end{rail} -\subsection{Terms and Types} +\subsection{Mixfix annotations} + +Mixfix annotations specify concrete \emph{inner} syntax. Some commands such +as $\TYPES$ admit infixes only, while $\CONSTS$ etc.\ support the full range +of general mixfixes and binders. +\indexouternonterm{infix}\indexouternonterm{mixfix} \begin{rail} - + infix : '(' ('infixl' | 'infixr') (() | string) nat ')' + ; + + mixfix : infix | string (() | '[' (nat + ',') ']') (() | nat) | + 'binder' string (() | '[' (nat + ',') ']') nat + ; \end{rail} -\subsection{Mixfix annotations} + +\subsection{Attributes and theorem specifications}\label{sec:syn-att} + +Attributes (and proof methods, see \S\ref{sec:syn-meth}) have their own +``semi-inner'' syntax, which does not have to be atomic at the outer level +unlike that of types and terms. Instead, the attribute argument +specifications may be any sequence of atomic entities (identifiers, strings +etc.), or properly bracketed argument lists. Below \railtoken{atom} refers to +any atomic entity (\railtoken{ident}, \railtoken{longident}, +\railtoken{symident} etc.), including keywords that conform to +\railtoken{symident}, but do not coincide with actual command names. + +\indexoutertoken{atom}\indexouternonterm{args}\indexouternonterm{attributes} +\begin{rail} + args : (atom | '(' (args *) ')' | '[' (args *) ']' | lbrace (args *) rbrace) * + ; + attributes : '[' (name args + ',') ']' + ; +\end{rail} + +Theorem specifications come in three flavours: \railnonterm{thmdecl} usually +refers to the result of a goal statement (such as $\SHOWNAME$), +\railnonterm{thmdef} collects lists of existing theorems (as in $\NOTENAME$), +\railnonterm{thmref} refers to any list of existing theorems (e.g.\ occurring +as proof method arguments). Any of these may include lists of attributes, +which are applied to the preceding theorem or list of theorems. + +\indexouternonterm{thmdecl}\indexouternonterm{thmdef}\indexouternonterm{thmref} +\begin{rail} + thmdecl : (() | name) (() | attributes) ':' + ; + thmdef : (() | name) (() | attributes) '=' + ; + thmref : (name (() | attributes) +) + ; +\end{rail} -\subsection{} +\subsection{Proof methods}\label{sec:syn-meth} -\subsection{} +Proof methods are either basic ones, or expressions composed of methods via +``\texttt{,}'' (sequential composition), ``\texttt{|}'' (alternatives), +``\texttt{?}'' (try), ``\texttt{*}'' (repeat, ${} \ge 0$ times), +``\texttt{+}'' (repeat, ${} > 0$ times). In practice, proof methods are +typically just a comma separeted list of \railtoken{name}~\railtoken{args} +specifications. Thus the syntax is similar to that of attributes, with plain +parentheses instead of square brackets (see also \S\ref{sec:syn-att}). Note +that parentheses may be dropped for methods without arguments. -\subsection{} +\indexouternonterm{method} +\begin{rail} + method : (name args | (name | '(' method ')') (() | '?' | '*' | '+')) + (',' | '|') + ; +\end{rail} %%% Local Variables: diff -r f59d33c6e1c7 -r c70d3402fef5 doc-src/isar.sty --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/doc-src/isar.sty Tue Jul 20 18:50:46 1999 +0200 @@ -0,0 +1,70 @@ + +%% $Id$ + +\usepackage{ifthen} + +%Isar language elements +\newcommand{\I@keyword}[1]{{\mathord{\mathbf{#1}}}} +\newcommand{\I@optname}[1]{\ifthenelse{\equal{}{#1}}{}{~#1\colon}} +\newcommand{\I@optoptname}[1]{\ifthenelse{\equal{}{#1}}{}{~[#1\colon]}} +\newcommand{\I@optmeth}[1]{\ifthenelse{\equal{}{#1}}{}{~(#1)}} +\newcommand{\I@optoptmeth}[1]{\ifthenelse{\equal{}{#1}}{}{~[(#1)]}} + +\newcommand{\LEMMANAME}{\I@keyword{lemma}} +\newcommand{\THEOREMNAME}{\I@keyword{theorem}} +\newcommand{\NOTENAME}{\I@keyword{note}} +\newcommand{\FROMNAME}{\I@keyword{from}} +\newcommand{\WITHNAME}{\I@keyword{with}} +\newcommand{\FIXNAME}{\I@keyword{fix}} +\newcommand{\ASSUMENAME}{\I@keyword{assume}} +\newcommand{\PRESUMENAME}{\I@keyword{presume}} +\newcommand{\HAVENAME}{\I@keyword{have}} +\newcommand{\SHOWNAME}{\I@keyword{show}} +\newcommand{\HENCENAME}{\I@keyword{hence}} +\newcommand{\THUSNAME}{\I@keyword{thus}} +\newcommand{\PROOFNAME}{\I@keyword{proof}} +\newcommand{\QEDNAME}{\I@keyword{qed}} +\newcommand{\BYNAME}{\I@keyword{by}} +\newcommand{\ISNAME}{\I@keyword{is}} +\newcommand{\CONCLNAME}{\I@keyword{concl}} +\newcommand{\LETNAME}{\I@keyword{let}} +\newcommand{\DEFNAME}{\I@keyword{def}} +\newcommand{\SUFFNAME}{\I@keyword{suffient}} +\newcommand{\CMTNAME}{\I@keyword{-{}-}} + +\newcommand{\TYPES}{\I@keyword{types}} +\newcommand{\CONSTS}{\I@keyword{consts}} +\newcommand{\DEFS}{\I@keyword{defs}} +\newcommand{\NOTE}[2]{\NOTENAME~#1=#2} +\newcommand{\FROM}[1]{\FROMNAME~#1} +\newcommand{\WITH}[1]{\WITHNAME~#1} +\newcommand{\FIX}[1]{\FIXNAME~#1} +\newcommand{\ASSUME}[2]{\ASSUMENAME\I@optname{#1}~#2} +\newcommand{\PRESUME}[2]{\PRESUMENAME\I@optname{#1}~#2} +\newcommand{\THEN}{\I@keyword{then}} +\newcommand{\BEGIN}{\I@keyword{begin}} +\newcommand{\END}{\I@keyword{end}} +\newcommand{\BG}{\lceil} +\newcommand{\EN}{\rfloor} +\newcommand{\HAVE}[2]{\I@keyword{have}\I@optname{#1}~#2} +\newcommand{\SHOW}[2]{\I@keyword{show}\I@optname{#1}~#2} +\newcommand{\HENCE}[2]{\I@keyword{hence}\I@optname{#1}~#2} +\newcommand{\THUS}[2]{\I@keyword{thus}\I@optname{#1}~#2} +\newcommand{\LEMMA}[2]{\LEMMANAME\I@optname{#1}~#2} +\newcommand{\THEOREM}[2]{\THEOREMNAME\I@optname{#1}~#2} +\newcommand{\PROOF}[1]{\PROOFNAME\I@optmeth{#1}} +\newcommand{\PPROOF}[1]{\PPROOFNAME\I@optmeth{#1}} +\newcommand{\QED}[1]{\QEDNAME\I@optmeth{#1}} +\newcommand{\BY}[1]{\BYNAME\I@optmeth{#1}} +\newcommand{\DOT}{\I@keyword{.}} +\newcommand{\DDOT}{\I@keyword{.\,.}} +\newcommand{\DDDOT}{\dots} +\newcommand{\IS}[1]{(\ISNAME~#1)} +\newcommand{\LET}[1]{\LETNAME~#1} +\newcommand{\LETT}[1]{\LETNAME~#1\dt\;} +\newcommand{\DEF}[2]{\DEFNAME\I@optname{#1}~#2} +\newcommand{\SUFF}[1]{\SUFFNAME~#1} +\newcommand{\ATT}[1]{\ap [#1]} +\newcommand{\CMT}[1]{\CMTNAME~\text{#1}} +\newcommand{\ALSO}{\I@keyword{also}} +\newcommand{\FINALLY}{\I@keyword{finally}}