1.1 --- a/doc-src/isac/jrocnik/bakkarbeit_jrocnik.tex Mon Feb 13 17:40:30 2012 +0100
1.2 +++ b/doc-src/isac/jrocnik/bakkarbeit_jrocnik.tex Tue Feb 14 22:55:03 2012 +0100
1.3 @@ -429,8 +429,12 @@
1.4
1.5 \part{Implementation}
1.6
1.7 +
1.8 \input{./preambleForGeneratedDocuments.tex}
1.9 +
1.10 \HRule
1.11 +
1.12 +\setcounter{section}{0}
1.13 \input{../../../test/Tools/isac/ADDTESTS/course/SignalProcess/document/Build_Inverse_Z_Transform}
1.14
1.15 \clearpage
1.16 @@ -498,7 +502,7 @@
1.17 \end{longtable}
1.18 \end{footnotesize}
1.19
1.20 -\section{Calculations}
1.21 +\section{Calculations\label{app:calc}}
1.22 \input{calulations}
1.23 \end{document}
1.24
2.1 --- a/doc-src/isac/jrocnik/calulations.tex Mon Feb 13 17:40:30 2012 +0100
2.2 +++ b/doc-src/isac/jrocnik/calulations.tex Tue Feb 14 22:55:03 2012 +0100
2.3 @@ -21,8 +21,8 @@
2.4 %------------------------------------------------------------------------------
2.5 %FOURIER
2.6
2.7 -\section*{Fourier Transformation}
2.8 -\subsection*{Problem\endnote{Problem submitted by Bernhard Geiger. Originally fragment of the exam to \emph{Signaltransformationen VO} from 04.03.2011. Translated from German.}}
2.9 +\subsection{Fourier Transformation}
2.10 +\subsubsection*{Problem\endnote{Problem submitted by Bernhard Geiger. Originally fragment of the exam to \emph{Signaltransformationen VO} from 04.03.2011. Translated from German.}}
2.11 \textbf{(a)} Determine the fourier transform for the given rectangular impulse:
2.12
2.13 \begin{center}
2.14 @@ -45,7 +45,7 @@
2.15 \right.$
2.16 \end{center}
2.17
2.18 -\subsection*{Solution}
2.19 +\subsubsection{Solution}
2.20 \textbf{(a)}
2.21 \onehalfspace{
2.22 \begin{tabbing}
2.23 @@ -103,8 +103,8 @@
2.24 %------------------------------------------------------------------------------
2.25 %CONVOLUTION
2.26
2.27 -\section*{Convolution}
2.28 -\subsection*{Problem\endnote{Problem submitted by Bernhard Geiger. Originally part of the SPSC Problem Class 2, Summer term 2008}}
2.29 +\subsection{Convolution}
2.30 +\subsubsection*{Problem\endnote{Problem submitted by Bernhard Geiger. Originally part of the SPSC Problem Class 2, Summer term 2008}}
2.31 Consider the two discrete-time, linear and time-invariant (LTI) systems with the following impulse response:
2.32
2.33 \begin{center}
2.34 @@ -113,7 +113,7 @@
2.35 \end{center}
2.36
2.37 The two systems are cascaded seriell. Derive the impulse respinse of the overall system $h_c[n]$.
2.38 -\subsection*{Solution}
2.39 +\subsubsection*{Solution}
2.40
2.41 \doublespace{
2.42 \begin{tabbing}
2.43 @@ -152,15 +152,15 @@
2.44 %------------------------------------------------------------------------------
2.45 %Z-Transformation
2.46
2.47 -\section*{$\cal Z$-Transformation}
2.48 -\subsection*{Problem\endnote{Problem submitted by Bernhard Geiger. Originally part of the signal processing problem class 5, summer term 2008.}}
2.49 +\subsection{$\cal Z$-Transformation\label{sec:calc:ztrans}}
2.50 +\subsubsection*{Problem\endnote{Problem submitted by Bernhard Geiger. Originally part of the signal processing problem class 5, summer term 2008.}}
2.51 Determine the inverse $\cal{z}$ transform of the following expression. Hint: applay the partial fraction expansion.
2.52
2.53 \begin{center}
2.54 $X(z)=\frac{3}{z-\frac{1}{4}-\frac{1}{8}z^{-1}},\ \ x[n]$ is absolute summable
2.55 \end{center}
2.56
2.57 -\subsection*{Solution}
2.58 +\subsubsection*{Solution}
2.59 \onehalfspace{
2.60 \begin{tabbing}
2.61 000\=\kill
3.1 --- a/doc-src/isac/jrocnik/preambleForGeneratedDocuments.tex Mon Feb 13 17:40:30 2012 +0100
3.2 +++ b/doc-src/isac/jrocnik/preambleForGeneratedDocuments.tex Tue Feb 14 22:55:03 2012 +0100
3.3 @@ -1,4 +1,4 @@
3.4 -\section{Preamble}
3.5 +\section*{Preamble}
3.6 This document shows the main structure of an {\sisac{}} theory. All of the following part is automatically generated out of an {\sisac{}}-theory file (.thy - extension). In this case the file is called \texttt{Build\_Inverse\_Z\_Transform} it can be found in the {\sisac{}} directory: \texttt{test/Tools/isac/ADDTESTS/course/}. {\sisac{}} provides inbuild tools for translating theories into latex documents. To set up such an envoriemt a file called \texttt{isacmakefile} is needed. Further information about this automatic generation can be found in \cite{wenzel2011system}.
3.7 \par The following theory can be modified and used as a guiedline for implementing new applications. Everything found here is just a snapshot of the work with \today.
3.8 \begin{center}TODO\end{center}
3.9 \ No newline at end of file
4.1 --- a/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy Mon Feb 13 17:40:30 2012 +0100
4.2 +++ b/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy Tue Feb 14 22:55:03 2012 +0100
4.3 @@ -9,43 +9,51 @@
4.4
4.5 begin
4.6
4.7 -text{* We stepwise build \texttt{Inverse\_Z\_Transform.thy} as an exercise.
4.8 - Because subsection "Stepwise Check the Program" requires
4.9 - \texttt{Inverse\_Z\_Transform.thy} as a subtheory of Isac.thy, the setup has been changed
4.10 - from "theory Inverse_Z_Transform imports Isac begin.." to the above.
4.11 +text{* We stepwise build \ttfamily Inverse\_Z\_Transform.thy \normalfont as an
4.12 + exercise. Because subsection~\ref{sec:stepcheck} requires
4.13 + \ttfamily Inverse\_Z\_Transform.thy \normalfont as a subtheory of \ttfamily
4.14 + Isac.thy\normalfont, the setup has been changed from \ttfamily theory
4.15 + Inverse\_Z\_Transform imports Isac \normalfont to the above one.
4.16 + \par \noindent
4.17 + \begin{center}
4.18 + \textbf{ATTENTION WITH NAMES OF IDENTIFIERS WHEN GOING INTO INTERNALS}
4.19 + \end{center}
4.20 + Here in this theory there are the internal names twice, for instance we have
4.21 + \ttfamily (Thm.derivation\_name @{thm rule1} =
4.22 + "Build\_Inverse\_Z\_Transform.rule1") = true; \normalfont
4.23 + but actually in us will be \ttfamily Inverse\_Z\_Transform.rule1 \normalfont
4.24 +*}
4.25
4.26 - ATTENTION WITH NAMES OF IDENTIFIERS WHEN GOING INTO INTERNALS:
4.27 - Here in this theory there are the internal names twice, for instance we have
4.28 - (Thm.derivation_name @{thm rule1} = "Build_Inverse_Z_Transform.rule1") = true;
4.29 - but actually in us will be "Inverse_Z_Transform.rule1"
4.30 -*}
4.31 +section {*Trials towards the Z-Transform\label{sec:trials}*}
4.32 +
4.33 ML {*val thy = @{theory Isac};*}
4.34
4.35 -
4.36 -section {*trials towards Z transform *}
4.37 -text{*===============================*}
4.38 -subsection {*terms*}
4.39 +subsection {*Notations and Terms*}
4.40 +text{*\noindent Try which notations we are able to use.*}
4.41 ML {*
4.42 -@{term "1 < || z ||"};
4.43 -@{term "z / (z - 1)"};
4.44 -@{term "-u -n - 1"};
4.45 -@{term "-u [-n - 1]"}; (*[ ] denotes lists !!!*)
4.46 -@{term "z /(z - 1) = -u [-n - 1]"};Isac
4.47 -@{term "1 < || z || ==> z / (z - 1) = -u [-n - 1]"};
4.48 -term2str @{term "1 < || z || ==> z / (z - 1) = -u [-n - 1]"};
4.49 + @{term "1 < || z ||"};
4.50 + @{term "z / (z - 1)"};
4.51 + @{term "-u -n - 1"};
4.52 + @{term "-u [-n - 1]"}; (*[ ] denotes lists !!!*)
4.53 + @{term "z /(z - 1) = -u [-n - 1]"};Isac
4.54 + @{term "1 < || z || ==> z / (z - 1) = -u [-n - 1]"};
4.55 + term2str @{term "1 < || z || ==> z / (z - 1) = -u [-n - 1]"};
4.56 *}
4.57 +text{*\noindent Try which symbols we are able to use and how we generate them.*}
4.58 ML {*
4.59 -(*alpha --> "</alpha>" *)
4.60 -@{term "\<alpha> "};
4.61 -@{term "\<delta> "};
4.62 -@{term "\<phi> "};
4.63 -@{term "\<rho> "};
4.64 -term2str @{term "\<rho> "};
4.65 + (*alpha --> "</alpha>" *)
4.66 + @{term "\<alpha> "};
4.67 + @{term "\<delta> "};
4.68 + @{term "\<phi> "};
4.69 + @{term "\<rho> "};
4.70 + term2str @{term "\<rho> "};
4.71 *}
4.72
4.73 -subsection {*rules*}
4.74 -(*axiomatization "z / (z - 1) = -u [-n - 1]" Illegal variable name: "z / (z - 1) = -u [-n - 1]" *)
4.75 -(*definition "z / (z - 1) = -u [-n - 1]" Bad head of lhs: existing constant "op /"*)
4.76 +subsection {*Rules*}
4.77 +(*axiomatization "z / (z - 1) = -u [-n - 1]"
4.78 + Illegal variable name: "z / (z - 1) = -u [-n - 1]" *)
4.79 +(*definition "z / (z - 1) = -u [-n - 1]"
4.80 + Bad head of lhs: existing constant "op /"*)
4.81 axiomatization where
4.82 rule1: "1 = \<delta>[n]" and
4.83 rule2: "|| z || > 1 ==> z / (z - 1) = u [n]" and
4.84 @@ -53,122 +61,167 @@
4.85 rule4: "|| z || > || \<alpha> || ==> z / (z - \<alpha>) = \<alpha>^^^n * u [n]" and
4.86 rule5: "|| z || < || \<alpha> || ==> z / (z - \<alpha>) = -(\<alpha>^^^n) * u [-n - 1]" and
4.87 rule6: "|| z || > 1 ==> z/(z - 1)^^^2 = n * u [n]"
4.88 +
4.89 +text{*\noindent Check the rules for their correct notation.
4.90 + (See the machine output.)*}
4.91 ML {*
4.92 -@{thm rule1};
4.93 -@{thm rule2};
4.94 -@{thm rule3};
4.95 -@{thm rule4};
4.96 + @{thm rule1};
4.97 + @{thm rule2};
4.98 + @{thm rule3};
4.99 + @{thm rule4};
4.100 *}
4.101
4.102 -subsection {*apply rules*}
4.103 +subsection {*Apply Rules*}
4.104 +text{*\noindent We try to apply the rules to a given expression.*}
4.105 +
4.106 ML {*
4.107 -val inverse_Z = append_rls "inverse_Z" e_rls
4.108 - [ Thm ("rule3",num_str @{thm rule3}),
4.109 - Thm ("rule4",num_str @{thm rule4}),
4.110 - Thm ("rule1",num_str @{thm rule1})
4.111 - ];
4.112 + val inverse_Z = append_rls "inverse_Z" e_rls
4.113 + [ Thm ("rule3",num_str @{thm rule3}),
4.114 + Thm ("rule4",num_str @{thm rule4}),
4.115 + Thm ("rule1",num_str @{thm rule1})
4.116 + ];
4.117
4.118 -val t = str2term "z / (z - 1) + z / (z - \<alpha>) + 1";
4.119 -val SOME (t', asm) = rewrite_set_ thy true inverse_Z t;
4.120 -term2str t' = "z / (z - ?\<delta> [?n]) + z / (z - \<alpha>) + ?\<delta> [?n]"; (*attention rule1 !!!*)
4.121 -*}
4.122 -ML {*
4.123 -val (thy, ro, er) = (@{theory Isac}, tless_true, eval_rls);
4.124 -*}
4.125 -ML {*
4.126 -val SOME (t, asm1) = rewrite_ thy ro er true (num_str @{thm rule3}) t;
4.127 -term2str t = "- ?u [- ?n - 1] + z / (z - \<alpha>) + 1"; (*- real *)
4.128 -term2str t;*}
4.129 -ML {*
4.130 -val SOME (t, asm2) = rewrite_ thy ro er true (num_str @{thm rule4}) t;
4.131 -term2str t = "- ?u [- ?n - 1] + \<alpha> ^^^ ?n * ?u [?n] + 1"; (*- real *)
4.132 -term2str t;
4.133 -*}
4.134 -ML {*
4.135 -val SOME (t, asm3) = rewrite_ thy ro er true (num_str @{thm rule1}) t;
4.136 -term2str t = "- ?u [- ?n - 1] + \<alpha> ^^^ ?n * ?u [?n] + ?\<delta> [?n]"; (*- real *)
4.137 -term2str t;
4.138 -*}
4.139 -ML {*
4.140 -terms2str (asm1 @ asm2 @ asm3);
4.141 + val t = str2term "z / (z - 1) + z / (z - \<alpha>) + 1";
4.142 + val SOME (t', asm) = rewrite_set_ thy true inverse_Z t;
4.143 + term2str t' = "z / (z - ?\<delta> [?n]) + z / (z - \<alpha>) + ?\<delta> [?n]";
4.144 + (*
4.145 + * Attention rule1 is applied before the expression is
4.146 + * checked for rule4 which would be correct!!!
4.147 + *)
4.148 *}
4.149
4.150 -section {*Prepare steps for CTP-based programming language*}
4.151 -text{*TODO insert Calculation (Referenz?!)
4.152 +ML {* val (thy, ro, er) = (@{theory Isac}, tless_true, eval_rls); *}
4.153 +ML {*
4.154 + val SOME (t, asm1) =
4.155 + rewrite_ thy ro er true (num_str @{thm rule3}) t;
4.156 + term2str t = "- ?u [- ?n - 1] + z / (z - \<alpha>) + 1";
4.157 + (*- real *)
4.158 + term2str t;
4.159
4.160 -The goal... realized in sections below, in Sect.\ref{spec-meth} and Sect.\ref{prog-steps}
4.161 + val SOME (t, asm2) =
4.162 + rewrite_ thy ro er true (num_str @{thm rule4}) t;
4.163 + term2str t = "- ?u [- ?n - 1] + \<alpha> ^^^ ?n * ?u [?n] + 1";
4.164 + (*- real *)
4.165 + term2str t;
4.166
4.167 -the reader is advised to jump between the subsequent subsections and the respective steps in Sect.\ref{prog-steps}
4.168 + val SOME (t, asm3) =
4.169 + rewrite_ thy ro er true (num_str @{thm rule1}) t;
4.170 + term2str t = "- ?u [- ?n - 1] + \<alpha> ^^^ ?n * ?u [?n] + ?\<delta> [?n]";
4.171 + (*- real *)
4.172 + term2str t;
4.173 +*}
4.174 +ML {* terms2str (asm1 @ asm2 @ asm3); *}
4.175
4.176 -*}
4.177 -subsection {*prepare expression \label{prep-expr}*}
4.178 -ML {*
4.179 -val ctxt = ProofContext.init_global @{theory Isac};
4.180 -val ctxt = declare_constraints' [@{term "z::real"}] ctxt;
4.181 -
4.182 -val SOME fun1 = parseNEW ctxt "X z = 3 / (z - 1/4 + -1/8 * z ^^^ -1)"; term2str fun1;
4.183 -val SOME fun1' = parseNEW ctxt "X z = 3 / (z - 1/4 + -1/8 * (1/z))"; term2str fun1';
4.184 +section{*Prepare Steps for CTP-based programming Language\label{sec:prepstep}*}
4.185 +text{*
4.186 + \par \noindent The following sections are challanging with the CTP-based
4.187 + possibilities of building the programm. The goal is realized in
4.188 + Section~\ref{spec-meth} and Section~\ref{prog-steps}.
4.189 + \par The reader is advised to jump between the subsequent subsections and
4.190 + the respective steps in Section~\ref{prog-steps}. By comparing
4.191 + Section~\ref{sec:calc:ztrans} the calculation can be comprehended step
4.192 + by step.
4.193 *}
4.194
4.195 -subsubsection {*multply with z*}
4.196 +subsection {*Prepare Expression\label{prep-expr}*}
4.197 +ML {*
4.198 + val ctxt = ProofContext.init_global @{theory Isac};
4.199 + val ctxt = declare_constraints' [@{term "z::real"}] ctxt;
4.200 +
4.201 + val SOME fun1 =
4.202 + parseNEW ctxt "X z = 3 / (z - 1/4 + -1/8 * z ^^^ -1)"; term2str fun1;
4.203 + val SOME fun1' =
4.204 + parseNEW ctxt "X z = 3 / (z - 1/4 + -1/8 * (1/z))"; term2str fun1';
4.205 +*}
4.206 +
4.207 +subsubsection {*Prepare Numerator and Denominator*}
4.208 +text{*\noindent The partial fraction decomposion is only possible ig we
4.209 + get the bound variable out of the numerator. Therefor we divide
4.210 + the expression by $z$. Follow up the Calculation at
4.211 + Section~\ref{sec:calc:ztrans} line number 02.*}
4.212 +
4.213 axiomatization where
4.214 ruleZY: "(X z = a / b) = (X' z = a / (z * b))"
4.215
4.216 ML {*
4.217 -val (thy, ro, er) = (@{theory Isac}, tless_true, eval_rls);
4.218 -val SOME (fun2, asm1) = rewrite_ thy ro er true @{thm ruleZY} fun1; term2str fun2;
4.219 -val SOME (fun2', asm1) = rewrite_ thy ro er true @{thm ruleZY} fun1'; term2str fun2';
4.220 + val (thy, ro, er) = (@{theory Isac}, tless_true, eval_rls);
4.221 + val SOME (fun2, asm1) =
4.222 + rewrite_ thy ro er true @{thm ruleZY} fun1; term2str fun2;
4.223 + val SOME (fun2', asm1) =
4.224 + rewrite_ thy ro er true @{thm ruleZY} fun1'; term2str fun2';
4.225
4.226 -val SOME (fun3,_) = rewrite_set_ @{theory Isac} false norm_Rational fun2;
4.227 -term2str fun3; (*fails on x^^^(-1) TODO*)
4.228 -val SOME (fun3',_) = rewrite_set_ @{theory Isac} false norm_Rational fun2';
4.229 -term2str fun3'; (*OK*)
4.230 + val SOME (fun3,_) =
4.231 + rewrite_set_ @{theory Isac} false norm_Rational fun2;
4.232 + term2str fun3;
4.233 + (*
4.234 + * Fails on x^^^(-1)
4.235 + * We solve this problem by using 1/x as a workaround.
4.236 + *)
4.237 + val SOME (fun3',_) =
4.238 + rewrite_set_ @{theory Isac} false norm_Rational fun2';
4.239 + term2str fun3';
4.240 + (*
4.241 + * OK - workaround!
4.242 + *)
4.243 *}
4.244
4.245 -subsubsection {*get argument of X': z is the variable the equation is solved for*}
4.246 -text{*grep... Atools.thy, Tools.thy contain general utilities: eval_argument_in, eval_rhs, eval_lhs,...
4.247 -
4.248 -grep -r "fun eva_" ... shows all functions witch can be used in a script.
4.249 -lookup this files how to build and handle such functions.
4.250 -
4.251 -the next section shows how to introduce such a function.
4.252 +subsubsection {*Get the Argument of the Expression X'*}
4.253 +text{*\noindent We use \texttt{grep} for finding possibilities how we can
4.254 + extract the bound variable in the expression. \ttfamily Atools.thy,
4.255 + Tools.thy \normalfont contain general utilities: \ttfamily
4.256 + eval\_argument\_in, eval\_rhs, eval\_lhs,\ldots \normalfont
4.257 + \ttfamily grep -r "fun eva\_" * \normalfont shows all functions
4.258 + witch can be used in a script. Lookup this files how to build
4.259 + and handle such functions.
4.260 + \par The next section shows how to introduce such a function.
4.261 *}
4.262
4.263 -subsubsection {*Decompose given term into lhs = rhs*}
4.264 +subsubsection{*Decompose the Given Term Into lhs and rhs\footnote{Note:
4.265 + lhs means \em Left Hand Side \normalfont and rhs means
4.266 + \em Right Hand Side \normalfont and indicates the left or
4.267 + the right part of an equation.}*}
4.268 ML {*
4.269 val (_, expr) = HOLogic.dest_eq fun3'; term2str expr;
4.270 - val (_, denom) = HOLogic.dest_bin "Rings.inverse_class.divide" (type_of expr) expr;
4.271 + val (_, denom) =
4.272 + HOLogic.dest_bin "Rings.inverse_class.divide" (type_of expr) expr;
4.273 term2str denom = "-1 + -2 * z + 8 * z ^^^ 2";
4.274 *}
4.275 -text {*we have rhs in the Script language, but we need a function
4.276 - which gets the denominator of a fraction*}
4.277
4.278 +text{*\noindent We have rhs in the Script language, but we need a function
4.279 + which gets the denominator of a fraction.*}
4.280
4.281 -subsubsection {*get the denominator and numerator out of a fraction*}
4.282 -text {*get denominator should become a constant for the isabelle parser: *}
4.283 +subsubsection{*Get the Denominator and Numerator out of a Fraction*}
4.284 +text{*\noindent The selv written functions in e.g. \texttt{get\_denominator}
4.285 + should become a constant for the isabelle parser:*}
4.286
4.287 consts
4.288 get_denominator :: "real => real"
4.289 get_numerator :: "real => real"
4.290
4.291 -text {* With the above definition we run into problems with parsing the Script InverseZTransform:
4.292 - This leads to "ambiguous parse trees" and we avoid this by shifting the definition
4.293 - to Rational.thy and re-building Isac.
4.294 - ATTENTION: from now on Build_Inverse_Z_Transform mimics a build from scratch;
4.295 - it only works due to re-building Isac several times (indicated explicityl).
4.296 +text {*\noindent With the above definition we run into problems when we parse
4.297 + the Script \texttt{InverseZTransform}. This leads to \em ambiguous
4.298 + parse trees. \normalfont We avoid this by moving the definition
4.299 + to \ttfamily Rational.thy \normalfont and re-building Isac.
4.300 + \par \noindent ATTENTION: From now on \ttfamily
4.301 + Build\_Inverse\_Z\_Transform \normalfont mimics a build from scratch;
4.302 + it only works due to re-building Isac several times (indicated
4.303 + explicityl).
4.304 *}
4.305
4.306 ML {*
4.307 -(*("get_denominator", ("Rational.get_denominator", eval_get_denominator ""))*)
4.308 +(*
4.309 + *("get_denominator",
4.310 + * ("Rational.get_denominator", eval_get_denominator ""))
4.311 + *)
4.312 fun eval_get_denominator (thmid:string) _
4.313 (t as Const ("Rational.get_denominator", _) $
4.314 (Const ("Rings.inverse_class.divide", _) $ num $
4.315 denom)) thy =
4.316 SOME (mk_thmid thmid ""
4.317 - (Print_Mode.setmp [] (Syntax.string_of_term (thy2ctxt thy)) denom) "",
4.318 + (Print_Mode.setmp []
4.319 + (Syntax.string_of_term (thy2ctxt thy)) denom) "",
4.320 Trueprop $ (mk_equality (t, denom)))
4.321 | eval_get_denominator _ _ _ _ = NONE;
4.322 -
4.323 *}
4.324 text {* tests of eval_get_denominator see test/Knowledge/rational.sml*}
4.325
4.326 @@ -888,7 +941,7 @@
4.327 atomty sc;
4.328 *}
4.329
4.330 -subsubsection {*Stepwise check the program*}
4.331 +subsubsection {*Stepwise check the program\label{sec:stepcheck}*}
4.332 ML {*
4.333 trace_rewrite := false;
4.334 trace_script := false; print_depth 9;
5.1 --- a/test/Tools/isac/ADDTESTS/course/SignalProcess/document/Build_Inverse_Z_Transform.tex Mon Feb 13 17:40:30 2012 +0100
5.2 +++ b/test/Tools/isac/ADDTESTS/course/SignalProcess/document/Build_Inverse_Z_Transform.tex Tue Feb 14 22:55:03 2012 +0100
5.3 @@ -21,18 +21,26 @@
5.4 \endisadelimtheory
5.5 %
5.6 \begin{isamarkuptext}%
5.7 -We stepwise build \texttt{Inverse\_Z\_Transform.thy} as an exercise.
5.8 - Because subsection "Stepwise Check the Program" requires
5.9 - \texttt{Inverse\_Z\_Transform.thy} as a subtheory of Isac.thy, the setup has been changed
5.10 - from "theory Inverse_Z_Transform imports Isac begin.." to the above.
5.11 -
5.12 - ATTENTION WITH NAMES OF IDENTIFIERS WHEN GOING INTO INTERNALS:
5.13 +We stepwise build \ttfamily Inverse\_Z\_Transform.thy \normalfont as an
5.14 + exercise. Because subsection~\ref{sec:stepcheck} requires
5.15 + \ttfamily Inverse\_Z\_Transform.thy \normalfont as a subtheory of \ttfamily
5.16 + Isac.thy\normalfont, the setup has been changed from \ttfamily theory
5.17 + Inverse\_Z\_Transform imports Isac \normalfont to the above one.
5.18 + \par \noindent
5.19 + \begin{center}
5.20 + \textbf{ATTENTION WITH NAMES OF IDENTIFIERS WHEN GOING INTO INTERNALS}
5.21 + \end{center}
5.22 Here in this theory there are the internal names twice, for instance we have
5.23 - (Thm.derivation_name \isa{rule{\isadigit{1}}} = "Build_Inverse_Z_Transform.rule1") = true;
5.24 - but actually in us will be "Inverse_Z_Transform.rule1"%
5.25 + \ttfamily (Thm.derivation\_name \isa{rule{\isadigit{1}}} = "Build\_Inverse\_Z\_Transform.rule1") = true;
5.26 + \normalfont
5.27 + but actually in us will be \ttfamily Inverse\_Z\_Transform.rule1 \normalfont%
5.28 \end{isamarkuptext}%
5.29 \isamarkuptrue%
5.30 %
5.31 +\isamarkupsection{Trials towards the Z-Transform\label{sec:trials}%
5.32 +}
5.33 +\isamarkuptrue%
5.34 +%
5.35 \isadelimML
5.36 %
5.37 \endisadelimML
5.38 @@ -51,19 +59,15 @@
5.39 %
5.40 \endisadelimML
5.41 %
5.42 -\isamarkupsection{trials towards Z transform%
5.43 +\isamarkupsubsection{Notations and Terms%
5.44 }
5.45 \isamarkuptrue%
5.46 %
5.47 \begin{isamarkuptext}%
5.48 -===============================%
5.49 +\noindent Try which notations we are able to use.%
5.50 \end{isamarkuptext}%
5.51 \isamarkuptrue%
5.52 %
5.53 -\isamarkupsubsection{terms%
5.54 -}
5.55 -\isamarkuptrue%
5.56 -%
5.57 \isadelimML
5.58 %
5.59 \endisadelimML
5.60 @@ -71,66 +75,83 @@
5.61 \isatagML
5.62 \isacommand{ML}\isamarkupfalse%
5.63 \ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
5.64 -%
5.65 +\ \ %
5.66 \isaantiq
5.67 term\ {\isaliteral{22}{\isachardoublequote}}{\isadigit{1}}\ {\isaliteral{3C}{\isacharless}}\ {\isaliteral{7C}{\isacharbar}}{\isaliteral{7C}{\isacharbar}}\ z\ {\isaliteral{7C}{\isacharbar}}{\isaliteral{7C}{\isacharbar}}{\isaliteral{22}{\isachardoublequote}}{}%
5.68 \endisaantiq
5.69 {\isaliteral{3B}{\isacharsemicolon}}\isanewline
5.70 -%
5.71 +\ \ %
5.72 \isaantiq
5.73 term\ {\isaliteral{22}{\isachardoublequote}}z\ {\isaliteral{2F}{\isacharslash}}\ {\isaliteral{28}{\isacharparenleft}}z\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{1}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}{}%
5.74 \endisaantiq
5.75 {\isaliteral{3B}{\isacharsemicolon}}\isanewline
5.76 -%
5.77 +\ \ %
5.78 \isaantiq
5.79 term\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{2D}{\isacharminus}}u\ {\isaliteral{2D}{\isacharminus}}n\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{1}}{\isaliteral{22}{\isachardoublequote}}{}%
5.80 \endisaantiq
5.81 {\isaliteral{3B}{\isacharsemicolon}}\isanewline
5.82 -%
5.83 +\ \ %
5.84 \isaantiq
5.85 term\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{2D}{\isacharminus}}u\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{2D}{\isacharminus}}n\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{1}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequote}}{}%
5.86 \endisaantiq
5.87 {\isaliteral{3B}{\isacharsemicolon}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{5B}{\isacharbrackleft}}\ {\isaliteral{5D}{\isacharbrackright}}\ denotes\ lists\ {\isaliteral{21}{\isacharbang}}{\isaliteral{21}{\isacharbang}}{\isaliteral{21}{\isacharbang}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline
5.88 -%
5.89 +\ \ %
5.90 \isaantiq
5.91 term\ {\isaliteral{22}{\isachardoublequote}}z\ {\isaliteral{2F}{\isacharslash}}{\isaliteral{28}{\isacharparenleft}}z\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{1}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{2D}{\isacharminus}}u\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{2D}{\isacharminus}}n\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{1}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequote}}{}%
5.92 \endisaantiq
5.93 {\isaliteral{3B}{\isacharsemicolon}}Isac\isanewline
5.94 -%
5.95 +\ \ %
5.96 \isaantiq
5.97 term\ {\isaliteral{22}{\isachardoublequote}}{\isadigit{1}}\ {\isaliteral{3C}{\isacharless}}\ {\isaliteral{7C}{\isacharbar}}{\isaliteral{7C}{\isacharbar}}\ z\ {\isaliteral{7C}{\isacharbar}}{\isaliteral{7C}{\isacharbar}}\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\ z\ {\isaliteral{2F}{\isacharslash}}\ {\isaliteral{28}{\isacharparenleft}}z\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{1}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{2D}{\isacharminus}}u\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{2D}{\isacharminus}}n\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{1}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequote}}{}%
5.98 \endisaantiq
5.99 {\isaliteral{3B}{\isacharsemicolon}}\isanewline
5.100 -term{\isadigit{2}}str\ %
5.101 +\ \ term{\isadigit{2}}str\ %
5.102 \isaantiq
5.103 term\ {\isaliteral{22}{\isachardoublequote}}{\isadigit{1}}\ {\isaliteral{3C}{\isacharless}}\ {\isaliteral{7C}{\isacharbar}}{\isaliteral{7C}{\isacharbar}}\ z\ {\isaliteral{7C}{\isacharbar}}{\isaliteral{7C}{\isacharbar}}\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\ z\ {\isaliteral{2F}{\isacharslash}}\ {\isaliteral{28}{\isacharparenleft}}z\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{1}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{2D}{\isacharminus}}u\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{2D}{\isacharminus}}n\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{1}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequote}}{}%
5.104 \endisaantiq
5.105 {\isaliteral{3B}{\isacharsemicolon}}\isanewline
5.106 -{\isaliteral{2A7D}{\isacharverbatimclose}}\isanewline
5.107 +{\isaliteral{2A7D}{\isacharverbatimclose}}%
5.108 +\endisatagML
5.109 +{\isafoldML}%
5.110 +%
5.111 +\isadelimML
5.112 +%
5.113 +\endisadelimML
5.114 +%
5.115 +\begin{isamarkuptext}%
5.116 +\noindent Try which symbols we are able to use and how we generate them.%
5.117 +\end{isamarkuptext}%
5.118 +\isamarkuptrue%
5.119 +%
5.120 +\isadelimML
5.121 +%
5.122 +\endisadelimML
5.123 +%
5.124 +\isatagML
5.125 \isacommand{ML}\isamarkupfalse%
5.126 \ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
5.127 -{\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}alpha\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ \ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{3C}{\isacharless}}{\isaliteral{2F}{\isacharslash}}alpha{\isaliteral{3E}{\isachargreater}}{\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline
5.128 -%
5.129 +\ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}alpha\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ \ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{3C}{\isacharless}}{\isaliteral{2F}{\isacharslash}}alpha{\isaliteral{3E}{\isachargreater}}{\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline
5.130 +\ \ %
5.131 \isaantiq
5.132 term\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}\ {\isaliteral{22}{\isachardoublequote}}{}%
5.133 \endisaantiq
5.134 {\isaliteral{3B}{\isacharsemicolon}}\isanewline
5.135 -%
5.136 +\ \ %
5.137 \isaantiq
5.138 term\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C64656C74613E}{\isasymdelta}}\ {\isaliteral{22}{\isachardoublequote}}{}%
5.139 \endisaantiq
5.140 {\isaliteral{3B}{\isacharsemicolon}}\isanewline
5.141 -%
5.142 +\ \ %
5.143 \isaantiq
5.144 term\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C7068693E}{\isasymphi}}\ {\isaliteral{22}{\isachardoublequote}}{}%
5.145 \endisaantiq
5.146 {\isaliteral{3B}{\isacharsemicolon}}\isanewline
5.147 -%
5.148 +\ \ %
5.149 \isaantiq
5.150 term\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C72686F3E}{\isasymrho}}\ {\isaliteral{22}{\isachardoublequote}}{}%
5.151 \endisaantiq
5.152 {\isaliteral{3B}{\isacharsemicolon}}\isanewline
5.153 -term{\isadigit{2}}str\ %
5.154 +\ \ term{\isadigit{2}}str\ %
5.155 \isaantiq
5.156 term\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C72686F3E}{\isasymrho}}\ {\isaliteral{22}{\isachardoublequote}}{}%
5.157 \endisaantiq
5.158 @@ -143,7 +164,7 @@
5.159 %
5.160 \endisadelimML
5.161 %
5.162 -\isamarkupsubsection{rules%
5.163 +\isamarkupsubsection{Rules%
5.164 }
5.165 \isamarkuptrue%
5.166 \isacommand{axiomatization}\isamarkupfalse%
5.167 @@ -153,7 +174,12 @@
5.168 \ \ rule{\isadigit{3}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{7C}{\isacharbar}}{\isaliteral{7C}{\isacharbar}}\ z\ {\isaliteral{7C}{\isacharbar}}{\isaliteral{7C}{\isacharbar}}\ {\isaliteral{3C}{\isacharless}}\ {\isadigit{1}}\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\ z\ {\isaliteral{2F}{\isacharslash}}\ {\isaliteral{28}{\isacharparenleft}}z\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{1}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{2D}{\isacharminus}}u\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{2D}{\isacharminus}}n\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{1}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{and}\ \isanewline
5.169 \ \ rule{\isadigit{4}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{7C}{\isacharbar}}{\isaliteral{7C}{\isacharbar}}\ z\ {\isaliteral{7C}{\isacharbar}}{\isaliteral{7C}{\isacharbar}}\ {\isaliteral{3E}{\isachargreater}}\ {\isaliteral{7C}{\isacharbar}}{\isaliteral{7C}{\isacharbar}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\ {\isaliteral{7C}{\isacharbar}}{\isaliteral{7C}{\isacharbar}}\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\ z\ {\isaliteral{2F}{\isacharslash}}\ {\isaliteral{28}{\isacharparenleft}}z\ {\isaliteral{2D}{\isacharminus}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}{\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}n\ {\isaliteral{2A}{\isacharasterisk}}\ u\ {\isaliteral{5B}{\isacharbrackleft}}n{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{and}\isanewline
5.170 \ \ rule{\isadigit{5}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{7C}{\isacharbar}}{\isaliteral{7C}{\isacharbar}}\ z\ {\isaliteral{7C}{\isacharbar}}{\isaliteral{7C}{\isacharbar}}\ {\isaliteral{3C}{\isacharless}}\ {\isaliteral{7C}{\isacharbar}}{\isaliteral{7C}{\isacharbar}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\ {\isaliteral{7C}{\isacharbar}}{\isaliteral{7C}{\isacharbar}}\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\ z\ {\isaliteral{2F}{\isacharslash}}\ {\isaliteral{28}{\isacharparenleft}}z\ {\isaliteral{2D}{\isacharminus}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}{\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}n{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{2A}{\isacharasterisk}}\ u\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{2D}{\isacharminus}}n\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{1}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{and}\isanewline
5.171 -\ \ rule{\isadigit{6}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{7C}{\isacharbar}}{\isaliteral{7C}{\isacharbar}}\ z\ {\isaliteral{7C}{\isacharbar}}{\isaliteral{7C}{\isacharbar}}\ {\isaliteral{3E}{\isachargreater}}\ {\isadigit{1}}\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\ z{\isaliteral{2F}{\isacharslash}}{\isaliteral{28}{\isacharparenleft}}z\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{1}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}{\isadigit{2}}\ {\isaliteral{3D}{\isacharequal}}\ n\ {\isaliteral{2A}{\isacharasterisk}}\ u\ {\isaliteral{5B}{\isacharbrackleft}}n{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
5.172 +\ \ rule{\isadigit{6}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{7C}{\isacharbar}}{\isaliteral{7C}{\isacharbar}}\ z\ {\isaliteral{7C}{\isacharbar}}{\isaliteral{7C}{\isacharbar}}\ {\isaliteral{3E}{\isachargreater}}\ {\isadigit{1}}\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\ z{\isaliteral{2F}{\isacharslash}}{\isaliteral{28}{\isacharparenleft}}z\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{1}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}{\isadigit{2}}\ {\isaliteral{3D}{\isacharequal}}\ n\ {\isaliteral{2A}{\isacharasterisk}}\ u\ {\isaliteral{5B}{\isacharbrackleft}}n{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequoteclose}}%
5.173 +\begin{isamarkuptext}%
5.174 +\noindent Check the rules for their correct notation.
5.175 + (See the machine output.)%
5.176 +\end{isamarkuptext}%
5.177 +\isamarkuptrue%
5.178 %
5.179 \isadelimML
5.180 %
5.181 @@ -162,22 +188,22 @@
5.182 \isatagML
5.183 \isacommand{ML}\isamarkupfalse%
5.184 \ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
5.185 -%
5.186 +\ \ %
5.187 \isaantiq
5.188 thm\ rule{\isadigit{1}}{}%
5.189 \endisaantiq
5.190 {\isaliteral{3B}{\isacharsemicolon}}\isanewline
5.191 -%
5.192 +\ \ %
5.193 \isaantiq
5.194 thm\ rule{\isadigit{2}}{}%
5.195 \endisaantiq
5.196 {\isaliteral{3B}{\isacharsemicolon}}\isanewline
5.197 -%
5.198 +\ \ %
5.199 \isaantiq
5.200 thm\ rule{\isadigit{3}}{}%
5.201 \endisaantiq
5.202 {\isaliteral{3B}{\isacharsemicolon}}\isanewline
5.203 -%
5.204 +\ \ %
5.205 \isaantiq
5.206 thm\ rule{\isadigit{4}}{}%
5.207 \endisaantiq
5.208 @@ -190,7 +216,112 @@
5.209 %
5.210 \endisadelimML
5.211 %
5.212 -\isamarkupsubsection{apply rules%
5.213 +\isamarkupsubsection{Apply Rules%
5.214 +}
5.215 +\isamarkuptrue%
5.216 +%
5.217 +\begin{isamarkuptext}%
5.218 +\noindent We try to apply the rules to a given expression.%
5.219 +\end{isamarkuptext}%
5.220 +\isamarkuptrue%
5.221 +%
5.222 +\isadelimML
5.223 +%
5.224 +\endisadelimML
5.225 +%
5.226 +\isatagML
5.227 +\isacommand{ML}\isamarkupfalse%
5.228 +\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
5.229 +\ \ val\ inverse{\isaliteral{5F}{\isacharunderscore}}Z\ {\isaliteral{3D}{\isacharequal}}\ append{\isaliteral{5F}{\isacharunderscore}}rls\ {\isaliteral{22}{\isachardoublequote}}inverse{\isaliteral{5F}{\isacharunderscore}}Z{\isaliteral{22}{\isachardoublequote}}\ e{\isaliteral{5F}{\isacharunderscore}}rls\isanewline
5.230 +\ \ \ \ {\isaliteral{5B}{\isacharbrackleft}}\ Thm\ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequote}}rule{\isadigit{3}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}num{\isaliteral{5F}{\isacharunderscore}}str\ %
5.231 +\isaantiq
5.232 +thm\ rule{\isadigit{3}}{}%
5.233 +\endisaantiq
5.234 +{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\isanewline
5.235 +\ \ \ \ \ \ Thm\ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequote}}rule{\isadigit{4}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}num{\isaliteral{5F}{\isacharunderscore}}str\ %
5.236 +\isaantiq
5.237 +thm\ rule{\isadigit{4}}{}%
5.238 +\endisaantiq
5.239 +{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\isanewline
5.240 +\ \ \ \ \ \ Thm\ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequote}}rule{\isadigit{1}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}num{\isaliteral{5F}{\isacharunderscore}}str\ %
5.241 +\isaantiq
5.242 +thm\ rule{\isadigit{1}}{}%
5.243 +\endisaantiq
5.244 +{\isaliteral{29}{\isacharparenright}}\ \ \ \isanewline
5.245 +\ \ \ \ {\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
5.246 +\isanewline
5.247 +\ \ val\ t\ {\isaliteral{3D}{\isacharequal}}\ str{\isadigit{2}}term\ {\isaliteral{22}{\isachardoublequote}}z\ {\isaliteral{2F}{\isacharslash}}\ {\isaliteral{28}{\isacharparenleft}}z\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{1}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{2B}{\isacharplus}}\ z\ {\isaliteral{2F}{\isacharslash}}\ {\isaliteral{28}{\isacharparenleft}}z\ {\isaliteral{2D}{\isacharminus}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{2B}{\isacharplus}}\ {\isadigit{1}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
5.248 +\ \ val\ SOME\ {\isaliteral{28}{\isacharparenleft}}t{\isaliteral{27}{\isacharprime}}{\isaliteral{2C}{\isacharcomma}}\ asm{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ rewrite{\isaliteral{5F}{\isacharunderscore}}set{\isaliteral{5F}{\isacharunderscore}}\ thy\ true\ inverse{\isaliteral{5F}{\isacharunderscore}}Z\ t{\isaliteral{3B}{\isacharsemicolon}}\isanewline
5.249 +\ \ term{\isadigit{2}}str\ t{\isaliteral{27}{\isacharprime}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{22}{\isachardoublequote}}z\ {\isaliteral{2F}{\isacharslash}}\ {\isaliteral{28}{\isacharparenleft}}z\ {\isaliteral{2D}{\isacharminus}}\ {\isaliteral{3F}{\isacharquery}}{\isaliteral{5C3C64656C74613E}{\isasymdelta}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{3F}{\isacharquery}}n{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{2B}{\isacharplus}}\ z\ {\isaliteral{2F}{\isacharslash}}\ {\isaliteral{28}{\isacharparenleft}}z\ {\isaliteral{2D}{\isacharminus}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{2B}{\isacharplus}}\ {\isaliteral{3F}{\isacharquery}}{\isaliteral{5C3C64656C74613E}{\isasymdelta}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{3F}{\isacharquery}}n{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
5.250 +\ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}\isanewline
5.251 +\ \ \ {\isaliteral{2A}{\isacharasterisk}}\ Attention\ rule{\isadigit{1}}\ is\ applied\ before\ the\ expression\ is\ \isanewline
5.252 +\ \ \ {\isaliteral{2A}{\isacharasterisk}}\ checked\ for\ rule{\isadigit{4}}\ which\ would\ be\ correct{\isaliteral{21}{\isacharbang}}{\isaliteral{21}{\isacharbang}}{\isaliteral{21}{\isacharbang}}\isanewline
5.253 +\ \ \ {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline
5.254 +{\isaliteral{2A7D}{\isacharverbatimclose}}\isanewline
5.255 +\isanewline
5.256 +\isacommand{ML}\isamarkupfalse%
5.257 +\ {\isaliteral{7B2A}{\isacharverbatimopen}}\ val\ {\isaliteral{28}{\isacharparenleft}}thy{\isaliteral{2C}{\isacharcomma}}\ ro{\isaliteral{2C}{\isacharcomma}}\ er{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}%
5.258 +\isaantiq
5.259 +theory\ Isac{}%
5.260 +\endisaantiq
5.261 +{\isaliteral{2C}{\isacharcomma}}\ tless{\isaliteral{5F}{\isacharunderscore}}true{\isaliteral{2C}{\isacharcomma}}\ eval{\isaliteral{5F}{\isacharunderscore}}rls{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\ {\isaliteral{2A7D}{\isacharverbatimclose}}\isanewline
5.262 +\isacommand{ML}\isamarkupfalse%
5.263 +\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
5.264 +\ \ val\ SOME\ {\isaliteral{28}{\isacharparenleft}}t{\isaliteral{2C}{\isacharcomma}}\ asm{\isadigit{1}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ \isanewline
5.265 +\ \ \ \ rewrite{\isaliteral{5F}{\isacharunderscore}}\ thy\ ro\ er\ true\ {\isaliteral{28}{\isacharparenleft}}num{\isaliteral{5F}{\isacharunderscore}}str\ %
5.266 +\isaantiq
5.267 +thm\ rule{\isadigit{3}}{}%
5.268 +\endisaantiq
5.269 +{\isaliteral{29}{\isacharparenright}}\ t{\isaliteral{3B}{\isacharsemicolon}}\isanewline
5.270 +\ \ term{\isadigit{2}}str\ t\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{2D}{\isacharminus}}\ {\isaliteral{3F}{\isacharquery}}u\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{2D}{\isacharminus}}\ {\isaliteral{3F}{\isacharquery}}n\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{1}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{2B}{\isacharplus}}\ z\ {\isaliteral{2F}{\isacharslash}}\ {\isaliteral{28}{\isacharparenleft}}z\ {\isaliteral{2D}{\isacharminus}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{2B}{\isacharplus}}\ {\isadigit{1}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
5.271 +\ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{2D}{\isacharminus}}\ real\ {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline
5.272 +\ \ term{\isadigit{2}}str\ t{\isaliteral{3B}{\isacharsemicolon}}\isanewline
5.273 +\isanewline
5.274 +\ \ val\ SOME\ {\isaliteral{28}{\isacharparenleft}}t{\isaliteral{2C}{\isacharcomma}}\ asm{\isadigit{2}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ \isanewline
5.275 +\ \ \ \ rewrite{\isaliteral{5F}{\isacharunderscore}}\ thy\ ro\ er\ true\ {\isaliteral{28}{\isacharparenleft}}num{\isaliteral{5F}{\isacharunderscore}}str\ %
5.276 +\isaantiq
5.277 +thm\ rule{\isadigit{4}}{}%
5.278 +\endisaantiq
5.279 +{\isaliteral{29}{\isacharparenright}}\ t{\isaliteral{3B}{\isacharsemicolon}}\isanewline
5.280 +\ \ term{\isadigit{2}}str\ t\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{2D}{\isacharminus}}\ {\isaliteral{3F}{\isacharquery}}u\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{2D}{\isacharminus}}\ {\isaliteral{3F}{\isacharquery}}n\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{1}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{2B}{\isacharplus}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\ {\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}\ {\isaliteral{3F}{\isacharquery}}n\ {\isaliteral{2A}{\isacharasterisk}}\ {\isaliteral{3F}{\isacharquery}}u\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{3F}{\isacharquery}}n{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{2B}{\isacharplus}}\ {\isadigit{1}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
5.281 +\ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{2D}{\isacharminus}}\ real\ {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline
5.282 +\ \ term{\isadigit{2}}str\ t{\isaliteral{3B}{\isacharsemicolon}}\isanewline
5.283 +\isanewline
5.284 +\ \ val\ SOME\ {\isaliteral{28}{\isacharparenleft}}t{\isaliteral{2C}{\isacharcomma}}\ asm{\isadigit{3}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ \isanewline
5.285 +\ \ \ \ rewrite{\isaliteral{5F}{\isacharunderscore}}\ thy\ ro\ er\ true\ {\isaliteral{28}{\isacharparenleft}}num{\isaliteral{5F}{\isacharunderscore}}str\ %
5.286 +\isaantiq
5.287 +thm\ rule{\isadigit{1}}{}%
5.288 +\endisaantiq
5.289 +{\isaliteral{29}{\isacharparenright}}\ t{\isaliteral{3B}{\isacharsemicolon}}\isanewline
5.290 +\ \ term{\isadigit{2}}str\ t\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{2D}{\isacharminus}}\ {\isaliteral{3F}{\isacharquery}}u\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{2D}{\isacharminus}}\ {\isaliteral{3F}{\isacharquery}}n\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{1}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{2B}{\isacharplus}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\ {\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}\ {\isaliteral{3F}{\isacharquery}}n\ {\isaliteral{2A}{\isacharasterisk}}\ {\isaliteral{3F}{\isacharquery}}u\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{3F}{\isacharquery}}n{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{2B}{\isacharplus}}\ {\isaliteral{3F}{\isacharquery}}{\isaliteral{5C3C64656C74613E}{\isasymdelta}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{3F}{\isacharquery}}n{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
5.291 +\ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{2D}{\isacharminus}}\ real\ {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline
5.292 +\ \ term{\isadigit{2}}str\ t{\isaliteral{3B}{\isacharsemicolon}}\isanewline
5.293 +{\isaliteral{2A7D}{\isacharverbatimclose}}\isanewline
5.294 +\isacommand{ML}\isamarkupfalse%
5.295 +\ {\isaliteral{7B2A}{\isacharverbatimopen}}\ terms{\isadigit{2}}str\ {\isaliteral{28}{\isacharparenleft}}asm{\isadigit{1}}\ {\isaliteral{40}{\isacharat}}\ asm{\isadigit{2}}\ {\isaliteral{40}{\isacharat}}\ asm{\isadigit{3}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\ {\isaliteral{2A7D}{\isacharverbatimclose}}%
5.296 +\endisatagML
5.297 +{\isafoldML}%
5.298 +%
5.299 +\isadelimML
5.300 +%
5.301 +\endisadelimML
5.302 +%
5.303 +\isamarkupsection{Prepare Steps for CTP-based programming Language\label{sec:prepstep}%
5.304 +}
5.305 +\isamarkuptrue%
5.306 +%
5.307 +\begin{isamarkuptext}%
5.308 +\par \noindent The following sections are challanging with the CTP-based
5.309 + possibilities of building the programm. The goal is realized in
5.310 + Section~\ref{spec-meth} and Section~\ref{prog-steps}.
5.311 + \par The reader is advised to jump between the subsequent subsections and
5.312 + the respective steps in Section~\ref{prog-steps}. By comparing
5.313 + Section~\ref{sec:calc:ztrans} the calculation can be comprehended step
5.314 + by step.%
5.315 +\end{isamarkuptext}%
5.316 +\isamarkuptrue%
5.317 +%
5.318 +\isamarkupsubsection{Prepare Expression\label{prep-expr}%
5.319 }
5.320 \isamarkuptrue%
5.321 %
5.322 @@ -201,68 +332,21 @@
5.323 \isatagML
5.324 \isacommand{ML}\isamarkupfalse%
5.325 \ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
5.326 -val\ inverse{\isaliteral{5F}{\isacharunderscore}}Z\ {\isaliteral{3D}{\isacharequal}}\ append{\isaliteral{5F}{\isacharunderscore}}rls\ {\isaliteral{22}{\isachardoublequote}}inverse{\isaliteral{5F}{\isacharunderscore}}Z{\isaliteral{22}{\isachardoublequote}}\ e{\isaliteral{5F}{\isacharunderscore}}rls\isanewline
5.327 -\ \ {\isaliteral{5B}{\isacharbrackleft}}\ Thm\ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequote}}rule{\isadigit{3}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}num{\isaliteral{5F}{\isacharunderscore}}str\ %
5.328 -\isaantiq
5.329 -thm\ rule{\isadigit{3}}{}%
5.330 -\endisaantiq
5.331 -{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\isanewline
5.332 -\ \ \ \ Thm\ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequote}}rule{\isadigit{4}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}num{\isaliteral{5F}{\isacharunderscore}}str\ %
5.333 -\isaantiq
5.334 -thm\ rule{\isadigit{4}}{}%
5.335 -\endisaantiq
5.336 -{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\isanewline
5.337 -\ \ \ \ Thm\ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequote}}rule{\isadigit{1}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}num{\isaliteral{5F}{\isacharunderscore}}str\ %
5.338 -\isaantiq
5.339 -thm\ rule{\isadigit{1}}{}%
5.340 -\endisaantiq
5.341 -{\isaliteral{29}{\isacharparenright}}\ \ \ \isanewline
5.342 -\ \ {\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
5.343 -\isanewline
5.344 -val\ t\ {\isaliteral{3D}{\isacharequal}}\ str{\isadigit{2}}term\ {\isaliteral{22}{\isachardoublequote}}z\ {\isaliteral{2F}{\isacharslash}}\ {\isaliteral{28}{\isacharparenleft}}z\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{1}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{2B}{\isacharplus}}\ z\ {\isaliteral{2F}{\isacharslash}}\ {\isaliteral{28}{\isacharparenleft}}z\ {\isaliteral{2D}{\isacharminus}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{2B}{\isacharplus}}\ {\isadigit{1}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
5.345 -val\ SOME\ {\isaliteral{28}{\isacharparenleft}}t{\isaliteral{27}{\isacharprime}}{\isaliteral{2C}{\isacharcomma}}\ asm{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ rewrite{\isaliteral{5F}{\isacharunderscore}}set{\isaliteral{5F}{\isacharunderscore}}\ thy\ true\ inverse{\isaliteral{5F}{\isacharunderscore}}Z\ t{\isaliteral{3B}{\isacharsemicolon}}\isanewline
5.346 -term{\isadigit{2}}str\ t{\isaliteral{27}{\isacharprime}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{22}{\isachardoublequote}}z\ {\isaliteral{2F}{\isacharslash}}\ {\isaliteral{28}{\isacharparenleft}}z\ {\isaliteral{2D}{\isacharminus}}\ {\isaliteral{3F}{\isacharquery}}{\isaliteral{5C3C64656C74613E}{\isasymdelta}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{3F}{\isacharquery}}n{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{2B}{\isacharplus}}\ z\ {\isaliteral{2F}{\isacharslash}}\ {\isaliteral{28}{\isacharparenleft}}z\ {\isaliteral{2D}{\isacharminus}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{2B}{\isacharplus}}\ {\isaliteral{3F}{\isacharquery}}{\isaliteral{5C3C64656C74613E}{\isasymdelta}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{3F}{\isacharquery}}n{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3B}{\isacharsemicolon}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}attention\ rule{\isadigit{1}}\ {\isaliteral{21}{\isacharbang}}{\isaliteral{21}{\isacharbang}}{\isaliteral{21}{\isacharbang}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline
5.347 -{\isaliteral{2A7D}{\isacharverbatimclose}}\isanewline
5.348 -\isacommand{ML}\isamarkupfalse%
5.349 -\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
5.350 -val\ {\isaliteral{28}{\isacharparenleft}}thy{\isaliteral{2C}{\isacharcomma}}\ ro{\isaliteral{2C}{\isacharcomma}}\ er{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}%
5.351 +\ \ val\ ctxt\ {\isaliteral{3D}{\isacharequal}}\ ProofContext{\isaliteral{2E}{\isachardot}}init{\isaliteral{5F}{\isacharunderscore}}global\ %
5.352 \isaantiq
5.353 theory\ Isac{}%
5.354 \endisaantiq
5.355 -{\isaliteral{2C}{\isacharcomma}}\ tless{\isaliteral{5F}{\isacharunderscore}}true{\isaliteral{2C}{\isacharcomma}}\ eval{\isaliteral{5F}{\isacharunderscore}}rls{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
5.356 -{\isaliteral{2A7D}{\isacharverbatimclose}}\isanewline
5.357 -\isacommand{ML}\isamarkupfalse%
5.358 -\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
5.359 -val\ SOME\ {\isaliteral{28}{\isacharparenleft}}t{\isaliteral{2C}{\isacharcomma}}\ asm{\isadigit{1}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ rewrite{\isaliteral{5F}{\isacharunderscore}}\ thy\ ro\ er\ true\ {\isaliteral{28}{\isacharparenleft}}num{\isaliteral{5F}{\isacharunderscore}}str\ %
5.360 +{\isaliteral{3B}{\isacharsemicolon}}\isanewline
5.361 +\ \ val\ ctxt\ {\isaliteral{3D}{\isacharequal}}\ declare{\isaliteral{5F}{\isacharunderscore}}constraints{\isaliteral{27}{\isacharprime}}\ {\isaliteral{5B}{\isacharbrackleft}}%
5.362 \isaantiq
5.363 -thm\ rule{\isadigit{3}}{}%
5.364 +term\ {\isaliteral{22}{\isachardoublequote}}z{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}real{\isaliteral{22}{\isachardoublequote}}{}%
5.365 \endisaantiq
5.366 -{\isaliteral{29}{\isacharparenright}}\ t{\isaliteral{3B}{\isacharsemicolon}}\isanewline
5.367 -term{\isadigit{2}}str\ t\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{2D}{\isacharminus}}\ {\isaliteral{3F}{\isacharquery}}u\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{2D}{\isacharminus}}\ {\isaliteral{3F}{\isacharquery}}n\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{1}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{2B}{\isacharplus}}\ z\ {\isaliteral{2F}{\isacharslash}}\ {\isaliteral{28}{\isacharparenleft}}z\ {\isaliteral{2D}{\isacharminus}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{2B}{\isacharplus}}\ {\isadigit{1}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3B}{\isacharsemicolon}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{2D}{\isacharminus}}\ real\ {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline
5.368 -term{\isadigit{2}}str\ t{\isaliteral{3B}{\isacharsemicolon}}{\isaliteral{2A7D}{\isacharverbatimclose}}\isanewline
5.369 -\isacommand{ML}\isamarkupfalse%
5.370 -\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
5.371 -val\ SOME\ {\isaliteral{28}{\isacharparenleft}}t{\isaliteral{2C}{\isacharcomma}}\ asm{\isadigit{2}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ rewrite{\isaliteral{5F}{\isacharunderscore}}\ thy\ ro\ er\ true\ {\isaliteral{28}{\isacharparenleft}}num{\isaliteral{5F}{\isacharunderscore}}str\ %
5.372 -\isaantiq
5.373 -thm\ rule{\isadigit{4}}{}%
5.374 -\endisaantiq
5.375 -{\isaliteral{29}{\isacharparenright}}\ t{\isaliteral{3B}{\isacharsemicolon}}\isanewline
5.376 -term{\isadigit{2}}str\ t\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{2D}{\isacharminus}}\ {\isaliteral{3F}{\isacharquery}}u\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{2D}{\isacharminus}}\ {\isaliteral{3F}{\isacharquery}}n\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{1}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{2B}{\isacharplus}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\ {\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}\ {\isaliteral{3F}{\isacharquery}}n\ {\isaliteral{2A}{\isacharasterisk}}\ {\isaliteral{3F}{\isacharquery}}u\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{3F}{\isacharquery}}n{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{2B}{\isacharplus}}\ {\isadigit{1}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3B}{\isacharsemicolon}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{2D}{\isacharminus}}\ real\ {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline
5.377 -term{\isadigit{2}}str\ t{\isaliteral{3B}{\isacharsemicolon}}\isanewline
5.378 -{\isaliteral{2A7D}{\isacharverbatimclose}}\isanewline
5.379 -\isacommand{ML}\isamarkupfalse%
5.380 -\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
5.381 -val\ SOME\ {\isaliteral{28}{\isacharparenleft}}t{\isaliteral{2C}{\isacharcomma}}\ asm{\isadigit{3}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ rewrite{\isaliteral{5F}{\isacharunderscore}}\ thy\ ro\ er\ true\ {\isaliteral{28}{\isacharparenleft}}num{\isaliteral{5F}{\isacharunderscore}}str\ %
5.382 -\isaantiq
5.383 -thm\ rule{\isadigit{1}}{}%
5.384 -\endisaantiq
5.385 -{\isaliteral{29}{\isacharparenright}}\ t{\isaliteral{3B}{\isacharsemicolon}}\isanewline
5.386 -term{\isadigit{2}}str\ t\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{2D}{\isacharminus}}\ {\isaliteral{3F}{\isacharquery}}u\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{2D}{\isacharminus}}\ {\isaliteral{3F}{\isacharquery}}n\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{1}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{2B}{\isacharplus}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\ {\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}\ {\isaliteral{3F}{\isacharquery}}n\ {\isaliteral{2A}{\isacharasterisk}}\ {\isaliteral{3F}{\isacharquery}}u\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{3F}{\isacharquery}}n{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{2B}{\isacharplus}}\ {\isaliteral{3F}{\isacharquery}}{\isaliteral{5C3C64656C74613E}{\isasymdelta}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{3F}{\isacharquery}}n{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3B}{\isacharsemicolon}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{2D}{\isacharminus}}\ real\ {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline
5.387 -term{\isadigit{2}}str\ t{\isaliteral{3B}{\isacharsemicolon}}\isanewline
5.388 -{\isaliteral{2A7D}{\isacharverbatimclose}}\isanewline
5.389 -\isacommand{ML}\isamarkupfalse%
5.390 -\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
5.391 -terms{\isadigit{2}}str\ {\isaliteral{28}{\isacharparenleft}}asm{\isadigit{1}}\ {\isaliteral{40}{\isacharat}}\ asm{\isadigit{2}}\ {\isaliteral{40}{\isacharat}}\ asm{\isadigit{3}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
5.392 +{\isaliteral{5D}{\isacharbrackright}}\ ctxt{\isaliteral{3B}{\isacharsemicolon}}\isanewline
5.393 +\isanewline
5.394 +\ \ val\ SOME\ fun{\isadigit{1}}\ {\isaliteral{3D}{\isacharequal}}\ \isanewline
5.395 +\ \ \ \ parseNEW\ ctxt\ {\isaliteral{22}{\isachardoublequote}}X\ z\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{3}}\ {\isaliteral{2F}{\isacharslash}}\ {\isaliteral{28}{\isacharparenleft}}z\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{1}}{\isaliteral{2F}{\isacharslash}}{\isadigit{4}}\ {\isaliteral{2B}{\isacharplus}}\ {\isaliteral{2D}{\isacharminus}}{\isadigit{1}}{\isaliteral{2F}{\isacharslash}}{\isadigit{8}}\ {\isaliteral{2A}{\isacharasterisk}}\ z\ {\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}\ {\isaliteral{2D}{\isacharminus}}{\isadigit{1}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3B}{\isacharsemicolon}}\ term{\isadigit{2}}str\ fun{\isadigit{1}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
5.396 +\ \ val\ SOME\ fun{\isadigit{1}}{\isaliteral{27}{\isacharprime}}\ {\isaliteral{3D}{\isacharequal}}\ \isanewline
5.397 +\ \ \ \ parseNEW\ ctxt\ {\isaliteral{22}{\isachardoublequote}}X\ z\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{3}}\ {\isaliteral{2F}{\isacharslash}}\ {\isaliteral{28}{\isacharparenleft}}z\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{1}}{\isaliteral{2F}{\isacharslash}}{\isadigit{4}}\ {\isaliteral{2B}{\isacharplus}}\ {\isaliteral{2D}{\isacharminus}}{\isadigit{1}}{\isaliteral{2F}{\isacharslash}}{\isadigit{8}}\ {\isaliteral{2A}{\isacharasterisk}}\ {\isaliteral{28}{\isacharparenleft}}{\isadigit{1}}{\isaliteral{2F}{\isacharslash}}z{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3B}{\isacharsemicolon}}\ term{\isadigit{2}}str\ fun{\isadigit{1}}{\isaliteral{27}{\isacharprime}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
5.398 {\isaliteral{2A7D}{\isacharverbatimclose}}%
5.399 \endisatagML
5.400 {\isafoldML}%
5.401 @@ -271,54 +355,17 @@
5.402 %
5.403 \endisadelimML
5.404 %
5.405 -\isamarkupsection{Prepare steps for CTP-based programming language%
5.406 +\isamarkupsubsubsection{Prepare Numerator and Denominator%
5.407 }
5.408 \isamarkuptrue%
5.409 %
5.410 \begin{isamarkuptext}%
5.411 -TODO insert Calculation (Referenz?!)
5.412 -
5.413 -The goal... realized in sections below, in Sect.\ref{spec-meth} and Sect.\ref{prog-steps}
5.414 -
5.415 -the reader is advised to jump between the subsequent subsections and the respective steps in Sect.\ref{prog-steps}%
5.416 +\noindent The partial fraction decomposion is only possible ig we
5.417 + get the bound variable out of the numerator. Therefor we divide
5.418 + the expression by $z$. Follow up the Calculation at
5.419 + Section~\ref{sec:calc:ztrans} line number 02.%
5.420 \end{isamarkuptext}%
5.421 \isamarkuptrue%
5.422 -%
5.423 -\isamarkupsubsection{prepare expression \label{prep-expr}%
5.424 -}
5.425 -\isamarkuptrue%
5.426 -%
5.427 -\isadelimML
5.428 -%
5.429 -\endisadelimML
5.430 -%
5.431 -\isatagML
5.432 -\isacommand{ML}\isamarkupfalse%
5.433 -\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
5.434 -val\ ctxt\ {\isaliteral{3D}{\isacharequal}}\ ProofContext{\isaliteral{2E}{\isachardot}}init{\isaliteral{5F}{\isacharunderscore}}global\ %
5.435 -\isaantiq
5.436 -theory\ Isac{}%
5.437 -\endisaantiq
5.438 -{\isaliteral{3B}{\isacharsemicolon}}\isanewline
5.439 -val\ ctxt\ {\isaliteral{3D}{\isacharequal}}\ declare{\isaliteral{5F}{\isacharunderscore}}constraints{\isaliteral{27}{\isacharprime}}\ {\isaliteral{5B}{\isacharbrackleft}}%
5.440 -\isaantiq
5.441 -term\ {\isaliteral{22}{\isachardoublequote}}z{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}real{\isaliteral{22}{\isachardoublequote}}{}%
5.442 -\endisaantiq
5.443 -{\isaliteral{5D}{\isacharbrackright}}\ ctxt{\isaliteral{3B}{\isacharsemicolon}}\isanewline
5.444 -\isanewline
5.445 -val\ SOME\ fun{\isadigit{1}}\ {\isaliteral{3D}{\isacharequal}}\ parseNEW\ ctxt\ {\isaliteral{22}{\isachardoublequote}}X\ z\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{3}}\ {\isaliteral{2F}{\isacharslash}}\ {\isaliteral{28}{\isacharparenleft}}z\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{1}}{\isaliteral{2F}{\isacharslash}}{\isadigit{4}}\ {\isaliteral{2B}{\isacharplus}}\ {\isaliteral{2D}{\isacharminus}}{\isadigit{1}}{\isaliteral{2F}{\isacharslash}}{\isadigit{8}}\ {\isaliteral{2A}{\isacharasterisk}}\ z\ {\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}\ {\isaliteral{2D}{\isacharminus}}{\isadigit{1}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3B}{\isacharsemicolon}}\ term{\isadigit{2}}str\ fun{\isadigit{1}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
5.446 -val\ SOME\ fun{\isadigit{1}}{\isaliteral{27}{\isacharprime}}\ {\isaliteral{3D}{\isacharequal}}\ parseNEW\ ctxt\ {\isaliteral{22}{\isachardoublequote}}X\ z\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{3}}\ {\isaliteral{2F}{\isacharslash}}\ {\isaliteral{28}{\isacharparenleft}}z\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{1}}{\isaliteral{2F}{\isacharslash}}{\isadigit{4}}\ {\isaliteral{2B}{\isacharplus}}\ {\isaliteral{2D}{\isacharminus}}{\isadigit{1}}{\isaliteral{2F}{\isacharslash}}{\isadigit{8}}\ {\isaliteral{2A}{\isacharasterisk}}\ {\isaliteral{28}{\isacharparenleft}}{\isadigit{1}}{\isaliteral{2F}{\isacharslash}}z{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3B}{\isacharsemicolon}}\ term{\isadigit{2}}str\ fun{\isadigit{1}}{\isaliteral{27}{\isacharprime}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
5.447 -{\isaliteral{2A7D}{\isacharverbatimclose}}%
5.448 -\endisatagML
5.449 -{\isafoldML}%
5.450 -%
5.451 -\isadelimML
5.452 -%
5.453 -\endisadelimML
5.454 -%
5.455 -\isamarkupsubsubsection{multply with z%
5.456 -}
5.457 -\isamarkuptrue%
5.458 \isacommand{axiomatization}\isamarkupfalse%
5.459 \ \isakeyword{where}\isanewline
5.460 \ \ ruleZY{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}X\ z\ {\isaliteral{3D}{\isacharequal}}\ a\ {\isaliteral{2F}{\isacharslash}}\ b{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}X{\isaliteral{27}{\isacharprime}}\ z\ {\isaliteral{3D}{\isacharequal}}\ a\ {\isaliteral{2F}{\isacharslash}}\ {\isaliteral{28}{\isacharparenleft}}z\ {\isaliteral{2A}{\isacharasterisk}}\ b{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
5.461 @@ -331,34 +378,45 @@
5.462 \isatagML
5.463 \isacommand{ML}\isamarkupfalse%
5.464 \ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
5.465 -val\ {\isaliteral{28}{\isacharparenleft}}thy{\isaliteral{2C}{\isacharcomma}}\ ro{\isaliteral{2C}{\isacharcomma}}\ er{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}%
5.466 +\ \ val\ {\isaliteral{28}{\isacharparenleft}}thy{\isaliteral{2C}{\isacharcomma}}\ ro{\isaliteral{2C}{\isacharcomma}}\ er{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}%
5.467 \isaantiq
5.468 theory\ Isac{}%
5.469 \endisaantiq
5.470 {\isaliteral{2C}{\isacharcomma}}\ tless{\isaliteral{5F}{\isacharunderscore}}true{\isaliteral{2C}{\isacharcomma}}\ eval{\isaliteral{5F}{\isacharunderscore}}rls{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
5.471 -val\ SOME\ {\isaliteral{28}{\isacharparenleft}}fun{\isadigit{2}}{\isaliteral{2C}{\isacharcomma}}\ asm{\isadigit{1}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ rewrite{\isaliteral{5F}{\isacharunderscore}}\ thy\ ro\ er\ true\ \ %
5.472 +\ \ val\ SOME\ {\isaliteral{28}{\isacharparenleft}}fun{\isadigit{2}}{\isaliteral{2C}{\isacharcomma}}\ asm{\isadigit{1}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ \isanewline
5.473 +\ \ \ \ rewrite{\isaliteral{5F}{\isacharunderscore}}\ thy\ ro\ er\ true\ \ %
5.474 \isaantiq
5.475 thm\ ruleZY{}%
5.476 \endisaantiq
5.477 \ fun{\isadigit{1}}{\isaliteral{3B}{\isacharsemicolon}}\ term{\isadigit{2}}str\ fun{\isadigit{2}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
5.478 -val\ SOME\ {\isaliteral{28}{\isacharparenleft}}fun{\isadigit{2}}{\isaliteral{27}{\isacharprime}}{\isaliteral{2C}{\isacharcomma}}\ asm{\isadigit{1}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ rewrite{\isaliteral{5F}{\isacharunderscore}}\ thy\ ro\ er\ true\ \ %
5.479 +\ \ val\ SOME\ {\isaliteral{28}{\isacharparenleft}}fun{\isadigit{2}}{\isaliteral{27}{\isacharprime}}{\isaliteral{2C}{\isacharcomma}}\ asm{\isadigit{1}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ \isanewline
5.480 +\ \ \ \ rewrite{\isaliteral{5F}{\isacharunderscore}}\ thy\ ro\ er\ true\ \ %
5.481 \isaantiq
5.482 thm\ ruleZY{}%
5.483 \endisaantiq
5.484 \ fun{\isadigit{1}}{\isaliteral{27}{\isacharprime}}{\isaliteral{3B}{\isacharsemicolon}}\ term{\isadigit{2}}str\ fun{\isadigit{2}}{\isaliteral{27}{\isacharprime}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
5.485 \isanewline
5.486 -val\ SOME\ {\isaliteral{28}{\isacharparenleft}}fun{\isadigit{3}}{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ rewrite{\isaliteral{5F}{\isacharunderscore}}set{\isaliteral{5F}{\isacharunderscore}}\ %
5.487 +\ \ val\ SOME\ {\isaliteral{28}{\isacharparenleft}}fun{\isadigit{3}}{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ \isanewline
5.488 +\ \ \ \ rewrite{\isaliteral{5F}{\isacharunderscore}}set{\isaliteral{5F}{\isacharunderscore}}\ %
5.489 \isaantiq
5.490 theory\ Isac{}%
5.491 \endisaantiq
5.492 \ false\ norm{\isaliteral{5F}{\isacharunderscore}}Rational\ fun{\isadigit{2}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
5.493 -term{\isadigit{2}}str\ fun{\isadigit{3}}{\isaliteral{3B}{\isacharsemicolon}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}fails\ on\ x{\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{2D}{\isacharminus}}{\isadigit{1}}{\isaliteral{29}{\isacharparenright}}\ TODO{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline
5.494 -val\ SOME\ {\isaliteral{28}{\isacharparenleft}}fun{\isadigit{3}}{\isaliteral{27}{\isacharprime}}{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ rewrite{\isaliteral{5F}{\isacharunderscore}}set{\isaliteral{5F}{\isacharunderscore}}\ %
5.495 +\ \ term{\isadigit{2}}str\ fun{\isadigit{3}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
5.496 +\ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}\isanewline
5.497 +\ \ \ {\isaliteral{2A}{\isacharasterisk}}\ Fails\ on\ x{\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{2D}{\isacharminus}}{\isadigit{1}}{\isaliteral{29}{\isacharparenright}}\isanewline
5.498 +\ \ \ {\isaliteral{2A}{\isacharasterisk}}\ We\ solve\ this\ problem\ by\ using\ {\isadigit{1}}{\isaliteral{2F}{\isacharslash}}x\ as\ a\ workaround{\isaliteral{2E}{\isachardot}}\isanewline
5.499 +\ \ \ {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline
5.500 +\ \ val\ SOME\ {\isaliteral{28}{\isacharparenleft}}fun{\isadigit{3}}{\isaliteral{27}{\isacharprime}}{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ \isanewline
5.501 +\ \ \ \ rewrite{\isaliteral{5F}{\isacharunderscore}}set{\isaliteral{5F}{\isacharunderscore}}\ %
5.502 \isaantiq
5.503 theory\ Isac{}%
5.504 \endisaantiq
5.505 \ false\ norm{\isaliteral{5F}{\isacharunderscore}}Rational\ fun{\isadigit{2}}{\isaliteral{27}{\isacharprime}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
5.506 -term{\isadigit{2}}str\ fun{\isadigit{3}}{\isaliteral{27}{\isacharprime}}{\isaliteral{3B}{\isacharsemicolon}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}OK{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline
5.507 +\ \ term{\isadigit{2}}str\ fun{\isadigit{3}}{\isaliteral{27}{\isacharprime}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
5.508 +\ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}\isanewline
5.509 +\ \ \ {\isaliteral{2A}{\isacharasterisk}}\ OK\ {\isaliteral{2D}{\isacharminus}}\ workaround{\isaliteral{21}{\isacharbang}}\isanewline
5.510 +\ \ \ {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline
5.511 {\isaliteral{2A7D}{\isacharverbatimclose}}%
5.512 \endisatagML
5.513 {\isafoldML}%
5.514 @@ -367,21 +425,26 @@
5.515 %
5.516 \endisadelimML
5.517 %
5.518 -\isamarkupsubsubsection{get argument of X': z is the variable the equation is solved for%
5.519 +\isamarkupsubsubsection{Get the Argument of the Expression X'%
5.520 }
5.521 \isamarkuptrue%
5.522 %
5.523 \begin{isamarkuptext}%
5.524 -grep... Atools.thy, Tools.thy contain general utilities: eval_argument_in, eval_rhs, eval_lhs,...
5.525 -
5.526 -grep -r "fun eva_" ... shows all functions witch can be used in a script.
5.527 -lookup this files how to build and handle such functions.
5.528 -
5.529 -the next section shows how to introduce such a function.%
5.530 +\noindent We use \texttt{grep} for finding possibilities how we can
5.531 + extract the bound variable in the expression. \ttfamily Atools.thy,
5.532 + Tools.thy \normalfont contain general utilities: \ttfamily
5.533 + eval\_argument\_in, eval\_rhs, eval\_lhs,\ldots \normalfont
5.534 + \ttfamily grep -r "fun eva\_" * \normalfont shows all functions
5.535 + witch can be used in a script. Lookup this files how to build
5.536 + and handle such functions.
5.537 + \par The next section shows how to introduce such a function.%
5.538 \end{isamarkuptext}%
5.539 \isamarkuptrue%
5.540 %
5.541 -\isamarkupsubsubsection{Decompose given term into lhs = rhs%
5.542 +\isamarkupsubsubsection{Decompose the Given Term Into lhs and rhs\footnote{Note:
5.543 + lhs means \em Left Hand Side \normalfont and rhs means
5.544 + \em Right Hand Side \normalfont and indicates the left or
5.545 + the right part of an equation.}%
5.546 }
5.547 \isamarkuptrue%
5.548 %
5.549 @@ -393,7 +456,8 @@
5.550 \isacommand{ML}\isamarkupfalse%
5.551 \ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
5.552 \ \ val\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}\ expr{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ HOLogic{\isaliteral{2E}{\isachardot}}dest{\isaliteral{5F}{\isacharunderscore}}eq\ fun{\isadigit{3}}{\isaliteral{27}{\isacharprime}}{\isaliteral{3B}{\isacharsemicolon}}\ term{\isadigit{2}}str\ expr{\isaliteral{3B}{\isacharsemicolon}}\isanewline
5.553 -\ \ val\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}\ denom{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ HOLogic{\isaliteral{2E}{\isachardot}}dest{\isaliteral{5F}{\isacharunderscore}}bin\ {\isaliteral{22}{\isachardoublequote}}Rings{\isaliteral{2E}{\isachardot}}inverse{\isaliteral{5F}{\isacharunderscore}}class{\isaliteral{2E}{\isachardot}}divide{\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{28}{\isacharparenleft}}type{\isaliteral{5F}{\isacharunderscore}}of\ expr{\isaliteral{29}{\isacharparenright}}\ expr{\isaliteral{3B}{\isacharsemicolon}}\isanewline
5.554 +\ \ val\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}\ denom{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ \isanewline
5.555 +\ \ \ \ HOLogic{\isaliteral{2E}{\isachardot}}dest{\isaliteral{5F}{\isacharunderscore}}bin\ {\isaliteral{22}{\isachardoublequote}}Rings{\isaliteral{2E}{\isachardot}}inverse{\isaliteral{5F}{\isacharunderscore}}class{\isaliteral{2E}{\isachardot}}divide{\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{28}{\isacharparenleft}}type{\isaliteral{5F}{\isacharunderscore}}of\ expr{\isaliteral{29}{\isacharparenright}}\ expr{\isaliteral{3B}{\isacharsemicolon}}\isanewline
5.556 \ \ term{\isadigit{2}}str\ denom\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{2D}{\isacharminus}}{\isadigit{1}}\ {\isaliteral{2B}{\isacharplus}}\ {\isaliteral{2D}{\isacharminus}}{\isadigit{2}}\ {\isaliteral{2A}{\isacharasterisk}}\ z\ {\isaliteral{2B}{\isacharplus}}\ {\isadigit{8}}\ {\isaliteral{2A}{\isacharasterisk}}\ z\ {\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}\ {\isadigit{2}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
5.557 {\isaliteral{2A7D}{\isacharverbatimclose}}%
5.558 \endisatagML
5.559 @@ -404,17 +468,18 @@
5.560 \endisadelimML
5.561 %
5.562 \begin{isamarkuptext}%
5.563 -we have rhs in the Script language, but we need a function
5.564 - which gets the denominator of a fraction%
5.565 +\noindent We have rhs in the Script language, but we need a function
5.566 + which gets the denominator of a fraction.%
5.567 \end{isamarkuptext}%
5.568 \isamarkuptrue%
5.569 %
5.570 -\isamarkupsubsubsection{get the denominator and numerator out of a fraction%
5.571 +\isamarkupsubsubsection{Get the Denominator and Numerator out of a Fraction%
5.572 }
5.573 \isamarkuptrue%
5.574 %
5.575 \begin{isamarkuptext}%
5.576 -get denominator should become a constant for the isabelle parser:%
5.577 +\noindent The selv written functions in e.g. \texttt{get\_denominator}
5.578 + should become a constant for the isabelle parser:%
5.579 \end{isamarkuptext}%
5.580 \isamarkuptrue%
5.581 \isacommand{consts}\isamarkupfalse%
5.582 @@ -422,11 +487,14 @@
5.583 \ \ get{\isaliteral{5F}{\isacharunderscore}}denominator\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}real\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\ real{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
5.584 \ \ get{\isaliteral{5F}{\isacharunderscore}}numerator\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}real\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\ real{\isaliteral{22}{\isachardoublequoteclose}}%
5.585 \begin{isamarkuptext}%
5.586 -With the above definition we run into problems with parsing the Script InverseZTransform:
5.587 - This leads to "ambiguous parse trees" and we avoid this by shifting the definition
5.588 - to Rational.thy and re-building Isac.
5.589 - ATTENTION: from now on Build_Inverse_Z_Transform mimics a build from scratch;
5.590 - it only works due to re-building Isac several times (indicated explicityl).%
5.591 +\noindent With the above definition we run into problems when we parse
5.592 + the Script \texttt{InverseZTransform}. This leads to \em ambiguous
5.593 + parse trees. \normalfont We avoid this by moving the definition
5.594 + to \ttfamily Rational.thy \normalfont and re-building Isac.
5.595 + \par \noindent ATTENTION: From now on \ttfamily
5.596 + Build\_Inverse\_Z\_Transform \normalfont mimics a build from scratch;
5.597 + it only works due to re-building Isac several times (indicated
5.598 + explicityl).%
5.599 \end{isamarkuptext}%
5.600 \isamarkuptrue%
5.601 %
5.602 @@ -437,16 +505,19 @@
5.603 \isatagML
5.604 \isacommand{ML}\isamarkupfalse%
5.605 \ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
5.606 -{\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequote}}get{\isaliteral{5F}{\isacharunderscore}}denominator{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequote}}Rational{\isaliteral{2E}{\isachardot}}get{\isaliteral{5F}{\isacharunderscore}}denominator{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ eval{\isaliteral{5F}{\isacharunderscore}}get{\isaliteral{5F}{\isacharunderscore}}denominator\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline
5.607 +{\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}\isanewline
5.608 +\ {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequote}}get{\isaliteral{5F}{\isacharunderscore}}denominator{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\isanewline
5.609 +\ {\isaliteral{2A}{\isacharasterisk}}\ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequote}}Rational{\isaliteral{2E}{\isachardot}}get{\isaliteral{5F}{\isacharunderscore}}denominator{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ eval{\isaliteral{5F}{\isacharunderscore}}get{\isaliteral{5F}{\isacharunderscore}}denominator\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\isanewline
5.610 +\ {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline
5.611 fun\ eval{\isaliteral{5F}{\isacharunderscore}}get{\isaliteral{5F}{\isacharunderscore}}denominator\ {\isaliteral{28}{\isacharparenleft}}thmid{\isaliteral{3A}{\isacharcolon}}string{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5F}{\isacharunderscore}}\ \isanewline
5.612 \ \ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}t\ as\ Const\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequote}}Rational{\isaliteral{2E}{\isachardot}}get{\isaliteral{5F}{\isacharunderscore}}denominator{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5F}{\isacharunderscore}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{24}{\isachardollar}}\isanewline
5.613 \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}Const\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequote}}Rings{\isaliteral{2E}{\isachardot}}inverse{\isaliteral{5F}{\isacharunderscore}}class{\isaliteral{2E}{\isachardot}}divide{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5F}{\isacharunderscore}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{24}{\isachardollar}}\ num\ {\isaliteral{24}{\isachardollar}}\isanewline
5.614 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ denom{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ thy\ {\isaliteral{3D}{\isacharequal}}\ \isanewline
5.615 \ \ \ \ \ \ \ \ SOME\ {\isaliteral{28}{\isacharparenleft}}mk{\isaliteral{5F}{\isacharunderscore}}thmid\ thmid\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{22}{\isachardoublequote}}\ \isanewline
5.616 -\ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}Print{\isaliteral{5F}{\isacharunderscore}}Mode{\isaliteral{2E}{\isachardot}}setmp\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{28}{\isacharparenleft}}Syntax{\isaliteral{2E}{\isachardot}}string{\isaliteral{5F}{\isacharunderscore}}of{\isaliteral{5F}{\isacharunderscore}}term\ {\isaliteral{28}{\isacharparenleft}}thy{\isadigit{2}}ctxt\ thy{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ denom{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ \isanewline
5.617 +\ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}Print{\isaliteral{5F}{\isacharunderscore}}Mode{\isaliteral{2E}{\isachardot}}setmp\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ \isanewline
5.618 +\ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}Syntax{\isaliteral{2E}{\isachardot}}string{\isaliteral{5F}{\isacharunderscore}}of{\isaliteral{5F}{\isacharunderscore}}term\ {\isaliteral{28}{\isacharparenleft}}thy{\isadigit{2}}ctxt\ thy{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ denom{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ \isanewline
5.619 \ \ \ \ \ \ \ \ \ \ Trueprop\ {\isaliteral{24}{\isachardollar}}\ {\isaliteral{28}{\isacharparenleft}}mk{\isaliteral{5F}{\isacharunderscore}}equality\ {\isaliteral{28}{\isacharparenleft}}t{\isaliteral{2C}{\isacharcomma}}\ denom{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\isanewline
5.620 \ \ {\isaliteral{7C}{\isacharbar}}\ eval{\isaliteral{5F}{\isacharunderscore}}get{\isaliteral{5F}{\isacharunderscore}}denominator\ {\isaliteral{5F}{\isacharunderscore}}\ {\isaliteral{5F}{\isacharunderscore}}\ {\isaliteral{5F}{\isacharunderscore}}\ {\isaliteral{5F}{\isacharunderscore}}\ {\isaliteral{3D}{\isacharequal}}\ NONE{\isaliteral{3B}{\isacharsemicolon}}\ \isanewline
5.621 -\isanewline
5.622 {\isaliteral{2A7D}{\isacharverbatimclose}}%
5.623 \endisatagML
5.624 {\isafoldML}%
5.625 @@ -704,7 +775,7 @@
5.626 \ \ in\ HOLogic{\isaliteral{2E}{\isachardot}}mk{\isaliteral{5F}{\isacharunderscore}}binop\ {\isaliteral{22}{\isachardoublequote}}Groups{\isaliteral{2E}{\isachardot}}times{\isaliteral{5F}{\isacharunderscore}}class{\isaliteral{2E}{\isachardot}}times{\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{28}{\isacharparenleft}}minus{\isaliteral{5F}{\isacharunderscore}}{\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ t{\isaliteral{29}{\isacharparenright}}\ end{\isaliteral{3B}{\isacharsemicolon}}\isanewline
5.627 fun\ fac{\isaliteral{5F}{\isacharunderscore}}from{\isaliteral{5F}{\isacharunderscore}}sol\ s\ {\isaliteral{3D}{\isacharequal}}\isanewline
5.628 \ \ let\ val\ {\isaliteral{28}{\isacharparenleft}}lhs{\isaliteral{2C}{\isacharcomma}}\ rhs{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ HOLogic{\isaliteral{2E}{\isachardot}}dest{\isaliteral{5F}{\isacharunderscore}}eq\ s\isanewline
5.629 -\ \ in\ HOLogic{\isaliteral{2E}{\isachardot}}mk{\isaliteral{5F}{\isacharunderscore}}binop\ {\isaliteral{22}{\isachardoublequote}}Groups{\isaliteral{2E}{\isachardot}}plus{\isaliteral{5F}{\isacharunderscore}}class{\isaliteral{2E}{\isachardot}}plus{\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{28}{\isacharparenleft}}lhs{\isaliteral{2C}{\isacharcomma}}\ flip{\isaliteral{5F}{\isacharunderscore}}sign\ rhs{\isaliteral{29}{\isacharparenright}}\ end{\isaliteral{3B}{\isacharsemicolon}}\isanewline
5.630 +\ \ in\ HOLogic{\isaliteral{2E}{\isachardot}}mk{\isaliteral{5F}{\isacharunderscore}}binop\ {\isaliteral{22}{\isachardoublequote}}Groups{\isaliteral{2E}{\isachardot}}minus{\isaliteral{5F}{\isacharunderscore}}class{\isaliteral{2E}{\isachardot}}minus{\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{28}{\isacharparenleft}}lhs{\isaliteral{2C}{\isacharcomma}}\ rhs{\isaliteral{29}{\isacharparenright}}\ end{\isaliteral{3B}{\isacharsemicolon}}\isanewline
5.631 {\isaliteral{2A7D}{\isacharverbatimclose}}\isanewline
5.632 \isacommand{ML}\isamarkupfalse%
5.633 \ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
5.634 @@ -1569,8 +1640,6 @@
5.635 \ \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ \ \ \ \ {\isaliteral{5B}{\isacharbrackleft}}univariate{\isaliteral{2C}{\isacharcomma}}equation{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5B}{\isacharbrackleft}}no{\isaliteral{5F}{\isacharunderscore}}met{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{5E}{\isacharcircum}}\isanewline
5.636 \ \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ \ \ {\isaliteral{5B}{\isacharbrackleft}}BOOL\ eq{\isaliteral{5F}{\isacharunderscore}}a{\isaliteral{2C}{\isacharcomma}}\ REAL\ {\isaliteral{28}{\isacharparenleft}}A{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}real{\isaliteral{29}{\isacharparenright}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5E}{\isacharcircum}}\isanewline
5.637 \ \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}a{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}real{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}rhs{\isaliteral{28}{\isacharparenleft}}NTH\ {\isadigit{1}}\ sol{\isaliteral{5F}{\isacharunderscore}}a{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5E}{\isacharcircum}}\isanewline
5.638 -{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}aarg{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}real{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}lhs{\isaliteral{28}{\isacharparenleft}}NTH\ {\isadigit{1}}\ sol{\isaliteral{5F}{\isacharunderscore}}a{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5E}{\isacharcircum}}\isanewline
5.639 -\isanewline
5.640 \isanewline
5.641 \ \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}eq{\isaliteral{5F}{\isacharunderscore}}b{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}bool{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ Take\ eq{\isaliteral{3B}{\isacharsemicolon}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5E}{\isacharcircum}}\isanewline
5.642 \ \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ eq{\isaliteral{5F}{\isacharunderscore}}b\ {\isaliteral{3D}{\isacharequal}}\ \ {\isaliteral{28}{\isacharparenleft}}Substitute\ {\isaliteral{5B}{\isacharbrackleft}}zzz{\isaliteral{3D}{\isacharequal}}z{\isadigit{2}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}\ eq{\isaliteral{5F}{\isacharunderscore}}b{\isaliteral{3B}{\isacharsemicolon}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5E}{\isacharcircum}}\isanewline
5.643 @@ -1578,15 +1647,23 @@
5.644 \ \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}sol{\isaliteral{5F}{\isacharunderscore}}b{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}bool\ list{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}SubProblem\ {\isaliteral{28}{\isacharparenleft}}Isac{\isaliteral{27}{\isacharprime}}{\isaliteral{2C}{\isacharcomma}}{\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{5E}{\isacharcircum}}\isanewline
5.645 \ \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ \ \ \ \ {\isaliteral{5B}{\isacharbrackleft}}univariate{\isaliteral{2C}{\isacharcomma}}equation{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5B}{\isacharbrackleft}}no{\isaliteral{5F}{\isacharunderscore}}met{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{5E}{\isacharcircum}}\isanewline
5.646 \ \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ \ \ {\isaliteral{5B}{\isacharbrackleft}}BOOL\ eq{\isaliteral{5F}{\isacharunderscore}}b{\isaliteral{2C}{\isacharcomma}}\ REAL\ {\isaliteral{28}{\isacharparenleft}}B{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}real{\isaliteral{29}{\isacharparenright}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5E}{\isacharcircum}}\isanewline
5.647 +\ \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}b{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}real{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}rhs{\isaliteral{28}{\isacharparenleft}}NTH\ {\isadigit{1}}\ sol{\isaliteral{5F}{\isacharunderscore}}b{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5E}{\isacharcircum}}\isanewline
5.648 \isanewline
5.649 +\isanewline
5.650 +\ \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ eqr\ {\isaliteral{3D}{\isacharequal}}\ drop{\isaliteral{5F}{\isacharunderscore}}questionmarks\ eqr{\isaliteral{3B}{\isacharsemicolon}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5E}{\isacharcircum}}\isanewline
5.651 \ \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}pbz{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}real{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ Take\ eqr{\isaliteral{3B}{\isacharsemicolon}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5E}{\isacharcircum}}\isanewline
5.652 +\ \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ pbz\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{28}{\isacharparenleft}}Substitute\ {\isaliteral{5B}{\isacharbrackleft}}A{\isaliteral{3D}{\isacharequal}}a{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}\ pbz{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5E}{\isacharcircum}}\isanewline
5.653 +\ \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ pbz\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{28}{\isacharparenleft}}Substitute\ {\isaliteral{5B}{\isacharbrackleft}}B{\isaliteral{3D}{\isacharequal}}b{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}\ pbz{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5E}{\isacharcircum}}\isanewline
5.654 +\isanewline
5.655 +\ \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ pbz\ {\isaliteral{3D}{\isacharequal}}\ Rewrite\ ruleYZ\ False\ pbz{\isaliteral{3B}{\isacharsemicolon}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5E}{\isacharcircum}}\isanewline
5.656 \ \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ pbz\ {\isaliteral{3D}{\isacharequal}}\ drop{\isaliteral{5F}{\isacharunderscore}}questionmarks\ pbz{\isaliteral{3B}{\isacharsemicolon}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5E}{\isacharcircum}}\isanewline
5.657 \isanewline
5.658 -\ \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}pbz{\isadigit{2}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}real{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}Substitute\ {\isaliteral{5B}{\isacharbrackleft}}A{\isaliteral{3D}{\isacharequal}}a{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}\ pbz{\isaliteral{3B}{\isacharsemicolon}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5E}{\isacharcircum}}\isanewline
5.659 +\ \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}iztrans{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}real{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ Take\ pbz{\isaliteral{3B}{\isacharsemicolon}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5E}{\isacharcircum}}\isanewline
5.660 +\ \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ iztrans\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}Rewrite{\isaliteral{5F}{\isacharunderscore}}Set\ inverse{\isaliteral{5F}{\isacharunderscore}}z\ False{\isaliteral{29}{\isacharparenright}}\ iztrans{\isaliteral{3B}{\isacharsemicolon}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5E}{\isacharcircum}}\isanewline
5.661 +\ \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ iztrans\ {\isaliteral{3D}{\isacharequal}}\ drop{\isaliteral{5F}{\isacharunderscore}}questionmarks\ iztrans{\isaliteral{3B}{\isacharsemicolon}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5E}{\isacharcircum}}\isanewline
5.662 +\ \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}n{\isaliteral{5F}{\isacharunderscore}}eq{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}bool{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ Take\ {\isaliteral{28}{\isacharparenleft}}X{\isaliteral{5F}{\isacharunderscore}}n\ {\isaliteral{3D}{\isacharequal}}\ iztrans{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5E}{\isacharcircum}}\ \isanewline
5.663 \isanewline
5.664 -\ \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}real{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ Take\ pbz{\isadigit{2}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5E}{\isacharcircum}}\isanewline
5.665 -\isanewline
5.666 -\ \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ in\ X{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}\ \isanewline
5.667 +\ \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ in\ n{\isaliteral{5F}{\isacharunderscore}}eq{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}\ \isanewline
5.668 \ \ \ \ \ \ {\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
5.669 {\isaliteral{2A7D}{\isacharverbatimclose}}%
5.670 \endisatagML
5.671 @@ -1634,7 +1711,7 @@
5.672 %
5.673 \endisadelimML
5.674 %
5.675 -\isamarkupsubsubsection{Stepwise check the program%
5.676 +\isamarkupsubsubsection{Stepwise check the program\label{sec:stepcheck}%
5.677 }
5.678 \isamarkuptrue%
5.679 %
5.680 @@ -1902,6 +1979,11 @@
5.681 val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}f{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\isanewline
5.682 {\isaliteral{2A7D}{\isacharverbatimclose}}\isanewline
5.683 \isanewline
5.684 +\isacommand{ML}\isamarkupfalse%
5.685 +\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
5.686 +val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}f{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\isanewline
5.687 +val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}f{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\isanewline
5.688 +{\isaliteral{2A7D}{\isacharverbatimclose}}\isanewline
5.689 \isanewline
5.690 \isacommand{ML}\isamarkupfalse%
5.691 \ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline