
ahirn@37877: \documentclass[11pt,a4paper,headline,headcount,towside,nocenter]{report}
ahirn@37877: \usepackage{latexsym} 
alexandra@37882: 
ahirn@37877: %\usepackage{ngerman}
ahirn@37877: %\grmn@dq@error ...and \dq \string #1 is undefined}
ahirn@37877: %l.989 ...tch the problem type \\{\tt["squareroot",
ahirn@37877: %                                                  "univ
ahirn@37877: \bibliographystyle{alpha}
ahirn@37877: 
ahirn@37877: \def\isac{${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$}
ahirn@37877: 
ahirn@37877: \title{\isac --- Interface for\\
ahirn@37877:   Developers of Math Knowledge\\[1.0ex]
ahirn@37877:   and\\[1.0ex]
ahirn@37877:   Tools for Experiments in\\
ahirn@37877:   Symbolic Computation\\[1.0ex]}
ahirn@37877: \author{The \isac-Team\\
ahirn@37877:   \tt isac-users@ist.tugraz.at\\[1.0ex]}
ahirn@37877: \date{\today}
ahirn@37877: 
ahirn@37877: \begin{document}
ahirn@37877: \maketitle
ahirn@37877: \newpage
ahirn@37877: \tableofcontents
ahirn@37877: \newpage
ahirn@37877: \listoftables
ahirn@37877: \newpage
ahirn@37877: 
alexandra@37887: \chapter{Einleitung}
ahirn@37877: \section{``Authoring'' und ``Tutoring''}
ahirn@37877: {TO DO} Mathematik lernen -- verschiedene Autoren -- Isabelle
ahirn@37877: 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.
ahirn@37877: \section{Der Inhalt des Dokuments}
ahirn@37877: \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.
ahirn@37877: 
ahirn@37877: \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.
ahirn@37877: 
ahirn@37877: Das Dokument ist eigenst\"andig; Basiswissen \"uber SML (für eine Einf\"uhrung siehe \cite{Paulson:91}), Terme und Umschreibung wird vorrausgesetzt.
ahirn@37877: 
ahirn@37877: %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.
ahirn@37877: 
ahirn@37877: Hinweis: SML Code, Verzeichnis, Dateien sind {\tt in 'tt' geschrieben}; besonders in {\tt ML>} ist das Kerngebiet schnell.
ahirn@37877: 
ahirn@37877: \paragraph{Versuchen Sie es!}  Ein weiteres Anliegen dieses Textes ist, dem Leser Tipps f\"ur Versuche mit den Anwendungen zu geben.
ahirn@37877: 
ahirn@37877: \section{Gleich am Computer ausprobieren!}\label{get-started}
ahirn@37877: \paragraph{TO DO screenshot} Bevor Sie mit Ihren Versuchen beginnen, m\"ochten wir Ihnen noch einige Hinweise geben.
ahirn@37877: \begin{itemize}
ahirn@37877:  \item System starten
ahirn@37877:  \item Shell aufmachen und die Datei mat-eng-de.sml \"offnen.
ahirn@37877:  \item $>$  :  Hinter diesem Zeichen (``Prompt'') stehen jene, die Sie selbst eingeben bzw. mit Copy und Paste aus der Datei kopieren.
ahirn@37877:  \item Die Eingabe wird mit ``;'' und ``Enter'' abgeschlossen.
ahirn@37877:  \item Zeilen, die nicht mit Prompt beginnen, werden vom Computer ausgegeben.
ahirn@37877:  
ahirn@37877: \end{itemize}
ahirn@37877: 
ahirn@37877: \part{Experimentelle Ann\"aherung}
ahirn@37877: 
ahirn@37877: \chapter{Terme und Theorien}
ahirn@37877: 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.
ahirn@37877: 
ahirn@37877: \section{Von der Formel zum Term}
ahirn@37877: Um ein Beispiel zu nennen: Die Formel $a+b\cdot 3$ l\"asst sich in lesbarer Form so eingeben:
ahirn@37877: {\footnotesize\begin{verbatim}
ahirn@37877:   > "a + b * 3";
ahirn@37877:   val it = "a + b * 3" : string
ahirn@37877: \end{verbatim}}
ahirn@37877: \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:
ahirn@37877: {\footnotesize\begin{verbatim}
ahirn@37877:   > str2term "a + b * 3";
ahirn@37877:   val it =
ahirn@37877:      Const ("op +", "[RealDef.real, RealDef.real] => RealDef.real") $
ahirn@37877:            Free ("a", "RealDef.real") $
ahirn@37877:         (Const ("op *", "[RealDef.real, RealDef.real] => RealDef.real") $ ... $
ahirn@37877:            ...) : Term.term
ahirn@37877: \end{verbatim}}
ahirn@37877: \noindent Jene Form braucht Isabelle intern zum rechnen. Sie heisst Term und ist nicht lesbar, daf\"ur aber speicherbar mit Hilfe von ``val'' (=value) 
ahirn@37877: {\footnotesize\begin{verbatim}
ahirn@37877:   > val term = str2term "a + b * 3";
ahirn@37877:   val term =  
ahirn@37877:      Const ("op +", "[RealDef.real, RealDef.real] => RealDef.real") $
ahirn@37877:            Free ("a", "RealDef.real") $
ahirn@37877:         (Const ("op *", "[RealDef.real, RealDef.real] => RealDef.real") $ ... $
ahirn@37877:            ...) : Term.term
ahirn@37877: \end{verbatim}
ahirn@37877: Der gespeicherte Term kann einer Funktion ``atomty'' \"ubergeben werden, die jenen in einer abstrakten Struktur zeigt:
ahirn@37877: {\footnotesize\begin{verbatim}
ahirn@37877:   > atomty term;
ahirn@37877:  
ahirn@37877:   ***
ahirn@37877:   *** Const (op +, [real, real] => real)
ahirn@37877:   *** . Free (a, real)
ahirn@37877:   *** . Const (op *, [real, real] => real)
ahirn@37877:   *** . . Free (b, real)
ahirn@37877:   *** . . Free (3, real)
ahirn@37877:   ***
ahirn@37877:  
ahirn@37877:   val it = () : unit
ahirn@37877: \end{verbatim}%size
ahirn@37877: 
ahirn@37877: 
ahirn@37877: \section{``Theory'' und ``Parsing``}
ahirn@37877: 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{}. 
ahirn@37877: 
ahirn@37877: {\footnotesize\begin{verbatim}
ahirn@37877:   > Isac.thy;
ahirn@37877:        val it =
ahirn@37877:           {ProtoPure, CPure, HOL, Set, Typedef, Fun, Product_Type, Lfp, Gfp,
ahirn@37877:           Sum_Type, Relation, Record, Inductive, Transitive_Closure,
ahirn@37877:           Wellfounded_Recursion, NatDef, Nat, NatArith, Divides, Power,
ahirn@37877:           SetInterval, Finite_Set, Equiv, IntDef, Int, Datatype_Universe,
ahirn@37877:           Datatype, Numeral, Bin, IntArith, Wellfounded_Relations, Recdef, IntDiv,
ahirn@37877:           IntPower, NatBin, NatSimprocs, Relation_Power, PreList, List, Map,
ahirn@37877:           Hilbert_Choice, Main, Lubs, PNat, PRat, PReal, RealDef, RealOrd,
ahirn@37877:           RealInt, RealBin, RealArith0, RealArith, RComplete, RealAbs, RealPow,
ahirn@37877:           Ring_and_Field, Complex_Numbers, Real, ListG, Tools, Script, Typefix,
ahirn@37877:           Float, ComplexI, Descript, Atools, Simplify, Poly, Rational, PolyMinus,
ahirn@37877:           Equation, LinEq, Root, RootEq, RatEq, RootRat, RootRatEq, PolyEq, Vect,
ahirn@37877:           Calculus, Trig, LogExp, Diff, DiffApp, Integrate, EqSystem, Biegelinie,
ahirn@37877:           AlgEin, Test, Isac} : Theory.theory
ahirn@37877: \end{verbatim}
ahirn@37877: Die, die ein Mal enth\"alt ist groups.thy. Suchen Sie nach '*' unter der Adresse:
ahirn@37877: 
ahirn@37877: http://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/library/HOL/Groups.html
ahirn@37877: Hier wird Ihnen erkl\"art, wie das Mal vom Computer gelesen wird.
ahirn@37877: {\footnotesize\begin{verbatim}
ahirn@37877:   > Group.thy
ahirn@37877:       fixes f :: "'a => 'a => 'a" (infixl "*" 70)
ahirn@37877:       assumes assoc [ac_simps]: "a * b * c = a * (b * c)"
ahirn@37877: \end{verbatim}
ahirn@37877: 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). 
ahirn@37877: 
ahirn@37877: Parsing entsteht durch einen string und eine theory. Es verwendet Informationen, die in der theory von Isabelle enthalten sind.
ahirn@37877: {\footnotesize\begin{verbatim}
ahirn@37877:   > parse;
ahirn@37877:        val it = fn : Theory.theory -> string -> Thm.cterm Library.option
ahirn@37877: \end{verbatim}
ahirn@37877: Dieser term kann wieder in seine einzelnen Teile zerlegt werden.
ahirn@37877: {\footnotesize\begin{verbatim}
ahirn@37877:    > val it = (term_of o the) it;
ahirn@37877:         val it =
ahirn@37877:            Const ("op +", "[RealDef.real, RealDef.real] => RealDef.real") $
ahirn@37877:                Free ("a", "RealDef.real") $
ahirn@37877:            (Const ("op *", "[RealDef.real, RealDef.real] => RealDef.real") $ ... $
ahirn@37877:                ...) : Term.term
ahirn@37877: \end{verbatim}
ahirn@37877: 
ahirn@37877: \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.
ahirn@37877: 
ahirn@37877: {\footnotesize\begin{verbatim}
ahirn@37877:    > (*-1-*);
ahirn@37877:    > parse HOL.thy "2^^^3";
ahirn@37877:       *** Inner lexical error at: "^^^3"
ahirn@37877:       val it = None : Thm.cterm Library.option         
ahirn@37877: \end{verbatim}
ahirn@37877: ''Inner lexical error`` bedeutet, dass ein Fehler aufgetreten ist, vermutlich hat man sich vertippt.
ahirn@37877: 
ahirn@37877: {\footnotesize\begin{verbatim}
ahirn@37877:    > (*-2-*);
ahirn@37877:    > parse HOL.thy "d_d x (a + x)";
ahirn@37877:       val it = None : Thm.cterm Library.option               
ahirn@37877: \end{verbatim}
ahirn@37877: Fehlt ''Inner lexical error`` wurde der Parse nicht gefunden.
ahirn@37877: 
ahirn@37877: {\footnotesize\begin{verbatim}
ahirn@37877:    > (*-3-*);
ahirn@37877:    > parse Rational.thy "2^^^3";
ahirn@37877:       val it = Some "2 ^^^ 3" : Thm.cterm Library.option               
ahirn@37877: \end{verbatim}
ahirn@37877: 
ahirn@37877: {\footnotesize\begin{verbatim}
ahirn@37877:    > (*-4-*);
ahirn@37877:    > val Some t4 = parse Rational.thy "d_d x (a + x)";
ahirn@37877:       val t4 = "d_d x (a + x)" : Thm.cterm              
ahirn@37877: \end{verbatim}
ahirn@37877: 
ahirn@37877: {\footnotesize\begin{verbatim}
ahirn@37877:    > (*-5-*);
ahirn@37877:    > val Some t5 = parse Diff.thy  "d_d x (a + x)";
ahirn@37877:       val t5 = "d_d x (a + x)" : Thm.cterm             
ahirn@37877: \end{verbatim}
ahirn@37877: 
ahirn@37877: 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.
ahirn@37877: 
ahirn@37877: \section{Details von Termen}
ahirn@37877: Mit Hilfe der darunterliegenden Darstellung sieht man, dass ein cterm in einen term umgewandelt werden kann.
ahirn@37877: {\footnotesize\begin{verbatim}
ahirn@37877:    > term_of;
ahirn@37877:       val it = fn : Thm.cterm -> Term.term
ahirn@37877: \end{verbatim}
ahirn@37877: Durch die Umwandlung eines cterms in einen term sieht man die einzelnen Teile des Terms. ''Free`` bedeutet, dass man die Variable \"andern kann.
ahirn@37877: {\footnotesize\begin{verbatim}
ahirn@37877:    > term_of t4;
ahirn@37877:       val it =
ahirn@37877:          Free ("d_d", "[RealDef.real, RealDef.real] => RealDef.real") $ ... $
ahirn@37877:          ...: Term.term
ahirn@37877: 
ahirn@37877: \end{verbatim}
ahirn@37877: In diesem Fall sagt uns das ''Const``, dass die Variable eine Konstante ist, also ein Fixwert ist und immer die selbe Funktion hat.
ahirn@37877: {\footnotesize\begin{verbatim}
ahirn@37877:    > term_of t5;
ahirn@37877:       val it =
ahirn@37877:          Const ("Diff.d_d", "[RealDef.real, RealDef.real] => RealDef.real") $ ... $
ahirn@37877:          ... : Term.term
ahirn@37877: \end{verbatim}
ahirn@37877: Sollten verschiedene Teile des Output nicht sichtbar sein, kann die Schriftgr\"osse ge\"andert werden.
ahirn@37877: {\footnotesize\begin{verbatim}
ahirn@37877:    > print_depth;
ahirn@37877:       val it = fn : int -> unit
ahirn@37877:  \end{verbatim}
ahirn@37877: Zuerst gibt man die Schriftgr\"osse ein, danach den term, der gr\"osser werden soll.
ahirn@37877: {\footnotesize\begin{verbatim}
ahirn@37877:    > print_depth 10;
ahirn@37877:       val it = () : unit
ahirn@37877:    > term_of t4;
ahirn@37877:          val it =
ahirn@37877:             Free ("d_d", "[RealDef.real, RealDef.real] => RealDef.real") $
ahirn@37877:                 Free ("x", "RealDef.real") $
ahirn@37877:             (Const ("op +", "[RealDef.real, RealDef.real] => RealDef.real") $
ahirn@37877:                 Free ("a", "RealDef.real") $ Free ("x", "RealDef.real"))
ahirn@37877:          : Term.term
ahirn@37877: 
ahirn@37877:    > print_depth 10;
ahirn@37877:          val it = () : unit
ahirn@37877:    > term_of t5;
ahirn@37877:          val it =
ahirn@37877:             Const ("Diff.d_d", "[RealDef.real, RealDef.real] => RealDef.real") $
ahirn@37877:                 Free ("x", "RealDef.real") $
ahirn@37877:             (Const ("op +", "[RealDef.real, RealDef.real] => RealDef.real") $
ahirn@37877:                 Free ("a", "RealDef.real") $ Free ("x", "RealDef.real"))
ahirn@37877:          : Term.term
ahirn@37877: \end{verbatim}
ahirn@37877: 
ahirn@37877: Eine andere Variante um den Unterschied der beiden Terme zu sehen ist folgende: 
ahirn@37877: {\footnotesize\begin{verbatim}
ahirn@37877:    > (*-4-*) val thy = Rational.thy;
ahirn@37877:       val thy =
ahirn@37877:          {ProtoPure, CPure, HOL, Set, Typedef, Fun, Product_Type, Lfp, Gfp,
ahirn@37877:          Sum_Type, Relation, Record, Inductive, Transitive_Closure,
ahirn@37877:          Wellfounded_Recursion, NatDef, Nat, NatArith, Divides, Power,
ahirn@37877:          SetInterval, Finite_Set, Equiv, IntDef, Int, Datatype_Universe,
ahirn@37877:          Datatype, Numeral, Bin, IntArith, Wellfounded_Relations, Recdef, IntDiv,
ahirn@37877:          IntPower, NatBin, NatSimprocs, Relation_Power, PreList, List, Map,
ahirn@37877:          Hilbert_Choice, Main, Lubs, PNat, PRat, PReal, RealDef, RealOrd,
ahirn@37877:          RealInt, RealBin, RealArith0, RealArith, RComplete, RealAbs, RealPow,
ahirn@37877:          Ring_and_Field, Complex_Numbers, Real, ListG, Tools, Script, Typefix,
ahirn@37877:          Float, ComplexI, Descript, Atools, Simplify, Poly, Rational}
ahirn@37877:      : Theory.theory
ahirn@37877:    > ((atomty) o term_of o the o (parse thy)) "d_d x (a + x)";
ahirn@37877:  
ahirn@37877:       ***
ahirn@37877:       *** Free (d_d, [real, real] => real)
ahirn@37877:       *** . Free (x, real)
ahirn@37877:       *** . Const (op +, [real, real] => real)
ahirn@37877:       *** . . Free (a, real)
ahirn@37877:       *** . . Free (x, real)
ahirn@37877:       ***
ahirn@37877:  
ahirn@37877:       val it = () : unit
ahirn@37877: 
ahirn@37877: 
ahirn@37877:    > (*-5-*) val thy = Diff.thy;
ahirn@37877:       val thy =
ahirn@37877:          {ProtoPure, CPure, HOL, Set, Typedef, Fun, Product_Type, Lfp, Gfp,
ahirn@37877:          Sum_Type, Relation, Record, Inductive, Transitive_Closure,
ahirn@37877:          Wellfounded_Recursion, NatDef, Nat, NatArith, Divides, Power,
ahirn@37877:          SetInterval, Finite_Set, Equiv, IntDef, Int, Datatype_Universe,
ahirn@37877:          Datatype, Numeral, Bin, IntArith, Wellfounded_Relations, Recdef, IntDiv,
ahirn@37877:          IntPower, NatBin, NatSimprocs, Relation_Power, PreList, List, Map,
ahirn@37877:          Hilbert_Choice, Main, Lubs, PNat, PRat, PReal, RealDef, RealOrd,
ahirn@37877:          RealInt, RealBin, RealArith0, RealArith, RComplete, RealAbs, RealPow,
ahirn@37877:          Ring_and_Field, Complex_Numbers, Real, Calculus, Trig, ListG, Tools,
ahirn@37877:          Script, Typefix, Float, ComplexI, Descript, Atools, Simplify, Poly,
ahirn@37877:          Equation, LinEq, Root, RootEq, Rational, RatEq, RootRat, RootRatEq,
ahirn@37877:          PolyEq, LogExp, Diff} : Theory.theory
ahirn@37877:  
ahirn@37877:    > ((atomty) o term_of o the o (parse thy)) "d_d x (a + x)";
ahirn@37877:  
ahirn@37877:       ***
ahirn@37877:       *** Const (Diff.d_d, [real, real] => real)
ahirn@37877:       *** . Free (x, real)
ahirn@37877:       *** . Const (op +, [real, real] => real)
ahirn@37877:       *** . . Free (a, real)
ahirn@37877:       *** . . Free (x, real)
ahirn@37877:       ***
ahirn@37877:  
ahirn@37877:       val it = () : unit
ahirn@37877: \end{verbatim}
ahirn@37877: 
ahirn@37877: 
ahirn@37877: {\chapter{''Rewriting``}}
ahirn@37877: {\section{}}
ahirn@37877: 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.
ahirn@37877: 
ahirn@37877: {\footnotesize\begin{verbatim}
ahirn@37877: > rewrite_;
ahirn@37877: val it = fn
ahirn@37877: :
ahirn@37877:    Theory.theory ->
ahirn@37877:    ((Term.term * Term.term) list -> Term.term * Term.term -> bool) ->
ahirn@37877:    rls ->
ahirn@37877:    bool ->
ahirn@37877:    Thm.thm -> Term.term -> (Term.term * Term.term list) Library.option
ahirn@37877: 
ahirn@37877: > rewrite;
ahirn@37877: val it = fn
ahirn@37877: :
ahirn@37877:    theory' ->
ahirn@37877:    rew_ord' ->
ahirn@37877:    rls' -> bool -> thm' -> cterm' -> (string * string list) Library.option
ahirn@37877: 
ahirn@37877: \end{verbatim}
ahirn@37877: \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!
ahirn@37877: 
ahirn@37877: Zuerst legt man fest, dass es sich um eine Differenzierung handelt.
ahirn@37877: {\footnotesize\begin{verbatim}
ahirn@37877:    > val thy' = "Diff.thy";
ahirn@37877:       val thy' = "Diff.thy" : string
ahirn@37877: \end{verbatim}
ahirn@37877: Dann gibt man die zu l\"osende Rechnung ein.
ahirn@37877: {\footnotesize\begin{verbatim}
ahirn@37877:    > val ct = "d_d x (a + a * (2 + b))";
ahirn@37877:       val ct = "d_d x (a + a * (2 + b))" : string
ahirn@37877: \end{verbatim}
ahirn@37877: Anschließend gibt man bekannt, dass die Summenregel angewandt werden soll.
ahirn@37877: {\footnotesize\begin{verbatim}
ahirn@37877:    > val thm = ("diff_sum","");
ahirn@37877:       val thm = ("diff_sum", "") : string * string
ahirn@37877: \end{verbatim}
ahirn@37877: Schliesslich wird die erste Ableitung angezeigt.
ahirn@37877: {\footnotesize\begin{verbatim}
ahirn@37877:    > val Some (ct,_) = rewrite_inst thy' "tless_true" "eval_rls" true
ahirn@37877:                         [("bdv","x::real")] thm ct;#
ahirn@37877:       val ct = "d_d x a + d_d x (a * (2 + b))" : cterm'
ahirn@37877: \end{verbatim}
ahirn@37877: Will man auch die zweite Ableitung sehen, geht man so vor:
ahirn@37877: {\footnotesize\begin{verbatim}
ahirn@37877:    > val thm = ("diff_prod_const","");
ahirn@37877:       val thm = ("diff_prod_const", "") : string * string
ahirn@37877: \end{verbatim} 
ahirn@37877: Auch die zweite Ableitung wird sichtbar.
ahirn@37877: {\footnotesize\begin{verbatim}
ahirn@37877:    > val Some (ct,_) = rewrite_inst thy' "tless_true" "eval_rls" true
ahirn@37877:                         [("bdv","x::real")] thm ct;#
ahirn@37877:       val ct = "d_d x a + a * d_d x (2 + b)" : cterm'
ahirn@37877: \end{verbatim}
ahirn@37877: 
alexandra@37882: {\section{M\"oglichkeiten von Rewriting}
alexandra@37882: Es gibt verscheidene Varianten von Rewriting, die alle eine bestimmte Bedeutung haben.
alexandra@37882: \textit{rewrite\_inst} bedeutet, dass die Liste der Terme vor dem Rewriting durch ein ''Theorem`` (ein mathematischer Begriff f\"ur einen Satz) ersetzt wird.
alexandra@37882: {\footnotesize\begin{verbatim}
alexandra@37882: > rewrite_inst;
alexandra@37882: val it = fn
alexandra@37882: :
alexandra@37882:    theory' ->
alexandra@37882:    rew_ord' ->
alexandra@37882:    rls' ->
alexandra@37882:    bool -> 'a -> thm' -> cterm' -> (cterm' * cterm' list) Library.option
alexandra@37882: \end{verbatim}
alexandra@37882: 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.
alexandra@37882: {\footnotesize\begin{verbatim}
alexandra@37882:    > rewrite_set;
alexandra@37882:       val it = fn
alexandra@37882:       : theory' -> bool -> rls' -> cterm' -> (string * string list) Library.option
alexandra@37882: \end{verbatim}
alexandra@37882: \textit{rewrite\_set\_inst} ist eine Kombination der beiden oben genannten M\"oglichkeiten.
alexandra@37882: {\footnotesize\begin{verbatim}
alexandra@37882:    > rewrite_set_inst;
alexandra@37882:       val it = fn
alexandra@37882:       :
alexandra@37882:          theory' ->
alexandra@37882:          bool -> subs' -> rls' -> cterm' -> (string * string list) Library.option
alexandra@37882: \end{verbatim}
alexandra@37882: Wenn man sehen m\"ochte, wie Rewriting bei den einzelnen Theorems funktioniert, kann man dies mit \textit{trace\_rewrite} versuchen.
alexandra@37882: {\footnotesize\begin{verbatim}
alexandra@37882:    > toggle;
alexandra@37882:       val it = fn : bool ref -> bool
alexandra@37882:    > toggle trace_rewrite;
alexandra@37882:       val it = true : bool
alexandra@37882:    > toggle trace_rewrite;
alexandra@37882:       val it = false : bool
alexandra@37882: \end{verbatim}
alexandra@37882:  
alexandra@37882: \section{Rule sets}
alexandra@37882: 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.
alexandra@37882: 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.
alexandra@37882: Ein Beispiel f\"ur einen Regelsatz ist folgendes:
alexandra@37882: \footnotesize\begin{verbatim}
alexandra@37882: ???????????
alexandra@37882: \end{verbatim}
ahirn@37877: 
alexandra@37882: \footnotesize\begin{verbatim}
alexandra@37882:    > sym;
alexandra@37882:       val it = "?s = ?t ==> ?t = ?s" : Thm.thm
alexandra@37882:    > rearrange_assoc;
alexandra@37882:       val it =
alexandra@37882:          Rls
alexandra@37882:             {id = "rearrange_assoc",
alexandra@37882:                scr = Script (Free ("empty_script", "RealDef.real")),
alexandra@37882:                calc = [],
alexandra@37882:                erls =
alexandra@37882:                Rls
alexandra@37882:                   {id = "e_rls",
alexandra@37882:                      scr = EmptyScr,
alexandra@37882:                      calc = [],
alexandra@37882:                      erls = Erls,
alexandra@37882:                      srls = Erls,
alexandra@37882:                      rules = [],
alexandra@37882:                      rew_ord = ("dummy_ord", fn),
alexandra@37882:                      preconds = []},
alexandra@37882:                srls =
alexandra@37882:                Rls
alexandra@37882:                   {id = "e_rls",
alexandra@37882:                      scr = EmptyScr,
alexandra@37882:                      calc = [],
alexandra@37882:                      erls = Erls,
alexandra@37882:                      srls = Erls,
alexandra@37882:                      rules = [],
alexandra@37882:                      rew_ord = ("dummy_ord", fn),
alexandra@37882:                      preconds = []},
alexandra@37882:                rules =
alexandra@37882:                [Thm ("sym_radd_assoc", "?m1 + (?n1 + ?k1) = ?m1 + ?n1 + ?k1"  [.]),
alexandra@37882:                   Thm
alexandra@37882:                      ("sym_rmult_assoc",
alexandra@37882:                         "?m1 * (?n1 * ?k1) = ?m1 * ?n1 * ?k1"  [.])],
alexandra@37882:                rew_ord = ("e_rew_ord", fn),
alexandra@37882:                preconds = []} : rls
alexandra@37882: \end{verbatim}
ahirn@37877: 
ahirn@37877: 
alexandra@37882: \section{Berechnung von Konstanten}
alexandra@37882: Sobald Konstanten in dem Bereich des Subterms sind, k\"onnen sie von einer Funktion berechnet werden:
alexandra@37882: \footnotesize\begin{verbatim}
alexandra@37882:    > calculate;
alexandra@37882:       val it = fn
alexandra@37882:       :
alexandra@37882:          theory' ->
alexandra@37882:          string *
alexandra@37882:          (
alexandra@37882:          string ->
alexandra@37882:          Term.term -> Theory.theory -> (string * Term.term) Library.option) ->
alexandra@37882:          cterm' -> (string * thm') Library.option
ahirn@37877: 
alexandra@37882:    > calculate_;
alexandra@37882:       val it = fn
alexandra@37882:       :
alexandra@37882:          Theory.theory ->
alexandra@37882:          string *
alexandra@37882:          (
alexandra@37882:          string ->
alexandra@37882:          Term.term -> Theory.theory -> (string * Term.term) Library.option) ->
alexandra@37882:          Term.term -> (Term.term * (string * Thm.thm)) Library.option
alexandra@37882: \end{verbatim}
alexandra@37882: Man bekommt das Ergebnis und die Theorem bezieht sich darauf. Daher sind die folgenden mathematischen Rechnungen m\"oglich:
alexandra@37882: \footnotesize\begin{verbatim}
alexandra@37882:    > calclist;
alexandra@37882:       val it =
alexandra@37882:          [("Vars", ("Tools.Vars", fn)), ("matches", ("Tools.matches", fn)),
alexandra@37882:             ("lhs", ("Tools.lhs", fn)), ("plus", ("op +", fn)),
alexandra@37882:             ("times", ("op *", fn)), ("divide_", ("HOL.divide", fn)),
alexandra@37882:             ("power_", ("Atools.pow", fn)), ("is_const", ("Atools.is'_const", fn)),
alexandra@37882:             ("le", ("op <", fn)), ("leq", ("op <=", fn)),
alexandra@37882:             ("ident", ("Atools.ident", fn)), ("sqrt", ("Root.sqrt", fn)),
alexandra@37882:             ("Test.is_root_free", ("is'_root'_free", fn)),
alexandra@37882:             ("Test.contains_root", ("contains'_root", fn))]
alexandra@37882:       :
alexandra@37882:          (
alexandra@37882:          string *
alexandra@37882:          (
alexandra@37882:          string *
alexandra@37882:          (
alexandra@37882:          string ->
alexandra@37882:          Term.term -> Theory.theory -> (string * Term.term) Library.option))) list
alexandra@37882: \end{verbatim}
alexandra@37882: Diese werden so angewendet:
alexandra@37882: \footnotesize\begin{verbatim}
alexandra@37882: \end{verbatim}
ahirn@37877: 
ahirn@37877: 
ahirn@37877: 
alexandra@37882: \chapter{Termordnung}
alexandra@37882: 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.
alexandra@37882: 
alexandra@37882: \section{Beispiel f\"ur Termordnungen}
alexandra@37882: 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.
alexandra@37882: Hier ein Beispiel:
alexandra@37882: 
alexandra@37882: {\footnotesize\begin{verbatim}
alexandra@37882:    > sqrt_right;
alexandra@37882:       val it = fn : bool -> Theory.theory -> subst -> Term.term * Term.term -> b       ool
alexandra@37882:    > tless_true;
alexandra@37882:       val it = fn : subst -> Term.term * Term.term -> bool
alexandra@37882: \end{verbatim}
alexandra@37882: 
alexandra@37882: 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.
alexandra@37882: 
alexandra@37888: {\section{Geordnetes Rewriting}}
alexandra@37888: Beim Rewriting entstehen Probleme in den meisten elementaren Bereichen. Es gibt ein ''law of commutativity`` das genau solche Probleme mit '+' und '*' verursacht. Diese Probleme können nur durch geordnetes Rewriting gel\"ost werden, da hier ein Term nur umgeschrieben wird, wenn ein kleinerer dadurch entsteht.
alexandra@37888: \paragraph{Versuchen Sie es!} Das geordnete Rewriting ist eine Technik, um ein normales Polynom aus ganzzahligen Termen zu schaffen.
alexandra@37888: Geordnetes Rewriting endet mit Klammern, aber auf Grund der weggelassenen Verbindung.
alexandra@37888: 
alexandra@37888: 
alexandra@37888: \chapter{Die Hirarchie von Problemen}
alexandra@37888: \section{''Matching``}
alexandra@37888: Matching ist eine Technik von Rewriting, die von \isac verwendet wird, um ein Problem und den passenden Problemtyp daf\"ur zu finden. Die folgende Funktion, die \"uberpr\"uft, ob matching möglich ist, hat diese Signatur:
alexandra@37888: {\footnotesize\begin{verbatim}
alexandra@37888: > matches;
alexandra@37888: val it = fn : Theory.theory -> Term.term -> Term.term -> bool
alexandra@37888: \end{verbatim}
alexandra@37888: Die folgende Gleichung wird in Operatoren und freie Variablen zerlegt.
alexandra@37888: {\footnotesize\begin{verbatim}
alexandra@37888: > val t = (term_of o the o (parse thy)) "3 * x^^^2 = 1";
alexandra@37888: val t =
alexandra@37888: Const ("op =", "[RealDef.real, RealDef.real] => bool") $
alexandra@37888: (Const ("op *", "[RealDef.real, RealDef.real] => RealDef.real") $
alexandra@37888: Free ("3", "RealDef.real") $
alexandra@37888: (Const
alexandra@37888: ("Atools.pow",
alexandra@37888: "[RealDef.real, RealDef.real] => RealDef.real") $
alexandra@37888: Free ("x", "RealDef.real") $ Free ("2", " RealDef.real"))) $
alexandra@37888: Free ("1", "RealDef.real") : Term.term
alexandra@37888: \end{verbatim}
alexandra@37888: Nun wird ein Modell erstellt, das sich nicht auf bestimmte Zahlen bezieht, sondern nur eine generelle Zerlegung durchführt.
alexandra@37888: {\footnotesize\begin{verbatim}
alexandra@37888: > val p = (term_of o the o (parse thy)) "a * b^^^2 = c";
alexandra@37888: val p =
alexandra@37888: Const ("op =", "[RealDef.real, RealDef.real] => bool") $
alexandra@37888: (Const ("op *", "[RealDef.real, RealDef.real] => RealDef.real") $
alexandra@37888: Free ("a", "RealDef.real") $
alexandra@37888: (Const
alexandra@37888: ("Atools.pow",
alexandra@37888: "[RealDef.real, RealDef.real] => RealDef.real") $
alexandra@37888: Free ("b", "RealDef.real") $ Free ("2", "RealDef.real"))) $
alexandra@37888: Free ("c", "RealDef.real") : Term.term
alexandra@37888: \end{verbatim}
alexandra@37888: Dieses Modell enth\"allt sogenannte \textit{scheme variables}.
alexandra@37888: {\footnotesize\begin{verbatim}
alexandra@37888: > atomt p;
alexandra@37888: "*** -------------"
alexandra@37888: "*** Const (op =)"
alexandra@37888: "*** . Const (op *)""*** . . Free (a, )"
alexandra@37888: "*** . . Const (Atools.pow)"
alexandra@37888: "*** . . . Free (b, )"
alexandra@37888: "*** . . . Free (2, )"
alexandra@37888: "*** . Free (c, )"
alexandra@37888: "\n"
alexandra@37888: val it = "\n" : string
alexandra@37888: \end{verbatim}
alexandra@37888: Das Modell wird durch den Befehl free2var erstellt.
alexandra@37888: {\footnotesize\begin{verbatim}
alexandra@37888: > free2var;
alexandra@37888: val it = fn : Term.term -> Term.term
alexandra@37888: > val pat = free2var p;
alexandra@37888: val pat =
alexandra@37888: Const ("op =", "[RealDef.real, RealDef.real] => bool") $
alexandra@37888: (Const ("op *", "[RealDef.real, RealDef.real] => RealDef.real") $
alexandra@37888: Var (("a", 0), "RealDef.real") $
alexandra@37888: (Const
alexandra@37888: ("Atools.pow",
alexandra@37888: "[RealDef.real, RealDef.real] => RealDef.real") $
alexandra@37888: Var (("b", 0), "RealDef.real") $
alexandra@37888: Free ("2", "RealDef.real"))) $ Var (("c", 0), "RealDef.real")
alexandra@37888: : Term.term
alexandra@37888: > Sign.string_of_term (sign_of thy) pat;
alexandra@37888: val it = "?a * ?b ^^^ 2 = ?c" : string
alexandra@37888: \end{verbatim}
alexandra@37888: Durch atomt pat wird der Term aufgespalten und so in eine Form gebracht, die f\"ur die weiteren Schritte ben\"otigt werden.
alexandra@37888: {\footnotesize\begin{verbatim}
alexandra@37888: > atomt pat;
alexandra@37888: "*** -------------"
alexandra@37888: "*** Const (op =)"
alexandra@37888: "*** . Const (op *)"
alexandra@37888: "*** . . Var ((a, 0), )"
alexandra@37888: "*** . . Const (Atools.pow)"
alexandra@37888: "*** . . . Var ((b, 0), )"
alexandra@37888: "*** . . . Free (2, )"
alexandra@37888: "*** . Var ((c, 0), )"
alexandra@37888: "\n"
alexandra@37888: val it = "\n" : string
alexandra@37888: \end{verbatim}
alexandra@37888: Jetzt kann das Matching f\"ur die beiden vorigen Terme angewendet werden.
alexandra@37888: {\footnotesize\begin{verbatim}
alexandra@37888: > matches thy t pat;
alexandra@37888: val it = true : bool
alexandra@37888: > val t2 = (term_of o the o (parse thy)) "x^^^2 = 1";
alexandra@37888: val t2 =
alexandra@37888: Const ("op =", "[RealDef.real, RealDef.real] => bool") $
alexandra@37888: (Const
alexandra@37888: ("Atools.pow",
alexandra@37888: "[RealDef.real, RealDef.real] => RealDef.real") $
alexandra@37888: Free ("x", "RealDef.real") $ Free ("2", "RealDef.real")) $
alexandra@37888: Free ("1", "RealDef.real") : Term.term
alexandra@37888: > matches thy t2 pat;
alexandra@37888: val it = false : bool
alexandra@37888: > val pat2 = (term_of o the o (parse thy)) "?u^^^2 = ?v";
alexandra@37888: val pat2 =
alexandra@37888: Const ("op =", "[RealDef.real, RealDef.real] => bool") $
alexandra@37888: (Const
alexandra@37888: ("Atools.pow",
alexandra@37888: "[RealDef.real, RealDef.real] => RealDef.real") $
alexandra@37888: Var (("u", 0), "RealDef.real") $ Free ("2", "RealDef.real")) $
alexandra@37888: Var (("v", 0), "RealDef.real") : Term.term
alexandra@37888: > matches thy t2 pat2;
alexandra@37888: val it = true : bool
alexandra@37888: \end{verbatim}
alexandra@37888: 
alexandra@37888: \section{Zugriff auf die Hierarchie}
alexandra@37888: Man verwendet folgenden Befehl, um sich Zugang zur Hierarchie von Problemtypen zu verschaffen.
alexandra@37888: {\footnotesize\begin{verbatim}
alexandra@37888: > show_ptyps;
alexandra@37888: val it = fn : unit -> unit
alexandra@37888: > show_ptyps();
alexandra@37888: [
alexandra@37888: ["e_pblID"],
alexandra@37888: ["simplification", "polynomial"],
alexandra@37888: ["simplification", "rational"],
alexandra@37888: ["vereinfachen", "polynom", "plus_minus"],
alexandra@37888: ["vereinfachen", "polynom", "klammer"],
alexandra@37888: ["vereinfachen", "polynom", "binom_klammer"],
alexandra@37888: ["probe", "polynom"],
alexandra@37888: ["probe", "bruch"],
alexandra@37888: ["equation", "univariate", "linear"],
alexandra@37888: ["equation", "univariate", "root", "sq", "rat"],
alexandra@37888: ["equation", "univariate", "root", "normalize"],
alexandra@37888: ["equation", "univariate", "rational"],
alexandra@37888: ["equation", "univariate", "polynomial", "degree_0"],
alexandra@37888: ["equation", "univariate", "polynomial", "degree_1"],
alexandra@37888: ["equation", "univariate", "polynomial", "degree_2", "sq_only"],
alexandra@37888: ["equation", "univariate", "polynomial", " 
alexandra@37888:  degree_2", "bdv_only"],
alexandra@37888: ["equation", "univariate", "polynomial", "degree_2", "pqFormula"],
alexandra@37888: ["equation", "univariate", "polynomial", "degree_2", "abcFormula"],
alexandra@37888: ["equation", "univariate", "polynomial", "degree_3"],
alexandra@37888: ["equation", "univariate", "polynomial", "degree_4"],
alexandra@37888: ["equation", "univariate", "polynomial", "normalize"],
alexandra@37888: ["equation", "univariate", "expanded", "degree_2"],
alexandra@37888: ["equation", "makeFunctionTo"],
alexandra@37888: ["function", "derivative_of", "named"],
alexandra@37888: ["function", "maximum_of", "on_interval"],
alexandra@37888: ["function", "make", "by_explicit"],
alexandra@37888: ["function", "make", "by_new_variable"],
alexandra@37888: ["function", "integrate", "named"],
alexandra@37888: ["tool", "find_values"],
alexandra@37888: ["system", "linear", "2x2", "triangular"],
alexandra@37888: ["system", "linear", "2x2", "normalize"],
alexandra@37888: ["system", "linear", "3x3"],
alexandra@37888: ["system", "linear", "4x4", "triangular"],
alexandra@37888: ["system", "linear", "4x4", "normalize"],
alexandra@37888: ["Biegelinien", "
alexandra@37888: MomentBestimmte"],
alexandra@37888: ["Biegelinien", "MomentGegebene"],
alexandra@37888: ["Biegelinien", "einfache"],
alexandra@37888: ["Biegelinien", "QuerkraftUndMomentBestimmte"],
alexandra@37888: ["Biegelinien", "vonBelastungZu"],
alexandra@37888: ["Biegelinien", "setzeRandbedingungen"],
alexandra@37888: ["Berechnung", "numerischSymbolische"],
alexandra@37888: ["test", "equation", "univariate", "linear"],
alexandra@37888: ["test", "equation", "univariate", "plain_square"],
alexandra@37888: ["test", "equation", "univariate", "polynomial", "degree_two", "pq_formula"],
alexandra@37888: ["test", "equation", "univariate", "polynomial", "degree_two", "abc_formula"],
alexandra@37888: ["test", "equation", "univariate", "squareroot"],
alexandra@37888: ["test", "equation", "univariate", "normalize"],
alexandra@37888: ["test", "equation", "univariate", "sqroot-test"]
alexandra@37888: ]
alexandra@37888: val it = () : unit
alexandra@37888: \end{verbatim}
alexandra@37888: 
alexandra@37888: \section{Die passende ''Formalization`` f\"ur den Problemtyp}
alexandra@37888: Eine andere Art des Matching ist es die richtige ''Formalization`` zum jeweiligen Problemtyp zu finden. Wenn es eine ''Formalization`` gibt, dann kann \isac{} selbstst\"andig die Probleme l\"osen.
alexandra@37888: 
alexandra@37888: \section{Problem - Refinement}
alexandra@37888: Will man die Hierarchie der Probleme aufstellen, so ist darauf zu achten, dass man die verschiedenen Branches so konstruiert, dass das Problem - Refinement automatisch durchgef\"uhrt werden kann. F\"ur diese Anwendung wird die Hierarchie nach folgenden Regeln aufgestellt:
alexandra@37888: $F$ ist eine Formalization und $P$ und $P_i,\:i=1\cdots n$ sind Problemtypen, wobei $P_i$ ein spezieller Problemtyp ist, im Bezug auf $P$, dann gilt:
alexandra@37888: {\small
alexandra@37888: \begin{enumerate}
alexandra@37888: \item wenn für $F$ der Problemtyp $P_i$ passt, dann passt auch $P$
alexandra@37888: \item wenn zu $F$ der Problemtyp P passt, dann sollte es nicht mehr als ein $P_i$ geben, das zu $F$ passt.
alexandra@37888: \item alle $F$ , die zu $P$ passen, m\"ussen auch zu $P_n$ passen
alexandra@37888: \end{enumerate}
alexandra@37888: Zuerst ein Beispiel für die ersten zwei Punkte:
alexandra@37888: {\footnotesize\begin{verbatim}
alexandra@37888: > refine;
alexandra@37888: val it = fn : fmz_ -> pblID -> SpecifyTools.match list
alexandra@37888: > val fmz = ["equality (sqrt(9 + 4 * x)=sqrt x 
alexandra@37888: + sqrt (5 + x))",
alexandra@37888: # "soleFor x","errorBound (eps=0)",
alexandra@37888: # "solutions L"];
alexandra@37888: val fmz =
alexandra@37888: ["equality (sqrt(9 + 4 * x)=sqrt x + sqrt (5 + x))", "soleFor x",
alexandra@37888: "errorBound (eps=0)", ...] : string list
alexandra@37888: > refine fmz ["univariate","equation"];
alexandra@37888: *** pass ["equation","univariate"]
alexandra@37888: *** comp_dts: ??.empty $ soleFor x
alexandra@37888: Exception- ERROR raised
alexandra@37888: \end{verbatim}
alexandra@37888: Wenn die ersten zwei Regeln nicht angewendet werden k\"onnen, wird die dritte verwendet:
alexandra@37888: {\footnotesize\begin{verbatim}
alexandra@37888: > val fmz = ["equality (x + 1 = 2)",
alexandra@37888: # "solveFor x","errorBound (eps=0)",
alexandra@37888: # "solutions L"];
alexandra@37888: val fmz = ["equality (x + 1 = 2)", "solveFor x", "errorBound (eps=0)", ...]
alexandra@37888: : string list
alexandra@37888: > refine fmz ["univariate","equation"];
alexandra@37888: *** pass ["equation","univariate"]
alexandra@37888: *** pass ["equation","univariate","linear"]
alexandra@37888: *** pass ["equation","univariate","root"]
alexandra@37888: *** pass ["equation","univariate","rational"]
alexandra@37888: *** pass ["equation","univariate","polynomial" ]
alexandra@37888: *** pass ["equation","univariate","polynomial","degree_0"]
alexandra@37888: *** pass ["equation","univariate","polynomial","degree_1"]
alexandra@37888: *** pass ["equation","univariate","polynomial","degree_2"]
alexandra@37888: *** pass ["equation","univariate","polynomial","degree_3"]
alexandra@37888: *** pass ["equation","univariate","polynomial","degree_4"]
alexandra@37888: *** pass ["equation","univariate","polynomial","normalize"]
alexandra@37888: val it =
alexandra@37888: [Matches
alexandra@37888: (["univariate", "equation"],
alexandra@37888: {Find = [Correct "solutions L"], With = [...], ...}),
alexandra@37888: NoMatch (["linear", "univariate", ...], {Find = [...], ...}),
alexandra@37888: NoMatch (["root", ...], ...), ...] : SpecifyTools.match list
alexandra@37888: \end{verbatim}
alexandra@37888: Der Problemtyp $P_n$ verwandelt x + 1 = 2 in die normale Form -1 + x = 0. Diese suche nach der jeweiligen Problemhierarchie kann mit Hilfe von einem ''proof state`` durchgeführt werden (siehe nächstes Kapitel).
alexandra@37882: 
alexandra@37887: 
alexandra@37882: \chapter{Methods}
alexandra@37882: 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.
alexandra@37882: \section{Der ''Syntax`` des Scriptes}
alexandra@37882: Syntax beschreibt den Zusammenhang der einzelnen Zeichen und Zeichenfolgen mit den Theorien.
alexandra@37882: Er kann so definiert werden:
alexandra@37882: \begin{tabbing}
alexandra@37882: 123\=123\=expr ::=\=$|\;\;$\=\kill
alexandra@37882: \>script ::= {\tt Script} id arg$\,^*$ = body\\
alexandra@37882: \>\>arg ::= id $\;|\;\;($ ( id :: type ) $)$\\
alexandra@37882: \>\>body ::= expr\\
alexandra@37882: \>\>expr ::= \>\>{\tt let} id = expr $($ ; id = expr$)^*$ {\tt in} expr\\
alexandra@37882: \>\>\>$|\;$\>{\tt if} prop {\tt then} expr {\tt else} expr\\
alexandra@37882: \>\>\>$|\;$\>listexpr\\
alexandra@37882: \>\>\>$|\;$\>id\\
alexandra@37882: \>\>\>$|\;$\>seqex id\\
alexandra@37882: \>\>seqex ::= \>\>{\tt While} prop {\tt Do} seqex\\
alexandra@37882: \>\>\>$|\;$\>{\tt Repeat} seqex\\
alexandra@37882: \>\>\>$|\;$\>{\tt Try} seqex\\
alexandra@37882: \>\>\>$|\;$\>seqex {\tt Or} seqex\\
alexandra@37882: \>\>\>$|\;$\>seqex {\tt @@} seqex\\
alexandra@37882: \>\>\>$|\;$\>tac $($ id $|$ listexpr $)^*$\\
alexandra@37882: \>\>type ::= id\\
alexandra@37882: \>\>tac ::= id
alexandra@37882: \end{tabbing}}
ahirn@37877: 
alexandra@37887: \section{\"Uberpr\"ufung der Auswertung}
alexandra@37887: Das Kontrollsystem arbeitet mit den folgenden Script-Ausdr\"ucken, die {\it tacticals} genannt werden:
alexandra@37887: \begin{description}
alexandra@37887: \item{{\tt while} prop {\tt Do} expr id} 
alexandra@37887: \item{{\tt if} prop {\tt then} expr {\tt else} expr}
alexandra@37887: \end{description}
alexandra@37887: W\"ahrend die genannten Bezeichnungen das Kontrollsystem durch Auswertung der Formeln ausl\"osen, h\"angen die anderen von der Anwendbarkeit der Formel in den entsprechenden Unterbegriffen ab:
alexandra@37887: \begin{description}
alexandra@37887: \item{{\tt Repeat} expr id}
alexandra@37887: \item{{\tt Try} expr id}
alexandra@37887: \item{expr {\tt Or} expr id}
alexandra@37887: \item{expr {\tt @@} expr id}
alexandra@37887: \item xxx
alexandra@37887: \end{description}
alexandra@37887: 
alexandra@37887: 
alexandra@37888: 
alexandra@37888: \chapter{Befehle von \isac{}}
alexandra@37888: 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.
alexandra@37888: \newline \textbf{Init\_Proof\_Hid (dialogmode, formalization, specifictaion} gibt die eingegebenen Befehle weiter an die mathematic engine, wobei die beiden letzten Begriffe die Beispiele automatisch speichern. Es ist nicht vorgesehen, dass der Sch\"uler die Taktik verwendet.
alexandra@37888: \newline \textbf{Init\_Proof} bildet mit einem ''proof tree`` ein leeres Modell.
alexandra@37888: \newline \textbf{Model\_Problem problem} bestimmt ein problemtype, das wom\"oglich in der ''hierachy`` gefunden wurde, und verwendet es f\"u das Umformen.
alexandra@37888: \newline \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 Taktik und Formel von einer Liste w\"ahlen will.
alexandra@37888: \newline \textbf{Specify\_Theorie theory, Specify\_Problem proble, Specify\_Method method} gibt das entsprechende Element des Basiswissens an.
alexandra@37888: \newline \textbf{Refine\_Problem problem} sucht nach einem Problem in der hierachy, das auf das vorhandene zutrifft.
alexandra@37888: \newline \textbf{Apply\_Method method} beendet das Modell und die Beschreibung. Danach wird die L\"osungmeldung ge\"offnet.
alexandra@37888: \newline \textbf{Free\_Solve} beginnt eine L\"osungsmeldung ohne die Hilfe eine method.
alexandra@37888: \newline \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``.
alexandra@37888: \newline \textbf{Rewrite\_Asm theorem} hat die gleiche Funktion wie Rewrite, speichert jedoch eine endg\"ultige Vorraussetzung des Theorems, anstatt diese zu sch\"atzen.
alexandra@37888: \newline \textbf{Rewrite\_Set ruleset} hat \"ahnliche Funktionen wie Rewrite, gilt aber f\"ur einen ganzen Satz von Theorems, dem rule set.
alexandra@37888: \newline \textbf{Rewrite\_Inst (substitution, theorem), Rewrite\_Set\_Inst (substitution, rule set)} ist vergleichbar mit besonderen Taktiken, ersetzt aber Konstanten in der Theorem, bevor es zu einer Anwendung kommt.
alexandra@37888: 
alexandra@37888: 
alexandra@37888: 
alexandra@37887: 
alexandra@37887: 
alexandra@37887: 
alexandra@37887: 
ahirn@37877: 
ahirn@37877: 
ahirn@37877: \newpage
ahirn@37877: ------------------------------- ALTER TEXT -------------------------------
ahirn@37877: 
ahirn@37877: \chapter{Do a calculational proof}
ahirn@37877: First we list all the tactics available so far (this list may be extended during further development of \isac).
ahirn@37877: 
ahirn@37877: \section{Tactics for doing steps in calculations}
ahirn@37877: \input{tactics}
ahirn@37877: 
ahirn@37877: \section{The functionality of the math engine}
ahirn@37877: A proof is being started in the math engine {\tt me} by the tactic
ahirn@37877: \footnote{In the present version a tactic is of type {\tt mstep}.}
ahirn@37877:  {\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.
ahirn@37877: 
ahirn@37877: 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 ...
ahirn@37877: {\footnotesize\begin{verbatim}
ahirn@37877:    ML> val fmz = ["equality ((x+#1)*(x+#2)=x^^^#2+#8)","solveFor x",
ahirn@37877:                   "errorBound (eps=#0)","solutions L"];
ahirn@37877:    val fmz =
ahirn@37877:      ["equality ((x+#1)*(x+#2)=x^^^#2+#8)","solveFor x","errorBound (eps=#0)",
ahirn@37877:       "solutions L"] : string list
ahirn@37877:    ML>
ahirn@37877:    ML> val spec as (dom, pbt, met) = ("SqRoot.thy",["univariate","equation"],
ahirn@37877:                                  ("SqRoot.thy","no_met"));
ahirn@37877:    val dom = "SqRoot.thy" : string
ahirn@37877:    val pbt = ["univariate","equation"] : string list
ahirn@37877:    val met = ("SqRoot.thy","no_met") : string * string
ahirn@37877: \end{verbatim}}%size
ahirn@37877: ... 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.
ahirn@37877: 
ahirn@37877: Nevertheless this specification is sufficient for automatically solving the equation --- the appropriate method will be found by refinement within the hierarchy of problem types.
ahirn@37877: 
ahirn@37877: 
ahirn@37877: \section{Initialize the calculation}
ahirn@37877: 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.
ahirn@37877: {\footnotesize\begin{verbatim}
ahirn@37877:    ML>  val (mID,m) = ("Init_Proof",Init_Proof (fmz, (dom,pbt,met)));
ahirn@37877:    val mID = "Init_Proof" : string
ahirn@37877:    val m =
ahirn@37877:      Init_Proof
ahirn@37877:        (["equality ((x+#1)*(x+#2)=x^^^#2+#8)","solveFor x","errorBound (eps=#0)",
ahirn@37877:          "solutions L"],("SqRoot.thy",[#,#],(#,#))) : mstep
ahirn@37877:    ML>
ahirn@37877:    ML>  val (p,_,f,nxt,_,pt) = me (mID,m) e_pos' c EmptyPtree;
ahirn@37877:    val p = ([],Pbl) : pos'
ahirn@37877:    val f = Form' (PpcKF (0,EdUndef,0,Nundef,(#,#))) : mout
ahirn@37877:    val nxt = ("Refine_Tacitly",Refine_Tacitly ["univariate","equation"])
ahirn@37877:      : string * mstep
ahirn@37877:    val pt =
ahirn@37877:      Nd
ahirn@37877:        (PblObj
ahirn@37877:           {branch=#,cell=#,env=#,loc=#,meth=#,model=#,origin=#,ostate=#,probl=#,
ahirn@37877:            result=#,spec=#},[]) : ptree
ahirn@37877:    \end{verbatim}}%size
ahirn@37877: 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'}).
ahirn@37877: 
ahirn@37877: We can convince ourselves, that the problem is still empty, by increasing {\tt Compiler.Control.Print.printDepth}:
ahirn@37877: {\footnotesize\begin{verbatim}
ahirn@37877:    ML> Compiler.Control.Print.printDepth:=8; (*4 default*)
ahirn@37877:    val it = () : unit
ahirn@37877:    ML>
ahirn@37877:    ML> f;
ahirn@37877:    val it =
ahirn@37877:      Form'
ahirn@37877:        (PpcKF
ahirn@37877:           (0,EdUndef,0,Nundef,
ahirn@37877:            (Problem [],
ahirn@37877:             {Find=[Incompl "solutions []"],
ahirn@37877:              Given=[Incompl "equality",Incompl "solveFor"],Relate=[],
ahirn@37877:              Where=[False "matches (?a = ?b) e_"],With=[]}))) : mout
ahirn@37877: \end{verbatim}}%size
ahirn@37877: 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).\\
ahirn@37877: 
ahirn@37877: {\it In the sequel we will omit output of the {\tt me} if it is not important for the respective context}.\\
ahirn@37877: 
ahirn@37877: In general, the dialog guide will hide the following two tactics {\tt Refine\_Tacitly} and {\tt Model\_Problem} from the user.
ahirn@37877: {\footnotesize\begin{verbatim}
ahirn@37877:    ML>  nxt;
ahirn@37877:    val it = ("Refine_Tacitly",Refine_Tacitly ["univariate","equation"])
ahirn@37877:      : string * mstep
ahirn@37877:    ML>
ahirn@37877:    ML>  val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
ahirn@37877:    val nxt = ("Model_Problem",Model_Problem ["normalize","univariate","equation"])
ahirn@37877:      : string * mstep
ahirn@37877:    ML>
ahirn@37877:    ML>  val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
ahirn@37877: \end{verbatim}}%size
ahirn@37877: 
ahirn@37877: 
ahirn@37877: \section{The phase of modeling} 
ahirn@37877: 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}.
ahirn@37877: 
ahirn@37877: {\footnotesize\begin{verbatim}
ahirn@37877:    ML>  nxt;
ahirn@37877:    val it =
ahirn@37877:      ("Add_Given",Add_Given "equality ((x + #1) * (x + #2) = x ^^^ #2 + #8)")
ahirn@37877:      : string * mstep
ahirn@37877:    ML>
ahirn@37877:    ML>  val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
ahirn@37877:    val nxt = ("Add_Given",Add_Given "solveFor x") : string * mstep
ahirn@37877:    ML>
ahirn@37877:    ML>  val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
ahirn@37877:    val nxt = ("Add_Find",Add_Find "solutions L") : string * mstep
ahirn@37877:    ML>
ahirn@37877:    ML>  val (p,_,f,nxt,_,pt) = me nxt p [1] pt; 
ahirn@37877:    val f = Form' (PpcKF (0,EdUndef,0,Nundef,(#,#))) : mout
ahirn@37877: \end{verbatim}}%size
ahirn@37877: \noindent Now the problem is 'modeled', all items are input. We convince ourselves by increasing {\tt Compiler.Control.Print.printDepth} once more.
ahirn@37877: {\footnotesize\begin{verbatim}
ahirn@37877:    ML>  Compiler.Control.Print.printDepth:=8;
ahirn@37877:    ML>  f;
ahirn@37877:    val it =
ahirn@37877:      Form'
ahirn@37877:        (PpcKF
ahirn@37877:           (0,EdUndef,0,Nundef,
ahirn@37877:            (Problem [],
ahirn@37877:             {Find=[Correct "solutions L"],
ahirn@37877:              Given=[Correct "equality ((x + #1) * (x + #2) = x ^^^ #2 + #8)",
ahirn@37877:                     Correct "solveFor x"],Relate=[],Where=[],With=[]}))) : mout
ahirn@37877: \end{verbatim}}%size
ahirn@37877: %One of the input items is considered {\tt Superfluous} by the {\tt me} consulting the problem type {\tt ["univariate","equation"]}. The {\tt ErrorBound}, however, could become important in case the equation only could be solved by some iteration method.
ahirn@37877: 
ahirn@37877: \section{The phase of specification} 
ahirn@37877: This phase provides for explicit determination of the domain, the problem type, and the method to be used. In particular, the search for the appropriate problem type is being supported. There are two tactics for this purpose: {\tt Specify\_Problem} generates feedback on how a candidate of a problem type matches the current problem, and {\tt Refine\_Problem} provides help by the system, if the user gets lost.
ahirn@37877: {\footnotesize\begin{verbatim}
ahirn@37877: ML> nxt;
ahirn@37877:    val it = ("Specify_Domain",Specify_Domain "SqRoot.thy") : string * mstep
ahirn@37877:    ML>
ahirn@37877:    ML> val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
ahirn@37877:    val nxt =
ahirn@37877:      ("Specify_Problem",Specify_Problem ["normalize","univariate","equation"])
ahirn@37877:      : string * mstep
ahirn@37877:    val pt =
ahirn@37877:      Nd
ahirn@37877:        (PblObj
ahirn@37877:           {branch=#,cell=#,env=#,loc=#,meth=#,model=#,origin=#,ostate=#,probl=#,
ahirn@37877:               result=#,spec=#},[]) : ptree
ahirn@37877: \end{verbatim}}%size
ahirn@37877: The {\tt me} is smart enough to know the appropriate problem type (transferred tacitly with {\tt Init\_Proof}). In order to challenge the student, the dialog guide may hide this information; then the {\tt me} works as follows.
ahirn@37877: {\footnotesize\begin{verbatim}
ahirn@37877:    ML> val nxt = ("Specify_Problem",
ahirn@37877:                Specify_Problem ["polynomial","univariate","equation"]);
ahirn@37877:    ML> val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
ahirn@37877:    val f = Form' (PpcKF (0,EdUndef,0,Nundef,(#,#))) : mout
ahirn@37877:    val nxt =
ahirn@37877:      ("Refine_Problem",Refine_Problem ["normalize","univariate","equation"])
ahirn@37877:      : string * mstep
ahirn@37877:    ML>
ahirn@37877:    ML> val nxt = ("Specify_Problem",
ahirn@37877:                Specify_Problem ["linear","univariate","equation"]);
ahirn@37877:    ML> val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
ahirn@37877:    val f =
ahirn@37877:      Form'
ahirn@37877:        (PpcKF
ahirn@37877:           (0,EdUndef,0,Nundef,
ahirn@37877:            (Problem ["linear","univariate","equation"],
ahirn@37877:             {Find=[Correct "solutions L"],
ahirn@37877:              Given=[Correct "equality ((x + #1) * (x + #2) = x ^^^ #2 + #8)",
ahirn@37877:                     Correct "solveFor x"],Relate=[],
ahirn@37877:              Where=[False
ahirn@37877:                     "matches (?a + ?b * x = #0) ((x + #1) * (x + #2) = x ^^^ #2 + #8)"],
ahirn@37877:              With=[]}))) : mout 
ahirn@37877: \end{verbatim}}%size
ahirn@37877: Again assuming that the dialog guide hide the next tactic proposed by the {\tt me}, and the student gets lost, {\tt Refine\_Problem} always 'knows' the way out, if applied to the problem type {\tt["univariate","equation"]}.
ahirn@37877: {\footnotesize\begin{verbatim}
ahirn@37877:    ML> val nxt = ("Refine_Problem",
ahirn@37877:                   Refine_Problem ["linear","univariate","equation
ahirn@37877:    ML> val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
ahirn@37877:    val f = Problems (RefinedKF [NoMatch #]) : mout
ahirn@37877:    ML>
ahirn@37877:    ML>  Compiler.Control.Print.printDepth:=9;f;Compiler.Control.Print.printDepth:=4;
ahirn@37877:    val f =
ahirn@37877:      Problems
ahirn@37877:        (RefinedKF
ahirn@37877:           [NoMatch
ahirn@37877:              (["linear","univariate","equation"],
ahirn@37877:               {Find=[Correct "solutions L"],
ahirn@37877:                Given=[Correct "equality ((x + #1) * (x + #2) = x ^^^ #2 + #8)",
ahirn@37877:                       Correct "solveFor x"],Relate=[],
ahirn@37877:                Where=[False
ahirn@37877:                      "matches (?a + ?b * x = #0) ((x + #1) * (x + #2) = x ^^^ #2 + #8)"],
ahirn@37877:                With=[]})]) : mout
ahirn@37877:    ML>
ahirn@37877:    ML> val nxt = ("Refine_Problem",Refine_Problem ["univariate","equation"]);
ahirn@37877:    ML> val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
ahirn@37877:    val f =
ahirn@37877:      Problems
ahirn@37877:        (RefinedKF [Matches #,NoMatch #,NoMatch #,NoMatch #,NoMatch #,Matches #])
ahirn@37877:      : mout
ahirn@37877:    ML>
ahirn@37877:    ML>
ahirn@37877:    ML>  Compiler.Control.Print.printDepth:=9;f;Compiler.Control.Print.printDepth:=4;
ahirn@37877:    val f =
ahirn@37877:      Problems
ahirn@37877:        (RefinedKF
ahirn@37877:           [Matches
ahirn@37877:              (["univariate","equation"],
ahirn@37877:               {Find=[Correct "solutions L"],
ahirn@37877:                Given=[Correct "equality ((x + #1) * (x + #2) = x ^^^ #2 + #8)",
ahirn@37877:                       Correct "solveFor x"],Relate=[],
ahirn@37877:                Where=[Correct
ahirn@37877:                With=[]}),
ahirn@37877:            NoMatch
ahirn@37877:              (["linear","univariate","equation"],
ahirn@37877:               {Find=[Correct "solutions L"],
ahirn@37877:                Given=[Correct "equality ((x + #1) * (x + #2) = x ^^^ #2 + #8)",
ahirn@37877:                       Correct "solveFor x"],Relate=[],
ahirn@37877:                Where=[False
ahirn@37877:                       "matches (?a + ?b * x = #0) ((x + #1) * (x + #2) = x ^^^ #2 + #8)"],
ahirn@37877:                   With=[]}),
ahirn@37877:            NoMatch
ahirn@37877:              ...
ahirn@37877:              ...   
ahirn@37877:            Matches
ahirn@37877:              (["normalize","univariate","equation"],
ahirn@37877:               {Find=[Correct "solutions L"],
ahirn@37877:                Given=[Correct "equality ((x + #1) * (x + #2) = x ^^^ #2 + #8)",
ahirn@37877:                       Correct "solveFor x"],Relate=[],Where=[],With=[]})]) : mout
ahirn@37877: \end{verbatim}}%size
ahirn@37877: The tactic {\tt Refine\_Problem} returns all matches to problem types along the path traced in the problem hierarchy (anlogously to the authoring tool for refinement in sect.\ref{refine} on p.\pageref{refine}) --- a lot of information to be displayed appropriately in the hiearchy browser~!
ahirn@37877: 
ahirn@37877: \section{The phase of solving} 
ahirn@37877: This phase starts by invoking a method, which acchieves the normal form within two tactics, {\tt Rewrite rnorm\_equation\_add} and {\tt Rewrite\_Set SqRoot\_simplify}:
ahirn@37877: {\footnotesize\begin{verbatim} 
ahirn@37877:    ML> nxt;
ahirn@37877:    val it = ("Apply_Method",Apply_Method ("SqRoot.thy","norm_univar_equation"))
ahirn@37877:      : string * mstep
ahirn@37877:    ML>
ahirn@37877:    ML> val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
ahirn@37877:    val f =
ahirn@37877:      Form' (FormKF (~1,EdUndef,1,Nundef,"(x + #1) * (x + #2) = x ^^^ #2 + #8"))
ahirn@37877:    val nxt =
ahirn@37877:      ("Rewrite", Rewrite
ahirn@37877:         ("rnorm_equation_add","~ ?b =!= #0 ==> (?a = ?b) = (?a + #-1 * ?b = #0)"))
ahirn@37877:    ML>
ahirn@37877:    ML>  val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
ahirn@37877:    val f =
ahirn@37877:      Form' (FormKF (~1,EdUndef,1,Nundef,
ahirn@37877:            "(x + #1) * (x + #2) + #-1 * (x ^^^ #2 + #8) = #0")) : mout
ahirn@37877:    val nxt = ("Rewrite_Set",Rewrite_Set "SqRoot_simplify") : string * mstep
ahirn@37877:    ML>
ahirn@37877:    ML>  val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
ahirn@37877:    val f = Form' (FormKF (~1,EdUndef,1,Nundef,"#-6 + #3 * x = #0")) : mout
ahirn@37877:    val nxt = ("Subproblem",Subproblem ("SqRoot.thy",[#,#])) : string * mstep
ahirn@37877: \end{verbatim}}%size
ahirn@37877: Now the normal form {\tt \#-6 + \#3 * x = \#0} is the input to a subproblem, which again allows for specification of the type of equation, and the respective method:
ahirn@37877: {\footnotesize\begin{verbatim}
ahirn@37877:    ML> nxt;
ahirn@37877:    val it = ("Subproblem",Subproblem ("SqRoot.thy",["univariate","equation"]))
ahirn@37877:    ML>   
ahirn@37877:    ML> val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
ahirn@37877:    val f =
ahirn@37877:      Form' (FormKF
ahirn@37877:           (~1,EdUndef,1,Nundef,"Subproblem (SqRoot.thy, [univariate, equation])"))
ahirn@37877:      : mout
ahirn@37877:    val nxt = ("Refine_Tacitly",Refine_Tacitly ["univariate","equation"])
ahirn@37877:    ML>
ahirn@37877:    ML> val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
ahirn@37877:    val nxt = ("Model_Problem",Model_Problem ["linear","univariate","equation"])
ahirn@37877: \end{verbatim}}%size
ahirn@37877: As required, the tactic {\tt Refine ["univariate","equation"]} selects the appropriate type of equation from the problem hierarchy, which can be seen by the tactic {\tt Model\_Problem ["linear","univariate","equation"]} prosed by the system.
ahirn@37877: 
ahirn@37877: Again the whole phase of modeling and specification follows; we skip it here, and \isac's dialog guide may decide to do so as well.
ahirn@37877: 
ahirn@37877: 
ahirn@37877: \section{The final phase: check the post-condition}
ahirn@37877: The type of problems solved by \isac{} are so-called 'example construction problems' as shown above. The most characteristic point of such a problem is the post-condition. The handling of the post-condition in the given context is an open research question.
ahirn@37877: 
ahirn@37877: Thus the post-condition is just mentioned, in our example for both, the problem and the subproblem:
ahirn@37877: {\footnotesize\begin{verbatim}
ahirn@37877:    ML> nxt;
ahirn@37877:    val it = ("Check_Postcond",Check_Postcond ["linear","univariate","equation"])
ahirn@37877:    ML>
ahirn@37877:    ML>  val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
ahirn@37877:    val f = Form' (FormKF (~1,EdUndef,1,Nundef,"[x = #2]")) : mout
ahirn@37877:    val nxt =
ahirn@37877:      ("Check_Postcond",Check_Postcond ["normalize","univariate","equation"])
ahirn@37877:    ML>
ahirn@37877:    ML>  val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
ahirn@37877:    val f = Form' (FormKF (~1,EdUndef,0,Nundef,"[x = #2]")) : mout
ahirn@37877:    val nxt = ("End_Proof'",End_Proof') : string * mstep
ahirn@37877: \end{verbatim}}%size
ahirn@37877: The next tactic proposed by the system, {\tt End\_Proof'} indicates that the proof has finished successfully.\\
ahirn@37877: 
ahirn@37877: {\it The tactics proposed by the system need {\em not} be followed by the user; the user is free to choose other tactics, and the system will report, if this is applicable at the respective proof state, or not~! The reader may try out~!}
ahirn@37877: 
ahirn@37877: 
ahirn@37877: 
ahirn@37877: \part{Systematic description}
ahirn@37877: 
ahirn@37877: 
ahirn@37877: \chapter{The structure of the knowledge base}
ahirn@37877: 
ahirn@37877: \section{Tactics and data}
ahirn@37877: First we view the ME from outside, i.e. we regard tactics and relate them to the knowledge base (KB). W.r.t. the KB we address the atomic items which have to be implemented in detail by the authors of the KB
ahirn@37877: \footnote{Some of these items are fetched by the tactics from intermediate storage within the ME, and not directly from the KB.}
ahirn@37877: . The items are listed in alphabetical order in Tab.\ref{kb-items} on p.\pageref{kb-items}.
ahirn@37877: {\begin{table}[h]
ahirn@37877: \caption{Atomic items of the KB} \label{kb-items}
ahirn@37877: %\tabcolsep=0.3mm
ahirn@37877: \begin{center}
ahirn@37877: \def\arraystretch{1.0}
ahirn@37877: \begin{tabular}{lp{9.0cm}}
ahirn@37877: abbrevation & description \\
ahirn@37877: \hline
ahirn@37877: &\\
ahirn@37877: {\it calc\_list}
ahirn@37877: & associationlist of the evaluation-functions {\it eval\_fn}\\
ahirn@37877: {\it eval\_fn}
ahirn@37877: & evaluation-function for numerals and for predicates coded in SML\\
ahirn@37877: {\it eval\_rls   }
ahirn@37877: & ruleset {\it rls} for simplifying expressions with {\it eval\_fn}s\\
ahirn@37877: {\it fmz}
ahirn@37877: & formalization, i.e. a minimal formula representation of an example \\
ahirn@37877: {\it met}
ahirn@37877: & a method, i.e. a datastructure holding all informations for the solving phase ({\it rew\_ord}, {\it scr}, etc.)\\
ahirn@37877: {\it metID}
ahirn@37877: & reference to a {\it met}\\
ahirn@37877: {\it op}
ahirn@37877: & operator as key to an {\it eval\_fn} in a {\it calc\_list}\\
ahirn@37877: {\it pbl}
ahirn@37877: & problem, i.e. a node in the problem-hierarchy\\
ahirn@37877: {\it pblID}
ahirn@37877: & reference to a {\it pbl}\\
ahirn@37877: {\it rew\_ord}
ahirn@37877: & rewrite-order\\
ahirn@37877: {\it rls}
ahirn@37877: & ruleset, i.e. a datastructure holding theorems {\it thm} and operators {\it op} for simplification (with a {\it rew\_ord})\\
ahirn@37877: {\it Rrls}
ahirn@37877: & ruleset for 'reverse rewriting' (an \isac-technique generating stepwise rewriting, e.g. for cancelling fractions)\\
ahirn@37877: {\it scr}
ahirn@37877: & script describing algorithms by tactics, part of a {\it met} \\
ahirn@37877: {\it norm\_rls}
ahirn@37877: & special ruleset calculating a normalform, associated with a {\it thy}\\
ahirn@37877: {\it spec}
ahirn@37877: & specification, i.e. a tripel ({\it thyID, pblID, metID})\\
ahirn@37877: {\it subs}
ahirn@37877: & substitution, i.e. a list of variable-value-pairs\\
ahirn@37877: {\it term}
ahirn@37877: & Isabelle term, i.e. a formula\\
ahirn@37877: {\it thm}
ahirn@37877: & theorem\\     
ahirn@37877: {\it thy}
ahirn@37877: & theory\\
ahirn@37877: {\it thyID}
ahirn@37877: & reference to a {\it thy} \\
ahirn@37877: \end{tabular}\end{center}\end{table}
ahirn@37877: }
ahirn@37877: The relations between tactics and data items are shown in Tab.\ref{tac-kb}on p.\pageref{tac-kb}.
ahirn@37877: {\def\arraystretch{1.2}
ahirn@37877: \begin{table}[h]
ahirn@37877: \caption{Which tactic uses which KB's item~?} \label{tac-kb}
ahirn@37877: \tabcolsep=0.3mm
ahirn@37877: \begin{center}
ahirn@37877: \begin{tabular}{|ll||cccc|ccc|cccc|} \hline
ahirn@37877: tactic  &input &    &    &    &norm\_&   &rew\_&rls &eval\_&eval\_&calc\_&   \\
ahirn@37877:         &      &thy &scr &Rrls&rls  &thm &ord  &Rrls&fn    &rls   &list  &dsc\\
ahirn@37877: \hline\hline
ahirn@37877: Init\_Proof
ahirn@37877:         &fmz   & x  &    &    & x   &    &     &    &      &      &      & x \\
ahirn@37877:         &spec  &    &    &    &     &    &     &    &      &      &      &   \\
ahirn@37877: \hline
ahirn@37877: \multicolumn{13}{|l|}{model phase}\\
ahirn@37877: \hline
ahirn@37877: Add\_*  &term  & x  &    &    & x   &    &     &    &      &      &      & x \\
ahirn@37877: FormFK  &model & x  &    &    & x   &    &     &    &      &      &      & x \\
ahirn@37877: \hline
ahirn@37877: \multicolumn{13}{|l|}{specify phase}\\
ahirn@37877: \hline
ahirn@37877: Specify\_Theory 
ahirn@37877:         &thyID & x  &    &    & x   &    &     &    & x    & x    &      & x \\
ahirn@37877: Specify\_Problem 
ahirn@37877:         &pblID & x  &    &    & x   &    &     &    & x    & x    &      & x \\
ahirn@37877: Refine\_Problem 
ahirn@37877:            &pblID & x  &    &    & x   &    &     &    & x    & x    &      & x \\
ahirn@37877: Specify\_Method 
ahirn@37877:         &metID & x  &    &    & x   &    &     &    & x    & x    &      & x \\
ahirn@37877: Apply\_Method 
ahirn@37877:         &metID & x  & x  &    & x   &    &     &    & x    & x    &      & x \\
ahirn@37877: \hline
ahirn@37877: \multicolumn{13}{|l|}{solve phase}\\
ahirn@37877: \hline
ahirn@37877: Rewrite,\_Inst 
ahirn@37877:         &thm   & x  & x  &    &     & x  &met  &    & x    &met   &      &   \\
ahirn@37877: Rewrite, Detail
ahirn@37877:         &thm   & x  & x  &    &     & x  &rls  &    & x    &rls   &      &   \\
ahirn@37877: Rewrite, Detail
ahirn@37877:         &thm   & x  & x  &    &     & x  &Rrls &    & x    &Rrls  &      &   \\
ahirn@37877: Rewrite\_Set,\_Inst
ahirn@37877:         &rls   & x  & x  &    &     &    &     & x  & x    & x    &      &   \\
ahirn@37877: Calculate  
ahirn@37877:         &op    & x  & x  &    &     &    &     &    &      &      & x    &   \\
ahirn@37877: Substitute 
ahirn@37877:         &subs  & x  &    &    & x   &    &     &    &      &      &      &   \\
ahirn@37877:         &      &    &    &    &     &    &     &    &      &      &      &   \\
ahirn@37877: SubProblem 
ahirn@37877:         &spec  & x  & x  &    & x   &    &     &    & x    & x    &      & x \\
ahirn@37877:         &fmz   &    &    &    &     &    &     &    &      &      &      &   \\
ahirn@37877: \hline
ahirn@37877: \end{tabular}\end{center}\end{table}
ahirn@37877: }
ahirn@37877: 
ahirn@37877: \section{\isac's theories}
ahirn@37877: \isac's theories build upon Isabelles theories for high-order-logic (HOL) up to the respective development of real numbers ({\tt HOL/Real}). Theories have a special format defined in \cite{Isa-ref} and the suffix {\tt *.thy}; usually theories are paired with SML-files having the same filename and the suffix {\tt *.ML}.
ahirn@37877: 
ahirn@37877: \isac's theories represent the deductive part of \isac's knowledge base, the hierarchy of theories is structured accordingly. The {\tt *.ML}-files, however, contain {\em all} data of the other two axes of the knowledge base, the problems and the methods (without presenting their respective structure, which is done by the problem browser and the method browser, see \ref{pbt}).
ahirn@37877: 
ahirn@37877: Tab.\ref{theories} on p.\pageref{theories} lists the basic theories planned to be implemented in version \isac.1. We expext the list to be expanded in the near future, actually, have a look to the theory browser~!
ahirn@37877: 
ahirn@37877: The first three theories in the list do {\em not} belong to \isac's knowledge base; they are concerned with \isac's script-language for methods and listed here for completeness.
ahirn@37877: {\begin{table}[h]
ahirn@37877: \caption{Theories in \isac-version I} \label{theories}
ahirn@37877: %\tabcolsep=0.3mm
ahirn@37877: \begin{center}
ahirn@37877: \def\arraystretch{1.0}
ahirn@37877: \begin{tabular}{lp{9.0cm}}
ahirn@37877: theory & description \\
ahirn@37877: \hline
ahirn@37877: &\\
ahirn@37877: ListI.thy
ahirn@37877: & assigns identifiers to the functions defined in {\tt Isabelle2002/src/HOL/List.thy} and (intermediatly~?) defines some more list functions\\
ahirn@37877: ListI.ML
ahirn@37877: & {\tt eval\_fn} for the additional list functions\\
ahirn@37877: Tools.thy
ahirn@37877: & functions required for the evaluation of scripts\\
ahirn@37877: Tools.ML
ahirn@37877: & the respective {\tt eval\_fn}s\\
ahirn@37877: Script.thy
ahirn@37877: & prerequisites for scripts: types, tactics, tacticals,\\
ahirn@37877: Script.ML
ahirn@37877: & sets of tactics and functions for internal use\\
ahirn@37877: & \\
ahirn@37877: \hline
ahirn@37877: & \\
ahirn@37877: Typefix.thy
ahirn@37877: & an intermediate hack for escaping type errors\\
ahirn@37877: Descript.thy
ahirn@37877: & {\it description}s for the formulas in {\it model}s and {\it problem}s\\
ahirn@37877: Atools
ahirn@37877: & (re-)definition of operators; general predicates and functions for preconditions; theorems for the {\tt eval\_rls}\\
ahirn@37877: Float
ahirn@37877: & floating point numerals\\
ahirn@37877: Equation
ahirn@37877: & basic notions for equations and equational systems\\
ahirn@37877: Poly
ahirn@37877: & polynomials\\
ahirn@37877: PolyEq
ahirn@37877: & polynomial equations and equational systems \\
ahirn@37877: Rational.thy
ahirn@37877: & additional theorems for rationals\\
ahirn@37877: Rational.ML
ahirn@37877: & cancel, add and simplify rationals using (a generalization of) Euclids algorithm; respective reverse rulesets\\
ahirn@37877: RatEq
ahirn@37877: & equations on rationals\\
ahirn@37877: Root
ahirn@37877: & radicals; calculate normalform; respective reverse rulesets\\
ahirn@37877: RootEq
ahirn@37877: & equations on roots\\
ahirn@37877: RatRootEq
ahirn@37877: & equations on rationals and roots (i.e. on terms containing both operations)\\
ahirn@37877: Vect
ahirn@37877: & vector analysis\\
ahirn@37877: Trig
ahirn@37877: & trigonometriy\\
ahirn@37877: LogExp
ahirn@37877: & logarithms and exponential functions\\
ahirn@37877: Calculus
ahirn@37877: & nonstandard analysis\\
ahirn@37877: Diff
ahirn@37877: & differentiation\\
ahirn@37877: DiffApp
ahirn@37877: & applications of differentiaten (maxima-minima-problems)\\
ahirn@37877: Test
ahirn@37877: & (old) data for the test suite\\
ahirn@37877: Isac
ahirn@37877: & collects all \isac-theoris.\\
ahirn@37877: \end{tabular}\end{center}\end{table}
ahirn@37877: }
ahirn@37877: 
ahirn@37877: 
ahirn@37877: \section{Data in {\tt *.thy}- and {\tt *.ML}-files}
ahirn@37877: As already mentioned, theories come in pairs of {\tt *.thy}- and {\tt *.ML}-files with the same respective filename. How data are distributed between the two files is shown in Tab.\ref{thy-ML} on p.\pageref{thy-ML}.
ahirn@37877: {\begin{table}[h]
ahirn@37877: \caption{Data in {\tt *.thy}- and {\tt *.ML}-files} \label{thy-ML}
ahirn@37877: \tabcolsep=2.0mm
ahirn@37877: \begin{center}
ahirn@37877: \def\arraystretch{1.0}
ahirn@37877: \begin{tabular}{llp{7.7cm}}
ahirn@37877: file & data & description \\
ahirn@37877: \hline
ahirn@37877: & &\\
ahirn@37877: {\tt *.thy}
ahirn@37877: & consts 
ahirn@37877: & operators, predicates, functions, script-names ('{\tt Script} name \dots{\tt arguments}')
ahirn@37877: \\
ahirn@37877: & rules  
ahirn@37877: & theorems: \isac{} uses Isabelles theorems if possible; additional theorems analoguous to such existing in Isabelle get the Isabelle-identifier attached an {\it I}
ahirn@37877: \\& &\\
ahirn@37877: {\tt *.ML}
ahirn@37877: & {\tt theory' :=} 
ahirn@37877: & the theory defined by the actual {\tt *.thy}-file is made accessible to \isac
ahirn@37877: \\
ahirn@37877: & {\tt eval\_fn}
ahirn@37877: & evaluation function for operators and predicates, coded on the meta-level (SML); the identifier of such a function is a combination of the keyword {\tt eval\_} with the identifier of the function as defined in {\tt *.thy}
ahirn@37877: \\
ahirn@37877: & {\tt *\_simplify} 
ahirn@37877: & the canonical simplifier for the actual theory, i.e. the identifier for this ruleset is a combination of the theories identifier and the keyword {\tt *\_simplify}
ahirn@37877: \\
ahirn@37877: & {\tt norm\_rls :=}
ahirn@37877: & the canonical simplifier {\tt *\_simplify} is stored such that it is accessible for \isac
ahirn@37877: \\
ahirn@37877: & {\tt rew\_ord' :=}
ahirn@37877: & the same for rewrite orders, if needed outside of one particular ruleset
ahirn@37877: \\
ahirn@37877: & {\tt ruleset' :=}
ahirn@37877: & the same for rulesets (ordinary rulesets, reverse rulesets and {\tt eval\_rls})
ahirn@37877: \\
ahirn@37877: & {\tt calc\_list :=}
ahirn@37877: & the same for {\tt eval\_fn}s, if needed outside of one particular ruleset (e.g. for a tactic {\tt Calculate} in a script)
ahirn@37877: \\
ahirn@37877: & {\tt store\_pbl}
ahirn@37877: & problems defined within this {\tt *.ML}-file are made accessible for \isac
ahirn@37877: \\
ahirn@37877: & {\tt methods :=}
ahirn@37877: & methods defined within this {\tt *.ML}-file are made accessible for \isac
ahirn@37877: \\
ahirn@37877: \end{tabular}\end{center}\end{table}
ahirn@37877: }
ahirn@37877: The order of the data-items within the theories should adhere to the order given in this list.
ahirn@37877: 
ahirn@37877: \section{Formal description of the problem-hierarchy}
ahirn@37877: %for Richard Lang
ahirn@37877: 
ahirn@37877: \section{Script tactics}
ahirn@37877: The tactics actually promote the calculation: they construct the prooftree behind the scenes, and they are the points during evaluation where the script-interpreter transfers control to the user. Here we only describe the sytax of the tactics; the semantics is described on p.\pageref{user-tactics} below in context with the tactics the student uses ('user-tactics'): there is a 1-to-1 correspondence between user-tactics and script-tactics.
ahirn@37877: 
ahirn@37877: 
ahirn@37877: 
ahirn@37877: 
ahirn@37877: 
ahirn@37877: \part{Authoring on the knowledge}
ahirn@37877: 
ahirn@37877: 
ahirn@37877: \section{Add a theorem}
ahirn@37877: \section{Define and add a problem}
ahirn@37877: \section{Define and add a predicate}
ahirn@37877: \section{Define and add a method}
ahirn@37877: \section{}
ahirn@37877: \section{}
ahirn@37877: \section{}
ahirn@37877: \section{}
ahirn@37877: 
ahirn@37877: 
ahirn@37877: 
ahirn@37877: \newpage
ahirn@37877: \bibliography{bib/isac,bib/from-theses}
ahirn@37877: 
ahirn@37877: \end{document}




