1 (******************************************************************************)
2 (* FILE : induction.ml *)
3 (* DESCRIPTION : Induction. *)
5 (* READS FILES : <none> *)
6 (* WRITES FILES : <none> *)
8 (* AUTHOR : R.J.Boulton *)
9 (* DATE : 26th June 1991 *)
11 (* LAST MODIFIED : P. Papapanagiotou (University of Edinburgh) *)
13 (******************************************************************************)
15 let (CONV_OF_RCONV: conv -> conv) =
17 if is_abs tm then bndvar tm
18 else if is_comb tm then
19 try get_bv (rand tm) with Failure _ -> get_bv (rator tm)
24 let th2 = ONCE_DEPTH_CONV (GEN_ALPHA_CONV v) (rhs(concl th1)) in
27 let (CONV_OF_THM: thm -> conv) =
28 CONV_OF_RCONV o REWR_CONV;;
30 let RIGHT_IMP_FORALL_CONV = CONV_OF_THM RIGHT_IMP_FORALL_THM;;
31 (* Does this work?? *)
33 (*----------------------------------------------------------------------------*)
34 (* is_rec_const_app : term -> bool *)
36 (* This function returns true if the term it is given is an application of a *)
37 (* currently known recursive function constant. *)
38 (*----------------------------------------------------------------------------*)
40 let is_rec_const_app tm =
41 try (let (f,args) = strip_comb tm
42 in let (n,defs) = (get_def o fst o dest_const) f
44 ((length o snd o strip_comb o lhs o concl o snd o hd) defs = length args)
45 ) with Failure _ -> false;;
48 (*----------------------------------------------------------------------------*)
49 (* possible_inductions : term -> (term list # term list) *)
51 (* Function to compute two lists of variables on which induction could be *)
52 (* performed. The first list of variables for which the induction is unflawed *)
53 (* and the second is of variables for which the induction is flawed. *)
55 (* From a list of applications of recursive functions, the arguments are *)
56 (* split into those that are in a recursive argument position and those that *)
57 (* are not. Possible inductions are on the variables in the recursive *)
58 (* argument positions, but if the variable also appears in a non-recursive *)
59 (* argument position then the induction is flawed. *)
60 (*----------------------------------------------------------------------------*)
62 let possible_inductions tm =
63 let apps = find_bm_terms is_rec_const_app tm
64 in let (rec_args,other_args) =
65 List.split (map (fun app -> let (f,args) = strip_comb app
66 in let name = fst (dest_const f)
67 in let n = (fst o get_def) name
68 in remove_el n args) apps)
69 in let vars = setify (filter is_var rec_args)
70 in let others = setify (flat other_args)
71 in partition (fun v -> not (mem v others)) vars;;
73 (*----------------------------------------------------------------------------*)
74 (* DEPTH_FORALL_CONV : conv -> conv *)
76 (* Given a term of the form "!x1 ... xn. t", this function applies the *)
77 (* argument conversion to "t". *)
78 (*----------------------------------------------------------------------------*)
80 let rec DEPTH_FORALL_CONV conv tm =
82 then RAND_CONV (ABS_CONV (DEPTH_FORALL_CONV conv)) tm
85 (*----------------------------------------------------------------------------*)
86 (* induction_heuristic : (term # bool) -> ((term # bool) list # proof) *)
88 (* Heuristic for induction. It performs one of the possible unflawed *)
89 (* inductions on a clause, or failing that, one of the flawed inductions. *)
90 (* The heuristic fails if no inductions are possible. *)
92 (* Having obtained a variable on which to perform induction, the function *)
93 (* computes the name of the top-level type constructor in the type of the *)
94 (* variable. The appropriate induction theorem is then obtained from the *)
95 (* shell environment. The theorem is specialised for the argument clause and *)
96 (* beta-reduction is performed at the appropriate places. *)
98 (* The resulting theorem will be of the form: *)
100 (* |- (case1 /\ ... /\ casen) ==> (!x. f[x]) ( * ) *)
102 (* So, if we can establish casei for each i, we shall have |- !x. f[x]. When *)
103 (* specialised with the induction variable, this theorem has the original *)
104 (* clause as its conclusion. Each casei is of one of these forms: *)
106 (* !x1 ... xn. s ==> (!y1 ... ym. t) *)
109 (* where the yi's do not appear in s. We simplify the casei's that have the *)
110 (* first form by proving theorems like: *)
112 (* |- (!x1 ... xn. s ==> (!y1 ... ym. t)) = *)
113 (* (!x1 ... xn y1 ... ym. s ==> t) *)
115 (* For consistency, theorems of the form |- (!x1 ... xn. t) = (!x1 ... xn. t) *)
116 (* are proved for the casei's that have the second form. The bodies of the *)
117 (* right-hand sides of these equations are returned as the new goal clauses. *)
118 (* A body that is an implication is taken to be an inductive step and so is *)
119 (* returned paired with true. Bodies that are not implications are paired *)
122 (* The proof of the original clause from these new clauses proceeds as *)
123 (* follows. The universal quantifications that were stripped from the *)
124 (* right-hand sides are restored by generalizing the theorems. From the *)
125 (* equations we can then obtain theorems for the left-hand sides. These are *)
126 (* conjoined and used to satisfy the antecedant of the theorem ( * ). As *)
127 (* described above, specialising the resulting theorem gives a theorem for *)
128 (* the original clause. *)
129 (*----------------------------------------------------------------------------*)
131 let induction_heuristic (tm,(ind:bool)) =
133 (let (unflawed,flawed) = possible_inductions tm
134 in let var = try (hd unflawed) with Failure _ -> (hd flawed)
135 in let ty_name = fst (dest_type (type_of var))
136 in let induct_thm = (sys_shell_info ty_name).induct
137 in let P = mk_abs (var,tm)
138 in let th1 = ISPEC P induct_thm
142 (fun tm -> if (rator tm = P) then BETA_CONV tm else failwith "")) th1
143 in let new_goals = conj_list (rand (rator (concl th2)))
145 map (REPEATC (DEPTH_FORALL_CONV RIGHT_IMP_FORALL_CONV)) new_goals
146 in let (varsl,tml) = List.split (map (strip_forall o rhs o concl) ths)
148 let thl' = map (uncurry GENL) (lcombinep (varsl,thl))
149 in let thl'' = map (fun (eq,th) -> EQ_MP (SYM eq) th) (lcombinep (ths,thl'))
150 in SPEC var (MP th2 (LIST_CONJ thl''))
151 in (map (fun tm -> (tm,((is_imp tm) & (not (is_neg tm))))) tml,
152 apply_proof proof tml)
153 ) with Failure _ -> failwith "induction_heuristic";;