1 (******************************************************************************)
2 (* FILE : generalize.ml *)
3 (* DESCRIPTION : Generalization. *)
5 (* READS FILES : <none> *)
6 (* WRITES FILES : <none> *)
8 (* AUTHOR : R.J.Boulton *)
9 (* DATE : 21st June 1991 *)
11 (* LAST MODIFIED : R.J.Boulton *)
12 (* DATE : 12th October 1992 *)
14 (* LAST MODIFIED : P. Papapanagiotou (University of Edinburgh) *)
15 (* DATE : July 2009 *)
16 (******************************************************************************)
18 (*----------------------------------------------------------------------------*)
19 (* is_generalizable : string list -> term -> bool *)
21 (* Function to determine whether or not a term has the correct properties to *)
22 (* be generalizable. It takes a list of accessor function names as its first *)
23 (* argument. This is for efficiency. It could compute them itself, but if an *)
24 (* external function is going to call is_generalizable many times it is *)
25 (* better for the external function to compute the list of accessors. *)
26 (*----------------------------------------------------------------------------*)
28 let is_generalizable accessors tm =
30 (is_explicit_value_template tm) or
32 (try(mem ((fst o dest_const o fst o strip_comb) tm) accessors)
33 with Failure _ -> false));;
35 (*----------------------------------------------------------------------------*)
36 (* generalizable_subterms : string list -> term -> term list *)
38 (* Computes the generalizable subterms of a literal, given a list of accessor *)
40 (*----------------------------------------------------------------------------*)
42 let generalizable_subterms accessors tm =
43 try (setify (find_bm_terms (is_generalizable accessors) tm)
44 ) with Failure _ -> failwith "generalizable_subterms";;
46 (*----------------------------------------------------------------------------*)
47 (* minimal_common_subterms : term list -> term list *)
49 (* Given a list of terms, this function removes from the list any term that *)
50 (* has one of the other terms as a proper subterm. It also eliminates any *)
52 (*----------------------------------------------------------------------------*)
54 let minimal_common_subterms tml =
57 (fun tm -> not (exists (fun tm' -> (is_subterm tm' tm) & (not (tm' = tm))) tml'))
60 (*----------------------------------------------------------------------------*)
61 (* to_be_generalized : term -> term list -> term -> bool *)
63 (* This function decides whether a subterm of a literal should be generalized.*)
64 (* It takes a literal, a list of other literals, and a subterm of the literal *)
65 (* as arguments. The subterm should be generalized if it occurs in one of the *)
66 (* other literals, or if the literal is an equality and it occurs on both *)
67 (* sides, or if the literal is the negation of an equality and the subterm *)
68 (* occurs on both sides. *)
69 (*----------------------------------------------------------------------------*)
71 let to_be_generalized tm tml gen =
72 try (let (l,r) = dest_eq (dest_neg tm)
73 in if ((is_subterm gen l) & (is_subterm gen r))
75 else failwith "") with Failure _ ->
76 try (let (l,r) = dest_eq tm
77 in if ((is_subterm gen l) & (is_subterm gen r))
79 else failwith "") with Failure _ ->
80 (exists (is_subterm gen) tml);;
82 (*----------------------------------------------------------------------------*)
83 (* terms_to_be_generalized : term -> term list *)
85 (* Given a clause, this function determines the subterms of the clause that *)
86 (* are to be generalized. For each literal, the function computes the *)
87 (* generalizable subterms. It then filters out those subterms that are not to *)
88 (* be generalized. It only looks at the remaining literals when doing this, *)
89 (* not at those already processed. This is legitimate because if the subterm *)
90 (* occurs in a previous literal, it would have already been added to the main *)
91 (* list of subterms that should be generalized. Before returning this main *)
92 (* list, the function removes any non-minimal common subterms. This operation *)
93 (* also removes any duplicates. *)
94 (*----------------------------------------------------------------------------*)
96 let terms_to_be_generalized tm =
97 let accessors = (all_accessors ()) @ (all_constructors())
98 in let rec terms_to_be_generalized' tml =
102 in let gens = generalizable_subterms accessors h
103 in let gens' = filter (to_be_generalized h t) gens
104 in gens' @ (terms_to_be_generalized' t)
105 in minimal_common_subterms (terms_to_be_generalized' (disj_list tm));;
107 (*----------------------------------------------------------------------------*)
108 (* distinct_var : term list -> type -> term *)
110 (* Function to generate a sensibly-named variable of a specified type. *)
111 (* Variables that the new variable must be distinct from can be specified in *)
112 (* the first argument. The new variable will be named according to the first *)
113 (* letter of the top-level constructor in the specified type, or if the type *)
114 (* is a simple polymorphic type, the name `x' is used. The actual name will *)
115 (* be this name followed by zero or more apostrophes. *)
116 (*----------------------------------------------------------------------------*)
118 let distinct_var vars ty =
119 let letter = try((hd o explode o fst o dest_type) ty) with Failure _ -> "x"
120 in variant vars (mk_var (letter,ty));;
122 (*----------------------------------------------------------------------------*)
123 (* distinct_vars : term list -> type list -> term list *)
125 (* Generates new variables using `distinct_var' for each of the types in the *)
126 (* given list. The function ensures that each of the new variables are *)
127 (* distinct from each other, as well as from the argument list of variables. *)
128 (*----------------------------------------------------------------------------*)
130 let rec distinct_vars vars tyl =
133 else let var = distinct_var vars (hd tyl)
134 in var::(distinct_vars (var::vars) (tl tyl));;
136 (*----------------------------------------------------------------------------*)
137 (* apply_gen_lemma : term -> thm -> thm *)
139 (* Given a term to be generalized and a generalization lemma, this function *)
140 (* tries to apply the lemma to the term. The result, if successful, is a *)
141 (* specialization of the lemma. *)
143 (* The function checks that the lemma has no hypotheses, and then extracts a *)
144 (* list of subterms of the conclusion that match the given term and contain *)
145 (* all the free variables of the conclusion. The second condition prevents *)
146 (* new variables being introduced into the goal clause. The ordering of the *)
147 (* subterms in the list is dependent on the implementation of `find_terms', *)
148 (* but probably doesn't matter anyway, because the function tries each of *)
149 (* them until it finds one that is acceptable. *)
151 (* Each subterm is tried as follows. A matching between the subterm and the *)
152 (* term to be generalized is obtained. This is used to instantiate the lemma. *)
153 (* The function then checks that when the conclusion of this new theorem is *)
154 (* generalized (by replacing the term to be generalized with a variable), the *)
155 (* function symbol of the term to be generalized no longer appears in it. *)
156 (*----------------------------------------------------------------------------*)
158 let apply_gen_lemma tm th =
160 (let apply_gen_lemma' subtm =
161 (let (_,tm_bind,ty_bind) = term_match [] subtm tm
162 in let (insts,vars) = List.split tm_bind
163 in let th' = ((SPECL insts) o (GENL vars) o (INST_TYPE ty_bind)) th
164 in let gen_conc = subst [(genvar (type_of tm),tm)] (concl th')
165 and f = fst (strip_comb tm)
166 in if (is_subterm f gen_conc)
169 in let ([],conc) = dest_thm th
170 in let conc_vars = frees conc
171 in let good_subterm subtm =
172 ((can (term_match [] subtm) tm) & ((subtract conc_vars (frees subtm)) = []))
173 in let subtms = rev (find_terms good_subterm conc)
174 in tryfind apply_gen_lemma' subtms
175 ) with Failure _ -> failwith "apply_gen_lemma";;
177 (*----------------------------------------------------------------------------*)
178 (* applicable_gen_lemmas : term list -> thm list *)
180 (* Computes instantiations of generalization lemmas applicable to a list of *)
181 (* terms, the terms to be generalized. *)
182 (*----------------------------------------------------------------------------*)
184 let applicable_gen_lemmas tml =
185 flat (map (fun tm -> mapfilter (apply_gen_lemma tm) (gen_lemmas ())) tml);;
187 (*----------------------------------------------------------------------------*)
188 (* generalize_heuristic : (term # bool) -> ((term # bool) list # proof) *)
190 (* Generalization heuristic. *)
192 (* This function first computes the terms to be generalized in a clause. It *)
193 (* fails if there are none. It then obtains a list of instantiated *)
194 (* generalization lemmas for these terms. Each of these lemmas is transformed *)
195 (* to a theorem of the form |- x = F. If the original lemma was a negation, *)
196 (* x is the argument of the negation. Otherwise x is the negation of the *)
197 (* original lemma. *)
199 (* The negated lemmas are added to the clause, and the result is generalized *)
200 (* by replacing each of the terms to be generalized by new distinct *)
201 (* variables. This generalized clause is returned together with a proof of *)
202 (* the original clause from it. *)
204 (* The proof begins by specializing the variables that were used to replace *)
205 (* the generalized terms. The theorem is then of the form: *)
207 (* |- lemma1 \/ lemma2 \/ ... \/ lemman \/ original_clause (1) *)
209 (* We have a theorem |- lemmai = F for each i between 1 and n. Consider the *)
210 (* first of these. From it, the following theorem can be obtained: *)
212 (* |- lemma1 \/ lemma2 \/ ... \/ lemman \/ original_clause = *)
213 (* F \/ lemma2 \/ ... \/ lemman \/ original_clause *)
215 (* Simplifying using |- F \/ x = x, this gives: *)
217 (* |- lemma1 \/ lemma2 \/ ... \/ lemman \/ original_clause = *)
218 (* lemma2 \/ ... \/ lemman \/ original_clause *)
220 (* From this theorem and (1), we obtain: *)
222 (* |- lemma2 \/ ... \/ lemman \/ original_clause *)
224 (* Having repeated this process for each of the lemmas, the proof eventually *)
225 (* returns a theorem for the original clause, i.e. |- original_clause. *)
226 (*----------------------------------------------------------------------------*)
228 let generalize_heuristic (tm,(ind:bool)) =
231 let ([],tm) = dest_thm th
237 (SYM (SPEC_ALL (hd (CONJUNCTS NOT_CLAUSES))))) th)
238 and ELIM_LEMMA lemma th =
239 let rest = snd (dest_disj (concl th))
240 in EQ_MP (CONV_RULE (RAND_CONV (REWR_CONV F_OR))
241 (AP_THM (AP_TERM `(\/)` lemma) rest)) th
242 in let gen_terms = check (fun l -> not (l = [])) (terms_to_be_generalized tm)
243 in let lemmas = map NEGATE (applicable_gen_lemmas gen_terms)
244 in let tm' = itlist (curry mk_disj) (map (lhs o concl) lemmas) tm
245 in let new_vars = distinct_vars (frees tm') (map type_of gen_terms)
246 in let tm'' = subst (lcombinep (new_vars,gen_terms)) tm'
247 in let countercheck = try counter_check 5 tm'' with Failure _ ->
248 warn true "Could not generate counter example!" ; true
249 in if (countercheck = true) then let proof th'' =
250 let th' = SPECL gen_terms (GENL new_vars th'')
251 in rev_itlist ELIM_LEMMA lemmas th'
252 in (proof_print_string_l "-> Generalize Heuristic"() ; my_gen_terms := tm''::!my_gen_terms ; ([(tm'',ind)],apply_proof (proof o hd) [tm'']))
253 else failwith "Counter example failure!"
254 ) with Failure _ -> failwith "generalize_heuristic";;
257 (* Implementation of Aderhold's Generalization techniques: *)
259 let is_constructor_eq constructor v tm =
261 let (a,b) = dest_eq tm
262 in let cand_c = ( if ( v = a ) then b
263 else if ( v = b ) then a
265 in let cand_name = (fst o dest_const o fst o strip_comb) cand_c
266 in constructor = cand_name
267 (* then cand_name else failwith ""*)
268 ) with Failure _ -> false;;
271 let is_constructor_neq constructor v tm =
273 let tm' = dest_neg tm
274 in let (a,b) = dest_eq tm'
275 in let cand_c = ( if ( v = a ) then b
276 else if ( v = b ) then a
278 in let cand_name = (fst o dest_const o fst o strip_comb) cand_c
279 in constructor = cand_name
280 ) with Failure _ -> false;;
283 let infer_constructor v tm =
285 print_term v;print_string " XXX ";print_term tm;print_newline();
286 let v_ty = (fst o dest_type) (type_of v)
287 in let clist = map fst3 ((shell_constructors o sys_shell_info) v_ty)
288 in let conjs = conj_list tm
289 in let check_constructor_eq c v tms =
290 let res = map (is_constructor_eq c v) tms
291 in if (mem true res) then true
293 in let check_constructor_neq c v tms =
294 let res = map (is_constructor_neq c v) tms
295 in if (mem true res) then true
297 in let check_constructor c all_constr v tms =
298 if (check_constructor_eq c v tms) then true
299 else let constrs = subtract all_constr [c]
300 in let res = map (fun c -> check_constructor_neq c v tms) constrs
301 in if (mem false res) then false
303 in let res = map (fun c -> check_constructor c clist v conjs) clist
304 in let reslist = List.combine res clist
305 in assoc true reslist
306 ) with Failure _ -> failwith "infer_constructor";;
308 let get_rec_pos_of_fun f =
310 (fst o get_def o fst o dest_const) f
311 ) with Failure _ -> 0;;
313 let rec is_in_rec_pos subtm tm =
314 let (op,args) = strip_comb tm
316 let rec_argn = get_rec_pos_of_fun op
317 in if ( (el (rec_argn - 1) args) = subtm )
320 ) with Failure _ -> mem true (map (is_in_rec_pos subtm) args) ;;
322 let is_var_in_rec_pos v tm =
324 if (not (is_var v)) then false
325 else if (not (mem v (frees tm))) then false
326 else is_in_rec_pos v tm
327 ) with Failure _ -> false;;
329 let eliminateSelectors tm =
332 in let vars' = filter (not o (fun v -> is_var_in_rec_pos v tm )) vars
333 in if (vars' = []) then tm
334 else let rec find_candidate vars tm =
335 if ( vars = [] ) then failwith "find_candidate"
336 else let var = (hd vars) in try ( (var,infer_constructor var tm) )
337 with Failure _ -> find_candidate (tl vars) tm
338 in let (var,constr) = find_candidate vars' tm
339 in let v_ty = (fst o dest_type) (type_of var)
340 in let s_info = sys_shell_info v_ty
341 in let new_vars = distinct_vars vars (shell_constructor_arg_types constr s_info)
342 in let new_subtm = list_mk_icomb constr new_vars
343 in let new_tm = subst [new_subtm,var] tm
344 in (snd o dest_eq o concl) (REWRITE_CONV (map snd (shell_constructor_accessors constr s_info)) new_tm)
345 ) with Failure _ -> failwith "eliminateSelectors";;
349 let rec vars(acc,tm) =
350 if is_var tm then tm::acc
351 else if is_const tm then acc
352 else if is_abs tm then
353 let v,bod = dest_abs tm in
356 let l,r = dest_comb tm in
357 vars(vars(acc,r),l) in
358 fun tm -> vars([],tm);;
361 let rec eqs(acc,tm) =
362 if is_eq tm then tm::acc
363 else if is_var tm then acc
364 else if is_const tm then acc
365 else if is_abs tm then
366 let v,bod = dest_abs tm in
369 let l,r = dest_comb tm in
371 fun tm -> eqs([],tm);;
373 let rec contains_any tm args =
374 if is_var tm then false
375 else if is_numeral tm then false
376 else if is_const tm then mem ((fst o dest_const) tm) args
377 else if is_abs tm then
378 let v,bod = dest_abs tm in
381 let l,r = dest_comb tm in
382 (contains_any l args) or (contains_any r args);;
384 let is_rec_type tm = try( mem ((fst o dest_type o type_of) tm) (shells()) ) with Failure _ -> false;;
386 let is_generalizable_subterm bad tm =
391 (contains_any tm bad) );;
393 (*----------------------------------------------------------------------------*)
394 (* A set S of terms is called a suitable proposal for some formula phi if each*)
395 (* t' in S is a generalizable subterm of phi and if there is some t' in S that*)
396 (* occurs at least twice in phi. *)
397 (* Here gens is assumed to be the generalizable subterms of phi as found by *)
398 (* find_bm_terms. This means that it will contain t' as many times as it was *)
399 (* found in phi. Therefore, the occurences of t' in gens are equivalent to its*)
400 (* occurences in phi. *)
401 (*----------------------------------------------------------------------------*)
403 let is_suitable_proposal s phi gens =
404 ( forall (fun tm -> mem tm gens) s ) & (exists (fun tm -> lcount tm gens > 1) s);;
407 let checksuitableeq = ref true;; (* equation criterion *)
408 let newisgen = ref true;; (* Use Aderhold's (true) or Boulton's (false) is_generalizable for terms *)
410 let is_eq_suitable t eq =
411 if (not !checksuitableeq) then true
412 else if (not (is_eq eq)) then false
413 else let l,r = dest_eq eq in
414 if ((is_subterm t r) & (is_subterm t l)) then true
415 else length(find_bm_terms ((=) t) eq) > 1;;
418 let generateProposals tm phi =
419 let rec generateProposals' bad tm phi gens =
422 then let (t1,t2) = dest_eq tm
423 in let p1 = (generateProposals' bad t1 phi gens)
424 in let p1' = if (is_suitable_proposal [t1] phi gens) then p1@[[t1]] else p1
425 in let p = p @ filter (exists (fun t -> is_eq_suitable t tm)) p1'
426 in let p2 = (generateProposals' bad t2 phi gens)
427 in let p2' = if (is_suitable_proposal [t2] phi gens) then p2@[[t2]] else p2
428 in p @ filter (exists (fun t -> is_eq_suitable t tm)) p2'
430 then let (op,args) = strip_comb tm
431 in let recpos = get_rec_pos_of_fun op
432 in let s = if (recpos > 0) then [el (recpos-1) args] else []
433 in let p = if (is_suitable_proposal s phi gens) then p@[s] else p
434 in p @ flat (map (fun tm -> generateProposals' bad tm phi gens) args)
436 in let bad = (all_accessors()) @ (all_constructors())
437 in let gens = if (!newisgen) then find_bm_terms (is_generalizable_subterm bad) phi
438 else find_bm_terms (is_generalizable bad) phi
439 in generateProposals' bad tm phi gens;;
441 let proposal_induction_test s phi =
442 let newvars = distinct_vars (frees phi) (map (type_of) s)
443 in let subs = List.combine newvars s
444 in let newterm = subst subs phi
445 in let (unfl,fl) = possible_inductions newterm
446 in if (exists (fun v -> (mem v (unfl@fl)) ) newvars ) then true else false;;
448 let get_proposal_term_occs s phi =
449 let gens = find_bm_terms (fun tm -> true) phi
450 in let scount = map (fun tm -> lcount tm gens) s
451 in itlist (+) scount 0;;
453 let organizeProposals s phi =
454 let stest = map (fun prop -> (prop,proposal_induction_test prop phi)) s
455 in let indok = filter (((=) true) o snd) stest
456 in let s' = if (indok = []) then (proof_print_string_l "Weak Generalization" (map fst stest)) else (map fst indok)
457 in if (length s' = 1) then hd s'
458 else let scounted = (rev o sort_on_snd) (map (fun prop -> (prop,lcount prop s')) s')
459 in let smax = (snd o hd) scounted
460 in let s'' = map fst (filter (((=) smax) o snd) scounted)
461 in if (length s'' = 1) then hd s''
462 else let soccscounted = (rev o sort_on_snd) (map (fun prop -> (prop,get_proposal_term_occs prop phi)) s'')
463 in (fst o hd) soccscounted;;
465 let generalizeCommonSubterms tm =
466 let props = generateProposals tm tm
467 in if (props = []) then failwith ""
468 else let s = organizeProposals props tm
469 in let newvars = distinct_vars (frees tm) (map type_of s)
470 in let varcomb = List.combine newvars s
471 in (subst varcomb tm,varcomb);;
473 let rec separate f v v' allrpos tm =
474 let replace tm v v' rpos =
475 if (not rpos) then tm
476 else if (tm = v) then v'
477 else (separate f v v' allrpos tm)
478 in if (is_comb tm) then (
479 let (op,args) = strip_comb tm
480 in let recpos = get_rec_pos_of_fun op
481 in if ((allrpos) & not (op = `(=)`))
482 then (list_mk_comb (op,(map (fun (t,i) -> replace t v v' ((i = recpos) or (recpos = 0))) (number_list args))))
484 then (list_mk_comb(op,[replace (hd args) v v' true;replace ((hd o tl) args) v v' true]))
486 then (list_mk_comb (op,(map (fun (t,i) -> replace t v v' (i = recpos)) (number_list args))))
487 else (list_mk_comb (op,(map (separate f v v' allrpos) args)))
492 let rec generalized_apart_successfully v v' tm tm' =
493 if (tm' = v') then true
494 else if (is_eq tm) then ( let (tm1,tm2) = dest_eq tm
495 in let (tm1',tm2') = dest_eq tm'
496 in (generalized_apart_successfully v v' tm1 tm1')
497 & (generalized_apart_successfully v v' tm2 tm2') )
498 else ( let av = all_variables tm
499 in let av' = all_variables tm'
500 in let varsub = List.combine av av'
501 in ((mem (v,v') varsub) & (mem v av')) );;
503 let useful_apart_generalization v v' tm gen =
504 let eqssub = List.combine (all_equations tm) (all_equations gen)
505 in let eqsok = forall (fun (x,y) -> (x=y) or (generalized_apart_successfully v v' x y)) eqssub
506 in let countercheck = try counter_check 5 gen with Failure s ->
507 warn true ("Could not generate counter example: " ^ s) ; true
508 in eqsok & (generalized_apart_successfully v v' tm gen) & countercheck;;
510 let generalize_Apart tm =
511 let is_fun tm = (try( mem ((fst o dest_const o fst o strip_comb) tm) (defs_names ()) ) with Failure _ -> false)
512 in let fs = find_bm_terms is_fun tm
513 in let dfs = map strip_comb fs
514 in let find_f (op,args) dfs = (
515 let r = get_rec_pos_of_fun op
516 in let arg_filter args args' =
517 (let v = el (r-1) args
518 in (is_var v) & (mem v (snd (remove_el r args'))))
519 in let match_filter (op',args') =
520 ((op' = op) & (arg_filter args args'))
521 in can (find match_filter) dfs )
522 in let (f,args) = try( find (fun (op,args) -> find_f (op,args) dfs) dfs ) with Failure _ -> failwith ""
523 in let v = el ((get_rec_pos_of_fun f) -1) args
524 in let v' = distinct_var (flat (map frees args)) (type_of v)
525 in let gen = separate f v v' false tm
526 in if (useful_apart_generalization v v' tm gen) then (gen,[v',v])
527 else let pcs = map fst dfs
528 in let restpcs = subtract pcs [f]
529 in let recposs = map get_rec_pos_of_fun restpcs
530 in let recpos = try (find ((<) 0) recposs) with Failure _ -> 0
531 in let gen = if (forall (fun x -> (x = 0) or (x = recpos)) recposs)
532 then separate f v v' true tm
533 else failwith "not same recpos for all functions"
534 in if (useful_apart_generalization v v' tm gen) then (gen,[v',v])
535 else failwith "failed";;
537 (*----------------------------------------------------------------------------*)
538 (* Reference flag to check if a term has already been generalized so as to *)
539 (* avoid multiple proposal generalization because of the waterfall loop. *)
540 (*----------------------------------------------------------------------------*)
541 let checkgen = ref true;;
543 let generalize_heuristic_ext (tm,(ind:bool)) =
544 if (mem tm !my_gen_terms & !checkgen) then failwith ""
547 (let ELIM_LEMMA lemma th =
548 let rest = snd (dest_disj (concl th))
549 in EQ_MP (CONV_RULE (RAND_CONV (REWR_CONV F_OR))
550 (AP_THM (AP_TERM `(\/)` lemma) rest)) th
551 in let (tm',subs) = try( generalize_Apart tm ) with Failure _ -> (tm,[])
552 in let (new_vars,gen_terms) = List.split subs
553 in let (tm'',subs) = try( generalizeCommonSubterms tm' ) with Failure _ -> (tm',[])
554 in if (tm = tm'') then failwith ""
555 else let (new_vars',gen_terms') = List.split subs
556 in let gen_terms = gen_terms@gen_terms' and new_vars = new_vars @ new_vars'
558 in let countercheck = try counter_check 5 tm'' with Failure s ->
559 warn true ("Could not generate counter example: " ^ s) ; true
560 in if (countercheck = true) then let proof th'' =
561 let th' = SPECL gen_terms (GENL new_vars th'')
562 in rev_itlist ELIM_LEMMA lemmas th'
563 in (proof_print_string_l "-> Generalize Heuristic"() ; my_gen_terms := tm''::!my_gen_terms ; ([(tm'',ind)],apply_proof (proof o hd) [tm'']))
564 else failwith "Counter example failure!"
565 ) with Failure _ -> failwith "generalize_heuristic";;