326 $\leq$ most of which are overloaded for various types. |
326 $\leq$ most of which are overloaded for various types. |
327 |
327 |
328 HOL also supports some basic constructs from functional programming: |
328 HOL also supports some basic constructs from functional programming: |
329 {\footnotesize\it\label{isabelle-stmts} |
329 {\footnotesize\it\label{isabelle-stmts} |
330 \begin{tabbing} 123\=\kill |
330 \begin{tabbing} 123\=\kill |
331 \>$( \; {\tt if} \; b \; {\tt then} \; t_1 \; {\tt else} \; t_2 \;)$\\ |
331 01\>$( \; {\tt if} \; b \; {\tt then} \; t_1 \; {\tt else} \; t_2 \;)$\\ |
332 \>$( \; {\tt let} \; x=t \; {\tt in} \; u \; )$\\ |
332 02\>$( \; {\tt let} \; x=t \; {\tt in} \; u \; )$\\ |
333 \>$( \; {\tt case} \; t \; {\tt of} \; {\it pat}_1 |
333 03\>$( \; {\tt case} \; t \; {\tt of} \; {\it pat}_1 |
334 \Rightarrow t_1 \; |\dots| \; {\it pat}_n\Rightarrow t_n \; )$ |
334 \Rightarrow t_1 \; |\dots| \; {\it pat}_n\Rightarrow t_n \; )$ |
335 \end{tabbing}} |
335 \end{tabbing}} |
336 \noindent The running example's program uses some of these elements |
336 \noindent The running example's program uses some of these elements |
337 (marked by {\tt tt-font} on p.\pageref{s:impl}): for instance {\tt |
337 (marked by {\tt tt-font} on p.\pageref{s:impl}): for instance {\tt |
338 let}\dots{\tt in} in lines {\rm 02} \dots {\rm 13}. In fact, the whole program |
338 let}\dots{\tt in} in lines {\rm 02} \dots {\rm 13}. In fact, the whole program |
628 Z$-transform for a class of functions. The domain of Signal Processing |
628 Z$-transform for a class of functions. The domain of Signal Processing |
629 is accustomed to specific notation for the resulting functions, which |
629 is accustomed to specific notation for the resulting functions, which |
630 are absolutely capable of being totalled and are called step-response: $u[n]$, where $u$ is the |
630 are absolutely capable of being totalled and are called step-response: $u[n]$, where $u$ is the |
631 function, $n$ is the argument and the brackets indicate that the |
631 function, $n$ is the argument and the brackets indicate that the |
632 arguments are discrete. Surprisingly, Isabelle accepts the rules for |
632 arguments are discrete. Surprisingly, Isabelle accepts the rules for |
633 ${\cal z}^{-1}$ in this traditional notation~\footnote{Isabelle |
633 $z^{-1}$ in this traditional notation~\footnote{Isabelle |
634 experts might be particularly surprised, that the brackets do not |
634 experts might be particularly surprised, that the brackets do not |
635 cause errors in typing (as lists).}: |
635 cause errors in typing (as lists).}: |
636 %\vbox{ |
636 %\vbox{ |
637 % \begin{example} |
637 % \begin{example} |
638 \label{eg:neuper1} |
638 \label{eg:neuper1} |
639 {\footnotesize\begin{tabbing} |
639 {\footnotesize\begin{tabbing} |
640 123\=123\=123\=123\=\kill |
640 123\=123\=123\=123\=\kill |
641 |
641 |
642 \>axiomatization where \\ |
642 01\>axiomatization where \\ |
643 \>\> rule1: ``${\cal z}^{-1}\;1 = \delta [n]$'' and\\ |
643 02\>\> rule1: ``$z^{-1}\;1 = \delta [n]$'' and\\ |
644 \>\> rule2: ``$\vert\vert z \vert\vert > 1 \Rightarrow {\cal z}^{-1}\;z / (z - 1) = u [n]$'' and\\ |
644 03\>\> rule2: ``$\vert\vert z \vert\vert > 1 \Rightarrow z^{-1}\;z / (z - 1) = u [n]$'' and\\ |
645 \>\> rule3: ``$\vert\vert$ z $\vert\vert$ < 1 ==> z / (z - 1) = -u [-n - 1]'' and \\ |
645 04\>\> rule3: ``$\vert\vert z \vert\vert < 1 \Rightarrow z / (z - 1) = -u [-n - 1]$'' and \\ |
646 \>\> rule4: ``$\vert\vert$ z $\vert\vert$ > $\vert\vert$ $\alpha$ $\vert\vert$ ==> z / (z - $\alpha$) = $\alpha^n$ $\cdot$ u [n]'' and\\ |
646 05\>\> rule4: ``$\vert\vert z \vert\vert > \vert\vert$ $\alpha$ $\vert\vert \Rightarrow z / (z - \alpha) = \alpha^n \cdot u [n]$'' and\\ |
647 \>\> rule5: ``$\vert\vert$ z $\vert\vert$ < $\vert\vert$ $\alpha$ $\vert\vert$ ==> z / (z - $\alpha$) = -($\alpha^n$) $\cdot$ u [-n - 1]'' and\\ |
647 06\>\> rule5: ``$\vert\vert z \vert\vert < \vert\vert \alpha \vert\vert \Rightarrow z / (z - \alpha) = -(\alpha^n) \cdot u [-n - 1]$'' and\\ |
648 \>\> rule6: ``$\vert\vert$ z $\vert\vert$ > 1 ==> z/(z - 1)$^2$ = n $\cdot$ u [n]'' |
648 07\>\> rule6: ``$\vert\vert z \vert\vert > 1 \Rightarrow z/(z - 1)^2 = n \cdot u [n]$'' |
649 \end{tabbing}} |
649 \end{tabbing}} |
650 % \end{example} |
650 % \end{example} |
651 %} |
651 %} |
652 These 6 rules can be used as conditional rewrite rules, depending on |
652 These 6 rules can be used as conditional rewrite rules, depending on |
653 the respective convergence radius. Satisfaction from accordance with traditional notation |
653 the respective convergence radius. Satisfaction from accordance with traditional notation |
810 \textit{Build\_Inverse\_Z\_Transform.thy}; then it can be parsed in |
810 \textit{Build\_Inverse\_Z\_Transform.thy}; then it can be parsed in |
811 the context \textit{ctxt} of that theory: |
811 the context \textit{ctxt} of that theory: |
812 |
812 |
813 {\footnotesize |
813 {\footnotesize |
814 \begin{verbatim} |
814 \begin{verbatim} |
815 consts |
815 01 consts |
816 argument'_in :: "real => real" ("argument'_in _" 10) |
816 02 argument'_in :: "real => real" ("argument'_in _" 10) |
817 \end{verbatim}} |
817 \end{verbatim}} |
818 |
818 |
819 %^3.2^ ML {* val SOME t = parse ctxt "argument_in (X z)"; *} |
819 %^3.2^ ML {* val SOME t = parse ctxt "argument_in (X z)"; *} |
820 %^3.2^ val t = Const ("Build_Inverse_Z_Transform.argument'_in", "RealDef.real ⇒ RealDef.real") |
820 %^3.2^ val t = Const ("Build_Inverse_Z_Transform.argument'_in", "RealDef.real ⇒ RealDef.real") |
821 %^3.2^ $ (Free ("X", "RealDef.real ⇒ RealDef.real") $ Free ("z", "RealDef.real")): term |
821 %^3.2^ $ (Free ("X", "RealDef.real ⇒ RealDef.real") $ Free ("z", "RealDef.real")): term |
832 i.e in an \texttt{ML \{* *\}} block; the function definition provides |
832 i.e in an \texttt{ML \{* *\}} block; the function definition provides |
833 a unique prefix \texttt{eval\_} to the function name: |
833 a unique prefix \texttt{eval\_} to the function name: |
834 |
834 |
835 {\footnotesize |
835 {\footnotesize |
836 \begin{verbatim} |
836 \begin{verbatim} |
837 ML {* |
837 01 ML {* |
838 fun eval_argument_in _ |
838 02 fun eval_argument_in _ |
839 "Build_Inverse_Z_Transform.argument'_in" |
839 03 "Build_Inverse_Z_Transform.argument'_in" |
840 (t as (Const ("Build_Inverse_Z_Transform.argument'_in", _) $(f $arg))) _ = |
840 04 (t as (Const ("Build_Inverse_Z_Transform.argument'_in", _) $(f $arg))) _ = |
841 if is_Free arg (*could be something to be simplified before*) |
841 05 if is_Free arg (*could be something to be simplified before*) |
842 then SOME (term2str t ^"="^ term2str arg, Trueprop $(mk_equality (t, arg))) |
842 06 then SOME (term2str t ^"="^ term2str arg, Trueprop $(mk_equality (t, arg))) |
843 else NONE |
843 07 else NONE |
844 | eval_argument_in _ _ _ _ = NONE; |
844 08 | eval_argument_in _ _ _ _ = NONE; |
845 *} |
845 09 *} |
846 \end{verbatim}} |
846 \end{verbatim}} |
847 |
847 |
848 \noindent The function body creates either creates \texttt{NONE} |
848 \noindent The function body creates either creates \texttt{NONE} |
849 telling the rewrite-engine to search for the next regex, or creates an |
849 telling the rewrite-engine to search for the next regex, or creates an |
850 ad-hoc theorem for rewriting, thus the programmer needs to adopt many |
850 ad-hoc theorem for rewriting, thus the programmer needs to adopt many |
1337 the reason: type errors, a missing entry of the function somewhere or |
1337 the reason: type errors, a missing entry of the function somewhere or |
1338 even more nasty technicalities \dots |
1338 even more nasty technicalities \dots |
1339 |
1339 |
1340 {\footnotesize |
1340 {\footnotesize |
1341 \begin{verbatim} |
1341 \begin{verbatim} |
1342 ML {* |
1342 01 ML {* |
1343 val SOME t = parseNEW ctxt "argument_in (X (z::real))"; |
1343 02 val SOME t = parseNEW ctxt "argument_in (X (z::real))"; |
1344 val SOME (str, t') = eval_argument_in "" |
1344 03 val SOME (str, t') = eval_argument_in "" |
1345 "Build_Inverse_Z_Transform.argument'_in" t 0; |
1345 04 "Build_Inverse_Z_Transform.argument'_in" t 0; |
1346 term2str t'; |
1346 05 term2str t'; |
1347 *} |
1347 06 *} |
1348 val it = "(argument_in X z) = z": string |
1348 07 val it = "(argument_in X z) = z": string\end{verbatim}} |
1349 \end{verbatim}} |
|
1350 |
1349 |
1351 \noindent So, this works: we get an ad-hoc theorem, which used in |
1350 \noindent So, this works: we get an ad-hoc theorem, which used in |
1352 rewriting would reduce \texttt{argument\_in X z} to \texttt{z}. Now we check this |
1351 rewriting would reduce \texttt{argument\_in X z} to \texttt{z}. Now we check this |
1353 reduction and create a rule-set \texttt{rls} for that purpose: |
1352 reduction and create a rule-set \texttt{rls} for that purpose: |
1354 |
1353 |
1355 {\footnotesize |
1354 {\footnotesize |
1356 \begin{verbatim} |
1355 \begin{verbatim} |
1357 ML {* |
1356 01 ML {* |
1358 val rls = append_rls "test" e_rls |
1357 02 val rls = append_rls "test" e_rls |
1359 [Calc ("Build_Inverse_Z_Transform.argument'_in", eval_argument_in "")] |
1358 03 [Calc ("Build_Inverse_Z_Transform.argument'_in", eval_argument_in "")] |
1360 val SOME (t', asm) = rewrite_set_ @{theory} rls t; |
1359 04 val SOME (t', asm) = rewrite_set_ @{theory} rls t; |
1361 *} |
1360 05 *} |
1362 val t' = Free ("z", "RealDef.real"): term |
1361 06 val t' = Free ("z", "RealDef.real"): term |
1363 val asm = []: term list |
1362 07 val asm = []: term list\end{verbatim}} |
1364 \end{verbatim}} |
|
1365 |
1363 |
1366 \noindent The resulting term \texttt{t'} is \texttt{Free ("z", |
1364 \noindent The resulting term \texttt{t'} is \texttt{Free ("z", |
1367 "RealDef.real")}, i.e the variable \texttt{z}, so all is |
1365 "RealDef.real")}, i.e the variable \texttt{z}, so all is |
1368 perfect. Probably we have forgotten to store this function correctly~? |
1366 perfect. Probably we have forgotten to store this function correctly~? |
1369 We review the respective \texttt{calclist} (again an |
1367 We review the respective \texttt{calclist} (again an |
1370 \textit{Unsynchronized.ref} to be removed in order to adjust to |
1368 \textit{Unsynchronized.ref} to be removed in order to adjust to |
1371 IsabelleIsar's asynchronous document model): |
1369 IsabelleIsar's asynchronous document model): |
1372 |
1370 |
1373 {\footnotesize |
1371 {\footnotesize |
1374 \begin{verbatim} |
1372 \begin{verbatim} |
1375 calclist:= overwritel (! calclist, |
1373 01 calclist:= overwritel (! calclist, |
1376 [("argument_in",("Build_Inverse_Z_Transform.argument'_in", eval_argument_in "")), |
1374 02 [("argument_in", |
1377 ... |
1375 03 ("Build_Inverse_Z_Transform.argument'_in", eval_argument_in "")), |
1378 ]); |
1376 04 ... |
1379 \end{verbatim}} |
1377 05 ]);\end{verbatim}} |
1380 |
1378 |
1381 \noindent The entry is perfect. So what is the reason~? Ah, probably there |
1379 \noindent The entry is perfect. So what is the reason~? Ah, probably there |
1382 is something messed up with the many rule-sets in the method, see \S\ref{meth} --- |
1380 is something messed up with the many rule-sets in the method, see \S\ref{meth} --- |
1383 right, the function \texttt{argument\_in} is not contained in the respective |
1381 right, the function \texttt{argument\_in} is not contained in the respective |
1384 rule-set \textit{srls} \dots this just as an example of the intricacies in |
1382 rule-set \textit{srls} \dots this just as an example of the intricacies in |
1407 p.\pageref{fig-interactive} is different from this function}: |
1405 p.\pageref{fig-interactive} is different from this function}: |
1408 %the following is a simplification of the actual function |
1406 %the following is a simplification of the actual function |
1409 |
1407 |
1410 {\footnotesize |
1408 {\footnotesize |
1411 \begin{verbatim} |
1409 \begin{verbatim} |
1412 ML {* me; *} |
1410 01 ML {* me; *} |
1413 val it = tac -> ctree * pos -> mout * tac * ctree * pos |
1411 02 val it = tac -> ctree * pos -> mout * tac * ctree * pos\end{verbatim}} |
1414 \end{verbatim}} |
|
1415 |
1412 |
1416 \noindent This function takes as arguments a tactic \texttt{tac} which |
1413 \noindent This function takes as arguments a tactic \texttt{tac} which |
1417 determines the next step, the step applied to the interpreter-state |
1414 determines the next step, the step applied to the interpreter-state |
1418 \texttt{ctree * pos} as last argument taken. The interpreter-state is |
1415 \texttt{ctree * pos} as last argument taken. The interpreter-state is |
1419 a pair of a tree \texttt{ctree} representing the calculation created |
1416 a pair of a tree \texttt{ctree} representing the calculation created |
1424 |
1421 |
1425 This function allows to stepwise check the program: |
1422 This function allows to stepwise check the program: |
1426 |
1423 |
1427 {\footnotesize |
1424 {\footnotesize |
1428 \begin{verbatim} |
1425 \begin{verbatim} |
1429 ML {* |
1426 01 ML {* |
1430 val fmz = |
1427 02 val fmz = |
1431 ["filterExpression (X z = 3 / ((z::real) + 1/10 - 1/50*(1/z)))", |
1428 03 ["filterExpression (X z = 3 / ((z::real) + 1/10 - 1/50*(1/z)))", |
1432 "stepResponse (x[n::real]::bool)"]; |
1429 04 "stepResponse (x[n::real]::bool)"]; |
1433 val (dI,pI,mI) = |
1430 05 val (dI,pI,mI) = |
1434 ("Isac", |
1431 06 ("Isac", |
1435 ["Inverse", "Z_Transform", "SignalProcessing"], |
1432 07 ["Inverse", "Z_Transform", "SignalProcessing"], |
1436 ["SignalProcessing","Z_Transform","Inverse"]); |
1433 08 ["SignalProcessing","Z_Transform","Inverse"]); |
1437 val (mout, tac, ctree, pos) = CalcTreeTEST [(fmz, (dI, pI, mI))]; |
1434 09 val (mout, tac, ctree, pos) = CalcTreeTEST [(fmz, (dI, pI, mI))]; |
1438 val (mout, tac, ctree, pos) = me tac (ctree, pos); |
1435 10 val (mout, tac, ctree, pos) = me tac (ctree, pos); |
1439 val (mout, tac, ctree, pos) = me tac (ctree, pos); |
1436 11 val (mout, tac, ctree, pos) = me tac (ctree, pos); |
1440 val (mout, tac, ctree, pos) = me tac (ctree, pos); |
1437 12 val (mout, tac, ctree, pos) = me tac (ctree, pos); |
1441 ...\end{verbatim}} |
1438 13 ...\end{verbatim}} |
1442 |
1439 |
1443 \noindent Several dozens of calls for \texttt{me} are required to |
1440 \noindent Several dozens of calls for \texttt{me} are required to |
1444 create the lines in the calculation below (including the sub-problems |
1441 create the lines in the calculation below (including the sub-problems |
1445 not shown). When an error occurs, the reason might be located |
1442 not shown). When an error occurs, the reason might be located |
1446 many steps before: if evaluation by rewriting, as done by the prototype, |
1443 many steps before: if evaluation by rewriting, as done by the prototype, |