
neuper@42301: (* Title:  Build_Inverse_Z_Transform
neuper@42279:    Author: Jan Rocnik
neuper@42376:    (c) copyright due to license terms.
neuper@42279: *)
neuper@42279: 
wneuper@59465: theory Build_Inverse_Z_Transform imports Isac.Inverse_Z_Transform
neuper@42289:   
neuper@42289: begin
neuper@42279: 
wneuper@59472: text\<open>We stepwise build \ttfamily Inverse\_Z\_Transform.thy \normalfont as an 
jan@42381:   exercise. Because Subsection~\ref{sec:stepcheck} requires 
jan@42371:   \ttfamily Inverse\_Z\_Transform.thy \normalfont as a subtheory of \ttfamily 
jan@42368:   Isac.thy\normalfont, the setup has been changed from \ttfamily theory 
jan@42371:   Inverse\_Z\_Transform imports Isac \normalfont to the above one.
jan@42368:   \par \noindent
jan@42368:   \begin{center} 
jan@42381:   \textbf{Attention with the names of identifiers when going into internals!}
jan@42368:   \end{center}
jan@42368:   Here in this theory there are the internal names twice, for instance we have
jan@42368:   \ttfamily (Thm.derivation\_name @{thm rule1} = 
jan@42368:   "Build\_Inverse\_Z\_Transform.rule1") = true; \normalfont
jan@42368:   but actually in us will be \ttfamily Inverse\_Z\_Transform.rule1 \normalfont
wneuper@59472: \<close>
neuper@42279: 
wneuper@59472: section \<open>Trials towards the Z-Transform\label{sec:trials}\<close>
jan@42368: 
wneuper@59472: ML \<open>val thy = @{theory};\<close>
neuper@42279: 
wneuper@59472: subsection \<open>Notations and Terms\<close>
wneuper@59472: text\<open>\noindent Try which notations we are able to use.\<close>
wneuper@59472: ML \<open>
jan@42368:   @{term "1 < || z ||"};
jan@42368:   @{term "z / (z - 1)"};
jan@42368:   @{term "-u -n - 1"};
jan@42368:   @{term "-u [-n - 1]"}; (*[ ] denotes lists !!!*)
neuper@42389:   @{term "z /(z - 1) = -u [-n - 1]"};
jan@42368:   @{term "1 < || z || ==> z / (z - 1) = -u [-n - 1]"};
walther@59868:   UnparseC.term @{term "1 < || z || ==> z / (z - 1) = -u [-n - 1]"};
wneuper@59472: \<close>
wneuper@59472: text\<open>\noindent Try which symbols we are able to use and how we generate them.\<close>
wneuper@59472: ML \<open>
jan@42368:   (*alpha -->  "</alpha>" *)
jan@42368:   @{term "\<alpha> "};
jan@42368:   @{term "\<delta> "};
jan@42368:   @{term "\<phi> "};
jan@42368:   @{term "\<rho> "};
walther@59868:   UnparseC.term @{term "\<rho> "};
wneuper@59472: \<close>
neuper@42279: 
wneuper@59472: subsection \<open>Rules\<close>
jan@42368: (*axiomatization "z / (z - 1) = -u [-n - 1]"
jan@42368:   Illegal variable name: "z / (z - 1) = -u [-n - 1]" *)
jan@42368: (*definition     "z / (z - 1) = -u [-n - 1]"
jan@42368:   Bad head of lhs: existing constant "op /"*)
neuper@42279: axiomatization where 
neuper@42279:   rule1: "1 = \<delta>[n]" and
neuper@42279:   rule2: "|| z || > 1 ==> z / (z - 1) = u [n]" and
neuper@42279:   rule3: "|| z || < 1 ==> z / (z - 1) = -u [-n - 1]" and 
walther@60242:   rule4: "|| z || > || \<alpha> || ==> z / (z - \<alpha>) = \<alpha> \<up> n * u [n]" and
walther@60242:   rule5: "|| z || < || \<alpha> || ==> z / (z - \<alpha>) = -(\<alpha> \<up> n) * u [-n - 1]" and
walther@60242:   rule6: "|| z || > 1 ==> z/(z - 1) \<up> 2 = n * u [n]"
jan@42368: 
wneuper@59472: text\<open>\noindent Check the rules for their correct notation. 
wneuper@59472:       (See the machine output.)\<close>
wneuper@59472: ML \<open>
jan@42368:   @{thm rule1};
jan@42368:   @{thm rule2};
jan@42368:   @{thm rule3};
jan@42368:   @{thm rule4};
wneuper@59472: \<close>
neuper@42279: 
wneuper@59472: subsection \<open>Apply Rules\<close>
wneuper@59472: text\<open>\noindent We try to apply the rules to a given expression.\<close>
jan@42368: 
wneuper@59472: ML \<open>
walther@60278:   val inverse_Z = Rule_Set.append_rules "inverse_Z" Atools_erls
wenzelm@60297:     [ \<^rule_thm>\<open>rule3\<close>,
wenzelm@60297:       \<^rule_thm>\<open>rule4\<close>,
wenzelm@60297:       \<^rule_thm>\<open>rule1\<close>   
jan@42368:     ];
neuper@42279: 
walther@60278: \<close> ML \<open>
Walther@60565:   val t = TermC.parse_test @{context} "z / (z - 1) + z / (z - \<alpha>) + 1::real";
walther@60278: \<close> ML \<open>
wneuper@59395:   val SOME (t', asm) = Rewrite.rewrite_set_ thy true inverse_Z t;
walther@60336: (*rewrite__set_ called with 'Erls' for '|| z || < 1'*)
walther@60336: \<close> ML \<open>
walther@59868:   UnparseC.term t' = "z / (z - ?\<delta> [?n]) + z / (z - \<alpha>) + ?\<delta> [?n]";
jan@42368:   (*
jan@42368:    * Attention rule1 is applied before the expression is 
jan@42368:    * checked for rule4 which would be correct!!!
jan@42368:    *)
walther@60278: \<close> ML \<open>
wneuper@59472: \<close>
neuper@42279: 
wneuper@59472: ML \<open>val (thy, ro, er) = (@{theory}, tless_true, eval_rls);\<close>
wneuper@59472: ML \<open>
jan@42368:   val SOME (t, asm1) = 
walther@59871:     Rewrite.rewrite_ thy ro er true (ThmC.numerals_to_Free @{thm rule3}) t;
walther@59868:   UnparseC.term t = "- ?u [- ?n - 1] + z / (z - \<alpha>) + 1";
jan@42368:   (*- real *)
walther@59868:   UnparseC.term t;
jan@42296: 
jan@42368:   val SOME (t, asm2) = 
walther@59871:     Rewrite.rewrite_ thy ro er true (ThmC.numerals_to_Free @{thm rule4}) t;
walther@60242:   UnparseC.term t = "- ?u [- ?n - 1] + \<alpha> \<up> ?n * ?u [?n] + 1";
jan@42368:   (*- real *)
walther@59868:   UnparseC.term t;
jan@42296: 
jan@42368:   val SOME (t, asm3) = 
walther@59871:     Rewrite.rewrite_ thy ro er true (ThmC.numerals_to_Free @{thm rule1}) t;
walther@60242:   UnparseC.term t = "- ?u [- ?n - 1] + \<alpha> \<up> ?n * ?u [?n] + ?\<delta> [?n]";
jan@42368:   (*- real *)
walther@59868:   UnparseC.term t;
wneuper@59472: \<close>
walther@59868: ML \<open>UnparseC.terms (asm1 @ asm2 @ asm3);\<close>
jan@42296: 
wneuper@59472: section\<open>Prepare Steps for TP-based programming Language\label{sec:prepstep}\<close>
wneuper@59472: text\<open>
neuper@42376:       \par \noindent The following sections are challenging with the CTP-based 
neuper@42376:       possibilities of building the program. The goal is realized in 
jan@42368:       Section~\ref{spec-meth} and Section~\ref{prog-steps}.
jan@42368:       \par The reader is advised to jump between the subsequent subsections and 
jan@42368:       the respective steps in Section~\ref{prog-steps}. By comparing 
jan@42368:       Section~\ref{sec:calc:ztrans} the calculation can be comprehended step 
jan@42368:       by step.
wneuper@59472: \<close>
neuper@42279: 
wneuper@59472: subsection \<open>Prepare Expression\label{prep-expr}\<close>
wneuper@59472: text\<open>\noindent We try two different notations and check which of them 
wneuper@59472:        Isabelle can handle best.\<close>
wneuper@59472: ML \<open>
neuper@48761:   val ctxt = Proof_Context.init_global @{theory};
wneuper@59582: (*val ctxt = ContextC.declare_constraints' [@{term "z::real"}] ctxt;*)
jan@42368: 
jan@42368:   val SOME fun1 = 
walther@60242:     TermC.parseNEW ctxt "X z = 3 / (z - 1/4 + -1/8 * z \<up> -1)"; UnparseC.term fun1;
jan@42368:   val SOME fun1' = 
walther@59868:     TermC.parseNEW ctxt "X z = 3 / (z - 1/4 + -1/8 * (1/z))"; UnparseC.term fun1';
wneuper@59472: \<close>
jan@42368: 
wneuper@59472: subsubsection \<open>Prepare Numerator and Denominator\<close>
wneuper@59472: text\<open>\noindent The partial fraction decomposition is only possible if we
jan@42368:        get the bound variable out of the numerator. Therefor we divide
jan@42368:        the expression by $z$. Follow up the Calculation at 
wneuper@59472:        Section~\ref{sec:calc:ztrans} line number 02.\<close>
jan@42368: 
neuper@42279: axiomatization where
neuper@42279:   ruleZY: "(X z = a / b) = (X' z = a / (z * b))"
neuper@42279: 
wneuper@59472: ML \<open>
neuper@42384:   val (thy, ro, er) = (@{theory}, tless_true, eval_rls);
jan@42368:   val SOME (fun2, asm1) = 
walther@59868:     Rewrite.rewrite_ thy ro er true  @{thm ruleZY} fun1; UnparseC.term fun2;
jan@42368:   val SOME (fun2', asm1) = 
walther@59868:     Rewrite.rewrite_ thy ro er true  @{thm ruleZY} fun1'; UnparseC.term fun2';
neuper@42279: 
jan@42368:   val SOME (fun3,_) = 
wneuper@59395:     Rewrite.rewrite_set_ @{theory} false norm_Rational fun2;
walther@59868:   UnparseC.term fun3;
jan@42368:   (*
walther@60242:    * Fails on x \<up> (-1)
jan@42368:    * We solve this problem by using 1/x as a workaround.
jan@42368:    *)
jan@42368:   val SOME (fun3',_) = 
wneuper@59395:     Rewrite.rewrite_set_ @{theory} false norm_Rational fun2';
walther@59868:   UnparseC.term fun3';
jan@42368:   (*
jan@42368:    * OK - workaround!
jan@42368:    *)
wneuper@59472: \<close>
neuper@42279: 
wneuper@59472: subsubsection \<open>Get the Argument of the Expression X'\<close>
wneuper@59472: text\<open>\noindent We use \texttt{grep} for finding possibilities how we can
walther@59603:        extract the bound variable in the expression. \ttfamily Prog_Expr.thy, 
jan@42368:        Tools.thy \normalfont contain general utilities: \ttfamily 
jan@42368:        eval\_argument\_in, eval\_rhs, eval\_lhs,\ldots \normalfont
jan@42368:        \ttfamily grep -r "fun eva\_" * \normalfont shows all functions 
jan@42371:        witch can be used in a script. Lookup this files how to build 
jan@42368:        and handle such functions.
jan@42368:        \par The next section shows how to introduce such a function.
wneuper@59472: \<close>
jan@42298: 
wneuper@59472: subsubsection\<open>Decompose the Given Term Into lhs and rhs\<close>
wneuper@59472: ML \<open>
walther@59868:   val (_, expr) = HOLogic.dest_eq fun3'; UnparseC.term expr;
jan@42368:   val (_, denom) = 
wenzelm@60309:     HOLogic.dest_bin \<^const_name>\<open>divide\<close> (type_of expr) expr;
walther@60242:   UnparseC.term denom = "-1 + -2 * z + 8 * z \<up> 2";
wneuper@59472: \<close>
jan@42298: 
wneuper@59472: text\<open>\noindent We have rhs\footnote{Note: lhs means \em Left Hand Side
jan@42370:       \normalfont and rhs means \em Right Hand Side \normalfont and indicates
wneuper@59585:       the left or the right part of an equation.} in the Program language, but
wneuper@59472:       we need a function which gets the denominator of a fraction.\<close>
jan@42298: 
wneuper@59472: subsubsection\<open>Get the Denominator and Numerator out of a Fraction\<close>
wneuper@59472: text\<open>\noindent The self written functions in e.g. \texttt{get\_denominator}
wneuper@59472:        should become a constant for the Isabelle parser:\<close>
jan@42298: 
jan@42298: consts
jan@42345:   get_denominator :: "real => real"
jan@42344:   get_numerator :: "real => real"
jan@42298: 
wneuper@59472: text \<open>\noindent With the above definition we run into problems when we parse
wneuper@59585:         the Program \texttt{InverseZTransform}. This leads to \em ambiguous
jan@42368:         parse trees. \normalfont We avoid this by moving the definition
jan@42369:         to \ttfamily Rational.thy \normalfont and re-building {\sisac}.
jan@42368:         \par \noindent ATTENTION: From now on \ttfamily 
jan@42368:         Build\_Inverse\_Z\_Transform \normalfont mimics a build from scratch;
jan@42369:         it only works due to re-building {\sisac} several times (indicated 
neuper@42376:         explicitly).
wneuper@59472: \<close>
jan@42300: 
wneuper@59472: ML \<open>
jan@42368: (*
jan@42368:  *("get_denominator",
jan@42368:  *  ("Rational.get_denominator", eval_get_denominator ""))
jan@42368:  *)
jan@42298: fun eval_get_denominator (thmid:string) _ 
walther@60336: 		      (t as Const (\<^const_name>\<open>get_denominator\<close>, _) $
wenzelm@60309:               (Const (\<^const_name>\<open>divide\<close>, _) $num 
jan@42369:                 $denom)) thy = 
walther@59870:         SOME (TermC.mk_thmid thmid (UnparseC.term_in_thy thy denom) "", 
wneuper@59395: 	        HOLogic.Trueprop $ (TermC.mk_equality (t, denom)))
jan@42300:   | eval_get_denominator _ _ _ _ = NONE; 
wneuper@59472: \<close>
wneuper@59472: text \<open>\noindent For the tests of \ttfamily eval\_get\_denominator \normalfont
wneuper@59472:         see \ttfamily test/Knowledge/rational.sml\normalfont\<close>
neuper@42289: 
wneuper@59472: text \<open>\noindent \ttfamily get\_numerator \normalfont should also become a
neuper@42376:         constant for the Isabelle parser, follow up the \texttt{const}
wneuper@59472:         declaration above.\<close>
jan@42337: 
wneuper@59472: ML \<open>
jan@42369: (*
jan@42369:  *("get_numerator",
jan@42369:  *  ("Rational.get_numerator", eval_get_numerator ""))
jan@42369:  *)
jan@42337: fun eval_get_numerator (thmid:string) _ 
walther@60336: 		      (t as Const (\<^const_name>\<open>Rational.get_numerator\<close>, _) $
wenzelm@60309:               (Const (\<^const_name>\<open>divide\<close>, _) $num
jan@42338:                 $denom )) thy = 
walther@59870:         SOME (TermC.mk_thmid thmid (UnparseC.term_in_thy thy num) "", 
wneuper@59395: 	        HOLogic.Trueprop $ (TermC.mk_equality (t, num)))
jan@42337:   | eval_get_numerator _ _ _ _ = NONE; 
wneuper@59472: \<close>
jan@42337: 
wneuper@59472: text \<open>\noindent We discovered several problems by implementing the 
jan@42369:        \ttfamily get\_numerator \normalfont function. Remember when 
jan@42369:        putting new functions to {\sisac}, put them in a thy file and rebuild 
wneuper@59472:        {\sisac}, also put them in the ruleset for the script!\<close>
jan@42369: 
wneuper@59472: subsection \<open>Solve Equation\label{sec:solveq}\<close>
wneuper@59472: text \<open>\noindent We have to find the zeros of the term, therefor we use our
jan@42369:        \ttfamily get\_denominator \normalfont function from the step before
neuper@42376:        and try to solve the second order equation. (Follow up the Calculation
jan@42369:        in Section~\ref{sec:calc:ztrans} Subproblem 2) Note: This type of
jan@42369:        equation is too general for the present program.
jan@42369:        \par We know that this equation can be categorized as \em univariate
jan@42369:        equation \normalfont and solved with the functions {\sisac} provides
jan@42369:        for this equation type. Later on {\sisac} should determine the type
wneuper@59472:        of the given equation self.\<close>
wneuper@59472: ML \<open>
walther@60242:   val denominator = TermC.parseNEW ctxt "z \<up> 2 - 1/4*z - 1/8 = 0";
walther@60242:   val fmz = ["equality (z \<up> 2 - 1/4*z - 1/8 = (0::real))",
jan@42369:              "solveFor z",
jan@42369:              "solutions L"];
walther@59997:   val (dI',pI',mI') =("Isac_Knowledge", ["univariate", "equation"], ["no_met"]);
wneuper@59472: \<close>
wneuper@59472: text \<open>\noindent Check if the given equation matches the specification of this
wneuper@59472:         equation type.\<close>
wneuper@59472: ML \<open>
walther@59997:   M_Match.match_pbl fmz (Problem.from_store ["univariate", "equation"]);
wneuper@59472: \<close>
jan@42345: 
wneuper@59472: text\<open>\noindent We switch up to the {\sisac} Context and try to solve the 
wneuper@59472:        equation with a more specific type definition.\<close>
neuper@42279: 
wneuper@59472: ML \<open>
wneuper@59592:   Context.theory_name thy = "Isac_Knowledge";
walther@60242:   val denominator = TermC.parseNEW ctxt "-1 + -2 * z + 8 * z \<up> 2 = 0";
jan@42369:   val fmz =                                             (*specification*)
walther@60242:     ["equality (-1 + -2 * z + 8 * z \<up> 2 = (0::real))",(*equality*)
jan@42369:      "solveFor z",                                      (*bound variable*)
jan@42369:      "solutions L"];                                    (*identifier for
jan@42369:                                                           solution*)
jan@42369:   val (dI',pI',mI') =
wneuper@59592:     ("Isac_Knowledge", 
walther@59997:       ["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
jan@42369:       ["no_met"]);
wneuper@59472: \<close>
neuper@42279: 
wneuper@59472: text \<open>\noindent Check if the (other) given equation matches the 
wneuper@59472:         specification of this equation type.\<close>
jan@42369:         
wneuper@59472: ML \<open>
walther@59984:   M_Match.match_pbl fmz (Problem.from_store
walther@59997:     ["abcFormula", "degree_2", "polynomial", "univariate", "equation"]);
wneuper@59472: \<close>
neuper@42279: 
wneuper@59472: text \<open>\noindent We stepwise solve the equation. This is done by the
wneuper@59472:         use of a so called calc tree seen downwards.\<close>
jan@42369: 
wneuper@59472: ML \<open>
Walther@60571:   val (p,_,f,nxt,_,pt) = Test_Code.init_calc @{context} [(fmz, (dI',pI',mI'))];
jan@42369:   val (p,_,f,nxt,_,pt) = me nxt p [] pt;
jan@42369:   val (p,_,f,nxt,_,pt) = me nxt p [] pt;
jan@42369:   val (p,_,f,nxt,_,pt) = me nxt p [] pt;
jan@42369:   val (p,_,f,nxt,_,pt) = me nxt p [] pt;
jan@42369:   val (p,_,f,nxt,_,pt) = me nxt p [] pt;
jan@42369:   val (p,_,f,nxt,_,pt) = me nxt p [] pt;
jan@42369:   val (p,_,f,nxt,_,pt) = me nxt p [] pt;
jan@42369:   val (p,_,f,nxt,_,pt) = me nxt p [] pt;
jan@42369:   val (p,_,f,nxt,_,pt) = me nxt p [] pt;
jan@42369:   val (p,_,f,nxt,_,pt) = me nxt p [] pt;
jan@42369:   val (p,_,f,nxt,_,pt) = me nxt p [] pt;         
jan@42369:   val (p,_,f,nxt,_,pt) = me nxt p [] pt;
jan@42369:   (*
jan@42369:    * nxt =..,Check_elementwise "Assumptions") 
jan@42369:    *)
jan@42369:   val (p,_,f,nxt,_,pt) = me nxt p [] pt;         
jan@42369:   val (p,_,f,nxt,_,pt) = me nxt p [] pt; f2str f;
jan@42369:   (*
jan@42369:    * [z = 1 / 2, z = -1 / 4]
jan@42369:    *)
walther@59983:   Test_Tool.show_pt pt; 
jan@42369:   val SOME f = parseNEW ctxt "[z=1/2, z=-1/4]";
wneuper@59472: \<close>
neuper@42279: 
wneuper@59472: subsection \<open>Partial Fraction Decomposition\label{sec:pbz}\<close>
wneuper@59472: text\<open>\noindent We go on with the decomposition of our expression. Follow up the
jan@42369:        Calculation in Section~\ref{sec:calc:ztrans} Step~3 and later on
wneuper@59472:        Subproblem~1.\<close>
wneuper@59472: subsubsection \<open>Solutions of the Equation\<close>
wneuper@59472: text\<open>\noindent We get the solutions of the before solved equation in a list.\<close>
jan@42369: 
wneuper@59472: ML \<open>
jan@42369:   val SOME solutions = parseNEW ctxt "[z=1/2, z=-1/4]";
walther@59868:   UnparseC.term solutions;
Walther@60650:   TermC.atom_trace_detail @{context} solutions;
wneuper@59472: \<close>
jan@42369: 
wneuper@59472: subsubsection \<open>Get Solutions out of a List\<close>
wneuper@59472: text \<open>\noindent In {\sisac}'s TP-based programming language: 
jan@42381: \begin{verbatim}
jan@42381:   let $ $ s_1 = NTH 1 $ solutions; $ s_2 = NTH 2... $
jan@42381: \end{verbatim}
jan@42381:        can be useful.
wneuper@59472: \<close>
jan@42369: 
wneuper@59472: ML \<open>
wenzelm@60309:   val Const (\<^const_name>\<open>Cons\<close>, _) $ s_1 $ (Const (\<^const_name>\<open>Cons\<close>, _)
wenzelm@60309:         $ s_2 $ Const (\<^const_name>\<open>Nil\<close>, _)) = solutions;
walther@59868:   UnparseC.term s_1;
walther@59868:   UnparseC.term s_2;
wneuper@59472: \<close>
jan@42369: 
wneuper@59472: text\<open>\noindent The ansatz for the \em Partial Fraction Decomposition \normalfont
jan@42369:       requires to get the denominators of the partial fractions out of the 
jan@42369:       Solutions as:
jan@42369:       \begin{itemize}
jan@42381:         \item $Denominator_{1}=z-Zeropoint_{1}$
jan@42381:         \item $Denominator_{2}=z-Zeropoint_{2}$
jan@42381:         \item \ldots
jan@42381:       \end{itemize}
wneuper@59472: \<close>
jan@42369:       
wneuper@59472: ML \<open>
jan@42369:   val xx = HOLogic.dest_eq s_1;
wenzelm@60309:   val s_1' = HOLogic.mk_binop \<^const_name>\<open>minus\<close> xx;
jan@42369:   val xx = HOLogic.dest_eq s_2;
wenzelm@60309:   val s_2' = HOLogic.mk_binop \<^const_name>\<open>minus\<close> xx;
walther@59868:   UnparseC.term s_1';
walther@59868:   UnparseC.term s_2';
wneuper@59472: \<close>
jan@42369: 
wneuper@59472: text \<open>\noindent For the programming language a function collecting all the 
wneuper@59472:         above manipulations is helpful.\<close>
jan@42369: 
wneuper@59472: ML \<open>
jan@42369:   fun fac_from_sol s =
jan@42369:     let val (lhs, rhs) = HOLogic.dest_eq s
wenzelm@60309:     in HOLogic.mk_binop \<^const_name>\<open>minus\<close> (lhs, rhs) end;
wneuper@59472: \<close>
jan@42369: 
wneuper@59472: ML \<open>
jan@42369:   fun mk_prod prod [] =
walther@59861:         if prod = TermC.empty
jan@42369:         then error "mk_prod called with []" 
jan@42369:         else prod
jan@42369:     | mk_prod prod (t :: []) =
walther@59861:         if prod = TermC.empty
jan@42369:         then t
wenzelm@60309:         else HOLogic.mk_binop \<^const_name>\<open>times\<close> (prod, t)
jan@42369:     | mk_prod prod (t1 :: t2 :: ts) =
walther@59861:           if prod = TermC.empty 
jan@42369:           then 
jan@42369:              let val p = 
wenzelm@60309:                HOLogic.mk_binop \<^const_name>\<open>times\<close> (t1, t2)
jan@42369:              in mk_prod p ts end 
jan@42369:           else 
jan@42369:              let val p =
wenzelm@60309:                HOLogic.mk_binop \<^const_name>\<open>times\<close> (prod, t1)
jan@42369:              in mk_prod p (t2 :: ts) end 
wneuper@59472: \<close>
jan@42369: (* ML {* 
neuper@42376: probably keep these test in test/Tools/isac/...
walther@59861: (*mk_prod TermC.empty [];*)
neuper@42335: 
Walther@60565: val prod = mk_prod TermC.empty [parse_test @{context} "x + 123"]; 
walther@59868: UnparseC.term prod = "x + 123";
neuper@42335: 
Walther@60565: val sol = parse_test @{context} "[z = 1 / 2, z = -1 / 4]";
neuper@42335: val sols = HOLogic.dest_list sol;
neuper@42335: val facs = map fac_from_sol sols;
walther@59861: val prod = mk_prod TermC.empty facs; 
walther@59868: UnparseC.term prod = "(z + -1 * (1 / 2)) * (z + -1 * (-1 / 4))";
neuper@42335: 
jan@42369: val prod = 
Walther@60565:   mk_prod TermC.empty [parse_test @{context} "x + 1", parse_test @{context} "x + 2", parse_test @{context} "x + 3"]; 
walther@59868: UnparseC.term prod = "(x + 1) * (x + 2) * (x + 3)";
jan@42369: *} *)
wneuper@59472: ML \<open>
jan@42369:   fun factors_from_solution sol = 
jan@42369:     let val ts = HOLogic.dest_list sol
walther@59861:     in mk_prod TermC.empty (map fac_from_sol ts) end;
wneuper@59472: \<close>
jan@42369: (* ML {*
Walther@60565: val sol = parse_test @{context} "[z = 1 / 2, z = -1 / 4]";
neuper@42335: val fs = factors_from_solution sol;
walther@59868: UnparseC.term fs = "(z + -1 * (1 / 2)) * (z + -1 * (-1 / 4))"
jan@42369: *} *)
wneuper@59472: text \<open>\noindent This function needs to be packed such that it can be evaluated
jan@42369:         by the Lucas-Interpreter. Therefor we moved the function to the
jan@42369:         corresponding \ttfamily Equation.thy \normalfont in our case
neuper@42376:         \ttfamily PartialFractions.thy \normalfont. The necessary steps
jan@42381:         are quit the same as we have done with \ttfamily get\_denominator 
wneuper@59472:         \normalfont before.\<close>
wneuper@59472: ML \<open>
jan@42369:   (*("factors_from_solution",
jan@42369:     ("Partial_Fractions.factors_from_solution",
jan@42369:       eval_factors_from_solution ""))*)
jan@42369:       
jan@42369:   fun eval_factors_from_solution (thmid:string) _
walther@60270:       (t as Const ("Partial_Fractions.factors_from_solution", _) $ sol) thy =
walther@60270:         let val prod = factors_from_solution sol
walther@60270:         in SOME (TermC.mk_thmid thmid (UnparseC.term_in_thy thy prod) "",
walther@60270:              HOLogic.Trueprop $ (TermC.mk_equality (t, prod)))
walther@60270:         end
walther@60270:     | eval_factors_from_solution _ _ _ _ = NONE;
wneuper@59472: \<close>
jan@42352: 
wneuper@59472: text \<open>\noindent The tracing output of the calc tree after applying this
jan@42381:        function was:
jan@42381: \begin{verbatim}
jan@42381:   24 / factors_from_solution [z = 1/ 2, z = -1 / 4])]
jan@42381: \end{verbatim}
jan@42381:        and the next step:
jan@42381: \begin{verbatim}
jan@42381:   val nxt = ("Empty_Tac", ...): tac'_)
jan@42381: \end{verbatim}
jan@42381:        These observations indicate, that the Lucas-Interpreter (LIP) 
jan@42381:        does not know how to evaluate \ttfamily factors\_from\_solution
jan@42381:        \normalfont, so we knew that there is something wrong or missing.
wneuper@59472: \<close>
jan@42369:        
wneuper@59472: text\<open>\noindent First we isolate the difficulty in the program as follows:
jan@42381: \begin{verbatim}      
wneuper@59476:   " (L_L::bool list) = (SubProblem (PolyEqX,      " ^
jan@42381:   "   [abcFormula, degree_2, polynomial,          " ^
jan@42381:   "    univariate,equation],                      " ^
jan@42381:   "   [no_met])                                   " ^
jan@42381:   "   [BOOL equ, REAL zzz]);                      " ^
jan@42381:   " (facs::real) = factors_from_solution L_L;     " ^
jan@42381:   " (foo::real) = Take facs                       " ^
jan@42381: \end{verbatim}
jan@42381: 
jan@42381:       \par \noindent And see the tracing output:
jan@42381:       
jan@42381: \begin{verbatim}
jan@42381:   [(([], Frm), Problem (Isac, [inverse, 
jan@42381:                                Z_Transform,
jan@42381:                                 SignalProcessing])),
jan@42381:    (([1], Frm), X z = 3 / (z - 1 / 4 + -1 / 8 * (1 / z))),
jan@42381:    (([1], Res), ?X' z = 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))),
walther@60242:    (([2], Res), ?X' z = 24 / (-1 + -2 * z + 8 * z \<up> 2)),
walther@60242:    (([3], Pbl), solve (-1 + -2 * z + 8 * z \<up> 2 = 0, z)),
walther@60242:    (([3,1], Frm), -1 + -2 * z + 8 * z \<up> 2 = 0),
walther@60242:    (([3,1], Res), z = (- -2 + sqrt (-2 \<up> 2 - 4 * 8 * -1)) / (2 * 8)|
walther@60242:                   z = (- -2 - sqrt (-2 \<up> 2 - 4 * 8 * -1)) / (2 * 8)),
jan@42381:    (([3,2], Res), z = 1 / 2 | z = -1 / 4),
jan@42381:    (([3,3], Res), [ z = 1 / 2, z = -1 / 4]),
jan@42381:    (([3,4], Res), [ z = 1 / 2, z = -1 / 4]),
jan@42381:    (([3], Res), [ z = 1 / 2, z = -1 / 4]),
jan@42381:    (([4], Frm), factors_from_solution [z = 1 / 2, z = -1 / 4])]
jan@42381: \end{verbatim}      
jan@42381:       
jan@42381:       \par \noindent In particular that:
jan@42381:       
jan@42381: \begin{verbatim}
walther@60242:   (([3], Pbl), solve (-1 + -2 * z + 8 * z \<up> 2 = 0, z)),
jan@42381: \end{verbatim}
jan@42381:       \par \noindent Shows the equation which has been created in
jan@42381:       the program by: 
jan@42381: \begin{verbatim}
jan@42381:   "(denom::real) = get_denominator funterm;      " ^ 
jan@42381:     (* get_denominator *)
jan@42381:   "(equ::bool) = (denom = (0::real));            " ^
jan@42381: \end{verbatim}
jan@42369:         
jan@42381:       \noindent \ttfamily get\_denominator \normalfont has been evaluated successfully,
jan@42369:       but not\\ \ttfamily factors\_from\_solution.\normalfont
jan@42369:       So we stepwise compare with an analogous case, \ttfamily get\_denominator
jan@42369:       \normalfont successfully done above: We know that LIP evaluates
Walther@60586:       expressions in the program by use of the \emph{prog_rls}, so we try to get
Walther@60586:       the original \emph{prog_rls}.\\
jan@42352: 
jan@42381: \begin{verbatim}
Walther@60586:   val {prog_rls,...} = MethodC.from_store ctxt ["SignalProcessing",
jan@42381:                             "Z_Transform",
neuper@42405:                             "Inverse"];
jan@42381: \end{verbatim}
jan@42369:           
jan@42381:       \par \noindent Create 2 good example terms:
jan@42352: 
jan@42381: \begin{verbatim}
jan@42381: val SOME t1 =
jan@42381:   parseNEW ctxt "get_denominator ((111::real) / 222)";
jan@42381: val SOME t2 =
jan@42381:   parseNEW ctxt "factors_from_solution [(z::real)=1/2, z=-1/4]";
jan@42381: \end{verbatim}
jan@42381: 
Walther@60586:       \par \noindent Rewrite the terms using prog_rls:\\
Walther@60586:       \ttfamily \par \noindent rewrite\_set\_ thy true prog_rls t1;\\
Walther@60586:         rewrite\_set\_ thy true prog_rls t2;\\
jan@42369:       \par \noindent \normalfont Now we see a difference: \texttt{t1} gives
jan@42369:       \texttt{SOME} but \texttt{t2} gives \texttt{NONE}. We look at the 
Walther@60586:       \emph{prog_rls}:
jan@42381: \begin{verbatim}
Walther@60586:   val prog_rls = 
walther@59851:     Rule_Set.Repeat{id = "srls_InverseZTransform",
walther@59878:         rules = [Eval("Rational.get_numerator",
jan@42381:                    eval_get_numerator "Rational.get_numerator"),
walther@59878:                  Eval("Partial_Fractions.factors_from_solution",
jan@42381:                    eval_factors_from_solution 
jan@42381:                      "Partial_Fractions.factors_from_solution")]}
jan@42381: \end{verbatim}                
jan@42381:       \par \noindent Here everthing is perfect. So the error can
jan@42369:       only be in the SML code of \ttfamily eval\_factors\_from\_solution.
jan@42369:       \normalfont We try to check the code with an existing test; since the 
jan@42369:       \emph{code} is in 
jan@42369:       \begin{center}\ttfamily src/Tools/isac/Knowledge/Partial\_Fractions.thy
jan@42369:       \normalfont\end{center}
jan@42369:       the \emph{test} should be in
jan@42369:       \begin{center}\ttfamily test/Tools/isac/Knowledge/partial\_fractions.sml
jan@42369:       \normalfont\end{center}
jan@42369:       \par \noindent After updating the function \ttfamily
jan@42369:       factors\_from\_solution \normalfont to a new version and putting a
neuper@42376:       test-case to \ttfamily Partial\_Fractions.sml \normalfont we tried again
jan@42369:       to evaluate the term with the same result.
jan@42369:       \par We opened the test \ttfamily Test\_Isac.thy \normalfont and saw that
jan@42369:       everything is working fine. Also we checked that the test \ttfamily 
jan@42369:       partial\_fractions.sml \normalfont is used in \ttfamily Test\_Isac.thy 
jan@42369:       \normalfont
jan@42369:       \begin{center}use \ttfamily "Knowledge/partial\_fractions.sml"
jan@42369:       \normalfont \end{center}
jan@42369:       and \ttfamily Partial\_Fractions.thy \normalfont is part is part of
jan@42381:       {\sisac} by evaluating
jan@42352: 
jan@42381: \begin{verbatim}
neuper@42389:   val thy = @{theory "Inverse_Z_Transform"};
jan@42381: \end{verbatim}
jan@42352: 
jan@42381:       After rebuilding {\sisac} again it worked.
wneuper@59472: \<close>
neuper@42279: 
wneuper@59472: subsubsection \<open>Build Expression\<close>
wneuper@59472: text \<open>\noindent In {\sisac}'s TP-based programming language we can build
jan@42369:        expressions by:\\
wneuper@59472:        \ttfamily let s\_1 = Take numerator / (s\_1 * s\_2) \normalfont\<close>
jan@42369:        
wneuper@59472: ML \<open>
jan@42369:   (*
neuper@42376:    * The main denominator is the multiplication of the denominators of
jan@42369:    * all partial fractions.
jan@42369:    *)
jan@42369:    
jan@42369:   val denominator' = HOLogic.mk_binop 
wenzelm@60309:     \<^const_name>\<open>times\<close> (s_1', s_2') ;
jan@42369:   val SOME numerator = parseNEW ctxt "3::real";
neuper@42279: 
jan@42369:   val expr' = HOLogic.mk_binop
wenzelm@60309:     \<^const_name>\<open>divide\<close> (numerator, denominator');
walther@59868:   UnparseC.term expr';
wneuper@59472: \<close>
neuper@42279: 
wneuper@59472: subsubsection \<open>Apply the Partial Fraction Decomposion Ansatz\<close>
jan@42369: 
wneuper@59472: text\<open>\noindent We use the Ansatz of the Partial Fraction Decomposition for our
jan@42369:       expression 2nd order. Follow up the calculation in 
wneuper@59472:       Section~\ref{sec:calc:ztrans} Step~03.\<close>
jan@42369: 
wneuper@59592: ML \<open>Context.theory_name thy = "Isac_Knowledge"\<close>
neuper@42279: 
wneuper@59472: text\<open>\noindent We define two axiomatization, the first one is the main ansatz,
neuper@42376:       the next one is just an equivalent transformation of the resulting
jan@42369:       equation. Both axiomatizations were moved to \ttfamily
jan@42369:       Partial\_Fractions.thy \normalfont and got their own rulesets. In later
neuper@42376:       programs it is possible to use the rulesets and the machine will find
wneuper@59472:       the correct ansatz and equivalent transformation itself.\<close>
jan@42369: 
neuper@42279: axiomatization where
jan@42369:   ansatz_2nd_order: "n / (a*b) = A/a + B/b" and
jan@42369:   equival_trans_2nd_order: "(n/(a*b) = A/a + B/b) = (n = A*b + B*a)"
jan@42369: 
wneuper@59472: text\<open>\noindent We use our \ttfamily ansatz\_2nd\_order \normalfont to rewrite
neuper@42376:        our expression and get an equation with our expression on the left
wneuper@59472:        and the partial fractions of it on the right hand side.\<close>
jan@42369:   
wneuper@59472: ML \<open>
jan@42369:   val SOME (t1,_) = 
walther@59852:     rewrite_ @{theory} e_rew_ord Rule_Set.empty false 
jan@42369:              @{thm ansatz_2nd_order} expr';
Walther@60650:   UnparseC.term t1; TermC.atom_trace_detail @{context} t1;
jan@42369:   val eq1 = HOLogic.mk_eq (expr', t1);
walther@59868:   UnparseC.term eq1;
wneuper@59472: \<close>
jan@42369: 
wneuper@59472: text\<open>\noindent Eliminate the denominators by multiplying the left and the
jan@42369:       right hand side of the equation with the main denominator. This is an
jan@42369:       simple equivalent transformation. Later on we use an own ruleset
jan@42369:       defined in \ttfamily Partial\_Fractions.thy \normalfont for doing this.
wneuper@59472:       Follow up the calculation in Section~\ref{sec:calc:ztrans} Step~04.\<close>
neuper@42279: 
wneuper@59472: ML \<open>
jan@42369:   val SOME (eq2,_) = 
walther@59852:     rewrite_ @{theory} e_rew_ord Rule_Set.empty false 
jan@42369:              @{thm equival_trans_2nd_order} eq1;
walther@59868:   UnparseC.term eq2;
wneuper@59472: \<close>
neuper@42342: 
wneuper@59472: text\<open>\noindent We use the existing ruleset \ttfamily norm\_Rational \normalfont 
wneuper@59472:      for simplifications on expressions.\<close>
neuper@42279: 
wneuper@59472: ML \<open>
neuper@42384:   val SOME (eq3,_) = rewrite_set_ @{theory} false norm_Rational eq2;
walther@59868:   UnparseC.term eq3;
jan@42369:   (*
jan@42369:    * ?A ?B not simplified
jan@42369:    *)
wneuper@59472: \<close>
neuper@42279: 
wneuper@59472: text\<open>\noindent In Example~\ref{eg:gap} of my thesis I'm describing a problem about
jan@42369:       simplifications. The problem that we would like to have only a specific degree
wneuper@59472:       of simplification occurs right here, in the next step.\<close>
jan@42369: 
wneuper@59472: ML \<open>
walther@60330:   Rewrite.trace_on := false; (*true false*)
jan@42369:   val SOME fract1 =
jan@42369:     parseNEW ctxt "(z - 1/2)*(z - -1/4) * (A/(z - 1/2) + B/(z - -1/4))";
jan@42369:   (*
jan@42369:    * A B !
jan@42369:    *)
jan@42369:   val SOME (fract2,_) = 
neuper@42384:     rewrite_set_ @{theory} false norm_Rational fract1;
walther@59868:   UnparseC.term fract2 = "(A + -2 * B + 4 * A * z + 4 * B * z) / 4";
jan@42369:   (*
walther@59868:    * UnparseC.term fract2 = "A * (1 / 4 + z) + B * (-1 / 2 + z)" 
jan@42369:    * would be more traditional...
jan@42369:    *)
wneuper@59472: \<close>
jan@42369: 
wneuper@59472: text\<open>\noindent We walk around this problem by generating our new equation first.\<close>
jan@42369: 
wneuper@59472: ML \<open>
jan@42369:   val (numerator, denominator) = HOLogic.dest_eq eq3;
jan@42369:   val eq3' = HOLogic.mk_eq (numerator, fract1);
jan@42369:   (*
jan@42369:    * A B !
jan@42369:    *)
walther@59868:   UnparseC.term eq3';
jan@42369:   (*
jan@42369:    * MANDATORY: simplify (and remove denominator) otherwise 3 = 0
jan@42369:    *)
jan@42369:   val SOME (eq3'' ,_) = 
neuper@42384:     rewrite_set_ @{theory} false norm_Rational eq3';
walther@59868:   UnparseC.term eq3'';
wneuper@59472: \<close>
jan@42369: 
wneuper@59472: text\<open>\noindent Still working at {\sisac}\ldots\<close>
jan@42369: 
wneuper@59592: ML \<open>Context.theory_name thy = "Isac_Knowledge"\<close>
jan@42369: 
wneuper@59472: subsubsection \<open>Build a Rule-Set for the Ansatz\<close>
wneuper@59472: text \<open>\noindent The \emph{ansatz} rules violate the principle that each
jan@42369:        variable on the right-hand-side must also occur on the
jan@42369:        left-hand-side of the rule: A, B, etc. don't do that. Thus the
jan@42369:        rewriter marks these variables with question marks: ?A, ?B, etc.
jan@42369:        These question marks can be dropped by \ttfamily fun
wneuper@59472:        drop\_questionmarks\normalfont.\<close>
jan@42369:        
wneuper@59472: ML \<open>
s1210629013@55444:   val ansatz_rls = prep_rls @{theory} (
walther@59851:     Rule_Set.Repeat {id = "ansatz_rls", preconds = [], rew_ord = ("dummy_ord",dummy_ord),
Walther@60586:       asm_rls = Rule_Set.empty, prog_rls = Rule_Set.Empty, calc = [], errpatts = [],
jan@42369:       rules = [
walther@59871:         Thm ("ansatz_2nd_order",ThmC.numerals_to_Free @{thm ansatz_2nd_order}),
walther@59871:         Thm ("equival_trans_2nd_order",ThmC.numerals_to_Free @{thm equival_trans_2nd_order})
jan@42369:               ], 
Walther@60586:       program = Empty_Prog});
wneuper@59472: \<close>
jan@42369: 
wneuper@59472: text\<open>\noindent We apply the ruleset\ldots\<close>
jan@42369: 
wneuper@59472: ML \<open>
jan@42369:   val SOME (ttttt,_) = 
neuper@42384:     rewrite_set_ @{theory} false ansatz_rls expr';
wneuper@59472: \<close>
jan@42369: 
wneuper@59472: text\<open>\noindent And check the output\ldots\<close>
jan@42369: 
wneuper@59472: ML \<open>
walther@59868:   UnparseC.term expr' = "3 / ((z - 1 / 2) * (z - -1 / 4))";
walther@59868:   UnparseC.term ttttt = "?A / (z - 1 / 2) + ?B / (z - -1 / 4)";
wneuper@59472: \<close>
jan@42369: 
wneuper@59472: subsubsection \<open>Get the First Coefficient\<close>
jan@42369: 
wneuper@59472: text\<open>\noindent Now it's up to get the two coefficients A and B, which will be
neuper@42376:       the numerators of our partial fractions. Continue following up the 
wneuper@59472:       Calculation in Section~\ref{sec:calc:ztrans} Subproblem~1.\<close>
jan@42369:       
wneuper@59472: text\<open>\noindent To get the first coefficient we substitute $z$ with the first
wneuper@59472:       zero-point we determined in Section~\ref{sec:solveq}.\<close>
jan@42369: 
wneuper@59472: ML \<open>
jan@42369:   val SOME (eq4_1,_) =
walther@59852:     rewrite_terms_ @{theory} e_rew_ord Rule_Set.empty [s_1] eq3'';
walther@59868:   UnparseC.term eq4_1;
jan@42369:   val SOME (eq4_2,_) =
neuper@42384:     rewrite_set_ @{theory} false norm_Rational eq4_1;
walther@59868:   UnparseC.term eq4_2;
jan@42369: 
walther@59997:   val fmz = ["equality (3=3*A/(4::real))", "solveFor A", "solutions L"];
walther@59997:   val (dI',pI',mI') =("Isac_Knowledge", ["univariate", "equation"], ["no_met"]);
jan@42369:   (*
neuper@42377:    * Solve the simple linear equation for A:
jan@42369:    * Return eq, not list of eq's
jan@42369:    *)
Walther@60571:   val (p,_,fa,nxt,_,pt) = Test_Code.init_calc @{context} [(fmz, (dI',pI',mI'))];
jan@42369:   val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
jan@42369:     (*Add_Given "equality (3=3*A/4)"*)
jan@42369:   val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
jan@42369:     (*Add_Given "solveFor A"*)
jan@42369:   val (p,_,fa,nxt,_,pt) = me nxt p [] pt; 
jan@42369:     (*Add_Find "solutions L"*)
jan@42369:   val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
wneuper@59592:     (*Specify_Theory "Isac_Knowledge"*)
jan@42369:   val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
walther@59997:     (*Specify_Problem ["normalise", "polynomial",
walther@59997:                        "univariate", "equation"])*)
jan@42369:   val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
walther@59997:     (* Specify_Method["PolyEq", "normalise_poly"]*)
jan@42369:   val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
walther@59997:     (*Apply_Method["PolyEq", "normalise_poly"]*)
jan@42369:   val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
walther@59997:     (*Rewrite ("all_left", "PolyEq.all_left")*)
jan@42369:   val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
wneuper@59497:     (*Rewrite_Set_Inst(["(''bdv'',A)"],"make_ratpoly_in")*)
jan@42369:   val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
jan@42369:     (*Rewrite_Set "polyeq_simplify"*)
jan@42369:   val (p,_,fa,nxt,_,pt) = me nxt p [] pt; 
jan@42369:   val (p,_,fa,nxt,_,pt) = me nxt p [] pt; 
jan@42369:   val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
jan@42369:     (*Add_Given "equality (3 + -3 / 4 * A =0)"*)
jan@42369:   val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
jan@42369:     (*Add_Given "solveFor A"*)
jan@42369:   val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
jan@42369:     (*Add_Find "solutions A_i"*)
jan@42369:   val (p,_,fa,nxt,_,pt) = me nxt p [] pt; 
jan@42369:   val (p,_,fa,nxt,_,pt) = me nxt p [] pt; 
jan@42369:   val (p,_,fa,nxt,_,pt) = me nxt p [] pt; 
jan@42369:   val (p,_,fa,nxt,_,pt) = me nxt p [] pt; 
walther@59997:     (*Apply_Method ["PolyEq", "solve_d1_polyeq_equation"]*)
jan@42369:   val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
wneuper@59497:     (*Rewrite_Set_Inst(["(''bdv'',A)"],"d1_polyeq_simplify")*)
jan@42369:   val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
jan@42369:     (*Rewrite_Set "polyeq_simplify"*)
jan@42369:   val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
jan@42369:     (*Rewrite_Set "norm_Rational_parenthesized"*)
jan@42369:   val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
jan@42369:     (*Or_to_List*)
jan@42369:   val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
jan@42369:     (*Check_elementwise "Assumptions"*)
jan@42369:   val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
walther@59997:     (*Check_Postcond ["degree_1", "polynomial",
walther@59997:                       "univariate", "equation"]*)
jan@42369:   val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
walther@59997:     (*Check_Postcond ["normalise", "polynomial",
walther@59997:                       "univariate", "equation"]*)
jan@42369:   val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
jan@42369:     (*End_Proof'*)
jan@42369:   f2str fa;
wneuper@59472: \<close>
jan@42369: 
wneuper@59472: subsubsection \<open>Get Second Coefficient\<close>
jan@42369: 
wneuper@59472: text\<open>\noindent With the use of \texttt{thy} we check which theories the 
wneuper@59472:       interpreter knows.\<close>
jan@42369: 
wneuper@59472: ML \<open>thy\<close>
neuper@42279: 
wneuper@59472: text\<open>\noindent To get the second coefficient we substitute $z$ with the second
wneuper@59472:       zero-point we determined in Section~\ref{sec:solveq}.\<close>
jan@42369: 
wneuper@59472: ML \<open>
jan@42369:   val SOME (eq4b_1,_) =
walther@59852:     rewrite_terms_ @{theory} e_rew_ord Rule_Set.empty [s_2] eq3'';
walther@59868:   UnparseC.term eq4b_1;
jan@42369:   val SOME (eq4b_2,_) =
neuper@42384:     rewrite_set_ @{theory} false norm_Rational eq4b_1;
walther@59868:   UnparseC.term eq4b_2;
neuper@42279: 
walther@59997:   val fmz = ["equality (3= -3*B/(4::real))", "solveFor B", "solutions L"];
walther@59997:   val (dI',pI',mI') =("Isac_Knowledge", ["univariate", "equation"], ["no_met"]);
Walther@60571:   val (p,_,fb,nxt,_,pt) = Test_Code.init_calc @{context} [(fmz, (dI',pI',mI'))];
jan@42369:   val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
jan@42369:   val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
jan@42369:   val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
jan@42369:   val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
jan@42369:   val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
jan@42369:   val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
jan@42369:   val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
jan@42369:   val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
jan@42369:   val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
jan@42369:   val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
jan@42369:   val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
jan@42369:   val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
jan@42369:   val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
jan@42369:   val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
jan@42369:   val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
jan@42369:   val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
jan@42369:   val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
jan@42369:   val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
jan@42369:   val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
jan@42369:   val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
jan@42369:   val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
jan@42369:   val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
jan@42369:   val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
jan@42369:   val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
jan@42369:   val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
jan@42369:   val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
jan@42369:   val (p,_,fb,nxt,_,pt) = me nxt p [] pt; 
jan@42369:   f2str fb;
wneuper@59472: \<close>
neuper@42279: 
Walther@60586: text\<open>\noindent We compare our results with the where_ calculated upshot.\<close>
jan@42369: 
wneuper@59472: ML \<open>
jan@42369:   if f2str fa = "[A = 4]" then () else error "part.fract. eq4_1";
jan@42369:   if f2str fb = "[B = -4]" then () else error "part.fract. eq4_1";
wneuper@59472: \<close>
neuper@42279: 
walther@60154: section \<open>Implement the Specification and the MethodC \label{spec-meth}\<close>
neuper@42279: 
wneuper@59472: text\<open>\noindent Now everything we need for solving the problem has been
jan@42369:       tested out. We now start by creating new nodes for our methods and
wneuper@59472:       further on our new program in the interpreter.\<close>
jan@42369: 
wneuper@59472: subsection\<open>Define the Field Descriptions for the 
wneuper@59472:             Specification\label{sec:deffdes}\<close>
jan@42369: 
wneuper@59472: text\<open>\noindent We define the fields \em filterExpression \normalfont and
neuper@42376:       \em stepResponse \normalfont both as equations, they represent the in- and
wneuper@59472:       output of the program.\<close>
jan@42369: 
neuper@42279: consts
neuper@42279:   filterExpression  :: "bool => una"
neuper@42279:   stepResponse      :: "bool => una"
neuper@42279: 
wneuper@59472: subsection\<open>Define the Specification\<close>
jan@42369: 
wneuper@59472: text\<open>\noindent The next step is defining the specifications as nodes in the
neuper@42376:       designated part. We have to create the hierarchy node by node and start
jan@42369:       with \em SignalProcessing \normalfont and go on by creating the node
wneuper@59472:       \em Z\_Transform\normalfont.\<close>
jan@42369: 
Walther@60588: setup \<open>Know_Store.add_pbls
wenzelm@60290:   [Problem.prep_input @{theory} "pbl_SP" [] Problem.id_empty (["SignalProcessing"], [], Rule_Set.empty, NONE, []),
wenzelm@60290:     Problem.prep_input @{theory} "pbl_SP_Ztrans" [] Problem.id_empty
walther@59997:       (["Z_Transform", "SignalProcessing"], [], Rule_Set.empty, NONE, [])]\<close>
jan@42369: 
wneuper@59472: text\<open>\noindent For the suddenly created node we have to define the input
neuper@42376:        and output parameters. We already prepared their definition in
wneuper@59472:        Section~\ref{sec:deffdes}.\<close>
jan@42369: 
Walther@60588: setup \<open>Know_Store.add_pbls
wenzelm@60290:   [Problem.prep_input @{theory} "pbl_SP_Ztrans_inv" [] Problem.id_empty
s1210629013@55355:       (["Inverse", "Z_Transform", "SignalProcessing"],
wneuper@59550:         [("#Given" ,["filterExpression X_eq"]),
s1210629013@55355:           ("#Find", ["stepResponse n_eq"])],
walther@59852:         Rule_Set.append_rules "empty" Rule_Set.empty [(*for preds in where_*)],
s1210629013@55355:         NONE,
walther@59997:         [["SignalProcessing", "Z_Transform", "Inverse"]])]\<close>
wneuper@59472: ML \<open>
walther@59971:   Test_Tool.show_ptyps() ();
walther@59997:   Problem.from_store ["Inverse", "Z_Transform", "SignalProcessing"];
wneuper@59472: \<close>
neuper@42279: 
walther@60154: subsection \<open>Define Name and Signature for the MethodC\<close>
jan@42369: 
wneuper@59472: text\<open>\noindent As a next step we store the definition of our new method as a
wneuper@59472:       constant for the interpreter.\<close>
jan@42369: 
neuper@42279: consts
neuper@42279:   InverseZTransform :: "[bool, bool] => bool"
wneuper@59585:     ("((Program InverseZTransform (_ =))// (_))" 9)
neuper@42279: 
walther@60154: subsection \<open>Setup Parent Nodes in Hierarchy of MethodC\label{sec:cparentnode}\<close>
jan@42369: 
wneuper@59472: text\<open>\noindent Again we have to generate the nodes step by step, first the
jan@42369:       parent node and then the originally \em Z\_Transformation 
jan@42369:       \normalfont node. We have to define both nodes first with an empty script
wneuper@59472:       as content.\<close>
jan@42369: 
Walther@60588: setup \<open>Know_Store.add_mets
wenzelm@60290:   [MethodC.prep_input @{theory} "met_SP" [] e_metID
s1210629013@55377:       (["SignalProcessing"], [],
Walther@60586:         {rew_ord="tless_true", rls'= Rule_Set.empty, calc = [], prog_rls = Rule_Set.empty, where_rls = Rule_Set.empty, crls = Rule_Set.empty,
Walther@60586:           errpats = [], rew_rls = Rule_Set.empty},
s1210629013@55377:         "empty_script"),
wenzelm@60290:     MethodC.prep_input @{theory} "met_SP_Ztrans" [] e_metID
s1210629013@55377:       (["SignalProcessing", "Z_Transform"], [],
Walther@60586:         {rew_ord="tless_true", rls'= Rule_Set.empty, calc = [], prog_rls = Rule_Set.empty, where_rls = Rule_Set.empty, crls = Rule_Set.empty,
Walther@60586:           errpats = [], rew_rls = Rule_Set.empty},
s1210629013@55377:         "empty_script")]
wneuper@59472: \<close>
jan@42369: 
wneuper@59472: text\<open>\noindent After we generated both nodes, we can fill the containing
jan@42369:       script we want to implement later. First we define the specifications
wneuper@59472:       of the script in e.g. the in- and output.\<close>
jan@42369: 
Walther@60588: setup \<open>Know_Store.add_mets
walther@60154:   [MethodC.prep_input thy "met_SP_Ztrans_inv" [] e_metID
s1210629013@55377:       (["SignalProcessing", "Z_Transform", "Inverse"], 
wneuper@59550:         [("#Given" ,["filterExpression X_eq", "boundVariable X_z"]),
wneuper@59550:           ("#Find", ["stepResponse n_eq"])],
Walther@60586:         {rew_ord="tless_true", rls'= Rule_Set.empty, calc = [], prog_rls = Rule_Set.empty, where_rls = Rule_Set.empty, crls = Rule_Set.empty,
Walther@60586:           errpats = [], rew_rls = Rule_Set.empty},
s1210629013@55377:         "empty_script")]
wneuper@59472: \<close>
jan@42369: 
wneuper@59472: text\<open>\noindent After we stored the definition we can start implementing the
jan@42369:       script itself. As a first try we define only three rows containing one
wneuper@59472:       simple operation.\<close>
jan@42369: 
Walther@60588: setup \<open>Know_Store.add_mets
walther@60154:   [MethodC.prep_input thy "met_SP_Ztrans_inv" [] e_metID
s1210629013@55377:       (["SignalProcessing", "Z_Transform", "Inverse"], 
wneuper@59550:         [("#Given" , ["filterExpression X_eq", "boundVariable X_z"]),
wneuper@59550:           ("#Find", ["stepResponse n_eq"])],
Walther@60586:         {rew_ord="tless_true", rls'= Rule_Set.empty, calc = [], prog_rls = Rule_Set.empty, where_rls = Rule_Set.empty, crls = Rule_Set.empty,
Walther@60586:           errpats = [], rew_rls = Rule_Set.empty},
wneuper@59585:         "Program InverseZTransform (Xeq::bool) =" ^ (*TODO boundVariable X_z*)
s1210629013@55377:           " (let X = Take Xeq;" ^
walther@59635:           "      X = Rewrite ruleZY X" ^
s1210629013@55377:           "  in X)")]
wneuper@59472: \<close>
jan@42369: 
wneuper@59472: text\<open>\noindent Check if the method has been stored correctly\ldots\<close>
jan@42369: 
wneuper@59472: ML \<open>
jan@42369:   show_mets(); 
wneuper@59472: \<close>
jan@42369: 
wneuper@59472: text\<open>\noindent If yes we can get the method by stepping backwards through
wneuper@59472:       the hierarchy.\<close>
jan@42369: 
wneuper@59472: ML \<open>
Walther@60559:   MethodC.from_store ctxt ["SignalProcessing", "Z_Transform", "Inverse"];
wneuper@59472: \<close>
neuper@42279: 
wneuper@59472: section \<open>Program in TP-based language \label{prog-steps}\<close>
jan@42369: 
wneuper@59472: text\<open>\noindent We start stepwise expanding our program. The script is a
neuper@42376:       simple string containing several manipulation instructions.
jan@42370:       \par The first script we try contains no instruction, we only test if
wneuper@59472:       building scripts that way work.\<close>
jan@42369: 
wneuper@59472: subsection \<open>Stepwise Extend the Program\<close>
wneuper@59472: ML \<open>
jan@42370:   val str = 
wneuper@59585:     "Program InverseZTransform (Xeq::bool) =                          "^
jan@42370:     " Xeq";
wneuper@59472: \<close>
jan@42300: 
wneuper@59472: text\<open>\noindent Next we put some instructions in the script and try if we are
wneuper@59472:       able to solve our first equation.\<close>
jan@42370: 
wneuper@59472: ML \<open>
jan@42370:   val str = 
wneuper@59585:     "Program InverseZTransform (Xeq::bool) =                          "^
jan@42370:     (*
walther@60242:      * 1/z) instead of z \<up> -1
jan@42370:      *)
jan@42381:     " (let X = Take Xeq;                                             "^
jan@42381:     "      X' = Rewrite ruleZY False X;                              "^
jan@42370:     (*
jan@42370:      * z * denominator
jan@42370:      *)
jan@42381:     "      X' = (Rewrite_Set norm_Rational False) X'                 "^
jan@42370:     (*
jan@42370:      * simplify
jan@42370:      *)
jan@42370:     "  in X)";
jan@42370:     (*
jan@42370:      * NONE
jan@42370:      *)
wneuper@59585:     "Program InverseZTransform (Xeq::bool) =                          "^
jan@42370:     (*
walther@60242:      * (1/z) instead of z \<up> -1
jan@42370:      *)
jan@42381:     " (let X = Take Xeq;                                             "^
jan@42381:     "      X' = Rewrite ruleZY False X;                              "^
jan@42370:     (*
jan@42370:      * z * denominator
jan@42370:      *)
jan@42381:     "      X' = (Rewrite_Set norm_Rational False) X';                "^
jan@42370:     (*
jan@42370:      * simplify
jan@42370:      *)
wneuper@59476:     "      X' = (SubProblem (IsacX,[pqFormula,degree_2,              "^
jan@42381:     "                               polynomial,univariate,equation], "^
jan@42381:     "                              [no_met])                         "^
jan@42381:     "                              [BOOL e_e, REAL v_v])             "^
jan@42370:     "            in X)";
wneuper@59472: \<close>
jan@42370: 
wneuper@59472: text\<open>\noindent To solve the equation it is necessary to drop the left hand
jan@42370:       side, now we only need the denominator of the right hand side. The first
wneuper@59472:       equation solves the zeros of our expression.\<close>
jan@42370: 
wneuper@59472: ML \<open>
jan@42370:   val str = 
wneuper@59585:     "Program InverseZTransform (Xeq::bool) =                          "^
jan@42381:     " (let X = Take Xeq;                                             "^
jan@42381:     "      X' = Rewrite ruleZY False X;                              "^
jan@42381:     "      X' = (Rewrite_Set norm_Rational False) X';                "^
jan@42381:     "      funterm = rhs X'                                          "^
jan@42370:     (*
jan@42370:      * drop X'= for equation solving
jan@42370:      *)
jan@42370:     "  in X)";
wneuper@59472: \<close>
jan@42370: 
wneuper@59472: text\<open>\noindent As mentioned above, we need the denominator of the right hand
jan@42370:       side. The equation itself consists of this denominator and tries to find
wneuper@59472:       a $z$ for this the denominator is equal to zero.\<close>
jan@42370: 
wneuper@59585: text \<open> dropped during switch from Program to partial_function:
jan@42370:   val str = 
wneuper@59585:     "Program InverseZTransform (X_eq::bool) =                         "^
jan@42381:     " (let X = Take X_eq;                                            "^
jan@42381:     "      X' = Rewrite ruleZY False X;                              "^
jan@42381:     "      X' = (Rewrite_Set norm_Rational False) X';                "^
jan@42381:     "      (X'_z::real) = lhs X';                                    "^
jan@42381:     "      (z::real) = argument_in X'_z;                             "^
jan@42381:     "      (funterm::real) = rhs X';                                 "^
jan@42381:     "      (denom::real) = get_denominator funterm;                  "^
jan@42370:     (*
jan@42370:      * get_denominator
jan@42370:      *)
jan@42381:     "      (equ::bool) = (denom = (0::real));                        "^
jan@42381:     "      (L_L::bool list) =                                        "^
wneuper@59546:     "            (SubProblem (Test,                                 "^
neuper@55279:     "                         [LINEAR,univariate,equation,test],     "^
jan@42381:     "                         [Test,solve_linear])                   "^
jan@42381:     "                         [BOOL equ, REAL z])                    "^
jan@42370:     "  in X)";
jan@42370: 
jan@42370:   parse thy str;
wneuper@59395:   val sc = (inst_abs o Thm.term_of o the o (parse thy)) str;
Walther@60650:   TermC.atom_trace_detail @{context} sc;
wneuper@59472: \<close>
jan@42370: 
wneuper@59472: text \<open>\noindent This ruleset contains all functions that are in the script; 
wneuper@59472:        The evaluation of the functions is done by rewriting using this ruleset.\<close>
jan@42370: 
wneuper@59472: ML \<open>
Walther@60586:   val prog_rls = 
walther@59851:     Rule_Set.Repeat {id="srls_InverseZTransform", 
jan@42381:          preconds = [],
jan@42381:          rew_ord = ("termlessI",termlessI),
Walther@60586:          asm_rls = Rule_Set.append_rules "erls_in_srls_InverseZTransform" Rule_Set.empty
jan@42381:            [(*for asm in NTH_CONS ...*)
wenzelm@60309:             Eval (\<^const_name>\<open>less\<close>,eval_equ "#less_"),
jan@42381:             (*2nd NTH_CONS pushes n+-1 into asms*)
Walther@60516:             Eval(\<^const_name>\<open>plus\<close>, Calc_Binop.numeric "#add_")
jan@42381:            ], 
Walther@60586:          prog_rls = Rule_Set.Empty, calc = [], errpatts = [],
jan@42381:          rules = [
walther@59871:                   Thm ("NTH_CONS",ThmC.numerals_to_Free @{thm NTH_CONS}),
Walther@60516:                   Eval(\<^const_name>\<open>plus\<close>, Calc_Binop.numeric "#add_"),
walther@59871:                   Thm ("NTH_NIL",ThmC.numerals_to_Free @{thm NTH_NIL}),
walther@59878:                   Eval("Prog_Expr.lhs", eval_lhs"eval_lhs_"),
walther@59878:                   Eval("Prog_Expr.rhs", eval_rhs"eval_rhs_"),
walther@59878:                   Eval("Prog_Expr.argument'_in", eval_argument_in "Prog_Expr.argument'_in"),
walther@59878:                   Eval("Rational.get_denominator", eval_get_denominator "#get_denominator"),
walther@59878:                   Eval("Rational.get_numerator", eval_get_numerator "#get_numerator"),
walther@59878:                   Eval("Partial_Fractions.factors_from_solution",
walther@59603:                        eval_factors_from_solution "#factors_from_solution"),
walther@59878:                   Eval("Partial_Fractions.drop_questionmarks",
jan@42381:                        eval_drop_questionmarks "#drop_?")
jan@42381:                  ],
Walther@60586:          program = Empty_Prog};
wneuper@59472: \<close>
jan@42370: 
jan@42370: 
wneuper@59472: subsection \<open>Store Final Version of Program for Execution\<close>
jan@42370: 
wneuper@59472: text\<open>\noindent After we also tested how to write scripts and run them,
jan@42370:       we start creating the final version of our script and store it into
jan@42381:       the method for which we created a node in Section~\ref{sec:cparentnode}
jan@42370:       Note that we also did this stepwise, but we didn't kept every
wneuper@59472:       subversion.\<close>
jan@42370: 
Walther@60588: setup \<open>Know_Store.add_mets
walther@60154:   [MethodC.prep_input thy "met_SP_Ztrans_inv" [] e_metID
s1210629013@55377:       (["SignalProcessing", "Z_Transform", "Inverse"], 
wneuper@59550:         [("#Given" , ["filterExpression X_eq"]), (*TODO boundVariable X_z*)
wneuper@59550:           ("#Find", ["stepResponse n_eq"])],
Walther@60586:         {rew_ord="tless_true", rls'= Rule_Set.empty, calc = [], prog_rls = prog_rls, where_rls = Rule_Set.empty, crls = Rule_Set.empty,
Walther@60586:           errpats = [], rew_rls = Rule_Set.empty},
wneuper@59585:         "Program InverseZTransform (X_eq::bool) =                        "^
walther@60242:           (*(1/z) instead of z \<up> -1*)
s1210629013@55377:           "(let X = Take X_eq;                                            "^
s1210629013@55377:           "      X' = Rewrite ruleZY False X;                             "^
s1210629013@55377:           (*z * denominator*)
s1210629013@55377:           "      (num_orig::real) = get_numerator (rhs X');               "^
s1210629013@55377:           "      X' = (Rewrite_Set norm_Rational False) X';               "^
s1210629013@55377:           (*simplify*)
s1210629013@55377:           "      (X'_z::real) = lhs X';                                   "^
s1210629013@55377:           "      (zzz::real) = argument_in X'_z;                          "^
s1210629013@55377:           "      (funterm::real) = rhs X';                                "^
s1210629013@55377:           (*drop X' z = for equation solving*)
s1210629013@55377:           "      (denom::real) = get_denominator funterm;                 "^
s1210629013@55377:           (*get_denominator*)
s1210629013@55377:           "      (num::real) = get_numerator funterm;                     "^
s1210629013@55377:           (*get_numerator*)
s1210629013@55377:           "      (equ::bool) = (denom = (0::real));                       "^
wneuper@59476:           "      (L_L::bool list) = (SubProblem (PolyEqX,                 "^
s1210629013@55377:           "         [abcFormula,degree_2,polynomial,univariate,equation], "^
s1210629013@55377:           "         [no_met])                                             "^
s1210629013@55377:           "         [BOOL equ, REAL zzz]);                                "^
s1210629013@55377:           "      (facs::real) = factors_from_solution L_L;                "^
s1210629013@55377:           "      (eql::real) = Take (num_orig / facs);                    "^ 
s1210629013@55377: 
s1210629013@55377:           "      (eqr::real) = (Try (Rewrite_Set ansatz_rls False)) eql;  "^
s1210629013@55377: 
s1210629013@55377:           "      (eq::bool) = Take (eql = eqr);                           "^
s1210629013@55377:           (*Maybe possible to use HOLogic.mk_eq ??*)
s1210629013@55377:           "      eq = (Try (Rewrite_Set equival_trans False)) eq;         "^ 
s1210629013@55377: 
s1210629013@55377:           "      eq = drop_questionmarks eq;                              "^
s1210629013@55377:           "      (z1::real) = (rhs (NTH 1 L_L));                          "^
s1210629013@55377:           (* 
s1210629013@55377:           * prepare equation for a - eq_a
s1210629013@55377:           * therefor substitute z with solution 1 - z1
s1210629013@55377:           *)
s1210629013@55377:           "      (z2::real) = (rhs (NTH 2 L_L));                          "^
s1210629013@55377: 
s1210629013@55377:           "      (eq_a::bool) = Take eq;                                  "^
s1210629013@55377:           "      eq_a = (Substitute [zzz=z1]) eq;                         "^
s1210629013@55377:           "      eq_a = (Rewrite_Set norm_Rational False) eq_a;           "^
s1210629013@55377:           "      (sol_a::bool list) =                                     "^
wneuper@59476:           "                 (SubProblem (IsacX,                           "^
s1210629013@55377:           "                              [univariate,equation],[no_met])  "^
s1210629013@55377:           "                              [BOOL eq_a, REAL (A::real)]);    "^
s1210629013@55377:           "      (a::real) = (rhs(NTH 1 sol_a));                          "^
s1210629013@55377: 
s1210629013@55377:           "      (eq_b::bool) = Take eq;                                  "^
s1210629013@55377:           "      eq_b =  (Substitute [zzz=z2]) eq_b;                      "^
s1210629013@55377:           "      eq_b = (Rewrite_Set norm_Rational False) eq_b;           "^
s1210629013@55377:           "      (sol_b::bool list) =                                     "^
wneuper@59476:           "                 (SubProblem (IsacX,                           "^
s1210629013@55377:           "                              [univariate,equation],[no_met])  "^
s1210629013@55377:           "                              [BOOL eq_b, REAL (B::real)]);    "^
s1210629013@55377:           "      (b::real) = (rhs(NTH 1 sol_b));                          "^
s1210629013@55377: 
s1210629013@55377:           "      eqr = drop_questionmarks eqr;                            "^
s1210629013@55377:           "      (pbz::real) = Take eqr;                                  "^
s1210629013@55377:           "      pbz = ((Substitute [A=a, B=b]) pbz);                     "^
s1210629013@55377: 
s1210629013@55377:           "      pbz = Rewrite ruleYZ False pbz;                          "^
s1210629013@55377:           "      pbz = drop_questionmarks pbz;                            "^
s1210629013@55377: 
s1210629013@55377:           "      (X_z::bool) = Take (X_z = pbz);                          "^
s1210629013@55377:           "      (n_eq::bool) = (Rewrite_Set inverse_z False) X_z;        "^
s1210629013@55377:           "      n_eq = drop_questionmarks n_eq                           "^
s1210629013@55377:           "in n_eq)")]
wneuper@59472: \<close>
jan@42370: 
jan@42370: 
wneuper@59472: subsection \<open>Check the Program\<close>
wneuper@59472: text\<open>\noindent When the script is ready we can start checking our work.\<close>
wneuper@59472: subsubsection \<open>Check the Formalization\<close>
wneuper@59472: text\<open>\noindent First we want to check the formalization of the in and
wneuper@59472:        output of our program.\<close>
jan@42370: 
wneuper@59472: ML \<open>
jan@42370:   val fmz = 
jan@42370:     ["filterExpression (X  = 3 / (z - 1/4 + -1/8 * (1/(z::real))))",
jan@42370:      "stepResponse (x[n::real]::bool)"];
jan@42370:   val (dI,pI,mI) = 
wneuper@59592:     ("Isac_Knowledge", ["Inverse", "Z_Transform", "SignalProcessing"], 
walther@59997:              ["SignalProcessing", "Z_Transform", "Inverse"]);
jan@42370: 
jan@42370:   val ([
jan@42370:           (
jan@42370:             1,
jan@42370:             [1],
jan@42370:             "#Given",
jan@42370:             Const ("Inverse_Z_Transform.filterExpression", _),
wenzelm@60309:             [Const (\<^const_name>\<open>HOL.eq\<close>, _) $ _ $ _]
jan@42370:           ),
jan@42370:           (
jan@42370:             2,
jan@42370:             [1],
jan@42370:             "#Find",
jan@42370:             Const ("Inverse_Z_Transform.stepResponse", _),
jan@42370:             [Free ("x", _) $ _]
jan@42370:           )
jan@42370:        ],_
Walther@60586:       ) = O_Model.init thy fmz ((#model o Problem.from_store) pI);
jan@42370: 
neuper@48790:   val Prog sc 
Walther@60586:     = (#program o MethodC.from_store ctxt) ["SignalProcessing",
jan@42370:                         "Z_Transform",
neuper@42405:                         "Inverse"];
Walther@60650:   TermC.atom_trace_detail @{context} sc;
wneuper@59472: \<close>
jan@42370: 
wneuper@59472: subsubsection \<open>Stepwise Check the Program\label{sec:stepcheck}\<close>
wneuper@59472: text\<open>\noindent We start to stepwise execute our new program in a calculation
wneuper@59472:       tree and check if every node implements that what we have wanted.\<close>
jan@42370:       
wneuper@59472: ML \<open>
walther@60330:   Rewrite.trace_on := false; (*true false*)
walther@59901:   LItool.trace_on := false; (*true*)
jan@42370:   print_depth 9;
jan@42370:   
jan@42370:   val fmz =
jan@42418:     ["filterExpression (X z = 3 / ((z::real) + 1/10 - 1/50*(1/z)))",
jan@42370:      "stepResponse (x[n::real]::bool)"];
jan@42370:      
jan@42370:   val (dI,pI,mI) =
wneuper@59592:     ("Isac_Knowledge", ["Inverse", "Z_Transform", "SignalProcessing"], 
walther@59997:              ["SignalProcessing", "Z_Transform", "Inverse"]);
jan@42370:              
Walther@60571:   val (p,_,f,nxt,_,pt)  = Test_Code.init_calc @{context} [(fmz, (dI,pI,mI))];
jan@42370:   val (p,_,f,nxt,_,pt) = me nxt p [] pt; 
jan@42370:     "Add_Given";
jan@42370:   val (p,_,f,nxt,_,pt) = me nxt p [] pt;
jan@42370:     "Add_Find";
jan@42370:   val (p,_,f,nxt,_,pt) = me nxt p [] pt;
jan@42370:     "Specify_Theory";
jan@42370:   val (p,_,f,nxt,_,pt) = me nxt p [] pt;
jan@42370:     "Specify_Problem";
jan@42370:   val (p,_,f,nxt,_,pt) = me nxt p [] pt;
jan@42370:     "Specify_Method";
jan@42370:   val (p,_,f,nxt,_,pt) = me nxt p [] pt;
jan@42370:     "Apply_Method";
jan@42370:   val (p,_,f,nxt,_,pt) = me nxt p [] pt;
jan@42370:     "Rewrite (ruleZY, Inverse_Z_Transform.ruleZY)";
jan@42370:     "--> X z = 3 / (z - 1 / 4 + -1 / 8 * (1 / z))";
jan@42370:   (*
jan@42370:    * TODO naming!
jan@42370:    *)
jan@42370:   val (p,_,f,nxt,_,pt) = me nxt p [] pt;
jan@42370:     "Rewrite_Set norm_Rational";
jan@42370:     " --> X' z = 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))";
jan@42371:   val (p,_,f,nxt,_,pt) = me nxt p [] pt; 
jan@42370:     "SubProblem";
neuper@52101:   print_depth 3;
wneuper@59472: \<close>
jan@42370: 
wneuper@59472: text \<open>\noindent Instead of \ttfamily nxt = Subproblem \normalfont above we had
jan@42370:        \ttfamily Empty\_Tac; \normalfont the search for the reason considered
jan@42370:        the following points:\begin{itemize}
jan@42381:        \item What shows \ttfamily show\_pt pt;\normalfont\ldots?
walther@60242: \begin{verbatim}(([2], Res), ?X' z = 24 / (-1 + -2 * z + 8 * z \<up> 2))]\end{verbatim}
jan@42370:          The calculation is ok but no \ttfamily next \normalfont step found:
jan@42370:          Should be\\ \ttfamily nxt = Subproblem\normalfont!
jan@42370:        \item What shows \ttfamily trace\_script := true; \normalfont we read
jan@42381:          bottom up\ldots
jan@42381:      \begin{verbatim}
jan@42381:      @@@next leaf 'SubProblem
jan@42381:      (PolyEq',[abcFormula, degree_2, polynomial, 
jan@42381:                univariate, equation], no_meth)
jan@42381:      [BOOL equ, REAL z]' 
walther@59717:        ---> Program.Tac 'SubProblem (PolyEq',
jan@42381:               [abcFormula, degree_2, polynomial,
jan@42381:                univariate, equation], no_meth)
jan@42381:      [BOOL (-1 + -2 * z + 8 * z \^\^\^ ~2 = 0), REAL z]'
jan@42381:      \end{verbatim}
jan@42370:          We see the SubProblem with correct arguments from searching next
walther@59717:          step (program text !!!--->!!! Program.Tac (script tactic) with arguments
jan@42370:          evaluated.)
wneuper@59585:      \item Do we have the right Program \ldots difference in the
jan@42381:          arguments in the arguments\ldots
jan@42381:          \begin{verbatim}
neuper@48790:      val Prog s =
Walther@60586:      (#program o MethodC.from_store ctxt) ["SignalProcessing",
jan@42381:                        "Z_Transform",
neuper@42405:                        "Inverse"];
walther@59868:      writeln (UnparseC.term s);
jan@42381:          \end{verbatim}
jan@42370:          \ldots shows the right script. Difference in the arguments.
jan@42370:      \item Test --- Why helpless here ? --- shows: \ttfamily replace
wneuper@59585:          no\_meth by [no\_meth] \normalfont in Program
jan@42370:      \end{itemize}
wneuper@59472: \<close>
jan@42300: 
wneuper@59472: ML \<open>
jan@42370:   val (p,_,f,nxt,_,pt) = me nxt p [] pt; 
jan@42370:     (*Model_Problem";*)
wneuper@59472: \<close>
neuper@42279: 
wneuper@59472: text \<open>\noindent Instead of \ttfamily nxt = Model\_Problem \normalfont above
jan@42370:        we had \ttfamily Empty\_Tac; \normalfont the search for the reason 
jan@42370:        considered the following points:\begin{itemize}
jan@42370:        \item Difference in the arguments
jan@42381:        \item Comparison with Subsection~\ref{sec:solveq}: There solving this
jan@42370:          equation works, so there must be some difference in the arguments
jan@42370:          of the Subproblem: RIGHT: we had \ttfamily [no\_meth] \normalfont
jan@42370:          instead of \ttfamily [no\_met] \normalfont ;-)
wneuper@59472:        \end{itemize}\<close>
jan@42338: 
wneuper@59472: ML \<open>
jan@42370:   val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@60242:     (*Add_Given equality (-1 + -2 * z + 8 * z \<up> 2 = 0)";*)
jan@42370:   val (p,_,f,nxt,_,pt) = me nxt p [] pt;
jan@42370:     (*Add_Given solveFor z";*)
jan@42370:   val (p,_,f,nxt,_,pt) = me nxt p [] pt;
jan@42370:     (*Add_Find solutions z_i";*)
jan@42370:   val (p,_,f,nxt,_,pt) = me nxt p [] pt;
jan@42370:     (*Specify_Theory Isac";*)
wneuper@59472: \<close>
neuper@42279: 
wneuper@59472: text \<open>\noindent We had \ttfamily nxt = Empty\_Tac instead Specify\_Theory;
jan@42370:        \normalfont The search for the reason considered the following points:
jan@42370:        \begin{itemize}
jan@42370:        \item Was there an error message? NO -- ok
jan@42370:        \item Has \ttfamily nxt = Add\_Find \normalfont been inserted in pt:\\
jan@42370:          \ttfamily get\_obj g\_pbl pt (fst p);\normalfont? YES -- ok
jan@42381:        \item What is the returned formula:
jan@42381: \begin{verbatim}
neuper@52101: print_depth 999; f; print_depth 3;
jan@42381: { Find = [ Correct "solutions z_i"],
jan@42381:   With = [],
walther@60242:   Given = [Correct "equality (-1 + -2*z + 8*z \<up> 2 = 0)",
jan@42381:            Correct "solveFor z"],
jan@42381:   Where = [...],
jan@42381:   Relate = [] }
jan@42381: \end{verbatim}
jan@42370:      \normalfont The only False is the reason: the Where (the precondition) is
jan@42370:      False for good reasons: The precondition seems to check for linear
jan@42370:      equations, not for the one we want to solve! Removed this error by
wneuper@59585:      correcting the Program from \ttfamily SubProblem (PolyEq',
jan@42370:      \lbrack linear,univariate,equation,
jan@42370:        test\rbrack, \lbrack Test,solve\_linear\rbrack \normalfont to
jan@42370:      \ttfamily SubProblem (PolyEq',\\ \lbrack abcFormula,degree\_2,
jan@42370:        polynomial,univariate,equation\rbrack,\\
jan@42370:                    \lbrack PolyEq,solve\_d2\_polyeq\_abc\_equation
jan@42370:                    \rbrack\normalfont
jan@42370:      You find the appropriate type of equation at the
jan@42370:      {\sisac}-WEB-Page\footnote{
jan@42370:      \href{http://www.ist.tugraz.at/projects/isac/www/kbase/pbl/index\_pbl.html}
jan@42370:           {http://www.ist.tugraz.at/projects/isac/www/kbase/pbl/index\_pbl.html}
jan@42370:                                }
jan@42370:      And the respective method in \ttfamily Knowledge/PolyEq.thy \normalfont
jan@42370:      at the respective \ttfamily store\_pbt. \normalfont Or you leave the
wneuper@59585:      selection of the appropriate type to isac as done in the final Program ;-))
wneuper@59472:   \end{itemize}\<close>
jan@42370:   
wneuper@59472: ML \<open>
jan@42370:   val (p,_,f,nxt,_,pt) = me nxt p [] pt; 
jan@42370:     (*Specify_Problem [abcFormula,...";*)
jan@42370:   val (p,_,f,nxt,_,pt) = me nxt p [] pt;
jan@42370:     (*Specify_Method [PolyEq,solve_d2_polyeq_abc_equation";*)
jan@42370:   val (p,_,f,nxt,_,pt) = me nxt p [] pt; 
jan@42370:     (*Apply_Method [PolyEq,solve_d2_polyeq_abc_equation";*)
jan@42370:   val (p,_,f,nxt,_,pt) = me nxt p [] pt;
wneuper@59497:     (*Rewrite_Set_Inst [(''bdv'', z)], d2_polyeq_abcFormula_simplify";*)
jan@42370:   val (p,_,f,nxt,_,pt) = me nxt p [] pt;
jan@42370:   val (p,_,f,nxt,_,pt) = me nxt p [] pt;
jan@42370:   val (p,_,f,nxt,_,pt) = me nxt p [] pt;
jan@42370:   val (p,_,f,nxt,_,pt) = me nxt p [] pt;
jan@42370:   val (p,_,f,nxt,_,pt) = me nxt p [] pt;
jan@42370:   val (p,_,f,nxt,_,pt) = me nxt p [] pt;
jan@42370:   val (p,_,f,nxt,_,pt) = me nxt p [] pt;
jan@42370:   val (p,_,f,nxt,_,pt) = me nxt p [] pt;
jan@42370:   val (p,_,f,nxt,_,pt) = me nxt p [] pt;
jan@42370:   val (p,_,f,nxt,_,pt) = me nxt p [] pt;
jan@42370:   val (p,_,f,nxt,_,pt) = me nxt p [] pt;
jan@42370:   val (p,_,f,nxt,_,pt) = me nxt p [] pt;
jan@42370:   val (p,_,f,nxt,_,pt) = me nxt p [] pt;
jan@42370:   val (p,_,f,nxt,_,pt) = me nxt p [] pt;
jan@42370:   val (p,_,f,nxt,_,pt) = me nxt p [] pt;
jan@42370:   val (p,_,f,nxt,_,pt) = me nxt p [] pt;
jan@42370:   val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59997:     (*Specify_Problem ["normalise", "polynomial", "univariate", "equation"]*)
jan@42370:   val (p,_,f,nxt,_,pt) = me nxt p [] pt;
wneuper@59370:     (*Specify_Method ["PolyEq", "normalise_poly"]*)
jan@42370:   val (p,_,f,nxt,_,pt) = me nxt p [] pt;
wneuper@59370:     (*Apply_Method ["PolyEq", "normalise_poly"]*)
jan@42370:   val (p,_,f,nxt,_,pt) = me nxt p [] pt;
jan@42370:     (*Rewrite ("all_left", "PolyEq.all_left")*)
jan@42370:   val (p,_,f,nxt,_,pt) = me nxt p [] pt;
wneuper@59497:     (*Rewrite_Set_Inst (["(''bdv'', A)"], "make_ratpoly_in")*)
jan@42370:   val (p,_,f,nxt,_,pt) = me nxt p [] pt; 
jan@42370:     (*Rewrite_Set "polyeq_simplify"*)
jan@42370:   val (p,_,f,nxt,_,pt) = me nxt p [] pt; 
walther@59997:     (*Subproblem("Isac_Knowledge",["degree_1", "polynomial", "univariate", "equation"])*)
jan@42370:   val (p,_,f,nxt,_,pt) = me nxt p [] pt;
jan@42370:   val (p,_,f,nxt,_,pt) = me nxt p [] pt;
jan@42370:   val (p,_,f,nxt,_,pt) = me nxt p [] pt;
jan@42370:   val (p,_,f,nxt,_,pt) = me nxt p [] pt;
jan@42370:   val (p,_,f,nxt,_,pt) = me nxt p [] pt;
jan@42370:   val (p,_,f,nxt,_,pt) = me nxt p [] pt;
jan@42370:   val (p,_,f,nxt,_,pt) = me nxt p [] pt;
jan@42370:   val (p,_,f,nxt,_,pt) = me nxt p [] pt;
jan@42370:   val (p,_,f,nxt,_,pt) = me nxt p [] pt;
jan@42370:   val (p,_,f,nxt,_,pt) = me nxt p [] pt;
jan@42370:   val (p,_,f,nxt,_,pt) = me nxt p [] pt;
jan@42370:   val (p,_,f,nxt,_,pt) = me nxt p [] pt;
jan@42370:   val (p,_,f,nxt,_,pt) = me nxt p [] pt;
jan@42370:   val (p,_,f,nxt,_,pt) = me nxt p [] pt;
jan@42370:   val (p,_,f,nxt,_,pt) = me nxt p [] pt;
jan@42370:   val (p,_,f,nxt,_,pt) = me nxt p [] pt;
jan@42370:   val (p,_,f,nxt,_,pt) = me nxt p [] pt;
jan@42370:   val (p,_,f,nxt,_,pt) = me nxt p [] pt;
jan@42370:   val (p,_,f,nxt,_,pt) = me nxt p [] pt;
jan@42370:   val (p,_,f,nxt,_,pt) = me nxt p [] pt;
jan@42370:   val (p,_,f,nxt,_,pt) = me nxt p [] pt;
jan@42370:   val (p,_,f,nxt,_,pt) = me nxt p [] pt;
jan@42370:   val (p,_,f,nxt,_,pt) = me nxt p [] pt;
jan@42370:   val (p,_,f,nxt,_,pt) = me nxt p [] pt;
jan@42370:   val (p,_,f,nxt,_,pt) = me nxt p [] pt;
jan@42370:   val (p,_,f,nxt,_,pt) = me nxt p [] pt;
jan@42370:   val (p,_,f,nxt,_,pt) = me nxt p [] pt;
jan@42370:   val (p,_,f,nxt,_,pt) = me nxt p [] pt;
jan@42370:   val (p,_,f,nxt,_,pt) = me nxt p [] pt;
jan@42370:   val (p,_,f,nxt,_,pt) = me nxt p [] pt;
jan@42370:   val (p,_,f,nxt,_,pt) = me nxt p [] pt;
jan@42370:   val (p,_,f,nxt,_,pt) = me nxt p [] pt;
jan@42370:   val (p,_,f,nxt,_,pt) = me nxt p [] pt;
jan@42370:   val (p,_,f,nxt,_,pt) = me nxt p [] pt;
jan@42370:   val (p,_,f,nxt,_,pt) = me nxt p [] pt;
jan@42370:   val (p,_,f,nxt,_,pt) = me nxt p [] pt;
jan@42370:   val (p,_,f,nxt,_,pt) = me nxt p [] pt;
jan@42370:   val (p,_,f,nxt,_,pt) = me nxt p [] pt;
jan@42370:   val (p,_,f,nxt,_,pt) = me nxt p [] pt;
jan@42370:   val (p,_,f,nxt,_,pt) = me nxt p [] pt;
jan@42370:   val (p,_,f,nxt,_,pt) = me nxt p [] pt;
jan@42370:   val (p,_,f,nxt,_,pt) = me nxt p [] pt;
jan@42370:   val (p,_,f,nxt,_,pt) = me nxt p [] pt;
jan@42370:   val (p,_,f,nxt,_,pt) = me nxt p [] pt;
jan@42370:   val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42451:   val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*([11, 4, 5], Res) Check_Postcond*)
neuper@42451:   val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*([11, 4], Res) Check_Postcond*)
neuper@42451:   val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*([11], Res) Take*)
neuper@42451:   val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*([12], Frm) Substitute*)
neuper@42451:   val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*([12], Res) Rewrite*)
neuper@42451:   val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*([13], Res) Take*)
neuper@42451:   val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*([14], Frm) Empty_Tac*)
wneuper@59472: \<close>
wneuper@59472: ML \<open>
jan@42370:   val (p,_,f,nxt,_,pt) = me nxt p [] pt;
wneuper@59472: \<close>
wneuper@59472: ML \<open>
jan@42370:   val (p,_,f,nxt,_,pt) = me nxt p [] pt;
wneuper@59472: \<close>
wneuper@59472: ML \<open>
jan@42370:   val (p,_,f,nxt,_,pt) = me nxt p [] pt;
wneuper@59472: \<close>
wneuper@59472: ML \<open>
jan@42370:   val (p,_,f,nxt,_,pt) = me nxt p [] pt;
wneuper@59472: \<close>
wneuper@59472: ML \<open>
jan@42370:   val (p,_,f,nxt,_,pt) = me nxt p [] pt;
wneuper@59472: \<close>
wneuper@59472: ML \<open>
jan@42370:   val (p,_,f,nxt,_,pt) = me nxt p [] pt;
wneuper@59472: \<close>
neuper@42281: 
wneuper@59472: ML \<open>
walther@59901: LItool.trace_on := true;
wneuper@59472: \<close>
wneuper@59472: ML \<open>
jan@42418: val (p,_,f,nxt,_,pt) = me nxt p [] pt;
wneuper@59472: \<close>
wneuper@59472: ML \<open>
walther@59983: Test_Tool.show_pt pt;
wneuper@59472: \<close>
wneuper@59472: ML \<open>
wneuper@59472: \<close> 
wneuper@59472: ML \<open>
wneuper@59472: \<close> 
wneuper@59472: ML \<open>
wneuper@59472: \<close> 
wneuper@59472: ML \<open>
wneuper@59472: \<close> 
wneuper@59472: ML \<open>
wneuper@59472: \<close> 
wneuper@59472: ML \<open>
wneuper@59472: \<close> 
jan@42418: 
wneuper@59472: text\<open>\noindent As a last step we check the tracing output of the last calc
Walther@60586:       tree instruction and compare it with the where_-calculated result.\<close>
neuper@42315: 
wneuper@59472: section \<open>Improve and Transfer into Knowledge\<close>
wneuper@59472: text \<open>
neuper@42376:   We want to improve the very long program \ttfamily InverseZTransform
neuper@42376:   \normalfont by modularisation: partial fraction decomposition shall
neuper@42376:   become a sub-problem.
neuper@42376: 
neuper@42376:   We could transfer all knowledge in \ttfamily Build\_Inverse\_Z\_Transform.thy 
neuper@42376:   \normalfont first to the \ttfamily Knowledge/Inverse\_Z\_Transform.thy 
neuper@42376:   \normalfont and then modularise. In this case TODO problems?!?
neuper@42376: 
neuper@42376:   We chose another way and go bottom up: first we build the sub-problem in
jan@42381:   \ttfamily Partial\_Fractions.thy \normalfont with the term:
neuper@42376: 
jan@42381:       $$\frac{3}{x\cdot(z - \frac{1}{4} + \frac{-1}{8}\cdot\frac{1}{z})}$$
neuper@42376: 
jan@42381:   \noindent (how this still can be improved see \ttfamily Partial\_Fractions.thy\normalfont),
neuper@42376:   and re-use all stuff prepared in \ttfamily Build\_Inverse\_Z\_Transform.thy:
jan@42381:   \normalfont The knowledge will be transferred to \ttfamily src/../Partial\_Fractions.thy 
jan@42381:   \normalfont and the respective tests to:
jan@42381:   \begin{center}\ttfamily test/../sartial\_fractions.sml\normalfont\end{center}
wneuper@59472: \<close>
neuper@42279: 
wneuper@59472: subsection \<open>Transfer to Partial\_Fractions.thy\<close>
wneuper@59472: text \<open>
jan@42381:   First we transfer both, knowledge and tests into:
jan@42381:   \begin{center}\ttfamily src/../Partial\_Fractions.thy\normalfont\end{center}
jan@42381:   in order to immediately have the test results.
neuper@42376: 
jan@42381:   We copy \ttfamily factors\_from\_solution, drop\_questionmarks,\\
jan@42381:   ansatz\_2nd\_order \normalfont and rule-sets --- no problem.
jan@42381:   
jan@42381:   Also \ttfamily store\_pbt ..\\ "pbl\_simp\_rat\_partfrac"
neuper@42376:   \normalfont is easy.
neuper@42376: 
jan@42381:   But then we copy from:\\
jan@42381:   (1) \ttfamily Build\_Inverse\_Z\_Transform.thy store\_met\ldots "met\_SP\_Ztrans\_inv"
jan@42381:   \normalfont\\ to\\ 
jan@42381:   (2) \ttfamily Partial\_Fractions.thy store\_met\ldots "met\_SP\_Ztrans\_inv" 
jan@42381:   \normalfont\\ and cut out the respective part from the program. First we ensure that
neuper@42376:   the string is correct. When we insert the string into (2)
jan@42381:   \ttfamily store\_met .. "met\_partial\_fraction" \normalfont --- and get an error.
wneuper@59472: \<close>
neuper@42376: 
wneuper@59472: subsubsection \<open>'Programming' in ISAC's TP-based Language\<close>
wneuper@59472: text \<open>
neuper@42376:   At the present state writing programs in {\sisac} is particularly cumbersome.
neuper@42376:   So we give hints how to cope with the many obstacles. Below we describe the
neuper@42376:   steps we did in making (2) run.
neuper@42376:   
neuper@42376:   \begin{enumerate}
neuper@42376:     \item We check if the \textbf{string} containing the program is correct.
neuper@42376:     \item We check if the \textbf{types in the program} are correct.
neuper@42376:       For this purpose we start start with the first and last lines
jan@42381:      \begin{verbatim}
jan@42381:      "PartFracScript (f_f::real) (v_v::real) =       " ^
jan@42381:      " (let X = Take f_f;                            " ^
jan@42381:      "      pbz = ((Substitute []) X)                " ^
jan@42381:      "  in pbz)"
jan@42381:      \end{verbatim}
neuper@42376:        The last but one line helps not to bother with ';'.
neuper@42376:      \item Then we add line by line. Already the first line causes the error. 
neuper@42376:         So we investigate it by
jan@42381:       \begin{verbatim}
neuper@48761:       val ctxt = Proof_Context.init_global @{theory "Inverse_Z_Transform"} ;
jan@42381:       val SOME t = 
jan@42381:         parseNEW ctxt "(num_orig::real) = 
jan@42381:                           get_numerator(rhs f_f)";
jan@42381:       \end{verbatim}
neuper@42376:         and see a type clash: \ttfamily rhs \normalfont from (1) requires type 
jan@42381:         \ttfamily bool \normalfont while (2) wants to have \ttfamily (f\_f::real).
neuper@42376:         \normalfont Of course, we don't need \ttfamily rhs \normalfont anymore.
neuper@42376:       \item Type-checking can be very tedious. One might even inspect the
jan@42381:         parse-tree of the program with {\sisac}'s specific debug tools:
jan@42381:       \begin{verbatim}
Walther@60586:       val {program = Prog t,...} = 
Walther@60559:         MethodC.from_store ctxt ["simplification",
jan@42381:                  "of_rationals",
jan@42381:                  "to_partial_fraction"];
neuper@42389:       atomty_thy @{theory "Inverse_Z_Transform"} t ;
jan@42381:       \end{verbatim}
neuper@42376:       \item We check if the \textbf{semantics of the program} by stepwise evaluation
neuper@42376:         of the program. Evaluation is done by the Lucas-Interpreter, which works
wneuper@59592:         using the knowledge in theory Isac_Knowledge; so we have to re-build Isac. And the
neuper@42376:         test are performed simplest in a file which is loaded with Isac.
jan@42381:         See \ttfamily tests/../partial\_fractions.sml \normalfont.
neuper@42376:   \end{enumerate}
wneuper@59472: \<close>
neuper@42376: 
wneuper@59472: subsection \<open>Transfer to Inverse\_Z\_Transform.thy\<close>
wneuper@59472: text \<open>
neuper@42388:   It was not possible to complete this task, because we ran out of time.
wneuper@59472: \<close>
neuper@42376: 
neuper@42376: 
neuper@42279: end
neuper@42279: 




