doc-src/Ref/theory-syntax.tex

A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
the tactic has also changed and allows the abstaction over fuction occurences whose type is nat or int.

%% $Id$

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

\chapter{Syntax of Isabelle Theories}\label{app:TheorySyntax}

Below we present the full syntax of theory definition files as provided by
Pure Isabelle --- object-logics may add their own sections.
\S\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 $longident$ are the lexical
  classes of identifiers, type identifiers, natural numbers, quoted
  strings (without the need for \verb$\$\dots\verb$\$ between lines)
  and long qualified \ML{} identifiers.
  The categories $id$, $tid$, $nat$ are fully defined in \iflabelundefined{Defining-Logics}%
  {{\it The Isabelle Reference Manual}, chapter `Defining Logics'}%
  {\S\ref{Defining-Logics}}.
  
\item $text$ is all text from the current position to the end of file,
  $verbatim$ is any text enclosed in \verb.{|.\dots\verb.|}.
  
\item Comments in theories take the form {\tt (*}\dots{\tt*)} and may
  be nested, just as in \ML.
\end{itemize}

\begin{rail}

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

name : id | string
     ;

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

section : classes
        | default
        | types
        | arities
        | nonterminals
        | consts
        | syntax
        | trans
        | defs
        | constdefs
        | rules
        | axclass
        | instance
        | oracle
        | locale
        | local
        | global
        | setup
        ;

classes : 'classes' ( classDecl + )
        ;

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

default : 'default' sort 
        ;

sort :  id
     | lbrace (id * ',') rbrace
     ;

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

infix : ( 'infixr' | 'infixl' ) (() | string) 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 + ',') ')' ) sort
      ;

nonterminals : 'nonterminals' (name+)
             ;

consts : 'consts' ( mixfixConstDecl + )
       ;

syntax : 'syntax' (() | mode) ( mixfixConstDecl + );

mode : '(' name (() | 'output') ')'
     ;

mixfixConstDecl : constDecl (() | ( '(' mixfix ')' ))
                ;

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

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

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

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

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

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

constdefs : 'constdefs' (name '::' (string | type) (() | mixfix) string +)
          ;

axclass : 'axclass' classDecl (() | ( id string ) +)
        ;

instance : 'instance' ( name '<' name | name '::' arity) witness
         ;

witness : (() | '(' ((string | id | longident) + ',') ')') (() | verbatim)
        ;

locale : 'locale' name '=' ( () | name '+' ) localeBody
       ;

localeBody : localeConsts ( () | localeAsms ) ( () | localeDefs )
       ;

localeConsts: ( 'fixes' ( ( (name '::' ( string | type )) ( () | '(' mixfix ')' ) ) + ) )
       ;


localeAsms:    ( 'assumes' ( ( id string ) + ) )
       ;

localeDefs:   ( 'defines' ( ( id string ) +) )
       ;

oracle : 'oracle' name '=' name
       ;

local : 'local'
      ;

global : 'global'
       ;

setup : 'setup' (id | longident)
      ;

ml : 'ML' text
   ;

\end{rail}


%%% Local Variables: 
%%% mode: latex
%%% TeX-master: "ref"
%%% End: