1 (******************************************************************************)
2 (* FILE : irrelevance.ml *)
3 (* DESCRIPTION : Eliminating irrelevance. *)
5 (* READS FILES : <none> *)
6 (* WRITES FILES : <none> *)
8 (* AUTHOR : R.J.Boulton *)
9 (* DATE : 25th June 1991 *)
11 (* LAST MODIFIED : R.J.Boulton *)
12 (* DATE : 12th October 1992 *)
14 (* LAST MODIFIED : P. Papapanagiotou (University of Edinburgh) *)
16 (******************************************************************************)
19 let pth = TAUT`!t1 t2. t1 \/ t2 ==> ~t1 ==> t2` in
21 try let a,b = dest_disj(concl th) in MP (SPECL [a;b] pth) th
22 with Failure _ -> failwith "DISJ_IMP";;
25 let pth = TAUT`!t1 t2. (t1 ==> t2) ==> ~t1 \/ t2` in
27 try let a,b = dest_imp(concl th) in MP (SPECL [a;b] pth) th
28 with Failure _ -> failwith "IMP_ELIM";;
30 (*----------------------------------------------------------------------------*)
31 (* partition_literals : (term # int) list -> (term # int) list list *)
33 (* Function to partition a list of numbered terms into lists that share *)
34 (* variables. A term in one partition has no variables in common with any *)
35 (* term in one of the other partitions. Within a partition the terms are *)
36 (* ordered as they were in the input list. *)
38 (* The function begins by putting every term in a separate partition. It then *)
39 (* tries to merge the first partition with one of the others. Two partitions *)
40 (* can be merged if they have at least one variable in common. If a merge can *)
41 (* be done, the process is repeated for the new head of the partition list. *)
42 (* This continues until a merge cannot take place (this causes a failure in *)
43 (* `merge_partitions' due to an attempt to split an empty list into a head *)
44 (* and a tail). When this happens, the head partition is separated from the *)
45 (* others because it cannot have any variables in common with the others. The *)
46 (* entire process is repeated for the remaining partitions. This goes on *)
47 (* until the list is exhausted. *)
49 (* When as much merging as possible has been done, the terms within each *)
50 (* partition are sorted based on the number they are paired with. *)
51 (*----------------------------------------------------------------------------*)
53 let partition_literals tmnl =
54 let rec merge_partitions partition partitions =
55 if (partitions = []) then failwith "merge_partitions"
56 else let h::t = partitions
57 in if ((intersect ((freesl o map fst) partition)
58 ((freesl o map fst) h)) = [])
59 then h::(merge_partitions partition t)
60 else (partition @ h)::t
61 and repeated_merge partitions =
64 else let h::t = partitions
65 in try repeated_merge (merge_partitions h t)
66 with Failure _ -> h::(repeated_merge t)
67 in map sort_on_snd (repeated_merge (map (fun tmn -> [tmn]) tmnl));;
69 (*----------------------------------------------------------------------------*)
70 (* contains_recursive_fun : term list -> bool *)
72 (* Determines whether a list of terms (a partition) mentions a recursive *)
73 (* function. A constant that does not have a definition in the environment is *)
74 (* taken to be non-recursive. *)
75 (*----------------------------------------------------------------------------*)
77 let contains_recursive_fun tml =
78 let consts = flat (mapfilter (find_terms is_const) tml)
79 in let names = setify (map (fst o dest_const) consts)
80 in exists (fun name -> not (try ((fst o get_def) name = 0) with Failure _ -> true)) names;;
82 (*----------------------------------------------------------------------------*)
83 (* is_singleton_rec_app : term list -> bool *)
85 (* Returns true if the list of terms (a partition) given as argument is a *)
86 (* single literal whose atom is of the form (f v1 ... vn) where f is a *)
87 (* recursive function and the vi are distinct variables. *)
88 (*----------------------------------------------------------------------------*)
90 let is_singleton_rec_app tml =
94 let tm' = if (is_neg tm) then (rand tm) else tm
95 in let (f,args) = strip_comb tm'
96 in let name = fst (dest_const f)
97 in (not ((fst o get_def) name = 0)) &
98 (forall is_var args) &
101 ) with Failure _ -> false;;
103 (*----------------------------------------------------------------------------*)
104 (* merge_numbered_lists : ( # int) list -> ( # int) list -> ( # int) list *)
106 (* Merges two numbered lists. The lists must be in increasing order by the *)
107 (* number, and no number may appear more than once in a list or appear in *)
108 (* both lists. The result will then be ordered by the numbers. *)
109 (*----------------------------------------------------------------------------*)
111 let rec merge_numbered_lists xnl1 xnl2 =
112 if (xnl1 = []) then xnl2
113 else if (xnl2 = []) then xnl1
114 else let ((x1,n1)::t1) = xnl1
115 and ((x2,n2)::t2) = xnl2
117 then (x1,n1)::(merge_numbered_lists t1 xnl2)
118 else (x2,n2)::(merge_numbered_lists xnl1 t2);;
120 (*----------------------------------------------------------------------------*)
121 (* find_irrelevant_literals : term -> ((term # int) list # (term # int) list) *)
123 (* Given a clause, this function produces two lists of term/integer pairs. *)
124 (* The first list is of literals deemed to be irrelevant. The second list is *)
125 (* the remaining literals. The number with each literal is its position in *)
126 (* the original clause. *)
127 (*----------------------------------------------------------------------------*)
129 let find_irrelevant_literals tm =
130 let can_be_falsified tmnl =
131 let tml = map fst tmnl
132 in (not (contains_recursive_fun tml)) or (is_singleton_rec_app tml)
133 and tmnll = partition_literals (number_list (disj_list tm))
134 in let (irrels,rels) = partition can_be_falsified tmnll
135 in (itlist merge_numbered_lists irrels [],
136 itlist merge_numbered_lists rels []);;
138 (*----------------------------------------------------------------------------*)
139 (* DISJ_UNDISCH : thm -> thm *)
142 (* ------------- DISJ_UNDISCH *)
144 (*----------------------------------------------------------------------------*)
146 let DISJ_UNDISCH th = try UNDISCH (DISJ_IMP th) with Failure _ -> failwith "DISJ_UNDISCH";;
148 (*----------------------------------------------------------------------------*)
149 (* DISJ_DISCH : term -> thm -> thm *)
152 (* ------------- DISJ_DISCH "x:bool" *)
154 (*----------------------------------------------------------------------------*)
156 let DISJ_DISCH tm th =
158 (CONV_RULE (RATOR_CONV (RAND_CONV (REWR_CONV NOT_NOT_NORM)))
159 (IMP_ELIM (DISCH (mk_neg tm) th))
160 ) with Failure _ -> failwith "DISJ_DISCH";;
162 (*----------------------------------------------------------------------------*)
163 (* BUILD_DISJ : ((term # int) list # (term # int) list) -> thm -> thm *)
165 (* Function to build a disjunctive theorem from another theorem that has as *)
166 (* its conclusion a subset of the disjuncts. The first argument is a pair of *)
167 (* term/integer lists. Each list contains literals (disjuncts) and their *)
168 (* position within the required result. The first list is of those disjuncts *)
169 (* not in the theorem. The second list is of disjuncts in the theorem. Both *)
170 (* lists are assumed to be ordered by their numbers (increasing order). *)
174 (* BUILD_DISJ ([("x2",2);("x5",5);("x6",6)],[("x1",1);("x3",3);("x4",4)]) *)
175 (* |- x1 \/ x3 \/ x4 *)
177 (* The required result is: *)
179 (* |- x1 \/ x2 \/ x3 \/ x4 \/ x5 \/ x6 *)
181 (* The first step is to undischarge all the disjuncts except for the last: *)
185 (* The disjuncts not in the theorem, and which are to come after x4, are now *)
186 (* `added' to the theorem. (Note that we have to undischarge all but the last *)
187 (* disjunct in order to get the correct associativity of OR (\/) at this *)
190 (* ~x1, ~x3 |- x4 \/ x5 \/ x6 *)
192 (* We now repeatedly either discharge one of the assumptions, or add a *)
193 (* disjunct from the `outs' list, according to the values of the numbers *)
194 (* associated with the terms: *)
196 (* ~x1 |- x3 \/ x4 \/ x5 \/ x6 *)
198 (* ~x1 |- x2 \/ x3 \/ x4 \/ x5 \/ x6 *)
200 (* |- x1 \/ x2 \/ x3 \/ x4 \/ x5 \/ x6 *)
201 (*----------------------------------------------------------------------------*)
203 let BUILD_DISJ (outs,ins) inth =
204 try (let rec rebuild rev_outs rev_ins th =
206 then if (rev_outs = [])
208 else rebuild (tl rev_outs) rev_ins (DISJ2 (fst (hd rev_outs)) th)
209 else if (rev_outs = [])
210 then rebuild rev_outs (tl rev_ins) (DISJ_DISCH (fst (hd rev_ins)) th)
211 else let (inh::int) = rev_ins
212 and (outh::outt) = rev_outs
213 in if (snd inh > snd outh)
214 then rebuild rev_outs int (DISJ_DISCH (fst inh) th)
215 else rebuild outt rev_ins (DISJ2 (fst outh) th)
216 in let last_in = snd (last ins)
217 in let (under_outs,over_outs) = partition (fun (_,n) -> n > last_in) outs
218 in let over_ins = butlast ins
219 in let th1 = funpow (length over_ins) DISJ_UNDISCH inth
220 in let th2 = try (DISJ1 th1 (list_mk_disj (map fst under_outs))) with Failure _ -> th1
221 in rebuild (rev over_outs) (rev over_ins) th2
222 ) with Failure _ -> failwith "BUILD_DISJ";;
224 (*----------------------------------------------------------------------------*)
225 (* irrelevance_heuristic : (term # bool) -> ((term # bool) list # proof) *)
227 (* Heuristic for eliminating irrelevant literals. The function splits the *)
228 (* literals into two sets: those that are irrelevant and those that are not. *)
229 (* If there are no relevant terms left, the heuristic fails in a way that *)
230 (* indicates the conjecture cannot be proved. If there are no irrelevant *)
231 (* literals, the function fails indicating that it cannot do anything with *)
232 (* the clause. In all other circumstances the function returns a new clause *)
233 (* consisting of only the relevant literals, together with a proof of the *)
234 (* original clause from this new clause. *)
235 (*----------------------------------------------------------------------------*)
237 let irrelevance_heuristic (tm,(ind:bool)) =
238 let (outs,ins) = find_irrelevant_literals tm
239 in if (ins = []) then failwith "cannot prove"
240 else if (outs = []) then failwith "irrelevance_heuristic"
241 else let tm' = list_mk_disj (map fst ins)
242 and proof = BUILD_DISJ (outs,ins)
243 in (proof_print_string_l "-> Irrelevance Heuristic" () ; ([(tm',ind)],apply_proof (proof o hd) [tm']));;