(* Title:  Build_Inverse_Z_Transform

   Author: Jan Rocnik

   (c) copyright due to license terms.

12345678901234567890123456789012345678901234567890123456789012345678901234567890

        10        20        30        40        50        60        70        80

*)

theory Build_Inverse_Z_Transform imports 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",num_str @{thm rule3}),

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

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

    ];

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

  val SOME (t', asm) = 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_ thy ro er true (num_str @{thm rule3}) t;

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

  (*- real *)

  term2str t;

  val SOME (t, asm2) = 

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

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

  (*- real *)

  term2str t;

  val SOME (t, asm3) = 

    rewrite_ thy ro er true (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 = ProofContext.init_global @{theory};

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

  val SOME fun1 = 

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

  val SOME fun1' = 

    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_ thy ro er true  @{thm ruleZY} fun1; term2str fun2;

  val SOME (fun2', asm1) = 

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

  val SOME (fun3,_) = 

    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_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.inverse_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.inverse_class.divide", _) $num 

                $denom)) thy = 

        SOME (mk_thmid thmid "" 

            (Print_Mode.setmp [] 

              (Syntax.string_of_term (thy2ctxt thy)) denom) "", 

	          Trueprop $ (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.inverse_class.divide", _) $num

                $denom )) thy = 

        SOME (mk_thmid thmid "" 

            (Print_Mode.setmp [] 

              (Syntax.string_of_term (thy2ctxt thy)) num) "", 

	          Trueprop $ (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 = 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 {*

  match_pbl fmz (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 = 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 {*

  match_pbl fmz (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]

   *)

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

                     (Print_Mode.setmp []

                       (Syntax.string_of_term (thy2ctxt 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.inverse_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 {*

  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(

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

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

      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 ["normalize","polynomial",

                       "univariate","equation"])*)

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

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

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

    (*Apply_Method["PolyEq","normalize_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 ["normalize","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.*}

ML {*

  store_pbt

   (prep_pbt thy "pbl_SP" [] e_pblID

   (["SignalProcessing"], [], e_rls, NONE, []));

  store_pbt

   (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}.*}

ML {*

  store_pbt

   (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"]]));

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

ML {*

  store_met

   (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, nrls = e_rls}, "empty_script"));

  store_met

   (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, 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.*}

ML {*

  store_met

   (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, 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.*}

ML {*

  store_met

   (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, 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.*}