tuned decompose-isar
authorJan Rocnik <jan.rocnik@student.tugraz.at>
Tue, 20 Sep 2011 10:59:55 +0200
branchdecompose-isar
changeset 422768d642a598ca3
parent 42275 9f6d15630042
child 42277 78d34d2ac9f2
tuned
doc-src/isac/jrocnik/Inverse_Z_Transform/Inverse_Z_Transform.thy
doc-src/isac/jrocnik/Test_SUM.thy
doc-src/isac/jrocnik/bakkarbeit_jrocnik.tex
     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