4 imports Main |
4 imports Main |
5 begin |
5 begin |
6 |
6 |
7 chapter {* Specifications *} |
7 chapter {* Specifications *} |
8 |
8 |
|
9 section {* Defining theories \label{sec:begin-thy} *} |
|
10 |
|
11 text {* |
|
12 \begin{matharray}{rcl} |
|
13 @{command_def "header"} & : & \isarkeep{toplevel} \\ |
|
14 @{command_def "theory"} & : & \isartrans{toplevel}{theory} \\ |
|
15 @{command_def "end"} & : & \isartrans{theory}{toplevel} \\ |
|
16 \end{matharray} |
|
17 |
|
18 Isabelle/Isar theories are defined via theory, which contain both |
|
19 specifications and proofs; occasionally definitional mechanisms also |
|
20 require some explicit proof. |
|
21 |
|
22 The first ``real'' command of any theory has to be @{command |
|
23 "theory"}, which starts a new theory based on the merge of existing |
|
24 ones. Just preceding the @{command "theory"} keyword, there may be |
|
25 an optional @{command "header"} declaration, which is relevant to |
|
26 document preparation only; it acts very much like a special |
|
27 pre-theory markup command (cf.\ \secref{sec:markup-thy} and |
|
28 \secref{sec:markup-thy}). The @{command "end"} command concludes a |
|
29 theory development; it has to be the very last command of any theory |
|
30 file loaded in batch-mode. |
|
31 |
|
32 \begin{rail} |
|
33 'header' text |
|
34 ; |
|
35 'theory' name 'imports' (name +) uses? 'begin' |
|
36 ; |
|
37 |
|
38 uses: 'uses' ((name | parname) +); |
|
39 \end{rail} |
|
40 |
|
41 \begin{descr} |
|
42 |
|
43 \item [@{command "header"}~@{text "text"}] provides plain text |
|
44 markup just preceding the formal beginning of a theory. In actual |
|
45 document preparation the corresponding {\LaTeX} macro @{verbatim |
|
46 "\\isamarkupheader"} may be redefined to produce chapter or section |
|
47 headings. See also \secref{sec:markup-thy} and |
|
48 \secref{sec:markup-prf} for further markup commands. |
|
49 |
|
50 \item [@{command "theory"}~@{text "A \<IMPORTS> B\<^sub>1 \<dots> |
|
51 B\<^sub>n \<BEGIN>"}] starts a new theory @{text A} based on the |
|
52 merge of existing theories @{text "B\<^sub>1 \<dots> B\<^sub>n"}. |
|
53 |
|
54 Due to inclusion of several ancestors, the overall theory structure |
|
55 emerging in an Isabelle session forms a directed acyclic graph |
|
56 (DAG). Isabelle's theory loader ensures that the sources |
|
57 contributing to the development graph are always up-to-date. |
|
58 Changed files are automatically reloaded when processing theory |
|
59 headers. |
|
60 |
|
61 The optional @{keyword_def "uses"} specification declares additional |
|
62 dependencies on extra files (usually ML sources). Files will be |
|
63 loaded immediately (as ML), unless the name is put in parentheses, |
|
64 which merely documents the dependency to be resolved later in the |
|
65 text (typically via explicit @{command_ref "use"} in the body text, |
|
66 see \secref{sec:ML}). |
|
67 |
|
68 \item [@{command "end"}] concludes the current theory definition or |
|
69 context switch. |
|
70 |
|
71 \end{descr} |
|
72 *} |
|
73 |
9 end |
74 end |