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{setspace} %for "\begin{onehalfspace}" neuper@42074: \usepackage[english]{babel} neuper@42074: % or whatever neuper@42074: neuper@42074: \usepackage[utf8]{inputenc} neuper@42074: % or whatever neuper@42074: neuper@42074: \usepackage{times} neuper@42074: \usepackage[T1]{fontenc} neuper@42074: % Or whatever. Note that the encoding and the font should match. If T1 neuper@42074: % does not look nice, try deleting the line with the 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: neuper@42074: \author[Rocnik] % (optional, use only with lots of authors) neuper@42074: {Jan~Rocnik} neuper@42074: % - Give the names in the same order as the appear in the paper. neuper@42074: % - Use the \inst{?} command only if the authors have different neuper@42074: % affiliation. 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: % - Use the \inst command only if there are several affiliations. neuper@42074: % - Keep it simple, no one is interested in your street address. neuper@42074: neuper@42074: % \date[CFP 2003] % (optional, should be abbreviation of conference name) neuper@42074: % {Conference on Fabulous Presentations, 2003} neuper@42074: % - Either use conference name or its abbreviation. neuper@42074: % - Not really informative to the audience, more for people (including neuper@42074: % yourself) who are reading the slides online neuper@42074: neuper@42074: % \subject{Theoretical Computer Science} neuper@42074: % This is only inserted into the PDF information catalog. Can be left neuper@42074: % out. neuper@42074: 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: neuper@42074: % If you wish to uncover everything in a step-wise fashion, uncomment neuper@42074: % the following command: neuper@42074: neuper@42074: %\beamerdefaultoverlayspecification{<+->} 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@42163: \begin{frame}{Introduction} jan@42163: Issues to be accomplished in this thesis: jan@42163: jan@42163: \begin{itemize} jan@42163: jan@42163: \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@42163: \item How do calculations look like, if using mechanised knowledge? jan@42163: \item What are the problems and subproblems to be solved? jan@42163: \item Which problems are already implemented in \sisac? jan@42163: \item How are the new Problems specified rigorously (\sisac)? jan@42163: \item Which variantes of programms in \sisac{} solving 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: neuper@42075: \section[Fourier]{Fourier transform} neuper@42122: neuper@42122: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% neuper@42122: %% Fourier INTRO %% neuper@42122: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% neuper@42122: neuper@42122: \begin{frame}\frametitle{Fourier Transformation: Introduction} neuper@42122: \begin{itemize} neuper@42122: \item Transform operation by using property-tables $\rightarrow$ \emph{easy} neuper@42122: \item Transform operation by using integral $\rightarrow$ \emph{difficult} neuper@42122: \item No math \emph{tricks} neuper@42122: \item Important: Visualisation?! neuper@42122: \end{itemize} neuper@42074: \end{frame} neuper@42074: neuper@42122: \subsection[simple]{Fourier transform Example 1} neuper@42122: neuper@42122: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% neuper@42122: %% Transform expl 1 SPEC %% neuper@42122: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% neuper@42122: neuper@42122: \begin{frame}\frametitle{Fourier Transform 1: Specification} neuper@42122: {\footnotesize\it neuper@42122: Fourier Transform jrocnik@42159: jan@42173: \hrulefill jan@42173: neuper@42122: \begin{tabbing} neuper@42122: 1\=postcond \=: \= \= $\;\;\;\;$\=\kill neuper@42122: \>given \>:\> Time continiues, not periodic Signal \\ neuper@42122: \> \> \> \>$(x (t::real), exp(-\,(\alpha::real\,+\,\alpha::imag)\,*\,t::real)*u(t::real))$\\ neuper@42122: \>precond \>:\> TODO\\ neuper@42122: \>find \>:\> $X(j\cdot\omega)$\\ neuper@42122: \>postcond \>:\> TODO\\ neuper@42122: \end{tabbing} neuper@42122: neuper@42122: } neuper@42122: \end{frame} neuper@42074: neuper@42122: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% neuper@42122: %% Transform expl 1 REQ %% neuper@42122: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% neuper@42122: neuper@42122: \begin{frame}\frametitle{Fourier Transform 1: 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: example collection & with explanations & 20\\ \hline\hline neuper@42122: & & 60-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} neuper@42074: neuper@42122: \subsection[difficult]{Fourier transform Example 2} neuper@42074: neuper@42122: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% neuper@42122: %% Transform expl 2 SPEC %% neuper@42122: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% neuper@42122: neuper@42122: \begin{frame}\frametitle{Fourier Transform 2: Specification} neuper@42076: {\footnotesize\it jrocnik@42159: jrocnik@42159: \textbf{(a)} 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: neuper@42076: \begin{tabbing} neuper@42076: 1\=postcond \=: \= \= $\;\;\;\;$\=\kill neuper@42076: \>given \>:\> piecewise\_function \\ neuper@42076: \> \> \> \>$(x (t::real), [(0,-\infty \> \> translation $T=2$\\ 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: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% neuper@42122: %% Transform expl 2 REQ %% neuper@42122: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% neuper@42122: neuper@42122: \begin{frame}\frametitle{Fourier Transform 2: 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@42163: \begin{frame}{Summary} jan@42163: todo jan@42163: jan@42163: \begin{itemize} jan@42163: jan@42163: \item todo jan@42163: jan@42163: \end{itemize} jan@42163: \end{frame} jan@42163: neuper@42122: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% neuper@42122: %-----------------------------------------------------------------% neuper@42122: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% neuper@42074: neuper@42076: \section[Discrete time]{Discrete-time systems} neuper@42076: \subsection[Convolution]{Convolution} neuper@42122: neuper@42122: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% jan@42173: %% LTI INTRO %% neuper@42122: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% neuper@42122: neuper@42122: \begin{frame}\frametitle{Convolution: Introduction} neuper@42122: \begin{itemize} neuper@42122: \item Calculation\ldots neuper@42122: \item Visualisation\ldots neuper@42122: \end{itemize} neuper@42122: \begin{center} neuper@42122: \ldots of parallel filter structures neuper@42122: \end{center} neuper@42122: \end{frame} neuper@42122: neuper@42122: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% jan@42173: %% LTI SPEC %% neuper@42122: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% neuper@42122: neuper@42122: \begin{frame}\frametitle{Convolution: Specification} neuper@42122: {\footnotesize\it 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@42173: neuper@42122: \begin{tabbing} neuper@42122: 1\=postcond \=: \= \= $\;\;\;\;$\=\kill neuper@42122: \>given \>:\> Signals h1[n], h2[n] \\ neuper@42122: \> \> \> \>((h1 (n::real),(3/5)\textasciicircum{}n\,u(n::real)),\,(h2 (n::real),(-2/3)\textasciicircum{}n\,u(n::real)))\\ neuper@42122: %?(iterativer) datentyp in Isabelle/HOL 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@42173: \begin{frame}{Summary} jan@42173: todo jan@42173: jan@42173: \begin{itemize} jan@42173: jan@42173: \item todo 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} neuper@42122: {\footnotesize\it jrocnik@42159: jrocnik@42159: Determine the inverse $\cal{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@42173: \hrulefill jan@42173: neuper@42122: \begin{tabbing} neuper@42122: 1\=postcond \=: \= \= $\;\;\;\;$\=\kill neuper@42122: \>given \>:\> Expression of z \\ neuper@42122: \> \> \> \>(X (z::real\,+z::imag),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@42173: \begin{frame}{Summary} jan@42173: todo jan@42173: jan@42173: \begin{itemize} jan@42173: jan@42173: \item todo jan@42173: jan@42173: \end{itemize} jan@42173: \end{frame} jan@42173: neuper@42074: \end{document} neuper@42074: neuper@42074: