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 UnparseC.term @{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 UnparseC.term @{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> \<up> n * u [n]" and
60 rule5: "|| z || < || \<alpha> || ==> z / (z - \<alpha>) = -(\<alpha> \<up> n) * u [-n - 1]" and
61 rule6: "|| z || > 1 ==> z/(z - 1) \<up> 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 = Rule_Set.append_rules "inverse_Z" Rule_Set.empty
77 [ Thm ("rule3",ThmC.numerals_to_Free @{thm rule3}),
78 Thm ("rule4",ThmC.numerals_to_Free @{thm rule4}),
79 Thm ("rule1",ThmC.numerals_to_Free @{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 UnparseC.term 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 (ThmC.numerals_to_Free @{thm rule3}) t;
95 UnparseC.term t = "- ?u [- ?n - 1] + z / (z - \<alpha>) + 1";
100 Rewrite.rewrite_ thy ro er true (ThmC.numerals_to_Free @{thm rule4}) t;
101 UnparseC.term t = "- ?u [- ?n - 1] + \<alpha> \<up> ?n * ?u [?n] + 1";
106 Rewrite.rewrite_ thy ro er true (ThmC.numerals_to_Free @{thm rule1}) t;
107 UnparseC.term t = "- ?u [- ?n - 1] + \<alpha> \<up> ?n * ?u [?n] + ?\<delta> [?n]";
111 ML \<open>UnparseC.terms (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 = ContextC.declare_constraints' [@{term "z::real"}] ctxt;*)
132 TermC.parseNEW ctxt "X z = 3 / (z - 1/4 + -1/8 * z \<up> -1)"; UnparseC.term fun1;
134 TermC.parseNEW ctxt "X z = 3 / (z - 1/4 + -1/8 * (1/z))"; UnparseC.term 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; UnparseC.term fun2;
150 val SOME (fun2', asm1) =
151 Rewrite.rewrite_ thy ro er true @{thm ruleZY} fun1'; UnparseC.term fun2';
154 Rewrite.rewrite_set_ @{theory} false norm_Rational fun2;
157 * Fails on x \<up> (-1)
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 Prog_Expr.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'; UnparseC.term expr;
183 HOLogic.dest_bin "Rings.divide_class.divide" (type_of expr) expr;
184 UnparseC.term denom = "-1 + -2 * z + 8 * z \<up> 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 Program 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 Program \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 (UnparseC.term_in_thy 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 (UnparseC.term_in_thy 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 \<up> 2 - 1/4*z - 1/8 = 0";
261 val fmz = ["equality (z \<up> 2 - 1/4*z - 1/8 = (0::real))",
264 val (dI',pI',mI') =("Isac_Knowledge", ["univariate", "equation"], ["no_met"]);
266 text \<open>\noindent Check if the given equation matches the specification of this
267 equation type.\<close>
269 M_Match.match_pbl fmz (Problem.from_store ["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_Knowledge";
277 val denominator = TermC.parseNEW ctxt "-1 + -2 * z + 8 * z \<up> 2 = 0";
278 val fmz = (*specification*)
279 ["equality (-1 + -2 * z + 8 * z \<up> 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 M_Match.match_pbl fmz (Problem.from_store
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]
322 Test_Tool.show_pt pt;
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]";
335 UnparseC.term solutions;
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 [] =
384 if prod = TermC.empty
385 then error "mk_prod called with []"
387 | mk_prod prod (t :: []) =
388 if prod = TermC.empty
390 else HOLogic.mk_binop "Groups.times_class.times" (prod, t)
391 | mk_prod prod (t1 :: t2 :: ts) =
392 if prod = TermC.empty
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 TermC.empty [];*)
406 val prod = mk_prod TermC.empty [str2term "x + 123"];
407 UnparseC.term 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 TermC.empty facs;
413 UnparseC.term prod = "(z + -1 * (1 / 2)) * (z + -1 * (-1 / 4))";
416 mk_prod TermC.empty [str2term "x + 1", str2term "x + 2", str2term "x + 3"];
417 UnparseC.term 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 TermC.empty (map fac_from_sol ts) end;
425 val sol = str2term "[z = 1 / 2, z = -1 / 4]";
426 val fs = factors_from_solution sol;
427 UnparseC.term 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) thy =
442 let val prod = factors_from_solution sol
443 in SOME (TermC.mk_thmid thmid (UnparseC.term_in_thy thy prod) "",
444 HOLogic.Trueprop $ (TermC.mk_equality (t, prod)))
446 | eval_factors_from_solution _ _ _ _ = NONE;
449 text \<open>\noindent The tracing output of the calc tree after applying this
452 24 / factors_from_solution [z = 1/ 2, z = -1 / 4])]
456 val nxt = ("Empty_Tac", ...): tac'_)
458 These observations indicate, that the Lucas-Interpreter (LIP)
459 does not know how to evaluate \ttfamily factors\_from\_solution
460 \normalfont, so we knew that there is something wrong or missing.
463 text\<open>\noindent First we isolate the difficulty in the program as follows:
465 " (L_L::bool list) = (SubProblem (PolyEqX, " ^
466 " [abcFormula, degree_2, polynomial, " ^
467 " univariate,equation], " ^
469 " [BOOL equ, REAL zzz]); " ^
470 " (facs::real) = factors_from_solution L_L; " ^
471 " (foo::real) = Take facs " ^
474 \par \noindent And see the tracing output:
477 [(([], Frm), Problem (Isac, [inverse,
480 (([1], Frm), X z = 3 / (z - 1 / 4 + -1 / 8 * (1 / z))),
481 (([1], Res), ?X' z = 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))),
482 (([2], Res), ?X' z = 24 / (-1 + -2 * z + 8 * z \<up> 2)),
483 (([3], Pbl), solve (-1 + -2 * z + 8 * z \<up> 2 = 0, z)),
484 (([3,1], Frm), -1 + -2 * z + 8 * z \<up> 2 = 0),
485 (([3,1], Res), z = (- -2 + sqrt (-2 \<up> 2 - 4 * 8 * -1)) / (2 * 8)|
486 z = (- -2 - sqrt (-2 \<up> 2 - 4 * 8 * -1)) / (2 * 8)),
487 (([3,2], Res), z = 1 / 2 | z = -1 / 4),
488 (([3,3], Res), [ z = 1 / 2, z = -1 / 4]),
489 (([3,4], Res), [ z = 1 / 2, z = -1 / 4]),
490 (([3], Res), [ z = 1 / 2, z = -1 / 4]),
491 (([4], Frm), factors_from_solution [z = 1 / 2, z = -1 / 4])]
494 \par \noindent In particular that:
497 (([3], Pbl), solve (-1 + -2 * z + 8 * z \<up> 2 = 0, z)),
499 \par \noindent Shows the equation which has been created in
502 "(denom::real) = get_denominator funterm; " ^
503 (* get_denominator *)
504 "(equ::bool) = (denom = (0::real)); " ^
507 \noindent \ttfamily get\_denominator \normalfont has been evaluated successfully,
508 but not\\ \ttfamily factors\_from\_solution.\normalfont
509 So we stepwise compare with an analogous case, \ttfamily get\_denominator
510 \normalfont successfully done above: We know that LIP evaluates
511 expressions in the program by use of the \emph{srls}, so we try to get
512 the original \emph{srls}.\\
515 val {srls,...} = MethodC.from_store ["SignalProcessing",
520 \par \noindent Create 2 good example terms:
524 parseNEW ctxt "get_denominator ((111::real) / 222)";
526 parseNEW ctxt "factors_from_solution [(z::real)=1/2, z=-1/4]";
529 \par \noindent Rewrite the terms using srls:\\
530 \ttfamily \par \noindent rewrite\_set\_ thy true srls t1;\\
531 rewrite\_set\_ thy true srls t2;\\
532 \par \noindent \normalfont Now we see a difference: \texttt{t1} gives
533 \texttt{SOME} but \texttt{t2} gives \texttt{NONE}. We look at the
537 Rule_Set.Repeat{id = "srls_InverseZTransform",
538 rules = [Eval("Rational.get_numerator",
539 eval_get_numerator "Rational.get_numerator"),
540 Eval("Partial_Fractions.factors_from_solution",
541 eval_factors_from_solution
542 "Partial_Fractions.factors_from_solution")]}
544 \par \noindent Here everthing is perfect. So the error can
545 only be in the SML code of \ttfamily eval\_factors\_from\_solution.
546 \normalfont We try to check the code with an existing test; since the
548 \begin{center}\ttfamily src/Tools/isac/Knowledge/Partial\_Fractions.thy
549 \normalfont\end{center}
550 the \emph{test} should be in
551 \begin{center}\ttfamily test/Tools/isac/Knowledge/partial\_fractions.sml
552 \normalfont\end{center}
553 \par \noindent After updating the function \ttfamily
554 factors\_from\_solution \normalfont to a new version and putting a
555 test-case to \ttfamily Partial\_Fractions.sml \normalfont we tried again
556 to evaluate the term with the same result.
557 \par We opened the test \ttfamily Test\_Isac.thy \normalfont and saw that
558 everything is working fine. Also we checked that the test \ttfamily
559 partial\_fractions.sml \normalfont is used in \ttfamily Test\_Isac.thy
561 \begin{center}use \ttfamily "Knowledge/partial\_fractions.sml"
562 \normalfont \end{center}
563 and \ttfamily Partial\_Fractions.thy \normalfont is part is part of
564 {\sisac} by evaluating
567 val thy = @{theory "Inverse_Z_Transform"};
570 After rebuilding {\sisac} again it worked.
573 subsubsection \<open>Build Expression\<close>
574 text \<open>\noindent In {\sisac}'s TP-based programming language we can build
576 \ttfamily let s\_1 = Take numerator / (s\_1 * s\_2) \normalfont\<close>
580 * The main denominator is the multiplication of the denominators of
581 * all partial fractions.
584 val denominator' = HOLogic.mk_binop
585 "Groups.times_class.times" (s_1', s_2') ;
586 val SOME numerator = parseNEW ctxt "3::real";
588 val expr' = HOLogic.mk_binop
589 "Rings.divide_class.divide" (numerator, denominator');
593 subsubsection \<open>Apply the Partial Fraction Decomposion Ansatz\<close>
595 text\<open>\noindent We use the Ansatz of the Partial Fraction Decomposition for our
596 expression 2nd order. Follow up the calculation in
597 Section~\ref{sec:calc:ztrans} Step~03.\<close>
599 ML \<open>Context.theory_name thy = "Isac_Knowledge"\<close>
601 text\<open>\noindent We define two axiomatization, the first one is the main ansatz,
602 the next one is just an equivalent transformation of the resulting
603 equation. Both axiomatizations were moved to \ttfamily
604 Partial\_Fractions.thy \normalfont and got their own rulesets. In later
605 programs it is possible to use the rulesets and the machine will find
606 the correct ansatz and equivalent transformation itself.\<close>
609 ansatz_2nd_order: "n / (a*b) = A/a + B/b" and
610 equival_trans_2nd_order: "(n/(a*b) = A/a + B/b) = (n = A*b + B*a)"
612 text\<open>\noindent We use our \ttfamily ansatz\_2nd\_order \normalfont to rewrite
613 our expression and get an equation with our expression on the left
614 and the partial fractions of it on the right hand side.\<close>
618 rewrite_ @{theory} e_rew_ord Rule_Set.empty false
619 @{thm ansatz_2nd_order} expr';
620 UnparseC.term t1; atomty t1;
621 val eq1 = HOLogic.mk_eq (expr', t1);
625 text\<open>\noindent Eliminate the denominators by multiplying the left and the
626 right hand side of the equation with the main denominator. This is an
627 simple equivalent transformation. Later on we use an own ruleset
628 defined in \ttfamily Partial\_Fractions.thy \normalfont for doing this.
629 Follow up the calculation in Section~\ref{sec:calc:ztrans} Step~04.\<close>
633 rewrite_ @{theory} e_rew_ord Rule_Set.empty false
634 @{thm equival_trans_2nd_order} eq1;
638 text\<open>\noindent We use the existing ruleset \ttfamily norm\_Rational \normalfont
639 for simplifications on expressions.\<close>
642 val SOME (eq3,_) = rewrite_set_ @{theory} false norm_Rational eq2;
645 * ?A ?B not simplified
649 text\<open>\noindent In Example~\ref{eg:gap} of my thesis I'm describing a problem about
650 simplifications. The problem that we would like to have only a specific degree
651 of simplification occurs right here, in the next step.\<close>
654 Rewrite.trace_on := false;
656 parseNEW ctxt "(z - 1/2)*(z - -1/4) * (A/(z - 1/2) + B/(z - -1/4))";
660 val SOME (fract2,_) =
661 rewrite_set_ @{theory} false norm_Rational fract1;
662 UnparseC.term fract2 = "(A + -2 * B + 4 * A * z + 4 * B * z) / 4";
664 * UnparseC.term fract2 = "A * (1 / 4 + z) + B * (-1 / 2 + z)"
665 * would be more traditional...
669 text\<open>\noindent We walk around this problem by generating our new equation first.\<close>
672 val (numerator, denominator) = HOLogic.dest_eq eq3;
673 val eq3' = HOLogic.mk_eq (numerator, fract1);
679 * MANDATORY: simplify (and remove denominator) otherwise 3 = 0
681 val SOME (eq3'' ,_) =
682 rewrite_set_ @{theory} false norm_Rational eq3';
686 text\<open>\noindent Still working at {\sisac}\ldots\<close>
688 ML \<open>Context.theory_name thy = "Isac_Knowledge"\<close>
690 subsubsection \<open>Build a Rule-Set for the Ansatz\<close>
691 text \<open>\noindent The \emph{ansatz} rules violate the principle that each
692 variable on the right-hand-side must also occur on the
693 left-hand-side of the rule: A, B, etc. don't do that. Thus the
694 rewriter marks these variables with question marks: ?A, ?B, etc.
695 These question marks can be dropped by \ttfamily fun
696 drop\_questionmarks\normalfont.\<close>
699 val ansatz_rls = prep_rls @{theory} (
700 Rule_Set.Repeat {id = "ansatz_rls", preconds = [], rew_ord = ("dummy_ord",dummy_ord),
701 erls = Rule_Set.empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
703 Thm ("ansatz_2nd_order",ThmC.numerals_to_Free @{thm ansatz_2nd_order}),
704 Thm ("equival_trans_2nd_order",ThmC.numerals_to_Free @{thm equival_trans_2nd_order})
709 text\<open>\noindent We apply the ruleset\ldots\<close>
713 rewrite_set_ @{theory} false ansatz_rls expr';
716 text\<open>\noindent And check the output\ldots\<close>
719 UnparseC.term expr' = "3 / ((z - 1 / 2) * (z - -1 / 4))";
720 UnparseC.term ttttt = "?A / (z - 1 / 2) + ?B / (z - -1 / 4)";
723 subsubsection \<open>Get the First Coefficient\<close>
725 text\<open>\noindent Now it's up to get the two coefficients A and B, which will be
726 the numerators of our partial fractions. Continue following up the
727 Calculation in Section~\ref{sec:calc:ztrans} Subproblem~1.\<close>
729 text\<open>\noindent To get the first coefficient we substitute $z$ with the first
730 zero-point we determined in Section~\ref{sec:solveq}.\<close>
734 rewrite_terms_ @{theory} e_rew_ord Rule_Set.empty [s_1] eq3'';
737 rewrite_set_ @{theory} false norm_Rational eq4_1;
740 val fmz = ["equality (3=3*A/(4::real))", "solveFor A", "solutions L"];
741 val (dI',pI',mI') =("Isac_Knowledge", ["univariate", "equation"], ["no_met"]);
743 * Solve the simple linear equation for A:
744 * Return eq, not list of eq's
746 val (p,_,fa,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
747 val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
748 (*Add_Given "equality (3=3*A/4)"*)
749 val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
750 (*Add_Given "solveFor A"*)
751 val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
752 (*Add_Find "solutions L"*)
753 val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
754 (*Specify_Theory "Isac_Knowledge"*)
755 val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
756 (*Specify_Problem ["normalise", "polynomial",
757 "univariate", "equation"])*)
758 val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
759 (* Specify_Method["PolyEq", "normalise_poly"]*)
760 val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
761 (*Apply_Method["PolyEq", "normalise_poly"]*)
762 val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
763 (*Rewrite ("all_left", "PolyEq.all_left")*)
764 val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
765 (*Rewrite_Set_Inst(["(''bdv'',A)"],"make_ratpoly_in")*)
766 val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
767 (*Rewrite_Set "polyeq_simplify"*)
768 val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
769 val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
770 val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
771 (*Add_Given "equality (3 + -3 / 4 * A =0)"*)
772 val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
773 (*Add_Given "solveFor A"*)
774 val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
775 (*Add_Find "solutions A_i"*)
776 val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
777 val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
778 val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
779 val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
780 (*Apply_Method ["PolyEq", "solve_d1_polyeq_equation"]*)
781 val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
782 (*Rewrite_Set_Inst(["(''bdv'',A)"],"d1_polyeq_simplify")*)
783 val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
784 (*Rewrite_Set "polyeq_simplify"*)
785 val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
786 (*Rewrite_Set "norm_Rational_parenthesized"*)
787 val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
789 val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
790 (*Check_elementwise "Assumptions"*)
791 val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
792 (*Check_Postcond ["degree_1", "polynomial",
793 "univariate", "equation"]*)
794 val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
795 (*Check_Postcond ["normalise", "polynomial",
796 "univariate", "equation"]*)
797 val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
802 subsubsection \<open>Get Second Coefficient\<close>
804 text\<open>\noindent With the use of \texttt{thy} we check which theories the
805 interpreter knows.\<close>
807 ML \<open>thy\<close>
809 text\<open>\noindent To get the second coefficient we substitute $z$ with the second
810 zero-point we determined in Section~\ref{sec:solveq}.\<close>
813 val SOME (eq4b_1,_) =
814 rewrite_terms_ @{theory} e_rew_ord Rule_Set.empty [s_2] eq3'';
815 UnparseC.term eq4b_1;
816 val SOME (eq4b_2,_) =
817 rewrite_set_ @{theory} false norm_Rational eq4b_1;
818 UnparseC.term eq4b_2;
820 val fmz = ["equality (3= -3*B/(4::real))", "solveFor B", "solutions L"];
821 val (dI',pI',mI') =("Isac_Knowledge", ["univariate", "equation"], ["no_met"]);
822 val (p,_,fb,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
823 val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
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;
853 text\<open>\noindent We compare our results with the pre calculated upshot.\<close>
856 if f2str fa = "[A = 4]" then () else error "part.fract. eq4_1";
857 if f2str fb = "[B = -4]" then () else error "part.fract. eq4_1";
860 section \<open>Implement the Specification and the MethodC \label{spec-meth}\<close>
862 text\<open>\noindent Now everything we need for solving the problem has been
863 tested out. We now start by creating new nodes for our methods and
864 further on our new program in the interpreter.\<close>
866 subsection\<open>Define the Field Descriptions for the
867 Specification\label{sec:deffdes}\<close>
869 text\<open>\noindent We define the fields \em filterExpression \normalfont and
870 \em stepResponse \normalfont both as equations, they represent the in- and
871 output of the program.\<close>
874 filterExpression :: "bool => una"
875 stepResponse :: "bool => una"
877 subsection\<open>Define the Specification\<close>
879 text\<open>\noindent The next step is defining the specifications as nodes in the
880 designated part. We have to create the hierarchy node by node and start
881 with \em SignalProcessing \normalfont and go on by creating the node
882 \em Z\_Transform\normalfont.\<close>
884 setup \<open>KEStore_Elems.add_pbts
885 [Problem.prep_input thy "pbl_SP" [] Problem.id_empty (["SignalProcessing"], [], Rule_Set.empty, NONE, []),
886 Problem.prep_input thy "pbl_SP_Ztrans" [] Problem.id_empty
887 (["Z_Transform", "SignalProcessing"], [], Rule_Set.empty, NONE, [])]\<close>
889 text\<open>\noindent For the suddenly created node we have to define the input
890 and output parameters. We already prepared their definition in
891 Section~\ref{sec:deffdes}.\<close>
893 setup \<open>KEStore_Elems.add_pbts
894 [Problem.prep_input thy "pbl_SP_Ztrans_inv" [] Problem.id_empty
895 (["Inverse", "Z_Transform", "SignalProcessing"],
896 [("#Given" ,["filterExpression X_eq"]),
897 ("#Find", ["stepResponse n_eq"])],
898 Rule_Set.append_rules "empty" Rule_Set.empty [(*for preds in where_*)],
900 [["SignalProcessing", "Z_Transform", "Inverse"]])]\<close>
902 Test_Tool.show_ptyps() ();
903 Problem.from_store ["Inverse", "Z_Transform", "SignalProcessing"];
906 subsection \<open>Define Name and Signature for the MethodC\<close>
908 text\<open>\noindent As a next step we store the definition of our new method as a
909 constant for the interpreter.\<close>
912 InverseZTransform :: "[bool, bool] => bool"
913 ("((Program InverseZTransform (_ =))// (_))" 9)
915 subsection \<open>Setup Parent Nodes in Hierarchy of MethodC\label{sec:cparentnode}\<close>
917 text\<open>\noindent Again we have to generate the nodes step by step, first the
918 parent node and then the originally \em Z\_Transformation
919 \normalfont node. We have to define both nodes first with an empty script
922 setup \<open>KEStore_Elems.add_mets
923 [MethodC.prep_input thy "met_SP" [] e_metID
924 (["SignalProcessing"], [],
925 {rew_ord'="tless_true", rls'= Rule_Set.empty, calc = [], srls = Rule_Set.empty, prls = Rule_Set.empty, crls = Rule_Set.empty,
926 errpats = [], nrls = Rule_Set.empty},
928 MethodC.prep_input thy "met_SP_Ztrans" [] e_metID
929 (["SignalProcessing", "Z_Transform"], [],
930 {rew_ord'="tless_true", rls'= Rule_Set.empty, calc = [], srls = Rule_Set.empty, prls = Rule_Set.empty, crls = Rule_Set.empty,
931 errpats = [], nrls = Rule_Set.empty},
935 text\<open>\noindent After we generated both nodes, we can fill the containing
936 script we want to implement later. First we define the specifications
937 of the script in e.g. the in- and output.\<close>
939 setup \<open>KEStore_Elems.add_mets
940 [MethodC.prep_input thy "met_SP_Ztrans_inv" [] e_metID
941 (["SignalProcessing", "Z_Transform", "Inverse"],
942 [("#Given" ,["filterExpression X_eq", "boundVariable X_z"]),
943 ("#Find", ["stepResponse n_eq"])],
944 {rew_ord'="tless_true", rls'= Rule_Set.empty, calc = [], srls = Rule_Set.empty, prls = Rule_Set.empty, crls = Rule_Set.empty,
945 errpats = [], nrls = Rule_Set.empty},
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 [MethodC.prep_input thy "met_SP_Ztrans_inv" [] e_metID
955 (["SignalProcessing", "Z_Transform", "Inverse"],
956 [("#Given" , ["filterExpression X_eq", "boundVariable X_z"]),
957 ("#Find", ["stepResponse n_eq"])],
958 {rew_ord'="tless_true", rls'= Rule_Set.empty, calc = [], srls = Rule_Set.empty, prls = Rule_Set.empty, crls = Rule_Set.empty,
959 errpats = [], nrls = Rule_Set.empty},
960 "Program InverseZTransform (Xeq::bool) =" ^ (*TODO boundVariable X_z*)
961 " (let X = Take Xeq;" ^
962 " X = Rewrite ruleZY X" ^
966 text\<open>\noindent Check if the method has been stored correctly\ldots\<close>
972 text\<open>\noindent If yes we can get the method by stepping backwards through
973 the hierarchy.\<close>
976 MethodC.from_store ["SignalProcessing", "Z_Transform", "Inverse"];
979 section \<open>Program in TP-based language \label{prog-steps}\<close>
981 text\<open>\noindent We start stepwise expanding our program. The script is a
982 simple string containing several manipulation instructions.
983 \par The first script we try contains no instruction, we only test if
984 building scripts that way work.\<close>
986 subsection \<open>Stepwise Extend the Program\<close>
989 "Program InverseZTransform (Xeq::bool) = "^
993 text\<open>\noindent Next we put some instructions in the script and try if we are
994 able to solve our first equation.\<close>
998 "Program InverseZTransform (Xeq::bool) = "^
1000 * 1/z) instead of z \<up> -1
1002 " (let X = Take Xeq; "^
1003 " X' = Rewrite ruleZY False X; "^
1007 " X' = (Rewrite_Set norm_Rational False) X' "^
1015 "Program InverseZTransform (Xeq::bool) = "^
1017 * (1/z) instead of z \<up> -1
1019 " (let X = Take Xeq; "^
1020 " X' = Rewrite ruleZY False X; "^
1024 " X' = (Rewrite_Set norm_Rational False) X'; "^
1028 " X' = (SubProblem (IsacX,[pqFormula,degree_2, "^
1029 " polynomial,univariate,equation], "^
1031 " [BOOL e_e, REAL v_v]) "^
1035 text\<open>\noindent To solve the equation it is necessary to drop the left hand
1036 side, now we only need the denominator of the right hand side. The first
1037 equation solves the zeros of our expression.\<close>
1041 "Program InverseZTransform (Xeq::bool) = "^
1042 " (let X = Take Xeq; "^
1043 " X' = Rewrite ruleZY False X; "^
1044 " X' = (Rewrite_Set norm_Rational False) X'; "^
1045 " funterm = rhs X' "^
1047 * drop X'= for equation solving
1052 text\<open>\noindent As mentioned above, we need the denominator of the right hand
1053 side. The equation itself consists of this denominator and tries to find
1054 a $z$ for this the denominator is equal to zero.\<close>
1056 text \<open> dropped during switch from Program to partial_function:
1058 "Program InverseZTransform (X_eq::bool) = "^
1059 " (let X = Take X_eq; "^
1060 " X' = Rewrite ruleZY False X; "^
1061 " X' = (Rewrite_Set norm_Rational False) X'; "^
1062 " (X'_z::real) = lhs X'; "^
1063 " (z::real) = argument_in X'_z; "^
1064 " (funterm::real) = rhs X'; "^
1065 " (denom::real) = get_denominator funterm; "^
1069 " (equ::bool) = (denom = (0::real)); "^
1070 " (L_L::bool list) = "^
1071 " (SubProblem (Test, "^
1072 " [LINEAR,univariate,equation,test], "^
1073 " [Test,solve_linear]) "^
1074 " [BOOL equ, REAL z]) "^
1078 val sc = (inst_abs o Thm.term_of o the o (parse thy)) str;
1082 text \<open>\noindent This ruleset contains all functions that are in the script;
1083 The evaluation of the functions is done by rewriting using this ruleset.\<close>
1087 Rule_Set.Repeat {id="srls_InverseZTransform",
1089 rew_ord = ("termlessI",termlessI),
1090 erls = Rule_Set.append_rules "erls_in_srls_InverseZTransform" Rule_Set.empty
1091 [(*for asm in NTH_CONS ...*)
1092 Eval ("Orderings.ord_class.less",eval_equ "#less_"),
1093 (*2nd NTH_CONS pushes n+-1 into asms*)
1094 Eval("Groups.plus_class.plus", eval_binop "#add_")
1096 srls = Rule_Set.Empty, calc = [], errpatts = [],
1098 Thm ("NTH_CONS",ThmC.numerals_to_Free @{thm NTH_CONS}),
1099 Eval("Groups.plus_class.plus", eval_binop "#add_"),
1100 Thm ("NTH_NIL",ThmC.numerals_to_Free @{thm NTH_NIL}),
1101 Eval("Prog_Expr.lhs", eval_lhs"eval_lhs_"),
1102 Eval("Prog_Expr.rhs", eval_rhs"eval_rhs_"),
1103 Eval("Prog_Expr.argument'_in", eval_argument_in "Prog_Expr.argument'_in"),
1104 Eval("Rational.get_denominator", eval_get_denominator "#get_denominator"),
1105 Eval("Rational.get_numerator", eval_get_numerator "#get_numerator"),
1106 Eval("Partial_Fractions.factors_from_solution",
1107 eval_factors_from_solution "#factors_from_solution"),
1108 Eval("Partial_Fractions.drop_questionmarks",
1109 eval_drop_questionmarks "#drop_?")
1115 subsection \<open>Store Final Version of Program for Execution\<close>
1117 text\<open>\noindent After we also tested how to write scripts and run them,
1118 we start creating the final version of our script and store it into
1119 the method for which we created a node in Section~\ref{sec:cparentnode}
1120 Note that we also did this stepwise, but we didn't kept every
1123 setup \<open>KEStore_Elems.add_mets
1124 [MethodC.prep_input thy "met_SP_Ztrans_inv" [] e_metID
1125 (["SignalProcessing", "Z_Transform", "Inverse"],
1126 [("#Given" , ["filterExpression X_eq"]), (*TODO boundVariable X_z*)
1127 ("#Find", ["stepResponse n_eq"])],
1128 {rew_ord'="tless_true", rls'= Rule_Set.empty, calc = [], srls = srls, prls = Rule_Set.empty, crls = Rule_Set.empty,
1129 errpats = [], nrls = Rule_Set.empty},
1130 "Program InverseZTransform (X_eq::bool) = "^
1131 (*(1/z) instead of z \<up> -1*)
1132 "(let X = Take X_eq; "^
1133 " X' = Rewrite ruleZY False X; "^
1135 " (num_orig::real) = get_numerator (rhs X'); "^
1136 " X' = (Rewrite_Set norm_Rational False) X'; "^
1138 " (X'_z::real) = lhs X'; "^
1139 " (zzz::real) = argument_in X'_z; "^
1140 " (funterm::real) = rhs X'; "^
1141 (*drop X' z = for equation solving*)
1142 " (denom::real) = get_denominator funterm; "^
1144 " (num::real) = get_numerator funterm; "^
1146 " (equ::bool) = (denom = (0::real)); "^
1147 " (L_L::bool list) = (SubProblem (PolyEqX, "^
1148 " [abcFormula,degree_2,polynomial,univariate,equation], "^
1150 " [BOOL equ, REAL zzz]); "^
1151 " (facs::real) = factors_from_solution L_L; "^
1152 " (eql::real) = Take (num_orig / facs); "^
1154 " (eqr::real) = (Try (Rewrite_Set ansatz_rls False)) eql; "^
1156 " (eq::bool) = Take (eql = eqr); "^
1157 (*Maybe possible to use HOLogic.mk_eq ??*)
1158 " eq = (Try (Rewrite_Set equival_trans False)) eq; "^
1160 " eq = drop_questionmarks eq; "^
1161 " (z1::real) = (rhs (NTH 1 L_L)); "^
1163 * prepare equation for a - eq_a
1164 * therefor substitute z with solution 1 - z1
1166 " (z2::real) = (rhs (NTH 2 L_L)); "^
1168 " (eq_a::bool) = Take eq; "^
1169 " eq_a = (Substitute [zzz=z1]) eq; "^
1170 " eq_a = (Rewrite_Set norm_Rational False) eq_a; "^
1171 " (sol_a::bool list) = "^
1172 " (SubProblem (IsacX, "^
1173 " [univariate,equation],[no_met]) "^
1174 " [BOOL eq_a, REAL (A::real)]); "^
1175 " (a::real) = (rhs(NTH 1 sol_a)); "^
1177 " (eq_b::bool) = Take eq; "^
1178 " eq_b = (Substitute [zzz=z2]) eq_b; "^
1179 " eq_b = (Rewrite_Set norm_Rational False) eq_b; "^
1180 " (sol_b::bool list) = "^
1181 " (SubProblem (IsacX, "^
1182 " [univariate,equation],[no_met]) "^
1183 " [BOOL eq_b, REAL (B::real)]); "^
1184 " (b::real) = (rhs(NTH 1 sol_b)); "^
1186 " eqr = drop_questionmarks eqr; "^
1187 " (pbz::real) = Take eqr; "^
1188 " pbz = ((Substitute [A=a, B=b]) pbz); "^
1190 " pbz = Rewrite ruleYZ False pbz; "^
1191 " pbz = drop_questionmarks pbz; "^
1193 " (X_z::bool) = Take (X_z = pbz); "^
1194 " (n_eq::bool) = (Rewrite_Set inverse_z False) X_z; "^
1195 " n_eq = drop_questionmarks n_eq "^
1200 subsection \<open>Check the Program\<close>
1201 text\<open>\noindent When the script is ready we can start checking our work.\<close>
1202 subsubsection \<open>Check the Formalization\<close>
1203 text\<open>\noindent First we want to check the formalization of the in and
1204 output of our program.\<close>
1208 ["filterExpression (X = 3 / (z - 1/4 + -1/8 * (1/(z::real))))",
1209 "stepResponse (x[n::real]::bool)"];
1211 ("Isac_Knowledge", ["Inverse", "Z_Transform", "SignalProcessing"],
1212 ["SignalProcessing", "Z_Transform", "Inverse"]);
1219 Const ("Inverse_Z_Transform.filterExpression", _),
1220 [Const ("HOL.eq", _) $ _ $ _]
1226 Const ("Inverse_Z_Transform.stepResponse", _),
1230 ) = O_Model.init fmz thy ((#ppc o Problem.from_store) pI);
1233 = (#scr o MethodC.from_store) ["SignalProcessing",
1239 subsubsection \<open>Stepwise Check the Program\label{sec:stepcheck}\<close>
1240 text\<open>\noindent We start to stepwise execute our new program in a calculation
1241 tree and check if every node implements that what we have wanted.\<close>
1244 Rewrite.trace_on := false; (*true*)
1245 LItool.trace_on := false; (*true*)
1249 ["filterExpression (X z = 3 / ((z::real) + 1/10 - 1/50*(1/z)))",
1250 "stepResponse (x[n::real]::bool)"];
1253 ("Isac_Knowledge", ["Inverse", "Z_Transform", "SignalProcessing"],
1254 ["SignalProcessing", "Z_Transform", "Inverse"]);
1256 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI,pI,mI))];
1257 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1259 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1261 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1263 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1265 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1267 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1269 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1270 "Rewrite (ruleZY, Inverse_Z_Transform.ruleZY)";
1271 "--> X z = 3 / (z - 1 / 4 + -1 / 8 * (1 / z))";
1275 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1276 "Rewrite_Set norm_Rational";
1277 " --> X' z = 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))";
1278 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1283 text \<open>\noindent Instead of \ttfamily nxt = Subproblem \normalfont above we had
1284 \ttfamily Empty\_Tac; \normalfont the search for the reason considered
1285 the following points:\begin{itemize}
1286 \item What shows \ttfamily show\_pt pt;\normalfont\ldots?
1287 \begin{verbatim}(([2], Res), ?X' z = 24 / (-1 + -2 * z + 8 * z \<up> 2))]\end{verbatim}
1288 The calculation is ok but no \ttfamily next \normalfont step found:
1289 Should be\\ \ttfamily nxt = Subproblem\normalfont!
1290 \item What shows \ttfamily trace\_script := true; \normalfont we read
1293 @@@next leaf 'SubProblem
1294 (PolyEq',[abcFormula, degree_2, polynomial,
1295 univariate, equation], no_meth)
1297 ---> Program.Tac 'SubProblem (PolyEq',
1298 [abcFormula, degree_2, polynomial,
1299 univariate, equation], no_meth)
1300 [BOOL (-1 + -2 * z + 8 * z \^\^\^ ~2 = 0), REAL z]'
1302 We see the SubProblem with correct arguments from searching next
1303 step (program text !!!--->!!! Program.Tac (script tactic) with arguments
1305 \item Do we have the right Program \ldots difference in the
1306 arguments in the arguments\ldots
1309 (#scr o MethodC.from_store) ["SignalProcessing",
1312 writeln (UnparseC.term s);
1314 \ldots shows the right script. Difference in the arguments.
1315 \item Test --- Why helpless here ? --- shows: \ttfamily replace
1316 no\_meth by [no\_meth] \normalfont in Program
1321 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1325 text \<open>\noindent Instead of \ttfamily nxt = Model\_Problem \normalfont above
1326 we had \ttfamily Empty\_Tac; \normalfont the search for the reason
1327 considered the following points:\begin{itemize}
1328 \item Difference in the arguments
1329 \item Comparison with Subsection~\ref{sec:solveq}: There solving this
1330 equation works, so there must be some difference in the arguments
1331 of the Subproblem: RIGHT: we had \ttfamily [no\_meth] \normalfont
1332 instead of \ttfamily [no\_met] \normalfont ;-)
1333 \end{itemize}\<close>
1336 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1337 (*Add_Given equality (-1 + -2 * z + 8 * z \<up> 2 = 0)";*)
1338 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1339 (*Add_Given solveFor z";*)
1340 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1341 (*Add_Find solutions z_i";*)
1342 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1343 (*Specify_Theory Isac";*)
1346 text \<open>\noindent We had \ttfamily nxt = Empty\_Tac instead Specify\_Theory;
1347 \normalfont The search for the reason considered the following points:
1349 \item Was there an error message? NO -- ok
1350 \item Has \ttfamily nxt = Add\_Find \normalfont been inserted in pt:\\
1351 \ttfamily get\_obj g\_pbl pt (fst p);\normalfont? YES -- ok
1352 \item What is the returned formula:
1354 print_depth 999; f; print_depth 3;
1355 { Find = [ Correct "solutions z_i"],
1357 Given = [Correct "equality (-1 + -2*z + 8*z \<up> 2 = 0)",
1358 Correct "solveFor z"],
1362 \normalfont The only False is the reason: the Where (the precondition) is
1363 False for good reasons: The precondition seems to check for linear
1364 equations, not for the one we want to solve! Removed this error by
1365 correcting the Program from \ttfamily SubProblem (PolyEq',
1366 \lbrack linear,univariate,equation,
1367 test\rbrack, \lbrack Test,solve\_linear\rbrack \normalfont to
1368 \ttfamily SubProblem (PolyEq',\\ \lbrack abcFormula,degree\_2,
1369 polynomial,univariate,equation\rbrack,\\
1370 \lbrack PolyEq,solve\_d2\_polyeq\_abc\_equation
1372 You find the appropriate type of equation at the
1373 {\sisac}-WEB-Page\footnote{
1374 \href{http://www.ist.tugraz.at/projects/isac/www/kbase/pbl/index\_pbl.html}
1375 {http://www.ist.tugraz.at/projects/isac/www/kbase/pbl/index\_pbl.html}
1377 And the respective method in \ttfamily Knowledge/PolyEq.thy \normalfont
1378 at the respective \ttfamily store\_pbt. \normalfont Or you leave the
1379 selection of the appropriate type to isac as done in the final Program ;-))
1380 \end{itemize}\<close>
1383 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1384 (*Specify_Problem [abcFormula,...";*)
1385 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1386 (*Specify_Method [PolyEq,solve_d2_polyeq_abc_equation";*)
1387 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1388 (*Apply_Method [PolyEq,solve_d2_polyeq_abc_equation";*)
1389 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1390 (*Rewrite_Set_Inst [(''bdv'', z)], d2_polyeq_abcFormula_simplify";*)
1391 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1392 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1393 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
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 (*Specify_Problem ["normalise", "polynomial", "univariate", "equation"]*)
1409 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1410 (*Specify_Method ["PolyEq", "normalise_poly"]*)
1411 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1412 (*Apply_Method ["PolyEq", "normalise_poly"]*)
1413 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1414 (*Rewrite ("all_left", "PolyEq.all_left")*)
1415 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1416 (*Rewrite_Set_Inst (["(''bdv'', A)"], "make_ratpoly_in")*)
1417 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1418 (*Rewrite_Set "polyeq_simplify"*)
1419 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1420 (*Subproblem("Isac_Knowledge",["degree_1", "polynomial", "univariate", "equation"])*)
1421 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1422 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
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 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; (*([11, 4, 5], Res) Check_Postcond*)
1467 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*([11, 4], Res) Check_Postcond*)
1468 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*([11], Res) Take*)
1469 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*([12], Frm) Substitute*)
1470 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*([12], Res) Rewrite*)
1471 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*([13], Res) Take*)
1472 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*([14], Frm) Empty_Tac*)
1475 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
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;
1494 LItool.trace_on := true;
1497 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1500 Test_Tool.show_pt pt;
1515 text\<open>\noindent As a last step we check the tracing output of the last calc
1516 tree instruction and compare it with the pre-calculated result.\<close>
1518 section \<open>Improve and Transfer into Knowledge\<close>
1520 We want to improve the very long program \ttfamily InverseZTransform
1521 \normalfont by modularisation: partial fraction decomposition shall
1522 become a sub-problem.
1524 We could transfer all knowledge in \ttfamily Build\_Inverse\_Z\_Transform.thy
1525 \normalfont first to the \ttfamily Knowledge/Inverse\_Z\_Transform.thy
1526 \normalfont and then modularise. In this case TODO problems?!?
1528 We chose another way and go bottom up: first we build the sub-problem in
1529 \ttfamily Partial\_Fractions.thy \normalfont with the term:
1531 $$\frac{3}{x\cdot(z - \frac{1}{4} + \frac{-1}{8}\cdot\frac{1}{z})}$$
1533 \noindent (how this still can be improved see \ttfamily Partial\_Fractions.thy\normalfont),
1534 and re-use all stuff prepared in \ttfamily Build\_Inverse\_Z\_Transform.thy:
1535 \normalfont The knowledge will be transferred to \ttfamily src/../Partial\_Fractions.thy
1536 \normalfont and the respective tests to:
1537 \begin{center}\ttfamily test/../sartial\_fractions.sml\normalfont\end{center}
1540 subsection \<open>Transfer to Partial\_Fractions.thy\<close>
1542 First we transfer both, knowledge and tests into:
1543 \begin{center}\ttfamily src/../Partial\_Fractions.thy\normalfont\end{center}
1544 in order to immediately have the test results.
1546 We copy \ttfamily factors\_from\_solution, drop\_questionmarks,\\
1547 ansatz\_2nd\_order \normalfont and rule-sets --- no problem.
1549 Also \ttfamily store\_pbt ..\\ "pbl\_simp\_rat\_partfrac"
1550 \normalfont is easy.
1552 But then we copy from:\\
1553 (1) \ttfamily Build\_Inverse\_Z\_Transform.thy store\_met\ldots "met\_SP\_Ztrans\_inv"
1555 (2) \ttfamily Partial\_Fractions.thy store\_met\ldots "met\_SP\_Ztrans\_inv"
1556 \normalfont\\ and cut out the respective part from the program. First we ensure that
1557 the string is correct. When we insert the string into (2)
1558 \ttfamily store\_met .. "met\_partial\_fraction" \normalfont --- and get an error.
1561 subsubsection \<open>'Programming' in ISAC's TP-based Language\<close>
1563 At the present state writing programs in {\sisac} is particularly cumbersome.
1564 So we give hints how to cope with the many obstacles. Below we describe the
1565 steps we did in making (2) run.
1568 \item We check if the \textbf{string} containing the program is correct.
1569 \item We check if the \textbf{types in the program} are correct.
1570 For this purpose we start start with the first and last lines
1572 "PartFracScript (f_f::real) (v_v::real) = " ^
1573 " (let X = Take f_f; " ^
1574 " pbz = ((Substitute []) X) " ^
1577 The last but one line helps not to bother with ';'.
1578 \item Then we add line by line. Already the first line causes the error.
1579 So we investigate it by
1581 val ctxt = Proof_Context.init_global @{theory "Inverse_Z_Transform"} ;
1583 parseNEW ctxt "(num_orig::real) =
1584 get_numerator(rhs f_f)";
1586 and see a type clash: \ttfamily rhs \normalfont from (1) requires type
1587 \ttfamily bool \normalfont while (2) wants to have \ttfamily (f\_f::real).
1588 \normalfont Of course, we don't need \ttfamily rhs \normalfont anymore.
1589 \item Type-checking can be very tedious. One might even inspect the
1590 parse-tree of the program with {\sisac}'s specific debug tools:
1592 val {scr = Prog t,...} =
1593 MethodC.from_store ["simplification",
1595 "to_partial_fraction"];
1596 atomty_thy @{theory "Inverse_Z_Transform"} t ;
1598 \item We check if the \textbf{semantics of the program} by stepwise evaluation
1599 of the program. Evaluation is done by the Lucas-Interpreter, which works
1600 using the knowledge in theory Isac_Knowledge; so we have to re-build Isac. And the
1601 test are performed simplest in a file which is loaded with Isac.
1602 See \ttfamily tests/../partial\_fractions.sml \normalfont.
1606 subsection \<open>Transfer to Inverse\_Z\_Transform.thy\<close>
1608 It was not possible to complete this task, because we ran out of time.