1.1 --- a/src/Tools/isac/Doc/Specify_Phase/Specify_Phase.thy Sun Dec 31 09:42:27 2023 +0100
1.2 +++ b/src/Tools/isac/Doc/Specify_Phase/Specify_Phase.thy Sun Dec 31 15:13:39 2023 +0100
1.3 @@ -3,6 +3,19 @@
1.4 theory Specify_Phase
1.5 imports "Specify.Specify"
1.6 begin
1.7 +ML \<open>
1.8 + open O_Model
1.9 + open I_Model
1.10 +\<close> ML \<open>
1.11 +\<close> ML \<open>
1.12 + open Tactic
1.13 +\<close> ML \<open>
1.14 +Model_Problem
1.15 +\<close> text \<open>
1.16 +@{theory_text problem};
1.17 +@{theory_text INTERACTION_MODEL};
1.18 +\<close> ML \<open>
1.19 +\<close>
1.20 (*>*)
1.21
1.22 text \<open>
1.23 @@ -297,7 +310,7 @@
1.24 for example ${\it Maximum\;A}$.
1.25 \end{itemize}
1.26
1.27 -\item\label{UR:toggle-problem-method} Within the \emph{Specification} the
1.28 +\item\label{UR:toggle-problem-method} Within the @{theory_text Specification} the
1.29 \textbf{\emph{Model} serves two purposes}: for the \emph{Problem\_Ref} it shows
1.30 the fields from \emph{Given} to \emph{Relate} according to Pt.\ref{UR:model}
1.31 and for \emph{Method\_Ref} it shows the guard of the program guiding
1.32 @@ -407,8 +420,9 @@
1.33 Most of the lecturers and teachers want to expose their \emph{personal} collection of
1.34 exercises to their students; so lecturers should be enabled to implement these
1.35 independently in the system, without further expertise -- so \emph{authoring for
1.36 -lecturers} needs to be supported eventually for type \texttt{Formalise.T}
1.37 -below. However, the implementation of problem patterns \texttt{Model\_Pattern.T}
1.38 +lecturers} needs to be supported eventually for type @{ML_type Formalise.T}
1.39 +below. However, the implementation of problem patterns
1.40 +@{ML_type Model_Pattern.T}
1.41 involves specific knowledge in computer mathematics --
1.42 so \emph{maths authoring} needs to be supported in addition, eventually.
1.43 %ref.2: ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ repetitive/ confusing
1.44 @@ -439,15 +453,15 @@
1.45 \end{verbatim}
1.46 \end{small}
1.47
1.48 -The \texttt{type Formalise.T} consists of a (preparatory form of) model and
1.49 -\texttt{refs}; the latter are explained below in \S\ref{ssec:solve-phase}.
1.50 -\texttt{Model\_Pattern.T} is designed according to \UR\ref{UR:model}.
1.51 -Each \texttt{term}
1.52 -is accompanied by a \texttt{descriptor}, which informs the user about what
1.53 -is requested from him to input. Pairs of \texttt{(descriptor * term)} are
1.54 -assigned to \texttt{m\_field}s according to \UR\ref{UR:model}.
1.55 +The type @{ML_type Formalise.T} consists of a (preparatory form of) model and
1.56 +@{ML_type Formalise.refs}; the latter are explained below in \S\ref{ssec:solve-phase}.
1.57 +@{ML_type Model_Pattern.T} is designed according to \UR\ref{UR:model}.
1.58 +Each @{ML_type term}
1.59 +is accompanied by a @{ML_type descriptor}, which informs the user about what
1.60 +is requested from him to input. Pairs of @{ML_type "(descriptor * term)"} are
1.61 +assigned to @{ML_type m_field}s according to \UR\ref{UR:model}.
1.62 The special values for the running example
1.63 -are as follows, where the \texttt{descriptor}s are \texttt{Constants},
1.64 +are as follows, where the @{ML_type descriptor}s are \texttt{Constants},
1.65 \texttt{Maximum}, \texttt{AdditionalValues}, \texttt{Extremum},
1.66 \texttt{SideConditions}, \texttt{FunctionVariable}, \texttt{Domain}
1.67 and \texttt{ErrorBound}:
1.68 @@ -474,18 +488,18 @@
1.69 The text in line \texttt{01} exceeds the line limit, it has already been
1.70 shown with the problem statement of the running example in \S\ref{ssec:running-expl}.
1.71 The reader may be surprised by the multiple entries for the descriptors
1.72 -\texttt{SideConditions}, \texttt{FunctionVariable} and \texttt{Domain};
1.73 +@{term SideConditions}, @{term FunctionVariable} and @{term Domain};
1.74 this is due to \emph{variants} introduced in \S\ref{ssec:variants} below ---
1.75 this representation of variants is considered intermediate, it was easy
1.76 to implement and will be up to further refinement. The lines \texttt{14} and
1.77 -\texttt{15} represent the \texttt{refs} introduced above in \texttt{Formalise.T}
1.78 +\texttt{15} represent the \texttt{refs} introduced above in @{ML_type Formalise.T}
1.79 and explained in \S\ref{ssec:solve-phase} below.
1.80 The attentive reader will also notice that the items of the example's \texttt{model}
1.81 -are not assigned to an \texttt{m\_field}
1.82 +are not assigned to an @{ML_type m_field}
1.83 (line \texttt{02} on p.\pageref{src:model-pattern}), rather the
1.84 -\texttt{descriptor} is the means to relate items between different data
1.85 -structures, in this case between \texttt{Formalise.model} and the
1.86 -\texttt{problem} below defining the running example:
1.87 +@{ML_type descriptor} is the means to relate items between different data
1.88 +structures, in this case between @{ML_type Formalise.model} and the
1.89 +@{theory_text problem} below defining the running example:
1.90 \begin{small}
1.91 \begin{verbatim}
1.92 01 problem pbl_opti_univ : "univariate_calculus/Optimisation" =
1.93 @@ -497,19 +511,19 @@
1.94 07 Relate: "Extremum extr" "SideConditions sideconds"
1.95 \end{verbatim}\label{problem}
1.96 \end{small}
1.97 -The above \texttt{problem} assigns the elements of the model (in \sisac{} we
1.98 +The above @{theory_text problem} assigns the elements of the model (in \sisac{} we
1.99 call an element of a model an \emph{item} in order not to confuse with
1.100 -\emph{elements} of lists or sets) to a respective \texttt{m\_field}.
1.101 -As already mentioned, the assignment is done via \texttt{descriptor}s accompanied with
1.102 +\emph{elements} of lists or sets) to a respective @{ML_type m_field}.
1.103 +As already mentioned, the assignment is done via @{ML_type descriptor}s accompanied with
1.104 place-holders (\texttt{fixes}, \texttt{maxx}, etc; see line \texttt{03}
1.105 -in \texttt{type Model\_Pattern.T} on p.\pageref{src:model-pattern}) -- these are instantiated
1.106 +in type @{ML_type Model_Pattern.T} on p.\pageref{src:model-pattern}) -- these are instantiated
1.107 on the fly with values of the concrete example selected by the user.
1.108
1.109 It is the task of a mathematics author to decide the structure
1.110 of the model such that it covers an appropriate collection of examples,
1.111 -where a respective \texttt{Model\_Pattern.T} of a \texttt{problem} is
1.112 -instantiated for several examples by values of a \texttt{Formalise.T}.
1.113 -For instantiation of the model for a \texttt{problem} an environment is
1.114 +where a respective @{ML_type Model_Pattern.T} of a @{theory_text problem} is
1.115 +instantiated for several examples by values of a @{ML_type Formalise.T}.
1.116 +For instantiation of the model for a @{theory_text problem} an environment is
1.117 required, for instance for the \texttt{demo\_example} the environment
1.118 \label{env-subst}
1.119 \begin{small}
1.120 @@ -524,7 +538,7 @@
1.121 is required.
1.122
1.123 Another reason for this late assignment is that one and the same item may
1.124 -belong to \texttt{m\_field} \texttt{Relate} for a problem but to \texttt{Given}
1.125 +belong to @{ML_type m_field} \texttt{Relate} for a problem but to \texttt{Given}
1.126 for a \texttt{method}, see \S\ref{ssec:solve-phase}.
1.127 Finally it may be remarked that the identifier
1.128 \texttt{"univariate\_calculus/Optimisation"} can be found in a more
1.129 @@ -545,22 +559,22 @@
1.130 \caption{The template for starting a \emph{Specification}.}
1.131 \label{fig:specification-template}
1.132 \end{figure}
1.133 -There the \texttt{descriptor}s (\texttt{Constants}, etc) are followed by
1.134 +There the @{ML_type descriptor}s (@{term Constants}, etc) are followed by
1.135 templates giving hints on the input format according to
1.136 \UR\ref{UR:template} in order to help students to cope with the troublesome
1.137 -transition to exact formal representation. The \texttt{Model} is embedded
1.138 -into the \texttt{Specification} which also contains \texttt{References}
1.139 +transition to exact formal representation. The @{theory_text Model} is embedded
1.140 +into the @{theory_text Specification} which also contains \texttt{References}
1.141 explained in \S\ref{ssec:solve-phase} below. The above template is completed
1.142 in Fig.\ref{fig:specification-complete} on p.\pageref{fig:specification-complete}
1.143 -and the reader may refer to the \texttt{Relate} in the \texttt{Model} when
1.144 +and the reader may refer to the \texttt{Relate} in the @{theory_text Model} when
1.145 reading the next paragraph.
1.146
1.147 \subparagraph{Representation in field \texttt{Relate} is simplified}\label{post-cond}
1.148 such that a student needs not encounter formal logic according to \UR\ref{UR:relate}.
1.149 Fig.\ref{fig:specification-complete} %on p.\pageref{fig:specification-complete}
1.150 shows that for the \texttt{demo\_example}
1.151 -\texttt{Extremum} and \texttt{SideConditions} actually are the
1.152 -essential parts of the postcondition, which characterises a \texttt{problem}
1.153 +@{term Extremum} and @{term SideConditions} actually are the
1.154 +essential parts of the postcondition, which characterises a @{theory_text problem}
1.155 by relating \texttt{Given} and \texttt{Find}:
1.156 \begin{eqnarray*}
1.157 &\;& (A = 2 * u * v - u \uparrow 2)\;\;\land\;\;
1.158 @@ -577,8 +591,8 @@
1.159 parts of the postcondition:
1.160 \begin{tabbing}
1.161 12345\=\kill
1.162 -\> \texttt{Extremum} $(A = 2 * u * v - u \uparrow 2)$,
1.163 - \texttt{SideConditions} $(u / 2) \uparrow 2 + (v / 2) \uparrow 2 = r \uparrow 2$
1.164 +\> @{term Extremum} $(A = 2 * u * v - u \uparrow 2)$,
1.165 + @{term SideConditions} $(u / 2) \uparrow 2 + (v / 2) \uparrow 2 = r \uparrow 2$
1.166 \end{tabbing}
1.167 These parts also are sufficient to automatically generate user-guidance
1.168 according to \UR\ref{UR:next-step} (by enabling Lucas-Interpretation
1.169 @@ -590,7 +604,7 @@
1.170 semantics, it should also adapt to fresh ideas of a student and support various
1.171 variants in solving a particular problem.
1.172 Let us look at Fig.\ref{fig:specification-complete} with the completed
1.173 -\texttt{Specification} and ask an important question:
1.174 +@{theory_text Specification} and ask an important question:
1.175 \begin{figure} [htb]
1.176 \centering
1.177 \includegraphics[width=0.65\textwidth]{specification-complete.png}
1.178 @@ -603,16 +617,16 @@
1.179 might focus on the width $u$ and the length $v$, and apply Pythagoras theorem
1.180 $(u / 2) \uparrow 2 + (v / 2) \uparrow 2 = r \uparrow 2$.
1.181 But students might focus as well on the angle $\alpha$ and formalise
1.182 -the \texttt{SideConditions} as $u / 2 = r * \sin \alpha,\;v / 2 = r * \cos \alpha$.
1.183 +the @{term SideConditions} as $u / 2 = r * \sin \alpha,\;v / 2 = r * \cos \alpha$.
1.184
1.185 \medskip
1.186 And what if a student has an eye for simple solutions and takes as
1.187 -\texttt{SideConditions} either $u = \cos\alpha, v = \sin\alpha$ or
1.188 +@{term SideConditions} either $u = \cos\alpha, v = \sin\alpha$ or
1.189 $u \uparrow 2 + v \uparrow 2 = 4 * r \uparrow 2$ ? The latter is semantically
1.190 equivalent (equivalent in this specific example) to the variant shown in
1.191 Fig.\ref{fig:specification-complete}. So, during the whole specify-phase,
1.192 each formula input by a student must be checked for equivalence with the
1.193 -formulas prepared in the \texttt{Formalise.T}. Such checking is done via
1.194 +formulas prepared in the @{ML_type Formalise.T}. Such checking is done via
1.195 rewriting to a normal form. This might be quite tedious, for instance with
1.196 equations involving fractions like in showing equivalence of the equations
1.197 $u \uparrow 2 + v \uparrow 2 = 4 * r \uparrow 2
1.198 @@ -625,21 +639,21 @@
1.199 and simplistic for the purpose of simple implementation.
1.200 Much information is redundant there, apparently, and on the other hand interesting
1.201 structural properties are hardly visible. For instance, the student's decision
1.202 -whether to take the \texttt{FunctionVariable u} or the
1.203 -\texttt{FunctionVariable v} for differentiation (see \S\ref{ssec:solve-phase}),
1.204 -this decision is fairly independent from the \texttt{problem}'s model --
1.205 -the \texttt{Model} just must no refer to $\alpha$.
1.206 +whether to take the @{term "FunctionVariable u"} or the
1.207 +@{term "FunctionVariable v"} for differentiation (see \S\ref{ssec:solve-phase}),
1.208 +this decision is fairly independent from the @{theory_text problem}'s model --
1.209 +the @{theory_text Model} just must no refer to $\alpha$.
1.210
1.211 -The need for a separated language for \texttt{Specification} becomes definitely
1.212 +The need for a separated language for @{theory_text Specification} becomes definitely
1.213 clear when considering the precondition and the postcondition (the latter
1.214 introduced above on p.\pageref{postcondition}). The precondition must evaluate
1.215 -to true for a \texttt{Specification} to be valid, and the postcondition must be
1.216 +to true for a @{theory_text Specification} to be valid, and the postcondition must be
1.217 true for a \texttt{Solution} to be accepted by the system.
1.218
1.219 In order to evaluate precondition \texttt{Where} $0 < r$ to true, we need to
1.220 -create the environment $[(r, 7)]$ from \texttt{Constants}. With the
1.221 +create the environment $[(r, 7)]$ from @{term Constants}. With the
1.222 \texttt{demo\_example} this is straight forward, but if we had
1.223 -\texttt{Constants [s = 1, t = 2]} we already need to employ some trickery with
1.224 +@{term "Constants [s = 1, t = 2]"} we already need to employ some trickery with
1.225 indexing. And what about the postcondition?
1.226 \begin{tabbing}
1.227 123 \= $\forall \;\; {\it maxx}' \;\; {\it funvar}'\;\; . \;\;$ \=\kill
1.228 @@ -650,12 +664,12 @@
1.229 \end{tabbing}
1.230 How could such a ``pattern-matching'' description be instantiated to the
1.231 postcondition on p.\pageref{postcondition}? Instantiated reliably, such that Isabelle could
1.232 -evaluate it to true with the values found by \texttt{Solution}? How would the
1.233 -variant with the $\alpha$ work out, which has two \texttt{SideConditions}?
1.234 +evaluate it to true with the values found by @{term Solution}? How would the
1.235 +variant with the $\alpha$ work out, which has two @{term SideConditions}?
1.236
1.237 \medskip
1.238 Answering the open question above may go in parallel to implementation of a larger
1.239 -body of examples and respective \texttt{problem}s.
1.240 +body of examples and respective @{theory_text problem}s.
1.241 Field tests \cite{imst-htl06,imst-htl07,imst-hpts08} in the \sisac{} project
1.242 were based on limited content and thus did not gain much experience with a
1.243 variety of problems with variants and respective flexibility of the system;
1.244 @@ -663,12 +677,12 @@
1.245
1.246 \subsection{Interactivity and Feedback} \label{ssec:interactivity}
1.247 %------------------------------------------------------------------------------
1.248 -The previous section describes how \sisac{} makes a \texttt{Specification}
1.249 +The previous section describes how \sisac{} makes a @{theory_text Specification}
1.250 flexible and open for various variants in solving a particular problem.
1.251 Flexibility in problem solving must be accompanied by flexible interactivity
1.252 -and appropriate feedback. Feedback for input to a \texttt{Model} is
1.253 +and appropriate feedback. Feedback for input to a @{theory_text Model} is
1.254 predefined by \UR\ref{UR:feedback} and modelled by a respective datatype as
1.255 -follows (\texttt{values} are of type \texttt{term list})
1.256 +follows (@{ML_type values} are of type @{ML_type "term list"})
1.257 \begin{small}
1.258 \begin{verbatim}
1.259 01 datatype I_Model.feedback =
1.260 @@ -678,29 +692,29 @@
1.261 05 | Syntax of TermC.as_string (* in case of switching model *)
1.262 \end{verbatim}\label{src:feedback}
1.263 \end{small}
1.264 -The above code plus comments appear fairly self-explaining. \texttt{descriptor}
1.265 +The above code plus comments appear fairly self-explaining. @{ML_type descriptor}
1.266 has been introduced already. In case of empty input, we shall have
1.267 \texttt{Incomplete (\_, [])} and display templates for input-format
1.268 according to \UR\ref{UR:template}. Syntax errors are handled very elegantly in
1.269 Isabelle/PIDE (see \S\ref{ssec:outer-syntax}); in case of switching from the
1.270 -\texttt{Model} of the \texttt{Problem\_Ref} to the \texttt{Model} of the
1.271 +@{theory_text Model} of the \texttt{Problem\_Ref} to the @{theory_text Model} of the
1.272 \texttt{Method\_Ref} (see \S\ref{ssec:solve-phase} below) it might be useful
1.273 to keep a copy of an input with syntax errors. Items can be \texttt{Superfluous}
1.274 -either because they are syntactically correct but not related the \texttt{Model}
1.275 -under construction, or they belong to a \texttt{variant}, which has not yet been
1.276 -decided for. For instance, if the \texttt{Model} is as in
1.277 +either because they are syntactically correct but not related the @{theory_text Model}
1.278 +under construction, or they belong to a @{ML_type variant}, which has not yet been
1.279 +decided for. For instance, if the @{theory_text Model} is as in
1.280 Fig.\ref{fig:specification-complete} on p.\pageref{fig:specification-complete}
1.281 -and the student adds \texttt{SideConditions} $[v = \sin\alpha]$, this item
1.282 +and the student adds @{term SideConditions} $[v = \sin\alpha]$, this item
1.283 will be marked as \texttt{Superfluous} unless interactive
1.284 -completion to \texttt{SideConditions} $[v = \sin\alpha, v = \cos\alpha]$
1.285 -and deletion of a competing item like \texttt{SideConditions}
1.286 +completion to @{term SideConditions} $[v = \sin\alpha, v = \cos\alpha]$
1.287 +and deletion of a competing item like @{term SideConditions}
1.288 $[u \uparrow 2 + v \uparrow 2 = 4 * r \uparrow 2]$.
1.289
1.290 \bigskip
1.291 -If a student gets stuck during input to a \texttt{Model}, then \UR\ref{UR:next-step}
1.292 +If a student gets stuck during input to a @{theory_text Model}, then \UR\ref{UR:next-step}
1.293 allows him or her to request help. In the specify-phase such help is given
1.294 best by presenting a (partial -- predefined setting!) missing item.
1.295 -\emph{But output of a \texttt{Model} with item does not conform to Isabelle's
1.296 +\emph{But output of a @{theory_text Model} with item does not conform to Isabelle's
1.297 document model}: The content of an Isabelle theory is considered a document
1.298 which has to be checked by the system --- Isabelle is in principle a reactive
1.299 system.
1.300 @@ -710,7 +724,7 @@
1.301 displays the respective proof steps.
1.302
1.303 \sisac{}, in contrary, is designed as a tutoring system, where partners
1.304 -construct a \texttt{Specification} and a \texttt{Solution} in cooperation,
1.305 +construct a @{theory_text Specification} and a \texttt{Solution} in cooperation,
1.306 where the user can propose a step while the system checks it and where the
1.307 student can request help such that the system can propose a step as well.
1.308 Since here psychology of learning is involved,
1.309 @@ -726,7 +740,7 @@
1.310 %------------------------------------------------------------------------------
1.311 Sometimes a user might not be interested in specification. For instance, when
1.312 solving an equation, the type of the problem and the respective
1.313 -\texttt{Model\_Pattern.T} are clear, and only the hierarchy of problem types
1.314 +@{ML_type Model_Pattern.T} are clear, and only the hierarchy of problem types
1.315 would have to be searched for the appropriate type.
1.316
1.317 \sisac's old Java front-end had a so-called CAS-command for that situation,
1.318 @@ -756,23 +770,23 @@
1.319 The solve-phase tackles the construction of a \texttt{Solution} for a given problem,
1.320 where ``next-step-guidance'' is provided by Lucas-Interpretation \cite{wn:lucin-thedu20}.
1.321 For that purpose Lucas-Interpretation uses a program, and for such a program
1.322 -the values specified by a \texttt{Model} instantiate the formal arguments
1.323 +the values specified by a @{theory_text Model} instantiate the formal arguments
1.324 of the program to actual arguments. So items move from \texttt{Relate} to
1.325 \texttt{Given} and new items need to be added to the program's guard
1.326 in order to provide the program
1.327 with all data required for automatically construct a \texttt{Solution}. Thus the
1.328 -\texttt{Model} for the guard of the \texttt{demo\_example} might look as shown in
1.329 +@{theory_text Model} for the guard of the \texttt{demo\_example} might look as shown in
1.330 Fig.\ref{fig:specification-method} below.
1.331 %on p.\pageref{fig:specification-method}.
1.332 \begin{figure} [htb]
1.333 \centering
1.334 \includegraphics[width=0.75\textwidth]{specification-method.png}
1.335 - \caption{The \texttt{Model} for the \texttt{Method\_Ref}.}
1.336 + \caption{The @{theory_text Model} for the \texttt{Method\_Ref}.}
1.337 \label{fig:specification-method}
1.338 \end{figure}
1.339
1.340 The reader might notice that the toggle $\odot\otimes$ has changed,
1.341 -indicating that the \texttt{Model} belongs to the \texttt{Method\_Ref}
1.342 +indicating that the @{theory_text Model} belongs to the \texttt{Method\_Ref}
1.343 (The toggle is not implemented presently and just reminded of by a comment).
1.344
1.345 \medskip
1.346 @@ -784,13 +798,13 @@
1.347 a certain class from problem solving? Should students be forced to input
1.348 \texttt{References}, and when?
1.349
1.350 -A reasonable intermediate step in development might be that a \texttt{Model}
1.351 +A reasonable intermediate step in development might be that a @{theory_text Model}
1.352 could be accepted as complete (e.g. Fig.\ref{fig:specification-complete}) by the
1.353 system even with empty \texttt{References} (e.g.
1.354 Fig.\ref{fig:specification-template}) and a \texttt{Solution} could be started.
1.355
1.356 \medskip
1.357 -Toggling the \texttt{Model} between \texttt{Model\_Ref} and \texttt{Method\_Ref}
1.358 +Toggling the @{theory_text Model} between \texttt{Model\_Ref} and \texttt{Method\_Ref}
1.359 (the former shown in Fig.\ref{fig:specification-complete} on p.\pageref{fig:specification-complete},
1.360 the latter in Fig.\ref{fig:specification-method})
1.361 will be a challenge for implementation in Isabelle/VSCode.
1.362 @@ -818,7 +832,7 @@
1.363 Isabelle separates two kinds of syntax, an inner syntax for mathematical terms
1.364 and an outer syntax for Isabelle/Isar's language elements. The latter is generic
1.365 such that it allows for definition of various language layers. And it is a
1.366 -pleasure to show how easily an \sisac{} \texttt{Specification} is defined such
1.367 +pleasure to show how easily an \sisac{} @{theory_text Specification} is defined such
1.368 that all inner syntax errors are indicated at the right location on screen,
1.369 i.e. how easily all what is shown in the screen-shots on the previous pages
1.370 are implemented such that syntax errors are shown appropriately:
1.371 @@ -851,7 +865,7 @@
1.372 \end{verbatim}
1.373 \end{small}
1.374
1.375 -With these two definitions done, one has in \texttt{update\_step} only to
1.376 +With these two definitions done, one has in @{term update_step} only to
1.377 provide appropriate calls of this function:
1.378 \begin{small}
1.379 \begin{verbatim}
1.380 @@ -861,8 +875,9 @@
1.381 04 (*this exception is caught by PIDE to show "msg" at the proper location*)
1.382 \end{verbatim}
1.383 \end{small}
1.384 -The exception \texttt{ERROR} is caught by Isabelle/PIDE and, for instance,
1.385 -syntax errors detected by \texttt{Syntax.read\_term} are displayed at the
1.386 +The exception @{term ERROR} is caught by Isabelle/PIDE and, for instance,
1.387 +syntax errors detected by \texttt{Syntax.read\_term} %TODO: not known here?!
1.388 +are displayed at the
1.389 proper locations on screen together with \texttt{msg}.
1.390 \emph{That is all what Isar requires to check syntax of input as
1.391 shown in the screen shots in the previous section and to indicate errors
1.392 @@ -880,24 +895,24 @@
1.393 %------------------------------------------------------------------------------
1.394 Checking semantic appropriateness of user input to a Specification as
1.395 described in \S\ref{sect:design} above, comprises a lot of
1.396 -questions: Does an item input to a \texttt{Model} belong to this particular
1.397 +questions: Does an item input to a @{theory_text Model} belong to this particular
1.398 example or is it just \texttt{Superfluous}? If there a list is
1.399 to be input, are all the elements present or are some missing (items are
1.400 \texttt{Incomplete})? Is a
1.401 -\texttt{Model} complete with respect to a specified \texttt{Problem\_Ref}?
1.402 -If \texttt{Theory\_Ref} is input, are all the items of a \texttt{Model} still
1.403 +@{theory_text Model} complete with respect to a specified \texttt{Problem\_Ref}?
1.404 +If \texttt{Theory\_Ref} is input, are all the items of a @{theory_text Model} still
1.405 parsed correctly (or can, for instance, $"\it{Re}\, a + \it{Im}\, b")$ not be
1.406 parsed correctly, because the specified theory does not know the type
1.407 ``complex'')? Etc.
1.408
1.409 The central device for handling feedback to the above questions is the so-called\\
1.410 -\texttt{INTERACTION\_MODEL} with the type \texttt{I\_Model.T}
1.411 +@{theory_text INTERACTION_MODEL} with the type @{ML_type I_Model.T}
1.412 \footnote{In \sisac's code this definition is shifted into a separate
1.413 \texttt{structure Model\_Def} \emph{before} the definition of the store of a
1.414 calculation, \texttt{Ctree}, which still lacks type polymorphism}
1.415 -(where \texttt{variants} is a list of integers and \texttt{m\_field} has been
1.416 -introduced by \texttt{type Model\_Pattern.T} on p.\pageref{src:model-pattern}).
1.417 -\texttt{Position.T} establishes the reference to the location on screen:
1.418 +(where @{ML_type variants} is a list of integers and @{ML_type m_field} has been
1.419 +introduced by type @{ML_type Model_Pattern.T} on p.\pageref{src:model-pattern}).
1.420 +@{ML_type Position.T} establishes the reference to the location on screen:
1.421 \begin{small}
1.422 \begin{verbatim}
1.423 01 type I_Model.single =
1.424 @@ -909,8 +924,8 @@
1.425 06 type I_Model.T = I_Model.single list;
1.426 \end{verbatim}
1.427 \end{small}
1.428 -\texttt{feedback} implements \UR\ref{UR:feedback} and resembles the
1.429 -structure of \texttt{datatype feedback} in the presentation layer as shown on
1.430 +@{ML_type feedback} implements \UR\ref{UR:feedback} and resembles the
1.431 +structure of datatype @{ML_type feedback} in the presentation layer as shown on
1.432 p.\pageref{src:feedback} in \S\ref{ssec:interactivity}.
1.433 The first three characters suffice for internal naming:
1.434 \begin{small}
1.435 @@ -932,38 +947,39 @@
1.436 p.\pageref{axiom:stepwise-inter}. While step-wise construction appears
1.437 self-evident for the solve-phase, where Lucas-Interpretation suggests or checks
1.438 one input formula after the other, this appears artificial for the
1.439 -specify-phase: one can input any item to a \texttt{Specification} in any
1.440 -sequence, items of a \texttt{Model} as well as \texttt{References}.
1.441 +specify-phase: one can input any item to a @{theory_text Specification} in any
1.442 +sequence, items of a @{theory_text Model} as well as \texttt{References}.
1.443 But there is also \UR\ref{UR:next-step}, which calls for the system's ability
1.444 to propose a next step -- and here we are:
1.445 \begin{small}
1.446 \begin{verbatim}
1.447 01 datatype Tactic.input =
1.448 02 (* for specify-phase *)
1.449 - 04 Add_Find of TermC.as_string (*add to the model*)
1.450 + 04 Add_Find of TermC.as_string (*add to the model*)
1.451 05 | Add_Given of TermC.as_string | Add_Relation of TermC.as_string
1.452 06 | Model_Problem (*internal*)
1.453 - 07 | Refine_Problem of Problem.id (*refine a Model_Pattern.T*)
1.454 + 07 | Refine_Problem of Problem.id (*refine a Model_Pattern.T*)
1.455 08 | Refine_Tacitly of Problem.id (*internal*)
1.456 - 09 | Specify_Method of MethodC.id (*specify References*)
1.457 + 09 | Specify_Method of MethodC.id (*specify References*)
1.458 10 | Specify_Problem of Problem.id | Specify_Theory of ThyC.id
1.459 11 (* for solve-phase *)
1.460 12 | ...
1.461 \end{verbatim}
1.462 \end{small}
1.463 -The above \texttt{Tactic}s are shown to the user, while some are used only
1.464 +The above @{ML_type Tactic.T}s are shown to the user, while some are used only
1.465 internally; \texttt{Refine\_*} will be introduced in \S\ref{ssec:refine} below.
1.466 A variant stuffed with lots of data serve internal construction of a next step;
1.467 the lists below shows only some examples:
1.468 \begin{small}
1.469 \begin{verbatim}
1.470 01 datatype T =
1.471 - 02 Add_Find' of TermC.as_string * I_Model.T | Add_Given' of TermC.as_string * I_Model.T
1.472 + 02 Add_Find' of TermC.as_string * I_Model.T
1.473 + 03 | Add_Given' of TermC.as_string * I_Model.T
1.474 04 | Add_Relation' of TermC.as_string * I_Model.T
1.475 - 05 | Model_Problem' of (*starts the specify-phase *)
1.476 - 06 Problem.id * (*key to a Problem.T Store.node*)
1.477 - 07 I_Model.T * (*model for the Problem *)
1.478 - 08 I_Model.T (*model for the MethoC *)
1.479 + 05 | Model_Problem' of (*starts the specify-phase *)
1.480 + 06 Problem.id * (*key to a Problem.T Store.node*)
1.481 + 07 I_Model.T * (*model for the Problem *)
1.482 + 08 I_Model.T (*model for the MethoC *)
1.483 09 | Refine_Problem' ...
1.484 \end{verbatim}
1.485 \end{small}
1.486 @@ -979,7 +995,7 @@
1.487 considerably when equation solving in sub-problems automatically refines to
1.488 the appropriate type of equation}.
1.489
1.490 -A \texttt{Problem.T} is defined in an Isabelle theory; here the definition of
1.491 +A @{ML_type Problem.T} is defined in an Isabelle theory; here the definition of
1.492 the model-pattern of the running example is shown.
1.493 \begin{figure} [htb]
1.494 \centering
1.495 @@ -988,13 +1004,13 @@
1.496 \label{fig:pbl-max-expl}
1.497 \end{figure}
1.498 This model-pattern covers almost all examples of a well-known text book, the items
1.499 -are identified by the \texttt{descriptor}s; variables like \texttt{fixes}
1.500 -are to be instantiated from a \texttt{Formalise.model} as explained on
1.501 +are identified by the @{ML_type descriptor}s; variables like \texttt{fixes}
1.502 +are to be instantiated from a @{ML_type Formalise.model} as explained on
1.503 p.\pageref{env-subst}.
1.504 The convenient representation in Fig.\ref{fig:pbl-max-expl}
1.505 is stuffed with data required to solve a problem
1.506 (see, for instance, the \texttt{$<$eval\_rls$>$}) and expanded to the type
1.507 -\texttt{Problem.T}:
1.508 +@{ML_type Problem.T}:
1.509 \begin{small}
1.510 \begin{verbatim}
1.511 01 type Problem.T =
1.512 @@ -1024,9 +1040,9 @@
1.513 \subsection{Efficiency Considerations with Parsing} \label{ssec:efficiency}
1.514 %------------------------------------------------------------------------------
1.515 Two decades ago, at the time when \sisac{} started with development, parsing
1.516 -required substantial resources. Thus a specific component, \texttt{O\_Model.T}
1.517 -was shifted in-between \texttt{Formalise.model} (p.\pageref{src:demo-expl})
1.518 -and the interaction model \texttt{I\_Model.T} (p.\pageref{src:i-model}).
1.519 +required substantial resources. Thus a specific component, @{ML_type O_Model.T}
1.520 +was shifted in-between @{ML_type Formalise.model} (p.\pageref{src:demo-expl})
1.521 +and the interaction model @{ML_type I_Model.T} (p.\pageref{src:i-model}).
1.522 \begin{small}
1.523 \begin{verbatim}
1.524 01 type O_Model.single =
1.525 @@ -1040,10 +1056,10 @@
1.526 \end{small}
1.527 This structure is created at the beginning of the specify-phase
1.528 (by \texttt{Tactic.Model\_Problem}). The terms are already parsed,
1.529 -\texttt{descriptor} and \texttt{values} conveniently separated;
1.530 +@{ML_type descriptor} and @{ML_type values} conveniently separated;
1.531 also the variants are ready for convenient handling. At the occasion of parsing
1.532 also an Isabelle \texttt{Proof\_Context} is fed with the types of all variables
1.533 -in \texttt{Formalise.model}. This discharges the student of the necessity
1.534 +in @{ML_type Formalise.model}. This discharges the student of the necessity
1.535 to explicitly input types.
1.536
1.537 \paragraph{Refinement of types of equations} as introduced by \UR\ref{UR:refine}
1.538 @@ -1051,21 +1067,21 @@
1.539 p.\pageref{fig:tre-of-equations} shows that already the old prototype
1.540 implemented quite a lot of types of equations. Refinement starts at the root
1.541 \texttt{["univariate", "equation"]} of the branch, an environment with respect
1.542 -to the given equation has to be created from the \texttt{I\_Model.T} and
1.543 -the current \texttt{Model\_Pattern.T},
1.544 +to the given equation has to be created from the @{ML_type I_Model.T} and
1.545 +the current @{ML_type Model_Pattern.T},
1.546 with this environment for each node in the tree the respective \texttt{"\#Given"}
1.547 and \texttt{"\#Where"} needs to be instantiated, and last not least the latter
1.548 requires evaluation by rewriting (see \S\ref{ssec:preconds} below).
1.549
1.550 All that tasks act on terms, i.e. require parsing. If this is done during interactive
1.551 problem solving, response time will get to high even with modern hardware.
1.552 -Thus not only \texttt{Problem.T} (see definition on p.\pageref{problem})
1.553 -contains terms alreay parsed, but also \texttt{Model\_Pattern.T} and other
1.554 +Thus not only @{ML_type Problem.T} (see definition on p.\pageref{problem})
1.555 +contains terms alreay parsed, but also @{ML_type Model_Pattern.T} and other
1.556 structures.
1.557 -These structures (\texttt{Model\_Pattern.T}, \texttt{Problem.T},
1.558 -\texttt{MethodC.T} and \texttt{Error\_Pattern.T}) hold terms, where the exact
1.559 +These structures (@{ML_type Model_Pattern.T}, @{ML_type Problem.T},
1.560 +@{ML_type MethodC.T} and \texttt{Error\_Pattern.T}) hold terms, where the exact
1.561 type is not known at compile time, and where the type needs to be adapted to
1.562 -the current \texttt{Problem.T}. Thus all these structures have a function
1.563 +the current @{ML_type Problem.T}. Thus all these structures have a function
1.564 \begin{small}
1.565 \begin{verbatim}
1.566 01 val adapt_to_type Proof.context -> T -> T
1.567 @@ -1085,11 +1101,11 @@
1.568 Pre-conditions are an essential part of a formal specification
1.569 (definition in \S\ref{ssec:urs-specify} Pt.\ref{UR:form-spec} on
1.570 p.\pageref{UR:form-spec}). We compare the definition to \sisac's representation
1.571 -of a \texttt{Model} (e.g. on p.\pageref{fig:specification-template},
1.572 +of a @{theory_text Model} (e.g. on p.\pageref{fig:specification-template},
1.573 p.\pageref{fig:specification-complete} or p.\pageref{fig:specification-method}):
1.574 \begin{center}
1.575 \begin{tabular}{ l | l}
1.576 - formal specification & \sisac's \texttt{Model} \\ \hline\hline
1.577 + formal specification & \sisac's @{theory_text Model} \\ \hline\hline
1.578 $\it{in}$ & \texttt{Given} \\ \hline
1.579 $\it{Pre}\;(\it{in})$ & \texttt{Where} \\ \hline
1.580 $\it{out}$ & \texttt{Find} \\ \hline
1.581 @@ -1097,15 +1113,15 @@
1.582 \hline
1.583 \end{tabular}
1.584 \end{center}
1.585 -However, \texttt{type Model\_Pattern.T} (defintion on p.\pageref{src:model-pattern})
1.586 +However, type @{ML_type Model_Pattern.T} (defintion on p.\pageref{src:model-pattern})
1.587 does \emph{not} contain a precondition ($\it{Pre}\;(\it{in})$, \texttt{Where})
1.588 -and so does the actual \texttt{Model} of a \texttt{Problem.T} (defintion on
1.589 +and so does the actual @{theory_text Model} of a @{ML_type Problem.T} (defintion on
1.590 p.\pageref{src:Problem-T}; for specifics of \texttt{Relate} see
1.591 p.\pageref{post-cond}).
1.592 -The reason is that the role of items in a \texttt{Model} is to
1.593 -conform with a particular \texttt{Formalise.model} (made ready by parsing
1.594 -in \texttt{I\_Model.T}) and whether it is present or not --
1.595 -whereas a precondition must evaluate to true in order to make a \texttt{Model}
1.596 +The reason is that the role of items in a @{theory_text Model} is to
1.597 +conform with a particular @{ML_type Formalise.model} (made ready by parsing
1.598 +in @{ML_type I_Model.T}) and whether it is present or not --
1.599 +whereas a precondition must evaluate to true in order to make a @{theory_text Model}
1.600 complete; this involves rewriting. The implementation details are as follows.
1.601 \begin{small}
1.602 \begin{verbatim}
1.603 @@ -1114,10 +1130,10 @@
1.604 03 type Pre_Conds.checked_pos = bool * ((bool * (term * Position.T)) list)
1.605 \end{verbatim}
1.606 \end{small}
1.607 -The role of preconditions is different from \texttt{Model}-items such that
1.608 -preconditions are stored only in a \texttt{Problem.T}
1.609 -(accompanied by a \texttt{Model}) and evaluated by use of environments,
1.610 -which are generated on the fly according to \texttt{I\_Model} actually
1.611 +The role of preconditions is different from @{theory_text Model}-items such that
1.612 +preconditions are stored only in a @{ML_type Problem.T}
1.613 +(accompanied by a @{theory_text Model}) and evaluated by use of environments,
1.614 +which are generated on the fly according to @{ML_type I_Model.T} actually
1.615 input:
1.616 \begin{small}
1.617 \begin{verbatim}
1.618 @@ -1171,8 +1187,8 @@
1.619 The sudden penetration of AI will pose the following new research tasks.
1.620 Starting from a differentiation of problem solving through
1.621 \begin{compactenum}
1.622 -\item intuitively and associatively thinking humans who bear
1.623 - responsibility for their actions
1.624 +\item intuitively and associatively thinking humans (who bear
1.625 + responsibility for their actions, etc)
1.626 \item AI with deep learning
1.627 \item formal mathematics
1.628 \end{compactenum}