1.1 --- a/doc-src/isac/jrocnik/eJMT-paper/jrocnik_eJMT.tex Sun Sep 09 17:32:22 2012 +0200
1.2 +++ b/doc-src/isac/jrocnik/eJMT-paper/jrocnik_eJMT.tex Sun Sep 09 19:05:02 2012 +0200
1.3 @@ -336,13 +336,13 @@
1.4 \>$( \; {\tt case} \; t \; {\tt of} \; {\it pat}_1
1.5 \Rightarrow t_1 \; |\dots| \; {\it pat}_n\Rightarrow t_n \; )$
1.6 \end{tabbing} }
1.7 -\noindent \textit{The running example's program uses some of these elements
1.8 -(marked by {\tt tt-font} on p.\pageref{expl-program}): ${\tt
1.9 -let}\dots{\tt in}$ in lines $02 \dots 11$, as well as {\tt last} for
1.10 -lists and {\tt o} for functional (forward) composition in line
1.11 -$10$. In fact, the whole program is an Isabelle term with specific
1.12 -function constants like {\sc program}, {\sc Substitute} and {\sc
1.13 -Rewrite\_Set\_Inst} in lines $01$ and $10$ respectively.}
1.14 +\noindent The running example's program uses some of these elements
1.15 +(marked by {\tt tt-font} on p.\pageref{s:impl}): for instance {\tt
1.16 +let}\dots{\tt in} in lines {\rm 02} \dots {\rm 13}. In fact, the whole program
1.17 +is an Isabelle term with specific function constants like {\tt
1.18 +program}, {\tt Take}, {\tt Rewrite}, {\tt Subproblem} and {\tt
1.19 +Rewrite\_Set} in lines {\rm 01, 03. 04, 07, 10} and {\rm 11, 12}
1.20 +respectively.
1.21
1.22 % Terms may also contain $\lambda$-abstractions. For example, $\lambda
1.23 % x. \; x$ is the identity function.
1.24 @@ -403,7 +403,7 @@
1.25 % list}$:
1.26
1.27 \item[Substitute:] ${\it substitution}\Rightarrow{\it
1.28 -term}\Rightarrow{\it term}$:
1.29 +term}\Rightarrow{\it term}$: allows to access sub-terms.
1.30
1.31 \item[Take:] ${\it term}\Rightarrow{\it term}$:
1.32 this tactic has no effect in the program; but it creates a side-effect
1.33 @@ -412,15 +412,25 @@
1.34
1.35 \item[Subproblem:] ${\it theory} * {\it specification} * {\it
1.36 method}\Rightarrow{\it argument}\;{\it list}\Rightarrow{\it term}$:
1.37 -this tactic allows to enter a phase of interactive specification
1.38 -of a theory ($\Re$, $\cal C$, etc), a formal specification (for instance,
1.39 -a specific type of equation) and a method (for instance, solving an
1.40 -equation symbolically or numerically).
1.41 -
1.42 +this tactic is a generalisation of a function call: it takes an
1.43 +\textit{argument list} as usual, and additionally a triple consisting
1.44 +of an Isabelle \textit{theory}, an implicit \textit{specification} of the
1.45 +program and a \textit{method} containing data for Lucas-Interpretation,
1.46 +last not least a program (as an explicit specification)~\footnote{In
1.47 +interactive tutoring these three items can be determined explicitly
1.48 +by the user.}.
1.49 \end{description}
1.50 The tactics play a specific role in
1.51 Lucas-Interpretation~\cite{wn:lucas-interp-12}: they are treated as
1.52 -break-points and control is handed over to the user. The user is free
1.53 +break-points where, as a side-effect, a line is added to a calculation
1.54 +
1.55 +.\\.\\.\\
1.56 +
1.57 +protocol
1.58 +
1.59 +.\\.\\.\\
1.60 +
1.61 +and control is handed over to the user. The user is free
1.62 to investigate underlying knowledge, applicable theorems, etc. And
1.63 the user can proceed constructing a solution by input of a tactic to
1.64 be applied or by input of a formula; in the latter case the
1.65 @@ -436,7 +446,7 @@
1.66 \begin{description}
1.67 \item[Repeat:] ${\it tactic}\Rightarrow{\it term}\Rightarrow{\it
1.68 term}$: iterates over tactics which take a {\it term} as argument as
1.69 -long as a tactic is applicable (for instance, {\it Rewrite\_Set} might
1.70 +long as a tactic is applicable (for instance, {\tt Rewrite\_Set} might
1.71 not be applicable).
1.72
1.73 \item[Try:] ${\it tactic}\Rightarrow{\it term}\Rightarrow{\it term}$:
1.74 @@ -984,12 +994,12 @@
1.75 computes a solution for the problem from Fig.\ref{fig-interactive} on
1.76 p.\pageref{fig-interactive}. The reader is reminded of
1.77 \S\ref{PL-isab}, the introduction of the programming language:
1.78 -{\small\it
1.79 -\begin{tabbing}\label{s:impl}
1.80 +{\small\it\label{s:impl}
1.81 +\begin{tabbing}
1.82 123l\=123\=123\=123\=123\=123\=123\=((x\=123\=(x \=123\=123\=\kill
1.83 \>{\rm 00}\>val program =\\
1.84 \>{\rm 01}\> "{\tt Program} InverseZTransform (X\_eq::bool) = \\
1.85 -\>{\rm 02}\>\> {\tt LET} \\
1.86 +\>{\rm 02}\>\> {\tt let} \\
1.87 \>{\rm 03}\>\>\> X\_eq = {\tt Take} X\_eq ; \\
1.88 \>{\rm 04}\>\>\> X\_eq = {\tt Rewrite} ruleZY X\_eq ; \\
1.89 \>{\rm 05}\>\>\> (X\_z::real) = lhs X\_eq ; \\ %no inside-out evaluation
1.90 @@ -1001,7 +1011,7 @@
1.91 \>{\rm 10}\>\>\> (X'\_eq::bool) = {\tt Take} ((X'::real =$>$ bool) z = ZZ\_1 part\_frac) ; \\
1.92 \>{\rm 11}\>\>\> X'\_eq = (({\tt Rewrite\_Set} ruleYZ) @@ \\
1.93 \>{\rm 12}\>\>\>\>\> $\;\;$ ({\tt Rewrite\_Set} inverse\_z)) X'\_eq \\
1.94 -\>{\rm 13}\>\> {\tt IN } \\
1.95 +\>{\rm 13}\>\> {\tt in } \\
1.96 \>{\rm 14}\>\>\> X'\_eq"
1.97 \end{tabbing}}
1.98 % ORIGINAL FROM Inverse_Z_Transform.thy
1.99 @@ -1030,22 +1040,22 @@
1.100 the steps of calculation towards a solution (and interactive tutoring
1.101 in step-wise problem solving) are created as a side-effect by
1.102 Lucas-Interpretation. The side-effects are triggered by the tactics
1.103 -\textit{Take}, \textit{Rewrite}, \textit{SubProblem} and
1.104 -\textit{Rewrite\_Set} in the above lines {\rm 03, 04, 07, 10, 11} and
1.105 +\texttt{Take}, \texttt{Rewrite}, \texttt{SubProblem} and
1.106 +\texttt{Rewrite\_Set} in the above lines {\rm 03, 04, 07, 10, 11} and
1.107 {\rm 12} respectively. These tactics produce the lines in the
1.108 calculation on p.\pageref{flow-impl}.
1.109
1.110 The above lines {\rm 05, 06} do not contain a tactics, so they do not
1.111 immediately contribute to the calculation on p.\pageref{flow-impl};
1.112 -rather, they compute actual arguments for the \textit{SubProblem} in
1.113 +rather, they compute actual arguments for the \texttt{SubProblem} in
1.114 line {\rm 09}~\footnote{The tactics also are break-points for the
1.115 interpreter, where control is handed over to the user in interactive
1.116 -tutoring.}.
1.117 +tutoring.}. Line {\rm 11} contains tactical \textit{@@}.
1.118
1.119 \medskip The above program also indicates the dominant role of interactive
1.120 selection of knowledge in the three-dimensional universe of
1.121 mathematics as depicted in Fig.\ref{fig:mathuni} on
1.122 -p.\pageref{fig:mathuni}, The \textit{SubProblem} in the above lines
1.123 +p.\pageref{fig:mathuni}, The \texttt{SubProblem} in the above lines
1.124 {\rm 07..09} is more than a function call with the actual arguments
1.125 \textit{[ (rhs X\_eq)::real, z::real ]}. The programmer has to determine
1.126 three items:
1.127 @@ -1089,12 +1099,51 @@
1.128 The development in the {\sisac}-prototype was done in a separate
1.129 theory~\footnote{http://www.ist.tugraz.at/projects/isac/publ/Build\_Inverse\_Z\_Transform.thy}.
1.130 The workflow tackled the tasks more or less following the order of the
1.131 -above sections from \S\ref{isabisac} to \S\ref{funs}. At each stage the
1.132 -interactivity of Isabelle/jEdit is very supportive. For instance, as soon as the
1.133 -theorems for the Z-transform are established (see \S\ref{isabisac}) it is tempting
1.134 -to see them at work:
1.135 +above sections from \S\ref{isabisac} to \S\ref{funs}. At each stage
1.136 +the interactivity of Isabelle/jEdit is very supportive. For instance,
1.137 +as soon as the theorems for the Z-transform are established (see
1.138 +\S\ref{isabisac}) it is tempting to see them at work: First we need
1.139 +technical prerequisites not worth to mention and parse a string to a
1.140 +term using {\sisac}'s function \textit{str2term}:
1.141 +{\footnotesize\label{exp-spec}
1.142 +\begin{verbatim}
1.143 + ML {*
1.144 + val (thy, ro, er) = (@{theory}, tless_true, eval_rls);
1.145 + val t = str2term "z / (z - 1) + z / (z - \<alpha>) + 1";
1.146 + *}
1.147 +\end{verbatim}}
1.148 +Then we call {\sisac}'s rewrite-engine directly by \textit{rewrite\_} (instead via Lucas-Interpreter by \textit{Rewrite}) and yield
1.149 +a rewritten term \textit{t'} together with assumptions:
1.150 +{\footnotesize\label{exp-spec}
1.151 +\begin{verbatim}
1.152 + ML {*
1.153 + val SOME (t', asm) = rewrite_ thy ro er true (num_str @{thm rule3}) t;
1.154 + *}
1.155 +\end{verbatim}}
1.156 +And any evaluation of an \texttt{ML} section immediately responds with the
1.157 +values computed, for instance with the result of the rewrites, which above
1.158 +have been returned in the internal term representation --- here are the more
1.159 +readable string representations:
1.160 +{\footnotesize\label{exp-spec}
1.161 +\begin{verbatim}
1.162 + ML {*
1.163 + term2str t';
1.164 + terms2str (asm);
1.165 + *}
1.166 + val it = "- ?u [- ?n - 1] + z / (z - α) + 1": string
1.167 + val it = "[|| z || < 1]": string
1.168 +\end{verbatim}}
1.169 +Looking at the last line shows how the system will reliably handle
1.170 +assumptions like the convergence radius.
1.171 +%WN gerne w"urde ich oben das Beispiel aus subsection {*Apply Rules*}
1.172 +%WN aus http://www.ist.tugraz.at/projects/isac/publ/Build_Inverse_Z_Transform.thy.
1.173 +%WN Leider bekomme ich einen Fehler --- siehst Du eine schnelle Korrektur ?
1.174
1.175
1.176 +.\\.\\.\\
1.177 +
1.178 +TODO test the function \textit{argument\_of} which is embedded in the
1.179 +ruleset which is used to evaluate the program by the Lucas-Interpreter.
1.180
1.181 .\\.\\.\\
1.182