
diff -r 7f3760f39bdc -r f8845fc8f38d doc-isac/jrocnik/eJMT-paper/jrocnik_eJMT.tex
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-isac/jrocnik/eJMT-paper/jrocnik_eJMT.tex	Tue Sep 17 09:50:52 2013 +0200
@@ -0,0 +1,2135 @@
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+% Electronic Journal of Mathematics and Technology (eJMT) %
+% style sheet for LaTeX.  Please do not modify sections   %
+% or commands marked 'eJMT'.                              %
+%                                                         %
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%                                                         %
+% eJMT commands                                           %
+%                                                         %
+\documentclass[12pt,a4paper]{article}%                    %
+\usepackage{times}                                        %
+\usepackage{amsfonts,amsmath,amssymb}                     %
+\usepackage[a4paper]{geometry}                            %
+\usepackage{fancyhdr}                                     %
+\usepackage{color}                                        %
+\usepackage[pdftex]{hyperref} % see note below            %
+\usepackage{graphicx}%                                    %
+\hypersetup{                                              %
+    a4paper,                                              %
+    breaklinks                                            %
+}                                                         %
+%                                                         %
+\newtheorem{theorem}{Theorem}                             %
+\newtheorem{acknowledgement}[theorem]{Acknowledgement}    %
+\newtheorem{algorithm}[theorem]{Algorithm}                %
+\newtheorem{axiom}[theorem]{Axiom}                        %
+\newtheorem{case}[theorem]{Case}                          %
+\newtheorem{claim}[theorem]{Claim}                        %
+\newtheorem{conclusion}[theorem]{Conclusion}              %
+\newtheorem{condition}[theorem]{Condition}                %
+\newtheorem{conjecture}[theorem]{Conjecture}              %
+\newtheorem{corollary}[theorem]{Corollary}                %
+\newtheorem{criterion}[theorem]{Criterion}                %
+\newtheorem{definition}[theorem]{Definition}              %
+\newtheorem{example}[theorem]{Example}                    %
+\newtheorem{exercise}[theorem]{Exercise}                  %
+\newtheorem{lemma}[theorem]{Lemma}                        %
+\newtheorem{notation}[theorem]{Notation}                  %
+\newtheorem{problem}[theorem]{Problem}                    %
+\newtheorem{proposition}[theorem]{Proposition}            %
+\newtheorem{remark}[theorem]{Remark}                      %
+\newtheorem{solution}[theorem]{Solution}                  %
+\newtheorem{summary}[theorem]{Summary}                    %
+\newenvironment{proof}[1][Proof]{\noindent\textbf{#1.} }  %
+{\ \rule{0.5em}{0.5em}}                                   %
+%                                                         %
+% eJMT page dimensions                                    %
+%                                                         %
+\geometry{left=2cm,right=2cm,top=3.2cm,bottom=4cm}        %
+%                                                         %
+% eJMT header & footer                                    %
+%                                                         %
+\newcounter{ejmtFirstpage}                                %
+\setcounter{ejmtFirstpage}{1}                             %
+\pagestyle{empty}                                         %
+\setlength{\headheight}{14pt}                             %
+\geometry{left=2cm,right=2cm,top=3.2cm,bottom=4cm}        %
+\pagestyle{fancyplain}                                    %
+\fancyhf{}                                                %
+\fancyhead[c]{\small The Electronic Journal of Mathematics%
+\ and Technology, Volume 1, Number 1, ISSN 1933-2823}     %
+\cfoot{%                                                  %
+  \ifnum\value{ejmtFirstpage}=0%                          %
+    {\vtop to\hsize{\hrule\vskip .2cm\thepage}}%          %
+  \else\setcounter{ejmtFirstpage}{0}\fi%                  %
+}                                                         %
+%                                                         %
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%
+% Please place your own definitions here
+%
+\def\isac{${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$}
+\def\sisac{\footnotesize${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$}
+
+\usepackage{color}
+\definecolor{lgray}{RGB}{238,238,238}
+
+\usepackage{hyperref}
+
+%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%                                                         %
+% How to use hyperref                                     %
+% -------------------                                     %
+%                                                         %
+% Probably the only way you will need to use the hyperref %
+% package is as follows.  To make some text, say          %
+% "My Text Link", into a link to the URL                  %
+% http://something.somewhere.com/mystuff, use             %
+%                                                         %
+% \href{http://something.somewhere.com/mystuff}{My Text Link}
+%                                                         %
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%
+\begin{document}
+%
+% document title
+%
+\title{Trials with TP-based Programming
+\\
+for Interactive Course Material}%
+%
+% Single author.  Please supply at least your name,
+% email address, and affiliation here.
+%
+\author{\begin{tabular}{c}
+\textit{Jan Ro\v{c}nik} \\
+jan.rocnik@student.tugraz.at \\
+IST, SPSC\\
+Graz University of Technology\\
+Austria\end{tabular}
+}%
+%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%                                                         %
+% eJMT commands - do not change these                     %
+%                                                         %
+\date{}                                                   %
+\maketitle                                                %
+%                                                         %
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%
+% abstract
+%
+\begin{abstract}
+
+Traditional course material in engineering disciplines lacks an
+important component, interactive support for step-wise problem
+solving. Theorem-Proving (TP) technology is appropriate for one part
+of such support, in checking user-input. For the other part of such
+support, guiding the learner towards a solution, another kind of
+technology is required.
+
+Both kinds of support can be achieved by so-called
+Lucas-Interpretation which combines deduction and computation and, for
+the latter, uses a novel kind of programming language. This language
+is based on (Computer) Theorem Proving (TP), thus called a ``TP-based
+programming language''.
+
+This paper is the experience report of the first ``application
+programmer'' using this language for creating exercises in step-wise
+problem solving for an advanced lab in Signal Processing. The tasks
+involved in TP-based programming are described together with the
+experience gained from a prototype of the programming language and of
+it's interpreter.
+
+The report concludes with a positive proof of concept, states
+insufficiency usability of the prototype and captures the requirements
+for further development of both, the programming language and the
+interpreter.
+%
+\end{abstract}%
+%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%                                                         %
+% eJMT command                                            %
+%                                                         %
+\thispagestyle{fancy}                                     %
+%                                                         %
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%
+% Please use the following to indicate sections, subsections,
+% etc.  Please also use \subsubsection{...}, \paragraph{...}
+% and \subparagraph{...} as necessary.
+%
+
+\section{Introduction}\label{intro}
+
+% \paragraph{Didactics of mathematics} 
+%WN: wenn man in einem high-quality paper von 'didactics' spricht, 
+%WN muss man am state-of-the-art ankn"upfen -- siehe
+%WN W.Neuper, On the Emergence of TP-based Educational Math Assistants
+% faces a specific issue, a gap
+% between (1) introduction of math concepts and skills and (2)
+% application of these concepts and skills, which usually are separated
+% into different units in curricula (for good reasons). For instance,
+% (1) teaching partial fraction decomposition is separated from (2)
+% application for inverse Z-transform in signal processing.
+% 
+% \par This gap is an obstacle for applying math as an fundamental
+% thinking technology in engineering: In (1) motivation is lacking
+% because the question ``What is this stuff good for?'' cannot be
+% treated sufficiently, and in (2) the ``stuff'' is not available to
+% students in higher semesters as widespread experience shows.
+% 
+% \paragraph{Motivation} taken by this didactic issue on the one hand,
+% and ongoing research and development on a novel kind of educational
+% mathematics assistant at Graz University of
+% Technology~\footnote{http://www.ist.tugraz.at/isac/} promising to
+% scope with this issue on the other hand, several institutes are
+% planning to join their expertise: the Institute for Information
+% Systems and Computer Media (IICM), the Institute for Software
+% Technology (IST), the Institutes for Mathematics, the Institute for
+% Signal Processing and Speech Communication (SPSC), the Institute for
+% Structural Analysis and the Institute of Electrical Measurement and
+% Measurement Signal Processing.
+%WN diese Information ist f"ur das Paper zu spezielle, zu aktuell 
+%WN und damit zu verg"anglich.
+% \par This thesis is the first attempt to tackle the above mentioned
+% issue, it focuses on Telematics, because these specific studies focus
+% on mathematics in \emph{STEOP}, the introductory orientation phase in
+% Austria. \emph{STEOP} is considered an opportunity to investigate the
+% impact of {\sisac}'s prototype on the issue and others.
+% 
+
+Traditional course material in engineering disciplines lacks an
+important component, interactive support for step-wise problem
+solving. The lack becomes evident by comparing existing course
+material with the sheets collected from written exams (in case solving
+engineering problems is {\em not} deteriorated to multiple choice
+tests) on the topics addressed by the materials.
+Theorem-Proving (TP) technology can provide such support by
+specific services. An important part of such services is called
+``next-step-guidance'', generated by a specific kind of ``TP-based
+programming language''. In the
+{\sisac}-project~\footnote{http://www.ist.tugraz.at/projects/isac/} such
+a language is prototyped in line with~\cite{plmms10} and built upon
+the theorem prover Isabelle~\cite{Nipkow-Paulson-Wenzel:2002}
+\footnote{http://isabelle.in.tum.de/}.
+The TP services are coordinated by a specific interpreter for the
+programming language, called
+Lucas-Interpreter~\cite{wn:lucas-interp-12}. The language 
+ will be briefly re-introduced in order to make the paper
+self-contained.
+
+The main part of the paper is an account of first experiences
+with programming in this TP-based language. The experience was gained
+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
+Telematics (computer science with focus on Signal Processing) he had
+general knowledge in programming as well as specific domain knowledge
+in Signal Processing; and he was {\em not} involved in the development of
+{\sisac}'s programming language and interpreter, thus being a novice to the
+language.
+
+The goals of the case study were: (1) to identify some TP-based programs for
+interactive course material for a specific ``Advanced Signal
+Processing Lab'' in a higher semester, (2) respective program
+development with as little advice as possible from the {\sisac}-team and (3) 
+to document records and comments for the main steps of development in an
+Isabelle theory; this theory should provide guidelines for future programmers.
+An excerpt from this theory is the main part of this paper.
+\par
+
+\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 ${\cal Z}$-transform
+notation is often more convenient than the Fourier transform
+notation.''  ~\cite[p. 128]{oppenheim2010discrete}.  The ${\cal 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 ${\cal 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 transform 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 {\em one inconsistent} formula can reside on
+the Worksheet (on the input line, marked by the red $\otimes$).
+\begin{figure} [htb]
+\begin{center}
+\includegraphics[width=140mm]{fig/isac-Ztrans-math-3}
+%\includegraphics[width=140mm]{fig/isac-Ztrans-math}
+\caption{Step-wise problem solving guided by the TP-based program
+\label{fig-interactive}}
+\end{center}
+\end{figure}
+If the student gets stuck and does not know the formula to proceed
+with, there is the button \framebox{NEXT} presenting the next formula
+on the Worksheet; this feature is called ``next-step-guidance''~\cite{wn:lucas-interp-12}. The button \framebox{AUTO} immediately delivers the
+final result in case the student is not interested in intermediate
+steps.
+
+Adaptive dialogue guidance is already under
+construction~\cite{gdaroczy-EP-13} and the two buttons will disappear,
+since their presence is not wanted in many learning scenarios (in
+particular, {\em not} in written exams).
+
+The buttons \framebox{Theories}, \framebox{Problems} and
+\framebox{Methods} are the entry points for interactive lookup of the
+underlying knowledge.  For instance, pushing \framebox{Theories} in
+the configuration shown in Fig.\ref{fig-interactive}, pops up a
+``Theory browser'' displaying the theorem(s) justifying the current
+step.  The browser allows to lookup all other theories, thus
+supporting indepentend investigation of underlying definitions,
+theorems, proofs --- where the HTML representation of the browsers is
+ready for arbitrary multimedia add-ons. Likewise, the browsers for
+\framebox{Problems} and \framebox{Methods} support context sensitive
+as well as interactive access to specifications and programs
+respectively. 
+
+There is also a simple web-based representation of knowledge items;
+the items under consideration in this paper can be looked up as
+well
+~\footnote{\href{http://www.ist.tugraz.at/projects/isac/www/kbase/thy/browser\_info/HOL/HOL-Real/Isac/Inverse\_Z\_Transform.thy}{http://www.ist.tugraz.at/projects/isac/www/kbase/thy/browser\_info/HOL/HOL-Real/Isac/\textbf{Inverse\_Z\_Transform.thy}}}
+~\footnote{\href{http://www.ist.tugraz.at/projects/isac/www/kbase/thy/browser\_info/HOL/HOL-Real/Isac/Partial\_Fractions.thy}{http://www.ist.tugraz.at/projects/isac/www/kbase/thy/browser\_info/HOL/HOL-Real/Isac/\textbf{Partial\_Fractions.thy}}}
+~\footnote{\href{http://www.ist.tugraz.at/projects/isac/www/kbase/thy/browser\_info/HOL/HOL-Real/Isac/Build\_Inverse\_Z\_Transform.thy}{http://www.ist.tugraz.at/projects/isac/www/kbase/thy/browser\_info/HOL/HOL-Real/Isac/\textbf{Build\_Inverse\_Z\_Transform.thy}}}.
+
+% can be explained by having a look at 
+% Fig.\ref{fig-interactive} which shows the beginning of the interactive 
+% construction of a solution for the problem. This construction is done in the 
+% right window named ``Worksheet''.
+% \par
+% User-interaction on the Worksheet is {\em checked} and {\em guided} by
+% TP services:
+% \begin{enumerate}
+% \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 from the logical context. The context is built up from the
+% formal specification of the problem (here hidden from the user) by the
+% 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.
+
+\bigskip The paper is structured as follows: The introduction
+\S\ref{intro} is followed by a brief re-introduction of the TP-based
+programming language in \S\ref{PL}, which extends the executable
+fragment of Isabelle's language (\S\ref{PL-isab}) by tactics which
+play a specific role in Lucas-Interpretation and in providing the TP
+services (\S\ref{PL-tacs}). The main part \S\ref{trial} describes
+the main steps in developing the program for the running example:
+prepare domain knowledge, implement the formal specification of the
+problem, prepare the environment for the interpreter, implement the
+program in \S\ref{isabisac} to \S\ref{progr} respectively. 
+The work-flow of programming, debugging and testing is
+described in \S\ref{workflow}. The conclusion \S\ref{conclusion} will
+give directions identified for future development. 
+
+
+\section{\isac's Prototype for a Programming Language}\label{PL} 
+The prototype of the language and of the Lucas-Interpreter is briefly
+described from the point of view of a programmer. The language extends
+the executable fragment of Higher-Order Logic (HOL) in the theorem prover
+Isabelle~\cite{Nipkow-Paulson-Wenzel:2002}\footnote{http://isabelle.in.tum.de/}.
+
+\subsection{The Executable Fragment of Isabelle's Language}\label{PL-isab}
+The executable fragment consists of data-type and function
+definitions.  It's usability even suggests that fragment for
+introductory courses \cite{nipkow-prog-prove}. HOL is a typed logic whose type system resembles that of functional programming
+languages. Thus there are
+\begin{description}
+\item[base types,] in particular \textit{bool}, the type of truth
+values, \textit{nat}, \textit{int}, \textit{complex}, and the types of
+natural, integer and complex numbers respectively in mathematics.
+\item[type constructors] allow to define arbitrary types, from
+\textit{set}, \textit{list} to advanced data-structures like
+\textit{trees}, red-black-trees etc.
+\item[function types,] denoted by $\Rightarrow$.
+\item[type variables,] denoted by $^\prime a, ^\prime b$ etc, provide
+type polymorphism. Isabelle automatically computes the type of each
+variable in a term by use of Hindley-Milner type inference
+\cite{pl:hind97,Milner-78}.
+\end{description}
+
+\textbf{Terms} are formed as in functional programming by applying
+functions to arguments. If $f$ is a function of type
+$\tau_1\Rightarrow \tau_2$ and $t$ is a term of type $\tau_1$ then
+$f\;t$ is a term of type~$\tau_2$. $t\;::\;\tau$ means that term $t$
+has type $\tau$. There are many predefined infix symbols like $+$ and
+$\leq$ most of which are overloaded for various types.
+
+HOL also supports some basic constructs from functional programming:
+{\footnotesize\it\label{isabelle-stmts}
+\begin{tabbing} 123\=\kill
+01\>$( \; {\tt if} \; b \; {\tt then} \; t_1 \; {\tt else} \; t_2 \;)$\\
+02\>$( \; {\tt let} \; x=t \; {\tt in} \; u \; )$\\
+03\>$( \; {\tt case} \; t \; {\tt of} \; {\it pat}_1
+  \Rightarrow t_1 \; |\dots| \; {\it pat}_n\Rightarrow t_n \; )$
+\end{tabbing}}
+\noindent The running example's program uses some of these elements
+(marked by {\tt tt-font} on p.\pageref{s:impl}): for instance {\tt
+let}\dots{\tt in} in lines {\rm 02} \dots {\rm 13}. In fact, the whole program
+is an Isabelle term with specific function constants like {\tt
+program}, {\tt Take}, {\tt Rewrite}, {\tt Subproblem} and {\tt
+Rewrite\_Set} in lines {\rm 01, 03. 04, 07, 10} and {\rm 11, 12}
+respectively.
+
+% Terms may also contain $\lambda$-abstractions. For example, $\lambda
+% x. \; x$ is the identity function.
+
+%JR warum auskommentiert? WN2...
+%WN2 weil ein Punkt wie dieser in weiteren Zusammenh"angen innerhalb
+%WN2 des Papers auftauchen m"usste; nachdem ich einen solchen
+%WN2 Zusammenhang _noch_ nicht sehe, habe ich den Punkt _noch_ nicht
+%WN2 gel"oscht.
+%WN2 Wenn der Punkt nicht weiter gebraucht wird, nimmt er nur wertvollen
+%WN2 Platz f"ur Anderes weg.
+
+\textbf{Formulae} are terms of type \textit{bool}. There are the basic
+constants \textit{True} and \textit{False} and the usual logical
+connectives (in decreasing order of precedence): $\neg, \land, \lor,
+\rightarrow$.
+
+\textbf{Equality} is available in the form of the infix function $=$
+of type $a \Rightarrow a \Rightarrow {\it bool}$. It also works for
+formulas, where it means ``if and only if''.
+
+\textbf{Quantifiers} are written $\forall x. \; P$ and $\exists x. \;
+P$.  Quantifiers lead to non-executable functions, so functions do not
+always correspond to programs, for instance, if comprising \\$(
+\;{\it if} \; \exists x.\;P \; {\it then} \; e_1 \; {\it else} \; e_2
+\;)$.
+
+\subsection{\isac's Tactics for Lucas-Interpretation}\label{PL-tacs}
+The prototype extends Isabelle's language by specific statements
+called tactics~\footnote{{\sisac}'s. These tactics are different from
+Isabelle's tactics: the former concern steps in a calculation, the
+latter concern proofs.}. For the programmer these
+statements are functions with the following signatures:
+
+\begin{description}
+\item[Rewrite:] ${\it theorem}\Rightarrow{\it term}\Rightarrow{\it
+term} * {\it term}\;{\it list}$:
+this tactic applies {\it theorem} to a {\it term} yielding a {\it
+term} and a {\it term list}, the list are assumptions generated by
+conditional rewriting. For instance, the {\it theorem}
+$b\not=0\land c\not=0\Rightarrow\frac{a\cdot c}{b\cdot c}=\frac{a}{b}$
+applied to the {\it term} $\frac{2\cdot x}{3\cdot x}$ yields
+$(\frac{2}{3}, [x\not=0])$.
+
+\item[Rewrite\_Set:] ${\it ruleset}\Rightarrow{\it
+term}\Rightarrow{\it term} * {\it term}\;{\it list}$:
+this tactic applies {\it ruleset} to a {\it term}; {\it ruleset} is
+a confluent and terminating term rewrite system, in general. If
+none of the rules ({\it theorem}s) is applicable on interpretation
+of this tactic, an exception is thrown.
+
+% \item[Rewrite\_Inst:] ${\it substitution}\Rightarrow{\it
+% theorem}\Rightarrow{\it term}\Rightarrow{\it term} * {\it term}\;{\it
+% list}$:
+% 
+% \item[Rewrite\_Set\_Inst:] ${\it substitution}\Rightarrow{\it
+% ruleset}\Rightarrow{\it term}\Rightarrow{\it term} * {\it term}\;{\it
+% list}$:
+
+%SPACEvvv
+\item[Substitute:] ${\it substitution}\Rightarrow{\it
+term}\Rightarrow{\it term}$: allows to access sub-terms.
+%SPACE^^^
+
+\item[Take:] ${\it term}\Rightarrow{\it term}$:
+this tactic has no effect in the program; but it creates a side-effect
+by Lucas-Interpretation (see below) and writes {\it term} to the
+Worksheet.
+
+\item[Subproblem:] ${\it theory} * {\it specification} * {\it
+method}\Rightarrow{\it argument}\;{\it list}\Rightarrow{\it term}$:
+this tactic is a generalisation of a function call: it takes an
+\textit{argument list} as usual, and additionally a triple consisting
+of an Isabelle \textit{theory}, an implicit \textit{specification} of the
+program and a \textit{method} containing data for Lucas-Interpretation,
+last not least a program (as an explicit specification)~\footnote{In
+interactive tutoring these three items can be determined explicitly
+by the user.}.
+\end{description}
+The tactics play a specific role in
+Lucas-Interpretation~\cite{wn:lucas-interp-12}: they are treated as
+break-points where, as a side-effect, a line is added to a calculation
+as a protocol for proceeding towards a solution in step-wise problem
+solving. At the same points Lucas-Interpretation serves interactive
+tutoring and hands over control to the user. The user is free to
+investigate underlying knowledge, applicable theorems, etc.  And the
+user can proceed constructing a solution by input of a tactic to be
+applied or by input of a formula; in the latter case the
+Lucas-Interpreter has built up a logical context (initialised with the
+precondition of the formal specification) such that Isabelle can
+derive the formula from this context --- or give feedback, that no
+derivation can be found.
+
+\subsection{Tactics as Control Flow Statements}
+The flow of control in a program can be determined by {\tt if then else}
+and {\tt case of} as mentioned on p.\pageref{isabelle-stmts} and also
+by additional tactics:
+\begin{description}
+\item[Repeat:] ${\it tactic}\Rightarrow{\it term}\Rightarrow{\it
+term}$: iterates over tactics which take a {\it term} as argument as
+long as a tactic is applicable (for instance, {\tt Rewrite\_Set} might
+not be applicable).
+
+\item[Try:] ${\it tactic}\Rightarrow{\it term}\Rightarrow{\it term}$:
+if {\it tactic} is applicable, then it is applied to {\it term},
+otherwise {\it term} is passed on without changes.
+
+\item[Or:] ${\it tactic}\Rightarrow{\it tactic}\Rightarrow{\it
+term}\Rightarrow{\it term}$: If the first {\it tactic} is applicable,
+it is applied to the first {\it term} yielding another {\it term},
+otherwise the second {\it tactic} is applied; if none is applicable an
+exception is raised.
+
+\item[@@:] ${\it tactic}\Rightarrow{\it tactic}\Rightarrow{\it
+term}\Rightarrow{\it term}$: applies the first {\it tactic} to the
+first {\it term} yielding an intermediate term (not appearing in the
+signature) to which the second {\it tactic} is applied.
+
+\item[While:] ${\it term::bool}\Rightarrow{\it tactic}\Rightarrow{\it
+term}\Rightarrow{\it term}$: if the first {\it term} is true, then the
+{\it tactic} is applied to the first {\it term} yielding an
+intermediate term (not appearing in the signature); the intermediate
+term is added to the environment the first {\it term} is evaluated in
+etc. as long as the first {\it term} is true.
+\end{description}
+The tactics are not treated as break-points by Lucas-Interpretation
+and thus do neither contribute to the calculation nor to interaction.
+
+\section{Concepts and Tasks in TP-based Programming}\label{trial}
+%\section{Development of a Program on Trial}
+
+This section presents all the concepts involved in TP-based
+programming and all the tasks to be accomplished by programmers. The
+presentation uses the running example from
+Fig.\ref{fig-interactive} on p.\pageref{fig-interactive}.
+
+\subsection{Mechanization of Math --- Domain Engineering}\label{isabisac}
+
+%WN was Fachleute unter obigem Titel interessiert findet sich
+%WN unterhalb des auskommentierten Textes.
+
+%WN der Text unten spricht Benutzer-Aspekte anund ist nicht speziell
+%WN auf Computer-Mathematiker fokussiert.
+% \paragraph{As mentioned in the introduction,} a prototype of an
+% educational math assistant called
+% {{\sisac}}\footnote{{{\sisac}}=\textbf{Isa}belle for
+% \textbf{C}alculations, see http://www.ist.tugraz.at/isac/.} bridges
+% the gap between (1) introducation and (2) application of mathematics:
+% {{\sisac}} is based on Computer Theorem Proving (TP), a technology which
+% requires each fact and each action justified by formal logic, so
+% {{{\sisac}{}}} makes justifications transparent to students in
+% interactive step-wise problem solving. By that way {{\sisac}} already
+% can serve both:
+% \begin{enumerate}
+%   \item Introduction of math stuff (in e.g. partial fraction
+% decomposition) by stepwise explaining and exercising respective
+% symbolic calculations with ``next step guidance (NSG)'' and rigorously
+% checking steps freely input by students --- this also in context with
+% advanced applications (where the stuff to be taught in higher
+% semesters can be skimmed through by NSG), and
+%   \item Application of math stuff in advanced engineering courses
+% (e.g. problems to be solved by inverse Z-transform in a Signal
+% Processing Lab) and now without much ado about basic math techniques
+% (like partial fraction decomposition): ``next step guidance'' supports
+% students in independently (re-)adopting such techniques.
+% \end{enumerate} 
+% Before the question is answers, how {{\sisac}}
+% accomplishes this task from a technical point of view, some remarks on
+% the state-of-the-art is given, therefor follow up Section~\ref{emas}.
+% 
+% \subsection{Educational Mathematics Assistants (EMAs)}\label{emas}
+% 
+% \paragraph{Educational software in mathematics} is, if at all, based
+% on Computer Algebra Systems (CAS, for instance), Dynamic Geometry
+% Systems (DGS, for instance \footnote{GeoGebra http://www.geogebra.org}
+% \footnote{Cinderella http://www.cinderella.de/}\footnote{GCLC
+% http://poincare.matf.bg.ac.rs/~janicic/gclc/}) or spread-sheets. These
+% base technologies are used to program math lessons and sometimes even
+% exercises. The latter are cumbersome: the steps towards a solution of
+% such an interactive exercise need to be provided with feedback, where
+% at each step a wide variety of possible input has to be foreseen by
+% the programmer - so such interactive exercises either require high
+% development efforts or the exercises constrain possible inputs.
+% 
+% \subparagraph{A new generation} of educational math assistants (EMAs)
+% is emerging presently, which is based on Theorem Proving (TP). TP, for
+% instance Isabelle and Coq, is a technology which requires each fact
+% and each action justified by formal logic. Pushed by demands for
+% \textit{proven} correctness of safety-critical software TP advances
+% into software engineering; from these advancements computer
+% mathematics benefits in general, and math education in particular. Two
+% features of TP are immediately beneficial for learning:
+% 
+% \paragraph{TP have knowledge in human readable format,} that is in
+% standard predicate calculus. TP following the LCF-tradition have that
+% knowledge down to the basic definitions of set, equality,
+% etc~\footnote{http://isabelle.in.tum.de/dist/library/HOL/HOL.html};
+% following the typical deductive development of math, natural numbers
+% are defined and their properties
+% proven~\footnote{http://isabelle.in.tum.de/dist/library/HOL/Number\_Theory/Primes.html},
+% etc. Present knowledge mechanized in TP exceeds high-school
+% mathematics by far, however by knowledge required in software
+% technology, and not in other engineering sciences.
+% 
+% \paragraph{TP can model the whole problem solving process} in
+% mathematical problem solving {\em within} a coherent logical
+% framework. This is already being done by three projects, by
+% Ralph-Johan Back, by ActiveMath and by Carnegie Mellon Tutor.
+% \par
+% Having the whole problem solving process within a logical coherent
+% system, such a design guarantees correctness of intermediate steps and
+% of the result (which seems essential for math software); and the
+% second advantage is that TP provides a wealth of theories which can be
+% exploited for mechanizing other features essential for educational
+% software.
+% 
+% \subsubsection{Generation of User Guidance in EMAs}\label{user-guid}
+% 
+% One essential feature for educational software is feedback to user
+% input and assistance in coming to a solution.
+% 
+% \paragraph{Checking user input} by ATP during stepwise problem solving
+% is being accomplished by the three projects mentioned above
+% exclusively. They model the whole problem solving process as mentioned
+% above, so all what happens between formalized assumptions (or formal
+% specification) and goal (or fulfilled postcondition) can be
+% mechanized. Such mechanization promises to greatly extend the scope of
+% educational software in stepwise problem solving.
+% 
+% \paragraph{NSG (Next step guidance)} comprises the system's ability to
+% propose a next step; this is a challenge for TP: either a radical
+% restriction of the search space by restriction to very specific
+% problem classes is required, or much care and effort is required in
+% designing possible variants in the process of problem solving
+% \cite{proof-strategies-11}.
+% \par
+% Another approach is restricted to problem solving in engineering
+% domains, where a problem is specified by input, precondition, output
+% and postcondition, and where the postcondition is proven by ATP behind
+% the scenes: Here the possible variants in the process of problem
+% solving are provided with feedback {\em automatically}, if the problem
+% is described in a TP-based programing language: \cite{plmms10} the
+% programmer only describes the math algorithm without caring about
+% interaction (the respective program is functional and even has no
+% input or output statements!); interaction is generated as a
+% side-effect by the interpreter --- an efficient separation of concern
+% between math programmers and dialog designers promising application
+% all over engineering disciplines.
+% 
+% 
+% \subsubsection{Math Authoring in Isabelle/ISAC\label{math-auth}}
+% Authoring new mathematics knowledge in {{\sisac}} can be compared with
+% ``application programing'' of engineering problems; most of such
+% programing uses CAS-based programing languages (CAS = Computer Algebra
+% Systems; e.g. Mathematica's or Maple's programing language).
+% 
+% \paragraph{A novel type of TP-based language} is used by {{\sisac}{}}
+% \cite{plmms10} for describing how to construct a solution to an
+% engineering problem and for calling equation solvers, integration,
+% etc~\footnote{Implementation of CAS-like functionality in TP is not
+% primarily concerned with efficiency, but with a didactic question:
+% What to decide for: for high-brow algorithms at the state-of-the-art
+% or for elementary algorithms comprehensible for students?} within TP;
+% TP can ensure ``systems that never make a mistake'' \cite{casproto} -
+% are impossible for CAS which have no logics underlying.
+% 
+% \subparagraph{Authoring is perfect} by writing such TP based programs;
+% the application programmer is not concerned with interaction or with
+% user guidance: this is concern of a novel kind of program interpreter
+% called Lucas-Interpreter. This interpreter hands over control to a
+% dialog component at each step of calculation (like a debugger at
+% breakpoints) and calls automated TP to check user input following
+% personalized strategies according to a feedback module.
+% \par
+% However ``application programing with TP'' is not done with writing a
+% program: according to the principles of TP, each step must be
+% justified. Such justifications are given by theorems. So all steps
+% must be related to some theorem, if there is no such theorem it must
+% be added to the existing knowledge, which is organized in so-called
+% \textbf{theories} in Isabelle. A theorem must be proven; fortunately
+% Isabelle comprises a mechanism (called ``axiomatization''), which
+% allows to omit proofs. Such a theorem is shown in
+% Example~\ref{eg:neuper1}.
+
+The running example requires to determine the inverse ${\cal Z}$-transform
+for a class of functions. The domain of Signal Processing
+is accustomed to specific notation for the resulting functions, which
+are absolutely capable of being totalled and are called step-response: $u[n]$, where $u$ is the
+function, $n$ is the argument and the brackets indicate that the
+arguments are discrete. Surprisingly, Isabelle accepts the rules for
+$z^{-1}$ in this traditional notation~\footnote{Isabelle
+experts might be particularly surprised, that the brackets do not
+cause errors in typing (as lists).}:
+%\vbox{
+% \begin{example}
+  \label{eg:neuper1}
+  {\footnotesize\begin{tabbing}
+  123\=123\=123\=123\=\kill
+
+  01\>axiomatization where \\
+  02\>\>  rule1: ``$z^{-1}\;1 = \delta [n]$'' and\\
+  03\>\>  rule2: ``$\vert\vert z \vert\vert > 1 \Rightarrow z^{-1}\;z / (z - 1) = u [n]$'' and\\
+  04\>\>  rule3: ``$\vert\vert z \vert\vert < 1 \Rightarrow z / (z - 1) = -u [-n - 1]$'' and \\
+  05\>\>  rule4: ``$\vert\vert z \vert\vert > \vert\vert$ $\alpha$ $\vert\vert \Rightarrow z / (z - \alpha) = \alpha^n \cdot u [n]$'' and\\
+  06\>\>  rule5: ``$\vert\vert z \vert\vert < \vert\vert \alpha \vert\vert \Rightarrow z / (z - \alpha) = -(\alpha^n) \cdot u [-n - 1]$'' and\\
+  07\>\>  rule6: ``$\vert\vert z \vert\vert > 1 \Rightarrow z/(z - 1)^2 = n \cdot u [n]$''
+  \end{tabbing}}
+% \end{example}
+%}
+These 6 rules can be used as conditional rewrite rules, depending on
+the respective convergence radius. Satisfaction from accordance with traditional
+notation contrasts with the above word {\em axiomatization}: As TP-based, the
+programming language expects these rules as {\em proved} theorems, and
+not as axioms implemented in the above brute force manner; otherwise
+all the verification efforts envisaged (like proof of the
+post-condition, see below) would be meaningless.
+
+Isabelle provides a large body of knowledge, rigorously proved from
+the basic axioms of mathematics~\footnote{This way of rigorously
+deriving all knowledge from first principles is called the
+LCF-paradigm in TP.}. In the case of the ${\cal Z}$-transform the most advanced
+knowledge can be found in the theories on Multivariate
+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
+reasonably short and easily comprehensible, still requires lots of
+work (and is definitely out of scope of our case study).
+
+%REMOVED DUE TO SPACE CONSTRAINTS
+%At the state-of-the-art in mechanization of knowledge in engineering
+%sciences, the process does not stop with the mechanization of
+%mathematics traditionally used in these sciences. Rather, ``Formal
+%Methods''~\cite{ fm-03} are expected to proceed to formal and explicit
+%description of physical items.  Signal Processing, for instance is
+%concerned with physical devices for signal acquisition and
+%reconstruction, which involve measuring a physical signal, storing it,
+%and possibly later rebuilding the original signal or an approximation
+%thereof. For digital systems, this typically includes sampling and
+%quantization; devices for signal compression, including audio
+%compression, image compression, and video compression, etc.  ``Domain
+%engineering''\cite{db:dom-eng} is concerned with {\em specification}
+%of these devices' components and features; this part in the process of
+%mechanization is only at the beginning in domains like Signal
+%Processing.
+%
+%TP-based programming, concern of this paper, is determined to
+%add ``algorithmic knowledge'' to the mechanised body of knowledge.
+%% in Fig.\ref{fig:mathuni} on
+%% p.\pageref{fig:mathuni}.  As we shall see below, TP-based programming
+%% starts with a formal {\em specification} of the problem to be solved.
+%% \begin{figure}
+%%   \begin{center}
+%%     \includegraphics[width=110mm]{../../fig/jrocnik/math-universe-small}
+%%     \caption{The three-dimensional universe of mathematics knowledge}
+%%     \label{fig:mathuni}
+%%   \end{center}
+%% \end{figure}
+%% The language for both axes is defined in the axis at the bottom, deductive
+%% knowledge, in {\sisac} represented by Isabelle's theories.
+
+\subsection{Preparation of Simplifiers for the Program}\label{simp}
+
+All evaluation in the prototype's Lucas-Interpreter is done by term rewriting on
+Isabelle's terms, see \S\ref{meth} below; in this section some of respective
+preparations are described. In order to work reliably with term rewriting, the
+respective rule-sets must be confluent and terminating~\cite{nipk:rew-all-that},
+then they are called (canonical) simplifiers. These properties do not go without
+saying, their establishment is a difficult task for the programmer; this task is
+not yet supported in the prototype.
+
+The prototype rewrites using theorems only. Axioms which are theorems as well 
+have been already shown in \S\ref{eg:neuper1} on p.\pageref{eg:neuper1} , we
+assemble them in a rule-set and apply them in ML as follows:
+
+{\footnotesize
+\begin{verbatim}
+   01  val inverse_z = Rls 
+   02      {id       = "inverse_z",
+   03       rew_ord  = dummy_ord,
+   04       erls     = Erls,
+   05       rules    = [Thm ("rule1", @{thm rule1}), Thm ("rule2", @{thm rule1}), 
+   06                   Thm ("rule3", @{thm rule3}), Thm ("rule4", @{thm rule4}), 
+   07                   Thm ("rule5", @{thm rule5}), Thm ("rule6", @{thm rule6})],
+   08       errpatts = [],
+   09       scr      = ""}
+\end{verbatim}}
+
+\noindent The items, line by line, in the above record have the following purpose:
+\begin{description}
+\item[01..02] the ML-value \textit{inverse\_z} stores it's identifier
+as a string for ``reflection'' when switching between the language
+layers of Isabelle/ML (like in the Lucas-Interpreter) and
+Isabelle/Isar (like in the example program on p.\pageref{s:impl} on
+line {\rm 12}).
+
+\item[03..04] both, (a) the rewrite-order~\cite{nipk:rew-all-that}
+\textit{rew\_ord} and (b) the rule-set \textit{erls} are trivial here:
+(a) the \textit{rules} in {\rm 07..12} don't need ordered rewriting
+and (b) the assumptions of the \textit{rules} need not be evaluated
+(they just go into the context during rewriting).
+
+\item[05..07] the \textit{rules} are the axioms from p.\pageref{eg:neuper1};
+also ML-functions (\S\ref{funs}) can come into this list as shown in
+\S\ref{flow-prep}; so they are distinguished by type-constructors \textit{Thm}
+and \textit{Calc} respectively; for the purpose of reflection both
+contain their identifiers.
+
+\item[08..09] are error-patterns not discussed here and \textit{scr}
+is prepared to get a program, automatically generated by {\sisac} for
+producing intermediate rewrites when requested by the user.
+
+\end{description}
+
+%OUTCOMMENTED DUE TO SPACE RESTRICTIONS
+% \noindent It is advisable to immediately test rule-sets; for that
+% purpose an appropriate term has to be created; \textit{parse} takes a
+% context \textit{ctxt} and a string (with \textit{ZZ\_1} denoting ${\cal
+% Z}^{-1}$) and creates a term:
+% 
+% {\footnotesize
+% \begin{verbatim}
+%    01 ML {*
+%    02   val t = parse ctxt "ZZ_1 (z / (z - 1) + z / (z - </alpha>) + 1)";
+%    03 *}
+%    04 val t = Const ("Build_Inverse_Z_Transform.ZZ_1", 
+%    05   "RealDef.real => RealDef.real => RealDef.real") $
+%    06     (Const (...) $ (Const (...) $ Free (...) $ (Const (...) $ Free (...) 
+% \end{verbatim}}
+% 
+% \noindent The internal representation of the term, as required for
+% rewriting, consists of \textit{Const}ants, a pair of a string
+% \textit{"Groups.plus\_class.plus"} for $+$ and a type, variables
+% \textit{Free} and the respective constructor \textit{\$}. Now the
+% term can be rewritten by the rule-set \textit{inverse\_z}:
+% 
+% {\footnotesize
+% \begin{verbatim}
+%    01 ML {*
+%    02   val SOME (t', asm) = rewrite_set_ @{theory} inverse\_z t;
+%    03   term2str t';
+%    04   terms2str asm;
+%    05 *}
+%    06 val it = "u[n] + </alpha> ^ n * u[n] + </delta>[n]" : string
+%    07 val it = "|| z || > 1 & || z || > </alpha>" : string
+% \end{verbatim}}
+% 
+% \noindent The resulting term \textit{t} and the assumptions
+% \textit{asm} are converted to readable strings by \textit{term2str}
+% and \textit{terms2str}.
+
+\subsection{Preparation of ML-Functions}\label{funs}
+Some functionality required in programming, cannot be accomplished by
+rewriting. So the prototype has a mechanism to call functions within
+the rewrite-engine: certain redexes in Isabelle terms call these
+functions written in SML~\cite{pl:milner97}, the implementation {\em
+and} meta-language of Isabelle. The programmer has to use this
+mechanism.
+
+In the running example's program on p.\pageref{s:impl} the lines {\rm
+05} and {\rm 06} contain such functions; we go into the details with
+\textit{argument\_in X\_z;}. This function fetches the argument from a
+function application: Line {\rm 03} in the example calculation on
+p.\pageref{exp-calc} is created by line {\rm 06} of the example
+program on p.\pageref{s:impl} where the program's environment assigns
+the value \textit{X z} to the variable \textit{X\_z}; so the function
+shall extract the argument \textit{z}.
+
+\medskip In order to be recognised as a function constant in the
+program source the constant needs to be declared in a theory, here in
+\textit{Build\_Inverse\_Z\_Transform.thy}; then it can be parsed in
+the context \textit{ctxt} of that theory:
+
+{\footnotesize
+\begin{verbatim}
+01   consts
+02     argument'_in :: "real => real" ("argument'_in _" 10)
+\end{verbatim}}
+   
+%^3.2^    ML {* val SOME t = parse ctxt "argument_in (X z)"; *}
+%^3.2^    val t = Const ("Build_Inverse_Z_Transform.argument'_in", "RealDef.real ⇒ RealDef.real") 
+%^3.2^              $ (Free ("X", "RealDef.real ⇒ RealDef.real") $ Free ("z", "RealDef.real")): term
+%^3.2^ \end{verbatim}}
+%^3.2^ 
+%^3.2^ \noindent Parsing produces a term \texttt{t} in internal
+%^3.2^ representation~\footnote{The attentive reader realizes the 
+%^3.2^ differences between interal and extermal representation even in the
+%^3.2^ strings, i.e \texttt{'\_}}, consisting of \texttt{Const
+%^3.2^ ("argument'\_in", type)} and the two variables \texttt{Free ("X",
+%^3.2^ type)} and \texttt{Free ("z", type)}, \texttt{\$} is the term
+%^3.2^ constructor. 
+The function body below is implemented directly in SML,
+i.e in an \texttt{ML \{* *\}} block; the function definition provides
+a unique prefix \texttt{eval\_} to the function name:
+
+{\footnotesize
+\begin{verbatim}
+01   ML {*
+02     fun eval_argument_in _ 
+03       "Build_Inverse_Z_Transform.argument'_in" 
+04       (t as (Const ("Build_Inverse_Z_Transform.argument'_in", _) $(f $arg))) _ =
+05         if is_Free arg (*could be something to be simplified before*)
+06         then SOME (term2str t ^"="^ term2str arg, Trueprop $(mk_equality (t, arg)))
+07         else NONE
+08     | eval_argument_in _ _ _ _ = NONE;
+09   *}
+\end{verbatim}}
+
+\noindent The function body creates either \texttt{NONE}
+telling the rewrite-engine to search for the next redex, or creates an
+ad-hoc theorem for rewriting, thus the programmer needs to adopt many
+technicalities of Isabelle, for instance, the \textit{Trueprop}
+constant.
+
+\bigskip This sub-task particularly sheds light on basic issues in the
+design of a programming language, the integration of differential language
+layers, the layer of Isabelle/Isar and Isabelle/ML.
+
+Another point of improvement for the prototype is the rewrite-engine: The
+program on p.\pageref{s:impl} would not allow to contract the two lines {\rm 05}
+and {\rm 06} to
+
+{\small\it\label{s:impl}
+\begin{tabbing}
+123l\=123\=123\=123\=123\=123\=123\=((x\=123\=(x \=123\=123\=\kill
+\>{\rm 05/06}\>\>\>  (z::real) = argument\_in (lhs X\_eq) ;
+\end{tabbing}}
+
+\noindent because nested function calls would require creating redexes
+inside-out; however, the prototype's rewrite-engine only works top down
+from the root of a term down to the leaves.
+
+How all these technicalities are to be checked in the prototype is 
+shown in \S\ref{flow-prep} below.
+
+% \paragraph{Explicit Problems} require explicit methods to solve them, and within
+% this methods we have some explicit steps to do. This steps can be unique for
+% a special problem or refindable in other problems. No mather what case, such
+% steps often require some technical functions behind. For the solving process
+% of the Inverse Z Transformation and the corresponding partial fraction it was
+% neccessary to build helping functions like \texttt{get\_denominator},
+% \texttt{get\_numerator} or \texttt{argument\_in}. First two functions help us
+% to filter the denominator or numerator out of a fraction, last one helps us to
+% get to know the bound variable in a equation.
+% \par
+% By taking \texttt{get\_denominator} as an example, we want to explain how to 
+% implement new functions into the existing system and how we can later use them
+% in our program.
+% 
+% \subsubsection{Find a place to Store the Function}
+% 
+% The whole system builds up on a well defined structure of Knowledge. This
+% Knowledge sets up at the Path:
+% \begin{center}\ttfamily src/Tools/isac/Knowledge\normalfont\end{center}
+% For implementing the Function \texttt{get\_denominator} (which let us extract
+% the denominator out of a fraction) we have choosen the Theory (file)
+% \texttt{Rational.thy}.
+% 
+% \subsubsection{Write down the new Function}
+% 
+% In upper Theory we now define the new function and its purpose:
+% \begin{verbatim}
+%   get_denominator :: "real => real"
+% \end{verbatim}
+% This command tells the machine that a function with the name
+% \texttt{get\_denominator} exists which gets a real expression as argument and
+% returns once again a real expression. Now we are able to implement the function
+% itself, upcoming example now shows the implementation of
+% \texttt{get\_denominator}.
+% 
+% %\begin{example}
+%   \label{eg:getdenom}
+%   \begin{verbatim}
+% 
+% 01  (*
+% 02   *("get_denominator",
+% 03   *  ("Rational.get_denominator", eval_get_denominator ""))
+% 04   *)
+% 05  fun eval_get_denominator (thmid:string) _ 
+% 06            (t as Const ("Rational.get_denominator", _) $
+% 07                (Const ("Rings.inverse_class.divide", _) $num 
+% 08                  $denom)) thy = 
+% 09          SOME (mk_thmid thmid "" 
+% 10              (Print_Mode.setmp [] 
+% 11                (Syntax.string_of_term (thy2ctxt thy)) denom) "", 
+% 12              Trueprop $ (mk_equality (t, denom)))
+% 13    | eval_get_denominator _ _ _ _ = NONE;\end{verbatim}
+% %\end{example}
+% 
+% Line \texttt{07} and \texttt{08} are describing the mode of operation the best -
+% there is a fraction\\ (\ttfamily Rings.inverse\_class.divide\normalfont) 
+% splittet
+% into its two parts (\texttt{\$num \$denom}). The lines before are additionals
+% commands for declaring the function and the lines after are modeling and 
+% returning a real variable out of \texttt{\$denom}.
+% 
+% \subsubsection{Add a test for the new Function}
+% 
+% \paragraph{Everytime when adding} a new function it is essential also to add
+% a test for it. Tests for all functions are sorted in the same structure as the
+% knowledge it self and can be found up from the path:
+% \begin{center}\ttfamily test/Tools/isac/Knowledge\normalfont\end{center}
+% This tests are nothing very special, as a first prototype the functionallity
+% of a function can be checked by evaluating the result of a simple expression
+% passed to the function. Example~\ref{eg:getdenomtest} shows the test for our
+% \textit{just} created function \texttt{get\_denominator}.
+% 
+% %\begin{example}
+% \label{eg:getdenomtest}
+% \begin{verbatim}
+% 
+% 01 val thy = @{theory Isac};
+% 02 val t = term_of (the (parse thy "get_denominator ((a +x)/b)"));
+% 03 val SOME (_, t') = eval_get_denominator "" 0 t thy;
+% 04 if term2str t' = "get_denominator ((a + x) / b) = b" then ()
+% 05 else error "get_denominator ((a + x) / b) = b" \end{verbatim}
+% %\end{example}
+% 
+% \begin{description}
+% \item[01] checks if the proofer set up on our {\sisac{}} System.
+% \item[02] passes a simple expression (fraction) to our suddenly created
+%           function.
+% \item[04] checks if the resulting variable is the correct one (in this case
+%           ``b'' the denominator) and returns.
+% \item[05] handels the error case and reports that the function is not able to
+%           solve the given problem.
+% \end{description}
+
+\subsection{Specification of the Problem}\label{spec}
+%WN <--> \chapter 7 der Thesis
+%WN die Argumentation unten sollte sich NUR auf Verifikation beziehen..
+
+Mechanical treatment requires to translate a textual problem
+description like in Fig.\ref{fig-interactive} on
+p.\pageref{fig-interactive} into a {\em formal} specification. The
+formal specification of the running example could look like is this
+~\footnote{The ``TODO'' in the postcondition indicates, that postconditions
+are not yet handled in the prototype; in particular, the postcondition, i.e.
+the correctness of the result is not yet automatically proved.}:
+
+%WN Hier brauchen wir die Spezifikation des 'running example' ...
+%JR Habe input, output und precond vom Beispiel eingefügt brauche aber Hilfe bei
+%JR der post condition - die existiert für uns ja eigentlich nicht aka
+%JR haben sie bis jetzt nicht beachtet WN...
+%WN2 Mein Vorschlag ist, das TODO zu lassen und deutlich zu kommentieren.
+%JR2 done
+
+\label{eg:neuper2}
+{\small\begin{tabbing}
+  123\=123\=postcond \=: \= $\forall \,A^\prime\, u^\prime \,v^\prime.\,$\=\kill
+  %\hfill \\
+  \>Specification:\\
+  \>  \>input    \>: ${\it filterExpression} \;\;X\;z=\frac{3}{z-\frac{1}{4}+-\frac{1}{8}*\frac{1}{z}}, \;{\it domain}\;\mathbb{R}-\{\frac{1}{2}, \frac{-1}{4}\}$\\
+  \>\>precond  \>: $\frac{3}{z-\frac{1}{4}+-\frac{1}{8}*\frac{1}{z}}\;\; {\it continuous\_on}\; \mathbb{R}-\{\frac{1}{2}, \frac{-1}{4}\}$ \\
+  \>\>output   \>: stepResponse $x[n]$ \\
+  \>\>postcond \>: TODO
+\end{tabbing}}
+
+%JR wie besprochen, kein remark, keine begründung, nur simples "nicht behandelt"
+
+% \begin{remark}
+%    Defining the postcondition requires a high amount mathematical 
+%    knowledge, the difficult part in our case is not to set up this condition 
+%    nor it is more to define it in a way the interpreter is able to handle it. 
+%    Due the fact that implementing that mechanisms is quite the same amount as 
+%    creating the programm itself, it is not avaible in our prototype.
+%    \label{rm:postcond}
+% \end{remark}
+
+The implementation of the formal specification in the present
+prototype, still bar-bones without support for authoring, is done
+like that:
+%WN Kopie von Inverse_Z_Transform.thy, leicht versch"onert:
+
+{\footnotesize\label{exp-spec}
+\begin{verbatim}
+   00 ML {*
+   01  store_specification
+   02    (prepare_specification
+   03      "pbl_SP_Ztrans_inv"
+   04      ["Jan Rocnik"]
+   05      thy
+   06      ( ["Inverse", "Z_Transform", "SignalProcessing"],
+   07        [ ("#Given", ["filterExpression X_eq", "domain D"]),
+   08          ("#Pre"  , ["(rhs X_eq) is_continuous_in D"]),
+   09          ("#Find" , ["stepResponse n_eq"]),
+   10          ("#Post" , [" TODO "])])
+   11        prls
+   12        NONE
+   13        [["SignalProcessing","Z_Transform","Inverse"]]);
+   14 *}
+\end{verbatim}}
+
+Although the above details are partly very technical, we explain them
+in order to document some intricacies of TP-based programming in the
+present state of the {\sisac} prototype:
+\begin{description}
+\item[01..02]\textit{store\_specification:} stores the result of the
+function \textit{prep\_specification} in a global reference
+\textit{Unsynchronized.ref}, which causes principal conflicts with
+Isabelle's asynchronous document model~\cite{Wenzel-11:doc-orient} and
+parallel execution~\cite{Makarius-09:parall-proof} and is under
+reconstruction already.
+
+\textit{prep\_specification:} translates the specification to an internal format
+which allows efficient processing; see for instance line {\rm 07}
+below.
+\item[03..04] are a unique identifier for the specification within {\sisac}
+and the ``mathematics author'' holding the copy-rights.
+\item[05] is the Isabelle \textit{theory} required to parse the
+specification in lines {\rm 07..10}.
+\item[06] is a key into the tree of all specifications as presented to
+the user (where some branches might be hidden by the dialogue
+component).
+\item[07..10] are the specification with input, pre-condition, output
+and post-condition respectively; note that the specification contains
+variables to be instantiated with concrete values for a concrete problem ---
+thus the specification actually captures a class of problems. The post-condition is not handled in
+the prototype presently.
+\item[11] is a rule-set (defined elsewhere) for evaluation of the pre-condition: \textit{(rhs X\_eq) is\_continuous\_in D}, instantiated with the values of a concrete problem, evaluates to true or false --- and all evaluation is done by
+rewriting determined by rule-sets.
+\item[12]\textit{NONE:} could be \textit{SOME ``solve ...''} for a
+problem associated to a function from Computer Algebra (like an
+equation solver) which is not the case here.
+\item[13] is a list of methods solving the specified problem (here
+only one list item) represented analogously to {\rm 06}.
+\end{description}
+
+
+%WN die folgenden Erkl"arungen finden sich durch "grep -r 'datatype pbt' *"
+%WN ...
+%  type pbt = 
+%     {guh  : guh,         (*unique within this isac-knowledge*)
+%      mathauthors: string list, (*copyright*)
+%      init  : pblID,      (*to start refinement with*)
+%      thy   : theory,     (* which allows to compile that pbt
+%			  TODO: search generalized for subthy (ref.p.69*)
+%      (*^^^ WN050912 NOT used during application of the problem,
+%       because applied terms may be from 'subthy' as well as from super;
+%       thus we take 'maxthy'; see match_ags !*)
+%      cas   : term option,(*'CAS-command'*)
+%      prls  : rls,        (* for preds in where_*)
+%      where_: term list,  (* where - predicates*)
+%      ppc   : pat list,
+%      (*this is the model-pattern; 
+%       it contains "#Given","#Where","#Find","#Relate"-patterns
+%       for constraints on identifiers see "fun cpy_nam"*)
+%      met   : metID list}; (* methods solving the pbt*)
+%
+%WN weil dieser Code sehr unaufger"aumt ist, habe ich die Erkl"arungen
+%WN oben selbst geschrieben.
+
+
+
+
+%WN das w"urde ich in \sec\label{progr} verschieben und
+%WN das SubProblem partial fractions zum Erkl"aren verwenden.
+% Such a specification is checked before the execution of a program is
+% started, the same applies for sub-programs. In the following example
+% (Example~\ref{eg:subprob}) shows the call of such a subproblem:
+% 
+% \vbox{
+%   \begin{example}
+%   \label{eg:subprob}
+%   \hfill \\
+%   {\ttfamily \begin{tabbing}
+%   ``(L\_L::bool list) = (\=SubProblem (\=Test','' \\
+%   ``\>\>[linear,univariate,equation,test],'' \\
+%   ``\>\>[Test,solve\_linear])'' \\
+%   ``\>[BOOL equ, REAL z])'' \\
+%   \end{tabbing}
+%   }
+%   {\small\textit{
+%     \noindent If a program requires a result which has to be
+% calculated first we can use a subproblem to do so. In our specific
+% case we wanted to calculate the zeros of a fraction and used a
+% subproblem to calculate the zeros of the denominator polynom.
+%     }}
+%   \end{example}
+% }
+
+\subsection{Implementation of the Method}\label{meth}
+A method collects all data required to interpret a certain program by
+Lucas-Interpretation. The \texttt{program} from p.\pageref{s:impl} of
+the running example is embedded on the last line in the following method:
+%The methods represent the different ways a problem can be solved. This can
+%include mathematical tactics as well as tactics taught in different courses.
+%Declaring the Method itself gives us the possibilities to describe the way of 
+%calculation in deep, as well we get the oppertunities to build in different
+%rulesets.
+
+{\footnotesize
+\begin{verbatim}
+   00 ML {*
+   01  store_method
+   02    (prep_method
+   03      "SP_InverseZTransformation_classic" 
+   04      ["Jan Rocnik"]
+   05      thy 
+   06      ( ["SignalProcessing", "Z_Transform", "Inverse"], 
+   07        [ ("#Given", ["filterExpression X_eq", "domain D"]),
+   08          ("#Pre"  , ["(rhs X_eq) is_continuous_in D"]),
+   09          ("#Find" , ["stepResponse n_eq"]),
+   10        rew_ord  erls
+   11        srls  prls  nrls
+   12        errpats 
+   13        program);
+   14 *}
+\end{verbatim}}
+
+\noindent The above code stores the whole structure analogously to a
+specification as described above:
+\begin{description}
+\item[01..06] are identical to those for the example specification on
+p.\pageref{exp-spec}.
+
+\item[07..09] show something looking like the specification; this is a
+{\em guard}: as long as not all \textit{Given} items are present and
+the \textit{Pre}-conditions is not true, interpretation of the program
+is not started.
+
+\item[10..11] all concern rewriting (the respective data are defined elsewhere): \textit{rew\_ord} is the rewrite order~\cite{nipk:rew-all-that} in case
+\textit{program} contains a \textit{Rewrite} tactic; and in case the respective rule is a conditional rewrite-rule, \textit{erls} features evaluating the conditions. The rule-sets 
+\textit{srls, prls, nrls} feature evaluating (a) the ML-functions in the program (e.g.
+\textit{lhs, argument\_in, rhs} in the program on p.\pageref{s:impl}, (b) the pre-condition analogous to the specification in line 11 on p.\pageref{exp-spec}
+and (c) is required for the derivation-machinery checking user-input formulas.
+
+\item[12..13] \textit{errpats} are error-patterns~\cite{gdaroczy-EP-13} for this method and \textit{program} is the variable holding the example from p.\pageref {s:impl}.
+\end{description}
+The many rule-sets above cause considerable efforts for the
+programmers, in particular, because there are no tools for checking
+essential features of rule-sets.
+
+% is again very technical and goes hard in detail. Unfortunataly
+% most declerations are not essential for a basic programm but leads us to a huge
+% range of powerful possibilities.
+% 
+% \begin{description}
+% \item[01..02] stores the method with the given name into the system under a global
+% reference.
+% \item[03] specifies the topic within which context the method can be found.
+% \item[04..05] as the requirements for different methods can be deviant we 
+% declare what is \emph{given} and and what to \emph{find} for this specific method.
+% The code again helds on the topic of the case studie, where the inverse 
+% z-transformation does a switch between a term describing a electrical filter into
+% its step response. Also the datatype has to be declared (bool - due the fact that 
+% we handle equations).
+% \item[06] \emph{rewrite order} is the order of this rls (ruleset), where one 
+% theorem of it is used for rewriting one single step.
+% \item[07] \texttt{rls} is the currently used ruleset for this method. This set
+% has already been defined before.
+% \item[08] we would have the possiblitiy to add this method to a predefined tree of
+% calculations, i.eg. if it would be a sub of a bigger problem, here we leave it
+% independend.
+% \item[09] The \emph{source ruleset}, can be used to evaluate list expressions in 
+% the source.
+% \item[10] \emph{predicates ruleset} can be used to indicates predicates within 
+% model patterns.
+% \item[11] The \emph{check ruleset} summarizes rules for checking formulas 
+% elementwise.
+% \item[12] \emph{error patterns} which are expected in this kind of method can be
+% pre-specified to recognize them during the method.
+% \item[13] finally the \emph{canonical ruleset}, declares the canonical simplifier 
+% of the specific method.
+% \item[14] for this code snipset we don't specify the programm itself and keep it 
+% empty. Follow up \S\ref{progr} for informations on how to implement this
+% \textit{main} part.
+% \end{description}
+
+\subsection{Implementation of the TP-based Program}\label{progr} 
+So finally all the prerequisites are described and the final task can
+be addressed. The program below comes back to the running example: it
+computes a solution for the problem from Fig.\ref{fig-interactive} on
+p.\pageref{fig-interactive}. The reader is reminded of
+\S\ref{PL-isab}, the introduction of the programming language:
+
+{\footnotesize\it\label{s:impl}
+\begin{tabbing}
+123l\=123\=123\=123\=123\=123\=123\=((x\=123\=(x \=123\=123\=\kill
+\>{\rm 00}\>ML \{*\\
+\>{\rm 00}\>val program =\\
+\>{\rm 01}\>  "{\tt Program} InverseZTransform (X\_eq::bool) =   \\
+\>{\rm 02}\>\>  {\tt let}                                       \\
+\>{\rm 03}\>\>\>  X\_eq = {\tt Take} X\_eq ;   \\
+\>{\rm 04}\>\>\>  X\_eq = {\tt Rewrite} prep\_for\_part\_frac X\_eq ; \\
+\>{\rm 05}\>\>\>  (X\_z::real) = lhs X\_eq ;       \\ %no inside-out evaluation
+\>{\rm 06}\>\>\>  (z::real) = argument\_in X\_z; \\
+\>{\rm 07}\>\>\>  (part\_frac::real) = {\tt SubProblem} \\
+\>{\rm 08}\>\>\>\>\>\>\>\>  ( Isac, [partial\_fraction, rational, simplification], [] )\\
+%\>{\rm 10}\>\>\>\>\>\>\>\>\>  [simplification, of\_rationals, to\_partial\_fraction] ) \\
+\>{\rm 09}\>\>\>\>\>\>\>\>  [ (rhs X\_eq)::real, z::real ]; \\
+\>{\rm 10}\>\>\>  (X'\_eq::bool) = {\tt Take} ((X'::real =$>$ bool) z = ZZ\_1 part\_frac) ; \\
+\>{\rm 11}\>\>\>  X'\_eq = (({\tt Rewrite\_Set} prep\_for\_inverse\_z) @@   \\
+\>{\rm 12}\>\>\>\>\>  $\;\;$ ({\tt Rewrite\_Set} inverse\_z)) X'\_eq \\
+\>{\rm 13}\>\>  {\tt in } \\
+\>{\rm 14}\>\>\>  X'\_eq"\\
+\>{\rm 15}\>*\}
+\end{tabbing}}
+% ORIGINAL FROM Inverse_Z_Transform.thy
+% "Script InverseZTransform (X_eq::bool) =            "^(*([], Frm), Problem (Isac, [Inverse, Z_Transform, SignalProcessing])*)
+% "(let X = Take X_eq;                                "^(*([1], Frm), X z = 3 / (z - 1 / 4 + -1 / 8 * (1 / z))*)
+% "  X' = Rewrite ruleZY False X;                     "^(*([1], Res), ?X' z = 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))*)
+% "  (X'_z::real) = lhs X';                           "^(*            ?X' z*)
+% "  (zzz::real) = argument_in X'_z;                  "^(*            z *)
+% "  (funterm::real) = rhs X';                        "^(*            3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))*)
+%
+% "  (pbz::real) = (SubProblem (Isac',                "^(**)
+% "    [partial_fraction,rational,simplification],    "^
+% "    [simplification,of_rationals,to_partial_fraction]) "^
+% "    [REAL funterm, REAL zzz]);                     "^(*([2], Res), 4 / (z - 1 / 2) + -4 / (z - -1 / 4)*)
+%
+% "  (pbz_eq::bool) = Take (X'_z = pbz);              "^(*([3], Frm), ?X' z = 4 / (z - 1 / 2) + -4 / (z - -1 / 4)*)
+% "  pbz_eq = Rewrite ruleYZ False pbz_eq;            "^(*([3], Res), ?X' z = 4 * (?z / (z - 1 / 2)) + -4 * (?z / (z - -1 / 4))*)
+% "  pbz_eq = drop_questionmarks pbz_eq;              "^(*               4 * (z / (z - 1 / 2)) + -4 * (z / (z - -1 / 4))*)
+% "  (X_zeq::bool) = Take (X_z = rhs pbz_eq);         "^(*([4], Frm), X_z = 4 * (z / (z - 1 / 2)) + -4 * (z / (z - -1 / 4))*)
+% "  n_eq = (Rewrite_Set inverse_z False) X_zeq;      "^(*([4], Res), X_z = 4 * (1 / 2) ^^^ ?n * ?u [?n] + -4 * (-1 / 4) ^^^ ?n * ?u [?n]*)
+% "  n_eq = drop_questionmarks n_eq                   "^(*            X_z = 4 * (1 / 2) ^^^ n * u [n] + -4 * (-1 / 4) ^^^ n * u [n]*)
+% "in n_eq)"                                            (*([], Res), X_z = 4 * (1 / 2) ^^^ n * u [n] + -4 * (-1 / 4) ^^^ n * u [n]*)
+The program is represented as a string and part of the method in
+\S\ref{meth}.  As mentioned in \S\ref{PL} the program is purely
+functional and lacks any input statements and output statements. So
+the steps of calculation towards a solution (and interactive tutoring
+in step-wise problem solving) are created as a side-effect by
+Lucas-Interpretation.  The side-effects are triggered by the tactics
+\texttt{Take}, \texttt{Rewrite}, \texttt{SubProblem} and
+\texttt{Rewrite\_Set} in the above lines {\rm 03, 04, 07, 10, 11} and
+{\rm 12} respectively. These tactics produce the respective lines in the
+calculation on p.\pageref{flow-impl}.
+
+The above lines {\rm 05, 06} do not contain a tactics, so they do not
+immediately contribute to the calculation on p.\pageref{flow-impl};
+rather, they compute actual arguments for the \texttt{SubProblem} in
+line {\rm 09}~\footnote{The tactics also are break-points for the
+interpreter, where control is handed over to the user in interactive
+tutoring.}. Line {\rm 11} contains tactical \textit{@@}.
+
+\medskip The above program also indicates the dominant role of interactive
+selection of knowledge in the three-dimensional universe of
+mathematics. The \texttt{SubProblem} in the above lines
+{\rm 07..09} is more than a function call with the actual arguments
+\textit{[ (rhs X\_eq)::real, z::real ]}. The programmer has to determine
+three items:
+
+\begin{enumerate}
+\item the theory, in the example \textit{Isac} because different
+methods can be selected in Pt.3 below, which are defined in different
+theories with \textit{Isac} collecting them.
+\item the specification identified by \textit{[partial\_fraction,
+rational, simplification]} in the tree of specifications; this
+specification is analogous to the specification of the main program
+described in \S\ref{spec}; the problem is to find a ``partial fraction
+decomposition'' for a univariate rational polynomial.
+\item the method in the above example is \textit{[ ]}, i.e. empty,
+which supposes the interpreter to select one of the methods predefined
+in the specification, for instance in line {\rm 13} in the running
+example's specification on p.\pageref{exp-spec}~\footnote{The freedom
+(or obligation) for selection carries over to the student in
+interactive tutoring.}.
+\end{enumerate}
+
+The program code, above presented as a string, is parsed by Isabelle's
+parser --- the program is an Isabelle term. This fact is expected to
+simplify verification tasks in the future; on the other hand, this
+fact causes troubles in error detection which are discussed as part
+of the work-flow in the subsequent section.
+
+\section{Work-flow of Programming in the Prototype}\label{workflow}
+The new prover IDE Isabelle/jEdit~\cite{makar-jedit-12} is a great
+step forward for interactive theory and proof development. The
+{\sisac}-prototype re-uses this IDE as a programming environment.  The
+experiences from this re-use show, that the essential components are
+available from Isabelle/jEdit. However, additional tools and features
+are required to achieve acceptable usability.
+
+So notable experiences are reported here, also as a requirement
+capture for further development of TP-based languages and respective
+IDEs.
+
+\subsection{Preparations and Trials}\label{flow-prep}
+The many sub-tasks to be accomplished {\em before} the first line of
+program code can be written and tested suggest an approach which
+step-wise establishes the prerequisites. The case study underlying
+this paper~\cite{jrocnik-bakk} documents the approach in a separate
+Isabelle theory,
+\textit{Build\_Inverse\_Z\_Transform.thy}~\footnote{http://www.ist.tugraz.at/projects/isac/publ/Build\_Inverse\_Z\_Transform.thy}. Part
+II in the study comprises this theory, \LaTeX ed from the theory by
+use of Isabelle's document preparation system. This paper resembles
+the approach in \S\ref{isabisac} to \S\ref{meth}, which in actual
+implementation work involves several iterations.
+
+\bigskip For instance, only the last step, implementing the program
+described in \S\ref{meth}, reveals details required. Let us assume,
+this is the ML-function \textit{argument\_in} required in line {\rm 06}
+of the example program on p.\pageref{s:impl}; how this function needs
+to be implemented in the prototype has been discussed in \S\ref{funs}
+already.
+
+Now let us assume, that calling this function from the program code
+does not work; so testing this function is required in order to find out
+the reason: type errors, a missing entry of the function somewhere or
+even more nasty technicalities \dots
+
+{\footnotesize
+\begin{verbatim}
+01   ML {*
+02     val SOME t = parseNEW ctxt "argument_in (X (z::real))";
+03     val SOME (str, t') = eval_argument_in "" 
+04       "Build_Inverse_Z_Transform.argument'_in" t 0;
+05     term2str t';
+06   *}
+07   val it = "(argument_in X z) = z": string\end{verbatim}}
+
+\noindent So, this works: we get an ad-hoc theorem, which used in
+rewriting would reduce \texttt{argument\_in X z} to \texttt{z}. Now we check this
+reduction and create a rule-set \texttt{rls} for that purpose:
+
+{\footnotesize
+\begin{verbatim}
+01   ML {*
+02     val rls = append_rls "test" e_rls 
+03       [Calc ("Build_Inverse_Z_Transform.argument'_in", eval_argument_in "")]
+04     val SOME (t', asm) = rewrite_set_ @{theory} rls t;
+05   *}
+06   val t' = Free ("z", "RealDef.real"): term
+07   val asm = []: term list\end{verbatim}}
+
+\noindent The resulting term \texttt{t'} is \texttt{Free ("z",
+"RealDef.real")}, i.e the variable \texttt{z}, so all is
+perfect. Probably we have forgotten to store this function correctly~?
+We review the respective \texttt{calclist} (again an
+\textit{Unsynchronized.ref} to be removed in order to adjust to
+Isabelle/Isar's asynchronous document model):
+
+{\footnotesize
+\begin{verbatim}
+01   calclist:= overwritel (! calclist, 
+02    [("argument_in",
+03     ("Build_Inverse_Z_Transform.argument'_in", eval_argument_in "")),
+04       ...
+05    ]);\end{verbatim}}
+
+\noindent The entry is perfect. So what is the reason~? Ah, probably there
+is something messed up with the many rule-sets in the method, see \S\ref{meth} ---
+right, the function \texttt{argument\_in} is not contained in the respective
+rule-set \textit{srls} \dots this just as an example of the intricacies in
+debugging a program in the present state of the prototype.
+
+\subsection{Implementation in Isabelle/{\isac}}\label{flow-impl}
+Given all the prerequisites from \S\ref{isabisac} to \S\ref{meth},
+usually developed within several iterations, the program can be
+assembled; on p.\pageref{s:impl} there is the complete program of the
+running example.
+
+The completion of this program required efforts for several weeks
+(after some months of familiarisation with {\sisac}), caused by the
+abundance of intricacies indicated above. Also writing the program is
+not pleasant, given Isabelle/Isar/ without add-ons for
+programming. Already writing and parsing a few lines of program code
+is a challenge: the program is an Isabelle term; Isabelle's parser,
+however, is not meant for huge terms like the program of the running
+example. So reading out the specific error (usually type errors) from
+Isabelle's message is difficult.
+
+\medskip Testing the evaluation of the program has to rely on very
+simple tools. Step-wise execution is modeled by a function
+\texttt{me}, short for mathematics-engine~\footnote{The interface used
+by the front-end which created the calculation on
+p.\pageref{fig-interactive} is different from this function}:
+%the following is a simplification of the actual function 
+
+{\footnotesize
+\begin{verbatim}
+01   ML {* me; *}
+02   val it = tac -> ctree * pos -> mout * tac * ctree * pos\end{verbatim}} 
+
+\noindent This function takes as arguments a tactic \texttt{tac} which
+determines the next step, the step applied to the interpreter-state
+\texttt{ctree * pos} as last argument taken. The interpreter-state is
+a pair of a tree \texttt{ctree} representing the calculation created
+(see the example below) and a position \texttt{pos} in the
+calculation. The function delivers a quadruple, beginning with the new
+formula \texttt{mout} and the next tactic followed by the new
+interpreter-state.
+
+This function allows to stepwise check the program:
+
+{\footnotesize\label{ml-check-program}
+\begin{verbatim}
+01   ML {*
+02     val fmz =
+03       ["filterExpression (X z = 3 / ((z::real) + 1/10 - 1/50*(1/z)))",
+04        "stepResponse (x[n::real]::bool)"];     
+05     val (dI,pI,mI) =
+06       ("Isac", 
+07        ["Inverse", "Z_Transform", "SignalProcessing"], 
+08        ["SignalProcessing","Z_Transform","Inverse"]);
+09     val (mout, tac, ctree, pos)  = CalcTreeTEST [(fmz, (dI, pI, mI))];
+10     val (mout, tac, ctree, pos)  = me tac (ctree, pos);
+11     val (mout, tac, ctree, pos)  = me tac (ctree, pos);
+12     val (mout, tac, ctree, pos)  = me tac (ctree, pos);
+13     ...
+\end{verbatim}} 
+
+\noindent Several dozens of calls for \texttt{me} are required to
+create the lines in the calculation below (including the sub-problems
+not shown). When an error occurs, the reason might be located
+many steps before: if evaluation by rewriting, as done by the prototype,
+fails, then first nothing happens --- the effects come later and
+cause unpleasant checks.
+
+The checks comprise watching the rewrite-engine for many different
+kinds of rule-sets (see \S\ref{meth}), the interpreter-state, in
+particular the environment and the context at the states position ---
+all checks have to rely on simple functions accessing the
+\texttt{ctree}. So getting the calculation below (which resembles the
+calculation in Fig.\ref{fig-interactive} on p.\pageref{fig-interactive})
+is the result of several weeks of development:
+
+{\small\it\label{exp-calc}
+\begin{tabbing}
+123l\=123\=123\=123\=123\=123\=123\=123\=123\=123\=123\=123\=\kill
+\>{\rm 01}\> $\bullet$  \> {\tt Problem } (Inverse\_Z\_Transform, [Inverse, Z\_Transform, SignalProcessing])       \`\\
+\>{\rm 02}\>\> $\vdash\;\;X z = \frac{3}{z - \frac{1}{4} - \frac{1}{8} \cdot z^{-1}}$       \`{\footnotesize {\tt Take} X\_eq}\\
+\>{\rm 03}\>\> $X z = \frac{3}{z + \frac{-1}{4} + \frac{-1}{8} \cdot \frac{1}{z}}$          \`{\footnotesize {\tt Rewrite} prep\_for\_part\_frac X\_eq}\\
+\>{\rm 04}\>\> $\bullet$\> {\tt Problem } [partial\_fraction,rational,simplification]        \`{\footnotesize {\tt SubProblem} \dots}\\
+\>{\rm 05}\>\>\>  $\vdash\;\;\frac{3}{z + \frac{-1}{4} + \frac{-1}{8} \cdot \frac{1}{z}}=$    \`- - -\\
+\>{\rm 06}\>\>\>  $\frac{24}{-1 + -2 \cdot z + 8 \cdot z^2}$                                   \`- - -\\
+\>{\rm 07}\>\>\>  $\bullet$\> solve ($-1 + -2 \cdot z + 8 \cdot z^2,\;z$ )                      \`- - -\\
+\>{\rm 08}\>\>\>\>   $\vdash$ \> $\frac{3}{z + \frac{-1}{4} + \frac{-1}{8} \cdot \frac{1}{z}}=0$ \`- - -\\
+\>{\rm 09}\>\>\>\>   $z = \frac{2+\sqrt{-4+8}}{16}\;\lor\;z = \frac{2-\sqrt{-4+8}}{16}$           \`- - -\\
+\>{\rm 10}\>\>\>\>   $z = \frac{1}{2}\;\lor\;z =$ \_\_\_                                           \`- - -\\
+\>        \>\>\>\>   \_\_\_                                                                        \`- - -\\
+\>{\rm 11}\>\> \dots\> $\frac{4}{z - \frac{1}{2}} + \frac{-4}{z - \frac{-1}{4}}$                   \`\\
+\>{\rm 12}\>\> $X^\prime z = {\cal z}^{-1} (\frac{4}{z - \frac{1}{2}} + \frac{-4}{z - \frac{-1}{4}})$ \`{\footnotesize {\tt Take} ((X'::real =$>$ bool) z = ZZ\_1 part\_frac)}\\
+\>{\rm 13}\>\> $X^\prime z = {\cal z}^{-1} (4\cdot\frac{z}{z - \frac{1}{2}} + -4\cdot\frac{z}{z - \frac{-1}{4}})$ \`{\footnotesize{\tt Rewrite\_Set} prep\_for\_inverse\_z X'\_eq }\\
+\>{\rm 14}\>\> $X^\prime z = 4\cdot(\frac{1}{2})^n \cdot u [n] + -4\cdot(\frac{-1}{4})^n \cdot u [n]$  \`{\footnotesize {\tt Rewrite\_Set} inverse\_z X'\_eq}\\
+\>{\rm 15}\> \dots\> $X^\prime z = 4\cdot(\frac{1}{2})^n \cdot u [n] + -4\cdot(\frac{-1}{4})^n \cdot u [n]$ \`{\footnotesize {\tt Check\_Postcond}}
+\end{tabbing}}
+The tactics on the right margin of the above calculation are those in
+the program on p.\pageref{s:impl} which create the respective formulas
+on the left.
+% ORIGINAL FROM Inverse_Z_Transform.thy
+%    "Script InverseZTransform (X_eq::bool) =            "^(*([], Frm), Problem (Isac, [Inverse, Z_Transform, SignalProcessing])*)
+%    "(let X = Take X_eq;                                "^(*([1], Frm), X z = 3 / (z - 1 / 4 + -1 / 8 * (1 / z))*)
+%    "  X' = Rewrite ruleZY False X;                     "^(*([1], Res), ?X' z = 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))*)
+%    "  (X'_z::real) = lhs X';                           "^(*            ?X' z*)
+%    "  (zzz::real) = argument_in X'_z;                  "^(*            z *)
+%    "  (funterm::real) = rhs X';                        "^(*            3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))*)
+% 
+%    "  (pbz::real) = (SubProblem (Isac',                "^(**)
+%    "    [partial_fraction,rational,simplification],    "^
+%    "    [simplification,of_rationals,to_partial_fraction]) "^
+%    "    [REAL funterm, REAL zzz]);                     "^(*([2], Res), 4 / (z - 1 / 2) + -4 / (z - -1 / 4)*)
+% 
+%    "  (pbz_eq::bool) = Take (X'_z = pbz);              "^(*([3], Frm), ?X' z = 4 / (z - 1 / 2) + -4 / (z - -1 / 4)*)
+%    "  pbz_eq = Rewrite ruleYZ False pbz_eq;            "^(*([3], Res), ?X' z = 4 * (?z / (z - 1 / 2)) + -4 * (?z / (z - -1 / 4))*)
+%    "  pbz_eq = drop_questionmarks pbz_eq;              "^(*               4 * (z / (z - 1 / 2)) + -4 * (z / (z - -1 / 4))*)
+%    "  (X_zeq::bool) = Take (X_z = rhs pbz_eq);         "^(*([4], Frm), X_z = 4 * (z / (z - 1 / 2)) + -4 * (z / (z - -1 / 4))*)
+%    "  n_eq = (Rewrite_Set inverse_z False) X_zeq;      "^(*([4], Res), X_z = 4 * (1 / 2) ^^^ ?n * ?u [?n] + -4 * (-1 / 4) ^^^ ?n * ?u [?n]*)
+%    "  n_eq = drop_questionmarks n_eq                   "^(*            X_z = 4 * (1 / 2) ^^^ n * u [n] + -4 * (-1 / 4) ^^^ n * u [n]*)
+%    "in n_eq)"                                            (*([], Res), X_z = 4 * (1 / 2) ^^^ n * u [n] + -4 * (-1 / 4) ^^^ n * u [n]*)
+
+\subsection{Transfer into the Isabelle/{\isac} Knowledge}\label{flow-trans}
+Finally \textit{Build\_Inverse\_Z\_Transform.thy} has got the job done
+and the knowledge accumulated in it can be distributed to appropriate
+theories: the program to \textit{Inverse\_Z\_Transform.thy}, the
+sub-problem accomplishing the partial fraction decomposition to
+\textit{Partial\_Fractions.thy}. Since there are hacks into Isabelle's
+internals, this kind of distribution is not trivial. For instance, the
+function \texttt{argument\_in} in \S\ref{funs} explicitly contains a
+string with the theory it has been defined in, so this string needs to
+be updated from \texttt{Build\_Inverse\_Z\_Transform} to
+\texttt{Atools} if that function is transferred to theory
+\textit{Atools.thy}.
+
+In order to obtain the functionality presented in Fig.\ref{fig-interactive} on p.\pageref{fig-interactive} data must be exported from SML-structures to XML.
+This process is also rather bare-bones without authoring tools and is
+described in detail in the {\sisac} wiki~\footnote{http://www.ist.tugraz.at/isac/index.php/Generate\_representations\_for\_ISAC\_Knowledge}.
+
+% \newpage
+% -------------------------------------------------------------------
+% 
+% Material, falls noch Platz bleibt ...
+% 
+% -------------------------------------------------------------------
+% 
+% 
+% \subsubsection{Trials on Notation and Termination}
+% 
+% \paragraph{Technical notations} are a big problem for our piece of software,
+% but the reason for that isn't a fault of the software itself, one of the
+% troubles comes out of the fact that different technical subtopics use different
+% symbols and notations for a different purpose. The most famous example for such
+% a symbol is the complex number $i$ (in cassique math) or $j$ (in technical
+% math). In the specific part of signal processing one of this notation issues is
+% the use of brackets --- we use round brackets for analoge signals and squared
+% brackets for digital samples. Also if there is no problem for us to handle this
+% fact, we have to tell the machine what notation leads to wich meaning and that
+% this purpose seperation is only valid for this special topic - signal
+% processing.
+% \subparagraph{In the programming language} itself it is not possible to declare
+% fractions, exponents, absolutes and other operators or remarks in a way to make
+% them pretty to read; our only posssiblilty were ASCII characters and a handfull
+% greek symbols like: $\alpha, \beta, \gamma, \phi,\ldots$.
+% \par
+% With the upper collected knowledge it is possible to check if we were able to
+% donate all required terms and expressions.
+% 
+% \subsubsection{Definition and Usage of Rules}
+% 
+% \paragraph{The core} of our implemented problem is the Z-Transformation, due
+% the fact that the transformation itself would require higher math which isn't
+% yet avaible in our system we decided to choose the way like it is applied in
+% labratory and problem classes at our university - by applying transformation
+% rules (collected in transformation tables).
+% \paragraph{Rules,} in {\sisac{}}'s programming language can be designed by the
+% use of axiomatizations like shown in Example~\ref{eg:ruledef}
+% 
+% \begin{example}
+%   \label{eg:ruledef}
+%   \hfill\\
+%   \begin{verbatim}
+%   axiomatization where
+%     rule1: ``1 = $\delta$[n]'' and
+%     rule2: ``|| z || > 1 ==> z / (z - 1) = u [n]'' and
+%     rule3: ``|| z || < 1 ==> z / (z - 1) = -u [-n - 1]''
+%   \end{verbatim}
+% \end{example}
+% 
+% This rules can be collected in a ruleset and applied to a given expression as
+% follows in Example~\ref{eg:ruleapp}.
+% 
+% \begin{example}
+%   \hfill\\
+%   \label{eg:ruleapp}
+%   \begin{enumerate}
+%   \item Store rules in ruleset:
+%   \begin{verbatim}
+%   val inverse_Z = append_rls "inverse_Z" e_rls
+%     [ Thm ("rule1",num_str @{thm rule1}),
+%       Thm ("rule2",num_str @{thm rule2}),
+%       Thm ("rule3",num_str @{thm rule3})
+%     ];\end{verbatim}
+%   \item Define exression:
+%   \begin{verbatim}
+%   val sample_term = str2term "z/(z-1)+z/(z-</delta>)+1";\end{verbatim}
+%   \item Apply ruleset:
+%   \begin{verbatim}
+%   val SOME (sample_term', asm) = 
+%     rewrite_set_ thy true inverse_Z sample_term;\end{verbatim}
+%   \end{enumerate}
+% \end{example}
+% 
+% The use of rulesets makes it much easier to develop our designated applications,
+% but the programmer has to be careful and patient. When applying rulesets
+% two important issues have to be mentionend:
+% \subparagraph{How often} the rules have to be applied? In case of
+% transformations it is quite clear that we use them once but other fields
+% reuqire to apply rules until a special condition is reached (e.g.
+% a simplification is finished when there is nothing to be done left).
+% \subparagraph{The order} in which rules are applied often takes a big effect
+% and has to be evaluated for each purpose once again.
+% \par
+% In our special case of Signal Processing and the rules defined in
+% Example~\ref{eg:ruledef} we have to apply rule~1 first of all to transform all
+% constants. After this step has been done it no mather which rule fit's next.
+% 
+% \subsubsection{Helping Functions}
+% 
+% \paragraph{New Programms require,} often new ways to get through. This new ways
+% means that we handle functions that have not been in use yet, they can be 
+% something special and unique for a programm or something famous but unneeded in
+% the system yet. In our dedicated example it was for example neccessary to split
+% a fraction into numerator and denominator; the creation of such function and
+% even others is described in upper Sections~\ref{simp} and \ref{funs}.
+% 
+% \subsubsection{Trials on equation solving}
+% %simple eq and problem with double fractions/negative exponents
+% \paragraph{The Inverse Z-Transformation} makes it neccessary to solve
+% equations degree one and two. Solving equations in the first degree is no 
+% problem, wether for a student nor for our machine; but even second degree
+% equations can lead to big troubles. The origin of this troubles leads from
+% the build up process of our equation solving functions; they have been
+% implemented some time ago and of course they are not as good as we want them to
+% be. Wether or not following we only want to show how cruel it is to build up new
+% work on not well fundamentials.
+% \subparagraph{A simple equation solving,} can be set up as shown in the next
+% example:
+% 
+% \begin{example}
+% \begin{verbatim}
+%   
+%   val fmz =
+%     ["equality (-1 + -2 * z + 8 * z ^^^ 2 = (0::real))",
+%      "solveFor z",
+%      "solutions L"];                                    
+% 
+%   val (dI',pI',mI') =
+%     ("Isac", 
+%       ["abcFormula","degree_2","polynomial","univariate","equation"],
+%       ["no_met"]);\end{verbatim}
+% \end{example}
+% 
+% Here we want to solve the equation: $-1+-2\cdot z+8\cdot z^{2}=0$. (To give
+% a short overview on the commands; at first we set up the equation and tell the
+% machine what's the bound variable and where to store the solution. Second step 
+% is to define the equation type and determine if we want to use a special method
+% to solve this type.) Simple checks tell us that the we will get two results for
+% this equation and this results will be real.
+% So far it is easy for us and for our machine to solve, but
+% mentioned that a unvariate equation second order can have three different types
+% of solutions it is getting worth.
+% \subparagraph{The solving of} all this types of solutions is not yet supported.
+% Luckily it was needed for us; but something which has been needed in this 
+% context, would have been the solving of an euation looking like:
+% $-z^{-2}+-2\cdot z^{-1}+8=0$ which is basically the same equation as mentioned
+% before (remember that befor it was no problem to handle for the machine) but
+% now, after a simple equivalent transformation, we are not able to solve
+% it anymore.
+% \subparagraph{Error messages} we get when we try to solve something like upside
+% were very confusing and also leads us to no special hint about a problem.
+% \par The fault behind is, that we have no well error handling on one side and
+% no sufficient formed equation solving on the other side. This two facts are
+% making the implemention of new material very difficult.
+% 
+% \subsection{Formalization of missing knowledge in Isabelle}
+% 
+% \paragraph{A problem} behind is the mechanization of mathematic
+% theories in TP-bases languages. There is still a huge gap between
+% these algorithms and this what we want as a solution - in Example
+% Signal Processing. 
+% 
+% \vbox{
+%   \begin{example}
+%     \label{eg:gap}
+%     \[
+%       X\cdot(a+b)+Y\cdot(c+d)=aX+bX+cY+dY
+%     \]
+%     {\small\textit{
+%       \noindent A very simple example on this what we call gap is the
+% simplification above. It is needles to say that it is correct and also
+% Isabelle for fills it correct - \emph{always}. But sometimes we don't
+% want expand such terms, sometimes we want another structure of
+% them. Think of a problem were we now would need only the coefficients
+% of $X$ and $Y$. This is what we call the gap between mechanical
+% simplification and the solution.
+%     }}
+%   \end{example}
+% }
+% 
+% \paragraph{We are not able to fill this gap,} until we have to live
+% with it but first have a look on the meaning of this statement:
+% Mechanized math starts from mathematical models and \emph{hopefully}
+% proceeds to match physics. Academic engineering starts from physics
+% (experimentation, measurement) and then proceeds to mathematical
+% modeling and formalization. The process from a physical observance to
+% a mathematical theory is unavoidable bound of setting up a big
+% collection of standards, rules, definition but also exceptions. These
+% are the things making mechanization that difficult.
+% 
+% \vbox{
+%   \begin{example}
+%     \label{eg:units}
+%     \[
+%       m,\ kg,\ s,\ldots
+%     \]
+%     {\small\textit{
+%       \noindent Think about some units like that one's above. Behind
+% each unit there is a discerning and very accurate definition: One
+% Meter is the distance the light travels, in a vacuum, through the time
+% of 1 / 299.792.458 second; one kilogram is the weight of a
+% platinum-iridium cylinder in paris; and so on. But are these
+% definitions usable in a computer mechanized world?!
+%     }}
+%   \end{example}
+% }
+% 
+% \paragraph{A computer} or a TP-System builds on programs with
+% predefined logical rules and does not know any mathematical trick
+% (follow up example \ref{eg:trick}) or recipe to walk around difficult
+% expressions. 
+% 
+% \vbox{
+%   \begin{example}
+%     \label{eg:trick}
+%   \[ \frac{1}{j\omega}\cdot\left(e^{-j\omega}-e^{j3\omega}\right)= \]
+%   \[ \frac{1}{j\omega}\cdot e^{-j2\omega}\cdot\left(e^{j\omega}-e^{-j\omega}\right)=
+%      \frac{1}{\omega}\, e^{-j2\omega}\cdot\colorbox{lgray}{$\frac{1}{j}\,\left(e^{j\omega}-e^{-j\omega}\right)$}= \]
+%   \[ \frac{1}{\omega}\, e^{-j2\omega}\cdot\colorbox{lgray}{$2\, sin(\omega)$} \]
+%     {\small\textit{
+%       \noindent Sometimes it is also useful to be able to apply some
+% \emph{tricks} to get a beautiful and particularly meaningful result,
+% which we are able to interpret. But as seen in this example it can be
+% hard to find out what operations have to be done to transform a result
+% into a meaningful one.
+%     }}
+%   \end{example}
+% }
+% 
+% \paragraph{The only possibility,} for such a system, is to work
+% through its known definitions and stops if none of these
+% fits. Specified on Signal Processing or any other application it is
+% often possible to walk through by doing simple creases. This creases
+% are in general based on simple math operational but the challenge is
+% to teach the machine \emph{all}\footnote{Its pride to call it
+% \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
+% survey of knowledge which links to other knowledge and {{\sisac}{}} a
+% trainer and helper but no human compensating calculator. 
+% \par
+% {{{\sisac}{}}} itself aims to adds \emph{Algorithmic Knowledge} (formal
+% specifications of problems out of topics from Signal Processing, etc.)
+% and \emph{Application-oriented Knowledge} to the \emph{deductive} axis of
+% physical knowledge. The result is a three-dimensional universe of
+% mathematics seen in Figure~\ref{fig:mathuni}.
+% 
+% \begin{figure}
+%   \begin{center}
+%     \includegraphics{fig/universe}
+%     \caption{Didactic ``Math-Universe'': Algorithmic Knowledge (Programs) is
+%              combined with Application-oriented Knowledge (Specifications) and Deductive Knowledge (Axioms, Definitions, Theorems). The Result
+%              leads to a three dimensional math universe.\label{fig:mathuni}}
+%   \end{center}
+% \end{figure}
+% 
+% %WN Deine aktuelle Benennung oben wird Dir kein Fachmann abnehmen;
+% %WN bitte folgende Bezeichnungen nehmen:
+% %WN 
+% %WN axis 1: Algorithmic Knowledge (Programs)
+% %WN axis 2: Application-oriented Knowledge (Specifications)
+% %WN axis 3: Deductive Knowledge (Axioms, Definitions, Theorems)
+% %WN 
+% %WN und bitte die R"ander von der Grafik wegschneiden (was ich f"ur *.pdf
+% %WN nicht hinkriege --- weshalb ich auch die eJMT-Forderung nicht ganz
+% %WN verstehe, separierte PDFs zu schicken; ich w"urde *.png schicken)
+% 
+% %JR Ränder und beschriftung geändert. Keine Ahnung warum eJMT sich pdf's
+% %JR wünschen, würde ebenfalls png oder ähnliches verwenden, aber wenn pdf's
+% %JR gefordert werden WN2...
+% %WN2 meiner Meinung nach hat sich eJMT unklar ausgedr"uckt (z.B. kann
+% %WN2 man meines Wissens pdf-figures nicht auf eine bestimmte Gr"osse
+% %WN2 zusammenschneiden um die R"ander weg zu bekommen)
+% %WN2 Mein Vorschlag ist, in umserem tex-file bei *.png zu bleiben und
+% %WN2 png + pdf figures mitzuschicken.
+% 
+% \subsection{Notes on Problems with Traditional Notation}
+% 
+% \paragraph{During research} on these topic severely problems on
+% traditional notations have been discovered. Some of them have been
+% known in computer science for many years now and are still unsolved,
+% one of them aggregates with the so called \emph{Lambda Calculus},
+% Example~\ref{eg:lamda} provides a look on the problem that embarrassed
+% us.
+% 
+% \vbox{
+%   \begin{example}
+%     \label{eg:lamda}
+% 
+%   \[ f(x)=\ldots\;  \quad R \rightarrow \quad R \]
+% 
+% 
+%   \[ f(p)=\ldots\;  p \in \quad R \]
+% 
+%     {\small\textit{
+%       \noindent Above we see two equations. The first equation aims to
+% be a mapping of an function from the reel range to the reel one, but
+% when we change only one letter we get the second equation which
+% usually aims to insert a reel point $p$ into the reel function. In
+% computer science now we have the problem to tell the machine (TP) the
+% difference between this two notations. This Problem is called
+% \emph{Lambda Calculus}.
+%     }}
+%   \end{example}
+% }
+% 
+% \paragraph{An other problem} is that terms are not full simplified in
+% traditional notations, in {{\sisac}} we have to simplify them complete
+% to check weather results are compatible or not. in e.g. the solutions
+% of an second order linear equation is an rational in {{\sisac}} but in
+% tradition we keep fractions as long as possible and as long as they
+% aim to be \textit{beautiful} (1/8, 5/16,...).
+% \subparagraph{The math} which should be mechanized in Computer Theorem
+% Provers (\emph{TP}) has (almost) a problem with traditional notations
+% (predicate calculus) for axioms, definitions, lemmas, theorems as a
+% computer program or script is not able to interpret every Greek or
+% Latin letter and every Greek, Latin or whatever calculations
+% symbol. Also if we would be able to handle these symbols we still have
+% a problem to interpret them at all. (Follow up \hbox{Example
+% \ref{eg:symbint1}})
+% 
+% \vbox{
+%   \begin{example}
+%     \label{eg:symbint1}
+%     \[
+%       u\left[n\right] \ \ldots \ unitstep
+%     \]
+%     {\small\textit{
+%       \noindent The unitstep is something we need to solve Signal
+% Processing problem classes. But in {{{\sisac}{}}} the rectangular
+% brackets have a different meaning. So we abuse them for our
+% requirements. We get something which is not defined, but usable. The
+% Result is syntax only without semantic.
+%     }}
+%   \end{example}
+% }
+% 
+% In different problems, symbols and letters have different meanings and
+% ask for different ways to get through. (Follow up \hbox{Example
+% \ref{eg:symbint2}}) 
+% 
+% \vbox{
+%   \begin{example}
+%     \label{eg:symbint2}
+%     \[
+%       \widehat{\ }\ \widehat{\ }\ \widehat{\ } \  \ldots \  exponent
+%     \]
+%     {\small\textit{
+%     \noindent For using exponents the three \texttt{widehat} symbols
+% are required. The reason for that is due the development of
+% {{{\sisac}{}}} the single \texttt{widehat} and also the double were
+% already in use for different operations.
+%     }}
+%   \end{example}
+% }
+% 
+% \paragraph{Also the output} can be a problem. We are familiar with a
+% specified notations and style taught in university but a computer
+% program has no knowledge of the form proved by a professor and the
+% machines themselves also have not yet the possibilities to print every
+% symbol (correct) Recent developments provide proofs in a human
+% readable format but according to the fact that there is no money for
+% good working formal editors yet, the style is one thing we have to
+% live with.
+% 
+% \section{Problems rising out of the Development Environment}
+% 
+% fehlermeldungen! TODO
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\end{verbatim}
+
+\section{Summary and Conclusions}\label{conclusion}
+
+%JR obvious
+
+%This paper gives a first experience report about programming with a
+%TP-based programming language.
+
+A brief re-introduction of the novel kind of programming
+language by example of the {\sisac}-prototype makes the paper
+self-contained. The main section describes all the main concepts
+involved in TP-based programming and all the sub-tasks concerning
+respective implementation in the {\sisac} prototype: mechanisation of mathematics and domain
+modeling, implementation of term rewriting systems for the
+rewriting-engine, formal (implicit) specification of the problem to be
+(explicitly) described by the program, implementation of the many components
+required for Lucas-Interpretation and finally implementation of the
+program itself.
+
+The many concepts and sub-tasks involved in programming require a
+comprehensive work-flow; first experiences with the work-flow as
+supported by the present prototype are described as well: Isabelle +
+Isar + jEdit provide appropriate components for establishing an
+efficient development environment integrating computation and
+deduction. However, the present state of the prototype is far off a
+state appropriate for wide-spread use: the prototype of the program
+language lacks expressiveness and elegance, the prototype of the
+development environment is hardly usable: error messages still address
+the developer of the prototype's interpreter rather than the
+application programmer, implementation of the many settings for the
+Lucas-Interpreter is cumbersome. 
+
+\subsection{Conclusions for Future Development}
+From the above mentioned experiences a successful proof of concept can be concluded:
+programming arbitrary problems from engineering sciences is possible,
+in principle even in the prototype. Furthermore the experiences allow
+to conclude detailed requirements for further development:
+\begin{enumerate}
+\item Clarify underlying logics such that programming is smoothly
+integrated with verification of the program; the post-condition should
+be proved more or less automatically, otherwise working engineers
+would not encounter such programming.
+\item Combine the prototype's programming language with Isabelle's
+powerful function package and probably with more of SML's
+pattern-matching features; include parallel execution on multi-core
+machines into the language design.
+\item Extend the prototype's Lucas-Interpreter such that it also
+handles functions defined by use of Isabelle's functions package; and
+generalize Isabelle's code generator such that efficient code for the
+whole definition of the programming language can be generated (for
+multi-core machines).
+\item Develop an efficient development environment with
+integration of programming and proving, with management not only of
+Isabelle theories, but also of large collections of specifications and
+of programs.
+\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} 
+Provided successful accomplishment, these points provide distinguished
+components for virtual workbenches appealing to practitioners of
+engineering in the near future.
+
+\subsection{Preview to Development of Course Material}
+Interactive course material, as addressed by the title,
+can comprise step-wise problem solving created as a side-effect of a
+TP-based program: The introduction \S\ref{intro} briefly shows that Lucas-Interpretation not only provides an
+interactive programming environment, Lucas-Interpretation also can
+provide TP-based services for a flexible dialogue component with
+adaptive user guidance for independent and inquiry-based learning.
+
+However, the {\sisac} prototype is not ready for use in field-tests,
+not only due to the above five requirements not sufficiently
+accomplished, but also due to usability of the fron-end, in particular
+the lack of an editor for formulas in 2-dimension representation.
+
+Nevertheless, the experiences from the case study described in this
+paper, allow to give a preview to the development of course material,
+if based on Lucas-Interpretation:
+
+\paragraph{Development of material from scratch} is too much effort
+just for e-learning; this has become clear with the case study.  For
+getting support for stepwise problem solving just in {\em one} example
+class, the one presented in this paper, involved the following tasks:
+\begin{itemize}
+\item Adapt the equation solver; since that was too laborous, the
+program has been adapted in an unelegant way.
+\item Implement an algorithms for partial fraction decomposition,
+which is considered a standard normal form in Computer Algebra.
+\item Implement a specification for partial fraction decomposition and
+locate it appropriately in the hierarchy of specification.
+\item Declare definitions and theorems within the theory of
+${\cal Z}$-transform, and prove the theorems (which was not done in the
+case study).
+\end{itemize}
+On the other hand, for the one the class of problems implemented,
+adding an arbitrary number of examples within this class requires a
+few minutes~\footnote{As shown in Fig.\ref{fig-interactive}, an
+example is called from an HTML-file by an URL, which addresses an
+XML-structure holding the respective data as shown on
+p.\pageref{ml-check-program}.} and the support for individual stepwise
+problem solving comes for free.
+
+\paragraph{E-learning benefits from Formal Domain Engineering} which can be
+expected for various domains in the near future. In order to cope with
+increasing complexity in domain of technology, specific domain
+knowledge is beeing mechanised, not only for software technology
+\footnote{For instance, the Archive of Formal Proofs
+http://afp.sourceforge.net/} but also for other engineering domains
+\cite{Dehbonei&94,Hansen94b,db:dom-eng}.  This fairly new part of
+engineering sciences is called ``domain engineering'' in
+\cite{db:SW-engIII}.
+
+Given this kind of mechanised knowledge including mathematical
+theories, domain specific definitions, specifications and algorithms,
+theorems and proofs, then e-learning with support for individual
+stepwise problem solving will not be much ado anymore; then e-learning
+media in technology education can be derived from this knowledge with
+reasonable effort.
+
+\paragraph{Development differentiates into tasks} more separated than
+without Lucas-Interpretation and more challenginging in specific
+expertise. These are the kinds of experts expected to cooperate in
+development of
+\begin{itemize}
+\item ``Domain engineers'', who accomplish fairly novel tasks
+described in this paper.
+\item Course designers, who provide the instructional design according
+to curricula, together with usability experts and media designers, are
+indispensable in production of e-learning media at the state-of-the
+art.
+\item ``Dialog designers'', whose part of development is clearly
+separated from the part of domain engineers as a consequence of
+Lucas-Interpretation: TP-based programs are functional, as mentioned,
+and are only concerned with describing mathematics --- and not at all
+concerned with interaction, psychology, learning theory and the like,
+because there are no in/output statements. Dialog designers can expect
+a high-level rule-based language~\cite{gdaroczy-EP-13} for describing
+their part.
+\end{itemize}
+
+% response-to-referees:
+% (2.1) details of novel technology in order to estimate the impact
+% (2.2) which kinds of expertise are required for production of e-learning media (instructional design, math authoring, dialog authoring, media design)
+% (2.3) what in particular is required for programming new exercises supported by next-step-guidance (expertise / efforts)
+% (2.4) estimation of break-even points for development of next-step-guidance
+% (2.5) usability of ISAC prototype at the present state
+% 
+% The points (1.*) seem to be well covered in the paper, the points (2.*) are not. So I decided to address the points (2.*) in a separate section §5.1."".
+
+\bigskip\noindent For this decade there seems to be a window of opportunity opening from
+one side inreasing demand for formal domain engineering and from the
+other side from TP more and more gaining industrial relevance. Within
+this window, development of TP-based educational software can take
+benefit from the fact, that the TPs leading in Europe, Coq~\cite{coq-team-10} and
+Isabelle are still open source together with the major part of
+mechanised knowledge.%~\footnote{NICTA}.
+
+\bibliographystyle{alpha}
+{\small\bibliography{references}}
+
+\end{document}
+% LocalWords:  TP IST SPSC Telematics Dialogues dialogue HOL bool nat Hindley
+% LocalWords:  Milner tt Subproblem Formulae ruleset generalisation initialised
+% LocalWords:  axiomatization LCF Simplifiers simplifiers Isar rew Thm Calc SML
+% LocalWords:  recognised hoc Trueprop redexes Unsynchronized pre rhs ord erls
+% LocalWords:  srls prls nrls lhs errpats InverseZTransform SubProblem IDE IDEs
+% LocalWords:  univariate jEdit rls RealDef calclist familiarisation ons pos eq
+% LocalWords:  mout ctree SignalProcessing frac ZZ Postcond Atools wiki SML's
+% LocalWords:  mechanisation multi




