%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

 % 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}

 %

 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

 %                                                         %

 % 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 Technologie\\

 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. %TODO ... connect to prototype ...

 A prototype combines TP with a programming language, the latter

 interpreted in a specific way: certain statements in a program, called

 tactics, are treated as breakpoints where control is handed over to

 the user. An input formula is checked by TP (using logical context

 built up by the interpreter); and if a learner gets stuck, a program

 describing the steps towards a solution of a problem ``knows the next

 step''. This kind of interpretation is called Lucas-Interpretation for

 \emph{TP-based programming languages}.

 This paper describes the prototype's TP-based programming language

 within a case study creating interactive material for an advanced

 course in Signal Processing: implementation of definitions and

 theorems in TP, formal specification of a problem and step-wise

 development of the program solving the problem. Experiences with the

 ork flow in iterative development with testing and identifying errors

 are described, too. The description clarifies the components missing

 in the prototype's language as well as deficiencies experienced during

 programming.

 \par

 These experiences are particularly notable, because the author is the

 first programmer using the language beyond the core team which

 developed the prototype's TP-based language 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.

 % 

 \paragraph{Traditional course material} in engineering disciplines lacks an

 important component, interactive support for step-wise problem

 solving. 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 and the

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

 self-contained.

 \subparagraph{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 not involved in the development of

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

 language.

 \subparagraph{The goal} of the case study was (1) some TP-based programs for

 interactive course material for a specific ``Adavanced Signal

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

 development with as little advice from the {\sisac}-team and (3) 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

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

 running example:

 \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}

 \paragraph{The problem is} from the domain of Signal Processing and requests to

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

 also 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'' from behind the scenes. How the latter

 TP-service is exploited by dialogue authoring 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 services

 generated automatically.

 \par

 So there is a clear separation of concerns: Dialogues are

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

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

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

 paper.

 \paragraph{The paper is structed} 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 in \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 program, implement the

 program. The workflow 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's language extends the executable fragment in the

 language of the theorem prover

 Isabelle~\cite{Nipkow-Paulson-Wenzel:2002}\footnote{http://isabelle.in.tum.de/}

 by tactics which have a specific role in Lucas-Interpretation.

 \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:

 {\it\label{isabelle-stmts}

 \begin{tabbing} 123\=\kill

 \>$( \; {\tt if} \; b \; {\tt then} \; t_1 \; {\tt else} \; t_2 \;)$\\

 \>$( \; {\tt let} \; x=t \; {\tt in} \; u \; )$\\

 \>$( \; {\tt case} \; t \; {\tt of} \; {\it pat}_1

   \Rightarrow t_1 \; |\dots| \; {\it pat}_n\Rightarrow t_n \; )$

 \end{tabbing} }

 \noindent \textit{The running example's program uses some of these elements

 (marked by {\tt tt-font} on p.\pageref{expl-program}): ${\tt

 let}\dots{\tt in}$ in lines $02 \dots 11$, as well as {\tt last} for

 lists and {\tt o} for functional (forward) composition in line

 $10$. In fact, the whole program is an Isabelle term with specific

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

 Rewrite\_Set\_Inst} in lines $01$ and $10$ 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 tactics are different from

 Isabelle's tactics: the former concern steps in a calculation, the

 latter concern proof steps.}  and tacticals. 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 appplies {\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 appplies {\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}$:

 \item[Substitute:] ${\it substitution}\Rightarrow{\it

 term}\Rightarrow{\it term}$:

 \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 allows to enter a phase of interactive specification

 of a theory ($\Re$, $\cal C$, etc), a formal specification (for instance,

 a specific type of equation) and a method (for instance, solving an

 equation symbolically or numerically).

 \end{description}

 The tactics play a specific role in

 Lucas-Interpretation~\cite{wn:lucas-interp-12}: they are treated as

 break-points and control is handed over 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{Tacticals for Control of Interpretation}

 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 tacticals:

 \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, {\it 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 unchanged.

 \item[Or:] ${\it tactic}\Rightarrow{\it tactic}\Rightarrow{\it

 term}\Rightarrow{\it term}$:

 \item[@@:] ${\it tactic}\Rightarrow{\it tactic}\Rightarrow{\it

 term}\Rightarrow{\it term}$:

 \item[While:] ${\it term::bool}\Rightarrow{\it tactic}\Rightarrow{\it

 term}\Rightarrow{\it term}$:

 \end{description}

 no input / output --- Lucas-Interpretation

 .\\.\\.\\TODO\\.\\.\\

 \section{Development of a Program on Trial}\label{trial} 

 As mentioned above, {\sisac} is an experimental system for a proof of

 concept for Lucas-Interpretation~\cite{wn:lucas-interp-12}.  The

 latter interprets a specific kind of TP-based programming language,

 which is as experimental as the whole prototype --- so programming in

 this language can be only ``on trial'', presently.  However, as a

 prototype, the language addresses essentials described below.

 \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, introduced by Fig.\ref{fig-interactive} on

 p.\pageref{fig-interactive}, 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 summable and are called TODO: $u[n]$, where $u$ is the

 function, $n$ is the argument and the brackets indicate that the

 arguments are TODO. Surprisingly, Isabelle accepts the rules for

 ${\cal 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}

   {\small\begin{tabbing}

   123\=123\=123\=123\=\kill

   \hfill \\

   \>axiomatization where \\

   \>\>  rule1: ``${\cal Z}^{-1}\;1 = \delta [n]$'' and\\

   \>\>  rule2: ``$\vert\vert z \vert\vert > 1 \Rightarrow {\cal Z}^{-1}\;z / (z - 1) = u [n]$'' and\\

   \>\>  rule3: ``$\vert\vert$ z $\vert\vert$ < 1 ==> z / (z - 1) = -u [-n - 1]'' and \\

 %TODO

   \>\>  rule4: ``$\vert\vert$ z $\vert\vert$ > $\vert\vert$ $\alpha$ $\vert\vert$ ==> z / (z - $\alpha$) = $\alpha^n$ $\cdot$ u [n]'' and\\

 %TODO

   \>\>  rule5: ``$\vert\vert$ z $\vert\vert$ < $\vert\vert$ $\alpha$ $\vert\vert$ ==> z / (z - $\alpha$) = -($\alpha^n$) $\cdot$ u [-n - 1]'' and\\

 %TODO

   \>\>  rule6: ``$\vert\vert$ z $\vert\vert$ > 1 ==> z/(z - 1)$^2$ = n $\cdot$ u [n]''\\

 %TODO

   \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 proven 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 Z-Transform the most advanced

 knowledge can be found in the theoris 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).

 \paragraph{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{TODO-formal-methods}

 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-domain-engineering} 

 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.

 \subparagraph{TP-based programming, concern of this paper,} is determined to

 add ``algorithmic 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.

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

 %WN <--> \chapter 7 der Thesis

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

 The problem of the running example is textually described in

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

 formal} specification of this problem, in traditional mathematical

 notation, could look like is this:

 %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,\=postcond \=: \= $\forall \,A^\prime\, u^\prime \,v^\prime.\,$\=\kill

   \hfill \\

   Specification:\\

     \>input    \>: filterExpression $X=\frac{3}{(z-\frac{1}{4}+-\frac{1}{8}*\frac{1}{z}}$\\

   \>precond  \>: filterExpression continius on $\mathbb{R}$ \\

   \>output   \>: stepResponse $x[n]$ \\

   \>postcond \>: TODO - (Mind the following remark)\\ \end{tabbing}}

 \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}

 \paragraph{The implementation} of the formal specification in the present

 prototype, still bar-bones without support for authoring:

 %WN Kopie von Inverse_Z_Transform.thy, leicht versch"onert:

 {\footnotesize

 \begin{verbatim}

    01  store_specification

    02    (prepare_specification

    03      ["Jan Rocnik"]

    04      "pbl_SP_Ztrans_inv"

    05      thy

    06      ( ["Inverse", "Z_Transform", "SignalProcessing"],

    07        [ ("#Given", ["filterExpression X_eq"]),

    08          ("#Pre"  , ["X_eq is_continuous"]),

    19          ("#Find" , ["stepResponse n_eq"]),

    10          ("#Post" , [" TODO "])],

    11        append_rls Erls [Calc ("Atools.is_continuous", eval_is_continuous)], 

    12        NONE, 

    13        [["SignalProcessing","Z_Transform","Inverse"]]));

 \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 asyncronous document model~\cite{Wenzel-11:doc-orient} and

 parallel execution~\cite{Makarius-09:parall-proof} and is under

 reconstruction already.

 \textit{prep\_pbt:} translates the specification to an internal format

 which allows efficient processing; see for instance line {\rm 07}

 below.

 \item[03..04] are the ``mathematics author'' holding the copy-rights

 and a unique identifier for the specification within {\sisac},

 complare line {\rm 06}.

 \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 dialog

 component).

 \item[07..10] are the specification with input, pre-condition, output

 and post-condition respectively; the post-condition is not handled in

 the prototype presently. (Follow up Remark~\ref{rm:postcond})

 \item[11] creates a term rewriting system (abbreviated \textit{rls} in

 {\sisac}) which evaluates the pre-condition for the actual input data.

 Only if the evaluation yields \textit{True}, a program con be started.

 \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 the specific key into the tree of programs addressing a

 method which is able to find a solution which satiesfies the

 post-condition of the specification.

 \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}

 %WN <--> \chapter 7 der Thesis

 TODO

 \subsection{Preparation of Simplifiers for the Program}\label{simp}

 %JR: ich denke wir können diesen punkt weglassen, methoden wie

 %JR: drop_questionmarks und ähnliche sind im arical nicht ersichtlich und im 

 %JR: grunde nicht relevant (ihre erstellung gleich wie functionen im nächsten

 %JR: Punkt)

 \subsection{Preparation of ML-Functions}\label{funs}

 \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, Example~\ref{eg:getdenom} 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{Implementation of the TP-based Program}\label{progr}

 \paragraph{After introducing} neccesarry informations about the {\sisac{}}

 System, the main part of a implementation in the TP-bases language can be shown.

 \par

 Solution~\ref{s:impl} shows us the implementation of the

 Inverse-Z-Transformation, a description on the code is given afterwards.

 \begin{solution}

 \label{s:impl}

 \begin{tabbing}

 \small\it

 123l\=123\=123\=123\=123\=123\=123\=123\=123\=(x \=123\=123\=\kill

 \> \\

 \> \\

 \>{\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} ruleZY 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, \\

 \>{\rm 08}\>\>\>\>\>\>\>\>\>  [partial\_fraction, rational, simplification]\\

 \>{\rm 09}\>\>\>\>\>\>\>\>\>  [simplification,of\_rationals,to\_partial\_fraction] ) \\

 \>{\rm 10}\>\>\>\>\>\>\>\>  [ (rhs X\_eq)::real, z::real ]; \\

 \>{\rm 12}\>\>\>  (X'\_eq::bool) = {\tt Take} ((X'::real =$>$ bool) z = ZZ\_1 part\_frac) ; \\

 \>{\rm 12}\>\>\>  X'\_eq = {\tt Rewrite\_Set} ruleYZ X'\_eq ;   \\

 \>{\rm 15}\>\>\>  X'\_eq = {\tt Rewrite\_Set} inverse\_z X'\_eq \\

 \>{\rm 16}\>\>  {\tt IN } \\

 \>{\rm 15}\>\>\>  X'\_eq

 \end{tabbing}

 \end{solution}

 % 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]*)

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

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

 TODO Build\_Inverse\_Z\_Transform.thy ... ``imports PolyEq DiffApp Partial\_Fractions''

 .\\.\\.\\

 %JR: Hier sollte eigentlich stehen was nun bei 4.3.1 ist. Habe das erst kürzlich

 %JR: eingefügt; das war der beinn unserer Arbeit in

 %JR: Build_Inverse_Z_Transformation und beschreibt die meiner Meinung nach bei

 %JR: jedem neuen Programm nötigen Schritte.

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

 \paragraph{At the beginning} of the implementation it is good to decide on one

 way the problem should be solved. We also did this for our Z-Transformation

 Problem and have choosen the way it is also thaugt in the Signal Processing

 Problem classes.

 \subparagraph{By writing down} each of this neccesarry steps we are describing

 one line of our upcoming program. In the following example we show the 

 Calculation on the left and on the right the tactics in the program which

 created the respective formula on the left.

 \begin{example}

 \hfill\\

 {\small\it

 \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} ruleZY 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} ruleYZ 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}}

 \end{example}

 % 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}

 TODO http://www.ist.tugraz.at/isac/index.php/Extend\_ISAC\_Knowledge\#Add\_an\_example ?

 \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

 \section{Conclusion}\label{conclusion}

 TODO

 \bibliographystyle{alpha}

 \bibliography{references}

 \end{document}