1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/doc-isac/README Wed Mar 11 15:25:52 2020 +0100
1.3 @@ -0,0 +1,7 @@
1.4 +~~/doc-isac/README
1.5 +
1.6 +Much documentation is still in theses are found at
1.7 +https://isac.miraheze.org/wiki/Publications_and_Theses#Refereed_Papers
1.8 +
1.9 +In March 2020 formally checked documentation started in
1.10 +~~/src/Tools/isac/Doc
1.11 \ No newline at end of file
2.1 --- a/src/Tools/isac/CLEANUP Tue Mar 10 13:25:00 2020 +0100
2.2 +++ b/src/Tools/isac/CLEANUP Wed Mar 11 15:25:52 2020 +0100
2.3 @@ -57,6 +57,19 @@
2.4 rm *.orig~~
2.5 rm *.orig~~~
2.6 cd ..
2.7 +cd Doc
2.8 + rm *~
2.9 + cd Lucas_Interpreter
2.10 + rm *~
2.11 + cd document
2.12 + rm *~
2.13 + cd ..
2.14 + cd output
2.15 + rm *
2.16 + rm -rf document/
2.17 + cd ..
2.18 + cd ..
2.19 + cd ..
2.20 cd ProgLang
2.21 echo "cd ProgLang was successful -------------------------------------------------------------"
2.22 rm *.sml~
3.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
3.2 +++ b/src/Tools/isac/Doc/Lucas_Interpreter/Lucas_Interpreter.thy Wed Mar 11 15:25:52 2020 +0100
3.3 @@ -0,0 +1,615 @@
3.4 +(*<*)
3.5 +(*%:wrap=soft:maxLineLen=78:*)
3.6 +(*partially copied from
3.7 + ~/material/texts/emat/lucin-isa/paper-isabisac/Lucin_Isa_IJCAR.thy *)
3.8 +theory Lucas_Interpreter
3.9 + imports "~~/src/Tools/isac/Interpret/Interpret"
3.10 +begin
3.11 +ML \<open>
3.12 + open LI
3.13 + open Istate
3.14 + open TermC
3.15 +\<close>
3.16 +(*>*)
3.17 +
3.18 +text \<open>
3.19 +\section{Lucas--Interpretation (\LI)}\label{lucin}
3.20 +%=============================================================================
3.21 +The interpreter is named after the inventor of top-down-parsing in the ALGOL
3.22 +project~\cite{pl:formal-lang-hist}, Peter Lucas. As a dedicated expert in
3.23 +programming languages he initially objected ``yet another programming
3.24 +language'' (in analogy to ``Yacc'' \cite{Yacc-1975}), but then he helped to
3.25 +clarify the unusual requirements for a novel programming language in the
3.26 +\sisac-project, which later led to the notion of \LI.
3.27 +
3.28 +\LI{} is the most prominent component in a prototype developed in the
3.29 +\sisac-project, there embedded in a mathematics-engine, which interacts with a
3.30 +dialogue-module in a Java-based front-end managing interaction with students
3.31 +(out of scope of this paper).
3.32 +
3.33 +\subsection{The Concept of \LI}\label{concept-LI}
3.34 +%-----------------------------------------------------------------------------
3.35 +The concept of \LI{} is simple: \LI{} \emph{acts as a debugger on functional
3.36 +programs with hard-coded breakpoints, where control is handed over to a
3.37 +student; a student, however, does \emph{not} interact with the software
3.38 +presenting the program, but with the software presenting steps of forward
3.39 +reasoning, where the steps are rigorously constructed by tactics acting as the
3.40 +break-points mentioned}. Following the \LI{} terminology, we will call
3.41 +``programs'' the functions defined with the function package and refer to
3.42 +their evaluation as ``execution''.
3.43 +
3.44 +\paragraph{Types occurring in the signatures} of \LI{} are as follows. Besides
3.45 +the program of type @{ML_type Program.T} there is an interpreter state
3.46 +@{ML_type Istate.T}, a record type passing data from one step of execution to
3.47 +the next step, in particular a location in the program, where the next step
3.48 +will be read off, and an environment for evaluating the step.
3.49 +As invisible in the program language as the interpreter state is @{ML_type
3.50 +Calc.T}, a ``calculation'' as a sequence of steps in forward reasoning, a
3.51 +variant of ``structured derivations'' \cite{back-SD-2010}. Visible in the
3.52 +language and in the signature, however, are the tactics @{ML_type Tactic.T},
3.53 +which create steps in a calculation.
3.54 +
3.55 +Novel in connection with calculations is the idea to maintain a logical
3.56 +context in order to provide automated provers with data required for checking
3.57 +input by the student. Isabelle's @{ML_type Proof.context}, as is, turned out
3.58 +perfect for this task~\cite{mlehnf:bakk-11}.
3.59 +
3.60 +\paragraph{The signatures of the main functions,} the functions @{term
3.61 +find_next_step}, \\@{term locate_input_tactic} and @{term locate_input_term},
3.62 +are as follows:\label{sig-lucin}
3.63 +\<close>
3.64 +(*<*)ML(*>*) \<open>
3.65 +signature LUCAS_INTERPRETER =
3.66 +sig
3.67 + datatype next_step_result =
3.68 + Next_Step of Istate.T * Proof.context * Tactic.T
3.69 + | Helpless | End_Program of Istate.T * Tactic.T
3.70 + val find_next_step: Program.T -> Calc.T -> Istate.T -> Proof.context
3.71 + -> next_step_result
3.72 +
3.73 + datatype input_tactic_result =
3.74 + Safe_Step of Istate.T * Proof.context * Tactic.T
3.75 + | Unsafe_Step of Istate.T * Proof.context * Tactic.T
3.76 + | Not_Locatable of message
3.77 + val locate_input_tactic: Program.T -> Calc.T -> Istate.T -> Proof.context
3.78 + -> Tactic.T -> input_tactic_result
3.79 +
3.80 + datatype input_term_result =
3.81 + Found_Step of Calc.T | Not_Derivable
3.82 + val locate_input_term: Calc.T -> term -> input_term_result
3.83 +end
3.84 +\<close>
3.85 +text \<open>
3.86 +\begin{description}
3.87 +\item[@{term find_next_step}] accomplishes what usually is expected from a
3.88 +@{ML_type Program.T}: find a @{term Next_Step} to be executed, in the case of
3.89 +\LI{} to be inserted into a \texttt{\small Calc.T} under construction. This
3.90 +step can be a @{ML_type Tactic.T}, directly found in @{term next_step_result},
3.91 +or a @{ML_type term} produced by applying the tactic. If such a step cannot be
3.92 +found (due to previous student interaction), \LI{} is @{term Helpless}.
3.93 +
3.94 +\item[@{term locate_input_tactic}] gets a @{ML_type Tactic.T} as argument
3.95 +(which has been input and checked applicable in @{ML_type Calc.T}) and tries
3.96 +to locate it in the \texttt{Prog.T} such that a @{term Next_Step} can be
3.97 +generated from the subsequent location in the @{ML_type Program.T}. A step can
3.98 +be an @{term Unsafe_Step}, if the input @{ML_type Tactic.T} cannot safely be
3.99 +associated with any tactic in the @{ML_type Program.T}. This function has a
3.100 +signature similar to @{term find_next_step} (here the respective input
3.101 +@{ML_type Tactic.T} and the one in the result are the same) in order to unify
3.102 +internal technicalities of \LI{}.
3.103 +
3.104 +\item[@{term locate_input_term}] tries to find a derivation from the current
3.105 +@{ML_type Proof.context} for the term input to @{ML_type Calc.T} and to locate
3.106 +a \texttt{Tactic.T} in the @{ML_type Program.T}, which as @{term Found_Step}
3.107 +allows to find a next step later. Such a @{term Found_Step} can be located in
3.108 +another program (a sub-program or a calling program); thus @{ML_type
3.109 +Program.T}, @{ML_type Istate.T} and @{ML_type Proof.context} are packed into
3.110 +@{ML_type Calc.T} at appropriate positions and do not show up in the
3.111 +signature.
3.112 +\end{description}
3.113 +
3.114 +Automated reasoning is concern of the third function @{term
3.115 +locate_input_term}, actually a typical application case for Isabelle's
3.116 +Sledgehammer~\cite{sledgehammer-tutorial}, but not yet realised and
3.117 +preliminarily substituted by \sisac's simplifier. @{term locate_input_term} is
3.118 +the function used predominantly in interaction with students: these input term
3.119 +by term into the calculation under construction (as familiar from
3.120 +paper\&pencil work) and \LI{} checks for correctness automatically.
3.121 +\<close>
3.122 +text \<open>
3.123 +\subsection{Examples for \LI}\label{expl-lucin}
3.124 +%-----------------------------------------------------------------------------
3.125 +\LI's novel concept relating program execution with construction of
3.126 +calculations is best demonstrated by examples. The first one is from
3.127 +structural engineering given by the following problem statement:\\
3.128 +\medskip
3.129 +
3.130 +% first column
3.131 +\begin{minipage}{0.55\textwidth}
3.132 +\textit{Determine the bending line of a beam of length $L$,
3.133 +which consists of homogeneous material, which is clamped on one side
3.134 +and which is under constant line load $q_0$; see the Figure right.}\\
3.135 +\end{minipage}
3.136 +\hfill
3.137 +%second column
3.138 +\begin{minipage}{0.42\textwidth}
3.139 + \includegraphics[width=0.6\textwidth]{bend-7-70-en.png}\\
3.140 +\end{minipage}
3.141 +
3.142 +\medskip
3.143 +This problem is solved by the following program, which is shown by a
3.144 +screen-shot\footnote{The corresponding code is at
3.145 +\url{https://hg.risc.uni-linz.ac.at/wneuper/isa/file/df1b56b0d2a2/src/Tools/isac/Knowledge/Biegelinie.thy\#l174}.
3.146 +%When inner syntax double-quotes are discontinued eventually, the inner syntax
3.147 +of the HOL library may use double quotes for char/string literals, instead of
3.148 +slightly odd double single-quotes.
3.149 +}
3.150 +in order to demonstrate the colouring helpful for programmers (compare the old
3.151 +bare string version in \cite[p.~92]{wn:proto-sys}).
3.152 +\begin{figure} [htb]
3.153 + \centering
3.154 + \includegraphics[width=\textwidth]{fun-pack-biegelinie-2.png}
3.155 + \caption{The program implemented by the function package}
3.156 + \label{fig:fun-pack-biegelinie}
3.157 +\end{figure}
3.158 +The program is implemented as a @{theory_text partial_function}: it calculates
3.159 +results for a whole class of problems and termination cannot be proven in such
3.160 +generality, although preconditions guard execution.
3.161 +%
3.162 +The program reflects a ``divide \& conquer'' strategy by calling three @{term
3.163 +SubProblem}s. It was implemented for field-tests in German-speaking countries,
3.164 +so arguments of the @{term SubProblem}s are in German, because they appear in
3.165 +the calculation as well. The third @{term SubProblem} adopts the format from
3.166 +Computer Algebra. The calculation, if finished successfully, looks as follows
3.167 +(a screen-shot of intermediate steps on the prototype's front-end is shown in
3.168 +\cite[p.~97]{wn:proto-sys}):\label{biegel_calc}
3.169 +{\footnotesize\begin{tabbing}
3.170 +123\=12\=12\=12\=12\=12\=12\=123\=123\=123\=123\=\kill
3.171 +01\> Problem (Biegelinie, [Biegelinien]) \\
3.172 +02\>\> Specification: \\
3.173 +03\>\> Solution: \\
3.174 +04\>\>\> Problem (Biegelinie, [vonBelastungZu, Biegelinien]) \\
3.175 +05\>\>\> $[$\>$V\,x = c + -1\cdot q_0\cdot x, $\\
3.176 +06\>\>\> \>$M_b\,x = c_2 + c\cdot x + \frac{-1\cdot q_0}{2\cdot x ^ 2}, $\\
3.177 +07\>\>\> \>$\frac{d}{dx}y\,x = c_3 + \frac{-1}{EI} \cdot (c_2\cdot x +
3.178 +\frac{c}{2\cdot x ^ 2} + \frac{-1\cdot q_0}{6\cdot x ^ 3}, $\\
3.179 +08\>\>\> \>$y\,x = c_4 + c_3\cdot x + \frac{-1}{EI} \cdot
3.180 +(\frac{c_2}{2}\cdot x ^ 2 + \frac{c}{6}\cdot x ^ 3 + \frac{-1\cdot
3.181 +q_0}{24}\cdot x ^ 4)\;\;]$ \\
3.182 +09\>\>\> Problem (Biegelinie, [setzeRandbedingungen, Biegelinien])\\
3.183 +10\>\>\> $[$\>$L \cdot q_0 = c,\; 0 = \frac{2 \cdot c_2 + 2 \cdot L \cdot c +
3.184 +-1 \dot L ^ 2 \cdot q_0}{2},\; 0 = c_4,\; 0 = c_3\;\;]$\\
3.185 +11\>\>\> solveSystem $(L \cdot q_0 = c,\; 0 = \frac{2 \cdot c_2 + 2 \cdot L
3.186 +\cdot c + -1 \cdot L ^ 2 \cdot q_0}{2},\; 0 = c_4,\; 0 = c_3\;\;],\; [c, c_2,
3.187 +c_3, c_4])$\\
3.188 +12\>\>\> $[$\>$c = L \cdot q_0 ,\; c_2 = \frac{-1 \cdot L ^ 2 \cdot q_0}{2},\;
3.189 +c_3 = 0,\; c_4 = 0]$\\
3.190 +13 \` Take $y\,x = c_4 + c_3\cdot x + \frac{-1}{EI} \cdot
3.191 +(\frac{c_2}{2}\cdot x ^ 2 + \frac{c}{6}\cdot x ^ 3 + \frac{-1\cdot
3.192 +q_0}{24}\cdot x ^ 4)$ \\
3.193 +
3.194 +14\>\>\> $y\,x = c_4 + c_3 \cdot x + \frac{-1}{EI} \cdot (\frac{c_2}{2} \cdot
3.195 +x ^ 2 + \frac{c}{6} \cdot x ^ 3 + \frac{-1 \cdot q_0}{24} \cdot x ^ 4)$\\
3.196 +15 \` Substitute $[c,c_2,c_3,c_4]$ \\
3.197 +
3.198 +16\>\>\> $y\,x = 0 + 0 \cdot x + \frac{-1}{EI} \cdot (\frac{\frac{-1 \cdot L ^
3.199 +2 \cdot q_0}{2}}{2} \cdot x ^ 2 + \frac{L \cdot q_0}{6} \cdot x ^ 3 + \frac{-1
3.200 +\cdot q_0}{24} \cdot x ^ 4)$\label{exp-biegel-Substitute}\\
3.201 +17 \` Rewrite\_Set\_Inst $([({\it bdv},x)], {\it make\_ratpoly\_in})$ \\
3.202 +
3.203 +18\>\>\> $y\;x = \frac{q_0 \cdot L ^ 2}{4 \cdot EI} \cdot x ^ 2 + \frac{L
3.204 +\cdot q_0 }{6 \cdot EI} \cdot x ^ 3 + \frac{q_0}{24 \cdot EI} \cdot x ^ 4$\\
3.205 +19\> $y\;x = \frac{q_0 \cdot L ^ 2}{4 \cdot EI} \cdot x ^ 2 + \frac{L \cdot
3.206 +q_0 }{6 \cdot EI} \cdot x ^ 3 + \frac{q_0}{24 \cdot EI} \cdot x ^ 4$
3.207 +\end{tabbing}}
3.208 +The calculation is what a student interacts with. Above the \texttt{\small
3.209 +Specification} is folded in, the specification phase and respective user
3.210 +interaction is skipped here. The \texttt{\small Solution} must be constructed
3.211 +step-wise line by line (while the line numbers do not belong to the
3.212 +calculation) in forward reasoning.
3.213 +\label{1-2-3}A student inputs either (1) a term (displayed on the left above
3.214 +with indentations) or (2) a tactic (shifted to the right margin). If the
3.215 +student gets stuck (3) a next step (as a term or a tactic) is suggested by
3.216 +\LI{}, which works behind the scenes; the corresponding functions have been
3.217 +introduced in \S\ref{concept-LI} (for (1) @{term locate_input_term}, (2)
3.218 +@{term locate_input_tactic} and for (3) @{term find_next_step}).
3.219 +
3.220 +\medskip
3.221 +This example hopefully clarifies the relation between program and calculation
3.222 +in \LI{}: execution of the program stops at tactics (above called
3.223 +break-points), displays the tactic or the result produced by the tactic (as
3.224 +decided by the dialogue-module) in the calculation under construction, hands
3.225 +over control to the student working on the calculation and resumes checking
3.226 +user input.
3.227 +
3.228 +\paragraph{A typical example from Computer Algebra}\label{expl-rewrite} shall
3.229 +shed light on a notions introduced later, on tacticals. The program in
3.230 +Fig.\ref{fig:fun-pack-diff} %on p.\pageref{fig:fun-pack-diff}
3.231 +simplifies rational terms (typed as ``real'' due to limited development
3.232 +resources):
3.233 +\begin{figure} [htb]
3.234 + \centering
3.235 + \includegraphics[width=0.95\textwidth]{fun-pack-simplify.png}
3.236 + %\includegraphics[width=0.85\textwidth]{fig/scrshot/fun-pack/fun-pack-diff.png}
3.237 + \caption{Simplification implemented by the function package}
3.238 + \label{fig:fun-pack-diff}
3.239 +\end{figure}
3.240 +
3.241 +The program executes the tactic @{const Rewrite'_Set}\footnote{Isabelle's
3.242 +document preparation system preserves the apostroph from the definition, while
3.243 +Isabelle's pretty printer drops it in the presentation of the program as
3.244 +above.}
3.245 +with different canonical term rewriting systems (called ``rule sets'' in
3.246 +\sisac) guided by tacticals. The output (disregarding user interaction) is a
3.247 +calculation with steps of simplification, where the steps are created by
3.248 +@{const Rewrite'_Set}.
3.249 +
3.250 +Chained functions (by \texttt{\small \#>}) %TODO which antiquot?
3.251 +are applied curried to @{ML_type term}. The initial part of the chain, from
3.252 +\texttt{\small ''discard\_minus''} to \texttt{\small ''cancel''} does
3.253 +preprocessing, for instance replaces $\;a - b\;$ by $\;a + (-b)\;$ in
3.254 +\texttt{\small ''discard\_minus''} for reducing
3.255 +the number of theorems to be used in simplification.
3.256 +%
3.257 +The second chain of @{const Rewrite'_Set} is @{const Repeat}ed until no
3.258 +further rewrites are possible; this is necessary in case of nested fractions.
3.259 +
3.260 +In cases like the one above, a confluent and terminating term rewrite system,
3.261 +not only \emph{all} correct input terms are accepted, but also \emph{all}
3.262 +incorrect input is rejected as @{term Not_Derivable} by the function @{term
3.263 +locate_input_term}.
3.264 +
3.265 +
3.266 +\section{Adaptation of Isabelle's Functions}\label{lucin-funpack}
3.267 +%=============================================================================
3.268 +Isabelle's function package presents functions in ``inner syntax'' to users,
3.269 +i.e. as terms in Isabelle/HOL. The \LI{} design recognised these terms
3.270 +suitable for parse trees of programs, Isabelle realised the same idea in a
3.271 +more general way with the function package a few years later --- so migration
3.272 +from \sisac's programs to Isabelle's functions was surprisingly easy. The main
3.273 +features required were tactics, tacticals and program expressions as described
3.274 +below.
3.275 +
3.276 +\subsection{Tactics Creating Steps in Calculations}\label{tactics}
3.277 +%-----------------------------------------------------------------------------
3.278 +The examples in the previous section showed how tactics in programs create
3.279 +steps in calculations. Tactics in programs are defined as follows\footnote{
3.280 +\url{https://hg.risc.uni-linz.ac.at/wneuper/isa/file/df1b56b0d2a2/src/Tools/isac/ProgLang/Prog_Tac.thy\#l36}}
3.281 +:
3.282 +\<close>
3.283 +consts
3.284 + Calculate :: "[char list, 'a] => 'a"
3.285 + Rewrite :: "[char list, 'a] => 'a"
3.286 + Rewrite'_Inst :: "[(char list * 'a) list, char list, 'a] => 'a"
3.287 + Rewrite'_Set :: "[char list, 'a] => 'a"
3.288 + Rewrite'_Set'_Inst :: "[((char list) * 'a) list, char list, 'a] => 'a"
3.289 + Or'_to'_List :: "bool => 'a list"
3.290 + SubProblem ::
3.291 + "[char list * char list list * char list list, arg list] => 'a"
3.292 + Substitute :: "[bool list, 'a] => 'a"
3.293 + Take :: "'a => 'a"
3.294 +
3.295 +text \<open>
3.296 +These tactics transform a term of some type @{typ "'a"} to a resulting term of
3.297 +the same type. @{const[names_short] Calculate} applies operators like $+,-,*$
3.298 +as @{typ "char list"} (i.e. a string in inner syntax) to numerals of type
3.299 +@{typ "'a"}. The tactics beginning with @{const[names_short] Rewrite} do
3.300 +exactly what they indicate by applying a theorem (in the program given by type
3.301 +@{typ "char list"}) or a list of theorems, called ``rule-set''. The
3.302 +corresponding \texttt{\small \_Inst} variants instantiate bound variables with
3.303 +respective constants before rewriting (this is due to the user requirement,
3.304 +that terms in calculations are close to traditional notation, which excludes
3.305 +$\lambda$-terms), for instance modelling bound variables in equation solving.
3.306 +@{const[names_short] Or'_to'_List} is due to a similar requirement: logically
3.307 +appropriate for describing solution sets in equation solving are equalities
3.308 +connected by $\land,\lor$, but traditional notation uses sets (and these are
3.309 +still lists for convenience). @{const[names_short] SubProblem}s not only take
3.310 +arguments (@{typ "arg list"} like any (sub-)program, but also three references
3.311 +into \sisac's knowledge base (theory, formal specification, method) for
3.312 +guided interaction in the specification phase.
3.313 +
3.314 +Tactics appear simple: they operate on terms adhering to one type ---
3.315 +different types are handled by different tactics and (sub-) programs; and they
3.316 +cover only basic functionality --- but they operate on terms, which are well
3.317 +tooled by Isabelle and which can contain functions evaluated as program
3.318 +expressions introduced in the next but one subsection.
3.319 +
3.320 +Section \S\ref{expl-lucin} showed how tactics can be input by students. So
3.321 +tactics in programs have analogies for user input with type @{ML_type
3.322 +Tactic.input} defined at\footnote{
3.323 +\url{https://hg.risc.uni-linz.ac.at/wneuper/isa/file/df1b56b0d2a2/src/Tools/isac/MathEngBasic/tactic-def.sml\#l122}}. These tactics also cover the specification phase (wich is out of scope of the
3.324 +paper). And there is another @{ML_type Tactic.T} defined at\footnote{
3.325 +\url{https://hg.risc.uni-linz.ac.at/wneuper/isa/file/df1b56b0d2a2/src/Tools/isac/MathEngBasic/tactic-def.sml\#l241}} for internal use by the mathematics-engine, which already appeared in the
3.326 +signature of Lucas-Interpretation on p.\pageref{sig-lucin}.
3.327 +
3.328 +\subsection{Tacticals Guiding Flow of Execution}\label{tacticals}
3.329 +%-----------------------------------------------------------------------------
3.330 +The example on p.\pageref{expl-rewrite} for canonical rewriting showed, how
3.331 +tacticals guide the flow of execution. The complete list of tacticals is as
3.332 +follows.
3.333 +\<close>
3.334 +consts
3.335 + Chain :: "['a => 'a, 'a => 'a, 'a] => 'a" (infixr "#>" 10)
3.336 + If :: "[bool, 'a => 'a, 'a => 'a, 'a] => 'a"
3.337 + Or :: "['a => 'a, 'a => 'a, 'a] => 'a" (infixr "Or" 10)
3.338 + Repeat :: "['a => 'a, 'a] => 'a"
3.339 + Try :: "['a => 'a, 'a] => 'a"
3.340 + While :: "[bool, 'a => 'a, 'a] => 'a" ("((While (_) Do)//(_))" 9)
3.341 +
3.342 +text \<open>
3.343 +\texttt{\small Chain} is forward application of functions and made an infix
3.344 +operator @{const[names_short] Chain}; @{const[names_short] If} decides by
3.345 +@{typ bool}en expression for execution of one of two arguments of type @{typ
3.346 +"'a => 'a"} (which can be combinations of tacticals or tactics);
3.347 +@{const[names_short] Or} decides on execution of one of the arguments
3.348 +depending of applicability of tactics; @{const[names_short] Repeat} is a one
3.349 +way loop which terminates, if the argument is not applicable (e.g.
3.350 +applicability of a theorem for rewriting on a term) any more;
3.351 +@{const[names_short] Try} skips the argument if not applicable and
3.352 +@{const[names_short] While} is a zero way loop as usual.
3.353 +
3.354 +\subsection{Program Expressions to be Evaluated}\label{prog-expr}
3.355 +%-----------------------------------------------------------------------------
3.356 +Some tacticals, \texttt{If} and \texttt{While}, involve boolean expressions,
3.357 +which need to be evaluated: such expressions denote another element of
3.358 +programs. This kind of element has been shown in the example on
3.359 +p.\pageref{fig:fun-pack-biegelinie} as argument of @{const[names_short]
3.360 +Take}: sometimes it is necessary to pick parts of elements of a calculation,
3.361 +for instance the last element from a list. So Isabelle's @{theory_text List}
3.362 +is adapted for \sisac's purposes in @{theory_text ListC}\footnote{
3.363 +\url{https://hg.risc.uni-linz.ac.at/wneuper/isa/file/df1b56b0d2a2/src/Tools/isac/ProgLang/ListC.thy}}.
3.364 +%
3.365 +Such expressions are substituted from the environment in @{ML_type Istate.T},
3.366 +evaluated to terms by rewriting (and for that purpose using the same rewrite
3.367 +engine as for the tactics @{const[names_short] Rewrite}*) and marked by the
3.368 +constructor @{term Term_Val} which is introduced below.
3.369 +
3.370 +
3.371 +\section{Implementation of \LI}\label{LI-impl}
3.372 +%=============================================================================
3.373 +The implementation of the interpreter is as experimental as is the respective
3.374 +programming language introduced in the previous section. So below there will
3.375 +be particularly such implementation details, which are required for discussing
3.376 +open design \& implementation issues.
3.377 +
3.378 +All of the function package's syntactic part plus semantic markup is perfect
3.379 +for \LI. The evaluation part of the function package, however, implements
3.380 +automated evaluation in one go and automated
3.381 +code-generation~\cite{code-gen-tutorial} --- both goals are not compatible
3.382 +with \sisac's goal to feature step-wise construction of calculations, so this
3.383 +part had to be done from scratch.
3.384 +
3.385 +
3.386 +\subsection{Scanning the Parse Tree}\label{scanning}
3.387 +%-----------------------------------------------------------------------------
3.388 +Isabelle's function package parses the program body from function definitions
3.389 +to terms, the data structure of simply typed $\lambda$ terms, which also
3.390 +encode the objects of proofs. Thus there is a remarkable collection of tools,
3.391 +readily available in Isabelle; but this collection does not accommodate the
3.392 +requirement of scanning a term to a certain location, remembering the location
3.393 +and returning there later, as required by \LI. So this has been introduced
3.394 +\<close>
3.395 +(*<*)ML(*>*) \<open>
3.396 +datatype lrd = L | R | D
3.397 +type path = lrd list
3.398 +\<close>
3.399 +(*<*)ML \<open>
3.400 +open TermC (*avoids type clashes below from the new typ above*)
3.401 +\<close>
3.402 + ML(*>*) \<open>
3.403 +fun at_location [] t = t
3.404 + | at_location (D :: p) (Abs(_, _, body)) = at_location p body
3.405 + | at_location (L :: p) (t1 $ _) = at_location p t1
3.406 + | at_location (R :: p) (_ $ t2) = at_location p t2
3.407 + | at_location l t =
3.408 + raise TERM ("at_location: no " ^ string_of_path l ^ " for ", [t]);
3.409 +\<close>
3.410 +text \<open>
3.411 +with a @{term path} to a location according to the term constructors
3.412 +\texttt{\small \$} and @{term Abs}. This is an implementation detail; an
3.413 +abstract, denotational view starts with this datatype
3.414 +\<close>
3.415 +(*<*)ML(*>*) \<open>
3.416 +datatype expr_val =
3.417 + Term_Val of term | Reject_Tac
3.418 + | Accept_Tac of Istate.pstate * Proof.context * Tactic.T
3.419 +\<close>
3.420 +text \<open>
3.421 +which models the meaning of an expression in the parse-tree: this is either a
3.422 +@{term Term_Val}ue (introduced in \S\ref{prog-expr}) or a tactic (introduced
3.423 +in \S\ref{tactics}); the latter is either accepted by @{term Accept_Tac} or
3.424 +rejected by @{term Reject_Tac}; an error value is still missing.
3.425 +%
3.426 +The arguments of the above constant @{term Accept_Tac} are the same as
3.427 +introduced for \LI{} in \S\ref{concept-LI}. Thus @{ML_type expr_val} is the
3.428 +return value for functions scanning the parse-tree for an acceptable tactic:
3.429 +\<close>
3.430 +(*<*)ML \<open>
3.431 +open LI (*avoids type clashes below from the new typ above*)
3.432 +\<close>
3.433 + ML(*>*) \<open>
3.434 +scan_to_tactic: term * (Calc.T * Proof.context) -> Istate.T -> expr_val;
3.435 +scan_dn: Calc.T * Proof.context -> Istate.pstate -> term -> expr_val;
3.436 +go_scan_up: term * (Calc.T * Proof.context) -> Istate.pstate -> expr_val;
3.437 +scan_up: term * (Calc.T * Proof.context) -> Istate.pstate -> term -> expr_val;
3.438 +check_tac: Calc.T * Proof.context -> Istate.pstate -> term * term option ->
3.439 +expr_val;
3.440 +\<close>
3.441 +text \<open>
3.442 +The first argument of each function above, if of type @{ML_type term}, is the
3.443 +whole program. It is not required by @{term scan_dn}, simple top-down
3.444 +scanning, and by @{term check_tac}, if a tactic has been reached. The
3.445 +rightmost argument, if of type @{ML_type term}, serves matching as shown
3.446 +later. @{term scan_to_tactic} recognises, whether interpretation is just
3.447 +starting a new program (@{term "path = []"}) or interpretation resumes at a
3.448 +certain location:
3.449 +\<close>
3.450 +(*<*)ML \<open>
3.451 +open Celem
3.452 +open LI
3.453 +\<close>
3.454 + ML(*>*) \<open>
3.455 +fun scan_to_tactic (prog, cc) (Pstate (ist as {path, ...})) =
3.456 + if path = []
3.457 + then scan_dn cc (ist |> set_path [R]) (Program.body_of prog)
3.458 + else go_scan_up (prog, cc) ist
3.459 + | scan_to_tactic _ _ =
3.460 + raise ERROR "scan_to_tactic1: uncovered pattern in fun.def"
3.461 +\<close>
3.462 + text \<open>
3.463 +@{term scan_dn} sets the path in the interpreter state @{term ist} to @{term
3.464 +R}, the program body, while @{term go_scan_up} goes one level up the path in
3.465 +order to call @{term go_scan_up}. Both functions, scanning down and up, are
3.466 +shown below\footnote{
3.467 +Referring to the example in Fig.\ref{fig:fun-pack-diff} on
3.468 +p.\pageref{fig:fun-pack-diff} we show the interpreter code only for tacticals
3.469 +@{const[names_short] Try}, @{const[names_short] Repeat} and chaining
3.470 +\texttt{\small \#>} (which is \texttt{\small "Tactical.Chain"} in the code).
3.471 +We also omit the cases for uncurried application, which only occurs once (in
3.472 +the first, i.e. the out-most @{const[names_short] Try}) in the example.
3.473 +}:
3.474 +\<close>
3.475 +(*<*)ML(*>*) \<open>
3.476 +fun scan_dn cc (ist as {act_arg, ...}) (Const ("Tactical.Try", _) $ e) =
3.477 + (case scan_dn cc (ist |> path_down [R]) e of
3.478 + Reject_Tac => Term_Val act_arg
3.479 + | goback => goback)
3.480 + | scan_dn cc ist (Const ("Tactical.Repeat", _) $ e) =
3.481 + scan_dn cc (ist |> path_down [R]) e
3.482 + | scan_dn cc ist (Const ("Tactical.Chain"(*2*), _) $ e1 $ e2) =
3.483 + (case scan_dn cc (ist |> path_down [L, R]) e1 of
3.484 + Term_Val v => scan_dn cc (ist |> path_down [R] |> set_act v) e2
3.485 + | goback => goback)
3.486 +(*|*)
3.487 + | scan_dn (cc as (_, ctxt)) (ist as {eval, ...}) t =
3.488 + if Tactical.contained_in t
3.489 + then raise TERM ("scan_dn expects Prog_Tac or Prog_Expr", [t])
3.490 + else
3.491 + case LItool.check_leaf "next " ctxt eval (get_subst ist) t of
3.492 + (Program.Expr s, _) => Term_Val s
3.493 + | (Program.Tac prog_tac, form_arg) =>
3.494 + check_tac cc ist (prog_tac, form_arg)
3.495 +\<close>
3.496 + text \<open>
3.497 +The last case of @{term scan_dn} must have reached a leaf. @{term check_leaf}
3.498 +distinguishes between @{term Expr} and @{term Tac}; the former returns a
3.499 +@{term Term_Val}, the latter returns the result of @{term check_tac} called by
3.500 +@{term scan_dn}, where the result is either @{term Accept_Tac} or @{term
3.501 +Reject_Tac}. In case of @{term Accept_Tac} scanning is stalled (in
3.502 +\S\ref{expl-lucin} such a tactic has been called a beak-point), the respective
3.503 +tactic is returned (together with corresponding @{ML_type Istate.T} and
3.504 +@{ML_type Proof.context}) to the mathematics-engine.
3.505 +In case of @{term Reject_Tac} an explicit back tracking by @{term scan_up}
3.506 +tries other branches with @{term scan_dn}.
3.507 +
3.508 +\medskip
3.509 +@{term scan_up} is as simple as @{term scan_dn}; an essential difference is,
3.510 +that the former requires the whole program for @{term go_scan_up} as follows:
3.511 +\<close>
3.512 +(*<*)ML(*>*) \<open>
3.513 +fun go_scan_up (pcc as (sc, _)) (ist as {path, act_arg, found_accept,...})=
3.514 + if path = [R]
3.515 + then
3.516 + if found_accept then Term_Val act_arg else Reject_Tac
3.517 + else
3.518 + scan_up pcc (ist |> path_up) (go_up path sc)
3.519 +and scan_up pcc ist (Const ("Tactical.Try"(*2*), _) $ _) = go_scan_up pcc ist
3.520 + | scan_up (pcc as (_, cc)) ist (Const ("Tactical.Repeat"(*2*), _) $ e) =
3.521 + (case scan_dn cc (ist |> path_down [R]) e of
3.522 + Accept_Tac ict => Accept_Tac ict
3.523 + | Reject_Tac => go_scan_up pcc ist
3.524 + | Term_Val v => go_scan_up pcc (ist |> set_act v |> set_found))
3.525 + | scan_up pcc ist (Const ("Tactical.Chain"(*2*), _) $ _ $ _) =
3.526 + go_scan_up pcc ist
3.527 + | scan_up (pcc as (sc, cc)) ist (Const ("Tactical.Chain"(*3*), _) $ _) =
3.528 + let
3.529 + val e2 = check_Seq_up ist sc
3.530 + in
3.531 + case scan_dn cc (ist |> path_up_down [R]) e2 of
3.532 + Accept_Tac ict => Accept_Tac ict
3.533 + | Reject_Tac => go_scan_up pcc (ist |> path_up)
3.534 + | Term_Val v => go_scan_up pcc (ist |> path_up |> set_act v |>
3.535 +set_found)
3.536 + end
3.537 +(*|*)
3.538 +\<close>
3.539 +text \<open>
3.540 +\subsection{Use of Isabelle's Contexts}\label{ctxt}
3.541 +%-----------------------------------------------------------------------------
3.542 +Isabelle's \textit{``logical context represents the background that is
3.543 +required for formulating statements and composing proofs. It acts as a medium
3.544 +to produce formal content, depending on earlier material (declarations,
3.545 +results etc.).''} \cite{implem-tutorial}. The \sisac-prototype introduced
3.546 +Isabelle's @{ML_structure Context} in collaboration with a
3.547 +student~\cite{mlehnf:bakk-11}, now uses them throughout construction of
3.548 +problem solutions and implements a specific structure @{ML_structure
3.549 +ContextC}\footnote{A closing ``C'' indicates an \sisac{} extension, see
3.550 +{\url{https://hg.risc.uni-linz.ac.at/wneuper/isa/file/00612574cbfd/src/Tools/isac/CalcElements/contextC.sml}}}.
3.551 +
3.552 +At the beginning of the specification phase (briefly touched by tactic
3.553 +@{term[names_short] SubProblem} in \S\ref{expl-lucin} and explained in little
3.554 +more detail in the subsequent section) an Isabelle theory must be specified,
3.555 +this is followed by \texttt{\small Proof\_Context.init\_global} in the
3.556 +specification module. Then \texttt{\small Proof\_Context.initialise'} takes a
3.557 +formalisation of the problem as strings, which are parsed by \texttt{\small
3.558 +Syntax.read\_term} using the context, and finally the resulting term's types
3.559 +are recorded in the context by \texttt{\small Variable.declare\_constraints}.
3.560 +The latter relieves students from type constraints for input terms. Finally,
3.561 +as soon as a problem type is specified, the respective preconditions are
3.562 +stored by \texttt{\small ContextC.insert\_assumptions}.
3.563 +
3.564 +\medskip
3.565 +During \LI{} the context is updated with assumptions generated by conditional
3.566 +rewriting and by switching to and from sub-programs. An example for the former
3.567 +is tactic @{term[names_short] SubProblem} applied with theorem $x \ne 0
3.568 +\Rightarrow (\frac{a}{x} = b) = (a = b\cdot x)$ during equation solving.
3.569 +
3.570 +A still not completely solved issue is switching to and from
3.571 +@{term[names_short] SubProblem}s; the scope of an interpreter's environment is
3.572 +different from a logical context's scope. When calling a sub-program, \sisac{}
3.573 +uses \texttt{\small Proof\_Context.initialise}, but returning execution from a
3.574 +@{term[names_short] SubProblem} is not so clear. For instance, if such a
3.575 +sub-program determined the solutions $[x=0,\;x=\sqrt{2}]$, while the calling
3.576 +program maintains the assumption $x\not=0$ from above, then the solution $x=0$
3.577 +must be dropped, this is clear. But how determine in full generality, which
3.578 +context data to consider when returning execution to a calling program?
3.579 +Presently the decision in \texttt{\small
3.580 +ContextC.subpbl\_to\_caller}\footnote{
3.581 +\url{https://hg.risc.uni-linz.ac.at/wneuper/isa/file/ce071aa3eae4/src/Tools/isac/CalcElements/contextC.sml\#l73}}
3.582 +is, to transfer all content data which contain at least one variable of the
3.583 +calling program and drop them on contradiction.
3.584 +
3.585 +\subsection{Guarding and Embedding Execution}\label{embedding}
3.586 +%-----------------------------------------------------------------------------
3.587 +Guardin
3.588 +
3.589 +@{theory_text partial_function}s as used by \LI{} are alien to HOL for
3.590 +fundamental reasons. And when the \sisac-project started with the aim to
3.591 +support learning mathematics as taught at engineering faculties, it was clear,
3.592 +that formal specifications should guard execution of programs under \LI{}
3.593 +(i.e. execution only starts, when the specification's preconditions evaluate
3.594 +to true).
3.595 +
3.596 +So formal specification is required for technical reasons \emph{and} for
3.597 +educational reasons in engineering education. The \sisac-project designed a
3.598 +separate specification phase, where input to a problem and corresponding
3.599 +output as well as preconditions and post-condition are handled explicitly by
3.600 +students; example in Fig.\ref{fig:fun-pack-biegelinie} shows several
3.601 +@{term[names_short] SubProblem}s, which lead to mutual recursion between
3.602 +specification phase and phases creating a solution (supported by \LI).
3.603 +
3.604 +\paragraph{Embedding} \LI{} into a dialogue-module is required in order to
3.605 +meet user requirements in educational settings. Looking at the calculation
3.606 +shown on p.\pageref{biegel_calc} and considering the power of the three
3.607 +mainfunction (1)\dots(3) mentioned in the respective comment on
3.608 +p.\pageref{1-2-3}, it is clear, that in particular @{term[names_short]
3.609 +find_next_step} needs control: The dialogue-module hands over control to a
3.610 +student at each step of \LI, but students should also be warned against using
3.611 +a button creating the next step too frequently. A careful reduction of help
3.612 +from \LI{} might make the learning system also usable for written exams.
3.613 +
3.614 +\<close>
3.615 +
3.616 +(*<*)
3.617 +end
3.618 +(*>*)
4.1 Binary file src/Tools/isac/Doc/Lucas_Interpreter/document/bend-7-70-en.png has changed
5.1 Binary file src/Tools/isac/Doc/Lucas_Interpreter/document/fun-pack-biegelinie-2.png has changed
6.1 Binary file src/Tools/isac/Doc/Lucas_Interpreter/document/fun-pack-simplify.png has changed
7.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
7.2 +++ b/src/Tools/isac/Doc/Lucas_Interpreter/document/root.bib Wed Mar 11 15:25:52 2020 +0100
7.3 @@ -0,0 +1,351 @@
7.4 +
7.5 +@Proceedings{EPTCS79,
7.6 + title = {{\rm Proceedings First Workshop on}
7.7 + CTP Components for Educational Software (THedu'11)},
7.8 + year = {2012},
7.9 + booktitle = {Electronic Proceedings in Theoretical Computer Science},
7.10 + editor = "Quaresma, Pedro and Back, Ralph-Johan",
7.11 + volume = "79",
7.12 + publisher = "Open Publishing Association"
7.13 +}
7.14 +@techreport{RISC5885,
7.15 +author = {David M. Cerna},
7.16 +title = {{Evaluation of the VL Logic (342.208-9) 2018W End of Semester Questionnaire}},
7.17 +year = {2019},
7.18 +month = {Feburary},
7.19 +length = {17},
7.20 +type = {RISC Report Series},
7.21 +institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz},
7.22 +address = {Schloss Hagenberg, 4232 Hagenberg, Austria}
7.23 +}
7.24 +@Article{EMS-STT-19,
7.25 + author = {Koichu, Boris and Pinto, Alon},
7.26 + title = {The Seoncdary-Tertiary Transition in Mathematics. What are our current challenges and what can we do about them?},
7.27 + journal = {EMS Newsletter},
7.28 + year = {2019},
7.29 + pages = {34-35},
7.30 + month = {June},
7.31 + doi = {10.4171/NEWS}
7.32 +}
7.33 +
7.34 +@Inproceedings{EPTCS290.6,
7.35 + author = {Neuper, Walther},
7.36 + year = {2019},
7.37 + title = {Technologies for "Complete, Transparent \& Interactive Models of Math" in Education},
7.38 + editor = {Quaresma, Pedro and Neuper, Walther},
7.39 + booktitle = {{\rm Proceedings 7th International Workshop on}
7.40 + Theorem proving components for Educational software,
7.41 + {\rm Oxford, United Kingdom, 18 july 2018}},
7.42 + series = {Electronic Proceedings in Theoretical Computer Science},
7.43 + volume = {290},
7.44 + publisher = {Open Publishing Association},
7.45 + pages = {76-95},
7.46 + doi = {10.4204/EPTCS.290.6}
7.47 +}
7.48 +@InProceedings{wneuper:gcd-coimbra,
7.49 + author = {Neuper, Walther},
7.50 + title = {{GCD} --- A Case Study on {L}ucas-Interpretation},
7.51 + booktitle = {Joint Proceedings of the MathUI, OpenMath and ThEdu Workshops and Work in Progress track at CICM},
7.52 + year = {2014},
7.53 + address = {Coimbra, Portugal},
7.54 + month = {July 7-11},
7.55 + note = {\url{http://ceur-ws.org/Vol-1186/paper-17.pdf}}
7.56 +}
7.57 +@Article{flip-class-meta,
7.58 + author = {Shi, Y. and Ma, Y. and MacLeod, J. and others},
7.59 + title = {College students’ cognitive learning outcomes in flipped classroom instruction: a meta-analysis of the empirical literature},
7.60 + journal = {Journal of Computers in Education},
7.61 + year = {2019},
7.62 + pages = {1-25},
7.63 + month = {May},
7.64 + doi = {https://doi.org/10.1007/s40692-019-00142-8}
7.65 +}
7.66 +@inproceedings{krauss,
7.67 + author = {Krauss, Alexander},
7.68 + title = {Partial Recursive Functions in Higher-Order Logic},
7.69 + pages = {589-603},
7.70 + doi = {10.1007/11814771\_48},
7.71 + editor = {Ulrich Furbach and Natarajan Shankar},
7.72 + booktitle = {Automated Reasoning, Third International Joint Conference, IJCAR 2006},
7.73 + publisher = {Springer},
7.74 + series = {Lecture Notes in Computer Science},
7.75 + volume = {4130},
7.76 + year = {2006},
7.77 + bibsource = {DBLP, http://dblp.uni-trier.de}
7.78 +}
7.79 +@Manual{funpack-tutorial,
7.80 + title = {Defining Recursive Functions in {Isabelle/HOL}},
7.81 + author = {Alexander Krauss},
7.82 + address = {Munich},
7.83 + year = {},
7.84 + note = {{P}art of the Isabelle distribution},
7.85 + url = {\url{http://isabelle.in.tum.de/doc/functions.pdf}}
7.86 +}
7.87 +@Misc{nipkow-prog-prove-ny,
7.88 + author = {Nipkow, Tobias},
7.89 + title = {Programming and Proving in {Isabelle/HOL}},
7.90 + howpublished = {contained in the Isabelle distribution},
7.91 + year = {},
7.92 + url = {\url{http://isabelle.in.tum.de/doc/prog-prove.pdf}}
7.93 +}
7.94 +@Misc{code-gen-tutorial,
7.95 + author = {Florian Haftmann},
7.96 + title = {Code generation from {Isabelle/HOL} theories},
7.97 + howpublished = {Contained in the Isabelle distribution},
7.98 + year = {},
7.99 + url = {\url{http://isabelle.in.tum.de/doc/prog-prove.pdf}}
7.100 +}
7.101 +@Misc{implem-tutorial,
7.102 + author = {Makarius Wenzel},
7.103 + title = {The {Isabelle/Isar} Implementation},
7.104 + howpublished = {Contained in the Isabelle distribution},
7.105 + year = {},
7.106 + url = {\url{http://isabelle.in.tum.de/doc/implementation.pdf}}
7.107 +}
7.108 +@Misc{sledgehammer-tutorial,
7.109 + author = {Jasmin C.Blanchette},
7.110 + title = {{Hammering Away. A User's Guide to Sledgehammer for Isabelle/HOL}},
7.111 + howpublished = {contained in the Isabelle distribution},
7.112 + year = {},
7.113 + url = {\url{http://isabelle.in.tum.de/doc/sledgehammer.pdf}}
7.114 +}
7.115 +@incollection {haftm-nipkow-code-gen-HRS-10,
7.116 + author = {Haftmann, Florian and Nipkow, Tobias},
7.117 + affiliation = {Institut für Informatik, Technische Universität München},
7.118 + title = {Code Generation via Higher-Order Rewrite Systems},
7.119 + booktitle = {Functional and Logic Programming},
7.120 + series = {Lecture Notes in Computer Science},
7.121 + editor = {Blume, Matthias and Kobayashi, Naoki and Vidal, Germán},
7.122 + publisher = {Springer Berlin / Heidelberg},
7.123 + isbn = {978-3-642-12250-7},
7.124 + keyword = {Computer Science},
7.125 + pages = {103-117},
7.126 + volume = {6009},
7.127 + url = {http://dx.doi.org/10.1007/978-3-642-12251-4\_9},
7.128 + doi = {10.1007/978-3-642-12251-4\_9},
7.129 + year = {2010}
7.130 +}
7.131 +@misc{url-afp,
7.132 + title = {Archive of {F}ormal {P}roofs},
7.133 + howpublished = {\url{http://afp.sourceforge.net}}
7.134 +}
7.135 +@incollection {Cogent-to-C-2016,
7.136 + author = {S. Amani and A. Hixon and Z. Chen and C. Rizkallah and P. Chubb and L. O’Connor and
7.137 +J. Beeren and Y. Nagashima and J. Lim and T. Sewell and J. Tuong and G. Keller and T. Murray and
7.138 +G. Klein and G. Heiser},
7.139 + title = {Cogent: Verifying High-Assurance File System Implementations},
7.140 + booktitle = {International Conference on Architectural Support for Programming Languages and
7.141 +Operating Systems},
7.142 + publisher = {Springer Berlin / Heidelberg},
7.143 + address = {Atlanta, GA, USA},
7.144 + pages = {175-188},
7.145 + doi = {10.1145/2872362.2872404},
7.146 + year = {2016}
7.147 +}
7.148 +@InProceedings{wn:proto-sys,
7.149 + author = {Krempler, Alan and Neuper, Walther},
7.150 + year = {2018},
7.151 + title = {Prototyping ``Systems that Explain Themselves'' for Education},
7.152 + editor = {Quaresma, Pedro and Neuper, Walther},
7.153 + booktitle = {{\rm Proceedings 6th International Workshop on}
7.154 + Theorem proving components for Educational software,
7.155 + {\rm Gothenburg, Sweden, 6 Aug 2017}},
7.156 + series = {Electronic Proceedings in Theoretical Computer Science},
7.157 + volume = {267},
7.158 + publisher = {Open Publishing Association},
7.159 + pages = {89-107},
7.160 + doi = {10.4204/EPTCS.267.6}
7.161 +}
7.162 +@Book{Isa-tutor08,
7.163 + author = {Nipkow, Tobias and Paulson, Lawrence C. and Wenzel, Markus},
7.164 + title = {Isabelle/HOL, a proof assistant for high-order logic},
7.165 + publisher = {Springer Verlag},
7.166 + year = {2008}
7.167 +}
7.168 +@InCollection{pl:formal-lang-hist,
7.169 + author = {Lucas, Peter},
7.170 + title = {On the Formalization of Programming Languages: Early History and Main Approaches},
7.171 + booktitle = {The Vienna Development Method: The Meta-Language},
7.172 + publisher = {Springer},
7.173 + year = {1978},
7.174 + editor = {D. Bj{\o}rner and C. B. Jones},
7.175 + volume = {16},
7.176 + series = {LNCS},
7.177 + doi = {10.1007/3-540-08766-4\_8}
7.178 +}
7.179 +@InProceedings{thedu16:lucin-user-view,
7.180 + author = {Neuper, Walther},
7.181 + title = {Lucas-Interpretation from Users' Perspective},
7.182 + booktitle = {Joint Proceedings of the FM4M, MathUI, and ThEdu Workshops, Doctoral Program,
7.183 +and Work in Progress at the Conference on Intelligent Computer Mathematics},
7.184 + year = {2016},
7.185 + address = {Bialystok, Poland},
7.186 + month = {July 25-29},
7.187 + pages = {83-89},
7.188 + note = {\url{http://cicm-conference.org/2016/ceur-ws/CICM2016-WIP.pdf}}
7.189 +}
7.190 +@Misc{wn:lucin-thedu18,
7.191 + author = {Walther Neuper},
7.192 + title = {Lucas-Interpretation from Programmers' Perspective},
7.193 + year = {2018},
7.194 + note = {Abstract for ThEdu'18 \url{http://www.ist.tugraz.at/projects/isac/publ/lucin-prog-view.pdf}}
7.195 +}
7.196 +@InProceedings{wn:lucas-interp-12,
7.197 + author = "Neuper, Walther",
7.198 + year = "2012",
7.199 + title = "Automated Generation of User Guidance by Combining Computation and Deduction",
7.200 + pages = "82-101",
7.201 + doi = "10.4204/EPTCS.79.5",
7.202 + booktitle = {Electronic Proceedings in Theoretical Computer Science},
7.203 + editor = "Quaresma, Pedro and Back, Ralph-Johan",
7.204 + volume = "79",
7.205 + publisher = "Open Publishing Association"
7.206 +}
7.207 +@Book{progr-mathematica-2012,
7.208 + author = {Maeder, Roman E.},
7.209 + title = {Programming in Mathematica},
7.210 + publisher = {Addison-Wesley},
7.211 + address = {Reading, Mass.},
7.212 + year = {2012},
7.213 + edition = {3rd}
7.214 +}
7.215 +@PhdThesis{wn:diss,
7.216 + author = {Neuper, Walther },
7.217 + title = {Reactive User-Guidance by an Autonomous Engine Doing High-School Math},
7.218 + school = {IICM - Inst. f. Softwaretechnology},
7.219 + year = {2001},
7.220 + address = {Technical University, A-8010 Graz},
7.221 + note = {\url{http://www.ist.tugraz.at/projects/isac/publ/wn-diss.ps.gz}}
7.222 +}
7.223 +@Article{plmms10,
7.224 + author = {Florian Haftmann and Cezary Kaliszyk and Walther Neuper},
7.225 + title = {{CTP}-based programming languages~? {C}onsiderations about an experimental design},
7.226 + journal = {ACM Communications in Computer Algebra},
7.227 + doi = {10.1145/1838599.1838621},
7.228 + year = {2010},
7.229 + volume = {44},
7.230 + number = {1/2},
7.231 + pages = {27-41},
7.232 + month = {March/June}
7.233 +}
7.234 +@Article{back-SD-2010,
7.235 + author = {R.-J. Back},
7.236 + title = {Structured derivations: a unified proof style for teaching mathematics},
7.237 + journal = {Formal Aspects of Computing},
7.238 + year = {2010},
7.239 + volume = {22},
7.240 + number = {5},
7.241 + pages = {629-661}
7.242 +}
7.243 +@MastersThesis{mlehnf:bakk-11,
7.244 + author = {Mathias Lehnfeld},
7.245 + title = {Verbindung von 'Computation' und 'Deduction' im \sisac-System},
7.246 + school = {Institut f\"ur Computersprachen, Technische Universit\"at Wien},
7.247 + year = {2011},
7.248 + note = {Bakkalaureate project}
7.249 +}
7.250 +@incollection{paulson700,
7.251 + author = {Lawrence C. Paulson},
7.252 + title = {{Isabelle}: The Next 700 Theorem Provers},
7.253 + booktitle = {Logic and Computer Science},
7.254 + editor = {P. Odifreddi},
7.255 + pages = {361-386},
7.256 + publisher = {Academic Press},
7.257 + url = {https://arxiv.org/abs/cs/9301106},
7.258 + year = {1990}
7.259 +}
7.260 +@misc{RISC4777,
7.261 + author = {B. Buchberger},
7.262 + title = {{The Role of Mathematical Thinking for 21st Century Society}},
7.263 + language = {english},
7.264 + year = {2013},
7.265 + month = {March 4-6},
7.266 + annote = {2013-03-04-A},
7.267 + note = {Invited talk at The 2nd International Conference on Mathematics and Technology in Mathematics Education},
7.268 + institution = {Khemarak University, Phnom Penh, Cambodia},
7.269 + conferencename = {The 2nd International Conference on Mathematics and Technology in Mathematics Education}
7.270 +}
7.271 +@Article{EMS-math-ethics,
7.272 + author = {Chiodo, Maurice and Clifton, Toby},
7.273 + title = {The Importance of Ethics in Mathematics},
7.274 + journal = {Newsletter of the European Mathematical Society},
7.275 + year = {2019},
7.276 + volume = {114},
7.277 + pages = {34-37},
7.278 + month = {December},
7.279 + url = {\url{https://euro-math-soc.eu/newsletter}}
7.280 +}
7.281 +@MastersThesis{ggt02,
7.282 + author = {Karnel, Stefan},
7.283 + title = {Gr\"o{\ss}te gemeinsame Teiler in Polynomringen und Implementierung im \isac-Projekt},
7.284 + school = {University of Technology, Institute of Mathematics},
7.285 + year = {2002},
7.286 + address = {Graz, Austria},
7.287 + month = {Aug}
7.288 +}
7.289 +@InProceedings{gdaroczy-EP-13,
7.290 + author = {Gabriella Dar\'{o}czy and Walther Neuper},
7.291 + title = {Error-Patterns within ``Next-Step-Guidance'' in TP-based Educational Systems},
7.292 + booktitle = {eJMT, the Electronic Journal of Mathematics \& Technology},
7.293 + year = {2013},
7.294 + volume = {7},
7.295 + pages = {175-194},
7.296 + month = {February},
7.297 + note = {Special Issue ``TP-based Systems and Education''},
7.298 + url = {\url{https://php.radford.edu/~ejmt/ContentIndex.php\#v7n2}}
7.299 +}
7.300 +@TECHREPORT{tBaBoEr07a,
7.301 + author = {Back, Ralph-Johan and Bos, Victor and Eriksson, Johannes},
7.302 + title = {MathEdit: Tool Support for Structured Calculational Proofs},
7.303 + institution = {TUCS},
7.304 + year = {2007},
7.305 + number = {854},
7.306 + month = {Dec},
7.307 + note = {\url{http://tucs.fi/publications/view/?pub_id=tBaBoEr07a}}
7.308 +}
7.309 +@article{Farmer_al:93,
7.310 +author = {W. D. Farmer and J. D. Guttman and F. J. Thayer},
7.311 +title = {{IMPS: An Interactive Mathematical Proof System}},
7.312 +journal = {Journal of Automated Reasoning},
7.313 +year = {1993},
7.314 +volume = {11},
7.315 +month = {August},
7.316 +number = {2},
7.317 +pages = {213-248},
7.318 +}
7.319 +@InProceedings{gclc-06,
7.320 + author = {Jani\v{c}i\'c, Predrag},
7.321 + title = {{GCLC} --- a tool for constructive euclidean geometry and more than that},
7.322 + booktitle = {Mathematical Software -- {ICMS} 2006},
7.323 + pages = {58-73},
7.324 + year = {2006},
7.325 + number = {4151}
7.326 +}
7.327 +@Article{ggb:atp-15,
7.328 + author = {Botana, F. and Hohenwarter, M. and Jani\v{c}i\'c, P. and Kov\'acs, Z. and Petrovi\'c, I. and Recio, T. and Weitzhofer, S.},
7.329 + title = {Automated Theorem Proving in {GeoGebra}: Current Achievements},
7.330 + journal = {Journal of Automated Reasoning},
7.331 + year = {2015},
7.332 + volume = {55},
7.333 + number = {1},
7.334 + pages = {39-59},
7.335 + ISSN = {0168-7433},
7.336 + DOI = {http://dx.doi.org/10.1007/s10817-015-9326-4}
7.337 +}
7.338 +@Manual{isabelle-jedit,
7.339 + title = {{Isabelle/jEdit}},
7.340 + author = {Makarius Wenzel},
7.341 + address = {Munich},
7.342 + note = {Part of the Isabelle distribution},
7.343 + note = {\url{http://isabelle.in.tum.de/doc/jedit.pdf}}
7.344 +}
7.345 +@TechReport{Yacc-1975,
7.346 + author = {Johnson, Stephen C.},
7.347 + title = {Yacc: {Y}et {A}nother {C}ompiler-{C}ompiler},
7.348 + institution = {AT\&T Bell Laboratories},
7.349 + year = {1975},
7.350 + number = {32},
7.351 + address = {Murray Hill, New Jersey},
7.352 + note = {Retrieved 31 January 2020}
7.353 +}
7.354 +
8.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
8.2 +++ b/src/Tools/isac/Doc/Lucas_Interpreter/document/root.tex Wed Mar 11 15:25:52 2020 +0100
8.3 @@ -0,0 +1,75 @@
8.4 +% into "root.tex" as created by "isabelle mkdir"
8.5 +% code from "llncs/samplepaper.tex" is inserted
8.6 +
8.7 +\documentclass{article}
8.8 +\usepackage{isabelle,isabellesym}
8.9 +\usepackage{graphicx}
8.10 +%\usepackage{hyperref} %\url{...} don't use together with isabelle,isabellesym
8.11 +%\usepackage{breakurl} %\url{...} don't use together with isabelle,isabellesym
8.12 +%\renewcommand\UrlFont{\color{blue}\rmfamily} % ..recommended by llncs/samplepaper.tex
8.13 +% but isabelle says *** \UrlFont undefined.
8.14 +
8.15 +% further packages required for unusual symbols (see also
8.16 +% isabellesym.sty), use only when needed
8.17 +
8.18 +%\usepackage{amssymb}
8.19 + %for \<leadsto>, \<box>, \<diamond>, \<sqsupset>, \<mho>, \<Join>,
8.20 + %\<lhd>, \<lesssim>, \<greatersim>, \<lessapprox>, \<greaterapprox>,
8.21 + %\<triangleq>, \<yen>, \<lozenge>
8.22 +
8.23 +%\usepackage{eurosym}
8.24 + %for \<euro>
8.25 +
8.26 +%\usepackage[only,bigsqcap]{stmaryrd}
8.27 + %for \<Sqinter>
8.28 +
8.29 +%\usepackage{eufrak}
8.30 + %for \<AA> ... \<ZZ>, \<aa> ... \<zz> (also included in amssymb)
8.31 +
8.32 +%\usepackage{textcomp}
8.33 + %for \<onequarter>, \<onehalf>, \<threequarters>, \<degree>, \<cent>,
8.34 + %\<currency>
8.35 +
8.36 +% this should be the last package used
8.37 +\usepackage{pdfsetup}
8.38 +
8.39 +% urls in roman style, theory text in math-similar italics
8.40 +\urlstyle{rm}
8.41 +\isabellestyle{tt} %better readable than {it}
8.42 +
8.43 +% for uniform font size
8.44 +%\renewcommand{\isastyle}{\isastyleminor}
8.45 +
8.46 +\def\isac{${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$}
8.47 +\def\sisac{{\footnotesize${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$}}
8.48 +\def\LI{$\cal{LI}$}
8.49 +
8.50 +\begin{document}
8.51 +
8.52 +\title{Introduction to Lucas-Interpretation}
8.53 +\author{Walther Neuper}
8.54 +%\institute{Johannes Kepler University, Linz, Austria}
8.55 +\maketitle
8.56 +\vspace{2cm}
8.57 +\tableofcontents
8.58 +\newpage
8.59 +
8.60 +% sane default for proof documents
8.61 +\parindent 0pt\parskip 0.5ex
8.62 +
8.63 +% generated text of all theories
8.64 +\input{Lucas_Interpreter.tex} %*.tex created by isabelle build
8.65 +
8.66 +% optional bibliography
8.67 +\bibliographystyle{plain}
8.68 +% \bibliographystyle{splncs04}
8.69 +% splncs04 CAUSES ERROR
8.70 +% SEE ~/material/templates/llncs/README
8.71 +\bibliography{root}
8.72 +
8.73 +\end{document}
8.74 +
8.75 +%%% Local Variables:
8.76 +%%% mode: latex
8.77 +%%% TeX-master: t
8.78 +%%% End:
9.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
9.2 +++ b/src/Tools/isac/Doc/README Wed Mar 11 15:25:52 2020 +0100
9.3 @@ -0,0 +1,7 @@
9.4 +~~/src/Tools/isac/Doc/README
9.5 +
9.6 +pdflatex in ~~/src/Tools/isac/Doc/ by:
9.7 +/usr/local/isabisac/bin/isabelle build -D .
9.8 +
9.9 +In case nothing happens with the above command, go
9.10 +~/.isabelle/isabisac/heaps/polyml-5.8_x86_64_32-linux/log$ rm Lucas_Interpreter*
10.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
10.2 +++ b/src/Tools/isac/Doc/ROOT Wed Mar 11 15:25:52 2020 +0100
10.3 @@ -0,0 +1,16 @@
10.4 +session "Lucas_Interpreter" in "Lucas_Interpreter" = HOL +
10.5 + options [document = pdf, document_output = "output"]
10.6 + sessions
10.7 + "Interpret"
10.8 + theories
10.9 + "Lucas_Interpreter"
10.10 + document_files (in "../")
10.11 + "isabelle.sty"
10.12 + "isabellesym.sty"
10.13 + "pdfsetup.sty"
10.14 + document_files
10.15 + "bend-7-70-en.png"
10.16 + "fun-pack-biegelinie-2.png"
10.17 + "fun-pack-simplify.png"
10.18 + "root.bib"
10.19 + "root.tex"
11.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
11.2 +++ b/src/Tools/isac/Doc/comment.sty Wed Mar 11 15:25:52 2020 +0100
11.3 @@ -0,0 +1,278 @@
11.4 +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
11.5 +% Comment.sty version 3.6, October 1999
11.6 +%
11.7 +% Purpose:
11.8 +% selectively in/exclude pieces of text: the user can define new
11.9 +% comment versions, and each is controlled separately.
11.10 +% Special comments can be defined where the user specifies the
11.11 +% action that is to be taken with each comment line.
11.12 +%
11.13 +% Author
11.14 +% Victor Eijkhout
11.15 +% Department of Computer Science
11.16 +% University of Tennessee
11.17 +% 107 Ayres Hall
11.18 +% Knoxville TN 37996
11.19 +% USA
11.20 +%
11.21 +% victor@eijkhout.net
11.22 +%
11.23 +% This program is free software; you can redistribute it and/or
11.24 +% modify it under the terms of the GNU General Public License
11.25 +% as published by the Free Software Foundation; either version 2
11.26 +% of the License, or (at your option) any later version.
11.27 +%
11.28 +% This program is distributed in the hope that it will be useful,
11.29 +% but WITHOUT ANY WARRANTY; without even the implied warranty of
11.30 +% MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
11.31 +% GNU General Public License for more details.
11.32 +%
11.33 +% For a copy of the GNU General Public License, write to the
11.34 +% Free Software Foundation, Inc.,
11.35 +% 59 Temple Place - Suite 330, Boston, MA 02111-1307, USA,
11.36 +% or find it on the net, for instance at
11.37 +% http://www.gnu.org/copyleft/gpl.html
11.38 +%
11.39 +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
11.40 +% This style can be used with plain TeX or LaTeX, and probably
11.41 +% most other packages too.
11.42 +%
11.43 +% Usage: all text included between
11.44 +% \comment ... \endcomment
11.45 +% or \begin{comment} ... \end{comment}
11.46 +% is discarded.
11.47 +%
11.48 +% The opening and closing commands should appear on a line
11.49 +% of their own. No starting spaces, nothing after it.
11.50 +% This environment should work with arbitrary amounts
11.51 +% of comment, and the comment can be arbitrary text.
11.52 +%
11.53 +% Other `comment' environments are defined by
11.54 +% and are selected/deselected with
11.55 +% \includecomment{versiona}
11.56 +% \excludecoment{versionb}
11.57 +%
11.58 +% These environments are used as
11.59 +% \versiona ... \endversiona
11.60 +% or \begin{versiona} ... \end{versiona}
11.61 +% with the opening and closing commands again on a line of
11.62 +% their own.
11.63 +%
11.64 +% LaTeX users note: for an included comment, the
11.65 +% \begin and \end lines act as if they don't exist.
11.66 +% In particular, they don't imply grouping, so assignments
11.67 +% &c are not local.
11.68 +%
11.69 +% Special comments are defined as
11.70 +% \specialcomment{name}{before commands}{after commands}
11.71 +% where the second and third arguments are executed before
11.72 +% and after each comment block. You can use this for global
11.73 +% formatting commands.
11.74 +% To keep definitions &c local, you can include \begingroup
11.75 +% in the `before commands' and \endgroup in the `after commands'.
11.76 +% ex:
11.77 +% \specialcomment{smalltt}
11.78 +% {\begingroup\ttfamily\footnotesize}{\endgroup}
11.79 +% You do *not* have to do an additional
11.80 +% \includecomment{smalltt}
11.81 +% To remove 'smalltt' blocks, give \excludecomment{smalltt}
11.82 +% after the definition.
11.83 +%
11.84 +% Processing comments can apply processing to each line.
11.85 +% \processcomment{name}{each-line commands}%
11.86 +% {before commands}{after commands}
11.87 +% By defining a control sequence
11.88 +% \def\Thiscomment##1{...} in the before commands the user can
11.89 +% specify what is to be done with each comment line.
11.90 +% BUG this does not work quite yet BUG
11.91 +%
11.92 +% Trick for short in/exclude macros (such as \maybe{this snippet}):
11.93 +%\includecomment{cond}
11.94 +%\newcommand{\maybe}[1]{}
11.95 +%\begin{cond}
11.96 +%\renewcommand{\maybe}[1]{#1}
11.97 +%\end{cond}
11.98 +%
11.99 +% Basic approach of the implementation:
11.100 +% to comment something out, scoop up every line in verbatim mode
11.101 +% as macro argument, then throw it away.
11.102 +% For inclusions, in LaTeX the block is written out to
11.103 +% a file \CommentCutFile (default "comment.cut"), which is
11.104 +% then included.
11.105 +% In plain TeX (and other formats) both the opening and
11.106 +% closing comands are defined as noop.
11.107 +%
11.108 +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
11.109 +% Changes in version 3.1
11.110 +% - updated author's address
11.111 +% - cleaned up some code
11.112 +% - trailing contents on \begin{env} line is always discarded
11.113 +% even if you've done \includecomment{env}
11.114 +% - comments no longer define grouping!! you can even
11.115 +% \includecomment{env}
11.116 +% \begin{env}
11.117 +% \begin{itemize}
11.118 +% \end{env}
11.119 +% Isn't that something ...
11.120 +% - included comments are written to file and input again.
11.121 +% Changes in 3.2
11.122 +% - \specialcomment brought up to date (thanks to Ivo Welch).
11.123 +% Changes in 3.3
11.124 +% - updated author's address again
11.125 +% - parametrised \CommentCutFile
11.126 +% Changes in 3.4
11.127 +% - added GNU public license
11.128 +% - added \processcomment, because Ivo's fix (above) brought an
11.129 +% inconsistency to light.
11.130 +% Changes in 3.5
11.131 +% - corrected typo in header.
11.132 +% - changed author email
11.133 +% - corrected \specialcomment yet again.
11.134 +% - fixed excludecomment of an earlier defined environment.
11.135 +% Changes in 3.6
11.136 +% - The 'cut' file is now written more verbatim, using \meaning;
11.137 +% some people reported having trouble with ISO latin 1, or umlaute.sty.
11.138 +% - removed some \newif statements.
11.139 +% Has this suddenly become \outer again?
11.140 +%
11.141 +% Known bugs:
11.142 +% - excludecomment leads to one superfluous space
11.143 +% - processcomment leads to a superfluous line break
11.144 +%
11.145 +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
11.146 +
11.147 +\def\makeinnocent#1{\catcode`#1=12 }
11.148 +\def\csarg#1#2{\expandafter#1\csname#2\endcsname}
11.149 +\def\latexname{lplain}\def\latexename{LaTeX2e}
11.150 +\newwrite\CommentStream
11.151 +\def\CommentCutFile{comment.cut}
11.152 +
11.153 +\def\ProcessComment#1% start it all of
11.154 + {\begingroup
11.155 + \def\CurrentComment{#1}%
11.156 + \let\do\makeinnocent \dospecials
11.157 + \makeinnocent\^^L% and whatever other special cases
11.158 + \endlinechar`\^^M \catcode`\^^M=12 \xComment}
11.159 +%\def\ProcessCommentWithArg#1#2% to be used in \leveledcomment
11.160 +% {\begingroup
11.161 +% \def\CurrentComment{#1}%
11.162 +% \let\do\makeinnocent \dospecials
11.163 +% \makeinnocent\^^L% and whatever other special cases
11.164 +% \endlinechar`\^^M \catcode`\^^M=12 \xComment}
11.165 +{\catcode`\^^M=12 \endlinechar=-1 %
11.166 + \gdef\xComment#1^^M{%
11.167 + \expandafter\ProcessCommentLine}
11.168 + \gdef\ProcessCommentLine#1^^M{\def\test{#1}
11.169 + \csarg\ifx{End\CurrentComment Test}\test
11.170 + \edef\next{\noexpand\EndOfComment{\CurrentComment}}%
11.171 + \else \ThisComment{#1}\let\next\ProcessCommentLine
11.172 + \fi \next}
11.173 +}
11.174 +
11.175 +\def\CSstringmeaning#1{\expandafter\CSgobblearrow\meaning#1}
11.176 +\def\CSstringcsnoescape#1{\expandafter\CSgobbleescape\string#1}
11.177 +{\escapechar-1
11.178 +\expandafter\expandafter\expandafter\gdef
11.179 + \expandafter\expandafter\expandafter\CSgobblearrow
11.180 + \expandafter\string\csname macro:->\endcsname{}
11.181 +}
11.182 +\def\CSgobbleescape#1{\ifnum`\\=`#1 \else #1\fi}
11.183 +\def\WriteCommentLine#1{\def\CStmp{#1}%
11.184 + \immediate\write\CommentStream{\CSstringmeaning\CStmp}}
11.185 +
11.186 +% 3.1 change: in LaTeX and LaTeX2e prevent grouping
11.187 +\if 0%
11.188 +\ifx\fmtname\latexename
11.189 + 0%
11.190 +\else \ifx\fmtname\latexname
11.191 + 0%
11.192 + \else
11.193 + 1%
11.194 +\fi \fi
11.195 +%%%%
11.196 +%%%% definitions for LaTeX
11.197 +%%%%
11.198 +\def\AfterIncludedComment
11.199 + {\immediate\closeout\CommentStream
11.200 + \input{\CommentCutFile}\relax
11.201 + }%
11.202 +\def\TossComment{\immediate\closeout\CommentStream}
11.203 +\def\BeforeIncludedComment
11.204 + {\immediate\openout\CommentStream=\CommentCutFile
11.205 + \let\ThisComment\WriteCommentLine}
11.206 +\def\includecomment
11.207 + #1{\message{Include comment '#1'}%
11.208 + \csarg\let{After#1Comment}\AfterIncludedComment
11.209 + \csarg\def{#1}{\BeforeIncludedComment
11.210 + \ProcessComment{#1}}%
11.211 + \CommentEndDef{#1}}
11.212 +\long\def\specialcomment
11.213 + #1#2#3{\message{Special comment '#1'}%
11.214 + % note: \AfterIncludedComment does \input, so #2 goes here!
11.215 + \csarg\def{After#1Comment}{#2\AfterIncludedComment#3}%
11.216 + \csarg\def{#1}{\BeforeIncludedComment\relax
11.217 + \ProcessComment{#1}}%
11.218 + \CommentEndDef{#1}}
11.219 +\long\def\processcomment
11.220 + #1#2#3#4{\message{Lines-Processing comment '#1'}%
11.221 + \csarg\def{After#1Comment}{#3\AfterIncludedComment#4}%
11.222 + \csarg\def{#1}{\BeforeIncludedComment#2\relax
11.223 + \ProcessComment{#1}}%
11.224 + \CommentEndDef{#1}}
11.225 +\def\leveledcomment
11.226 + #1#2{\message{Include comment '#1' up to level '#2'}%
11.227 + %\csname #1IsLeveledCommenttrue\endcsname
11.228 + \csarg\let{After#1Comment}\AfterIncludedComment
11.229 + \csarg\def{#1}{\BeforeIncludedComment
11.230 + \ProcessCommentWithArg{#1}}%
11.231 + \CommentEndDef{#1}}
11.232 +\else
11.233 +%%%%
11.234 +%%%%plain TeX and other formats
11.235 +%%%%
11.236 +\def\includecomment
11.237 + #1{\message{Including comment '#1'}%
11.238 + \csarg\def{#1}{}%
11.239 + \csarg\def{end#1}{}}
11.240 +\long\def\specialcomment
11.241 + #1#2#3{\message{Special comment '#1'}%
11.242 + \csarg\def{#1}{\def\ThisComment{}\def\AfterComment{#3}#2%
11.243 + \ProcessComment{#1}}%
11.244 + \CommentEndDef{#1}}
11.245 +\fi
11.246 +
11.247 +%%%%
11.248 +%%%% general definition of skipped comment
11.249 +%%%%
11.250 +\def\excludecomment
11.251 + #1{\message{Excluding comment '#1'}%
11.252 + \csarg\def{#1}{\let\AfterComment\relax
11.253 + \def\ThisComment####1{}\ProcessComment{#1}}%
11.254 + \csarg\let{After#1Comment}\TossComment
11.255 + \CommentEndDef{#1}}
11.256 +
11.257 +\if 0%
11.258 +\ifx\fmtname\latexename
11.259 + 0%
11.260 +\else \ifx\fmtname\latexname
11.261 + 0%
11.262 + \else
11.263 + 1%
11.264 +\fi \fi
11.265 +% latex & latex2e:
11.266 +\def\EndOfComment#1{\endgroup\end{#1}%
11.267 + \csname After#1Comment\endcsname}
11.268 +\def\CommentEndDef#1{{\escapechar=-1\relax
11.269 + \csarg\xdef{End#1Test}{\string\\end\string\{#1\string\}}%
11.270 + }}
11.271 +\else
11.272 +% plain & other
11.273 +\def\EndOfComment#1{\endgroup\AfterComment}
11.274 +\def\CommentEndDef#1{{\escapechar=-1\relax
11.275 + \csarg\xdef{End#1Test}{\string\\end#1}%
11.276 + }}
11.277 +\fi
11.278 +
11.279 +\excludecomment{comment}
11.280 +
11.281 +\endinput
12.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
12.2 +++ b/src/Tools/isac/Doc/isabelle.sty Wed Mar 11 15:25:52 2020 +0100
12.3 @@ -0,0 +1,269 @@
12.4 +%%
12.5 +%% macros for Isabelle generated LaTeX output
12.6 +%%
12.7 +
12.8 +%%% Simple document preparation (based on theory token language and symbols)
12.9 +
12.10 +% isabelle environments
12.11 +
12.12 +\newcommand{\isabellecontext}{UNKNOWN}
12.13 +\newcommand{\setisabellecontext}[1]{\def\isabellecontext{#1}}
12.14 +
12.15 +\newcommand{\isastyle}{\UNDEF}
12.16 +\newcommand{\isastylett}{\UNDEF}
12.17 +\newcommand{\isastyleminor}{\UNDEF}
12.18 +\newcommand{\isastyleminortt}{\UNDEF}
12.19 +\newcommand{\isastylescript}{\UNDEF}
12.20 +\newcommand{\isastyletext}{\normalsize\normalfont\rmfamily}
12.21 +\newcommand{\isastyletxt}{\normalfont\rmfamily}
12.22 +\newcommand{\isastylecmt}{\normalfont\rmfamily}
12.23 +
12.24 +\newcommand{\isaspacing}{%
12.25 + \sfcode 42 1000 % .
12.26 + \sfcode 63 1000 % ?
12.27 + \sfcode 33 1000 % !
12.28 + \sfcode 58 1000 % :
12.29 + \sfcode 59 1000 % ;
12.30 + \sfcode 44 1000 % ,
12.31 +}
12.32 +
12.33 +%symbol markup -- \emph achieves decent spacing via italic corrections
12.34 +\newcommand{\isamath}[1]{\emph{$#1$}}
12.35 +\newcommand{\isatext}[1]{\emph{#1}}
12.36 +\DeclareRobustCommand{\isascriptstyle}{\def\isamath##1{##1}\def\isatext##1{\mbox{\isaspacing\isastylescript##1}}}
12.37 +\newcommand{\isactrlsub}[1]{\emph{\isascriptstyle${}\sb{#1}$}}
12.38 +\newcommand{\isactrlsup}[1]{\emph{\isascriptstyle${}\sp{#1}$}}
12.39 +\DeclareRobustCommand{\isactrlbsub}{\emph\bgroup\math{}\sb\bgroup\mbox\bgroup\isaspacing\isastylescript}
12.40 +\DeclareRobustCommand{\isactrlesub}{\egroup\egroup\endmath\egroup}
12.41 +\DeclareRobustCommand{\isactrlbsup}{\emph\bgroup\math{}\sp\bgroup\mbox\bgroup\isaspacing\isastylescript}
12.42 +\DeclareRobustCommand{\isactrlesup}{\egroup\egroup\endmath\egroup}
12.43 +\newcommand{\isactrlbold}[1]{{\bfseries\upshape\boldmath#1}}
12.44 +
12.45 +\newenvironment{isaantiq}{{\isacharat\isacharbraceleft}}{{\isacharbraceright}}
12.46 +
12.47 +\newdimen\isa@parindent\newdimen\isa@parskip
12.48 +
12.49 +\newenvironment{isabellebody}{%
12.50 +\isamarkuptrue\par%
12.51 +\isa@parindent\parindent\parindent0pt%
12.52 +\isa@parskip\parskip\parskip0pt%
12.53 +\isaspacing\isastyle}{\par}
12.54 +
12.55 +\newenvironment{isabellebodytt}{%
12.56 +\isamarkuptrue\par%
12.57 +\isa@parindent\parindent\parindent0pt%
12.58 +\isa@parskip\parskip\parskip0pt%
12.59 +\isaspacing\isastylett}{\par}
12.60 +
12.61 +\newenvironment{isabelle}
12.62 +{\begin{trivlist}\begin{isabellebody}\item\relax}
12.63 +{\end{isabellebody}\end{trivlist}}
12.64 +
12.65 +\newenvironment{isabellett}
12.66 +{\begin{trivlist}\begin{isabellebodytt}\item\relax}
12.67 +{\end{isabellebodytt}\end{trivlist}}
12.68 +
12.69 +\newcommand{\isa}[1]{\emph{\isaspacing\isastyleminor #1}}
12.70 +\newcommand{\isatt}[1]{\emph{\isaspacing\isastyleminortt #1}}
12.71 +
12.72 +\newcommand{\isaindent}[1]{\hphantom{#1}}
12.73 +\newcommand{\isanewline}{\mbox{}\par\mbox{}}
12.74 +\newcommand{\isasep}{}
12.75 +\newcommand{\isadigit}[1]{#1}
12.76 +
12.77 +\newcommand{\isachardefaults}{%
12.78 +\def\isacharbell{\isamath{\bigbox}}%requires stmaryrd
12.79 +\chardef\isacharbang=`\!%
12.80 +\chardef\isachardoublequote=`\"%
12.81 +\chardef\isachardoublequoteopen=`\"%
12.82 +\chardef\isachardoublequoteclose=`\"%
12.83 +\chardef\isacharhash=`\#%
12.84 +\chardef\isachardollar=`\$%
12.85 +\chardef\isacharpercent=`\%%
12.86 +\chardef\isacharampersand=`\&%
12.87 +\chardef\isacharprime=`\'%
12.88 +\chardef\isacharparenleft=`\(%
12.89 +\chardef\isacharparenright=`\)%
12.90 +\chardef\isacharasterisk=`\*%
12.91 +\chardef\isacharplus=`\+%
12.92 +\chardef\isacharcomma=`\,%
12.93 +\chardef\isacharminus=`\-%
12.94 +\chardef\isachardot=`\.%
12.95 +\chardef\isacharslash=`\/%
12.96 +\chardef\isacharcolon=`\:%
12.97 +\chardef\isacharsemicolon=`\;%
12.98 +\chardef\isacharless=`\<%
12.99 +\chardef\isacharequal=`\=%
12.100 +\chardef\isachargreater=`\>%
12.101 +\chardef\isacharquery=`\?%
12.102 +\chardef\isacharat=`\@%
12.103 +\chardef\isacharbrackleft=`\[%
12.104 +\chardef\isacharbackslash=`\\%
12.105 +\chardef\isacharbrackright=`\]%
12.106 +\chardef\isacharcircum=`\^%
12.107 +\chardef\isacharunderscore=`\_%
12.108 +\def\isacharunderscorekeyword{\_}%
12.109 +\chardef\isacharbackquote=`\`%
12.110 +\chardef\isacharbackquoteopen=`\`%
12.111 +\chardef\isacharbackquoteclose=`\`%
12.112 +\chardef\isacharbraceleft=`\{%
12.113 +\chardef\isacharbar=`\|%
12.114 +\chardef\isacharbraceright=`\}%
12.115 +\chardef\isachartilde=`\~%
12.116 +\def\isacharverbatimopen{\isacharbraceleft\isacharasterisk}%
12.117 +\def\isacharverbatimclose{\isacharasterisk\isacharbraceright}%
12.118 +\def\isacartoucheopen{\isatext{\raise.3ex\hbox{$\scriptscriptstyle\langle$}}}%
12.119 +\def\isacartoucheclose{\isatext{\raise.3ex\hbox{$\scriptscriptstyle\rangle$}}}%
12.120 +}
12.121 +
12.122 +
12.123 +% keyword and section markup
12.124 +
12.125 +\newcommand{\isakeyword}[1]
12.126 +{\emph{\normalfont\bfseries\def\isachardot{.}\def\isacharunderscore{\isacharunderscorekeyword}%
12.127 +\def\isacharbraceleft{\{}\def\isacharbraceright{\}}#1}}
12.128 +\newcommand{\isacommand}[1]{\isakeyword{#1}}
12.129 +
12.130 +\newcommand{\isakeywordcontrol}[1]
12.131 +{\emph{\normalfont\bfseries\itshape\def\isacharunderscore{\isacharunderscorekeyword}#1\,}}
12.132 +
12.133 +\newcommand{\isamarkupchapter}[1]{\chapter{#1}}
12.134 +\newcommand{\isamarkupsection}[1]{\section{#1}}
12.135 +\newcommand{\isamarkupsubsection}[1]{\subsection{#1}}
12.136 +\newcommand{\isamarkupsubsubsection}[1]{\subsubsection{#1}}
12.137 +\newcommand{\isamarkupparagraph}[1]{\paragraph{#1}}
12.138 +\newcommand{\isamarkupsubparagraph}[1]{\subparagraph{#1}}
12.139 +
12.140 +\newif\ifisamarkup
12.141 +\newcommand{\isabeginpar}{\par\ifisamarkup\relax\else\medskip\fi}
12.142 +\newcommand{\isaendpar}{\par\medskip}
12.143 +\newenvironment{isapar}{\parindent\isa@parindent\parskip\isa@parskip\isabeginpar}{\isaendpar}
12.144 +\newenvironment{isamarkuptext}{\par\isastyletext\begin{isapar}}{\end{isapar}}
12.145 +\newenvironment{isamarkuptxt}{\par\isastyletxt\begin{isapar}}{\end{isapar}}
12.146 +\newcommand{\isamarkupcmt}[1]{{\isastylecmt--- #1}}
12.147 +
12.148 +
12.149 +% styles
12.150 +
12.151 +\def\isabellestyle#1{\csname isabellestyle#1\endcsname}
12.152 +
12.153 +\newcommand{\isabellestyledefault}{%
12.154 +\def\isastyle{\small\normalfont\ttfamily\slshape}%
12.155 +\def\isastylett{\small\normalfont\ttfamily}%
12.156 +\def\isastyleminor{\small\normalfont\ttfamily\slshape}%
12.157 +\def\isastyleminortt{\small\normalfont\ttfamily}%
12.158 +\def\isastylescript{\footnotesize\normalfont\ttfamily\slshape}%
12.159 +\isachardefaults%
12.160 +}
12.161 +\isabellestyledefault
12.162 +
12.163 +\newcommand{\isabellestylett}{%
12.164 +\def\isastyle{\small\normalfont\ttfamily}%
12.165 +\def\isastylett{\small\normalfont\ttfamily}%
12.166 +\def\isastyleminor{\small\normalfont\ttfamily}%
12.167 +\def\isastyleminortt{\small\normalfont\ttfamily}%
12.168 +\def\isastylescript{\footnotesize\normalfont\ttfamily}%
12.169 +\isachardefaults%
12.170 +}
12.171 +
12.172 +\newcommand{\isabellestyleit}{%
12.173 +\def\isastyle{\small\normalfont\itshape}%
12.174 +\def\isastylett{\small\normalfont\ttfamily}%
12.175 +\def\isastyleminor{\normalfont\itshape}%
12.176 +\def\isastyleminortt{\normalfont\ttfamily}%
12.177 +\def\isastylescript{\footnotesize\normalfont\itshape}%
12.178 +\isachardefaults%
12.179 +\def\isacharunderscorekeyword{\mbox{-}}%
12.180 +\def\isacharbang{\isamath{!}}%
12.181 +\def\isachardoublequote{}%
12.182 +\def\isachardoublequoteopen{}%
12.183 +\def\isachardoublequoteclose{}%
12.184 +\def\isacharhash{\isamath{\#}}%
12.185 +\def\isachardollar{\isamath{\$}}%
12.186 +\def\isacharpercent{\isamath{\%}}%
12.187 +\def\isacharampersand{\isamath{\&}}%
12.188 +\def\isacharprime{\isamath{\mskip2mu{'}\mskip-2mu}}%
12.189 +\def\isacharparenleft{\isamath{(}}%
12.190 +\def\isacharparenright{\isamath{)}}%
12.191 +\def\isacharasterisk{\isamath{*}}%
12.192 +\def\isacharplus{\isamath{+}}%
12.193 +\def\isacharcomma{\isamath{\mathord,}}%
12.194 +\def\isacharminus{\isamath{-}}%
12.195 +\def\isachardot{\isamath{\mathord.}}%
12.196 +\def\isacharslash{\isamath{/}}%
12.197 +\def\isacharcolon{\isamath{\mathord:}}%
12.198 +\def\isacharsemicolon{\isamath{\mathord;}}%
12.199 +\def\isacharless{\isamath{<}}%
12.200 +\def\isacharequal{\isamath{=}}%
12.201 +\def\isachargreater{\isamath{>}}%
12.202 +\def\isacharat{\isamath{@}}%
12.203 +\def\isacharbrackleft{\isamath{[}}%
12.204 +\def\isacharbackslash{\isamath{\backslash}}%
12.205 +\def\isacharbrackright{\isamath{]}}%
12.206 +\def\isacharunderscore{\mbox{-}}%
12.207 +\def\isacharbraceleft{\isamath{\{}}%
12.208 +\def\isacharbar{\isamath{\mid}}%
12.209 +\def\isacharbraceright{\isamath{\}}}%
12.210 +\def\isachartilde{\isamath{{}\sp{\sim}}}%
12.211 +\def\isacharbackquoteopen{\isatext{\raise.3ex\hbox{$\scriptscriptstyle\langle$}}}%
12.212 +\def\isacharbackquoteclose{\isatext{\raise.3ex\hbox{$\scriptscriptstyle\rangle$}}}%
12.213 +\def\isacharverbatimopen{\isamath{\langle\!\langle}}%
12.214 +\def\isacharverbatimclose{\isamath{\rangle\!\rangle}}%
12.215 +}
12.216 +
12.217 +\newcommand{\isabellestyleliteral}{%
12.218 +\isabellestyleit%
12.219 +\def\isacharunderscore{\_}%
12.220 +\def\isacharunderscorekeyword{\_}%
12.221 +\chardef\isacharbackquoteopen=`\`%
12.222 +\chardef\isacharbackquoteclose=`\`%
12.223 +}
12.224 +
12.225 +\newcommand{\isabellestyleliteralunderscore}{%
12.226 +\isabellestyleliteral%
12.227 +\def\isacharunderscore{\textunderscore}%
12.228 +\def\isacharunderscorekeyword{\textunderscore}%
12.229 +}
12.230 +
12.231 +\newcommand{\isabellestylesl}{%
12.232 +\isabellestyleit%
12.233 +\def\isastyle{\small\normalfont\slshape}%
12.234 +\def\isastylett{\small\normalfont\ttfamily}%
12.235 +\def\isastyleminor{\normalfont\slshape}%
12.236 +\def\isastyleminortt{\normalfont\ttfamily}%
12.237 +\def\isastylescript{\footnotesize\normalfont\slshape}%
12.238 +}
12.239 +
12.240 +
12.241 +% cancel text
12.242 +
12.243 +\usepackage[normalem]{ulem}
12.244 +\newcommand{\isamarkupcancel}[1]{\isa{\xout{#1}}}
12.245 +
12.246 +
12.247 +% tagged regions
12.248 +
12.249 +%plain TeX version of comment package -- much faster!
12.250 +\let\isafmtname\fmtname\def\fmtname{plain}
12.251 +\usepackage{comment}
12.252 +\let\fmtname\isafmtname
12.253 +
12.254 +\newcommand{\isafold}[1]{\emph{$\langle\mathord{\mathit{#1}}\rangle$}}
12.255 +
12.256 +\newcommand{\isakeeptag}[1]%
12.257 +{\includecomment{isadelim#1}\includecomment{isatag#1}\csarg\def{isafold#1}{}}
12.258 +\newcommand{\isadroptag}[1]%
12.259 +{\excludecomment{isadelim#1}\excludecomment{isatag#1}\csarg\def{isafold#1}{}}
12.260 +\newcommand{\isafoldtag}[1]%
12.261 +{\includecomment{isadelim#1}\excludecomment{isatag#1}\csarg\def{isafold#1}{\isafold{#1}}}
12.262 +
12.263 +\isakeeptag{document}
12.264 +\isakeeptag{theory}
12.265 +\isakeeptag{proof}
12.266 +\isakeeptag{ML}
12.267 +\isakeeptag{visible}
12.268 +\isadroptag{invisible}
12.269 +\isakeeptag{important}
12.270 +\isakeeptag{unimportant}
12.271 +
12.272 +\IfFileExists{isabelletags.sty}{\usepackage{isabelletags}}{}
13.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
13.2 +++ b/src/Tools/isac/Doc/isabellesym.sty Wed Mar 11 15:25:52 2020 +0100
13.3 @@ -0,0 +1,417 @@
13.4 +%%
13.5 +%% definitions of standard Isabelle symbols
13.6 +%%
13.7 +
13.8 +\newcommand{\isasymzero}{\isamath{\mathbf{0}}} %requires amssymb
13.9 +\newcommand{\isasymone}{\isamath{\mathbf{1}}} %requires amssymb
13.10 +\newcommand{\isasymtwo}{\isamath{\mathbf{2}}} %requires amssymb
13.11 +\newcommand{\isasymthree}{\isamath{\mathbf{3}}} %requires amssymb
13.12 +\newcommand{\isasymfour}{\isamath{\mathbf{4}}} %requires amssymb
13.13 +\newcommand{\isasymfive}{\isamath{\mathbf{5}}} %requires amssymb
13.14 +\newcommand{\isasymsix}{\isamath{\mathbf{6}}} %requires amssymb
13.15 +\newcommand{\isasymseven}{\isamath{\mathbf{7}}} %requires amssymb
13.16 +\newcommand{\isasymeight}{\isamath{\mathbf{8}}} %requires amssymb
13.17 +\newcommand{\isasymnine}{\isamath{\mathbf{9}}} %requires amssymb
13.18 +\newcommand{\isasymA}{\isamath{\mathcal{A}}}
13.19 +\newcommand{\isasymB}{\isamath{\mathcal{B}}}
13.20 +\newcommand{\isasymC}{\isamath{\mathcal{C}}}
13.21 +\newcommand{\isasymD}{\isamath{\mathcal{D}}}
13.22 +\newcommand{\isasymE}{\isamath{\mathcal{E}}}
13.23 +\newcommand{\isasymF}{\isamath{\mathcal{F}}}
13.24 +\newcommand{\isasymG}{\isamath{\mathcal{G}}}
13.25 +\newcommand{\isasymH}{\isamath{\mathcal{H}}}
13.26 +\newcommand{\isasymI}{\isamath{\mathcal{I}}}
13.27 +\newcommand{\isasymJ}{\isamath{\mathcal{J}}}
13.28 +\newcommand{\isasymK}{\isamath{\mathcal{K}}}
13.29 +\newcommand{\isasymL}{\isamath{\mathcal{L}}}
13.30 +\newcommand{\isasymM}{\isamath{\mathcal{M}}}
13.31 +\newcommand{\isasymN}{\isamath{\mathcal{N}}}
13.32 +\newcommand{\isasymO}{\isamath{\mathcal{O}}}
13.33 +\newcommand{\isasymP}{\isamath{\mathcal{P}}}
13.34 +\newcommand{\isasymQ}{\isamath{\mathcal{Q}}}
13.35 +\newcommand{\isasymR}{\isamath{\mathcal{R}}}
13.36 +\newcommand{\isasymS}{\isamath{\mathcal{S}}}
13.37 +\newcommand{\isasymT}{\isamath{\mathcal{T}}}
13.38 +\newcommand{\isasymU}{\isamath{\mathcal{U}}}
13.39 +\newcommand{\isasymV}{\isamath{\mathcal{V}}}
13.40 +\newcommand{\isasymW}{\isamath{\mathcal{W}}}
13.41 +\newcommand{\isasymX}{\isamath{\mathcal{X}}}
13.42 +\newcommand{\isasymY}{\isamath{\mathcal{Y}}}
13.43 +\newcommand{\isasymZ}{\isamath{\mathcal{Z}}}
13.44 +\newcommand{\isasyma}{\isamath{\mathrm{a}}}
13.45 +\newcommand{\isasymb}{\isamath{\mathrm{b}}}
13.46 +\newcommand{\isasymc}{\isamath{\mathrm{c}}}
13.47 +\newcommand{\isasymd}{\isamath{\mathrm{d}}}
13.48 +\newcommand{\isasyme}{\isamath{\mathrm{e}}}
13.49 +\newcommand{\isasymf}{\isamath{\mathrm{f}}}
13.50 +\newcommand{\isasymg}{\isamath{\mathrm{g}}}
13.51 +\newcommand{\isasymh}{\isamath{\mathrm{h}}}
13.52 +\newcommand{\isasymi}{\isamath{\mathrm{i}}}
13.53 +\newcommand{\isasymj}{\isamath{\mathrm{j}}}
13.54 +\newcommand{\isasymk}{\isamath{\mathrm{k}}}
13.55 +\newcommand{\isasyml}{\isamath{\mathrm{l}}}
13.56 +\newcommand{\isasymm}{\isamath{\mathrm{m}}}
13.57 +\newcommand{\isasymn}{\isamath{\mathrm{n}}}
13.58 +\newcommand{\isasymo}{\isamath{\mathrm{o}}}
13.59 +\newcommand{\isasymp}{\isamath{\mathrm{p}}}
13.60 +\newcommand{\isasymq}{\isamath{\mathrm{q}}}
13.61 +\newcommand{\isasymr}{\isamath{\mathrm{r}}}
13.62 +\newcommand{\isasyms}{\isamath{\mathrm{s}}}
13.63 +\newcommand{\isasymt}{\isamath{\mathrm{t}}}
13.64 +\newcommand{\isasymu}{\isamath{\mathrm{u}}}
13.65 +\newcommand{\isasymv}{\isamath{\mathrm{v}}}
13.66 +\newcommand{\isasymw}{\isamath{\mathrm{w}}}
13.67 +\newcommand{\isasymx}{\isamath{\mathrm{x}}}
13.68 +\newcommand{\isasymy}{\isamath{\mathrm{y}}}
13.69 +\newcommand{\isasymz}{\isamath{\mathrm{z}}}
13.70 +\newcommand{\isasymAA}{\isamath{\mathfrak{A}}} %requires eufrak
13.71 +\newcommand{\isasymBB}{\isamath{\mathfrak{B}}} %requires eufrak
13.72 +\newcommand{\isasymCC}{\isamath{\mathfrak{C}}} %requires eufrak
13.73 +\newcommand{\isasymDD}{\isamath{\mathfrak{D}}} %requires eufrak
13.74 +\newcommand{\isasymEE}{\isamath{\mathfrak{E}}} %requires eufrak
13.75 +\newcommand{\isasymFF}{\isamath{\mathfrak{F}}} %requires eufrak
13.76 +\newcommand{\isasymGG}{\isamath{\mathfrak{G}}} %requires eufrak
13.77 +\newcommand{\isasymHH}{\isamath{\mathfrak{H}}} %requires eufrak
13.78 +\newcommand{\isasymII}{\isamath{\mathfrak{I}}} %requires eufrak
13.79 +\newcommand{\isasymJJ}{\isamath{\mathfrak{J}}} %requires eufrak
13.80 +\newcommand{\isasymKK}{\isamath{\mathfrak{K}}} %requires eufrak
13.81 +\newcommand{\isasymLL}{\isamath{\mathfrak{L}}} %requires eufrak
13.82 +\newcommand{\isasymMM}{\isamath{\mathfrak{M}}} %requires eufrak
13.83 +\newcommand{\isasymNN}{\isamath{\mathfrak{N}}} %requires eufrak
13.84 +\newcommand{\isasymOO}{\isamath{\mathfrak{O}}} %requires eufrak
13.85 +\newcommand{\isasymPP}{\isamath{\mathfrak{P}}} %requires eufrak
13.86 +\newcommand{\isasymQQ}{\isamath{\mathfrak{Q}}} %requires eufrak
13.87 +\newcommand{\isasymRR}{\isamath{\mathfrak{R}}} %requires eufrak
13.88 +\newcommand{\isasymSS}{\isamath{\mathfrak{S}}} %requires eufrak
13.89 +\newcommand{\isasymTT}{\isamath{\mathfrak{T}}} %requires eufrak
13.90 +\newcommand{\isasymUU}{\isamath{\mathfrak{U}}} %requires eufrak
13.91 +\newcommand{\isasymVV}{\isamath{\mathfrak{V}}} %requires eufrak
13.92 +\newcommand{\isasymWW}{\isamath{\mathfrak{W}}} %requires eufrak
13.93 +\newcommand{\isasymXX}{\isamath{\mathfrak{X}}} %requires eufrak
13.94 +\newcommand{\isasymYY}{\isamath{\mathfrak{Y}}} %requires eufrak
13.95 +\newcommand{\isasymZZ}{\isamath{\mathfrak{Z}}} %requires eufrak
13.96 +\newcommand{\isasymaa}{\isamath{\mathfrak{a}}} %requires eufrak
13.97 +\newcommand{\isasymbb}{\isamath{\mathfrak{b}}} %requires eufrak
13.98 +\newcommand{\isasymcc}{\isamath{\mathfrak{c}}} %requires eufrak
13.99 +\newcommand{\isasymdd}{\isamath{\mathfrak{d}}} %requires eufrak
13.100 +\newcommand{\isasymee}{\isamath{\mathfrak{e}}} %requires eufrak
13.101 +\newcommand{\isasymff}{\isamath{\mathfrak{f}}} %requires eufrak
13.102 +\newcommand{\isasymgg}{\isamath{\mathfrak{g}}} %requires eufrak
13.103 +\newcommand{\isasymhh}{\isamath{\mathfrak{h}}} %requires eufrak
13.104 +\newcommand{\isasymii}{\isamath{\mathfrak{i}}} %requires eufrak
13.105 +\newcommand{\isasymjj}{\isamath{\mathfrak{j}}} %requires eufrak
13.106 +\newcommand{\isasymkk}{\isamath{\mathfrak{k}}} %requires eufrak
13.107 +\newcommand{\isasymll}{\isamath{\mathfrak{l}}} %requires eufrak
13.108 +\newcommand{\isasymmm}{\isamath{\mathfrak{m}}} %requires eufrak
13.109 +\newcommand{\isasymnn}{\isamath{\mathfrak{n}}} %requires eufrak
13.110 +\newcommand{\isasymoo}{\isamath{\mathfrak{o}}} %requires eufrak
13.111 +\newcommand{\isasympp}{\isamath{\mathfrak{p}}} %requires eufrak
13.112 +\newcommand{\isasymqq}{\isamath{\mathfrak{q}}} %requires eufrak
13.113 +\newcommand{\isasymrr}{\isamath{\mathfrak{r}}} %requires eufrak
13.114 +\newcommand{\isasymss}{\isamath{\mathfrak{s}}} %requires eufrak
13.115 +\newcommand{\isasymtt}{\isamath{\mathfrak{t}}} %requires eufrak
13.116 +\newcommand{\isasymuu}{\isamath{\mathfrak{u}}} %requires eufrak
13.117 +\newcommand{\isasymvv}{\isamath{\mathfrak{v}}} %requires eufrak
13.118 +\newcommand{\isasymww}{\isamath{\mathfrak{w}}} %requires eufrak
13.119 +\newcommand{\isasymxx}{\isamath{\mathfrak{x}}} %requires eufrak
13.120 +\newcommand{\isasymyy}{\isamath{\mathfrak{y}}} %requires eufrak
13.121 +\newcommand{\isasymzz}{\isamath{\mathfrak{z}}} %requires eufrak
13.122 +\newcommand{\isasymalpha}{\isamath{\alpha}}
13.123 +\newcommand{\isasymbeta}{\isamath{\beta}}
13.124 +\newcommand{\isasymgamma}{\isamath{\gamma}}
13.125 +\newcommand{\isasymdelta}{\isamath{\delta}}
13.126 +\newcommand{\isasymepsilon}{\isamath{\varepsilon}}
13.127 +\newcommand{\isasymzeta}{\isamath{\zeta}}
13.128 +\newcommand{\isasymeta}{\isamath{\eta}}
13.129 +\newcommand{\isasymtheta}{\isamath{\vartheta}}
13.130 +\newcommand{\isasymiota}{\isamath{\iota}}
13.131 +\newcommand{\isasymkappa}{\isamath{\kappa}}
13.132 +\newcommand{\isasymlambda}{\isamath{\lambda}}
13.133 +\newcommand{\isasymmu}{\isamath{\mu}}
13.134 +\newcommand{\isasymnu}{\isamath{\nu}}
13.135 +\newcommand{\isasymxi}{\isamath{\xi}}
13.136 +\newcommand{\isasympi}{\isamath{\pi}}
13.137 +\newcommand{\isasymrho}{\isamath{\varrho}}
13.138 +\newcommand{\isasymsigma}{\isamath{\sigma}}
13.139 +\newcommand{\isasymtau}{\isamath{\tau}}
13.140 +\newcommand{\isasymupsilon}{\isamath{\upsilon}}
13.141 +\newcommand{\isasymphi}{\isamath{\varphi}}
13.142 +\newcommand{\isasymchi}{\isamath{\chi}}
13.143 +\newcommand{\isasympsi}{\isamath{\psi}}
13.144 +\newcommand{\isasymomega}{\isamath{\omega}}
13.145 +\newcommand{\isasymGamma}{\isamath{\Gamma}}
13.146 +\newcommand{\isasymDelta}{\isamath{\Delta}}
13.147 +\newcommand{\isasymTheta}{\isamath{\Theta}}
13.148 +\newcommand{\isasymLambda}{\isamath{\Lambda}}
13.149 +\newcommand{\isasymXi}{\isamath{\Xi}}
13.150 +\newcommand{\isasymPi}{\isamath{\Pi}}
13.151 +\newcommand{\isasymSigma}{\isamath{\Sigma}}
13.152 +\newcommand{\isasymUpsilon}{\isamath{\Upsilon}}
13.153 +\newcommand{\isasymPhi}{\isamath{\Phi}}
13.154 +\newcommand{\isasymPsi}{\isamath{\Psi}}
13.155 +\newcommand{\isasymOmega}{\isamath{\Omega}}
13.156 +\newcommand{\isasymbool}{\isamath{\mathrm{I}\mkern-3.8mu\mathrm{B}}}
13.157 +\newcommand{\isasymcomplex}{\isamath{\mathrm{C}\mkern-15mu{\phantom{\mathrm{t}}\vrule}\mkern9mu}}
13.158 +\newcommand{\isasymnat}{\isamath{\mathrm{I}\mkern-3.8mu\mathrm{N}}}
13.159 +\newcommand{\isasymrat}{\isamath{\mathrm{Q}\mkern-16mu{\phantom{\mathrm{t}}\vrule}\mkern10mu}}
13.160 +\newcommand{\isasymreal}{\isamath{\mathrm{I}\mkern-3.8mu\mathrm{R}}}
13.161 +\newcommand{\isasymint}{\isamath{\mathsf{Z}\mkern-7.5mu\mathsf{Z}}}
13.162 +\newcommand{\isasymleftarrow}{\isamath{\leftarrow}}
13.163 +\newcommand{\isasymrightarrow}{\isamath{\rightarrow}}
13.164 +\newcommand{\isasymlongleftarrow}{\isamath{\longleftarrow}}
13.165 +\newcommand{\isasymlongrightarrow}{\isamath{\longrightarrow}}
13.166 +\newcommand{\isasymlonglongleftarrow}{\isamath{\xleftarrow{\hphantom{AAA}}}} %requires amsmath
13.167 +\newcommand{\isasymlonglongrightarrow}{\isamath{\xrightarrow{\hphantom{AAA}}}} %requires amsmath
13.168 +\newcommand{\isasymlonglonglongleftarrow}{\isamath{\xleftarrow{\hphantom{AAAA}}}} %requires amsmath
13.169 +\newcommand{\isasymlonglonglongrightarrow}{\isamath{\xrightarrow{\hphantom{AAAA}}}} %requires amsmath
13.170 +\newcommand{\isasymLeftarrow}{\isamath{\Leftarrow}}
13.171 +\newcommand{\isasymRightarrow}{\isamath{\Rightarrow}}
13.172 +\newcommand{\isasymLongleftarrow}{\isamath{\Longleftarrow}}
13.173 +\newcommand{\isasymLongrightarrow}{\isamath{\Longrightarrow}}
13.174 +\newcommand{\isasymLleftarrow}{\isamath{\Lleftarrow}} %requires amssymb
13.175 +\newcommand{\isasymRrightarrow}{\isamath{\Rrightarrow}} %requires amssymb
13.176 +\newcommand{\isasymleftrightarrow}{\isamath{\leftrightarrow}}
13.177 +\newcommand{\isasymLeftrightarrow}{\isamath{\Leftrightarrow}}
13.178 +\newcommand{\isasymlongleftrightarrow}{\isamath{\longleftrightarrow}}
13.179 +\newcommand{\isasymLongleftrightarrow}{\isamath{\Longleftrightarrow}}
13.180 +\newcommand{\isasymmapsto}{\isamath{\mapsto}}
13.181 +\newcommand{\isasymlongmapsto}{\isamath{\longmapsto}}
13.182 +\newcommand{\isasymmidarrow}{\isamath{\relbar}}
13.183 +\newcommand{\isasymMidarrow}{\isamath{\Relbar}}
13.184 +\newcommand{\isasymhookleftarrow}{\isamath{\hookleftarrow}}
13.185 +\newcommand{\isasymhookrightarrow}{\isamath{\hookrightarrow}}
13.186 +\newcommand{\isasymleftharpoondown}{\isamath{\leftharpoondown}}
13.187 +\newcommand{\isasymrightharpoondown}{\isamath{\rightharpoondown}}
13.188 +\newcommand{\isasymleftharpoonup}{\isamath{\leftharpoonup}}
13.189 +\newcommand{\isasymrightharpoonup}{\isamath{\rightharpoonup}}
13.190 +\newcommand{\isasymrightleftharpoons}{\isamath{\rightleftharpoons}}
13.191 +\newcommand{\isasymleadsto}{\isamath{\leadsto}} %requires amssymb
13.192 +\newcommand{\isasymdownharpoonleft}{\isamath{\downharpoonleft}} %requires amssymb
13.193 +\newcommand{\isasymdownharpoonright}{\isamath{\downharpoonright}} %requires amssymb
13.194 +\newcommand{\isasymupharpoonleft}{\isamath{\upharpoonleft}} %requires amssymb
13.195 +\newcommand{\isasymupharpoonright}{\isamath{\upharpoonright}} %requires amssymb
13.196 +\newcommand{\isasymrestriction}{\isamath{\restriction}} %requires amssymb
13.197 +\newcommand{\isasymColon}{\isamath{\mathrel{::}}}
13.198 +\newcommand{\isasymup}{\isamath{\uparrow}}
13.199 +\newcommand{\isasymUp}{\isamath{\Uparrow}}
13.200 +\newcommand{\isasymdown}{\isamath{\downarrow}}
13.201 +\newcommand{\isasymDown}{\isamath{\Downarrow}}
13.202 +\newcommand{\isasymupdown}{\isamath{\updownarrow}}
13.203 +\newcommand{\isasymUpdown}{\isamath{\Updownarrow}}
13.204 +\newcommand{\isasymlangle}{\isamath{\langle}}
13.205 +\newcommand{\isasymrangle}{\isamath{\rangle}}
13.206 +\newcommand{\isasymlceil}{\isamath{\lceil}}
13.207 +\newcommand{\isasymrceil}{\isamath{\rceil}}
13.208 +\newcommand{\isasymlfloor}{\isamath{\lfloor}}
13.209 +\newcommand{\isasymrfloor}{\isamath{\rfloor}}
13.210 +\newcommand{\isasymlparr}{\isamath{\mathopen{(\mkern-3mu\mid}}}
13.211 +\newcommand{\isasymrparr}{\isamath{\mathclose{\mid\mkern-3mu)}}}
13.212 +\newcommand{\isasymlbrakk}{\isamath{\mathopen{\lbrack\mkern-3mu\lbrack}}}
13.213 +\newcommand{\isasymrbrakk}{\isamath{\mathclose{\rbrack\mkern-3mu\rbrack}}}
13.214 +\newcommand{\isasymlbrace}{\isamath{\mathopen{\lbrace\mkern-4.5mu\mid}}}
13.215 +\newcommand{\isasymrbrace}{\isamath{\mathclose{\mid\mkern-4.5mu\rbrace}}}
13.216 +\newcommand{\isasymguillemotleft}{\isatext{\flqq}} %requires babel
13.217 +\newcommand{\isasymguillemotright}{\isatext{\frqq}} %requires babel
13.218 +\newcommand{\isasymbottom}{\isamath{\bot}}
13.219 +\newcommand{\isasymtop}{\isamath{\top}}
13.220 +\newcommand{\isasymand}{\isamath{\wedge}}
13.221 +\newcommand{\isasymAnd}{\isamath{\bigwedge}}
13.222 +\newcommand{\isasymor}{\isamath{\vee}}
13.223 +\newcommand{\isasymOr}{\isamath{\bigvee}}
13.224 +\newcommand{\isasymforall}{\isamath{\forall\,}}
13.225 +\newcommand{\isasymexists}{\isamath{\exists\,}}
13.226 +\newcommand{\isasymnot}{\isamath{\neg}}
13.227 +\newcommand{\isasymnexists}{\isamath{\nexists\,}} %requires amssymb
13.228 +\newcommand{\isasymcircle}{\isamath{\ocircle}} %requires wasysym
13.229 +\newcommand{\isasymbox}{\isamath{\Box}} %requires amssymb
13.230 +\newcommand{\isasymdiamond}{\isamath{\Diamond}} %requires amssymb
13.231 +\newcommand{\isasymdiamondop}{\isamath{\diamond}}
13.232 +\newcommand{\isasymsurd}{\isamath{\surd}}
13.233 +\newcommand{\isasymturnstile}{\isamath{\vdash}}
13.234 +\newcommand{\isasymTurnstile}{\isamath{\models}}
13.235 +\newcommand{\isasymtturnstile}{\isamath{\vdash\!\!\!\vdash}}
13.236 +\newcommand{\isasymTTurnstile}{\isamath{\mid\!\models}}
13.237 +\newcommand{\isasymstileturn}{\isamath{\dashv}}
13.238 +\newcommand{\isasymle}{\isamath{\le}}
13.239 +\newcommand{\isasymge}{\isamath{\ge}}
13.240 +\newcommand{\isasymlless}{\isamath{\ll}}
13.241 +\newcommand{\isasymggreater}{\isamath{\gg}}
13.242 +\newcommand{\isasymlesssim}{\isamath{\lesssim}} %requires amssymb
13.243 +\newcommand{\isasymgreatersim}{\isamath{\gtrsim}} %requires amssymb
13.244 +\newcommand{\isasymlessapprox}{\isamath{\lessapprox}} %requires amssymb
13.245 +\newcommand{\isasymgreaterapprox}{\isamath{\gtrapprox}} %requires amssymb
13.246 +\newcommand{\isasymin}{\isamath{\in}}
13.247 +\newcommand{\isasymnotin}{\isamath{\notin}}
13.248 +\newcommand{\isasymsubset}{\isamath{\subset}}
13.249 +\newcommand{\isasymsupset}{\isamath{\supset}}
13.250 +\newcommand{\isasymsubseteq}{\isamath{\subseteq}}
13.251 +\newcommand{\isasymsupseteq}{\isamath{\supseteq}}
13.252 +\newcommand{\isasymsqsubset}{\isamath{\sqsubset}} %requires amssymb
13.253 +\newcommand{\isasymsqsupset}{\isamath{\sqsupset}} %requires amssymb
13.254 +\newcommand{\isasymsqsubseteq}{\isamath{\sqsubseteq}}
13.255 +\newcommand{\isasymsqsupseteq}{\isamath{\sqsupseteq}}
13.256 +\newcommand{\isasyminter}{\isamath{\cap}}
13.257 +\newcommand{\isasymInter}{\isamath{\bigcap\,}}
13.258 +\newcommand{\isasymunion}{\isamath{\cup}}
13.259 +\newcommand{\isasymUnion}{\isamath{\bigcup\,}}
13.260 +\newcommand{\isasymsqunion}{\isamath{\sqcup}}
13.261 +\newcommand{\isasymSqunion}{\isamath{\bigsqcup\,}}
13.262 +\newcommand{\isasymsqinter}{\isamath{\sqcap}}
13.263 +\newcommand{\isasymSqinter}{\isamath{\bigsqcap\,}} %requires stmaryrd
13.264 +\newcommand{\isasymsetminus}{\isamath{\setminus}}
13.265 +\newcommand{\isasympropto}{\isamath{\propto}}
13.266 +\newcommand{\isasymuplus}{\isamath{\uplus}}
13.267 +\newcommand{\isasymUplus}{\isamath{\biguplus\,}}
13.268 +\newcommand{\isasymnoteq}{\isamath{\not=}}
13.269 +\newcommand{\isasymsim}{\isamath{\sim}}
13.270 +\newcommand{\isasymdoteq}{\isamath{\doteq}}
13.271 +\newcommand{\isasymsimeq}{\isamath{\simeq}}
13.272 +\newcommand{\isasymapprox}{\isamath{\approx}}
13.273 +\newcommand{\isasymasymp}{\isamath{\asymp}}
13.274 +\newcommand{\isasymcong}{\isamath{\cong}}
13.275 +\newcommand{\isasymsmile}{\isamath{\smile}}
13.276 +\newcommand{\isasymequiv}{\isamath{\equiv}}
13.277 +\newcommand{\isasymfrown}{\isamath{\frown}}
13.278 +\newcommand{\isasymJoin}{\isamath{\Join}} %requires amssymb
13.279 +\newcommand{\isasymbowtie}{\isamath{\bowtie}}
13.280 +\newcommand{\isasymprec}{\isamath{\prec}}
13.281 +\newcommand{\isasymsucc}{\isamath{\succ}}
13.282 +\newcommand{\isasympreceq}{\isamath{\preceq}}
13.283 +\newcommand{\isasymsucceq}{\isamath{\succeq}}
13.284 +\newcommand{\isasymparallel}{\isamath{\parallel}}
13.285 +\newcommand{\isasymbar}{\isamath{\mid}}
13.286 +\newcommand{\isasymplusminus}{\isamath{\pm}}
13.287 +\newcommand{\isasymminusplus}{\isamath{\mp}}
13.288 +\newcommand{\isasymtimes}{\isamath{\times}}
13.289 +\newcommand{\isasymdiv}{\isamath{\div}}
13.290 +\newcommand{\isasymcdot}{\isamath{\cdot}}
13.291 +\newcommand{\isasymstar}{\isamath{\star}}
13.292 +\newcommand{\isasymbullet}{\boldmath\isamath{\mathchoice{\displaystyle{\cdot}}{\textstyle{\cdot}}{\scriptstyle{\bullet}}{\scriptscriptstyle{\bullet}}}}
13.293 +\newcommand{\isasymcirc}{\isamath{\circ}}
13.294 +\newcommand{\isasymdagger}{\isamath{\dagger}}
13.295 +\newcommand{\isasymddagger}{\isamath{\ddagger}}
13.296 +\newcommand{\isasymlhd}{\isamath{\lhd}} %requires amssymb
13.297 +\newcommand{\isasymrhd}{\isamath{\rhd}} %requires amssymb
13.298 +\newcommand{\isasymunlhd}{\isamath{\unlhd}} %requires amssymb
13.299 +\newcommand{\isasymunrhd}{\isamath{\unrhd}} %requires amssymb
13.300 +\newcommand{\isasymtriangleleft}{\isamath{\triangleleft}}
13.301 +\newcommand{\isasymtriangleright}{\isamath{\triangleright}}
13.302 +\newcommand{\isasymtriangle}{\isamath{\triangle}}
13.303 +\newcommand{\isasymtriangleq}{\isamath{\triangleq}} %requires amssymb
13.304 +\newcommand{\isasymoplus}{\isamath{\oplus}}
13.305 +\newcommand{\isasymOplus}{\isamath{\bigoplus\,}}
13.306 +\newcommand{\isasymotimes}{\isamath{\otimes}}
13.307 +\newcommand{\isasymOtimes}{\isamath{\bigotimes\,}}
13.308 +\newcommand{\isasymodot}{\isamath{\odot}}
13.309 +\newcommand{\isasymOdot}{\isamath{\bigodot\,}}
13.310 +\newcommand{\isasymominus}{\isamath{\ominus}}
13.311 +\newcommand{\isasymoslash}{\isamath{\oslash}}
13.312 +\newcommand{\isasymdots}{\isamath{\dots}}
13.313 +\newcommand{\isasymcdots}{\isamath{\cdots}}
13.314 +\newcommand{\isasymSum}{\isamath{\sum\,}}
13.315 +\newcommand{\isasymProd}{\isamath{\prod\,}}
13.316 +\newcommand{\isasymCoprod}{\isamath{\coprod\,}}
13.317 +\newcommand{\isasyminfinity}{\isamath{\infty}}
13.318 +\newcommand{\isasymintegral}{\isamath{\int\,}}
13.319 +\newcommand{\isasymointegral}{\isamath{\oint\,}}
13.320 +\newcommand{\isasymclubsuit}{\isamath{\clubsuit}}
13.321 +\newcommand{\isasymdiamondsuit}{\isamath{\diamondsuit}}
13.322 +\newcommand{\isasymheartsuit}{\isamath{\heartsuit}}
13.323 +\newcommand{\isasymspadesuit}{\isamath{\spadesuit}}
13.324 +\newcommand{\isasymaleph}{\isamath{\aleph}}
13.325 +\newcommand{\isasymemptyset}{\isamath{\emptyset}}
13.326 +\newcommand{\isasymnabla}{\isamath{\nabla}}
13.327 +\newcommand{\isasympartial}{\isamath{\partial}}
13.328 +\newcommand{\isasymRe}{\isamath{\Re}}
13.329 +\newcommand{\isasymIm}{\isamath{\Im}}
13.330 +\newcommand{\isasymflat}{\isamath{\flat}}
13.331 +\newcommand{\isasymnatural}{\isamath{\natural}}
13.332 +\newcommand{\isasymsharp}{\isamath{\sharp}}
13.333 +\newcommand{\isasymangle}{\isamath{\angle}}
13.334 +\newcommand{\isasymcopyright}{\isatext{\normalfont\rmfamily\copyright}}
13.335 +\newcommand{\isasymregistered}{\isatext{\normalfont\rmfamily\textregistered}}
13.336 +\newcommand{\isasyminverse}{\isamath{{}^{-1}}}
13.337 +\newcommand{\isasymonequarter}{\isatext{\normalfont\rmfamily\textonequarter}} %requires textcomp
13.338 +\newcommand{\isasymonehalf}{\isatext{\normalfont\rmfamily\textonehalf}} %requires textcomp
13.339 +\newcommand{\isasymthreequarters}{\isatext{\normalfont\rmfamily\textthreequarters}} %requires textcomp
13.340 +\newcommand{\isasymordfeminine}{\isatext{\normalfont\rmfamily\textordfeminine}}
13.341 +\newcommand{\isasymordmasculine}{\isatext{\normalfont\rmfamily\textordmasculine}}
13.342 +\newcommand{\isasymsection}{\isatext{\normalfont\rmfamily\S}}
13.343 +\newcommand{\isasymparagraph}{\isatext{\normalfont\rmfamily\P}}
13.344 +\newcommand{\isasymexclamdown}{\isatext{\normalfont\rmfamily\textexclamdown}}
13.345 +\newcommand{\isasymquestiondown}{\isatext{\normalfont\rmfamily\textquestiondown}}
13.346 +\newcommand{\isasymeuro}{\isatext{\euro}} %requires eurosym
13.347 +\newcommand{\isasympounds}{\isamath{\pounds}}
13.348 +\newcommand{\isasymyen}{\isatext{\yen}} %requires amssymb
13.349 +\newcommand{\isasymcent}{\isatext{\textcent}} %requires textcomp
13.350 +\newcommand{\isasymcurrency}{\isatext{\textcurrency}} %requires textcomp
13.351 +\newcommand{\isasymdegree}{\isatext{\normalfont\rmfamily\textdegree}} %requires textcomp
13.352 +\newcommand{\isasymhyphen}{\isatext{\normalfont\rmfamily-}}
13.353 +\newcommand{\isasymamalg}{\isamath{\amalg}}
13.354 +\newcommand{\isasymmho}{\isamath{\mho}} %requires amssymb
13.355 +\newcommand{\isasymlozenge}{\isamath{\lozenge}} %requires amssymb
13.356 +\newcommand{\isasymwp}{\isamath{\wp}}
13.357 +\newcommand{\isasymwrong}{\isamath{\wr}}
13.358 +\newcommand{\isasymacute}{\isatext{\'\relax}}
13.359 +\newcommand{\isasymindex}{\isatext{\i}}
13.360 +\newcommand{\isasymdieresis}{\isatext{\"\relax}}
13.361 +\newcommand{\isasymcedilla}{\isatext{\c\relax}}
13.362 +\newcommand{\isasymhungarumlaut}{\isatext{\H\relax}}
13.363 +\newcommand{\isasymsome}{\isamath{\epsilon\,}}
13.364 +\newcommand{\isasymbind}{\isamath{\mathbin{>\!\!\!>\mkern-6.7mu=}}}
13.365 +\newcommand{\isasymthen}{\isamath{\mathbin{>\!\!\!>}}}
13.366 +\newcommand{\isasymopen}{\isatext{\raise.3ex\hbox{$\scriptscriptstyle\langle$}}}
13.367 +\newcommand{\isasymclose}{\isatext{\raise.3ex\hbox{$\scriptscriptstyle\rangle$}}}
13.368 +\newcommand{\isasymhole}{\isatext{\normalfont\rmfamily\wasylozenge}} %requires wasysym
13.369 +\newcommand{\isasymnewline}{\isatext{\fbox{$\hookleftarrow$}}}
13.370 +\newcommand{\isasymcomment}{\isatext{\isastylecmt---}}
13.371 +\newcommand{\isasymproof}{\isamath{\,\langle\mathit{proof}\rangle}}
13.372 +
13.373 +\newcommand{\isactrlmarker}{\isatext{\ding{48}}} %requires pifont
13.374 +\newcommand{\isactrlassert}{\isakeywordcontrol{assert}}
13.375 +\newcommand{\isactrlcancel}{\isakeywordcontrol{cancel}}
13.376 +\newcommand{\isactrlbinding}{\isakeywordcontrol{binding}}
13.377 +\newcommand{\isactrlclass}{\isakeywordcontrol{class}}
13.378 +\newcommand{\isactrlclassUNDERSCOREsyntax}{\isakeywordcontrol{class{\isacharunderscore}syntax}}
13.379 +\newcommand{\isactrlcommandUNDERSCOREkeyword}{\isakeywordcontrol{command{\isacharunderscore}keyword}}
13.380 +\newcommand{\isactrlconst}{\isakeywordcontrol{const}}
13.381 +\newcommand{\isactrlconstUNDERSCOREabbrev}{\isakeywordcontrol{const{\isacharunderscore}abbrev}}
13.382 +\newcommand{\isactrlconstUNDERSCOREname}{\isakeywordcontrol{const{\isacharunderscore}name}}
13.383 +\newcommand{\isactrlconstUNDERSCOREsyntax}{\isakeywordcontrol{const{\isacharunderscore}syntax}}
13.384 +\newcommand{\isactrlcontext}{\isakeywordcontrol{context}}
13.385 +\newcommand{\isactrlcprop}{\isakeywordcontrol{cprop}}
13.386 +\newcommand{\isactrlcterm}{\isakeywordcontrol{cterm}}
13.387 +\newcommand{\isactrlctyp}{\isakeywordcontrol{ctyp}}
13.388 +\newcommand{\isactrldir}{\isakeywordcontrol{dir}}
13.389 +\newcommand{\isactrlfile}{\isakeywordcontrol{file}}
13.390 +\newcommand{\isactrlhere}{\isakeywordcontrol{here}}
13.391 +\newcommand{\isactrlkeyword}{\isakeywordcontrol{keyword}}
13.392 +\newcommand{\isactrllatex}{\isakeywordcontrol{latex}}
13.393 +\newcommand{\isactrllocale}{\isakeywordcontrol{locale}}
13.394 +\newcommand{\isactrlmakeUNDERSCOREstring}{\isakeywordcontrol{make{\isacharunderscore}string}}
13.395 +\newcommand{\isactrlmasterUNDERSCOREdir}{\isakeywordcontrol{master{\isacharunderscore}dir}}
13.396 +\newcommand{\isactrlmethod}{\isakeywordcontrol{method}}
13.397 +\newcommand{\isactrlnamedUNDERSCOREtheorems}{\isakeywordcontrol{named{\isacharunderscore}theorems}}
13.398 +\newcommand{\isactrlnonterminal}{\isakeywordcontrol{nonterminal}}
13.399 +\newcommand{\isactrlpath}{\isakeywordcontrol{path}}
13.400 +\newcommand{\isactrlpathUNDERSCOREbinding}{\isakeywordcontrol{path{\isacharunderscore}binding}}
13.401 +\newcommand{\isactrlplugin}{\isakeywordcontrol{plugin}}
13.402 +\newcommand{\isactrlprint}{\isakeywordcontrol{print}}
13.403 +\newcommand{\isactrlprop}{\isakeywordcontrol{prop}}
13.404 +\newcommand{\isactrlsimproc}{\isakeywordcontrol{simproc}}
13.405 +\newcommand{\isactrlsort}{\isakeywordcontrol{sort}}
13.406 +\newcommand{\isactrlsyntaxUNDERSCOREconst}{\isakeywordcontrol{syntax{\isacharunderscore}const}}
13.407 +\newcommand{\isactrlsystemUNDERSCOREoption}{\isakeywordcontrol{system{\isacharunderscore}option}}
13.408 +\newcommand{\isactrlterm}{\isakeywordcontrol{term}}
13.409 +\newcommand{\isactrltheory}{\isakeywordcontrol{theory}}
13.410 +\newcommand{\isactrltheoryUNDERSCOREcontext}{\isakeywordcontrol{theory{\isacharunderscore}context}}
13.411 +\newcommand{\isactrltyp}{\isakeywordcontrol{typ}}
13.412 +\newcommand{\isactrltypeUNDERSCOREabbrev}{\isakeywordcontrol{type{\isacharunderscore}abbrev}}
13.413 +\newcommand{\isactrltypeUNDERSCOREname}{\isakeywordcontrol{type{\isacharunderscore}name}}
13.414 +\newcommand{\isactrltypeUNDERSCOREsyntax}{\isakeywordcontrol{type{\isacharunderscore}syntax}}
13.415 +\newcommand{\isactrlundefined}{\isakeywordcontrol{undefined}}
13.416 +
13.417 +\newcommand{\isactrlcode}{\isakeywordcontrol{code}}
13.418 +\newcommand{\isactrlcomputation}{\isakeywordcontrol{computation}}
13.419 +\newcommand{\isactrlcomputationUNDERSCOREconv}{\isakeywordcontrol{computation{\isacharunderscore}conv}}
13.420 +\newcommand{\isactrlcomputationUNDERSCOREcheck}{\isakeywordcontrol{computation{\isacharunderscore}check}}
14.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
14.2 +++ b/src/Tools/isac/Doc/isabelletags.sty Wed Mar 11 15:25:52 2020 +0100
14.3 @@ -0,0 +1,1 @@
14.4 +
15.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
15.2 +++ b/src/Tools/isac/Doc/pdfsetup.sty Wed Mar 11 15:25:52 2020 +0100
15.3 @@ -0,0 +1,7 @@
15.4 +%%
15.5 +%% default hyperref setup (both for pdf and dvi output)
15.6 +%%
15.7 +
15.8 +\usepackage{color}
15.9 +\definecolor{linkcolor}{rgb}{0,0,0.5}
15.10 +\usepackage[colorlinks=true,linkcolor=linkcolor,citecolor=linkcolor,filecolor=linkcolor,urlcolor=linkcolor,pdfpagelabels]{hyperref}
16.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
16.2 +++ b/src/Tools/isac/Doc/railsetup.sty Wed Mar 11 15:25:52 2020 +0100
16.3 @@ -0,0 +1,1202 @@
16.4 +% rail.sty - style file to support railroad diagrams
16.5 +%
16.6 +% 09-Jul-90 L. Rooijakkers
16.7 +% 08-Oct-90 L. Rooijakkers fixed centering bug when \rail@tmpc<0.
16.8 +% 07-Feb-91 L. Rooijakkers added \railoptions command, indexing
16.9 +% 08-Feb-91 L. Rooijakkers minor fixes
16.10 +% 28-Jun-94 K. Barthelmann turned into LaTeX2e package
16.11 +% 08-Dec-96 K. Barthelmann replaced \@writefile
16.12 +% 13-Dec-96 K. Barthelmann cleanup
16.13 +% 22-Feb-98 K. Barthelmann fixed catcodes of special characters
16.14 +% 18-Apr-98 K. Barthelmann fixed \par handling
16.15 +% 19-May-98 J. Olsson Added new macros to support arrow heads.
16.16 +% 26-Jul-98 K. Barthelmann changed \par to output newlines
16.17 +% 02-May-11 M. Wenzel default setup for Isabelle
16.18 +%
16.19 +% This style file needs to be used in conjunction with the 'rail'
16.20 +% program. Running LaTeX as 'latex file' produces file.rai, which should be
16.21 +% processed by Rail with 'rail file'. This produces file.rao, which will
16.22 +% be picked up by LaTeX on the next 'latex file' run.
16.23 +%
16.24 +% LaTeX will warn if there is no file.rao or it's out of date.
16.25 +%
16.26 +% The macros in this file thus consist of two parts: those that read and
16.27 +% write the .rai and .rao files, and those that do the actual formatting
16.28 +% of the railroad diagrams.
16.29 +
16.30 +\NeedsTeXFormat{LaTeX2e}
16.31 +\ProvidesPackage{rail}[1998/05/19]
16.32 +
16.33 +% railroad diagram formatting parameters (user level)
16.34 +% all of these are copied into their internal versions by \railinit
16.35 +%
16.36 +% \railunit : \unitlength within railroad diagrams
16.37 +% \railextra : extra length at outside of diagram
16.38 +% \railboxheight : height of ovals and frames
16.39 +% \railboxskip : vertical space between lines
16.40 +% \railboxleft : space to the left of a box
16.41 +% \railboxright : space to the right of a box
16.42 +% \railovalspace : extra space around contents of oval
16.43 +% \railframespace : extra space around contents of frame
16.44 +% \railtextleft : space to the left of text
16.45 +% \railtextright : space to the right of text
16.46 +% \railtextup : space to lift text up
16.47 +% \railjoinsize : circle size of join/split arcs
16.48 +% \railjoinadjust : space to adjust join
16.49 +%
16.50 +% \railnamesep : separator between name and rule body
16.51 +
16.52 +\newlength\railunit
16.53 +\newlength\railextra
16.54 +\newlength\railboxheight
16.55 +\newlength\railboxskip
16.56 +\newlength\railboxleft
16.57 +\newlength\railboxright
16.58 +\newlength\railovalspace
16.59 +\newlength\railframespace
16.60 +\newlength\railtextleft
16.61 +\newlength\railtextright
16.62 +\newlength\railtextup
16.63 +\newlength\railjoinsize
16.64 +\newlength\railjoinadjust
16.65 +\newlength\railnamesep
16.66 +
16.67 +% initialize the parameters
16.68 +
16.69 +\setlength\railunit{1sp}
16.70 +\setlength\railextra{4ex}
16.71 +\setlength\railboxleft{1ex}
16.72 +\setlength\railboxright{1ex}
16.73 +\setlength\railovalspace{2ex}
16.74 +\setlength\railframespace{2ex}
16.75 +\setlength\railtextleft{1ex}
16.76 +\setlength\railtextright{1ex}
16.77 +\setlength\railjoinadjust{0pt}
16.78 +\setlength\railnamesep{1ex}
16.79 +
16.80 +\DeclareOption{10pt}{
16.81 + \setlength\railboxheight{16pt}
16.82 + \setlength\railboxskip{24pt}
16.83 + \setlength\railtextup{5pt}
16.84 + \setlength\railjoinsize{16pt}
16.85 +}
16.86 +\DeclareOption{11pt}{
16.87 + \setlength\railboxheight{16pt}
16.88 + \setlength\railboxskip{24pt}
16.89 + \setlength\railtextup{5pt}
16.90 + \setlength\railjoinsize{16pt}
16.91 +}
16.92 +\DeclareOption{12pt}{
16.93 + \setlength\railboxheight{20pt}
16.94 + \setlength\railboxskip{28pt}
16.95 + \setlength\railtextup{6pt}
16.96 + \setlength\railjoinsize{20pt}
16.97 +}
16.98 +
16.99 +\ExecuteOptions{10pt}
16.100 +\ProcessOptions
16.101 +
16.102 +% internal versions of the formatting parameters
16.103 +%
16.104 +% \rail@extra : \railextra
16.105 +% \rail@boxht : \railboxheight
16.106 +% \rail@boxsp : \railboxskip
16.107 +% \rail@boxlf : \railboxleft
16.108 +% \rail@boxrt : \railboxright
16.109 +% \rail@boxhht : \railboxheight / 2
16.110 +% \rail@ovalsp : \railovalspace
16.111 +% \rail@framesp : \railframespace
16.112 +% \rail@textlf : \railtextleft
16.113 +% \rail@textrt : \railtextright
16.114 +% \rail@textup : \railtextup
16.115 +% \rail@joinsz : \railjoinsize
16.116 +% \rail@joinhsz : \railjoinsize / 2
16.117 +% \rail@joinadj : \railjoinadjust
16.118 +%
16.119 +% \railinit : internalize all of the parameters.
16.120 +
16.121 +\newcount\rail@extra
16.122 +\newcount\rail@boxht
16.123 +\newcount\rail@boxsp
16.124 +\newcount\rail@boxlf
16.125 +\newcount\rail@boxrt
16.126 +\newcount\rail@boxhht
16.127 +\newcount\rail@ovalsp
16.128 +\newcount\rail@framesp
16.129 +\newcount\rail@textlf
16.130 +\newcount\rail@textrt
16.131 +\newcount\rail@textup
16.132 +\newcount\rail@joinsz
16.133 +\newcount\rail@joinhsz
16.134 +\newcount\rail@joinadj
16.135 +
16.136 +\newcommand\railinit{
16.137 +\rail@extra=\railextra
16.138 +\divide\rail@extra by \railunit
16.139 +\rail@boxht=\railboxheight
16.140 +\divide\rail@boxht by \railunit
16.141 +\rail@boxsp=\railboxskip
16.142 +\divide\rail@boxsp by \railunit
16.143 +\rail@boxlf=\railboxleft
16.144 +\divide\rail@boxlf by \railunit
16.145 +\rail@boxrt=\railboxright
16.146 +\divide\rail@boxrt by \railunit
16.147 +\rail@boxhht=\railboxheight
16.148 +\divide\rail@boxhht by \railunit
16.149 +\divide\rail@boxhht by 2
16.150 +\rail@ovalsp=\railovalspace
16.151 +\divide\rail@ovalsp by \railunit
16.152 +\rail@framesp=\railframespace
16.153 +\divide\rail@framesp by \railunit
16.154 +\rail@textlf=\railtextleft
16.155 +\divide\rail@textlf by \railunit
16.156 +\rail@textrt=\railtextright
16.157 +\divide\rail@textrt by \railunit
16.158 +\rail@textup=\railtextup
16.159 +\divide\rail@textup by \railunit
16.160 +\rail@joinsz=\railjoinsize
16.161 +\divide\rail@joinsz by \railunit
16.162 +\rail@joinhsz=\railjoinsize
16.163 +\divide\rail@joinhsz by \railunit
16.164 +\divide\rail@joinhsz by 2
16.165 +\rail@joinadj=\railjoinadjust
16.166 +\divide\rail@joinadj by \railunit
16.167 +}
16.168 +
16.169 +\AtBeginDocument{\railinit}
16.170 +
16.171 +% \rail@param : declarations for list environment
16.172 +%
16.173 +% \railparam{TEXT} : sets \rail@param to TEXT
16.174 +%
16.175 +% \rail@reserved : characters reserved for grammar
16.176 +
16.177 +\newcommand\railparam[1]{
16.178 +\def\rail@param{
16.179 + \setlength\leftmargin{0pt}\setlength\rightmargin{0pt}
16.180 + \setlength\labelwidth{0pt}\setlength\labelsep{0pt}
16.181 + \setlength\itemindent{0pt}\setlength\listparindent{0pt}
16.182 + #1
16.183 +}
16.184 +}
16.185 +\railparam{}
16.186 +
16.187 +\newtoks\rail@reserved
16.188 +\rail@reserved={:;|*+?[]()'"}
16.189 +
16.190 +% \rail@termfont : format setup for terminals
16.191 +%
16.192 +% \rail@nontfont : format setup for nonterminals
16.193 +%
16.194 +% \rail@annofont : format setup for annotations
16.195 +%
16.196 +% \rail@rulefont : format setup for rule names
16.197 +%
16.198 +% \rail@indexfont : format setup for index entry
16.199 +%
16.200 +% \railtermfont{TEXT} : set terminal format setup to TEXT
16.201 +%
16.202 +% \railnontermfont{TEXT} : set nonterminal format setup to TEXT
16.203 +%
16.204 +% \railannotatefont{TEXT} : set annotation format setup to TEXT
16.205 +%
16.206 +% \railnamefont{TEXT} : set rule name format setup to TEXT
16.207 +%
16.208 +% \railindexfont{TEXT} : set index entry format setup to TEXT
16.209 +
16.210 +\def\rail@termfont{\ttfamily\upshape}
16.211 +\def\rail@nontfont{\rmfamily\upshape}
16.212 +\def\rail@annofont{\rmfamily\itshape}
16.213 +\def\rail@namefont{\rmfamily\itshape}
16.214 +\def\rail@indexfont{\rmfamily\itshape}
16.215 +
16.216 +\newcommand\railtermfont[1]{
16.217 +\def\rail@termfont{#1}
16.218 +}
16.219 +
16.220 +\newcommand\railnontermfont[1]{
16.221 +\def\rail@nontfont{#1}
16.222 +}
16.223 +
16.224 +\newcommand\railannotatefont[1]{
16.225 +\def\rail@annofont{#1}
16.226 +}
16.227 +
16.228 +\newcommand\railnamefont[1]{
16.229 +\def\rail@namefont{#1}
16.230 +}
16.231 +
16.232 +\newcommand\railindexfont[1]{
16.233 +\def\rail@indexfont{#1}
16.234 +}
16.235 +
16.236 +% railroad read/write macros
16.237 +%
16.238 +% \begin{rail} TEXT \end{rail} : TEXT is written out to the .rai file,
16.239 +% as \rail@i{NR}{TEXT}. Then the matching
16.240 +% \rail@o{NR}{FMT} from the .rao file is
16.241 +% executed (if defined).
16.242 +%
16.243 +% \railoptions{OPTIONS} : OPTIONS are written out to the .rai file,
16.244 +% as \rail@p{OPTIONS}.
16.245 +%
16.246 +% \railterm{IDENT,IDENT,...} : format IDENT as terminals. writes out
16.247 +% \rail@t{IDENT} to the .rai file
16.248 +%
16.249 +% \railalias{IDENT}{TEXT} : format IDENT as TEXT. defines \rail@t@IDENT as
16.250 +% TEXT.
16.251 +%
16.252 +% \railtoken{IDENT}{TEXT} : abbreviates \railalias{IDENT}{TEXT}\railterm{IDENT}
16.253 +% (for backward compatibility)
16.254 +%
16.255 +% \rail@setcodes : guards special characters
16.256 +%
16.257 +% \rail@makeother{CHARACTER} : sets \catcode of CHARACTER to "other"
16.258 +% used inside a loop for \rail@setcodes
16.259 +%
16.260 +% \rail@nr : railroad diagram counter
16.261 +%
16.262 +% \ifrail@match : current \rail@i{NR}{TEXT} matches
16.263 +%
16.264 +% \rail@first : actions to be done first. read in .rao file,
16.265 +% open .rai file if \@filesw true, undefine \rail@first.
16.266 +% executed from \begin{rail}, \railoptions and \railterm.
16.267 +%
16.268 +% \rail@i{NR}{TEXT} : defines \rail@i@NR as TEXT. written to the .rai
16.269 +% file by \rail, read from the .rao file by
16.270 +% \rail@first
16.271 +%
16.272 +% \rail@t{IDENT} : tells Rail that IDENT is to be custom formatted,
16.273 +% written to the .rai file by \railterm.
16.274 +%
16.275 +% \rail@o{NR}{TEXT} : defines \rail@o@NR as TEXT, read from the .rao
16.276 +% file by \rail@first.
16.277 +%
16.278 +% \rail@p{OPTIONS} : pass options to rail, written to the .rai file by
16.279 +% \railoptions
16.280 +%
16.281 +% \rail@write{TEXT} : write TEXT to the .rai file
16.282 +%
16.283 +% \rail@warn : warn user for mismatching diagrams
16.284 +%
16.285 +% \rail@endwarn : either \relax or \rail@warn
16.286 +%
16.287 +% \ifrail@all : checked at the end of the document
16.288 +
16.289 +\def\rail@makeother#1{
16.290 + \expandafter\catcode\expandafter`\csname\string #1\endcsname=12
16.291 +}
16.292 +
16.293 +\def\rail@setcodes{
16.294 +\let\par=\relax
16.295 +\let\\=\relax
16.296 +\expandafter\@tfor\expandafter\rail@symbol\expandafter:\expandafter=%
16.297 + \the\rail@reserved
16.298 +\do{\expandafter\rail@makeother\rail@symbol}
16.299 +}
16.300 +
16.301 +\newcount\rail@nr
16.302 +
16.303 +\newif\ifrail@all
16.304 +\rail@alltrue
16.305 +
16.306 +\newif\ifrail@match
16.307 +
16.308 +\def\rail@first{
16.309 +\begingroup
16.310 +\makeatletter
16.311 +\rail@setcodes
16.312 +\InputIfFileExists{\jobname.rao}{}{\PackageInfo{rail}{No file \jobname.rao}}
16.313 +\makeatother
16.314 +\endgroup
16.315 +\if@filesw
16.316 +\newwrite\tf@rai
16.317 +\immediate\openout\tf@rai=\jobname.rai
16.318 +\fi
16.319 +\global\let\rail@first=\relax
16.320 +}
16.321 +
16.322 +\long\def\rail@body#1\end{
16.323 +{
16.324 +\newlinechar=`^^J
16.325 +\def\par{\string\par^^J}
16.326 +\rail@write{\string\rail@i{\number\rail@nr}{#1}}
16.327 +}
16.328 +\xdef\rail@i@{#1}
16.329 +\end
16.330 +}
16.331 +
16.332 +\newenvironment{rail}{
16.333 +\global\advance\rail@nr by 1
16.334 +\rail@first
16.335 +\begingroup
16.336 +\rail@setcodes
16.337 +\rail@body
16.338 +}{
16.339 +\endgroup
16.340 +\rail@matchtrue
16.341 +\@ifundefined{rail@o@\number\rail@nr}{\rail@matchfalse}{}
16.342 +\expandafter\ifx\csname rail@i@\number\rail@nr\endcsname\rail@i@
16.343 +\else
16.344 +\rail@matchfalse
16.345 +\fi
16.346 +\ifrail@match
16.347 +\csname rail@o@\number\rail@nr\endcsname
16.348 +\else
16.349 +\PackageWarning{rail}{Railroad diagram {\number\rail@nr} doesn't match}
16.350 +\global\let\rail@endwarn=\rail@warn
16.351 +\begin{list}{}{\rail@param}
16.352 +\rail@begin{1}{}
16.353 +\rail@setbox{\bfseries ???}
16.354 +\rail@oval
16.355 +\rail@end
16.356 +\end{list}
16.357 +\fi
16.358 +}
16.359 +
16.360 +\newcommand\railoptions[1]{
16.361 +\rail@first
16.362 +\rail@write{\string\rail@p{#1}}
16.363 +}
16.364 +
16.365 +\newcommand\railterm[1]{
16.366 +\rail@first
16.367 +\@for\rail@@:=#1\do{
16.368 +\rail@write{\string\rail@t{\rail@@}}
16.369 +}
16.370 +}
16.371 +
16.372 +\newcommand\railalias[2]{
16.373 +\expandafter\def\csname rail@t@#1\endcsname{#2}
16.374 +}
16.375 +
16.376 +\newcommand\railtoken[2]{\railalias{#1}{#2}\railterm{#1}}
16.377 +
16.378 +\long\def\rail@i#1#2{
16.379 +\expandafter\gdef\csname rail@i@#1\endcsname{#2}
16.380 +}
16.381 +
16.382 +\def\rail@o#1#2{
16.383 +\expandafter\gdef\csname rail@o@#1\endcsname{
16.384 +\begin{list}{}{\rail@param}
16.385 +#2
16.386 +\end{list}
16.387 +}
16.388 +}
16.389 +
16.390 +\def\rail@t#1{}
16.391 +
16.392 +\def\rail@p#1{}
16.393 +
16.394 +\long\def\rail@write#1{\@ifundefined{tf@rai}{}{\immediate\write\tf@rai{#1}}}
16.395 +
16.396 +\def\rail@warn{
16.397 +\PackageWarningNoLine{rail}{Railroad diagram(s) may have changed.
16.398 + Use 'rail' and rerun}
16.399 +}
16.400 +
16.401 +\let\rail@endwarn=\relax
16.402 +
16.403 +\AtEndDocument{\rail@endwarn}
16.404 +
16.405 +% index entry macro
16.406 +%
16.407 +% \rail@index{IDENT} : add index entry for IDENT
16.408 +
16.409 +\def\rail@index#1{
16.410 +\index{\rail@indexfont#1}
16.411 +}
16.412 +
16.413 +% railroad formatting primitives
16.414 +%
16.415 +% \rail@x : current x
16.416 +% \rail@y : current y
16.417 +% \rail@ex : current end x
16.418 +% \rail@sx : starting x for \rail@cr
16.419 +% \rail@rx : rightmost previous x for \rail@cr
16.420 +%
16.421 +% \rail@tmpa : temporary count
16.422 +% \rail@tmpb : temporary count
16.423 +% \rail@tmpc : temporary count
16.424 +%
16.425 +% \rail@put : put at (\rail@x,\rail@y)
16.426 +% \rail@vput : put vector at (\rail@x,\rail@y)
16.427 +%
16.428 +% \rail@eline : end line by drawing from \rail@ex to \rail@x
16.429 +%
16.430 +% \rail@vreline : end line by drawing a vector from \rail@x to \rail@ex
16.431 +%
16.432 +% \rail@vleline : end line by drawing a vector from \rail@ex to \rail@x
16.433 +%
16.434 +% \rail@sety{LEVEL} : set \rail@y to level LEVEL
16.435 +
16.436 +\newcount\rail@x
16.437 +\newcount\rail@y
16.438 +\newcount\rail@ex
16.439 +\newcount\rail@sx
16.440 +\newcount\rail@rx
16.441 +
16.442 +\newcount\rail@tmpa
16.443 +\newcount\rail@tmpb
16.444 +\newcount\rail@tmpc
16.445 +
16.446 +\def\rail@put{\put(\number\rail@x,\number\rail@y)}
16.447 +
16.448 +\def\rail@vput{\put(\number\rail@ex,\number\rail@y)}
16.449 +
16.450 +\def\rail@eline{
16.451 +\rail@tmpb=\rail@x
16.452 +\advance\rail@tmpb by -\rail@ex
16.453 +\rail@put{\line(-1,0){\number\rail@tmpb}}
16.454 +}
16.455 +
16.456 +\def\rail@vreline{
16.457 +\rail@tmpb=\rail@x
16.458 +\advance\rail@tmpb by -\rail@ex
16.459 +\rail@vput{\vector(1,0){\number\rail@tmpb}}
16.460 +}
16.461 +
16.462 +\def\rail@vleline{
16.463 +\rail@tmpb=\rail@x
16.464 +\advance\rail@tmpb by -\rail@ex
16.465 +\rail@put{\vector(-1,0){\number\rail@tmpb}}
16.466 +}
16.467 +
16.468 +\def\rail@sety#1{
16.469 +\rail@y=#1
16.470 +\multiply\rail@y by -\rail@boxsp
16.471 +\advance\rail@y by -\rail@boxht
16.472 +}
16.473 +
16.474 +% \rail@begin{HEIGHT}{NAME} : begin a railroad diagram of height HEIGHT
16.475 +%
16.476 +% \rail@end : end a railroad diagram
16.477 +%
16.478 +% \rail@expand{IDENT} : expand IDENT
16.479 +
16.480 +\def\rail@begin#1#2{
16.481 +\item
16.482 +\begin{minipage}[t]{\linewidth}
16.483 +\ifx\@empty#2\else
16.484 +{\rail@namefont \rail@expand{#2}}\\*[\railnamesep]
16.485 +\fi
16.486 +\unitlength=\railunit
16.487 +\rail@tmpa=#1
16.488 +\multiply\rail@tmpa by \rail@boxsp
16.489 +\begin{picture}(0,\number\rail@tmpa)(0,-\number\rail@tmpa)
16.490 +\rail@ex=0
16.491 +\rail@rx=0
16.492 +\rail@x=\rail@extra
16.493 +\rail@sx=\rail@x
16.494 +\rail@sety{0}
16.495 +}
16.496 +
16.497 +\def\rail@end{
16.498 +\advance\rail@x by \rail@extra
16.499 +\rail@eline
16.500 +\end{picture}
16.501 +\end{minipage}
16.502 +}
16.503 +
16.504 +\def\rail@vend{
16.505 +\advance\rail@x by \rail@extra
16.506 +\rail@vreline
16.507 +\end{picture}
16.508 +\end{minipage}
16.509 +}
16.510 +
16.511 +\def\rail@expand#1{\@ifundefined{rail@t@#1}{#1}{\csname rail@t@#1\endcsname}}
16.512 +
16.513 +% \rail@token{TEXT}[ANNOT] : format token TEXT with annotation
16.514 +% \rail@ltoken{TEXT}[ANNOT] : format token TEXT with annotation, arrow left
16.515 +% \rail@rtoken{TEXT}[ANNOT] : format token TEXT with annotation, arrow right
16.516 +%
16.517 +% \rail@ctoken{TEXT}[ANNOT] : format token TEXT centered with annotation
16.518 +% \rail@lctoken{TEXT}[ANNOT] : format token TEXT centered with annotation, arrow left
16.519 +% \rail@rctoken{TEXT}[ANNOT] : format token TEXT centered with annotation, arrow right
16.520 +%
16.521 +% \rail@nont{TEXT}[ANNOT] : format nonterminal TEXT with annotation
16.522 +% \rail@lnont{TEXT}[ANNOT] : format nonterminal TEXT with annotation, arrow left
16.523 +% \rail@rnont{TEXT}[ANNOT] : format nonterminal TEXT with annotation. arrow right
16.524 +%
16.525 +% \rail@cnont{TEXT}[ANNOT] : format nonterminal TEXT centered with annotation
16.526 +% \rail@lcnont{TEXT}[ANNOT] : format nonterminal TEXT centered with annotation,
16.527 +% arrow left
16.528 +% \rail@rcnont{TEXT}[ANNOT] : format nonterminal TEXT centered with annotation,
16.529 +% arrow right
16.530 +%
16.531 +% \rail@term{TEXT}[ANNOT] : format terminal TEXT with annotation
16.532 +% \rail@lterm{TEXT}[ANNOT] : format terminal TEXT with annotation, arrow left
16.533 +% \rail@rterm{TEXT}[ANNOT] : format terminal TEXT with annotation, arrow right
16.534 +%
16.535 +% \rail@cterm{TEXT}[ANNOT] : format terminal TEXT centered with annotation
16.536 +% \rail@lcterm{TEXT}[ANNOT] : format terminal TEXT centered with annotation, arrow left
16.537 +% \rail@rcterm{TEXT}[ANNOT] : format terminal TEXT centered with annotation,
16.538 +% arrow right
16.539 +%
16.540 +% \rail@annote[TEXT] : format TEXT as annotation
16.541 +
16.542 +\def\rail@token#1[#2]{
16.543 +\rail@setbox{%
16.544 +{\rail@termfont \rail@expand{#1}}\ifx\@empty#2\else\ {\rail@annofont #2}\fi
16.545 +}
16.546 +\rail@oval
16.547 +}
16.548 +
16.549 +\def\rail@ltoken#1[#2]{
16.550 +\rail@setbox{%
16.551 +{\rail@termfont \rail@expand{#1}}\ifx\@empty#2\else\ {\rail@annofont #2}\fi
16.552 +}
16.553 +\rail@vloval
16.554 +}
16.555 +
16.556 +\def\rail@rtoken#1[#2]{
16.557 +\rail@setbox{%
16.558 +{\rail@termfont \rail@expand{#1}}\ifx\@empty#2\else\ {\rail@annofont #2}\fi
16.559 +}
16.560 +\rail@vroval
16.561 +}
16.562 +
16.563 +\def\rail@ctoken#1[#2]{
16.564 +\rail@setbox{%
16.565 +{\rail@termfont \rail@expand{#1}}\ifx\@empty#2\else\ {\rail@annofont #2}\fi
16.566 +}
16.567 +\rail@coval
16.568 +}
16.569 +
16.570 +\def\rail@lctoken#1[#2]{
16.571 +\rail@setbox{%
16.572 +{\rail@termfont \rail@expand{#1}}\ifx\@empty#2\else\ {\rail@annofont #2}\fi
16.573 +}
16.574 +\rail@vlcoval
16.575 +}
16.576 +
16.577 +\def\rail@rctoken#1[#2]{
16.578 +\rail@setbox{%
16.579 +{\rail@termfont \rail@expand{#1}}\ifx\@empty#2\else\ {\rail@annofont #2}\fi
16.580 +}
16.581 +\rail@vrcoval
16.582 +}
16.583 +
16.584 +\def\rail@nont#1[#2]{
16.585 +\rail@setbox{%
16.586 +{\rail@nontfont \rail@expand{#1}}\ifx\@empty#2\else\ {\rail@annofont #2}\fi
16.587 +}
16.588 +\rail@frame
16.589 +}
16.590 +
16.591 +\def\rail@lnont#1[#2]{
16.592 +\rail@setbox{%
16.593 +{\rail@nontfont \rail@expand{#1}}\ifx\@empty#2\else\ {\rail@annofont #2}\fi
16.594 +}
16.595 +\rail@vlframe
16.596 +}
16.597 +
16.598 +\def\rail@rnont#1[#2]{
16.599 +\rail@setbox{%
16.600 +{\rail@nontfont \rail@expand{#1}}\ifx\@empty#2\else\ {\rail@annofont #2}\fi
16.601 +}
16.602 +\rail@vrframe
16.603 +}
16.604 +
16.605 +\def\rail@cnont#1[#2]{
16.606 +\rail@setbox{%
16.607 +{\rail@nontfont \rail@expand{#1}}\ifx\@empty#2\else\ {\rail@annofont #2}\fi
16.608 +}
16.609 +\rail@cframe
16.610 +}
16.611 +
16.612 +\def\rail@lcnont#1[#2]{
16.613 +\rail@setbox{%
16.614 +{\rail@nontfont \rail@expand{#1}}\ifx\@empty#2\else\ {\rail@annofont #2}\fi
16.615 +}
16.616 +\rail@vlcframe
16.617 +}
16.618 +
16.619 +\def\rail@rcnont#1[#2]{
16.620 +\rail@setbox{%
16.621 +{\rail@nontfont \rail@expand{#1}}\ifx\@empty#2\else\ {\rail@annofont #2}\fi
16.622 +}
16.623 +\rail@vrcframe
16.624 +}
16.625 +
16.626 +\def\rail@term#1[#2]{
16.627 +\rail@setbox{%
16.628 +{\rail@termfont #1}\ifx\@empty#2\else\ {\rail@annofont #2}\fi
16.629 +}
16.630 +\rail@oval
16.631 +}
16.632 +
16.633 +\def\rail@lterm#1[#2]{
16.634 +\rail@setbox{%
16.635 +{\rail@termfont #1}\ifx\@empty#2\else\ {\rail@annofont #2}\fi
16.636 +}
16.637 +\rail@vloval
16.638 +}
16.639 +
16.640 +\def\rail@rterm#1[#2]{
16.641 +\rail@setbox{%
16.642 +{\rail@termfont #1}\ifx\@empty#2\else\ {\rail@annofont #2}\fi
16.643 +}
16.644 +\rail@vroval
16.645 +}
16.646 +
16.647 +\def\rail@cterm#1[#2]{
16.648 +\rail@setbox{%
16.649 +{\rail@termfont #1}\ifx\@empty#2\else\ {\rail@annofont #2}\fi
16.650 +}
16.651 +\rail@coval
16.652 +}
16.653 +
16.654 +\def\rail@lcterm#1[#2]{
16.655 +\rail@setbox{%
16.656 +{\rail@termfont #1}\ifx\@empty#2\else\ {\rail@annofont #2}\fi
16.657 +}
16.658 +\rail@vlcoval
16.659 +}
16.660 +
16.661 +\def\rail@rcterm#1[#2]{
16.662 +\rail@setbox{%
16.663 +{\rail@termfont #1}\ifx\@empty#2\else\ {\rail@annofont #2}\fi
16.664 +}
16.665 +\rail@vrcoval
16.666 +}
16.667 +
16.668 +\def\rail@annote[#1]{
16.669 +\rail@setbox{\rail@annofont #1}
16.670 +\rail@text
16.671 +}
16.672 +
16.673 +% \rail@box : temporary box for \rail@oval and \rail@frame
16.674 +%
16.675 +% \rail@setbox{TEXT} : set \rail@box to TEXT, set \rail@tmpa to width
16.676 +%
16.677 +% \rail@oval : format \rail@box of width \rail@tmpa inside an oval
16.678 +% \rail@vloval : format \rail@box of width \rail@tmpa inside an oval, vector left
16.679 +% \rail@vroval : format \rail@box of width \rail@tmpa inside an oval, vector right
16.680 +%
16.681 +% \rail@coval : same as \rail@oval, but centered between \rail@x and
16.682 +% \rail@mx
16.683 +% \rail@vlcoval : same as \rail@oval, but centered between \rail@x and
16.684 +% \rail@mx, vector left
16.685 +% \rail@vrcoval : same as \rail@oval, but centered between \rail@x and
16.686 +% \rail@mx, vector right
16.687 +%
16.688 +% \rail@frame : format \rail@box of width \rail@tmpa inside a frame
16.689 +% \rail@vlframe : format \rail@box of width \rail@tmpa inside a frame, vector left
16.690 +% \rail@vrframe : format \rail@box of width \rail@tmpa inside a frame, vector right
16.691 +%
16.692 +% \rail@cframe : same as \rail@frame, but centered between \rail@x and
16.693 +% \rail@mx
16.694 +% \rail@vlcframe : same as \rail@frame, but centered between \rail@x and
16.695 +% \rail@mx, vector left
16.696 +% \rail@vrcframe : same as \rail@frame, but centered between \rail@x and
16.697 +% \rail@mx, vector right
16.698 +%
16.699 +% \rail@text : format \rail@box of width \rail@tmpa above the line
16.700 +
16.701 +\newbox\rail@box
16.702 +
16.703 +\def\rail@setbox#1{
16.704 +\setbox\rail@box\hbox{\strut#1}
16.705 +\rail@tmpa=\wd\rail@box
16.706 +\divide\rail@tmpa by \railunit
16.707 +}
16.708 +
16.709 +\def\rail@oval{
16.710 +\advance\rail@x by \rail@boxlf
16.711 +\rail@eline
16.712 +\advance\rail@tmpa by \rail@ovalsp
16.713 +\ifnum\rail@tmpa<\rail@boxht\rail@tmpa=\rail@boxht\fi
16.714 +\rail@tmpb=\rail@tmpa
16.715 +\divide\rail@tmpb by 2
16.716 +\advance\rail@y by -\rail@boxhht
16.717 +\rail@put{\makebox(\number\rail@tmpa,\number\rail@boxht){\box\rail@box}}
16.718 +\advance\rail@y by \rail@boxhht
16.719 +\advance\rail@x by \rail@tmpb
16.720 +\rail@put{\oval(\number\rail@tmpa,\number\rail@boxht)}
16.721 +\advance\rail@x by \rail@tmpb
16.722 +\rail@ex=\rail@x
16.723 +\advance\rail@x by \rail@boxrt
16.724 +}
16.725 +
16.726 +\def\rail@vloval{
16.727 +\advance\rail@x by \rail@boxlf
16.728 +\rail@eline
16.729 +\advance\rail@tmpa by \rail@ovalsp
16.730 +\ifnum\rail@tmpa<\rail@boxht\rail@tmpa=\rail@boxht\fi
16.731 +\rail@tmpb=\rail@tmpa
16.732 +\divide\rail@tmpb by 2
16.733 +\advance\rail@y by -\rail@boxhht
16.734 +\rail@put{\makebox(\number\rail@tmpa,\number\rail@boxht){\box\rail@box}}
16.735 +\advance\rail@y by \rail@boxhht
16.736 +\advance\rail@x by \rail@tmpb
16.737 +\rail@put{\oval(\number\rail@tmpa,\number\rail@boxht)}
16.738 +\advance\rail@x by \rail@tmpb
16.739 +\rail@ex=\rail@x
16.740 +\advance\rail@x by \rail@boxrt
16.741 +\rail@vleline
16.742 +}
16.743 +
16.744 +\def\rail@vroval{
16.745 +\advance\rail@x by \rail@boxlf
16.746 +\rail@vreline
16.747 +\advance\rail@tmpa by \rail@ovalsp
16.748 +\ifnum\rail@tmpa<\rail@boxht\rail@tmpa=\rail@boxht\fi
16.749 +\rail@tmpb=\rail@tmpa
16.750 +\divide\rail@tmpb by 2
16.751 +\advance\rail@y by -\rail@boxhht
16.752 +\rail@put{\makebox(\number\rail@tmpa,\number\rail@boxht){\box\rail@box}}
16.753 +\advance\rail@y by \rail@boxhht
16.754 +\advance\rail@x by \rail@tmpb
16.755 +\rail@put{\oval(\number\rail@tmpa,\number\rail@boxht)}
16.756 +\advance\rail@x by \rail@tmpb
16.757 +\rail@ex=\rail@x
16.758 +\advance\rail@x by \rail@boxrt
16.759 +}
16.760 +
16.761 +\def\rail@coval{
16.762 +\rail@tmpb=\rail@tmpa
16.763 +\advance\rail@tmpb by \rail@ovalsp
16.764 +\ifnum\rail@tmpb<\rail@boxht\rail@tmpb=\rail@boxht\fi
16.765 +\advance\rail@tmpb by \rail@boxlf
16.766 +\advance\rail@tmpb by \rail@boxrt
16.767 +\rail@tmpc=\rail@mx
16.768 +\advance\rail@tmpc by -\rail@x
16.769 +\advance\rail@tmpc by -\rail@tmpb
16.770 +\divide\rail@tmpc by 2
16.771 +\ifnum\rail@tmpc>0
16.772 +\advance\rail@x by \rail@tmpc
16.773 +\fi
16.774 +\rail@oval
16.775 +}
16.776 +
16.777 +\def\rail@vlcoval{
16.778 +\rail@tmpb=\rail@tmpa
16.779 +\advance\rail@tmpb by \rail@ovalsp
16.780 +\ifnum\rail@tmpb<\rail@boxht\rail@tmpb=\rail@boxht\fi
16.781 +\advance\rail@tmpb by \rail@boxlf
16.782 +\advance\rail@tmpb by \rail@boxrt
16.783 +\rail@tmpc=\rail@mx
16.784 +\advance\rail@tmpc by -\rail@x
16.785 +\advance\rail@tmpc by -\rail@tmpb
16.786 +\divide\rail@tmpc by 2
16.787 +\ifnum\rail@tmpc>0
16.788 +\advance\rail@x by \rail@tmpc
16.789 +\fi
16.790 +\rail@vloval
16.791 +}
16.792 +
16.793 +\def\rail@vrcoval{
16.794 +\rail@tmpb=\rail@tmpa
16.795 +\advance\rail@tmpb by \rail@ovalsp
16.796 +\ifnum\rail@tmpb<\rail@boxht\rail@tmpb=\rail@boxht\fi
16.797 +\advance\rail@tmpb by \rail@boxlf
16.798 +\advance\rail@tmpb by \rail@boxrt
16.799 +\rail@tmpc=\rail@mx
16.800 +\advance\rail@tmpc by -\rail@x
16.801 +\advance\rail@tmpc by -\rail@tmpb
16.802 +\divide\rail@tmpc by 2
16.803 +\ifnum\rail@tmpc>0
16.804 +\advance\rail@x by \rail@tmpc
16.805 +\fi
16.806 +\rail@vroval
16.807 +}
16.808 +
16.809 +\def\rail@frame{
16.810 +\advance\rail@x by \rail@boxlf
16.811 +\rail@eline
16.812 +\advance\rail@tmpa by \rail@framesp
16.813 +\ifnum\rail@tmpa<\rail@boxht\rail@tmpa=\rail@boxht\fi
16.814 +\advance\rail@y by -\rail@boxhht
16.815 +\rail@put{\framebox(\number\rail@tmpa,\number\rail@boxht){\box\rail@box}}
16.816 +\advance\rail@y by \rail@boxhht
16.817 +\advance\rail@x by \rail@tmpa
16.818 +\rail@ex=\rail@x
16.819 +\advance\rail@x by \rail@boxrt
16.820 +}
16.821 +
16.822 +\def\rail@vlframe{
16.823 +\advance\rail@x by \rail@boxlf
16.824 +\rail@eline
16.825 +\advance\rail@tmpa by \rail@framesp
16.826 +\ifnum\rail@tmpa<\rail@boxht\rail@tmpa=\rail@boxht\fi
16.827 +\advance\rail@y by -\rail@boxhht
16.828 +\rail@put{\framebox(\number\rail@tmpa,\number\rail@boxht){\box\rail@box}}
16.829 +\advance\rail@y by \rail@boxhht
16.830 +\advance\rail@x by \rail@tmpa
16.831 +\rail@ex=\rail@x
16.832 +\advance\rail@x by \rail@boxrt
16.833 +\rail@vleline
16.834 +}
16.835 +
16.836 +\def\rail@vrframe{
16.837 +\advance\rail@x by \rail@boxlf
16.838 +\rail@vreline
16.839 +\advance\rail@tmpa by \rail@framesp
16.840 +\ifnum\rail@tmpa<\rail@boxht\rail@tmpa=\rail@boxht\fi
16.841 +\advance\rail@y by -\rail@boxhht
16.842 +\rail@put{\framebox(\number\rail@tmpa,\number\rail@boxht){\box\rail@box}}
16.843 +\advance\rail@y by \rail@boxhht
16.844 +\advance\rail@x by \rail@tmpa
16.845 +\rail@ex=\rail@x
16.846 +\advance\rail@x by \rail@boxrt
16.847 +}
16.848 +
16.849 +\def\rail@cframe{
16.850 +\rail@tmpb=\rail@tmpa
16.851 +\advance\rail@tmpb by \rail@framesp
16.852 +\ifnum\rail@tmpb<\rail@boxht\rail@tmpb=\rail@boxht\fi
16.853 +\advance\rail@tmpb by \rail@boxlf
16.854 +\advance\rail@tmpb by \rail@boxrt
16.855 +\rail@tmpc=\rail@mx
16.856 +\advance\rail@tmpc by -\rail@x
16.857 +\advance\rail@tmpc by -\rail@tmpb
16.858 +\divide\rail@tmpc by 2
16.859 +\ifnum\rail@tmpc>0
16.860 +\advance\rail@x by \rail@tmpc
16.861 +\fi
16.862 +\rail@frame
16.863 +}
16.864 +
16.865 +\def\rail@vlcframe{
16.866 +\rail@tmpb=\rail@tmpa
16.867 +\advance\rail@tmpb by \rail@framesp
16.868 +\ifnum\rail@tmpb<\rail@boxht\rail@tmpb=\rail@boxht\fi
16.869 +\advance\rail@tmpb by \rail@boxlf
16.870 +\advance\rail@tmpb by \rail@boxrt
16.871 +\rail@tmpc=\rail@mx
16.872 +\advance\rail@tmpc by -\rail@x
16.873 +\advance\rail@tmpc by -\rail@tmpb
16.874 +\divide\rail@tmpc by 2
16.875 +\ifnum\rail@tmpc>0
16.876 +\advance\rail@x by \rail@tmpc
16.877 +\fi
16.878 +\rail@vlframe
16.879 +}
16.880 +
16.881 +\def\rail@vrcframe{
16.882 +\rail@tmpb=\rail@tmpa
16.883 +\advance\rail@tmpb by \rail@framesp
16.884 +\ifnum\rail@tmpb<\rail@boxht\rail@tmpb=\rail@boxht\fi
16.885 +\advance\rail@tmpb by \rail@boxlf
16.886 +\advance\rail@tmpb by \rail@boxrt
16.887 +\rail@tmpc=\rail@mx
16.888 +\advance\rail@tmpc by -\rail@x
16.889 +\advance\rail@tmpc by -\rail@tmpb
16.890 +\divide\rail@tmpc by 2
16.891 +\ifnum\rail@tmpc>0
16.892 +\advance\rail@x by \rail@tmpc
16.893 +\fi
16.894 +\rail@vrframe
16.895 +}
16.896 +
16.897 +\def\rail@text{
16.898 +\advance\rail@x by \rail@textlf
16.899 +\advance\rail@y by \rail@textup
16.900 +\rail@put{\box\rail@box}
16.901 +\advance\rail@y by -\rail@textup
16.902 +\advance\rail@x by \rail@tmpa
16.903 +\advance\rail@x by \rail@textrt
16.904 +}
16.905 +
16.906 +% alternatives
16.907 +%
16.908 +% \rail@jx \rail@jy : current join point
16.909 +%
16.910 +% \rail@gx \rail@gy \rail@gex \rail@grx : global versions of \rail@x etc,
16.911 +% to pass values over group closings
16.912 +%
16.913 +% \rail@mx : maximum x so far
16.914 +%
16.915 +% \rail@sy : starting \rail@y for alternatives
16.916 +%
16.917 +% \rail@jput : put at (\rail@jx,\rail@jy)
16.918 +%
16.919 +% \rail@joval[PART] : put \oval[PART] with adjust
16.920 +
16.921 +\newcount\rail@jx
16.922 +\newcount\rail@jy
16.923 +
16.924 +\newcount\rail@gx
16.925 +\newcount\rail@gy
16.926 +\newcount\rail@gex
16.927 +\newcount\rail@grx
16.928 +
16.929 +\newcount\rail@sy
16.930 +\newcount\rail@mx
16.931 +
16.932 +\def\rail@jput{
16.933 +\put(\number\rail@jx,\number\rail@jy)
16.934 +}
16.935 +
16.936 +\def\rail@joval[#1]{
16.937 +\advance\rail@jx by \rail@joinadj
16.938 +\rail@jput{\oval(\number\rail@joinsz,\number\rail@joinsz)[#1]}
16.939 +\advance\rail@jx by -\rail@joinadj
16.940 +}
16.941 +
16.942 +% \rail@barsplit : incoming split for '|'
16.943 +%
16.944 +% \rail@plussplit : incoming split for '+'
16.945 +%
16.946 +
16.947 +\def\rail@barsplit{
16.948 +\advance\rail@jy by -\rail@joinhsz
16.949 +\rail@joval[tr]
16.950 +\advance\rail@jx by \rail@joinhsz
16.951 +}
16.952 +
16.953 +\def\rail@plussplit{
16.954 +\advance\rail@jy by -\rail@joinhsz
16.955 +\advance\rail@jx by \rail@joinsz
16.956 +\rail@joval[tl]
16.957 +\advance\rail@jx by -\rail@joinhsz
16.958 +}
16.959 +
16.960 +% \rail@alt{SPLIT} : start alternatives with incoming split SPLIT
16.961 +%
16.962 +
16.963 +\def\rail@alt#1{
16.964 +\rail@sy=\rail@y
16.965 +\rail@jx=\rail@x
16.966 +\rail@jy=\rail@y
16.967 +\advance\rail@x by \rail@joinsz
16.968 +\rail@mx=0
16.969 +\let\rail@list=\@empty
16.970 +\let\rail@comma=\@empty
16.971 +\let\rail@split=#1
16.972 +\begingroup
16.973 +\rail@sx=\rail@x
16.974 +\rail@rx=0
16.975 +}
16.976 +
16.977 +% \rail@nextalt{FIX}{Y} : start next alternative at vertical position Y
16.978 +% and fix-up FIX
16.979 +%
16.980 +
16.981 +\def\rail@nextalt#1#2{
16.982 +\global\rail@gx=\rail@x
16.983 +\global\rail@gy=\rail@y
16.984 +\global\rail@gex=\rail@ex
16.985 +\global\rail@grx=\rail@rx
16.986 +\endgroup
16.987 +#1
16.988 +\ifnum\rail@gx>\rail@mx\rail@mx=\rail@gx\fi
16.989 +\ifnum\rail@grx>\rail@mx\rail@mx=\rail@grx\fi
16.990 +\edef\rail@list{\rail@list\rail@comma\number\rail@gex:\number\rail@gy}
16.991 +\def\rail@comma{,}
16.992 +\rail@split
16.993 +\let\rail@split=\@empty
16.994 +\rail@sety{#2}
16.995 +\rail@tmpa=\rail@jy
16.996 +\advance\rail@tmpa by -\rail@y
16.997 +\advance\rail@tmpa by -\rail@joinhsz
16.998 +\rail@jput{\line(0,-1){\number\rail@tmpa}}
16.999 +\rail@jy=\rail@y
16.1000 +\advance\rail@jy by \rail@joinhsz
16.1001 +\advance\rail@jx by \rail@joinhsz
16.1002 +\rail@joval[bl]
16.1003 +\advance\rail@jx by -\rail@joinhsz
16.1004 +\rail@ex=\rail@x
16.1005 +\begingroup
16.1006 +\rail@sx=\rail@x
16.1007 +\rail@rx=0
16.1008 +}
16.1009 +
16.1010 +% \rail@barjoin : outgoing join for first '|' alternative
16.1011 +%
16.1012 +% \rail@plusjoin : outgoing join for first '+' alternative
16.1013 +%
16.1014 +% \rail@altjoin : join for subsequent alternative
16.1015 +%
16.1016 +
16.1017 +\def\rail@barjoin{
16.1018 +\ifnum\rail@y<\rail@sy
16.1019 +\global\rail@gex=\rail@jx
16.1020 +\else
16.1021 +\global\rail@gex=\rail@ex
16.1022 +\fi
16.1023 +\advance\rail@jy by -\rail@joinhsz
16.1024 +\rail@joval[tl]
16.1025 +\advance\rail@jx by -\rail@joinhsz
16.1026 +\ifnum\rail@y<\rail@sy
16.1027 +\rail@altjoin
16.1028 +\fi
16.1029 +}
16.1030 +
16.1031 +\def\rail@plusjoin{
16.1032 +\global\rail@gex=\rail@ex
16.1033 +\advance\rail@jy by -\rail@joinhsz
16.1034 +\advance\rail@jx by -\rail@joinsz
16.1035 +\rail@joval[tr]
16.1036 +\advance\rail@jx by \rail@joinhsz
16.1037 +}
16.1038 +
16.1039 +\def\rail@altjoin{
16.1040 +\rail@eline
16.1041 +\rail@tmpa=\rail@jy
16.1042 +\advance\rail@tmpa by -\rail@y
16.1043 +\advance\rail@tmpa by -\rail@joinhsz
16.1044 +\rail@jput{\line(0,-1){\number\rail@tmpa}}
16.1045 +\rail@jy=\rail@y
16.1046 +\advance\rail@jy by \rail@joinhsz
16.1047 +\advance\rail@jx by -\rail@joinhsz
16.1048 +\rail@joval[br]
16.1049 +\advance\rail@jx by \rail@joinhsz
16.1050 +}
16.1051 +
16.1052 +% \rail@eltsplit EX:Y; : split EX:Y into \rail@ex \rail@y
16.1053 +%
16.1054 +% \rail@endalt{JOIN} : end alternatives with outgoing join JOIN
16.1055 +
16.1056 +\def\rail@eltsplit#1:#2;{\rail@ex=#1\rail@y=#2}
16.1057 +
16.1058 +\def\rail@endalt#1{
16.1059 +\global\rail@gx=\rail@x
16.1060 +\global\rail@gy=\rail@y
16.1061 +\global\rail@gex=\rail@ex
16.1062 +\global\rail@grx=\rail@rx
16.1063 +\endgroup
16.1064 +\ifnum\rail@gx>\rail@mx\rail@mx=\rail@gx\fi
16.1065 +\ifnum\rail@grx>\rail@mx\rail@mx=\rail@grx\fi
16.1066 +\edef\rail@list{\rail@list\rail@comma\number\rail@gex:\number\rail@gy}
16.1067 +\rail@x=\rail@mx
16.1068 +\rail@jx=\rail@x
16.1069 +\rail@jy=\rail@sy
16.1070 +\advance\rail@jx by \rail@joinsz
16.1071 +\let\rail@join=#1
16.1072 +\@for\rail@elt:=\rail@list\do{
16.1073 +\expandafter\rail@eltsplit\rail@elt;
16.1074 +\rail@join
16.1075 +\let\rail@join=\rail@altjoin
16.1076 +}
16.1077 +\rail@x=\rail@mx
16.1078 +\rail@y=\rail@sy
16.1079 +\rail@ex=\rail@gex
16.1080 +\advance\rail@x by \rail@joinsz
16.1081 +}
16.1082 +
16.1083 +% \rail@bar : start '|' alternatives
16.1084 +%
16.1085 +% \rail@nextbar : next '|' alternative
16.1086 +%
16.1087 +% \rail@endbar : end '|' alternatives
16.1088 +%
16.1089 +
16.1090 +\def\rail@bar{
16.1091 +\rail@alt\rail@barsplit
16.1092 +}
16.1093 +
16.1094 +\def\rail@nextbar{
16.1095 +\rail@nextalt\relax
16.1096 +}
16.1097 +
16.1098 +\def\rail@endbar{
16.1099 +\rail@endalt\rail@barjoin
16.1100 +}
16.1101 +
16.1102 +% \rail@plus : start '+' alternatives
16.1103 +%
16.1104 +% \rail@nextplus: next '+' alternative
16.1105 +%
16.1106 +% \rail@endplus : end '+' alternatives
16.1107 +%
16.1108 +
16.1109 +\def\rail@plus{
16.1110 +\rail@alt\rail@plussplit
16.1111 +}
16.1112 +
16.1113 +\def\rail@nextplus{
16.1114 +\rail@nextalt\rail@fixplus
16.1115 +}
16.1116 +
16.1117 +\def\rail@fixplus{
16.1118 +\ifnum\rail@gy<\rail@sy
16.1119 +\begingroup
16.1120 +\rail@x=\rail@gx
16.1121 +\rail@y=\rail@gy
16.1122 +\rail@ex=\rail@gex
16.1123 +\rail@rx=\rail@grx
16.1124 +\ifnum\rail@x<\rail@rx
16.1125 +\rail@x=\rail@rx
16.1126 +\fi
16.1127 +\rail@eline
16.1128 +\rail@jx=\rail@x
16.1129 +\rail@jy=\rail@y
16.1130 +\advance\rail@jy by \rail@joinhsz
16.1131 +\rail@joval[br]
16.1132 +\advance\rail@jx by \rail@joinhsz
16.1133 +\rail@tmpa=\rail@sy
16.1134 +\advance\rail@tmpa by -\rail@joinhsz
16.1135 +\advance\rail@tmpa by -\rail@jy
16.1136 +\rail@jput{\line(0,1){\number\rail@tmpa}}
16.1137 +\rail@jy=\rail@sy
16.1138 +\advance\rail@jy by -\rail@joinhsz
16.1139 +\advance\rail@jx by \rail@joinhsz
16.1140 +\rail@joval[tl]
16.1141 +\advance\rail@jy by \rail@joinhsz
16.1142 +\global\rail@gx=\rail@jx
16.1143 +\global\rail@gy=\rail@jy
16.1144 +\global\rail@gex=\rail@gx
16.1145 +\global\rail@grx=\rail@rx
16.1146 +\endgroup
16.1147 +\fi
16.1148 +}
16.1149 +
16.1150 +\def\rail@endplus{
16.1151 +\rail@endalt\rail@plusjoin
16.1152 +}
16.1153 +
16.1154 +% \rail@cr{Y} : carriage return to vertical position Y
16.1155 +
16.1156 +\def\rail@cr#1{
16.1157 +\rail@tmpa=\rail@sx
16.1158 +\advance\rail@tmpa by \rail@joinsz
16.1159 +\ifnum\rail@x<\rail@tmpa\rail@x=\rail@tmpa\fi
16.1160 +\rail@eline
16.1161 +\rail@jx=\rail@x
16.1162 +\rail@jy=\rail@y
16.1163 +\advance\rail@x by \rail@joinsz
16.1164 +\ifnum\rail@x>\rail@rx\rail@rx=\rail@x\fi
16.1165 +\advance\rail@jy by -\rail@joinhsz
16.1166 +\rail@joval[tr]
16.1167 +\advance\rail@jx by \rail@joinhsz
16.1168 +\rail@sety{#1}
16.1169 +\rail@tmpa=\rail@jy
16.1170 +\advance\rail@tmpa by -\rail@y
16.1171 +\advance\rail@tmpa by -\rail@boxsp
16.1172 +\advance\rail@tmpa by -\rail@joinhsz
16.1173 +\rail@jput{\line(0,-1){\number\rail@tmpa}}
16.1174 +\rail@jy=\rail@y
16.1175 +\advance\rail@jy by \rail@boxsp
16.1176 +\advance\rail@jy by \rail@joinhsz
16.1177 +\advance\rail@jx by -\rail@joinhsz
16.1178 +\rail@joval[br]
16.1179 +\advance\rail@jy by -\rail@joinhsz
16.1180 +\rail@tmpa=\rail@jx
16.1181 +\advance\rail@tmpa by -\rail@sx
16.1182 +\advance\rail@tmpa by -\rail@joinhsz
16.1183 +\rail@jput{\line(-1,0){\number\rail@tmpa}}
16.1184 +\rail@jx=\rail@sx
16.1185 +\advance\rail@jx by \rail@joinhsz
16.1186 +\advance\rail@jy by -\rail@joinhsz
16.1187 +\rail@joval[tl]
16.1188 +\advance\rail@jx by -\rail@joinhsz
16.1189 +\rail@tmpa=\rail@boxsp
16.1190 +\advance\rail@tmpa by -\rail@joinsz
16.1191 +\rail@jput{\line(0,-1){\number\rail@tmpa}}
16.1192 +\advance\rail@jy by -\rail@tmpa
16.1193 +\advance\rail@jx by \rail@joinhsz
16.1194 +\rail@joval[bl]
16.1195 +\rail@x=\rail@jx
16.1196 +\rail@ex=\rail@x
16.1197 +}
16.1198 +
16.1199 +% default setup for Isabelle
16.1200 +\newenvironment{railoutput}%
16.1201 +{\begin{list}{}{\rail@param}\def\rail@expand{\relax}\makeatletter}{\makeatother\end{list}}
16.1202 +
16.1203 +\def\rail@termfont{\isabellestyle{tt}}
16.1204 +\def\rail@nontfont{\isabellestyle{it}}
16.1205 +\def\rail@namefont{\isabellestyle{it}}
17.1 --- a/src/Tools/isac/ROOT Tue Mar 10 13:25:00 2020 +0100
17.2 +++ b/src/Tools/isac/ROOT Wed Mar 11 15:25:52 2020 +0100
17.3 @@ -26,7 +26,7 @@
17.4 Build_Isac
17.5
17.6 (* run "./bin/isabelle build -v -b Lucas_Interpreter" *)
17.7 -session Lucas_Interpreter = HOL +
17.8 +session Interpret = HOL +
17.9 description \<open>
17.10 Session Isac restricted to code required for Lucas_Interpreter.
17.11 "Lucas-Interpretation on Isabelle’s Functions"
