1.1 --- a/doc-src/isac/jrocnik/bakkarbeit_jrocnik.tex Mon Feb 20 18:31:00 2012 +0100
1.2 +++ b/doc-src/isac/jrocnik/bakkarbeit_jrocnik.tex Wed Mar 07 15:29:02 2012 +0100
1.3 @@ -21,11 +21,12 @@
1.4 \usepackage{longtable}
1.5
1.6 \usepackage{float} %For restylefloat
1.7 -\newfloat{example}{h}{} %self made floats
1.8 +\newfloat{example}{ht}{} %self made floats
1.9 \floatname{example}{Example} %name for float
1.10 \restylefloat{table} %float tables
1.11 \floatstyle{ruled} %boxes around floats
1.12 \restylefloat{example} %float examples --> boxes
1.13 +\restylefloat{figure}
1.14
1.15 %colors and graphics
1.16 \usepackage{graphicx}
1.17 @@ -91,14 +92,14 @@
1.18
1.19 \newevenside
1.20 \begin{abstract}
1.21 -The Baccalaureate Thesis creates interactive course material for Signal Processing (SP) based on the experimental educational math assistant Isabelle/{\sisac} ({\em Isa}belle for Transparent {\em C}alculations in Applied Mathematics).
1.22 -\par The content of the course material is defined together with the Signal Processing and Speech Communication Laboratory (SPSC Lab) of Graz University of Technology (TUG). The content is planned to be used in specific lectures and labs of the SPSC and thus is thoroughly concerned with underlying mathematical and physical theory.
1.23 -One challenge of this thesis is, that much theory required for SPSC is not yet mechanized in Computer Theorem Provers (CTP); so this thesis will provide preliminary definitions and theorems (without proofs~!) implemented in Isabelle \emph{theories}.
1.24 -\par Another challenge is the implementation of interactive courses: this is done within the educational math assistant Isabelle/{\sisac}, which is under development at TU Graz. The present state of {\sisac{}} happens to provide the {\em first} occasion for authoring by a non-member of the {\sisac}-developer team. So this challenge involves alpha-testing of the underlying \emph{CTP-based programming language}, because error messages are still not user-friendly and need frequent contact with {\sisac}-developers.
1.25 +The Baccalaureate Thesis creates interactivee course material for Signal Processing (SP) based on the experimental educational math assistant Isabelle/{\sisac} ({\em Isa}belle for Transparent {\em C}alculations in Applied Mathematics).
1.26 +\par The content of the course material is defined together with the Institute for Signal Processing and Speech Communication (SPSC) of Graz University of Technology (TUG). The content is planned to be used in specific lectures and labs of the SPSC and thus is thoroughly concerned with underlying mathematical and physical theory.
1.27 +One challenge of this thesis is, that much theory required for SPSC is not yet mechanized in Computer Theorem Provers (TP); so this thesis will provide preliminary definitions and theorems (without proofs~!) implemented in Isabelle \emph{theories}.
1.28 +\par Another challenge is the implementation of interactivee courses: this is done within the educational math assistant Isabelle/{\sisac}, which is under development at Austrian Universities, one of them TU Graz. The present state of {\sisac{}} happens to provide the {\em first} occasion for authoring by a non-member of the {\sisac}-developer team. So this challenge involves alpha-testing of the underlying \emph{TP-based programing language}, because error messages are still not user-friendly and need frequent contact with {\sisac}-developers.
1.29 So the practical outcome of this thesis is twofold:
1.30 \begin{enumerate}
1.31 -\item Interactive course material hopefully useful in education within the SPSC Lab and within STEOP, the introductory orientation phase at TUG, as a preview for students in Telematics on later application of math knowledge introduced in the first semester and
1.32 -\item A detailed description of technicalities in programming implemented as an interactive Isabelle/Isar theory, providing future programmers with guidelines and {\sisac}-developers with feedback in usability of the CTP-based program language.
1.33 +\item Interactive course material hopefully useful in education within the SPSC and within \emph{STEOP}\footnote{German: "`Studieneingangs- und Orientierungsphase"'}, the introductory orientation phase at TUG, as a preview for students in Telematics on later application of math knowledge introduced in the first semester and
1.34 +\item A detailed description of technicalities in programing implemented as an interactivee Isabelle/Isar theory, providing future programers with guidelines and {\sisac}-developers with feedback in usability of the CTP-based program language.
1.35 \end{enumerate}
1.36 \end{abstract}
1.37 \clearpage
1.38 @@ -126,63 +127,63 @@
1.39 \part{Project Fundamentals}
1.40
1.41 \section{Introduction}
1.42 -Didactics of mathematics faces a specific issue, a gap between (1) introduction of math concepts and skills and (2) application of these concepts and skills, which ususally are separated into different units in curricula (for good reasons). For instance, (1) teaching partial fraction decomposition is separated from (2) application for inverse Z-transform in signal processing.
1.43 +Didactics of mathematics faces a specific issue, a gap between (1) introduction of math concepts and skills and (2) application of these concepts and skills, which usually are separated into different units in curricula (for good reasons). For instance, (1) teaching partial fraction decomposition is separated from (2) application for inverse Z-transform in signal processing.
1.44
1.45 -This gap is an obstacle for applying math as an foundamental thinking technology in engineering: In (1) motivation is lacking because the question ``What is this stuff good for~?'' cannot be treated sufficiently, and in (2) the ``stuff'' is not available to students in higher semesters as widespread experience shows.
1.46 +This gap is an obstacle for applying math as an fundamental thinking technology in engineering: In (1) motivation is lacking because the question ``What is this stuff good for~?'' cannot be treated sufficiently, and in (2) the ``stuff'' is not available to students in higher semesters as widespread experience shows.
1.47
1.48 \medskip
1.49 Motivated by this didactical issue on the one hand, and ongoing R\&D on a novel kind of educational mathematics assistant at Graz University of Technology~\footnote{http://www.ist.tugraz.at/isac/} promising to cope with this issue on the other hand, several institutes are planning to join their expertise: the Institutes for Institute for Information Systems and Computer Media (IICM), the Institute for Software Technology (IST), the Institutes for Mathematics, the Signal Processing and Speech Communication Institute (SPSC), the Institute for Structural Analysis and the Institute of Electrical Measurement and Measurement Signal Processing.
1.50 -\par This thesis is the first attempt to tackle the above mentioned issue, it focuses on Telematics, because these specific studies focus on mathematics in STEOP, the introductory orientation phase. STEOP is considered an opportunity to investigate the impact of {\sisac}'s prototype on the issue and others.
1.51 +\par This thesis is the first attempt to tackle the above mentioned issue, it focuses on Telematics, because these specific studies focus on mathematics in \emph{STEOP}, the introductory orientation phase. \emph{STEOP} is considered an opportunity to investigate the impact of {\sisac}'s prototype on the issue and others.
1.52
1.53 \medskip
1.54 -The thesis is structured as follows: Part I concerns theory, part II the implementation work, where the latter is the main part.
1.55 +The thesis is structured as follows: Part~I concerns theory and project controlling, Part~II the implementation work, where the latter is the main work, Part~III the resume including summary, open questions and conclusion and the appendixes in Part~IV.
1.56 \par In part I, Section~\ref{isabisac} gives a brief description of the state-of-the-art for educational math assistants (Section~\ref{emas}) and introduces the notions required for the implementation work (Section~\ref{math-auth}). In particular, Section~\ref{user-guid} explains, why math authoring in {\sisac{}} is {\em not} concerned with interaction (and thus not with user guidance etc at all~!). So a concise description of the thesis' goals needs to be postponed to Section~\ref{sec:goals}.
1.57 \par Section~\ref{sp} analyzes a problems defined by the SPSC for the knowledge already provided (Section~\ref{know-isab}, Section~\ref{know-isac}), discusses the selection of problems for implementation (Section~\ref{know-missing}) TODO: further structure ?
1.58 %(\S\ref{})
1.59
1.60 -\section{Mechanization of Math in Isabelle/{\isac}}\label{isabisac}
1.61 +\section{Mechanization of Math in Isabelle/ISAC\label{isabisac}}
1.62
1.63 %\subsubsection*{Notes on Mechanization of Mathematics}
1.64 %This thesis tries to \emph{connect} these two worlds and is one of the first guidelines to implement problem classes in {\sisac}. As we are still in a eary part of development, this is the first thesis dealing within this topic and there is \emph{no} related work to guid through. A more detailed description about this fact can be found in Section \ref{sec:related}.
1.65 -%The major challenge of the practical part, of this thesis, is, that "connecting the two worlds" involves programming in a CTP-based programming language which is in a very early state of prototyping. There is no concrete experience data ready to grep.
1.66 +%The major challenge of the practical part, of this thesis, is, that "connecting the two worlds" involves programing in a CTP-based programing language which is in a very early state of prototyping. There is no concrete experience data ready to grep.
1.67 %
1.68 -As mentioned in the introduction, a prototype of an educational math assistant called {\sisac}\footnote{{\sisac}=\textbf{Isa}belle \cite{Nipkow-Paulson-Wenzel:2002} for \textbf{C}alculations, see http://www.ist.tugraz.at/isac/.} bridges the gap between (1) introducation and (2) application of mathematics: {\sisac} is based on Computer Theorem Proving (CTP), a technology which requires each fact and each action justified by formal logic, so {{\sisac{}}} makes justifications transparent to students in interactive step-wise problem solving. By that way {\sisac} already can serve both:
1.69 +As mentioned in the introduction, a prototype of an educational math assistant called {\sisac}\footnote{{\sisac}=\textbf{Isa}belle \cite{Nipkow-Paulson-Wenzel:2002} for \textbf{C}alculations, see http://www.ist.tugraz.at/isac/.} bridges the gap between (1) introducation and (2) application of mathematics: {\sisac} is based on Computer Theorem Proving (TP), a technology which requires each fact and each action justified by formal logic, so {{\sisac{}}} makes justifications transparent to students in interactivee step-wise problem solving. By that way {\sisac} already can serve both:
1.70 \begin{enumerate}
1.71 \item Introduction of math stuff (in e.g. partial fraction decomposition) by stepwise explaining and exercising respective symbolic calculations with ``next step guidance (NSG)'' and rigorously checking steps freely input by students --- this also in context with advanced applications (where the stuff to be taught in higher semesters can be skimmed through by NSG), and
1.72 -\item Application of math stuff in advanced engineering courses (e.g. problems to be solved by inverse Z-transform in a Signal Processing Lab) --- and now without much ado about basic math techniques (like partical fraction decomposition): ``next step guidance'' supports students in independenly (re-)adopting such techniques.
1.73 +\item Application of math stuff in advanced engineering courses (e.g. problems to be solved by inverse Z-transform in a Signal Processing Lab) --- and now without much ado about basic math techniques (like partial fraction decomposition): ``next step guidance'' supports students in independently (re-)adopting such techniques.
1.74 \end{enumerate}
1.75 -Before the question is answers, how {\sisac} accoplishes this task from a technical point of view, some remarks on the state-of-the-art is given, therefor follow up Section~\ref{emas}.
1.76 +Before the question is answers, how {\sisac} accomplishes this task from a technical point of view, some remarks on the state-of-the-art is given, therefor follow up Section~\ref{emas}.
1.77
1.78 \subsection{Educational Mathematics Assistants (EMAs)}\label{emas}
1.79 -Educational software in mathematics is, if at all, based on Computer Algebra Systems (CAS, for instance \cite{progr-mathematica,prog-maple06}), Dynamic Geometry Systems (DGS, for instance \footnote{GeoGebra http://www.geogebra.org, Cinderella http://www.cinderella.de/, GCLC http://poincare.matf.bg.ac.rs/~janicic/gclc/}) or spread-sheets. These base technologies are used to program math lessons and sometimes even exercises. The latter are cumbersome: the steps towards a solution of such an interactive exercise need to be provided with feedback, where at each step a wide variety of possible input has to be foreseen by the programmer --- so such interactive exercises either require high development efforts or the exercises constrain possible inputs.
1.80 +Educational software in mathematics is, if at all, based on Computer Algebra Systems (CAS, for instance \cite{progr-mathematica,prog-maple06}), Dynamic Geometry Systems (DGS, for instance \footnote{GeoGebra http://www.geogebra.org, Cinderella http://www.cinderella.de/, GCLC http://poincare.matf.bg.ac.rs/~janicic/gclc/}) or spread-sheets. These base technologies are used to program math lessons and sometimes even exercises. The latter are cumbersome: the steps towards a solution of such an interactivee exercise need to be provided with feedback, where at each step a wide variety of possible input has to be foreseen by the programer --- so such interactivee exercises either require high development efforts or the exercises constrain possible inputs.
1.81
1.82 -A new generation of educational math assistants (EMAs) is emerging presently, which is based on Computer Theorem Proving (CTP). CTP, for instance Isabelle \cite{Nipkow-Paulson-Wenzel:2002} and Coq \cite{Huet_all:94}, is a technology which requires each fact and each action justified by formal logic. Pushed by demands for \textit{proven} correctness of safety-critical software CTP advances into software engineering; from these advancements computer mathematics benefits in general, and math education in particular. Two features of CTP are immediately beneficial for learning:
1.83 +A new generation of educational math assistants (EMAs) is emerging presently, which is based on Theorem Proving (TP). TP, for instance Isabelle \cite{Nipkow-Paulson-Wenzel:2002} and Coq \cite{Huet_all:94}, is a technology which requires each fact and each action justified by formal logic. Pushed by demands for \textit{proven} correctness of safety-critical software TP advances into software engineering; from these advancements computer mathematics benefits in general, and math education in particular. Two features of TP are immediately beneficial for learning:
1.84
1.85 -\paragraph{CTP have knowledge in human readable format,} that is in standard predicate calculus. CTP following the LCF-tradition have that knowledge down to the basic definitions of set, equality, etc~\footnote{http://isabelle.in.tum.de/dist/library/HOL/HOL.html}; following the typical deductive development of math, natural numbers are defined and their properties proven~\footnote{http://isabelle.in.tum.de/dist/library/HOL/Number\_Theory/Primes.html}, etc. Present knowledge mechanized in CTP exceeds high-school mathematics by far, however by knowledge required in software technology, and not in other engineering sciences.
1.86 +\paragraph{TP have knowledge in human readable format,} that is in standard predicate calculus. TP following the LCF-tradition have that knowledge down to the basic definitions of set, equality, etc~\footnote{http://isabelle.in.tum.de/dist/library/HOL/HOL.html}; following the typical deductive development of math, natural numbers are defined and their properties proven~\footnote{http://isabelle.in.tum.de/dist/library/HOL/Number\_Theory/Primes.html}, etc. Present knowledge mechanized in TP exceeds high-school mathematics by far, however by knowledge required in software technology, and not in other engineering sciences.
1.87
1.88 -\paragraph{CTP can model the whole problem solving process} in mathematical problem solving {\em within} a coherent logical framework. This is already being done by three projects, by Ralph-Johan Back \cite{Back-SD09}, by ActiveMath \cite{ActiveMath-MAIN11} and by Carnegie Mellon Tutor \cite{mat-tutor-cmu-MAIN11}.
1.89 +\paragraph{TP can model the whole problem solving process} in mathematical problem solving {\em within} a coherent logical framework. This is already being done by three projects, by Ralph-Johan Back \cite{Back-SD09}, by ActiveMath \cite{ActiveMath-MAIN11} and by Carnegie Mellon Tutor \cite{mat-tutor-cmu-MAIN11}.
1.90
1.91 -Having the whole problem solving process within a logical coherent system, such a design guarantees correctness of intermediate steps and of the result (which seems essential for math software); and the second advantage is that CTP provides a wealth of theories which can be exploited for mechanizing other features essential for educational software.
1.92 +Having the whole problem solving process within a logical coherent system, such a design guarantees correctness of intermediate steps and of the result (which seems essential for math software); and the second advantage is that TP provides a wealth of theories which can be exploited for mechanizing other features essential for educational software.
1.93
1.94 \subsection{Generation of User Guidance in EMAs}\label{user-guid}
1.95 One essential feature for educational software is feedback to user input and assistance in coming to a solution.
1.96
1.97 \paragraph{Checking user input} by ATP during stepwise problem solving is being accomplished by the three projects mentioned above \cite{Back-SD09,ActiveMath-MAIN11,mat-tutor-cmu-MAIN11} exclusively. They model the whole problem solving process as mentioned above, so all what happens between formalized assumptions (or formal specification) and goal (or fulfilled postcondition) can be mechanized. Such mechanization promises to greatly extend the scope of educational software in stepwise problem solving.
1.98
1.99 -\paragraph{Next step guidance (NSG)} comprises the system's ability to propose a next step; this is a challenge for CTP: either a radical restriction of the search space by restriction to very specific problem classes is required, or much care and effort is required in designing possible variants in the process of problem solving \cite{proof-strategies-11}.
1.100 +\paragraph{Next step guidance (NSG)} comprises the system's ability to propose a next step; this is a challenge for TP: either a radical restriction of the search space by restriction to very specific problem classes is required, or much care and effort is required in designing possible variants in the process of problem solving \cite{proof-strategies-11}.
1.101
1.102 -Another approach is restricted to problem solving in engineering domains, where a problem is specified by input, precondition, output and postcondition, and where the postcondition is proven by ATP behind the scenes \cite{wn:lucas-interp-12}: Here the possible variants in the process of problem solving are provided with feedback {\em automatically}, if the problem is described in a CTP-based programming language~\cite{plmms10}: the programmer only describes the math algorithm without caring about interaction (the respective program is functional and even has no in/output statements~!); interaction is generated as a side-effect by the interpreter --- an efficient separation of concern between math programmers and dialog designers promising application all over engineering disciplines.
1.103 +Another approach is restricted to problem solving in engineering domains, where a problem is specified by input, precondition, output and postcondition, and where the postcondition is proven by ATP behind the scenes \cite{wn:lucas-interp-12}: Here the possible variants in the process of problem solving are provided with feedback {\em automatically}, if the problem is described in a TP-based programing language~\cite{plmms10}: the programer only describes the math algorithm without caring about interaction (the respective program is functional and even has no in/output statements~!); interaction is generated as a side-effect by the interpreter --- an efficient separation of concern between math programers and dialog designers promising application all over engineering disciplines.
1.104
1.105
1.106 -\subsection{Math Authoring in Isabelle/\isac}\label{math-auth}
1.107 -Authoring new mathematics knowledge in {\sisac} can be compared with ``application programming'' of engineering problems; most of such programming uses CAS-based programming languages (CAS = Computer Algebra Systems; e.g. Mathematica's \cite{progr-mathematica} or Maple's programming language \cite{prog-maple06}).
1.108 +\subsection{Math Authoring in Isabelle/ISAC\label{math-auth}}
1.109 +Authoring new mathematics knowledge in {\sisac} can be compared with ``application programing'' of engineering problems; most of such programing uses CAS-based programing languages (CAS = Computer Algebra Systems; e.g. Mathematica's \cite{progr-mathematica} or Maple's programing language \cite{prog-maple06}).
1.110
1.111 -{\sisac}, however, uses a novel type of CTP-based language \cite{plmms10} for describing how to constuct a solution to an engineering problem and for calling equation solvers, integration, etc~\footnote{Implementation of CAS-like functionality in CTP is not primarily concerned with efficiency, but with a didactic question: What to decide for: for high-brow algorithms at the state-of-the-art or for elementary algorithms comprehensible for students~?} within CTP; CTP can ensure ``systems that never make a mistake'' \cite{casproto} --- are impossible for CAS which have no logics underlying.
1.112 +{\sisac}, however, uses a novel type of TP-based language \cite{plmms10} for describing how to construct a solution to an engineering problem and for calling equation solvers, integration, etc~\footnote{Implementation of CAS-like functionality in TP is not primarily concerned with efficiency, but with a didactic question: What to decide for: for high-brow algorithms at the state-of-the-art or for elementary algorithms comprehensible for students~?} within TP; TP can ensure ``systems that never make a mistake'' \cite{casproto} --- are impossible for CAS which have no logics underlying.
1.113
1.114 -With writing such CTP-based programs authoring is perfect, the application programmer is not concerned with interaction or with user guidance: this is concern of a novel kind of program interpreter called Lucas-Interpreter \cite{wn:lucas-interp-12}. This interpreter hands over control to a dialog component at each step of calculation (like a debugger at breakpoints) and calls automated CTP to check user input following personalized strategies according to a feedback module.
1.115 +With writing such TP-based programs authoring is perfect, the application programer is not concerned with interaction or with user guidance: this is concern of a novel kind of program interpreter called Lucas-Interpreter \cite{wn:lucas-interp-12}. This interpreter hands over control to a dialog component at each step of calculation (like a debugger at breakpoints) and calls automated TP to check user input following personalized strategies according to a feedback module.
1.116
1.117 \medskip
1.118 -However ``application programming with CTP'' is not done with writing a program: according to the principles of CTP, each step must be justified. Such justifications are given by theorems. So all steps must be related to some theorem, if there is no such theorem it must be added to the existing knowledge, which is organized in so-called \textbf{theories} in Isabelle. A theorem must be proven; fortunately Isabelle comprises a mechanism (called ``axiomatization''), which allows to omit proofs. Such a theorem is shown in Example~\ref{eg:neuper1}.
1.119 +However ``application programing with TP'' is not done with writing a program: according to the principles of TP, each step must be justified. Such justifications are given by theorems. So all steps must be related to some theorem, if there is no such theorem it must be added to the existing knowledge, which is organized in so-called \textbf{theories} in Isabelle. A theorem must be proven; fortunately Isabelle comprises a mechanism (called ``axiomatization''), which allows to omit proofs. Such a theorem is shown in Example~\ref{eg:neuper1}.
1.120
1.121 \begin{example}
1.122 {\small\begin{tabbing}
1.123 @@ -200,7 +201,7 @@
1.124 \caption{Axiomatization in Isabelle\label{eg:neuper1}}
1.125 \end{example}
1.126
1.127 -In order to provide CTP with logical facts for checking user input, the Lucas-Interpreter requires a \textbf{specification}. Such a specification is shown in Example~ref{eg:neuper2}.
1.128 +In order to provide TP with logical facts for checking user input, the Lucas-Interpreter requires a \textbf{specification}. Such a specification is shown in Example~\ref{eg:neuper2}.
1.129
1.130 \begin{example}
1.131 {\small\begin{tabbing}
1.132 @@ -232,32 +233,32 @@
1.133 \end{tabbing}
1.134 }
1.135 {\small\textit{
1.136 - \noindent If a programm requires a result which has to be calculated first we can use a subproblem to do so. In our specific case we wanted to calculate the zeros of a fraction and used a subproblem to calculate the zeros of the denominator polynom.
1.137 + \noindent If a program requires a result which has to be calculated first we can use a subproblem to do so. In our specific case we wanted to calculate the zeros of a fraction and used a subproblem to calculate the zeros of the denominator polynom.
1.138 }}
1.139 -\caption{Ussage of Subproblems in Programms\label{eg:subprob}}
1.140 +\caption{Usage of Subproblems in Programs\label{eg:subprob}}
1.141 \end{example}
1.142
1.143
1.144 \subsection{Goals of the Thesis}\label{sec:goals}
1.145 Imagine a piece of software would be able to support you by understanding every problem class, upcoming in the first years attending university - wouldn't it be great?
1.146 -\par {{\sisac{}}} tries to do that, but the current state of the art is miles away from this goal and a single implementation of a problem is not enough to cahnge this circumstamce. Through this fact it is all the more essential to try, test, research and document the implementation of problem classes from "`real world"' applications. Responding to the abstract at the begin of this document the thesis has two folds; on the one hand certainly to provide interactiv course material for Signal Processing (which means to implement a single problem provided by the Institute of Signal Processing and Speech Communication (SPSC); follow up Calulcations), and to extract experience data respectively help the {{\sisac{}}}-team by setting up a detailed description of technicalities hacking {{\sisac{}}} on the other hand.
1.147 +\par {{\sisac{}}} tries to do that, but the current state of the art is miles away from this goal and a single implementation of a problem is not enough to change this circumstance. Through this fact it is all the more essential to try, test, research and document the implementation of problem classes from "`real world"' applications. Responding to the abstract at the begin of this document the thesis has two folds; on the one hand certainly to provide interactivee course material for Signal Processing (which means to implement a single problem provided by the Institute of Signal Processing and Speech Communication (SPSC); follow up Calulcations), and to extract experience data respectively help the {{\sisac{}}}-team by setting up a detailed description of technicalities hacking {\sisac{}} on the other hand.
1.148
1.149 All the notions are in place to describe the task ``Interactive Course Material for Signal Processing based on Isabelle/{\sisac}'', the main task of this thesis, appropriately by the following points:
1.150 \begin{enumerate}
1.151 \item Analyze the problems given by the SPSC Lab for mathematics \textbf{knowledge required}, search the knowledge already available in Isabelle/{\sisac}, estimate efforts required to fill the gap between knowledge required and knowledge available, and finally select problems for implementation accordingly.
1.152 \item Implement the selected problems in Isabelle/{\sisac}, which means, in appropriate Isabelle theories \textbf{for each problem} implement:
1.153 \begin{enumerate}
1.154 - \item \textbf{Definitions and theorems} required within the specification (including ``descriptions'' for input variables and output variables) and the program (proofs omitted via ``axiomaization'')
1.155 + \item \textbf{Definitions and theorems} required within the specification (including ``descriptions'' for input variables and output variables) and the program (proofs omitted via ``axiomatization'')
1.156 \item \textbf{A specification} which describes the input variables, the preconditions on the input (a challenge for rigorously exact mathematics~!), the output variables and the postcondition, which relates input to output such that the problem is characterized formally (another challenge for rigorously exact mathematics~!)
1.157 \item \textbf{A program} describing the algorithm which solves the problem, i.e. which constructs output meeting the postcondition. Programming involves identifying the steps (tactics~!) which create the calculation and calling CAS-functions (simplification, equation solvers, etc) appropriately. Modularization of programs into {\tt SubProblems} has to prepare for re-use of code.
1.158 \end{enumerate}
1.159 -\item Add \textbf{multimedia explanations} to each problem (i.e. to specific definitions, theorems, the specification and the program) such that non-expert students (e.g. within STEOP, the introductory orientation phase at TUG) get an idea the problem is about.
1.160 +\item Add \textbf{multimedia explanations} to each problem (i.e. to specific definitions, theorems, the specification and the program) such that non-expert students (e.g. within \emph{STEOP}, the introductory orientation phase at TUG) get an idea the problem is about.
1.161 \item \textbf{Document the implementation} such that
1.162 \begin{enumerate}
1.163 - \item Interactive course material hopefully useful in education within the SPSC and within STEOP, the introductory orientation phase at TUG, as a preview for students in Telematics on later application of math knowledge introduced in the first semester and
1.164 - \item A detailed description of technicalities in programming implemented as an interactive Isabelle/Isar theory, providing future programmers with guidelines and {\sisac}-developers with feedback in usability of the CTP-based program language.
1.165 - \item subsequent application programmers have guidelines for further implementation of interactive course material in SPSC and other engineering sciences
1.166 - \item {\sisac{}} developers get feedback for ongoing improvement of the CTP-based programming language, the respective development environment and the respective program interpreter (called Lucas-Interpreter)
1.167 + \item Interactive course material hopefully useful in education within the SPSC and within \emph{STEOP}, the introductory orientation phase at TUG, as a preview for students in Telematics on later application of math knowledge introduced in the first semester and
1.168 + \item A detailed description of technicalities in programing implemented as an interactivee Isabelle/Isar theory, providing future programers with guidelines and {\sisac}-developers with feedback in usability of the TP-based program language.
1.169 + \item subsequent application programers have guidelines for further implementation of interactivee course material in SPSC and other engineering sciences
1.170 + \item {\sisac{}} developers get feedback for ongoing improvement of the TP-based programing language, the respective development environment and the respective program interpreter (called Lucas-Interpreter)
1.171 \item development of knowledge for engineering sciences is being motivated in the Isabelle community.
1.172 \end{enumerate}
1.173 \end{enumerate}
1.174 @@ -265,39 +266,38 @@
1.175
1.176 \section{Mechanization of Signal Processing Problems}\label{sp}
1.177 \subsection{Relevant Knowledge available in Isabelle}\label{know-isab}
1.178 -Isabelle is developed now for a long time and so we are able to access a huge range of theories and usefull snipsets. The main problem according this snipsets is that isabelle still is a theorem proofer and not an algebra system. But due the work of the {\sisac}-development team there are already also many calculation examples provided.
1.179 -\par The SPSC provided a list of problems which are often done wrong or are missunderstood by studentsin term of the problem classes. Out of these tasks we tried to extract the core operations and looked up which parts are already implemented or usefull. The provided problems are:
1.180 +Isabelle is developed now for a long time and so we are able to access a huge range of theories and useful snippets. The main problem according this snip sets is that isabelle still is a theorem proofer and not an algebra system. But due the work of the {\sisac}-development team there are already also many calculation examples provided.
1.181 +\par The SPSC provided a list of problems which are often done wrong or are misunderstood by students in term of the problem classes. Out of these tasks we tried to extract the core operations and looked up which parts are already implemented or useful. The provided problem classes are:
1.182 \begin{itemize}
1.183 -\item Fourier-Transformation
1.184 -\item Convolution
1.185 -\item Inverse z-Transformation and partial fraction decomposition
1.186 -\item Indextransformation
1.187 + \item Fourier-Transformation
1.188 + \item Convolution
1.189 + \item Inverse Z-Transformation and partial fraction decomposition
1.190 + \item Index transformation
1.191 \end{itemize}
1.192 -Following the collection and evaluation of core operations collated with isabelle:
1.193
1.194 -\paragraph{example FFT}, describe in detail !!!!
1.195 +A survey of these selected Problems on their "`correct"' solution can be found in Appendix~\ref{app:calc}. After manually solving this problems we started checking which of them are able to realizable. As already remarked above, isabelle is just a theorem proover due this fact isabelle only provides some theories which are useful for the provided problem classes.
1.196 +\par Yet, isabelle also has some problems on traditional notation. For example a theory called FFT is already implemented this theory does not provide methods for solving fourier transformation tasks, it only defines the basic condition a fast Fourier transformed expression has to fulfill.
1.197 +\par For the problems we had a look-on isabelle did not provide specific theories which can be implemented one by one, so a look at the mechanized knowledge in {\sisac} is the next step, therefore follow up Section~\ref{know-isac}.
1.198
1.199 -? different meaning: FFT in Maple
1.200 +\subsection{Relevant Knowledge available in ISAC}\label{know-isac}
1.201 +{\sisac} already provides a small registry of useful programs and surveys on using isabelle as for solving problems. These snip sets are things like norming rational numbers, solving variate and univariate equations, substitutions, some simple integrals and so on. For a detailed review on the currently implemented theories a look at the {\sisac} project web-page\footnote{http://www.ist.tugraz.at/projects/isac/www/kbase/pbl/index\_pbl.html} is strongly recommended, as the appreciation for this thesis is no describing all parts of {\sisac} in detail. This would also not be possible as {\sisac} is permanently growing.
1.202 +\par After we differenced {\sisac} and isabelle we are able to introduce two axes in the project. This axes are the specifications (``application axis'' represented as isabelle) and methods (``algorithmic axis'' represented as {\sisac}).
1.203 +\par During the first weeks of work on this thesis we decided on implementing the Z-Transformation and particullary the included partial fraction decomposion first. The algoritmix axis therefor already provides the knowledge for the following parts:
1.204 +\begin{description}
1.205 +\item[Partial Fractions] We now how to handle them and we are able to illustrate them.
1.206 +\item[Cancellation of multivariate rational terms] Simplification is possible.
1.207 +\item[Equations] The possibility of solving linear and second order equations is provided, also the possibility to get the left or right hand side of an equation.
1.208 +\item[Substitution] We are able to substitute given variables in terms, we are also able to subsitude a list of variables in terms.
1.209 +\end{description}
1.210
1.211 -gap between what is available and what is required (@)!
1.212 -
1.213 -traditional notation ?
1.214 -
1.215 -\subsection{Relevant Knowledge available in isac}\label{know-isac}
1.216 -todo
1.217 -
1.218 -specifications (``application axis'') and methods (``algorithmic axis'')
1.219 -
1.220 -partial fractions, cancellation of multivariate rational terms, ...
1.221 -
1.222 -\subsection{Survey: Requiered Knowledge and Selected Problem(s)}\label{know-missing}
1.223 -Following tables (Table~\ref{tab:eff-four},~\ref{tab:eff-conv},~\ref{tab:eff-ztrans}) are showing the expected development effort for speciefic problems. The values are only very inaccurately approximations of the real work, but needed as a basis for descieding with which problem to start:
1.224 +\subsection{Survey on Required Knowledge}\label{know-missing}
1.225 +Following tables (Table~\ref{tab:eff-four},~\ref{tab:eff-conv},~\ref{tab:eff-ztrans}) are showing the expected development effort for specific problems. The values are only very inaccurately approximations of the real work, but needed as a basis for descieding with which problem to start:
1.226
1.227 \begin{table}
1.228 \centering
1.229 \begin{tabular}{p{4cm}|p{5cm}|rp{2.5cm}}
1.230 - \textbf{Requirements} & \textbf{Comments} &\textbf{Effort}\\ \hline\hline
1.231 - solving Intrgrals & simple via propertie table & 20\\
1.232 + \textbf{Requirements} & \textbf{Comments} &\textbf{Effort}\\ \hline\hline
1.233 + solving Integrals & simple via properties table & 20\\
1.234 & \emph{real} & MT\\ \hline
1.235 transformation table & simple transform & 20\\ \hline
1.236 visualisation & backend & 10\\ \hline
1.237 @@ -312,8 +312,8 @@
1.238 \begin{table}
1.239 \centering
1.240 \begin{tabular}{p{4cm}|p{5cm}|rp{2.5cm}}
1.241 - \textbf{Requirements} & \textbf{Comments} &\textbf{Effort}\\ \hline\hline
1.242 - simplify rationals & {\sisac} & 0\\ \hline
1.243 + \textbf{Requirements} & \textbf{Comments} &\textbf{Effort}\\ \hline\hline
1.244 + simplify rationals & {\sisac} & 0\\ \hline
1.245 define $\sum\limits_{i=0}^{n}i$ & partly {\sisac} & 10\\ \hline
1.246 simplify sum & termorder & 10\\
1.247 & simplify rules & 20\\
1.248 @@ -329,89 +329,95 @@
1.249 \begin{table}
1.250 \centering
1.251 \begin{tabular}{p{4cm}|p{5cm}|rp{2.5cm}}
1.252 - \textbf{Requirements} & \textbf{Comments} &\textbf{Effort}\\ \hline\hline
1.253 - solve for part.fract. & {\sisac}: degree 2 & 0\\
1.254 + \textbf{Requirements} & \textbf{Comments} &\textbf{Effort}\\ \hline\hline
1.255 + solve for part.fract. & {\sisac}: degree 2 & 0\\
1.256 & complex nomminators & 30\\
1.257 & degree > 2 & MT\\ \hline
1.258 - simplify polynomial & {\sisac} & 0\\
1.259 - simplify rational & {\sisac} & 0\\ \hline
1.260 + simplify polynomial & {\sisac} & 0\\
1.261 + simplify rational & {\sisac} & 0\\ \hline
1.262 partial fraction & degree 2, & 20\\
1.263 decomposition & specification, method& 30\\ \hline
1.264 ${\cal Z}^{-1}$ table & explanations, figures& 20\\ \hline
1.265 example collection & with explanations & 20\\ \hline\hline
1.266 - \multicolumn{2}{c|}{} & 90-120\\
1.267 + \multicolumn{2}{c|}{} & 90-120\\
1.268 \end{tabular}
1.269
1.270 \caption{Z-Transformation development effort\label{tab:eff-ztrans}}
1.271 \end{table}
1.272
1.273 -As conclusion of the summerized efforts it is evident that only one topic can be tried to realized as a baccalaureate thesis. In accord with Dr. Neuper we decided after some practical tests to start with the implementation of the (Inverse) Z-Transformation. The Reason is that this topic can mostly be done with knowledge which was already tried to be mechanized in {\sisac}.
1.274 +As conclusion of the summarized efforts it is evident that only one topic can be tried to realized as a baccalaureate thesis. In accord with Dr. Neuper we decided after some practical tests to start with the implementation of the (Inverse) Z-Transformation. The Reason is that this topic can mostly be done with knowledge which was already tried to be mechanized in {\sisac}.
1.275
1.276 \subsection{Formalization of missing knowledge in Isabelle}
1.277
1.278 -A problem behind is the mechanization of mathematic theories in CTP-bases languages. There is still a huge gap between these algoritms and this what we want as a solution - in Example Signal Processing.
1.279 +A problem behind is the mechanization of mathematic theories in TP-bases languages. There is still a huge gap between these algorithms and this what we want as a solution - in Example Signal Processing.
1.280 \begin{example}
1.281 \[
1.282 X\cdot(a+b)+Y\cdot(c+d)=aX+bX+cY+dY
1.283 \]
1.284 {\small\textit{
1.285 - \noindent A very simple example on this what we call gap is the simplification above. It is needles to say that it is correct and also isabell forfills it correct - \emph{always}. But sometimes we don't want expand such terms, sometimes we want another structure of them. Think of a problem were we now would need only the coefficients of $X$ and $Y$. This is what we call the gap between mechanical simplification and the solution.
1.286 + \noindent A very simple example on this what we call gap is the simplification above. It is needles to say that it is correct and also Isabelle for fills it correct - \emph{always}. But sometimes we don't want expand such terms, sometimes we want another structure of them. Think of a problem were we now would need only the coefficients of $X$ and $Y$. This is what we call the gap between mechanical simplification and the solution.
1.287 }}
1.288 - \caption{Correct but not usefull}\label{eg:gap}
1.289 + \caption{Correct but not useful}\label{eg:gap}
1.290 \end{example}
1.291 Until we are not able to fill this gap we have to live with it but first have a look on the meaning of this statement:
1.292 -\par Mechanized math starts from mathematical models and \emph{hopefully} proceeds to match physics. Academic engineering starts from physics (experimentation, measurement) and then proceeds to mathematical modelling and formalization. The process from a physical observance to a mathematical theory is unavoidable bound of setting up a big collection of standards, rules, definition but also exceptions. These are the things making mechanization that difficult.
1.293 +\par Mechanized math starts from mathematical models and \emph{hopefully} proceeds to match physics. Academic engineering starts from physics (experimentation, measurement) and then proceeds to mathematical modeling and formalization. The process from a physical observance to a mathematical theory is unavoidable bound of setting up a big collection of standards, rules, definition but also exceptions. These are the things making mechanization that difficult.
1.294 \begin{example}
1.295 \[
1.296 m,\ kg,\ s,\ldots
1.297 \]
1.298 {\small\textit{
1.299 - \noindent Think about some units like that one's above. Behind each unit there is a discerning and very accurate definition: One Meter is the distance the light travels, in a vacuum, through the time of 1 / 299.792.458 second; one kilogramm is the weight of a platinum-iridium cylindar in paris; and so on. But are these definitions useable in a computer mechanized world?!
1.300 + \noindent Think about some units like that one's above. Behind each unit there is a discerning and very accurate definition: One Meter is the distance the light travels, in a vacuum, through the time of 1 / 299.792.458 second; one kilogram is the weight of a platinum-iridium cylinder in paris; and so on. But are these definitions usable in a computer mechanized world?!
1.301 }}
1.302 \caption{Units in measurement}\label{eg:units}
1.303 \end{example}
1.304 -\par A computer or a CTP-System builds on programms witth predefined logical ruels and does not know any mathematical trick (follow up example \ref{eg:trick}) or recipe to walk around difficult expressions.
1.305 +\par A computer or a TP-System builds on programs with predefined logical rules and does not know any mathematical trick (follow up example \ref{eg:trick}) or recipe to walk around difficult expressions.
1.306 \begin{example}
1.307 \[ \frac{1}{j\omega}\cdot\left(e^{-j\omega}-e^{j3\omega}\right)= \]
1.308 \[ \frac{1}{j\omega}\cdot e^{-j2\omega}\cdot\left(e^{j\omega}-e^{-j\omega}\right)=
1.309 \frac{1}{\omega}\, e^{-j2\omega}\cdot\colorbox{lgray}{$\frac{1}{j}\,\left(e^{j\omega}-e^{-j\omega}\right)$}= \]
1.310 \[ \frac{1}{\omega}\, e^{-j2\omega}\cdot\colorbox{lgray}{$2\, sin(\omega)$} \]
1.311 {\small\textit{
1.312 - \noindent Sometimes it is also usefull to be able to apply some \emph{tricks} to get a beautiful and particulary meaningful result, which we are able to interpret. But as seen in this example it can be hard to find out what operations have to be done to transform a result into a meaningful one.
1.313 + \noindent Sometimes it is also useful to be able to apply some \emph{tricks} to get a beautiful and particularly meaningful result, which we are able to interpret. But as seen in this example it can be hard to find out what operations have to be done to transform a result into a meaningful one.
1.314 }}
1.315 \caption{Mathematic tricks}\label{eg:trick}
1.316 \end{example}
1.317 -For such a system the only possibility is to work through its known definitions and stops if none of these fits. Specified on Signal Processing or any other application it is often possible to walk through by doing simple creases. This creases are in generell based on simple math operatiopms but the challange is to teach the machine \emph{all}\footnote{Its pride to call it \emph{all}.} of them. Unfortunataly the goal of CTP Isabelle is to reach a high level of \emph{all} but it in real it will still be a survey of knowledge which links to other knowledge and {{\sisac{}}} a trainer and helper but no human compensating calulator.
1.318 -\par {{\sisac{}}} itselfs aims to adds an \emph{application} axis (formal specifications of problems outof topics from Signal Processing, etc.) and an \emph{algorithmic} axis to the \emph{deductive} axis of physical knowledge. The result is a three-dimensional universe of mathematics.
1.319 +For such a system the only possibility is to work through its known definitions and stops if none of these fits. Specified on Signal Processing or any other application it is often possible to walk through by doing simple creases. This creases are in generell based on simple math operatiopms but the challenge is to teach the machine \emph{all}\footnote{Its pride to call it \emph{all}.} of them. Unfortunately the goal of TP Isabelle is to reach a high level of \emph{all} but it in real it will still be a survey of knowledge which links to other knowledge and {\sisac{}} a trainer and helper but no human compensating calculator.
1.320 +\par {{\sisac{}}} itself aims to adds an \emph{application} axis (formal specifications of problems out of topics from Signal Processing, etc.) and an \emph{algorithmic} axis to the \emph{deductive} axis of physical knowledge. The result is a three-dimensional universe of mathematics seen in Figure~\ref{fig:mathuni}.
1.321
1.322 -
1.323 -
1.324 -todo
1.325 -
1.326 -axiomatization ... where ... and
1.327 +\begin{figure}
1.328 +\hfill \\
1.329 + \begin{center}
1.330 + \includegraphics[scale=0.7]{math-universe}
1.331 + \end{center}
1.332 + \caption{Three-dimensional universe of mathematics\label{fig:mathuni}}
1.333 +\end{figure}
1.334
1.335 \subsection{Notes on Problems with Traditional Notation}
1.336 -%{\footnotesize
1.337 -%\textbf{TODO}
1.338 -%Due the thesis work we discorvers severell problems of traditional notations.
1.339 -%
1.340 -%u[n] !!
1.341 -%
1.342 -%f x = why not f(x) ?!?!
1.343 -%
1.344 -%...
1.345 -%
1.346 -%terms are not full simplified in traditional notations, in isac we have to simplify them complete to check weather results are compatible or not. in e.g. the solutions of an second order linear equation is an rational in isac but in tradition we keep fractions as long as possible and as long as they are 'beautiful' (1/8, 5/16,...)
1.347 -%}\\
1.348 +Due the thesis work we discovers sever ell problems of traditional notations. Some of them have been known in computer science for many years now and are still unsolved, one of them aggregates with the so called \emph{Lambda Calculus}, Example~\ref{eg:lamda} provides a look on the problem that embarrassed us.
1.349
1.350 -The math which should be mechanized in Computer Theorem Provers (\emph{CTP}) has (almost) a problem with traditional notations (predicate calculus) for axioms, definitions, lemmas, theorems as a computer programm or script is not able to interpret every greek or latin letter and every greek, latin or whatever calculations symbol. Also if we would be able to handle thehse symbols we still have a problem to interpret them at all. (Follow up \hbox{Example \ref{eg:symbint1}})
1.351 +\begin{example}
1.352 +
1.353 +\[ f(x)=\ldots\; \quad R \rightarrow \quad R \]
1.354 +
1.355 +
1.356 +\[ f(p)=\ldots\; p \in \quad R \]
1.357 +
1.358 + {\small\textit{
1.359 + \noindent Above we see two equations. The first equation aims to be a mapping of an function from the reell range to the reell one, but when we change only one letter we get the second equation which usually aims to insert a reel point $p$ into the reell function. In computer science now we have the problem to tell the machine (TP) the difference between this two notations. This Problem is called Lambda Calculus.
1.360 + }}
1.361 + \caption{Towards the Lambda Calculus\label{eg:lamda}}
1.362 +\end{example}
1.363 +
1.364 +An other problem is that terms are not full simplified in traditional notations, in {\sisac} we have to simplify them complete to check weather results are compatible or not. in e.g. the solutions of an second order linear equation is an rational in {\sisac} but in tradition we keep fractions as long as possible and as long as they aim to be 'beautiful' (1/8, 5/16,...).
1.365 +
1.366 +The math which should be mechanized in Computer Theorem Provers (\emph{TP}) has (almost) a problem with traditional notations (predicate calculus) for axioms, definitions, lemmas, theorems as a computer program or script is not able to interpret every Greek or Latin letter and every Greek, Latin or whatever calculations symbol. Also if we would be able to handle these symbols we still have a problem to interpret them at all. (Follow up \hbox{Example \ref{eg:symbint1}})
1.367
1.368 \begin{example}
1.369 \[
1.370 u\left[n\right] \ \ldots \ unitstep
1.371 \]
1.372 {\small\textit{
1.373 - \noindent The unitstep is something we need to solve Signal Processing problem classes. But in {{\sisac{}}} the rectangular breakets have a different meaning. So we abuse them for our requirements. We get something which is not defined, but useable. The Result is syntax only without semantic.
1.374 + \noindent The unitstep is something we need to solve Signal Processing problem classes. But in {{\sisac{}}} the rectangular brackets have a different meaning. So we abuse them for our requirements. We get something which is not defined, but usable. The Result is syntax only without semantic.
1.375 }}
1.376 \caption{Expression Interpretation}\label{eg:symbint1}
1.377 \end{example}
1.378 @@ -426,13 +432,13 @@
1.379 }}
1.380 \caption{Symbol Interpretation}\label{eg:symbint2}
1.381 \end{example}
1.382 -Exclusive from the input, also the output can be a problem. We are familar with a specified notations and style taught in university but a computer programm has no knowledge of the form probved by a professor and the maschines themselve also have not yet the possibilities to print every symbol (correct) Recent developments provide proofs in a humand readable format but according to the fact that there is no mony for good working formel editors yet, the style is one thing we have to live with.
1.383 +Exclusive from the input, also the output can be a problem. We are familiar with a specified notations and style taught in university but a computer program has no knowledge of the form proved by a professor and the machines themselves also have not yet the possibilities to print every symbol (correct) Recent developments provide proofs in a human readable format but according to the fact that there is no money for good working formel editors yet, the style is one thing we have to live with.
1.384
1.385 \section{Project Controlling}
1.386 -We decided to split the thesis into five Iteration defined in Section~\ref{sec:milesurv}. As there is also a lot of work todo outer the thesis we accord on an increased contact by mail. For the coordination of the whole {\sisac} files i got access to the mercurial repository. We also appointed on periodic team meetings.
1.387 +We decided to split the thesis into five Iteration defined in Section~\ref{sec:milesurv}. As there is also a lot of work to do outer the thesis we accord on an increased contact by mail. For the coordination of the whole {\sisac} files i got access to the mercurial repository. We also appointed on periodic team meetings.
1.388
1.389 -\subsection{Survay on Milestones\label{sec:milesurv}}
1.390 -Doing something completly new requires a good controlling, the thesis itself also needs it. After the first meetings and the definition of the intrinsic work we decided on splitting the thesis into the following iterations.
1.391 +\subsection{Survey on Milestones\label{sec:milesurv}}
1.392 +Doing something completely new requires a good controlling, the thesis itself also needs it. After the first meetings and the definition of the intrinsic work we decided on splitting the thesis into the following iterations.
1.393 \begin{description}
1.394 \item[1st Iteration] Information Collection
1.395 \item[2nd Iteration] Problem Selection
1.396 @@ -444,11 +450,11 @@
1.397
1.398 \subsection{Milestone Details\label{sec:detmile}}
1.399 \begin{description}
1.400 - \item[Information Collection] The first iteration starts by an intruduction to the {\sisac} System and ends up with the first presentation. Listeners of the first presentation were \em Dr. Walther Neuper \normalfont and \em DI Bernhard Geiger\normalfont. We talked about common SPSC problems and the possibilities of realize them in the {\sisac} System. In preparation of the Presentation \em DI Geiger \normalfont sent us a few example problems and we had a experimental survay about the realization effort.
1.401 - \item[Problem Selection] In the second iteration we collected informations about the knowledge mechanized in {\sisac} (cf. Section~\ref{know-isab}). After the first iteration it was clear that implementing of problems in {\sisac} requires a higher effort than originally excpected due this fact the second iteration ends up on the decission which of the provided problems is going to be implemented. We wrote and collected a handfull of experimental scripts regarding sums, fourie transformation and partial fraction decomposition.
1.402 - \item[Implementation] Unfortunataly the biggest and most importent part is the implementation. The iteration started with the decission on the problem and ends up by finishing the test Script (seen in Part~\ref{part:impl}) as well as the integration of this work into the {\sisac}-Knowledge. For a better controlling and result of this iteration we had severell regular meetings (\em Dr. Neuper \normalfont and \em Jan Rocnik\normalfont) and contact over e-mail to assess the state of the {\sisac}-developers work.
1.403 - \item[Thesis Writing] One part of this thesis is generated automatically out of \ttfamily Build\_Inverse\_Z\_Transform\normalfont. Maybe this part well be the most important result of the thesis as it will be used as a documentation for the upcoming developers. Due this fact this iteration started also contemporaneous with the implementation but ends up seperate after finishing the implementation with describing the needed theory and background.
1.404 - \item[Finalization] The work ends up with the last iteration - finalization. It is started by completing the written thesis and the preperation of the second presentation which concludes this project. In the second presentation we will have demonstrated our realised problem embedded in the new {\sisac}-frontend as well as the work, hiding behind. We will also want to give a clear view about the power of {\sisac} and animate the attending agents to go on working within this project.
1.405 + \item[Information Collection] The first iteration starts by an introduction to the {\sisac} System and ends up with the first presentation. Listeners of the first presentation were \em Dr. Walther Neuper \normalfont and \em DI Bernhard Geiger\normalfont. We talked about common SPSC problems and the possibilities of realize them in the {\sisac} System. In preparation of the Presentation \em DI Geiger \normalfont sent us a few example problems and we had a experimental survey about the realization effort.
1.406 + \item[Problem Selection] In the second iteration we collected informations about the knowledge mechanized in {\sisac} (cf. Section~\ref{know-isab}). After the first iteration it was clear that implementing of problems in {\sisac} requires a higher effort than originally expected due this fact the second iteration ends up on the decision which of the provided problems is going to be implemented. We wrote and collected a handful of experimental scripts regarding sums, Fourier transformation and partial fraction decomposition.
1.407 + \item[Implementation] Unfortunately the biggest and most important part is the implementation. The iteration started with the decision on the problem and ends up by finishing the test Script (seen in Part~\ref{part:impl}) as well as the integration of this work into the {\sisac}-Knowledge. For a better controlling and result of this iteration we had severe ll regular meetings (\em Dr. Neuper \normalfont and \em Jan Ro\v{c}nik\normalfont) and contact over e-mail to assess the state of the {\sisac}-developers work.
1.408 + \item[Thesis Writing] One part of this thesis is generated automatically out of \ttfamily Build\_Inverse\_Z\_Transform\normalfont. Maybe this part well be the most important result of the thesis as it will be used as a documentation for the upcoming developers. Due this fact this iteration started also contemporaneous with the implementation but ends up separate after finishing the implementation with describing the needed theory and background.
1.409 + \item[Finalization] The work ends up with the last iteration - finalization. It is started by completing the written thesis and the preparation of the second presentation which concludes this project. In the second presentation we will have demonstrated our realized problem embedded in the new {\sisac}-frontend as well as the work, hiding behind. We will also want to give a clear view about the power of {\sisac} and animate the attending agents to go on working within this project.
1.410 \end{description}
1.411
1.412 %\clearpage
1.413 @@ -459,50 +465,215 @@
1.414
1.415 \part{Implementation\label{part:impl}}
1.416 \input{./preambleForGeneratedDocuments.tex}
1.417 +\par Please be aware that this is only a part of the thesis output, also follow up the theories and according tests that have been improved or created by me and are involved to the work on this thesis:
1.418 +\begin{itemize}
1.419 +\item \ttfamily Partial\_Fractions.thy \normalfont - \ttfamily partial\_fractions.sml \normalfont
1.420 +\item \ttfamily Inverse\_Z\_Transformation.thy \normalfont - \ttfamily inverse\_z\_transformation.sml \normalfont
1.421 +\item \ttfamily Rational.thy \normalfont - \ttfamily rational.sml \normalfont
1.422 +\end{itemize}
1.423 \HRule
1.424 %\setcounter{section}{0}
1.425 \input{../../../test/Tools/isac/ADDTESTS/course/SignalProcess/document/Build_Inverse_Z_Transform}
1.426
1.427 -%\clearpage
1.428 +\clearpage
1.429
1.430 %----------// PART 3 \\----------%
1.431
1.432 \newevenside
1.433 -\part{Summary, Conclusion and Related Work}
1.434 +\part{Thesis Summary and Review}
1.435 \section{Related Work}\label{sec:related}
1.436 Unusual for a Baccalaureate Thesis, there is {\em no} related work; this requires explanation.
1.437 -Of course, this thesis relies on front-of-the wave computer mathematics, on CTP. But {{\sisac{}}} uses CTP in a very specific way, which is too weakly related to other work: programming in the CTP-based language and rigorous formal specification of problems in Signal Processing where the main tasks in the practical part of this thesis. The major challenge for the practical work was given by the fact, that the work concerned alpha-testing of the CTP-based programming environment.
1.438 -\par Another area of work could be considered as related work: authoring of e-learning content. However, {{\sisac{}}} provides division of concern such that the practical part of this thesis could focus on computer mathematics; this work was not concerned with interaction (the CTP-based programming language has neither input statements nor output statements), nor with dialog guidance nor with any kind of learning theory.
1.439 +Of course, this thesis relies on front-of-the wave computer mathematics, on TP. But {{\sisac{}}} uses TP in a very specific way, which is too weakly related to other work: programing in the TP-based language and rigorous formal specification of problems in Signal Processing where the main tasks in the practical part of this thesis. The major challenge for the practical work was given by the fact, that the work concerned alpha-testing of the TP-based programing environment.
1.440 +\par Another area of work could be considered as related work: authoring of e-learning content. However, {{\sisac{}}} provides division of concern such that the practical part of this thesis could focus on computer mathematics; this work was not concerned with interaction (the TP-based programing language has neither input statements nor output statements), nor with dialog guidance nor with any kind of learning theory.
1.441 \par These two reasons are given for the unusual statement, that there is no related work to be discussed in this thesis.
1.442
1.443 -\section{Summary}
1.444 -todo
1.445 -\section{Open Questions}
1.446 -todo
1.447 -\section{Conclusions}
1.448 -todo
1.449 +\section{Issues and Open Questions}
1.450 +At the end of the first Iteration we agreed on a view issues that might have to be accomplished during the thesis. This Issues were:
1.451 +\begin{itemize}
1.452 + \item What knowledge is already mechanized in \emph{Isabelle}?
1.453 + \item How can missing theorems and definitions be mechanized?
1.454 + \item What is the effort for such mechanization?
1.455 + \item How do calculations look like, by using mechanized knowledge?
1.456 + \item What problems and subproblems have to be solved?
1.457 + \item Which problems are already implemented in {\sisac}?
1.458 + \item How are the new problems specified ({\sisac})?
1.459 + \item Which variants of programs in {\sisac} solve the problems?
1.460 + \item What is the contents of the interactive course material (Figures, etc.)?
1.461 +\end{itemize}
1.462 +The significant part of this list was declared during the thesis. Next sections will review the most important items, regardless they where accomplished or not.
1.463 +
1.464 +\subsection{Accomplished}
1.465 +We discovered the process how missing theorems and definitions can be mechanized and used this knowledge to implement new material. Now we ware able to solve partial fractions, we built theorems, specification and program. We completed the background work for interactive solving them. The same thing applies to the inverse Z-transformation with partial fractions; we built theorems, specification and program to step through an amount of exercises. But the most important accomplished part is the Isabelle theory (\ttfamily Build\_Inverse\_Z\_Transform.thy\normalfont) indicating issues for the coming {\sisac}-developers. Until we were not able to fulfill all the things we wanted, this is the most recent work and will be the headstone for the further work on {\sisac}.
1.466 +\par Expect the necessary theories for solving the mentioned part and the guideline we also put tests for the new theories to the system and added some new methods to existing theories with their according tests. Also we were able to answer the questions about the mechanized knowledge in \emph{isabelle} and {\sisac}. We checked the required effort to add new material to the system and we walked through the question what subproblems have to be solved and how they are declared, when adding new material. Now we also know how problems are declared and which variants exist to solve them. All this can be found in this thesis.
1.467 +\subsection{Partially Accomplished}
1.468 +As already told upwards, we accomplished a guideline for upcoming {\sisac}-developers this was a very important and necessary task; but through upcoming changes in the development environment and programing language there is a need for more descriptions and informations. This changes are not yet fulfilled and so it was not possible to include a correct guideline fot them in our example theory or this thesis.
1.469 +\par Also we were not able to provide a representative count of example problems for partial fractions or the inverse Z-Transformation. We are able to say that our accomplished material can handle one problem each, exactly as we wanted and it is toughed but due to less time we have no more experience data.
1.470 +\subsection{Not Accomplished}
1.471 +The properly longest item is the list with the not accomplished issues, but there is no need to count this as a negative aspect due the fact that we collected experience data for following needs:
1.472 +\par We were not able to put explanations, figures to examples, theorem descriptions and problem description to our course material. The reason for that was the time at one side and the ongoing restructuration of the system on the other side.
1.473 +\par Only a sufficient number of topics was implemented. There were more problems to solve than we expected. We were only able to implement one from the SPSC given tasks m entered in Appendix~\ref{app:calc}. Due this fact the material we got as an output of the thesis will be no support for labs or lectures at the SPSC and also no material for the STEOP, which also was a big wish at the beginning.
1.474 +\subsection{Open Questions and Work}
1.475 +At the end of this thesis there is now part left unattended, but many parts that require beauty corrections and many parts that require a few more manpower. This upcoming open tasks are:
1.476 +\begin{itemize}
1.477 + \item What is the contents of the interactive course material (Figures, etc.)?
1.478 + \item What are the pre and post conditions of the problems?
1.479 + \item How would a correct implementation of the Z-Transformation look like?
1.480 + \item What do students expect of this implementation?
1.481 +\end{itemize}
1.482 +To complete the task of creating course material describing the needed steps to do a partial fraction or inverse Z-Transformation in {\sisac} the real effort is not conceivable. But for a first usable version only a few steps are left to do this steps would be:
1.483 +\begin{enumerate}
1.484 + \item Cleanup the\ttfamily InverseZTransformation.thy\normalfont file and put it into the {\sisac} knowledge tree like it was done with\ttfamily PartialFractions.thy\normalfont.
1.485 + \item Create a good example program and test it.
1.486 + \item Describe the used theories with the mathematic definitions and background.
1.487 + \item Add figures and small examples.
1.488 +\end{enumerate}
1.489 +There are also needs on finishing other parts to get a complete part of course material but this would be the steps to get a first usable version.
1.490 +
1.491 +\section{Conclusion and Personal Experience}
1.492 +After working on {\sisac} for month, it is hard do find the right words about the system. For sure the system itself is a great idea and it would have been a big relaxation if i would have been able to use this system in the last years for sever ell subjects. But for me the biggest disadvantage of {\sisac} is the frontend until there is no mathematical notation and visualisation of simply fractions i don't think that i or other students would be able to use it for learning. I also think that for learning there is no need of complex examples or complex solutions, examples have to be simple but also have to cover all necessary steps of a calculation. Unfortunately there exist different learning types and I'm a visual one, what is also the explanation for my maybe drastic explanation.
1.493 +\par About the backend, what finally was my main work there is not much left to say. The programing language requires a long time to work in and to find out how decelerations work and how isabelle and {\sisac} is build up, maybe this period of collecting informations is to long for a Bakk. Thesis. Also it is hard to find informations about the theories until there was no related work and no usable documentation wether for {\sisac} nor for isabelle or ML.
1.494 +\par When working within the {\sisac} sources you often hung up on problems which would be simple to solve but are hard to discover, therefor it was often necessary to make breaks and define concrete steps on problem solving. Also when having a plan of the upcoming implementation I had to break myself out to do not to much step at once. Often its better to implement small parts and test, write tests and wait then hurrying up. An other aspect is that it was necessary to build {\sisac} from scratch after every change; this and the fact that my finally theories had over 1000 lines often made the development process to a stop and go dilemma.
1.495 +\par Finally I have to say a big \bfseries thank you \normalfont to Dr.~Neuper who invested a lot of his time in my thesis and the {\sisac} project, I remember some hard and long meetings but finally I look back glad.
1.496 +
1.497 +\subsection{Anecdotes}
1.498 +At the very beginning of the thesis i made some calculations and thoughed of every step more than twice. This calculations were the ground stone of my work, we build every step in the calculation following up the real calculations - when doing them by hand. Time went on and after adding the last commands to the programm for applying the transformation ruleset i compared the results - oh wonder there was a mistake in my calculation :)
1.499 +\begin{center}
1.500 +Thank you {\sisac}!
1.501 +\end{center}
1.502
1.503 %----------// BIB \\-----------%
1.504
1.505 -\renewcommand{\refname}{\section{Reference}} % Using "Sources" as the title of the section
1.506 +\renewcommand{\refname}{\section{References}}
1.507 \bibliographystyle{alpha}
1.508 \bibliography{references}
1.509 \clearpage
1.510
1.511 %----------// APPENDIX \\-----------%
1.512 -
1.513 +\newevenside
1.514 +\part{Appendix}
1.515 \appendix
1.516 -
1.517 %----------// WORK TIME \\-----------%
1.518
1.519 -\newevenside
1.520 +
1.521 \section{Record of Working Time}
1.522 \begin{footnotesize}
1.523 -\begin{longtable}[h]{l p{6.5cm} c c r}
1.524 +\begin{longtable}{l p{6.5cm} c c r}
1.525 {\bf Date} & {\bf Description} & {\bf Begin} & {\bf End} & {\bf Dur.}\\
1.526 \hline \hline
1.527 \endhead
1.528 -29.06.2011 & Treffen mit Geiger und Neuper & 15:00 & 17:30 & 2,50\\
1.529 +
1.530 +\hline
1.531 + \multicolumn{5}{r}{{Continued on next page}} \\
1.532 +\hline
1.533 +\endfoot
1.534 +
1.535 +\hline
1.536 +\hline
1.537 +\endlastfoot
1.538 +
1.539 +\multicolumn{5}{l}{Start 1st Iteration} \\
1.540 +\hline
1.541 +29.06.2011 & Meeting Dr. Neuper and DI Geiger & 15:00 & 17:30 & 2,50 \\
1.542 +02.07.2011 & Working on Examples from DI Geiger & 20:00 & 21:30 & 1,50 \\
1.543 +03.07.2011 & Working on Examples from DI Geiger & 21:00 & 22:45 & 1,75 \\
1.544 +05.07.2011 & Meeting Dr. Neuper, Information Exchange & 10:00 & 13:00 & 3,00 \\
1.545 +06.07.2011 & Installing Isabelle & 20:00 & 22:30 & 2,50 \\
1.546 +07.07.2011 & Meeting Dr. Neuper, present-1 & 14:45 & 16:15 & 1,50 \\
1.547 +18.07.2011 & Meeting Dr. Neuper, present-1 Structure & 14:15 & 16:00 & 1,75 \\
1.548 +19.07.2011 & Meeting Dr. Neuper, present-1 Content & 07:20 & 09:20 & 2,00\\
1.549 +19.07.2011 & Meeting Dr. Neuper & 10:00 & 12:00 & 2,00\\
1.550 +21.07.2011 & HG Error Correction, Latex for Thesis & 11:10 & 14:00 & 2,83\\
1.551 +22.07.2011 & Meeting Dr. Neuper & 10:00 & 12:00 & 2,00\\
1.552 +23.07.2011 & Latex for Calculations & 13:45 & 16:30 & 2,75\\
1.553 +24.07.2011 & Meeting Dr. Neuper, present-1 & 20:10 & 20:40 & 0,50\\
1.554 +25.07.2011 & Meeting Dr. Neuper, present-1 & 15:15 & 17:55 & 2,67\\
1.555 +26.07.2011 & Work on Test\_Complex.thy & 10:45 & 12:10 & 1,42\\
1.556 +27.07.2011 & present-1 (Dr. Neuper, DI Geiger) & 10:00 & 12:00 & 2,00\\
1.557 +\hline
1.558 +\multicolumn{5}{l}{End 1st Iteration} \\
1.559 +\multicolumn{5}{l}{Start 2nd Iteration} \\
1.560 +\hline
1.561 +02.09.2011 & Meeting Dr. Neuper, Latex for Thesis & 08:30 & 10:20 & 1,83\\
1.562 +05.09.2011 & Meeting Dr. Neuper, Partial\_Frations.thy & 09:30 & 12:45 & 3,25\\
1.563 +05.09.2011 & Partial\_Fractions.thy & 17:10 & 18:30 & 1,33\\
1.564 +06.09.2011 & Documentation Partial\_Fractions.thy & 10:00 & 13:15 & 3,25\\
1.565 +07.09.2011 & Meeting Dr. Neuper, ML Introduction & 10:00 & 12:50 & 2,83\\
1.566 +08.09.2011 & Preparing Scripts for Latex Output & 19:00 & 22:45 & 3,75\\
1.567 +09.09.2011 & Preparing Scripts for Latex Output & 11:40 & 15:00 & 3,33\\
1.568 +10.09.2011 & Meeting Dr. Neuper, Latex Output, HG Errors & 10:00 & 12:00 & 2,00\\
1.569 +\hline
1.570 +\multicolumn{5}{l}{End 2nd Iteration} \\
1.571 +\multicolumn{5}{l}{Start 3rd and 4th Iteration} \\
1.572 +\hline
1.573 +14.09.2011 & Start on Inverse\_Z\_Transf. Script & 09:10 & 12:25 & 3,25\\
1.574 +16.09.2011 & Information Exchange Sums & 13:15 & 16:00 & 2,75\\
1.575 +19.09.2011 & Programming on Inverse\_Z\_Transf. & 10:00 & 13:10 & 3,17\\
1.576 +20.09.2011 & Meeting Dr. Neuper, Inverse\_Z\_Transf. Script & 15:30 & 18:10 & 2,67\\
1.577 +23.09.2011 & New IsaMakefile for Latex generation & 13:00 & 14:30 & 1,50\\
1.578 +23.09.2011 & Meeting Dr. Neuper, Inverse\_Z\_Transf. Script & 14:30 & 17:30 & 3,00\\
1.579 +26.09.2011 & Partial\_Fractions.thy, get\_Argument & 13:30 & 16:15 & 2,75\\
1.580 +27.09.2011 & Meeting Dr. Neuper, HG Error & 09:00 & 12:20 & 3,33\\
1.581 +28.09.2011 & Meeting Dr. Neuper, Hierarchy Reconstruction & 10:00 & 12:30 & 2,50\\
1.582 +01.10.2011 & Some Testing & 10:00 & 11:00 & 1,00\\
1.583 +02.10.2011 & Inverse\_Z\_Transf. Errors & 15:00 & 16:10 & 1,17\\
1.584 +06.10.2011 & Meeting Dr. Neuper & 15:00 & 17:50 & 2,83\\
1.585 +07.10.2011 & Meeting Dr. Neuper, Inverse\_Z\_Transf. Script & 15:00 & 16:50 & 1,83\\
1.586 +09.10.2011 & Work on Thesis & 16:30 & 18:45 & 2,25\\
1.587 +11.10.2011 & Meeting Dr. Neuper, Abstract & 14:10 & 17:10 & 3,00\\
1.588 +13.10.2011 & Work on Thesis, Implemention part & 08:30 & 10:00 & 1,50\\
1.589 +18.10.2011 & Work on Thesis & 20:30 & 22:50 & 2,33\\
1.590 +19.10.2011 & Work on Thesis & 21:20 & 23:40 & 2,33\\
1.591 +20.10.2011 & Work on Thesis & 08:45 & 10:45 & 2,00\\
1.592 +25.10.2011 & Meeting Dr. Neuper: thesis review & 08:00 & 10:00 & 2,00\\
1.593 +25.10.2011 & Reorganising after meeting & 20:10 & 23:50 & 3,67\\
1.594 +26.10.2011 & Reorganising after meeting, examples in thesis & 08:30 & 11:10 & 2,67\\
1.595 +07.11.2011 & Meeting Preparation & 16:30 & 17:15 & 0,75\\
1.596 +08.11.2011 & Meeting Dr. Neuper: thesis addons & 16:00 & 17:30 & 1,50\\
1.597 +12.11.2011 & Reorganization after meeting & 21:10 & 22:30 & 1,33\\
1.598 +20.11.2011 & Review of Inv\_Z\_Trans & 10:15 & 13:30 & 3,25\\
1.599 +21.11.2011 & get\_numerator & 12:15 & 14:30 & 2,25\\
1.600 +23.11.2011 & get\_numerator & 20:30 & 21:15 & 0,75\\
1.601 +24.11.2011 & get\_numerator final & 14:10 & 15:30 & 1,33\\
1.602 +28.11.2011 & tried to go on in build\_inverse\_ & 11:00 & 13:10 & 2,17\\
1.603 +01.12.2012 & Tuning Invers\_Z\_Tansf. Script & 16:15 & 19:30 & 3,25\\
1.604 +04.12.2012 & Moved Some Tests to Knowledge & 15:30 & 18:15 & 2,75\\
1.605 +05.12.2012 & Tuning Invers\_Z\_Tansf. Script & 13:10 & 14:15 & 1,08\\
1.606 +08.12.2012 & Inverse\_Z\_Tansf. Script, Factors from Solution & 14:30 & 16:15 & 1,75\\
1.607 +10.12.2012 & Moved Some Tests to Knowledge & 20:10 & 23:00 & 2,83\\
1.608 +11.12.2012 & Inverse\_Z\_Tansf. Script, PBZ Ansatz & 10:10 & 12:30 & 2,33\\
1.609 +12.12.2012 & Inverse\_Z\_Tansf. Script, Subsitution & 09:00 & 11:30 & 2,50\\
1.610 +16.12.2012 & Tuning Invers\_Z\_Tansf. Script & 17:15 & 18:45 & 1,50\\
1.611 +19.12.2012 & Tuning Invers\_Z\_Tansf. Script & 19:00 & 20:30 & 1,50\\
1.612 +14.01.2012 & Inverse\_Z\_Tansf. Script, Substitution & 18:45 & 20:30 & 1,75\\
1.613 +22.01.2012 & Inverse\_Z\_Transf. Script, Calc Coeff. & 20:10 & 21:45 & 1,58\\
1.614 +12.02.2012 & Inverse\_Z\_Transf. Script & 17:30 & 19:00 & 1,50\\
1.615 +13.02.2012 & Finished Work on Inverse\_Z\_Transf. Script & 19:30 & 22:10 & 2,67\\
1.616 +14.02.2012 & Formatting for Latex output & 09:00 & 14:45 & 5,75\\
1.617 +15.02.2012 & Formatting for Latex output & 10:00 & 15:30 & 5,50\\
1.618 +16.02.2012 & Going on Work on Thesis & 14:45 & 18:30 & 3,75\\
1.619 +17.02.2012 & Tuning Invers\_Z\_Tansf. Script & 18:30 & 19:45 & 1,25\\
1.620 +19.02.2012 & Meeting Dr. Neuper, present-2 & 09:00 & 13:30 & 4,50\\
1.621 +19.02.2012 & Meeting Dr. Neuper, Integration of work to Isac & 15:00 & 19:10 & 4,17\\
1.622 +20.02.2012 & Meeting Dr. Neuper, Integration of work to Isac & 09:00 & 12:45 & 3,75\\
1.623 +20.02.2012 & Meeting Dr. Neuper, Integration of work to Isac & 14:10 & 18:30 & 4,33\\
1.624 +\hline
1.625 +\multicolumn{5}{l}{End 3rd Iteration}\\
1.626 +\hline
1.627 +20.02.2012 & Finishing Thesis & 20:30 & 22:50 & 2,33\\
1.628 +21.02.2012 & Finishing Thesis & 13:30 & 14:45 & 1,25\\
1.629 +02.03.2012 & Finishing Thesis & 15:45 & 19:00 & 3,25\\
1.630 +06.03.2012 & Finishing Thesis & 09:15 & 10:30 & 1,25\\
1.631 +07.03.2012 & Finishing Thesis & 13:15 & 15:30 & 2,75\\
1.632 +\hline
1.633 +\multicolumn{5}{l}{End 4th Iteration} \\
1.634 +\multicolumn{5}{l}{Start 5th Iteration} \\
1.635 +\hline
1.636 +26.02.2012 & Preparing present-2 & 09:30 & 13:00 & 3,5 \\
1.637 +TBA & present-2 & 0 & 0 & 0 \\
1.638 +\hline
1.639 +\multicolumn{5}{l}{End 5th Iteration} \\
1.640 +\hline
1.641 +\multicolumn{4}{l}{Total working time:} & 196 \\
1.642 \end{longtable}
1.643 \end{footnotesize}
1.644
2.1 --- a/doc-src/isac/jrocnik/bakkarbeit_titlepage.tex Mon Feb 20 18:31:00 2012 +0100
2.2 +++ b/doc-src/isac/jrocnik/bakkarbeit_titlepage.tex Wed Mar 07 15:29:02 2012 +0100
2.3 @@ -16,7 +16,7 @@
2.4 \HRule
2.5 \vspace{0.3cm}
2.6 \Large{
2.7 - \bf Towards Interactive Course Material\\ for Signal Processing based on Isabelle/\isac\\
2.8 + \bf Interactive Course Material for Signal Processing based on Isabelle/\isac\\
2.9 }
2.10 \HRule
2.11
2.12 @@ -29,7 +29,7 @@
2.13
2.14 \vspace{1cm}
2.15 \normalsize{by}\\
2.16 - Jan Simon Rocnik\\\href{mailto:student.tugraz.at}{\tt jan.rocnik@student.tugraz.at}
2.17 + Jan Simon Ro\v{c}nik\\\href{mailto:student.tugraz.at}{\tt jan.rocnik@student.tugraz.at}
2.18
2.19 \vspace{1cm}
2.20 \normalsize{Supervisor}\\
3.1 --- a/doc-src/isac/jrocnik/calulations.tex Mon Feb 20 18:31:00 2012 +0100
3.2 +++ b/doc-src/isac/jrocnik/calulations.tex Wed Mar 07 15:29:02 2012 +0100
3.3 @@ -34,7 +34,7 @@
3.4 \right.$
3.5 \end{center}
3.6
3.7 -\textbf{(b)} Now consider the given delayed impulse, determine its fourie transformation and calculate phase and magnitude:
3.8 +\textbf{\noindent (b)} Now consider the given delayed impulse, determine its fourie transformation and calculate phase and magnitude:
3.9
3.10 \begin{center}
3.11 $x(t)= \left\{
3.12 @@ -46,7 +46,7 @@
3.13 \end{center}
3.14
3.15 \subsubsection{Solution}
3.16 -\textbf{(a)}
3.17 +\textbf{(a)} \textsf{Subproblem 1}
3.18 \onehalfspace{
3.19 \begin{tabbing}
3.20 000\=\kill
3.21 @@ -69,11 +69,10 @@
3.22 \end{tabbing}
3.23 }
3.24
3.25 -\textbf{(b)}
3.26 +\noindent\textbf{(b)} \textsf{Subproblem 1}
3.27 \onehalfspace{
3.28 \begin{tabbing}
3.29 000\=\kill
3.30 -\textsf{Subproblem 1}\\
3.31 \texttt{\footnotesize{01}} \> Definition: $X(j\omega)=\int_\infty^\infty{x(t)\cdot e^{-j\omega t}}$\\
3.32 \`Insert Condition: $x(t) = 1\;$ for $\;\{1\leq t\;\land\;t\leq 3\}\;$ and $\;x(t)=0\;$ otherwise\\
3.33 \texttt{\footnotesize{02}} \> $X(j\omega)=\int_{-1}^{1}{1\cdot e^{-j\omega t}}$\\
3.34 @@ -91,7 +90,7 @@
3.35 \texttt{\footnotesize{08}} \> $\frac{1}{\omega}\cdot e^{j\omega2}\cdot(\frac{e^{j\omega} - e^{-j\omega}}{j})$\\
3.36 \` table\\
3.37 \texttt{\footnotesize{09}} \> $2\cdot e^{j\omega2}\cdot\frac{\sin\;\omega}{\omega}$\\
3.38 -\textsf{Subproblem 2}\\
3.39 +\noindent\textbf{(b)} \textsf{Subproblem 2}\\
3.40 \`Definition: $X(j\omega)=|X(j\omega)|\cdot e^{arg(X(j\omega))}$\\
3.41 \`$|X(j\omega)|$ is called \emph{Magnitude}\\
3.42 \`$arg(X(j\omega))$ is called \emph{Phase}\\
3.43 @@ -99,7 +98,6 @@
3.44 \texttt{\footnotesize{11}} \> $arg(X(j\omega)=-2\omega$\\
3.45 \end{tabbing}
3.46 }
3.47 -
3.48 %------------------------------------------------------------------------------
3.49 %CONVOLUTION
3.50
3.51 @@ -152,7 +150,7 @@
3.52 %------------------------------------------------------------------------------
3.53 %Z-Transformation
3.54
3.55 -\subsection{$\cal Z$-Transformation\label{sec:calc:ztrans}}
3.56 +\subsection{Z-Transformation\label{sec:calc:ztrans}}
3.57 \subsubsection*{Problem\endnote{Problem submitted by Bernhard Geiger. Originally part of the signal processing problem class 5, summer term 2008.}}
3.58 Determine the inverse $\cal{z}$ transform of the following expression. Hint: applay the partial fraction expansion.
3.59
4.1 Binary file doc-src/isac/jrocnik/math-universe.png has changed
5.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
5.2 +++ b/doc-src/isac/jrocnik/pdfsetup.sty Wed Mar 07 15:29:02 2012 +0100
5.3 @@ -0,0 +1,7 @@
5.4 +%%
5.5 +%% default hyperref setup (both for pdf and dvi output)
5.6 +%%
5.7 +
5.8 +\usepackage{color}
5.9 +\definecolor{linkcolor}{rgb}{0,0,0.5}
5.10 +\usepackage[colorlinks=true,linkcolor=linkcolor,citecolor=linkcolor,filecolor=linkcolor,pagecolor=linkcolor,urlcolor=linkcolor]{hyperref}
6.1 --- a/doc-src/isac/jrocnik/preambleForGeneratedDocuments.tex Mon Feb 20 18:31:00 2012 +0100
6.2 +++ b/doc-src/isac/jrocnik/preambleForGeneratedDocuments.tex Wed Mar 07 15:29:02 2012 +0100
6.3 @@ -1,3 +1,5 @@
6.4 \section*{Preamble}
6.5 -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}.
6.6 -\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 by \today.
6.7 \ No newline at end of file
6.8 +This part gives a detailed review on the development and testing process of new programms. All of the following part is automatically generated out of an {\sisac{}}-theory file (\texttt{.thy} - extension). In this case the file is called \texttt{Build\_Inverse\_Z\_Transform} it can be found in the {\sisac{}} directory:
6.9 +\begin{center}\texttt{test/Tools/isac/ADDTESTS/course/}\end{center}
6.10 +{\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}.
6.11 +\par The following theory can be modified and used as a guiedline for implementing new material. Everything found here is just a snapshot of the work by \today.
6.12 \ No newline at end of file
7.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
7.2 +++ b/doc-src/isac/jrocnik/present-2.tex Wed Mar 07 15:29:02 2012 +0100
7.3 @@ -0,0 +1,210 @@
7.4 +\documentclass[%
7.5 +%handout, % prints handouts (=no animations, for printed version)
7.6 +%mathserif
7.7 +%xcolor=pst,
7.8 +14pt
7.9 +% fleqn
7.10 +]{beamer}
7.11 +
7.12 +\usepackage{beamerthemedefault}
7.13 +
7.14 +\useoutertheme[subsection=false]{smoothbars}
7.15 +\useinnertheme{circles}
7.16 +
7.17 +\setbeamercolor{block title}{fg=black,bg=gray}
7.18 +\setbeamercolor{block title alerted}{use=alerted text,fg=black,bg=alerted text.fg!75!bg}
7.19 +\setbeamercolor{block title example}{use=example text,fg=black,bg=example text.fg!75!bg}
7.20 +\setbeamercolor{block body}{parent=normal text,use=block title,bg=block title.bg!25!bg}
7.21 +\setbeamercolor{block body alerted}{parent=normal text,use=block title alerted,bg=block title alerted.bg!25!bg}
7.22 +\setbeamercolor{block body example}{parent=normal text,use=block title example,bg=block title example.bg!25!bg}
7.23 +
7.24 +%aktivate hyperlinks at the end
7.25 +%\usepackage{hyperref}
7.26 +
7.27 +\usepackage[english]{babel}
7.28 +\usepackage[utf8]{inputenc}
7.29 +\usepackage{array}
7.30 +\usepackage{setspace}
7.31 +
7.32 +\definecolor{tug}{rgb}{0.96862,0.14509,0.27450}
7.33 +
7.34 +\def\isac{${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$}
7.35 +\def\sisac{{\footnotesize${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$}}
7.36 +
7.37 +\setbeamertemplate{headline}[text line]{
7.38 + \begin{beamercolorbox}[wd=\paperwidth,ht=8ex,dp=4ex]{}
7.39 + \insertnavigation{0.85\paperwidth}
7.40 + \raisebox{-10pt}{\includegraphics[width=15mm]{tuglogo}}\vskip2pt
7.41 + \hskip-1pt\rule{\paperwidth}{0.3pt}
7.42 + \end{beamercolorbox}
7.43 +}
7.44 +
7.45 +\setbeamertemplate{navigation symbols}{}
7.46 +
7.47 +\definecolor{gray}{rgb}{0.8,0.8,0.8}
7.48 +\setbeamercolor{footline}{fg=black,bg=gray}
7.49 +
7.50 +% Fusszeile mit Autor, Titel und Foliennummer / Gesamtfolienzahl
7.51 +\setbeamertemplate{footline}[text line]{
7.52 + \hskip-1pt
7.53 + \begin{beamercolorbox}[wd=\paperwidth]{footline}
7.54 + \rule{\paperwidth}{0.3pt}
7.55 + \colorbox{tug}{\rule{3pt}{0pt}\rule{0pt}{3pt}}
7.56 + \textbf{\rule{0pt}{5pt}\insertshortauthor\hfill\insertshortinstitute\hfill%
7.57 + \insertshorttitle\rule{1em}{0pt}}
7.58 + \rule{\paperwidth}{0.3pt}
7.59 + \end{beamercolorbox}
7.60 + \begin{beamercolorbox}[wd=\paperwidth,ht=2ex,dp=2ex]{white}
7.61 + \end{beamercolorbox}
7.62 +}%
7.63 +
7.64 +%% Titelblatt-Einstellungen
7.65 +\institute[IST, SPSC]{Institute for Software Technology\\Institute of Signal Processing and Speech Communication\\Graz University of Technology}
7.66 +\title[ISAC for Signal Processing]{Interactive Course Material for\\ Signal Processing based on\\ Isabelle/\isac}
7.67 +\subtitle{Baccalaureate Thesis}
7.68 +\author{Jan Rocnik}
7.69 +\date{01.04.2012}
7.70 +
7.71 +% Subject and Keywords for PDF
7.72 +\subject{Final presentation of Bakk. Thesis}
7.73 +\keywords{isac, isabelle, ist, spsc, thesis, course material}
7.74 +
7.75 +\titlegraphic{\includegraphics[width=20mm]{tuglogo}}
7.76 +
7.77 +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
7.78 +\begin{document}
7.79 +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
7.80 +
7.81 +\begin{frame}[plain]
7.82 + \frametitle{}
7.83 + \titlepage
7.84 +\end{frame}
7.85 +
7.86 +
7.87 +
7.88 +\begin{frame}
7.89 + \frametitle{Contents}
7.90 + \tableofcontents[hideallsubsections %
7.91 + % ,pausesections
7.92 + ] % erzeugt Inhaltsverzeichnis
7.93 +\end{frame}
7.94 +
7.95 +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
7.96 +\section{Introduction}
7.97 +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
7.98 +
7.99 +\subsection{isabelle}
7.100 +\begin{frame}
7.101 + \frametitle{What is isabelle?}
7.102 + \begin{spacing}{1.5}
7.103 + \begin{itemize}
7.104 + \item Punkt 1
7.105 + \item Punkt 2
7.106 + \item Punkt 3
7.107 + \end{itemize}
7.108 + \end{spacing}
7.109 +\end{frame}
7.110 +
7.111 +\subsection{isac}
7.112 +\begin{frame}
7.113 + \frametitle{What is isac?}
7.114 + \begin{spacing}{1.5}
7.115 + \begin{itemize}
7.116 + \item Punkt 1
7.117 + \item Punkt 2
7.118 + \item Punkt 3
7.119 + \end{itemize}
7.120 + \end{spacing}
7.121 +\end{frame}
7.122 +
7.123 +
7.124 +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
7.125 +\section{Thesis Definition}
7.126 +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
7.127 +
7.128 +\begin{frame}
7.129 + \frametitle{Definitions of the Baccalaureate Thesis}
7.130 +
7.131 +\end{frame}
7.132 +
7.133 +\subsection{issues}
7.134 +\begin{frame}
7.135 + \frametitle{Accomplished Issues}
7.136 +
7.137 +\begin{itemize}
7.138 + \item What knowledge is already mechanised in \emph{Isabelle}?
7.139 + \item How can missing theorems and definitions be mechanised?
7.140 + \item What is the effort for such mechanisation?
7.141 + \item How do calculations look like, by using mechanised knowledge?
7.142 + \item What problems and subproblems have to be solved?
7.143 + \item Which problems are already implemented in {\sisac}?
7.144 + \item How are the new problems specified ({\sisac})?
7.145 + \item Which variantes of programms in {\sisac} solve the problems?
7.146 + \item What is the contents of the interactiv course material (Figures, etc.)?
7.147 +\end{itemize}
7.148 +
7.149 +\end{frame}
7.150 +
7.151 +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
7.152 +\section{Demo}
7.153 +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
7.154 +
7.155 +\begin{frame}
7.156 + \frametitle{Demonstration of ISAC}
7.157 + \begin{spacing}{1.5}
7.158 + \begin{itemize}
7.159 + \item development environment
7.160 + \item math assistant
7.161 + \end{itemize}
7.162 + \end{spacing}
7.163 +\end{frame}
7.164 +
7.165 +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
7.166 +\section{Summary}
7.167 +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
7.168 +
7.169 +\subsection{Accomplished}
7.170 +\begin{frame}
7.171 + \frametitle{Accomplished}
7.172 + \begin{itemize}
7.173 + \item partial fractions: theorems, specification, program
7.174 + \item inverse Z-transform with partial fractions: thm, spec, prog
7.175 + \item Isabelle theory indicating issues for {/sisac}-developers
7.176 + \end{itemize}
7.177 +\end{frame}
7.178 +
7.179 +\subsection{Partially Accomplished}
7.180 +\begin{frame}
7.181 + \frametitle{Partially Accomplished}
7.182 + \begin{itemize}
7.183 + \item guidelines for future TP-programmers:\\
7.184 + development environment and programming language will be changed
7.185 + \item examples
7.186 + \end{itemize}
7.187 +\end{frame}
7.188 +
7.189 +\subsection{Not Accomplished}
7.190 +\begin{frame}
7.191 + \frametitle{Not Accomplished}
7.192 + \begin{itemize}
7.193 + \item explanations, figures to examples, theorems, problems
7.194 + \item a sufficient number of implemented topics
7.195 + \item no support of labs and lectures in SP and SPSC
7.196 + \item no material for STEOP
7.197 + \end{itemize}
7.198 +\end{frame}
7.199 +
7.200 +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
7.201 +\section{Conclusion}
7.202 +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
7.203 +
7.204 +\begin{frame}
7.205 + \frametitle{Conculsion}
7.206 + TP-based programming language not ready for production programming fehler in eigener rechnung gefunden...
7.207 +\end{frame}
7.208 +
7.209 +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
7.210 +\end{document}
7.211 +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
7.212 +
7.213 +%% EOF
7.214 \ No newline at end of file
8.1 --- a/doc-src/isac/jrocnik/references.bib Mon Feb 20 18:31:00 2012 +0100
8.2 +++ b/doc-src/isac/jrocnik/references.bib Wed Mar 07 15:29:02 2012 +0100
8.3 @@ -20,7 +20,7 @@
8.4 @manual{wenzel2011system,
8.5 title={The Isabelle System Manual},
8.6 author={Wenzel, M. and Berghofer, S.},
8.7 - organization={TU München},
8.8 + organization={TU Muenchen},
8.9 year={2011},
8.10 month={January}
8.11 }
9.1 --- a/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy Mon Feb 20 18:31:00 2012 +0100
9.2 +++ b/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy Wed Mar 07 15:29:02 2012 +0100
9.3 @@ -5,20 +5,18 @@
9.4 10 20 30 40 50 60 70 80
9.5 *)
9.6
9.7 -header{* Build_Inverse_Z_Transform *}
9.8 -
9.9 theory Build_Inverse_Z_Transform imports Isac
9.10
9.11 begin
9.12
9.13 text{* We stepwise build \ttfamily Inverse\_Z\_Transform.thy \normalfont as an
9.14 - exercise. Because subsection~\ref{sec:stepcheck} requires
9.15 + exercise. Because Subsection~\ref{sec:stepcheck} requires
9.16 \ttfamily Inverse\_Z\_Transform.thy \normalfont as a subtheory of \ttfamily
9.17 Isac.thy\normalfont, the setup has been changed from \ttfamily theory
9.18 Inverse\_Z\_Transform imports Isac \normalfont to the above one.
9.19 \par \noindent
9.20 \begin{center}
9.21 - \textbf{ATTENTION WITH NAMES OF IDENTIFIERS WHEN GOING INTO INTERNALS}
9.22 + \textbf{Attention with the names of identifiers when going into internals!}
9.23 \end{center}
9.24 Here in this theory there are the internal names twice, for instance we have
9.25 \ttfamily (Thm.derivation\_name @{thm rule1} =
9.26 @@ -346,8 +344,11 @@
9.27
9.28 subsubsection {*Get Solutions out of a List*}
9.29 text {*\noindent In {\sisac}'s TP-based programming language:
9.30 - \ttfamily let\$ \$s\_1 = NTH 1\$ solutions; \$s\_2 = NTH 2...\$ \normalfont
9.31 - can be useful.*}
9.32 +\begin{verbatim}
9.33 + let $ $ s_1 = NTH 1 $ solutions; $ s_2 = NTH 2... $
9.34 +\end{verbatim}
9.35 + can be useful.
9.36 + *}
9.37
9.38 ML {*
9.39 val Const ("List.list.Cons", _) $ s_1 $ (Const ("List.list.Cons", _)
9.40 @@ -360,10 +361,11 @@
9.41 requires to get the denominators of the partial fractions out of the
9.42 Solutions as:
9.43 \begin{itemize}
9.44 - \item $ \text{Denominator} _{1} = z - \text{Zeropoint}_{1}$
9.45 - \item $ \text{Denominator} _{2} = z - \text{Zeropoint}_{2}$
9.46 - \item \ldots
9.47 - \end{itemize}*}
9.48 + \item $Denominator_{1}=z-Zeropoint_{1}$
9.49 + \item $Denominator_{2}=z-Zeropoint_{2}$
9.50 + \item \ldots
9.51 + \end{itemize}
9.52 +*}
9.53
9.54 ML {*
9.55 val xx = HOLogic.dest_eq s_1;
9.56 @@ -434,7 +436,7 @@
9.57 by the Lucas-Interpreter. Therefor we moved the function to the
9.58 corresponding \ttfamily Equation.thy \normalfont in our case
9.59 \ttfamily PartialFractions.thy \normalfont. The necessary steps
9.60 - are quit the same as we have done with \ttfamliy get\_denominator
9.61 + are quit the same as we have done with \ttfamily get\_denominator
9.62 \normalfont before.*}
9.63 ML {*
9.64 (*("factors_from_solution",
9.65 @@ -454,88 +456,101 @@
9.66 *}
9.67
9.68 text {*\noindent The tracing output of the calc tree after applying this
9.69 - function was \ttfamily 24 / factors\_from\_solution
9.70 - [z = 1/ 2, z = -1 / 4])] \normalfont and the next step \ttfamily
9.71 - val nxt = ("Empty\_Tac", ...): tac'\_)\normalfont. These observations
9.72 - indicate, that the Lucas-Interpreter (LIP) does not know how to
9.73 - evaluate\\ \ttfamily factors\_from\_solution, \normalfont so we knew
9.74 - that there is something wrong or missing.*}
9.75 + function was:
9.76 +\begin{verbatim}
9.77 + 24 / factors_from_solution [z = 1/ 2, z = -1 / 4])]
9.78 +\end{verbatim}
9.79 + and the next step:
9.80 +\begin{verbatim}
9.81 + val nxt = ("Empty_Tac", ...): tac'_)
9.82 +\end{verbatim}
9.83 + These observations indicate, that the Lucas-Interpreter (LIP)
9.84 + does not know how to evaluate \ttfamily factors\_from\_solution
9.85 + \normalfont, so we knew that there is something wrong or missing.
9.86 + *}
9.87
9.88 -text{*\noindent First we isolate the difficulty in the program as follows:\\
9.89 - \ttfamily \par \noindent
9.90 - "(L\_L::bool list) = (SubProblem (PolyEq',"\^\\
9.91 - "[abcFormula,degree\_2,polynomial,univariate,equation],[no\_met])"\^\\
9.92 - "[BOOL equ, REAL zzz]);"\^\\
9.93 - "(facs::real) = factors\_from\_solution L\_L;"\^\\
9.94 - "(foo::real) = Take facs"\^\\
9.95 +text{*\noindent First we isolate the difficulty in the program as follows:
9.96 +\begin{verbatim}
9.97 + " (L_L::bool list) = (SubProblem (PolyEq', " ^
9.98 + " [abcFormula, degree_2, polynomial, " ^
9.99 + " univariate,equation], " ^
9.100 + " [no_met]) " ^
9.101 + " [BOOL equ, REAL zzz]); " ^
9.102 + " (facs::real) = factors_from_solution L_L; " ^
9.103 + " (foo::real) = Take facs " ^
9.104 +\end{verbatim}
9.105 +
9.106 + \par \noindent And see the tracing output:
9.107 +
9.108 +\begin{verbatim}
9.109 + [(([], Frm), Problem (Isac, [inverse,
9.110 + Z_Transform,
9.111 + SignalProcessing])),
9.112 + (([1], Frm), X z = 3 / (z - 1 / 4 + -1 / 8 * (1 / z))),
9.113 + (([1], Res), ?X' z = 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))),
9.114 + (([2], Res), ?X' z = 24 / (-1 + -2 * z + 8 * z ^^^ 2)),
9.115 + (([3], Pbl), solve (-1 + -2 * z + 8 * z ^^^ 2 = 0, z)),
9.116 + (([3,1], Frm), -1 + -2 * z + 8 * z ^^^ 2 = 0),
9.117 + (([3,1], Res), z = (- -2 + sqrt (-2 ^^^ 2 - 4 * 8 * -1)) / (2 * 8)|
9.118 + z = (- -2 - sqrt (-2 ^^^ 2 - 4 * 8 * -1)) / (2 * 8)),
9.119 + (([3,2], Res), z = 1 / 2 | z = -1 / 4),
9.120 + (([3,3], Res), [ z = 1 / 2, z = -1 / 4]),
9.121 + (([3,4], Res), [ z = 1 / 2, z = -1 / 4]),
9.122 + (([3], Res), [ z = 1 / 2, z = -1 / 4]),
9.123 + (([4], Frm), factors_from_solution [z = 1 / 2, z = -1 / 4])]
9.124 +\end{verbatim}
9.125 +
9.126 + \par \noindent In particular that:
9.127 +
9.128 +\begin{verbatim}
9.129 + (([3], Pbl), solve (-1 + -2 * z + 8 * z ^^^ 2 = 0, z)),
9.130 +\end{verbatim}
9.131 + \par \noindent Shows the equation which has been created in
9.132 + the program by:
9.133 +\begin{verbatim}
9.134 + "(denom::real) = get_denominator funterm; " ^
9.135 + (* get_denominator *)
9.136 + "(equ::bool) = (denom = (0::real)); " ^
9.137 +\end{verbatim}
9.138
9.139 - \normalfont \par \noindent And see the tracing output:\\
9.140 - \ttfamily \par \noindent \lbrack\\
9.141 - ((\lbrack\rbrack, Frm), Problem
9.142 - (Isac, \lbrack inverse, Z\_Transform, SignalProcessing\rbrack)),\\
9.143 - ((\lbrack 1\rbrack, Frm), X z = 3 / (z - 1 / 4 + -1 / 8 * (1 / z))),\\
9.144 - ((\lbrack 1\rbrack, Res),
9.145 - ?X' z = 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))),\\
9.146 - ((\lbrack 2\rbrack, Res),
9.147 - ?X' z = 24 / (-1 + -2 * z + 8 * z \^\^\^ ~2)),\\
9.148 - ((\lbrack 3\rbrack, Pbl),
9.149 - solve (-1 + -2 * z + 8 * z \^\^\^ ~2 = 0, z)),\\
9.150 - ((\lbrack 3,1\rbrack, Frm), -1 + -2 * z + 8 * z \^\^\^ ~2 = 0),\\
9.151 - ((\lbrack 3,1\rbrack, Res),
9.152 - z = (- -2 + sqrt (-2 \^\^\^ ~2 - 4 * 8 * -1)) / (2 * 8)|\\
9.153 - z = (- -2 - sqrt (-2 \^\^\^ ~2 - 4 * 8 * -1)) / (2 * 8)),\\
9.154 - ((\lbrack 3,2\rbrack, Res), z = 1 / 2 | z = -1 / 4),\\
9.155 - ((\lbrack 3,3\rbrack, Res), \lbrack z = 1 / 2, z = -1 / 4\rbrack),\\
9.156 - ((\lbrack 3,4\rbrack, Res), \lbrack z = 1 / 2, z = -1 / 4\rbrack),\\
9.157 - ((\lbrack 3\rbrack, Res), \lbrack z = 1 / 2, z = -1 / 4\rbrack),\\
9.158 - ((\lbrack 4\rbrack, Frm),
9.159 - factors\_from\_solution \lbrackz = 1 / 2, z = -1 / 4])\\
9.160 - \rbrack\\
9.161 -
9.162 - \normalfont \noindent In particular that:\\
9.163 - \ttfamily \par \noindent ((\lbrack 3\rbrack, Pbl),
9.164 - solve (-1 + -2 * z + 8 * z \^\^\^ ~2 = 0, z)),\\
9.165 - \normalfont \par \noindent Shows the equation which has been created in
9.166 - the program by: \ttfamily \\
9.167 -
9.168 - \noindent "(denom::real) = get\_denominator funterm;"\^
9.169 - ~(*get\_denominator*)\\
9.170 - "(equ::bool) = (denom = (0::real));"\^\\
9.171 -
9.172 - \noindent get\_denominator \normalfont has been evaluated successfully,
9.173 + \noindent \ttfamily get\_denominator \normalfont has been evaluated successfully,
9.174 but not\\ \ttfamily factors\_from\_solution.\normalfont
9.175 So we stepwise compare with an analogous case, \ttfamily get\_denominator
9.176 \normalfont successfully done above: We know that LIP evaluates
9.177 expressions in the program by use of the \emph{srls}, so we try to get
9.178 the original \emph{srls}.\\
9.179
9.180 - \noindent \ttfamily val \lbrace srls,\ldots\rbrace\ttfamily
9.181 - = get\_met \lbrack "SignalProcessing",
9.182 - "Z\_Transform","inverse"\rbrack;\\
9.183 +\begin{verbatim}
9.184 + val {srls,...} = get_met ["SignalProcessing",
9.185 + "Z_Transform",
9.186 + "inverse"];
9.187 +\end{verbatim}
9.188
9.189 - \par \noindent \normalfont Create 2 good example terms\\
9.190 - \ttfamily \par \noindent val SOME t1 =\\
9.191 - parseNEW ctxt "get\_denominator ((111::real) / 222)";
9.192 - \par \noindent val SOME t2 =\\
9.193 - parseNEW ctxt "factors\_from\_solution \lbrack(z::real)
9.194 - = 1/2, z = -1/4\rbrack";\\
9.195 + \par \noindent Create 2 good example terms:
9.196
9.197 - \par \noindent \normalfont Rewrite the terms using srls:\\
9.198 +\begin{verbatim}
9.199 +val SOME t1 =
9.200 + parseNEW ctxt "get_denominator ((111::real) / 222)";
9.201 +val SOME t2 =
9.202 + parseNEW ctxt "factors_from_solution [(z::real)=1/2, z=-1/4]";
9.203 +\end{verbatim}
9.204 +
9.205 + \par \noindent Rewrite the terms using srls:\\
9.206 \ttfamily \par \noindent rewrite\_set\_ thy true srls t1;\\
9.207 rewrite\_set\_ thy true srls t2;\\
9.208 \par \noindent \normalfont Now we see a difference: \texttt{t1} gives
9.209 \texttt{SOME} but \texttt{t2} gives \texttt{NONE}. We look at the
9.210 - \emph{srls}:\\
9.211 -
9.212 - \par \noindent \ttfamily val srls = Rls \lbrace id =
9.213 - "srls\_InverseZTransform", rules =\\
9.214 - \lbrack Calc("Rational.get\_numerator",\\
9.215 - eval\_get\_numerator "Rational.get\_numerator"),\\
9.216 - Calc("Partial\_Fractions.factors\_from\_solution",\\
9.217 - eval\_factors\_from\_solution
9.218 - "Partial\_Fractions.factors\_from\_solution")\rbrack\rbrace\\
9.219 -
9.220 - \par \noindent \normalfont Here everthing is perfect. So the error can
9.221 + \emph{srls}:
9.222 +\begin{verbatim}
9.223 + val srls =
9.224 + Rls{id = "srls_InverseZTransform",
9.225 + rules = [Calc("Rational.get_numerator",
9.226 + eval_get_numerator "Rational.get_numerator"),
9.227 + Calc("Partial_Fractions.factors_from_solution",
9.228 + eval_factors_from_solution
9.229 + "Partial_Fractions.factors_from_solution")]}
9.230 +\end{verbatim}
9.231 + \par \noindent Here everthing is perfect. So the error can
9.232 only be in the SML code of \ttfamily eval\_factors\_from\_solution.
9.233 \normalfont We try to check the code with an existing test; since the
9.234 \emph{code} is in
9.235 @@ -555,12 +570,13 @@
9.236 \begin{center}use \ttfamily "Knowledge/partial\_fractions.sml"
9.237 \normalfont \end{center}
9.238 and \ttfamily Partial\_Fractions.thy \normalfont is part is part of
9.239 - {\sisac} by evaluating\\
9.240 + {\sisac} by evaluating
9.241
9.242 - \par \noindent \ttfamily val thy = @\lbrace theory~Isac \rbrace;
9.243 - \normalfont \\
9.244 +\begin{verbatim}
9.245 + val thy = @{theory Isac};
9.246 +\end{verbatim}
9.247
9.248 - \par \noindent \normalfont After rebuilding {\sisac} again it worked.
9.249 + After rebuilding {\sisac} again it worked.
9.250 *}
9.251
9.252 subsubsection {*Build Expression*}
9.253 @@ -698,7 +714,7 @@
9.254 scr = EmptyScr});
9.255 *}
9.256
9.257 -text{*\noindent We apply the ruleset\lodts*}
9.258 +text{*\noindent We apply the ruleset\ldots*}
9.259
9.260 ML {*
9.261 val SOME (ttttt,_) =
9.262 @@ -719,7 +735,7 @@
9.263 Calculation in Section~\ref{sec:calc:ztrans} Subproblem~1.*}
9.264
9.265 text{*\noindent To get the first coefficient we substitute $z$ with the first
9.266 - zero-point we determined in section~\ref{sec:solveq}.*}
9.267 + zero-point we determined in Section~\ref{sec:solveq}.*}
9.268
9.269 ML {*
9.270 val SOME (eq4_1,_) =
9.271 @@ -799,7 +815,7 @@
9.272 ML {*thy*}
9.273
9.274 text{*\noindent To get the second coefficient we substitute $z$ with the second
9.275 - zero-point we determined in section~\ref{sec:solveq}.*}
9.276 + zero-point we determined in Section~\ref{sec:solveq}.*}
9.277
9.278 ML {*
9.279 val SOME (eq4b_1,_) =
9.280 @@ -884,7 +900,7 @@
9.281
9.282 text{*\noindent For the suddenly created node we have to define the input
9.283 and output parameters. We already prepared their definition in
9.284 - section~\ref{sec:deffdes}.*}
9.285 + Section~\ref{sec:deffdes}.*}
9.286
9.287 ML {*
9.288 store_pbt
9.289 @@ -990,7 +1006,7 @@
9.290 subsection {*Stepwise Extend the Program*}
9.291 ML {*
9.292 val str =
9.293 - "Script InverseZTransform (Xeq::bool) =" ^
9.294 + "Script InverseZTransform (Xeq::bool) = "^
9.295 " Xeq";
9.296 *}
9.297
9.298 @@ -999,16 +1015,16 @@
9.299
9.300 ML {*
9.301 val str =
9.302 - "Script InverseZTransform (Xeq::bool) =" ^
9.303 + "Script InverseZTransform (Xeq::bool) = "^
9.304 (*
9.305 * 1/z) instead of z ^^^ -1
9.306 *)
9.307 - " (let X = Take Xeq;" ^
9.308 - " X' = Rewrite ruleZY False X;" ^
9.309 + " (let X = Take Xeq; "^
9.310 + " X' = Rewrite ruleZY False X; "^
9.311 (*
9.312 * z * denominator
9.313 *)
9.314 - " X' = (Rewrite_Set norm_Rational False) X'" ^
9.315 + " X' = (Rewrite_Set norm_Rational False) X' "^
9.316 (*
9.317 * simplify
9.318 *)
9.319 @@ -1016,23 +1032,23 @@
9.320 (*
9.321 * NONE
9.322 *)
9.323 - "Script InverseZTransform (Xeq::bool) =" ^
9.324 + "Script InverseZTransform (Xeq::bool) = "^
9.325 (*
9.326 * (1/z) instead of z ^^^ -1
9.327 *)
9.328 - " (let X = Take Xeq;" ^
9.329 - " X' = Rewrite ruleZY False X;" ^
9.330 + " (let X = Take Xeq; "^
9.331 + " X' = Rewrite ruleZY False X; "^
9.332 (*
9.333 * z * denominator
9.334 *)
9.335 - " X' = (Rewrite_Set norm_Rational False) X';" ^
9.336 + " X' = (Rewrite_Set norm_Rational False) X'; "^
9.337 (*
9.338 * simplify
9.339 *)
9.340 - " X' = (SubProblem (Isac',[pqFormula,degree_2," ^
9.341 - " polynomial,univariate,equation]," ^
9.342 - " [no_met]) " ^
9.343 - " [BOOL e_e, REAL v_v])" ^
9.344 + " X' = (SubProblem (Isac',[pqFormula,degree_2, "^
9.345 + " polynomial,univariate,equation], "^
9.346 + " [no_met]) "^
9.347 + " [BOOL e_e, REAL v_v]) "^
9.348 " in X)";
9.349 *}
9.350
9.351 @@ -1042,11 +1058,11 @@
9.352
9.353 ML {*
9.354 val str =
9.355 - "Script InverseZTransform (Xeq::bool) =" ^
9.356 - " (let X = Take Xeq;" ^
9.357 - " X' = Rewrite ruleZY False X;" ^
9.358 - " X' = (Rewrite_Set norm_Rational False) X';" ^
9.359 - " funterm = rhs X'" ^
9.360 + "Script InverseZTransform (Xeq::bool) = "^
9.361 + " (let X = Take Xeq; "^
9.362 + " X' = Rewrite ruleZY False X; "^
9.363 + " X' = (Rewrite_Set norm_Rational False) X'; "^
9.364 + " funterm = rhs X' "^
9.365 (*
9.366 * drop X'= for equation solving
9.367 *)
9.368 @@ -1059,23 +1075,23 @@
9.369
9.370 ML {*
9.371 val str =
9.372 - "Script InverseZTransform (X_eq::bool) =" ^
9.373 - " (let X = Take X_eq;" ^
9.374 - " X' = Rewrite ruleZY False X;" ^
9.375 - " X' = (Rewrite_Set norm_Rational False) X';" ^
9.376 - " (X'_z::real) = lhs X';" ^
9.377 - " (z::real) = argument_in X'_z;" ^
9.378 - " (funterm::real) = rhs X';" ^
9.379 - " (denom::real) = get_denominator funterm;" ^
9.380 + "Script InverseZTransform (X_eq::bool) = "^
9.381 + " (let X = Take X_eq; "^
9.382 + " X' = Rewrite ruleZY False X; "^
9.383 + " X' = (Rewrite_Set norm_Rational False) X'; "^
9.384 + " (X'_z::real) = lhs X'; "^
9.385 + " (z::real) = argument_in X'_z; "^
9.386 + " (funterm::real) = rhs X'; "^
9.387 + " (denom::real) = get_denominator funterm; "^
9.388 (*
9.389 * get_denominator
9.390 *)
9.391 - " (equ::bool) = (denom = (0::real));" ^
9.392 - " (L_L::bool list) = " ^
9.393 - " (SubProblem (Test', " ^
9.394 - " [linear,univariate,equation,test], " ^
9.395 - " [Test,solve_linear]) " ^
9.396 - " [BOOL equ, REAL z]) " ^
9.397 + " (equ::bool) = (denom = (0::real)); "^
9.398 + " (L_L::bool list) = "^
9.399 + " (SubProblem (Test', "^
9.400 + " [linear,univariate,equation,test], "^
9.401 + " [Test,solve_linear]) "^
9.402 + " [BOOL equ, REAL z]) "^
9.403 " in X)";
9.404
9.405 parse thy str;
9.406 @@ -1087,37 +1103,37 @@
9.407 The evaluation of the functions is done by rewriting using this ruleset.*}
9.408
9.409 ML {*
9.410 - val srls = Rls {id="srls_InverseZTransform",
9.411 - preconds = [],
9.412 - rew_ord = ("termlessI",termlessI),
9.413 - erls = append_rls "erls_in_srls_InverseZTransform" e_rls
9.414 - [(*for asm in NTH_CONS ...*)
9.415 - Calc ("Orderings.ord_class.less",eval_equ "#less_"),
9.416 - (*2nd NTH_CONS pushes n+-1 into asms*)
9.417 - Calc("Groups.plus_class.plus", eval_binop "#add_")
9.418 - ],
9.419 - srls = Erls, calc = [],
9.420 - rules = [
9.421 - Thm ("NTH_CONS",num_str @{thm NTH_CONS}),
9.422 - Calc("Groups.plus_class.plus",
9.423 - eval_binop "#add_"),
9.424 - Thm ("NTH_NIL",num_str @{thm NTH_NIL}),
9.425 - Calc("Tools.lhs", eval_lhs"eval_lhs_"),
9.426 - Calc("Tools.rhs", eval_rhs"eval_rhs_"),
9.427 - Calc("Atools.argument'_in",
9.428 - eval_argument_in "Atools.argument'_in"),
9.429 - Calc("Rational.get_denominator",
9.430 - eval_get_denominator "#get_denominator"),
9.431 - Calc("Rational.get_numerator",
9.432 - eval_get_numerator "#get_numerator"),
9.433 - Calc("Partial_Fractions.factors_from_solution",
9.434 - eval_factors_from_solution
9.435 - "#factors_from_solution"),
9.436 - Calc("Partial_Fractions.drop_questionmarks",
9.437 - eval_drop_questionmarks "#drop_?")
9.438 - ],
9.439 - scr = EmptyScr
9.440 - };
9.441 + val srls =
9.442 + Rls {id="srls_InverseZTransform",
9.443 + preconds = [],
9.444 + rew_ord = ("termlessI",termlessI),
9.445 + erls = append_rls "erls_in_srls_InverseZTransform" e_rls
9.446 + [(*for asm in NTH_CONS ...*)
9.447 + Calc ("Orderings.ord_class.less",eval_equ "#less_"),
9.448 + (*2nd NTH_CONS pushes n+-1 into asms*)
9.449 + Calc("Groups.plus_class.plus", eval_binop "#add_")
9.450 + ],
9.451 + srls = Erls, calc = [],
9.452 + rules = [
9.453 + Thm ("NTH_CONS",num_str @{thm NTH_CONS}),
9.454 + Calc("Groups.plus_class.plus",
9.455 + eval_binop "#add_"),
9.456 + Thm ("NTH_NIL",num_str @{thm NTH_NIL}),
9.457 + Calc("Tools.lhs", eval_lhs"eval_lhs_"),
9.458 + Calc("Tools.rhs", eval_rhs"eval_rhs_"),
9.459 + Calc("Atools.argument'_in",
9.460 + eval_argument_in "Atools.argument'_in"),
9.461 + Calc("Rational.get_denominator",
9.462 + eval_get_denominator "#get_denominator"),
9.463 + Calc("Rational.get_numerator",
9.464 + eval_get_numerator "#get_numerator"),
9.465 + Calc("Partial_Fractions.factors_from_solution",
9.466 + eval_factors_from_solution
9.467 + "#factors_from_solution"),
9.468 + Calc("Partial_Fractions.drop_questionmarks",
9.469 + eval_drop_questionmarks "#drop_?")
9.470 + ],
9.471 + scr = EmptyScr};
9.472 *}
9.473
9.474
9.475 @@ -1125,7 +1141,7 @@
9.476
9.477 text{*\noindent After we also tested how to write scripts and run them,
9.478 we start creating the final version of our script and store it into
9.479 - the method for which we created a node in section~\ref{sec:cparentnode}
9.480 + the method for which we created a node in Section~\ref{sec:cparentnode}
9.481 Note that we also did this stepwise, but we didn't kept every
9.482 subversion.*}
9.483
9.484 @@ -1303,32 +1319,34 @@
9.485 text {*\noindent Instead of \ttfamily nxt = Subproblem \normalfont above we had
9.486 \ttfamily Empty\_Tac; \normalfont the search for the reason considered
9.487 the following points:\begin{itemize}
9.488 - \item What shows \ttfamily show\_pt pt;\normalfont\ldots?\\
9.489 - \ttfamily ((\lbrack 2\rbrack, Res), ?X' z = 24 /
9.490 - (-1 + -2 * z + 8 * z \^\^\^ ~2))\rbrack\normalfont\\
9.491 + \item What shows \ttfamily show\_pt pt;\normalfont\ldots?
9.492 +\begin{verbatim}(([2], Res), ?X' z = 24 / (-1 + -2 * z + 8 * z ^^^ 2))]\end{verbatim}
9.493 The calculation is ok but no \ttfamily next \normalfont step found:
9.494 Should be\\ \ttfamily nxt = Subproblem\normalfont!
9.495 \item What shows \ttfamily trace\_script := true; \normalfont we read
9.496 - bottom up\ldots\\
9.497 - \ttfamily @@@next leaf 'SubProbfrom\\
9.498 - (PolyEq',\\
9.499 - \lbrack abcFormula, degree\_2, polynomial, univariate,
9.500 - equation\rbrack,\\
9.501 - no\_meth)\\
9.502 - \lbrack BOOL equ, REAL z\rbrack' ---> STac 'SubProblem\\
9.503 - (PolyEq',\\
9.504 - [abcFormula, degree\_2, polynomial, univariate, equation],\\
9.505 - no\_meth)\\
9.506 - \lbrack BOOL (-1 + -2 * z + 8 * z \^\^\^ ~2 = 0),
9.507 - REAL z\rbrack'\normalfont\\
9.508 + bottom up\ldots
9.509 + \begin{verbatim}
9.510 + @@@next leaf 'SubProblem
9.511 + (PolyEq',[abcFormula, degree_2, polynomial,
9.512 + univariate, equation], no_meth)
9.513 + [BOOL equ, REAL z]'
9.514 + ---> STac 'SubProblem (PolyEq',
9.515 + [abcFormula, degree_2, polynomial,
9.516 + univariate, equation], no_meth)
9.517 + [BOOL (-1 + -2 * z + 8 * z \^\^\^ ~2 = 0), REAL z]'
9.518 + \end{verbatim}
9.519 We see the SubProblem with correct arguments from searching next
9.520 step (program text !!!--->!!! STac (script tactic) with arguments
9.521 evaluated.)
9.522 \item Do we have the right Script \ldots difference in the
9.523 - arguments in the arguments\ldots\\
9.524 - \ttfamily val Script s =\\
9.525 - (#scr o get\_met) ["SignalProcessing","Z\_Transform","inverse"];\\
9.526 - writeln (term2str s);\normalfont\\
9.527 + arguments in the arguments\ldots
9.528 + \begin{verbatim}
9.529 + val Script s =
9.530 + (#scr o get_met) ["SignalProcessing",
9.531 + "Z_Transform",
9.532 + "inverse"];
9.533 + writeln (term2str s);
9.534 + \end{verbatim}
9.535 \ldots shows the right script. Difference in the arguments.
9.536 \item Test --- Why helpless here ? --- shows: \ttfamily replace
9.537 no\_meth by [no\_meth] \normalfont in Script
9.538 @@ -1344,7 +1362,7 @@
9.539 we had \ttfamily Empty\_Tac; \normalfont the search for the reason
9.540 considered the following points:\begin{itemize}
9.541 \item Difference in the arguments
9.542 - \item Comparison with subsection~ref{sec:solveq}: There solving this
9.543 + \item Comparison with Subsection~\ref{sec:solveq}: There solving this
9.544 equation works, so there must be some difference in the arguments
9.545 of the Subproblem: RIGHT: we had \ttfamily [no\_meth] \normalfont
9.546 instead of \ttfamily [no\_met] \normalfont ;-)
9.547 @@ -1367,14 +1385,16 @@
9.548 \item Was there an error message? NO -- ok
9.549 \item Has \ttfamily nxt = Add\_Find \normalfont been inserted in pt:\\
9.550 \ttfamily get\_obj g\_pbl pt (fst p);\normalfont? YES -- ok
9.551 - \item What is the returned formula:
9.552 - \ttfamily print\_depth 999; f; print\_depth 999;\\
9.553 - \lbrace Find = \lbrack Correct "solutions z\_i"\rbrack,
9.554 - With = \lbrack\rbrack,\\
9.555 - Given = \lbrack Correct "equality (-1 + -2 * z + 8 * z ^^^ 2 = 0)",
9.556 - Correct "solveFor z"\rbrack,\\
9.557 - Where = \lbrack \ldots \rbrack,
9.558 - Relate = \lbrack\rbrack\rbrace $ \normalfont\\
9.559 + \item What is the returned formula:
9.560 +\begin{verbatim}
9.561 +print_depth 999; f; print_depth 999;
9.562 +{ Find = [ Correct "solutions z_i"],
9.563 + With = [],
9.564 + Given = [Correct "equality (-1 + -2*z + 8*z ^^^ 2 = 0)",
9.565 + Correct "solveFor z"],
9.566 + Where = [...],
9.567 + Relate = [] }
9.568 +\end{verbatim}
9.569 \normalfont The only False is the reason: the Where (the precondition) is
9.570 False for good reasons: The precondition seems to check for linear
9.571 equations, not for the one we want to solve! Removed this error by
9.572 @@ -1508,35 +1528,39 @@
9.573 \normalfont and then modularise. In this case TODO problems?!?
9.574
9.575 We chose another way and go bottom up: first we build the sub-problem in
9.576 - \ttfamily Partial\_Fractions.thy \normalfont with the term
9.577 + \ttfamily Partial\_Fractions.thy \normalfont with the term:
9.578
9.579 - $$\frac{3}{x\cdot(z - \fract{1}{4} + \frac{-1}{8}\cdot\fract{1}{z})}$$
9.580 + $$\frac{3}{x\cdot(z - \frac{1}{4} + \frac{-1}{8}\cdot\frac{1}{z})}$$
9.581
9.582 - (how this still can be improved see \ttfamily Partial\_Fractions.thy \normalfont),
9.583 + \noindent (how this still can be improved see \ttfamily Partial\_Fractions.thy\normalfont),
9.584 and re-use all stuff prepared in \ttfamily Build\_Inverse\_Z\_Transform.thy:
9.585 - The knowledge will be transferred to \ttfamily src/../Partial\_Fractions.thy
9.586 - \normalfont and the respective tests to \ttfamily test/../sartial\_fractions.sml.
9.587 + \normalfont The knowledge will be transferred to \ttfamily src/../Partial\_Fractions.thy
9.588 + \normalfont and the respective tests to:
9.589 + \begin{center}\ttfamily test/../sartial\_fractions.sml\normalfont\end{center}
9.590 *}
9.591
9.592 subsection {* Transfer to Partial\_Fractions.thy *}
9.593 text {*
9.594 - First we transfer both, knowledge and tests into \ttfamily src/../Partial\_Fractions.thy
9.595 - \normalfont in order to immediately have the test results.
9.596 + First we transfer both, knowledge and tests into:
9.597 + \begin{center}\ttfamily src/../Partial\_Fractions.thy\normalfont\end{center}
9.598 + in order to immediately have the test results.
9.599
9.600 - We copy \ttfamily factors_from_solution, drop_questionmarks,
9.601 - ansatz_2nd_order \normalfont and rule-sets --- no problem.
9.602 - Also \ttfamily store_pbt .. "pbl_simp_rat_partfrac"
9.603 + We copy \ttfamily factors\_from\_solution, drop\_questionmarks,\\
9.604 + ansatz\_2nd\_order \normalfont and rule-sets --- no problem.
9.605 +
9.606 + Also \ttfamily store\_pbt ..\\ "pbl\_simp\_rat\_partfrac"
9.607 \normalfont is easy.
9.608
9.609 - But then we copy from (1) \ttfamily Build\_Inverse\_Z\_Transform.thy
9.610 - store_met .. "met_SP_Ztrans_inv" to (2) \ttfamily Partial\_Fractions.thy
9.611 - store_met .. "met_SP_Ztrans_inv"
9.612 - \normalfont and cut out the respective part from the program. First we ensure that
9.613 + But then we copy from:\\
9.614 + (1) \ttfamily Build\_Inverse\_Z\_Transform.thy store\_met\ldots "met\_SP\_Ztrans\_inv"
9.615 + \normalfont\\ to\\
9.616 + (2) \ttfamily Partial\_Fractions.thy store\_met\ldots "met\_SP\_Ztrans\_inv"
9.617 + \normalfont\\ and cut out the respective part from the program. First we ensure that
9.618 the string is correct. When we insert the string into (2)
9.619 - \ttfamily store_met .. "met_partial_fraction" \normalfont --- and get an error.
9.620 + \ttfamily store\_met .. "met\_partial\_fraction" \normalfont --- and get an error.
9.621 *}
9.622
9.623 -subsubsection {* 'Programming' in \sisac}'s TP-based Language *}
9.624 +subsubsection {* 'Programming' in ISAC's TP-based Language *}
9.625 text {*
9.626 At the present state writing programs in {\sisac} is particularly cumbersome.
9.627 So we give hints how to cope with the many obstacles. Below we describe the
9.628 @@ -1546,39 +1570,44 @@
9.629 \item We check if the \textbf{string} containing the program is correct.
9.630 \item We check if the \textbf{types in the program} are correct.
9.631 For this purpose we start start with the first and last lines
9.632 - \begin{verbatim}
9.633 - "PartFracScript (f_f::real) (v_v::real) = " ^
9.634 - " (let X = Take f_f; " ^
9.635 - " pbz = ((Substitute []) X) " ^
9.636 - " in pbz)"
9.637 - \end{verbatim}
9.638 + \begin{verbatim}
9.639 + "PartFracScript (f_f::real) (v_v::real) = " ^
9.640 + " (let X = Take f_f; " ^
9.641 + " pbz = ((Substitute []) X) " ^
9.642 + " in pbz)"
9.643 + \end{verbatim}
9.644 The last but one line helps not to bother with ';'.
9.645 \item Then we add line by line. Already the first line causes the error.
9.646 So we investigate it by
9.647 - \begin{verbatim}
9.648 - val ctxt = ProofContext.init_global @{theory};
9.649 - val SOME t = parseNEW ctxt "(num_orig::real) = get_numerator (rhs f_f)";
9.650 - \end{verbatim}
9.651 + \begin{verbatim}
9.652 + val ctxt = ProofContext.init_global @ { theory } ;
9.653 + val SOME t =
9.654 + parseNEW ctxt "(num_orig::real) =
9.655 + get_numerator(rhs f_f)";
9.656 + \end{verbatim}
9.657 and see a type clash: \ttfamily rhs \normalfont from (1) requires type
9.658 - \ttfamily bool \normalfont while (2) wants to have \ttfamily (f_f::real).
9.659 + \ttfamily bool \normalfont while (2) wants to have \ttfamily (f\_f::real).
9.660 \normalfont Of course, we don't need \ttfamily rhs \normalfont anymore.
9.661 \item Type-checking can be very tedious. One might even inspect the
9.662 - parse-tree of the program with \sisac's specific debug tools:
9.663 - \begin{verbatim}
9.664 - val {scr = Script t,...} = get_met ["simplification","of_rationals","to_partial_fraction"];
9.665 - atomty_thy @{theory} t;
9.666 - \end{verbatim}
9.667 + parse-tree of the program with {\sisac}'s specific debug tools:
9.668 + \begin{verbatim}
9.669 + val {scr = Script t,...} =
9.670 + get_met ["simplification",
9.671 + "of_rationals",
9.672 + "to_partial_fraction"];
9.673 + atomty_thy @ { theory } t ;
9.674 + \end{verbatim}
9.675 \item We check if the \textbf{semantics of the program} by stepwise evaluation
9.676 of the program. Evaluation is done by the Lucas-Interpreter, which works
9.677 using the knowledge in theory Isac; so we have to re-build Isac. And the
9.678 test are performed simplest in a file which is loaded with Isac.
9.679 - See \ttfamily tests/../partial_fractions.sml \normalfont.
9.680 + See \ttfamily tests/../partial\_fractions.sml \normalfont.
9.681 \end{enumerate}
9.682 *}
9.683
9.684 subsection {* Transfer to Inverse\_Z\_Transform.thy *}
9.685 text {*
9.686 -
9.687 + Unfortunately it was not possible to complete this task. Because we ran out of time\ldots
9.688 *}
9.689
9.690
10.1 --- a/test/Tools/isac/ADDTESTS/course/SignalProcess/document/Build_Inverse_Z_Transform.tex Mon Feb 20 18:31:00 2012 +0100
10.2 +++ b/test/Tools/isac/ADDTESTS/course/SignalProcess/document/Build_Inverse_Z_Transform.tex Wed Mar 07 15:29:02 2012 +0100
10.3 @@ -22,13 +22,13 @@
10.4 %
10.5 \begin{isamarkuptext}%
10.6 We stepwise build \ttfamily Inverse\_Z\_Transform.thy \normalfont as an
10.7 - exercise. Because subsection~\ref{sec:stepcheck} requires
10.8 + exercise. Because Subsection~\ref{sec:stepcheck} requires
10.9 \ttfamily Inverse\_Z\_Transform.thy \normalfont as a subtheory of \ttfamily
10.10 Isac.thy\normalfont, the setup has been changed from \ttfamily theory
10.11 Inverse\_Z\_Transform imports Isac \normalfont to the above one.
10.12 \par \noindent
10.13 \begin{center}
10.14 - \textbf{ATTENTION WITH NAMES OF IDENTIFIERS WHEN GOING INTO INTERNALS}
10.15 + \textbf{Attention with the names of identifiers when going into internals!}
10.16 \end{center}
10.17 Here in this theory there are the internal names twice, for instance we have
10.18 \ttfamily (Thm.derivation\_name \isa{rule{\isadigit{1}}} =
10.19 @@ -306,13 +306,13 @@
10.20 %
10.21 \endisadelimML
10.22 %
10.23 -\isamarkupsection{Prepare Steps for CTP-based programming Language\label{sec:prepstep}%
10.24 +\isamarkupsection{Prepare Steps for TP-based programming Language\label{sec:prepstep}%
10.25 }
10.26 \isamarkuptrue%
10.27 %
10.28 \begin{isamarkuptext}%
10.29 -\par \noindent The following sections are challanging with the CTP-based
10.30 - possibilities of building the programm. The goal is realized in
10.31 +\par \noindent The following sections are challenging with the CTP-based
10.32 + possibilities of building the program. The goal is realized in
10.33 Section~\ref{spec-meth} and Section~\ref{prog-steps}.
10.34 \par The reader is advised to jump between the subsequent subsections and
10.35 the respective steps in Section~\ref{prog-steps}. By comparing
10.36 @@ -327,7 +327,7 @@
10.37 %
10.38 \begin{isamarkuptext}%
10.39 \noindent We try two different notations and check which of them
10.40 - isabelle can handle best.%
10.41 + Isabelle can handle best.%
10.42 \end{isamarkuptext}%
10.43 \isamarkuptrue%
10.44 %
10.45 @@ -366,7 +366,7 @@
10.46 \isamarkuptrue%
10.47 %
10.48 \begin{isamarkuptext}%
10.49 -\noindent The partial fraction decomposion is only possible ig we
10.50 +\noindent The partial fraction decomposition is only possible if we
10.51 get the bound variable out of the numerator. Therefor we divide
10.52 the expression by $z$. Follow up the Calculation at
10.53 Section~\ref{sec:calc:ztrans} line number 02.%
10.54 @@ -483,8 +483,8 @@
10.55 \isamarkuptrue%
10.56 %
10.57 \begin{isamarkuptext}%
10.58 -\noindent The selv written functions in e.g. \texttt{get\_denominator}
10.59 - should become a constant for the isabelle parser:%
10.60 +\noindent The self written functions in e.g. \texttt{get\_denominator}
10.61 + should become a constant for the Isabelle parser:%
10.62 \end{isamarkuptext}%
10.63 \isamarkuptrue%
10.64 \isacommand{consts}\isamarkupfalse%
10.65 @@ -499,7 +499,7 @@
10.66 \par \noindent ATTENTION: From now on \ttfamily
10.67 Build\_Inverse\_Z\_Transform \normalfont mimics a build from scratch;
10.68 it only works due to re-building {\sisac} several times (indicated
10.69 - explicityl).%
10.70 + explicitly).%
10.71 \end{isamarkuptext}%
10.72 \isamarkuptrue%
10.73 %
10.74 @@ -539,8 +539,8 @@
10.75 %
10.76 \begin{isamarkuptext}%
10.77 \noindent \ttfamily get\_numerator \normalfont should also become a
10.78 - constant for the isabelle parser, follow up the \texttt{const}
10.79 - decleration above.%
10.80 + constant for the Isabelle parser, follow up the \texttt{const}
10.81 + declaration above.%
10.82 \end{isamarkuptext}%
10.83 \isamarkuptrue%
10.84 %
10.85 @@ -573,7 +573,7 @@
10.86 \endisadelimML
10.87 %
10.88 \begin{isamarkuptext}%
10.89 -\noindent We discovered severell problems by implementing the
10.90 +\noindent We discovered several problems by implementing the
10.91 \ttfamily get\_numerator \normalfont function. Remember when
10.92 putting new functions to {\sisac}, put them in a thy file and rebuild
10.93 {\sisac}, also put them in the ruleset for the script!%
10.94 @@ -587,7 +587,7 @@
10.95 \begin{isamarkuptext}%
10.96 \noindent We have to find the zeros of the term, therefor we use our
10.97 \ttfamily get\_denominator \normalfont function from the step before
10.98 - and try to solve the second order eqeuation. (Follow up the Calculation
10.99 + and try to solve the second order equation. (Follow up the Calculation
10.100 in Section~\ref{sec:calc:ztrans} Subproblem 2) Note: This type of
10.101 equation is too general for the present program.
10.102 \par We know that this equation can be categorized as \em univariate
10.103 @@ -619,7 +619,7 @@
10.104 %
10.105 \begin{isamarkuptext}%
10.106 \noindent Check if the given equation matches the specification of this
10.107 - quation type.%
10.108 + equation type.%
10.109 \end{isamarkuptext}%
10.110 \isamarkuptrue%
10.111 %
10.112 @@ -673,7 +673,7 @@
10.113 %
10.114 \begin{isamarkuptext}%
10.115 \noindent Check if the (other) given equation matches the
10.116 - specification of this quation type.%
10.117 + specification of this equation type.%
10.118 \end{isamarkuptext}%
10.119 \isamarkuptrue%
10.120 %
10.121 @@ -743,7 +743,7 @@
10.122 \isamarkuptrue%
10.123 %
10.124 \begin{isamarkuptext}%
10.125 -\noindent We go on with the decomposion of our expression. Follow up the
10.126 +\noindent We go on with the decomposition of our expression. Follow up the
10.127 Calculation in Section~\ref{sec:calc:ztrans} Step~3 and later on
10.128 Subproblem~1.%
10.129 \end{isamarkuptext}%
10.130 @@ -781,9 +781,11 @@
10.131 \isamarkuptrue%
10.132 %
10.133 \begin{isamarkuptext}%
10.134 -\noindent In {\sisac}'s CTP-based programming language:
10.135 - \ttfamily let\$ \$s\_1 = NTH 1\$ solutions; \$s\_2 = NTH 2...\$ \normalfont
10.136 - can be usefull.%
10.137 +\noindent In {\sisac}'s TP-based programming language:
10.138 +\begin{verbatim}
10.139 + let $ $ s_1 = NTH 1 $ solutions; $ s_2 = NTH 2... $
10.140 +\end{verbatim}
10.141 + can be useful.%
10.142 \end{isamarkuptext}%
10.143 \isamarkuptrue%
10.144 %
10.145 @@ -807,13 +809,13 @@
10.146 \endisadelimML
10.147 %
10.148 \begin{isamarkuptext}%
10.149 -\noindent The ansatz for the \em Partial Fraction Decomposion \normalfont
10.150 +\noindent The ansatz for the \em Partial Fraction Decomposition \normalfont
10.151 requires to get the denominators of the partial fractions out of the
10.152 Solutions as:
10.153 \begin{itemize}
10.154 - \item $ \text{Denominator} _{1} = z - \text{Zeropoint}_{1}$
10.155 - \item $ \text{Denominator} _{2} = z - \text{Zeropoint}_{2}$
10.156 - \item \ldots
10.157 + \item $Denominator_{1}=z-Zeropoint_{1}$
10.158 + \item $Denominator_{2}=z-Zeropoint_{2}$
10.159 + \item \ldots
10.160 \end{itemize}%
10.161 \end{isamarkuptext}%
10.162 \isamarkuptrue%
10.163 @@ -896,8 +898,8 @@
10.164 \noindent This function needs to be packed such that it can be evaluated
10.165 by the Lucas-Interpreter. Therefor we moved the function to the
10.166 corresponding \ttfamily Equation.thy \normalfont in our case
10.167 - \ttfamily PartialFractions.thy \normalfont. The neccessary steps
10.168 - are quit the same as we have done with \ttfamliy get\_denominator
10.169 + \ttfamily PartialFractions.thy \normalfont. The necessary steps
10.170 + are quit the same as we have done with \ttfamily get\_denominator
10.171 \normalfont before.%
10.172 \end{isamarkuptext}%
10.173 \isamarkuptrue%
10.174 @@ -932,92 +934,104 @@
10.175 \endisadelimML
10.176 %
10.177 \begin{isamarkuptext}%
10.178 -\noindent The tracing output of the calc tree after apllying this
10.179 - function was \ttfamily 24 / factors\_from\_solution
10.180 - [z = 1/ 2, z = -1 / 4])] \normalfont and the next step \ttfamily
10.181 - val nxt = ("Empty\_Tac", ...): tac'\_)\normalfont. These observations
10.182 - indicate, that the Lucas-Interpreter (LIP) does not know how to
10.183 - evaluate\\ \ttfamily factors\_from\_solution, \normalfont so we knew
10.184 - that there is something wrong or missing.%
10.185 +\noindent The tracing output of the calc tree after applying this
10.186 + function was:
10.187 +\begin{verbatim}
10.188 + 24 / factors_from_solution [z = 1/ 2, z = -1 / 4])]
10.189 +\end{verbatim}
10.190 + and the next step:
10.191 +\begin{verbatim}
10.192 + val nxt = ("Empty_Tac", ...): tac'_)
10.193 +\end{verbatim}
10.194 + These observations indicate, that the Lucas-Interpreter (LIP)
10.195 + does not know how to evaluate \ttfamily factors\_from\_solution
10.196 + \normalfont, so we knew that there is something wrong or missing.%
10.197 \end{isamarkuptext}%
10.198 \isamarkuptrue%
10.199 %
10.200 \begin{isamarkuptext}%
10.201 -\noindent First we isolate the difficulty in the program as follows:\\
10.202 - \ttfamily \par \noindent
10.203 - "(L\_L::bool list) = (SubProblem (PolyEq',"\^\\
10.204 - "[abcFormula,degree\_2,polynomial,univariate,equation],[no\_met])"\^\\
10.205 - "[BOOL equ, REAL zzz]);"\^\\
10.206 - "(facs::real) = factors\_from\_solution L\_L;"\^\\
10.207 - "(foo::real) = Take facs"\^\\
10.208 +\noindent First we isolate the difficulty in the program as follows:
10.209 +\begin{verbatim}
10.210 + " (L_L::bool list) = (SubProblem (PolyEq', " ^
10.211 + " [abcFormula, degree_2, polynomial, " ^
10.212 + " univariate,equation], " ^
10.213 + " [no_met]) " ^
10.214 + " [BOOL equ, REAL zzz]); " ^
10.215 + " (facs::real) = factors_from_solution L_L; " ^
10.216 + " (foo::real) = Take facs " ^
10.217 +\end{verbatim}
10.218 +
10.219 + \par \noindent And see the tracing output:
10.220 +
10.221 +\begin{verbatim}
10.222 + [(([], Frm), Problem (Isac, [inverse,
10.223 + Z_Transform,
10.224 + SignalProcessing])),
10.225 + (([1], Frm), X z = 3 / (z - 1 / 4 + -1 / 8 * (1 / z))),
10.226 + (([1], Res), ?X' z = 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))),
10.227 + (([2], Res), ?X' z = 24 / (-1 + -2 * z + 8 * z ^^^ 2)),
10.228 + (([3], Pbl), solve (-1 + -2 * z + 8 * z ^^^ 2 = 0, z)),
10.229 + (([3,1], Frm), -1 + -2 * z + 8 * z ^^^ 2 = 0),
10.230 + (([3,1], Res), z = (- -2 + sqrt (-2 ^^^ 2 - 4 * 8 * -1)) / (2 * 8)|
10.231 + z = (- -2 - sqrt (-2 ^^^ 2 - 4 * 8 * -1)) / (2 * 8)),
10.232 + (([3,2], Res), z = 1 / 2 | z = -1 / 4),
10.233 + (([3,3], Res), [ z = 1 / 2, z = -1 / 4]),
10.234 + (([3,4], Res), [ z = 1 / 2, z = -1 / 4]),
10.235 + (([3], Res), [ z = 1 / 2, z = -1 / 4]),
10.236 + (([4], Frm), factors_from_solution [z = 1 / 2, z = -1 / 4])]
10.237 +\end{verbatim}
10.238 +
10.239 + \par \noindent In particular that:
10.240 +
10.241 +\begin{verbatim}
10.242 + (([3], Pbl), solve (-1 + -2 * z + 8 * z ^^^ 2 = 0, z)),
10.243 +\end{verbatim}
10.244 + \par \noindent Shows the equation which has been created in
10.245 + the program by:
10.246 +\begin{verbatim}
10.247 + "(denom::real) = get_denominator funterm; " ^
10.248 + (* get_denominator *)
10.249 + "(equ::bool) = (denom = (0::real)); " ^
10.250 +\end{verbatim}
10.251
10.252 - \normalfont \par \noindent And see the tracing output:\\
10.253 - \ttfamily \par \noindent \lbrack\\
10.254 - ((\lbrack\rbrack, Frm), Problem
10.255 - (Isac, \lbrack inverse, Z\_Transform, SignalProcessing\rbrack)),\\
10.256 - ((\lbrack 1\rbrack, Frm), X z = 3 / (z - 1 / 4 + -1 / 8 * (1 / z))),\\
10.257 - ((\lbrack 1\rbrack, Res),
10.258 - ?X' z = 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))),\\
10.259 - ((\lbrack 2\rbrack, Res),
10.260 - ?X' z = 24 / (-1 + -2 * z + 8 * z \^\^\^ ~2)),\\
10.261 - ((\lbrack 3\rbrack, Pbl),
10.262 - solve (-1 + -2 * z + 8 * z \^\^\^ ~2 = 0, z)),\\
10.263 - ((\lbrack 3,1\rbrack, Frm), -1 + -2 * z + 8 * z \^\^\^ ~2 = 0),\\
10.264 - ((\lbrack 3,1\rbrack, Res),
10.265 - z = (- -2 + sqrt (-2 \^\^\^ ~2 - 4 * 8 * -1)) / (2 * 8)|\\
10.266 - z = (- -2 - sqrt (-2 \^\^\^ ~2 - 4 * 8 * -1)) / (2 * 8)),\\
10.267 - ((\lbrack 3,2\rbrack, Res), z = 1 / 2 | z = -1 / 4),\\
10.268 - ((\lbrack 3,3\rbrack, Res), \lbrack z = 1 / 2, z = -1 / 4\rbrack),\\
10.269 - ((\lbrack 3,4\rbrack, Res), \lbrack z = 1 / 2, z = -1 / 4\rbrack),\\
10.270 - ((\lbrack 3\rbrack, Res), \lbrack z = 1 / 2, z = -1 / 4\rbrack),\\
10.271 - ((\lbrack 4\rbrack, Frm),
10.272 - factors\_from\_solution \lbrackz = 1 / 2, z = -1 / 4])\\
10.273 - \rbrack\\
10.274 -
10.275 - \normalfont \noindent In particular that:\\
10.276 - \ttfamily \par \noindent ((\lbrack 3\rbrack, Pbl),
10.277 - solve (-1 + -2 * z + 8 * z \^\^\^ ~2 = 0, z)),\\
10.278 - \normalfont \par \noindent Shows the equation which has been created in
10.279 - the program by: \ttfamily \\
10.280 -
10.281 - \noindent "(denom::real) = get\_denominator funterm;"\^
10.282 - ~(*get\_denominator*)\\
10.283 - "(equ::bool) = (denom = (0::real));"\^\\
10.284 -
10.285 - \noindent get\_denominator \normalfont has been evaluated successfully,
10.286 + \noindent \ttfamily get\_denominator \normalfont has been evaluated successfully,
10.287 but not\\ \ttfamily factors\_from\_solution.\normalfont
10.288 So we stepwise compare with an analogous case, \ttfamily get\_denominator
10.289 \normalfont successfully done above: We know that LIP evaluates
10.290 expressions in the program by use of the \emph{srls}, so we try to get
10.291 the original \emph{srls}.\\
10.292
10.293 - \noindent \ttfamily val \lbrace srls,\ldots\rbrace\ttfamily
10.294 - = get\_met \lbrack "SignalProcessing",
10.295 - "Z\_Transform","inverse"\rbrack;\\
10.296 +\begin{verbatim}
10.297 + val {srls,...} = get_met ["SignalProcessing",
10.298 + "Z_Transform",
10.299 + "inverse"];
10.300 +\end{verbatim}
10.301
10.302 - \par \noindent \normalfont Create 2 good example terms\\
10.303 - \ttfamily \par \noindent val SOME t1 =\\
10.304 - parseNEW ctxt "get\_denominator ((111::real) / 222)";
10.305 - \par \noindent val SOME t2 =\\
10.306 - parseNEW ctxt "factors\_from\_solution \lbrack(z::real)
10.307 - = 1/2, z = -1/4\rbrack";\\
10.308 + \par \noindent Create 2 good example terms:
10.309
10.310 - \par \noindent \normalfont Rewrite the terms using srls:\\
10.311 +\begin{verbatim}
10.312 +val SOME t1 =
10.313 + parseNEW ctxt "get_denominator ((111::real) / 222)";
10.314 +val SOME t2 =
10.315 + parseNEW ctxt "factors_from_solution [(z::real)=1/2, z=-1/4]";
10.316 +\end{verbatim}
10.317 +
10.318 + \par \noindent Rewrite the terms using srls:\\
10.319 \ttfamily \par \noindent rewrite\_set\_ thy true srls t1;\\
10.320 rewrite\_set\_ thy true srls t2;\\
10.321 \par \noindent \normalfont Now we see a difference: \texttt{t1} gives
10.322 \texttt{SOME} but \texttt{t2} gives \texttt{NONE}. We look at the
10.323 - \emph{srls}:\\
10.324 -
10.325 - \par \noindent \ttfamily val srls = Rls \lbrace id =
10.326 - "srls\_InverseZTransform", rules =\\
10.327 - \lbrack Calc("Rational.get\_numerator",\\
10.328 - eval\_get\_numerator "Rational.get\_numerator"),\\
10.329 - Calc("Partial\_Fractions.factors\_from\_solution",\\
10.330 - eval\_factors\_from\_solution
10.331 - "Partial\_Fractions.factors\_from\_solution")\rbrack\rbrace\\
10.332 -
10.333 - \par \noindent \normalfont Here everthing is perfect. So the error can
10.334 + \emph{srls}:
10.335 +\begin{verbatim}
10.336 + val srls =
10.337 + Rls{id = "srls_InverseZTransform",
10.338 + rules = [Calc("Rational.get_numerator",
10.339 + eval_get_numerator "Rational.get_numerator"),
10.340 + Calc("Partial_Fractions.factors_from_solution",
10.341 + eval_factors_from_solution
10.342 + "Partial_Fractions.factors_from_solution")]}
10.343 +\end{verbatim}
10.344 + \par \noindent Here everthing is perfect. So the error can
10.345 only be in the SML code of \ttfamily eval\_factors\_from\_solution.
10.346 \normalfont We try to check the code with an existing test; since the
10.347 \emph{code} is in
10.348 @@ -1028,7 +1042,7 @@
10.349 \normalfont\end{center}
10.350 \par \noindent After updating the function \ttfamily
10.351 factors\_from\_solution \normalfont to a new version and putting a
10.352 - testcase to \ttfamily Partial\_Fractions.sml \normalfont we tried again
10.353 + test-case to \ttfamily Partial\_Fractions.sml \normalfont we tried again
10.354 to evaluate the term with the same result.
10.355 \par We opened the test \ttfamily Test\_Isac.thy \normalfont and saw that
10.356 everything is working fine. Also we checked that the test \ttfamily
10.357 @@ -1037,12 +1051,13 @@
10.358 \begin{center}use \ttfamily "Knowledge/partial\_fractions.sml"
10.359 \normalfont \end{center}
10.360 and \ttfamily Partial\_Fractions.thy \normalfont is part is part of
10.361 - {\sisac} by evaluating\\
10.362 + {\sisac} by evaluating
10.363
10.364 - \par \noindent \ttfamily val thy = @\lbrace theory~Isac \rbrace;
10.365 - \normalfont \\
10.366 +\begin{verbatim}
10.367 + val thy = \hyperlink{theory.Isac}{\mbox{\isa{Isac}}};
10.368 +\end{verbatim}
10.369
10.370 - \par \noindent \normalfont After rebuilding {\sisac} again it worked.%
10.371 + After rebuilding {\sisac} again it worked.%
10.372 \end{isamarkuptext}%
10.373 \isamarkuptrue%
10.374 %
10.375 @@ -1051,7 +1066,7 @@
10.376 \isamarkuptrue%
10.377 %
10.378 \begin{isamarkuptext}%
10.379 -\noindent In {\sisac}'s CTP-based programming language we can build
10.380 +\noindent In {\sisac}'s TP-based programming language we can build
10.381 expressions by:\\
10.382 \ttfamily let s\_1 = Take numerator / (s\_1 * s\_2) \normalfont%
10.383 \end{isamarkuptext}%
10.384 @@ -1065,7 +1080,7 @@
10.385 \isacommand{ML}\isamarkupfalse%
10.386 \ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
10.387 \ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}\isanewline
10.388 -\ \ \ {\isaliteral{2A}{\isacharasterisk}}\ The\ main\ denominator\ is\ the\ multiplikation\ of\ the\ denominators\ of\isanewline
10.389 +\ \ \ {\isaliteral{2A}{\isacharasterisk}}\ The\ main\ denominator\ is\ the\ multiplication\ of\ the\ denominators\ of\isanewline
10.390 \ \ \ {\isaliteral{2A}{\isacharasterisk}}\ all\ partial\ fractions{\isaliteral{2E}{\isachardot}}\isanewline
10.391 \ \ \ {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline
10.392 \ \ \ \isanewline
10.393 @@ -1089,7 +1104,7 @@
10.394 \isamarkuptrue%
10.395 %
10.396 \begin{isamarkuptext}%
10.397 -\noindent We use the Ansatz of the Partial Fraction Decomposen for our
10.398 +\noindent We use the Ansatz of the Partial Fraction Decomposition for our
10.399 expression 2nd order. Follow up the calculation in
10.400 Section~\ref{sec:calc:ztrans} Step~03.%
10.401 \end{isamarkuptext}%
10.402 @@ -1110,11 +1125,11 @@
10.403 \endisadelimML
10.404 %
10.405 \begin{isamarkuptext}%
10.406 -\noindent We define two aximatizations, the first one is the main ansatz,
10.407 - the next one is just an eqivalent transformation of the resulting
10.408 +\noindent We define two axiomatization, the first one is the main ansatz,
10.409 + the next one is just an equivalent transformation of the resulting
10.410 equation. Both axiomatizations were moved to \ttfamily
10.411 Partial\_Fractions.thy \normalfont and got their own rulesets. In later
10.412 - programms it is possible to use the rulesets and the machine will find
10.413 + programs it is possible to use the rulesets and the machine will find
10.414 the correct ansatz and equivalent transformation itself.%
10.415 \end{isamarkuptext}%
10.416 \isamarkuptrue%
10.417 @@ -1124,7 +1139,7 @@
10.418 \ \ equival{\isaliteral{5F}{\isacharunderscore}}trans{\isaliteral{5F}{\isacharunderscore}}{\isadigit{2}}nd{\isaliteral{5F}{\isacharunderscore}}order{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}n{\isaliteral{2F}{\isacharslash}}{\isaliteral{28}{\isacharparenleft}}a{\isaliteral{2A}{\isacharasterisk}}b{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ A{\isaliteral{2F}{\isacharslash}}a\ {\isaliteral{2B}{\isacharplus}}\ B{\isaliteral{2F}{\isacharslash}}b{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}n\ {\isaliteral{3D}{\isacharequal}}\ A{\isaliteral{2A}{\isacharasterisk}}b\ {\isaliteral{2B}{\isacharplus}}\ B{\isaliteral{2A}{\isacharasterisk}}a{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}%
10.419 \begin{isamarkuptext}%
10.420 \noindent We use our \ttfamily ansatz\_2nd\_order \normalfont to rewrite
10.421 - our expression and get an equilation with our expression on the left
10.422 + our expression and get an equation with our expression on the left
10.423 and the partial fractions of it on the right hand side.%
10.424 \end{isamarkuptext}%
10.425 \isamarkuptrue%
10.426 @@ -1159,7 +1174,7 @@
10.427 \endisadelimML
10.428 %
10.429 \begin{isamarkuptext}%
10.430 -\noindent Eliminate the demoninators by multiplying the left and the
10.431 +\noindent Eliminate the denominators by multiplying the left and the
10.432 right hand side of the equation with the main denominator. This is an
10.433 simple equivalent transformation. Later on we use an own ruleset
10.434 defined in \ttfamily Partial\_Fractions.thy \normalfont for doing this.
10.435 @@ -1225,9 +1240,9 @@
10.436 \endisadelimML
10.437 %
10.438 \begin{isamarkuptext}%
10.439 -\noindent In Example~\ref{eg:gap} of my thesis I'm describin a problem about
10.440 +\noindent In Example~\ref{eg:gap} of my thesis I'm describing a problem about
10.441 simplifications. The problem that we would like to have only a specific degree
10.442 - of simplification occours right here, in the next step.%
10.443 + of simplification occurs right here, in the next step.%
10.444 \end{isamarkuptext}%
10.445 \isamarkuptrue%
10.446 %
10.447 @@ -1363,7 +1378,7 @@
10.448 \endisadelimML
10.449 %
10.450 \begin{isamarkuptext}%
10.451 -\noindent We apply the ruleset\lodts%
10.452 +\noindent We apply the ruleset\ldots%
10.453 \end{isamarkuptext}%
10.454 \isamarkuptrue%
10.455 %
10.456 @@ -1410,20 +1425,20 @@
10.457 %
10.458 \endisadelimML
10.459 %
10.460 -\isamarkupsubsubsection{Get the First Koeffizient%
10.461 +\isamarkupsubsubsection{Get the First Coefficient%
10.462 }
10.463 \isamarkuptrue%
10.464 %
10.465 \begin{isamarkuptext}%
10.466 -\noindent Now it's up to get the two koeffizients A and B, which will be
10.467 - the numerators of our partial fractions. Continiue following up the
10.468 +\noindent Now it's up to get the two coefficients A and B, which will be
10.469 + the numerators of our partial fractions. Continue following up the
10.470 Calculation in Section~\ref{sec:calc:ztrans} Subproblem~1.%
10.471 \end{isamarkuptext}%
10.472 \isamarkuptrue%
10.473 %
10.474 \begin{isamarkuptext}%
10.475 -\noindent To get the first koeffizient we substitude $z$ with the first
10.476 - zeropoint we determined in section~\ref{sec:solveq}.%
10.477 +\noindent To get the first coefficient we substitute $z$ with the first
10.478 + zero-point we determined in Section~\ref{sec:solveq}.%
10.479 \end{isamarkuptext}%
10.480 \isamarkuptrue%
10.481 %
10.482 @@ -1452,7 +1467,7 @@
10.483 \ \ val\ fmz\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{22}{\isachardoublequote}}equality\ {\isaliteral{28}{\isacharparenleft}}{\isadigit{3}}{\isaliteral{3D}{\isacharequal}}{\isadigit{3}}{\isaliteral{2A}{\isacharasterisk}}A{\isaliteral{2F}{\isacharslash}}{\isaliteral{28}{\isacharparenleft}}{\isadigit{4}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}real{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{22}{\isachardoublequote}}solveFor\ A{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}{\isaliteral{22}{\isachardoublequote}}solutions\ L{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
10.484 \ \ val\ {\isaliteral{28}{\isacharparenleft}}dI{\isaliteral{27}{\isacharprime}}{\isaliteral{2C}{\isacharcomma}}pI{\isaliteral{27}{\isacharprime}}{\isaliteral{2C}{\isacharcomma}}mI{\isaliteral{27}{\isacharprime}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequote}}Isac{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{22}{\isachardoublequote}}univariate{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}{\isaliteral{22}{\isachardoublequote}}equation{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{22}{\isachardoublequote}}no{\isaliteral{5F}{\isacharunderscore}}met{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
10.485 \ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}\isanewline
10.486 -\ \ \ {\isaliteral{2A}{\isacharasterisk}}\ Solve\ the\ simple\ linear\ equilation\ for\ A\ TODO{\isaliteral{3A}{\isacharcolon}}\isanewline
10.487 +\ \ \ {\isaliteral{2A}{\isacharasterisk}}\ Solve\ the\ simple\ linear\ equation\ for\ A{\isaliteral{3A}{\isacharcolon}}\isanewline
10.488 \ \ \ {\isaliteral{2A}{\isacharasterisk}}\ Return\ eq{\isaliteral{2C}{\isacharcomma}}\ not\ list\ of\ eq{\isaliteral{27}{\isacharprime}}s\isanewline
10.489 \ \ \ {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline
10.490 \ \ val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}fa{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ CalcTreeTEST\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{28}{\isacharparenleft}}fmz{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{28}{\isacharparenleft}}dI{\isaliteral{27}{\isacharprime}}{\isaliteral{2C}{\isacharcomma}}pI{\isaliteral{27}{\isacharprime}}{\isaliteral{2C}{\isacharcomma}}mI{\isaliteral{27}{\isacharprime}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
10.491 @@ -1517,7 +1532,7 @@
10.492 %
10.493 \endisadelimML
10.494 %
10.495 -\isamarkupsubsubsection{Get Second Koeffizient%
10.496 +\isamarkupsubsubsection{Get Second Coefficient%
10.497 }
10.498 \isamarkuptrue%
10.499 %
10.500 @@ -1542,8 +1557,8 @@
10.501 \endisadelimML
10.502 %
10.503 \begin{isamarkuptext}%
10.504 -\noindent To get the second koeffizient we substitude $z$ with the second
10.505 - zeropoint we determined in section~\ref{sec:solveq}.%
10.506 +\noindent To get the second coefficient we substitute $z$ with the second
10.507 + zero-point we determined in Section~\ref{sec:solveq}.%
10.508 \end{isamarkuptext}%
10.509 \isamarkuptrue%
10.510 %
10.511 @@ -1637,7 +1652,7 @@
10.512 \begin{isamarkuptext}%
10.513 \noindent Now everything we need for solving the problem has been
10.514 tested out. We now start by creating new nodes for our methods and
10.515 - further on our new programm in the interpreter.%
10.516 + further on our new program in the interpreter.%
10.517 \end{isamarkuptext}%
10.518 \isamarkuptrue%
10.519 %
10.520 @@ -1648,7 +1663,7 @@
10.521 %
10.522 \begin{isamarkuptext}%
10.523 \noindent We define the fields \em filterExpression \normalfont and
10.524 - \em stepResponse \normalfont both as quations, they represent the in- and
10.525 + \em stepResponse \normalfont both as equations, they represent the in- and
10.526 output of the program.%
10.527 \end{isamarkuptext}%
10.528 \isamarkuptrue%
10.529 @@ -1662,7 +1677,7 @@
10.530 %
10.531 \begin{isamarkuptext}%
10.532 \noindent The next step is defining the specifications as nodes in the
10.533 - designated part. We have to create the hierachy node by node and start
10.534 + designated part. We have to create the hierarchy node by node and start
10.535 with \em SignalProcessing \normalfont and go on by creating the node
10.536 \em Z\_Transform\normalfont.%
10.537 \end{isamarkuptext}%
10.538 @@ -1691,8 +1706,8 @@
10.539 %
10.540 \begin{isamarkuptext}%
10.541 \noindent For the suddenly created node we have to define the input
10.542 - and output parameters. We already prepaired their definition in
10.543 - section~\ref{sec:deffdes}.%
10.544 + and output parameters. We already prepared their definition in
10.545 + Section~\ref{sec:deffdes}.%
10.546 \end{isamarkuptext}%
10.547 \isamarkuptrue%
10.548 %
10.549 @@ -1862,8 +1877,8 @@
10.550 \endisadelimML
10.551 %
10.552 \begin{isamarkuptext}%
10.553 -\noindent If yes we can get the method by steping backwards through
10.554 - the hierachy.%
10.555 +\noindent If yes we can get the method by stepping backwards through
10.556 + the hierarchy.%
10.557 \end{isamarkuptext}%
10.558 \isamarkuptrue%
10.559 %
10.560 @@ -1883,13 +1898,13 @@
10.561 %
10.562 \endisadelimML
10.563 %
10.564 -\isamarkupsection{Program in CTP-based language \label{prog-steps}%
10.565 +\isamarkupsection{Program in TP-based language \label{prog-steps}%
10.566 }
10.567 \isamarkuptrue%
10.568 %
10.569 \begin{isamarkuptext}%
10.570 -\noindent We start stepwise expanding our programm. The script is a
10.571 - simple string containing severell manipulation instructions.
10.572 +\noindent We start stepwise expanding our program. The script is a
10.573 + simple string containing several manipulation instructions.
10.574 \par The first script we try contains no instruction, we only test if
10.575 building scripts that way work.%
10.576 \end{isamarkuptext}%
10.577 @@ -1907,7 +1922,7 @@
10.578 \isacommand{ML}\isamarkupfalse%
10.579 \ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
10.580 \ \ val\ str\ {\isaliteral{3D}{\isacharequal}}\ \isanewline
10.581 -\ \ \ \ {\isaliteral{22}{\isachardoublequote}}Script\ InverseZTransform\ {\isaliteral{28}{\isacharparenleft}}Xeq{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}bool{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{5E}{\isacharcircum}}\isanewline
10.582 +\ \ \ \ {\isaliteral{22}{\isachardoublequote}}Script\ InverseZTransform\ {\isaliteral{28}{\isacharparenleft}}Xeq{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}bool{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{5E}{\isacharcircum}}\isanewline
10.583 \ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ Xeq{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
10.584 {\isaliteral{2A7D}{\isacharverbatimclose}}%
10.585 \endisatagML
10.586 @@ -1931,16 +1946,16 @@
10.587 \isacommand{ML}\isamarkupfalse%
10.588 \ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
10.589 \ \ val\ str\ {\isaliteral{3D}{\isacharequal}}\ \isanewline
10.590 -\ \ \ \ {\isaliteral{22}{\isachardoublequote}}Script\ InverseZTransform\ {\isaliteral{28}{\isacharparenleft}}Xeq{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}bool{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{5E}{\isacharcircum}}\isanewline
10.591 +\ \ \ \ {\isaliteral{22}{\isachardoublequote}}Script\ InverseZTransform\ {\isaliteral{28}{\isacharparenleft}}Xeq{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}bool{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{5E}{\isacharcircum}}\isanewline
10.592 \ \ \ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}\isanewline
10.593 \ \ \ \ \ {\isaliteral{2A}{\isacharasterisk}}\ {\isadigit{1}}{\isaliteral{2F}{\isacharslash}}z{\isaliteral{29}{\isacharparenright}}\ instead\ of\ z\ {\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}\ {\isaliteral{2D}{\isacharminus}}{\isadigit{1}}\isanewline
10.594 \ \ \ \ \ {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline
10.595 -\ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{28}{\isacharparenleft}}let\ X\ {\isaliteral{3D}{\isacharequal}}\ Take\ Xeq{\isaliteral{3B}{\isacharsemicolon}}{\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{5E}{\isacharcircum}}\isanewline
10.596 -\ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ X{\isaliteral{27}{\isacharprime}}\ {\isaliteral{3D}{\isacharequal}}\ Rewrite\ ruleZY\ False\ X{\isaliteral{3B}{\isacharsemicolon}}{\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{5E}{\isacharcircum}}\isanewline
10.597 +\ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{28}{\isacharparenleft}}let\ X\ {\isaliteral{3D}{\isacharequal}}\ Take\ Xeq{\isaliteral{3B}{\isacharsemicolon}}\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{5E}{\isacharcircum}}\isanewline
10.598 +\ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ X{\isaliteral{27}{\isacharprime}}\ {\isaliteral{3D}{\isacharequal}}\ Rewrite\ ruleZY\ False\ X{\isaliteral{3B}{\isacharsemicolon}}\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{5E}{\isacharcircum}}\isanewline
10.599 \ \ \ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}\isanewline
10.600 \ \ \ \ \ {\isaliteral{2A}{\isacharasterisk}}\ z\ {\isaliteral{2A}{\isacharasterisk}}\ denominator\isanewline
10.601 \ \ \ \ \ {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline
10.602 -\ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ X{\isaliteral{27}{\isacharprime}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}Rewrite{\isaliteral{5F}{\isacharunderscore}}Set\ norm{\isaliteral{5F}{\isacharunderscore}}Rational\ False{\isaliteral{29}{\isacharparenright}}\ X{\isaliteral{27}{\isacharprime}}{\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{5E}{\isacharcircum}}\isanewline
10.603 +\ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ X{\isaliteral{27}{\isacharprime}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}Rewrite{\isaliteral{5F}{\isacharunderscore}}Set\ norm{\isaliteral{5F}{\isacharunderscore}}Rational\ False{\isaliteral{29}{\isacharparenright}}\ X{\isaliteral{27}{\isacharprime}}\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{5E}{\isacharcircum}}\isanewline
10.604 \ \ \ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}\isanewline
10.605 \ \ \ \ \ {\isaliteral{2A}{\isacharasterisk}}\ simplify\isanewline
10.606 \ \ \ \ \ {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline
10.607 @@ -1948,23 +1963,23 @@
10.608 \ \ \ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}\isanewline
10.609 \ \ \ \ \ {\isaliteral{2A}{\isacharasterisk}}\ NONE\isanewline
10.610 \ \ \ \ \ {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline
10.611 -\ \ \ \ {\isaliteral{22}{\isachardoublequote}}Script\ InverseZTransform\ {\isaliteral{28}{\isacharparenleft}}Xeq{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}bool{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{5E}{\isacharcircum}}\isanewline
10.612 +\ \ \ \ {\isaliteral{22}{\isachardoublequote}}Script\ InverseZTransform\ {\isaliteral{28}{\isacharparenleft}}Xeq{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}bool{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{5E}{\isacharcircum}}\isanewline
10.613 \ \ \ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}\isanewline
10.614 \ \ \ \ \ {\isaliteral{2A}{\isacharasterisk}}\ {\isaliteral{28}{\isacharparenleft}}{\isadigit{1}}{\isaliteral{2F}{\isacharslash}}z{\isaliteral{29}{\isacharparenright}}\ instead\ of\ z\ {\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}\ {\isaliteral{2D}{\isacharminus}}{\isadigit{1}}\isanewline
10.615 \ \ \ \ \ {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline
10.616 -\ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{28}{\isacharparenleft}}let\ X\ {\isaliteral{3D}{\isacharequal}}\ Take\ Xeq{\isaliteral{3B}{\isacharsemicolon}}{\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{5E}{\isacharcircum}}\isanewline
10.617 -\ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ X{\isaliteral{27}{\isacharprime}}\ {\isaliteral{3D}{\isacharequal}}\ Rewrite\ ruleZY\ False\ X{\isaliteral{3B}{\isacharsemicolon}}{\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{5E}{\isacharcircum}}\isanewline
10.618 +\ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{28}{\isacharparenleft}}let\ X\ {\isaliteral{3D}{\isacharequal}}\ Take\ Xeq{\isaliteral{3B}{\isacharsemicolon}}\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{5E}{\isacharcircum}}\isanewline
10.619 +\ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ X{\isaliteral{27}{\isacharprime}}\ {\isaliteral{3D}{\isacharequal}}\ Rewrite\ ruleZY\ False\ X{\isaliteral{3B}{\isacharsemicolon}}\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{5E}{\isacharcircum}}\isanewline
10.620 \ \ \ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}\isanewline
10.621 \ \ \ \ \ {\isaliteral{2A}{\isacharasterisk}}\ z\ {\isaliteral{2A}{\isacharasterisk}}\ denominator\isanewline
10.622 \ \ \ \ \ {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline
10.623 -\ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ X{\isaliteral{27}{\isacharprime}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}Rewrite{\isaliteral{5F}{\isacharunderscore}}Set\ norm{\isaliteral{5F}{\isacharunderscore}}Rational\ False{\isaliteral{29}{\isacharparenright}}\ X{\isaliteral{27}{\isacharprime}}{\isaliteral{3B}{\isacharsemicolon}}{\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{5E}{\isacharcircum}}\isanewline
10.624 +\ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ X{\isaliteral{27}{\isacharprime}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}Rewrite{\isaliteral{5F}{\isacharunderscore}}Set\ norm{\isaliteral{5F}{\isacharunderscore}}Rational\ False{\isaliteral{29}{\isacharparenright}}\ X{\isaliteral{27}{\isacharprime}}{\isaliteral{3B}{\isacharsemicolon}}\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{5E}{\isacharcircum}}\isanewline
10.625 \ \ \ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}\isanewline
10.626 \ \ \ \ \ {\isaliteral{2A}{\isacharasterisk}}\ simplify\isanewline
10.627 \ \ \ \ \ {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline
10.628 -\ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ X{\isaliteral{27}{\isacharprime}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}SubProblem\ {\isaliteral{28}{\isacharparenleft}}Isac{\isaliteral{27}{\isacharprime}}{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5B}{\isacharbrackleft}}pqFormula{\isaliteral{2C}{\isacharcomma}}degree{\isaliteral{5F}{\isacharunderscore}}{\isadigit{2}}{\isaliteral{2C}{\isacharcomma}}{\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{5E}{\isacharcircum}}\isanewline
10.629 -\ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ polynomial{\isaliteral{2C}{\isacharcomma}}univariate{\isaliteral{2C}{\isacharcomma}}equation{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{2C}{\isacharcomma}}{\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{5E}{\isacharcircum}}\isanewline
10.630 -\ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{5B}{\isacharbrackleft}}no{\isaliteral{5F}{\isacharunderscore}}met{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}\ \ \ {\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{5E}{\isacharcircum}}\isanewline
10.631 -\ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{5B}{\isacharbrackleft}}BOOL\ e{\isaliteral{5F}{\isacharunderscore}}e{\isaliteral{2C}{\isacharcomma}}\ REAL\ v{\isaliteral{5F}{\isacharunderscore}}v{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{5E}{\isacharcircum}}\isanewline
10.632 +\ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ X{\isaliteral{27}{\isacharprime}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}SubProblem\ {\isaliteral{28}{\isacharparenleft}}Isac{\isaliteral{27}{\isacharprime}}{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5B}{\isacharbrackleft}}pqFormula{\isaliteral{2C}{\isacharcomma}}degree{\isaliteral{5F}{\isacharunderscore}}{\isadigit{2}}{\isaliteral{2C}{\isacharcomma}}\ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{5E}{\isacharcircum}}\isanewline
10.633 +\ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ polynomial{\isaliteral{2C}{\isacharcomma}}univariate{\isaliteral{2C}{\isacharcomma}}equation{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{5E}{\isacharcircum}}\isanewline
10.634 +\ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{5B}{\isacharbrackleft}}no{\isaliteral{5F}{\isacharunderscore}}met{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{5E}{\isacharcircum}}\isanewline
10.635 +\ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{5B}{\isacharbrackleft}}BOOL\ e{\isaliteral{5F}{\isacharunderscore}}e{\isaliteral{2C}{\isacharcomma}}\ REAL\ v{\isaliteral{5F}{\isacharunderscore}}v{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}\ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{5E}{\isacharcircum}}\isanewline
10.636 \ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ \ \ \ \ \ \ in\ X{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
10.637 {\isaliteral{2A7D}{\isacharverbatimclose}}%
10.638 \endisatagML
10.639 @@ -1975,7 +1990,7 @@
10.640 \endisadelimML
10.641 %
10.642 \begin{isamarkuptext}%
10.643 -\noindent To solve the equation it is neccessary to drop the left hand
10.644 +\noindent To solve the equation it is necessary to drop the left hand
10.645 side, now we only need the denominator of the right hand side. The first
10.646 equation solves the zeros of our expression.%
10.647 \end{isamarkuptext}%
10.648 @@ -1989,11 +2004,11 @@
10.649 \isacommand{ML}\isamarkupfalse%
10.650 \ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
10.651 \ \ val\ str\ {\isaliteral{3D}{\isacharequal}}\ \isanewline
10.652 -\ \ \ \ {\isaliteral{22}{\isachardoublequote}}Script\ InverseZTransform\ {\isaliteral{28}{\isacharparenleft}}Xeq{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}bool{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{5E}{\isacharcircum}}\isanewline
10.653 -\ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{28}{\isacharparenleft}}let\ X\ {\isaliteral{3D}{\isacharequal}}\ Take\ Xeq{\isaliteral{3B}{\isacharsemicolon}}{\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{5E}{\isacharcircum}}\isanewline
10.654 -\ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ X{\isaliteral{27}{\isacharprime}}\ {\isaliteral{3D}{\isacharequal}}\ Rewrite\ ruleZY\ False\ X{\isaliteral{3B}{\isacharsemicolon}}{\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{5E}{\isacharcircum}}\isanewline
10.655 -\ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ X{\isaliteral{27}{\isacharprime}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}Rewrite{\isaliteral{5F}{\isacharunderscore}}Set\ norm{\isaliteral{5F}{\isacharunderscore}}Rational\ False{\isaliteral{29}{\isacharparenright}}\ X{\isaliteral{27}{\isacharprime}}{\isaliteral{3B}{\isacharsemicolon}}{\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{5E}{\isacharcircum}}\isanewline
10.656 -\ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ funterm\ {\isaliteral{3D}{\isacharequal}}\ rhs\ X{\isaliteral{27}{\isacharprime}}{\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{5E}{\isacharcircum}}\ \isanewline
10.657 +\ \ \ \ {\isaliteral{22}{\isachardoublequote}}Script\ InverseZTransform\ {\isaliteral{28}{\isacharparenleft}}Xeq{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}bool{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{5E}{\isacharcircum}}\isanewline
10.658 +\ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{28}{\isacharparenleft}}let\ X\ {\isaliteral{3D}{\isacharequal}}\ Take\ Xeq{\isaliteral{3B}{\isacharsemicolon}}\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{5E}{\isacharcircum}}\isanewline
10.659 +\ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ X{\isaliteral{27}{\isacharprime}}\ {\isaliteral{3D}{\isacharequal}}\ Rewrite\ ruleZY\ False\ X{\isaliteral{3B}{\isacharsemicolon}}\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{5E}{\isacharcircum}}\isanewline
10.660 +\ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ X{\isaliteral{27}{\isacharprime}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}Rewrite{\isaliteral{5F}{\isacharunderscore}}Set\ norm{\isaliteral{5F}{\isacharunderscore}}Rational\ False{\isaliteral{29}{\isacharparenright}}\ X{\isaliteral{27}{\isacharprime}}{\isaliteral{3B}{\isacharsemicolon}}\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{5E}{\isacharcircum}}\isanewline
10.661 +\ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ funterm\ {\isaliteral{3D}{\isacharequal}}\ rhs\ X{\isaliteral{27}{\isacharprime}}\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{5E}{\isacharcircum}}\isanewline
10.662 \ \ \ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}\isanewline
10.663 \ \ \ \ \ {\isaliteral{2A}{\isacharasterisk}}\ drop\ X{\isaliteral{27}{\isacharprime}}{\isaliteral{3D}{\isacharequal}}\ for\ equation\ solving\isanewline
10.664 \ \ \ \ \ {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline
10.665 @@ -2021,23 +2036,23 @@
10.666 \isacommand{ML}\isamarkupfalse%
10.667 \ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
10.668 \ \ val\ str\ {\isaliteral{3D}{\isacharequal}}\ \isanewline
10.669 -\ \ \ \ {\isaliteral{22}{\isachardoublequote}}Script\ InverseZTransform\ {\isaliteral{28}{\isacharparenleft}}X{\isaliteral{5F}{\isacharunderscore}}eq{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}bool{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{5E}{\isacharcircum}}\ \isanewline
10.670 -\ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{28}{\isacharparenleft}}let\ X\ {\isaliteral{3D}{\isacharequal}}\ Take\ X{\isaliteral{5F}{\isacharunderscore}}eq{\isaliteral{3B}{\isacharsemicolon}}{\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{5E}{\isacharcircum}}\isanewline
10.671 -\ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ X{\isaliteral{27}{\isacharprime}}\ {\isaliteral{3D}{\isacharequal}}\ Rewrite\ ruleZY\ False\ X{\isaliteral{3B}{\isacharsemicolon}}{\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{5E}{\isacharcircum}}\ \isanewline
10.672 -\ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ X{\isaliteral{27}{\isacharprime}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}Rewrite{\isaliteral{5F}{\isacharunderscore}}Set\ norm{\isaliteral{5F}{\isacharunderscore}}Rational\ False{\isaliteral{29}{\isacharparenright}}\ X{\isaliteral{27}{\isacharprime}}{\isaliteral{3B}{\isacharsemicolon}}{\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{5E}{\isacharcircum}}\ \isanewline
10.673 -\ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}X{\isaliteral{27}{\isacharprime}}{\isaliteral{5F}{\isacharunderscore}}z{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}real{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ lhs\ X{\isaliteral{27}{\isacharprime}}{\isaliteral{3B}{\isacharsemicolon}}{\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{5E}{\isacharcircum}}\isanewline
10.674 -\ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}z{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}real{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ argument{\isaliteral{5F}{\isacharunderscore}}in\ X{\isaliteral{27}{\isacharprime}}{\isaliteral{5F}{\isacharunderscore}}z{\isaliteral{3B}{\isacharsemicolon}}{\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{5E}{\isacharcircum}}\isanewline
10.675 -\ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}funterm{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}real{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ rhs\ X{\isaliteral{27}{\isacharprime}}{\isaliteral{3B}{\isacharsemicolon}}{\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{5E}{\isacharcircum}}\ \isanewline
10.676 -\ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}denom{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}real{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ get{\isaliteral{5F}{\isacharunderscore}}denominator\ funterm{\isaliteral{3B}{\isacharsemicolon}}{\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{5E}{\isacharcircum}}\ \isanewline
10.677 +\ \ \ \ {\isaliteral{22}{\isachardoublequote}}Script\ InverseZTransform\ {\isaliteral{28}{\isacharparenleft}}X{\isaliteral{5F}{\isacharunderscore}}eq{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}bool{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{5E}{\isacharcircum}}\isanewline
10.678 +\ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{28}{\isacharparenleft}}let\ X\ {\isaliteral{3D}{\isacharequal}}\ Take\ X{\isaliteral{5F}{\isacharunderscore}}eq{\isaliteral{3B}{\isacharsemicolon}}\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{5E}{\isacharcircum}}\isanewline
10.679 +\ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ X{\isaliteral{27}{\isacharprime}}\ {\isaliteral{3D}{\isacharequal}}\ Rewrite\ ruleZY\ False\ X{\isaliteral{3B}{\isacharsemicolon}}\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{5E}{\isacharcircum}}\isanewline
10.680 +\ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ X{\isaliteral{27}{\isacharprime}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}Rewrite{\isaliteral{5F}{\isacharunderscore}}Set\ norm{\isaliteral{5F}{\isacharunderscore}}Rational\ False{\isaliteral{29}{\isacharparenright}}\ X{\isaliteral{27}{\isacharprime}}{\isaliteral{3B}{\isacharsemicolon}}\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{5E}{\isacharcircum}}\isanewline
10.681 +\ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}X{\isaliteral{27}{\isacharprime}}{\isaliteral{5F}{\isacharunderscore}}z{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}real{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ lhs\ X{\isaliteral{27}{\isacharprime}}{\isaliteral{3B}{\isacharsemicolon}}\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{5E}{\isacharcircum}}\isanewline
10.682 +\ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}z{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}real{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ argument{\isaliteral{5F}{\isacharunderscore}}in\ X{\isaliteral{27}{\isacharprime}}{\isaliteral{5F}{\isacharunderscore}}z{\isaliteral{3B}{\isacharsemicolon}}\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{5E}{\isacharcircum}}\isanewline
10.683 +\ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}funterm{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}real{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ rhs\ X{\isaliteral{27}{\isacharprime}}{\isaliteral{3B}{\isacharsemicolon}}\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{5E}{\isacharcircum}}\isanewline
10.684 +\ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}denom{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}real{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ get{\isaliteral{5F}{\isacharunderscore}}denominator\ funterm{\isaliteral{3B}{\isacharsemicolon}}\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{5E}{\isacharcircum}}\isanewline
10.685 \ \ \ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}\isanewline
10.686 \ \ \ \ \ {\isaliteral{2A}{\isacharasterisk}}\ get{\isaliteral{5F}{\isacharunderscore}}denominator\isanewline
10.687 \ \ \ \ \ {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline
10.688 -\ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}equ{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}bool{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}denom\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}{\isadigit{0}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}real{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}{\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{5E}{\isacharcircum}}\isanewline
10.689 -\ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}L{\isaliteral{5F}{\isacharunderscore}}L{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}bool\ list{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{5E}{\isacharcircum}}\isanewline
10.690 -\ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}SubProblem\ {\isaliteral{28}{\isacharparenleft}}Test{\isaliteral{27}{\isacharprime}}{\isaliteral{2C}{\isacharcomma}}\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{5E}{\isacharcircum}}\isanewline
10.691 -\ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{5B}{\isacharbrackleft}}linear{\isaliteral{2C}{\isacharcomma}}univariate{\isaliteral{2C}{\isacharcomma}}equation{\isaliteral{2C}{\isacharcomma}}test{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{5E}{\isacharcircum}}\isanewline
10.692 -\ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{5B}{\isacharbrackleft}}Test{\isaliteral{2C}{\isacharcomma}}solve{\isaliteral{5F}{\isacharunderscore}}linear{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{5E}{\isacharcircum}}\isanewline
10.693 -\ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{5B}{\isacharbrackleft}}BOOL\ equ{\isaliteral{2C}{\isacharcomma}}\ REAL\ z{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{5E}{\isacharcircum}}\isanewline
10.694 +\ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}equ{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}bool{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}denom\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}{\isadigit{0}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}real{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{5E}{\isacharcircum}}\isanewline
10.695 +\ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}L{\isaliteral{5F}{\isacharunderscore}}L{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}bool\ list{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{5E}{\isacharcircum}}\isanewline
10.696 +\ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}SubProblem\ {\isaliteral{28}{\isacharparenleft}}Test{\isaliteral{27}{\isacharprime}}{\isaliteral{2C}{\isacharcomma}}\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{5E}{\isacharcircum}}\isanewline
10.697 +\ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{5B}{\isacharbrackleft}}linear{\isaliteral{2C}{\isacharcomma}}univariate{\isaliteral{2C}{\isacharcomma}}equation{\isaliteral{2C}{\isacharcomma}}test{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{2C}{\isacharcomma}}\ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{5E}{\isacharcircum}}\isanewline
10.698 +\ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{5B}{\isacharbrackleft}}Test{\isaliteral{2C}{\isacharcomma}}solve{\isaliteral{5F}{\isacharunderscore}}linear{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{5E}{\isacharcircum}}\isanewline
10.699 +\ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{5B}{\isacharbrackleft}}BOOL\ equ{\isaliteral{2C}{\isacharcomma}}\ REAL\ z{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{5E}{\isacharcircum}}\isanewline
10.700 \ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ in\ X{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
10.701 \isanewline
10.702 \ \ parse\ thy\ str{\isaliteral{3B}{\isacharsemicolon}}\isanewline
10.703 @@ -2064,45 +2079,45 @@
10.704 \isatagML
10.705 \isacommand{ML}\isamarkupfalse%
10.706 \ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
10.707 -\ \ val\ srls\ {\isaliteral{3D}{\isacharequal}}\ Rls\ {\isaliteral{7B}{\isacharbraceleft}}id{\isaliteral{3D}{\isacharequal}}{\isaliteral{22}{\isachardoublequote}}srls{\isaliteral{5F}{\isacharunderscore}}InverseZTransform{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ \isanewline
10.708 -\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ preconds\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{2C}{\isacharcomma}}\isanewline
10.709 -\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ rew{\isaliteral{5F}{\isacharunderscore}}ord\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequote}}termlessI{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}termlessI{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\isanewline
10.710 -\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ erls\ {\isaliteral{3D}{\isacharequal}}\ append{\isaliteral{5F}{\isacharunderscore}}rls\ {\isaliteral{22}{\isachardoublequote}}erls{\isaliteral{5F}{\isacharunderscore}}in{\isaliteral{5F}{\isacharunderscore}}srls{\isaliteral{5F}{\isacharunderscore}}InverseZTransform{\isaliteral{22}{\isachardoublequote}}\ e{\isaliteral{5F}{\isacharunderscore}}rls\isanewline
10.711 -\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}for\ asm\ in\ NTH{\isaliteral{5F}{\isacharunderscore}}CONS\ {\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline
10.712 -\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Calc\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequote}}Orderings{\isaliteral{2E}{\isachardot}}ord{\isaliteral{5F}{\isacharunderscore}}class{\isaliteral{2E}{\isachardot}}less{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}eval{\isaliteral{5F}{\isacharunderscore}}equ\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{23}{\isacharhash}}less{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\isanewline
10.713 -\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}{\isadigit{2}}nd\ NTH{\isaliteral{5F}{\isacharunderscore}}CONS\ pushes\ n{\isaliteral{2B}{\isacharplus}}{\isaliteral{2D}{\isacharminus}}{\isadigit{1}}\ into\ asms{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline
10.714 -\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Calc{\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequote}}Groups{\isaliteral{2E}{\isachardot}}plus{\isaliteral{5F}{\isacharunderscore}}class{\isaliteral{2E}{\isachardot}}plus{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ eval{\isaliteral{5F}{\isacharunderscore}}binop\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{23}{\isacharhash}}add{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{29}{\isacharparenright}}\isanewline
10.715 -\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{5D}{\isacharbrackright}}{\isaliteral{2C}{\isacharcomma}}\ \isanewline
10.716 -\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ srls\ {\isaliteral{3D}{\isacharequal}}\ Erls{\isaliteral{2C}{\isacharcomma}}\ calc\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{2C}{\isacharcomma}}\isanewline
10.717 -\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ rules\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5B}{\isacharbrackleft}}\isanewline
10.718 -\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Thm\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequote}}NTH{\isaliteral{5F}{\isacharunderscore}}CONS{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}num{\isaliteral{5F}{\isacharunderscore}}str\ %
10.719 +\ \ val\ srls\ {\isaliteral{3D}{\isacharequal}}\ \isanewline
10.720 +\ \ \ \ Rls\ {\isaliteral{7B}{\isacharbraceleft}}id{\isaliteral{3D}{\isacharequal}}{\isaliteral{22}{\isachardoublequote}}srls{\isaliteral{5F}{\isacharunderscore}}InverseZTransform{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ \isanewline
10.721 +\ \ \ \ \ \ \ \ \ preconds\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{2C}{\isacharcomma}}\isanewline
10.722 +\ \ \ \ \ \ \ \ \ rew{\isaliteral{5F}{\isacharunderscore}}ord\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequote}}termlessI{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}termlessI{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\isanewline
10.723 +\ \ \ \ \ \ \ \ \ erls\ {\isaliteral{3D}{\isacharequal}}\ append{\isaliteral{5F}{\isacharunderscore}}rls\ {\isaliteral{22}{\isachardoublequote}}erls{\isaliteral{5F}{\isacharunderscore}}in{\isaliteral{5F}{\isacharunderscore}}srls{\isaliteral{5F}{\isacharunderscore}}InverseZTransform{\isaliteral{22}{\isachardoublequote}}\ e{\isaliteral{5F}{\isacharunderscore}}rls\isanewline
10.724 +\ \ \ \ \ \ \ \ \ \ \ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}for\ asm\ in\ NTH{\isaliteral{5F}{\isacharunderscore}}CONS\ {\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline
10.725 +\ \ \ \ \ \ \ \ \ \ \ \ Calc\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequote}}Orderings{\isaliteral{2E}{\isachardot}}ord{\isaliteral{5F}{\isacharunderscore}}class{\isaliteral{2E}{\isachardot}}less{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}eval{\isaliteral{5F}{\isacharunderscore}}equ\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{23}{\isacharhash}}less{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\isanewline
10.726 +\ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}{\isadigit{2}}nd\ NTH{\isaliteral{5F}{\isacharunderscore}}CONS\ pushes\ n{\isaliteral{2B}{\isacharplus}}{\isaliteral{2D}{\isacharminus}}{\isadigit{1}}\ into\ asms{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline
10.727 +\ \ \ \ \ \ \ \ \ \ \ \ Calc{\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequote}}Groups{\isaliteral{2E}{\isachardot}}plus{\isaliteral{5F}{\isacharunderscore}}class{\isaliteral{2E}{\isachardot}}plus{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ eval{\isaliteral{5F}{\isacharunderscore}}binop\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{23}{\isacharhash}}add{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{29}{\isacharparenright}}\isanewline
10.728 +\ \ \ \ \ \ \ \ \ \ \ {\isaliteral{5D}{\isacharbrackright}}{\isaliteral{2C}{\isacharcomma}}\ \isanewline
10.729 +\ \ \ \ \ \ \ \ \ srls\ {\isaliteral{3D}{\isacharequal}}\ Erls{\isaliteral{2C}{\isacharcomma}}\ calc\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{2C}{\isacharcomma}}\isanewline
10.730 +\ \ \ \ \ \ \ \ \ rules\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5B}{\isacharbrackleft}}\isanewline
10.731 +\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Thm\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequote}}NTH{\isaliteral{5F}{\isacharunderscore}}CONS{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}num{\isaliteral{5F}{\isacharunderscore}}str\ %
10.732 \isaantiq
10.733 thm\ NTH{\isaliteral{5F}{\isacharunderscore}}CONS{}%
10.734 \endisaantiq
10.735 {\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\isanewline
10.736 -\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Calc{\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequote}}Groups{\isaliteral{2E}{\isachardot}}plus{\isaliteral{5F}{\isacharunderscore}}class{\isaliteral{2E}{\isachardot}}plus{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ \isanewline
10.737 -\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ eval{\isaliteral{5F}{\isacharunderscore}}binop\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{23}{\isacharhash}}add{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\isanewline
10.738 -\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Thm\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequote}}NTH{\isaliteral{5F}{\isacharunderscore}}NIL{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}num{\isaliteral{5F}{\isacharunderscore}}str\ %
10.739 +\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Calc{\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequote}}Groups{\isaliteral{2E}{\isachardot}}plus{\isaliteral{5F}{\isacharunderscore}}class{\isaliteral{2E}{\isachardot}}plus{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ \isanewline
10.740 +\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ eval{\isaliteral{5F}{\isacharunderscore}}binop\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{23}{\isacharhash}}add{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\isanewline
10.741 +\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Thm\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequote}}NTH{\isaliteral{5F}{\isacharunderscore}}NIL{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}num{\isaliteral{5F}{\isacharunderscore}}str\ %
10.742 \isaantiq
10.743 thm\ NTH{\isaliteral{5F}{\isacharunderscore}}NIL{}%
10.744 \endisaantiq
10.745 {\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\isanewline
10.746 -\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Calc{\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequote}}Tools{\isaliteral{2E}{\isachardot}}lhs{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ eval{\isaliteral{5F}{\isacharunderscore}}lhs{\isaliteral{22}{\isachardoublequote}}eval{\isaliteral{5F}{\isacharunderscore}}lhs{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\isanewline
10.747 -\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Calc{\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequote}}Tools{\isaliteral{2E}{\isachardot}}rhs{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ eval{\isaliteral{5F}{\isacharunderscore}}rhs{\isaliteral{22}{\isachardoublequote}}eval{\isaliteral{5F}{\isacharunderscore}}rhs{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\isanewline
10.748 -\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Calc{\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequote}}Atools{\isaliteral{2E}{\isachardot}}argument{\isaliteral{27}{\isacharprime}}{\isaliteral{5F}{\isacharunderscore}}in{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\isanewline
10.749 -\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ eval{\isaliteral{5F}{\isacharunderscore}}argument{\isaliteral{5F}{\isacharunderscore}}in\ {\isaliteral{22}{\isachardoublequote}}Atools{\isaliteral{2E}{\isachardot}}argument{\isaliteral{27}{\isacharprime}}{\isaliteral{5F}{\isacharunderscore}}in{\isaliteral{22}{\isachardoublequote}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\isanewline
10.750 -\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Calc{\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequote}}Rational{\isaliteral{2E}{\isachardot}}get{\isaliteral{5F}{\isacharunderscore}}denominator{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\isanewline
10.751 -\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ eval{\isaliteral{5F}{\isacharunderscore}}get{\isaliteral{5F}{\isacharunderscore}}denominator\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{23}{\isacharhash}}get{\isaliteral{5F}{\isacharunderscore}}denominator{\isaliteral{22}{\isachardoublequote}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\isanewline
10.752 -\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Calc{\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequote}}Rational{\isaliteral{2E}{\isachardot}}get{\isaliteral{5F}{\isacharunderscore}}numerator{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\isanewline
10.753 -\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ eval{\isaliteral{5F}{\isacharunderscore}}get{\isaliteral{5F}{\isacharunderscore}}numerator\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{23}{\isacharhash}}get{\isaliteral{5F}{\isacharunderscore}}numerator{\isaliteral{22}{\isachardoublequote}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\isanewline
10.754 -\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Calc{\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequote}}Partial{\isaliteral{5F}{\isacharunderscore}}Fractions{\isaliteral{2E}{\isachardot}}factors{\isaliteral{5F}{\isacharunderscore}}from{\isaliteral{5F}{\isacharunderscore}}solution{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\isanewline
10.755 -\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ eval{\isaliteral{5F}{\isacharunderscore}}factors{\isaliteral{5F}{\isacharunderscore}}from{\isaliteral{5F}{\isacharunderscore}}solution\ \isanewline
10.756 -\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{23}{\isacharhash}}factors{\isaliteral{5F}{\isacharunderscore}}from{\isaliteral{5F}{\isacharunderscore}}solution{\isaliteral{22}{\isachardoublequote}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\isanewline
10.757 -\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Calc{\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequote}}Partial{\isaliteral{5F}{\isacharunderscore}}Fractions{\isaliteral{2E}{\isachardot}}drop{\isaliteral{5F}{\isacharunderscore}}questionmarks{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\isanewline
10.758 -\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ eval{\isaliteral{5F}{\isacharunderscore}}drop{\isaliteral{5F}{\isacharunderscore}}questionmarks\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{23}{\isacharhash}}drop{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{3F}{\isacharquery}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{29}{\isacharparenright}}\isanewline
10.759 -\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{5D}{\isacharbrackright}}{\isaliteral{2C}{\isacharcomma}}\isanewline
10.760 -\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ scr\ {\isaliteral{3D}{\isacharequal}}\ EmptyScr\isanewline
10.761 -\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{7D}{\isacharbraceright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
10.762 +\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Calc{\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequote}}Tools{\isaliteral{2E}{\isachardot}}lhs{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ eval{\isaliteral{5F}{\isacharunderscore}}lhs{\isaliteral{22}{\isachardoublequote}}eval{\isaliteral{5F}{\isacharunderscore}}lhs{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\isanewline
10.763 +\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Calc{\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequote}}Tools{\isaliteral{2E}{\isachardot}}rhs{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ eval{\isaliteral{5F}{\isacharunderscore}}rhs{\isaliteral{22}{\isachardoublequote}}eval{\isaliteral{5F}{\isacharunderscore}}rhs{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\isanewline
10.764 +\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Calc{\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequote}}Atools{\isaliteral{2E}{\isachardot}}argument{\isaliteral{27}{\isacharprime}}{\isaliteral{5F}{\isacharunderscore}}in{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\isanewline
10.765 +\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ eval{\isaliteral{5F}{\isacharunderscore}}argument{\isaliteral{5F}{\isacharunderscore}}in\ {\isaliteral{22}{\isachardoublequote}}Atools{\isaliteral{2E}{\isachardot}}argument{\isaliteral{27}{\isacharprime}}{\isaliteral{5F}{\isacharunderscore}}in{\isaliteral{22}{\isachardoublequote}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\isanewline
10.766 +\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Calc{\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequote}}Rational{\isaliteral{2E}{\isachardot}}get{\isaliteral{5F}{\isacharunderscore}}denominator{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\isanewline
10.767 +\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ eval{\isaliteral{5F}{\isacharunderscore}}get{\isaliteral{5F}{\isacharunderscore}}denominator\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{23}{\isacharhash}}get{\isaliteral{5F}{\isacharunderscore}}denominator{\isaliteral{22}{\isachardoublequote}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\isanewline
10.768 +\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Calc{\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequote}}Rational{\isaliteral{2E}{\isachardot}}get{\isaliteral{5F}{\isacharunderscore}}numerator{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\isanewline
10.769 +\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ eval{\isaliteral{5F}{\isacharunderscore}}get{\isaliteral{5F}{\isacharunderscore}}numerator\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{23}{\isacharhash}}get{\isaliteral{5F}{\isacharunderscore}}numerator{\isaliteral{22}{\isachardoublequote}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\isanewline
10.770 +\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Calc{\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequote}}Partial{\isaliteral{5F}{\isacharunderscore}}Fractions{\isaliteral{2E}{\isachardot}}factors{\isaliteral{5F}{\isacharunderscore}}from{\isaliteral{5F}{\isacharunderscore}}solution{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\isanewline
10.771 +\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ eval{\isaliteral{5F}{\isacharunderscore}}factors{\isaliteral{5F}{\isacharunderscore}}from{\isaliteral{5F}{\isacharunderscore}}solution\ \isanewline
10.772 +\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{23}{\isacharhash}}factors{\isaliteral{5F}{\isacharunderscore}}from{\isaliteral{5F}{\isacharunderscore}}solution{\isaliteral{22}{\isachardoublequote}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\isanewline
10.773 +\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Calc{\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequote}}Partial{\isaliteral{5F}{\isacharunderscore}}Fractions{\isaliteral{2E}{\isachardot}}drop{\isaliteral{5F}{\isacharunderscore}}questionmarks{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\isanewline
10.774 +\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ eval{\isaliteral{5F}{\isacharunderscore}}drop{\isaliteral{5F}{\isacharunderscore}}questionmarks\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{23}{\isacharhash}}drop{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{3F}{\isacharquery}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{29}{\isacharparenright}}\isanewline
10.775 +\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{5D}{\isacharbrackright}}{\isaliteral{2C}{\isacharcomma}}\isanewline
10.776 +\ \ \ \ \ \ \ \ \ scr\ {\isaliteral{3D}{\isacharequal}}\ EmptyScr{\isaliteral{7D}{\isacharbraceright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
10.777 {\isaliteral{2A7D}{\isacharverbatimclose}}%
10.778 \endisatagML
10.779 {\isafoldML}%
10.780 @@ -2118,7 +2133,7 @@
10.781 \begin{isamarkuptext}%
10.782 \noindent After we also tested how to write scripts and run them,
10.783 we start creating the final version of our script and store it into
10.784 - the method for which we created a node in section~\ref{sec:cparentnode}
10.785 + the method for which we created a node in Section~\ref{sec:cparentnode}
10.786 Note that we also did this stepwise, but we didn't kept every
10.787 subversion.%
10.788 \end{isamarkuptext}%
10.789 @@ -2180,8 +2195,8 @@
10.790 \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ eq\ {\isaliteral{3D}{\isacharequal}}\ drop{\isaliteral{5F}{\isacharunderscore}}questionmarks\ eq{\isaliteral{3B}{\isacharsemicolon}}\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{5E}{\isacharcircum}}\isanewline
10.791 \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}z{\isadigit{1}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}real{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}rhs\ {\isaliteral{28}{\isacharparenleft}}NTH\ {\isadigit{1}}\ L{\isaliteral{5F}{\isacharunderscore}}L{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{5E}{\isacharcircum}}\isanewline
10.792 \ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}\ \isanewline
10.793 -\ \ \ \ \ \ {\isaliteral{2A}{\isacharasterisk}}\ prepare\ equliation\ for\ a\ {\isaliteral{2D}{\isacharminus}}\ eq{\isaliteral{5F}{\isacharunderscore}}a\isanewline
10.794 -\ \ \ \ \ \ {\isaliteral{2A}{\isacharasterisk}}\ therfor\ subsitude\ z\ with\ solution\ {\isadigit{1}}\ {\isaliteral{2D}{\isacharminus}}\ z{\isadigit{1}}\isanewline
10.795 +\ \ \ \ \ \ {\isaliteral{2A}{\isacharasterisk}}\ prepare\ equation\ for\ a\ {\isaliteral{2D}{\isacharminus}}\ eq{\isaliteral{5F}{\isacharunderscore}}a\isanewline
10.796 +\ \ \ \ \ \ {\isaliteral{2A}{\isacharasterisk}}\ therefor\ substitute\ z\ with\ solution\ {\isadigit{1}}\ {\isaliteral{2D}{\isacharminus}}\ z{\isadigit{1}}\isanewline
10.797 \ \ \ \ \ \ {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline
10.798 \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}z{\isadigit{2}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}real{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}rhs\ {\isaliteral{28}{\isacharparenleft}}NTH\ {\isadigit{2}}\ L{\isaliteral{5F}{\isacharunderscore}}L{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{5E}{\isacharcircum}}\isanewline
10.799 \ \isanewline
10.800 @@ -2205,16 +2220,14 @@
10.801 \isanewline
10.802 \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ eqr\ {\isaliteral{3D}{\isacharequal}}\ drop{\isaliteral{5F}{\isacharunderscore}}questionmarks\ eqr{\isaliteral{3B}{\isacharsemicolon}}\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{5E}{\isacharcircum}}\isanewline
10.803 \ \ \ \ \ {\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
10.804 -\ \ \ \ \ {\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
10.805 -\ \ \ \ \ {\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
10.806 +\ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ pbz\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{28}{\isacharparenleft}}Substitute\ {\isaliteral{5B}{\isacharbrackleft}}A{\isaliteral{3D}{\isacharequal}}a{\isaliteral{2C}{\isacharcomma}}\ 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
10.807 \isanewline
10.808 \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ pbz\ {\isaliteral{3D}{\isacharequal}}\ Rewrite\ ruleYZ\ False\ pbz{\isaliteral{3B}{\isacharsemicolon}}\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{5E}{\isacharcircum}}\isanewline
10.809 \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ pbz\ {\isaliteral{3D}{\isacharequal}}\ drop{\isaliteral{5F}{\isacharunderscore}}questionmarks\ pbz{\isaliteral{3B}{\isacharsemicolon}}\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{5E}{\isacharcircum}}\isanewline
10.810 \isanewline
10.811 -\ \ \ \ \ {\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
10.812 -\ \ \ \ \ {\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
10.813 -\ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ iztrans\ {\isaliteral{3D}{\isacharequal}}\ drop{\isaliteral{5F}{\isacharunderscore}}questionmarks\ iztrans{\isaliteral{3B}{\isacharsemicolon}}\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{5E}{\isacharcircum}}\isanewline
10.814 -\ \ \ \ \ {\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
10.815 +\ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}X{\isaliteral{5F}{\isacharunderscore}}z{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}bool{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ Take\ {\isaliteral{28}{\isacharparenleft}}X{\isaliteral{5F}{\isacharunderscore}}z\ {\isaliteral{3D}{\isacharequal}}\ pbz{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{5E}{\isacharcircum}}\isanewline
10.816 +\ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}n{\isaliteral{5F}{\isacharunderscore}}eq{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}bool{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}Rewrite{\isaliteral{5F}{\isacharunderscore}}Set\ inverse{\isaliteral{5F}{\isacharunderscore}}z\ False{\isaliteral{29}{\isacharparenright}}\ X{\isaliteral{5F}{\isacharunderscore}}z{\isaliteral{3B}{\isacharsemicolon}}\ \ \ \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{5E}{\isacharcircum}}\isanewline
10.817 +\ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ n{\isaliteral{5F}{\isacharunderscore}}eq\ {\isaliteral{3D}{\isacharequal}}\ drop{\isaliteral{5F}{\isacharunderscore}}questionmarks\ n{\isaliteral{5F}{\isacharunderscore}}eq\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{5E}{\isacharcircum}}\isanewline
10.818 \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}in\ n{\isaliteral{5F}{\isacharunderscore}}eq{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}\ \isanewline
10.819 \ \ \ \ {\isaliteral{29}{\isacharparenright}}\isanewline
10.820 \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
10.821 @@ -2241,7 +2254,7 @@
10.822 %
10.823 \begin{isamarkuptext}%
10.824 \noindent First we want to check the formalization of the in and
10.825 - output of our programm.%
10.826 + output of our program.%
10.827 \end{isamarkuptext}%
10.828 \isamarkuptrue%
10.829 %
10.830 @@ -2295,7 +2308,7 @@
10.831 \isamarkuptrue%
10.832 %
10.833 \begin{isamarkuptext}%
10.834 -\noindent We start to stepwise execute our new programm in a calculation
10.835 +\noindent We start to stepwise execute our new program in a calculation
10.836 tree and check if every node implements that what we have wanted.%
10.837 \end{isamarkuptext}%
10.838 \isamarkuptrue%
10.839 @@ -2355,32 +2368,34 @@
10.840 \noindent Instead of \ttfamily nxt = Subproblem \normalfont above we had
10.841 \ttfamily Empty\_Tac; \normalfont the search for the reason considered
10.842 the following points:\begin{itemize}
10.843 - \item What shows \ttfamily show\_pt pt;\normalfont\ldots?\\
10.844 - \ttfamily ((\lbrack 2\rbrack, Res), ?X' z = 24 /
10.845 - (-1 + -2 * z + 8 * z \^\^\^ ~2))\rbrack\normalfont\\
10.846 + \item What shows \ttfamily show\_pt pt;\normalfont\ldots?
10.847 +\begin{verbatim}(([2], Res), ?X' z = 24 / (-1 + -2 * z + 8 * z ^^^ 2))]\end{verbatim}
10.848 The calculation is ok but no \ttfamily next \normalfont step found:
10.849 Should be\\ \ttfamily nxt = Subproblem\normalfont!
10.850 \item What shows \ttfamily trace\_script := true; \normalfont we read
10.851 - bottom up\ldots\\
10.852 - \ttfamily @@@next leaf 'SubProbfrom\\
10.853 - (PolyEq',\\
10.854 - \lbrack abcFormula, degree\_2, polynomial, univariate,
10.855 - equation\rbrack,\\
10.856 - no\_meth)\\
10.857 - \lbrack BOOL equ, REAL z\rbrack' ---> STac 'SubProblem\\
10.858 - (PolyEq',\\
10.859 - [abcFormula, degree\_2, polynomial, univariate, equation],\\
10.860 - no\_meth)\\
10.861 - \lbrack BOOL (-1 + -2 * z + 8 * z \^\^\^ ~2 = 0),
10.862 - REAL z\rbrack'\normalfont\\
10.863 + bottom up\ldots
10.864 + \begin{verbatim}
10.865 + @@@next leaf 'SubProblem
10.866 + (PolyEq',[abcFormula, degree_2, polynomial,
10.867 + univariate, equation], no_meth)
10.868 + [BOOL equ, REAL z]'
10.869 + ---> STac 'SubProblem (PolyEq',
10.870 + [abcFormula, degree_2, polynomial,
10.871 + univariate, equation], no_meth)
10.872 + [BOOL (-1 + -2 * z + 8 * z \^\^\^ ~2 = 0), REAL z]'
10.873 + \end{verbatim}
10.874 We see the SubProblem with correct arguments from searching next
10.875 step (program text !!!--->!!! STac (script tactic) with arguments
10.876 evaluated.)
10.877 \item Do we have the right Script \ldots difference in the
10.878 - argumentsdifference in the arguments\ldots\\
10.879 - \ttfamily val Script s =\\
10.880 - (#scr o get\_met) ["SignalProcessing","Z\_Transform","inverse"];\\
10.881 - writeln (term2str s);\normalfont\\
10.882 + arguments in the arguments\ldots
10.883 + \begin{verbatim}
10.884 + val Script s =
10.885 + (#scr o get_met) ["SignalProcessing",
10.886 + "Z_Transform",
10.887 + "inverse"];
10.888 + writeln (term2str s);
10.889 + \end{verbatim}
10.890 \ldots shows the right script. Difference in the arguments.
10.891 \item Test --- Why helpless here ? --- shows: \ttfamily replace
10.892 no\_meth by [no\_meth] \normalfont in Script
10.893 @@ -2410,7 +2425,7 @@
10.894 we had \ttfamily Empty\_Tac; \normalfont the search for the reason
10.895 considered the following points:\begin{itemize}
10.896 \item Difference in the arguments
10.897 - \item Comparison with subsection~ref{sec:solveq}: There solving this
10.898 + \item Comparison with Subsection~\ref{sec:solveq}: There solving this
10.899 equation works, so there must be some difference in the arguments
10.900 of the Subproblem: RIGHT: we had \ttfamily [no\_meth] \normalfont
10.901 instead of \ttfamily [no\_met] \normalfont ;-)
10.902 @@ -2448,14 +2463,16 @@
10.903 \item Was there an error message? NO -- ok
10.904 \item Has \ttfamily nxt = Add\_Find \normalfont been inserted in pt:\\
10.905 \ttfamily get\_obj g\_pbl pt (fst p);\normalfont? YES -- ok
10.906 - \item What is the returned formula:
10.907 - \ttfamily print\_depth 999; f; print\_depth 999;\\
10.908 - \lbrace Find = \lbrack Correct "solutions z\_i"\rbrack,
10.909 - With = \lbrack\rbrack,\\
10.910 - Given = \lbrack Correct "equality (-1 + -2 * z + 8 * z ^^^ 2 = 0)",
10.911 - Correct "solveFor z"\rbrack,\\
10.912 - Where = \lbrack \ldots \rbrack,
10.913 - Relate = \lbrack\rbrack\rbrace $ \normalfont\\
10.914 + \item What is the returned formula:
10.915 +\begin{verbatim}
10.916 +print_depth 999; f; print_depth 999;
10.917 +{ Find = [ Correct "solutions z_i"],
10.918 + With = [],
10.919 + Given = [Correct "equality (-1 + -2*z + 8*z ^^^ 2 = 0)",
10.920 + Correct "solveFor z"],
10.921 + Where = [...],
10.922 + Relate = [] }
10.923 +\end{verbatim}
10.924 \normalfont The only False is the reason: the Where (the precondition) is
10.925 False for good reasons: The precondition seems to check for linear
10.926 equations, not for the one we want to solve! Removed this error by
10.927 @@ -2595,27 +2612,116 @@
10.928 \end{isamarkuptext}%
10.929 \isamarkuptrue%
10.930 %
10.931 -\isadelimML
10.932 -%
10.933 -\endisadelimML
10.934 -%
10.935 -\isatagML
10.936 -\isacommand{ML}\isamarkupfalse%
10.937 -\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
10.938 -\ \ trace{\isaliteral{5F}{\isacharunderscore}}script\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3D}{\isacharequal}}\ true{\isaliteral{3B}{\isacharsemicolon}}\isanewline
10.939 -\ \ 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
10.940 -\ \ show{\isaliteral{5F}{\isacharunderscore}}pt\ pt{\isaliteral{3B}{\isacharsemicolon}}\isanewline
10.941 -{\isaliteral{2A7D}{\isacharverbatimclose}}%
10.942 -\endisatagML
10.943 -{\isafoldML}%
10.944 -%
10.945 -\isadelimML
10.946 -%
10.947 -\endisadelimML
10.948 -\isanewline
10.949 +\isamarkupsection{Improve and Transfer into Knowledge%
10.950 +}
10.951 +\isamarkuptrue%
10.952 +%
10.953 +\begin{isamarkuptext}%
10.954 +We want to improve the very long program \ttfamily InverseZTransform
10.955 + \normalfont by modularisation: partial fraction decomposition shall
10.956 + become a sub-problem.
10.957 +
10.958 + We could transfer all knowledge in \ttfamily Build\_Inverse\_Z\_Transform.thy
10.959 + \normalfont first to the \ttfamily Knowledge/Inverse\_Z\_Transform.thy
10.960 + \normalfont and then modularise. In this case TODO problems?!?
10.961 +
10.962 + We chose another way and go bottom up: first we build the sub-problem in
10.963 + \ttfamily Partial\_Fractions.thy \normalfont with the term:
10.964 +
10.965 + $$\frac{3}{x\cdot(z - \frac{1}{4} + \frac{-1}{8}\cdot\frac{1}{z})}$$
10.966 +
10.967 + \noindent (how this still can be improved see \ttfamily Partial\_Fractions.thy\normalfont),
10.968 + and re-use all stuff prepared in \ttfamily Build\_Inverse\_Z\_Transform.thy:
10.969 + \normalfont The knowledge will be transferred to \ttfamily src/../Partial\_Fractions.thy
10.970 + \normalfont and the respective tests to:
10.971 + \begin{center}\ttfamily test/../sartial\_fractions.sml\normalfont\end{center}%
10.972 +\end{isamarkuptext}%
10.973 +\isamarkuptrue%
10.974 +%
10.975 +\isamarkupsubsection{Transfer to Partial\_Fractions.thy%
10.976 +}
10.977 +\isamarkuptrue%
10.978 +%
10.979 +\begin{isamarkuptext}%
10.980 +First we transfer both, knowledge and tests into:
10.981 + \begin{center}\ttfamily src/../Partial\_Fractions.thy\normalfont\end{center}
10.982 + in order to immediately have the test results.
10.983 +
10.984 + We copy \ttfamily factors\_from\_solution, drop\_questionmarks,\\
10.985 + ansatz\_2nd\_order \normalfont and rule-sets --- no problem.
10.986 +
10.987 + Also \ttfamily store\_pbt ..\\ "pbl\_simp\_rat\_partfrac"
10.988 + \normalfont is easy.
10.989 +
10.990 + But then we copy from:\\
10.991 + (1) \ttfamily Build\_Inverse\_Z\_Transform.thy store\_met\ldots "met\_SP\_Ztrans\_inv"
10.992 + \normalfont\\ to\\
10.993 + (2) \ttfamily Partial\_Fractions.thy store\_met\ldots "met\_SP\_Ztrans\_inv"
10.994 + \normalfont\\ and cut out the respective part from the program. First we ensure that
10.995 + the string is correct. When we insert the string into (2)
10.996 + \ttfamily store\_met .. "met\_partial\_fraction" \normalfont --- and get an error.%
10.997 +\end{isamarkuptext}%
10.998 +\isamarkuptrue%
10.999 +%
10.1000 +\isamarkupsubsubsection{'Programming' in ISAC's TP-based Language%
10.1001 +}
10.1002 +\isamarkuptrue%
10.1003 +%
10.1004 +\begin{isamarkuptext}%
10.1005 +At the present state writing programs in {\sisac} is particularly cumbersome.
10.1006 + So we give hints how to cope with the many obstacles. Below we describe the
10.1007 + steps we did in making (2) run.
10.1008 +
10.1009 + \begin{enumerate}
10.1010 + \item We check if the \textbf{string} containing the program is correct.
10.1011 + \item We check if the \textbf{types in the program} are correct.
10.1012 + For this purpose we start start with the first and last lines
10.1013 + \begin{verbatim}
10.1014 + "PartFracScript (f_f::real) (v_v::real) = " ^
10.1015 + " (let X = Take f_f; " ^
10.1016 + " pbz = ((Substitute []) X) " ^
10.1017 + " in pbz)"
10.1018 + \end{verbatim}
10.1019 + The last but one line helps not to bother with ';'.
10.1020 + \item Then we add line by line. Already the first line causes the error.
10.1021 + So we investigate it by
10.1022 + \begin{verbatim}
10.1023 + val ctxt = ProofContext.init_global @ { theory } ;
10.1024 + val SOME t =
10.1025 + parseNEW ctxt "(num_orig::real) =
10.1026 + get_numerator(rhs f_f)";
10.1027 + \end{verbatim}
10.1028 + and see a type clash: \ttfamily rhs \normalfont from (1) requires type
10.1029 + \ttfamily bool \normalfont while (2) wants to have \ttfamily (f\_f::real).
10.1030 + \normalfont Of course, we don't need \ttfamily rhs \normalfont anymore.
10.1031 + \item Type-checking can be very tedious. One might even inspect the
10.1032 + parse-tree of the program with {\sisac}'s specific debug tools:
10.1033 + \begin{verbatim}
10.1034 + val {scr = Script t,...} =
10.1035 + get_met ["simplification",
10.1036 + "of_rationals",
10.1037 + "to_partial_fraction"];
10.1038 + atomty_thy @ { theory } t ;
10.1039 + \end{verbatim}
10.1040 + \item We check if the \textbf{semantics of the program} by stepwise evaluation
10.1041 + of the program. Evaluation is done by the Lucas-Interpreter, which works
10.1042 + using the knowledge in theory Isac; so we have to re-build Isac. And the
10.1043 + test are performed simplest in a file which is loaded with Isac.
10.1044 + See \ttfamily tests/../partial\_fractions.sml \normalfont.
10.1045 + \end{enumerate}%
10.1046 +\end{isamarkuptext}%
10.1047 +\isamarkuptrue%
10.1048 +%
10.1049 +\isamarkupsubsection{Transfer to Inverse\_Z\_Transform.thy%
10.1050 +}
10.1051 +\isamarkuptrue%
10.1052 +%
10.1053 +\begin{isamarkuptext}%
10.1054 +Unfortunately it was not possible to complete this task. Because we ran out of time\ldots%
10.1055 +\end{isamarkuptext}%
10.1056 +\isamarkuptrue%
10.1057 %
10.1058 \isadelimtheory
10.1059 -\isanewline
10.1060 %
10.1061 \endisadelimtheory
10.1062 %
