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

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