1 |
|
2 section {* Sessions and document preparation *} |
|
3 |
|
4 section {* Structured output *} |
|
5 |
|
6 subsection {* Pretty printing *} |
|
7 |
|
8 text FIXME |
|
9 |
|
10 subsection {* Output channels *} |
|
11 |
|
12 text FIXME |
|
13 |
|
14 subsection {* Print modes \label{sec:print-mode} *} |
|
15 |
|
16 text FIXME |
|
17 |
|
18 text {* |
|
19 |
|
20 |
|
21 \medskip The general concept supports block-structured reasoning |
|
22 nicely, with arbitrary mechanisms for introducing local assumptions. |
|
23 The common reasoning pattern is as follows: |
|
24 |
|
25 \medskip |
|
26 \begin{tabular}{l} |
|
27 @{text "add_assms e\<^isub>1 A\<^isub>1"} \\ |
|
28 @{text "\<dots>"} \\ |
|
29 @{text "add_assms e\<^isub>n A\<^isub>n"} \\ |
|
30 @{text "export"} \\ |
|
31 \end{tabular} |
|
32 \medskip |
|
33 |
|
34 \noindent The final @{text "export"} will turn any fact @{text |
|
35 "A\<^isub>1, \<dots>, A\<^isub>n \<turnstile> B"} into some @{text "\<turnstile> B'"}, by |
|
36 applying the export rules @{text "e\<^isub>1, \<dots>, e\<^isub>n"} |
|
37 inside-out. |
|
38 |
|
39 |
|
40 A \emph{fixed variable} acts like a local constant in the current |
|
41 context, representing some simple type @{text "\<alpha>"}, or some value |
|
42 @{text "x: \<tau>"} (for a fixed type expression @{text "\<tau>"}). A |
|
43 \emph{schematic variable} acts like a placeholder for arbitrary |
|
44 elements, similar to outermost quantification. The division between |
|
45 fixed and schematic variables tells which abstract entities are |
|
46 inside and outside the current context. |
|
47 |
|
48 |
|
49 @{index_ML Variable.trade: "Proof.context -> (thm list -> thm list) -> thm list -> thm list"} \\ |
|
50 |
|
51 |
|
52 |
|
53 \item @{ML Variable.trade} composes @{ML Variable.import} and @{ML |
|
54 Variable.export}, i.e.\ it provides a view on facts with all |
|
55 variables being fixed in the current context. |
|
56 |
|
57 |
|
58 In practice, super-contexts emerge either by merging existing ones, |
|
59 or by adding explicit declarations. For example, new theories are |
|
60 usually derived by importing existing theories from the library |
|
61 @{text "\<Theta> = \<Theta>\<^sub>1 + \<dots> + \<Theta>\<^isub>n"}, or |
|
62 |
|
63 |
|
64 |
|
65 The Isar toplevel works differently for interactive developments |
|
66 vs.\ batch processing of theory sources. For example, diagnostic |
|
67 commands produce a warning batch mode, because they are considered |
|
68 alien to the final theory document being produced eventually. |
|
69 Moreover, full @{text undo} with intermediate checkpoints to protect |
|
70 against destroying theories accidentally are limited to interactive |
|
71 mode. In batch mode there is only a single strictly linear stream |
|
72 of potentially desctructive theory transformations. |
|
73 |
|
74 \item @{ML Toplevel.empty} is an empty transition; the Isar command |
|
75 dispatcher internally applies @{ML Toplevel.name} (for the command) |
|
76 name and @{ML Toplevel.position} for the source position. |
|
77 |
|
78 *} |
|
79 |
|