\documentclass[11pt,a4paper,headline,headcount,towside,nocenter]{report}

\usepackage{latexsym} 

%\usepackage{ngerman}

%\grmn@dq@error ...and \dq \string #1 is undefined}

%l.989 ...tch the problem type \\{\tt["squareroot",

%                                                  "univ

\bibliographystyle{alpha}

\def\isac{${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$}

\title{\isac --- Interface for\\

  Developers of Math Knowledge\\[1.0ex]

  and\\[1.0ex]

  Tools for Experiments in\\

  Symbolic Computation\\[1.0ex]}

\author{The \isac-Team\\

  \tt isac-users@ist.tugraz.at\\[1.0ex]}

\date{\today}

\begin{document}

\maketitle

\newpage

\tableofcontents

\newpage

\listoftables

\newpage

\chapter{Einleitung}

\section{``Authoring'' und ``Tutoring''}

{TO DO} Mathematik lernen -- verschiedene Autoren -- Isabelle

Die Grundlage f\"ur \isac{} bildet Isabelle. Dies ist ein ``theorem prover'', der von L. Paulson und T. Nipkow entwickelt wird und Hard- und Software pr\"uft.

\section{Der Inhalt des Dokuments}

\paragraph{TO DO} {Als Anleitung:} Dieses Dokument beschreibt das Kerngebiet (KE) von \isac{}, das Gebiet der mathematics engine (ME) im Kerngebiet und die verschiedenen Funktionen wie das Umschreiben und der Vergleich.

\isac{} und KE wurden in SML geschrieben, die Sprache in Verbindung mit dem Vorg\"anger des Theorem Provers Isabelle entwickelt. So kam es, dass in diesem Dokument die Ebene ASCII als SML Code pr\"asentiert wird. Der Leser wird vermutlich erkennen, dass der \isac{} Benutzer eine vollkommen andere Sichtweise auf eine grafische Benutzeroberfl\"ache bekommt.

Das Dokument ist eigenst\"andig; Basiswissen \"uber SML (für eine Einf\"uhrung siehe \cite{Paulson:91}), Terme und Umschreibung wird vorrausgesetzt.

%The interfaces will be moderately exended during the first phase of development of the mathematics knowledge. The work on the subprojects defined should {\em not} create interfaces of any interest to a user or another author of knowledge except identifiers (of type string) for theorems, rulesets etc.

Hinweis: SML Code, Verzeichnis, Dateien sind {\tt in 'tt' geschrieben}; besonders in {\tt ML>} ist das Kerngebiet schnell.

\paragraph{Versuchen Sie es!}  Ein weiteres Anliegen dieses Textes ist, dem Leser Tipps f\"ur Versuche mit den Anwendungen zu geben.

\section{Gleich am Computer ausprobieren!}\label{get-started}

\paragraph{TO DO screenshot} Bevor Sie mit Ihren Versuchen beginnen, m\"ochten wir Ihnen noch einige Hinweise geben.

\begin{itemize}

 \item System starten

 \item Shell aufmachen und die Datei mat-eng-de.sml \"offnen.

 \item $>$  :  Hinter diesem Zeichen (``Prompt'') stehen jene, die Sie selbst eingeben bzw. mit Copy und Paste aus der Datei kopieren.

 \item Die Eingabe wird mit ``;'' und ``Enter'' abgeschlossen.

 \item Zeilen, die nicht mit Prompt beginnen, werden vom Computer ausgegeben.

\end{itemize}

\part{Experimentelle Ann\"aherung}

\chapter{Terme und Theorien}

Wie bereits erw\"ahnt, geht es um Computer-Mathematik. In den letzten Jahren hat die ``computer science'' grosse Fortschritte darin gemacht, Mathematik auf dem Computer verst\"andlich darzustellen. Dies gilt f\"ur mathematische Formeln, f\"ur die Beschreibung von Problem (behandelt in Abs.\ref{pbl}), f\"ur L\"osungsmethoden (behandelt in Abs.\ref{met}) etc. Wir beginnen mit mathematischen Formeln --- gleich zum Ausprobieren wie in Abs.\ref{get-started} oben vorbereitet.

\section{Von der Formel zum Term}

Um ein Beispiel zu nennen: Die Formel $a+b\cdot 3$ l\"asst sich in lesbarer Form so eingeben:

{\footnotesize\begin{verbatim}

  > "a + b * 3";

  val it = "a + b * 3" : string

\end{verbatim}}

\noindent ``a + b * 3'' ist also ein String (=Zeichenfolge). In dieser Form weiss der Computer nicht, dass z.B. eine Multiplikation {\em vor} einer Addition zu rechnen ist. Isabelle braucht Formeln in einer anderen Form; Diese kann man mit der Funktion ``str2term'' (= string to term) umrechnen:

{\footnotesize\begin{verbatim}

  > str2term "a + b * 3";

  val it =

     Const ("op +", "[RealDef.real, RealDef.real] => RealDef.real") $

           Free ("a", "RealDef.real") $

        (Const ("op *", "[RealDef.real, RealDef.real] => RealDef.real") $ ... $

           ...) : Term.term

\end{verbatim}}

\noindent Jene Form braucht Isabelle intern zum rechnen. Sie heisst Term und ist nicht lesbar, daf\"ur aber speicherbar mit Hilfe von ``val'' (=value) 

{\footnotesize\begin{verbatim}

  > val term = str2term "a + b * 3";

  val term =  

     Const ("op +", "[RealDef.real, RealDef.real] => RealDef.real") $

           Free ("a", "RealDef.real") $

        (Const ("op *", "[RealDef.real, RealDef.real] => RealDef.real") $ ... $

           ...) : Term.term

\end{verbatim}

Der gespeicherte Term kann einer Funktion ``atomty'' \"ubergeben werden, die jenen in einer abstrakten Struktur zeigt:

{\footnotesize\begin{verbatim}

  > atomty term;

  ***

  *** Const (op +, [real, real] => real)

  *** . Free (a, real)

  *** . Const (op *, [real, real] => real)

  *** . . Free (b, real)

  *** . . Free (3, real)

  ***

  val it = () : unit

\end{verbatim}%size

\section{``Theory'' und ``Parsing``}

Die theory gibt an, welcher Ausdruck wo steht. Eine derzeitige theory wird intern als \texttt{thy} gekennzeichnet. Jene theory, die alles Wissen ent\"ahlt ist \isac{}. 

{\footnotesize\begin{verbatim}

  > Isac.thy;

       val it =

          {ProtoPure, CPure, HOL, Set, Typedef, Fun, Product_Type, Lfp, Gfp,

          Sum_Type, Relation, Record, Inductive, Transitive_Closure,

          Wellfounded_Recursion, NatDef, Nat, NatArith, Divides, Power,

          SetInterval, Finite_Set, Equiv, IntDef, Int, Datatype_Universe,

          Datatype, Numeral, Bin, IntArith, Wellfounded_Relations, Recdef, IntDiv,

          IntPower, NatBin, NatSimprocs, Relation_Power, PreList, List, Map,

          Hilbert_Choice, Main, Lubs, PNat, PRat, PReal, RealDef, RealOrd,

          RealInt, RealBin, RealArith0, RealArith, RComplete, RealAbs, RealPow,

          Ring_and_Field, Complex_Numbers, Real, ListG, Tools, Script, Typefix,

          Float, ComplexI, Descript, Atools, Simplify, Poly, Rational, PolyMinus,

          Equation, LinEq, Root, RootEq, RatEq, RootRat, RootRatEq, PolyEq, Vect,

          Calculus, Trig, LogExp, Diff, DiffApp, Integrate, EqSystem, Biegelinie,

          AlgEin, Test, Isac} : Theory.theory

\end{verbatim}

Die, die ein Mal enth\"alt ist groups.thy. Suchen Sie nach '*' unter der Adresse:

http://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/library/HOL/Groups.html

Hier wird Ihnen erkl\"art, wie das Mal vom Computer gelesen wird.

{\footnotesize\begin{verbatim}

  > Group.thy

      fixes f :: "'a => 'a => 'a" (infixl "*" 70)

      assumes assoc [ac_simps]: "a * b * c = a * (b * c)"

\end{verbatim}

Der ''infix`` ist der Operator, der zwischen zwei Argumenten steht. 70 bedeutet, dass Mal eine hohe Priorit\"at hat (bei einem Plus liegt der Wert bei 50 oder 60). 

Parsing entsteht durch einen string und eine theory. Es verwendet Informationen, die in der theory von Isabelle enthalten sind.

{\footnotesize\begin{verbatim}

  > parse;

       val it = fn : Theory.theory -> string -> Thm.cterm Library.option

\end{verbatim}

Dieser term kann wieder in seine einzelnen Teile zerlegt werden.

{\footnotesize\begin{verbatim}

   > val it = (term_of o the) it;

        val it =

           Const ("op +", "[RealDef.real, RealDef.real] => RealDef.real") $

               Free ("a", "RealDef.real") $

           (Const ("op *", "[RealDef.real, RealDef.real] => RealDef.real") $ ... $

               ...) : Term.term

\end{verbatim}

\paragraph{Versuchen Sie es!} Das mathematische Wissen w\"achst, indem man zu den Urspr\"ungen schaut. In den folgenden Beispielen werden verschiedene Meldungen genauer erkl\"art.

{\footnotesize\begin{verbatim}

   > (*-1-*);

   > parse HOL.thy "2^^^3";

      *** Inner lexical error at: "^^^3"

      val it = None : Thm.cterm Library.option         

\end{verbatim}

''Inner lexical error`` bedeutet, dass ein Fehler aufgetreten ist, vermutlich hat man sich vertippt.

{\footnotesize\begin{verbatim}

   > (*-2-*);

   > parse HOL.thy "d_d x (a + x)";

      val it = None : Thm.cterm Library.option               

\end{verbatim}

Fehlt ''Inner lexical error`` wurde der Parse nicht gefunden.

{\footnotesize\begin{verbatim}

   > (*-3-*);

   > parse Rational.thy "2^^^3";

      val it = Some "2 ^^^ 3" : Thm.cterm Library.option               

\end{verbatim}

{\footnotesize\begin{verbatim}

   > (*-4-*);

   > val Some t4 = parse Rational.thy "d_d x (a + x)";

      val t4 = "d_d x (a + x)" : Thm.cterm              

\end{verbatim}

{\footnotesize\begin{verbatim}

   > (*-5-*);

   > val Some t5 = parse Diff.thy  "d_d x (a + x)";

      val t5 = "d_d x (a + x)" : Thm.cterm             

\end{verbatim}

Der Pase liefert hier einen ''zu sch\"onen`` Ausdruck in Form eines cterms, der wie ein string aussieht. Am verl\"asslichsten sind terme, die sich selbst erzeugen lassen.

\section{Details von Termen}

Mit Hilfe der darunterliegenden Darstellung sieht man, dass ein cterm in einen term umgewandelt werden kann.

{\footnotesize\begin{verbatim}

   > term_of;

      val it = fn : Thm.cterm -> Term.term

\end{verbatim}

Durch die Umwandlung eines cterms in einen term sieht man die einzelnen Teile des Terms. ''Free`` bedeutet, dass man die Variable \"andern kann.

{\footnotesize\begin{verbatim}

   > term_of t4;

      val it =

         Free ("d_d", "[RealDef.real, RealDef.real] => RealDef.real") $ ... $

         ...: Term.term

\end{verbatim}

In diesem Fall sagt uns das ''Const``, dass die Variable eine Konstante ist, also ein Fixwert ist und immer die selbe Funktion hat.

{\footnotesize\begin{verbatim}

   > term_of t5;

      val it =

         Const ("Diff.d_d", "[RealDef.real, RealDef.real] => RealDef.real") $ ... $

         ... : Term.term

\end{verbatim}

Sollten verschiedene Teile des Output nicht sichtbar sein, kann die Schriftgr\"osse ge\"andert werden.

{\footnotesize\begin{verbatim}

   > print_depth;

      val it = fn : int -> unit

 \end{verbatim}

Zuerst gibt man die Schriftgr\"osse ein, danach den term, der gr\"osser werden soll.

{\footnotesize\begin{verbatim}

   > print_depth 10;

      val it = () : unit

   > term_of t4;

         val it =

            Free ("d_d", "[RealDef.real, RealDef.real] => RealDef.real") $

                Free ("x", "RealDef.real") $

            (Const ("op +", "[RealDef.real, RealDef.real] => RealDef.real") $

                Free ("a", "RealDef.real") $ Free ("x", "RealDef.real"))

         : Term.term

   > print_depth 10;

         val it = () : unit

   > term_of t5;

         val it =

            Const ("Diff.d_d", "[RealDef.real, RealDef.real] => RealDef.real") $

                Free ("x", "RealDef.real") $

            (Const ("op +", "[RealDef.real, RealDef.real] => RealDef.real") $

                Free ("a", "RealDef.real") $ Free ("x", "RealDef.real"))

         : Term.term

\end{verbatim}

Eine andere Variante um den Unterschied der beiden Terme zu sehen ist folgende: 

{\footnotesize\begin{verbatim}

   > (*-4-*) val thy = Rational.thy;

      val thy =

         {ProtoPure, CPure, HOL, Set, Typedef, Fun, Product_Type, Lfp, Gfp,

         Sum_Type, Relation, Record, Inductive, Transitive_Closure,

         Wellfounded_Recursion, NatDef, Nat, NatArith, Divides, Power,

         SetInterval, Finite_Set, Equiv, IntDef, Int, Datatype_Universe,

         Datatype, Numeral, Bin, IntArith, Wellfounded_Relations, Recdef, IntDiv,

         IntPower, NatBin, NatSimprocs, Relation_Power, PreList, List, Map,

         Hilbert_Choice, Main, Lubs, PNat, PRat, PReal, RealDef, RealOrd,

         RealInt, RealBin, RealArith0, RealArith, RComplete, RealAbs, RealPow,

         Ring_and_Field, Complex_Numbers, Real, ListG, Tools, Script, Typefix,

         Float, ComplexI, Descript, Atools, Simplify, Poly, Rational}

     : Theory.theory

   > ((atomty) o term_of o the o (parse thy)) "d_d x (a + x)";

      ***

      *** Free (d_d, [real, real] => real)

      *** . Free (x, real)

      *** . Const (op +, [real, real] => real)

      *** . . Free (a, real)

      *** . . Free (x, real)

      ***

      val it = () : unit

   > (*-5-*) val thy = Diff.thy;

      val thy =

         {ProtoPure, CPure, HOL, Set, Typedef, Fun, Product_Type, Lfp, Gfp,

         Sum_Type, Relation, Record, Inductive, Transitive_Closure,

         Wellfounded_Recursion, NatDef, Nat, NatArith, Divides, Power,

         SetInterval, Finite_Set, Equiv, IntDef, Int, Datatype_Universe,

         Datatype, Numeral, Bin, IntArith, Wellfounded_Relations, Recdef, IntDiv,

         IntPower, NatBin, NatSimprocs, Relation_Power, PreList, List, Map,

         Hilbert_Choice, Main, Lubs, PNat, PRat, PReal, RealDef, RealOrd,

         RealInt, RealBin, RealArith0, RealArith, RComplete, RealAbs, RealPow,

         Ring_and_Field, Complex_Numbers, Real, Calculus, Trig, ListG, Tools,

         Script, Typefix, Float, ComplexI, Descript, Atools, Simplify, Poly,

         Equation, LinEq, Root, RootEq, Rational, RatEq, RootRat, RootRatEq,

         PolyEq, LogExp, Diff} : Theory.theory

   > ((atomty) o term_of o the o (parse thy)) "d_d x (a + x)";

      ***

      *** Const (Diff.d_d, [real, real] => real)

      *** . Free (x, real)

      *** . Const (op +, [real, real] => real)

      *** . . Free (a, real)

      *** . . Free (x, real)

      ***

      val it = () : unit

\end{verbatim}

{\chapter{''Rewriting``}}

{\section{}}

Bei Rewriting handelt es sich um die Vereinfachung eines Terms in vielen kleinen Schritten und nach bestimmten Regeln. Der Computer wendet dabei hintereinander verschiedene Rechengesetze an, weil er den Term ansonsten nicht l\"osen kann.

{\footnotesize\begin{verbatim}

> rewrite_;

val it = fn

:

   Theory.theory ->

   ((Term.term * Term.term) list -> Term.term * Term.term -> bool) ->

   rls ->

   bool ->

   Thm.thm -> Term.term -> (Term.term * Term.term list) Library.option

> rewrite;

val it = fn

:

   theory' ->

   rew_ord' ->

   rls' -> bool -> thm' -> cterm' -> (string * string list) Library.option

\end{verbatim}

\textbf{Versuchen Sie es!} Um zu sehen, wie der Computer vorgeht und welche Rechengesetze er anwendet, zeigen wir Ihnen durch Differenzieren von (a + a * (2 + b)), die einzelnen Schritte. Sie k\"onnen nat\"urlichauch selbst einige Beispiele ausprobieren!

Zuerst legt man fest, dass es sich um eine Differenzierung handelt.

{\footnotesize\begin{verbatim}

   > val thy' = "Diff.thy";

      val thy' = "Diff.thy" : string

\end{verbatim}

Dann gibt man die zu l\"osende Rechnung ein.

{\footnotesize\begin{verbatim}

   > val ct = "d_d x (a + a * (2 + b))";

      val ct = "d_d x (a + a * (2 + b))" : string

\end{verbatim}

Anschließend gibt man bekannt, dass die Summenregel angewandt werden soll.

{\footnotesize\begin{verbatim}

   > val thm = ("diff_sum","");

      val thm = ("diff_sum", "") : string * string

\end{verbatim}

Schliesslich wird die erste Ableitung angezeigt.

{\footnotesize\begin{verbatim}

   > val Some (ct,_) = rewrite_inst thy' "tless_true" "eval_rls" true

                        [("bdv","x::real")] thm ct;#

      val ct = "d_d x a + d_d x (a * (2 + b))" : cterm'

\end{verbatim}

Will man auch die zweite Ableitung sehen, geht man so vor:

{\footnotesize\begin{verbatim}

   > val thm = ("diff_prod_const","");

      val thm = ("diff_prod_const", "") : string * string

\end{verbatim} 

Auch die zweite Ableitung wird sichtbar.

{\footnotesize\begin{verbatim}

   > val Some (ct,_) = rewrite_inst thy' "tless_true" "eval_rls" true

                        [("bdv","x::real")] thm ct;#

      val ct = "d_d x a + a * d_d x (2 + b)" : cterm'

\end{verbatim}

{\section{M\"oglichkeiten von Rewriting}

Es gibt verscheidene Varianten von Rewriting, die alle eine bestimmte Bedeutung haben.

\textit{rewrite\_inst} bedeutet, dass die Liste der Terme vor dem Rewriting durch ein ''Theorem`` (ein mathematischer Begriff f\"ur einen Satz) ersetzt wird.

{\footnotesize\begin{verbatim}

> rewrite_inst;

val it = fn

:

   theory' ->

   rew_ord' ->

   rls' ->

   bool -> 'a -> thm' -> cterm' -> (cterm' * cterm' list) Library.option

\end{verbatim}

Mit Hilfe von \textit{rewrite\_set} werden Terme, die normalerweise nur mit einem Thoerem vereinfacht dargestellt werden, mit einem ganzen ''rule set`` (=Regelsatz, weiter unten erkl\"art) umgeschrieben.

{\footnotesize\begin{verbatim}

   > rewrite_set;

      val it = fn

      : theory' -> bool -> rls' -> cterm' -> (string * string list) Library.option

\end{verbatim}

\textit{rewrite\_set\_inst} ist eine Kombination der beiden oben genannten M\"oglichkeiten.

{\footnotesize\begin{verbatim}

   > rewrite_set_inst;

      val it = fn

      :

         theory' ->

         bool -> subs' -> rls' -> cterm' -> (string * string list) Library.option

\end{verbatim}

Wenn man sehen m\"ochte, wie Rewriting bei den einzelnen Theorems funktioniert, kann man dies mit \textit{trace\_rewrite} versuchen.

{\footnotesize\begin{verbatim}

   > toggle;

      val it = fn : bool ref -> bool

   > toggle trace_rewrite;

      val it = true : bool

   > toggle trace_rewrite;

      val it = false : bool

\end{verbatim}

\section{Rule sets}

Einige der oben genannten Varianten von Rewriting beziehen sich nicht nur auf einen Theorem, sondern auf einen ganzen Block von Theorems, die man als Rule set bezeichnet.

Dieser wird so lange angewendet, bis ein Element davon f\"ur Rewriting verwendet werden kann. Sollte der Begriff ''terminate`` fehlen, wird das Rule set nicht beendet und l\"auft weiter.

Ein Beispiel f\"ur einen Regelsatz ist folgendes:

\footnotesize\begin{verbatim}

???????????

\end{verbatim}

\footnotesize\begin{verbatim}

   > sym;

      val it = "?s = ?t ==> ?t = ?s" : Thm.thm

   > rearrange_assoc;

      val it =

         Rls

            {id = "rearrange_assoc",

               scr = Script (Free ("empty_script", "RealDef.real")),

               calc = [],

               erls =

               Rls

                  {id = "e_rls",

                     scr = EmptyScr,

                     calc = [],

                     erls = Erls,

                     srls = Erls,

                     rules = [],

                     rew_ord = ("dummy_ord", fn),

                     preconds = []},

               srls =

               Rls

                  {id = "e_rls",

                     scr = EmptyScr,

                     calc = [],

                     erls = Erls,

                     srls = Erls,

                     rules = [],

                     rew_ord = ("dummy_ord", fn),

                     preconds = []},

               rules =

               [Thm ("sym_radd_assoc", "?m1 + (?n1 + ?k1) = ?m1 + ?n1 + ?k1"  [.]),

                  Thm

                     ("sym_rmult_assoc",

                        "?m1 * (?n1 * ?k1) = ?m1 * ?n1 * ?k1"  [.])],

               rew_ord = ("e_rew_ord", fn),

               preconds = []} : rls

\end{verbatim}

\section{Berechnung von Konstanten}

Sobald Konstanten in dem Bereich des Subterms sind, k\"onnen sie von einer Funktion berechnet werden:

\footnotesize\begin{verbatim}

   > calculate;

      val it = fn

      :

         theory' ->

         string *

         (

         string ->

         Term.term -> Theory.theory -> (string * Term.term) Library.option) ->

         cterm' -> (string * thm') Library.option

   > calculate_;

      val it = fn

      :

         Theory.theory ->

         string *

         (

         string ->

         Term.term -> Theory.theory -> (string * Term.term) Library.option) ->

         Term.term -> (Term.term * (string * Thm.thm)) Library.option

\end{verbatim}

Man bekommt das Ergebnis und die Theorem bezieht sich darauf. Daher sind die folgenden mathematischen Rechnungen m\"oglich:

\footnotesize\begin{verbatim}

   > calclist;

      val it =

         [("Vars", ("Tools.Vars", fn)), ("matches", ("Tools.matches", fn)),

            ("lhs", ("Tools.lhs", fn)), ("plus", ("op +", fn)),

            ("times", ("op *", fn)), ("divide_", ("HOL.divide", fn)),

            ("power_", ("Atools.pow", fn)), ("is_const", ("Atools.is'_const", fn)),

            ("le", ("op <", fn)), ("leq", ("op <=", fn)),

            ("ident", ("Atools.ident", fn)), ("sqrt", ("Root.sqrt", fn)),

            ("Test.is_root_free", ("is'_root'_free", fn)),

            ("Test.contains_root", ("contains'_root", fn))]

      :

         (

         string *

         (

         string *

         (

         string ->

         Term.term -> Theory.theory -> (string * Term.term) Library.option))) list

\end{verbatim}

Diese werden so angewendet:

\footnotesize\begin{verbatim}

\end{verbatim}

\chapter{Termordnung}

Die Anordnungen der Begriffe sind unverzichtbar f\"ur den Gebrauch des Umschreibens von normalen Funktionen und von normalen Formeln, die n\"otig sind um passende Modelle für Probleme zu finden.

\section{Beispiel f\"ur Termordnungen}

Es ist nicht unbedeutend eine Verbindung $<$ zu Termen herzustellen, die wirklich eine Ordnung besitzen, wie eine \"ubergehende und antisymmetrische Verbindung. Diese Ordnungen sind selbstaufrufende Bahnordnungen.

Hier ein Beispiel:

{\footnotesize\begin{verbatim}

   > sqrt_right;

      val it = fn : bool -> Theory.theory -> subst -> Term.term * Term.term -> b       ool

   > tless_true;

      val it = fn : subst -> Term.term * Term.term -> bool

\end{verbatim}

Das bool Argument gibt Ihnen die M\"oglichkeit die Kontrolle zu den zugeh\"origen Unterordunungen zur\"uck zu verfolgen, damit sich die Unterordnungen, die 'true' sind als strings anzeigen lassen.

\chapter{Methods}

Methods werden dazu verwendet, Probleme von \texttt{type} zu l\"osen. Sie sind in einer anderen Programmiersprache beschrieben. Die Sprache sieht einfach aus, hat aber im Hintergrund einen enormen Pr\"ufauffwand. So muss sich der Programmierer nicht mit technischen Details befassen, gleichzeitig k\"onnen aber auch keine falschen Anweisungen eingegeben werden.

\section{Der ''Syntax`` des Scriptes}

Syntax beschreibt den Zusammenhang der einzelnen Zeichen und Zeichenfolgen mit den Theorien.

Er kann so definiert werden:

\begin{tabbing}

123\=123\=expr ::=\=$|\;\;$\=\kill

\>script ::= {\tt Script} id arg$\,^*$ = body\\

\>\>arg ::= id $\;|\;\;($ ( id :: type ) $)$\\

\>\>body ::= expr\\

\>\>expr ::= \>\>{\tt let} id = expr $($ ; id = expr$)^*$ {\tt in} expr\\

\>\>\>$|\;$\>{\tt if} prop {\tt then} expr {\tt else} expr\\

\>\>\>$|\;$\>listexpr\\

\>\>\>$|\;$\>id\\

\>\>\>$|\;$\>seqex id\\

\>\>seqex ::= \>\>{\tt While} prop {\tt Do} seqex\\

\>\>\>$|\;$\>{\tt Repeat} seqex\\

\>\>\>$|\;$\>{\tt Try} seqex\\

\>\>\>$|\;$\>seqex {\tt Or} seqex\\

\>\>\>$|\;$\>seqex {\tt @@} seqex\\

\>\>\>$|\;$\>tac $($ id $|$ listexpr $)^*$\\

\>\>type ::= id\\

\>\>tac ::= id

\end{tabbing}}

\newpage

------------------------------- ALTER TEXT -------------------------------

\chapter{The hierarchy of problem types}\label{pbt}

\section{The standard-function for 'matching'}

Matching \cite{nipk:rew-all-that} is a technique used within rewriting, and used by \isac{} also for (a generalized) 'matching' a problem with a problem type. The function which tests for matching has the following signature:

{\footnotesize\begin{verbatim}

   ML> matches;

   val it = fn : theory -> term -> term -> bool

\end{verbatim}}%size

where the first of the two {\tt term} arguments is the particular term to be tested, and the second one is the pattern:

{\footnotesize\begin{verbatim}

   ML> val t = (term_of o the o (parse thy)) "#3 * x^^^#2 = #1";

   val t = Const (#,#) $ (# $ # $ (# $ #)) $ Free ("#1","RealDef.real") : term

   ML>

   ML> val p = (term_of o the o (parse thy)) "a * b^^^#2 = c";

   val p = Const (#,#) $ (# $ # $ (# $ #)) $ Free ("c","RealDef.real") : term

   ML> atomt p;

   *** -------------

   *** Const ( op =)

   *** . Const ( op *)

   *** . . Free ( a, )

   *** . . Const ( RatArith.pow)

   *** . . . Free ( b, )

   *** . . . Free ( #2, )

   *** . Free ( c, )

   val it = () : unit

   ML>

   ML> free2var;

   val it = fn : term -> term

   ML>

   ML> val pat = free2var p;

   val pat = Const (#,#) $ (# $ # $ (# $ #)) $ Var ((#,#),"RealDef.real") : term

   ML> Sign.string_of_term (sign_of thy) pat;

   val it = "?a * ?b ^^^ #2 = ?c" : cterm' 

   ML> atomt pat;

   *** -------------

   *** Const ( op =)

   *** . Const ( op *)

   *** . . Var ((a, 0), )

   *** . . Const ( RatArith.pow)

   *** . . . Var ((b, 0), )

   *** . . . Free ( #2, )

   *** . Var ((c, 0), )

   val it = () : unit

\end{verbatim}}%size % $ 

Note that the pattern {\tt pat} contains so-called {\it scheme variables} decorated with a {\tt ?} (analoguous to theorems). The pattern is generated by the function {\tt free2var}. This format of the pattern is necessary in order to obtain results like these:

{\footnotesize\begin{verbatim}

   ML> matches thy t pat;

   val it = true : bool

   ML>

   ML> val t2 = (term_of o the o (parse thy)) "x^^^#2 = #1";

   val t2 = Const (#,#) $ (# $ # $ Free #) $ Free ("#1","RealDef.real") : term

   ML> matches thy t2 pat;

   val it = false : bool    

   ML>

   ML> val pat2 = (term_of o the o (parse thy)) "?u^^^#2 = ?v";

   val pat2 = Const (#,#) $ (# $ # $ Free #) $ Var ((#,#),"RealDef.real") : term

   ML> matches thy t2 pat2;

   val it = true : bool 

\end{verbatim}}%size % $

\section{Accessing the hierarchy}

The hierarchy of problem types is encapsulated; it can be accessed by the following functions. {\tt show\_ptyps} retrieves all leaves of the hierarchy (here in an early version for testing):

{\footnotesize\begin{verbatim}

   ML> show_ptyps;

   val it = fn : unit -> unit

   ML> show_ptyps();

   [

    ["e_pblID"],

    ["equation", "univariate", "linear"],

    ["equation", "univariate", "plain_square"],

    ["equation", "univariate", "polynomial", "degree_two", "pq_formula"],

    ["equation", "univariate", "polynomial", "degree_two", "abc_formula"],

    ["equation", "univariate", "squareroot"],

    ["equation", "univariate", "normalize"],

    ["equation", "univariate", "sqroot-test"],

    ["function", "derivative_of"],

    ["function", "maximum_of", "on_interval"],

    ["function", "make"],

    ["tool", "find_values"],

    ["functional", "inssort"]

   ]

   val it = () : unit

\end{verbatim}}%size

The retrieve function for individual problem types is {\tt get\_pbt}

\footnote{A function providing better readable output is in preparation}. Note that its argument, the 'problem identifier' {\tt pblID}, has the strings listed in reverse order w.r.t. the hierarchy, i.e. from the leave to the root. This order makes the {\tt pblID} closer to a natural description:

{\footnotesize\begin{verbatim}

   ML> get_pbt;

   val it = fn : pblID -> pbt

   ML> get_pbt ["squareroot", "univariate", "equation"];

   val it =

     {met=[("SqRoot.thy","square_equation")],

      ppc=[("#Given",(Const (#,#),Free (#,#))),

           ("#Given",(Const (#,#),Free (#,#))),

           ("#Given",(Const (#,#),Free (#,#))),

           ("#Find",(Const (#,#),Free (#,#)))],

      thy={ProtoPure, CPure, HOL, Ord, Set, subset, equalities, mono, Vimage, Fun,

            Prod, Lfp, Relation, Trancl, WF, NatDef, Gfp, Sum, Inductive, Nat,

            Arith, Divides, Power, Finite, Equiv, IntDef, Int, Univ, Datatype,

            Numeral, Bin, IntArith, WF_Rel, Recdef, IntDiv, NatBin, List, Option,

            Map, Record, RelPow, Sexp, String, Calculation, SVC_Oracle, Main,

            Zorn, Filter, PNat, PRat, PReal, RealDef, RealOrd, RealInt, RealBin,

            HyperDef, Descript, ListG, Tools, Script, Typefix, Atools, RatArith,

            SqRoot},

      where_=[Const ("SqRoot.contains'_root","bool => bool") $

              Free ("e_","bool")]} : pbt

\end{verbatim}}%size %$

where the records fields hold the following data:

\begin{description}

\item [\tt thy]: the theory necessary for parsing the formulas

\item [\tt ppc]: the items of the problem type, divided into those {\tt Given}, the precondition {\tt Where} and the output item(s) {\tt Find}. The items of {\tt Given} and {\tt Find} are all headed by so-called descriptions, which determine the type. These descriptions are defined in {\tt [isac-src]/Isa99/Descript.thy}.

\item [\tt met]: the list of methods solving this problem type.\\

\end{description}

The following function adds or replaces a problem type (after having it prepared using {\tt prep\_pbt})

{\footnotesize\begin{verbatim}

   ML> store_pbt;

   val it = fn : pbt * pblID -> unit

   ML> store_pbt

    (prep_pbt SqRoot.thy

    (["newtype","univariate","equation"],

     [("#Given" ,["equality e_","solveFor v_","errorBound err_"]),

      ("#Where" ,["contains_root (e_::bool)"]),

      ("#Find"  ,["solutions v_i_"])

     ],

     [("SqRoot.thy","square_equation")]));

   val it = () : unit

\end{verbatim}}%size

When adding a new type with argument {\tt pblID}, an immediate parent must already exist in the hierarchy (this is the one with the tail of {\tt pblID}).

\section{Internals of the datastructure}

This subsection only serves for the implementation of the hierarchy browser and can be skipped by the authors of math knowledge.

A problem type is described by the following record type (in the file {\tt [isac-src]/globals.sml}, the respective functions are in {\tt [isac-src]/ME/ptyps.sml}), and held in a global reference variable:

{\footnotesize\begin{verbatim}

   type pbt = 

        {thy   : theory,       (* the nearest to the root,

                                  which allows to compile that pbt  *)

         where_: term list,    (* where - predicates                *)

         ppc   : ((string *    (* fields "#Given","#Find"           *)

                   (term *     (* description                       *)

                    term))     (* id                                *)

                      list),                                        

         met   : metID list};  (* methods solving the pbt           *)

   datatype ptyp = 

            Ptyp of string *   (* key within pblID                  *)

                    pbt list * (* several pbts with different domIDs*)

                    ptyp list;

   val e_Ptyp = Ptyp ("empty",[],[]);

   type ptyps = ptyp list;

   val ptyps = ref ([e_Ptyp]:ptyps);

\end{verbatim}}%size

The predicates in {\tt where\_} (i.e. the preconditions) usually are defined in the respective theory in {\tt[isac-src]/knowledge}. Most of the predicates are not defined by rewriting, but by SML-code contained in the respective {\tt *.ML} file.

Each item is headed by a so-called description which provides some guidance for interactive input. The descriptions are defined in {\tt[isac-src]/Isa99/Descript.thy}.

\section{Match a formalization with a problem type}\label{pbl}

A formalization is {\it match}ed with a problem type which yields a problem. A formal description of this kind of {\it match}ing can be found in \\{\tt ftp://ft.ist.tugraz.at/projects/isac/publ/calculemus01.ps.gz}. A formalization of an equation is e.g.

{\footnotesize\begin{verbatim}

   ML> val fmz = ["equality (#1 + #2 * x = #0)",

                  "solveFor x",

                  "solutions L"] : fmz;

   val fmz = ["equality (#1 + #2 * x = #0)","solveFor x","solutions L"] : fmz

\end{verbatim}}%size

Given a formalization (and a specification of the problem, i.e. a theory, a problemtype, and a method) \isac{} can solve the respective problem automatically. The formalization must match the problem type for this purpose:

{\footnotesize\begin{verbatim}

   ML> match_pbl;

   val it = fn : fmz -> pbt -> match'

   ML>

   ML> match_pbl fmz (get_pbt ["univariate","equation"]);

   val it =

     Matches'

       {Find=[Correct "solutions L"],

        Given=[Correct "equality (#1 + #2 * x = #0)",Correct "solveFor x"],

        Relate=[],Where=[Correct "matches (?a = ?b) (#1 + #2 * x = #0)"],With=[]}

     : match'

   ML>

   ML> match_pbl fmz (get_pbt ["linear","univariate","equation"]);

   val it =

     Matches'

       {Find=[Correct "solutions L"],

        Given=[Correct "equality (#1 + #2 * x = #0)",Correct "solveFor x"],

        Relate=[],

        Where=[Correct

                 "matches (          x = #0) (#1 + #2 * x = #0) |

                  matches (     ?b * x = #0) (#1 + #2 * x = #0) |

                  matches (?a      + x = #0) (#1 + #2 * x = #0) |

                  matches (?a + ?b * x = #0) (#1 + #2 * x = #0)"],

        With=[]} : match'

   ML>

   ML> match_pbl fmz (get_pbt ["squareroot","univariate","equation"]);

   val it =

     NoMatch'

       {Find=[Correct "solutions L"],

        Given=[Correct "equality (#1 + #2 * x = #0)",Correct "solveFor x",

               Missing "errorBound err_"],Relate=[],

        Where=[False "contains_root #1 + #2 * x = #0 "],With=[]} : match'

\end{verbatim}}%size

The above formalization does not match the problem type \\{\tt["squareroot","univariate","equation"]} which is explained by the tags:

\begin{tabbing}

123\=\kill

\> {\tt Missing:} the item is missing in the formalization as required by the problem type\\

\> {\tt Superfl:} the item is not required by the problem type\\

\> {\tt Correct:} the item is correct, or the precondition ({\tt Where}) is true\\

\> {\tt False:} the precondition ({\tt Where}) is false\\

\> {\tt Incompl:} the item is incomlete, or not yet input.\\

\end{tabbing}

\section{Refine a problem specification}

The challenge in constructing the problem hierarchy is, to design the branches in such a way, that problem refinement can be done automatically (as it is done in algebra system e.g. by a internal hierarchy of equations).

For this purpose the hierarchy must be built using the following rules: Let $F$ be a formalization and $P$ and $P_i,\:i=1\cdots n$ problem types, where the $P_i$ are specialized problem types w.r.t. $P$ (i.e. $P$ is a parent node of $P_i$), then

{\small

\begin{enumerate}

\item for all $F$ matching some $P_i$ must follow, that $F$ matches $P$

\item an $F$ matching $P$ should not have more than {\em one} $P_i,\:i=1\cdots n-1$ with $F$ matching $P_i$ (if there are more than one $P_i$, the first one will be taken)

\item for all $F$ matching some $P$ must follow, that $F$ matches $P_n$\\

\end{enumerate}}%small

\noindent Let us give an example for the point (1.) and (2.) first:

{\footnotesize\begin{verbatim}

   ML> refine;

   val it = fn : fmz -> pblID -> match list

   ML>

   ML> val fmz = ["equality (sqrt(#9+#4*x)=sqrt x + sqrt(#5+x))",

              "solveFor x","errorBound (eps=#0)",

              "solutions L"];

   ML>

   ML> refine fmz ["univariate","equation"];

   *** pass ["equation","univariate"]

   *** pass ["equation","univariate","linear"]

   *** pass ["equation","univariate","plain_square"]

   *** pass ["equation","univariate","polynomial"]

   *** pass ["equation","univariate","squareroot"]

   val it =

     [Matches

        (["univariate","equation"],

         {Find=[Correct "solutions L"],

          Given=[Correct "equality (sqrt (#9 + #4 * x) = sqrt x + sqrt (#5 + x))",

                 Correct "solveFor x",Superfl "errorBound (eps = #0)"],Relate=[],

          Where=[Correct

                   "matches (?a = ?b) (sqrt (#9 + #4 * x) = sqrt x + sqrt (#5 + x))"],

          With=[]}),

      NoMatch

        (["linear","univariate","equation"],

         {Find=[Correct "solutions L"],

          Given=[Correct "equality (sqrt (#9 + #4 * x) = sqrt x + sqrt (#5 + x))",

                 Correct "solveFor x",Superfl "errorBound (eps = #0)"],Relate=[],

          Where=[False "(?a + ?b * x = #0) (sqrt (#9 + #4 * x#"],

          With=[]}),

      NoMatch

        (["plain_square","univariate","equation"],

         {Find=[Correct "solutions L"],

          Given=[Correct "equality (sqrt (#9 + #4 * x) = sqrt x + sqrt (#5 + x))",

                 Correct "solveFor x",Superfl "errorBound (eps = #0)"],Relate=[],

          Where=[False

                   "matches (?a + ?b * x ^^^ #2 = #0)"],

          With=[]}),

      NoMatch

        (["polynomial","univariate","equation"],

         {Find=[Correct "solutions L"],

          Given=[Correct "equality (sqrt (#9 + #4 * x) = sqrt x + sqrt (#5 + x))",

                 Correct "solveFor x",Superfl "errorBound (eps = #0)"],Relate=[],

          Where=[False 

                 "is_polynomial_in sqrt (#9 + #4 * x) = sqrt x + sqrt (#5 + x) x"],

          With=[]}),

      Matches

        (["squareroot","univariate","equation"],

         {Find=[Correct "solutions L"],

          Given=[Correct "equality (sqrt (#9 + #4 * x) = sqrt x + sqrt (#5 + x))",

                 Correct "solveFor x",Correct "errorBound (eps = #0)"],Relate=[],

          Where=[Correct

                   "contains_root sqrt (#9 + #4 * x) = sqrt x + sqrt (#5 + x) "],

          With=[]})] : match list

\end{verbatim}}%size}%footnotesize\label{refine}

This example shows, that in order to refine an {\tt["univariate","equation"]}, the formalization must match respective respective problem type (rule (1.)) and one of the descendants which should match selectively (rule (2.)).

If no one of the descendants of {\tt["univariate","equation"]} match, rule (3.) comes into play: The {\em last} problem type on this level ($P_n$) provides for a special 'problem type' {\tt["normalize"]}. This node calls a method transforming the equation to a (or another) normal form, which then may match. Look at this example:

{\footnotesize\begin{verbatim}

   ML>  val fmz = ["equality (x+#1=#2)",

               "solveFor x","errorBound (eps=#0)",

               "solutions L"];

   [...]

   ML>

   ML>  refine fmz ["univariate","equation"];

   *** pass ["equation","univariate"]

   *** pass ["equation","univariate","linear"]

   *** pass ["equation","univariate","plain_square"]

   *** pass ["equation","univariate","polynomial"]

   *** pass ["equation","univariate","squareroot"]

   *** pass ["equation","univariate","normalize"]

   val it =

     [Matches

        (["univariate","equation"],

         {Find=[Correct "solutions L"],

          Given=[Correct "equality (x + #1 = #2)",Correct "solveFor x",

                 Superfl "errorBound (eps = #0)"],Relate=[],

          Where=[Correct "matches (?a = ?b) (x + #1 = #2)"],With=[]}),

      NoMatch

        (["linear","univariate","equation"],

   [...]

          With=[]}),

      NoMatch

        (["squareroot","univariate","equation"],

         {Find=[Correct "solutions L"],

          Given=[Correct "equality (x + #1 = #2)",Correct "solveFor x",

                 Correct "errorBound (eps = #0)"],Relate=[],

          Where=[False "contains_root x + #1 = #2 "],With=[]}),

      Matches

        (["normalize","univariate","equation"],

         {Find=[Correct "solutions L"],

          Given=[Correct "equality (x + #1 = #2)",Correct "solveFor x",

                 Superfl "errorBound (eps = #0)"],Relate=[],Where=[],With=[]})]

     : match list

\end{verbatim}}%size

The problem type $P_n$, {\tt["normalize","univariate","equation"]}, will transform the equation {\tt x + \#1 = \#2} to the normal form {\tt \#-1 + x = \#0}, which then will match {\tt["linear","univariate","equation"]}.

This recursive search on the problem hierarchy can be  done within a proof state. This leads to the next section.

\chapter{Methods}\label{met}

A problem type can have one ore more methods solving a respective problem. A method is described by means of another new program language. The language itself looks like a simple functional language, but constructs an imperative proof-state behind the scenes (thus liberating the programer from dealing with technical details and also prohibiting incorrect construction of the proof tree). The interpreter of 'scripts' written in this language evaluates the scriptexpressions, and also delivers certain parts of the script itself for discussion with the user.

\section{The scripts' syntax}

The syntax of scripts follows the definition given in Backus-normal-form:

{\it

\begin{tabbing}

123\=123\=expr ::=\=$|\;\;$\=\kill

\>script ::= {\tt Script} id arg$\,^*$ = body\\

\>\>arg ::= id $\;|\;\;($ ( id :: type ) $)$\\

\>\>body ::= expr\\

\>\>expr ::= \>\>{\tt let} id = expr $($ ; id = expr$)^*$ {\tt in} expr\\

\>\>\>$|\;$\>{\tt if} prop {\tt then} expr {\tt else} expr\\

\>\>\>$|\;$\>listexpr\\

\>\>\>$|\;$\>id\\

\>\>\>$|\;$\>seqex id\\

\>\>seqex ::= \>\>{\tt While} prop {\tt Do} seqex\\

\>\>\>$|\;$\>{\tt Repeat} seqex\\

\>\>\>$|\;$\>{\tt Try} seqex\\

\>\>\>$|\;$\>seqex {\tt Or} seqex\\

\>\>\>$|\;$\>seqex {\tt @@} seqex\\

\>\>\>$|\;$\>tac $($ id $|$ listexpr $)^*$\\

\>\>type ::= id\\

\>\>tac ::= id

\end{tabbing}}

where {\it id} is an identifier with the usual syntax, {\it prop} is a proposition constructed by Isabelles logical operators (see \cite{Isa-obj} {\tt [isabelle]/src/HOL/HOL.thy}), {\it listexpr} (called {\bf list-expression}) is constructed by Isabelles list functions like {\tt hd, tl, nth} described in {\tt [isabelle]/src/HOL/List.thy}, and {\it type} are (virtually) all types declared in Isabelles version 99.

Expressions containing some of the keywords {\tt let}, {\tt if} etc. are called {\bf script-expressions}.

Tactics {\it tac} are (curried) functions. For clarity and simplicity reasons, {\it listexpr} must not contain a {\it tac}, and {\it tac}s must not be nested,

\section{Control the flow of evaluation}

The flow of control is managed by the following script-expressions called {\it tacticals}.

\begin{description}

\item{{\tt while} prop {\tt Do} expr id} 

\item{{\tt if} prop {\tt then} expr {\tt else} expr}

\end{description}

While the the above script-expressions trigger the flow of control by evaluating the current formula, the other expressions depend on the applicability of the tactics within their respective subexpressions (which in turn depends on the proofstate)

\begin{description}

\item{{\tt Repeat} expr id}

\item{{\tt Try} expr id}

\item{expr {\tt Or} expr id}

\item{expr {\tt @@} expr id}

\end{description}

\begin{description}

\item xxx

\end{description}

\chapter{Do a calculational proof}

First we list all the tactics available so far (this list may be extended during further development of \isac).

\section{Tactics for doing steps in calculations}

\input{tactics}

\section{The functionality of the math engine}

A proof is being started in the math engine {\tt me} by the tactic

\footnote{In the present version a tactic is of type {\tt mstep}.}

 {\tt Init\_Proof}, and interactively promoted by other tactics. On input of each tactic the {\tt me} returns the resulting formula and the next tactic applicable. The proof is finished, when the {\tt me} proposes {\tt End\_Proof} as the next tactic.

We show a calculation (calculational proof) concerning equation solving, where the type of equation is refined automatically: The equation is given by the respective formalization ...

{\footnotesize\begin{verbatim}

   ML> val fmz = ["equality ((x+#1)*(x+#2)=x^^^#2+#8)","solveFor x",

                  "errorBound (eps=#0)","solutions L"];

   val fmz =

     ["equality ((x+#1)*(x+#2)=x^^^#2+#8)","solveFor x","errorBound (eps=#0)",

      "solutions L"] : string list

   ML>

   ML> val spec as (dom, pbt, met) = ("SqRoot.thy",["univariate","equation"],

                                 ("SqRoot.thy","no_met"));

   val dom = "SqRoot.thy" : string

   val pbt = ["univariate","equation"] : string list

   val met = ("SqRoot.thy","no_met") : string * string

\end{verbatim}}%size

... and the specification {\tt spec} of a domain {\tt dom}, a problem type {\tt pbt} and a method {\tt met}. Note that the equation is such, that it is not immediatly clear, what type it is in particular (it could be a polynomial of degree 2; but, for sure, the type is some specialized type of a univariate equation). Thus, no method ({\tt no\_met}) can be specified for solving the problem.

Nevertheless this specification is sufficient for automatically solving the equation --- the appropriate method will be found by refinement within the hierarchy of problem types.

\section{Initialize the calculation}

The start of a new proof requires the following initializations: The proof state is given by a proof tree {\tt ptree} and a position {\tt pos'}; both are empty at the beginning. The tactic {\tt Init\_Proof} is, like all other tactics, paired with an identifier of type {\tt string} for technical reasons.

{\footnotesize\begin{verbatim}

   ML>  val (mID,m) = ("Init_Proof",Init_Proof (fmz, (dom,pbt,met)));

   val mID = "Init_Proof" : string

   val m =

     Init_Proof

       (["equality ((x+#1)*(x+#2)=x^^^#2+#8)","solveFor x","errorBound (eps=#0)",

         "solutions L"],("SqRoot.thy",[#,#],(#,#))) : mstep

   ML>

   ML>  val (p,_,f,nxt,_,pt) = me (mID,m) e_pos' c EmptyPtree;

   val p = ([],Pbl) : pos'

   val f = Form' (PpcKF (0,EdUndef,0,Nundef,(#,#))) : mout

   val nxt = ("Refine_Tacitly",Refine_Tacitly ["univariate","equation"])

     : string * mstep

   val pt =

     Nd

       (PblObj

          {branch=#,cell=#,env=#,loc=#,meth=#,model=#,origin=#,ostate=#,probl=#,

           result=#,spec=#},[]) : ptree

   \end{verbatim}}%size

The mathematics engine {\tt me} returns the resulting formula {\tt f} of type {\tt mout} (which in this case is a problem), the next tactic {\tt nxt}, and a new proof state ({\tt ptree}, {\tt pos'}).

We can convince ourselves, that the problem is still empty, by increasing {\tt Compiler.Control.Print.printDepth}:

{\footnotesize\begin{verbatim}

   ML> Compiler.Control.Print.printDepth:=8; (*4 default*)

   val it = () : unit

   ML>

   ML> f;

   val it =

     Form'

       (PpcKF

          (0,EdUndef,0,Nundef,

           (Problem [],

            {Find=[Incompl "solutions []"],

             Given=[Incompl "equality",Incompl "solveFor"],Relate=[],

             Where=[False "matches (?a = ?b) e_"],With=[]}))) : mout

\end{verbatim}}%size

Recall, please, the format of a problem as presented in sect.\ref{pbl} on p.\pageref{pbl}; such an 'empty' problem can be found above encapsulated by several constructors containing additional data (necessary for the dialog guide, not relevant here).\\

{\it In the sequel we will omit output of the {\tt me} if it is not important for the respective context}.\\

In general, the dialog guide will hide the following two tactics {\tt Refine\_Tacitly} and {\tt Model\_Problem} from the user.

{\footnotesize\begin{verbatim}

   ML>  nxt;

   val it = ("Refine_Tacitly",Refine_Tacitly ["univariate","equation"])

     : string * mstep

   ML>

   ML>  val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   val nxt = ("Model_Problem",Model_Problem ["normalize","univariate","equation"])

     : string * mstep

   ML>

   ML>  val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

\end{verbatim}}%size

\section{The phase of modeling} 

comprises the input of the items of the problem; the {\tt me} can help by use of the formalization tacitly transferred by {\tt Init\_Proof}. In particular, the {\tt me} in general 'knows' the next promising tactic; the first one has been returned by the (hidden) tactic {\tt Model\_Problem}.

{\footnotesize\begin{verbatim}

   ML>  nxt;

   val it =