|
1 (* tools for rewriting, reverse rewriting, context to thy concerning rewriting |
|
2 authors: Walther Neuper 2002, 2006 |
|
3 (c) due to copyright terms |
|
4 |
|
5 use"ME/rewtools.sml"; |
|
6 use"rewtools.sml"; |
|
7 *) |
|
8 |
|
9 |
|
10 |
|
11 (***.reverse rewriting.***) |
|
12 |
|
13 (*.derivation for insertin one level of nodes into the calctree.*) |
|
14 type deriv = (term * rule * (term *term list)) list; |
|
15 |
|
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; |
|
24 |
|
25 |
|
26 (*.A1==>...==>An==>(Lhs = Rhs) goes to A1==>...==>An==>(Rhs = Lhs).*) |
|
27 fun sym_thm thm = |
|
28 let |
|
29 val (deriv, {thy_ref = thy_ref, tags = tags, maxidx = maxidx, |
|
30 shyps = shyps, hyps = hyps, tpairs = tpairs, |
|
31 prop = prop}) = |
|
32 rep_thm_G thm; |
|
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)) |
|
37 | SOME cs => |
|
38 ins_concl cs (Trueprop $ (mk_equality (rhs, lhs))); |
|
39 in assbl_thm deriv thy_ref tags maxidx shyps hyps tpairs prop' end; |
|
40 (* |
|
41 (sym RS real_mult_div_cancel1) handle e => print_exn e; |
|
42 Exception THM 1 raised: |
|
43 RSN: no unifiers |
|
44 "?s = ?t ==> ?t = ?s" |
|
45 "?k ~= 0 ==> ?k * ?m / (?k * ?n) = ?m / ?n" |
|
46 |
|
47 val thm = real_mult_div_cancel1; |
|
48 val prop = (#prop o rep_thm) thm; |
|
49 atomt prop; |
|
50 val ppp = Logic.strip_imp_concl prop; |
|
51 atomt ppp; |
|
52 ((#prop o rep_thm o sym_thm o sym_thm) thm) = (#prop o rep_thm) thm; |
|
53 val it = true : bool |
|
54 ((sym_thm o sym_thm) thm) = thm; |
|
55 val it = true : bool |
|
56 |
|
57 val thm = real_le_anti_sym; |
|
58 ((sym_thm o sym_thm) thm) = thm; |
|
59 val it = true : bool |
|
60 |
|
61 val thm = real_minus_zero; |
|
62 ((sym_thm o sym_thm) thm) = thm; |
|
63 val it = true : bool |
|
64 *) |
|
65 |
|
66 |
|
67 |
|
68 (*.derive normalform of a rls, or derive until SOME goal, |
|
69 and record rules applied and rewrites. |
|
70 val it = fn |
|
71 : theory |
|
72 -> rls |
|
73 -> rule list |
|
74 -> rew_ord : the order of this rls, which 1 theorem of is used |
|
75 for rewriting 1 single step (?14.4.03) |
|
76 -> term option : 040214 ??? nonsense ??? |
|
77 -> term |
|
78 -> (term * : to this term ... |
|
79 rule * : ... this rule is applied yielding ... |
|
80 (term * : ... this term ... |
|
81 term list)) : ... under these assumptions. |
|
82 list : |
|
83 returns empty list for a normal form |
|
84 FIXME.WN040214: treats rules as in Rls, _not_ as in Seq |
|
85 |
|
86 WN060825 too complicated for the intended use by cancel_, common_nominator_ |
|
87 and unreflectedly adapted to extion of rules by Rls_: returns Rls_("sym_simpl.. |
|
88 -- replaced below*) |
|
89 (* val (thy, erls, rs, ro, goal, tt) = (thy, erls, rs, ro, goal, t); |
|
90 val (thy, erls, rs, ro, goal, tt) = (thy, Atools_erls, rules, ro, NONE, tt); |
|
91 *) |
|
92 fun make_deriv thy erls (rs:rule list) ro(*rew_ord*) goal tt = |
|
93 let datatype switch = Appl | Noap |
|
94 fun rew_once lim rts t Noap [] = |
|
95 (case goal of |
|
96 NONE => rts |
|
97 | SOME g => |
|
98 raise error ("make_deriv: no derivation for "^(term2str t))) |
|
99 | rew_once lim rts t Appl [] = |
|
100 (*(case rs of Rls _ =>*) rew_once lim rts t Noap rs |
|
101 (*| Seq _ => rts) FIXXXXXME 14.3.03*) |
|
102 | rew_once lim rts t apno rs' = |
|
103 (case goal of |
|
104 NONE => rew_or_calc lim rts t apno rs' |
|
105 | SOME g => |
|
106 if g = t then rts |
|
107 else rew_or_calc lim rts t apno rs') |
|
108 and rew_or_calc lim rts t apno (rrs' as (r::rs')) = |
|
109 if lim < 0 |
|
110 then (writeln ("make_deriv exceeds " ^ int2str (!lim_deriv) ^ |
|
111 "with deriv =\n"); writeln (deriv2str rts); rts) |
|
112 else |
|
113 case r of |
|
114 Thm (thmid, tm) => |
|
115 (if not (!trace_rewrite) then () else |
|
116 writeln ("### trying thm '" ^ thmid ^ "'"); |
|
117 case rewrite_ thy ro erls true tm t of |
|
118 NONE => rew_once lim rts t apno rs' |
|
119 | SOME (t',a') => |
|
120 (if ! trace_rewrite |
|
121 then writeln ("### rewrites to: "^(term2str t')) else(); |
|
122 rew_once (lim-1) (rts@[(t,r,(t',a'))]) t' Appl rrs')) |
|
123 | Calc (c as (op_,_)) => |
|
124 let val _ = if not (!trace_rewrite) then () else |
|
125 writeln ("### trying calc. '" ^ op_ ^ "'") |
|
126 val t = uminus_to_string t |
|
127 in case get_calculation_ thy c t of |
|
128 NONE => rew_once lim rts t apno rs' |
|
129 | SOME (thmid, tm) => |
|
130 (let val SOME (t',a') = rewrite_ thy ro erls true tm t |
|
131 val _ = if not (!trace_rewrite) then () else |
|
132 writeln("### calc. to: " ^ (term2str t')) |
|
133 val r' = Thm (thmid, tm) |
|
134 in rew_once (lim-1) (rts@[(t,r',(t',a'))]) t' Appl rrs' |
|
135 end) |
|
136 handle _ => raise error "derive_norm, Calc: no rewrite" |
|
137 end |
|
138 (* TODO.WN080222: see rewrite__set_ |
|
139 @@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@ |
|
140 | Cal1 (cc as (op_,_)) => |
|
141 (let val _= if !trace_rewrite andalso i < ! depth then |
|
142 writeln((idt"#"(i+1))^" try cal1: "^op_^"'") else (); |
|
143 val ct = uminus_to_string ct |
|
144 in case get_calculation_ thy cc ct of |
|
145 NONE => (ct, asm) |
|
146 | SOME (thmid, thm') => |
|
147 let |
|
148 val pairopt = |
|
149 rewrite__ thy (i+1) bdv ((snd o #rew_ord o rep_rls) rls) |
|
150 ((#erls o rep_rls) rls) put_asm thm' ct; |
|
151 val _ = if pairopt <> NONE then () |
|
152 else raise error("rewrite_set_, rewrite_ \""^ |
|
153 (string_of_thmI thm')^"\" "^(term2str ct)^" = NONE") |
|
154 val _ = if ! trace_rewrite andalso i < ! depth |
|
155 then writeln((idt"="(i+1))^" cal1. to: "^ |
|
156 (term2str ((fst o the) pairopt))) |
|
157 else() |
|
158 in the pairopt end |
|
159 end) |
|
160 @@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@*) |
|
161 | Rls_ rls => |
|
162 (case rewrite_set_ thy true rls t of |
|
163 NONE => rew_once lim rts t apno rs' |
|
164 | SOME (t',a') => |
|
165 rew_once (lim-1) (rts @ [(t,r,(t',a'))]) t' Appl rrs'); |
|
166 (*WN060829 | Rls_ rls => |
|
167 (case rewrite_set_ thy true rls t of |
|
168 NONE => rew_once lim rts t apno rs' |
|
169 | SOME (t',a') => |
|
170 if ro [] (t, t') then rew_once lim rts t apno rs' |
|
171 else rew_once (lim-1) (rts@[(t,r,(t',a'))]) t' Appl rrs'); |
|
172 ...lead to deriv = [] with make_polynomial. |
|
173 THERE IS SOMETHING DIFFERENT beetween rewriting with the code above |
|
174 and between rewriting with rewrite_set: with rules from make_polynomial and |
|
175 t = "(a^^^2 + -1*b^^^2) / (a^^^2 + -2*a*b + b^^^2)" the actual code |
|
176 leads to cycling Rls_ order_mult_rls_..Rls_ discard_parentheses_..Rls_ order.. |
|
177 *) |
|
178 in rew_once (!lim_deriv) [] tt Noap rs end; |
|
179 |
|
180 |
|
181 (*.toggles the marker for 'fun sym_thm'.*) |
|
182 fun sym_thmID (thmID : thmID) = |
|
183 case explode thmID of |
|
184 "s"::"y"::"m"::"_"::id => implode id : thmID |
|
185 | id => "sym_"^thmID; |
|
186 (* |
|
187 > val thmID = "sym_real_mult_2"; |
|
188 > sym_thmID thmID; |
|
189 val it = "real_mult_2" : string |
|
190 > val thmID = "real_num_collect"; |
|
191 > sym_thmID thmID; |
|
192 val it = "sym_real_num_collect" : string*) |
|
193 fun sym_drop (thmID : thmID) = |
|
194 case explode thmID of |
|
195 "s"::"y"::"m"::"_"::id => implode id : thmID |
|
196 | id => thmID; |
|
197 fun is_sym (thmID : thmID) = |
|
198 case explode thmID of |
|
199 "s"::"y"::"m"::"_"::id => true |
|
200 | id => false; |
|
201 |
|
202 |
|
203 (*FIXXXXME.040219: detail has to handle Rls id="sym_..." |
|
204 by applying make_deriv, rev_deriv'; see concat_deriv*) |
|
205 fun sym_rls Erls = Erls |
|
206 | sym_rls (Rls {id, scr, calc, erls, srls, rules, rew_ord, preconds}) = |
|
207 Rls {id="sym_"^id, scr=scr, calc=calc, erls=erls, srls=srls, |
|
208 rules=rules, rew_ord=rew_ord, preconds=preconds} |
|
209 | sym_rls (Seq {id, scr, calc, erls, srls, rules, rew_ord, preconds}) = |
|
210 Seq {id="sym_"^id, scr=scr, calc=calc, erls=erls, srls=srls, |
|
211 rules=rules, rew_ord=rew_ord, preconds=preconds} |
|
212 | sym_rls (Rrls {id, scr, calc, erls, prepat, rew_ord}) = |
|
213 Rrls {id="sym_"^id, scr=scr, calc=calc, erls=erls, prepat=prepat, |
|
214 rew_ord=rew_ord}; |
|
215 |
|
216 fun sym_Thm (Thm (thmID, thm)) = Thm (sym_thmID thmID, sym_thm thm) |
|
217 | sym_Thm (Rls_ rls) = Rls_ (*WN060825?!?*) (sym_rls rls) |
|
218 | sym_Thm r = raise error ("sym_Thm: not for "^(rule2str r)); |
|
219 (* |
|
220 val th = Thm ("real_one_collect",num_str real_one_collect); |
|
221 sym_Thm th; |
|
222 val th = |
|
223 Thm ("real_one_collect","?m is_const ==> ?n + ?m * ?n = (1 + ?m) * ?n") |
|
224 : rule |
|
225 ML> val it = |
|
226 Thm ("sym_real_one_collect","?m is_const ==> (1 + ?m) * ?n = ?n + ?m * ?n")*) |
|
227 |
|
228 |
|
229 (*version for reverse rewrite used before 040214*) |
|
230 fun rev_deriv (t, r, (t', a)) = (sym_Thm r, (t, a)); |
|
231 (* val (thy, erls, rs, ro, goal, t) = (thy, eval_rls, rules, ro, NONE, t'); |
|
232 *) |
|
233 fun reverse_deriv thy erls (rs:rule list) ro(*rew_ord*) goal t = |
|
234 (rev o (map rev_deriv)) (make_deriv thy erls (rs:rule list) ro goal t); |
|
235 (* |
|
236 val rev_rew = reverse_deriv thy e_rls ; |
|
237 writeln(rtas2str rev_rew); |
|
238 *) |
|
239 |
|
240 fun eq_Thm (Thm (id1,_), Thm (id2,_)) = id1 = id2 |
|
241 | eq_Thm (Thm (id1,_), _) = false |
|
242 | eq_Thm (Rls_ r1, Rls_ r2) = id_rls r1 = id_rls r2 |
|
243 | eq_Thm (Rls_ r1, _) = false |
|
244 | eq_Thm (r1, r2) = raise error ("eq_Thm: called with '"^ |
|
245 (rule2str r1)^"' '"^(rule2str r2)^"'"); |
|
246 fun distinct_Thm r = gen_distinct eq_Thm r; |
|
247 |
|
248 fun eq_Thms thmIDs thm = (member op = thmIDs (id_of_thm thm)) |
|
249 handle _ => false; |
|
250 |
|
251 |
|
252 (***. context to thy concerning rewriting .***) |
|
253 |
|
254 (*.create the unique handles and filenames for the theory-data.*) |
|
255 fun part2guh ([str]:theID) = |
|
256 (case str of |
|
257 "Isabelle" => "thy_isab_" ^ str ^ "-part" : guh |
|
258 | "IsacScripts" => "thy_scri_" ^ str ^ "-part" |
|
259 | "IsacKnowledge" => "thy_isac_" ^ str ^ "-part" |
|
260 | str => raise error ("thy2guh: called with '"^str^"'")) |
|
261 | part2guh theID = raise error ("part2guh called with theID = " |
|
262 ^ theID2str theID); |
|
263 fun part2filename str = part2guh str ^ ".xml" : filename; |
|
264 |
|
265 |
|
266 fun thy2guh ([part, thyID]:theID) = |
|
267 (case part of |
|
268 "Isabelle" => "thy_isab_" ^ thyID : guh |
|
269 | "IsacScripts" => "thy_scri_" ^ thyID |
|
270 | "IsacKnowledge" => "thy_isac_" ^ thyID |
|
271 | str => raise error ("thy2guh: called with '"^str^"'")) |
|
272 | thy2guh theID = raise error ("thy2guh called with '"^strs2str' theID^"'"); |
|
273 fun thy2filename thy' = thy2guh thy' ^ ".xml" : filename; |
|
274 fun thypart2guh ([part, thyID, thypart]:theID) = |
|
275 case part of |
|
276 "Isabelle" => "thy_isab_" ^ thyID ^ "-" ^ thypart : guh |
|
277 | "IsacScripts" => "thy_scri_" ^ thyID ^ "-" ^ thypart |
|
278 | "IsacKnowledge" => "thy_isac_" ^ thyID ^ "-" ^ thypart |
|
279 | str => raise error ("thypart2guh: called with '"^str^"'"); |
|
280 fun thypart2filename thy' = thypart2guh thy' ^ ".xml" : filename; |
|
281 |
|
282 (*.convert the data got via contextToThy to a globally unique handle |
|
283 there is another way to get the guh out of the 'theID' in the hierarchy.*) |
|
284 fun thm2guh (isa, thyID:thyID) (thmID:thmID) = |
|
285 case isa of |
|
286 "Isabelle" => |
|
287 "thy_isab_" ^ theory'2thyID thyID ^ "-thm-" ^ strip_thy thmID : guh |
|
288 | "IsacKnowledge" => |
|
289 "thy_isac_" ^ theory'2thyID thyID ^ "-thm-" ^ strip_thy thmID |
|
290 | "IsacScripts" => |
|
291 "thy_scri_" ^ theory'2thyID thyID ^ "-thm-" ^ strip_thy thmID |
|
292 | str => raise error ("thm2guh called with isa = '"^isa^ |
|
293 "' for thm = "^thmID^"'"); |
|
294 fun thm2filename (isa_thyID: string * thyID) thmID = |
|
295 (thm2guh isa_thyID thmID) ^ ".xml" : filename; |
|
296 |
|
297 fun rls2guh (isa, thyID:thyID) (rls':rls') = |
|
298 case isa of |
|
299 "Isabelle" => |
|
300 "thy_isab_" ^ theory'2thyID thyID ^ "-rls-" ^ rls' : guh |
|
301 | "IsacKnowledge" => |
|
302 "thy_isac_" ^ theory'2thyID thyID ^ "-rls-" ^ rls' |
|
303 | "IsacScripts" => |
|
304 "thy_scri_" ^ theory'2thyID thyID ^ "-rls-" ^ rls' |
|
305 | str => raise error ("rls2guh called with isa = '"^isa^ |
|
306 "' for rls = '"^rls'^"'"); |
|
307 fun rls2filename (isa, thyID) rls' = |
|
308 rls2guh (isa, thyID) rls' ^ ".xml" : filename; |
|
309 |
|
310 fun cal2guh (isa, thyID:thyID) calID = |
|
311 case isa of |
|
312 "Isabelle" => |
|
313 "thy_isab_" ^ theory'2thyID thyID ^ "-cal-" ^ calID : guh |
|
314 | "IsacKnowledge" => |
|
315 "thy_isac_" ^ theory'2thyID thyID ^ "-cal-" ^ calID |
|
316 | "IsacScripts" => |
|
317 "thy_scri_" ^ theory'2thyID thyID ^ "-cal-" ^ calID |
|
318 | str => raise error ("cal2guh called with isa = '"^isa^ |
|
319 "' for cal = '"^calID^"'"); |
|
320 fun cal2filename (isa, thyID:thyID) calID = |
|
321 cal2guh (isa, thyID:thyID) calID ^ ".xml" : filename; |
|
322 |
|
323 fun ord2guh (isa, thyID:thyID) (rew_ord':rew_ord') = |
|
324 case isa of |
|
325 "Isabelle" => |
|
326 "thy_isab_" ^ theory'2thyID thyID ^ "-ord-" ^ rew_ord' : guh |
|
327 | "IsacKnowledge" => |
|
328 "thy_isac_" ^ theory'2thyID thyID ^ "-ord-" ^ rew_ord' |
|
329 | "IsacScripts" => |
|
330 "thy_scri_" ^ theory'2thyID thyID ^ "-ord-" ^ rew_ord' |
|
331 | str => raise error ("ord2guh called with isa = '"^isa^ |
|
332 "' for ord = '"^rew_ord'^"'"); |
|
333 fun ord2filename (isa, thyID:thyID) (rew_ord':rew_ord') = |
|
334 ord2guh (isa, thyID:thyID) (rew_ord':rew_ord') ^ ".xml" : filename; |
|
335 |
|
336 |
|
337 (**.set up isab_thm_thy in Isac.ML.**) |
|
338 |
|
339 fun rearrange (thyID, (thmID, thm)) = (thmID, (thyID, thm)); |
|
340 fun rearrange_inv (thmID, (thyID, thm)) = (thyID, (thmID, thm)); |
|
341 |
|
342 (*.lookup the missing theorems in some thy (of Isabelle).*) |
|
343 fun make_isa missthms thy = |
|
344 map (pair (theory2thyID thy)) |
|
345 ((inter eq_thmI) missthms (PureThy.all_thms_of thy)) |
|
346 : (thyID * (thmID * Thm.thm)) list; |
|
347 |
|
348 (*.separate handling of sym_thms.*) |
|
349 fun make_isab rlsthmsNOTisac isab_thys = |
|
350 let fun les ((s1,_), (s2,_)) = (s1 : string) < s2 |
|
351 val notsym = filter_out (is_sym o #1) rlsthmsNOTisac |
|
352 val notsym_isab = (flat o (map (make_isa notsym))) isab_thys |
|
353 |
|
354 val sym = filter (is_sym o #1) rlsthmsNOTisac |
|
355 |
|
356 val symsym = map ((apfst sym_drop) o (apsnd sym_thm)) sym |
|
357 val symsym_isab = (flat o (map (make_isa symsym))) isab_thys |
|
358 |
|
359 val sym_isab = map (((apsnd o apfst) sym_drop) o |
|
360 ((apsnd o apsnd) sym_thm)) symsym_isab |
|
361 |
|
362 val isab = notsym_isab @ symsym_isab @ sym_isab |
|
363 in ((map rearrange) o (gen_sort les)) isab |
|
364 : (thmID * (thyID * Thm.thm)) list |
|
365 end; |
|
366 |
|
367 (*.which theory below thy' contains a theorem; this can be in isabelle ! |
|
368 get the occurence _after_ in the _list_ (is up to asking TUM) theory'.*) |
|
369 (* val (str, (_, thy)) = ("real_diff_minus", ("Root.thy", Root.thy)); |
|
370 val (str, (_, thy)) = ("real_diff_minus", ("Poly.thy", Poly.thy)); |
|
371 *) |
|
372 fun thy_contains_thm (str:xstring) (_, thy) = |
|
373 member op = (map (strip_thy o fst) (PureThy.all_thms_of thy)) str; |
|
374 (* val (thy', str) = ("Isac.thy", "real_mult_minus1"); |
|
375 val (thy', str) = ("PolyMinus.thy", "klammer_minus_plus"); |
|
376 *) |
|
377 fun thy_containing_thm (thy':theory') (str:xstring) = |
|
378 let val thy' = thyID2theory' thy' |
|
379 val str = sym_drop str |
|
380 val startsearch = dropuntil ((curry op= thy') o |
|
381 (#1:theory' * theory -> theory')) |
|
382 (rev (!theory')) |
|
383 in case find_first (thy_contains_thm str) startsearch of |
|
384 SOME (thy',_) => ("IsacKnowledge", thy') |
|
385 | NONE => (case assoc (!isab_thm_thy (*see Isac.ML*), str) of |
|
386 SOME (thyID,_) => ("Isabelle", thyID) |
|
387 | NONE => |
|
388 raise error ("thy_containing_thm: theorem '"^str^ |
|
389 "' not in !theory' above thy '"^thy'^"'")) |
|
390 end; |
|
391 |
|
392 |
|
393 (*.which theory below thy' contains a ruleset; |
|
394 get the occurence _after_ in the _list_ (is up to asking TUM) theory'.*) |
|
395 (* val (thy', rls') = ("PolyEq.thy", "separate_bdv"); |
|
396 *) |
|
397 local infix mem; (*from Isabelle2002*) |
|
398 fun x mem [] = false |
|
399 | x mem (y :: ys) = x = y orelse x mem ys; |
|
400 in |
|
401 fun thy_containing_rls (thy':theory') (rls':rls') = |
|
402 let val rls' = strip_thy rls' |
|
403 val thy' = thyID2theory' thy' |
|
404 (*take thys between "Isac" and thy' not to search #1#*) |
|
405 val dropthys = takewhile [] (not o (curry op= thy') o |
|
406 (#1:theory' * theory -> theory')) |
|
407 (rev (!theory')) |
|
408 val dropthy's = map (get_thy o (#1 : (theory' * theory) -> theory')) |
|
409 dropthys |
|
410 (*drop those rulesets which are generated in a theory found in #1#*) |
|
411 val startsearch = filter_out ((curry ((op mem) o swap) dropthy's) o |
|
412 ((#1 o #2) : rls' * (theory' * rls) |
|
413 -> theory')) |
|
414 (rev (!ruleset')) |
|
415 in case assoc (startsearch, rls') of |
|
416 SOME (thy', _) => ("IsacKnowledge", thyID2theory' thy') |
|
417 | _ => raise error ("thy_containing_rls : rls '"^rls'^ |
|
418 "' not in !rulset' above thy '"^thy'^"'") |
|
419 end; |
|
420 (* val (thy', termop) = (thyID, termop); |
|
421 *) |
|
422 fun thy_containing_cal (thy':theory') termop = |
|
423 let val thy' = thyID2theory' thy' |
|
424 val dropthys = takewhile [] (not o (curry op= thy') o |
|
425 (#1:theory' * theory -> theory')) |
|
426 (rev (!theory')) |
|
427 val dropthy's = map (get_thy o (#1 : (theory' * theory) -> theory')) |
|
428 dropthys |
|
429 val startsearch = filter_out ((curry ((op mem) o swap) dropthy's) o |
|
430 (#1 : calc -> string)) (rev (!calclist')) |
|
431 in case assoc (startsearch, strip_thy termop) of |
|
432 SOME (th_termop, _) => ("IsacKnowledge", strip_thy th_termop) |
|
433 | _ => raise error ("thy_containing_rls : rls '"^termop^ |
|
434 "' not in !calclist' above thy '"^thy'^"'") |
|
435 end |
|
436 end; |
|
437 |
|
438 (* print_depth 99; map #1 startsearch; print_depth 3; |
|
439 *) |
|
440 |
|
441 (*.packing return-values to matchTheory, contextToThy for xml-generation.*) |
|
442 datatype contthy = (*also an item from KEStore on Browser ......#*) |
|
443 EContThy (*not from KEStore ...........................*) |
|
444 | ContThm of (*a theorem in contex =============*) |
|
445 {thyID : thyID, (*for *2guh in sub-elems here .*) |
|
446 thm : guh, (*theorem in the context .*) |
|
447 applto : term, (*applied to formula ... .*) |
|
448 applat : term, (*... with lhs inserted .*) |
|
449 reword : rew_ord', (*order used for rewrite .*) |
|
450 asms : (term (*asumption instantiated .*) |
|
451 * term) list, (*asumption evaluated .*) |
|
452 lhs : term (*lhs of the theorem ... #*) |
|
453 * term, (*... instantiated .*) |
|
454 rhs : term (*rhs of the theorem ... #*) |
|
455 * term, (*... instantiated .*) |
|
456 result : term, (*resulting from the rewrite .*) |
|
457 resasms : term list, (*... with asms stored .*) |
|
458 asmrls : rls' (*ruleset for evaluating asms .*) |
|
459 } |
|
460 | ContThmInst of (*a theorem with bdvs in contex ======== *) |
|
461 {thyID : thyID, (*for *2guh in sub-elems here .*) |
|
462 thm : guh, (*theorem in the context .*) |
|
463 bdvs : subst, (*bound variables to modify....*) |
|
464 thminst : term, (*... theorem instantiated .*) |
|
465 applto : term, (*applied to formula ... .*) |
|
466 applat : term, (*... with lhs inserted .*) |
|
467 reword : rew_ord', (*order used for rewrite .*) |
|
468 asms : (term (*asumption instantiated .*) |
|
469 * term) list, (*asumption evaluated .*) |
|
470 lhs : term (*lhs of the theorem ... #*) |
|
471 * term, (*... instantiated .*) |
|
472 rhs : term (*rhs of the theorem ... #*) |
|
473 * term, (*... instantiated .*) |
|
474 result : term, (*resulting from the rewrite .*) |
|
475 resasms : term list, (*... with asms stored .*) |
|
476 asmrls : rls' (*ruleset for evaluating asms .*) |
|
477 } |
|
478 | ContRls of (*a rule set in contex ===================== *) |
|
479 {thyID : thyID, (*for *2guh in sub-elems here .*) |
|
480 rls : guh, (*rule set in the context .*) |
|
481 applto : term, (*rewrite this formula .*) |
|
482 result : term, (*resulting from the rewrite .*) |
|
483 asms : term list (*... with asms stored .*) |
|
484 } |
|
485 | ContRlsInst of (*a rule set with bdvs in contex ======= *) |
|
486 {thyID : thyID, (*for *2guh in sub-elems here .*) |
|
487 rls : guh, (*rule set in the context .*) |
|
488 bdvs : subst, (*for bound variables in thms .*) |
|
489 applto : term, (*rewrite this formula .*) |
|
490 result : term, (*resulting from the rewrite .*) |
|
491 asms : term list (*... with asms stored .*) |
|
492 } |
|
493 | ContNOrew of (*no rewrite for thm or rls ============== *) |
|
494 {thyID : thyID, (*for *2guh in sub-elems here .*) |
|
495 thm_rls : guh, (*thm or rls in the context .*) |
|
496 applto : term (*rewrite this formula .*) |
|
497 } |
|
498 | ContNOrewInst of (*no rewrite for some instantiation == *) |
|
499 {thyID : thyID, (*for *2guh in sub-elems here .*) |
|
500 thm_rls : guh, (*thm or rls in the context .*) |
|
501 bdvs : subst, (*for bound variables in thms .*) |
|
502 thminst : term, (*... theorem instantiated .*) |
|
503 applto : term (*rewrite this formula .*) |
|
504 }; |
|
505 |
|
506 (*.check a rewrite-tac for bdv (RL always used *_Inst !) TODO.WN060718 |
|
507 pass other tacs unchanged.*) |
|
508 fun get_tac_checked pt ((p,p_) : pos') = get_obj g_tac pt p; |
|
509 |
|
510 (*..*) |
|
511 |
|
512 |
|
513 |
|
514 (*.get the formula f at ptp rewritten by the Rewrite_* already applied to f.*) |
|
515 (* val (Rewrite' (thy', ord', erls, _, (thmID,_), f, (res,asm))) = tac'; |
|
516 *) |
|
517 fun context_thy (pt, pos as (p,p_)) (tac as Rewrite (thmID,_)) = |
|
518 (case applicable_in pos pt tac of |
|
519 Appl (Rewrite' (thy', ord', erls, _, (thmID,_), f, (res,asm))) => |
|
520 let val thy = assoc_thy thy' |
|
521 val thm = (norm o #prop o rep_thm o (PureThy.get_thm thy)) thmID |
|
522 (*WN060616 the following must be done on subterm found _IN_ rew_sub |
|
523 val (lhs,rhs) = (dest_equals' o strip_trueprop |
|
524 o Logic.strip_imp_concl) thm |
|
525 val insts = Pattern.match (Sign.tsig_of (sign_of thy)) (lhs, f) |
|
526 val thm' = ren_inst (insts, thm, lhs, f) |
|
527 val (lhs',rhs') = (dest_equals' o strip_trueprop |
|
528 o Logic.strip_imp_concl) thm' |
|
529 val asms = map strip_trueprop (Logic.strip_imp_prems thm) |
|
530 val asms' = map strip_trueprop (Logic.strip_imp_prems thm') |
|
531 *) |
|
532 in ContThm {thyID = theory'2thyID thy', |
|
533 thm = thm2guh (thy_containing_thm thy' thmID) thmID, |
|
534 applto = f, |
|
535 applat = e_term, |
|
536 reword = ord', |
|
537 asms = [](*asms ~~ asms'*), |
|
538 lhs = (e_term, e_term)(*(lhs, lhs')*), |
|
539 rhs = (e_term, e_term)(*(rhs, rhs')*), |
|
540 result = res, |
|
541 resasms = asm, |
|
542 asmrls = id_rls erls} |
|
543 end |
|
544 | Notappl _ => |
|
545 let val pp = par_pblobj pt p |
|
546 val thy' = get_obj g_domID pt pp |
|
547 val f = case p_ of |
|
548 Frm => get_obj g_form pt p |
|
549 | Res => (fst o (get_obj g_result pt)) p |
|
550 in ContNOrew {thyID = theory'2thyID thy', |
|
551 thm_rls = thm2guh (thy_containing_thm thy' thmID) thmID, |
|
552 applto = f} |
|
553 end) |
|
554 |
|
555 (* val ((pt,p), tac as Rewrite_Inst (subs, (thmID,_))) = ((pt,pos), tac); |
|
556 *) |
|
557 | context_thy (pt, pos as (p,p_)) |
|
558 (tac as Rewrite_Inst (subs, (thmID,_))) = |
|
559 (case applicable_in pos pt tac of |
|
560 (* val Appl (Rewrite_Inst' (thy', ord', erls, _, subst, (thmID,_), |
|
561 f, (res,asm))) = applicable_in p pt tac; |
|
562 *) |
|
563 Appl (Rewrite_Inst' (thy', ord', erls, _, subst, (thmID,_), |
|
564 f, (res,(*path to subterm,*)asm))) => |
|
565 let val thm = (norm o #prop o rep_thm o |
|
566 (PureThy.get_thm (assoc_thy thy'))) thmID |
|
567 val thminst = inst_bdv subst thm |
|
568 (*WN060616 the following must be done on subterm found _IN_ rew_sub |
|
569 val (lhs,rhs) = (dest_equals' o strip_trueprop |
|
570 o Logic.strip_imp_concl) thminst |
|
571 val insts = Pattern.match (Sign.tsig_of (sign_of thy)) (lhs, f) |
|
572 val thm' = ren_inst (insts, thminst, lhs, f) |
|
573 val (lhs',rhs') = (dest_equals' o strip_trueprop |
|
574 o Logic.strip_imp_concl) thm' |
|
575 val asms = map strip_trueprop (Logic.strip_imp_prems thminst) |
|
576 val asms' = map strip_trueprop (Logic.strip_imp_prems thm') |
|
577 *) |
|
578 in ContThmInst {thyID = theory'2thyID thy', |
|
579 thm = thm2guh (thy_containing_thm |
|
580 thy' thmID) thmID, |
|
581 bdvs = subst, |
|
582 thminst = thminst, |
|
583 applto = f, |
|
584 applat = e_term, |
|
585 reword = ord', |
|
586 asms = [](*asms ~~ asms'*), |
|
587 lhs = (e_term, e_term)(*(lhs, lhs')*), |
|
588 rhs = (e_term, e_term)(*(rhs, rhs')*), |
|
589 result = res, |
|
590 resasms = asm, |
|
591 asmrls = id_rls erls} |
|
592 end |
|
593 | Notappl _ => |
|
594 let val pp = par_pblobj pt p |
|
595 val thy' = get_obj g_domID pt pp |
|
596 val subst = subs2subst (assoc_thy thy') subs |
|
597 val thm = (norm o #prop o rep_thm o |
|
598 (PureThy.get_thm (assoc_thy thy'))) thmID |
|
599 val thminst = inst_bdv subst thm |
|
600 val f = case p_ of |
|
601 Frm => get_obj g_form pt p |
|
602 | Res => (fst o (get_obj g_result pt)) p |
|
603 in ContNOrewInst {thyID = theory'2thyID thy', |
|
604 thm_rls = thm2guh (thy_containing_thm |
|
605 thy' thmID) thmID, |
|
606 bdvs = subst, |
|
607 thminst = thminst, |
|
608 applto = f} |
|
609 end) |
|
610 | context_thy (pt,p) (tac as Rewrite_Set rls') = |
|
611 (case applicable_in p pt tac of |
|
612 Appl (Rewrite_Set' (thy', _, rls, f, (res,asm))) => |
|
613 ContRls {thyID = theory'2thyID thy', |
|
614 rls = rls2guh (thy_containing_rls thy' rls') rls', |
|
615 applto = f, |
|
616 result = res, |
|
617 asms = asm}) |
|
618 | context_thy (pt,p) (tac as Rewrite_Set_Inst (subs, rls')) = |
|
619 (case applicable_in p pt tac of |
|
620 Appl (Rewrite_Set_Inst' (thy', _, subst, rls, f, (res,asm))) => |
|
621 ContRlsInst {thyID = theory'2thyID thy', |
|
622 rls = rls2guh (thy_containing_rls thy' rls') rls', |
|
623 bdvs = subst, |
|
624 applto = f, |
|
625 result = res, |
|
626 asms = asm}); |
|
627 |
|
628 (*.get all theorems in a rule set (recursivley containing rule sets).*) |
|
629 fun thm_of_rule Erule = [] |
|
630 | thm_of_rule (thm as Thm _) = [thm] |
|
631 | thm_of_rule (Calc _) = [] |
|
632 | thm_of_rule (Cal1 _) = [] |
|
633 | thm_of_rule (Rls_ rls) = thms_of_rls rls |
|
634 and thms_of_rls Erls = [] |
|
635 | thms_of_rls (Rls {rules,...}) = (flat o (map thm_of_rule)) rules |
|
636 | thms_of_rls (Seq {rules,...}) = (flat o (map thm_of_rule)) rules |
|
637 | thms_of_rls (Rrls _) = []; |
|
638 (* val Hrls {thy_rls = (_, rls),...} = |
|
639 get_the ["IsacKnowledge", "Test", "Rulesets", "expand_binomtest"]; |
|
640 > thms_of_rls rls; |
|
641 *) |
|
642 |
|
643 (*. check if a rule is contained in a rule-set (recursivley down in Rls_); |
|
644 this rule can even be a rule-set itself.*) |
|
645 fun contains_rule r rls = |
|
646 let fun find (r, Rls_ rls) = finds (get_rules rls) |
|
647 | find r12 = eq_rule r12 |
|
648 and finds [] = false |
|
649 | finds (r1 :: rs) = if eq_rule (r, r1) then true else finds rs; |
|
650 in |
|
651 (*writeln ("### contains_rule: r = "^rule2str r^", rls = "^rls2str rls);*) |
|
652 finds (get_rules rls) |
|
653 end; |
|
654 |
|
655 (*. try if a rewrite-rule is applicable to a given formula; |
|
656 in case of rule-sets (recursivley) collect all _atomic_ rewrites .*) |
|
657 fun try_rew thy ((_, ro):rew_ord) erls (subst:subst) f (thm' as Thm(id, thm)) = |
|
658 if contains_bdv thm |
|
659 then case rewrite_inst_ thy ro erls false subst thm f of |
|
660 SOME (f',_) =>[rule2tac subst thm'] |
|
661 | NONE => [] |
|
662 else (case rewrite_ thy ro erls false thm f of |
|
663 SOME (f',_) => [rule2tac [] thm'] |
|
664 | NONE => []) |
|
665 | try_rew thy _ _ _ f (cal as Calc c) = |
|
666 (case get_calculation_ thy c f of |
|
667 SOME (str, _) => [rule2tac [] cal] |
|
668 | NONE => []) |
|
669 | try_rew thy _ _ _ f (cal as Cal1 c) = |
|
670 (case get_calculation_ thy c f of |
|
671 SOME (str, _) => [rule2tac [] cal] |
|
672 | NONE => []) |
|
673 | try_rew thy _ _ subst f (Rls_ rls) = filter_appl_rews thy subst f rls |
|
674 and filter_appl_rews thy subst f (Rls {rew_ord = ro, erls, rules,...}) = |
|
675 distinct (flat (map (try_rew thy ro erls subst f) rules)) |
|
676 | filter_appl_rews thy subst f (Seq {rew_ord = ro, erls, rules,...}) = |
|
677 distinct (flat (map (try_rew thy ro erls subst f) rules)) |
|
678 | filter_appl_rews thy subst f (Rrls _) = []; |
|
679 |
|
680 (*. decide if a tactic is applicable to a given formula; |
|
681 in case of Rewrite_Set* go down to _atomic_ rewrite-tactics .*) |
|
682 (* val |
|
683 *) |
|
684 fun atomic_appl_tacs thy _ _ f (Calculate scrID) = |
|
685 try_rew thy e_rew_ordX e_rls [] f (Calc (snd(assoc1 (!calclist', scrID)))) |
|
686 | atomic_appl_tacs thy ro erls f (Rewrite (thm' as (thmID, _))) = |
|
687 try_rew thy (ro, assoc_rew_ord ro) erls [] f |
|
688 (Thm (thmID, assoc_thm' thy thm')) |
|
689 | atomic_appl_tacs thy ro erls f (Rewrite_Inst (subs, thm' as (thmID, _))) = |
|
690 try_rew thy (ro, assoc_rew_ord ro) erls (subs2subst thy subs) f |
|
691 (Thm (thmID, assoc_thm' thy thm')) |
|
692 |
|
693 | atomic_appl_tacs thy _ _ f (Rewrite_Set rls') = |
|
694 filter_appl_rews thy [] f (assoc_rls rls') |
|
695 | atomic_appl_tacs thy _ _ f (Rewrite_Set_Inst (subs, rls')) = |
|
696 filter_appl_rews thy (subs2subst thy subs) f (assoc_rls rls') |
|
697 | atomic_appl_tacs _ _ _ _ tac = |
|
698 (writeln ("### atomic_appl_tacs: not impl. for tac = '"^ tac2str tac ^"'"); |
|
699 []); |
|
700 |
|
701 |
|
702 |
|
703 |
|
704 |
|
705 (*.not only for thydata, but also for thy's etc.*) |
|
706 fun theID2guh (theID:theID) = |
|
707 case length theID of |
|
708 0 => raise error ("theID2guh: called with theID = "^strs2str' theID) |
|
709 | 1 => part2guh theID |
|
710 | 2 => thy2guh theID |
|
711 | 3 => thypart2guh theID |
|
712 | 4 => let val [isa, thyID, typ, elemID] = theID |
|
713 in case typ of |
|
714 "Theorems" => thm2guh (isa, thyID) elemID |
|
715 | "Rulesets" => rls2guh (isa, thyID) elemID |
|
716 | "Calculations" => cal2guh (isa, thyID) elemID |
|
717 | "Orders" => ord2guh (isa, thyID) elemID |
|
718 | "Theorems" => thy2guh [isa, thyID] |
|
719 | str => raise error ("theID2guh: called with theID = "^ |
|
720 strs2str' theID) |
|
721 end |
|
722 | n => raise error ("theID2guh called with theID = "^strs2str' theID); |
|
723 (*.filenames not only for thydata, but also for thy's etc.*) |
|
724 fun theID2filename (theID:theID) = theID2guh theID ^ ".xml" : filename; |
|
725 |
|
726 fun guh2theID (guh:guh) = |
|
727 let val guh' = explode guh |
|
728 val part = implode (take_fromto 1 4 guh') |
|
729 val isa = implode (take_fromto 5 9 guh') |
|
730 in if not (member op = ["exp_", "thy_", "pbl_", "met_"] part) |
|
731 then raise error ("guh '"^guh^"' does not begin with \ |
|
732 \exp_ | thy_ | pbl_ | met_") |
|
733 else let val chap = case isa of |
|
734 "isab_" => "Isabelle" |
|
735 | "scri_" => "IsacScripts" |
|
736 | "isac_" => "IsacKnowledge" |
|
737 | _ => |
|
738 raise error ("guh2theID: '"^guh^ |
|
739 "' does not have isab_ | scri_ | \ |
|
740 \isac_ at position 5..9") |
|
741 val rest = takerest (9, guh') |
|
742 val thyID = takewhile [] (not o (curry op= "-")) rest |
|
743 val rest' = dropuntil (curry op= "-") rest |
|
744 in case implode rest' of |
|
745 "-part" => [chap] : theID |
|
746 | "" => [chap, implode thyID] |
|
747 | "-Theorems" => [chap, implode thyID, "Theorems"] |
|
748 | "-Rulesets" => [chap, implode thyID, "Rulesets"] |
|
749 | "-Operations" => [chap, implode thyID, "Operations"] |
|
750 | "-Orders" => [chap, implode thyID, "Orders"] |
|
751 | _ => |
|
752 let val sect = implode (take_fromto 1 5 rest') |
|
753 val sect' = |
|
754 case sect of |
|
755 "-thm-" => "Theorems" |
|
756 | "-rls-" => "Rulesets" |
|
757 | "-cal-" => "Operations" |
|
758 | "-ord-" => "Orders" |
|
759 | str => |
|
760 raise error ("guh2theID: '"^guh^"' has '"^sect^ |
|
761 "' instead -thm- | -rls- | \ |
|
762 \-cal- | -ord-") |
|
763 in [chap, implode thyID, sect', implode |
|
764 (takerest (5, rest'))] |
|
765 end |
|
766 end |
|
767 end; |
|
768 (*> guh2theID "thy_isac_Biegelinie-Theorems"; |
|
769 val it = ["IsacKnowledge", "Biegelinie", "Theorems"] : theID |
|
770 > guh2theID "thy_scri_ListC-thm-zip_Nil"; |
|
771 val it = ["IsacScripts", "ListC", "Theorems", "zip_Nil"] : theID*) |
|
772 |
|
773 fun guh2filename (guh : guh) = guh ^ ".xml" : filename; |
|
774 |
|
775 |
|
776 (*..*) |
|
777 fun guh2rewtac (guh:guh) ([] : subs) = |
|
778 let val [isa, thy, sect, xstr] = guh2theID guh |
|
779 in case sect of |
|
780 "Theorems" => Rewrite (xstr, "") |
|
781 | "Rulesets" => Rewrite_Set xstr |
|
782 | str => raise error ("guh2rewtac: not impl. for '"^xstr^"'") |
|
783 end |
|
784 | guh2rewtac (guh:guh) subs = |
|
785 let val [isa, thy, sect, xstr] = guh2theID guh |
|
786 in case sect of |
|
787 "Theorems" => Rewrite_Inst (subs, (xstr, "")) |
|
788 | "Rulesets" => Rewrite_Set_Inst (subs, xstr) |
|
789 | str => raise error ("guh2rewtac: not impl. for '"^xstr^"'") |
|
790 end; |
|
791 (*> guh2rewtac "thy_isac_Test-thm-constant_mult_square" []; |
|
792 val it = Rewrite ("constant_mult_square", "") : tac |
|
793 > guh2rewtac "thy_isac_Test-thm-risolate_bdv_add" ["(bdv, x)"]; |
|
794 val it = Rewrite_Inst (["(bdv, x)"], ("risolate_bdv_add", "")) : tac |
|
795 > guh2rewtac "thy_isac_Test-rls-Test_simplify" []; |
|
796 val it = Rewrite_Set "Test_simplify" : tac |
|
797 > guh2rewtac "thy_isac_Test-rls-isolate_bdv" ["(bdv, x)"]; |
|
798 val it = Rewrite_Set_Inst (["(bdv, x)"], "isolate_bdv") : tac*) |
|
799 |
|
800 |
|
801 (*.the front-end may request a context for any element of the hierarchy.*) |
|
802 (* val guh = "thy_isac_Test-rls-Test_simplify"; |
|
803 *) |
|
804 fun no_thycontext (guh : guh) = (guh2theID guh; false) |
|
805 handle _ => true; |
|
806 |
|
807 (*> has_thycontext "thy_isac_Test"; |
|
808 if has_thycontext "thy_isac_Test" then "OK" else "NOTOK"; |
|
809 *) |
|
810 |
|
811 |
|
812 |
|
813 (*.get the substitution of bound variables for matchTheory: |
|
814 # lookup the thm|rls' in the script |
|
815 # take the [(bdv, v_),..] from the respective Rewrite_(Set_)Inst |
|
816 # instantiate this subs with the istates env to [(bdv, x),..] |
|
817 # otherwise [].*) |
|
818 (*WN060617 hack assuming that all scripts use only one bound variable |
|
819 and use 'v_' as the formal argument for this bound variable*) |
|
820 (* val (ScrState (env,_,_,_,_,_), _, guh) = (is, "dummy", guh); |
|
821 *) |
|
822 fun subs_from (ScrState (env,_,_,_,_,_)) _(*:Script sc*) (guh:guh) = |
|
823 let val theID as [isa, thyID, sect, xstr] = guh2theID guh |
|
824 in case sect of |
|
825 "Theorems" => |
|
826 let val thm = PureThy.get_thm (assoc_thy (thyID2theory' thyID)) xstr |
|
827 in if contains_bdv thm |
|
828 then let val formal_arg = str2term "v_" |
|
829 val value = subst_atomic env formal_arg |
|
830 in ["(bdv," ^ term2str value ^ ")"]:subs end |
|
831 else [] |
|
832 end |
|
833 | "Rulesets" => |
|
834 let val rules = (get_rules o assoc_rls) xstr |
|
835 in if contain_bdv rules |
|
836 then let val formal_arg = str2term"v_" |
|
837 val value = subst_atomic env formal_arg |
|
838 in ["(bdv,"^term2str value^")"]:subs end |
|
839 else [] |
|
840 end |
|
841 end; |
|
842 |
|
843 (* use"ME/rewtools.sml"; |
|
844 *) |
|
845 |