5 begin |
5 begin |
6 |
6 |
7 chapter \<open>Outer syntax --- the theory language \label{ch:outer-syntax}\<close> |
7 chapter \<open>Outer syntax --- the theory language \label{ch:outer-syntax}\<close> |
8 |
8 |
9 text \<open> |
9 text \<open> |
10 The rather generic framework of Isabelle/Isar syntax emerges from |
10 The rather generic framework of Isabelle/Isar syntax emerges from three main |
11 three main syntactic categories: \<^emph>\<open>commands\<close> of the top-level |
11 syntactic categories: \<^emph>\<open>commands\<close> of the top-level Isar engine (covering |
12 Isar engine (covering theory and proof elements), \<^emph>\<open>methods\<close> for |
12 theory and proof elements), \<^emph>\<open>methods\<close> for general goal refinements |
13 general goal refinements (analogous to traditional ``tactics''), and |
13 (analogous to traditional ``tactics''), and \<^emph>\<open>attributes\<close> for operations on |
14 \<^emph>\<open>attributes\<close> for operations on facts (within a certain |
14 facts (within a certain context). Subsequently we give a reference of basic |
15 context). Subsequently we give a reference of basic syntactic |
15 syntactic entities underlying Isabelle/Isar syntax in a bottom-up manner. |
16 entities underlying Isabelle/Isar syntax in a bottom-up manner. |
16 Concrete theory and proof language elements will be introduced later on. |
17 Concrete theory and proof language elements will be introduced later |
|
18 on. |
|
19 |
17 |
20 \<^medskip> |
18 \<^medskip> |
21 In order to get started with writing well-formed |
19 In order to get started with writing well-formed Isabelle/Isar documents, |
22 Isabelle/Isar documents, the most important aspect to be noted is |
20 the most important aspect to be noted is the difference of \<^emph>\<open>inner\<close> versus |
23 the difference of \<^emph>\<open>inner\<close> versus \<^emph>\<open>outer\<close> syntax. Inner |
21 \<^emph>\<open>outer\<close> syntax. Inner syntax is that of Isabelle types and terms of the |
24 syntax is that of Isabelle types and terms of the logic, while outer |
22 logic, while outer syntax is that of Isabelle/Isar theory sources |
25 syntax is that of Isabelle/Isar theory sources (specifications and |
23 (specifications and proofs). As a general rule, inner syntax entities may |
26 proofs). As a general rule, inner syntax entities may occur only as |
24 occur only as \<^emph>\<open>atomic entities\<close> within outer syntax. For example, the |
27 \<^emph>\<open>atomic entities\<close> within outer syntax. For example, the string |
25 string \<^verbatim>\<open>"x + y"\<close> and identifier \<^verbatim>\<open>z\<close> are legal term specifications within a |
28 \<^verbatim>\<open>"x + y"\<close> and identifier \<^verbatim>\<open>z\<close> are legal term |
26 theory, while \<^verbatim>\<open>x + y\<close> without quotes is not. |
29 specifications within a theory, while \<^verbatim>\<open>x + y\<close> without |
27 |
30 quotes is not. |
28 Printed theory documents usually omit quotes to gain readability (this is a |
31 |
29 matter of {\LaTeX} macro setup, say via \<^verbatim>\<open>\isabellestyle\<close>, see also @{cite |
32 Printed theory documents usually omit quotes to gain readability |
30 "isabelle-system"}). Experienced users of Isabelle/Isar may easily |
33 (this is a matter of {\LaTeX} macro setup, say via \<^verbatim>\<open>\isabellestyle\<close>, |
31 reconstruct the lost technical information, while mere readers need not care |
34 see also @{cite "isabelle-system"}). Experienced |
32 about quotes at all. |
35 users of Isabelle/Isar may easily reconstruct the lost technical |
|
36 information, while mere readers need not care about quotes at all. |
|
37 \<close> |
33 \<close> |
38 |
34 |
39 |
35 |
40 section \<open>Commands\<close> |
36 section \<open>Commands\<close> |
41 |
37 |
57 \<close> |
53 \<close> |
58 |
54 |
59 |
55 |
60 subsubsection \<open>Examples\<close> |
56 subsubsection \<open>Examples\<close> |
61 |
57 |
62 text \<open>Some common diagnostic commands are retrieved like this |
58 text \<open> |
63 (according to usual naming conventions):\<close> |
59 Some common diagnostic commands are retrieved like this (according to usual |
|
60 naming conventions): |
|
61 \<close> |
64 |
62 |
65 help "print" |
63 help "print" |
66 help "find" |
64 help "find" |
67 |
65 |
68 |
66 |
69 section \<open>Lexical matters \label{sec:outer-lex}\<close> |
67 section \<open>Lexical matters \label{sec:outer-lex}\<close> |
70 |
68 |
71 text \<open>The outer lexical syntax consists of three main categories of |
69 text \<open> |
72 syntax tokens: |
70 The outer lexical syntax consists of three main categories of syntax tokens: |
73 |
71 |
74 \<^enum> \<^emph>\<open>major keywords\<close> --- the command names that are available |
72 \<^enum> \<^emph>\<open>major keywords\<close> --- the command names that are available |
75 in the present logic session; |
73 in the present logic session; |
76 |
74 |
77 \<^enum> \<^emph>\<open>minor keywords\<close> --- additional literal tokens required |
75 \<^enum> \<^emph>\<open>minor keywords\<close> --- additional literal tokens required |
78 by the syntax of commands; |
76 by the syntax of commands; |
79 |
77 |
80 \<^enum> \<^emph>\<open>named tokens\<close> --- various categories of identifiers etc. |
78 \<^enum> \<^emph>\<open>named tokens\<close> --- various categories of identifiers etc. |
81 |
79 |
82 |
80 Major keywords and minor keywords are guaranteed to be disjoint. This helps |
83 Major keywords and minor keywords are guaranteed to be disjoint. |
81 user-interfaces to determine the overall structure of a theory text, without |
84 This helps user-interfaces to determine the overall structure of a |
82 knowing the full details of command syntax. Internally, there is some |
85 theory text, without knowing the full details of command syntax. |
83 additional information about the kind of major keywords, which approximates |
86 Internally, there is some additional information about the kind of |
84 the command type (theory command, proof command etc.). |
87 major keywords, which approximates the command type (theory command, |
85 |
88 proof command etc.). |
86 Keywords override named tokens. For example, the presence of a command |
89 |
87 called \<^verbatim>\<open>term\<close> inhibits the identifier \<^verbatim>\<open>term\<close>, but the string \<^verbatim>\<open>"term"\<close> can |
90 Keywords override named tokens. For example, the presence of a |
88 be used instead. By convention, the outer syntax always allows quoted |
91 command called \<^verbatim>\<open>term\<close> inhibits the identifier \<^verbatim>\<open>term\<close>, but the |
89 strings in addition to identifiers, wherever a named entity is expected. |
92 string \<^verbatim>\<open>"term"\<close> can be used instead. |
90 |
93 By convention, the outer syntax always allows quoted strings in |
91 When tokenizing a given input sequence, the lexer repeatedly takes the |
94 addition to identifiers, wherever a named entity is expected. |
92 longest prefix of the input that forms a valid token. Spaces, tabs, newlines |
95 |
93 and formfeeds between tokens serve as explicit separators. |
96 When tokenizing a given input sequence, the lexer repeatedly takes |
|
97 the longest prefix of the input that forms a valid token. Spaces, |
|
98 tabs, newlines and formfeeds between tokens serve as explicit |
|
99 separators. |
|
100 |
94 |
101 \<^medskip> |
95 \<^medskip> |
102 The categories for named tokens are defined once and for all as follows. |
96 The categories for named tokens are defined once and for all as follows. |
103 |
97 |
104 \begin{center} |
98 \begin{center} |
132 & & \<^verbatim>\<open>\<Lambda>\<close>~~\<open>|\<close>~~\<^verbatim>\<open>\<Xi>\<close>~~\<open>|\<close>~~\<^verbatim>\<open>\<Pi>\<close>~~\<open>|\<close>~~\<^verbatim>\<open>\<Sigma>\<close>~~\<open>|\<close> \\ |
126 & & \<^verbatim>\<open>\<Lambda>\<close>~~\<open>|\<close>~~\<^verbatim>\<open>\<Xi>\<close>~~\<open>|\<close>~~\<^verbatim>\<open>\<Pi>\<close>~~\<open>|\<close>~~\<^verbatim>\<open>\<Sigma>\<close>~~\<open>|\<close> \\ |
133 & & \<^verbatim>\<open>\<Upsilon>\<close>~~\<open>|\<close>~~\<^verbatim>\<open>\<Phi>\<close>~~\<open>|\<close>~~\<^verbatim>\<open>\<Psi>\<close>~~\<open>|\<close>~~\<^verbatim>\<open>\<Omega>\<close> \\ |
127 & & \<^verbatim>\<open>\<Upsilon>\<close>~~\<open>|\<close>~~\<^verbatim>\<open>\<Phi>\<close>~~\<open>|\<close>~~\<^verbatim>\<open>\<Psi>\<close>~~\<open>|\<close>~~\<^verbatim>\<open>\<Omega>\<close> \\ |
134 \end{supertabular} |
128 \end{supertabular} |
135 \end{center} |
129 \end{center} |
136 |
130 |
137 A @{syntax_ref var} or @{syntax_ref typevar} describes an unknown, |
131 A @{syntax_ref var} or @{syntax_ref typevar} describes an unknown, which is |
138 which is internally a pair of base name and index (ML type @{ML_type |
132 internally a pair of base name and index (ML type @{ML_type indexname}). |
139 indexname}). These components are either separated by a dot as in |
133 These components are either separated by a dot as in \<open>?x.1\<close> or \<open>?x7.3\<close> or |
140 \<open>?x.1\<close> or \<open>?x7.3\<close> or run together as in \<open>?x1\<close>. The latter form is possible |
134 run together as in \<open>?x1\<close>. The latter form is possible if the base name does |
141 if the base name does not end with digits. If the index is 0, it may be |
135 not end with digits. If the index is 0, it may be dropped altogether: \<open>?x\<close> |
142 dropped altogether: \<open>?x\<close> and \<open>?x0\<close> and \<open>?x.0\<close> all refer to the |
136 and \<open>?x0\<close> and \<open>?x.0\<close> all refer to the same unknown, with basename \<open>x\<close> and |
143 same unknown, with basename \<open>x\<close> and index 0. |
137 index 0. |
144 |
138 |
145 The syntax of @{syntax_ref string} admits any characters, including |
139 The syntax of @{syntax_ref string} admits any characters, including |
146 newlines; ``\<^verbatim>\<open>"\<close>'' (double-quote) and ``\<^verbatim>\<open>\\<close>'' |
140 newlines; ``\<^verbatim>\<open>"\<close>'' (double-quote) and ``\<^verbatim>\<open>\\<close>'' (backslash) need to be |
147 (backslash) need to be escaped by a backslash; arbitrary |
141 escaped by a backslash; arbitrary character codes may be specified as |
148 character codes may be specified as ``\<^verbatim>\<open>\\<close>\<open>ddd\<close>'', |
142 ``\<^verbatim>\<open>\\<close>\<open>ddd\<close>'', with three decimal digits. Alternative strings according to |
149 with three decimal digits. Alternative strings according to |
143 @{syntax_ref altstring} are analogous, using single back-quotes instead. |
150 @{syntax_ref altstring} are analogous, using single back-quotes |
|
151 instead. |
|
152 |
144 |
153 The body of @{syntax_ref verbatim} may consist of any text not containing |
145 The body of @{syntax_ref verbatim} may consist of any text not containing |
154 ``\<^verbatim>\<open>*}\<close>''; this allows to include quotes without further |
146 ``\<^verbatim>\<open>*}\<close>''; this allows to include quotes without further escapes, but there |
155 escapes, but there is no way to escape ``\<^verbatim>\<open>*}\<close>''. Cartouches |
147 is no way to escape ``\<^verbatim>\<open>*}\<close>''. Cartouches do not have this limitation. |
156 do not have this limitation. |
148 |
157 |
149 A @{syntax_ref cartouche} consists of arbitrary text, with properly balanced |
158 A @{syntax_ref cartouche} consists of arbitrary text, with properly |
150 blocks of ``@{verbatim "\<open>"}~\<open>\<dots>\<close>~@{verbatim "\<close>"}''. Note that the rendering |
159 balanced blocks of ``@{verbatim "\<open>"}~\<open>\<dots>\<close>~@{verbatim |
151 of cartouche delimiters is usually like this: ``\<open>\<open> \<dots> \<close>\<close>''. |
160 "\<close>"}''. Note that the rendering of cartouche delimiters is |
152 |
161 usually like this: ``\<open>\<open> \<dots> \<close>\<close>''. |
153 Source comments take the form \<^verbatim>\<open>(*\<close>~\<open>\<dots>\<close>~\<^verbatim>\<open>*)\<close> and may be nested, although |
162 |
154 the user-interface might prevent this. Note that this form indicates source |
163 Source comments take the form \<^verbatim>\<open>(*\<close>~\<open>\<dots>\<close>~\<^verbatim>\<open>*)\<close> and may be nested, although the user-interface |
155 comments only, which are stripped after lexical analysis of the input. The |
164 might prevent this. Note that this form indicates source comments |
156 Isar syntax also provides proper \<^emph>\<open>document comments\<close> that are considered as |
165 only, which are stripped after lexical analysis of the input. The |
157 part of the text (see \secref{sec:comments}). |
166 Isar syntax also provides proper \<^emph>\<open>document comments\<close> that are |
158 |
167 considered as part of the text (see \secref{sec:comments}). |
159 Common mathematical symbols such as \<open>\<forall>\<close> are represented in Isabelle as \<^verbatim>\<open>\<forall>\<close>. |
168 |
160 There are infinitely many Isabelle symbols like this, although proper |
169 Common mathematical symbols such as \<open>\<forall>\<close> are represented in |
161 presentation is left to front-end tools such as {\LaTeX} or Isabelle/jEdit. |
170 Isabelle as \<^verbatim>\<open>\<forall>\<close>. There are infinitely many Isabelle |
162 A list of predefined Isabelle symbols that work well with these tools is |
171 symbols like this, although proper presentation is left to front-end |
163 given in \appref{app:symbols}. Note that \<^verbatim>\<open>\<lambda>\<close> does not belong to the |
172 tools such as {\LaTeX} or Isabelle/jEdit. A list of |
164 \<open>letter\<close> category, since it is already used differently in the Pure term |
173 predefined Isabelle symbols that work well with these tools is given |
165 language. |
174 in \appref{app:symbols}. Note that \<^verbatim>\<open>\<lambda>\<close> does not belong |
166 \<close> |
175 to the \<open>letter\<close> category, since it is already used differently |
|
176 in the Pure term language.\<close> |
|
177 |
167 |
178 |
168 |
179 section \<open>Common syntax entities\<close> |
169 section \<open>Common syntax entities\<close> |
180 |
170 |
181 text \<open> |
171 text \<open> |
182 We now introduce several basic syntactic entities, such as names, |
172 We now introduce several basic syntactic entities, such as names, terms, and |
183 terms, and theorem specifications, which are factored out of the |
173 theorem specifications, which are factored out of the actual Isar language |
184 actual Isar language elements to be described later. |
174 elements to be described later. |
185 \<close> |
175 \<close> |
186 |
176 |
187 |
177 |
188 subsection \<open>Names\<close> |
178 subsection \<open>Names\<close> |
189 |
179 |
190 text \<open>Entity @{syntax name} usually refers to any name of types, |
180 text \<open> |
191 constants, theorems etc.\ that are to be \<^emph>\<open>declared\<close> or |
181 Entity @{syntax name} usually refers to any name of types, constants, |
192 \<^emph>\<open>defined\<close> (so qualified identifiers are excluded here). Quoted |
182 theorems etc.\ that are to be \<^emph>\<open>declared\<close> or \<^emph>\<open>defined\<close> (so qualified |
193 strings provide an escape for non-identifier names or those ruled |
183 identifiers are excluded here). Quoted strings provide an escape for |
194 out by outer syntax keywords (e.g.\ quoted \<^verbatim>\<open>"let"\<close>). |
184 non-identifier names or those ruled out by outer syntax keywords (e.g.\ |
195 Already existing objects are usually referenced by @{syntax |
185 quoted \<^verbatim>\<open>"let"\<close>). Already existing objects are usually referenced by |
196 nameref}. |
186 @{syntax nameref}. |
197 |
187 |
198 @{rail \<open> |
188 @{rail \<open> |
199 @{syntax_def name}: @{syntax ident} | @{syntax symident} | |
189 @{syntax_def name}: @{syntax ident} | @{syntax symident} | |
200 @{syntax string} | @{syntax nat} |
190 @{syntax string} | @{syntax nat} |
201 ; |
191 ; |
261 |
251 |
262 |
252 |
263 subsection \<open>Types and terms \label{sec:types-terms}\<close> |
253 subsection \<open>Types and terms \label{sec:types-terms}\<close> |
264 |
254 |
265 text \<open> |
255 text \<open> |
266 The actual inner Isabelle syntax, that of types and terms of the |
256 The actual inner Isabelle syntax, that of types and terms of the logic, is |
267 logic, is far too sophisticated in order to be modelled explicitly |
257 far too sophisticated in order to be modelled explicitly at the outer theory |
268 at the outer theory level. Basically, any such entity has to be |
258 level. Basically, any such entity has to be quoted to turn it into a single |
269 quoted to turn it into a single token (the parsing and type-checking |
259 token (the parsing and type-checking is performed internally later). For |
270 is performed internally later). For convenience, a slightly more |
260 convenience, a slightly more liberal convention is adopted: quotes may be |
271 liberal convention is adopted: quotes may be omitted for any type or |
261 omitted for any type or term that is already atomic at the outer level. For |
272 term that is already atomic at the outer level. For example, one |
262 example, one may just write \<^verbatim>\<open>x\<close> instead of quoted \<^verbatim>\<open>"x"\<close>. Note that |
273 may just write \<^verbatim>\<open>x\<close> instead of quoted \<^verbatim>\<open>"x"\<close>. |
263 symbolic identifiers (e.g.\ \<^verbatim>\<open>++\<close> or \<open>\<forall>\<close> are available as well, provided |
274 Note that symbolic identifiers (e.g.\ \<^verbatim>\<open>++\<close> or \<open>\<forall>\<close> are available as well, |
264 these have not been superseded by commands or other keywords already (such |
275 provided these have not been superseded |
265 as \<^verbatim>\<open>=\<close> or \<^verbatim>\<open>+\<close>). |
276 by commands or other keywords already (such as \<^verbatim>\<open>=\<close> or |
|
277 \<^verbatim>\<open>+\<close>). |
|
278 |
266 |
279 @{rail \<open> |
267 @{rail \<open> |
280 @{syntax_def type}: @{syntax nameref} | @{syntax typefree} | |
268 @{syntax_def type}: @{syntax nameref} | @{syntax typefree} | |
281 @{syntax typevar} |
269 @{syntax typevar} |
282 ; |
270 ; |
292 @{syntax_def inst}: '_' | @{syntax term} |
280 @{syntax_def inst}: '_' | @{syntax term} |
293 ; |
281 ; |
294 @{syntax_def insts}: (@{syntax inst} *) |
282 @{syntax_def insts}: (@{syntax inst} *) |
295 \<close>} |
283 \<close>} |
296 |
284 |
297 Named instantiations are specified as pairs of assignments \<open>v = |
285 Named instantiations are specified as pairs of assignments \<open>v = t\<close>, which |
298 t\<close>, which refer to schematic variables in some theorem that is |
286 refer to schematic variables in some theorem that is instantiated. Both type |
299 instantiated. Both type and terms instantiations are admitted, and |
287 and terms instantiations are admitted, and distinguished by the usual syntax |
300 distinguished by the usual syntax of variable names. |
288 of variable names. |
301 |
289 |
302 @{rail \<open> |
290 @{rail \<open> |
303 @{syntax_def named_inst}: variable '=' (type | term) |
291 @{syntax_def named_inst}: variable '=' (type | term) |
304 ; |
292 ; |
305 @{syntax_def named_insts}: (named_inst @'and' +) |
293 @{syntax_def named_insts}: (named_inst @'and' +) |
306 ; |
294 ; |
307 variable: @{syntax name} | @{syntax var} | @{syntax typefree} | @{syntax typevar} |
295 variable: @{syntax name} | @{syntax var} | @{syntax typefree} | @{syntax typevar} |
308 \<close>} |
296 \<close>} |
309 |
297 |
310 Type declarations and definitions usually refer to @{syntax |
298 Type declarations and definitions usually refer to @{syntax typespec} on the |
311 typespec} on the left-hand side. This models basic type constructor |
299 left-hand side. This models basic type constructor application at the outer |
312 application at the outer syntax level. Note that only plain postfix |
300 syntax level. Note that only plain postfix notation is available here, but |
313 notation is available here, but no infixes. |
301 no infixes. |
314 |
302 |
315 @{rail \<open> |
303 @{rail \<open> |
316 @{syntax_def typespec}: |
304 @{syntax_def typespec}: |
317 (() | @{syntax typefree} | '(' ( @{syntax typefree} + ',' ) ')') @{syntax name} |
305 (() | @{syntax typefree} | '(' ( @{syntax typefree} + ',' ) ')') @{syntax name} |
318 ; |
306 ; |
323 \<close> |
311 \<close> |
324 |
312 |
325 |
313 |
326 subsection \<open>Term patterns and declarations \label{sec:term-decls}\<close> |
314 subsection \<open>Term patterns and declarations \label{sec:term-decls}\<close> |
327 |
315 |
328 text \<open>Wherever explicit propositions (or term fragments) occur in a |
316 text \<open> |
329 proof text, casual binding of schematic term variables may be given |
317 Wherever explicit propositions (or term fragments) occur in a proof text, |
330 specified via patterns of the form ``\<open>(\<IS> p\<^sub>1 \<dots> p\<^sub>n)\<close>''. |
318 casual binding of schematic term variables may be given specified via |
331 This works both for @{syntax term} and @{syntax prop}. |
319 patterns of the form ``\<open>(\<IS> p\<^sub>1 \<dots> p\<^sub>n)\<close>''. This works both for @{syntax |
|
320 term} and @{syntax prop}. |
332 |
321 |
333 @{rail \<open> |
322 @{rail \<open> |
334 @{syntax_def term_pat}: '(' (@'is' @{syntax term} +) ')' |
323 @{syntax_def term_pat}: '(' (@'is' @{syntax term} +) ')' |
335 ; |
324 ; |
336 @{syntax_def prop_pat}: '(' (@'is' @{syntax prop} +) ')' |
325 @{syntax_def prop_pat}: '(' (@'is' @{syntax prop} +) ')' |
337 \<close>} |
326 \<close>} |
338 |
327 |
339 \<^medskip> |
328 \<^medskip> |
340 Declarations of local variables \<open>x :: \<tau>\<close> and |
329 Declarations of local variables \<open>x :: \<tau>\<close> and logical propositions \<open>a : \<phi>\<close> |
341 logical propositions \<open>a : \<phi>\<close> represent different views on |
330 represent different views on the same principle of introducing a local |
342 the same principle of introducing a local scope. In practice, one |
331 scope. In practice, one may usually omit the typing of @{syntax vars} (due |
343 may usually omit the typing of @{syntax vars} (due to |
332 to type-inference), and the naming of propositions (due to implicit |
344 type-inference), and the naming of propositions (due to implicit |
333 references of current facts). In any case, Isar proof elements usually admit |
345 references of current facts). In any case, Isar proof elements |
334 to introduce multiple such items simultaneously. |
346 usually admit to introduce multiple such items simultaneously. |
|
347 |
335 |
348 @{rail \<open> |
336 @{rail \<open> |
349 @{syntax_def vars}: (@{syntax name} +) ('::' @{syntax type})? |
337 @{syntax_def vars}: (@{syntax name} +) ('::' @{syntax type})? |
350 ; |
338 ; |
351 @{syntax_def props}: @{syntax thmdecl}? (@{syntax prop} @{syntax prop_pat}? +) |
339 @{syntax_def props}: @{syntax thmdecl}? (@{syntax prop} @{syntax prop_pat}? +) |
352 ; |
340 ; |
353 @{syntax_def props'}: (@{syntax prop} @{syntax prop_pat}? +) |
341 @{syntax_def props'}: (@{syntax prop} @{syntax prop_pat}? +) |
354 \<close>} |
342 \<close>} |
355 |
343 |
356 The treatment of multiple declarations corresponds to the |
344 The treatment of multiple declarations corresponds to the complementary |
357 complementary focus of @{syntax vars} versus @{syntax props}. In |
345 focus of @{syntax vars} versus @{syntax props}. In ``\<open>x\<^sub>1 \<dots> x\<^sub>n :: \<tau>\<close>'' the |
358 ``\<open>x\<^sub>1 \<dots> x\<^sub>n :: \<tau>\<close>'' the typing refers to all variables, while |
346 typing refers to all variables, while in \<open>a: \<phi>\<^sub>1 \<dots> \<phi>\<^sub>n\<close> the naming refers to |
359 in \<open>a: \<phi>\<^sub>1 \<dots> \<phi>\<^sub>n\<close> the naming refers to all propositions |
347 all propositions collectively. Isar language elements that refer to @{syntax |
360 collectively. Isar language elements that refer to @{syntax vars} |
348 vars} or @{syntax props} typically admit separate typings or namings via |
361 or @{syntax props} typically admit separate typings or namings via |
349 another level of iteration, with explicit @{keyword_ref "and"} separators; |
362 another level of iteration, with explicit @{keyword_ref "and"} |
350 e.g.\ see @{command "fix"} and @{command "assume"} in |
363 separators; e.g.\ see @{command "fix"} and @{command "assume"} in |
|
364 \secref{sec:proof-context}. |
351 \secref{sec:proof-context}. |
365 |
352 |
366 @{rail \<open> |
353 @{rail \<open> |
367 @{syntax_def "fixes"}: |
354 @{syntax_def "fixes"}: |
368 ((@{syntax name} ('::' @{syntax type})? @{syntax mixfix}? | @{syntax vars}) + @'and') |
355 ((@{syntax name} ('::' @{syntax type})? @{syntax mixfix}? | @{syntax vars}) + @'and') |
370 @{syntax_def "for_fixes"}: (@'for' @{syntax "fixes"})? |
357 @{syntax_def "for_fixes"}: (@'for' @{syntax "fixes"})? |
371 \<close>} |
358 \<close>} |
372 |
359 |
373 The category @{syntax "fixes"} is a richer variant of @{syntax vars}: it |
360 The category @{syntax "fixes"} is a richer variant of @{syntax vars}: it |
374 admits specification of mixfix syntax for the entities that are introduced |
361 admits specification of mixfix syntax for the entities that are introduced |
375 into the context. An optional suffix ``@{keyword "for"}~\<open>fixes\<close>'' |
362 into the context. An optional suffix ``@{keyword "for"}~\<open>fixes\<close>'' is |
376 is admitted in many situations to indicate a so-called ``eigen-context'' |
363 admitted in many situations to indicate a so-called ``eigen-context'' of a |
377 of a formal element: the result will be exported and thus generalized over |
364 formal element: the result will be exported and thus generalized over the |
378 the given variables.\<close> |
365 given variables. |
|
366 \<close> |
379 |
367 |
380 |
368 |
381 subsection \<open>Attributes and theorems \label{sec:syn-att}\<close> |
369 subsection \<open>Attributes and theorems \label{sec:syn-att}\<close> |
382 |
370 |
383 text \<open>Attributes have their own ``semi-inner'' syntax, in the sense |
371 text \<open> |
384 that input conforming to @{syntax args} below is parsed by the |
372 Attributes have their own ``semi-inner'' syntax, in the sense that input |
385 attribute a second time. The attribute argument specifications may |
373 conforming to @{syntax args} below is parsed by the attribute a second time. |
386 be any sequence of atomic entities (identifiers, strings etc.), or |
374 The attribute argument specifications may be any sequence of atomic entities |
387 properly bracketed argument lists. Below @{syntax atom} refers to |
375 (identifiers, strings etc.), or properly bracketed argument lists. Below |
388 any atomic entity, including any @{syntax keyword} conforming to |
376 @{syntax atom} refers to any atomic entity, including any @{syntax keyword} |
389 @{syntax symident}. |
377 conforming to @{syntax symident}. |
390 |
378 |
391 @{rail \<open> |
379 @{rail \<open> |
392 @{syntax_def atom}: @{syntax nameref} | @{syntax typefree} | |
380 @{syntax_def atom}: @{syntax nameref} | @{syntax typefree} | |
393 @{syntax typevar} | @{syntax var} | @{syntax nat} | @{syntax float} | |
381 @{syntax typevar} | @{syntax var} | @{syntax nat} | @{syntax float} | |
394 @{syntax keyword} | @{syntax cartouche} |
382 @{syntax keyword} | @{syntax cartouche} |
398 @{syntax_def args}: arg * |
386 @{syntax_def args}: arg * |
399 ; |
387 ; |
400 @{syntax_def attributes}: '[' (@{syntax nameref} @{syntax args} * ',') ']' |
388 @{syntax_def attributes}: '[' (@{syntax nameref} @{syntax args} * ',') ']' |
401 \<close>} |
389 \<close>} |
402 |
390 |
403 Theorem specifications come in several flavors: @{syntax axmdecl} |
391 Theorem specifications come in several flavors: @{syntax axmdecl} and |
404 and @{syntax thmdecl} usually refer to axioms, assumptions or |
392 @{syntax thmdecl} usually refer to axioms, assumptions or results of goal |
405 results of goal statements, while @{syntax thmdef} collects lists of |
393 statements, while @{syntax thmdef} collects lists of existing theorems. |
406 existing theorems. Existing theorems are given by @{syntax thmref} |
394 Existing theorems are given by @{syntax thmref} and @{syntax thmrefs}, the |
407 and @{syntax thmrefs}, the former requires an actual singleton |
395 former requires an actual singleton result. |
408 result. |
|
409 |
396 |
410 There are three forms of theorem references: |
397 There are three forms of theorem references: |
411 |
398 |
412 \<^enum> named facts \<open>a\<close>, |
399 \<^enum> named facts \<open>a\<close>, |
413 |
400 |
414 \<^enum> selections from named facts \<open>a(i)\<close> or \<open>a(j - k)\<close>, |
401 \<^enum> selections from named facts \<open>a(i)\<close> or \<open>a(j - k)\<close>, |
415 |
402 |
416 \<^enum> literal fact propositions using token syntax @{syntax_ref altstring} |
403 \<^enum> literal fact propositions using token syntax @{syntax_ref altstring} |
417 \<^verbatim>\<open>`\<close>\<open>\<phi>\<close>\<^verbatim>\<open>`\<close> or @{syntax_ref cartouche} |
404 \<^verbatim>\<open>`\<close>\<open>\<phi>\<close>\<^verbatim>\<open>`\<close> or @{syntax_ref cartouche} |
418 \<open>\<open>\<phi>\<close>\<close> (see also method @{method_ref fact}). |
405 \<open>\<open>\<phi>\<close>\<close> (see also method @{method_ref fact}). |
419 |
406 |
420 |
407 Any kind of theorem specification may include lists of attributes both on |
421 Any kind of theorem specification may include lists of attributes |
408 the left and right hand sides; attributes are applied to any immediately |
422 both on the left and right hand sides; attributes are applied to any |
409 preceding fact. If names are omitted, the theorems are not stored within the |
423 immediately preceding fact. If names are omitted, the theorems are |
410 theorem database of the theory or proof context, but any given attributes |
424 not stored within the theorem database of the theory or proof |
411 are applied nonetheless. |
425 context, but any given attributes are applied nonetheless. |
412 |
426 |
413 An extra pair of brackets around attributes (like ``\<open>[[simproc a]]\<close>'') |
427 An extra pair of brackets around attributes (like ``\<open>[[simproc a]]\<close>'') abbreviates a theorem reference involving an |
414 abbreviates a theorem reference involving an internal dummy fact, which will |
428 internal dummy fact, which will be ignored later on. So only the |
415 be ignored later on. So only the effect of the attribute on the background |
429 effect of the attribute on the background context will persist. |
416 context will persist. This form of in-place declarations is particularly |
430 This form of in-place declarations is particularly useful with |
417 useful with commands like @{command "declare"} and @{command "using"}. |
431 commands like @{command "declare"} and @{command "using"}. |
|
432 |
418 |
433 @{rail \<open> |
419 @{rail \<open> |
434 @{syntax_def axmdecl}: @{syntax name} @{syntax attributes}? ':' |
420 @{syntax_def axmdecl}: @{syntax name} @{syntax attributes}? ':' |
435 ; |
421 ; |
436 @{syntax_def thmbind}: |
422 @{syntax_def thmbind}: |
490 @@{command thm_deps} @{syntax thmrefs} |
476 @@{command thm_deps} @{syntax thmrefs} |
491 ; |
477 ; |
492 @@{command unused_thms} ((@{syntax name} +) '-' (@{syntax name} * ))? |
478 @@{command unused_thms} ((@{syntax name} +) '-' (@{syntax name} * ))? |
493 \<close>} |
479 \<close>} |
494 |
480 |
495 These commands print certain parts of the theory and proof context. |
481 These commands print certain parts of the theory and proof context. Note |
496 Note that there are some further ones available, such as for the set |
482 that there are some further ones available, such as for the set of rules |
497 of rules declared for simplifications. |
483 declared for simplifications. |
498 |
484 |
499 \<^descr> @{command "print_theory"} prints the main logical content of the |
485 \<^descr> @{command "print_theory"} prints the main logical content of the |
500 background theory; the ``\<open>!\<close>'' option indicates extra verbosity. |
486 background theory; the ``\<open>!\<close>'' option indicates extra verbosity. |
501 |
487 |
502 \<^descr> @{command "print_definitions"} prints dependencies of definitional |
488 \<^descr> @{command "print_definitions"} prints dependencies of definitional |
503 specifications within the background theory, which may be constants |
489 specifications within the background theory, which may be constants |
504 \secref{sec:consts} or types (\secref{sec:types-pure}, |
490 \secref{sec:consts} or types (\secref{sec:types-pure}, |
505 \secref{sec:hol-typedef}); the ``\<open>!\<close>'' option indicates extra |
491 \secref{sec:hol-typedef}); the ``\<open>!\<close>'' option indicates extra verbosity. |
|
492 |
|
493 \<^descr> @{command "print_methods"} prints all proof methods available in the |
|
494 current theory context; the ``\<open>!\<close>'' option indicates extra verbosity. |
|
495 |
|
496 \<^descr> @{command "print_attributes"} prints all attributes available in the |
|
497 current theory context; the ``\<open>!\<close>'' option indicates extra verbosity. |
|
498 |
|
499 \<^descr> @{command "print_theorems"} prints theorems of the background theory |
|
500 resulting from the last command; the ``\<open>!\<close>'' option indicates extra |
506 verbosity. |
501 verbosity. |
507 |
502 |
508 \<^descr> @{command "print_methods"} prints all proof methods available in the |
503 \<^descr> @{command "print_facts"} prints all local facts of the current context, |
509 current theory context; the ``\<open>!\<close>'' option indicates extra |
504 both named and unnamed ones; the ``\<open>!\<close>'' option indicates extra verbosity. |
510 verbosity. |
505 |
511 |
506 \<^descr> @{command "print_term_bindings"} prints all term bindings that are present |
512 \<^descr> @{command "print_attributes"} prints all attributes available in the |
507 in the context. |
513 current theory context; the ``\<open>!\<close>'' option indicates extra |
508 |
514 verbosity. |
509 \<^descr> @{command "find_theorems"}~\<open>criteria\<close> retrieves facts from the theory or |
515 |
510 proof context matching all of given search criteria. The criterion \<open>name: p\<close> |
516 \<^descr> @{command "print_theorems"} prints theorems of the background theory |
511 selects all theorems whose fully qualified name matches pattern \<open>p\<close>, which |
517 resulting from the last command; the ``\<open>!\<close>'' option indicates |
512 may contain ``\<open>*\<close>'' wildcards. The criteria \<open>intro\<close>, \<open>elim\<close>, and \<open>dest\<close> |
518 extra verbosity. |
513 select theorems that match the current goal as introduction, elimination or |
519 |
514 destruction rules, respectively. The criterion \<open>solves\<close> returns all rules |
520 \<^descr> @{command "print_facts"} prints all local facts of the current |
515 that would directly solve the current goal. The criterion \<open>simp: t\<close> selects |
521 context, both named and unnamed ones; the ``\<open>!\<close>'' option indicates |
516 all rewrite rules whose left-hand side matches the given term. The criterion |
522 extra verbosity. |
517 term \<open>t\<close> selects all theorems that contain the pattern \<open>t\<close> -- as usual, |
523 |
518 patterns may contain occurrences of the dummy ``\<open>_\<close>'', schematic variables, |
524 \<^descr> @{command "print_term_bindings"} prints all term bindings that |
519 and type constraints. |
525 are present in the context. |
520 |
526 |
521 Criteria can be preceded by ``\<open>-\<close>'' to select theorems that do \<^emph>\<open>not\<close> match. |
527 \<^descr> @{command "find_theorems"}~\<open>criteria\<close> retrieves facts |
522 Note that giving the empty list of criteria yields \<^emph>\<open>all\<close> currently known |
528 from the theory or proof context matching all of given search |
523 facts. An optional limit for the number of printed facts may be given; the |
529 criteria. The criterion \<open>name: p\<close> selects all theorems |
524 default is 40. By default, duplicates are removed from the search result. |
530 whose fully qualified name matches pattern \<open>p\<close>, which may |
525 Use \<open>with_dups\<close> to display duplicates. |
531 contain ``\<open>*\<close>'' wildcards. The criteria \<open>intro\<close>, |
526 |
532 \<open>elim\<close>, and \<open>dest\<close> select theorems that match the |
527 \<^descr> @{command "find_consts"}~\<open>criteria\<close> prints all constants whose type meets |
533 current goal as introduction, elimination or destruction rules, |
528 all of the given criteria. The criterion \<open>strict: ty\<close> is met by any type |
534 respectively. The criterion \<open>solves\<close> returns all rules |
529 that matches the type pattern \<open>ty\<close>. Patterns may contain both the dummy type |
535 that would directly solve the current goal. The criterion |
530 ``\<open>_\<close>'' and sort constraints. The criterion \<open>ty\<close> is similar, but it also |
536 \<open>simp: t\<close> selects all rewrite rules whose left-hand side |
531 matches against subtypes. The criterion \<open>name: p\<close> and the prefix ``\<open>-\<close>'' |
537 matches the given term. The criterion term \<open>t\<close> selects all |
532 function as described for @{command "find_theorems"}. |
538 theorems that contain the pattern \<open>t\<close> -- as usual, patterns |
533 |
539 may contain occurrences of the dummy ``\<open>_\<close>'', schematic |
534 \<^descr> @{command "thm_deps"}~\<open>a\<^sub>1 \<dots> a\<^sub>n\<close> visualizes dependencies of facts, using |
540 variables, and type constraints. |
535 Isabelle's graph browser tool (see also @{cite "isabelle-system"}). |
541 |
536 |
542 Criteria can be preceded by ``\<open>-\<close>'' to select theorems that |
537 \<^descr> @{command "unused_thms"}~\<open>A\<^sub>1 \<dots> A\<^sub>m - B\<^sub>1 \<dots> B\<^sub>n\<close> displays all theorems |
543 do \<^emph>\<open>not\<close> match. Note that giving the empty list of criteria |
538 that are proved in theories \<open>B\<^sub>1 \<dots> B\<^sub>n\<close> or their parents but not in \<open>A\<^sub>1 \<dots> |
544 yields \<^emph>\<open>all\<close> currently known facts. An optional limit for the |
539 A\<^sub>m\<close> or their parents and that are never used. If \<open>n\<close> is \<open>0\<close>, the end of the |
545 number of printed facts may be given; the default is 40. By |
540 range of theories defaults to the current theory. If no range is specified, |
546 default, duplicates are removed from the search result. Use |
|
547 \<open>with_dups\<close> to display duplicates. |
|
548 |
|
549 \<^descr> @{command "find_consts"}~\<open>criteria\<close> prints all constants |
|
550 whose type meets all of the given criteria. The criterion \<open>strict: ty\<close> is met by any type that matches the type pattern |
|
551 \<open>ty\<close>. Patterns may contain both the dummy type ``\<open>_\<close>'' |
|
552 and sort constraints. The criterion \<open>ty\<close> is similar, but it |
|
553 also matches against subtypes. The criterion \<open>name: p\<close> and |
|
554 the prefix ``\<open>-\<close>'' function as described for @{command |
|
555 "find_theorems"}. |
|
556 |
|
557 \<^descr> @{command "thm_deps"}~\<open>a\<^sub>1 \<dots> a\<^sub>n\<close> |
|
558 visualizes dependencies of facts, using Isabelle's graph browser |
|
559 tool (see also @{cite "isabelle-system"}). |
|
560 |
|
561 \<^descr> @{command "unused_thms"}~\<open>A\<^sub>1 \<dots> A\<^sub>m - B\<^sub>1 \<dots> B\<^sub>n\<close> |
|
562 displays all theorems that are proved in theories \<open>B\<^sub>1 \<dots> B\<^sub>n\<close> |
|
563 or their parents but not in \<open>A\<^sub>1 \<dots> A\<^sub>m\<close> or their parents and |
|
564 that are never used. |
|
565 If \<open>n\<close> is \<open>0\<close>, the end of the range of theories |
|
566 defaults to the current theory. If no range is specified, |
|
567 only the unused theorems in the current theory are displayed. |
541 only the unused theorems in the current theory are displayed. |
568 \<close> |
542 \<close> |
569 |
543 |
570 end |
544 end |