1 (* tools for rewriting, reverse rewriting, context to thy concerning rewriting
2 authors: Walther Neuper 2002, 2006
3 (c) due to copyright terms
6 signature REWRITE_TOOLS =
9 val contains_rule : rule -> rls -> bool
10 val atomic_appl_tacs : theory -> string -> rls -> term -> Ctree.tac -> Ctree.tac list
11 val thy_containing_rls : theory' -> rls' -> string * theory'
12 val thy_containing_cal : theory' -> prog_calcID -> string * string
14 = ContNOrew of {applto: term, thm_rls: guh, thyID: thyID}
15 | ContNOrewInst of {applto: term, bdvs: subst, thm_rls: guh, thminst: term, thyID: thyID}
16 | ContRls of {applto: term, asms: term list, result: term, rls: guh, thyID: thyID}
17 | ContRlsInst of {applto: term, asms: term list, bdvs: subst, result: term, rls: guh, thyID: thyID}
18 | ContThm of {applat: term, applto: term, asmrls: rls', asms: (term * term) list,
19 lhs: term * term, resasms: term list, result: term, reword: rew_ord', rhs: term * term,
20 thm: guh, thyID: thyID}
21 | ContThmInst of {applat: term, applto: term, asmrls: rls', asms: (term * term) list,
22 bdvs: subst, lhs: term * term, resasms: term list, result: term, reword: rew_ord',
23 rhs: term * term, thm: guh, thminst: term, thyID: thyID}
25 val guh2filename : guh -> filename
26 val is_sym : thmID -> bool
27 val sym_drop : thmID -> thmID val sym_rls : rls -> rls
28 val sym_rule : rule -> rule
29 val thms_of_rls : rls -> rule list
30 val theID2filename : theID -> filename
31 val no_thycontext : guh -> bool
32 val subs_from : Ctree.istate -> 'a -> guh -> Ctree.subs
33 val guh2rewtac : guh -> Ctree.subs -> Ctree.tac
34 val get_tac_checked : Ctree.ctree -> Ctree.pos' -> Ctree.tac
35 val context_thy : Ctree.ctree * Ctree.pos' -> Ctree.tac -> contthy
36 val distinct_Thm : rule list -> rule list
37 val eq_Thms : string list -> rule -> bool
38 val make_deriv : theory -> rls -> rule list -> ((term * term) list -> term * term -> bool) ->
39 term option -> term -> deriv
40 val reverse_deriv : theory -> rls -> rule list -> ((term * term) list -> term * term -> bool) ->
41 term option -> term -> (rule * (term * term list)) list
42 val get_bdv_subst : term -> (term * term) list -> Ctree.subs option * subst
43 val thy_containing_thm : string -> string * string val thypart2filename : theID -> filename
44 val guh2theID : guh -> theID
45 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
46 val trtas2str : (term * rule * (term * term list)) list -> string
47 val eq_Thm : rule * rule -> bool
48 val deriv2str : (term * rule * (term * term list)) list -> string val deriv_of_thm'' : thm'' -> string
49 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
53 structure Rtools(**): REWRITE_TOOLS(**) =
56 (*** reverse rewriting ***)
57 (*. a '_deriv'ation is constructed during 'reverse rewring' by an Rrls *
58 * of for connecting a user-input formula with the current calc-state. *
59 *# It is somewhat incompatible with the rest of the math-engine: *
60 * (1) it is not created by a script *
61 * (2) thus there cannot be another user-input within a derivation *
62 *# It suffers particularily from the not-well-foundedness of the math-engine*
63 * (1) FIXME other branchtyptes than Transitive will change 'embed_deriv' *
64 * (2) FIXME and eventually 'compare_step' (ie. the script interpreter) *
65 * (3) FIXME and eventually 'lev_back' *
66 *# SOME improvements are evident FIXME.040215 '_deriv'ation: *
67 * (1) FIXME nest Rls_ in 'make_deriv' *
68 * (2) FIXME do the not-reversed part in 'make_deriv' by scripts -- thus *
69 * user-input will become possible in this part of a derivation *
70 * (3) FIXME do (2) only if a derivation has been found -- for efficiency, *
71 * while a non-derivable inform requires to step until End_Proof' *
72 * (4) FIXME find criteria on when _not_ to step until End_Proof' *
75 type deriv = (* derivation for insertin one level of nodes into the calctree *)
76 ( term * (* where the rule is applied to *)
77 rule * (* rule to be applied *)
78 ( term * (* resulting from rule application *)
79 term list)) (* assumptions resulting from rule application *)
82 fun trta2str (t, r, (t', a)) =
83 "\n(" ^ term2str t ^ ", " ^ rule2str' r ^ ", (" ^ term2str t' ^ ", " ^ terms2str a ^ "))"
84 fun trtas2str trtas = (strs2str o (map trta2str)) trtas
85 val deriv2str = trtas2str
86 fun rta2str (r, (t, a)) =
87 "\n(" ^ rule2str' r ^ ", (" ^ term2str t ^ ", " ^ terms2str a ^ "))"
88 fun rtas2str rtas = (strs2str o (map rta2str)) rtas
89 val deri2str = rtas2str
91 (* A1==>...==> An ==> (Lhs = Rhs) goes to A1 ==>...==> An ==> (Rhs = Lhs)
92 WN120320: reconsider the desing including the java front-end with html representation;
94 --- OLD compute rlsthmsNOTisac by eq_thmID ---
95 --- compute val rlsthmsNOTisac ---
100 {thy = thy, tags = tags, maxidx = maxidx, shyps = shyps, hyps = hyps, tpairs = tpairs,
101 prop = prop}) = Thm.rep_thm_G thm
102 val (lhs, rhs) = (dest_equals' o strip_trueprop o Logic.strip_imp_concl) prop
103 val prop' = case strip_imp_prems' prop of
104 NONE => Trueprop $ (mk_equality (rhs, lhs))
105 | SOME cs => ins_concl cs (Trueprop $ (mk_equality (rhs, lhs)))
106 in Thm.assbl_thm deriv thy tags maxidx shyps hyps tpairs prop' end
108 (* WN100910 weaker than fun sym_thm for Theory.axioms_of in isa02 *)
111 val (lhs, rhs) = (dest_equals' o strip_trueprop o Logic.strip_imp_concl) trm
112 val trm' = case strip_imp_prems' trm of
113 NONE => mk_equality (rhs, lhs)
114 | SOME cs => ins_concl cs (mk_equality (rhs, lhs))
117 (* derive normalform of a rls, or derive until SOME goal,
118 and record rules applied and rewrites.
123 -> rew_ord : the order of this rls, which 1 theorem of is used
124 for rewriting 1 single step (?14.4.03)
125 -> term option : 040214 ??? use for "derive until SOME goal" ???
127 -> (term * : to this term ...
128 rule * : ... this rule is applied yielding ...
129 (term * : ... this term ...
130 term list)) : ... under these assumptions.
132 returns empty list for a normal form
133 FIXME.WN040214: treats rules as in Rls, _not_ as in Seq
135 WN060825 too complicated for the intended use by cancel_, common_nominator_
136 and unreflectedly adapted to extension of rules by Rls_: returns Rls_("sym_simpl..
138 fun make_deriv thy erls (rs:rule list) ro goal tt =
140 datatype switch = Appl | Noap (* unify with version in rewrite.sml *)
141 fun rew_once _ rts t Noap [] =
142 (case goal of NONE => rts | SOME _ => error ("make_deriv: no derivation for " ^ term2str t))
143 | rew_once lim rts t Appl [] = rew_once lim rts t Noap rs
144 (*| Seq _ => rts) FIXXXXXME 14.3.03*)
145 | rew_once lim rts t apno rs' =
147 NONE => rew_or_calc lim rts t apno rs'
148 | SOME g => if g = t then rts else rew_or_calc lim rts t apno rs')
149 and rew_or_calc lim rts t apno (rrs' as (r :: rs')) =
151 then (tracing ("make_deriv exceeds " ^ int2str (! lim_deriv) ^ "with deriv =\n");
152 tracing (deriv2str rts); rts)
156 (if not (! trace_rewrite) then () else tracing ("### trying thm \"" ^ thmid ^ "\"");
157 case rewrite_ thy ro erls true tm t of
158 NONE => rew_once lim rts t apno rs'
160 (if ! trace_rewrite then tracing ("### rewrites to: " ^ term2str t') else ();
161 rew_once (lim - 1) (rts @ [(t, r, (t', a'))]) t' Appl rrs'))
162 | Calc (c as (op_, _)) =>
164 val _ = if not (! trace_rewrite) then () else tracing ("### trying calc. \"" ^ op_^"\"")
165 val t = uminus_to_string t
167 case adhoc_thm thy c t of
168 NONE => rew_once lim rts t apno rs'
169 | SOME (thmid, tm) =>
171 val (t', a') = case rewrite_ thy ro erls true tm t of
173 | NONE => error "adhoc_thm: NONE"
174 val _ = if not (! trace_rewrite) then () else tracing("### calc. to: " ^term2str t')
175 val r' = Thm (thmid, tm)
176 in rew_once (lim - 1) (rts @ [(t, r', (t', a'))]) t' Appl rrs' end)
177 handle _ => error "derive_norm, Calc: no rewrite"
179 (*| Cal1 (cc as (op_,_)) => ... WN080222 see rewrite__set_: see 7df94616c1bd and earlier*)
180 | Rls_ rls => (* WN060829: CREATES "sym_rlsID", see 7df94616c1bd and earlier*)
181 (case rewrite_set_ thy true rls t of
182 NONE => rew_once lim rts t apno rs'
183 | SOME (t', a') => rew_once (lim - 1) (rts @ [(t, r, (t', a'))]) t' Appl rrs')
184 | rule => error ("rew_once: uncovered case " ^ rule2str rule))
185 | rew_or_calc _ _ _ _ [] = error "rew_or_calc: called with []"
186 in rew_once (! lim_deriv) [] tt Noap rs : deriv end
188 fun sym_drop (thmID : thmID) =
189 case Symbol.explode thmID of
190 "s" :: "y" :: "m" :: "_" :: id => implode id : thmID
192 fun is_sym (thmID : thmID) =
193 case Symbol.explode thmID of
194 "s" :: "y" :: "m" :: "_" :: _ => true
197 (*FIXXXXME.040219: detail has to handle Rls id="sym_..."
198 by applying make_deriv, rev_deriv'; see concat_deriv*)
199 fun sym_rls Erls = Erls
200 | sym_rls (Rls {id, scr, calc, errpatts, erls, srls, rules, rew_ord, preconds}) =
201 Rls {id = "sym_" ^ id, scr = scr, calc = calc, errpatts = errpatts, erls = erls, srls = srls,
202 rules = rules, rew_ord = rew_ord, preconds = preconds}
203 | sym_rls (Seq {id, scr, calc, errpatts, erls, srls, rules, rew_ord, preconds}) =
204 Seq {id = "sym_" ^ id, scr = scr, calc = calc, errpatts = errpatts, erls = erls, srls = srls,
205 rules = rules, rew_ord = rew_ord, preconds = preconds}
206 | sym_rls (Rrls {id, scr, calc, errpatts, erls, prepat, rew_ord}) =
207 Rrls {id = "sym_" ^ id, scr = scr, calc = calc, errpatts = errpatts, erls = erls,
208 prepat = prepat, rew_ord = rew_ord}
210 (* toggles sym_* and keeps "#:" for ad-hoc calculations *)
211 fun sym_rule (Thm (thmID, thm)) =
213 val thm' = sym_thm thm
214 val thmID' = case Symbol.explode thmID of
215 "s" :: "y" :: "m" :: "_" :: id => implode id
216 | "#" :: ":" :: _ => "#: " ^ string_of_thmI thm'
217 | _ => "sym_" ^ thmID
218 in Thm (thmID', thm') end
219 | sym_rule (Rls_ rls) = Rls_ (sym_rls rls) (* TODO? handle with interSteps ? *)
220 | sym_rule r = error ("sym_rule: not for " ^ rule2str r)
222 (*version for reverse rewrite used before 040214*)
223 fun rev_deriv (t, r, (_, a)) = (sym_rule r, (t, a));
224 fun reverse_deriv thy erls (rs:rule list) ro goal t =
225 (rev o (map rev_deriv)) (make_deriv thy erls (rs:rule list) ro goal t)
227 fun eq_Thm (Thm (id1, _), Thm (id2,_)) = id1 = id2
228 | eq_Thm (Thm (_, _), _) = false
229 | eq_Thm (Rls_ r1, Rls_ r2) = id_rls r1 = id_rls r2
230 | eq_Thm (Rls_ _, _) = false
231 | eq_Thm (r1, r2) = error ("eq_Thm: called with '" ^ rule2str r1 ^ "' '"^ rule2str r2 ^ "'")
232 fun distinct_Thm r = gen_distinct eq_Thm r
234 fun eq_Thms thmIDs thm = (member op = thmIDs (id_of_thm thm))
235 handle ERROR _ => false
238 (*** context to thy concerning rewriting ***)
240 (* create the unique handles and filenames for the theory-data *)
241 fun part2filename str = part2guh str ^ ".xml" : filename
242 fun thy2filename thy' = thy2guh thy' ^ ".xml" : filename
243 fun thypart2filename thy' = thypart2guh thy' ^ ".xml" : filename
245 fun thm2filename (isa_thyID: string * thyID) thmID = thm2guh isa_thyID thmID ^ ".xml" : filename
246 fun rls2filename (isa, thyID) rls' = rls2guh (isa, thyID) rls' ^ ".xml" : filename
247 fun cal2filename (isa, thyID:thyID) calID = cal2guh (isa, thyID : thyID) calID ^ ".xml" : filename
248 fun ord2filename (isa, thyID:thyID) (rew_ord' : rew_ord') =
249 ord2guh (isa, thyID:thyID) (rew_ord' : rew_ord') ^ ".xml" : filename
251 fun rearrange (thyID : thyID, (thmID : thmID, thm)) = (thmID, (thyID, Thm.prop_of thm));
252 fun rearrange' (thmID : thmID, thm) =
253 (thmID_of_derivation_name thmID,
254 (thyID_of_derivation_name thmID, Thm.prop_of thm)) : (thmID * (thyID * term))
255 fun rearrange_inv (thmID, (thyID, term)) = (thyID, (thmID, term))
257 (* cheap version without sym_* thms *)
258 fun make_isab rlsthmsNOTisac = map rearrange' rlsthmsNOTisac;
260 fun thy_containing_thm thmDeriv =
262 val isabthys' = map Context.theory_name (isabthys ());
264 if member op= isabthys' (thyID_of_derivation_name thmDeriv)
265 then ("Isabelle", thyID_of_derivation_name thmDeriv)
266 else ("IsacKnowledge", thyID_of_derivation_name thmDeriv)
269 (* which theory in ancestors of thy' contains a ruleset *)
270 fun thy_containing_rls (thy' : theory') (rls' : rls') =
272 val thy = Thy_Info.get_theory thy'
274 case AList.lookup op= (KEStore_Elems.get_rlss thy) rls' of
275 SOME (thy'', _) => (partID' thy'', thy'')
276 | _ => error ("thy_containing_rls : rls '" ^ rls' ^ "' not in ancestors of thy '" ^ thy' ^ "'")
279 (* this function cannot work as long as the datastructure does not contain thy' *)
280 fun thy_containing_cal (thy' : theory') (sop : prog_calcID) =
282 val thy = Thy_Info.get_theory thy'
284 case AList.lookup op= (KEStore_Elems.get_calcs thy) sop of
285 SOME (_(*"Groups.plus_class.plus"*), _) => ("IsacKnowledge", "Atools" (*FIXME*))
286 | _ => error ("thy_containing_cal : rls '" ^ sop ^ "' not in ancestors of thy '" ^ thy' ^ "'")
289 (* packing return-values to matchTheory, contextToThy for xml-generation *)
290 datatype contthy = (*also an item from KEStore on Browser .....#*)
291 EContThy (* not from KEStore ..............................*)
292 | ContThm of (* a theorem in contex ===========================*)
293 {thyID : thyID, (* for *2guh in sub-elems here .*)
294 thm : guh, (* theorem in the context .*)
295 applto : term, (* applied to formula ... .*)
296 applat : term, (* ... with lhs inserted .*)
297 reword : rew_ord', (* order used for rewrite .*)
298 asms : (term (* asumption instantiated .*)
299 * term) list, (* asumption evaluated .*)
300 lhs : term (* lhs of the theorem ... #*)
301 * term, (* ... instantiated .*)
302 rhs : term (* rhs of the theorem ... #*)
303 * term, (* ... instantiated .*)
304 result : term, (* resulting from the rewrite .*)
305 resasms : term list, (* ... with asms stored .*)
306 asmrls : rls' (* ruleset for evaluating asms .*)
308 | ContThmInst of (* a theorem with bdvs in contex ============ *)
309 {thyID : thyID, (*for *2guh in sub-elems here .*)
310 thm : guh, (*theorem in the context .*)
311 bdvs : subst, (*bound variables to modify... .*)
312 thminst : term, (*... theorem instantiated .*)
313 applto : term, (*applied to formula ... .*)
314 applat : term, (*... with lhs inserted .*)
315 reword : rew_ord', (*order used for rewrite .*)
316 asms : (term (*asumption instantiated .*)
317 * term) list, (*asumption evaluated .*)
318 lhs : term (*lhs of the theorem ... #*)
319 * term, (*... instantiated .*)
320 rhs : term (*rhs of the theorem ... #*)
321 * term, (*... instantiated .*)
322 result : term, (*resulting from the rewrite .*)
323 resasms : term list, (*... with asms stored .*)
324 asmrls : rls' (*ruleset for evaluating asms .*)
326 | ContRls of (* a rule set in contex ========================= *)
327 {thyID : thyID, (*for *2guh in sub-elems here .*)
328 rls : guh, (*rule set in the context .*)
329 applto : term, (*rewrite this formula .*)
330 result : term, (*resulting from the rewrite .*)
331 asms : term list (*... with asms stored .*)
333 | ContRlsInst of (* a rule set with bdvs in contex =========== *)
334 {thyID : thyID, (*for *2guh in sub-elems here .*)
335 rls : guh, (*rule set in the context .*)
336 bdvs : subst, (*for bound variables in thms .*)
337 applto : term, (*rewrite this formula .*)
338 result : term, (*resulting from the rewrite .*)
339 asms : term list (*... with asms stored .*)
341 | ContNOrew of (* no rewrite for thm or rls ================== *)
342 {thyID : thyID, (*for *2guh in sub-elems here .*)
343 thm_rls : guh, (*thm or rls in the context .*)
344 applto : term (*rewrite this formula .*)
346 | ContNOrewInst of (* no rewrite for some instantiation ====== *)
347 {thyID : thyID, (*for *2guh in sub-elems here .*)
348 thm_rls : guh, (*thm or rls in the context .*)
349 bdvs : subst, (*for bound variables in thms .*)
350 thminst : term, (*... theorem instantiated .*)
351 applto : term (*rewrite this formula .*)
354 (*.check a rewrite-tac for bdv (RL always used *_Inst !) TODO.WN060718
355 pass other tacs unchanged.*)
356 fun get_tac_checked pt ((p, _) : Ctree.pos') = Ctree.get_obj Ctree.g_tac pt p;
358 (* create a derivation-name, eg. ("refl", _) --> "HOL.refl"*)
359 fun deriv_of_thm'' ((thmID, _) : thm'') =
360 thmID |> Global_Theory.get_thm (Isac ()) |> Thm.get_name_hint
362 (* get the formula f at ptp rewritten by the Rewrite_* already applied to f *)
363 fun context_thy (pt, pos as (p,p_)) (tac as Ctree.Rewrite thm'') =
364 let val thm_deriv = deriv_of_thm'' thm''
366 (case Applicable.applicable_in pos pt tac of
367 Chead.Appl (Ctree.Rewrite' (thy', ord', erls, _, _, f, (res,asm))) =>
369 {thyID = theory'2thyID thy',
370 thm = thm2guh (thy_containing_thm thm_deriv) (thmID_of_derivation_name thm_deriv),
371 applto = f, applat = e_term, reword = ord',
372 asms = [](*asms ~~ asms'*), lhs = (e_term, e_term)(*(lhs, lhs')*), rhs = (e_term, e_term)(*(rhs, rhs')*),
373 result = res, resasms = asm, asmrls = id_rls erls}
376 val pp = Ctree.par_pblobj pt p
377 val thy' = Ctree.get_obj Ctree.g_domID pt pp
379 Frm => Ctree.get_obj Ctree.g_form pt p
380 | Res => (fst o (Ctree.get_obj Ctree.g_result pt)) p | _ => error "context_thy: uncovered position"
383 {thyID = theory'2thyID thy',
385 thm2guh (thy_containing_thm thm_deriv) (thmID_of_derivation_name thm_deriv),
388 | _ => error "context_thy..Rewrite: uncovered case 2")
390 | context_thy (pt, pos as (p, p_)) (tac as Ctree.Rewrite_Inst (subs, (thmID, _))) =
391 let val thm = Global_Theory.get_thm (Isac ()) thmID
393 (case Applicable.applicable_in pos pt tac of
394 Chead.Appl (Ctree.Rewrite_Inst' (thy', ord', erls, _, subst, _, f, (res, asm))) =>
396 val thm_deriv = Thm.get_name_hint thm
397 val thminst = inst_bdv subst ((norm o #prop o Thm.rep_thm) thm)
400 {thyID = theory'2thyID thy',
402 thm2guh (thy_containing_thm thm_deriv) (thmID_of_derivation_name thm_deriv),
403 bdvs = subst, thminst = thminst, applto = f, applat = e_term, reword = ord',
404 asms = [](*asms ~~ asms'*), lhs = (e_term, e_term)(*(lhs, lhs')*), rhs = (e_term, e_term)(*(rhs, rhs')*),
405 result = res, resasms = asm, asmrls = id_rls erls}
409 val thm = Global_Theory.get_thm (Isac ()(*WN141021 assoc_thy thy' ERROR*)) thmID
410 val thm_deriv = Thm.get_name_hint thm
411 val pp = Ctree.par_pblobj pt p
412 val thy' = Ctree.get_obj Ctree.g_domID pt pp
413 val subst = Ctree.subs2subst (assoc_thy thy') subs
414 val thminst = inst_bdv subst ((norm o #prop o Thm.rep_thm) thm)
416 Frm => Ctree.get_obj Ctree.g_form pt p
417 | Res => (fst o (Ctree.get_obj Ctree.g_result pt)) p | _ => error "context_thy: uncovered case 3"
420 {thyID = theory'2thyID thy',
421 thm_rls = thm2guh (thy_containing_thm thm_deriv) (thmID_of_derivation_name thm_deriv),
422 bdvs = subst, thminst = thminst, applto = f}
424 | _ => error "context_thy..Rewrite_Inst: uncovered case 4")
426 | context_thy (pt, p) (tac as Ctree.Rewrite_Set rls') =
427 (case Applicable.applicable_in p pt tac of
428 Chead.Appl (Ctree.Rewrite_Set' (thy', _, _(*rls*), f, (res,asm))) =>
430 {thyID = theory'2thyID thy',
431 rls = rls2guh (thy_containing_rls thy' rls') rls',
432 applto = f, result = res, asms = asm}
433 | _ => error ("context_thy Rewrite_Set: not for Chead.Notappl"))
434 | context_thy (pt,p) (tac as Ctree.Rewrite_Set_Inst (_(*subs*), rls')) =
435 (case Applicable.applicable_in p pt tac of
436 Chead.Appl (Ctree.Rewrite_Set_Inst' (thy', _, subst, _, f, (res,asm))) =>
438 {thyID = theory'2thyID thy',
439 rls = rls2guh (thy_containing_rls thy' rls') rls',
440 bdvs = subst, applto = f, result = res, asms = asm}
441 | _ => error ("context_thy Rewrite_Set_Inst: not for Chead.Notappl"))
442 | context_thy (_, p) tac =
443 error ("context_thy: not for tac " ^ Ctree.tac2str tac ^ " at " ^ Ctree.pos'2str p)
445 (* get all theorems in a rule set (recursivley containing rule sets) *)
446 fun thm_of_rule Erule = []
447 | thm_of_rule (thm as Thm _) = [thm]
448 | thm_of_rule (Calc _) = []
449 | thm_of_rule (Cal1 _) = []
450 | thm_of_rule (Rls_ rls) = thms_of_rls rls
451 and thms_of_rls Erls = []
452 | thms_of_rls (Rls {rules,...}) = (flat o (map thm_of_rule)) rules
453 | thms_of_rls (Seq {rules,...}) = (flat o (map thm_of_rule)) rules
454 | thms_of_rls (Rrls _) = []
456 (* check if a rule is contained in a rule-set (recursivley down in Rls_);
457 this rule can even be a rule-set itself *)
458 fun contains_rule r rls =
460 fun (*find (_, Rls_ rls) = finds (get_rules rls)
461 | find r12 = eq_rule r12
462 and*) finds [] = false
463 | finds (r1 :: rs) = if eq_rule (r, r1) then true else finds rs
465 finds (get_rules rls)
468 (* try if a rewrite-rule is applicable to a given formula;
469 in case of rule-sets (recursivley) collect all _atomic_ rewrites *)
470 fun try_rew thy ((_, ro) : rew_ord) erls (subst : subst) f (thm' as Thm (_, thm)) =
472 then case rewrite_inst_ thy ro erls false subst thm f of
473 SOME _ => [Ctree.rule2tac thy subst thm']
475 else (case rewrite_ thy ro erls false thm f of
476 SOME _ => [Ctree.rule2tac thy [] thm']
478 | try_rew thy _ _ _ f (cal as Calc c) =
479 (case adhoc_thm thy c f of
480 SOME _ => [Ctree.rule2tac thy [] cal]
482 | try_rew thy _ _ _ f (cal as Cal1 c) =
483 (case adhoc_thm thy c f of
484 SOME _ => [Ctree.rule2tac thy [] cal]
486 | try_rew thy _ _ subst f (Rls_ rls) = filter_appl_rews thy subst f rls
487 | try_rew _ _ _ _ _ _ = error "try_rew: uncovered case"
488 and filter_appl_rews thy subst f (Rls {rew_ord = ro, erls, rules, ...}) =
489 gen_distinct Ctree.eq_tac (flat (map (try_rew thy ro erls subst f) rules))
490 | filter_appl_rews thy subst f (Seq {rew_ord = ro, erls, rules,...}) =
491 gen_distinct Ctree.eq_tac (flat (map (try_rew thy ro erls subst f) rules))
492 | filter_appl_rews _ _ _ (Rrls _) = []
493 | filter_appl_rews _ _ _ _ = error "filter_appl_rews: uncovered case"
495 (* decide if a tactic is applicable to a given formula;
496 in case of Rewrite_Set* go down to _atomic_ rewrite-tactics *)
497 fun atomic_appl_tacs thy _ _ f (Ctree.Calculate scrID) =
498 try_rew thy e_rew_ordX e_rls [] f (Calc (assoc_calc' thy scrID |> snd))
499 | atomic_appl_tacs thy ro erls f (Ctree.Rewrite thm'') =
500 try_rew thy (ro, assoc_rew_ord ro) erls [] f (Thm thm'')
501 | atomic_appl_tacs thy ro erls f (Ctree.Rewrite_Inst (subs, thm'')) =
502 try_rew thy (ro, assoc_rew_ord ro) erls (Ctree.subs2subst thy subs) f (Thm thm'')
504 | atomic_appl_tacs thy _ _ f (Ctree.Rewrite_Set rls') =
505 filter_appl_rews thy [] f (assoc_rls rls')
506 | atomic_appl_tacs thy _ _ f (Ctree.Rewrite_Set_Inst (subs, rls')) =
507 filter_appl_rews thy (Ctree.subs2subst thy subs) f (assoc_rls rls')
508 | atomic_appl_tacs _ _ _ _ tac =
509 (tracing ("### atomic_appl_tacs: not impl. for tac = '" ^ Ctree.tac2str tac ^ "'"); []);
511 (* filenames not only for thydata, but also for thy's etc *)
512 fun theID2filename (theID : theID) = theID2guh theID ^ ".xml" : filename
514 fun guh2theID (guh : guh) =
516 val guh' = Symbol.explode guh
517 val part = implode (take_fromto 1 4 guh')
518 val isa = implode (take_fromto 5 9 guh')
520 if not (member op = ["exp_", "thy_", "pbl_", "met_"] part)
521 then raise ERROR ("guh '" ^ guh ^ "' does not begin with exp_ | thy_ | pbl_ | met_")
524 val chap = case isa of
525 "isab_" => "Isabelle"
526 | "scri_" => "IsacScripts"
527 | "isac_" => "IsacKnowledge"
529 raise ERROR ("guh2theID: '" ^ guh ^ "' does not have isab_ | scri_ | isac_ at position 5..9")
530 val rest = takerest (9, guh')
531 val thyID = takewhile [] (not o (curry op= "-")) rest
532 val rest' = dropuntil (curry op = "-") rest
533 in case implode rest' of
534 "-part" => [chap] : theID
535 | "" => [chap, implode thyID]
536 | "-Theorems" => [chap, implode thyID, "Theorems"]
537 | "-Rulesets" => [chap, implode thyID, "Rulesets"]
538 | "-Operations" => [chap, implode thyID, "Operations"]
539 | "-Orders" => [chap, implode thyID, "Orders"]
541 let val sect = implode (take_fromto 1 5 rest')
542 val sect' = case sect of
543 "-thm-" => "Theorems"
544 | "-rls-" => "Rulesets"
545 | "-cal-" => "Operations"
546 | "-ord-" => "Orders"
548 raise ERROR ("guh2theID: '" ^ guh ^ "' has '" ^ sect ^ "' instead -thm- | -rls- | -cal- | -ord-")
550 [chap, implode thyID, sect', implode (takerest (5, rest'))]
555 fun guh2filename (guh : guh) = guh ^ ".xml" : filename;
557 fun guh2rewtac (guh : guh) ([] : Ctree.subs) =
559 val (_, thy, sect, xstr) = case guh2theID guh of
560 [isa, thy, sect, xstr] => (isa, thy, sect, xstr)
561 | _ => error "guh2rewtac: uncovered case"
563 "Theorems" => Ctree.Rewrite (xstr, assoc_thm'' (assoc_thy thy) xstr)
564 | "Rulesets" => Ctree.Rewrite_Set xstr
565 | _ => error ("guh2rewtac: not impl. for '"^xstr^"'")
567 | guh2rewtac guh subs =
569 val (_, thy, sect, xstr) = case guh2theID guh of
570 [isa, thy, sect, xstr] => (isa, thy, sect, xstr)
571 | _ => error "guh2rewtac: uncovered case"
574 Ctree.Rewrite_Inst (subs, (xstr, assoc_thm'' (assoc_thy thy) xstr))
575 | "Rulesets" => Ctree.Rewrite_Set_Inst (subs, xstr)
576 | str => error ("guh2rewtac: not impl. for '" ^ str ^ "'")
579 (* the front-end may request a context for any element of the hierarchy *)
580 fun no_thycontext (guh : guh) = (guh2theID guh; false)
581 handle ERROR _ => true;
583 (* get the substitution of bound variables for matchTheory:
584 # lookup the thm|rls' in the script
585 # take the [(bdv, v_),..] from the respective Rewrite_(Set_)Inst
586 # instantiate this subs with the istates env to [(bdv, x),..]
588 WN060617 hack assuming that all scripts use only one bound variable
589 and use 'v_' as the formal argument for this bound variable*)
590 fun subs_from (Ctree.ScrState (env, _, _, _, _, _)) _ (guh : guh) =
592 val (_, _, thyID, sect, xstr) = case guh2theID guh of
593 theID as [isa, thyID, sect, xstr] => (theID, isa, thyID, sect, xstr)
594 | _ => error "subs_from: uncovered case"
598 let val thm = Global_Theory.get_thm (assoc_thy (thyID2theory' thyID)) xstr
603 val formal_arg = str2term "v_"
604 val value = subst_atomic env formal_arg
605 in ["(bdv," ^ term2str value ^ ")"] : Ctree.subs end
610 val rules = (get_rules o assoc_rls) xstr
615 val formal_arg = str2term "v_"
616 val value = subst_atomic env formal_arg
617 in ["(bdv," ^ term2str value ^ ")"] : Ctree.subs end
620 | str => error ("subs_from: uncovered case with " ^ str)
622 | subs_from _ _ (guh : guh) = error ("subs_from: uncovered case with " ^ guh)
624 (* get a substitution for "bdv*" from the current program and environment.
625 returns a substitution: subst for rewriting and another: sube for Rewrite: *)
626 fun get_bdv_subst prog env =
628 fun scan (Const _) = NONE
629 | scan (Free _) = NONE
630 | scan (Var _) = NONE
631 | scan (Bound _) = NONE
632 | scan (t as Const ("List.list.Cons", _) $ (Const ("Product_Type.Pair", _) $ Free _$ _) $ _) =
633 if is_bdv_subst t then SOME t else NONE
634 | scan (Abs (_, _, body)) = scan body
635 | scan (t1 $ t2) = case scan t1 of NONE => scan t2 | SOME subst => SOME subst
638 NONE => (NONE: Ctree.subs option, []: subst)
640 let val subst = tm |> subst_atomic env |> isalist2list |> map isapair2pair
641 (* "[(bdv,v_v)]": term
642 |> "[(bdv,x)]": term |> ["(bdv,x)"]: term list
643 |> [("bdv","x")]: (term * term) list *)
644 in (SOME (Ctree.subst2subs subst), subst) end
645 (*"SOME [(bdv,v_v)]": term --> ["(bdv,v_v)"]: string list*)