2 (c) Walther Neuper 2000
4 use"ProgLang/rewrite.sml";
10 exception STOP_REW_SUB; (*WN050820 quick and dirty*)
12 (*17.6.00: rewrite by going down the term with rew_sub*)
13 (* val (thy, i, bdv, tless, rls, put_asm, thm, ct) =
14 (thy, 1, []:(Term.term * Term.term) list, rew_ord, erls, bool,thm,term);
16 fun rewrite__ thy i bdv tless rls put_asm thm ct =
18 val (t',asms,lrd,rew) =
19 rew_sub thy i bdv tless rls put_asm [(*root of the term*)]
20 (((inst_bdv bdv) o norm o #prop o rep_thm) thm) ct;
21 in if rew then SOME (t', distinct asms)
23 (* one rewrite (possibly conditional, ordered) EXOR exn EXOR go into subterms *)
24 and rew_sub thy i bdv tless rls put_asm lrd r t =
25 ((*tracing ("@@@ rew_sub begin: t = "^(term2str t));*)
26 let (* copy from Pure/thm.ML: fun rewritec *)
27 val (lhs, rhs) = (HOLogic.dest_eq o HOLogic.dest_Trueprop
28 o Logic.strip_imp_concl) r;
29 val r' = Envir.subst_term (Pattern.match thy (lhs, t)
30 (Vartab.empty, Vartab.empty)) r;
31 val p' = map HOLogic.dest_Trueprop ((fst o Logic.strip_prems)
32 (Logic.count_prems r', [], r'));
33 val t' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop
34 o Logic.strip_imp_concl) r';
35 (*val _= tracing("@@@ rew_sub match: t'= "^(term2str t'));*)
36 val _= if ! trace_rewrite andalso i < ! depth andalso p' <> []
37 then tracing((idt"#"(i+1))^" eval asms: "^(term2str r')) else();
38 val (t'',p'') = (*conditional rewriting*)
39 let val (simpl_p', nofalse) = eval__true thy (i+1) p' bdv rls
41 then (if ! trace_rewrite andalso i < ! depth andalso p' <> []
42 then tracing((idt"#"(i+1))^" asms accepted: "^(terms2str p')^
43 " stored: "^(terms2str simpl_p'))
44 else(); (t',simpl_p')) (* uncond.rew. from above*)
46 (if ! trace_rewrite andalso i < ! depth
47 then tracing((idt"#"(i+1))^" asms false: "^(terms2str p'))
48 else(); raise STOP_REW_SUB (*dont go into subterms of cond*))
50 in if perm lhs rhs andalso not (tless bdv (t',t)) (*ordered rewriting*)
51 then (if ! trace_rewrite andalso i < ! depth
52 then tracing((idt"#"i)^" not: \""^
53 (term2str t)^"\" > \""^
54 (term2str t')^"\"") else ();
56 else ((*tracing("##@ rew_sub: (t''= "^(term2str t'')^
57 ", p'' ="^(terms2str p'')^", true)");*)
60 ) handle _ (*NO_REWRITE WN050820 causes diff.behav. in tests + MATCH!*) =>
61 ((*tracing ("@@@ rew_sub gosub: t = "^(term2str t));*)
63 Const(s,T) => (Const(s,T),[],lrd,false)
64 | Free(s,T) => (Free(s,T),[],lrd,false)
65 | Var(n,T) => (Var(n,T),[],lrd,false)
66 | Bound i => (Bound i,[],lrd,false)
68 let val (t', asms, lrd, rew) =
69 rew_sub thy i bdv tless rls put_asm (lrd@[D]) r body
70 in (Abs(s,T,t'), asms, [], rew) end
72 let val (t2', asm2, lrd, rew2) =
73 rew_sub thy i bdv tless rls put_asm (lrd@[R]) r t2
74 in if rew2 then (t1 $ t2', asm2, lrd, true)
75 else let val (t1', asm1, lrd, rew1) =
76 rew_sub thy i bdv tless rls put_asm (lrd@[L]) r t1
77 in if rew1 then (t1' $ t2, asm1, lrd, true)
78 else (t1 $ t2,[], lrd, false) end
80 (* simplify asumptions until one evaluates to false, store intermined's (x~=0)*)
81 and eval__true thy i asms bdv rls =
82 if asms = [HOLogic.true_const] orelse asms = [] then ([], true)
83 (* this allows to check Rrls with prepat = ([HOLogic.true_const], pat) *)
84 else if asms = [HOLogic.false_const] then ([], false)
86 fun chk indets [] = (indets, true)(*return asms<>True until false*)
87 | chk indets (a::asms) =
88 (case rewrite__set_ thy (i+1) false bdv rls a of
89 NONE => (chk (indets @ [a]) asms)
91 if t = HOLogic.true_const
92 then (chk (indets @ a') asms)
93 else if t = HOLogic.false_const then ([], false)
94 (*asm false .. thm not applied ^^^; continue until False vvv*)
95 else chk (indets @ [t] @ a') asms);
97 (* rewrite with a rule set, which must not be the empty Erls *)
98 and rewrite__set_ _ _ __ Erls t =
99 error("rewrite__set_ called with 'Erls' for '"^term2str t^"'")
100 (* rewrite with a 'reverse rule set' implemented by ML code *)
101 | rewrite__set_ thy i _ _ (rrls as Rrls _) t =
102 let val _= if ! trace_rewrite andalso i < ! depth
103 then tracing ((idt"#"i)^" rls: "^(id_rls rrls)^" on: "^
104 (term2str t)) else ()
105 val (t', asm, rew) = app_rev thy (i+1) rrls t
106 in if rew then SOME (t', distinct asm)
108 (* rewrite with a rule set containing Thms or Calculations *)
109 | rewrite__set_ thy i put_asm bdv rls ct =
110 (* val (thy, i, put_asm, bdv, rls, ct) = (thy, 1, bool, [], rls, term);
113 datatype switch = Appl | Noap;
114 fun rew_once ruls asm ct Noap [] = (ct,asm)
115 | rew_once ruls asm ct Appl [] =
116 (case rls of Rls _ => rew_once ruls asm ct Noap ruls
118 | rew_once ruls asm ct apno (rul::thms) =
119 (* val (ruls, asm, ct, apno, (rul::thms)) = (ruls, [], ct, Noap, ruls);
120 val Thm (thmid, thm) = rul;
124 (if !trace_rewrite andalso i < ! depth
125 then tracing((idt"#"(i+1))^" try thm: "^thmid) else ();
126 case rewrite__ thy (i+1) bdv ((snd o #rew_ord o rep_rls) rls)
127 ((#erls o rep_rls) rls) put_asm thm ct of
128 NONE => rew_once ruls asm ct apno thms
129 | SOME (ct',asm') => (if ! trace_rewrite andalso i < ! depth
130 then tracing((idt"="(i+1))^" rewrites to: "^
131 (term2str ct')) else ();
132 rew_once ruls (union (op =) asm asm') ct' Appl (rul::thms)))
133 | Calc (cc as (op_,_)) =>
134 (let val _= if !trace_rewrite andalso i < ! depth then
135 tracing((idt"#"(i+1))^" try calc: "^op_^"'") else ();
136 val ct = uminus_to_string ct
137 in case get_calculation_ thy cc ct of
138 NONE => rew_once ruls asm ct apno thms
139 | SOME (thmid, thm') =>
142 rewrite__ thy (i+1) bdv ((snd o #rew_ord o rep_rls) rls)
143 ((#erls o rep_rls) rls) put_asm thm' ct;
144 val _ = if pairopt <> NONE then ()
145 else error("rewrite_set_, rewrite_ \""^
146 (string_of_thmI thm')^"\" "^(term2str ct)^" = NONE")
147 val _ = if ! trace_rewrite andalso i < ! depth
148 then tracing((idt"="(i+1))^" calc. to: "^
149 (term2str ((fst o the) pairopt)))
151 in rew_once ruls asm ((fst o the) pairopt) Appl (rul::thms) end
153 | Cal1 (cc as (op_,_)) =>
154 (let val _= if !trace_rewrite andalso i < ! depth then
155 tracing((idt"#"(i+1))^" try cal1: "^op_^"'") else ();
156 val ct = uminus_to_string ct
157 in case get_calculation1_ thy cc ct of
159 | SOME (thmid, thm') =>
162 rewrite__ thy (i+1) bdv ((snd o #rew_ord o rep_rls) rls)
163 ((#erls o rep_rls) rls) put_asm thm' ct;
164 val _ = if pairopt <> NONE then ()
165 else error("rewrite_set_, rewrite_ \""^
166 (string_of_thmI thm')^"\" "^(term2str ct)^" = NONE")
167 val _ = if ! trace_rewrite andalso i < ! depth
168 then tracing((idt"="(i+1))^" cal1. to: "^
169 (term2str ((fst o the) pairopt)))
174 (case rewrite__set_ thy (i+1) put_asm bdv rls' ct of
175 SOME (t',asm') => rew_once ruls (union (op =) asm asm') t' Appl thms
176 | NONE => rew_once ruls asm ct apno thms);
178 val ruls = (#rules o rep_rls) rls;
179 val _= if ! trace_rewrite andalso i < ! depth
180 then tracing ((idt"#"i)^" rls: "^(id_rls rls)^" on: "^
181 (term2str ct)) else ()
182 val (ct',asm') = rew_once ruls [] ct Noap ruls;
183 in if ct = ct' then NONE else SOME (ct', distinct asm') end
185 and app_rev thy i rrls t =
186 let (* check a (precond, pattern) of a rev-set; stops with 1st true *)
187 fun chk_prepat thy erls [] t = true
188 | chk_prepat thy erls prepat t =
189 let fun chk (pres, pat) =
190 (let val subst: Type.tyenv * Envir.tenv =
191 Pattern.match thy (pat, t)
192 (Vartab.empty, Vartab.empty)
193 val _ = tracing ("app_rev: pres=------------------");
194 val _ = tracing ("app_rev: pres=" ^ terms2str pres);
195 val _ = tracing ("app_rev: pat =" ^ term2str pat);
196 val _ = tracing ("app_rev: t =" ^ term2str t);
197 in snd (eval__true thy (i+1)
198 (map (Envir.subst_term subst) pres)
202 fun scan_ f [] = false (*scan_ NEVER called by []*)
203 | scan_ f (pp::pps) = if f pp then true
205 in scan_ chk prepat end;
207 (* apply the normal_form of a rev-set *)
208 fun app_rev' thy (Rrls{erls,prepat,scr=Rfuns{normal_form,...},...}) t =
209 if chk_prepat thy erls prepat t
210 then ((*tracing("### app_rev': t = "^(term2str t));*)
214 val opt = app_rev' thy rrls t
216 SOME (t', asm) => (t', asm, true)
217 | NONE => app_sub thy i rrls t
219 and app_sub thy i rrls t =
220 ((*tracing("### app_sub: subterm = "^(term2str t));*)
222 Const (s, T) => (Const(s, T), [], false)
223 | Free (s, T) => (Free(s, T), [], false)
224 | Var (n, T) => (Var(n, T), [], false)
225 | Bound i => (Bound i, [], false)
226 | Abs (s, T, body) =>
227 let val (t', asm, rew) = app_rev thy i rrls body
228 in (Abs(s, T, t'), asm, rew) end
230 let val (t2', asm2, rew2) = app_rev thy i rrls t2
231 in if rew2 then (t1 $ t2', asm2, true)
232 else let val (t1', asm1, rew1) = app_rev thy i rrls t1
233 in if rew1 then (t1' $ t2, asm1, true)
234 else (t1 $ t2, [], false) end
239 (*.rewriting without argument [] for rew_ord.*)
240 (*WN.11.6.03: shouldnt asm<>[] lead to false ????*)
241 fun eval_true thy terms rls = (snd o (eval__true thy 1 terms [])) rls;
244 (*.rewriting without internal argument [] for rew_ord.*)
245 (* val (thy, rew_ord, erls, bool, thm, term) =
246 (thy, (assoc_rew_ord ro), rls', false, (assoc_thm' thy thm'), f);
247 val (thy, rew_ord, erls, bool, thm, term) =
248 (thy, rew_ord, erls, false, thm, t'');
250 fun rewrite_ thy rew_ord erls bool thm term =
251 rewrite__ thy 1 [] rew_ord erls bool thm term;
252 fun rewrite_set_ thy bool rls term =
253 (* val (thy, bool, rls, term) = (thy, false, srls, t);
255 rewrite__set_ thy 1 bool [] rls term;
258 fun subs'2subst thy (s:subs') =
259 (((map (apfst (term_of o the o (parse thy))))
260 o (map (apsnd (term_of o the o (parse thy))))) s):subst;
262 (*.variants of rewrite.*)
263 (*FIXME 12.8.02: put_asm = true <==> rewrite_inst,
264 thus the argument put_asm IS NOT NECESSARY -- FIXME*)
265 (* val (rew_ord,rls,put_asm,thm,ct)=
266 (e_rew_ord,poly_erls,false,num_str d1_isolate_add2,t);
268 fun rewrite_inst_ (thy:theory) rew_ord (rls:rls) (put_asm:bool)
269 (subst:(term * term) list) (thm:thm) (ct:term) =
270 rewrite__ thy 1 subst rew_ord rls put_asm thm ct;
272 fun rewrite_set_inst_ (thy:theory)
273 (put_asm:bool) (subst:(term * term) list) (rls:rls) (ct:term) =
275 val subst = subs'2subst thy subs';
276 val subrls = instantiate_rls subs' rls
277 in*) rewrite__set_ thy 1 put_asm subst (*sub*)rls ct
280 (* given a list of equalities (lhs = rhs) and a term,
281 replace all occurrences of lhs in the term with rhs;
282 thus the order or equalities matters: put variables in lhs first. *)
283 fun rewrite_terms_ thy ord erls equs t =
284 let (*val _=tracing("### rewrite_terms_ equs= '"^terms2str equs^"' ..."^
285 term_detail2str (hd equs)^
286 "### rewrite_terms_ t= '"^term2str t^"' ..."^
287 term_detail2str t);*)
288 fun rew_ (t', asm') [] _ = (t', asm')
289 (* 1st val (t', asm', rules as r::rs, t) = (e_term, [], equs, t);
290 2nd val (t', asm', rules as r::rs, t) = (t'', [], rules, t'');
291 rew_ (t', asm') (r::rs) t;
293 | rew_ (t', asm') (rules as r::rs) t =
294 let val _ = tracing("rew_ "^term2str t);
295 val (t'', asm'', lrd, rew) =
296 rew_sub thy 1 [] ord erls false [] (Trueprop $ r) t
298 then (tracing ("true rew_ " ^ term2str t'');
299 rew_ (t'', asm' @ asm'') rules t'')
300 else (tracing ("false rew_ " ^ term2str t'');
301 rew_ (t', asm') rs t')
303 val (t'', asm'') = rew_ (e_term, []) equs t
305 then NONE else SOME (t'', asm'')
309 (*. search ct for adjacent numerals and calculate them by operator isa_fn .*)
310 fun calculate_ thy isa_fn ct =
311 let val ct = uminus_to_string ct
312 in case get_calculation_ thy isa_fn ct of
314 | SOME (thmID, thm) =>
315 (let val SOME (rew,_) = rewrite_ thy dummy_ord e_rls false thm ct
316 in SOME (rew,(thmID, thm)) end)
317 handle _ => error ("calculate_: "^thmID^" does not rewrite")
320 > val thy = InsSort.thy;
321 > val op_ = "le"; (* < *)
322 > val ct = (the o (parse thy))
323 "foldr ins [#2] (if #1 < #3 then #1 # ins [] #3 else [#3, #1])";
324 > calculate_ thy op_ ct;
326 ("foldr ins [#2] (if True then #1 # ins [] #3 else [#3, #1])",
327 "(#1 < #3) = True") : (cterm * thm) option *)
330 (* for test-printouts:
331 val _ = tracing("in rew_sub : "^( Syntax.string_of_term (thy2ctxt thy) t))
332 val _ = tracing("in eval_true: prems= "^(commas (map (Syntax.string_of_term (thy2ctxt thy)) prems')))
340 fun get_rls_scr rs' = ((#scr o rep_rls o #2 o the o assoc') (!ruleset',rs'))
341 handle _ => error ("get_rls_scr: no script for "^rs');
344 (*make_thm added to Pure/thm.ML*)
346 let val t = (term_of o the o (parse thy)) str
348 Const ("==>",_) $ _ $ _ => t
350 in make_thm (cterm_of thy t') end;
352 val str = "?r ^^^ 2 = ?r * ?r";
353 val thm = realpow_twoI;
355 val t1 = (#prop o rep_thm) (num_str thm);
356 val t2 = Trueprop $ ((term_of o the o (parse thy)) str);
358 val it = true : bool ... !!!
359 val th1 = (num_str thm);
360 val th2 = ((*num_str*) (mk_thm thy str)) handle e => print_exn e;
362 ML> val it = false : bool ... HIDDEN DIFFERENCES IRRELEVANT FOR ISAC ?!
364 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
365 val str = "k ~= 0 ==> m * k / (n * k) = m / n";
366 val thm = real_mult_div_cancel2;
368 val t1 = (#prop o rep_thm) (num_str thm);
369 val t2 = ((term_of o the o (parse thy)) str);
371 val it = false : bool ... Var .. Free
372 val th1 = (num_str thm);
373 val th2 = ((*num_str*) (mk_thm thy str)) handle e => print_exn e;
375 ML> val it = false : bool ... PLUS HIDDEN DIFFERENCES IRRELEVANT FOR ISAC ?!
379 (*prints subgoal etc.
380 ((goal thy);(topthm()) o ) str; *)
381 (*assume rejects scheme variables
382 assume ((cterm_of thy) (Trueprop $
383 (term_of o the o (parse thy)) str)); *)
386 (* outcommented 18.11.xx, xx < 02 -------
387 fun rul2rul' (Thm (thmid, thm)) = Thm'(thmid, string_of_thmI thm)
388 | rul2rul' (Calc op_) = Calc' op_;
389 fun rul'2rul thy (Thm'(thmid, ct')) =
390 Thm (thmid, mk_thm thy ct')
391 | rul'2rul thy' (Calc' op_) = Calc op_;
394 fun rls2rls' (Rls{preconds=preconds,rew_ord=rew_ord,rules=rules}:rls) =
395 Rls'{preconds'= map string_of_cterm preconds,
396 rew_ord' = fst rew_ord,
397 rules' = map rul2rul' rules}:rlsdat';
399 fun rls'2rls thy' (Rls'{preconds'=preconds,rew_ord'=rew_ord,
400 rules'=rules}:rlsdat') =
401 let val thy = the (assoc' (theory',thy'))
402 in Rls{preconds = map (the o (parse thy)) preconds,
403 rew_ord = (rew_ord, the (assoc'(rew_ord',rew_ord))),
404 rules = map (rul'2rul thy) rules}:rls end;
407 (*.get the theorem associated with the xstring-identifier;
408 if the identifier starts with "sym_" then swap lhs = rhs around =
409 (ATTENTION: "RS sym" attaches a [.] -- remove it with string_of_thmI);
410 identifiers starting with "#" come from Calc and
411 get a hand-made theorem (containing numerals only).*)
412 fun assoc_thm' (thy:theory) ((thmid, ct'):thm') =
413 (case explode thmid of
414 "s"::"y"::"m"::"_"::id =>
417 else ((num_str o (PureThy.get_thm thy)) (implode id)) RS sym
421 else (num_str o (PureThy.get_thm thy)) thmid
423 error ("assoc_thm': '"^thmid^"' not in '"^
424 (theory2domID thy)^"' (and parents)");
425 (*> assoc_thm' Isac.thy ("sym_#mult_2_3","6 = 2 * 3");
426 val it = "6 = 2 * 3" : thm
428 > assoc_thm' Isac.thy ("add_0_left","");
429 val it = "0 + ?z = ?z" : thm
431 > assoc_thm' Isac.thy ("sym_real_add_zero_left","");
432 val it = "?t = 0 + ?t" [.] : thm
434 > assoc_thm' HOL.thy ("sym_real_add_zero_left","");
435 *** Unknown theorem(s) "add_0_left"
436 *** assoc_thm': 'sym_real_add_zero_left' not in 'HOL.thy' (and parents)
437 uncaught exception ERROR*)
440 fun parse' (thy:theory') (ct:cterm') =
441 case parse ((the o assoc')(!theory',thy)) ct of
443 | SOME ct => SOME ((term2str (term_of ct)):cterm');
446 (*FIXME 12.8.02: put_asm = true <==> rewrite_inst, rewrite_set_inst
447 thus the argument put_asm IS NOT NECESSARY -- FIXME ~~~~~*)
448 fun rewrite (thy':theory') (rew_ord:rew_ord') (rls:rls')
449 (put_asm:bool) (thm:thm') (ct:cterm') =
450 (* val (rew_ord, rls, thm, ct) = (rew_ord', id_rls rls', thm', f);
452 let val thy = (the o assoc')(!theory',thy');
455 ((the o assoc')(!rew_ord',rew_ord))((#2 o the o assoc')(!ruleset',rls))
456 put_asm ((assoc_thm' thy) thm)
457 ((term_of o the o (parse thy)) ct) of
459 | SOME (t, ts) => SOME (term2str t, terms2str ts)
463 val thy = "RatArith.thy";
464 val rew_ord = "dummy_ord";
465 > val rls = "eval_rls";
467 val thm = ("square_equation_left","");
468 val ct = "sqrt(#9+#4*x)=sqrt x + sqrt(#-3+x)";
470 val Zthy = ((the o assoc')(!theory',thy));
471 val Zrew_ord = ((the o assoc')(!rew_ord',rew_ord));
472 val Zrls = ((the o assoc')(!ruleset',rls));
473 val Zput_asm = put_asm;
474 val Zthm = ((the o (assoc'_thm' thy)) thm);
475 val Zct = ((the o (parse ((the o assoc')(!theory',thy)))) ct);
477 rewrite_ Zthy Zrew_ord Zrls Zput_asm Zthm Zct;
479 use"Isa99/interface_ME_ISA.sml";
482 (*FIXME 12.8.02: put_asm = true <==> rewrite_inst, rewrite_set_inst
483 thus the argument put_asm IS NOT NECESSARY -- FIXME ~~~~~*)
484 fun rewrite_set (thy':theory') (put_asm:bool)
485 (rls:rls') (ct:cterm') =
486 let val thy = (the o assoc')(!theory',thy');
488 case rewrite_set_ thy put_asm ((#2 o the o assoc')(!ruleset',rls))
489 ((term_of o the o (parse thy)) ct) of
491 | SOME (t, ts) => SOME (term2str t, terms2str ts)
494 (*evaluate list-expressions
495 should work on term, and stand in Isa99/rewrite-parse.sml,
496 but there list_rls <- eval_binop is not yet defined*)
497 (*fun eval_listexpr' ct =
498 let val rew = rewrite_set "ListC.thy" false "list_rls" ct;
501 | NONE => ct end;-----------------30.9.02---*)
502 fun eval_listexpr_ thy srls t =
503 (* val (thy, srls, t) =
504 ((assoc_thy th), sr, (subst_atomic (upd_env_opt E (a,v)) t));
506 let val rew = rewrite_set_ thy false srls t;
512 fun get_calculation' (thy:theory') op_ (ct:cterm') =
513 case get_calculation_ ((the o assoc')(!theory',thy)) op_
514 ((uminus_to_string o term_of o the o
515 (parse ((the o assoc')(!theory',thy)))) ct) of
517 | SOME (thmid, thm) =>
518 SOME ((thmid, string_of_thmI thm):thm');
520 fun calculate (thy':theory') op_ (ct:cterm') =
521 let val thy = (the o assoc')(!theory',thy');
523 case calculate_ thy op_
524 ((term_of o the o (parse thy)) ct) of
526 | SOME (ct,(thmID,thm)) =>
528 (thmID, string_of_thmI thm):thm')
531 fun instantiate'' thy' subs ((thmid,ct'):thm') =
532 let val thmid_ = implode ("#"::(explode thmid)) (*see type thm'*)
533 in (thmid_, (string_of_thmI o (read_instantiate subs))
534 ((the o (assoc_thm' thy')) (thmid_,ct'))):thm' end;
536 fun instantiate_rls' thy' subs (rls:rls') =
537 rls2rls' (instantiate_rls subs ((the o (assoc_rls thy')) rls)):rlsdat';
539 ... problem with these functions:
540 > val thm = mk_thm thy "(bdv + a = b) = (bdv = b - a)";
541 val thm = "(bdv + a = b) = (bdv = b - a)" : thm
542 > show_types:=true; thm;
543 val it = "((bdv::'a) + (a::'a) = (b::'a)) = (bdv = b - a)" : thm
544 ... and this doesn't match because of too general typing (?!)
545 and read_insitantiate doesn't instantiate the types (?!)
547 (1) hard-coded type-instantiation ("'a", "RatArith.rat")
548 (2) instantiate', instantiate ... no help by isabelle-users@ !!!
550 rewrite_inst, rewrite_set_inst circumvent the problem,
551 according functions out-commented with 'instantiate''
555 fun instantiate'' thy' subs ((thmid,ct'):thm') =
557 val thmid_ = implode ("#"::(explode thmid)); (*see type thm'*)
558 val thy = (the o assoc')(!theory',thy');
559 val typs = map (#T o rep_cterm o the o (parse thy))
560 ((snd o split_list) subs);
562 ((ctyp_of (sign_of thy)) o #T o rep_cterm o the o (parse thy))
563 ((snd o split_list) subs);
565 > val thy' = "RatArith.thy";
566 > val subs = [("bdv","x::rat"),("zzz","z::nat")];
567 > (the o (parse ((the o assoc')(!theory',thy')))) "x::rat";
568 > (#T o rep_cterm o the o (parse ((the o assoc')(!theory',thy'))));
570 > val ctyp = ((ctyp_of (sign_of thy)) o #T o rep_cterm o the o
571 (parse ((the o assoc')(!theory',thy')))) "x::rat";
572 > val bdv = (the o (parse thy)) "bdv";
573 > val x = (the o (parse thy)) "x";
574 > (instantiate ([(("'a",0),ctyp)],[(bdv,x)]) isolate_bdv_add)
575 handle e => print_exn e;
576 uncaught exception THM
577 raised at: thm.ML:1085.18-1085.69
581 > val bdv = (the o (parse thy)) "bdv::nat";
582 > val x = (the o (parse thy)) "x::nat";
583 > (instantiate ([(("'a",0),ctyp)],[(bdv,x)]) isolate_bdv_add)
584 handle e => print_exn e;
585 uncaught exception THM
586 raised at: thm.ML:1085.18-1085.69
590 > (instantiate' [SOME ctyp] [] isolate_bdv_add)
591 handle e => print_exn e;
592 uncaught exception TYPE
593 raised at: drule.ML:613.13-615.44
596 > val repct = (rep_cterm o the o (parse ((the o assoc')(!theory',thy')))) "x::rat";
599 (*FIXME 12.8.02: put_asm = true <==> rewrite_inst, rewrite_set_inst
600 thus the argument put_asm IS NOT NECESSARY -- FIXME ~~~~~*)
601 fun rewrite_inst (thy':theory') (rew_ord:rew_ord') (rls:rls')
602 (put_asm:bool) subs (thm:thm') (ct:cterm') =
604 val thy = (the o assoc')(!theory',thy');
605 val thm = assoc_thm' thy thm; (*28.10.02*)
606 (*val subthm = read_instantiate subs ((assoc_thm' thy) thm)*)
609 ((the o assoc')(!rew_ord',rew_ord)) ((#2 o the o assoc')(!ruleset',rls))
610 put_asm (*sub*)thm ((term_of o the o (parse thy)) ct) of
612 | SOME (ctm, ctms) =>
613 SOME ((term2str ctm):cterm', (map term2str ctms):cterm' list)
616 (*FIXME 12.8.02: put_asm = true <==> rewrite_inst, rewrite_set_inst
617 thus the argument put_asm IS NOT NECESSARY -- FIXME ~~~~~*)
618 fun rewrite_set_inst (thy':theory') (put_asm:bool)
619 subs' (rls:rls') (ct:cterm') =
621 val thy = (the o assoc')(!theory',thy');
622 val rls = assoc_rls rls
623 val subst = subs'2subst thy subs'
624 (*val subrls = instantiate_rls subs ((the o assoc')(!ruleset',rls))*)
625 in case rewrite_set_inst_ thy put_asm subst (*sub*)rls
626 ((term_of o the o (parse thy)) ct) of
628 | SOME (t, ts) => SOME (term2str t, terms2str ts)
632 (*vor check_elementwise: SqRoot_eval_rls .. wie *_simplify ?! TODO *)
633 fun eval_true' (thy':theory') (rls':rls') (Const ("True",_)) = true
635 | eval_true' (thy':theory') (rls':rls') (t:term) =
636 (* val thy'="Isac.thy"; val rls'="eval_rls"; val t=hd pres';
638 let val ct' = term2str t;
639 in case rewrite_set thy' false rls' ct' of
640 SOME ("True",_) => true
643 fun eval_true_ _ _ (Const ("True",_)) = true
644 | eval_true_ (thy':theory') rls t =
645 case rewrite_set_ (assoc_thy thy') false rls t of
646 SOME (Const ("True",_),_) => true
651 Rls{preconds = [], rew_ord = ("sqrt_right",sqrt_right),
652 rules = [Calc ("matches",eval_matches "")
654 scr = Script ((term_of o the o (parse thy))
660 rewrite_set_ Isac.thy eval_rls false test_rls
661 ((the o (parse thy)) "matches (?a = ?b) (x = #0)");
662 val xxx = (term_of o the o (parse thy))
663 "matches (?a = ?b) (x = #0)";
664 eval_matches """" xxx thy;
665 SOME ("matches (?a = ?b) (x + #1 + #-1 * #2 = #0) = True",
666 Const ("Trueprop","bool => prop") $ (Const # $ (# $ #) $ Const (#,#)))
670 rewrite_set_ Isac.thy eval_rls false eval_rls
671 ((the o (parse thy)) "contains_root (sqrt #0)");
672 val it = SOME ("True",[]) : (cterm * cterm list) option
677 (*----------WN:16.5.03 stuff below considered illdesigned, thus coded from scratch in appl.sml fun check_elementwise
678 datatype det = TRUE | FALSE | INDET;(*FIXXME.WN:16.5.03
679 introduced with quick-and-dirty code*)
681 let val false_indet =
682 filter_out ((curry op= TRUE) o (#1:det * term -> det)) dts
683 val ts = map (#2: det * term -> term) dts
684 in if nil = false_indet then (TRUE, ts)
685 else if nil = filter ((curry op= FALSE) o (#1:det * term -> det))
688 else (FALSE, ts) end;
689 (* val dts = [(INDET,e_term), (FALSE,HOLogic.false_const),
690 (INDET,e_term), (TRUE,HOLogic.true_const)];
694 [Const ("empty","'a"),Const ("False","bool"),Const ("empty","'a"),
695 Const ("True","bool")]) : det * term list*)
697 fun eval__indet_ thy cs rls = (*FIXXME.WN:16.5.03 pull into eval__true_, update check (check_elementwise), and regard eval_true_ + eval_true*)
698 if cs = [HOLogic.true_const] orelse cs = [] then (TRUE, [])
699 else if cs = [HOLogic.false_const] then (FALSE, cs)
702 let val taopt = rewrite__set_ thy 1 false [] rls t
705 if t = HOLogic.true_const then (TRUE, t)
706 else if t = HOLogic.false_const then (FALSE, t)
708 | NONE => (INDET, t) end
709 in (determine o (map eval)) cs end;
710 WN.16.5.0-------------------------------------------------------------*)