text{* We stepwise build \texttt{Inverse\_Z\_Transform.thy} as an exercise.

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

   Because subsection "Stepwise Check the Program" requires 

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

   \texttt{Inverse\_Z\_Transform.thy} as a subtheory of Isac.thy, the setup has been changed 

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

   from "theory Inverse_Z_Transform imports Isac begin.." to the above.

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

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

   ATTENTION WITH NAMES OF IDENTIFIERS WHEN GOING INTO INTERNALS:

   \par \noindent

   \begin{center} 

   \textbf{ATTENTION WITH NAMES OF IDENTIFIERS WHEN GOING INTO INTERNALS}

   \end{center}

   (Thm.derivation_name @{thm rule1} = "Build_Inverse_Z_Transform.rule1") = true;

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

   but actually in us will be "Inverse_Z_Transform.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}*}

 subsection {*Notations and Terms*}

 section {*trials towards Z transform *}

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

 text{*===============================*}

 ML {*

 subsection {*terms*}

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

 ML {*

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

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

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

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

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

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

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

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

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

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

   term2str @{term "1 < || z || ==> 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 {*

 ML {*

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

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

   @{term "\<alpha> "};

 @{term "\<alpha> "};

   @{term "\<delta> "};

 @{term "\<delta> "};

   @{term "\<phi> "};

 @{term "\<phi> "};

   @{term "\<rho> "};

 @{term "\<rho> "};

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

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

 *}

 *}

 subsection {*Rules*}

 subsection {*rules*}

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

 (*axiomatization "z / (z - 1) = -u [-n - 1]" Illegal variable name: "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 /"*)

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

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

 ML {*

 @{thm rule1};

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

 @{thm rule2};

       (See the machine output.)*}

 @{thm rule3};

 ML {*

 @{thm rule4};

   @{thm rule1};

 *}

   @{thm rule2};

   @{thm rule3};

 subsection {*apply rules*}

   @{thm rule4};

 ML {*

 *}

 val inverse_Z = append_rls "inverse_Z" e_rls

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

 subsection {*Apply Rules*}

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

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

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

   ];

 ML {*

   val inverse_Z = append_rls "inverse_Z" e_rls

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

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

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

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

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

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

 *}

     ];

 ML {*

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

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

 *}

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

 ML {*

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

 val SOME (t, asm1) = rewrite_ thy ro er true (num_str @{thm rule3}) t;

   (*

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

    * Attention rule1 is applied before the expression is 

 term2str t;*}

    * checked for rule4 which would be correct!!!

 ML {*

    *)

 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;

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

 *}

 ML {*

 ML {*

   val SOME (t, asm1) = 

 val SOME (t, asm3) = rewrite_ thy ro er true (num_str @{thm rule1}) t;

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

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

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

 term2str t;

   (*- real *)

 *}

   term2str t;

 ML {*

 terms2str (asm1 @ asm2 @ asm3);

   val SOME (t, asm2) = 

 *}

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

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

 section {*Prepare steps for CTP-based programming language*}

   (*- real *)

 text{*TODO insert Calculation (Referenz?!)

   term2str t;

 The goal... realized in sections below, in Sect.\ref{spec-meth} and Sect.\ref{prog-steps} 

   val SOME (t, asm3) = 

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

 the reader is advised to jump between the subsequent subsections and the respective steps in Sect.\ref{prog-steps} 

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

   (*- real *)

 *}

   term2str t;

 subsection {*prepare expression \label{prep-expr}*}

 *}

 ML {*

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

 val ctxt = ProofContext.init_global @{theory Isac};

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

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

 text{*

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

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

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

       possibilities of building the programm. 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 

 subsubsection {*multply with z*}

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

 ML {*

   val ctxt = ProofContext.init_global @{theory Isac};

   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 decomposion is only possible ig 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.*}

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

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

 val SOME (fun2, asm1) = rewrite_ thy ro er true  @{thm ruleZY} fun1; term2str fun2;

   val SOME (fun2, asm1) = 

 val SOME (fun2', asm1) = rewrite_ thy ro er true  @{thm ruleZY} fun1'; term2str fun2';

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

   val SOME (fun2', asm1) = 

 val SOME (fun3,_) = rewrite_set_ @{theory Isac} false norm_Rational fun2;

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

 term2str fun3; (*fails on x^^^(-1) TODO*)

 val SOME (fun3',_) = rewrite_set_ @{theory Isac} false norm_Rational fun2';

   val SOME (fun3,_) = 

 term2str fun3'; (*OK*)

     rewrite_set_ @{theory Isac} false norm_Rational fun2;

 *}

   term2str fun3;

   (*

 subsubsection {*get argument of X': z is the variable the equation is solved for*}

    * Fails on x^^^(-1)

 text{*grep... Atools.thy, Tools.thy contain general utilities: eval_argument_in, eval_rhs, eval_lhs,...

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

    *)

 grep -r "fun eva_" ... shows all functions witch can be used in a script.

   val SOME (fun3',_) = 

 lookup this files how to build and handle such functions.

     rewrite_set_ @{theory Isac} false norm_Rational fun2';

   term2str fun3';

 the next section shows how to introduce such a function.

   (*

 *}

    * OK - workaround!

    *)

 subsubsection {*Decompose given term into lhs = rhs*}

 *}

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

   val (_, denom) = HOLogic.dest_bin "Rings.inverse_class.divide" (type_of expr) expr;

   val (_, denom) = 

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

 text {*we have rhs in the Script language, but we need a function 

   which gets the denominator of a fraction*}

 text{*\noindent We have rhs 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*}

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

 text {*get denominator should become a constant for the isabelle parser: *}

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

        should become a constant for the isabelle parser:*}

 text {* With the above definition we run into problems with parsing the Script InverseZTransform:

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

   This leads to "ambiguous parse trees" and we avoid this by shifting the definition

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

   to Rational.thy and re-building Isac.

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

   ATTENTION: from now on Build_Inverse_Z_Transform mimics a build from scratch;

         to \ttfamily Rational.thy \normalfont and re-building Isac.

   it only works due to re-building Isac several times (indicated explicityl).

         \par \noindent ATTENTION: From now on \ttfamily 

 *}

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

         it only works due to re-building Isac several times (indicated 

 ML {*

         explicityl).

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

 *}

 ML {*

 (*

  *("get_denominator",

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

  *)

             (Print_Mode.setmp [] (Syntax.string_of_term (thy2ctxt thy)) denom) "", 

             (Print_Mode.setmp [] 

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

 subsubsection {*Stepwise check the program*}

 subsubsection {*Stepwise check the program\label{sec:stepcheck}*}