1 \documentclass[11pt,a4paper,headline,headcount,towside,nocenter]{report}
5 %\grmn@dq@error ...and \dq \string #1 is undefined}
6 %l.989 ...tch the problem type \\{\tt["squareroot",
8 \bibliographystyle{alpha}
10 \def\isac{${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$}
12 \title{\isac --- Interface for\\
13 Developers of Math Knowledge\\[1.0ex]
15 Tools for Experiments in\\
16 Symbolic Computation\\[1.0ex]}
17 \author{The \isac-Team\\
18 \tt isac-users@ist.tugraz.at\\[1.0ex]}
30 \section{``Authoring'' und ``Tutoring''}
31 {TO DO} Mathematik lernen -- verschiedene Autoren -- Isabelle
32 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.
33 \section{Der Inhalt des Dokuments}
34 \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.
36 \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.
38 Das Dokument ist eigenst\"andig; Basiswissen \"uber SML (für eine Einf\"uhrung siehe \cite{Paulson:91}), Terme und Umschreibung wird vorrausgesetzt.
40 %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.
42 Hinweis: SML Code, Verzeichnis, Dateien sind {\tt in 'tt' geschrieben}; besonders in {\tt ML>} ist das Kerngebiet schnell.
44 \paragraph{Versuchen Sie es!} Ein weiteres Anliegen dieses Textes ist, dem Leser Tipps f\"ur Versuche mit den Anwendungen zu geben.
46 \section{Gleich am Computer ausprobieren!}\label{get-started}
47 \paragraph{TO DO screenshot} Bevor Sie mit Ihren Versuchen beginnen, m\"ochten wir Ihnen noch einige Hinweise geben.
50 \item Shell aufmachen und die Datei mat-eng-de.sml \"offnen.
51 \item $>$ : Hinter diesem Zeichen (``Prompt'') stehen jene, die Sie selbst eingeben bzw. mit Copy und Paste aus der Datei kopieren.
52 \item Die Eingabe wird mit ``;'' und ``Enter'' abgeschlossen.
53 \item Zeilen, die nicht mit Prompt beginnen, werden vom Computer ausgegeben.
57 \part{Experimentelle Ann\"aherung}
59 \chapter{Terme und Theorien}
60 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.
62 \section{Von der Formel zum Term}
63 Um ein Beispiel zu nennen: Die Formel $a+b\cdot 3$ l\"asst sich in lesbarer Form so eingeben:
64 {\footnotesize\begin{verbatim}
66 val it = "a + b * 3" : string
68 \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:
69 {\footnotesize\begin{verbatim}
70 > str2term "a + b * 3";
72 Const ("op +", "[RealDef.real, RealDef.real] => RealDef.real") $
73 Free ("a", "RealDef.real") $
74 (Const ("op *", "[RealDef.real, RealDef.real] => RealDef.real") $ ... $
77 \noindent Jene Form braucht Isabelle intern zum rechnen. Sie heisst Term und ist nicht lesbar, daf\"ur aber speicherbar mit Hilfe von ``val'' (=value)
78 {\footnotesize\begin{verbatim}
79 > val term = str2term "a + b * 3";
81 Const ("op +", "[RealDef.real, RealDef.real] => RealDef.real") $
82 Free ("a", "RealDef.real") $
83 (Const ("op *", "[RealDef.real, RealDef.real] => RealDef.real") $ ... $
86 Der gespeicherte Term kann einer Funktion ``atomty'' \"ubergeben werden, die jenen in einer abstrakten Struktur zeigt:
87 {\footnotesize\begin{verbatim}
91 *** Const (op +, [real, real] => real)
93 *** . Const (op *, [real, real] => real)
94 *** . . Free (b, real)
95 *** . . Free (3, real)
102 \section{``Theory'' und ``Parsing``}
103 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{}.
105 {\footnotesize\begin{verbatim}
108 {ProtoPure, CPure, HOL, Set, Typedef, Fun, Product_Type, Lfp, Gfp,
109 Sum_Type, Relation, Record, Inductive, Transitive_Closure,
110 Wellfounded_Recursion, NatDef, Nat, NatArith, Divides, Power,
111 SetInterval, Finite_Set, Equiv, IntDef, Int, Datatype_Universe,
112 Datatype, Numeral, Bin, IntArith, Wellfounded_Relations, Recdef, IntDiv,
113 IntPower, NatBin, NatSimprocs, Relation_Power, PreList, List, Map,
114 Hilbert_Choice, Main, Lubs, PNat, PRat, PReal, RealDef, RealOrd,
115 RealInt, RealBin, RealArith0, RealArith, RComplete, RealAbs, RealPow,
116 Ring_and_Field, Complex_Numbers, Real, ListG, Tools, Script, Typefix,
117 Float, ComplexI, Descript, Atools, Simplify, Poly, Rational, PolyMinus,
118 Equation, LinEq, Root, RootEq, RatEq, RootRat, RootRatEq, PolyEq, Vect,
119 Calculus, Trig, LogExp, Diff, DiffApp, Integrate, EqSystem, Biegelinie,
120 AlgEin, Test, Isac} : Theory.theory
122 Die, die ein Mal enth\"alt ist groups.thy. Suchen Sie nach '*' unter der Adresse:
124 http://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/library/HOL/Groups.html
125 Hier wird Ihnen erkl\"art, wie das Mal vom Computer gelesen wird.
126 {\footnotesize\begin{verbatim}
128 fixes f :: "'a => 'a => 'a" (infixl "*" 70)
129 assumes assoc [ac_simps]: "a * b * c = a * (b * c)"
131 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).
133 Parsing entsteht durch einen string und eine theory. Es verwendet Informationen, die in der theory von Isabelle enthalten sind.
134 {\footnotesize\begin{verbatim}
136 val it = fn : Theory.theory -> string -> Thm.cterm Library.option
138 Dieser term kann wieder in seine einzelnen Teile zerlegt werden.
139 {\footnotesize\begin{verbatim}
140 > val it = (term_of o the) it;
142 Const ("op +", "[RealDef.real, RealDef.real] => RealDef.real") $
143 Free ("a", "RealDef.real") $
144 (Const ("op *", "[RealDef.real, RealDef.real] => RealDef.real") $ ... $
148 \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.
150 {\footnotesize\begin{verbatim}
152 > parse HOL.thy "2^^^3";
153 *** Inner lexical error at: "^^^3"
154 val it = None : Thm.cterm Library.option
156 ''Inner lexical error`` bedeutet, dass ein Fehler aufgetreten ist, vermutlich hat man sich vertippt.
158 {\footnotesize\begin{verbatim}
160 > parse HOL.thy "d_d x (a + x)";
161 val it = None : Thm.cterm Library.option
163 Fehlt ''Inner lexical error`` wurde der Parse nicht gefunden.
165 {\footnotesize\begin{verbatim}
167 > parse Rational.thy "2^^^3";
168 val it = Some "2 ^^^ 3" : Thm.cterm Library.option
171 {\footnotesize\begin{verbatim}
173 > val Some t4 = parse Rational.thy "d_d x (a + x)";
174 val t4 = "d_d x (a + x)" : Thm.cterm
177 {\footnotesize\begin{verbatim}
179 > val Some t5 = parse Diff.thy "d_d x (a + x)";
180 val t5 = "d_d x (a + x)" : Thm.cterm
183 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.
185 \section{Details von Termen}
186 Mit Hilfe der darunterliegenden Darstellung sieht man, dass ein cterm in einen term umgewandelt werden kann.
187 {\footnotesize\begin{verbatim}
189 val it = fn : Thm.cterm -> Term.term
191 Durch die Umwandlung eines cterms in einen term sieht man die einzelnen Teile des Terms. ''Free`` bedeutet, dass man die Variable \"andern kann.
192 {\footnotesize\begin{verbatim}
195 Free ("d_d", "[RealDef.real, RealDef.real] => RealDef.real") $ ... $
199 In diesem Fall sagt uns das ''Const``, dass die Variable eine Konstante ist, also ein Fixwert ist und immer die selbe Funktion hat.
200 {\footnotesize\begin{verbatim}
203 Const ("Diff.d_d", "[RealDef.real, RealDef.real] => RealDef.real") $ ... $
206 Sollten verschiedene Teile des Output nicht sichtbar sein, kann die Schriftgr\"osse ge\"andert werden.
207 {\footnotesize\begin{verbatim}
209 val it = fn : int -> unit
211 Zuerst gibt man die Schriftgr\"osse ein, danach den term, der gr\"osser werden soll.
212 {\footnotesize\begin{verbatim}
217 Free ("d_d", "[RealDef.real, RealDef.real] => RealDef.real") $
218 Free ("x", "RealDef.real") $
219 (Const ("op +", "[RealDef.real, RealDef.real] => RealDef.real") $
220 Free ("a", "RealDef.real") $ Free ("x", "RealDef.real"))
227 Const ("Diff.d_d", "[RealDef.real, RealDef.real] => RealDef.real") $
228 Free ("x", "RealDef.real") $
229 (Const ("op +", "[RealDef.real, RealDef.real] => RealDef.real") $
230 Free ("a", "RealDef.real") $ Free ("x", "RealDef.real"))
234 Eine andere Variante um den Unterschied der beiden Terme zu sehen ist folgende:
235 {\footnotesize\begin{verbatim}
236 > (*-4-*) val thy = Rational.thy;
238 {ProtoPure, CPure, HOL, Set, Typedef, Fun, Product_Type, Lfp, Gfp,
239 Sum_Type, Relation, Record, Inductive, Transitive_Closure,
240 Wellfounded_Recursion, NatDef, Nat, NatArith, Divides, Power,
241 SetInterval, Finite_Set, Equiv, IntDef, Int, Datatype_Universe,
242 Datatype, Numeral, Bin, IntArith, Wellfounded_Relations, Recdef, IntDiv,
243 IntPower, NatBin, NatSimprocs, Relation_Power, PreList, List, Map,
244 Hilbert_Choice, Main, Lubs, PNat, PRat, PReal, RealDef, RealOrd,
245 RealInt, RealBin, RealArith0, RealArith, RComplete, RealAbs, RealPow,
246 Ring_and_Field, Complex_Numbers, Real, ListG, Tools, Script, Typefix,
247 Float, ComplexI, Descript, Atools, Simplify, Poly, Rational}
249 > ((atomty) o term_of o the o (parse thy)) "d_d x (a + x)";
252 *** Free (d_d, [real, real] => real)
254 *** . Const (op +, [real, real] => real)
255 *** . . Free (a, real)
256 *** . . Free (x, real)
262 > (*-5-*) val thy = Diff.thy;
264 {ProtoPure, CPure, HOL, Set, Typedef, Fun, Product_Type, Lfp, Gfp,
265 Sum_Type, Relation, Record, Inductive, Transitive_Closure,
266 Wellfounded_Recursion, NatDef, Nat, NatArith, Divides, Power,
267 SetInterval, Finite_Set, Equiv, IntDef, Int, Datatype_Universe,
268 Datatype, Numeral, Bin, IntArith, Wellfounded_Relations, Recdef, IntDiv,
269 IntPower, NatBin, NatSimprocs, Relation_Power, PreList, List, Map,
270 Hilbert_Choice, Main, Lubs, PNat, PRat, PReal, RealDef, RealOrd,
271 RealInt, RealBin, RealArith0, RealArith, RComplete, RealAbs, RealPow,
272 Ring_and_Field, Complex_Numbers, Real, Calculus, Trig, ListG, Tools,
273 Script, Typefix, Float, ComplexI, Descript, Atools, Simplify, Poly,
274 Equation, LinEq, Root, RootEq, Rational, RatEq, RootRat, RootRatEq,
275 PolyEq, LogExp, Diff} : Theory.theory
277 > ((atomty) o term_of o the o (parse thy)) "d_d x (a + x)";
280 *** Const (Diff.d_d, [real, real] => real)
282 *** . Const (op +, [real, real] => real)
283 *** . . Free (a, real)
284 *** . . Free (x, real)
291 {\chapter{''Rewriting``}}
293 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.
295 {\footnotesize\begin{verbatim}
300 ((Term.term * Term.term) list -> Term.term * Term.term -> bool) ->
303 Thm.thm -> Term.term -> (Term.term * Term.term list) Library.option
310 rls' -> bool -> thm' -> cterm' -> (string * string list) Library.option
313 \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!
315 Zuerst legt man fest, dass es sich um eine Differenzierung handelt.
316 {\footnotesize\begin{verbatim}
317 > val thy' = "Diff.thy";
318 val thy' = "Diff.thy" : string
320 Dann gibt man die zu l\"osende Rechnung ein.
321 {\footnotesize\begin{verbatim}
322 > val ct = "d_d x (a + a * (2 + b))";
323 val ct = "d_d x (a + a * (2 + b))" : string
325 Anschließend gibt man bekannt, dass die Summenregel angewandt werden soll.
326 {\footnotesize\begin{verbatim}
327 > val thm = ("diff_sum","");
328 val thm = ("diff_sum", "") : string * string
330 Schliesslich wird die erste Ableitung angezeigt.
331 {\footnotesize\begin{verbatim}
332 > val Some (ct,_) = rewrite_inst thy' "tless_true" "eval_rls" true
333 [("bdv","x::real")] thm ct;#
334 val ct = "d_d x a + d_d x (a * (2 + b))" : cterm'
336 Will man auch die zweite Ableitung sehen, geht man so vor:
337 {\footnotesize\begin{verbatim}
338 > val thm = ("diff_prod_const","");
339 val thm = ("diff_prod_const", "") : string * string
341 Auch die zweite Ableitung wird sichtbar.
342 {\footnotesize\begin{verbatim}
343 > val Some (ct,_) = rewrite_inst thy' "tless_true" "eval_rls" true
344 [("bdv","x::real")] thm ct;#
345 val ct = "d_d x a + a * d_d x (2 + b)" : cterm'
348 {\section{M\"oglichkeiten von Rewriting}
349 Es gibt verscheidene Varianten von Rewriting, die alle eine bestimmte Bedeutung haben.
350 \textit{rewrite\_inst} bedeutet, dass die Liste der Terme vor dem Rewriting durch ein ''Theorem`` (ein mathematischer Begriff f\"ur einen Satz) ersetzt wird.
351 {\footnotesize\begin{verbatim}
358 bool -> 'a -> thm' -> cterm' -> (cterm' * cterm' list) Library.option
360 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.
361 {\footnotesize\begin{verbatim}
364 : theory' -> bool -> rls' -> cterm' -> (string * string list) Library.option
366 \textit{rewrite\_set\_inst} ist eine Kombination der beiden oben genannten M\"oglichkeiten.
367 {\footnotesize\begin{verbatim}
372 bool -> subs' -> rls' -> cterm' -> (string * string list) Library.option
374 Wenn man sehen m\"ochte, wie Rewriting bei den einzelnen Theorems funktioniert, kann man dies mit \textit{trace\_rewrite} versuchen.
375 {\footnotesize\begin{verbatim}
377 val it = fn : bool ref -> bool
378 > toggle trace_rewrite;
380 > toggle trace_rewrite;
381 val it = false : bool
385 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.
386 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.
387 Ein Beispiel f\"ur einen Regelsatz ist folgendes:
388 \footnotesize\begin{verbatim}
392 \footnotesize\begin{verbatim}
394 val it = "?s = ?t ==> ?t = ?s" : Thm.thm
398 {id = "rearrange_assoc",
399 scr = Script (Free ("empty_script", "RealDef.real")),
409 rew_ord = ("dummy_ord", fn),
419 rew_ord = ("dummy_ord", fn),
422 [Thm ("sym_radd_assoc", "?m1 + (?n1 + ?k1) = ?m1 + ?n1 + ?k1" [.]),
425 "?m1 * (?n1 * ?k1) = ?m1 * ?n1 * ?k1" [.])],
426 rew_ord = ("e_rew_ord", fn),
431 \section{Berechnung von Konstanten}
432 Sobald Konstanten in dem Bereich des Subterms sind, k\"onnen sie von einer Funktion berechnet werden:
433 \footnotesize\begin{verbatim}
441 Term.term -> Theory.theory -> (string * Term.term) Library.option) ->
442 cterm' -> (string * thm') Library.option
451 Term.term -> Theory.theory -> (string * Term.term) Library.option) ->
452 Term.term -> (Term.term * (string * Thm.thm)) Library.option
454 Man bekommt das Ergebnis und die Theorem bezieht sich darauf. Daher sind die folgenden mathematischen Rechnungen m\"oglich:
455 \footnotesize\begin{verbatim}
458 [("Vars", ("Tools.Vars", fn)), ("matches", ("Tools.matches", fn)),
459 ("lhs", ("Tools.lhs", fn)), ("plus", ("op +", fn)),
460 ("times", ("op *", fn)), ("divide_", ("HOL.divide", fn)),
461 ("power_", ("Atools.pow", fn)), ("is_const", ("Atools.is'_const", fn)),
462 ("le", ("op <", fn)), ("leq", ("op <=", fn)),
463 ("ident", ("Atools.ident", fn)), ("sqrt", ("Root.sqrt", fn)),
464 ("Test.is_root_free", ("is'_root'_free", fn)),
465 ("Test.contains_root", ("contains'_root", fn))]
473 Term.term -> Theory.theory -> (string * Term.term) Library.option))) list
475 Diese werden so angewendet:
476 \footnotesize\begin{verbatim}
481 \chapter{Termordnung}
482 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.
484 \section{Beispiel f\"ur Termordnungen}
485 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.
488 {\footnotesize\begin{verbatim}
490 val it = fn : bool -> Theory.theory -> subst -> Term.term * Term.term -> b ool
492 val it = fn : subst -> Term.term * Term.term -> bool
495 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.
500 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.
502 \section{Der ''Syntax`` des Scriptes}
503 Syntax beschreibt den Zusammenhang der einzelnen Zeichen und Zeichenfolgen mit den Theorien.
504 Er kann so definiert werden:
506 123\=123\=expr ::=\=$|\;\;$\=\kill
507 \>script ::= {\tt Script} id arg$\,^*$ = body\\
508 \>\>arg ::= id $\;|\;\;($ ( id :: type ) $)$\\
510 \>\>expr ::= \>\>{\tt let} id = expr $($ ; id = expr$)^*$ {\tt in} expr\\
511 \>\>\>$|\;$\>{\tt if} prop {\tt then} expr {\tt else} expr\\
512 \>\>\>$|\;$\>listexpr\\
514 \>\>\>$|\;$\>seqex id\\
515 \>\>seqex ::= \>\>{\tt While} prop {\tt Do} seqex\\
516 \>\>\>$|\;$\>{\tt Repeat} seqex\\
517 \>\>\>$|\;$\>{\tt Try} seqex\\
518 \>\>\>$|\;$\>seqex {\tt Or} seqex\\
519 \>\>\>$|\;$\>seqex {\tt @@} seqex\\
520 \>\>\>$|\;$\>tac $($ id $|$ listexpr $)^*$\\
525 \section{\"Uberpr\"ufung der Auswertung}
526 Das Kontrollsystem arbeitet mit den folgenden Script-Ausdr\"ucken, die {\it tacticals} genannt werden:
528 \item{{\tt while} prop {\tt Do} expr id}
529 \item{{\tt if} prop {\tt then} expr {\tt else} expr}
531 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:
533 \item{{\tt Repeat} expr id}
534 \item{{\tt Try} expr id}
535 \item{expr {\tt Or} expr id}
536 \item{expr {\tt @@} expr id}
549 ------------------------------- ALTER TEXT -------------------------------
551 \chapter{The hierarchy of problem types}\label{pbt}
552 \section{The standard-function for 'matching'}
553 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:
554 {\footnotesize\begin{verbatim}
556 val it = fn : theory -> term -> term -> bool
558 where the first of the two {\tt term} arguments is the particular term to be tested, and the second one is the pattern:
559 {\footnotesize\begin{verbatim}
560 ML> val t = (term_of o the o (parse thy)) "#3 * x^^^#2 = #1";
561 val t = Const (#,#) $ (# $ # $ (# $ #)) $ Free ("#1","RealDef.real") : term
563 ML> val p = (term_of o the o (parse thy)) "a * b^^^#2 = c";
564 val p = Const (#,#) $ (# $ # $ (# $ #)) $ Free ("c","RealDef.real") : term
570 *** . . Const ( RatArith.pow)
571 *** . . . Free ( b, )
572 *** . . . Free ( #2, )
577 val it = fn : term -> term
579 ML> val pat = free2var p;
580 val pat = Const (#,#) $ (# $ # $ (# $ #)) $ Var ((#,#),"RealDef.real") : term
581 ML> Sign.string_of_term (sign_of thy) pat;
582 val it = "?a * ?b ^^^ #2 = ?c" : cterm'
587 *** . . Var ((a, 0), )
588 *** . . Const ( RatArith.pow)
589 *** . . . Var ((b, 0), )
590 *** . . . Free ( #2, )
593 \end{verbatim}}%size % $
594 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:
595 {\footnotesize\begin{verbatim}
596 ML> matches thy t pat;
599 ML> val t2 = (term_of o the o (parse thy)) "x^^^#2 = #1";
600 val t2 = Const (#,#) $ (# $ # $ Free #) $ Free ("#1","RealDef.real") : term
601 ML> matches thy t2 pat;
602 val it = false : bool
604 ML> val pat2 = (term_of o the o (parse thy)) "?u^^^#2 = ?v";
605 val pat2 = Const (#,#) $ (# $ # $ Free #) $ Var ((#,#),"RealDef.real") : term
606 ML> matches thy t2 pat2;
608 \end{verbatim}}%size % $
610 \section{Accessing the hierarchy}
611 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):
612 {\footnotesize\begin{verbatim}
614 val it = fn : unit -> unit
618 ["equation", "univariate", "linear"],
619 ["equation", "univariate", "plain_square"],
620 ["equation", "univariate", "polynomial", "degree_two", "pq_formula"],
621 ["equation", "univariate", "polynomial", "degree_two", "abc_formula"],
622 ["equation", "univariate", "squareroot"],
623 ["equation", "univariate", "normalize"],
624 ["equation", "univariate", "sqroot-test"],
625 ["function", "derivative_of"],
626 ["function", "maximum_of", "on_interval"],
627 ["function", "make"],
628 ["tool", "find_values"],
629 ["functional", "inssort"]
633 The retrieve function for individual problem types is {\tt get\_pbt}
634 \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:
635 {\footnotesize\begin{verbatim}
637 val it = fn : pblID -> pbt
638 ML> get_pbt ["squareroot", "univariate", "equation"];
640 {met=[("SqRoot.thy","square_equation")],
641 ppc=[("#Given",(Const (#,#),Free (#,#))),
642 ("#Given",(Const (#,#),Free (#,#))),
643 ("#Given",(Const (#,#),Free (#,#))),
644 ("#Find",(Const (#,#),Free (#,#)))],
645 thy={ProtoPure, CPure, HOL, Ord, Set, subset, equalities, mono, Vimage, Fun,
646 Prod, Lfp, Relation, Trancl, WF, NatDef, Gfp, Sum, Inductive, Nat,
647 Arith, Divides, Power, Finite, Equiv, IntDef, Int, Univ, Datatype,
648 Numeral, Bin, IntArith, WF_Rel, Recdef, IntDiv, NatBin, List, Option,
649 Map, Record, RelPow, Sexp, String, Calculation, SVC_Oracle, Main,
650 Zorn, Filter, PNat, PRat, PReal, RealDef, RealOrd, RealInt, RealBin,
651 HyperDef, Descript, ListG, Tools, Script, Typefix, Atools, RatArith,
653 where_=[Const ("SqRoot.contains'_root","bool => bool") $
654 Free ("e_","bool")]} : pbt
655 \end{verbatim}}%size %$
656 where the records fields hold the following data:
658 \item [\tt thy]: the theory necessary for parsing the formulas
659 \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}.
660 \item [\tt met]: the list of methods solving this problem type.\\
663 The following function adds or replaces a problem type (after having it prepared using {\tt prep\_pbt})
664 {\footnotesize\begin{verbatim}
666 val it = fn : pbt * pblID -> unit
669 (["newtype","univariate","equation"],
670 [("#Given" ,["equality e_","solveFor v_","errorBound err_"]),
671 ("#Where" ,["contains_root (e_::bool)"]),
672 ("#Find" ,["solutions v_i_"])
674 [("SqRoot.thy","square_equation")]));
677 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}).
679 \section{Internals of the datastructure}
680 This subsection only serves for the implementation of the hierarchy browser and can be skipped by the authors of math knowledge.
682 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:
683 {\footnotesize\begin{verbatim}
685 {thy : theory, (* the nearest to the root,
686 which allows to compile that pbt *)
687 where_: term list, (* where - predicates *)
688 ppc : ((string * (* fields "#Given","#Find" *)
689 (term * (* description *)
692 met : metID list}; (* methods solving the pbt *)
694 Ptyp of string * (* key within pblID *)
695 pbt list * (* several pbts with different domIDs*)
697 val e_Ptyp = Ptyp ("empty",[],[]);
699 type ptyps = ptyp list;
700 val ptyps = ref ([e_Ptyp]:ptyps);
702 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.
704 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}.
708 \section{Match a formalization with a problem type}\label{pbl}
709 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.
710 {\footnotesize\begin{verbatim}
711 ML> val fmz = ["equality (#1 + #2 * x = #0)",
713 "solutions L"] : fmz;
714 val fmz = ["equality (#1 + #2 * x = #0)","solveFor x","solutions L"] : fmz
716 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:
717 {\footnotesize\begin{verbatim}
719 val it = fn : fmz -> pbt -> match'
721 ML> match_pbl fmz (get_pbt ["univariate","equation"]);
724 {Find=[Correct "solutions L"],
725 Given=[Correct "equality (#1 + #2 * x = #0)",Correct "solveFor x"],
726 Relate=[],Where=[Correct "matches (?a = ?b) (#1 + #2 * x = #0)"],With=[]}
729 ML> match_pbl fmz (get_pbt ["linear","univariate","equation"]);
732 {Find=[Correct "solutions L"],
733 Given=[Correct "equality (#1 + #2 * x = #0)",Correct "solveFor x"],
736 "matches ( x = #0) (#1 + #2 * x = #0) |
737 matches ( ?b * x = #0) (#1 + #2 * x = #0) |
738 matches (?a + x = #0) (#1 + #2 * x = #0) |
739 matches (?a + ?b * x = #0) (#1 + #2 * x = #0)"],
742 ML> match_pbl fmz (get_pbt ["squareroot","univariate","equation"]);
745 {Find=[Correct "solutions L"],
746 Given=[Correct "equality (#1 + #2 * x = #0)",Correct "solveFor x",
747 Missing "errorBound err_"],Relate=[],
748 Where=[False "contains_root #1 + #2 * x = #0 "],With=[]} : match'
750 The above formalization does not match the problem type \\{\tt["squareroot","univariate","equation"]} which is explained by the tags:
753 \> {\tt Missing:} the item is missing in the formalization as required by the problem type\\
754 \> {\tt Superfl:} the item is not required by the problem type\\
755 \> {\tt Correct:} the item is correct, or the precondition ({\tt Where}) is true\\
756 \> {\tt False:} the precondition ({\tt Where}) is false\\
757 \> {\tt Incompl:} the item is incomlete, or not yet input.\\
762 \section{Refine a problem specification}
763 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).
765 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
768 \item for all $F$ matching some $P_i$ must follow, that $F$ matches $P$
769 \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)
770 \item for all $F$ matching some $P$ must follow, that $F$ matches $P_n$\\
771 \end{enumerate}}%small
772 \noindent Let us give an example for the point (1.) and (2.) first:
773 {\footnotesize\begin{verbatim}
775 val it = fn : fmz -> pblID -> match list
777 ML> val fmz = ["equality (sqrt(#9+#4*x)=sqrt x + sqrt(#5+x))",
778 "solveFor x","errorBound (eps=#0)",
781 ML> refine fmz ["univariate","equation"];
782 *** pass ["equation","univariate"]
783 *** pass ["equation","univariate","linear"]
784 *** pass ["equation","univariate","plain_square"]
785 *** pass ["equation","univariate","polynomial"]
786 *** pass ["equation","univariate","squareroot"]
789 (["univariate","equation"],
790 {Find=[Correct "solutions L"],
791 Given=[Correct "equality (sqrt (#9 + #4 * x) = sqrt x + sqrt (#5 + x))",
792 Correct "solveFor x",Superfl "errorBound (eps = #0)"],Relate=[],
794 "matches (?a = ?b) (sqrt (#9 + #4 * x) = sqrt x + sqrt (#5 + x))"],
797 (["linear","univariate","equation"],
798 {Find=[Correct "solutions L"],
799 Given=[Correct "equality (sqrt (#9 + #4 * x) = sqrt x + sqrt (#5 + x))",
800 Correct "solveFor x",Superfl "errorBound (eps = #0)"],Relate=[],
801 Where=[False "(?a + ?b * x = #0) (sqrt (#9 + #4 * x#"],
804 (["plain_square","univariate","equation"],
805 {Find=[Correct "solutions L"],
806 Given=[Correct "equality (sqrt (#9 + #4 * x) = sqrt x + sqrt (#5 + x))",
807 Correct "solveFor x",Superfl "errorBound (eps = #0)"],Relate=[],
809 "matches (?a + ?b * x ^^^ #2 = #0)"],
812 (["polynomial","univariate","equation"],
813 {Find=[Correct "solutions L"],
814 Given=[Correct "equality (sqrt (#9 + #4 * x) = sqrt x + sqrt (#5 + x))",
815 Correct "solveFor x",Superfl "errorBound (eps = #0)"],Relate=[],
817 "is_polynomial_in sqrt (#9 + #4 * x) = sqrt x + sqrt (#5 + x) x"],
820 (["squareroot","univariate","equation"],
821 {Find=[Correct "solutions L"],
822 Given=[Correct "equality (sqrt (#9 + #4 * x) = sqrt x + sqrt (#5 + x))",
823 Correct "solveFor x",Correct "errorBound (eps = #0)"],Relate=[],
825 "contains_root sqrt (#9 + #4 * x) = sqrt x + sqrt (#5 + x) "],
826 With=[]})] : match list
827 \end{verbatim}}%size}%footnotesize\label{refine}
828 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.)).
830 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:
831 {\footnotesize\begin{verbatim}
832 ML> val fmz = ["equality (x+#1=#2)",
833 "solveFor x","errorBound (eps=#0)",
837 ML> refine fmz ["univariate","equation"];
838 *** pass ["equation","univariate"]
839 *** pass ["equation","univariate","linear"]
840 *** pass ["equation","univariate","plain_square"]
841 *** pass ["equation","univariate","polynomial"]
842 *** pass ["equation","univariate","squareroot"]
843 *** pass ["equation","univariate","normalize"]
846 (["univariate","equation"],
847 {Find=[Correct "solutions L"],
848 Given=[Correct "equality (x + #1 = #2)",Correct "solveFor x",
849 Superfl "errorBound (eps = #0)"],Relate=[],
850 Where=[Correct "matches (?a = ?b) (x + #1 = #2)"],With=[]}),
852 (["linear","univariate","equation"],
856 (["squareroot","univariate","equation"],
857 {Find=[Correct "solutions L"],
858 Given=[Correct "equality (x + #1 = #2)",Correct "solveFor x",
859 Correct "errorBound (eps = #0)"],Relate=[],
860 Where=[False "contains_root x + #1 = #2 "],With=[]}),
862 (["normalize","univariate","equation"],
863 {Find=[Correct "solutions L"],
864 Given=[Correct "equality (x + #1 = #2)",Correct "solveFor x",
865 Superfl "errorBound (eps = #0)"],Relate=[],Where=[],With=[]})]
868 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"]}.
870 This recursive search on the problem hierarchy can be done within a proof state. This leads to the next section.
873 \chapter{Methods}\label{met}
874 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.
876 \section{The scripts' syntax}
877 The syntax of scripts follows the definition given in Backus-normal-form:
880 123\=123\=expr ::=\=$|\;\;$\=\kill
881 \>script ::= {\tt Script} id arg$\,^*$ = body\\
882 \>\>arg ::= id $\;|\;\;($ ( id :: type ) $)$\\
884 \>\>expr ::= \>\>{\tt let} id = expr $($ ; id = expr$)^*$ {\tt in} expr\\
885 \>\>\>$|\;$\>{\tt if} prop {\tt then} expr {\tt else} expr\\
886 \>\>\>$|\;$\>listexpr\\
888 \>\>\>$|\;$\>seqex id\\
889 \>\>seqex ::= \>\>{\tt While} prop {\tt Do} seqex\\
890 \>\>\>$|\;$\>{\tt Repeat} seqex\\
891 \>\>\>$|\;$\>{\tt Try} seqex\\
892 \>\>\>$|\;$\>seqex {\tt Or} seqex\\
893 \>\>\>$|\;$\>seqex {\tt @@} seqex\\
894 \>\>\>$|\;$\>tac $($ id $|$ listexpr $)^*$\\
898 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.
900 Expressions containing some of the keywords {\tt let}, {\tt if} etc. are called {\bf script-expressions}.
902 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,
905 \section{Control the flow of evaluation}
906 The flow of control is managed by the following script-expressions called {\it tacticals}.
908 \item{{\tt while} prop {\tt Do} expr id}
909 \item{{\tt if} prop {\tt then} expr {\tt else} expr}
911 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)
913 \item{{\tt Repeat} expr id}
914 \item{{\tt Try} expr id}
915 \item{expr {\tt Or} expr id}
916 \item{expr {\tt @@} expr id}
924 \chapter{Do a calculational proof}
925 First we list all the tactics available so far (this list may be extended during further development of \isac).
927 \section{Tactics for doing steps in calculations}
930 \section{The functionality of the math engine}
931 A proof is being started in the math engine {\tt me} by the tactic
932 \footnote{In the present version a tactic is of type {\tt mstep}.}
933 {\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.
935 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 ...
936 {\footnotesize\begin{verbatim}
937 ML> val fmz = ["equality ((x+#1)*(x+#2)=x^^^#2+#8)","solveFor x",
938 "errorBound (eps=#0)","solutions L"];
940 ["equality ((x+#1)*(x+#2)=x^^^#2+#8)","solveFor x","errorBound (eps=#0)",
941 "solutions L"] : string list
943 ML> val spec as (dom, pbt, met) = ("SqRoot.thy",["univariate","equation"],
944 ("SqRoot.thy","no_met"));
945 val dom = "SqRoot.thy" : string
946 val pbt = ["univariate","equation"] : string list
947 val met = ("SqRoot.thy","no_met") : string * string
949 ... 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.
951 Nevertheless this specification is sufficient for automatically solving the equation --- the appropriate method will be found by refinement within the hierarchy of problem types.
954 \section{Initialize the calculation}
955 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.
956 {\footnotesize\begin{verbatim}
957 ML> val (mID,m) = ("Init_Proof",Init_Proof (fmz, (dom,pbt,met)));
958 val mID = "Init_Proof" : string
961 (["equality ((x+#1)*(x+#2)=x^^^#2+#8)","solveFor x","errorBound (eps=#0)",
962 "solutions L"],("SqRoot.thy",[#,#],(#,#))) : mstep
964 ML> val (p,_,f,nxt,_,pt) = me (mID,m) e_pos' c EmptyPtree;
965 val p = ([],Pbl) : pos'
966 val f = Form' (PpcKF (0,EdUndef,0,Nundef,(#,#))) : mout
967 val nxt = ("Refine_Tacitly",Refine_Tacitly ["univariate","equation"])
972 {branch=#,cell=#,env=#,loc=#,meth=#,model=#,origin=#,ostate=#,probl=#,
973 result=#,spec=#},[]) : ptree
975 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'}).
977 We can convince ourselves, that the problem is still empty, by increasing {\tt Compiler.Control.Print.printDepth}:
978 {\footnotesize\begin{verbatim}
979 ML> Compiler.Control.Print.printDepth:=8; (*4 default*)
988 {Find=[Incompl "solutions []"],
989 Given=[Incompl "equality",Incompl "solveFor"],Relate=[],
990 Where=[False "matches (?a = ?b) e_"],With=[]}))) : mout
992 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).\\
994 {\it In the sequel we will omit output of the {\tt me} if it is not important for the respective context}.\\
996 In general, the dialog guide will hide the following two tactics {\tt Refine\_Tacitly} and {\tt Model\_Problem} from the user.
997 {\footnotesize\begin{verbatim}
999 val it = ("Refine_Tacitly",Refine_Tacitly ["univariate","equation"])
1002 ML> val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1003 val nxt = ("Model_Problem",Model_Problem ["normalize","univariate","equation"])
1006 ML> val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1007 \end{verbatim}}%size
1010 \section{The phase of modeling}
1011 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}.
1013 {\footnotesize\begin{verbatim}
1016 ("Add_Given",Add_Given "equality ((x + #1) * (x + #2) = x ^^^ #2 + #8)")
1019 ML> val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1020 val nxt = ("Add_Given",Add_Given "solveFor x") : string * mstep
1022 ML> val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1023 val nxt = ("Add_Find",Add_Find "solutions L") : string * mstep
1025 ML> val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1026 val f = Form' (PpcKF (0,EdUndef,0,Nundef,(#,#))) : mout
1027 \end{verbatim}}%size
1028 \noindent Now the problem is 'modeled', all items are input. We convince ourselves by increasing {\tt Compiler.Control.Print.printDepth} once more.
1029 {\footnotesize\begin{verbatim}
1030 ML> Compiler.Control.Print.printDepth:=8;
1035 (0,EdUndef,0,Nundef,
1037 {Find=[Correct "solutions L"],
1038 Given=[Correct "equality ((x + #1) * (x + #2) = x ^^^ #2 + #8)",
1039 Correct "solveFor x"],Relate=[],Where=[],With=[]}))) : mout
1040 \end{verbatim}}%size
1041 %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.
1043 \section{The phase of specification}
1044 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.
1045 {\footnotesize\begin{verbatim}
1047 val it = ("Specify_Domain",Specify_Domain "SqRoot.thy") : string * mstep
1049 ML> val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1051 ("Specify_Problem",Specify_Problem ["normalize","univariate","equation"])
1056 {branch=#,cell=#,env=#,loc=#,meth=#,model=#,origin=#,ostate=#,probl=#,
1057 result=#,spec=#},[]) : ptree
1058 \end{verbatim}}%size
1059 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.
1060 {\footnotesize\begin{verbatim}
1061 ML> val nxt = ("Specify_Problem",
1062 Specify_Problem ["polynomial","univariate","equation"]);
1063 ML> val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1064 val f = Form' (PpcKF (0,EdUndef,0,Nundef,(#,#))) : mout
1066 ("Refine_Problem",Refine_Problem ["normalize","univariate","equation"])
1069 ML> val nxt = ("Specify_Problem",
1070 Specify_Problem ["linear","univariate","equation"]);
1071 ML> val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1075 (0,EdUndef,0,Nundef,
1076 (Problem ["linear","univariate","equation"],
1077 {Find=[Correct "solutions L"],
1078 Given=[Correct "equality ((x + #1) * (x + #2) = x ^^^ #2 + #8)",
1079 Correct "solveFor x"],Relate=[],
1081 "matches (?a + ?b * x = #0) ((x + #1) * (x + #2) = x ^^^ #2 + #8)"],
1083 \end{verbatim}}%size
1084 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"]}.
1085 {\footnotesize\begin{verbatim}
1086 ML> val nxt = ("Refine_Problem",
1087 Refine_Problem ["linear","univariate","equation
1088 ML> val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1089 val f = Problems (RefinedKF [NoMatch #]) : mout
1091 ML> Compiler.Control.Print.printDepth:=9;f;Compiler.Control.Print.printDepth:=4;
1096 (["linear","univariate","equation"],
1097 {Find=[Correct "solutions L"],
1098 Given=[Correct "equality ((x + #1) * (x + #2) = x ^^^ #2 + #8)",
1099 Correct "solveFor x"],Relate=[],
1101 "matches (?a + ?b * x = #0) ((x + #1) * (x + #2) = x ^^^ #2 + #8)"],
1104 ML> val nxt = ("Refine_Problem",Refine_Problem ["univariate","equation"]);
1105 ML> val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1108 (RefinedKF [Matches #,NoMatch #,NoMatch #,NoMatch #,NoMatch #,Matches #])
1112 ML> Compiler.Control.Print.printDepth:=9;f;Compiler.Control.Print.printDepth:=4;
1117 (["univariate","equation"],
1118 {Find=[Correct "solutions L"],
1119 Given=[Correct "equality ((x + #1) * (x + #2) = x ^^^ #2 + #8)",
1120 Correct "solveFor x"],Relate=[],
1124 (["linear","univariate","equation"],
1125 {Find=[Correct "solutions L"],
1126 Given=[Correct "equality ((x + #1) * (x + #2) = x ^^^ #2 + #8)",
1127 Correct "solveFor x"],Relate=[],
1129 "matches (?a + ?b * x = #0) ((x + #1) * (x + #2) = x ^^^ #2 + #8)"],
1135 (["normalize","univariate","equation"],
1136 {Find=[Correct "solutions L"],
1137 Given=[Correct "equality ((x + #1) * (x + #2) = x ^^^ #2 + #8)",
1138 Correct "solveFor x"],Relate=[],Where=[],With=[]})]) : mout
1139 \end{verbatim}}%size
1140 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~!
1142 \section{The phase of solving}
1143 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}:
1144 {\footnotesize\begin{verbatim}
1146 val it = ("Apply_Method",Apply_Method ("SqRoot.thy","norm_univar_equation"))
1149 ML> val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1151 Form' (FormKF (~1,EdUndef,1,Nundef,"(x + #1) * (x + #2) = x ^^^ #2 + #8"))
1154 ("rnorm_equation_add","~ ?b =!= #0 ==> (?a = ?b) = (?a + #-1 * ?b = #0)"))
1156 ML> val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1158 Form' (FormKF (~1,EdUndef,1,Nundef,
1159 "(x + #1) * (x + #2) + #-1 * (x ^^^ #2 + #8) = #0")) : mout
1160 val nxt = ("Rewrite_Set",Rewrite_Set "SqRoot_simplify") : string * mstep
1162 ML> val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1163 val f = Form' (FormKF (~1,EdUndef,1,Nundef,"#-6 + #3 * x = #0")) : mout
1164 val nxt = ("Subproblem",Subproblem ("SqRoot.thy",[#,#])) : string * mstep
1165 \end{verbatim}}%size
1166 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:
1167 {\footnotesize\begin{verbatim}
1169 val it = ("Subproblem",Subproblem ("SqRoot.thy",["univariate","equation"]))
1171 ML> val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1174 (~1,EdUndef,1,Nundef,"Subproblem (SqRoot.thy, [univariate, equation])"))
1176 val nxt = ("Refine_Tacitly",Refine_Tacitly ["univariate","equation"])
1178 ML> val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1179 val nxt = ("Model_Problem",Model_Problem ["linear","univariate","equation"])
1180 \end{verbatim}}%size
1181 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.
1183 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.
1186 \section{The final phase: check the post-condition}
1187 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.
1189 Thus the post-condition is just mentioned, in our example for both, the problem and the subproblem:
1190 {\footnotesize\begin{verbatim}
1192 val it = ("Check_Postcond",Check_Postcond ["linear","univariate","equation"])
1194 ML> val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1195 val f = Form' (FormKF (~1,EdUndef,1,Nundef,"[x = #2]")) : mout
1197 ("Check_Postcond",Check_Postcond ["normalize","univariate","equation"])
1199 ML> val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1200 val f = Form' (FormKF (~1,EdUndef,0,Nundef,"[x = #2]")) : mout
1201 val nxt = ("End_Proof'",End_Proof') : string * mstep
1202 \end{verbatim}}%size
1203 The next tactic proposed by the system, {\tt End\_Proof'} indicates that the proof has finished successfully.\\
1205 {\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~!}
1209 \part{Systematic description}
1212 \chapter{The structure of the knowledge base}
1214 \section{Tactics and data}
1215 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
1216 \footnote{Some of these items are fetched by the tactics from intermediate storage within the ME, and not directly from the KB.}
1217 . The items are listed in alphabetical order in Tab.\ref{kb-items} on p.\pageref{kb-items}.
1219 \caption{Atomic items of the KB} \label{kb-items}
1222 \def\arraystretch{1.0}
1223 \begin{tabular}{lp{9.0cm}}
1224 abbrevation & description \\
1228 & associationlist of the evaluation-functions {\it eval\_fn}\\
1230 & evaluation-function for numerals and for predicates coded in SML\\
1232 & ruleset {\it rls} for simplifying expressions with {\it eval\_fn}s\\
1234 & formalization, i.e. a minimal formula representation of an example \\
1236 & a method, i.e. a datastructure holding all informations for the solving phase ({\it rew\_ord}, {\it scr}, etc.)\\
1238 & reference to a {\it met}\\
1240 & operator as key to an {\it eval\_fn} in a {\it calc\_list}\\
1242 & problem, i.e. a node in the problem-hierarchy\\
1244 & reference to a {\it pbl}\\
1248 & ruleset, i.e. a datastructure holding theorems {\it thm} and operators {\it op} for simplification (with a {\it rew\_ord})\\
1250 & ruleset for 'reverse rewriting' (an \isac-technique generating stepwise rewriting, e.g. for cancelling fractions)\\
1252 & script describing algorithms by tactics, part of a {\it met} \\
1254 & special ruleset calculating a normalform, associated with a {\it thy}\\
1256 & specification, i.e. a tripel ({\it thyID, pblID, metID})\\
1258 & substitution, i.e. a list of variable-value-pairs\\
1260 & Isabelle term, i.e. a formula\\
1266 & reference to a {\it thy} \\
1267 \end{tabular}\end{center}\end{table}
1269 The relations between tactics and data items are shown in Tab.\ref{tac-kb}on p.\pageref{tac-kb}.
1270 {\def\arraystretch{1.2}
1272 \caption{Which tactic uses which KB's item~?} \label{tac-kb}
1275 \begin{tabular}{|ll||cccc|ccc|cccc|} \hline
1276 tactic &input & & & &norm\_& &rew\_&rls &eval\_&eval\_&calc\_& \\
1277 & &thy &scr &Rrls&rls &thm &ord &Rrls&fn &rls &list &dsc\\
1280 &fmz & x & & & x & & & & & & & x \\
1281 &spec & & & & & & & & & & & \\
1283 \multicolumn{13}{|l|}{model phase}\\
1285 Add\_* &term & x & & & x & & & & & & & x \\
1286 FormFK &model & x & & & x & & & & & & & x \\
1288 \multicolumn{13}{|l|}{specify phase}\\
1291 &thyID & x & & & x & & & & x & x & & x \\
1293 &pblID & x & & & x & & & & x & x & & x \\
1295 &pblID & x & & & x & & & & x & x & & x \\
1297 &metID & x & & & x & & & & x & x & & x \\
1299 &metID & x & x & & x & & & & x & x & & x \\
1301 \multicolumn{13}{|l|}{solve phase}\\
1304 &thm & x & x & & & x &met & & x &met & & \\
1306 &thm & x & x & & & x &rls & & x &rls & & \\
1308 &thm & x & x & & & x &Rrls & & x &Rrls & & \\
1310 &rls & x & x & & & & & x & x & x & & \\
1312 &op & x & x & & & & & & & & x & \\
1314 &subs & x & & & x & & & & & & & \\
1315 & & & & & & & & & & & & \\
1317 &spec & x & x & & x & & & & x & x & & x \\
1318 &fmz & & & & & & & & & & & \\
1320 \end{tabular}\end{center}\end{table}
1323 \section{\isac's theories}
1324 \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}.
1326 \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}).
1328 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~!
1330 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.
1332 \caption{Theories in \isac-version I} \label{theories}
1335 \def\arraystretch{1.0}
1336 \begin{tabular}{lp{9.0cm}}
1337 theory & description \\
1341 & assigns identifiers to the functions defined in {\tt Isabelle2002/src/HOL/List.thy} and (intermediatly~?) defines some more list functions\\
1343 & {\tt eval\_fn} for the additional list functions\\
1345 & functions required for the evaluation of scripts\\
1347 & the respective {\tt eval\_fn}s\\
1349 & prerequisites for scripts: types, tactics, tacticals,\\
1351 & sets of tactics and functions for internal use\\
1356 & an intermediate hack for escaping type errors\\
1358 & {\it description}s for the formulas in {\it model}s and {\it problem}s\\
1360 & (re-)definition of operators; general predicates and functions for preconditions; theorems for the {\tt eval\_rls}\\
1362 & floating point numerals\\
1364 & basic notions for equations and equational systems\\
1368 & polynomial equations and equational systems \\
1370 & additional theorems for rationals\\
1372 & cancel, add and simplify rationals using (a generalization of) Euclids algorithm; respective reverse rulesets\\
1374 & equations on rationals\\
1376 & radicals; calculate normalform; respective reverse rulesets\\
1378 & equations on roots\\
1380 & equations on rationals and roots (i.e. on terms containing both operations)\\
1386 & logarithms and exponential functions\\
1388 & nonstandard analysis\\
1392 & applications of differentiaten (maxima-minima-problems)\\
1394 & (old) data for the test suite\\
1396 & collects all \isac-theoris.\\
1397 \end{tabular}\end{center}\end{table}
1401 \section{Data in {\tt *.thy}- and {\tt *.ML}-files}
1402 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}.
1404 \caption{Data in {\tt *.thy}- and {\tt *.ML}-files} \label{thy-ML}
1407 \def\arraystretch{1.0}
1408 \begin{tabular}{llp{7.7cm}}
1409 file & data & description \\
1414 & operators, predicates, functions, script-names ('{\tt Script} name \dots{\tt arguments}')
1417 & theorems: \isac{} uses Isabelles theorems if possible; additional theorems analoguous to such existing in Isabelle get the Isabelle-identifier attached an {\it I}
1421 & the theory defined by the actual {\tt *.thy}-file is made accessible to \isac
1424 & 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}
1427 & 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}
1429 & {\tt norm\_rls :=}
1430 & the canonical simplifier {\tt *\_simplify} is stored such that it is accessible for \isac
1432 & {\tt rew\_ord' :=}
1433 & the same for rewrite orders, if needed outside of one particular ruleset
1436 & the same for rulesets (ordinary rulesets, reverse rulesets and {\tt eval\_rls})
1438 & {\tt calc\_list :=}
1439 & the same for {\tt eval\_fn}s, if needed outside of one particular ruleset (e.g. for a tactic {\tt Calculate} in a script)
1442 & problems defined within this {\tt *.ML}-file are made accessible for \isac
1445 & methods defined within this {\tt *.ML}-file are made accessible for \isac
1447 \end{tabular}\end{center}\end{table}
1449 The order of the data-items within the theories should adhere to the order given in this list.
1451 \section{Formal description of the problem-hierarchy}
1454 \section{Script tactics}
1455 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.
1461 \part{Authoring on the knowledge}
1464 \section{Add a theorem}
1465 \section{Define and add a problem}
1466 \section{Define and add a predicate}
1467 \section{Define and add a method}
1476 \bibliography{bib/isac,bib/from-theses}