(******************************************************************************)
(* FILE : irrelevance.ml *)
(* DESCRIPTION : Eliminating irrelevance. *)
(* *)
(* READS FILES : <none> *)
(* WRITES FILES : <none> *)
(* *)
(* AUTHOR : R.J.Boulton *)
(* DATE : 25th June 1991 *)
(* *)
(* LAST MODIFIED : R.J.Boulton *)
(* DATE : 12th October 1992 *)
(* *)
(* LAST MODIFIED : P. Papapanagiotou (University of Edinburgh) *)
(* DATE : 2008 *)
(******************************************************************************)
let DISJ_IMP =
let pth = TAUT`!t1 t2. t1 \/ t2 ==> ~t1 ==> t2` in
fun th ->
try let a,b = dest_disj(concl th) in MP (SPECL [a;b] pth) th
with Failure _ -> failwith "DISJ_IMP";;
let IMP_ELIM =
let pth = TAUT`!t1 t2. (t1 ==> t2) ==> ~t1 \/ t2` in
fun th ->
try let a,b = dest_imp(concl th) in MP (SPECL [a;b] pth) th
with Failure _ -> failwith "IMP_ELIM";;
(*----------------------------------------------------------------------------*)
(* partition_literals : (term # int) list -> (term # int) list list *)
(* *)
(* Function to partition a list of numbered terms into lists that share *)
(* variables. A term in one partition has no variables in common with any *)
(* term in one of the other partitions. Within a partition the terms are *)
(* ordered as they were in the input list. *)
(* *)
(* The function begins by putting every term in a separate partition. It then *)
(* tries to merge the first partition with one of the others. Two partitions *)
(* can be merged if they have at least one variable in common. If a merge can *)
(* be done, the process is repeated for the new head of the partition list. *)
(* This continues until a merge cannot take place (this causes a failure in *)
(* `merge_partitions' due to an attempt to split an empty list into a head *)
(* and a tail). When this happens, the head partition is separated from the *)
(* others because it cannot have any variables in common with the others. The *)
(* entire process is repeated for the remaining partitions. This goes on *)
(* until the list is exhausted. *)
(* *)
(* When as much merging as possible has been done, the terms within each *)
(* partition are sorted based on the number they are paired with. *)
(*----------------------------------------------------------------------------*)
let partition_literals tmnl =
let rec merge_partitions partition partitions =
if (partitions = []) then failwith "merge_partitions"
else let h::t = partitions
in if ((intersect ((freesl o map fst) partition)
((freesl o map fst) h)) = [])
then h::(merge_partitions partition t)
else (partition @ h)::t
and repeated_merge partitions =
if (partitions = [])
then []
else let h::t = partitions
in try repeated_merge (merge_partitions h t)
with Failure _ -> h::(repeated_merge t)
in map sort_on_snd (repeated_merge (map (fun tmn -> [tmn]) tmnl));;
(*----------------------------------------------------------------------------*)
(* contains_recursive_fun : term list -> bool *)
(* *)
(* Determines whether a list of terms (a partition) mentions a recursive *)
(* function. A constant that does not have a definition in the environment is *)
(* taken to be non-recursive. *)
(*----------------------------------------------------------------------------*)
let contains_recursive_fun tml =
let consts = flat (mapfilter (find_terms is_const) tml)
in let names = setify (map (fst o dest_const) consts)
in exists (fun name -> not (try ((fst o get_def) name = 0) with Failure _ -> true)) names;;
(*----------------------------------------------------------------------------*)
(* is_singleton_rec_app : term list -> bool *)
(* *)
(* Returns true if the list of terms (a partition) given as argument is a *)
(* single literal whose atom is of the form (f v1 ... vn) where f is a *)
(* recursive function and the vi are distinct variables. *)
(*----------------------------------------------------------------------------*)
let is_singleton_rec_app tml =
try (
match (tml) with
| [tm] ->
let tm' = if (is_neg tm) then (rand tm) else tm
in let (f,args) = strip_comb tm'
in let name = fst (dest_const f)
in (not ((fst o get_def) name = 0)) &
(forall is_var args) &
(distinct args)
| _ -> false
) with Failure _ -> false;;
(*----------------------------------------------------------------------------*)
(* merge_numbered_lists : ( # int) list -> ( # int) list -> ( # int) list *)
(* *)
(* Merges two numbered lists. The lists must be in increasing order by the *)
(* number, and no number may appear more than once in a list or appear in *)
(* both lists. The result will then be ordered by the numbers. *)
(*----------------------------------------------------------------------------*)
let rec merge_numbered_lists xnl1 xnl2 =
if (xnl1 = []) then xnl2
else if (xnl2 = []) then xnl1
else let ((x1,n1)::t1) = xnl1
and ((x2,n2)::t2) = xnl2
in if (n1 < n2)
then (x1,n1)::(merge_numbered_lists t1 xnl2)
else (x2,n2)::(merge_numbered_lists xnl1 t2);;
(*----------------------------------------------------------------------------*)
(* find_irrelevant_literals : term -> ((term # int) list # (term # int) list) *)
(* *)
(* Given a clause, this function produces two lists of term/integer pairs. *)
(* The first list is of literals deemed to be irrelevant. The second list is *)
(* the remaining literals. The number with each literal is its position in *)
(* the original clause. *)
(*----------------------------------------------------------------------------*)
let find_irrelevant_literals tm =
let can_be_falsified tmnl =
let tml = map fst tmnl
in (not (contains_recursive_fun tml)) or (is_singleton_rec_app tml)
and tmnll = partition_literals (number_list (disj_list tm))
in let (irrels,rels) = partition can_be_falsified tmnll
in (itlist merge_numbered_lists irrels [],
itlist merge_numbered_lists rels []);;
(*----------------------------------------------------------------------------*)
(* DISJ_UNDISCH : thm -> thm *)
(* *)
(* A |- x \/ y *)
(* ------------- DISJ_UNDISCH *)
(* A, ~x |- y *)
(*----------------------------------------------------------------------------*)
let DISJ_UNDISCH th = try UNDISCH (DISJ_IMP th) with Failure _ -> failwith "DISJ_UNDISCH";;
(*----------------------------------------------------------------------------*)
(* DISJ_DISCH : term -> thm -> thm *)
(* *)
(* A, ~x |- y *)
(* ------------- DISJ_DISCH "x:bool" *)
(* A |- x \/ y *)
(*----------------------------------------------------------------------------*)
let DISJ_DISCH tm th =
try
(CONV_RULE (RATOR_CONV (RAND_CONV (REWR_CONV NOT_NOT_NORM)))
(IMP_ELIM (DISCH (mk_neg tm) th))
) with Failure _ -> failwith "DISJ_DISCH";;
(*----------------------------------------------------------------------------*)
(* BUILD_DISJ : ((term # int) list # (term # int) list) -> thm -> thm *)
(* *)
(* Function to build a disjunctive theorem from another theorem that has as *)
(* its conclusion a subset of the disjuncts. The first argument is a pair of *)
(* term/integer lists. Each list contains literals (disjuncts) and their *)
(* position within the required result. The first list is of those disjuncts *)
(* not in the theorem. The second list is of disjuncts in the theorem. Both *)
(* lists are assumed to be ordered by their numbers (increasing order). *)
(* *)
(* Example: *)
(* *)
(* BUILD_DISJ ([("x2",2);("x5",5);("x6",6)],[("x1",1);("x3",3);("x4",4)]) *)
(* |- x1 \/ x3 \/ x4 *)
(* *)
(* The required result is: *)
(* *)
(* |- x1 \/ x2 \/ x3 \/ x4 \/ x5 \/ x6 *)
(* *)
(* The first step is to undischarge all the disjuncts except for the last: *)
(* *)
(* ~x1, ~x3 |- x4 *)
(* *)
(* The disjuncts not in the theorem, and which are to come after x4, are now *)
(* `added' to the theorem. (Note that we have to undischarge all but the last *)
(* disjunct in order to get the correct associativity of OR (\/) at this *)
(* stage): *)
(* *)
(* ~x1, ~x3 |- x4 \/ x5 \/ x6 *)
(* *)
(* We now repeatedly either discharge one of the assumptions, or add a *)
(* disjunct from the `outs' list, according to the values of the numbers *)
(* associated with the terms: *)
(* *)
(* ~x1 |- x3 \/ x4 \/ x5 \/ x6 *)
(* *)
(* ~x1 |- x2 \/ x3 \/ x4 \/ x5 \/ x6 *)
(* *)
(* |- x1 \/ x2 \/ x3 \/ x4 \/ x5 \/ x6 *)
(*----------------------------------------------------------------------------*)
let BUILD_DISJ (outs,ins) inth =
try (let rec rebuild rev_outs rev_ins th =
if (rev_ins = [])
then if (rev_outs = [])
then th
else rebuild (tl rev_outs) rev_ins (DISJ2 (fst (hd rev_outs)) th)
else if (rev_outs = [])
then rebuild rev_outs (tl rev_ins) (DISJ_DISCH (fst (hd rev_ins)) th)
else let (inh::int) = rev_ins
and (outh::outt) = rev_outs
in if (snd inh > snd outh)
then rebuild rev_outs int (DISJ_DISCH (fst inh) th)
else rebuild outt rev_ins (DISJ2 (fst outh) th)
in let last_in = snd (last ins)
in let (under_outs,over_outs) = partition (fun (_,n) -> n > last_in) outs
in let over_ins = butlast ins
in let th1 = funpow (length over_ins) DISJ_UNDISCH inth
in let th2 = try (DISJ1 th1 (list_mk_disj (map fst under_outs))) with Failure _ -> th1
in rebuild (rev over_outs) (rev over_ins) th2
) with Failure _ -> failwith "BUILD_DISJ";;
(*----------------------------------------------------------------------------*)
(* irrelevance_heuristic : (term # bool) -> ((term # bool) list # proof) *)
(* *)
(* Heuristic for eliminating irrelevant literals. The function splits the *)
(* literals into two sets: those that are irrelevant and those that are not. *)
(* If there are no relevant terms left, the heuristic fails in a way that *)
(* indicates the conjecture cannot be proved. If there are no irrelevant *)
(* literals, the function fails indicating that it cannot do anything with *)
(* the clause. In all other circumstances the function returns a new clause *)
(* consisting of only the relevant literals, together with a proof of the *)
(* original clause from this new clause. *)
(*----------------------------------------------------------------------------*)
let irrelevance_heuristic (tm,(ind:bool)) =
let (outs,ins) = find_irrelevant_literals tm
in if (ins = []) then failwith "cannot prove"
else if (outs = []) then failwith "irrelevance_heuristic"
else let tm' = list_mk_disj (map fst ins)
and proof = BUILD_DISJ (outs,ins)
in (proof_print_string_l "-> Irrelevance Heuristic" () ; ([(tm',ind)],apply_proof (proof o hd) [tm']));;