1.1 --- a/doc-src/isac/jrocnik/eJMT-paper/jrocnik_eJMT.tex	Sun Sep 09 21:12:49 2012 +0200
     1.2 +++ b/doc-src/isac/jrocnik/eJMT-paper/jrocnik_eJMT.tex	Sun Sep 09 21:14:20 2012 +0200
     1.3 @@ -848,47 +848,101 @@
     1.4  % }
     1.5  
     1.6  \subsection{Implementation of the Method}\label{meth}
     1.7 -%WN <--> \chapter 7 der Thesis
     1.8 -TODO
     1.9 -\subsection{Preparation of Simplifiers for the Program}\label{simp}
    1.10  
    1.11 -\paragraph{After collecting} informations about the problem 
    1.12 -%WN4 welche 'informations' ?
    1.13 -%WN4 Wenn das welche sind, die oben NICHT vorgekommen sind, dann anf"uhren
    1.14 -%WN4 Wenn das welche sind, die oben SCHON vorgekommen sind, dann weglassen
    1.15 -%WN4                       und Platz sparen.
    1.16 -%WN4 
    1.17 -%WN4 Wenn wir diese Bemerkung hier weglassen (sie m"usste eigentlich an jedem
    1.18 -%WN4 Beginn von 3.* stehen), dann kommt sie gleich an den Anfang
    1.19 -%WN4 nach der "Uberschrift von 3.
    1.20 -and reviewing the calculations, 
    1.21 -%WN4 welche 'calculations', ist von solchen bisher schon die Rede gewesen ?
    1.22 -the programm may be seem hard and heavy, therefor we can set up
    1.23 -some simplifications, for e.g. is the simplification of reational expressions
    1.24 -already provided in the {\sisac{}} system. 
    1.25 -%WN4 
    1.26 -Also obligate is the use of the 
    1.27 -function \texttt{drop\_questionmarks} which excludes irrelevant symbols out of
    1.28 -the expression. (Irrelevant symbols may be result out of the system during the
    1.29 -calculation.)
    1.30 -
    1.31 -\subparagraph{Simplifiers often are represented} through rulesets\footnote{More
    1.32 -information about rulesets can be found in \S\ref{sec:rules}}, this rulesets
    1.33 -tell the machine which terms should be simplified into which representation. In
    1.34 -the upcoming programm a simplification is applied only in using such rulesets
    1.35 -on existing terms.
    1.36 -\par
    1.37 -Following example line was taken out of a finished programm and shows how
    1.38 -an rational expression can be simplified.
    1.39 +\paragraph{todo}
    1.40  
    1.41  \begin{example}
    1.42  \begin{verbatim}
    1.43  
    1.44 -  "expression = (Rewrite_Set norm_Rational False) expression;"^\end{verbatim}
    1.45 +01 store_met
    1.46 +02  (prep_met thy "met_SP_Ztrans_inv" [] e_metID
    1.47 +03  (["SignalProcessing", "Z_Transform", "Inverse"], 
    1.48 +04   [("#Given" ,["filterExpression (X_eq::bool)"]),
    1.49 +05    ("#Find"  ,["stepResponse (n_eq::bool)"])],
    1.50 +06   {rew_ord'="tless_true",
    1.51 +07    rls'= e_rls, 
    1.52 +08    calc = [],
    1.53 +09    srls = e_rls,
    1.54 +10    prls = e_rls,
    1.55 +11    crls = e_rls,
    1.56 +12    errpats = [],
    1.57 +13    nrls = e_rls},
    1.58 +14   "empty_script"
    1.59 +15  ));
    1.60 +\end{verbatim}
    1.61  \end{example}
    1.62  
    1.63 -\subparagraph{If other} methods for use in term with simplification are needed
    1.64 -\S\ref{funs} gives informations about new ML-Functions can be prepared.
    1.65 +
    1.66 +\subsection{Preparation of Simplifiers for the Program}\label{simp}
    1.67 +
    1.68 +\paragraph{If it is clear} how the later calculation should look like and when
    1.69 +which mathematic rule should be applied, it can be started to find ways of
    1.70 +simplifications. This includes in e.g. the simplification of reational 
    1.71 +expressions or also rewrites of an expession.
    1.72 +\subparagraph{Obligate is the use} of the function \texttt{drop\_questionmarks} 
    1.73 +which excludes irrelevant symbols out of the expression. (Irrelevant symbols may 
    1.74 +be result out of the system during the calculation. The function has to be
    1.75 +applied for two reasons. First two make every placeholder in a expression 
    1.76 +useable as a constant and second to provide a better view at the frontend.) 
    1.77 +\subparagraph{Most rewrites are represented} through rulesets this
    1.78 +rulesets tell the machine which terms have to be rewritten into which
    1.79 +representation. In the upcoming programm a rewrite can be applied only in using
    1.80 +such rulesets on existing terms.
    1.81 +\paragraph{The core} of our implemented problem is the Z-Transformation
    1.82 +(remember the description of the running example, introduced by
    1.83 +Fig.\ref{fig-interactive} on p.\pageref{fig-interactive}) due the fact that the
    1.84 +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
    1.85 +transformation tables).
    1.86 +\paragraph{Rules,} in {\sisac{}}'s programming language can be designed by the
    1.87 +use of axiomatizations like shown in Example~\ref{eg:ruledef}. This rules can be
    1.88 +collected in a ruleset (collection of rules) and applied to a given expression
    1.89 +as follows in Example~\ref{eg:ruleapp}.
    1.90 +
    1.91 +\begin{example}
    1.92 +  \label{eg:ruledef}
    1.93 +  \hfill\\
    1.94 +  \begin{verbatim}
    1.95 +  axiomatization where
    1.96 +    rule1: ``1 = $\delta$[n]'' and
    1.97 +    rule2: ``|| z || > 1 ==> z / (z - 1) = u [n]'' and
    1.98 +    rule3: ``|| z || < 1 ==> z / (z - 1) = -u [-n - 1]''
    1.99 +  \end{verbatim}
   1.100 +\end{example}
   1.101 +
   1.102 +\begin{example}
   1.103 +  \hfill\\
   1.104 +  \label{eg:ruleapp}
   1.105 +  \begin{enumerate}
   1.106 +  \item Store rules in ruleset:
   1.107 +  \begin{verbatim}
   1.108 +  val inverse_Z = append_rls "inverse_Z" e_rls
   1.109 +    [ Thm ("rule1",num_str @{thm rule1}),
   1.110 +      Thm ("rule2",num_str @{thm rule2}),
   1.111 +      Thm ("rule3",num_str @{thm rule3})
   1.112 +    ];\end{verbatim}
   1.113 +  \item Define exression:
   1.114 +  \begin{verbatim}
   1.115 +  val sample_term = str2term "z/(z-1)+z/(z-</delta>)+1";\end{verbatim}
   1.116 +  \item Apply ruleset:
   1.117 +  \begin{verbatim}
   1.118 +  val SOME (sample_term', asm) = 
   1.119 +    rewrite_set_ thy true inverse_Z sample_term;\end{verbatim}
   1.120 +  \end{enumerate}
   1.121 +\end{example}
   1.122 + 
   1.123 +The use of rulesets makes it much easier to develop our designated applications,
   1.124 +but the programmer has to be careful and patient. When applying rulesets
   1.125 +two important issues have to be mentionend:
   1.126 +\subparagraph{How often} the rules have to be applied? In case of
   1.127 +transformations it is quite clear that we use them once but other fields
   1.128 +reuqire to apply rules until a special condition is reached (e.g.
   1.129 +a simplification is finished when there is nothing to be done left).
   1.130 +\subparagraph{The order} in which rules are applied often takes a big effect
   1.131 +and has to be evaluated for each purpose once again.
   1.132 +\par
   1.133 +In our special case of Signal Processing and the rules defined in
   1.134 +Example~\ref{eg:ruledef} we have to apply rule~1 first of all to transform all
   1.135 +constants. After this step has been done it no mather which rule fit's next.
   1.136  
   1.137  \subsection{Preparation of ML-Functions}\label{funs}
   1.138