(* Title:  Build_Inverse_Z_Transform

    Author: Jan Rocnik

    (c) copyright due to license terms.

 *)

 theory Build_Inverse_Z_Transform imports Isac.Inverse_Z_Transform

 begin

 text{* We stepwise build \ttfamily Inverse\_Z\_Transform.thy \normalfont as an 

   exercise. Because Subsection~\ref{sec:stepcheck} requires 

   \ttfamily Inverse\_Z\_Transform.thy \normalfont as a subtheory of \ttfamily 

   Isac.thy\normalfont, the setup has been changed from \ttfamily theory 

   Inverse\_Z\_Transform imports Isac \normalfont to the above one.

   \par \noindent

   \begin{center} 

   \textbf{Attention with the names of identifiers when going into internals!}

   \end{center}

   Here in this theory there are the internal names twice, for instance we have

   \ttfamily (Thm.derivation\_name @{thm rule1} = 

   "Build\_Inverse\_Z\_Transform.rule1") = true; \normalfont

   but actually in us will be \ttfamily Inverse\_Z\_Transform.rule1 \normalfont

 *}

 section {*Trials towards the Z-Transform\label{sec:trials}*}

 ML {*val thy = @{theory};*}

 subsection {*Notations and Terms*}

 text{*\noindent Try which notations we are able to use.*}

 ML {*

   @{term "1 < || z ||"};

   @{term "z / (z - 1)"};

   @{term "-u -n - 1"};

   @{term "-u [-n - 1]"}; (*[ ] denotes lists !!!*)

   @{term "z /(z - 1) = -u [-n - 1]"};

   @{term "1 < || z || ==> z / (z - 1) = -u [-n - 1]"};

   term2str @{term "1 < || z || ==> z / (z - 1) = -u [-n - 1]"};

 *}

 text{*\noindent Try which symbols we are able to use and how we generate them.*}

 ML {*

   (*alpha -->  "</alpha>" *)

   @{term "\<alpha> "};

   @{term "\<delta> "};

   @{term "\<phi> "};

   @{term "\<rho> "};

   term2str @{term "\<rho> "};

 *}

 subsection {*Rules*}

 (*axiomatization "z / (z - 1) = -u [-n - 1]"

   Illegal variable name: "z / (z - 1) = -u [-n - 1]" *)

 (*definition     "z / (z - 1) = -u [-n - 1]"

   Bad head of lhs: existing constant "op /"*)

 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]" and 

   rule4: "|| z || > || \<alpha> || ==> z / (z - \<alpha>) = \<alpha>^^^n * u [n]" and

   rule5: "|| z || < || \<alpha> || ==> z / (z - \<alpha>) = -(\<alpha>^^^n) * u [-n - 1]" and

   rule6: "|| z || > 1 ==> z/(z - 1)^^^2 = n * u [n]"

 text{*\noindent Check the rules for their correct notation. 

       (See the machine output.)*}

 ML {*

   @{thm rule1};

   @{thm rule2};

   @{thm rule3};

   @{thm rule4};

 *}

 subsection {*Apply Rules*}

 text{*\noindent We try to apply the rules to a given expression.*}

 ML {*

   val inverse_Z = append_rls "inverse_Z" e_rls

     [ Thm  ("rule3",TermC.num_str @{thm rule3}),

       Thm  ("rule4",TermC.num_str @{thm rule4}),

       Thm  ("rule1",TermC.num_str @{thm rule1})   

     ];

   val t = TermC.str2term "z / (z - 1) + z / (z - \<alpha>) + 1";

   val SOME (t', asm) = Rewrite.rewrite_set_ thy true inverse_Z t;

   term2str t' = "z / (z - ?\<delta> [?n]) + z / (z - \<alpha>) + ?\<delta> [?n]";

   (*

    * Attention rule1 is applied before the expression is 

    * checked for rule4 which would be correct!!!

    *)

 *}

 ML {* val (thy, ro, er) = (@{theory}, tless_true, eval_rls); *}

 ML {*

   val SOME (t, asm1) = 

     Rewrite.rewrite_ thy ro er true (TermC.num_str @{thm rule3}) t;

   term2str t = "- ?u [- ?n - 1] + z / (z - \<alpha>) + 1";

   (*- real *)

   term2str t;

   val SOME (t, asm2) = 

     Rewrite.rewrite_ thy ro er true (TermC.num_str @{thm rule4}) t;

   term2str t = "- ?u [- ?n - 1] + \<alpha> ^^^ ?n * ?u [?n] + 1";

   (*- real *)

   term2str t;

   val SOME (t, asm3) = 

     Rewrite.rewrite_ thy ro er true (TermC.num_str @{thm rule1}) t;

   term2str t = "- ?u [- ?n - 1] + \<alpha> ^^^ ?n * ?u [?n] + ?\<delta> [?n]";

   (*- real *)

   term2str t;

 *}

 ML {* terms2str (asm1 @ asm2 @ asm3); *}

 section{*Prepare Steps for TP-based programming Language\label{sec:prepstep}*}

 text{*

       \par \noindent The following sections are challenging with the CTP-based 

       possibilities of building the program. The goal is realized in 

       Section~\ref{spec-meth} and Section~\ref{prog-steps}.

       \par The reader is advised to jump between the subsequent subsections and 

       the respective steps in Section~\ref{prog-steps}. By comparing 

       Section~\ref{sec:calc:ztrans} the calculation can be comprehended step 

       by step.

 *}

 subsection {*Prepare Expression\label{prep-expr}*}

 text{*\noindent We try two different notations and check which of them 

        Isabelle can handle best.*}

 ML {*

   val ctxt = Proof_Context.init_global @{theory};

   val ctxt = Stool.declare_constraints' [@{term "z::real"}] ctxt;

   val SOME fun1 = 

     TermC.parseNEW ctxt "X z = 3 / (z - 1/4 + -1/8 * z ^^^ -1)"; term2str fun1;

   val SOME fun1' = 

     TermC.parseNEW ctxt "X z = 3 / (z - 1/4 + -1/8 * (1/z))"; term2str fun1';

 *}

 subsubsection {*Prepare Numerator and Denominator*}

 text{*\noindent The partial fraction decomposition is only possible if we

        get the bound variable out of the numerator. Therefor we divide

        the expression by $z$. Follow up the Calculation at 

        Section~\ref{sec:calc:ztrans} line number 02.*}

 axiomatization where

   ruleZY: "(X z = a / b) = (X' z = a / (z * b))"

 ML {*

   val (thy, ro, er) = (@{theory}, tless_true, eval_rls);

   val SOME (fun2, asm1) = 

     Rewrite.rewrite_ thy ro er true  @{thm ruleZY} fun1; term2str fun2;

   val SOME (fun2', asm1) = 

     Rewrite.rewrite_ thy ro er true  @{thm ruleZY} fun1'; term2str fun2';

   val SOME (fun3,_) = 

     Rewrite.rewrite_set_ @{theory} false norm_Rational fun2;

   term2str fun3;

   (*

    * Fails on x^^^(-1)

    * We solve this problem by using 1/x as a workaround.

    *)

   val SOME (fun3',_) = 

     Rewrite.rewrite_set_ @{theory} false norm_Rational fun2';

   term2str fun3';

   (*

    * OK - workaround!

    *)

 *}

 subsubsection {*Get the Argument of the Expression X'*}

 text{*\noindent We use \texttt{grep} for finding possibilities how we can

        extract the bound variable in the expression. \ttfamily Atools.thy, 

        Tools.thy \normalfont contain general utilities: \ttfamily 

        eval\_argument\_in, eval\_rhs, eval\_lhs,\ldots \normalfont

        \ttfamily grep -r "fun eva\_" * \normalfont shows all functions 

        witch can be used in a script. Lookup this files how to build 

        and handle such functions.

        \par The next section shows how to introduce such a function.

 *}

 subsubsection{*Decompose the Given Term Into lhs and rhs*}

 ML {*

   val (_, expr) = HOLogic.dest_eq fun3'; term2str expr;

   val (_, denom) = 

     HOLogic.dest_bin "Rings.divide_class.divide" (type_of expr) expr;

   term2str denom = "-1 + -2 * z + 8 * z ^^^ 2";

 *}

 text{*\noindent We have rhs\footnote{Note: lhs means \em Left Hand Side

       \normalfont and rhs means \em Right Hand Side \normalfont and indicates

       the left or the right part of an equation.} in the Script language, but

       we need a function which gets the denominator of a fraction.*}

 subsubsection{*Get the Denominator and Numerator out of a Fraction*}

 text{*\noindent The self written functions in e.g. \texttt{get\_denominator}

        should become a constant for the Isabelle parser:*}

 consts

   get_denominator :: "real => real"

   get_numerator :: "real => real"

 text {*\noindent With the above definition we run into problems when we parse

         the Script \texttt{InverseZTransform}. This leads to \em ambiguous

         parse trees. \normalfont We avoid this by moving the definition

         to \ttfamily Rational.thy \normalfont and re-building {\sisac}.

         \par \noindent ATTENTION: From now on \ttfamily 

         Build\_Inverse\_Z\_Transform \normalfont mimics a build from scratch;

         it only works due to re-building {\sisac} several times (indicated 

         explicitly).

 *}

 ML {*

 (*

  *("get_denominator",

  *  ("Rational.get_denominator", eval_get_denominator ""))

  *)

 fun eval_get_denominator (thmid:string) _ 

 		      (t as Const ("Rational.get_denominator", _) $

               (Const ("Rings.divide_class.divide", _) $num 

                 $denom)) thy = 

         SOME (TermC.mk_thmid thmid (term_to_string''' thy denom) "", 

 	        HOLogic.Trueprop $ (TermC.mk_equality (t, denom)))

   | eval_get_denominator _ _ _ _ = NONE; 

 *}

 text {*\noindent For the tests of \ttfamily eval\_get\_denominator \normalfont

         see \ttfamily test/Knowledge/rational.sml\normalfont*}

 text {*\noindent \ttfamily get\_numerator \normalfont should also become a

         constant for the Isabelle parser, follow up the \texttt{const}

         declaration above.*}

 ML {*

 (*

  *("get_numerator",

  *  ("Rational.get_numerator", eval_get_numerator ""))

  *)

 fun eval_get_numerator (thmid:string) _ 

 		      (t as Const ("Rational.get_numerator", _) $

               (Const ("Rings.divide_class.divide", _) $num

                 $denom )) thy = 

         SOME (TermC.mk_thmid thmid (term_to_string''' thy num) "", 

 	        HOLogic.Trueprop $ (TermC.mk_equality (t, num)))

   | eval_get_numerator _ _ _ _ = NONE; 

 *}

 text {*\noindent We discovered several problems by implementing the 

        \ttfamily get\_numerator \normalfont function. Remember when 

        putting new functions to {\sisac}, put them in a thy file and rebuild 

        {\sisac}, also put them in the ruleset for the script!*}

 subsection {*Solve Equation\label{sec:solveq}*}

 text {*\noindent We have to find the zeros of the term, therefor we use our

        \ttfamily get\_denominator \normalfont function from the step before

        and try to solve the second order equation. (Follow up the Calculation

        in Section~\ref{sec:calc:ztrans} Subproblem 2) Note: This type of

        equation is too general for the present program.

        \par We know that this equation can be categorized as \em univariate

        equation \normalfont and solved with the functions {\sisac} provides

        for this equation type. Later on {\sisac} should determine the type

        of the given equation self.*}

 ML {*

   val denominator = TermC.parseNEW ctxt "z^^^2 - 1/4*z - 1/8 = 0";

   val fmz = ["equality (z^^^2 - 1/4*z - 1/8 = (0::real))",

              "solveFor z",

              "solutions L"];

   val (dI',pI',mI') =("Isac", ["univariate","equation"], ["no_met"]);

 *}

 text {*\noindent Check if the given equation matches the specification of this

         equation type.*}

 ML {*

   Specify.match_pbl fmz (Specify.get_pbt ["univariate","equation"]);

 *}

 text{*\noindent We switch up to the {\sisac} Context and try to solve the 

        equation with a more specific type definition.*}

 ML {*

   Context.theory_name thy = "Isac";

   val denominator = TermC.parseNEW ctxt "-1 + -2 * z + 8 * z ^^^ 2 = 0";

   val fmz =                                             (*specification*)

     ["equality (-1 + -2 * z + 8 * z ^^^ 2 = (0::real))",(*equality*)

      "solveFor z",                                      (*bound variable*)

      "solutions L"];                                    (*identifier for

                                                           solution*)

   val (dI',pI',mI') =

     ("Isac", 

       ["abcFormula","degree_2","polynomial","univariate","equation"],

       ["no_met"]);

 *}

 text {*\noindent Check if the (other) given equation matches the 

         specification of this equation type.*}

 ML {*

   Specify.match_pbl fmz (Specify.get_pbt

     ["abcFormula","degree_2","polynomial","univariate","equation"]);

 *}

 text {*\noindent We stepwise solve the equation. This is done by the

         use of a so called calc tree seen downwards.*}

 ML {*

   val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];

   val (p,_,f,nxt,_,pt) = me nxt p [] pt;

   val (p,_,f,nxt,_,pt) = me nxt p [] pt;

   val (p,_,f,nxt,_,pt) = me nxt p [] pt;

   val (p,_,f,nxt,_,pt) = me nxt p [] pt;

   val (p,_,f,nxt,_,pt) = me nxt p [] pt;

   val (p,_,f,nxt,_,pt) = me nxt p [] pt;

   val (p,_,f,nxt,_,pt) = me nxt p [] pt;

   val (p,_,f,nxt,_,pt) = me nxt p [] pt;

   val (p,_,f,nxt,_,pt) = me nxt p [] pt;

   val (p,_,f,nxt,_,pt) = me nxt p [] pt;

   val (p,_,f,nxt,_,pt) = me nxt p [] pt;         

   val (p,_,f,nxt,_,pt) = me nxt p [] pt;

   (*

    * nxt =..,Check_elementwise "Assumptions") 

    *)

   val (p,_,f,nxt,_,pt) = me nxt p [] pt;         

   val (p,_,f,nxt,_,pt) = me nxt p [] pt; f2str f;

   (*

    * [z = 1 / 2, z = -1 / 4]

    *)

   Chead.show_pt pt; 

   val SOME f = parseNEW ctxt "[z=1/2, z=-1/4]";

 *}

 subsection {*Partial Fraction Decomposition\label{sec:pbz}*}

 text{*\noindent We go on with the decomposition of our expression. Follow up the

        Calculation in Section~\ref{sec:calc:ztrans} Step~3 and later on

        Subproblem~1.*}

 subsubsection {*Solutions of the Equation*}

 text{*\noindent We get the solutions of the before solved equation in a list.*}

 ML {*

   val SOME solutions = parseNEW ctxt "[z=1/2, z=-1/4]";

   term2str solutions;

   atomty solutions;

 *}

 subsubsection {*Get Solutions out of a List*}

 text {*\noindent In {\sisac}'s TP-based programming language: 

 \begin{verbatim}

   let $ $ s_1 = NTH 1 $ solutions; $ s_2 = NTH 2... $

 \end{verbatim}

        can be useful.

        *}

 ML {*

   val Const ("List.list.Cons", _) $ s_1 $ (Const ("List.list.Cons", _)

         $ s_2 $ Const ("List.list.Nil", _)) = solutions;

   term2str s_1;

   term2str s_2;

 *}

 text{*\noindent The ansatz for the \em Partial Fraction Decomposition \normalfont

       requires to get the denominators of the partial fractions out of the 

       Solutions as:

       \begin{itemize}

         \item $Denominator_{1}=z-Zeropoint_{1}$

         \item $Denominator_{2}=z-Zeropoint_{2}$

         \item \ldots

       \end{itemize}

 *}

 ML {*

   val xx = HOLogic.dest_eq s_1;

   val s_1' = HOLogic.mk_binop "Groups.minus_class.minus" xx;

   val xx = HOLogic.dest_eq s_2;

   val s_2' = HOLogic.mk_binop "Groups.minus_class.minus" xx;

   term2str s_1';

   term2str s_2';

 *}

 text {*\noindent For the programming language a function collecting all the 

         above manipulations is helpful.*}

 ML {*

   fun fac_from_sol s =

     let val (lhs, rhs) = HOLogic.dest_eq s

     in HOLogic.mk_binop "Groups.minus_class.minus" (lhs, rhs) end;

 *}

 ML {*

   fun mk_prod prod [] =

         if prod = e_term

         then error "mk_prod called with []" 

         else prod

     | mk_prod prod (t :: []) =

         if prod = e_term

         then t

         else HOLogic.mk_binop "Groups.times_class.times" (prod, t)

     | mk_prod prod (t1 :: t2 :: ts) =

           if prod = e_term 

           then 

              let val p = 

                HOLogic.mk_binop "Groups.times_class.times" (t1, t2)

              in mk_prod p ts end 

           else 

              let val p =

                HOLogic.mk_binop "Groups.times_class.times" (prod, t1)

              in mk_prod p (t2 :: ts) end 

 *}

 (* ML {* 

 probably keep these test in test/Tools/isac/...

 (*mk_prod e_term [];*)

 val prod = mk_prod e_term [str2term "x + 123"]; 

 term2str prod = "x + 123";

 val sol = str2term "[z = 1 / 2, z = -1 / 4]";

 val sols = HOLogic.dest_list sol;

 val facs = map fac_from_sol sols;

 val prod = mk_prod e_term facs; 

 term2str prod = "(z + -1 * (1 / 2)) * (z + -1 * (-1 / 4))";

 val prod = 

   mk_prod e_term [str2term "x + 1", str2term "x + 2", str2term "x + 3"]; 

 term2str prod = "(x + 1) * (x + 2) * (x + 3)";

 *} *)

 ML {*

   fun factors_from_solution sol = 

     let val ts = HOLogic.dest_list sol

     in mk_prod e_term (map fac_from_sol ts) end;

 *}

 (* ML {*

 val sol = str2term "[z = 1 / 2, z = -1 / 4]";

 val fs = factors_from_solution sol;

 term2str fs = "(z + -1 * (1 / 2)) * (z + -1 * (-1 / 4))"

 *} *)

 text {*\noindent This function needs to be packed such that it can be evaluated

         by the Lucas-Interpreter. Therefor we moved the function to the

         corresponding \ttfamily Equation.thy \normalfont in our case

         \ttfamily PartialFractions.thy \normalfont. The necessary steps

         are quit the same as we have done with \ttfamily get\_denominator 

         \normalfont before.*}

 ML {*

   (*("factors_from_solution",

     ("Partial_Fractions.factors_from_solution",

       eval_factors_from_solution ""))*)

   fun eval_factors_from_solution (thmid:string) _

        (t as Const ("Partial_Fractions.factors_from_solution", _) $ sol)

          thy = ((let val prod = factors_from_solution sol

                    in SOME (mk_thmid thmid "" (term_to_string''' thy prod) "",

                          Trueprop $ (mk_equality (t, prod)))

                 end)

                handle _ => NONE)

    | eval_factors_from_solution _ _ _ _ = NONE;

 *}

 text {*\noindent The tracing output of the calc tree after applying this

        function was:

 \begin{verbatim}

   24 / factors_from_solution [z = 1/ 2, z = -1 / 4])]

 \end{verbatim}

        and the next step:

 \begin{verbatim}

   val nxt = ("Empty_Tac", ...): tac'_)

 \end{verbatim}

        These observations indicate, that the Lucas-Interpreter (LIP) 

        does not know how to evaluate \ttfamily factors\_from\_solution

        \normalfont, so we knew that there is something wrong or missing.

        *}

 text{*\noindent First we isolate the difficulty in the program as follows:

 \begin{verbatim}      

   " (L_L::bool list) = (SubProblem (PolyEq',      " ^

   "   [abcFormula, degree_2, polynomial,          " ^

   "    univariate,equation],                      " ^

   "   [no_met])                                   " ^

   "   [BOOL equ, REAL zzz]);                      " ^

   " (facs::real) = factors_from_solution L_L;     " ^

   " (foo::real) = Take facs                       " ^

 \end{verbatim}

       \par \noindent And see the tracing output:

 \begin{verbatim}

   [(([], Frm), Problem (Isac, [inverse, 

                                Z_Transform,

                                 SignalProcessing])),

    (([1], Frm), X z = 3 / (z - 1 / 4 + -1 / 8 * (1 / z))),

    (([1], Res), ?X' z = 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))),

    (([2], Res), ?X' z = 24 / (-1 + -2 * z + 8 * z ^^^ 2)),

    (([3], Pbl), solve (-1 + -2 * z + 8 * z ^^^ 2 = 0, z)),

    (([3,1], Frm), -1 + -2 * z + 8 * z ^^^ 2 = 0),

    (([3,1], Res), z = (- -2 + sqrt (-2 ^^^ 2 - 4 * 8 * -1)) / (2 * 8)|

                   z = (- -2 - sqrt (-2 ^^^ 2 - 4 * 8 * -1)) / (2 * 8)),

    (([3,2], Res), z = 1 / 2 | z = -1 / 4),

    (([3,3], Res), [ z = 1 / 2, z = -1 / 4]),

    (([3,4], Res), [ z = 1 / 2, z = -1 / 4]),

    (([3], Res), [ z = 1 / 2, z = -1 / 4]),

    (([4], Frm), factors_from_solution [z = 1 / 2, z = -1 / 4])]

 \end{verbatim}      

       \par \noindent In particular that:

 \begin{verbatim}

   (([3], Pbl), solve (-1 + -2 * z + 8 * z ^^^ 2 = 0, z)),

 \end{verbatim}

       \par \noindent Shows the equation which has been created in

       the program by: 

 \begin{verbatim}

   "(denom::real) = get_denominator funterm;      " ^ 

     (* get_denominator *)

   "(equ::bool) = (denom = (0::real));            " ^

 \end{verbatim}

       \noindent \ttfamily get\_denominator \normalfont has been evaluated successfully,

       but not\\ \ttfamily factors\_from\_solution.\normalfont

       So we stepwise compare with an analogous case, \ttfamily get\_denominator

       \normalfont successfully done above: We know that LIP evaluates

       expressions in the program by use of the \emph{srls}, so we try to get

       the original \emph{srls}.\\

 \begin{verbatim}

   val {srls,...} = get_met ["SignalProcessing",

                             "Z_Transform",

                             "Inverse"];

 \end{verbatim}

       \par \noindent Create 2 good example terms:

 \begin{verbatim}

 val SOME t1 =

   parseNEW ctxt "get_denominator ((111::real) / 222)";

 val SOME t2 =

   parseNEW ctxt "factors_from_solution [(z::real)=1/2, z=-1/4]";

 \end{verbatim}

       \par \noindent Rewrite the terms using srls:\\

       \ttfamily \par \noindent rewrite\_set\_ thy true srls t1;\\

         rewrite\_set\_ thy true srls t2;\\

       \par \noindent \normalfont Now we see a difference: \texttt{t1} gives

       \texttt{SOME} but \texttt{t2} gives \texttt{NONE}. We look at the 

       \emph{srls}:

 \begin{verbatim}

   val srls = 

     Rls{id = "srls_InverseZTransform",

         rules = [Calc("Rational.get_numerator",

                    eval_get_numerator "Rational.get_numerator"),

                  Calc("Partial_Fractions.factors_from_solution",

                    eval_factors_from_solution 

                      "Partial_Fractions.factors_from_solution")]}

 \end{verbatim}                

       \par \noindent Here everthing is perfect. So the error can

       only be in the SML code of \ttfamily eval\_factors\_from\_solution.

       \normalfont We try to check the code with an existing test; since the 

       \emph{code} is in 

       \begin{center}\ttfamily src/Tools/isac/Knowledge/Partial\_Fractions.thy

       \normalfont\end{center}

       the \emph{test} should be in

       \begin{center}\ttfamily test/Tools/isac/Knowledge/partial\_fractions.sml

       \normalfont\end{center}

       \par \noindent After updating the function \ttfamily

       factors\_from\_solution \normalfont to a new version and putting a

       test-case to \ttfamily Partial\_Fractions.sml \normalfont we tried again

       to evaluate the term with the same result.

       \par We opened the test \ttfamily Test\_Isac.thy \normalfont and saw that

       everything is working fine. Also we checked that the test \ttfamily 

       partial\_fractions.sml \normalfont is used in \ttfamily Test\_Isac.thy 

       \normalfont

       \begin{center}use \ttfamily "Knowledge/partial\_fractions.sml"

       \normalfont \end{center}

       and \ttfamily Partial\_Fractions.thy \normalfont is part is part of

       {\sisac} by evaluating

 \begin{verbatim}

   val thy = @{theory "Inverse_Z_Transform"};

 \end{verbatim}

       After rebuilding {\sisac} again it worked.

 *}

 subsubsection {*Build Expression*}

 text {*\noindent In {\sisac}'s TP-based programming language we can build

        expressions by:\\

        \ttfamily let s\_1 = Take numerator / (s\_1 * s\_2) \normalfont*}

 ML {*

   (*

    * The main denominator is the multiplication of the denominators of

    * all partial fractions.

    *)

   val denominator' = HOLogic.mk_binop 

     "Groups.times_class.times" (s_1', s_2') ;

   val SOME numerator = parseNEW ctxt "3::real";

   val expr' = HOLogic.mk_binop

     "Rings.divide_class.divide" (numerator, denominator');

   term2str expr';

 *}

 subsubsection {*Apply the Partial Fraction Decomposion Ansatz*}

 text{*\noindent We use the Ansatz of the Partial Fraction Decomposition for our

       expression 2nd order. Follow up the calculation in 

       Section~\ref{sec:calc:ztrans} Step~03.*}

 ML {*Context.theory_name thy = "Isac"*}

 text{*\noindent We define two axiomatization, the first one is the main ansatz,

       the next one is just an equivalent transformation of the resulting

       equation. Both axiomatizations were moved to \ttfamily

       Partial\_Fractions.thy \normalfont and got their own rulesets. In later

       programs it is possible to use the rulesets and the machine will find

       the correct ansatz and equivalent transformation itself.*}

 axiomatization where

   ansatz_2nd_order: "n / (a*b) = A/a + B/b" and

   equival_trans_2nd_order: "(n/(a*b) = A/a + B/b) = (n = A*b + B*a)"

 text{*\noindent We use our \ttfamily ansatz\_2nd\_order \normalfont to rewrite

        our expression and get an equation with our expression on the left

        and the partial fractions of it on the right hand side.*}

 ML {*

   val SOME (t1,_) = 

     rewrite_ @{theory} e_rew_ord e_rls false 

              @{thm ansatz_2nd_order} expr';

   term2str t1; atomty t1;

   val eq1 = HOLogic.mk_eq (expr', t1);

   term2str eq1;

 *}

 text{*\noindent Eliminate the denominators by multiplying the left and the

       right hand side of the equation with the main denominator. This is an

       simple equivalent transformation. Later on we use an own ruleset

       defined in \ttfamily Partial\_Fractions.thy \normalfont for doing this.

       Follow up the calculation in Section~\ref{sec:calc:ztrans} Step~04.*}

 ML {*

   val SOME (eq2,_) = 

     rewrite_ @{theory} e_rew_ord e_rls false 

              @{thm equival_trans_2nd_order} eq1;

   term2str eq2;

 *}

 text{*\noindent We use the existing ruleset \ttfamily norm\_Rational \normalfont 

      for simplifications on expressions.*}

 ML {*

   val SOME (eq3,_) = rewrite_set_ @{theory} false norm_Rational eq2;

   term2str eq3;

   (*

    * ?A ?B not simplified

    *)

 *}

 text{*\noindent In Example~\ref{eg:gap} of my thesis I'm describing a problem about

       simplifications. The problem that we would like to have only a specific degree

       of simplification occurs right here, in the next step.*}

 ML {*

   trace_rewrite := false;

   val SOME fract1 =

     parseNEW ctxt "(z - 1/2)*(z - -1/4) * (A/(z - 1/2) + B/(z - -1/4))";

   (*

    * A B !

    *)

   val SOME (fract2,_) = 

     rewrite_set_ @{theory} false norm_Rational fract1;

   term2str fract2 = "(A + -2 * B + 4 * A * z + 4 * B * z) / 4";

   (*

    * term2str fract2 = "A * (1 / 4 + z) + B * (-1 / 2 + z)" 

    * would be more traditional...

    *)

 *}

 text{*\noindent We walk around this problem by generating our new equation first.*}

 ML {*

   val (numerator, denominator) = HOLogic.dest_eq eq3;

   val eq3' = HOLogic.mk_eq (numerator, fract1);

   (*

    * A B !

    *)

   term2str eq3';

   (*

    * MANDATORY: simplify (and remove denominator) otherwise 3 = 0

    *)

   val SOME (eq3'' ,_) = 

     rewrite_set_ @{theory} false norm_Rational eq3';

   term2str eq3'';

 *}

 text{*\noindent Still working at {\sisac}\ldots*}

 ML {* Context.theory_name thy = "Isac" *}

 subsubsection {*Build a Rule-Set for the Ansatz*}

 text {*\noindent The \emph{ansatz} rules violate the principle that each

        variable on the right-hand-side must also occur on the

        left-hand-side of the rule: A, B, etc. don't do that. Thus the

        rewriter marks these variables with question marks: ?A, ?B, etc.

        These question marks can be dropped by \ttfamily fun

        drop\_questionmarks\normalfont.*}

 ML {*

   val ansatz_rls = prep_rls @{theory} (

     Rls {id = "ansatz_rls", preconds = [], rew_ord = ("dummy_ord",dummy_ord),

       erls = e_rls, srls = Erls, calc = [], errpatts = [],

       rules = [

         Thm ("ansatz_2nd_order",num_str @{thm ansatz_2nd_order}),

         Thm ("equival_trans_2nd_order",num_str @{thm equival_trans_2nd_order})

               ], 

       scr = EmptyScr});

 *}

 text{*\noindent We apply the ruleset\ldots*}

 ML {*

   val SOME (ttttt,_) = 

     rewrite_set_ @{theory} false ansatz_rls expr';

 *}

 text{*\noindent And check the output\ldots*}

 ML {*

   term2str expr' = "3 / ((z - 1 / 2) * (z - -1 / 4))";

   term2str ttttt = "?A / (z - 1 / 2) + ?B / (z - -1 / 4)";

 *}

 subsubsection {*Get the First Coefficient*}

 text{*\noindent Now it's up to get the two coefficients A and B, which will be

       the numerators of our partial fractions. Continue following up the 

       Calculation in Section~\ref{sec:calc:ztrans} Subproblem~1.*}

 text{*\noindent To get the first coefficient we substitute $z$ with the first

       zero-point we determined in Section~\ref{sec:solveq}.*}

 ML {*

   val SOME (eq4_1,_) =

     rewrite_terms_ @{theory} e_rew_ord e_rls [s_1] eq3'';

   term2str eq4_1;

   val SOME (eq4_2,_) =

     rewrite_set_ @{theory} false norm_Rational eq4_1;

   term2str eq4_2;

   val fmz = ["equality (3=3*A/(4::real))", "solveFor A","solutions L"];

   val (dI',pI',mI') =("Isac", ["univariate","equation"], ["no_met"]);

   (*

    * Solve the simple linear equation for A:

    * Return eq, not list of eq's

    *)

   val (p,_,fa,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];

   val (p,_,fa,nxt,_,pt) = me nxt p [] pt;

     (*Add_Given "equality (3=3*A/4)"*)

   val (p,_,fa,nxt,_,pt) = me nxt p [] pt;

     (*Add_Given "solveFor A"*)

   val (p,_,fa,nxt,_,pt) = me nxt p [] pt; 

     (*Add_Find "solutions L"*)

   val (p,_,fa,nxt,_,pt) = me nxt p [] pt;

     (*Specify_Theory "Isac"*)

   val (p,_,fa,nxt,_,pt) = me nxt p [] pt;

     (*Specify_Problem ["normalise","polynomial",

                        "univariate","equation"])*)

   val (p,_,fa,nxt,_,pt) = me nxt p [] pt;

     (* Specify_Method["PolyEq","normalise_poly"]*)

   val (p,_,fa,nxt,_,pt) = me nxt p [] pt;

     (*Apply_Method["PolyEq","normalise_poly"]*)

   val (p,_,fa,nxt,_,pt) = me nxt p [] pt;

     (*Rewrite ("all_left","PolyEq.all_left")*)

   val (p,_,fa,nxt,_,pt) = me nxt p [] pt;

     (*Rewrite_Set_Inst(["(bdv,A)"],"make_ratpoly_in")*)

   val (p,_,fa,nxt,_,pt) = me nxt p [] pt;

     (*Rewrite_Set "polyeq_simplify"*)

   val (p,_,fa,nxt,_,pt) = me nxt p [] pt; 

   val (p,_,fa,nxt,_,pt) = me nxt p [] pt; 

   val (p,_,fa,nxt,_,pt) = me nxt p [] pt;

     (*Add_Given "equality (3 + -3 / 4 * A =0)"*)

   val (p,_,fa,nxt,_,pt) = me nxt p [] pt;

     (*Add_Given "solveFor A"*)

   val (p,_,fa,nxt,_,pt) = me nxt p [] pt;

     (*Add_Find "solutions A_i"*)

   val (p,_,fa,nxt,_,pt) = me nxt p [] pt; 

   val (p,_,fa,nxt,_,pt) = me nxt p [] pt; 

   val (p,_,fa,nxt,_,pt) = me nxt p [] pt; 

   val (p,_,fa,nxt,_,pt) = me nxt p [] pt; 

     (*Apply_Method ["PolyEq","solve_d1_polyeq_equation"]*)

   val (p,_,fa,nxt,_,pt) = me nxt p [] pt;

     (*Rewrite_Set_Inst(["(bdv,A)"],"d1_polyeq_simplify")*)

   val (p,_,fa,nxt,_,pt) = me nxt p [] pt;

     (*Rewrite_Set "polyeq_simplify"*)

   val (p,_,fa,nxt,_,pt) = me nxt p [] pt;

     (*Rewrite_Set "norm_Rational_parenthesized"*)

   val (p,_,fa,nxt,_,pt) = me nxt p [] pt;

     (*Or_to_List*)

   val (p,_,fa,nxt,_,pt) = me nxt p [] pt;

     (*Check_elementwise "Assumptions"*)

   val (p,_,fa,nxt,_,pt) = me nxt p [] pt;

     (*Check_Postcond ["degree_1","polynomial",

                       "univariate","equation"]*)

   val (p,_,fa,nxt,_,pt) = me nxt p [] pt;

     (*Check_Postcond ["normalise","polynomial",

                       "univariate","equation"]*)

   val (p,_,fa,nxt,_,pt) = me nxt p [] pt;

     (*End_Proof'*)

   f2str fa;

 *}

 subsubsection {*Get Second Coefficient*}

 text{*\noindent With the use of \texttt{thy} we check which theories the 

       interpreter knows.*}

 ML {*thy*}

 text{*\noindent To get the second coefficient we substitute $z$ with the second

       zero-point we determined in Section~\ref{sec:solveq}.*}

 ML {*

   val SOME (eq4b_1,_) =

     rewrite_terms_ @{theory} e_rew_ord e_rls [s_2] eq3'';

   term2str eq4b_1;

   val SOME (eq4b_2,_) =

     rewrite_set_ @{theory} false norm_Rational eq4b_1;

   term2str eq4b_2;

   val fmz = ["equality (3= -3*B/(4::real))", "solveFor B","solutions L"];

   val (dI',pI',mI') =("Isac", ["univariate","equation"], ["no_met"]);

   val (p,_,fb,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];

   val (p,_,fb,nxt,_,pt) = me nxt p [] pt;

   val (p,_,fb,nxt,_,pt) = me nxt p [] pt;

   val (p,_,fb,nxt,_,pt) = me nxt p [] pt;

   val (p,_,fb,nxt,_,pt) = me nxt p [] pt;

   val (p,_,fb,nxt,_,pt) = me nxt p [] pt;

   val (p,_,fb,nxt,_,pt) = me nxt p [] pt;

   val (p,_,fb,nxt,_,pt) = me nxt p [] pt;

   val (p,_,fb,nxt,_,pt) = me nxt p [] pt;

   val (p,_,fb,nxt,_,pt) = me nxt p [] pt;

   val (p,_,fb,nxt,_,pt) = me nxt p [] pt;

   val (p,_,fb,nxt,_,pt) = me nxt p [] pt;

   val (p,_,fb,nxt,_,pt) = me nxt p [] pt;

   val (p,_,fb,nxt,_,pt) = me nxt p [] pt;

   val (p,_,fb,nxt,_,pt) = me nxt p [] pt;

   val (p,_,fb,nxt,_,pt) = me nxt p [] pt;

   val (p,_,fb,nxt,_,pt) = me nxt p [] pt;

   val (p,_,fb,nxt,_,pt) = me nxt p [] pt;

   val (p,_,fb,nxt,_,pt) = me nxt p [] pt;

   val (p,_,fb,nxt,_,pt) = me nxt p [] pt;

   val (p,_,fb,nxt,_,pt) = me nxt p [] pt;

   val (p,_,fb,nxt,_,pt) = me nxt p [] pt;

   val (p,_,fb,nxt,_,pt) = me nxt p [] pt;

   val (p,_,fb,nxt,_,pt) = me nxt p [] pt;

   val (p,_,fb,nxt,_,pt) = me nxt p [] pt;

   val (p,_,fb,nxt,_,pt) = me nxt p [] pt;

   val (p,_,fb,nxt,_,pt) = me nxt p [] pt;

   val (p,_,fb,nxt,_,pt) = me nxt p [] pt; 

   f2str fb;

 *}

 text{*\noindent We compare our results with the pre calculated upshot.*}

 ML {*

   if f2str fa = "[A = 4]" then () else error "part.fract. eq4_1";

   if f2str fb = "[B = -4]" then () else error "part.fract. eq4_1";

 *}

 section {*Implement the Specification and the Method \label{spec-meth}*}

 text{*\noindent Now everything we need for solving the problem has been

       tested out. We now start by creating new nodes for our methods and

       further on our new program in the interpreter.*}

 subsection{*Define the Field Descriptions for the 

             Specification\label{sec:deffdes}*}

 text{*\noindent We define the fields \em filterExpression \normalfont and

       \em stepResponse \normalfont both as equations, they represent the in- and

       output of the program.*}

 consts

   filterExpression  :: "bool => una"

   stepResponse      :: "bool => una"

 subsection{*Define the Specification*}

 text{*\noindent The next step is defining the specifications as nodes in the

       designated part. We have to create the hierarchy node by node and start

       with \em SignalProcessing \normalfont and go on by creating the node

       \em Z\_Transform\normalfont.*}

 setup {* KEStore_Elems.add_pbts

   [prep_pbt thy "pbl_SP" [] e_pblID (["SignalProcessing"], [], e_rls, NONE, []),

     prep_pbt thy "pbl_SP_Ztrans" [] e_pblID

       (["Z_Transform","SignalProcessing"], [], e_rls, NONE, [])] *}

 text{*\noindent For the suddenly created node we have to define the input

        and output parameters. We already prepared their definition in

        Section~\ref{sec:deffdes}.*}

 setup {* KEStore_Elems.add_pbts

   [prep_pbt thy "pbl_SP_Ztrans_inv" [] e_pblID

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

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

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

         append_rls "e_rls" e_rls [(*for preds in where_*)],

         NONE,

         [["SignalProcessing","Z_Transform","Inverse"]])] *}

 ML {*

   show_ptyps ();

   get_pbt ["Inverse","Z_Transform","SignalProcessing"];

 *}

 subsection {*Define Name and Signature for the Method*}

 text{*\noindent As a next step we store the definition of our new method as a

       constant for the interpreter.*}

 consts

   InverseZTransform :: "[bool, bool] => bool"

     ("((Script InverseZTransform (_ =))// (_))" 9)

 subsection {*Setup Parent Nodes in Hierarchy of Method\label{sec:cparentnode}*}

 text{*\noindent Again we have to generate the nodes step by step, first the

       parent node and then the originally \em Z\_Transformation 

       \normalfont node. We have to define both nodes first with an empty script

       as content.*}

 setup {* KEStore_Elems.add_mets

   [prep_met thy "met_SP" [] e_metID

       (["SignalProcessing"], [],

         {rew_ord'="tless_true", rls'= e_rls, calc = [], srls = e_rls, prls = e_rls, crls = e_rls,

           errpats = [], nrls = e_rls},

         "empty_script"),

     prep_met thy "met_SP_Ztrans" [] e_metID

       (["SignalProcessing", "Z_Transform"], [],

         {rew_ord'="tless_true", rls'= e_rls, calc = [], srls = e_rls, prls = e_rls, crls = e_rls,

           errpats = [], nrls = e_rls},

         "empty_script")]

 *}

 text{*\noindent After we generated both nodes, we can fill the containing

       script we want to implement later. First we define the specifications

       of the script in e.g. the in- and output.*}

 setup {* KEStore_Elems.add_mets

   [prep_met thy "met_SP_Ztrans_inv" [] e_metID

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

         [("#Given" ,["filterExpression X_eq"]), ("#Find"  ,["stepResponse n_eq"])],

         {rew_ord'="tless_true", rls'= e_rls, calc = [], srls = e_rls, prls = e_rls, crls = e_rls,

           errpats = [], nrls = e_rls},

         "empty_script")]

 *}

 text{*\noindent After we stored the definition we can start implementing the

       script itself. As a first try we define only three rows containing one

       simple operation.*}

 setup {* KEStore_Elems.add_mets

   [prep_met thy "met_SP_Ztrans_inv" [] e_metID

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

         [("#Given" ,["filterExpression X_eq"]), ("#Find"  ,["stepResponse n_eq"])],

         {rew_ord'="tless_true", rls'= e_rls, calc = [], srls = e_rls, prls = e_rls, crls = e_rls,

           errpats = [], nrls = e_rls},

         "Script InverseZTransform (Xeq::bool) =" ^

           " (let X = Take Xeq;" ^

           "      X = Rewrite ruleZY False X" ^

           "  in X)")]

 *}

 text{*\noindent Check if the method has been stored correctly\ldots*}

 ML {*

   show_mets(); 

 *}

 text{*\noindent If yes we can get the method by stepping backwards through

       the hierarchy.*}

 ML {*

   get_met ["SignalProcessing","Z_Transform","Inverse"];

 *}

 section {*Program in TP-based language \label{prog-steps}*}

 text{*\noindent We start stepwise expanding our program. The script is a

       simple string containing several manipulation instructions.

       \par The first script we try contains no instruction, we only test if

       building scripts that way work.*}

 subsection {*Stepwise Extend the Program*}

 ML {*

   val str = 

     "Script InverseZTransform (Xeq::bool) =                          "^

     " Xeq";

 *}

 text{*\noindent Next we put some instructions in the script and try if we are

       able to solve our first equation.*}

 ML {*

   val str = 

     "Script InverseZTransform (Xeq::bool) =                          "^

     (*

      * 1/z) instead of z ^^^ -1

      *)

     " (let X = Take Xeq;                                             "^

     "      X' = Rewrite ruleZY False X;                              "^

     (*

      * z * denominator

      *)

     "      X' = (Rewrite_Set norm_Rational False) X'                 "^

     (*

      * simplify

      *)

     "  in X)";

     (*

      * NONE

      *)

     "Script InverseZTransform (Xeq::bool) =                          "^

     (*

      * (1/z) instead of z ^^^ -1

      *)

     " (let X = Take Xeq;                                             "^

     "      X' = Rewrite ruleZY False X;                              "^

     (*

      * z * denominator

      *)

     "      X' = (Rewrite_Set norm_Rational False) X';                "^

     (*

      * simplify

      *)

     "      X' = (SubProblem (Isac',[pqFormula,degree_2,              "^

     "                               polynomial,univariate,equation], "^

     "                              [no_met])                         "^

     "                              [BOOL e_e, REAL v_v])             "^

     "            in X)";

 *}

 text{*\noindent To solve the equation it is necessary to drop the left hand

       side, now we only need the denominator of the right hand side. The first

       equation solves the zeros of our expression.*}

 ML {*

   val str = 

     "Script InverseZTransform (Xeq::bool) =                          "^

     " (let X = Take Xeq;                                             "^

     "      X' = Rewrite ruleZY False X;                              "^

     "      X' = (Rewrite_Set norm_Rational False) X';                "^

     "      funterm = rhs X'                                          "^

     (*

      * drop X'= for equation solving

      *)

     "  in X)";

 *}

 text{*\noindent As mentioned above, we need the denominator of the right hand

       side. The equation itself consists of this denominator and tries to find

       a $z$ for this the denominator is equal to zero.*}

 ML {*

   val str = 

     "Script InverseZTransform (X_eq::bool) =                         "^

     " (let X = Take X_eq;                                            "^

     "      X' = Rewrite ruleZY False X;                              "^

     "      X' = (Rewrite_Set norm_Rational False) X';                "^

     "      (X'_z::real) = lhs X';                                    "^

     "      (z::real) = argument_in X'_z;                             "^

     "      (funterm::real) = rhs X';                                 "^

     "      (denom::real) = get_denominator funterm;                  "^

     (*

      * get_denominator

      *)

     "      (equ::bool) = (denom = (0::real));                        "^

     "      (L_L::bool list) =                                        "^

     "            (SubProblem (Test',                                 "^

     "                         [LINEAR,univariate,equation,test],     "^

     "                         [Test,solve_linear])                   "^

     "                         [BOOL equ, REAL z])                    "^

     "  in X)";

   parse thy str;

   val sc = (inst_abs o Thm.term_of o the o (parse thy)) str;

   atomty sc;

 *}

 text {*\noindent This ruleset contains all functions that are in the script; 

        The evaluation of the functions is done by rewriting using this ruleset.*}

 ML {*

   val srls = 

     Rls {id="srls_InverseZTransform", 

          preconds = [],

          rew_ord = ("termlessI",termlessI),

          erls = append_rls "erls_in_srls_InverseZTransform" e_rls

            [(*for asm in NTH_CONS ...*)

             Calc ("Orderings.ord_class.less",eval_equ "#less_"),

             (*2nd NTH_CONS pushes n+-1 into asms*)

             Calc("Groups.plus_class.plus", eval_binop "#add_")

            ], 

          srls = Erls, calc = [], errpatts = [],

          rules = [

                   Thm ("NTH_CONS",num_str @{thm NTH_CONS}),

                   Calc("Groups.plus_class.plus", 

                        eval_binop "#add_"),

                   Thm ("NTH_NIL",num_str @{thm NTH_NIL}),

                   Calc("Tools.lhs", eval_lhs"eval_lhs_"),

                   Calc("Tools.rhs", eval_rhs"eval_rhs_"),

                   Calc("Atools.argument'_in",

                        eval_argument_in "Atools.argument'_in"),

                   Calc("Rational.get_denominator",

                        eval_get_denominator "#get_denominator"),

                   Calc("Rational.get_numerator",

                        eval_get_numerator "#get_numerator"),

                   Calc("Partial_Fractions.factors_from_solution",

                        eval_factors_from_solution 

                          "#factors_from_solution"),

                   Calc("Partial_Fractions.drop_questionmarks",

                        eval_drop_questionmarks "#drop_?")

                  ],

          scr = EmptyScr};

 *}

 subsection {*Store Final Version of Program for Execution*}

 text{*\noindent After we also tested how to write scripts and run them,

       we start creating the final version of our script and store it into

       the method for which we created a node in Section~\ref{sec:cparentnode}

       Note that we also did this stepwise, but we didn't kept every

       subversion.*}

 setup {* KEStore_Elems.add_mets

   [prep_met thy "met_SP_Ztrans_inv" [] e_metID

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

         [("#Given" ,["filterExpression X_eq"]), ("#Find"  ,["stepResponse n_eq"])],

         {rew_ord'="tless_true", rls'= e_rls, calc = [], srls = srls, prls = e_rls, crls = e_rls,

           errpats = [], nrls = e_rls},

         "Script InverseZTransform (X_eq::bool) =                        "^

           (*(1/z) instead of z ^^^ -1*)

           "(let X = Take X_eq;                                            "^

           "      X' = Rewrite ruleZY False X;                             "^

           (*z * denominator*)

           "      (num_orig::real) = get_numerator (rhs X');               "^

           "      X' = (Rewrite_Set norm_Rational False) X';               "^

           (*simplify*)

           "      (X'_z::real) = lhs X';                                   "^

           "      (zzz::real) = argument_in X'_z;                          "^

           "      (funterm::real) = rhs X';                                "^

           (*drop X' z = for equation solving*)

           "      (denom::real) = get_denominator funterm;                 "^

           (*get_denominator*)

           "      (num::real) = get_numerator funterm;                     "^

           (*get_numerator*)

           "      (equ::bool) = (denom = (0::real));                       "^

           "      (L_L::bool list) = (SubProblem (PolyEq',                 "^

           "         [abcFormula,degree_2,polynomial,univariate,equation], "^

           "         [no_met])                                             "^

           "         [BOOL equ, REAL zzz]);                                "^

           "      (facs::real) = factors_from_solution L_L;                "^

           "      (eql::real) = Take (num_orig / facs);                    "^ 

           "      (eqr::real) = (Try (Rewrite_Set ansatz_rls False)) eql;  "^

           "      (eq::bool) = Take (eql = eqr);                           "^

           (*Maybe possible to use HOLogic.mk_eq ??*)

           "      eq = (Try (Rewrite_Set equival_trans False)) eq;         "^ 

           "      eq = drop_questionmarks eq;                              "^

           "      (z1::real) = (rhs (NTH 1 L_L));                          "^

           (* 

           * prepare equation for a - eq_a

           * therefor substitute z with solution 1 - z1

           *)

           "      (z2::real) = (rhs (NTH 2 L_L));                          "^

           "      (eq_a::bool) = Take eq;                                  "^

           "      eq_a = (Substitute [zzz=z1]) eq;                         "^

           "      eq_a = (Rewrite_Set norm_Rational False) eq_a;           "^

           "      (sol_a::bool list) =                                     "^

           "                 (SubProblem (Isac',                           "^

           "                              [univariate,equation],[no_met])  "^

           "                              [BOOL eq_a, REAL (A::real)]);    "^

           "      (a::real) = (rhs(NTH 1 sol_a));                          "^

           "      (eq_b::bool) = Take eq;                                  "^

           "      eq_b =  (Substitute [zzz=z2]) eq_b;                      "^

           "      eq_b = (Rewrite_Set norm_Rational False) eq_b;           "^

           "      (sol_b::bool list) =                                     "^

           "                 (SubProblem (Isac',                           "^

           "                              [univariate,equation],[no_met])  "^

           "                              [BOOL eq_b, REAL (B::real)]);    "^

           "      (b::real) = (rhs(NTH 1 sol_b));                          "^

           "      eqr = drop_questionmarks eqr;                            "^

           "      (pbz::real) = Take eqr;                                  "^

           "      pbz = ((Substitute [A=a, B=b]) pbz);                     "^

           "      pbz = Rewrite ruleYZ False pbz;                          "^

           "      pbz = drop_questionmarks pbz;                            "^

           "      (X_z::bool) = Take (X_z = pbz);                          "^

           "      (n_eq::bool) = (Rewrite_Set inverse_z False) X_z;        "^

           "      n_eq = drop_questionmarks n_eq                           "^

           "in n_eq)")]

 *}

 subsection {*Check the Program*}

 text{*\noindent When the script is ready we can start checking our work.*}

 subsubsection {*Check the Formalization*}

 text{*\noindent First we want to check the formalization of the in and

        output of our program.*}

 ML {*

   val fmz = 

     ["filterExpression (X  = 3 / (z - 1/4 + -1/8 * (1/(z::real))))",

      "stepResponse (x[n::real]::bool)"];

   val (dI,pI,mI) = 

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

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

   val ([

           (

             1,

             [1],

             "#Given",

             Const ("Inverse_Z_Transform.filterExpression", _),

             [Const ("HOL.eq", _) $ _ $ _]

           ),

           (

             2,

             [1],

             "#Find",

             Const ("Inverse_Z_Transform.stepResponse", _),

             [Free ("x", _) $ _]

           )

        ],_

       ) = prep_ori fmz thy ((#ppc o get_pbt) pI);

   val Prog sc 

     = (#scr o get_met) ["SignalProcessing",

                         "Z_Transform",

                         "Inverse"];

   atomty sc;

 *}

 subsubsection {*Stepwise Check the Program\label{sec:stepcheck}*}

 text{*\noindent We start to stepwise execute our new program in a calculation

       tree and check if every node implements that what we have wanted.*}

 ML {*

   trace_rewrite := false; (*true*)

   trace_script := false; (*true*)

   print_depth 9;

   val fmz =

     ["filterExpression (X z = 3 / ((z::real) + 1/10 - 1/50*(1/z)))",

      "stepResponse (x[n::real]::bool)"];

   val (dI,pI,mI) =

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

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

   val (p,_,f,nxt,_,pt)  = CalcTreeTEST [(fmz, (dI,pI,mI))];

   val (p,_,f,nxt,_,pt) = me nxt p [] pt; 

     "Add_Given";

   val (p,_,f,nxt,_,pt) = me nxt p [] pt;

     "Add_Find";

   val (p,_,f,nxt,_,pt) = me nxt p [] pt;

     "Specify_Theory";

   val (p,_,f,nxt,_,pt) = me nxt p [] pt;

     "Specify_Problem";

   val (p,_,f,nxt,_,pt) = me nxt p [] pt;

     "Specify_Method";

   val (p,_,f,nxt,_,pt) = me nxt p [] pt;

     "Apply_Method";

   val (p,_,f,nxt,_,pt) = me nxt p [] pt;

     "Rewrite (ruleZY, Inverse_Z_Transform.ruleZY)";

     "--> X z = 3 / (z - 1 / 4 + -1 / 8 * (1 / z))";

   (*

    * TODO naming!

    *)

   val (p,_,f,nxt,_,pt) = me nxt p [] pt;

     "Rewrite_Set norm_Rational";

     " --> X' z = 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))";

   val (p,_,f,nxt,_,pt) = me nxt p [] pt; 

     "SubProblem";

   print_depth 3;

 *}

 text {*\noindent Instead of \ttfamily nxt = Subproblem \normalfont above we had

        \ttfamily Empty\_Tac; \normalfont the search for the reason considered

        the following points:\begin{itemize}

        \item What shows \ttfamily show\_pt pt;\normalfont\ldots?

 \begin{verbatim}(([2], Res), ?X' z = 24 / (-1 + -2 * z + 8 * z ^^^ 2))]\end{verbatim}

          The calculation is ok but no \ttfamily next \normalfont step found:

          Should be\\ \ttfamily nxt = Subproblem\normalfont!

        \item What shows \ttfamily trace\_script := true; \normalfont we read

          bottom up\ldots

      \begin{verbatim}

      @@@next leaf 'SubProblem

      (PolyEq',[abcFormula, degree_2, polynomial, 

                univariate, equation], no_meth)

      [BOOL equ, REAL z]' 

        ---> STac 'SubProblem (PolyEq',

               [abcFormula, degree_2, polynomial,

                univariate, equation], no_meth)

      [BOOL (-1 + -2 * z + 8 * z \^\^\^ ~2 = 0), REAL z]'

      \end{verbatim}

          We see the SubProblem with correct arguments from searching next

          step (program text !!!--->!!! STac (script tactic) with arguments

          evaluated.)

      \item Do we have the right Script \ldots difference in the

          arguments in the arguments\ldots

          \begin{verbatim}

      val Prog s =

      (#scr o get_met) ["SignalProcessing",

                        "Z_Transform",

                        "Inverse"];

      writeln (term2str s);

          \end{verbatim}

          \ldots shows the right script. Difference in the arguments.

      \item Test --- Why helpless here ? --- shows: \ttfamily replace

          no\_meth by [no\_meth] \normalfont in Script

      \end{itemize}

 *}

 ML {*

   val (p,_,f,nxt,_,pt) = me nxt p [] pt; 

     (*Model_Problem";*)

 *}

 text {*\noindent Instead of \ttfamily nxt = Model\_Problem \normalfont above

        we had \ttfamily Empty\_Tac; \normalfont the search for the reason 

        considered the following points:\begin{itemize}

        \item Difference in the arguments

        \item Comparison with Subsection~\ref{sec:solveq}: There solving this

          equation works, so there must be some difference in the arguments

          of the Subproblem: RIGHT: we had \ttfamily [no\_meth] \normalfont

          instead of \ttfamily [no\_met] \normalfont ;-)

        \end{itemize}*}

 ML {*

   val (p,_,f,nxt,_,pt) = me nxt p [] pt;

     (*Add_Given equality (-1 + -2 * z + 8 * z ^^^ 2 = 0)";*)

   val (p,_,f,nxt,_,pt) = me nxt p [] pt;

     (*Add_Given solveFor z";*)

   val (p,_,f,nxt,_,pt) = me nxt p [] pt;

     (*Add_Find solutions z_i";*)

   val (p,_,f,nxt,_,pt) = me nxt p [] pt;

     (*Specify_Theory Isac";*)

 *}

 text {*\noindent We had \ttfamily nxt = Empty\_Tac instead Specify\_Theory;

        \normalfont The search for the reason considered the following points:

        \begin{itemize}

        \item Was there an error message? NO -- ok

        \item Has \ttfamily nxt = Add\_Find \normalfont been inserted in pt:\\

          \ttfamily get\_obj g\_pbl pt (fst p);\normalfont? YES -- ok

        \item What is the returned formula:

 \begin{verbatim}

 print_depth 999; f; print_depth 3;

 { Find = [ Correct "solutions z_i"],

   With = [],

   Given = [Correct "equality (-1 + -2*z + 8*z ^^^ 2 = 0)",

            Correct "solveFor z"],

   Where = [...],

   Relate = [] }

 \end{verbatim}

      \normalfont The only False is the reason: the Where (the precondition) is

      False for good reasons: The precondition seems to check for linear

      equations, not for the one we want to solve! Removed this error by

      correcting the Script from \ttfamily SubProblem (PolyEq',

      \lbrack linear,univariate,equation,

        test\rbrack, \lbrack Test,solve\_linear\rbrack \normalfont to

      \ttfamily SubProblem (PolyEq',\\ \lbrack abcFormula,degree\_2,

        polynomial,univariate,equation\rbrack,\\

                    \lbrack PolyEq,solve\_d2\_polyeq\_abc\_equation

                    \rbrack\normalfont

      You find the appropriate type of equation at the

      {\sisac}-WEB-Page\footnote{

      \href{http://www.ist.tugraz.at/projects/isac/www/kbase/pbl/index\_pbl.html}

           {http://www.ist.tugraz.at/projects/isac/www/kbase/pbl/index\_pbl.html}

                                }

      And the respective method in \ttfamily Knowledge/PolyEq.thy \normalfont

      at the respective \ttfamily store\_pbt. \normalfont Or you leave the

      selection of the appropriate type to isac as done in the final Script ;-))

   \end{itemize}*}

 ML {*

   val (p,_,f,nxt,_,pt) = me nxt p [] pt; 

     (*Specify_Problem [abcFormula,...";*)

   val (p,_,f,nxt,_,pt) = me nxt p [] pt;

     (*Specify_Method [PolyEq,solve_d2_polyeq_abc_equation";*)

   val (p,_,f,nxt,_,pt) = me nxt p [] pt; 

     (*Apply_Method [PolyEq,solve_d2_polyeq_abc_equation";*)

   val (p,_,f,nxt,_,pt) = me nxt p [] pt;

     (*Rewrite_Set_Inst ([(bdv, z)], d2_polyeq_abcFormula_simplify";*)

   val (p,_,f,nxt,_,pt) = me nxt p [] pt;

   val (p,_,f,nxt,_,pt) = me nxt p [] pt;

   val (p,_,f,nxt,_,pt) = me nxt p [] pt;

   val (p,_,f,nxt,_,pt) = me nxt p [] pt;

   val (p,_,f,nxt,_,pt) = me nxt p [] pt;

   val (p,_,f,nxt,_,pt) = me nxt p [] pt;

   val (p,_,f,nxt,_,pt) = me nxt p [] pt;

   val (p,_,f,nxt,_,pt) = me nxt p [] pt;

   val (p,_,f,nxt,_,pt) = me nxt p [] pt;

   val (p,_,f,nxt,_,pt) = me nxt p [] pt;

   val (p,_,f,nxt,_,pt) = me nxt p [] pt;

   val (p,_,f,nxt,_,pt) = me nxt p [] pt;

   val (p,_,f,nxt,_,pt) = me nxt p [] pt;

   val (p,_,f,nxt,_,pt) = me nxt p [] pt;

   val (p,_,f,nxt,_,pt) = me nxt p [] pt;

   val (p,_,f,nxt,_,pt) = me nxt p [] pt;

   val (p,_,f,nxt,_,pt) = me nxt p [] pt;

     (*Specify_Problem ["normalise","polynomial","univariate","equation"]*)

   val (p,_,f,nxt,_,pt) = me nxt p [] pt;

     (*Specify_Method ["PolyEq", "normalise_poly"]*)

   val (p,_,f,nxt,_,pt) = me nxt p [] pt;

     (*Apply_Method ["PolyEq", "normalise_poly"]*)

   val (p,_,f,nxt,_,pt) = me nxt p [] pt;

     (*Rewrite ("all_left", "PolyEq.all_left")*)

   val (p,_,f,nxt,_,pt) = me nxt p [] pt;

     (*Rewrite_Set_Inst (["(bdv, A)"], "make_ratpoly_in")*)

   val (p,_,f,nxt,_,pt) = me nxt p [] pt; 

     (*Rewrite_Set "polyeq_simplify"*)

   val (p,_,f,nxt,_,pt) = me nxt p [] pt; 

     (*Subproblem("Isac",["degree_1","polynomial","univariate","equation"])*)

   val (p,_,f,nxt,_,pt) = me nxt p [] pt;

   val (p,_,f,nxt,_,pt) = me nxt p [] pt;

   val (p,_,f,nxt,_,pt) = me nxt p [] pt;

   val (p,_,f,nxt,_,pt) = me nxt p [] pt;

   val (p,_,f,nxt,_,pt) = me nxt p [] pt;

   val (p,_,f,nxt,_,pt) = me nxt p [] pt;

   val (p,_,f,nxt,_,pt) = me nxt p [] pt;

   val (p,_,f,nxt,_,pt) = me nxt p [] pt;

   val (p,_,f,nxt,_,pt) = me nxt p [] pt;

   val (p,_,f,nxt,_,pt) = me nxt p [] pt;

   val (p,_,f,nxt,_,pt) = me nxt p [] pt;

   val (p,_,f,nxt,_,pt) = me nxt p [] pt;

   val (p,_,f,nxt,_,pt) = me nxt p [] pt;

   val (p,_,f,nxt,_,pt) = me nxt p [] pt;

   val (p,_,f,nxt,_,pt) = me nxt p [] pt;

   val (p,_,f,nxt,_,pt) = me nxt p [] pt;

   val (p,_,f,nxt,_,pt) = me nxt p [] pt;

   val (p,_,f,nxt,_,pt) = me nxt p [] pt;

   val (p,_,f,nxt,_,pt) = me nxt p [] pt;

   val (p,_,f,nxt,_,pt) = me nxt p [] pt;

   val (p,_,f,nxt,_,pt) = me nxt p [] pt;

   val (p,_,f,nxt,_,pt) = me nxt p [] pt;

   val (p,_,f,nxt,_,pt) = me nxt p [] pt;

   val (p,_,f,nxt,_,pt) = me nxt p [] pt;

   val (p,_,f,nxt,_,pt) = me nxt p [] pt;

   val (p,_,f,nxt,_,pt) = me nxt p [] pt;

   val (p,_,f,nxt,_,pt) = me nxt p [] pt;

   val (p,_,f,nxt,_,pt) = me nxt p [] pt;

   val (p,_,f,nxt,_,pt) = me nxt p [] pt;

   val (p,_,f,nxt,_,pt) = me nxt p [] pt;

   val (p,_,f,nxt,_,pt) = me nxt p [] pt;

   val (p,_,f,nxt,_,pt) = me nxt p [] pt;

   val (p,_,f,nxt,_,pt) = me nxt p [] pt;

   val (p,_,f,nxt,_,pt) = me nxt p [] pt;

   val (p,_,f,nxt,_,pt) = me nxt p [] pt;

   val (p,_,f,nxt,_,pt) = me nxt p [] pt;

   val (p,_,f,nxt,_,pt) = me nxt p [] pt;

   val (p,_,f,nxt,_,pt) = me nxt p [] pt;

   val (p,_,f,nxt,_,pt) = me nxt p [] pt;

   val (p,_,f,nxt,_,pt) = me nxt p [] pt;

   val (p,_,f,nxt,_,pt) = me nxt p [] pt;

   val (p,_,f,nxt,_,pt) = me nxt p [] pt;

   val (p,_,f,nxt,_,pt) = me nxt p [] pt;

   val (p,_,f,nxt,_,pt) = me nxt p [] pt;

   val (p,_,f,nxt,_,pt) = me nxt p [] pt;

   val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*([11, 4, 5], Res) Check_Postcond*)

   val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*([11, 4], Res) Check_Postcond*)

   val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*([11], Res) Take*)

   val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*([12], Frm) Substitute*)

   val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*([12], Res) Rewrite*)

   val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*([13], Res) Take*)

   val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*([14], Frm) Empty_Tac*)

 *}

 ML {*

   val (p,_,f,nxt,_,pt) = me nxt p [] pt;

 *}

 ML {*

   val (p,_,f,nxt,_,pt) = me nxt p [] pt;

 *}

 ML {*

   val (p,_,f,nxt,_,pt) = me nxt p [] pt;

 *}

 ML {*

   val (p,_,f,nxt,_,pt) = me nxt p [] pt;

 *}

 ML {*

   val (p,_,f,nxt,_,pt) = me nxt p [] pt;

 *}

 ML {*

   val (p,_,f,nxt,_,pt) = me nxt p [] pt;

 *}

 ML {*

 trace_script := true;

 *}

 ML {*

 val (p,_,f,nxt,_,pt) = me nxt p [] pt;

 *}

 ML {*

 Chead.show_pt pt;

 *}

 ML {*

 *} 

 ML {*

 *} 

 ML {*

 *} 

 ML {*

 *} 

 ML {*

 *} 

 ML {*

 *} 

 text{*\noindent As a last step we check the tracing output of the last calc

       tree instruction and compare it with the pre-calculated result.*}

 section {* Improve and Transfer into Knowledge *}

 text {*

   We want to improve the very long program \ttfamily InverseZTransform

   \normalfont by modularisation: partial fraction decomposition shall

   become a sub-problem.

   We could transfer all knowledge in \ttfamily Build\_Inverse\_Z\_Transform.thy 

   \normalfont first to the \ttfamily Knowledge/Inverse\_Z\_Transform.thy 

   \normalfont and then modularise. In this case TODO problems?!?

   We chose another way and go bottom up: first we build the sub-problem in

   \ttfamily Partial\_Fractions.thy \normalfont with the term:

       $$\frac{3}{x\cdot(z - \frac{1}{4} + \frac{-1}{8}\cdot\frac{1}{z})}$$

   \noindent (how this still can be improved see \ttfamily Partial\_Fractions.thy\normalfont),

   and re-use all stuff prepared in \ttfamily Build\_Inverse\_Z\_Transform.thy:

   \normalfont The knowledge will be transferred to \ttfamily src/../Partial\_Fractions.thy 

   \normalfont and the respective tests to:

   \begin{center}\ttfamily test/../sartial\_fractions.sml\normalfont\end{center}

 *}

 subsection {* Transfer to Partial\_Fractions.thy *}

 text {*

   First we transfer both, knowledge and tests into:

   \begin{center}\ttfamily src/../Partial\_Fractions.thy\normalfont\end{center}

   in order to immediately have the test results.

   We copy \ttfamily factors\_from\_solution, drop\_questionmarks,\\

   ansatz\_2nd\_order \normalfont and rule-sets --- no problem.

   Also \ttfamily store\_pbt ..\\ "pbl\_simp\_rat\_partfrac"

   \normalfont is easy.

   But then we copy from:\\

   (1) \ttfamily Build\_Inverse\_Z\_Transform.thy store\_met\ldots "met\_SP\_Ztrans\_inv"

   \normalfont\\ to\\ 

   (2) \ttfamily Partial\_Fractions.thy store\_met\ldots "met\_SP\_Ztrans\_inv" 

   \normalfont\\ and cut out the respective part from the program. First we ensure that

   the string is correct. When we insert the string into (2)

   \ttfamily store\_met .. "met\_partial\_fraction" \normalfont --- and get an error.

 *}

 subsubsection {* 'Programming' in ISAC's TP-based Language *}

 text {* 

   At the present state writing programs in {\sisac} is particularly cumbersome.

   So we give hints how to cope with the many obstacles. Below we describe the

   steps we did in making (2) run.

   \begin{enumerate}

     \item We check if the \textbf{string} containing the program is correct.

     \item We check if the \textbf{types in the program} are correct.

       For this purpose we start start with the first and last lines

      \begin{verbatim}

      "PartFracScript (f_f::real) (v_v::real) =       " ^

      " (let X = Take f_f;                            " ^

      "      pbz = ((Substitute []) X)                " ^

      "  in pbz)"

      \end{verbatim}

        The last but one line helps not to bother with ';'.

      \item Then we add line by line. Already the first line causes the error. 

         So we investigate it by

       \begin{verbatim}

       val ctxt = Proof_Context.init_global @{theory "Inverse_Z_Transform"} ;

       val SOME t = 

         parseNEW ctxt "(num_orig::real) = 

                           get_numerator(rhs f_f)";

       \end{verbatim}

         and see a type clash: \ttfamily rhs \normalfont from (1) requires type 

         \ttfamily bool \normalfont while (2) wants to have \ttfamily (f\_f::real).

         \normalfont Of course, we don't need \ttfamily rhs \normalfont anymore.

       \item Type-checking can be very tedious. One might even inspect the

         parse-tree of the program with {\sisac}'s specific debug tools:

       \begin{verbatim}

       val {scr = Prog t,...} = 

         get_met ["simplification",

                  "of_rationals",

                  "to_partial_fraction"];

       atomty_thy @{theory "Inverse_Z_Transform"} t ;

       \end{verbatim}

       \item We check if the \textbf{semantics of the program} by stepwise evaluation

         of the program. Evaluation is done by the Lucas-Interpreter, which works

         using the knowledge in theory Isac; so we have to re-build Isac. And the

         test are performed simplest in a file which is loaded with Isac.

         See \ttfamily tests/../partial\_fractions.sml \normalfont.

   \end{enumerate}

 *}

 subsection {* Transfer to Inverse\_Z\_Transform.thy *}

 text {*

   It was not possible to complete this task, because we ran out of time.

 *}

 end