doc-src/Ref/theory-syntax.tex
author berghofe
Fri, 02 May 1997 16:41:35 +0200
changeset 3098 a31170b67367
parent 1846 763f08fb194f
child 3108 335efc3f5632
permissions -rw-r--r--
Updated to LaTeX 2e
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
285
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
     1
%% $Id$
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
     2
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
     3
\appendix
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
     4
\newlinechar=-1  %mathsing.sty sets \newlinechar=`\|, which would cause mayhem
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
     5
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
     6
\chapter{Syntax of Isabelle Theories}\label{app:TheorySyntax}
325
49baeba86546 penultimate Springer draft
lcp
parents: 295
diff changeset
     7
Chapter~\ref{sec:ref-defining-theories} explains the meanings of these
49baeba86546 penultimate Springer draft
lcp
parents: 295
diff changeset
     8
constructs.  The syntax obeys the following conventions:
285
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
     9
\begin{itemize}
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
    10
\item {\tt Typewriter font} denotes terminal symbols.
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
    11
\item $id$, $tid$, $nat$, $string$ and $text$ are the lexical classes of
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
    12
  identifiers, type identifiers, natural numbers, \ML\ strings (with their
1148
e125fc7a1183 Added remark that \...\ in strings is unnecessary.
nipkow
parents: 1082
diff changeset
    13
  quotation marks, but without the need for \verb$\$ at the end of a line and
e125fc7a1183 Added remark that \...\ in strings is unnecessary.
nipkow
parents: 1082
diff changeset
    14
  the beginning of the next line) and arbitrary \ML\ text.  The first three
e125fc7a1183 Added remark that \...\ in strings is unnecessary.
nipkow
parents: 1082
diff changeset
    15
  are fully defined in \iflabelundefined{Defining-Logics}%
325
49baeba86546 penultimate Springer draft
lcp
parents: 295
diff changeset
    16
    {{\it The Isabelle Reference Manual}, chapter `Defining Logics'}%
49baeba86546 penultimate Springer draft
lcp
parents: 295
diff changeset
    17
    {Chap.\ts\ref{Defining-Logics}}.
285
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
    18
\end{itemize}
325
49baeba86546 penultimate Springer draft
lcp
parents: 295
diff changeset
    19
Comments in theories take the form {\tt (*} {\it text\/} {\tt*)}, where
49baeba86546 penultimate Springer draft
lcp
parents: 295
diff changeset
    20
{\it text\/} should not contain the character sequence {\tt*)}.
285
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
    21
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
    22
\begin{rail}
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
    23
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
    24
theoryDef : id '=' (name + '+') ('+' extension | ());
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
    25
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
    26
name: id | string;
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
    27
1082
1b30e27aca82 Simplified layout a little.
nipkow
parents: 1080
diff changeset
    28
extension : (section +) 'end' ( () | ml );
285
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
    29
1080
13c35eb5169b Sections can now be given in any order.
nipkow
parents: 325
diff changeset
    30
section : classes
13c35eb5169b Sections can now be given in any order.
nipkow
parents: 325
diff changeset
    31
        | default
13c35eb5169b Sections can now be given in any order.
nipkow
parents: 325
diff changeset
    32
        | types
13c35eb5169b Sections can now be given in any order.
nipkow
parents: 325
diff changeset
    33
        | arities
13c35eb5169b Sections can now be given in any order.
nipkow
parents: 325
diff changeset
    34
        | consts
1650
a4ed2655b08c Added 'constdefs'
nipkow
parents: 1488
diff changeset
    35
        | constdefs
1080
13c35eb5169b Sections can now be given in any order.
nipkow
parents: 325
diff changeset
    36
        | trans
13c35eb5169b Sections can now be given in any order.
nipkow
parents: 325
diff changeset
    37
        | defs
13c35eb5169b Sections can now be given in any order.
nipkow
parents: 325
diff changeset
    38
        | rules
1846
763f08fb194f Documentation of oracles and their syntax
paulson
parents: 1650
diff changeset
    39
        | oracle
1080
13c35eb5169b Sections can now be given in any order.
nipkow
parents: 325
diff changeset
    40
        ;
13c35eb5169b Sections can now be given in any order.
nipkow
parents: 325
diff changeset
    41
13c35eb5169b Sections can now be given in any order.
nipkow
parents: 325
diff changeset
    42
classes : 'classes' ( ( id (  ()
285
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
    43
                            | '<' (id + ',')
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
    44
                           ) 
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
    45
                       ) + )
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
    46
        ;
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
    47
1080
13c35eb5169b Sections can now be given in any order.
nipkow
parents: 325
diff changeset
    48
default : 'default' sort 
285
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
    49
        ;
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
    50
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
    51
sort :  id
3098
a31170b67367 Updated to LaTeX 2e
berghofe
parents: 1846
diff changeset
    52
     | lbrace (id * ',') rbrace
