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 then normal_form t else NONE;
218 val opt = app_rev' thy rrls t
221 SOME (t', asm) => (t', asm, true)
222 | NONE => app_sub thy i rrls t
225 (* apply an Rrls to subterms *)
226 and app_sub thy i rrls t =
227 ((*tracing("### app_sub: subterm = "^(term2str t));*)
229 Const (s, T) => (Const(s, T), [], false)
230 | Free (s, T) => (Free(s, T), [], false)
231 | Var (n, T) => (Var(n, T), [], false)
232 | Bound i => (Bound i, [], false)
233 | Abs (s, T, body) =>
234 let val (t', asm, rew) = app_rev thy i rrls body
235 in (Abs(s, T, t'), asm, rew) end
237 let val (t2', asm2, rew2) = app_rev thy i rrls t2
239 if rew2 then (t1 $ t2', asm2, true)
241 let val (t1', asm1, rew1) = app_rev thy i rrls t1
242 in if rew1 then (t1' $ t2, asm1, true)
243 else (t1 $ t2, [], false)
249 (*.rewriting without argument [] for rew_ord.*)
250 (*WN.11.6.03: shouldnt asm<>[] lead to false ????*)
251 fun eval_true thy terms rls = (snd o (eval__true thy 1 terms [])) rls;
253 (* rewriting without internal argument [] *)
254 fun rewrite_ thy rew_ord erls bool thm term = rewrite__ thy 1 [] rew_ord erls bool thm term;
255 fun rewrite_set_ thy bool rls term = rewrite__set_ thy 1 bool [] rls term;
257 fun subs'2subst thy (s:subs') =
258 (((map (apfst (term_of o the o (parse thy))))
259 o (map (apsnd (term_of o the o (parse thy))))) s):subst;
261 (*.variants of rewrite.*)
262 (*FIXME 12.8.02: put_asm = true <==> rewrite_inst,
263 thus the argument put_asm IS NOT NECESSARY -- FIXME*)
264 (* val (rew_ord,rls,put_asm,thm,ct)=
265 (e_rew_ord,poly_erls,false,num_str d1_isolate_add2,t);
267 fun rewrite_inst_ (thy:theory) rew_ord (rls:rls) (put_asm:bool)
268 (subst:(term * term) list) (thm:thm) (ct:term) =
269 rewrite__ thy 1 subst rew_ord rls put_asm thm ct;
271 fun rewrite_set_inst_ (thy:theory)
272 (put_asm:bool) (subst:(term * term) list) (rls:rls) (ct:term) =
274 val subst = subs'2subst thy subs';
275 val subrls = instantiate_rls subs' rls
276 in*) rewrite__set_ thy 1 put_asm subst (*sub*)rls ct
279 (* given a list of equalities (lhs = rhs) and a term,
280 replace all occurrences of lhs in the term with rhs;
281 thus the order or equalities matters: put variables in lhs first. *)
282 fun rewrite_terms_ thy ord erls equs t =
284 fun rew_ (t', asm') [] _ = (t', asm')
285 | rew_ (t', asm') (rules as r::rs) t =
287 val (t'', asm'', lrd, rew) = rew_sub thy 1 [] ord erls false [] (Trueprop $ r) t
290 then rew_ (t'', asm' @ asm'') rules t''
291 else rew_ (t', asm') rs t'
293 val (t'', asm'') = rew_ (e_term, []) equs t
294 in if t'' = e_term then NONE else SOME (t'', asm'')
297 (*. search ct for adjacent numerals and calculate them by operator isa_fn .*)
298 fun calculate_ thy isa_fn ct =
299 let val ct = uminus_to_string ct
300 in case get_calculation_ thy isa_fn ct of
302 | SOME (thmID, thm) =>
303 (let val SOME (rew,_) = rewrite_ thy dummy_ord e_rls false thm ct
304 in SOME (rew,(thmID, thm)) end)
305 handle _ => error ("calculate_: "^thmID^" does not rewrite")
308 > val thy = InsSort.thy;
309 > val op_ = "le"; (* < *)
310 > val ct = (the o (parse thy))
311 "foldr ins [#2] (if #1 < #3 then #1 # ins [] #3 else [#3, #1])";
312 > calculate_ thy op_ ct;
314 ("foldr ins [#2] (if True then #1 # ins [] #3 else [#3, #1])",
315 "(#1 < #3) = True") : (cterm * thm) option *)
317 fun get_rls_scr rls' = ((#scr o rep_rls o assoc_rls) rls')
318 handle _ => error ("get_rls_scr: no script for " ^ rls');
320 (*make_thm added to Pure/thm.ML*)
322 let val t = (term_of o the o (parse thy)) str
324 Const ("==>",_) $ _ $ _ => t
326 in make_thm (cterm_of thy t') end;
328 val str = "?r ^^^ 2 = ?r * ?r";
329 val thm = realpow_twoI;
331 val t1 = (#prop o rep_thm) (num_str thm);
332 val t2 = Trueprop $ ((term_of o the o (parse thy)) str);
334 val it = true : bool ... !!!
335 val th1 = (num_str thm);
336 val th2 = ((*num_str*) (mk_thm thy str)) handle e => print_exn e;
338 ML> val it = false : bool ... HIDDEN DIFFERENCES IRRELEVANT FOR ISAC ?!
340 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
341 val str = "k ~= 0 ==> m * k / (n * k) = m / n";
342 val thm = real_mult_div_cancel2;
344 val t1 = (#prop o rep_thm) (num_str thm);
345 val t2 = ((term_of o the o (parse thy)) str);
347 val it = false : bool ... Var .. Free
348 val th1 = (num_str thm);
349 val th2 = ((*num_str*) (mk_thm thy str)) handle e => print_exn e;
351 ML> val it = false : bool ... PLUS HIDDEN DIFFERENCES IRRELEVANT FOR ISAC ?!
355 (*prints subgoal etc.
356 ((goal thy);(topthm()) o ) str; *)
357 (*assume rejects scheme variables
358 assume ((cterm_of thy) (Trueprop $
359 (term_of o the o (parse thy)) str)); *)
362 (* outcommented 18.11.xx, xx < 02 -------
363 fun rul2rul' (Thm (thmid, thm)) = Thm'(thmid, string_of_thmI thm)
364 | rul2rul' (Calc op_) = Calc' op_;
365 fun rul'2rul thy (Thm'(thmid, ct')) =
366 Thm (thmid, mk_thm thy ct')
367 | rul'2rul thy' (Calc' op_) = Calc op_;
370 fun rls2rls' (Rls{preconds=preconds,rew_ord=rew_ord,rules=rules}:rls) =
371 Rls'{preconds'= map string_of_cterm preconds,
372 rew_ord' = fst rew_ord,
373 rules' = map rul2rul' rules}:rlsdat';
375 fun rls'2rls thy' (Rls'{preconds'=preconds,rew_ord'=rew_ord,
376 rules'=rules}:rlsdat') =
377 let val thy = assoc_thy thy';
378 in Rls{preconds = map (the o (parse thy)) preconds,
379 rew_ord = (rew_ord, the (assoc'(rew_ord',rew_ord))),
380 rules = map (rul'2rul thy) rules}:rls end;
383 (*.get the theorem associated with the xstring-identifier;
384 if the identifier starts with "sym_" then swap lhs = rhs around =
385 (ATTENTION: "RS sym" attaches a [.] -- remove it with string_of_thmI);
386 identifiers starting with "#" come from Calc and
387 get a hand-made theorem (containing numerals only).*)
388 fun assoc_thm' (thy:theory) ((thmid, ct'):thm') =
389 (case Symbol.explode thmid of
390 "s"::"y"::"m"::"_"::id =>
393 else ((num_str o (Global_Theory.get_thm thy)) (implode id)) RS sym
397 else (num_str o (Global_Theory.get_thm thy)) thmid
399 error ("assoc_thm': \"" ^ thmid ^ "\" not in \"" ^ theory2domID thy ^ "\" (and parents)")
400 (*> assoc_thm' (Thy_Info.get_theory "Isac") ("sym_#mult_2_3","6 = 2 * 3");
401 val it = "6 = 2 * 3" : thm
403 > assoc_thm' (Thy_Info.get_theory "Isac") ("add_0_left","");
404 val it = "0 + ?z = ?z" : thm
406 > assoc_thm' (Thy_Info.get_theory "Isac") ("sym_real_add_zero_left","");
407 val it = "?t = 0 + ?t" [.] : thm
409 > assoc_thm' @{theory HOL} ("sym_real_add_zero_left","");
410 *** Unknown theorem(s) "add_0_left"
411 *** assoc_thm': 'sym_real_add_zero_left' not in 'HOL.thy' (and parents)
412 uncaught exception ERROR*)
415 fun parse' (thy:theory') (ct:cterm') =
416 case parse (assoc_thy thy) ct of
418 | SOME ct => SOME ((term2str (term_of ct)):cterm');
421 (*FIXME 12.8.02: put_asm = true <==> rewrite_inst, rewrite_set_inst
422 thus the argument put_asm IS NOT NECESSARY -- FIXME ~~~~~*)
423 fun rewrite (thy':theory') (rew_ord:rew_ord') (rls:rls') (put_asm:bool) (thm:thm') (ct:cterm') =
424 let val thy = assoc_thy thy';
426 case rewrite_ thy ((the o assoc')(!rew_ord',rew_ord))(assoc_rls rls)
427 put_asm ((assoc_thm' thy) thm) ((term_of o the o (parse thy)) ct) of
429 | SOME (t, ts) => SOME (term2str t, terms2str ts)
432 (*FIXME 12.8.02: put_asm = true <==> rewrite_inst, rewrite_set_inst
433 thus the argument put_asm IS NOT NECESSARY -- FIXME ~~~~~*)
434 fun rewrite_set (thy':theory') (put_asm:bool) (rls:rls') (ct:cterm') =
435 let val thy = (assoc_thy thy');
437 case rewrite_set_ thy put_asm (assoc_rls rls) ((term_of o the o (parse thy)) ct) of
439 | SOME (t, ts) => SOME (term2str t, terms2str ts)
442 fun eval_listexpr_ thy srls t =
443 let val rew = rewrite_set_ thy false srls t;
444 in case rew of SOME (res,_) => res | NONE => t end;
446 fun get_calculation' (thy:theory') op_ (ct:cterm') =
447 case get_calculation_ (assoc_thy thy) op_
448 ((uminus_to_string o term_of o the o
449 (parse (assoc_thy thy))) ct) of
451 | SOME (thmid, thm) =>
452 SOME ((thmid, string_of_thmI thm):thm');
454 fun calculate (thy':theory') op_ (ct:cterm') =
455 let val thy = (assoc_thy thy');
457 case calculate_ thy op_
458 ((term_of o the o (parse thy)) ct) of
460 | SOME (ct,(thmID,thm)) =>
462 (thmID, string_of_thmI thm):thm')
465 (*FIXME 12.8.02: put_asm = true <==> rewrite_inst, rewrite_set_inst
466 thus the argument put_asm IS NOT NECESSARY -- FIXME ~~~~~*)
467 fun rewrite_inst (thy':theory') (rew_ord:rew_ord') (rls:rls')
468 (put_asm:bool) subs (thm:thm') (ct:cterm') =
470 val thy = assoc_thy thy';
471 val thm = assoc_thm' thy thm; (*28.10.02*)
472 (*val subthm = read_instantiate subs ((assoc_thm' thy) thm)*)
475 ((the o assoc')(!rew_ord',rew_ord)) (assoc_rls rls)
476 put_asm (*sub*)thm ((term_of o the o (parse thy)) ct) of
478 | SOME (ctm, ctms) =>
479 SOME ((term2str ctm):cterm', (map term2str ctms):cterm' list)
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_inst (thy':theory') (put_asm:bool)
485 subs' (rls:rls') (ct:cterm') =
487 val thy = assoc_thy thy';
488 val rls = assoc_rls rls
489 val subst = subs'2subst thy subs'
490 in case rewrite_set_inst_ thy put_asm subst (*sub*)rls
491 ((term_of o the o (parse thy)) ct) of
493 | SOME (t, ts) => SOME (term2str t, terms2str ts)
497 (*vor check_elementwise: SqRoot_eval_rls .. wie *_simplify ?! TODO *)
498 fun eval_true' (thy':theory') (rls':rls') (Const ("HOL.True",_)) = true
500 | eval_true' (thy':theory') (rls':rls') (t:term) =
501 (* val thy'="Isac"; val rls'="eval_rls"; val t=hd pres';
503 let val ct' = term2str t;
504 in case rewrite_set thy' false rls' ct' of
505 SOME ("HOL.True",_) => true
508 fun eval_true_ _ _ (Const ("HOL.True",_)) = true
509 | eval_true_ (thy':theory') rls t =
510 case rewrite_set_ (assoc_thy thy') false rls t of
511 SOME (Const ("HOL.True",_),_) => true
516 Rls{preconds = [], rew_ord = ("sqrt_right",sqrt_right),
517 rules = [Calc ("matches",eval_matches "")
519 scr = Prog ((term_of o the o (parse thy))
525 rewrite_set_ (Thy_Info.get_theory "Isac") eval_rls false test_rls
526 ((the o (parse thy)) "matches (?a = ?b) (x = #0)");
527 val xxx = (term_of o the o (parse thy))
528 "matches (?a = ?b) (x = #0)";
529 eval_matches """" xxx thy;
530 SOME ("matches (?a = ?b) (x + #1 + #-1 * #2 = #0) = True",
531 Const ("HOL.Trueprop","bool => prop") $ (Const # $ (# $ #) $ Const (#,#)))
535 rewrite_set_ (Thy_Info.get_theory "Isac") eval_rls false eval_rls
536 ((the o (parse thy)) "contains_root (sqrt #0)");
537 val it = SOME ("HOL.True",[]) : (cterm * cterm list) option
542 (*----------WN:16.5.03 stuff below considered illdesigned, thus coded from scratch in appl.sml fun check_elementwise
543 datatype det = TRUE | FALSE | INDET;(*FIXXME.WN:16.5.03
544 introduced with quick-and-dirty code*)
546 let val false_indet =
547 filter_out ((curry op= TRUE) o (#1:det * term -> det)) dts
548 val ts = map (#2: det * term -> term) dts
549 in if nil = false_indet then (TRUE, ts)
550 else if nil = filter ((curry op= FALSE) o (#1:det * term -> det))
553 else (FALSE, ts) end;
554 (* val dts = [(INDET,e_term), (FALSE,@{term False}),
555 (INDET,e_term), (TRUE,@{term True})];
559 [Const ("empty","'a"),Const ("HOL.False","bool"),Const ("empty","'a"),
560 Const ("HOL.True","bool")]) : det * term list*)
562 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*)
563 if cs = [@{term True}] orelse cs = [] then (TRUE, [])
564 else if cs = [@{term False}] then (FALSE, cs)
567 let val taopt = rewrite__set_ thy 1 false [] rls t
570 if t = @{term True} then (TRUE, t)
571 else if t = @{term False} then (FALSE, t)
573 | NONE => (INDET, t) end
574 in (determine o (map eval)) cs end;
575 WN.16.5.0-------------------------------------------------------------*)