doc-src/Ref/theory-syntax.tex
author obua
Fri, 16 Sep 2005 21:02:15 +0200
changeset 17440 df77edc4f5d0
parent 9695 ec7d7f877712
permissions -rw-r--r--
fixed HOL-light/Isabelle syntax incompatability via more protect_xxx functions
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
9695
ec7d7f877712 proper setup of iman.sty/extra.sty/ttbox.sty;
wenzelm
parents: 6669
diff changeset
     8
Below we present the full syntax of theory definition files as provided by
ec7d7f877712 proper setup of iman.sty/extra.sty/ttbox.sty;
wenzelm
parents: 6669
diff changeset
     9
Pure Isabelle --- object-logics may add their own sections.
ec7d7f877712 proper setup of iman.sty/extra.sty/ttbox.sty;
wenzelm
parents: 6669
diff changeset
    10
\S\ref{sec:ref-defining-theories} explains the meanings of these constructs.
ec7d7f877712 proper setup of iman.sty/extra.sty/ttbox.sty;
wenzelm
parents: 6669
diff changeset
    11
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
6669
5f1ce866c497 locale documentation (from Florian)
paulson
parents: 5369
diff changeset
    55
        | locale
4543
82a45bdd0e80 several minor updates;
wenzelm
parents: 4317
diff changeset
    56
        | local
82a45bdd0e80 several minor updates;
wenzelm
parents: 4317
diff changeset
    57
        | global
5369
8384e01b6cf8 added nonterminals, setup;
wenzelm
parents: 4891
diff changeset
    58
        | setup
1080
13c35eb5169b Sections can now be given in any order.
nipkow
parents: 325
diff changeset
    59
        ;
13c35eb5169b Sections can now be given in any order.
nipkow
parents: 325
diff changeset
    60
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset
    61
classes : 'classes' ( classDecl + )
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset
    62
        ;
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset
    63
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset
    64
classDecl : (id (() | '<' (id + ',')))
5369
8384e01b6cf8 added nonterminals, setup;
wenzelm
parents: 4891
diff changeset
    65
          ;
285
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
    66
1080
13c35eb5169b Sections can now be given in any order.
nipkow
parents: 325
diff changeset
    67
default : 'default' sort 
285
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
    68
        ;
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
    69
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
    70
sort :  id
3098
a31170b67367 Updated to LaTeX 2e
berghofe
parents: 1846
diff changeset
    71
     | lbrace (id * ',') rbrace
285
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
    72
     ;
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
    73
1080
13c35eb5169b Sections can now be given in any order.
nipkow
parents: 325
diff changeset
    74
types : 'types' ( ( typeDecl ( () | '(' infix ')' ) ) + )
285
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
    75
      ;
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
    76
3215
9e097d5cc246 fixed infix syntax;
wenzelm
parents: 3130
diff changeset
    77
infix : ( 'infixr' | 'infixl' ) (() | string) nat
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset
    78
      ;
1488
b25a747876a4 Added typevarlist
nipkow
parents: 1385
diff changeset
    79
b25a747876a4 Added typevarlist
nipkow
parents: 1385
diff changeset
    80
typeDecl : typevarlist name
1385
63c3d78df538 changed typeDecl
clasohm
parents: 1382
diff changeset
    81
           ( () | '=' ( string | type ) );
63c3d78df538 changed typeDecl
clasohm
parents: 1382
diff changeset
    82
1488
b25a747876a4 Added typevarlist
nipkow
parents: 1385
diff changeset
    83
typevarlist : () | tid | '(' ( tid + ',' ) ')';
b25a747876a4 Added typevarlist
nipkow
parents: 1385
diff changeset
    84
1385
63c3d78df538 changed typeDecl
clasohm
parents: 1382
diff changeset
    85
type : simpleType | '(' type ')' | type '=>' type |
63c3d78df538 changed typeDecl
clasohm
parents: 1382
diff changeset
    86
       '[' ( type + "," ) ']' '=>' type;
