1 %WN051006 dropped in code, but interesting for case study 'order a list' |
|
2 %EqSystem.thy |
|
3 %--------------------------------------------------------------------------- |
|
4 % |
|
5 % order'_system :: "bool list => bool list " ("order'_system _") |
|
6 % |
|
7 %EqSystem.ML |
|
8 %--------------------------------------------------------------------------- |
|
9 %(*("order_system", ("EqSystem.order'_system", |
|
10 % eval_order_system "#eval_order_system_"))*) |
|
11 %fun eval_order_system _ "EqSystem.order'_system" |
|
12 % (p as (Const ("EqSystem.order'_system",_) $ ts)) _ = |
|
13 % let val ts' = sort (ord_simplify_Integral_ false (assoc_thy"Isac.thy") []) |
|
14 % (isalist2list ts) |
|
15 % val ts'' = list2isalist HOLogic.boolT ts' |
|
16 % in if ts <> ts'' |
|
17 % then Some (term2str p ^ " = " ^ term2str ts'', |
|
18 % Trueprop $ (mk_equality (p,ts''))) |
|
19 % else None |
|
20 % end |
|
21 % | eval_order_system _ _ _ _ = None; |
|
22 % |
|
23 % |
|
24 %"Script Norm2SystemScript (es_::bool list) (vs_::real list) = \ |
|
25 %\ (let es__ = Try (Rewrite_Set simplify_Integral_parenthesized False) es_; \ |
|
26 %\ es__ = (Try (Calculate order_system_) (order_system es__))\ |
|
27 %\in (SubProblem (Biegelinie_,[linear,system],[no_met])\ |
|
28 %\ [bool_list_ es__, real_list_ vs_]))" |
|
29 % )); |
|
30 % |
|
31 %eqsystem.sml |
|
32 %--------------------------------------------------------------------------- |
|
33 %"----------- eval_sort -------------------------------------------"; |
|
34 %"----------- eval_sort -------------------------------------------"; |
|
35 %"----------- eval_sort -------------------------------------------"; |
|
36 %val ts = str2term "[c_2 = 0, -1 * (q_0 * L ^^^ 2) / 2 + (L * c + c_2) = 0]"; |
|
37 %val ts' = sort (ord_simplify_Integral_ false (assoc_thy"Isac.thy") []) |
|
38 % (isalist2list ts); |
|
39 %terms2str ts'; |
|
40 %val ts'' = list2isalist HOLogic.boolT ts'; |
|
41 %if term2str ts'' = "[-1 * (q_0 * L ^^^ 2) / 2 + (L * c + c_2) = 0, c_2 = 0]" |
|
42 %then () else raise error "eqsystem.sml eval_sort 1"; |
|
43 % |
|
44 %val t = str2term "order_system [c_2 = 0,\ |
|
45 % \-1 * (q_0 * L ^^^ 2) / 2 + (L * c + c_2) = 0]"; |
|
46 %val Some (str,_) = eval_order_system "" "EqSystem.order'_system" t ""; |
|
47 %if str = "order_system [c_2 = 0, -1 * (q_0 * L ^^^ 2) / 2 + (L * c + c_2) = 0] = [-1 * (q_0 * L ^^^ 2) / 2 + (L * c + c_2) = 0, c_2 = 0]" then () |
|
48 %else raise error "eqsystem.sml eval_sort 2"; |
|
49 % |
|
50 % |
|
51 % |
|
52 % calculate_ thy ("EqSystem.order'_system", |
|
53 % eval_order_system "#eval_order_system_") t; |
|
54 % |
|
55 %--------------------------------------------------------------------------- |
|
56 %--------------------------------------------------------------------------- |
|
57 %--------------------------------------------------------------------------- |
|
58 |
|
59 |
|
60 %In the following this text is not compatible with isac-code: |
|
61 %* move termorder to knowledge: FIXXXmat0201a |
|
62 % |
|
63 % |
|
64 |
|
65 \documentclass[11pt,a4paper,headline,headcount,towside,nocenter]{report} |
|
66 \usepackage{latexsym} % recommended by Ch.Schinagl 10.98 |
|
67 \bibliographystyle{alpha} |
|
68 |
|
69 \def\isac{${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$} |
|
70 |
|
71 \title{\isac --- Interface for\\ |
|
72 Developers of Math Knowledge\\[1.0ex] |
|
73 and\\[1.0ex] |
|
74 Tools for Experiments in\\ |
|
75 Symbolic Computation\\[1.0ex]} |
|
76 \author{The \isac-Team\\ |
|
77 \tt isac-users@ist.tugraz.at\\[1.0ex]} |
|
78 \date{\today} |
|
79 |
|
80 \begin{document} |
|
81 \maketitle |
|
82 \newpage |
|
83 \tableofcontents |
|
84 \newpage |
|
85 \listoftables |
|
86 \newpage |
|
87 |
|
88 \chapter{Introduction} |
|
89 \section{The scope of this document} |
|
90 \paragraph{As a manual:} This document describes the interface to \isac's kernel (KE), the interface to the mathematics engine (ME) included in the KE, and to the various tools like rewriting, matching etc. |
|
91 |
|
92 \isac's KE is written in SML, the language developed in conjunction with predecessors of the theorem prover Isabelle. Thus, in this document we use the plain ASCII representation of SML code. The reader may note that the \isac-user is presented a completely different view on a graphical user interface. |
|
93 |
|
94 The document is selfcontained; basic knowledge about SML (as an introduction \cite{Paulson:91} is recommended), terms and rewriting is assumed. |
|
95 |
|
96 %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. |
|
97 |
|
98 Notation: SML code, directories, file names are {\tt written in 'tt'}; in particular {\tt ML>} is the KE prompt. |
|
99 |
|
100 \paragraph{Give it a try !} Another aim of this text is to give the reader hints for experiments with the tools introduced. |
|
101 |
|
102 \section{Related documents}\label{related-docs} |
|
103 Isabelle reference manual \cite{Isa-ref}, also contained in the Isabelle distribution under $\sim${\tt /doc/}. |
|
104 |
|
105 {\bf The actual locations of files is being recorded in \\{\tt /software/services/isac/README} |
|
106 \footnote{The KEs current version is {\tt isac.020120-math/} which is based on the version Isabelle99 at {\tt http://isabelle.in.tum.de}.\\ |
|
107 The current locations at IST are\\ |
|
108 {\tt [isabelle]\hspace{3em} /software/sol26/Isabelle99/}\\ |
|
109 {\tt [isac-src]\hspace{3em} /software/services/isac/src/ke/}\\ |
|
110 {\tt [isac-bin]\hspace{3em} /software/services/isac/bin/ke/} |
|
111 } |
|
112 and rigorously updated.} In this document we refer to the following directories |
|
113 \begin{tabbing} |
|
114 xxx\=Isabelle sources1234 \=\kill |
|
115 \>Isabelle sources \> {\tt [isabelle]/}\\ |
|
116 \>KE sources \> {\tt [isac-src]/\dots{version}\dots/}\\ |
|
117 \>KE binary \> {\tt [isac-bin]/\dots{version}\dots/} |
|
118 \end{tabbing} |
|
119 where {\tt\dots version\dots} stands for a directory-name containing information on the version. |
|
120 |
|
121 \section{Getting started} |
|
122 Change to the directory {\tt [isac-bin]} where \isac's binary is located and type to the unix-prompt '$>$' (ask your system administrator where the directory {\tt [isac-bin]} is on your system): |
|
123 \begin{verbatim} |
|
124 > [isac-bin]/sml @SMLload=isac.020120-math |
|
125 val it = false : bool |
|
126 ML> |
|
127 \end{verbatim} |
|
128 yielding the message {\tt val it = false : bool} followed by the prompt of the KE. Having been successful so far, just type in the input presented below -- all of it belongs to {\em one} session~! |
|
129 |
|
130 \part{Experimental approach} |
|
131 |
|
132 \chapter{Basics, terms and parsing} |
|
133 Isabelle implements terms of the {\it simply typed lambda calculus} \cite{typed-lambda} defined in $\sim${\tt/src/Pure.ML}. |
|
134 \section{The definition of terms} |
|
135 There are two kinds of terms in Isabelle, 'raw terms' and 'certified terms'. \isac{} works on raw terms, which are efficient but hard to comprehend. |
|
136 {\footnotesize\begin{verbatim} |
|
137 datatype term = |
|
138 Const of string * typ |
|
139 | Free of string * typ |
|
140 | Var of indexname * typ |
|
141 | Bound of int |
|
142 | Abs of string * typ * term |
|
143 | op $ of term * term; |
|
144 |
|
145 datatype typ = Type of string * typ list |
|
146 | TFree of string * sort |
|
147 | TVar of indexname * sort; |
|
148 \end{verbatim}}%size % $ |
|
149 where the definitions of sort and indexname is not relevant in this context. The {\tt typ}e is being inferred during parsing. Parsing creates the other kind of terms, {\tt cterm}. These {\tt cterm}s are encapsulated records, which cannot be composed without the respective Isabelle functions (checking for type correctness), but which then are conveniently displayed as strings (using SML compiler internals -- see below). |
|
150 |
|
151 \section{Theories and parsing} |
|
152 Parsing uses information contained in Isabelles theories $\sim${\tt /src/HOL}. The currently active theory is held in a global variable {\tt thy}; theories can be accessed individually; |
|
153 {\footnotesize\begin{verbatim} |
|
154 ML> thy; |
|
155 val it = |
|
156 {ProtoPure, CPure, HOL, Ord, Set, subset, equalities, mono, Vimage, Fun, |
|
157 Prod, Lfp, Relation, Trancl, WF, NatDef, Gfp, Sum, Inductive, Nat, Arith, |
|
158 Divides, Power, Finite, Equiv, IntDef, Int, Univ, Datatype, Numeral, Bin, |
|
159 IntArith, WF_Rel, Recdef, IntDiv, NatBin, List, Option, Map, Record, |
|
160 RelPow, Sexp, String, Calculation, SVC_Oracle, Main, Zorn, Filter, PNat, |
|
161 PRat, PReal, RealDef, RealOrd, RealInt, RealBin, HyperDef, Descript, ListG, |
|
162 Tools, Script, Typefix, Atools, RatArith, SqRoot, Differentiate, DiffAppl, |
|
163 InsSort, Isac} : theory ML> |
|
164 ML> HOL.thy; |
|
165 val it = {ProtoPure, CPure, HOL} : theory |
|
166 ML> |
|
167 ML> parse; |
|
168 val it = fn : theory -> string -> cterm option |
|
169 ML> parse thy "a + b * #3"; |
|
170 val it = Some "a + b * #3" : cterm option |
|
171 ML> |
|
172 ML> val t = (term_of o the) it; |
|
173 val t = Const (#,#) $ Free (#,#) $ (Const # $ Free # $ Free (#,#)) : term |
|
174 \end{verbatim}}%size |
|
175 where {\tt term\_of} and {\tt the} are explained below. The syntax of the list of characters can be read out of Isabelles theories \cite{Isa-obj} {\tt [isabelle]/src/HOL/}\footnote{Or you may use your internetbrowser to look at the files in {\tt [isabelle]/browser\_info}.} |
|
176 and from theories developed with in \isac{} at {\tt [isac-src]/knowledge/}. Note that the syntax of the terms is different from those displayed at \isac's frontend after conversion to MathML. |
|
177 |
|
178 |
|
179 \section{Displaying terms} |
|
180 The print depth on the SML top-level can be set in order to produce output in the amount of detail desired: |
|
181 {\footnotesize\begin{verbatim} |
|
182 ML> Compiler.Control.Print.printDepth; |
|
183 val it = ref 4 : int ref |
|
184 ML> |
|
185 ML> Compiler.Control.Print.printDepth:= 2; |
|
186 val it = () : unit |
|
187 ML> t; |
|
188 val it = # $ # $ (# $ #) : term |
|
189 ML> |
|
190 ML> Compiler.Control.Print.printDepth:= 6; |
|
191 val it = () : unit |
|
192 ML> t; |
|
193 val it = |
|
194 Const ("op +","[RealDef.real, RealDef.real] => RealDef.real") $ |
|
195 Free ("a","RealDef.real") $ |
|
196 (Const ("op *","[RealDef.real, RealDef.real] => RealDef.real") $ |
|
197 Free ("b","RealDef.real") $ Free ("#3","RealDef.real")) : term |
|
198 \end{verbatim}}%size % $ |
|
199 A closer look to the latter output shows that {\tt typ} is output as a string like {\tt cterm}. Other useful settings for the output are: |
|
200 {\footnotesize\begin{verbatim} |
|
201 ML> Compiler.Control.Print.printLength; |
|
202 val it = ref 8 : int ref |
|
203 ML> Compiler.Control.Print.stringDepth; |
|
204 val it = ref 250 : int ref |
|
205 \end{verbatim}}%size |
|
206 Anyway, the SML output of terms is not very readable; there are functions in the KE to display them: |
|
207 {\footnotesize\begin{verbatim} |
|
208 ML> atomt; |
|
209 val it = fn : term -> unit |
|
210 ML> atomt t; |
|
211 *** ------------- |
|
212 *** Const ( op +) |
|
213 *** . Free ( a, ) |
|
214 *** . Const ( op *) |
|
215 *** . . Free ( b, ) |
|
216 *** . . Free ( #3, ) |
|
217 val it = () : unit |
|
218 ML> |
|
219 ML> atomty; |
|
220 val it = fn : theory -> term -> unit |
|
221 ML> atomty thy t; |
|
222 *** ------------- |
|
223 *** Const ( op +, [real, real] => real) |
|
224 *** . Free ( a, real) |
|
225 *** . Const ( op *, [real, real] => real) |
|
226 *** . . Free ( b, real) |
|
227 *** . . Free ( #3, real) |
|
228 val it = () : unit |
|
229 \end{verbatim}}%size |
|
230 where again the {\tt typ}s are rendered as strings, but more elegantly by use of the information contained in {\tt thy}.. |
|
231 |
|
232 \paragraph{Give it a try !} {\bf The mathematics knowledge grows} as it is defined in Isabelle theory by theory. Have a look by your internet browser to the hierarchy of those theories at {\tt [isabelle]/src/HOL/HOL.thy} and its children available on your system. Or you may use your internetbrowser to look at the files in {\tt [isabelle]/browser\_info}. |
|
233 {\footnotesize\begin{verbatim} |
|
234 ML> (*-1-*) parse HOL.thy "#2^^^#3"; |
|
235 *** Inner lexical error at: "^^^#3" |
|
236 val it = None : cterm option |
|
237 ML> |
|
238 ML> (*-2-*) parse HOL.thy "d_d x (a + x)"; |
|
239 val it = None : cterm option |
|
240 ML> |
|
241 ML> |
|
242 ML> (*-3-*) parse RatArith.thy "#2^^^#3"; |
|
243 val it = Some "#2 ^^^ #3" : cterm option |
|
244 ML> |
|
245 ML> (*-4-*) parse RatArith.thy "d_d x (a + x)"; |
|
246 val it = Some "d_d x (a + x)" : cterm option |
|
247 ML> |
|
248 ML> |
|
249 ML> (*-5-*) parse Differentiate.thy "d_d x (a + x)"; |
|
250 val it = Some "d_d x (a + x)" : cterm option |
|
251 ML> |
|
252 ML> (*-6-*) parse Differentiate.thy "#2^^^#3"; |
|
253 val it = Some "#2 ^^^ #3" : cterm option |
|
254 \end{verbatim}}%size |
|
255 Don't trust the string representation: if we convert {\tt(*-4-*)} and {\tt(*-6-*)} to terms \dots |
|
256 {\footnotesize\begin{verbatim} |
|
257 ML> (*-4-*) val thy = RatArith.thy; |
|
258 ML> ((atomty thy) o term_of o the o (parse thy)) "d_d x (a + x)"; |
|
259 *** ------------- |
|
260 *** Free ( d_d, [real, real] => real) |
|
261 *** . Free ( x, real) |
|
262 *** . Const ( op +, [real, real] => real) |
|
263 *** . . Free ( a, real) |
|
264 *** . . Free ( x, real) |
|
265 val it = () : unit |
|
266 ML> |
|
267 ML> (*-6-*) val thy = Differentiate.thy; |
|
268 ML> ((atomty thy) o term_of o the o (parse thy)) "d_d x (a + x)"; |
|
269 *** ------------- |
|
270 *** Const ( Differentiate.d_d, [real, real] => real) |
|
271 *** . Free ( x, real) |
|
272 *** . Const ( op +, [real, real] => real) |
|
273 *** . . Free ( a, real) |
|
274 *** . . Free ( x, real) |
|
275 val it = () : unit |
|
276 \end{verbatim}}%size |
|
277 \dots we see: in {\tt(*-4-*)} we have an arbitrary function {\tt Free ( d\_d, \_)} and in {\tt(*-6-*)} we have the special function constant {\tt Const ( Differentiate.d\_d, \_)} for differentiation, which is defined in {\tt Differentiate.thy} and presumerably is meant. |
|
278 |
|
279 |
|
280 \section{Converting terms} |
|
281 The conversion from {\tt cterm} to {\tt term} has been shown above: |
|
282 {\footnotesize\begin{verbatim} |
|
283 ML> term_of; |
|
284 val it = fn : cterm -> term |
|
285 ML> |
|
286 ML> the; |
|
287 val it = fn : 'a option -> 'a |
|
288 ML> |
|
289 ML> val t = (term_of o the o (parse thy)) "a + b * #3"; |
|
290 val t = Const (#,#) $ Free (#,#) $ (Const # $ Free # $ Free (#,#)) : term |
|
291 \end{verbatim}}%size |
|
292 where {\tt the} unwraps the {\tt term option} --- an auxiliary function from Larry Paulsons basic library at {\tt [isabelle]/src/Pure/library.ML}, which is really worthwile to study for any SML programmer. |
|
293 |
|
294 The other conversions are the following, some of which use the {\it signature} {\tt sign} of a theory: |
|
295 {\footnotesize\begin{verbatim} |
|
296 ML> sign_of; |
|
297 val it = fn : theory -> Sign.sg |
|
298 ML> |
|
299 ML> cterm_of; |
|
300 val it = fn : Sign.sg -> term -> cterm |
|
301 ML> val ct = cterm_of (sign_of thy) t; |
|
302 val ct = "a + b * #3" : cterm |
|
303 ML> |
|
304 ML> Sign.string_of_term; |
|
305 val it = fn : Sign.sg -> term -> string |
|
306 ML> Sign.string_of_term (sign_of thy) t; |
|
307 val it = "a + b * #3" : ctem' |
|
308 ML> |
|
309 ML> string_of_cterm; |
|
310 val it = fn : cterm -> string |
|
311 ML> string_of_cterm ct; |
|
312 val it = "a + b * #3" : ctem' |
|
313 \end{verbatim}}%size |
|
314 |
|
315 \section{Theorems} |
|
316 Theorems are a type, {\tt thm}, even more protected than {\tt cterms}: they are defined as axioms or proven in Isabelle. These definitions and proofs are contained in theories in the directory {\tt[isac-src]/knowledge/}, e.g. the theorem {\tt diff\_sum} in the theory {\tt[isac-src]/knowledge/Differentiate.thy}. Additionally, each theorem has to be recorded for \isac{} in the respective {\tt *.ML}, e.g. {\tt diff\_sum} in {\tt[isac-src]/knowledge/Differentiate.ML} as follows: |
|
317 {\footnotesize\begin{verbatim} |
|
318 ML> theorem' := overwritel (!theorem', |
|
319 [("diff_const",num_str diff_const) |
|
320 ]); |
|
321 \end{verbatim}}%size |
|
322 The additional recording of theorems and other values will disappear in later versions of \isac. |
|
323 |
|
324 \chapter{Rewriting} |
|
325 \section{The arguments for rewriting} |
|
326 The type identifiers of the arguments and values of the rewrite-functions in \ref{rewrite} differ only in an apostroph: the apostrohped types are re-named strings in order to maintain readability. |
|
327 {\footnotesize\begin{verbatim} |
|
328 ML> HOL.thy; |
|
329 val it = {ProtoPure, CPure, HOL} : theory |
|
330 ML> "HOL.thy" : theory'; |
|
331 val it = "HOL.thy" : theory' |
|
332 ML> |
|
333 ML> sqrt_right; |
|
334 val it = fn : rew_ord (* term * term -> bool *) |
|
335 ML> "sqrt_right" : rew_ord'; |
|
336 val it = "sqrt_right" : rew_ord' |
|
337 ML> |
|
338 ML> eval_rls; |
|
339 val it = |
|
340 Rls |
|
341 {preconds=[],rew_ord=("sqrt_right",fn), |
|
342 rules=[Thm #,Thm #,Thm #,Thm #,Thm #,Thm #,Thm #,Thm #, |
|
343 Thm #,Thm #,Thm #,Thm #,Thm #,Calc #,Calc #,...], |
|
344 scr=Script (Free #)} : rls |
|
345 ML> "eval_rls" : rls'; |
|
346 val it = "eval_rls" : rls' |
|
347 ML> |
|
348 ML> diff_sum; |
|
349 val it = "d_d ?bdv (?u + ?v) = d_d ?bdv ?u + d_d ?bdv ?v" : thm |
|
350 ML> ("diff_sum", "") : thm'; |
|
351 val it = ("diff_sum","") : thm' |
|
352 \end{verbatim}}%size |
|
353 where a {\tt thm'} is a pair, eventually with the string-representation of the respective theorem. |
|
354 |
|
355 \section{The functions for rewriting}\label{rewrite} |
|
356 Rewriting comes along with two equivalent functions, where the first is being actually used within the KE, and the second one is useful for tests: |
|
357 {\footnotesize\begin{verbatim} |
|
358 ML> rewrite_; |
|
359 val it = fn |
|
360 : theory |
|
361 -> rew_ord |
|
362 -> rls -> bool -> thm -> term -> (term * term list) option |
|
363 ML> |
|
364 ML> rewrite; |
|
365 val it = fn |
|
366 : theory' |
|
367 -> rew_ord' |
|
368 -> rls' -> bool -> thm' -> cterm' -> (cterm' * cterm' list) option |
|
369 \end{verbatim}}%size |
|
370 The arguments are the following:\\ |
|
371 \tabcolsep=4mm |
|
372 \def\arraystretch{1.5} |
|
373 \begin{tabular}{lp{11.0cm}} |
|
374 {\tt theory} & the Isabelle theory containing the definitions necessary for parsing the {\tt term} \\ |
|
375 {\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 \\ |
|
376 {\tt rls} & the rule set for evaluating the condition within {\tt thm} in case {\tt thm} is a conditional rule \\ |
|
377 {\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 \\ |
|
378 {\tt thm} & the theorem used to try to rewrite {\tt term} \\ |
|
379 {\tt term} & the term eventually rewritten by {\tt thm} \\ |
|
380 \end{tabular}\\ |
|
381 |
|
382 \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:\\ |
|
383 \begin{tabular}{lp{10.4cm}} |
|
384 {\tt term} & the term rewritten \\ |
|
385 {\tt term list}& the assumptions eventually generated if the {\tt bool} flag is set to {\tt true} and {\tt thm} is applicable. \\ |
|
386 \end{tabular}\\ |
|
387 |
|
388 \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: |
|
389 {\footnotesize\begin{verbatim} |
|
390 ML> val thy' = "Differentiate.thy"; |
|
391 val thy' = "Differentiate.thy" : string |
|
392 ML> val ct = "d_d x (x ^^^ #2 + #3 * x + #4)"; |
|
393 val ct = "d_d x (x ^^^ #2 + #3 * x + #4)" : cterm' |
|
394 ML> |
|
395 ML> val thm = ("diff_sum",""); |
|
396 val thm = ("diff_sum","") : thm' |
|
397 ML> val Some (ct,_) = rewrite_inst thy' "tless_true" "eval_rls" true |
|
398 [("bdv","x::real")] thm ct; |
|
399 val ct = "d_d x (x ^^^ #2 + #3 * x) + d_d x #4" : cterm' |
|
400 ML> |
|
401 ML> val Some (ct,_) = rewrite_inst thy' "tless_true" "eval_rls" true |
|
402 [("bdv","x::real")] thm ct; |
|
403 val ct = "d_d x (x ^^^ #2) + d_d x (#3 * x) + d_d x #4" : cterm' |
|
404 ML> |
|
405 ML> val thm = ("diff_prod_const",""); |
|
406 val thm = ("diff_prod_const","") : thm' |
|
407 ML> val Some (ct,_) = rewrite_inst thy' "tless_true" "eval_rls" true |
|
408 [("bdv","x::real")] thm ct; |
|
409 val ct = "d_d x (x ^^^ #2) + #3 * d_d x x + d_d x #4" : cterm' |
|
410 \end{verbatim}}%size |
|
411 You can look up the theorems in {\tt [isac-src]/knowledge/Differentiate.thy} and try to apply them until you get the result you would expect if calculating by hand. |
|
412 \footnote{Hint: At the end you will need {\tt val (ct,\_) = the (rewrite\_set thy' "eval\_rls" false "SqRoot\_simplify" ct);}} |
|
413 |
|
414 \paragraph{Give it a try !}\label{cond-rew} {\bf Conditional rewriting} is a more powerful technique then ordinary rewriting, and is closer to the power of programming languages (see the subsequent 'try it out'~!). The following example expands a term to poynomial form: |
|
415 {\footnotesize\begin{verbatim} |
|
416 ML> val thy' = "Isac.thy"; |
|
417 val thy' = "Isac.thy" : string |
|
418 ML> val ct' = "#3 * a + #2 * (a + #1)"; |
|
419 val ct' = "#3 * a + #2 * (a + #1)" : cterm' |
|
420 ML> |
|
421 ML> val thm' = ("radd_mult_distrib2","?k * (?m + ?n) = ?k * ?m + ?k * ?n"); |
|
422 val thm' = ("radd_mult_distrib2","?k * (?m + ?n) = ?k * ?m + ?k * ?n") |
|
423 : thm' |
|
424 ML> (*1*) val Some (ct',_) = rewrite thy' "tless_true" "eval_rls" true thm' ct'; |
|
425 val ct' = "#3 * a + (#2 * a + #2 * #1)" : cterm' |
|
426 ML> |
|
427 ML> val thm' = ("radd_assoc_RS_sym","?m1 + (?n1 + ?k1) = ?m1 + ?n1 + ?k1"); |
|
428 val thm' = ("radd_assoc_RS_sym","?m1 + (?n1 + ?k1) = ?m1 + ?n1 + ?k1") |
|
429 : thm' |
|
430 ML> (*2*) val Some (ct',_) = rewrite thy' "tless_true" "eval_rls" true thm' ct'; |
|
431 val ct' = "#3 * a + #2 * a + #2 * #1" : cterm' |
|
432 ML> |
|
433 ML> val thm' = ("rcollect_right", |
|
434 "[| ?l is_const; ?m is_const |] ==> ?l * ?n + ?m * ?n = (?l + ?m) * ?n"); |
|
435 val thm' = |
|
436 ("rcollect_right", |
|
437 "[| ?l is_const; ?m is_const |] ==> ?l * ?n + ?m * ?n = (?l + ?m) * ?n") |
|
438 : thm' |
|
439 ML> (*3*) val Some (ct',_) = rewrite thy' "tless_true" "eval_rls" true thm' ct'; |
|
440 val ct' = "(#3 + #2) * a + #2 * #1" : cterm' |
|
441 ML> |
|
442 ML> (*4*) val Some (ct',_) = calculate' thy' "plus" ct'; |
|
443 val ct' = "#5 * a + #2 * #1" : cterm' |
|
444 ML> |
|
445 ML> (*5*) val Some (ct',_) = calculate' thy' "times" ct'; |
|
446 val ct' = "#5 * a + #2" : cterm' |
|
447 \end{verbatim}}%size |
|
448 Note, that the two rules, {\tt radd\_mult\_distrib2} in {\tt(*1*)} and {\tt rcollect\_right} in {\tt(*3*)} would neutralize each other (i.e. a rule set would not terminate), if there would not be the condition {\tt is\_const}. |
|
449 |
|
450 \paragraph{Give it a try !} {\bf Functional programming} can, within a certain range, modeled by rewriting. In {\tt [isac-src]/\dots/tests/InsSort.thy} the following rules can be found, which are able to sort a list ('insertion sort'): |
|
451 {\footnotesize\begin{verbatim} |
|
452 sort_def "sort ls = foldr ins ls []" |
|
453 |
|
454 ins_base "ins [] a = [a]" |
|
455 ins_rec "ins (x#xs) a = (if x < a then x#(ins xs a) else a#(x#xs))" |
|
456 |
|
457 foldr_base "foldr f [] a = a" |
|
458 foldr_rec "foldr f (x#xs) a = foldr f xs (f a x)" |
|
459 |
|
460 if_True "(if True then ?x else ?y) = ?x" |
|
461 if_False "(if False then ?x else ?y) = ?y" |
|
462 \end{verbatim}}%size |
|
463 where {\tt\#} is the list-constructor, {\tt foldr} is the well-known standard function of functional programming, and {\tt if\_True, if\_False} are auxiliary rules. Then the sort may be done by the following rewrites: |
|
464 {\footnotesize\begin{verbatim} |
|
465 ML> val thy' = "InsSort.thy"; |
|
466 val thy' = "InsSort.thy" : theory' |
|
467 ML> val ct = "sort [#1,#3,#2]" : cterm'; |
|
468 val ct = "sort [#1,#3,#2]" : cterm' |
|
469 ML> |
|
470 ML> val thm = ("sort_def",""); |
|
471 ML> val (ct,_) = the (rewrite thy' "tless_true" "eval_rls" false thm ct); |
|
472 val ct = "foldr ins [#1, #3, #2] []" : cterm' |
|
473 ML> |
|
474 ML> val thm = ("foldr_rec",""); |
|
475 ML> val (ct,_) = the (rewrite thy' "tless_true" "eval_rls" false thm ct); |
|
476 val ct = "foldr ins [#3, #2] (ins [] #1)" : cterm' |
|
477 ML> |
|
478 ML> val thm = ("ins_base",""); |
|
479 ML> val (ct,_) = the (rewrite thy' "tless_true" "eval_rls" false thm ct); |
|
480 val ct = "foldr ins [#3, #2] [#1]" : cterm' |
|
481 ML> |
|
482 ML> val thm = ("foldr_rec",""); |
|
483 ML> val (ct,_) = the (rewrite thy' "tless_true" "eval_rls" false thm ct); |
|
484 val ct = "foldr ins [#2] (ins [#1] #3)" : cterm' |
|
485 ML> |
|
486 ML> val thm = ("ins_rec",""); |
|
487 ML> val (ct,_) = the (rewrite thy' "tless_true" "eval_rls" false thm ct); |
|
488 val ct = "foldr ins [#2] (if #1 < #3 then #1 # ins [] #3 else [#3, #1])" |
|
489 : cterm' |
|
490 ML> |
|
491 ML> val (ct,_) = the (calculate' thy' "le" ct); |
|
492 val ct = "foldr ins [#2] (if True then #1 # ins [] #3 else [#3, #1])" : cterm' |
|
493 ML> |
|
494 ML> val thm = ("if_True","(if True then ?x else ?y) = ?x"); |
|
495 ML> val (ct,_) = the (rewrite thy' "tless_true" "eval_rls" false thm ct); |
|
496 val ct = "foldr ins [#2] (#1 # ins [] #3)" : cterm' |
|
497 ML> |
|
498 ... |
|
499 val ct = "sort [#1,#3,#2]" : cterm' |
|
500 \end{verbatim}}%size |
|
501 |
|
502 |
|
503 \section{Variants of rewriting} |
|
504 Some of the above examples already used variants of {\tt rewrite} all of which have the same value, and very similar arguments: |
|
505 {\footnotesize\begin{verbatim} |
|
506 ML> rewrite_inst_; |
|
507 val it = fn |
|
508 : theory |
|
509 -> rew_ord |
|
510 -> rls |
|
511 -> bool |
|
512 -> (cterm' * cterm') list |
|
513 -> thm -> term -> (term * term list) option |
|
514 ML> rewrite_inst; |
|
515 val it = fn |
|
516 : theory' |
|
517 -> rew_ord' |
|
518 -> rls' |
|
519 -> bool |
|
520 -> (cterm' * cterm') list |
|
521 -> thm' -> cterm' -> (cterm' * cterm' list) option |
|
522 ML> |
|
523 ML> rewrite_set_; |
|
524 val it = fn |
|
525 : theory -> rls -> bool -> rls -> term -> (term * term list) option |
|
526 ML> rewrite_set; |
|
527 val it = fn |
|
528 : theory' -> rls' -> bool -> rls' -> cterm' -> (cterm' * cterm' list) option |
|
529 ML> |
|
530 ML> rewrite_set_inst_; |
|
531 val it = fn |
|
532 : theory |
|
533 -> rls |
|
534 -> bool |
|
535 -> (cterm' * cterm') list |
|
536 -> rls -> term -> (term * term list) option |
|
537 ML> rewrite_set_inst; |
|
538 val it = fn |
|
539 : theory' |
|
540 -> rls' |
|
541 -> bool |
|
542 -> (cterm' * cterm') list |
|
543 -> rls' -> cterm' -> (cterm' * cterm' list) option |
|
544 \end{verbatim}}%size |
|
545 |
|
546 \noindent The variant {\tt rewrite\_inst} substitutes {\tt (term * term) list} in {\tt thm} before rewriting,\\ |
|
547 the variant {\tt rewrite\_set} rewrites with a whole rule set {\tt rls} (instead with a {\tt thm} only),\\ |
|
548 the variant {\tt rewrite\_set\_inst} is a combination of the latter two variants. In order to watch how a term is rewritten theorem by theorem, there is a switch {\tt trace\_rewrite}: |
|
549 {\footnotesize\begin{verbatim} |
|
550 ML> toggle; |
|
551 val it = fn : bool ref -> bool |
|
552 ML> |
|
553 ML> toggle trace_rewrite; |
|
554 val it = true : bool |
|
555 ML> toggle trace_rewrite; |
|
556 val it = false : bool |
|
557 \end{verbatim}}%size |
|
558 |
|
559 \section{Rule sets} |
|
560 Some of the variants of {\tt rewrite} above do not only apply one theorem, but a whole set of theorems, called a 'rule set'. Such a rule set is applied as long one of its elements can be used for a rewrite (which can go forever, i.e. the rule set eventually does not 'terminate'). |
|
561 |
|
562 A simple example of a rule set is {\tt rearrange\_assoc} which is defined in {\tt knowledge/RatArith.ML} as: |
|
563 {\footnotesize\begin{verbatim} |
|
564 val rearrange_assoc = |
|
565 Rls{preconds = [], rew_ord = ("tless_true",tless_true), |
|
566 rules = |
|
567 [Thm ("radd_assoc_RS_sym",num_str (radd_assoc RS sym)), |
|
568 Thm ("rmult_assoc_RS_sym",num_str (rmult_assoc RS sym))], |
|
569 scr = Script ((term_of o the o (parse thy)) |
|
570 "empty_script") |
|
571 }:rls; |
|
572 \end{verbatim}}%size |
|
573 where |
|
574 \begin{description} |
|
575 \item [\tt preconds] are conditions which must be true in order to make the rule set applicable (the empty list evaluates to {\tt true}) |
|
576 \item [\tt rew\_ord] concerns term orders introduced below in \ref{term-order} |
|
577 \item [\tt rules] are the theorems to be applied -- in priciple applied in arbitrary order, because all these rule sets should be 'complete' \cite{nipk:rew-all-that} (and actually the theorems are applied in the sequence they appear in this list). The function {\tt num\_str} must be applied to theorems containing numeral constants (and thus is obsolete in this example). {\tt RS} is an infix function applying the theorem {\tt sym} to {\tt radd\_assoc} before storage (the effect see below) |
|
578 \item [\tt scr] is the script applying the ruleset; it will disappear in later versions of \isac. |
|
579 \end{description} |
|
580 These variables evaluate to |
|
581 {\footnotesize\begin{verbatim} |
|
582 ML> sym; |
|
583 val it = "?s = ?t ==> ?t = ?s" : thm |
|
584 ML> rearrange_assoc; |
|
585 val it = |
|
586 Rls |
|
587 {preconds=[],rew_ord=("tless_true",fn), |
|
588 rules=[Thm ("radd_assoc_RS_sym","?m1 + (?n1 + ?k1) = ?m1 + ?n1 + ?k1"), |
|
589 Thm ("rmult_assoc_RS_sym","?m1 * (?n1 * ?k1) = ?m1 * ?n1 * ?k1")], |
|
590 scr=Script (Free ("empty_script","RealDef.real"))} : rls |
|
591 \end{verbatim}}%size |
|
592 |
|
593 \paragraph{Give it a try !} The above rule set makes an arbitrary number of parentheses disappear which are not necessary due to associativity of {\tt +} and |
|
594 {\footnotesize\begin{verbatim} |
|
595 ML> val ct = (string_of_cterm o the o (parse RatArith.thy)) |
|
596 "a + (b * (c * d) + e)"; |
|
597 val ct = "a + ((b * (c * d) + e) + f)" : cterm' |
|
598 ML> rewrite_set "RatArith.thy" "eval_rls" false "rearrange_assoc" ct; |
|
599 val it = Some ("a + b * c * d + e + f",[]) : (string * string list) option |
|
600 \end{verbatim}}%size |
|
601 For acchieving this result the rule set has to be surprisingly busy: |
|
602 {\footnotesize\begin{verbatim} |
|
603 ML> toggle trace_rewrite; |
|
604 val it = true : bool |
|
605 ML> rewrite_set "RatArith.thy" "eval_rls" false "rearrange_assoc" ct; |
|
606 ### trying thm 'radd_assoc_RS_sym' |
|
607 ### rewrite_set_: a + b * (c * d) + e |
|
608 ### trying thm 'radd_assoc_RS_sym' |
|
609 ### trying thm 'rmult_assoc_RS_sym' |
|
610 ### rewrite_set_: a + b * c * d + e |
|
611 ### trying thm 'rmult_assoc_RS_sym' |
|
612 ### trying thm 'radd_assoc_RS_sym' |
|
613 ### trying thm 'rmult_assoc_RS_sym' |
|
614 val it = Some ("a + b * c * d + e",[]) : (string * string list) option |
|
615 \end{verbatim}}%size |
|
616 |
|
617 |
|
618 \section{Calculate numeric constants} |
|
619 As soon as numeric constants are in adjacent subterms (see the example on p.\pageref{cond-rew}), they can be calculated by the function |
|
620 {\footnotesize\begin{verbatim} |
|
621 ML> calculate; |
|
622 val it = fn : theory' -> string -> cterm' -> (cterm' * thm') option |
|
623 ML> calculate_; |
|
624 val it = fn : theory -> string -> term -> (term * (string * thm)) option |
|
625 \end{verbatim}}%size |
|
626 where the {\tt string} in the arguments defines the algebraic operation to be calculated. The function returns the result of the calculation, and as second element in the pair the theorem applied. The following algebraic operations are available: |
|
627 {\footnotesize\begin{verbatim} |
|
628 ML> calc_list; |
|
629 val it = |
|
630 ref |
|
631 [("plus",("op +",fn)), |
|
632 ("times",("op *",fn)), |
|
633 ("cancel_",("cancel",fn)), |
|
634 ("power",("pow",fn)), |
|
635 ("sqrt",("sqrt",fn)), |
|
636 ("Var",("Var",fn)), |
|
637 ("Length",("Length",fn)), |
|
638 ("Nth",("Nth",fn)), |
|
639 ("power",("pow",fn)), |
|
640 ("le",("op <",fn)), |
|
641 ("leq",("op <=",fn)), |
|
642 ("is_const",("is'_const",fn)), |
|
643 ("is_root_free",("is'_root'_free",fn)), |
|
644 ("contains_root",("contains'_root",fn)), |
|
645 ("ident",("ident",fn))] |
|
646 : (string * (string * (string -> term -> theory -> |
|
647 (string * term) option))) list ref |
|
648 \end{verbatim}}%size |
|
649 These operations can be used in the following way. |
|
650 {\footnotesize\begin{verbatim} |
|
651 ML> calculate' "Isac.thy" "plus" "#1 + #2"; |
|
652 val it = Some ("#3",("#add_#1_#2","\"#1 + #2 = #3\"")) : (string * thm') option |
|
653 ML> |
|
654 ML> calculate' "Isac.thy" "times" "#2 * #3"; |
|
655 val it = Some ("#6",("#mult_#2_#3","\"#2 * #3 = #6\"")) |
|
656 : (string * thm') option |
|
657 ML> |
|
658 ML> calculate' "Isac.thy" "power" "#2 ^^^ #3"; |
|
659 val it = Some ("#8",("#power_#2_#3","\"#2 ^^^ #3 = #8\"")) |
|
660 : (string * thm') option |
|
661 ML> |
|
662 ML> calculate' "Isac.thy" "cancel_" "#9 // #12"; |
|
663 val it = Some ("#3 // #4",("#cancel_#9_#12","\"#9 // #12 = #3 // #4\"")) |
|
664 : (string * thm') option |
|
665 ML> |
|
666 ML> ... |
|
667 \end{verbatim}}%size |
|
668 |
|
669 |
|
670 |
|
671 \chapter{Term orders}\label{term-order} |
|
672 Orders on terms are indispensable for the purpose of rewriting to normal forms in associative - commutative domains \cite{nipk:rew-all-that}, and for rewriting to normal forms necessary for matching models to problems, see sect.\ref{pbt}. |
|
673 \section{Examples for term orders} |
|
674 It is not trivial to construct a relation $<$ on terms such that it is really an order, i.e. a transitive and antisymmetric relation. These orders are 'recursive path orders' \cite{nipk:rew-all-that}. Some orders implemented in the knowledgebase at {\tt [isac-src]/knowledge/\dots}, %FIXXXmat0201a |
|
675 e.g. |
|
676 {\footnotesize\begin{verbatim} |
|
677 ML> sqrt_right; |
|
678 val it = fn : bool -> theory -> term * term -> bool |
|
679 ML> tless_true; |
|
680 val it = fn : 'a -> bool |
|
681 \end{verbatim}}%size |
|
682 where the bool argument is a switch for tracing the checks on the respective subterms (and theory is necessary for displyinging the (sub-)terms as strings in the case of 'true'). The order {\tt tless\_true} is a dummy always yielding {\tt true}, and {\tt sqrt\_right} prefers a square root shifted to the right within a term: |
|
683 {\footnotesize\begin{verbatim} |
|
684 ML> val t1 = (term_of o the o (parse thy)) "(sqrt a) + b"; |
|
685 val t1 = Const # $ (# $ #) $ Free (#,#) : term |
|
686 ML> |
|
687 ML> val t2 = (term_of o the o (parse thy)) "b + (sqrt a)"; |
|
688 val t2 = Const # $ Free # $ (Const # $ Free #) : term |
|
689 ML> |
|
690 ML> sqrt_right false SqRoot.thy (t1, t2); |
|
691 val it = false : bool |
|
692 ML> sqrt_right false SqRoot.thy (t2, t1); |
|
693 val it = true : bool |
|
694 \end{verbatim}}%size |
|
695 The many checks performed recursively through all subterms can be traced throughout the algorithm in {\tt [isac-src]/knowledge/SqRoot.ML} by setting the flag to true: |
|
696 {\footnotesize\begin{verbatim} |
|
697 ML> val t1 = (term_of o the o (parse thy)) "a + b*(sqrt c) + d"; |
|
698 val t1 = Const (#,#) $ (# $ # $ (# $ #)) $ Free ("d","RealDef.real") : term |
|
699 ML> |
|
700 ML> val t2 = (term_of o the o (parse thy)) "a + (sqrt b)*c + d"; |
|
701 val t2 = Const (#,#) $ (# $ # $ (# $ #)) $ Free ("d","RealDef.real") : term |
|
702 ML> |
|
703 ML> sqrt_right true SqRoot.thy (t1, t2); |
|
704 t= f@ts= "op +" @ "[a + b * sqrt c,d]" |
|
705 u= g@us= "op +" @ "[a + sqrt b * c,d]" |
|
706 size_of_term(t,u)= (8, 8) |
|
707 hd_ord(f,g) = EQUAL |
|
708 terms_ord(ts,us) = LESS |
|
709 ------- |
|
710 t= f@ts= "op +" @ "[a,b * sqrt c]" |
|
711 u= g@us= "op +" @ "[a,sqrt b * c]" |
|
712 size_of_term(t,u)= (6, 6) |
|
713 hd_ord(f,g) = EQUAL |
|
714 terms_ord(ts,us) = LESS |
|
715 ------- |
|
716 t= f@ts= "a" @ "[]" |
|
717 u= g@us= "a" @ "[]" |
|
718 size_of_term(t,u)= (1, 1) |
|
719 hd_ord(f,g) = EQUAL |
|
720 terms_ord(ts,us) = EQUAL |
|
721 ------- |
|
722 t= f@ts= "op *" @ "[b,sqrt c]" |
|
723 u= g@us= "op *" @ "[sqrt b,c]" |
|
724 size_of_term(t,u)= (4, 4) |
|
725 hd_ord(f,g) = EQUAL |
|
726 terms_ord(ts,us) = LESS |
|
727 ------- |
|
728 t= f@ts= "b" @ "[]" |
|
729 u= g@us= "sqrt" @ "[b]" |
|
730 size_of_term(t,u)= (1, 2) |
|
731 hd_ord(f,g) = LESS |
|
732 terms_ord(ts,us) = LESS |
|
733 ------- |
|
734 val it = true : bool |
|
735 \end{verbatim}}%size |
|
736 |
|
737 |
|
738 |
|
739 \section{Ordered rewriting} |
|
740 Rewriting faces problems in just the most elementary domains, which are all associative and commutative w.r.t. {\tt +} and {\tt *} --- the law of commutativity applied within a rule set causes this set not to terminate~! One method to cope with this difficulty is ordered rewriting, where a rewrite is only done if the resulting term is smaller w.r.t. a term order (with some additional properties called 'rewrite orders' \cite{nipk:rew-all-that}). |
|
741 |
|
742 Such a rule set {\tt ac\_plus\_times}, called an AC-rewrite system, can be found in {\tt[isac-src]/knowledge/RathArith.ML}: |
|
743 {\footnotesize\begin{verbatim} |
|
744 val ac_plus_times = |
|
745 Rls{preconds = [], rew_ord = ("term_order",term_order), |
|
746 rules = |
|
747 [Thm ("radd_commute",radd_commute), |
|
748 Thm ("radd_left_commute",radd_left_commute), |
|
749 Thm ("radd_assoc",radd_assoc), |
|
750 Thm ("rmult_commute",rmult_commute), |
|
751 Thm ("rmult_left_commute",rmult_left_commute), |
|
752 Thm ("rmult_assoc",rmult_assoc)], |
|
753 scr = Script ((term_of o the o (parse thy)) |
|
754 "empty_script") |
|
755 }:rls; |
|
756 val ac_plus_times = |
|
757 Rls |
|
758 {preconds=[],rew_ord=("term_order",fn), |
|
759 rules=[Thm ("radd_commute","?m + ?n = ?n + ?m"), |
|
760 Thm ("radd_left_commute","?x + (?y + ?z) = ?y + (?x + ?z)"), |
|
761 Thm ("radd_assoc","?m + ?n + ?k = ?m + (?n + ?k)"), |
|
762 Thm ("rmult_commute","?m * ?n = ?n * ?m"), |
|
763 Thm ("rmult_left_commute","?x * (?y * ?z) = ?y * (?x * ?z)"), |
|
764 Thm ("rmult_assoc","?m * ?n * ?k = ?m * (?n * ?k)")], |
|
765 scr=Script (Free ("empty_script","RealDef.real"))} : rls |
|
766 \end{verbatim}}%size |
|
767 Note that the theorems {\tt radd\_left\_commute} and {\tt rmult\_left\_commute} are really necessary in order to make the rule set 'confluent'~! |
|
768 |
|
769 |
|
770 \paragraph{Give it a try !} Ordered rewriting is one technique to produce polynomial normal from from arbitrary integer terms: |
|
771 {\footnotesize\begin{verbatim} |
|
772 ML> val ct' = "#3 * a + b + #2 * a"; |
|
773 val ct' = "#3 * a + b + #2 * a" : cterm' |
|
774 ML> |
|
775 ML> (*-1-*) radd_commute; val thm' = ("radd_commute","") : thm'; |
|
776 val it = "?m + ?n = ?n + ?m" : thm |
|
777 val thm' = ("radd_commute","") : thm' |
|
778 ML> val Some (ct',_) = rewrite thy' "tless_true" "eval_rls" true thm' ct'; |
|
779 val ct' = "#2 * a + (#3 * a + b)" : cterm' |
|
780 ML> |
|
781 ML> (*-2-*) rdistr_right_assoc_p; val thm' = ("rdistr_right_assoc_p","") : thm'; |
|
782 val it = "?l * ?n + (?m * ?n + ?k) = (?l + ?m) * ?n + ?k" : thm |
|
783 val thm' = ("rdistr_right_assoc_p","") : thm' |
|
784 ML> val Some (ct',_) = rewrite thy' "tless_true" "eval_rls" true thm' ct'; |
|
785 val ct' = "(#2 + #3) * a + b" : cterm' |
|
786 ML> |
|
787 ML> (*-3-*) |
|
788 ML> val Some (ct',_) = calculate thy' "plus" ct'; |
|
789 val ct' = "#5 * a + b" : cterm' |
|
790 \end{verbatim}}%size %FIXXXmat0201b ... calculate ! |
|
791 This looks nice, but if {\tt radd\_commute} is applied automatically in {\tt (*-1-*)} without checking the resulting term to be 'smaller' w.r.t. a term order, then rewritin goes on forever (i.e. it does not 'terminate') \dots |
|
792 {\footnotesize\begin{verbatim} |
|
793 ML> val ct' = "#3 * a + b + #2 * a" : cterm'; |
|
794 val ct' = "#3 * a + b + #2 * a" : cterm' |
|
795 ML> val thm' = ("radd_commute","") : thm'; |
|
796 val thm' = ("radd_commute","") : thm' |
|
797 ML> |
|
798 ML> val Some (ct',_) = rewrite thy' "tless_true" "eval_rls" true thm' ct'; |
|
799 val ct' = "#2 * a + (#3 * a + b)" : cterm' |
|
800 ML> val Some (ct',_) = rewrite thy' "tless_true" "eval_rls" true thm' ct'; |
|
801 val ct' = "#3 * a + b + #2 * a" : cterm' |
|
802 ML> val Some (ct',_) = rewrite thy' "tless_true" "eval_rls" true thm' ct'; |
|
803 val ct' = "#2 * a + (#3 * a + b)" : cterm' |
|
804 .......... |
|
805 \end{verbatim}}%size |
|
806 |
|
807 Ordered rewriting with the above AC-rewrite system {\tt ac\_plus\_times} performs a kind of bubble sort which can be traced: |
|
808 {\footnotesize\begin{verbatim} |
|
809 ML> toggle trace_rewrite; |
|
810 val it = true : bool |
|
811 ML> |
|
812 ML> rewrite_set "RatArith.thy" "eval_rls" false "ac_plus_times" ct; |
|
813 ### trying thm 'radd_commute' |
|
814 ### not: "a + (b * (c * d) + e)" > "b * (c * d) + e + a" |
|
815 ### rewrite_set_: a + (e + b * (c * d)) |
|
816 ### trying thm 'radd_commute' |
|
817 ### not: "a + (e + b * (c * d))" > "e + b * (c * d) + a" |
|
818 ### not: "e + b * (c * d)" > "b * (c * d) + e" |
|
819 ### trying thm 'radd_left_commute' |
|
820 ### not: "a + (e + b * (c * d))" > "e + (a + b * (c * d))" |
|
821 ### trying thm 'radd_assoc' |
|
822 ### trying thm 'rmult_commute' |
|
823 ### not: "b * (c * d)" > "c * d * b" |
|
824 ### not: "c * d" > "d * c" |
|
825 ### trying thm 'rmult_left_commute' |
|
826 ### not: "b * (c * d)" > "c * (b * d)" |
|
827 ### trying thm 'rmult_assoc' |
|
828 ### trying thm 'radd_commute' |
|
829 ### not: "a + (e + b * (c * d))" > "e + b * (c * d) + a" |
|
830 ### not: "e + b * (c * d)" > "b * (c * d) + e" |
|
831 ### trying thm 'radd_left_commute' |
|
832 ### not: "a + (e + b * (c * d))" > "e + (a + b * (c * d))" |
|
833 ### trying thm 'radd_assoc' |
|
834 ### trying thm 'rmult_commute' |
|
835 ### not: "b * (c * d)" > "c * d * b" |
|
836 ### not: "c * d" > "d * c" |
|
837 ### trying thm 'rmult_left_commute' |
|
838 ### not: "b * (c * d)" > "c * (b * d)" |
|
839 ### trying thm 'rmult_assoc' |
|
840 val it = Some ("a + (e + b * (c * d))",[]) : (string * string list) option \end{verbatim}}%size |
|
841 Notice that {\tt +} is left-associative where the parentheses are omitted for {\tt (a + b) + c = a + b + c}, but not for {\tt a + (b + c)}. Ordered rewriting necessarily terminates with parentheses which could be omitted due to associativity. |
|
842 |
|
843 |
|
844 \chapter{The hierarchy of problem types}\label{pbt} |
|
845 \section{The standard-function for 'matching'} |
|
846 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: |
|
847 {\footnotesize\begin{verbatim} |
|
848 ML> matches; |
|
849 val it = fn : theory -> term -> term -> bool |
|
850 \end{verbatim}}%size |
|
851 where the first of the two {\tt term} arguments is the particular term to be tested, and the second one is the pattern: |
|
852 {\footnotesize\begin{verbatim} |
|
853 ML> val t = (term_of o the o (parse thy)) "#3 * x^^^#2 = #1"; |
|
854 val t = Const (#,#) $ (# $ # $ (# $ #)) $ Free ("#1","RealDef.real") : term |
|
855 ML> |
|
856 ML> val p = (term_of o the o (parse thy)) "a * b^^^#2 = c"; |
|
857 val p = Const (#,#) $ (# $ # $ (# $ #)) $ Free ("c","RealDef.real") : term |
|
858 ML> atomt p; |
|
859 *** ------------- |
|
860 *** Const ( op =) |
|
861 *** . Const ( op *) |
|
862 *** . . Free ( a, ) |
|
863 *** . . Const ( RatArith.pow) |
|
864 *** . . . Free ( b, ) |
|
865 *** . . . Free ( #2, ) |
|
866 *** . Free ( c, ) |
|
867 val it = () : unit |
|
868 ML> |
|
869 ML> free2var; |
|
870 val it = fn : term -> term |
|
871 ML> |
|
872 ML> val pat = free2var p; |
|
873 val pat = Const (#,#) $ (# $ # $ (# $ #)) $ Var ((#,#),"RealDef.real") : term |
|
874 ML> Sign.string_of_term (sign_of thy) pat; |
|
875 val it = "?a * ?b ^^^ #2 = ?c" : cterm' |
|
876 ML> atomt pat; |
|
877 *** ------------- |
|
878 *** Const ( op =) |
|
879 *** . Const ( op *) |
|
880 *** . . Var ((a, 0), ) |
|
881 *** . . Const ( RatArith.pow) |
|
882 *** . . . Var ((b, 0), ) |
|
883 *** . . . Free ( #2, ) |
|
884 *** . Var ((c, 0), ) |
|
885 val it = () : unit |
|
886 \end{verbatim}}%size % $ |
|
887 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: |
|
888 {\footnotesize\begin{verbatim} |
|
889 ML> matches thy t pat; |
|
890 val it = true : bool |
|
891 ML> |
|
892 ML> val t2 = (term_of o the o (parse thy)) "x^^^#2 = #1"; |
|
893 val t2 = Const (#,#) $ (# $ # $ Free #) $ Free ("#1","RealDef.real") : term |
|
894 ML> matches thy t2 pat; |
|
895 val it = false : bool |
|
896 ML> |
|
897 ML> val pat2 = (term_of o the o (parse thy)) "?u^^^#2 = ?v"; |
|
898 val pat2 = Const (#,#) $ (# $ # $ Free #) $ Var ((#,#),"RealDef.real") : term |
|
899 ML> matches thy t2 pat2; |
|
900 val it = true : bool |
|
901 \end{verbatim}}%size % $ |
|
902 |
|
903 \section{Accessing the hierarchy} |
|
904 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): |
|
905 {\footnotesize\begin{verbatim} |
|
906 ML> show_ptyps; |
|
907 val it = fn : unit -> unit |
|
908 ML> show_ptyps(); |
|
909 [ |
|
910 ["e_pblID"], |
|
911 ["equation", "univariate", "linear"], |
|
912 ["equation", "univariate", "plain_square"], |
|
913 ["equation", "univariate", "polynomial", "degree_two", "pq_formula"], |
|
914 ["equation", "univariate", "polynomial", "degree_two", "abc_formula"], |
|
915 ["equation", "univariate", "squareroot"], |
|
916 ["equation", "univariate", "normalize"], |
|
917 ["equation", "univariate", "sqroot-test"], |
|
918 ["function", "derivative_of"], |
|
919 ["function", "maximum_of", "on_interval"], |
|
920 ["function", "make"], |
|
921 ["tool", "find_values"], |
|
922 ["functional", "inssort"] |
|
923 ] |
|
924 val it = () : unit |
|
925 \end{verbatim}}%size |
|
926 The retrieve function for individual problem types is {\tt get\_pbt} |
|
927 \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: |
|
928 {\footnotesize\begin{verbatim} |
|
929 ML> get_pbt; |
|
930 val it = fn : pblID -> pbt |
|
931 ML> get_pbt ["squareroot", "univariate", "equation"]; |
|
932 val it = |
|
933 {met=[("SqRoot.thy","square_equation")], |
|
934 ppc=[("#Given",(Const (#,#),Free (#,#))), |
|
935 ("#Given",(Const (#,#),Free (#,#))), |
|
936 ("#Given",(Const (#,#),Free (#,#))), |
|
937 ("#Find",(Const (#,#),Free (#,#)))], |
|
938 thy={ProtoPure, CPure, HOL, Ord, Set, subset, equalities, mono, Vimage, Fun, |
|
939 Prod, Lfp, Relation, Trancl, WF, NatDef, Gfp, Sum, Inductive, Nat, |
|
940 Arith, Divides, Power, Finite, Equiv, IntDef, Int, Univ, Datatype, |
|
941 Numeral, Bin, IntArith, WF_Rel, Recdef, IntDiv, NatBin, List, Option, |
|
942 Map, Record, RelPow, Sexp, String, Calculation, SVC_Oracle, Main, |
|
943 Zorn, Filter, PNat, PRat, PReal, RealDef, RealOrd, RealInt, RealBin, |
|
944 HyperDef, Descript, ListG, Tools, Script, Typefix, Atools, RatArith, |
|
945 SqRoot}, |
|
946 where_=[Const ("SqRoot.contains'_root","bool => bool") $ |
|
947 Free ("e_","bool")]} : pbt |
|
948 \end{verbatim}}%size %$ |
|
949 where the records fields hold the following data: |
|
950 \begin{description} |
|
951 \item [\tt thy]: the theory necessary for parsing the formulas |
|
952 \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}. |
|
953 \item [\tt met]: the list of methods solving this problem type.\\ |
|
954 \end{description} |
|
955 |
|
956 The following function adds or replaces a problem type (after having it prepared using {\tt prep\_pbt}) |
|
957 {\footnotesize\begin{verbatim} |
|
958 ML> store_pbt; |
|
959 val it = fn : pbt * pblID -> unit |
|
960 ML> store_pbt |
|
961 (prep_pbt SqRoot.thy |
|
962 (["newtype","univariate","equation"], |
|
963 [("#Given" ,["equality e_","solveFor v_","errorBound err_"]), |
|
964 ("#Where" ,["contains_root (e_::bool)"]), |
|
965 ("#Find" ,["solutions v_i_"]) |
|
966 ], |
|
967 [("SqRoot.thy","square_equation")])); |
|
968 val it = () : unit |
|
969 \end{verbatim}}%size |
|
970 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}). |
|
971 |
|
972 \section{Internals of the datastructure} |
|
973 This subsection only serves for the implementation of the hierarchy browser and can be skipped by the authors of math knowledge. |
|
974 |
|
975 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: |
|
976 {\footnotesize\begin{verbatim} |
|
977 type pbt = |
|
978 {thy : theory, (* the nearest to the root, |
|
979 which allows to compile that pbt *) |
|
980 where_: term list, (* where - predicates *) |
|
981 ppc : ((string * (* fields "#Given","#Find" *) |
|
982 (term * (* description *) |
|
983 term)) (* id *) |
|
984 list), |
|
985 met : metID list}; (* methods solving the pbt *) |
|
986 datatype ptyp = |
|
987 Ptyp of string * (* key within pblID *) |
|
988 pbt list * (* several pbts with different domIDs*) |
|
989 ptyp list; |
|
990 val e_Ptyp = Ptyp ("empty",[],[]); |
|
991 |
|
992 type ptyps = ptyp list; |
|
993 val ptyps = ref ([e_Ptyp]:ptyps); |
|
994 \end{verbatim}}%size |
|
995 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. |
|
996 |
|
997 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}. |
|
998 |
|
999 |
|
1000 |
|
1001 \section{Match a formalization with a problem type}\label{pbl} |
|
1002 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. |
|
1003 {\footnotesize\begin{verbatim} |
|
1004 ML> val fmz = ["equality (#1 + #2 * x = #0)", |
|
1005 "solveFor x", |
|
1006 "solutions L"] : fmz; |
|
1007 val fmz = ["equality (#1 + #2 * x = #0)","solveFor x","solutions L"] : fmz |
|
1008 \end{verbatim}}%size |
|
1009 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: |
|
1010 {\footnotesize\begin{verbatim} |
|
1011 ML> match_pbl; |
|
1012 val it = fn : fmz -> pbt -> match' |
|
1013 ML> |
|
1014 ML> match_pbl fmz (get_pbt ["univariate","equation"]); |
|
1015 val it = |
|
1016 Matches' |
|
1017 {Find=[Correct "solutions L"], |
|
1018 Given=[Correct "equality (#1 + #2 * x = #0)",Correct "solveFor x"], |
|
1019 Relate=[],Where=[Correct "matches (?a = ?b) (#1 + #2 * x = #0)"],With=[]} |
|
1020 : match' |
|
1021 ML> |
|
1022 ML> match_pbl fmz (get_pbt ["linear","univariate","equation"]); |
|
1023 val it = |
|
1024 Matches' |
|
1025 {Find=[Correct "solutions L"], |
|
1026 Given=[Correct "equality (#1 + #2 * x = #0)",Correct "solveFor x"], |
|
1027 Relate=[], |
|
1028 Where=[Correct |
|
1029 "matches ( x = #0) (#1 + #2 * x = #0) | |
|
1030 matches ( ?b * x = #0) (#1 + #2 * x = #0) | |
|
1031 matches (?a + x = #0) (#1 + #2 * x = #0) | |
|
1032 matches (?a + ?b * x = #0) (#1 + #2 * x = #0)"], |
|
1033 With=[]} : match' |
|
1034 ML> |
|
1035 ML> match_pbl fmz (get_pbt ["squareroot","univariate","equation"]); |
|
1036 val it = |
|
1037 NoMatch' |
|
1038 {Find=[Correct "solutions L"], |
|
1039 Given=[Correct "equality (#1 + #2 * x = #0)",Correct "solveFor x", |
|
1040 Missing "errorBound err_"],Relate=[], |
|
1041 Where=[False "contains_root #1 + #2 * x = #0 "],With=[]} : match' |
|
1042 \end{verbatim}}%size |
|
1043 The above formalization does not match the problem type \\{\tt["squareroot","univariate","equation"]} which is explained by the tags: |
|
1044 \begin{tabbing} |
|
1045 123\=\kill |
|
1046 \> {\tt Missing:} the item is missing in the formalization as required by the problem type\\ |
|
1047 \> {\tt Superfl:} the item is not required by the problem type\\ |
|
1048 \> {\tt Correct:} the item is correct, or the precondition ({\tt Where}) is true\\ |
|
1049 \> {\tt False:} the precondition ({\tt Where}) is false\\ |
|
1050 \> {\tt Incompl:} the item is incomlete, or not yet input.\\ |
|
1051 \end{tabbing} |
|
1052 |
|
1053 |
|
1054 |
|
1055 \section{Refine a problem specification} |
|
1056 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). |
|
1057 |
|
1058 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 |
|
1059 {\small |
|
1060 \begin{enumerate} |
|
1061 \item for all $F$ matching some $P_i$ must follow, that $F$ matches $P$ |
|
1062 \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) |
|
1063 \item for all $F$ matching some $P$ must follow, that $F$ matches $P_n$\\ |
|
1064 \end{enumerate}}%small |
|
1065 \noindent Let us give an example for the point (1.) and (2.) first: |
|
1066 {\footnotesize\begin{verbatim} |
|
1067 ML> refine; |
|
1068 val it = fn : fmz -> pblID -> match list |
|
1069 ML> |
|
1070 ML> val fmz = ["equality (sqrt(#9+#4*x)=sqrt x + sqrt(#5+x))", |
|
1071 "solveFor x","errorBound (eps=#0)", |
|
1072 "solutions L"]; |
|
1073 ML> |
|
1074 ML> refine fmz ["univariate","equation"]; |
|
1075 *** pass ["equation","univariate"] |
|
1076 *** pass ["equation","univariate","linear"] |
|
1077 *** pass ["equation","univariate","plain_square"] |
|
1078 *** pass ["equation","univariate","polynomial"] |
|
1079 *** pass ["equation","univariate","squareroot"] |
|
1080 val it = |
|
1081 [Matches |
|
1082 (["univariate","equation"], |
|
1083 {Find=[Correct "solutions L"], |
|
1084 Given=[Correct "equality (sqrt (#9 + #4 * x) = sqrt x + sqrt (#5 + x))", |
|
1085 Correct "solveFor x",Superfl "errorBound (eps = #0)"],Relate=[], |
|
1086 Where=[Correct |
|
1087 "matches (?a = ?b) (sqrt (#9 + #4 * x) = sqrt x + sqrt (#5 + x))"], |
|
1088 With=[]}), |
|
1089 NoMatch |
|
1090 (["linear","univariate","equation"], |
|
1091 {Find=[Correct "solutions L"], |
|
1092 Given=[Correct "equality (sqrt (#9 + #4 * x) = sqrt x + sqrt (#5 + x))", |
|
1093 Correct "solveFor x",Superfl "errorBound (eps = #0)"],Relate=[], |
|
1094 Where=[False "(?a + ?b * x = #0) (sqrt (#9 + #4 * x#"], |
|
1095 With=[]}), |
|
1096 NoMatch |
|
1097 (["plain_square","univariate","equation"], |
|
1098 {Find=[Correct "solutions L"], |
|
1099 Given=[Correct "equality (sqrt (#9 + #4 * x) = sqrt x + sqrt (#5 + x))", |
|
1100 Correct "solveFor x",Superfl "errorBound (eps = #0)"],Relate=[], |
|
1101 Where=[False |
|
1102 "matches (?a + ?b * x ^^^ #2 = #0)"], |
|
1103 With=[]}), |
|
1104 NoMatch |
|
1105 (["polynomial","univariate","equation"], |
|
1106 {Find=[Correct "solutions L"], |
|
1107 Given=[Correct "equality (sqrt (#9 + #4 * x) = sqrt x + sqrt (#5 + x))", |
|
1108 Correct "solveFor x",Superfl "errorBound (eps = #0)"],Relate=[], |
|
1109 Where=[False |
|
1110 "is_polynomial_in sqrt (#9 + #4 * x) = sqrt x + sqrt (#5 + x) x"], |
|
1111 With=[]}), |
|
1112 Matches |
|
1113 (["squareroot","univariate","equation"], |
|
1114 {Find=[Correct "solutions L"], |
|
1115 Given=[Correct "equality (sqrt (#9 + #4 * x) = sqrt x + sqrt (#5 + x))", |
|
1116 Correct "solveFor x",Correct "errorBound (eps = #0)"],Relate=[], |
|
1117 Where=[Correct |
|
1118 "contains_root sqrt (#9 + #4 * x) = sqrt x + sqrt (#5 + x) "], |
|
1119 With=[]})] : match list |
|
1120 \end{verbatim}}%size}%footnotesize\label{refine} |
|
1121 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.)). |
|
1122 |
|
1123 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: |
|
1124 {\footnotesize\begin{verbatim} |
|
1125 ML> val fmz = ["equality (x+#1=#2)", |
|
1126 "solveFor x","errorBound (eps=#0)", |
|
1127 "solutions L"]; |
|
1128 [...] |
|
1129 ML> |
|
1130 ML> refine fmz ["univariate","equation"]; |
|
1131 *** pass ["equation","univariate"] |
|
1132 *** pass ["equation","univariate","linear"] |
|
1133 *** pass ["equation","univariate","plain_square"] |
|
1134 *** pass ["equation","univariate","polynomial"] |
|
1135 *** pass ["equation","univariate","squareroot"] |
|
1136 *** pass ["equation","univariate","normalize"] |
|
1137 val it = |
|
1138 [Matches |
|
1139 (["univariate","equation"], |
|
1140 {Find=[Correct "solutions L"], |
|
1141 Given=[Correct "equality (x + #1 = #2)",Correct "solveFor x", |
|
1142 Superfl "errorBound (eps = #0)"],Relate=[], |
|
1143 Where=[Correct "matches (?a = ?b) (x + #1 = #2)"],With=[]}), |
|
1144 NoMatch |
|
1145 (["linear","univariate","equation"], |
|
1146 [...] |
|
1147 With=[]}), |
|
1148 NoMatch |
|
1149 (["squareroot","univariate","equation"], |
|
1150 {Find=[Correct "solutions L"], |
|
1151 Given=[Correct "equality (x + #1 = #2)",Correct "solveFor x", |
|
1152 Correct "errorBound (eps = #0)"],Relate=[], |
|
1153 Where=[False "contains_root x + #1 = #2 "],With=[]}), |
|
1154 Matches |
|
1155 (["normalize","univariate","equation"], |
|
1156 {Find=[Correct "solutions L"], |
|
1157 Given=[Correct "equality (x + #1 = #2)",Correct "solveFor x", |
|
1158 Superfl "errorBound (eps = #0)"],Relate=[],Where=[],With=[]})] |
|
1159 : match list |
|
1160 \end{verbatim}}%size |
|
1161 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"]}. |
|
1162 |
|
1163 This recursive search on the problem hierarchy can be done within a proof state. This leads to the next section. |
|
1164 |
|
1165 |
|
1166 \chapter{Methods} |
|
1167 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. |
|
1168 |
|
1169 \section{The scripts' syntax} |
|
1170 The syntax of scripts follows the definition given in Backus-normal-form: |
|
1171 {\it |
|
1172 \begin{tabbing} |
|
1173 123\=123\=expr ::=\=$|\;\;$\=\kill |
|
1174 \>script ::= {\tt Script} id arg$\,^*$ = body\\ |
|
1175 \>\>arg ::= id $\;|\;\;($ ( id :: type ) $)$\\ |
|
1176 \>\>body ::= expr\\ |
|
1177 \>\>expr ::= \>\>{\tt let} id = expr $($ ; id = expr$)^*$ {\tt in} expr\\ |
|
1178 \>\>\>$|\;$\>{\tt if} prop {\tt then} expr {\tt else} expr\\ |
|
1179 \>\>\>$|\;$\>listexpr\\ |
|
1180 \>\>\>$|\;$\>id\\ |
|
1181 \>\>\>$|\;$\>seqex id\\ |
|
1182 \>\>seqex ::= \>\>{\tt While} prop {\tt Do} seqex\\ |
|
1183 \>\>\>$|\;$\>{\tt Repeat} seqex\\ |
|
1184 \>\>\>$|\;$\>{\tt Try} seqex\\ |
|
1185 \>\>\>$|\;$\>seqex {\tt Or} seqex\\ |
|
1186 \>\>\>$|\;$\>seqex {\tt @@} seqex\\ |
|
1187 \>\>\>$|\;$\>tac $($ id $|$ listexpr $)^*$\\ |
|
1188 \>\>type ::= id\\ |
|
1189 \>\>tac ::= id |
|
1190 \end{tabbing}} |
|
1191 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. |
|
1192 |
|
1193 Expressions containing some of the keywords {\tt let}, {\tt if} etc. are called {\bf script-expressions}. |
|
1194 |
|
1195 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, |
|
1196 |
|
1197 |
|
1198 \section{Control the flow of evaluation} |
|
1199 The flow of control is managed by the following script-expressions called {\it tacticals}. |
|
1200 \begin{description} |
|
1201 \item{{\tt while} prop {\tt Do} expr id} |
|
1202 \item{{\tt if} prop {\tt then} expr {\tt else} expr} |
|
1203 \end{description} |
|
1204 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) |
|
1205 \begin{description} |
|
1206 \item{{\tt Repeat} expr id} |
|
1207 \item{{\tt Try} expr id} |
|
1208 \item{expr {\tt Or} expr id} |
|
1209 \item{expr {\tt @@} expr id} |
|
1210 \end{description} |
|
1211 |
|
1212 \begin{description} |
|
1213 \item xxx |
|
1214 |
|
1215 \end{description} |
|
1216 |
|
1217 \chapter{Do a calculational proof} |
|
1218 First we list all the tactics available so far (this list may be extended during further development of \isac). |
|
1219 |
|
1220 \section{Tactics for doing steps in calculations} |
|
1221 \input{tactics} |
|
1222 |
|
1223 \section{The functionality of the math engine} |
|
1224 A proof is being started in the math engine {\tt me} by the tactic |
|
1225 \footnote{In the present version a tactic is of type {\tt mstep}.} |
|
1226 {\tt Init\_Proof}, and interactively promoted by other tactics. On input of each tactic the {\tt me} returns the resulting formula and the next tactic applicable. The proof is finished, when the {\tt me} proposes {\tt End\_Proof} as the next tactic. |
|
1227 |
|
1228 We show a calculation (calculational proof) concerning equation solving, where the type of equation is refined automatically: The equation is given by the respective formalization ... |
|
1229 {\footnotesize\begin{verbatim} |
|
1230 ML> val fmz = ["equality ((x+#1)*(x+#2)=x^^^#2+#8)","solveFor x", |
|
1231 "errorBound (eps=#0)","solutions L"]; |
|
1232 val fmz = |
|
1233 ["equality ((x+#1)*(x+#2)=x^^^#2+#8)","solveFor x","errorBound (eps=#0)", |
|
1234 "solutions L"] : string list |
|
1235 ML> |
|
1236 ML> val spec as (dom, pbt, met) = ("SqRoot.thy",["univariate","equation"], |
|
1237 ("SqRoot.thy","no_met")); |
|
1238 val dom = "SqRoot.thy" : string |
|
1239 val pbt = ["univariate","equation"] : string list |
|
1240 val met = ("SqRoot.thy","no_met") : string * string |
|
1241 \end{verbatim}}%size |
|
1242 ... and the specification {\tt spec} of a domain {\tt dom}, a problem type {\tt pbt} and a method {\tt met}. Note that the equation is such, that it is not immediatly clear, what type it is in particular (it could be a polynomial of degree 2; but, for sure, the type is some specialized type of a univariate equation). Thus, no method ({\tt no\_met}) can be specified for solving the problem. |
|
1243 |
|
1244 Nevertheless this specification is sufficient for automatically solving the equation --- the appropriate method will be found by refinement within the hierarchy of problem types. |
|
1245 |
|
1246 |
|
1247 \section{Initialize the calculation} |
|
1248 The start of a new proof requires the following initializations: The proof state is given by a proof tree {\tt ptree} and a position {\tt pos'}; both are empty at the beginning. The tactic {\tt Init\_Proof} is, like all other tactics, paired with an identifier of type {\tt string} for technical reasons. |
|
1249 {\footnotesize\begin{verbatim} |
|
1250 ML> val (mID,m) = ("Init_Proof",Init_Proof (fmz, (dom,pbt,met))); |
|
1251 val mID = "Init_Proof" : string |
|
1252 val m = |
|
1253 Init_Proof |
|
1254 (["equality ((x+#1)*(x+#2)=x^^^#2+#8)","solveFor x","errorBound (eps=#0)", |
|
1255 "solutions L"],("SqRoot.thy",[#,#],(#,#))) : mstep |
|
1256 ML> |
|
1257 ML> val (p,_,f,nxt,_,pt) = me (mID,m) e_pos' c EmptyPtree; |
|
1258 val p = ([],Pbl) : pos' |
|
1259 val f = Form' (PpcKF (0,EdUndef,0,Nundef,(#,#))) : mout |
|
1260 val nxt = ("Refine_Tacitly",Refine_Tacitly ["univariate","equation"]) |
|
1261 : string * mstep |
|
1262 val pt = |
|
1263 Nd |
|
1264 (PblObj |
|
1265 {branch=#,cell=#,env=#,loc=#,meth=#,model=#,origin=#,ostate=#,probl=#, |
|
1266 result=#,spec=#},[]) : ptree |
|
1267 \end{verbatim}}%size |
|
1268 The mathematics engine {\tt me} returns the resulting formula {\tt f} of type {\tt mout} (which in this case is a problem), the next tactic {\tt nxt}, and a new proof state ({\tt ptree}, {\tt pos'}). |
|
1269 |
|
1270 We can convince ourselves, that the problem is still empty, by increasing {\tt Compiler.Control.Print.printDepth}: |
|
1271 {\footnotesize\begin{verbatim} |
|
1272 ML> Compiler.Control.Print.printDepth:=8; (*4 default*) |
|
1273 val it = () : unit |
|
1274 ML> |
|
1275 ML> f; |
|
1276 val it = |
|
1277 Form' |
|
1278 (PpcKF |
|
1279 (0,EdUndef,0,Nundef, |
|
1280 (Problem [], |
|
1281 {Find=[Incompl "solutions []"], |
|
1282 Given=[Incompl "equality",Incompl "solveFor"],Relate=[], |
|
1283 Where=[False "matches (?a = ?b) e_"],With=[]}))) : mout |
|
1284 \end{verbatim}}%size |
|
1285 Recall, please, the format of a problem as presented in sect.\ref{pbl} on p.\pageref{pbl}; such an 'empty' problem can be found above encapsulated by several constructors containing additional data (necessary for the dialog guide, not relevant here).\\ |
|
1286 |
|
1287 {\it In the sequel we will omit output of the {\tt me} if it is not important for the respective context}.\\ |
|
1288 |
|
1289 In general, the dialog guide will hide the following two tactics {\tt Refine\_Tacitly} and {\tt Model\_Problem} from the user. |
|
1290 {\footnotesize\begin{verbatim} |
|
1291 ML> nxt; |
|
1292 val it = ("Refine_Tacitly",Refine_Tacitly ["univariate","equation"]) |
|
1293 : string * mstep |
|
1294 ML> |
|
1295 ML> val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
|
1296 val nxt = ("Model_Problem",Model_Problem ["normalize","univariate","equation"]) |
|
1297 : string * mstep |
|
1298 ML> |
|
1299 ML> val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
|
1300 \end{verbatim}}%size |
|
1301 |
|
1302 |
|
1303 \section{The phase of modeling} |
|
1304 comprises the input of the items of the problem; the {\tt me} can help by use of the formalization tacitly transferred by {\tt Init\_Proof}. In particular, the {\tt me} in general 'knows' the next promising tactic; the first one has been returned by the (hidden) tactic {\tt Model\_Problem}. |
|
1305 |
|
1306 {\footnotesize\begin{verbatim} |
|
1307 ML> nxt; |
|
1308 val it = |
|
1309 ("Add_Given",Add_Given "equality ((x + #1) * (x + #2) = x ^^^ #2 + #8)") |
|
1310 : string * mstep |
|
1311 ML> |
|
1312 ML> val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
|
1313 val nxt = ("Add_Given",Add_Given "solveFor x") : string * mstep |
|
1314 ML> |
|
1315 ML> val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
|
1316 val nxt = ("Add_Find",Add_Find "solutions L") : string * mstep |
|
1317 ML> |
|
1318 ML> val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
|
1319 val f = Form' (PpcKF (0,EdUndef,0,Nundef,(#,#))) : mout |
|
1320 \end{verbatim}}%size |
|
1321 \noindent Now the problem is 'modeled', all items are input. We convince ourselves by increasing {\tt Compiler.Control.Print.printDepth} once more. |
|
1322 {\footnotesize\begin{verbatim} |
|
1323 ML> Compiler.Control.Print.printDepth:=8; |
|
1324 ML> f; |
|
1325 val it = |
|
1326 Form' |
|
1327 (PpcKF |
|
1328 (0,EdUndef,0,Nundef, |
|
1329 (Problem [], |
|
1330 {Find=[Correct "solutions L"], |
|
1331 Given=[Correct "equality ((x + #1) * (x + #2) = x ^^^ #2 + #8)", |
|
1332 Correct "solveFor x"],Relate=[],Where=[],With=[]}))) : mout |
|
1333 \end{verbatim}}%size |
|
1334 %One of the input items is considered {\tt Superfluous} by the {\tt me} consulting the problem type {\tt ["univariate","equation"]}. The {\tt ErrorBound}, however, could become important in case the equation only could be solved by some iteration method. |
|
1335 |
|
1336 \section{The phase of specification} |
|
1337 This phase provides for explicit determination of the domain, the problem type, and the method to be used. In particular, the search for the appropriate problem type is being supported. There are two tactics for this purpose: {\tt Specify\_Problem} generates feedback on how a candidate of a problem type matches the current problem, and {\tt Refine\_Problem} provides help by the system, if the user gets lost. |
|
1338 {\footnotesize\begin{verbatim} |
|
1339 ML> nxt; |
|
1340 val it = ("Specify_Domain",Specify_Domain "SqRoot.thy") : string * mstep |
|
1341 ML> |
|
1342 ML> val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
|
1343 val nxt = |
|
1344 ("Specify_Problem",Specify_Problem ["normalize","univariate","equation"]) |
|
1345 : string * mstep |
|
1346 val pt = |
|
1347 Nd |
|
1348 (PblObj |
|
1349 {branch=#,cell=#,env=#,loc=#,meth=#,model=#,origin=#,ostate=#,probl=#, |
|
1350 result=#,spec=#},[]) : ptree |
|
1351 \end{verbatim}}%size |
|
1352 The {\tt me} is smart enough to know the appropriate problem type (transferred tacitly with {\tt Init\_Proof}). In order to challenge the student, the dialog guide may hide this information; then the {\tt me} works as follows. |
|
1353 {\footnotesize\begin{verbatim} |
|
1354 ML> val nxt = ("Specify_Problem", |
|
1355 Specify_Problem ["polynomial","univariate","equation"]); |
|
1356 ML> val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
|
1357 val f = Form' (PpcKF (0,EdUndef,0,Nundef,(#,#))) : mout |
|
1358 val nxt = |
|
1359 ("Refine_Problem",Refine_Problem ["normalize","univariate","equation"]) |
|
1360 : string * mstep |
|
1361 ML> |
|
1362 ML> val nxt = ("Specify_Problem", |
|
1363 Specify_Problem ["linear","univariate","equation"]); |
|
1364 ML> val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
|
1365 val f = |
|
1366 Form' |
|
1367 (PpcKF |
|
1368 (0,EdUndef,0,Nundef, |
|
1369 (Problem ["linear","univariate","equation"], |
|
1370 {Find=[Correct "solutions L"], |
|
1371 Given=[Correct "equality ((x + #1) * (x + #2) = x ^^^ #2 + #8)", |
|
1372 Correct "solveFor x"],Relate=[], |
|
1373 Where=[False |
|
1374 "matches (?a + ?b * x = #0) ((x + #1) * (x + #2) = x ^^^ #2 + #8)"], |
|
1375 With=[]}))) : mout |
|
1376 \end{verbatim}}%size |
|
1377 Again assuming that the dialog guide hide the next tactic proposed by the {\tt me}, and the student gets lost, {\tt Refine\_Problem} always 'knows' the way out, if applied to the problem type {\tt["univariate","equation"]}. |
|
1378 {\footnotesize\begin{verbatim} |
|
1379 ML> val nxt = ("Refine_Problem", |
|
1380 Refine_Problem ["linear","univariate","equation |
|
1381 ML> val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
|
1382 val f = Problems (RefinedKF [NoMatch #]) : mout |
|
1383 ML> |
|
1384 ML> Compiler.Control.Print.printDepth:=9;f;Compiler.Control.Print.printDepth:=4; |
|
1385 val f = |
|
1386 Problems |
|
1387 (RefinedKF |
|
1388 [NoMatch |
|
1389 (["linear","univariate","equation"], |
|
1390 {Find=[Correct "solutions L"], |
|
1391 Given=[Correct "equality ((x + #1) * (x + #2) = x ^^^ #2 + #8)", |
|
1392 Correct "solveFor x"],Relate=[], |
|
1393 Where=[False |
|
1394 "matches (?a + ?b * x = #0) ((x + #1) * (x + #2) = x ^^^ #2 + #8)"], |
|
1395 With=[]})]) : mout |
|
1396 ML> |
|
1397 ML> val nxt = ("Refine_Problem",Refine_Problem ["univariate","equation"]); |
|
1398 ML> val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
|
1399 val f = |
|
1400 Problems |
|
1401 (RefinedKF [Matches #,NoMatch #,NoMatch #,NoMatch #,NoMatch #,Matches #]) |
|
1402 : mout |
|
1403 ML> |
|
1404 ML> |
|
1405 ML> Compiler.Control.Print.printDepth:=9;f;Compiler.Control.Print.printDepth:=4; |
|
1406 val f = |
|
1407 Problems |
|
1408 (RefinedKF |
|
1409 [Matches |
|
1410 (["univariate","equation"], |
|
1411 {Find=[Correct "solutions L"], |
|
1412 Given=[Correct "equality ((x + #1) * (x + #2) = x ^^^ #2 + #8)", |
|
1413 Correct "solveFor x"],Relate=[], |
|
1414 Where=[Correct |
|
1415 With=[]}), |
|
1416 NoMatch |
|
1417 (["linear","univariate","equation"], |
|
1418 {Find=[Correct "solutions L"], |
|
1419 Given=[Correct "equality ((x + #1) * (x + #2) = x ^^^ #2 + #8)", |
|
1420 Correct "solveFor x"],Relate=[], |
|
1421 Where=[False |
|
1422 "matches (?a + ?b * x = #0) ((x + #1) * (x + #2) = x ^^^ #2 + #8)"], |
|
1423 With=[]}), |
|
1424 NoMatch |
|
1425 ... |
|
1426 ... |
|
1427 Matches |
|
1428 (["normalize","univariate","equation"], |
|
1429 {Find=[Correct "solutions L"], |
|
1430 Given=[Correct "equality ((x + #1) * (x + #2) = x ^^^ #2 + #8)", |
|
1431 Correct "solveFor x"],Relate=[],Where=[],With=[]})]) : mout |
|
1432 \end{verbatim}}%size |
|
1433 The tactic {\tt Refine\_Problem} returns all matches to problem types along the path traced in the problem hierarchy (anlogously to the authoring tool for refinement in sect.\ref{refine} on p.\pageref{refine}) --- a lot of information to be displayed appropriately in the hiearchy browser~! |
|
1434 |
|
1435 \section{The phase of solving} |
|
1436 This phase starts by invoking a method, which acchieves the normal form within two tactics, {\tt Rewrite rnorm\_equation\_add} and {\tt Rewrite\_Set SqRoot\_simplify}: |
|
1437 {\footnotesize\begin{verbatim} |
|
1438 ML> nxt; |
|
1439 val it = ("Apply_Method",Apply_Method ("SqRoot.thy","norm_univar_equation")) |
|
1440 : string * mstep |
|
1441 ML> |
|
1442 ML> val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
|
1443 val f = |
|
1444 Form' (FormKF (~1,EdUndef,1,Nundef,"(x + #1) * (x + #2) = x ^^^ #2 + #8")) |
|
1445 val nxt = |
|
1446 ("Rewrite", Rewrite |
|
1447 ("rnorm_equation_add","~ ?b =!= #0 ==> (?a = ?b) = (?a + #-1 * ?b = #0)")) |
|
1448 ML> |
|
1449 ML> val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
|
1450 val f = |
|
1451 Form' (FormKF (~1,EdUndef,1,Nundef, |
|
1452 "(x + #1) * (x + #2) + #-1 * (x ^^^ #2 + #8) = #0")) : mout |
|
1453 val nxt = ("Rewrite_Set",Rewrite_Set "SqRoot_simplify") : string * mstep |
|
1454 ML> |
|
1455 ML> val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
|
1456 val f = Form' (FormKF (~1,EdUndef,1,Nundef,"#-6 + #3 * x = #0")) : mout |
|
1457 val nxt = ("Subproblem",Subproblem ("SqRoot.thy",[#,#])) : string * mstep |
|
1458 \end{verbatim}}%size |
|
1459 Now the normal form {\tt \#-6 + \#3 * x = \#0} is the input to a subproblem, which again allows for specification of the type of equation, and the respective method: |
|
1460 {\footnotesize\begin{verbatim} |
|
1461 ML> nxt; |
|
1462 val it = ("Subproblem",Subproblem ("SqRoot.thy",["univariate","equation"])) |
|
1463 ML> |
|
1464 ML> val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
|
1465 val f = |
|
1466 Form' (FormKF |
|
1467 (~1,EdUndef,1,Nundef,"Subproblem (SqRoot.thy, [univariate, equation])")) |
|
1468 : mout |
|
1469 val nxt = ("Refine_Tacitly",Refine_Tacitly ["univariate","equation"]) |
|
1470 ML> |
|
1471 ML> val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
|
1472 val nxt = ("Model_Problem",Model_Problem ["linear","univariate","equation"]) |
|
1473 \end{verbatim}}%size |
|
1474 As required, the tactic {\tt Refine ["univariate","equation"]} selects the appropriate type of equation from the problem hierarchy, which can be seen by the tactic {\tt Model\_Problem ["linear","univariate","equation"]} prosed by the system. |
|
1475 |
|
1476 Again the whole phase of modeling and specification follows; we skip it here, and \isac's dialog guide may decide to do so as well. |
|
1477 |
|
1478 |
|
1479 \section{The final phase: check the post-condition} |
|
1480 The type of problems solved by \isac{} are so-called 'example construction problems' as shown above. The most characteristic point of such a problem is the post-condition. The handling of the post-condition in the given context is an open research question. |
|
1481 |
|
1482 Thus the post-condition is just mentioned, in our example for both, the problem and the subproblem: |
|
1483 {\footnotesize\begin{verbatim} |
|
1484 ML> nxt; |
|
1485 val it = ("Check_Postcond",Check_Postcond ["linear","univariate","equation"]) |
|
1486 ML> |
|
1487 ML> val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
|
1488 val f = Form' (FormKF (~1,EdUndef,1,Nundef,"[x = #2]")) : mout |
|
1489 val nxt = |
|
1490 ("Check_Postcond",Check_Postcond ["normalize","univariate","equation"]) |
|
1491 ML> |
|
1492 ML> val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
|
1493 val f = Form' (FormKF (~1,EdUndef,0,Nundef,"[x = #2]")) : mout |
|
1494 val nxt = ("End_Proof'",End_Proof') : string * mstep |
|
1495 \end{verbatim}}%size |
|
1496 The next tactic proposed by the system, {\tt End\_Proof'} indicates that the proof has finished successfully.\\ |
|
1497 |
|
1498 {\it The tactics proposed by the system need {\em not} be followed by the user; the user is free to choose other tactics, and the system will report, if this is applicable at the respective proof state, or not~! The reader may try out~!} |
|
1499 |
|
1500 |
|
1501 |
|
1502 \part{Systematic description} |
|
1503 |
|
1504 |
|
1505 \chapter{The structure of the knowledge base} |
|
1506 |
|
1507 \section{Tactics and data} |
|
1508 First we view the ME from outside, i.e. we regard tactics and relate them to the knowledge base (KB). W.r.t. the KB we address the atomic items which have to be implemented in detail by the authors of the KB |
|
1509 \footnote{Some of these items are fetched by the tactics from intermediate storage within the ME, and not directly from the KB.} |
|
1510 . The items are listed in alphabetical order in Tab.\ref{kb-items} on p.\pageref{kb-items}. |
|
1511 {\begin{table}[h] |
|
1512 \caption{Atomic items of the KB} \label{kb-items} |
|
1513 %\tabcolsep=0.3mm |
|
1514 \begin{center} |
|
1515 \def\arraystretch{1.0} |
|
1516 \begin{tabular}{lp{9.0cm}} |
|
1517 abbrevation & description \\ |
|
1518 \hline |
|
1519 &\\ |
|
1520 {\it calc\_list} |
|
1521 & associationlist of the evaluation-functions {\it eval\_fn}\\ |
|
1522 {\it eval\_fn} |
|
1523 & evaluation-function for numerals and for predicates coded in SML\\ |
|
1524 {\it eval\_rls } |
|
1525 & ruleset {\it rls} for simplifying expressions with {\it eval\_fn}s\\ |
|
1526 {\it fmz} |
|
1527 & formalization, i.e. a minimal formula representation of an example \\ |
|
1528 {\it met} |
|
1529 & a method, i.e. a datastructure holding all informations for the solving phase ({\it rew\_ord}, {\it scr}, etc.)\\ |
|
1530 {\it metID} |
|
1531 & reference to a {\it met}\\ |
|
1532 {\it op} |
|
1533 & operator as key to an {\it eval\_fn} in a {\it calc\_list}\\ |
|
1534 {\it pbl} |
|
1535 & problem, i.e. a node in the problem-hierarchy\\ |
|
1536 {\it pblID} |
|
1537 & reference to a {\it pbl}\\ |
|
1538 {\it rew\_ord} |
|
1539 & rewrite-order\\ |
|
1540 {\it rls} |
|
1541 & ruleset, i.e. a datastructure holding theorems {\it thm} and operators {\it op} for simplification (with a {\it rew\_ord})\\ |
|
1542 {\it Rrls} |
|
1543 & ruleset for 'reverse rewriting' (an \isac-technique generating stepwise rewriting, e.g. for cancelling fractions)\\ |
|
1544 {\it scr} |
|
1545 & script describing algorithms by tactics, part of a {\it met} \\ |
|
1546 {\it norm\_rls} |
|
1547 & special ruleset calculating a normalform, associated with a {\it thy}\\ |
|
1548 {\it spec} |
|
1549 & specification, i.e. a tripel ({\it thyID, pblID, metID})\\ |
|
1550 {\it subs} |
|
1551 & substitution, i.e. a list of variable-value-pairs\\ |
|
1552 {\it term} |
|
1553 & Isabelle term, i.e. a formula\\ |
|
1554 {\it thm} |
|
1555 & theorem\\ |
|
1556 {\it thy} |
|
1557 & theory\\ |
|
1558 {\it thyID} |
|
1559 & reference to a {\it thy} \\ |
|
1560 \end{tabular}\end{center}\end{table} |
|
1561 } |
|
1562 The relations between tactics and data items are shown in Tab.\ref{tac-kb}on p.\pageref{tac-kb}. |
|
1563 {\def\arraystretch{1.2} |
|
1564 \begin{table}[h] |
|
1565 \caption{Which tactic uses which KB's item~?} \label{tac-kb} |
|
1566 \tabcolsep=0.3mm |
|
1567 \begin{center} |
|
1568 \begin{tabular}{|ll||cccc|ccc|cccc|} \hline |
|
1569 tactic &input & & & &norm\_& &rew\_&rls &eval\_&eval\_&calc\_& \\ |
|
1570 & &thy &scr &Rrls&rls &thm &ord &Rrls&fn &rls &list &dsc\\ |
|
1571 \hline\hline |
|
1572 Init\_Proof |
|
1573 &fmz & x & & & x & & & & & & & x \\ |
|
1574 &spec & & & & & & & & & & & \\ |
|
1575 \hline |
|
1576 \multicolumn{13}{|l|}{model phase}\\ |
|
1577 \hline |
|
1578 Add\_* &term & x & & & x & & & & & & & x \\ |
|
1579 FormFK &model & x & & & x & & & & & & & x \\ |
|
1580 \hline |
|
1581 \multicolumn{13}{|l|}{specify phase}\\ |
|
1582 \hline |
|
1583 Specify\_Theory |
|
1584 &thyID & x & & & x & & & & x & x & & x \\ |
|
1585 Specify\_Problem |
|
1586 &pblID & x & & & x & & & & x & x & & x \\ |
|
1587 Refine\_Problem |
|
1588 &pblID & x & & & x & & & & x & x & & x \\ |
|
1589 Specify\_Method |
|
1590 &metID & x & & & x & & & & x & x & & x \\ |
|
1591 Apply\_Method |
|
1592 &metID & x & x & & x & & & & x & x & & x \\ |
|
1593 \hline |
|
1594 \multicolumn{13}{|l|}{solve phase}\\ |
|
1595 \hline |
|
1596 Rewrite,\_Inst |
|
1597 &thm & x & x & & & x &met & & x &met & & \\ |
|
1598 Rewrite, Detail |
|
1599 &thm & x & x & & & x &rls & & x &rls & & \\ |
|
1600 Rewrite, Detail |
|
1601 &thm & x & x & & & x &Rrls & & x &Rrls & & \\ |
|
1602 Rewrite\_Set,\_Inst |
|
1603 &rls & x & x & & & & & x & x & x & & \\ |
|
1604 Calculate |
|
1605 &op & x & x & & & & & & & & x & \\ |
|
1606 Substitute |
|
1607 &subs & x & & & x & & & & & & & \\ |
|
1608 & & & & & & & & & & & & \\ |
|
1609 SubProblem |
|
1610 &spec & x & x & & x & & & & x & x & & x \\ |
|
1611 &fmz & & & & & & & & & & & \\ |
|
1612 \hline |
|
1613 \end{tabular}\end{center}\end{table} |
|
1614 } |
|
1615 |
|
1616 \section{\isac's theories} |
|
1617 \isac's theories build upon Isabelles theories for high-order-logic (HOL) up to the respective development of real numbers ({\tt HOL/Real}). Theories have a special format defined in \cite{Isa-ref} and the suffix {\tt *.thy}; usually theories are paired with SML-files having the same filename and the suffix {\tt *.ML}. |
|
1618 |
|
1619 \isac's theories represent the deductive part of \isac's knowledge base, the hierarchy of theories is structured accordingly. The {\tt *.ML}-files, however, contain {\em all} data of the other two axes of the knowledge base, the problems and the methods (without presenting their respective structure, which is done by the problem browser and the method browser, see \ref{pbt}). |
|
1620 |
|
1621 Tab.\ref{theories} on p.\pageref{theories} lists the basic theories planned to be implemented in version \isac.1. We expext the list to be expanded in the near future, actually, have a look to the theory browser~! |
|
1622 |
|
1623 The first three theories in the list do {\em not} belong to \isac's knowledge base; they are concerned with \isac's script-language for methods and listed here for completeness. |
|
1624 {\begin{table}[h] |
|
1625 \caption{Theories in \isac-version I} \label{theories} |
|
1626 %\tabcolsep=0.3mm |
|
1627 \begin{center} |
|
1628 \def\arraystretch{1.0} |
|
1629 \begin{tabular}{lp{9.0cm}} |
|
1630 theory & description \\ |
|
1631 \hline |
|
1632 &\\ |
|
1633 ListI.thy |
|
1634 & assigns identifiers to the functions defined in {\tt Isabelle2002/src/HOL/List.thy} and (intermediatly~?) defines some more list functions\\ |
|
1635 ListI.ML |
|
1636 & {\tt eval\_fn} for the additional list functions\\ |
|
1637 Tools.thy |
|
1638 & functions required for the evaluation of scripts\\ |
|
1639 Tools.ML |
|
1640 & the respective {\tt eval\_fn}s\\ |
|
1641 Script.thy |
|
1642 & prerequisites for scripts: types, tactics, tacticals,\\ |
|
1643 Script.ML |
|
1644 & sets of tactics and functions for internal use\\ |
|
1645 & \\ |
|
1646 \hline |
|
1647 & \\ |
|
1648 Typefix.thy |
|
1649 & an intermediate hack for escaping type errors\\ |
|
1650 Descript.thy |
|
1651 & {\it description}s for the formulas in {\it model}s and {\it problem}s\\ |
|
1652 Atools |
|
1653 & (re-)definition of operators; general predicates and functions for preconditions; theorems for the {\tt eval\_rls}\\ |
|
1654 Float |
|
1655 & floating point numerals\\ |
|
1656 Equation |
|
1657 & basic notions for equations and equational systems\\ |
|
1658 Poly |
|
1659 & polynomials\\ |
|
1660 PolyEq |
|
1661 & polynomial equations and equational systems \\ |
|
1662 Rational.thy |
|
1663 & additional theorems for rationals\\ |
|
1664 Rational.ML |
|
1665 & cancel, add and simplify rationals using (a generalization of) Euclids algorithm; respective reverse rulesets\\ |
|
1666 RatEq |
|
1667 & equations on rationals\\ |
|
1668 Root |
|
1669 & radicals; calculate normalform; respective reverse rulesets\\ |
|
1670 RootEq |
|
1671 & equations on roots\\ |
|
1672 RatRootEq |
|
1673 & equations on rationals and roots (i.e. on terms containing both operations)\\ |
|
1674 Vect |
|
1675 & vector analysis\\ |
|
1676 Trig |
|
1677 & trigonometriy\\ |
|
1678 LogExp |
|
1679 & logarithms and exponential functions\\ |
|
1680 Calculus |
|
1681 & nonstandard analysis\\ |
|
1682 Diff |
|
1683 & differentiation\\ |
|
1684 DiffApp |
|
1685 & applications of differentiaten (maxima-minima-problems)\\ |
|
1686 Test |
|
1687 & (old) data for the test suite\\ |
|
1688 Isac |
|
1689 & collects all \isac-theoris.\\ |
|
1690 \end{tabular}\end{center}\end{table} |
|
1691 } |
|
1692 |
|
1693 |
|
1694 \section{Data in {\tt *.thy}- and {\tt *.ML}-files} |
|
1695 As already mentioned, theories come in pairs of {\tt *.thy}- and {\tt *.ML}-files with the same respective filename. How data are distributed between the two files is shown in Tab.\ref{thy-ML} on p.\pageref{thy-ML}. |
|
1696 {\begin{table}[h] |
|
1697 \caption{Data in {\tt *.thy}- and {\tt *.ML}-files} \label{thy-ML} |
|
1698 \tabcolsep=2.0mm |
|
1699 \begin{center} |
|
1700 \def\arraystretch{1.0} |
|
1701 \begin{tabular}{llp{7.7cm}} |
|
1702 file & data & description \\ |
|
1703 \hline |
|
1704 & &\\ |
|
1705 {\tt *.thy} |
|
1706 & consts |
|
1707 & operators, predicates, functions, script-names ('{\tt Script} name \dots{\tt arguments}') |
|
1708 \\ |
|
1709 & rules |
|
1710 & theorems: \isac{} uses Isabelles theorems if possible; additional theorems analoguous to such existing in Isabelle get the Isabelle-identifier attached an {\it I} |
|
1711 \\& &\\ |
|
1712 {\tt *.ML} |
|
1713 & {\tt theory' :=} |
|
1714 & the theory defined by the actual {\tt *.thy}-file is made accessible to \isac |
|
1715 \\ |
|
1716 & {\tt eval\_fn} |
|
1717 & evaluation function for operators and predicates, coded on the meta-level (SML); the identifier of such a function is a combination of the keyword {\tt eval\_} with the identifier of the function as defined in {\tt *.thy} |
|
1718 \\ |
|
1719 & {\tt *\_simplify} |
|
1720 & the canonical simplifier for the actual theory, i.e. the identifier for this ruleset is a combination of the theories identifier and the keyword {\tt *\_simplify} |
|
1721 \\ |
|
1722 & {\tt norm\_rls :=} |
|
1723 & the canonical simplifier {\tt *\_simplify} is stored such that it is accessible for \isac |
|
1724 \\ |
|
1725 & {\tt rew\_ord' :=} |
|
1726 & the same for rewrite orders, if needed outside of one particular ruleset |
|
1727 \\ |
|
1728 & {\tt ruleset' :=} |
|
1729 & the same for rulesets (ordinary rulesets, reverse rulesets and {\tt eval\_rls}) |
|
1730 \\ |
|
1731 & {\tt calc\_list :=} |
|
1732 & the same for {\tt eval\_fn}s, if needed outside of one particular ruleset (e.g. for a tactic {\tt Calculate} in a script) |
|
1733 \\ |
|
1734 & {\tt store\_pbl} |
|
1735 & problems defined within this {\tt *.ML}-file are made accessible for \isac |
|
1736 \\ |
|
1737 & {\tt methods :=} |
|
1738 & methods defined within this {\tt *.ML}-file are made accessible for \isac |
|
1739 \\ |
|
1740 \end{tabular}\end{center}\end{table} |
|
1741 } |
|
1742 The order of the data-items within the theories should adhere to the order given in this list. |
|
1743 |
|
1744 \section{Formal description of the problem-hierarchy} |
|
1745 %for Richard Lang |
|
1746 |
|
1747 \section{Script tactics} |
|
1748 The tactics actually promote the calculation: they construct the prooftree behind the scenes, and they are the points during evaluation where the script-interpreter transfers control to the user. Here we only describe the sytax of the tactics; the semantics is described on p.\pageref{user-tactics} below in context with the tactics the student uses ('user-tactics'): there is a 1-to-1 correspondence between user-tactics and script-tactics. |
|
1749 |
|
1750 |
|
1751 |
|
1752 |
|
1753 |
|
1754 \part{Authoring on the knowledge} |
|
1755 |
|
1756 |
|
1757 \section{Add a theorem} |
|
1758 \section{Define and add a problem} |
|
1759 \section{Define and add a predicate} |
|
1760 \section{Define and add a method} |
|
1761 \section{} |
|
1762 \section{} |
|
1763 \section{} |
|
1764 \section{} |
|
1765 |
|
1766 |
|
1767 |
|
1768 \newpage |
|
1769 \bibliography{bib/isac,bib/from-theses} |
|
1770 |
|
1771 \end{document} |
|