1.1 --- a/doc-src/isac/mat-eng-de.tex Wed Jul 28 10:01:33 2010 +0200
1.2 +++ b/doc-src/isac/mat-eng-de.tex Wed Jul 28 13:26:19 2010 +0200
1.3 @@ -494,11 +494,236 @@
1.4
1.5 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.6
1.7 +{\section{Geordnetes Rewriting}}
1.8 +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.9 +\paragraph{Versuchen Sie es!} Das geordnete Rewriting ist eine Technik, um ein normales Polynom aus ganzzahligen Termen zu schaffen.
1.10 +Geordnetes Rewriting endet mit Klammern, aber auf Grund der weggelassenen Verbindung.
1.11 +
1.12 +
1.13 +\chapter{Die Hirarchie von Problemen}
1.14 +\section{''Matching``}
1.15 +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.16 +{\footnotesize\begin{verbatim}
1.17 +> matches;
1.18 +val it = fn : Theory.theory -> Term.term -> Term.term -> bool
1.19 +\end{verbatim}
1.20 +Die folgende Gleichung wird in Operatoren und freie Variablen zerlegt.
1.21 +{\footnotesize\begin{verbatim}
1.22 +> val t = (term_of o the o (parse thy)) "3 * x^^^2 = 1";
1.23 +val t =
1.24 +Const ("op =", "[RealDef.real, RealDef.real] => bool") $
1.25 +(Const ("op *", "[RealDef.real, RealDef.real] => RealDef.real") $
1.26 +Free ("3", "RealDef.real") $
1.27 +(Const
1.28 +("Atools.pow",
1.29 +"[RealDef.real, RealDef.real] => RealDef.real") $
1.30 +Free ("x", "RealDef.real") $ Free ("2", " RealDef.real"))) $
1.31 +Free ("1", "RealDef.real") : Term.term
1.32 +\end{verbatim}
1.33 +Nun wird ein Modell erstellt, das sich nicht auf bestimmte Zahlen bezieht, sondern nur eine generelle Zerlegung durchführt.
1.34 +{\footnotesize\begin{verbatim}
1.35 +> val p = (term_of o the o (parse thy)) "a * b^^^2 = c";
1.36 +val p =
1.37 +Const ("op =", "[RealDef.real, RealDef.real] => bool") $
1.38 +(Const ("op *", "[RealDef.real, RealDef.real] => RealDef.real") $
1.39 +Free ("a", "RealDef.real") $
1.40 +(Const
1.41 +("Atools.pow",
1.42 +"[RealDef.real, RealDef.real] => RealDef.real") $
1.43 +Free ("b", "RealDef.real") $ Free ("2", "RealDef.real"))) $
1.44 +Free ("c", "RealDef.real") : Term.term
1.45 +\end{verbatim}
1.46 +Dieses Modell enth\"allt sogenannte \textit{scheme variables}.
1.47 +{\footnotesize\begin{verbatim}
1.48 +> atomt p;
1.49 +"*** -------------"
1.50 +"*** Const (op =)"
1.51 +"*** . Const (op *)""*** . . Free (a, )"
1.52 +"*** . . Const (Atools.pow)"
1.53 +"*** . . . Free (b, )"
1.54 +"*** . . . Free (2, )"
1.55 +"*** . Free (c, )"
1.56 +"\n"
1.57 +val it = "\n" : string
1.58 +\end{verbatim}
1.59 +Das Modell wird durch den Befehl free2var erstellt.
1.60 +{\footnotesize\begin{verbatim}
1.61 +> free2var;
1.62 +val it = fn : Term.term -> Term.term
1.63 +> val pat = free2var p;
1.64 +val pat =
1.65 +Const ("op =", "[RealDef.real, RealDef.real] => bool") $
1.66 +(Const ("op *", "[RealDef.real, RealDef.real] => RealDef.real") $
1.67 +Var (("a", 0), "RealDef.real") $
1.68 +(Const
1.69 +("Atools.pow",
1.70 +"[RealDef.real, RealDef.real] => RealDef.real") $
1.71 +Var (("b", 0), "RealDef.real") $
1.72 +Free ("2", "RealDef.real"))) $ Var (("c", 0), "RealDef.real")
1.73 +: Term.term
1.74 +> Sign.string_of_term (sign_of thy) pat;
1.75 +val it = "?a * ?b ^^^ 2 = ?c" : string
1.76 +\end{verbatim}
1.77 +Durch atomt pat wird der Term aufgespalten und so in eine Form gebracht, die f\"ur die weiteren Schritte ben\"otigt werden.
1.78 +{\footnotesize\begin{verbatim}
1.79 +> atomt pat;
1.80 +"*** -------------"
1.81 +"*** Const (op =)"
1.82 +"*** . Const (op *)"
1.83 +"*** . . Var ((a, 0), )"
1.84 +"*** . . Const (Atools.pow)"
1.85 +"*** . . . Var ((b, 0), )"
1.86 +"*** . . . Free (2, )"
1.87 +"*** . Var ((c, 0), )"
1.88 +"\n"
1.89 +val it = "\n" : string
1.90 +\end{verbatim}
1.91 +Jetzt kann das Matching f\"ur die beiden vorigen Terme angewendet werden.
1.92 +{\footnotesize\begin{verbatim}
1.93 +> matches thy t pat;
1.94 +val it = true : bool
1.95 +> val t2 = (term_of o the o (parse thy)) "x^^^2 = 1";
1.96 +val t2 =
1.97 +Const ("op =", "[RealDef.real, RealDef.real] => bool") $
1.98 +(Const
1.99 +("Atools.pow",
1.100 +"[RealDef.real, RealDef.real] => RealDef.real") $
1.101 +Free ("x", "RealDef.real") $ Free ("2", "RealDef.real")) $
1.102 +Free ("1", "RealDef.real") : Term.term
1.103 +> matches thy t2 pat;
1.104 +val it = false : bool
1.105 +> val pat2 = (term_of o the o (parse thy)) "?u^^^2 = ?v";
1.106 +val pat2 =
1.107 +Const ("op =", "[RealDef.real, RealDef.real] => bool") $
1.108 +(Const
1.109 +("Atools.pow",
1.110 +"[RealDef.real, RealDef.real] => RealDef.real") $
1.111 +Var (("u", 0), "RealDef.real") $ Free ("2", "RealDef.real")) $
1.112 +Var (("v", 0), "RealDef.real") : Term.term
1.113 +> matches thy t2 pat2;
1.114 +val it = true : bool
1.115 +\end{verbatim}
1.116 +
1.117 +\section{Zugriff auf die Hierarchie}
1.118 +Man verwendet folgenden Befehl, um sich Zugang zur Hierarchie von Problemtypen zu verschaffen.
1.119 +{\footnotesize\begin{verbatim}
1.120 +> show_ptyps;
1.121 +val it = fn : unit -> unit
1.122 +> show_ptyps();
1.123 +[
1.124 +["e_pblID"],
1.125 +["simplification", "polynomial"],
1.126 +["simplification", "rational"],
1.127 +["vereinfachen", "polynom", "plus_minus"],
1.128 +["vereinfachen", "polynom", "klammer"],
1.129 +["vereinfachen", "polynom", "binom_klammer"],
1.130 +["probe", "polynom"],
1.131 +["probe", "bruch"],
1.132 +["equation", "univariate", "linear"],
1.133 +["equation", "univariate", "root", "sq", "rat"],
1.134 +["equation", "univariate", "root", "normalize"],
1.135 +["equation", "univariate", "rational"],
1.136 +["equation", "univariate", "polynomial", "degree_0"],
1.137 +["equation", "univariate", "polynomial", "degree_1"],
1.138 +["equation", "univariate", "polynomial", "degree_2", "sq_only"],
1.139 +["equation", "univariate", "polynomial", "
1.140 + degree_2", "bdv_only"],
1.141 +["equation", "univariate", "polynomial", "degree_2", "pqFormula"],
1.142 +["equation", "univariate", "polynomial", "degree_2", "abcFormula"],
1.143 +["equation", "univariate", "polynomial", "degree_3"],
1.144 +["equation", "univariate", "polynomial", "degree_4"],
1.145 +["equation", "univariate", "polynomial", "normalize"],
1.146 +["equation", "univariate", "expanded", "degree_2"],
1.147 +["equation", "makeFunctionTo"],
1.148 +["function", "derivative_of", "named"],
1.149 +["function", "maximum_of", "on_interval"],
1.150 +["function", "make", "by_explicit"],
1.151 +["function", "make", "by_new_variable"],
1.152 +["function", "integrate", "named"],
1.153 +["tool", "find_values"],
1.154 +["system", "linear", "2x2", "triangular"],
1.155 +["system", "linear", "2x2", "normalize"],
1.156 +["system", "linear", "3x3"],
1.157 +["system", "linear", "4x4", "triangular"],
1.158 +["system", "linear", "4x4", "normalize"],
1.159 +["Biegelinien", "
1.160 +MomentBestimmte"],
1.161 +["Biegelinien", "MomentGegebene"],
1.162 +["Biegelinien", "einfache"],
1.163 +["Biegelinien", "QuerkraftUndMomentBestimmte"],
1.164 +["Biegelinien", "vonBelastungZu"],
1.165 +["Biegelinien", "setzeRandbedingungen"],
1.166 +["Berechnung", "numerischSymbolische"],
1.167 +["test", "equation", "univariate", "linear"],
1.168 +["test", "equation", "univariate", "plain_square"],
1.169 +["test", "equation", "univariate", "polynomial", "degree_two", "pq_formula"],
1.170 +["test", "equation", "univariate", "polynomial", "degree_two", "abc_formula"],
1.171 +["test", "equation", "univariate", "squareroot"],
1.172 +["test", "equation", "univariate", "normalize"],
1.173 +["test", "equation", "univariate", "sqroot-test"]
1.174 +]
1.175 +val it = () : unit
1.176 +\end{verbatim}
1.177 +
1.178 +\section{Die passende ''Formalization`` f\"ur den Problemtyp}
1.179 +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.180 +
1.181 +\section{Problem - Refinement}
1.182 +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.183 +$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.184 +{\small
1.185 +\begin{enumerate}
1.186 +\item wenn für $F$ der Problemtyp $P_i$ passt, dann passt auch $P$
1.187 +\item wenn zu $F$ der Problemtyp P passt, dann sollte es nicht mehr als ein $P_i$ geben, das zu $F$ passt.
1.188 +\item alle $F$ , die zu $P$ passen, m\"ussen auch zu $P_n$ passen
1.189 +\end{enumerate}
1.190 +Zuerst ein Beispiel für die ersten zwei Punkte:
1.191 +{\footnotesize\begin{verbatim}
1.192 +> refine;
1.193 +val it = fn : fmz_ -> pblID -> SpecifyTools.match list
1.194 +> val fmz = ["equality (sqrt(9 + 4 * x)=sqrt x
1.195 ++ sqrt (5 + x))",
1.196 +# "soleFor x","errorBound (eps=0)",
1.197 +# "solutions L"];
1.198 +val fmz =
1.199 +["equality (sqrt(9 + 4 * x)=sqrt x + sqrt (5 + x))", "soleFor x",
1.200 +"errorBound (eps=0)", ...] : string list
1.201 +> refine fmz ["univariate","equation"];
1.202 +*** pass ["equation","univariate"]
1.203 +*** comp_dts: ??.empty $ soleFor x
1.204 +Exception- ERROR raised
1.205 +\end{verbatim}
1.206 +Wenn die ersten zwei Regeln nicht angewendet werden k\"onnen, wird die dritte verwendet:
1.207 +{\footnotesize\begin{verbatim}
1.208 +> val fmz = ["equality (x + 1 = 2)",
1.209 +# "solveFor x","errorBound (eps=0)",
1.210 +# "solutions L"];
1.211 +val fmz = ["equality (x + 1 = 2)", "solveFor x", "errorBound (eps=0)", ...]
1.212 +: string list
1.213 +> refine fmz ["univariate","equation"];
1.214 +*** pass ["equation","univariate"]
1.215 +*** pass ["equation","univariate","linear"]
1.216 +*** pass ["equation","univariate","root"]
1.217 +*** pass ["equation","univariate","rational"]
1.218 +*** pass ["equation","univariate","polynomial" ]
1.219 +*** pass ["equation","univariate","polynomial","degree_0"]
1.220 +*** pass ["equation","univariate","polynomial","degree_1"]
1.221 +*** pass ["equation","univariate","polynomial","degree_2"]
1.222 +*** pass ["equation","univariate","polynomial","degree_3"]
1.223 +*** pass ["equation","univariate","polynomial","degree_4"]
1.224 +*** pass ["equation","univariate","polynomial","normalize"]
1.225 +val it =
1.226 +[Matches
1.227 +(["univariate", "equation"],
1.228 +{Find = [Correct "solutions L"], With = [...], ...}),
1.229 +NoMatch (["linear", "univariate", ...], {Find = [...], ...}),
1.230 +NoMatch (["root", ...], ...), ...] : SpecifyTools.match list
1.231 +\end{verbatim}
1.232 +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.233
1.234
1.235 \chapter{Methods}
1.236 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.237 -
1.238 \section{Der ''Syntax`` des Scriptes}
1.239 Syntax beschreibt den Zusammenhang der einzelnen Zeichen und Zeichenfolgen mit den Theorien.
1.240 Er kann so definiert werden:
1.241 @@ -538,7 +763,24 @@
1.242 \end{description}
1.243
1.244
1.245 -hallo
1.246 +
1.247 +\chapter{Befehle von \isac{}}
1.248 +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.249 +\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 die Taktik verwendet.
1.250 +\newline \textbf{Init\_Proof} bildet mit einem ''proof tree`` ein leeres Modell.
1.251 +\newline \textbf{Model\_Problem problem} bestimmt ein problemtype, das wom\"oglich in der ''hierachy`` gefunden wurde, und verwendet es f\"u das Umformen.
1.252 +\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 Taktik und Formel von einer Liste w\"ahlen will.
1.253 +\newline \textbf{Specify\_Theorie theory, Specify\_Problem proble, Specify\_Method method} gibt das entsprechende Element des Basiswissens an.
1.254 +\newline \textbf{Refine\_Problem problem} sucht nach einem Problem in der hierachy, das auf das vorhandene zutrifft.
1.255 +\newline \textbf{Apply\_Method method} beendet das Modell und die Beschreibung. Danach wird die L\"osungmeldung ge\"offnet.
1.256 +\newline \textbf{Free\_Solve} beginnt eine L\"osungsmeldung ohne die Hilfe eine method.
1.257 +\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.258 +\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.259 +\newline \textbf{Rewrite\_Set ruleset} hat \"ahnliche Funktionen wie Rewrite, gilt aber f\"ur einen ganzen Satz von Theorems, dem rule set.
1.260 +\newline \textbf{Rewrite\_Inst (substitution, theorem), Rewrite\_Set\_Inst (substitution, rule set)} ist vergleichbar mit besonderen Taktiken, ersetzt aber Konstanten in der Theorem, bevor es zu einer Anwendung kommt.
1.261 +
1.262 +
1.263 +
1.264
1.265
1.266
1.267 @@ -548,379 +790,6 @@
1.268 \newpage
1.269 ------------------------------- ALTER TEXT -------------------------------
1.270
1.271 -\chapter{The hierarchy of problem types}\label{pbt}
1.272 -\section{The standard-function for 'matching'}
1.273 -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:
1.274 -{\footnotesize\begin{verbatim}
1.275 - ML> matches;
1.276 - val it = fn : theory -> term -> term -> bool
1.277 -\end{verbatim}}%size
1.278 -where the first of the two {\tt term} arguments is the particular term to be tested, and the second one is the pattern:
1.279 -{\footnotesize\begin{verbatim}
1.280 - ML> val t = (term_of o the o (parse thy)) "#3 * x^^^#2 = #1";
1.281 - val t = Const (#,#) $ (# $ # $ (# $ #)) $ Free ("#1","RealDef.real") : term
1.282 - ML>
1.283 - ML> val p = (term_of o the o (parse thy)) "a * b^^^#2 = c";
1.284 - val p = Const (#,#) $ (# $ # $ (# $ #)) $ Free ("c","RealDef.real") : term
1.285 - ML> atomt p;
1.286 - *** -------------
1.287 - *** Const ( op =)
1.288 - *** . Const ( op *)
1.289 - *** . . Free ( a, )
1.290 - *** . . Const ( RatArith.pow)
1.291 - *** . . . Free ( b, )
1.292 - *** . . . Free ( #2, )
1.293 - *** . Free ( c, )
1.294 - val it = () : unit
1.295 - ML>
1.296 - ML> free2var;
1.297 - val it = fn : term -> term
1.298 - ML>
1.299 - ML> val pat = free2var p;
1.300 - val pat = Const (#,#) $ (# $ # $ (# $ #)) $ Var ((#,#),"RealDef.real") : term
1.301 - ML> Sign.string_of_term (sign_of thy) pat;
1.302 - val it = "?a * ?b ^^^ #2 = ?c" : cterm'
1.303 - ML> atomt pat;
1.304 - *** -------------
1.305 - *** Const ( op =)
1.306 - *** . Const ( op *)
1.307 - *** . . Var ((a, 0), )
1.308 - *** . . Const ( RatArith.pow)
1.309 - *** . . . Var ((b, 0), )
1.310 - *** . . . Free ( #2, )
1.311 - *** . Var ((c, 0), )
1.312 - val it = () : unit
1.313 -\end{verbatim}}%size % $
1.314 -Note that the pattern {\tt pat} contains so-called {\it scheme variables} decorated with a {\tt ?} (analoguous to theorems). The pattern is generated by the function {\tt free2var}. This format of the pattern is necessary in order to obtain results like these:
1.315 -{\footnotesize\begin{verbatim}
1.316 - ML> matches thy t pat;
1.317 - val it = true : bool
1.318 - ML>
1.319 - ML> val t2 = (term_of o the o (parse thy)) "x^^^#2 = #1";
1.320 - val t2 = Const (#,#) $ (# $ # $ Free #) $ Free ("#1","RealDef.real") : term
1.321 - ML> matches thy t2 pat;
1.322 - val it = false : bool
1.323 - ML>
1.324 - ML> val pat2 = (term_of o the o (parse thy)) "?u^^^#2 = ?v";
1.325 - val pat2 = Const (#,#) $ (# $ # $ Free #) $ Var ((#,#),"RealDef.real") : term
1.326 - ML> matches thy t2 pat2;
1.327 - val it = true : bool
1.328 -\end{verbatim}}%size % $
1.329 -
1.330 -\section{Accessing the hierarchy}
1.331 -The hierarchy of problem types is encapsulated; it can be accessed by the following functions. {\tt show\_ptyps} retrieves all leaves of the hierarchy (here in an early version for testing):
1.332 -{\footnotesize\begin{verbatim}
1.333 - ML> show_ptyps;
1.334 - val it = fn : unit -> unit
1.335 - ML> show_ptyps();
1.336 - [
1.337 - ["e_pblID"],
1.338 - ["equation", "univariate", "linear"],
1.339 - ["equation", "univariate", "plain_square"],
1.340 - ["equation", "univariate", "polynomial", "degree_two", "pq_formula"],
1.341 - ["equation", "univariate", "polynomial", "degree_two", "abc_formula"],
1.342 - ["equation", "univariate", "squareroot"],
1.343 - ["equation", "univariate", "normalize"],
1.344 - ["equation", "univariate", "sqroot-test"],
1.345 - ["function", "derivative_of"],
1.346 - ["function", "maximum_of", "on_interval"],
1.347 - ["function", "make"],
1.348 - ["tool", "find_values"],
1.349 - ["functional", "inssort"]
1.350 - ]
1.351 - val it = () : unit
1.352 -\end{verbatim}}%size
1.353 -The retrieve function for individual problem types is {\tt get\_pbt}
1.354 -\footnote{A function providing better readable output is in preparation}. Note that its argument, the 'problem identifier' {\tt pblID}, has the strings listed in reverse order w.r.t. the hierarchy, i.e. from the leave to the root. This order makes the {\tt pblID} closer to a natural description:
1.355 -{\footnotesize\begin{verbatim}
1.356 - ML> get_pbt;
1.357 - val it = fn : pblID -> pbt
1.358 - ML> get_pbt ["squareroot", "univariate", "equation"];
1.359 - val it =
1.360 - {met=[("SqRoot.thy","square_equation")],
1.361 - ppc=[("#Given",(Const (#,#),Free (#,#))),
1.362 - ("#Given",(Const (#,#),Free (#,#))),
1.363 - ("#Given",(Const (#,#),Free (#,#))),
1.364 - ("#Find",(Const (#,#),Free (#,#)))],
1.365 - thy={ProtoPure, CPure, HOL, Ord, Set, subset, equalities, mono, Vimage, Fun,
1.366 - Prod, Lfp, Relation, Trancl, WF, NatDef, Gfp, Sum, Inductive, Nat,
1.367 - Arith, Divides, Power, Finite, Equiv, IntDef, Int, Univ, Datatype,
1.368 - Numeral, Bin, IntArith, WF_Rel, Recdef, IntDiv, NatBin, List, Option,
1.369 - Map, Record, RelPow, Sexp, String, Calculation, SVC_Oracle, Main,
1.370 - Zorn, Filter, PNat, PRat, PReal, RealDef, RealOrd, RealInt, RealBin,
1.371 - HyperDef, Descript, ListG, Tools, Script, Typefix, Atools, RatArith,
1.372 - SqRoot},
1.373 - where_=[Const ("SqRoot.contains'_root","bool => bool") $
1.374 - Free ("e_","bool")]} : pbt
1.375 -\end{verbatim}}%size %$
1.376 -where the records fields hold the following data:
1.377 -\begin{description}
1.378 -\item [\tt thy]: the theory necessary for parsing the formulas
1.379 -\item [\tt ppc]: the items of the problem type, divided into those {\tt Given}, the precondition {\tt Where} and the output item(s) {\tt Find}. The items of {\tt Given} and {\tt Find} are all headed by so-called descriptions, which determine the type. These descriptions are defined in {\tt [isac-src]/Isa99/Descript.thy}.
1.380 -\item [\tt met]: the list of methods solving this problem type.\\
1.381 -\end{description}
1.382 -
1.383 -The following function adds or replaces a problem type (after having it prepared using {\tt prep\_pbt})
1.384 -{\footnotesize\begin{verbatim}
1.385 - ML> store_pbt;
1.386 - val it = fn : pbt * pblID -> unit
1.387 - ML> store_pbt
1.388 - (prep_pbt SqRoot.thy
1.389 - (["newtype","univariate","equation"],
1.390 - [("#Given" ,["equality e_","solveFor v_","errorBound err_"]),
1.391 - ("#Where" ,["contains_root (e_::bool)"]),
1.392 - ("#Find" ,["solutions v_i_"])
1.393 - ],
1.394 - [("SqRoot.thy","square_equation")]));
1.395 - val it = () : unit
1.396 -\end{verbatim}}%size
1.397 -When adding a new type with argument {\tt pblID}, an immediate parent must already exist in the hierarchy (this is the one with the tail of {\tt pblID}).
1.398 -
1.399 -\section{Internals of the datastructure}
1.400 -This subsection only serves for the implementation of the hierarchy browser and can be skipped by the authors of math knowledge.
1.401 -
1.402 -A problem type is described by the following record type (in the file {\tt [isac-src]/globals.sml}, the respective functions are in {\tt [isac-src]/ME/ptyps.sml}), and held in a global reference variable:
1.403 -{\footnotesize\begin{verbatim}
1.404 - type pbt =
1.405 - {thy : theory, (* the nearest to the root,
1.406 - which allows to compile that pbt *)
1.407 - where_: term list, (* where - predicates *)
1.408 - ppc : ((string * (* fields "#Given","#Find" *)
1.409 - (term * (* description *)
1.410 - term)) (* id *)
1.411 - list),
1.412 - met : metID list}; (* methods solving the pbt *)
1.413 - datatype ptyp =
1.414 - Ptyp of string * (* key within pblID *)
1.415 - pbt list * (* several pbts with different domIDs*)
1.416 - ptyp list;
1.417 - val e_Ptyp = Ptyp ("empty",[],[]);
1.418 -
1.419 - type ptyps = ptyp list;
1.420 - val ptyps = ref ([e_Ptyp]:ptyps);
1.421 -\end{verbatim}}%size
1.422 -The predicates in {\tt where\_} (i.e. the preconditions) usually are defined in the respective theory in {\tt[isac-src]/knowledge}. Most of the predicates are not defined by rewriting, but by SML-code contained in the respective {\tt *.ML} file.
1.423 -
1.424 -Each item is headed by a so-called description which provides some guidance for interactive input. The descriptions are defined in {\tt[isac-src]/Isa99/Descript.thy}.
1.425 -
1.426 -
1.427 -
1.428 -\section{Match a formalization with a problem type}\label{pbl}
1.429 -A formalization is {\it match}ed with a problem type which yields a problem. A formal description of this kind of {\it match}ing can be found in \\{\tt ftp://ft.ist.tugraz.at/projects/isac/publ/calculemus01.ps.gz}. A formalization of an equation is e.g.
1.430 -{\footnotesize\begin{verbatim}
1.431 - ML> val fmz = ["equality (#1 + #2 * x = #0)",
1.432 - "solveFor x",
1.433 - "solutions L"] : fmz;
1.434 - val fmz = ["equality (#1 + #2 * x = #0)","solveFor x","solutions L"] : fmz
1.435 -\end{verbatim}}%size
1.436 -Given a formalization (and a specification of the problem, i.e. a theory, a problemtype, and a method) \isac{} can solve the respective problem automatically. The formalization must match the problem type for this purpose:
1.437 -{\footnotesize\begin{verbatim}
1.438 - ML> match_pbl;
1.439 - val it = fn : fmz -> pbt -> match'
1.440 - ML>
1.441 - ML> match_pbl fmz (get_pbt ["univariate","equation"]);
1.442 - val it =
1.443 - Matches'
1.444 - {Find=[Correct "solutions L"],
1.445 - Given=[Correct "equality (#1 + #2 * x = #0)",Correct "solveFor x"],
1.446 - Relate=[],Where=[Correct "matches (?a = ?b) (#1 + #2 * x = #0)"],With=[]}
1.447 - : match'
1.448 - ML>
1.449 - ML> match_pbl fmz (get_pbt ["linear","univariate","equation"]);
1.450 - val it =
1.451 - Matches'
1.452 - {Find=[Correct "solutions L"],
1.453 - Given=[Correct "equality (#1 + #2 * x = #0)",Correct "solveFor x"],
1.454 - Relate=[],
1.455 - Where=[Correct
1.456 - "matches ( x = #0) (#1 + #2 * x = #0) |
1.457 - matches ( ?b * x = #0) (#1 + #2 * x = #0) |
1.458 - matches (?a + x = #0) (#1 + #2 * x = #0) |
1.459 - matches (?a + ?b * x = #0) (#1 + #2 * x = #0)"],
1.460 - With=[]} : match'
1.461 - ML>
1.462 - ML> match_pbl fmz (get_pbt ["squareroot","univariate","equation"]);
1.463 - val it =
1.464 - NoMatch'
1.465 - {Find=[Correct "solutions L"],
1.466 - Given=[Correct "equality (#1 + #2 * x = #0)",Correct "solveFor x",
1.467 - Missing "errorBound err_"],Relate=[],
1.468 - Where=[False "contains_root #1 + #2 * x = #0 "],With=[]} : match'
1.469 -\end{verbatim}}%size
1.470 -The above formalization does not match the problem type \\{\tt["squareroot","univariate","equation"]} which is explained by the tags:
1.471 -\begin{tabbing}
1.472 -123\=\kill
1.473 -\> {\tt Missing:} the item is missing in the formalization as required by the problem type\\
1.474 -\> {\tt Superfl:} the item is not required by the problem type\\
1.475 -\> {\tt Correct:} the item is correct, or the precondition ({\tt Where}) is true\\
1.476 -\> {\tt False:} the precondition ({\tt Where}) is false\\
1.477 -\> {\tt Incompl:} the item is incomlete, or not yet input.\\
1.478 -\end{tabbing}
1.479 -
1.480 -
1.481 -
1.482 -\section{Refine a problem specification}
1.483 -The challenge in constructing the problem hierarchy is, to design the branches in such a way, that problem refinement can be done automatically (as it is done in algebra system e.g. by a internal hierarchy of equations).
1.484 -
1.485 -For this purpose the hierarchy must be built using the following rules: Let $F$ be a formalization and $P$ and $P_i,\:i=1\cdots n$ problem types, where the $P_i$ are specialized problem types w.r.t. $P$ (i.e. $P$ is a parent node of $P_i$), then
1.486 -{\small
1.487 -\begin{enumerate}
1.488 -\item for all $F$ matching some $P_i$ must follow, that $F$ matches $P$
1.489 -\item an $F$ matching $P$ should not have more than {\em one} $P_i,\:i=1\cdots n-1$ with $F$ matching $P_i$ (if there are more than one $P_i$, the first one will be taken)
1.490 -\item for all $F$ matching some $P$ must follow, that $F$ matches $P_n$\\
1.491 -\end{enumerate}}%small
1.492 -\noindent Let us give an example for the point (1.) and (2.) first:
1.493 -{\footnotesize\begin{verbatim}
1.494 - ML> refine;
1.495 - val it = fn : fmz -> pblID -> match list
1.496 - ML>
1.497 - ML> val fmz = ["equality (sqrt(#9+#4*x)=sqrt x + sqrt(#5+x))",
1.498 - "solveFor x","errorBound (eps=#0)",
1.499 - "solutions L"];
1.500 - ML>
1.501 - ML> refine fmz ["univariate","equation"];
1.502 - *** pass ["equation","univariate"]
1.503 - *** pass ["equation","univariate","linear"]
1.504 - *** pass ["equation","univariate","plain_square"]
1.505 - *** pass ["equation","univariate","polynomial"]
1.506 - *** pass ["equation","univariate","squareroot"]
1.507 - val it =
1.508 - [Matches
1.509 - (["univariate","equation"],
1.510 - {Find=[Correct "solutions L"],
1.511 - Given=[Correct "equality (sqrt (#9 + #4 * x) = sqrt x + sqrt (#5 + x))",
1.512 - Correct "solveFor x",Superfl "errorBound (eps = #0)"],Relate=[],
1.513 - Where=[Correct
1.514 - "matches (?a = ?b) (sqrt (#9 + #4 * x) = sqrt x + sqrt (#5 + x))"],
1.515 - With=[]}),
1.516 - NoMatch
1.517 - (["linear","univariate","equation"],
1.518 - {Find=[Correct "solutions L"],
1.519 - Given=[Correct "equality (sqrt (#9 + #4 * x) = sqrt x + sqrt (#5 + x))",
1.520 - Correct "solveFor x",Superfl "errorBound (eps = #0)"],Relate=[],
1.521 - Where=[False "(?a + ?b * x = #0) (sqrt (#9 + #4 * x#"],
1.522 - With=[]}),
1.523 - NoMatch
1.524 - (["plain_square","univariate","equation"],
1.525 - {Find=[Correct "solutions L"],
1.526 - Given=[Correct "equality (sqrt (#9 + #4 * x) = sqrt x + sqrt (#5 + x))",
1.527 - Correct "solveFor x",Superfl "errorBound (eps = #0)"],Relate=[],
1.528 - Where=[False
1.529 - "matches (?a + ?b * x ^^^ #2 = #0)"],
1.530 - With=[]}),
1.531 - NoMatch
1.532 - (["polynomial","univariate","equation"],
1.533 - {Find=[Correct "solutions L"],
1.534 - Given=[Correct "equality (sqrt (#9 + #4 * x) = sqrt x + sqrt (#5 + x))",
1.535 - Correct "solveFor x",Superfl "errorBound (eps = #0)"],Relate=[],
1.536 - Where=[False
1.537 - "is_polynomial_in sqrt (#9 + #4 * x) = sqrt x + sqrt (#5 + x) x"],
1.538 - With=[]}),
1.539 - Matches
1.540 - (["squareroot","univariate","equation"],
1.541 - {Find=[Correct "solutions L"],
1.542 - Given=[Correct "equality (sqrt (#9 + #4 * x) = sqrt x + sqrt (#5 + x))",
1.543 - Correct "solveFor x",Correct "errorBound (eps = #0)"],Relate=[],
1.544 - Where=[Correct
1.545 - "contains_root sqrt (#9 + #4 * x) = sqrt x + sqrt (#5 + x) "],
1.546 - With=[]})] : match list
1.547 -\end{verbatim}}%size}%footnotesize\label{refine}
1.548 -This example shows, that in order to refine an {\tt["univariate","equation"]}, the formalization must match respective respective problem type (rule (1.)) and one of the descendants which should match selectively (rule (2.)).
1.549 -
1.550 -If no one of the descendants of {\tt["univariate","equation"]} match, rule (3.) comes into play: The {\em last} problem type on this level ($P_n$) provides for a special 'problem type' {\tt["normalize"]}. This node calls a method transforming the equation to a (or another) normal form, which then may match. Look at this example:
1.551 -{\footnotesize\begin{verbatim}
1.552 - ML> val fmz = ["equality (x+#1=#2)",
1.553 - "solveFor x","errorBound (eps=#0)",
1.554 - "solutions L"];
1.555 - [...]
1.556 - ML>
1.557 - ML> refine fmz ["univariate","equation"];
1.558 - *** pass ["equation","univariate"]
1.559 - *** pass ["equation","univariate","linear"]
1.560 - *** pass ["equation","univariate","plain_square"]
1.561 - *** pass ["equation","univariate","polynomial"]
1.562 - *** pass ["equation","univariate","squareroot"]
1.563 - *** pass ["equation","univariate","normalize"]
1.564 - val it =
1.565 - [Matches
1.566 - (["univariate","equation"],
1.567 - {Find=[Correct "solutions L"],
1.568 - Given=[Correct "equality (x + #1 = #2)",Correct "solveFor x",
1.569 - Superfl "errorBound (eps = #0)"],Relate=[],
1.570 - Where=[Correct "matches (?a = ?b) (x + #1 = #2)"],With=[]}),
1.571 - NoMatch
1.572 - (["linear","univariate","equation"],
1.573 - [...]
1.574 - With=[]}),
1.575 - NoMatch
1.576 - (["squareroot","univariate","equation"],
1.577 - {Find=[Correct "solutions L"],
1.578 - Given=[Correct "equality (x + #1 = #2)",Correct "solveFor x",
1.579 - Correct "errorBound (eps = #0)"],Relate=[],
1.580 - Where=[False "contains_root x + #1 = #2 "],With=[]}),
1.581 - Matches
1.582 - (["normalize","univariate","equation"],
1.583 - {Find=[Correct "solutions L"],
1.584 - Given=[Correct "equality (x + #1 = #2)",Correct "solveFor x",
1.585 - Superfl "errorBound (eps = #0)"],Relate=[],Where=[],With=[]})]
1.586 - : match list
1.587 -\end{verbatim}}%size
1.588 -The problem type $P_n$, {\tt["normalize","univariate","equation"]}, will transform the equation {\tt x + \#1 = \#2} to the normal form {\tt \#-1 + x = \#0}, which then will match {\tt["linear","univariate","equation"]}.
1.589 -
1.590 -This recursive search on the problem hierarchy can be done within a proof state. This leads to the next section.
1.591 -
1.592 -
1.593 -\chapter{Methods}\label{met}
1.594 -A problem type can have one ore more methods solving a respective problem. A method is described by means of another new program language. The language itself looks like a simple functional language, but constructs an imperative proof-state behind the scenes (thus liberating the programer from dealing with technical details and also prohibiting incorrect construction of the proof tree). The interpreter of 'scripts' written in this language evaluates the scriptexpressions, and also delivers certain parts of the script itself for discussion with the user.
1.595 -
1.596 -\section{The scripts' syntax}
1.597 -The syntax of scripts follows the definition given in Backus-normal-form:
1.598 -{\it
1.599 -\begin{tabbing}
1.600 -123\=123\=expr ::=\=$|\;\;$\=\kill
1.601 -\>script ::= {\tt Script} id arg$\,^*$ = body\\
1.602 -\>\>arg ::= id $\;|\;\;($ ( id :: type ) $)$\\
1.603 -\>\>body ::= expr\\
1.604 -\>\>expr ::= \>\>{\tt let} id = expr $($ ; id = expr$)^*$ {\tt in} expr\\
1.605 -\>\>\>$|\;$\>{\tt if} prop {\tt then} expr {\tt else} expr\\
1.606 -\>\>\>$|\;$\>listexpr\\
1.607 -\>\>\>$|\;$\>id\\
1.608 -\>\>\>$|\;$\>seqex id\\
1.609 -\>\>seqex ::= \>\>{\tt While} prop {\tt Do} seqex\\
1.610 -\>\>\>$|\;$\>{\tt Repeat} seqex\\
1.611 -\>\>\>$|\;$\>{\tt Try} seqex\\
1.612 -\>\>\>$|\;$\>seqex {\tt Or} seqex\\
1.613 -\>\>\>$|\;$\>seqex {\tt @@} seqex\\
1.614 -\>\>\>$|\;$\>tac $($ id $|$ listexpr $)^*$\\
1.615 -\>\>type ::= id\\
1.616 -\>\>tac ::= id
1.617 -\end{tabbing}}
1.618 -where {\it id} is an identifier with the usual syntax, {\it prop} is a proposition constructed by Isabelles logical operators (see \cite{Isa-obj} {\tt [isabelle]/src/HOL/HOL.thy}), {\it listexpr} (called {\bf list-expression}) is constructed by Isabelles list functions like {\tt hd, tl, nth} described in {\tt [isabelle]/src/HOL/List.thy}, and {\it type} are (virtually) all types declared in Isabelles version 99.
1.619 -
1.620 -Expressions containing some of the keywords {\tt let}, {\tt if} etc. are called {\bf script-expressions}.
1.621 -
1.622 -Tactics {\it tac} are (curried) functions. For clarity and simplicity reasons, {\it listexpr} must not contain a {\it tac}, and {\it tac}s must not be nested,
1.623 -
1.624 -
1.625 -\section{Control the flow of evaluation}
1.626 -The flow of control is managed by the following script-expressions called {\it tacticals}.
1.627 -\begin{description}
1.628 -\item{{\tt while} prop {\tt Do} expr id}
1.629 -\item{{\tt if} prop {\tt then} expr {\tt else} expr}
1.630 -\end{description}
1.631 -While the the above script-expressions trigger the flow of control by evaluating the current formula, the other expressions depend on the applicability of the tactics within their respective subexpressions (which in turn depends on the proofstate)
1.632 -\begin{description}
1.633 -\item{{\tt Repeat} expr id}
1.634 -\item{{\tt Try} expr id}
1.635 -\item{expr {\tt Or} expr id}
1.636 -\item{expr {\tt @@} expr id}
1.637 -\end{description}
1.638 -
1.639 -\begin{description}
1.640 -\item xxx
1.641 -
1.642 -\end{description}
1.643 -
1.644 \chapter{Do a calculational proof}
1.645 First we list all the tactics available so far (this list may be extended during further development of \isac).
1.646