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 Isac
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 Isac};*}
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]"};Isac
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 Isac}, 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 = ProofContext.init_global @{theory Isac};
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 Isac}, 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 Isac} false norm_Rational fun2;
160 * We solve this problem by using 1/x as a workaround.
163 rewrite_set_ @{theory Isac} 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 "Rings.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 ("Rings.inverse_class.divide", _) $num
221 SOME (mk_thmid thmid ""
223 (Syntax.string_of_term (thy2ctxt thy)) denom) "",
224 Trueprop $ (mk_equality (t, denom)))
225 | eval_get_denominator _ _ _ _ = NONE;
227 text {*\noindent For the tests of \ttfamily eval\_get\_denominator \normalfont
228 see \ttfamily test/Knowledge/rational.sml\normalfont*}
230 text {*\noindent \ttfamily get\_numerator \normalfont should also become a
231 constant for the Isabelle parser, follow up the \texttt{const}
237 * ("Rational.get_numerator", eval_get_numerator ""))
239 fun eval_get_numerator (thmid:string) _
240 (t as Const ("Rational.get_numerator", _) $
241 (Const ("Rings.inverse_class.divide", _) $num
243 SOME (mk_thmid thmid ""
245 (Syntax.string_of_term (thy2ctxt thy)) num) "",
246 Trueprop $ (mk_equality (t, num)))
247 | eval_get_numerator _ _ _ _ = NONE;
250 text {*\noindent We discovered several problems by implementing the
251 \ttfamily get\_numerator \normalfont function. Remember when
252 putting new functions to {\sisac}, put them in a thy file and rebuild
253 {\sisac}, also put them in the ruleset for the script!*}
255 subsection {*Solve Equation\label{sec:solveq}*}
256 text {*\noindent We have to find the zeros of the term, therefor we use our
257 \ttfamily get\_denominator \normalfont function from the step before
258 and try to solve the second order equation. (Follow up the Calculation
259 in Section~\ref{sec:calc:ztrans} Subproblem 2) Note: This type of
260 equation is too general for the present program.
261 \par We know that this equation can be categorized as \em univariate
262 equation \normalfont and solved with the functions {\sisac} provides
263 for this equation type. Later on {\sisac} should determine the type
264 of the given equation self.*}
266 val denominator = parseNEW ctxt "z^^^2 - 1/4*z - 1/8 = 0";
267 val fmz = ["equality (z^^^2 - 1/4*z - 1/8 = (0::real))",
270 val (dI',pI',mI') =("Isac", ["univariate","equation"], ["no_met"]);
272 text {*\noindent Check if the given equation matches the specification of this
275 match_pbl fmz (get_pbt ["univariate","equation"]);
278 text{*\noindent We switch up to the {\sisac} Context and try to solve the
279 equation with a more specific type definition.*}
282 Context.theory_name thy = "Isac";
283 val denominator = parseNEW ctxt "-1 + -2 * z + 8 * z ^^^ 2 = 0";
284 val fmz = (*specification*)
285 ["equality (-1 + -2 * z + 8 * z ^^^ 2 = (0::real))",(*equality*)
286 "solveFor z", (*bound variable*)
287 "solutions L"]; (*identifier for
291 ["abcFormula","degree_2","polynomial","univariate","equation"],
295 text {*\noindent Check if the (other) given equation matches the
296 specification of this equation type.*}
299 match_pbl fmz (get_pbt
300 ["abcFormula","degree_2","polynomial","univariate","equation"]);
303 text {*\noindent We stepwise solve the equation. This is done by the
304 use of a so called calc tree seen downwards.*}
307 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
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;
316 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
317 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
318 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
319 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
321 * nxt =..,Check_elementwise "Assumptions")
323 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
324 val (p,_,f,nxt,_,pt) = me nxt p [] pt; f2str f;
326 * [z = 1 / 2, z = -1 / 4]
329 val SOME f = parseNEW ctxt "[z=1/2, z=-1/4]";
332 subsection {*Partial Fraction Decomposition\label{sec:pbz}*}
333 text{*\noindent We go on with the decomposition of our expression. Follow up the
334 Calculation in Section~\ref{sec:calc:ztrans} Step~3 and later on
336 subsubsection {*Solutions of the Equation*}
337 text{*\noindent We get the solutions of the before solved equation in a list.*}
340 val SOME solutions = parseNEW ctxt "[z=1/2, z=-1/4]";
345 subsubsection {*Get Solutions out of a List*}
346 text {*\noindent In {\sisac}'s TP-based programming language:
348 let $ $ s_1 = NTH 1 $ solutions; $ s_2 = NTH 2... $
354 val Const ("List.list.Cons", _) $ s_1 $ (Const ("List.list.Cons", _)
355 $ s_2 $ Const ("List.list.Nil", _)) = solutions;
360 text{*\noindent The ansatz for the \em Partial Fraction Decomposition \normalfont
361 requires to get the denominators of the partial fractions out of the
364 \item $Denominator_{1}=z-Zeropoint_{1}$
365 \item $Denominator_{2}=z-Zeropoint_{2}$
371 val xx = HOLogic.dest_eq s_1;
372 val s_1' = HOLogic.mk_binop "Groups.minus_class.minus" xx;
373 val xx = HOLogic.dest_eq s_2;
374 val s_2' = HOLogic.mk_binop "Groups.minus_class.minus" xx;
379 text {*\noindent For the programming language a function collecting all the
380 above manipulations is helpful.*}
384 let val (lhs, rhs) = HOLogic.dest_eq s
385 in HOLogic.mk_binop "Groups.minus_class.minus" (lhs, rhs) end;
389 fun mk_prod prod [] =
391 then error "mk_prod called with []"
393 | mk_prod prod (t :: []) =
396 else HOLogic.mk_binop "Groups.times_class.times" (prod, t)
397 | mk_prod prod (t1 :: t2 :: ts) =
401 HOLogic.mk_binop "Groups.times_class.times" (t1, t2)
405 HOLogic.mk_binop "Groups.times_class.times" (prod, t1)
406 in mk_prod p (t2 :: ts) end
409 probably keep these test in test/Tools/isac/...
410 (*mk_prod e_term [];*)
412 val prod = mk_prod e_term [str2term "x + 123"];
413 term2str prod = "x + 123";
415 val sol = str2term "[z = 1 / 2, z = -1 / 4]";
416 val sols = HOLogic.dest_list sol;
417 val facs = map fac_from_sol sols;
418 val prod = mk_prod e_term facs;
419 term2str prod = "(z + -1 * (1 / 2)) * (z + -1 * (-1 / 4))";
422 mk_prod e_term [str2term "x + 1", str2term "x + 2", str2term "x + 3"];
423 term2str prod = "(x + 1) * (x + 2) * (x + 3)";
426 fun factors_from_solution sol =
427 let val ts = HOLogic.dest_list sol
428 in mk_prod e_term (map fac_from_sol ts) end;
431 val sol = str2term "[z = 1 / 2, z = -1 / 4]";
432 val fs = factors_from_solution sol;
433 term2str fs = "(z + -1 * (1 / 2)) * (z + -1 * (-1 / 4))"
435 text {*\noindent This function needs to be packed such that it can be evaluated
436 by the Lucas-Interpreter. Therefor we moved the function to the
437 corresponding \ttfamily Equation.thy \normalfont in our case
438 \ttfamily PartialFractions.thy \normalfont. The necessary steps
439 are quit the same as we have done with \ttfamily get\_denominator
440 \normalfont before.*}
442 (*("factors_from_solution",
443 ("Partial_Fractions.factors_from_solution",
444 eval_factors_from_solution ""))*)
446 fun eval_factors_from_solution (thmid:string) _
447 (t as Const ("Partial_Fractions.factors_from_solution", _) $ sol)
448 thy = ((let val prod = factors_from_solution sol
449 in SOME (mk_thmid thmid ""
451 (Syntax.string_of_term (thy2ctxt thy)) prod) "",
452 Trueprop $ (mk_equality (t, prod)))
455 | eval_factors_from_solution _ _ _ _ = NONE;
458 text {*\noindent The tracing output of the calc tree after applying this
461 24 / factors_from_solution [z = 1/ 2, z = -1 / 4])]
465 val nxt = ("Empty_Tac", ...): tac'_)
467 These observations indicate, that the Lucas-Interpreter (LIP)
468 does not know how to evaluate \ttfamily factors\_from\_solution
469 \normalfont, so we knew that there is something wrong or missing.
472 text{*\noindent First we isolate the difficulty in the program as follows:
474 " (L_L::bool list) = (SubProblem (PolyEq', " ^
475 " [abcFormula, degree_2, polynomial, " ^
476 " univariate,equation], " ^
478 " [BOOL equ, REAL zzz]); " ^
479 " (facs::real) = factors_from_solution L_L; " ^
480 " (foo::real) = Take facs " ^
483 \par \noindent And see the tracing output:
486 [(([], Frm), Problem (Isac, [inverse,
489 (([1], Frm), X z = 3 / (z - 1 / 4 + -1 / 8 * (1 / z))),
490 (([1], Res), ?X' z = 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))),
491 (([2], Res), ?X' z = 24 / (-1 + -2 * z + 8 * z ^^^ 2)),
492 (([3], Pbl), solve (-1 + -2 * z + 8 * z ^^^ 2 = 0, z)),
493 (([3,1], Frm), -1 + -2 * z + 8 * z ^^^ 2 = 0),
494 (([3,1], Res), z = (- -2 + sqrt (-2 ^^^ 2 - 4 * 8 * -1)) / (2 * 8)|
495 z = (- -2 - sqrt (-2 ^^^ 2 - 4 * 8 * -1)) / (2 * 8)),
496 (([3,2], Res), z = 1 / 2 | z = -1 / 4),
497 (([3,3], Res), [ z = 1 / 2, z = -1 / 4]),
498 (([3,4], Res), [ z = 1 / 2, z = -1 / 4]),
499 (([3], Res), [ z = 1 / 2, z = -1 / 4]),
500 (([4], Frm), factors_from_solution [z = 1 / 2, z = -1 / 4])]
503 \par \noindent In particular that:
506 (([3], Pbl), solve (-1 + -2 * z + 8 * z ^^^ 2 = 0, z)),
508 \par \noindent Shows the equation which has been created in
511 "(denom::real) = get_denominator funterm; " ^
512 (* get_denominator *)
513 "(equ::bool) = (denom = (0::real)); " ^
516 \noindent \ttfamily get\_denominator \normalfont has been evaluated successfully,
517 but not\\ \ttfamily factors\_from\_solution.\normalfont
518 So we stepwise compare with an analogous case, \ttfamily get\_denominator
519 \normalfont successfully done above: We know that LIP evaluates
520 expressions in the program by use of the \emph{srls}, so we try to get
521 the original \emph{srls}.\\
524 val {srls,...} = get_met ["SignalProcessing",
529 \par \noindent Create 2 good example terms:
533 parseNEW ctxt "get_denominator ((111::real) / 222)";
535 parseNEW ctxt "factors_from_solution [(z::real)=1/2, z=-1/4]";
538 \par \noindent Rewrite the terms using srls:\\
539 \ttfamily \par \noindent rewrite\_set\_ thy true srls t1;\\
540 rewrite\_set\_ thy true srls t2;\\
541 \par \noindent \normalfont Now we see a difference: \texttt{t1} gives
542 \texttt{SOME} but \texttt{t2} gives \texttt{NONE}. We look at the
546 Rls{id = "srls_InverseZTransform",
547 rules = [Calc("Rational.get_numerator",
548 eval_get_numerator "Rational.get_numerator"),
549 Calc("Partial_Fractions.factors_from_solution",
550 eval_factors_from_solution
551 "Partial_Fractions.factors_from_solution")]}
553 \par \noindent Here everthing is perfect. So the error can
554 only be in the SML code of \ttfamily eval\_factors\_from\_solution.
555 \normalfont We try to check the code with an existing test; since the
557 \begin{center}\ttfamily src/Tools/isac/Knowledge/Partial\_Fractions.thy
558 \normalfont\end{center}
559 the \emph{test} should be in
560 \begin{center}\ttfamily test/Tools/isac/Knowledge/partial\_fractions.sml
561 \normalfont\end{center}
562 \par \noindent After updating the function \ttfamily
563 factors\_from\_solution \normalfont to a new version and putting a
564 test-case to \ttfamily Partial\_Fractions.sml \normalfont we tried again
565 to evaluate the term with the same result.
566 \par We opened the test \ttfamily Test\_Isac.thy \normalfont and saw that
567 everything is working fine. Also we checked that the test \ttfamily
568 partial\_fractions.sml \normalfont is used in \ttfamily Test\_Isac.thy
570 \begin{center}use \ttfamily "Knowledge/partial\_fractions.sml"
571 \normalfont \end{center}
572 and \ttfamily Partial\_Fractions.thy \normalfont is part is part of
573 {\sisac} by evaluating
576 val thy = @{theory Isac};
579 After rebuilding {\sisac} again it worked.
582 subsubsection {*Build Expression*}
583 text {*\noindent In {\sisac}'s TP-based programming language we can build
585 \ttfamily let s\_1 = Take numerator / (s\_1 * s\_2) \normalfont*}
589 * The main denominator is the multiplication of the denominators of
590 * all partial fractions.
593 val denominator' = HOLogic.mk_binop
594 "Groups.times_class.times" (s_1', s_2') ;
595 val SOME numerator = parseNEW ctxt "3::real";
597 val expr' = HOLogic.mk_binop
598 "Rings.inverse_class.divide" (numerator, denominator');
602 subsubsection {*Apply the Partial Fraction Decomposion Ansatz*}
604 text{*\noindent We use the Ansatz of the Partial Fraction Decomposition for our
605 expression 2nd order. Follow up the calculation in
606 Section~\ref{sec:calc:ztrans} Step~03.*}
608 ML {*Context.theory_name thy = "Isac"*}
610 text{*\noindent We define two axiomatization, the first one is the main ansatz,
611 the next one is just an equivalent transformation of the resulting
612 equation. Both axiomatizations were moved to \ttfamily
613 Partial\_Fractions.thy \normalfont and got their own rulesets. In later
614 programs it is possible to use the rulesets and the machine will find
615 the correct ansatz and equivalent transformation itself.*}
618 ansatz_2nd_order: "n / (a*b) = A/a + B/b" and
619 equival_trans_2nd_order: "(n/(a*b) = A/a + B/b) = (n = A*b + B*a)"
621 text{*\noindent We use our \ttfamily ansatz\_2nd\_order \normalfont to rewrite
622 our expression and get an equation with our expression on the left
623 and the partial fractions of it on the right hand side.*}
627 rewrite_ @{theory Isac} e_rew_ord e_rls false
628 @{thm ansatz_2nd_order} expr';
629 term2str t1; atomty t1;
630 val eq1 = HOLogic.mk_eq (expr', t1);
634 text{*\noindent Eliminate the denominators by multiplying the left and the
635 right hand side of the equation with the main denominator. This is an
636 simple equivalent transformation. Later on we use an own ruleset
637 defined in \ttfamily Partial\_Fractions.thy \normalfont for doing this.
638 Follow up the calculation in Section~\ref{sec:calc:ztrans} Step~04.*}
642 rewrite_ @{theory Isac} e_rew_ord e_rls false
643 @{thm equival_trans_2nd_order} eq1;
647 text{*\noindent We use the existing ruleset \ttfamily norm\_Rational \normalfont
648 for simplifications on expressions.*}
651 val SOME (eq3,_) = rewrite_set_ @{theory Isac} false norm_Rational eq2;
654 * ?A ?B not simplified
658 text{*\noindent In Example~\ref{eg:gap} of my thesis I'm describing a problem about
659 simplifications. The problem that we would like to have only a specific degree
660 of simplification occurs right here, in the next step.*}
664 parseNEW ctxt "(z - 1/2)*(z - -1/4) * (A/(z - 1/2) + B/(z - -1/4))";
668 val SOME (fract2,_) =
669 rewrite_set_ @{theory Isac} false norm_Rational fract1;
670 term2str fract2 = "(A + -2 * B + 4 * A * z + 4 * B * z) / 4";
672 * term2str fract2 = "A * (1 / 4 + z) + B * (-1 / 2 + z)"
673 * would be more traditional...
677 text{*\noindent We walk around this problem by generating our new equation first.*}
680 val (numerator, denominator) = HOLogic.dest_eq eq3;
681 val eq3' = HOLogic.mk_eq (numerator, fract1);
687 * MANDATORY: simplify (and remove denominator) otherwise 3 = 0
689 val SOME (eq3'' ,_) =
690 rewrite_set_ @{theory Isac} false norm_Rational eq3';
694 text{*\noindent Still working at {\sisac}\ldots*}
696 ML {* Context.theory_name thy = "Isac" *}
698 subsubsection {*Build a Rule-Set for the Ansatz*}
699 text {*\noindent The \emph{ansatz} rules violate the principle that each
700 variable on the right-hand-side must also occur on the
701 left-hand-side of the rule: A, B, etc. don't do that. Thus the
702 rewriter marks these variables with question marks: ?A, ?B, etc.
703 These question marks can be dropped by \ttfamily fun
704 drop\_questionmarks\normalfont.*}
707 val ansatz_rls = prep_rls(
708 Rls {id = "ansatz_rls", preconds = [], rew_ord = ("dummy_ord",dummy_ord),
709 erls = e_rls, srls = Erls, calc = [],
711 Thm ("ansatz_2nd_order",num_str @{thm ansatz_2nd_order}),
712 Thm ("equival_trans_2nd_order",num_str @{thm equival_trans_2nd_order})
717 text{*\noindent We apply the ruleset\ldots*}
721 rewrite_set_ @{theory Isac} false ansatz_rls expr';
724 text{*\noindent And check the output\ldots*}
727 term2str expr' = "3 / ((z - 1 / 2) * (z - -1 / 4))";
728 term2str ttttt = "?A / (z - 1 / 2) + ?B / (z - -1 / 4)";
731 subsubsection {*Get the First Coefficient*}
733 text{*\noindent Now it's up to get the two coefficients A and B, which will be
734 the numerators of our partial fractions. Continue following up the
735 Calculation in Section~\ref{sec:calc:ztrans} Subproblem~1.*}
737 text{*\noindent To get the first coefficient we substitute $z$ with the first
738 zero-point we determined in Section~\ref{sec:solveq}.*}
742 rewrite_terms_ @{theory Isac} e_rew_ord e_rls [s_1] eq3'';
745 rewrite_set_ @{theory Isac} false norm_Rational eq4_1;
748 val fmz = ["equality (3=3*A/(4::real))", "solveFor A","solutions L"];
749 val (dI',pI',mI') =("Isac", ["univariate","equation"], ["no_met"]);
751 * Solve the simple linear equation for A:
752 * Return eq, not list of eq's
754 val (p,_,fa,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
755 val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
756 (*Add_Given "equality (3=3*A/4)"*)
757 val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
758 (*Add_Given "solveFor A"*)
759 val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
760 (*Add_Find "solutions L"*)
761 val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
762 (*Specify_Theory "Isac"*)
763 val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
764 (*Specify_Problem ["normalize","polynomial",
765 "univariate","equation"])*)
766 val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
767 (* Specify_Method["PolyEq","normalize_poly"]*)
768 val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
769 (*Apply_Method["PolyEq","normalize_poly"]*)
770 val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
771 (*Rewrite ("all_left","PolyEq.all_left")*)
772 val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
773 (*Rewrite_Set_Inst(["(bdv,A)"],"make_ratpoly_in")*)
774 val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
775 (*Rewrite_Set "polyeq_simplify"*)
776 val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
777 val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
778 val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
779 (*Add_Given "equality (3 + -3 / 4 * A =0)"*)
780 val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
781 (*Add_Given "solveFor A"*)
782 val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
783 (*Add_Find "solutions A_i"*)
784 val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
785 val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
786 val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
787 val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
788 (*Apply_Method ["PolyEq","solve_d1_polyeq_equation"]*)
789 val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
790 (*Rewrite_Set_Inst(["(bdv,A)"],"d1_polyeq_simplify")*)
791 val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
792 (*Rewrite_Set "polyeq_simplify"*)
793 val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
794 (*Rewrite_Set "norm_Rational_parenthesized"*)
795 val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
797 val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
798 (*Check_elementwise "Assumptions"*)
799 val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
800 (*Check_Postcond ["degree_1","polynomial",
801 "univariate","equation"]*)
802 val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
803 (*Check_Postcond ["normalize","polynomial",
804 "univariate","equation"]*)
805 val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
810 subsubsection {*Get Second Coefficient*}
812 text{*\noindent With the use of \texttt{thy} we check which theories the
817 text{*\noindent To get the second coefficient we substitute $z$ with the second
818 zero-point we determined in Section~\ref{sec:solveq}.*}
821 val SOME (eq4b_1,_) =
822 rewrite_terms_ @{theory Isac} e_rew_ord e_rls [s_2] eq3'';
824 val SOME (eq4b_2,_) =
825 rewrite_set_ @{theory Isac} false norm_Rational eq4b_1;
828 val fmz = ["equality (3= -3*B/(4::real))", "solveFor B","solutions L"];
829 val (dI',pI',mI') =("Isac", ["univariate","equation"], ["no_met"]);
830 val (p,_,fb,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
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;
853 val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
854 val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
855 val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
856 val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
857 val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
861 text{*\noindent We compare our results with the pre calculated upshot.*}
864 if f2str fa = "[A = 4]" then () else error "part.fract. eq4_1";
865 if f2str fb = "[B = -4]" then () else error "part.fract. eq4_1";
868 section {*Implement the Specification and the Method \label{spec-meth}*}
870 text{*\noindent Now everything we need for solving the problem has been
871 tested out. We now start by creating new nodes for our methods and
872 further on our new program in the interpreter.*}
874 subsection{*Define the Field Descriptions for the
875 Specification\label{sec:deffdes}*}
877 text{*\noindent We define the fields \em filterExpression \normalfont and
878 \em stepResponse \normalfont both as equations, they represent the in- and
879 output of the program.*}
882 filterExpression :: "bool => una"
883 stepResponse :: "bool => una"
885 subsection{*Define the Specification*}
887 text{*\noindent The next step is defining the specifications as nodes in the
888 designated part. We have to create the hierarchy node by node and start
889 with \em SignalProcessing \normalfont and go on by creating the node
890 \em Z\_Transform\normalfont.*}
894 (prep_pbt thy "pbl_SP" [] e_pblID
895 (["SignalProcessing"], [], e_rls, NONE, []));
897 (prep_pbt thy "pbl_SP_Ztrans" [] e_pblID
898 (["Z_Transform","SignalProcessing"], [], e_rls, NONE, []));
901 text{*\noindent For the suddenly created node we have to define the input
902 and output parameters. We already prepared their definition in
903 Section~\ref{sec:deffdes}.*}
907 (prep_pbt thy "pbl_SP_Ztrans_inv" [] e_pblID
908 (["inverse", "Z_Transform", "SignalProcessing"],
909 [("#Given" ,["filterExpression X_eq"]),
910 ("#Find" ,["stepResponse n_eq"])
912 append_rls "e_rls" e_rls [(*for preds in where_*)], NONE,
913 [["SignalProcessing","Z_Transform","inverse"]]));
916 get_pbt ["inverse","Z_Transform","SignalProcessing"];
919 subsection {*Define Name and Signature for the Method*}
921 text{*\noindent As a next step we store the definition of our new method as a
922 constant for the interpreter.*}
925 InverseZTransform :: "[bool, bool] => bool"
926 ("((Script InverseZTransform (_ =))// (_))" 9)
928 subsection {*Setup Parent Nodes in Hierarchy of Method\label{sec:cparentnode}*}
930 text{*\noindent Again we have to generate the nodes step by step, first the
931 parent node and then the originally \em Z\_Transformation
932 \normalfont node. We have to define both nodes first with an empty script
937 (prep_met thy "met_SP" [] e_metID
938 (["SignalProcessing"], [],
939 {rew_ord'="tless_true", rls'= e_rls, calc = [],
940 srls = e_rls, prls = e_rls,
941 crls = e_rls, nrls = e_rls}, "empty_script"));
943 (prep_met thy "met_SP_Ztrans" [] e_metID
944 (["SignalProcessing", "Z_Transform"], [],
945 {rew_ord'="tless_true", rls'= e_rls, calc = [],
946 srls = e_rls, prls = e_rls,
947 crls = e_rls, nrls = e_rls}, "empty_script"));
950 text{*\noindent After we generated both nodes, we can fill the containing
951 script we want to implement later. First we define the specifications
952 of the script in e.g. the in- and output.*}
956 (prep_met thy "met_SP_Ztrans_inv" [] e_metID
957 (["SignalProcessing", "Z_Transform", "inverse"],
958 [("#Given" ,["filterExpression X_eq"]),
959 ("#Find" ,["stepResponse n_eq"])
961 {rew_ord'="tless_true", rls'= e_rls, calc = [],
962 srls = e_rls, prls = e_rls,
963 crls = e_rls, nrls = e_rls}, "empty_script"));
966 text{*\noindent After we stored the definition we can start implementing the
967 script itself. As a first try we define only three rows containing one
972 (prep_met thy "met_SP_Ztrans_inv" [] e_metID
973 (["SignalProcessing", "Z_Transform", "inverse"],
974 [("#Given" ,["filterExpression X_eq"]),
975 ("#Find" ,["stepResponse n_eq"])
977 {rew_ord'="tless_true", rls'= e_rls, calc = [],
978 srls = e_rls, prls = e_rls,
979 crls = e_rls, nrls = e_rls},
980 "Script InverseZTransform (Xeq::bool) =" ^
981 " (let X = Take Xeq;" ^
982 " X = Rewrite ruleZY False X" ^
986 text{*\noindent Check if the method has been stored correctly\ldots*}
992 text{*\noindent If yes we can get the method by stepping backwards through
996 get_met ["SignalProcessing","Z_Transform","inverse"];
999 section {*Program in TP-based language \label{prog-steps}*}
1001 text{*\noindent We start stepwise expanding our program. The script is a
1002 simple string containing several manipulation instructions.
1003 \par The first script we try contains no instruction, we only test if
1004 building scripts that way work.*}
1006 subsection {*Stepwise Extend the Program*}
1009 "Script InverseZTransform (Xeq::bool) = "^
1013 text{*\noindent Next we put some instructions in the script and try if we are
1014 able to solve our first equation.*}
1018 "Script InverseZTransform (Xeq::bool) = "^
1020 * 1/z) instead of z ^^^ -1
1022 " (let X = Take Xeq; "^
1023 " X' = Rewrite ruleZY False X; "^
1027 " X' = (Rewrite_Set norm_Rational False) X' "^
1035 "Script InverseZTransform (Xeq::bool) = "^
1037 * (1/z) instead of z ^^^ -1
1039 " (let X = Take Xeq; "^
1040 " X' = Rewrite ruleZY False X; "^
1044 " X' = (Rewrite_Set norm_Rational False) X'; "^
1048 " X' = (SubProblem (Isac',[pqFormula,degree_2, "^
1049 " polynomial,univariate,equation], "^
1051 " [BOOL e_e, REAL v_v]) "^
1055 text{*\noindent To solve the equation it is necessary to drop the left hand
1056 side, now we only need the denominator of the right hand side. The first
1057 equation solves the zeros of our expression.*}
1061 "Script InverseZTransform (Xeq::bool) = "^
1062 " (let X = Take Xeq; "^
1063 " X' = Rewrite ruleZY False X; "^
1064 " X' = (Rewrite_Set norm_Rational False) X'; "^
1065 " funterm = rhs X' "^
1067 * drop X'= for equation solving
1072 text{*\noindent As mentioned above, we need the denominator of the right hand
1073 side. The equation itself consists of this denominator and tries to find
1074 a $z$ for this the denominator is equal to zero.*}
1078 "Script InverseZTransform (X_eq::bool) = "^
1079 " (let X = Take X_eq; "^
1080 " X' = Rewrite ruleZY False X; "^
1081 " X' = (Rewrite_Set norm_Rational False) X'; "^
1082 " (X'_z::real) = lhs X'; "^
1083 " (z::real) = argument_in X'_z; "^
1084 " (funterm::real) = rhs X'; "^
1085 " (denom::real) = get_denominator funterm; "^
1089 " (equ::bool) = (denom = (0::real)); "^
1090 " (L_L::bool list) = "^
1091 " (SubProblem (Test', "^
1092 " [linear,univariate,equation,test], "^
1093 " [Test,solve_linear]) "^
1094 " [BOOL equ, REAL z]) "^
1098 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
1102 text {*\noindent This ruleset contains all functions that are in the script;
1103 The evaluation of the functions is done by rewriting using this ruleset.*}
1107 Rls {id="srls_InverseZTransform",
1109 rew_ord = ("termlessI",termlessI),
1110 erls = append_rls "erls_in_srls_InverseZTransform" e_rls
1111 [(*for asm in NTH_CONS ...*)
1112 Calc ("Orderings.ord_class.less",eval_equ "#less_"),
1113 (*2nd NTH_CONS pushes n+-1 into asms*)
1114 Calc("Groups.plus_class.plus", eval_binop "#add_")
1116 srls = Erls, calc = [],
1118 Thm ("NTH_CONS",num_str @{thm NTH_CONS}),
1119 Calc("Groups.plus_class.plus",
1120 eval_binop "#add_"),
1121 Thm ("NTH_NIL",num_str @{thm NTH_NIL}),
1122 Calc("Tools.lhs", eval_lhs"eval_lhs_"),
1123 Calc("Tools.rhs", eval_rhs"eval_rhs_"),
1124 Calc("Atools.argument'_in",
1125 eval_argument_in "Atools.argument'_in"),
1126 Calc("Rational.get_denominator",
1127 eval_get_denominator "#get_denominator"),
1128 Calc("Rational.get_numerator",
1129 eval_get_numerator "#get_numerator"),
1130 Calc("Partial_Fractions.factors_from_solution",
1131 eval_factors_from_solution
1132 "#factors_from_solution"),
1133 Calc("Partial_Fractions.drop_questionmarks",
1134 eval_drop_questionmarks "#drop_?")
1140 subsection {*Store Final Version of Program for Execution*}
1142 text{*\noindent After we also tested how to write scripts and run them,
1143 we start creating the final version of our script and store it into
1144 the method for which we created a node in Section~\ref{sec:cparentnode}
1145 Note that we also did this stepwise, but we didn't kept every
1150 prep_met thy "met_SP_Ztrans_inv" [] e_metID
1151 (["SignalProcessing",
1155 ("#Given" ,["filterExpression X_eq"]),
1156 ("#Find" ,["stepResponse n_eq"])
1159 rew_ord'="tless_true",
1160 rls'= e_rls, calc = [],
1163 crls = e_rls, nrls = e_rls
1165 "Script InverseZTransform (X_eq::bool) = "^
1166 (*(1/z) instead of z ^^^ -1*)
1167 "(let X = Take X_eq; "^
1168 " X' = Rewrite ruleZY False X; "^
1170 " (num_orig::real) = get_numerator (rhs X'); "^
1171 " X' = (Rewrite_Set norm_Rational False) X'; "^
1173 " (X'_z::real) = lhs X'; "^
1174 " (zzz::real) = argument_in X'_z; "^
1175 " (funterm::real) = rhs X'; "^
1176 (*drop X' z = for equation solving*)
1177 " (denom::real) = get_denominator funterm; "^
1179 " (num::real) = get_numerator funterm; "^
1181 " (equ::bool) = (denom = (0::real)); "^
1182 " (L_L::bool list) = (SubProblem (PolyEq', "^
1183 " [abcFormula,degree_2,polynomial,univariate,equation], "^
1185 " [BOOL equ, REAL zzz]); "^
1186 " (facs::real) = factors_from_solution L_L; "^
1187 " (eql::real) = Take (num_orig / facs); "^
1189 " (eqr::real) = (Try (Rewrite_Set ansatz_rls False)) eql; "^
1191 " (eq::bool) = Take (eql = eqr); "^
1192 (*Maybe possible to use HOLogic.mk_eq ??*)
1193 " eq = (Try (Rewrite_Set equival_trans False)) eq; "^
1195 " eq = drop_questionmarks eq; "^
1196 " (z1::real) = (rhs (NTH 1 L_L)); "^
1198 * prepare equation for a - eq_a
1199 * therefor substitute z with solution 1 - z1
1201 " (z2::real) = (rhs (NTH 2 L_L)); "^
1203 " (eq_a::bool) = Take eq; "^
1204 " eq_a = (Substitute [zzz=z1]) eq; "^
1205 " eq_a = (Rewrite_Set norm_Rational False) eq_a; "^
1206 " (sol_a::bool list) = "^
1207 " (SubProblem (Isac', "^
1208 " [univariate,equation],[no_met]) "^
1209 " [BOOL eq_a, REAL (A::real)]); "^
1210 " (a::real) = (rhs(NTH 1 sol_a)); "^
1212 " (eq_b::bool) = Take eq; "^
1213 " eq_b = (Substitute [zzz=z2]) eq_b; "^
1214 " eq_b = (Rewrite_Set norm_Rational False) eq_b; "^
1215 " (sol_b::bool list) = "^
1216 " (SubProblem (Isac', "^
1217 " [univariate,equation],[no_met]) "^
1218 " [BOOL eq_b, REAL (B::real)]); "^
1219 " (b::real) = (rhs(NTH 1 sol_b)); "^
1221 " eqr = drop_questionmarks eqr; "^
1222 " (pbz::real) = Take eqr; "^
1223 " pbz = ((Substitute [A=a, B=b]) pbz); "^
1225 " pbz = Rewrite ruleYZ False pbz; "^
1226 " pbz = drop_questionmarks pbz; "^
1228 " (X_z::bool) = Take (X_z = pbz); "^
1229 " (n_eq::bool) = (Rewrite_Set inverse_z False) X_z; "^
1230 " n_eq = drop_questionmarks n_eq "^
1237 subsection {*Check the Program*}
1238 text{*\noindent When the script is ready we can start checking our work.*}
1239 subsubsection {*Check the Formalization*}
1240 text{*\noindent First we want to check the formalization of the in and
1241 output of our program.*}
1245 ["filterExpression (X = 3 / (z - 1/4 + -1/8 * (1/(z::real))))",
1246 "stepResponse (x[n::real]::bool)"];
1248 ("Isac", ["inverse", "Z_Transform", "SignalProcessing"],
1249 ["SignalProcessing","Z_Transform","inverse"]);
1256 Const ("Inverse_Z_Transform.filterExpression", _),
1257 [Const ("HOL.eq", _) $ _ $ _]
1263 Const ("Inverse_Z_Transform.stepResponse", _),
1267 ) = prep_ori fmz thy ((#ppc o get_pbt) pI);
1270 = (#scr o get_met) ["SignalProcessing",
1276 subsubsection {*Stepwise Check the Program\label{sec:stepcheck}*}
1277 text{*\noindent We start to stepwise execute our new program in a calculation
1278 tree and check if every node implements that what we have wanted.*}
1281 trace_rewrite := false;
1282 trace_script := false;
1286 ["filterExpression (X z = 3 / (z - 1/4 + -1/8 * (1/(z::real))))",
1287 "stepResponse (x[n::real]::bool)"];
1290 ("Isac", ["inverse", "Z_Transform", "SignalProcessing"],
1291 ["SignalProcessing","Z_Transform","inverse"]);
1293 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI,pI,mI))];
1294 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1296 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1298 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1300 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1302 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1304 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1306 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1307 "Rewrite (ruleZY, Inverse_Z_Transform.ruleZY)";
1308 "--> X z = 3 / (z - 1 / 4 + -1 / 8 * (1 / z))";
1312 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1313 "Rewrite_Set norm_Rational";
1314 " --> X' z = 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))";
1315 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1319 text {*\noindent Instead of \ttfamily nxt = Subproblem \normalfont above we had
1320 \ttfamily Empty\_Tac; \normalfont the search for the reason considered
1321 the following points:\begin{itemize}
1322 \item What shows \ttfamily show\_pt pt;\normalfont\ldots?
1323 \begin{verbatim}(([2], Res), ?X' z = 24 / (-1 + -2 * z + 8 * z ^^^ 2))]\end{verbatim}
1324 The calculation is ok but no \ttfamily next \normalfont step found:
1325 Should be\\ \ttfamily nxt = Subproblem\normalfont!
1326 \item What shows \ttfamily trace\_script := true; \normalfont we read
1329 @@@next leaf 'SubProblem
1330 (PolyEq',[abcFormula, degree_2, polynomial,
1331 univariate, equation], no_meth)
1333 ---> STac 'SubProblem (PolyEq',
1334 [abcFormula, degree_2, polynomial,
1335 univariate, equation], no_meth)
1336 [BOOL (-1 + -2 * z + 8 * z \^\^\^ ~2 = 0), REAL z]'
1338 We see the SubProblem with correct arguments from searching next
1339 step (program text !!!--->!!! STac (script tactic) with arguments
1341 \item Do we have the right Script \ldots difference in the
1342 arguments in the arguments\ldots
1345 (#scr o get_met) ["SignalProcessing",
1348 writeln (term2str s);
1350 \ldots shows the right script. Difference in the arguments.
1351 \item Test --- Why helpless here ? --- shows: \ttfamily replace
1352 no\_meth by [no\_meth] \normalfont in Script
1357 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1361 text {*\noindent Instead of \ttfamily nxt = Model\_Problem \normalfont above
1362 we had \ttfamily Empty\_Tac; \normalfont the search for the reason
1363 considered the following points:\begin{itemize}
1364 \item Difference in the arguments
1365 \item Comparison with Subsection~\ref{sec:solveq}: There solving this
1366 equation works, so there must be some difference in the arguments
1367 of the Subproblem: RIGHT: we had \ttfamily [no\_meth] \normalfont
1368 instead of \ttfamily [no\_met] \normalfont ;-)
1372 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1373 (*Add_Given equality (-1 + -2 * z + 8 * z ^^^ 2 = 0)";*)
1374 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1375 (*Add_Given solveFor z";*)
1376 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1377 (*Add_Find solutions z_i";*)
1378 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1379 (*Specify_Theory Isac";*)
1382 text {*\noindent We had \ttfamily nxt = Empty\_Tac instead Specify\_Theory;
1383 \normalfont The search for the reason considered the following points:
1385 \item Was there an error message? NO -- ok
1386 \item Has \ttfamily nxt = Add\_Find \normalfont been inserted in pt:\\
1387 \ttfamily get\_obj g\_pbl pt (fst p);\normalfont? YES -- ok
1388 \item What is the returned formula:
1390 print_depth 999; f; print_depth 999;
1391 { Find = [ Correct "solutions z_i"],
1393 Given = [Correct "equality (-1 + -2*z + 8*z ^^^ 2 = 0)",
1394 Correct "solveFor z"],
1398 \normalfont The only False is the reason: the Where (the precondition) is
1399 False for good reasons: The precondition seems to check for linear
1400 equations, not for the one we want to solve! Removed this error by
1401 correcting the Script from \ttfamily SubProblem (PolyEq',
1402 \lbrack linear,univariate,equation,
1403 test\rbrack, \lbrack Test,solve\_linear\rbrack \normalfont to
1404 \ttfamily SubProblem (PolyEq',\\ \lbrack abcFormula,degree\_2,
1405 polynomial,univariate,equation\rbrack,\\
1406 \lbrack PolyEq,solve\_d2\_polyeq\_abc\_equation
1408 You find the appropriate type of equation at the
1409 {\sisac}-WEB-Page\footnote{
1410 \href{http://www.ist.tugraz.at/projects/isac/www/kbase/pbl/index\_pbl.html}
1411 {http://www.ist.tugraz.at/projects/isac/www/kbase/pbl/index\_pbl.html}
1413 And the respective method in \ttfamily Knowledge/PolyEq.thy \normalfont
1414 at the respective \ttfamily store\_pbt. \normalfont Or you leave the
1415 selection of the appropriate type to isac as done in the final Script ;-))
1419 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1420 (*Specify_Problem [abcFormula,...";*)
1421 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1422 (*Specify_Method [PolyEq,solve_d2_polyeq_abc_equation";*)
1423 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1424 (*Apply_Method [PolyEq,solve_d2_polyeq_abc_equation";*)
1425 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1426 (*Rewrite_Set_Inst ([(bdv, z)], d2_polyeq_abcFormula_simplify";*)
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 (*Specify_Problem ["normalize","polynomial","univariate","equation"]*)
1445 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1446 (*Specify_Method ["PolyEq", "normalize_poly"]*)
1447 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1448 (*Apply_Method ["PolyEq", "normalize_poly"]*)
1449 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1450 (*Rewrite ("all_left", "PolyEq.all_left")*)
1451 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1452 (*Rewrite_Set_Inst (["(bdv, A)"], "make_ratpoly_in")*)
1453 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1454 (*Rewrite_Set "polyeq_simplify"*)
1455 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1456 (*Subproblem("Isac",["degree_1","polynomial","univariate","equation"])*)
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;
1472 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1473 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1474 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1475 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1476 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1477 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1478 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1479 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1480 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1481 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1482 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1483 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1484 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1485 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1486 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1487 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1488 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1489 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1490 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1491 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1492 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1493 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1494 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1495 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1496 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1497 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1498 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1499 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1500 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1501 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1502 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1503 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1504 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1505 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1506 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1507 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1508 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1509 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1510 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1511 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1512 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1513 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1514 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1517 text{*\noindent As a last step we check the tracing output of the last calc
1518 tree instruction and compare it with the pre-calculated result.*}
1520 section {* Improve and Transfer into Knowledge *}
1522 We want to improve the very long program \ttfamily InverseZTransform
1523 \normalfont by modularisation: partial fraction decomposition shall
1524 become a sub-problem.
1526 We could transfer all knowledge in \ttfamily Build\_Inverse\_Z\_Transform.thy
1527 \normalfont first to the \ttfamily Knowledge/Inverse\_Z\_Transform.thy
1528 \normalfont and then modularise. In this case TODO problems?!?
1530 We chose another way and go bottom up: first we build the sub-problem in
1531 \ttfamily Partial\_Fractions.thy \normalfont with the term:
1533 $$\frac{3}{x\cdot(z - \frac{1}{4} + \frac{-1}{8}\cdot\frac{1}{z})}$$
1535 \noindent (how this still can be improved see \ttfamily Partial\_Fractions.thy\normalfont),
1536 and re-use all stuff prepared in \ttfamily Build\_Inverse\_Z\_Transform.thy:
1537 \normalfont The knowledge will be transferred to \ttfamily src/../Partial\_Fractions.thy
1538 \normalfont and the respective tests to:
1539 \begin{center}\ttfamily test/../sartial\_fractions.sml\normalfont\end{center}
1542 subsection {* Transfer to Partial\_Fractions.thy *}
1544 First we transfer both, knowledge and tests into:
1545 \begin{center}\ttfamily src/../Partial\_Fractions.thy\normalfont\end{center}
1546 in order to immediately have the test results.
1548 We copy \ttfamily factors\_from\_solution, drop\_questionmarks,\\
1549 ansatz\_2nd\_order \normalfont and rule-sets --- no problem.
1551 Also \ttfamily store\_pbt ..\\ "pbl\_simp\_rat\_partfrac"
1552 \normalfont is easy.
1554 But then we copy from:\\
1555 (1) \ttfamily Build\_Inverse\_Z\_Transform.thy store\_met\ldots "met\_SP\_Ztrans\_inv"
1557 (2) \ttfamily Partial\_Fractions.thy store\_met\ldots "met\_SP\_Ztrans\_inv"
1558 \normalfont\\ and cut out the respective part from the program. First we ensure that
1559 the string is correct. When we insert the string into (2)
1560 \ttfamily store\_met .. "met\_partial\_fraction" \normalfont --- and get an error.
1563 subsubsection {* 'Programming' in ISAC's TP-based Language *}
1565 At the present state writing programs in {\sisac} is particularly cumbersome.
1566 So we give hints how to cope with the many obstacles. Below we describe the
1567 steps we did in making (2) run.
1570 \item We check if the \textbf{string} containing the program is correct.
1571 \item We check if the \textbf{types in the program} are correct.
1572 For this purpose we start start with the first and last lines
1574 "PartFracScript (f_f::real) (v_v::real) = " ^
1575 " (let X = Take f_f; " ^
1576 " pbz = ((Substitute []) X) " ^
1579 The last but one line helps not to bother with ';'.
1580 \item Then we add line by line. Already the first line causes the error.
1581 So we investigate it by
1583 val ctxt = ProofContext.init_global @ { theory } ;
1585 parseNEW ctxt "(num_orig::real) =
1586 get_numerator(rhs f_f)";
1588 and see a type clash: \ttfamily rhs \normalfont from (1) requires type
1589 \ttfamily bool \normalfont while (2) wants to have \ttfamily (f\_f::real).
1590 \normalfont Of course, we don't need \ttfamily rhs \normalfont anymore.
1591 \item Type-checking can be very tedious. One might even inspect the
1592 parse-tree of the program with {\sisac}'s specific debug tools:
1594 val {scr = Script t,...} =
1595 get_met ["simplification",
1597 "to_partial_fraction"];
1598 atomty_thy @ { theory } t ;
1600 \item We check if the \textbf{semantics of the program} by stepwise evaluation
1601 of the program. Evaluation is done by the Lucas-Interpreter, which works
1602 using the knowledge in theory Isac; so we have to re-build Isac. And the
1603 test are performed simplest in a file which is loaded with Isac.
1604 See \ttfamily tests/../partial\_fractions.sml \normalfont.
1608 subsection {* Transfer to Inverse\_Z\_Transform.thy *}
1610 Unfortunately it was not possible to complete this task. Because we ran out of time\ldots