12 \begin{matharray}{rcl} |
12 \begin{matharray}{rcl} |
13 @{command_def "theory"} & : & \isartrans{toplevel}{theory} \\ |
13 @{command_def "theory"} & : & \isartrans{toplevel}{theory} \\ |
14 @{command_def (global) "end"} & : & \isartrans{theory}{toplevel} \\ |
14 @{command_def (global) "end"} & : & \isartrans{theory}{toplevel} \\ |
15 \end{matharray} |
15 \end{matharray} |
16 |
16 |
17 Isabelle/Isar theories are defined via theory file, which contain |
17 Isabelle/Isar theories are defined via theory files, which may |
18 both specifications and proofs; occasionally definitional mechanisms |
18 contain both specifications and proofs; occasionally definitional |
19 also require some explicit proof. The theory body may be |
19 mechanisms also require some explicit proof. The theory body may be |
20 sub-structered by means of \emph{local theory} target mechanisms, |
20 sub-structured by means of \emph{local theory targets}, such as |
21 notably @{command "locale"} and @{command "class"}. |
21 @{command "locale"} and @{command "class"}. |
22 |
22 |
23 The first ``real'' command of any theory has to be @{command |
23 The first proper command of a theory is @{command "theory"}, which |
24 "theory"}, which starts a new theory based on the merge of existing |
24 indicates imports of previous theories and optional dependencies on |
25 ones. Just preceding the @{command "theory"} keyword, there may be |
25 other source files (usually in ML). Just preceding the initial |
26 an optional @{command "header"} declaration, which is relevant to |
26 @{command "theory"} command there may be an optional @{command |
27 document preparation only; it acts very much like a special |
27 "header"} declaration, which is only relevant to document |
28 pre-theory markup command (cf.\ \secref{sec:markup}). The @{command |
28 preparation: see also the other section markup commands in |
29 (global) "end"} command concludes a theory development; it has to be |
29 \secref{sec:markup}. |
30 the very last command of any theory file loaded in batch-mode. |
30 |
|
31 A theory is concluded by a final @{command (global) "end"} command, |
|
32 one that does not belong to a local theory target. No further |
|
33 commands may follow such a global @{command (global) "end"}, |
|
34 although some user-interfaces might pretend that trailing input is |
|
35 admissible. |
31 |
36 |
32 \begin{rail} |
37 \begin{rail} |
33 'theory' name 'imports' (name +) uses? 'begin' |
38 'theory' name 'imports' (name +) uses? 'begin' |
34 ; |
39 ; |
35 |
40 |
40 |
45 |
41 \item [@{command "theory"}~@{text "A \<IMPORTS> B\<^sub>1 \<dots> |
46 \item [@{command "theory"}~@{text "A \<IMPORTS> B\<^sub>1 \<dots> |
42 B\<^sub>n \<BEGIN>"}] starts a new theory @{text A} based on the |
47 B\<^sub>n \<BEGIN>"}] starts a new theory @{text A} based on the |
43 merge of existing theories @{text "B\<^sub>1 \<dots> B\<^sub>n"}. |
48 merge of existing theories @{text "B\<^sub>1 \<dots> B\<^sub>n"}. |
44 |
49 |
45 Due to inclusion of several ancestors, the overall theory structure |
50 Due to the possibility to import more than one ancestor, the |
46 emerging in an Isabelle session forms a directed acyclic graph |
51 resulting theory structure of an Isabelle session forms a directed |
47 (DAG). Isabelle's theory loader ensures that the sources |
52 acyclic graph (DAG). Isabelle's theory loader ensures that the |
48 contributing to the development graph are always up-to-date. |
53 sources contributing to the development graph are always up-to-date: |
49 Changed files are automatically reloaded when processing theory |
54 changed files are automatically reloaded whenever a theory header |
50 headers. |
55 specification is processed. |
51 |
56 |
52 The optional @{keyword_def "uses"} specification declares additional |
57 The optional @{keyword_def "uses"} specification declares additional |
53 dependencies on extra files (usually ML sources). Files will be |
58 dependencies on extra files (usually ML sources). Files will be |
54 loaded immediately (as ML), unless the name is put in parentheses, |
59 loaded immediately (as ML), unless the name is parenthesized. The |
55 which merely documents the dependency to be resolved later in the |
60 latter case records a dependency that needs to be resolved later in |
56 text (typically via explicit @{command_ref "use"} in the body text, |
61 the text, usually via explicit @{command_ref "use"} for ML files; |
57 see \secref{sec:ML}). |
62 other file formats require specific load commands defined by the |
|
63 corresponding tools or packages. |
58 |
64 |
59 \item [@{command (global) "end"}] concludes the current theory |
65 \item [@{command (global) "end"}] concludes the current theory |
60 definition. |
66 definition. Note that local theory targets involve a local |
|
67 @{command (local) "end"}, which is clear from the nesting. |
61 |
68 |
62 \end{descr} |
69 \end{descr} |
63 *} |
70 *} |
64 |
71 |
65 |
72 |