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