1 (* tools for rewriting, reverse rewriting, context to thy concerning rewriting
2 authors: Walther Neuper 2002, 2006
3 (c) due to copyright terms
11 (***.reverse rewriting.***)
13 (*.derivation for insertin one level of nodes into the calctree.*)
14 type deriv = (term * rule * (term *term list)) list;
16 fun trta2str (t,r,(t',a)) = "\n("^(term2str t)^", "^(rule2str' r)^", ("^
17 (term2str t')^", "^(terms2str a)^"))";
18 fun trtas2str trtas = (strs2str o (map trta2str)) trtas;
19 val deriv2str = trtas2str;
20 fun rta2str (r,(t,a)) = "\n("^(rule2str' r)^", ("^
21 (term2str t)^", "^(terms2str a)^"))";
22 fun rtas2str rtas = (strs2str o (map rta2str)) rtas;
23 val deri2str = rtas2str;
26 (*.A1==>...==>An==>(Lhs = Rhs) goes to A1==>...==>An==>(Rhs = Lhs).*)
29 val (deriv, {thy_ref = thy_ref, tags = tags, maxidx = maxidx,
30 shyps = shyps, hyps = hyps, tpairs = tpairs,
33 val (lhs,rhs) = (dest_equals' o strip_trueprop
34 o Logic.strip_imp_concl) prop;
35 val prop' = case strip_imp_prems' prop of
36 NONE => Trueprop $ (mk_equality (rhs, lhs))
38 ins_concl cs (Trueprop $ (mk_equality (rhs, lhs)));
39 in assbl_thm deriv thy_ref tags maxidx shyps hyps tpairs prop' end;
41 (sym RS real_mult_div_cancel1) handle e => print_exn e;
42 Exception THM 1 raised:
45 "?k ~= 0 ==> ?k * ?m / (?k * ?n) = ?m / ?n"
47 val thm = real_mult_div_cancel1;
48 val prop = (#prop o rep_thm) thm;
50 val ppp = Logic.strip_imp_concl prop;
52 ((#prop o rep_thm o sym_thm o sym_thm) thm) = (#prop o rep_thm) thm;
54 ((sym_thm o sym_thm) thm) = thm;
57 val thm = real_le_anti_sym;
58 ((sym_thm o sym_thm) thm) = thm;
61 val thm = real_minus_zero;
62 ((sym_thm o sym_thm) thm) = thm;
65 (*WN10-910 weaker than fun sym_thm for Theory.axioms_of in isa02*)
67 let val (lhs,rhs) = (dest_equals' o strip_trueprop
68 o Logic.strip_imp_concl) trm;
69 val trm' = case strip_imp_prems' trm of
70 NONE => mk_equality (rhs, lhs)
72 ins_concl cs (mk_equality (rhs, lhs));
75 val trm = @{term "k ~= 0 ==> k * m / (k * n) = m / n"};
76 (tracing o (Syntax.string_of_term @{context})) (sym_trm trm);
77 "~ k = (0::'a) ==> m / n = k * m / (k * n)"
82 (*.derive normalform of a rls, or derive until SOME goal,
83 and record rules applied and rewrites.
88 -> rew_ord : the order of this rls, which 1 theorem of is used
89 for rewriting 1 single step (?14.4.03)
90 -> term option : 040214 ??? nonsense ???
92 -> (term * : to this term ...
93 rule * : ... this rule is applied yielding ...
94 (term * : ... this term ...
95 term list)) : ... under these assumptions.
97 returns empty list for a normal form
98 FIXME.WN040214: treats rules as in Rls, _not_ as in Seq
100 WN060825 too complicated for the intended use by cancel_, common_nominator_
101 and unreflectedly adapted to extion of rules by Rls_: returns Rls_("sym_simpl..
103 (* val (thy, erls, rs, ro, goal, tt) = (thy, erls, rs, ro, goal, t);
104 val (thy, erls, rs, ro, goal, tt) = (thy, Atools_erls, rules, ro, NONE, tt);
106 fun make_deriv thy erls (rs:rule list) ro(*rew_ord*) goal tt =
107 let datatype switch = Appl | Noap
108 fun rew_once lim rts t Noap [] =
112 error ("make_deriv: no derivation for "^(term2str t)))
113 | rew_once lim rts t Appl [] =
114 (*(case rs of Rls _ =>*) rew_once lim rts t Noap rs
115 (*| Seq _ => rts) FIXXXXXME 14.3.03*)
116 | rew_once lim rts t apno rs' =
118 NONE => rew_or_calc lim rts t apno rs'
121 else rew_or_calc lim rts t apno rs')
122 and rew_or_calc lim rts t apno (rrs' as (r::rs')) =
124 then (tracing ("make_deriv exceeds " ^ int2str (!lim_deriv) ^
125 "with deriv =\n"); tracing (deriv2str rts); rts)
129 (if not (!trace_rewrite) then () else
130 tracing ("### trying thm '" ^ thmid ^ "'");
131 case rewrite_ thy ro erls true tm t of
132 NONE => rew_once lim rts t apno rs'
135 then tracing ("### rewrites to: "^(term2str t')) else();
136 rew_once (lim-1) (rts@[(t,r,(t',a'))]) t' Appl rrs'))
137 | Calc (c as (op_,_)) =>
138 let val _ = if not (!trace_rewrite) then () else
139 tracing ("### trying calc. '" ^ op_ ^ "'")
140 val t = uminus_to_string t
141 in case get_calculation_ thy c t of
142 NONE => rew_once lim rts t apno rs'
143 | SOME (thmid, tm) =>
144 (let val SOME (t',a') = rewrite_ thy ro erls true tm t
145 val _ = if not (!trace_rewrite) then () else
146 tracing("### calc. to: " ^ (term2str t'))
147 val r' = Thm (thmid, tm)
148 in rew_once (lim-1) (rts@[(t,r',(t',a'))]) t' Appl rrs'
150 handle _ => error "derive_norm, Calc: no rewrite"
152 (* TODO.WN080222: see rewrite__set_
153 @@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@
154 | Cal1 (cc as (op_,_)) =>
155 (let val _= if !trace_rewrite andalso i < ! depth then
156 tracing((idt"#"(i+1))^" try cal1: "^op_^"'") else ();
157 val ct = uminus_to_string ct
158 in case get_calculation_ thy cc ct of
160 | SOME (thmid, thm') =>
163 rewrite__ thy (i+1) bdv ((snd o #rew_ord o rep_rls) rls)
164 ((#erls o rep_rls) rls) put_asm thm' ct;
165 val _ = if pairopt <> NONE then ()
166 else error("rewrite_set_, rewrite_ \""^
167 (string_of_thmI thm')^"\" "^(term2str ct)^" = NONE")
168 val _ = if ! trace_rewrite andalso i < ! depth
169 then tracing((idt"="(i+1))^" cal1. to: "^
170 (term2str ((fst o the) pairopt)))
174 @@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@*)
176 (case rewrite_set_ thy true rls t of
177 NONE => rew_once lim rts t apno rs'
179 rew_once (lim-1) (rts @ [(t,r,(t',a'))]) t' Appl rrs');
180 (*WN060829 | Rls_ rls =>
181 (case rewrite_set_ thy true rls t of
182 NONE => rew_once lim rts t apno rs'
184 if ro [] (t, t') then rew_once lim rts t apno rs'
185 else rew_once (lim-1) (rts@[(t,r,(t',a'))]) t' Appl rrs');
186 ...lead to deriv = [] with make_polynomial.
187 THERE IS SOMETHING DIFFERENT beetween rewriting with the code above
188 and between rewriting with rewrite_set: with rules from make_polynomial and
189 t = "(a^^^2 + -1*b^^^2) / (a^^^2 + -2*a*b + b^^^2)" the actual code
190 leads to cycling Rls_ order_mult_rls_..Rls_ discard_parentheses1..Rls_ order..
192 in rew_once (!lim_deriv) [] tt Noap rs end;
195 (*.toggles the marker for 'fun sym_thm'.*)
196 fun sym_thmID (thmID : thmID) =
197 case explode thmID of
198 "s"::"y"::"m"::"_"::id => implode id : thmID
199 | id => "sym_"^thmID;
201 > val thmID = "sym_real_mult_2";
203 val it = "real_mult_2" : string
204 > val thmID = "real_num_collect";
206 val it = "sym_real_num_collect" : string*)
207 fun sym_drop (thmID : thmID) =
208 case explode thmID of
209 "s"::"y"::"m"::"_"::id => implode id : thmID
211 fun is_sym (thmID : thmID) =
212 case explode thmID of
213 "s"::"y"::"m"::"_"::id => true
217 (*FIXXXXME.040219: detail has to handle Rls id="sym_..."
218 by applying make_deriv, rev_deriv'; see concat_deriv*)
219 fun sym_rls Erls = Erls
220 | sym_rls (Rls {id, scr, calc, erls, srls, rules, rew_ord, preconds}) =
221 Rls {id="sym_"^id, scr=scr, calc=calc, erls=erls, srls=srls,
222 rules=rules, rew_ord=rew_ord, preconds=preconds}
223 | sym_rls (Seq {id, scr, calc, erls, srls, rules, rew_ord, preconds}) =
224 Seq {id="sym_"^id, scr=scr, calc=calc, erls=erls, srls=srls,
225 rules=rules, rew_ord=rew_ord, preconds=preconds}
226 | sym_rls (Rrls {id, scr, calc, erls, prepat, rew_ord}) =
227 Rrls {id="sym_"^id, scr=scr, calc=calc, erls=erls, prepat=prepat,
230 fun sym_Thm (Thm (thmID, thm)) = Thm (sym_thmID thmID, sym_thm thm)
231 | sym_Thm (Rls_ rls) = Rls_ (*WN060825?!?*) (sym_rls rls)
232 | sym_Thm r = error ("sym_Thm: not for "^(rule2str r));
234 val th = Thm ("real_one_collect",num_str @{thm real_one_collect});
237 Thm ("real_one_collect","?m is_const ==> ?n + ?m * ?n = (1 + ?m) * ?n")
240 Thm ("sym_real_one_collect","?m is_const ==> (1 + ?m) * ?n = ?n + ?m * ?n")*)
243 (*version for reverse rewrite used before 040214*)
244 fun rev_deriv (t, r, (t', a)) = (sym_Thm r, (t, a));
245 (* val (thy, erls, rs, ro, goal, t) = (thy, eval_rls, rules, ro, NONE, t');
247 fun reverse_deriv thy erls (rs:rule list) ro(*rew_ord*) goal t =
248 (rev o (map rev_deriv)) (make_deriv thy erls (rs:rule list) ro goal t);
250 val rev_rew = reverse_deriv thy e_rls ;
251 tracing(rtas2str rev_rew);
254 fun eq_Thm (Thm (id1,_), Thm (id2,_)) = id1 = id2
255 | eq_Thm (Thm (id1,_), _) = false
256 | eq_Thm (Rls_ r1, Rls_ r2) = id_rls r1 = id_rls r2
257 | eq_Thm (Rls_ r1, _) = false
258 | eq_Thm (r1, r2) = error ("eq_Thm: called with '"^
259 (rule2str r1)^"' '"^(rule2str r2)^"'");
260 fun distinct_Thm r = gen_distinct eq_Thm r;
262 fun eq_Thms thmIDs thm = (member op = thmIDs (id_of_thm thm))
266 (***. context to thy concerning rewriting .***)
268 (*.create the unique handles and filenames for the theory-data.*)
269 fun part2guh ([str]:theID) =
271 "Isabelle" => "thy_isab_" ^ str ^ "-part" : guh
272 | "IsacScripts" => "thy_scri_" ^ str ^ "-part"
273 | "IsacKnowledge" => "thy_isac_" ^ str ^ "-part"
274 | str => error ("thy2guh: called with '"^str^"'"))
275 | part2guh theID = error ("part2guh called with theID = "
277 fun part2filename str = part2guh str ^ ".xml" : filename;
280 fun thy2guh ([part, thyID]:theID) =
282 "Isabelle" => "thy_isab_" ^ thyID : guh
283 | "IsacScripts" => "thy_scri_" ^ thyID
284 | "IsacKnowledge" => "thy_isac_" ^ thyID
285 | str => error ("thy2guh: called with '"^str^"'"))
286 | thy2guh theID = error ("thy2guh called with '"^strs2str' theID^"'");
287 fun thy2filename thy' = thy2guh thy' ^ ".xml" : filename;
288 fun thypart2guh ([part, thyID, thypart]:theID) =
290 "Isabelle" => "thy_isab_" ^ thyID ^ "-" ^ thypart : guh
291 | "IsacScripts" => "thy_scri_" ^ thyID ^ "-" ^ thypart
292 | "IsacKnowledge" => "thy_isac_" ^ thyID ^ "-" ^ thypart
293 | str => error ("thypart2guh: called with '"^str^"'");
294 fun thypart2filename thy' = thypart2guh thy' ^ ".xml" : filename;
296 (*.convert the data got via contextToThy to a globally unique handle
297 there is another way to get the guh out of the 'theID' in the hierarchy.*)
298 fun thm2guh (isa, thyID:thyID) (thmID:thmID) =
301 "thy_isab_" ^ theory'2thyID thyID ^ "-thm-" ^ strip_thy thmID : guh
303 "thy_isac_" ^ theory'2thyID thyID ^ "-thm-" ^ strip_thy thmID
305 "thy_scri_" ^ theory'2thyID thyID ^ "-thm-" ^ strip_thy thmID
306 | str => error ("thm2guh called with isa = '"^isa^
307 "' for thm = "^thmID^"'");
308 fun thm2filename (isa_thyID: string * thyID) thmID =
309 (thm2guh isa_thyID thmID) ^ ".xml" : filename;
311 fun rls2guh (isa, thyID:thyID) (rls':rls') =
314 "thy_isab_" ^ theory'2thyID thyID ^ "-rls-" ^ rls' : guh
316 "thy_isac_" ^ theory'2thyID thyID ^ "-rls-" ^ rls'
318 "thy_scri_" ^ theory'2thyID thyID ^ "-rls-" ^ rls'
319 | str => error ("rls2guh called with isa = '"^isa^
320 "' for rls = '"^rls'^"'");
321 fun rls2filename (isa, thyID) rls' =
322 rls2guh (isa, thyID) rls' ^ ".xml" : filename;
324 fun cal2guh (isa, thyID:thyID) calID =
327 "thy_isab_" ^ theory'2thyID thyID ^ "-cal-" ^ calID : guh
329 "thy_isac_" ^ theory'2thyID thyID ^ "-cal-" ^ calID
331 "thy_scri_" ^ theory'2thyID thyID ^ "-cal-" ^ calID
332 | str => error ("cal2guh called with isa = '"^isa^
333 "' for cal = '"^calID^"'");
334 fun cal2filename (isa, thyID:thyID) calID =
335 cal2guh (isa, thyID:thyID) calID ^ ".xml" : filename;
337 fun ord2guh (isa, thyID:thyID) (rew_ord':rew_ord') =
340 "thy_isab_" ^ theory'2thyID thyID ^ "-ord-" ^ rew_ord' : guh
342 "thy_isac_" ^ theory'2thyID thyID ^ "-ord-" ^ rew_ord'
344 "thy_scri_" ^ theory'2thyID thyID ^ "-ord-" ^ rew_ord'
345 | str => error ("ord2guh called with isa = '"^isa^
346 "' for ord = '"^rew_ord'^"'");
347 fun ord2filename (isa, thyID:thyID) (rew_ord':rew_ord') =
348 ord2guh (isa, thyID:thyID) (rew_ord':rew_ord') ^ ".xml" : filename;
351 (**.set up isab_thm_thy in Isac.ML.**)
353 fun rearrange (thyID, (thmID, thm)) = (thmID, (thyID, thm));
354 fun rearrange_inv (thmID, (thyID, thm)) = (thyID, (thmID, thm));
356 (*.lookup the missing theorems in some thy (of Isabelle).*)
357 fun make_isa missthms thy =
358 map (pair (theory2thyID thy))
359 ((inter eq_thmI) missthms (PureThy.all_thms_of thy))
360 : (thyID * (thmID * Thm.thm)) list;
362 (*.separate handling of sym_thms.*)
363 fun make_isab rlsthmsNOTisac isab_thys =
364 let fun les ((s1,_), (s2,_)) = (s1 : string) < s2
365 val notsym = filter_out (is_sym o #1) rlsthmsNOTisac
366 val notsym_isab = (flat o (map (make_isa notsym))) isab_thys
368 val sym = filter (is_sym o #1) rlsthmsNOTisac
370 val symsym = map ((apfst sym_drop) o (apsnd sym_thm)) sym
371 val symsym_isab = (flat o (map (make_isa symsym))) isab_thys
373 val sym_isab = map (((apsnd o apfst) sym_drop) o
374 ((apsnd o apsnd) sym_thm)) symsym_isab
376 val isab = notsym_isab @ symsym_isab @ sym_isab
377 in ((map rearrange) o (gen_sort les)) isab
378 : (thmID * (thyID * Thm.thm)) list
380 (* version with term instead of thm, for Theory.axioms_of in isa02*)
381 fun make_isa missthms thy =
382 map (pair (theory2thyID thy))
383 ((inter eq_thmI') missthms (Theory.axioms_of thy))
384 : (thyID * (thmID * term)) list;
385 fun make_isab rlsthmsNOTisac isab_thys =
386 let fun les ((s1,_), (s2,_)) = (s1 : string) < s2
387 val notsym = filter_out (is_sym o #1) rlsthmsNOTisac
388 val notsym_isab = (flat o (map (make_isa notsym))) isab_thys
390 val sym = filter (is_sym o #1) rlsthmsNOTisac
392 val symsym = map ((apfst sym_drop) o (apsnd sym_trm)) sym
393 val symsym_isab = (flat o (map (make_isa symsym))) isab_thys
395 val sym_isab = map (((apsnd o apfst) sym_drop) o
396 ((apsnd o apsnd) sym_trm)) symsym_isab
398 val isab = notsym_isab @ symsym_isab @ sym_isab
399 in ((map rearrange) o (gen_sort les)) isab
400 : (thmID * (thyID * term)) list
403 (*.which theory below thy' contains a theorem; this can be in isabelle !
404 get the occurence _after_ in the _list_ (is up to asking TUM) theory'.*)
405 (* val (str, (_, thy)) = ("real_diff_minus", ("Root.thy", Root.thy));
406 val (str, (_, thy)) = ("real_diff_minus", ("Poly.thy", Poly.thy));
408 fun thy_contains_thm (str:xstring) (_, thy) =
409 member op = (map (strip_thy o fst) (PureThy.all_thms_of thy)) str;
410 (* val (thy', str) = ("Isac.thy", "real_mult_minus1");
411 val (thy', str) = ("PolyMinus.thy", "klammer_minus_plus");
413 fun thy_containing_thm (thy':theory') (str:xstring) =
414 let val thy' = thyID2theory' thy'
415 val str = sym_drop str
416 val startsearch = dropuntil ((curry op= thy') o
417 (#1:theory' * theory -> theory'))
419 in case find_first (thy_contains_thm str) startsearch of
420 SOME (thy',_) => ("IsacKnowledge", thy')
421 | NONE => (case assoc (!isab_thm_thy (*see Isac.ML*), str) of
422 SOME (thyID,_) => ("Isabelle", thyID)
424 error ("thy_containing_thm: theorem '"^str^
425 "' not in !theory' above thy '"^thy'^"'"))
429 (*.which theory below thy' contains a ruleset;
430 get the occurence _after_ in the _list_ (is up to asking TUM) theory'.*)
431 (* val (thy', rls') = ("PolyEq.thy", "separate_bdv");
433 local infix mem; (*from Isabelle2002*)
435 | x mem (y :: ys) = x = y orelse x mem ys;
437 fun thy_containing_rls (thy':theory') (rls':rls') =
438 let val rls' = strip_thy rls'
439 val thy' = thyID2theory' thy'
440 (*take thys between "Isac" and thy' not to search #1#*)
441 val dropthys = takewhile [] (not o (curry op= thy') o
442 (#1:theory' * theory -> theory'))
444 val dropthy's = map (get_thy o (#1 : (theory' * theory) -> theory'))
446 (*drop those rulesets which are generated in a theory found in #1#*)
447 val startsearch = filter_out ((curry ((op mem) o swap) dropthy's) o
448 ((#1 o #2) : rls' * (theory' * rls)
451 in case assoc (startsearch, rls') of
452 SOME (thy', _) => ("IsacKnowledge", thyID2theory' thy')
453 | _ => error ("thy_containing_rls : rls '"^rls'^
454 "' not in !rulset' above thy '"^thy'^"'")
456 (* val (thy', termop) = (thyID, termop);
458 fun thy_containing_cal (thy':theory') termop =
459 let val thy' = thyID2theory' thy'
460 val dropthys = takewhile [] (not o (curry op= thy') o
461 (#1:theory' * theory -> theory'))
463 val dropthy's = map (get_thy o (#1 : (theory' * theory) -> theory'))
465 val startsearch = filter_out ((curry ((op mem) o swap) dropthy's) o
466 (#1 : calc -> string)) (rev (!calclist'))
467 in case assoc (startsearch, strip_thy termop) of
468 SOME (th_termop, _) => ("IsacKnowledge", strip_thy th_termop)
469 | _ => error ("thy_containing_rls : rls '"^termop^
470 "' not in !calclist' above thy '"^thy'^"'")
474 (* print_depth 99; map #1 startsearch; print_depth 3;
477 (*.packing return-values to matchTheory, contextToThy for xml-generation.*)
478 datatype contthy = (*also an item from KEStore on Browser ......#*)
479 EContThy (*not from KEStore ...........................*)
480 | ContThm of (*a theorem in contex =============*)
481 {thyID : thyID, (*for *2guh in sub-elems here .*)
482 thm : guh, (*theorem in the context .*)
483 applto : term, (*applied to formula ... .*)
484 applat : term, (*... with lhs inserted .*)
485 reword : rew_ord', (*order used for rewrite .*)
486 asms : (term (*asumption instantiated .*)
487 * term) list, (*asumption evaluated .*)
488 lhs : term (*lhs of the theorem ... #*)
489 * term, (*... instantiated .*)
490 rhs : term (*rhs of the theorem ... #*)
491 * term, (*... instantiated .*)
492 result : term, (*resulting from the rewrite .*)
493 resasms : term list, (*... with asms stored .*)
494 asmrls : rls' (*ruleset for evaluating asms .*)
496 | ContThmInst of (*a theorem with bdvs in contex ======== *)
497 {thyID : thyID, (*for *2guh in sub-elems here .*)
498 thm : guh, (*theorem in the context .*)
499 bdvs : subst, (*bound variables to modify....*)
500 thminst : term, (*... theorem instantiated .*)
501 applto : term, (*applied to formula ... .*)
502 applat : term, (*... with lhs inserted .*)
503 reword : rew_ord', (*order used for rewrite .*)
504 asms : (term (*asumption instantiated .*)
505 * term) list, (*asumption evaluated .*)
506 lhs : term (*lhs of the theorem ... #*)
507 * term, (*... instantiated .*)
508 rhs : term (*rhs of the theorem ... #*)
509 * term, (*... instantiated .*)
510 result : term, (*resulting from the rewrite .*)
511 resasms : term list, (*... with asms stored .*)
512 asmrls : rls' (*ruleset for evaluating asms .*)
514 | ContRls of (*a rule set in contex ===================== *)
515 {thyID : thyID, (*for *2guh in sub-elems here .*)
516 rls : guh, (*rule set in the context .*)
517 applto : term, (*rewrite this formula .*)
518 result : term, (*resulting from the rewrite .*)
519 asms : term list (*... with asms stored .*)
521 | ContRlsInst of (*a rule set with bdvs in contex ======= *)
522 {thyID : thyID, (*for *2guh in sub-elems here .*)
523 rls : guh, (*rule set in the context .*)
524 bdvs : subst, (*for bound variables in thms .*)
525 applto : term, (*rewrite this formula .*)
526 result : term, (*resulting from the rewrite .*)
527 asms : term list (*... with asms stored .*)
529 | ContNOrew of (*no rewrite for thm or rls ============== *)
530 {thyID : thyID, (*for *2guh in sub-elems here .*)
531 thm_rls : guh, (*thm or rls in the context .*)
532 applto : term (*rewrite this formula .*)
534 | ContNOrewInst of (*no rewrite for some instantiation == *)
535 {thyID : thyID, (*for *2guh in sub-elems here .*)
536 thm_rls : guh, (*thm or rls in the context .*)
537 bdvs : subst, (*for bound variables in thms .*)
538 thminst : term, (*... theorem instantiated .*)
539 applto : term (*rewrite this formula .*)
542 (*.check a rewrite-tac for bdv (RL always used *_Inst !) TODO.WN060718
543 pass other tacs unchanged.*)
544 fun get_tac_checked pt ((p,p_) : pos') = get_obj g_tac pt p;
550 (*.get the formula f at ptp rewritten by the Rewrite_* already applied to f.*)
551 (* val (Rewrite' (thy', ord', erls, _, (thmID,_), f, (res,asm))) = tac';
553 fun context_thy (pt, pos as (p,p_)) (tac as Rewrite (thmID,_)) =
554 (case applicable_in pos pt tac of
555 Appl (Rewrite' (thy', ord', erls, _, (thmID,_), f, (res,asm))) =>
556 let val thy = assoc_thy thy'
557 val thm = (norm o #prop o rep_thm o (PureThy.get_thm thy)) thmID
558 (*WN060616 the following must be done on subterm found _IN_ rew_sub
559 val (lhs,rhs) = (dest_equals' o strip_trueprop
560 o Logic.strip_imp_concl) thm
561 val insts = Pattern.match (Sign.tsig_of (sign_of thy)) (lhs, f)
562 val thm' = ren_inst (insts, thm, lhs, f)
563 val (lhs',rhs') = (dest_equals' o strip_trueprop
564 o Logic.strip_imp_concl) thm'
565 val asms = map strip_trueprop (Logic.strip_imp_prems thm)
566 val asms' = map strip_trueprop (Logic.strip_imp_prems thm')
568 in ContThm {thyID = theory'2thyID thy',
569 thm = thm2guh (thy_containing_thm thy' thmID) thmID,
573 asms = [](*asms ~~ asms'*),
574 lhs = (e_term, e_term)(*(lhs, lhs')*),
575 rhs = (e_term, e_term)(*(rhs, rhs')*),
578 asmrls = id_rls erls}
581 let val pp = par_pblobj pt p
582 val thy' = get_obj g_domID pt pp
584 Frm => get_obj g_form pt p
585 | Res => (fst o (get_obj g_result pt)) p
586 in ContNOrew {thyID = theory'2thyID thy',
587 thm_rls = thm2guh (thy_containing_thm thy' thmID) thmID,
591 (* val ((pt,p), tac as Rewrite_Inst (subs, (thmID,_))) = ((pt,pos), tac);
593 | context_thy (pt, pos as (p,p_))
594 (tac as Rewrite_Inst (subs, (thmID,_))) =
595 (case applicable_in pos pt tac of
596 (* val Appl (Rewrite_Inst' (thy', ord', erls, _, subst, (thmID,_),
597 f, (res,asm))) = applicable_in p pt tac;
599 Appl (Rewrite_Inst' (thy', ord', erls, _, subst, (thmID,_),
600 f, (res,(*path to subterm,*)asm))) =>
601 let val thm = (norm o #prop o rep_thm o
602 (PureThy.get_thm (assoc_thy thy'))) thmID
603 val thminst = inst_bdv subst thm
604 (*WN060616 the following must be done on subterm found _IN_ rew_sub
605 val (lhs,rhs) = (dest_equals' o strip_trueprop
606 o Logic.strip_imp_concl) thminst
607 val insts = Pattern.match (Sign.tsig_of (sign_of thy)) (lhs, f)
608 val thm' = ren_inst (insts, thminst, lhs, f)
609 val (lhs',rhs') = (dest_equals' o strip_trueprop
610 o Logic.strip_imp_concl) thm'
611 val asms = map strip_trueprop (Logic.strip_imp_prems thminst)
612 val asms' = map strip_trueprop (Logic.strip_imp_prems thm')
614 in ContThmInst {thyID = theory'2thyID thy',
615 thm = thm2guh (thy_containing_thm
622 asms = [](*asms ~~ asms'*),
623 lhs = (e_term, e_term)(*(lhs, lhs')*),
624 rhs = (e_term, e_term)(*(rhs, rhs')*),
627 asmrls = id_rls erls}
630 let val pp = par_pblobj pt p
631 val thy' = get_obj g_domID pt pp
632 val subst = subs2subst (assoc_thy thy') subs
633 val thm = (norm o #prop o rep_thm o
634 (PureThy.get_thm (assoc_thy thy'))) thmID
635 val thminst = inst_bdv subst thm
637 Frm => get_obj g_form pt p
638 | Res => (fst o (get_obj g_result pt)) p
639 in ContNOrewInst {thyID = theory'2thyID thy',
640 thm_rls = thm2guh (thy_containing_thm
646 | context_thy (pt,p) (tac as Rewrite_Set rls') =
647 (case applicable_in p pt tac of
648 Appl (Rewrite_Set' (thy', _, rls, f, (res,asm))) =>
649 ContRls {thyID = theory'2thyID thy',
650 rls = rls2guh (thy_containing_rls thy' rls') rls',
654 | context_thy (pt,p) (tac as Rewrite_Set_Inst (subs, rls')) =
655 (case applicable_in p pt tac of
656 Appl (Rewrite_Set_Inst' (thy', _, subst, rls, f, (res,asm))) =>
657 ContRlsInst {thyID = theory'2thyID thy',
658 rls = rls2guh (thy_containing_rls thy' rls') rls',
664 (*.get all theorems in a rule set (recursivley containing rule sets).*)
665 fun thm_of_rule Erule = []
666 | thm_of_rule (thm as Thm _) = [thm]
667 | thm_of_rule (Calc _) = []
668 | thm_of_rule (Cal1 _) = []
669 | thm_of_rule (Rls_ rls) = thms_of_rls rls
670 and thms_of_rls Erls = []
671 | thms_of_rls (Rls {rules,...}) = (flat o (map thm_of_rule)) rules
672 | thms_of_rls (Seq {rules,...}) = (flat o (map thm_of_rule)) rules
673 | thms_of_rls (Rrls _) = [];
674 (* val Hrls {thy_rls = (_, rls),...} =
675 get_the ["IsacKnowledge", "Test", "Rulesets", "expand_binomtest"];
679 (*. check if a rule is contained in a rule-set (recursivley down in Rls_);
680 this rule can even be a rule-set itself.*)
681 fun contains_rule r rls =
682 let fun find (r, Rls_ rls) = finds (get_rules rls)
683 | find r12 = eq_rule r12
685 | finds (r1 :: rs) = if eq_rule (r, r1) then true else finds rs;
687 (*tracing ("### contains_rule: r = "^rule2str r^", rls = "^rls2str rls);*)
688 finds (get_rules rls)
691 (*. try if a rewrite-rule is applicable to a given formula;
692 in case of rule-sets (recursivley) collect all _atomic_ rewrites .*)
693 fun try_rew thy ((_, ro):rew_ord) erls (subst:subst) f (thm' as Thm(id, thm)) =
695 then case rewrite_inst_ thy ro erls false subst thm f of
696 SOME (f',_) =>[rule2tac subst thm']
698 else (case rewrite_ thy ro erls false thm f of
699 SOME (f',_) => [rule2tac [] thm']
701 | try_rew thy _ _ _ f (cal as Calc c) =
702 (case get_calculation_ thy c f of
703 SOME (str, _) => [rule2tac [] cal]
705 | try_rew thy _ _ _ f (cal as Cal1 c) =
706 (case get_calculation_ thy c f of
707 SOME (str, _) => [rule2tac [] cal]
709 | try_rew thy _ _ subst f (Rls_ rls) = filter_appl_rews thy subst f rls
710 and filter_appl_rews thy subst f (Rls {rew_ord = ro, erls, rules,...}) =
711 distinct (flat (map (try_rew thy ro erls subst f) rules))
712 | filter_appl_rews thy subst f (Seq {rew_ord = ro, erls, rules,...}) =
713 distinct (flat (map (try_rew thy ro erls subst f) rules))
714 | filter_appl_rews thy subst f (Rrls _) = [];
716 (*. decide if a tactic is applicable to a given formula;
717 in case of Rewrite_Set* go down to _atomic_ rewrite-tactics .*)
720 fun atomic_appl_tacs thy _ _ f (Calculate scrID) =
721 try_rew thy e_rew_ordX e_rls [] f (Calc (snd(assoc1 (!calclist', scrID))))
722 | atomic_appl_tacs thy ro erls f (Rewrite (thm' as (thmID, _))) =
723 try_rew thy (ro, assoc_rew_ord ro) erls [] f
724 (Thm (thmID, assoc_thm' thy thm'))
725 | atomic_appl_tacs thy ro erls f (Rewrite_Inst (subs, thm' as (thmID, _))) =
726 try_rew thy (ro, assoc_rew_ord ro) erls (subs2subst thy subs) f
727 (Thm (thmID, assoc_thm' thy thm'))
729 | atomic_appl_tacs thy _ _ f (Rewrite_Set rls') =
730 filter_appl_rews thy [] f (assoc_rls rls')
731 | atomic_appl_tacs thy _ _ f (Rewrite_Set_Inst (subs, rls')) =
732 filter_appl_rews thy (subs2subst thy subs) f (assoc_rls rls')
733 | atomic_appl_tacs _ _ _ _ tac =
734 (tracing ("### atomic_appl_tacs: not impl. for tac = '"^ tac2str tac ^"'");
741 (*.not only for thydata, but also for thy's etc.*)
742 fun theID2guh (theID:theID) =
744 0 => error ("theID2guh: called with theID = "^strs2str' theID)
745 | 1 => part2guh theID
747 | 3 => thypart2guh theID
748 | 4 => let val [isa, thyID, typ, elemID] = theID
750 "Theorems" => thm2guh (isa, thyID) elemID
751 | "Rulesets" => rls2guh (isa, thyID) elemID
752 | "Calculations" => cal2guh (isa, thyID) elemID
753 | "Orders" => ord2guh (isa, thyID) elemID
754 | "Theorems" => thy2guh [isa, thyID]
755 | str => error ("theID2guh: called with theID = "^
758 | n => error ("theID2guh called with theID = "^strs2str' theID);
759 (*.filenames not only for thydata, but also for thy's etc.*)
760 fun theID2filename (theID:theID) = theID2guh theID ^ ".xml" : filename;
762 fun guh2theID (guh:guh) =
763 let val guh' = explode guh
764 val part = implode (take_fromto 1 4 guh')
765 val isa = implode (take_fromto 5 9 guh')
766 in if not (member op = ["exp_", "thy_", "pbl_", "met_"] part)
767 then error ("guh '"^guh^"' does not begin with \
768 \exp_ | thy_ | pbl_ | met_")
769 else let val chap = case isa of
770 "isab_" => "Isabelle"
771 | "scri_" => "IsacScripts"
772 | "isac_" => "IsacKnowledge"
774 error ("guh2theID: '"^guh^
775 "' does not have isab_ | scri_ | \
776 \isac_ at position 5..9")
777 val rest = takerest (9, guh')
778 val thyID = takewhile [] (not o (curry op= "-")) rest
779 val rest' = dropuntil (curry op= "-") rest
780 in case implode rest' of
781 "-part" => [chap] : theID
782 | "" => [chap, implode thyID]
783 | "-Theorems" => [chap, implode thyID, "Theorems"]
784 | "-Rulesets" => [chap, implode thyID, "Rulesets"]
785 | "-Operations" => [chap, implode thyID, "Operations"]
786 | "-Orders" => [chap, implode thyID, "Orders"]
788 let val sect = implode (take_fromto 1 5 rest')
791 "-thm-" => "Theorems"
792 | "-rls-" => "Rulesets"
793 | "-cal-" => "Operations"
794 | "-ord-" => "Orders"
796 error ("guh2theID: '"^guh^"' has '"^sect^
797 "' instead -thm- | -rls- | \
799 in [chap, implode thyID, sect', implode
800 (takerest (5, rest'))]
804 (*> guh2theID "thy_isac_Biegelinie-Theorems";
805 val it = ["IsacKnowledge", "Biegelinie", "Theorems"] : theID
806 > guh2theID "thy_scri_ListC-thm-zip_Nil";
807 val it = ["IsacScripts", "ListC", "Theorems", "zip_Nil"] : theID*)
809 fun guh2filename (guh : guh) = guh ^ ".xml" : filename;
813 fun guh2rewtac (guh:guh) ([] : subs) =
814 let val [isa, thy, sect, xstr] = guh2theID guh
816 "Theorems" => Rewrite (xstr, "")
817 | "Rulesets" => Rewrite_Set xstr
818 | str => error ("guh2rewtac: not impl. for '"^xstr^"'")
820 | guh2rewtac (guh:guh) subs =
821 let val [isa, thy, sect, xstr] = guh2theID guh
823 "Theorems" => Rewrite_Inst (subs, (xstr, ""))
824 | "Rulesets" => Rewrite_Set_Inst (subs, xstr)
825 | str => error ("guh2rewtac: not impl. for '"^xstr^"'")
827 (*> guh2rewtac "thy_isac_Test-thm-constant_mult_square" [];
828 val it = Rewrite ("constant_mult_square", "") : tac
829 > guh2rewtac "thy_isac_Test-thm-risolate_bdv_add" ["(bdv, x)"];
830 val it = Rewrite_Inst (["(bdv, x)"], ("risolate_bdv_add", "")) : tac
831 > guh2rewtac "thy_isac_Test-rls-Test_simplify" [];
832 val it = Rewrite_Set "Test_simplify" : tac
833 > guh2rewtac "thy_isac_Test-rls-isolate_bdv" ["(bdv, x)"];
834 val it = Rewrite_Set_Inst (["(bdv, x)"], "isolate_bdv") : tac*)
837 (*.the front-end may request a context for any element of the hierarchy.*)
838 (* val guh = "thy_isac_Test-rls-Test_simplify";
840 fun no_thycontext (guh : guh) = (guh2theID guh; false)
843 (*> has_thycontext "thy_isac_Test";
844 if has_thycontext "thy_isac_Test" then "OK" else "NOTOK";
849 (*.get the substitution of bound variables for matchTheory:
850 # lookup the thm|rls' in the script
851 # take the [(bdv, v_),..] from the respective Rewrite_(Set_)Inst
852 # instantiate this subs with the istates env to [(bdv, x),..]
854 (*WN060617 hack assuming that all scripts use only one bound variable
855 and use 'v_' as the formal argument for this bound variable*)
856 (* val (ScrState (env,_,_,_,_,_), _, guh) = (is, "dummy", guh);
858 fun subs_from (ScrState (env,_,_,_,_,_)) _(*:Script sc*) (guh:guh) =
859 let val theID as [isa, thyID, sect, xstr] = guh2theID guh
862 let val thm = PureThy.get_thm (assoc_thy (thyID2theory' thyID)) xstr
863 in if contains_bdv thm
864 then let val formal_arg = str2term "v_"
865 val value = subst_atomic env formal_arg
866 in ["(bdv," ^ term2str value ^ ")"]:subs end
870 let val rules = (get_rules o assoc_rls) xstr
871 in if contain_bdv rules
872 then let val formal_arg = str2term"v_"
873 val value = subst_atomic env formal_arg
874 in ["(bdv,"^term2str value^")"]:subs end
879 (* use"ME/rewtools.sml";