The paper will use the problem in Fig.\ref{fig-interactive} as a

 running example:

 \medskip The major example resulting from the case study will be used

 as running example throughout this paper. This example requires a

 program resembling the size of real-world applications in engineering;

 such a size was considered essential for the case study, since there

 are many small programs for a long time (mainly concerned with

 elementary Computer Algebra like simplification, equation solving,

 calculus, etc.~\footnote{The programs existing in the {\sisac}

 prototype are found at

 http://www.ist.tugraz.at/projects/isac/www/kbase/met/index\_met.html})

 \paragraph{The mathematical background of the running example} is the

 following: In Signal Processing, ``the ${\cal Z}$-Transform for

 discrete-time signals is the counterpart of the Laplace transform for

 continuous-time signals, and they each have a similar relationship to

 the corresponding Fourier transform. One motivation for introducing

 this generalization is that the Fourier transform does not converge

 for all sequences, and it is useful to have a generalization of the

 Fourier transform that encompasses a broader class of signals. A

 second advantage is that in analytic problems, the $z$-transform

 notation is often more convenient than the Fourier transform

 notation.''  ~\cite[p. 128]{oppenheim2010discrete}.  The $z$-transform

 is defined as

 \begin{equation*}

 X(z)=\sum_{n=-\infty }^{\infty }x[n]z^{-n}

 \end{equation*}

 where a discrete time sequence $x[n]$ is transformed into the function

 $X(z)$ where $z$ is a continuous complex variable. The inverse

 function is addressed in the running example and can be determined by

 the integral

 \begin{equation*}

 x[n]=\frac{1}{2\pi j} \oint_{C} X(z)\cdot z^{n-1} dz

 \end{equation*}

 where the letter $C$ represents a contour within the range of

 convergence of the $z$- transform. The unit circle can be a special

 case of this contour. Remember that $j$ is the complex number in the

 domain of engineering.  As this transformation requires high effort to

 be solved, tables of commonly used transform pairs are used in

 education as well as in engineering practice; such tables can be found

 at~\cite{wiki:1} or~\cite[Table~3.1]{oppenheim2010discrete} as well.

 A completely solved and more detailed example can be found at

 ~\cite[p. 149f]{oppenheim2010discrete}. 

 Following conventions in engineering education and in practice, the

 running example solves the problem by use of a table. 

 \paragraph{Support for interactive stepwise problem solving} in the

 {\sisac} prototype is shown in Fig.\ref{fig-interactive}~\footnote{ Fig.\ref{fig-interactive} also shows the prototype status of {\sisac}; for instance,

 the lack of 2-dimensional presentation and input of formulas is the major obstacle for field-tests in standard classes.}:

 A student inputs formulas line by line on the \textit{``Worksheet''},

 and each step (i.e. each formula on completion) is immediately checked

 by the system such that at most one inconsistent formula can reside on

 the Worksheet (on the input line, marked by the red $\otimes$).

 If the student gets stuck and does not know the formula to proceed with,

 \paragraph{The Engineering Background of the Problem} comes out of the domain 

 there is the button \framebox{NEXT} proceeding to the next step. The

 Signal Processing, which takes a major part n the authors field of education. 

 button \framebox{AUTO} immediately delivers the final result in case

 The given Problem requests to determine the inverse $z$-transform for a 

 the student is not interested in intermediate steps.

 given term.

 \par

 Adaptive dialogue guidance is already under

 ``The $z$-Transform for discrete-time signals is the counterpart of the 

 construction~\cite{gdaroczy-EP-13} and the two buttons will disappear,

 Laplace transform for continuous-time signals, and they each have a similar 

 since their presence is not wanted in many learning scenarios (in

 relationship to the corresponding Fourier transform. One motivation for 

 particular, {\em not} in written exams).

 introducing this generalization is that the Fourier transform does not 

 converge for all sequences, and it is useful to have a generalization of the 

 The buttons \framebox{Theories}, \framebox{Problems} and

 Fourier transform that encompasses a broader class of signals. A second 

 \framebox{Methods} are the entry points for interactive lookup of the

 advantage is that in analytic problems, the $z$-transform notation is often 

 underlying knowledge.  For instance, pushing \framebox{Theories} in

 more convenient than the Fourier transform notation.''

 the configuration shown in Fig.\ref{fig-interactive}, pops up a

 ~\cite[p. 128]{oppenheim2010discrete}

 ``Theory browser'' displaying the theorem(s) justifying the current

 \par

 step.  All browsers allow to lookup all other theories, thus

 The $z$-transform can be defined as:

 supporting indepentend investigation of underlying definitions,

 \begin{equation}

 theorems, proofs --- where the HTML representation of the browsers is

 X(z)=\sum_{n=-\infty }^{\infty }x[n]z^{-n}

 ready for arbitrary multimedia add-ons.

 \end{equation}

 Upper equation transforms a discrete time sequence $x[n]$ into the function 

 % can be explained by having a look at 

 $X(z)$ where $z$ is a continuous complex variable. The inverse function (as it 

 % Fig.\ref{fig-interactive} which shows the beginning of the interactive 

 is used in the given problem) is defined as:

 % construction of a solution for the problem. This construction is done in the 

 \begin{equation}

 % right window named ``Worksheet''.

 x[n]=\frac{1}{2\pi j} \oint_{C} X(z)\cdot z^{n-1} dz

 % \par

 \end{equation}

 % User-interaction on the Worksheet is {\em checked} and {\em guided} by

 The letter $C$ represents a contour within the range of converge of the $z$-

 % TP services:

 transform. The unit circle can be a special case of this contour. Remember 

 % \begin{enumerate}

 that $j$ is the complex number in the field of engineering.

 % \item Formulas input by the user are {\em checked} by TP: such a

 As this transformation requires high effort to be solved, tables of 

 % formula establishes a proof situation --- the prover has to derive the

 common transform pairs are used in education as well as in (TODO: real); such 

 % formula from the logical context. The context is built up from the

 tables can be found at~\cite{wiki:1} or~\cite[Table~3.1]{oppenheim2010discrete} as well.

 % formal specification of the problem (here hidden from the user) by the

 A completely solved and more detailed example can be found at

 % Lucas-Interpreter.

 ~\cite[p. 149f]{oppenheim2010discrete}. The upcoming implementation tries to 

 % \item If the user gets stuck, the program developed below in this

 fit this example in the way it is toughed at the authors university.

 % paper ``knows the next step'' and Lucas-Interpretation provides services

 % featuring so-called ``next-step-guidance''; this is out of scope of this

 % paper and can be studied in~\cite{gdaroczy-EP-13}.

 % \end{enumerate} It should be noted that the programmer using the

 \paragraph{The educational aspect} can be explained by having a look at 

 % TP-based language is not concerned with interaction at all; we will

 Fig.\ref{fig-interactive} which shows the beginning of the interactive 

 % see that the program contains neither input-statements nor

 construction of a solution for the problem. This construction is done in the 

 % output-statements. Rather, interaction is handled by the interpreter

 right window named ``Worksheet''.

 % of the language.

 \par

 % 

 User-interaction on the Worksheet is {\em checked} and {\em guided} by

 % So there is a clear separation of concerns: Dialogues are adapted by

 TP services:

 % dialogue authors (in Java-based tools), using TP services provided by

 \begin{enumerate}

 % Lucas-Interpretation. The latter acts on programs developed by

 \item Formulas input by the user are {\em checked} by TP: such a

 % mathematics-authors (in Isabelle/ML); their task is concern of this

 formula establishes a proof situation --- the prover has to derive the

 % paper.

 formula from the logical context. The context is built up from the

 formal specification of the problem (here hidden from the user) by the

 \bigskip The paper is structured as follows: The introduction

 Lucas-Interpreter.

 \item If the user gets stuck, the program developed below in this

 paper ``knows the next step'' and Lucas-Interpretation provides services

 featuring so-called ``next-step-guidance''; this is out of scope of this

 paper and can be studied in~\cite{gdaroczy-EP-13}.

 \end{enumerate} It should be noted that the programmer using the

 TP-based language is not concerned with interaction at all; we will

 see that the program contains neither input-statements nor

 output-statements. Rather, interaction is handled by the interpreter

 of the language.

 So there is a clear separation of concerns: Dialogues are adapted by

 dialogue authors (in Java-based tools), using TP services provided by

 Lucas-Interpretation. The latter acts on programs developed by

 mathematics-authors (in Isabelle/ML); their task is concern of this

 paper.

 The paper is structured as follows: The introduction

 the executable fragment in the language of the theorem prover

 the executable fragment of Higher-Order Logic (HOL) in the theorem prover

 introductory courses \cite{nipkow-prog-prove}. HOL (Higher-Order Logic)

 introductory courses \cite{nipkow-prog-prove}. HOL is a typed logic whose type system resembles that of functional programming

 is a typed logic whose type system resembles that of functional programming

 {\footnotesize

 {\footnotesize\label{ml-check-program}

 13     ...\end{verbatim}} 

 13     ...

 \end{verbatim}} 

 \section{Conclusion}\label{conclusion}

 \section{Summary and Conclusions}\label{conclusion}

 respective implementation: mechanisation of mathematics and domain

 respective implementation in the {\sisac} prototype: mechanisation of mathematics and domain

 Lucas-Interpreter is cumbersome.

 Lucas-Interpreter is cumbersome. 

 From these experiences a successful proof of concept can be concluded:

 \subsection{Conclusions and Expectations to the Future}

 From the above mentioned experiences a successful proof of concept can be concluded:

 \begin{itemize}

 \begin{enumerate}

 \end{itemize} 

 \item\label{CAS} Extend Isabelle's computational features in direction of

 \textit{verfied} Computer Algebra: simplification extended by

 algorithms beyond rewriting (cancellation of multivariate rationals,

 factorisation, partial fraction decomposition, etc), equation solving

 , integration, etc.

 \end{enumerate} 

 components for virtual workbenches appealing to practitioner of

 components for virtual workbenches appealing to practitioners of

 \medskip Interactive course material, as addressed by the title, then

 \subsection{Preview to Development of Course Material}

 Interactive course material, as addressed by the title,

 TP-based program: Lucas-Interpretation not only provides an

 TP-based program: The introduction \S\ref{intro} briefly shows that Lucas-Interpretation not only provides an