doc-src/Ref/theory-syntax.tex

first draft of Springer book

%% $Id$

\appendix
\newlinechar=-1  %mathsing.sty sets \newlinechar=`\|, which would cause mayhem

\chapter{Syntax of Isabelle Theories}\label{app:TheorySyntax}
\begin{itemize}
\item {\tt Typewriter font} denotes terminal symbols.
\item $id$, $tid$, $nat$, $string$ and $text$ are the lexical classes of
  identifiers, type identifiers, natural numbers, \ML\ strings (with their
  quotation marks) and arbitrary \ML\ text.  The first three are fully defined
  in the {\it Defining Logics} chapter of {\it Isabelle's Object Logics}.
\end{itemize}

\begin{rail}

theoryDef : id '=' (name + '+') ('+' extension | ());

name: id | string;

extension : classes default types arities consts trans rules 'end' ml
          ;

classes : ()
        | 'classes' ( ( id (  ()
                            | '<' (id + ',')
                           ) 
                       ) + )
        ;

default : ()
        | 'default' sort 
        ;

sort :  id
     | '\{' (id * ',') '\}'
     ;

types :  ()
      | 'types' ( ( type ( () | '(' infix ')' ) ) + )
      ;

type : ( () | tid | '(' ( tid + ',' ) ')') name ( () | '='  string );

infix : ( 'infixr' | 'infixl' ) nat;


arities :  ()
        | 'arities' ((( name + ',' ) '::' arity ) + )
        ;

arity   : ( () 
          | '(' (sort + ',') ')' 
          ) id
        ;


consts :  ()
       | 'consts' ( ( constDecl ( () | ( '(' mixfix ')' ) ) ) + )
       ;

constDecl : ( name + ',') '::' string ;


mixfix :  string ( () | ( () | ('[' (nat + ',') ']')) nat )
       | infix
       | 'binder' string nat ;

trans : ()
      | 'translations' ( pat ( '==' | '=>' | '<=' ) pat + )
      ;

pat : ( () | ( '(' id ')' ) ) string;

rules :  ()
      | 'rules' (( id string ) + )
      ;

ml :  ()
   | 'ML' text
   ;

\end{rail}