1 (* Title: Build_Inverse_Z_Transform
3 (c) copyright due to license terms.
4 12345678901234567890123456789012345678901234567890123456789012345678901234567890
5 10 20 30 40 50 60 70 80
8 theory Build_Inverse_Z_Transform imports Inverse_Z_Transform
12 text{* We stepwise build \ttfamily Inverse\_Z\_Transform.thy \normalfont as an
13 exercise. Because Subsection~\ref{sec:stepcheck} requires
14 \ttfamily Inverse\_Z\_Transform.thy \normalfont as a subtheory of \ttfamily
15 Isac.thy\normalfont, the setup has been changed from \ttfamily theory
16 Inverse\_Z\_Transform imports Isac \normalfont to the above one.
19 \textbf{Attention with the names of identifiers when going into internals!}
21 Here in this theory there are the internal names twice, for instance we have
22 \ttfamily (Thm.derivation\_name @{thm rule1} =
23 "Build\_Inverse\_Z\_Transform.rule1") = true; \normalfont
24 but actually in us will be \ttfamily Inverse\_Z\_Transform.rule1 \normalfont
27 section {*Trials towards the Z-Transform\label{sec:trials}*}
29 ML {*val thy = @{theory};*}
31 subsection {*Notations and Terms*}
32 text{*\noindent Try which notations we are able to use.*}
34 @{term "1 < || z ||"};
35 @{term "z / (z - 1)"};
37 @{term "-u [-n - 1]"}; (*[ ] denotes lists !!!*)
38 @{term "z /(z - 1) = -u [-n - 1]"};
39 @{term "1 < || z || ==> z / (z - 1) = -u [-n - 1]"};
40 term2str @{term "1 < || z || ==> z / (z - 1) = -u [-n - 1]"};
42 text{*\noindent Try which symbols we are able to use and how we generate them.*}
44 (*alpha --> "</alpha>" *)
49 term2str @{term "\<rho> "};
53 (*axiomatization "z / (z - 1) = -u [-n - 1]"
54 Illegal variable name: "z / (z - 1) = -u [-n - 1]" *)
55 (*definition "z / (z - 1) = -u [-n - 1]"
56 Bad head of lhs: existing constant "op /"*)
58 rule1: "1 = \<delta>[n]" and
59 rule2: "|| z || > 1 ==> z / (z - 1) = u [n]" and
60 rule3: "|| z || < 1 ==> z / (z - 1) = -u [-n - 1]" and
61 rule4: "|| z || > || \<alpha> || ==> z / (z - \<alpha>) = \<alpha>^^^n * u [n]" and
62 rule5: "|| z || < || \<alpha> || ==> z / (z - \<alpha>) = -(\<alpha>^^^n) * u [-n - 1]" and
63 rule6: "|| z || > 1 ==> z/(z - 1)^^^2 = n * u [n]"
65 text{*\noindent Check the rules for their correct notation.
66 (See the machine output.)*}
74 subsection {*Apply Rules*}
75 text{*\noindent We try to apply the rules to a given expression.*}
78 val inverse_Z = append_rls "inverse_Z" e_rls
79 [ Thm ("rule3",num_str @{thm rule3}),
80 Thm ("rule4",num_str @{thm rule4}),
81 Thm ("rule1",num_str @{thm rule1})
84 val t = str2term "z / (z - 1) + z / (z - \<alpha>) + 1";
85 val SOME (t', asm) = rewrite_set_ thy true inverse_Z t;
86 term2str t' = "z / (z - ?\<delta> [?n]) + z / (z - \<alpha>) + ?\<delta> [?n]";
88 * Attention rule1 is applied before the expression is
89 * checked for rule4 which would be correct!!!
93 ML {* val (thy, ro, er) = (@{theory}, tless_true, eval_rls); *}
96 rewrite_ thy ro er true (num_str @{thm rule3}) t;
97 term2str t = "- ?u [- ?n - 1] + z / (z - \<alpha>) + 1";
102 rewrite_ thy ro er true (num_str @{thm rule4}) t;
103 term2str t = "- ?u [- ?n - 1] + \<alpha> ^^^ ?n * ?u [?n] + 1";
108 rewrite_ thy ro er true (num_str @{thm rule1}) t;
109 term2str t = "- ?u [- ?n - 1] + \<alpha> ^^^ ?n * ?u [?n] + ?\<delta> [?n]";
113 ML {* terms2str (asm1 @ asm2 @ asm3); *}
115 section{*Prepare Steps for TP-based programming Language\label{sec:prepstep}*}
117 \par \noindent The following sections are challenging with the CTP-based
118 possibilities of building the program. The goal is realized in
119 Section~\ref{spec-meth} and Section~\ref{prog-steps}.
120 \par The reader is advised to jump between the subsequent subsections and
121 the respective steps in Section~\ref{prog-steps}. By comparing
122 Section~\ref{sec:calc:ztrans} the calculation can be comprehended step
126 subsection {*Prepare Expression\label{prep-expr}*}
127 text{*\noindent We try two different notations and check which of them
128 Isabelle can handle best.*}
130 val ctxt = Proof_Context.init_global @{theory};
131 val ctxt = declare_constraints' [@{term "z::real"}] ctxt;
134 parseNEW ctxt "X z = 3 / (z - 1/4 + -1/8 * z ^^^ -1)"; term2str fun1;
136 parseNEW ctxt "X z = 3 / (z - 1/4 + -1/8 * (1/z))"; term2str fun1';
139 subsubsection {*Prepare Numerator and Denominator*}
140 text{*\noindent The partial fraction decomposition is only possible if we
141 get the bound variable out of the numerator. Therefor we divide
142 the expression by $z$. Follow up the Calculation at
143 Section~\ref{sec:calc:ztrans} line number 02.*}
146 ruleZY: "(X z = a / b) = (X' z = a / (z * b))"
149 val (thy, ro, er) = (@{theory}, tless_true, eval_rls);
150 val SOME (fun2, asm1) =
151 rewrite_ thy ro er true @{thm ruleZY} fun1; term2str fun2;
152 val SOME (fun2', asm1) =
153 rewrite_ thy ro er true @{thm ruleZY} fun1'; term2str fun2';
156 rewrite_set_ @{theory} false norm_Rational fun2;
160 * We solve this problem by using 1/x as a workaround.
163 rewrite_set_ @{theory} false norm_Rational fun2';
170 subsubsection {*Get the Argument of the Expression X'*}
171 text{*\noindent We use \texttt{grep} for finding possibilities how we can
172 extract the bound variable in the expression. \ttfamily Atools.thy,
173 Tools.thy \normalfont contain general utilities: \ttfamily
174 eval\_argument\_in, eval\_rhs, eval\_lhs,\ldots \normalfont
175 \ttfamily grep -r "fun eva\_" * \normalfont shows all functions
176 witch can be used in a script. Lookup this files how to build
177 and handle such functions.
178 \par The next section shows how to introduce such a function.
181 subsubsection{*Decompose the Given Term Into lhs and rhs*}
183 val (_, expr) = HOLogic.dest_eq fun3'; term2str expr;
185 HOLogic.dest_bin "Fields.inverse_class.divide" (type_of expr) expr;
186 term2str denom = "-1 + -2 * z + 8 * z ^^^ 2";
189 text{*\noindent We have rhs\footnote{Note: lhs means \em Left Hand Side
190 \normalfont and rhs means \em Right Hand Side \normalfont and indicates
191 the left or the right part of an equation.} in the Script language, but
192 we need a function which gets the denominator of a fraction.*}
194 subsubsection{*Get the Denominator and Numerator out of a Fraction*}
195 text{*\noindent The self written functions in e.g. \texttt{get\_denominator}
196 should become a constant for the Isabelle parser:*}
199 get_denominator :: "real => real"
200 get_numerator :: "real => real"
202 text {*\noindent With the above definition we run into problems when we parse
203 the Script \texttt{InverseZTransform}. This leads to \em ambiguous
204 parse trees. \normalfont We avoid this by moving the definition
205 to \ttfamily Rational.thy \normalfont and re-building {\sisac}.
206 \par \noindent ATTENTION: From now on \ttfamily
207 Build\_Inverse\_Z\_Transform \normalfont mimics a build from scratch;
208 it only works due to re-building {\sisac} several times (indicated
215 * ("Rational.get_denominator", eval_get_denominator ""))
217 fun eval_get_denominator (thmid:string) _
218 (t as Const ("Rational.get_denominator", _) $
219 (Const ("Fields.inverse_class.divide", _) $num
221 SOME (mk_thmid thmid "" (term_to_string''' thy denom) "",
222 Trueprop $ (mk_equality (t, denom)))
223 | eval_get_denominator _ _ _ _ = NONE;
225 text {*\noindent For the tests of \ttfamily eval\_get\_denominator \normalfont
226 see \ttfamily test/Knowledge/rational.sml\normalfont*}
228 text {*\noindent \ttfamily get\_numerator \normalfont should also become a
229 constant for the Isabelle parser, follow up the \texttt{const}
235 * ("Rational.get_numerator", eval_get_numerator ""))
237 fun eval_get_numerator (thmid:string) _
238 (t as Const ("Rational.get_numerator", _) $
239 (Const ("Fields.inverse_class.divide", _) $num
241 SOME (mk_thmid thmid "" (term_to_string''' thy num) "",
242 Trueprop $ (mk_equality (t, num)))
243 | eval_get_numerator _ _ _ _ = NONE;
246 text {*\noindent We discovered several problems by implementing the
247 \ttfamily get\_numerator \normalfont function. Remember when
248 putting new functions to {\sisac}, put them in a thy file and rebuild
249 {\sisac}, also put them in the ruleset for the script!*}
251 subsection {*Solve Equation\label{sec:solveq}*}
252 text {*\noindent We have to find the zeros of the term, therefor we use our
253 \ttfamily get\_denominator \normalfont function from the step before
254 and try to solve the second order equation. (Follow up the Calculation
255 in Section~\ref{sec:calc:ztrans} Subproblem 2) Note: This type of
256 equation is too general for the present program.
257 \par We know that this equation can be categorized as \em univariate
258 equation \normalfont and solved with the functions {\sisac} provides
259 for this equation type. Later on {\sisac} should determine the type
260 of the given equation self.*}
262 val denominator = parseNEW ctxt "z^^^2 - 1/4*z - 1/8 = 0";
263 val fmz = ["equality (z^^^2 - 1/4*z - 1/8 = (0::real))",
266 val (dI',pI',mI') =("Isac", ["univariate","equation"], ["no_met"]);
268 text {*\noindent Check if the given equation matches the specification of this
271 match_pbl fmz (get_pbt ["univariate","equation"]);
274 text{*\noindent We switch up to the {\sisac} Context and try to solve the
275 equation with a more specific type definition.*}
278 Context.theory_name thy = "Isac";
279 val denominator = parseNEW ctxt "-1 + -2 * z + 8 * z ^^^ 2 = 0";
280 val fmz = (*specification*)
281 ["equality (-1 + -2 * z + 8 * z ^^^ 2 = (0::real))",(*equality*)
282 "solveFor z", (*bound variable*)
283 "solutions L"]; (*identifier for
287 ["abcFormula","degree_2","polynomial","univariate","equation"],
291 text {*\noindent Check if the (other) given equation matches the
292 specification of this equation type.*}
295 match_pbl fmz (get_pbt
296 ["abcFormula","degree_2","polynomial","univariate","equation"]);
299 text {*\noindent We stepwise solve the equation. This is done by the
300 use of a so called calc tree seen downwards.*}
303 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
304 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
305 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
306 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
307 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
308 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
309 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
310 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
311 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
312 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
313 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
314 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
315 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
317 * nxt =..,Check_elementwise "Assumptions")
319 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
320 val (p,_,f,nxt,_,pt) = me nxt p [] pt; f2str f;
322 * [z = 1 / 2, z = -1 / 4]
325 val SOME f = parseNEW ctxt "[z=1/2, z=-1/4]";
328 subsection {*Partial Fraction Decomposition\label{sec:pbz}*}
329 text{*\noindent We go on with the decomposition of our expression. Follow up the
330 Calculation in Section~\ref{sec:calc:ztrans} Step~3 and later on
332 subsubsection {*Solutions of the Equation*}
333 text{*\noindent We get the solutions of the before solved equation in a list.*}
336 val SOME solutions = parseNEW ctxt "[z=1/2, z=-1/4]";
341 subsubsection {*Get Solutions out of a List*}
342 text {*\noindent In {\sisac}'s TP-based programming language:
344 let $ $ s_1 = NTH 1 $ solutions; $ s_2 = NTH 2... $
350 val Const ("List.list.Cons", _) $ s_1 $ (Const ("List.list.Cons", _)
351 $ s_2 $ Const ("List.list.Nil", _)) = solutions;
356 text{*\noindent The ansatz for the \em Partial Fraction Decomposition \normalfont
357 requires to get the denominators of the partial fractions out of the
360 \item $Denominator_{1}=z-Zeropoint_{1}$
361 \item $Denominator_{2}=z-Zeropoint_{2}$
367 val xx = HOLogic.dest_eq s_1;
368 val s_1' = HOLogic.mk_binop "Groups.minus_class.minus" xx;
369 val xx = HOLogic.dest_eq s_2;
370 val s_2' = HOLogic.mk_binop "Groups.minus_class.minus" xx;
375 text {*\noindent For the programming language a function collecting all the
376 above manipulations is helpful.*}
380 let val (lhs, rhs) = HOLogic.dest_eq s
381 in HOLogic.mk_binop "Groups.minus_class.minus" (lhs, rhs) end;
385 fun mk_prod prod [] =
387 then error "mk_prod called with []"
389 | mk_prod prod (t :: []) =
392 else HOLogic.mk_binop "Groups.times_class.times" (prod, t)
393 | mk_prod prod (t1 :: t2 :: ts) =
397 HOLogic.mk_binop "Groups.times_class.times" (t1, t2)
401 HOLogic.mk_binop "Groups.times_class.times" (prod, t1)
402 in mk_prod p (t2 :: ts) end
405 probably keep these test in test/Tools/isac/...
406 (*mk_prod e_term [];*)
408 val prod = mk_prod e_term [str2term "x + 123"];
409 term2str prod = "x + 123";
411 val sol = str2term "[z = 1 / 2, z = -1 / 4]";
412 val sols = HOLogic.dest_list sol;
413 val facs = map fac_from_sol sols;
414 val prod = mk_prod e_term facs;
415 term2str prod = "(z + -1 * (1 / 2)) * (z + -1 * (-1 / 4))";
418 mk_prod e_term [str2term "x + 1", str2term "x + 2", str2term "x + 3"];
419 term2str prod = "(x + 1) * (x + 2) * (x + 3)";
422 fun factors_from_solution sol =
423 let val ts = HOLogic.dest_list sol
424 in mk_prod e_term (map fac_from_sol ts) end;
427 val sol = str2term "[z = 1 / 2, z = -1 / 4]";
428 val fs = factors_from_solution sol;
429 term2str fs = "(z + -1 * (1 / 2)) * (z + -1 * (-1 / 4))"
431 text {*\noindent This function needs to be packed such that it can be evaluated
432 by the Lucas-Interpreter. Therefor we moved the function to the
433 corresponding \ttfamily Equation.thy \normalfont in our case
434 \ttfamily PartialFractions.thy \normalfont. The necessary steps
435 are quit the same as we have done with \ttfamily get\_denominator
436 \normalfont before.*}
438 (*("factors_from_solution",
439 ("Partial_Fractions.factors_from_solution",
440 eval_factors_from_solution ""))*)
442 fun eval_factors_from_solution (thmid:string) _
443 (t as Const ("Partial_Fractions.factors_from_solution", _) $ sol)
444 thy = ((let val prod = factors_from_solution sol
445 in SOME (mk_thmid thmid "" (term_to_string''' thy prod) "",
446 Trueprop $ (mk_equality (t, prod)))
449 | eval_factors_from_solution _ _ _ _ = NONE;
452 text {*\noindent The tracing output of the calc tree after applying this
455 24 / factors_from_solution [z = 1/ 2, z = -1 / 4])]
459 val nxt = ("Empty_Tac", ...): tac'_)
461 These observations indicate, that the Lucas-Interpreter (LIP)
462 does not know how to evaluate \ttfamily factors\_from\_solution
463 \normalfont, so we knew that there is something wrong or missing.
466 text{*\noindent First we isolate the difficulty in the program as follows:
468 " (L_L::bool list) = (SubProblem (PolyEq', " ^
469 " [abcFormula, degree_2, polynomial, " ^
470 " univariate,equation], " ^
472 " [BOOL equ, REAL zzz]); " ^
473 " (facs::real) = factors_from_solution L_L; " ^
474 " (foo::real) = Take facs " ^
477 \par \noindent And see the tracing output:
480 [(([], Frm), Problem (Isac, [inverse,
483 (([1], Frm), X z = 3 / (z - 1 / 4 + -1 / 8 * (1 / z))),
484 (([1], Res), ?X' z = 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))),
485 (([2], Res), ?X' z = 24 / (-1 + -2 * z + 8 * z ^^^ 2)),
486 (([3], Pbl), solve (-1 + -2 * z + 8 * z ^^^ 2 = 0, z)),
487 (([3,1], Frm), -1 + -2 * z + 8 * z ^^^ 2 = 0),
488 (([3,1], Res), z = (- -2 + sqrt (-2 ^^^ 2 - 4 * 8 * -1)) / (2 * 8)|
489 z = (- -2 - sqrt (-2 ^^^ 2 - 4 * 8 * -1)) / (2 * 8)),
490 (([3,2], Res), z = 1 / 2 | z = -1 / 4),
491 (([3,3], Res), [ z = 1 / 2, z = -1 / 4]),
492 (([3,4], Res), [ z = 1 / 2, z = -1 / 4]),
493 (([3], Res), [ z = 1 / 2, z = -1 / 4]),
494 (([4], Frm), factors_from_solution [z = 1 / 2, z = -1 / 4])]
497 \par \noindent In particular that:
500 (([3], Pbl), solve (-1 + -2 * z + 8 * z ^^^ 2 = 0, z)),
502 \par \noindent Shows the equation which has been created in
505 "(denom::real) = get_denominator funterm; " ^
506 (* get_denominator *)
507 "(equ::bool) = (denom = (0::real)); " ^
510 \noindent \ttfamily get\_denominator \normalfont has been evaluated successfully,
511 but not\\ \ttfamily factors\_from\_solution.\normalfont
512 So we stepwise compare with an analogous case, \ttfamily get\_denominator
513 \normalfont successfully done above: We know that LIP evaluates
514 expressions in the program by use of the \emph{srls}, so we try to get
515 the original \emph{srls}.\\
518 val {srls,...} = get_met ["SignalProcessing",
523 \par \noindent Create 2 good example terms:
527 parseNEW ctxt "get_denominator ((111::real) / 222)";
529 parseNEW ctxt "factors_from_solution [(z::real)=1/2, z=-1/4]";
532 \par \noindent Rewrite the terms using srls:\\
533 \ttfamily \par \noindent rewrite\_set\_ thy true srls t1;\\
534 rewrite\_set\_ thy true srls t2;\\
535 \par \noindent \normalfont Now we see a difference: \texttt{t1} gives
536 \texttt{SOME} but \texttt{t2} gives \texttt{NONE}. We look at the
540 Rls{id = "srls_InverseZTransform",
541 rules = [Calc("Rational.get_numerator",
542 eval_get_numerator "Rational.get_numerator"),
543 Calc("Partial_Fractions.factors_from_solution",
544 eval_factors_from_solution
545 "Partial_Fractions.factors_from_solution")]}
547 \par \noindent Here everthing is perfect. So the error can
548 only be in the SML code of \ttfamily eval\_factors\_from\_solution.
549 \normalfont We try to check the code with an existing test; since the
551 \begin{center}\ttfamily src/Tools/isac/Knowledge/Partial\_Fractions.thy
552 \normalfont\end{center}
553 the \emph{test} should be in
554 \begin{center}\ttfamily test/Tools/isac/Knowledge/partial\_fractions.sml
555 \normalfont\end{center}
556 \par \noindent After updating the function \ttfamily
557 factors\_from\_solution \normalfont to a new version and putting a
558 test-case to \ttfamily Partial\_Fractions.sml \normalfont we tried again
559 to evaluate the term with the same result.
560 \par We opened the test \ttfamily Test\_Isac.thy \normalfont and saw that
561 everything is working fine. Also we checked that the test \ttfamily
562 partial\_fractions.sml \normalfont is used in \ttfamily Test\_Isac.thy
564 \begin{center}use \ttfamily "Knowledge/partial\_fractions.sml"
565 \normalfont \end{center}
566 and \ttfamily Partial\_Fractions.thy \normalfont is part is part of
567 {\sisac} by evaluating
570 val thy = @{theory "Inverse_Z_Transform"};
573 After rebuilding {\sisac} again it worked.
576 subsubsection {*Build Expression*}
577 text {*\noindent In {\sisac}'s TP-based programming language we can build
579 \ttfamily let s\_1 = Take numerator / (s\_1 * s\_2) \normalfont*}
583 * The main denominator is the multiplication of the denominators of
584 * all partial fractions.
587 val denominator' = HOLogic.mk_binop
588 "Groups.times_class.times" (s_1', s_2') ;
589 val SOME numerator = parseNEW ctxt "3::real";
591 val expr' = HOLogic.mk_binop
592 "Fields.inverse_class.divide" (numerator, denominator');
596 subsubsection {*Apply the Partial Fraction Decomposion Ansatz*}
598 text{*\noindent We use the Ansatz of the Partial Fraction Decomposition for our
599 expression 2nd order. Follow up the calculation in
600 Section~\ref{sec:calc:ztrans} Step~03.*}
602 ML {*Context.theory_name thy = "Isac"*}
604 text{*\noindent We define two axiomatization, the first one is the main ansatz,
605 the next one is just an equivalent transformation of the resulting
606 equation. Both axiomatizations were moved to \ttfamily
607 Partial\_Fractions.thy \normalfont and got their own rulesets. In later
608 programs it is possible to use the rulesets and the machine will find
609 the correct ansatz and equivalent transformation itself.*}
612 ansatz_2nd_order: "n / (a*b) = A/a + B/b" and
613 equival_trans_2nd_order: "(n/(a*b) = A/a + B/b) = (n = A*b + B*a)"
615 text{*\noindent We use our \ttfamily ansatz\_2nd\_order \normalfont to rewrite
616 our expression and get an equation with our expression on the left
617 and the partial fractions of it on the right hand side.*}
621 rewrite_ @{theory} e_rew_ord e_rls false
622 @{thm ansatz_2nd_order} expr';
623 term2str t1; atomty t1;
624 val eq1 = HOLogic.mk_eq (expr', t1);
628 text{*\noindent Eliminate the denominators by multiplying the left and the
629 right hand side of the equation with the main denominator. This is an
630 simple equivalent transformation. Later on we use an own ruleset
631 defined in \ttfamily Partial\_Fractions.thy \normalfont for doing this.
632 Follow up the calculation in Section~\ref{sec:calc:ztrans} Step~04.*}
636 rewrite_ @{theory} e_rew_ord e_rls false
637 @{thm equival_trans_2nd_order} eq1;
641 text{*\noindent We use the existing ruleset \ttfamily norm\_Rational \normalfont
642 for simplifications on expressions.*}
645 val SOME (eq3,_) = rewrite_set_ @{theory} false norm_Rational eq2;
648 * ?A ?B not simplified
652 text{*\noindent In Example~\ref{eg:gap} of my thesis I'm describing a problem about
653 simplifications. The problem that we would like to have only a specific degree
654 of simplification occurs right here, in the next step.*}
657 trace_rewrite := false;
659 parseNEW ctxt "(z - 1/2)*(z - -1/4) * (A/(z - 1/2) + B/(z - -1/4))";
663 val SOME (fract2,_) =
664 rewrite_set_ @{theory} false norm_Rational fract1;
665 term2str fract2 = "(A + -2 * B + 4 * A * z + 4 * B * z) / 4";
667 * term2str fract2 = "A * (1 / 4 + z) + B * (-1 / 2 + z)"
668 * would be more traditional...
672 text{*\noindent We walk around this problem by generating our new equation first.*}
675 val (numerator, denominator) = HOLogic.dest_eq eq3;
676 val eq3' = HOLogic.mk_eq (numerator, fract1);
682 * MANDATORY: simplify (and remove denominator) otherwise 3 = 0
684 val SOME (eq3'' ,_) =
685 rewrite_set_ @{theory} false norm_Rational eq3';
689 text{*\noindent Still working at {\sisac}\ldots*}
691 ML {* Context.theory_name thy = "Isac" *}
693 subsubsection {*Build a Rule-Set for the Ansatz*}
694 text {*\noindent The \emph{ansatz} rules violate the principle that each
695 variable on the right-hand-side must also occur on the
696 left-hand-side of the rule: A, B, etc. don't do that. Thus the
697 rewriter marks these variables with question marks: ?A, ?B, etc.
698 These question marks can be dropped by \ttfamily fun
699 drop\_questionmarks\normalfont.*}
702 val ansatz_rls = prep_rls @{theory} (
703 Rls {id = "ansatz_rls", preconds = [], rew_ord = ("dummy_ord",dummy_ord),
704 erls = e_rls, srls = Erls, calc = [], errpatts = [],
706 Thm ("ansatz_2nd_order",num_str @{thm ansatz_2nd_order}),
707 Thm ("equival_trans_2nd_order",num_str @{thm equival_trans_2nd_order})
712 text{*\noindent We apply the ruleset\ldots*}
716 rewrite_set_ @{theory} false ansatz_rls expr';
719 text{*\noindent And check the output\ldots*}
722 term2str expr' = "3 / ((z - 1 / 2) * (z - -1 / 4))";
723 term2str ttttt = "?A / (z - 1 / 2) + ?B / (z - -1 / 4)";
726 subsubsection {*Get the First Coefficient*}
728 text{*\noindent Now it's up to get the two coefficients A and B, which will be
729 the numerators of our partial fractions. Continue following up the
730 Calculation in Section~\ref{sec:calc:ztrans} Subproblem~1.*}
732 text{*\noindent To get the first coefficient we substitute $z$ with the first
733 zero-point we determined in Section~\ref{sec:solveq}.*}
737 rewrite_terms_ @{theory} e_rew_ord e_rls [s_1] eq3'';
740 rewrite_set_ @{theory} false norm_Rational eq4_1;
743 val fmz = ["equality (3=3*A/(4::real))", "solveFor A","solutions L"];
744 val (dI',pI',mI') =("Isac", ["univariate","equation"], ["no_met"]);
746 * Solve the simple linear equation for A:
747 * Return eq, not list of eq's
749 val (p,_,fa,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
750 val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
751 (*Add_Given "equality (3=3*A/4)"*)
752 val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
753 (*Add_Given "solveFor A"*)
754 val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
755 (*Add_Find "solutions L"*)
756 val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
757 (*Specify_Theory "Isac"*)
758 val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
759 (*Specify_Problem ["normalize","polynomial",
760 "univariate","equation"])*)
761 val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
762 (* Specify_Method["PolyEq","normalize_poly"]*)
763 val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
764 (*Apply_Method["PolyEq","normalize_poly"]*)
765 val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
766 (*Rewrite ("all_left","PolyEq.all_left")*)
767 val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
768 (*Rewrite_Set_Inst(["(bdv,A)"],"make_ratpoly_in")*)
769 val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
770 (*Rewrite_Set "polyeq_simplify"*)
771 val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
772 val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
773 val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
774 (*Add_Given "equality (3 + -3 / 4 * A =0)"*)
775 val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
776 (*Add_Given "solveFor A"*)
777 val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
778 (*Add_Find "solutions A_i"*)
779 val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
780 val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
781 val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
782 val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
783 (*Apply_Method ["PolyEq","solve_d1_polyeq_equation"]*)
784 val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
785 (*Rewrite_Set_Inst(["(bdv,A)"],"d1_polyeq_simplify")*)
786 val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
787 (*Rewrite_Set "polyeq_simplify"*)
788 val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
789 (*Rewrite_Set "norm_Rational_parenthesized"*)
790 val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
792 val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
793 (*Check_elementwise "Assumptions"*)
794 val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
795 (*Check_Postcond ["degree_1","polynomial",
796 "univariate","equation"]*)
797 val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
798 (*Check_Postcond ["normalize","polynomial",
799 "univariate","equation"]*)
800 val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
805 subsubsection {*Get Second Coefficient*}
807 text{*\noindent With the use of \texttt{thy} we check which theories the
812 text{*\noindent To get the second coefficient we substitute $z$ with the second
813 zero-point we determined in Section~\ref{sec:solveq}.*}
816 val SOME (eq4b_1,_) =
817 rewrite_terms_ @{theory} e_rew_ord e_rls [s_2] eq3'';
819 val SOME (eq4b_2,_) =
820 rewrite_set_ @{theory} false norm_Rational eq4b_1;
823 val fmz = ["equality (3= -3*B/(4::real))", "solveFor B","solutions L"];
824 val (dI',pI',mI') =("Isac", ["univariate","equation"], ["no_met"]);
825 val (p,_,fb,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
826 val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
827 val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
828 val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
829 val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
830 val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
831 val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
832 val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
833 val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
834 val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
835 val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
836 val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
837 val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
838 val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
839 val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
840 val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
841 val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
842 val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
843 val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
844 val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
845 val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
846 val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
847 val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
848 val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
849 val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
850 val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
851 val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
852 val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
856 text{*\noindent We compare our results with the pre calculated upshot.*}
859 if f2str fa = "[A = 4]" then () else error "part.fract. eq4_1";
860 if f2str fb = "[B = -4]" then () else error "part.fract. eq4_1";
863 section {*Implement the Specification and the Method \label{spec-meth}*}
865 text{*\noindent Now everything we need for solving the problem has been
866 tested out. We now start by creating new nodes for our methods and
867 further on our new program in the interpreter.*}
869 subsection{*Define the Field Descriptions for the
870 Specification\label{sec:deffdes}*}
872 text{*\noindent We define the fields \em filterExpression \normalfont and
873 \em stepResponse \normalfont both as equations, they represent the in- and
874 output of the program.*}
877 filterExpression :: "bool => una"
878 stepResponse :: "bool => una"
880 subsection{*Define the Specification*}
882 text{*\noindent The next step is defining the specifications as nodes in the
883 designated part. We have to create the hierarchy node by node and start
884 with \em SignalProcessing \normalfont and go on by creating the node
885 \em Z\_Transform\normalfont.*}
887 setup {* KEStore_Elems.add_pbts
888 [prep_pbt thy "pbl_SP" [] e_pblID (["SignalProcessing"], [], e_rls, NONE, []),
889 prep_pbt thy "pbl_SP_Ztrans" [] e_pblID
890 (["Z_Transform","SignalProcessing"], [], e_rls, NONE, [])] *}
892 text{*\noindent For the suddenly created node we have to define the input
893 and output parameters. We already prepared their definition in
894 Section~\ref{sec:deffdes}.*}
896 setup {* KEStore_Elems.add_pbts
897 [prep_pbt thy "pbl_SP_Ztrans_inv" [] e_pblID
898 (["Inverse", "Z_Transform", "SignalProcessing"],
899 [("#Given", ["filterExpression X_eq"]),
900 ("#Find", ["stepResponse n_eq"])],
901 append_rls "e_rls" e_rls [(*for preds in where_*)],
903 [["SignalProcessing","Z_Transform","Inverse"]])] *}
906 get_pbt ["Inverse","Z_Transform","SignalProcessing"];
909 subsection {*Define Name and Signature for the Method*}
911 text{*\noindent As a next step we store the definition of our new method as a
912 constant for the interpreter.*}
915 InverseZTransform :: "[bool, bool] => bool"
916 ("((Script InverseZTransform (_ =))// (_))" 9)
918 subsection {*Setup Parent Nodes in Hierarchy of Method\label{sec:cparentnode}*}
920 text{*\noindent Again we have to generate the nodes step by step, first the
921 parent node and then the originally \em Z\_Transformation
922 \normalfont node. We have to define both nodes first with an empty script
925 setup {* KEStore_Elems.add_mets
926 [prep_met thy "met_SP" [] e_metID
927 (["SignalProcessing"], [],
928 {rew_ord'="tless_true", rls'= e_rls, calc = [], srls = e_rls, prls = e_rls, crls = e_rls,
929 errpats = [], nrls = e_rls},
931 prep_met thy "met_SP_Ztrans" [] e_metID
932 (["SignalProcessing", "Z_Transform"], [],
933 {rew_ord'="tless_true", rls'= e_rls, calc = [], srls = e_rls, prls = e_rls, crls = e_rls,
934 errpats = [], nrls = e_rls},
938 text{*\noindent After we generated both nodes, we can fill the containing
939 script we want to implement later. First we define the specifications
940 of the script in e.g. the in- and output.*}
942 setup {* KEStore_Elems.add_mets
943 [prep_met thy "met_SP_Ztrans_inv" [] e_metID
944 (["SignalProcessing", "Z_Transform", "Inverse"],
945 [("#Given" ,["filterExpression X_eq"]), ("#Find" ,["stepResponse n_eq"])],
946 {rew_ord'="tless_true", rls'= e_rls, calc = [], srls = e_rls, prls = e_rls, crls = e_rls,
947 errpats = [], nrls = e_rls},
951 text{*\noindent After we stored the definition we can start implementing the
952 script itself. As a first try we define only three rows containing one
955 setup {* KEStore_Elems.add_mets
956 [prep_met thy "met_SP_Ztrans_inv" [] e_metID
957 (["SignalProcessing", "Z_Transform", "Inverse"],
958 [("#Given" ,["filterExpression X_eq"]), ("#Find" ,["stepResponse n_eq"])],
959 {rew_ord'="tless_true", rls'= e_rls, calc = [], srls = e_rls, prls = e_rls, crls = e_rls,
960 errpats = [], nrls = e_rls},
961 "Script InverseZTransform (Xeq::bool) =" ^
962 " (let X = Take Xeq;" ^
963 " X = Rewrite ruleZY False X" ^
967 text{*\noindent Check if the method has been stored correctly\ldots*}
973 text{*\noindent If yes we can get the method by stepping backwards through
977 get_met ["SignalProcessing","Z_Transform","Inverse"];
980 section {*Program in TP-based language \label{prog-steps}*}
982 text{*\noindent We start stepwise expanding our program. The script is a
983 simple string containing several manipulation instructions.
984 \par The first script we try contains no instruction, we only test if
985 building scripts that way work.*}
987 subsection {*Stepwise Extend the Program*}
990 "Script InverseZTransform (Xeq::bool) = "^
994 text{*\noindent Next we put some instructions in the script and try if we are
995 able to solve our first equation.*}
999 "Script InverseZTransform (Xeq::bool) = "^
1001 * 1/z) instead of z ^^^ -1
1003 " (let X = Take Xeq; "^
1004 " X' = Rewrite ruleZY False X; "^
1008 " X' = (Rewrite_Set norm_Rational False) X' "^
1016 "Script InverseZTransform (Xeq::bool) = "^
1018 * (1/z) instead of z ^^^ -1
1020 " (let X = Take Xeq; "^
1021 " X' = Rewrite ruleZY False X; "^
1025 " X' = (Rewrite_Set norm_Rational False) X'; "^
1029 " X' = (SubProblem (Isac',[pqFormula,degree_2, "^
1030 " polynomial,univariate,equation], "^
1032 " [BOOL e_e, REAL v_v]) "^
1036 text{*\noindent To solve the equation it is necessary to drop the left hand
1037 side, now we only need the denominator of the right hand side. The first
1038 equation solves the zeros of our expression.*}
1042 "Script InverseZTransform (Xeq::bool) = "^
1043 " (let X = Take Xeq; "^
1044 " X' = Rewrite ruleZY False X; "^
1045 " X' = (Rewrite_Set norm_Rational False) X'; "^
1046 " funterm = rhs X' "^
1048 * drop X'= for equation solving
1053 text{*\noindent As mentioned above, we need the denominator of the right hand
1054 side. The equation itself consists of this denominator and tries to find
1055 a $z$ for this the denominator is equal to zero.*}
1059 "Script InverseZTransform (X_eq::bool) = "^
1060 " (let X = Take X_eq; "^
1061 " X' = Rewrite ruleZY False X; "^
1062 " X' = (Rewrite_Set norm_Rational False) X'; "^
1063 " (X'_z::real) = lhs X'; "^
1064 " (z::real) = argument_in X'_z; "^
1065 " (funterm::real) = rhs X'; "^
1066 " (denom::real) = get_denominator funterm; "^
1070 " (equ::bool) = (denom = (0::real)); "^
1071 " (L_L::bool list) = "^
1072 " (SubProblem (Test', "^
1073 " [LINEAR,univariate,equation,test], "^
1074 " [Test,solve_linear]) "^
1075 " [BOOL equ, REAL z]) "^
1079 val sc = ((inst_abs thy) o Thm.term_of o the o (parse thy)) str;
1083 text {*\noindent This ruleset contains all functions that are in the script;
1084 The evaluation of the functions is done by rewriting using this ruleset.*}
1088 Rls {id="srls_InverseZTransform",
1090 rew_ord = ("termlessI",termlessI),
1091 erls = append_rls "erls_in_srls_InverseZTransform" e_rls
1092 [(*for asm in NTH_CONS ...*)
1093 Calc ("Orderings.ord_class.less",eval_equ "#less_"),
1094 (*2nd NTH_CONS pushes n+-1 into asms*)
1095 Calc("Groups.plus_class.plus", eval_binop "#add_")
1097 srls = Erls, calc = [], errpatts = [],
1099 Thm ("NTH_CONS",num_str @{thm NTH_CONS}),
1100 Calc("Groups.plus_class.plus",
1101 eval_binop "#add_"),
1102 Thm ("NTH_NIL",num_str @{thm NTH_NIL}),
1103 Calc("Tools.lhs", eval_lhs"eval_lhs_"),
1104 Calc("Tools.rhs", eval_rhs"eval_rhs_"),
1105 Calc("Atools.argument'_in",
1106 eval_argument_in "Atools.argument'_in"),
1107 Calc("Rational.get_denominator",
1108 eval_get_denominator "#get_denominator"),
1109 Calc("Rational.get_numerator",
1110 eval_get_numerator "#get_numerator"),
1111 Calc("Partial_Fractions.factors_from_solution",
1112 eval_factors_from_solution
1113 "#factors_from_solution"),
1114 Calc("Partial_Fractions.drop_questionmarks",
1115 eval_drop_questionmarks "#drop_?")
1121 subsection {*Store Final Version of Program for Execution*}
1123 text{*\noindent After we also tested how to write scripts and run them,
1124 we start creating the final version of our script and store it into
1125 the method for which we created a node in Section~\ref{sec:cparentnode}
1126 Note that we also did this stepwise, but we didn't kept every
1129 setup {* KEStore_Elems.add_mets
1130 [prep_met thy "met_SP_Ztrans_inv" [] e_metID
1131 (["SignalProcessing", "Z_Transform", "Inverse"],
1132 [("#Given" ,["filterExpression X_eq"]), ("#Find" ,["stepResponse n_eq"])],
1133 {rew_ord'="tless_true", rls'= e_rls, calc = [], srls = srls, prls = e_rls, crls = e_rls,
1134 errpats = [], nrls = e_rls},
1135 "Script InverseZTransform (X_eq::bool) = "^
1136 (*(1/z) instead of z ^^^ -1*)
1137 "(let X = Take X_eq; "^
1138 " X' = Rewrite ruleZY False X; "^
1140 " (num_orig::real) = get_numerator (rhs X'); "^
1141 " X' = (Rewrite_Set norm_Rational False) X'; "^
1143 " (X'_z::real) = lhs X'; "^
1144 " (zzz::real) = argument_in X'_z; "^
1145 " (funterm::real) = rhs X'; "^
1146 (*drop X' z = for equation solving*)
1147 " (denom::real) = get_denominator funterm; "^
1149 " (num::real) = get_numerator funterm; "^
1151 " (equ::bool) = (denom = (0::real)); "^
1152 " (L_L::bool list) = (SubProblem (PolyEq', "^
1153 " [abcFormula,degree_2,polynomial,univariate,equation], "^
1155 " [BOOL equ, REAL zzz]); "^
1156 " (facs::real) = factors_from_solution L_L; "^
1157 " (eql::real) = Take (num_orig / facs); "^
1159 " (eqr::real) = (Try (Rewrite_Set ansatz_rls False)) eql; "^
1161 " (eq::bool) = Take (eql = eqr); "^
1162 (*Maybe possible to use HOLogic.mk_eq ??*)
1163 " eq = (Try (Rewrite_Set equival_trans False)) eq; "^
1165 " eq = drop_questionmarks eq; "^
1166 " (z1::real) = (rhs (NTH 1 L_L)); "^
1168 * prepare equation for a - eq_a
1169 * therefor substitute z with solution 1 - z1
1171 " (z2::real) = (rhs (NTH 2 L_L)); "^
1173 " (eq_a::bool) = Take eq; "^
1174 " eq_a = (Substitute [zzz=z1]) eq; "^
1175 " eq_a = (Rewrite_Set norm_Rational False) eq_a; "^
1176 " (sol_a::bool list) = "^
1177 " (SubProblem (Isac', "^
1178 " [univariate,equation],[no_met]) "^
1179 " [BOOL eq_a, REAL (A::real)]); "^
1180 " (a::real) = (rhs(NTH 1 sol_a)); "^
1182 " (eq_b::bool) = Take eq; "^
1183 " eq_b = (Substitute [zzz=z2]) eq_b; "^
1184 " eq_b = (Rewrite_Set norm_Rational False) eq_b; "^
1185 " (sol_b::bool list) = "^
1186 " (SubProblem (Isac', "^
1187 " [univariate,equation],[no_met]) "^
1188 " [BOOL eq_b, REAL (B::real)]); "^
1189 " (b::real) = (rhs(NTH 1 sol_b)); "^
1191 " eqr = drop_questionmarks eqr; "^
1192 " (pbz::real) = Take eqr; "^
1193 " pbz = ((Substitute [A=a, B=b]) pbz); "^
1195 " pbz = Rewrite ruleYZ False pbz; "^
1196 " pbz = drop_questionmarks pbz; "^
1198 " (X_z::bool) = Take (X_z = pbz); "^
1199 " (n_eq::bool) = (Rewrite_Set inverse_z False) X_z; "^
1200 " n_eq = drop_questionmarks n_eq "^
1205 subsection {*Check the Program*}
1206 text{*\noindent When the script is ready we can start checking our work.*}
1207 subsubsection {*Check the Formalization*}
1208 text{*\noindent First we want to check the formalization of the in and
1209 output of our program.*}
1213 ["filterExpression (X = 3 / (z - 1/4 + -1/8 * (1/(z::real))))",
1214 "stepResponse (x[n::real]::bool)"];
1216 ("Isac", ["Inverse", "Z_Transform", "SignalProcessing"],
1217 ["SignalProcessing","Z_Transform","Inverse"]);
1224 Const ("Inverse_Z_Transform.filterExpression", _),
1225 [Const ("HOL.eq", _) $ _ $ _]
1231 Const ("Inverse_Z_Transform.stepResponse", _),
1235 ) = prep_ori fmz thy ((#ppc o get_pbt) pI);
1238 = (#scr o get_met) ["SignalProcessing",
1244 subsubsection {*Stepwise Check the Program\label{sec:stepcheck}*}
1245 text{*\noindent We start to stepwise execute our new program in a calculation
1246 tree and check if every node implements that what we have wanted.*}
1249 trace_rewrite := false; (*true*)
1250 trace_script := false; (*true*)
1254 ["filterExpression (X z = 3 / ((z::real) + 1/10 - 1/50*(1/z)))",
1255 "stepResponse (x[n::real]::bool)"];
1258 ("Isac", ["Inverse", "Z_Transform", "SignalProcessing"],
1259 ["SignalProcessing","Z_Transform","Inverse"]);
1261 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI,pI,mI))];
1262 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1264 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1266 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1268 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1270 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1272 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1274 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1275 "Rewrite (ruleZY, Inverse_Z_Transform.ruleZY)";
1276 "--> X z = 3 / (z - 1 / 4 + -1 / 8 * (1 / z))";
1280 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1281 "Rewrite_Set norm_Rational";
1282 " --> X' z = 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))";
1283 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1288 text {*\noindent Instead of \ttfamily nxt = Subproblem \normalfont above we had
1289 \ttfamily Empty\_Tac; \normalfont the search for the reason considered
1290 the following points:\begin{itemize}
1291 \item What shows \ttfamily show\_pt pt;\normalfont\ldots?
1292 \begin{verbatim}(([2], Res), ?X' z = 24 / (-1 + -2 * z + 8 * z ^^^ 2))]\end{verbatim}
1293 The calculation is ok but no \ttfamily next \normalfont step found:
1294 Should be\\ \ttfamily nxt = Subproblem\normalfont!
1295 \item What shows \ttfamily trace\_script := true; \normalfont we read
1298 @@@next leaf 'SubProblem
1299 (PolyEq',[abcFormula, degree_2, polynomial,
1300 univariate, equation], no_meth)
1302 ---> STac 'SubProblem (PolyEq',
1303 [abcFormula, degree_2, polynomial,
1304 univariate, equation], no_meth)
1305 [BOOL (-1 + -2 * z + 8 * z \^\^\^ ~2 = 0), REAL z]'
1307 We see the SubProblem with correct arguments from searching next
1308 step (program text !!!--->!!! STac (script tactic) with arguments
1310 \item Do we have the right Script \ldots difference in the
1311 arguments in the arguments\ldots
1314 (#scr o get_met) ["SignalProcessing",
1317 writeln (term2str s);
1319 \ldots shows the right script. Difference in the arguments.
1320 \item Test --- Why helpless here ? --- shows: \ttfamily replace
1321 no\_meth by [no\_meth] \normalfont in Script
1326 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1330 text {*\noindent Instead of \ttfamily nxt = Model\_Problem \normalfont above
1331 we had \ttfamily Empty\_Tac; \normalfont the search for the reason
1332 considered the following points:\begin{itemize}
1333 \item Difference in the arguments
1334 \item Comparison with Subsection~\ref{sec:solveq}: There solving this
1335 equation works, so there must be some difference in the arguments
1336 of the Subproblem: RIGHT: we had \ttfamily [no\_meth] \normalfont
1337 instead of \ttfamily [no\_met] \normalfont ;-)
1341 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1342 (*Add_Given equality (-1 + -2 * z + 8 * z ^^^ 2 = 0)";*)
1343 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1344 (*Add_Given solveFor z";*)
1345 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1346 (*Add_Find solutions z_i";*)
1347 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1348 (*Specify_Theory Isac";*)
1351 text {*\noindent We had \ttfamily nxt = Empty\_Tac instead Specify\_Theory;
1352 \normalfont The search for the reason considered the following points:
1354 \item Was there an error message? NO -- ok
1355 \item Has \ttfamily nxt = Add\_Find \normalfont been inserted in pt:\\
1356 \ttfamily get\_obj g\_pbl pt (fst p);\normalfont? YES -- ok
1357 \item What is the returned formula:
1359 print_depth 999; f; print_depth 3;
1360 { Find = [ Correct "solutions z_i"],
1362 Given = [Correct "equality (-1 + -2*z + 8*z ^^^ 2 = 0)",
1363 Correct "solveFor z"],
1367 \normalfont The only False is the reason: the Where (the precondition) is
1368 False for good reasons: The precondition seems to check for linear
1369 equations, not for the one we want to solve! Removed this error by
1370 correcting the Script from \ttfamily SubProblem (PolyEq',
1371 \lbrack linear,univariate,equation,
1372 test\rbrack, \lbrack Test,solve\_linear\rbrack \normalfont to
1373 \ttfamily SubProblem (PolyEq',\\ \lbrack abcFormula,degree\_2,
1374 polynomial,univariate,equation\rbrack,\\
1375 \lbrack PolyEq,solve\_d2\_polyeq\_abc\_equation
1377 You find the appropriate type of equation at the
1378 {\sisac}-WEB-Page\footnote{
1379 \href{http://www.ist.tugraz.at/projects/isac/www/kbase/pbl/index\_pbl.html}
1380 {http://www.ist.tugraz.at/projects/isac/www/kbase/pbl/index\_pbl.html}
1382 And the respective method in \ttfamily Knowledge/PolyEq.thy \normalfont
1383 at the respective \ttfamily store\_pbt. \normalfont Or you leave the
1384 selection of the appropriate type to isac as done in the final Script ;-))
1388 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1389 (*Specify_Problem [abcFormula,...";*)
1390 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1391 (*Specify_Method [PolyEq,solve_d2_polyeq_abc_equation";*)
1392 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1393 (*Apply_Method [PolyEq,solve_d2_polyeq_abc_equation";*)
1394 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1395 (*Rewrite_Set_Inst ([(bdv, z)], d2_polyeq_abcFormula_simplify";*)
1396 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1397 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1398 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1399 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1400 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1401 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1402 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1403 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1404 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1405 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1406 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1407 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1408 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1409 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1410 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1411 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1412 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1413 (*Specify_Problem ["normalize","polynomial","univariate","equation"]*)
1414 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1415 (*Specify_Method ["PolyEq", "normalize_poly"]*)
1416 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1417 (*Apply_Method ["PolyEq", "normalize_poly"]*)
1418 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1419 (*Rewrite ("all_left", "PolyEq.all_left")*)
1420 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1421 (*Rewrite_Set_Inst (["(bdv, A)"], "make_ratpoly_in")*)
1422 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1423 (*Rewrite_Set "polyeq_simplify"*)
1424 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1425 (*Subproblem("Isac",["degree_1","polynomial","univariate","equation"])*)
1426 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1427 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1428 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1429 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1430 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1431 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1432 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1433 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1434 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1435 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1436 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1437 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1438 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1439 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1440 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1441 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1442 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1443 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1444 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1445 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1446 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1447 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1448 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1449 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1450 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1451 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1452 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1453 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1454 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1455 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1456 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1457 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1458 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1459 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1460 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1461 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1462 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1463 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1464 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1465 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1466 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1467 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1468 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1469 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1470 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1471 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*([11, 4, 5], Res) Check_Postcond*)
1472 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*([11, 4], Res) Check_Postcond*)
1473 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*([11], Res) Take*)
1474 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*([12], Frm) Substitute*)
1475 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*([12], Res) Rewrite*)
1476 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*([13], Res) Take*)
1477 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*([14], Frm) Empty_Tac*)
1480 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1483 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1486 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1489 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1492 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1495 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1499 trace_script := true;
1502 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1520 text{*\noindent As a last step we check the tracing output of the last calc
1521 tree instruction and compare it with the pre-calculated result.*}
1523 section {* Improve and Transfer into Knowledge *}
1525 We want to improve the very long program \ttfamily InverseZTransform
1526 \normalfont by modularisation: partial fraction decomposition shall
1527 become a sub-problem.
1529 We could transfer all knowledge in \ttfamily Build\_Inverse\_Z\_Transform.thy
1530 \normalfont first to the \ttfamily Knowledge/Inverse\_Z\_Transform.thy
1531 \normalfont and then modularise. In this case TODO problems?!?
1533 We chose another way and go bottom up: first we build the sub-problem in
1534 \ttfamily Partial\_Fractions.thy \normalfont with the term:
1536 $$\frac{3}{x\cdot(z - \frac{1}{4} + \frac{-1}{8}\cdot\frac{1}{z})}$$
1538 \noindent (how this still can be improved see \ttfamily Partial\_Fractions.thy\normalfont),
1539 and re-use all stuff prepared in \ttfamily Build\_Inverse\_Z\_Transform.thy:
1540 \normalfont The knowledge will be transferred to \ttfamily src/../Partial\_Fractions.thy
1541 \normalfont and the respective tests to:
1542 \begin{center}\ttfamily test/../sartial\_fractions.sml\normalfont\end{center}
1545 subsection {* Transfer to Partial\_Fractions.thy *}
1547 First we transfer both, knowledge and tests into:
1548 \begin{center}\ttfamily src/../Partial\_Fractions.thy\normalfont\end{center}
1549 in order to immediately have the test results.
1551 We copy \ttfamily factors\_from\_solution, drop\_questionmarks,\\
1552 ansatz\_2nd\_order \normalfont and rule-sets --- no problem.
1554 Also \ttfamily store\_pbt ..\\ "pbl\_simp\_rat\_partfrac"
1555 \normalfont is easy.
1557 But then we copy from:\\
1558 (1) \ttfamily Build\_Inverse\_Z\_Transform.thy store\_met\ldots "met\_SP\_Ztrans\_inv"
1560 (2) \ttfamily Partial\_Fractions.thy store\_met\ldots "met\_SP\_Ztrans\_inv"
1561 \normalfont\\ and cut out the respective part from the program. First we ensure that
1562 the string is correct. When we insert the string into (2)
1563 \ttfamily store\_met .. "met\_partial\_fraction" \normalfont --- and get an error.
1566 subsubsection {* 'Programming' in ISAC's TP-based Language *}
1568 At the present state writing programs in {\sisac} is particularly cumbersome.
1569 So we give hints how to cope with the many obstacles. Below we describe the
1570 steps we did in making (2) run.
1573 \item We check if the \textbf{string} containing the program is correct.
1574 \item We check if the \textbf{types in the program} are correct.
1575 For this purpose we start start with the first and last lines
1577 "PartFracScript (f_f::real) (v_v::real) = " ^
1578 " (let X = Take f_f; " ^
1579 " pbz = ((Substitute []) X) " ^
1582 The last but one line helps not to bother with ';'.
1583 \item Then we add line by line. Already the first line causes the error.
1584 So we investigate it by
1586 val ctxt = Proof_Context.init_global @{theory "Inverse_Z_Transform"} ;
1588 parseNEW ctxt "(num_orig::real) =
1589 get_numerator(rhs f_f)";
1591 and see a type clash: \ttfamily rhs \normalfont from (1) requires type
1592 \ttfamily bool \normalfont while (2) wants to have \ttfamily (f\_f::real).
1593 \normalfont Of course, we don't need \ttfamily rhs \normalfont anymore.
1594 \item Type-checking can be very tedious. One might even inspect the
1595 parse-tree of the program with {\sisac}'s specific debug tools:
1597 val {scr = Prog t,...} =
1598 get_met ["simplification",
1600 "to_partial_fraction"];
1601 atomty_thy @{theory "Inverse_Z_Transform"} t ;
1603 \item We check if the \textbf{semantics of the program} by stepwise evaluation
1604 of the program. Evaluation is done by the Lucas-Interpreter, which works
1605 using the knowledge in theory Isac; so we have to re-build Isac. And the
1606 test are performed simplest in a file which is loaded with Isac.
1607 See \ttfamily tests/../partial\_fractions.sml \normalfont.
1611 subsection {* Transfer to Inverse\_Z\_Transform.thy *}
1613 It was not possible to complete this task, because we ran out of time.