4 |
4 |
5 chapter \<open>Outer syntax --- the theory language \label{ch:outer-syntax}\<close> |
5 chapter \<open>Outer syntax --- the theory language \label{ch:outer-syntax}\<close> |
6 |
6 |
7 text \<open> |
7 text \<open> |
8 The rather generic framework of Isabelle/Isar syntax emerges from |
8 The rather generic framework of Isabelle/Isar syntax emerges from |
9 three main syntactic categories: \emph{commands} of the top-level |
9 three main syntactic categories: \<^emph>\<open>commands\<close> of the top-level |
10 Isar engine (covering theory and proof elements), \emph{methods} for |
10 Isar engine (covering theory and proof elements), \<^emph>\<open>methods\<close> for |
11 general goal refinements (analogous to traditional ``tactics''), and |
11 general goal refinements (analogous to traditional ``tactics''), and |
12 \emph{attributes} for operations on facts (within a certain |
12 \<^emph>\<open>attributes\<close> for operations on facts (within a certain |
13 context). Subsequently we give a reference of basic syntactic |
13 context). Subsequently we give a reference of basic syntactic |
14 entities underlying Isabelle/Isar syntax in a bottom-up manner. |
14 entities underlying Isabelle/Isar syntax in a bottom-up manner. |
15 Concrete theory and proof language elements will be introduced later |
15 Concrete theory and proof language elements will be introduced later |
16 on. |
16 on. |
17 |
17 |
18 \<^medskip> |
18 \<^medskip> |
19 In order to get started with writing well-formed |
19 In order to get started with writing well-formed |
20 Isabelle/Isar documents, the most important aspect to be noted is |
20 Isabelle/Isar documents, the most important aspect to be noted is |
21 the difference of \emph{inner} versus \emph{outer} syntax. Inner |
21 the difference of \<^emph>\<open>inner\<close> versus \<^emph>\<open>outer\<close> syntax. Inner |
22 syntax is that of Isabelle types and terms of the logic, while outer |
22 syntax is that of Isabelle types and terms of the logic, while outer |
23 syntax is that of Isabelle/Isar theory sources (specifications and |
23 syntax is that of Isabelle/Isar theory sources (specifications and |
24 proofs). As a general rule, inner syntax entities may occur only as |
24 proofs). As a general rule, inner syntax entities may occur only as |
25 \emph{atomic entities} within outer syntax. For example, the string |
25 \<^emph>\<open>atomic entities\<close> within outer syntax. For example, the string |
26 @{verbatim \<open>"x + y"\<close>} and identifier @{verbatim z} are legal term |
26 @{verbatim \<open>"x + y"\<close>} and identifier @{verbatim z} are legal term |
27 specifications within a theory, while @{verbatim "x + y"} without |
27 specifications within a theory, while @{verbatim "x + y"} without |
28 quotes is not. |
28 quotes is not. |
29 |
29 |
30 Printed theory documents usually omit quotes to gain readability |
30 Printed theory documents usually omit quotes to gain readability |
67 section \<open>Lexical matters \label{sec:outer-lex}\<close> |
67 section \<open>Lexical matters \label{sec:outer-lex}\<close> |
68 |
68 |
69 text \<open>The outer lexical syntax consists of three main categories of |
69 text \<open>The outer lexical syntax consists of three main categories of |
70 syntax tokens: |
70 syntax tokens: |
71 |
71 |
72 \<^enum> \emph{major keywords} --- the command names that are available |
72 \<^enum> \<^emph>\<open>major keywords\<close> --- the command names that are available |
73 in the present logic session; |
73 in the present logic session; |
74 |
74 |
75 \<^enum> \emph{minor keywords} --- additional literal tokens required |
75 \<^enum> \<^emph>\<open>minor keywords\<close> --- additional literal tokens required |
76 by the syntax of commands; |
76 by the syntax of commands; |
77 |
77 |
78 \<^enum> \emph{named tokens} --- various categories of identifiers etc. |
78 \<^enum> \<^emph>\<open>named tokens\<close> --- various categories of identifiers etc. |
79 |
79 |
80 |
80 |
81 Major keywords and minor keywords are guaranteed to be disjoint. |
81 Major keywords and minor keywords are guaranteed to be disjoint. |
82 This helps user-interfaces to determine the overall structure of a |
82 This helps user-interfaces to determine the overall structure of a |
83 theory text, without knowing the full details of command syntax. |
83 theory text, without knowing the full details of command syntax. |
161 |
161 |
162 Source comments take the form @{verbatim "(*"}~@{text |
162 Source comments take the form @{verbatim "(*"}~@{text |
163 "\<dots>"}~@{verbatim "*)"} and may be nested, although the user-interface |
163 "\<dots>"}~@{verbatim "*)"} and may be nested, although the user-interface |
164 might prevent this. Note that this form indicates source comments |
164 might prevent this. Note that this form indicates source comments |
165 only, which are stripped after lexical analysis of the input. The |
165 only, which are stripped after lexical analysis of the input. The |
166 Isar syntax also provides proper \emph{document comments} that are |
166 Isar syntax also provides proper \<^emph>\<open>document comments\<close> that are |
167 considered as part of the text (see \secref{sec:comments}). |
167 considered as part of the text (see \secref{sec:comments}). |
168 |
168 |
169 Common mathematical symbols such as @{text \<forall>} are represented in |
169 Common mathematical symbols such as @{text \<forall>} are represented in |
170 Isabelle as @{verbatim \<forall>}. There are infinitely many Isabelle |
170 Isabelle as @{verbatim \<forall>}. There are infinitely many Isabelle |
171 symbols like this, although proper presentation is left to front-end |
171 symbols like this, although proper presentation is left to front-end |
186 |
186 |
187 |
187 |
188 subsection \<open>Names\<close> |
188 subsection \<open>Names\<close> |
189 |
189 |
190 text \<open>Entity @{syntax name} usually refers to any name of types, |
190 text \<open>Entity @{syntax name} usually refers to any name of types, |
191 constants, theorems etc.\ that are to be \emph{declared} or |
191 constants, theorems etc.\ that are to be \<^emph>\<open>declared\<close> or |
192 \emph{defined} (so qualified identifiers are excluded here). Quoted |
192 \<^emph>\<open>defined\<close> (so qualified identifiers are excluded here). Quoted |
193 strings provide an escape for non-identifier names or those ruled |
193 strings provide an escape for non-identifier names or those ruled |
194 out by outer syntax keywords (e.g.\ quoted @{verbatim \<open>"let"\<close>}). |
194 out by outer syntax keywords (e.g.\ quoted @{verbatim \<open>"let"\<close>}). |
195 Already existing objects are usually referenced by @{syntax |
195 Already existing objects are usually referenced by @{syntax |
196 nameref}. |
196 nameref}. |
197 |
197 |
536 theorems that contain the pattern @{text t} -- as usual, patterns |
536 theorems that contain the pattern @{text t} -- as usual, patterns |
537 may contain occurrences of the dummy ``@{text _}'', schematic |
537 may contain occurrences of the dummy ``@{text _}'', schematic |
538 variables, and type constraints. |
538 variables, and type constraints. |
539 |
539 |
540 Criteria can be preceded by ``@{text "-"}'' to select theorems that |
540 Criteria can be preceded by ``@{text "-"}'' to select theorems that |
541 do \emph{not} match. Note that giving the empty list of criteria |
541 do \<^emph>\<open>not\<close> match. Note that giving the empty list of criteria |
542 yields \emph{all} currently known facts. An optional limit for the |
542 yields \<^emph>\<open>all\<close> currently known facts. An optional limit for the |
543 number of printed facts may be given; the default is 40. By |
543 number of printed facts may be given; the default is 40. By |
544 default, duplicates are removed from the search result. Use |
544 default, duplicates are removed from the search result. Use |
545 @{text with_dups} to display duplicates. |
545 @{text with_dups} to display duplicates. |
546 |
546 |
547 \<^descr> @{command "find_consts"}~@{text criteria} prints all constants |
547 \<^descr> @{command "find_consts"}~@{text criteria} prints all constants |