doc-src/Ref/theory-syntax.tex
author paulson
Wed, 07 Oct 1998 10:31:30 +0200
changeset 5619 76a8c72e3fd4
parent 5369 8384e01b6cf8
child 6669 5f1ce866c497
permissions -rw-r--r--
new theorems
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}
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset
     7
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset
     8
Below we present the full syntax of theory definition files as
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset
     9
provided by {\Pure} Isabelle --- object-logics may add their own
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset
    10
sections.  \S\ref{sec:ref-defining-theories} explains the meanings of
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset
    11
these constructs.  The syntax obeys the following conventions:
285
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
    12
\begin{itemize}
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
    13
\item {\tt Typewriter font} denotes terminal symbols.
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset
    14
  
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset
    15
\item $id$, $tid$, $nat$, $string$ and $longident$ are the lexical
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset
    16
  classes of identifiers, type identifiers, natural numbers, quoted
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset
    17
  strings (without the need for \verb$\$\dots\verb$\$ between lines)
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset
    18
  and long qualified \ML{} identifiers.
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset
    19
  The categories $id$, $tid$, $nat$ are fully defined in \iflabelundefined{Defining-Logics}%
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset
    20
  {{\it The Isabelle Reference Manual}, chapter `Defining Logics'}%
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset
    21
  {\S\ref{Defining-Logics}}.
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset
    22
  
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset
    23
\item $text$ is all text from the current position to the end of file,
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset
    24
  $verbatim$ is any text enclosed in \verb.{|.\dots\verb.|}.
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset
    25
  
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset
    26
\item Comments in theories take the form {\tt (*}\dots{\tt*)} and may
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset
    27
  be nested, just as in \ML.
285
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
    28
\end{itemize}
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
    29
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
    30
\begin{rail}
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
    31
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset
    32
theoryDef : id '=' (name + '+') ('+' extension | ())
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset
    33
          ;
285
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
    34
5369
8384e01b6cf8 added nonterminals, setup;
wenzelm
parents: 4891
diff changeset
    35
name : id | string
8384e01b6cf8 added nonterminals, setup;
wenzelm
parents: 4891
diff changeset
    36
     ;
285
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
    37
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset
    38
extension : (section +) 'end' ( () | ml )
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset
    39
          ;
285
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
    40
1080
13c35eb5169b Sections can now be given in any order.
nipkow
parents: 325
diff changeset
    41
section : classes
13c35eb5169b Sections can now be given in any order.
nipkow
parents: 325
diff changeset
    42
        | default
13c35eb5169b Sections can now be given in any order.
nipkow
parents: 325
diff changeset
    43
        | types
13c35eb5169b Sections can now be given in any order.
nipkow
parents: 325
diff changeset
    44
        | arities
5369
8384e01b6cf8 added nonterminals, setup;
wenzelm
parents: 4891
diff changeset
    45
        | nonterminals
1080
13c35eb5169b Sections can now be given in any order.
nipkow
parents: 325
diff changeset
    46
        | consts
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset
    47
        | syntax
1080
13c35eb5169b Sections can now be given in any order.
nipkow
parents: 325
diff changeset
    48
        | trans
13c35eb5169b Sections can now be given in any order.
nipkow
parents: 325
diff changeset
    49
        | defs
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset
    50
        | constdefs
1080
13c35eb5169b Sections can now be given in any order.
nipkow
parents: 325
diff changeset
    51
        | rules
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset
    52
        | axclass
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset
    53
        | instance
1846
763f08fb194f Documentation of oracles and their syntax
paulson
parents: 1650
diff changeset
    54
        | oracle
4543
82a45bdd0e80 several minor updates;
wenzelm
parents: 4317
diff changeset
    55
        | local
82a45bdd0e80 several minor updates;
wenzelm
parents: 4317
diff changeset
    56
        | global
5369
8384e01b6cf8 added nonterminals, setup;
wenzelm
parents: 4891
diff changeset
    57
        | setup
1080
13c35eb5169b Sections can now be given in any order.
nipkow
parents: 325
diff changeset
    58
        ;
13c35eb5169b Sections can now be given in any order.
nipkow
parents: 325
diff changeset
    59
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset
    60
classes : 'classes' ( classDecl + )
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset
    61
        ;
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset
    62
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset
    63
classDecl : (id (() | '<' (id + ',')))
5369
8384e01b6cf8 added nonterminals, setup;
wenzelm
parents: 4891
diff changeset
    64
          ;
285
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
    65
1080
13c35eb5169b Sections can now be given in any order.
nipkow
parents: 325
diff changeset
    66
default : 'default' sort 
285
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
    67
        ;
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
    68
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
    69
sort :  id
3098
a31170b67367 Updated to LaTeX 2e
berghofe
parents: 1846
diff changeset
    70
     | lbrace (id * ',') rbrace
285
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
    71
     ;
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
    72
1080
13c35eb5169b Sections can now be given in any order.
nipkow
parents: 325
diff changeset
    73
types : 'types' ( ( typeDecl ( () | '(' infix ')' ) ) + )
285
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
    74
      ;
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
    75
3215
9e097d5cc246 fixed infix syntax;
wenzelm
parents: 3130
diff changeset
    76
infix : ( 'infixr' | 'infixl' ) (() | string) nat
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset
    77
      ;
1488
b25a747876a4 Added typevarlist
nipkow
parents: 1385
diff changeset
    78
b25a747876a4 Added typevarlist
nipkow
parents: 1385
diff changeset
    79
typeDecl : typevarlist name
1385
63c3d78df538 changed typeDecl
clasohm
parents: 1382
diff changeset
    80
           ( () | '=' ( string | type ) );
63c3d78df538 changed typeDecl
clasohm
parents: 1382
diff changeset
    81
1488
b25a747876a4 Added typevarlist
nipkow
parents: 1385
diff changeset
    82
typevarlist : () | tid | '(' ( tid + ',' ) ')';
b25a747876a4 Added typevarlist
nipkow
parents: 1385
diff changeset
    83
1385
63c3d78df538 changed typeDecl
clasohm
parents: 1382
diff changeset
    84
type : simpleType | '(' type ')' | type '=>' type |
63c3d78df538 changed typeDecl
clasohm
parents: 1382
diff changeset
    85
       '[' ( type + "," ) ']' '=>' type;
63c3d78df538 changed typeDecl
clasohm
parents: 1382
diff changeset
    86
63c3d78df538 changed typeDecl
clasohm
parents: 1382
diff changeset
    87
simpleType: id | ( tid ( () | '::' id ) ) |
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset
    88
            '(' ( type + "," ) ')' id | simpleType id
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset
    89
          ;
285
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
    90
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset
    91
arities : 'arities' ((name + ',') '::' arity +)
285
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
    92
        ;
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
    93
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset
    94
arity : ( () | '(' (sort + ',') ')' ) sort
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset
    95
      ;
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset
    96
5369
8384e01b6cf8 added nonterminals, setup;
wenzelm
parents: 4891
diff changeset
    97
nonterminals : 'nonterminals' (name+)
8384e01b6cf8 added nonterminals, setup;
wenzelm
parents: 4891
diff changeset
    98
             ;
8384e01b6cf8 added nonterminals, setup;
wenzelm
parents: 4891
diff changeset
    99
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset
   100
consts : 'consts' ( mixfixConstDecl + )
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset
   101
       ;
285
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
   102
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset
   103
syntax : 'syntax' (() | mode) ( mixfixConstDecl + );
285
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
   104
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset
   105
mode : '(' name (() | 'output') ')'
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset
   106
     ;
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset
   107
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset
   108
mixfixConstDecl : constDecl (() | ( '(' mixfix ')' ))
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset
   109
                ;
285
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
   110
1382
7e97232c1159 corrected diagrams for type and simpleType
clasohm
parents: 1379
diff changeset
   111
constDecl : ( name + ',') '::' (string | type);
285
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
   112
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
   113
mixfix :  string ( () | ( () | ('[' (nat + ',') ']')) nat )
3215
9e097d5cc246 fixed infix syntax;
wenzelm
parents: 3130
diff changeset
   114
       |  infix
285
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
   115
       | 'binder' string nat ;
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
   116
1080
13c35eb5169b Sections can now be given in any order.
nipkow
parents: 325
diff changeset
   117
trans : 'translations' ( pat ( '==' | '=>' | '<=' ) pat + )
285
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
   118
      ;
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
   119
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
   120
pat : ( () | ( '(' id ')' ) ) string;
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
   121
1080
13c35eb5169b Sections can now be given in any order.
nipkow
parents: 325
diff changeset
   122
rules : 'rules' (( id string ) + )
285
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
   123
      ;
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
   124
1080
13c35eb5169b Sections can now be given in any order.
nipkow
parents: 325
diff changeset
   125
defs : 'defs' (( id string ) + )
13c35eb5169b Sections can now be given in any order.
nipkow
parents: 325
diff changeset
   126
     ;
13c35eb5169b Sections can now be given in any order.
nipkow
parents: 325
diff changeset
   127
4891
19ff46cd2bad fixed constdefs syntax;
wenzelm
parents: 4543
diff changeset
   128
constdefs : 'constdefs' (name '::' (string | type) (() | mixfix) string +)
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset
   129
          ;
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset
   130
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset
   131
axclass : 'axclass' classDecl (() | ( id string ) +)
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset
   132
        ;
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset
   133
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset
   134
instance : 'instance' ( name '<' name | name '::' arity) witness
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset
   135
         ;
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset
   136
5369
8384e01b6cf8 added nonterminals, setup;
wenzelm
parents: 4891
diff changeset
   137
witness : (() | '(' ((string | id | longident) + ',') ')') (() | verbatim)
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset
   138
        ;
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset
   139
4317
7264fa2ff2ec several minor updates;
wenzelm
parents: 3215
diff changeset
   140
oracle : 'oracle' name '=' name
1846
763f08fb194f Documentation of oracles and their syntax
paulson
parents: 1650
diff changeset
   141
       ;
763f08fb194f Documentation of oracles and their syntax
paulson
parents: 1650
diff changeset
   142
4543
82a45bdd0e80 several minor updates;
wenzelm
parents: 4317
diff changeset
   143
local : 'local'
5369
8384e01b6cf8 added nonterminals, setup;
wenzelm
parents: 4891
diff changeset
   144
      ;
4543
82a45bdd0e80 several minor updates;
wenzelm
parents: 4317
diff changeset
   145
82a45bdd0e80 several minor updates;
wenzelm
parents: 4317
diff changeset
   146
global : 'global'
82a45bdd0e80 several minor updates;
wenzelm
parents: 4317
diff changeset
   147
       ;
82a45bdd0e80 several minor updates;
wenzelm
parents: 4317
diff changeset
   148
5369
8384e01b6cf8 added nonterminals, setup;
wenzelm
parents: 4891
diff changeset
   149
setup : 'setup' (id | longident)
8384e01b6cf8 added nonterminals, setup;
wenzelm
parents: 4891
diff changeset
   150
      ;
8384e01b6cf8 added nonterminals, setup;
wenzelm
parents: 4891
diff changeset
   151
1082
1b30e27aca82 Simplified layout a little.
nipkow
parents: 1080
diff changeset
   152
ml : 'ML' text
285
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
   153
   ;
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
   154
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
   155
\end{rail}
5369
8384e01b6cf8 added nonterminals, setup;
wenzelm
parents: 4891
diff changeset
   156
8384e01b6cf8 added nonterminals, setup;
wenzelm
parents: 4891
diff changeset
   157
8384e01b6cf8 added nonterminals, setup;
wenzelm
parents: 4891
diff changeset
   158
%%% Local Variables: 
8384e01b6cf8 added nonterminals, setup;
wenzelm
parents: 4891
diff changeset
   159
%%% mode: latex
8384e01b6cf8 added nonterminals, setup;
wenzelm
parents: 4891
diff changeset
   160
%%% TeX-master: "ref"
8384e01b6cf8 added nonterminals, setup;
wenzelm
parents: 4891
diff changeset
   161
%%% End: