Boyer_Moore/equalities.ml

   1 (******************************************************************************)
   2 (* FILE          : equalities.ml                                              *)
   3 (* DESCRIPTION   : Using equalities.                                          *)
   4 (*                                                                            *)
   5 (* READS FILES   : <none>                                                     *)
   6 (* WRITES FILES  : <none>                                                     *)
   7 (*                                                                            *)
   8 (* AUTHOR        : R.J.Boulton                                                *)
   9 (* DATE          : 19th June 1991                                             *)
  10 (*                                                                            *)
  11 (* LAST MODIFIED : R.J.Boulton                                                *)
  12 (* DATE          : 7th August 1992                                            *)
  13 (*                                                                            *)
  14 (* LAST MODIFIED : P. Papapanagiotou (University of Edinburgh)                *)
  15 (* DATE          : 2008                                                       *)
  16 (******************************************************************************)
  17
  18 (*----------------------------------------------------------------------------*)
  19 (* is_explicit_value_template : term -> bool                                  *)
  20 (*                                                                            *)
  21 (* Function to compute whether a term is an explicit value template.          *)
  22 (* An explicit value template is a non-variable term composed entirely of     *)
  23 (* T or F or variables or applications of shell constructors.                 *)
  24 (* A `bottom object' corresponds to an application to no arguments. I have    *)
  25 (* also made numeric constants valid components of explicit value templates,  *)
  26 (* since they are equivalent to some number of applications of SUC to 0.      *)
  27 (*----------------------------------------------------------------------------*)
  28
  29 let is_explicit_value_template tm =
  30    let rec is_explicit_value_template' constructors tm =
  31       (is_T tm) or (is_F tm) or ((is_const tm) & (type_of tm = `:num`)) or
  32       (is_var tm) or (is_numeral tm) or
  33       (let (f,args) = strip_comb tm
  34        in  (try(mem (fst (dest_const f)) constructors) with Failure _ -> false) &
  35            (forall (is_explicit_value_template' constructors) args))
  36    in (not (is_var tm)) &
  37       (is_explicit_value_template' (all_constructors ()) tm);;
  38
  39 (*----------------------------------------------------------------------------*)
  40 (* subst_conv : thm -> conv                                                   *)
  41 (*                                                                            *)
  42 (* Substitution conversion. Given a theorem |- l = r, it replaces all         *)
  43 (* occurrences of l in the term with r.                                       *)
  44 (*----------------------------------------------------------------------------*)
  45
  46 let subst_conv th tm = SUBST_CONV [(th,lhs (concl th))] tm tm;;
  47
  48 (*----------------------------------------------------------------------------*)
  49 (* use_equality_subst : bool -> bool -> thm -> conv                           *)
  50 (*                                                                            *)
  51 (* Function to perform substitution when using equalities. The first argument *)
  52 (* is a Boolean that controls which side of an equation substitution is to    *)
  53 (* take place on. The second argument is also a Boolean, indicating whether   *)
  54 (* or not we have decided to cross-fertilize. The third argument is a         *)
  55 (* substitution theorem of the form:                                          *)
  56 (*                                                                            *)
  57 (*    t' = s' |- t' = s'                                                      *)
  58 (*                                                                            *)
  59 (* If we are not cross-fertilizing, s' is substituted for t' throughout the   *)
  60 (* term. If we are cross-fertilizing, the behaviour depends on the structure  *)
  61 (* of the term, tm:                                                           *)
  62 (*                                                                            *)
  63 (*    (a) if tm is "l = r", substitute s' for t' in either r or l.            *)
  64 (*    (b) if tm is "~(l = r)", substitute s' for t' throughout tm.            *)
  65 (*    (c) otherwise, do not substitute.                                       *)
  66 (*----------------------------------------------------------------------------*)
  67
  68 (* The heuristic above is modified so that in case (c) a substitution does    *)
  69 (* take place. This reduces the chances of an invalid subgoal (clause) being  *)
  70 (* generated, and has been shown to be a better option for certain examples.  *)
  71
  72 let use_equality_subst right cross_fert th tm =
  73  try (if cross_fert
  74   then if (is_eq tm) then
  75           (if right
  76            then RAND_CONV (subst_conv th) tm
  77            else RATOR_CONV (RAND_CONV (subst_conv th)) tm)
  78        else if ((is_neg tm) & (try(is_eq (rand tm)) with Failure _ -> false)) then subst_conv th tm
  79        else (* ALL_CONV tm *) subst_conv th tm
  80   else subst_conv th tm
  81  ) with Failure _ -> failwith "use_equality_subst";;
  82
  83 (*----------------------------------------------------------------------------*)
  84 (* EQ_EQ_IMP_DISJ_EQ =                                                        *)
  85 (* |- !x x' y y'. (x = x') /\ (y = y') ==> (x \/ y = x' \/ y')                *)
  86 (*----------------------------------------------------------------------------*)
  87
  88 let EQ_EQ_IMP_DISJ_EQ =
  89  prove
  90   (`!x x' y y'. (x = x') /\ (y = y') ==> ((x \/ y) = (x' \/ y'))`,
  91    REPEAT STRIP_TAC THEN
  92    ASM_REWRITE_TAC []);;
  93
  94 (*----------------------------------------------------------------------------*)
  95 (* DISJ_EQ : thm -> thm -> thm                                                *)
  96 (*                                                                            *)
  97 (*     |- x = x'    |- y = y'                                                 *)
  98 (*    ------------------------                                                *)
  99 (*    |- (x \/ y) = (x' \/ y')                                                *)
 100 (*----------------------------------------------------------------------------*)
 101
 102 let DISJ_EQ th1 th2 =
 103 try
 104  (let (x,x') = dest_eq (concl th1)
 105   and (y,y') = dest_eq (concl th2)
 106   in  MP (SPECL [x;x';y;y'] EQ_EQ_IMP_DISJ_EQ) (CONJ th1 th2)
 107  ) with Failure _ -> failwith "DISJ_EQ";;
 108
 109 (*----------------------------------------------------------------------------*)
 110 (* use_equality_heuristic : (term # bool) -> ((term # bool) list # proof)     *)
 111 (*                                                                            *)
 112 (* Heuristic for using equalities, and in particular for cross-fertilizing.   *)
 113 (* Given a clause, the function looks for a literal of the form ~(s' = t')    *)
 114 (* where t' occurs in another literal and is not an explicit value template.  *)
 115 (* If no such literal is present, the function looks for a literal of the     *)
 116 (* form ~(t' = s') where t' occurs in another literal and is not an explicit  *)
 117 (* value template. If a substitution literal of one of these two forms is     *)
 118 (* found, substitution takes place as follows.                                *)
 119 (*                                                                            *)
 120 (* If the clause is an induction step, and there is an equality literal       *)
 121 (* mentioning t' on the RHS (or LHS if the substitution literal was           *)
 122 (* ~(t' = s')), and s' is not an explicit value, the function performs a      *)
 123 (* cross-fertilization. The substitution function is called for each literal  *)
 124 (* other than the substitution literal. Each call results in a theorem of the *)
 125 (* form:                                                                      *)
 126 (*                                                                            *)
 127 (*    t' = s' |- old_lit = new_lit                                            *)
 128 (*                                                                            *)
 129 (* If the clause is an induction step and s' is not an explicit value, the    *)
 130 (* substitution literal is rewritten to F, and so will subsequently be        *)
 131 (* eliminated. Otherwise this literal is unchanged. The theorems for each     *)
 132 (* literal are recombined using the DISJ_EQ rule, and the new clause is       *)
 133 (* returned. See the comments for the substitution heuristic for a            *)
 134 (* description of how the original clause is proved from the new clause.      *)
 135 (*----------------------------------------------------------------------------*)
 136
 137 let use_equality_heuristic (tm,(ind:bool)) =
 138 try (let checkx (tml1,tml2) t' =
 139      (not (is_explicit_value_template t')) &
 140      ((exists (is_subterm t') tml1) or (exists (is_subterm t') tml2))
 141   in  let rec split_disjuncts side prevl tml =
 142          if (can (check (checkx (prevl,tl tml)) o side o dest_neg) (hd tml))
 143          then (prevl,tml)
 144          else split_disjuncts side ((hd tml)::prevl) (tl tml)
 145   in  let is_subterm_of_side side subterm tm =
 146          (try(is_subterm subterm (side tm)) with Failure _ -> false)
 147   in  let literals = disj_list tm
 148   in  let (right,(overs,neq'::unders)) =
 149         try (true,(hashI rev) (split_disjuncts rhs [] literals)) with Failure _ ->
 150          (false,(hashI rev) (split_disjuncts lhs [] literals))
 151   in  let side = if right then rhs else lhs
 152   in  let flipth = if right then ALL_CONV neq' else RAND_CONV SYM_CONV neq'
 153   in  let neq = rhs (concl flipth)
 154   in  let eq = dest_neg neq
 155   in  let (s',t') = dest_eq eq
 156   in  let delete = ind & (not (is_explicit_value s'))
 157   in  let cross_fert = delete &
 158                        ((exists (is_subterm_of_side side t') overs) or
 159                         (exists (is_subterm_of_side side t') unders))
 160   in  let sym_eq = mk_eq (t',s')
 161   in  let sym_neq = mk_neg sym_eq
 162   in  let ass1 = EQ_MP (SYM flipth) (NOT_EQ_SYM (ASSUME sym_neq))
 163       and ass2 = ASSUME sym_eq
 164   in  let subsfun = use_equality_subst right cross_fert ass2
 165   in  let overths = map subsfun overs
 166       and neqth =
 167          if delete
 168          then TRANS (RAND_CONV (RAND_CONV (subst_conv ass2)) neq)
 169               (ISPEC s' NOT_EQ_F)
 170          else ADD_ASSUM sym_eq (REFL neq)
 171       and underths = map subsfun unders
 172   in  let neqth' = TRANS flipth neqth
 173   in  let th1 = itlist DISJ2 overs (try DISJ1 ass1 (list_mk_disj unders) with Failure _ -> ass1)
 174       and th2 = itlist DISJ_EQ overths (end_itlist DISJ_EQ (neqth'::underths))
 175       and th3 = SPEC sym_eq EXCLUDED_MIDDLE
 176   in  let tm' = rhs (concl th2)
 177   in  let proof th = DISJ_CASES th3 (EQ_MP (SYM th2) th) th1
 178   in  (proof_print_string_l "-> Use Equality Heuristic" () ; ([(tm',ind)],apply_proof (proof o hd) [tm']))
 179  ) with Failure _ -> failwith "use_equality_heuristic`";