1.1 --- a/doc-src/isac/mlehnfeld/presentation.tex Fri May 27 18:00:42 2011 +0200
1.2 +++ b/doc-src/isac/mlehnfeld/presentation.tex Sat May 28 02:55:36 2011 +0200
1.3 @@ -53,20 +53,16 @@
1.4
1.5 \subtitle{Projektpraktikum: Introducing Isabelle's Contexts}
1.6
1.7 -\author[Lehnfeld, Neuper] % (optional, use only with lots of authors)
1.8 -{Mathias~Lehnfeld\inst{1} \and Walther~Neuper\inst{2}}
1.9 +\author[Lehnfeld] % (optional, use only with lots of authors)
1.10 +{Mathias~Lehnfeld}
1.11 % - Give the names in the same order as the appear in the paper.
1.12 % - Use the \inst{?} command only if the authors have different
1.13 % affiliation.
1.14
1.15 \institute % (optional, but mostly needed)
1.16 {
1.17 - \inst{1}%
1.18 - Vienna University of Technology
1.19 - \and
1.20 - \inst{2}%
1.21 - Institute of Software Technology\\
1.22 - Graz University of Technology
1.23 + Vienna University of Technology\\
1.24 + Institute of Computer Languages
1.25 }
1.26 % - Use the \inst command only if there are several affiliations.
1.27 % - Keep it simple, no one is interested in your street address.
1.28 @@ -138,51 +134,100 @@
1.29 % just say so once. Everybody will be happy with that.
1.30
1.31 \section[Introduction]{Introduction}
1.32 -\subsection[TODO]{Isabelle and \isac}
1.33 +\subsection[Isabelle \& \isac]{Isabelle and \isac}
1.34 \begin{frame}
1.35 \frametitle{Isabelle and \isac}
1.36 -TODO
1.37 + \begin{itemize}
1.38 + \item Computer Theorem Prover Isabelle
1.39 + \item Math Learning Assistent \isac
1.40 + \end{itemize}
1.41 \end{frame}
1.42
1.43 -\subsection[TODO]{Computation and deduction in a Lucas-Interpreter}
1.44 +\subsection[Computation \& Deduction]{Computation and Deduction in a Lucas-Interpreter}
1.45 \begin{frame}
1.46 - \frametitle{Computation and deduction in a Lucas-Interpreter}
1.47 -TODO
1.48 + \frametitle{Computation and Deduction in a Lucas-Interpreter}
1.49 + \includegraphics[width=100mm]{overview.pdf}
1.50 \end{frame}
1.51
1.52 \section[Contributions]{Contributions of the project}
1.53 -\subsection[TODO]{Introduction of Isabelle Contexts}
1.54 +\subsection[Contexts]{Introduction of Isabelle Contexts}
1.55 \begin{frame}
1.56 - \frametitle{TODO}
1.57 -TODO
1.58 + \frametitle{Introduction of Isabelle Contexts}
1.59 + \begin{itemize}
1.60 + \item theories too general
1.61 + \item not capable of type inference
1.62 + \item replace function \texttt{parseNEW}
1.63 + \end{itemize}
1.64 \end{frame}
1.65
1.66 -\subsection[TODO]{Redesign of type inference in \isac}
1.67 \begin{frame}
1.68 - \frametitle{TODO}
1.69 -TODO
1.70 + \frametitle{Introduction of Isabelle Contexts}
1.71 + \texttt{\tiny{
1.72 + \begin{tabbing}
1.73 +xx\=xx\=xx\=xx\=\kill
1.74 +fun parse thy str =\\
1.75 +\>(let val t = (typ\_a2real o numbers\_to\_string)\\
1.76 +\>\>\>\>(Syntax.read\_term\_global thy str)\\
1.77 +\>\>in SOME (cterm\_of thy t) end)\\
1.78 +\>\>\>handle \_ => NONE;
1.79 +\\~\\~\\
1.80 +fun parseNEW ctxt str = SOME (Syntax.read\_term ctxt str |> numbers\_to\_string)\\
1.81 +\>\>\>handle \_ => NONE;
1.82 +\\~\\~\\
1.83 +local\\
1.84 +\>fun insert\_ctxt data = ContextData.map (fn xs => distinct (data@xs));\\
1.85 +in\\
1.86 +\>fun insert\_assumptions asms = map (fn t => Asm t) asms |> insert\_ctxt;\\
1.87 +\>fun insert\_environments envs = map (fn t => Env t) envs |> insert\_ctxt;\\
1.88 +end
1.89 + \end{tabbing}
1.90 + }}
1.91 \end{frame}
1.92
1.93 -\subsection[TODO]{Improvement of functional code}
1.94 +\subsection[Redesign]{Redesign of Type Inference in \isac}
1.95 \begin{frame}
1.96 - \frametitle{Drop \textit{Check\_Elementwise} !}
1.97 -%\begin{verbatim}
1.98 -%solve (x / (x ^ 2 - 6 * x + 9) - 1 / (x ^ 2 - 3 * x) = 1 / x, x)
1.99 -% x / (x ^ 2 - 6 * x + 9) - 1 / (x ^ 2 - 3 * x) = 1 / x
1.100 -% x / (x ^ 2 + -1 * (6 * x) + 9) + -1 * 1 / (x ^ 2 + -1 * (3 * x)) = 1 / x
1.101 -% (3 + -1 * x + x ^ 2) / (9 * x + -6 * x ^ 2 + x ^ 3) = 1 / x
1.102 -% (3 + -1 * x + x ^ 2) * x = 1 * (9 * x + -6 * x ^ 2 + x ^ 3)
1.103 -% solve ((3 + -1 * x + x ^ 2) * x = 1 * (9 * x + -6 * x ^ 2 + x ^ 3), x)
1.104 -% (3 + -1 * x + x ^ 2) * x = 1 * (9 * x + -6 * x ^ 2 + x ^ 3)
1.105 -% (3 + -1 * x + x ^ 2) * x - 1 * (9 * x + -6 * x ^ 2 + x ^ 3) = 0
1.106 -% (3 + -1 * x + x ^ 2) * x - (9 * x + -6 * x ^ 2 + x ^ 3) = 0
1.107 -% -6 * x + 5 * x ^ 2 = 0
1.108 -% solve (-6 * x + 5 * x ^ 2 = 0, x)
1.109 -% [x = 0, x = 6 / 5]
1.110 -% [x = 0, x = 6 / 5]
1.111 -% [x = 6 / 5]
1.112 -%[x = 6 / 5]
1.113 -%\end{verbatim}
1.114 + \frametitle{Redesign of type inference in \isac}
1.115 + \begin{itemize}
1.116 + \item use context type inference
1.117 + \item parsing input (specification \& user input)
1.118 + \item specification with polymorphic types
1.119 + \item etc.
1.120 + \end{itemize}
1.121 +\end{frame}
1.122 +
1.123 +\subsection[Code Improvement]{Improvement of functional code}
1.124 +\begin{frame}
1.125 + \frametitle{Improvement of functional code}
1.126 + \begin{itemize}
1.127 + \item combinators
1.128 + \item code conventions
1.129 + \end{itemize}
1.130 +\end{frame}
1.131 +
1.132 +\begin{frame}
1.133 + \frametitle{Combinators \& Code Conventions}
1.134 + \texttt{\tiny{
1.135 + \begin{tabbing}
1.136 +xx\=xx\=xx\=xx\=xx\=\kill
1.137 +fun prep\_ori [] \_ \_ = ([], e\_ctxt)\\
1.138 +\>| prep\_ori fmz thy pbt =\\
1.139 +\>\>\>let\\
1.140 +\>\>\>\>val ctxt = ProofContext.init\_global thy |> fold declare\_constraints fmz\\
1.141 +\>\>\>\>val ori = map (add\_field thy pbt o split\_dts o the o parseNEW ctxt) fmz\\
1.142 +\>\>\>\>\>|> add\_variants\\
1.143 +\>\>\>\>val maxv = map fst ori |> max\\
1.144 +\>\>\>\>val maxv = if maxv = 0 then 1 else maxv\\
1.145 +\>\>\>\>val oris = coll\_variants ori\\
1.146 +\>\>\>\>\>|> map (replace\_0 maxv |> apfst)\\
1.147 +\>\>\>\>\>|> add\_id\\
1.148 +\>\>\>\>\>|> map flattup\\
1.149 +\>\>\>in (oris, ctxt) end;
1.150 + \end{tabbing}
1.151 + }}
1.152 +\end{frame}
1.153 +
1.154 +\begin{frame}
1.155 + \frametitle{Drop \tt{Check\_Elementwise}!}
1.156
1.157 \small{
1.158 %\begin{onehalfspace}
1.159 @@ -210,26 +255,29 @@
1.160
1.161 \end{frame}
1.162
1.163 -\subsection[TODO]{Preparation of future development}
1.164 +\subsection[Future Development]{Preparation of Future Development}
1.165 \begin{frame}
1.166 - \frametitle{TODO}
1.167 -TODO
1.168 + \frametitle{Preparation of Future Development}
1.169 + \begin{itemize}
1.170 + \item logical data for Isabelle provers in contexts
1.171 + \item \isac programming language more compact\\
1.172 + $\rightarrow$ context built automatically
1.173 + \end{itemize}
1.174 \end{frame}
1.175
1.176 \section[Problems]{Problems encountered in the project}
1.177 -%\subsection[TODO]{TODO}
1.178 \begin{frame}
1.179 - \frametitle{TODO}
1.180 -\begin{itemize}
1.181 -\item Publication of new Isabelle release
1.182 -\item Amount of code in Isabelle and \isac
1.183 -\item Changes scattered throughout the code
1.184 -\end{itemize}
1.185 + \frametitle{Problems encountered in the project}
1.186 + \begin{itemize}
1.187 + \item publication of new Isabelle release
1.188 + \item amount of code in Isabelle and \isac
1.189 + \item changes scattered throughout the code
1.190 + \end{itemize}
1.191 \end{frame}
1.192
1.193 \section{Summary}
1.194 \begin{frame}
1.195 - \frametitle{TODO}
1.196 + \frametitle{Summary}
1.197 TODO
1.198 \end{frame}
1.199