(******************************************************************************)
(* FILE : generalize.ml *)
(* DESCRIPTION : Generalization. *)
(* *)
(* READS FILES : <none> *)
(* WRITES FILES : <none> *)
(* *)
(* AUTHOR : R.J.Boulton *)
(* DATE : 21st June 1991 *)
(* *)
(* LAST MODIFIED : R.J.Boulton *)
(* DATE : 12th October 1992 *)
(* *)
(* LAST MODIFIED : P. Papapanagiotou (University of Edinburgh) *)
(* DATE : July 2009 *)
(******************************************************************************)
(*----------------------------------------------------------------------------*)
(* is_generalizable : string list -> term -> bool *)
(* *)
(* Function to determine whether or not a term has the correct properties to *)
(* be generalizable. It takes a list of accessor function names as its first *)
(* argument. This is for efficiency. It could compute them itself, but if an *)
(* external function is going to call is_generalizable many times it is *)
(* better for the external function to compute the list of accessors. *)
(*----------------------------------------------------------------------------*)
let is_generalizable accessors tm =
not ((is_var tm) or
(is_explicit_value_template tm) or
(is_eq tm) or
(try(mem ((fst o dest_const o fst o strip_comb) tm) accessors)
with Failure _ -> false));;
(*----------------------------------------------------------------------------*)
(* generalizable_subterms : string list -> term -> term list *)
(* *)
(* Computes the generalizable subterms of a literal, given a list of accessor *)
(* function names. *)
(*----------------------------------------------------------------------------*)
let generalizable_subterms accessors tm =
try (setify (find_bm_terms (is_generalizable accessors) tm)
) with Failure _ -> failwith "generalizable_subterms";;
(*----------------------------------------------------------------------------*)
(* minimal_common_subterms : term list -> term list *)
(* *)
(* Given a list of terms, this function removes from the list any term that *)
(* has one of the other terms as a proper subterm. It also eliminates any *)
(* duplicates. *)
(*----------------------------------------------------------------------------*)
let minimal_common_subterms tml =
let tml' = setify tml
in filter
(fun tm -> not (exists (fun tm' -> (is_subterm tm' tm) & (not (tm' = tm))) tml'))
tml';;
(*----------------------------------------------------------------------------*)
(* to_be_generalized : term -> term list -> term -> bool *)
(* *)
(* This function decides whether a subterm of a literal should be generalized.*)
(* It takes a literal, a list of other literals, and a subterm of the literal *)
(* as arguments. The subterm should be generalized if it occurs in one of the *)
(* other literals, or if the literal is an equality and it occurs on both *)
(* sides, or if the literal is the negation of an equality and the subterm *)
(* occurs on both sides. *)
(*----------------------------------------------------------------------------*)
let to_be_generalized tm tml gen =
try (let (l,r) = dest_eq (dest_neg tm)
in if ((is_subterm gen l) & (is_subterm gen r))
then true
else failwith "") with Failure _ ->
try (let (l,r) = dest_eq tm
in if ((is_subterm gen l) & (is_subterm gen r))
then true
else failwith "") with Failure _ ->
(exists (is_subterm gen) tml);;
(*----------------------------------------------------------------------------*)
(* terms_to_be_generalized : term -> term list *)
(* *)
(* Given a clause, this function determines the subterms of the clause that *)
(* are to be generalized. For each literal, the function computes the *)
(* generalizable subterms. It then filters out those subterms that are not to *)
(* be generalized. It only looks at the remaining literals when doing this, *)
(* not at those already processed. This is legitimate because if the subterm *)
(* occurs in a previous literal, it would have already been added to the main *)
(* list of subterms that should be generalized. Before returning this main *)
(* list, the function removes any non-minimal common subterms. This operation *)
(* also removes any duplicates. *)
(*----------------------------------------------------------------------------*)
let terms_to_be_generalized tm =
let accessors = (all_accessors ()) @ (all_constructors())
in let rec terms_to_be_generalized' tml =
if (tml = [])
then []
else let h::t = tml
in let gens = generalizable_subterms accessors h
in let gens' = filter (to_be_generalized h t) gens
in gens' @ (terms_to_be_generalized' t)
in minimal_common_subterms (terms_to_be_generalized' (disj_list tm));;
(*----------------------------------------------------------------------------*)
(* distinct_var : term list -> type -> term *)
(* *)
(* Function to generate a sensibly-named variable of a specified type. *)
(* Variables that the new variable must be distinct from can be specified in *)
(* the first argument. The new variable will be named according to the first *)
(* letter of the top-level constructor in the specified type, or if the type *)
(* is a simple polymorphic type, the name `x' is used. The actual name will *)
(* be this name followed by zero or more apostrophes. *)
(*----------------------------------------------------------------------------*)
let distinct_var vars ty =
let letter = try((hd o explode o fst o dest_type) ty) with Failure _ -> "x"
in variant vars (mk_var (letter,ty));;
(*----------------------------------------------------------------------------*)
(* distinct_vars : term list -> type list -> term list *)
(* *)
(* Generates new variables using `distinct_var' for each of the types in the *)
(* given list. The function ensures that each of the new variables are *)
(* distinct from each other, as well as from the argument list of variables. *)
(*----------------------------------------------------------------------------*)
let rec distinct_vars vars tyl =
if (tyl = [])
then []
else let var = distinct_var vars (hd tyl)
in var::(distinct_vars (var::vars) (tl tyl));;
(*----------------------------------------------------------------------------*)
(* apply_gen_lemma : term -> thm -> thm *)
(* *)
(* Given a term to be generalized and a generalization lemma, this function *)
(* tries to apply the lemma to the term. The result, if successful, is a *)
(* specialization of the lemma. *)
(* *)
(* The function checks that the lemma has no hypotheses, and then extracts a *)
(* list of subterms of the conclusion that match the given term and contain *)
(* all the free variables of the conclusion. The second condition prevents *)
(* new variables being introduced into the goal clause. The ordering of the *)
(* subterms in the list is dependent on the implementation of `find_terms', *)
(* but probably doesn't matter anyway, because the function tries each of *)
(* them until it finds one that is acceptable. *)
(* *)
(* Each subterm is tried as follows. A matching between the subterm and the *)
(* term to be generalized is obtained. This is used to instantiate the lemma. *)
(* The function then checks that when the conclusion of this new theorem is *)
(* generalized (by replacing the term to be generalized with a variable), the *)
(* function symbol of the term to be generalized no longer appears in it. *)
(*----------------------------------------------------------------------------*)
let apply_gen_lemma tm th =
try
(let apply_gen_lemma' subtm =
(let (_,tm_bind,ty_bind) = term_match [] subtm tm
in let (insts,vars) = List.split tm_bind
in let th' = ((SPECL insts) o (GENL vars) o (INST_TYPE ty_bind)) th
in let gen_conc = subst [(genvar (type_of tm),tm)] (concl th')
and f = fst (strip_comb tm)
in if (is_subterm f gen_conc)
then failwith ""
else th')
in let ([],conc) = dest_thm th
in let conc_vars = frees conc
in let good_subterm subtm =
((can (term_match [] subtm) tm) & ((subtract conc_vars (frees subtm)) = []))
in let subtms = rev (find_terms good_subterm conc)
in tryfind apply_gen_lemma' subtms
) with Failure _ -> failwith "apply_gen_lemma";;
(*----------------------------------------------------------------------------*)
(* applicable_gen_lemmas : term list -> thm list *)
(* *)
(* Computes instantiations of generalization lemmas applicable to a list of *)
(* terms, the terms to be generalized. *)
(*----------------------------------------------------------------------------*)
let applicable_gen_lemmas tml =
flat (map (fun tm -> mapfilter (apply_gen_lemma tm) (gen_lemmas ())) tml);;
(*----------------------------------------------------------------------------*)
(* generalize_heuristic : (term # bool) -> ((term # bool) list # proof) *)
(* *)
(* Generalization heuristic. *)
(* *)
(* This function first computes the terms to be generalized in a clause. It *)
(* fails if there are none. It then obtains a list of instantiated *)
(* generalization lemmas for these terms. Each of these lemmas is transformed *)
(* to a theorem of the form |- x = F. If the original lemma was a negation, *)
(* x is the argument of the negation. Otherwise x is the negation of the *)
(* original lemma. *)
(* *)
(* The negated lemmas are added to the clause, and the result is generalized *)
(* by replacing each of the terms to be generalized by new distinct *)
(* variables. This generalized clause is returned together with a proof of *)
(* the original clause from it. *)
(* *)
(* The proof begins by specializing the variables that were used to replace *)
(* the generalized terms. The theorem is then of the form: *)
(* *)
(* |- lemma1 \/ lemma2 \/ ... \/ lemman \/ original_clause (1) *)
(* *)
(* We have a theorem |- lemmai = F for each i between 1 and n. Consider the *)
(* first of these. From it, the following theorem can be obtained: *)
(* *)
(* |- lemma1 \/ lemma2 \/ ... \/ lemman \/ original_clause = *)
(* F \/ lemma2 \/ ... \/ lemman \/ original_clause *)
(* *)
(* Simplifying using |- F \/ x = x, this gives: *)
(* *)
(* |- lemma1 \/ lemma2 \/ ... \/ lemman \/ original_clause = *)
(* lemma2 \/ ... \/ lemman \/ original_clause *)
(* *)
(* From this theorem and (1), we obtain: *)
(* *)
(* |- lemma2 \/ ... \/ lemman \/ original_clause *)
(* *)
(* Having repeated this process for each of the lemmas, the proof eventually *)
(* returns a theorem for the original clause, i.e. |- original_clause. *)
(*----------------------------------------------------------------------------*)
let generalize_heuristic (tm,(ind:bool)) =
try
(let NEGATE th =
let ([],tm) = dest_thm th
in if (is_neg tm)
then EQF_INTRO th
else EQF_INTRO
(CONV_RULE
(REWR_CONV
(SYM (SPEC_ALL (hd (CONJUNCTS NOT_CLAUSES))))) th)
and ELIM_LEMMA lemma th =
let rest = snd (dest_disj (concl th))
in EQ_MP (CONV_RULE (RAND_CONV (REWR_CONV F_OR))
(AP_THM (AP_TERM `(\/)` lemma) rest)) th
in let gen_terms = check (fun l -> not (l = [])) (terms_to_be_generalized tm)
in let lemmas = map NEGATE (applicable_gen_lemmas gen_terms)
in let tm' = itlist (curry mk_disj) (map (lhs o concl) lemmas) tm
in let new_vars = distinct_vars (frees tm') (map type_of gen_terms)
in let tm'' = subst (lcombinep (new_vars,gen_terms)) tm'
in let countercheck = try counter_check 5 tm'' with Failure _ ->
warn true "Could not generate counter example!" ; true
in if (countercheck = true) then let proof th'' =
let th' = SPECL gen_terms (GENL new_vars th'')
in rev_itlist ELIM_LEMMA lemmas th'
in (proof_print_string_l "-> Generalize Heuristic"() ; my_gen_terms := tm''::!my_gen_terms ; ([(tm'',ind)],apply_proof (proof o hd) [tm'']))
else failwith "Counter example failure!"
) with Failure _ -> failwith "generalize_heuristic";;
(* Implementation of Aderhold's Generalization techniques: *)
let is_constructor_eq constructor v tm =
try (
let (a,b) = dest_eq tm
in let cand_c = ( if ( v = a ) then b
else if ( v = b ) then a
else failwith "" )
in let cand_name = (fst o dest_const o fst o strip_comb) cand_c
in constructor = cand_name
(* then cand_name else failwith ""*)
) with Failure _ -> false;;
let is_constructor_neq constructor v tm =
try (
let tm' = dest_neg tm
in let (a,b) = dest_eq tm'
in let cand_c = ( if ( v = a ) then b
else if ( v = b ) then a
else failwith "" )
in let cand_name = (fst o dest_const o fst o strip_comb) cand_c
in constructor = cand_name
) with Failure _ -> false;;
let infer_constructor v tm =
try (
print_term v;print_string " XXX ";print_term tm;print_newline();
let v_ty = (fst o dest_type) (type_of v)
in let clist = map fst3 ((shell_constructors o sys_shell_info) v_ty)
in let conjs = conj_list tm
in let check_constructor_eq c v tms =
let res = map (is_constructor_eq c v) tms
in if (mem true res) then true
else false
in let check_constructor_neq c v tms =
let res = map (is_constructor_neq c v) tms
in if (mem true res) then true
else false
in let check_constructor c all_constr v tms =
if (check_constructor_eq c v tms) then true
else let constrs = subtract all_constr [c]
in let res = map (fun c -> check_constructor_neq c v tms) constrs
in if (mem false res) then false
else true
in let res = map (fun c -> check_constructor c clist v conjs) clist
in let reslist = List.combine res clist
in assoc true reslist
) with Failure _ -> failwith "infer_constructor";;
let get_rec_pos_of_fun f =
try (
(fst o get_def o fst o dest_const) f
) with Failure _ -> 0;;
let rec is_in_rec_pos subtm tm =
let (op,args) = strip_comb tm
in try (
let rec_argn = get_rec_pos_of_fun op
in if ( (el (rec_argn - 1) args) = subtm )
then true
else failwith ""
) with Failure _ -> mem true (map (is_in_rec_pos subtm) args) ;;
let is_var_in_rec_pos v tm =
try (
if (not (is_var v)) then false
else if (not (mem v (frees tm))) then false
else is_in_rec_pos v tm
) with Failure _ -> false;;
let eliminateSelectors tm =
try (
let vars = frees tm
in let vars' = filter (not o (fun v -> is_var_in_rec_pos v tm )) vars
in if (vars' = []) then tm
else let rec find_candidate vars tm =
if ( vars = [] ) then failwith "find_candidate"
else let var = (hd vars) in try ( (var,infer_constructor var tm) )
with Failure _ -> find_candidate (tl vars) tm
in let (var,constr) = find_candidate vars' tm
in let v_ty = (fst o dest_type) (type_of var)
in let s_info = sys_shell_info v_ty
in let new_vars = distinct_vars vars (shell_constructor_arg_types constr s_info)
in let new_subtm = list_mk_icomb constr new_vars
in let new_tm = subst [new_subtm,var] tm
in (snd o dest_eq o concl) (REWRITE_CONV (map snd (shell_constructor_accessors constr s_info)) new_tm)
) with Failure _ -> failwith "eliminateSelectors";;
let all_variables =
let rec vars(acc,tm) =
if is_var tm then tm::acc
else if is_const tm then acc
else if is_abs tm then
let v,bod = dest_abs tm in
vars(v::acc,bod)
else
let l,r = dest_comb tm in
vars(vars(acc,r),l) in
fun tm -> vars([],tm);;
let all_equations =
let rec eqs(acc,tm) =
if is_eq tm then tm::acc
else if is_var tm then acc
else if is_const tm then acc
else if is_abs tm then
let v,bod = dest_abs tm in
eqs(acc,bod)
else
let l,r = dest_comb tm in
eqs(eqs(acc,r),l) in
fun tm -> eqs([],tm);;
let rec contains_any tm args =
if is_var tm then false
else if is_numeral tm then false
else if is_const tm then mem ((fst o dest_const) tm) args
else if is_abs tm then
let v,bod = dest_abs tm in
contains_any v args
else
let l,r = dest_comb tm in
(contains_any l args) or (contains_any r args);;
let is_rec_type tm = try( mem ((fst o dest_type o type_of) tm) (shells()) ) with Failure _ -> false;;
let is_generalizable_subterm bad tm =
(is_rec_type tm) &
not ( (is_var tm) or
(is_const tm) or
(is_numeral tm) or
(contains_any tm bad) );;
(*----------------------------------------------------------------------------*)
(* A set S of terms is called a suitable proposal for some formula phi if each*)
(* t' in S is a generalizable subterm of phi and if there is some t' in S that*)
(* occurs at least twice in phi. *)
(* Here gens is assumed to be the generalizable subterms of phi as found by *)
(* find_bm_terms. This means that it will contain t' as many times as it was *)
(* found in phi. Therefore, the occurences of t' in gens are equivalent to its*)
(* occurences in phi. *)
(*----------------------------------------------------------------------------*)
let is_suitable_proposal s phi gens =
( forall (fun tm -> mem tm gens) s ) & (exists (fun tm -> lcount tm gens > 1) s);;
let checksuitableeq = ref true;; (* equation criterion *)
let newisgen = ref true;; (* Use Aderhold's (true) or Boulton's (false) is_generalizable for terms *)
let is_eq_suitable t eq =
if (not !checksuitableeq) then true
else if (not (is_eq eq)) then false
else let l,r = dest_eq eq in
if ((is_subterm t r) & (is_subterm t l)) then true
else length(find_bm_terms ((=) t) eq) > 1;;
let generateProposals tm phi =
let rec generateProposals' bad tm phi gens =
let p = [] in
if (is_eq tm)
then let (t1,t2) = dest_eq tm
in let p1 = (generateProposals' bad t1 phi gens)
in let p1' = if (is_suitable_proposal [t1] phi gens) then p1@[[t1]] else p1
in let p = p @ filter (exists (fun t -> is_eq_suitable t tm)) p1'
in let p2 = (generateProposals' bad t2 phi gens)
in let p2' = if (is_suitable_proposal [t2] phi gens) then p2@[[t2]] else p2
in p @ filter (exists (fun t -> is_eq_suitable t tm)) p2'
else if (is_comb tm)
then let (op,args) = strip_comb tm
in let recpos = get_rec_pos_of_fun op
in let s = if (recpos > 0) then [el (recpos-1) args] else []
in let p = if (is_suitable_proposal s phi gens) then p@[s] else p
in p @ flat (map (fun tm -> generateProposals' bad tm phi gens) args)
else p
in let bad = (all_accessors()) @ (all_constructors())
in let gens = if (!newisgen) then find_bm_terms (is_generalizable_subterm bad) phi
else find_bm_terms (is_generalizable bad) phi
in generateProposals' bad tm phi gens;;
let proposal_induction_test s phi =
let newvars = distinct_vars (frees phi) (map (type_of) s)
in let subs = List.combine newvars s
in let newterm = subst subs phi
in let (unfl,fl) = possible_inductions newterm
in if (exists (fun v -> (mem v (unfl@fl)) ) newvars ) then true else false;;
let get_proposal_term_occs s phi =
let gens = find_bm_terms (fun tm -> true) phi
in let scount = map (fun tm -> lcount tm gens) s
in itlist (+) scount 0;;
let organizeProposals s phi =
let stest = map (fun prop -> (prop,proposal_induction_test prop phi)) s
in let indok = filter (((=) true) o snd) stest
in let s' = if (indok = []) then (proof_print_string_l "Weak Generalization" (map fst stest)) else (map fst indok)
in if (length s' = 1) then hd s'
else let scounted = (rev o sort_on_snd) (map (fun prop -> (prop,lcount prop s')) s')
in let smax = (snd o hd) scounted
in let s'' = map fst (filter (((=) smax) o snd) scounted)
in if (length s'' = 1) then hd s''
else let soccscounted = (rev o sort_on_snd) (map (fun prop -> (prop,get_proposal_term_occs prop phi)) s'')
in (fst o hd) soccscounted;;
let generalizeCommonSubterms tm =
let props = generateProposals tm tm
in if (props = []) then failwith ""
else let s = organizeProposals props tm
in let newvars = distinct_vars (frees tm) (map type_of s)
in let varcomb = List.combine newvars s
in (subst varcomb tm,varcomb);;
let rec separate f v v' allrpos tm =
let replace tm v v' rpos =
if (not rpos) then tm
else if (tm = v) then v'
else (separate f v v' allrpos tm)
in if (is_comb tm) then (
let (op,args) = strip_comb tm
in let recpos = get_rec_pos_of_fun op
in if ((allrpos) & not (op = `(=)`))
then (list_mk_comb (op,(map (fun (t,i) -> replace t v v' ((i = recpos) or (recpos = 0))) (number_list args))))
else if (op = `(=)`)
then (list_mk_comb(op,[replace (hd args) v v' true;replace ((hd o tl) args) v v' true]))
else if (op = f)
then (list_mk_comb (op,(map (fun (t,i) -> replace t v v' (i = recpos)) (number_list args))))
else (list_mk_comb (op,(map (separate f v v' allrpos) args)))
)
else tm;;
let rec generalized_apart_successfully v v' tm tm' =
if (tm' = v') then true
else if (is_eq tm) then ( let (tm1,tm2) = dest_eq tm
in let (tm1',tm2') = dest_eq tm'
in (generalized_apart_successfully v v' tm1 tm1')
& (generalized_apart_successfully v v' tm2 tm2') )
else ( let av = all_variables tm
in let av' = all_variables tm'
in let varsub = List.combine av av'
in ((mem (v,v') varsub) & (mem v av')) );;
let useful_apart_generalization v v' tm gen =
let eqssub = List.combine (all_equations tm) (all_equations gen)
in let eqsok = forall (fun (x,y) -> (x=y) or (generalized_apart_successfully v v' x y)) eqssub
in let countercheck = try counter_check 5 gen with Failure s ->
warn true ("Could not generate counter example: " ^ s) ; true
in eqsok & (generalized_apart_successfully v v' tm gen) & countercheck;;
let generalize_Apart tm =
let is_fun tm = (try( mem ((fst o dest_const o fst o strip_comb) tm) (defs_names ()) ) with Failure _ -> false)
in let fs = find_bm_terms is_fun tm
in let dfs = map strip_comb fs
in let find_f (op,args) dfs = (
let r = get_rec_pos_of_fun op
in let arg_filter args args' =
(let v = el (r-1) args
in (is_var v) & (mem v (snd (remove_el r args'))))
in let match_filter (op',args') =
((op' = op) & (arg_filter args args'))
in can (find match_filter) dfs )
in let (f,args) = try( find (fun (op,args) -> find_f (op,args) dfs) dfs ) with Failure _ -> failwith ""
in let v = el ((get_rec_pos_of_fun f) -1) args
in let v' = distinct_var (flat (map frees args)) (type_of v)
in let gen = separate f v v' false tm
in if (useful_apart_generalization v v' tm gen) then (gen,[v',v])
else let pcs = map fst dfs
in let restpcs = subtract pcs [f]
in let recposs = map get_rec_pos_of_fun restpcs
in let recpos = try (find ((<) 0) recposs) with Failure _ -> 0
in let gen = if (forall (fun x -> (x = 0) or (x = recpos)) recposs)
then separate f v v' true tm
else failwith "not same recpos for all functions"
in if (useful_apart_generalization v v' tm gen) then (gen,[v',v])
else failwith "failed";;
(*----------------------------------------------------------------------------*)
(* Reference flag to check if a term has already been generalized so as to *)
(* avoid multiple proposal generalization because of the waterfall loop. *)
(*----------------------------------------------------------------------------*)
let checkgen = ref true;;
let generalize_heuristic_ext (tm,(ind:bool)) =
if (mem tm !my_gen_terms & !checkgen) then failwith ""
else
try
(let ELIM_LEMMA lemma th =
let rest = snd (dest_disj (concl th))
in EQ_MP (CONV_RULE (RAND_CONV (REWR_CONV F_OR))
(AP_THM (AP_TERM `(\/)` lemma) rest)) th
in let (tm',subs) = try( generalize_Apart tm ) with Failure _ -> (tm,[])
in let (new_vars,gen_terms) = List.split subs
in let (tm'',subs) = try( generalizeCommonSubterms tm' ) with Failure _ -> (tm',[])
in if (tm = tm'') then failwith ""
else let (new_vars',gen_terms') = List.split subs
in let gen_terms = gen_terms@gen_terms' and new_vars = new_vars @ new_vars'
in let lemmas = []
in let countercheck = try counter_check 5 tm'' with Failure s ->
warn true ("Could not generate counter example: " ^ s) ; true
in if (countercheck = true) then let proof th'' =
let th' = SPECL gen_terms (GENL new_vars th'')
in rev_itlist ELIM_LEMMA lemmas th'
in (proof_print_string_l "-> Generalize Heuristic"() ; my_gen_terms := tm''::!my_gen_terms ; ([(tm'',ind)],apply_proof (proof o hd) [tm'']))
else failwith "Counter example failure!"
) with Failure _ -> failwith "generalize_heuristic";;