
diff -r 7f3760f39bdc -r f8845fc8f38d src/Doc/isac/jrocnik/final/jrocnik_present1.tex
--- a/src/Doc/isac/jrocnik/final/jrocnik_present1.tex	Mon Sep 16 12:27:20 2013 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,434 +0,0 @@
-
-\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}
-
-




