(******************************************************************************)
(* 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";;