doc-src/Ref/theory-syntax.tex
author clasohm
Fri, 01 Dec 1995 14:20:09 +0100
changeset 1385 63c3d78df538
parent 1382 7e97232c1159
child 1488 b25a747876a4
permissions -rw-r--r--
changed typeDecl
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
13c35eb5169b Sections can now be given in any order.
nipkow
parents: 325
diff changeset
    35
        | trans
13c35eb5169b Sections can now be given in any order.
nipkow
parents: 325
diff changeset
    36
        | defs
13c35eb5169b Sections can now be given in any order.
nipkow
parents: 325
diff changeset
    37
        | rules
13c35eb5169b Sections can now be given in any order.
nipkow
parents: 325
diff changeset
    38
        ;
13c35eb5169b Sections can now be given in any order.
nipkow
parents: 325
diff changeset
    39
13c35eb5169b Sections can now be given in any order.
nipkow
parents: 325
diff changeset
    40
classes : 'classes' ( ( id (  ()
285
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
    41
                            | '<' (id + ',')
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
    42
                           ) 
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
    43
                       ) + )
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
    44
        ;
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
    45
1080
13c35eb5169b Sections can now be given in any order.
nipkow
parents: 325
diff changeset
    46
default : 'default' sort 
285
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
    47
        ;
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
    48
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
    49
sort :  id
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
    50
     | '\{' (id * ',') '\}'
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
    51
     ;
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
    52
1080
13c35eb5169b Sections can now be given in any order.
nipkow
parents: 325
diff changeset
    53
types : 'types' ( ( typeDecl ( () | '(' infix ')' ) ) + )
285
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
    54
      ;
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
    55
1385
63c3d78df538 changed typeDecl
clasohm
parents: 1382
diff changeset
    56
typeDecl : ( () | tid | '(' ( tid + ',' ) ')') name
63c3d78df538 changed typeDecl
clasohm
parents: 1382
diff changeset
    57
           ( () | '=' ( string | type ) );
63c3d78df538 changed typeDecl
clasohm
parents: 1382
diff changeset
    58
63c3d78df538 changed typeDecl
clasohm
parents: 1382
diff changeset
    59
type : simpleType | '(' type ')' | type '=>' type |
63c3d78df538 changed typeDecl
clasohm
parents: 1382
diff changeset
    60
       '[' ( type + "," ) ']' '=>' type;
63c3d78df538 changed typeDecl
clasohm
parents: 1382
diff changeset
    61
63c3d78df538 changed typeDecl
clasohm
parents: 1382
diff changeset
    62
simpleType: id | ( tid ( () | '::' id ) ) |
63c3d78df538 changed typeDecl
clasohm
parents: 1382
diff changeset
    63
            '(' ( type + "," ) ')' id | simpleType id;
285
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
    64
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
    65
infix : ( 'infixr' | 'infixl' ) nat;
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
    66
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
    67
1080
13c35eb5169b Sections can now be given in any order.
nipkow
parents: 325
diff changeset
    68
arities : 'arities' ((( name + ',' ) '::' arity ) + )
285
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
    69
        ;
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
    70
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
    71
arity   : ( () 
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
    72
          | '(' (sort + ',') ')' 
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
    73
          ) id
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
    74
        ;
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
    75
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
    76
1080
13c35eb5169b Sections can now be given in any order.
nipkow
parents: 325
diff changeset
    77
consts : 'consts' ( ( constDecl ( () | ( '(' mixfix ')' ) ) ) + )
285
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
    78
       ;
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
    79
1382
7e97232c1159 corrected diagrams for type and simpleType
clasohm
parents: 1379
diff changeset
    80
constDecl : ( name + ',') '::' (string | type);
285
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
    81
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
    82
mixfix :  string ( () | ( () | ('[' (nat + ',') ']')) nat )
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
    83
       | infix
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
    84
       | 'binder' string nat ;
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
    85
1080
13c35eb5169b Sections can now be given in any order.
nipkow
parents: 325
diff changeset
    86
trans : 'translations' ( pat ( '==' | '=>' | '<=' ) pat + )
285
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
    87
      ;
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
    88
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
    89
pat : ( () | ( '(' id ')' ) ) string;
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
    90
1080
13c35eb5169b Sections can now be given in any order.
nipkow
parents: 325
diff changeset
    91
rules : 'rules' (( id string ) + )
285
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
    92
      ;
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
    93
1080
13c35eb5169b Sections can now be given in any order.
nipkow
parents: 325
diff changeset
    94
defs : 'defs' (( id string ) + )
13c35eb5169b Sections can now be given in any order.
nipkow
parents: 325
diff changeset
    95
     ;
13c35eb5169b Sections can now be given in any order.
nipkow
parents: 325
diff changeset
    96
1082
1b30e27aca82 Simplified layout a little.
nipkow
parents: 1080
diff changeset
    97
ml : 'ML' text
285
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
    98
   ;
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
    99
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
   100
\end{rail}