837 |
838 |
838 {\small\it\begin{tabbing} |
839 {\small\it\begin{tabbing} |
839 123l\=123\=123\=123\=123\=123\=123\=123\=123\=(x \=123\=123\=\kill |
840 123l\=123\=123\=123\=123\=123\=123\=123\=123\=(x \=123\=123\=\kill |
840 \>{\rm 01}\> {\tt Program} InverseZTransform (X\_eq::bool) = \\ |
841 \>{\rm 01}\> {\tt Program} InverseZTransform (X\_eq::bool) = \\ |
841 \>{\rm 02}\>\> {\tt LET} \\ |
842 \>{\rm 02}\>\> {\tt LET} \\ |
842 \>{\rm 03}\>\>\> X = {\tt Take} X\_eq ; \\ |
843 \>{\rm 03}\>\>\> X\_eq = {\tt Take} X\_eq ; \\ |
843 \>{\rm 04}\>\>\> X' = {\tt Rewrite} ruleZY X ; \\ |
844 \>{\rm 04}\>\>\> X\_eq = {\tt Rewrite} ruleZY X\_eq ; \\ |
844 \>{\rm 05}\>\>\> (X'\_z::real) = lhs X' ; \\ |
845 \>{\rm 05}\>\>\> (X\_z::real) = lhs X\_eq ; \\ %no inside-out evaluation |
845 \>{\rm 06}\>\>\> (zzz::real) = argument\_in X'\_z; \\ |
846 \>{\rm 06}\>\>\> (z::real) = argument\_in X\_z; \\ |
846 \>{\rm 07}\>\>\> (funterm::real) = rhs X’; \\ |
847 \>{\rm 07}\>\>\> (part\_frac::real) = {\tt SubProblem} \\ |
847 \>{\rm 07}\>\>\> (pbz::real) = {\tt SubProblem} \\ |
848 \>{\rm 08}\>\>\>\>\>\>\>\> ( \> Isac, \\ |
848 \>{\rm 08}\>\>\>\>\>\>\>\> ( \> Inverse\_Z\_Transform, \\ |
849 \>{\rm 08}\>\>\>\>\>\>\>\>\> [partial\_fraction, rational, simplification]\\ |
849 \>{\rm 08}\>\>\>\>\>\>\>\>\> [partial\_fraction,rational,simplification]\\ |
|
850 \>{\rm 09}\>\>\>\>\>\>\>\>\> [simplification,of\_rationals,to\_partial\_fraction] ) \\ |
850 \>{\rm 09}\>\>\>\>\>\>\>\>\> [simplification,of\_rationals,to\_partial\_fraction] ) \\ |
851 \>{\rm 10}\>\>\>\>\>\>\>\> [ funterm::real, zzz::real ]; \\ |
851 \>{\rm 10}\>\>\>\>\>\>\>\> [ (rhs X\_eq)::real, z::real ]; \\ |
852 \>{\rm 12}\>\>\> (pbz\_eq::bool) = {\tt Take} (X'\_z = pbz) ; \\ |
852 \>{\rm 12}\>\>\> (X'\_eq::bool) = {\tt Take} ((X'::real =$>$ bool) z = ZZ\_1 part\_frac) ; \\ |
853 |
853 |
854 \>{\rm 12}\>\>\> pbz\_eq = {\tt Rewrite} ruleYZ pbz\_eq ; \\ |
854 \>{\rm 12}\>\>\> X'\_eq = {\tt Rewrite\_Set} ruleYZ X'\_eq ; \\ |
855 \>{\rm 13}\>\>\> pbz\_eq = drop\_questionmarks pbz\_eq ; \\ |
855 \>{\rm 15}\>\>\> X'\_eq = {\tt Rewrite\_Set} inverse\_z X'\_eq \\ |
856 \>{\rm 14}\>\>\> (X\_zeq::bool) = {\tt Take} (X\_z = rhs pbz\_eq) ; \\ |
|
857 \>{\rm 15}\>\>\> n\_eq = {\tt Rewrite\_Set} inverse\_z X\_zeq ; \\ |
|
858 \>{\rm 15}\>\>\> n\_eq = drop\_questionmarks n\_eq \\ |
|
859 \>{\rm 16}\>\> {\tt IN } \\ |
856 \>{\rm 16}\>\> {\tt IN } \\ |
860 \>{\rm 15}\>\>\> n\_eq |
857 \>{\rm 15}\>\>\> X'\_eq |
861 \end{tabbing}} |
858 \end{tabbing}} |
862 |
859 % ORIGINAL FROM Inverse_Z_Transform.thy |
863 {\small\it\begin{tabbing} |
860 % "Script InverseZTransform (X_eq::bool) = "^(*([], Frm), Problem (Isac, [Inverse, Z_Transform, SignalProcessing])*) |
864 123l\=123\=123\=123\=123\=123\=123\=123\=123\=123\=123\=123\=\kill\label{exp-calc} |
861 % "(let X = Take X_eq; "^(*([1], Frm), X z = 3 / (z - 1 / 4 + -1 / 8 * (1 / z))*) |
865 \>{\rm 01}\> $\bullet$\> {\tt Problem } [maximum\_by, calculus] \`- - -\\ |
862 % " X' = Rewrite ruleZY False X; "^(*([1], Res), ?X' z = 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))*) |
866 \>{\rm 02}\>\> $\vdash$\> $A = 2\cdot u\cdot v - u^2$ \`- - -\\ |
863 % " (X'_z::real) = lhs X'; "^(* ?X' z*) |
867 \>{\rm 03}\>\> $\bullet$\> {\tt Problem } [make, diffable, function] \`- - -\\ |
864 % " (zzz::real) = argument_in X'_z; "^(* z *) |
868 \>{\rm 04}\>\> \dots\> $\widetilde{A}(\alpha) = 8\cdot r^2\cdot\sin\alpha\cdot\cos\alpha - 4\cdot r^2\cdot(\sin\alpha)^2$ \`- - -\\ |
865 % " (funterm::real) = rhs X'; "^(* 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))*) |
869 \\ |
866 % |
870 \\ |
867 % " (pbz::real) = (SubProblem (Isac', "^(**) |
871 \>{\rm 18}\>\> $\bullet$\> {\tt Problem} [find\_values, tool] \`- - -\\ |
868 % " [partial_fraction,rational,simplification], "^ |
872 % \`{\tt Apply\_Method} [tool, find\_values]\\ |
869 % " [simplification,of_rationals,to_partial_fraction]) "^ |
873 \>{\rm 19}\>\> \dots\> [ $u=0.23\cdot r, \:v=0.76\cdot r$ ] \`- - -\\ |
870 % " [REAL funterm, REAL zzz]); "^(*([2], Res), 4 / (z - 1 / 2) + -4 / (z - -1 / 4)*) |
874 % \`{\tt Check\_Postcond}\\ |
871 % |
875 \>{\rm 20}\> \dots\> [ $u=0.23\cdot r, \:v=0.76\cdot r$ ] %TODO calculate ! |
872 % " (pbz_eq::bool) = Take (X'_z = pbz); "^(*([3], Frm), ?X' z = 4 / (z - 1 / 2) + -4 / (z - -1 / 4)*) |
876 |
873 % " pbz_eq = Rewrite ruleYZ False pbz_eq; "^(*([3], Res), ?X' z = 4 * (?z / (z - 1 / 2)) + -4 * (?z / (z - -1 / 4))*) |
|
874 % " pbz_eq = drop_questionmarks pbz_eq; "^(* 4 * (z / (z - 1 / 2)) + -4 * (z / (z - -1 / 4))*) |
|
875 % " (X_zeq::bool) = Take (X_z = rhs pbz_eq); "^(*([4], Frm), X_z = 4 * (z / (z - 1 / 2)) + -4 * (z / (z - -1 / 4))*) |
|
876 % " 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]*) |
|
877 % " n_eq = drop_questionmarks n_eq "^(* X_z = 4 * (1 / 2) ^^^ n * u [n] + -4 * (-1 / 4) ^^^ n * u [n]*) |
|
878 % "in n_eq)" (*([], Res), X_z = 4 * (1 / 2) ^^^ n * u [n] + -4 * (-1 / 4) ^^^ n * u [n]*) |
|
879 |
|
880 |
|
881 .\\.\\.\\ |
|
882 |
|
883 \section{Workflow of Programming in the Prototype}\label{workflow} |
|
884 |
|
885 \cite{makar-jedit-12} |
|
886 |
|
887 \subsection{Preparations and Trials}\label{flow-prep} |
|
888 TODO Build\_Inverse\_Z\_Transform.thy ... ``imports PolyEq DiffApp Partial\_Fractions'' |
|
889 .\\.\\.\\ |
|
890 |
|
891 \subsection{Implementation in Isabelle/{\isac}}\label{flow-impl} |
|
892 TODO Build\_Inverse\_Z\_Transform.thy ... ``imports Isac'' |
|
893 .\\.\\.\\ |
|
894 |
|
895 below: calculation on the left; on the right are the tactics in the |
|
896 program which created the respective formula on the left. |
|
897 {\small\it |
|
898 \begin{tabbing} |
|
899 123l\=123\=123\=123\=123\=123\=123\=123\=123\=123\=123\=123\=\kill |
|
900 \>{\rm 01}\> $\bullet$ \> {\tt Problem } (Inverse\_Z\_Transform, [Inverse, Z\_Transform, SignalProcessing]) \`\\ |
|
901 \>{\rm 02}\>\> $\vdash\;\;X z = \frac{3}{z - \frac{1}{4} - \frac{1}{8} \cdot z^{-1}}$ \`{\footnotesize {\tt Take} X\_eq}\\ |
|
902 \>{\rm 03}\>\> $X z = \frac{3}{z + \frac{-1}{4} + \frac{-1}{8} \cdot \frac{1}{z}}$ \`{\footnotesize {\tt Rewrite} ruleZY X\_eq}\\ |
|
903 \>{\rm 04}\>\> $\bullet$\> {\tt Problem } [partial\_fraction,rational,simplification] \`{\footnotesize {\tt SubProblem} \dots}\\ |
|
904 \>{\rm 05}\>\>\> $\vdash\;\;\frac{3}{z + \frac{-1}{4} + \frac{-1}{8} \cdot \frac{1}{z}}=$ \`- - -\\ |
|
905 \>{\rm 06}\>\>\> $\frac{24}{-1 + -2 \cdot z + 8 \cdot z^2}$ \`- - -\\ |
|
906 \>{\rm 07}\>\>\> $\bullet$\> solve ($-1 + -2 \cdot z + 8 \cdot z^2,\;z$ ) \`- - -\\ |
|
907 \>{\rm 08}\>\>\>\> $\vdash$ \> $\frac{3}{z + \frac{-1}{4} + \frac{-1}{8} \cdot \frac{1}{z}}=0$ \`- - -\\ |
|
908 \>{\rm 09}\>\>\>\> $z = \frac{2+\sqrt{-4+8}}{16}\;\lor\;z = \frac{2-\sqrt{-4+8}}{16}$ \`- - -\\ |
|
909 \>{\rm 10}\>\>\>\> $z = \frac{1}{2}\;\lor\;z =$ \_\_\_ \`- - -\\ |
|
910 \> \>\>\>\> \_\_\_ \`- - -\\ |
|
911 \>{\rm 11}\>\> \dots\> $\frac{4}{z - \frac{1}{2}} + \frac{-4}{z - \frac{-1}{4}}$ \`\\ |
|
912 \>{\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)}\\ |
|
913 \>{\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 }\\ |
|
914 \>{\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}\\ |
|
915 \>{\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}} |
877 \end{tabbing}} |
916 \end{tabbing}} |
878 |
917 % ORIGINAL FROM Inverse_Z_Transform.thy |
|
918 % "Script InverseZTransform (X_eq::bool) = "^(*([], Frm), Problem (Isac, [Inverse, Z_Transform, SignalProcessing])*) |
|
919 % "(let X = Take X_eq; "^(*([1], Frm), X z = 3 / (z - 1 / 4 + -1 / 8 * (1 / z))*) |
|
920 % " X' = Rewrite ruleZY False X; "^(*([1], Res), ?X' z = 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))*) |
|
921 % " (X'_z::real) = lhs X'; "^(* ?X' z*) |
|
922 % " (zzz::real) = argument_in X'_z; "^(* z *) |
|
923 % " (funterm::real) = rhs X'; "^(* 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))*) |
|
924 % |
|
925 % " (pbz::real) = (SubProblem (Isac', "^(**) |
|
926 % " [partial_fraction,rational,simplification], "^ |
|
927 % " [simplification,of_rationals,to_partial_fraction]) "^ |
|
928 % " [REAL funterm, REAL zzz]); "^(*([2], Res), 4 / (z - 1 / 2) + -4 / (z - -1 / 4)*) |
|
929 % |
|
930 % " (pbz_eq::bool) = Take (X'_z = pbz); "^(*([3], Frm), ?X' z = 4 / (z - 1 / 2) + -4 / (z - -1 / 4)*) |
|
931 % " pbz_eq = Rewrite ruleYZ False pbz_eq; "^(*([3], Res), ?X' z = 4 * (?z / (z - 1 / 2)) + -4 * (?z / (z - -1 / 4))*) |
|
932 % " pbz_eq = drop_questionmarks pbz_eq; "^(* 4 * (z / (z - 1 / 2)) + -4 * (z / (z - -1 / 4))*) |
|
933 % " (X_zeq::bool) = Take (X_z = rhs pbz_eq); "^(*([4], Frm), X_z = 4 * (z / (z - 1 / 2)) + -4 * (z / (z - -1 / 4))*) |
|
934 % " 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]*) |
|
935 % " n_eq = drop_questionmarks n_eq "^(* X_z = 4 * (1 / 2) ^^^ n * u [n] + -4 * (-1 / 4) ^^^ n * u [n]*) |
|
936 % "in n_eq)" (*([], Res), X_z = 4 * (1 / 2) ^^^ n * u [n] + -4 * (-1 / 4) ^^^ n * u [n]*) |
879 |
937 |
880 .\\.\\.\\ |
938 .\\.\\.\\ |
881 {\footnotesize |
939 |
882 \begin{verbatim} |
940 \subsection{Transfer into the Isabelle/{\isac} Knowledge}\label{flow-trans} |
883 "Script InverseZTransform (X_eq::bool) = "^(*([], Frm), Problem (Isac, [Inverse, Z_Transform, SignalProcessing])*) |
941 TODO http://www.ist.tugraz.at/isac/index.php/Extend\_ISAC\_Knowledge\#Add\_an\_example ? |
884 "(let X = Take X_eq; "^(*([1], Frm), X z = 3 / (z - 1 / 4 + -1 / 8 * (1 / z))*) |
942 |
885 " X' = Rewrite ruleZY False X; "^(*([1], Res), ?X' z = 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))*) |
943 |
886 " (X'_z::real) = lhs X'; "^(* ?X' z*) |
944 |
887 " (zzz::real) = argument_in X'_z; "^(* z *) |
945 |
888 " (funterm::real) = rhs X'; "^(* 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))*) |
946 \newpage |
889 |
947 ------------------------------------------------------------------- |
890 " (pbz::real) = (SubProblem (Isac', "^(**) |
948 |
891 " [partial_fraction,rational,simplification], "^ |
949 Material, falls noch Platz bleibt ... |
892 " [simplification,of_rationals,to_partial_fraction]) "^ |
950 |
893 " [REAL funterm, REAL zzz]); "^(*([2], Res), 4 / (z - 1 / 2) + -4 / (z - -1 / 4)*) |
951 ------------------------------------------------------------------- |
894 |
952 |
895 " (pbz_eq::bool) = Take (X'_z = pbz); "^(*([3], Frm), ?X' z = 4 / (z - 1 / 2) + -4 / (z - -1 / 4)*) |
953 |
896 " pbz_eq = Rewrite ruleYZ False pbz_eq; "^(*([3], Res), ?X' z = 4 * (?z / (z - 1 / 2)) + -4 * (?z / (z - -1 / 4))*) |
|
897 " pbz_eq = drop_questionmarks pbz_eq; "^(* 4 * (z / (z - 1 / 2)) + -4 * (z / (z - -1 / 4))*) |
|
898 " (X_zeq::bool) = Take (X_z = rhs pbz_eq); "^(*([4], Frm), X_z = 4 * (z / (z - 1 / 2)) + -4 * (z / (z - -1 / 4))*) |
|
899 " 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]*) |
|
900 " n_eq = drop_questionmarks n_eq "^(* X_z = 4 * (1 / 2) ^^^ n * u [n] + -4 * (-1 / 4) ^^^ n * u [n]*) |
|
901 "in n_eq)" (*([], Res), X_z = 4 * (1 / 2) ^^^ n * u [n] + -4 * (-1 / 4) ^^^ n * u [n]*) |
|
902 \end{verbatim}} |
|
903 |
|
904 \section{Workflow of Programming in the Prototype}\label{workflow} |
|
905 %WN ``workflow'' heisst: das mache ich zuerst, dann das ... |
|
906 \subsection{Preparations and Trials}\label{flow-prep} |
|
907 \subsubsection{Trials on Notation and Termination} |
954 \subsubsection{Trials on Notation and Termination} |
908 |
955 |
909 \paragraph{Technical notations} are a big problem for our piece of software, |
956 \paragraph{Technical notations} are a big problem for our piece of software, |
910 but the reason for that isn't a fault of the software itself, one of the |
957 but the reason for that isn't a fault of the software itself, one of the |
911 troubles comes out of the fact that different technical subtopics use different |
958 troubles comes out of the fact that different technical subtopics use different |