1.1 --- a/doc-isac/jrocnik/eJMT-paper/jrocnik_eJMT.tex Mon Oct 31 18:28:36 2022 +0100
1.2 +++ b/doc-isac/jrocnik/eJMT-paper/jrocnik_eJMT.tex Mon Nov 07 17:37:20 2022 +0100
1.3 @@ -802,12 +802,12 @@
1.4 01 val inverse_z = Rls
1.5 02 {id = "inverse_z",
1.6 03 rew_ord = dummy_ord,
1.7 - 04 erls = Erls,
1.8 + 04 asm_rls = Erls,
1.9 05 rules = [Thm ("rule1", @{thm rule1}), Thm ("rule2", @{thm rule1}),
1.10 06 Thm ("rule3", @{thm rule3}), Thm ("rule4", @{thm rule4}),
1.11 07 Thm ("rule5", @{thm rule5}), Thm ("rule6", @{thm rule6})],
1.12 08 errpatts = [],
1.13 - 09 scr = ""}
1.14 + 09 program = ""}
1.15 \end{verbatim}}
1.16
1.17 \noindent The items, line by line, in the above record have the following purpose:
1.18 @@ -819,7 +819,7 @@
1.19 line {\rm 12}).
1.20
1.21 \item[03..04] both, (a) the rewrite-order~\cite{nipk:rew-all-that}
1.22 -\textit{rew\_ord} and (b) the rule-set \textit{erls} are trivial here:
1.23 +\textit{rew\_ord} and (b) the rule-set \textit{asm_rls} are trivial here:
1.24 (a) the \textit{rules} in {\rm 07..12} don't need ordered rewriting
1.25 and (b) the assumptions of the \textit{rules} need not be evaluated
1.26 (they just go into the context during rewriting).
1.27 @@ -830,7 +830,7 @@
1.28 and \textit{Calc} respectively; for the purpose of reflection both
1.29 contain their identifiers.
1.30
1.31 -\item[08..09] are error-patterns not discussed here and \textit{scr}
1.32 +\item[08..09] are error-patterns not discussed here and \textit{program}
1.33 is prepared to get a program, automatically generated by {\sisac} for
1.34 producing intermediate rewrites when requested by the user.
1.35
1.36 @@ -1109,7 +1109,7 @@
1.37 08 ("#Pre" , ["(rhs X_eq) is_continuous_in D"]),
1.38 09 ("#Find" , ["stepResponse n_eq"]),
1.39 10 ("#Post" , [" TODO "])])
1.40 - 11 prls
1.41 + 11 where_rls
1.42 12 NONE
1.43 13 [["SignalProcessing","Z_Transform","Inverse"]]);
1.44 14 *}
1.45 @@ -1163,9 +1163,9 @@
1.46 % because applied terms may be from 'subthy' as well as from super;
1.47 % thus we take 'maxthy'; see match_ags !*)
1.48 % cas : term option,(*'CAS-command'*)
1.49 -% prls : rls, (* for preds in where_*)
1.50 +% where_rls : rls, (* for preds in where_*)
1.51 % where_: term list, (* where - predicates*)
1.52 -% ppc : pat list,
1.53 +% model : pat list,
1.54 % (*this is the model-pattern;
1.55 % it contains "#Given","#Where","#Find","#Relate"-patterns
1.56 % for constraints on identifiers see "fun copy_name"*)
1.57 @@ -1225,8 +1225,8 @@
1.58 07 [ ("#Given", ["filterExpression X_eq", "domain D"]),
1.59 08 ("#Pre" , ["(rhs X_eq) is_continuous_in D"]),
1.60 09 ("#Find" , ["stepResponse n_eq"]),
1.61 - 10 rew_ord erls
1.62 - 11 srls prls nrls
1.63 + 10 rew_ord asm_rls
1.64 + 11 prog_rls where_rls rew_rls
1.65 12 errpats
1.66 13 program);
1.67 14 *}
1.68 @@ -1244,8 +1244,8 @@
1.69 is not started.
1.70
1.71 \item[10..11] all concern rewriting (the respective data are defined elsewhere): \textit{rew\_ord} is the rewrite order~\cite{nipk:rew-all-that} in case
1.72 -\textit{program} contains a \textit{Rewrite} tactic; and in case the respective rule is a conditional rewrite-rule, \textit{erls} features evaluating the conditions. The rule-sets
1.73 -\textit{srls, prls, nrls} feature evaluating (a) the ML-functions in the program (e.g.
1.74 +\textit{program} contains a \textit{Rewrite} tactic; and in case the respective rule is a conditional rewrite-rule, \textit{asm_rls} features evaluating the conditions. The rule-sets
1.75 +\textit{prog_rls, where_rls, rew_rls} feature evaluating (a) the ML-functions in the program (e.g.
1.76 \textit{lhs, argument\_in, rhs} in the program on p.\pageref{s:impl}, (b) the pre-condition analogous to the specification in line 11 on p.\pageref{exp-spec}
1.77 and (c) is required for the derivation-machinery checking user-input formulas.
1.78
1.79 @@ -1466,7 +1466,7 @@
1.80 \noindent The entry is perfect. So what is the reason~? Ah, probably there
1.81 is something messed up with the many rule-sets in the method, see \S\ref{meth} ---
1.82 right, the function \texttt{argument\_in} is not contained in the respective
1.83 -rule-set \textit{srls} \dots this just as an example of the intricacies in
1.84 +rule-set \textit{prog_rls} \dots this just as an example of the intricacies in
1.85 debugging a program in the present state of the prototype.
1.86
1.87 \subsection{Implementation in Isabelle/{\isac}}\label{flow-impl}
1.88 @@ -2128,8 +2128,8 @@
1.89 % LocalWords: TP IST SPSC Telematics Dialogues dialogue HOL bool nat Hindley
1.90 % LocalWords: Milner tt Subproblem Formulae ruleset generalisation initialised
1.91 % LocalWords: axiomatization LCF Simplifiers simplifiers Isar rew Thm Calc SML
1.92 -% LocalWords: recognised hoc Trueprop redexes Unsynchronized pre rhs ord erls
1.93 -% LocalWords: srls prls nrls lhs errpats InverseZTransform SubProblem IDE IDEs
1.94 +% LocalWords: recognised hoc Trueprop redexes Unsynchronized where_ rhs ord asm_rls
1.95 +% LocalWords: prog_rls where_rls rew_rls lhs errpats InverseZTransform SubProblem IDE IDEs
1.96 % LocalWords: univariate jEdit rls RealDef calclist familiarisation ons pos eq
1.97 % LocalWords: mout ctree SignalProcessing frac ZZ Postcond Atools wiki SML's
1.98 % LocalWords: mechanisation multi