author | wenzelm |
Mon, 08 Nov 2010 00:00:47 +0100 | |
changeset 40406 | 313a24b66a8d |
parent 40296 | ac4d75f86d97 |
child 40628 | 1b1484c3b163 |
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 |
|
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
267 |
\begin{rail} |
40241
56fad09655a5
discontinued obsolete ML antiquotation @{theory_ref};
wenzelm
parents:
40126
diff
changeset
|
268 |
'theory' nameref? |
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
269 |
; |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
270 |
\end{rail} |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
271 |
|
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
272 |
\begin{description} |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
273 |
|
40406 | 274 |
\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
|
275 |
current context --- as abstract value. |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
276 |
|
40406 | 277 |
\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
|
278 |
theory \isa{A} of the background theory of the current context |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
279 |
--- as abstract value. |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
280 |
|
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
281 |
\end{description}% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
282 |
\end{isamarkuptext}% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
283 |
\isamarkuptrue% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
284 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
285 |
\endisatagmlantiq |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
286 |
{\isafoldmlantiq}% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
287 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
288 |
\isadelimmlantiq |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
289 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
290 |
\endisadelimmlantiq |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
291 |
% |
30296 | 292 |
\isamarkupsubsection{Proof context \label{sec:context-proof}% |
293 |
} |
|
294 |
\isamarkuptrue% |
|
295 |
% |
|
296 |
\begin{isamarkuptext}% |
|
35001 | 297 |
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
|
298 |
back-reference to the theory from which it is derived. The \isa{init} operation creates a proof context from a given theory. |
35001 | 299 |
Modifications to draft theories are propagated to the proof context |
300 |
as usual, but there is also an explicit \isa{transfer} operation |
|
301 |
to force resynchronization with more substantial updates to the |
|
302 |
underlying theory. |
|
30296 | 303 |
|
35001 | 304 |
Entities derived in a proof context need to record logical |
30296 | 305 |
requirements explicitly, since there is no separate context |
35001 | 306 |
identification or symbolic inclusion as for theories. For example, |
307 |
hypotheses used in primitive derivations (cf.\ \secref{sec:thms}) |
|
40406 | 308 |
are recorded separately within the sequent \isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ {\isaliteral{5C3C7068693E}{\isasymphi}}}, just to |
35001 | 309 |
make double sure. Results could still leak into an alien proof |
310 |
context due to programming errors, but Isabelle/Isar includes some |
|
311 |
extra validity checks in critical positions, notably at the end of a |
|
312 |
sub-proof. |
|
30296 | 313 |
|
314 |
Proof contexts may be manipulated arbitrarily, although the common |
|
315 |
discipline is to follow block structure as a mental model: a given |
|
316 |
context is extended consecutively, and results are exported back |
|
35001 | 317 |
into the original context. Note that an Isar proof state models |
30296 | 318 |
block-structured reasoning explicitly, using a stack of proof |
35001 | 319 |
contexts internally. For various technical reasons, the background |
320 |
theory of an Isar proof state must not be changed while the proof is |
|
321 |
still under construction!% |
|
30296 | 322 |
\end{isamarkuptext}% |
323 |
\isamarkuptrue% |
|
324 |
% |
|
325 |
\isadelimmlref |
|
326 |
% |
|
327 |
\endisadelimmlref |
|
328 |
% |
|
329 |
\isatagmlref |
|
330 |
% |
|
331 |
\begin{isamarkuptext}% |
|
332 |
\begin{mldecls} |
|
333 |
\indexdef{}{ML type}{Proof.context}\verb|type Proof.context| \\ |
|
36611 | 334 |
\indexdef{}{ML}{ProofContext.init\_global}\verb|ProofContext.init_global: theory -> Proof.context| \\ |
30296 | 335 |
\indexdef{}{ML}{ProofContext.theory\_of}\verb|ProofContext.theory_of: Proof.context -> theory| \\ |
336 |
\indexdef{}{ML}{ProofContext.transfer}\verb|ProofContext.transfer: theory -> Proof.context -> Proof.context| \\ |
|
337 |
\end{mldecls} |
|
338 |
||
339 |
\begin{description} |
|
340 |
||
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
341 |
\item Type \verb|Proof.context| represents proof contexts. |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
342 |
Elements of this type are essentially pure values, with a sliding |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
343 |
reference to the background theory. |
30296 | 344 |
|
36611 | 345 |
\item \verb|ProofContext.init_global|~\isa{thy} produces a proof context |
30296 | 346 |
derived from \isa{thy}, initializing all data. |
347 |
||
348 |
\item \verb|ProofContext.theory_of|~\isa{ctxt} selects the |
|
349 |
background theory from \isa{ctxt}, dereferencing its internal |
|
350 |
\verb|theory_ref|. |
|
351 |
||
352 |
\item \verb|ProofContext.transfer|~\isa{thy\ ctxt} promotes the |
|
353 |
background theory of \isa{ctxt} to the super theory \isa{thy}. |
|
354 |
||
355 |
\end{description}% |
|
356 |
\end{isamarkuptext}% |
|
357 |
\isamarkuptrue% |
|
358 |
% |
|
359 |
\endisatagmlref |
|
360 |
{\isafoldmlref}% |
|
361 |
% |
|
362 |
\isadelimmlref |
|
363 |
% |
|
364 |
\endisadelimmlref |
|
365 |
% |
|
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
366 |
\isadelimmlantiq |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
367 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
368 |
\endisadelimmlantiq |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
369 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
370 |
\isatagmlantiq |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
371 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
372 |
\begin{isamarkuptext}% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
373 |
\begin{matharray}{rcl} |
40406 | 374 |
\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
|
375 |
\end{matharray} |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
376 |
|
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
377 |
\begin{description} |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
378 |
|
40406 | 379 |
\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
|
380 |
compile-time --- as abstract value. Independently of (local) theory |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
381 |
or proof mode, this always produces a meaningful result. |
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 |
This is probably the most common antiquotation in interactive |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
384 |
experimentation with ML inside Isar. |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
385 |
|
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
386 |
\end{description}% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
387 |
\end{isamarkuptext}% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
388 |
\isamarkuptrue% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
389 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
390 |
\endisatagmlantiq |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
391 |
{\isafoldmlantiq}% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
392 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
393 |
\isadelimmlantiq |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
394 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
395 |
\endisadelimmlantiq |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
396 |
% |
30296 | 397 |
\isamarkupsubsection{Generic contexts \label{sec:generic-context}% |
398 |
} |
|
399 |
\isamarkuptrue% |
|
400 |
% |
|
401 |
\begin{isamarkuptext}% |
|
402 |
A generic context is the disjoint sum of either a theory or proof |
|
403 |
context. Occasionally, this enables uniform treatment of generic |
|
404 |
context data, typically extra-logical information. Operations on |
|
405 |
generic contexts include the usual injections, partial selections, |
|
406 |
and combinators for lifting operations on either component of the |
|
407 |
disjoint sum. |
|
408 |
||
40406 | 409 |
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 | 410 |
can always be selected from the sum, while a proof context might |
35001 | 411 |
have to be constructed by an ad-hoc \isa{init} operation, which |
412 |
incurs a small runtime overhead.% |
|
30296 | 413 |
\end{isamarkuptext}% |
414 |
\isamarkuptrue% |
|
415 |
% |
|
416 |
\isadelimmlref |
|
417 |
% |
|
418 |
\endisadelimmlref |
|
419 |
% |
|
420 |
\isatagmlref |
|
421 |
% |
|
422 |
\begin{isamarkuptext}% |
|
423 |
\begin{mldecls} |
|
424 |
\indexdef{}{ML type}{Context.generic}\verb|type Context.generic| \\ |
|
425 |
\indexdef{}{ML}{Context.theory\_of}\verb|Context.theory_of: Context.generic -> theory| \\ |
|
426 |
\indexdef{}{ML}{Context.proof\_of}\verb|Context.proof_of: Context.generic -> Proof.context| \\ |
|
427 |
\end{mldecls} |
|
428 |
||
429 |
\begin{description} |
|
430 |
||
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
431 |
\item Type \verb|Context.generic| is the direct sum of \verb|theory| and \verb|Proof.context|, with the datatype |
30296 | 432 |
constructors \verb|Context.Theory| and \verb|Context.Proof|. |
433 |
||
434 |
\item \verb|Context.theory_of|~\isa{context} always produces a |
|
435 |
theory from the generic \isa{context}, using \verb|ProofContext.theory_of| as required. |
|
436 |
||
437 |
\item \verb|Context.proof_of|~\isa{context} always produces a |
|
36611 | 438 |
proof context from the generic \isa{context}, using \verb|ProofContext.init_global| as required (note that this re-initializes the |
30296 | 439 |
context data with each invocation). |
440 |
||
441 |
\end{description}% |
|
442 |
\end{isamarkuptext}% |
|
443 |
\isamarkuptrue% |
|
444 |
% |
|
445 |
\endisatagmlref |
|
446 |
{\isafoldmlref}% |
|
447 |
% |
|
448 |
\isadelimmlref |
|
449 |
% |
|
450 |
\endisadelimmlref |
|
451 |
% |
|
452 |
\isamarkupsubsection{Context data \label{sec:context-data}% |
|
453 |
} |
|
454 |
\isamarkuptrue% |
|
455 |
% |
|
456 |
\begin{isamarkuptext}% |
|
33524
a08e6c1cbc04
updated functor Theory_Data, Proof_Data, Generic_Data;
wenzelm
parents:
33174
diff
changeset
|
457 |
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
|
458 |
arbitrary (pure) data. New data types can be declared incrementally |
a08e6c1cbc04
updated functor Theory_Data, Proof_Data, Generic_Data;
wenzelm
parents:
33174
diff
changeset
|
459 |
at compile time. There are separate declaration mechanisms for any |
a08e6c1cbc04
updated functor Theory_Data, Proof_Data, Generic_Data;
wenzelm
parents:
33174
diff
changeset
|
460 |
of the three kinds of contexts: theory, proof, generic. |
30296 | 461 |
|
33524
a08e6c1cbc04
updated functor Theory_Data, Proof_Data, Generic_Data;
wenzelm
parents:
33174
diff
changeset
|
462 |
\paragraph{Theory data} declarations need to implement the following |
a08e6c1cbc04
updated functor Theory_Data, Proof_Data, Generic_Data;
wenzelm
parents:
33174
diff
changeset
|
463 |
SML signature: |
30296 | 464 |
|
465 |
\medskip |
|
466 |
\begin{tabular}{ll} |
|
40406 | 467 |
\isa{{\isaliteral{5C3C747970653E}{\isasymtype}}\ T} & representing type \\ |
468 |
\isa{{\isaliteral{5C3C76616C3E}{\isasymval}}\ empty{\isaliteral{3A}{\isacharcolon}}\ T} & empty default value \\ |
|
469 |
\isa{{\isaliteral{5C3C76616C3E}{\isasymval}}\ extend{\isaliteral{3A}{\isacharcolon}}\ T\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ T} & re-initialize on import \\ |
|
470 |
\isa{{\isaliteral{5C3C76616C3E}{\isasymval}}\ merge{\isaliteral{3A}{\isacharcolon}}\ T\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ T\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ T} & join on import \\ |
|
30296 | 471 |
\end{tabular} |
472 |
\medskip |
|
473 |
||
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
474 |
The \isa{empty} value acts as initial default for \emph{any} |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
475 |
theory that does not declare actual data content; \isa{extend} |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
476 |
is acts like a unitary version of \isa{merge}. |
30296 | 477 |
|
35001 | 478 |
Implementing \isa{merge} can be tricky. The general idea is |
40406 | 479 |
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 | 480 |
keeping the general order of things. The \verb|Library.merge| |
481 |
function on plain lists may serve as canonical template. |
|
482 |
||
483 |
Particularly note that shared parts of the data must not be |
|
484 |
duplicated by naive concatenation, or a theory graph that is like a |
|
485 |
chain of diamonds would cause an exponential blowup! |
|
486 |
||
33524
a08e6c1cbc04
updated functor Theory_Data, Proof_Data, Generic_Data;
wenzelm
parents:
33174
diff
changeset
|
487 |
\paragraph{Proof context data} declarations need to implement the |
a08e6c1cbc04
updated functor Theory_Data, Proof_Data, Generic_Data;
wenzelm
parents:
33174
diff
changeset
|
488 |
following SML signature: |
30296 | 489 |
|
490 |
\medskip |
|
491 |
\begin{tabular}{ll} |
|
40406 | 492 |
\isa{{\isaliteral{5C3C747970653E}{\isasymtype}}\ T} & representing type \\ |
493 |
\isa{{\isaliteral{5C3C76616C3E}{\isasymval}}\ init{\isaliteral{3A}{\isacharcolon}}\ theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ T} & produce initial value \\ |
|
30296 | 494 |
\end{tabular} |
495 |
\medskip |
|
496 |
||
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
497 |
The \isa{init} operation is supposed to produce a pure value |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
498 |
from the given background theory and should be somehow |
35001 | 499 |
``immediate''. Whenever a proof context is initialized, which |
500 |
happens frequently, the the system invokes the \isa{init} |
|
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
501 |
operation of \emph{all} theory data slots ever declared. This also |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
502 |
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
|
503 |
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
|
504 |
at most one, sometimes two data slots for its internal use. |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
505 |
Repeated data declarations to simulate a record type should be |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
506 |
avoided! |
30296 | 507 |
|
508 |
\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
|
509 |
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
|
510 |
predefined to select the current data value from the background |
a08e6c1cbc04
updated functor Theory_Data, Proof_Data, Generic_Data;
wenzelm
parents:
33174
diff
changeset
|
511 |
theory. |
30296 | 512 |
|
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
513 |
\bigskip Any of the above data declarations over type \isa{T} |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
514 |
result in an ML structure with the following signature: |
30296 | 515 |
|
516 |
\medskip |
|
517 |
\begin{tabular}{ll} |
|
40406 | 518 |
\isa{get{\isaliteral{3A}{\isacharcolon}}\ context\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ T} \\ |
519 |
\isa{put{\isaliteral{3A}{\isacharcolon}}\ T\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ context\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ context} \\ |
|
520 |
\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 | 521 |
\end{tabular} |
522 |
\medskip |
|
523 |
||
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
524 |
These other operations provide exclusive access for the particular |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
525 |
kind of context (theory, proof, or generic context). This interface |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
526 |
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
|
527 |
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
|
528 |
these operations private, an Isabelle/ML module may maintain |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
529 |
abstract values authentically.% |
30296 | 530 |
\end{isamarkuptext}% |
531 |
\isamarkuptrue% |
|
532 |
% |
|
533 |
\isadelimmlref |
|
534 |
% |
|
535 |
\endisadelimmlref |
|
536 |
% |
|
537 |
\isatagmlref |
|
538 |
% |
|
539 |
\begin{isamarkuptext}% |
|
540 |
\begin{mldecls} |
|
33524
a08e6c1cbc04
updated functor Theory_Data, Proof_Data, Generic_Data;
wenzelm
parents:
33174
diff
changeset
|
541 |
\indexdef{}{ML functor}{Theory\_Data}\verb|functor Theory_Data| \\ |
a08e6c1cbc04
updated functor Theory_Data, Proof_Data, Generic_Data;
wenzelm
parents:
33174
diff
changeset
|
542 |
\indexdef{}{ML functor}{Proof\_Data}\verb|functor Proof_Data| \\ |
a08e6c1cbc04
updated functor Theory_Data, Proof_Data, Generic_Data;
wenzelm
parents:
33174
diff
changeset
|
543 |
\indexdef{}{ML functor}{Generic\_Data}\verb|functor Generic_Data| \\ |
30296 | 544 |
\end{mldecls} |
545 |
||
546 |
\begin{description} |
|
547 |
||
40406 | 548 |
\item \verb|Theory_Data|\isa{{\isaliteral{28}{\isacharparenleft}}spec{\isaliteral{29}{\isacharparenright}}} declares data for |
30296 | 549 |
type \verb|theory| according to the specification provided as |
550 |
argument structure. The resulting structure provides data init and |
|
551 |
access operations as described above. |
|
552 |
||
40406 | 553 |
\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
|
554 |
\verb|Theory_Data| for type \verb|Proof.context|. |
30296 | 555 |
|
40406 | 556 |
\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
|
557 |
\verb|Theory_Data| for type \verb|Context.generic|. |
30296 | 558 |
|
559 |
\end{description}% |
|
560 |
\end{isamarkuptext}% |
|
561 |
\isamarkuptrue% |
|
562 |
% |
|
563 |
\endisatagmlref |
|
564 |
{\isafoldmlref}% |
|
565 |
% |
|
566 |
\isadelimmlref |
|
567 |
% |
|
568 |
\endisadelimmlref |
|
569 |
% |
|
35001 | 570 |
\isadelimmlex |
571 |
% |
|
572 |
\endisadelimmlex |
|
573 |
% |
|
574 |
\isatagmlex |
|
575 |
% |
|
576 |
\begin{isamarkuptext}% |
|
577 |
The following artificial example demonstrates theory |
|
578 |
data: we maintain a set of terms that are supposed to be wellformed |
|
579 |
wrt.\ the enclosing theory. The public interface is as follows:% |
|
580 |
\end{isamarkuptext}% |
|
581 |
\isamarkuptrue% |
|
582 |
% |
|
583 |
\endisatagmlex |
|
584 |
{\isafoldmlex}% |
|
585 |
% |
|
586 |
\isadelimmlex |
|
587 |
% |
|
588 |
\endisadelimmlex |
|
589 |
% |
|
590 |
\isadelimML |
|
591 |
% |
|
592 |
\endisadelimML |
|
593 |
% |
|
594 |
\isatagML |
|
595 |
\isacommand{ML}\isamarkupfalse% |
|
40406 | 596 |
\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline |
597 |
\ \ signature\ WELLFORMED{\isaliteral{5F}{\isacharunderscore}}TERMS\ {\isaliteral{3D}{\isacharequal}}\isanewline |
|
35001 | 598 |
\ \ sig\isanewline |
40406 | 599 |
\ \ \ \ val\ get{\isaliteral{3A}{\isacharcolon}}\ theory\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ term\ list\isanewline |
600 |
\ \ \ \ val\ add{\isaliteral{3A}{\isacharcolon}}\ term\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ theory\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ theory\isanewline |
|
601 |
\ \ end{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
|
602 |
{\isaliteral{2A7D}{\isacharverbatimclose}}% |
|
35001 | 603 |
\endisatagML |
604 |
{\isafoldML}% |
|
605 |
% |
|
606 |
\isadelimML |
|
607 |
% |
|
608 |
\endisadelimML |
|
609 |
% |
|
610 |
\begin{isamarkuptext}% |
|
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
611 |
The implementation uses private theory data internally, and |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
612 |
only exposes an operation that involves explicit argument checking |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
613 |
wrt.\ the given theory.% |
35001 | 614 |
\end{isamarkuptext}% |
615 |
\isamarkuptrue% |
|
616 |
% |
|
617 |
\isadelimML |
|
618 |
% |
|
619 |
\endisadelimML |
|
620 |
% |
|
621 |
\isatagML |
|
622 |
\isacommand{ML}\isamarkupfalse% |
|
40406 | 623 |
\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline |
624 |
\ \ structure\ Wellformed{\isaliteral{5F}{\isacharunderscore}}Terms{\isaliteral{3A}{\isacharcolon}}\ WELLFORMED{\isaliteral{5F}{\isacharunderscore}}TERMS\ {\isaliteral{3D}{\isacharequal}}\isanewline |
|
35001 | 625 |
\ \ struct\isanewline |
626 |
\isanewline |
|
40406 | 627 |
\ \ structure\ Terms\ {\isaliteral{3D}{\isacharequal}}\ Theory{\isaliteral{5F}{\isacharunderscore}}Data\isanewline |
628 |
\ \ {\isaliteral{28}{\isacharparenleft}}\isanewline |
|
629 |
\ \ \ \ type\ T\ {\isaliteral{3D}{\isacharequal}}\ term\ Ord{\isaliteral{5F}{\isacharunderscore}}List{\isaliteral{2E}{\isachardot}}T{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
|
630 |
\ \ \ \ val\ empty\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
|
631 |
\ \ \ \ val\ extend\ {\isaliteral{3D}{\isacharequal}}\ I{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
|
632 |
\ \ \ \ fun\ merge\ {\isaliteral{28}{\isacharparenleft}}ts{\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ ts{\isadigit{2}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\isanewline |
|
633 |
\ \ \ \ \ \ 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 |
|
634 |
\ \ {\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
|
35001 | 635 |
\isanewline |
40406 | 636 |
\ \ val\ get\ {\isaliteral{3D}{\isacharequal}}\ Terms{\isaliteral{2E}{\isachardot}}get{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
35001 | 637 |
\isanewline |
40406 | 638 |
\ \ 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
|
639 |
\ \ \ \ let\isanewline |
40406 | 640 |
\ \ \ \ \ \ 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
|
641 |
\ \ \ \ in\isanewline |
40406 | 642 |
\ \ \ \ \ \ 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 |
643 |
\ \ \ \ end{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
|
35001 | 644 |
\isanewline |
40406 | 645 |
\ \ end{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
646 |
{\isaliteral{2A7D}{\isacharverbatimclose}}% |
|
35001 | 647 |
\endisatagML |
648 |
{\isafoldML}% |
|
649 |
% |
|
650 |
\isadelimML |
|
651 |
% |
|
652 |
\endisadelimML |
|
653 |
% |
|
654 |
\begin{isamarkuptext}% |
|
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
655 |
Type \verb|term Ord_List.T| is used for reasonably |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
656 |
efficient representation of a set of terms: all operations are |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
657 |
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
|
658 |
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
|
659 |
data structure forces its own arrangement of elements. |
35001 | 660 |
|
661 |
Observe how the \verb|merge| operation joins the data slots of |
|
39688 | 662 |
the two constituents: \verb|Ord_List.union| prevents duplication of |
35001 | 663 |
common data from different branches, thus avoiding the danger of |
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
664 |
exponential blowup. Plain list append etc.\ must never be used for |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
665 |
theory data merges! |
35001 | 666 |
|
667 |
\medskip Our intended invariant is achieved as follows: |
|
668 |
\begin{enumerate} |
|
669 |
||
670 |
\item \verb|Wellformed_Terms.add| only admits terms that have passed |
|
671 |
the \verb|Sign.cert_term| check of the given theory at that point. |
|
672 |
||
673 |
\item Wellformedness in the sense of \verb|Sign.cert_term| is |
|
674 |
monotonic wrt.\ the sub-theory relation. So our data can move |
|
675 |
upwards in the hierarchy (via extension or merges), and maintain |
|
676 |
wellformedness without further checks. |
|
677 |
||
678 |
\end{enumerate} |
|
679 |
||
680 |
Note that all basic operations of the inference kernel (which |
|
681 |
includes \verb|Sign.cert_term|) observe this monotonicity principle, |
|
682 |
but other user-space tools don't. For example, fully-featured |
|
683 |
type-inference via \verb|Syntax.check_term| (cf.\ |
|
684 |
\secref{sec:term-check}) is not necessarily monotonic wrt.\ the |
|
685 |
background theory, since constraints of term constants can be |
|
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
686 |
modified by later declarations, for example. |
35001 | 687 |
|
688 |
In most cases, user-space context data does not have to take such |
|
689 |
invariants too seriously. The situation is different in the |
|
690 |
implementation of the inference kernel itself, which uses the very |
|
691 |
same data mechanisms for types, constants, axioms etc.% |
|
692 |
\end{isamarkuptext}% |
|
693 |
\isamarkuptrue% |
|
694 |
% |
|
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
695 |
\isamarkupsubsection{Configuration options \label{sec:config-options}% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
696 |
} |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
697 |
\isamarkuptrue% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
698 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
699 |
\begin{isamarkuptext}% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
700 |
A \emph{configuration option} is a named optional value of |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
701 |
some basic type (Boolean, integer, string) that is stored in the |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
702 |
context. It is a simple application of general context data |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
703 |
(\secref{sec:context-data}) that is sufficiently common to justify |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
704 |
customized setup, which includes some concrete declarations for |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
705 |
end-users using existing notation for attributes (cf.\ |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
706 |
\secref{sec:attributes}). |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
707 |
|
40406 | 708 |
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
|
709 |
variables in printed terms (cf.\ \secref{sec:read-print}). Its |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
710 |
value can be modified within Isar text like this:% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
711 |
\end{isamarkuptext}% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
712 |
\isamarkuptrue% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
713 |
\isacommand{declare}\isamarkupfalse% |
40406 | 714 |
\ {\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
|
715 |
\ \ % |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
716 |
\isamarkupcmt{declaration within (local) theory context% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
717 |
} |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
718 |
\isanewline |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
719 |
\isanewline |
40406 | 720 |
\isacommand{example{\isaliteral{5F}{\isacharunderscore}}proof}\isamarkupfalse% |
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
721 |
\isanewline |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
722 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
723 |
\isadelimproof |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
724 |
\ \ % |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
725 |
\endisadelimproof |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
726 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
727 |
\isatagproof |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
728 |
\isacommand{note}\isamarkupfalse% |
40406 | 729 |
\ {\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
|
730 |
\ \ \ \ % |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
731 |
\isamarkupcmt{declaration within proof (forward mode)% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
732 |
} |
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 |
\endisatagproof |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
735 |
{\isafoldproof}% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
736 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
737 |
\isadelimproof |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
738 |
\isanewline |
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 |
\endisadelimproof |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
741 |
\ \ \isacommand{term}\isamarkupfalse% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
742 |
\ x\isanewline |
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 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
749 |
\isatagproof |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
750 |
\isacommand{have}\isamarkupfalse% |
40406 | 751 |
\ {\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
|
752 |
\ \ \ \ \isacommand{using}\isamarkupfalse% |
40406 | 753 |
\ {\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
|
754 |
\ \ \ \ \ \ % |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
755 |
\isamarkupcmt{declaration within proof (backward mode)% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
756 |
} |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
757 |
\isanewline |
40406 | 758 |
\ \ \ \ \isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}\isamarkupfalse% |
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
759 |
\isanewline |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
760 |
\isacommand{qed}\isamarkupfalse% |
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 |
\endisatagproof |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
763 |
{\isafoldproof}% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
764 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
765 |
\isadelimproof |
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 |
\endisadelimproof |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
768 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
769 |
\begin{isamarkuptext}% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
770 |
Configuration options that are not set explicitly hold a |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
771 |
default value that can depend on the application context. This |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
772 |
allows to retrieve the value from another slot within the context, |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
773 |
or fall back on a global preference mechanism, for example. |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
774 |
|
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
775 |
The operations to declare configuration options and get/map their |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
776 |
values are modeled as direct replacements for historic global |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
777 |
references, only that the context is made explicit. This allows |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
778 |
easy configuration of tools, without relying on the execution order |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
779 |
as required for old-style mutable references.% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
780 |
\end{isamarkuptext}% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
781 |
\isamarkuptrue% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
782 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
783 |
\isadelimmlref |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
784 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
785 |
\endisadelimmlref |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
786 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
787 |
\isatagmlref |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
788 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
789 |
\begin{isamarkuptext}% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
790 |
\begin{mldecls} |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
791 |
\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
|
792 |
\indexdef{}{ML}{Config.map}\verb|Config.map: 'a Config.T -> ('a -> 'a) -> Proof.context -> Proof.context| \\ |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
793 |
\indexdef{}{ML}{Attrib.config\_bool}\verb|Attrib.config_bool: string -> (Context.generic -> bool) ->|\isasep\isanewline% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
794 |
\verb| bool Config.T * (theory -> theory)| \\ |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
795 |
\indexdef{}{ML}{Attrib.config\_int}\verb|Attrib.config_int: string -> (Context.generic -> int) ->|\isasep\isanewline% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
796 |
\verb| int Config.T * (theory -> theory)| \\ |
40291 | 797 |
\indexdef{}{ML}{Attrib.config\_real}\verb|Attrib.config_real: string -> (Context.generic -> real) ->|\isasep\isanewline% |
798 |
\verb| real Config.T * (theory -> theory)| \\ |
|
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
799 |
\indexdef{}{ML}{Attrib.config\_string}\verb|Attrib.config_string: string -> (Context.generic -> string) ->|\isasep\isanewline% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
800 |
\verb| string Config.T * (theory -> theory)| \\ |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
801 |
\end{mldecls} |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
802 |
|
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
803 |
\begin{description} |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
804 |
|
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
805 |
\item \verb|Config.get|~\isa{ctxt\ config} gets the value of |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
806 |
\isa{config} in the given context. |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
807 |
|
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
808 |
\item \verb|Config.map|~\isa{config\ f\ ctxt} updates the context |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
809 |
by updating the value of \isa{config}. |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
810 |
|
40406 | 811 |
\item \isa{{\isaliteral{28}{\isacharparenleft}}config{\isaliteral{2C}{\isacharcomma}}\ setup{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}}~\verb|Attrib.config_bool|~\isa{name\ default} creates a named configuration option of type |
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
812 |
\verb|bool|, with the given \isa{default} depending on the |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
813 |
application context. The resulting \isa{config} can be used to |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
814 |
get/map its value in a given context. The \isa{setup} function |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
815 |
needs to be applied to the theory initially, in order to make |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
816 |
concrete declaration syntax available to the user. |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
817 |
|
40291 | 818 |
\item \verb|Attrib.config_int|, \verb|Attrib.config_real|, and \verb|Attrib.config_string| work like \verb|Attrib.config_bool|, but for |
819 |
types \verb|int| and \verb|string|, respectively. |
|
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
820 |
|
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
821 |
\end{description}% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
822 |
\end{isamarkuptext}% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
823 |
\isamarkuptrue% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
824 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
825 |
\endisatagmlref |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
826 |
{\isafoldmlref}% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
827 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
828 |
\isadelimmlref |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
829 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
830 |
\endisadelimmlref |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
831 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
832 |
\isadelimmlex |
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 |
\endisadelimmlex |
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 |
\isatagmlex |
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 |
\begin{isamarkuptext}% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
839 |
The following example shows how to declare and use a |
40406 | 840 |
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
|
841 |
default value \verb|false|.% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
842 |
\end{isamarkuptext}% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
843 |
\isamarkuptrue% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
844 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
845 |
\endisatagmlex |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
846 |
{\isafoldmlex}% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
847 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
848 |
\isadelimmlex |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
849 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
850 |
\endisadelimmlex |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
851 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
852 |
\isadelimML |
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 |
\endisadelimML |
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 |
\isatagML |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
857 |
\isacommand{ML}\isamarkupfalse% |
40406 | 858 |
\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline |
859 |
\ \ val\ {\isaliteral{28}{\isacharparenleft}}my{\isaliteral{5F}{\isacharunderscore}}flag{\isaliteral{2C}{\isacharcomma}}\ my{\isaliteral{5F}{\isacharunderscore}}flag{\isaliteral{5F}{\isacharunderscore}}setup{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\isanewline |
|
860 |
\ \ \ \ Attrib{\isaliteral{2E}{\isachardot}}config{\isaliteral{5F}{\isacharunderscore}}bool\ {\isaliteral{22}{\isachardoublequote}}my{\isaliteral{5F}{\isacharunderscore}}flag{\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{28}{\isacharparenleft}}K\ false{\isaliteral{29}{\isacharparenright}}\isanewline |
|
861 |
{\isaliteral{2A7D}{\isacharverbatimclose}}\isanewline |
|
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
862 |
\isacommand{setup}\isamarkupfalse% |
40406 | 863 |
\ my{\isaliteral{5F}{\isacharunderscore}}flag{\isaliteral{5F}{\isacharunderscore}}setup% |
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
864 |
\endisatagML |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
865 |
{\isafoldML}% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
866 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
867 |
\isadelimML |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
868 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
869 |
\endisadelimML |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
870 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
871 |
\begin{isamarkuptext}% |
40406 | 872 |
Now the user can refer to \hyperlink{attribute.my-flag}{\mbox{\isa{my{\isaliteral{5F}{\isacharunderscore}}flag}}} in |
40126 | 873 |
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
|
874 |
context via \verb|Config.get|.% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
875 |
\end{isamarkuptext}% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
876 |
\isamarkuptrue% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
877 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
878 |
\isadelimML |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
879 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
880 |
\endisadelimML |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
881 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
882 |
\isatagML |
40406 | 883 |
\isacommand{ML{\isaliteral{5F}{\isacharunderscore}}val}\isamarkupfalse% |
884 |
\ {\isaliteral{7B2A}{\isacharverbatimopen}}\ % |
|
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
885 |
\isaantiq |
40406 | 886 |
assert{}% |
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
887 |
\endisaantiq |
40406 | 888 |
\ {\isaliteral{28}{\isacharparenleft}}Config{\isaliteral{2E}{\isachardot}}get\ % |
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
889 |
\isaantiq |
40406 | 890 |
context{}% |
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
891 |
\endisaantiq |
40406 | 892 |
\ 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
|
893 |
\endisatagML |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
894 |
{\isafoldML}% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
895 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
896 |
\isadelimML |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
897 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
898 |
\endisadelimML |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
899 |
\isanewline |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
900 |
\isanewline |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
901 |
\isacommand{declare}\isamarkupfalse% |
40406 | 902 |
\ {\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
|
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 |
\isanewline |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
906 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
907 |
\endisadelimML |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
908 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
909 |
\isatagML |
40406 | 910 |
\isacommand{ML{\isaliteral{5F}{\isacharunderscore}}val}\isamarkupfalse% |
911 |
\ {\isaliteral{7B2A}{\isacharverbatimopen}}\ % |
|
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
912 |
\isaantiq |
40406 | 913 |
assert{}% |
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
914 |
\endisaantiq |
40406 | 915 |
\ {\isaliteral{28}{\isacharparenleft}}Config{\isaliteral{2E}{\isachardot}}get\ % |
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
916 |
\isaantiq |
40406 | 917 |
context{}% |
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
918 |
\endisaantiq |
40406 | 919 |
\ 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
|
920 |
\endisatagML |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
921 |
{\isafoldML}% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
922 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
923 |
\isadelimML |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
924 |
\isanewline |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
925 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
926 |
\endisadelimML |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
927 |
\isanewline |
40406 | 928 |
\isacommand{example{\isaliteral{5F}{\isacharunderscore}}proof}\isamarkupfalse% |
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
929 |
\isanewline |
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 |
\isadelimproof |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
932 |
\ \ % |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
933 |
\endisadelimproof |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
934 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
935 |
\isatagproof |
40406 | 936 |
\isacommand{{\isaliteral{7B}{\isacharbraceleft}}}\isamarkupfalse% |
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
937 |
\isanewline |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
938 |
\ \ \ \ \isacommand{note}\isamarkupfalse% |
40406 | 939 |
\ {\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
|
940 |
\endisatagproof |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
941 |
{\isafoldproof}% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
942 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
943 |
\isadelimproof |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
944 |
\isanewline |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
945 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
946 |
\endisadelimproof |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
947 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
948 |
\isadelimML |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
949 |
\ \ \ \ % |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
950 |
\endisadelimML |
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 |
\isatagML |
40406 | 953 |
\isacommand{ML{\isaliteral{5F}{\isacharunderscore}}val}\isamarkupfalse% |
954 |
\ {\isaliteral{7B2A}{\isacharverbatimopen}}\ % |
|
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
955 |
\isaantiq |
40406 | 956 |
assert{}% |
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
957 |
\endisaantiq |
40406 | 958 |
\ {\isaliteral{28}{\isacharparenleft}}Config{\isaliteral{2E}{\isachardot}}get\ % |
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
959 |
\isaantiq |
40406 | 960 |
context{}% |
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
961 |
\endisaantiq |
40406 | 962 |
\ 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
|
963 |
\endisatagML |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
964 |
{\isafoldML}% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
965 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
966 |
\isadelimML |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
967 |
\isanewline |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
968 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
969 |
\endisadelimML |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
970 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
971 |
\isadelimproof |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
972 |
\ \ % |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
973 |
\endisadelimproof |
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 |
\isatagproof |
40406 | 976 |
\isacommand{{\isaliteral{7D}{\isacharbraceright}}}\isamarkupfalse% |
39885
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 |
\endisatagproof |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
979 |
{\isafoldproof}% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
980 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
981 |
\isadelimproof |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
982 |
\isanewline |
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 |
\endisadelimproof |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
985 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
986 |
\isadelimML |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
987 |
\ \ % |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
988 |
\endisadelimML |
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 |
\isatagML |
40406 | 991 |
\isacommand{ML{\isaliteral{5F}{\isacharunderscore}}val}\isamarkupfalse% |
992 |
\ {\isaliteral{7B2A}{\isacharverbatimopen}}\ % |
|
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
993 |
\isaantiq |
40406 | 994 |
assert{}% |
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
995 |
\endisaantiq |
40406 | 996 |
\ {\isaliteral{28}{\isacharparenleft}}Config{\isaliteral{2E}{\isachardot}}get\ % |
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
997 |
\isaantiq |
40406 | 998 |
context{}% |
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
999 |
\endisaantiq |
40406 | 1000 |
\ 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
|
1001 |
\endisatagML |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1002 |
{\isafoldML}% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1003 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1004 |
\isadelimML |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1005 |
\isanewline |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1006 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1007 |
\endisadelimML |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1008 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1009 |
\isadelimproof |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1010 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1011 |
\endisadelimproof |
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 |
\isatagproof |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1014 |
\isacommand{qed}\isamarkupfalse% |
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 |
\endisatagproof |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1017 |
{\isafoldproof}% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1018 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1019 |
\isadelimproof |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1020 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1021 |
\endisadelimproof |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1022 |
% |
40291 | 1023 |
\begin{isamarkuptext}% |
1024 |
Here is another example involving ML type \verb|real| |
|
1025 |
(floating-point numbers).% |
|
1026 |
\end{isamarkuptext}% |
|
1027 |
\isamarkuptrue% |
|
1028 |
% |
|
1029 |
\isadelimML |
|
1030 |
% |
|
1031 |
\endisadelimML |
|
1032 |
% |
|
1033 |
\isatagML |
|
1034 |
\isacommand{ML}\isamarkupfalse% |
|
40406 | 1035 |
\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline |
1036 |
\ \ val\ {\isaliteral{28}{\isacharparenleft}}airspeed{\isaliteral{5F}{\isacharunderscore}}velocity{\isaliteral{2C}{\isacharcomma}}\ airspeed{\isaliteral{5F}{\isacharunderscore}}velocity{\isaliteral{5F}{\isacharunderscore}}setup{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\isanewline |
|
1037 |
\ \ \ \ Attrib{\isaliteral{2E}{\isachardot}}config{\isaliteral{5F}{\isacharunderscore}}real\ {\isaliteral{22}{\isachardoublequote}}airspeed{\isaliteral{5F}{\isacharunderscore}}velocity{\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{28}{\isacharparenleft}}K\ {\isadigit{0}}{\isaliteral{2E}{\isachardot}}{\isadigit{0}}{\isaliteral{29}{\isacharparenright}}\isanewline |
|
1038 |
{\isaliteral{2A7D}{\isacharverbatimclose}}\isanewline |
|
40291 | 1039 |
\isacommand{setup}\isamarkupfalse% |
40406 | 1040 |
\ airspeed{\isaliteral{5F}{\isacharunderscore}}velocity{\isaliteral{5F}{\isacharunderscore}}setup% |
40291 | 1041 |
\endisatagML |
1042 |
{\isafoldML}% |
|
1043 |
% |
|
1044 |
\isadelimML |
|
1045 |
% |
|
1046 |
\endisadelimML |
|
1047 |
\isanewline |
|
1048 |
\isanewline |
|
1049 |
\isacommand{declare}\isamarkupfalse% |
|
40406 | 1050 |
\ {\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 | 1051 |
\isacommand{declare}\isamarkupfalse% |
40406 | 1052 |
\ {\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 | 1053 |
\isamarkupsection{Names \label{sec:names}% |
1054 |
} |
|
1055 |
\isamarkuptrue% |
|
1056 |
% |
|
1057 |
\begin{isamarkuptext}% |
|
1058 |
In principle, a name is just a string, but there are various |
|
35001 | 1059 |
conventions for representing additional structure. For example, |
40406 | 1060 |
``\isa{Foo{\isaliteral{2E}{\isachardot}}bar{\isaliteral{2E}{\isachardot}}baz}'' is considered as a long name consisting of |
1061 |
qualifier \isa{Foo{\isaliteral{2E}{\isachardot}}bar} and base name \isa{baz}. The |
|
35001 | 1062 |
individual constituents of a name may have further substructure, |
1063 |
e.g.\ the string ``\verb,\,\verb,<alpha>,'' encodes as a single |
|
1064 |
symbol. |
|
1065 |
||
1066 |
\medskip Subsequently, we shall introduce specific categories of |
|
1067 |
names. Roughly speaking these correspond to logical entities as |
|
1068 |
follows: |
|
1069 |
\begin{itemize} |
|
1070 |
||
1071 |
\item Basic names (\secref{sec:basic-name}): free and bound |
|
1072 |
variables. |
|
1073 |
||
1074 |
\item Indexed names (\secref{sec:indexname}): schematic variables. |
|
1075 |
||
1076 |
\item Long names (\secref{sec:long-name}): constants of any kind |
|
1077 |
(type constructors, term constants, other concepts defined in user |
|
1078 |
space). Such entities are typically managed via name spaces |
|
1079 |
(\secref{sec:name-space}). |
|
1080 |
||
1081 |
\end{itemize}% |
|
30296 | 1082 |
\end{isamarkuptext}% |
1083 |
\isamarkuptrue% |
|
1084 |
% |
|
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1085 |
\isamarkupsubsection{Strings of symbols \label{sec:symbols}% |
30296 | 1086 |
} |
1087 |
\isamarkuptrue% |
|
1088 |
% |
|
1089 |
\begin{isamarkuptext}% |
|
35001 | 1090 |
A \emph{symbol} constitutes the smallest textual unit in |
1091 |
Isabelle --- raw ML characters are normally not encountered at all! |
|
1092 |
Isabelle strings consist of a sequence of symbols, represented as a |
|
1093 |
packed string or an exploded list of strings. Each symbol is in |
|
1094 |
itself a small string, which has either one of the following forms: |
|
30296 | 1095 |
|
1096 |
\begin{enumerate} |
|
1097 |
||
37533
d775bd70f571
explicit treatment of UTF8 character sequences as Isabelle symbols;
wenzelm
parents:
36611
diff
changeset
|
1098 |
\item a single ASCII character ``\isa{c}'', for example |
d775bd70f571
explicit treatment of UTF8 character sequences as Isabelle symbols;
wenzelm
parents:
36611
diff
changeset
|
1099 |
``\verb,a,'', |
d775bd70f571
explicit treatment of UTF8 character sequences as Isabelle symbols;
wenzelm
parents:
36611
diff
changeset
|
1100 |
|
d775bd70f571
explicit treatment of UTF8 character sequences as Isabelle symbols;
wenzelm
parents:
36611
diff
changeset
|
1101 |
\item a codepoint according to UTF8 (non-ASCII byte sequence), |
30296 | 1102 |
|
1103 |
\item a regular symbol ``\verb,\,\verb,<,\isa{ident}\verb,>,'', |
|
1104 |
for example ``\verb,\,\verb,<alpha>,'', |
|
1105 |
||
1106 |
\item a control symbol ``\verb,\,\verb,<^,\isa{ident}\verb,>,'', |
|
1107 |
for example ``\verb,\,\verb,<^bold>,'', |
|
1108 |
||
1109 |
\item a raw symbol ``\verb,\,\verb,<^raw:,\isa{text}\verb,>,'' |
|
35001 | 1110 |
where \isa{text} consists of printable characters excluding |
30296 | 1111 |
``\verb,.,'' and ``\verb,>,'', for example |
1112 |
``\verb,\,\verb,<^raw:$\sum_{i = 1}^n$>,'', |
|
1113 |
||
1114 |
\item a numbered raw control symbol ``\verb,\,\verb,<^raw,\isa{n}\verb,>, where \isa{n} consists of digits, for example |
|
1115 |
``\verb,\,\verb,<^raw42>,''. |
|
1116 |
||
1117 |
\end{enumerate} |
|
1118 |
||
40406 | 1119 |
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
|
1120 |
control symbols, but a fixed collection of standard symbols is |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1121 |
treated specifically. For example, ``\verb,\,\verb,<alpha>,'' is |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1122 |
classified as a letter, which means it may occur within regular |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1123 |
Isabelle identifiers. |
30296 | 1124 |
|
37533
d775bd70f571
explicit treatment of UTF8 character sequences as Isabelle symbols;
wenzelm
parents:
36611
diff
changeset
|
1125 |
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
|
1126 |
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
|
1127 |
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
|
1128 |
that well-formed code sequences are recognized |
d775bd70f571
explicit treatment of UTF8 character sequences as Isabelle symbols;
wenzelm
parents:
36611
diff
changeset
|
1129 |
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
|
1130 |
in some special punctuation characters that even have replacements |
d775bd70f571
explicit treatment of UTF8 character sequences as Isabelle symbols;
wenzelm
parents:
36611
diff
changeset
|
1131 |
within the standard collection of Isabelle symbols. Text consisting |
d775bd70f571
explicit treatment of UTF8 character sequences as Isabelle symbols;
wenzelm
parents:
36611
diff
changeset
|
1132 |
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
|
1133 |
Unicode provides its own collection of mathematical symbols, but |
d775bd70f571
explicit treatment of UTF8 character sequences as Isabelle symbols;
wenzelm
parents:
36611
diff
changeset
|
1134 |
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
|
1135 |
collection of Isabelle regular symbols. |
30296 | 1136 |
|
1137 |
\medskip Output of Isabelle symbols depends on the print mode |
|
1138 |
(\secref{print-mode}). For example, the standard {\LaTeX} setup of |
|
1139 |
the Isabelle document preparation system would present |
|
40406 | 1140 |
``\verb,\,\verb,<alpha>,'' as \isa{{\isaliteral{5C3C616C7068613E}{\isasymalpha}}}, and |
1141 |
``\verb,\,\verb,<^bold>,\verb,\,\verb,<alpha>,'' as \isa{\isaliteral{5C3C5E626F6C643E}{}\isactrlbold {\isaliteral{5C3C616C7068613E}{\isasymalpha}}}. On-screen rendering usually works by mapping a finite |
|
35001 | 1142 |
subset of Isabelle symbols to suitable Unicode characters.% |
30296 | 1143 |
\end{isamarkuptext}% |
1144 |
\isamarkuptrue% |
|
1145 |
% |
|
1146 |
\isadelimmlref |
|
1147 |
% |
|
1148 |
\endisadelimmlref |
|
1149 |
% |
|
1150 |
\isatagmlref |
|
1151 |
% |
|
1152 |
\begin{isamarkuptext}% |
|
1153 |
\begin{mldecls} |
|
35001 | 1154 |
\indexdef{}{ML type}{Symbol.symbol}\verb|type Symbol.symbol = string| \\ |
30296 | 1155 |
\indexdef{}{ML}{Symbol.explode}\verb|Symbol.explode: string -> Symbol.symbol list| \\ |
1156 |
\indexdef{}{ML}{Symbol.is\_letter}\verb|Symbol.is_letter: Symbol.symbol -> bool| \\ |
|
1157 |
\indexdef{}{ML}{Symbol.is\_digit}\verb|Symbol.is_digit: Symbol.symbol -> bool| \\ |
|
1158 |
\indexdef{}{ML}{Symbol.is\_quasi}\verb|Symbol.is_quasi: Symbol.symbol -> bool| \\ |
|
1159 |
\indexdef{}{ML}{Symbol.is\_blank}\verb|Symbol.is_blank: Symbol.symbol -> bool| \\ |
|
1160 |
\end{mldecls} |
|
1161 |
\begin{mldecls} |
|
1162 |
\indexdef{}{ML type}{Symbol.sym}\verb|type Symbol.sym| \\ |
|
1163 |
\indexdef{}{ML}{Symbol.decode}\verb|Symbol.decode: Symbol.symbol -> Symbol.sym| \\ |
|
1164 |
\end{mldecls} |
|
1165 |
||
1166 |
\begin{description} |
|
1167 |
||
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1168 |
\item Type \verb|Symbol.symbol| represents individual Isabelle |
35001 | 1169 |
symbols. |
30296 | 1170 |
|
1171 |
\item \verb|Symbol.explode|~\isa{str} produces a symbol list |
|
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1172 |
from the packed form. This function supersedes \verb|String.explode| for virtually all purposes of manipulating text in |
35001 | 1173 |
Isabelle!\footnote{The runtime overhead for exploded strings is |
1174 |
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
|
1175 |
be a singleton string do not require extra memory in Poly/ML.} |
30296 | 1176 |
|
1177 |
\item \verb|Symbol.is_letter|, \verb|Symbol.is_digit|, \verb|Symbol.is_quasi|, \verb|Symbol.is_blank| classify standard |
|
1178 |
symbols according to fixed syntactic conventions of Isabelle, cf.\ |
|
1179 |
\cite{isabelle-isar-ref}. |
|
1180 |
||
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1181 |
\item Type \verb|Symbol.sym| is a concrete datatype that |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1182 |
represents the different kinds of symbols explicitly, with |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1183 |
constructors \verb|Symbol.Char|, \verb|Symbol.Sym|, \verb|Symbol.UTF8|, \verb|Symbol.Ctrl|, \verb|Symbol.Raw|. |
30296 | 1184 |
|
1185 |
\item \verb|Symbol.decode| converts the string representation of a |
|
1186 |
symbol into the datatype version. |
|
1187 |
||
35001 | 1188 |
\end{description} |
1189 |
||
1190 |
\paragraph{Historical note.} In the original SML90 standard the |
|
1191 |
primitive ML type \verb|char| did not exists, and the basic \verb|explode: string -> string list| operation would produce a list of |
|
1192 |
singleton strings as in Isabelle/ML today. When SML97 came out, |
|
1193 |
Isabelle did not adopt its slightly anachronistic 8-bit characters, |
|
1194 |
but the idea of exploding a string into a list of small strings was |
|
1195 |
extended to ``symbols'' as explained above. Thus Isabelle sources |
|
1196 |
can refer to an infinite store of user-defined symbols, without |
|
1197 |
having to worry about the multitude of Unicode encodings.% |
|
30296 | 1198 |
\end{isamarkuptext}% |
1199 |
\isamarkuptrue% |
|
1200 |
% |
|
1201 |
\endisatagmlref |
|
1202 |
{\isafoldmlref}% |
|
1203 |
% |
|
1204 |
\isadelimmlref |
|
1205 |
% |
|
1206 |
\endisadelimmlref |
|
1207 |
% |
|
35001 | 1208 |
\isamarkupsubsection{Basic names \label{sec:basic-name}% |
30296 | 1209 |
} |
1210 |
\isamarkuptrue% |
|
1211 |
% |
|
1212 |
\begin{isamarkuptext}% |
|
1213 |
A \emph{basic name} essentially consists of a single Isabelle |
|
1214 |
identifier. There are conventions to mark separate classes of basic |
|
1215 |
names, by attaching a suffix of underscores: one underscore means |
|
1216 |
\emph{internal name}, two underscores means \emph{Skolem name}, |
|
1217 |
three underscores means \emph{internal Skolem name}. |
|
1218 |
||
1219 |
For example, the basic name \isa{foo} has the internal version |
|
40406 | 1220 |
\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 | 1221 |
|
1222 |
These special versions provide copies of the basic name space, apart |
|
1223 |
from anything that normally appears in the user text. For example, |
|
1224 |
system generated variables in Isar proof contexts are usually marked |
|
35001 | 1225 |
as internal, which prevents mysterious names like \isa{xaa} to |
1226 |
appear in human-readable text. |
|
30296 | 1227 |
|
1228 |
\medskip Manipulating binding scopes often requires on-the-fly |
|
1229 |
renamings. A \emph{name context} contains a collection of already |
|
1230 |
used names. The \isa{declare} operation adds names to the |
|
1231 |
context. |
|
1232 |
||
1233 |
The \isa{invents} operation derives a number of fresh names from |
|
1234 |
a given starting point. For example, the first three names derived |
|
1235 |
from \isa{a} are \isa{a}, \isa{b}, \isa{c}. |
|
1236 |
||
1237 |
The \isa{variants} operation produces fresh names by |
|
40406 | 1238 |
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 | 1239 |
step picks the next unused variant from this sequence.% |
1240 |
\end{isamarkuptext}% |
|
1241 |
\isamarkuptrue% |
|
1242 |
% |
|
1243 |
\isadelimmlref |
|
1244 |
% |
|
1245 |
\endisadelimmlref |
|
1246 |
% |
|
1247 |
\isatagmlref |
|
1248 |
% |
|
1249 |
\begin{isamarkuptext}% |
|
1250 |
\begin{mldecls} |
|
1251 |
\indexdef{}{ML}{Name.internal}\verb|Name.internal: string -> string| \\ |
|
1252 |
\indexdef{}{ML}{Name.skolem}\verb|Name.skolem: string -> string| \\ |
|
1253 |
\end{mldecls} |
|
1254 |
\begin{mldecls} |
|
1255 |
\indexdef{}{ML type}{Name.context}\verb|type Name.context| \\ |
|
1256 |
\indexdef{}{ML}{Name.context}\verb|Name.context: Name.context| \\ |
|
1257 |
\indexdef{}{ML}{Name.declare}\verb|Name.declare: string -> Name.context -> Name.context| \\ |
|
1258 |
\indexdef{}{ML}{Name.invents}\verb|Name.invents: Name.context -> string -> int -> string list| \\ |
|
1259 |
\indexdef{}{ML}{Name.variants}\verb|Name.variants: string list -> Name.context -> string list * Name.context| \\ |
|
1260 |
\end{mldecls} |
|
35001 | 1261 |
\begin{mldecls} |
1262 |
\indexdef{}{ML}{Variable.names\_of}\verb|Variable.names_of: Proof.context -> Name.context| \\ |
|
1263 |
\end{mldecls} |
|
30296 | 1264 |
|
1265 |
\begin{description} |
|
1266 |
||
1267 |
\item \verb|Name.internal|~\isa{name} produces an internal name |
|
1268 |
by adding one underscore. |
|
1269 |
||
1270 |
\item \verb|Name.skolem|~\isa{name} produces a Skolem name by |
|
1271 |
adding two underscores. |
|
1272 |
||
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1273 |
\item Type \verb|Name.context| represents the context of already |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1274 |
used names; the initial value is \verb|Name.context|. |
30296 | 1275 |
|
1276 |
\item \verb|Name.declare|~\isa{name} enters a used name into the |
|
1277 |
context. |
|
1278 |
||
1279 |
\item \verb|Name.invents|~\isa{context\ name\ n} produces \isa{n} fresh names derived from \isa{name}. |
|
1280 |
||
1281 |
\item \verb|Name.variants|~\isa{names\ context} produces fresh |
|
1282 |
variants of \isa{names}; the result is entered into the context. |
|
1283 |
||
35001 | 1284 |
\item \verb|Variable.names_of|~\isa{ctxt} retrieves the context |
1285 |
of declared type and term variable names. Projecting a proof |
|
1286 |
context down to a primitive name context is occasionally useful when |
|
1287 |
invoking lower-level operations. Regular management of ``fresh |
|
1288 |
variables'' is done by suitable operations of structure \verb|Variable|, which is also able to provide an official status of |
|
1289 |
``locally fixed variable'' within the logical environment (cf.\ |
|
1290 |
\secref{sec:variables}). |
|
1291 |
||
30296 | 1292 |
\end{description}% |
1293 |
\end{isamarkuptext}% |
|
1294 |
\isamarkuptrue% |
|
1295 |
% |
|
1296 |
\endisatagmlref |
|
1297 |
{\isafoldmlref}% |
|
1298 |
% |
|
1299 |
\isadelimmlref |
|
1300 |
% |
|
1301 |
\endisadelimmlref |
|
1302 |
% |
|
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1303 |
\isadelimmlex |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1304 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1305 |
\endisadelimmlex |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1306 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1307 |
\isatagmlex |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1308 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1309 |
\begin{isamarkuptext}% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1310 |
The following simple examples demonstrate how to produce |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1311 |
fresh names from the initial \verb|Name.context|.% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1312 |
\end{isamarkuptext}% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1313 |
\isamarkuptrue% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1314 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1315 |
\endisatagmlex |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1316 |
{\isafoldmlex}% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1317 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1318 |
\isadelimmlex |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1319 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1320 |
\endisadelimmlex |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1321 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1322 |
\isadelimML |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1323 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1324 |
\endisadelimML |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1325 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1326 |
\isatagML |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1327 |
\isacommand{ML}\isamarkupfalse% |
40406 | 1328 |
\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline |
1329 |
\ \ 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
|
1330 |
\ \ % |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1331 |
\isaantiq |
40406 | 1332 |
assert{}% |
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1333 |
\endisaantiq |
40406 | 1334 |
\ {\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
|
1335 |
\isanewline |
40406 | 1336 |
\ \ val\ list{\isadigit{2}}\ {\isaliteral{3D}{\isacharequal}}\isanewline |
1337 |
\ \ \ \ {\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
|
1338 |
\ \ % |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1339 |
\isaantiq |
40406 | 1340 |
assert{}% |
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1341 |
\endisaantiq |
40406 | 1342 |
\ {\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 |
1343 |
{\isaliteral{2A7D}{\isacharverbatimclose}}% |
|
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1344 |
\endisatagML |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1345 |
{\isafoldML}% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1346 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1347 |
\isadelimML |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1348 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1349 |
\endisadelimML |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1350 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1351 |
\begin{isamarkuptext}% |
40126 | 1352 |
\medskip The same works relatively to the formal context as |
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1353 |
follows.% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1354 |
\end{isamarkuptext}% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1355 |
\isamarkuptrue% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1356 |
\isacommand{locale}\isamarkupfalse% |
40406 | 1357 |
\ 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
|
1358 |
\isakeyword{begin}\isanewline |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1359 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1360 |
\isadelimML |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1361 |
\isanewline |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1362 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1363 |
\endisadelimML |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1364 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1365 |
\isatagML |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1366 |
\isacommand{ML}\isamarkupfalse% |
40406 | 1367 |
\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline |
1368 |
\ \ 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
|
1369 |
\isaantiq |
40406 | 1370 |
context{}% |
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1371 |
\endisaantiq |
40406 | 1372 |
{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1373 |
\isanewline |
40406 | 1374 |
\ \ 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
|
1375 |
\ \ % |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1376 |
\isaantiq |
40406 | 1377 |
assert{}% |
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1378 |
\endisaantiq |
40406 | 1379 |
\ {\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
|
1380 |
\isanewline |
40406 | 1381 |
\ \ val\ list{\isadigit{2}}\ {\isaliteral{3D}{\isacharequal}}\isanewline |
1382 |
\ \ \ \ {\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
|
1383 |
\ \ % |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1384 |
\isaantiq |
40406 | 1385 |
assert{}% |
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1386 |
\endisaantiq |
40406 | 1387 |
\ {\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 |
1388 |
{\isaliteral{2A7D}{\isacharverbatimclose}}% |
|
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1389 |
\endisatagML |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1390 |
{\isafoldML}% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1391 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1392 |
\isadelimML |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1393 |
\isanewline |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1394 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1395 |
\endisadelimML |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1396 |
\isanewline |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1397 |
\isacommand{end}\isamarkupfalse% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1398 |
% |
35001 | 1399 |
\isamarkupsubsection{Indexed names \label{sec:indexname}% |
30296 | 1400 |
} |
1401 |
\isamarkuptrue% |
|
1402 |
% |
|
1403 |
\begin{isamarkuptext}% |
|
1404 |
An \emph{indexed name} (or \isa{indexname}) is a pair of a basic |
|
1405 |
name and a natural number. This representation allows efficient |
|
1406 |
renaming by incrementing the second component only. The canonical |
|
1407 |
way to rename two collections of indexnames apart from each other is |
|
1408 |
this: determine the maximum index \isa{maxidx} of the first |
|
1409 |
collection, then increment all indexes of the second collection by |
|
40406 | 1410 |
\isa{maxidx\ {\isaliteral{2B}{\isacharplus}}\ {\isadigit{1}}}; the maximum index of an empty collection is |
1411 |
\isa{{\isaliteral{2D}{\isacharminus}}{\isadigit{1}}}. |
|
30296 | 1412 |
|
35001 | 1413 |
Occasionally, basic names are injected into the same pair type of |
40406 | 1414 |
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 | 1415 |
name \isa{x}. |
30296 | 1416 |
|
1417 |
\medskip Isabelle syntax observes the following rules for |
|
40406 | 1418 |
representing an indexname \isa{{\isaliteral{28}{\isacharparenleft}}x{\isaliteral{2C}{\isacharcomma}}\ i{\isaliteral{29}{\isacharparenright}}} as a packed string: |
30296 | 1419 |
|
1420 |
\begin{itemize} |
|
1421 |
||
40406 | 1422 |
\item \isa{{\isaliteral{3F}{\isacharquery}}x} if \isa{x} does not end with a digit and \isa{i\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{0}}}, |
30296 | 1423 |
|
40406 | 1424 |
\item \isa{{\isaliteral{3F}{\isacharquery}}xi} if \isa{x} does not end with a digit, |
30296 | 1425 |
|
40406 | 1426 |
\item \isa{{\isaliteral{3F}{\isacharquery}}x{\isaliteral{2E}{\isachardot}}i} otherwise. |
30296 | 1427 |
|
1428 |
\end{itemize} |
|
1429 |
||
35001 | 1430 |
Indexnames may acquire large index numbers after several maxidx |
1431 |
shifts have been applied. Results are usually normalized towards |
|
1432 |
\isa{{\isadigit{0}}} at certain checkpoints, notably at the end of a proof. |
|
1433 |
This works by producing variants of the corresponding basic name |
|
40406 | 1434 |
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}}} |
1435 |
becomes \isa{{\isaliteral{3F}{\isacharquery}}x{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{3F}{\isacharquery}}xa{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{3F}{\isacharquery}}xb}.% |
|
30296 | 1436 |
\end{isamarkuptext}% |
1437 |
\isamarkuptrue% |
|
1438 |
% |
|
1439 |
\isadelimmlref |
|
1440 |
% |
|
1441 |
\endisadelimmlref |
|
1442 |
% |
|
1443 |
\isatagmlref |
|
1444 |
% |
|
1445 |
\begin{isamarkuptext}% |
|
1446 |
\begin{mldecls} |
|
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1447 |
\indexdef{}{ML type}{indexname}\verb|type indexname = string * int| \\ |
30296 | 1448 |
\end{mldecls} |
1449 |
||
1450 |
\begin{description} |
|
1451 |
||
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1452 |
\item Type \verb|indexname| represents indexed names. This is |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1453 |
an abbreviation for \verb|string * int|. The second component |
40406 | 1454 |
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 | 1455 |
indexes should not be used. |
30296 | 1456 |
|
1457 |
\end{description}% |
|
1458 |
\end{isamarkuptext}% |
|
1459 |
\isamarkuptrue% |
|
1460 |
% |
|
1461 |
\endisatagmlref |
|
1462 |
{\isafoldmlref}% |
|
1463 |
% |
|
1464 |
\isadelimmlref |
|
1465 |
% |
|
1466 |
\endisadelimmlref |
|
1467 |
% |
|
35001 | 1468 |
\isamarkupsubsection{Long names \label{sec:long-name}% |
30296 | 1469 |
} |
1470 |
\isamarkuptrue% |
|
1471 |
% |
|
1472 |
\begin{isamarkuptext}% |
|
35001 | 1473 |
A \emph{long name} consists of a sequence of non-empty name |
1474 |
components. The packed representation uses a dot as separator, as |
|
40406 | 1475 |
in ``\isa{A{\isaliteral{2E}{\isachardot}}b{\isaliteral{2E}{\isachardot}}c}''. The last component is called \emph{base |
35001 | 1476 |
name}, the remaining prefix is called \emph{qualifier} (which may be |
1477 |
empty). The qualifier can be understood as the access path to the |
|
1478 |
named entity while passing through some nested block-structure, |
|
1479 |
although our free-form long names do not really enforce any strict |
|
1480 |
discipline. |
|
1481 |
||
40406 | 1482 |
For example, an item named ``\isa{A{\isaliteral{2E}{\isachardot}}b{\isaliteral{2E}{\isachardot}}c}'' may be understood as |
35001 | 1483 |
a local entity \isa{c}, within a local structure \isa{b}, |
1484 |
within a global structure \isa{A}. In practice, long names |
|
1485 |
usually represent 1--3 levels of qualification. User ML code should |
|
1486 |
not make any assumptions about the particular structure of long |
|
1487 |
names! |
|
30296 | 1488 |
|
1489 |
The empty name is commonly used as an indication of unnamed |
|
35001 | 1490 |
entities, or entities that are not entered into the corresponding |
1491 |
name space, whenever this makes any sense. The basic operations on |
|
1492 |
long names map empty names again to empty names.% |
|
30296 | 1493 |
\end{isamarkuptext}% |
1494 |
\isamarkuptrue% |
|
1495 |
% |
|
1496 |
\isadelimmlref |
|
1497 |
% |
|
1498 |
\endisadelimmlref |
|
1499 |
% |
|
1500 |
\isatagmlref |
|
1501 |
% |
|
1502 |
\begin{isamarkuptext}% |
|
1503 |
\begin{mldecls} |
|
30365 | 1504 |
\indexdef{}{ML}{Long\_Name.base\_name}\verb|Long_Name.base_name: string -> string| \\ |
1505 |
\indexdef{}{ML}{Long\_Name.qualifier}\verb|Long_Name.qualifier: string -> string| \\ |
|
1506 |
\indexdef{}{ML}{Long\_Name.append}\verb|Long_Name.append: string -> string -> string| \\ |
|
1507 |
\indexdef{}{ML}{Long\_Name.implode}\verb|Long_Name.implode: string list -> string| \\ |
|
1508 |
\indexdef{}{ML}{Long\_Name.explode}\verb|Long_Name.explode: string -> string list| \\ |
|
30296 | 1509 |
\end{mldecls} |
35001 | 1510 |
|
1511 |
\begin{description} |
|
1512 |
||
1513 |
\item \verb|Long_Name.base_name|~\isa{name} returns the base name |
|
1514 |
of a long name. |
|
1515 |
||
1516 |
\item \verb|Long_Name.qualifier|~\isa{name} returns the qualifier |
|
1517 |
of a long name. |
|
1518 |
||
40406 | 1519 |
\item \verb|Long_Name.append|~\isa{name\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ name\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{2}}} appends two long |
35001 | 1520 |
names. |
1521 |
||
1522 |
\item \verb|Long_Name.implode|~\isa{names} and \verb|Long_Name.explode|~\isa{name} convert between the packed string |
|
1523 |
representation and the explicit list form of long names. |
|
1524 |
||
1525 |
\end{description}% |
|
1526 |
\end{isamarkuptext}% |
|
1527 |
\isamarkuptrue% |
|
1528 |
% |
|
1529 |
\endisatagmlref |
|
1530 |
{\isafoldmlref}% |
|
1531 |
% |
|
1532 |
\isadelimmlref |
|
1533 |
% |
|
1534 |
\endisadelimmlref |
|
1535 |
% |
|
1536 |
\isamarkupsubsection{Name spaces \label{sec:name-space}% |
|
1537 |
} |
|
1538 |
\isamarkuptrue% |
|
1539 |
% |
|
1540 |
\begin{isamarkuptext}% |
|
1541 |
A \isa{name\ space} manages a collection of long names, |
|
1542 |
together with a mapping between partially qualified external names |
|
1543 |
and fully qualified internal names (in both directions). Note that |
|
1544 |
the corresponding \isa{intern} and \isa{extern} operations |
|
1545 |
are mostly used for parsing and printing only! The \isa{declare} operation augments a name space according to the accesses |
|
1546 |
determined by a given binding, and a naming policy from the context. |
|
1547 |
||
1548 |
\medskip A \isa{binding} specifies details about the prospective |
|
1549 |
long name of a newly introduced formal entity. It consists of a |
|
1550 |
base name, prefixes for qualification (separate ones for system |
|
1551 |
infrastructure and user-space mechanisms), a slot for the original |
|
1552 |
source position, and some additional flags. |
|
1553 |
||
1554 |
\medskip A \isa{naming} provides some additional details for |
|
1555 |
producing a long name from a binding. Normally, the naming is |
|
1556 |
implicit in the theory or proof context. The \isa{full} |
|
1557 |
operation (and its variants for different context types) produces a |
|
1558 |
fully qualified internal name to be entered into a name space. The |
|
1559 |
main equation of this ``chemical reaction'' when binding new |
|
1560 |
entities in a context is as follows: |
|
1561 |
||
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1562 |
\medskip |
35001 | 1563 |
\begin{tabular}{l} |
40406 | 1564 |
\isa{binding\ {\isaliteral{2B}{\isacharplus}}\ naming\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ long\ name\ {\isaliteral{2B}{\isacharplus}}\ name\ space\ accesses} |
35001 | 1565 |
\end{tabular} |
1566 |
||
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1567 |
\bigskip As a general principle, there is a separate name space for |
35001 | 1568 |
each kind of formal entity, e.g.\ fact, logical constant, type |
1569 |
constructor, type class. It is usually clear from the occurrence in |
|
1570 |
concrete syntax (or from the scope) which kind of entity a name |
|
1571 |
refers to. For example, the very same name \isa{c} may be used |
|
1572 |
uniformly for a constant, type constructor, and type class. |
|
1573 |
||
1574 |
There are common schemes to name derived entities systematically |
|
1575 |
according to the name of the main logical entity involved, e.g.\ |
|
40406 | 1576 |
fact \isa{c{\isaliteral{2E}{\isachardot}}intro} for a canonical introduction rule related to |
35001 | 1577 |
constant \isa{c}. This technique of mapping names from one |
1578 |
space into another requires some care in order to avoid conflicts. |
|
1579 |
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
|
1580 |
class should get an additional suffix in addition to the usual |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1581 |
qualification. This leads to the following conventions for derived |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1582 |
names: |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1583 |
|
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1584 |
\medskip |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1585 |
\begin{tabular}{ll} |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1586 |
logical entity & fact name \\\hline |
40406 | 1587 |
constant \isa{c} & \isa{c{\isaliteral{2E}{\isachardot}}intro} \\ |
1588 |
type \isa{c} & \isa{c{\isaliteral{5F}{\isacharunderscore}}type{\isaliteral{2E}{\isachardot}}intro} \\ |
|
1589 |
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
|
1590 |
\end{tabular}% |
35001 | 1591 |
\end{isamarkuptext}% |
1592 |
\isamarkuptrue% |
|
1593 |
% |
|
1594 |
\isadelimmlref |
|
1595 |
% |
|
1596 |
\endisadelimmlref |
|
1597 |
% |
|
1598 |
\isatagmlref |
|
1599 |
% |
|
1600 |
\begin{isamarkuptext}% |
|
1601 |
\begin{mldecls} |
|
1602 |
\indexdef{}{ML type}{binding}\verb|type binding| \\ |
|
1603 |
\indexdef{}{ML}{Binding.empty}\verb|Binding.empty: binding| \\ |
|
1604 |
\indexdef{}{ML}{Binding.name}\verb|Binding.name: string -> binding| \\ |
|
1605 |
\indexdef{}{ML}{Binding.qualify}\verb|Binding.qualify: bool -> string -> binding -> binding| \\ |
|
1606 |
\indexdef{}{ML}{Binding.prefix}\verb|Binding.prefix: bool -> string -> binding -> binding| \\ |
|
1607 |
\indexdef{}{ML}{Binding.conceal}\verb|Binding.conceal: binding -> binding| \\ |
|
1608 |
\indexdef{}{ML}{Binding.str\_of}\verb|Binding.str_of: binding -> string| \\ |
|
1609 |
\end{mldecls} |
|
30296 | 1610 |
\begin{mldecls} |
33174 | 1611 |
\indexdef{}{ML type}{Name\_Space.naming}\verb|type Name_Space.naming| \\ |
1612 |
\indexdef{}{ML}{Name\_Space.default\_naming}\verb|Name_Space.default_naming: Name_Space.naming| \\ |
|
1613 |
\indexdef{}{ML}{Name\_Space.add\_path}\verb|Name_Space.add_path: string -> Name_Space.naming -> Name_Space.naming| \\ |
|
1614 |
\indexdef{}{ML}{Name\_Space.full\_name}\verb|Name_Space.full_name: Name_Space.naming -> binding -> string| \\ |
|
30296 | 1615 |
\end{mldecls} |
1616 |
\begin{mldecls} |
|
33174 | 1617 |
\indexdef{}{ML type}{Name\_Space.T}\verb|type Name_Space.T| \\ |
1618 |
\indexdef{}{ML}{Name\_Space.empty}\verb|Name_Space.empty: string -> Name_Space.T| \\ |
|
1619 |
\indexdef{}{ML}{Name\_Space.merge}\verb|Name_Space.merge: Name_Space.T * Name_Space.T -> Name_Space.T| \\ |
|
1620 |
\indexdef{}{ML}{Name\_Space.declare}\verb|Name_Space.declare: bool -> Name_Space.naming -> binding -> Name_Space.T ->|\isasep\isanewline% |
|
1621 |
\verb| string * Name_Space.T| \\ |
|
1622 |
\indexdef{}{ML}{Name\_Space.intern}\verb|Name_Space.intern: Name_Space.T -> string -> string| \\ |
|
1623 |
\indexdef{}{ML}{Name\_Space.extern}\verb|Name_Space.extern: Name_Space.T -> string -> string| \\ |
|
35001 | 1624 |
\indexdef{}{ML}{Name\_Space.is\_concealed}\verb|Name_Space.is_concealed: Name_Space.T -> string -> bool| |
30296 | 1625 |
\end{mldecls} |
1626 |
||
1627 |
\begin{description} |
|
1628 |
||
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1629 |
\item Type \verb|binding| represents the abstract concept of |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1630 |
name bindings. |
35001 | 1631 |
|
1632 |
\item \verb|Binding.empty| is the empty binding. |
|
30296 | 1633 |
|
35001 | 1634 |
\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
|
1635 |
name \isa{name}. Note that this lacks proper source position |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1636 |
information; see also the ML antiquotation \hyperlink{ML antiquotation.binding}{\mbox{\isa{binding}}}. |
35001 | 1637 |
|
1638 |
\item \verb|Binding.qualify|~\isa{mandatory\ name\ binding} |
|
1639 |
prefixes qualifier \isa{name} to \isa{binding}. The \isa{mandatory} flag tells if this name component always needs to be |
|
1640 |
given in name space accesses --- this is mostly \isa{false} in |
|
1641 |
practice. Note that this part of qualification is typically used in |
|
1642 |
derived specification mechanisms. |
|
30296 | 1643 |
|
35001 | 1644 |
\item \verb|Binding.prefix| is similar to \verb|Binding.qualify|, but |
1645 |
affects the system prefix. This part of extra qualification is |
|
1646 |
typically used in the infrastructure for modular specifications, |
|
1647 |
notably ``local theory targets'' (see also \chref{ch:local-theory}). |
|
30296 | 1648 |
|
35001 | 1649 |
\item \verb|Binding.conceal|~\isa{binding} indicates that the |
1650 |
binding shall refer to an entity that serves foundational purposes |
|
1651 |
only. This flag helps to mark implementation details of |
|
1652 |
specification mechanism etc. Other tools should not depend on the |
|
1653 |
particulars of concealed entities (cf.\ \verb|Name_Space.is_concealed|). |
|
1654 |
||
1655 |
\item \verb|Binding.str_of|~\isa{binding} produces a string |
|
1656 |
representation for human-readable output, together with some formal |
|
1657 |
markup that might get used in GUI front-ends, for example. |
|
30296 | 1658 |
|
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1659 |
\item Type \verb|Name_Space.naming| represents the abstract |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1660 |
concept of a naming policy. |
30296 | 1661 |
|
33174 | 1662 |
\item \verb|Name_Space.default_naming| is the default naming policy. |
30296 | 1663 |
In a theory context, this is usually augmented by a path prefix |
1664 |
consisting of the theory name. |
|
1665 |
||
33174 | 1666 |
\item \verb|Name_Space.add_path|~\isa{path\ naming} augments the |
30296 | 1667 |
naming policy by extending its path component. |
1668 |
||
33174 | 1669 |
\item \verb|Name_Space.full_name|~\isa{naming\ binding} turns a |
30296 | 1670 |
name binding (usually a basic name) into the fully qualified |
1671 |
internal name, according to the given naming policy. |
|
1672 |
||
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1673 |
\item Type \verb|Name_Space.T| represents name spaces. |
30296 | 1674 |
|
40406 | 1675 |
\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 | 1676 |
maintaining name spaces according to theory data management |
1677 |
(\secref{sec:context-data}); \isa{kind} is a formal comment |
|
1678 |
to characterize the purpose of a name space. |
|
30296 | 1679 |
|
33174 | 1680 |
\item \verb|Name_Space.declare|~\isa{strict\ naming\ bindings\ space} enters a name binding as fully qualified internal name into |
1681 |
the name space, with external accesses determined by the naming |
|
1682 |
policy. |
|
1683 |
||
1684 |
\item \verb|Name_Space.intern|~\isa{space\ name} internalizes a |
|
30296 | 1685 |
(partially qualified) external name. |
1686 |
||
1687 |
This operation is mostly for parsing! Note that fully qualified |
|
33174 | 1688 |
names stemming from declarations are produced via \verb|Name_Space.full_name| and \verb|Name_Space.declare| |
30296 | 1689 |
(or their derivatives for \verb|theory| and |
1690 |
\verb|Proof.context|). |
|
1691 |
||
33174 | 1692 |
\item \verb|Name_Space.extern|~\isa{space\ name} externalizes a |
30296 | 1693 |
(fully qualified) internal name. |
1694 |
||
1695 |
This operation is mostly for printing! User code should not rely on |
|
1696 |
the precise result too much. |
|
1697 |
||
35001 | 1698 |
\item \verb|Name_Space.is_concealed|~\isa{space\ name} indicates |
1699 |
whether \isa{name} refers to a strictly private entity that |
|
1700 |
other tools are supposed to ignore! |
|
1701 |
||
30296 | 1702 |
\end{description}% |
1703 |
\end{isamarkuptext}% |
|
1704 |
\isamarkuptrue% |
|
1705 |
% |
|
1706 |
\endisatagmlref |
|
1707 |
{\isafoldmlref}% |
|
1708 |
% |
|
1709 |
\isadelimmlref |
|
1710 |
% |
|
1711 |
\endisadelimmlref |
|
1712 |
% |
|
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1713 |
\isadelimmlantiq |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1714 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1715 |
\endisadelimmlantiq |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1716 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1717 |
\isatagmlantiq |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1718 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1719 |
\begin{isamarkuptext}% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1720 |
\begin{matharray}{rcl} |
40406 | 1721 |
\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
|
1722 |
\end{matharray} |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1723 |
|
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1724 |
\begin{rail} |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1725 |
'binding' name |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1726 |
; |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1727 |
\end{rail} |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1728 |
|
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1729 |
\begin{description} |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1730 |
|
40406 | 1731 |
\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
|
1732 |
\isa{name} and the source position taken from the concrete |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1733 |
syntax of this antiquotation. In many situations this is more |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1734 |
appropriate than the more basic \verb|Binding.name| function. |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1735 |
|
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1736 |
\end{description}% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1737 |
\end{isamarkuptext}% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1738 |
\isamarkuptrue% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1739 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1740 |
\endisatagmlantiq |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1741 |
{\isafoldmlantiq}% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1742 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1743 |
\isadelimmlantiq |
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 |
\endisadelimmlantiq |
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 |
\isadelimmlex |
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 |
\endisadelimmlex |
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 |
\isatagmlex |
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 |
\begin{isamarkuptext}% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1754 |
The following example yields the source position of some |
40126 | 1755 |
concrete binding inlined into the text:% |
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1756 |
\end{isamarkuptext}% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1757 |
\isamarkuptrue% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1758 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1759 |
\endisatagmlex |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1760 |
{\isafoldmlex}% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1761 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1762 |
\isadelimmlex |
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 |
\endisadelimmlex |
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 |
\isadelimML |
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 |
\endisadelimML |
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 |
\isatagML |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1771 |
\isacommand{ML}\isamarkupfalse% |
40406 | 1772 |
\ {\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
|
1773 |
\isaantiq |
40406 | 1774 |
binding\ here{}% |
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1775 |
\endisaantiq |
40406 | 1776 |
\ {\isaliteral{2A7D}{\isacharverbatimclose}}% |
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1777 |
\endisatagML |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1778 |
{\isafoldML}% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1779 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1780 |
\isadelimML |
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 |
\endisadelimML |
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 |
\begin{isamarkuptext}% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1785 |
\medskip That position can be also printed in a message as |
40126 | 1786 |
follows:% |
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1787 |
\end{isamarkuptext}% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1788 |
\isamarkuptrue% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1789 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1790 |
\isadelimML |
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 |
\endisadelimML |
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 |
\isatagML |
40406 | 1795 |
\isacommand{ML{\isaliteral{5F}{\isacharunderscore}}command}\isamarkupfalse% |
1796 |
\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline |
|
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1797 |
\ \ writeln\isanewline |
40406 | 1798 |
\ \ \ \ {\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
|
1799 |
\isaantiq |
40406 | 1800 |
binding\ here{}% |
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1801 |
\endisaantiq |
40406 | 1802 |
{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\isanewline |
1803 |
{\isaliteral{2A7D}{\isacharverbatimclose}}% |
|
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1804 |
\endisatagML |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1805 |
{\isafoldML}% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1806 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1807 |
\isadelimML |
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 |
\endisadelimML |
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 |
\begin{isamarkuptext}% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1812 |
This illustrates a key virtue of formalized bindings as |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1813 |
opposed to raw specifications of base names: the system can use this |
40126 | 1814 |
additional information for feedback given to the user (error |
1815 |
messages etc.).% |
|
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1816 |
\end{isamarkuptext}% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1817 |
\isamarkuptrue% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
39688
diff
changeset
|
1818 |
% |
30296 | 1819 |
\isadelimtheory |
1820 |
% |
|
1821 |
\endisadelimtheory |
|
1822 |
% |
|
1823 |
\isatagtheory |
|
1824 |
\isacommand{end}\isamarkupfalse% |
|
1825 |
% |
|
1826 |
\endisatagtheory |
|
1827 |
{\isafoldtheory}% |
|
1828 |
% |
|
1829 |
\isadelimtheory |
|
1830 |
% |
|
1831 |
\endisadelimtheory |
|
1832 |
\isanewline |
|
1833 |
\end{isabellebody}% |
|
1834 |
%%% Local Variables: |
|
1835 |
%%% mode: latex |
|
1836 |
%%% TeX-master: "root" |
|
1837 |
%%% End: |