8 \setbeamercovered{transparent}
11 %\usepackage{setspace} %for "\begin{onehalfspace}"
12 \usepackage[english]{babel}
15 \usepackage[utf8]{inputenc}
19 \usepackage[T1]{fontenc}
20 % Or whatever. Note that the encoding and the font should match. If T1
21 % does not look nice, try deleting the line with the fontenc.
23 \def\isac{${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$}
24 \def\sisac{{\footnotesize${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$}}
26 \title[SPSC in \isac] % (optional, use only with long paper titles)
27 {Interactive Course Material\\ for Signal Processing\\ based on Isabelle/\isac}
29 \subtitle{Baccalaureate Thesis}
31 \author[Rocnik] % (optional, use only with lots of authors)
33 % - Give the names in the same order as the appear in the paper.
34 % - Use the \inst{?} command only if the authors have different
37 \institute % (optional, but mostly needed)
39 Technische Universit\"at Graz\\
42 % - Use the \inst command only if there are several affiliations.
43 % - Keep it simple, no one is interested in your street address.
45 % \date[CFP 2003] % (optional, should be abbreviation of conference name)
46 % {Conference on Fabulous Presentations, 2003}
47 % - Either use conference name or its abbreviation.
48 % - Not really informative to the audience, more for people (including
49 % yourself) who are reading the slides online
51 % \subject{Theoretical Computer Science}
52 % This is only inserted into the PDF information catalog. Can be left
57 % If you have a file called "university-logo-filename.xxx", where xxx
58 % is a graphic format that can be processed by latex or pdflatex,
59 % resp., then you can add a logo as follows:
61 % \pgfdeclareimage[height=0.5cm]{university-logo}{university-logo-filename}
62 % \logo{\pgfuseimage{university-logo}}
66 % Delete this, if you do not want the table of contents to pop up at
67 % the beginning of each subsection:
70 \begin{frame}<beamer>{Outline}
71 \tableofcontents[currentsection,currentsubsection]
76 % If you wish to uncover everything in a step-wise fashion, uncomment
77 % the following command:
79 %\beamerdefaultoverlayspecification{<+->}
84 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
86 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
92 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
93 %% Table of Contents %%
94 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
96 \begin{frame}{Outline}
98 % You might wish to add the option [pausesections]
101 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
102 %%---------------------------------------------------------------%%
103 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
105 \section[Intro]{Introduction}
107 \begin{frame}{Introduction}
108 Issues to be accomplished in this thesis:
112 \item What knowledge is already mechanised in \emph{isabelle}?
113 \item How can missing theorems and definitions be mechanised?
114 \item What is the effort for such mechanisation?
115 \item How do calculations look like, if using mechanised knowledge?
116 \item What are the problems and subproblems to be solved?
117 \item Which problems are already implemented in \sisac?
118 \item How are the new Problems specified rigorously (\sisac)?
119 \item Which variantes of programms in \sisac{} solving the problems?
120 \item What is the contents of the interactiv course material (Figures, etc.)?
125 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
126 %%---------------------------------------------------------------%%
127 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
129 \section[Fourier]{Fourier transform}
131 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
133 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
135 \begin{frame}\frametitle{Fourier Transformation: Introduction}
137 \item Transform operation by using property-tables $\rightarrow$ \emph{easy}
138 \item Transform operation by using integral $\rightarrow$ \emph{difficult}
139 \item No math \emph{tricks}
140 \item Important: Visualisation?!
144 \subsection[simple]{Fourier transform Example 1}
146 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
147 %% Transform expl 1 SPEC %%
148 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
150 \begin{frame}\frametitle{Fourier Transform 1: Specification}
155 1\=postcond \=: \= \= $\;\;\;\;$\=\kill
156 \>given \>:\> Time continiues, not periodic Signal \\
157 \> \> \> \>$(x (t::real), exp(-\,(\alpha::real\,+\,\alpha::imag)\,*\,t::real)*u(t::real))$\\
158 \>precond \>:\> TODO\\
159 \>find \>:\> $X(j\cdot\omega)$\\
160 \>postcond \>:\> TODO\\
165 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
166 %% Transform expl 1 CALC %%
167 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
169 \begin{frame}\frametitle{Fourier Transformation 1: Calculation}
170 TODO: Bernhard fragen ob Tabelle oder Rechnung
173 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
174 %% Transform expl 1 REQ %%
175 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
177 \begin{frame}\frametitle{Fourier Transform 1: Development effort}
180 \begin{tabular}{l|l|r}
181 requirements & comments &effort\\ \hline\hline
182 solving Intrgrals & simple via propertie table & 20\\
183 & \emph{real} & MT\\ \hline
184 transformation table & simple transform & 20\\ \hline
185 example collection & with explanations & 20\\ \hline\hline
189 effort --- in 45min units\\
190 MT --- thesis ``Integrals'' (mathematics)
194 \subsection[difficult]{Fourier transform Example 2}
196 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
197 %% Transform expl 2 SPEC %%
198 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
200 \begin{frame}\frametitle{Fourier Transform 2: Specification}
203 \textbf{(a)} Determine the fourier transform for the given rectangular impulse:
215 1\=postcond \=: \= \= $\;\;\;\;$\=\kill
216 \>given \>:\> piecewise\_function \\
217 \> \> \> \>$(x (t::real), [(0,-\infty<t<1), (1,1\leq t\leq 3), (0, 3<t<\infty)])$\\
218 %?(iterativer) datentyp in Isabelle/HOL
219 \> \> \> translation $T=2$\\
220 \>precond \>:\> TODO\\
221 \>find \>:\> $X(j\cdot\omega)$\\
222 \>postcond \>:\> TODO\\
228 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
229 %% Transform expl 2 CALC %%
230 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
232 %\begin{frame}\frametitle{Fourier Transform 2: Calculation}
236 %01 \> ${\cal F}\;(x(t-2)) =$\\
237 % \`${\cal F}\;(x(t-T)) = e^{-j\cdot\omega\cdot T}\cdot X\;j\cdot\omega$\\
238 %02 \> $e^{-j\cdot\omega\cdot 2}\cdot X\;(j\cdot\omega)$\\
239 % \`definition $X\;(j\cdot\omega)$\\
240 %03 \> $e^{-j\cdot\omega\cdot 2}\cdot \int_{-\infty}^\infty x\;t\;\cdot e^{-j\cdot\omega\cdot t} d t$\\
241 % \` $x\;t = 1\;{\it for}\;\{x.\;-1\leq t\;\land\;t\leq 1\}\;{\it and}\;x\;t=0\;{\it otherwise}$\\
242 %04 \> $e^{-j\cdot\omega\cdot 2}\cdot \int_{-1}^1 1\cdot e^{-j\cdot\omega\cdot t} d t$\\
243 % \` $\int_a^b f\;t\;dt = \int f\;t\;dt\;|_a^b$\\
244 %05 \> $e^{-j\cdot\omega\cdot 2}\cdot \int 1\cdot e^{-j\cdot\omega\cdot t} d t\;|_{-1}^1$\\
245 % %\` $\int e^{a\cdot t} = \frac{1}{a}\cdot e^{a\cdot t}$\\
246 % \` pbl: integration in $\cal C$\\
247 %06 \> $e^{-j\cdot\omega\cdot 2}\cdot (\frac{1}{-j\cdot\omega}\cdot e^{-j\cdot\omega\cdot t} \;|_{-1}^1)$\\
248 % \` $f\;t\;|_a^b = f\;b-f\;a$\\
249 %07 \> $e^{-j\cdot\omega\cdot 2}\cdot (\frac{1}{-j\cdot\omega}\cdot e^{-j\cdot\omega\cdot 1} - \frac{1}{-j\cdot\omega}\cdot e^{-j\cdot\omega\cdot -1})$\\
250 %\vdots\` pbl: simplification+factorization in $\cal C$\\
251 %08 \> $e^{-j\cdot\omega\cdot 2}\cdot \frac{1}{-j\cdot\omega}\cdot(e^{j\cdot\omega} - e^{-j\cdot\omega})$\\
253 %09 \> $e^{-j\cdot\omega\cdot 2}\cdot \frac{1}{\omega}\cdot(\frac{-e^{j\cdot\omega} + e^{-j\cdot\omega}}{j})$\\
255 %10 \> $e^{-j\cdot\omega\cdot 2}\cdot 2\cdot\frac{\sin\;\omega}{\omega}$
260 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
261 %% Transform expl 2 REQ %%
262 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
264 \begin{frame}\frametitle{Fourier Transform 2: Development effort}
267 \begin{tabular}{l|l|r}
268 requirements & comments &effort\\ \hline\hline
269 solving Intrgrals & simple via propertie table & 20\\
270 & \emph{real} & MT\\ \hline
271 transformation table & simple transform & 20\\ \hline
272 visualisation & backend & 10\\ \hline
273 example collection & with explanations & 20\\ \hline\hline
277 effort --- in 45min units\\
278 MT --- thesis ``Integrals'' (mathematics)
282 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
283 %%--------------------FOURIER---Conclusion-----------------------%%
284 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
286 %\subsection[Summary]{Summary}
288 \begin{frame}{Summary}
298 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
299 %-----------------------------------------------------------------%
300 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
302 \section[Discrete time]{Discrete-time systems}
303 \subsection[Convolution]{Convolution}
305 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
307 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
309 \begin{frame}\frametitle{Convolution: Introduction}
311 \item Calculation\ldots
312 \item Visualisation\ldots
315 \ldots of parallel filter structures
319 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
321 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
323 \begin{frame}\frametitle{Convolution: Specification}
326 Consider the two discrete-time, linear and time-invariant (LTI) systems with the following impulse response:
329 $h_1[n]=\left(\frac{3}{5}\right)^n\cdot u[n]$\\
330 $h_1[n]=\left(-\frac{2}{3}\right)^n\cdot u[n]$
333 The two systems are cascaded seriell. Derive the impulse respinse of the overall system $h_c[n]$.
336 1\=postcond \=: \= \= $\;\;\;\;$\=\kill
337 \>given \>:\> Signals h1[n], h2[n] \\
338 \> \> \> \>((h1 (n::real),(3/5)\textasciicircum{}n\,u(n::real)),\,(h2 (n::real),(-2/3)\textasciicircum{}n\,u(n::real)))\\
339 %?(iterativer) datentyp in Isabelle/HOL
340 \>precond \>:\> TODO\\
341 \>find \>:\> $h1[n]\,*\,h2[n]$\\
342 \>postcond \>:\> TODO\\
348 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
350 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
352 %\begin{frame}\frametitle{Convolution: Calculation}
356 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
358 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
360 \begin{frame}\frametitle{Convolution: Development effort}
363 \begin{tabular}{l|l|r}
364 requirements & comments &effort\\ \hline\hline
365 simplify rationals & \sisac & 0\\ \hline
366 define $\sum\limits_{i=0}^{n}i$ & partly \sisac & 10\\ \hline
367 simplify sum & termorder & 10\\
368 & simplify rules & 20\\
369 & use simplify rationals& 0\\ \hline
370 index adjustments & with unit step & 10\\ \hline
371 example collection & with explanations & 20\\ \hline\hline
375 effort --- in 45min units\\
378 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
379 %-----------------------------------------------------------------%
380 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
382 \section[Z-transform]{Z-Transform}
383 \subsection[(Inverse) Z-Transform]{(Inverse) Z-Transform}
385 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
386 %% Z-Transform INTRO %%
387 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
389 \begin{frame}\frametitle{(Inverse) ${\cal Z}$-Transformation: Introduction}
391 \item Pure Transformation is simple to realise with Z-Transform Properties (Table)
392 \item Partial Fraction are just math simplifications
397 %\subsection[]{Indextranformation}
398 %\begin{frame}\frametitle{TODO}
402 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
403 %% Z-Transform SPEC %%
404 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
406 \begin{frame}\frametitle{(Inverse) ${\cal Z}$-Transformation: Specification}
409 Determine the inverse $\cal{z}$ transform of the following expression. Hint: applay the partial fraction expansion.
412 $X(z)=\frac{3}{z-\frac{1}{4}-\frac{1}{8}z^{-1}},\ \ x[n]$ is absolute summable
416 1\=postcond \=: \= \= $\;\;\;\;$\=\kill
417 \>given \>:\> Expression of z \\
418 \> \> \> \>(X (z::real\,+z::imag),3/(z-1/4-1/8\,z\textasciicircum{}(-1)))\\
419 \>precond \>:\> TODO\\
420 \>find \>:\> Expression of n\\
422 \>postcond \>:\> TODO\\
428 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
430 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
432 %\begin{frame}\frametitle{(Inverse) ${\cal Z}$-Transformation: Calculation}
436 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
438 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
441 \begin{frame}\frametitle{(Inverse) ${\cal Z}$-Transformation: Development effort}
444 \begin{tabular}{l|l|r}
445 requirements & comments &effort\\ \hline\hline
446 solve for part.fract. & \sisac: degree 2 & 0\\
447 & complex nomminators & 30\\
448 & degree > 2 & MT\\ \hline
449 simplify polynomial & \sisac & 0\\
450 simplify rational & \sisac & 0\\ \hline
451 part.fract.decomposition& degree 2 & \\
452 & specification, method& 30\\ \hline
453 ${\cal Z}^{-1}$ table & & 20\\
454 & explanations, figures& 20\\ \hline
455 example collection & with explanations & 20\\ \hline\hline
460 effort --- in 45min units\\
461 MT --- thesis ``factorization'' (mathematics)