1.1 --- a/doc-src/isac/jrocnik/Inverse_Z_Transform/Inverse_Z_Transform.thy Mon Sep 19 08:47:07 2011 +0200
1.2 +++ b/doc-src/isac/jrocnik/Inverse_Z_Transform/Inverse_Z_Transform.thy Tue Sep 20 10:59:55 2011 +0200
1.3 @@ -166,7 +166,7 @@
1.4 *}
1.5
1.6 subsubsection {*get solutions out of list*}
1.7 -text {*in isac's CTP-based programming language: let s_1 = NTH 1 solutions; s_2 = NTH 2...*}
1.8 +text {$*in isac's CTP-based programming language: let$ $s_1 = NTH 1$ solutions; $s_2 = NTH 2...$*}
1.9 ML {*
1.10 val Const ("List.list.Cons", _) $ s_1 $ (Const ("List.list.Cons", _) $
1.11 s_2 $ Const ("List.list.Nil", _)) = solutions;
1.12 @@ -469,13 +469,31 @@
1.13
1.14
1.15 subsection {*Stepwise Execute the Program*}
1.16 +
1.17 +ML {*
1.18 +val thy = @{theory};
1.19 +(*val SOME func = parseNEW ctxt "X = 3 / (z - 1/4 + -1/8 * (1/z))"; term2str fun1;*)
1.20 +val fmz = ["equality X = 3 / (z - 1/4 + -1/8 * (1/z))", "solveFor A","solutions L"];
1.21 +val (dl,pl,ml) = ("isac", ["SignalProcessing", "Z_Transform", "inverse"], ["met_SP_Ztrans_inv"]);
1.22 +val (p,_,fb,nxt,_,pt) = CalcTreeTEST [(fmz, (dl,pl,ml))];
1.23 +val (p,_,fb,nxt,_,pt) = me nxt p [] pt
1.24 +*}
1.25 +
1.26 +ML {*
1.27 +f2str fb;
1.28 +*}
1.29 +
1.30 ML {*
1.31 val fmz = ["equality (3 = -3 * B / (4::real))", "solveFor B","solutions L"];
1.32 val (dI',pI',mI') =("Isac", ["univariate","equation"], ["no_met"]);
1.33 val (p,_,fb,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.34 val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
1.35 val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
1.36 +*}
1.37 +
1.38 +ML {*
1.39 val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
1.40 +f2str fb;
1.41 *}
1.42
1.43
2.1 --- a/doc-src/isac/jrocnik/Test_SUM.thy Mon Sep 19 08:47:07 2011 +0200
2.2 +++ b/doc-src/isac/jrocnik/Test_SUM.thy Tue Sep 20 10:59:55 2011 +0200
2.3 @@ -14,7 +14,8 @@
2.4 *}
2.5 section {*sums*}
2.6 ML {*
2.7 -@{term "(SUM i = 0..< k. f i)"}
2.8 +val x = @{term "(SUM i = 0..< k. f i)"};
2.9 +term2str x
2.10 *}
2.11 ML {*
2.12 *}
3.1 --- a/doc-src/isac/jrocnik/bakkarbeit_jrocnik.tex Mon Sep 19 08:47:07 2011 +0200
3.2 +++ b/doc-src/isac/jrocnik/bakkarbeit_jrocnik.tex Tue Sep 20 10:59:55 2011 +0200
3.3 @@ -22,10 +22,12 @@
3.4 \Large{
3.5 \bf Interactive Course Material for Signal Processing based on Isabelle/\isac\\~\\
3.6 }
3.7 - \sisac-Projektteam des Instituts für Softwaretechnologie,\\Technische Universität Graz\\
3.8 + \sisac-Team of the Institute for Software Technology,\\~\\
3.9 + in Cooperation with the Institute of Signal Processing and Speech Communication\\~\\
3.10 + Graz University of Technology\\
3.11 \vspace{0.7cm}
3.12 \large{
3.13 - Betreuer: Dr. Walther Neuper
3.14 + Advisor: tba
3.15 }
3.16 }
3.17 \author{Jan Simon Rocnik\\{\tt jan.rocnik@student.tugraz.at}}
3.18 @@ -134,6 +136,8 @@
3.19
3.20 ...
3.21
3.22 +terms are not full simplified in traditional notations, in isac we have to simplify them complete to check weather results are compatible or not. in e.g. the solutions of an second order linear equation is an rational in isac but in tradition we keep fractions as long as possible and as long as they are 'beautiful' (1/8, 5/16,...)
3.23 +
3.24 \section{Implementation of Certain SP Problems}
3.25 todo
3.26
3.27 @@ -174,7 +178,7 @@
3.28 %\section*{Anhang}
3.29 \section{Demobeispiel}
3.30
3.31 -\input{./Inverse_Z_Transform/document/Inverse_Z_Transform.tex}
3.32 +%\input{./Inverse_Z_Transform/document/Inverse_Z_Transform.tex}
3.33
3.34 \begin{verbatim}
3.35