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}$}
11 \def\sisac{{\footnotesize${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$}}
14 Experimente zur Computermathematik\\[1.0ex]
16 Handbuch f\"ur Autoren der\\
17 Mathematik-Wissensbasis\\[1.0ex]}
18 \author{Alexandra Hirn und Eva Rott\\
19 \tt isac-users@ist.tugraz.at\\[1.0ex]}
31 Dies ist die \"Ubersetzung der dersten Kapitel einer englischen Version \footnote{http://www.ist.tugraz.at/projects/isac/publ/mat-eng.pdf}, auf den Stand von \sisac{} 2008 gebracht. Die \"Ubersetzung und Anpassung erfolgte durch die Autorinnen im Rahmen einer Ferialpraxis am Institut f\"ur Softwaretechnologie der TU Graz.
33 Diese Version zeichnet sich dadurch aus, dass sie von ``Nicht-Computer-Freaks'' f\"ur ``Nicht-Computer-Freaks'' geschrieben wurde.
35 \section{``Authoring'' und ``Tutoring''}
36 \paragraph{TO DO} Mathematik lernen -- verschiedene Autoren -- Isabelle
37 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.
38 \section{Der Inhalt des Dokuments}
39 \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.
41 \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.
43 Das Dokument ist eigenst\"andig; Basiswissen \"uber SML (f\"ur eine Einf\"uhrung siehe \cite{Paulson:91}), Terme und Umschreibung wird vorrausgesetzt.
45 %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.
47 Hinweis: SML Code, Verzeichnis, Dateien sind {\tt in 'tt' geschrieben}; besonders in {\tt ML>} ist das Kerngebiet schnell.
49 \paragraph{Versuchen Sie es!} Ein weiteres Anliegen dieses Textes ist, dem Leser Tipps f\"ur Versuche mit den Anwendungen zu geben.
51 \section{Gleich am Computer ausprobieren!}\label{get-started}
52 \paragraph{TO DO screenshot} Bevor Sie mit Ihren Versuchen beginnen, m\"ochten wir Ihnen noch einige Hinweise geben:
55 \item Shell aufmachen und die Datei mat-eng-de.sml \"offnen.
56 \item $>$ : Hinter diesem Zeichen (``Prompt'') stehen jene, die Sie selbst eingeben bzw. mit Copy und Paste aus der Datei kopieren.
57 \item Die Eingabe wird mit ``;'' und ``Enter'' abgeschlossen.
58 \item Zeilen, die nicht mit Prompt beginnen, werden vom Computer ausgegeben.
62 \part{Experimentelle Ann\"aherung}
64 \chapter{Terme und Theorien}
65 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.
67 \section{Von der Formel zum Term}
68 Um ein Beispiel zu nennen: Die Formel $a+b\cdot 3$ l\"asst sich in lesbarer Form so eingeben:
69 {\footnotesize\begin{verbatim}
71 val it = "a + b * 3" : string
73 \noindent ``a + b * 3'' ist also ein string (eine Zeichenfolge). In dieser Form weiss der Computer nicht, dass z.B. eine Multiplikation {\em vor} einer Addition zu rechnen ist. Isabelle braucht dazu eine andere Darstellung f\"ur Formeln. In diese kann man mit der Funktion {\tt str2term} (string to term) umrechnen:
74 {\footnotesize\begin{verbatim}
75 > str2term "a + b * 3";
77 Const ("op +", "[RealDef.real, RealDef.real] => RealDef.real") $
78 Free ("a", "RealDef.real") $
79 (Const ("op *", "[RealDef.real, RealDef.real] => RealDef.real") $ ... $
82 \noindent Diese Form heisst {\tt term} und ist nicht f\"ur den Menschen zum lesen gedacht. Isabelle braucht sie aber intern zum Rechnen. Wir wollen sie mit Hilfe von {\tt val} (value) auf der Variable {\tt t} speichern:
83 {\footnotesize\begin{verbatim}
84 > val t = str2term "a + b * 3";
86 Const ("op +", "[RealDef.real, RealDef.real] => RealDef.real") $
87 Free ("a", "RealDef.real") $
88 (Const ("op *", "[RealDef.real, RealDef.real] => RealDef.real") $ ... $
91 Von dieser Variablen {\tt t} kann man den Wert jederzeit abrufen:
92 {\footnotesize\begin{verbatim}
95 Const ("op +", "[RealDef.real, RealDef.real] => RealDef.real") $
96 Free ("a", "RealDef.real") $
97 (Const ("op *", "[RealDef.real, RealDef.real] => RealDef.real") $ ... $
100 Der auf {\tt t} gespeicherte Term kann einer Funktion {\tt atomty} \"ubergeben werden, die diesen in einer dritten Form zeigt:
101 {\footnotesize\begin{verbatim}
105 *** Const (op +, [real, real] => real)
107 *** . Const (op *, [real, real] => real)
108 *** . . Free (b, real)
109 *** . . Free (3, real)
114 Diese Darstellung nennt man ``abstract syntax'' und macht unmittelbar klar, dass man a und b nicht addieren kann, weil ein Mal vorhanden ist.
115 \newline Es gibt noch eine vierte Art von Term, den cterm. Er wird weiter unten verwendet, weil er sich als string lesbar darstellt.
117 \section{``Theory'' und ``Parsing``}
118 Der Unterschied zwischen \isac{} und bisheriger Mathematiksoftware (GeoGebra, Mathematica, Maple, Derive etc.) ist, dass das mathematische Wissen nicht im Programmcode steht, sondern in sogenannten theories (Theorien).
119 Dort wird das Mathematikwissen in einer f\"ur nicht Programmierer lesbaren Form geschrieben. Das Wissen von \isac{} ist in folgenden Theorien entahlten:
120 {\footnotesize\begin{verbatim}
123 {ProtoPure, CPure, HOL, Set, Typedef, Fun, Product_Type, Lfp, Gfp,
124 Sum_Type, Relation, Record, Inductive, Transitive_Closure,
125 Wellfounded_Recursion, NatDef, Nat, NatArith, Divides, Power,
126 SetInterval, Finite_Set, Equiv, IntDef, Int, Datatype_Universe,
127 Datatype, Numeral, Bin, IntArith, Wellfounded_Relations, Recdef, IntDiv,
128 IntPower, NatBin, NatSimprocs, Relation_Power, PreList, List, Map,
129 Hilbert_Choice, Main, Lubs, PNat, PRat, PReal, RealDef, RealOrd,
130 RealInt, RealBin, RealArith0, RealArith, RComplete, RealAbs, RealPow,
131 Ring_and_Field, Complex_Numbers, Real, ListG, Tools, Script, Typefix,
132 Float, ComplexI, Descript, Atools, Simplify, Poly, Rational, PolyMinus,
133 Equation, LinEq, Root, RootEq, RatEq, RootRat, RootRatEq, PolyEq, Vect,
134 Calculus, Trig, LogExp, Diff, DiffApp, Integrate, EqSystem, Biegelinie,
135 AlgEin, Test, Isac} : Theory.theory
137 {\tt ProtoPure} und {\tt CPure} enthalten diese logischen Grundlagen, die in {\tt HOL} und den nachfolgenden Theorien erweitert werden. \isac{} als letzte Theorie beinhaltet das gesamte Wissen.
138 Dass das Mal vor dem Plus berechnet wird, ist so festgelegt:
139 {\footnotesize\begin{verbatim}
141 fixes plus :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "+" 65)
144 fixes minus :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "-" 65)
147 fixes uminus :: "'a \<Rightarrow> 'a" ("- _" [81] 80)
150 fixes times :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "*" 70)
152 {\tt infix} gibt an, dass der Operator zwischen den Zahlen steht und nicht, wie in ''abstract syntax``, vorne oben.
153 Die Zahlen rechts davon legen die Priorit\"at fest. 70 f\"ur Mal ist gr\"osser als 65 f\"ur Plus und wird daher zuerst berechnet.
155 Wollen Sie wissen, wie die einzelnen Rechengesetze aussehen, k\"onnen Sie im Internet folgenden Link ansehen: http://isabelle.in.tum.de/dist/library/HOL/Groups.html
157 \paragraph{} Der Vorgang, bei dem aus einem {\tt string} ein Term entsteht, nennt man Parsing. Dazu wird Wissen aus der Theorie ben\"otigt, denn {\tt str2term} nimmt intern eine parse-Funktion, bei der immer das gesamte \isac{}-Wissen verwendet wird. Bei dieser Funktion wird weiters festgelegt, aus welcher Theorie das Wissen genommen werden soll.
158 {\footnotesize\begin{verbatim}
159 > parse Isac.thy "a + b";
160 val it = Some "a + b" : Thm.cterm Library.option
162 Um sich das Weiterrechnen zu erleichtern, kann das Ergebnis vom Parsing auf eine Variable, wie zum Beispiel {\tt t} gespeichert werden:
163 {\footnotesize\begin{verbatim}
164 > val t = parse Isac.thy "a + b";
165 val t = Some "a + b" : Thm.cterm Library.option
167 {\tt Some} bedeutet, dass das n\"otige Wissen vorhanden ist, um die Rechnung durchzuf\"uhren. {\tt None} zeigt uns, dass das Wissen fehlt oder ein Fehler aufgetreten ist. Daher sieht man im folgenden Beispiel, dass {\tt HOL.thy} nicht ausreichend Wissen enth\"alt:
168 {\footnotesize\begin{verbatim}
169 > parse HOL.thy "a + b";
170 val it = None : Thm.cterm Library.option
172 Anschliessend zeigen wir Ihnen noch ein zweites Beispiel, bei dem sowohl ein Fehler aufgetreten ist, als auch das Wissen fehlt:
173 {\footnotesize\begin{verbatim}
174 > parse Isac.thy "a + ";
175 *** Inner syntax error: unexpected end of input
176 *** Expected tokens: "contains_root" "is_root_free" "q_" "M_b" "M_b'"
177 *** "Integral" "differentiate" "E_" "some_of" "||" "|||" "argument_in"
178 *** "filter_sameFunId" "I__" "letpar" "Rewrite_Inst" "Rewrite_Set"
179 *** "Rewrite_Set_Inst" "Check_elementwise" "Or_to_List" "While" "Script"
180 *** "\\" "\\" "\\" "CHR" "xstr" "SOME" "\\" "@"
181 *** "GREATEST" "[" "[]" "num" "\\" "{)" "{.." "\\" "(|"
182 *** "\\" "SIGMA" "()" "\\" "PI" "\\" "\\" "{" "INT"
183 *** "UN" "{}" "LEAST" "\\" "0" "1" "-" "!" "?" "?!" "\\"
184 *** "\\" "\\" "\\!" "THE" "let" "case" "~" "if" "ALL"
185 *** "EX" "EX!" "!!" "_" "\\" "\\" "PROP" "[|" "OFCLASS"
186 *** "\\" "op" "\\" "%" "TYPE" "id" "longid" "var" "..."
188 val it = None : Thm.cterm Library.option
191 Das mathematische Wissen w\"achst mit jeder Theorie von ProtoPure bis Isac. In den folgenden Beispielen wird gezeigt, wie das Wissen w\"achst.
193 {\footnotesize\begin{verbatim}
195 > parse HOL.thy "2^^^3";
196 *** Inner lexical error at: "^^^3"
197 val it = None : Thm.cterm Library.option
199 ''Inner lexical error`` und ''None`` bedeuten, dass ein Fehler aufgetreten ist, denn das Wissen \"uber {\tt *} findet sich erst in der {\tt theorie group}.
201 {\footnotesize\begin{verbatim}
203 > parse HOL.thy "d_d x (a + x)";
204 val it = None : Thm.cterm Library.option
206 Hier wiederum ist noch kein Wissen \"uber das Differenzieren vorhanden.
208 {\footnotesize\begin{verbatim}
210 > parse Rational.thy "2^^^3";
211 val it = Some "2 ^^^ 3" : Thm.cterm Library.option
214 {\footnotesize\begin{verbatim}
216 > val Some t4 = parse Rational.thy "d_d x (a + x)";
217 val t4 = "d_d x (a + x)" : Thm.cterm
220 {\footnotesize\begin{verbatim}
222 > val Some t5 = parse Diff.thy "d_d x (a + x)";
223 val t5 = "d_d x (a + x)" : Thm.cterm
225 Die letzen drei Aufgaben k\"onnen schon gel\"ost werden, da {\tt Rational.thy} \"uber das n\"otige Wissen verf\"ugt.
227 \section{Details von Termen}
228 Mit Hilfe der darunterliegenden Darstellung sieht man, dass ein cterm in einen Term umgewandelt werden kann.
229 {\footnotesize\begin{verbatim}
231 val it = fn : Thm.cterm -> Term.term
233 Durch die Umwandlung eines cterms in einen Term sieht man die einzelnen Teile des Terms. ''Free`` bedeutet, dass man die Variable \"andern kann.
234 {\footnotesize\begin{verbatim}
237 Free ("d_d", "[RealDef.real, RealDef.real] => RealDef.real") $ ... $
241 In diesem Fall sagt uns das ''Const``, dass die Variable eine Konstante ist, also ein Fixwert, der immer die selbe Funktion hat.
242 {\footnotesize\begin{verbatim}
245 Const ("Diff.d_d", "[RealDef.real, RealDef.real] => RealDef.real") $ ... $
248 Sollten verschiedene Teile des ''output`` (= das vom Computer Ausgegebene) nicht sichtbar sein, kann man mit einem bestimmten Befehl alles angezeigt werden.
249 {\footnotesize\begin{verbatim}
251 val it = fn : int -> unit
253 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.
254 {\footnotesize\begin{verbatim}
259 Free ("d_d", "[RealDef.real, RealDef.real] => RealDef.real") $
260 Free ("x", "RealDef.real") $
261 (Const ("op +", "[RealDef.real, RealDef.real] => RealDef.real") $
262 Free ("a", "RealDef.real") $ Free ("x", "RealDef.real"))
269 Const ("Diff.d_d", "[RealDef.real, RealDef.real] => RealDef.real") $
270 Free ("x", "RealDef.real") $
271 (Const ("op +", "[RealDef.real, RealDef.real] => RealDef.real") $
272 Free ("a", "RealDef.real") $ Free ("x", "RealDef.real"))
275 \paragraph{Versuchen Sie es!}
276 Eine andere Variante um den Unterschied der beiden Terme zu sehen ist folgende:
277 {\footnotesize\begin{verbatim}
278 > (*-4-*) val thy = Rational.thy;
280 {ProtoPure, CPure, HOL, Set, Typedef, Fun, Product_Type, Lfp, Gfp,
281 Sum_Type, Relation, Record, Inductive, Transitive_Closure,
282 Wellfounded_Recursion, NatDef, Nat, NatArith, Divides, Power,
283 SetInterval, Finite_Set, Equiv, IntDef, Int, Datatype_Universe,
284 Datatype, Numeral, Bin, IntArith, Wellfounded_Relations, Recdef, IntDiv,
285 IntPower, NatBin, NatSimprocs, Relation_Power, PreList, List, Map,
286 Hilbert_Choice, Main, Lubs, PNat, PRat, PReal, RealDef, RealOrd,
287 RealInt, RealBin, RealArith0, RealArith, RComplete, RealAbs, RealPow,
288 Ring_and_Field, Complex_Numbers, Real, ListG, Tools, Script, Typefix,
289 Float, ComplexI, Descript, Atools, Simplify, Poly, Rational}
291 > ((atomty) o term_of o the o (parse thy)) "d_d x (a + x)";
294 *** Free (d_d, [real, real] => real)
296 *** . Const (op +, [real, real] => real)
297 *** . . Free (a, real)
298 *** . . Free (x, real)
304 > (*-5-*) val thy = Diff.thy;
306 {ProtoPure, CPure, HOL, Set, Typedef, Fun, Product_Type, Lfp, Gfp,
307 Sum_Type, Relation, Record, Inductive, Transitive_Closure,
308 Wellfounded_Recursion, NatDef, Nat, NatArith, Divides, Power,
309 SetInterval, Finite_Set, Equiv, IntDef, Int, Datatype_Universe,
310 Datatype, Numeral, Bin, IntArith, Wellfounded_Relations, Recdef, IntDiv,
311 IntPower, NatBin, NatSimprocs, Relation_Power, PreList, List, Map,
312 Hilbert_Choice, Main, Lubs, PNat, PRat, PReal, RealDef, RealOrd,
313 RealInt, RealBin, RealArith0, RealArith, RComplete, RealAbs, RealPow,
314 Ring_and_Field, Complex_Numbers, Real, Calculus, Trig, ListG, Tools,
315 Script, Typefix, Float, ComplexI, Descript, Atools, Simplify, Poly,
316 Equation, LinEq, Root, RootEq, Rational, RatEq, RootRat, RootRatEq,
317 PolyEq, LogExp, Diff} : Theory.theory
319 > ((atomty) o term_of o the o (parse thy)) "d_d x (a + x)";
322 *** Const (Diff.d_d, [real, real] => real)
324 *** . Const (op +, [real, real] => real)
325 *** . . Free (a, real)
326 *** . . Free (x, real)
333 \chapter{''Rewriting``}
334 \section{Was ist Rewriting?}
335 Bei Rewriting handelt es sich um das Umformen von Termen nach vorgegebenen Regeln. Folgende zwei Funktionen sind notwendig:
336 {\footnotesize\begin{verbatim}
342 rls' -> bool -> thm' -> cterm' -> (string * string list) Library.option
344 Die Funktion hat zwei Argumente, die mitgeschickt werden m\"ussen, damit die Funktion arbeiten kann. Das letzte Element {\tt (cterm' * cterm' list) Library.option} im unteren Term ist das Ergebnis, das die Funktionen {\tt rewrite} zur\"uckgeben und die zwei vorhergehenden Argumente, {\tt theorem} und {\tt cterm}, sind die f\"ur uns wichtigen. {\tt Theorem} ist die Rechenregel und {\tt cterm} jene Formel auf die die Rechenregel angewendet wird.
345 {\footnotesize\begin{verbatim}
351 rls' ->bool -> 'a -> thm' -> cterm' -> (cterm' * cterm' list) Library.option
353 Die Funktion {\tt rewrite\_inst} wird ben\"otigt, um Gleichungen, Rechnungen zum Differenzieren etc. zu l\"osen. Dabei wird die gebundene Variable (bdv) instanziiert, d.h. es wird die Variable angegeben, nach der man differenzieren will, bzw. f\"ur die ein Wert bei einer Gleichung herauskommen soll.
354 Um zu sehen wie der Computer vorgeht nehmen wir folgendes Beispiel, dessen Ergebnis offenbar 0 ist, was der Computer jedoch erst nach einer Reihe von Schritten herausfindet.
355 Im Beispiel wird differenziert, wobei \isac's Schreibweise jene von Computer Algebra Systemen (CAS) anzugleichen: in CAS wird differenziert mit $\frac{d}{dx}\; x^2 + 3 \cdot x + 4$, in \isac{} mit {\tt d\_d x (x \^{ }\^{ }\^{ } 2 + 3 * x + 4)}.
356 Zuerst werden die einzelnen Werte als Variablen gespeichert:
357 {\footnotesize\begin{verbatim}
358 > val thy' = "Diff.thy";
359 val thy' = "Diff.thy" : string
360 > val ro = "tless_true";
361 val ro = "tless_true" : string
362 > val er = "eval_rls";
363 val er = "eval_rls" : string
364 > val inst = [("bdv","x::real")];
365 val inst = [("bdv", "x::real")] : (string * string) list
366 > val ct = "d_d x (a + a * (2 + b))";
367 val ct = "d_d x (a + a * (2 + b))" : string
369 Nun wird die Rechnung nach den Regeln ausgerechnet, wobei am Ende mehrere Dinge zugleich gemacht werden.
370 Folgende Regeln werden ben\"otigt: Summenregel, Produktregel, Multiplikationsregel mit einem konstanten Faktor und zum Schluss die Additionsregel.
371 {\footnotesize\begin{verbatim}
372 > val Some (ct,_) = rewrite_inst thy' ro er true inst ("diff_sum","") ct;
373 val ct = "d_d x a + d_d x (a * (2 + b))" : cterm'
374 > val Some (ct,_) = rewrite_inst thy' ro er true inst ("diff_prod","") ct;
375 val ct = "d_d x a + (d_d x a * (2 + b) + a * d_d x (2 + b))" : cterm'
376 > val Some (ct,_) = rewrite_inst thy' ro er true inst ("diff_const","") ct;
377 val ct = "d_d x a + (d_d x a * (2 + b) + a * 0) " : cterm'
378 > val Some (ct,_) = rewrite_inst thy' ro er true inst ("diff_const","") ct;
379 val ct = "d_d x a + (0 * (2 + b) + a * 0)" : cterm'
380 > val Some (ct,_) = rewrite_inst thy' ro er true inst ("diff_const","") ct;
381 val ct = "0 + (0 * (2 + b) + a * 0)" : cterm'
382 > val Some (ct,_) = rewrite_set thy' true "make_polynomial" ct;
383 val ct = "0" : string
385 Was {\tt rewrite\_set} genau macht, finden Sie im n\"achsten Kapitel.
387 Dies w\"are ein etwas ernsthafteres Beispiel zum Differenzieren:
388 {\footnotesize\begin{verbatim}
389 > val ct = "d_d x (x ^^^ 2 + 3 * x + 4)";
390 > val Some (ct,_) = rewrite_inst thy' ro er true inst ("diff_sum","") ct;
392 \paragraph{Versuchen Sie es,} diese Beispiel zu Ende zu f\"uhren! Die Regeln, die \isac{} kennt und zum Umformen verwenden kann, finden Sie im Internet \footnote{{\tiny\tt http://www.ist.tugraz.at/projects/isac/www/kbase/thy/browser\_info/HOL/HOL-Real/Isac/Diff.html}}.
394 \section{Welche W\"unsche kann man an Rewriting stellen?}
395 Es gibt verschiedene Varianten von Rewriting, die alle eine bestimmte Bedeutung haben.
396 {\tt rewrite\_ set} wandelt Terme in ein ganzes rule set um, die normalerweise nur mit einem Theorem vereinfacht dargestellt werden.
397 Hierbei werden auch folgende Argumente verwendet:\\
399 \def\arraystretch{1.5}
400 \begin{tabular}{lp{11.0cm}}
401 {\tt theory} & Die Theory von Isabelle, die alle n\"otigen Informationen f\"ur das Parsing {\tt term} enth\"alt. \\
402 {\tt rew\_ord}& die Ordnung f\"ur das geordnete Rewriting. F\"ur {\em no} ben\"otigt das geordnete Rewriting {\tt tless\_true}, eine Ordnung, die f\"ur alle nachgiebigen Argumente true ist \\
403 {\tt rls} & Das rule set; zur Auswertung von bestimmten Bedingungen in {\tt thm} falls {\tt thm} eine conditional rule ist \\
404 {\tt bool} & ein Bitschalter, der die Berechnungen der m\"oglichen condition in {\tt thm} ausl\"ost: wenn sie {\tt false} ist, dann wird die condition bewertet und auf Grund des Resultats wendet man {\tt thm} an, oder nicht; wenn {\tt true} dann wird die condition nicht ausgewertet, aber man gibt sie in eine Menge von Hypothesen \\
405 {\tt thm} & das theorem versucht den {\tt term} zu \"uberschreiben \\
406 {\tt term} & {\tt thm} wendet Rewriting m\"oglicherweise auf den Term an \\
409 {\footnotesize\begin{verbatim}
411 val it = fn : theory' -> bool -> rls' -> ...
413 {\footnotesize\begin{verbatim}
415 val it = fn : theory' -> bool -> subs' -> .
417 Wenn man sehen m\"ochte wie Rewriting bei den einzelnen theorems funktioniert kann man dies mit {\tt trace\_rewrite} versuchen.
418 {\footnotesize\begin{verbatim}
419 > trace_rewrite := true;
425 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.
426 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.
427 Ein Beispiel f\"ur einen rule set ist folgendes:
428 {\footnotesize\begin{verbatim}
432 {\footnotesize\begin{verbatim}
434 val it = "?s = ?t ==> ?t = ?s" : Thm.thm
438 {id = "rearrange_assoc",
439 scr = Script (Free ("empty_script", "RealDef.real")),
449 rew_ord = ("dummy_ord", fn),
459 rew_ord = ("dummy_ord", fn),
462 [Thm ("sym_radd_assoc", "?m1 + (?n1 + ?k1) = ?m1 + ?n1 + ?k1" [.]),
465 "?m1 * (?n1 * ?k1) = ?m1 * ?n1 * ?k1" [.])],
466 rew_ord = ("e_rew_ord", fn),
471 \section{Berechnung von Konstanten}
472 Sobald Konstanten in dem Bereich des Subterms sind, k\"onnen sie von einer Funktion berechnet werden:
473 {\footnotesize\begin{verbatim}
481 Term.term -> Theory.theory -> (string * Term.term) Library.option) ->
482 cterm' -> (string * thm') Library.option
491 Term.term -> Theory.theory -> (string * Term.term) Library.option) ->
492 Term.term -> (Term.term * (string * Thm.thm)) Library.option
494 Man bekommt das Ergebnis und das theorem bezieht sich darauf. Daher sind die folgenden mathematischen Rechnungen m\"oglich:
495 {\footnotesize\begin{verbatim}
498 [("Vars", ("Tools.Vars", fn)), ("matches", ("Tools.matches", fn)),
499 ("lhs", ("Tools.lhs", fn)), ("plus", ("op +", fn)),
500 ("times", ("op *", fn)), ("divide_", ("HOL.divide", fn)),
501 ("power_", ("Atools.pow", fn)), ("is_const", ("Atools.is'_const", fn)),
502 ("le", ("op <", fn)), ("leq", ("op <=", fn)),
503 ("ident", ("Atools.ident", fn)), ("sqrt", ("Root.sqrt", fn)),
504 ("Test.is_root_free", ("is'_root'_free", fn)),
505 ("Test.contains_root", ("contains'_root", fn))]
513 Term.term -> Theory.theory -> (string * Term.term) Library.option))) list
519 \chapter{Termordnung}
520 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.
522 \section{Beispiel f\"ur Termordnungen}
523 Es ist nicht unbedeutend, eine Verbindung zu Termen herzustellen, die wirklich eine Ordnung besitzen. Diese Ordnungen sind selbstaufrufende Bahnordnungen:
525 {\footnotesize\begin{verbatim}
527 val it = fn : bool -> Theory.theory -> subst -> Term.term * Term.term -> b ool
529 val it = fn : subst -> Term.term * Term.term -> bool
532 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.
534 {\section{Geordnetes Rewriting}}
535 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.
538 \chapter{Problem hierachy}
539 \section{''Matching``}
540 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:
541 {\footnotesize\begin{verbatim}
543 val it = fn : Theory.theory -> Term.term -> Term.term -> bool
545 Die folgende Gleichung wird in Operatoren und freie Variablen zerlegt.
546 {\footnotesize\begin{verbatim}
547 > val t = (term_of o the o (parse thy)) "3 * x^^^2 = 1";
549 Const ("op =", "[RealDef.real, RealDef.real] => bool") $
550 (Const ("op *", "[RealDef.real, RealDef.real] => RealDef.real") $
551 Free ("3", "RealDef.real") $
554 "[RealDef.real, RealDef.real] => RealDef.real") $
555 Free ("x", "RealDef.real") $ Free ("2", " RealDef.real"))) $
556 Free ("1", "RealDef.real") : Term.term
558 Nun wird ein Modell erstellt, das sich nicht auf bestimmte Zahlen bezieht, sondern nur eine generelle Zerlegung durchf\"uhrt.
559 {\footnotesize\begin{verbatim}
560 > val p = (term_of o the o (parse thy)) "a * b^^^2 = c";
562 Const ("op =", "[RealDef.real, RealDef.real] => bool") $
563 (Const ("op *", "[RealDef.real, RealDef.real] => RealDef.real") $
564 Free ("a", "RealDef.real") $
567 "[RealDef.real, RealDef.real] => RealDef.real") $
568 Free ("b", "RealDef.real") $ Free ("2", "RealDef.real"))) $
569 Free ("c", "RealDef.real") : Term.term
571 Dieses Modell enth\"alt sogenannte \textit{scheme variables}.
572 {\footnotesize\begin{verbatim}
576 "*** . Const (op *)""*** . . Free (a, )"
577 "*** . . Const (Atools.pow)"
578 "*** . . . Free (b, )"
579 "*** . . . Free (2, )"
582 val it = "\n" : string
584 Das Modell wird durch den Befehl \textit{free2var} erstellt.
585 {\footnotesize\begin{verbatim}
587 val it = fn : Term.term -> Term.term
588 > val pat = free2var p;
590 Const ("op =", "[RealDef.real, RealDef.real] => bool") $
591 (Const ("op *", "[RealDef.real, RealDef.real] => RealDef.real") $
592 Var (("a", 0), "RealDef.real") $
595 "[RealDef.real, RealDef.real] => RealDef.real") $
596 Var (("b", 0), "RealDef.real") $
597 Free ("2", "RealDef.real"))) $ Var (("c", 0), "RealDef.real")
599 > Sign.string_of_term (sign_of thy) pat;
600 val it = "?a * ?b ^^^ 2 = ?c" : string
602 Durch \textit{atomt pat} wird der Term aufgespalten und in eine Form gebracht, die f\"ur die weiteren Schritte ben\"otigt wird.
603 {\footnotesize\begin{verbatim}
608 "*** . . Var ((a, 0), )"
609 "*** . . Const (Atools.pow)"
610 "*** . . . Var ((b, 0), )"
611 "*** . . . Free (2, )"
612 "*** . Var ((c, 0), )"
614 val it = "\n" : string
616 Jetzt kann das Matching an den beiden vorigen Terme angewendet werden.
617 {\footnotesize\begin{verbatim}
620 > val t2 = (term_of o the o (parse thy)) "x^^^2 = 1";
622 Const ("op =", "[RealDef.real, RealDef.real] => bool") $
625 "[RealDef.real, RealDef.real] => RealDef.real") $
626 Free ("x", "RealDef.real") $ Free ("2", "RealDef.real")) $
627 Free ("1", "RealDef.real") : Term.term
628 > matches thy t2 pat;
629 val it = false : bool
630 > val pat2 = (term_of o the o (parse thy)) "?u^^^2 = ?v";
632 Const ("op =", "[RealDef.real, RealDef.real] => bool") $
635 "[RealDef.real, RealDef.real] => RealDef.real") $
636 Var (("u", 0), "RealDef.real") $ Free ("2", "RealDef.real")) $
637 Var (("v", 0), "RealDef.real") : Term.term
638 > matches thy t2 pat2;
642 \section{Zugriff auf die hierachy}
643 Man verwendet folgenden Befehl, um sich Zugang zur hierachy von problem type zu verschaffen.
644 {\footnotesize\begin{verbatim}
646 val it = fn : unit -> unit
650 ["simplification", "polynomial"],
651 ["simplification", "rational"],
652 ["vereinfachen", "polynom", "plus_minus"],
653 ["vereinfachen", "polynom", "klammer"],
654 ["vereinfachen", "polynom", "binom_klammer"],
655 ["probe", "polynom"],
657 ["equation", "univariate", "linear"],
658 ["equation", "univariate", "root", "sq", "rat"],
659 ["equation", "univariate", "root", "normalize"],
660 ["equation", "univariate", "rational"],
661 ["equation", "univariate", "polynomial", "degree_0"],
662 ["equation", "univariate", "polynomial", "degree_1"],
663 ["equation", "univariate", "polynomial", "degree_2", "sq_only"],
664 ["equation", "univariate", "polynomial", "
665 degree_2", "bdv_only"],
666 ["equation", "univariate", "polynomial", "degree_2", "pqFormula"],
667 ["equation", "univariate", "polynomial", "degree_2", "abcFormula"],
668 ["equation", "univariate", "polynomial", "degree_3"],
669 ["equation", "univariate", "polynomial", "degree_4"],
670 ["equation", "univariate", "polynomial", "normalize"],
671 ["equation", "univariate", "expanded", "degree_2"],
672 ["equation", "makeFunctionTo"],
673 ["function", "derivative_of", "named"],
674 ["function", "maximum_of", "on_interval"],
675 ["function", "make", "by_explicit"],
676 ["function", "make", "by_new_variable"],
677 ["function", "integrate", "named"],
678 ["tool", "find_values"],
679 ["system", "linear", "2x2", "triangular"],
680 ["system", "linear", "2x2", "normalize"],
681 ["system", "linear", "3x3"],
682 ["system", "linear", "4x4", "triangular"],
683 ["system", "linear", "4x4", "normalize"],
686 ["Biegelinien", "MomentGegebene"],
687 ["Biegelinien", "einfache"],
688 ["Biegelinien", "QuerkraftUndMomentBestimmte"],
689 ["Biegelinien", "vonBelastungZu"],
690 ["Biegelinien", "setzeRandbedingungen"],
691 ["Berechnung", "numerischSymbolische"],
692 ["test", "equation", "univariate", "linear"],
693 ["test", "equation", "univariate", "plain_square"],
694 ["test", "equation", "univariate", "polynomial", "degree_two", "pq_formula"],
695 ["test", "equation", "univariate", "polynomial", "degree_two", "abc_formula"],
696 ["test", "equation", "univariate", "squareroot"],
697 ["test", "equation", "univariate", "normalize"],
698 ["test", "equation", "univariate", "sqroot-test"]
703 \section{Die passende ''formalization`` f\"ur den problem type}
704 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.
706 \section{''problem-refinement``}
707 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.
708 {\footnotesize\begin{verbatim}
710 val it = fn : fmz_ -> pblID -> SpecifyTools.match list
711 > val fmz = ["equality (sqrt(9 + 4 * x)=sqrt x
713 # "soleFor x","errorBound (eps=0)",
716 ["equality (sqrt(9 + 4 * x)=sqrt x + sqrt (5 + x))", "soleFor x",
717 "errorBound (eps=0)", ...] : string list
718 > refine fmz ["univariate","equation"];
719 *** pass ["equation","univariate"]
720 *** comp_dts: ??.empty $ soleFor x
721 Exception- ERROR raised
723 Wenn die ersten zwei Regeln nicht angewendet werden k\"onnen, kommt die dritte zum Einsatz:
724 {\footnotesize\begin{verbatim}
725 > val fmz = ["equality (x + 1 = 2)",
726 # "solveFor x","errorBound (eps=0)",
728 val fmz = ["equality (x + 1 = 2)", "solveFor x", "errorBound (eps=0)", ...]
730 > refine fmz ["univariate","equation"];
731 *** pass ["equation","univariate"]
732 *** pass ["equation","univariate","linear"]
733 *** pass ["equation","univariate","root"]
734 *** pass ["equation","univariate","rational"]
735 *** pass ["equation","univariate","polynomial" ]
736 *** pass ["equation","univariate","polynomial","degree_0"]
737 *** pass ["equation","univariate","polynomial","degree_1"]
738 *** pass ["equation","univariate","polynomial","degree_2"]
739 *** pass ["equation","univariate","polynomial","degree_3"]
740 *** pass ["equation","univariate","polynomial","degree_4"]
741 *** pass ["equation","univariate","polynomial","normalize"]
744 (["univariate", "equation"],
745 {Find = [Correct "solutions L"], With = [...], ...}),
746 NoMatch (["linear", "univariate", ...], {Find = [...], ...}),
747 NoMatch (["root", ...], ...), ...] : SpecifyTools.match list
749 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).
752 \chapter{''Methods``}
753 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.
754 \section{Der ''Syntax`` des script}
755 Syntax beschreibt den Zusammenhang der einzelnen Zeichen und Zeichenfolgen mit den Theorien.
756 Er kann so definiert werden:
758 123\=123\=expr ::=\=$|\;\;$\=\kill
759 \>script ::= {\tt Script} id arg$\,^*$ = body\\
760 \>\>arg ::= id $\;|\;\;($ ( id :: type ) $)$\\
762 \>\>expr ::= \>\>{\tt let} id = expr $($ ; id = expr$)^*$ {\tt in} expr\\
763 \>\>\>$|\;$\>{\tt if} prop {\tt then} expr {\tt else} expr\\
764 \>\>\>$|\;$\>listexpr\\
766 \>\>\>$|\;$\>seqex id\\
767 \>\>seqex ::= \>\>{\tt While} prop {\tt Do} seqex\\
768 \>\>\>$|\;$\>{\tt Repeat} seqex\\
769 \>\>\>$|\;$\>{\tt Try} seqex\\
770 \>\>\>$|\;$\>seqex {\tt Or} seqex\\
771 \>\>\>$|\;$\>seqex {\tt @@} seqex\\
772 \>\>\>$|\;$\>tac $($ id $|$ listexpr $)^*$\\
777 \section{\"Uberpr\"ufung der Auswertung}
778 Das Kontrollsystem arbeitet mit den folgenden Script-Ausdr\"ucken, die {\it tacticals} genannt werden:
780 \item{{\tt while} prop {\tt Do} expr id}
781 \item{{\tt if} prop {\tt then} expr {\tt else} expr}
783 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:
785 \item{{\tt Repeat} expr id}
786 \item{{\tt Try} expr id}
787 \item{expr {\tt Or} expr id}
788 \item{expr {\tt @@} expr id}
794 \chapter{Befehle von \isac{}}
795 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.\
796 \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.\
797 \newline\linebreak \textbf{Init\_Proof} bildet mit einem ''proof tree`` ein leeres Modell.\
798 \newline\linebreak \textbf{Model\_Problem problem} bestimmt ein problemtype, das wom\"oglich in der ''hierachy`` gefunden wurde, und verwendet es f\"ur das Umformen.\
799 \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.\
800 \newline\linebreak \textbf{Specify\_Theorie theory, Specify\_Problem proble, Specify\_Method method} gibt das entsprechende Element des Basiswissens an.\
801 \newline\linebreak \textbf{Refine\_Problem problem} sucht nach einem Problem in der hierachy, das auf das vorhandene zutrifft.\
802 \newline\linebreak \textbf{Apply\_Method method} beendet das Modell und die Beschreibung. Danach wird die L\"osungmeldung ge\"offnet.\
803 \newline\linebreak \textbf{Free\_Solve} beginnt eine L\"osungsmeldung ohne die Hilfe einer method.\
804 \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``.\
805 \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.\
806 \newline\linebreak \textbf{Rewrite\_Set ruleset} hat \"ahnliche Funktionen wie Rewrite, gilt aber f\"ur einen ganzen Satz von theorems, dem rule set.\
807 \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.\
808 \newline\linebreak \textbf{Calculate operation} berechnet das Ergebnis der Eingabe mit der aktuellen Formel (plus, minus, times, cancel, pow, sqrt).\
809 \newline\linebreak \textbf{Substitute substitution} f\"ugt der momentanen Formel {\tt substitution} hinzu und wandelt es um.\
810 \newline\linebreak \textbf{Take formula} startet eine neue Reihe von Rechnungen in den Formeln, wo sich schon eine andere Rechnung befindet.\
811 \newline\linebreak \textbf{Subproblem (theory, problem)} beginnt ein subproblem innerhalb einer Rechnung.\
812 \newline\linebreak \textbf{Function formula} ruft eine Funktion auf, in der der Name in der Formel enthalten ist. ???????\
813 \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.\
814 \newline\linebreak \textbf{Check\_elementwise assumption} wird in Bezug auf die aktuelle Formel verwendet, die Elemente in einer Liste enth\"alt.\
815 \newline\linebreak \textbf{Or\_to\_List} wandelt eine Verbindung von Gleichungen in eine Liste von Gleichungen um.\
816 \newline\linebreak \textbf{Check\_postcond} \"uberpr\"uft die momentane Formel im Bezug auf die Nachbedinung beim Beenden des subproblem.\
817 \newline\linebreak \textbf{End\_Proof} beendet eine \"Uberpr\"ufung und gibt erst dann ein Ergebnis aus, wenn Check\_postcond erfolgreich abgeschlossen wurde.
819 \section{Die Funktionsweise der mathematic engine}
820 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.
821 \newline Im Anschluss werden Sie einen Rechenbeweis sehen, der von der L\"osung einer Gleichung (= equation) handelt, bei der diese automatisch differenziert wird.
822 {\footnotesize\begin{verbatim}
823 ??????????????????????????????????????????????????????????????????????????????????
825 ML> val fmz = ["equality ((x+#1)*(x+#2)=x^^^#2+#8)","solveFor x",
826 "errorBound (eps=#0)","solutions L"];
828 ["equality ((x+#1)*(x+#2)=x^^^#2+#8)","solveFor x","errorBound (eps=#0)",
829 "solutions L"] : string list
831 ML> val spec as (dom, pbt, met) = ("SqRoot.thy",["univariate","equation"],
832 ("SqRoot.thy","no_met"));
833 val dom = "SqRoot.thy" : string
834 val pbt = ["univariate","equation"] : string list
835 val met = ("SqRoot.thy","no_met") : string * string
838 \section{Der Beginn einer Rechnung}
840 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:
841 {\footnotesize\begin{verbatim}
842 ????????????????????????????????????????????????????????????????????????????????????????????
843 ML> val (mID,m) = ("Init_Proof",Init_Proof (fmz, (dom,pbt,met)));
844 val mID = "Init_Proof" : string
847 (["equality ((x+#1)*(x+#2)=x^^^#2+#8)","solveFor x","errorBound (eps=#0)",
848 "solutions L"],("SqRoot.thy",[#,#],(#,#))) : mstep
850 ML> val (p,_,f,nxt,_,pt) = me (mID,m) e_pos' c EmptyPtree;
851 val p = ([],Pbl) : pos'
852 val f = Form' (PpcKF (0,EdUndef,0,Nundef,(#,#))) : mout
853 val nxt = ("Refine_Tacitly",Refine_Tacitly ["univariate","equation"])
858 {branch=#,cell=#,env=#,loc=#,meth=#,model=#,origin=#,ostate=#,probl=#,
859 result=#,spec=#},[]) : ptree
861 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.
862 {\footnotesize\begin{verbatim}
863 ?????????????????????????????????????????????????????????????????????????????????????????????
864 ML> Compiler.Control.Print.printDepth:=8; (*4 default*)
873 {Find=[Incompl "solutions []"],
874 Given=[Incompl "equality",Incompl "solveFor"],Relate=[],
875 Where=[False "matches (?a = ?b) e_"],With=[]}))) : mout
877 {\footnotesize\begin{verbatim}
878 ?????????????????????????????????????????????????????????????????????????????????????????????
880 val it = ("Refine_Tacitly",Refine_Tacitly ["univariate","equation"])
883 ML> val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
884 val nxt = ("Model_Problem",Model_Problem ["normalize","univariate","equation"])
887 ML> val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
890 \section{The phase of modeling}
891 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.
892 {\footnotesize\begin{verbatim}
893 ?????????????????????????????????????????????????????????????????????????????????????????????
896 ("Add_Given",Add_Given "equality ((x + #1) * (x + #2) = x ^^^ #2 + #8)")
899 ML> val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
900 val nxt = ("Add_Given",Add_Given "solveFor x") : string * mstep
902 ML> val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
903 val nxt = ("Add_Find",Add_Find "solutions L") : string * mstep
905 ML> val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
906 val f = Form' (PpcKF (0,EdUndef,0,Nundef,(#,#))) : mout
908 {\footnotesize\begin{verbatim}
909 ?????????????????????????????????????????????????????????????????????????????????????????????
910 ML> Compiler.Control.Print.printDepth:=8;
917 {Find=[Correct "solutions L"],
918 Given=[Correct "equality ((x + #1) * (x + #2) = x ^^^ #2 + #8)",
919 Correct "solveFor x"],Relate=[],Where=[],With=[]}))) : mout
923 \section{The phase of specification}
924 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.
925 {\footnotesize\begin{verbatim}
926 ??????????????????????????????????????????????????????????????????????????????????????????
928 val it = ("Specify_Domain",Specify_Domain "SqRoot.thy") : string * mstep
930 ML> val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
932 ("Specify_Problem",Specify_Problem ["normalize","univariate","equation"])
937 {branch=#,cell=#,env=#,loc=#,meth=#,model=#,origin=#,ostate=#,probl=#,
938 result=#,spec=#},[]) : ptree
940 Die me erkennt den richtigen Problem type und arbeitet so weiter:
941 {\footnotesize\begin{verbatim}
942 ?????????????????????????????????????????????????????????????????????????????????????????
943 ML> val nxt = ("Specify_Problem",
944 Specify_Problem ["polynomial","univariate","equation"]);
945 ML> val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
946 val f = Form' (PpcKF (0,EdUndef,0,Nundef,(#,#))) : mout
948 ("Refine_Problem",Refine_Problem ["normalize","univariate","equation"])
951 ML> val nxt = ("Specify_Problem",
952 Specify_Problem ["linear","univariate","equation"]);
953 ML> val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
958 (Problem ["linear","univariate","equation"],
959 {Find=[Correct "solutions L"],
960 Given=[Correct "equality ((x + #1) * (x + #2) = x ^^^ #2 + #8)",
961 Correct "solveFor x"],Relate=[],
963 "matches (?a + ?b * x = #0) ((x + #1) * (x + #2) = x ^^^ #2 + #8)"],
966 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``].
967 {\footnotesize\begin{verbatim}
968 ????????????????????????????????????????????????????????????????????????????????????????????
969 ML> val nxt = ("Refine_Problem",
970 Refine_Problem ["linear","univariate","equation
971 ML> val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
972 val f = Problems (RefinedKF [NoMatch #]) : mout
974 ML> Compiler.Control.Print.printDepth:=9;f;Compiler.Control.Print.printDepth:=4;
979 (["linear","univariate","equation"],
980 {Find=[Correct "solutions L"],
981 Given=[Correct "equality ((x + #1) * (x + #2) = x ^^^ #2 + #8)",
982 Correct "solveFor x"],Relate=[],
984 "matches (?a + ?b * x = #0) ((x + #1) * (x + #2) = x ^^^ #2 + #8)"],
987 ML> val nxt = ("Refine_Problem",Refine_Problem ["univariate","equation"]);
988 ML> val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
991 (RefinedKF [Matches #,NoMatch #,NoMatch #,NoMatch #,NoMatch #,Matches #])
995 ML> Compiler.Control.Print.printDepth:=9;f;Compiler.Control.Print.printDepth:=4;
1000 (["univariate","equation"],
1001 {Find=[Correct "solutions L"],
1002 Given=[Correct "equality ((x + #1) * (x + #2) = x ^^^ #2 + #8)",
1003 Correct "solveFor x"],Relate=[],
1007 (["linear","univariate","equation"],
1008 {Find=[Correct "solutions L"],
1009 Given=[Correct "equality ((x + #1) * (x + #2) = x ^^^ #2 + #8)",
1010 Correct "solveFor x"],Relate=[],
1012 "matches (?a + ?b * x = #0) ((x + #1) * (x + #2) = x ^^^ #2 + #8)"],
1018 (["normalize","univariate","equation"],
1019 {Find=[Correct "solutions L"],
1020 Given=[Correct "equality ((x + #1) * (x + #2) = x ^^^ #2 + #8)",
1021 Correct "solveFor x"],Relate=[],Where=[],With=[]})]) : mout
1023 Die tactic {\tt Refine\_Problem} wandelt alle matches wieder in problem types um und sucht in der problem hierachy weiter.
1026 \section{The phase of solving}
1027 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}:
1028 {\footnotesize\begin{verbatim}
1030 val it = ("Apply_Method",Apply_Method ("SqRoot.thy","norm_univar_equation"))
1033 ML> val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1035 Form' (FormKF (~1,EdUndef,1,Nundef,"(x + #1) * (x + #2) = x ^^^ #2 + #8"))
1038 ("rnorm_equation_add","~ ?b =!= #0 ==> (?a = ?b) = (?a + #-1 * ?b = #0)"))
1040 ML> val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1042 Form' (FormKF (~1,EdUndef,1,Nundef,
1043 "(x + #1) * (x + #2) + #-1 * (x ^^^ #2 + #8) = #0")) : mout
1044 val nxt = ("Rewrite_Set",Rewrite_Set "SqRoot_simplify") : string * mstep
1046 ML> val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1047 val f = Form' (FormKF (~1,EdUndef,1,Nundef,"#-6 + #3 * x = #0")) : mout
1048 val nxt = ("Subproblem",Subproblem ("SqRoot.thy",[#,#])) : string * mstep
1050 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:
1051 {\footnotesize\begin{verbatim}
1053 val it = ("Subproblem",Subproblem ("SqRoot.thy",["univariate","equation"]))
1055 ML> val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1058 (~1,EdUndef,1,Nundef,"Subproblem (SqRoot.thy, [univariate, equation])"))
1060 val nxt = ("Refine_Tacitly",Refine_Tacitly ["univariate","equation"])
1062 ML> val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1063 val nxt = ("Model_Problem",Model_Problem ["linear","univariate","equation"])
1065 {\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.
1066 Nun folgt erneut die phase of modeling und die phase of specification.
1068 \section{The final phase: \"Uberpr\"ufung der ''post-condition``}
1069 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.
1070 Dadurch wird die post-condition im folgenden Beispiel als problem und subproblem erw\"ahnt.
1071 {\footnotesize\begin{verbatim}
1073 val it = ("Check_Postcond",Check_Postcond ["linear","univariate","equation"])
1075 ML> val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1076 val f = Form' (FormKF (~1,EdUndef,1,Nundef,"[x = #2]")) : mout
1078 ("Check_Postcond",Check_Postcond ["normalize","univariate","equation"])
1080 ML> val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1081 val f = Form' (FormKF (~1,EdUndef,0,Nundef,"[x = #2]")) : mout
1082 val nxt = ("End_Proof'",End_Proof') : string * mstep
1084 Die tactic {\tt End\_Proof'} bedeutet, dass der proof erflogreich beendet wurde.\\
1086 \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.
1089 \part{Handbuch f\"ur Autoren}
1091 \chapter{Die Struktur des Grundlagenwissens}
1093 \section{''tactics`` und Daten}
1094 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.
1095 Diese Teile sind in alphabetischer Anordnung in Tab.\ref{kb-items} auf Seite \pageref{kb-items} aufgelistet.
1098 \caption{Kleinste Teilchen des KB} \label{kb-items}
1101 \def\arraystretch{1.0}
1102 \begin{tabular}{lp{9.0cm}}
1103 Abk\"urzung & Beschreibung \\
1107 & gesammelte Liste von allen ausgewerteten Funktionen\\
1109 & ausgewertete Funktionen f\"ur Zahlen und f\"ur Eigenschaften, die in SML kodiert sind\\
1111 & rule set {\it rls} f\"ur einfache Ausdr\"ucke mit {\it eval\_fn}s\\
1113 & Formalisierung, d.h. eine sehr geringe Darstellung von einem Beispiel \\
1115 & eine method d.h. eine Datenstruktur, die alle Informationen zum L\"osen einer phase enth\"alt ({\it rew\_ord}, {\it scr}, etc.)\\
1117 & bezieht sich auf {\it met}\\
1119 & ein Operator, der der Schl\"ussel zu {\it eval\_fn} in einer {\it calc\_list} ist \\
1121 & Problem d.h. der Knotenpunkt in der problem hierachy\\
1123 & bezieht sich auf {\it pbl}\\
1125 & Anordnung beim Rewriting\\
1127 & rule set, d.h. eine Datenstruktur, die theorems {\it thm} und Operatoren {\it op} zur Vereinfachung (mit {\it rew\_ord}) enth\"alt \\
1129 & rule set f\"ur das 'reverse rewriting' (eine \isac-Technik, die schrittweise Rewriting entwickelt, z.B. f\"ur die zur\"uckgenommenen Teile)\\
1131 & script, das die Algorithmen durch Anwenden von tactics beschreibt und ein Teil von {\it met} ist \\
1133 & spezielles Regelwerk zum Berechnen von Normalformen, im Zusammenhang mit {\it thy}\\
1135 & Spezifikation, z.B, ein Tripel ({\it thyID, pblID, metID})\\
1137 & Ersatz, z.B. eine Liste von Variablen und ihren jeweiligen Werten\\
1139 & Term von Isabelle, z.B. eine Formel\\
1145 & im Bezug auf {\it thy} \\
1146 \end{tabular}\end{center}\end{table}}
1148 Die Verbindung zwischen tactics und Daten werden in Tab.\ref{tac-kb} auf Seite \pageref{tac-kb} dargestellt.
1152 \caption{Welche tactics verwenden die Teile des KB~?} \label{tac-kb}
1155 \begin{tabular}{|ll||cccc|ccc|cccc|} \hline
1156 tactic &Eingabe & & & &norm\_& &rew\_&rls &eval\_&eval\_&calc\_& \\
1157 & &thy &scr &Rrls&rls &thm &ord &Rrls&fn &rls &list &dsc\\
1160 &fmz & x & & & x & & & & & & & x \\
1161 &spec & & & & & & & & & & & \\
1163 \multicolumn{13}{|l|}{model phase}\\
1166 &Term & x & & & x & & & & & & & x \\
1167 FormFK &model & x & & & x & & & & & & & x \\
1169 \multicolumn{13}{|l|}{specify phase}\\
1172 &thyID & x & & & x & & & & x & x & & x \\
1174 &pblID & x & & & x & & & & x & x & & x \\
1176 &pblID & x & & & x & & & & x & x & & x \\
1178 &metID & x & & & x & & & & x & x & & x \\
1180 &metID & x & x & & x & & & & x & x & & x \\
1182 \multicolumn{13}{|l|}{solve phase}\\
1185 &thm & x & x & & & x &met & & x &met & & \\
1187 &thm & x & x & & & x &rls & & x &rls & & \\
1189 &thm & x & x & & & x &Rrls & & x &Rrls & & \\
1191 &rls & x & x & & & & & x & x & x & & \\
1193 &op & x & x & & & & & & & & x & \\
1195 &subs & x & & & x & & & & & & & \\
1196 & & & & & & & & & & & & \\
1198 &spec & x & x & & x & & & & x & x & & x \\
1199 &fmz & & & & & & & & & & & \\
1201 \end{tabular}\end{center}\end{table}
1204 \section{Die theories von \isac{}}
1205 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}.
1206 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.
1207 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.
1208 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.
1211 \caption{theory von der ersten Version von \isac} \label{theories}
1214 \def\arraystretch{1.0}
1215 \begin{tabular}{lp{9.0cm}}
1216 theory & Beschreibung \\
1220 & ordnet die Bezeichnungen den Funktionen, die in {\tt Isabelle2002/src/HOL/List.thy} sind, zu und (intermediatly~?) definiert einige weitere Listen von Funktionen\\
1222 & {\tt eval\_fn} f\"ur die zus\"atzliche Listen von Funktionen\\
1224 & Funktion, die f\"ur die Auswertung von Skripten ben\"otigt wird\\
1226 & bezieht sich auf {\tt eval\_fn}s\\
1228 & Vorraussetzung f\"ur script: types, tactics, tacticals\\
1230 & eine Reihe von tactics und Funktionen f\"ur den internen Gebrauch\\
1235 & fortgeschrittener Austritt, um den type Fehlern zu entkommen\\
1237 & {\it Beschreibungen} f\"ur die Formeln von {\it Modellen} und {\it Problemen}\\
1239 & Neudefinierung von Operatoren; allgemeine Eigenschaften und Funktionen f\"ur Vorraussetzungen; theorems f\"ur {\tt eval\_rls}\\
1241 & Gleitkommerzahlendarstellung\\
1243 & grunds\"atzliche Vorstellung f\"ur Gleichungen und Gleichungssysteme\\
1247 & polynomiale Gleichungen und Gleichungssysteme \\
1249 & zus\"atzliche theorems f\"ur Rationale Zahlen\\
1251 & abbrechen, hinzuf\"ugen und vereinfachen von Rationalen Zahlen durch Verwenden von (einer allgemeineren Form von) Euclids Algorithmus; die entsprechenden umgekehrten Regels\"atze\\
1253 & Gleichung mit rationalen Zahlen\\
1255 & Radikanten; berechnen der Normalform; das betreffende umgekehrte Regelwerk\\
1257 & Gleichungen mit Wurzeln\\
1259 & Gleichungen mit rationalen Zahlen und Wurzeln (z.B. mit Termen, die beide Vorg\"ange enthalten)\\
1261 & Vektoren Analysis\\
1265 & Logarithmus und Exponentialfunktionen\\
1267 & nicht der Norm entsprechende Analysis\\
1271 & Anwendungen beim Differenzieren (Maximum-Minimum-Probleme)\\
1273 & (alte) Daten f\"ur Testfolgen\\
1275 & enth\"alt alle Theorien von\isac{}\\
1276 \end{tabular}\end{center}\end{table}}
1279 \section{Daten in {\tt *.thy} und {\tt *.ML}}
1280 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
1281 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.
1284 \caption{Daten in {\tt *.thy}- und {\tt *.ML}-files} \label{thy-ML}
1287 \def\arraystretch{1.0}
1288 \begin{tabular}{llp{7.7cm}}
1289 Datei & Daten & Beschreibung \\
1294 & Operatoren, Eigenschaften, Funktionen und Skriptnamen ('{\tt Skript} Name \dots{\tt Argumente}')
1297 & theorems: \isac{} verwendet theorems von Isabelle, wenn m\"oglich; zus\"atzliche theorems, die jenen von Isabelle entsprechen, bekommen ein {\it I} angeh\"angt
1302 abgegrenzt ist von der {\tt *.thy}-Datei, wird durch \isac{} zug\"anglich gemacht
1305 & 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
1308 & 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}
1310 & {\tt norm\_rls :=}
1311 & der automatisierte Vereinfacher {\tt *\_simplify} wird so aufgehoben, dass er \"uber \isac{} zug\"anglich ist
1313 & {\tt rew\_ord' :=}
1314 & das Gleiche f\"ur die Anordnung des Rewriting, wenn es ausserhalb eines speziellen Regelwerks gebraucht wird
1317 & dasselbe wie f\"ur Regels\"atze (gew\"ohnliche Regels\"atze, umgekehrte Regels\"atze, und {\tt eval\_rls})
1319 & {\tt calc\_list :=}
1320 & 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)
1323 & Problems, die in {\tt *.ML}-Dateien definiert sind, werden zug\"anglich f\"ur \isac{}
1326 & methods, die in {\tt *.ML}-Dateien definiert sind werden zug\"anglich f\"ur \isac{}
1328 \end{tabular}\end{center}\end{table}}
1330 \section{Formale Beschreibung der Hierarchie von Problemen}
1332 \section{Skripttaktiken}
1333 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.
1337 \part{Authoring on the knowledge}
1340 \section{Add a theorem}
1341 \section{Define and add a problem}
1342 \section{Define and add a predicate}
1343 \section{Define and add a method}
1352 \bibliography{bib/isac,bib/from-theses}