e0726734@42027: % $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 $
e0726734@42027: 
e0726734@42027: \documentclass{beamer}
e0726734@42027: 
e0726734@42027: % This file is a solution template for:
e0726734@42027: 
e0726734@42027: % - Talk at a conference/colloquium.
e0726734@42027: % - Talk length is about 20min.
e0726734@42027: % - Style is ornate.
e0726734@42027: 
e0726734@42027: 
e0726734@42027: 
e0726734@42027: % Copyright 2004 by Till Tantau <tantau@users.sourceforge.net>.
e0726734@42027: %
e0726734@42027: % In principle, this file can be redistributed and/or modified under
e0726734@42027: % the terms of the GNU Public License, version 2.
e0726734@42027: %
e0726734@42027: % However, this file is supposed to be a template to be modified
e0726734@42027: % for your own needs. For this reason, if you use this file as a
e0726734@42027: % template and not specifically distribute it as part of a another
e0726734@42027: % package/program, I grant the extra permission to freely copy and
e0726734@42027: % modify this file as you see fit and even to delete this copyright
e0726734@42027: % notice.
e0726734@42027: 
e0726734@42027: 
e0726734@42027: \mode<presentation>
e0726734@42027: {
e0726734@42027:   \usetheme{Hannover}
e0726734@42027:   % or ...
e0726734@42027: 
e0726734@42027:   \setbeamercovered{transparent}
e0726734@42027:   % or whatever (possibly just delete it)
e0726734@42027: }
e0726734@42027: 
neuper@42029: %\usepackage{setspace} %for "\begin{onehalfspace}"
e0726734@42027: \usepackage[english]{babel}
e0726734@42027: % or whatever
e0726734@42027: 
e0726734@42027: \usepackage[utf8]{inputenc}
e0726734@42027: % or whatever
e0726734@42027: 
e0726734@42027: \usepackage{times}
e0726734@42027: \usepackage[T1]{fontenc}
e0726734@42027: % Or whatever. Note that the encoding and the font should match. If T1
e0726734@42027: % does not look nice, try deleting the line with the fontenc.
e0726734@42027: 
e0726734@42027: \def\isac{${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$}
e0726734@42027: \def\sisac{{\footnotesize${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$}}
e0726734@42027: 
e0726734@42027: \title[\isac: Computation \& Deduction] % (optional, use only with long paper titles)
e0726734@42027: {Integrating Computation and Deduction\\
e0726734@42027:   in the \isac-System}
e0726734@42027: 
e0726734@42027: \subtitle{Projektpraktikum: Introducing Isabelle's Contexts}
e0726734@42027: 
e0726734@42030: \author[Lehnfeld] % (optional, use only with lots of authors)
e0726734@42030: {Mathias~Lehnfeld}
e0726734@42027: % - Give the names in the same order as the appear in the paper.
e0726734@42027: % - Use the \inst{?} command only if the authors have different
e0726734@42027: %   affiliation.
e0726734@42027: 
e0726734@42027: \institute % (optional, but mostly needed)
e0726734@42027: {
e0726734@42030:   Vienna University of Technology\\
e0726734@42030:   Institute of Computer Languages
e0726734@42027: }
e0726734@42027: % - Use the \inst command only if there are several affiliations.
e0726734@42027: % - Keep it simple, no one is interested in your street address.
e0726734@42027: 
e0726734@42027: % \date[CFP 2003] % (optional, should be abbreviation of conference name)
e0726734@42027: % {Conference on Fabulous Presentations, 2003}
e0726734@42027: % - Either use conference name or its abbreviation.
e0726734@42027: % - Not really informative to the audience, more for people (including
e0726734@42027: %   yourself) who are reading the slides online
e0726734@42027: 
e0726734@42027: % \subject{Theoretical Computer Science}
e0726734@42027: % This is only inserted into the PDF information catalog. Can be left
e0726734@42027: % out.
e0726734@42027: 
e0726734@42027: 
e0726734@42027: 
e0726734@42027: % If you have a file called "university-logo-filename.xxx", where xxx
e0726734@42027: % is a graphic format that can be processed by latex or pdflatex,
e0726734@42027: % resp., then you can add a logo as follows:
e0726734@42027: 
e0726734@42027: % \pgfdeclareimage[height=0.5cm]{university-logo}{university-logo-filename}
e0726734@42027: % \logo{\pgfuseimage{university-logo}}
e0726734@42027: 
e0726734@42027: 
e0726734@42027: 
e0726734@42027: % Delete this, if you do not want the table of contents to pop up at
e0726734@42027: % the beginning of each subsection:
e0726734@42027: \AtBeginSubsection[]
e0726734@42027: {
e0726734@42027:   \begin{frame}<beamer>{Outline}
e0726734@42027:     \tableofcontents[currentsection,currentsubsection]
e0726734@42027:   \end{frame}
e0726734@42027: }
e0726734@42027: 
e0726734@42027: 
e0726734@42027: % If you wish to uncover everything in a step-wise fashion, uncomment
e0726734@42027: % the following command:
e0726734@42027: 
e0726734@42027: %\beamerdefaultoverlayspecification{<+->}
e0726734@42027: 
e0726734@42027: 
e0726734@42027: \begin{document}
e0726734@42027: 
e0726734@42027: \begin{frame}
e0726734@42027:   \titlepage
e0726734@42027: \end{frame}
e0726734@42027: 
e0726734@42027: \begin{frame}{Outline}
e0726734@42027:   \tableofcontents
e0726734@42027:   % You might wish to add the option [pausesections]
e0726734@42027: \end{frame}
e0726734@42027: 
e0726734@42027: 
e0726734@42027: % Structuring a talk is a difficult task and the following structure
e0726734@42027: % may not be suitable. Here are some rules that apply for this
e0726734@42027: % solution:
e0726734@42027: 
e0726734@42027: % - Exactly two or three sections (other than the summary).
e0726734@42027: % - At *most* three subsections per section.
e0726734@42027: % - Talk about 30s to 2min per frame. So there should be between about
e0726734@42027: %   15 and 30 frames, all told.
e0726734@42027: 
e0726734@42027: % - A conference audience is likely to know very little of what you
e0726734@42027: %   are going to talk about. So *simplify*!
e0726734@42027: % - In a 20min talk, getting the main ideas across is hard
e0726734@42027: %   enough. Leave out details, even if it means being less precise than
e0726734@42027: %   you think necessary.
e0726734@42027: % - If you omit details that are vital to the proof/implementation,
e0726734@42027: %   just say so once. Everybody will be happy with that.
e0726734@42027: 
neuper@42028: \section[Introduction]{Introduction}
e0726734@42030: \subsection[Isabelle \& \isac]{Isabelle and \isac}
neuper@42028: \begin{frame}
neuper@42028:   \frametitle{Isabelle and \isac}
e0726734@42030:     \begin{itemize}
e0726734@42030:     \item Computer Theorem Prover Isabelle
e0726734@42030:     \item Math Learning Assistent \isac
e0726734@42030:     \end{itemize}
e0726734@42027: \end{frame}
e0726734@42027: 
e0726734@42030: \subsection[Computation \& Deduction]{Computation and Deduction in a Lucas-Interpreter}
neuper@42028: \begin{frame}
e0726734@42030:   \frametitle{Computation and Deduction in a Lucas-Interpreter}
e0726734@42030:     \includegraphics[width=100mm]{overview.pdf}
e0726734@42027: \end{frame}
e0726734@42027: 
neuper@42028: \section[Contributions]{Contributions of the project}
e0726734@42030: \subsection[Contexts]{Introduction of Isabelle Contexts}
neuper@42028: \begin{frame}
e0726734@42030:   \frametitle{Introduction of Isabelle Contexts}
e0726734@42030:     \begin{itemize}
e0726734@42030:     \item theories too general
e0726734@42030:     \item not capable of type inference
e0726734@42030:     \item replace function \texttt{parseNEW}
e0726734@42031:     \item assumptions \& environment $\rightarrow$ context
e0726734@42030:     \end{itemize}
e0726734@42027: \end{frame}
e0726734@42027: 
neuper@42028: \begin{frame}
e0726734@42031:   \frametitle{Code Snippets: \texttt{parse}}
e0726734@42030:     \texttt{\tiny{
e0726734@42030:       \begin{tabbing}
e0726734@42030: xx\=xx\=xx\=xx\=\kill
e0726734@42030: fun parse thy str =\\
e0726734@42030: \>(let val t = (typ\_a2real o numbers\_to\_string)\\
e0726734@42030: \>\>\>\>(Syntax.read\_term\_global thy str)\\
e0726734@42030: \>\>in SOME (cterm\_of thy t) end)\\
e0726734@42030: \>\>\>handle \_ => NONE;
e0726734@42030: \\~\\~\\
e0726734@42030: fun parseNEW ctxt str = SOME (Syntax.read\_term ctxt str |> numbers\_to\_string)\\
e0726734@42030: \>\>\>handle \_ => NONE;
e0726734@42031:       \end{tabbing}
e0726734@42031:     }}
e0726734@42031: \end{frame}
e0726734@42031: 
e0726734@42031: 
e0726734@42031: \begin{frame}
e0726734@42031:   \frametitle{Code Snippets: context data}
e0726734@42031:     \texttt{\tiny{
e0726734@42031:       \begin{tabbing}
e0726734@42031: xx\=xx\=xx\=xx\=\kill
e0726734@42031: datatype Isac\_Ctxt =\\
e0726734@42031: \>\>Env of term * term\\
e0726734@42031: \>| Asm of term;\\
e0726734@42031: \\
e0726734@42031: structure ContextData = Proof\_Data\\
e0726734@42031: \>~(type T = Isac\_Ctxt list\\
e0726734@42031: \>\>fun init \_ = []);\\
e0726734@42031: \\
e0726734@42030: local\\
e0726734@42030: \>fun insert\_ctxt data = ContextData.map (fn xs => distinct (data@xs));\\
e0726734@42030: in\\
e0726734@42030: \>fun insert\_assumptions asms = map (fn t => Asm t) asms |> insert\_ctxt;\\
e0726734@42030: \>fun insert\_environments envs = map (fn t => Env t) envs |> insert\_ctxt;\\
e0726734@42031: end\\
e0726734@42031: \\
e0726734@42031: local\\
e0726734@42031: \>fun unpack\_asms (Asm t::ts) = t::(unpack\_asms ts)\\
e0726734@42031: \>\>| unpack\_asms (Env \_::ts) = unpack\_asms ts\\
e0726734@42031: \>\>| unpack\_asms [] = [];\\
e0726734@42031: \>fun unpack\_envs (Env t::ts) = t::(unpack\_envs ts)\\
e0726734@42031: \>\>| unpack\_envs (Asm \_::ts) = unpack\_envs ts\\
e0726734@42031: \>\>| unpack\_envs [] = [];\\
e0726734@42031: in\\
e0726734@42031: \>fun get\_assumptions ctxt = ContextData.get ctxt |> unpack\_asms;\\
e0726734@42031: \>fun get\_environments ctxt = ContextData.get ctxt |> unpack\_envs;\\
e0726734@42030: end
e0726734@42030:       \end{tabbing}
e0726734@42030:     }}
e0726734@42027: \end{frame}
e0726734@42027: 
e0726734@42030: \subsection[Redesign]{Redesign of Type Inference in \isac}
neuper@42028: \begin{frame}
e0726734@42031:   \frametitle{Redesign of Type Inference in \isac}
e0726734@42030:     \begin{itemize}
e0726734@42030:     \item use context type inference
e0726734@42030:     \item parsing input (specification \& user input)
e0726734@42030:     \item specification with polymorphic types
e0726734@42030:     \item etc.
e0726734@42030:     \end{itemize}
e0726734@42030: \end{frame}
e0726734@42030: 
e0726734@42031: \begin{frame}
e0726734@42031:   \frametitle{Lines of Code}
e0726734@42031:     \begin{tabular}{lr}
e0726734@42031:       src/ & 1700 k \\
e0726734@42031:       src/Pure/ & 70 k \\
e0726734@42031:       src/Provers/ & 8 k \\
e0726734@42031:       src/Tools/ & 800 k \\
e0726734@42031:       src/isac/ & 37 k \\
e0726734@42031:       src/isac/Knowledge & 16 k \\
e0726734@42031:     \end{tabular}
e0726734@42031: \end{frame}
e0726734@42031: 
e0726734@42030: \subsection[Code Improvement]{Improvement of functional code}
e0726734@42030: \begin{frame}
e0726734@42030:   \frametitle{Improvement of functional code}
e0726734@42030:   \begin{itemize}
e0726734@42030:   \item combinators
e0726734@42030:   \item code conventions
e0726734@42030:   \end{itemize}
e0726734@42030: \end{frame}
e0726734@42030: 
e0726734@42030: \begin{frame}
e0726734@42030:   \frametitle{Combinators \& Code Conventions}
e0726734@42030:     \texttt{\tiny{
e0726734@42030:       \begin{tabbing}
e0726734@42030: xx\=xx\=xx\=xx\=xx\=\kill
e0726734@42030: fun prep\_ori [] \_ \_ = ([], e\_ctxt)\\
e0726734@42030: \>| prep\_ori fmz thy pbt =\\
e0726734@42030: \>\>\>let\\
e0726734@42030: \>\>\>\>val ctxt = ProofContext.init\_global thy |> fold declare\_constraints fmz\\
e0726734@42030: \>\>\>\>val ori = map (add\_field thy pbt o split\_dts o the o parseNEW ctxt) fmz\\
e0726734@42030: \>\>\>\>\>|> add\_variants\\
e0726734@42030: \>\>\>\>val maxv = map fst ori |> max\\
e0726734@42030: \>\>\>\>val maxv = if maxv = 0 then 1 else maxv\\
e0726734@42030: \>\>\>\>val oris = coll\_variants ori\\
e0726734@42030: \>\>\>\>\>|> map (replace\_0 maxv |> apfst)\\
e0726734@42030: \>\>\>\>\>|> add\_id\\
e0726734@42030: \>\>\>\>\>|> map flattup\\
e0726734@42030: \>\>\>in (oris, ctxt) end;
e0726734@42030:       \end{tabbing}
e0726734@42030:     }}
e0726734@42030: \end{frame}
e0726734@42030: 
e0726734@42030: \begin{frame}
e0726734@42030:   \frametitle{Drop \tt{Check\_Elementwise}!}
neuper@42029: 
neuper@42029: \small{
neuper@42029: %\begin{onehalfspace}
neuper@42029: \begin{tabbing}
neuper@42029: xxx\=xxx\=\kill
neuper@42029: $\mathit{solve}\;(\frac{x}{x ^ 2 - 6 * x + 9} - \frac{1}{x ^ 2 - 3 * x} = \frac{1}{x}, x)$\\ \\
neuper@42029: \>$\frac{x}{x ^ 2 - 6 * x + 9} - \frac{1}{x ^ 2 - 3 * x} = \frac{1}{x}$ \\ \\
neuper@42029: \>$\frac{x}{x ^ 2 + -1 * (6 * x) + 9} + \frac{-1 * 1}{x ^ 2 + -1 * (3 * x)} = \frac{1}{x}$ \\ \\
neuper@42029: %\>$\frac{3 + -1 * x + x ^ 2}{9 * x + -6 * x ^ 2 + x ^ 3} = \frac{1}{x}$ \\ \\
neuper@42029: \>$(3 + -1 * x + x ^ 2) * x = 1 * (9 * x + -6 * x ^ 2 + x ^ 3)$ \\
neuper@42029: \>$\mathit{solve}\;((3 + -1 * x + x ^ 2) * x = 1 * (9 * x + -6 * x ^ 2 + x ^ 3), x)$ \\
neuper@42029: \>\>$(3 + -1 * x + x ^ 2) * x = 1 * (9 * x + -6 * x ^ 2 + x ^ 3)$ \\
neuper@42029: %\>\>$(3 + -1 * x + x ^ 2) * x - 1 * (9 * x + -6 * x ^ 2 + x ^ 3) = 0$ \\
neuper@42029: \>\>$(3 + -1 * x + x ^ 2) * x - (9 * x + -6 * x ^ 2 + x ^ 3) = 0$ \\
neuper@42029: \>\>$-6 * x + 5 * x ^ 2 = 0$ \\
neuper@42029: \>\>$\mathit{solve}\;(-6 * x + 5 * x ^ 2 = 0, x)$ \\
neuper@42029: \>\>$[x = 0, x = \frac{6}{5}]$ \\
neuper@42029: \>$[x = 0, x = \frac{6}{5}]$ \\
neuper@42029:                                           \`\alert{$\mathit{Check\_Elementwise}\;\mathit{Assumptions}$}\\
neuper@42029: \>$[x = \frac{6}{5}]$ \\
neuper@42029: $[x = \frac{6}{5}]$
neuper@42029: \end{tabbing}
neuper@42029: }
neuper@42029: %\end{onehalfspace}
neuper@42029: 
e0726734@42027: \end{frame}
e0726734@42027: 
e0726734@42030: \subsection[Future Development]{Preparation of Future Development}
neuper@42028: \begin{frame}
e0726734@42030:   \frametitle{Preparation of Future Development}
e0726734@42030:     \begin{itemize}
e0726734@42030:     \item logical data for Isabelle provers in contexts
e0726734@42030:     \item \isac programming language more compact\\
e0726734@42030:       $\rightarrow$ context built automatically
e0726734@42030:     \end{itemize}
e0726734@42027: \end{frame}
e0726734@42027: 
e0726734@42031: \begin{frame}
e0726734@42031:   \frametitle{jedit demonstration}
e0726734@42031:   DEMO
e0726734@42031: \end{frame}
e0726734@42031: 
neuper@42028: \section[Problems]{Problems encountered in the project}
neuper@42028: \begin{frame}
e0726734@42030:   \frametitle{Problems encountered in the project}
e0726734@42030:     \begin{itemize}
e0726734@42030:     \item publication of new Isabelle release
e0726734@42030:     \item amount of code in Isabelle and \isac
e0726734@42031:     \item changes scattered throughout the code ($\rightarrow$ grep)
e0726734@42030:     \end{itemize}
e0726734@42027: \end{frame}
e0726734@42027: 
neuper@42028: \section{Summary}
neuper@42028: \begin{frame}
e0726734@42030:   \frametitle{Summary}
neuper@42028: TODO
e0726734@42027: \end{frame}
e0726734@42027: 
e0726734@42027: \end{document}
e0726734@42027: 
e0726734@42027: