1.1 --- a/doc-src/isac/jrocnik/eJMT-paper/jrocnik_eJMT.tex Fri Sep 07 13:34:07 2012 +0200
1.2 +++ b/doc-src/isac/jrocnik/eJMT-paper/jrocnik_eJMT.tex Fri Sep 07 18:12:50 2012 +0200
1.3 @@ -244,7 +244,8 @@
1.4 running example:
1.5 \begin{figure} [htb]
1.6 \begin{center}
1.7 -\includegraphics[width=140mm]{fig/isac-Ztrans-math}
1.8 +\includegraphics[width=140mm]{fig/isac-Ztrans-math-3}
1.9 +%\includegraphics[width=140mm]{fig/isac-Ztrans-math}
1.10 \caption{Step-wise problem solving guided by the TP-based program}
1.11 \label{fig-interactive}
1.12 \end{center}
1.13 @@ -839,71 +840,117 @@
1.14 123l\=123\=123\=123\=123\=123\=123\=123\=123\=(x \=123\=123\=\kill
1.15 \>{\rm 01}\> {\tt Program} InverseZTransform (X\_eq::bool) = \\
1.16 \>{\rm 02}\>\> {\tt LET} \\
1.17 -\>{\rm 03}\>\>\> X = {\tt Take} X\_eq ; \\
1.18 -\>{\rm 04}\>\>\> X' = {\tt Rewrite} ruleZY X ; \\
1.19 -\>{\rm 05}\>\>\> (X'\_z::real) = lhs X' ; \\
1.20 -\>{\rm 06}\>\>\> (zzz::real) = argument\_in X'\_z; \\
1.21 -\>{\rm 07}\>\>\> (funterm::real) = rhs X’; \\
1.22 -\>{\rm 07}\>\>\> (pbz::real) = {\tt SubProblem} \\
1.23 -\>{\rm 08}\>\>\>\>\>\>\>\> ( \> Inverse\_Z\_Transform, \\
1.24 -\>{\rm 08}\>\>\>\>\>\>\>\>\> [partial\_fraction,rational,simplification]\\
1.25 +\>{\rm 03}\>\>\> X\_eq = {\tt Take} X\_eq ; \\
1.26 +\>{\rm 04}\>\>\> X\_eq = {\tt Rewrite} ruleZY X\_eq ; \\
1.27 +\>{\rm 05}\>\>\> (X\_z::real) = lhs X\_eq ; \\ %no inside-out evaluation
1.28 +\>{\rm 06}\>\>\> (z::real) = argument\_in X\_z; \\
1.29 +\>{\rm 07}\>\>\> (part\_frac::real) = {\tt SubProblem} \\
1.30 +\>{\rm 08}\>\>\>\>\>\>\>\> ( \> Isac, \\
1.31 +\>{\rm 08}\>\>\>\>\>\>\>\>\> [partial\_fraction, rational, simplification]\\
1.32 \>{\rm 09}\>\>\>\>\>\>\>\>\> [simplification,of\_rationals,to\_partial\_fraction] ) \\
1.33 -\>{\rm 10}\>\>\>\>\>\>\>\> [ funterm::real, zzz::real ]; \\
1.34 -\>{\rm 12}\>\>\> (pbz\_eq::bool) = {\tt Take} (X'\_z = pbz) ; \\
1.35 +\>{\rm 10}\>\>\>\>\>\>\>\> [ (rhs X\_eq)::real, z::real ]; \\
1.36 +\>{\rm 12}\>\>\> (X'\_eq::bool) = {\tt Take} ((X'::real =$>$ bool) z = ZZ\_1 part\_frac) ; \\
1.37
1.38 -\>{\rm 12}\>\>\> pbz\_eq = {\tt Rewrite} ruleYZ pbz\_eq ; \\
1.39 -\>{\rm 13}\>\>\> pbz\_eq = drop\_questionmarks pbz\_eq ; \\
1.40 -\>{\rm 14}\>\>\> (X\_zeq::bool) = {\tt Take} (X\_z = rhs pbz\_eq) ; \\
1.41 -\>{\rm 15}\>\>\> n\_eq = {\tt Rewrite\_Set} inverse\_z X\_zeq ; \\
1.42 -\>{\rm 15}\>\>\> n\_eq = drop\_questionmarks n\_eq \\
1.43 +\>{\rm 12}\>\>\> X'\_eq = {\tt Rewrite\_Set} ruleYZ X'\_eq ; \\
1.44 +\>{\rm 15}\>\>\> X'\_eq = {\tt Rewrite\_Set} inverse\_z X'\_eq \\
1.45 \>{\rm 16}\>\> {\tt IN } \\
1.46 -\>{\rm 15}\>\>\> n\_eq
1.47 +\>{\rm 15}\>\>\> X'\_eq
1.48 \end{tabbing}}
1.49 -
1.50 -{\small\it\begin{tabbing}
1.51 -123l\=123\=123\=123\=123\=123\=123\=123\=123\=123\=123\=123\=\kill\label{exp-calc}
1.52 -\>{\rm 01}\> $\bullet$\> {\tt Problem } [maximum\_by, calculus] \`- - -\\
1.53 -\>{\rm 02}\>\> $\vdash$\> $A = 2\cdot u\cdot v - u^2$ \`- - -\\
1.54 -\>{\rm 03}\>\> $\bullet$\> {\tt Problem } [make, diffable, function] \`- - -\\
1.55 -\>{\rm 04}\>\> \dots\> $\widetilde{A}(\alpha) = 8\cdot r^2\cdot\sin\alpha\cdot\cos\alpha - 4\cdot r^2\cdot(\sin\alpha)^2$ \`- - -\\
1.56 -\\
1.57 -\\
1.58 -\>{\rm 18}\>\> $\bullet$\> {\tt Problem} [find\_values, tool] \`- - -\\
1.59 -% \`{\tt Apply\_Method} [tool, find\_values]\\
1.60 -\>{\rm 19}\>\> \dots\> [ $u=0.23\cdot r, \:v=0.76\cdot r$ ] \`- - -\\
1.61 -% \`{\tt Check\_Postcond}\\
1.62 -\>{\rm 20}\> \dots\> [ $u=0.23\cdot r, \:v=0.76\cdot r$ ] %TODO calculate !
1.63 -
1.64 -\end{tabbing}}
1.65 +% ORIGINAL FROM Inverse_Z_Transform.thy
1.66 +% "Script InverseZTransform (X_eq::bool) = "^(*([], Frm), Problem (Isac, [Inverse, Z_Transform, SignalProcessing])*)
1.67 +% "(let X = Take X_eq; "^(*([1], Frm), X z = 3 / (z - 1 / 4 + -1 / 8 * (1 / z))*)
1.68 +% " X' = Rewrite ruleZY False X; "^(*([1], Res), ?X' z = 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))*)
1.69 +% " (X'_z::real) = lhs X'; "^(* ?X' z*)
1.70 +% " (zzz::real) = argument_in X'_z; "^(* z *)
1.71 +% " (funterm::real) = rhs X'; "^(* 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))*)
1.72 +%
1.73 +% " (pbz::real) = (SubProblem (Isac', "^(**)
1.74 +% " [partial_fraction,rational,simplification], "^
1.75 +% " [simplification,of_rationals,to_partial_fraction]) "^
1.76 +% " [REAL funterm, REAL zzz]); "^(*([2], Res), 4 / (z - 1 / 2) + -4 / (z - -1 / 4)*)
1.77 +%
1.78 +% " (pbz_eq::bool) = Take (X'_z = pbz); "^(*([3], Frm), ?X' z = 4 / (z - 1 / 2) + -4 / (z - -1 / 4)*)
1.79 +% " pbz_eq = Rewrite ruleYZ False pbz_eq; "^(*([3], Res), ?X' z = 4 * (?z / (z - 1 / 2)) + -4 * (?z / (z - -1 / 4))*)
1.80 +% " pbz_eq = drop_questionmarks pbz_eq; "^(* 4 * (z / (z - 1 / 2)) + -4 * (z / (z - -1 / 4))*)
1.81 +% " (X_zeq::bool) = Take (X_z = rhs pbz_eq); "^(*([4], Frm), X_z = 4 * (z / (z - 1 / 2)) + -4 * (z / (z - -1 / 4))*)
1.82 +% " n_eq = (Rewrite_Set inverse_z False) X_zeq; "^(*([4], Res), X_z = 4 * (1 / 2) ^^^ ?n * ?u [?n] + -4 * (-1 / 4) ^^^ ?n * ?u [?n]*)
1.83 +% " n_eq = drop_questionmarks n_eq "^(* X_z = 4 * (1 / 2) ^^^ n * u [n] + -4 * (-1 / 4) ^^^ n * u [n]*)
1.84 +% "in n_eq)" (*([], Res), X_z = 4 * (1 / 2) ^^^ n * u [n] + -4 * (-1 / 4) ^^^ n * u [n]*)
1.85
1.86
1.87 .\\.\\.\\
1.88 -{\footnotesize
1.89 -\begin{verbatim}
1.90 - "Script InverseZTransform (X_eq::bool) = "^(*([], Frm), Problem (Isac, [Inverse, Z_Transform, SignalProcessing])*)
1.91 - "(let X = Take X_eq; "^(*([1], Frm), X z = 3 / (z - 1 / 4 + -1 / 8 * (1 / z))*)
1.92 - " X' = Rewrite ruleZY False X; "^(*([1], Res), ?X' z = 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))*)
1.93 - " (X'_z::real) = lhs X'; "^(* ?X' z*)
1.94 - " (zzz::real) = argument_in X'_z; "^(* z *)
1.95 - " (funterm::real) = rhs X'; "^(* 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))*)
1.96 -
1.97 - " (pbz::real) = (SubProblem (Isac', "^(**)
1.98 - " [partial_fraction,rational,simplification], "^
1.99 - " [simplification,of_rationals,to_partial_fraction]) "^
1.100 - " [REAL funterm, REAL zzz]); "^(*([2], Res), 4 / (z - 1 / 2) + -4 / (z - -1 / 4)*)
1.101 -
1.102 - " (pbz_eq::bool) = Take (X'_z = pbz); "^(*([3], Frm), ?X' z = 4 / (z - 1 / 2) + -4 / (z - -1 / 4)*)
1.103 - " pbz_eq = Rewrite ruleYZ False pbz_eq; "^(*([3], Res), ?X' z = 4 * (?z / (z - 1 / 2)) + -4 * (?z / (z - -1 / 4))*)
1.104 - " pbz_eq = drop_questionmarks pbz_eq; "^(* 4 * (z / (z - 1 / 2)) + -4 * (z / (z - -1 / 4))*)
1.105 - " (X_zeq::bool) = Take (X_z = rhs pbz_eq); "^(*([4], Frm), X_z = 4 * (z / (z - 1 / 2)) + -4 * (z / (z - -1 / 4))*)
1.106 - " n_eq = (Rewrite_Set inverse_z False) X_zeq; "^(*([4], Res), X_z = 4 * (1 / 2) ^^^ ?n * ?u [?n] + -4 * (-1 / 4) ^^^ ?n * ?u [?n]*)
1.107 - " n_eq = drop_questionmarks n_eq "^(* X_z = 4 * (1 / 2) ^^^ n * u [n] + -4 * (-1 / 4) ^^^ n * u [n]*)
1.108 - "in n_eq)" (*([], Res), X_z = 4 * (1 / 2) ^^^ n * u [n] + -4 * (-1 / 4) ^^^ n * u [n]*)
1.109 -\end{verbatim}}
1.110
1.111 \section{Workflow of Programming in the Prototype}\label{workflow}
1.112 -%WN ``workflow'' heisst: das mache ich zuerst, dann das ...
1.113 +
1.114 +\cite{makar-jedit-12}
1.115 +
1.116 \subsection{Preparations and Trials}\label{flow-prep}
1.117 +TODO Build\_Inverse\_Z\_Transform.thy ... ``imports PolyEq DiffApp Partial\_Fractions''
1.118 +.\\.\\.\\
1.119 +
1.120 +\subsection{Implementation in Isabelle/{\isac}}\label{flow-impl}
1.121 +TODO Build\_Inverse\_Z\_Transform.thy ... ``imports Isac''
1.122 +.\\.\\.\\
1.123 +
1.124 +below: calculation on the left; on the right are the tactics in the
1.125 +program which created the respective formula on the left.
1.126 +{\small\it
1.127 +\begin{tabbing}
1.128 +123l\=123\=123\=123\=123\=123\=123\=123\=123\=123\=123\=123\=\kill
1.129 +\>{\rm 01}\> $\bullet$ \> {\tt Problem } (Inverse\_Z\_Transform, [Inverse, Z\_Transform, SignalProcessing]) \`\\
1.130 +\>{\rm 02}\>\> $\vdash\;\;X z = \frac{3}{z - \frac{1}{4} - \frac{1}{8} \cdot z^{-1}}$ \`{\footnotesize {\tt Take} X\_eq}\\
1.131 +\>{\rm 03}\>\> $X z = \frac{3}{z + \frac{-1}{4} + \frac{-1}{8} \cdot \frac{1}{z}}$ \`{\footnotesize {\tt Rewrite} ruleZY X\_eq}\\
1.132 +\>{\rm 04}\>\> $\bullet$\> {\tt Problem } [partial\_fraction,rational,simplification] \`{\footnotesize {\tt SubProblem} \dots}\\
1.133 +\>{\rm 05}\>\>\> $\vdash\;\;\frac{3}{z + \frac{-1}{4} + \frac{-1}{8} \cdot \frac{1}{z}}=$ \`- - -\\
1.134 +\>{\rm 06}\>\>\> $\frac{24}{-1 + -2 \cdot z + 8 \cdot z^2}$ \`- - -\\
1.135 +\>{\rm 07}\>\>\> $\bullet$\> solve ($-1 + -2 \cdot z + 8 \cdot z^2,\;z$ ) \`- - -\\
1.136 +\>{\rm 08}\>\>\>\> $\vdash$ \> $\frac{3}{z + \frac{-1}{4} + \frac{-1}{8} \cdot \frac{1}{z}}=0$ \`- - -\\
1.137 +\>{\rm 09}\>\>\>\> $z = \frac{2+\sqrt{-4+8}}{16}\;\lor\;z = \frac{2-\sqrt{-4+8}}{16}$ \`- - -\\
1.138 +\>{\rm 10}\>\>\>\> $z = \frac{1}{2}\;\lor\;z =$ \_\_\_ \`- - -\\
1.139 +\> \>\>\>\> \_\_\_ \`- - -\\
1.140 +\>{\rm 11}\>\> \dots\> $\frac{4}{z - \frac{1}{2}} + \frac{-4}{z - \frac{-1}{4}}$ \`\\
1.141 +\>{\rm 12}\>\> $X^\prime z = {\cal Z}^{-1} (\frac{4}{z - \frac{1}{2}} + \frac{-4}{z - \frac{-1}{4}})$ \`{\footnotesize {\tt Take} ((X'::real =$>$ bool) z = ZZ\_1 part\_frac)}\\
1.142 +\>{\rm 13}\>\> $X^\prime z = {\cal Z}^{-1} (4\cdot\frac{z}{z - \frac{1}{2}} + -4\cdot\frac{z}{z - \frac{-1}{4}})$ \`{\footnotesize{\tt Rewrite\_Set} ruleYZ X'\_eq }\\
1.143 +\>{\rm 14}\>\> $X^\prime z = 4\cdot(\frac{1}{2})^n \cdot u [n] + -4\cdot(\frac{-1}{4})^n \cdot u [n]$ \`{\footnotesize {\tt Rewrite\_Set} inverse\_z X'\_eq}\\
1.144 +\>{\rm 15}\> \dots\> $X^\prime z = 4\cdot(\frac{1}{2})^n \cdot u [n] + -4\cdot(\frac{-1}{4})^n \cdot u [n]$ \`{\footnotesize {\tt Check\_Postcond}}
1.145 +\end{tabbing}}
1.146 +% ORIGINAL FROM Inverse_Z_Transform.thy
1.147 +% "Script InverseZTransform (X_eq::bool) = "^(*([], Frm), Problem (Isac, [Inverse, Z_Transform, SignalProcessing])*)
1.148 +% "(let X = Take X_eq; "^(*([1], Frm), X z = 3 / (z - 1 / 4 + -1 / 8 * (1 / z))*)
1.149 +% " X' = Rewrite ruleZY False X; "^(*([1], Res), ?X' z = 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))*)
1.150 +% " (X'_z::real) = lhs X'; "^(* ?X' z*)
1.151 +% " (zzz::real) = argument_in X'_z; "^(* z *)
1.152 +% " (funterm::real) = rhs X'; "^(* 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))*)
1.153 +%
1.154 +% " (pbz::real) = (SubProblem (Isac', "^(**)
1.155 +% " [partial_fraction,rational,simplification], "^
1.156 +% " [simplification,of_rationals,to_partial_fraction]) "^
1.157 +% " [REAL funterm, REAL zzz]); "^(*([2], Res), 4 / (z - 1 / 2) + -4 / (z - -1 / 4)*)
1.158 +%
1.159 +% " (pbz_eq::bool) = Take (X'_z = pbz); "^(*([3], Frm), ?X' z = 4 / (z - 1 / 2) + -4 / (z - -1 / 4)*)
1.160 +% " pbz_eq = Rewrite ruleYZ False pbz_eq; "^(*([3], Res), ?X' z = 4 * (?z / (z - 1 / 2)) + -4 * (?z / (z - -1 / 4))*)
1.161 +% " pbz_eq = drop_questionmarks pbz_eq; "^(* 4 * (z / (z - 1 / 2)) + -4 * (z / (z - -1 / 4))*)
1.162 +% " (X_zeq::bool) = Take (X_z = rhs pbz_eq); "^(*([4], Frm), X_z = 4 * (z / (z - 1 / 2)) + -4 * (z / (z - -1 / 4))*)
1.163 +% " n_eq = (Rewrite_Set inverse_z False) X_zeq; "^(*([4], Res), X_z = 4 * (1 / 2) ^^^ ?n * ?u [?n] + -4 * (-1 / 4) ^^^ ?n * ?u [?n]*)
1.164 +% " n_eq = drop_questionmarks n_eq "^(* X_z = 4 * (1 / 2) ^^^ n * u [n] + -4 * (-1 / 4) ^^^ n * u [n]*)
1.165 +% "in n_eq)" (*([], Res), X_z = 4 * (1 / 2) ^^^ n * u [n] + -4 * (-1 / 4) ^^^ n * u [n]*)
1.166 +
1.167 +.\\.\\.\\
1.168 +
1.169 +\subsection{Transfer into the Isabelle/{\isac} Knowledge}\label{flow-trans}
1.170 +TODO http://www.ist.tugraz.at/isac/index.php/Extend\_ISAC\_Knowledge\#Add\_an\_example ?
1.171 +
1.172 +
1.173 +
1.174 +
1.175 +\newpage
1.176 +-------------------------------------------------------------------
1.177 +
1.178 +Material, falls noch Platz bleibt ...
1.179 +
1.180 +-------------------------------------------------------------------
1.181 +
1.182 +
1.183 \subsubsection{Trials on Notation and Termination}
1.184
1.185 \paragraph{Technical notations} are a big problem for our piece of software,
1.186 @@ -990,18 +1037,6 @@
1.187 %simple eq and problem with double fractions/negative exponents
1.188
1.189
1.190 -\subsection{Implementation in Isabelle/{\isac}}\label{flow-impl}
1.191 -TODO Build\_Inverse\_Z\_Transform.thy ... ``imports Isac''
1.192 -
1.193 -\subsection{Transfer into the Isabelle/{\isac} Knowledge}\label{flow-trans}
1.194 -TODO http://www.ist.tugraz.at/isac/index.php/Extend\_ISAC\_Knowledge\#Add\_an\_example ?
1.195 -
1.196 --------------------------------------------------------------------
1.197 -
1.198 -Das unterhalb hab' ich noch nicht durchgearbeitet; einiges w\"are
1.199 -vermutlich auf andere sections aufzuteilen.
1.200 -
1.201 --------------------------------------------------------------------
1.202
1.203 \subsection{Formalization of missing knowledge in Isabelle}
1.204