\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{Alexandra Hirn und Eva Rott\\

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

\date{\today}

\begin{document}

\maketitle

\newpage

\tableofcontents

\newpage

\listoftables

\newpage

\chapter{Einleitung}

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

\paragraph{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\"ur 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 Problemen, f\"ur L\"osungsmethoden etc. Wir beginnen mit mathematischen Formeln.

\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 (eine Zeichenfolge). In dieser Form weiss der Computer nicht, dass z.B. eine Multiplikation {\em vor} einer Addition zu rechnen ist. Isabelle braucht dazu eine andere Darstellung f\"ur Formeln. In diese kann man mit der Funktion {\tt 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 Diese Form heisst {\tt term} und ist nicht f\"ur den Menschen zum lesen gedacht. Isabelle braucht sie aber intern zum Rechnen. Wir wollen sie mit Hilfe von {\tt val} (value) auf der Variable {\tt t} speichern:

{\footnotesize\begin{verbatim}

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

      val t =  

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

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

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

               ...) : Term.term

\end{verbatim}

Von dieser Variable {\tt t} kann man den Wert jederzeit abrufen:

\footnotesize\begin{verbatim}

   > t;

      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}

Der auf {\tt t} gespeicherte Term kann einer Funktion {\tt atomty} \"ubergeben werden, die diesen in einer dritten Form 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}

Diese Darstellung nennt man ``abstract syntax'' und macht unmittelbar klar, dass man a und b nicht addieren kann, weil ein Mal vorhanden ist.

\newline Es gibt noch eine vierte Art von Term, den cterm. Er wird weiter unten verwendet, weil er sich als string lesbar darstellt.

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

Der Unterschied zwischen \isac{} und bisheriger Mathematiksoftware (GeoGebra, Mathematica, Maple, Derive etc.) ist, dass das mathematische Wissen nicht im Programmcode steht, sondern in sogenannten theories (Theorien).

Dort wird das Mathematikwissen in einer f\"ur nicht Programmierer lesbaren Form geschrieben. Das Wissen von \isac{} ist in folgenden Theorien entahlten:

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

{\tt ProtoPure} und {\tt CPure} enthalten diese logischen Grundlagen, die in {\tt HOL} und den nachfolgenden Theorien erweitert werden. \isac{} als letzte Theorie beinhaltet das gesamte Wissen.

Dass das Mal vor dem Plus berechnet wird, ist so festgelegt:

\footnotesize\begin{verbatim}

   class plus =

   fixes plus :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "+" 65)

   class minus =

   fixes minus :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "-" 65)

   class uminus =

   fixes uminus :: "'a \<Rightarrow> 'a" ("- _" [81] 80)

   class times =

   fixes times :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "*" 70) 

\end{verbatim}

{\tt infix} gibt an, dass der Operator zwischen den Zahlen steht und nicht, wie in ''abstract syntax``, vorne oben.

Die Zahlen rechts davon legen die Priorit\"at fest. 70 f\"ur Mal ist gr\"osser als 65 f\"ur Plus und wird daher zuerst berechnet.

Wollen Sie wissen, wie die einzelnen Rechengesetze aussehen, k\"onnen Sie im Internet folgenden Link ansehen: http://isabelle.in.tum.de/dist/library/HOL/Groups.html

\paragraph{} Der Vorgang, bei dem aus einem {\tt string} ein Term entsteht, nennt man Parsing. Dazu wird Wissen aus der Theorie ben\"otigt, denn {\tt str2term} nimmt intern eine parse-Funktion, bei der immer das gesamte \isac{}-Wissen verwendet wird. Bei dieser Funktion wird weiters festgelegt, aus welcher Theorie das Wissen genommen werden soll.

\footnotesize\begin{verbatim}

   > parse Isac.thy "a + b";

      val it = Some "a + b" : Thm.cterm Library.option

\end{verbatim}

Um sich das Weiterrechnen zu erleichtern, kann das Ergebnis vom Parsing auf eine Variable, wie zum Beispiel {\tt t} gespeichert werden:

\footnotesize\begin{verbatim}

   > val t = parse Isac.thy "a + b";

      val t = Some "a + b" : Thm.cterm Library.option

