\section[Introduction]{Introduction}

 \section[Introduction]{Introduction: Isabelle and \isac}

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

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

     \begin{itemize}

 The task of this ``Projektpraktikum'' (6 ECTS) was to

     \item Computer Theorem Prover Isabelle

 \begin{itemize}

     \item Math Learning Assistent \isac

 \item study the concept of ``context'' in the theorem prover \textbf{Isabelle} from TU Munich

     \end{itemize}

 \item study basic concepts of the math assistant \sisac{} from TU Graz

 \end{frame}

 \pause

 \item redesign \sisac{} with respect to contexts

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

   \begin{itemize}

   \item use contexts for type inference of user input

   \item handle preconditions of specifications

   \item clarify the transfer of context data from sub-programs to the calling program

   \end{itemize}

 \pause

 \item introduce contexts to \sisac{} according to the new design

 \item use the coding standards of Isabelle2011 for new code.

 \end{itemize}

 \end{frame}

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

 \section[Contributions]{Contributions of the project}

 \section[Contributions]{Contributions of the project to \isac}

 \subsection[Contexts]{Introduction of Isabelle Contexts}

 \subsection[Contexts]{Isabelle's Contexts, advantages and use}

 \begin{frame}

 \begin{frame}

   \frametitle{Introduction of Isabelle Contexts}

   \frametitle{Advantages of Isabelle's Contexts}

     \begin{itemize}

 Isabelle's context replaced theories because \dots:

     \item theories too general

 \begin{itemize}

     \item not capable of type inference

 \item theories are static containers of \textit{all} logical data

     \item replace function \texttt{parseNEW}

 \item contexts are \textit{dynamic} containers of logical data:

     \item assumptions \& environment $\rightarrow$ context

   \begin{itemize}

     \end{itemize}

   \item functions for storing and retrieving various logical data

 \end{frame}

   \item functions for type inference

   \item provide data for Isabelle's automated provers

 \begin{frame}

   \end{itemize}

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

 %\item e.g. theories have no direct functions for type inference

     \texttt{\tiny{

 %\item replace function \texttt{parseNEW}

 %\item assumptions \& environment $\rightarrow$ context

 \item allow to conform with scopes for subprograms.

 \end{itemize}

 \end{frame}

 \begin{frame}

   \frametitle{Isabelle's context mechanism}

     \texttt{\small{

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

 xx\=xx\=in\=\kill

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

 %datatype Isac\_Ctxt =\\

 %\>\>Env of term * term\\

 %\>| Asm of term;\\

 %\\

 structure ContextData =  \alert{Proof\_Data}\\

 \>~(\alert{type T} = term list\\

 \>\>\alert{fun init \_} = []);\\

 \\

 %local\\

 %\>fun insert\_ctxt data = ContextData\alert{.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\\

 fun insert\_assumptions asms = \\

 \>\>\>ContextData\alert{.map} (fn xs => distinct (data@xs));\\

 \\

 %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

 fun get\_assumptions ctxt = ContextData\alert{.get} ctxt;\\

 \\

 \\

 val declare\_constraints : \\

 \>\>\>term -> Proof.context -> Proof.context

       \end{tabbing}

     }}

 \end{frame}

 \begin{frame}

   \frametitle{Usage of Contexts}

     \texttt{\footnotesize{

       \begin{tabbing}

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

 fun transfer\_asms\_from\_to from\_ctxt to\_ctxt =\\

 \>  let\\

 \>\>    val to\_vars = get\_assumptions to\_ctxt |> map vars |> flat\\

 \>\>    fun transfer [] to\_ctxt = to\_ctxt\\

 \>\>\>      | transfer (from\_asm::fas) to\_ctxt =\\

 \>\>\>\>\>          if inter op = (vars from\_asm) to\_vars = []\\

 \>\>\>\>\>         then transfer fas to\_ctxt\\

 \>\>\>\>\>          else transfer fas (insert\_assumptions [from\_asm] to\_ctxt)\\

 \>  in transfer (get\_assumptions from\_ctxt) to\_ctxt end\\

 \\

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

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

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

 \>\>\>\>(\alert{Syntax.read\_term\_global thy} str)\\

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

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

 \\~\\~\\

 \\

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

 fun parseNEW ctxt str = \\

 \>\>\>SOME (\alert{Syntax.read\_term ctxt} str |> numbers\_to\_string)\\

 \end{frame}

 \end{frame}

 \begin{frame}

   \frametitle{Code Snippets: context data}

 \subsection[Redesign]{Redesign of \isac{} using contexts}

     \texttt{\tiny{

 \begin{frame}

       \begin{tabbing}

   \frametitle{Redesign of \isac{} using contexts}

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

 \begin{center} DEMO \end{center}

 datatype Isac\_Ctxt =\\

 \end{frame}

 \>\>Env of term * term\\

 \>| Asm of term;\\

 \begin{frame}

 \\

   \frametitle{Deduction simplifies computation}

 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/Tools/isac/ & 37 k \\

       src/Tools/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}!}

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

      \`$\mathit{(some)}\;\mathit{assumptions}$\\

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

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

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

 %     \`$x ^ 2 - 6 * x + 9\not=0\land x ^ 2 - 3 * x\not=0$\\

 %\>$\frac{3 + -1 * x + x ^ 2}{9 * x + -6 * x ^ 2 + x ^ 3} = \frac{1}{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}$ \\ 

      \`$x\not=3\land x\not=0$\\

 \>\>$(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)$ \\

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

      \`$x = 0\land x = \frac{6}{5}$\\

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

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

      \`\alert{$\mathit{Check\_Elementwise}\;\mathit{Assumptions}:x\not=0\land x = 0$}\\

 \end{frame}

 \end{frame}

 \begin{frame}

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

   \frametitle{More ``deduction'', \\less ``computation''}

 \begin{frame}

 \footnotesize{\tt

   \frametitle{Preparation of Future Development}

 \begin{tabbing}

     \begin{itemize}

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

     \item logical data for Isabelle provers in contexts

 Script Solve\_root\_equation (e\_e::bool) (v\_v::real) =      \\

     \item \isac{} programming language more compact\\

 \> (let e\_e = ((Try (Rewrite\_Set norm\_equation False)) \@\@   \\

       $\rightarrow$ context built automatically

 \>\>\>            (Try (Rewrite\_Set Test\_simplify False))) e\_e; \\

     \end{itemize}

 \>\>     (L\_L::bool list) =                                   \\

 \end{frame}

 \>\>\>            (SubProblem (Test',                           \\

 \>\>\>\>                         [linear,univariate,equation,test]\\

 \begin{frame}

 \>\>\>\>                         [Test,solve\_linear])             \\

   \frametitle{jedit demonstration}

 \>\>\>\>                        [BOOL e\_e, REAL v\_v])             \\

   DEMO

 \>  in \alert{Check\_elementwise L\_L \{(v\_v::real). Assumptions\}})\\      

 \end{frame}

 \end{tabbing}

 }

 \small{

 ``Deductive'' part of Lucas-Interpretation relives the ``computational'' part: \alert{one statement becomes obsolete~!}

 }

 \end{frame}

 \begin{frame}

   \frametitle{Redesign of \isac{} using contexts}

 Advantages of the redesign:

 \begin{itemize}

 \item type inference by \textit{local} contexts\\

 \pause

      \alert{now user-input without type constraints~!}

 \pause

 \item consistent handling of logical data

   \begin{itemize}

   \item preconditions and partiality conditions in contexts

   \item transfer of context data into subprograms clarified

   \item transfer of context data from subprograms clarified

   \end{itemize}

 \pause

      \alert{now some statements become obsolete.}\\

 \end{itemize}

 \pause

 Now Lucas-interpretation shifts efforts from ``computation'' further to ``deduction''.

 \end{frame}

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

 \begin{frame}

   \frametitle{Improvement of functional code}

   \begin{itemize}

   \item \textbf{code conventions}: Isabelle2011 published coding standards first time

   \item \textbf{combinators}: Isabelle2011 introduced a library containing the following combinators:

 \\\vspace{0.2cm}

 \tiny{\tt%

   val |$>$ : 'a * ('a -$>$ 'b) -$>$ 'b\\

   val |-$>$ : ('c * 'a) * ('c -$>$ 'a -$>$ 'b) -$>$ 'b\\

   val |$>>$ : ('a * 'c) * ('a -$>$ 'b) -$>$ 'b * 'c\\

   val ||$>$ : ('c * 'a) * ('a -$>$ 'b) -$>$ 'c * 'b\\

   val ||$>>$ : ('c * 'a) * ('a -$>$ 'd * 'b) -$>$ ('c * 'd) * 'b\\

   val \#$>$ : ('a -$>$ 'b) * ('b -$>$ 'c) -$>$ 'a -$>$ 'c\\

   val \#-$>$ : ('a -$>$ 'c * 'b) * ('c -$>$ 'b -$>$ 'd) -$>$ 'a -$>$ 'd\\

   val \#$>>$ : ('a -$>$ 'c * 'b) * ('c -$>$ 'd) -$>$ 'a -$>$ 'd * 'b\\

   val \#\#$>$ : ('a -$>$ 'c * 'b) * ('b -$>$ 'd) -$>$ 'a -$>$ 'c * 'd\\

   val \#\#$>>$ : ('a -$>$ 'c * 'b) * ('b -$>$ 'e * 'd) -$>$ 'a -$>$ ('c * 'e) * 'd\\

 }

   \end{itemize}

 \end{frame}

 \begin{frame}

   \frametitle{Example with combinators}

     \texttt{\footnotesize{

       \begin{tabbing}

 xx\=xx\=xx\=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}

     }}

 \dots which probably can be further polished.

 \end{frame}

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

 %\begin{frame}

 %  \frametitle{Preparation of Future Development}

 %

 %%  "Script Solve_root_equation (e_e::bool) (v_v::real) =       " ^

 %%  " (let e_e = ((Try (Rewrite_Set norm_equation False)) @@    " ^

 %%  "            (Try (Rewrite_Set Test_simplify False))) e_e;  " ^

 %%  "     (L_L::bool list) =                                    " ^

 %%  "            (SubProblem (Test',                            " ^

 %%  "                         [linear,univariate,equation,test]," ^

 %%  "                         [Test,solve_linear])              " ^

 %%  "                        [BOOL e_e, REAL v_v])              " ^

 %%  "  in Check_elementwise L_L {(v_v::real). Assumptions})     "

 %\end{frame}

 %

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

     \item publication of new Isabelle release

     \item new Isabelle release in February 2011: update \sisac{} first

     \item amount of code in Isabelle and \isac

 \pause

     \item lines of code (LOC) in Isabelle and \sisac{}\\ \vspace{0.2cm}

 \textit{

     \begin{tabular}{lrl}

       src/ & 1700 & $\,$k LOC\\

       src/Pure/ & 70 & k LOC\\

       src/Provers/ & 8 & k LOC\\

       src/Tools/ & 800 & k LOC\\

       src/Tools/isac/ & 37 & k LOC\\

       src/Tools/isac/Knowledge & 16 & k LOC

     \end{tabular}

 }

 \pause

 TODO

 The project succeeded in all goals:

 \begin{itemize}

 \item implemented Isabelle's contexts in \sisac{} such that

 \item user input requires no type constraints anymore

 \item consistent logical data is prepared for Isabelle's provers

 \end{itemize}

 \pause

 The course of the project was close to the plan:

 \begin{itemize}

 \item faster in writing new code

 \item slower in integrating the code into \sisac

 \end{itemize}

 \pause

 The project provided essential prerequisites for further development of the Lucas-interpreter.