1.1 --- a/doc-src/isac/mlehnfeld/presentation.tex Sun May 29 12:53:49 2011 +0200
1.2 +++ b/doc-src/isac/mlehnfeld/presentation.tex Sun May 29 18:14:43 2011 +0200
1.3 @@ -133,199 +133,335 @@
1.4 % - If you omit details that are vital to the proof/implementation,
1.5 % just say so once. Everybody will be happy with that.
1.6
1.7 -\section[Introduction]{Introduction}
1.8 -\subsection[Isabelle \& \isac]{Isabelle and \isac}
1.9 +\section[Introduction]{Introduction: Isabelle and \isac}
1.10 +%\subsection[Isabelle \& \isac]{Isabelle and \isac}
1.11 \begin{frame}
1.12 \frametitle{Isabelle and \isac}
1.13 - \begin{itemize}
1.14 - \item Computer Theorem Prover Isabelle
1.15 - \item Math Learning Assistent \isac
1.16 - \end{itemize}
1.17 +The task of this ``Projektpraktikum'' (6 ECTS) was to
1.18 +\begin{itemize}
1.19 +\item study the concept of ``context'' in the theorem prover \textbf{Isabelle} from TU Munich
1.20 +\item study basic concepts of the math assistant \sisac{} from TU Graz
1.21 +\pause
1.22 +\item redesign \sisac{} with respect to contexts
1.23 + \begin{itemize}
1.24 + \item use contexts for type inference of user input
1.25 + \item handle preconditions of specifications
1.26 + \item clarify the transfer of context data from sub-programs to the calling program
1.27 + \end{itemize}
1.28 +\pause
1.29 +\item introduce contexts to \sisac{} according to the new design
1.30 +\item use the coding standards of Isabelle2011 for new code.
1.31 +\end{itemize}
1.32 \end{frame}
1.33
1.34 -\subsection[Computation \& Deduction]{Computation and Deduction in a Lucas-Interpreter}
1.35 +%\subsection[Computation \& Deduction]{Computation and Deduction in a Lucas-Interpreter}
1.36 \begin{frame}
1.37 \frametitle{Computation and Deduction in a Lucas-Interpreter}
1.38 \includegraphics[width=100mm]{overview.pdf}
1.39 \end{frame}
1.40
1.41 -\section[Contributions]{Contributions of the project}
1.42 -\subsection[Contexts]{Introduction of Isabelle Contexts}
1.43 +\section[Contributions]{Contributions of the project to \isac}
1.44 +\subsection[Contexts]{Isabelle's Contexts, advantages and use}
1.45 \begin{frame}
1.46 - \frametitle{Introduction of Isabelle Contexts}
1.47 - \begin{itemize}
1.48 - \item theories too general
1.49 - \item not capable of type inference
1.50 - \item replace function \texttt{parseNEW}
1.51 - \item assumptions \& environment $\rightarrow$ context
1.52 - \end{itemize}
1.53 + \frametitle{Advantages of Isabelle's Contexts}
1.54 +Isabelle's context replaced theories because \dots:
1.55 +\begin{itemize}
1.56 +\item theories are static containers of \textit{all} logical data
1.57 +\item contexts are \textit{dynamic} containers of logical data:
1.58 + \begin{itemize}
1.59 + \item functions for storing and retrieving various logical data
1.60 + \item functions for type inference
1.61 + \item provide data for Isabelle's automated provers
1.62 + \end{itemize}
1.63 +%\item e.g. theories have no direct functions for type inference
1.64 +%\item replace function \texttt{parseNEW}
1.65 +%\item assumptions \& environment $\rightarrow$ context
1.66 +\item allow to conform with scopes for subprograms.
1.67 +\end{itemize}
1.68 \end{frame}
1.69
1.70 \begin{frame}
1.71 - \frametitle{Code Snippets: \texttt{parse}}
1.72 - \texttt{\tiny{
1.73 + \frametitle{Isabelle's context mechanism}
1.74 + \texttt{\small{
1.75 \begin{tabbing}
1.76 -xx\=xx\=xx\=xx\=\kill
1.77 -fun parse thy str =\\
1.78 -\>(let val t = (typ\_a2real o numbers\_to\_string)\\
1.79 -\>\>\>\>(Syntax.read\_term\_global thy str)\\
1.80 -\>\>in SOME (cterm\_of thy t) end)\\
1.81 -\>\>\>handle \_ => NONE;
1.82 -\\~\\~\\
1.83 -fun parseNEW ctxt str = SOME (Syntax.read\_term ctxt str |> numbers\_to\_string)\\
1.84 -\>\>\>handle \_ => NONE;
1.85 +xx\=xx\=in\=\kill
1.86 +%xx\=xx\=xx\=xx\=\kill
1.87 +%datatype Isac\_Ctxt =\\
1.88 +%\>\>Env of term * term\\
1.89 +%\>| Asm of term;\\
1.90 +%\\
1.91 +structure ContextData = \alert{Proof\_Data}\\
1.92 +\>~(\alert{type T} = term list\\
1.93 +\>\>\alert{fun init \_} = []);\\
1.94 +\\
1.95 +%local\\
1.96 +%\>fun insert\_ctxt data = ContextData\alert{.map} (fn xs => distinct (data@xs));\\
1.97 +%in\\
1.98 +%\>fun insert\_assumptions asms = map (fn t => Asm t) asms |> insert\_ctxt;\\
1.99 +%\>fun insert\_environments envs = map (fn t => Env t) envs |> insert\_ctxt;\\
1.100 +%end\\
1.101 +fun insert\_assumptions asms = \\
1.102 +\>\>\>ContextData\alert{.map} (fn xs => distinct (data@xs));\\
1.103 +\\
1.104 +%local\\
1.105 +%\>fun unpack\_asms (Asm t::ts) = t::(unpack\_asms ts)\\
1.106 +%\>\>| unpack\_asms (Env \_::ts) = unpack\_asms ts\\
1.107 +%\>\>| unpack\_asms [] = [];\\
1.108 +%\>fun unpack\_envs (Env t::ts) = t::(unpack\_envs ts)\\
1.109 +%\>\>| unpack\_envs (Asm \_::ts) = unpack\_envs ts\\
1.110 +%\>\>| unpack\_envs [] = [];\\
1.111 +%in\\
1.112 +%\>fun get\_assumptions ctxt = ContextData.get ctxt |> unpack\_asms;\\
1.113 +%\>fun get\_environments ctxt = ContextData.get ctxt |> unpack\_envs;\\
1.114 +%end
1.115 +fun get\_assumptions ctxt = ContextData\alert{.get} ctxt;\\
1.116 +\\
1.117 +\\
1.118 +val declare\_constraints : \\
1.119 +\>\>\>term -> Proof.context -> Proof.context
1.120 \end{tabbing}
1.121 }}
1.122 \end{frame}
1.123
1.124 -
1.125 \begin{frame}
1.126 - \frametitle{Code Snippets: context data}
1.127 - \texttt{\tiny{
1.128 + \frametitle{Usage of Contexts}
1.129 + \texttt{\footnotesize{
1.130 \begin{tabbing}
1.131 -xx\=xx\=xx\=xx\=\kill
1.132 -datatype Isac\_Ctxt =\\
1.133 -\>\>Env of term * term\\
1.134 -\>| Asm of term;\\
1.135 +xx\=xx\=xx\=xx\=xx\=\kill
1.136 +fun transfer\_asms\_from\_to from\_ctxt to\_ctxt =\\
1.137 +\> let\\
1.138 +\>\> val to\_vars = get\_assumptions to\_ctxt |> map vars |> flat\\
1.139 +\>\> fun transfer [] to\_ctxt = to\_ctxt\\
1.140 +\>\>\> | transfer (from\_asm::fas) to\_ctxt =\\
1.141 +\>\>\>\>\> if inter op = (vars from\_asm) to\_vars = []\\
1.142 +\>\>\>\>\> then transfer fas to\_ctxt\\
1.143 +\>\>\>\>\> else transfer fas (insert\_assumptions [from\_asm] to\_ctxt)\\
1.144 +\> in transfer (get\_assumptions from\_ctxt) to\_ctxt end\\
1.145 \\
1.146 -structure ContextData = Proof\_Data\\
1.147 -\>~(type T = Isac\_Ctxt list\\
1.148 -\>\>fun init \_ = []);\\
1.149 +fun parse thy str =\\
1.150 +\>(let val t = (\alert{typ\_a2real} o numbers\_to\_string)\\
1.151 +\>\>\>\>(\alert{Syntax.read\_term\_global thy} str)\\
1.152 +\>\>in SOME (cterm\_of thy t) end)\\
1.153 +\>\>\>handle \_ => NONE;\\
1.154 \\
1.155 -local\\
1.156 -\>fun insert\_ctxt data = ContextData.map (fn xs => distinct (data@xs));\\
1.157 -in\\
1.158 -\>fun insert\_assumptions asms = map (fn t => Asm t) asms |> insert\_ctxt;\\
1.159 -\>fun insert\_environments envs = map (fn t => Env t) envs |> insert\_ctxt;\\
1.160 -end\\
1.161 -\\
1.162 -local\\
1.163 -\>fun unpack\_asms (Asm t::ts) = t::(unpack\_asms ts)\\
1.164 -\>\>| unpack\_asms (Env \_::ts) = unpack\_asms ts\\
1.165 -\>\>| unpack\_asms [] = [];\\
1.166 -\>fun unpack\_envs (Env t::ts) = t::(unpack\_envs ts)\\
1.167 -\>\>| unpack\_envs (Asm \_::ts) = unpack\_envs ts\\
1.168 -\>\>| unpack\_envs [] = [];\\
1.169 -in\\
1.170 -\>fun get\_assumptions ctxt = ContextData.get ctxt |> unpack\_asms;\\
1.171 -\>fun get\_environments ctxt = ContextData.get ctxt |> unpack\_envs;\\
1.172 -end
1.173 +fun parseNEW ctxt str = \\
1.174 +\>\>\>SOME (\alert{Syntax.read\_term ctxt} str |> numbers\_to\_string)\\
1.175 +\>\>\>handle \_ => NONE;
1.176 \end{tabbing}
1.177 }}
1.178 +
1.179 +
1.180 \end{frame}
1.181
1.182 -\subsection[Redesign]{Redesign of Type Inference in \isac}
1.183 +\subsection[Redesign]{Redesign of \isac{} using contexts}
1.184 \begin{frame}
1.185 - \frametitle{Redesign of Type Inference in \isac}
1.186 - \begin{itemize}
1.187 - \item use context type inference
1.188 - \item parsing input (specification \& user input)
1.189 - \item specification with polymorphic types
1.190 - \item etc.
1.191 - \end{itemize}
1.192 + \frametitle{Redesign of \isac{} using contexts}
1.193 +\begin{center} DEMO \end{center}
1.194 \end{frame}
1.195
1.196 \begin{frame}
1.197 - \frametitle{Lines of Code}
1.198 - \begin{tabular}{lr}
1.199 - src/ & 1700 k \\
1.200 - src/Pure/ & 70 k \\
1.201 - src/Provers/ & 8 k \\
1.202 - src/Tools/ & 800 k \\
1.203 - src/Tools/isac/ & 37 k \\
1.204 - src/Tools/isac/Knowledge & 16 k \\
1.205 - \end{tabular}
1.206 + \frametitle{Deduction simplifies computation}
1.207 +\small{
1.208 +%\begin{onehalfspace}
1.209 +\begin{tabbing}
1.210 +xxx\=xxx\=\kill
1.211 + \`$\mathit{(some)}\;\mathit{assumptions}$\\
1.212 +$\mathit{solve}\;(\frac{x}{x ^ 2 - 6 * x + 9} - \frac{1}{x ^ 2 - 3 * x} = \frac{1}{x}, x)$\\
1.213 +% \`$x ^ 2 - 6 * x + 9\not=0\land x ^ 2 - 3 * x\not=0$\\
1.214 +%\>$\frac{x}{x ^ 2 - 6 * x + 9} - \frac{1}{x ^ 2 - 3 * x} = \frac{1}{x}$ \\ \\
1.215 +%\>$\frac{x}{x ^ 2 + -1 * (6 * x) + 9} + \frac{-1 * 1}{x ^ 2 + -1 * (3 * x)} = \frac{1}{x}$ \\ \\
1.216 +\>$\frac{3 + -1 * x + x ^ 2}{9 * x + -6 * x ^ 2 + x ^ 3} = \frac{1}{x}$ \\
1.217 + \`$x\not=3\land x\not=0$\\
1.218 +\>$(3 + -1 * x + x ^ 2) * x = 1 * (9 * x + -6 * x ^ 2 + x ^ 3)$ \\
1.219 +\>$\mathit{solve}\;((3 + -1 * x + x ^ 2) * x = 1 * (9 * x + -6 * x ^ 2 + x ^ 3), x)$ \\
1.220 +%\>\>$(3 + -1 * x + x ^ 2) * x = 1 * (9 * x + -6 * x ^ 2 + x ^ 3)$ \\
1.221 +%\>\>$(3 + -1 * x + x ^ 2) * x - 1 * (9 * x + -6 * x ^ 2 + x ^ 3) = 0$ \\
1.222 +\>\>$(3 + -1 * x + x ^ 2) * x - (9 * x + -6 * x ^ 2 + x ^ 3) = 0$ \\
1.223 +\>\>$-6 * x + 5 * x ^ 2 = 0$ \\
1.224 +\>\>$\mathit{solve}\;(-6 * x + 5 * x ^ 2 = 0, x)$ \\
1.225 +\>\>$[x = 0, x = \frac{6}{5}]$ \\
1.226 + \`$x = 0\land x = \frac{6}{5}$\\
1.227 +\>$[\alert{x = 0}, x = \frac{6}{5}]$ \\
1.228 + \`\alert{$\mathit{Check\_Elementwise}\;\mathit{Assumptions}:x\not=0\land x = 0$}\\
1.229 +\>$[x = \frac{6}{5}]$ \\
1.230 +$[x = \frac{6}{5}]$
1.231 +\end{tabbing}
1.232 +}
1.233 +%\end{onehalfspace}
1.234 \end{frame}
1.235
1.236 +\begin{frame}
1.237 + \frametitle{More ``deduction'', \\less ``computation''}
1.238 +\footnotesize{\tt
1.239 +\begin{tabbing}
1.240 +xx\=xx\=xx\=xx\=xx\=xx\=\kill
1.241 +Script Solve\_root\_equation (e\_e::bool) (v\_v::real) = \\
1.242 +\> (let e\_e = ((Try (Rewrite\_Set norm\_equation False)) \@\@ \\
1.243 +\>\>\> (Try (Rewrite\_Set Test\_simplify False))) e\_e; \\
1.244 +\>\> (L\_L::bool list) = \\
1.245 +\>\>\> (SubProblem (Test', \\
1.246 +\>\>\>\> [linear,univariate,equation,test]\\
1.247 +\>\>\>\> [Test,solve\_linear]) \\
1.248 +\>\>\>\> [BOOL e\_e, REAL v\_v]) \\
1.249 +\> in \alert{Check\_elementwise L\_L \{(v\_v::real). Assumptions\}})\\
1.250 +\end{tabbing}
1.251 +}
1.252 +\small{
1.253 +``Deductive'' part of Lucas-Interpretation relives the ``computational'' part: \alert{one statement becomes obsolete~!}
1.254 +}
1.255 +\end{frame}
1.256 +
1.257 +
1.258 +\begin{frame}
1.259 + \frametitle{Redesign of \isac{} using contexts}
1.260 +Advantages of the redesign:
1.261 +\begin{itemize}
1.262 +\item type inference by \textit{local} contexts\\
1.263 +\pause
1.264 + \alert{now user-input without type constraints~!}
1.265 +\pause
1.266 +\item consistent handling of logical data
1.267 + \begin{itemize}
1.268 + \item preconditions and partiality conditions in contexts
1.269 + \item transfer of context data into subprograms clarified
1.270 + \item transfer of context data from subprograms clarified
1.271 + \end{itemize}
1.272 +\pause
1.273 + \alert{now some statements become obsolete.}\\
1.274 +\end{itemize}
1.275 +\pause
1.276 +Now Lucas-interpretation shifts efforts from ``computation'' further to ``deduction''.
1.277 +\end{frame}
1.278 +
1.279 +
1.280 +
1.281 \subsection[Code Improvement]{Improvement of functional code}
1.282 \begin{frame}
1.283 \frametitle{Improvement of functional code}
1.284 \begin{itemize}
1.285 - \item combinators
1.286 - \item code conventions
1.287 + \item \textbf{code conventions}: Isabelle2011 published coding standards first time
1.288 + \item \textbf{combinators}: Isabelle2011 introduced a library containing the following combinators:
1.289 +\\\vspace{0.2cm}
1.290 +\tiny{\tt%
1.291 + val |$>$ : 'a * ('a -$>$ 'b) -$>$ 'b\\
1.292 + val |-$>$ : ('c * 'a) * ('c -$>$ 'a -$>$ 'b) -$>$ 'b\\
1.293 + val |$>>$ : ('a * 'c) * ('a -$>$ 'b) -$>$ 'b * 'c\\
1.294 + val ||$>$ : ('c * 'a) * ('a -$>$ 'b) -$>$ 'c * 'b\\
1.295 + val ||$>>$ : ('c * 'a) * ('a -$>$ 'd * 'b) -$>$ ('c * 'd) * 'b\\
1.296 + val \#$>$ : ('a -$>$ 'b) * ('b -$>$ 'c) -$>$ 'a -$>$ 'c\\
1.297 + val \#-$>$ : ('a -$>$ 'c * 'b) * ('c -$>$ 'b -$>$ 'd) -$>$ 'a -$>$ 'd\\
1.298 + val \#$>>$ : ('a -$>$ 'c * 'b) * ('c -$>$ 'd) -$>$ 'a -$>$ 'd * 'b\\
1.299 + val \#\#$>$ : ('a -$>$ 'c * 'b) * ('b -$>$ 'd) -$>$ 'a -$>$ 'c * 'd\\
1.300 + val \#\#$>>$ : ('a -$>$ 'c * 'b) * ('b -$>$ 'e * 'd) -$>$ 'a -$>$ ('c * 'e) * 'd\\
1.301 +}
1.302 \end{itemize}
1.303 \end{frame}
1.304
1.305 \begin{frame}
1.306 - \frametitle{Combinators \& Code Conventions}
1.307 - \texttt{\tiny{
1.308 + \frametitle{Example with combinators}
1.309 + \texttt{\footnotesize{
1.310 \begin{tabbing}
1.311 -xx\=xx\=xx\=xx\=xx\=\kill
1.312 +xx\=xx\=xx\=xx\=xx\=xx\=xx\=xx\=\kill
1.313 fun prep\_ori [] \_ \_ = ([], e\_ctxt)\\
1.314 \>| prep\_ori fmz thy pbt =\\
1.315 \>\>\>let\\
1.316 -\>\>\>\>val ctxt = ProofContext.init\_global thy |> fold declare\_constraints fmz\\
1.317 -\>\>\>\>val ori = map (add\_field thy pbt o split\_dts o the o parseNEW ctxt) fmz\\
1.318 -\>\>\>\>\>|> add\_variants\\
1.319 +\>\>\>\>val ctxt = ProofContext.init\_global thy \\
1.320 +\>\>\>\>\> |> fold declare\_constraints fmz\\
1.321 +\>\>\>\>val ori = \\
1.322 +\>\>\>\>\> map (add\_field thy pbt o split\_dts o the o parseNEW ctxt) fmz\\
1.323 +\>\>\>\>\>\> |> add\_variants\\
1.324 \>\>\>\>val maxv = map fst ori |> max\\
1.325 \>\>\>\>val maxv = if maxv = 0 then 1 else maxv\\
1.326 \>\>\>\>val oris = coll\_variants ori\\
1.327 -\>\>\>\>\>|> map (replace\_0 maxv |> apfst)\\
1.328 -\>\>\>\>\>|> add\_id\\
1.329 -\>\>\>\>\>|> map flattup\\
1.330 +\>\>\>\>\> |> map (replace\_0 maxv |> apfst)\\
1.331 +\>\>\>\>\> |> add\_id\\
1.332 +\>\>\>\>\> |> map flattup\\
1.333 \>\>\>in (oris, ctxt) end;
1.334 \end{tabbing}
1.335 }}
1.336 +\dots which probably can be further polished.
1.337 \end{frame}
1.338
1.339 -\begin{frame}
1.340 - \frametitle{Drop \tt{Check\_Elementwise}!}
1.341 +%\subsection[Future Development]{Preparation of Future Development}
1.342 +%\begin{frame}
1.343 +% \frametitle{Preparation of Future Development}
1.344 +%
1.345 +%% "Script Solve_root_equation (e_e::bool) (v_v::real) = " ^
1.346 +%% " (let e_e = ((Try (Rewrite_Set norm_equation False)) @@ " ^
1.347 +%% " (Try (Rewrite_Set Test_simplify False))) e_e; " ^
1.348 +%% " (L_L::bool list) = " ^
1.349 +%% " (SubProblem (Test', " ^
1.350 +%% " [linear,univariate,equation,test]," ^
1.351 +%% " [Test,solve_linear]) " ^
1.352 +%% " [BOOL e_e, REAL v_v]) " ^
1.353 +%% " in Check_elementwise L_L {(v_v::real). Assumptions}) "
1.354 +%\end{frame}
1.355 +%
1.356 +%\begin{frame}
1.357 +% \frametitle{Preparation of Future Development}
1.358 +% \begin{itemize}
1.359 +% \item logical data for Isabelle provers in contexts
1.360 +% \item \isac{} programming language more compact\\
1.361 +% $\rightarrow$ context built automatically
1.362 +% \end{itemize}
1.363 +%\end{frame}
1.364
1.365 -\small{
1.366 -%\begin{onehalfspace}
1.367 -\begin{tabbing}
1.368 -xxx\=xxx\=\kill
1.369 -$\mathit{solve}\;(\frac{x}{x ^ 2 - 6 * x + 9} - \frac{1}{x ^ 2 - 3 * x} = \frac{1}{x}, x)$\\ \\
1.370 -\>$\frac{x}{x ^ 2 - 6 * x + 9} - \frac{1}{x ^ 2 - 3 * x} = \frac{1}{x}$ \\ \\
1.371 -\>$\frac{x}{x ^ 2 + -1 * (6 * x) + 9} + \frac{-1 * 1}{x ^ 2 + -1 * (3 * x)} = \frac{1}{x}$ \\ \\
1.372 -%\>$\frac{3 + -1 * x + x ^ 2}{9 * x + -6 * x ^ 2 + x ^ 3} = \frac{1}{x}$ \\ \\
1.373 -\>$(3 + -1 * x + x ^ 2) * x = 1 * (9 * x + -6 * x ^ 2 + x ^ 3)$ \\
1.374 -\>$\mathit{solve}\;((3 + -1 * x + x ^ 2) * x = 1 * (9 * x + -6 * x ^ 2 + x ^ 3), x)$ \\
1.375 -\>\>$(3 + -1 * x + x ^ 2) * x = 1 * (9 * x + -6 * x ^ 2 + x ^ 3)$ \\
1.376 -%\>\>$(3 + -1 * x + x ^ 2) * x - 1 * (9 * x + -6 * x ^ 2 + x ^ 3) = 0$ \\
1.377 -\>\>$(3 + -1 * x + x ^ 2) * x - (9 * x + -6 * x ^ 2 + x ^ 3) = 0$ \\
1.378 -\>\>$-6 * x + 5 * x ^ 2 = 0$ \\
1.379 -\>\>$\mathit{solve}\;(-6 * x + 5 * x ^ 2 = 0, x)$ \\
1.380 -\>\>$[x = 0, x = \frac{6}{5}]$ \\
1.381 -\>$[x = 0, x = \frac{6}{5}]$ \\
1.382 - \`\alert{$\mathit{Check\_Elementwise}\;\mathit{Assumptions}$}\\
1.383 -\>$[x = \frac{6}{5}]$ \\
1.384 -$[x = \frac{6}{5}]$
1.385 -\end{tabbing}
1.386 -}
1.387 -%\end{onehalfspace}
1.388 -
1.389 -\end{frame}
1.390 -
1.391 -\subsection[Future Development]{Preparation of Future Development}
1.392 -\begin{frame}
1.393 - \frametitle{Preparation of Future Development}
1.394 - \begin{itemize}
1.395 - \item logical data for Isabelle provers in contexts
1.396 - \item \isac{} programming language more compact\\
1.397 - $\rightarrow$ context built automatically
1.398 - \end{itemize}
1.399 -\end{frame}
1.400 -
1.401 -\begin{frame}
1.402 - \frametitle{jedit demonstration}
1.403 - DEMO
1.404 -\end{frame}
1.405
1.406 \section[Problems]{Problems encountered in the project}
1.407 \begin{frame}
1.408 \frametitle{Problems encountered in the project}
1.409 \begin{itemize}
1.410 - \item publication of new Isabelle release
1.411 - \item amount of code in Isabelle and \isac
1.412 + \item new Isabelle release in February 2011: update \sisac{} first
1.413 +\pause
1.414 + \item lines of code (LOC) in Isabelle and \sisac{}\\ \vspace{0.2cm}
1.415 +\textit{
1.416 + \begin{tabular}{lrl}
1.417 + src/ & 1700 & $\,$k LOC\\
1.418 + src/Pure/ & 70 & k LOC\\
1.419 + src/Provers/ & 8 & k LOC\\
1.420 + src/Tools/ & 800 & k LOC\\
1.421 + src/Tools/isac/ & 37 & k LOC\\
1.422 + src/Tools/isac/Knowledge & 16 & k LOC
1.423 + \end{tabular}
1.424 +}
1.425 +\pause
1.426 \item changes scattered throughout the code ($\rightarrow$ grep)
1.427 +\pause
1.428 + \item documentation of Isabelle very ``technical'' (no API)
1.429 +\pause
1.430 + \item documentation of \sisac{} not up to date
1.431 \end{itemize}
1.432 \end{frame}
1.433
1.434 +%\begin{frame}
1.435 +% \frametitle{Lines of Code}
1.436 +% \begin{tabular}{lr}
1.437 +% src/ & 1700 k \\
1.438 +% src/Pure/ & 70 k \\
1.439 +% src/Provers/ & 8 k \\
1.440 +% src/Tools/ & 800 k \\
1.441 +% src/Tools/isac/ & 37 k \\
1.442 +% src/Tools/isac/Knowledge & 16 k \\
1.443 +% \end{tabular}
1.444 +%\end{frame}
1.445 +
1.446 \section{Summary}
1.447 \begin{frame}
1.448 \frametitle{Summary}
1.449 -TODO
1.450 +The project succeeded in all goals:
1.451 +\begin{itemize}
1.452 +\item implemented Isabelle's contexts in \sisac{} such that
1.453 +\item user input requires no type constraints anymore
1.454 +\item consistent logical data is prepared for Isabelle's provers
1.455 +\end{itemize}
1.456 +\pause
1.457 +The course of the project was close to the plan:
1.458 +\begin{itemize}
1.459 +\item faster in writing new code
1.460 +\item slower in integrating the code into \sisac
1.461 +\end{itemize}
1.462 +\pause
1.463 +The project provided essential prerequisites for further development of the Lucas-interpreter.
1.464 \end{frame}
1.465
1.466 \end{document}