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




