Boyer_Moore/irrelevance.ml

   1 (******************************************************************************)
   2 (* FILE          : irrelevance.ml                                             *)
   3 (* DESCRIPTION   : Eliminating irrelevance.                                   *)
   4 (*                                                                            *)
   5 (* READS FILES   : <none>                                                     *)
   6 (* WRITES FILES  : <none>                                                     *)
   7 (*                                                                            *)
   8 (* AUTHOR        : R.J.Boulton                                                *)
   9 (* DATE          : 25th June 1991                                             *)
  10 (*                                                                            *)
  11 (* LAST MODIFIED : R.J.Boulton                                                *)
  12 (* DATE          : 12th October 1992                                          *)
  13 (*                                                                            *)
  14 (* LAST MODIFIED : P. Papapanagiotou (University of Edinburgh)                *)
  15 (* DATE          : 2008                                                       *)
  16 (******************************************************************************)
  17
  18 let DISJ_IMP =
  19   let pth = TAUT`!t1 t2. t1 \/ t2 ==> ~t1 ==> t2` in
  20   fun th ->
  21     try let a,b = dest_disj(concl th) in MP (SPECL [a;b] pth) th
  22     with Failure _ -> failwith "DISJ_IMP";;
  23
  24 let IMP_ELIM =
  25   let pth = TAUT`!t1 t2. (t1 ==> t2) ==> ~t1 \/ t2` in
  26   fun th ->
  27     try let a,b = dest_imp(concl th) in MP (SPECL [a;b] pth) th
  28     with Failure _ -> failwith "IMP_ELIM";;
  29
  30 (*----------------------------------------------------------------------------*)
  31 (* partition_literals : (term # int) list -> (term # int) list list           *)
  32 (*                                                                            *)
  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.                                    *)
  37 (*                                                                            *)
  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.                                               *)
  48 (*                                                                            *)
  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 (*----------------------------------------------------------------------------*)
  52
  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 =
  62       if (partitions = [])
  63       then []
  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));;
  68
  69 (*----------------------------------------------------------------------------*)
  70 (* contains_recursive_fun : term list -> bool                                 *)
  71 (*                                                                            *)
  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 (*----------------------------------------------------------------------------*)
  76
  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;;
  81
  82 (*----------------------------------------------------------------------------*)
  83 (* is_singleton_rec_app : term list -> bool                                   *)
  84 (*                                                                            *)
  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 (*----------------------------------------------------------------------------*)
  89
  90 let is_singleton_rec_app tml =
  91 try  (
  92   match (tml) with
  93   | [tm] ->
  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) &
  99       (distinct args)
 100   | _ -> false
 101  ) with Failure _ -> false;;
 102
 103 (*----------------------------------------------------------------------------*)
 104 (* merge_numbered_lists : ( # int) list -> ( # int) list -> ( # int) list  *)
 105 (*                                                                            *)
 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 (*----------------------------------------------------------------------------*)
 110
 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
 116         in  if (n1 < n2)
 117             then (x1,n1)::(merge_numbered_lists t1 xnl2)
 118             else (x2,n2)::(merge_numbered_lists xnl1 t2);;
 119
 120 (*----------------------------------------------------------------------------*)
 121 (* find_irrelevant_literals : term -> ((term # int) list # (term # int) list) *)
 122 (*                                                                            *)
 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 (*----------------------------------------------------------------------------*)
 128
 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 []);;
 137
 138 (*----------------------------------------------------------------------------*)
 139 (* DISJ_UNDISCH : thm -> thm                                                  *)
 140 (*                                                                            *)
 141 (*     A |- x \/ y                                                            *)
 142 (*    -------------  DISJ_UNDISCH                                             *)
 143 (*     A, ~x |- y                                                             *)
 144 (*----------------------------------------------------------------------------*)
 145
 146 let DISJ_UNDISCH th = try UNDISCH (DISJ_IMP th) with Failure _ -> failwith "DISJ_UNDISCH";;
 147
 148 (*----------------------------------------------------------------------------*)
 149 (* DISJ_DISCH : term -> thm -> thm                                            *)
 150 (*                                                                            *)
 151 (*     A, ~x |- y                                                             *)
 152 (*    -------------  DISJ_DISCH "x:bool"                                      *)
 153 (*     A |- x \/ y                                                            *)
 154 (*----------------------------------------------------------------------------*)
 155
 156 let DISJ_DISCH tm th =
 157 try
 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";;
 161
 162 (*----------------------------------------------------------------------------*)
 163 (* BUILD_DISJ : ((term # int) list # (term # int) list) -> thm -> thm         *)
 164 (*                                                                            *)
 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).       *)
 171 (*                                                                            *)
 172 (* Example:                                                                   *)
 173 (*                                                                            *)
 174 (*    BUILD_DISJ ([("x2",2);("x5",5);("x6",6)],[("x1",1);("x3",3);("x4",4)])  *)
 175 (*               |- x1 \/ x3 \/ x4                                            *)
 176 (*                                                                            *)
 177 (* The required result is:                                                    *)
 178 (*                                                                            *)
 179 (*    |- x1 \/ x2 \/ x3 \/ x4 \/ x5 \/ x6                                     *)
 180 (*                                                                            *)
 181 (* The first step is to undischarge all the disjuncts except for the last:    *)
 182 (*                                                                            *)
 183 (*    ~x1, ~x3 |- x4                                                          *)
 184 (*                                                                            *)
 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      *)
 188 (* stage):                                                                    *)
 189 (*                                                                            *)
 190 (*    ~x1, ~x3 |- x4 \/ x5 \/ x6                                              *)
 191 (*                                                                            *)
 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:                                                 *)
 195 (*                                                                            *)
 196 (*    ~x1 |- x3 \/ x4 \/ x5 \/ x6                                             *)
 197 (*                                                                            *)
 198 (*    ~x1 |- x2 \/ x3 \/ x4 \/ x5 \/ x6                                       *)
 199 (*                                                                            *)
 200 (*    |- x1 \/ x2 \/ x3 \/ x4 \/ x5 \/ x6                                     *)
 201 (*----------------------------------------------------------------------------*)
 202
 203 let BUILD_DISJ (outs,ins) inth =
 204 try (let rec rebuild rev_outs rev_ins th =
 205      if (rev_ins = [])
 206      then if (rev_outs = [])
 207           then th
 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";;
 223
 224 (*----------------------------------------------------------------------------*)
 225 (* irrelevance_heuristic : (term # bool) -> ((term # bool) list # proof)      *)
 226 (*                                                                            *)
 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 (*----------------------------------------------------------------------------*)
 236
 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']));;