1 \documentclass[11pt,a4paper,headline,headcount,towside,nocenter]{report}
4 %\grmn@dq@error ...and \dq \string #1 is undefined}
5 %l.989 ...tch the problem type \\{\tt["squareroot",
7 \bibliographystyle{alpha}
9 \def\isac{${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$}
11 \title{\isac --- Interface for\\
12 Developers of Math Knowledge\\[1.0ex]
14 Tools for Experiments in\\
15 Symbolic Computation\\[1.0ex]}
16 \author{The \isac-Team\\
17 \tt isac-users@ist.tugraz.at\\[1.0ex]}
29 \section{``Authoring'' und ``Tutoring''}
30 {TO DO} Mathematik lernen -- verschiedene Autoren -- Isabelle
31 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.
32 \section{Der Inhalt des Dokuments}
33 \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.
35 \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.
37 Das Dokument ist eigenst\"andig; Basiswissen \"uber SML (für eine Einf\"uhrung siehe \cite{Paulson:91}), Terme und Umschreibung wird vorrausgesetzt.
39 %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.
41 Hinweis: SML Code, Verzeichnis, Dateien sind {\tt in 'tt' geschrieben}; besonders in {\tt ML>} ist das Kerngebiet schnell.
43 \paragraph{Versuchen Sie es!} Ein weiteres Anliegen dieses Textes ist, dem Leser Tipps f\"ur Versuche mit den Anwendungen zu geben.
45 \section{Gleich am Computer ausprobieren!}\label{get-started}
46 \paragraph{TO DO screenshot} Bevor Sie mit Ihren Versuchen beginnen, m\"ochten wir Ihnen noch einige Hinweise geben.
49 \item Shell aufmachen und die Datei mat-eng-de.sml \"offnen.
50 \item $>$ : Hinter diesem Zeichen (``Prompt'') stehen jene, die Sie selbst eingeben bzw. mit Copy und Paste aus der Datei kopieren.
51 \item Die Eingabe wird mit ``;'' und ``Enter'' abgeschlossen.
52 \item Zeilen, die nicht mit Prompt beginnen, werden vom Computer ausgegeben.
56 \part{Experimentelle Ann\"aherung}
58 \chapter{Terme und Theorien}
59 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.
61 \section{Von der Formel zum Term}
62 Um ein Beispiel zu nennen: Die Formel $a+b\cdot 3$ l\"asst sich in lesbarer Form so eingeben:
63 {\footnotesize\begin{verbatim}
65 val it = "a + b * 3" : string
67 \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:
68 {\footnotesize\begin{verbatim}
69 > str2term "a + b * 3";
71 Const ("op +", "[RealDef.real, RealDef.real] => RealDef.real") $
72 Free ("a", "RealDef.real") $
73 (Const ("op *", "[RealDef.real, RealDef.real] => RealDef.real") $ ... $
76 \noindent Jene Form braucht Isabelle intern zum rechnen. Sie heisst Term und ist nicht lesbar, daf\"ur aber speicherbar mit Hilfe von ``val'' (=value)
77 {\footnotesize\begin{verbatim}
78 > val term = str2term "a + b * 3";
80 Const ("op +", "[RealDef.real, RealDef.real] => RealDef.real") $
81 Free ("a", "RealDef.real") $
82 (Const ("op *", "[RealDef.real, RealDef.real] => RealDef.real") $ ... $
85 Der gespeicherte Term kann einer Funktion ``atomty'' \"ubergeben werden, die jenen in einer abstrakten Struktur zeigt:
86 {\footnotesize\begin{verbatim}
90 *** Const (op +, [real, real] => real)
92 *** . Const (op *, [real, real] => real)
93 *** . . Free (b, real)
94 *** . . Free (3, real)
101 \section{``Theory'' und ``Parsing``}
102 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{}.
104 {\footnotesize\begin{verbatim}
107 {ProtoPure, CPure, HOL, Set, Typedef, Fun, Product_Type, Lfp, Gfp,
108 Sum_Type, Relation, Record, Inductive, Transitive_Closure,
109 Wellfounded_Recursion, NatDef, Nat, NatArith, Divides, Power,
110 SetInterval, Finite_Set, Equiv, IntDef, Int, Datatype_Universe,
111 Datatype, Numeral, Bin, IntArith, Wellfounded_Relations, Recdef, IntDiv,
112 IntPower, NatBin, NatSimprocs, Relation_Power, PreList, List, Map,
113 Hilbert_Choice, Main, Lubs, PNat, PRat, PReal, RealDef, RealOrd,
114 RealInt, RealBin, RealArith0, RealArith, RComplete, RealAbs, RealPow,
115 Ring_and_Field, Complex_Numbers, Real, ListG, Tools, Script, Typefix,
116 Float, ComplexI, Descript, Atools, Simplify, Poly, Rational, PolyMinus,
117 Equation, LinEq, Root, RootEq, RatEq, RootRat, RootRatEq, PolyEq, Vect,
118 Calculus, Trig, LogExp, Diff, DiffApp, Integrate, EqSystem, Biegelinie,
119 AlgEin, Test, Isac} : Theory.theory
121 Die, die ein Mal enth\"alt ist groups.thy. Suchen Sie nach '*' unter der Adresse:
123 http://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/library/HOL/Groups.html
124 Hier wird Ihnen erkl\"art, wie das Mal vom Computer gelesen wird.
125 {\footnotesize\begin{verbatim}
127 fixes f :: "'a => 'a => 'a" (infixl "*" 70)
128 assumes assoc [ac_simps]: "a * b * c = a * (b * c)"
130 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).
132 Parsing entsteht durch einen string und eine theory. Es verwendet Informationen, die in der theory von Isabelle enthalten sind.
133 {\footnotesize\begin{verbatim}
135 val it = fn : Theory.theory -> string -> Thm.cterm Library.option
137 Dieser term kann wieder in seine einzelnen Teile zerlegt werden.
138 {\footnotesize\begin{verbatim}
139 > val it = (term_of o the) it;
141 Const ("op +", "[RealDef.real, RealDef.real] => RealDef.real") $
142 Free ("a", "RealDef.real") $
143 (Const ("op *", "[RealDef.real, RealDef.real] => RealDef.real") $ ... $
147 \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.
149 {\footnotesize\begin{verbatim}
151 > parse HOL.thy "2^^^3";
152 *** Inner lexical error at: "^^^3"
153 val it = None : Thm.cterm Library.option
155 ''Inner lexical error`` bedeutet, dass ein Fehler aufgetreten ist, vermutlich hat man sich vertippt.
157 {\footnotesize\begin{verbatim}
159 > parse HOL.thy "d_d x (a + x)";
160 val it = None : Thm.cterm Library.option
162 Fehlt ''Inner lexical error`` wurde der Parse nicht gefunden.
164 {\footnotesize\begin{verbatim}
166 > parse Rational.thy "2^^^3";
167 val it = Some "2 ^^^ 3" : Thm.cterm Library.option
170 {\footnotesize\begin{verbatim}
172 > val Some t4 = parse Rational.thy "d_d x (a + x)";
173 val t4 = "d_d x (a + x)" : Thm.cterm
176 {\footnotesize\begin{verbatim}
178 > val Some t5 = parse Diff.thy "d_d x (a + x)";
179 val t5 = "d_d x (a + x)" : Thm.cterm
182 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.
184 \section{Details von Termen}
185 Mit Hilfe der darunterliegenden Darstellung sieht man, dass ein cterm in einen term umgewandelt werden kann.
186 {\footnotesize\begin{verbatim}
188 val it = fn : Thm.cterm -> Term.term
190 Durch die Umwandlung eines cterms in einen term sieht man die einzelnen Teile des Terms. ''Free`` bedeutet, dass man die Variable \"andern kann.
191 {\footnotesize\begin{verbatim}
194 Free ("d_d", "[RealDef.real, RealDef.real] => RealDef.real") $ ... $
198 In diesem Fall sagt uns das ''Const``, dass die Variable eine Konstante ist, also ein Fixwert ist und immer die selbe Funktion hat.
199 {\footnotesize\begin{verbatim}
202 Const ("Diff.d_d", "[RealDef.real, RealDef.real] => RealDef.real") $ ... $
205 Sollten verschiedene Teile des Output nicht sichtbar sein, kann die Schriftgr\"osse ge\"andert werden.
206 {\footnotesize\begin{verbatim}
208 val it = fn : int -> unit
210 Zuerst gibt man die Schriftgr\"osse ein, danach den term, der gr\"osser werden soll.
211 {\footnotesize\begin{verbatim}
216 Free ("d_d", "[RealDef.real, RealDef.real] => RealDef.real") $
217 Free ("x", "RealDef.real") $
218 (Const ("op +", "[RealDef.real, RealDef.real] => RealDef.real") $
219 Free ("a", "RealDef.real") $ Free ("x", "RealDef.real"))
226 Const ("Diff.d_d", "[RealDef.real, RealDef.real] => RealDef.real") $
227 Free ("x", "RealDef.real") $
228 (Const ("op +", "[RealDef.real, RealDef.real] => RealDef.real") $
229 Free ("a", "RealDef.real") $ Free ("x", "RealDef.real"))
233 Eine andere Variante um den Unterschied der beiden Terme zu sehen ist folgende:
234 {\footnotesize\begin{verbatim}
235 > (*-4-*) val thy = Rational.thy;
237 {ProtoPure, CPure, HOL, Set, Typedef, Fun, Product_Type, Lfp, Gfp,
238 Sum_Type, Relation, Record, Inductive, Transitive_Closure,
239 Wellfounded_Recursion, NatDef, Nat, NatArith, Divides, Power,
240 SetInterval, Finite_Set, Equiv, IntDef, Int, Datatype_Universe,
241 Datatype, Numeral, Bin, IntArith, Wellfounded_Relations, Recdef, IntDiv,
242 IntPower, NatBin, NatSimprocs, Relation_Power, PreList, List, Map,
243 Hilbert_Choice, Main, Lubs, PNat, PRat, PReal, RealDef, RealOrd,
244 RealInt, RealBin, RealArith0, RealArith, RComplete, RealAbs, RealPow,
245 Ring_and_Field, Complex_Numbers, Real, ListG, Tools, Script, Typefix,
246 Float, ComplexI, Descript, Atools, Simplify, Poly, Rational}
248 > ((atomty) o term_of o the o (parse thy)) "d_d x (a + x)";
251 *** Free (d_d, [real, real] => real)
253 *** . Const (op +, [real, real] => real)
254 *** . . Free (a, real)
255 *** . . Free (x, real)
261 > (*-5-*) val thy = Diff.thy;
263 {ProtoPure, CPure, HOL, Set, Typedef, Fun, Product_Type, Lfp, Gfp,
264 Sum_Type, Relation, Record, Inductive, Transitive_Closure,
265 Wellfounded_Recursion, NatDef, Nat, NatArith, Divides, Power,
266 SetInterval, Finite_Set, Equiv, IntDef, Int, Datatype_Universe,
267 Datatype, Numeral, Bin, IntArith, Wellfounded_Relations, Recdef, IntDiv,
268 IntPower, NatBin, NatSimprocs, Relation_Power, PreList, List, Map,
269 Hilbert_Choice, Main, Lubs, PNat, PRat, PReal, RealDef, RealOrd,
270 RealInt, RealBin, RealArith0, RealArith, RComplete, RealAbs, RealPow,
271 Ring_and_Field, Complex_Numbers, Real, Calculus, Trig, ListG, Tools,
272 Script, Typefix, Float, ComplexI, Descript, Atools, Simplify, Poly,
273 Equation, LinEq, Root, RootEq, Rational, RatEq, RootRat, RootRatEq,
274 PolyEq, LogExp, Diff} : Theory.theory
276 > ((atomty) o term_of o the o (parse thy)) "d_d x (a + x)";
279 *** Const (Diff.d_d, [real, real] => real)
281 *** . Const (op +, [real, real] => real)
282 *** . . Free (a, real)
283 *** . . Free (x, real)
290 {\chapter{''Rewriting``}}
292 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.
294 {\footnotesize\begin{verbatim}
299 ((Term.term * Term.term) list -> Term.term * Term.term -> bool) ->
302 Thm.thm -> Term.term -> (Term.term * Term.term list) Library.option
309 rls' -> bool -> thm' -> cterm' -> (string * string list) Library.option
312 \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!
314 Zuerst legt man fest, dass es sich um eine Differenzierung handelt.
315 {\footnotesize\begin{verbatim}
316 > val thy' = "Diff.thy";
317 val thy' = "Diff.thy" : string
319 Dann gibt man die zu l\"osende Rechnung ein.
320 {\footnotesize\begin{verbatim}
321 > val ct = "d_d x (a + a * (2 + b))";
322 val ct = "d_d x (a + a * (2 + b))" : string
324 Anschließend gibt man bekannt, dass die Summenregel angewandt werden soll.
325 {\footnotesize\begin{verbatim}
326 > val thm = ("diff_sum","");
327 val thm = ("diff_sum", "") : string * string
329 Schliesslich wird die erste Ableitung angezeigt.
330 {\footnotesize\begin{verbatim}
331 > val Some (ct,_) = rewrite_inst thy' "tless_true" "eval_rls" true
332 [("bdv","x::real")] thm ct;#
333 val ct = "d_d x a + d_d x (a * (2 + b))" : cterm'
335 Will man auch die zweite Ableitung sehen, geht man so vor:
336 {\footnotesize\begin{verbatim}
337 > val thm = ("diff_prod_const","");
338 val thm = ("diff_prod_const", "") : string * string
340 Auch die zweite Ableitung wird sichtbar.
341 {\footnotesize\begin{verbatim}
342 > val Some (ct,_) = rewrite_inst thy' "tless_true" "eval_rls" true
343 [("bdv","x::real")] thm ct;#
344 val ct = "d_d x a + a * d_d x (2 + b)" : cterm'
358 ------------------------------- ALTER TEXT -------------------------------
360 Ein Term ist eine Zeichenfolge. Das heisst Es gibt zwei Arten von Termen in Isabelle, 'raw terms' und 'certified terms'. \isac{} arbeitet mit raw terms, die effizient sind.
361 {\footnotesize\begin{verbatim}
363 Const of string * typ
364 | Free of string * typ
365 | Var of indexname * typ
367 | Abs of string * typ * term
368 | op $ of term * term;
370 datatype typ = Type of string * typ list
371 | TFree of string * sort
372 | TVar of indexname * sort;
373 \end{verbatim}}%size % $
374 Die Definition und der Indexname sind in diesem Zusammenhang nicht relevant. Der {\tt typ}e wird w\"ahrend der Parse angedeutet. Diese ist der Hauptbestandteil f\"ur andere Terms, {\tt cterm}. Sie {\tt cterm}s sind zusammengefasste Aufzeichnungen, die ohne die jeweiligen Isabelle-Funktionen nicht zusammengesetzt werden k\"onnen (type--Richtigkeit \"Uberpr\"ufen), aber dann g\"unstig als string dargestellt werden (Verwendung von SML Compiler Internals -- siehe unten).
376 \section{Theorien und Terme}
377 Die Parse verwendet Informationen, die in der Theorie von Isabelle $\sim${\tt /src/HOL}enthalten sind. Die derzeitige Theorie wird international als {\tt thy} gekennzeichnet; auf diese kann unterschiedlich zugegriffen werden.
378 {\footnotesize\begin{verbatim}
381 {ProtoPure, CPure, HOL, Set, Typedef, Fun, Product_Type, Lfp, Gfp,
382 Sum_Type, Relation, Record, Inductive, Transitive_Closure,
383 Wellfounded_Recursion, NatDef, Nat, NatArith, Divides, Power,
384 SetInterval, Finite_Set, Equiv, IntDef, Int, Datatype_Universe,
385 Datatype, Numeral, Bin, IntArith, Wellfounded_Relations, Recdef, IntDiv,
386 IntPower, NatBin, NatSimprocs, Relation_Power, PreList, List, Map,
387 Hilbert_Choice, Main, Lubs, PNat, PRat, PReal, RealDef, RealOrd,
388 RealInt, RealBin, RealArith0, RealArith, RComplete, RealAbs, RealPow,
389 Ring_and_Field, Complex_Numbers, Real, ListG, Tools, Script, Typefix,
390 Float, ComplexI, Descript, Atools, Simplify, Poly, Rational, PolyMinus,
391 Equation, LinEq, Root, RootEq, RatEq, RootRat, RootRatEq, PolyEq, Vect,
392 Calculus, Trig, LogExp, Diff, DiffApp, Integrate, EqSystem, Biegelinie,
393 AlgEin, Test, Isac} : Theory.theory
395 val it = {ProtoPure, CPure, HOL} : Theory.theory
398 val it = fn : Theory.theory -> string -> Thm.cterm Library.option
399 ML> parse thy "a + b * 3";
400 val it = Some "a + b * 3" : Thm.cterm Library.option
402 ML> val t = (term_of o the) it;
404 Const ("op +", "[RealDef.real, RealDef.real] => RealDef.real") $
405 Free ("a", "RealDef.real") $
406 (Const ("op *", "[RealDef.real, RealDef.real] => RealDef.real") $ ... $
410 Die Ausdr\"ucke {\tt term\_of} und {\tt the} werden weiter unten erkl\"art. Den Syntax aus der Liste der Funktionen kann man aus den Theorien von Isabelle \cite{Isa-obj} {\tt [isabelle]/src/HOL/}\footnote{Oder Sie schauen ins Internet unter {\tt [isabelle]/browser\_info}.} und aus den entwickelten Theorien von \isac{} unter {\tt [isac-src]/knowledge/} herauslesen. Beachten Sie, dass der Syntax von diesem Ausdruck anders ist, als jene die bei \isac vom Vorrechner nach der Umrechnung zu MathML angezeigt werden.
413 \section{Anzeigen von Termen}
414 Die Drucktiefe auf der höchsten Ebene des SML kann in Ordnung gebracht werden, um den output in der Menge des gewünschten Details zu erzeugen:
415 {\footnotesize\begin{verbatim}
416 ML> Compiler.Control.Print.printDepth;
417 val it = ref 4 : int ref
419 ML> Compiler.Control.Print.printDepth:= 2;
423 Const ("op +", "[RealDef.real, RealDef.real] => RealDef.real") $
424 Free ("a", "RealDef.real") $
425 (Const ("op *", "[RealDef.real, RealDef.real] => RealDef.real") $ ... $
428 ML> Compiler.Control.Print.printDepth:= 6;
432 Const ("op +","[RealDef.real, RealDef.real] => RealDef.real") $
433 Free ("a","RealDef.real") $
434 (Const ("op *","[RealDef.real, RealDef.real] => RealDef.real") $
435 Free ("b","RealDef.real") $ Free ("#3","RealDef.real")) : term
436 \end{verbatim}}%size % $
437 Ein n\"aherer Blick zum letzten output zeigt, dass {\tt typ} wie der string {\tt cterm} ausgegeben worden ist. Andere n\"utzliche Einstellungen für den output sind:
438 {\footnotesize\begin{verbatim}
439 ML> Compiler.Control.Print.printLength;
440 val it = ref 8 : int ref
441 ML> Compiler.Control.Print.stringDepth;
442 val it = ref 250 : int ref
444 Die SML der Terme ist nicht lesbar; es gibt Funktionen im KE, um sie zu zeigen:
445 {\footnotesize\begin{verbatim}
447 val it = fn : Term.term -> string
456 val it = "\n" : string
459 val it = fn : Term.term -> unit
462 *** Const ( op +, [real, real] => real)
463 *** . Free ( a, real)
464 *** . Const ( op *, [real, real] => real)
465 *** . . Free ( b, real)
466 *** . . Free ( #3, real)
469 {\tt typ} wird als string wiedergegeben. Diesaml aber durch die Informationen von {\tt thy} in besserer Darstellung.
471 \paragraph{Versuchen Sie es!} {\bf Das mathematische Wissen w\"achst} wie es in Isabelle schrittweise beschrieben ist. Schauen Sie ins Internet um diese Beschreibungen aufzurufen {\tt [isabelle]/src/HOL/HOL.thy} und zu sehen, ob es Kindern auf Ihrem System zur Verf\"ugung steht. Oder Sie sehen sich die verschiedenen Dateien unter {\tt [isabelle]/browser\_info} an.
472 {\footnotesize\begin{verbatim}
473 ML> (*-1-*) parse HOL.thy "#2^^^#3";
474 *** Inner lexical error at: "^^^3"
475 val it = None : Thm.cterm Library.option
477 ML> (*-2-*) parse HOL.thy "d_d x (a + x)";
478 val it = None : Thm.cterm Library.option
481 ML> (*-3-*) parse RatArith.thy "#2^^^#3";
482 val it = Some "#2 ^^^ #3" : cterm option
484 ML> (*-4-*) parse RatArith.thy "d_d x (a + x)";
485 val it = Some "d_d x (a + x)" : cterm option
488 ML> (*-5-*) parse Differentiate.thy "d_d x (a + x)";
489 val it = Some "d_d x (a + x)" : cterm option
491 ML> (*-6-*) parse Differentiate.thy "#2^^^#3";
492 val it = Some "#2 ^^^ #3" : cterm option
494 Vertrauen sie nicht der string Darstellung: Wenn wir {\tt(*-4-*)} und {\tt(*-6-*)} zu folgenden Ausdr\"ucken umwandel:\dots
495 {\footnotesize\begin{verbatim}
496 ML> (*-4-*) val thy = RatArith.thy;
497 ML> ((atomty thy) o term_of o the o (parse thy)) "d_d x (a + x)";
499 *** Free ( d_d, [real, real] => real)
500 *** . Free ( x, real)
501 *** . Const ( op +, [real, real] => real)
502 *** . . Free ( a, real)
503 *** . . Free ( x, real)
506 ML> (*-6-*) val thy = Differentiate.thy;
507 ML> ((atomty thy) o term_of o the o (parse thy)) "d_d x (a + x)";
509 *** Const ( Differentiate.d_d, [real, real] => real)
510 *** . Free ( x, real)
511 *** . Const ( op +, [real, real] => real)
512 *** . . Free ( a, real)
513 *** . . Free ( x, real)
516 \dots Wir sehen: Bei {\tt(*-4-*)} handelt es sich um eine willk\"urliche Funktion {\tt Free ( d\_d, \_)} und bei {\tt(*-6-*)} um eine spezielle unver\"anderliche Funktion {\tt Const ( Differentiate.d\_d, \_)} für das Differenzieren, welches in {\tt Differentiate.thy} erkl\"art wird und vermutlich gemeint ist.
519 \section{Terme umwandeln}
520 Die Umwandlung von {\tt cterm} zu {\tt term} wurde bereits oberhalb gezeigt:
521 {\footnotesize\begin{verbatim}
523 val it = fn : Thm.cterm -> Term.term
526 val it = fn : 'a Library.option -> 'a
528 ML> val t = (term_of o the o (parse thy)) "a + b * 3";
529 val t = Const (#,#) $ Free (#,#) $ (Const # $ Free # $ Free (#,#)) : term
531 {\tt the} wird dabei von {\tt term option} ausgewickelt --- eine hilfreiche Funktion von Larry Paulsons Grundlagen {\tt [isabelle]/src/Pure/library.ML}, die für jeden SML Programmierer sehr wertvoll ist.
533 Die anderen Umwandlungen sind folgende, wobei einige {\it signature} {\tt sign} als Theorie verwenden:
534 {\footnotesize\begin{verbatim}
536 val it = fn : theory -> Sign.sg
539 val it = fn : Sign.sg -> term -> cterm
540 ML> val ct = cterm_of (sign_of thy) t;
541 val ct = "a + b * #3" : cterm
543 ML> Sign.string_of_term;
544 val it = fn : Sign.sg -> term -> string
545 ML> Sign.string_of_term (sign_of thy) t;
546 val it = "a + b * #3" : ctem'
549 val it = fn : cterm -> string
550 ML> string_of_cterm ct;
551 val it = "a + b * #3" : ctem'
554 \section{Lehrs\"atze}
555 Theorems sind types, {\tt thm}, gesch\"utzter als {\tt cterms}: Sie sind als axioms beschrieben und haben sich in Isabelle bew\"ahrt. Diese Definitionen und Beweise sind in den Theorien im Verzeichnis {\tt[isac-src]/knowledge/} enthalten, zum Beispiel der Lehrsatz {\tt diff\_sum} in der Theorie {\tt[isac-src]/knowledge/Differentiate.thy}. Zus\"atzlich muss jeder Lehrsatz für \isac{} im zugeh\"origen {\tt *.ML}, wie etwa {\tt diff\_sum} in {\tt[isac-src]/knowledge/Differentiate.ML} aufgenommen werden, wie das Folgende:
556 {\footnotesize\begin{verbatim}
557 ML> theorem' := overwritel (!theorem',
558 [("diff_const",num_str diff_const)
561 The additional recording of theorems and other values will disappear in later versions of \isac.
563 \chapter{Umschreiben}
564 \section{Argumente f\"ur Umschreibungen}
565 Die Bezeichnung des type der Argumente und Werte der Umschreibfunktionen in \ref{rewrite} unterscheiden sich durch ein Apostroph: Die types mit einem Apostroph sind umbenannte strings um die Lesbarkeit aufrecht zu erhalten.
566 {\footnotesize\begin{verbatim}
568 val it = {ProtoPure, CPure, HOL} : theory
569 ML> "HOL.thy" : theory';
570 val it = "HOL.thy" : theory'
573 val it = fn : rew_ord (* term * term -> bool *)
574 ML> "sqrt_right" : rew_ord';
575 val it = "sqrt_right" : rew_ord'
580 {preconds=[],rew_ord=("sqrt_right",fn),
581 rules=[Thm #,Thm #,Thm #,Thm #,Thm #,Thm #,Thm #,Thm #,
582 Thm #,Thm #,Thm #,Thm #,Thm #,Calc #,Calc #,...],
583 scr=Script (Free #)} : rls
584 ML> "eval_rls" : rls';
585 val it = "eval_rls" : rls'
588 val it = "d_d ?bdv (?u + ?v) = d_d ?bdv ?u + d_d ?bdv ?v" : thm
589 ML> ("diff_sum", "") : thm';
590 val it = ("diff_sum","") : thm'
592 {\tt thm'} ist ein Teil, eventuell mit strin-Darstellung von dem zugeh\"origen Lehrsatz.
594 \section{Die Funktionen des Umschreibens}\label{rewrite}
595 Das Umschreiben wird von zwei equvalenten Funktionen begleitet, wobei die erste im KE verwendet wird und sie zweite n\"utzlich für Tests ist:
596 {\footnotesize\begin{verbatim}
601 -> rls -> bool -> thm -> term -> (term * term list) option
607 -> rls' -> bool -> thm' -> cterm' -> (cterm' * cterm' list) option
609 The arguments are the following:\\
611 \def\arraystretch{1.5}
612 \begin{tabular}{lp{11.0cm}}
613 {\tt theory} & the Isabelle theory containing the definitions necessary for parsing the {\tt term} \\
614 {\tt rew\_ord}& the rewrite order \cite{nipk:rew-all-that} for ordered rewriting -- see the section \ref{term-order} below. For {\em no} ordered rewriting take {\tt tless\_true}, a dummy order yielding true for all arguments \\
615 {\tt rls} & the rule set for evaluating the condition within {\tt thm} in case {\tt thm} is a conditional rule \\
616 {\tt bool} & a flag which triggers the evaluation of the eventual condition in {\tt thm}: if {\tt false} then evaluate the condition and according to the result of the evaluation apply {\tt thm} or not (conditional rewriting \cite{nipk:rew-all-that}), if {\tt true} then don't evaluate the condition, but put it into the set of assumptions \\
617 {\tt thm} & the theorem used to try to rewrite {\tt term} \\
618 {\tt term} & the term eventually rewritten by {\tt thm} \\
621 \noindent The respective values of {\tt rewrite\_} and {\tt rewrite} are an {\tt option} of a pair, i.e. {\tt Some(\_,\_)} in case the {\tt term} can be rewritten by {\tt thm} w.r.t. {\tt rew\_ord} and/or {\tt rls}, or {\tt None} if no rewrite is found:\\
622 \begin{tabular}{lp{10.4cm}}
623 {\tt term} & the term rewritten \\
624 {\tt term list}& the assumptions eventually generated if the {\tt bool} flag is set to {\tt true} and {\tt thm} is applicable. \\
627 \paragraph{Give it a try !} {\bf\dots rewriting is fun~!} many examples can be found in {\tt [isac-src]/tests/\dots}. In {\tt [isac-src]/tests/differentiate.sml} the following can be found:
628 {\footnotesize\begin{verbatim}
629 ML> val thy' = "Differentiate.thy";
630 val thy' = "Differentiate.thy" : string
631 ML> val ct = "d_d x (x ^^^ #2 + #3 * x + #4)";
632 val ct = "d_d x (x ^^^ #2 + #3 * x + #4)" : cterm'
634 ML> val thm = ("diff_sum","");
635 val thm = ("diff_sum","") : thm'
636 ML> val Some (ct,_) = rewrite_inst thy' "tless_true" "eval_rls" true
637 [("bdv","x::real")] thm ct;
638 val ct = "d_d x (x ^^^ #2 + #3 * x) + d_d x #4" : cterm'
640 ML> val Some (ct,_) = rewrite_inst thy' "tless_true" "eval_rls" true
641 [("bdv","x::real")] thm ct;
642 val ct = "d_d x (x ^^^ #2) + d_d x (#3 * x) + d_d x #4" : cterm'
644 ML> val thm = ("diff_prod_const","");
645 val thm = ("diff_prod_const","") : thm'
646 ML> val Some (ct,_) = rewrite_inst thy' "tless_true" "eval_rls" true
647 [("bdv","x::real")] thm ct;
648 val ct = "d_d x (x ^^^ #2) + #3 * d_d x x + d_d x #4" : cterm'
650 Sie k\"onnen unter {\tt [isac-src]/knowledge/Differentiate.thy} die Lehrs\"atze nachschlagen und versuchen Sie, diese anzuwenden bis Sie die Ergebnisse bekommen.
651 \footnote{Hinweis: Am Ende werden Sie {\tt val (ct,\_) = the (rewrite\_set thy' "eval\_rls" false "SqRoot\_simplify" ct);} benötigen.}
653 \paragraph{Versuchen Sie es!}\label{cond-rew} {\bf Conditional rewriting} ist eine besser Technik als \"ubliche Umschreibungen und \"ahnelt den Programmiersprachen mehr (siehe n\"achstes 'Versuchen Sie es'~!). Das folgende Beispiel liegt im Bereich der ??poynomial form??:
654 {\footnotesize\begin{verbatim}
655 ML> val thy' = "Isac.thy";
656 val thy' = "Isac.thy" : string
657 ML> val ct' = "#3 * a + #2 * (a + #1)";
658 val ct' = "#3 * a + #2 * (a + #1)" : cterm'
660 ML> val thm' = ("radd_mult_distrib2","?k * (?m + ?n) = ?k * ?m + ?k * ?n");
661 val thm' = ("radd_mult_distrib2","?k * (?m + ?n) = ?k * ?m + ?k * ?n")
663 ML> (*1*) val Some (ct',_) = rewrite thy' "tless_true" "eval_rls" true thm' ct';
664 val ct' = "#3 * a + (#2 * a + #2 * #1)" : cterm'
666 ML> val thm' = ("radd_assoc_RS_sym","?m1 + (?n1 + ?k1) = ?m1 + ?n1 + ?k1");
667 val thm' = ("radd_assoc_RS_sym","?m1 + (?n1 + ?k1) = ?m1 + ?n1 + ?k1")
669 ML> (*2*) val Some (ct',_) = rewrite thy' "tless_true" "eval_rls" true thm' ct';
670 val ct' = "#3 * a + #2 * a + #2 * #1" : cterm'
672 ML> val thm' = ("rcollect_right",
673 "[| ?l is_const; ?m is_const |] ==> ?l * ?n + ?m * ?n = (?l + ?m) * ?n");
676 "[| ?l is_const; ?m is_const |] ==> ?l * ?n + ?m * ?n = (?l + ?m) * ?n")
678 ML> (*3*) val Some (ct',_) = rewrite thy' "tless_true" "eval_rls" true thm' ct';
679 val ct' = "(#3 + #2) * a + #2 * #1" : cterm'
681 ML> (*4*) val Some (ct',_) = calculate' thy' "plus" ct';
682 val ct' = "#5 * a + #2 * #1" : cterm'
684 ML> (*5*) val Some (ct',_) = calculate' thy' "times" ct';
685 val ct' = "#5 * a + #2" : cterm'
687 Beachten Sie, dass es zwei Regeln gibt {\tt radd\_mult\_distrib2} in {\tt(*1*)} und {\tt rcollect\_right} in {\tt(*3*)}, die einander aufheben, (das heißt, eine angesetzte Regel w\"urde es nicht beenden), wenn es diese Bedinung nicht vorhanden ist {\tt is\_const}.
689 \paragraph{Versuchen Sie es!} {\bf Funktionelle Programmierung} kann, innerhalb einer bestimmten Reihe, durch das Umschreiben bearbeitet werden. In {\tt [isac-src]/\dots/tests/InsSort.thy} k\"onnen die Regeln gefunden werden, mit denen man eine Liste sortieren kann ('insertion sort'):
690 {\footnotesize\begin{verbatim}
691 sort_def "sort ls = foldr ins ls []"
693 ins_base "ins [] a = [a]"
694 ins_rec "ins (x#xs) a = (if x < a then x#(ins xs a) else a#(x#xs))"
696 foldr_base "foldr f [] a = a"
697 foldr_rec "foldr f (x#xs) a = foldr f xs (f a x)"
699 if_True "(if True then ?x else ?y) = ?x"
700 if_False "(if False then ?x else ?y) = ?y"
702 {\tt\#} ist ein Listenersteller, {\tt foldr} ist die bekannte Funktion beim funktionellen Programmieren und {\tt if\_True, if\_False} sind die Hilfsregeln. Dann kann das Sortieren mit den folgenden Umschreibungen durchgef\"uhrt werden.
703 {\footnotesize\begin{verbatim}
704 ML> val thy' = "InsSort.thy";
705 val thy' = "InsSort.thy" : theory'
706 ML> val ct = "sort [#1,#3,#2]" : cterm';
707 val ct = "sort [#1,#3,#2]" : cterm'
709 ML> val thm = ("sort_def","");
710 ML> val (ct,_) = the (rewrite thy' "tless_true" "eval_rls" false thm ct);
711 val ct = "foldr ins [#1, #3, #2] []" : cterm'
713 ML> val thm = ("foldr_rec","");
714 ML> val (ct,_) = the (rewrite thy' "tless_true" "eval_rls" false thm ct);
715 val ct = "foldr ins [#3, #2] (ins [] #1)" : cterm'
717 ML> val thm = ("ins_base","");
718 ML> val (ct,_) = the (rewrite thy' "tless_true" "eval_rls" false thm ct);
719 val ct = "foldr ins [#3, #2] [#1]" : cterm'
721 ML> val thm = ("foldr_rec","");
722 ML> val (ct,_) = the (rewrite thy' "tless_true" "eval_rls" false thm ct);
723 val ct = "foldr ins [#2] (ins [#1] #3)" : cterm'
725 ML> val thm = ("ins_rec","");
726 ML> val (ct,_) = the (rewrite thy' "tless_true" "eval_rls" false thm ct);
727 val ct = "foldr ins [#2] (if #1 < #3 then #1 # ins [] #3 else [#3, #1])"
730 ML> val (ct,_) = the (calculate' thy' "le" ct);
731 val ct = "foldr ins [#2] (if True then #1 # ins [] #3 else [#3, #1])" : cterm'
733 ML> val thm = ("if_True","(if True then ?x else ?y) = ?x");
734 ML> val (ct,_) = the (rewrite thy' "tless_true" "eval_rls" false thm ct);
735 val ct = "foldr ins [#2] (#1 # ins [] #3)" : cterm'
738 val ct = "sort [#1,#3,#2]" : cterm'
742 \section{Varianten des Umschreibens}
743 Einige der genannten Beispiele verwendeten schon Methoden von {\tt rewrite}, welche den selben Wert haben und sehr \"ahnliche Argumente verwenden:
744 {\footnotesize\begin{verbatim}
751 -> (cterm' * cterm') list
752 -> thm -> term -> (term * term list) option
759 -> (cterm' * cterm') list
760 -> thm' -> cterm' -> (cterm' * cterm' list) option
764 : theory -> rls -> bool -> rls -> term -> (term * term list) option
767 : theory' -> rls' -> bool -> rls' -> cterm' -> (cterm' * cterm' list) option
769 ML> rewrite_set_inst_;
774 -> (cterm' * cterm') list
775 -> rls -> term -> (term * term list) option
776 ML> rewrite_set_inst;
781 -> (cterm' * cterm') list
782 -> rls' -> cterm' -> (cterm' * cterm' list) option
785 \noindent Die Variante {\tt rewrite\_inst} \"andert {\tt (term * term) list} zu {\tt thm} vor dem Umschreiben,\\
786 Die Variante {\tt rewrite\_set} umschreibt {\tt rls} mit einem ganzen Regelsatz (anstatt mit {\tt thm}),\\
787 Die Variante {\tt rewrite\_set\_inst} ist eine Kombination aus den letzten zwei Varianten. Um zu sehen wie ein Ausdruck umgeschreiben wird, gibt es einen Schalter {\tt trace\_rewrite}:
788 {\footnotesize\begin{verbatim}
790 val it = fn : bool ref -> bool
792 ML> toggle trace_rewrite;
794 ML> toggle trace_rewrite;
795 val it = false : bool
798 \section{Regels\"atze}
799 Eine Varianten von {\tt rewrite} oberhalb gelten nicht nur für einen Lehrsatz, sondern für eine Vielzahl von Lehrs\"atzen, die 'Regels\"atze' genannt werden. Ein Regelsatz wird so lange angewendet, bis eines seiner Elemente f\"ur das Umschreiben verwendet werden kann (das kann ewig dauern, zum Beispiel, wenn ein Regelsatz nicht endet).
801 Ein einfaches Beispiel für einen Regelsatz ist {\tt rearrange\_assoc}, welches in {\tt knowledge/RatArith.ML} beschrieben wird:
802 {\footnotesize\begin{verbatim}
803 val rearrange_assoc =
804 Rls{preconds = [], rew_ord = ("tless_true",tless_true),
806 [Thm ("radd_assoc_RS_sym",num_str (radd_assoc RS sym)),
807 Thm ("rmult_assoc_RS_sym",num_str (rmult_assoc RS sym))],
808 scr = Script ((term_of o the o (parse thy))
814 \item [\tt preconds] sind Bedinungen, die zutreffen m\"ussen, um den Regelsatz anwendbar zu machen (eine leere Liste berechnet {\tt true}).
815 \item [\tt rew\_ord] betrifft die Anordnung der Ausdr\"ucke, dei weiter unten in \ref{term-order} vorgestellt werden.
816 \item [\tt rules] sind die angewandten Lehrs\"atze -- grunds\"atzlich in beliebiger Anordnung, weil die Regels\"atze vervollst\"andigt werden sollten \cite{nipk:rew-all-that} (und die Lehrs\"atze werden tats\"achlich in der Reihenfolge, in der sie auf der Liste erscheinen, angewendet). Die Funktion {\tt num\_str}, muss bei den Lehrs\"atzen, die viele Konstanten enthalten, angewendet werden (und demnach ist das bei diesem Beispiel veraltert). {\tt RS} ist eine eingef\"ugte Funktion, die im Lehrsatz {\tt sym} zu {\tt radd\_assoc} vor der Abspeicherung angewendet wird (siehe 'Effekt')
817 \item [\tt scr] auch wenn das script den Regelsatz anwendet, wird es in späteren Versionen von \isac verschwinden.
819 Diese Variablen bestimmen folgendes:
820 {\footnotesize\begin{verbatim}
822 val it = "?s = ?t ==> ?t = ?s" : thm
826 {preconds=[],rew_ord=("tless_true",fn),
827 rules=[Thm ("radd_assoc_RS_sym","?m1 + (?n1 + ?k1) = ?m1 + ?n1 + ?k1"),
828 Thm ("rmult_assoc_RS_sym","?m1 * (?n1 * ?k1) = ?m1 * ?n1 * ?k1")],
829 scr=Script (Free ("empty_script","RealDef.real"))} : rls
832 \paragraph{Versuchen Sie es!} Der obengenannte Regel-Satz l\"asst eine beliebige Zahl von Parenthesen verschwinden, die auf Grund von Assoziation auf {\tt +} nicht notwendig sind.
833 {\footnotesize\begin{verbatim}
834 ML> val ct = (string_of_cterm o the o (parse RatArith.thy))
835 "a + (b * (c * d) + e)";
836 val ct = "a + ((b * (c * d) + e) + f)" : cterm'
837 ML> rewrite_set "RatArith.thy" "eval_rls" false "rearrange_assoc" ct;
838 val it = Some ("a + b * c * d + e + f",[]) : (string * string list) option
840 Um dieses Ergebnis zu erreichen muss der Regelsatz \"uberraschend schnell sein:
841 {\footnotesize\begin{verbatim}
842 ML> toggle trace_rewrite;
844 ML> rewrite_set "RatArith.thy" "eval_rls" false "rearrange_assoc" ct;
845 ### trying thm 'radd_assoc_RS_sym'
846 ### rewrite_set_: a + b * (c * d) + e
847 ### trying thm 'radd_assoc_RS_sym'
848 ### trying thm 'rmult_assoc_RS_sym'
849 ### rewrite_set_: a + b * c * d + e
850 ### trying thm 'rmult_assoc_RS_sym'
851 ### trying thm 'radd_assoc_RS_sym'
852 ### trying thm 'rmult_assoc_RS_sym'
853 val it = Some ("a + b * c * d + e",[]) : (string * string list) option
857 \section{Berechnung von numerischen Konstanten}
858 Sobald numerische Konstanten in angrenzenden Subfristen sind, können sie durch die Funktion berechnet werden (siehe p.\pageref{cond-rew}):
859 {\footnotesize\begin{verbatim}
861 val it = fn : theory' -> string -> cterm' -> (cterm' * thm') option
863 val it = fn : theory -> string -> term -> (term * (string * thm)) option
865 {\tt string} beschreibt in den Angaben die mathematisch zu berechnende Operation. Die Funktion gibt das Ergebnis der Berechnung, und als zweites Element in der Reihe gilt der Lehrsatz. Die folgenden mathematischen Operationen sind verfügbar:
866 {\footnotesize\begin{verbatim}
870 [("plus",("op +",fn)),
871 ("times",("op *",fn)),
872 ("cancel_",("cancel",fn)),
873 ("power",("pow",fn)),
874 ("sqrt",("sqrt",fn)),
876 ("Length",("Length",fn)),
878 ("power",("pow",fn)),
880 ("leq",("op <=",fn)),
881 ("is_const",("is'_const",fn)),
882 ("is_root_free",("is'_root'_free",fn)),
883 ("contains_root",("contains'_root",fn)),
884 ("ident",("ident",fn))]
885 : (string * (string * (string -> term -> theory ->
886 (string * term) option))) list ref
888 Diese Vorgänge k\"onnen so verwendet werden:
889 {\footnotesize\begin{verbatim}
890 ML> calculate' "Isac.thy" "plus" "#1 + #2";
891 val it = Some ("#3",("#add_#1_#2","\"#1 + #2 = #3\"")) : (string * thm') option
893 ML> calculate' "Isac.thy" "times" "#2 * #3";
894 val it = Some ("#6",("#mult_#2_#3","\"#2 * #3 = #6\""))
895 : (string * thm') option
897 ML> calculate' "Isac.thy" "power" "#2 ^^^ #3";
898 val it = Some ("#8",("#power_#2_#3","\"#2 ^^^ #3 = #8\""))
899 : (string * thm') option
901 ML> calculate' "Isac.thy" "cancel_" "#9 // #12";
902 val it = Some ("#3 // #4",("#cancel_#9_#12","\"#9 // #12 = #3 // #4\""))
903 : (string * thm') option
910 \chapter{Begriff-Ordnung}\label{term-order}
911 Die Anordnungen der Terme sind unverzichtbar f\"ur den Gebrauch des Umschreibens von normalen Funktionen in inhaltsorientierten - kommunikativen Breichen, wie \cite{nipk:rew-all-that}, und zum Umschreiben von normalen Formeln, die n\"otig sind um passende Modelle f\"ur Probleme zu finden, siehe \ref{pbt}.
912 \section{Beispiel f\"ur Begriff-Ordnungen}
913 Es ist nicht unbedeutend, eine Verbindung $<$ zu Termen herzustellen, die wirklich eine Anordnung besitzen, wie eine transitive und antisymmetrische Verbindung. Diese Anordnungen sind 'rekursive Bahnanordnungen' \cite{nipk:rew-all-that}. Einige Anordnungen sind im Basiswissen bei {\tt [isac-src]/knowledge/\dots}, angeführt. %FIXXXmat0201a
915 {\footnotesize\begin{verbatim}
917 val it = fn : bool -> theory -> term * term -> bool
919 val it = fn : 'a -> bool
921 Das bool Argument ist ein Schalter um die Kontrolle zur\"uck zu den zugeh\"origen Unterordnungen zu verfolgen (diese Theorie ist notwendig um die Unterordnungen als strings, sollten sie 'true' sein, anzuzeigen). Die Anordnung {\tt tless\_true} ist belanglos und tr\"agt immer {\tt true}, und {\tt sqrt\_right} bevorzugt eine Quadratwurzel, die nach rechts im Ausdruck geschoben wird:
922 {\footnotesize\begin{verbatim}
923 ML> val t1 = (term_of o the o (parse thy)) "(sqrt a) + b";
924 val t1 = Const # $ (# $ #) $ Free (#,#) : term
926 ML> val t2 = (term_of o the o (parse thy)) "b + (sqrt a)";
927 val t2 = Const # $ Free # $ (Const # $ Free #) : term
929 ML> sqrt_right false SqRoot.thy (t1, t2);
930 val it = false : bool
931 ML> sqrt_right false SqRoot.thy (t2, t1);
934 Die vielen Kontrollen, die rekursiv durch alle Subbegriffe durchgef\"uhrt werden, können überall im Algorithmus in {\tt [isac-src]/knowledge/SqRoot.ML} verfolgt werden, wenn man die flag auf true setzt:
935 {\footnotesize\begin{verbatim}
936 ML> val t1 = (term_of o the o (parse thy)) "a + b*(sqrt c) + d";
937 val t1 = Const (#,#) $ (# $ # $ (# $ #)) $ Free ("d","RealDef.real") : term
939 ML> val t2 = (term_of o the o (parse thy)) "a + (sqrt b)*c + d";
940 val t2 = Const (#,#) $ (# $ # $ (# $ #)) $ Free ("d","RealDef.real") : term
942 ML> sqrt_right true SqRoot.thy (t1, t2);
943 t= f@ts= "op +" @ "[a + b * sqrt c,d]"
944 u= g@us= "op +" @ "[a + sqrt b * c,d]"
945 size_of_term(t,u)= (8, 8)
947 terms_ord(ts,us) = LESS
949 t= f@ts= "op +" @ "[a,b * sqrt c]"
950 u= g@us= "op +" @ "[a,sqrt b * c]"
951 size_of_term(t,u)= (6, 6)
953 terms_ord(ts,us) = LESS
957 size_of_term(t,u)= (1, 1)
959 terms_ord(ts,us) = EQUAL
961 t= f@ts= "op *" @ "[b,sqrt c]"
962 u= g@us= "op *" @ "[sqrt b,c]"
963 size_of_term(t,u)= (4, 4)
965 terms_ord(ts,us) = LESS
968 u= g@us= "sqrt" @ "[b]"
969 size_of_term(t,u)= (1, 2)
971 terms_ord(ts,us) = LESS
978 \section{Geordnetes Umschreiben}
979 Das Umschreiben beinhaltet in fast allen elementaren Bereichen Probleme, die alle assoziieren und ausgewechselt werden k\"onnen, im Bezug auf {\tt +} und {\tt *} --- Das Gesetz der Wandelbarkeit angewendet mit einem Regelsatzes, veranlasst den Satz, nicht zu enden! Ein Weg mit dieser Schwierigkeit umzugehen ist das geordnete Umschreiben, bei dem die Umschreibung erst beendet ist, wenn der Begriff des Ergebnisses kleiner ist, im Bezug auf eine Begriff-Ordnung (mit einigen zus\"atzlichen Eigenschaften, die 'rewrite orders' \cite{nipk:rew-all-that} genannt werden).
981 Ein solcher Regelsatz {\tt ac\_plus\_times}, der als AC-rewrite system bezeichnet wird, kann in {\tt[isac-src]/knowledge/RathArith.ML} gefunden werden:
982 {\footnotesize\begin{verbatim}
984 Rls{preconds = [], rew_ord = ("term_order",term_order),
986 [Thm ("radd_commute",radd_commute),
987 Thm ("radd_left_commute",radd_left_commute),
988 Thm ("radd_assoc",radd_assoc),
989 Thm ("rmult_commute",rmult_commute),
990 Thm ("rmult_left_commute",rmult_left_commute),
991 Thm ("rmult_assoc",rmult_assoc)],
992 scr = Script ((term_of o the o (parse thy))
997 {preconds=[],rew_ord=("term_order",fn),
998 rules=[Thm ("radd_commute","?m + ?n = ?n + ?m"),
999 Thm ("radd_left_commute","?x + (?y + ?z) = ?y + (?x + ?z)"),
1000 Thm ("radd_assoc","?m + ?n + ?k = ?m + (?n + ?k)"),
1001 Thm ("rmult_commute","?m * ?n = ?n * ?m"),
1002 Thm ("rmult_left_commute","?x * (?y * ?z) = ?y * (?x * ?z)"),
1003 Thm ("rmult_assoc","?m * ?n * ?k = ?m * (?n * ?k)")],
1004 scr=Script (Free ("empty_script","RealDef.real"))} : rls
1005 \end{verbatim}}%size
1006 Beachten Sie, dass die Lehrs\"atze {\tt radd\_left\_commute} und {\tt rmult\_left\_commute} notwendig sind, um den Regelsatz 'confluent' zu machen!
1009 \paragraph{Versuchen Sie es!} Das geordnete Umschreiben ist eine Technik um ein normales Polynom von willk\"urlich, ganzzahligen Termen zu schafffen.:
1010 {\footnotesize\begin{verbatim}
1011 ML> val ct' = "#3 * a + b + #2 * a";
1012 val ct' = "#3 * a + b + #2 * a" : cterm'
1014 ML> (*-1-*) radd_commute; val thm' = ("radd_commute","") : thm';
1015 val it = "?m + ?n = ?n + ?m" : thm
1016 val thm' = ("radd_commute","") : thm'
1017 ML> val Some (ct',_) = rewrite thy' "tless_true" "eval_rls" true thm' ct';
1018 val ct' = "#2 * a + (#3 * a + b)" : cterm'
1020 ML> (*-2-*) rdistr_right_assoc_p; val thm' = ("rdistr_right_assoc_p","") : thm';
1021 val it = "?l * ?n + (?m * ?n + ?k) = (?l + ?m) * ?n + ?k" : thm
1022 val thm' = ("rdistr_right_assoc_p","") : thm'
1023 ML> val Some (ct',_) = rewrite thy' "tless_true" "eval_rls" true thm' ct';
1024 val ct' = "(#2 + #3) * a + b" : cterm'
1027 ML> val Some (ct',_) = calculate thy' "plus" ct';
1028 val ct' = "#5 * a + b" : cterm'
1029 \end{verbatim}}%size %FIXXXmat0201b ... calculate !
1030 Das sieht toll aus, aber wenn {\tt radd\_commute} automatisch angewendet wird {\tt (*-1-*)} ohne zu \"uberpr\"ufen, ob ide daraus entstehenden Terme kleiner werden im Bezug auf die Begriffsordnung, dann geht das Umschreiben endlos weiter. (das heißt, es wird nicht beendet) \dots
1031 {\footnotesize\begin{verbatim}
1032 ML> val ct' = "#3 * a + b + #2 * a" : cterm';
1033 val ct' = "#3 * a + b + #2 * a" : cterm'
1034 ML> val thm' = ("radd_commute","") : thm';
1035 val thm' = ("radd_commute","") : thm'
1037 ML> val Some (ct',_) = rewrite thy' "tless_true" "eval_rls" true thm' ct';
1038 val ct' = "#2 * a + (#3 * a + b)" : cterm'
1039 ML> val Some (ct',_) = rewrite thy' "tless_true" "eval_rls" true thm' ct';
1040 val ct' = "#3 * a + b + #2 * a" : cterm'
1041 ML> val Some (ct',_) = rewrite thy' "tless_true" "eval_rls" true thm' ct';
1042 val ct' = "#2 * a + (#3 * a + b)" : cterm'
1044 \end{verbatim}}%size
1046 Geordnetes Umschreiben mit dem obrigen AC-rewrite system {\tt ac\_plus\_times} verursacht eine Art Durcheinander, dem man auf die Spur kommen kann:
1047 {\footnotesize\begin{verbatim}
1048 ML> toggle trace_rewrite;
1049 val it = true : bool
1051 ML> rewrite_set "RatArith.thy" "eval_rls" false "ac_plus_times" ct;
1052 ### trying thm 'radd_commute'
1053 ### not: "a + (b * (c * d) + e)" > "b * (c * d) + e + a"
1054 ### rewrite_set_: a + (e + b * (c * d))
1055 ### trying thm 'radd_commute'
1056 ### not: "a + (e + b * (c * d))" > "e + b * (c * d) + a"
1057 ### not: "e + b * (c * d)" > "b * (c * d) + e"
1058 ### trying thm 'radd_left_commute'
1059 ### not: "a + (e + b * (c * d))" > "e + (a + b * (c * d))"
1060 ### trying thm 'radd_assoc'
1061 ### trying thm 'rmult_commute'
1062 ### not: "b * (c * d)" > "c * d * b"
1063 ### not: "c * d" > "d * c"
1064 ### trying thm 'rmult_left_commute'
1065 ### not: "b * (c * d)" > "c * (b * d)"
1066 ### trying thm 'rmult_assoc'
1067 ### trying thm 'radd_commute'
1068 ### not: "a + (e + b * (c * d))" > "e + b * (c * d) + a"
1069 ### not: "e + b * (c * d)" > "b * (c * d) + e"
1070 ### trying thm 'radd_left_commute'
1071 ### not: "a + (e + b * (c * d))" > "e + (a + b * (c * d))"
1072 ### trying thm 'radd_assoc'
1073 ### trying thm 'rmult_commute'
1074 ### not: "b * (c * d)" > "c * d * b"
1075 ### not: "c * d" > "d * c"
1076 ### trying thm 'rmult_left_commute'
1077 ### not: "b * (c * d)" > "c * (b * d)"
1078 ### trying thm 'rmult_assoc'
1079 val it = Some ("a + (e + b * (c * d))",[]) : (string * string list) option \end{verbatim}}%size
1080 Beachten Sie, dass {\tt +} nach links ausgerichtet ist, bei dem die Parenthesen f\"ur {\tt (a + b) + c = a + b + c}, aber nicht f\"ur {\tt a + (b + c)} weggelassen werden. Geordnetes Umschreiben endet unbedingt mit Parenthesen, die auf Grund der Assoziation weggelassen werden k\"onnen.
1083 \chapter{The hierarchy of problem types}\label{pbt}
1084 \section{The standard-function for 'matching'}
1085 Matching \cite{nipk:rew-all-that} is a technique used within rewriting, and used by \isac{} also for (a generalized) 'matching' a problem with a problem type. The function which tests for matching has the following signature:
1086 {\footnotesize\begin{verbatim}
1088 val it = fn : theory -> term -> term -> bool
1089 \end{verbatim}}%size
1090 where the first of the two {\tt term} arguments is the particular term to be tested, and the second one is the pattern:
1091 {\footnotesize\begin{verbatim}
1092 ML> val t = (term_of o the o (parse thy)) "#3 * x^^^#2 = #1";
1093 val t = Const (#,#) $ (# $ # $ (# $ #)) $ Free ("#1","RealDef.real") : term
1095 ML> val p = (term_of o the o (parse thy)) "a * b^^^#2 = c";
1096 val p = Const (#,#) $ (# $ # $ (# $ #)) $ Free ("c","RealDef.real") : term
1102 *** . . Const ( RatArith.pow)
1103 *** . . . Free ( b, )
1104 *** . . . Free ( #2, )
1109 val it = fn : term -> term
1111 ML> val pat = free2var p;
1112 val pat = Const (#,#) $ (# $ # $ (# $ #)) $ Var ((#,#),"RealDef.real") : term
1113 ML> Sign.string_of_term (sign_of thy) pat;
1114 val it = "?a * ?b ^^^ #2 = ?c" : cterm'
1119 *** . . Var ((a, 0), )
1120 *** . . Const ( RatArith.pow)
1121 *** . . . Var ((b, 0), )
1122 *** . . . Free ( #2, )
1123 *** . Var ((c, 0), )
1125 \end{verbatim}}%size % $
1126 Note that the pattern {\tt pat} contains so-called {\it scheme variables} decorated with a {\tt ?} (analoguous to theorems). The pattern is generated by the function {\tt free2var}. This format of the pattern is necessary in order to obtain results like these:
1127 {\footnotesize\begin{verbatim}
1128 ML> matches thy t pat;
1129 val it = true : bool
1131 ML> val t2 = (term_of o the o (parse thy)) "x^^^#2 = #1";
1132 val t2 = Const (#,#) $ (# $ # $ Free #) $ Free ("#1","RealDef.real") : term
1133 ML> matches thy t2 pat;
1134 val it = false : bool
1136 ML> val pat2 = (term_of o the o (parse thy)) "?u^^^#2 = ?v";
1137 val pat2 = Const (#,#) $ (# $ # $ Free #) $ Var ((#,#),"RealDef.real") : term
1138 ML> matches thy t2 pat2;
1139 val it = true : bool
1140 \end{verbatim}}%size % $
1142 \section{Accessing the hierarchy}
1143 The hierarchy of problem types is encapsulated; it can be accessed by the following functions. {\tt show\_ptyps} retrieves all leaves of the hierarchy (here in an early version for testing):
1144 {\footnotesize\begin{verbatim}
1146 val it = fn : unit -> unit
1150 ["equation", "univariate", "linear"],
1151 ["equation", "univariate", "plain_square"],
1152 ["equation", "univariate", "polynomial", "degree_two", "pq_formula"],
1153 ["equation", "univariate", "polynomial", "degree_two", "abc_formula"],
1154 ["equation", "univariate", "squareroot"],
1155 ["equation", "univariate", "normalize"],
1156 ["equation", "univariate", "sqroot-test"],
1157 ["function", "derivative_of"],
1158 ["function", "maximum_of", "on_interval"],
1159 ["function", "make"],
1160 ["tool", "find_values"],
1161 ["functional", "inssort"]
1164 \end{verbatim}}%size
1165 The retrieve function for individual problem types is {\tt get\_pbt}
1166 \footnote{A function providing better readable output is in preparation}. Note that its argument, the 'problem identifier' {\tt pblID}, has the strings listed in reverse order w.r.t. the hierarchy, i.e. from the leave to the root. This order makes the {\tt pblID} closer to a natural description:
1167 {\footnotesize\begin{verbatim}
1169 val it = fn : pblID -> pbt
1170 ML> get_pbt ["squareroot", "univariate", "equation"];
1172 {met=[("SqRoot.thy","square_equation")],
1173 ppc=[("#Given",(Const (#,#),Free (#,#))),
1174 ("#Given",(Const (#,#),Free (#,#))),
1175 ("#Given",(Const (#,#),Free (#,#))),
1176 ("#Find",(Const (#,#),Free (#,#)))],
1177 thy={ProtoPure, CPure, HOL, Ord, Set, subset, equalities, mono, Vimage, Fun,
1178 Prod, Lfp, Relation, Trancl, WF, NatDef, Gfp, Sum, Inductive, Nat,
1179 Arith, Divides, Power, Finite, Equiv, IntDef, Int, Univ, Datatype,
1180 Numeral, Bin, IntArith, WF_Rel, Recdef, IntDiv, NatBin, List, Option,
1181 Map, Record, RelPow, Sexp, String, Calculation, SVC_Oracle, Main,
1182 Zorn, Filter, PNat, PRat, PReal, RealDef, RealOrd, RealInt, RealBin,
1183 HyperDef, Descript, ListG, Tools, Script, Typefix, Atools, RatArith,
1185 where_=[Const ("SqRoot.contains'_root","bool => bool") $
1186 Free ("e_","bool")]} : pbt
1187 \end{verbatim}}%size %$
1188 where the records fields hold the following data:
1190 \item [\tt thy]: the theory necessary for parsing the formulas
1191 \item [\tt ppc]: the items of the problem type, divided into those {\tt Given}, the precondition {\tt Where} and the output item(s) {\tt Find}. The items of {\tt Given} and {\tt Find} are all headed by so-called descriptions, which determine the type. These descriptions are defined in {\tt [isac-src]/Isa99/Descript.thy}.
1192 \item [\tt met]: the list of methods solving this problem type.\\
1195 The following function adds or replaces a problem type (after having it prepared using {\tt prep\_pbt})
1196 {\footnotesize\begin{verbatim}
1198 val it = fn : pbt * pblID -> unit
1200 (prep_pbt SqRoot.thy
1201 (["newtype","univariate","equation"],
1202 [("#Given" ,["equality e_","solveFor v_","errorBound err_"]),
1203 ("#Where" ,["contains_root (e_::bool)"]),
1204 ("#Find" ,["solutions v_i_"])
1206 [("SqRoot.thy","square_equation")]));
1208 \end{verbatim}}%size
1209 When adding a new type with argument {\tt pblID}, an immediate parent must already exist in the hierarchy (this is the one with the tail of {\tt pblID}).
1211 \section{Internals of the datastructure}
1212 This subsection only serves for the implementation of the hierarchy browser and can be skipped by the authors of math knowledge.
1214 A problem type is described by the following record type (in the file {\tt [isac-src]/globals.sml}, the respective functions are in {\tt [isac-src]/ME/ptyps.sml}), and held in a global reference variable:
1215 {\footnotesize\begin{verbatim}
1217 {thy : theory, (* the nearest to the root,
1218 which allows to compile that pbt *)
1219 where_: term list, (* where - predicates *)
1220 ppc : ((string * (* fields "#Given","#Find" *)
1221 (term * (* description *)
1224 met : metID list}; (* methods solving the pbt *)
1226 Ptyp of string * (* key within pblID *)
1227 pbt list * (* several pbts with different domIDs*)
1229 val e_Ptyp = Ptyp ("empty",[],[]);
1231 type ptyps = ptyp list;
1232 val ptyps = ref ([e_Ptyp]:ptyps);
1233 \end{verbatim}}%size
1234 The predicates in {\tt where\_} (i.e. the preconditions) usually are defined in the respective theory in {\tt[isac-src]/knowledge}. Most of the predicates are not defined by rewriting, but by SML-code contained in the respective {\tt *.ML} file.
1236 Each item is headed by a so-called description which provides some guidance for interactive input. The descriptions are defined in {\tt[isac-src]/Isa99/Descript.thy}.
1240 \section{Match a formalization with a problem type}\label{pbl}
1241 A formalization is {\it match}ed with a problem type which yields a problem. A formal description of this kind of {\it match}ing can be found in \\{\tt ftp://ft.ist.tugraz.at/projects/isac/publ/calculemus01.ps.gz}. A formalization of an equation is e.g.
1242 {\footnotesize\begin{verbatim}
1243 ML> val fmz = ["equality (#1 + #2 * x = #0)",
1245 "solutions L"] : fmz;
1246 val fmz = ["equality (#1 + #2 * x = #0)","solveFor x","solutions L"] : fmz
1247 \end{verbatim}}%size
1248 Given a formalization (and a specification of the problem, i.e. a theory, a problemtype, and a method) \isac{} can solve the respective problem automatically. The formalization must match the problem type for this purpose:
1249 {\footnotesize\begin{verbatim}
1251 val it = fn : fmz -> pbt -> match'
1253 ML> match_pbl fmz (get_pbt ["univariate","equation"]);
1256 {Find=[Correct "solutions L"],
1257 Given=[Correct "equality (#1 + #2 * x = #0)",Correct "solveFor x"],
1258 Relate=[],Where=[Correct "matches (?a = ?b) (#1 + #2 * x = #0)"],With=[]}
1261 ML> match_pbl fmz (get_pbt ["linear","univariate","equation"]);
1264 {Find=[Correct "solutions L"],
1265 Given=[Correct "equality (#1 + #2 * x = #0)",Correct "solveFor x"],
1268 "matches ( x = #0) (#1 + #2 * x = #0) |
1269 matches ( ?b * x = #0) (#1 + #2 * x = #0) |
1270 matches (?a + x = #0) (#1 + #2 * x = #0) |
1271 matches (?a + ?b * x = #0) (#1 + #2 * x = #0)"],
1274 ML> match_pbl fmz (get_pbt ["squareroot","univariate","equation"]);
1277 {Find=[Correct "solutions L"],
1278 Given=[Correct "equality (#1 + #2 * x = #0)",Correct "solveFor x",
1279 Missing "errorBound err_"],Relate=[],
1280 Where=[False "contains_root #1 + #2 * x = #0 "],With=[]} : match'
1281 \end{verbatim}}%size
1282 The above formalization does not match the problem type \\{\tt["squareroot","univariate","equation"]} which is explained by the tags:
1285 \> {\tt Missing:} the item is missing in the formalization as required by the problem type\\
1286 \> {\tt Superfl:} the item is not required by the problem type\\
1287 \> {\tt Correct:} the item is correct, or the precondition ({\tt Where}) is true\\
1288 \> {\tt False:} the precondition ({\tt Where}) is false\\
1289 \> {\tt Incompl:} the item is incomlete, or not yet input.\\
1294 \section{Refine a problem specification}
1295 The challenge in constructing the problem hierarchy is, to design the branches in such a way, that problem refinement can be done automatically (as it is done in algebra system e.g. by a internal hierarchy of equations).
1297 For this purpose the hierarchy must be built using the following rules: Let $F$ be a formalization and $P$ and $P_i,\:i=1\cdots n$ problem types, where the $P_i$ are specialized problem types w.r.t. $P$ (i.e. $P$ is a parent node of $P_i$), then
1300 \item for all $F$ matching some $P_i$ must follow, that $F$ matches $P$
1301 \item an $F$ matching $P$ should not have more than {\em one} $P_i,\:i=1\cdots n-1$ with $F$ matching $P_i$ (if there are more than one $P_i$, the first one will be taken)
1302 \item for all $F$ matching some $P$ must follow, that $F$ matches $P_n$\\
1303 \end{enumerate}}%small
1304 \noindent Let us give an example for the point (1.) and (2.) first:
1305 {\footnotesize\begin{verbatim}
1307 val it = fn : fmz -> pblID -> match list
1309 ML> val fmz = ["equality (sqrt(#9+#4*x)=sqrt x + sqrt(#5+x))",
1310 "solveFor x","errorBound (eps=#0)",
1313 ML> refine fmz ["univariate","equation"];
1314 *** pass ["equation","univariate"]
1315 *** pass ["equation","univariate","linear"]
1316 *** pass ["equation","univariate","plain_square"]
1317 *** pass ["equation","univariate","polynomial"]
1318 *** pass ["equation","univariate","squareroot"]
1321 (["univariate","equation"],
1322 {Find=[Correct "solutions L"],
1323 Given=[Correct "equality (sqrt (#9 + #4 * x) = sqrt x + sqrt (#5 + x))",
1324 Correct "solveFor x",Superfl "errorBound (eps = #0)"],Relate=[],
1326 "matches (?a = ?b) (sqrt (#9 + #4 * x) = sqrt x + sqrt (#5 + x))"],
1329 (["linear","univariate","equation"],
1330 {Find=[Correct "solutions L"],
1331 Given=[Correct "equality (sqrt (#9 + #4 * x) = sqrt x + sqrt (#5 + x))",
1332 Correct "solveFor x",Superfl "errorBound (eps = #0)"],Relate=[],
1333 Where=[False "(?a + ?b * x = #0) (sqrt (#9 + #4 * x#"],
1336 (["plain_square","univariate","equation"],
1337 {Find=[Correct "solutions L"],
1338 Given=[Correct "equality (sqrt (#9 + #4 * x) = sqrt x + sqrt (#5 + x))",
1339 Correct "solveFor x",Superfl "errorBound (eps = #0)"],Relate=[],
1341 "matches (?a + ?b * x ^^^ #2 = #0)"],
1344 (["polynomial","univariate","equation"],
1345 {Find=[Correct "solutions L"],
1346 Given=[Correct "equality (sqrt (#9 + #4 * x) = sqrt x + sqrt (#5 + x))",
1347 Correct "solveFor x",Superfl "errorBound (eps = #0)"],Relate=[],
1349 "is_polynomial_in sqrt (#9 + #4 * x) = sqrt x + sqrt (#5 + x) x"],
1352 (["squareroot","univariate","equation"],
1353 {Find=[Correct "solutions L"],
1354 Given=[Correct "equality (sqrt (#9 + #4 * x) = sqrt x + sqrt (#5 + x))",
1355 Correct "solveFor x",Correct "errorBound (eps = #0)"],Relate=[],
1357 "contains_root sqrt (#9 + #4 * x) = sqrt x + sqrt (#5 + x) "],
1358 With=[]})] : match list
1359 \end{verbatim}}%size}%footnotesize\label{refine}
1360 This example shows, that in order to refine an {\tt["univariate","equation"]}, the formalization must match respective respective problem type (rule (1.)) and one of the descendants which should match selectively (rule (2.)).
1362 If no one of the descendants of {\tt["univariate","equation"]} match, rule (3.) comes into play: The {\em last} problem type on this level ($P_n$) provides for a special 'problem type' {\tt["normalize"]}. This node calls a method transforming the equation to a (or another) normal form, which then may match. Look at this example:
1363 {\footnotesize\begin{verbatim}
1364 ML> val fmz = ["equality (x+#1=#2)",
1365 "solveFor x","errorBound (eps=#0)",
1369 ML> refine fmz ["univariate","equation"];
1370 *** pass ["equation","univariate"]
1371 *** pass ["equation","univariate","linear"]
1372 *** pass ["equation","univariate","plain_square"]
1373 *** pass ["equation","univariate","polynomial"]
1374 *** pass ["equation","univariate","squareroot"]
1375 *** pass ["equation","univariate","normalize"]
1378 (["univariate","equation"],
1379 {Find=[Correct "solutions L"],
1380 Given=[Correct "equality (x + #1 = #2)",Correct "solveFor x",
1381 Superfl "errorBound (eps = #0)"],Relate=[],
1382 Where=[Correct "matches (?a = ?b) (x + #1 = #2)"],With=[]}),
1384 (["linear","univariate","equation"],
1388 (["squareroot","univariate","equation"],
1389 {Find=[Correct "solutions L"],
1390 Given=[Correct "equality (x + #1 = #2)",Correct "solveFor x",
1391 Correct "errorBound (eps = #0)"],Relate=[],
1392 Where=[False "contains_root x + #1 = #2 "],With=[]}),
1394 (["normalize","univariate","equation"],
1395 {Find=[Correct "solutions L"],
1396 Given=[Correct "equality (x + #1 = #2)",Correct "solveFor x",
1397 Superfl "errorBound (eps = #0)"],Relate=[],Where=[],With=[]})]
1399 \end{verbatim}}%size
1400 The problem type $P_n$, {\tt["normalize","univariate","equation"]}, will transform the equation {\tt x + \#1 = \#2} to the normal form {\tt \#-1 + x = \#0}, which then will match {\tt["linear","univariate","equation"]}.
1402 This recursive search on the problem hierarchy can be done within a proof state. This leads to the next section.
1405 \chapter{Methods}\label{met}
1406 A problem type can have one ore more methods solving a respective problem. A method is described by means of another new program language. The language itself looks like a simple functional language, but constructs an imperative proof-state behind the scenes (thus liberating the programer from dealing with technical details and also prohibiting incorrect construction of the proof tree). The interpreter of 'scripts' written in this language evaluates the scriptexpressions, and also delivers certain parts of the script itself for discussion with the user.
1408 \section{The scripts' syntax}
1409 The syntax of scripts follows the definition given in Backus-normal-form:
1412 123\=123\=expr ::=\=$|\;\;$\=\kill
1413 \>script ::= {\tt Script} id arg$\,^*$ = body\\
1414 \>\>arg ::= id $\;|\;\;($ ( id :: type ) $)$\\
1416 \>\>expr ::= \>\>{\tt let} id = expr $($ ; id = expr$)^*$ {\tt in} expr\\
1417 \>\>\>$|\;$\>{\tt if} prop {\tt then} expr {\tt else} expr\\
1418 \>\>\>$|\;$\>listexpr\\
1420 \>\>\>$|\;$\>seqex id\\
1421 \>\>seqex ::= \>\>{\tt While} prop {\tt Do} seqex\\
1422 \>\>\>$|\;$\>{\tt Repeat} seqex\\
1423 \>\>\>$|\;$\>{\tt Try} seqex\\
1424 \>\>\>$|\;$\>seqex {\tt Or} seqex\\
1425 \>\>\>$|\;$\>seqex {\tt @@} seqex\\
1426 \>\>\>$|\;$\>tac $($ id $|$ listexpr $)^*$\\
1430 where {\it id} is an identifier with the usual syntax, {\it prop} is a proposition constructed by Isabelles logical operators (see \cite{Isa-obj} {\tt [isabelle]/src/HOL/HOL.thy}), {\it listexpr} (called {\bf list-expression}) is constructed by Isabelles list functions like {\tt hd, tl, nth} described in {\tt [isabelle]/src/HOL/List.thy}, and {\it type} are (virtually) all types declared in Isabelles version 99.
1432 Expressions containing some of the keywords {\tt let}, {\tt if} etc. are called {\bf script-expressions}.
1434 Tactics {\it tac} are (curried) functions. For clarity and simplicity reasons, {\it listexpr} must not contain a {\it tac}, and {\it tac}s must not be nested,
1437 \section{Control the flow of evaluation}
1438 The flow of control is managed by the following script-expressions called {\it tacticals}.
1440 \item{{\tt while} prop {\tt Do} expr id}
1441 \item{{\tt if} prop {\tt then} expr {\tt else} expr}
1443 While the the above script-expressions trigger the flow of control by evaluating the current formula, the other expressions depend on the applicability of the tactics within their respective subexpressions (which in turn depends on the proofstate)
1445 \item{{\tt Repeat} expr id}
1446 \item{{\tt Try} expr id}
1447 \item{expr {\tt Or} expr id}
1448 \item{expr {\tt @@} expr id}
1456 \chapter{Do a calculational proof}
1457 First we list all the tactics available so far (this list may be extended during further development of \isac).
1459 \section{Tactics for doing steps in calculations}
1462 \section{The functionality of the math engine}
1463 A proof is being started in the math engine {\tt me} by the tactic
1464 \footnote{In the present version a tactic is of type {\tt mstep}.}
1465 {\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.
1467 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 ...
1468 {\footnotesize\begin{verbatim}
1469 ML> val fmz = ["equality ((x+#1)*(x+#2)=x^^^#2+#8)","solveFor x",
1470 "errorBound (eps=#0)","solutions L"];
1472 ["equality ((x+#1)*(x+#2)=x^^^#2+#8)","solveFor x","errorBound (eps=#0)",
1473 "solutions L"] : string list
1475 ML> val spec as (dom, pbt, met) = ("SqRoot.thy",["univariate","equation"],
1476 ("SqRoot.thy","no_met"));
1477 val dom = "SqRoot.thy" : string
1478 val pbt = ["univariate","equation"] : string list
1479 val met = ("SqRoot.thy","no_met") : string * string
1480 \end{verbatim}}%size
1481 ... 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.
1483 Nevertheless this specification is sufficient for automatically solving the equation --- the appropriate method will be found by refinement within the hierarchy of problem types.
1486 \section{Initialize the calculation}
1487 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.
1488 {\footnotesize\begin{verbatim}
1489 ML> val (mID,m) = ("Init_Proof",Init_Proof (fmz, (dom,pbt,met)));
1490 val mID = "Init_Proof" : string
1493 (["equality ((x+#1)*(x+#2)=x^^^#2+#8)","solveFor x","errorBound (eps=#0)",
1494 "solutions L"],("SqRoot.thy",[#,#],(#,#))) : mstep
1496 ML> val (p,_,f,nxt,_,pt) = me (mID,m) e_pos' c EmptyPtree;
1497 val p = ([],Pbl) : pos'
1498 val f = Form' (PpcKF (0,EdUndef,0,Nundef,(#,#))) : mout
1499 val nxt = ("Refine_Tacitly",Refine_Tacitly ["univariate","equation"])
1504 {branch=#,cell=#,env=#,loc=#,meth=#,model=#,origin=#,ostate=#,probl=#,
1505 result=#,spec=#},[]) : ptree
1506 \end{verbatim}}%size
1507 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'}).
1509 We can convince ourselves, that the problem is still empty, by increasing {\tt Compiler.Control.Print.printDepth}:
1510 {\footnotesize\begin{verbatim}
1511 ML> Compiler.Control.Print.printDepth:=8; (*4 default*)
1518 (0,EdUndef,0,Nundef,
1520 {Find=[Incompl "solutions []"],
1521 Given=[Incompl "equality",Incompl "solveFor"],Relate=[],
1522 Where=[False "matches (?a = ?b) e_"],With=[]}))) : mout
1523 \end{verbatim}}%size
1524 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).\\
1526 {\it In the sequel we will omit output of the {\tt me} if it is not important for the respective context}.\\
1528 In general, the dialog guide will hide the following two tactics {\tt Refine\_Tacitly} and {\tt Model\_Problem} from the user.
1529 {\footnotesize\begin{verbatim}
1531 val it = ("Refine_Tacitly",Refine_Tacitly ["univariate","equation"])
1534 ML> val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1535 val nxt = ("Model_Problem",Model_Problem ["normalize","univariate","equation"])
1538 ML> val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1539 \end{verbatim}}%size
1542 \section{The phase of modeling}
1543 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}.
1545 {\footnotesize\begin{verbatim}
1548 ("Add_Given",Add_Given "equality ((x + #1) * (x + #2) = x ^^^ #2 + #8)")
1551 ML> val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1552 val nxt = ("Add_Given",Add_Given "solveFor x") : string * mstep
1554 ML> val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1555 val nxt = ("Add_Find",Add_Find "solutions L") : string * mstep
1557 ML> val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1558 val f = Form' (PpcKF (0,EdUndef,0,Nundef,(#,#))) : mout
1559 \end{verbatim}}%size
1560 \noindent Now the problem is 'modeled', all items are input. We convince ourselves by increasing {\tt Compiler.Control.Print.printDepth} once more.
1561 {\footnotesize\begin{verbatim}
1562 ML> Compiler.Control.Print.printDepth:=8;
1567 (0,EdUndef,0,Nundef,
1569 {Find=[Correct "solutions L"],
1570 Given=[Correct "equality ((x + #1) * (x + #2) = x ^^^ #2 + #8)",
1571 Correct "solveFor x"],Relate=[],Where=[],With=[]}))) : mout
1572 \end{verbatim}}%size
1573 %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.
1575 \section{The phase of specification}
1576 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.
1577 {\footnotesize\begin{verbatim}
1579 val it = ("Specify_Domain",Specify_Domain "SqRoot.thy") : string * mstep
1581 ML> val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1583 ("Specify_Problem",Specify_Problem ["normalize","univariate","equation"])
1588 {branch=#,cell=#,env=#,loc=#,meth=#,model=#,origin=#,ostate=#,probl=#,
1589 result=#,spec=#},[]) : ptree
1590 \end{verbatim}}%size
1591 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.
1592 {\footnotesize\begin{verbatim}
1593 ML> val nxt = ("Specify_Problem",
1594 Specify_Problem ["polynomial","univariate","equation"]);
1595 ML> val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1596 val f = Form' (PpcKF (0,EdUndef,0,Nundef,(#,#))) : mout
1598 ("Refine_Problem",Refine_Problem ["normalize","univariate","equation"])
1601 ML> val nxt = ("Specify_Problem",
1602 Specify_Problem ["linear","univariate","equation"]);
1603 ML> val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1607 (0,EdUndef,0,Nundef,
1608 (Problem ["linear","univariate","equation"],
1609 {Find=[Correct "solutions L"],
1610 Given=[Correct "equality ((x + #1) * (x + #2) = x ^^^ #2 + #8)",
1611 Correct "solveFor x"],Relate=[],
1613 "matches (?a + ?b * x = #0) ((x + #1) * (x + #2) = x ^^^ #2 + #8)"],
1615 \end{verbatim}}%size
1616 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"]}.
1617 {\footnotesize\begin{verbatim}
1618 ML> val nxt = ("Refine_Problem",
1619 Refine_Problem ["linear","univariate","equation
1620 ML> val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1621 val f = Problems (RefinedKF [NoMatch #]) : mout
1623 ML> Compiler.Control.Print.printDepth:=9;f;Compiler.Control.Print.printDepth:=4;
1628 (["linear","univariate","equation"],
1629 {Find=[Correct "solutions L"],
1630 Given=[Correct "equality ((x + #1) * (x + #2) = x ^^^ #2 + #8)",
1631 Correct "solveFor x"],Relate=[],
1633 "matches (?a + ?b * x = #0) ((x + #1) * (x + #2) = x ^^^ #2 + #8)"],
1636 ML> val nxt = ("Refine_Problem",Refine_Problem ["univariate","equation"]);
1637 ML> val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1640 (RefinedKF [Matches #,NoMatch #,NoMatch #,NoMatch #,NoMatch #,Matches #])
1644 ML> Compiler.Control.Print.printDepth:=9;f;Compiler.Control.Print.printDepth:=4;
1649 (["univariate","equation"],
1650 {Find=[Correct "solutions L"],
1651 Given=[Correct "equality ((x + #1) * (x + #2) = x ^^^ #2 + #8)",
1652 Correct "solveFor x"],Relate=[],
1656 (["linear","univariate","equation"],
1657 {Find=[Correct "solutions L"],
1658 Given=[Correct "equality ((x + #1) * (x + #2) = x ^^^ #2 + #8)",
1659 Correct "solveFor x"],Relate=[],
1661 "matches (?a + ?b * x = #0) ((x + #1) * (x + #2) = x ^^^ #2 + #8)"],
1667 (["normalize","univariate","equation"],
1668 {Find=[Correct "solutions L"],
1669 Given=[Correct "equality ((x + #1) * (x + #2) = x ^^^ #2 + #8)",
1670 Correct "solveFor x"],Relate=[],Where=[],With=[]})]) : mout
1671 \end{verbatim}}%size
1672 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~!
1674 \section{The phase of solving}
1675 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}:
1676 {\footnotesize\begin{verbatim}
1678 val it = ("Apply_Method",Apply_Method ("SqRoot.thy","norm_univar_equation"))
1681 ML> val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1683 Form' (FormKF (~1,EdUndef,1,Nundef,"(x + #1) * (x + #2) = x ^^^ #2 + #8"))
1686 ("rnorm_equation_add","~ ?b =!= #0 ==> (?a = ?b) = (?a + #-1 * ?b = #0)"))
1688 ML> val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1690 Form' (FormKF (~1,EdUndef,1,Nundef,
1691 "(x + #1) * (x + #2) + #-1 * (x ^^^ #2 + #8) = #0")) : mout
1692 val nxt = ("Rewrite_Set",Rewrite_Set "SqRoot_simplify") : string * mstep
1694 ML> val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1695 val f = Form' (FormKF (~1,EdUndef,1,Nundef,"#-6 + #3 * x = #0")) : mout
1696 val nxt = ("Subproblem",Subproblem ("SqRoot.thy",[#,#])) : string * mstep
1697 \end{verbatim}}%size
1698 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:
1699 {\footnotesize\begin{verbatim}
1701 val it = ("Subproblem",Subproblem ("SqRoot.thy",["univariate","equation"]))
1703 ML> val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1706 (~1,EdUndef,1,Nundef,"Subproblem (SqRoot.thy, [univariate, equation])"))
1708 val nxt = ("Refine_Tacitly",Refine_Tacitly ["univariate","equation"])
1710 ML> val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1711 val nxt = ("Model_Problem",Model_Problem ["linear","univariate","equation"])
1712 \end{verbatim}}%size
1713 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.
1715 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.
1718 \section{The final phase: check the post-condition}
1719 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.
1721 Thus the post-condition is just mentioned, in our example for both, the problem and the subproblem:
1722 {\footnotesize\begin{verbatim}
1724 val it = ("Check_Postcond",Check_Postcond ["linear","univariate","equation"])
1726 ML> val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1727 val f = Form' (FormKF (~1,EdUndef,1,Nundef,"[x = #2]")) : mout
1729 ("Check_Postcond",Check_Postcond ["normalize","univariate","equation"])
1731 ML> val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1732 val f = Form' (FormKF (~1,EdUndef,0,Nundef,"[x = #2]")) : mout
1733 val nxt = ("End_Proof'",End_Proof') : string * mstep
1734 \end{verbatim}}%size
1735 The next tactic proposed by the system, {\tt End\_Proof'} indicates that the proof has finished successfully.\\
1737 {\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~!}
1741 \part{Systematic description}
1744 \chapter{The structure of the knowledge base}
1746 \section{Tactics and data}
1747 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
1748 \footnote{Some of these items are fetched by the tactics from intermediate storage within the ME, and not directly from the KB.}
1749 . The items are listed in alphabetical order in Tab.\ref{kb-items} on p.\pageref{kb-items}.
1751 \caption{Atomic items of the KB} \label{kb-items}
1754 \def\arraystretch{1.0}
1755 \begin{tabular}{lp{9.0cm}}
1756 abbrevation & description \\
1760 & associationlist of the evaluation-functions {\it eval\_fn}\\
1762 & evaluation-function for numerals and for predicates coded in SML\\
1764 & ruleset {\it rls} for simplifying expressions with {\it eval\_fn}s\\
1766 & formalization, i.e. a minimal formula representation of an example \\
1768 & a method, i.e. a datastructure holding all informations for the solving phase ({\it rew\_ord}, {\it scr}, etc.)\\
1770 & reference to a {\it met}\\
1772 & operator as key to an {\it eval\_fn} in a {\it calc\_list}\\
1774 & problem, i.e. a node in the problem-hierarchy\\
1776 & reference to a {\it pbl}\\
1780 & ruleset, i.e. a datastructure holding theorems {\it thm} and operators {\it op} for simplification (with a {\it rew\_ord})\\
1782 & ruleset for 'reverse rewriting' (an \isac-technique generating stepwise rewriting, e.g. for cancelling fractions)\\
1784 & script describing algorithms by tactics, part of a {\it met} \\
1786 & special ruleset calculating a normalform, associated with a {\it thy}\\
1788 & specification, i.e. a tripel ({\it thyID, pblID, metID})\\
1790 & substitution, i.e. a list of variable-value-pairs\\
1792 & Isabelle term, i.e. a formula\\
1798 & reference to a {\it thy} \\
1799 \end{tabular}\end{center}\end{table}
1801 The relations between tactics and data items are shown in Tab.\ref{tac-kb}on p.\pageref{tac-kb}.
1802 {\def\arraystretch{1.2}
1804 \caption{Which tactic uses which KB's item~?} \label{tac-kb}
1807 \begin{tabular}{|ll||cccc|ccc|cccc|} \hline
1808 tactic &input & & & &norm\_& &rew\_&rls &eval\_&eval\_&calc\_& \\
1809 & &thy &scr &Rrls&rls &thm &ord &Rrls&fn &rls &list &dsc\\
1812 &fmz & x & & & x & & & & & & & x \\
1813 &spec & & & & & & & & & & & \\
1815 \multicolumn{13}{|l|}{model phase}\\
1817 Add\_* &term & x & & & x & & & & & & & x \\
1818 FormFK &model & x & & & x & & & & & & & x \\
1820 \multicolumn{13}{|l|}{specify phase}\\
1823 &thyID & x & & & x & & & & x & x & & x \\
1825 &pblID & x & & & x & & & & x & x & & x \\
1827 &pblID & x & & & x & & & & x & x & & x \\
1829 &metID & x & & & x & & & & x & x & & x \\
1831 &metID & x & x & & x & & & & x & x & & x \\
1833 \multicolumn{13}{|l|}{solve phase}\\
1836 &thm & x & x & & & x &met & & x &met & & \\
1838 &thm & x & x & & & x &rls & & x &rls & & \\
1840 &thm & x & x & & & x &Rrls & & x &Rrls & & \\
1842 &rls & x & x & & & & & x & x & x & & \\
1844 &op & x & x & & & & & & & & x & \\
1846 &subs & x & & & x & & & & & & & \\
1847 & & & & & & & & & & & & \\
1849 &spec & x & x & & x & & & & x & x & & x \\
1850 &fmz & & & & & & & & & & & \\
1852 \end{tabular}\end{center}\end{table}
1855 \section{\isac's theories}
1856 \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}.
1858 \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}).
1860 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~!
1862 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.
1864 \caption{Theories in \isac-version I} \label{theories}
1867 \def\arraystretch{1.0}
1868 \begin{tabular}{lp{9.0cm}}
1869 theory & description \\
1873 & assigns identifiers to the functions defined in {\tt Isabelle2002/src/HOL/List.thy} and (intermediatly~?) defines some more list functions\\
1875 & {\tt eval\_fn} for the additional list functions\\
1877 & functions required for the evaluation of scripts\\
1879 & the respective {\tt eval\_fn}s\\
1881 & prerequisites for scripts: types, tactics, tacticals,\\
1883 & sets of tactics and functions for internal use\\
1888 & an intermediate hack for escaping type errors\\
1890 & {\it description}s for the formulas in {\it model}s and {\it problem}s\\
1892 & (re-)definition of operators; general predicates and functions for preconditions; theorems for the {\tt eval\_rls}\\
1894 & floating point numerals\\
1896 & basic notions for equations and equational systems\\
1900 & polynomial equations and equational systems \\
1902 & additional theorems for rationals\\
1904 & cancel, add and simplify rationals using (a generalization of) Euclids algorithm; respective reverse rulesets\\
1906 & equations on rationals\\
1908 & radicals; calculate normalform; respective reverse rulesets\\
1910 & equations on roots\\
1912 & equations on rationals and roots (i.e. on terms containing both operations)\\
1918 & logarithms and exponential functions\\
1920 & nonstandard analysis\\
1924 & applications of differentiaten (maxima-minima-problems)\\
1926 & (old) data for the test suite\\
1928 & collects all \isac-theoris.\\
1929 \end{tabular}\end{center}\end{table}
1933 \section{Data in {\tt *.thy}- and {\tt *.ML}-files}
1934 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}.
1936 \caption{Data in {\tt *.thy}- and {\tt *.ML}-files} \label{thy-ML}
1939 \def\arraystretch{1.0}
1940 \begin{tabular}{llp{7.7cm}}
1941 file & data & description \\
1946 & operators, predicates, functions, script-names ('{\tt Script} name \dots{\tt arguments}')
1949 & theorems: \isac{} uses Isabelles theorems if possible; additional theorems analoguous to such existing in Isabelle get the Isabelle-identifier attached an {\it I}
1953 & the theory defined by the actual {\tt *.thy}-file is made accessible to \isac
1956 & 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}
1959 & 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}
1961 & {\tt norm\_rls :=}
1962 & the canonical simplifier {\tt *\_simplify} is stored such that it is accessible for \isac
1964 & {\tt rew\_ord' :=}
1965 & the same for rewrite orders, if needed outside of one particular ruleset
1968 & the same for rulesets (ordinary rulesets, reverse rulesets and {\tt eval\_rls})
1970 & {\tt calc\_list :=}
1971 & the same for {\tt eval\_fn}s, if needed outside of one particular ruleset (e.g. for a tactic {\tt Calculate} in a script)
1974 & problems defined within this {\tt *.ML}-file are made accessible for \isac
1977 & methods defined within this {\tt *.ML}-file are made accessible for \isac
1979 \end{tabular}\end{center}\end{table}
1981 The order of the data-items within the theories should adhere to the order given in this list.
1983 \section{Formal description of the problem-hierarchy}
1986 \section{Script tactics}
1987 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.
1993 \part{Authoring on the knowledge}
1996 \section{Add a theorem}
1997 \section{Define and add a problem}
1998 \section{Define and add a predicate}
1999 \section{Define and add a method}
2008 \bibliography{bib/isac,bib/from-theses}