author | wenzelm |
Mon, 02 May 2011 16:33:21 +0200 | |
changeset 42616 | 92715b528e78 |
parent 42510 | b9c106763325 |
child 42662 | 2080fe35abea |
permissions | -rw-r--r-- |
30296 | 1 |
% |
2 |
\begin{isabellebody}% |
|
3 |
\def\isabellecontext{Prelim}% |
|
4 |
% |
|
5 |
\isadelimtheory |
|
6 |
% |
|
7 |
\endisadelimtheory |
|
8 |
% |
|
9 |
\isatagtheory |
|
10 |
\isacommand{theory}\isamarkupfalse% |
|
11 |
\ Prelim\isanewline |
|
12 |
\isakeyword{imports}\ Base\isanewline |
|
13 |
\isakeyword{begin}% |
|
14 |
\endisatagtheory |
|
15 |
{\isafoldtheory}% |
|
16 |
% |
|
17 |
\isadelimtheory |
|
18 |
% |
|
19 |
\endisadelimtheory |
|
20 |
% |
|
21 |
\isamarkupchapter{Preliminaries% |
|
22 |
} |
|
23 |
\isamarkuptrue% |
|
24 |
% |
|
25 |
\isamarkupsection{Contexts \label{sec:context}% |
|
26 |
} |
|
27 |
\isamarkuptrue% |
|
28 |
% |
|
29 |
\begin{isamarkuptext}% |
|
30 |
A logical context represents the background that is required for |
|
31 |
formulating statements and composing proofs. It acts as a medium to |
|
32 |
produce formal content, depending on earlier material (declarations, |
|
33 |
results etc.). |
|
34 |
||
35 |
For example, derivations within the Isabelle/Pure logic can be |
|
40406 | 36 |
described as a judgment \isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isaliteral{5C3C54686574613E}{\isasymTheta}}\ {\isaliteral{5C3C7068693E}{\isasymphi}}}, which means that a |
37 |
proposition \isa{{\isaliteral{5C3C7068693E}{\isasymphi}}} is derivable from hypotheses \isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}} |
|
38 |
within the theory \isa{{\isaliteral{5C3C54686574613E}{\isasymTheta}}}. There are logical reasons for |
|
39 |
keeping \isa{{\isaliteral{5C3C54686574613E}{\isasymTheta}}} and \isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}} separate: theories can be |
|
30296 | 40 |
liberal about supporting type constructors and schematic |
41 |
polymorphism of constants and axioms, while the inner calculus of |
|
40406 | 42 |
\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ {\isaliteral{5C3C7068693E}{\isasymphi}}} is strictly limited to Simple Type Theory (with |
30296 | 43 |
fixed type variables in the assumptions). |
44 |
||
45 |
\medskip Contexts and derivations are linked by the following key |
|
46 |
principles: |
|
47 |
||
48 |
\begin{itemize} |
|
49 |
||
50 |
\item Transfer: monotonicity of derivations admits results to be |
|
40406 | 51 |
transferred into a \emph{larger} context, i.e.\ \isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isaliteral{5C3C54686574613E}{\isasymTheta}}\ {\isaliteral{5C3C7068693E}{\isasymphi}}} implies \isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}{\isaliteral{27}{\isacharprime}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isaliteral{5C3C54686574613E}{\isasymTheta}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isaliteral{27}{\isacharprime}}\ {\isaliteral{5C3C7068693E}{\isasymphi}}} for contexts \isa{{\isaliteral{5C3C54686574613E}{\isasymTheta}}{\isaliteral{27}{\isacharprime}}\ {\isaliteral{5C3C73757073657465713E}{\isasymsupseteq}}\ {\isaliteral{5C3C54686574613E}{\isasymTheta}}} and \isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}{\isaliteral{27}{\isacharprime}}\ {\isaliteral{5C3C73757073657465713E}{\isasymsupseteq}}\ {\isaliteral{5C3C47616D6D613E}{\isasymGamma}}}. |
30296 | 52 |
|
53 |
\item Export: discharge of hypotheses admits results to be exported |
|
40406 | 54 |
into a \emph{smaller} context, i.e.\ \isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}{\isaliteral{27}{\isacharprime}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isaliteral{5C3C54686574613E}{\isasymTheta}}\ {\isaliteral{5C3C7068693E}{\isasymphi}}} |
55 |
implies \isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isaliteral{5C3C54686574613E}{\isasymTheta}}\ {\isaliteral{5C3C44656C74613E}{\isasymDelta}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{5C3C7068693E}{\isasymphi}}} where \isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}{\isaliteral{27}{\isacharprime}}\ {\isaliteral{5C3C73757073657465713E}{\isasymsupseteq}}\ {\isaliteral{5C3C47616D6D613E}{\isasymGamma}}} and |
|
56 |
\isa{{\isaliteral{5C3C44656C74613E}{\isasymDelta}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5C3C47616D6D613E}{\isasymGamma}}{\isaliteral{27}{\isacharprime}}\ {\isaliteral{2D}{\isacharminus}}\ {\isaliteral{5C3C47616D6D613E}{\isasymGamma}}}. Note that \isa{{\isaliteral{5C3C54686574613E}{\isasymTheta}}} remains unchanged here, |
|
57 |
only the \isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}} part is affected. |
|
30296 | 58 |
|
59 |
\end{itemize} |
|
60 |
||
61 |
\medskip By modeling the main characteristics of the primitive |
|
40406 | 62 |
\isa{{\isaliteral{5C3C54686574613E}{\isasymTheta}}} and \isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}} above, and abstracting over any |
30296 | 63 |
particular logical content, we arrive at the fundamental notions of |
64 |
\emph{theory context} and \emph{proof context} in Isabelle/Isar. |
|
65 |
These implement a certain policy to manage arbitrary \emph{context |
|
66 |
data}. There is a strongly-typed mechanism to declare new kinds of |
|
67 |
data at compile time. |
|
68 |
||
69 |
The internal bootstrap process of Isabelle/Pure eventually reaches a |
|
40406 | 70 |
stage where certain data slots provide the logical content of \isa{{\isaliteral{5C3C54686574613E}{\isasymTheta}}} and \isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}} sketched above, but this does not stop there! |
30296 | 71 |
Various additional data slots support all kinds of mechanisms that |
72 |
are not necessarily part of the core logic. |
|
73 |
||
74 |
For example, there would be data for canonical introduction and |
|
75 |
elimination rules for arbitrary operators (depending on the |
|
76 |
object-logic and application), which enables users to perform |
|
77 |
standard proof steps implicitly (cf.\ the \isa{rule} method |
|
78 |
\cite{isabelle-isar-ref}). |
|
79 |
||
80 |
\medskip Thus Isabelle/Isar is able to bring forth more and more |
|
81 |
concepts successively. In particular, an object-logic like |
|
82 |
Isabelle/HOL continues the Isabelle/Pure setup by adding specific |
|
83 |
components for automated reasoning (classical reasoner, tableau |
|
84 |
prover, structured induction etc.) and derived specification |
|
85 |
mechanisms (inductive predicates, recursive functions etc.). All of |
|
86 |
this is ultimately based on the generic data management by theory |
|
87 |
and proof contexts introduced here.% |
|
88 |
\end{isamarkuptext}% |
|
89 |
\isamarkuptrue% |
|
90 |
% |
|
91 |
\isamarkupsubsection{Theory context \label{sec:context-theory}% |
|
92 |
} |
|
93 |
\isamarkuptrue% |
|
94 |
% |
|
95 |
\begin{isamarkuptext}% |
|
35001 | 96 |
A \emph{theory} is a data container with explicit name and |
97 |
unique identifier. Theories are related by a (nominal) sub-theory |
|
30296 | 98 |
relation, which corresponds to the dependency graph of the original |
99 |
construction; each theory is derived from a certain sub-graph of |
|
35001 | 100 |
ancestor theories. To this end, the system maintains a set of |
101 |
symbolic ``identification stamps'' within each theory. |
|
30296 | 102 |
|
35001 | 103 |
In order to avoid the full-scale overhead of explicit sub-theory |
104 |
identification of arbitrary intermediate stages, a theory is |
|
105 |
switched into \isa{draft} mode under certain circumstances. A |
|
106 |
draft theory acts like a linear type, where updates invalidate |
|
107 |
earlier versions. An invalidated draft is called \emph{stale}. |
|
30296 | 108 |
|
35001 | 109 |
The \isa{checkpoint} operation produces a safe stepping stone |
110 |
that will survive the next update without becoming stale: both the |
|
111 |
old and the new theory remain valid and are related by the |
|
112 |
sub-theory relation. Checkpointing essentially recovers purely |
|
113 |
functional theory values, at the expense of some extra internal |
|
114 |
bookkeeping. |
|
30296 | 115 |
|
116 |
The \isa{copy} operation produces an auxiliary version that has |
|
117 |
the same data content, but is unrelated to the original: updates of |
|
118 |
the copy do not affect the original, neither does the sub-theory |
|
119 |
relation hold. |
|
120 |
||
35001 | 121 |
The \isa{merge} operation produces the least upper bound of two |
122 |
theories, which actually degenerates into absorption of one theory |
|
123 |
into the other (according to the nominal sub-theory relation). |
|
124 |
||
125 |
The \isa{begin} operation starts a new theory by importing |
|
126 |
several parent theories and entering a special mode of nameless |
|
127 |
incremental updates, until the final \isa{end} operation is |
|
128 |
performed. |
|
129 |
||
30296 | 130 |
\medskip The example in \figref{fig:ex-theory} below shows a theory |
131 |
graph derived from \isa{Pure}, with theory \isa{Length} |
|
132 |
importing \isa{Nat} and \isa{List}. The body of \isa{Length} consists of a sequence of updates, working mostly on |
|
35001 | 133 |
drafts internally, while transaction boundaries of Isar top-level |
134 |
commands (\secref{sec:isar-toplevel}) are guaranteed to be safe |
|
135 |
checkpoints. |
|
30296 | 136 |
|
137 |
\begin{figure}[htb] |
|
138 |
\begin{center} |
|
139 |
\begin{tabular}{rcccl} |
|
140 |
& & \isa{Pure} \\ |
|
40406 | 141 |
& & \isa{{\isaliteral{5C3C646F776E3E}{\isasymdown}}} \\ |
30296 | 142 |
& & \isa{FOL} \\ |
143 |
& $\swarrow$ & & $\searrow$ & \\ |
|
144 |
\isa{Nat} & & & & \isa{List} \\ |
|
145 |
& $\searrow$ & & $\swarrow$ \\ |
|
146 |
& & \isa{Length} \\ |
|
147 |
& & \multicolumn{3}{l}{~~\hyperlink{keyword.imports}{\mbox{\isa{\isakeyword{imports}}}}} \\ |
|
148 |
& & \multicolumn{3}{l}{~~\hyperlink{keyword.begin}{\mbox{\isa{\isakeyword{begin}}}}} \\ |
|
149 |
& & $\vdots$~~ \\ |
|
40406 | 150 |
& & \isa{{\isaliteral{5C3C62756C6C65743E}{\isasymbullet}}}~~ \\ |
30296 | 151 |
& & $\vdots$~~ \\ |
40406 | 152 |
& & \isa{{\isaliteral{5C3C62756C6C65743E}{\isasymbullet}}}~~ \\ |
30296 | 153 |
& & $\vdots$~~ \\ |
154 |
& & \multicolumn{3}{l}{~~\hyperlink{command.end}{\mbox{\isa{\isacommand{end}}}}} \\ |
|
155 |
\end{tabular} |
|
156 |
\caption{A theory definition depending on ancestors}\label{fig:ex-theory} |
|
157 |
\end{center} |
|
158 |
\end{figure} |
|
159 |
||
160 |
\medskip There is a separate notion of \emph{theory reference} for |
|
161 |
maintaining a live link to an evolving theory context: updates on |
|
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
162 |
drafts are propagated automatically. Dynamic updating stops when |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
163 |
the next \isa{checkpoint} is reached. |
30296 | 164 |
|
165 |
Derived entities may store a theory reference in order to indicate |
|
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
166 |
the formal context from which they are derived. This implicitly |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
167 |
assumes monotonic reasoning, because the referenced context may |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
168 |
become larger without further notice.% |
30296 | 169 |
\end{isamarkuptext}% |
170 |
\isamarkuptrue% |
|
171 |
% |
|
172 |
\isadelimmlref |
|
173 |
% |
|
174 |
\endisadelimmlref |
|
175 |
% |
|
176 |
\isatagmlref |
|
177 |
% |
|
178 |
\begin{isamarkuptext}% |
|
179 |
\begin{mldecls} |
|
180 |
\indexdef{}{ML type}{theory}\verb|type theory| \\ |
|
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
181 |
\indexdef{}{ML}{Theory.eq\_thy}\verb|Theory.eq_thy: theory * theory -> bool| \\ |
30296 | 182 |
\indexdef{}{ML}{Theory.subthy}\verb|Theory.subthy: theory * theory -> bool| \\ |
183 |
\indexdef{}{ML}{Theory.checkpoint}\verb|Theory.checkpoint: theory -> theory| \\ |
|
184 |
\indexdef{}{ML}{Theory.copy}\verb|Theory.copy: theory -> theory| \\ |
|
35001 | 185 |
\indexdef{}{ML}{Theory.merge}\verb|Theory.merge: theory * theory -> theory| \\ |
186 |
\indexdef{}{ML}{Theory.begin\_theory}\verb|Theory.begin_theory: string -> theory list -> theory| \\ |
|
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
187 |
\indexdef{}{ML}{Theory.parents\_of}\verb|Theory.parents_of: theory -> theory list| \\ |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
188 |
\indexdef{}{ML}{Theory.ancestors\_of}\verb|Theory.ancestors_of: theory -> theory list| \\ |
30296 | 189 |
\end{mldecls} |
190 |
\begin{mldecls} |
|
191 |
\indexdef{}{ML type}{theory\_ref}\verb|type theory_ref| \\ |
|
192 |
\indexdef{}{ML}{Theory.deref}\verb|Theory.deref: theory_ref -> theory| \\ |
|
193 |
\indexdef{}{ML}{Theory.check\_thy}\verb|Theory.check_thy: theory -> theory_ref| \\ |
|
194 |
\end{mldecls} |
|
195 |
||
196 |
\begin{description} |
|
197 |
||
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
198 |
\item Type \verb|theory| represents theory contexts. This is |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
199 |
essentially a linear type, with explicit runtime checking. |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
200 |
Primitive theory operations destroy the original version, which then |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
201 |
becomes ``stale''. This can be prevented by explicit checkpointing, |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
202 |
which the system does at least at the boundary of toplevel command |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
203 |
transactions \secref{sec:isar-toplevel}. |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
204 |
|
40406 | 205 |
\item \verb|Theory.eq_thy|~\isa{{\isaliteral{28}{\isacharparenleft}}thy\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ thy\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}{\isaliteral{29}{\isacharparenright}}} check strict |
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
206 |
identity of two theories. |
30296 | 207 |
|
40406 | 208 |
\item \verb|Theory.subthy|~\isa{{\isaliteral{28}{\isacharparenleft}}thy\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ thy\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}{\isaliteral{29}{\isacharparenright}}} compares theories |
35001 | 209 |
according to the intrinsic graph structure of the construction. |
210 |
This sub-theory relation is a nominal approximation of inclusion |
|
40406 | 211 |
(\isa{{\isaliteral{5C3C73756273657465713E}{\isasymsubseteq}}}) of the corresponding content (according to the |
35001 | 212 |
semantics of the ML modules that implement the data). |
30296 | 213 |
|
214 |
\item \verb|Theory.checkpoint|~\isa{thy} produces a safe |
|
35001 | 215 |
stepping stone in the linear development of \isa{thy}. This |
216 |
changes the old theory, but the next update will result in two |
|
217 |
related, valid theories. |
|
218 |
||
219 |
\item \verb|Theory.copy|~\isa{thy} produces a variant of \isa{thy} with the same data. The copy is not related to the original, |
|
220 |
but the original is unchanged. |
|
30296 | 221 |
|
40406 | 222 |
\item \verb|Theory.merge|~\isa{{\isaliteral{28}{\isacharparenleft}}thy\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ thy\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}{\isaliteral{29}{\isacharparenright}}} absorbs one theory |
223 |
into the other, without changing \isa{thy\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}} or \isa{thy\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}}. |
|
35001 | 224 |
This version of ad-hoc theory merge fails for unrelated theories! |
225 |
||
226 |
\item \verb|Theory.begin_theory|~\isa{name\ parents} constructs |
|
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
227 |
a new theory based on the given parents. This ML function is |
35001 | 228 |
normally not invoked directly. |
30296 | 229 |
|
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
230 |
\item \verb|Theory.parents_of|~\isa{thy} returns the direct |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
231 |
ancestors of \isa{thy}. |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
232 |
|
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
233 |
\item \verb|Theory.ancestors_of|~\isa{thy} returns all |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
234 |
ancestors of \isa{thy} (not including \isa{thy} itself). |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
235 |
|
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
236 |
\item Type \verb|theory_ref| represents a sliding reference to |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
237 |
an always valid theory; updates on the original are propagated |
30296 | 238 |
automatically. |
239 |
||
40406 | 240 |
\item \verb|Theory.deref|~\isa{thy{\isaliteral{5F}{\isacharunderscore}}ref} turns a \verb|theory_ref| into an \verb|theory| value. As the referenced |
30296 | 241 |
theory evolves monotonically over time, later invocations of \verb|Theory.deref| may refer to a larger context. |
242 |
||
243 |
\item \verb|Theory.check_thy|~\isa{thy} produces a \verb|theory_ref| from a valid \verb|theory| value. |
|
244 |
||
245 |
\end{description}% |
|
246 |
\end{isamarkuptext}% |
|
247 |
\isamarkuptrue% |
|
248 |
% |
|
249 |
\endisatagmlref |
|
250 |
{\isafoldmlref}% |
|
251 |
% |
|
252 |
\isadelimmlref |
|
253 |
% |
|
254 |
\endisadelimmlref |
|
255 |
% |
|
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
256 |
\isadelimmlantiq |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
257 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
258 |
\endisadelimmlantiq |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
259 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
260 |
\isatagmlantiq |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
261 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
262 |
\begin{isamarkuptext}% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
263 |
\begin{matharray}{rcl} |
40406 | 264 |
\indexdef{}{ML antiquotation}{theory}\hypertarget{ML antiquotation.theory}{\hyperlink{ML antiquotation.theory}{\mbox{\isa{theory}}}} & : & \isa{ML{\isaliteral{5F}{\isacharunderscore}}antiquotation} \\ |
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
265 |
\end{matharray} |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
266 |
|
42510
b9c106763325
use @{rail} antiquotation (with some nested markup);
wenzelm
parents:
42401
diff
changeset
|
267 |
\begin{railoutput} |
b9c106763325
use @{rail} antiquotation (with some nested markup);
wenzelm
parents:
42401
diff
changeset
|
268 |
\rail@begin{2}{\isa{}} |
b9c106763325
use @{rail} antiquotation (with some nested markup);
wenzelm
parents:
42401
diff
changeset
|
269 |
\rail@term{\hyperlink{ML antiquotation.theory}{\mbox{\isa{theory}}}}[] |
b9c106763325
use @{rail} antiquotation (with some nested markup);
wenzelm
parents:
42401
diff
changeset
|
270 |
\rail@bar |
b9c106763325
use @{rail} antiquotation (with some nested markup);
wenzelm
parents:
42401
diff
changeset
|
271 |
\rail@nextbar{1} |
b9c106763325
use @{rail} antiquotation (with some nested markup);
wenzelm
parents:
42401
diff
changeset
|
272 |
\rail@nont{\isa{nameref}}[] |
b9c106763325
use @{rail} antiquotation (with some nested markup);
wenzelm
parents:
42401
diff
changeset
|
273 |
\rail@endbar |
b9c106763325
use @{rail} antiquotation (with some nested markup);
wenzelm
parents:
42401
diff
changeset
|
274 |
\rail@end |
b9c106763325
use @{rail} antiquotation (with some nested markup);
wenzelm
parents:
42401
diff
changeset
|
275 |
\end{railoutput} |
b9c106763325
use @{rail} antiquotation (with some nested markup);
wenzelm
parents:
42401
diff
changeset
|
276 |
|
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
277 |
|
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
278 |
\begin{description} |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
279 |
|
40406 | 280 |
\item \isa{{\isaliteral{40}{\isacharat}}{\isaliteral{7B}{\isacharbraceleft}}theory{\isaliteral{7D}{\isacharbraceright}}} refers to the background theory of the |
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
281 |
current context --- as abstract value. |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
282 |
|
40406 | 283 |
\item \isa{{\isaliteral{40}{\isacharat}}{\isaliteral{7B}{\isacharbraceleft}}theory\ A{\isaliteral{7D}{\isacharbraceright}}} refers to an explicitly named ancestor |
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
284 |
theory \isa{A} of the background theory of the current context |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
285 |
--- as abstract value. |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
286 |
|
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
287 |
\end{description}% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
288 |
\end{isamarkuptext}% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
289 |
\isamarkuptrue% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
290 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
291 |
\endisatagmlantiq |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
292 |
{\isafoldmlantiq}% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
293 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
294 |
\isadelimmlantiq |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
295 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
296 |
\endisadelimmlantiq |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
297 |
% |
30296 | 298 |
\isamarkupsubsection{Proof context \label{sec:context-proof}% |
299 |
} |
|
300 |
\isamarkuptrue% |
|
301 |
% |
|
302 |
\begin{isamarkuptext}% |
|
35001 | 303 |
A proof context is a container for pure data with a |
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
304 |
back-reference to the theory from which it is derived. The \isa{init} operation creates a proof context from a given theory. |
35001 | 305 |
Modifications to draft theories are propagated to the proof context |
306 |
as usual, but there is also an explicit \isa{transfer} operation |
|
307 |
to force resynchronization with more substantial updates to the |
|
308 |
underlying theory. |
|
30296 | 309 |
|
35001 | 310 |
Entities derived in a proof context need to record logical |
30296 | 311 |
requirements explicitly, since there is no separate context |
35001 | 312 |
identification or symbolic inclusion as for theories. For example, |
313 |
hypotheses used in primitive derivations (cf.\ \secref{sec:thms}) |
|
40406 | 314 |
are recorded separately within the sequent \isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ {\isaliteral{5C3C7068693E}{\isasymphi}}}, just to |
35001 | 315 |
make double sure. Results could still leak into an alien proof |
316 |
context due to programming errors, but Isabelle/Isar includes some |
|
317 |
extra validity checks in critical positions, notably at the end of a |
|
318 |
sub-proof. |
|
30296 | 319 |
|
320 |
Proof contexts may be manipulated arbitrarily, although the common |
|
321 |
discipline is to follow block structure as a mental model: a given |
|
322 |
context is extended consecutively, and results are exported back |
|
35001 | 323 |
into the original context. Note that an Isar proof state models |
30296 | 324 |
block-structured reasoning explicitly, using a stack of proof |
35001 | 325 |
contexts internally. For various technical reasons, the background |
326 |
theory of an Isar proof state must not be changed while the proof is |
|
327 |
still under construction!% |
|
30296 | 328 |
\end{isamarkuptext}% |
329 |
\isamarkuptrue% |
|
330 |
% |
|
331 |
\isadelimmlref |
|
332 |
% |
|
333 |
\endisadelimmlref |
|
334 |
% |
|
335 |
\isatagmlref |
|
336 |
% |
|
337 |
\begin{isamarkuptext}% |
|
338 |
\begin{mldecls} |
|
339 |
\indexdef{}{ML type}{Proof.context}\verb|type Proof.context| \\ |
|
42361 | 340 |
\indexdef{}{ML}{Proof\_Context.init\_global}\verb|Proof_Context.init_global: theory -> Proof.context| \\ |
341 |
\indexdef{}{ML}{Proof\_Context.theory\_of}\verb|Proof_Context.theory_of: Proof.context -> theory| \\ |
|
342 |
\indexdef{}{ML}{Proof\_Context.transfer}\verb|Proof_Context.transfer: theory -> Proof.context -> Proof.context| \\ |
|
30296 | 343 |
\end{mldecls} |
344 |
||
345 |
\begin{description} |
|
346 |
||
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
347 |
\item Type \verb|Proof.context| represents proof contexts. |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
348 |
Elements of this type are essentially pure values, with a sliding |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
349 |
reference to the background theory. |
30296 | 350 |
|
42361 | 351 |
\item \verb|Proof_Context.init_global|~\isa{thy} produces a proof context |
30296 | 352 |
derived from \isa{thy}, initializing all data. |
353 |
||
42361 | 354 |
\item \verb|Proof_Context.theory_of|~\isa{ctxt} selects the |
30296 | 355 |
background theory from \isa{ctxt}, dereferencing its internal |
356 |
\verb|theory_ref|. |
|
357 |
||
42361 | 358 |
\item \verb|Proof_Context.transfer|~\isa{thy\ ctxt} promotes the |
30296 | 359 |
background theory of \isa{ctxt} to the super theory \isa{thy}. |
360 |
||
361 |
\end{description}% |
|
362 |
\end{isamarkuptext}% |
|
363 |
\isamarkuptrue% |
|
364 |
% |
|
365 |
\endisatagmlref |
|
366 |
{\isafoldmlref}% |
|
367 |
% |
|
368 |
\isadelimmlref |
|
369 |
% |
|
370 |
\endisadelimmlref |
|
371 |
% |
|
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
372 |
\isadelimmlantiq |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
373 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
374 |
\endisadelimmlantiq |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
375 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
376 |
\isatagmlantiq |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
377 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
378 |
\begin{isamarkuptext}% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
379 |
\begin{matharray}{rcl} |
40406 | 380 |
\indexdef{}{ML antiquotation}{context}\hypertarget{ML antiquotation.context}{\hyperlink{ML antiquotation.context}{\mbox{\isa{context}}}} & : & \isa{ML{\isaliteral{5F}{\isacharunderscore}}antiquotation} \\ |
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
381 |
\end{matharray} |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
382 |
|
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
383 |
\begin{description} |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
384 |
|
40406 | 385 |
\item \isa{{\isaliteral{40}{\isacharat}}{\isaliteral{7B}{\isacharbraceleft}}context{\isaliteral{7D}{\isacharbraceright}}} refers to \emph{the} context at |
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
386 |
compile-time --- as abstract value. Independently of (local) theory |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
387 |
or proof mode, this always produces a meaningful result. |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
388 |
|
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
389 |
This is probably the most common antiquotation in interactive |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
390 |
experimentation with ML inside Isar. |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
391 |
|
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
392 |
\end{description}% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
393 |
\end{isamarkuptext}% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
394 |
\isamarkuptrue% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
395 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
396 |
\endisatagmlantiq |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
397 |
{\isafoldmlantiq}% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
398 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
399 |
\isadelimmlantiq |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
400 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
401 |
\endisadelimmlantiq |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
402 |
% |
30296 | 403 |
\isamarkupsubsection{Generic contexts \label{sec:generic-context}% |
404 |
} |
|
405 |
\isamarkuptrue% |
|
406 |
% |
|
407 |
\begin{isamarkuptext}% |
|
408 |
A generic context is the disjoint sum of either a theory or proof |
|
409 |
context. Occasionally, this enables uniform treatment of generic |
|
410 |
context data, typically extra-logical information. Operations on |
|
411 |
generic contexts include the usual injections, partial selections, |
|
412 |
and combinators for lifting operations on either component of the |
|
413 |
disjoint sum. |
|
414 |
||
40406 | 415 |
Moreover, there are total operations \isa{theory{\isaliteral{5F}{\isacharunderscore}}of} and \isa{proof{\isaliteral{5F}{\isacharunderscore}}of} to convert a generic context into either kind: a theory |
30296 | 416 |
can always be selected from the sum, while a proof context might |
35001 | 417 |
have to be constructed by an ad-hoc \isa{init} operation, which |
418 |
incurs a small runtime overhead.% |
|
30296 | 419 |
\end{isamarkuptext}% |
420 |
\isamarkuptrue% |
|
421 |
% |
|
422 |
\isadelimmlref |
|
423 |
% |
|
424 |
\endisadelimmlref |
|
425 |
% |
|
426 |
\isatagmlref |
|
427 |
% |
|
428 |
\begin{isamarkuptext}% |
|
429 |
\begin{mldecls} |
|
430 |
\indexdef{}{ML type}{Context.generic}\verb|type Context.generic| \\ |
|
431 |
\indexdef{}{ML}{Context.theory\_of}\verb|Context.theory_of: Context.generic -> theory| \\ |
|
432 |
\indexdef{}{ML}{Context.proof\_of}\verb|Context.proof_of: Context.generic -> Proof.context| \\ |
|
433 |
\end{mldecls} |
|
434 |
||
435 |
\begin{description} |
|
436 |
||
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
437 |
\item Type \verb|Context.generic| is the direct sum of \verb|theory| and \verb|Proof.context|, with the datatype |
30296 | 438 |
constructors \verb|Context.Theory| and \verb|Context.Proof|. |
439 |
||
440 |
\item \verb|Context.theory_of|~\isa{context} always produces a |
|
42361 | 441 |
theory from the generic \isa{context}, using \verb|Proof_Context.theory_of| as required. |
30296 | 442 |
|
443 |
\item \verb|Context.proof_of|~\isa{context} always produces a |
|
42361 | 444 |
proof context from the generic \isa{context}, using \verb|Proof_Context.init_global| as required (note that this re-initializes the |
30296 | 445 |
context data with each invocation). |
446 |
||
447 |
\end{description}% |
|
448 |
\end{isamarkuptext}% |
|
449 |
\isamarkuptrue% |
|
450 |
% |
|
451 |
\endisatagmlref |
|
452 |
{\isafoldmlref}% |
|
453 |
% |
|
454 |
\isadelimmlref |
|
455 |
% |
|
456 |
\endisadelimmlref |
|
457 |
% |
|
458 |
\isamarkupsubsection{Context data \label{sec:context-data}% |
|
459 |
} |
|
460 |
\isamarkuptrue% |
|
461 |
% |
|
462 |
\begin{isamarkuptext}% |
|
33524
a08e6c1cbc04
updated functor Theory_Data, Proof_Data, Generic_Data;
wenzelm
parents:
33174
diff
changeset
|
463 |
The main purpose of theory and proof contexts is to manage |
a08e6c1cbc04
updated functor Theory_Data, Proof_Data, Generic_Data;
wenzelm
parents:
33174
diff
changeset
|
464 |
arbitrary (pure) data. New data types can be declared incrementally |
a08e6c1cbc04
updated functor Theory_Data, Proof_Data, Generic_Data;
wenzelm
parents:
33174
diff
changeset
|
465 |
at compile time. There are separate declaration mechanisms for any |
a08e6c1cbc04
updated functor Theory_Data, Proof_Data, Generic_Data;
wenzelm
parents:
33174
diff
changeset
|
466 |
of the three kinds of contexts: theory, proof, generic. |
30296 | 467 |
|
33524
a08e6c1cbc04
updated functor Theory_Data, Proof_Data, Generic_Data;
wenzelm
parents:
33174
diff
changeset
|
468 |
\paragraph{Theory data} declarations need to implement the following |
a08e6c1cbc04
updated functor Theory_Data, Proof_Data, Generic_Data;
wenzelm
parents:
33174
diff
changeset
|
469 |
SML signature: |
30296 | 470 |
|
471 |
\medskip |
|
472 |
\begin{tabular}{ll} |
|
40406 | 473 |
\isa{{\isaliteral{5C3C747970653E}{\isasymtype}}\ T} & representing type \\ |
474 |
\isa{{\isaliteral{5C3C76616C3E}{\isasymval}}\ empty{\isaliteral{3A}{\isacharcolon}}\ T} & empty default value \\ |
|
475 |
\isa{{\isaliteral{5C3C76616C3E}{\isasymval}}\ extend{\isaliteral{3A}{\isacharcolon}}\ T\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ T} & re-initialize on import \\ |
|
476 |
\isa{{\isaliteral{5C3C76616C3E}{\isasymval}}\ merge{\isaliteral{3A}{\isacharcolon}}\ T\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ T\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ T} & join on import \\ |
|
30296 | 477 |
\end{tabular} |
478 |
\medskip |
|
479 |
||
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
480 |
The \isa{empty} value acts as initial default for \emph{any} |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
481 |
theory that does not declare actual data content; \isa{extend} |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
482 |
is acts like a unitary version of \isa{merge}. |
30296 | 483 |
|
35001 | 484 |
Implementing \isa{merge} can be tricky. The general idea is |
40406 | 485 |
that \isa{merge\ {\isaliteral{28}{\isacharparenleft}}data\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ data\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}{\isaliteral{29}{\isacharparenright}}} inserts those parts of \isa{data\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}} into \isa{data\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}} that are not yet present, while |
35001 | 486 |
keeping the general order of things. The \verb|Library.merge| |
487 |
function on plain lists may serve as canonical template. |
|
488 |
||
489 |
Particularly note that shared parts of the data must not be |
|
490 |
duplicated by naive concatenation, or a theory graph that is like a |
|
491 |
chain of diamonds would cause an exponential blowup! |
|
492 |
||
33524
a08e6c1cbc04
updated functor Theory_Data, Proof_Data, Generic_Data;
wenzelm
parents:
33174
diff
changeset
|
493 |
\paragraph{Proof context data} declarations need to implement the |
a08e6c1cbc04
updated functor Theory_Data, Proof_Data, Generic_Data;
wenzelm
parents:
33174
diff
changeset
|
494 |
following SML signature: |
30296 | 495 |
|
496 |
\medskip |
|
497 |
\begin{tabular}{ll} |
|
40406 | 498 |
\isa{{\isaliteral{5C3C747970653E}{\isasymtype}}\ T} & representing type \\ |
499 |
\isa{{\isaliteral{5C3C76616C3E}{\isasymval}}\ init{\isaliteral{3A}{\isacharcolon}}\ theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ T} & produce initial value \\ |
|
30296 | 500 |
\end{tabular} |
501 |
\medskip |
|
502 |
||
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
503 |
The \isa{init} operation is supposed to produce a pure value |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
504 |
from the given background theory and should be somehow |
35001 | 505 |
``immediate''. Whenever a proof context is initialized, which |
506 |
happens frequently, the the system invokes the \isa{init} |
|
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
507 |
operation of \emph{all} theory data slots ever declared. This also |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
508 |
means that one needs to be economic about the total number of proof |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
509 |
data declarations in the system, i.e.\ each ML module should declare |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
510 |
at most one, sometimes two data slots for its internal use. |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
511 |
Repeated data declarations to simulate a record type should be |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
512 |
avoided! |
30296 | 513 |
|
514 |
\paragraph{Generic data} provides a hybrid interface for both theory |
|
33524
a08e6c1cbc04
updated functor Theory_Data, Proof_Data, Generic_Data;
wenzelm
parents:
33174
diff
changeset
|
515 |
and proof data. The \isa{init} operation for proof contexts is |
a08e6c1cbc04
updated functor Theory_Data, Proof_Data, Generic_Data;
wenzelm
parents:
33174
diff
changeset
|
516 |
predefined to select the current data value from the background |
a08e6c1cbc04
updated functor Theory_Data, Proof_Data, Generic_Data;
wenzelm
parents:
33174
diff
changeset
|
517 |
theory. |
30296 | 518 |
|
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
519 |
\bigskip Any of the above data declarations over type \isa{T} |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
520 |
result in an ML structure with the following signature: |
30296 | 521 |
|
522 |
\medskip |
|
523 |
\begin{tabular}{ll} |
|
40406 | 524 |
\isa{get{\isaliteral{3A}{\isacharcolon}}\ context\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ T} \\ |
525 |
\isa{put{\isaliteral{3A}{\isacharcolon}}\ T\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ context\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ context} \\ |
|
526 |
\isa{map{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{28}{\isacharparenleft}}T\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ T{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ context\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ context} \\ |
|
30296 | 527 |
\end{tabular} |
528 |
\medskip |
|
529 |
||
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
530 |
These other operations provide exclusive access for the particular |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
531 |
kind of context (theory, proof, or generic context). This interface |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
532 |
observes the ML discipline for types and scopes: there is no other |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
533 |
way to access the corresponding data slot of a context. By keeping |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
534 |
these operations private, an Isabelle/ML module may maintain |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
535 |
abstract values authentically.% |
30296 | 536 |
\end{isamarkuptext}% |
537 |
\isamarkuptrue% |
|
538 |
% |
|
539 |
\isadelimmlref |
|
540 |
% |
|
541 |
\endisadelimmlref |
|
542 |
% |
|
543 |
\isatagmlref |
|
544 |
% |
|
545 |
\begin{isamarkuptext}% |
|
546 |
\begin{mldecls} |
|
33524
a08e6c1cbc04
updated functor Theory_Data, Proof_Data, Generic_Data;
wenzelm
parents:
33174
diff
changeset
|
547 |
\indexdef{}{ML functor}{Theory\_Data}\verb|functor Theory_Data| \\ |
a08e6c1cbc04
updated functor Theory_Data, Proof_Data, Generic_Data;
wenzelm
parents:
33174
diff
changeset
|
548 |
\indexdef{}{ML functor}{Proof\_Data}\verb|functor Proof_Data| \\ |
a08e6c1cbc04
updated functor Theory_Data, Proof_Data, Generic_Data;
wenzelm
parents:
33174
diff
changeset
|
549 |
\indexdef{}{ML functor}{Generic\_Data}\verb|functor Generic_Data| \\ |
30296 | 550 |
\end{mldecls} |
551 |
||
552 |
\begin{description} |
|
553 |
||
40406 | 554 |
\item \verb|Theory_Data|\isa{{\isaliteral{28}{\isacharparenleft}}spec{\isaliteral{29}{\isacharparenright}}} declares data for |
30296 | 555 |
type \verb|theory| according to the specification provided as |
556 |
argument structure. The resulting structure provides data init and |
|
557 |
access operations as described above. |
|
558 |
||
40406 | 559 |
\item \verb|Proof_Data|\isa{{\isaliteral{28}{\isacharparenleft}}spec{\isaliteral{29}{\isacharparenright}}} is analogous to |
33524
a08e6c1cbc04
updated functor Theory_Data, Proof_Data, Generic_Data;
wenzelm
parents:
33174
diff
changeset
|
560 |
\verb|Theory_Data| for type \verb|Proof.context|. |
30296 | 561 |
|
40406 | 562 |
\item \verb|Generic_Data|\isa{{\isaliteral{28}{\isacharparenleft}}spec{\isaliteral{29}{\isacharparenright}}} is analogous to |
33524
a08e6c1cbc04
updated functor Theory_Data, Proof_Data, Generic_Data;
wenzelm
parents:
33174
diff
changeset
|
563 |
\verb|Theory_Data| for type \verb|Context.generic|. |
30296 | 564 |
|
565 |
\end{description}% |
|
566 |
\end{isamarkuptext}% |
|
567 |
\isamarkuptrue% |
|
568 |
% |
|
569 |
\endisatagmlref |
|
570 |
{\isafoldmlref}% |
|
571 |
% |
|
572 |
\isadelimmlref |
|
573 |
% |
|
574 |
\endisadelimmlref |
|
575 |
% |
|
35001 | 576 |
\isadelimmlex |
577 |
% |
|
578 |
\endisadelimmlex |
|
579 |
% |
|
580 |
\isatagmlex |
|
581 |
% |
|
582 |
\begin{isamarkuptext}% |
|
583 |
The following artificial example demonstrates theory |
|
584 |
data: we maintain a set of terms that are supposed to be wellformed |
|
585 |
wrt.\ the enclosing theory. The public interface is as follows:% |
|
586 |
\end{isamarkuptext}% |
|
587 |
\isamarkuptrue% |
|
588 |
% |
|
589 |
\endisatagmlex |
|
590 |
{\isafoldmlex}% |
|
591 |
% |
|
592 |
\isadelimmlex |
|
593 |
% |
|
594 |
\endisadelimmlex |
|
595 |
% |
|
596 |
\isadelimML |
|
597 |
% |
|
598 |
\endisadelimML |
|
599 |
% |
|
600 |
\isatagML |
|
601 |
\isacommand{ML}\isamarkupfalse% |
|
40406 | 602 |
\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline |
603 |
\ \ signature\ WELLFORMED{\isaliteral{5F}{\isacharunderscore}}TERMS\ {\isaliteral{3D}{\isacharequal}}\isanewline |
|
35001 | 604 |
\ \ sig\isanewline |
40406 | 605 |
\ \ \ \ val\ get{\isaliteral{3A}{\isacharcolon}}\ theory\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ term\ list\isanewline |
606 |
\ \ \ \ val\ add{\isaliteral{3A}{\isacharcolon}}\ term\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ theory\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ theory\isanewline |
|
607 |
\ \ end{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
|
608 |
{\isaliteral{2A7D}{\isacharverbatimclose}}% |
|
35001 | 609 |
\endisatagML |
610 |
{\isafoldML}% |
|
611 |
% |
|
612 |
\isadelimML |
|
613 |
% |
|
614 |
\endisadelimML |
|
615 |
% |
|
616 |
\begin{isamarkuptext}% |
|
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
617 |
The implementation uses private theory data internally, and |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
618 |
only exposes an operation that involves explicit argument checking |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
619 |
wrt.\ the given theory.% |
35001 | 620 |
\end{isamarkuptext}% |
621 |
\isamarkuptrue% |
|
622 |
% |
|
623 |
\isadelimML |
|
624 |
% |
|
625 |
\endisadelimML |
|
626 |
% |
|
627 |
\isatagML |
|
628 |
\isacommand{ML}\isamarkupfalse% |
|
40406 | 629 |
\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline |
630 |
\ \ structure\ Wellformed{\isaliteral{5F}{\isacharunderscore}}Terms{\isaliteral{3A}{\isacharcolon}}\ WELLFORMED{\isaliteral{5F}{\isacharunderscore}}TERMS\ {\isaliteral{3D}{\isacharequal}}\isanewline |
|
35001 | 631 |
\ \ struct\isanewline |
632 |
\isanewline |
|
40406 | 633 |
\ \ structure\ Terms\ {\isaliteral{3D}{\isacharequal}}\ Theory{\isaliteral{5F}{\isacharunderscore}}Data\isanewline |
634 |
\ \ {\isaliteral{28}{\isacharparenleft}}\isanewline |
|
635 |
\ \ \ \ type\ T\ {\isaliteral{3D}{\isacharequal}}\ term\ Ord{\isaliteral{5F}{\isacharunderscore}}List{\isaliteral{2E}{\isachardot}}T{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
|
636 |
\ \ \ \ val\ empty\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
|
637 |
\ \ \ \ val\ extend\ {\isaliteral{3D}{\isacharequal}}\ I{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
|
638 |
\ \ \ \ fun\ merge\ {\isaliteral{28}{\isacharparenleft}}ts{\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ ts{\isadigit{2}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\isanewline |
|
639 |
\ \ \ \ \ \ Ord{\isaliteral{5F}{\isacharunderscore}}List{\isaliteral{2E}{\isachardot}}union\ Term{\isaliteral{5F}{\isacharunderscore}}Ord{\isaliteral{2E}{\isachardot}}fast{\isaliteral{5F}{\isacharunderscore}}term{\isaliteral{5F}{\isacharunderscore}}ord\ ts{\isadigit{1}}\ ts{\isadigit{2}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
|
640 |
\ \ {\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
|
35001 | 641 |
\isanewline |
40406 | 642 |
\ \ val\ get\ {\isaliteral{3D}{\isacharequal}}\ Terms{\isaliteral{2E}{\isachardot}}get{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
35001 | 643 |
\isanewline |
40406 | 644 |
\ \ fun\ add\ raw{\isaliteral{5F}{\isacharunderscore}}t\ thy\ {\isaliteral{3D}{\isacharequal}}\isanewline |
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
645 |
\ \ \ \ let\isanewline |
40406 | 646 |
\ \ \ \ \ \ val\ t\ {\isaliteral{3D}{\isacharequal}}\ Sign{\isaliteral{2E}{\isachardot}}cert{\isaliteral{5F}{\isacharunderscore}}term\ thy\ raw{\isaliteral{5F}{\isacharunderscore}}t{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
647 |
\ \ \ \ in\isanewline |
40406 | 648 |
\ \ \ \ \ \ Terms{\isaliteral{2E}{\isachardot}}map\ {\isaliteral{28}{\isacharparenleft}}Ord{\isaliteral{5F}{\isacharunderscore}}List{\isaliteral{2E}{\isachardot}}insert\ Term{\isaliteral{5F}{\isacharunderscore}}Ord{\isaliteral{2E}{\isachardot}}fast{\isaliteral{5F}{\isacharunderscore}}term{\isaliteral{5F}{\isacharunderscore}}ord\ t{\isaliteral{29}{\isacharparenright}}\ thy\isanewline |
649 |
\ \ \ \ end{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
|
35001 | 650 |
\isanewline |
40406 | 651 |
\ \ end{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
652 |
{\isaliteral{2A7D}{\isacharverbatimclose}}% |
|
35001 | 653 |
\endisatagML |
654 |
{\isafoldML}% |
|
655 |
% |
|
656 |
\isadelimML |
|
657 |
% |
|
658 |
\endisadelimML |
|
659 |
% |
|
660 |
\begin{isamarkuptext}% |
|
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
661 |
Type \verb|term Ord_List.T| is used for reasonably |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
662 |
efficient representation of a set of terms: all operations are |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
663 |
linear in the number of stored elements. Here we assume that users |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
664 |
of this module do not care about the declaration order, since that |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
665 |
data structure forces its own arrangement of elements. |
35001 | 666 |
|
667 |
Observe how the \verb|merge| operation joins the data slots of |
|
39688 | 668 |
the two constituents: \verb|Ord_List.union| prevents duplication of |
35001 | 669 |
common data from different branches, thus avoiding the danger of |
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
670 |
exponential blowup. Plain list append etc.\ must never be used for |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
671 |
theory data merges! |
35001 | 672 |
|
673 |
\medskip Our intended invariant is achieved as follows: |
|
674 |
\begin{enumerate} |
|
675 |
||
676 |
\item \verb|Wellformed_Terms.add| only admits terms that have passed |
|
677 |
the \verb|Sign.cert_term| check of the given theory at that point. |
|
678 |
||
679 |
\item Wellformedness in the sense of \verb|Sign.cert_term| is |
|
680 |
monotonic wrt.\ the sub-theory relation. So our data can move |
|
681 |
upwards in the hierarchy (via extension or merges), and maintain |
|
682 |
wellformedness without further checks. |
|
683 |
||
684 |
\end{enumerate} |
|
685 |
||
686 |
Note that all basic operations of the inference kernel (which |
|
687 |
includes \verb|Sign.cert_term|) observe this monotonicity principle, |
|
688 |
but other user-space tools don't. For example, fully-featured |
|
689 |
type-inference via \verb|Syntax.check_term| (cf.\ |
|
690 |
\secref{sec:term-check}) is not necessarily monotonic wrt.\ the |
|
691 |
background theory, since constraints of term constants can be |
|
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
692 |
modified by later declarations, for example. |
35001 | 693 |
|
694 |
In most cases, user-space context data does not have to take such |
|
695 |
invariants too seriously. The situation is different in the |
|
696 |
implementation of the inference kernel itself, which uses the very |
|
697 |
same data mechanisms for types, constants, axioms etc.% |
|
698 |
\end{isamarkuptext}% |
|
699 |
\isamarkuptrue% |
|
700 |
% |
|
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
701 |
\isamarkupsubsection{Configuration options \label{sec:config-options}% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
702 |
} |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
703 |
\isamarkuptrue% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
704 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
705 |
\begin{isamarkuptext}% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
706 |
A \emph{configuration option} is a named optional value of |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
707 |
some basic type (Boolean, integer, string) that is stored in the |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
708 |
context. It is a simple application of general context data |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
709 |
(\secref{sec:context-data}) that is sufficiently common to justify |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
710 |
customized setup, which includes some concrete declarations for |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
711 |
end-users using existing notation for attributes (cf.\ |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
712 |
\secref{sec:attributes}). |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
713 |
|
40406 | 714 |
For example, the predefined configuration option \hyperlink{attribute.show-types}{\mbox{\isa{show{\isaliteral{5F}{\isacharunderscore}}types}}} controls output of explicit type constraints for |
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
715 |
variables in printed terms (cf.\ \secref{sec:read-print}). Its |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
716 |
value can be modified within Isar text like this:% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
717 |
\end{isamarkuptext}% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
718 |
\isamarkuptrue% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
719 |
\isacommand{declare}\isamarkupfalse% |
40406 | 720 |
\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5B}{\isacharbrackleft}}show{\isaliteral{5F}{\isacharunderscore}}types\ {\isaliteral{3D}{\isacharequal}}\ false{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{5D}{\isacharbrackright}}\isanewline |
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
721 |
\ \ % |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
722 |
\isamarkupcmt{declaration within (local) theory context% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
723 |
} |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
724 |
\isanewline |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
725 |
\isanewline |
40964 | 726 |
\isacommand{notepad}\isamarkupfalse% |
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
727 |
\isanewline |
40964 | 728 |
\isakeyword{begin}\isanewline |
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
729 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
730 |
\isadelimproof |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
731 |
\ \ % |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
732 |
\endisadelimproof |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
733 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
734 |
\isatagproof |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
735 |
\isacommand{note}\isamarkupfalse% |
40406 | 736 |
\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5B}{\isacharbrackleft}}show{\isaliteral{5F}{\isacharunderscore}}types\ {\isaliteral{3D}{\isacharequal}}\ true{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{5D}{\isacharbrackright}}\isanewline |
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
737 |
\ \ \ \ % |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
738 |
\isamarkupcmt{declaration within proof (forward mode)% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
739 |
} |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
740 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
741 |
\endisatagproof |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
742 |
{\isafoldproof}% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
743 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
744 |
\isadelimproof |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
745 |
\isanewline |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
746 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
747 |
\endisadelimproof |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
748 |
\ \ \isacommand{term}\isamarkupfalse% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
749 |
\ x\isanewline |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
750 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
751 |
\isadelimproof |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
752 |
\isanewline |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
753 |
\ \ % |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
754 |
\endisadelimproof |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
755 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
756 |
\isatagproof |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
757 |
\isacommand{have}\isamarkupfalse% |
40406 | 758 |
\ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{3D}{\isacharequal}}\ x{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
759 |
\ \ \ \ \isacommand{using}\isamarkupfalse% |
40406 | 760 |
\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5B}{\isacharbrackleft}}show{\isaliteral{5F}{\isacharunderscore}}types\ {\isaliteral{3D}{\isacharequal}}\ false{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{5D}{\isacharbrackright}}\isanewline |
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
761 |
\ \ \ \ \ \ % |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
762 |
\isamarkupcmt{declaration within proof (backward mode)% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
763 |
} |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
764 |
\isanewline |
40406 | 765 |
\ \ \ \ \isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}\isamarkupfalse% |
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
766 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
767 |
\endisatagproof |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
768 |
{\isafoldproof}% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
769 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
770 |
\isadelimproof |
40964 | 771 |
\isanewline |
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
772 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
773 |
\endisadelimproof |
40964 | 774 |
\isacommand{end}\isamarkupfalse% |
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
775 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
776 |
\begin{isamarkuptext}% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
777 |
Configuration options that are not set explicitly hold a |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
778 |
default value that can depend on the application context. This |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
779 |
allows to retrieve the value from another slot within the context, |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
780 |
or fall back on a global preference mechanism, for example. |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
781 |
|
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
782 |
The operations to declare configuration options and get/map their |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
783 |
values are modeled as direct replacements for historic global |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
784 |
references, only that the context is made explicit. This allows |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
785 |
easy configuration of tools, without relying on the execution order |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
786 |
as required for old-style mutable references.% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
787 |
\end{isamarkuptext}% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
788 |
\isamarkuptrue% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
789 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
790 |
\isadelimmlref |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
791 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
792 |
\endisadelimmlref |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
793 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
794 |
\isatagmlref |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
795 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
796 |
\begin{isamarkuptext}% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
797 |
\begin{mldecls} |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
798 |
\indexdef{}{ML}{Config.get}\verb|Config.get: Proof.context -> 'a Config.T -> 'a| \\ |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
799 |
\indexdef{}{ML}{Config.map}\verb|Config.map: 'a Config.T -> ('a -> 'a) -> Proof.context -> Proof.context| \\ |
42616
92715b528e78
added Attrib.setup_config_XXX conveniences, with implicit setup of the background theory;
wenzelm
parents:
42510
diff
changeset
|
800 |
\indexdef{}{ML}{Attrib.setup\_config\_bool}\verb|Attrib.setup_config_bool: binding -> (Context.generic -> bool) ->|\isasep\isanewline% |
92715b528e78
added Attrib.setup_config_XXX conveniences, with implicit setup of the background theory;
wenzelm
parents:
42510
diff
changeset
|
801 |
\verb| bool Config.T| \\ |
92715b528e78
added Attrib.setup_config_XXX conveniences, with implicit setup of the background theory;
wenzelm
parents:
42510
diff
changeset
|
802 |
\indexdef{}{ML}{Attrib.setup\_config\_int}\verb|Attrib.setup_config_int: binding -> (Context.generic -> int) ->|\isasep\isanewline% |
92715b528e78
added Attrib.setup_config_XXX conveniences, with implicit setup of the background theory;
wenzelm
parents:
42510
diff
changeset
|
803 |
\verb| int Config.T| \\ |
92715b528e78
added Attrib.setup_config_XXX conveniences, with implicit setup of the background theory;
wenzelm
parents:
42510
diff
changeset
|
804 |
\indexdef{}{ML}{Attrib.setup\_config\_real}\verb|Attrib.setup_config_real: binding -> (Context.generic -> real) ->|\isasep\isanewline% |
92715b528e78
added Attrib.setup_config_XXX conveniences, with implicit setup of the background theory;
wenzelm
parents:
42510
diff
changeset
|
805 |
\verb| real Config.T| \\ |
92715b528e78
added Attrib.setup_config_XXX conveniences, with implicit setup of the background theory;
wenzelm
parents:
42510
diff
changeset
|
806 |
\indexdef{}{ML}{Attrib.setup\_config\_string}\verb|Attrib.setup_config_string: binding -> (Context.generic -> string) ->|\isasep\isanewline% |
92715b528e78
added Attrib.setup_config_XXX conveniences, with implicit setup of the background theory;
wenzelm
parents:
42510
diff
changeset
|
807 |
\verb| string Config.T| \\ |
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
808 |
\end{mldecls} |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
809 |
|
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
810 |
\begin{description} |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
811 |
|
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
812 |
\item \verb|Config.get|~\isa{ctxt\ config} gets the value of |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
813 |
\isa{config} in the given context. |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
814 |
|
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
815 |
\item \verb|Config.map|~\isa{config\ f\ ctxt} updates the context |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
816 |
by updating the value of \isa{config}. |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
817 |
|
42616
92715b528e78
added Attrib.setup_config_XXX conveniences, with implicit setup of the background theory;
wenzelm
parents:
42510
diff
changeset
|
818 |
\item \isa{config\ {\isaliteral{3D}{\isacharequal}}}~\verb|Attrib.setup_config_bool|~\isa{name\ default} creates a named configuration option of type \verb|bool|, with the given \isa{default} depending on the application |
92715b528e78
added Attrib.setup_config_XXX conveniences, with implicit setup of the background theory;
wenzelm
parents:
42510
diff
changeset
|
819 |
context. The resulting \isa{config} can be used to get/map its |
92715b528e78
added Attrib.setup_config_XXX conveniences, with implicit setup of the background theory;
wenzelm
parents:
42510
diff
changeset
|
820 |
value in a given context. There is an implicit update of the |
92715b528e78
added Attrib.setup_config_XXX conveniences, with implicit setup of the background theory;
wenzelm
parents:
42510
diff
changeset
|
821 |
background theory that registers the option as attribute with some |
92715b528e78
added Attrib.setup_config_XXX conveniences, with implicit setup of the background theory;
wenzelm
parents:
42510
diff
changeset
|
822 |
concrete syntax. |
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
823 |
|
40291 | 824 |
\item \verb|Attrib.config_int|, \verb|Attrib.config_real|, and \verb|Attrib.config_string| work like \verb|Attrib.config_bool|, but for |
825 |
types \verb|int| and \verb|string|, respectively. |
|
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
826 |
|
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
827 |
\end{description}% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
828 |
\end{isamarkuptext}% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
829 |
\isamarkuptrue% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
830 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
831 |
\endisatagmlref |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
832 |
{\isafoldmlref}% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
833 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
834 |
\isadelimmlref |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
835 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
836 |
\endisadelimmlref |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
837 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
838 |
\isadelimmlex |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
839 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
840 |
\endisadelimmlex |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
841 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
842 |
\isatagmlex |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
843 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
844 |
\begin{isamarkuptext}% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
845 |
The following example shows how to declare and use a |
40406 | 846 |
Boolean configuration option called \isa{my{\isaliteral{5F}{\isacharunderscore}}flag} with constant |
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
847 |
default value \verb|false|.% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
848 |
\end{isamarkuptext}% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
849 |
\isamarkuptrue% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
850 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
851 |
\endisatagmlex |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
852 |
{\isafoldmlex}% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
853 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
854 |
\isadelimmlex |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
855 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
856 |
\endisadelimmlex |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
857 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
858 |
\isadelimML |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
859 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
860 |
\endisadelimML |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
861 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
862 |
\isatagML |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
863 |
\isacommand{ML}\isamarkupfalse% |
40406 | 864 |
\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline |
42616
92715b528e78
added Attrib.setup_config_XXX conveniences, with implicit setup of the background theory;
wenzelm
parents:
42510
diff
changeset
|
865 |
\ \ val\ my{\isaliteral{5F}{\isacharunderscore}}flag\ {\isaliteral{3D}{\isacharequal}}\isanewline |
92715b528e78
added Attrib.setup_config_XXX conveniences, with implicit setup of the background theory;
wenzelm
parents:
42510
diff
changeset
|
866 |
\ \ \ \ Attrib{\isaliteral{2E}{\isachardot}}setup{\isaliteral{5F}{\isacharunderscore}}config{\isaliteral{5F}{\isacharunderscore}}bool\ % |
92715b528e78
added Attrib.setup_config_XXX conveniences, with implicit setup of the background theory;
wenzelm
parents:
42510
diff
changeset
|
867 |
\isaantiq |
92715b528e78
added Attrib.setup_config_XXX conveniences, with implicit setup of the background theory;
wenzelm
parents:
42510
diff
changeset
|
868 |
binding\ my{\isaliteral{5F}{\isacharunderscore}}flag{}% |
92715b528e78
added Attrib.setup_config_XXX conveniences, with implicit setup of the background theory;
wenzelm
parents:
42510
diff
changeset
|
869 |
\endisaantiq |
92715b528e78
added Attrib.setup_config_XXX conveniences, with implicit setup of the background theory;
wenzelm
parents:
42510
diff
changeset
|
870 |
\ {\isaliteral{28}{\isacharparenleft}}K\ false{\isaliteral{29}{\isacharparenright}}\isanewline |
92715b528e78
added Attrib.setup_config_XXX conveniences, with implicit setup of the background theory;
wenzelm
parents:
42510
diff
changeset
|
871 |
{\isaliteral{2A7D}{\isacharverbatimclose}}% |
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
872 |
\endisatagML |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
873 |
{\isafoldML}% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
874 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
875 |
\isadelimML |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
876 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
877 |
\endisadelimML |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
878 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
879 |
\begin{isamarkuptext}% |
40406 | 880 |
Now the user can refer to \hyperlink{attribute.my-flag}{\mbox{\isa{my{\isaliteral{5F}{\isacharunderscore}}flag}}} in |
40126 | 881 |
declarations, while ML tools can retrieve the current value from the |
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
882 |
context via \verb|Config.get|.% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
883 |
\end{isamarkuptext}% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
884 |
\isamarkuptrue% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
885 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
886 |
\isadelimML |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
887 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
888 |
\endisadelimML |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
889 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
890 |
\isatagML |
40406 | 891 |
\isacommand{ML{\isaliteral{5F}{\isacharunderscore}}val}\isamarkupfalse% |
892 |
\ {\isaliteral{7B2A}{\isacharverbatimopen}}\ % |
|
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
893 |
\isaantiq |
40406 | 894 |
assert{}% |
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
895 |
\endisaantiq |
40406 | 896 |
\ {\isaliteral{28}{\isacharparenleft}}Config{\isaliteral{2E}{\isachardot}}get\ % |
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
897 |
\isaantiq |
40406 | 898 |
context{}% |
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
899 |
\endisaantiq |
40406 | 900 |
\ my{\isaliteral{5F}{\isacharunderscore}}flag\ {\isaliteral{3D}{\isacharequal}}\ false{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{2A7D}{\isacharverbatimclose}}% |
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
901 |
\endisatagML |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
902 |
{\isafoldML}% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
903 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
904 |
\isadelimML |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
905 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
906 |
\endisadelimML |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
907 |
\isanewline |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
908 |
\isanewline |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
909 |
\isacommand{declare}\isamarkupfalse% |
40406 | 910 |
\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5B}{\isacharbrackleft}}my{\isaliteral{5F}{\isacharunderscore}}flag\ {\isaliteral{3D}{\isacharequal}}\ true{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{5D}{\isacharbrackright}}\isanewline |
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
911 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
912 |
\isadelimML |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
913 |
\isanewline |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
914 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
915 |
\endisadelimML |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
916 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
917 |
\isatagML |
40406 | 918 |
\isacommand{ML{\isaliteral{5F}{\isacharunderscore}}val}\isamarkupfalse% |
919 |
\ {\isaliteral{7B2A}{\isacharverbatimopen}}\ % |
|
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
920 |
\isaantiq |
40406 | 921 |
assert{}% |
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
922 |
\endisaantiq |
40406 | 923 |
\ {\isaliteral{28}{\isacharparenleft}}Config{\isaliteral{2E}{\isachardot}}get\ % |
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
924 |
\isaantiq |
40406 | 925 |
context{}% |
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
926 |
\endisaantiq |
40406 | 927 |
\ my{\isaliteral{5F}{\isacharunderscore}}flag\ {\isaliteral{3D}{\isacharequal}}\ true{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{2A7D}{\isacharverbatimclose}}% |
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
928 |
\endisatagML |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
929 |
{\isafoldML}% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
930 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
931 |
\isadelimML |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
932 |
\isanewline |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
933 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
934 |
\endisadelimML |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
935 |
\isanewline |
40964 | 936 |
\isacommand{notepad}\isamarkupfalse% |
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
937 |
\isanewline |
40964 | 938 |
\isakeyword{begin}\isanewline |
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
939 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
940 |
\isadelimproof |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
941 |
\ \ % |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
942 |
\endisadelimproof |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
943 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
944 |
\isatagproof |
40406 | 945 |
\isacommand{{\isaliteral{7B}{\isacharbraceleft}}}\isamarkupfalse% |
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
946 |
\isanewline |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
947 |
\ \ \ \ \isacommand{note}\isamarkupfalse% |
40406 | 948 |
\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5B}{\isacharbrackleft}}my{\isaliteral{5F}{\isacharunderscore}}flag\ {\isaliteral{3D}{\isacharequal}}\ false{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{5D}{\isacharbrackright}}% |
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
949 |
\endisatagproof |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
950 |
{\isafoldproof}% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
951 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
952 |
\isadelimproof |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
953 |
\isanewline |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
954 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
955 |
\endisadelimproof |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
956 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
957 |
\isadelimML |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
958 |
\ \ \ \ % |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
959 |
\endisadelimML |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
960 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
961 |
\isatagML |
40406 | 962 |
\isacommand{ML{\isaliteral{5F}{\isacharunderscore}}val}\isamarkupfalse% |
963 |
\ {\isaliteral{7B2A}{\isacharverbatimopen}}\ % |
|
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
964 |
\isaantiq |
40406 | 965 |
assert{}% |
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
966 |
\endisaantiq |
40406 | 967 |
\ {\isaliteral{28}{\isacharparenleft}}Config{\isaliteral{2E}{\isachardot}}get\ % |
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
968 |
\isaantiq |
40406 | 969 |
context{}% |
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
970 |
\endisaantiq |
40406 | 971 |
\ my{\isaliteral{5F}{\isacharunderscore}}flag\ {\isaliteral{3D}{\isacharequal}}\ false{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{2A7D}{\isacharverbatimclose}}% |
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
972 |
\endisatagML |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
973 |
{\isafoldML}% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
974 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
975 |
\isadelimML |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
976 |
\isanewline |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
977 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
978 |
\endisadelimML |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
979 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
980 |
\isadelimproof |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
981 |
\ \ % |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
982 |
\endisadelimproof |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
983 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
984 |
\isatagproof |
40406 | 985 |
\isacommand{{\isaliteral{7D}{\isacharbraceright}}}\isamarkupfalse% |
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
986 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
987 |
\endisatagproof |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
988 |
{\isafoldproof}% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
989 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
990 |
\isadelimproof |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
991 |
\isanewline |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
992 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
993 |
\endisadelimproof |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
994 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
995 |
\isadelimML |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
996 |
\ \ % |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
997 |
\endisadelimML |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
998 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
999 |
\isatagML |
40406 | 1000 |
\isacommand{ML{\isaliteral{5F}{\isacharunderscore}}val}\isamarkupfalse% |
1001 |
\ {\isaliteral{7B2A}{\isacharverbatimopen}}\ % |
|
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1002 |
\isaantiq |
40406 | 1003 |
assert{}% |
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1004 |
\endisaantiq |
40406 | 1005 |
\ {\isaliteral{28}{\isacharparenleft}}Config{\isaliteral{2E}{\isachardot}}get\ % |
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1006 |
\isaantiq |
40406 | 1007 |
context{}% |
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1008 |
\endisaantiq |
40406 | 1009 |
\ my{\isaliteral{5F}{\isacharunderscore}}flag\ {\isaliteral{3D}{\isacharequal}}\ true{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{2A7D}{\isacharverbatimclose}}% |
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1010 |
\endisatagML |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1011 |
{\isafoldML}% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1012 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1013 |
\isadelimML |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1014 |
\isanewline |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1015 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1016 |
\endisadelimML |
40964 | 1017 |
\isacommand{end}\isamarkupfalse% |
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1018 |
% |
40291 | 1019 |
\begin{isamarkuptext}% |
1020 |
Here is another example involving ML type \verb|real| |
|
1021 |
(floating-point numbers).% |
|
1022 |
\end{isamarkuptext}% |
|
1023 |
\isamarkuptrue% |
|
1024 |
% |
|
1025 |
\isadelimML |
|
1026 |
% |
|
1027 |
\endisadelimML |
|
1028 |
% |
|
1029 |
\isatagML |
|
1030 |
\isacommand{ML}\isamarkupfalse% |
|
40406 | 1031 |
\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline |
42616
92715b528e78
added Attrib.setup_config_XXX conveniences, with implicit setup of the background theory;
wenzelm
parents:
42510
diff
changeset
|
1032 |
\ \ val\ airspeed{\isaliteral{5F}{\isacharunderscore}}velocity\ {\isaliteral{3D}{\isacharequal}}\isanewline |
92715b528e78
added Attrib.setup_config_XXX conveniences, with implicit setup of the background theory;
wenzelm
parents:
42510
diff
changeset
|
1033 |
\ \ \ \ Attrib{\isaliteral{2E}{\isachardot}}setup{\isaliteral{5F}{\isacharunderscore}}config{\isaliteral{5F}{\isacharunderscore}}real\ % |
92715b528e78
added Attrib.setup_config_XXX conveniences, with implicit setup of the background theory;
wenzelm
parents:
42510
diff
changeset
|
1034 |
\isaantiq |
92715b528e78
added Attrib.setup_config_XXX conveniences, with implicit setup of the background theory;
wenzelm
parents:
42510
diff
changeset
|
1035 |
binding\ airspeed{\isaliteral{5F}{\isacharunderscore}}velocity{}% |
92715b528e78
added Attrib.setup_config_XXX conveniences, with implicit setup of the background theory;
wenzelm
parents:
42510
diff
changeset
|
1036 |
\endisaantiq |
92715b528e78
added Attrib.setup_config_XXX conveniences, with implicit setup of the background theory;
wenzelm
parents:
42510
diff
changeset
|
1037 |
\ {\isaliteral{28}{\isacharparenleft}}K\ {\isadigit{0}}{\isaliteral{2E}{\isachardot}}{\isadigit{0}}{\isaliteral{29}{\isacharparenright}}\isanewline |
92715b528e78
added Attrib.setup_config_XXX conveniences, with implicit setup of the background theory;
wenzelm
parents:
42510
diff
changeset
|
1038 |
{\isaliteral{2A7D}{\isacharverbatimclose}}% |
40291 | 1039 |
\endisatagML |
1040 |
{\isafoldML}% |
|
1041 |
% |
|
1042 |
\isadelimML |
|
1043 |
% |
|
1044 |
\endisadelimML |
|
1045 |
\isanewline |
|
1046 |
\isanewline |
|
1047 |
\isacommand{declare}\isamarkupfalse% |
|
40406 | 1048 |
\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5B}{\isacharbrackleft}}airspeed{\isaliteral{5F}{\isacharunderscore}}velocity\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{1}}{\isadigit{0}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{5D}{\isacharbrackright}}\isanewline |
40296 | 1049 |
\isacommand{declare}\isamarkupfalse% |
40406 | 1050 |
\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5B}{\isacharbrackleft}}airspeed{\isaliteral{5F}{\isacharunderscore}}velocity\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{9}}{\isaliteral{2E}{\isachardot}}{\isadigit{9}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{5D}{\isacharbrackright}}% |
30296 | 1051 |
\isamarkupsection{Names \label{sec:names}% |
1052 |
} |
|
1053 |
\isamarkuptrue% |
|
1054 |
% |
|
1055 |
\begin{isamarkuptext}% |
|
1056 |
In principle, a name is just a string, but there are various |
|
35001 | 1057 |
conventions for representing additional structure. For example, |
40406 | 1058 |
``\isa{Foo{\isaliteral{2E}{\isachardot}}bar{\isaliteral{2E}{\isachardot}}baz}'' is considered as a long name consisting of |
1059 |
qualifier \isa{Foo{\isaliteral{2E}{\isachardot}}bar} and base name \isa{baz}. The |
|
35001 | 1060 |
individual constituents of a name may have further substructure, |
1061 |
e.g.\ the string ``\verb,\,\verb,<alpha>,'' encodes as a single |
|
1062 |
symbol. |
|
1063 |
||
1064 |
\medskip Subsequently, we shall introduce specific categories of |
|
1065 |
names. Roughly speaking these correspond to logical entities as |
|
1066 |
follows: |
|
1067 |
\begin{itemize} |
|
1068 |
||
1069 |
\item Basic names (\secref{sec:basic-name}): free and bound |
|
1070 |
variables. |
|
1071 |
||
1072 |
\item Indexed names (\secref{sec:indexname}): schematic variables. |
|
1073 |
||
1074 |
\item Long names (\secref{sec:long-name}): constants of any kind |
|
1075 |
(type constructors, term constants, other concepts defined in user |
|
1076 |
space). Such entities are typically managed via name spaces |
|
1077 |
(\secref{sec:name-space}). |
|
1078 |
||
1079 |
\end{itemize}% |
|
30296 | 1080 |
\end{isamarkuptext}% |
1081 |
\isamarkuptrue% |
|
1082 |
% |
|
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1083 |
\isamarkupsubsection{Strings of symbols \label{sec:symbols}% |
30296 | 1084 |
} |
1085 |
\isamarkuptrue% |
|
1086 |
% |
|
1087 |
\begin{isamarkuptext}% |
|
35001 | 1088 |
A \emph{symbol} constitutes the smallest textual unit in |
1089 |
Isabelle --- raw ML characters are normally not encountered at all! |
|
1090 |
Isabelle strings consist of a sequence of symbols, represented as a |
|
1091 |
packed string or an exploded list of strings. Each symbol is in |
|
1092 |
itself a small string, which has either one of the following forms: |
|
30296 | 1093 |
|
1094 |
\begin{enumerate} |
|
1095 |
||
37533
d775bd70f571
explicit treatment of UTF8 character sequences as Isabelle symbols;
wenzelm
parents:
36611
diff
changeset
|
1096 |
\item a single ASCII character ``\isa{c}'', for example |
d775bd70f571
explicit treatment of UTF8 character sequences as Isabelle symbols;
wenzelm
parents:
36611
diff
changeset
|
1097 |
``\verb,a,'', |
d775bd70f571
explicit treatment of UTF8 character sequences as Isabelle symbols;
wenzelm
parents:
36611
diff
changeset
|
1098 |
|
d775bd70f571
explicit treatment of UTF8 character sequences as Isabelle symbols;
wenzelm
parents:
36611
diff
changeset
|
1099 |
\item a codepoint according to UTF8 (non-ASCII byte sequence), |
30296 | 1100 |
|
1101 |
\item a regular symbol ``\verb,\,\verb,<,\isa{ident}\verb,>,'', |
|
1102 |
for example ``\verb,\,\verb,<alpha>,'', |
|
1103 |
||
1104 |
\item a control symbol ``\verb,\,\verb,<^,\isa{ident}\verb,>,'', |
|
1105 |
for example ``\verb,\,\verb,<^bold>,'', |
|
1106 |
||
1107 |
\item a raw symbol ``\verb,\,\verb,<^raw:,\isa{text}\verb,>,'' |
|
35001 | 1108 |
where \isa{text} consists of printable characters excluding |
30296 | 1109 |
``\verb,.,'' and ``\verb,>,'', for example |
1110 |
``\verb,\,\verb,<^raw:$\sum_{i = 1}^n$>,'', |
|
1111 |
||
1112 |
\item a numbered raw control symbol ``\verb,\,\verb,<^raw,\isa{n}\verb,>, where \isa{n} consists of digits, for example |
|
1113 |
``\verb,\,\verb,<^raw42>,''. |
|
1114 |
||
1115 |
\end{enumerate} |
|
1116 |
||
40406 | 1117 |
The \isa{ident} syntax for symbol names is \isa{letter\ {\isaliteral{28}{\isacharparenleft}}letter\ {\isaliteral{7C}{\isacharbar}}\ digit{\isaliteral{29}{\isacharparenright}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}}, where \isa{letter\ {\isaliteral{3D}{\isacharequal}}\ A{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}Za{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}z} and \isa{digit\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{0}}{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}{\isadigit{9}}}. There are infinitely many regular symbols and |
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1118 |
control symbols, but a fixed collection of standard symbols is |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1119 |
treated specifically. For example, ``\verb,\,\verb,<alpha>,'' is |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1120 |
classified as a letter, which means it may occur within regular |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1121 |
Isabelle identifiers. |
30296 | 1122 |
|
37533
d775bd70f571
explicit treatment of UTF8 character sequences as Isabelle symbols;
wenzelm
parents:
36611
diff
changeset
|
1123 |
The character set underlying Isabelle symbols is 7-bit ASCII, but |
d775bd70f571
explicit treatment of UTF8 character sequences as Isabelle symbols;
wenzelm
parents:
36611
diff
changeset
|
1124 |
8-bit character sequences are passed-through unchanged. Unicode/UCS |
d775bd70f571
explicit treatment of UTF8 character sequences as Isabelle symbols;
wenzelm
parents:
36611
diff
changeset
|
1125 |
data in UTF-8 encoding is processed in a non-strict fashion, such |
d775bd70f571
explicit treatment of UTF8 character sequences as Isabelle symbols;
wenzelm
parents:
36611
diff
changeset
|
1126 |
that well-formed code sequences are recognized |
d775bd70f571
explicit treatment of UTF8 character sequences as Isabelle symbols;
wenzelm
parents:
36611
diff
changeset
|
1127 |
accordingly.\footnote{Note that ISO-Latin-1 differs from UTF-8 only |
d775bd70f571
explicit treatment of UTF8 character sequences as Isabelle symbols;
wenzelm
parents:
36611
diff
changeset
|
1128 |
in some special punctuation characters that even have replacements |
d775bd70f571
explicit treatment of UTF8 character sequences as Isabelle symbols;
wenzelm
parents:
36611
diff
changeset
|
1129 |
within the standard collection of Isabelle symbols. Text consisting |
d775bd70f571
explicit treatment of UTF8 character sequences as Isabelle symbols;
wenzelm
parents:
36611
diff
changeset
|
1130 |
of ASCII plus accented letters can be processed in either encoding.} |
d775bd70f571
explicit treatment of UTF8 character sequences as Isabelle symbols;
wenzelm
parents:
36611
diff
changeset
|
1131 |
Unicode provides its own collection of mathematical symbols, but |
d775bd70f571
explicit treatment of UTF8 character sequences as Isabelle symbols;
wenzelm
parents:
36611
diff
changeset
|
1132 |
within the core Isabelle/ML world there is no link to the standard |
d775bd70f571
explicit treatment of UTF8 character sequences as Isabelle symbols;
wenzelm
parents:
36611
diff
changeset
|
1133 |
collection of Isabelle regular symbols. |
30296 | 1134 |
|
1135 |
\medskip Output of Isabelle symbols depends on the print mode |
|
1136 |
(\secref{print-mode}). For example, the standard {\LaTeX} setup of |
|
1137 |
the Isabelle document preparation system would present |
|
40406 | 1138 |
``\verb,\,\verb,<alpha>,'' as \isa{{\isaliteral{5C3C616C7068613E}{\isasymalpha}}}, and |
1139 |
``\verb,\,\verb,<^bold>,\verb,\,\verb,<alpha>,'' as \isa{\isaliteral{5C3C5E626F6C643E}{}\isactrlbold {\isaliteral{5C3C616C7068613E}{\isasymalpha}}}. On-screen rendering usually works by mapping a finite |
|
35001 | 1140 |
subset of Isabelle symbols to suitable Unicode characters.% |
30296 | 1141 |
\end{isamarkuptext}% |
1142 |
\isamarkuptrue% |
|
1143 |
% |
|
1144 |
\isadelimmlref |
|
1145 |
% |
|
1146 |
\endisadelimmlref |
|
1147 |
% |
|
1148 |
\isatagmlref |
|
1149 |
% |
|
1150 |
\begin{isamarkuptext}% |
|
1151 |
\begin{mldecls} |
|
35001 | 1152 |
\indexdef{}{ML type}{Symbol.symbol}\verb|type Symbol.symbol = string| \\ |
30296 | 1153 |
\indexdef{}{ML}{Symbol.explode}\verb|Symbol.explode: string -> Symbol.symbol list| \\ |
1154 |
\indexdef{}{ML}{Symbol.is\_letter}\verb|Symbol.is_letter: Symbol.symbol -> bool| \\ |
|
1155 |
\indexdef{}{ML}{Symbol.is\_digit}\verb|Symbol.is_digit: Symbol.symbol -> bool| \\ |
|
1156 |
\indexdef{}{ML}{Symbol.is\_quasi}\verb|Symbol.is_quasi: Symbol.symbol -> bool| \\ |
|
1157 |
\indexdef{}{ML}{Symbol.is\_blank}\verb|Symbol.is_blank: Symbol.symbol -> bool| \\ |
|
1158 |
\end{mldecls} |
|
1159 |
\begin{mldecls} |
|
1160 |
\indexdef{}{ML type}{Symbol.sym}\verb|type Symbol.sym| \\ |
|
1161 |
\indexdef{}{ML}{Symbol.decode}\verb|Symbol.decode: Symbol.symbol -> Symbol.sym| \\ |
|
1162 |
\end{mldecls} |
|
1163 |
||
1164 |
\begin{description} |
|
1165 |
||
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1166 |
\item Type \verb|Symbol.symbol| represents individual Isabelle |
35001 | 1167 |
symbols. |
30296 | 1168 |
|
1169 |
\item \verb|Symbol.explode|~\isa{str} produces a symbol list |
|
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1170 |
from the packed form. This function supersedes \verb|String.explode| for virtually all purposes of manipulating text in |
35001 | 1171 |
Isabelle!\footnote{The runtime overhead for exploded strings is |
1172 |
mainly that of the list structure: individual symbols that happen to |
|
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1173 |
be a singleton string do not require extra memory in Poly/ML.} |
30296 | 1174 |
|
1175 |
\item \verb|Symbol.is_letter|, \verb|Symbol.is_digit|, \verb|Symbol.is_quasi|, \verb|Symbol.is_blank| classify standard |
|
1176 |
symbols according to fixed syntactic conventions of Isabelle, cf.\ |
|
1177 |
\cite{isabelle-isar-ref}. |
|
1178 |
||
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1179 |
\item Type \verb|Symbol.sym| is a concrete datatype that |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1180 |
represents the different kinds of symbols explicitly, with |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1181 |
constructors \verb|Symbol.Char|, \verb|Symbol.Sym|, \verb|Symbol.UTF8|, \verb|Symbol.Ctrl|, \verb|Symbol.Raw|. |
30296 | 1182 |
|
1183 |
\item \verb|Symbol.decode| converts the string representation of a |
|
1184 |
symbol into the datatype version. |
|
1185 |
||
35001 | 1186 |
\end{description} |
1187 |
||
1188 |
\paragraph{Historical note.} In the original SML90 standard the |
|
40628 | 1189 |
primitive ML type \verb|char| did not exists, and the \verb|explode: string -> string list| operation would produce a list of |
1190 |
singleton strings as does \verb|raw_explode: string -> string list| |
|
1191 |
in Isabelle/ML today. When SML97 came out, Isabelle did not adopt |
|
1192 |
its slightly anachronistic 8-bit characters, but the idea of |
|
1193 |
exploding a string into a list of small strings was extended to |
|
1194 |
``symbols'' as explained above. Thus Isabelle sources can refer to |
|
1195 |
an infinite store of user-defined symbols, without having to worry |
|
1196 |
about the multitude of Unicode encodings.% |
|
30296 | 1197 |
\end{isamarkuptext}% |
1198 |
\isamarkuptrue% |
|
1199 |
% |
|
1200 |
\endisatagmlref |
|
1201 |
{\isafoldmlref}% |
|
1202 |
% |
|
1203 |
\isadelimmlref |
|
1204 |
% |
|
1205 |
\endisadelimmlref |
|
1206 |
% |
|
35001 | 1207 |
\isamarkupsubsection{Basic names \label{sec:basic-name}% |
30296 | 1208 |
} |
1209 |
\isamarkuptrue% |
|
1210 |
% |
|
1211 |
\begin{isamarkuptext}% |
|
1212 |
A \emph{basic name} essentially consists of a single Isabelle |
|
1213 |
identifier. There are conventions to mark separate classes of basic |
|
1214 |
names, by attaching a suffix of underscores: one underscore means |
|
1215 |
\emph{internal name}, two underscores means \emph{Skolem name}, |
|
1216 |
three underscores means \emph{internal Skolem name}. |
|
1217 |
||
1218 |
For example, the basic name \isa{foo} has the internal version |
|
40406 | 1219 |
\isa{foo{\isaliteral{5F}{\isacharunderscore}}}, with Skolem versions \isa{foo{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{5F}{\isacharunderscore}}} and \isa{foo{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{5F}{\isacharunderscore}}}, respectively. |
30296 | 1220 |
|
1221 |
These special versions provide copies of the basic name space, apart |
|
1222 |
from anything that normally appears in the user text. For example, |
|
1223 |
system generated variables in Isar proof contexts are usually marked |
|
35001 | 1224 |
as internal, which prevents mysterious names like \isa{xaa} to |
1225 |
appear in human-readable text. |
|
30296 | 1226 |
|
1227 |
\medskip Manipulating binding scopes often requires on-the-fly |
|
1228 |
renamings. A \emph{name context} contains a collection of already |
|
1229 |
used names. The \isa{declare} operation adds names to the |
|
1230 |
context. |
|
1231 |
||
1232 |
The \isa{invents} operation derives a number of fresh names from |
|
1233 |
a given starting point. For example, the first three names derived |
|
1234 |
from \isa{a} are \isa{a}, \isa{b}, \isa{c}. |
|
1235 |
||
1236 |
The \isa{variants} operation produces fresh names by |
|
40406 | 1237 |
incrementing tentative names as base-26 numbers (with digits \isa{a{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}z}) until all clashes are resolved. For example, name \isa{foo} results in variants \isa{fooa}, \isa{foob}, \isa{fooc}, \dots, \isa{fooaa}, \isa{fooab} etc.; each renaming |
30296 | 1238 |
step picks the next unused variant from this sequence.% |
1239 |
\end{isamarkuptext}% |
|
1240 |
\isamarkuptrue% |
|
1241 |
% |
|
1242 |
\isadelimmlref |
|
1243 |
% |
|
1244 |
\endisadelimmlref |
|
1245 |
% |
|
1246 |
\isatagmlref |
|
1247 |
% |
|
1248 |
\begin{isamarkuptext}% |
|
1249 |
\begin{mldecls} |
|
1250 |
\indexdef{}{ML}{Name.internal}\verb|Name.internal: string -> string| \\ |
|
1251 |
\indexdef{}{ML}{Name.skolem}\verb|Name.skolem: string -> string| \\ |
|
1252 |
\end{mldecls} |
|
1253 |
\begin{mldecls} |
|
1254 |
\indexdef{}{ML type}{Name.context}\verb|type Name.context| \\ |
|
1255 |
\indexdef{}{ML}{Name.context}\verb|Name.context: Name.context| \\ |
|
1256 |
\indexdef{}{ML}{Name.declare}\verb|Name.declare: string -> Name.context -> Name.context| \\ |
|
1257 |
\indexdef{}{ML}{Name.invents}\verb|Name.invents: Name.context -> string -> int -> string list| \\ |
|
1258 |
\indexdef{}{ML}{Name.variants}\verb|Name.variants: string list -> Name.context -> string list * Name.context| \\ |
|
1259 |
\end{mldecls} |
|
35001 | 1260 |
\begin{mldecls} |
1261 |
\indexdef{}{ML}{Variable.names\_of}\verb|Variable.names_of: Proof.context -> Name.context| \\ |
|
1262 |
\end{mldecls} |
|
30296 | 1263 |
|
1264 |
\begin{description} |
|
1265 |
||
1266 |
\item \verb|Name.internal|~\isa{name} produces an internal name |
|
1267 |
by adding one underscore. |
|
1268 |
||
1269 |
\item \verb|Name.skolem|~\isa{name} produces a Skolem name by |
|
1270 |
adding two underscores. |
|
1271 |
||
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1272 |
\item Type \verb|Name.context| represents the context of already |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1273 |
used names; the initial value is \verb|Name.context|. |
30296 | 1274 |
|
1275 |
\item \verb|Name.declare|~\isa{name} enters a used name into the |
|
1276 |
context. |
|
1277 |
||
1278 |
\item \verb|Name.invents|~\isa{context\ name\ n} produces \isa{n} fresh names derived from \isa{name}. |
|
1279 |
||
1280 |
\item \verb|Name.variants|~\isa{names\ context} produces fresh |
|
1281 |
variants of \isa{names}; the result is entered into the context. |
|
1282 |
||
35001 | 1283 |
\item \verb|Variable.names_of|~\isa{ctxt} retrieves the context |
1284 |
of declared type and term variable names. Projecting a proof |
|
1285 |
context down to a primitive name context is occasionally useful when |
|
1286 |
invoking lower-level operations. Regular management of ``fresh |
|
1287 |
variables'' is done by suitable operations of structure \verb|Variable|, which is also able to provide an official status of |
|
1288 |
``locally fixed variable'' within the logical environment (cf.\ |
|
1289 |
\secref{sec:variables}). |
|
1290 |
||
30296 | 1291 |
\end{description}% |
1292 |
\end{isamarkuptext}% |
|
1293 |
\isamarkuptrue% |
|
1294 |
% |
|
1295 |
\endisatagmlref |
|
1296 |
{\isafoldmlref}% |
|
1297 |
% |
|
1298 |
\isadelimmlref |
|
1299 |
% |
|
1300 |
\endisadelimmlref |
|
1301 |
% |
|
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1302 |
\isadelimmlex |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1303 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1304 |
\endisadelimmlex |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1305 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1306 |
\isatagmlex |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1307 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1308 |
\begin{isamarkuptext}% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1309 |
The following simple examples demonstrate how to produce |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1310 |
fresh names from the initial \verb|Name.context|.% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1311 |
\end{isamarkuptext}% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1312 |
\isamarkuptrue% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1313 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1314 |
\endisatagmlex |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1315 |
{\isafoldmlex}% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1316 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1317 |
\isadelimmlex |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1318 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1319 |
\endisadelimmlex |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1320 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1321 |
\isadelimML |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1322 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1323 |
\endisadelimML |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1324 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1325 |
\isatagML |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1326 |
\isacommand{ML}\isamarkupfalse% |
40406 | 1327 |
\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline |
1328 |
\ \ val\ list{\isadigit{1}}\ {\isaliteral{3D}{\isacharequal}}\ Name{\isaliteral{2E}{\isachardot}}invents\ Name{\isaliteral{2E}{\isachardot}}context\ {\isaliteral{22}{\isachardoublequote}}a{\isaliteral{22}{\isachardoublequote}}\ {\isadigit{5}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
|
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1329 |
\ \ % |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1330 |
\isaantiq |
40406 | 1331 |
assert{}% |
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1332 |
\endisaantiq |
40406 | 1333 |
\ {\isaliteral{28}{\isacharparenleft}}list{\isadigit{1}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{22}{\isachardoublequote}}a{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{22}{\isachardoublequote}}b{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{22}{\isachardoublequote}}c{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{22}{\isachardoublequote}}d{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{22}{\isachardoublequote}}e{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1334 |
\isanewline |
40406 | 1335 |
\ \ val\ list{\isadigit{2}}\ {\isaliteral{3D}{\isacharequal}}\isanewline |
1336 |
\ \ \ \ {\isaliteral{23}{\isacharhash}}{\isadigit{1}}\ {\isaliteral{28}{\isacharparenleft}}Name{\isaliteral{2E}{\isachardot}}variants\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{22}{\isachardoublequote}}x{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{22}{\isachardoublequote}}x{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{22}{\isachardoublequote}}a{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{22}{\isachardoublequote}}a{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{27}{\isacharprime}}a{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{27}{\isacharprime}}a{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5D}{\isacharbrackright}}\ Name{\isaliteral{2E}{\isachardot}}context{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
|
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1337 |
\ \ % |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1338 |
\isaantiq |
40406 | 1339 |
assert{}% |
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1340 |
\endisaantiq |
40406 | 1341 |
\ {\isaliteral{28}{\isacharparenleft}}list{\isadigit{2}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{22}{\isachardoublequote}}x{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{22}{\isachardoublequote}}xa{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{22}{\isachardoublequote}}a{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{22}{\isachardoublequote}}aa{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{27}{\isacharprime}}a{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{27}{\isacharprime}}aa{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
1342 |
{\isaliteral{2A7D}{\isacharverbatimclose}}% |
|
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1343 |
\endisatagML |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1344 |
{\isafoldML}% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1345 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1346 |
\isadelimML |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1347 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1348 |
\endisadelimML |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1349 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1350 |
\begin{isamarkuptext}% |
40126 | 1351 |
\medskip The same works relatively to the formal context as |
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1352 |
follows.% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1353 |
\end{isamarkuptext}% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1354 |
\isamarkuptrue% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1355 |
\isacommand{locale}\isamarkupfalse% |
40406 | 1356 |
\ ex\ {\isaliteral{3D}{\isacharequal}}\ \isakeyword{fixes}\ a\ b\ c\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{27}{\isacharprime}}a\isanewline |
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1357 |
\isakeyword{begin}\isanewline |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1358 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1359 |
\isadelimML |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1360 |
\isanewline |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1361 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1362 |
\endisadelimML |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1363 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1364 |
\isatagML |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1365 |
\isacommand{ML}\isamarkupfalse% |
40406 | 1366 |
\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline |
1367 |
\ \ val\ names\ {\isaliteral{3D}{\isacharequal}}\ Variable{\isaliteral{2E}{\isachardot}}names{\isaliteral{5F}{\isacharunderscore}}of\ % |
|
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1368 |
\isaantiq |
40406 | 1369 |
context{}% |
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1370 |
\endisaantiq |
40406 | 1371 |
{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1372 |
\isanewline |
40406 | 1373 |
\ \ val\ list{\isadigit{1}}\ {\isaliteral{3D}{\isacharequal}}\ Name{\isaliteral{2E}{\isachardot}}invents\ names\ {\isaliteral{22}{\isachardoublequote}}a{\isaliteral{22}{\isachardoublequote}}\ {\isadigit{5}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1374 |
\ \ % |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1375 |
\isaantiq |
40406 | 1376 |
assert{}% |
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1377 |
\endisaantiq |
40406 | 1378 |
\ {\isaliteral{28}{\isacharparenleft}}list{\isadigit{1}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{22}{\isachardoublequote}}d{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{22}{\isachardoublequote}}e{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{22}{\isachardoublequote}}f{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{22}{\isachardoublequote}}g{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{22}{\isachardoublequote}}h{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1379 |
\isanewline |
40406 | 1380 |
\ \ val\ list{\isadigit{2}}\ {\isaliteral{3D}{\isacharequal}}\isanewline |
1381 |
\ \ \ \ {\isaliteral{23}{\isacharhash}}{\isadigit{1}}\ {\isaliteral{28}{\isacharparenleft}}Name{\isaliteral{2E}{\isachardot}}variants\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{22}{\isachardoublequote}}x{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{22}{\isachardoublequote}}x{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{22}{\isachardoublequote}}a{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{22}{\isachardoublequote}}a{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{27}{\isacharprime}}a{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{27}{\isacharprime}}a{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5D}{\isacharbrackright}}\ names{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
|
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1382 |
\ \ % |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1383 |
\isaantiq |
40406 | 1384 |
assert{}% |
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1385 |
\endisaantiq |
40406 | 1386 |
\ {\isaliteral{28}{\isacharparenleft}}list{\isadigit{2}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{22}{\isachardoublequote}}x{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{22}{\isachardoublequote}}xa{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{22}{\isachardoublequote}}aa{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{22}{\isachardoublequote}}ab{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{27}{\isacharprime}}aa{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{27}{\isacharprime}}ab{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
1387 |
{\isaliteral{2A7D}{\isacharverbatimclose}}% |
|
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1388 |
\endisatagML |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1389 |
{\isafoldML}% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1390 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1391 |
\isadelimML |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1392 |
\isanewline |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1393 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1394 |
\endisadelimML |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1395 |
\isanewline |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1396 |
\isacommand{end}\isamarkupfalse% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1397 |
% |
35001 | 1398 |
\isamarkupsubsection{Indexed names \label{sec:indexname}% |
30296 | 1399 |
} |
1400 |
\isamarkuptrue% |
|
1401 |
% |
|
1402 |
\begin{isamarkuptext}% |
|
1403 |
An \emph{indexed name} (or \isa{indexname}) is a pair of a basic |
|
1404 |
name and a natural number. This representation allows efficient |
|
1405 |
renaming by incrementing the second component only. The canonical |
|
1406 |
way to rename two collections of indexnames apart from each other is |
|
1407 |
this: determine the maximum index \isa{maxidx} of the first |
|
1408 |
collection, then increment all indexes of the second collection by |
|
40406 | 1409 |
\isa{maxidx\ {\isaliteral{2B}{\isacharplus}}\ {\isadigit{1}}}; the maximum index of an empty collection is |
1410 |
\isa{{\isaliteral{2D}{\isacharminus}}{\isadigit{1}}}. |
|
30296 | 1411 |
|
35001 | 1412 |
Occasionally, basic names are injected into the same pair type of |
40406 | 1413 |
indexed names: then \isa{{\isaliteral{28}{\isacharparenleft}}x{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{2D}{\isacharminus}}{\isadigit{1}}{\isaliteral{29}{\isacharparenright}}} is used to encode the basic |
35001 | 1414 |
name \isa{x}. |
30296 | 1415 |
|
1416 |
\medskip Isabelle syntax observes the following rules for |
|
40406 | 1417 |
representing an indexname \isa{{\isaliteral{28}{\isacharparenleft}}x{\isaliteral{2C}{\isacharcomma}}\ i{\isaliteral{29}{\isacharparenright}}} as a packed string: |
30296 | 1418 |
|
1419 |
\begin{itemize} |
|
1420 |
||
40406 | 1421 |
\item \isa{{\isaliteral{3F}{\isacharquery}}x} if \isa{x} does not end with a digit and \isa{i\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{0}}}, |
30296 | 1422 |
|
40406 | 1423 |
\item \isa{{\isaliteral{3F}{\isacharquery}}xi} if \isa{x} does not end with a digit, |
30296 | 1424 |
|
40406 | 1425 |
\item \isa{{\isaliteral{3F}{\isacharquery}}x{\isaliteral{2E}{\isachardot}}i} otherwise. |
30296 | 1426 |
|
1427 |
\end{itemize} |
|
1428 |
||
35001 | 1429 |
Indexnames may acquire large index numbers after several maxidx |
1430 |
shifts have been applied. Results are usually normalized towards |
|
1431 |
\isa{{\isadigit{0}}} at certain checkpoints, notably at the end of a proof. |
|
1432 |
This works by producing variants of the corresponding basic name |
|
40406 | 1433 |
components. For example, the collection \isa{{\isaliteral{3F}{\isacharquery}}x{\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{3F}{\isacharquery}}x{\isadigit{7}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{3F}{\isacharquery}}x{\isadigit{4}}{\isadigit{2}}} |
1434 |
becomes \isa{{\isaliteral{3F}{\isacharquery}}x{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{3F}{\isacharquery}}xa{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{3F}{\isacharquery}}xb}.% |
|
30296 | 1435 |
\end{isamarkuptext}% |
1436 |
\isamarkuptrue% |
|
1437 |
% |
|
1438 |
\isadelimmlref |
|
1439 |
% |
|
1440 |
\endisadelimmlref |
|
1441 |
% |
|
1442 |
\isatagmlref |
|
1443 |
% |
|
1444 |
\begin{isamarkuptext}% |
|
1445 |
\begin{mldecls} |
|
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1446 |
\indexdef{}{ML type}{indexname}\verb|type indexname = string * int| \\ |
30296 | 1447 |
\end{mldecls} |
1448 |
||
1449 |
\begin{description} |
|
1450 |
||
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1451 |
\item Type \verb|indexname| represents indexed names. This is |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1452 |
an abbreviation for \verb|string * int|. The second component |
40406 | 1453 |
is usually non-negative, except for situations where \isa{{\isaliteral{28}{\isacharparenleft}}x{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{2D}{\isacharminus}}{\isadigit{1}}{\isaliteral{29}{\isacharparenright}}} is used to inject basic names into this type. Other negative |
35001 | 1454 |
indexes should not be used. |
30296 | 1455 |
|
1456 |
\end{description}% |
|
1457 |
\end{isamarkuptext}% |
|
1458 |
\isamarkuptrue% |
|
1459 |
% |
|
1460 |
\endisatagmlref |
|
1461 |
{\isafoldmlref}% |
|
1462 |
% |
|
1463 |
\isadelimmlref |
|
1464 |
% |
|
1465 |
\endisadelimmlref |
|
1466 |
% |
|
35001 | 1467 |
\isamarkupsubsection{Long names \label{sec:long-name}% |
30296 | 1468 |
} |
1469 |
\isamarkuptrue% |
|
1470 |
% |
|
1471 |
\begin{isamarkuptext}% |
|
35001 | 1472 |
A \emph{long name} consists of a sequence of non-empty name |
1473 |
components. The packed representation uses a dot as separator, as |
|
40406 | 1474 |
in ``\isa{A{\isaliteral{2E}{\isachardot}}b{\isaliteral{2E}{\isachardot}}c}''. The last component is called \emph{base |
35001 | 1475 |
name}, the remaining prefix is called \emph{qualifier} (which may be |
1476 |
empty). The qualifier can be understood as the access path to the |
|
1477 |
named entity while passing through some nested block-structure, |
|
1478 |
although our free-form long names do not really enforce any strict |
|
1479 |
discipline. |
|
1480 |
||
40406 | 1481 |
For example, an item named ``\isa{A{\isaliteral{2E}{\isachardot}}b{\isaliteral{2E}{\isachardot}}c}'' may be understood as |
35001 | 1482 |
a local entity \isa{c}, within a local structure \isa{b}, |
1483 |
within a global structure \isa{A}. In practice, long names |
|
1484 |
usually represent 1--3 levels of qualification. User ML code should |
|
1485 |
not make any assumptions about the particular structure of long |
|
1486 |
names! |
|
30296 | 1487 |
|
1488 |
The empty name is commonly used as an indication of unnamed |
|
35001 | 1489 |
entities, or entities that are not entered into the corresponding |
1490 |
name space, whenever this makes any sense. The basic operations on |
|
1491 |
long names map empty names again to empty names.% |
|
30296 | 1492 |
\end{isamarkuptext}% |
1493 |
\isamarkuptrue% |
|
1494 |
% |
|
1495 |
\isadelimmlref |
|
1496 |
% |
|
1497 |
\endisadelimmlref |
|
1498 |
% |
|
1499 |
\isatagmlref |
|
1500 |
% |
|
1501 |
\begin{isamarkuptext}% |
|
1502 |
\begin{mldecls} |
|
30365 | 1503 |
\indexdef{}{ML}{Long\_Name.base\_name}\verb|Long_Name.base_name: string -> string| \\ |
1504 |
\indexdef{}{ML}{Long\_Name.qualifier}\verb|Long_Name.qualifier: string -> string| \\ |
|
1505 |
\indexdef{}{ML}{Long\_Name.append}\verb|Long_Name.append: string -> string -> string| \\ |
|
1506 |
\indexdef{}{ML}{Long\_Name.implode}\verb|Long_Name.implode: string list -> string| \\ |
|
1507 |
\indexdef{}{ML}{Long\_Name.explode}\verb|Long_Name.explode: string -> string list| \\ |
|
30296 | 1508 |
\end{mldecls} |
35001 | 1509 |
|
1510 |
\begin{description} |
|
1511 |
||
1512 |
\item \verb|Long_Name.base_name|~\isa{name} returns the base name |
|
1513 |
of a long name. |
|
1514 |
||
1515 |
\item \verb|Long_Name.qualifier|~\isa{name} returns the qualifier |
|
1516 |
of a long name. |
|
1517 |
||
40406 | 1518 |
\item \verb|Long_Name.append|~\isa{name\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ name\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{2}}} appends two long |
35001 | 1519 |
names. |
1520 |
||
1521 |
\item \verb|Long_Name.implode|~\isa{names} and \verb|Long_Name.explode|~\isa{name} convert between the packed string |
|
1522 |
representation and the explicit list form of long names. |
|
1523 |
||
1524 |
\end{description}% |
|
1525 |
\end{isamarkuptext}% |
|
1526 |
\isamarkuptrue% |
|
1527 |
% |
|
1528 |
\endisatagmlref |
|
1529 |
{\isafoldmlref}% |
|
1530 |
% |
|
1531 |
\isadelimmlref |
|
1532 |
% |
|
1533 |
\endisadelimmlref |
|
1534 |
% |
|
1535 |
\isamarkupsubsection{Name spaces \label{sec:name-space}% |
|
1536 |
} |
|
1537 |
\isamarkuptrue% |
|
1538 |
% |
|
1539 |
\begin{isamarkuptext}% |
|
1540 |
A \isa{name\ space} manages a collection of long names, |
|
1541 |
together with a mapping between partially qualified external names |
|
1542 |
and fully qualified internal names (in both directions). Note that |
|
1543 |
the corresponding \isa{intern} and \isa{extern} operations |
|
1544 |
are mostly used for parsing and printing only! The \isa{declare} operation augments a name space according to the accesses |
|
1545 |
determined by a given binding, and a naming policy from the context. |
|
1546 |
||
1547 |
\medskip A \isa{binding} specifies details about the prospective |
|
1548 |
long name of a newly introduced formal entity. It consists of a |
|
1549 |
base name, prefixes for qualification (separate ones for system |
|
1550 |
infrastructure and user-space mechanisms), a slot for the original |
|
1551 |
source position, and some additional flags. |
|
1552 |
||
1553 |
\medskip A \isa{naming} provides some additional details for |
|
1554 |
producing a long name from a binding. Normally, the naming is |
|
1555 |
implicit in the theory or proof context. The \isa{full} |
|
1556 |
operation (and its variants for different context types) produces a |
|
1557 |
fully qualified internal name to be entered into a name space. The |
|
1558 |
main equation of this ``chemical reaction'' when binding new |
|
1559 |
entities in a context is as follows: |
|
1560 |
||
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1561 |
\medskip |
35001 | 1562 |
\begin{tabular}{l} |
40406 | 1563 |
\isa{binding\ {\isaliteral{2B}{\isacharplus}}\ naming\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ long\ name\ {\isaliteral{2B}{\isacharplus}}\ name\ space\ accesses} |
35001 | 1564 |
\end{tabular} |
1565 |
||
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1566 |
\bigskip As a general principle, there is a separate name space for |
35001 | 1567 |
each kind of formal entity, e.g.\ fact, logical constant, type |
1568 |
constructor, type class. It is usually clear from the occurrence in |
|
1569 |
concrete syntax (or from the scope) which kind of entity a name |
|
1570 |
refers to. For example, the very same name \isa{c} may be used |
|
1571 |
uniformly for a constant, type constructor, and type class. |
|
1572 |
||
1573 |
There are common schemes to name derived entities systematically |
|
1574 |
according to the name of the main logical entity involved, e.g.\ |
|
40406 | 1575 |
fact \isa{c{\isaliteral{2E}{\isachardot}}intro} for a canonical introduction rule related to |
35001 | 1576 |
constant \isa{c}. This technique of mapping names from one |
1577 |
space into another requires some care in order to avoid conflicts. |
|
1578 |
In particular, theorem names derived from a type constructor or type |
|
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1579 |
class should get an additional suffix in addition to the usual |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1580 |
qualification. This leads to the following conventions for derived |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1581 |
names: |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1582 |
|
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1583 |
\medskip |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1584 |
\begin{tabular}{ll} |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1585 |
logical entity & fact name \\\hline |
40406 | 1586 |
constant \isa{c} & \isa{c{\isaliteral{2E}{\isachardot}}intro} \\ |
1587 |
type \isa{c} & \isa{c{\isaliteral{5F}{\isacharunderscore}}type{\isaliteral{2E}{\isachardot}}intro} \\ |
|
1588 |
class \isa{c} & \isa{c{\isaliteral{5F}{\isacharunderscore}}class{\isaliteral{2E}{\isachardot}}intro} \\ |
|
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1589 |
\end{tabular}% |
35001 | 1590 |
\end{isamarkuptext}% |
1591 |
\isamarkuptrue% |
|
1592 |
% |
|
1593 |
\isadelimmlref |
|
1594 |
% |
|
1595 |
\endisadelimmlref |
|
1596 |
% |
|
1597 |
\isatagmlref |
|
1598 |
% |
|
1599 |
\begin{isamarkuptext}% |
|
1600 |
\begin{mldecls} |
|
1601 |
\indexdef{}{ML type}{binding}\verb|type binding| \\ |
|
1602 |
\indexdef{}{ML}{Binding.empty}\verb|Binding.empty: binding| \\ |
|
1603 |
\indexdef{}{ML}{Binding.name}\verb|Binding.name: string -> binding| \\ |
|
1604 |
\indexdef{}{ML}{Binding.qualify}\verb|Binding.qualify: bool -> string -> binding -> binding| \\ |
|
1605 |
\indexdef{}{ML}{Binding.prefix}\verb|Binding.prefix: bool -> string -> binding -> binding| \\ |
|
1606 |
\indexdef{}{ML}{Binding.conceal}\verb|Binding.conceal: binding -> binding| \\ |
|
1607 |
\indexdef{}{ML}{Binding.str\_of}\verb|Binding.str_of: binding -> string| \\ |
|
1608 |
\end{mldecls} |
|
30296 | 1609 |
\begin{mldecls} |
33174 | 1610 |
\indexdef{}{ML type}{Name\_Space.naming}\verb|type Name_Space.naming| \\ |
1611 |
\indexdef{}{ML}{Name\_Space.default\_naming}\verb|Name_Space.default_naming: Name_Space.naming| \\ |
|
1612 |
\indexdef{}{ML}{Name\_Space.add\_path}\verb|Name_Space.add_path: string -> Name_Space.naming -> Name_Space.naming| \\ |
|
1613 |
\indexdef{}{ML}{Name\_Space.full\_name}\verb|Name_Space.full_name: Name_Space.naming -> binding -> string| \\ |
|
30296 | 1614 |
\end{mldecls} |
1615 |
\begin{mldecls} |
|
33174 | 1616 |
\indexdef{}{ML type}{Name\_Space.T}\verb|type Name_Space.T| \\ |
1617 |
\indexdef{}{ML}{Name\_Space.empty}\verb|Name_Space.empty: string -> Name_Space.T| \\ |
|
1618 |
\indexdef{}{ML}{Name\_Space.merge}\verb|Name_Space.merge: Name_Space.T * Name_Space.T -> Name_Space.T| \\ |
|
42401
9bfaf6819291
updated some theory primitives, which now depend on auxiliary context;
wenzelm
parents:
42361
diff
changeset
|
1619 |
\indexdef{}{ML}{Name\_Space.declare}\verb|Name_Space.declare: Proof.context -> bool ->|\isasep\isanewline% |
9bfaf6819291
updated some theory primitives, which now depend on auxiliary context;
wenzelm
parents:
42361
diff
changeset
|
1620 |
\verb| Name_Space.naming -> binding -> Name_Space.T -> string * Name_Space.T| \\ |
33174 | 1621 |
\indexdef{}{ML}{Name\_Space.intern}\verb|Name_Space.intern: Name_Space.T -> string -> string| \\ |
42358
b47d41d9f4b5
Name_Space: proper configuration options long_names, short_names, unique_names instead of former unsynchronized references;
wenzelm
parents:
40964
diff
changeset
|
1622 |
\indexdef{}{ML}{Name\_Space.extern}\verb|Name_Space.extern: Proof.context -> Name_Space.T -> string -> string| \\ |
35001 | 1623 |
\indexdef{}{ML}{Name\_Space.is\_concealed}\verb|Name_Space.is_concealed: Name_Space.T -> string -> bool| |
30296 | 1624 |
\end{mldecls} |
1625 |
||
1626 |
\begin{description} |
|
1627 |
||
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1628 |
\item Type \verb|binding| represents the abstract concept of |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1629 |
name bindings. |
35001 | 1630 |
|
1631 |
\item \verb|Binding.empty| is the empty binding. |
|
30296 | 1632 |
|
35001 | 1633 |
\item \verb|Binding.name|~\isa{name} produces a binding with base |
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1634 |
name \isa{name}. Note that this lacks proper source position |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1635 |
information; see also the ML antiquotation \hyperlink{ML antiquotation.binding}{\mbox{\isa{binding}}}. |
35001 | 1636 |
|
1637 |
\item \verb|Binding.qualify|~\isa{mandatory\ name\ binding} |
|
1638 |
prefixes qualifier \isa{name} to \isa{binding}. The \isa{mandatory} flag tells if this name component always needs to be |
|
1639 |
given in name space accesses --- this is mostly \isa{false} in |
|
1640 |
practice. Note that this part of qualification is typically used in |
|
1641 |
derived specification mechanisms. |
|
30296 | 1642 |
|
35001 | 1643 |
\item \verb|Binding.prefix| is similar to \verb|Binding.qualify|, but |
1644 |
affects the system prefix. This part of extra qualification is |
|
1645 |
typically used in the infrastructure for modular specifications, |
|
1646 |
notably ``local theory targets'' (see also \chref{ch:local-theory}). |
|
30296 | 1647 |
|
35001 | 1648 |
\item \verb|Binding.conceal|~\isa{binding} indicates that the |
1649 |
binding shall refer to an entity that serves foundational purposes |
|
1650 |
only. This flag helps to mark implementation details of |
|
1651 |
specification mechanism etc. Other tools should not depend on the |
|
1652 |
particulars of concealed entities (cf.\ \verb|Name_Space.is_concealed|). |
|
1653 |
||
1654 |
\item \verb|Binding.str_of|~\isa{binding} produces a string |
|
1655 |
representation for human-readable output, together with some formal |
|
1656 |
markup that might get used in GUI front-ends, for example. |
|
30296 | 1657 |
|
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1658 |
\item Type \verb|Name_Space.naming| represents the abstract |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1659 |
concept of a naming policy. |
30296 | 1660 |
|
33174 | 1661 |
\item \verb|Name_Space.default_naming| is the default naming policy. |
30296 | 1662 |
In a theory context, this is usually augmented by a path prefix |
1663 |
consisting of the theory name. |
|
1664 |
||
33174 | 1665 |
\item \verb|Name_Space.add_path|~\isa{path\ naming} augments the |
30296 | 1666 |
naming policy by extending its path component. |
1667 |
||
33174 | 1668 |
\item \verb|Name_Space.full_name|~\isa{naming\ binding} turns a |
30296 | 1669 |
name binding (usually a basic name) into the fully qualified |
1670 |
internal name, according to the given naming policy. |
|
1671 |
||
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1672 |
\item Type \verb|Name_Space.T| represents name spaces. |
30296 | 1673 |
|
40406 | 1674 |
\item \verb|Name_Space.empty|~\isa{kind} and \verb|Name_Space.merge|~\isa{{\isaliteral{28}{\isacharparenleft}}space\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ space\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{2}}{\isaliteral{29}{\isacharparenright}}} are the canonical operations for |
33174 | 1675 |
maintaining name spaces according to theory data management |
1676 |
(\secref{sec:context-data}); \isa{kind} is a formal comment |
|
1677 |
to characterize the purpose of a name space. |
|
30296 | 1678 |
|
42401
9bfaf6819291
updated some theory primitives, which now depend on auxiliary context;
wenzelm
parents:
42361
diff
changeset
|
1679 |
\item \verb|Name_Space.declare|~\isa{ctxt\ strict\ naming\ bindings\ space} enters a name binding as fully qualified internal name into |
33174 | 1680 |
the name space, with external accesses determined by the naming |
1681 |
policy. |
|
1682 |
||
1683 |
\item \verb|Name_Space.intern|~\isa{space\ name} internalizes a |
|
30296 | 1684 |
(partially qualified) external name. |
1685 |
||
1686 |
This operation is mostly for parsing! Note that fully qualified |
|
33174 | 1687 |
names stemming from declarations are produced via \verb|Name_Space.full_name| and \verb|Name_Space.declare| |
30296 | 1688 |
(or their derivatives for \verb|theory| and |
1689 |
\verb|Proof.context|). |
|
1690 |
||
42358
b47d41d9f4b5
Name_Space: proper configuration options long_names, short_names, unique_names instead of former unsynchronized references;
wenzelm
parents:
40964
diff
changeset
|
1691 |
\item \verb|Name_Space.extern|~\isa{ctxt\ space\ name} externalizes a |
30296 | 1692 |
(fully qualified) internal name. |
1693 |
||
1694 |
This operation is mostly for printing! User code should not rely on |
|
1695 |
the precise result too much. |
|
1696 |
||
35001 | 1697 |
\item \verb|Name_Space.is_concealed|~\isa{space\ name} indicates |
1698 |
whether \isa{name} refers to a strictly private entity that |
|
1699 |
other tools are supposed to ignore! |
|
1700 |
||
30296 | 1701 |
\end{description}% |
1702 |
\end{isamarkuptext}% |
|
1703 |
\isamarkuptrue% |
|
1704 |
% |
|
1705 |
\endisatagmlref |
|
1706 |
{\isafoldmlref}% |
|
1707 |
% |
|
1708 |
\isadelimmlref |
|
1709 |
% |
|
1710 |
\endisadelimmlref |
|
1711 |
% |
|
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1712 |
\isadelimmlantiq |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1713 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1714 |
\endisadelimmlantiq |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1715 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1716 |
\isatagmlantiq |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1717 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1718 |
\begin{isamarkuptext}% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1719 |
\begin{matharray}{rcl} |
40406 | 1720 |
\indexdef{}{ML antiquotation}{binding}\hypertarget{ML antiquotation.binding}{\hyperlink{ML antiquotation.binding}{\mbox{\isa{binding}}}} & : & \isa{ML{\isaliteral{5F}{\isacharunderscore}}antiquotation} \\ |
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1721 |
\end{matharray} |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1722 |
|
42510
b9c106763325
use @{rail} antiquotation (with some nested markup);
wenzelm
parents:
42401
diff
changeset
|
1723 |
\begin{railoutput} |
b9c106763325
use @{rail} antiquotation (with some nested markup);
wenzelm
parents:
42401
diff
changeset
|
1724 |
\rail@begin{1}{\isa{}} |
b9c106763325
use @{rail} antiquotation (with some nested markup);
wenzelm
parents:
42401
diff
changeset
|
1725 |
\rail@term{\hyperlink{ML antiquotation.binding}{\mbox{\isa{binding}}}}[] |
b9c106763325
use @{rail} antiquotation (with some nested markup);
wenzelm
parents:
42401
diff
changeset
|
1726 |
\rail@nont{\isa{name}}[] |
b9c106763325
use @{rail} antiquotation (with some nested markup);
wenzelm
parents:
42401
diff
changeset
|
1727 |
\rail@end |
b9c106763325
use @{rail} antiquotation (with some nested markup);
wenzelm
parents:
42401
diff
changeset
|
1728 |
\end{railoutput} |
b9c106763325
use @{rail} antiquotation (with some nested markup);
wenzelm
parents:
42401
diff
changeset
|
1729 |
|
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1730 |
|
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1731 |
\begin{description} |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1732 |
|
40406 | 1733 |
\item \isa{{\isaliteral{40}{\isacharat}}{\isaliteral{7B}{\isacharbraceleft}}binding\ name{\isaliteral{7D}{\isacharbraceright}}} produces a binding with base name |
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1734 |
\isa{name} and the source position taken from the concrete |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1735 |
syntax of this antiquotation. In many situations this is more |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1736 |
appropriate than the more basic \verb|Binding.name| function. |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1737 |
|
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1738 |
\end{description}% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1739 |
\end{isamarkuptext}% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1740 |
\isamarkuptrue% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1741 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1742 |
\endisatagmlantiq |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1743 |
{\isafoldmlantiq}% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1744 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1745 |
\isadelimmlantiq |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1746 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1747 |
\endisadelimmlantiq |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1748 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1749 |
\isadelimmlex |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1750 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1751 |
\endisadelimmlex |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1752 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1753 |
\isatagmlex |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1754 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1755 |
\begin{isamarkuptext}% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1756 |
The following example yields the source position of some |
40126 | 1757 |
concrete binding inlined into the text:% |
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1758 |
\end{isamarkuptext}% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1759 |
\isamarkuptrue% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1760 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1761 |
\endisatagmlex |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1762 |
{\isafoldmlex}% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1763 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1764 |
\isadelimmlex |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1765 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1766 |
\endisadelimmlex |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1767 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1768 |
\isadelimML |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1769 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1770 |
\endisadelimML |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1771 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1772 |
\isatagML |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1773 |
\isacommand{ML}\isamarkupfalse% |
40406 | 1774 |
\ {\isaliteral{7B2A}{\isacharverbatimopen}}\ Binding{\isaliteral{2E}{\isachardot}}pos{\isaliteral{5F}{\isacharunderscore}}of\ % |
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1775 |
\isaantiq |
40406 | 1776 |
binding\ here{}% |
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1777 |
\endisaantiq |
40406 | 1778 |
\ {\isaliteral{2A7D}{\isacharverbatimclose}}% |
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1779 |
\endisatagML |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1780 |
{\isafoldML}% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1781 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1782 |
\isadelimML |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1783 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1784 |
\endisadelimML |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1785 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1786 |
\begin{isamarkuptext}% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1787 |
\medskip That position can be also printed in a message as |
40126 | 1788 |
follows:% |
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1789 |
\end{isamarkuptext}% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1790 |
\isamarkuptrue% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1791 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1792 |
\isadelimML |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1793 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1794 |
\endisadelimML |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1795 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1796 |
\isatagML |
40406 | 1797 |
\isacommand{ML{\isaliteral{5F}{\isacharunderscore}}command}\isamarkupfalse% |
1798 |
\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline |
|
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1799 |
\ \ writeln\isanewline |
40406 | 1800 |
\ \ \ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequote}}Look\ here{\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{5E}{\isacharcircum}}\ Position{\isaliteral{2E}{\isachardot}}str{\isaliteral{5F}{\isacharunderscore}}of\ {\isaliteral{28}{\isacharparenleft}}Binding{\isaliteral{2E}{\isachardot}}pos{\isaliteral{5F}{\isacharunderscore}}of\ % |
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1801 |
\isaantiq |
40406 | 1802 |
binding\ here{}% |
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1803 |
\endisaantiq |
40406 | 1804 |
{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\isanewline |
1805 |
{\isaliteral{2A7D}{\isacharverbatimclose}}% |
|
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1806 |
\endisatagML |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1807 |
{\isafoldML}% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1808 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1809 |
\isadelimML |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1810 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1811 |
\endisadelimML |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1812 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1813 |
\begin{isamarkuptext}% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1814 |
This illustrates a key virtue of formalized bindings as |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1815 |
opposed to raw specifications of base names: the system can use this |
40126 | 1816 |
additional information for feedback given to the user (error |
1817 |
messages etc.).% |
|
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1818 |
\end{isamarkuptext}% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1819 |
\isamarkuptrue% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1820 |
% |
30296 | 1821 |
\isadelimtheory |
1822 |
% |
|
1823 |
\endisadelimtheory |
|
1824 |
% |
|
1825 |
\isatagtheory |
|
1826 |
\isacommand{end}\isamarkupfalse% |
|
1827 |
% |
|
1828 |
\endisatagtheory |
|
1829 |
{\isafoldtheory}% |
|
1830 |
% |
|
1831 |
\isadelimtheory |
|
1832 |
% |
|
1833 |
\endisadelimtheory |
|
1834 |
\isanewline |
|
1835 |
\end{isabellebody}% |
|
1836 |
%%% Local Variables: |
|
1837 |
%%% mode: latex |
|
1838 |
%%% TeX-master: "root" |
|
1839 |
%%% End: |