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{Alexandra Hirn und Eva Rott\\
18 \tt isac-users@ist.tugraz.at\\[1.0ex]}
30 \section{``Authoring'' und ``Tutoring''}
31 \paragraph{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\"ur 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 Problemen, f\"ur L\"osungsmethoden etc. Wir beginnen mit mathematischen Formeln.
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 dazu eine andere Darstellung f\"u Formeln. Diese kann man mit der Funktion {\tt 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 {\tt term} und ist nicht f\"ur den Menschen zum lesen gedacht. Wir wollen sie {\tt val} (= value) auf {\tt t} speichern
78 {\footnotesize\begin{verbatim}
79 > val t = 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 \footnotesize\begin{verbatim}
89 Const ("op +", "[RealDef.real, RealDef.real] => RealDef.real") $
90 Free ("a", "RealDef.real") $
91 (Const ("op *", "[RealDef.real, RealDef.real] => RealDef.real") $ ... $
93 > parse Isac.thy "a + b * 3";
94 val it = Some "a + b * 3" : Thm.cterm Library.option
95 > val t = parse Isac.thy "a + b * 3";
96 val t = Some "a + b * 3" : Thm.cterm Library.option
98 Der gespeicherte term {\tt t} kann einer Funktion {\tt atomty} \"ubergeben werden, die diesen in einer dritten Form zeigt:
99 {\footnotesize\begin{verbatim}
103 *** Const (op +, [real, real] => real)
105 *** . Const (op *, [real, real] => real)
106 *** . . Free (b, real)
107 *** . . Free (3, real)
112 Diese Darstellung nennt man ``abstract syntax'' und macht unmittelbar klar, dass man a und b nicht addieren kann, weil ein Mal vorhanden ist.
114 \section{``Theory'' und ``Parsing``}
115 Der Unterschied zwischen \isac{} und bisheriger Mathematiksoftware (GeoGebra, Mathematica, Maple, Derive etc.) ist, dass das mathematische Wissen nicht im Programmcode steht, sondern in den theories.
116 Die mathematischen Festlegungen des CTP werden in den theories abgelegt und sind nicht in Programmiersprachen, sondern in einer f\"ur Mathematik-lernende Personen lesbaren Form geschrieben. Das Wissen von \isac{} beinhaltet folgende {\tt thy}:
117 {\footnotesize\begin{verbatim}
120 {ProtoPure, CPure, HOL, Set, Typedef, Fun, Product_Type, Lfp, Gfp,
121 Sum_Type, Relation, Record, Inductive, Transitive_Closure,
122 Wellfounded_Recursion, NatDef, Nat, NatArith, Divides, Power,
123 SetInterval, Finite_Set, Equiv, IntDef, Int, Datatype_Universe,
124 Datatype, Numeral, Bin, IntArith, Wellfounded_Relations, Recdef, IntDiv,
125 IntPower, NatBin, NatSimprocs, Relation_Power, PreList, List, Map,
126 Hilbert_Choice, Main, Lubs, PNat, PRat, PReal, RealDef, RealOrd,
127 RealInt, RealBin, RealArith0, RealArith, RComplete, RealAbs, RealPow,
128 Ring_and_Field, Complex_Numbers, Real, ListG, Tools, Script, Typefix,
129 Float, ComplexI, Descript, Atools, Simplify, Poly, Rational, PolyMinus,
130 Equation, LinEq, Root, RootEq, RatEq, RootRat, RootRatEq, PolyEq, Vect,
131 Calculus, Trig, LogExp, Diff, DiffApp, Integrate, EqSystem, Biegelinie,
132 AlgEin, Test, Isac} : Theory.theory
134 Dass das Mal vor dem Plus berechnet wird, ist so festgelegt:
135 {\footnotesize\begin{verbatim}
137 fixes f :: "'a => 'a => 'a" (infixl "*" 70)
138 assumes assoc [ac_simps]: "a * b * c = a * (b * c)"
140 Ohne weitere Erkl\"arungen: 70 bedeutet, dass Mal eine hohe Priorit\"at hat als Plus (hier liegt der Wert zwischen 50 und 60).
142 Parsing entsteht durch einen string und eine theory. Es verwendet Informationen, die in der theory von Isabelle enthalten sind.
143 {\footnotesize\begin{verbatim}
145 val it = fn : Theory.theory -> string -> Thm.cterm Library.option
147 Dieser term kann wieder in seine einzelnen Teile zerlegt werden.
148 {\footnotesize\begin{verbatim}
149 > val it = (term_of o the) it;
151 Const ("op +", "[RealDef.real, RealDef.real] => RealDef.real") $
152 Free ("a", "RealDef.real") $
153 (Const ("op *", "[RealDef.real, RealDef.real] => RealDef.real") $ ... $
157 \paragraph{Versuchen Sie es!} Das mathematische Wissen w\"achst mit jeder {\tt thy} von ProtoPure bis Isac. In den folgenden Beispielen wird gezeigt, wie das Wissen w\"achst.
159 {\footnotesize\begin{verbatim}
161 > parse HOL.thy "2^^^3";
162 *** Inner lexical error at: "^^^3"
163 val it = None : Thm.cterm Library.option
165 ''Inner lexical error`` und ''None`` bedeuten, dass ein Fehler aufgetreten ist, denn das Wissen \"uber {\tt *} findet sich erst in der theorie group.
167 {\footnotesize\begin{verbatim}
169 > parse HOL.thy "d_d x (a + x)";
170 val it = None : Thm.cterm Library.option
172 Hier wiederum ist noch kein Wissen \"uber das Differenzieren vorhanden.
174 {\footnotesize\begin{verbatim}
176 > parse Rational.thy "2^^^3";
177 val it = Some "2 ^^^ 3" : Thm.cterm Library.option
180 {\footnotesize\begin{verbatim}
182 > val Some t4 = parse Rational.thy "d_d x (a + x)";
183 val t4 = "d_d x (a + x)" : Thm.cterm
186 {\footnotesize\begin{verbatim}
188 > val Some t5 = parse Diff.thy "d_d x (a + x)";
189 val t5 = "d_d x (a + x)" : Thm.cterm
191 Die letzen drei Aufgaben k\"onnen schon gel\"ost werden, da Rational.thy \"uber das n\"otige Wissen verf\"ugt.
193 \section{Details von Termen}
194 Mit Hilfe der darunterliegenden Darstellung sieht man, dass ein cterm in einen term umgewandelt werden kann.
195 {\footnotesize\begin{verbatim}
197 val it = fn : Thm.cterm -> Term.term
199 Durch die Umwandlung eines cterms in einen term sieht man die einzelnen Teile des Terms. ''Free`` bedeutet, dass man die Variable \"andern kann.
200 {\footnotesize\begin{verbatim}
203 Free ("d_d", "[RealDef.real, RealDef.real] => RealDef.real") $ ... $
207 In diesem Fall sagt uns das ''Const``, dass die Variable eine Konstante ist, also ein Fixwert, der immer die selbe Funktion hat.
208 {\footnotesize\begin{verbatim}
211 Const ("Diff.d_d", "[RealDef.real, RealDef.real] => RealDef.real") $ ... $
214 Sollten verschiedene Teile des ''output`` (= das vom Computer Ausgegebene) nicht sichtbar sein, kann man mit einem bestimmten Befehl alles angezeigt werden.
215 {\footnotesize\begin{verbatim}
217 val it = fn : int -> unit
219 Zuerst gibt man den Befehl ein, danach den term, der gr\"osser werden soll. Dabei kann man selbst einen Wert f\"ur die L\"ange bestimmen.
220 {\footnotesize\begin{verbatim}
225 Free ("d_d", "[RealDef.real, RealDef.real] => RealDef.real") $
226 Free ("x", "RealDef.real") $
227 (Const ("op +", "[RealDef.real, RealDef.real] => RealDef.real") $
228 Free ("a", "RealDef.real") $ Free ("x", "RealDef.real"))
235 Const ("Diff.d_d", "[RealDef.real, RealDef.real] => RealDef.real") $
236 Free ("x", "RealDef.real") $
237 (Const ("op +", "[RealDef.real, RealDef.real] => RealDef.real") $
238 Free ("a", "RealDef.real") $ Free ("x", "RealDef.real"))
241 \paragraph{Versuchen Sie es!}
242 Eine andere Variante um den Unterschied der beiden Terme zu sehen ist folgende:
243 {\footnotesize\begin{verbatim}
244 > (*-4-*) val thy = Rational.thy;
246 {ProtoPure, CPure, HOL, Set, Typedef, Fun, Product_Type, Lfp, Gfp,
247 Sum_Type, Relation, Record, Inductive, Transitive_Closure,
248 Wellfounded_Recursion, NatDef, Nat, NatArith, Divides, Power,
249 SetInterval, Finite_Set, Equiv, IntDef, Int, Datatype_Universe,
250 Datatype, Numeral, Bin, IntArith, Wellfounded_Relations, Recdef, IntDiv,
251 IntPower, NatBin, NatSimprocs, Relation_Power, PreList, List, Map,
252 Hilbert_Choice, Main, Lubs, PNat, PRat, PReal, RealDef, RealOrd,
253 RealInt, RealBin, RealArith0, RealArith, RComplete, RealAbs, RealPow,
254 Ring_and_Field, Complex_Numbers, Real, ListG, Tools, Script, Typefix,
255 Float, ComplexI, Descript, Atools, Simplify, Poly, Rational}
257 > ((atomty) o term_of o the o (parse thy)) "d_d x (a + x)";
260 *** Free (d_d, [real, real] => real)
262 *** . Const (op +, [real, real] => real)
263 *** . . Free (a, real)
264 *** . . Free (x, real)
270 > (*-5-*) val thy = Diff.thy;
272 {ProtoPure, CPure, HOL, Set, Typedef, Fun, Product_Type, Lfp, Gfp,
273 Sum_Type, Relation, Record, Inductive, Transitive_Closure,
274 Wellfounded_Recursion, NatDef, Nat, NatArith, Divides, Power,
275 SetInterval, Finite_Set, Equiv, IntDef, Int, Datatype_Universe,
276 Datatype, Numeral, Bin, IntArith, Wellfounded_Relations, Recdef, IntDiv,
277 IntPower, NatBin, NatSimprocs, Relation_Power, PreList, List, Map,
278 Hilbert_Choice, Main, Lubs, PNat, PRat, PReal, RealDef, RealOrd,
279 RealInt, RealBin, RealArith0, RealArith, RComplete, RealAbs, RealPow,
280 Ring_and_Field, Complex_Numbers, Real, Calculus, Trig, ListG, Tools,
281 Script, Typefix, Float, ComplexI, Descript, Atools, Simplify, Poly,
282 Equation, LinEq, Root, RootEq, Rational, RatEq, RootRat, RootRatEq,
283 PolyEq, LogExp, Diff} : Theory.theory
285 > ((atomty) o term_of o the o (parse thy)) "d_d x (a + x)";
288 *** Const (Diff.d_d, [real, real] => real)
290 *** . Const (op +, [real, real] => real)
291 *** . . Free (a, real)
292 *** . . Free (x, real)
299 \chapter{''Rewriting``}
300 \section{Was ist Rewriting?}
301 Bei Rewriting handelt es sich um das Umformen von Termen nach vorgegebenen Regeln. Folgende zwei Funktionen sind notwendig:
302 \footnotesize\begin{verbatim}
308 rls' -> bool -> thm' -> cterm' -> (string * string list) Library.option
310 Im Rewriting stehen die Argumente, die mitgeschickt werden m\"ussen, um die verschiedenen Rechnungen zu l\"osen.
311 Da es jedoch so viele Argumente (7) sind werden die Werte in Variablen abgespeichert.
312 \footnotesize\begin{verbatim}
319 bool -> 'a -> thm' -> cterm' -> (cterm' * cterm'list) Library.option
321 Die Funktion {\tt rewrite\_inst} wird ben\"otigt, um Gleichungen und Aufgaben, bei welchen differenziert werden muss zu l\"osen. Dabei wird die ungebundene Variable (bdv) instanziiert, d.h. es wird die Variable angegeben, nach der man differenzieren will, bzw. f\"ur die ein Wert/Ausdruck bei einer Gleichung herauskommen soll.
322 \paragraph{Versuchen Sie es!} Um zu sehen wie der Computer vorgeht, um folgendes Beispiel, dessen Ergebnis logischer Weise 0 ist, zu l\"osen werden hier die einzelnen Schritte durch differenzieren von a + a * (2 + b) gezeigt.
323 Zuerst werden die einzelnen Werte als Variablen gespeichert:
324 \footnotesize\begin{verbatim}
325 > val thy' = "Differentiate.thy";
326 val thy' = "Differentiate.thy" : string
327 > val ct = "d_d x (x ^^^ 2 + 3 * x + 4)";
328 val ct = "d_d x (x ^^^ 2 + 3 * x + 4)" : string
329 > val thm = ("diff_sum","");
330 val thm = ("diff_sum", "") : string * string
332 Schliesslich wird die erste Ableitung angezeigt.
333 \footnotesize\begin{verbatim}
334 > val Some (ct,_) = rewrite_inst thy' "tless_true" "eval_rls" true
335 [("bdv","x::real")] thm ct;
336 val ct = "d_d x (x ^^^ 2) + d_d x (3 * x) + d_d x 4" : cterm'
338 Will man auch die zweite Ableitung sehen, geht man so vor:
339 \footnotesize\begin{verbatim}
340 > val thm = ("diff_prod_const","");
341 val thm = ("diff_prod_const", "") : string * string
342 > val Some (ct,_) = rewrite_inst thy' "tless_true" "eval_rls" true
343 [("bdv","x::real")] thm ct;
344 val ct = "d_d x (x ^^^ 2) + 3 * d_d x x + d_d x 4" : cterm'
346 Wenn Sie sich noch weitere Beispiele ansehen wollen, dann besuchen sie bitte die folgende Site: {\tt [isac-src]/tests/\dots}.
348 \section{Was kann Rewriting?}
349 Es gibt verschiedene Varianten von Rewriting, die alle eine bestimmte Bedeutung haben.
350 {\tt rewrite\_ set} verwandelt Terme, die normalerweise nur mit einem Theorem vereinfacht dargestellt werden, in ein ganzes Rule Set.
351 Hierbei werden auch folgende Argumente verwendet:\\
353 \def\arraystretch{1.5}
354 \begin{tabular}{lp{11.0cm}}
355 {\tt theory} & Die Theory von Isabelle, die die n\"otigen Informationen f\"ur das Parsing {\tt term} enth\"alt. \\
356 {\tt rew\_ord}& die Rewriting Ordnung f\"ur das geordnete Rewriting. F\"ur {\em no} ben\"otigt das geordnete Rewriting {\tt tless\_true}, eine Ordnung, die f\"ur alle nachgiebigen Argumente true ist \\
357 {\tt rls} & Das rule set; zur Auswertung von bestimmten Bedingungen in {\tt thm} falls {\tt thm} eine conditional rule ist \\
358 {\tt bool} & ein Bitschalter, der die Berechnungen der m\"oglichen condition in {\tt thm} ausl\"ost: wenn sie {\tt falsch} ist, dann wird die condition bewertet und auf Grund des Resultats wendet man {\tt thm} an, oder nicht (conditional rewriting), wenn {\tt true} dann wird die condition nicht ausgewertet, aber man gibt sie in ein Menge von Hypothesen \\
359 {\tt thm} & das theorem versucht den {\tt term} zu \"uberschreiben \\
360 {\tt term} & {\tt thm} wendet Rewriting m\"oglicherweise auf den Term an \\
363 \footnotesize\begin{verbatim}
366 : theory -> rls -> bool -> rls -> term -> (term * term list) option
368 {\tt rewrite\_ set\_ inst} ist eine Kombination der oben genannten M\"oglichkeiten.
369 \footnotesize\begin{verbatim}
375 -> (cterm' * cterm') list
376 -> rls -> term -> (term * term list) option
378 Wenn man sehen m\"ochte wie Rewriting bei den einzelnen theorems funktioniert kann man dies mit {\tt trace\_ rewrite} versuchen.
379 \footnotesize\begin{verbatim}
381 val it = fn : bool ref -> bool
382 > toggle trace_rewrite;
384 > toggle trace_rewrite;
385 val it = false : bool
390 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.
391 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.
392 Ein Beispiel f\"ur einen rule set ist folgendes:
393 \footnotesize\begin{verbatim}
397 \footnotesize\begin{verbatim}
399 val it = "?s = ?t ==> ?t = ?s" : Thm.thm
403 {id = "rearrange_assoc",
404 scr = Script (Free ("empty_script", "RealDef.real")),
414 rew_ord = ("dummy_ord", fn),
424 rew_ord = ("dummy_ord", fn),
427 [Thm ("sym_radd_assoc", "?m1 + (?n1 + ?k1) = ?m1 + ?n1 + ?k1" [.]),
430 "?m1 * (?n1 * ?k1) = ?m1 * ?n1 * ?k1" [.])],
431 rew_ord = ("e_rew_ord", fn),
436 \section{Berechnung von Konstanten}
437 Sobald Konstanten in dem Bereich des Subterms sind, k\"onnen sie von einer Funktion berechnet werden:
438 \footnotesize\begin{verbatim}
446 Term.term -> Theory.theory -> (string * Term.term) Library.option) ->
447 cterm' -> (string * thm') Library.option
456 Term.term -> Theory.theory -> (string * Term.term) Library.option) ->
457 Term.term -> (Term.term * (string * Thm.thm)) Library.option
459 Man bekommt das Ergebnis und das theorem bezieht sich darauf. Daher sind die folgenden mathematischen Rechnungen m\"oglich:
460 \footnotesize\begin{verbatim}
463 [("Vars", ("Tools.Vars", fn)), ("matches", ("Tools.matches", fn)),
464 ("lhs", ("Tools.lhs", fn)), ("plus", ("op +", fn)),
465 ("times", ("op *", fn)), ("divide_", ("HOL.divide", fn)),
466 ("power_", ("Atools.pow", fn)), ("is_const", ("Atools.is'_const", fn)),
467 ("le", ("op <", fn)), ("leq", ("op <=", fn)),
468 ("ident", ("Atools.ident", fn)), ("sqrt", ("Root.sqrt", fn)),
469 ("Test.is_root_free", ("is'_root'_free", fn)),
470 ("Test.contains_root", ("contains'_root", fn))]
478 Term.term -> Theory.theory -> (string * Term.term) Library.option))) list
484 \chapter{Termordnung}
485 Die Anordnungen der Begriffe sind unverzichtbar f\"ur den Gebrauch des Umschreibens von normalen Funktionen und von normalen Formeln, die n\"otig sind um passende Modelle f\"ur Probleme zu finden.
487 \section{Beispiel f\"ur Termordnungen}
488 Es ist nicht unbedeutend, eine Verbindung zu Termen herzustellen, die wirklich eine Ordnung besitzen. Diese Ordnungen sind selbstaufrufende Bahnordnungen:
490 {\footnotesize\begin{verbatim}
492 val it = fn : bool -> Theory.theory -> subst -> Term.term * Term.term -> b ool
494 val it = fn : subst -> Term.term * Term.term -> bool
497 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.
499 {\section{Geordnetes Rewriting}}
500 Beim Rewriting entstehen Probleme, die vom ''law of commutativity`` (= Kommutativgesetz) durch '+' und '*' verursacht werden. Diese Probleme k\"onnen nur durch geordnetes Rewriting gel\"ost werden, da hier ein term nur umgeschrieben wird, wenn ein kleinerer dadurch entsteht.
503 \chapter{Problem hierachy}
504 \section{''Matching``}
505 Matching ist eine Technik von Rewriting, die von \isac{} verwendet wird, um ein Problem und den passenden problem type daf\"ur zu finden. Die folgende Funktion \"uberpr\"uft, ob Matching m\"oglich ist:
506 {\footnotesize\begin{verbatim}
508 val it = fn : Theory.theory -> Term.term -> Term.term -> bool
510 Die folgende Gleichung wird in Operatoren und freie Variablen zerlegt.
511 {\footnotesize\begin{verbatim}
512 > val t = (term_of o the o (parse thy)) "3 * x^^^2 = 1";
514 Const ("op =", "[RealDef.real, RealDef.real] => bool") $
515 (Const ("op *", "[RealDef.real, RealDef.real] => RealDef.real") $
516 Free ("3", "RealDef.real") $
519 "[RealDef.real, RealDef.real] => RealDef.real") $
520 Free ("x", "RealDef.real") $ Free ("2", " RealDef.real"))) $
521 Free ("1", "RealDef.real") : Term.term
523 Nun wird ein Modell erstellt, das sich nicht auf bestimmte Zahlen bezieht, sondern nur eine generelle Zerlegung durchf\"uhrt.
524 {\footnotesize\begin{verbatim}
525 > val p = (term_of o the o (parse thy)) "a * b^^^2 = c";
527 Const ("op =", "[RealDef.real, RealDef.real] => bool") $
528 (Const ("op *", "[RealDef.real, RealDef.real] => RealDef.real") $
529 Free ("a", "RealDef.real") $
532 "[RealDef.real, RealDef.real] => RealDef.real") $
533 Free ("b", "RealDef.real") $ Free ("2", "RealDef.real"))) $
534 Free ("c", "RealDef.real") : Term.term
536 Dieses Modell enth\"alt sogenannte \textit{scheme variables}.
537 {\footnotesize\begin{verbatim}
541 "*** . Const (op *)""*** . . Free (a, )"
542 "*** . . Const (Atools.pow)"
543 "*** . . . Free (b, )"
544 "*** . . . Free (2, )"
547 val it = "\n" : string
549 Das Modell wird durch den Befehl \textit{free2var} erstellt.
550 {\footnotesize\begin{verbatim}
552 val it = fn : Term.term -> Term.term
553 > val pat = free2var p;
555 Const ("op =", "[RealDef.real, RealDef.real] => bool") $
556 (Const ("op *", "[RealDef.real, RealDef.real] => RealDef.real") $
557 Var (("a", 0), "RealDef.real") $
560 "[RealDef.real, RealDef.real] => RealDef.real") $
561 Var (("b", 0), "RealDef.real") $
562 Free ("2", "RealDef.real"))) $ Var (("c", 0), "RealDef.real")
564 > Sign.string_of_term (sign_of thy) pat;
565 val it = "?a * ?b ^^^ 2 = ?c" : string
567 Durch \textit{atomt pat} wird der term aufgespalten und in eine Form gebracht, die f\"ur die weiteren Schritte ben\"otigt wird.
568 {\footnotesize\begin{verbatim}
573 "*** . . Var ((a, 0), )"
574 "*** . . Const (Atools.pow)"
575 "*** . . . Var ((b, 0), )"
576 "*** . . . Free (2, )"
577 "*** . Var ((c, 0), )"
579 val it = "\n" : string
581 Jetzt kann das Matching an den beiden vorigen Terme angewendet werden.
582 {\footnotesize\begin{verbatim}
585 > val t2 = (term_of o the o (parse thy)) "x^^^2 = 1";
587 Const ("op =", "[RealDef.real, RealDef.real] => bool") $
590 "[RealDef.real, RealDef.real] => RealDef.real") $
591 Free ("x", "RealDef.real") $ Free ("2", "RealDef.real")) $
592 Free ("1", "RealDef.real") : Term.term
593 > matches thy t2 pat;
594 val it = false : bool
595 > val pat2 = (term_of o the o (parse thy)) "?u^^^2 = ?v";
597 Const ("op =", "[RealDef.real, RealDef.real] => bool") $
600 "[RealDef.real, RealDef.real] => RealDef.real") $
601 Var (("u", 0), "RealDef.real") $ Free ("2", "RealDef.real")) $
602 Var (("v", 0), "RealDef.real") : Term.term
603 > matches thy t2 pat2;
607 \section{Zugriff auf die hierachy}
608 Man verwendet folgenden Befehl, um sich Zugang zur hierachy von problem type zu verschaffen.
609 {\footnotesize\begin{verbatim}
611 val it = fn : unit -> unit
615 ["simplification", "polynomial"],
616 ["simplification", "rational"],
617 ["vereinfachen", "polynom", "plus_minus"],
618 ["vereinfachen", "polynom", "klammer"],
619 ["vereinfachen", "polynom", "binom_klammer"],
620 ["probe", "polynom"],
622 ["equation", "univariate", "linear"],
623 ["equation", "univariate", "root", "sq", "rat"],
624 ["equation", "univariate", "root", "normalize"],
625 ["equation", "univariate", "rational"],
626 ["equation", "univariate", "polynomial", "degree_0"],
627 ["equation", "univariate", "polynomial", "degree_1"],
628 ["equation", "univariate", "polynomial", "degree_2", "sq_only"],
629 ["equation", "univariate", "polynomial", "
630 degree_2", "bdv_only"],
631 ["equation", "univariate", "polynomial", "degree_2", "pqFormula"],
632 ["equation", "univariate", "polynomial", "degree_2", "abcFormula"],
633 ["equation", "univariate", "polynomial", "degree_3"],
634 ["equation", "univariate", "polynomial", "degree_4"],
635 ["equation", "univariate", "polynomial", "normalize"],
636 ["equation", "univariate", "expanded", "degree_2"],
637 ["equation", "makeFunctionTo"],
638 ["function", "derivative_of", "named"],
639 ["function", "maximum_of", "on_interval"],
640 ["function", "make", "by_explicit"],
641 ["function", "make", "by_new_variable"],
642 ["function", "integrate", "named"],
643 ["tool", "find_values"],
644 ["system", "linear", "2x2", "triangular"],
645 ["system", "linear", "2x2", "normalize"],
646 ["system", "linear", "3x3"],
647 ["system", "linear", "4x4", "triangular"],
648 ["system", "linear", "4x4", "normalize"],
651 ["Biegelinien", "MomentGegebene"],
652 ["Biegelinien", "einfache"],
653 ["Biegelinien", "QuerkraftUndMomentBestimmte"],
654 ["Biegelinien", "vonBelastungZu"],
655 ["Biegelinien", "setzeRandbedingungen"],
656 ["Berechnung", "numerischSymbolische"],
657 ["test", "equation", "univariate", "linear"],
658 ["test", "equation", "univariate", "plain_square"],
659 ["test", "equation", "univariate", "polynomial", "degree_two", "pq_formula"],
660 ["test", "equation", "univariate", "polynomial", "degree_two", "abc_formula"],
661 ["test", "equation", "univariate", "squareroot"],
662 ["test", "equation", "univariate", "normalize"],
663 ["test", "equation", "univariate", "sqroot-test"]
668 \section{Die passende ''formalization`` f\"ur den problem type}
669 Eine andere Art des Matching ist es die richtige ''formalization`` zum jeweiligen problem type zu finden. Wenn eine solche vorhanden ist, kann \isac{} selbstst\"andig die Probleme l\"osen.
671 \section{''problem-refinement``}
672 Will man die problem hierachy (= ) aufstellen, so ist darauf zu achten, dass man die verschiedenen Branches so konstruiert, dass das problem-refinement automatisch durchgef\"uhrt werden kann.
673 {\footnotesize\begin{verbatim}
675 val it = fn : fmz_ -> pblID -> SpecifyTools.match list
676 > val fmz = ["equality (sqrt(9 + 4 * x)=sqrt x
678 # "soleFor x","errorBound (eps=0)",
681 ["equality (sqrt(9 + 4 * x)=sqrt x + sqrt (5 + x))", "soleFor x",
682 "errorBound (eps=0)", ...] : string list
683 > refine fmz ["univariate","equation"];
684 *** pass ["equation","univariate"]
685 *** comp_dts: ??.empty $ soleFor x
686 Exception- ERROR raised
688 Wenn die ersten zwei Regeln nicht angewendet werden k\"onnen, kommt die dritte zum Einsatz:
689 {\footnotesize\begin{verbatim}
690 > val fmz = ["equality (x + 1 = 2)",
691 # "solveFor x","errorBound (eps=0)",
693 val fmz = ["equality (x + 1 = 2)", "solveFor x", "errorBound (eps=0)", ...]
695 > refine fmz ["univariate","equation"];
696 *** pass ["equation","univariate"]
697 *** pass ["equation","univariate","linear"]
698 *** pass ["equation","univariate","root"]
699 *** pass ["equation","univariate","rational"]
700 *** pass ["equation","univariate","polynomial" ]
701 *** pass ["equation","univariate","polynomial","degree_0"]
702 *** pass ["equation","univariate","polynomial","degree_1"]
703 *** pass ["equation","univariate","polynomial","degree_2"]
704 *** pass ["equation","univariate","polynomial","degree_3"]
705 *** pass ["equation","univariate","polynomial","degree_4"]
706 *** pass ["equation","univariate","polynomial","normalize"]
709 (["univariate", "equation"],
710 {Find = [Correct "solutions L"], With = [...], ...}),
711 NoMatch (["linear", "univariate", ...], {Find = [...], ...}),
712 NoMatch (["root", ...], ...), ...] : SpecifyTools.match list
714 Der problem type wandelt $x + 1 = 2$ in die normale Form $-1 + x = 0$ um. Diese Suche nach der jeweiligen problem hierachy kann mit Hilfe eines ''proof state`` durchgef\"uhrt werden (siehe n\"achstes Kapitel).
717 \chapter{''Methods``}
718 Methods werden dazu verwendet, Probleme von type zu l\"osen. Sie sind in einer anderen Programmiersprache beschrieben. Die Sprache sieht einfach aus, betreibt aber im Hintergrund einen enormen Pr\"ufaufwand. So muss sich der Programmierer nicht mit technischen Details befassen, gleichzeitig k\"onnen aber auch keine falschen Anweisungen eingegeben werden.
719 \section{Der ''Syntax`` des script}
720 Syntax beschreibt den Zusammenhang der einzelnen Zeichen und Zeichenfolgen mit den Theorien.
721 Er kann so definiert werden:
723 123\=123\=expr ::=\=$|\;\;$\=\kill
724 \>script ::= {\tt Script} id arg$\,^*$ = body\\
725 \>\>arg ::= id $\;|\;\;($ ( id :: type ) $)$\\
727 \>\>expr ::= \>\>{\tt let} id = expr $($ ; id = expr$)^*$ {\tt in} expr\\
728 \>\>\>$|\;$\>{\tt if} prop {\tt then} expr {\tt else} expr\\
729 \>\>\>$|\;$\>listexpr\\
731 \>\>\>$|\;$\>seqex id\\
732 \>\>seqex ::= \>\>{\tt While} prop {\tt Do} seqex\\
733 \>\>\>$|\;$\>{\tt Repeat} seqex\\
734 \>\>\>$|\;$\>{\tt Try} seqex\\
735 \>\>\>$|\;$\>seqex {\tt Or} seqex\\
736 \>\>\>$|\;$\>seqex {\tt @@} seqex\\
737 \>\>\>$|\;$\>tac $($ id $|$ listexpr $)^*$\\
742 \section{\"Uberpr\"ufung der Auswertung}
743 Das Kontrollsystem arbeitet mit den folgenden Script-Ausdr\"ucken, die {\it tacticals} genannt werden:
745 \item{{\tt while} prop {\tt Do} expr id}
746 \item{{\tt if} prop {\tt then} expr {\tt else} expr}
748 W\"ahrend die genannten Befehle das Kontrollsystem durch Auswertung der Formeln ausl\"osen, h\"angen die anderen von der Anwendbarkeit der Formel in den entsprechenden Unterbegriffen ab:
750 \item{{\tt Repeat} expr id}
751 \item{{\tt Try} expr id}
752 \item{expr {\tt Or} expr id}
753 \item{expr {\tt @@} expr id}
759 \chapter{Befehle von \isac{}}
760 In diesem Kapitel werden alle schon zur Verf\"ugung stehenden Schritte aufgelistet. Diese Liste kann sich auf Grund von weiteren Entwicklungen von \isac{} noch \"andern.\
761 \newline\linebreak \textbf{Init\_Proof\_Hid (dialogmode, formalization, specifictaion)} gibt die eingegebenen Befehle an die mathematic engine weiter, wobei die beiden letzten Begriffe die Beispiele automatisch speichern. Es ist nicht vorgesehen, dass der Sch\"uler tactic verwendet.\
762 \newline\linebreak \textbf{Init\_Proof} bildet mit einem ''proof tree`` ein leeres Modell.\
763 \newline\linebreak \textbf{Model\_Problem problem} bestimmt ein problemtype, das wom\"oglich in der ''hierachy`` gefunden wurde, und verwendet es f\"ur das Umformen.\
764 \newline\linebreak \textbf{Add\_Given, Add\_Find, Add\_Relation formula} f\"ugt eine Formel in ein bestimmtes Feld eines Modells ein. Dies ist notwendig, solange noch kein Objekt f\"ur den Benutzer vorhanden ist, in dem man die Formel eingeben kann, und nicht die gew\"unschte tactic und Formel von einer Liste w\"ahlen will.\
765 \newline\linebreak \textbf{Specify\_Theorie theory, Specify\_Problem proble, Specify\_Method method} gibt das entsprechende Element des Basiswissens an.\
766 \newline\linebreak \textbf{Refine\_Problem problem} sucht nach einem Problem in der hierachy, das auf das vorhandene zutrifft.\
767 \newline\linebreak \textbf{Apply\_Method method} beendet das Modell und die Beschreibung. Danach wird die L\"osungmeldung ge\"offnet.\
768 \newline\linebreak \textbf{Free\_Solve} beginnt eine L\"osungsmeldung ohne die Hilfe einer method.\
769 \newline\linebreak \textbf{Rewrite theorem} bef\"ordert ein theorem in die aktuelle Formel und wandelt es demenetsprechend um. Wenn dies nicht m\"oglich ist, kommt eine Meldung mit ''error``.\
770 \newline\linebreak \textbf{Rewrite\_Asm theorem} hat die gleiche Funktion wie Rewrite, speichert jedoch eine endg\"ultige Vorraussetzung des theorems, anstatt diese zu sch\"atzen.\
771 \newline\linebreak \textbf{Rewrite\_Set ruleset} hat \"ahnliche Funktionen wie Rewrite, gilt aber f\"ur einen ganzen Satz von theorems, dem rule set.\
772 \newline\linebreak \textbf{Rewrite\_Inst (substitution, theorem), Rewrite\_Set\_Inst (substitution, rule set)} ist vergleichbar mit besonderen tactics, ersetzt aber Konstanten im theorem, bevor es zu einer Anwendung kommt.\
773 \newline\linebreak \textbf{Calculate operation} berechnet das Ergebnis der Eingabe mit der aktuellen Formel (plus, minus, times, cancel, pow, sqrt).\
774 \newline\linebreak \textbf{Substitute substitution} f\"ugt der momentanen Formel {\tt substitution} hinzu und wandelt es um.\
775 \newline\linebreak \textbf{Take formula} startet eine neue Reihe von Rechnungen in den Formeln, wo sich schon eine andere Rechnung befindet.\
776 \newline\linebreak \textbf{Subproblem (theory, problem)} beginnt ein subproblem innerhalb einer Rechnung.\
777 \newline\linebreak \textbf{Function formula} ruft eine Funktion auf, in der der Name in der Formel enthalten ist. ???????\
778 \newline\linebreak \textbf{Split\_And, Conclude\_And, Split\_Or, Conclude\_Or, Begin\_Trans, End\_Trans, Begin\_Sequ, End\_Sequ, Split\_Intersect, End\_Intersect} betreffen den Bau einzelner branches des proof trees. Normalerweise werden sie vom dialog guide verdr\"angt.\
779 \newline\linebreak \textbf{Check\_elementwise assumption} wird in Bezug auf die aktuelle Formel verwendet, die Elemente in einer Liste enth\"alt.\
780 \newline\linebreak \textbf{Or\_to\_List} wandelt eine Verbindung von Gleichungen in eine Liste von Gleichungen um.\
781 \newline\linebreak \textbf{Check\_postcond} \"uberpr\"uft die momentane Formel im Bezug auf die Nachbedinung beim Beenden des subproblem.\
782 \newline\linebreak \textbf{End\_Proof} beendet eine \"Uberpr\"ufung und gibt erst dann ein Ergebnis aus, wenn Check\_postcond erfolgreich abgeschlossen wurde.
784 \section{Die Funktionsweise der mathematic engine}
785 Ein proof (= Beweis) wird in der mathematic engine me von der tactic {\tt Init\_Proof} gestartet und wird wechselwirkend mit anderen tactics vorangebracht. Auf den input (= das, was eingegeben wurde) einzelner tactics folgt eine Formel, die von der me ausgegeben wird, und die darauf folgende tactic gilt. Der proof ist beendet, sobald die me {\tt End\_Proof} als n\"achste tactic vorschl\"agt.
786 \newline Im Anschluss werden Sie einen Rechenbeweis sehen, der von der L\"osung einer Gleichung (= equation) handelt, bei der diese automatisch differenziert wird.
787 {\footnotesize\begin{verbatim}
788 ??????????????????????????????????????????????????????????????????????????????????
790 ML> val fmz = ["equality ((x+#1)*(x+#2)=x^^^#2+#8)","solveFor x",
791 "errorBound (eps=#0)","solutions L"];
793 ["equality ((x+#1)*(x+#2)=x^^^#2+#8)","solveFor x","errorBound (eps=#0)",
794 "solutions L"] : string list
796 ML> val spec as (dom, pbt, met) = ("SqRoot.thy",["univariate","equation"],
797 ("SqRoot.thy","no_met"));
798 val dom = "SqRoot.thy" : string
799 val pbt = ["univariate","equation"] : string list
800 val met = ("SqRoot.thy","no_met") : string * string
803 \section{Der Beginn einer Rechnung}
805 Der proof state wird von einem proof tree und einer position ausgegeben. Beide sind zu Beginn leer. Die tactic {\tt Init\_Proof} ist, wie alle anderen tactics auch, an einen string gekoppelt. Um einen neuen proof beginnen zu k\"onnen, werden folgende Schritte durchgef\"uhrt:
806 \footnotesize\begin{verbatim}
807 ????????????????????????????????????????????????????????????????????????????????????????????
808 ML> val (mID,m) = ("Init_Proof",Init_Proof (fmz, (dom,pbt,met)));
809 val mID = "Init_Proof" : string
812 (["equality ((x+#1)*(x+#2)=x^^^#2+#8)","solveFor x","errorBound (eps=#0)",
813 "solutions L"],("SqRoot.thy",[#,#],(#,#))) : mstep
815 ML> val (p,_,f,nxt,_,pt) = me (mID,m) e_pos' c EmptyPtree;
816 val p = ([],Pbl) : pos'
817 val f = Form' (PpcKF (0,EdUndef,0,Nundef,(#,#))) : mout
818 val nxt = ("Refine_Tacitly",Refine_Tacitly ["univariate","equation"])
823 {branch=#,cell=#,env=#,loc=#,meth=#,model=#,origin=#,ostate=#,probl=#,
824 result=#,spec=#},[]) : ptree
826 Die mathematics engine gibt etwas mit dem type {\tt mout} aus, was in unserem Fall ein Problem darstellt. Sobald mehr angezeigt wird, m\"usste dieses jedoch gel\"ost sein.
827 \footnotesize\begin{verbatim}
828 ?????????????????????????????????????????????????????????????????????????????????????????????
829 ML> Compiler.Control.Print.printDepth:=8; (*4 default*)
838 {Find=[Incompl "solutions []"],
839 Given=[Incompl "equality",Incompl "solveFor"],Relate=[],
840 Where=[False "matches (?a = ?b) e_"],With=[]}))) : mout
842 {\footnotesize\begin{verbatim}
843 ?????????????????????????????????????????????????????????????????????????????????????????????
845 val it = ("Refine_Tacitly",Refine_Tacitly ["univariate","equation"])
848 ML> val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
849 val nxt = ("Model_Problem",Model_Problem ["normalize","univariate","equation"])
852 ML> val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
855 \section{The phase of modeling}
856 Dieses Kapitel besch\"aftigt sich mit dem input der Einzelheiten bei einem Problem. Die me kann dabei helfen, wenn man die formalization durch {\tt Init\_Proof} darauf hinweist. Normalerweise weiss die mathematics engine die n\"achste gute tactic.
857 {\footnotesize\begin{verbatim}
858 ?????????????????????????????????????????????????????????????????????????????????????????????
861 ("Add_Given",Add_Given "equality ((x + #1) * (x + #2) = x ^^^ #2 + #8)")
864 ML> val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
865 val nxt = ("Add_Given",Add_Given "solveFor x") : string * mstep
867 ML> val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
868 val nxt = ("Add_Find",Add_Find "solutions L") : string * mstep
870 ML> val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
871 val f = Form' (PpcKF (0,EdUndef,0,Nundef,(#,#))) : mout
873 {\footnotesize\begin{verbatim}
874 ?????????????????????????????????????????????????????????????????????????????????????????????
875 ML> Compiler.Control.Print.printDepth:=8;
882 {Find=[Correct "solutions L"],
883 Given=[Correct "equality ((x + #1) * (x + #2) = x ^^^ #2 + #8)",
884 Correct "solveFor x"],Relate=[],Where=[],With=[]}))) : mout
888 \section{The phase of specification}
889 Diese phase liefert eindeutige Bestimmungen einer domain, den problem type und die method damit man sie verwenden kann. F\"ur gew\"ohnlich wird die Suche nach dem richtigen problem type unterst\"utzt. Dazu sind zwei tactics verwendbar: {\tt Specify\_Problem} entwickelt ein Feedback, wie ein problem type bei dem jetzigen problem zusammenpasst und {\tt Refine\_Problem} stellt Hilfe durch das System bereit, falls der Benutzer die \"Ubersicht verliert.
890 {\footnotesize\begin{verbatim}
891 ??????????????????????????????????????????????????????????????????????????????????????????
893 val it = ("Specify_Domain",Specify_Domain "SqRoot.thy") : string * mstep
895 ML> val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
897 ("Specify_Problem",Specify_Problem ["normalize","univariate","equation"])
902 {branch=#,cell=#,env=#,loc=#,meth=#,model=#,origin=#,ostate=#,probl=#,
903 result=#,spec=#},[]) : ptree
905 Die me erkennt den richtigen Problem type und arbeitet so weiter:
906 {\footnotesize\begin{verbatim}
907 ?????????????????????????????????????????????????????????????????????????????????????????
908 ML> val nxt = ("Specify_Problem",
909 Specify_Problem ["polynomial","univariate","equation"]);
910 ML> val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
911 val f = Form' (PpcKF (0,EdUndef,0,Nundef,(#,#))) : mout
913 ("Refine_Problem",Refine_Problem ["normalize","univariate","equation"])
916 ML> val nxt = ("Specify_Problem",
917 Specify_Problem ["linear","univariate","equation"]);
918 ML> val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
923 (Problem ["linear","univariate","equation"],
924 {Find=[Correct "solutions L"],
925 Given=[Correct "equality ((x + #1) * (x + #2) = x ^^^ #2 + #8)",
926 Correct "solveFor x"],Relate=[],
928 "matches (?a + ?b * x = #0) ((x + #1) * (x + #2) = x ^^^ #2 + #8)"],
931 Wir nehmen wieder an, dass der dialog guide die n\"achsten tactics, veranlasst von der mathematic engine, versteckt und der Sch\"uler Hilfe ben\"otigt. Dann muss {\tt Refine\_Problem} angewandt werden. Dieser Befehl findet immer den richtigen Weg, wenn man es auf den problem type bezieht [''univariate``, ''equation``].
932 {\footnotesize\begin{verbatim}
933 ????????????????????????????????????????????????????????????????????????????????????????????
934 ML> val nxt = ("Refine_Problem",
935 Refine_Problem ["linear","univariate","equation
936 ML> val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
937 val f = Problems (RefinedKF [NoMatch #]) : mout
939 ML> Compiler.Control.Print.printDepth:=9;f;Compiler.Control.Print.printDepth:=4;
944 (["linear","univariate","equation"],
945 {Find=[Correct "solutions L"],
946 Given=[Correct "equality ((x + #1) * (x + #2) = x ^^^ #2 + #8)",
947 Correct "solveFor x"],Relate=[],
949 "matches (?a + ?b * x = #0) ((x + #1) * (x + #2) = x ^^^ #2 + #8)"],
952 ML> val nxt = ("Refine_Problem",Refine_Problem ["univariate","equation"]);
953 ML> val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
956 (RefinedKF [Matches #,NoMatch #,NoMatch #,NoMatch #,NoMatch #,Matches #])
960 ML> Compiler.Control.Print.printDepth:=9;f;Compiler.Control.Print.printDepth:=4;
965 (["univariate","equation"],
966 {Find=[Correct "solutions L"],
967 Given=[Correct "equality ((x + #1) * (x + #2) = x ^^^ #2 + #8)",
968 Correct "solveFor x"],Relate=[],
972 (["linear","univariate","equation"],
973 {Find=[Correct "solutions L"],
974 Given=[Correct "equality ((x + #1) * (x + #2) = x ^^^ #2 + #8)",
975 Correct "solveFor x"],Relate=[],
977 "matches (?a + ?b * x = #0) ((x + #1) * (x + #2) = x ^^^ #2 + #8)"],
983 (["normalize","univariate","equation"],
984 {Find=[Correct "solutions L"],
985 Given=[Correct "equality ((x + #1) * (x + #2) = x ^^^ #2 + #8)",
986 Correct "solveFor x"],Relate=[],Where=[],With=[]})]) : mout
988 Die tactic {\tt Refine\_Problem} wandelt alle matches wieder in problem types um und sucht in der problem hierachy weiter.
991 \section{The phase of solving}
992 Diese phase beginnt mit dem Aufruf einer method, die eine normale form innerhalb einer tactic ausf\"uhrt: {\tt Rewrite rnorm\_equation\_add} und {\tt Rewrite\_Set SqRoot\_simplify}:
993 {\footnotesize\begin{verbatim}
995 val it = ("Apply_Method",Apply_Method ("SqRoot.thy","norm_univar_equation"))
998 ML> val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1000 Form' (FormKF (~1,EdUndef,1,Nundef,"(x + #1) * (x + #2) = x ^^^ #2 + #8"))
1003 ("rnorm_equation_add","~ ?b =!= #0 ==> (?a = ?b) = (?a + #-1 * ?b = #0)"))
1005 ML> val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1007 Form' (FormKF (~1,EdUndef,1,Nundef,
1008 "(x + #1) * (x + #2) + #-1 * (x ^^^ #2 + #8) = #0")) : mout
1009 val nxt = ("Rewrite_Set",Rewrite_Set "SqRoot_simplify") : string * mstep
1011 ML> val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1012 val f = Form' (FormKF (~1,EdUndef,1,Nundef,"#-6 + #3 * x = #0")) : mout
1013 val nxt = ("Subproblem",Subproblem ("SqRoot.thy",[#,#])) : string * mstep
1015 Die Formel $-6 + 3\cdot x = 0$ ist die Eingabe eine subproblems, das wiederum gebraucht wird, um die Gleichungsart zu erkennen und die entsprechende method auszuf\"uhren:
1016 {\footnotesize\begin{verbatim}
1018 val it = ("Subproblem",Subproblem ("SqRoot.thy",["univariate","equation"]))
1020 ML> val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1023 (~1,EdUndef,1,Nundef,"Subproblem (SqRoot.thy, [univariate, equation])"))
1025 val nxt = ("Refine_Tacitly",Refine_Tacitly ["univariate","equation"])
1027 ML> val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1028 val nxt = ("Model_Problem",Model_Problem ["linear","univariate","equation"])
1030 {\tt Refine [''univariate``, ''equation``]} sucht die passende Gleichungsart aus der problem hierachy heraus, welche man mit {\tt Model\_Problem [''linear``, ''univariate``, ''equation``]} \"uber das System ansehen kann.
1031 Nun folgt erneut die phase of modeling und die phase of specification.
1033 \section{The final phase: \"Uberpr\"ufung der ''post-condition``}
1034 Die gezeigten problems, die durch \isac{} gel\"ost wurden, sind so genannte 'example construction problems'. Das massivste Merkmal solcher problems ist die post-condition. Im Umgang mit dieser gibt es noch offene Fragen.
1035 Dadurch wird die post-condition im folgenden Beispiel als problem und subproblem erw\"ahnt.
1036 {\footnotesize\begin{verbatim}
1038 val it = ("Check_Postcond",Check_Postcond ["linear","univariate","equation"])
1040 ML> val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1041 val f = Form' (FormKF (~1,EdUndef,1,Nundef,"[x = #2]")) : mout
1043 ("Check_Postcond",Check_Postcond ["normalize","univariate","equation"])
1045 ML> val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1046 val f = Form' (FormKF (~1,EdUndef,0,Nundef,"[x = #2]")) : mout
1047 val nxt = ("End_Proof'",End_Proof') : string * mstep
1049 Die tactic {\tt End\_Proof'} bedeutet, dass der proof erflogreich beendet wurde.\\
1051 \paragraph{Versuchen Sie es!} Die tactics, die vom System vorgeschlagen werden, m\"ussen vom Benutzer nicht angewendet werden. Er kann selbstverst\"andlich auch andere tactics verwenden und das System wird melden, ob dieser Befehl zutreffend ist oder nicht.
1054 \part{Handbuch f\"ur Autoren}
1056 \chapter{Die Struktur des Grundlagenwissens}
1058 \section{''tactics`` und Daten}
1059 Zuerst betrachten wir die me von aussen. Wir sehen uns tactics und an und verbinden sie mit unserem Grundwissen (KB). Im Bezug auf das KB befassen wir uns mit den kleinsten Teilchen, die von den Autoren des KB sehr genau durchgef\"uhrt werden m\"ussen.
1060 Diese Teile sind in alphabetischer Anordnung in Tab.\ref{kb-items} auf Seite \pageref{kb-items} aufgelistet.
1063 \caption{Kleinste Teilchen des KB} \label{kb-items}
1066 \def\arraystretch{1.0}
1067 \begin{tabular}{lp{9.0cm}}
1068 Abk\"urzung & Beschreibung \\
1072 & gesammelte Liste von allen ausgewerteten Funktionen\\
1074 & ausgewertete Funktionen f\"ur Zahlen und f\"ur Eigenschaften, die in SML kodiert sind\\
1076 & rule set {\it rls} f\"ur einfache Ausdr\"ucke mit {\it eval\_fn}s\\
1078 & Formalisierung, d.h. eine sehr geringe Darstellung von einem Beispiel \\
1080 & eine method d.h. eine Datenstruktur, die alle Informationen zum L\"osen einer phase enth\"alt ({\it rew\_ord}, {\it scr}, etc.)\\
1082 & bezieht sich auf {\it met}\\
1084 & ein Operator, der der Schl\"ussel zu {\it eval\_fn} in einer {\it calc\_list} ist \\
1086 & Problem d.h. der Knotenpunkt in der problem hierachy\\
1088 & bezieht sich auf {\it pbl}\\
1090 & Anordnung beim Rewriting\\
1092 & rule set, d.h. eine Datenstruktur, die theorems {\it thm} und Operatoren {\it op} zur Vereinfachung (mit {\it rew\_ord}) enth\"alt \\
1094 & rule set f\"ur das 'reverse rewriting' (eine \isac-Technik, die schrittweise Rewriting entwickelt, z.B. f\"ur die zur\"uckgenommenen Teile)\\
1096 & script, das die Algorithmen durch Anwenden von tactics beschreibt und ein Teil von {\it met} ist \\
1098 & spezielles Regelwerk zum Berechnen von Normalformen, im Zusammenhang mit {\it thy}\\
1100 & Spezifikation, z.B, ein Tripel ({\it thyID, pblID, metID})\\
1102 & Ersatz, z.B. eine Liste von Variablen und ihren jeweiligen Werten\\
1104 & Term von Isabelle, z.B. eine Formel\\
1110 & im Bezug auf {\it thy} \\
1111 \end{tabular}\end{center}\end{table}}
1113 Die Verbindung zwischen tactics und Daten werden in Tab.\ref{tac-kb} auf Seite \pageref{tac-kb} dargestellt.
1117 \caption{Welche tactics verwenden die Teile des KB~?} \label{tac-kb}
1120 \begin{tabular}{|ll||cccc|ccc|cccc|} \hline
1121 tactic &Eingabe & & & &norm\_& &rew\_&rls &eval\_&eval\_&calc\_& \\
1122 & &thy &scr &Rrls&rls &thm &ord &Rrls&fn &rls &list &dsc\\
1125 &fmz & x & & & x & & & & & & & x \\
1126 &spec & & & & & & & & & & & \\
1128 \multicolumn{13}{|l|}{model phase}\\
1131 &term & x & & & x & & & & & & & x \\
1132 FormFK &model & x & & & x & & & & & & & x \\
1134 \multicolumn{13}{|l|}{specify phase}\\
1137 &thyID & x & & & x & & & & x & x & & x \\
1139 &pblID & x & & & x & & & & x & x & & x \\
1141 &pblID & x & & & x & & & & x & x & & x \\
1143 &metID & x & & & x & & & & x & x & & x \\
1145 &metID & x & x & & x & & & & x & x & & x \\
1147 \multicolumn{13}{|l|}{solve phase}\\
1150 &thm & x & x & & & x &met & & x &met & & \\
1152 &thm & x & x & & & x &rls & & x &rls & & \\
1154 &thm & x & x & & & x &Rrls & & x &Rrls & & \\
1156 &rls & x & x & & & & & x & x & x & & \\
1158 &op & x & x & & & & & & & & x & \\
1160 &subs & x & & & x & & & & & & & \\
1161 & & & & & & & & & & & & \\
1163 &spec & x & x & & x & & & & x & x & & x \\
1164 &fmz & & & & & & & & & & & \\
1166 \end{tabular}\end{center}\end{table}}
1169 \section{Die theories von \isac{}}
1170 Die theories von \isac{} basieren auf den theories f\"ur HOL und Real von Isabelle. Diese theories haben eine spezielle Form, die durch die Endung {\tt *.thy} gekennzeichnet sind; normalerweise werden diese theories zusammen mit SML verwendet. Dann haben sie den selben Dateinamen, aber die Endung {\tt *.ML}.
1171 Die theories von \isac{} representieren den Teil vom Basiswissen von \isac{}, die hierachy von den zwei theories ist nach diesen strukturiert. Die {\tt *.ML} Dateien beinhalten {\em alle} Daten von den anderen zwei Hauptlinien des Basiswissens, die problems und methods (ohne ihre jeweilige Struktur, die von den problem Browsern und den method Browsern gemacht wird, zu pr\"asentieren.
1172 Die Tab.\ref{theories} auf Seite \pageref{theories} listet die base theories auf, die geplant sind in der Version \isac{} 1 angewendet zu werden. Wir erwarten, dass die Liste erweitert wird in n\"aherer Zukunft, und wir werden uns auch den theorie Browser genauer ansehen.
1173 Die ersten drei theories auf der Liste geh\"oren {\em nicht} zum Grundwissen von \isac{}; sie besch\"aftigen sich mit der Skriptsprache f\"ur methods und ist hier nur zur Vollst\"andigkeit angef\"uhrt.
1176 \caption{theory von der ersten Version von \isac} \label{theories}
1179 \def\arraystretch{1.0}
1180 \begin{tabular}{lp{9.0cm}}
1181 theory & Beschreibung \\
1185 & ordnet die Bezeichnungen den Funktionen, die in {\tt Isabelle2002/src/HOL/List.thy} sind, zu und (intermediatly~?) definiert einige weitere Listen von Funktionen\\
1187 & {\tt eval\_fn} f\"ur die zus\"atzliche Listen von Funktionen\\
1189 & Funktion, die f\"ur die Auswertung von Skripten ben\"otigt wird\\
1191 & bezieht sich auf {\tt eval\_fn}s\\
1193 & Vorraussetzung f\"ur script: types, tactics, tacticals\\
1195 & eine Reihe von tactics und Funktionen f\"ur den internen Gebrauch\\
1200 & fortgeschrittener Austritt, um den type Fehlern zu entkommen\\
1202 & {\it Beschreibungen} f\"ur die Formeln von {\it Modellen} und {\it Problemen}\\
1204 & Neudefinierung von Operatoren; allgemeine Eigenschaften und Funktionen f\"ur Vorraussetzungen; theorems f\"ur {\tt eval\_rls}\\
1206 & Gleitkommerzahlendarstellung\\
1208 & grunds\"atzliche Vorstellung f\"ur Gleichungen und Gleichungssysteme\\
1212 & polynomiale Gleichungen und Gleichungssysteme \\
1214 & zus\"atzliche theorems f\"ur Rationale Zahlen\\
1216 & abbrechen, hinzuf\"ugen und vereinfachen von Rationalen Zahlen durch Verwenden von (einer allgemeineren Form von) Euclids Algorithmus; die entsprechenden umgekehrten Regels\"atze\\
1218 & Gleichung mit rationalen Zahlen\\
1220 & Radikanten; berechnen der Normalform; das betreffende umgekehrte Regelwerk\\
1222 & Gleichungen mit Wurzeln\\
1224 & Gleichungen mit rationalen Zahlen und Wurzeln (z.B. mit Termen, die beide Vorg\"ange enthalten)\\
1226 & Vektoren Analysis\\
1230 & Logarithmus und Exponentialfunktionen\\
1232 & nicht der Norm entsprechende Analysis\\
1236 & Anwendungen beim Differenzieren (Maximum-Minimum-Probleme)\\
1238 & (alte) Daten f\"ur Testfolgen\\
1240 & enth\"alt alle Theorien von\isac{}\\
1241 \end{tabular}\end{center}\end{table}}
1244 \section{Daten in {\tt *.thy} und {\tt *.ML}}
1245 Wie schon zuvor angesprochen, haben die Arbeiten die theories von *.thy und *.ML zusammen und haben deswegen den selben Dateiname. Wie diese Daten zwischen den zwei Dateien verteilt werden wird in der
1246 Tab.\ref{thy-ML} auf Seite \pageref{thy-ML} gezeigt. Die Ordnung von den Datenteilchen in den theories sollte an der Ordnung von der Liste festhalten.
1249 \caption{Daten in {\tt *.thy}- und {\tt *.ML}-files} \label{thy-ML}
1252 \def\arraystretch{1.0}
1253 \begin{tabular}{llp{7.7cm}}
1254 Datei & Daten & Beschreibung \\
1259 & Operatoren, Eigenschaften, Funktionen und Skriptnamen ('{\tt Skript} Name \dots{\tt Argumente}')
1262 & theorems: \isac{} verwendet theorems von Isabelle, wenn m\"oglich; zus\"atzliche theorems, die jenen von Isabelle entsprechen, bekommen ein {\it I} angeh\"angt
1267 abgegrenzt ist von der {\tt *.thy}-Datei, wird durch \isac{} zug\"anglich gemacht
1270 & die Auswertungsfunktion f\"ur die Operatoren und Eigenschaften, kodiert im meta-Level (SML); die Bezeichnugn von so einer Funktion ist eine Kombination von Schl\"usselw\"ortern {\tt eval\_} und einer Bezeichnung von der Funktion, die in in {\tt *.thy} erkl\"art ist
1273 & der automatisierte Vereinfacher f\"ur die tats\"achliche Theorie, z.B. die Bezeichnung von diesem Regelwerk ist eine Kombination aus den Theorienbezeichnungen und dem Schl\"usselwort {\tt *\_simplify}
1275 & {\tt norm\_rls :=}
1276 & der automatisierte Vereinfacher {\tt *\_simplify} wird so aufgehoben, dass er \"uber \isac{} zug\"anglich ist
1278 & {\tt rew\_ord' :=}
1279 & das Gleiche f\"ur die Anordnung des Rewriting, wenn es ausserhalb eines speziellen Regelwerks gebraucht wird
1282 & dasselbe wie f\"ur Regels\"atze (gew\"ohnliche Regels\"atze, umgekehrte Regels\"atze, und {\tt eval\_rls})
1284 & {\tt calc\_list :=}
1285 & dasselbe f\"ur {\tt eval\_fn}s, wenn es ausserhalb eines bestimmten Regelwerks gebraucht wird (wenn es ausserhalb eines bestimmten Regelwerks ben\"otigt wird) (z.B. f\"ur eine tactic {\tt Calculate} in einem Skript)
1288 & Problems, die in {\tt *.ML}-Dateien definiert sind, werden zug\"anglich f\"ur \isac{}
1291 & methods, die in {\tt *.ML}-Dateien definiert sind werden zug\"anglich f\"ur \isac{}
1293 \end{tabular}\end{center}\end{table}}
1295 \section{Formale Beschreibung der Hierarchie von Problemen}
1297 \section{Skripttaktiken}
1298 Tats\"achlich sind es die tactics, die die Berechnungen vorantreiben: im Hintergrund bauen sie den proof tree und sie \"ubernehmen die wichtigsten Aufgaben w\"ahrend der Auswertung bei der der ''script-interpreter`` zur Steuerung des Benutzers transferiert wird. Hier beschreiben wir nur den Syntax von tactics; die Semantik ist beschrieben etwas weiter unten im Kontext mit tactics, die die Benutzer/Innen dieses Programmes verwenden: Es gibt einen Schriftverkehr zwischen den user-tactics und den script tactics.
1302 \part{Authoring on the knowledge}
1305 \section{Add a theorem}
1306 \section{Define and add a problem}
1307 \section{Define and add a predicate}
1308 \section{Define and add a method}
1317 \bibliography{bib/isac,bib/from-theses}