% $Header: /cvsroot/latex-beamer/latex-beamer/solutions/conference-talks/conference-ornate-20min.en.tex,v 1.7 2007/01/28 20:48:23 tantau Exp $

 \documentclass{beamer}

 % This file is a solution template for:

 % - Talk at a conference/colloquium.

 % - Talk length is about 20min.

 % - Style is ornate.

 % Copyright 2004 by Till Tantau <tantau@users.sourceforge.net>.

 %

 % In principle, this file can be redistributed and/or modified under

 % the terms of the GNU Public License, version 2.

 %

 % However, this file is supposed to be a template to be modified

 % for your own needs. For this reason, if you use this file as a

 % template and not specifically distribute it as part of a another

 % package/program, I grant the extra permission to freely copy and

 % modify this file as you see fit and even to delete this copyright

 % notice.

 \mode<presentation>

 {

   \usetheme{Hannover}

   % or ...

   \setbeamercovered{transparent}

   % or whatever (possibly just delete it)

 }

 %\usepackage{setspace} %for "\begin{onehalfspace}"

 \usepackage[english]{babel}

 % or whatever

 \usepackage[utf8]{inputenc}

 % or whatever

 \usepackage{times}

 \usepackage[T1]{fontenc}

 % Or whatever. Note that the encoding and the font should match. If T1

 % does not look nice, try deleting the line with the 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[\isac: Computation \& Deduction] % (optional, use only with long paper titles)

 {Integrating Computation and Deduction\\

   in the \isac-System}

 \subtitle{Projektpraktikum: Introducing Isabelle's Contexts}

 \author[Lehnfeld] % (optional, use only with lots of authors)

 {Mathias~Lehnfeld}

 % - Give the names in the same order as the appear in the paper.

 % - Use the \inst{?} command only if the authors have different

 %   affiliation.

 \institute % (optional, but mostly needed)

 {

   Vienna University of Technology\\

   Institute of Computer Languages

 }

 % - Use the \inst command only if there are several affiliations.

 % - Keep it simple, no one is interested in your street address.

 % \date[CFP 2003] % (optional, should be abbreviation of conference name)

 % {Conference on Fabulous Presentations, 2003}

 % - Either use conference name or its abbreviation.

 % - Not really informative to the audience, more for people (including

 %   yourself) who are reading the slides online

 % \subject{Theoretical Computer Science}

 % This is only inserted into the PDF information catalog. Can be left

 % out.

 % 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}

 }

 % If you wish to uncover everything in a step-wise fashion, uncomment

 % the following command:

 %\beamerdefaultoverlayspecification{<+->}

 \begin{document}

 \begin{frame}

   \titlepage

 \end{frame}

 \begin{frame}{Outline}

   \tableofcontents

   % You might wish to add the option [pausesections]

 \end{frame}

 % Structuring a talk is a difficult task and the following structure

 % may not be suitable. Here are some rules that apply for this

 % solution:

 % - Exactly two or three sections (other than the summary).

 % - At *most* three subsections per section.

 % - Talk about 30s to 2min per frame. So there should be between about

 %   15 and 30 frames, all told.

 % - A conference audience is likely to know very little of what you

 %   are going to talk about. So *simplify*!

 % - In a 20min talk, getting the main ideas across is hard

 %   enough. Leave out details, even if it means being less precise than

 %   you think necessary.

 % - If you omit details that are vital to the proof/implementation,

 %   just say so once. Everybody will be happy with that.

 \section[Introduction]{Introduction}

 \subsection[Isabelle \& \isac]{Isabelle and \isac}

 \begin{frame}

   \frametitle{Isabelle and \isac}

     \begin{itemize}

     \item Computer Theorem Prover Isabelle

     \item Math Learning Assistent \isac

     \end{itemize}

 \end{frame}

 \subsection[Computation \& Deduction]{Computation and Deduction in a Lucas-Interpreter}

 \begin{frame}

   \frametitle{Computation and Deduction in a Lucas-Interpreter}

     \includegraphics[width=100mm]{overview.pdf}

 \end{frame}

 \section[Contributions]{Contributions of the project}

 \subsection[Contexts]{Introduction of Isabelle Contexts}

 \begin{frame}

   \frametitle{Introduction of Isabelle Contexts}

     \begin{itemize}

     \item theories too general

     \item not capable of type inference

     \item replace function \texttt{parseNEW}

     \item assumptions \& environment $\rightarrow$ context

     \end{itemize}

 \end{frame}

 \begin{frame}

   \frametitle{Code Snippets: \texttt{parse}}

     \texttt{\tiny{

       \begin{tabbing}

 xx\=xx\=xx\=xx\=\kill

 fun parse thy str =\\

 \>(let val t = (typ\_a2real o numbers\_to\_string)\\

 \>\>\>\>(Syntax.read\_term\_global thy str)\\

 \>\>in SOME (cterm\_of thy t) end)\\

 \>\>\>handle \_ => NONE;

 \\~\\~\\

 fun parseNEW ctxt str = SOME (Syntax.read\_term ctxt str |> numbers\_to\_string)\\

 \>\>\>handle \_ => NONE;

       \end{tabbing}

     }}

 \end{frame}

 \begin{frame}

   \frametitle{Code Snippets: context data}

     \texttt{\tiny{

       \begin{tabbing}

 xx\=xx\=xx\=xx\=\kill

 datatype Isac\_Ctxt =\\

 \>\>Env of term * term\\

 \>| Asm of term;\\

 \\

 structure ContextData = Proof\_Data\\

 \>~(type T = Isac\_Ctxt list\\

 \>\>fun init \_ = []);\\

 \\

 local\\

 \>fun insert\_ctxt data = ContextData.map (fn xs => distinct (data@xs));\\

 in\\

 \>fun insert\_assumptions asms = map (fn t => Asm t) asms |> insert\_ctxt;\\

 \>fun insert\_environments envs = map (fn t => Env t) envs |> insert\_ctxt;\\

 end\\

 \\

 local\\

 \>fun unpack\_asms (Asm t::ts) = t::(unpack\_asms ts)\\

 \>\>| unpack\_asms (Env \_::ts) = unpack\_asms ts\\

 \>\>| unpack\_asms [] = [];\\

 \>fun unpack\_envs (Env t::ts) = t::(unpack\_envs ts)\\

 \>\>| unpack\_envs (Asm \_::ts) = unpack\_envs ts\\

 \>\>| unpack\_envs [] = [];\\

 in\\

 \>fun get\_assumptions ctxt = ContextData.get ctxt |> unpack\_asms;\\

 \>fun get\_environments ctxt = ContextData.get ctxt |> unpack\_envs;\\

 end

       \end{tabbing}

     }}

 \end{frame}

 \subsection[Redesign]{Redesign of Type Inference in \isac}

 \begin{frame}

   \frametitle{Redesign of Type Inference in \isac}

     \begin{itemize}

     \item use context type inference

     \item parsing input (specification \& user input)

     \item specification with polymorphic types

     \item etc.

     \end{itemize}

 \end{frame}

 \begin{frame}

   \frametitle{Lines of Code}

     \begin{tabular}{lr}

       src/ & 1700 k \\

       src/Pure/ & 70 k \\

       src/Provers/ & 8 k \\

       src/Tools/ & 800 k \\

       src/isac/ & 37 k \\

       src/isac/Knowledge & 16 k \\

     \end{tabular}

 \end{frame}

 \subsection[Code Improvement]{Improvement of functional code}

 \begin{frame}

   \frametitle{Improvement of functional code}

   \begin{itemize}

   \item combinators

   \item code conventions

   \end{itemize}

 \end{frame}

 \begin{frame}

   \frametitle{Combinators \& Code Conventions}

     \texttt{\tiny{

       \begin{tabbing}

 xx\=xx\=xx\=xx\=xx\=\kill

 fun prep\_ori [] \_ \_ = ([], e\_ctxt)\\

 \>| prep\_ori fmz thy pbt =\\

 \>\>\>let\\

 \>\>\>\>val ctxt = ProofContext.init\_global thy |> fold declare\_constraints fmz\\

 \>\>\>\>val ori = map (add\_field thy pbt o split\_dts o the o parseNEW ctxt) fmz\\

 \>\>\>\>\>|> add\_variants\\

 \>\>\>\>val maxv = map fst ori |> max\\

 \>\>\>\>val maxv = if maxv = 0 then 1 else maxv\\

 \>\>\>\>val oris = coll\_variants ori\\

 \>\>\>\>\>|> map (replace\_0 maxv |> apfst)\\

 \>\>\>\>\>|> add\_id\\

 \>\>\>\>\>|> map flattup\\

 \>\>\>in (oris, ctxt) end;

       \end{tabbing}

     }}

 \end{frame}

 \begin{frame}

   \frametitle{Drop \tt{Check\_Elementwise}!}

 \small{

 %\begin{onehalfspace}

 \begin{tabbing}

 xxx\=xxx\=\kill

 $\mathit{solve}\;(\frac{x}{x ^ 2 - 6 * x + 9} - \frac{1}{x ^ 2 - 3 * x} = \frac{1}{x}, x)$\\ \\

 \>$\frac{x}{x ^ 2 - 6 * x + 9} - \frac{1}{x ^ 2 - 3 * x} = \frac{1}{x}$ \\ \\

 \>$\frac{x}{x ^ 2 + -1 * (6 * x) + 9} + \frac{-1 * 1}{x ^ 2 + -1 * (3 * x)} = \frac{1}{x}$ \\ \\

 %\>$\frac{3 + -1 * x + x ^ 2}{9 * x + -6 * x ^ 2 + x ^ 3} = \frac{1}{x}$ \\ \\

 \>$(3 + -1 * x + x ^ 2) * x = 1 * (9 * x + -6 * x ^ 2 + x ^ 3)$ \\

 \>$\mathit{solve}\;((3 + -1 * x + x ^ 2) * x = 1 * (9 * x + -6 * x ^ 2 + x ^ 3), x)$ \\

 \>\>$(3 + -1 * x + x ^ 2) * x = 1 * (9 * x + -6 * x ^ 2 + x ^ 3)$ \\

 %\>\>$(3 + -1 * x + x ^ 2) * x - 1 * (9 * x + -6 * x ^ 2 + x ^ 3) = 0$ \\

 \>\>$(3 + -1 * x + x ^ 2) * x - (9 * x + -6 * x ^ 2 + x ^ 3) = 0$ \\

 \>\>$-6 * x + 5 * x ^ 2 = 0$ \\

 \>\>$\mathit{solve}\;(-6 * x + 5 * x ^ 2 = 0, x)$ \\

 \>\>$[x = 0, x = \frac{6}{5}]$ \\

 \>$[x = 0, x = \frac{6}{5}]$ \\

                                           \`\alert{$\mathit{Check\_Elementwise}\;\mathit{Assumptions}$}\\

 \>$[x = \frac{6}{5}]$ \\

 $[x = \frac{6}{5}]$

 \end{tabbing}

 }

 %\end{onehalfspace}

 \end{frame}

 \subsection[Future Development]{Preparation of Future Development}

 \begin{frame}

   \frametitle{Preparation of Future Development}

     \begin{itemize}

     \item logical data for Isabelle provers in contexts

     \item \isac programming language more compact\\

       $\rightarrow$ context built automatically

     \end{itemize}

 \end{frame}

 \begin{frame}

   \frametitle{jedit demonstration}

   DEMO

 \end{frame}

 \section[Problems]{Problems encountered in the project}

 \begin{frame}

   \frametitle{Problems encountered in the project}

     \begin{itemize}

     \item publication of new Isabelle release

     \item amount of code in Isabelle and \isac

     \item changes scattered throughout the code ($\rightarrow$ grep)

     \end{itemize}

 \end{frame}

 \section{Summary}

 \begin{frame}

   \frametitle{Summary}

 TODO

 \end{frame}

 \end{document}