1 (* Title: Build_Inverse_Z_Transform
3 (c) copyright due to license terms.
6 theory Build_Inverse_Z_Transform imports Isac.Inverse_Z_Transform
10 text\<open>We stepwise build \ttfamily Inverse\_Z\_Transform.thy \normalfont as an
11 exercise. Because Subsection~\ref{sec:stepcheck} requires
12 \ttfamily Inverse\_Z\_Transform.thy \normalfont as a subtheory of \ttfamily
13 Isac.thy\normalfont, the setup has been changed from \ttfamily theory
14 Inverse\_Z\_Transform imports Isac \normalfont to the above one.
17 \textbf{Attention with the names of identifiers when going into internals!}
19 Here in this theory there are the internal names twice, for instance we have
20 \ttfamily (Thm.derivation\_name @{thm rule1} =
21 "Build\_Inverse\_Z\_Transform.rule1") = true; \normalfont
22 but actually in us will be \ttfamily Inverse\_Z\_Transform.rule1 \normalfont
25 section \<open>Trials towards the Z-Transform\label{sec:trials}\<close>
27 ML \<open>val thy = @{theory};\<close>
29 subsection \<open>Notations and Terms\<close>
30 text\<open>\noindent Try which notations we are able to use.\<close>
32 @{term "1 < || z ||"};
33 @{term "z / (z - 1)"};
35 @{term "-u [-n - 1]"}; (*[ ] denotes lists !!!*)
36 @{term "z /(z - 1) = -u [-n - 1]"};
37 @{term "1 < || z || ==> z / (z - 1) = -u [-n - 1]"};
38 term2str @{term "1 < || z || ==> z / (z - 1) = -u [-n - 1]"};
40 text\<open>\noindent Try which symbols we are able to use and how we generate them.\<close>
42 (*alpha --> "</alpha>" *)
47 term2str @{term "\<rho> "};
50 subsection \<open>Rules\<close>
51 (*axiomatization "z / (z - 1) = -u [-n - 1]"
52 Illegal variable name: "z / (z - 1) = -u [-n - 1]" *)
53 (*definition "z / (z - 1) = -u [-n - 1]"
54 Bad head of lhs: existing constant "op /"*)
56 rule1: "1 = \<delta>[n]" and
57 rule2: "|| z || > 1 ==> z / (z - 1) = u [n]" and
58 rule3: "|| z || < 1 ==> z / (z - 1) = -u [-n - 1]" and
59 rule4: "|| z || > || \<alpha> || ==> z / (z - \<alpha>) = \<alpha>^^^n * u [n]" and
60 rule5: "|| z || < || \<alpha> || ==> z / (z - \<alpha>) = -(\<alpha>^^^n) * u [-n - 1]" and
61 rule6: "|| z || > 1 ==> z/(z - 1)^^^2 = n * u [n]"
63 text\<open>\noindent Check the rules for their correct notation.
64 (See the machine output.)\<close>
72 subsection \<open>Apply Rules\<close>
73 text\<open>\noindent We try to apply the rules to a given expression.\<close>
76 val inverse_Z = append_rls "inverse_Z" e_rls
77 [ Thm ("rule3",TermC.num_str @{thm rule3}),
78 Thm ("rule4",TermC.num_str @{thm rule4}),
79 Thm ("rule1",TermC.num_str @{thm rule1})
82 val t = TermC.str2term "z / (z - 1) + z / (z - \<alpha>) + 1";
83 val SOME (t', asm) = Rewrite.rewrite_set_ thy true inverse_Z t;
84 term2str t' = "z / (z - ?\<delta> [?n]) + z / (z - \<alpha>) + ?\<delta> [?n]";
86 * Attention rule1 is applied before the expression is
87 * checked for rule4 which would be correct!!!
91 ML \<open>val (thy, ro, er) = (@{theory}, tless_true, eval_rls);\<close>
94 Rewrite.rewrite_ thy ro er true (TermC.num_str @{thm rule3}) t;
95 term2str t = "- ?u [- ?n - 1] + z / (z - \<alpha>) + 1";
100 Rewrite.rewrite_ thy ro er true (TermC.num_str @{thm rule4}) t;
101 term2str t = "- ?u [- ?n - 1] + \<alpha> ^^^ ?n * ?u [?n] + 1";
106 Rewrite.rewrite_ thy ro er true (TermC.num_str @{thm rule1}) t;
107 term2str t = "- ?u [- ?n - 1] + \<alpha> ^^^ ?n * ?u [?n] + ?\<delta> [?n]";
111 ML \<open>terms2str (asm1 @ asm2 @ asm3);\<close>
113 section\<open>Prepare Steps for TP-based programming Language\label{sec:prepstep}\<close>
115 \par \noindent The following sections are challenging with the CTP-based
116 possibilities of building the program. The goal is realized in
117 Section~\ref{spec-meth} and Section~\ref{prog-steps}.
118 \par The reader is advised to jump between the subsequent subsections and
119 the respective steps in Section~\ref{prog-steps}. By comparing
120 Section~\ref{sec:calc:ztrans} the calculation can be comprehended step
124 subsection \<open>Prepare Expression\label{prep-expr}\<close>
125 text\<open>\noindent We try two different notations and check which of them
126 Isabelle can handle best.\<close>
128 val ctxt = Proof_Context.init_global @{theory};
129 val ctxt = Stool.declare_constraints' [@{term "z::real"}] ctxt;
132 TermC.parseNEW ctxt "X z = 3 / (z - 1/4 + -1/8 * z ^^^ -1)"; term2str fun1;
134 TermC.parseNEW ctxt "X z = 3 / (z - 1/4 + -1/8 * (1/z))"; term2str fun1';
137 subsubsection \<open>Prepare Numerator and Denominator\<close>
138 text\<open>\noindent The partial fraction decomposition is only possible if we
139 get the bound variable out of the numerator. Therefor we divide
140 the expression by $z$. Follow up the Calculation at
141 Section~\ref{sec:calc:ztrans} line number 02.\<close>
144 ruleZY: "(X z = a / b) = (X' z = a / (z * b))"
147 val (thy, ro, er) = (@{theory}, tless_true, eval_rls);
148 val SOME (fun2, asm1) =
149 Rewrite.rewrite_ thy ro er true @{thm ruleZY} fun1; term2str fun2;
150 val SOME (fun2', asm1) =
151 Rewrite.rewrite_ thy ro er true @{thm ruleZY} fun1'; term2str fun2';
154 Rewrite.rewrite_set_ @{theory} false norm_Rational fun2;
158 * We solve this problem by using 1/x as a workaround.
161 Rewrite.rewrite_set_ @{theory} false norm_Rational fun2';
168 subsubsection \<open>Get the Argument of the Expression X'\<close>
169 text\<open>\noindent We use \texttt{grep} for finding possibilities how we can
170 extract the bound variable in the expression. \ttfamily Atools.thy,
171 Tools.thy \normalfont contain general utilities: \ttfamily
172 eval\_argument\_in, eval\_rhs, eval\_lhs,\ldots \normalfont
173 \ttfamily grep -r "fun eva\_" * \normalfont shows all functions
174 witch can be used in a script. Lookup this files how to build
175 and handle such functions.
176 \par The next section shows how to introduce such a function.
179 subsubsection\<open>Decompose the Given Term Into lhs and rhs\<close>
181 val (_, expr) = HOLogic.dest_eq fun3'; term2str expr;
183 HOLogic.dest_bin "Rings.divide_class.divide" (type_of expr) expr;
184 term2str denom = "-1 + -2 * z + 8 * z ^^^ 2";
187 text\<open>\noindent We have rhs\footnote{Note: lhs means \em Left Hand Side
188 \normalfont and rhs means \em Right Hand Side \normalfont and indicates
189 the left or the right part of an equation.} in the Script language, but
190 we need a function which gets the denominator of a fraction.\<close>
192 subsubsection\<open>Get the Denominator and Numerator out of a Fraction\<close>
193 text\<open>\noindent The self written functions in e.g. \texttt{get\_denominator}
194 should become a constant for the Isabelle parser:\<close>
197 get_denominator :: "real => real"
198 get_numerator :: "real => real"
200 text \<open>\noindent With the above definition we run into problems when we parse
201 the Script \texttt{InverseZTransform}. This leads to \em ambiguous
202 parse trees. \normalfont We avoid this by moving the definition
203 to \ttfamily Rational.thy \normalfont and re-building {\sisac}.
204 \par \noindent ATTENTION: From now on \ttfamily
205 Build\_Inverse\_Z\_Transform \normalfont mimics a build from scratch;
206 it only works due to re-building {\sisac} several times (indicated
213 * ("Rational.get_denominator", eval_get_denominator ""))
215 fun eval_get_denominator (thmid:string) _
216 (t as Const ("Rational.get_denominator", _) $
217 (Const ("Rings.divide_class.divide", _) $num
219 SOME (TermC.mk_thmid thmid (term_to_string''' thy denom) "",
220 HOLogic.Trueprop $ (TermC.mk_equality (t, denom)))
221 | eval_get_denominator _ _ _ _ = NONE;
223 text \<open>\noindent For the tests of \ttfamily eval\_get\_denominator \normalfont
224 see \ttfamily test/Knowledge/rational.sml\normalfont\<close>
226 text \<open>\noindent \ttfamily get\_numerator \normalfont should also become a
227 constant for the Isabelle parser, follow up the \texttt{const}
228 declaration above.\<close>
233 * ("Rational.get_numerator", eval_get_numerator ""))
235 fun eval_get_numerator (thmid:string) _
236 (t as Const ("Rational.get_numerator", _) $
237 (Const ("Rings.divide_class.divide", _) $num
239 SOME (TermC.mk_thmid thmid (term_to_string''' thy num) "",
240 HOLogic.Trueprop $ (TermC.mk_equality (t, num)))
241 | eval_get_numerator _ _ _ _ = NONE;
244 text \<open>\noindent We discovered several problems by implementing the
245 \ttfamily get\_numerator \normalfont function. Remember when
246 putting new functions to {\sisac}, put them in a thy file and rebuild
247 {\sisac}, also put them in the ruleset for the script!\<close>
249 subsection \<open>Solve Equation\label{sec:solveq}\<close>
250 text \<open>\noindent We have to find the zeros of the term, therefor we use our
251 \ttfamily get\_denominator \normalfont function from the step before
252 and try to solve the second order equation. (Follow up the Calculation
253 in Section~\ref{sec:calc:ztrans} Subproblem 2) Note: This type of
254 equation is too general for the present program.
255 \par We know that this equation can be categorized as \em univariate
256 equation \normalfont and solved with the functions {\sisac} provides
257 for this equation type. Later on {\sisac} should determine the type
258 of the given equation self.\<close>
260 val denominator = TermC.parseNEW ctxt "z^^^2 - 1/4*z - 1/8 = 0";
261 val fmz = ["equality (z^^^2 - 1/4*z - 1/8 = (0::real))",
264 val (dI',pI',mI') =("Isac", ["univariate","equation"], ["no_met"]);
266 text \<open>\noindent Check if the given equation matches the specification of this
267 equation type.\<close>
269 Specify.match_pbl fmz (Specify.get_pbt ["univariate","equation"]);
272 text\<open>\noindent We switch up to the {\sisac} Context and try to solve the
273 equation with a more specific type definition.\<close>
276 Context.theory_name thy = "Isac";
277 val denominator = TermC.parseNEW ctxt "-1 + -2 * z + 8 * z ^^^ 2 = 0";
278 val fmz = (*specification*)
279 ["equality (-1 + -2 * z + 8 * z ^^^ 2 = (0::real))",(*equality*)
280 "solveFor z", (*bound variable*)
281 "solutions L"]; (*identifier for
285 ["abcFormula","degree_2","polynomial","univariate","equation"],
289 text \<open>\noindent Check if the (other) given equation matches the
290 specification of this equation type.\<close>
293 Specify.match_pbl fmz (Specify.get_pbt
294 ["abcFormula","degree_2","polynomial","univariate","equation"]);
297 text \<open>\noindent We stepwise solve the equation. This is done by the
298 use of a so called calc tree seen downwards.\<close>
301 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
302 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
303 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
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;
315 * nxt =..,Check_elementwise "Assumptions")
317 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
318 val (p,_,f,nxt,_,pt) = me nxt p [] pt; f2str f;
320 * [z = 1 / 2, z = -1 / 4]
323 val SOME f = parseNEW ctxt "[z=1/2, z=-1/4]";
326 subsection \<open>Partial Fraction Decomposition\label{sec:pbz}\<close>
327 text\<open>\noindent We go on with the decomposition of our expression. Follow up the
328 Calculation in Section~\ref{sec:calc:ztrans} Step~3 and later on
329 Subproblem~1.\<close>
330 subsubsection \<open>Solutions of the Equation\<close>
331 text\<open>\noindent We get the solutions of the before solved equation in a list.\<close>
334 val SOME solutions = parseNEW ctxt "[z=1/2, z=-1/4]";
339 subsubsection \<open>Get Solutions out of a List\<close>
340 text \<open>\noindent In {\sisac}'s TP-based programming language:
342 let $ $ s_1 = NTH 1 $ solutions; $ s_2 = NTH 2... $
348 val Const ("List.list.Cons", _) $ s_1 $ (Const ("List.list.Cons", _)
349 $ s_2 $ Const ("List.list.Nil", _)) = solutions;
354 text\<open>\noindent The ansatz for the \em Partial Fraction Decomposition \normalfont
355 requires to get the denominators of the partial fractions out of the
358 \item $Denominator_{1}=z-Zeropoint_{1}$
359 \item $Denominator_{2}=z-Zeropoint_{2}$
365 val xx = HOLogic.dest_eq s_1;
366 val s_1' = HOLogic.mk_binop "Groups.minus_class.minus" xx;
367 val xx = HOLogic.dest_eq s_2;
368 val s_2' = HOLogic.mk_binop "Groups.minus_class.minus" xx;
373 text \<open>\noindent For the programming language a function collecting all the
374 above manipulations is helpful.\<close>
378 let val (lhs, rhs) = HOLogic.dest_eq s
379 in HOLogic.mk_binop "Groups.minus_class.minus" (lhs, rhs) end;
383 fun mk_prod prod [] =
385 then error "mk_prod called with []"
387 | mk_prod prod (t :: []) =
390 else HOLogic.mk_binop "Groups.times_class.times" (prod, t)
391 | mk_prod prod (t1 :: t2 :: ts) =
395 HOLogic.mk_binop "Groups.times_class.times" (t1, t2)
399 HOLogic.mk_binop "Groups.times_class.times" (prod, t1)
400 in mk_prod p (t2 :: ts) end
403 probably keep these test in test/Tools/isac/...
404 (*mk_prod e_term [];*)
406 val prod = mk_prod e_term [str2term "x + 123"];
407 term2str prod = "x + 123";
409 val sol = str2term "[z = 1 / 2, z = -1 / 4]";
410 val sols = HOLogic.dest_list sol;
411 val facs = map fac_from_sol sols;
412 val prod = mk_prod e_term facs;
413 term2str prod = "(z + -1 * (1 / 2)) * (z + -1 * (-1 / 4))";
416 mk_prod e_term [str2term "x + 1", str2term "x + 2", str2term "x + 3"];
417 term2str prod = "(x + 1) * (x + 2) * (x + 3)";
420 fun factors_from_solution sol =
421 let val ts = HOLogic.dest_list sol
422 in mk_prod e_term (map fac_from_sol ts) end;
425 val sol = str2term "[z = 1 / 2, z = -1 / 4]";
426 val fs = factors_from_solution sol;
427 term2str fs = "(z + -1 * (1 / 2)) * (z + -1 * (-1 / 4))"
429 text \<open>\noindent This function needs to be packed such that it can be evaluated
430 by the Lucas-Interpreter. Therefor we moved the function to the
431 corresponding \ttfamily Equation.thy \normalfont in our case
432 \ttfamily PartialFractions.thy \normalfont. The necessary steps
433 are quit the same as we have done with \ttfamily get\_denominator
434 \normalfont before.\<close>
436 (*("factors_from_solution",
437 ("Partial_Fractions.factors_from_solution",
438 eval_factors_from_solution ""))*)
440 fun eval_factors_from_solution (thmid:string) _
441 (t as Const ("Partial_Fractions.factors_from_solution", _) $ sol)
442 thy = ((let val prod = factors_from_solution sol
443 in SOME (mk_thmid thmid "" (term_to_string''' thy prod) "",
444 Trueprop $ (mk_equality (t, prod)))
447 | eval_factors_from_solution _ _ _ _ = NONE;
450 text \<open>\noindent The tracing output of the calc tree after applying this
453 24 / factors_from_solution [z = 1/ 2, z = -1 / 4])]
457 val nxt = ("Empty_Tac", ...): tac'_)
459 These observations indicate, that the Lucas-Interpreter (LIP)
460 does not know how to evaluate \ttfamily factors\_from\_solution
461 \normalfont, so we knew that there is something wrong or missing.
464 text\<open>\noindent First we isolate the difficulty in the program as follows:
466 " (L_L::bool list) = (SubProblem (PolyEqX, " ^
467 " [abcFormula, degree_2, polynomial, " ^
468 " univariate,equation], " ^
470 " [BOOL equ, REAL zzz]); " ^
471 " (facs::real) = factors_from_solution L_L; " ^
472 " (foo::real) = Take facs " ^
475 \par \noindent And see the tracing output:
478 [(([], Frm), Problem (Isac, [inverse,
481 (([1], Frm), X z = 3 / (z - 1 / 4 + -1 / 8 * (1 / z))),
482 (([1], Res), ?X' z = 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))),
483 (([2], Res), ?X' z = 24 / (-1 + -2 * z + 8 * z ^^^ 2)),
484 (([3], Pbl), solve (-1 + -2 * z + 8 * z ^^^ 2 = 0, z)),
485 (([3,1], Frm), -1 + -2 * z + 8 * z ^^^ 2 = 0),
486 (([3,1], Res), z = (- -2 + sqrt (-2 ^^^ 2 - 4 * 8 * -1)) / (2 * 8)|
487 z = (- -2 - sqrt (-2 ^^^ 2 - 4 * 8 * -1)) / (2 * 8)),
488 (([3,2], Res), z = 1 / 2 | z = -1 / 4),
489 (([3,3], Res), [ z = 1 / 2, z = -1 / 4]),
490 (([3,4], Res), [ z = 1 / 2, z = -1 / 4]),
491 (([3], Res), [ z = 1 / 2, z = -1 / 4]),
492 (([4], Frm), factors_from_solution [z = 1 / 2, z = -1 / 4])]
495 \par \noindent In particular that:
498 (([3], Pbl), solve (-1 + -2 * z + 8 * z ^^^ 2 = 0, z)),
500 \par \noindent Shows the equation which has been created in
503 "(denom::real) = get_denominator funterm; " ^
504 (* get_denominator *)
505 "(equ::bool) = (denom = (0::real)); " ^
508 \noindent \ttfamily get\_denominator \normalfont has been evaluated successfully,
509 but not\\ \ttfamily factors\_from\_solution.\normalfont
510 So we stepwise compare with an analogous case, \ttfamily get\_denominator
511 \normalfont successfully done above: We know that LIP evaluates
512 expressions in the program by use of the \emph{srls}, so we try to get
513 the original \emph{srls}.\\
516 val {srls,...} = get_met ["SignalProcessing",
521 \par \noindent Create 2 good example terms:
525 parseNEW ctxt "get_denominator ((111::real) / 222)";
527 parseNEW ctxt "factors_from_solution [(z::real)=1/2, z=-1/4]";
530 \par \noindent Rewrite the terms using srls:\\
531 \ttfamily \par \noindent rewrite\_set\_ thy true srls t1;\\
532 rewrite\_set\_ thy true srls t2;\\
533 \par \noindent \normalfont Now we see a difference: \texttt{t1} gives
534 \texttt{SOME} but \texttt{t2} gives \texttt{NONE}. We look at the
538 Rls{id = "srls_InverseZTransform",
539 rules = [Calc("Rational.get_numerator",
540 eval_get_numerator "Rational.get_numerator"),
541 Calc("Partial_Fractions.factors_from_solution",
542 eval_factors_from_solution
543 "Partial_Fractions.factors_from_solution")]}
545 \par \noindent Here everthing is perfect. So the error can
546 only be in the SML code of \ttfamily eval\_factors\_from\_solution.
547 \normalfont We try to check the code with an existing test; since the
549 \begin{center}\ttfamily src/Tools/isac/Knowledge/Partial\_Fractions.thy
550 \normalfont\end{center}
551 the \emph{test} should be in
552 \begin{center}\ttfamily test/Tools/isac/Knowledge/partial\_fractions.sml
553 \normalfont\end{center}
554 \par \noindent After updating the function \ttfamily
555 factors\_from\_solution \normalfont to a new version and putting a
556 test-case to \ttfamily Partial\_Fractions.sml \normalfont we tried again
557 to evaluate the term with the same result.
558 \par We opened the test \ttfamily Test\_Isac.thy \normalfont and saw that
559 everything is working fine. Also we checked that the test \ttfamily
560 partial\_fractions.sml \normalfont is used in \ttfamily Test\_Isac.thy
562 \begin{center}use \ttfamily "Knowledge/partial\_fractions.sml"
563 \normalfont \end{center}
564 and \ttfamily Partial\_Fractions.thy \normalfont is part is part of
565 {\sisac} by evaluating
568 val thy = @{theory "Inverse_Z_Transform"};
571 After rebuilding {\sisac} again it worked.
574 subsubsection \<open>Build Expression\<close>
575 text \<open>\noindent In {\sisac}'s TP-based programming language we can build
577 \ttfamily let s\_1 = Take numerator / (s\_1 * s\_2) \normalfont\<close>
581 * The main denominator is the multiplication of the denominators of
582 * all partial fractions.
585 val denominator' = HOLogic.mk_binop
586 "Groups.times_class.times" (s_1', s_2') ;
587 val SOME numerator = parseNEW ctxt "3::real";
589 val expr' = HOLogic.mk_binop
590 "Rings.divide_class.divide" (numerator, denominator');
594 subsubsection \<open>Apply the Partial Fraction Decomposion Ansatz\<close>
596 text\<open>\noindent We use the Ansatz of the Partial Fraction Decomposition for our
597 expression 2nd order. Follow up the calculation in
598 Section~\ref{sec:calc:ztrans} Step~03.\<close>
600 ML \<open>Context.theory_name thy = "Isac"\<close>
602 text\<open>\noindent We define two axiomatization, the first one is the main ansatz,
603 the next one is just an equivalent transformation of the resulting
604 equation. Both axiomatizations were moved to \ttfamily
605 Partial\_Fractions.thy \normalfont and got their own rulesets. In later
606 programs it is possible to use the rulesets and the machine will find
607 the correct ansatz and equivalent transformation itself.\<close>
610 ansatz_2nd_order: "n / (a*b) = A/a + B/b" and
611 equival_trans_2nd_order: "(n/(a*b) = A/a + B/b) = (n = A*b + B*a)"
613 text\<open>\noindent We use our \ttfamily ansatz\_2nd\_order \normalfont to rewrite
614 our expression and get an equation with our expression on the left
615 and the partial fractions of it on the right hand side.\<close>
619 rewrite_ @{theory} e_rew_ord e_rls false
620 @{thm ansatz_2nd_order} expr';
621 term2str t1; atomty t1;
622 val eq1 = HOLogic.mk_eq (expr', t1);
626 text\<open>\noindent Eliminate the denominators by multiplying the left and the
627 right hand side of the equation with the main denominator. This is an
628 simple equivalent transformation. Later on we use an own ruleset
629 defined in \ttfamily Partial\_Fractions.thy \normalfont for doing this.
630 Follow up the calculation in Section~\ref{sec:calc:ztrans} Step~04.\<close>
634 rewrite_ @{theory} e_rew_ord e_rls false
635 @{thm equival_trans_2nd_order} eq1;
639 text\<open>\noindent We use the existing ruleset \ttfamily norm\_Rational \normalfont
640 for simplifications on expressions.\<close>
643 val SOME (eq3,_) = rewrite_set_ @{theory} false norm_Rational eq2;
646 * ?A ?B not simplified
650 text\<open>\noindent In Example~\ref{eg:gap} of my thesis I'm describing a problem about
651 simplifications. The problem that we would like to have only a specific degree
652 of simplification occurs right here, in the next step.\<close>
655 trace_rewrite := false;
657 parseNEW ctxt "(z - 1/2)*(z - -1/4) * (A/(z - 1/2) + B/(z - -1/4))";
661 val SOME (fract2,_) =
662 rewrite_set_ @{theory} false norm_Rational fract1;
663 term2str fract2 = "(A + -2 * B + 4 * A * z + 4 * B * z) / 4";
665 * term2str fract2 = "A * (1 / 4 + z) + B * (-1 / 2 + z)"
666 * would be more traditional...
670 text\<open>\noindent We walk around this problem by generating our new equation first.\<close>
673 val (numerator, denominator) = HOLogic.dest_eq eq3;
674 val eq3' = HOLogic.mk_eq (numerator, fract1);
680 * MANDATORY: simplify (and remove denominator) otherwise 3 = 0
682 val SOME (eq3'' ,_) =
683 rewrite_set_ @{theory} false norm_Rational eq3';
687 text\<open>\noindent Still working at {\sisac}\ldots\<close>
689 ML \<open>Context.theory_name thy = "Isac"\<close>
691 subsubsection \<open>Build a Rule-Set for the Ansatz\<close>
692 text \<open>\noindent The \emph{ansatz} rules violate the principle that each
693 variable on the right-hand-side must also occur on the
694 left-hand-side of the rule: A, B, etc. don't do that. Thus the
695 rewriter marks these variables with question marks: ?A, ?B, etc.
696 These question marks can be dropped by \ttfamily fun
697 drop\_questionmarks\normalfont.\<close>
700 val ansatz_rls = prep_rls @{theory} (
701 Rls {id = "ansatz_rls", preconds = [], rew_ord = ("dummy_ord",dummy_ord),
702 erls = e_rls, srls = Erls, calc = [], errpatts = [],
704 Thm ("ansatz_2nd_order",num_str @{thm ansatz_2nd_order}),
705 Thm ("equival_trans_2nd_order",num_str @{thm equival_trans_2nd_order})
710 text\<open>\noindent We apply the ruleset\ldots\<close>
714 rewrite_set_ @{theory} false ansatz_rls expr';
717 text\<open>\noindent And check the output\ldots\<close>
720 term2str expr' = "3 / ((z - 1 / 2) * (z - -1 / 4))";
721 term2str ttttt = "?A / (z - 1 / 2) + ?B / (z - -1 / 4)";
724 subsubsection \<open>Get the First Coefficient\<close>
726 text\<open>\noindent Now it's up to get the two coefficients A and B, which will be
727 the numerators of our partial fractions. Continue following up the
728 Calculation in Section~\ref{sec:calc:ztrans} Subproblem~1.\<close>
730 text\<open>\noindent To get the first coefficient we substitute $z$ with the first
731 zero-point we determined in Section~\ref{sec:solveq}.\<close>
735 rewrite_terms_ @{theory} e_rew_ord e_rls [s_1] eq3'';
738 rewrite_set_ @{theory} false norm_Rational eq4_1;
741 val fmz = ["equality (3=3*A/(4::real))", "solveFor A","solutions L"];
742 val (dI',pI',mI') =("Isac", ["univariate","equation"], ["no_met"]);
744 * Solve the simple linear equation for A:
745 * Return eq, not list of eq's
747 val (p,_,fa,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
748 val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
749 (*Add_Given "equality (3=3*A/4)"*)
750 val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
751 (*Add_Given "solveFor A"*)
752 val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
753 (*Add_Find "solutions L"*)
754 val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
755 (*Specify_Theory "Isac"*)
756 val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
757 (*Specify_Problem ["normalise","polynomial",
758 "univariate","equation"])*)
759 val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
760 (* Specify_Method["PolyEq","normalise_poly"]*)
761 val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
762 (*Apply_Method["PolyEq","normalise_poly"]*)
763 val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
764 (*Rewrite ("all_left","PolyEq.all_left")*)
765 val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
766 (*Rewrite_Set_Inst(["(''bdv'',A)"],"make_ratpoly_in")*)
767 val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
768 (*Rewrite_Set "polyeq_simplify"*)
769 val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
770 val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
771 val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
772 (*Add_Given "equality (3 + -3 / 4 * A =0)"*)
773 val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
774 (*Add_Given "solveFor A"*)
775 val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
776 (*Add_Find "solutions A_i"*)
777 val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
778 val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
779 val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
780 val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
781 (*Apply_Method ["PolyEq","solve_d1_polyeq_equation"]*)
782 val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
783 (*Rewrite_Set_Inst(["(''bdv'',A)"],"d1_polyeq_simplify")*)
784 val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
785 (*Rewrite_Set "polyeq_simplify"*)
786 val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
787 (*Rewrite_Set "norm_Rational_parenthesized"*)
788 val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
790 val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
791 (*Check_elementwise "Assumptions"*)
792 val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
793 (*Check_Postcond ["degree_1","polynomial",
794 "univariate","equation"]*)
795 val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
796 (*Check_Postcond ["normalise","polynomial",
797 "univariate","equation"]*)
798 val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
803 subsubsection \<open>Get Second Coefficient\<close>
805 text\<open>\noindent With the use of \texttt{thy} we check which theories the
806 interpreter knows.\<close>
808 ML \<open>thy\<close>
810 text\<open>\noindent To get the second coefficient we substitute $z$ with the second
811 zero-point we determined in Section~\ref{sec:solveq}.\<close>
814 val SOME (eq4b_1,_) =
815 rewrite_terms_ @{theory} e_rew_ord e_rls [s_2] eq3'';
817 val SOME (eq4b_2,_) =
818 rewrite_set_ @{theory} false norm_Rational eq4b_1;
821 val fmz = ["equality (3= -3*B/(4::real))", "solveFor B","solutions L"];
822 val (dI',pI',mI') =("Isac", ["univariate","equation"], ["no_met"]);
823 val (p,_,fb,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
824 val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
825 val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
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;
854 text\<open>\noindent We compare our results with the pre calculated upshot.\<close>
857 if f2str fa = "[A = 4]" then () else error "part.fract. eq4_1";
858 if f2str fb = "[B = -4]" then () else error "part.fract. eq4_1";
861 section \<open>Implement the Specification and the Method \label{spec-meth}\<close>
863 text\<open>\noindent Now everything we need for solving the problem has been
864 tested out. We now start by creating new nodes for our methods and
865 further on our new program in the interpreter.\<close>
867 subsection\<open>Define the Field Descriptions for the
868 Specification\label{sec:deffdes}\<close>
870 text\<open>\noindent We define the fields \em filterExpression \normalfont and
871 \em stepResponse \normalfont both as equations, they represent the in- and
872 output of the program.\<close>
875 filterExpression :: "bool => una"
876 stepResponse :: "bool => una"
878 subsection\<open>Define the Specification\<close>
880 text\<open>\noindent The next step is defining the specifications as nodes in the
881 designated part. We have to create the hierarchy node by node and start
882 with \em SignalProcessing \normalfont and go on by creating the node
883 \em Z\_Transform\normalfont.\<close>
885 setup \<open>KEStore_Elems.add_pbts
886 [prep_pbt thy "pbl_SP" [] e_pblID (["SignalProcessing"], [], e_rls, NONE, []),
887 prep_pbt thy "pbl_SP_Ztrans" [] e_pblID
888 (["Z_Transform","SignalProcessing"], [], e_rls, NONE, [])]\<close>
890 text\<open>\noindent For the suddenly created node we have to define the input
891 and output parameters. We already prepared their definition in
892 Section~\ref{sec:deffdes}.\<close>
894 setup \<open>KEStore_Elems.add_pbts
895 [prep_pbt thy "pbl_SP_Ztrans_inv" [] e_pblID
896 (["Inverse", "Z_Transform", "SignalProcessing"],
897 [("#Given", ["filterExpression X_eq"]),
898 ("#Find", ["stepResponse n_eq"])],
899 append_rls "e_rls" e_rls [(*for preds in where_*)],
901 [["SignalProcessing","Z_Transform","Inverse"]])]\<close>
904 get_pbt ["Inverse","Z_Transform","SignalProcessing"];
907 subsection \<open>Define Name and Signature for the Method\<close>
909 text\<open>\noindent As a next step we store the definition of our new method as a
910 constant for the interpreter.\<close>
913 InverseZTransform :: "[bool, bool] => bool"
914 ("((Script InverseZTransform (_ =))// (_))" 9)
916 subsection \<open>Setup Parent Nodes in Hierarchy of Method\label{sec:cparentnode}\<close>
918 text\<open>\noindent Again we have to generate the nodes step by step, first the
919 parent node and then the originally \em Z\_Transformation
920 \normalfont node. We have to define both nodes first with an empty script
923 setup \<open>KEStore_Elems.add_mets
924 [prep_met thy "met_SP" [] e_metID
925 (["SignalProcessing"], [],
926 {rew_ord'="tless_true", rls'= e_rls, calc = [], srls = e_rls, prls = e_rls, crls = e_rls,
927 errpats = [], nrls = e_rls},
929 prep_met thy "met_SP_Ztrans" [] e_metID
930 (["SignalProcessing", "Z_Transform"], [],
931 {rew_ord'="tless_true", rls'= e_rls, calc = [], srls = e_rls, prls = e_rls, crls = e_rls,
932 errpats = [], nrls = e_rls},
936 text\<open>\noindent After we generated both nodes, we can fill the containing
937 script we want to implement later. First we define the specifications
938 of the script in e.g. the in- and output.\<close>
940 setup \<open>KEStore_Elems.add_mets
941 [prep_met thy "met_SP_Ztrans_inv" [] e_metID
942 (["SignalProcessing", "Z_Transform", "Inverse"],
943 [("#Given" ,["filterExpression X_eq"]), ("#Find" ,["stepResponse n_eq"])],
944 {rew_ord'="tless_true", rls'= e_rls, calc = [], srls = e_rls, prls = e_rls, crls = e_rls,
945 errpats = [], nrls = e_rls},
949 text\<open>\noindent After we stored the definition we can start implementing the
950 script itself. As a first try we define only three rows containing one
951 simple operation.\<close>
953 setup \<open>KEStore_Elems.add_mets
954 [prep_met thy "met_SP_Ztrans_inv" [] e_metID
955 (["SignalProcessing", "Z_Transform", "Inverse"],
956 [("#Given" ,["filterExpression X_eq"]), ("#Find" ,["stepResponse n_eq"])],
957 {rew_ord'="tless_true", rls'= e_rls, calc = [], srls = e_rls, prls = e_rls, crls = e_rls,
958 errpats = [], nrls = e_rls},
959 "Script InverseZTransform (Xeq::bool) =" ^
960 " (let X = Take Xeq;" ^
961 " X = Rewrite ruleZY False X" ^
965 text\<open>\noindent Check if the method has been stored correctly\ldots\<close>
971 text\<open>\noindent If yes we can get the method by stepping backwards through
972 the hierarchy.\<close>
975 get_met ["SignalProcessing","Z_Transform","Inverse"];
978 section \<open>Program in TP-based language \label{prog-steps}\<close>
980 text\<open>\noindent We start stepwise expanding our program. The script is a
981 simple string containing several manipulation instructions.
982 \par The first script we try contains no instruction, we only test if
983 building scripts that way work.\<close>
985 subsection \<open>Stepwise Extend the Program\<close>
988 "Script InverseZTransform (Xeq::bool) = "^
992 text\<open>\noindent Next we put some instructions in the script and try if we are
993 able to solve our first equation.\<close>
997 "Script InverseZTransform (Xeq::bool) = "^
999 * 1/z) instead of z ^^^ -1
1001 " (let X = Take Xeq; "^
1002 " X' = Rewrite ruleZY False X; "^
1006 " X' = (Rewrite_Set norm_Rational False) X' "^
1014 "Script InverseZTransform (Xeq::bool) = "^
1016 * (1/z) instead of z ^^^ -1
1018 " (let X = Take Xeq; "^
1019 " X' = Rewrite ruleZY False X; "^
1023 " X' = (Rewrite_Set norm_Rational False) X'; "^
1027 " X' = (SubProblem (IsacX,[pqFormula,degree_2, "^
1028 " polynomial,univariate,equation], "^
1030 " [BOOL e_e, REAL v_v]) "^
1034 text\<open>\noindent To solve the equation it is necessary to drop the left hand
1035 side, now we only need the denominator of the right hand side. The first
1036 equation solves the zeros of our expression.\<close>
1040 "Script InverseZTransform (Xeq::bool) = "^
1041 " (let X = Take Xeq; "^
1042 " X' = Rewrite ruleZY False X; "^
1043 " X' = (Rewrite_Set norm_Rational False) X'; "^
1044 " funterm = rhs X' "^
1046 * drop X'= for equation solving
1051 text\<open>\noindent As mentioned above, we need the denominator of the right hand
1052 side. The equation itself consists of this denominator and tries to find
1053 a $z$ for this the denominator is equal to zero.\<close>
1057 "Script InverseZTransform (X_eq::bool) = "^
1058 " (let X = Take X_eq; "^
1059 " X' = Rewrite ruleZY False X; "^
1060 " X' = (Rewrite_Set norm_Rational False) X'; "^
1061 " (X'_z::real) = lhs X'; "^
1062 " (z::real) = argument_in X'_z; "^
1063 " (funterm::real) = rhs X'; "^
1064 " (denom::real) = get_denominator funterm; "^
1068 " (equ::bool) = (denom = (0::real)); "^
1069 " (L_L::bool list) = "^
1070 " (SubProblem (TestX, "^
1071 " [LINEAR,univariate,equation,test], "^
1072 " [Test,solve_linear]) "^
1073 " [BOOL equ, REAL z]) "^
1077 val sc = (inst_abs o Thm.term_of o the o (parse thy)) str;
1081 text \<open>\noindent This ruleset contains all functions that are in the script;
1082 The evaluation of the functions is done by rewriting using this ruleset.\<close>
1086 Rls {id="srls_InverseZTransform",
1088 rew_ord = ("termlessI",termlessI),
1089 erls = append_rls "erls_in_srls_InverseZTransform" e_rls
1090 [(*for asm in NTH_CONS ...*)
1091 Calc ("Orderings.ord_class.less",eval_equ "#less_"),
1092 (*2nd NTH_CONS pushes n+-1 into asms*)
1093 Calc("Groups.plus_class.plus", eval_binop "#add_")
1095 srls = Erls, calc = [], errpatts = [],
1097 Thm ("NTH_CONS",num_str @{thm NTH_CONS}),
1098 Calc("Groups.plus_class.plus",
1099 eval_binop "#add_"),
1100 Thm ("NTH_NIL",num_str @{thm NTH_NIL}),
1101 Calc("Tools.lhs", eval_lhs"eval_lhs_"),
1102 Calc("Tools.rhs", eval_rhs"eval_rhs_"),
1103 Calc("Atools.argument'_in",
1104 eval_argument_in "Atools.argument'_in"),
1105 Calc("Rational.get_denominator",
1106 eval_get_denominator "#get_denominator"),
1107 Calc("Rational.get_numerator",
1108 eval_get_numerator "#get_numerator"),
1109 Calc("Partial_Fractions.factors_from_solution",
1110 eval_factors_from_solution
1111 "#factors_from_solution"),
1112 Calc("Partial_Fractions.drop_questionmarks",
1113 eval_drop_questionmarks "#drop_?")
1119 subsection \<open>Store Final Version of Program for Execution\<close>
1121 text\<open>\noindent After we also tested how to write scripts and run them,
1122 we start creating the final version of our script and store it into
1123 the method for which we created a node in Section~\ref{sec:cparentnode}
1124 Note that we also did this stepwise, but we didn't kept every
1127 setup \<open>KEStore_Elems.add_mets
1128 [prep_met thy "met_SP_Ztrans_inv" [] e_metID
1129 (["SignalProcessing", "Z_Transform", "Inverse"],
1130 [("#Given" ,["filterExpression X_eq"]), ("#Find" ,["stepResponse n_eq"])],
1131 {rew_ord'="tless_true", rls'= e_rls, calc = [], srls = srls, prls = e_rls, crls = e_rls,
1132 errpats = [], nrls = e_rls},
1133 "Script InverseZTransform (X_eq::bool) = "^
1134 (*(1/z) instead of z ^^^ -1*)
1135 "(let X = Take X_eq; "^
1136 " X' = Rewrite ruleZY False X; "^
1138 " (num_orig::real) = get_numerator (rhs X'); "^
1139 " X' = (Rewrite_Set norm_Rational False) X'; "^
1141 " (X'_z::real) = lhs X'; "^
1142 " (zzz::real) = argument_in X'_z; "^
1143 " (funterm::real) = rhs X'; "^
1144 (*drop X' z = for equation solving*)
1145 " (denom::real) = get_denominator funterm; "^
1147 " (num::real) = get_numerator funterm; "^
1149 " (equ::bool) = (denom = (0::real)); "^
1150 " (L_L::bool list) = (SubProblem (PolyEqX, "^
1151 " [abcFormula,degree_2,polynomial,univariate,equation], "^
1153 " [BOOL equ, REAL zzz]); "^
1154 " (facs::real) = factors_from_solution L_L; "^
1155 " (eql::real) = Take (num_orig / facs); "^
1157 " (eqr::real) = (Try (Rewrite_Set ansatz_rls False)) eql; "^
1159 " (eq::bool) = Take (eql = eqr); "^
1160 (*Maybe possible to use HOLogic.mk_eq ??*)
1161 " eq = (Try (Rewrite_Set equival_trans False)) eq; "^
1163 " eq = drop_questionmarks eq; "^
1164 " (z1::real) = (rhs (NTH 1 L_L)); "^
1166 * prepare equation for a - eq_a
1167 * therefor substitute z with solution 1 - z1
1169 " (z2::real) = (rhs (NTH 2 L_L)); "^
1171 " (eq_a::bool) = Take eq; "^
1172 " eq_a = (Substitute [zzz=z1]) eq; "^
1173 " eq_a = (Rewrite_Set norm_Rational False) eq_a; "^
1174 " (sol_a::bool list) = "^
1175 " (SubProblem (IsacX, "^
1176 " [univariate,equation],[no_met]) "^
1177 " [BOOL eq_a, REAL (A::real)]); "^
1178 " (a::real) = (rhs(NTH 1 sol_a)); "^
1180 " (eq_b::bool) = Take eq; "^
1181 " eq_b = (Substitute [zzz=z2]) eq_b; "^
1182 " eq_b = (Rewrite_Set norm_Rational False) eq_b; "^
1183 " (sol_b::bool list) = "^
1184 " (SubProblem (IsacX, "^
1185 " [univariate,equation],[no_met]) "^
1186 " [BOOL eq_b, REAL (B::real)]); "^
1187 " (b::real) = (rhs(NTH 1 sol_b)); "^
1189 " eqr = drop_questionmarks eqr; "^
1190 " (pbz::real) = Take eqr; "^
1191 " pbz = ((Substitute [A=a, B=b]) pbz); "^
1193 " pbz = Rewrite ruleYZ False pbz; "^
1194 " pbz = drop_questionmarks pbz; "^
1196 " (X_z::bool) = Take (X_z = pbz); "^
1197 " (n_eq::bool) = (Rewrite_Set inverse_z False) X_z; "^
1198 " n_eq = drop_questionmarks n_eq "^
1203 subsection \<open>Check the Program\<close>
1204 text\<open>\noindent When the script is ready we can start checking our work.\<close>
1205 subsubsection \<open>Check the Formalization\<close>
1206 text\<open>\noindent First we want to check the formalization of the in and
1207 output of our program.\<close>
1211 ["filterExpression (X = 3 / (z - 1/4 + -1/8 * (1/(z::real))))",
1212 "stepResponse (x[n::real]::bool)"];
1214 ("Isac", ["Inverse", "Z_Transform", "SignalProcessing"],
1215 ["SignalProcessing","Z_Transform","Inverse"]);
1222 Const ("Inverse_Z_Transform.filterExpression", _),
1223 [Const ("HOL.eq", _) $ _ $ _]
1229 Const ("Inverse_Z_Transform.stepResponse", _),
1233 ) = prep_ori fmz thy ((#ppc o get_pbt) pI);
1236 = (#scr o get_met) ["SignalProcessing",
1242 subsubsection \<open>Stepwise Check the Program\label{sec:stepcheck}\<close>
1243 text\<open>\noindent We start to stepwise execute our new program in a calculation
1244 tree and check if every node implements that what we have wanted.\<close>
1247 trace_rewrite := false; (*true*)
1248 trace_script := false; (*true*)
1252 ["filterExpression (X z = 3 / ((z::real) + 1/10 - 1/50*(1/z)))",
1253 "stepResponse (x[n::real]::bool)"];
1256 ("Isac", ["Inverse", "Z_Transform", "SignalProcessing"],
1257 ["SignalProcessing","Z_Transform","Inverse"]);
1259 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI,pI,mI))];
1260 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1262 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1264 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1266 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1268 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1270 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1272 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1273 "Rewrite (ruleZY, Inverse_Z_Transform.ruleZY)";
1274 "--> X z = 3 / (z - 1 / 4 + -1 / 8 * (1 / z))";
1278 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1279 "Rewrite_Set norm_Rational";
1280 " --> X' z = 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))";
1281 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1286 text \<open>\noindent Instead of \ttfamily nxt = Subproblem \normalfont above we had
1287 \ttfamily Empty\_Tac; \normalfont the search for the reason considered
1288 the following points:\begin{itemize}
1289 \item What shows \ttfamily show\_pt pt;\normalfont\ldots?
1290 \begin{verbatim}(([2], Res), ?X' z = 24 / (-1 + -2 * z + 8 * z ^^^ 2))]\end{verbatim}
1291 The calculation is ok but no \ttfamily next \normalfont step found:
1292 Should be\\ \ttfamily nxt = Subproblem\normalfont!
1293 \item What shows \ttfamily trace\_script := true; \normalfont we read
1296 @@@next leaf 'SubProblem
1297 (PolyEq',[abcFormula, degree_2, polynomial,
1298 univariate, equation], no_meth)
1300 ---> STac 'SubProblem (PolyEq',
1301 [abcFormula, degree_2, polynomial,
1302 univariate, equation], no_meth)
1303 [BOOL (-1 + -2 * z + 8 * z \^\^\^ ~2 = 0), REAL z]'
1305 We see the SubProblem with correct arguments from searching next
1306 step (program text !!!--->!!! STac (script tactic) with arguments
1308 \item Do we have the right Script \ldots difference in the
1309 arguments in the arguments\ldots
1312 (#scr o get_met) ["SignalProcessing",
1315 writeln (term2str s);
1317 \ldots shows the right script. Difference in the arguments.
1318 \item Test --- Why helpless here ? --- shows: \ttfamily replace
1319 no\_meth by [no\_meth] \normalfont in Script
1324 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1328 text \<open>\noindent Instead of \ttfamily nxt = Model\_Problem \normalfont above
1329 we had \ttfamily Empty\_Tac; \normalfont the search for the reason
1330 considered the following points:\begin{itemize}
1331 \item Difference in the arguments
1332 \item Comparison with Subsection~\ref{sec:solveq}: There solving this
1333 equation works, so there must be some difference in the arguments
1334 of the Subproblem: RIGHT: we had \ttfamily [no\_meth] \normalfont
1335 instead of \ttfamily [no\_met] \normalfont ;-)
1336 \end{itemize}\<close>
1339 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1340 (*Add_Given equality (-1 + -2 * z + 8 * z ^^^ 2 = 0)";*)
1341 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1342 (*Add_Given solveFor z";*)
1343 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1344 (*Add_Find solutions z_i";*)
1345 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1346 (*Specify_Theory Isac";*)
1349 text \<open>\noindent We had \ttfamily nxt = Empty\_Tac instead Specify\_Theory;
1350 \normalfont The search for the reason considered the following points:
1352 \item Was there an error message? NO -- ok
1353 \item Has \ttfamily nxt = Add\_Find \normalfont been inserted in pt:\\
1354 \ttfamily get\_obj g\_pbl pt (fst p);\normalfont? YES -- ok
1355 \item What is the returned formula:
1357 print_depth 999; f; print_depth 3;
1358 { Find = [ Correct "solutions z_i"],
1360 Given = [Correct "equality (-1 + -2*z + 8*z ^^^ 2 = 0)",
1361 Correct "solveFor z"],
1365 \normalfont The only False is the reason: the Where (the precondition) is
1366 False for good reasons: The precondition seems to check for linear
1367 equations, not for the one we want to solve! Removed this error by
1368 correcting the Script from \ttfamily SubProblem (PolyEq',
1369 \lbrack linear,univariate,equation,
1370 test\rbrack, \lbrack Test,solve\_linear\rbrack \normalfont to
1371 \ttfamily SubProblem (PolyEq',\\ \lbrack abcFormula,degree\_2,
1372 polynomial,univariate,equation\rbrack,\\
1373 \lbrack PolyEq,solve\_d2\_polyeq\_abc\_equation
1375 You find the appropriate type of equation at the
1376 {\sisac}-WEB-Page\footnote{
1377 \href{http://www.ist.tugraz.at/projects/isac/www/kbase/pbl/index\_pbl.html}
1378 {http://www.ist.tugraz.at/projects/isac/www/kbase/pbl/index\_pbl.html}
1380 And the respective method in \ttfamily Knowledge/PolyEq.thy \normalfont
1381 at the respective \ttfamily store\_pbt. \normalfont Or you leave the
1382 selection of the appropriate type to isac as done in the final Script ;-))
1383 \end{itemize}\<close>
1386 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1387 (*Specify_Problem [abcFormula,...";*)
1388 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1389 (*Specify_Method [PolyEq,solve_d2_polyeq_abc_equation";*)
1390 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1391 (*Apply_Method [PolyEq,solve_d2_polyeq_abc_equation";*)
1392 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1393 (*Rewrite_Set_Inst [(''bdv'', z)], d2_polyeq_abcFormula_simplify";*)
1394 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1395 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1396 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1397 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1398 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1399 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1400 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1401 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1402 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1403 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1404 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1405 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1406 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1407 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1408 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1409 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1410 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1411 (*Specify_Problem ["normalise","polynomial","univariate","equation"]*)
1412 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1413 (*Specify_Method ["PolyEq", "normalise_poly"]*)
1414 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1415 (*Apply_Method ["PolyEq", "normalise_poly"]*)
1416 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1417 (*Rewrite ("all_left", "PolyEq.all_left")*)
1418 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1419 (*Rewrite_Set_Inst (["(''bdv'', A)"], "make_ratpoly_in")*)
1420 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1421 (*Rewrite_Set "polyeq_simplify"*)
1422 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1423 (*Subproblem("Isac",["degree_1","polynomial","univariate","equation"])*)
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 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1441 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1442 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1443 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1444 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1445 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1446 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1447 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1448 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1449 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1450 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1451 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1452 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1453 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1454 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1455 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1456 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1457 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1458 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1459 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1460 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1461 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1462 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1463 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1464 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1465 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1466 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1467 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1468 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1469 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*([11, 4, 5], Res) Check_Postcond*)
1470 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*([11, 4], Res) Check_Postcond*)
1471 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*([11], Res) Take*)
1472 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*([12], Frm) Substitute*)
1473 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*([12], Res) Rewrite*)
1474 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*([13], Res) Take*)
1475 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*([14], Frm) Empty_Tac*)
1478 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1481 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1484 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1487 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1490 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1493 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1497 trace_script := true;
1500 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1518 text\<open>\noindent As a last step we check the tracing output of the last calc
1519 tree instruction and compare it with the pre-calculated result.\<close>
1521 section \<open>Improve and Transfer into Knowledge\<close>
1523 We want to improve the very long program \ttfamily InverseZTransform
1524 \normalfont by modularisation: partial fraction decomposition shall
1525 become a sub-problem.
1527 We could transfer all knowledge in \ttfamily Build\_Inverse\_Z\_Transform.thy
1528 \normalfont first to the \ttfamily Knowledge/Inverse\_Z\_Transform.thy
1529 \normalfont and then modularise. In this case TODO problems?!?
1531 We chose another way and go bottom up: first we build the sub-problem in
1532 \ttfamily Partial\_Fractions.thy \normalfont with the term:
1534 $$\frac{3}{x\cdot(z - \frac{1}{4} + \frac{-1}{8}\cdot\frac{1}{z})}$$
1536 \noindent (how this still can be improved see \ttfamily Partial\_Fractions.thy\normalfont),
1537 and re-use all stuff prepared in \ttfamily Build\_Inverse\_Z\_Transform.thy:
1538 \normalfont The knowledge will be transferred to \ttfamily src/../Partial\_Fractions.thy
1539 \normalfont and the respective tests to:
1540 \begin{center}\ttfamily test/../sartial\_fractions.sml\normalfont\end{center}
1543 subsection \<open>Transfer to Partial\_Fractions.thy\<close>
1545 First we transfer both, knowledge and tests into:
1546 \begin{center}\ttfamily src/../Partial\_Fractions.thy\normalfont\end{center}
1547 in order to immediately have the test results.
1549 We copy \ttfamily factors\_from\_solution, drop\_questionmarks,\\
1550 ansatz\_2nd\_order \normalfont and rule-sets --- no problem.
1552 Also \ttfamily store\_pbt ..\\ "pbl\_simp\_rat\_partfrac"
1553 \normalfont is easy.
1555 But then we copy from:\\
1556 (1) \ttfamily Build\_Inverse\_Z\_Transform.thy store\_met\ldots "met\_SP\_Ztrans\_inv"
1558 (2) \ttfamily Partial\_Fractions.thy store\_met\ldots "met\_SP\_Ztrans\_inv"
1559 \normalfont\\ and cut out the respective part from the program. First we ensure that
1560 the string is correct. When we insert the string into (2)
1561 \ttfamily store\_met .. "met\_partial\_fraction" \normalfont --- and get an error.
1564 subsubsection \<open>'Programming' in ISAC's TP-based Language\<close>
1566 At the present state writing programs in {\sisac} is particularly cumbersome.
1567 So we give hints how to cope with the many obstacles. Below we describe the
1568 steps we did in making (2) run.
1571 \item We check if the \textbf{string} containing the program is correct.
1572 \item We check if the \textbf{types in the program} are correct.
1573 For this purpose we start start with the first and last lines
1575 "PartFracScript (f_f::real) (v_v::real) = " ^
1576 " (let X = Take f_f; " ^
1577 " pbz = ((Substitute []) X) " ^
1580 The last but one line helps not to bother with ';'.
1581 \item Then we add line by line. Already the first line causes the error.
1582 So we investigate it by
1584 val ctxt = Proof_Context.init_global @{theory "Inverse_Z_Transform"} ;
1586 parseNEW ctxt "(num_orig::real) =
1587 get_numerator(rhs f_f)";
1589 and see a type clash: \ttfamily rhs \normalfont from (1) requires type
1590 \ttfamily bool \normalfont while (2) wants to have \ttfamily (f\_f::real).
1591 \normalfont Of course, we don't need \ttfamily rhs \normalfont anymore.
1592 \item Type-checking can be very tedious. One might even inspect the
1593 parse-tree of the program with {\sisac}'s specific debug tools:
1595 val {scr = Prog t,...} =
1596 get_met ["simplification",
1598 "to_partial_fraction"];
1599 atomty_thy @{theory "Inverse_Z_Transform"} t ;
1601 \item We check if the \textbf{semantics of the program} by stepwise evaluation
1602 of the program. Evaluation is done by the Lucas-Interpreter, which works
1603 using the knowledge in theory Isac; so we have to re-build Isac. And the
1604 test are performed simplest in a file which is loaded with Isac.
1605 See \ttfamily tests/../partial\_fractions.sml \normalfont.
1609 subsection \<open>Transfer to Inverse\_Z\_Transform.thy\<close>
1611 It was not possible to complete this task, because we ran out of time.