\documentclass{beamer}

\mode<presentation>

{

  \usetheme{Hannover}

  \setbeamercovered{transparent}

}

%\usepackage{setspace} %for "\begin{onehalfspace}"

\usepackage[english]{babel}

% or whatever

\usepackage[utf8]{inputenc}

% or whatever

\usepackage{times}

\usepackage[T1]{fontenc}

% Or whatever. Note that the encoding and the font should match. If T1

% does not look nice, try deleting the line with the fontenc.

\def\isac{${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$}

\def\sisac{{\footnotesize${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$}}

\title[SPSC in \isac] % (optional, use only with long paper titles)

{Interactive Course Material\\ for Signal Processing\\ based on Isabelle/\isac}

\subtitle{Baccalaureate Thesis}

\author[Rocnik] % (optional, use only with lots of authors)

{Jan~Rocnik}

% - Give the names in the same order as the appear in the paper.

% - Use the \inst{?} command only if the authors have different

%   affiliation.

\institute % (optional, but mostly needed)

{

  Technische Universit\"at Graz\\

  Institut f\"ur TODO

}

% - Use the \inst command only if there are several affiliations.

% - Keep it simple, no one is interested in your street address.

% \date[CFP 2003] % (optional, should be abbreviation of conference name)

% {Conference on Fabulous Presentations, 2003}

% - Either use conference name or its abbreviation.

% - Not really informative to the audience, more for people (including

%   yourself) who are reading the slides online

% \subject{Theoretical Computer Science}

% This is only inserted into the PDF information catalog. Can be left

% out.

% If you have a file called "university-logo-filename.xxx", where xxx

% is a graphic format that can be processed by latex or pdflatex,

% resp., then you can add a logo as follows:

% \pgfdeclareimage[height=0.5cm]{university-logo}{university-logo-filename}

% \logo{\pgfuseimage{university-logo}}

% Delete this, if you do not want the table of contents to pop up at

% the beginning of each subsection:

\AtBeginSubsection[]

{

  \begin{frame}<beamer>{Outline}

    \tableofcontents[currentsection,currentsubsection]

  \end{frame}

}

% If you wish to uncover everything in a step-wise fashion, uncomment

% the following command:

%\beamerdefaultoverlayspecification{<+->}

\begin{document}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%												Title Page                             %%

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\begin{frame}

  \titlepage

\end{frame}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%												Table of Contents                      %%

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\begin{frame}{Outline}

  \tableofcontents

  % You might wish to add the option [pausesections]

\end{frame}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%---------------------------------------------------------------%%

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\section[Intro]{Introduction}

\begin{frame}{Introduction}

Issues to be accomplished in this thesis:

\begin{itemize}

\item What knowledge is already mechanised in \emph{isabelle}?

\item How can missing theorems and definitions be mechanised?

\item What is the effort for such mechanisation?

\item How do calculations look like, if using mechanised knowledge?

\item What are the problems and subproblems to be solved?

\item Which problems are already implemented in \sisac?

\item How are the new Problems specified rigorously (\sisac)?

\item Which variantes of programms in \sisac{} solving the problems?

\item What is the contents of the interactiv course material (Figures, etc.)?

\end{itemize}

\end{frame}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%---------------------------------------------------------------%%

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\section[Fourier]{Fourier transform}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%												Fourier INTRO                          %%

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\begin{frame}\frametitle{Fourier Transformation: Introduction}

\begin{itemize}

\item Transform operation by using property-tables $\rightarrow$ \emph{easy}

\item Transform operation by using integral $\rightarrow$ \emph{difficult}

\item No math \emph{tricks}

\item Important: Visualisation?!

\end{itemize}

\end{frame}

\subsection[simple]{Fourier transform Example 1}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%												Transform expl 1 SPEC                  %%

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\begin{frame}\frametitle{Fourier Transform 1: Specification}

{\footnotesize\it

Fourier Transform

\begin{tabbing}

1\=postcond \=: \= \= $\;\;\;\;$\=\kill

\>given    \>:\>  Time continiues, not periodic Signal \\

\>         \> \>  \>$(x (t::real), exp(-\,(\alpha::real\,+\,\alpha::imag)\,*\,t::real)*u(t::real))$\\

\>precond  \>:\>  TODO\\

\>find     \>:\>  $X(j\cdot\omega)$\\

\>postcond \>:\>  TODO\\

\end{tabbing}

}

\end{frame}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%												Transform expl 1 CALC                  %%

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\begin{frame}\frametitle{Fourier Transformation 1: Calculation}

TODO: Bernhard fragen ob Tabelle oder Rechnung

\end{frame}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%												Transform expl 1 REQ                  %%

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\begin{frame}\frametitle{Fourier Transform 1: Development effort}

{\small

\begin{center}

\begin{tabular}{l|l|r}

requirements            & comments             &effort\\ \hline\hline

solving Intrgrals		    & simple via propertie table     &     20\\

                        & \emph{real}          &    MT\\ \hline

transformation table    & simple transform     &    20\\ \hline

example collection      & with explanations    &    20\\ \hline\hline

                        &                      & 60-80\\

\end{tabular}

\end{center}

effort --- in 45min units\\

MT --- thesis ``Integrals'' (mathematics)

}

\end{frame}

\subsection[difficult]{Fourier transform Example 2}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%										Transform expl 2 SPEC                      %%

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\begin{frame}\frametitle{Fourier Transform 2: Specification}

{\footnotesize\it

\textbf{(a)} Determine the fourier transform for the given rectangular impulse:

\begin{center}

$x(t)= \left\{

     \begin{array}{lr}

       1 & -1\leq t\leq1\\

       0 & else

     \end{array}

   \right.$

\end{center}

\begin{tabbing}

1\=postcond \=: \= \= $\;\;\;\;$\=\kill

\>given    \>:\>  piecewise\_function \\

\>         \> \>  \>$(x (t::real), [(0,-\infty<t<1), (1,1\leq t\leq 3), (0, 3<t<\infty)])$\\

                        %?(iterativer) datentyp in Isabelle/HOL

\>         \> \>  translation $T=2$\\

\>precond  \>:\>  TODO\\

\>find     \>:\>  $X(j\cdot\omega)$\\

\>postcond \>:\>  TODO\\

\end{tabbing}

}

\end{frame}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%												Transform expl  2 CALC                 %%

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%\begin{frame}\frametitle{Fourier Transform 2: Calculation}

%\footnotesize{

%\begin{tabbing}

%000\=\kill

%01 \> ${\cal F}\;(x(t-2)) =$\\

%      \`${\cal F}\;(x(t-T)) = e^{-j\cdot\omega\cdot T}\cdot X\;j\cdot\omega$\\

%02 \> $e^{-j\cdot\omega\cdot 2}\cdot X\;(j\cdot\omega)$\\

%      \`definition $X\;(j\cdot\omega)$\\

%03 \> $e^{-j\cdot\omega\cdot 2}\cdot \int_{-\infty}^\infty x\;t\;\cdot e^{-j\cdot\omega\cdot t} d t$\\

%      \` $x\;t = 1\;{\it for}\;\{x.\;-1\leq t\;\land\;t\leq 1\}\;{\it and}\;x\;t=0\;{\it otherwise}$\\

%04 \> $e^{-j\cdot\omega\cdot 2}\cdot \int_{-1}^1 1\cdot e^{-j\cdot\omega\cdot t} d t$\\

%      \` $\int_a^b f\;t\;dt = \int f\;t\;dt\;|_a^b$\\

%05 \> $e^{-j\cdot\omega\cdot 2}\cdot \int 1\cdot e^{-j\cdot\omega\cdot t} d t\;|_{-1}^1$\\

%      %\` $\int e^{a\cdot t} = \frac{1}{a}\cdot e^{a\cdot t}$\\

%       \` pbl: integration in $\cal C$\\

%06 \> $e^{-j\cdot\omega\cdot 2}\cdot (\frac{1}{-j\cdot\omega}\cdot e^{-j\cdot\omega\cdot t} \;|_{-1}^1)$\\

%      \` $f\;t\;|_a^b = f\;b-f\;a$\\

%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})$\\

%\vdots\` pbl: simplification+factorization in $\cal C$\\

%08 \> $e^{-j\cdot\omega\cdot 2}\cdot \frac{1}{-j\cdot\omega}\cdot(e^{j\cdot\omega} - e^{-j\cdot\omega})$\\

%      \` trick~!\\

%09 \> $e^{-j\cdot\omega\cdot 2}\cdot \frac{1}{\omega}\cdot(\frac{-e^{j\cdot\omega} + e^{-j\cdot\omega}}{j})$\\

%      \` table\\

%10 \> $e^{-j\cdot\omega\cdot 2}\cdot 2\cdot\frac{\sin\;\omega}{\omega}$

%\end{tabbing}

%}

%\end{frame}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%												Transform expl 2 REQ                   %%

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\begin{frame}\frametitle{Fourier Transform 2: Development effort}

{\small

\begin{center}

\begin{tabular}{l|l|r}

requirements            & comments             &effort\\ \hline\hline

solving Intrgrals		    & simple via propertie table     &     20\\

                        & \emph{real}          &    MT\\ \hline

transformation table    & simple transform     &    20\\ \hline

visualisation						& backend							 &    10\\ \hline

example collection      & with explanations    &    20\\ \hline\hline

                        &                      & 70-80\\

\end{tabular}

\end{center}

effort --- in 45min units\\

MT --- thesis ``Integrals'' (mathematics)

}

\end{frame}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%--------------------FOURIER---Conclusion-----------------------%%

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%\subsection[Summary]{Summary}

\begin{frame}{Summary}

todo

\begin{itemize}

\item todo

\end{itemize}

\end{frame}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%-----------------------------------------------------------------%

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\section[Discrete time]{Discrete-time systems}

\subsection[Convolution]{Convolution}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%												DTS INTRO				                       %%

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\begin{frame}\frametitle{Convolution: Introduction}

\begin{itemize}

\item Calculation\ldots

\item Visualisation\ldots

\end{itemize}

\begin{center}

\ldots of parallel filter structures

\end{center}

\end{frame}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%												DTS SPEC				                       %%

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\begin{frame}\frametitle{Convolution: Specification}

{\footnotesize\it

Consider the two discrete-time, linear and time-invariant (LTI) systems with the following impulse response:

\begin{center}

$h_1[n]=\left(\frac{3}{5}\right)^n\cdot u[n]$\\

$h_1[n]=\left(-\frac{2}{3}\right)^n\cdot u[n]$

\end{center}

The two systems are cascaded seriell. Derive the impulse respinse of the overall system $h_c[n]$.

\begin{tabbing}

1\=postcond \=: \= \= $\;\;\;\;$\=\kill

\>given    \>:\>  Signals h1[n], h2[n] \\

\>         \> \>  \>((h1 (n::real),(3/5)\textasciicircum{}n\,u(n::real)),\,(h2 (n::real),(-2/3)\textasciicircum{}n\,u(n::real)))\\

                        %?(iterativer) datentyp in Isabelle/HOL

\>precond  \>:\>  TODO\\

\>find     \>:\>  $h1[n]\,*\,h2[n]$\\

\>postcond \>:\>  TODO\\

\end{tabbing}

}

\end{frame}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%												DTS CALC				                       %%

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%\begin{frame}\frametitle{Convolution: Calculation}

%TODO

%\end{frame}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%												DTS REQ  				                       %%

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\begin{frame}\frametitle{Convolution: Development effort}

{\small

\begin{center}

\begin{tabular}{l|l|r}

requirements            & comments             &effort\\ \hline\hline

simplify rationals      & \sisac               &     0\\ \hline

define $\sum\limits_{i=0}^{n}i$ & partly \sisac  &    10\\ \hline

simplify sum			      & termorder            &    10\\

                        & simplify rules       &    20\\

                        & use simplify rationals&     0\\ \hline

index adjustments       & with unit step       &      10\\ \hline

example collection      & with explanations    &    20\\ \hline\hline

                        &                      & 70-90\\

\end{tabular}

\end{center}

effort --- in 45min units\\

}

\end{frame}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%-----------------------------------------------------------------%

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\section[Z-transform]{Z-Transform}

\subsection[(Inverse) Z-Transform]{(Inverse) Z-Transform}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%												Z-Transform  INTRO                     %%

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\begin{frame}\frametitle{(Inverse) ${\cal Z}$-Transformation: Introduction}

\begin{itemize}

\item Pure Transformation is simple to realise with Z-Transform Properties (Table)

\item Partial Fraction are just math simplifications

\end{itemize}

\end{frame}

% does not fit?!

%\subsection[]{Indextranformation}

%\begin{frame}\frametitle{TODO}

%TODO

%\end{frame}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%												Z-Transform  SPEC                      %%

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\begin{frame}\frametitle{(Inverse) ${\cal Z}$-Transformation: Specification}

{\footnotesize\it

Determine the inverse $\cal{z}$ transform of the following expression. Hint: applay the partial fraction expansion.

\begin{center}

$X(z)=\frac{3}{z-\frac{1}{4}-\frac{1}{8}z^{-1}},\ \ x[n]$ is absolute summable

\end{center}

\begin{tabbing}

1\=postcond \=: \= \= $\;\;\;\;$\=\kill

\>given    \>:\>  Expression of z \\

\>         \> \>  \>(X (z::real\,+z::imag),3/(z-1/4-1/8\,z\textasciicircum{}(-1)))\\

\>precond  \>:\>  TODO\\

\>find     \>:\>  Expression of n\\

\>         \> \>  \>$h[n]$\\

\>postcond \>:\>  TODO\\

\end{tabbing}

}

\end{frame}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%												Z expl		CALC                         %%

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%\begin{frame}\frametitle{(Inverse) ${\cal Z}$-Transformation: Calculation}

%TODO

%\end{frame}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%												Z expl		REQ	                         %%

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\begin{frame}\frametitle{(Inverse) ${\cal Z}$-Transformation: Development effort}

{\small

\begin{center}

\begin{tabular}{l|l|r}

requirements            & comments             &effort\\ \hline\hline

solve for part.fract.   & \sisac: degree 2     &     0\\

                        & complex nomminators  &    30\\

                        & degree > 2           &    MT\\ \hline

simplify polynomial     & \sisac               &     0\\

simplify rational       & \sisac               &     0\\ \hline

part.fract.decomposition& degree 2             &      \\

                        & specification, method&    30\\ \hline

${\cal Z}^{-1}$ table    &                       &   20\\

                        & explanations, figures&    20\\ \hline

example collection      & with explanations    &    20\\ \hline\hline

                        &                      & 90-120\\

%                        &                      & 1 MT

\end{tabular}

\end{center}

effort --- in 45min units\\

MT --- thesis ``factorization'' (mathematics)

}

\end{frame}

\end{document}