63c3d78df538 changed typeDecl
clasohm
parents: 1382
diff changeset
    87
63c3d78df538 changed typeDecl
clasohm
parents: 1382
diff changeset
    88
simpleType: id | ( tid ( () | '::' id ) ) |
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset
    89
            '(' ( type + "," ) ')' id | simpleType id
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset
    90
          ;
285
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
    91
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset
    92
arities : 'arities' ((name + ',') '::' arity +)
285
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
    93
        ;
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
    94
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset
    95
arity : ( () | '(' (sort + ',') ')' ) sort
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset
    96
      ;
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset
    97
5369
8384e01b6cf8 added nonterminals, setup;
wenzelm
parents: 4891
diff changeset
    98
nonterminals : 'nonterminals' (name+)
8384e01b6cf8 added nonterminals, setup;
wenzelm
parents: 4891
diff changeset
    99
             ;
8384e01b6cf8 added nonterminals, setup;
wenzelm
parents: 4891
diff changeset
   100
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset
   101
consts : 'consts' ( mixfixConstDecl + )
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset
   102
       ;
285
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
   103
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset
   104
syntax : 'syntax' (() | mode) ( mixfixConstDecl + );
285
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
   105
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset
   106
mode : '(' name (() | 'output') ')'
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset
   107
     ;
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset
   108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset
   109
mixfixConstDecl : constDecl (() | ( '(' mixfix ')' ))
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset
   110
                ;
285
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
   111
1382
7e97232c1159 corrected diagrams for type and simpleType
clasohm
parents: 1379
diff changeset
   112
constDecl : ( name + ',') '::' (string | type);
285
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
   113
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
   114
mixfix :  string ( () | ( () | ('[' (nat + ',') ']')) nat )
3215
9e097d5cc246 fixed infix syntax;
wenzelm
parents: 3130
diff changeset
   115
       |  infix
285
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
   116
       | 'binder' string nat ;
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
   117
1080
13c35eb5169b Sections can now be given in any order.
nipkow
parents: 325
diff changeset
   118
trans : 'translations' ( pat ( '==' | '=>' | '<=' ) pat + )
285
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
   119
      ;
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
   120
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
   121
pat : ( () | ( '(' id ')' ) ) string;
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
   122
1080
13c35eb5169b Sections can now be given in any order.
nipkow
parents: 325
diff changeset
   123
rules : 'rules' (( id string ) + )
285
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
   124
      ;
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
   125
1080
13c35eb5169b Sections can now be given in any order.
nipkow
parents: 325
diff changeset
   126
defs : 'defs' (( id string ) + )
13c35eb5169b Sections can now be given in any order.
nipkow
parents: 325
diff changeset
   127
     ;
13c35eb5169b Sections can now be given in any order.
nipkow
parents: 325
diff changeset
   128
4891
19ff46cd2bad fixed constdefs syntax;
wenzelm
parents: 4543
diff changeset
   129
constdefs : 'constdefs' (name '::' (string | type) (() | mixfix) string +)
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset
   130
          ;
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset
   131
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset
   132
axclass : 'axclass' classDecl (() | ( id string ) +)
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset
   133
        ;
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset
   134
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset
   135
instance : 'instance' ( name '<' name | name '::' arity) witness
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset
   136
         ;
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset
   137
5369
8384e01b6cf8 added nonterminals, setup;
wenzelm
parents: 4891
diff changeset
   138
witness : (() | '(' ((string | id | longident) + ',') ')') (() | verbatim)
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset
   139
        ;
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset
   140
6669
5f1ce866c497 locale documentation (from Florian)
paulson
parents: 5369
diff changeset
   141
locale : 'locale' name '=' ( () | name '+' ) localeBody
5f1ce866c497 locale documentation (from Florian)
paulson
parents: 5369
diff changeset
   142
       ;
5f1ce866c497 locale documentation (from Florian)
paulson
parents: 5369
diff changeset
   143
5f1ce866c497 locale documentation (from Florian)
paulson
parents: 5369
diff changeset
   144
