neuper@42074: neuper@42074: \documentclass{beamer} neuper@42074: neuper@42074: neuper@42074: \mode neuper@42074: { neuper@42074: \usetheme{Hannover} neuper@42074: \setbeamercovered{transparent} neuper@42074: } neuper@42074: neuper@42074: \usepackage[english]{babel} neuper@42074: \usepackage[utf8]{inputenc} neuper@42074: \usepackage{times} neuper@42074: \usepackage[T1]{fontenc} neuper@42074: neuper@42074: \def\isac{${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$} neuper@42074: \def\sisac{{\footnotesize${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$}} neuper@42074: jan@42163: \title[SPSC in \isac] % (optional, use only with long paper titles) jan@42163: {Interactive Course Material\\ for Signal Processing\\ based on Isabelle/\isac} neuper@42074: jan@42163: \subtitle{Baccalaureate Thesis} neuper@42074: jan@42175: \author[Ro\v{c}nik] jan@42175: {Jan Rocnik} neuper@42074: neuper@42074: \institute % (optional, but mostly needed) neuper@42074: { neuper@42074: Technische Universit\"at Graz\\ neuper@42074: Institut f\"ur TODO neuper@42074: } neuper@42074: neuper@42074: % If you have a file called "university-logo-filename.xxx", where xxx neuper@42074: % is a graphic format that can be processed by latex or pdflatex, neuper@42074: % resp., then you can add a logo as follows: neuper@42074: neuper@42074: % \pgfdeclareimage[height=0.5cm]{university-logo}{university-logo-filename} neuper@42074: % \logo{\pgfuseimage{university-logo}} neuper@42074: neuper@42074: neuper@42074: neuper@42074: % Delete this, if you do not want the table of contents to pop up at neuper@42074: % the beginning of each subsection: neuper@42074: \AtBeginSubsection[] neuper@42074: { neuper@42074: \begin{frame}{Outline} neuper@42074: \tableofcontents[currentsection,currentsubsection] neuper@42074: \end{frame} neuper@42074: } neuper@42074: neuper@42074: \begin{document} neuper@42074: neuper@42122: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% neuper@42122: %% Title Page %% neuper@42122: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% neuper@42122: neuper@42074: \begin{frame} neuper@42074: \titlepage neuper@42074: \end{frame} neuper@42074: neuper@42122: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% neuper@42122: %% Table of Contents %% neuper@42122: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% neuper@42122: neuper@42074: \begin{frame}{Outline} neuper@42074: \tableofcontents neuper@42074: % You might wish to add the option [pausesections] neuper@42074: \end{frame} neuper@42074: neuper@42122: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% neuper@42122: %%---------------------------------------------------------------%% neuper@42122: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% neuper@42074: jan@42163: \section[Intro]{Introduction} jan@42163: jan@42175: \begin{frame}{Issues to be Accomplished} jan@42163: jan@42163: \begin{itemize} jan@42163: jan@42183: \item What knowledge is already mechanised in \emph{Isabelle}? jan@42163: \item How can missing theorems and definitions be mechanised? jan@42163: \item What is the effort for such mechanisation? jan@42175: \item How do calculations look like, by using mechanised knowledge? jan@42175: \item What problems and subproblems have to be solved? jan@42163: \item Which problems are already implemented in \sisac? jan@42175: \item How are the new problems specified (\sisac)? jan@42175: \item Which variantes of programms in \sisac\ solve the problems? jan@42163: \item What is the contents of the interactiv course material (Figures, etc.)? jan@42163: jan@42163: \end{itemize} jan@42163: \end{frame} jan@42163: jan@42163: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% jan@42163: %%---------------------------------------------------------------%% jan@42163: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% jan@42163: jan@42175: \section[Fourier]{Fourier transformation} jan@42175: \subsection[Fourier]{Fourier transform} neuper@42122: neuper@42122: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% neuper@42122: %% Fourier INTRO %% neuper@42122: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% neuper@42122: neuper@42122: \begin{frame}\frametitle{Fourier Transformation: Introduction} jan@42191: Possibilities: neuper@42122: \begin{itemize} jan@42175: \item Transform operation by using property-tables jan@42175: \item Transform operation by using integral jan@42191: \end{itemize} jan@42191: Also Important: jan@42191: \begin{itemize} jan@42191: \item Visualisation?! neuper@42122: \end{itemize} neuper@42074: \end{frame} neuper@42074: neuper@42122: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% jan@42175: %% Transform expl SPEC %% neuper@42122: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% neuper@42122: jan@42175: \begin{frame}\frametitle{Fourier Transformation: Specification} jan@42175: {\footnotesize jrocnik@42159: jan@42175: Determine the fourier transform for the given rectangular impulse: jrocnik@42159: jrocnik@42159: \begin{center} jrocnik@42159: $x(t)= \left\{ jrocnik@42159: \begin{array}{lr} jan@42163: 1 & -1\leq t\leq1\\ jrocnik@42159: 0 & else jrocnik@42159: \end{array} jrocnik@42159: \right.$ jrocnik@42159: \end{center} jrocnik@42159: jan@42175: \hrulefill jan@42175: neuper@42076: \begin{tabbing} neuper@42076: 1\=postcond \=: \= \= $\;\;\;\;$\=\kill neuper@42076: \>given \>:\> piecewise\_function \\ jan@42191: \> \> \> \>$fun (x (t::real),\ x=1\ ((t>=-1)\ \&\ (t<=1)),\ x=0)$\\ neuper@42076: \>precond \>:\> TODO\\ neuper@42076: \>find \>:\> $X(j\cdot\omega)$\\ neuper@42076: \>postcond \>:\> TODO\\ neuper@42076: \end{tabbing} neuper@42076: neuper@42076: } neuper@42076: \end{frame} neuper@42076: neuper@42122: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% jan@42175: %% Transform expl REQ %% neuper@42122: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% neuper@42122: jan@42175: \begin{frame}\frametitle{Fourier Transform: Development effort} neuper@42122: {\small neuper@42122: \begin{center} neuper@42122: \begin{tabular}{l|l|r} neuper@42122: requirements & comments &effort\\ \hline\hline neuper@42122: solving Intrgrals & simple via propertie table & 20\\ neuper@42122: & \emph{real} & MT\\ \hline neuper@42122: transformation table & simple transform & 20\\ \hline neuper@42122: visualisation & backend & 10\\ \hline neuper@42122: example collection & with explanations & 20\\ \hline\hline neuper@42122: & & 70-80\\ neuper@42122: \end{tabular} neuper@42122: \end{center} neuper@42122: effort --- in 45min units\\ neuper@42122: MT --- thesis ``Integrals'' (mathematics) neuper@42122: } neuper@42074: \end{frame} jan@42163: jan@42163: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% jan@42163: %%--------------------FOURIER---Conclusion-----------------------%% jan@42163: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% jan@42163: jan@42175: \begin{frame}{Fourier Transformation: Summary} jan@42163: \begin{itemize} jan@42163: jan@42175: \item Standard integrals can be solved with tables jan@42183: \item No real integration (yet avaible) jan@42175: \item Math \emph{tricks} difficult to implement jan@42175: jan@42163: jan@42163: \end{itemize} jan@42163: \end{frame} jan@42163: neuper@42122: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% neuper@42122: %-----------------------------------------------------------------% neuper@42122: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% neuper@42074: jan@42175: \section[LTI Systems]{LTI systems} jan@42183: \subsection[Convolution]{Convolution (Faltung)} neuper@42122: neuper@42122: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% jan@42173: %% LTI INTRO %% neuper@42122: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% neuper@42122: neuper@42122: \begin{frame}\frametitle{Convolution: Introduction} neuper@42122: \begin{itemize} jan@42191: \item Calculation include sums jan@42191: \item Demonstrative examples jan@42191: \item Visualisation is important neuper@42122: \end{itemize} neuper@42122: \end{frame} neuper@42122: neuper@42122: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% jan@42173: %% LTI SPEC %% neuper@42122: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% neuper@42122: neuper@42122: \begin{frame}\frametitle{Convolution: Specification} jan@42175: {\footnotesize jrocnik@42159: jrocnik@42159: Consider the two discrete-time, linear and time-invariant (LTI) systems with the following impulse response: jrocnik@42159: jrocnik@42159: \begin{center} jrocnik@42159: $h_1[n]=\left(\frac{3}{5}\right)^n\cdot u[n]$\\ jrocnik@42159: $h_1[n]=\left(-\frac{2}{3}\right)^n\cdot u[n]$ jrocnik@42159: \end{center} jrocnik@42159: jrocnik@42159: The two systems are cascaded seriell. Derive the impulse respinse of the overall system $h_c[n]$. jrocnik@42159: jan@42173: \hrulefill jan@42191: neuper@42122: \begin{tabbing} neuper@42122: 1\=postcond \=: \= \= $\;\;\;\;$\=\kill neuper@42122: \>given \>:\> Signals h1[n], h2[n] \\ jan@42191: \> \> \> \>((h1[n]=(3/5)\textasciicircum{}n*u[n]),\,h2[n]=(-2/3)\textasciicircum{}n*u[n]))\\ jan@42191: neuper@42122: \>precond \>:\> TODO\\ neuper@42122: \>find \>:\> $h1[n]\,*\,h2[n]$\\ neuper@42122: \>postcond \>:\> TODO\\ neuper@42122: \end{tabbing} neuper@42122: neuper@42122: } neuper@42122: \end{frame} neuper@42122: neuper@42122: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% jan@42173: %% LTI REQ %% neuper@42122: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% neuper@42122: neuper@42122: \begin{frame}\frametitle{Convolution: Development effort} neuper@42122: {\small neuper@42122: \begin{center} neuper@42122: \begin{tabular}{l|l|r} neuper@42122: requirements & comments &effort\\ \hline\hline neuper@42122: simplify rationals & \sisac & 0\\ \hline neuper@42122: define $\sum\limits_{i=0}^{n}i$ & partly \sisac & 10\\ \hline neuper@42122: simplify sum & termorder & 10\\ neuper@42122: & simplify rules & 20\\ neuper@42122: & use simplify rationals& 0\\ \hline neuper@42122: index adjustments & with unit step & 10\\ \hline neuper@42122: example collection & with explanations & 20\\ \hline\hline neuper@42122: & & 70-90\\ neuper@42122: \end{tabular} neuper@42122: \end{center} neuper@42122: effort --- in 45min units\\ neuper@42122: } neuper@42122: \end{frame} jan@42173: jan@42173: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% jan@42173: %%--------------------LTI-------Conclusion-----------------------%% jan@42173: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% jan@42173: jan@42175: \begin{frame}{Convolution: Summary} jan@42173: \begin{itemize} jan@42173: jan@42175: \item Standard example jan@42183: \item Straight forward jan@42175: \item Challenge are sum limits jan@42173: jan@42173: \end{itemize} jan@42173: \end{frame} jan@42173: neuper@42122: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% neuper@42122: %-----------------------------------------------------------------% neuper@42122: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% neuper@42122: neuper@42122: \section[Z-transform]{Z-Transform} neuper@42122: \subsection[(Inverse) Z-Transform]{(Inverse) Z-Transform} neuper@42122: neuper@42122: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% neuper@42122: %% Z-Transform INTRO %% neuper@42122: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% neuper@42122: neuper@42122: \begin{frame}\frametitle{(Inverse) ${\cal Z}$-Transformation: Introduction} neuper@42122: \begin{itemize} neuper@42122: \item Pure Transformation is simple to realise with Z-Transform Properties (Table) neuper@42122: \item Partial Fraction are just math simplifications neuper@42122: \end{itemize} neuper@42122: \end{frame} neuper@42122: neuper@42122: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% neuper@42122: %% Z-Transform SPEC %% neuper@42122: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% neuper@42122: jan@42173: \begin{frame}\frametitle{(Inverse) Z-Transformation: Specification} jan@42175: {\footnotesize jrocnik@42159: jan@42175: Determine the inverse z transform of the following expression. Hint: applay the partial fraction expansion. jrocnik@42159: jrocnik@42159: \begin{center} jrocnik@42159: $X(z)=\frac{3}{z-\frac{1}{4}-\frac{1}{8}z^{-1}},\ \ x[n]$ is absolute summable jrocnik@42159: \end{center} jrocnik@42159: jan@42175: jan@42173: \hrulefill jan@42173: neuper@42122: \begin{tabbing} neuper@42122: 1\=postcond \=: \= \= $\;\;\;\;$\=\kill neuper@42122: \>given \>:\> Expression of z \\ jan@42207: \> \> \> \>(X (z::complex),3/(z-1/4-1/8\,z\textasciicircum{}(-1)))\\ neuper@42122: \>precond \>:\> TODO\\ neuper@42122: \>find \>:\> Expression of n\\ neuper@42122: \> \> \> \>$h[n]$\\ neuper@42122: \>postcond \>:\> TODO\\ neuper@42122: \end{tabbing} neuper@42122: neuper@42122: } neuper@42122: \end{frame} neuper@42122: neuper@42122: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% neuper@42122: %% Z expl REQ %% neuper@42122: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% neuper@42076: neuper@42122: jan@42173: \begin{frame}\frametitle{(Inverse) Z-Transformation: Development effort} neuper@42075: {\small neuper@42075: \begin{center} neuper@42075: \begin{tabular}{l|l|r} neuper@42075: requirements & comments &effort\\ \hline\hline neuper@42075: solve for part.fract. & \sisac: degree 2 & 0\\ neuper@42075: & complex nomminators & 30\\ neuper@42075: & degree > 2 & MT\\ \hline neuper@42075: simplify polynomial & \sisac & 0\\ neuper@42075: simplify rational & \sisac & 0\\ \hline neuper@42075: part.fract.decomposition& degree 2 & \\ neuper@42075: & specification, method& 30\\ \hline neuper@42075: ${\cal Z}^{-1}$ table & & 20\\ neuper@42075: & explanations, figures& 20\\ \hline neuper@42075: example collection & with explanations & 20\\ \hline\hline neuper@42075: & & 90-120\\ neuper@42075: % & & 1 MT neuper@42075: \end{tabular} neuper@42075: \end{center} neuper@42075: effort --- in 45min units\\ neuper@42075: MT --- thesis ``factorization'' (mathematics) neuper@42075: } neuper@42075: \end{frame} neuper@42075: jan@42173: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% jan@42173: %%--------------------Z-TRANS---Conclusion-----------------------%% jan@42173: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% jan@42173: jan@42175: \begin{frame}{(Inverse) Z-Transformation: Summary} jan@42173: \begin{itemize} jan@42173: jan@42175: \item No \emph{higher} math operations jan@42175: \item Different subproblems of math (equation systems, etc.) jan@42175: \item Both directions have the same effort jan@42173: jan@42173: \end{itemize} jan@42173: \end{frame} jan@42173: jan@42175: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% jan@42175: %-----------------------------------------------------------------% jan@42175: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% jan@42175: jan@42183: \section[Conclusions]{Conclusions} jan@42175: jan@42175: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% jan@42191: %--------------------------DEMONSTRATION--------------------------% jan@42191: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% jan@42191: jan@42191: \begin{frame}{Demonstration} jan@42191: jan@42191: \centering{Demonstration} jan@42191: jan@42191: \end{frame} jan@42191: jan@42191: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% jan@42175: %--------------------------CONCLUSION-----------------------------% jan@42175: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% jan@42175: jan@42175: \begin{frame}{Conclusions} jan@42175: jan@42175: Design Challanges: jan@42175: jan@42175: {\small jan@42175: \begin{itemize} jan@42175: jan@42175: \item Pre and Post conditions jan@42175: \item Exact mathematic behind functions jan@42207: \item Accurate mathematic notation jan@42175: jan@42175: \end{itemize} jan@42175: } jan@42175: jan@42175: Goals: jan@42175: {\small jan@42175: \begin{itemize} jan@42175: jan@42175: \item Spot the power of \sisac jan@42175: \item Implementation of generell but simple math problems jan@42175: \item Setting up a good first guideline (documentation) for furher problem implemenations jan@42175: jan@42175: \end{itemize} jan@42175: jan@42175: \centering{Efforts are only approximations, due we have no \emph{real} experience data!} jan@42175: } jan@42175: jan@42175: \end{frame} jan@42175: jan@42175: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% jan@42175: %--------------------------TIME LINE------------------------------% jan@42175: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% jan@42175: jan@42175: \begin{frame}{Comming up} jan@42175: jan@42175: {\small jan@42175: \begin{tabular}{l r} jan@42175: jan@42175: Juli 2011 & project startup\\ jan@42175: Juli 2011 & information collection, 1st presentation\\ jan@42175: August 2011 & extern traineeship\\ jan@42175: September 2011 & main work\\ jan@42175: after Oktober & finishing, documentation\\ jan@42175: jan@42175: \end{tabular} jan@42175: } jan@42175: jan@42175: \end{frame} jan@42175: jan@42175: neuper@42074: \end{document} neuper@42074: neuper@42074: