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}
157 1\=postcond \=: \= \= $\;\;\;\;$\=\kill
158 \>given \>:\> Time continiues, not periodic Signal \\
159 \> \> \> \>$(x (t::real), exp(-\,(\alpha::real\,+\,\alpha::imag)\,*\,t::real)*u(t::real))$\\
160 \>precond \>:\> TODO\\
161 \>find \>:\> $X(j\cdot\omega)$\\
162 \>postcond \>:\> TODO\\
168 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
169 %% Transform expl 1 REQ %%
170 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
172 \begin{frame}\frametitle{Fourier Transform 1: Development effort}
175 \begin{tabular}{l|l|r}
176 requirements & comments &effort\\ \hline\hline
177 solving Intrgrals & simple via propertie table & 20\\
178 & \emph{real} & MT\\ \hline
179 transformation table & simple transform & 20\\ \hline
180 example collection & with explanations & 20\\ \hline\hline
184 effort --- in 45min units\\
185 MT --- thesis ``Integrals'' (mathematics)
189 \subsection[difficult]{Fourier transform Example 2}
191 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
192 %% Transform expl 2 SPEC %%
193 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
195 \begin{frame}\frametitle{Fourier Transform 2: Specification}
198 \textbf{(a)} Determine the fourier transform for the given rectangular impulse:
210 1\=postcond \=: \= \= $\;\;\;\;$\=\kill
211 \>given \>:\> piecewise\_function \\
212 \> \> \> \>$(x (t::real), [(0,-\infty<t<1), (1,1\leq t\leq 3), (0, 3<t<\infty)])$\\
213 %?(iterativer) datentyp in Isabelle/HOL
214 \> \> \> translation $T=2$\\
215 \>precond \>:\> TODO\\
216 \>find \>:\> $X(j\cdot\omega)$\\
217 \>postcond \>:\> TODO\\
223 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
224 %% Transform expl 2 REQ %%
225 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
227 \begin{frame}\frametitle{Fourier Transform 2: Development effort}
230 \begin{tabular}{l|l|r}
231 requirements & comments &effort\\ \hline\hline
232 solving Intrgrals & simple via propertie table & 20\\
233 & \emph{real} & MT\\ \hline
234 transformation table & simple transform & 20\\ \hline
235 visualisation & backend & 10\\ \hline
236 example collection & with explanations & 20\\ \hline\hline
240 effort --- in 45min units\\
241 MT --- thesis ``Integrals'' (mathematics)
245 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
246 %%--------------------FOURIER---Conclusion-----------------------%%
247 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
249 \begin{frame}{Summary}
259 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
260 %-----------------------------------------------------------------%
261 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
263 \section[Discrete time]{Discrete-time systems}
264 \subsection[Convolution]{Convolution}
266 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
268 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
270 \begin{frame}\frametitle{Convolution: Introduction}
272 \item Calculation\ldots
273 \item Visualisation\ldots
276 \ldots of parallel filter structures
280 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
282 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
284 \begin{frame}\frametitle{Convolution: Specification}
287 Consider the two discrete-time, linear and time-invariant (LTI) systems with the following impulse response:
290 $h_1[n]=\left(\frac{3}{5}\right)^n\cdot u[n]$\\
291 $h_1[n]=\left(-\frac{2}{3}\right)^n\cdot u[n]$
294 The two systems are cascaded seriell. Derive the impulse respinse of the overall system $h_c[n]$.
299 1\=postcond \=: \= \= $\;\;\;\;$\=\kill
300 \>given \>:\> Signals h1[n], h2[n] \\
301 \> \> \> \>((h1 (n::real),(3/5)\textasciicircum{}n\,u(n::real)),\,(h2 (n::real),(-2/3)\textasciicircum{}n\,u(n::real)))\\
302 %?(iterativer) datentyp in Isabelle/HOL
303 \>precond \>:\> TODO\\
304 \>find \>:\> $h1[n]\,*\,h2[n]$\\
305 \>postcond \>:\> TODO\\
311 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
313 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
315 \begin{frame}\frametitle{Convolution: Development effort}
318 \begin{tabular}{l|l|r}
319 requirements & comments &effort\\ \hline\hline
320 simplify rationals & \sisac & 0\\ \hline
321 define $\sum\limits_{i=0}^{n}i$ & partly \sisac & 10\\ \hline
322 simplify sum & termorder & 10\\
323 & simplify rules & 20\\
324 & use simplify rationals& 0\\ \hline
325 index adjustments & with unit step & 10\\ \hline
326 example collection & with explanations & 20\\ \hline\hline
330 effort --- in 45min units\\
334 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
335 %%--------------------LTI-------Conclusion-----------------------%%
336 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
338 \begin{frame}{Summary}
348 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
349 %-----------------------------------------------------------------%
350 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
352 \section[Z-transform]{Z-Transform}
353 \subsection[(Inverse) Z-Transform]{(Inverse) Z-Transform}
355 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
356 %% Z-Transform INTRO %%
357 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
359 \begin{frame}\frametitle{(Inverse) ${\cal Z}$-Transformation: Introduction}
361 \item Pure Transformation is simple to realise with Z-Transform Properties (Table)
362 \item Partial Fraction are just math simplifications
366 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
367 %% Z-Transform SPEC %%
368 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
370 \begin{frame}\frametitle{(Inverse) Z-Transformation: Specification}
373 Determine the inverse $\cal{z}$ transform of the following expression. Hint: applay the partial fraction expansion.
376 $X(z)=\frac{3}{z-\frac{1}{4}-\frac{1}{8}z^{-1}},\ \ x[n]$ is absolute summable
382 1\=postcond \=: \= \= $\;\;\;\;$\=\kill
383 \>given \>:\> Expression of z \\
384 \> \> \> \>(X (z::real\,+z::imag),3/(z-1/4-1/8\,z\textasciicircum{}(-1)))\\
385 \>precond \>:\> TODO\\
386 \>find \>:\> Expression of n\\
388 \>postcond \>:\> TODO\\
394 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
396 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
399 \begin{frame}\frametitle{(Inverse) Z-Transformation: Development effort}
402 \begin{tabular}{l|l|r}
403 requirements & comments &effort\\ \hline\hline
404 solve for part.fract. & \sisac: degree 2 & 0\\
405 & complex nomminators & 30\\
406 & degree > 2 & MT\\ \hline
407 simplify polynomial & \sisac & 0\\
408 simplify rational & \sisac & 0\\ \hline
409 part.fract.decomposition& degree 2 & \\
410 & specification, method& 30\\ \hline
411 ${\cal Z}^{-1}$ table & & 20\\
412 & explanations, figures& 20\\ \hline
413 example collection & with explanations & 20\\ \hline\hline
418 effort --- in 45min units\\
419 MT --- thesis ``factorization'' (mathematics)
423 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
424 %%--------------------Z-TRANS---Conclusion-----------------------%%
425 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
427 \begin{frame}{Summary}