
diff -r 7f3760f39bdc -r f8845fc8f38d doc-isac/jrocnik/final/jrocnik_present1.tex
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-isac/jrocnik/final/jrocnik_present1.tex	Tue Sep 17 09:50:52 2013 +0200
@@ -0,0 +1,434 @@
+
+\documentclass{beamer}
+
+
+\mode<presentation>
+{
+  \usetheme{Hannover}
+  \setbeamercovered{transparent}
+}
+
+\usepackage[english]{babel}
+\usepackage[utf8]{inputenc}
+\usepackage{times}
+\usepackage[T1]{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[Ro\v{c}nik]
+{Jan Rocnik}
+
+\institute % (optional, but mostly needed)
+{
+  Technische Universit\"at Graz\\
+  Institut f\"ur TODO
+}
+
+% 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}
+}
+
+\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}{Issues to be Accomplished}
+
+\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, by using mechanised knowledge?
+\item What problems and subproblems have to be solved?
+\item Which problems are already implemented in \sisac?
+\item How are the new problems specified (\sisac)?
+\item Which variantes of programms in \sisac\ solve the problems?
+\item What is the contents of the interactiv course material (Figures, etc.)?
+
+\end{itemize}
+\end{frame}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%---------------------------------------------------------------%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\section[Fourier]{Fourier transformation}
+\subsection[Fourier]{Fourier transform}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%												Fourier INTRO                          %%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\begin{frame}\frametitle{Fourier Transformation: Introduction}
+Possibilities:
+\begin{itemize}
+\item Transform operation by using property-tables
+\item Transform operation by using integral
+\end{itemize}
+Also Important:
+\begin{itemize}
+\item Visualisation?!
+\end{itemize}
+\end{frame}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%										Transform expl   SPEC                      %%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\begin{frame}\frametitle{Fourier Transformation: Specification}
+{\footnotesize
+
+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}
+
+\hrulefill
+
+\begin{tabbing}
+1\=postcond \=: \= \= $\;\;\;\;$\=\kill
+\>given    \>:\>  piecewise\_function \\
+\>         \> \>  \>$fun (x (t::real),\ x=1\ ((t>=-1)\ \&\ (t<=1)),\ x=0)$\\
+\>precond  \>:\>  TODO\\
+\>find     \>:\>  $X(j\cdot\omega)$\\
+\>postcond \>:\>  TODO\\
+\end{tabbing}
+
+}
+\end{frame}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%												Transform expl   REQ                   %%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\begin{frame}\frametitle{Fourier Transform: 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-----------------------%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\begin{frame}{Fourier Transformation: Summary}
+\begin{itemize}
+
+\item Standard integrals can be solved with tables
+\item No real integration (yet avaible)
+\item Math \emph{tricks} difficult to implement
+
+
+\end{itemize}
+\end{frame}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%-----------------------------------------------------------------%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\section[LTI Systems]{LTI systems}
+\subsection[Convolution]{Convolution (Faltung)}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%												LTI INTRO				                       %%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\begin{frame}\frametitle{Convolution: Introduction}
+\begin{itemize}
+\item Calculation include sums
+\item Demonstrative examples
+\item Visualisation is important
+\end{itemize}
+\end{frame}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%												LTI SPEC				                       %%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\begin{frame}\frametitle{Convolution: Specification}
+{\footnotesize
+
+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]$.
+
+\hrulefill
+
+\begin{tabbing}
+1\=postcond \=: \= \= $\;\;\;\;$\=\kill
+\>given    \>:\>  Signals h1[n], h2[n] \\
+\>         \> \>  \>((h1[n]=(3/5)\textasciicircum{}n*u[n]),\,h2[n]=(-2/3)\textasciicircum{}n*u[n]))\\
+                        
+\>precond  \>:\>  TODO\\
+\>find     \>:\>  $h1[n]\,*\,h2[n]$\\
+\>postcond \>:\>  TODO\\
+\end{tabbing}
+
+}
+\end{frame}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%												LTI 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}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%--------------------LTI-------Conclusion-----------------------%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\begin{frame}{Convolution: Summary}
+\begin{itemize}
+
+\item Standard example
+\item Straight forward
+\item Challenge are sum limits
+
+\end{itemize}
+\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}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%												Z-Transform  SPEC                      %%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\begin{frame}\frametitle{(Inverse) Z-Transformation: Specification}
+{\footnotesize
+
+Determine the inverse 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}
+
+
+\hrulefill
+
+\begin{tabbing}
+1\=postcond \=: \= \= $\;\;\;\;$\=\kill
+\>given    \>:\>  Expression of z \\
+\>         \> \>  \>(X (z::complex),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		REQ	                         %%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+
+\begin{frame}\frametitle{(Inverse) 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}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%--------------------Z-TRANS---Conclusion-----------------------%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\begin{frame}{(Inverse) Z-Transformation: Summary}
+\begin{itemize}
+
+\item No \emph{higher} math operations
+\item Different subproblems of math (equation systems, etc.)
+\item Both directions have the same effort
+
+\end{itemize}
+\end{frame}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%-----------------------------------------------------------------%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\section[Conclusions]{Conclusions}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%--------------------------DEMONSTRATION--------------------------%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\begin{frame}{Demonstration}
+
+\centering{Demonstration}
+
+\end{frame}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%--------------------------CONCLUSION-----------------------------%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\begin{frame}{Conclusions}
+
+Design Challanges:
+
+{\small
+\begin{itemize}
+
+\item Pre and Post conditions
+\item Exact mathematic behind functions
+\item Accurate mathematic notation
+
+\end{itemize}
+}
+
+Goals:
+{\small
+\begin{itemize}
+
+\item Spot the power of \sisac
+\item Implementation of generell but simple math problems
+\item Setting up a good first guideline (documentation) for furher problem implemenations
+
+\end{itemize}
+
+\centering{Efforts are only approximations, due we have no \emph{real} experience data!}
+}
+
+\end{frame}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%--------------------------TIME LINE------------------------------%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\begin{frame}{Comming up}
+
+{\small
+\begin{tabular}{l r}
+
+Juli 2011 & project startup\\
+Juli 2011 & information collection, 1st presentation\\
+August 2011 & extern traineeship\\
+September 2011 & main work\\
+after Oktober & finishing, documentation\\
+
+\end{tabular}
+}
+
+\end{frame}
+
+
+\end{document}
+
+




