Test_Isac works again, almost ..
4 files raise errors:
# Interpret/solve.sml: "solve.sml: interSteps on norm_Rational 2"
# Interpret/inform.sml: "inform.sml: [rational,simplification] 2"
# Knowledge/partial_fractions.sml: "autoCalculate for met_partial_fraction changed: final result"
# Knowledge/eqsystem.sml: "eqsystem.sml: exp 7.70 normalize 4x4 by rewrite changed"
The chunk of changes is due to the fact, that Isac's code still is unstable.
The changes are accumulated since e8f46493af82.
2 (c) Walther Neuper 2000
4 use"ProgLang/rewrite.sml";
10 exception STOP_REW_SUB; (*WN050820 quick and dirty*)
13 if ! trace_rewrite andalso i < ! depth then tracing (idt "#" i ^ str) else ()
15 if ! trace_rewrite andalso i < ! depth then tracing (idt "#" (i + 1) ^ str) else ()
18 Synopsis rewriting (prep for reference manual):
19 ----------------------------------------------
20 Rewriting uses theorems for transforming terms. However, not all kinds
21 of such transformations can be done by rewriting. Examples are
22 calculation with numerals or cancellation of fractions.
24 Isac tries to present transformations like calculations or cancellation
25 as simple rewrite steps for the naive user. However, some of such
26 transformations should be transparent to the user by single-stepping.
27 For instance, cancellation involves interesting CA algorithms like
28 GCD of multivariate polynomials.
30 Thus Isac has two mechanisms for including SML code, "thm Calc" and "Rrls",
31 the former for steps which are not meant to be inspected by single-stepping
32 the latter meant for single-stepping and providing respective mechanisms.
34 (1) Inclusion by "thm Calc" for 1-step execution
37 (2) Inclusion by "Rrls" for multi-step execution
39 In multi-step execution "reverse rewriting" worked only as passive presentation
40 without any interaction. So the functions init_state, locate_rule etc are just dummies.
42 ? multi-step execution did never work.
43 what worked is "reverse rewriting",
44 i.e. presentation of intermediate steps *without* interaction
46 # type rule and scr | Rfuns
47 # type rrlsstate = (*state for reverse rewriting*)
52 fun rewrite__ thy i bdv tless rls put_asm thm ct =
54 val (t',asms,lrd,rew) =
55 rew_sub thy i bdv tless rls put_asm [(*root of the term*)]
56 (((inst_bdv bdv) o norm o #prop o rep_thm) thm) ct;
57 in if rew then SOME (t', distinct asms)
59 (* one rewrite (possibly conditional, ordered) EXOR exn EXOR go into subterms *)
60 and rew_sub thy i bdv tless rls put_asm lrd r t =
61 ((*tracing ("@@@ rew_sub begin: t = "^(term2str t));
62 tracing ("@@@ rew_sub begin: bdv = "^(PolyML.makestring bdv));
63 tracing ("@@@ rew_sub begin: r = "^(term2str r));*)
64 let (* copy from Pure/thm.ML: fun rewritec *)
65 val (lhs, rhs) = (HOLogic.dest_eq o HOLogic.dest_Trueprop
66 o Logic.strip_imp_concl) r;
67 val r' = Envir.subst_term (Pattern.match thy (lhs, t)
68 (Vartab.empty, Vartab.empty)) r;
69 val p' = map HOLogic.dest_Trueprop ((fst o Logic.strip_prems)
70 (Logic.count_prems r', [], r'));
71 val t' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop
72 o Logic.strip_imp_concl) r';
73 (*val _= tracing("@@@ rew_sub match: t'= "^(term2str t'));*)
74 val _= if ! trace_rewrite andalso i < ! depth andalso p' <> []
75 then tracing((idt"#"(i+1))^" eval asms: "^(term2str r')) else();
76 val (t'',p'') = (*conditional rewriting*)
77 let val (simpl_p', nofalse) = eval__true thy (i+1) p' bdv rls
79 then (if ! trace_rewrite andalso i < ! depth andalso p' <> []
80 then tracing((idt"#"(i+1))^" asms accepted: "^(terms2str p')^
81 " stored: "^(terms2str simpl_p'))
82 else(); (t',simpl_p')) (* uncond.rew. from above*)
84 (if ! trace_rewrite andalso i < ! depth
85 then tracing((idt"#"(i+1))^" asms false: "^(terms2str p'))
86 else(); raise STOP_REW_SUB (*dont go into subterms of cond*))
88 in if perm lhs rhs andalso not (tless bdv (t',t)) (*ordered rewriting*)
89 then (if ! trace_rewrite andalso i < ! depth
90 then tracing((idt"#"i)^" not: \""^
91 (term2str t)^"\" > \""^
92 (term2str t')^"\"") else ();
94 else ((*tracing("##@ rew_sub: (t''= "^(term2str t'')^
95 ", p'' ="^(terms2str p'')^", true)");*)
98 ) handle _ (*NO_REWRITE WN050820 causes diff.behav. in tests + MATCH!*) =>
99 ((*tracing ("@@@ rew_sub gosub: t = "^(term2str t));*)
101 Const(s,T) => (Const(s,T),[],lrd,false)
102 | Free(s,T) => (Free(s,T),[],lrd,false)
103 | Var(n,T) => (Var(n,T),[],lrd,false)
104 | Bound i => (Bound i,[],lrd,false)
106 let val (t', asms, lrd, rew) =
107 rew_sub thy i bdv tless rls put_asm (lrd@[D]) r body
108 in (Abs(s,T,t'), asms, [], rew) end
110 let val (t2', asm2, lrd, rew2) =
111 rew_sub thy i bdv tless rls put_asm (lrd@[R]) r t2
112 in if rew2 then (t1 $ t2', asm2, lrd, true)
113 else let val (t1', asm1, lrd, rew1) =
114 rew_sub thy i bdv tless rls put_asm (lrd@[L]) r t1
115 in if rew1 then (t1' $ t2, asm1, lrd, true)
116 else (t1 $ t2,[], lrd, false) end
118 (* simplify asumptions until one evaluates to false, store intermined's (x~=0)*)
119 and eval__true thy i asms bdv rls =
120 if asms = [@{term True}] orelse asms = [] then ([], true)
121 (* this allows to check Rrls with prepat = ([@{term True}], pat) *)
122 else if asms = [@{term False}] then ([], false) else
124 fun chk indets [] = (indets, true)(*return asms<>True until false*)
125 | chk indets (a::asms) =
126 (case rewrite__set_ thy (i + 1) false bdv rls a of
127 NONE => (chk (indets @ [a]) asms)
129 if t = @{term True} then (chk (indets @ a') asms)
130 else if t = @{term False} then ([], false)
131 (*asm false .. thm not applied ^^^; continue until False vvv*)
132 else chk (indets @ [t] @ a') asms);
134 (* rewrite with a rule set, which must not be the empty Erls *)
135 and rewrite__set_ _ _ __ Erls t =
136 error ("rewrite__set_ called with 'Erls' for '" ^ term2str t ^ "'")
137 (* rewrite with a 'reverse rule set' implemented by ML code *)
138 | rewrite__set_ thy i _ _ (rrls as Rrls _) t =
140 val _= trace i (" rls: " ^ id_rls rrls ^ " on: " ^ term2str t)
141 val (t', asm, rew) = app_rev thy (i + 1) rrls t
142 in if rew then SOME (t', distinct asm) else NONE end
143 (* rewrite with a rule set containing Thms or Calculations *)
144 | rewrite__set_ thy i put_asm bdv rls ct =
146 datatype switch = Appl | Noap;
147 fun rew_once ruls asm ct Noap [] = (ct, asm)
148 | rew_once ruls asm ct Appl [] =
149 (case rls of Rls _ => rew_once ruls asm ct Noap ruls
150 | Seq _ => (ct, asm))
151 | rew_once ruls asm ct apno (rul::thms) =
154 (trace1 i (" try thm: " ^ thmid);
155 case rewrite__ thy (i + 1) bdv ((snd o #rew_ord o rep_rls) rls)
156 ((#erls o rep_rls) rls) put_asm thm ct of
157 NONE => rew_once ruls asm ct apno thms
159 (trace1 i (" rewrites to: " ^ term2str ct');
160 rew_once ruls (union (op =) asm asm') ct' Appl (rul::thms)))
161 | Calc (cc as (op_, _)) =>
162 let val _= trace1 i (" try calc: " ^ op_ ^ "'")
163 val ct = uminus_to_string ct
164 in case get_calculation_ thy cc ct of
165 NONE => rew_once ruls asm ct apno thms
166 | SOME (thmid, thm') =>
168 val pairopt = rewrite__ thy (i + 1) bdv ((snd o #rew_ord o rep_rls) rls)
169 ((#erls o rep_rls) rls) put_asm thm' ct;
170 val _ = if pairopt <> NONE then () else error ("rewrite_set_, rewrite_ \"" ^
171 string_of_thmI thm' ^ "\" " ^ term2str ct ^ " = NONE")
172 val _ = trace1 i (" calc. to: " ^ term2str ((fst o the) pairopt))
173 in rew_once ruls asm ((fst o the) pairopt) Appl (rul :: thms) end
175 | Cal1 (cc as (op_, _)) =>
176 let val _= trace1 i (" try cal1: " ^ op_ ^ "'");
177 val ct = uminus_to_string ct
178 in case get_calculation1_ thy cc ct of
180 | SOME (thmid, thm') =>
182 val pairopt = rewrite__ thy (i + 1) bdv ((snd o #rew_ord o rep_rls) rls)
183 ((#erls o rep_rls) rls) put_asm thm' ct;
184 val _ = if pairopt <> NONE then () else error ("rewrite_set_, rewrite_ \"" ^
185 string_of_thmI thm' ^ "\" " ^ term2str ct ^ " = NONE")
186 val _ = trace1 i (" cal1. to: " ^ term2str ((fst o the) pairopt))
190 (case rewrite__set_ thy (i + 1) put_asm bdv rls' ct of
191 SOME (t', asm') => rew_once ruls (union (op =) asm asm') t' Appl thms
192 | NONE => rew_once ruls asm ct apno thms);
193 val ruls = (#rules o rep_rls) rls;
194 val _= trace i (" rls: " ^ id_rls rls ^ " on: " ^ term2str ct)
195 val (ct', asm') = rew_once ruls [] ct Noap ruls;
196 in if ct = ct' then NONE else SOME (ct', distinct asm') end
198 (* apply an Rrls; if not applicable proceed with subterms *)
199 and app_rev thy i rrls t =
200 let (* check a (precond, pattern) of a rev-set; stops with 1st true *)
201 fun chk_prepat thy erls [] t = true
202 | chk_prepat thy erls prepat t =
204 fun chk (pres, pat) =
206 val subst: Type.tyenv * Envir.tenv =
207 Pattern.match thy (pat, t) (Vartab.empty, Vartab.empty)
209 snd (eval__true thy (i + 1) (map (Envir.subst_term subst) pres) [] erls)
210 end) handle _ => false
211 fun scan_ f [] = false (*scan_ NEVER called by []*)
212 | scan_ f (pp::pps) =
213 if f pp then true else scan_ f pps;
214 in scan_ chk prepat end;
215 (* apply the normal_form of a rev-set *)
216 fun app_rev' thy (Rrls {erls, prepat, scr = Rfuns {normal_form, ...}, ...}) t =
217 if chk_prepat thy erls prepat t
218 then ((*tracing("### app_rev': t = "^(term2str t));*) normal_form t)
220 val opt = app_rev' thy rrls t
223 SOME (t', asm) => (t', asm, true)
224 | NONE => app_sub thy i rrls t
227 (* apply an Rrls to subterms *)
228 and app_sub thy i rrls t =
229 ((*tracing("### app_sub: subterm = "^(term2str t));*)
231 Const (s, T) => (Const(s, T), [], false)
232 | Free (s, T) => (Free(s, T), [], false)
233 | Var (n, T) => (Var(n, T), [], false)
234 | Bound i => (Bound i, [], false)
235 | Abs (s, T, body) =>
236 let val (t', asm, rew) = app_rev thy i rrls body
237 in (Abs(s, T, t'), asm, rew) end
239 let val (t2', asm2, rew2) = app_rev thy i rrls t2
241 if rew2 then (t1 $ t2', asm2, true)
243 let val (t1', asm1, rew1) = app_rev thy i rrls t1
244 in if rew1 then (t1' $ t2, asm1, true)
245 else (t1 $ t2, [], false)
251 (*.rewriting without argument [] for rew_ord.*)
252 (*WN.11.6.03: shouldnt asm<>[] lead to false ????*)
253 fun eval_true thy terms rls = (snd o (eval__true thy 1 terms [])) rls;
255 (* rewriting without internal argument [] *)
256 fun rewrite_ thy rew_ord erls bool thm term = rewrite__ thy 1 [] rew_ord erls bool thm term;
257 fun rewrite_set_ thy bool rls term = rewrite__set_ thy 1 bool [] rls term;
259 fun subs'2subst thy (s:subs') =
260 (((map (apfst (term_of o the o (parse thy))))
261 o (map (apsnd (term_of o the o (parse thy))))) s):subst;
263 (*.variants of rewrite.*)
264 (*FIXME 12.8.02: put_asm = true <==> rewrite_inst,
265 thus the argument put_asm IS NOT NECESSARY -- FIXME*)
266 (* val (rew_ord,rls,put_asm,thm,ct)=
267 (e_rew_ord,poly_erls,false,num_str d1_isolate_add2,t);
269 fun rewrite_inst_ (thy:theory) rew_ord (rls:rls) (put_asm:bool)
270 (subst:(term * term) list) (thm:thm) (ct:term) =
271 rewrite__ thy 1 subst rew_ord rls put_asm thm ct;
273 fun rewrite_set_inst_ (thy:theory)
274 (put_asm:bool) (subst:(term * term) list) (rls:rls) (ct:term) =
276 val subst = subs'2subst thy subs';
277 val subrls = instantiate_rls subs' rls
278 in*) rewrite__set_ thy 1 put_asm subst (*sub*)rls ct
281 (* given a list of equalities (lhs = rhs) and a term,
282 replace all occurrences of lhs in the term with rhs;
283 thus the order or equalities matters: put variables in lhs first. *)
284 fun rewrite_terms_ thy ord erls equs t =
286 fun rew_ (t', asm') [] _ = (t', asm')
287 | rew_ (t', asm') (rules as r::rs) t =
289 val (t'', asm'', lrd, rew) = rew_sub thy 1 [] ord erls false [] (Trueprop $ r) t
292 then rew_ (t'', asm' @ asm'') rules t''
293 else rew_ (t', asm') rs t'
295 val (t'', asm'') = rew_ (e_term, []) equs t
296 in if t'' = e_term then NONE else SOME (t'', asm'')
299 (*. search ct for adjacent numerals and calculate them by operator isa_fn .*)
300 fun calculate_ thy isa_fn ct =
301 let val ct = uminus_to_string ct
302 in case get_calculation_ thy isa_fn ct of
304 | SOME (thmID, thm) =>
305 (let val SOME (rew,_) = rewrite_ thy dummy_ord e_rls false thm ct
306 in SOME (rew,(thmID, thm)) end)
307 handle _ => error ("calculate_: "^thmID^" does not rewrite")
310 > val thy = InsSort.thy;
311 > val op_ = "le"; (* < *)
312 > val ct = (the o (parse thy))
313 "foldr ins [#2] (if #1 < #3 then #1 # ins [] #3 else [#3, #1])";
314 > calculate_ thy op_ ct;
316 ("foldr ins [#2] (if True then #1 # ins [] #3 else [#3, #1])",
317 "(#1 < #3) = True") : (cterm * thm) option *)
319 fun get_rls_scr rs' = ((#scr o rep_rls o #2 o the o assoc') (!ruleset',rs'))
320 handle _ => error ("get_rls_scr: no script for "^rs');
323 (*make_thm added to Pure/thm.ML*)
325 let val t = (term_of o the o (parse thy)) str
327 Const ("==>",_) $ _ $ _ => t
329 in make_thm (cterm_of thy t') end;
331 val str = "?r ^^^ 2 = ?r * ?r";
332 val thm = realpow_twoI;
334 val t1 = (#prop o rep_thm) (num_str thm);
335 val t2 = Trueprop $ ((term_of o the o (parse thy)) str);
337 val it = true : bool ... !!!
338 val th1 = (num_str thm);
339 val th2 = ((*num_str*) (mk_thm thy str)) handle e => print_exn e;
341 ML> val it = false : bool ... HIDDEN DIFFERENCES IRRELEVANT FOR ISAC ?!
343 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
344 val str = "k ~= 0 ==> m * k / (n * k) = m / n";
345 val thm = real_mult_div_cancel2;
347 val t1 = (#prop o rep_thm) (num_str thm);
348 val t2 = ((term_of o the o (parse thy)) str);
350 val it = false : bool ... Var .. Free
351 val th1 = (num_str thm);
352 val th2 = ((*num_str*) (mk_thm thy str)) handle e => print_exn e;
354 ML> val it = false : bool ... PLUS HIDDEN DIFFERENCES IRRELEVANT FOR ISAC ?!
358 (*prints subgoal etc.
359 ((goal thy);(topthm()) o ) str; *)
360 (*assume rejects scheme variables
361 assume ((cterm_of thy) (Trueprop $
362 (term_of o the o (parse thy)) str)); *)
365 (* outcommented 18.11.xx, xx < 02 -------
366 fun rul2rul' (Thm (thmid, thm)) = Thm'(thmid, string_of_thmI thm)
367 | rul2rul' (Calc op_) = Calc' op_;
368 fun rul'2rul thy (Thm'(thmid, ct')) =
369 Thm (thmid, mk_thm thy ct')
370 | rul'2rul thy' (Calc' op_) = Calc op_;
373 fun rls2rls' (Rls{preconds=preconds,rew_ord=rew_ord,rules=rules}:rls) =
374 Rls'{preconds'= map string_of_cterm preconds,
375 rew_ord' = fst rew_ord,
376 rules' = map rul2rul' rules}:rlsdat';
378 fun rls'2rls thy' (Rls'{preconds'=preconds,rew_ord'=rew_ord,
379 rules'=rules}:rlsdat') =
380 let val thy = assoc_thy thy';
381 in Rls{preconds = map (the o (parse thy)) preconds,
382 rew_ord = (rew_ord, the (assoc'(rew_ord',rew_ord))),
383 rules = map (rul'2rul thy) rules}:rls end;
386 (*.get the theorem associated with the xstring-identifier;
387 if the identifier starts with "sym_" then swap lhs = rhs around =
388 (ATTENTION: "RS sym" attaches a [.] -- remove it with string_of_thmI);
389 identifiers starting with "#" come from Calc and
390 get a hand-made theorem (containing numerals only).*)
391 fun assoc_thm' (thy:theory) ((thmid, ct'):thm') =
392 (case Symbol.explode thmid of
393 "s"::"y"::"m"::"_"::id =>
396 else ((num_str o (Global_Theory.get_thm thy)) (implode id)) RS sym
400 else (num_str o (Global_Theory.get_thm thy)) thmid
402 error ("assoc_thm': '"^thmid^"' not in '"^
403 (theory2domID thy)^"' (and parents)");
404 (*> assoc_thm' (Thy_Info.get_theory "Isac") ("sym_#mult_2_3","6 = 2 * 3");
405 val it = "6 = 2 * 3" : thm
407 > assoc_thm' (Thy_Info.get_theory "Isac") ("add_0_left","");
408 val it = "0 + ?z = ?z" : thm
410 > assoc_thm' (Thy_Info.get_theory "Isac") ("sym_real_add_zero_left","");
411 val it = "?t = 0 + ?t" [.] : thm
413 > assoc_thm' HOL.thy ("sym_real_add_zero_left","");
414 *** Unknown theorem(s) "add_0_left"
415 *** assoc_thm': 'sym_real_add_zero_left' not in 'HOL.thy' (and parents)
416 uncaught exception ERROR*)
419 fun parse' (thy:theory') (ct:cterm') =
420 case parse (assoc_thy thy) ct of
422 | SOME ct => SOME ((term2str (term_of ct)):cterm');
425 (*FIXME 12.8.02: put_asm = true <==> rewrite_inst, rewrite_set_inst
426 thus the argument put_asm IS NOT NECESSARY -- FIXME ~~~~~*)
427 fun rewrite (thy':theory') (rew_ord:rew_ord') (rls:rls')
428 (put_asm:bool) (thm:thm') (ct:cterm') =
429 (* val (rew_ord, rls, thm, ct) = (rew_ord', id_rls rls', thm', f);
431 let val thy = assoc_thy thy';
434 ((the o assoc')(!rew_ord',rew_ord))((#2 o the o assoc')(!ruleset',rls))
435 put_asm ((assoc_thm' thy) thm)
436 ((term_of o the o (parse thy)) ct) of
438 | SOME (t, ts) => SOME (term2str t, terms2str ts)
442 val thy = "RatArith";
443 val rew_ord = "dummy_ord";
444 > val rls = "eval_rls";
446 val thm = ("square_equation_left","");
447 val ct = "sqrt(#9+#4*x)=sqrt x + sqrt(#-3+x)";
449 val Zthy = assoc_thy thy;
450 val Zrew_ord = ((the o assoc')(!rew_ord',rew_ord));
451 val Zrls = ((the o assoc')(!ruleset',rls));
452 val Zput_asm = put_asm;
453 val Zthm = ((the o (assoc'_thm' thy)) thm);
454 val Zct = ((the o (parse (assoc_thy thy))) ct);
456 rewrite_ Zthy Zrew_ord Zrls Zput_asm Zthm Zct;
458 use"Isa99/interface_ME_ISA.sml";
461 (*FIXME 12.8.02: put_asm = true <==> rewrite_inst, rewrite_set_inst
462 thus the argument put_asm IS NOT NECESSARY -- FIXME ~~~~~*)
463 fun rewrite_set (thy':theory') (put_asm:bool)
464 (rls:rls') (ct:cterm') =
465 let val thy = (assoc_thy thy');
467 case rewrite_set_ thy put_asm ((#2 o the o assoc')(!ruleset',rls))
468 ((term_of o the o (parse thy)) ct) of
470 | SOME (t, ts) => SOME (term2str t, terms2str ts)
473 (*evaluate list-expressions
474 should work on term, and stand in Isa99/rewrite-parse.sml,
475 but there list_rls <- eval_binop is not yet defined*)
476 (*fun eval_listexpr' ct =
477 let val rew = rewrite_set "ListC" false "list_rls" ct;
480 | NONE => ct end;-----------------30.9.02---*)
481 fun eval_listexpr_ thy srls t =
482 (* val (thy, srls, t) =
483 ((assoc_thy th), sr, (subst_atomic (upd_env_opt E (a,v)) t));
485 let val rew = rewrite_set_ thy false srls t;
491 fun get_calculation' (thy:theory') op_ (ct:cterm') =
492 case get_calculation_ (assoc_thy thy) op_
493 ((uminus_to_string o term_of o the o
494 (parse (assoc_thy thy))) ct) of
496 | SOME (thmid, thm) =>
497 SOME ((thmid, string_of_thmI thm):thm');
499 fun calculate (thy':theory') op_ (ct:cterm') =
500 let val thy = (assoc_thy thy');
502 case calculate_ thy op_
503 ((term_of o the o (parse thy)) ct) of
505 | SOME (ct,(thmID,thm)) =>
507 (thmID, string_of_thmI thm):thm')
510 fun instantiate'' thy' subs ((thmid,ct'):thm') =
511 let val thmid_ = implode ("#"::(Symbol.explode thmid)) (*see type thm'*)
512 in (thmid_, (string_of_thmI o (read_instantiate subs))
513 ((the o (assoc_thm' thy')) (thmid_,ct'))):thm' end;
515 fun instantiate_rls' thy' subs (rls:rls') =
516 rls2rls' (instantiate_rls subs ((the o (assoc_rls thy')) rls)):rlsdat';
518 ... problem with these functions:
519 > val thm = mk_thm thy "(bdv + a = b) = (bdv = b - a)";
520 val thm = "(bdv + a = b) = (bdv = b - a)" : thm
521 > show_types:=true; thm;
522 val it = "((bdv::'a) + (a::'a) = (b::'a)) = (bdv = b - a)" : thm
523 ... and this doesn't match because of too general typing (?!)
524 and read_insitantiate doesn't instantiate the types (?!)
526 (1) hard-coded type-instantiation ("'a", "RatArith.rat")
527 (2) instantiate', instantiate ... no help by isabelle-users@ !!!
529 rewrite_inst, rewrite_set_inst circumvent the problem,
530 according functions out-commented with 'instantiate''
534 fun instantiate'' thy' subs ((thmid,ct'):thm') =
536 val thmid_ = implode ("#"::(Symbol.explode thmid)); (*see type thm'*)
537 val thy = assoc_thy thy';
538 val typs = map (#T o rep_cterm o the o (parse thy))
539 ((snd o split_list) subs);
541 ((ctyp_of (sign_of thy)) o #T o rep_cterm o the o (parse thy))
542 ((snd o split_list) subs);
544 > val thy' = "RatArith";
545 > val subs = [("bdv","x::rat"),("zzz","z::nat")];
546 > (the o (parse (assoc_thy thy'))) "x::rat";
547 > (#T o rep_cterm o the o (parse (assoc_thy thy')));
549 > val ctyp = ((ctyp_of (sign_of thy)) o #T o rep_cterm o the o
550 (parse (assoc_thy thy'))) "x::rat";
551 > val bdv = (the o (parse thy)) "bdv";
552 > val x = (the o (parse thy)) "x";
553 > (instantiate ([(("'a",0),ctyp)],[(bdv,x)]) isolate_bdv_add)
554 handle e => print_exn e;
555 uncaught exception THM
556 raised at: thm.ML:1085.18-1085.69
560 > val bdv = (the o (parse thy)) "bdv::nat";
561 > val x = (the o (parse thy)) "x::nat";
562 > (instantiate ([(("'a",0),ctyp)],[(bdv,x)]) isolate_bdv_add)
563 handle e => print_exn e;
564 uncaught exception THM
565 raised at: thm.ML:1085.18-1085.69
569 > (instantiate' [SOME ctyp] [] isolate_bdv_add)
570 handle e => print_exn e;
571 uncaught exception TYPE
572 raised at: drule.ML:613.13-615.44
575 > val repct = (rep_cterm o the o (parse ((the o assoc')(!theory',thy')))) "x::rat";
578 (*FIXME 12.8.02: put_asm = true <==> rewrite_inst, rewrite_set_inst
579 thus the argument put_asm IS NOT NECESSARY -- FIXME ~~~~~*)
580 fun rewrite_inst (thy':theory') (rew_ord:rew_ord') (rls:rls')
581 (put_asm:bool) subs (thm:thm') (ct:cterm') =
583 val thy = assoc_thy thy';
584 val thm = assoc_thm' thy thm; (*28.10.02*)
585 (*val subthm = read_instantiate subs ((assoc_thm' thy) thm)*)
588 ((the o assoc')(!rew_ord',rew_ord)) ((#2 o the o assoc')(!ruleset',rls))
589 put_asm (*sub*)thm ((term_of o the o (parse thy)) ct) of
591 | SOME (ctm, ctms) =>
592 SOME ((term2str ctm):cterm', (map term2str ctms):cterm' list)
595 (*FIXME 12.8.02: put_asm = true <==> rewrite_inst, rewrite_set_inst
596 thus the argument put_asm IS NOT NECESSARY -- FIXME ~~~~~*)
597 fun rewrite_set_inst (thy':theory') (put_asm:bool)
598 subs' (rls:rls') (ct:cterm') =
600 val thy = assoc_thy thy';
601 val rls = assoc_rls rls
602 val subst = subs'2subst thy subs'
603 (*val subrls = instantiate_rls subs ((the o assoc')(!ruleset',rls))*)
604 in case rewrite_set_inst_ thy put_asm subst (*sub*)rls
605 ((term_of o the o (parse thy)) ct) of
607 | SOME (t, ts) => SOME (term2str t, terms2str ts)
611 (*vor check_elementwise: SqRoot_eval_rls .. wie *_simplify ?! TODO *)
612 fun eval_true' (thy':theory') (rls':rls') (Const ("HOL.True",_)) = true
614 | eval_true' (thy':theory') (rls':rls') (t:term) =
615 (* val thy'="Isac"; val rls'="eval_rls"; val t=hd pres';
617 let val ct' = term2str t;
618 in case rewrite_set thy' false rls' ct' of
619 SOME ("HOL.True",_) => true
622 fun eval_true_ _ _ (Const ("HOL.True",_)) = true
623 | eval_true_ (thy':theory') rls t =
624 case rewrite_set_ (assoc_thy thy') false rls t of
625 SOME (Const ("HOL.True",_),_) => true
630 Rls{preconds = [], rew_ord = ("sqrt_right",sqrt_right),
631 rules = [Calc ("matches",eval_matches "")
633 scr = Prog ((term_of o the o (parse thy))
639 rewrite_set_ (Thy_Info.get_theory "Isac") eval_rls false test_rls
640 ((the o (parse thy)) "matches (?a = ?b) (x = #0)");
641 val xxx = (term_of o the o (parse thy))
642 "matches (?a = ?b) (x = #0)";
643 eval_matches """" xxx thy;
644 SOME ("matches (?a = ?b) (x + #1 + #-1 * #2 = #0) = True",
645 Const ("HOL.Trueprop","bool => prop") $ (Const # $ (# $ #) $ Const (#,#)))
649 rewrite_set_ (Thy_Info.get_theory "Isac") eval_rls false eval_rls
650 ((the o (parse thy)) "contains_root (sqrt #0)");
651 val it = SOME ("HOL.True",[]) : (cterm * cterm list) option
656 (*----------WN:16.5.03 stuff below considered illdesigned, thus coded from scratch in appl.sml fun check_elementwise
657 datatype det = TRUE | FALSE | INDET;(*FIXXME.WN:16.5.03
658 introduced with quick-and-dirty code*)
660 let val false_indet =
661 filter_out ((curry op= TRUE) o (#1:det * term -> det)) dts
662 val ts = map (#2: det * term -> term) dts
663 in if nil = false_indet then (TRUE, ts)
664 else if nil = filter ((curry op= FALSE) o (#1:det * term -> det))
667 else (FALSE, ts) end;
668 (* val dts = [(INDET,e_term), (FALSE,@{term False}),
669 (INDET,e_term), (TRUE,@{term True})];
673 [Const ("empty","'a"),Const ("HOL.False","bool"),Const ("empty","'a"),
674 Const ("HOL.True","bool")]) : det * term list*)
676 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*)
677 if cs = [@{term True}] orelse cs = [] then (TRUE, [])
678 else if cs = [@{term False}] then (FALSE, cs)
681 let val taopt = rewrite__set_ thy 1 false [] rls t
684 if t = @{term True} then (TRUE, t)
685 else if t = @{term False} then (FALSE, t)
687 | NONE => (INDET, t) end
688 in (determine o (map eval)) cs end;
689 WN.16.5.0-------------------------------------------------------------*)