localeBody : localeConsts ( () | localeAsms ) ( () | localeDefs )
5f1ce866c497 locale documentation (from Florian)
paulson
parents: 5369
diff changeset
   145
       ;
5f1ce866c497 locale documentation (from Florian)
paulson
parents: 5369
diff changeset
   146
5f1ce866c497 locale documentation (from Florian)
paulson
parents: 5369
diff changeset
   147
localeConsts: ( 'fixes' ( ( (name '::' ( string | type )) ( () | '(' mixfix ')' ) ) + ) )
5f1ce866c497 locale documentation (from Florian)
paulson
parents: 5369
diff changeset
   148
       ;
5f1ce866c497 locale documentation (from Florian)
paulson
parents: 5369
diff changeset
   149
5f1ce866c497 locale documentation (from Florian)
paulson
parents: 5369
diff changeset
   150
5f1ce866c497 locale documentation (from Florian)
paulson
parents: 5369
diff changeset
   151
localeAsms:    ( 'assumes' ( ( id string ) + ) )
5f1ce866c497 locale documentation (from Florian)
paulson
parents: 5369
diff changeset
   152
       ;
5f1ce866c497 locale documentation (from Florian)
paulson
parents: 5369
diff changeset
   153
5f1ce866c497 locale documentation (from Florian)
paulson
parents: 5369
diff changeset
   154
localeDefs:   ( 'defines' ( ( id string ) +) )
5f1ce866c497 locale documentation (from Florian)
paulson
parents: 5369
diff changeset
   155
       ;
5f1ce866c497 locale documentation (from Florian)
paulson
parents: 5369
diff changeset
   156
4317
7264fa2ff2ec several minor updates;
wenzelm
parents: 3215
diff changeset
   157
oracle : 'oracle' name '=' name
1846
763f08fb194f Documentation of oracles and their syntax
paulson
parents: 1650
diff changeset
   158
       ;
763f08fb194f Documentation of oracles and their syntax
paulson
parents: 1650
diff changeset
   159
4543
82a45bdd0e80 several minor updates;
wenzelm
parents: 4317
diff changeset
   160
local : 'local'
5369
8384e01b6cf8 added nonterminals, setup;
wenzelm
parents: 4891
diff changeset
   161
      ;
4543
82a45bdd0e80 several minor updates;
wenzelm
parents: 4317
diff changeset
   162
82a45bdd0e80 several minor updates;
wenzelm
parents: 4317
diff changeset
   163
global : 'global'
82a45bdd0e80 several minor updates;
wenzelm
parents: 4317
diff changeset
   164
       ;
82a45bdd0e80 several minor updates;
wenzelm
parents: 4317
diff changeset
   165
5369
8384e01b6cf8 added nonterminals, setup;
wenzelm
parents: 4891
diff changeset
   166
setup : 'setup' (id | longident)
8384e01b6cf8 added nonterminals, setup;
wenzelm
parents: 4891
diff changeset
   167
      ;
8384e01b6cf8 added nonterminals, setup;
wenzelm
parents: 4891
diff changeset
   168
1082
1b30e27aca82 Simplified layout a little.
nipkow
parents: 1080
diff changeset
   169
ml : 'ML' text
285
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
   170
   ;
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
   171
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
   172
\end{rail}
5369
8384e01b6cf8 added nonterminals, setup;
wenzelm
parents: 4891
diff changeset
   173
8384e01b6cf8 added nonterminals, setup;
wenzelm
parents: 4891
diff changeset
   174
8384e01b6cf8 added nonterminals, setup;
wenzelm
parents: 4891
diff changeset
   175
%%% Local Variables: 
8384e01b6cf8 added nonterminals, setup;
wenzelm
parents: 4891
diff changeset
   176
%%% mode: latex
8384e01b6cf8 added nonterminals, setup;
wenzelm
parents: 4891
diff changeset
   177
%%% TeX-master: "ref"
8384e01b6cf8 added nonterminals, setup;
wenzelm
parents: 4891
diff changeset
   178
%%% End: