1.1 --- a/doc-src/isac/mat-eng-de.tex Thu Jul 29 14:12:11 2010 +0200
1.2 +++ b/doc-src/isac/mat-eng-de.tex Tue Aug 03 13:55:24 2010 +0200
1.3 @@ -28,14 +28,14 @@
1.4
1.5 \chapter{Einleitung}
1.6 \section{``Authoring'' und ``Tutoring''}
1.7 -{TO DO} Mathematik lernen -- verschiedene Autoren -- Isabelle
1.8 +\paragraph{TO DO} Mathematik lernen -- verschiedene Autoren -- Isabelle
1.9 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.
1.10 \section{Der Inhalt des Dokuments}
1.11 \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.
1.12
1.13 -\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.
1.14 +\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.
1.15
1.16 -Das Dokument ist eigenst\"andig; Basiswissen \"uber SML (für eine Einf\"uhrung siehe \cite{Paulson:91}), Terme und Umschreibung wird vorrausgesetzt.
1.17 +Das Dokument ist eigenst\"andig; Basiswissen \"uber SML (f\"ur eine Einf\"uhrung siehe \cite{Paulson:91}), Terme und Umschreibung wird vorrausgesetzt.
1.18
1.19 %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.
1.20
1.21 @@ -44,7 +44,7 @@
1.22 \paragraph{Versuchen Sie es!} Ein weiteres Anliegen dieses Textes ist, dem Leser Tipps f\"ur Versuche mit den Anwendungen zu geben.
1.23
1.24 \section{Gleich am Computer ausprobieren!}\label{get-started}
1.25 -\paragraph{TO DO screenshot} Bevor Sie mit Ihren Versuchen beginnen, m\"ochten wir Ihnen noch einige Hinweise geben.
1.26 +\paragraph{TO DO screenshot} Bevor Sie mit Ihren Versuchen beginnen, m\"ochten wir Ihnen noch einige Hinweise geben:
1.27 \begin{itemize}
1.28 \item System starten
1.29 \item Shell aufmachen und die Datei mat-eng-de.sml \"offnen.
1.30 @@ -57,95 +57,104 @@
1.31 \part{Experimentelle Ann\"aherung}
1.32
1.33 \chapter{Terme und Theorien}
1.34 -Wie bereits erw\"ahnt, geht es um Computer-Mathematik. In den letzten Jahren hat die ``computer science'' grosse Fortschritte darin gemacht, Mathematik auf dem Computer verst\"andlich darzustellen. Dies gilt f\"ur mathematische Formeln, f\"ur die Beschreibung von Problem (behandelt in Abs.\ref{pbl}), f\"ur L\"osungsmethoden (behandelt in Abs.\ref{met}) etc. Wir beginnen mit mathematischen Formeln --- gleich zum Ausprobieren wie in Abs.\ref{get-started} oben vorbereitet.
1.35 +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.
1.36
1.37 \section{Von der Formel zum Term}
1.38 Um ein Beispiel zu nennen: Die Formel $a+b\cdot 3$ l\"asst sich in lesbarer Form so eingeben:
1.39 {\footnotesize\begin{verbatim}
1.40 - > "a + b * 3";
1.41 - val it = "a + b * 3" : string
1.42 + > "a + b * 3";
1.43 + val it = "a + b * 3" : string
1.44 \end{verbatim}}
1.45 -\noindent ``a + b * 3'' ist also ein String (=Zeichenfolge). In dieser Form weiss der Computer nicht, dass z.B. eine Multiplikation {\em vor} einer Addition zu rechnen ist. Isabelle braucht Formeln in einer anderen Form; Diese kann man mit der Funktion ``str2term'' (= string to term) umrechnen:
1.46 +\noindent ``a + b * 3'' ist also ein string (=Zeichenfolge). In dieser Form weiss der Computer nicht, dass z.B. eine Multiplikation {\em vor} einer Addition zu rechnen ist. Isabelle braucht dazu eine andere Darstellung f\"u Formeln. Diese kann man mit der Funktion {\tt str2term} (= string to term) umrechnen:
1.47 {\footnotesize\begin{verbatim}
1.48 - > str2term "a + b * 3";
1.49 - val it =
1.50 - Const ("op +", "[RealDef.real, RealDef.real] => RealDef.real") $
1.51 - Free ("a", "RealDef.real") $
1.52 - (Const ("op *", "[RealDef.real, RealDef.real] => RealDef.real") $ ... $
1.53 - ...) : Term.term
1.54 + > str2term "a + b * 3";
1.55 + val it =
1.56 + Const ("op +", "[RealDef.real, RealDef.real] => RealDef.real") $
1.57 + Free ("a", "RealDef.real") $
1.58 + (Const ("op *", "[RealDef.real, RealDef.real] => RealDef.real") $ ... $
1.59 + ...) : Term.term
1.60 \end{verbatim}}
1.61 -\noindent Jene Form braucht Isabelle intern zum rechnen. Sie heisst Term und ist nicht lesbar, daf\"ur aber speicherbar mit Hilfe von ``val'' (=value)
1.62 +\noindent Jene Form braucht Isabelle intern zum Rechnen. Sie heisst {\tt term} und ist nicht f\"ur den Menschen zum lesen gedacht. Wir wollen sie {\tt val} (= value) auf {\tt t} speichern
1.63 {\footnotesize\begin{verbatim}
1.64 - > val term = str2term "a + b * 3";
1.65 - val term =
1.66 - Const ("op +", "[RealDef.real, RealDef.real] => RealDef.real") $
1.67 - Free ("a", "RealDef.real") $
1.68 - (Const ("op *", "[RealDef.real, RealDef.real] => RealDef.real") $ ... $
1.69 - ...) : Term.term
1.70 + > val t = str2term "a + b * 3";
1.71 + val t =
1.72 + Const ("op +", "[RealDef.real, RealDef.real] => RealDef.real") $
1.73 + Free ("a", "RealDef.real") $
1.74 + (Const ("op *", "[RealDef.real, RealDef.real] => RealDef.real") $ ... $
1.75 + ...) : Term.term
1.76 \end{verbatim}
1.77 -Der gespeicherte Term kann einer Funktion ``atomty'' \"ubergeben werden, die jenen in einer abstrakten Struktur zeigt:
1.78 +\footnotesize\begin{verbatim}
1.79 + > t;
1.80 + val it =
1.81 + Const ("op +", "[RealDef.real, RealDef.real] => RealDef.real") $
1.82 + Free ("a", "RealDef.real") $
1.83 + (Const ("op *", "[RealDef.real, RealDef.real] => RealDef.real") $ ... $
1.84 + ...) : Term.term
1.85 + > parse Isac.thy "a + b * 3";
1.86 + val it = Some "a + b * 3" : Thm.cterm Library.option
1.87 + > val t = parse Isac.thy "a + b * 3";
1.88 + val t = Some "a + b * 3" : Thm.cterm Library.option
1.89 +\end{verbatim}
1.90 +Der gespeicherte term {\tt t} kann einer Funktion {\tt atomty} \"ubergeben werden, die diesen in einer dritten Form zeigt:
1.91 {\footnotesize\begin{verbatim}
1.92 - > atomty term;
1.93 + > atomty term;
1.94
1.95 - ***
1.96 - *** Const (op +, [real, real] => real)
1.97 - *** . Free (a, real)
1.98 - *** . Const (op *, [real, real] => real)
1.99 - *** . . Free (b, real)
1.100 - *** . . Free (3, real)
1.101 - ***
1.102 + ***
1.103 + *** Const (op +, [real, real] => real)
1.104 + *** . Free (a, real)
1.105 + *** . Const (op *, [real, real] => real)
1.106 + *** . . Free (b, real)
1.107 + *** . . Free (3, real)
1.108 + ***
1.109
1.110 - val it = () : unit
1.111 + val it = () : unit
1.112 \end{verbatim}%size
1.113 -
1.114 +Diese Darstellung nennt man ``abstract syntax'' und macht unmittelbar klar, dass man a und b nicht addieren kann, weil ein Mal vorhanden ist.
1.115
1.116 \section{``Theory'' und ``Parsing``}
1.117 -Die theory gibt an, welcher Ausdruck wo steht. Eine derzeitige theory wird intern als \texttt{thy} gekennzeichnet. Jene theory, die alles Wissen ent\"ahlt ist \isac{}.
1.118 -
1.119 +Der Unterschied zwischen \isac{} und bisheriger Mathematiksoftware (GeoGebra, Mathematica, Maple, Derive etc.) ist, dass das mathematische Wissen nicht im Programmcode steht, sondern in den theories.
1.120 +Die mathematischen Festlegungen des CTP werden in den theories abgelegt und sind nicht in Programmiersprachen, sondern in einer f\"ur Mathematik-lernende Personen lesbaren Form geschrieben. Das Wissen von \isac{} beinhaltet folgende {\tt thy}:
1.121 {\footnotesize\begin{verbatim}
1.122 - > Isac.thy;
1.123 - val it =
1.124 - {ProtoPure, CPure, HOL, Set, Typedef, Fun, Product_Type, Lfp, Gfp,
1.125 - Sum_Type, Relation, Record, Inductive, Transitive_Closure,
1.126 - Wellfounded_Recursion, NatDef, Nat, NatArith, Divides, Power,
1.127 - SetInterval, Finite_Set, Equiv, IntDef, Int, Datatype_Universe,
1.128 - Datatype, Numeral, Bin, IntArith, Wellfounded_Relations, Recdef, IntDiv,
1.129 - IntPower, NatBin, NatSimprocs, Relation_Power, PreList, List, Map,
1.130 - Hilbert_Choice, Main, Lubs, PNat, PRat, PReal, RealDef, RealOrd,
1.131 - RealInt, RealBin, RealArith0, RealArith, RComplete, RealAbs, RealPow,
1.132 - Ring_and_Field, Complex_Numbers, Real, ListG, Tools, Script, Typefix,
1.133 - Float, ComplexI, Descript, Atools, Simplify, Poly, Rational, PolyMinus,
1.134 - Equation, LinEq, Root, RootEq, RatEq, RootRat, RootRatEq, PolyEq, Vect,
1.135 - Calculus, Trig, LogExp, Diff, DiffApp, Integrate, EqSystem, Biegelinie,
1.136 - AlgEin, Test, Isac} : Theory.theory
1.137 + > Isac.thy;
1.138 + val it =
1.139 + {ProtoPure, CPure, HOL, Set, Typedef, Fun, Product_Type, Lfp, Gfp,
1.140 + Sum_Type, Relation, Record, Inductive, Transitive_Closure,
1.141 + Wellfounded_Recursion, NatDef, Nat, NatArith, Divides, Power,
1.142 + SetInterval, Finite_Set, Equiv, IntDef, Int, Datatype_Universe,
1.143 + Datatype, Numeral, Bin, IntArith, Wellfounded_Relations, Recdef, IntDiv,
1.144 + IntPower, NatBin, NatSimprocs, Relation_Power, PreList, List, Map,
1.145 + Hilbert_Choice, Main, Lubs, PNat, PRat, PReal, RealDef, RealOrd,
1.146 + RealInt, RealBin, RealArith0, RealArith, RComplete, RealAbs, RealPow,
1.147 + Ring_and_Field, Complex_Numbers, Real, ListG, Tools, Script, Typefix,
1.148 + Float, ComplexI, Descript, Atools, Simplify, Poly, Rational, PolyMinus,
1.149 + Equation, LinEq, Root, RootEq, RatEq, RootRat, RootRatEq, PolyEq, Vect,
1.150 + Calculus, Trig, LogExp, Diff, DiffApp, Integrate, EqSystem, Biegelinie,
1.151 + AlgEin, Test, Isac} : Theory.theory
1.152 \end{verbatim}
1.153 -Die, die ein Mal enth\"alt ist groups.thy. Suchen Sie nach '*' unter der Adresse:
1.154 -
1.155 -http://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/library/HOL/Groups.html
1.156 -Hier wird Ihnen erkl\"art, wie das Mal vom Computer gelesen wird.
1.157 +Dass das Mal vor dem Plus berechnet wird, ist so festgelegt:
1.158 {\footnotesize\begin{verbatim}
1.159 - > Group.thy
1.160 + > Group.thy
1.161 fixes f :: "'a => 'a => 'a" (infixl "*" 70)
1.162 assumes assoc [ac_simps]: "a * b * c = a * (b * c)"
1.163 \end{verbatim}
1.164 -Der ''infix`` ist der Operator, der zwischen zwei Argumenten steht. 70 bedeutet, dass Mal eine hohe Priorit\"at hat (bei einem Plus liegt der Wert bei 50 oder 60).
1.165 +Ohne weitere Erkl\"arungen: 70 bedeutet, dass Mal eine hohe Priorit\"at hat als Plus (hier liegt der Wert zwischen 50 und 60).
1.166
1.167 Parsing entsteht durch einen string und eine theory. Es verwendet Informationen, die in der theory von Isabelle enthalten sind.
1.168 {\footnotesize\begin{verbatim}
1.169 - > parse;
1.170 - val it = fn : Theory.theory -> string -> Thm.cterm Library.option
1.171 + > parse;
1.172 + val it = fn : Theory.theory -> string -> Thm.cterm Library.option
1.173 \end{verbatim}
1.174 Dieser term kann wieder in seine einzelnen Teile zerlegt werden.
1.175 {\footnotesize\begin{verbatim}
1.176 > val it = (term_of o the) it;
1.177 - val it =
1.178 - Const ("op +", "[RealDef.real, RealDef.real] => RealDef.real") $
1.179 - Free ("a", "RealDef.real") $
1.180 - (Const ("op *", "[RealDef.real, RealDef.real] => RealDef.real") $ ... $
1.181 - ...) : Term.term
1.182 + val it =
1.183 + Const ("op +", "[RealDef.real, RealDef.real] => RealDef.real") $
1.184 + Free ("a", "RealDef.real") $
1.185 + (Const ("op *", "[RealDef.real, RealDef.real] => RealDef.real") $ ... $
1.186 + ...) : Term.term
1.187 \end{verbatim}
1.188
1.189 -\paragraph{Versuchen Sie es!} Das mathematische Wissen w\"achst, indem man zu den Urspr\"ungen schaut. In den folgenden Beispielen werden verschiedene Meldungen genauer erkl\"art.
1.190 +\paragraph{Versuchen Sie es!} Das mathematische Wissen w\"achst mit jeder {\tt thy} von ProtoPure bis Isac. In den folgenden Beispielen wird gezeigt, wie das Wissen w\"achst.
1.191
1.192 {\footnotesize\begin{verbatim}
1.193 > (*-1-*);
1.194 @@ -153,14 +162,14 @@
1.195 *** Inner lexical error at: "^^^3"
1.196 val it = None : Thm.cterm Library.option
1.197 \end{verbatim}
1.198 -''Inner lexical error`` bedeutet, dass ein Fehler aufgetreten ist, vermutlich hat man sich vertippt.
1.199 +''Inner lexical error`` und ''None`` bedeuten, dass ein Fehler aufgetreten ist, denn das Wissen \"uber {\tt *} findet sich erst in der theorie group.
1.200
1.201 {\footnotesize\begin{verbatim}
1.202 > (*-2-*);
1.203 > parse HOL.thy "d_d x (a + x)";
1.204 val it = None : Thm.cterm Library.option
1.205 \end{verbatim}
1.206 -Fehlt ''Inner lexical error`` wurde der Parse nicht gefunden.
1.207 +Hier wiederum ist noch kein Wissen \"uber das Differenzieren vorhanden.
1.208
1.209 {\footnotesize\begin{verbatim}
1.210 > (*-3-*);
1.211 @@ -179,8 +188,7 @@
1.212 > val Some t5 = parse Diff.thy "d_d x (a + x)";
1.213 val t5 = "d_d x (a + x)" : Thm.cterm
1.214 \end{verbatim}
1.215 -
1.216 -Der Pase liefert hier einen ''zu sch\"onen`` Ausdruck in Form eines cterms, der wie ein string aussieht. Am verl\"asslichsten sind terme, die sich selbst erzeugen lassen.
1.217 +Die letzen drei Aufgaben k\"onnen schon gel\"ost werden, da Rational.thy \"uber das n\"otige Wissen verf\"ugt.
1.218
1.219 \section{Details von Termen}
1.220 Mit Hilfe der darunterliegenden Darstellung sieht man, dass ein cterm in einen term umgewandelt werden kann.
1.221 @@ -196,19 +204,19 @@
1.222 ...: Term.term
1.223
1.224 \end{verbatim}
1.225 -In diesem Fall sagt uns das ''Const``, dass die Variable eine Konstante ist, also ein Fixwert ist und immer die selbe Funktion hat.
1.226 +In diesem Fall sagt uns das ''Const``, dass die Variable eine Konstante ist, also ein Fixwert, der immer die selbe Funktion hat.
1.227 {\footnotesize\begin{verbatim}
1.228 > term_of t5;
1.229 val it =
1.230 Const ("Diff.d_d", "[RealDef.real, RealDef.real] => RealDef.real") $ ... $
1.231 ... : Term.term
1.232 \end{verbatim}
1.233 -Sollten verschiedene Teile des Output nicht sichtbar sein, kann die Schriftgr\"osse ge\"andert werden.
1.234 +Sollten verschiedene Teile des ''output`` (= das vom Computer Ausgegebene) nicht sichtbar sein, kann man mit einem bestimmten Befehl alles angezeigt werden.
1.235 {\footnotesize\begin{verbatim}
1.236 > print_depth;
1.237 val it = fn : int -> unit
1.238 \end{verbatim}
1.239 -Zuerst gibt man die Schriftgr\"osse ein, danach den term, der gr\"osser werden soll.
1.240 +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.
1.241 {\footnotesize\begin{verbatim}
1.242 > print_depth 10;
1.243 val it = () : unit
1.244 @@ -230,7 +238,7 @@
1.245 Free ("a", "RealDef.real") $ Free ("x", "RealDef.real"))
1.246 : Term.term
1.247 \end{verbatim}
1.248 -
1.249 +\paragraph{Versuchen Sie es!}
1.250 Eine andere Variante um den Unterschied der beiden Terme zu sehen ist folgende:
1.251 {\footnotesize\begin{verbatim}
1.252 > (*-4-*) val thy = Rational.thy;
1.253 @@ -288,103 +296,100 @@
1.254 \end{verbatim}
1.255
1.256
1.257 -{\chapter{''Rewriting``}}
1.258 -{\section{}}
1.259 -Bei Rewriting handelt es sich um die Vereinfachung eines Terms in vielen kleinen Schritten und nach bestimmten Regeln. Der Computer wendet dabei hintereinander verschiedene Rechengesetze an, weil er den Term ansonsten nicht l\"osen kann.
1.260 -
1.261 -{\footnotesize\begin{verbatim}
1.262 -> rewrite_;
1.263 -val it = fn
1.264 -:
1.265 - Theory.theory ->
1.266 - ((Term.term * Term.term) list -> Term.term * Term.term -> bool) ->
1.267 - rls ->
1.268 - bool ->
1.269 - Thm.thm -> Term.term -> (Term.term * Term.term list) Library.option
1.270 -
1.271 +\chapter{''Rewriting``}
1.272 +\section{Was ist Rewriting?}
1.273 +Bei Rewriting handelt es sich um das Umformen von Termen nach vorgegebenen Regeln. Folgende zwei Funktionen sind notwendig:
1.274 +\footnotesize\begin{verbatim}
1.275 > rewrite;
1.276 val it = fn
1.277 :
1.278 - theory' ->
1.279 - rew_ord' ->
1.280 - rls' -> bool -> thm' -> cterm' -> (string * string list) Library.option
1.281 -
1.282 +theory' ->
1.283 +rew_ord' ->
1.284 +rls' -> bool -> thm' -> cterm' -> (string * string list) Library.option
1.285 \end{verbatim}
1.286 -\textbf{Versuchen Sie es!} Um zu sehen, wie der Computer vorgeht und welche Rechengesetze er anwendet, zeigen wir Ihnen durch Differenzieren von (a + a * (2 + b)), die einzelnen Schritte. Sie k\"onnen nat\"urlichauch selbst einige Beispiele ausprobieren!
1.287 -
1.288 -Zuerst legt man fest, dass es sich um eine Differenzierung handelt.
1.289 -{\footnotesize\begin{verbatim}
1.290 - > val thy' = "Diff.thy";
1.291 - val thy' = "Diff.thy" : string
1.292 -\end{verbatim}
1.293 -Dann gibt man die zu l\"osende Rechnung ein.
1.294 -{\footnotesize\begin{verbatim}
1.295 - > val ct = "d_d x (a + a * (2 + b))";
1.296 - val ct = "d_d x (a + a * (2 + b))" : string
1.297 -\end{verbatim}
1.298 -Anschließend gibt man bekannt, dass die Summenregel angewandt werden soll.
1.299 -{\footnotesize\begin{verbatim}
1.300 - > val thm = ("diff_sum","");
1.301 - val thm = ("diff_sum", "") : string * string
1.302 -\end{verbatim}
1.303 -Schliesslich wird die erste Ableitung angezeigt.
1.304 -{\footnotesize\begin{verbatim}
1.305 - > val Some (ct,_) = rewrite_inst thy' "tless_true" "eval_rls" true
1.306 - [("bdv","x::real")] thm ct;#
1.307 - val ct = "d_d x a + d_d x (a * (2 + b))" : cterm'
1.308 -\end{verbatim}
1.309 -Will man auch die zweite Ableitung sehen, geht man so vor:
1.310 -{\footnotesize\begin{verbatim}
1.311 - > val thm = ("diff_prod_const","");
1.312 - val thm = ("diff_prod_const", "") : string * string
1.313 -\end{verbatim}
1.314 -Auch die zweite Ableitung wird sichtbar.
1.315 -{\footnotesize\begin{verbatim}
1.316 - > val Some (ct,_) = rewrite_inst thy' "tless_true" "eval_rls" true
1.317 - [("bdv","x::real")] thm ct;#
1.318 - val ct = "d_d x a + a * d_d x (2 + b)" : cterm'
1.319 -\end{verbatim}
1.320 -
1.321 -{\section{M\"oglichkeiten von Rewriting}
1.322 -Es gibt verscheidene Varianten von Rewriting, die alle eine bestimmte Bedeutung haben.
1.323 -\textit{rewrite\_inst} bedeutet, dass die Liste der Terme vor dem Rewriting durch ein ''Theorem`` (ein mathematischer Begriff f\"ur einen Satz) ersetzt wird.
1.324 -{\footnotesize\begin{verbatim}
1.325 +Im Rewriting stehen die Argumente, die mitgeschickt werden m\"ussen, um die verschiedenen Rechnungen zu l\"osen.
1.326 +Da es jedoch so viele Argumente (7) sind werden die Werte in Variablen abgespeichert.
1.327 +\footnotesize\begin{verbatim}
1.328 > rewrite_inst;
1.329 val it = fn
1.330 :
1.331 - theory' ->
1.332 - rew_ord' ->
1.333 - rls' ->
1.334 - bool -> 'a -> thm' -> cterm' -> (cterm' * cterm' list) Library.option
1.335 +theory' ->
1.336 +rew_ord' ->
1.337 +rls' ->
1.338 +bool -> 'a -> thm' -> cterm' -> (cterm' * cterm'list) Library.option
1.339 \end{verbatim}
1.340 -Mit Hilfe von \textit{rewrite\_set} werden Terme, die normalerweise nur mit einem Thoerem vereinfacht dargestellt werden, mit einem ganzen ''rule set`` (=Regelsatz, weiter unten erkl\"art) umgeschrieben.
1.341 -{\footnotesize\begin{verbatim}
1.342 - > rewrite_set;
1.343 - val it = fn
1.344 - : theory' -> bool -> rls' -> cterm' -> (string * string list) Library.option
1.345 +Die Funktion {\tt rewrite\_inst} wird ben\"otigt, um Gleichungen und Aufgaben, bei welchen differenziert werden muss zu l\"osen. Dabei wird die ungebundene Variable (bdv) instanziiert, d.h. es wird die Variable angegeben, nach der man differenzieren will, bzw. f\"ur die ein Wert/Ausdruck bei einer Gleichung herauskommen soll.
1.346 +\paragraph{Versuchen Sie es!} Um zu sehen wie der Computer vorgeht, um folgendes Beispiel, dessen Ergebnis logischer Weise 0 ist, zu l\"osen werden hier die einzelnen Schritte durch differenzieren von a + a * (2 + b) gezeigt.
1.347 +Zuerst werden die einzelnen Werte als Variablen gespeichert:
1.348 +\footnotesize\begin{verbatim}
1.349 +> val thy' = "Differentiate.thy";
1.350 +val thy' = "Differentiate.thy" : string
1.351 +> val ct = "d_d x (x ^^^ 2 + 3 * x + 4)";
1.352 +val ct = "d_d x (x ^^^ 2 + 3 * x + 4)" : string
1.353 +> val thm = ("diff_sum","");
1.354 +val thm = ("diff_sum", "") : string * string
1.355 \end{verbatim}
1.356 -\textit{rewrite\_set\_inst} ist eine Kombination der beiden oben genannten M\"oglichkeiten.
1.357 -{\footnotesize\begin{verbatim}
1.358 - > rewrite_set_inst;
1.359 - val it = fn
1.360 - :
1.361 - theory' ->
1.362 - bool -> subs' -> rls' -> cterm' -> (string * string list) Library.option
1.363 +Schliesslich wird die erste Ableitung angezeigt.
1.364 +\footnotesize\begin{verbatim}
1.365 +> val Some (ct,_) = rewrite_inst thy' "tless_true" "eval_rls" true
1.366 +[("bdv","x::real")] thm ct;
1.367 +val ct = "d_d x (x ^^^ 2) + d_d x (3 * x) + d_d x 4" : cterm'
1.368 \end{verbatim}
1.369 -Wenn man sehen m\"ochte, wie Rewriting bei den einzelnen Theorems funktioniert, kann man dies mit \textit{trace\_rewrite} versuchen.
1.370 -{\footnotesize\begin{verbatim}
1.371 - > toggle;
1.372 - val it = fn : bool ref -> bool
1.373 - > toggle trace_rewrite;
1.374 - val it = true : bool
1.375 - > toggle trace_rewrite;
1.376 - val it = false : bool
1.377 +Will man auch die zweite Ableitung sehen, geht man so vor:
1.378 +\footnotesize\begin{verbatim}
1.379 +> val thm = ("diff_prod_const","");
1.380 +val thm = ("diff_prod_const", "") : string * string
1.381 +> val Some (ct,_) = rewrite_inst thy' "tless_true" "eval_rls" true
1.382 +[("bdv","x::real")] thm ct;
1.383 +val ct = "d_d x (x ^^^ 2) + 3 * d_d x x + d_d x 4" : cterm'
1.384 \end{verbatim}
1.385 -
1.386 +Wenn Sie sich noch weitere Beispiele ansehen wollen, dann besuchen sie bitte die folgende Site: {\tt [isac-src]/tests/\dots}.
1.387 +
1.388 +\section{Was kann Rewriting?}
1.389 +Es gibt verschiedene Varianten von Rewriting, die alle eine bestimmte Bedeutung haben.
1.390 +{\tt rewrite\_ set} verwandelt Terme, die normalerweise nur mit einem Theorem vereinfacht dargestellt werden, in ein ganzes Rule Set.
1.391 +Hierbei werden auch folgende Argumente verwendet:\\
1.392 +\tabcolsep=4mm
1.393 +\def\arraystretch{1.5}
1.394 +\begin{tabular}{lp{11.0cm}}
1.395 +{\tt theory} & Die Theory von Isabelle, die die n\"otigen Informationen f\"ur das Parsing {\tt term} enth\"alt. \\
1.396 +{\tt rew\_ord}& die Rewriting Ordnung f\"ur das geordnete Rewriting. F\"ur {\em no} ben\"otigt das geordnete Rewriting {\tt tless\_true}, eine Ordnung, die f\"ur alle nachgiebigen Argumente true ist \\
1.397 +{\tt rls} & Das rule set; zur Auswertung von bestimmten Bedingungen in {\tt thm} falls {\tt thm} eine conditional rule ist \\
1.398 +{\tt bool} & ein Bitschalter, der die Berechnungen der m\"oglichen condition in {\tt thm} ausl\"ost: wenn sie {\tt falsch} ist, dann wird die condition bewertet und auf Grund des Resultats wendet man {\tt thm} an, oder nicht (conditional rewriting), wenn {\tt true} dann wird die condition nicht ausgewertet, aber man gibt sie in ein Menge von Hypothesen \\
1.399 +{\tt thm} & das theorem versucht den {\tt term} zu \"uberschreiben \\
1.400 +{\tt term} & {\tt thm} wendet Rewriting m\"oglicherweise auf den Term an \\
1.401 +\end{tabular}\\
1.402 +
1.403 +\footnotesize\begin{verbatim}
1.404 +> rewrite_set_;
1.405 +val it = fn
1.406 +: theory -> rls -> bool -> rls -> term -> (term * term list) option
1.407 +\end{verbatim}
1.408 +{\tt rewrite\_ set\_ inst} ist eine Kombination der oben genannten M\"oglichkeiten.
1.409 +\footnotesize\begin{verbatim}
1.410 +> rewrite_set_inst_;
1.411 +val it = fn
1.412 +: theory
1.413 +-> rls
1.414 +-> bool
1.415 +-> (cterm' * cterm') list
1.416 +-> rls -> term -> (term * term list) option
1.417 +\end{verbatim}
1.418 +Wenn man sehen m\"ochte wie Rewriting bei den einzelnen theorems funktioniert kann man dies mit {\tt trace\_ rewrite} versuchen.
1.419 +\footnotesize\begin{verbatim}
1.420 +> toggle;
1.421 +val it = fn : bool ref -> bool
1.422 +> toggle trace_rewrite;
1.423 +val it = true : bool
1.424 +> toggle trace_rewrite;
1.425 +val it = false : bool
1.426 +\end{verbatim}
1.427 +
1.428 +
1.429 \section{Rule sets}
1.430 -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.
1.431 +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.
1.432 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.
1.433 -Ein Beispiel f\"ur einen Regelsatz ist folgendes:
1.434 +Ein Beispiel f\"ur einen rule set ist folgendes:
1.435 \footnotesize\begin{verbatim}
1.436 ???????????
1.437 \end{verbatim}
1.438 @@ -451,7 +456,7 @@
1.439 Term.term -> Theory.theory -> (string * Term.term) Library.option) ->
1.440 Term.term -> (Term.term * (string * Thm.thm)) Library.option
1.441 \end{verbatim}
1.442 -Man bekommt das Ergebnis und die Theorem bezieht sich darauf. Daher sind die folgenden mathematischen Rechnungen m\"oglich:
1.443 +Man bekommt das Ergebnis und das theorem bezieht sich darauf. Daher sind die folgenden mathematischen Rechnungen m\"oglich:
1.444 \footnotesize\begin{verbatim}
1.445 > calclist;
1.446 val it =
1.447 @@ -472,18 +477,15 @@
1.448 string ->
1.449 Term.term -> Theory.theory -> (string * Term.term) Library.option))) list
1.450 \end{verbatim}
1.451 -Diese werden so angewendet:
1.452 -\footnotesize\begin{verbatim}
1.453 -\end{verbatim}
1.454 +
1.455
1.456
1.457
1.458 \chapter{Termordnung}
1.459 -Die Anordnungen der Begriffe sind unverzichtbar f\"ur den Gebrauch des Umschreibens von normalen Funktionen und von normalen Formeln, die n\"otig sind um passende Modelle für Probleme zu finden.
1.460 +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.
1.461
1.462 \section{Beispiel f\"ur Termordnungen}
1.463 -Es ist nicht unbedeutend eine Verbindung $<$ zu Termen herzustellen, die wirklich eine Ordnung besitzen, wie eine \"ubergehende und antisymmetrische Verbindung. Diese Ordnungen sind selbstaufrufende Bahnordnungen.
1.464 -Hier ein Beispiel:
1.465 +Es ist nicht unbedeutend, eine Verbindung zu Termen herzustellen, die wirklich eine Ordnung besitzen. Diese Ordnungen sind selbstaufrufende Bahnordnungen:
1.466
1.467 {\footnotesize\begin{verbatim}
1.468 > sqrt_right;
1.469 @@ -492,17 +494,15 @@
1.470 val it = fn : subst -> Term.term * Term.term -> bool
1.471 \end{verbatim}
1.472
1.473 -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.
1.474 +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.
1.475
1.476 {\section{Geordnetes Rewriting}}
1.477 -Beim Rewriting entstehen Probleme in den meisten elementaren Bereichen. Es gibt ein ''law of commutativity`` das genau solche Probleme mit '+' und '*' verursacht. Diese Probleme können nur durch geordnetes Rewriting gel\"ost werden, da hier ein Term nur umgeschrieben wird, wenn ein kleinerer dadurch entsteht.
1.478 -\paragraph{Versuchen Sie es!} Das geordnete Rewriting ist eine Technik, um ein normales Polynom aus ganzzahligen Termen zu schaffen.
1.479 -Geordnetes Rewriting endet mit Klammern, aber auf Grund der weggelassenen Verbindung.
1.480 +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.
1.481
1.482
1.483 -\chapter{Die Hirarchie von Problemen}
1.484 +\chapter{Problem hierachy}
1.485 \section{''Matching``}
1.486 -Matching ist eine Technik von Rewriting, die von \isac verwendet wird, um ein Problem und den passenden Problemtyp daf\"ur zu finden. Die folgende Funktion, die \"uberpr\"uft, ob matching möglich ist, hat diese Signatur:
1.487 +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:
1.488 {\footnotesize\begin{verbatim}
1.489 > matches;
1.490 val it = fn : Theory.theory -> Term.term -> Term.term -> bool
1.491 @@ -520,7 +520,7 @@
1.492 Free ("x", "RealDef.real") $ Free ("2", " RealDef.real"))) $
1.493 Free ("1", "RealDef.real") : Term.term
1.494 \end{verbatim}
1.495 -Nun wird ein Modell erstellt, das sich nicht auf bestimmte Zahlen bezieht, sondern nur eine generelle Zerlegung durchführt.
1.496 +Nun wird ein Modell erstellt, das sich nicht auf bestimmte Zahlen bezieht, sondern nur eine generelle Zerlegung durchf\"uhrt.
1.497 {\footnotesize\begin{verbatim}
1.498 > val p = (term_of o the o (parse thy)) "a * b^^^2 = c";
1.499 val p =
1.500 @@ -533,7 +533,7 @@
1.501 Free ("b", "RealDef.real") $ Free ("2", "RealDef.real"))) $
1.502 Free ("c", "RealDef.real") : Term.term
1.503 \end{verbatim}
1.504 -Dieses Modell enth\"allt sogenannte \textit{scheme variables}.
1.505 +Dieses Modell enth\"alt sogenannte \textit{scheme variables}.
1.506 {\footnotesize\begin{verbatim}
1.507 > atomt p;
1.508 "*** -------------"
1.509 @@ -546,7 +546,7 @@
1.510 "\n"
1.511 val it = "\n" : string
1.512 \end{verbatim}
1.513 -Das Modell wird durch den Befehl free2var erstellt.
1.514 +Das Modell wird durch den Befehl \textit{free2var} erstellt.
1.515 {\footnotesize\begin{verbatim}
1.516 > free2var;
1.517 val it = fn : Term.term -> Term.term
1.518 @@ -564,7 +564,7 @@
1.519 > Sign.string_of_term (sign_of thy) pat;
1.520 val it = "?a * ?b ^^^ 2 = ?c" : string
1.521 \end{verbatim}
1.522 -Durch atomt pat wird der Term aufgespalten und so in eine Form gebracht, die f\"ur die weiteren Schritte ben\"otigt werden.
1.523 +Durch \textit{atomt pat} wird der term aufgespalten und in eine Form gebracht, die f\"ur die weiteren Schritte ben\"otigt wird.
1.524 {\footnotesize\begin{verbatim}
1.525 > atomt pat;
1.526 "*** -------------"
1.527 @@ -578,7 +578,7 @@
1.528 "\n"
1.529 val it = "\n" : string
1.530 \end{verbatim}
1.531 -Jetzt kann das Matching f\"ur die beiden vorigen Terme angewendet werden.
1.532 +Jetzt kann das Matching an den beiden vorigen Terme angewendet werden.
1.533 {\footnotesize\begin{verbatim}
1.534 > matches thy t pat;
1.535 val it = true : bool
1.536 @@ -604,8 +604,8 @@
1.537 val it = true : bool
1.538 \end{verbatim}
1.539
1.540 -\section{Zugriff auf die Hierarchie}
1.541 -Man verwendet folgenden Befehl, um sich Zugang zur Hierarchie von Problemtypen zu verschaffen.
1.542 +\section{Zugriff auf die hierachy}
1.543 +Man verwendet folgenden Befehl, um sich Zugang zur hierachy von problem type zu verschaffen.
1.544 {\footnotesize\begin{verbatim}
1.545 > show_ptyps;
1.546 val it = fn : unit -> unit
1.547 @@ -665,19 +665,11 @@
1.548 val it = () : unit
1.549 \end{verbatim}
1.550
1.551 -\section{Die passende ''Formalization`` f\"ur den Problemtyp}
1.552 -Eine andere Art des Matching ist es die richtige ''Formalization`` zum jeweiligen Problemtyp zu finden. Wenn es eine ''Formalization`` gibt, dann kann \isac{} selbstst\"andig die Probleme l\"osen.
1.553 +\section{Die passende ''formalization`` f\"ur den problem type}
1.554 +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.
1.555
1.556 -\section{Problem - Refinement}
1.557 -Will man die Hierarchie der Probleme aufstellen, so ist darauf zu achten, dass man die verschiedenen Branches so konstruiert, dass das Problem - Refinement automatisch durchgef\"uhrt werden kann. F\"ur diese Anwendung wird die Hierarchie nach folgenden Regeln aufgestellt:
1.558 -$F$ ist eine Formalization und $P$ und $P_i,\:i=1\cdots n$ sind Problemtypen, wobei $P_i$ ein spezieller Problemtyp ist, im Bezug auf $P$, dann gilt:
1.559 -{\small
1.560 -\begin{enumerate}
1.561 -\item wenn für $F$ der Problemtyp $P_i$ passt, dann passt auch $P$
1.562 -\item wenn zu $F$ der Problemtyp P passt, dann sollte es nicht mehr als ein $P_i$ geben, das zu $F$ passt.
1.563 -\item alle $F$ , die zu $P$ passen, m\"ussen auch zu $P_n$ passen
1.564 -\end{enumerate}
1.565 -Zuerst ein Beispiel für die ersten zwei Punkte:
1.566 +\section{''problem-refinement``}
1.567 +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.
1.568 {\footnotesize\begin{verbatim}
1.569 > refine;
1.570 val it = fn : fmz_ -> pblID -> SpecifyTools.match list
1.571 @@ -693,7 +685,7 @@
1.572 *** comp_dts: ??.empty $ soleFor x
1.573 Exception- ERROR raised
1.574 \end{verbatim}
1.575 -Wenn die ersten zwei Regeln nicht angewendet werden k\"onnen, wird die dritte verwendet:
1.576 +Wenn die ersten zwei Regeln nicht angewendet werden k\"onnen, kommt die dritte zum Einsatz:
1.577 {\footnotesize\begin{verbatim}
1.578 > val fmz = ["equality (x + 1 = 2)",
1.579 # "solveFor x","errorBound (eps=0)",
1.580 @@ -719,12 +711,12 @@
1.581 NoMatch (["linear", "univariate", ...], {Find = [...], ...}),
1.582 NoMatch (["root", ...], ...), ...] : SpecifyTools.match list
1.583 \end{verbatim}
1.584 -Der Problemtyp $P_n$ verwandelt x + 1 = 2 in die normale Form -1 + x = 0. Diese suche nach der jeweiligen Problemhierarchie kann mit Hilfe von einem ''proof state`` durchgeführt werden (siehe nächstes Kapitel).
1.585 +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).
1.586
1.587
1.588 -\chapter{Methods}
1.589 -Methods werden dazu verwendet, Probleme von \texttt{type} zu l\"osen. Sie sind in einer anderen Programmiersprache beschrieben. Die Sprache sieht einfach aus, hat aber im Hintergrund einen enormen Pr\"ufauffwand. So muss sich der Programmierer nicht mit technischen Details befassen, gleichzeitig k\"onnen aber auch keine falschen Anweisungen eingegeben werden.
1.590 -\section{Der ''Syntax`` des Scriptes}
1.591 +\chapter{''Methods``}
1.592 +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.
1.593 +\section{Der ''Syntax`` des script}
1.594 Syntax beschreibt den Zusammenhang der einzelnen Zeichen und Zeichenfolgen mit den Theorien.
1.595 Er kann so definiert werden:
1.596 \begin{tabbing}
1.597 @@ -753,7 +745,7 @@
1.598 \item{{\tt while} prop {\tt Do} expr id}
1.599 \item{{\tt if} prop {\tt then} expr {\tt else} expr}
1.600 \end{description}
1.601 -W\"ahrend die genannten Bezeichnungen das Kontrollsystem durch Auswertung der Formeln ausl\"osen, h\"angen die anderen von der Anwendbarkeit der Formel in den entsprechenden Unterbegriffen ab:
1.602 +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:
1.603 \begin{description}
1.604 \item{{\tt Repeat} expr id}
1.605 \item{{\tt Try} expr id}
1.606 @@ -766,31 +758,31 @@
1.607
1.608 \chapter{Befehle von \isac{}}
1.609 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.\
1.610 -\newline \textbf{Init\_Proof\_Hid (dialogmode, formalization, specifictaion} gibt die eingegebenen Befehle weiter an die mathematic engine, wobei die beiden letzten Begriffe die Beispiele automatisch speichern. Es ist nicht vorgesehen, dass der Sch\"uler tactic verwendet.\
1.611 -\newline \textbf{Init\_Proof} bildet mit einem ''proof tree`` ein leeres Modell.\
1.612 -\newline \textbf{Model\_Problem problem} bestimmt ein problemtype, das wom\"oglich in der ''hierachy`` gefunden wurde, und verwendet es f\"u das Umformen.\
1.613 -\newline \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.\
1.614 -\newline \textbf{Specify\_Theorie theory, Specify\_Problem proble, Specify\_Method method} gibt das entsprechende Element des Basiswissens an.\
1.615 -\newline \textbf{Refine\_Problem problem} sucht nach einem Problem in der hierachy, das auf das vorhandene zutrifft.\
1.616 -\newline \textbf{Apply\_Method method} beendet das Modell und die Beschreibung. Danach wird die L\"osungmeldung ge\"offnet.\
1.617 -\newline \textbf{Free\_Solve} beginnt eine L\"osungsmeldung ohne die Hilfe eine method.\
1.618 -\newline \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``.\
1.619 -\newline \textbf{Rewrite\_Asm theorem} hat die gleiche Funktion wie Rewrite, speichert jedoch eine endg\"ultige Vorraussetzung des Theorems, anstatt diese zu sch\"atzen.\
1.620 -\newline \textbf{Rewrite\_Set ruleset} hat \"ahnliche Funktionen wie Rewrite, gilt aber f\"ur einen ganzen Satz von Theorems, dem rule set.\
1.621 -\newline \textbf{Rewrite\_Inst (substitution, theorem), Rewrite\_Set\_Inst (substitution, rule set)} ist vergleichbar mit besonderen tactics, ersetzt aber Konstanten in der Theorem, bevor es zu einer Anwendung kommt.\
1.622 -\newline \textbf{Calculate operation} berechnet das Ergebnis der Eingabe mit der aktuellen Formel (plus, minus, times, cancel, pow, sqrt).\
1.623 -\newline \textbf{Substitute substitution} f\"ugt substitution der momentanen Formel hinzu und wandelt es um.\
1.624 -\newline \textbf{Take formula} startet eine neue Reihe von Rechnungen in den Formeln, wo sich schon eine andere Rechnung befindet.\
1.625 -\newline \textbf{Subproblem (theory, problem)} beginnt ein subproblem innerhalb einer Rechnung.\
1.626 -\newline \textbf{Function formula} ruft eine Funktion auf, in der der Name in der Formel enthalten ist. ???????\
1.627 -\newline \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.\
1.628 -\newline \textbf{Check\_elementwise assumption} wird in Bezug auf die aktuelle Formel verwendet, die Elemente in einer Liste enth\"alt.\
1.629 -\newline \textbf{Or\_to\_List} wandelt eine Verbindung von Gleichungen in eine Liste von Gleichungen um.\
1.630 -\newline \textbf{Check\_postcond:} \"uberpr\"uft die momentane Formel im Bezug auf die Nachbedinung beim beenden des subproblem.\
1.631 -\newline \textbf{End\_Proof} beendet eine \"Uberpr\"ufung und gibt erst dann ein Ergebnis aus, wenn Check\_postcond erfolgreich abgeschlossen wurde.
1.632 +\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.\
1.633 +\newline\linebreak \textbf{Init\_Proof} bildet mit einem ''proof tree`` ein leeres Modell.\
1.634 +\newline\linebreak \textbf{Model\_Problem problem} bestimmt ein problemtype, das wom\"oglich in der ''hierachy`` gefunden wurde, und verwendet es f\"ur das Umformen.\
1.635 +\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.\
1.636 +\newline\linebreak \textbf{Specify\_Theorie theory, Specify\_Problem proble, Specify\_Method method} gibt das entsprechende Element des Basiswissens an.\
1.637 +\newline\linebreak \textbf{Refine\_Problem problem} sucht nach einem Problem in der hierachy, das auf das vorhandene zutrifft.\
1.638 +\newline\linebreak \textbf{Apply\_Method method} beendet das Modell und die Beschreibung. Danach wird die L\"osungmeldung ge\"offnet.\
1.639 +\newline\linebreak \textbf{Free\_Solve} beginnt eine L\"osungsmeldung ohne die Hilfe einer method.\
1.640 +\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``.\
1.641 +\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.\
1.642 +\newline\linebreak \textbf{Rewrite\_Set ruleset} hat \"ahnliche Funktionen wie Rewrite, gilt aber f\"ur einen ganzen Satz von theorems, dem rule set.\
1.643 +\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.\
1.644 +\newline\linebreak \textbf{Calculate operation} berechnet das Ergebnis der Eingabe mit der aktuellen Formel (plus, minus, times, cancel, pow, sqrt).\
1.645 +\newline\linebreak \textbf{Substitute substitution} f\"ugt der momentanen Formel {\tt substitution} hinzu und wandelt es um.\
1.646 +\newline\linebreak \textbf{Take formula} startet eine neue Reihe von Rechnungen in den Formeln, wo sich schon eine andere Rechnung befindet.\
1.647 +\newline\linebreak \textbf{Subproblem (theory, problem)} beginnt ein subproblem innerhalb einer Rechnung.\
1.648 +\newline\linebreak \textbf{Function formula} ruft eine Funktion auf, in der der Name in der Formel enthalten ist. ???????\
1.649 +\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.\
1.650 +\newline\linebreak \textbf{Check\_elementwise assumption} wird in Bezug auf die aktuelle Formel verwendet, die Elemente in einer Liste enth\"alt.\
1.651 +\newline\linebreak \textbf{Or\_to\_List} wandelt eine Verbindung von Gleichungen in eine Liste von Gleichungen um.\
1.652 +\newline\linebreak \textbf{Check\_postcond} \"uberpr\"uft die momentane Formel im Bezug auf die Nachbedinung beim Beenden des subproblem.\
1.653 +\newline\linebreak \textbf{End\_Proof} beendet eine \"Uberpr\"ufung und gibt erst dann ein Ergebnis aus, wenn Check\_postcond erfolgreich abgeschlossen wurde.
1.654
1.655 \section{Die Funktionsweise der mathematic engine}
1.656 -Ein proof (= Beweis) wird in der mathematic engine {\tt me} von der tactic {\tt Init\_Proof} gestartet und wird wechselwirkend mit anderen tactics vornagebracht. Auf den input (= das, was eingegeben wurde) einzelner tactics folgt eine Formel, die von der {\tt me} ausgegeben wird, und die darauf folgende tactic gilt. Der proof ist beendet, sobald die {\tt me} {\tt End\_Proof} als n\"achste tactic vorschl\"agt.
1.657 +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.
1.658 \newline Im Anschluss werden Sie einen Rechenbeweis sehen, der von der L\"osung einer Gleichung (= equation) handelt, bei der diese automatisch differenziert wird.
1.659 {\footnotesize\begin{verbatim}
1.660 ??????????????????????????????????????????????????????????????????????????????????
1.661 @@ -809,8 +801,8 @@
1.662 \end{verbatim}
1.663
1.664 \section{Der Beginn einer Rechnung}
1.665 -Um einen neuen proof beginnen zu k\"onnen, werden folgende Schritte durchgef\"uhrt:
1.666 -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.
1.667 +
1.668 +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:
1.669 \footnotesize\begin{verbatim}
1.670 ????????????????????????????????????????????????????????????????????????????????????????????
1.671 ML> val (mID,m) = ("Init_Proof",Init_Proof (fmz, (dom,pbt,met)));
1.672 @@ -831,7 +823,7 @@
1.673 {branch=#,cell=#,env=#,loc=#,meth=#,model=#,origin=#,ostate=#,probl=#,
1.674 result=#,spec=#},[]) : ptree
1.675 \end{verbatim}
1.676 -Die mathematics engine gibt etwas mit dem type {\tt mout} aus, was in unserem Fall ein Problem darstellt. Sobald die Schriftgr\"osse ge\"andert wird, m\"usste dieses jedoch gel\"ost sein.
1.677 +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.
1.678 \footnotesize\begin{verbatim}
1.679 ?????????????????????????????????????????????????????????????????????????????????????????????
1.680 ML> Compiler.Control.Print.printDepth:=8; (*4 default*)
1.681 @@ -861,7 +853,7 @@
1.682 \end{verbatim}
1.683
1.684 \section{The phase of modeling}
1.685 -Dieses Kapitel besch\"aftigt sich mit dem input der Einzelheiten bei einem Problem. Die {\tt me} kann dabei helfen, wenn man die formalization durch {\tt Init\_Proof} darauf hinweist. Normalerweise weiss die mathematic engine die n\"achste gute tactic.
1.686 +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.
1.687 {\footnotesize\begin{verbatim}
1.688 ?????????????????????????????????????????????????????????????????????????????????????????????
1.689 ML> nxt;
1.690 @@ -894,7 +886,7 @@
1.691
1.692
1.693 \section{The phase of specification}
1.694 -Diese phase liefert eindeutige Bestimmungen einer Domäne, 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.
1.695 +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.
1.696 {\footnotesize\begin{verbatim}
1.697 ??????????????????????????????????????????????????????????????????????????????????????????
1.698 ML> nxt;
1.699 @@ -910,7 +902,7 @@
1.700 {branch=#,cell=#,env=#,loc=#,meth=#,model=#,origin=#,ostate=#,probl=#,
1.701 result=#,spec=#},[]) : ptree
1.702 \end{verbatim}
1.703 -Die {\tt me} erkennt den richtigen Problem type und arbeitet so weiter:
1.704 +Die me erkennt den richtigen Problem type und arbeitet so weiter:
1.705 {\footnotesize\begin{verbatim}
1.706 ?????????????????????????????????????????????????????????????????????????????????????????
1.707 ML> val nxt = ("Specify_Problem",
1.708 @@ -997,7 +989,7 @@
1.709
1.710
1.711 \section{The phase of solving}
1.712 -Diese phase beginnt mit dem Aufruf einer method, die eine normale form innarhalb einer tactic ausf\"uhrt: {\tt Rewrite rnorm\_equation\_add} and {\tt Rewrite\_Set SqRoot\_simplify}:
1.713 +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}:
1.714 {\footnotesize\begin{verbatim}
1.715 ML> nxt;
1.716 val it = ("Apply_Method",Apply_Method ("SqRoot.thy","norm_univar_equation"))
1.717 @@ -1020,7 +1012,7 @@
1.718 val f = Form' (FormKF (~1,EdUndef,1,Nundef,"#-6 + #3 * x = #0")) : mout
1.719 val nxt = ("Subproblem",Subproblem ("SqRoot.thy",[#,#])) : string * mstep
1.720 \end{verbatim}
1.721 -Die Formel $-6 + 3 * x = 0$ ist die Eingabe eine subproblems, das wiederum gebraucht wird, um die Gleichungsart zu erkennen und die entsprechende method auszuf\"uhren:
1.722 +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:
1.723 {\footnotesize\begin{verbatim}
1.724 ML> nxt;
1.725 val it = ("Subproblem",Subproblem ("SqRoot.thy",["univariate","equation"]))
1.726 @@ -1039,7 +1031,7 @@
1.727 Nun folgt erneut die phase of modeling und die phase of specification.
1.728
1.729 \section{The final phase: \"Uberpr\"ufung der ''post-condition``}
1.730 -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 in diesem Zusammenhang noch offene Fragen.
1.731 +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.
1.732 Dadurch wird die post-condition im folgenden Beispiel als problem und subproblem erw\"ahnt.
1.733 {\footnotesize\begin{verbatim}
1.734 ML> nxt;
1.735 @@ -1056,15 +1048,15 @@
1.736 \end{verbatim}
1.737 Die tactic {\tt End\_Proof'} bedeutet, dass der proof erflogreich beendet wurde.\\
1.738
1.739 -{\it 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. Man sollte unbedingt selbst verschiedene Beispiele ausprobieren!}
1.740 +\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.
1.741
1.742
1.743 -\part{Systematische Beschreibung}
1.744 +\part{Handbuch f\"ur Autoren}
1.745
1.746 \chapter{Die Struktur des Grundlagenwissens}
1.747
1.748 -\section{Taktiken und Daten}
1.749 -Zuerst betrachten wir das ME von außen. Wir sehen uns Taktiken 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.
1.750 +\section{''tactics`` und Daten}
1.751 +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.
1.752 Diese Teile sind in alphabetischer Anordnung in Tab.\ref{kb-items} auf Seite \pageref{kb-items} aufgelistet.
1.753
1.754 {\begin{table}[h]
1.755 @@ -1077,31 +1069,31 @@
1.756 \hline
1.757 &\\
1.758 {\it calc\_list}
1.759 -& gesammelte Liste von allen ausgewerteten Funktionen {\it eval\_fn}\\
1.760 +& gesammelte Liste von allen ausgewerteten Funktionen\\
1.761 {\it eval\_fn}
1.762 -& ausgewertete Funktionen f\"r Zahlen und f\"ur Eigenschaften, die in SML kodiert sind\\
1.763 +& ausgewertete Funktionen f\"ur Zahlen und f\"ur Eigenschaften, die in SML kodiert sind\\
1.764 {\it eval\_rls }
1.765 -& Regelsatz {\it rls} f\"ur einfache Ausdr\"ucke mit {\it eval\_fn}s\\
1.766 +& rule set {\it rls} f\"ur einfache Ausdr\"ucke mit {\it eval\_fn}s\\
1.767 {\it fmz}
1.768 & Formalisierung, d.h. eine sehr geringe Darstellung von einem Beispiel \\
1.769 {\it met}
1.770 -& eine Methode d.h. eine Datenstruktur, die alle Informationen zum L\"osen einer Phase enth\"alt ({\it rew\_ord}, {\it scr}, etc.)\\
1.771 +& eine method d.h. eine Datenstruktur, die alle Informationen zum L\"osen einer phase enth\"alt ({\it rew\_ord}, {\it scr}, etc.)\\
1.772 {\it metID}
1.773 & bezieht sich auf {\it met}\\
1.774 {\it op}
1.775 & ein Operator, der der Schl\"ussel zu {\it eval\_fn} in einer {\it calc\_list} ist \\
1.776 {\it pbl}
1.777 -& Problem d.h. der Knotenpunkt in der Hierarchie von Problemen\\
1.778 +& Problem d.h. der Knotenpunkt in der problem hierachy\\
1.779 {\it pblID}
1.780 & bezieht sich auf {\it pbl}\\
1.781 {\it rew\_ord}
1.782 & Anordnung beim Rewriting\\
1.783 {\it rls}
1.784 -& Regelsatz, d.h. eine Datenstruktur, die Theoremss {\it thm} und Operatoren {\it op} zur Vereinfachuing (mit {\it rew\_ord}) enth\"alt \\
1.785 +& rule set, d.h. eine Datenstruktur, die theorems {\it thm} und Operatoren {\it op} zur Vereinfachung (mit {\it rew\_ord}) enth\"alt \\
1.786 {\it Rrls}
1.787 -& Regelsatz f\"ur das 'reverse rewriting' (eine \isac-Technik, die das schrittweise Rewriting entwickelt, z.B. f\"ur die zur\"uckgenommenen Teile)\\
1.788 +& rule set f\"ur das 'reverse rewriting' (eine \isac-Technik, die schrittweise Rewriting entwickelt, z.B. f\"ur die zur\"uckgenommenen Teile)\\
1.789 {\it scr}
1.790 -& Skript, das die Algorithmen durch Anwenden von Taktiken beschreibt und ein Teil von {\it met} ist \\
1.791 +& script, das die Algorithmen durch Anwenden von tactics beschreibt und ein Teil von {\it met} ist \\
1.792 {\it norm\_rls}
1.793 & spezielles Regelwerk zum Berechnen von Normalformen, im Zusammenhang mit {\it thy}\\
1.794 {\it spec}
1.795 @@ -1113,20 +1105,20 @@
1.796 {\it thm}
1.797 & theorem\\
1.798 {\it thy}
1.799 -& Theorie\\
1.800 +& theory\\
1.801 {\it thyID}
1.802 & im Bezug auf {\it thy} \\
1.803 \end{tabular}\end{center}\end{table}}
1.804
1.805 -Die Verbindung zwischen Taktiken und Daten werden in Tab.\ref{tac-kb} auf Seite \pageref{tac-kb} dargestellt.
1.806 +Die Verbindung zwischen tactics und Daten werden in Tab.\ref{tac-kb} auf Seite \pageref{tac-kb} dargestellt.
1.807
1.808
1.809 \begin{table}[h]
1.810 -\caption{Welche Taktiken verwenden die Teile des KB~?} \label{tac-kb}
1.811 +\caption{Welche tactics verwenden die Teile des KB~?} \label{tac-kb}
1.812 \tabcolsep=0.3mm
1.813 \begin{center}
1.814 \begin{tabular}{|ll||cccc|ccc|cccc|} \hline
1.815 -Taktik &Eingabe & & & &norm\_& &rew\_&rls &eval\_&eval\_&calc\_& \\
1.816 +tactic &Eingabe & & & &norm\_& &rew\_&rls &eval\_&eval\_&calc\_& \\
1.817 & &thy &scr &Rrls&rls &thm &ord &Rrls&fn &rls &list &dsc\\
1.818 \hline\hline
1.819 Init\_Proof
1.820 @@ -1175,22 +1167,22 @@
1.821
1.822
1.823 \section{Die theories von \isac{}}
1.824 -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} definiert sind; normalerweise werden diese theories zusammen mit SML verwendet, und dann haben sie den selben Dateinamen, aber die Endung {\tt *.ML}.
1.825 -Die theories von \isac{} representieren den folgenden Teil vom Basiswissen von \isac{}, die Hierarchie von den zwei theories ist demnach strukturiert. Die {\tt *.ML} Dateien beinhalten {\em alle} Daten von den anderen zwei Hauptlinien des Basiswissens, die Probleme und die Methoden(ohne ihre jeweilige Struktur, die von den Problem Browsern und den Methode Browsern gemacht wird, zu pr\"asentieren.
1.826 -Die Tab.\ref{theories} auf Seite \pageref{theories} listet die basis 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.
1.827 -Die ersten drei theories auf der Liste geh\"oren {\em nicht} zum Grundwissen von \isac{}; sie besch\"aftigen sich mit der Skriptsprache f\"ur Methoden und ist hier nur zur Vollst\"andigkeit angef\"uhrt.
1.828 +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}.
1.829 +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.
1.830 +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.
1.831 +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.
1.832
1.833 {\begin{table}[h]
1.834 -\caption{Theorien von der ersten Version von \isac} \label{theories}
1.835 +\caption{theory von der ersten Version von \isac} \label{theories}
1.836 %\tabcolsep=0.3mm
1.837 \begin{center}
1.838 \def\arraystretch{1.0}
1.839 \begin{tabular}{lp{9.0cm}}
1.840 -Theorie & Beschreibung \\
1.841 +theory & Beschreibung \\
1.842 \hline
1.843 &\\
1.844 ListI.thy
1.845 -& ordnet die Bezeichnungen den Funktionen, die in {\tt Isabelle2002/src/HOL/List.thy} sind zu, und (intermediatly~?) definiert einige weitere Listen von Funktionen\\
1.846 +& ordnet die Bezeichnungen den Funktionen, die in {\tt Isabelle2002/src/HOL/List.thy} sind, zu und (intermediatly~?) definiert einige weitere Listen von Funktionen\\
1.847 ListI.ML
1.848 & {\tt eval\_fn} f\"ur die zus\"atzliche Listen von Funktionen\\
1.849 Tools.thy
1.850 @@ -1198,9 +1190,9 @@
1.851 Tools.ML
1.852 & bezieht sich auf {\tt eval\_fn}s\\
1.853 Script.thy
1.854 -& Vorraussetzung f\"ur Skripten: Typen, Taktiken, tacticals\\
1.855 +& Vorraussetzung f\"ur script: types, tactics, tacticals\\
1.856 Script.ML
1.857 -& eine Reihe von Taktiken und Funktionen f\"ur den internen Gebrauch\\
1.858 +& eine Reihe von tactics und Funktionen f\"ur den internen Gebrauch\\
1.859 & \\
1.860 \hline
1.861 & \\
1.862 @@ -1209,7 +1201,7 @@
1.863 Descript.thy
1.864 & {\it Beschreibungen} f\"ur die Formeln von {\it Modellen} und {\it Problemen}\\
1.865 Atools
1.866 -& Neudefinierung von Operatoren; allgemeine Eigenschaften und Funktionen f\"ur Vorraussetzungen; Theorems f\"ur {\tt eval\_rls}\\
1.867 +& Neudefinierung von Operatoren; allgemeine Eigenschaften und Funktionen f\"ur Vorraussetzungen; theorems f\"ur {\tt eval\_rls}\\
1.868 Float
1.869 & Gleitkommerzahlendarstellung\\
1.870 Equation
1.871 @@ -1219,7 +1211,7 @@
1.872 PolyEq
1.873 & polynomiale Gleichungen und Gleichungssysteme \\
1.874 Rational.thy
1.875 -& zus\"atzliche Theorems f\"ur Rationale Zahlen\\
1.876 +& zus\"atzliche theorems f\"ur Rationale Zahlen\\
1.877 Rational.ML
1.878 & abbrechen, hinzuf\"ugen und vereinfachen von Rationalen Zahlen durch Verwenden von (einer allgemeineren Form von) Euclids Algorithmus; die entsprechenden umgekehrten Regels\"atze\\
1.879 RatEq
1.880 @@ -1250,8 +1242,8 @@
1.881
1.882
1.883 \section{Daten in {\tt *.thy} und {\tt *.ML}}
1.884 -Wie schon zuvor angesprochen, haben die arbeiten die theories von *.thy und *.ML zusamnmen und haben deswegen den selben Dateiname. Wie diese Daten zwischen den zwei Dateien verteilt werden wird in der
1.885 -Tab.\ref{thy-ML} auf Seite \pageref{thy-ML} gezeigt. Die Ordnung von den Dateinteilchen in den theories sollte an der Ordnung von der Liste festhalten.
1.886 +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
1.887 +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.
1.888
1.889 {\begin{table}[h]
1.890 \caption{Daten in {\tt *.thy}- und {\tt *.ML}-files} \label{thy-ML}
1.891 @@ -1267,20 +1259,21 @@
1.892 & Operatoren, Eigenschaften, Funktionen und Skriptnamen ('{\tt Skript} Name \dots{\tt Argumente}')
1.893 \\
1.894 & rules
1.895 -& theorems: \isac{} verwendet die Theorems von Isabelle, wenn m\"oglich; zus\"atzliche Theorems, die jenen von Isabelle entsprechen, bekommen ein {\it I} angeh\"angt
1.896 +& theorems: \isac{} verwendet theorems von Isabelle, wenn m\"oglich; zus\"atzliche theorems, die jenen von Isabelle entsprechen, bekommen ein {\it I} angeh\"angt
1.897 \\& &\\
1.898 {\tt *.ML}
1.899 & {\tt theory' :=}
1.900 -& Die Theorie, die
1.901 +& Die theory, die
1.902 abgegrenzt ist von der {\tt *.thy}-Datei, wird durch \isac{} zug\"anglich gemacht
1.903 \\
1.904 & {\tt eval\_fn}
1.905 -& 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\\
1.906 +& 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
1.907 +\\
1.908 & {\tt *\_simplify}
1.909 & 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}
1.910 \\
1.911 & {\tt norm\_rls :=}
1.912 -& der automatisierte Vereinfacherthe {\tt *\_simplify} wird so aufgehoben, dass er \"uber \isac zug\"anglich ist
1.913 +& der automatisierte Vereinfacher {\tt *\_simplify} wird so aufgehoben, dass er \"uber \isac{} zug\"anglich ist
1.914 \\
1.915 & {\tt rew\_ord' :=}
1.916 & das Gleiche f\"ur die Anordnung des Rewriting, wenn es ausserhalb eines speziellen Regelwerks gebraucht wird
1.917 @@ -1289,20 +1282,20 @@
1.918 & dasselbe wie f\"ur Regels\"atze (gew\"ohnliche Regels\"atze, umgekehrte Regels\"atze, und {\tt eval\_rls})
1.919 \\
1.920 & {\tt calc\_list :=}
1.921 -& 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 Taktik {\tt Calculate} in einem Skript)
1.922 +& 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)
1.923 \\
1.924 & {\tt store\_pbl}
1.925 -& Probleme, die in {\tt *.ML}-Dateien definiert sind, werden zug\"anglich f\"ur \isac{}
1.926 +& Problems, die in {\tt *.ML}-Dateien definiert sind, werden zug\"anglich f\"ur \isac{}
1.927 \\
1.928 & {\tt methods :=}
1.929 -& Methoden, die in {\tt *.ML}-Dateien definiert sind werden zug\"anglich f\"ur \isac{}
1.930 +& methods, die in {\tt *.ML}-Dateien definiert sind werden zug\"anglich f\"ur \isac{}
1.931 \\
1.932 \end{tabular}\end{center}\end{table}}
1.933
1.934 \section{Formale Beschreibung der Hierarchie von Problemen}
1.935
1.936 \section{Skripttaktiken}
1.937 -Tats\"achlich sind es die Taktiken, die die Berechnungen vorantreiben: im Hintergrund bauen sie den ''Prooftree`` 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 den Taktiken; die Semantik ist beschrieben etwas weiter unten im Kontext mit den Taktiken, die die Benutzer/Innen dieses Programmes verwenden: da gibt es einen Schriftverkehr zwischen den Benutzer Taktiken und den Skripttaktiken.
1.938 +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.
1.939
1.940
1.941