\end{verbatim}

{\tt Some} bedeutet, dass das n\"otige Wissen vorhanden ist, um die Rechnung durchzuf\"uhren. {\tt None} zeigt uns, dass das Wissen fehlt oder ein Fehler aufgetreten ist. Daher sieht man im folgenden Beispiel, dass {\tt HOL.thy} nicht ausreichend Wissen enth\"alt:

\footnotesize\begin{verbatim}

   > parse HOL.thy "a + b";

      val it = None : Thm.cterm Library.option

\end{verbatim}

Anschliessend zeigen wir Ihnen noch ein zweites Beispiel, bei dem sowohl ein Fehler aufgetreten ist, als auch das Wissen fehlt:

\footnotesize\begin{verbatim}

   > parse Isac.thy "a + ";

      *** Inner syntax error: unexpected end of input

      *** Expected tokens: "contains_root" "is_root_free" "q_" "M_b" "M_b'"

      *** "Integral" "differentiate" "E_" "some_of" "||" "|||" "argument_in"

      *** "filter_sameFunId" "I__" "letpar" "Rewrite_Inst" "Rewrite_Set"

      *** "Rewrite_Set_Inst" "Check_elementwise" "Or_to_List" "While" "Script"

      *** "\\" "\\" "\\" "CHR" "xstr" "SOME" "\\" "@"

      *** "GREATEST" "[" "[]" "num" "\\" "{)" "{.." "\\" "(|"

      *** "\\" "SIGMA" "()" "\\" "PI" "\\" "\\" "{" "INT"

      *** "UN" "{}" "LEAST" "\\" "0" "1" "-" "!" "?" "?!" "\\"

      *** "\\" "\\" "\\!" "THE" "let" "case" "~" "if" "ALL"

      *** "EX" "EX!" "!!" "_" "\\" "\\" "PROP" "[|" "OFCLASS"

      *** "\\" "op" "\\" "%" "TYPE" "id" "longid" "var" "..."

      *** "\\" "("

      val it = None : Thm.cterm Library.option

\end{verbatim}

Das mathematische Wissen w\"achst mit jeder Theorie von ProtoPure bis Isac. In den folgenden Beispielen wird gezeigt, wie das Wissen w\"achst.

