1.1 --- a/doc-src/isac/jrocnik/eJMT-paper/jrocnik_eJMT.tex Thu Sep 13 22:44:56 2012 +0200
1.2 +++ b/doc-src/isac/jrocnik/eJMT-paper/jrocnik_eJMT.tex Fri Sep 14 10:00:16 2012 +0200
1.3 @@ -328,9 +328,9 @@
1.4 HOL also supports some basic constructs from functional programming:
1.5 {\footnotesize\it\label{isabelle-stmts}
1.6 \begin{tabbing} 123\=\kill
1.7 -\>$( \; {\tt if} \; b \; {\tt then} \; t_1 \; {\tt else} \; t_2 \;)$\\
1.8 -\>$( \; {\tt let} \; x=t \; {\tt in} \; u \; )$\\
1.9 -\>$( \; {\tt case} \; t \; {\tt of} \; {\it pat}_1
1.10 +01\>$( \; {\tt if} \; b \; {\tt then} \; t_1 \; {\tt else} \; t_2 \;)$\\
1.11 +02\>$( \; {\tt let} \; x=t \; {\tt in} \; u \; )$\\
1.12 +03\>$( \; {\tt case} \; t \; {\tt of} \; {\it pat}_1
1.13 \Rightarrow t_1 \; |\dots| \; {\it pat}_n\Rightarrow t_n \; )$
1.14 \end{tabbing}}
1.15 \noindent The running example's program uses some of these elements
1.16 @@ -630,7 +630,7 @@
1.17 are absolutely capable of being totalled and are called step-response: $u[n]$, where $u$ is the
1.18 function, $n$ is the argument and the brackets indicate that the
1.19 arguments are discrete. Surprisingly, Isabelle accepts the rules for
1.20 -${\cal z}^{-1}$ in this traditional notation~\footnote{Isabelle
1.21 +$z^{-1}$ in this traditional notation~\footnote{Isabelle
1.22 experts might be particularly surprised, that the brackets do not
1.23 cause errors in typing (as lists).}:
1.24 %\vbox{
1.25 @@ -639,13 +639,13 @@
1.26 {\footnotesize\begin{tabbing}
1.27 123\=123\=123\=123\=\kill
1.28
1.29 - \>axiomatization where \\
1.30 - \>\> rule1: ``${\cal z}^{-1}\;1 = \delta [n]$'' and\\
1.31 - \>\> rule2: ``$\vert\vert z \vert\vert > 1 \Rightarrow {\cal z}^{-1}\;z / (z - 1) = u [n]$'' and\\
1.32 - \>\> rule3: ``$\vert\vert$ z $\vert\vert$ < 1 ==> z / (z - 1) = -u [-n - 1]'' and \\
1.33 - \>\> rule4: ``$\vert\vert$ z $\vert\vert$ > $\vert\vert$ $\alpha$ $\vert\vert$ ==> z / (z - $\alpha$) = $\alpha^n$ $\cdot$ u [n]'' and\\
1.34 - \>\> rule5: ``$\vert\vert$ z $\vert\vert$ < $\vert\vert$ $\alpha$ $\vert\vert$ ==> z / (z - $\alpha$) = -($\alpha^n$) $\cdot$ u [-n - 1]'' and\\
1.35 - \>\> rule6: ``$\vert\vert$ z $\vert\vert$ > 1 ==> z/(z - 1)$^2$ = n $\cdot$ u [n]''
1.36 + 01\>axiomatization where \\
1.37 + 02\>\> rule1: ``$z^{-1}\;1 = \delta [n]$'' and\\
1.38 + 03\>\> rule2: ``$\vert\vert z \vert\vert > 1 \Rightarrow z^{-1}\;z / (z - 1) = u [n]$'' and\\
1.39 + 04\>\> rule3: ``$\vert\vert z \vert\vert < 1 \Rightarrow z / (z - 1) = -u [-n - 1]$'' and \\
1.40 + 05\>\> rule4: ``$\vert\vert z \vert\vert > \vert\vert$ $\alpha$ $\vert\vert \Rightarrow z / (z - \alpha) = \alpha^n \cdot u [n]$'' and\\
1.41 + 06\>\> rule5: ``$\vert\vert z \vert\vert < \vert\vert \alpha \vert\vert \Rightarrow z / (z - \alpha) = -(\alpha^n) \cdot u [-n - 1]$'' and\\
1.42 + 07\>\> rule6: ``$\vert\vert z \vert\vert > 1 \Rightarrow z/(z - 1)^2 = n \cdot u [n]$''
1.43 \end{tabbing}}
1.44 % \end{example}
1.45 %}
1.46 @@ -812,8 +812,8 @@
1.47
1.48 {\footnotesize
1.49 \begin{verbatim}
1.50 - consts
1.51 - argument'_in :: "real => real" ("argument'_in _" 10)
1.52 +01 consts
1.53 +02 argument'_in :: "real => real" ("argument'_in _" 10)
1.54 \end{verbatim}}
1.55
1.56 %^3.2^ ML {* val SOME t = parse ctxt "argument_in (X z)"; *}
1.57 @@ -834,15 +834,15 @@
1.58
1.59 {\footnotesize
1.60 \begin{verbatim}
1.61 - ML {*
1.62 - fun eval_argument_in _
1.63 - "Build_Inverse_Z_Transform.argument'_in"
1.64 - (t as (Const ("Build_Inverse_Z_Transform.argument'_in", _) $(f $arg))) _ =
1.65 - if is_Free arg (*could be something to be simplified before*)
1.66 - then SOME (term2str t ^"="^ term2str arg, Trueprop $(mk_equality (t, arg)))
1.67 - else NONE
1.68 - | eval_argument_in _ _ _ _ = NONE;
1.69 - *}
1.70 +01 ML {*
1.71 +02 fun eval_argument_in _
1.72 +03 "Build_Inverse_Z_Transform.argument'_in"
1.73 +04 (t as (Const ("Build_Inverse_Z_Transform.argument'_in", _) $(f $arg))) _ =
1.74 +05 if is_Free arg (*could be something to be simplified before*)
1.75 +06 then SOME (term2str t ^"="^ term2str arg, Trueprop $(mk_equality (t, arg)))
1.76 +07 else NONE
1.77 +08 | eval_argument_in _ _ _ _ = NONE;
1.78 +09 *}
1.79 \end{verbatim}}
1.80
1.81 \noindent The function body creates either creates \texttt{NONE}
1.82 @@ -1339,14 +1339,13 @@
1.83
1.84 {\footnotesize
1.85 \begin{verbatim}
1.86 - ML {*
1.87 - val SOME t = parseNEW ctxt "argument_in (X (z::real))";
1.88 - val SOME (str, t') = eval_argument_in ""
1.89 - "Build_Inverse_Z_Transform.argument'_in" t 0;
1.90 - term2str t';
1.91 - *}
1.92 - val it = "(argument_in X z) = z": string
1.93 -\end{verbatim}}
1.94 +01 ML {*
1.95 +02 val SOME t = parseNEW ctxt "argument_in (X (z::real))";
1.96 +03 val SOME (str, t') = eval_argument_in ""
1.97 +04 "Build_Inverse_Z_Transform.argument'_in" t 0;
1.98 +05 term2str t';
1.99 +06 *}
1.100 +07 val it = "(argument_in X z) = z": string\end{verbatim}}
1.101
1.102 \noindent So, this works: we get an ad-hoc theorem, which used in
1.103 rewriting would reduce \texttt{argument\_in X z} to \texttt{z}. Now we check this
1.104 @@ -1354,14 +1353,13 @@
1.105
1.106 {\footnotesize
1.107 \begin{verbatim}
1.108 - ML {*
1.109 - val rls = append_rls "test" e_rls
1.110 - [Calc ("Build_Inverse_Z_Transform.argument'_in", eval_argument_in "")]
1.111 - val SOME (t', asm) = rewrite_set_ @{theory} rls t;
1.112 - *}
1.113 - val t' = Free ("z", "RealDef.real"): term
1.114 - val asm = []: term list
1.115 -\end{verbatim}}
1.116 +01 ML {*
1.117 +02 val rls = append_rls "test" e_rls
1.118 +03 [Calc ("Build_Inverse_Z_Transform.argument'_in", eval_argument_in "")]
1.119 +04 val SOME (t', asm) = rewrite_set_ @{theory} rls t;
1.120 +05 *}
1.121 +06 val t' = Free ("z", "RealDef.real"): term
1.122 +07 val asm = []: term list\end{verbatim}}
1.123
1.124 \noindent The resulting term \texttt{t'} is \texttt{Free ("z",
1.125 "RealDef.real")}, i.e the variable \texttt{z}, so all is
1.126 @@ -1372,11 +1370,11 @@
1.127
1.128 {\footnotesize
1.129 \begin{verbatim}
1.130 - calclist:= overwritel (! calclist,
1.131 - [("argument_in",("Build_Inverse_Z_Transform.argument'_in", eval_argument_in "")),
1.132 - ...
1.133 - ]);
1.134 -\end{verbatim}}
1.135 +01 calclist:= overwritel (! calclist,
1.136 +02 [("argument_in",
1.137 +03 ("Build_Inverse_Z_Transform.argument'_in", eval_argument_in "")),
1.138 +04 ...
1.139 +05 ]);\end{verbatim}}
1.140
1.141 \noindent The entry is perfect. So what is the reason~? Ah, probably there
1.142 is something messed up with the many rule-sets in the method, see \S\ref{meth} ---
1.143 @@ -1409,9 +1407,8 @@
1.144
1.145 {\footnotesize
1.146 \begin{verbatim}
1.147 - ML {* me; *}
1.148 - val it = tac -> ctree * pos -> mout * tac * ctree * pos
1.149 -\end{verbatim}}
1.150 +01 ML {* me; *}
1.151 +02 val it = tac -> ctree * pos -> mout * tac * ctree * pos\end{verbatim}}
1.152
1.153 \noindent This function takes as arguments a tactic \texttt{tac} which
1.154 determines the next step, the step applied to the interpreter-state
1.155 @@ -1426,19 +1423,19 @@
1.156
1.157 {\footnotesize
1.158 \begin{verbatim}
1.159 - ML {*
1.160 - val fmz =
1.161 - ["filterExpression (X z = 3 / ((z::real) + 1/10 - 1/50*(1/z)))",
1.162 - "stepResponse (x[n::real]::bool)"];
1.163 - val (dI,pI,mI) =
1.164 - ("Isac",
1.165 - ["Inverse", "Z_Transform", "SignalProcessing"],
1.166 - ["SignalProcessing","Z_Transform","Inverse"]);
1.167 - val (mout, tac, ctree, pos) = CalcTreeTEST [(fmz, (dI, pI, mI))];
1.168 - val (mout, tac, ctree, pos) = me tac (ctree, pos);
1.169 - val (mout, tac, ctree, pos) = me tac (ctree, pos);
1.170 - val (mout, tac, ctree, pos) = me tac (ctree, pos);
1.171 - ...\end{verbatim}}
1.172 +01 ML {*
1.173 +02 val fmz =
1.174 +03 ["filterExpression (X z = 3 / ((z::real) + 1/10 - 1/50*(1/z)))",
1.175 +04 "stepResponse (x[n::real]::bool)"];
1.176 +05 val (dI,pI,mI) =
1.177 +06 ("Isac",
1.178 +07 ["Inverse", "Z_Transform", "SignalProcessing"],
1.179 +08 ["SignalProcessing","Z_Transform","Inverse"]);
1.180 +09 val (mout, tac, ctree, pos) = CalcTreeTEST [(fmz, (dI, pI, mI))];
1.181 +10 val (mout, tac, ctree, pos) = me tac (ctree, pos);
1.182 +11 val (mout, tac, ctree, pos) = me tac (ctree, pos);
1.183 +12 val (mout, tac, ctree, pos) = me tac (ctree, pos);
1.184 +13 ...\end{verbatim}}
1.185
1.186 \noindent Several dozens of calls for \texttt{me} are required to
1.187 create the lines in the calculation below (including the sub-problems