|
1 \documentclass[11pt,a4paper,headline,headcount,towside,nocenter]{report} |
|
2 \usepackage{latexsym} |
|
3 |
|
4 %\usepackage{ngerman} |
|
5 %\grmn@dq@error ...and \dq \string #1 is undefined} |
|
6 %l.989 ...tch the problem type \\{\tt["squareroot", |
|
7 % "univ |
|
8 \bibliographystyle{alpha} |
|
9 |
|
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}$}} |
|
12 |
|
13 \title{\isac \\ |
|
14 Experimente zur Computermathematik\\[1.0ex] |
|
15 und\\[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]} |
|
20 \date{\today} |
|
21 |
|
22 \begin{document} |
|
23 \maketitle |
|
24 \newpage |
|
25 \tableofcontents |
|
26 \newpage |
|
27 \listoftables |
|
28 \newpage |
|
29 |
|
30 \chapter{Einleitung} |
|
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. |
|
32 |
|
33 Diese Version zeichnet sich dadurch aus, dass sie von ``Nicht-Computer-Freaks'' f\"ur ``Nicht-Computer-Freaks'' geschrieben wurde. |
|
34 |
|
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. |
|
40 |
|
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. |
|
42 |
|
43 Das Dokument ist eigenst\"andig; Basiswissen \"uber SML (f\"ur eine Einf\"uhrung siehe \cite{Paulson:91}), Terme und Umschreibung wird vorrausgesetzt. |
|
44 |
|
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. |
|
46 |
|
47 Hinweis: SML Code, Verzeichnis, Dateien sind {\tt in 'tt' geschrieben}; besonders in {\tt ML>} ist das Kerngebiet schnell. |
|
48 |
|
49 \paragraph{Versuchen Sie es!} Ein weiteres Anliegen dieses Textes ist, dem Leser Tipps f\"ur Versuche mit den Anwendungen zu geben. |
|
50 |
|
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: |
|
53 \begin{itemize} |
|
54 \item System starten |
|
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. |
|
59 |
|
60 \end{itemize} |
|
61 |
|
62 \part{Experimentelle Ann\"aherung} |
|
63 |
|
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. |
|
66 |
|
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} |
|
70 > "a + b * 3"; |
|
71 val it = "a + b * 3" : string |
|
72 \end{verbatim}} |
|
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"; |
|
76 val it = |
|
77 Const ("op +", "[RealDef.real, RealDef.real] => RealDef.real") $ |
|
78 Free ("a", "RealDef.real") $ |
|
79 (Const ("op *", "[RealDef.real, RealDef.real] => RealDef.real") $ ... $ |
|
80 ...) : Term.term |
|
81 \end{verbatim}} |
|
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"; |
|
85 val t = |
|
86 Const ("op +", "[RealDef.real, RealDef.real] => RealDef.real") $ |
|
87 Free ("a", "RealDef.real") $ |
|
88 (Const ("op *", "[RealDef.real, RealDef.real] => RealDef.real") $ ... $ |
|
89 ...) : Term.term |
|
90 \end{verbatim}} |
|
91 Von dieser Variablen {\tt t} kann man den Wert jederzeit abrufen: |
|
92 {\footnotesize\begin{verbatim} |
|
93 > t; |
|
94 val it = |
|
95 Const ("op +", "[RealDef.real, RealDef.real] => RealDef.real") $ |
|
96 Free ("a", "RealDef.real") $ |
|
97 (Const ("op *", "[RealDef.real, RealDef.real] => RealDef.real") $ ... $ |
|
98 ...) : Term.term |
|
99 \end{verbatim}} |
|
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} |
|
102 > atomty term; |
|
103 |
|
104 *** |
|
105 *** Const (op +, [real, real] => real) |
|
106 *** . Free (a, real) |
|
107 *** . Const (op *, [real, real] => real) |
|
108 *** . . Free (b, real) |
|
109 *** . . Free (3, real) |
|
110 *** |
|
111 |
|
112 val it = () : unit |
|
113 \end{verbatim}} |
|
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. |
|
116 |
|
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} |
|
121 > Isac.thy; |
|
122 val it = |
|
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 |
|
136 \end{verbatim}} |
|
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} |
|
140 class plus = |
|
141 fixes plus :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "+" 65) |
|
142 |
|
143 class minus = |
|
144 fixes minus :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "-" 65) |
|
145 |
|
146 class uminus = |
|
147 fixes uminus :: "'a \<Rightarrow> 'a" ("- _" [81] 80) |
|
148 |
|
149 class times = |
|
150 fixes times :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "*" 70) |
|
151 \end{verbatim}} |
|
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. |
|
154 |
|
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 |
|
156 |
|
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 |
|
161 \end{verbatim}} |
|
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 |
|
166 \end{verbatim}} |
|
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 |
|
171 \end{verbatim}} |
|
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" "..." |
|
187 *** "\\" "(" |
|
188 val it = None : Thm.cterm Library.option |
|
189 \end{verbatim}} |
|
190 |
|
191 Das mathematische Wissen w\"achst mit jeder Theorie von ProtoPure bis Isac. In den folgenden Beispielen wird gezeigt, wie das Wissen w\"achst. |
|
192 |
|
193 {\footnotesize\begin{verbatim} |
|
194 > (*-1-*); |
|
195 > parse HOL.thy "2^^^3"; |
|
196 *** Inner lexical error at: "^^^3" |
|
197 val it = None : Thm.cterm Library.option |
|
198 \end{verbatim}} |
|
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}. |
|
200 |
|
201 {\footnotesize\begin{verbatim} |
|
202 > (*-2-*); |
|
203 > parse HOL.thy "d_d x (a + x)"; |
|
204 val it = None : Thm.cterm Library.option |
|
205 \end{verbatim}} |
|
206 Hier wiederum ist noch kein Wissen \"uber das Differenzieren vorhanden. |
|
207 |
|
208 {\footnotesize\begin{verbatim} |
|
209 > (*-3-*); |
|
210 > parse Rational.thy "2^^^3"; |
|
211 val it = Some "2 ^^^ 3" : Thm.cterm Library.option |
|
212 \end{verbatim}} |
|
213 |
|
214 {\footnotesize\begin{verbatim} |
|
215 > (*-4-*); |
|
216 > val Some t4 = parse Rational.thy "d_d x (a + x)"; |
|
217 val t4 = "d_d x (a + x)" : Thm.cterm |
|
218 \end{verbatim}} |
|
219 |
|
220 {\footnotesize\begin{verbatim} |
|
221 > (*-5-*); |
|
222 > val Some t5 = parse Diff.thy "d_d x (a + x)"; |
|
223 val t5 = "d_d x (a + x)" : Thm.cterm |
|
224 \end{verbatim}} |
|
225 Die letzen drei Aufgaben k\"onnen schon gel\"ost werden, da {\tt Rational.thy} \"uber das n\"otige Wissen verf\"ugt. |
|
226 |
|
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} |
|
230 > term_of; |
|
231 val it = fn : Thm.cterm -> Term.term |
|
232 \end{verbatim}} |
|
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} |
|
235 > term_of t4; |
|
236 val it = |
|
237 Free ("d_d", "[RealDef.real, RealDef.real] => RealDef.real") $ ... $ |
|
238 ...: Term.term |
|
239 |
|
240 \end{verbatim}} |
|
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} |
|
243 > term_of t5; |
|
244 val it = |
|
245 Const ("Diff.d_d", "[RealDef.real, RealDef.real] => RealDef.real") $ ... $ |
|
246 ... : Term.term |
|
247 \end{verbatim}} |
|
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} |
|
250 > print_depth; |
|
251 val it = fn : int -> unit |
|
252 \end{verbatim}} |
|
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} |
|
255 > print_depth 10; |
|
256 val it = () : unit |
|
257 > term_of t4; |
|
258 val it = |
|
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")) |
|
263 : Term.term |
|
264 |
|
265 > print_depth 10; |
|
266 val it = () : unit |
|
267 > term_of t5; |
|
268 val it = |
|
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")) |
|
273 : Term.term |
|
274 \end{verbatim}} |
|
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; |
|
279 val 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} |
|
290 : Theory.theory |
|
291 > ((atomty) o term_of o the o (parse thy)) "d_d x (a + x)"; |
|
292 |
|
293 *** |
|
294 *** Free (d_d, [real, real] => real) |
|
295 *** . Free (x, real) |
|
296 *** . Const (op +, [real, real] => real) |
|
297 *** . . Free (a, real) |
|
298 *** . . Free (x, real) |
|
299 *** |
|
300 |
|
301 val it = () : unit |
|
302 |
|
303 |
|
304 > (*-5-*) val thy = Diff.thy; |
|
305 val 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 |
|
318 |
|
319 > ((atomty) o term_of o the o (parse thy)) "d_d x (a + x)"; |
|
320 |
|
321 *** |
|
322 *** Const (Diff.d_d, [real, real] => real) |
|
323 *** . Free (x, real) |
|
324 *** . Const (op +, [real, real] => real) |
|
325 *** . . Free (a, real) |
|
326 *** . . Free (x, real) |
|
327 *** |
|
328 |
|
329 val it = () : unit |
|
330 \end{verbatim}} |
|
331 |
|
332 |
|
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} |
|
337 > rewrite; |
|
338 val it = fn |
|
339 : |
|
340 theory' -> |
|
341 rew_ord' -> |
|
342 rls' -> bool -> thm' -> cterm' -> (string * string list) Library.option |
|
343 \end{verbatim}} |
|
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} |
|
346 > rewrite_inst; |
|
347 val it = fn |
|
348 : |
|
349 theory' -> |
|
350 rew_ord' -> |
|
351 rls' ->bool -> 'a -> thm' -> cterm' -> (cterm' * cterm' list) Library.option |
|
352 \end{verbatim}} |
|
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 |
|
368 \end{verbatim}} |
|
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 |
|
384 \end{verbatim}} |
|
385 Was {\tt rewrite\_set} genau macht, finden Sie im n\"achsten Kapitel. |
|
386 |
|
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; |
|
391 \end{verbatim}} |
|
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}}. |
|
393 |
|
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:\\ |
|
398 \tabcolsep=4mm |
|
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 \\ |
|
407 \end{tabular}\\ |
|
408 |
|
409 {\footnotesize\begin{verbatim} |
|
410 > rewrite_set; |
|
411 val it = fn : theory' -> bool -> rls' -> ... |
|
412 \end{verbatim}} |
|
413 {\footnotesize\begin{verbatim} |
|
414 > rewrite_set_inst; |
|
415 val it = fn : theory' -> bool -> subs' -> . |
|
416 \end{verbatim}} |
|
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; |
|
420 val it = () : unit |
|
421 \end{verbatim}} |
|
422 |
|
423 |
|
424 \section{Rule sets} |
|
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} |
|
429 ??????????? |
|
430 \end{verbatim}} |
|
431 |
|
432 {\footnotesize\begin{verbatim} |
|
433 > sym; |
|
434 val it = "?s = ?t ==> ?t = ?s" : Thm.thm |
|
435 > rearrange_assoc; |
|
436 val it = |
|
437 Rls |
|
438 {id = "rearrange_assoc", |
|
439 scr = Script (Free ("empty_script", "RealDef.real")), |
|
440 calc = [], |
|
441 erls = |
|
442 Rls |
|
443 {id = "e_rls", |
|
444 scr = EmptyScr, |
|
445 calc = [], |
|
446 erls = Erls, |
|
447 srls = Erls, |
|
448 rules = [], |
|
449 rew_ord = ("dummy_ord", fn), |
|
450 preconds = []}, |
|
451 srls = |
|
452 Rls |
|
453 {id = "e_rls", |
|
454 scr = EmptyScr, |
|
455 calc = [], |
|
456 erls = Erls, |
|
457 srls = Erls, |
|
458 rules = [], |
|
459 rew_ord = ("dummy_ord", fn), |
|
460 preconds = []}, |
|
461 rules = |
|
462 [Thm ("sym_radd_assoc", "?m1 + (?n1 + ?k1) = ?m1 + ?n1 + ?k1" [.]), |
|
463 Thm |
|
464 ("sym_rmult_assoc", |
|
465 "?m1 * (?n1 * ?k1) = ?m1 * ?n1 * ?k1" [.])], |
|
466 rew_ord = ("e_rew_ord", fn), |
|
467 preconds = []} : rls |
|
468 \end{verbatim}} |
|
469 |
|
470 |
|
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} |
|
474 > calculate; |
|
475 val it = fn |
|
476 : |
|
477 theory' -> |
|
478 string * |
|
479 ( |
|
480 string -> |
|
481 Term.term -> Theory.theory -> (string * Term.term) Library.option) -> |
|
482 cterm' -> (string * thm') Library.option |
|
483 |
|
484 > calculate_; |
|
485 val it = fn |
|
486 : |
|
487 Theory.theory -> |
|
488 string * |
|
489 ( |
|
490 string -> |
|
491 Term.term -> Theory.theory -> (string * Term.term) Library.option) -> |
|
492 Term.term -> (Term.term * (string * Thm.thm)) Library.option |
|
493 \end{verbatim}} |
|
494 Man bekommt das Ergebnis und das theorem bezieht sich darauf. Daher sind die folgenden mathematischen Rechnungen m\"oglich: |
|
495 {\footnotesize\begin{verbatim} |
|
496 > calclist; |
|
497 val it = |
|
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))] |
|
506 : |
|
507 ( |
|
508 string * |
|
509 ( |
|
510 string * |
|
511 ( |
|
512 string -> |
|
513 Term.term -> Theory.theory -> (string * Term.term) Library.option))) list |
|
514 \end{verbatim}} |
|
515 |
|
516 |
|
517 |
|
518 |
|
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. |
|
521 |
|
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: |
|
524 |
|
525 {\footnotesize\begin{verbatim} |
|
526 > sqrt_right; |
|
527 val it = fn : bool -> Theory.theory -> subst -> Term.term * Term.term -> b ool |
|
528 > tless_true; |
|
529 val it = fn : subst -> Term.term * Term.term -> bool |
|
530 \end{verbatim}} |
|
531 |
|
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. |
|
533 |
|
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. |
|
536 |
|
537 |
|
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} |
|
542 > matches; |
|
543 val it = fn : Theory.theory -> Term.term -> Term.term -> bool |
|
544 \end{verbatim}} |
|
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"; |
|
548 val t = |
|
549 Const ("op =", "[RealDef.real, RealDef.real] => bool") $ |
|
550 (Const ("op *", "[RealDef.real, RealDef.real] => RealDef.real") $ |
|
551 Free ("3", "RealDef.real") $ |
|
552 (Const |
|
553 ("Atools.pow", |
|
554 "[RealDef.real, RealDef.real] => RealDef.real") $ |
|
555 Free ("x", "RealDef.real") $ Free ("2", " RealDef.real"))) $ |
|
556 Free ("1", "RealDef.real") : Term.term |
|
557 \end{verbatim}} |
|
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"; |
|
561 val p = |
|
562 Const ("op =", "[RealDef.real, RealDef.real] => bool") $ |
|
563 (Const ("op *", "[RealDef.real, RealDef.real] => RealDef.real") $ |
|
564 Free ("a", "RealDef.real") $ |
|
565 (Const |
|
566 ("Atools.pow", |
|
567 "[RealDef.real, RealDef.real] => RealDef.real") $ |
|
568 Free ("b", "RealDef.real") $ Free ("2", "RealDef.real"))) $ |
|
569 Free ("c", "RealDef.real") : Term.term |
|
570 \end{verbatim}} |
|
571 Dieses Modell enth\"alt sogenannte \textit{scheme variables}. |
|
572 {\footnotesize\begin{verbatim} |
|
573 > atomt p; |
|
574 "*** -------------" |
|
575 "*** Const (op =)" |
|
576 "*** . Const (op *)""*** . . Free (a, )" |
|
577 "*** . . Const (Atools.pow)" |
|
578 "*** . . . Free (b, )" |
|
579 "*** . . . Free (2, )" |
|
580 "*** . Free (c, )" |
|
581 "\n" |
|
582 val it = "\n" : string |
|
583 \end{verbatim}} |
|
584 Das Modell wird durch den Befehl \textit{free2var} erstellt. |
|
585 {\footnotesize\begin{verbatim} |
|
586 > free2var; |
|
587 val it = fn : Term.term -> Term.term |
|
588 > val pat = free2var p; |
|
589 val pat = |
|
590 Const ("op =", "[RealDef.real, RealDef.real] => bool") $ |
|
591 (Const ("op *", "[RealDef.real, RealDef.real] => RealDef.real") $ |
|
592 Var (("a", 0), "RealDef.real") $ |
|
593 (Const |
|
594 ("Atools.pow", |
|
595 "[RealDef.real, RealDef.real] => RealDef.real") $ |
|
596 Var (("b", 0), "RealDef.real") $ |
|
597 Free ("2", "RealDef.real"))) $ Var (("c", 0), "RealDef.real") |
|
598 : Term.term |
|
599 > Sign.string_of_term (sign_of thy) pat; |
|
600 val it = "?a * ?b ^^^ 2 = ?c" : string |
|
601 \end{verbatim}} |
|
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} |
|
604 > atomt pat; |
|
605 "*** -------------" |
|
606 "*** Const (op =)" |
|
607 "*** . Const (op *)" |
|
608 "*** . . Var ((a, 0), )" |
|
609 "*** . . Const (Atools.pow)" |
|
610 "*** . . . Var ((b, 0), )" |
|
611 "*** . . . Free (2, )" |
|
612 "*** . Var ((c, 0), )" |
|
613 "\n" |
|
614 val it = "\n" : string |
|
615 \end{verbatim}} |
|
616 Jetzt kann das Matching an den beiden vorigen Terme angewendet werden. |
|
617 {\footnotesize\begin{verbatim} |
|
618 > matches thy t pat; |
|
619 val it = true : bool |
|
620 > val t2 = (term_of o the o (parse thy)) "x^^^2 = 1"; |
|
621 val t2 = |
|
622 Const ("op =", "[RealDef.real, RealDef.real] => bool") $ |
|
623 (Const |
|
624 ("Atools.pow", |
|
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"; |
|
631 val pat2 = |
|
632 Const ("op =", "[RealDef.real, RealDef.real] => bool") $ |
|
633 (Const |
|
634 ("Atools.pow", |
|
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; |
|
639 val it = true : bool |
|
640 \end{verbatim}} |
|
641 |
|
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} |
|
645 > show_ptyps; |
|
646 val it = fn : unit -> unit |
|
647 > show_ptyps(); |
|
648 [ |
|
649 ["e_pblID"], |
|
650 ["simplification", "polynomial"], |
|
651 ["simplification", "rational"], |
|
652 ["vereinfachen", "polynom", "plus_minus"], |
|
653 ["vereinfachen", "polynom", "klammer"], |
|
654 ["vereinfachen", "polynom", "binom_klammer"], |
|
655 ["probe", "polynom"], |
|
656 ["probe", "bruch"], |
|
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"], |
|
684 ["Biegelinien", " |
|
685 MomentBestimmte"], |
|
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"] |
|
699 ] |
|
700 val it = () : unit |
|
701 \end{verbatim}} |
|
702 |
|
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. |
|
705 |
|
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} |
|
709 > refine; |
|
710 val it = fn : fmz_ -> pblID -> SpecifyTools.match list |
|
711 > val fmz = ["equality (sqrt(9 + 4 * x)=sqrt x |
|
712 + sqrt (5 + x))", |
|
713 # "soleFor x","errorBound (eps=0)", |
|
714 # "solutions L"]; |
|
715 val fmz = |
|
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 |
|
722 \end{verbatim}} |
|
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)", |
|
727 # "solutions L"]; |
|
728 val fmz = ["equality (x + 1 = 2)", "solveFor x", "errorBound (eps=0)", ...] |
|
729 : string list |
|
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"] |
|
742 val it = |
|
743 [Matches |
|
744 (["univariate", "equation"], |
|
745 {Find = [Correct "solutions L"], With = [...], ...}), |
|
746 NoMatch (["linear", "univariate", ...], {Find = [...], ...}), |
|
747 NoMatch (["root", ...], ...), ...] : SpecifyTools.match list |
|
748 \end{verbatim}} |
|
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). |
|
750 |
|
751 |
|
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: |
|
757 \begin{tabbing} |
|
758 123\=123\=expr ::=\=$|\;\;$\=\kill |
|
759 \>script ::= {\tt Script} id arg$\,^*$ = body\\ |
|
760 \>\>arg ::= id $\;|\;\;($ ( id :: type ) $)$\\ |
|
761 \>\>body ::= expr\\ |
|
762 \>\>expr ::= \>\>{\tt let} id = expr $($ ; id = expr$)^*$ {\tt in} expr\\ |
|
763 \>\>\>$|\;$\>{\tt if} prop {\tt then} expr {\tt else} expr\\ |
|
764 \>\>\>$|\;$\>listexpr\\ |
|
765 \>\>\>$|\;$\>id\\ |
|
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 $)^*$\\ |
|
773 \>\>type ::= id\\ |
|
774 \>\>tac ::= id |
|
775 \end{tabbing} |
|
776 |
|
777 \section{\"Uberpr\"ufung der Auswertung} |
|
778 Das Kontrollsystem arbeitet mit den folgenden Script-Ausdr\"ucken, die {\it tacticals} genannt werden: |
|
779 \begin{description} |
|
780 \item{{\tt while} prop {\tt Do} expr id} |
|
781 \item{{\tt if} prop {\tt then} expr {\tt else} expr} |
|
782 \end{description} |
|
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: |
|
784 \begin{description} |
|
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} |
|
789 \item xxx |
|
790 \end{description} |
|
791 |
|
792 |
|
793 |
|
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. |
|
818 |
|
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 ?????????????????????????????????????????????????????????????????????????????????? |
|
824 |
|
825 ML> val fmz = ["equality ((x+#1)*(x+#2)=x^^^#2+#8)","solveFor x", |
|
826 "errorBound (eps=#0)","solutions L"]; |
|
827 val fmz = |
|
828 ["equality ((x+#1)*(x+#2)=x^^^#2+#8)","solveFor x","errorBound (eps=#0)", |
|
829 "solutions L"] : string list |
|
830 ML> |
|
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 |
|
836 \end{verbatim}} |
|
837 |
|
838 \section{Der Beginn einer Rechnung} |
|
839 |
|
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 |
|
845 val m = |
|
846 Init_Proof |
|
847 (["equality ((x+#1)*(x+#2)=x^^^#2+#8)","solveFor x","errorBound (eps=#0)", |
|
848 "solutions L"],("SqRoot.thy",[#,#],(#,#))) : mstep |
|
849 ML> |
|
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"]) |
|
854 : string * mstep |
|
855 val pt = |
|
856 Nd |
|
857 (PblObj |
|
858 {branch=#,cell=#,env=#,loc=#,meth=#,model=#,origin=#,ostate=#,probl=#, |
|
859 result=#,spec=#},[]) : ptree |
|
860 \end{verbatim}} |
|
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*) |
|
865 val it = () : unit |
|
866 ML> |
|
867 ML> f; |
|
868 val it = |
|
869 Form' |
|
870 (PpcKF |
|
871 (0,EdUndef,0,Nundef, |
|
872 (Problem [], |
|
873 {Find=[Incompl "solutions []"], |
|
874 Given=[Incompl "equality",Incompl "solveFor"],Relate=[], |
|
875 Where=[False "matches (?a = ?b) e_"],With=[]}))) : mout |
|
876 \end{verbatim}} |
|
877 {\footnotesize\begin{verbatim} |
|
878 ????????????????????????????????????????????????????????????????????????????????????????????? |
|
879 ML> nxt; |
|
880 val it = ("Refine_Tacitly",Refine_Tacitly ["univariate","equation"]) |
|
881 : string * mstep |
|
882 ML> |
|
883 ML> val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
|
884 val nxt = ("Model_Problem",Model_Problem ["normalize","univariate","equation"]) |
|
885 : string * mstep |
|
886 ML> |
|
887 ML> val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
|
888 \end{verbatim}} |
|
889 |
|
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 ????????????????????????????????????????????????????????????????????????????????????????????? |
|
894 ML> nxt; |
|
895 val it = |
|
896 ("Add_Given",Add_Given "equality ((x + #1) * (x + #2) = x ^^^ #2 + #8)") |
|
897 : string * mstep |
|
898 ML> |
|
899 ML> val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
|
900 val nxt = ("Add_Given",Add_Given "solveFor x") : string * mstep |
|
901 ML> |
|
902 ML> val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
|
903 val nxt = ("Add_Find",Add_Find "solutions L") : string * mstep |
|
904 ML> |
|
905 ML> val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
|
906 val f = Form' (PpcKF (0,EdUndef,0,Nundef,(#,#))) : mout |
|
907 \end{verbatim}} |
|
908 {\footnotesize\begin{verbatim} |
|
909 ????????????????????????????????????????????????????????????????????????????????????????????? |
|
910 ML> Compiler.Control.Print.printDepth:=8; |
|
911 ML> f; |
|
912 val it = |
|
913 Form' |
|
914 (PpcKF |
|
915 (0,EdUndef,0,Nundef, |
|
916 (Problem [], |
|
917 {Find=[Correct "solutions L"], |
|
918 Given=[Correct "equality ((x + #1) * (x + #2) = x ^^^ #2 + #8)", |
|
919 Correct "solveFor x"],Relate=[],Where=[],With=[]}))) : mout |
|
920 \end{verbatim}} |
|
921 |
|
922 |
|
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 ?????????????????????????????????????????????????????????????????????????????????????????? |
|
927 ML> nxt; |
|
928 val it = ("Specify_Domain",Specify_Domain "SqRoot.thy") : string * mstep |
|
929 ML> |
|
930 ML> val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
|
931 val nxt = |
|
932 ("Specify_Problem",Specify_Problem ["normalize","univariate","equation"]) |
|
933 : string * mstep |
|
934 val pt = |
|
935 Nd |
|
936 (PblObj |
|
937 {branch=#,cell=#,env=#,loc=#,meth=#,model=#,origin=#,ostate=#,probl=#, |
|
938 result=#,spec=#},[]) : ptree |
|
939 \end{verbatim}} |
|
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 |
|
947 val nxt = |
|
948 ("Refine_Problem",Refine_Problem ["normalize","univariate","equation"]) |
|
949 : string * mstep |
|
950 ML> |
|
951 ML> val nxt = ("Specify_Problem", |
|
952 Specify_Problem ["linear","univariate","equation"]); |
|
953 ML> val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
|
954 val f = |
|
955 Form' |
|
956 (PpcKF |
|
957 (0,EdUndef,0,Nundef, |
|
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=[], |
|
962 Where=[False |
|
963 "matches (?a + ?b * x = #0) ((x + #1) * (x + #2) = x ^^^ #2 + #8)"], |
|
964 With=[]}))) : mout |
|
965 \end{verbatim}} |
|
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 |
|
973 ML> |
|
974 ML> Compiler.Control.Print.printDepth:=9;f;Compiler.Control.Print.printDepth:=4; |
|
975 val f = |
|
976 Problems |
|
977 (RefinedKF |
|
978 [NoMatch |
|
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=[], |
|
983 Where=[False |
|
984 "matches (?a + ?b * x = #0) ((x + #1) * (x + #2) = x ^^^ #2 + #8)"], |
|
985 With=[]})]) : mout |
|
986 ML> |
|
987 ML> val nxt = ("Refine_Problem",Refine_Problem ["univariate","equation"]); |
|
988 ML> val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
|
989 val f = |
|
990 Problems |
|
991 (RefinedKF [Matches #,NoMatch #,NoMatch #,NoMatch #,NoMatch #,Matches #]) |
|
992 : mout |
|
993 ML> |
|
994 ML> |
|
995 ML> Compiler.Control.Print.printDepth:=9;f;Compiler.Control.Print.printDepth:=4; |
|
996 val f = |
|
997 Problems |
|
998 (RefinedKF |
|
999 [Matches |
|
1000 (["univariate","equation"], |
|
1001 {Find=[Correct "solutions L"], |
|
1002 Given=[Correct "equality ((x + #1) * (x + #2) = x ^^^ #2 + #8)", |
|
1003 Correct "solveFor x"],Relate=[], |
|
1004 Where=[Correct |
|
1005 With=[]}), |
|
1006 NoMatch |
|
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=[], |
|
1011 Where=[False |
|
1012 "matches (?a + ?b * x = #0) ((x + #1) * (x + #2) = x ^^^ #2 + #8)"], |
|
1013 With=[]}), |
|
1014 NoMatch |
|
1015 ... |
|
1016 ... |
|
1017 Matches |
|
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 |
|
1022 \end{verbatim}} |
|
1023 Die tactic {\tt Refine\_Problem} wandelt alle matches wieder in problem types um und sucht in der problem hierachy weiter. |
|
1024 |
|
1025 |
|
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} |
|
1029 ML> nxt; |
|
1030 val it = ("Apply_Method",Apply_Method ("SqRoot.thy","norm_univar_equation")) |
|
1031 : string * mstep |
|
1032 ML> |
|
1033 ML> val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
|
1034 val f = |
|
1035 Form' (FormKF (~1,EdUndef,1,Nundef,"(x + #1) * (x + #2) = x ^^^ #2 + #8")) |
|
1036 val nxt = |
|
1037 ("Rewrite", Rewrite |
|
1038 ("rnorm_equation_add","~ ?b =!= #0 ==> (?a = ?b) = (?a + #-1 * ?b = #0)")) |
|
1039 ML> |
|
1040 ML> val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
|
1041 val f = |
|
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 |
|
1045 ML> |
|
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 |
|
1049 \end{verbatim}} |
|
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} |
|
1052 ML> nxt; |
|
1053 val it = ("Subproblem",Subproblem ("SqRoot.thy",["univariate","equation"])) |
|
1054 ML> |
|
1055 ML> val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
|
1056 val f = |
|
1057 Form' (FormKF |
|
1058 (~1,EdUndef,1,Nundef,"Subproblem (SqRoot.thy, [univariate, equation])")) |
|
1059 : mout |
|
1060 val nxt = ("Refine_Tacitly",Refine_Tacitly ["univariate","equation"]) |
|
1061 ML> |
|
1062 ML> val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
|
1063 val nxt = ("Model_Problem",Model_Problem ["linear","univariate","equation"]) |
|
1064 \end{verbatim}} |
|
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. |
|
1067 |
|
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} |
|
1072 ML> nxt; |
|
1073 val it = ("Check_Postcond",Check_Postcond ["linear","univariate","equation"]) |
|
1074 ML> |
|
1075 ML> val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
|
1076 val f = Form' (FormKF (~1,EdUndef,1,Nundef,"[x = #2]")) : mout |
|
1077 val nxt = |
|
1078 ("Check_Postcond",Check_Postcond ["normalize","univariate","equation"]) |
|
1079 ML> |
|
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 |
|
1083 \end{verbatim}} |
|
1084 Die tactic {\tt End\_Proof'} bedeutet, dass der proof erflogreich beendet wurde.\\ |
|
1085 |
|
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. |
|
1087 |
|
1088 |
|
1089 \part{Handbuch f\"ur Autoren} |
|
1090 |
|
1091 \chapter{Die Struktur des Grundlagenwissens} |
|
1092 |
|
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. |
|
1096 |
|
1097 {\begin{table}[h] |
|
1098 \caption{Kleinste Teilchen des KB} \label{kb-items} |
|
1099 %\tabcolsep=0.3mm |
|
1100 \begin{center} |
|
1101 \def\arraystretch{1.0} |
|
1102 \begin{tabular}{lp{9.0cm}} |
|
1103 Abk\"urzung & Beschreibung \\ |
|
1104 \hline |
|
1105 &\\ |
|
1106 {\it calc\_list} |
|
1107 & gesammelte Liste von allen ausgewerteten Funktionen\\ |
|
1108 {\it eval\_fn} |
|
1109 & ausgewertete Funktionen f\"ur Zahlen und f\"ur Eigenschaften, die in SML kodiert sind\\ |
|
1110 {\it eval\_rls } |
|
1111 & rule set {\it rls} f\"ur einfache Ausdr\"ucke mit {\it eval\_fn}s\\ |
|
1112 {\it fmz} |
|
1113 & Formalisierung, d.h. eine sehr geringe Darstellung von einem Beispiel \\ |
|
1114 {\it met} |
|
1115 & eine method d.h. eine Datenstruktur, die alle Informationen zum L\"osen einer phase enth\"alt ({\it rew\_ord}, {\it scr}, etc.)\\ |
|
1116 {\it metID} |
|
1117 & bezieht sich auf {\it met}\\ |
|
1118 {\it op} |
|
1119 & ein Operator, der der Schl\"ussel zu {\it eval\_fn} in einer {\it calc\_list} ist \\ |
|
1120 {\it pbl} |
|
1121 & Problem d.h. der Knotenpunkt in der problem hierachy\\ |
|
1122 {\it pblID} |
|
1123 & bezieht sich auf {\it pbl}\\ |
|
1124 {\it rew\_ord} |
|
1125 & Anordnung beim Rewriting\\ |
|
1126 {\it rls} |
|
1127 & rule set, d.h. eine Datenstruktur, die theorems {\it thm} und Operatoren {\it op} zur Vereinfachung (mit {\it rew\_ord}) enth\"alt \\ |
|
1128 {\it Rrls} |
|
1129 & rule set f\"ur das 'reverse rewriting' (eine \isac-Technik, die schrittweise Rewriting entwickelt, z.B. f\"ur die zur\"uckgenommenen Teile)\\ |
|
1130 {\it scr} |
|
1131 & script, das die Algorithmen durch Anwenden von tactics beschreibt und ein Teil von {\it met} ist \\ |
|
1132 {\it norm\_rls} |
|
1133 & spezielles Regelwerk zum Berechnen von Normalformen, im Zusammenhang mit {\it thy}\\ |
|
1134 {\it spec} |
|
1135 & Spezifikation, z.B, ein Tripel ({\it thyID, pblID, metID})\\ |
|
1136 {\it subs} |
|
1137 & Ersatz, z.B. eine Liste von Variablen und ihren jeweiligen Werten\\ |
|
1138 {\it Term} |
|
1139 & Term von Isabelle, z.B. eine Formel\\ |
|
1140 {\it thm} |
|
1141 & theorem\\ |
|
1142 {\it thy} |
|
1143 & theory\\ |
|
1144 {\it thyID} |
|
1145 & im Bezug auf {\it thy} \\ |
|
1146 \end{tabular}\end{center}\end{table}} |
|
1147 |
|
1148 Die Verbindung zwischen tactics und Daten werden in Tab.\ref{tac-kb} auf Seite \pageref{tac-kb} dargestellt. |
|
1149 |
|
1150 |
|
1151 \begin{table}[h] |
|
1152 \caption{Welche tactics verwenden die Teile des KB~?} \label{tac-kb} |
|
1153 \tabcolsep=0.3mm |
|
1154 \begin{center} |
|
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\\ |
|
1158 \hline\hline |
|
1159 Init\_Proof |
|
1160 &fmz & x & & & x & & & & & & & x \\ |
|
1161 &spec & & & & & & & & & & & \\ |
|
1162 \hline |
|
1163 \multicolumn{13}{|l|}{model phase}\\ |
|
1164 \hline |
|
1165 Add\_* |
|
1166 &Term & x & & & x & & & & & & & x \\ |
|
1167 FormFK &model & x & & & x & & & & & & & x \\ |
|
1168 \hline |
|
1169 \multicolumn{13}{|l|}{specify phase}\\ |
|
1170 \hline |
|
1171 Specify\_Theory |
|
1172 &thyID & x & & & x & & & & x & x & & x \\ |
|
1173 Specify\_Problem |
|
1174 &pblID & x & & & x & & & & x & x & & x \\ |
|
1175 Refine\_Problem |
|
1176 &pblID & x & & & x & & & & x & x & & x \\ |
|
1177 Specify\_Method |
|
1178 &metID & x & & & x & & & & x & x & & x \\ |
|
1179 Apply\_Method |
|
1180 &metID & x & x & & x & & & & x & x & & x \\ |
|
1181 \hline |
|
1182 \multicolumn{13}{|l|}{solve phase}\\ |
|
1183 \hline |
|
1184 Rewrite,\_Inst |
|
1185 &thm & x & x & & & x &met & & x &met & & \\ |
|
1186 Rewrite, Detail |
|
1187 &thm & x & x & & & x &rls & & x &rls & & \\ |
|
1188 Rewrite, Detail |
|
1189 &thm & x & x & & & x &Rrls & & x &Rrls & & \\ |
|
1190 Rewrite\_Set,\_Inst |
|
1191 &rls & x & x & & & & & x & x & x & & \\ |
|
1192 Calculate |
|
1193 &op & x & x & & & & & & & & x & \\ |
|
1194 Substitute |
|
1195 &subs & x & & & x & & & & & & & \\ |
|
1196 & & & & & & & & & & & & \\ |
|
1197 SubProblem |
|
1198 &spec & x & x & & x & & & & x & x & & x \\ |
|
1199 &fmz & & & & & & & & & & & \\ |
|
1200 \hline |
|
1201 \end{tabular}\end{center}\end{table} |
|
1202 |
|
1203 |
|
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. |
|
1209 |
|
1210 {\begin{table}[h] |
|
1211 \caption{theory von der ersten Version von \isac} \label{theories} |
|
1212 %\tabcolsep=0.3mm |
|
1213 \begin{center} |
|
1214 \def\arraystretch{1.0} |
|
1215 \begin{tabular}{lp{9.0cm}} |
|
1216 theory & Beschreibung \\ |
|
1217 \hline |
|
1218 &\\ |
|
1219 ListI.thy |
|
1220 & ordnet die Bezeichnungen den Funktionen, die in {\tt Isabelle2002/src/HOL/List.thy} sind, zu und (intermediatly~?) definiert einige weitere Listen von Funktionen\\ |
|
1221 ListI.ML |
|
1222 & {\tt eval\_fn} f\"ur die zus\"atzliche Listen von Funktionen\\ |
|
1223 Tools.thy |
|
1224 & Funktion, die f\"ur die Auswertung von Skripten ben\"otigt wird\\ |
|
1225 Tools.ML |
|
1226 & bezieht sich auf {\tt eval\_fn}s\\ |
|
1227 Script.thy |
|
1228 & Vorraussetzung f\"ur script: types, tactics, tacticals\\ |
|
1229 Script.ML |
|
1230 & eine Reihe von tactics und Funktionen f\"ur den internen Gebrauch\\ |
|
1231 & \\ |
|
1232 \hline |
|
1233 & \\ |
|
1234 Typefix.thy |
|
1235 & fortgeschrittener Austritt, um den type Fehlern zu entkommen\\ |
|
1236 Descript.thy |
|
1237 & {\it Beschreibungen} f\"ur die Formeln von {\it Modellen} und {\it Problemen}\\ |
|
1238 Atools |
|
1239 & Neudefinierung von Operatoren; allgemeine Eigenschaften und Funktionen f\"ur Vorraussetzungen; theorems f\"ur {\tt eval\_rls}\\ |
|
1240 Float |
|
1241 & Gleitkommerzahlendarstellung\\ |
|
1242 Equation |
|
1243 & grunds\"atzliche Vorstellung f\"ur Gleichungen und Gleichungssysteme\\ |
|
1244 Poly |
|
1245 & Polynome\\ |
|
1246 PolyEq |
|
1247 & polynomiale Gleichungen und Gleichungssysteme \\ |
|
1248 Rational.thy |
|
1249 & zus\"atzliche theorems f\"ur Rationale Zahlen\\ |
|
1250 Rational.ML |
|
1251 & abbrechen, hinzuf\"ugen und vereinfachen von Rationalen Zahlen durch Verwenden von (einer allgemeineren Form von) Euclids Algorithmus; die entsprechenden umgekehrten Regels\"atze\\ |
|
1252 RatEq |
|
1253 & Gleichung mit rationalen Zahlen\\ |
|
1254 Root |
|
1255 & Radikanten; berechnen der Normalform; das betreffende umgekehrte Regelwerk\\ |
|
1256 RootEq |
|
1257 & Gleichungen mit Wurzeln\\ |
|
1258 RatRootEq |
|
1259 & Gleichungen mit rationalen Zahlen und Wurzeln (z.B. mit Termen, die beide Vorg\"ange enthalten)\\ |
|
1260 Vect |
|
1261 & Vektoren Analysis\\ |
|
1262 Trig |
|
1263 & Trigonometrie\\ |
|
1264 LogExp |
|
1265 & Logarithmus und Exponentialfunktionen\\ |
|
1266 Calculus |
|
1267 & nicht der Norm entsprechende Analysis\\ |
|
1268 Diff |
|
1269 & Differenzierung\\ |
|
1270 DiffApp |
|
1271 & Anwendungen beim Differenzieren (Maximum-Minimum-Probleme)\\ |
|
1272 Test |
|
1273 & (alte) Daten f\"ur Testfolgen\\ |
|
1274 Isac |
|
1275 & enth\"alt alle Theorien von\isac{}\\ |
|
1276 \end{tabular}\end{center}\end{table}} |
|
1277 |
|
1278 |
|
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. |
|
1282 |
|
1283 {\begin{table}[h] |
|
1284 \caption{Daten in {\tt *.thy}- und {\tt *.ML}-files} \label{thy-ML} |
|
1285 \tabcolsep=2.0mm |
|
1286 \begin{center} |
|
1287 \def\arraystretch{1.0} |
|
1288 \begin{tabular}{llp{7.7cm}} |
|
1289 Datei & Daten & Beschreibung \\ |
|
1290 \hline |
|
1291 & &\\ |
|
1292 {\tt *.thy} |
|
1293 & consts |
|
1294 & Operatoren, Eigenschaften, Funktionen und Skriptnamen ('{\tt Skript} Name \dots{\tt Argumente}') |
|
1295 \\ |
|
1296 & rules |
|
1297 & theorems: \isac{} verwendet theorems von Isabelle, wenn m\"oglich; zus\"atzliche theorems, die jenen von Isabelle entsprechen, bekommen ein {\it I} angeh\"angt |
|
1298 \\& &\\ |
|
1299 {\tt *.ML} |
|
1300 & {\tt theory' :=} |
|
1301 & Die theory, die |
|
1302 abgegrenzt ist von der {\tt *.thy}-Datei, wird durch \isac{} zug\"anglich gemacht |
|
1303 \\ |
|
1304 & {\tt eval\_fn} |
|
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 |
|
1306 \\ |
|
1307 & {\tt *\_simplify} |
|
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} |
|
1309 \\ |
|
1310 & {\tt norm\_rls :=} |
|
1311 & der automatisierte Vereinfacher {\tt *\_simplify} wird so aufgehoben, dass er \"uber \isac{} zug\"anglich ist |
|
1312 \\ |
|
1313 & {\tt rew\_ord' :=} |
|
1314 & das Gleiche f\"ur die Anordnung des Rewriting, wenn es ausserhalb eines speziellen Regelwerks gebraucht wird |
|
1315 \\ |
|
1316 & {\tt ruleset' :=} |
|
1317 & dasselbe wie f\"ur Regels\"atze (gew\"ohnliche Regels\"atze, umgekehrte Regels\"atze, und {\tt eval\_rls}) |
|
1318 \\ |
|
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) |
|
1321 \\ |
|
1322 & {\tt store\_pbl} |
|
1323 & Problems, die in {\tt *.ML}-Dateien definiert sind, werden zug\"anglich f\"ur \isac{} |
|
1324 \\ |
|
1325 & {\tt methods :=} |
|
1326 & methods, die in {\tt *.ML}-Dateien definiert sind werden zug\"anglich f\"ur \isac{} |
|
1327 \\ |
|
1328 \end{tabular}\end{center}\end{table}} |
|
1329 |
|
1330 \section{Formale Beschreibung der Hierarchie von Problemen} |
|
1331 |
|
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. |
|
1334 |
|
1335 |
|
1336 |
|
1337 \part{Authoring on the knowledge} |
|
1338 |
|
1339 |
|
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} |
|
1344 \section{} |
|
1345 \section{} |
|
1346 \section{} |
|
1347 \section{} |
|
1348 |
|
1349 |
|
1350 |
|
1351 \newpage |
|
1352 \bibliography{bib/isac,bib/from-theses} |
|
1353 |
|
1354 \end{document} |