wneuper/isa: comparison test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z

equal deleted inserted replaced

-:a8471740e3b0
+:8b94d811cb41
 (c) copyright due to license terms.
 12345678901234567890123456789012345678901234567890123456789012345678901234567890
 10        20        30        40        50        60        70        80
 *)
-header{* Build_Inverse_Z_Transform *}
 theory Build_Inverse_Z_Transform imports Isac
 begin
 text{* We stepwise build \ttfamily Inverse\_Z\_Transform.thy \normalfont as an
-exercise. Because subsection~\ref{sec:stepcheck} requires
+exercise. Because Subsection~\ref{sec:stepcheck} requires
 \ttfamily Inverse\_Z\_Transform.thy \normalfont as a subtheory of \ttfamily
 Isac.thy\normalfont, the setup has been changed from \ttfamily theory
 Inverse\_Z\_Transform imports Isac \normalfont to the above one.
 \par \noindent
 \begin{center}
-\textbf{ATTENTION WITH NAMES OF IDENTIFIERS WHEN GOING INTO INTERNALS}
+\textbf{Attention with the names of identifiers when going into internals!}
 \end{center}
 Here in this theory there are the internal names twice, for instance we have
 \ttfamily (Thm.derivation\_name @{thm rule1} =
 "Build\_Inverse\_Z\_Transform.rule1") = true; \normalfont
 but actually in us will be \ttfamily Inverse\_Z\_Transform.rule1 \normalfont
 atomty solutions;
 *}
 subsubsection {*Get Solutions out of a List*}
 text {*\noindent In {\sisac}'s TP-based programming language:
-\ttfamily let\$ \$s\_1 = NTH 1\$ solutions; \$s\_2 = NTH 2...\$ \normalfont
+\begin{verbatim}
-can be useful.*}
+let $ $ s_1 = NTH 1 $ solutions; $ s_2 = NTH 2... $
+\end{verbatim}
+can be useful.
+*}
 ML {*
 val Const ("List.list.Cons", _) $ s_1 $ (Const ("List.list.Cons", _)
 $ s_2 $ Const ("List.list.Nil", _)) = solutions;
 term2str s_1;
 text{*\noindent The ansatz for the \em Partial Fraction Decomposition \normalfont
 requires to get the denominators of the partial fractions out of the
 Solutions as:
 \begin{itemize}
-\item $ \text{Denominator} _{1} = z - \text{Zeropoint}_{1}$
+\item $Denominator_{1}=z-Zeropoint_{1}$
-\item $ \text{Denominator} _{2} = z - \text{Zeropoint}_{2}$
+\item $Denominator_{2}=z-Zeropoint_{2}$
 \item \ldots
-\end{itemize}*}
+\end{itemize}
+*}
 ML {*
 val xx = HOLogic.dest_eq s_1;
 val s_1' = HOLogic.mk_binop "Groups.minus_class.minus" xx;
 val xx = HOLogic.dest_eq s_2;
 *} *)
 text {*\noindent This function needs to be packed such that it can be evaluated
 by the Lucas-Interpreter. Therefor we moved the function to the
 corresponding \ttfamily Equation.thy \normalfont in our case
 \ttfamily PartialFractions.thy \normalfont. The necessary steps
-are quit the same as we have done with \ttfamliy get\_denominator
+are quit the same as we have done with \ttfamily get\_denominator
 \normalfont before.*}
 ML {*
 (*("factors_from_solution",
 ("Partial_Fractions.factors_from_solution",
 eval_factors_from_solution ""))*)
 handle _ => NONE)
 | eval_factors_from_solution _ _ _ _ = NONE;
 *}
 text {*\noindent The tracing output of the calc tree after applying this
-function was \ttfamily 24 / factors\_from\_solution
+function was:
-[z = 1/ 2, z = -1 / 4])] \normalfont and the next step \ttfamily
+\begin{verbatim}
-val nxt = ("Empty\_Tac", ...): tac'\_)\normalfont. These observations
+24 / factors_from_solution [z = 1/ 2, z = -1 / 4])]
-indicate, that the Lucas-Interpreter (LIP) does not know how to
+\end{verbatim}
-evaluate\\ \ttfamily factors\_from\_solution, \normalfont so we knew
+and the next step:
-that there is something wrong or missing.*}
+\begin{verbatim}
+val nxt = ("Empty_Tac", ...): tac'_)
+\end{verbatim}
+These observations indicate, that the Lucas-Interpreter (LIP)
+does not know how to evaluate \ttfamily factors\_from\_solution
+\normalfont, so we knew that there is something wrong or missing.
+*}
-text{*\noindent First we isolate the difficulty in the program as follows:\\
+text{*\noindent First we isolate the difficulty in the program as follows:
-\ttfamily \par \noindent
+\begin{verbatim}
-"(L\_L::bool list) = (SubProblem (PolyEq',"\^\\
+" (L_L::bool list) = (SubProblem (PolyEq',      " ^
-"[abcFormula,degree\_2,polynomial,univariate,equation],[no\_met])"\^\\
+"   [abcFormula, degree_2, polynomial,          " ^
-"[BOOL equ, REAL zzz]);"\^\\
+"    univariate,equation],                      " ^
-"(facs::real) = factors\_from\_solution L\_L;"\^\\
+"   [no_met])                                   " ^
-"(foo::real) = Take facs"\^\\
+"   [BOOL equ, REAL zzz]);                      " ^
+" (facs::real) = factors_from_solution L_L;     " ^
+" (foo::real) = Take facs                       " ^
+\end{verbatim}
+\par \noindent And see the tracing output:
+\begin{verbatim}
+[(([], Frm), Problem (Isac, [inverse,
+Z_Transform,
+SignalProcessing])),
+(([1], Frm), X z = 3 / (z - 1 / 4 + -1 / 8 * (1 / z))),
+(([1], Res), ?X' z = 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))),
+(([2], Res), ?X' z = 24 / (-1 + -2 * z + 8 * z ^^^ 2)),
+(([3], Pbl), solve (-1 + -2 * z + 8 * z ^^^ 2 = 0, z)),
+(([3,1], Frm), -1 + -2 * z + 8 * z ^^^ 2 = 0),
+(([3,1], Res), z = (- -2 + sqrt (-2 ^^^ 2 - 4 * 8 * -1)) / (2 * 8)|
+z = (- -2 - sqrt (-2 ^^^ 2 - 4 * 8 * -1)) / (2 * 8)),
+(([3,2], Res), z = 1 / 2 | z = -1 / 4),
+(([3,3], Res), [ z = 1 / 2, z = -1 / 4]),
+(([3,4], Res), [ z = 1 / 2, z = -1 / 4]),
+(([3], Res), [ z = 1 / 2, z = -1 / 4]),
+(([4], Frm), factors_from_solution [z = 1 / 2, z = -1 / 4])]
+\end{verbatim}
+\par \noindent In particular that:
+\begin{verbatim}
+(([3], Pbl), solve (-1 + -2 * z + 8 * z ^^^ 2 = 0, z)),
+\end{verbatim}
+\par \noindent Shows the equation which has been created in
+the program by:
+\begin{verbatim}
+"(denom::real) = get_denominator funterm;      " ^
+(* get_denominator *)
+"(equ::bool) = (denom = (0::real));            " ^
+\end{verbatim}
-\normalfont \par \noindent And see the tracing output:\\
+\noindent \ttfamily get\_denominator \normalfont has been evaluated successfully,
-\ttfamily \par \noindent \lbrack\\
-((\lbrack\rbrack, Frm), Problem
-(Isac, \lbrack inverse, Z\_Transform, SignalProcessing\rbrack)),\\
-((\lbrack 1\rbrack, Frm), X z = 3 / (z - 1 / 4 + -1 / 8 * (1 / z))),\\
-((\lbrack 1\rbrack, Res),
-?X' z = 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))),\\
-((\lbrack 2\rbrack, Res),
-?X' z = 24 / (-1 + -2 * z + 8 * z \^\^\^ ~2)),\\
-((\lbrack 3\rbrack, Pbl),
-solve (-1 + -2 * z + 8 * z \^\^\^ ~2 = 0, z)),\\
-((\lbrack 3,1\rbrack, Frm), -1 + -2 * z + 8 * z \^\^\^ ~2 = 0),\\
-((\lbrack 3,1\rbrack, Res),
-z = (- -2 + sqrt (-2 \^\^\^ ~2 - 4 * 8 * -1)) / (2 * 8)|\\
-z = (- -2 - sqrt (-2 \^\^\^ ~2 - 4 * 8 * -1)) / (2 * 8)),\\
-((\lbrack 3,2\rbrack, Res), z = 1 / 2 | z = -1 / 4),\\
-((\lbrack 3,3\rbrack, Res), \lbrack z = 1 / 2, z = -1 / 4\rbrack),\\
-((\lbrack 3,4\rbrack, Res), \lbrack z = 1 / 2, z = -1 / 4\rbrack),\\
-((\lbrack 3\rbrack, Res), \lbrack z = 1 / 2, z = -1 / 4\rbrack),\\
-((\lbrack 4\rbrack, Frm),
-factors\_from\_solution \lbrackz = 1 / 2, z = -1 / 4])\\
-\rbrack\\
-\normalfont \noindent In particular that:\\
-\ttfamily \par \noindent ((\lbrack 3\rbrack, Pbl),
-solve (-1 + -2 * z + 8 * z \^\^\^ ~2 = 0, z)),\\
-\normalfont \par \noindent Shows the equation which has been created in
-the program by: \ttfamily \\
-\noindent "(denom::real) = get\_denominator funterm;"\^
-~(*get\_denominator*)\\
-"(equ::bool) = (denom = (0::real));"\^\\
-\noindent get\_denominator \normalfont has been evaluated successfully,
 but not\\ \ttfamily factors\_from\_solution.\normalfont
 So we stepwise compare with an analogous case, \ttfamily get\_denominator
 \normalfont successfully done above: We know that LIP evaluates
 expressions in the program by use of the \emph{srls}, so we try to get
 the original \emph{srls}.\\
-\noindent \ttfamily val \lbrace srls,\ldots\rbrace\ttfamily
+\begin{verbatim}
-= get\_met \lbrack "SignalProcessing",
+val {srls,...} = get_met ["SignalProcessing",
-"Z\_Transform","inverse"\rbrack;\\
+"Z_Transform",
+"inverse"];
+\end{verbatim}
-\par \noindent \normalfont Create 2 good example terms\\
+\par \noindent Create 2 good example terms:
-\ttfamily \par \noindent val SOME t1 =\\
-parseNEW ctxt "get\_denominator ((111::real) / 222)";
+\begin{verbatim}
-\par \noindent val SOME t2 =\\
+val SOME t1 =
-parseNEW ctxt "factors\_from\_solution \lbrack(z::real)
+parseNEW ctxt "get_denominator ((111::real) / 222)";
-= 1/2, z = -1/4\rbrack";\\
+val SOME t2 =
+parseNEW ctxt "factors_from_solution [(z::real)=1/2, z=-1/4]";
-\par \noindent \normalfont Rewrite the terms using srls:\\
+\end{verbatim}
+\par \noindent Rewrite the terms using srls:\\
 \ttfamily \par \noindent rewrite\_set\_ thy true srls t1;\\
 rewrite\_set\_ thy true srls t2;\\
 \par \noindent \normalfont Now we see a difference: \texttt{t1} gives
 \texttt{SOME} but \texttt{t2} gives \texttt{NONE}. We look at the
-\emph{srls}:\\
+\emph{srls}:
+\begin{verbatim}
-\par \noindent \ttfamily  val srls = Rls \lbrace id =
+val srls =
-"srls\_InverseZTransform", rules =\\
+Rls{id = "srls_InverseZTransform",
-\lbrack Calc("Rational.get\_numerator",\\
+rules = [Calc("Rational.get_numerator",
-eval\_get\_numerator "Rational.get\_numerator"),\\
+eval_get_numerator "Rational.get_numerator"),
-Calc("Partial\_Fractions.factors\_from\_solution",\\
+Calc("Partial_Fractions.factors_from_solution",
-eval\_factors\_from\_solution
+eval_factors_from_solution
-"Partial\_Fractions.factors\_from\_solution")\rbrack\rbrace\\
+"Partial_Fractions.factors_from_solution")]}
+\end{verbatim}
-\par \noindent \normalfont Here everthing is perfect. So the error can
+\par \noindent Here everthing is perfect. So the error can
 only be in the SML code of \ttfamily eval\_factors\_from\_solution.
 \normalfont We try to check the code with an existing test; since the
 \emph{code} is in
 \begin{center}\ttfamily src/Tools/isac/Knowledge/Partial\_Fractions.thy
 \normalfont\end{center}
 partial\_fractions.sml \normalfont is used in \ttfamily Test\_Isac.thy
 \normalfont
 \begin{center}use \ttfamily "Knowledge/partial\_fractions.sml"
 \normalfont \end{center}
 and \ttfamily Partial\_Fractions.thy \normalfont is part is part of
-{\sisac} by evaluating\\
+{\sisac} by evaluating
-\par \noindent \ttfamily val thy = @\lbrace theory~Isac \rbrace;
+\begin{verbatim}
-\normalfont \\
+val thy = @{theory Isac};
+\end{verbatim}
-\par \noindent \normalfont After rebuilding {\sisac} again it worked.
+After rebuilding {\sisac} again it worked.
 *}
 subsubsection {*Build Expression*}
 text {*\noindent In {\sisac}'s TP-based programming language we can build
 expressions by:\\
 Thm ("equival_trans_2nd_order",num_str @{thm equival_trans_2nd_order})
 ],
 scr = EmptyScr});
 *}
-text{*\noindent We apply the ruleset\lodts*}
+text{*\noindent We apply the ruleset\ldots*}
 ML {*
 val SOME (ttttt,_) =
 rewrite_set_ @{theory Isac} false ansatz_rls expr';
 *}
 text{*\noindent Now it's up to get the two coefficients A and B, which will be
 the numerators of our partial fractions. Continue following up the
 Calculation in Section~\ref{sec:calc:ztrans} Subproblem~1.*}
 text{*\noindent To get the first coefficient we substitute $z$ with the first
-zero-point we determined in section~\ref{sec:solveq}.*}
+zero-point we determined in Section~\ref{sec:solveq}.*}
 ML {*
 val SOME (eq4_1,_) =
 rewrite_terms_ @{theory Isac} e_rew_ord e_rls [s_1] eq3'';
 term2str eq4_1;
 interpreter knows.*}
 ML {*thy*}
 text{*\noindent To get the second coefficient we substitute $z$ with the second
-zero-point we determined in section~\ref{sec:solveq}.*}
+zero-point we determined in Section~\ref{sec:solveq}.*}
 ML {*
 val SOME (eq4b_1,_) =
 rewrite_terms_ @{theory Isac} e_rew_ord e_rls [s_2] eq3'';
 term2str eq4b_1;
 (["Z_Transform","SignalProcessing"], [], e_rls, NONE, []));
 *}
 text{*\noindent For the suddenly created node we have to define the input
 and output parameters. We already prepared their definition in
-section~\ref{sec:deffdes}.*}
+Section~\ref{sec:deffdes}.*}
 ML {*
 store_pbt
 (prep_pbt thy "pbl_SP_Ztrans_inv" [] e_pblID
 (["inverse", "Z_Transform", "SignalProcessing"],
 building scripts that way work.*}
 subsection {*Stepwise Extend the Program*}
 ML {*
 val str =
-"Script InverseZTransform (Xeq::bool) =" ^
+"Script InverseZTransform (Xeq::bool) =                          "^
 " Xeq";
 *}
 text{*\noindent Next we put some instructions in the script and try if we are
 able to solve our first equation.*}
 ML {*
 val str =
-"Script InverseZTransform (Xeq::bool) =" ^
+"Script InverseZTransform (Xeq::bool) =                          "^
 (*
 * 1/z) instead of z ^^^ -1
 *)
-" (let X = Take Xeq;" ^
+" (let X = Take Xeq;                                             "^
-"      X' = Rewrite ruleZY False X;" ^
+"      X' = Rewrite ruleZY False X;                              "^
 (*
 * z * denominator
 *)
-"      X' = (Rewrite_Set norm_Rational False) X'" ^
+"      X' = (Rewrite_Set norm_Rational False) X'                 "^
 (*
 * simplify
 *)
 "  in X)";
 (*
 * NONE
 *)
-"Script InverseZTransform (Xeq::bool) =" ^
+"Script InverseZTransform (Xeq::bool) =                          "^
 (*
 * (1/z) instead of z ^^^ -1
 *)
-" (let X = Take Xeq;" ^
+" (let X = Take Xeq;                                             "^
-"      X' = Rewrite ruleZY False X;" ^
+"      X' = Rewrite ruleZY False X;                              "^
 (*
 * z * denominator
 *)
-"      X' = (Rewrite_Set norm_Rational False) X';" ^
+"      X' = (Rewrite_Set norm_Rational False) X';                "^
 (*
 * simplify
 *)
-"      X' = (SubProblem (Isac',[pqFormula,degree_2," ^
+"      X' = (SubProblem (Isac',[pqFormula,degree_2,              "^
-"                               polynomial,univariate,equation]," ^
+"                               polynomial,univariate,equation], "^
-"                              [no_met])   " ^
+"                              [no_met])                         "^
-"                              [BOOL e_e, REAL v_v])" ^
+"                              [BOOL e_e, REAL v_v])             "^
 "            in X)";
 *}
 text{*\noindent To solve the equation it is necessary to drop the left hand
 side, now we only need the denominator of the right hand side. The first
 equation solves the zeros of our expression.*}
 ML {*
 val str =
-"Script InverseZTransform (Xeq::bool) =" ^
+"Script InverseZTransform (Xeq::bool) =                          "^
-" (let X = Take Xeq;" ^
+" (let X = Take Xeq;                                             "^
-"      X' = Rewrite ruleZY False X;" ^
+"      X' = Rewrite ruleZY False X;                              "^
-"      X' = (Rewrite_Set norm_Rational False) X';" ^
+"      X' = (Rewrite_Set norm_Rational False) X';                "^
-"      funterm = rhs X'" ^
+"      funterm = rhs X'                                          "^
 (*
 * drop X'= for equation solving
 *)
 "  in X)";
 *}
 side. The equation itself consists of this denominator and tries to find
 a $z$ for this the denominator is equal to zero.*}
 ML {*
 val str =
-"Script InverseZTransform (X_eq::bool) =" ^
+"Script InverseZTransform (X_eq::bool) =                         "^
-" (let X = Take X_eq;" ^
+" (let X = Take X_eq;                                            "^
-"      X' = Rewrite ruleZY False X;" ^
+"      X' = Rewrite ruleZY False X;                              "^
-"      X' = (Rewrite_Set norm_Rational False) X';" ^
+"      X' = (Rewrite_Set norm_Rational False) X';                "^
-"      (X'_z::real) = lhs X';" ^
+"      (X'_z::real) = lhs X';                                    "^
-"      (z::real) = argument_in X'_z;" ^
+"      (z::real) = argument_in X'_z;                             "^
-"      (funterm::real) = rhs X';" ^
+"      (funterm::real) = rhs X';                                 "^
-"      (denom::real) = get_denominator funterm;" ^
+"      (denom::real) = get_denominator funterm;                  "^
 (*
 * get_denominator
 *)
-"      (equ::bool) = (denom = (0::real));" ^
+"      (equ::bool) = (denom = (0::real));                        "^
-"      (L_L::bool list) =                                    " ^
+"      (L_L::bool list) =                                        "^
-"            (SubProblem (Test',                             " ^
+"            (SubProblem (Test',                                 "^
-"                         [linear,univariate,equation,test], " ^
+"                         [linear,univariate,equation,test],     "^
-"                         [Test,solve_linear])               " ^
+"                         [Test,solve_linear])                   "^
-"                         [BOOL equ, REAL z])                " ^
+"                         [BOOL equ, REAL z])                    "^
 "  in X)";
 parse thy str;
 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
 atomty sc;
 text {*\noindent This ruleset contains all functions that are in the script;
 The evaluation of the functions is done by rewriting using this ruleset.*}
 ML {*
-val srls = Rls {id="srls_InverseZTransform",
+val srls =
-preconds = [],
+Rls {id="srls_InverseZTransform",
-rew_ord = ("termlessI",termlessI),
+preconds = [],
-erls = append_rls "erls_in_srls_InverseZTransform" e_rls
+rew_ord = ("termlessI",termlessI),
-[(*for asm in NTH_CONS ...*)
+erls = append_rls "erls_in_srls_InverseZTransform" e_rls
-Calc ("Orderings.ord_class.less",eval_equ "#less_"),
+[(*for asm in NTH_CONS ...*)
-(*2nd NTH_CONS pushes n+-1 into asms*)
+Calc ("Orderings.ord_class.less",eval_equ "#less_"),
-Calc("Groups.plus_class.plus", eval_binop "#add_")
+(*2nd NTH_CONS pushes n+-1 into asms*)
-],
+Calc("Groups.plus_class.plus", eval_binop "#add_")
-srls = Erls, calc = [],
+],
-rules = [
+srls = Erls, calc = [],
-Thm ("NTH_CONS",num_str @{thm NTH_CONS}),
+rules = [
-Calc("Groups.plus_class.plus",
+Thm ("NTH_CONS",num_str @{thm NTH_CONS}),
-eval_binop "#add_"),
+Calc("Groups.plus_class.plus",
-Thm ("NTH_NIL",num_str @{thm NTH_NIL}),
+eval_binop "#add_"),
-Calc("Tools.lhs", eval_lhs"eval_lhs_"),
+Thm ("NTH_NIL",num_str @{thm NTH_NIL}),
-Calc("Tools.rhs", eval_rhs"eval_rhs_"),
+Calc("Tools.lhs", eval_lhs"eval_lhs_"),
-Calc("Atools.argument'_in",
+Calc("Tools.rhs", eval_rhs"eval_rhs_"),
-eval_argument_in "Atools.argument'_in"),
+Calc("Atools.argument'_in",
-Calc("Rational.get_denominator",
+eval_argument_in "Atools.argument'_in"),
-eval_get_denominator "#get_denominator"),
+Calc("Rational.get_denominator",
-Calc("Rational.get_numerator",
+eval_get_denominator "#get_denominator"),
-eval_get_numerator "#get_numerator"),
+Calc("Rational.get_numerator",
-Calc("Partial_Fractions.factors_from_solution",
+eval_get_numerator "#get_numerator"),
-eval_factors_from_solution
+Calc("Partial_Fractions.factors_from_solution",
-"#factors_from_solution"),
+eval_factors_from_solution
-Calc("Partial_Fractions.drop_questionmarks",
+"#factors_from_solution"),
-eval_drop_questionmarks "#drop_?")
+Calc("Partial_Fractions.drop_questionmarks",
-],
+eval_drop_questionmarks "#drop_?")
-scr = EmptyScr
+],
-};
+scr = EmptyScr};
 *}
 subsection {*Store Final Version of Program for Execution*}
 text{*\noindent After we also tested how to write scripts and run them,
 we start creating the final version of our script and store it into
-the method for which we created a node in section~\ref{sec:cparentnode}
+the method for which we created a node in Section~\ref{sec:cparentnode}
 Note that we also did this stepwise, but we didn't kept every
 subversion.*}
 ML {*
 store_met(
 *}
 text {*\noindent Instead of \ttfamily nxt = Subproblem \normalfont above we had
 \ttfamily Empty\_Tac; \normalfont the search for the reason considered
 the following points:\begin{itemize}
-\item What shows \ttfamily show\_pt pt;\normalfont\ldots?\\
+\item What shows \ttfamily show\_pt pt;\normalfont\ldots?
-\ttfamily ((\lbrack 2\rbrack, Res), ?X' z = 24 /
+\begin{verbatim}(([2], Res), ?X' z = 24 / (-1 + -2 * z + 8 * z ^^^ 2))]\end{verbatim}
-(-1 + -2 * z + 8 * z \^\^\^ ~2))\rbrack\normalfont\\
 The calculation is ok but no \ttfamily next \normalfont step found:
 Should be\\ \ttfamily nxt = Subproblem\normalfont!
 \item What shows \ttfamily trace\_script := true; \normalfont we read
-bottom up\ldots\\
+bottom up\ldots
-\ttfamily @@@next leaf 'SubProbfrom\\
+\begin{verbatim}
-(PolyEq',\\
+@@@next leaf 'SubProblem
-\lbrack abcFormula, degree\_2, polynomial, univariate,
+(PolyEq',[abcFormula, degree_2, polynomial,
-equation\rbrack,\\
+univariate, equation], no_meth)
-no\_meth)\\
+[BOOL equ, REAL z]'
-\lbrack BOOL equ, REAL z\rbrack' ---> STac 'SubProblem\\
+---> STac 'SubProblem (PolyEq',
-(PolyEq',\\
+[abcFormula, degree_2, polynomial,
-[abcFormula, degree\_2, polynomial, univariate, equation],\\
+univariate, equation], no_meth)
-no\_meth)\\
+[BOOL (-1 + -2 * z + 8 * z \^\^\^ ~2 = 0), REAL z]'
-\lbrack BOOL (-1 + -2 * z + 8 * z \^\^\^ ~2 = 0),
+\end{verbatim}
-REAL z\rbrack'\normalfont\\
 We see the SubProblem with correct arguments from searching next
 step (program text !!!--->!!! STac (script tactic) with arguments
 evaluated.)
 \item Do we have the right Script \ldots difference in the
-arguments in the arguments\ldots\\
+arguments in the arguments\ldots
-\ttfamily val Script s =\\
+\begin{verbatim}
-(#scr o get\_met) ["SignalProcessing","Z\_Transform","inverse"];\\
+val Script s =
-writeln (term2str s);\normalfont\\
+(#scr o get_met) ["SignalProcessing",
+"Z_Transform",
+"inverse"];
+writeln (term2str s);
+\end{verbatim}
 \ldots shows the right script. Difference in the arguments.
 \item Test --- Why helpless here ? --- shows: \ttfamily replace
 no\_meth by [no\_meth] \normalfont in Script
 \end{itemize}
 *}
 text {*\noindent Instead of \ttfamily nxt = Model\_Problem \normalfont above
 we had \ttfamily Empty\_Tac; \normalfont the search for the reason
 considered the following points:\begin{itemize}
 \item Difference in the arguments
-\item Comparison with subsection~ref{sec:solveq}: There solving this
+\item Comparison with Subsection~\ref{sec:solveq}: There solving this
 equation works, so there must be some difference in the arguments
 of the Subproblem: RIGHT: we had \ttfamily [no\_meth] \normalfont
 instead of \ttfamily [no\_met] \normalfont ;-)
 \end{itemize}*}
 \normalfont The search for the reason considered the following points:
 \begin{itemize}
 \item Was there an error message? NO -- ok
 \item Has \ttfamily nxt = Add\_Find \normalfont been inserted in pt:\\
 \ttfamily get\_obj g\_pbl pt (fst p);\normalfont? YES -- ok
 \item What is the returned formula:
-\ttfamily print\_depth 999; f; print\_depth 999;\\
+\begin{verbatim}
-\lbrace Find = \lbrack Correct "solutions z\_i"\rbrack,
+print_depth 999; f; print_depth 999;
-With = \lbrack\rbrack,\\
+{ Find = [ Correct "solutions z_i"],
-Given = \lbrack Correct "equality (-1 + -2 * z + 8 * z ^^^ 2 = 0)",
+With = [],
-Correct "solveFor z"\rbrack,\\
+Given = [Correct "equality (-1 + -2*z + 8*z ^^^ 2 = 0)",
-Where = \lbrack \ldots \rbrack,
+Correct "solveFor z"],
-Relate = \lbrack\rbrack\rbrace $ \normalfont\\
+Where = [...],
+Relate = [] }
+\end{verbatim}
 \normalfont The only False is the reason: the Where (the precondition) is
 False for good reasons: The precondition seems to check for linear
 equations, not for the one we want to solve! Removed this error by
 correcting the Script from \ttfamily SubProblem (PolyEq',
 \lbrack linear,univariate,equation,
 We could transfer all knowledge in \ttfamily Build\_Inverse\_Z\_Transform.thy
 \normalfont first to the \ttfamily Knowledge/Inverse\_Z\_Transform.thy
 \normalfont and then modularise. In this case TODO problems?!?
 We chose another way and go bottom up: first we build the sub-problem in
-\ttfamily Partial\_Fractions.thy \normalfont with the term
+\ttfamily Partial\_Fractions.thy \normalfont with the term:
-$$\frac{3}{x\cdot(z - \fract{1}{4} + \frac{-1}{8}\cdot\fract{1}{z})}$$
+$$\frac{3}{x\cdot(z - \frac{1}{4} + \frac{-1}{8}\cdot\frac{1}{z})}$$
-(how this still can be improved see \ttfamily Partial\_Fractions.thy \normalfont),
+\noindent (how this still can be improved see \ttfamily Partial\_Fractions.thy\normalfont),
 and re-use all stuff prepared in \ttfamily Build\_Inverse\_Z\_Transform.thy:
-The knowledge will be transferred to \ttfamily src/../Partial\_Fractions.thy
+\normalfont The knowledge will be transferred to \ttfamily src/../Partial\_Fractions.thy
-\normalfont and the respective tests to \ttfamily test/../sartial\_fractions.sml.
+\normalfont and the respective tests to:
+\begin{center}\ttfamily test/../sartial\_fractions.sml\normalfont\end{center}
 *}
 subsection {* Transfer to Partial\_Fractions.thy *}
 text {*
-First we transfer both, knowledge and tests into \ttfamily src/../Partial\_Fractions.thy
+First we transfer both, knowledge and tests into:
-\normalfont in order to immediately have the test results.
+\begin{center}\ttfamily src/../Partial\_Fractions.thy\normalfont\end{center}
+in order to immediately have the test results.
-We copy \ttfamily factors_from_solution, drop_questionmarks,
-ansatz_2nd_order \normalfont and rule-sets --- no problem.
+We copy \ttfamily factors\_from\_solution, drop\_questionmarks,\\
-Also \ttfamily store_pbt .. "pbl_simp_rat_partfrac"
+ansatz\_2nd\_order \normalfont and rule-sets --- no problem.
+Also \ttfamily store\_pbt ..\\ "pbl\_simp\_rat\_partfrac"
 \normalfont is easy.
-But then we copy from (1) \ttfamily Build\_Inverse\_Z\_Transform.thy
+But then we copy from:\\
-store_met .. "met_SP_Ztrans_inv" to (2) \ttfamily Partial\_Fractions.thy
+(1) \ttfamily Build\_Inverse\_Z\_Transform.thy store\_met\ldots "met\_SP\_Ztrans\_inv"
-store_met .. "met_SP_Ztrans_inv"
+\normalfont\\ to\\
-\normalfont and cut out the respective part from the program. First we ensure that
+(2) \ttfamily Partial\_Fractions.thy store\_met\ldots "met\_SP\_Ztrans\_inv"
+\normalfont\\ and cut out the respective part from the program. First we ensure that
 the string is correct. When we insert the string into (2)
-\ttfamily store_met .. "met_partial_fraction" \normalfont --- and get an error.
+\ttfamily store\_met .. "met\_partial\_fraction" \normalfont --- and get an error.
 *}
-subsubsection {* 'Programming' in \sisac}'s TP-based Language *}
+subsubsection {* 'Programming' in ISAC's TP-based Language *}
 text {*
 At the present state writing programs in {\sisac} is particularly cumbersome.
 So we give hints how to cope with the many obstacles. Below we describe the
 steps we did in making (2) run.
 \begin{enumerate}
 \item We check if the \textbf{string} containing the program is correct.
 \item We check if the \textbf{types in the program} are correct.
 For this purpose we start start with the first and last lines
 \begin{verbatim}
-"PartFracScript (f_f::real) (v_v::real) =                       " ^
+"PartFracScript (f_f::real) (v_v::real) =       " ^
-" (let X = Take f_f;                                            " ^
+" (let X = Take f_f;                            " ^
-"      pbz = ((Substitute []) X)                                " ^
+"      pbz = ((Substitute []) X)                " ^
 "  in pbz)"
 \end{verbatim}
 The last but one line helps not to bother with ';'.
 \item Then we add line by line. Already the first line causes the error.
 So we investigate it by
 \begin{verbatim}
-val ctxt = ProofContext.init_global @{theory};
+val ctxt = ProofContext.init_global @ { theory } ;
-val SOME t = parseNEW ctxt "(num_orig::real) = get_numerator (rhs f_f)";
+val SOME t =
-\end{verbatim}
+parseNEW ctxt "(num_orig::real) =
+get_numerator(rhs f_f)";
+\end{verbatim}
 and see a type clash: \ttfamily rhs \normalfont from (1) requires type
-\ttfamily bool \normalfont while (2) wants to have \ttfamily (f_f::real).
+\ttfamily bool \normalfont while (2) wants to have \ttfamily (f\_f::real).
 \normalfont Of course, we don't need \ttfamily rhs \normalfont anymore.
 \item Type-checking can be very tedious. One might even inspect the
-parse-tree of the program with \sisac's specific debug tools:
+parse-tree of the program with {\sisac}'s specific debug tools:
 \begin{verbatim}
-val {scr = Script t,...} = get_met ["simplification","of_rationals","to_partial_fraction"];
+val {scr = Script t,...} =
-atomty_thy @{theory} t;
+get_met ["simplification",
-\end{verbatim}
+"of_rationals",
+"to_partial_fraction"];
+atomty_thy @ { theory } t ;
+\end{verbatim}
 \item We check if the \textbf{semantics of the program} by stepwise evaluation
 of the program. Evaluation is done by the Lucas-Interpreter, which works
 using the knowledge in theory Isac; so we have to re-build Isac. And the
 test are performed simplest in a file which is loaded with Isac.
-See \ttfamily tests/../partial_fractions.sml \normalfont.
+See \ttfamily tests/../partial\_fractions.sml \normalfont.
 \end{enumerate}
 *}
 subsection {* Transfer to Inverse\_Z\_Transform.thy *}
 text {*
+Unfortunately it was not possible to complete this task. Because we ran out of time\ldots
 *}
 end

changeset 42381	8b94d811cb41
parent 42377	da3a55182442
child 42388	65da7356f5cd