(******************************************************************************) (* FILE : induction.ml *) (* DESCRIPTION : Induction. *) (* *) (* READS FILES : <none> *) (* WRITES FILES : <none> *) (* *) (* AUTHOR : R.J.Boulton *) (* DATE : 26th June 1991 *) (* *) (* LAST MODIFIED : P. Papapanagiotou (University of Edinburgh) *) (* DATE : 2008 *) (******************************************************************************) let (CONV_OF_RCONV: conv -> conv) = let rec get_bv tm = if is_abs tm then bndvar tm else if is_comb tm then try get_bv (rand tm) with Failure _ -> get_bv (rator tm) else failwith "" in fun conv tm -> let v = get_bv tm in let th1 = conv tm in let th2 = ONCE_DEPTH_CONV (GEN_ALPHA_CONV v) (rhs(concl th1)) in TRANS th1 th2;; let (CONV_OF_THM: thm -> conv) = CONV_OF_RCONV o REWR_CONV;; let RIGHT_IMP_FORALL_CONV = CONV_OF_THM RIGHT_IMP_FORALL_THM;; (* Does this work?? *) (*----------------------------------------------------------------------------*) (* is_rec_const_app : term -> bool *) (* *) (* This function returns true if the term it is given is an application of a *) (* currently known recursive function constant. *) (*----------------------------------------------------------------------------*) let is_rec_const_app tm = try (let (f,args) = strip_comb tm in let (n,defs) = (get_def o fst o dest_const) f in (n > 0) & ((length o snd o strip_comb o lhs o concl o snd o hd) defs = length args) ) with Failure _ -> false;; (*----------------------------------------------------------------------------*) (* possible_inductions : term -> (term list # term list) *) (* *) (* Function to compute two lists of variables on which induction could be *) (* performed. The first list of variables for which the induction is unflawed *) (* and the second is of variables for which the induction is flawed. *) (* *) (* From a list of applications of recursive functions, the arguments are *) (* split into those that are in a recursive argument position and those that *) (* are not. Possible inductions are on the variables in the recursive *) (* argument positions, but if the variable also appears in a non-recursive *) (* argument position then the induction is flawed. *) (*----------------------------------------------------------------------------*) let possible_inductions tm = let apps = find_bm_terms is_rec_const_app tm in let (rec_args,other_args) = List.split (map (fun app -> let (f,args) = strip_comb app in let name = fst (dest_const f) in let n = (fst o get_def) name in remove_el n args) apps) in let vars = setify (filter is_var rec_args) in let others = setify (flat other_args) in partition (fun v -> not (mem v others)) vars;; (*----------------------------------------------------------------------------*) (* DEPTH_FORALL_CONV : conv -> conv *) (* *) (* Given a term of the form "!x1 ... xn. t", this function applies the *) (* argument conversion to "t". *) (*----------------------------------------------------------------------------*) let rec DEPTH_FORALL_CONV conv tm = if (is_forall tm) then RAND_CONV (ABS_CONV (DEPTH_FORALL_CONV conv)) tm else conv tm;; (*----------------------------------------------------------------------------*) (* induction_heuristic : (term # bool) -> ((term # bool) list # proof) *) (* *) (* Heuristic for induction. It performs one of the possible unflawed *) (* inductions on a clause, or failing that, one of the flawed inductions. *) (* The heuristic fails if no inductions are possible. *) (* *) (* Having obtained a variable on which to perform induction, the function *) (* computes the name of the top-level type constructor in the type of the *) (* variable. The appropriate induction theorem is then obtained from the *) (* shell environment. The theorem is specialised for the argument clause and *) (* beta-reduction is performed at the appropriate places. *) (* *) (* The resulting theorem will be of the form: *) (* *) (* |- (case1 /\ ... /\ casen) ==> (!x. f[x]) ( * ) *) (* *) (* So, if we can establish casei for each i, we shall have |- !x. f[x]. When *) (* specialised with the induction variable, this theorem has the original *) (* clause as its conclusion. Each casei is of one of these forms: *) (* *) (* !x1 ... xn. s ==> (!y1 ... ym. t) *) (* !x1 ... xn. t *) (* *) (* where the yi's do not appear in s. We simplify the casei's that have the *) (* first form by proving theorems like: *) (* *) (* |- (!x1 ... xn. s ==> (!y1 ... ym. t)) = *) (* (!x1 ... xn y1 ... ym. s ==> t) *) (* *) (* For consistency, theorems of the form |- (!x1 ... xn. t) = (!x1 ... xn. t) *) (* are proved for the casei's that have the second form. The bodies of the *) (* right-hand sides of these equations are returned as the new goal clauses. *) (* A body that is an implication is taken to be an inductive step and so is *) (* returned paired with true. Bodies that are not implications are paired *) (* with false. *) (* *) (* The proof of the original clause from these new clauses proceeds as *) (* follows. The universal quantifications that were stripped from the *) (* right-hand sides are restored by generalizing the theorems. From the *) (* equations we can then obtain theorems for the left-hand sides. These are *) (* conjoined and used to satisfy the antecedant of the theorem ( * ). As *) (* described above, specialising the resulting theorem gives a theorem for *) (* the original clause. *) (*----------------------------------------------------------------------------*) let induction_heuristic (tm,(ind:bool)) = try (let (unflawed,flawed) = possible_inductions tm in let var = try (hd unflawed) with Failure _ -> (hd flawed) in let ty_name = fst (dest_type (type_of var)) in let induct_thm = (sys_shell_info ty_name).induct in let P = mk_abs (var,tm) in let th1 = ISPEC P induct_thm in let th2 = CONV_RULE (ONCE_DEPTH_CONV (fun tm -> if (rator tm = P) then BETA_CONV tm else failwith "")) th1 in let new_goals = conj_list (rand (rator (concl th2))) in let ths = map (REPEATC (DEPTH_FORALL_CONV RIGHT_IMP_FORALL_CONV)) new_goals in let (varsl,tml) = List.split (map (strip_forall o rhs o concl) ths) in let proof thl = let thl' = map (uncurry GENL) (lcombinep (varsl,thl)) in let thl'' = map (fun (eq,th) -> EQ_MP (SYM eq) th) (lcombinep (ths,thl')) in SPEC var (MP th2 (LIST_CONJ thl'')) in (map (fun tm -> (tm,((is_imp tm) & (not (is_neg tm))))) tml, apply_proof proof tml) ) with Failure _ -> failwith "induction_heuristic";;