doc-src/Ref/theory-syntax.tex

New root file with more description, and merging LK and Modal to Sequents

%% $Id$

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

\chapter{Syntax of Isabelle Theories}\label{app:TheorySyntax}
Chapter~\ref{sec:ref-defining-theories} explains the meanings of these
constructs.  The syntax obeys the following conventions:
\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, but without the need for \verb$\$ at the end of a line and
  the beginning of the next line) and arbitrary \ML\ text.  The first three
  are fully defined in \iflabelundefined{Defining-Logics}%
    {{\it The Isabelle Reference Manual}, chapter `Defining Logics'}%
    {Chap.\ts\ref{Defining-Logics}}.
\end{itemize}
Comments in theories take the form {\tt (*} {\it text\/} {\tt*)}, where
{\it text\/} should not contain the character sequence {\tt*)}.

\begin{rail}

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

name: id | string;

extension : (section +) 'end' ( () | ml );

section : classes
        | default
        | types
        | arities
        | consts
        | constdefs
        | trans
        | defs
        | rules
        | oracle
        ;

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

default : 'default' sort 
        ;

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

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

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

typeDecl : typevarlist name
           ( () | '=' ( string | type ) );

typevarlist : () | tid | '(' ( tid + ',' ) ')';

type : simpleType | '(' type ')' | type '=>' type |
       '[' ( type + "," ) ']' '=>' type;

simpleType: id | ( tid ( () | '::' id ) ) |
            '(' ( type + "," ) ')' id | simpleType id;


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

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


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

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

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

constdefs : 'constdefs' (id '::' (string | type) string +)
          ;

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

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

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

defs : 'defs' (( id string ) + )
     ;

oracle : 'oracle' name
       ;

ml : 'ML' text
   ;

\end{rail}