{\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`` und ''None`` bedeuten, dass ein Fehler aufgetreten ist, denn das Wissen \"uber {\tt *} findet sich erst in der {\tt theorie group}.

{\footnotesize\begin{verbatim}

   > (*-2-*);

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

      val it = None : Thm.cterm Library.option               

\end{verbatim}

Hier wiederum ist noch kein Wissen \"uber das Differenzieren vorhanden.

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

Die letzen drei Aufgaben k\"onnen schon gel\"ost werden, da {\tt Rational.thy} \"uber das n\"otige Wissen verf\"ugt.

\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, der 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`` (= das vom Computer Ausgegebene) nicht sichtbar sein, kann man mit einem bestimmten Befehl alles angezeigt werden.

{\footnotesize\begin{verbatim}

   > print_depth;

      val it = fn : int -> unit

 \end{verbatim}

Zuerst gibt man den Befehl ein, danach den Term, der gr\"osser werden soll. Dabei kann man selbst einen Wert f\"ur die L\"ange bestimmen.

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

\paragraph{Versuchen Sie es!}

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{Was ist Rewriting?}

Bei Rewriting handelt es sich um das Umformen von Termen nach vorgegebenen Regeln. Folgende zwei Funktionen sind notwendig:

\footnotesize\begin{verbatim}

   > rewrite;

      val it = fn

      :

      theory' ->

      rew_ord' ->

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

\end{verbatim}

Die Funktion hat zwei Argumente, die mitgeschickt werden m\"ussen, damit die Funktion arbeiten kann. Das letzte Element {\tt (cterm' * cterm' list) Library.option} im unteren Term ist das Ergebnis, das die Funktionen {\tt rewrite} zur\"uckgeben und die zwei vorhergehenden Argumente, {\tt theorem} und {\tt cterm}, sind die f\"ur uns wichtigen. {\tt Theorem} ist die Rechenregel und {\tt cterm} jene Formel auf die die Rechenregel angewendet wird.

\footnotesize\begin{verbatim}

   > rewrite_inst;

      val it = fn

      :

      theory' ->

      rew_ord' ->

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

\end{verbatim}

Die Funktion {\tt rewrite\_inst} wird ben\"otigt, um Gleichungen, Rechnungen zum Differenzieren etc. zu l\"osen. Dabei wird die gebundene Variable (bdv) instanziiert, d.h. es wird die Variable angegeben, nach der man differenzieren will, bzw. f\"ur die ein Wert bei einer Gleichung herauskommen soll.

Um zu sehen wie der Computer vorgeht nehmen wir folgendes Beispiel, dessen Ergebnis offenbar 0 ist, was der Computer jedoch erst nach einer Reihe von Schritten herausfindet.

Im Beispiel wird differenziert, wobei \isac's Schreibweise jene von Computer Algebra Systemen (CAS) anzugleichen: in CAS wird differenziert mit $\frac{d}{dx}\; x^2 + 3 \cdot x + 4$, in \isac{} mit {\tt d\_d x (x \^{ }\^{ }\^{ } 2 + 3 * x + 4)}.

Zuerst werden die einzelnen Werte als Variablen gespeichert:

\footnotesize\begin{verbatim}

   > val thy' = "Diff.thy";

      val thy' = "Diff.thy" : string

   > val ro = "tless_true";

      val ro = "tless_true" : string

   > val er = "eval_rls";

      val er = "eval_rls" : string

   > val inst = [("bdv","x::real")];

      val inst = [("bdv", "x::real")] : (string * string) list

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

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

\end{verbatim}

Nun wird die Rechnung nach den Regeln ausgerechnet, wobei am Ende mehrere Dinge zugleich gemacht werden.

Folgende Regeln werden ben\"otigt: Summenregel, Produktregel, Multiplikationsregel mit einem konstanten Faktor und zum Schluss die Additionsregel.

\footnotesize\begin{verbatim}

   > val Some (ct,_) = rewrite_inst thy' ro er true inst ("diff_sum","") ct;

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

   > val Some (ct,_) = rewrite_inst thy' ro er true inst ("diff_prod","") ct;

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

   > val Some (ct,_) = rewrite_inst thy' ro er true inst ("diff_const","") ct;

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

   > val Some (ct,_) = rewrite_inst thy' ro er true inst ("diff_const","") ct;

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

   > val Some (ct,_) = rewrite_inst thy' ro er true inst ("diff_const","") ct;

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

   > val Some (ct,_) = rewrite_set thy' true "make_polynomial" ct;

      val ct = "0" : string

\end{verbatim}

Was {\tt rewrite\_set} genau macht, finden Sie im n\"achsten Kapitel.

Dies w\"are ein etwas ernsthafteres Beispiel zum Differenzieren:

\footnotesize\begin{verbatim}

   > val ct = "d_d x (x ^^^ 2 + 3 * x + 4)";

   > val Some (ct,_) = rewrite_inst thy' ro er true inst ("diff_sum","") ct;

\end{verbatim}

Versuchen Sie es, diese Beispiel zu Ende zu f\"uhren! Die Regeln, die \isac{} kennt und zum Umformen verwenden kann, finden Sie auf

$ http://www.ist.tugraz.at/projects/isac/www/kbase/thy/thy_isac_Diff.html$.

\paragraph{Versuchen Sie es!} wenn Sie sich noch weitere Beispiele ansehen wollen, dann besuchen sie bitte die folgende Site: {\tt [isac-src]/tests/\dots}.

\section{Was kann Rewriting?}

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

{\tt rewrite\_ set} wandelt Terme in ein ganzes rule set um, die normalerweise nur mit einem Theorem vereinfacht dargestellt werden.

Hierbei werden auch folgende Argumente verwendet:\\

\tabcolsep=4mm

\def\arraystretch{1.5}

\begin{tabular}{lp{11.0cm}}

{\tt theory} & Die Theory von Isabelle, die alle n\"otigen Informationen f\"ur das Parsing {\tt term} enth\"alt. \\

{\tt rew\_ord}& die Ordnung f\"ur das geordnete Rewriting. F\"ur {\em no} ben\"otigt das geordnete Rewriting {\tt tless\_true}, eine Ordnung, die f\"ur alle nachgiebigen Argumente true ist \\

{\tt rls} & Das rule set; zur Auswertung von bestimmten Bedingungen in {\tt thm} falls {\tt thm} eine conditional rule ist \\

{\tt bool} & ein Bitschalter, der die Berechnungen der m\"oglichen condition in {\tt thm} ausl\"ost: wenn sie {\tt false} ist, dann wird die condition bewertet und auf Grund des Resultats wendet man {\tt thm} an, oder nicht; wenn {\tt true} dann wird die condition nicht ausgewertet, aber man gibt sie in eine Menge von Hypothesen \\

{\tt thm} & das theorem versucht den {\tt term} zu \"uberschreiben \\

{\tt term} & {\tt thm} wendet Rewriting m\"oglicherweise auf den Term an \\

\end{tabular}\\

\footnotesize\begin{verbatim}

   > rewrite_set;

      val it = fn : theory' -> bool -> rls' -> ...

\end{verbatim}

\footnotesize\begin{verbatim}

   > rewrite_set_inst;

      val it = fn : theory' -> bool -> subs' -> .

\end{verbatim}

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

\footnotesize\begin{verbatim}

   > trace_rewrite := true;

      val it = () : unit

\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 rule set 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 das 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}

\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\"ur Probleme zu finden.

\section{Beispiel f\"ur Termordnungen}

Es ist nicht unbedeutend, eine Verbindung zu Termen herzustellen, die wirklich eine Ordnung besitzen. Diese Ordnungen sind selbstaufrufende Bahnordnungen:

{\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.

{\section{Geordnetes Rewriting}}

Beim Rewriting entstehen Probleme, die vom ''law of commutativity`` (= Kommutativgesetz) durch '+' und '*' verursacht werden. Diese Probleme k\"onnen nur durch geordnetes Rewriting gel\"ost werden, da hier ein Term nur umgeschrieben wird, wenn ein kleinerer dadurch entsteht.

\chapter{Problem hierachy}

\section{''Matching``}

Matching ist eine Technik von Rewriting, die von \isac{} verwendet wird, um ein Problem und den passenden problem type daf\"ur zu finden. Die folgende Funktion \"uberpr\"uft, ob Matching m\"oglich ist:

{\footnotesize\begin{verbatim}

> matches;

val it = fn : Theory.theory -> Term.term -> Term.term -> bool

\end{verbatim}

Die folgende Gleichung wird in Operatoren und freie Variablen zerlegt.

{\footnotesize\begin{verbatim}

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

val t =

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

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

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

(Const

("Atools.pow",

"[RealDef.real, RealDef.real] => RealDef.real") $

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

Free ("1", "RealDef.real") : Term.term

\end{verbatim}

Nun wird ein Modell erstellt, das sich nicht auf bestimmte Zahlen bezieht, sondern nur eine generelle Zerlegung durchf\"uhrt.

{\footnotesize\begin{verbatim}

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

val p =

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

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

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

(Const

("Atools.pow",

"[RealDef.real, RealDef.real] => RealDef.real") $

Free ("b", "RealDef.real") $ Free ("2", "RealDef.real"))) $

Free ("c", "RealDef.real") : Term.term

\end{verbatim}

Dieses Modell enth\"alt sogenannte \textit{scheme variables}.

{\footnotesize\begin{verbatim}

> atomt p;

"*** -------------"

"*** Const (op =)"

"*** . Const (op *)""*** . . Free (a, )"

"*** . . Const (Atools.pow)"

"*** . . . Free (b, )"

"*** . . . Free (2, )"

"*** . Free (c, )"

"\n"

val it = "\n" : string

\end{verbatim}

Das Modell wird durch den Befehl \textit{free2var} erstellt.

{\footnotesize\begin{verbatim}

> free2var;

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

> val pat = free2var p;

val pat =

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

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

Var (("a", 0), "RealDef.real") $

(Const

("Atools.pow",

"[RealDef.real, RealDef.real] => RealDef.real") $

Var (("b", 0), "RealDef.real") $

Free ("2", "RealDef.real"))) $ Var (("c", 0), "RealDef.real")

: Term.term

> Sign.string_of_term (sign_of thy) pat;

val it = "?a * ?b ^^^ 2 = ?c" : string

\end{verbatim}

Durch \textit{atomt pat} wird der Term aufgespalten und in eine Form gebracht, die f\"ur die weiteren Schritte ben\"otigt wird.

{\footnotesize\begin{verbatim}

> atomt pat;

"*** -------------"

"*** Const (op =)"

"*** . Const (op *)"

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

"*** . . Const (Atools.pow)"

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

"*** . . . Free (2, )"

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

"\n"

val it = "\n" : string

\end{verbatim}

Jetzt kann das Matching an den beiden vorigen Terme angewendet werden.

{\footnotesize\begin{verbatim}

> matches thy t pat;

val it = true : bool

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

val t2 =

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

(Const

("Atools.pow",

"[RealDef.real, RealDef.real] => RealDef.real") $

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

Free ("1", "RealDef.real") : Term.term

> matches thy t2 pat;

val it = false : bool

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

val pat2 =

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

(Const

("Atools.pow",

"[RealDef.real, RealDef.real] => RealDef.real") $

Var (("u", 0), "RealDef.real") $ Free ("2", "RealDef.real")) $

Var (("v", 0), "RealDef.real") : Term.term

> matches thy t2 pat2;

val it = true : bool

\end{verbatim}

\section{Zugriff auf die hierachy}

Man verwendet folgenden Befehl, um sich Zugang zur hierachy von problem type zu verschaffen.

{\footnotesize\begin{verbatim}

> show_ptyps;

val it = fn : unit -> unit

> show_ptyps();

[

["e_pblID"],

["simplification", "polynomial"],

["simplification", "rational"],

["vereinfachen", "polynom", "plus_minus"],

["vereinfachen", "polynom", "klammer"],

["vereinfachen", "polynom", "binom_klammer"],

["probe", "polynom"],

["probe", "bruch"],

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

["equation", "univariate", "root", "sq", "rat"],

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

["equation", "univariate", "rational"],

["equation", "univariate", "polynomial", "degree_0"],

["equation", "univariate", "polynomial", "degree_1"],

["equation", "univariate", "polynomial", "degree_2", "sq_only"],

["equation", "univariate", "polynomial", " 

 degree_2", "bdv_only"],

["equation", "univariate", "polynomial", "degree_2", "pqFormula"],

["equation", "univariate", "polynomial", "degree_2", "abcFormula"],

["equation", "univariate", "polynomial", "degree_3"],

["equation", "univariate", "polynomial", "degree_4"],

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

["equation", "univariate", "expanded", "degree_2"],

["equation", "makeFunctionTo"],

["function", "derivative_of", "named"],

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

["function", "make", "by_explicit"],

["function", "make", "by_new_variable"],

["function", "integrate", "named"],

["tool", "find_values"],

["system", "linear", "2x2", "triangular"],

["system", "linear", "2x2", "normalize"],

["system", "linear", "3x3"],

["system", "linear", "4x4", "triangular"],

["system", "linear", "4x4", "normalize"],

["Biegelinien", "

MomentBestimmte"],

["Biegelinien", "MomentGegebene"],

["Biegelinien", "einfache"],

["Biegelinien", "QuerkraftUndMomentBestimmte"],

["Biegelinien", "vonBelastungZu"],

["Biegelinien", "setzeRandbedingungen"],

["Berechnung", "numerischSymbolische"],

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

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

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

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

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

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

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

]

val it = () : unit

\end{verbatim}

\section{Die passende ''formalization`` f\"ur den problem type}

Eine andere Art des Matching ist es die richtige ''formalization`` zum jeweiligen problem type zu finden. Wenn eine solche vorhanden ist, kann \isac{} selbstst\"andig die Probleme l\"osen.

\section{''problem-refinement``}

Will man die problem hierachy (= ) aufstellen, so ist darauf zu achten, dass man die verschiedenen Branches so konstruiert, dass das problem-refinement automatisch durchgef\"uhrt werden kann.

{\footnotesize\begin{verbatim}

> refine;

val it = fn : fmz_ -> pblID -> SpecifyTools.match list

> val fmz = ["equality (sqrt(9 + 4 * x)=sqrt x 

+ sqrt (5 + x))",

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

# "solutions L"];

val fmz =

["equality (sqrt(9 + 4 * x)=sqrt x + sqrt (5 + x))", "soleFor x",

"errorBound (eps=0)", ...] : string list

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

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

*** comp_dts: ??.empty $ soleFor x

Exception- ERROR raised

\end{verbatim}

Wenn die ersten zwei Regeln nicht angewendet werden k\"onnen, kommt die dritte zum Einsatz:

{\footnotesize\begin{verbatim}

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

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

# "solutions L"];

val fmz = ["equality (x + 1 = 2)", "solveFor x", "errorBound (eps=0)", ...]

: string list

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

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

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

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

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

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

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

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

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

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

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

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

val it =

[Matches

(["univariate", "equation"],

{Find = [Correct "solutions L"], With = [...], ...}),

NoMatch (["linear", "univariate", ...], {Find = [...], ...}),

NoMatch (["root", ...], ...), ...] : SpecifyTools.match list

\end{verbatim}

Der problem type wandelt $x + 1 = 2$ in die normale Form $-1 + x = 0$ um. Diese Suche nach der jeweiligen problem hierachy kann mit Hilfe eines ''proof state`` durchgef\"uhrt werden (siehe n\"achstes Kapitel).

\chapter{''Methods``}

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

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

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

\section{\"Uberpr\"ufung der Auswertung}

Das Kontrollsystem arbeitet mit den folgenden Script-Ausdr\"ucken, die {\it tacticals} genannt werden:

\begin{description}

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

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

\end{description}

W\"ahrend die genannten Befehle das Kontrollsystem durch Auswertung der Formeln ausl\"osen, h\"angen die anderen von der Anwendbarkeit der Formel in den entsprechenden Unterbegriffen ab:

\begin{description}

\item{{\tt Repeat} expr id}

\item{{\tt Try} expr id}

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

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

\item xxx

\end{description}

\chapter{Befehle von \isac{}}

In diesem Kapitel werden alle schon zur Verf\"ugung stehenden Schritte aufgelistet. Diese Liste kann sich auf Grund von weiteren Entwicklungen von \isac{} noch \"andern.\

\newline\linebreak \textbf{Init\_Proof\_Hid (dialogmode, formalization, specifictaion)} gibt die eingegebenen Befehle an die mathematic engine weiter, wobei die beiden letzten Begriffe die Beispiele automatisch speichern. Es ist nicht vorgesehen, dass der Sch\"uler tactic verwendet.\

\newline\linebreak \textbf{Init\_Proof} bildet mit einem ''proof tree`` ein leeres Modell.\

\newline\linebreak \textbf{Model\_Problem problem} bestimmt ein problemtype, das wom\"oglich in der ''hierachy`` gefunden wurde, und verwendet es f\"ur das Umformen.\

\newline\linebreak \textbf{Add\_Given, Add\_Find, Add\_Relation formula} f\"ugt eine Formel in ein bestimmtes Feld eines Modells ein. Dies ist notwendig, solange noch kein Objekt f\"ur den Benutzer vorhanden ist, in dem man die Formel eingeben kann, und nicht die gew\"unschte tactic und Formel von einer Liste w\"ahlen will.\

\newline\linebreak \textbf{Specify\_Theorie theory, Specify\_Problem proble, Specify\_Method method} gibt das entsprechende Element des Basiswissens an.\

\newline\linebreak \textbf{Refine\_Problem problem} sucht nach einem Problem in der hierachy, das auf das vorhandene zutrifft.\

\newline\linebreak \textbf{Apply\_Method method} beendet das Modell und die Beschreibung. Danach wird die L\"osungmeldung ge\"offnet.\

\newline\linebreak \textbf{Free\_Solve} beginnt eine L\"osungsmeldung ohne die Hilfe einer method.\

\newline\linebreak \textbf{Rewrite theorem} bef\"ordert ein theorem in die aktuelle Formel und wandelt es demenetsprechend um. Wenn dies nicht m\"oglich ist, kommt eine Meldung mit ''error``.\

\newline\linebreak \textbf{Rewrite\_Asm theorem} hat die gleiche Funktion wie Rewrite, speichert jedoch eine endg\"ultige Vorraussetzung des theorems, anstatt diese zu sch\"atzen.\

\newline\linebreak \textbf{Rewrite\_Set ruleset} hat \"ahnliche Funktionen wie Rewrite, gilt aber f\"ur einen ganzen Satz von theorems, dem rule set.\

\newline\linebreak \textbf{Rewrite\_Inst (substitution, theorem), Rewrite\_Set\_Inst (substitution, rule set)} ist vergleichbar mit besonderen tactics, ersetzt aber Konstanten im theorem, bevor es zu einer Anwendung kommt.\

\newline\linebreak \textbf{Calculate operation} berechnet das Ergebnis der Eingabe mit der aktuellen Formel (plus, minus, times, cancel, pow, sqrt).\

\newline\linebreak \textbf{Substitute substitution} f\"ugt der momentanen Formel {\tt substitution} hinzu und wandelt es um.\

\newline\linebreak \textbf{Take formula} startet eine neue Reihe von Rechnungen in den Formeln, wo sich schon eine andere Rechnung befindet.\

\newline\linebreak \textbf{Subproblem (theory, problem)} beginnt ein subproblem innerhalb einer Rechnung.\

\newline\linebreak \textbf{Function formula} ruft eine Funktion auf, in der der Name in der Formel enthalten ist. ???????\

\newline\linebreak \textbf{Split\_And, Conclude\_And, Split\_Or, Conclude\_Or, Begin\_Trans, End\_Trans, Begin\_Sequ, End\_Sequ, Split\_Intersect, End\_Intersect} betreffen den Bau einzelner branches des proof trees. Normalerweise werden sie vom dialog guide verdr\"angt.\

\newline\linebreak \textbf{Check\_elementwise assumption} wird in Bezug auf die aktuelle Formel verwendet, die Elemente in einer Liste enth\"alt.\

\newline\linebreak \textbf{Or\_to\_List} wandelt eine Verbindung von Gleichungen in eine Liste von Gleichungen um.\

\newline\linebreak \textbf{Check\_postcond} \"uberpr\"uft die momentane Formel im Bezug auf die Nachbedinung beim Beenden des subproblem.\

\newline\linebreak \textbf{End\_Proof} beendet eine \"Uberpr\"ufung und gibt erst dann ein Ergebnis aus, wenn Check\_postcond erfolgreich abgeschlossen wurde.

\section{Die Funktionsweise der mathematic engine}

Ein proof (= Beweis) wird in der mathematic engine me von der tactic {\tt Init\_Proof} gestartet und wird wechselwirkend mit anderen tactics vorangebracht. Auf den input (= das, was eingegeben wurde) einzelner tactics folgt eine Formel, die von der me ausgegeben wird, und die darauf folgende tactic gilt. Der proof ist beendet, sobald die me {\tt End\_Proof} als n\"achste tactic vorschl\"agt.

\newline Im Anschluss werden Sie einen Rechenbeweis sehen, der von der L\"osung einer Gleichung (= equation) handelt, bei der diese automatisch differenziert wird. 

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

\section{Der Beginn einer Rechnung}

Der proof state wird von einem proof tree und einer position ausgegeben. Beide sind zu Beginn leer. Die tactic {\tt Init\_Proof} ist, wie alle anderen tactics auch, an einen string gekoppelt. Um einen neuen proof beginnen zu k\"onnen, werden folgende Schritte durchgef\"uhrt:

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

Die mathematics engine gibt etwas mit dem type {\tt mout} aus, was in unserem Fall ein Problem darstellt. Sobald mehr angezeigt wird, m\"usste dieses jedoch gel\"ost sein.

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

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

\section{The phase of modeling}

Dieses Kapitel besch\"aftigt sich mit dem input der Einzelheiten bei einem Problem. Die me kann dabei helfen, wenn man die formalization durch {\tt Init\_Proof} darauf hinweist. Normalerweise weiss die mathematics engine die n\"achste gute tactic.

{\footnotesize\begin{verbatim}

?????????????????????????????????????????????????????????????????????????????????????????????

   ML>  nxt;

   val it =

     ("Add_Given",Add_Given "equality ((x + #1) * (x + #2) = x ^^^ #2 + #8)")

     : string * mstep

   ML>

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

   val nxt = ("Add_Given",Add_Given "solveFor x") : string * mstep

   ML>

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

   val nxt = ("Add_Find",Add_Find "solutions L") : string * mstep

   ML>

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

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

\end{verbatim}

{\footnotesize\begin{verbatim}

?????????????????????????????????????????????????????????????????????????????????????????????

   ML>  Compiler.Control.Print.printDepth:=8;

   ML>  f;

   val it =

     Form'

       (PpcKF

          (0,EdUndef,0,Nundef,

           (Problem [],

            {Find=[Correct "solutions L"],

             Given=[Correct "equality ((x + #1) * (x + #2) = x ^^^ #2 + #8)",

                    Correct "solveFor x"],Relate=[],Where=[],With=[]}))) : mout

\end{verbatim}

\section{The phase of specification}

Diese phase liefert eindeutige Bestimmungen einer domain, den problem type und die method damit man sie verwenden kann. F\"ur gew\"ohnlich wird die Suche nach dem richtigen problem type unterst\"utzt. Dazu sind zwei tactics verwendbar: {\tt Specify\_Problem} entwickelt ein Feedback, wie ein problem type bei dem jetzigen problem zusammenpasst und {\tt Refine\_Problem} stellt Hilfe durch das System bereit, falls der Benutzer die \"Ubersicht verliert.

{\footnotesize\begin{verbatim}

??????????????????????????????????????????????????????????????????????????????????????????

   ML> nxt;

   val it = ("Specify_Domain",Specify_Domain "SqRoot.thy") : string * mstep

   ML>

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

   val nxt =

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

     : string * mstep

   val pt =

     Nd

       (PblObj

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

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

\end{verbatim}

Die me erkennt den richtigen Problem type und arbeitet so weiter:

{\footnotesize\begin{verbatim}

?????????????????????????????????????????????????????????????????????????????????????????

   ML> val nxt = ("Specify_Problem",

               Specify_Problem ["polynomial","univariate","equation"]);

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

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

   val nxt =

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

     : string * mstep

   ML>

   ML> val nxt = ("Specify_Problem",

               Specify_Problem ["linear","univariate","equation"]);

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

   val f =

     Form'

       (PpcKF

          (0,EdUndef,0,Nundef,

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

            {Find=[Correct "solutions L"],

             Given=[Correct "equality ((x + #1) * (x + #2) = x ^^^ #2 + #8)",

                    Correct "solveFor x"],Relate=[],

             Where=[False

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

             With=[]}))) : mout 

\end{verbatim}

Wir nehmen wieder an, dass der dialog guide die n\"achsten tactics, veranlasst von der mathematic engine, versteckt und der Sch\"uler Hilfe ben\"otigt. Dann muss {\tt Refine\_Problem} angewandt werden. Dieser Befehl findet immer den richtigen Weg, wenn man es auf den problem type bezieht [''univariate``, ''equation``].

{\footnotesize\begin{verbatim}

????????????????????????????????????????????????????????????????????????????????????????????

   ML> val nxt = ("Refine_Problem",

                  Refine_Problem ["linear","univariate","equation

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

   val f = Problems (RefinedKF [NoMatch #]) : mout

   ML>

   ML>  Compiler.Control.Print.printDepth:=9;f;Compiler.Control.Print.printDepth:=4;

   val f =

     Problems

       (RefinedKF

          [NoMatch

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

              {Find=[Correct "solutions L"],

               Given=[Correct "equality ((x + #1) * (x + #2) = x ^^^ #2 + #8)",

                      Correct "solveFor x"],Relate=[],

               Where=[False

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

               With=[]})]) : mout

   ML>

   ML> val nxt = ("Refine_Problem",Refine_Problem ["univariate","equation"]);

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

   val f =

     Problems

       (RefinedKF [Matches #,NoMatch #,NoMatch #,NoMatch #,NoMatch #,Matches #])

     : mout

   ML>

   ML>

   ML>  Compiler.Control.Print.printDepth:=9;f;Compiler.Control.Print.printDepth:=4;

   val f =