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" Atools_erls
77 [ \<^rule_thm>\<open>rule3\<close>,
78 \<^rule_thm>\<open>rule4\<close>,
79 \<^rule_thm>\<open>rule1\<close>
83 val t = TermC.parse_test @{context} "z / (z - 1) + z / (z - \<alpha>) + 1::real";
85 val SOME (t', asm) = Rewrite.rewrite_set_ thy true inverse_Z t;
86 (*rewrite__set_ called with 'Erls' for '|| z || < 1'*)
88 UnparseC.term t' = "z / (z - ?\<delta> [?n]) + z / (z - \<alpha>) + ?\<delta> [?n]";
90 * Attention rule1 is applied before the expression is
91 * checked for rule4 which would be correct!!!
96 ML \<open>val (thy, ro, er) = (@{theory}, tless_true, eval_rls);\<close>
99 Rewrite.rewrite_ thy ro er true (ThmC.numerals_to_Free @{thm rule3}) t;
100 UnparseC.term t = "- ?u [- ?n - 1] + z / (z - \<alpha>) + 1";
105 Rewrite.rewrite_ thy ro er true (ThmC.numerals_to_Free @{thm rule4}) t;
106 UnparseC.term t = "- ?u [- ?n - 1] + \<alpha> \<up> ?n * ?u [?n] + 1";
111 Rewrite.rewrite_ thy ro er true (ThmC.numerals_to_Free @{thm rule1}) t;
112 UnparseC.term t = "- ?u [- ?n - 1] + \<alpha> \<up> ?n * ?u [?n] + ?\<delta> [?n]";
116 ML \<open>UnparseC.terms (asm1 @ asm2 @ asm3);\<close>
118 section\<open>Prepare Steps for TP-based programming Language\label{sec:prepstep}\<close>
120 \par \noindent The following sections are challenging with the CTP-based
121 possibilities of building the program. The goal is realized in
122 Section~\ref{spec-meth} and Section~\ref{prog-steps}.
123 \par The reader is advised to jump between the subsequent subsections and
124 the respective steps in Section~\ref{prog-steps}. By comparing
125 Section~\ref{sec:calc:ztrans} the calculation can be comprehended step
129 subsection \<open>Prepare Expression\label{prep-expr}\<close>
130 text\<open>\noindent We try two different notations and check which of them
131 Isabelle can handle best.\<close>
133 val ctxt = Proof_Context.init_global @{theory};
134 (*val ctxt = ContextC.declare_constraints' [@{term "z::real"}] ctxt;*)
137 TermC.parseNEW ctxt "X z = 3 / (z - 1/4 + -1/8 * z \<up> -1)"; UnparseC.term fun1;
139 TermC.parseNEW ctxt "X z = 3 / (z - 1/4 + -1/8 * (1/z))"; UnparseC.term fun1';
142 subsubsection \<open>Prepare Numerator and Denominator\<close>
143 text\<open>\noindent The partial fraction decomposition is only possible if we
144 get the bound variable out of the numerator. Therefor we divide
145 the expression by $z$. Follow up the Calculation at
146 Section~\ref{sec:calc:ztrans} line number 02.\<close>
149 ruleZY: "(X z = a / b) = (X' z = a / (z * b))"
152 val (thy, ro, er) = (@{theory}, tless_true, eval_rls);
153 val SOME (fun2, asm1) =
154 Rewrite.rewrite_ thy ro er true @{thm ruleZY} fun1; UnparseC.term fun2;
155 val SOME (fun2', asm1) =
156 Rewrite.rewrite_ thy ro er true @{thm ruleZY} fun1'; UnparseC.term fun2';
159 Rewrite.rewrite_set_ @{theory} false norm_Rational fun2;
162 * Fails on x \<up> (-1)
163 * We solve this problem by using 1/x as a workaround.
166 Rewrite.rewrite_set_ @{theory} false norm_Rational fun2';
173 subsubsection \<open>Get the Argument of the Expression X'\<close>
174 text\<open>\noindent We use \texttt{grep} for finding possibilities how we can
175 extract the bound variable in the expression. \ttfamily Prog_Expr.thy,
176 Tools.thy \normalfont contain general utilities: \ttfamily
177 eval\_argument\_in, eval\_rhs, eval\_lhs,\ldots \normalfont
178 \ttfamily grep -r "fun eva\_" * \normalfont shows all functions
179 witch can be used in a script. Lookup this files how to build
180 and handle such functions.
181 \par The next section shows how to introduce such a function.
184 subsubsection\<open>Decompose the Given Term Into lhs and rhs\<close>
186 val (_, expr) = HOLogic.dest_eq fun3'; UnparseC.term expr;
188 HOLogic.dest_bin \<^const_name>\<open>divide\<close> (type_of expr) expr;
189 UnparseC.term denom = "-1 + -2 * z + 8 * z \<up> 2";
192 text\<open>\noindent We have rhs\footnote{Note: lhs means \em Left Hand Side
193 \normalfont and rhs means \em Right Hand Side \normalfont and indicates
194 the left or the right part of an equation.} in the Program language, but
195 we need a function which gets the denominator of a fraction.\<close>
197 subsubsection\<open>Get the Denominator and Numerator out of a Fraction\<close>
198 text\<open>\noindent The self written functions in e.g. \texttt{get\_denominator}
199 should become a constant for the Isabelle parser:\<close>
202 get_denominator :: "real => real"
203 get_numerator :: "real => real"
205 text \<open>\noindent With the above definition we run into problems when we parse
206 the Program \texttt{InverseZTransform}. This leads to \em ambiguous
207 parse trees. \normalfont We avoid this by moving the definition
208 to \ttfamily Rational.thy \normalfont and re-building {\sisac}.
209 \par \noindent ATTENTION: From now on \ttfamily
210 Build\_Inverse\_Z\_Transform \normalfont mimics a build from scratch;
211 it only works due to re-building {\sisac} several times (indicated
218 * ("Rational.get_denominator", eval_get_denominator ""))
220 fun eval_get_denominator (thmid:string) _
221 (t as Const (\<^const_name>\<open>get_denominator\<close>, _) $
222 (Const (\<^const_name>\<open>divide\<close>, _) $num
224 SOME (TermC.mk_thmid thmid (UnparseC.term_in_thy thy denom) "",
225 HOLogic.Trueprop $ (TermC.mk_equality (t, denom)))
226 | eval_get_denominator _ _ _ _ = NONE;
228 text \<open>\noindent For the tests of \ttfamily eval\_get\_denominator \normalfont
229 see \ttfamily test/Knowledge/rational.sml\normalfont\<close>
231 text \<open>\noindent \ttfamily get\_numerator \normalfont should also become a
232 constant for the Isabelle parser, follow up the \texttt{const}
233 declaration above.\<close>
238 * ("Rational.get_numerator", eval_get_numerator ""))
240 fun eval_get_numerator (thmid:string) _
241 (t as Const (\<^const_name>\<open>Rational.get_numerator\<close>, _) $
242 (Const (\<^const_name>\<open>divide\<close>, _) $num
244 SOME (TermC.mk_thmid thmid (UnparseC.term_in_thy thy num) "",
245 HOLogic.Trueprop $ (TermC.mk_equality (t, num)))
246 | eval_get_numerator _ _ _ _ = NONE;
249 text \<open>\noindent We discovered several problems by implementing the
250 \ttfamily get\_numerator \normalfont function. Remember when
251 putting new functions to {\sisac}, put them in a thy file and rebuild
252 {\sisac}, also put them in the ruleset for the script!\<close>
254 subsection \<open>Solve Equation\label{sec:solveq}\<close>
255 text \<open>\noindent We have to find the zeros of the term, therefor we use our
256 \ttfamily get\_denominator \normalfont function from the step before
257 and try to solve the second order equation. (Follow up the Calculation
258 in Section~\ref{sec:calc:ztrans} Subproblem 2) Note: This type of
259 equation is too general for the present program.
260 \par We know that this equation can be categorized as \em univariate
261 equation \normalfont and solved with the functions {\sisac} provides
262 for this equation type. Later on {\sisac} should determine the type
263 of the given equation self.\<close>
265 val denominator = TermC.parseNEW ctxt "z \<up> 2 - 1/4*z - 1/8 = 0";
266 val fmz = ["equality (z \<up> 2 - 1/4*z - 1/8 = (0::real))",
269 val (dI',pI',mI') =("Isac_Knowledge", ["univariate", "equation"], ["no_met"]);
271 text \<open>\noindent Check if the given equation matches the specification of this
272 equation type.\<close>
274 M_Match.match_pbl fmz (Problem.from_store ["univariate", "equation"]);
277 text\<open>\noindent We switch up to the {\sisac} Context and try to solve the
278 equation with a more specific type definition.\<close>
281 Context.theory_name thy = "Isac_Knowledge";
282 val denominator = TermC.parseNEW ctxt "-1 + -2 * z + 8 * z \<up> 2 = 0";
283 val fmz = (*specification*)
284 ["equality (-1 + -2 * z + 8 * z \<up> 2 = (0::real))",(*equality*)
285 "solveFor z", (*bound variable*)
286 "solutions L"]; (*identifier for
290 ["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
294 text \<open>\noindent Check if the (other) given equation matches the
295 specification of this equation type.\<close>
298 M_Match.match_pbl fmz (Problem.from_store
299 ["abcFormula", "degree_2", "polynomial", "univariate", "equation"]);
302 text \<open>\noindent We stepwise solve the equation. This is done by the
303 use of a so called calc tree seen downwards.\<close>
306 val (p,_,f,nxt,_,pt) = Test_Code.init_calc @{context} [(fmz, (dI',pI',mI'))];
307 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
308 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
309 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
310 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
311 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
312 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
313 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
314 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
315 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
316 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
317 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
318 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
320 * nxt =..,Check_elementwise "Assumptions")
322 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
323 val (p,_,f,nxt,_,pt) = me nxt p [] pt; f2str f;
325 * [z = 1 / 2, z = -1 / 4]
327 Test_Tool.show_pt pt;
328 val SOME f = parseNEW ctxt "[z=1/2, z=-1/4]";
331 subsection \<open>Partial Fraction Decomposition\label{sec:pbz}\<close>
332 text\<open>\noindent We go on with the decomposition of our expression. Follow up the
333 Calculation in Section~\ref{sec:calc:ztrans} Step~3 and later on
334 Subproblem~1.\<close>
335 subsubsection \<open>Solutions of the Equation\<close>
336 text\<open>\noindent We get the solutions of the before solved equation in a list.\<close>
339 val SOME solutions = parseNEW ctxt "[z=1/2, z=-1/4]";
340 UnparseC.term solutions;
344 subsubsection \<open>Get Solutions out of a List\<close>
345 text \<open>\noindent In {\sisac}'s TP-based programming language:
347 let $ $ s_1 = NTH 1 $ solutions; $ s_2 = NTH 2... $
353 val Const (\<^const_name>\<open>Cons\<close>, _) $ s_1 $ (Const (\<^const_name>\<open>Cons\<close>, _)
354 $ s_2 $ Const (\<^const_name>\<open>Nil\<close>, _)) = solutions;
359 text\<open>\noindent The ansatz for the \em Partial Fraction Decomposition \normalfont
360 requires to get the denominators of the partial fractions out of the
363 \item $Denominator_{1}=z-Zeropoint_{1}$
364 \item $Denominator_{2}=z-Zeropoint_{2}$
370 val xx = HOLogic.dest_eq s_1;
371 val s_1' = HOLogic.mk_binop \<^const_name>\<open>minus\<close> xx;
372 val xx = HOLogic.dest_eq s_2;
373 val s_2' = HOLogic.mk_binop \<^const_name>\<open>minus\<close> xx;
378 text \<open>\noindent For the programming language a function collecting all the
379 above manipulations is helpful.\<close>
383 let val (lhs, rhs) = HOLogic.dest_eq s
384 in HOLogic.mk_binop \<^const_name>\<open>minus\<close> (lhs, rhs) end;
388 fun mk_prod prod [] =
389 if prod = TermC.empty
390 then error "mk_prod called with []"
392 | mk_prod prod (t :: []) =
393 if prod = TermC.empty
395 else HOLogic.mk_binop \<^const_name>\<open>times\<close> (prod, t)
396 | mk_prod prod (t1 :: t2 :: ts) =
397 if prod = TermC.empty
400 HOLogic.mk_binop \<^const_name>\<open>times\<close> (t1, t2)
404 HOLogic.mk_binop \<^const_name>\<open>times\<close> (prod, t1)
405 in mk_prod p (t2 :: ts) end
408 probably keep these test in test/Tools/isac/...
409 (*mk_prod TermC.empty [];*)
411 val prod = mk_prod TermC.empty [parse_test @{context} "x + 123"];
412 UnparseC.term prod = "x + 123";
414 val sol = parse_test @{context} "[z = 1 / 2, z = -1 / 4]";
415 val sols = HOLogic.dest_list sol;
416 val facs = map fac_from_sol sols;
417 val prod = mk_prod TermC.empty facs;
418 UnparseC.term prod = "(z + -1 * (1 / 2)) * (z + -1 * (-1 / 4))";
421 mk_prod TermC.empty [parse_test @{context} "x + 1", parse_test @{context} "x + 2", parse_test @{context} "x + 3"];
422 UnparseC.term prod = "(x + 1) * (x + 2) * (x + 3)";
425 fun factors_from_solution sol =
426 let val ts = HOLogic.dest_list sol
427 in mk_prod TermC.empty (map fac_from_sol ts) end;
430 val sol = parse_test @{context} "[z = 1 / 2, z = -1 / 4]";
431 val fs = factors_from_solution sol;
432 UnparseC.term fs = "(z + -1 * (1 / 2)) * (z + -1 * (-1 / 4))"
434 text \<open>\noindent This function needs to be packed such that it can be evaluated
435 by the Lucas-Interpreter. Therefor we moved the function to the
436 corresponding \ttfamily Equation.thy \normalfont in our case
437 \ttfamily PartialFractions.thy \normalfont. The necessary steps
438 are quit the same as we have done with \ttfamily get\_denominator
439 \normalfont before.\<close>
441 (*("factors_from_solution",
442 ("Partial_Fractions.factors_from_solution",
443 eval_factors_from_solution ""))*)
445 fun eval_factors_from_solution (thmid:string) _
446 (t as Const ("Partial_Fractions.factors_from_solution", _) $ sol) thy =
447 let val prod = factors_from_solution sol
448 in SOME (TermC.mk_thmid thmid (UnparseC.term_in_thy thy prod) "",
449 HOLogic.Trueprop $ (TermC.mk_equality (t, prod)))
451 | eval_factors_from_solution _ _ _ _ = NONE;
454 text \<open>\noindent The tracing output of the calc tree after applying this
457 24 / factors_from_solution [z = 1/ 2, z = -1 / 4])]
461 val nxt = ("Empty_Tac", ...): tac'_)
463 These observations indicate, that the Lucas-Interpreter (LIP)
464 does not know how to evaluate \ttfamily factors\_from\_solution
465 \normalfont, so we knew that there is something wrong or missing.
468 text\<open>\noindent First we isolate the difficulty in the program as follows:
470 " (L_L::bool list) = (SubProblem (PolyEqX, " ^
471 " [abcFormula, degree_2, polynomial, " ^
472 " univariate,equation], " ^
474 " [BOOL equ, REAL zzz]); " ^
475 " (facs::real) = factors_from_solution L_L; " ^
476 " (foo::real) = Take facs " ^
479 \par \noindent And see the tracing output:
482 [(([], Frm), Problem (Isac, [inverse,
485 (([1], Frm), X z = 3 / (z - 1 / 4 + -1 / 8 * (1 / z))),
486 (([1], Res), ?X' z = 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))),
487 (([2], Res), ?X' z = 24 / (-1 + -2 * z + 8 * z \<up> 2)),
488 (([3], Pbl), solve (-1 + -2 * z + 8 * z \<up> 2 = 0, z)),
489 (([3,1], Frm), -1 + -2 * z + 8 * z \<up> 2 = 0),
490 (([3,1], Res), z = (- -2 + sqrt (-2 \<up> 2 - 4 * 8 * -1)) / (2 * 8)|
491 z = (- -2 - sqrt (-2 \<up> 2 - 4 * 8 * -1)) / (2 * 8)),
492 (([3,2], Res), z = 1 / 2 | z = -1 / 4),
493 (([3,3], Res), [ z = 1 / 2, z = -1 / 4]),
494 (([3,4], Res), [ z = 1 / 2, z = -1 / 4]),
495 (([3], Res), [ z = 1 / 2, z = -1 / 4]),
496 (([4], Frm), factors_from_solution [z = 1 / 2, z = -1 / 4])]
499 \par \noindent In particular that:
502 (([3], Pbl), solve (-1 + -2 * z + 8 * z \<up> 2 = 0, z)),
504 \par \noindent Shows the equation which has been created in
507 "(denom::real) = get_denominator funterm; " ^
508 (* get_denominator *)
509 "(equ::bool) = (denom = (0::real)); " ^
512 \noindent \ttfamily get\_denominator \normalfont has been evaluated successfully,
513 but not\\ \ttfamily factors\_from\_solution.\normalfont
514 So we stepwise compare with an analogous case, \ttfamily get\_denominator
515 \normalfont successfully done above: We know that LIP evaluates
516 expressions in the program by use of the \emph{prog_rls}, so we try to get
517 the original \emph{prog_rls}.\\
520 val {prog_rls,...} = MethodC.from_store ctxt ["SignalProcessing",
525 \par \noindent Create 2 good example terms:
529 parseNEW ctxt "get_denominator ((111::real) / 222)";
531 parseNEW ctxt "factors_from_solution [(z::real)=1/2, z=-1/4]";
534 \par \noindent Rewrite the terms using prog_rls:\\
535 \ttfamily \par \noindent rewrite\_set\_ thy true prog_rls t1;\\
536 rewrite\_set\_ thy true prog_rls t2;\\
537 \par \noindent \normalfont Now we see a difference: \texttt{t1} gives
538 \texttt{SOME} but \texttt{t2} gives \texttt{NONE}. We look at the
542 Rule_Set.Repeat{id = "srls_InverseZTransform",
543 rules = [Eval("Rational.get_numerator",
544 eval_get_numerator "Rational.get_numerator"),
545 Eval("Partial_Fractions.factors_from_solution",
546 eval_factors_from_solution
547 "Partial_Fractions.factors_from_solution")]}
549 \par \noindent Here everthing is perfect. So the error can
550 only be in the SML code of \ttfamily eval\_factors\_from\_solution.
551 \normalfont We try to check the code with an existing test; since the
553 \begin{center}\ttfamily src/Tools/isac/Knowledge/Partial\_Fractions.thy
554 \normalfont\end{center}
555 the \emph{test} should be in
556 \begin{center}\ttfamily test/Tools/isac/Knowledge/partial\_fractions.sml
557 \normalfont\end{center}
558 \par \noindent After updating the function \ttfamily
559 factors\_from\_solution \normalfont to a new version and putting a
560 test-case to \ttfamily Partial\_Fractions.sml \normalfont we tried again
561 to evaluate the term with the same result.
562 \par We opened the test \ttfamily Test\_Isac.thy \normalfont and saw that
563 everything is working fine. Also we checked that the test \ttfamily
564 partial\_fractions.sml \normalfont is used in \ttfamily Test\_Isac.thy
566 \begin{center}use \ttfamily "Knowledge/partial\_fractions.sml"
567 \normalfont \end{center}
568 and \ttfamily Partial\_Fractions.thy \normalfont is part is part of
569 {\sisac} by evaluating
572 val thy = @{theory "Inverse_Z_Transform"};
575 After rebuilding {\sisac} again it worked.
578 subsubsection \<open>Build Expression\<close>
579 text \<open>\noindent In {\sisac}'s TP-based programming language we can build
581 \ttfamily let s\_1 = Take numerator / (s\_1 * s\_2) \normalfont\<close>
585 * The main denominator is the multiplication of the denominators of
586 * all partial fractions.
589 val denominator' = HOLogic.mk_binop
590 \<^const_name>\<open>times\<close> (s_1', s_2') ;
591 val SOME numerator = parseNEW ctxt "3::real";
593 val expr' = HOLogic.mk_binop
594 \<^const_name>\<open>divide\<close> (numerator, denominator');
598 subsubsection \<open>Apply the Partial Fraction Decomposion Ansatz\<close>
600 text\<open>\noindent We use the Ansatz of the Partial Fraction Decomposition for our
601 expression 2nd order. Follow up the calculation in
602 Section~\ref{sec:calc:ztrans} Step~03.\<close>
604 ML \<open>Context.theory_name thy = "Isac_Knowledge"\<close>
606 text\<open>\noindent We define two axiomatization, the first one is the main ansatz,
607 the next one is just an equivalent transformation of the resulting
608 equation. Both axiomatizations were moved to \ttfamily
609 Partial\_Fractions.thy \normalfont and got their own rulesets. In later
610 programs it is possible to use the rulesets and the machine will find
611 the correct ansatz and equivalent transformation itself.\<close>
614 ansatz_2nd_order: "n / (a*b) = A/a + B/b" and
615 equival_trans_2nd_order: "(n/(a*b) = A/a + B/b) = (n = A*b + B*a)"
617 text\<open>\noindent We use our \ttfamily ansatz\_2nd\_order \normalfont to rewrite
618 our expression and get an equation with our expression on the left
619 and the partial fractions of it on the right hand side.\<close>
623 rewrite_ @{theory} e_rew_ord Rule_Set.empty false
624 @{thm ansatz_2nd_order} expr';
625 UnparseC.term t1; atomty t1;
626 val eq1 = HOLogic.mk_eq (expr', t1);
630 text\<open>\noindent Eliminate the denominators by multiplying the left and the
631 right hand side of the equation with the main denominator. This is an
632 simple equivalent transformation. Later on we use an own ruleset
633 defined in \ttfamily Partial\_Fractions.thy \normalfont for doing this.
634 Follow up the calculation in Section~\ref{sec:calc:ztrans} Step~04.\<close>
638 rewrite_ @{theory} e_rew_ord Rule_Set.empty false
639 @{thm equival_trans_2nd_order} eq1;
643 text\<open>\noindent We use the existing ruleset \ttfamily norm\_Rational \normalfont
644 for simplifications on expressions.\<close>
647 val SOME (eq3,_) = rewrite_set_ @{theory} false norm_Rational eq2;
650 * ?A ?B not simplified
654 text\<open>\noindent In Example~\ref{eg:gap} of my thesis I'm describing a problem about
655 simplifications. The problem that we would like to have only a specific degree
656 of simplification occurs right here, in the next step.\<close>
659 Rewrite.trace_on := false; (*true false*)
661 parseNEW ctxt "(z - 1/2)*(z - -1/4) * (A/(z - 1/2) + B/(z - -1/4))";
665 val SOME (fract2,_) =
666 rewrite_set_ @{theory} false norm_Rational fract1;
667 UnparseC.term fract2 = "(A + -2 * B + 4 * A * z + 4 * B * z) / 4";
669 * UnparseC.term fract2 = "A * (1 / 4 + z) + B * (-1 / 2 + z)"
670 * would be more traditional...
674 text\<open>\noindent We walk around this problem by generating our new equation first.\<close>
677 val (numerator, denominator) = HOLogic.dest_eq eq3;
678 val eq3' = HOLogic.mk_eq (numerator, fract1);
684 * MANDATORY: simplify (and remove denominator) otherwise 3 = 0
686 val SOME (eq3'' ,_) =
687 rewrite_set_ @{theory} false norm_Rational eq3';
691 text\<open>\noindent Still working at {\sisac}\ldots\<close>
693 ML \<open>Context.theory_name thy = "Isac_Knowledge"\<close>
695 subsubsection \<open>Build a Rule-Set for the Ansatz\<close>
696 text \<open>\noindent The \emph{ansatz} rules violate the principle that each
697 variable on the right-hand-side must also occur on the
698 left-hand-side of the rule: A, B, etc. don't do that. Thus the
699 rewriter marks these variables with question marks: ?A, ?B, etc.
700 These question marks can be dropped by \ttfamily fun
701 drop\_questionmarks\normalfont.\<close>
704 val ansatz_rls = prep_rls @{theory} (
705 Rule_Set.Repeat {id = "ansatz_rls", preconds = [], rew_ord = ("dummy_ord",dummy_ord),
706 asm_rls = Rule_Set.empty, prog_rls = Rule_Set.Empty, calc = [], errpatts = [],
708 Thm ("ansatz_2nd_order",ThmC.numerals_to_Free @{thm ansatz_2nd_order}),
709 Thm ("equival_trans_2nd_order",ThmC.numerals_to_Free @{thm equival_trans_2nd_order})
711 program = Empty_Prog});
714 text\<open>\noindent We apply the ruleset\ldots\<close>
718 rewrite_set_ @{theory} false ansatz_rls expr';
721 text\<open>\noindent And check the output\ldots\<close>
724 UnparseC.term expr' = "3 / ((z - 1 / 2) * (z - -1 / 4))";
725 UnparseC.term ttttt = "?A / (z - 1 / 2) + ?B / (z - -1 / 4)";
728 subsubsection \<open>Get the First Coefficient\<close>
730 text\<open>\noindent Now it's up to get the two coefficients A and B, which will be
731 the numerators of our partial fractions. Continue following up the
732 Calculation in Section~\ref{sec:calc:ztrans} Subproblem~1.\<close>
734 text\<open>\noindent To get the first coefficient we substitute $z$ with the first
735 zero-point we determined in Section~\ref{sec:solveq}.\<close>
739 rewrite_terms_ @{theory} e_rew_ord Rule_Set.empty [s_1] eq3'';
742 rewrite_set_ @{theory} false norm_Rational eq4_1;
745 val fmz = ["equality (3=3*A/(4::real))", "solveFor A", "solutions L"];
746 val (dI',pI',mI') =("Isac_Knowledge", ["univariate", "equation"], ["no_met"]);
748 * Solve the simple linear equation for A:
749 * Return eq, not list of eq's
751 val (p,_,fa,nxt,_,pt) = Test_Code.init_calc @{context} [(fmz, (dI',pI',mI'))];
752 val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
753 (*Add_Given "equality (3=3*A/4)"*)
754 val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
755 (*Add_Given "solveFor A"*)
756 val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
757 (*Add_Find "solutions L"*)
758 val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
759 (*Specify_Theory "Isac_Knowledge"*)
760 val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
761 (*Specify_Problem ["normalise", "polynomial",
762 "univariate", "equation"])*)
763 val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
764 (* Specify_Method["PolyEq", "normalise_poly"]*)
765 val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
766 (*Apply_Method["PolyEq", "normalise_poly"]*)
767 val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
768 (*Rewrite ("all_left", "PolyEq.all_left")*)
769 val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
770 (*Rewrite_Set_Inst(["(''bdv'',A)"],"make_ratpoly_in")*)
771 val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
772 (*Rewrite_Set "polyeq_simplify"*)
773 val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
774 val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
775 val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
776 (*Add_Given "equality (3 + -3 / 4 * A =0)"*)
777 val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
778 (*Add_Given "solveFor A"*)
779 val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
780 (*Add_Find "solutions A_i"*)
781 val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
782 val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
783 val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
784 val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
785 (*Apply_Method ["PolyEq", "solve_d1_polyeq_equation"]*)
786 val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
787 (*Rewrite_Set_Inst(["(''bdv'',A)"],"d1_polyeq_simplify")*)
788 val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
789 (*Rewrite_Set "polyeq_simplify"*)
790 val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
791 (*Rewrite_Set "norm_Rational_parenthesized"*)
792 val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
794 val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
795 (*Check_elementwise "Assumptions"*)
796 val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
797 (*Check_Postcond ["degree_1", "polynomial",
798 "univariate", "equation"]*)
799 val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
800 (*Check_Postcond ["normalise", "polynomial",
801 "univariate", "equation"]*)
802 val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
807 subsubsection \<open>Get Second Coefficient\<close>
809 text\<open>\noindent With the use of \texttt{thy} we check which theories the
810 interpreter knows.\<close>
812 ML \<open>thy\<close>
814 text\<open>\noindent To get the second coefficient we substitute $z$ with the second
815 zero-point we determined in Section~\ref{sec:solveq}.\<close>
818 val SOME (eq4b_1,_) =
819 rewrite_terms_ @{theory} e_rew_ord Rule_Set.empty [s_2] eq3'';
820 UnparseC.term eq4b_1;
821 val SOME (eq4b_2,_) =
822 rewrite_set_ @{theory} false norm_Rational eq4b_1;
823 UnparseC.term eq4b_2;
825 val fmz = ["equality (3= -3*B/(4::real))", "solveFor B", "solutions L"];
826 val (dI',pI',mI') =("Isac_Knowledge", ["univariate", "equation"], ["no_met"]);
827 val (p,_,fb,nxt,_,pt) = Test_Code.init_calc @{context} [(fmz, (dI',pI',mI'))];
828 val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
829 val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
830 val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
831 val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
832 val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
833 val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
834 val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
835 val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
836 val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
837 val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
838 val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
839 val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
840 val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
841 val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
842 val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
843 val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
844 val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
845 val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
846 val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
847 val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
848 val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
849 val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
850 val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
851 val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
852 val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
853 val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
854 val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
858 text\<open>\noindent We compare our results with the where_ calculated upshot.\<close>
861 if f2str fa = "[A = 4]" then () else error "part.fract. eq4_1";
862 if f2str fb = "[B = -4]" then () else error "part.fract. eq4_1";
865 section \<open>Implement the Specification and the MethodC \label{spec-meth}\<close>
867 text\<open>\noindent Now everything we need for solving the problem has been
868 tested out. We now start by creating new nodes for our methods and
869 further on our new program in the interpreter.\<close>
871 subsection\<open>Define the Field Descriptions for the
872 Specification\label{sec:deffdes}\<close>
874 text\<open>\noindent We define the fields \em filterExpression \normalfont and
875 \em stepResponse \normalfont both as equations, they represent the in- and
876 output of the program.\<close>
879 filterExpression :: "bool => una"
880 stepResponse :: "bool => una"
882 subsection\<open>Define the Specification\<close>
884 text\<open>\noindent The next step is defining the specifications as nodes in the
885 designated part. We have to create the hierarchy node by node and start
886 with \em SignalProcessing \normalfont and go on by creating the node
887 \em Z\_Transform\normalfont.\<close>
889 setup \<open>Know_Store.add_pbls
890 [Problem.prep_input @{theory} "pbl_SP" [] Problem.id_empty (["SignalProcessing"], [], Rule_Set.empty, NONE, []),
891 Problem.prep_input @{theory} "pbl_SP_Ztrans" [] Problem.id_empty
892 (["Z_Transform", "SignalProcessing"], [], Rule_Set.empty, NONE, [])]\<close>
894 text\<open>\noindent For the suddenly created node we have to define the input
895 and output parameters. We already prepared their definition in
896 Section~\ref{sec:deffdes}.\<close>
898 setup \<open>Know_Store.add_pbls
899 [Problem.prep_input @{theory} "pbl_SP_Ztrans_inv" [] Problem.id_empty
900 (["Inverse", "Z_Transform", "SignalProcessing"],
901 [("#Given" ,["filterExpression X_eq"]),
902 ("#Find", ["stepResponse n_eq"])],
903 Rule_Set.append_rules "empty" Rule_Set.empty [(*for preds in where_*)],
905 [["SignalProcessing", "Z_Transform", "Inverse"]])]\<close>
907 Test_Tool.show_ptyps() ();
908 Problem.from_store ["Inverse", "Z_Transform", "SignalProcessing"];
911 subsection \<open>Define Name and Signature for the MethodC\<close>
913 text\<open>\noindent As a next step we store the definition of our new method as a
914 constant for the interpreter.\<close>
917 InverseZTransform :: "[bool, bool] => bool"
918 ("((Program InverseZTransform (_ =))// (_))" 9)
920 subsection \<open>Setup Parent Nodes in Hierarchy of MethodC\label{sec:cparentnode}\<close>
922 text\<open>\noindent Again we have to generate the nodes step by step, first the
923 parent node and then the originally \em Z\_Transformation
924 \normalfont node. We have to define both nodes first with an empty script
927 setup \<open>Know_Store.add_mets
928 [MethodC.prep_input @{theory} "met_SP" [] e_metID
929 (["SignalProcessing"], [],
930 {rew_ord="tless_true", rls'= Rule_Set.empty, calc = [], prog_rls = Rule_Set.empty, where_rls = Rule_Set.empty, crls = Rule_Set.empty,
931 errpats = [], rew_rls = Rule_Set.empty},
933 MethodC.prep_input @{theory} "met_SP_Ztrans" [] e_metID
934 (["SignalProcessing", "Z_Transform"], [],
935 {rew_ord="tless_true", rls'= Rule_Set.empty, calc = [], prog_rls = Rule_Set.empty, where_rls = Rule_Set.empty, crls = Rule_Set.empty,
936 errpats = [], rew_rls = Rule_Set.empty},
940 text\<open>\noindent After we generated both nodes, we can fill the containing
941 script we want to implement later. First we define the specifications
942 of the script in e.g. the in- and output.\<close>
944 setup \<open>Know_Store.add_mets
945 [MethodC.prep_input thy "met_SP_Ztrans_inv" [] e_metID
946 (["SignalProcessing", "Z_Transform", "Inverse"],
947 [("#Given" ,["filterExpression X_eq", "boundVariable X_z"]),
948 ("#Find", ["stepResponse n_eq"])],
949 {rew_ord="tless_true", rls'= Rule_Set.empty, calc = [], prog_rls = Rule_Set.empty, where_rls = Rule_Set.empty, crls = Rule_Set.empty,
950 errpats = [], rew_rls = Rule_Set.empty},
954 text\<open>\noindent After we stored the definition we can start implementing the
955 script itself. As a first try we define only three rows containing one
956 simple operation.\<close>
958 setup \<open>Know_Store.add_mets
959 [MethodC.prep_input thy "met_SP_Ztrans_inv" [] e_metID
960 (["SignalProcessing", "Z_Transform", "Inverse"],
961 [("#Given" , ["filterExpression X_eq", "boundVariable X_z"]),
962 ("#Find", ["stepResponse n_eq"])],
963 {rew_ord="tless_true", rls'= Rule_Set.empty, calc = [], prog_rls = Rule_Set.empty, where_rls = Rule_Set.empty, crls = Rule_Set.empty,
964 errpats = [], rew_rls = Rule_Set.empty},
965 "Program InverseZTransform (Xeq::bool) =" ^ (*TODO boundVariable X_z*)
966 " (let X = Take Xeq;" ^
967 " X = Rewrite ruleZY X" ^
971 text\<open>\noindent Check if the method has been stored correctly\ldots\<close>
977 text\<open>\noindent If yes we can get the method by stepping backwards through
978 the hierarchy.\<close>
981 MethodC.from_store ctxt ["SignalProcessing", "Z_Transform", "Inverse"];
984 section \<open>Program in TP-based language \label{prog-steps}\<close>
986 text\<open>\noindent We start stepwise expanding our program. The script is a
987 simple string containing several manipulation instructions.
988 \par The first script we try contains no instruction, we only test if
989 building scripts that way work.\<close>
991 subsection \<open>Stepwise Extend the Program\<close>
994 "Program InverseZTransform (Xeq::bool) = "^
998 text\<open>\noindent Next we put some instructions in the script and try if we are
999 able to solve our first equation.\<close>
1003 "Program InverseZTransform (Xeq::bool) = "^
1005 * 1/z) instead of z \<up> -1
1007 " (let X = Take Xeq; "^
1008 " X' = Rewrite ruleZY False X; "^
1012 " X' = (Rewrite_Set norm_Rational False) X' "^
1020 "Program InverseZTransform (Xeq::bool) = "^
1022 * (1/z) instead of z \<up> -1
1024 " (let X = Take Xeq; "^
1025 " X' = Rewrite ruleZY False X; "^
1029 " X' = (Rewrite_Set norm_Rational False) X'; "^
1033 " X' = (SubProblem (IsacX,[pqFormula,degree_2, "^
1034 " polynomial,univariate,equation], "^
1036 " [BOOL e_e, REAL v_v]) "^
1040 text\<open>\noindent To solve the equation it is necessary to drop the left hand
1041 side, now we only need the denominator of the right hand side. The first
1042 equation solves the zeros of our expression.\<close>
1046 "Program InverseZTransform (Xeq::bool) = "^
1047 " (let X = Take Xeq; "^
1048 " X' = Rewrite ruleZY False X; "^
1049 " X' = (Rewrite_Set norm_Rational False) X'; "^
1050 " funterm = rhs X' "^
1052 * drop X'= for equation solving
1057 text\<open>\noindent As mentioned above, we need the denominator of the right hand
1058 side. The equation itself consists of this denominator and tries to find
1059 a $z$ for this the denominator is equal to zero.\<close>
1061 text \<open> dropped during switch from Program to partial_function:
1063 "Program InverseZTransform (X_eq::bool) = "^
1064 " (let X = Take X_eq; "^
1065 " X' = Rewrite ruleZY False X; "^
1066 " X' = (Rewrite_Set norm_Rational False) X'; "^
1067 " (X'_z::real) = lhs X'; "^
1068 " (z::real) = argument_in X'_z; "^
1069 " (funterm::real) = rhs X'; "^
1070 " (denom::real) = get_denominator funterm; "^
1074 " (equ::bool) = (denom = (0::real)); "^
1075 " (L_L::bool list) = "^
1076 " (SubProblem (Test, "^
1077 " [LINEAR,univariate,equation,test], "^
1078 " [Test,solve_linear]) "^
1079 " [BOOL equ, REAL z]) "^
1083 val sc = (inst_abs o Thm.term_of o the o (parse thy)) str;
1087 text \<open>\noindent This ruleset contains all functions that are in the script;
1088 The evaluation of the functions is done by rewriting using this ruleset.\<close>
1092 Rule_Set.Repeat {id="srls_InverseZTransform",
1094 rew_ord = ("termlessI",termlessI),
1095 asm_rls = Rule_Set.append_rules "erls_in_srls_InverseZTransform" Rule_Set.empty
1096 [(*for asm in NTH_CONS ...*)
1097 Eval (\<^const_name>\<open>less\<close>,eval_equ "#less_"),
1098 (*2nd NTH_CONS pushes n+-1 into asms*)
1099 Eval(\<^const_name>\<open>plus\<close>, Calc_Binop.numeric "#add_")
1101 prog_rls = Rule_Set.Empty, calc = [], errpatts = [],
1103 Thm ("NTH_CONS",ThmC.numerals_to_Free @{thm NTH_CONS}),
1104 Eval(\<^const_name>\<open>plus\<close>, Calc_Binop.numeric "#add_"),
1105 Thm ("NTH_NIL",ThmC.numerals_to_Free @{thm NTH_NIL}),
1106 Eval("Prog_Expr.lhs", eval_lhs"eval_lhs_"),
1107 Eval("Prog_Expr.rhs", eval_rhs"eval_rhs_"),
1108 Eval("Prog_Expr.argument'_in", eval_argument_in "Prog_Expr.argument'_in"),
1109 Eval("Rational.get_denominator", eval_get_denominator "#get_denominator"),
1110 Eval("Rational.get_numerator", eval_get_numerator "#get_numerator"),
1111 Eval("Partial_Fractions.factors_from_solution",
1112 eval_factors_from_solution "#factors_from_solution"),
1113 Eval("Partial_Fractions.drop_questionmarks",
1114 eval_drop_questionmarks "#drop_?")
1116 program = Empty_Prog};
1120 subsection \<open>Store Final Version of Program for Execution\<close>
1122 text\<open>\noindent After we also tested how to write scripts and run them,
1123 we start creating the final version of our script and store it into
1124 the method for which we created a node in Section~\ref{sec:cparentnode}
1125 Note that we also did this stepwise, but we didn't kept every
1128 setup \<open>Know_Store.add_mets
1129 [MethodC.prep_input thy "met_SP_Ztrans_inv" [] e_metID
1130 (["SignalProcessing", "Z_Transform", "Inverse"],
1131 [("#Given" , ["filterExpression X_eq"]), (*TODO boundVariable X_z*)
1132 ("#Find", ["stepResponse n_eq"])],
1133 {rew_ord="tless_true", rls'= Rule_Set.empty, calc = [], prog_rls = prog_rls, where_rls = Rule_Set.empty, crls = Rule_Set.empty,
1134 errpats = [], rew_rls = Rule_Set.empty},
1135 "Program InverseZTransform (X_eq::bool) = "^
1136 (*(1/z) instead of z \<up> -1*)
1137 "(let X = Take X_eq; "^
1138 " X' = Rewrite ruleZY False X; "^
1140 " (num_orig::real) = get_numerator (rhs X'); "^
1141 " X' = (Rewrite_Set norm_Rational False) X'; "^
1143 " (X'_z::real) = lhs X'; "^
1144 " (zzz::real) = argument_in X'_z; "^
1145 " (funterm::real) = rhs X'; "^
1146 (*drop X' z = for equation solving*)
1147 " (denom::real) = get_denominator funterm; "^
1149 " (num::real) = get_numerator funterm; "^
1151 " (equ::bool) = (denom = (0::real)); "^
1152 " (L_L::bool list) = (SubProblem (PolyEqX, "^
1153 " [abcFormula,degree_2,polynomial,univariate,equation], "^
1155 " [BOOL equ, REAL zzz]); "^
1156 " (facs::real) = factors_from_solution L_L; "^
1157 " (eql::real) = Take (num_orig / facs); "^
1159 " (eqr::real) = (Try (Rewrite_Set ansatz_rls False)) eql; "^
1161 " (eq::bool) = Take (eql = eqr); "^
1162 (*Maybe possible to use HOLogic.mk_eq ??*)
1163 " eq = (Try (Rewrite_Set equival_trans False)) eq; "^
1165 " eq = drop_questionmarks eq; "^
1166 " (z1::real) = (rhs (NTH 1 L_L)); "^
1168 * prepare equation for a - eq_a
1169 * therefor substitute z with solution 1 - z1
1171 " (z2::real) = (rhs (NTH 2 L_L)); "^
1173 " (eq_a::bool) = Take eq; "^
1174 " eq_a = (Substitute [zzz=z1]) eq; "^
1175 " eq_a = (Rewrite_Set norm_Rational False) eq_a; "^
1176 " (sol_a::bool list) = "^
1177 " (SubProblem (IsacX, "^
1178 " [univariate,equation],[no_met]) "^
1179 " [BOOL eq_a, REAL (A::real)]); "^
1180 " (a::real) = (rhs(NTH 1 sol_a)); "^
1182 " (eq_b::bool) = Take eq; "^
1183 " eq_b = (Substitute [zzz=z2]) eq_b; "^
1184 " eq_b = (Rewrite_Set norm_Rational False) eq_b; "^
1185 " (sol_b::bool list) = "^
1186 " (SubProblem (IsacX, "^
1187 " [univariate,equation],[no_met]) "^
1188 " [BOOL eq_b, REAL (B::real)]); "^
1189 " (b::real) = (rhs(NTH 1 sol_b)); "^
1191 " eqr = drop_questionmarks eqr; "^
1192 " (pbz::real) = Take eqr; "^
1193 " pbz = ((Substitute [A=a, B=b]) pbz); "^
1195 " pbz = Rewrite ruleYZ False pbz; "^
1196 " pbz = drop_questionmarks pbz; "^
1198 " (X_z::bool) = Take (X_z = pbz); "^
1199 " (n_eq::bool) = (Rewrite_Set inverse_z False) X_z; "^
1200 " n_eq = drop_questionmarks n_eq "^
1205 subsection \<open>Check the Program\<close>
1206 text\<open>\noindent When the script is ready we can start checking our work.\<close>
1207 subsubsection \<open>Check the Formalization\<close>
1208 text\<open>\noindent First we want to check the formalization of the in and
1209 output of our program.\<close>
1213 ["filterExpression (X = 3 / (z - 1/4 + -1/8 * (1/(z::real))))",
1214 "stepResponse (x[n::real]::bool)"];
1216 ("Isac_Knowledge", ["Inverse", "Z_Transform", "SignalProcessing"],
1217 ["SignalProcessing", "Z_Transform", "Inverse"]);
1224 Const ("Inverse_Z_Transform.filterExpression", _),
1225 [Const (\<^const_name>\<open>HOL.eq\<close>, _) $ _ $ _]
1231 Const ("Inverse_Z_Transform.stepResponse", _),
1235 ) = O_Model.init thy fmz ((#model o Problem.from_store) pI);
1238 = (#program o MethodC.from_store ctxt) ["SignalProcessing",
1244 subsubsection \<open>Stepwise Check the Program\label{sec:stepcheck}\<close>
1245 text\<open>\noindent We start to stepwise execute our new program in a calculation
1246 tree and check if every node implements that what we have wanted.\<close>
1249 Rewrite.trace_on := false; (*true false*)
1250 LItool.trace_on := false; (*true*)
1254 ["filterExpression (X z = 3 / ((z::real) + 1/10 - 1/50*(1/z)))",
1255 "stepResponse (x[n::real]::bool)"];
1258 ("Isac_Knowledge", ["Inverse", "Z_Transform", "SignalProcessing"],
1259 ["SignalProcessing", "Z_Transform", "Inverse"]);
1261 val (p,_,f,nxt,_,pt) = Test_Code.init_calc @{context} [(fmz, (dI,pI,mI))];
1262 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1264 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1266 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1268 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1270 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1272 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1274 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1275 "Rewrite (ruleZY, Inverse_Z_Transform.ruleZY)";
1276 "--> X z = 3 / (z - 1 / 4 + -1 / 8 * (1 / z))";
1280 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1281 "Rewrite_Set norm_Rational";
1282 " --> X' z = 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))";
1283 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1288 text \<open>\noindent Instead of \ttfamily nxt = Subproblem \normalfont above we had
1289 \ttfamily Empty\_Tac; \normalfont the search for the reason considered
1290 the following points:\begin{itemize}
1291 \item What shows \ttfamily show\_pt pt;\normalfont\ldots?
1292 \begin{verbatim}(([2], Res), ?X' z = 24 / (-1 + -2 * z + 8 * z \<up> 2))]\end{verbatim}
1293 The calculation is ok but no \ttfamily next \normalfont step found:
1294 Should be\\ \ttfamily nxt = Subproblem\normalfont!
1295 \item What shows \ttfamily trace\_script := true; \normalfont we read
1298 @@@next leaf 'SubProblem
1299 (PolyEq',[abcFormula, degree_2, polynomial,
1300 univariate, equation], no_meth)
1302 ---> Program.Tac 'SubProblem (PolyEq',
1303 [abcFormula, degree_2, polynomial,
1304 univariate, equation], no_meth)
1305 [BOOL (-1 + -2 * z + 8 * z \^\^\^ ~2 = 0), REAL z]'
1307 We see the SubProblem with correct arguments from searching next
1308 step (program text !!!--->!!! Program.Tac (script tactic) with arguments
1310 \item Do we have the right Program \ldots difference in the
1311 arguments in the arguments\ldots
1314 (#program o MethodC.from_store ctxt) ["SignalProcessing",
1317 writeln (UnparseC.term s);
1319 \ldots shows the right script. Difference in the arguments.
1320 \item Test --- Why helpless here ? --- shows: \ttfamily replace
1321 no\_meth by [no\_meth] \normalfont in Program
1326 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1330 text \<open>\noindent Instead of \ttfamily nxt = Model\_Problem \normalfont above
1331 we had \ttfamily Empty\_Tac; \normalfont the search for the reason
1332 considered the following points:\begin{itemize}
1333 \item Difference in the arguments
1334 \item Comparison with Subsection~\ref{sec:solveq}: There solving this
1335 equation works, so there must be some difference in the arguments
1336 of the Subproblem: RIGHT: we had \ttfamily [no\_meth] \normalfont
1337 instead of \ttfamily [no\_met] \normalfont ;-)
1338 \end{itemize}\<close>
1341 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1342 (*Add_Given equality (-1 + -2 * z + 8 * z \<up> 2 = 0)";*)
1343 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1344 (*Add_Given solveFor z";*)
1345 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1346 (*Add_Find solutions z_i";*)
1347 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1348 (*Specify_Theory Isac";*)
1351 text \<open>\noindent We had \ttfamily nxt = Empty\_Tac instead Specify\_Theory;
1352 \normalfont The search for the reason considered the following points:
1354 \item Was there an error message? NO -- ok
1355 \item Has \ttfamily nxt = Add\_Find \normalfont been inserted in pt:\\
1356 \ttfamily get\_obj g\_pbl pt (fst p);\normalfont? YES -- ok
1357 \item What is the returned formula:
1359 print_depth 999; f; print_depth 3;
1360 { Find = [ Correct "solutions z_i"],
1362 Given = [Correct "equality (-1 + -2*z + 8*z \<up> 2 = 0)",
1363 Correct "solveFor z"],
1367 \normalfont The only False is the reason: the Where (the precondition) is
1368 False for good reasons: The precondition seems to check for linear
1369 equations, not for the one we want to solve! Removed this error by
1370 correcting the Program from \ttfamily SubProblem (PolyEq',
1371 \lbrack linear,univariate,equation,
1372 test\rbrack, \lbrack Test,solve\_linear\rbrack \normalfont to
1373 \ttfamily SubProblem (PolyEq',\\ \lbrack abcFormula,degree\_2,
1374 polynomial,univariate,equation\rbrack,\\
1375 \lbrack PolyEq,solve\_d2\_polyeq\_abc\_equation
1377 You find the appropriate type of equation at the
1378 {\sisac}-WEB-Page\footnote{
1379 \href{http://www.ist.tugraz.at/projects/isac/www/kbase/pbl/index\_pbl.html}
1380 {http://www.ist.tugraz.at/projects/isac/www/kbase/pbl/index\_pbl.html}
1382 And the respective method in \ttfamily Knowledge/PolyEq.thy \normalfont
1383 at the respective \ttfamily store\_pbt. \normalfont Or you leave the
1384 selection of the appropriate type to isac as done in the final Program ;-))
1385 \end{itemize}\<close>
1388 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1389 (*Specify_Problem [abcFormula,...";*)
1390 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1391 (*Specify_Method [PolyEq,solve_d2_polyeq_abc_equation";*)
1392 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1393 (*Apply_Method [PolyEq,solve_d2_polyeq_abc_equation";*)
1394 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1395 (*Rewrite_Set_Inst [(''bdv'', z)], d2_polyeq_abcFormula_simplify";*)
1396 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1397 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1398 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1399 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1400 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1401 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1402 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1403 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1404 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1405 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1406 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1407 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1408 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1409 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1410 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1411 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1412 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1413 (*Specify_Problem ["normalise", "polynomial", "univariate", "equation"]*)
1414 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1415 (*Specify_Method ["PolyEq", "normalise_poly"]*)
1416 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1417 (*Apply_Method ["PolyEq", "normalise_poly"]*)
1418 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1419 (*Rewrite ("all_left", "PolyEq.all_left")*)
1420 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1421 (*Rewrite_Set_Inst (["(''bdv'', A)"], "make_ratpoly_in")*)
1422 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1423 (*Rewrite_Set "polyeq_simplify"*)
1424 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1425 (*Subproblem("Isac_Knowledge",["degree_1", "polynomial", "univariate", "equation"])*)
1426 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1427 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1428 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1429 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1430 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1431 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1432 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1433 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1434 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1435 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1436 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1437 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1438 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1439 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1440 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1441 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1442 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1443 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1444 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1445 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1446 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1447 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1448 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1449 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1450 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1451 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1452 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1453 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1454 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1455 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1456 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1457 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1458 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1459 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1460 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1461 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1462 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1463 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1464 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1465 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1466 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1467 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1468 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1469 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1470 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1471 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*([11, 4, 5], Res) Check_Postcond*)
1472 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*([11, 4], Res) Check_Postcond*)
1473 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*([11], Res) Take*)
1474 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*([12], Frm) Substitute*)
1475 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*([12], Res) Rewrite*)
1476 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*([13], Res) Take*)
1477 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*([14], Frm) Empty_Tac*)
1480 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1483 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1486 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1489 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1492 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1495 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1499 LItool.trace_on := true;
1502 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1505 Test_Tool.show_pt pt;
1520 text\<open>\noindent As a last step we check the tracing output of the last calc
1521 tree instruction and compare it with the where_-calculated result.\<close>
1523 section \<open>Improve and Transfer into Knowledge\<close>
1525 We want to improve the very long program \ttfamily InverseZTransform
1526 \normalfont by modularisation: partial fraction decomposition shall
1527 become a sub-problem.
1529 We could transfer all knowledge in \ttfamily Build\_Inverse\_Z\_Transform.thy
1530 \normalfont first to the \ttfamily Knowledge/Inverse\_Z\_Transform.thy
1531 \normalfont and then modularise. In this case TODO problems?!?
1533 We chose another way and go bottom up: first we build the sub-problem in
1534 \ttfamily Partial\_Fractions.thy \normalfont with the term:
1536 $$\frac{3}{x\cdot(z - \frac{1}{4} + \frac{-1}{8}\cdot\frac{1}{z})}$$
1538 \noindent (how this still can be improved see \ttfamily Partial\_Fractions.thy\normalfont),
1539 and re-use all stuff prepared in \ttfamily Build\_Inverse\_Z\_Transform.thy:
1540 \normalfont The knowledge will be transferred to \ttfamily src/../Partial\_Fractions.thy
1541 \normalfont and the respective tests to:
1542 \begin{center}\ttfamily test/../sartial\_fractions.sml\normalfont\end{center}
1545 subsection \<open>Transfer to Partial\_Fractions.thy\<close>
1547 First we transfer both, knowledge and tests into:
1548 \begin{center}\ttfamily src/../Partial\_Fractions.thy\normalfont\end{center}
1549 in order to immediately have the test results.
1551 We copy \ttfamily factors\_from\_solution, drop\_questionmarks,\\
1552 ansatz\_2nd\_order \normalfont and rule-sets --- no problem.
1554 Also \ttfamily store\_pbt ..\\ "pbl\_simp\_rat\_partfrac"
1555 \normalfont is easy.
1557 But then we copy from:\\
1558 (1) \ttfamily Build\_Inverse\_Z\_Transform.thy store\_met\ldots "met\_SP\_Ztrans\_inv"
1560 (2) \ttfamily Partial\_Fractions.thy store\_met\ldots "met\_SP\_Ztrans\_inv"
1561 \normalfont\\ and cut out the respective part from the program. First we ensure that
1562 the string is correct. When we insert the string into (2)
1563 \ttfamily store\_met .. "met\_partial\_fraction" \normalfont --- and get an error.
1566 subsubsection \<open>'Programming' in ISAC's TP-based Language\<close>
1568 At the present state writing programs in {\sisac} is particularly cumbersome.
1569 So we give hints how to cope with the many obstacles. Below we describe the
1570 steps we did in making (2) run.
1573 \item We check if the \textbf{string} containing the program is correct.
1574 \item We check if the \textbf{types in the program} are correct.
1575 For this purpose we start start with the first and last lines
1577 "PartFracScript (f_f::real) (v_v::real) = " ^
1578 " (let X = Take f_f; " ^
1579 " pbz = ((Substitute []) X) " ^
1582 The last but one line helps not to bother with ';'.
1583 \item Then we add line by line. Already the first line causes the error.
1584 So we investigate it by
1586 val ctxt = Proof_Context.init_global @{theory "Inverse_Z_Transform"} ;
1588 parseNEW ctxt "(num_orig::real) =
1589 get_numerator(rhs f_f)";
1591 and see a type clash: \ttfamily rhs \normalfont from (1) requires type
1592 \ttfamily bool \normalfont while (2) wants to have \ttfamily (f\_f::real).
1593 \normalfont Of course, we don't need \ttfamily rhs \normalfont anymore.
1594 \item Type-checking can be very tedious. One might even inspect the
1595 parse-tree of the program with {\sisac}'s specific debug tools:
1597 val {program = Prog t,...} =
1598 MethodC.from_store ctxt ["simplification",
1600 "to_partial_fraction"];
1601 atomty_thy @{theory "Inverse_Z_Transform"} t ;
1603 \item We check if the \textbf{semantics of the program} by stepwise evaluation
1604 of the program. Evaluation is done by the Lucas-Interpreter, which works
1605 using the knowledge in theory Isac_Knowledge; so we have to re-build Isac. And the
1606 test are performed simplest in a file which is loaded with Isac.
1607 See \ttfamily tests/../partial\_fractions.sml \normalfont.
1611 subsection \<open>Transfer to Inverse\_Z\_Transform.thy\<close>
1613 It was not possible to complete this task, because we ran out of time.