Test_Isac works again, almost ..
4 files raise errors:
# Interpret/solve.sml: "solve.sml: interSteps on norm_Rational 2"
# Interpret/inform.sml: "inform.sml: [rational,simplification] 2"
# Knowledge/partial_fractions.sml: "autoCalculate for met_partial_fraction changed: final result"
# Knowledge/eqsystem.sml: "eqsystem.sml: exp 7.70 normalize 4x4 by rewrite changed"
The chunk of changes is due to the fact, that Isac's code still is unstable.
The changes are accumulated since e8f46493af82.
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(
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.*}
889 (prep_pbt thy "pbl_SP" [] e_pblID
890 (["SignalProcessing"], [], e_rls, NONE, []));
892 (prep_pbt thy "pbl_SP_Ztrans" [] e_pblID
893 (["Z_Transform","SignalProcessing"], [], e_rls, NONE, []));
896 text{*\noindent For the suddenly created node we have to define the input
897 and output parameters. We already prepared their definition in
898 Section~\ref{sec:deffdes}.*}
902 (prep_pbt thy "pbl_SP_Ztrans_inv" [] e_pblID
903 (["Inverse", "Z_Transform", "SignalProcessing"],
904 [("#Given" ,["filterExpression X_eq"]),
905 ("#Find" ,["stepResponse n_eq"])
907 append_rls "e_rls" e_rls [(*for preds in where_*)], NONE,
908 [["SignalProcessing","Z_Transform","Inverse"]]));
911 get_pbt ["Inverse","Z_Transform","SignalProcessing"];
914 subsection {*Define Name and Signature for the Method*}
916 text{*\noindent As a next step we store the definition of our new method as a
917 constant for the interpreter.*}
920 InverseZTransform :: "[bool, bool] => bool"
921 ("((Script InverseZTransform (_ =))// (_))" 9)
923 subsection {*Setup Parent Nodes in Hierarchy of Method\label{sec:cparentnode}*}
925 text{*\noindent Again we have to generate the nodes step by step, first the
926 parent node and then the originally \em Z\_Transformation
927 \normalfont node. We have to define both nodes first with an empty script
932 (prep_met thy "met_SP" [] e_metID
933 (["SignalProcessing"], [],
934 {rew_ord'="tless_true", rls'= e_rls, calc = [],
935 srls = e_rls, prls = e_rls,
936 crls = e_rls, errpats = [], nrls = e_rls}, "empty_script"));
938 (prep_met thy "met_SP_Ztrans" [] e_metID
939 (["SignalProcessing", "Z_Transform"], [],
940 {rew_ord'="tless_true", rls'= e_rls, calc = [],
941 srls = e_rls, prls = e_rls,
942 crls = e_rls, errpats = [], nrls = e_rls}, "empty_script"));
945 text{*\noindent After we generated both nodes, we can fill the containing
946 script we want to implement later. First we define the specifications
947 of the script in e.g. the in- and output.*}
951 (prep_met thy "met_SP_Ztrans_inv" [] e_metID
952 (["SignalProcessing", "Z_Transform", "Inverse"],
953 [("#Given" ,["filterExpression X_eq"]),
954 ("#Find" ,["stepResponse n_eq"])
956 {rew_ord'="tless_true", rls'= e_rls, calc = [],
957 srls = e_rls, prls = e_rls,
958 crls = e_rls, errpats = [], nrls = e_rls}, "empty_script"));
961 text{*\noindent After we stored the definition we can start implementing the
962 script itself. As a first try we define only three rows containing one
967 (prep_met thy "met_SP_Ztrans_inv" [] e_metID
968 (["SignalProcessing", "Z_Transform", "Inverse"],
969 [("#Given" ,["filterExpression X_eq"]),
970 ("#Find" ,["stepResponse n_eq"])
972 {rew_ord'="tless_true", rls'= e_rls, calc = [],
973 srls = e_rls, prls = e_rls,
974 crls = e_rls, errpats = [], nrls = e_rls},
975 "Script InverseZTransform (Xeq::bool) =" ^
976 " (let X = Take Xeq;" ^
977 " X = Rewrite ruleZY False X" ^
981 text{*\noindent Check if the method has been stored correctly\ldots*}
987 text{*\noindent If yes we can get the method by stepping backwards through
991 get_met ["SignalProcessing","Z_Transform","Inverse"];
994 section {*Program in TP-based language \label{prog-steps}*}
996 text{*\noindent We start stepwise expanding our program. The script is a
997 simple string containing several manipulation instructions.
998 \par The first script we try contains no instruction, we only test if
999 building scripts that way work.*}
1001 subsection {*Stepwise Extend the Program*}
1004 "Script InverseZTransform (Xeq::bool) = "^
1008 text{*\noindent Next we put some instructions in the script and try if we are
1009 able to solve our first equation.*}
1013 "Script InverseZTransform (Xeq::bool) = "^
1015 * 1/z) instead of z ^^^ -1
1017 " (let X = Take Xeq; "^
1018 " X' = Rewrite ruleZY False X; "^
1022 " X' = (Rewrite_Set norm_Rational False) X' "^
1030 "Script InverseZTransform (Xeq::bool) = "^
1032 * (1/z) instead of z ^^^ -1
1034 " (let X = Take Xeq; "^
1035 " X' = Rewrite ruleZY False X; "^
1039 " X' = (Rewrite_Set norm_Rational False) X'; "^
1043 " X' = (SubProblem (Isac',[pqFormula,degree_2, "^
1044 " polynomial,univariate,equation], "^
1046 " [BOOL e_e, REAL v_v]) "^
1050 text{*\noindent To solve the equation it is necessary to drop the left hand
1051 side, now we only need the denominator of the right hand side. The first
1052 equation solves the zeros of our expression.*}
1056 "Script InverseZTransform (Xeq::bool) = "^
1057 " (let X = Take Xeq; "^
1058 " X' = Rewrite ruleZY False X; "^
1059 " X' = (Rewrite_Set norm_Rational False) X'; "^
1060 " funterm = rhs X' "^
1062 * drop X'= for equation solving
1067 text{*\noindent As mentioned above, we need the denominator of the right hand
1068 side. The equation itself consists of this denominator and tries to find
1069 a $z$ for this the denominator is equal to zero.*}
1073 "Script InverseZTransform (X_eq::bool) = "^
1074 " (let X = Take X_eq; "^
1075 " X' = Rewrite ruleZY False X; "^
1076 " X' = (Rewrite_Set norm_Rational False) X'; "^
1077 " (X'_z::real) = lhs X'; "^
1078 " (z::real) = argument_in X'_z; "^
1079 " (funterm::real) = rhs X'; "^
1080 " (denom::real) = get_denominator funterm; "^
1084 " (equ::bool) = (denom = (0::real)); "^
1085 " (L_L::bool list) = "^
1086 " (SubProblem (Test', "^
1087 " [linear,univariate,equation,test], "^
1088 " [Test,solve_linear]) "^
1089 " [BOOL equ, REAL z]) "^
1093 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
1097 text {*\noindent This ruleset contains all functions that are in the script;
1098 The evaluation of the functions is done by rewriting using this ruleset.*}
1102 Rls {id="srls_InverseZTransform",
1104 rew_ord = ("termlessI",termlessI),
1105 erls = append_rls "erls_in_srls_InverseZTransform" e_rls
1106 [(*for asm in NTH_CONS ...*)
1107 Calc ("Orderings.ord_class.less",eval_equ "#less_"),
1108 (*2nd NTH_CONS pushes n+-1 into asms*)
1109 Calc("Groups.plus_class.plus", eval_binop "#add_")
1111 srls = Erls, calc = [], errpatts = [],
1113 Thm ("NTH_CONS",num_str @{thm NTH_CONS}),
1114 Calc("Groups.plus_class.plus",
1115 eval_binop "#add_"),
1116 Thm ("NTH_NIL",num_str @{thm NTH_NIL}),
1117 Calc("Tools.lhs", eval_lhs"eval_lhs_"),
1118 Calc("Tools.rhs", eval_rhs"eval_rhs_"),
1119 Calc("Atools.argument'_in",
1120 eval_argument_in "Atools.argument'_in"),
1121 Calc("Rational.get_denominator",
1122 eval_get_denominator "#get_denominator"),
1123 Calc("Rational.get_numerator",
1124 eval_get_numerator "#get_numerator"),
1125 Calc("Partial_Fractions.factors_from_solution",
1126 eval_factors_from_solution
1127 "#factors_from_solution"),
1128 Calc("Partial_Fractions.drop_questionmarks",
1129 eval_drop_questionmarks "#drop_?")
1135 subsection {*Store Final Version of Program for Execution*}
1137 text{*\noindent After we also tested how to write scripts and run them,
1138 we start creating the final version of our script and store it into
1139 the method for which we created a node in Section~\ref{sec:cparentnode}
1140 Note that we also did this stepwise, but we didn't kept every
1145 prep_met thy "met_SP_Ztrans_inv" [] e_metID
1146 (["SignalProcessing",
1150 ("#Given" ,["filterExpression X_eq"]),
1151 ("#Find" ,["stepResponse n_eq"])
1154 rew_ord'="tless_true",
1155 rls'= e_rls, calc = [],
1158 crls = e_rls, errpats = [], nrls = e_rls
1160 "Script InverseZTransform (X_eq::bool) = "^
1161 (*(1/z) instead of z ^^^ -1*)
1162 "(let X = Take X_eq; "^
1163 " X' = Rewrite ruleZY False X; "^
1165 " (num_orig::real) = get_numerator (rhs X'); "^
1166 " X' = (Rewrite_Set norm_Rational False) X'; "^
1168 " (X'_z::real) = lhs X'; "^
1169 " (zzz::real) = argument_in X'_z; "^
1170 " (funterm::real) = rhs X'; "^
1171 (*drop X' z = for equation solving*)
1172 " (denom::real) = get_denominator funterm; "^
1174 " (num::real) = get_numerator funterm; "^
1176 " (equ::bool) = (denom = (0::real)); "^
1177 " (L_L::bool list) = (SubProblem (PolyEq', "^
1178 " [abcFormula,degree_2,polynomial,univariate,equation], "^
1180 " [BOOL equ, REAL zzz]); "^
1181 " (facs::real) = factors_from_solution L_L; "^
1182 " (eql::real) = Take (num_orig / facs); "^
1184 " (eqr::real) = (Try (Rewrite_Set ansatz_rls False)) eql; "^
1186 " (eq::bool) = Take (eql = eqr); "^
1187 (*Maybe possible to use HOLogic.mk_eq ??*)
1188 " eq = (Try (Rewrite_Set equival_trans False)) eq; "^
1190 " eq = drop_questionmarks eq; "^
1191 " (z1::real) = (rhs (NTH 1 L_L)); "^
1193 * prepare equation for a - eq_a
1194 * therefor substitute z with solution 1 - z1
1196 " (z2::real) = (rhs (NTH 2 L_L)); "^
1198 " (eq_a::bool) = Take eq; "^
1199 " eq_a = (Substitute [zzz=z1]) eq; "^
1200 " eq_a = (Rewrite_Set norm_Rational False) eq_a; "^
1201 " (sol_a::bool list) = "^
1202 " (SubProblem (Isac', "^
1203 " [univariate,equation],[no_met]) "^
1204 " [BOOL eq_a, REAL (A::real)]); "^
1205 " (a::real) = (rhs(NTH 1 sol_a)); "^
1207 " (eq_b::bool) = Take eq; "^
1208 " eq_b = (Substitute [zzz=z2]) eq_b; "^
1209 " eq_b = (Rewrite_Set norm_Rational False) eq_b; "^
1210 " (sol_b::bool list) = "^
1211 " (SubProblem (Isac', "^
1212 " [univariate,equation],[no_met]) "^
1213 " [BOOL eq_b, REAL (B::real)]); "^
1214 " (b::real) = (rhs(NTH 1 sol_b)); "^
1216 " eqr = drop_questionmarks eqr; "^
1217 " (pbz::real) = Take eqr; "^
1218 " pbz = ((Substitute [A=a, B=b]) pbz); "^
1220 " pbz = Rewrite ruleYZ False pbz; "^
1221 " pbz = drop_questionmarks pbz; "^
1223 " (X_z::bool) = Take (X_z = pbz); "^
1224 " (n_eq::bool) = (Rewrite_Set inverse_z False) X_z; "^
1225 " n_eq = drop_questionmarks n_eq "^
1232 subsection {*Check the Program*}
1233 text{*\noindent When the script is ready we can start checking our work.*}
1234 subsubsection {*Check the Formalization*}
1235 text{*\noindent First we want to check the formalization of the in and
1236 output of our program.*}
1240 ["filterExpression (X = 3 / (z - 1/4 + -1/8 * (1/(z::real))))",
1241 "stepResponse (x[n::real]::bool)"];
1243 ("Isac", ["Inverse", "Z_Transform", "SignalProcessing"],
1244 ["SignalProcessing","Z_Transform","Inverse"]);
1251 Const ("Inverse_Z_Transform.filterExpression", _),
1252 [Const ("HOL.eq", _) $ _ $ _]
1258 Const ("Inverse_Z_Transform.stepResponse", _),
1262 ) = prep_ori fmz thy ((#ppc o get_pbt) pI);
1265 = (#scr o get_met) ["SignalProcessing",
1271 subsubsection {*Stepwise Check the Program\label{sec:stepcheck}*}
1272 text{*\noindent We start to stepwise execute our new program in a calculation
1273 tree and check if every node implements that what we have wanted.*}
1276 trace_rewrite := false; (*true*)
1277 trace_script := false; (*true*)
1281 ["filterExpression (X z = 3 / ((z::real) + 1/10 - 1/50*(1/z)))",
1282 "stepResponse (x[n::real]::bool)"];
1285 ("Isac", ["Inverse", "Z_Transform", "SignalProcessing"],
1286 ["SignalProcessing","Z_Transform","Inverse"]);
1288 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI,pI,mI))];
1289 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1291 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1293 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1295 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1297 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1299 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1301 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1302 "Rewrite (ruleZY, Inverse_Z_Transform.ruleZY)";
1303 "--> X z = 3 / (z - 1 / 4 + -1 / 8 * (1 / z))";
1307 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1308 "Rewrite_Set norm_Rational";
1309 " --> X' z = 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))";
1310 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1315 text {*\noindent Instead of \ttfamily nxt = Subproblem \normalfont above we had
1316 \ttfamily Empty\_Tac; \normalfont the search for the reason considered
1317 the following points:\begin{itemize}
1318 \item What shows \ttfamily show\_pt pt;\normalfont\ldots?
1319 \begin{verbatim}(([2], Res), ?X' z = 24 / (-1 + -2 * z + 8 * z ^^^ 2))]\end{verbatim}
1320 The calculation is ok but no \ttfamily next \normalfont step found:
1321 Should be\\ \ttfamily nxt = Subproblem\normalfont!
1322 \item What shows \ttfamily trace\_script := true; \normalfont we read
1325 @@@next leaf 'SubProblem
1326 (PolyEq',[abcFormula, degree_2, polynomial,
1327 univariate, equation], no_meth)
1329 ---> STac 'SubProblem (PolyEq',
1330 [abcFormula, degree_2, polynomial,
1331 univariate, equation], no_meth)
1332 [BOOL (-1 + -2 * z + 8 * z \^\^\^ ~2 = 0), REAL z]'
1334 We see the SubProblem with correct arguments from searching next
1335 step (program text !!!--->!!! STac (script tactic) with arguments
1337 \item Do we have the right Script \ldots difference in the
1338 arguments in the arguments\ldots
1341 (#scr o get_met) ["SignalProcessing",
1344 writeln (term2str s);
1346 \ldots shows the right script. Difference in the arguments.
1347 \item Test --- Why helpless here ? --- shows: \ttfamily replace
1348 no\_meth by [no\_meth] \normalfont in Script
1353 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1357 text {*\noindent Instead of \ttfamily nxt = Model\_Problem \normalfont above
1358 we had \ttfamily Empty\_Tac; \normalfont the search for the reason
1359 considered the following points:\begin{itemize}
1360 \item Difference in the arguments
1361 \item Comparison with Subsection~\ref{sec:solveq}: There solving this
1362 equation works, so there must be some difference in the arguments
1363 of the Subproblem: RIGHT: we had \ttfamily [no\_meth] \normalfont
1364 instead of \ttfamily [no\_met] \normalfont ;-)
1368 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1369 (*Add_Given equality (-1 + -2 * z + 8 * z ^^^ 2 = 0)";*)
1370 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1371 (*Add_Given solveFor z";*)
1372 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1373 (*Add_Find solutions z_i";*)
1374 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1375 (*Specify_Theory Isac";*)
1378 text {*\noindent We had \ttfamily nxt = Empty\_Tac instead Specify\_Theory;
1379 \normalfont The search for the reason considered the following points:
1381 \item Was there an error message? NO -- ok
1382 \item Has \ttfamily nxt = Add\_Find \normalfont been inserted in pt:\\
1383 \ttfamily get\_obj g\_pbl pt (fst p);\normalfont? YES -- ok
1384 \item What is the returned formula:
1386 print_depth 999; f; print_depth 3;
1387 { Find = [ Correct "solutions z_i"],
1389 Given = [Correct "equality (-1 + -2*z + 8*z ^^^ 2 = 0)",
1390 Correct "solveFor z"],
1394 \normalfont The only False is the reason: the Where (the precondition) is
1395 False for good reasons: The precondition seems to check for linear
1396 equations, not for the one we want to solve! Removed this error by
1397 correcting the Script from \ttfamily SubProblem (PolyEq',
1398 \lbrack linear,univariate,equation,
1399 test\rbrack, \lbrack Test,solve\_linear\rbrack \normalfont to
1400 \ttfamily SubProblem (PolyEq',\\ \lbrack abcFormula,degree\_2,
1401 polynomial,univariate,equation\rbrack,\\
1402 \lbrack PolyEq,solve\_d2\_polyeq\_abc\_equation
1404 You find the appropriate type of equation at the
1405 {\sisac}-WEB-Page\footnote{
1406 \href{http://www.ist.tugraz.at/projects/isac/www/kbase/pbl/index\_pbl.html}
1407 {http://www.ist.tugraz.at/projects/isac/www/kbase/pbl/index\_pbl.html}
1409 And the respective method in \ttfamily Knowledge/PolyEq.thy \normalfont
1410 at the respective \ttfamily store\_pbt. \normalfont Or you leave the
1411 selection of the appropriate type to isac as done in the final Script ;-))
1415 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1416 (*Specify_Problem [abcFormula,...";*)
1417 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1418 (*Specify_Method [PolyEq,solve_d2_polyeq_abc_equation";*)
1419 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1420 (*Apply_Method [PolyEq,solve_d2_polyeq_abc_equation";*)
1421 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1422 (*Rewrite_Set_Inst ([(bdv, z)], d2_polyeq_abcFormula_simplify";*)
1423 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1424 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1425 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
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 (*Specify_Problem ["normalize","polynomial","univariate","equation"]*)
1441 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1442 (*Specify_Method ["PolyEq", "normalize_poly"]*)
1443 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1444 (*Apply_Method ["PolyEq", "normalize_poly"]*)
1445 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1446 (*Rewrite ("all_left", "PolyEq.all_left")*)
1447 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1448 (*Rewrite_Set_Inst (["(bdv, A)"], "make_ratpoly_in")*)
1449 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1450 (*Rewrite_Set "polyeq_simplify"*)
1451 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1452 (*Subproblem("Isac",["degree_1","polynomial","univariate","equation"])*)
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;
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; (*([11, 4, 5], Res) Check_Postcond*)
1499 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*([11, 4], Res) Check_Postcond*)
1500 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*([11], Res) Take*)
1501 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*([12], Frm) Substitute*)
1502 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*([12], Res) Rewrite*)
1503 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*([13], Res) Take*)
1504 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*([14], Frm) Empty_Tac*)
1507 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1510 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1513 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1516 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1519 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1522 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1526 trace_script := true;
1529 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1547 text{*\noindent As a last step we check the tracing output of the last calc
1548 tree instruction and compare it with the pre-calculated result.*}
1550 section {* Improve and Transfer into Knowledge *}
1552 We want to improve the very long program \ttfamily InverseZTransform
1553 \normalfont by modularisation: partial fraction decomposition shall
1554 become a sub-problem.
1556 We could transfer all knowledge in \ttfamily Build\_Inverse\_Z\_Transform.thy
1557 \normalfont first to the \ttfamily Knowledge/Inverse\_Z\_Transform.thy
1558 \normalfont and then modularise. In this case TODO problems?!?
1560 We chose another way and go bottom up: first we build the sub-problem in
1561 \ttfamily Partial\_Fractions.thy \normalfont with the term:
1563 $$\frac{3}{x\cdot(z - \frac{1}{4} + \frac{-1}{8}\cdot\frac{1}{z})}$$
1565 \noindent (how this still can be improved see \ttfamily Partial\_Fractions.thy\normalfont),
1566 and re-use all stuff prepared in \ttfamily Build\_Inverse\_Z\_Transform.thy:
1567 \normalfont The knowledge will be transferred to \ttfamily src/../Partial\_Fractions.thy
1568 \normalfont and the respective tests to:
1569 \begin{center}\ttfamily test/../sartial\_fractions.sml\normalfont\end{center}
1572 subsection {* Transfer to Partial\_Fractions.thy *}
1574 First we transfer both, knowledge and tests into:
1575 \begin{center}\ttfamily src/../Partial\_Fractions.thy\normalfont\end{center}
1576 in order to immediately have the test results.
1578 We copy \ttfamily factors\_from\_solution, drop\_questionmarks,\\
1579 ansatz\_2nd\_order \normalfont and rule-sets --- no problem.
1581 Also \ttfamily store\_pbt ..\\ "pbl\_simp\_rat\_partfrac"
1582 \normalfont is easy.
1584 But then we copy from:\\
1585 (1) \ttfamily Build\_Inverse\_Z\_Transform.thy store\_met\ldots "met\_SP\_Ztrans\_inv"
1587 (2) \ttfamily Partial\_Fractions.thy store\_met\ldots "met\_SP\_Ztrans\_inv"
1588 \normalfont\\ and cut out the respective part from the program. First we ensure that
1589 the string is correct. When we insert the string into (2)
1590 \ttfamily store\_met .. "met\_partial\_fraction" \normalfont --- and get an error.
1593 subsubsection {* 'Programming' in ISAC's TP-based Language *}
1595 At the present state writing programs in {\sisac} is particularly cumbersome.
1596 So we give hints how to cope with the many obstacles. Below we describe the
1597 steps we did in making (2) run.
1600 \item We check if the \textbf{string} containing the program is correct.
1601 \item We check if the \textbf{types in the program} are correct.
1602 For this purpose we start start with the first and last lines
1604 "PartFracScript (f_f::real) (v_v::real) = " ^
1605 " (let X = Take f_f; " ^
1606 " pbz = ((Substitute []) X) " ^
1609 The last but one line helps not to bother with ';'.
1610 \item Then we add line by line. Already the first line causes the error.
1611 So we investigate it by
1613 val ctxt = Proof_Context.init_global @{theory "Inverse_Z_Transform"} ;
1615 parseNEW ctxt "(num_orig::real) =
1616 get_numerator(rhs f_f)";
1618 and see a type clash: \ttfamily rhs \normalfont from (1) requires type
1619 \ttfamily bool \normalfont while (2) wants to have \ttfamily (f\_f::real).
1620 \normalfont Of course, we don't need \ttfamily rhs \normalfont anymore.
1621 \item Type-checking can be very tedious. One might even inspect the
1622 parse-tree of the program with {\sisac}'s specific debug tools:
1624 val {scr = Prog t,...} =
1625 get_met ["simplification",
1627 "to_partial_fraction"];
1628 atomty_thy @{theory "Inverse_Z_Transform"} t ;
1630 \item We check if the \textbf{semantics of the program} by stepwise evaluation
1631 of the program. Evaluation is done by the Lucas-Interpreter, which works
1632 using the knowledge in theory Isac; so we have to re-build Isac. And the
1633 test are performed simplest in a file which is loaded with Isac.
1634 See \ttfamily tests/../partial\_fractions.sml \normalfont.
1638 subsection {* Transfer to Inverse\_Z\_Transform.thy *}
1640 It was not possible to complete this task, because we ran out of time.