1.1 --- a/doc-src/isac/jrocnik/jrocnik_cadgme.tex Wed Jun 20 11:14:04 2012 +0200
1.2 +++ b/doc-src/isac/jrocnik/jrocnik_cadgme.tex Thu Jun 21 20:48:36 2012 +0200
1.3 @@ -10,9 +10,10 @@
1.4
1.5 \usepackage{color}
1.6 \definecolor{lgray}{RGB}{238,238,238}
1.7 +\definecolor{gray}{rgb}{0.8,0.8,0.8}
1.8
1.9 \useoutertheme[subsection=false]{smoothbars}
1.10 -\useinnertheme{circles}
1.11 +%\useinnertheme{circles}
1.12
1.13 \setbeamercolor{block title}{fg=black,bg=gray}
1.14 \setbeamercolor{block title alerted}{use=alerted text,fg=black,bg=alerted text.fg!75!bg}
1.15 @@ -44,8 +45,6 @@
1.16 }
1.17
1.18 \setbeamertemplate{navigation symbols}{}
1.19 -
1.20 -\definecolor{gray}{rgb}{0.8,0.8,0.8}
1.21 \setbeamercolor{footline}{fg=black,bg=gray}
1.22
1.23 % Fusszeile mit Autor, Titel und Foliennummer / Gesamtfolienzahl
1.24 @@ -103,7 +102,7 @@
1.25 \subsection{isabelle}
1.26 \begin{frame}
1.27 \frametitle{What is Isabelle?}
1.28 - \begin{spacing}{1.5}
1.29 + \begin{spacing}{2}
1.30 \begin{itemize}
1.31 \item Generic Proof Assistant
1.32 \item Formula proofing in logical calculus
1.33 @@ -115,7 +114,7 @@
1.34 \subsection{isac}
1.35 \begin{frame}
1.36 \frametitle{What is {\isac}?}
1.37 - \begin{spacing}{1.5}
1.38 + \begin{spacing}{1.7}
1.39 \begin{itemize}
1.40 \item \textcolor{tug}{${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal A}$}belle for~{}\textcolor{tug}{${\cal C}$}alculations
1.41 \item Interactive Course Material
1.42 @@ -146,45 +145,35 @@
1.43 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1.44
1.45 \begin{frame}
1.46 - \frametitle{Work flow}
1.47 - \begin{spacing}{1.8}
1.48 - \begin{itemize}
1.49 - \item Problem Analysis
1.50 - \item Information Collection
1.51 - \item \textbf{TP-Programming}
1.52 - \item Documentation
1.53 - \end{itemize}
1.54 + \frametitle{Course Material Creation {\normalsize Iterations}} %tasks? work flow?
1.55 + \begin{spacing}{1.3}
1.56 + \begin{enumerate}
1.57 + \item Problem Analysis\\
1.58 + {\small Calculation possiblities, Featured Steps} %example partial fractions
1.59 + \item Information Collection\\
1.60 + {\small Possiblies and Challanges in {\sisac{}}}
1.61 + \item \textbf{TP-Programming}
1.62 + \item Documentation\\
1.63 + {\small Representation of underlying knowledge in the system}
1.64 + \end{enumerate}
1.65 \end{spacing}
1.66 \end{frame}
1.67
1.68 \subsection{issues}
1.69 \begin{frame}
1.70 - \frametitle{Issues to Accomplish I}
1.71 - \begin{spacing}{1.4}
1.72 + \frametitle{Issues to Accomplish {\normalsize Information Collection}}
1.73 + \begin{spacing}{1.3}
1.74 \begin{itemize}
1.75 \item What knowledge is mechanized in Isabelle?\\
1.76 {\small How about new?}
1.77 \item What problems are implemented in {\sisac{}}?\\
1.78 {\small How about new?}
1.79 - \item What is the effort?
1.80 + \item What is the contents of the interactive course material?\\
1.81 + {\small Figures, Explanations,\ldots}
1.82 \end{itemize}
1.83 \end{spacing}
1.84 \end{frame}
1.85
1.86 -\begin{frame}
1.87 - \frametitle{Issues to Accomplish II}
1.88 -\begin{spacing}{1.4}
1.89 -\begin{itemize}
1.90 - \item How look calculations like?\\
1.91 - {\small Ansatzs, Subproblems?}
1.92 - \item How are problems specified?\\
1.93 - {\small Given, Pre-/Postcondition, Find?}
1.94 - \item What is the contents of the interactive course material?\\
1.95 - {\small Figures, Explanations,\ldots}
1.96 -\end{itemize}
1.97 -\end{spacing}
1.98 -\end{frame}
1.99 -
1.100 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1.101 \section{Details}
1.102 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1.103 @@ -204,25 +193,44 @@
1.104 \end{frame}
1.105
1.106 \begin{frame}
1.107 - \frametitle{Technical Survey II {\normalsize Notation Problems} }
1.108 - \begin{spacing}{1.5}
1.109 + \frametitle{Technical Survey II {\normalsize Representation Problems} }
1.110 + \begin{spacing}{1.9}
1.111 \begin{itemize}
1.112 \item Different brackets have different meanings\\
1.113 {\small $u[n] \neq u(n)$\ldots in Math; but also in the source code}
1.114 - \item Simplification, tricks and beauty\\
1.115 - {\small $X\cdot(a+b)+Y\cdot(c+d)=aX+bX+cY+dY$}\\
1.116 - {\small $\frac{1}{j\omega}\cdot\left(e^{-j\omega}-e^{j3\omega}\right)=\frac{1}{j\omega}\cdot e^{-j2\omega}\cdot\left(e^{j\omega}-e^{-j\omega}\right)=$}\\
1.117 - {\small $=\frac{1}{\omega}\, e^{-j2\omega}\cdot\colorbox{lgray}{$\frac{1}{j}\,\left(e^{j\omega}-e^{-j\omega}\right)$}=\frac{1}{\omega}\,e^{-j2\omega}\cdot\colorbox{lgray}{$2\, sin(\omega)$} $}
1.118 + \item We need Symbols, Indizes and Hochzahlen
1.119 + \item Different Representations for different purpos %winkel in polar oder kartesischen koordinaten usw.
1.120 \end{itemize}
1.121 \end{spacing}
1.122 \end{frame}
1.123
1.124 +\begin{frame}
1.125 + \frametitle{Technical Survey III {\normalsize Notation Problems} }
1.126 + \begin{spacing}{1.8}
1.127 + \begin{center}
1.128 + Simplification, tricks and beauty\\
1.129 + \vspace{7mm}
1.130 + {\small $X\cdot(a+b)+Y\cdot(c+d)=aX+bX+cY+dY$}\\
1.131 + \vspace{3mm}
1.132 + {\small $\frac{1}{j\omega}\cdot\left(e^{-j\omega}-e^{j3\omega}\right)=\frac{1}{j\omega}\cdot e^{-j2\omega}\cdot\left(e^{j\omega}-e^{-j\omega}\right)=$}\\
1.133 + {\small $=\frac{1}{\omega}\, e^{-j2\omega}\cdot\colorbox{lgray}{$\frac{1}{j}\,\left(e^{j\omega}-e^{-j\omega}\right)$}=\frac{1}{\omega}\,e^{-j2\omega}\cdot\colorbox{lgray}{$2\, sin(\omega)$} $}
1.134 + \end{center}
1.135 + \end{spacing}
1.136 +\end{frame}
1.137 +
1.138 \subsection{Demonstration}
1.139 \begin{frame}
1.140 \frametitle{Demonstration of {\isac}}
1.141 \begin{spacing}{1.5}
1.142 \begin{itemize}
1.143 - \item TODO
1.144 + \item Frontend - {\small The shiny side\ldots}
1.145 + \item Backend - {\small The dark side\ldots}
1.146 + \begin{itemize}
1.147 + \item Equation solving
1.148 + \item Notation problems, Working with Rulesets
1.149 + \item Framework expansion
1.150 + \item My Work
1.151 + \end{itemize}
1.152 \end{itemize}
1.153 \end{spacing}
1.154 \end{frame}
1.155 @@ -231,6 +239,7 @@
1.156 \section{Summary}
1.157 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1.158
1.159 +\subsection{conclusion}
1.160 \begin{frame}
1.161 \frametitle{Conclusion}
1.162 \begin{spacing}{1.2}
1.163 @@ -238,6 +247,7 @@
1.164 \item TP-based language not ready
1.165 \item Programming guideline not yet sufficient
1.166 \item Hope for usability in enginieering studies
1.167 + \item Wide range of interested people
1.168 \vspace{5mm}
1.169 \item Hard to spend 200h on 1 programm
1.170 \item \isac{} pointed at my own error
1.171 @@ -245,16 +255,16 @@
1.172 \end{spacing}
1.173 \end{frame}
1.174
1.175 -
1.176 +\subsection{contact}
1.177 \begin{frame}
1.178 \frametitle{Contact}
1.179 - \begin{spacing}{1.2}
1.180 - \begin{itemize}
1.181 - \item Isabelle \href{isabelle.in.tum.de}{isabelle.in.tum.de}
1.182 - \item The {\sisac}-Project: \href{www.ist.tugraz.at/isac}{www.ist.tugraz.at/isac}
1.183 - \item Projectleader: \href{mailto:neuper@ist.tugraz.at}{neuper@ist.tugraz.at}
1.184 - \item Jan Rocnik: \href{mailto:jan.rocnik@student.tugraz.at}{jan.rocnik@student.tugraz.at}
1.185 - \end{itemize}
1.186 + \begin{spacing}{1.7}
1.187 + \begin{tabular}{lr}
1.188 + Isabelle & \small \texttt{\href{isabelle.in.tum.de}{isabelle.in.tum.de}}\\
1.189 + The {\isac}-Project & \small \texttt{\href{www.ist.tugraz.at/isac}{www.ist.tugraz.at/isac}}\\
1.190 + Projectleader & \small \texttt{\href{mailto:neuper@ist.tugraz.at}{neuper@ist.tugraz.at}}\\
1.191 + Jan Rocnik & \small \texttt{\href{mailto:jan.rocnik@student.tugraz.at}{jan.rocnik@student.tugraz.at}}
1.192 + \end{tabular}
1.193 \end{spacing}
1.194 \end{frame}
1.195
2.1 --- a/test/Tools/isac/ADDTESTS/course/CADGME/example_1.thy Wed Jun 20 11:14:04 2012 +0200
2.2 +++ b/test/Tools/isac/ADDTESTS/course/CADGME/example_1.thy Thu Jun 21 20:48:36 2012 +0200
2.3 @@ -1,5 +1,8 @@
2.4 (* Title: example_1
2.5 Author: Jan Rocnik
2.6 + Description: The following Example can be used as an HOWTO on applying
2.7 + already implemented Subproblems. In example solving a
2.8 + linear equation.
2.9 (c) copyright due to license terms.
2.10 12345678901234567890123456789012345678901234567890123456789012345678901234567890
2.11 10 20 30 40 50 60 70 80
2.12 @@ -8,6 +11,9 @@
2.13 theory example_1 imports Isac
2.14 begin
2.15
2.16 +section{*Equation Solving*}
2.17 +text{*Setup equation, Calc Tree,\ldots*}
2.18 +
2.19 ML {*
2.20 val equation = "equality (-1 + -2 * z + 8 * z ^^^ 2 = (0::real))";
2.21 val expr = [ equation, "solveFor z", "solutions L"]; (*specification*)
2.22 @@ -19,12 +25,16 @@
2.23 ["no_met"]);
2.24
2.25 *}
2.26 +
2.27 +text{*Possible Check if the equation matches the designated Method*}
2.28
2.29 ML {*
2.30 match_pbl expr (get_pbt
2.31 ["abcFormula","degree_2","polynomial","univariate","equation"]);
2.32 *}
2.33
2.34 +text{*Step throuh the Calculation Tree*}
2.35 +
2.36 ML {*
2.37 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(expr, (dI',pI',mI'))];
2.38 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
3.1 --- a/test/Tools/isac/ADDTESTS/course/CADGME/example_2.thy Wed Jun 20 11:14:04 2012 +0200
3.2 +++ b/test/Tools/isac/ADDTESTS/course/CADGME/example_2.thy Thu Jun 21 20:48:36 2012 +0200
3.3 @@ -1,5 +1,7 @@
3.4 (* Title: example_2
3.5 Author: Jan Rocnik
3.6 + Description: The following Example can be used as an HOWTO on generating
3.7 + Rulesets and applying them to terms.
3.8 (c) copyright due to license terms.
3.9 12345678901234567890123456789012345678901234567890123456789012345678901234567890
3.10 10 20 30 40 50 60 70 80
3.11 @@ -8,8 +10,12 @@
3.12 theory example_2 imports Isac
3.13 begin
3.14
3.15 +section{*Symbol Representation*}
3.16 +
3.17 ML {*
3.18 - (*alpha --> "</alpha>" *)
3.19 + (*
3.20 + * alpha --> "</alpha>"
3.21 + *)
3.22 @{term "\<alpha> "};
3.23 @{term "\<delta> "};
3.24 @{term "\<phi> "};
3.25 @@ -17,6 +23,8 @@
3.26 term2str @{term "\<rho> "};
3.27 *}
3.28
3.29 +section{*Working with Rulesets*}
3.30 +
3.31 axiomatization where
3.32 rule1: "1 = \<delta>[n]" and
3.33 rule2: "|| z || > 1 ==> z / (z - 1) = u [n]" and
3.34 @@ -30,27 +38,31 @@
3.35 @{thm rule4};
3.36 *}
3.37
3.38 +text{*Create Ruleset and insert rules*}
3.39 +
3.40 ML {*
3.41 - val inverse_Z = append_rls "inverse_Z" e_rls
3.42 + val transform = append_rls "transform" e_rls
3.43 [ Thm ("rule3",num_str @{thm rule3}),
3.44 Thm ("rule4",num_str @{thm rule4}),
3.45 Thm ("rule1",num_str @{thm rule1})
3.46 ];
3.47 *}
3.48
3.49 +text{*Apply the Ruleset to a term*}
3.50 +
3.51 ML {*
3.52 - val t = str2term "z / (z - 1) + z / (z - \<alpha>) + 1";
3.53 - val SOME (t', asm) = rewrite_set_ thy true inverse_Z t;
3.54 - (*
3.55 - * Attention rule1 is applied before the expression is
3.56 - * checked for rule4 which would be correct!!!
3.57 - *)
3.58 + val t = str2term "z / (z - 1) + z / (z - \<alpha>) + 1::real";
3.59 + val SOME (t', asm) = rewrite_set_ thy true transform t;
3.60 *}
3.61
3.62 ML{*
3.63 term2str t';
3.64 term2str t' = "z / (z - ?\<delta> [?n]) + z / (z - \<alpha>) + ?\<delta> [?n]";
3.65 + term2str t' = "?u [?n] + \<alpha>^^^?n u[n] + ?\<delta> [?n]";
3.66 *}
3.67
3.68 +text{*Problems: Rule~1 is applied before the expression is checked for Rule~4
3.69 + which would be the correct one. Rule~1 only matches a part of the
3.70 + expression.*}
3.71
3.72 end
4.1 --- a/test/Tools/isac/ADDTESTS/course/CADGME/example_3.thy Wed Jun 20 11:14:04 2012 +0200
4.2 +++ b/test/Tools/isac/ADDTESTS/course/CADGME/example_3.thy Thu Jun 21 20:48:36 2012 +0200
4.3 @@ -1,5 +1,7 @@
4.4 -(* Title: example_2
4.5 +(* Title: example_3
4.6 Author: Jan Rocnik
4.7 + Description: The following Example can be used as an HOWTO on implementing
4.8 + new Functions within the ISAC-System.
4.9 (c) copyright due to license terms.
4.10 12345678901234567890123456789012345678901234567890123456789012345678901234567890
4.11 10 20 30 40 50 60 70 80
4.12 @@ -8,10 +10,20 @@
4.13 theory example_3 imports Isac
4.14 begin
4.15
4.16 +section{*Function Decleration*}
4.17 +text{*Following code should only represent an example and was taken as a
4.18 + snipset from Rationals.thy located in
4.19 + \texttt{/src/Tools/isac/Knowledge}*}
4.20 +
4.21 (*----START----Example Function Decleration from Rationals.thy----*)
4.22 +
4.23 +text{*Define Method name and input, output types*}
4.24 +
4.25 consts
4.26 get_denominator :: "real => real"
4.27
4.28 +text{*Always add a comment with the method name and where it can be found.*}
4.29 +
4.30 ML {*
4.31 (*
4.32 *("get_denominator",
4.33 @@ -29,8 +41,10 @@
4.34 *}
4.35 (*----END----Example Function Decleration from Rationals.thy----*)
4.36
4.37 +text{*Apply the Method to an expression.*}
4.38 +
4.39 ML{*
4.40 - val input = term_of (the (parse thy "get_denominator ((a +x)/b)"));
4.41 + val input = term_of (the (parse thy "get_denominator ((a + b) / c)"));
4.42 val SOME (_, output) = eval_get_denominator "" 0 input thy;
4.43 *}
4.44