285
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
    53
     ;
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
    54
1080
13c35eb5169b Sections can now be given in any order.
nipkow
parents: 325
diff changeset
    55
types : 'types' ( ( typeDecl ( () | '(' infix ')' ) ) + )
285
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
    56
      ;
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
    57
1488
b25a747876a4 Added typevarlist
nipkow
parents: 1385
diff changeset
    58
infix : ( 'infixr' | 'infixl' ) nat;
b25a747876a4 Added typevarlist
nipkow
parents: 1385
diff changeset
    59
b25a747876a4 Added typevarlist
nipkow
parents: 1385
diff changeset
    60
typeDecl : typevarlist name
1385
63c3d78df538 changed typeDecl
clasohm
parents: 1382
diff changeset
    61
           ( () | '=' ( string | type ) );
63c3d78df538 changed typeDecl
clasohm
parents: 1382
diff changeset
    62
1488
b25a747876a4 Added typevarlist
nipkow
parents: 1385
diff changeset
    63
typevarlist : () | tid | '(' ( tid + ',' ) ')';
b25a747876a4 Added typevarlist
nipkow
parents: 1385
diff changeset
    64
1385
63c3d78df538 changed typeDecl
clasohm
parents: 1382
diff changeset
    65
type : simpleType | '(' type ')' | type '=>' type |
63c3d78df538 changed typeDecl
clasohm
parents: 1382
diff changeset
    66
       '[' ( type + "," ) ']' '=>' type;
63c3d78df538 changed typeDecl
clasohm
parents: 1382
diff changeset
    67
63c3d78df538 changed typeDecl
clasohm
parents: 1382
diff changeset
    68
simpleType: id | ( tid ( () | '::' id ) ) |
63c3d78df538 changed typeDecl
clasohm
parents: 1382
diff changeset
    69
            '(' ( type + "," ) ')' id | simpleType id;
285
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
    70
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
    71
1080
13c35eb5169b Sections can now be given in any order.
nipkow
parents: 325
diff changeset
    72
arities : 'arities' ((( name + ',' ) '::' arity ) + )
285
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
    73
        ;
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
    74
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
    75
arity   : ( () 
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
    76
          | '(' (sort + ',') ')' 
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
    77
          ) id
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
    78
        ;
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
    79
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
    80
1080
13c35eb5169b Sections can now be given in any order.
nipkow
parents: 325
diff changeset
    81
consts : 'consts' ( ( constDecl ( () | ( '(' mixfix ')' ) ) ) + )
285
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
    82
       ;
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
    83
1382
7e97232c1159 corrected diagrams for type and simpleType
clasohm
parents: 1379
diff changeset
    84
constDecl : ( name + ',') '::' (string | type);
285
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
    85
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
    86
mixfix :  string ( () | ( () | ('[' (nat + ',') ']')) nat )
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
    87
       | infix
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
    88
       | 'binder' string nat ;
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
    89
1650
a4ed2655b08c Added 'constdefs'
nipkow
parents: 1488
diff changeset
    90
constdefs : 'constdefs' (id '::' (string | type) string +)
a4ed2655b08c Added 'constdefs'
nipkow
parents: 1488
diff changeset
    91
          ;
a4ed2655b08c Added 'constdefs'
nipkow
parents: 1488
diff changeset
    92
1080
13c35eb5169b Sections can now be given in any order.
nipkow
parents: 325
diff changeset
    93
trans : 'translations' ( pat ( '==' | '=>' | '<=' ) pat + )
285
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
    94
      ;
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
    95
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
    96
pat : ( () | ( '(' id ')' ) ) string;
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
    97
1080
13c35eb5169b Sections can now be given in any order.
nipkow
parents: 325
diff changeset
    98
rules : 'rules' (( id string ) + )
285
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
    99
      ;
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
   100
1080
13c35eb5169b Sections can now be given in any order.
nipkow
parents: 325
diff changeset
   101
defs : 'defs' (( id string ) + )
13c35eb5169b Sections can now be given in any order.
nipkow
parents: 325
diff changeset
   102
     ;
13c35eb5169b Sections can now be given in any order.
nipkow
parents: 325
diff changeset
   103
1846
763f08fb194f Documentation of oracles and their syntax
paulson
parents: 1650
diff changeset
   104
oracle : 'oracle' name
763f08fb194f Documentation of oracles and their syntax
paulson
parents: 1650
diff changeset
   105
       ;
763f08fb194f Documentation of oracles and their syntax
paulson
parents: 1650
diff changeset
   106
1082
1b30e27aca82 Simplified layout a little.
nipkow
parents: 1080
diff changeset
   107
ml : 'ML' text
285
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
   108
   ;
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
   109
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
   110
\end{rail}