1.1 --- a/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy Mon Feb 20 18:31:00 2012 +0100
1.2 +++ b/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy Wed Mar 07 15:29:02 2012 +0100
1.3 @@ -5,20 +5,18 @@
1.4 10 20 30 40 50 60 70 80
1.5 *)
1.6
1.7 -header{* Build_Inverse_Z_Transform *}
1.8 -
1.9 theory Build_Inverse_Z_Transform imports Isac
1.10
1.11 begin
1.12
1.13 text{* We stepwise build \ttfamily Inverse\_Z\_Transform.thy \normalfont as an
1.14 - exercise. Because subsection~\ref{sec:stepcheck} requires
1.15 + exercise. Because Subsection~\ref{sec:stepcheck} requires
1.16 \ttfamily Inverse\_Z\_Transform.thy \normalfont as a subtheory of \ttfamily
1.17 Isac.thy\normalfont, the setup has been changed from \ttfamily theory
1.18 Inverse\_Z\_Transform imports Isac \normalfont to the above one.
1.19 \par \noindent
1.20 \begin{center}
1.21 - \textbf{ATTENTION WITH NAMES OF IDENTIFIERS WHEN GOING INTO INTERNALS}
1.22 + \textbf{Attention with the names of identifiers when going into internals!}
1.23 \end{center}
1.24 Here in this theory there are the internal names twice, for instance we have
1.25 \ttfamily (Thm.derivation\_name @{thm rule1} =
1.26 @@ -346,8 +344,11 @@
1.27
1.28 subsubsection {*Get Solutions out of a List*}
1.29 text {*\noindent In {\sisac}'s TP-based programming language:
1.30 - \ttfamily let\$ \$s\_1 = NTH 1\$ solutions; \$s\_2 = NTH 2...\$ \normalfont
1.31 - can be useful.*}
1.32 +\begin{verbatim}
1.33 + let $ $ s_1 = NTH 1 $ solutions; $ s_2 = NTH 2... $
1.34 +\end{verbatim}
1.35 + can be useful.
1.36 + *}
1.37
1.38 ML {*
1.39 val Const ("List.list.Cons", _) $ s_1 $ (Const ("List.list.Cons", _)
1.40 @@ -360,10 +361,11 @@
1.41 requires to get the denominators of the partial fractions out of the
1.42 Solutions as:
1.43 \begin{itemize}
1.44 - \item $ \text{Denominator} _{1} = z - \text{Zeropoint}_{1}$
1.45 - \item $ \text{Denominator} _{2} = z - \text{Zeropoint}_{2}$
1.46 - \item \ldots
1.47 - \end{itemize}*}
1.48 + \item $Denominator_{1}=z-Zeropoint_{1}$
1.49 + \item $Denominator_{2}=z-Zeropoint_{2}$
1.50 + \item \ldots
1.51 + \end{itemize}
1.52 +*}
1.53
1.54 ML {*
1.55 val xx = HOLogic.dest_eq s_1;
1.56 @@ -434,7 +436,7 @@
1.57 by the Lucas-Interpreter. Therefor we moved the function to the
1.58 corresponding \ttfamily Equation.thy \normalfont in our case
1.59 \ttfamily PartialFractions.thy \normalfont. The necessary steps
1.60 - are quit the same as we have done with \ttfamliy get\_denominator
1.61 + are quit the same as we have done with \ttfamily get\_denominator
1.62 \normalfont before.*}
1.63 ML {*
1.64 (*("factors_from_solution",
1.65 @@ -454,88 +456,101 @@
1.66 *}
1.67
1.68 text {*\noindent The tracing output of the calc tree after applying this
1.69 - function was \ttfamily 24 / factors\_from\_solution
1.70 - [z = 1/ 2, z = -1 / 4])] \normalfont and the next step \ttfamily
1.71 - val nxt = ("Empty\_Tac", ...): tac'\_)\normalfont. These observations
1.72 - indicate, that the Lucas-Interpreter (LIP) does not know how to
1.73 - evaluate\\ \ttfamily factors\_from\_solution, \normalfont so we knew
1.74 - that there is something wrong or missing.*}
1.75 + function was:
1.76 +\begin{verbatim}
1.77 + 24 / factors_from_solution [z = 1/ 2, z = -1 / 4])]
1.78 +\end{verbatim}
1.79 + and the next step:
1.80 +\begin{verbatim}
1.81 + val nxt = ("Empty_Tac", ...): tac'_)
1.82 +\end{verbatim}
1.83 + These observations indicate, that the Lucas-Interpreter (LIP)
1.84 + does not know how to evaluate \ttfamily factors\_from\_solution
1.85 + \normalfont, so we knew that there is something wrong or missing.
1.86 + *}
1.87
1.88 -text{*\noindent First we isolate the difficulty in the program as follows:\\
1.89 - \ttfamily \par \noindent
1.90 - "(L\_L::bool list) = (SubProblem (PolyEq',"\^\\
1.91 - "[abcFormula,degree\_2,polynomial,univariate,equation],[no\_met])"\^\\
1.92 - "[BOOL equ, REAL zzz]);"\^\\
1.93 - "(facs::real) = factors\_from\_solution L\_L;"\^\\
1.94 - "(foo::real) = Take facs"\^\\
1.95 +text{*\noindent First we isolate the difficulty in the program as follows:
1.96 +\begin{verbatim}
1.97 + " (L_L::bool list) = (SubProblem (PolyEq', " ^
1.98 + " [abcFormula, degree_2, polynomial, " ^
1.99 + " univariate,equation], " ^
1.100 + " [no_met]) " ^
1.101 + " [BOOL equ, REAL zzz]); " ^
1.102 + " (facs::real) = factors_from_solution L_L; " ^
1.103 + " (foo::real) = Take facs " ^
1.104 +\end{verbatim}
1.105 +
1.106 + \par \noindent And see the tracing output:
1.107 +
1.108 +\begin{verbatim}
1.109 + [(([], Frm), Problem (Isac, [inverse,
1.110 + Z_Transform,
1.111 + SignalProcessing])),
1.112 + (([1], Frm), X z = 3 / (z - 1 / 4 + -1 / 8 * (1 / z))),
1.113 + (([1], Res), ?X' z = 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))),
1.114 + (([2], Res), ?X' z = 24 / (-1 + -2 * z + 8 * z ^^^ 2)),
1.115 + (([3], Pbl), solve (-1 + -2 * z + 8 * z ^^^ 2 = 0, z)),
1.116 + (([3,1], Frm), -1 + -2 * z + 8 * z ^^^ 2 = 0),
1.117 + (([3,1], Res), z = (- -2 + sqrt (-2 ^^^ 2 - 4 * 8 * -1)) / (2 * 8)|
1.118 + z = (- -2 - sqrt (-2 ^^^ 2 - 4 * 8 * -1)) / (2 * 8)),
1.119 + (([3,2], Res), z = 1 / 2 | z = -1 / 4),
1.120 + (([3,3], Res), [ z = 1 / 2, z = -1 / 4]),
1.121 + (([3,4], Res), [ z = 1 / 2, z = -1 / 4]),
1.122 + (([3], Res), [ z = 1 / 2, z = -1 / 4]),
1.123 + (([4], Frm), factors_from_solution [z = 1 / 2, z = -1 / 4])]
1.124 +\end{verbatim}
1.125 +
1.126 + \par \noindent In particular that:
1.127 +
1.128 +\begin{verbatim}
1.129 + (([3], Pbl), solve (-1 + -2 * z + 8 * z ^^^ 2 = 0, z)),
1.130 +\end{verbatim}
1.131 + \par \noindent Shows the equation which has been created in
1.132 + the program by:
1.133 +\begin{verbatim}
1.134 + "(denom::real) = get_denominator funterm; " ^
1.135 + (* get_denominator *)
1.136 + "(equ::bool) = (denom = (0::real)); " ^
1.137 +\end{verbatim}
1.138
1.139 - \normalfont \par \noindent And see the tracing output:\\
1.140 - \ttfamily \par \noindent \lbrack\\
1.141 - ((\lbrack\rbrack, Frm), Problem
1.142 - (Isac, \lbrack inverse, Z\_Transform, SignalProcessing\rbrack)),\\
1.143 - ((\lbrack 1\rbrack, Frm), X z = 3 / (z - 1 / 4 + -1 / 8 * (1 / z))),\\
1.144 - ((\lbrack 1\rbrack, Res),
1.145 - ?X' z = 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))),\\
1.146 - ((\lbrack 2\rbrack, Res),
1.147 - ?X' z = 24 / (-1 + -2 * z + 8 * z \^\^\^ ~2)),\\
1.148 - ((\lbrack 3\rbrack, Pbl),
1.149 - solve (-1 + -2 * z + 8 * z \^\^\^ ~2 = 0, z)),\\
1.150 - ((\lbrack 3,1\rbrack, Frm), -1 + -2 * z + 8 * z \^\^\^ ~2 = 0),\\
1.151 - ((\lbrack 3,1\rbrack, Res),
1.152 - z = (- -2 + sqrt (-2 \^\^\^ ~2 - 4 * 8 * -1)) / (2 * 8)|\\
1.153 - z = (- -2 - sqrt (-2 \^\^\^ ~2 - 4 * 8 * -1)) / (2 * 8)),\\
1.154 - ((\lbrack 3,2\rbrack, Res), z = 1 / 2 | z = -1 / 4),\\
1.155 - ((\lbrack 3,3\rbrack, Res), \lbrack z = 1 / 2, z = -1 / 4\rbrack),\\
1.156 - ((\lbrack 3,4\rbrack, Res), \lbrack z = 1 / 2, z = -1 / 4\rbrack),\\
1.157 - ((\lbrack 3\rbrack, Res), \lbrack z = 1 / 2, z = -1 / 4\rbrack),\\
1.158 - ((\lbrack 4\rbrack, Frm),
1.159 - factors\_from\_solution \lbrackz = 1 / 2, z = -1 / 4])\\
1.160 - \rbrack\\
1.161 -
1.162 - \normalfont \noindent In particular that:\\
1.163 - \ttfamily \par \noindent ((\lbrack 3\rbrack, Pbl),
1.164 - solve (-1 + -2 * z + 8 * z \^\^\^ ~2 = 0, z)),\\
1.165 - \normalfont \par \noindent Shows the equation which has been created in
1.166 - the program by: \ttfamily \\
1.167 -
1.168 - \noindent "(denom::real) = get\_denominator funterm;"\^
1.169 - ~(*get\_denominator*)\\
1.170 - "(equ::bool) = (denom = (0::real));"\^\\
1.171 -
1.172 - \noindent get\_denominator \normalfont has been evaluated successfully,
1.173 + \noindent \ttfamily get\_denominator \normalfont has been evaluated successfully,
1.174 but not\\ \ttfamily factors\_from\_solution.\normalfont
1.175 So we stepwise compare with an analogous case, \ttfamily get\_denominator
1.176 \normalfont successfully done above: We know that LIP evaluates
1.177 expressions in the program by use of the \emph{srls}, so we try to get
1.178 the original \emph{srls}.\\
1.179
1.180 - \noindent \ttfamily val \lbrace srls,\ldots\rbrace\ttfamily
1.181 - = get\_met \lbrack "SignalProcessing",
1.182 - "Z\_Transform","inverse"\rbrack;\\
1.183 +\begin{verbatim}
1.184 + val {srls,...} = get_met ["SignalProcessing",
1.185 + "Z_Transform",
1.186 + "inverse"];
1.187 +\end{verbatim}
1.188
1.189 - \par \noindent \normalfont Create 2 good example terms\\
1.190 - \ttfamily \par \noindent val SOME t1 =\\
1.191 - parseNEW ctxt "get\_denominator ((111::real) / 222)";
1.192 - \par \noindent val SOME t2 =\\
1.193 - parseNEW ctxt "factors\_from\_solution \lbrack(z::real)
1.194 - = 1/2, z = -1/4\rbrack";\\
1.195 + \par \noindent Create 2 good example terms:
1.196
1.197 - \par \noindent \normalfont Rewrite the terms using srls:\\
1.198 +\begin{verbatim}
1.199 +val SOME t1 =
1.200 + parseNEW ctxt "get_denominator ((111::real) / 222)";
1.201 +val SOME t2 =
1.202 + parseNEW ctxt "factors_from_solution [(z::real)=1/2, z=-1/4]";
1.203 +\end{verbatim}
1.204 +
1.205 + \par \noindent Rewrite the terms using srls:\\
1.206 \ttfamily \par \noindent rewrite\_set\_ thy true srls t1;\\
1.207 rewrite\_set\_ thy true srls t2;\\
1.208 \par \noindent \normalfont Now we see a difference: \texttt{t1} gives
1.209 \texttt{SOME} but \texttt{t2} gives \texttt{NONE}. We look at the
1.210 - \emph{srls}:\\
1.211 -
1.212 - \par \noindent \ttfamily val srls = Rls \lbrace id =
1.213 - "srls\_InverseZTransform", rules =\\
1.214 - \lbrack Calc("Rational.get\_numerator",\\
1.215 - eval\_get\_numerator "Rational.get\_numerator"),\\
1.216 - Calc("Partial\_Fractions.factors\_from\_solution",\\
1.217 - eval\_factors\_from\_solution
1.218 - "Partial\_Fractions.factors\_from\_solution")\rbrack\rbrace\\
1.219 -
1.220 - \par \noindent \normalfont Here everthing is perfect. So the error can
1.221 + \emph{srls}:
1.222 +\begin{verbatim}
1.223 + val srls =
1.224 + Rls{id = "srls_InverseZTransform",
1.225 + rules = [Calc("Rational.get_numerator",
1.226 + eval_get_numerator "Rational.get_numerator"),
1.227 + Calc("Partial_Fractions.factors_from_solution",
1.228 + eval_factors_from_solution
1.229 + "Partial_Fractions.factors_from_solution")]}
1.230 +\end{verbatim}
1.231 + \par \noindent Here everthing is perfect. So the error can
1.232 only be in the SML code of \ttfamily eval\_factors\_from\_solution.
1.233 \normalfont We try to check the code with an existing test; since the
1.234 \emph{code} is in
1.235 @@ -555,12 +570,13 @@
1.236 \begin{center}use \ttfamily "Knowledge/partial\_fractions.sml"
1.237 \normalfont \end{center}
1.238 and \ttfamily Partial\_Fractions.thy \normalfont is part is part of
1.239 - {\sisac} by evaluating\\
1.240 + {\sisac} by evaluating
1.241
1.242 - \par \noindent \ttfamily val thy = @\lbrace theory~Isac \rbrace;
1.243 - \normalfont \\
1.244 +\begin{verbatim}
1.245 + val thy = @{theory Isac};
1.246 +\end{verbatim}
1.247
1.248 - \par \noindent \normalfont After rebuilding {\sisac} again it worked.
1.249 + After rebuilding {\sisac} again it worked.
1.250 *}
1.251
1.252 subsubsection {*Build Expression*}
1.253 @@ -698,7 +714,7 @@
1.254 scr = EmptyScr});
1.255 *}
1.256
1.257 -text{*\noindent We apply the ruleset\lodts*}
1.258 +text{*\noindent We apply the ruleset\ldots*}
1.259
1.260 ML {*
1.261 val SOME (ttttt,_) =
1.262 @@ -719,7 +735,7 @@
1.263 Calculation in Section~\ref{sec:calc:ztrans} Subproblem~1.*}
1.264
1.265 text{*\noindent To get the first coefficient we substitute $z$ with the first
1.266 - zero-point we determined in section~\ref{sec:solveq}.*}
1.267 + zero-point we determined in Section~\ref{sec:solveq}.*}
1.268
1.269 ML {*
1.270 val SOME (eq4_1,_) =
1.271 @@ -799,7 +815,7 @@
1.272 ML {*thy*}
1.273
1.274 text{*\noindent To get the second coefficient we substitute $z$ with the second
1.275 - zero-point we determined in section~\ref{sec:solveq}.*}
1.276 + zero-point we determined in Section~\ref{sec:solveq}.*}
1.277
1.278 ML {*
1.279 val SOME (eq4b_1,_) =
1.280 @@ -884,7 +900,7 @@
1.281
1.282 text{*\noindent For the suddenly created node we have to define the input
1.283 and output parameters. We already prepared their definition in
1.284 - section~\ref{sec:deffdes}.*}
1.285 + Section~\ref{sec:deffdes}.*}
1.286
1.287 ML {*
1.288 store_pbt
1.289 @@ -990,7 +1006,7 @@
1.290 subsection {*Stepwise Extend the Program*}
1.291 ML {*
1.292 val str =
1.293 - "Script InverseZTransform (Xeq::bool) =" ^
1.294 + "Script InverseZTransform (Xeq::bool) = "^
1.295 " Xeq";
1.296 *}
1.297
1.298 @@ -999,16 +1015,16 @@
1.299
1.300 ML {*
1.301 val str =
1.302 - "Script InverseZTransform (Xeq::bool) =" ^
1.303 + "Script InverseZTransform (Xeq::bool) = "^
1.304 (*
1.305 * 1/z) instead of z ^^^ -1
1.306 *)
1.307 - " (let X = Take Xeq;" ^
1.308 - " X' = Rewrite ruleZY False X;" ^
1.309 + " (let X = Take Xeq; "^
1.310 + " X' = Rewrite ruleZY False X; "^
1.311 (*
1.312 * z * denominator
1.313 *)
1.314 - " X' = (Rewrite_Set norm_Rational False) X'" ^
1.315 + " X' = (Rewrite_Set norm_Rational False) X' "^
1.316 (*
1.317 * simplify
1.318 *)
1.319 @@ -1016,23 +1032,23 @@
1.320 (*
1.321 * NONE
1.322 *)
1.323 - "Script InverseZTransform (Xeq::bool) =" ^
1.324 + "Script InverseZTransform (Xeq::bool) = "^
1.325 (*
1.326 * (1/z) instead of z ^^^ -1
1.327 *)
1.328 - " (let X = Take Xeq;" ^
1.329 - " X' = Rewrite ruleZY False X;" ^
1.330 + " (let X = Take Xeq; "^
1.331 + " X' = Rewrite ruleZY False X; "^
1.332 (*
1.333 * z * denominator
1.334 *)
1.335 - " X' = (Rewrite_Set norm_Rational False) X';" ^
1.336 + " X' = (Rewrite_Set norm_Rational False) X'; "^
1.337 (*
1.338 * simplify
1.339 *)
1.340 - " X' = (SubProblem (Isac',[pqFormula,degree_2," ^
1.341 - " polynomial,univariate,equation]," ^
1.342 - " [no_met]) " ^
1.343 - " [BOOL e_e, REAL v_v])" ^
1.344 + " X' = (SubProblem (Isac',[pqFormula,degree_2, "^
1.345 + " polynomial,univariate,equation], "^
1.346 + " [no_met]) "^
1.347 + " [BOOL e_e, REAL v_v]) "^
1.348 " in X)";
1.349 *}
1.350
1.351 @@ -1042,11 +1058,11 @@
1.352
1.353 ML {*
1.354 val str =
1.355 - "Script InverseZTransform (Xeq::bool) =" ^
1.356 - " (let X = Take Xeq;" ^
1.357 - " X' = Rewrite ruleZY False X;" ^
1.358 - " X' = (Rewrite_Set norm_Rational False) X';" ^
1.359 - " funterm = rhs X'" ^
1.360 + "Script InverseZTransform (Xeq::bool) = "^
1.361 + " (let X = Take Xeq; "^
1.362 + " X' = Rewrite ruleZY False X; "^
1.363 + " X' = (Rewrite_Set norm_Rational False) X'; "^
1.364 + " funterm = rhs X' "^
1.365 (*
1.366 * drop X'= for equation solving
1.367 *)
1.368 @@ -1059,23 +1075,23 @@
1.369
1.370 ML {*
1.371 val str =
1.372 - "Script InverseZTransform (X_eq::bool) =" ^
1.373 - " (let X = Take X_eq;" ^
1.374 - " X' = Rewrite ruleZY False X;" ^
1.375 - " X' = (Rewrite_Set norm_Rational False) X';" ^
1.376 - " (X'_z::real) = lhs X';" ^
1.377 - " (z::real) = argument_in X'_z;" ^
1.378 - " (funterm::real) = rhs X';" ^
1.379 - " (denom::real) = get_denominator funterm;" ^
1.380 + "Script InverseZTransform (X_eq::bool) = "^
1.381 + " (let X = Take X_eq; "^
1.382 + " X' = Rewrite ruleZY False X; "^
1.383 + " X' = (Rewrite_Set norm_Rational False) X'; "^
1.384 + " (X'_z::real) = lhs X'; "^
1.385 + " (z::real) = argument_in X'_z; "^
1.386 + " (funterm::real) = rhs X'; "^
1.387 + " (denom::real) = get_denominator funterm; "^
1.388 (*
1.389 * get_denominator
1.390 *)
1.391 - " (equ::bool) = (denom = (0::real));" ^
1.392 - " (L_L::bool list) = " ^
1.393 - " (SubProblem (Test', " ^
1.394 - " [linear,univariate,equation,test], " ^
1.395 - " [Test,solve_linear]) " ^
1.396 - " [BOOL equ, REAL z]) " ^
1.397 + " (equ::bool) = (denom = (0::real)); "^
1.398 + " (L_L::bool list) = "^
1.399 + " (SubProblem (Test', "^
1.400 + " [linear,univariate,equation,test], "^
1.401 + " [Test,solve_linear]) "^
1.402 + " [BOOL equ, REAL z]) "^
1.403 " in X)";
1.404
1.405 parse thy str;
1.406 @@ -1087,37 +1103,37 @@
1.407 The evaluation of the functions is done by rewriting using this ruleset.*}
1.408
1.409 ML {*
1.410 - val srls = Rls {id="srls_InverseZTransform",
1.411 - preconds = [],
1.412 - rew_ord = ("termlessI",termlessI),
1.413 - erls = append_rls "erls_in_srls_InverseZTransform" e_rls
1.414 - [(*for asm in NTH_CONS ...*)
1.415 - Calc ("Orderings.ord_class.less",eval_equ "#less_"),
1.416 - (*2nd NTH_CONS pushes n+-1 into asms*)
1.417 - Calc("Groups.plus_class.plus", eval_binop "#add_")
1.418 - ],
1.419 - srls = Erls, calc = [],
1.420 - rules = [
1.421 - Thm ("NTH_CONS",num_str @{thm NTH_CONS}),
1.422 - Calc("Groups.plus_class.plus",
1.423 - eval_binop "#add_"),
1.424 - Thm ("NTH_NIL",num_str @{thm NTH_NIL}),
1.425 - Calc("Tools.lhs", eval_lhs"eval_lhs_"),
1.426 - Calc("Tools.rhs", eval_rhs"eval_rhs_"),
1.427 - Calc("Atools.argument'_in",
1.428 - eval_argument_in "Atools.argument'_in"),
1.429 - Calc("Rational.get_denominator",
1.430 - eval_get_denominator "#get_denominator"),
1.431 - Calc("Rational.get_numerator",
1.432 - eval_get_numerator "#get_numerator"),
1.433 - Calc("Partial_Fractions.factors_from_solution",
1.434 - eval_factors_from_solution
1.435 - "#factors_from_solution"),
1.436 - Calc("Partial_Fractions.drop_questionmarks",
1.437 - eval_drop_questionmarks "#drop_?")
1.438 - ],
1.439 - scr = EmptyScr
1.440 - };
1.441 + val srls =
1.442 + Rls {id="srls_InverseZTransform",
1.443 + preconds = [],
1.444 + rew_ord = ("termlessI",termlessI),
1.445 + erls = append_rls "erls_in_srls_InverseZTransform" e_rls
1.446 + [(*for asm in NTH_CONS ...*)
1.447 + Calc ("Orderings.ord_class.less",eval_equ "#less_"),
1.448 + (*2nd NTH_CONS pushes n+-1 into asms*)
1.449 + Calc("Groups.plus_class.plus", eval_binop "#add_")
1.450 + ],
1.451 + srls = Erls, calc = [],
1.452 + rules = [
1.453 + Thm ("NTH_CONS",num_str @{thm NTH_CONS}),
1.454 + Calc("Groups.plus_class.plus",
1.455 + eval_binop "#add_"),
1.456 + Thm ("NTH_NIL",num_str @{thm NTH_NIL}),
1.457 + Calc("Tools.lhs", eval_lhs"eval_lhs_"),
1.458 + Calc("Tools.rhs", eval_rhs"eval_rhs_"),
1.459 + Calc("Atools.argument'_in",
1.460 + eval_argument_in "Atools.argument'_in"),
1.461 + Calc("Rational.get_denominator",
1.462 + eval_get_denominator "#get_denominator"),
1.463 + Calc("Rational.get_numerator",
1.464 + eval_get_numerator "#get_numerator"),
1.465 + Calc("Partial_Fractions.factors_from_solution",
1.466 + eval_factors_from_solution
1.467 + "#factors_from_solution"),
1.468 + Calc("Partial_Fractions.drop_questionmarks",
1.469 + eval_drop_questionmarks "#drop_?")
1.470 + ],
1.471 + scr = EmptyScr};
1.472 *}
1.473
1.474
1.475 @@ -1125,7 +1141,7 @@
1.476
1.477 text{*\noindent After we also tested how to write scripts and run them,
1.478 we start creating the final version of our script and store it into
1.479 - the method for which we created a node in section~\ref{sec:cparentnode}
1.480 + the method for which we created a node in Section~\ref{sec:cparentnode}
1.481 Note that we also did this stepwise, but we didn't kept every
1.482 subversion.*}
1.483
1.484 @@ -1303,32 +1319,34 @@
1.485 text {*\noindent Instead of \ttfamily nxt = Subproblem \normalfont above we had
1.486 \ttfamily Empty\_Tac; \normalfont the search for the reason considered
1.487 the following points:\begin{itemize}
1.488 - \item What shows \ttfamily show\_pt pt;\normalfont\ldots?\\
1.489 - \ttfamily ((\lbrack 2\rbrack, Res), ?X' z = 24 /
1.490 - (-1 + -2 * z + 8 * z \^\^\^ ~2))\rbrack\normalfont\\
1.491 + \item What shows \ttfamily show\_pt pt;\normalfont\ldots?
1.492 +\begin{verbatim}(([2], Res), ?X' z = 24 / (-1 + -2 * z + 8 * z ^^^ 2))]\end{verbatim}
1.493 The calculation is ok but no \ttfamily next \normalfont step found:
1.494 Should be\\ \ttfamily nxt = Subproblem\normalfont!
1.495 \item What shows \ttfamily trace\_script := true; \normalfont we read
1.496 - bottom up\ldots\\
1.497 - \ttfamily @@@next leaf 'SubProbfrom\\
1.498 - (PolyEq',\\
1.499 - \lbrack abcFormula, degree\_2, polynomial, univariate,
1.500 - equation\rbrack,\\
1.501 - no\_meth)\\
1.502 - \lbrack BOOL equ, REAL z\rbrack' ---> STac 'SubProblem\\
1.503 - (PolyEq',\\
1.504 - [abcFormula, degree\_2, polynomial, univariate, equation],\\
1.505 - no\_meth)\\
1.506 - \lbrack BOOL (-1 + -2 * z + 8 * z \^\^\^ ~2 = 0),
1.507 - REAL z\rbrack'\normalfont\\
1.508 + bottom up\ldots
1.509 + \begin{verbatim}
1.510 + @@@next leaf 'SubProblem
1.511 + (PolyEq',[abcFormula, degree_2, polynomial,
1.512 + univariate, equation], no_meth)
1.513 + [BOOL equ, REAL z]'
1.514 + ---> STac 'SubProblem (PolyEq',
1.515 + [abcFormula, degree_2, polynomial,
1.516 + univariate, equation], no_meth)
1.517 + [BOOL (-1 + -2 * z + 8 * z \^\^\^ ~2 = 0), REAL z]'
1.518 + \end{verbatim}
1.519 We see the SubProblem with correct arguments from searching next
1.520 step (program text !!!--->!!! STac (script tactic) with arguments
1.521 evaluated.)
1.522 \item Do we have the right Script \ldots difference in the
1.523 - arguments in the arguments\ldots\\
1.524 - \ttfamily val Script s =\\
1.525 - (#scr o get\_met) ["SignalProcessing","Z\_Transform","inverse"];\\
1.526 - writeln (term2str s);\normalfont\\
1.527 + arguments in the arguments\ldots
1.528 + \begin{verbatim}
1.529 + val Script s =
1.530 + (#scr o get_met) ["SignalProcessing",
1.531 + "Z_Transform",
1.532 + "inverse"];
1.533 + writeln (term2str s);
1.534 + \end{verbatim}
1.535 \ldots shows the right script. Difference in the arguments.
1.536 \item Test --- Why helpless here ? --- shows: \ttfamily replace
1.537 no\_meth by [no\_meth] \normalfont in Script
1.538 @@ -1344,7 +1362,7 @@
1.539 we had \ttfamily Empty\_Tac; \normalfont the search for the reason
1.540 considered the following points:\begin{itemize}
1.541 \item Difference in the arguments
1.542 - \item Comparison with subsection~ref{sec:solveq}: There solving this
1.543 + \item Comparison with Subsection~\ref{sec:solveq}: There solving this
1.544 equation works, so there must be some difference in the arguments
1.545 of the Subproblem: RIGHT: we had \ttfamily [no\_meth] \normalfont
1.546 instead of \ttfamily [no\_met] \normalfont ;-)
1.547 @@ -1367,14 +1385,16 @@
1.548 \item Was there an error message? NO -- ok
1.549 \item Has \ttfamily nxt = Add\_Find \normalfont been inserted in pt:\\
1.550 \ttfamily get\_obj g\_pbl pt (fst p);\normalfont? YES -- ok
1.551 - \item What is the returned formula:
1.552 - \ttfamily print\_depth 999; f; print\_depth 999;\\
1.553 - \lbrace Find = \lbrack Correct "solutions z\_i"\rbrack,
1.554 - With = \lbrack\rbrack,\\
1.555 - Given = \lbrack Correct "equality (-1 + -2 * z + 8 * z ^^^ 2 = 0)",
1.556 - Correct "solveFor z"\rbrack,\\
1.557 - Where = \lbrack \ldots \rbrack,
1.558 - Relate = \lbrack\rbrack\rbrace $ \normalfont\\
1.559 + \item What is the returned formula:
1.560 +\begin{verbatim}
1.561 +print_depth 999; f; print_depth 999;
1.562 +{ Find = [ Correct "solutions z_i"],
1.563 + With = [],
1.564 + Given = [Correct "equality (-1 + -2*z + 8*z ^^^ 2 = 0)",
1.565 + Correct "solveFor z"],
1.566 + Where = [...],
1.567 + Relate = [] }
1.568 +\end{verbatim}
1.569 \normalfont The only False is the reason: the Where (the precondition) is
1.570 False for good reasons: The precondition seems to check for linear
1.571 equations, not for the one we want to solve! Removed this error by
1.572 @@ -1508,35 +1528,39 @@
1.573 \normalfont and then modularise. In this case TODO problems?!?
1.574
1.575 We chose another way and go bottom up: first we build the sub-problem in
1.576 - \ttfamily Partial\_Fractions.thy \normalfont with the term
1.577 + \ttfamily Partial\_Fractions.thy \normalfont with the term:
1.578
1.579 - $$\frac{3}{x\cdot(z - \fract{1}{4} + \frac{-1}{8}\cdot\fract{1}{z})}$$
1.580 + $$\frac{3}{x\cdot(z - \frac{1}{4} + \frac{-1}{8}\cdot\frac{1}{z})}$$
1.581
1.582 - (how this still can be improved see \ttfamily Partial\_Fractions.thy \normalfont),
1.583 + \noindent (how this still can be improved see \ttfamily Partial\_Fractions.thy\normalfont),
1.584 and re-use all stuff prepared in \ttfamily Build\_Inverse\_Z\_Transform.thy:
1.585 - The knowledge will be transferred to \ttfamily src/../Partial\_Fractions.thy
1.586 - \normalfont and the respective tests to \ttfamily test/../sartial\_fractions.sml.
1.587 + \normalfont The knowledge will be transferred to \ttfamily src/../Partial\_Fractions.thy
1.588 + \normalfont and the respective tests to:
1.589 + \begin{center}\ttfamily test/../sartial\_fractions.sml\normalfont\end{center}
1.590 *}
1.591
1.592 subsection {* Transfer to Partial\_Fractions.thy *}
1.593 text {*
1.594 - First we transfer both, knowledge and tests into \ttfamily src/../Partial\_Fractions.thy
1.595 - \normalfont in order to immediately have the test results.
1.596 + First we transfer both, knowledge and tests into:
1.597 + \begin{center}\ttfamily src/../Partial\_Fractions.thy\normalfont\end{center}
1.598 + in order to immediately have the test results.
1.599
1.600 - We copy \ttfamily factors_from_solution, drop_questionmarks,
1.601 - ansatz_2nd_order \normalfont and rule-sets --- no problem.
1.602 - Also \ttfamily store_pbt .. "pbl_simp_rat_partfrac"
1.603 + We copy \ttfamily factors\_from\_solution, drop\_questionmarks,\\
1.604 + ansatz\_2nd\_order \normalfont and rule-sets --- no problem.
1.605 +
1.606 + Also \ttfamily store\_pbt ..\\ "pbl\_simp\_rat\_partfrac"
1.607 \normalfont is easy.
1.608
1.609 - But then we copy from (1) \ttfamily Build\_Inverse\_Z\_Transform.thy
1.610 - store_met .. "met_SP_Ztrans_inv" to (2) \ttfamily Partial\_Fractions.thy
1.611 - store_met .. "met_SP_Ztrans_inv"
1.612 - \normalfont and cut out the respective part from the program. First we ensure that
1.613 + But then we copy from:\\
1.614 + (1) \ttfamily Build\_Inverse\_Z\_Transform.thy store\_met\ldots "met\_SP\_Ztrans\_inv"
1.615 + \normalfont\\ to\\
1.616 + (2) \ttfamily Partial\_Fractions.thy store\_met\ldots "met\_SP\_Ztrans\_inv"
1.617 + \normalfont\\ and cut out the respective part from the program. First we ensure that
1.618 the string is correct. When we insert the string into (2)
1.619 - \ttfamily store_met .. "met_partial_fraction" \normalfont --- and get an error.
1.620 + \ttfamily store\_met .. "met\_partial\_fraction" \normalfont --- and get an error.
1.621 *}
1.622
1.623 -subsubsection {* 'Programming' in \sisac}'s TP-based Language *}
1.624 +subsubsection {* 'Programming' in ISAC's TP-based Language *}
1.625 text {*
1.626 At the present state writing programs in {\sisac} is particularly cumbersome.
1.627 So we give hints how to cope with the many obstacles. Below we describe the
1.628 @@ -1546,39 +1570,44 @@
1.629 \item We check if the \textbf{string} containing the program is correct.
1.630 \item We check if the \textbf{types in the program} are correct.
1.631 For this purpose we start start with the first and last lines
1.632 - \begin{verbatim}
1.633 - "PartFracScript (f_f::real) (v_v::real) = " ^
1.634 - " (let X = Take f_f; " ^
1.635 - " pbz = ((Substitute []) X) " ^
1.636 - " in pbz)"
1.637 - \end{verbatim}
1.638 + \begin{verbatim}
1.639 + "PartFracScript (f_f::real) (v_v::real) = " ^
1.640 + " (let X = Take f_f; " ^
1.641 + " pbz = ((Substitute []) X) " ^
1.642 + " in pbz)"
1.643 + \end{verbatim}
1.644 The last but one line helps not to bother with ';'.
1.645 \item Then we add line by line. Already the first line causes the error.
1.646 So we investigate it by
1.647 - \begin{verbatim}
1.648 - val ctxt = ProofContext.init_global @{theory};
1.649 - val SOME t = parseNEW ctxt "(num_orig::real) = get_numerator (rhs f_f)";
1.650 - \end{verbatim}
1.651 + \begin{verbatim}
1.652 + val ctxt = ProofContext.init_global @ { theory } ;
1.653 + val SOME t =
1.654 + parseNEW ctxt "(num_orig::real) =
1.655 + get_numerator(rhs f_f)";
1.656 + \end{verbatim}
1.657 and see a type clash: \ttfamily rhs \normalfont from (1) requires type
1.658 - \ttfamily bool \normalfont while (2) wants to have \ttfamily (f_f::real).
1.659 + \ttfamily bool \normalfont while (2) wants to have \ttfamily (f\_f::real).
1.660 \normalfont Of course, we don't need \ttfamily rhs \normalfont anymore.
1.661 \item Type-checking can be very tedious. One might even inspect the
1.662 - parse-tree of the program with \sisac's specific debug tools:
1.663 - \begin{verbatim}
1.664 - val {scr = Script t,...} = get_met ["simplification","of_rationals","to_partial_fraction"];
1.665 - atomty_thy @{theory} t;
1.666 - \end{verbatim}
1.667 + parse-tree of the program with {\sisac}'s specific debug tools:
1.668 + \begin{verbatim}
1.669 + val {scr = Script t,...} =
1.670 + get_met ["simplification",
1.671 + "of_rationals",
1.672 + "to_partial_fraction"];
1.673 + atomty_thy @ { theory } t ;
1.674 + \end{verbatim}
1.675 \item We check if the \textbf{semantics of the program} by stepwise evaluation
1.676 of the program. Evaluation is done by the Lucas-Interpreter, which works
1.677 using the knowledge in theory Isac; so we have to re-build Isac. And the
1.678 test are performed simplest in a file which is loaded with Isac.
1.679 - See \ttfamily tests/../partial_fractions.sml \normalfont.
1.680 + See \ttfamily tests/../partial\_fractions.sml \normalfont.
1.681 \end{enumerate}
1.682 *}
1.683
1.684 subsection {* Transfer to Inverse\_Z\_Transform.thy *}
1.685 text {*
1.686 -
1.687 + Unfortunately it was not possible to complete this task. Because we ran out of time\ldots
1.688 *}
1.689
1.690