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{Terms and Types}
3.90 +\subsection{Types and terms}
3.91
3.92 +The actual inner Isabelle syntax, i.e.\ that of types and terms, is far too
3.93 +flexible in order to be modeled explicitly at the outer theory level.
3.94 +Basically, any such entity would have to be quoted at the outer level to turn
3.95 +it into a single token, with the actual parsing deferred to some functions
3.96 +that read and type-check terms etc.\ (note that \railtoken{prop}s will be
3.97 +handled differently from plain \railtoken{term}s here). For convenience, the
3.98 +quotes may be omitted for any \emph{atomic} term or type (e.g.\ a single
3.99 +variable).
3.100 +
3.101 +\indexoutertoken{type}\indexoutertoken{term}\indexoutertoken{prop}
3.102 \begin{rail}
3.103 -
3.104 + type : ident | longident | symident | typefree | typevar | string
3.105 + ;
3.106 + term : ident | longident | symident | var | textvar | nat | string
3.107 + ;
3.108 + prop : term
3.109 + ;
3.110 \end{rail}
3.111
3.112 +Type definitions etc.\ usually refer to \railnonterm{typespec} on the
3.113 +left-hand side. This models basic type constructor application at the outer
3.114 +syntax level. Note that only plain postfix notation is available here, but no
3.115 +infixes.
3.116 +
3.117 +\indexouternonterm{typespec}
3.118 +\begin{rail}
3.119 + typespec : (() | typefree | '(' ( typefree + ',' ) ')') name
3.120 + ;
3.121 +\end{rail}
3.122 +
3.123 +
3.124 +\subsection{Term patterns}
3.125 +
3.126 +Statements like $\SHOWNAME$ involve propositions, some others like $\DEFNAME$
3.127 +plain terms. Any of these usually admit automatic binding of schematic text
3.128 +variables by giving (optional) patterns $\IS{p@1 \dots p@n}$. For
3.129 +\railtoken{prop}s the $\CONCLNAME$ part refers to the conclusion only, in case
3.130 +actual rules are involved, rather than atomic propositions.
3.131 +
3.132 +\indexouternonterm{termpat}\indexouternonterm{proppat}
3.133 +\begin{rail}
3.134 + termpat : '(' (term + 'is' ) ')'
3.135 + ;
3.136 + proppat : '(' (() | (prop + 'is' )) (() | 'concl' (prop + 'is' )) ')'
3.137 + ;
3.138 +\end{rail}
3.139 +
3.140 +
3.141 \subsection{Mixfix annotations}
3.142
3.143 +Mixfix annotations specify concrete \emph{inner} syntax. Some commands such
3.144 +as $\TYPES$ admit infixes only, while $\CONSTS$ etc.\ support the full range
3.145 +of general mixfixes and binders.
3.146
3.147 -\subsection{}
3.148 +\indexouternonterm{infix}\indexouternonterm{mixfix}
3.149 +\begin{rail}
3.150 + infix : '(' ('infixl' | 'infixr') (() | string) nat ')'
3.151 + ;
3.152
3.153 -\subsection{}
3.154 + mixfix : infix | string (() | '[' (nat + ',') ']') (() | nat) |
3.155 + 'binder' string (() | '[' (nat + ',') ']') nat
3.156 + ;
3.157 +\end{rail}
3.158
3.159 -\subsection{}
3.160 +
3.161 +\subsection{Attributes and theorem specifications}\label{sec:syn-att}
3.162 +
3.163 +Attributes (and proof methods, see \S\ref{sec:syn-meth}) have their own
3.164 +``semi-inner'' syntax, which does not have to be atomic at the outer level
3.165 +unlike that of types and terms. Instead, the attribute argument
3.166 +specifications may be any sequence of atomic entities (identifiers, strings
3.167 +etc.), or properly bracketed argument lists. Below \railtoken{atom} refers to
3.168 +any atomic entity (\railtoken{ident}, \railtoken{longident},
3.169 +\railtoken{symident} etc.), including keywords that conform to
3.170 +\railtoken{symident}, but do not coincide with actual command names.
3.171 +
3.172 +\indexoutertoken{atom}\indexouternonterm{args}\indexouternonterm{attributes}
3.173 +\begin{rail}
3.174 + args : (atom | '(' (args *) ')' | '[' (args *) ']' | lbrace (args *) rbrace) *
3.175 + ;
3.176 + attributes : '[' (name args + ',') ']'
3.177 + ;
3.178 +\end{rail}
3.179 +
3.180 +Theorem specifications come in three flavours: \railnonterm{thmdecl} usually
3.181 +refers to the result of a goal statement (such as $\SHOWNAME$),
3.182 +\railnonterm{thmdef} collects lists of existing theorems (as in $\NOTENAME$),
3.183 +\railnonterm{thmref} refers to any list of existing theorems (e.g.\ occurring
3.184 +as proof method arguments). Any of these may include lists of attributes,
3.185 +which are applied to the preceding theorem or list of theorems.
3.186 +
3.187 +\indexouternonterm{thmdecl}\indexouternonterm{thmdef}\indexouternonterm{thmref}
3.188 +\begin{rail}
3.189 + thmdecl : (() | name) (() | attributes) ':'
3.190 + ;
3.191 + thmdef : (() | name) (() | attributes) '='
3.192 + ;
3.193 + thmref : (name (() | attributes) +)
3.194 + ;
3.195 +\end{rail}
3.196 +
3.197 +
3.198 +\subsection{Proof methods}\label{sec:syn-meth}
3.199 +
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 +\indexouternonterm{method}
3.210 +\begin{rail}
3.211 + method : (name args | (name | '(' method ')') (() | '?' | '*' | '+')) + (',' | '|')
3.212 + ;
3.213 +\end{rail}
3.214
3.215
3.216 %%% 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}}