% on mathematics in \emph{STEOP}, the introductory orientation phase in

 % on mathematics in \emph{STEOP}, the introductory orientation phase in

 % Austria. \emph{STEOP} is considered an opportunity to investigate the

 % Austria. \emph{STEOP} is considered an opportunity to investigate the

 % impact of {\sisac}'s prototype on the issue and others.

 % impact of {\sisac}'s prototype on the issue and others.

 % 

 % 

 important component, interactive support for step-wise problem

 important component, interactive support for step-wise problem

 solving. Theorem-Proving (TP) technology can provide such support by

 solving. Theorem-Proving (TP) technology can provide such support by

 specific services. An important part of such services is called

 specific services. An important part of such services is called

 ``next-step-guidance'', generated by a specific kind of ``TP-based

 ``next-step-guidance'', generated by a specific kind of ``TP-based

 programming language''. In the

 programming language''. In the

 programming language, called

 programming language, called

 Lucas-Interpreter~\cite{wn:lucas-interp-12}. The language and the

 Lucas-Interpreter~\cite{wn:lucas-interp-12}. The language and the

 interpreter will be briefly re-introduced in order to make the paper

 interpreter will be briefly re-introduced in order to make the paper

 self-contained.

 self-contained.

 with programming in this TP-based language. The experience was gained

 with programming in this TP-based language. The experience was gained

 in a case study by the author. The author was considered an ideal

 in a case study by the author. The author was considered an ideal

 candidate for this study for the following reasons: as a student in

 candidate for this study for the following reasons: as a student in

 Telematics (computer science with focus on Signal Processing) he had

 Telematics (computer science with focus on Signal Processing) he had

 general knowledge in programming as well as specific domain knowledge

 general knowledge in programming as well as specific domain knowledge

 in Signal Processing; and he was not involved in the development of

 in Signal Processing; and he was not involved in the development of

 {\sisac}'s programming language and interpeter, thus a novice to the

 {\sisac}'s programming language and interpeter, thus a novice to the

 language.

 language.

 interactive course material for a specific ``Adavanced Signal

 interactive course material for a specific ``Adavanced Signal

 Processing Lab'' in a higher semester, (2) respective program

 Processing Lab'' in a higher semester, (2) respective program

 development with as little advice from the {\sisac}-team and (3) records

 development with as little advice from the {\sisac}-team and (3) records

 and comments for the main steps of development in an Isabelle theory;

 and comments for the main steps of development in an Isabelle theory;

 this theory should provide guidelines for future programmers. An

 this theory should provide guidelines for future programmers. An

 excerpt from this theory is the main part of this paper.

 excerpt from this theory is the main part of this paper.

 running example:

 running example:

 \begin{figure} [htb]

 \begin{figure} [htb]

 \begin{center}

 \begin{center}

 \caption{Step-wise problem solving guided by the TP-based program}

 \caption{Step-wise problem solving guided by the TP-based program}

 \label{fig-interactive}

 \label{fig-interactive}

 \end{center}

 \end{center}

 \end{figure}

 \end{figure}

 determine the inverse Z-transform for a given term. Fig.\ref{fig-interactive}

 determine the inverse Z-transform for a given term. Fig.\ref{fig-interactive}

 also shows the beginning of the interactive construction of a solution

 also shows the beginning of the interactive construction of a solution

 for the problem. This construction is done in the right window named

 for the problem. This construction is done in the right window named

 ``Worksheet''.

 ``Worksheet''.

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

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

 TP services:

 TP services:

 \begin{enumerate}

 \begin{enumerate}

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

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

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

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

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

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

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

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

 see that the program contains neither input-statements nor

 see that the program contains neither input-statements nor

 output-statements. Rather, interaction is handled by services

 output-statements. Rather, interaction is handled by services

 generated automatically.

 generated automatically.

 adapted by dialogue authors (in Java-based tools), using automatically

 adapted by dialogue authors (in Java-based tools), using automatically

 generated TP services, while the TP-based program is written by

 generated TP services, while the TP-based program is written by

 mathematics experts (in Isabelle/ML). The latter is concern of this

 mathematics experts (in Isabelle/ML). The latter is concern of this

 paper.

 paper.

 \S\ref{intro} is followed by a brief re-introduction of the TP-based

 \S\ref{intro} is followed by a brief re-introduction of the TP-based

 programming language in \S\ref{PL}, which extends the executable

 programming language in \S\ref{PL}, which extends the executable

 fragment of Isabelle's language (\S\ref{PL-isab}) by tactics which

 fragment of Isabelle's language (\S\ref{PL-isab}) by tactics which

 play a specific role in Lucas-Interpretation and in providing the TP

 play a specific role in Lucas-Interpretation and in providing the TP

 services (\S\ref{PL-tacs}). The main part in \S\ref{trial} describes

 services (\S\ref{PL-tacs}). The main part in \S\ref{trial} describes

 function constants like {\sc program}, {\sc Substitute} and {\sc

 function constants like {\sc program}, {\sc Substitute} and {\sc

 Rewrite\_Set\_Inst} in lines $01$ and $10$ respectively.}

 Rewrite\_Set\_Inst} in lines $01$ and $10$ respectively.}

 % Terms may also contain $\lambda$-abstractions. For example, $\lambda

 % Terms may also contain $\lambda$-abstractions. For example, $\lambda

 % x. \; x$ is the identity function.

 % x. \; x$ is the identity function.

 \textbf{Formulae} are terms of type \textit{bool}. There are the basic

 \textbf{Formulae} are terms of type \textit{bool}. There are the basic

 constants \textit{True} and \textit{False} and the usual logical

 constants \textit{True} and \textit{False} and the usual logical

 connectives (in decreasing order of precedence): $\neg, \land, \lor,

 connectives (in decreasing order of precedence): $\neg, \land, \lor,

 \rightarrow$.

 \rightarrow$.

 Analysis~\footnote{http://isabelle.in.tum.de/dist/library/HOL/HOL-Multivariate\_Analysis}. However,

 Analysis~\footnote{http://isabelle.in.tum.de/dist/library/HOL/HOL-Multivariate\_Analysis}. However,

 building up knowledge such that a proof for the above rules would be

 building up knowledge such that a proof for the above rules would be

 reasonably short and easily comprehensible, still requires lots of

 reasonably short and easily comprehensible, still requires lots of

 work (and is definitely out of scope of our case study).

 work (and is definitely out of scope of our case study).

 engineering sciences, the process does not stop with the mechanization of

 engineering sciences, the process does not stop with the mechanization of

 mathematics traditionally used in these sciences. Rather, ``Formal Methods''~\cite{TODO-formal-methods}

 mathematics traditionally used in these sciences. Rather, ``Formal Methods''~\cite{TODO-formal-methods}

 are expected to proceed to formal and explicit description of physical items.  Signal Processing,

 are expected to proceed to formal and explicit description of physical items.  Signal Processing,

 for instance is concerned with physical devices for signal acquisition

 for instance is concerned with physical devices for signal acquisition

 and reconstruction, which involve measuring a physical signal, storing

 and reconstruction, which involve measuring a physical signal, storing

 ``Domain engineering''\cite{db-domain-engineering} is concerned with

 ``Domain engineering''\cite{db-domain-engineering} is concerned with

 {\em specification} of these devices' components and features; this

 {\em specification} of these devices' components and features; this

 part in the process of mechanization is only at the beginning in domains

 part in the process of mechanization is only at the beginning in domains

 like Signal Processing.

 like Signal Processing.

 add ``algorithmic knowledge'' in Fig.\ref{fig:mathuni} on

 add ``algorithmic knowledge'' in Fig.\ref{fig:mathuni} on

 p.\pageref{fig:mathuni}.  As we shall see below, TP-based programming

 p.\pageref{fig:mathuni}.  As we shall see below, TP-based programming

 starts with a formal {\em specification} of the problem to be solved.

 starts with a formal {\em specification} of the problem to be solved.

 \subsection{Specification of the Problem}\label{spec}

 \subsection{Specification of the Problem}\label{spec}

 %WN <--> \chapter 7 der Thesis

 %WN <--> \chapter 7 der Thesis

 %WN die Argumentation unten sollte sich NUR auf Verifikation beziehen..

 %WN die Argumentation unten sollte sich NUR auf Verifikation beziehen..

 The problem of the running example is textually described in

 The problem of the running example is textually described in

 Fig.\ref{fig-interactive} on p.\pageref{fig-interactive}. The {\em

 Fig.\ref{fig-interactive} on p.\pageref{fig-interactive}. The {\em

 formal} specification of this problem, in traditional mathematical

 formal} specification of this problem, in traditional mathematical

 notation, could look lik is this:

 notation, could look lik is this:

   \label{eg:neuper2}

   \label{eg:neuper2}

   {\small\begin{tabbing}

   {\small\begin{tabbing}

   123,\=postcond \=: \= $\forall \,A^\prime\, u^\prime \,v^\prime.\,$\=\kill

   123,\=postcond \=: \= $\forall \,A^\prime\, u^\prime \,v^\prime.\,$\=\kill

   \hfill \\

   \hfill \\

   Specification:\\

   Specification:\\

   \>postcond \>:{\small  $\;A=2uv-u^2 \;\land\; (\frac{u}{2})^2+(\frac{v}{2})^2=r^2 \;\land$}\\

   \>postcond \>:{\small  $\;A=2uv-u^2 \;\land\; (\frac{u}{2})^2+(\frac{v}{2})^2=r^2 \;\land$}\\

   \>     \>\>{\small $\;\forall \;A^\prime\; u^\prime \;v^\prime.\;(A^\prime=2u^\prime v^\prime-(u^\prime)^2 \land

   \>     \>\>{\small $\;\forall \;A^\prime\; u^\prime \;v^\prime.\;(A^\prime=2u^\prime v^\prime-(u^\prime)^2 \land

   (\frac{u^\prime}{2})^2+(\frac{v^\prime}{2})^2=r^2) \Longrightarrow A^\prime \leq A$} \\

   (\frac{u^\prime}{2})^2+(\frac{v^\prime}{2})^2=r^2) \Longrightarrow A^\prime \leq A$} \\

   \end{tabbing}

   \end{tabbing}

   }

   }

 And this is the implementation of the formal specification in the present

 And this is the implementation of the formal specification in the present

 prototype, still bar-bones without support for authoring:

 prototype, still bar-bones without support for authoring:

 \subsection{Implementation of the TP-based Program}\label{progr}

 \subsection{Implementation of the TP-based Program}\label{progr}

 %WN <--> \chapter 8 der Thesis

 %WN <--> \chapter 8 der Thesis

 TODO

 TODO

 \section{Workflow of Programming in the Prototype}\label{workflow}

 \section{Workflow of Programming in the Prototype}\label{workflow}

 \subsection{Preparations and Trials}\label{flow-prep}

 \subsection{Preparations and Trials}\label{flow-prep}

 \subsection{Implementation in Isabelle/{\isac}}\label{flow-impl}

 \subsection{Implementation in Isabelle/{\isac}}\label{flow-impl}

 TODO Build\_Inverse\_Z\_Transform.thy ... ``imports Isac''

 TODO Build\_Inverse\_Z\_Transform.thy ... ``imports Isac''

 \subsection{Transfer into the Isabelle/{\isac} Knowledge}\label{flow-trans}

 \subsection{Transfer into the Isabelle/{\isac} Knowledge}\label{flow-trans}

 \emph{all}.} of them. Unfortunately the goal of TP Isabelle is to

 \emph{all}.} of them. Unfortunately the goal of TP Isabelle is to

 reach a high level of \emph{all} but it in real it will still be a

 reach a high level of \emph{all} but it in real it will still be a

 survey of knowledge which links to other knowledge and {{\sisac}{}} a

 survey of knowledge which links to other knowledge and {{\sisac}{}} a

 trainer and helper but no human compensating calculator. 

 trainer and helper but no human compensating calculator. 

 \par

 \par

 specifications of problems out of topics from Signal Processing, etc.)

 specifications of problems out of topics from Signal Processing, etc.)

 physical knowledge. The result is a three-dimensional universe of

 physical knowledge. The result is a three-dimensional universe of

 mathematics seen in Figure~\ref{fig:mathuni}.

 mathematics seen in Figure~\ref{fig:mathuni}.

 \subsection{Notes on Problems with Traditional Notation}

 \subsection{Notes on Problems with Traditional Notation}

 \paragraph{During research} on these topic severely problems on

 \paragraph{During research} on these topic severely problems on

 traditional notations have been discovered. Some of them have been

 traditional notations have been discovered. Some of them have been