1.1 --- a/.hgignore Fri Jul 23 11:45:15 2010 +0200
1.2 +++ b/.hgignore Mon Jul 26 14:46:45 2010 +0200
1.3 @@ -21,6 +21,8 @@
1.4 ^doc-src/.*\.lof
1.5 ^doc-src/.*\.log
1.6 ^doc-src/.*\.out
1.7 +^doc-src/.*\.pdf
1.8 +^doc-src/.*\.tex.backup
1.9 ^doc-src/.*\.rai
1.10 ^doc-src/.*\.rao
1.11 ^doc-src/.*\.toc
2.1 --- a/doc-src/isac/mat-eng-de.tex Fri Jul 23 11:45:15 2010 +0200
2.2 +++ b/doc-src/isac/mat-eng-de.tex Mon Jul 26 14:46:45 2010 +0200
2.3 @@ -1,5 +1,6 @@
2.4 \documentclass[11pt,a4paper,headline,headcount,towside,nocenter]{report}
2.5 \usepackage{latexsym}
2.6 +
2.7 %\usepackage{ngerman}
2.8 %\grmn@dq@error ...and \dq \string #1 is undefined}
2.9 %l.989 ...tch the problem type \\{\tt["squareroot",
2.10 @@ -344,742 +345,187 @@
2.11 val ct = "d_d x a + a * d_d x (2 + b)" : cterm'
2.12 \end{verbatim}
2.13
2.14 +{\section{M\"oglichkeiten von Rewriting}
2.15 +Es gibt verscheidene Varianten von Rewriting, die alle eine bestimmte Bedeutung haben.
2.16 +\textit{rewrite\_inst} bedeutet, dass die Liste der Terme vor dem Rewriting durch ein ''Theorem`` (ein mathematischer Begriff f\"ur einen Satz) ersetzt wird.
2.17 +{\footnotesize\begin{verbatim}
2.18 +> rewrite_inst;
2.19 +val it = fn
2.20 +:
2.21 + theory' ->
2.22 + rew_ord' ->
2.23 + rls' ->
2.24 + bool -> 'a -> thm' -> cterm' -> (cterm' * cterm' list) Library.option
2.25 +\end{verbatim}
2.26 +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.
2.27 +{\footnotesize\begin{verbatim}
2.28 + > rewrite_set;
2.29 + val it = fn
2.30 + : theory' -> bool -> rls' -> cterm' -> (string * string list) Library.option
2.31 +\end{verbatim}
2.32 +\textit{rewrite\_set\_inst} ist eine Kombination der beiden oben genannten M\"oglichkeiten.
2.33 +{\footnotesize\begin{verbatim}
2.34 + > rewrite_set_inst;
2.35 + val it = fn
2.36 + :
2.37 + theory' ->
2.38 + bool -> subs' -> rls' -> cterm' -> (string * string list) Library.option
2.39 +\end{verbatim}
2.40 +Wenn man sehen m\"ochte, wie Rewriting bei den einzelnen Theorems funktioniert, kann man dies mit \textit{trace\_rewrite} versuchen.
2.41 +{\footnotesize\begin{verbatim}
2.42 + > toggle;
2.43 + val it = fn : bool ref -> bool
2.44 + > toggle trace_rewrite;
2.45 + val it = true : bool
2.46 + > toggle trace_rewrite;
2.47 + val it = false : bool
2.48 +\end{verbatim}
2.49 +
2.50 +\section{Rule sets}
2.51 +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.
2.52 +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.
2.53 +Ein Beispiel f\"ur einen Regelsatz ist folgendes:
2.54 +\footnotesize\begin{verbatim}
2.55 +???????????
2.56 +\end{verbatim}
2.57
2.58 +\footnotesize\begin{verbatim}
2.59 + > sym;
2.60 + val it = "?s = ?t ==> ?t = ?s" : Thm.thm
2.61 + > rearrange_assoc;
2.62 + val it =
2.63 + Rls
2.64 + {id = "rearrange_assoc",
2.65 + scr = Script (Free ("empty_script", "RealDef.real")),
2.66 + calc = [],
2.67 + erls =
2.68 + Rls
2.69 + {id = "e_rls",
2.70 + scr = EmptyScr,
2.71 + calc = [],
2.72 + erls = Erls,
2.73 + srls = Erls,
2.74 + rules = [],
2.75 + rew_ord = ("dummy_ord", fn),
2.76 + preconds = []},
2.77 + srls =
2.78 + Rls
2.79 + {id = "e_rls",
2.80 + scr = EmptyScr,
2.81 + calc = [],
2.82 + erls = Erls,
2.83 + srls = Erls,
2.84 + rules = [],
2.85 + rew_ord = ("dummy_ord", fn),
2.86 + preconds = []},
2.87 + rules =
2.88 + [Thm ("sym_radd_assoc", "?m1 + (?n1 + ?k1) = ?m1 + ?n1 + ?k1" [.]),
2.89 + Thm
2.90 + ("sym_rmult_assoc",
2.91 + "?m1 * (?n1 * ?k1) = ?m1 * ?n1 * ?k1" [.])],
2.92 + rew_ord = ("e_rew_ord", fn),
2.93 + preconds = []} : rls
2.94 +\end{verbatim}
2.95
2.96
2.97 +\section{Berechnung von Konstanten}
2.98 +Sobald Konstanten in dem Bereich des Subterms sind, k\"onnen sie von einer Funktion berechnet werden:
2.99 +\footnotesize\begin{verbatim}
2.100 + > calculate;
2.101 + val it = fn
2.102 + :
2.103 + theory' ->
2.104 + string *
2.105 + (
2.106 + string ->
2.107 + Term.term -> Theory.theory -> (string * Term.term) Library.option) ->
2.108 + cterm' -> (string * thm') Library.option
2.109
2.110 + > calculate_;
2.111 + val it = fn
2.112 + :
2.113 + Theory.theory ->
2.114 + string *
2.115 + (
2.116 + string ->
2.117 + Term.term -> Theory.theory -> (string * Term.term) Library.option) ->
2.118 + Term.term -> (Term.term * (string * Thm.thm)) Library.option
2.119 +\end{verbatim}
2.120 +Man bekommt das Ergebnis und die Theorem bezieht sich darauf. Daher sind die folgenden mathematischen Rechnungen m\"oglich:
2.121 +\footnotesize\begin{verbatim}
2.122 + > calclist;
2.123 + val it =
2.124 + [("Vars", ("Tools.Vars", fn)), ("matches", ("Tools.matches", fn)),
2.125 + ("lhs", ("Tools.lhs", fn)), ("plus", ("op +", fn)),
2.126 + ("times", ("op *", fn)), ("divide_", ("HOL.divide", fn)),
2.127 + ("power_", ("Atools.pow", fn)), ("is_const", ("Atools.is'_const", fn)),
2.128 + ("le", ("op <", fn)), ("leq", ("op <=", fn)),
2.129 + ("ident", ("Atools.ident", fn)), ("sqrt", ("Root.sqrt", fn)),
2.130 + ("Test.is_root_free", ("is'_root'_free", fn)),
2.131 + ("Test.contains_root", ("contains'_root", fn))]
2.132 + :
2.133 + (
2.134 + string *
2.135 + (
2.136 + string *
2.137 + (
2.138 + string ->
2.139 + Term.term -> Theory.theory -> (string * Term.term) Library.option))) list
2.140 +\end{verbatim}
2.141 +Diese werden so angewendet:
2.142 +\footnotesize\begin{verbatim}
2.143 +\end{verbatim}
2.144
2.145
2.146
2.147 +\chapter{Termordnung}
2.148 +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.
2.149 +
2.150 +\section{Beispiel f\"ur Termordnungen}
2.151 +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.
2.152 +Hier ein Beispiel:
2.153 +
2.154 +{\footnotesize\begin{verbatim}
2.155 + > sqrt_right;
2.156 + val it = fn : bool -> Theory.theory -> subst -> Term.term * Term.term -> b ool
2.157 + > tless_true;
2.158 + val it = fn : subst -> Term.term * Term.term -> bool
2.159 +\end{verbatim}
2.160 +
2.161 +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.
2.162 +
2.163 +
2.164 +\chapter{Methods}
2.165 +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.
2.166 +
2.167 +\section{Der ''Syntax`` des Scriptes}
2.168 +Syntax beschreibt den Zusammenhang der einzelnen Zeichen und Zeichenfolgen mit den Theorien.
2.169 +Er kann so definiert werden:
2.170 +\begin{tabbing}
2.171 +123\=123\=expr ::=\=$|\;\;$\=\kill
2.172 +\>script ::= {\tt Script} id arg$\,^*$ = body\\
2.173 +\>\>arg ::= id $\;|\;\;($ ( id :: type ) $)$\\
2.174 +\>\>body ::= expr\\
2.175 +\>\>expr ::= \>\>{\tt let} id = expr $($ ; id = expr$)^*$ {\tt in} expr\\
2.176 +\>\>\>$|\;$\>{\tt if} prop {\tt then} expr {\tt else} expr\\
2.177 +\>\>\>$|\;$\>listexpr\\
2.178 +\>\>\>$|\;$\>id\\
2.179 +\>\>\>$|\;$\>seqex id\\
2.180 +\>\>seqex ::= \>\>{\tt While} prop {\tt Do} seqex\\
2.181 +\>\>\>$|\;$\>{\tt Repeat} seqex\\
2.182 +\>\>\>$|\;$\>{\tt Try} seqex\\
2.183 +\>\>\>$|\;$\>seqex {\tt Or} seqex\\
2.184 +\>\>\>$|\;$\>seqex {\tt @@} seqex\\
2.185 +\>\>\>$|\;$\>tac $($ id $|$ listexpr $)^*$\\
2.186 +\>\>type ::= id\\
2.187 +\>\>tac ::= id
2.188 +\end{tabbing}}
2.189
2.190
2.191
2.192 \newpage
2.193 ------------------------------- ALTER TEXT -------------------------------
2.194
2.195 -Ein Term ist eine Zeichenfolge. Das heisst Es gibt zwei Arten von Termen in Isabelle, 'raw terms' und 'certified terms'. \isac{} arbeitet mit raw terms, die effizient sind.
2.196 -{\footnotesize\begin{verbatim}
2.197 - datatype term =
2.198 - Const of string * typ
2.199 - | Free of string * typ
2.200 - | Var of indexname * typ
2.201 - | Bound of int
2.202 - | Abs of string * typ * term
2.203 - | op $ of term * term;
2.204 -
2.205 - datatype typ = Type of string * typ list
2.206 - | TFree of string * sort
2.207 - | TVar of indexname * sort;
2.208 -\end{verbatim}}%size % $
2.209 -Die Definition und der Indexname sind in diesem Zusammenhang nicht relevant. Der {\tt typ}e wird w\"ahrend der Parse angedeutet. Diese ist der Hauptbestandteil f\"ur andere Terms, {\tt cterm}. Sie {\tt cterm}s sind zusammengefasste Aufzeichnungen, die ohne die jeweiligen Isabelle-Funktionen nicht zusammengesetzt werden k\"onnen (type--Richtigkeit \"Uberpr\"ufen), aber dann g\"unstig als string dargestellt werden (Verwendung von SML Compiler Internals -- siehe unten).
2.210 -
2.211 -\section{Theorien und Terme}
2.212 -Die Parse verwendet Informationen, die in der Theorie von Isabelle $\sim${\tt /src/HOL}enthalten sind. Die derzeitige Theorie wird international als {\tt thy} gekennzeichnet; auf diese kann unterschiedlich zugegriffen werden.
2.213 -{\footnotesize\begin{verbatim}
2.214 - ML> thy;
2.215 - val it =
2.216 - {ProtoPure, CPure, HOL, Set, Typedef, Fun, Product_Type, Lfp, Gfp,
2.217 - Sum_Type, Relation, Record, Inductive, Transitive_Closure,
2.218 - Wellfounded_Recursion, NatDef, Nat, NatArith, Divides, Power,
2.219 - SetInterval, Finite_Set, Equiv, IntDef, Int, Datatype_Universe,
2.220 - Datatype, Numeral, Bin, IntArith, Wellfounded_Relations, Recdef, IntDiv,
2.221 - IntPower, NatBin, NatSimprocs, Relation_Power, PreList, List, Map,
2.222 - Hilbert_Choice, Main, Lubs, PNat, PRat, PReal, RealDef, RealOrd,
2.223 - RealInt, RealBin, RealArith0, RealArith, RComplete, RealAbs, RealPow,
2.224 - Ring_and_Field, Complex_Numbers, Real, ListG, Tools, Script, Typefix,
2.225 - Float, ComplexI, Descript, Atools, Simplify, Poly, Rational, PolyMinus,
2.226 - Equation, LinEq, Root, RootEq, RatEq, RootRat, RootRatEq, PolyEq, Vect,
2.227 - Calculus, Trig, LogExp, Diff, DiffApp, Integrate, EqSystem, Biegelinie,
2.228 - AlgEin, Test, Isac} : Theory.theory
2.229 - ML> HOL.thy;
2.230 - val it = {ProtoPure, CPure, HOL} : Theory.theory
2.231 - ML>
2.232 - ML> parse;
2.233 - val it = fn : Theory.theory -> string -> Thm.cterm Library.option
2.234 - ML> parse thy "a + b * 3";
2.235 - val it = Some "a + b * 3" : Thm.cterm Library.option
2.236 - ML>
2.237 - ML> val t = (term_of o the) it;
2.238 - val t =
2.239 - Const ("op +", "[RealDef.real, RealDef.real] => RealDef.real") $
2.240 - Free ("a", "RealDef.real") $
2.241 - (Const ("op *", "[RealDef.real, RealDef.real] => RealDef.real") $ ... $
2.242 - ...) : Term.term
2.243 -
2.244 -\end{verbatim}}%size
2.245 -Die Ausdr\"ucke {\tt term\_of} und {\tt the} werden weiter unten erkl\"art. Den Syntax aus der Liste der Funktionen kann man aus den Theorien von Isabelle \cite{Isa-obj} {\tt [isabelle]/src/HOL/}\footnote{Oder Sie schauen ins Internet unter {\tt [isabelle]/browser\_info}.} und aus den entwickelten Theorien von \isac{} unter {\tt [isac-src]/knowledge/} herauslesen. Beachten Sie, dass der Syntax von diesem Ausdruck anders ist, als jene die bei \isac vom Vorrechner nach der Umrechnung zu MathML angezeigt werden.
2.246 -
2.247 -
2.248 -\section{Anzeigen von Termen}
2.249 -Die Drucktiefe auf der höchsten Ebene des SML kann in Ordnung gebracht werden, um den output in der Menge des gewünschten Details zu erzeugen:
2.250 -{\footnotesize\begin{verbatim}
2.251 - ML> Compiler.Control.Print.printDepth;
2.252 - val it = ref 4 : int ref
2.253 - ML>
2.254 - ML> Compiler.Control.Print.printDepth:= 2;
2.255 - val it = () : unit
2.256 - ML> t;
2.257 - val it =
2.258 - Const ("op +", "[RealDef.real, RealDef.real] => RealDef.real") $
2.259 - Free ("a", "RealDef.real") $
2.260 - (Const ("op *", "[RealDef.real, RealDef.real] => RealDef.real") $ ... $
2.261 - ...) : Term.term
2.262 - ML>
2.263 - ML> Compiler.Control.Print.printDepth:= 6;
2.264 - val it = () : unit
2.265 - ML> t;
2.266 - val it =
2.267 - Const ("op +","[RealDef.real, RealDef.real] => RealDef.real") $
2.268 - Free ("a","RealDef.real") $
2.269 - (Const ("op *","[RealDef.real, RealDef.real] => RealDef.real") $
2.270 - Free ("b","RealDef.real") $ Free ("#3","RealDef.real")) : term
2.271 -\end{verbatim}}%size % $
2.272 -Ein n\"aherer Blick zum letzten output zeigt, dass {\tt typ} wie der string {\tt cterm} ausgegeben worden ist. Andere n\"utzliche Einstellungen für den output sind:
2.273 -{\footnotesize\begin{verbatim}
2.274 - ML> Compiler.Control.Print.printLength;
2.275 - val it = ref 8 : int ref
2.276 - ML> Compiler.Control.Print.stringDepth;
2.277 - val it = ref 250 : int ref
2.278 -\end{verbatim}}%size
2.279 -Die SML der Terme ist nicht lesbar; es gibt Funktionen im KE, um sie zu zeigen:
2.280 -{\footnotesize\begin{verbatim}
2.281 - ML> atomt;
2.282 - val it = fn : Term.term -> string
2.283 - ML> atomt t;
2.284 - "*** -------------"
2.285 - "*** Const (op +)"
2.286 - "*** . Free (a, )"
2.287 - "*** . Const (op *)"
2.288 - "*** . . Free (b, )"
2.289 - "*** . . Free (3, )"
2.290 - "\n"
2.291 -val it = "\n" : string
2.292 - ML>
2.293 - ML> atomty;
2.294 - val it = fn : Term.term -> unit
2.295 - ML> atomty thy t;
2.296 - *** -------------
2.297 - *** Const ( op +, [real, real] => real)
2.298 - *** . Free ( a, real)
2.299 - *** . Const ( op *, [real, real] => real)
2.300 - *** . . Free ( b, real)
2.301 - *** . . Free ( #3, real)
2.302 - val it = () : unit
2.303 -\end{verbatim}}%size
2.304 -{\tt typ} wird als string wiedergegeben. Diesaml aber durch die Informationen von {\tt thy} in besserer Darstellung.
2.305 -
2.306 -\paragraph{Versuchen Sie es!} {\bf Das mathematische Wissen w\"achst} wie es in Isabelle schrittweise beschrieben ist. Schauen Sie ins Internet um diese Beschreibungen aufzurufen {\tt [isabelle]/src/HOL/HOL.thy} und zu sehen, ob es Kindern auf Ihrem System zur Verf\"ugung steht. Oder Sie sehen sich die verschiedenen Dateien unter {\tt [isabelle]/browser\_info} an.
2.307 -{\footnotesize\begin{verbatim}
2.308 - ML> (*-1-*) parse HOL.thy "#2^^^#3";
2.309 - *** Inner lexical error at: "^^^3"
2.310 - val it = None : Thm.cterm Library.option
2.311 - ML>
2.312 - ML> (*-2-*) parse HOL.thy "d_d x (a + x)";
2.313 - val it = None : Thm.cterm Library.option
2.314 - ML>
2.315 - ML>
2.316 - ML> (*-3-*) parse RatArith.thy "#2^^^#3";
2.317 - val it = Some "#2 ^^^ #3" : cterm option
2.318 - ML>
2.319 - ML> (*-4-*) parse RatArith.thy "d_d x (a + x)";
2.320 - val it = Some "d_d x (a + x)" : cterm option
2.321 - ML>
2.322 - ML>
2.323 - ML> (*-5-*) parse Differentiate.thy "d_d x (a + x)";
2.324 - val it = Some "d_d x (a + x)" : cterm option
2.325 - ML>
2.326 - ML> (*-6-*) parse Differentiate.thy "#2^^^#3";
2.327 - val it = Some "#2 ^^^ #3" : cterm option
2.328 -\end{verbatim}}%size
2.329 -Vertrauen sie nicht der string Darstellung: Wenn wir {\tt(*-4-*)} und {\tt(*-6-*)} zu folgenden Ausdr\"ucken umwandel:\dots
2.330 -{\footnotesize\begin{verbatim}
2.331 - ML> (*-4-*) val thy = RatArith.thy;
2.332 - ML> ((atomty thy) o term_of o the o (parse thy)) "d_d x (a + x)";
2.333 - *** -------------
2.334 - *** Free ( d_d, [real, real] => real)
2.335 - *** . Free ( x, real)
2.336 - *** . Const ( op +, [real, real] => real)
2.337 - *** . . Free ( a, real)
2.338 - *** . . Free ( x, real)
2.339 - val it = () : unit
2.340 - ML>
2.341 - ML> (*-6-*) val thy = Differentiate.thy;
2.342 - ML> ((atomty thy) o term_of o the o (parse thy)) "d_d x (a + x)";
2.343 - *** -------------
2.344 - *** Const ( Differentiate.d_d, [real, real] => real)
2.345 - *** . Free ( x, real)
2.346 - *** . Const ( op +, [real, real] => real)
2.347 - *** . . Free ( a, real)
2.348 - *** . . Free ( x, real)
2.349 - val it = () : unit
2.350 -\end{verbatim}}%size
2.351 -\dots Wir sehen: Bei {\tt(*-4-*)} handelt es sich um eine willk\"urliche Funktion {\tt Free ( d\_d, \_)} und bei {\tt(*-6-*)} um eine spezielle unver\"anderliche Funktion {\tt Const ( Differentiate.d\_d, \_)} für das Differenzieren, welches in {\tt Differentiate.thy} erkl\"art wird und vermutlich gemeint ist.
2.352 -
2.353 -
2.354 -\section{Terme umwandeln}
2.355 -Die Umwandlung von {\tt cterm} zu {\tt term} wurde bereits oberhalb gezeigt:
2.356 -{\footnotesize\begin{verbatim}
2.357 - ML> term_of;
2.358 - val it = fn : Thm.cterm -> Term.term
2.359 - ML>
2.360 - ML> the;
2.361 - val it = fn : 'a Library.option -> 'a
2.362 - ML>
2.363 - ML> val t = (term_of o the o (parse thy)) "a + b * 3";
2.364 - val t = Const (#,#) $ Free (#,#) $ (Const # $ Free # $ Free (#,#)) : term
2.365 -\end{verbatim}}%size
2.366 -{\tt the} wird dabei von {\tt term option} ausgewickelt --- eine hilfreiche Funktion von Larry Paulsons Grundlagen {\tt [isabelle]/src/Pure/library.ML}, die für jeden SML Programmierer sehr wertvoll ist.
2.367 -
2.368 -Die anderen Umwandlungen sind folgende, wobei einige {\it signature} {\tt sign} als Theorie verwenden:
2.369 -{\footnotesize\begin{verbatim}
2.370 - ML> sign_of;
2.371 - val it = fn : theory -> Sign.sg
2.372 - ML>
2.373 - ML> cterm_of;
2.374 - val it = fn : Sign.sg -> term -> cterm
2.375 - ML> val ct = cterm_of (sign_of thy) t;
2.376 - val ct = "a + b * #3" : cterm
2.377 - ML>
2.378 - ML> Sign.string_of_term;
2.379 - val it = fn : Sign.sg -> term -> string
2.380 - ML> Sign.string_of_term (sign_of thy) t;
2.381 - val it = "a + b * #3" : ctem'
2.382 - ML>
2.383 - ML> string_of_cterm;
2.384 - val it = fn : cterm -> string
2.385 - ML> string_of_cterm ct;
2.386 - val it = "a + b * #3" : ctem'
2.387 -\end{verbatim}}%size
2.388 -
2.389 -\section{Lehrs\"atze}
2.390 -Theorems sind types, {\tt thm}, gesch\"utzter als {\tt cterms}: Sie sind als axioms beschrieben und haben sich in Isabelle bew\"ahrt. Diese Definitionen und Beweise sind in den Theorien im Verzeichnis {\tt[isac-src]/knowledge/} enthalten, zum Beispiel der Lehrsatz {\tt diff\_sum} in der Theorie {\tt[isac-src]/knowledge/Differentiate.thy}. Zus\"atzlich muss jeder Lehrsatz für \isac{} im zugeh\"origen {\tt *.ML}, wie etwa {\tt diff\_sum} in {\tt[isac-src]/knowledge/Differentiate.ML} aufgenommen werden, wie das Folgende:
2.391 -{\footnotesize\begin{verbatim}
2.392 - ML> theorem' := overwritel (!theorem',
2.393 - [("diff_const",num_str diff_const)
2.394 - ]);
2.395 -\end{verbatim}}%size
2.396 -The additional recording of theorems and other values will disappear in later versions of \isac.
2.397 -
2.398 -\chapter{Umschreiben}
2.399 -\section{Argumente f\"ur Umschreibungen}
2.400 -Die Bezeichnung des type der Argumente und Werte der Umschreibfunktionen in \ref{rewrite} unterscheiden sich durch ein Apostroph: Die types mit einem Apostroph sind umbenannte strings um die Lesbarkeit aufrecht zu erhalten.
2.401 -{\footnotesize\begin{verbatim}
2.402 - ML> HOL.thy;
2.403 - val it = {ProtoPure, CPure, HOL} : theory
2.404 - ML> "HOL.thy" : theory';
2.405 - val it = "HOL.thy" : theory'
2.406 - ML>
2.407 - ML> sqrt_right;
2.408 - val it = fn : rew_ord (* term * term -> bool *)
2.409 - ML> "sqrt_right" : rew_ord';
2.410 - val it = "sqrt_right" : rew_ord'
2.411 - ML>
2.412 - ML> eval_rls;
2.413 - val it =
2.414 - Rls
2.415 - {preconds=[],rew_ord=("sqrt_right",fn),
2.416 - rules=[Thm #,Thm #,Thm #,Thm #,Thm #,Thm #,Thm #,Thm #,
2.417 - Thm #,Thm #,Thm #,Thm #,Thm #,Calc #,Calc #,...],
2.418 - scr=Script (Free #)} : rls
2.419 - ML> "eval_rls" : rls';
2.420 - val it = "eval_rls" : rls'
2.421 - ML>
2.422 - ML> diff_sum;
2.423 - val it = "d_d ?bdv (?u + ?v) = d_d ?bdv ?u + d_d ?bdv ?v" : thm
2.424 - ML> ("diff_sum", "") : thm';
2.425 - val it = ("diff_sum","") : thm'
2.426 -\end{verbatim}}%size
2.427 -{\tt thm'} ist ein Teil, eventuell mit strin-Darstellung von dem zugeh\"origen Lehrsatz.
2.428 -
2.429 -\section{Die Funktionen des Umschreibens}\label{rewrite}
2.430 -Das Umschreiben wird von zwei equvalenten Funktionen begleitet, wobei die erste im KE verwendet wird und sie zweite n\"utzlich für Tests ist:
2.431 -{\footnotesize\begin{verbatim}
2.432 - ML> rewrite_;
2.433 - val it = fn
2.434 - : theory
2.435 - -> rew_ord
2.436 - -> rls -> bool -> thm -> term -> (term * term list) option
2.437 - ML>
2.438 - ML> rewrite;
2.439 - val it = fn
2.440 - : theory'
2.441 - -> rew_ord'
2.442 - -> rls' -> bool -> thm' -> cterm' -> (cterm' * cterm' list) option
2.443 -\end{verbatim}}%size
2.444 -The arguments are the following:\\
2.445 -\tabcolsep=4mm
2.446 -\def\arraystretch{1.5}
2.447 -\begin{tabular}{lp{11.0cm}}
2.448 - {\tt theory} & the Isabelle theory containing the definitions necessary for parsing the {\tt term} \\
2.449 - {\tt rew\_ord}& the rewrite order \cite{nipk:rew-all-that} for ordered rewriting -- see the section \ref{term-order} below. For {\em no} ordered rewriting take {\tt tless\_true}, a dummy order yielding true for all arguments \\
2.450 - {\tt rls} & the rule set for evaluating the condition within {\tt thm} in case {\tt thm} is a conditional rule \\
2.451 - {\tt bool} & a flag which triggers the evaluation of the eventual condition in {\tt thm}: if {\tt false} then evaluate the condition and according to the result of the evaluation apply {\tt thm} or not (conditional rewriting \cite{nipk:rew-all-that}), if {\tt true} then don't evaluate the condition, but put it into the set of assumptions \\
2.452 - {\tt thm} & the theorem used to try to rewrite {\tt term} \\
2.453 - {\tt term} & the term eventually rewritten by {\tt thm} \\
2.454 -\end{tabular}\\
2.455 -
2.456 -\noindent The respective values of {\tt rewrite\_} and {\tt rewrite} are an {\tt option} of a pair, i.e. {\tt Some(\_,\_)} in case the {\tt term} can be rewritten by {\tt thm} w.r.t. {\tt rew\_ord} and/or {\tt rls}, or {\tt None} if no rewrite is found:\\
2.457 -\begin{tabular}{lp{10.4cm}}
2.458 - {\tt term} & the term rewritten \\
2.459 - {\tt term list}& the assumptions eventually generated if the {\tt bool} flag is set to {\tt true} and {\tt thm} is applicable. \\
2.460 -\end{tabular}\\
2.461 -
2.462 -\paragraph{Give it a try !} {\bf\dots rewriting is fun~!} many examples can be found in {\tt [isac-src]/tests/\dots}. In {\tt [isac-src]/tests/differentiate.sml} the following can be found:
2.463 -{\footnotesize\begin{verbatim}
2.464 - ML> val thy' = "Differentiate.thy";
2.465 - val thy' = "Differentiate.thy" : string
2.466 - ML> val ct = "d_d x (x ^^^ #2 + #3 * x + #4)";
2.467 - val ct = "d_d x (x ^^^ #2 + #3 * x + #4)" : cterm'
2.468 - ML>
2.469 - ML> val thm = ("diff_sum","");
2.470 - val thm = ("diff_sum","") : thm'
2.471 - ML> val Some (ct,_) = rewrite_inst thy' "tless_true" "eval_rls" true
2.472 - [("bdv","x::real")] thm ct;
2.473 - val ct = "d_d x (x ^^^ #2 + #3 * x) + d_d x #4" : cterm'
2.474 - ML>
2.475 - ML> val Some (ct,_) = rewrite_inst thy' "tless_true" "eval_rls" true
2.476 - [("bdv","x::real")] thm ct;
2.477 - val ct = "d_d x (x ^^^ #2) + d_d x (#3 * x) + d_d x #4" : cterm'
2.478 - ML>
2.479 - ML> val thm = ("diff_prod_const","");
2.480 - val thm = ("diff_prod_const","") : thm'
2.481 - ML> val Some (ct,_) = rewrite_inst thy' "tless_true" "eval_rls" true
2.482 - [("bdv","x::real")] thm ct;
2.483 - val ct = "d_d x (x ^^^ #2) + #3 * d_d x x + d_d x #4" : cterm'
2.484 -\end{verbatim}}%size
2.485 -Sie k\"onnen unter {\tt [isac-src]/knowledge/Differentiate.thy} die Lehrs\"atze nachschlagen und versuchen Sie, diese anzuwenden bis Sie die Ergebnisse bekommen.
2.486 -\footnote{Hinweis: Am Ende werden Sie {\tt val (ct,\_) = the (rewrite\_set thy' "eval\_rls" false "SqRoot\_simplify" ct);} benötigen.}
2.487 -
2.488 -\paragraph{Versuchen Sie es!}\label{cond-rew} {\bf Conditional rewriting} ist eine besser Technik als \"ubliche Umschreibungen und \"ahnelt den Programmiersprachen mehr (siehe n\"achstes 'Versuchen Sie es'~!). Das folgende Beispiel liegt im Bereich der ??poynomial form??:
2.489 -{\footnotesize\begin{verbatim}
2.490 - ML> val thy' = "Isac.thy";
2.491 - val thy' = "Isac.thy" : string
2.492 - ML> val ct' = "#3 * a + #2 * (a + #1)";
2.493 - val ct' = "#3 * a + #2 * (a + #1)" : cterm'
2.494 - ML>
2.495 - ML> val thm' = ("radd_mult_distrib2","?k * (?m + ?n) = ?k * ?m + ?k * ?n");
2.496 - val thm' = ("radd_mult_distrib2","?k * (?m + ?n) = ?k * ?m + ?k * ?n")
2.497 - : thm'
2.498 - ML> (*1*) val Some (ct',_) = rewrite thy' "tless_true" "eval_rls" true thm' ct';
2.499 - val ct' = "#3 * a + (#2 * a + #2 * #1)" : cterm'
2.500 - ML>
2.501 - ML> val thm' = ("radd_assoc_RS_sym","?m1 + (?n1 + ?k1) = ?m1 + ?n1 + ?k1");
2.502 - val thm' = ("radd_assoc_RS_sym","?m1 + (?n1 + ?k1) = ?m1 + ?n1 + ?k1")
2.503 - : thm'
2.504 - ML> (*2*) val Some (ct',_) = rewrite thy' "tless_true" "eval_rls" true thm' ct';
2.505 - val ct' = "#3 * a + #2 * a + #2 * #1" : cterm'
2.506 - ML>
2.507 - ML> val thm' = ("rcollect_right",
2.508 - "[| ?l is_const; ?m is_const |] ==> ?l * ?n + ?m * ?n = (?l + ?m) * ?n");
2.509 - val thm' =
2.510 - ("rcollect_right",
2.511 - "[| ?l is_const; ?m is_const |] ==> ?l * ?n + ?m * ?n = (?l + ?m) * ?n")
2.512 - : thm'
2.513 - ML> (*3*) val Some (ct',_) = rewrite thy' "tless_true" "eval_rls" true thm' ct';
2.514 - val ct' = "(#3 + #2) * a + #2 * #1" : cterm'
2.515 - ML>
2.516 - ML> (*4*) val Some (ct',_) = calculate' thy' "plus" ct';
2.517 - val ct' = "#5 * a + #2 * #1" : cterm'
2.518 - ML>
2.519 - ML> (*5*) val Some (ct',_) = calculate' thy' "times" ct';
2.520 - val ct' = "#5 * a + #2" : cterm'
2.521 -\end{verbatim}}%size
2.522 -Beachten Sie, dass es zwei Regeln gibt {\tt radd\_mult\_distrib2} in {\tt(*1*)} und {\tt rcollect\_right} in {\tt(*3*)}, die einander aufheben, (das heißt, eine angesetzte Regel w\"urde es nicht beenden), wenn es diese Bedinung nicht vorhanden ist {\tt is\_const}.
2.523 -
2.524 -\paragraph{Versuchen Sie es!} {\bf Funktionelle Programmierung} kann, innerhalb einer bestimmten Reihe, durch das Umschreiben bearbeitet werden. In {\tt [isac-src]/\dots/tests/InsSort.thy} k\"onnen die Regeln gefunden werden, mit denen man eine Liste sortieren kann ('insertion sort'):
2.525 -{\footnotesize\begin{verbatim}
2.526 - sort_def "sort ls = foldr ins ls []"
2.527 -
2.528 - ins_base "ins [] a = [a]"
2.529 - ins_rec "ins (x#xs) a = (if x < a then x#(ins xs a) else a#(x#xs))"
2.530 -
2.531 - foldr_base "foldr f [] a = a"
2.532 - foldr_rec "foldr f (x#xs) a = foldr f xs (f a x)"
2.533 -
2.534 - if_True "(if True then ?x else ?y) = ?x"
2.535 - if_False "(if False then ?x else ?y) = ?y"
2.536 -\end{verbatim}}%size
2.537 -{\tt\#} ist ein Listenersteller, {\tt foldr} ist die bekannte Funktion beim funktionellen Programmieren und {\tt if\_True, if\_False} sind die Hilfsregeln. Dann kann das Sortieren mit den folgenden Umschreibungen durchgef\"uhrt werden.
2.538 -{\footnotesize\begin{verbatim}
2.539 - ML> val thy' = "InsSort.thy";
2.540 - val thy' = "InsSort.thy" : theory'
2.541 - ML> val ct = "sort [#1,#3,#2]" : cterm';
2.542 - val ct = "sort [#1,#3,#2]" : cterm'
2.543 - ML>
2.544 - ML> val thm = ("sort_def","");
2.545 - ML> val (ct,_) = the (rewrite thy' "tless_true" "eval_rls" false thm ct);
2.546 - val ct = "foldr ins [#1, #3, #2] []" : cterm'
2.547 - ML>
2.548 - ML> val thm = ("foldr_rec","");
2.549 - ML> val (ct,_) = the (rewrite thy' "tless_true" "eval_rls" false thm ct);
2.550 - val ct = "foldr ins [#3, #2] (ins [] #1)" : cterm'
2.551 - ML>
2.552 - ML> val thm = ("ins_base","");
2.553 - ML> val (ct,_) = the (rewrite thy' "tless_true" "eval_rls" false thm ct);
2.554 - val ct = "foldr ins [#3, #2] [#1]" : cterm'
2.555 - ML>
2.556 - ML> val thm = ("foldr_rec","");
2.557 - ML> val (ct,_) = the (rewrite thy' "tless_true" "eval_rls" false thm ct);
2.558 - val ct = "foldr ins [#2] (ins [#1] #3)" : cterm'
2.559 - ML>
2.560 - ML> val thm = ("ins_rec","");
2.561 - ML> val (ct,_) = the (rewrite thy' "tless_true" "eval_rls" false thm ct);
2.562 - val ct = "foldr ins [#2] (if #1 < #3 then #1 # ins [] #3 else [#3, #1])"
2.563 - : cterm'
2.564 - ML>
2.565 - ML> val (ct,_) = the (calculate' thy' "le" ct);
2.566 - val ct = "foldr ins [#2] (if True then #1 # ins [] #3 else [#3, #1])" : cterm'
2.567 - ML>
2.568 - ML> val thm = ("if_True","(if True then ?x else ?y) = ?x");
2.569 - ML> val (ct,_) = the (rewrite thy' "tless_true" "eval_rls" false thm ct);
2.570 - val ct = "foldr ins [#2] (#1 # ins [] #3)" : cterm'
2.571 - ML>
2.572 - ...
2.573 - val ct = "sort [#1,#3,#2]" : cterm'
2.574 -\end{verbatim}}%size
2.575 -
2.576 -
2.577 -\section{Varianten des Umschreibens}
2.578 -Einige der genannten Beispiele verwendeten schon Methoden von {\tt rewrite}, welche den selben Wert haben und sehr \"ahnliche Argumente verwenden:
2.579 -{\footnotesize\begin{verbatim}
2.580 - ML> rewrite_inst_;
2.581 - val it = fn
2.582 - : theory
2.583 - -> rew_ord
2.584 - -> rls
2.585 - -> bool
2.586 - -> (cterm' * cterm') list
2.587 - -> thm -> term -> (term * term list) option
2.588 - ML> rewrite_inst;
2.589 - val it = fn
2.590 - : theory'
2.591 - -> rew_ord'
2.592 - -> rls'
2.593 - -> bool
2.594 - -> (cterm' * cterm') list
2.595 - -> thm' -> cterm' -> (cterm' * cterm' list) option
2.596 - ML>
2.597 - ML> rewrite_set_;
2.598 - val it = fn
2.599 - : theory -> rls -> bool -> rls -> term -> (term * term list) option
2.600 - ML> rewrite_set;
2.601 - val it = fn
2.602 - : theory' -> rls' -> bool -> rls' -> cterm' -> (cterm' * cterm' list) option
2.603 - ML>
2.604 - ML> rewrite_set_inst_;
2.605 - val it = fn
2.606 - : theory
2.607 - -> rls
2.608 - -> bool
2.609 - -> (cterm' * cterm') list
2.610 - -> rls -> term -> (term * term list) option
2.611 - ML> rewrite_set_inst;
2.612 - val it = fn
2.613 - : theory'
2.614 - -> rls'
2.615 - -> bool
2.616 - -> (cterm' * cterm') list
2.617 - -> rls' -> cterm' -> (cterm' * cterm' list) option
2.618 -\end{verbatim}}%size
2.619 -
2.620 -\noindent Die Variante {\tt rewrite\_inst} \"andert {\tt (term * term) list} zu {\tt thm} vor dem Umschreiben,\\
2.621 -Die Variante {\tt rewrite\_set} umschreibt {\tt rls} mit einem ganzen Regelsatz (anstatt mit {\tt thm}),\\
2.622 -Die Variante {\tt rewrite\_set\_inst} ist eine Kombination aus den letzten zwei Varianten. Um zu sehen wie ein Ausdruck umgeschreiben wird, gibt es einen Schalter {\tt trace\_rewrite}:
2.623 -{\footnotesize\begin{verbatim}
2.624 - ML> toggle;
2.625 - val it = fn : bool ref -> bool
2.626 - ML>
2.627 - ML> toggle trace_rewrite;
2.628 - val it = true : bool
2.629 - ML> toggle trace_rewrite;
2.630 - val it = false : bool
2.631 -\end{verbatim}}%size
2.632 -
2.633 -\section{Regels\"atze}
2.634 -Eine Varianten von {\tt rewrite} oberhalb gelten nicht nur für einen Lehrsatz, sondern für eine Vielzahl von Lehrs\"atzen, die 'Regels\"atze' genannt werden. Ein Regelsatz wird so lange angewendet, bis eines seiner Elemente f\"ur das Umschreiben verwendet werden kann (das kann ewig dauern, zum Beispiel, wenn ein Regelsatz nicht endet).
2.635 -
2.636 -Ein einfaches Beispiel für einen Regelsatz ist {\tt rearrange\_assoc}, welches in {\tt knowledge/RatArith.ML} beschrieben wird:
2.637 -{\footnotesize\begin{verbatim}
2.638 - val rearrange_assoc =
2.639 - Rls{preconds = [], rew_ord = ("tless_true",tless_true),
2.640 - rules =
2.641 - [Thm ("radd_assoc_RS_sym",num_str (radd_assoc RS sym)),
2.642 - Thm ("rmult_assoc_RS_sym",num_str (rmult_assoc RS sym))],
2.643 - scr = Script ((term_of o the o (parse thy))
2.644 - "empty_script")
2.645 - }:rls;
2.646 -\end{verbatim}}%size
2.647 -
2.648 -\begin{description}
2.649 -\item [\tt preconds] sind Bedinungen, die zutreffen m\"ussen, um den Regelsatz anwendbar zu machen (eine leere Liste berechnet {\tt true}).
2.650 -\item [\tt rew\_ord] betrifft die Anordnung der Ausdr\"ucke, dei weiter unten in \ref{term-order} vorgestellt werden.
2.651 -\item [\tt rules] sind die angewandten Lehrs\"atze -- grunds\"atzlich in beliebiger Anordnung, weil die Regels\"atze vervollst\"andigt werden sollten \cite{nipk:rew-all-that} (und die Lehrs\"atze werden tats\"achlich in der Reihenfolge, in der sie auf der Liste erscheinen, angewendet). Die Funktion {\tt num\_str}, muss bei den Lehrs\"atzen, die viele Konstanten enthalten, angewendet werden (und demnach ist das bei diesem Beispiel veraltert). {\tt RS} ist eine eingef\"ugte Funktion, die im Lehrsatz {\tt sym} zu {\tt radd\_assoc} vor der Abspeicherung angewendet wird (siehe 'Effekt')
2.652 -\item [\tt scr] auch wenn das script den Regelsatz anwendet, wird es in späteren Versionen von \isac verschwinden.
2.653 -\end{description}
2.654 -Diese Variablen bestimmen folgendes:
2.655 -{\footnotesize\begin{verbatim}
2.656 - ML> sym;
2.657 - val it = "?s = ?t ==> ?t = ?s" : thm
2.658 - ML> rearrange_assoc;
2.659 - val it =
2.660 - Rls
2.661 - {preconds=[],rew_ord=("tless_true",fn),
2.662 - rules=[Thm ("radd_assoc_RS_sym","?m1 + (?n1 + ?k1) = ?m1 + ?n1 + ?k1"),
2.663 - Thm ("rmult_assoc_RS_sym","?m1 * (?n1 * ?k1) = ?m1 * ?n1 * ?k1")],
2.664 - scr=Script (Free ("empty_script","RealDef.real"))} : rls
2.665 -\end{verbatim}}%size
2.666 -
2.667 -\paragraph{Versuchen Sie es!} Der obengenannte Regel-Satz l\"asst eine beliebige Zahl von Parenthesen verschwinden, die auf Grund von Assoziation auf {\tt +} nicht notwendig sind.
2.668 -{\footnotesize\begin{verbatim}
2.669 - ML> val ct = (string_of_cterm o the o (parse RatArith.thy))
2.670 - "a + (b * (c * d) + e)";
2.671 - val ct = "a + ((b * (c * d) + e) + f)" : cterm'
2.672 - ML> rewrite_set "RatArith.thy" "eval_rls" false "rearrange_assoc" ct;
2.673 - val it = Some ("a + b * c * d + e + f",[]) : (string * string list) option
2.674 -\end{verbatim}}%size
2.675 -Um dieses Ergebnis zu erreichen muss der Regelsatz \"uberraschend schnell sein:
2.676 -{\footnotesize\begin{verbatim}
2.677 - ML> toggle trace_rewrite;
2.678 - val it = true : bool
2.679 - ML> rewrite_set "RatArith.thy" "eval_rls" false "rearrange_assoc" ct;
2.680 - ### trying thm 'radd_assoc_RS_sym'
2.681 - ### rewrite_set_: a + b * (c * d) + e
2.682 - ### trying thm 'radd_assoc_RS_sym'
2.683 - ### trying thm 'rmult_assoc_RS_sym'
2.684 - ### rewrite_set_: a + b * c * d + e
2.685 - ### trying thm 'rmult_assoc_RS_sym'
2.686 - ### trying thm 'radd_assoc_RS_sym'
2.687 - ### trying thm 'rmult_assoc_RS_sym'
2.688 - val it = Some ("a + b * c * d + e",[]) : (string * string list) option
2.689 -\end{verbatim}}%size
2.690 -
2.691 -
2.692 -\section{Berechnung von numerischen Konstanten}
2.693 -Sobald numerische Konstanten in angrenzenden Subfristen sind, können sie durch die Funktion berechnet werden (siehe p.\pageref{cond-rew}):
2.694 -{\footnotesize\begin{verbatim}
2.695 - ML> calculate;
2.696 - val it = fn : theory' -> string -> cterm' -> (cterm' * thm') option
2.697 - ML> calculate_;
2.698 - val it = fn : theory -> string -> term -> (term * (string * thm)) option
2.699 -\end{verbatim}}%size
2.700 -{\tt string} beschreibt in den Angaben die mathematisch zu berechnende Operation. Die Funktion gibt das Ergebnis der Berechnung, und als zweites Element in der Reihe gilt der Lehrsatz. Die folgenden mathematischen Operationen sind verfügbar:
2.701 -{\footnotesize\begin{verbatim}
2.702 - ML> calc_list;
2.703 - val it =
2.704 - ref
2.705 - [("plus",("op +",fn)),
2.706 - ("times",("op *",fn)),
2.707 - ("cancel_",("cancel",fn)),
2.708 - ("power",("pow",fn)),
2.709 - ("sqrt",("sqrt",fn)),
2.710 - ("Var",("Var",fn)),
2.711 - ("Length",("Length",fn)),
2.712 - ("Nth",("Nth",fn)),
2.713 - ("power",("pow",fn)),
2.714 - ("le",("op <",fn)),
2.715 - ("leq",("op <=",fn)),
2.716 - ("is_const",("is'_const",fn)),
2.717 - ("is_root_free",("is'_root'_free",fn)),
2.718 - ("contains_root",("contains'_root",fn)),
2.719 - ("ident",("ident",fn))]
2.720 - : (string * (string * (string -> term -> theory ->
2.721 - (string * term) option))) list ref
2.722 -\end{verbatim}}%size
2.723 -Diese Vorgänge k\"onnen so verwendet werden:
2.724 -{\footnotesize\begin{verbatim}
2.725 - ML> calculate' "Isac.thy" "plus" "#1 + #2";
2.726 - val it = Some ("#3",("#add_#1_#2","\"#1 + #2 = #3\"")) : (string * thm') option
2.727 - ML>
2.728 - ML> calculate' "Isac.thy" "times" "#2 * #3";
2.729 - val it = Some ("#6",("#mult_#2_#3","\"#2 * #3 = #6\""))
2.730 - : (string * thm') option
2.731 - ML>
2.732 - ML> calculate' "Isac.thy" "power" "#2 ^^^ #3";
2.733 - val it = Some ("#8",("#power_#2_#3","\"#2 ^^^ #3 = #8\""))
2.734 - : (string * thm') option
2.735 - ML>
2.736 - ML> calculate' "Isac.thy" "cancel_" "#9 // #12";
2.737 - val it = Some ("#3 // #4",("#cancel_#9_#12","\"#9 // #12 = #3 // #4\""))
2.738 - : (string * thm') option
2.739 - ML>
2.740 - ML> ...
2.741 -\end{verbatim}}%size
2.742 -
2.743 -
2.744 -
2.745 -\chapter{Begriff-Ordnung}\label{term-order}
2.746 -Die Anordnungen der Terme sind unverzichtbar f\"ur den Gebrauch des Umschreibens von normalen Funktionen in inhaltsorientierten - kommunikativen Breichen, wie \cite{nipk:rew-all-that}, und zum Umschreiben von normalen Formeln, die n\"otig sind um passende Modelle f\"ur Probleme zu finden, siehe \ref{pbt}.
2.747 -\section{Beispiel f\"ur Begriff-Ordnungen}
2.748 -Es ist nicht unbedeutend, eine Verbindung $<$ zu Termen herzustellen, die wirklich eine Anordnung besitzen, wie eine transitive und antisymmetrische Verbindung. Diese Anordnungen sind 'rekursive Bahnanordnungen' \cite{nipk:rew-all-that}. Einige Anordnungen sind im Basiswissen bei {\tt [isac-src]/knowledge/\dots}, angeführt. %FIXXXmat0201a
2.749 -unter anderem
2.750 -{\footnotesize\begin{verbatim}
2.751 - ML> sqrt_right;
2.752 - val it = fn : bool -> theory -> term * term -> bool
2.753 - ML> tless_true;
2.754 - val it = fn : 'a -> bool
2.755 -\end{verbatim}}%size
2.756 -Das bool Argument ist ein Schalter um die Kontrolle zur\"uck zu den zugeh\"origen Unterordnungen zu verfolgen (diese Theorie ist notwendig um die Unterordnungen als strings, sollten sie 'true' sein, anzuzeigen). Die Anordnung {\tt tless\_true} ist belanglos und tr\"agt immer {\tt true}, und {\tt sqrt\_right} bevorzugt eine Quadratwurzel, die nach rechts im Ausdruck geschoben wird:
2.757 -{\footnotesize\begin{verbatim}
2.758 - ML> val t1 = (term_of o the o (parse thy)) "(sqrt a) + b";
2.759 - val t1 = Const # $ (# $ #) $ Free (#,#) : term
2.760 - ML>
2.761 - ML> val t2 = (term_of o the o (parse thy)) "b + (sqrt a)";
2.762 - val t2 = Const # $ Free # $ (Const # $ Free #) : term
2.763 - ML>
2.764 - ML> sqrt_right false SqRoot.thy (t1, t2);
2.765 - val it = false : bool
2.766 - ML> sqrt_right false SqRoot.thy (t2, t1);
2.767 - val it = true : bool
2.768 -\end{verbatim}}%size
2.769 -Die vielen Kontrollen, die rekursiv durch alle Subbegriffe durchgef\"uhrt werden, können überall im Algorithmus in {\tt [isac-src]/knowledge/SqRoot.ML} verfolgt werden, wenn man die flag auf true setzt:
2.770 -{\footnotesize\begin{verbatim}
2.771 - ML> val t1 = (term_of o the o (parse thy)) "a + b*(sqrt c) + d";
2.772 - val t1 = Const (#,#) $ (# $ # $ (# $ #)) $ Free ("d","RealDef.real") : term
2.773 - ML>
2.774 - ML> val t2 = (term_of o the o (parse thy)) "a + (sqrt b)*c + d";
2.775 - val t2 = Const (#,#) $ (# $ # $ (# $ #)) $ Free ("d","RealDef.real") : term
2.776 - ML>
2.777 - ML> sqrt_right true SqRoot.thy (t1, t2);
2.778 - t= f@ts= "op +" @ "[a + b * sqrt c,d]"
2.779 - u= g@us= "op +" @ "[a + sqrt b * c,d]"
2.780 - size_of_term(t,u)= (8, 8)
2.781 - hd_ord(f,g) = EQUAL
2.782 - terms_ord(ts,us) = LESS
2.783 - -------
2.784 - t= f@ts= "op +" @ "[a,b * sqrt c]"
2.785 - u= g@us= "op +" @ "[a,sqrt b * c]"
2.786 - size_of_term(t,u)= (6, 6)
2.787 - hd_ord(f,g) = EQUAL
2.788 - terms_ord(ts,us) = LESS
2.789 - -------
2.790 - t= f@ts= "a" @ "[]"
2.791 - u= g@us= "a" @ "[]"
2.792 - size_of_term(t,u)= (1, 1)
2.793 - hd_ord(f,g) = EQUAL
2.794 - terms_ord(ts,us) = EQUAL
2.795 - -------
2.796 - t= f@ts= "op *" @ "[b,sqrt c]"
2.797 - u= g@us= "op *" @ "[sqrt b,c]"
2.798 - size_of_term(t,u)= (4, 4)
2.799 - hd_ord(f,g) = EQUAL
2.800 - terms_ord(ts,us) = LESS
2.801 - -------
2.802 - t= f@ts= "b" @ "[]"
2.803 - u= g@us= "sqrt" @ "[b]"
2.804 - size_of_term(t,u)= (1, 2)
2.805 - hd_ord(f,g) = LESS
2.806 - terms_ord(ts,us) = LESS
2.807 - -------
2.808 - val it = true : bool
2.809 -\end{verbatim}}%size
2.810 -
2.811 -
2.812 -
2.813 -\section{Geordnetes Umschreiben}
2.814 -Das Umschreiben beinhaltet in fast allen elementaren Bereichen Probleme, die alle assoziieren und ausgewechselt werden k\"onnen, im Bezug auf {\tt +} und {\tt *} --- Das Gesetz der Wandelbarkeit angewendet mit einem Regelsatzes, veranlasst den Satz, nicht zu enden! Ein Weg mit dieser Schwierigkeit umzugehen ist das geordnete Umschreiben, bei dem die Umschreibung erst beendet ist, wenn der Begriff des Ergebnisses kleiner ist, im Bezug auf eine Begriff-Ordnung (mit einigen zus\"atzlichen Eigenschaften, die 'rewrite orders' \cite{nipk:rew-all-that} genannt werden).
2.815 -
2.816 -Ein solcher Regelsatz {\tt ac\_plus\_times}, der als AC-rewrite system bezeichnet wird, kann in {\tt[isac-src]/knowledge/RathArith.ML} gefunden werden:
2.817 -{\footnotesize\begin{verbatim}
2.818 - val ac_plus_times =
2.819 - Rls{preconds = [], rew_ord = ("term_order",term_order),
2.820 - rules =
2.821 - [Thm ("radd_commute",radd_commute),
2.822 - Thm ("radd_left_commute",radd_left_commute),
2.823 - Thm ("radd_assoc",radd_assoc),
2.824 - Thm ("rmult_commute",rmult_commute),
2.825 - Thm ("rmult_left_commute",rmult_left_commute),
2.826 - Thm ("rmult_assoc",rmult_assoc)],
2.827 - scr = Script ((term_of o the o (parse thy))
2.828 - "empty_script")
2.829 - }:rls;
2.830 - val ac_plus_times =
2.831 - Rls
2.832 - {preconds=[],rew_ord=("term_order",fn),
2.833 - rules=[Thm ("radd_commute","?m + ?n = ?n + ?m"),
2.834 - Thm ("radd_left_commute","?x + (?y + ?z) = ?y + (?x + ?z)"),
2.835 - Thm ("radd_assoc","?m + ?n + ?k = ?m + (?n + ?k)"),
2.836 - Thm ("rmult_commute","?m * ?n = ?n * ?m"),
2.837 - Thm ("rmult_left_commute","?x * (?y * ?z) = ?y * (?x * ?z)"),
2.838 - Thm ("rmult_assoc","?m * ?n * ?k = ?m * (?n * ?k)")],
2.839 - scr=Script (Free ("empty_script","RealDef.real"))} : rls
2.840 -\end{verbatim}}%size
2.841 -Beachten Sie, dass die Lehrs\"atze {\tt radd\_left\_commute} und {\tt rmult\_left\_commute} notwendig sind, um den Regelsatz 'confluent' zu machen!
2.842 -
2.843 -
2.844 -\paragraph{Versuchen Sie es!} Das geordnete Umschreiben ist eine Technik um ein normales Polynom von willk\"urlich, ganzzahligen Termen zu schafffen.:
2.845 -{\footnotesize\begin{verbatim}
2.846 - ML> val ct' = "#3 * a + b + #2 * a";
2.847 - val ct' = "#3 * a + b + #2 * a" : cterm'
2.848 - ML>
2.849 - ML> (*-1-*) radd_commute; val thm' = ("radd_commute","") : thm';
2.850 - val it = "?m + ?n = ?n + ?m" : thm
2.851 - val thm' = ("radd_commute","") : thm'
2.852 - ML> val Some (ct',_) = rewrite thy' "tless_true" "eval_rls" true thm' ct';
2.853 - val ct' = "#2 * a + (#3 * a + b)" : cterm'
2.854 - ML>
2.855 - ML> (*-2-*) rdistr_right_assoc_p; val thm' = ("rdistr_right_assoc_p","") : thm';
2.856 - val it = "?l * ?n + (?m * ?n + ?k) = (?l + ?m) * ?n + ?k" : thm
2.857 - val thm' = ("rdistr_right_assoc_p","") : thm'
2.858 - ML> val Some (ct',_) = rewrite thy' "tless_true" "eval_rls" true thm' ct';
2.859 - val ct' = "(#2 + #3) * a + b" : cterm'
2.860 - ML>
2.861 - ML> (*-3-*)
2.862 - ML> val Some (ct',_) = calculate thy' "plus" ct';
2.863 - val ct' = "#5 * a + b" : cterm'
2.864 -\end{verbatim}}%size %FIXXXmat0201b ... calculate !
2.865 -Das sieht toll aus, aber wenn {\tt radd\_commute} automatisch angewendet wird {\tt (*-1-*)} ohne zu \"uberpr\"ufen, ob ide daraus entstehenden Terme kleiner werden im Bezug auf die Begriffsordnung, dann geht das Umschreiben endlos weiter. (das heißt, es wird nicht beendet) \dots
2.866 -{\footnotesize\begin{verbatim}
2.867 - ML> val ct' = "#3 * a + b + #2 * a" : cterm';
2.868 - val ct' = "#3 * a + b + #2 * a" : cterm'
2.869 - ML> val thm' = ("radd_commute","") : thm';
2.870 - val thm' = ("radd_commute","") : thm'
2.871 - ML>
2.872 - ML> val Some (ct',_) = rewrite thy' "tless_true" "eval_rls" true thm' ct';
2.873 - val ct' = "#2 * a + (#3 * a + b)" : cterm'
2.874 - ML> val Some (ct',_) = rewrite thy' "tless_true" "eval_rls" true thm' ct';
2.875 - val ct' = "#3 * a + b + #2 * a" : cterm'
2.876 - ML> val Some (ct',_) = rewrite thy' "tless_true" "eval_rls" true thm' ct';
2.877 - val ct' = "#2 * a + (#3 * a + b)" : cterm'
2.878 - ..........
2.879 -\end{verbatim}}%size
2.880 -
2.881 -Geordnetes Umschreiben mit dem obrigen AC-rewrite system {\tt ac\_plus\_times} verursacht eine Art Durcheinander, dem man auf die Spur kommen kann:
2.882 -{\footnotesize\begin{verbatim}
2.883 - ML> toggle trace_rewrite;
2.884 - val it = true : bool
2.885 - ML>
2.886 - ML> rewrite_set "RatArith.thy" "eval_rls" false "ac_plus_times" ct;
2.887 - ### trying thm 'radd_commute'
2.888 - ### not: "a + (b * (c * d) + e)" > "b * (c * d) + e + a"
2.889 - ### rewrite_set_: a + (e + b * (c * d))
2.890 - ### trying thm 'radd_commute'
2.891 - ### not: "a + (e + b * (c * d))" > "e + b * (c * d) + a"
2.892 - ### not: "e + b * (c * d)" > "b * (c * d) + e"
2.893 - ### trying thm 'radd_left_commute'
2.894 - ### not: "a + (e + b * (c * d))" > "e + (a + b * (c * d))"
2.895 - ### trying thm 'radd_assoc'
2.896 - ### trying thm 'rmult_commute'
2.897 - ### not: "b * (c * d)" > "c * d * b"
2.898 - ### not: "c * d" > "d * c"
2.899 - ### trying thm 'rmult_left_commute'
2.900 - ### not: "b * (c * d)" > "c * (b * d)"
2.901 - ### trying thm 'rmult_assoc'
2.902 - ### trying thm 'radd_commute'
2.903 - ### not: "a + (e + b * (c * d))" > "e + b * (c * d) + a"
2.904 - ### not: "e + b * (c * d)" > "b * (c * d) + e"
2.905 - ### trying thm 'radd_left_commute'
2.906 - ### not: "a + (e + b * (c * d))" > "e + (a + b * (c * d))"
2.907 - ### trying thm 'radd_assoc'
2.908 - ### trying thm 'rmult_commute'
2.909 - ### not: "b * (c * d)" > "c * d * b"
2.910 - ### not: "c * d" > "d * c"
2.911 - ### trying thm 'rmult_left_commute'
2.912 - ### not: "b * (c * d)" > "c * (b * d)"
2.913 - ### trying thm 'rmult_assoc'
2.914 - val it = Some ("a + (e + b * (c * d))",[]) : (string * string list) option \end{verbatim}}%size
2.915 -Beachten Sie, dass {\tt +} nach links ausgerichtet ist, bei dem die Parenthesen f\"ur {\tt (a + b) + c = a + b + c}, aber nicht f\"ur {\tt a + (b + c)} weggelassen werden. Geordnetes Umschreiben endet unbedingt mit Parenthesen, die auf Grund der Assoziation weggelassen werden k\"onnen.
2.916 -
2.917 -
2.918 \chapter{The hierarchy of problem types}\label{pbt}
2.919 \section{The standard-function for 'matching'}
2.920 Matching \cite{nipk:rew-all-that} is a technique used within rewriting, and used by \isac{} also for (a generalized) 'matching' a problem with a problem type. The function which tests for matching has the following signature: