Boyer_Moore/rewrite_rules.ml

   1 (******************************************************************************)
   2 (* FILE          : rewrite_rules.ml                                           *)
   3 (* DESCRIPTION   : Using axioms and lemmas as rewrite rules.                  *)
   4 (*                                                                            *)
   5 (* READS FILES   : <none>                                                     *)
   6 (* WRITES FILES  : <none>                                                     *)
   7 (*                                                                            *)
   8 (* AUTHOR        : R.J.Boulton                                                *)
   9 (* DATE          : 14th May 1991                                              *)
  10 (*                                                                            *)
  11 (* LAST MODIFIED : R.J.Boulton                                                *)
  12 (* DATE          : 15th October 1992                                          *)
  13 (*                                                                            *)
  14 (* LAST MODIFIED : P. Papapanagiotou (University of Edinburgh)                *)
  15 (* DATE          : 2008                                                       *)
  16 (******************************************************************************)
  17
  18 (*----------------------------------------------------------------------------*)
  19 (* is_permutative : term -> bool                                              *)
  20 (*                                                                            *)
  21 (* Determines whether or not an equation is permutative (the left-hand and    *)
  22 (* right-hand sides are instances of one another). A permutative equation may *)
  23 (* cause looping when it is used for rewriting.                               *)
  24 (*----------------------------------------------------------------------------*)
  25
  26 let is_permutative tm =
  27  try (let (l,r) = dest_eq tm
  28   in  let bind1 = term_match [] l r
  29       and bind2 = term_match [] r l
  30   in  true
  31  ) with Failure _ -> false;;
  32
  33
  34 (*----------------------------------------------------------------------------*)
  35 (* lex_smaller_term : term -> term -> bool                                    *)
  36 (*                                                                            *)
  37 (* Computes whether the first term is `alphabetically' smaller than the       *)
  38 (* second term. Used to avoid looping when rewriting with permutative rules.  *)
  39 (*                                                                            *)
  40 (* A constant is considered to be smaller than a variable which in turn is    *)
  41 (* considered to be smaller than an application. Two variables or two         *)
  42 (* constants are compared alphabetically by name. An application (f1 x1) is   *)
  43 (* considered to be smaller than another application (f2 x2) if either f1 is  *)
  44 (* smaller than f2, or f1 equals f2 and x1 is smaller than x2.                *)
  45 (*----------------------------------------------------------------------------*)
  46
  47 let rec lex_smaller_term tm1 tm2 =
  48 try
  49  (if (is_const tm1) then
  50      (if (is_const tm2)
  51       then let (name1,type1) = dest_const tm1
  52            and (name2,type2) = dest_const tm2
  53            in  (if (type1 = type2)
  54                 then name1 < name2
  55                 else failwith "" )
  56       else true)
  57   else if (is_var tm1) then
  58      (if (is_const tm2) then false
  59       else if (is_var tm2)
  60       then let (name1,type1) = dest_var tm1
  61            and (name2,type2) = dest_var tm2
  62            in  (if (type1 = type2)
  63                 then name1 < name2
  64                 else failwith "" )
  65       else true)
  66   else if (is_comb tm1) then
  67      (if (is_comb tm2)
  68       then let (rator1,rand1) = dest_comb tm1
  69            and (rator2,rand2) = dest_comb tm2
  70            in  (lex_smaller_term rator1 rator2) or
  71                ((rator1 = rator2) & (lex_smaller_term rand1 rand2))
  72       else false)
  73   else failwith ""
  74  ) with Failure _ -> failwith "lex_smaller_term";;
  75
  76 (*----------------------------------------------------------------------------*)
  77 (* inst_eq_thm : ((term # term) list # (type # type) list) -> thm -> thm      *)
  78 (*                                                                            *)
  79 (* Instantiates a theorem (possibly having hypotheses) with a binding.        *)
  80 (* Assumes the conclusion is an equality, so that discharging then undisching *)
  81 (* cannot cause parts of the conclusion to be moved into the hypotheses.      *)
  82 (*----------------------------------------------------------------------------*)
  83
  84 let inst_eq_thm (tm_bind,ty_bind) th =
  85    let (insts,vars) = List.split tm_bind
  86    in  (UNDISCH_ALL o (SPECL insts) o (GENL vars) o
  87         (INST_TYPE ty_bind) o DISCH_ALL) th;;
  88
  89 (*----------------------------------------------------------------------------*)
  90 (* applicable_rewrites : term -> thm list                                     *)
  91 (*                                                                            *)
  92 (* Returns the results of rewriting the term with those rewrite rules that    *)
  93 (* are applicable to it. A rewrite rule is not applicable if it's permutative *)
  94 (* and the rewriting does not produce an alphabetically smaller term.         *)
  95 (*----------------------------------------------------------------------------*)
  96
  97 let applicable_rewrites tm =
  98    let applicable_rewrite tm th =
  99       let conc = concl th
 100       in  let (_,tm_bind,ty_bind) = term_match [] (lhs conc) tm
 101       in  let instth = inst_eq_thm (tm_bind,ty_bind) th
 102       in  if (is_permutative conc)
 103           then (let (l,r) = dest_eq (concl instth)
 104                 in  if (lex_smaller_term r l)
 105                     then instth
 106                     else failwith "")
 107           else instth
 108    in  mapfilter ((applicable_rewrite tm) o snd) !system_rewrites;;
 109
 110 (*----------------------------------------------------------------------------*)
 111 (* ARGS_CONV : conv -> conv                                                   *)
 112 (*                                                                            *)
 113 (* Applies a conversion to every argument of an application of the form       *)
 114 (* "f x1 ... xn".                                                             *)
 115 (*----------------------------------------------------------------------------*)
 116
 117 let rec ARGS_CONV conv tm =
 118 try (
 119  ((RATOR_CONV (ARGS_CONV conv)) THENC (RAND_CONV conv)) tm
 120  ) with Failure _ -> ALL_CONV tm;;
 121
 122 (*----------------------------------------------------------------------------*)
 123 (* assump_inst_hyps : term list ->                                            *)
 124 (*                    term ->                                                 *)
 125 (*                    term list ->                                            *)
 126 (*                    ((term # term) list # (type # type) list)               *)
 127 (*                                                                            *)
 128 (* Searches a list of hypotheses for one that matches the specified           *)
 129 (* assumption such that the variables instantiated are precisely those in the *)
 130 (* list of variables given. If such a hypothesis is found, the binding        *)
 131 (* produced by the match is returned.                                         *)
 132 (*----------------------------------------------------------------------------*)
 133
 134 let rec assump_inst_hyps vars assump hyps =
 135  try(let (_,tm_bind,ty_bind) = term_match [] (hd hyps) assump
 136   in let bind = (tm_bind,ty_bind)
 137   in  if (set_eq vars (map snd (fst bind)))
 138       then bind
 139       else failwith "")
 140  with Failure _ -> try (assump_inst_hyps vars assump (tl hyps))
 141  with Failure _ -> failwith "assump_inst_hyps";;
 142
 143 (*----------------------------------------------------------------------------*)
 144 (* assumps_inst_hyps : term list ->                                           *)
 145 (*                     term list ->                                           *)
 146 (*                     term list ->                                           *)
 147 (*                     ((term # term) list # (type # type) list)              *)
 148 (*                                                                            *)
 149 (* Searches a list of hypotheses and a list of assumptions for a pairing that *)
 150 (* match (the assumption is an instance of the hypothesis) such that the      *)
 151 (* variables instantiated are precisely those in the list of variables given. *)
 152 (* If such a pair is found, the binding produced by the match is returned.    *)
 153 (*----------------------------------------------------------------------------*)
 154
 155 let rec assumps_inst_hyps vars assumps hyps =
 156  try (assump_inst_hyps vars (hd assumps) hyps)
 157  with Failure _ -> try (assumps_inst_hyps vars (tl assumps) hyps)
 158  with Failure _ -> failwith "assumps_inst_hyps";;
 159
 160 (*----------------------------------------------------------------------------*)
 161 (* inst_frees_in_hyps : term list -> thm -> thm                               *)
 162 (*                                                                            *)
 163 (* Takes a theorem (possibly with hypotheses) and computes a list of          *)
 164 (* variables that are free in the hypotheses but not in the conclusion.       *)
 165 (* If this list of variables is empty the original theorem is returned.       *)
 166 (* The function also takes a list of assumptions as another argument. Once it *)
 167 (* has the list of variables it searches for an assumption and a hypothesis   *)
 168 (* such that the hypothesis matches the assumption binding precisely those    *)
 169 (* variables in the list. If this is successful the original theorem is       *)
 170 (* returned having had the variables in the list instantiated.                *)
 171 (*----------------------------------------------------------------------------*)
 172
 173 let inst_frees_in_hyps assumps th =
 174  try (let hyps = hyp th
 175   in  let hyp_frees = setify (flat (map frees hyps))
 176   in  let vars = subtract hyp_frees (frees (concl th))
 177   in  if (vars = [])
 178       then th
 179       else let bind = assumps_inst_hyps vars assumps hyps
 180            in  inst_eq_thm bind th
 181  ) with Failure _ -> failwith "inst_frees_in_hyps";;
 182
 183 (*----------------------------------------------------------------------------*)
 184 (* NOT_IMP_EQ_EQ_EQ_OR = |- (~x ==> (y = y')) = ((y \/ x) = (y' \/ x))        *)
 185 (*----------------------------------------------------------------------------*)
 186
 187 let NOT_IMP_EQ_EQ_EQ_OR =
 188  prove
 189   (`(~x ==> (y = y')) = ((y \/ x) = (y' \/ x))`,
 190    BOOL_CASES_TAC `x:bool` THEN
 191    BOOL_CASES_TAC `y:bool` THEN
 192    BOOL_CASES_TAC `y':bool` THEN
 193    REWRITE_TAC []);;
 194
 195 (*----------------------------------------------------------------------------*)
 196 (* IMP_EQ_EQ_EQ_OR_NOT = |- (x ==> (y = y')) = ((y \/ ~x) = (y' \/ ~x))       *)
 197 (*----------------------------------------------------------------------------*)
 198
 199 let IMP_EQ_EQ_EQ_OR_NOT =
 200  prove
 201   (`(x ==> (y = y')) = ((y \/ ~x) = (y' \/ ~x))`,
 202    BOOL_CASES_TAC `x:bool` THEN
 203    BOOL_CASES_TAC `y:bool` THEN
 204    BOOL_CASES_TAC `y':bool` THEN
 205    REWRITE_TAC []);;
 206
 207 (*----------------------------------------------------------------------------*)
 208 (* NOT_IMP_EQ_OR_EQ_EQ_OR_OR =                                                *)
 209 (* |- (~x ==> ((y \/ t) = (y' \/ t))) = ((y \/ (x \/ t)) = (y' \/ (x \/ t)))  *)
 210 (*----------------------------------------------------------------------------*)
 211
 212 let NOT_IMP_EQ_OR_EQ_EQ_OR_OR =
 213  prove
 214   (`(~x ==> ((y \/ t) = (y' \/ t))) = ((y \/ (x \/ t)) = (y' \/ (x \/ t)))`,
 215    BOOL_CASES_TAC `x:bool` THEN
 216    BOOL_CASES_TAC `y:bool` THEN
 217    BOOL_CASES_TAC `y':bool` THEN
 218    BOOL_CASES_TAC `t:bool` THEN
 219    REWRITE_TAC []);;
 220
 221 (*----------------------------------------------------------------------------*)
 222 (* IMP_EQ_OR_EQ_EQ_OR_NOT_OR =                                                *)
 223 (* |- (x ==> ((y \/ t) = (y' \/ t))) = ((y \/ (~x \/ t)) = (y' \/ (~x \/ t))) *)
 224 (*----------------------------------------------------------------------------*)
 225
 226 let IMP_EQ_OR_EQ_EQ_OR_NOT_OR =
 227  prove
 228   (`(x ==> ((y \/ t) = (y' \/ t))) = ((y \/ (~x \/ t)) = (y' \/ (~x \/ t)))`,
 229    BOOL_CASES_TAC `x:bool` THEN
 230    BOOL_CASES_TAC `y:bool` THEN
 231    BOOL_CASES_TAC `y':bool` THEN
 232    BOOL_CASES_TAC `t:bool` THEN
 233    REWRITE_TAC []);;
 234
 235 (*----------------------------------------------------------------------------*)
 236 (* IMP_EQ_EQ_EQ_NOT_OR = |- (x ==> (t = t')) = ((~x \/ t) = (~x \/ t'))       *)
 237 (*----------------------------------------------------------------------------*)
 238
 239 let IMP_EQ_EQ_EQ_NOT_OR =
 240  prove
 241   (`(x ==> (t = t')) = ((~x \/ t) = (~x \/ t'))`,
 242    BOOL_CASES_TAC `x:bool` THEN
 243    BOOL_CASES_TAC `t:bool` THEN
 244    BOOL_CASES_TAC `t':bool` THEN
 245    REWRITE_TAC []);;
 246
 247 (*----------------------------------------------------------------------------*)
 248 (* IMP_NOT_EQ_EQ_EQ_OR = |- (~x ==> (t = t')) = ((x \/ t) = (x \/ t'))        *)
 249 (*----------------------------------------------------------------------------*)
 250
 251 let IMP_NOT_EQ_EQ_EQ_OR =
 252  prove
 253   (`(~x ==> (t = t')) = ((x \/ t) = (x \/ t'))`,
 254    BOOL_CASES_TAC `x:bool` THEN
 255    BOOL_CASES_TAC `t:bool` THEN
 256    BOOL_CASES_TAC `t':bool` THEN
 257    REWRITE_TAC []);;
 258
 259 (*----------------------------------------------------------------------------*)
 260 (* T_OR = |- T \/ t = T                                                       *)
 261 (* OR_T = |- t \/ T = T                                                       *)
 262 (* F_OR = |- F \/ t = t                                                       *)
 263 (* OR_F = |- t \/ F = t                                                       *)
 264 (*----------------------------------------------------------------------------*)
 265
 266 let [T_OR;OR_T;F_OR;OR_F;_] = CONJUNCTS (SPEC_ALL OR_CLAUSES);;
 267
 268 (*----------------------------------------------------------------------------*)
 269 (* UNDER_DISJ_DISCH : term -> thm -> thm                                      *)
 270 (*                                                                            *)
 271 (*    A, ~x |- y \/ t = y' \/ t          A, x |- y \/ t = y' \/ t             *)
 272 (*    -------------------------------    ---------------------------------    *)
 273 (*    A |- y \/ x \/ t = y' \/ x \/ t    A |- y \/ ~x \/ t = y' \/ ~x \/ t    *)
 274 (*                                                                            *)
 275 (*    A, ~x |- y = y'                    A, x |- y = y'                       *)
 276 (*    ---------------------              -----------------------              *)
 277 (*    A |- y \/ x = y' \/ x              A |- y \/ ~x = y' \/ ~x              *)
 278 (*                                                                            *)
 279 (* The function assumes that y is a literal, so it is valid to test the LHS   *)
 280 (* of the theorem to see if it is a disjunction in order to determine which   *)
 281 (* rule to use.                                                               *)
 282 (*----------------------------------------------------------------------------*)
 283
 284 let UNDER_DISJ_DISCH tm th =
 285 try
 286  (let rewrite =
 287      if (is_disj (lhs (concl th)))
 288      then if (is_neg tm)
 289           then NOT_IMP_EQ_OR_EQ_EQ_OR_OR
 290           else IMP_EQ_OR_EQ_EQ_OR_NOT_OR
 291      else if (is_neg tm)
 292           then NOT_IMP_EQ_EQ_EQ_OR
 293           else IMP_EQ_EQ_EQ_OR_NOT
 294   in  CONV_RULE (REWR_CONV rewrite) (DISCH tm th)
 295  ) with Failure _ -> failwith "UNDER_DISJ_DISCH";;
 296
 297 (*----------------------------------------------------------------------------*)
 298 (* OVER_DISJ_DISCH : term -> thm -> thm                                       *)
 299 (*                                                                            *)
 300 (*    A, ~x |- t = t'                    A, x |- t = t'                       *)
 301 (*    ---------------------              -----------------------              *)
 302 (*    A |- x \/ t = x \/ t'              A |- ~x \/ t = ~x \/ t'              *)
 303 (*----------------------------------------------------------------------------*)
 304
 305 let OVER_DISJ_DISCH tm th =
 306  try (let rewrite =
 307      if (is_neg tm)
 308      then IMP_NOT_EQ_EQ_EQ_OR
 309      else IMP_EQ_EQ_EQ_NOT_OR
 310   in  CONV_RULE (REWR_CONV rewrite) (DISCH tm th)
 311  ) with Failure _ -> failwith "OVER_DISJ_DISCH";;
 312
 313 (*----------------------------------------------------------------------------*)
 314 (* MULTI_DISJ_DISCH : (term list # term list) -> thm -> thm                   *)
 315 (*                                                                            *)
 316 (* Examples:                                                                  *)
 317 (*                                                                            *)
 318 (*    MULTI_DISJ_DISCH (["x1"; "x2"],["~x3"; "x4"]) x1, ~x3, x4, x2 |- y = y' *)
 319 (*    --->                                                                    *)
 320 (*    |- ~x1 \/ ~x2 \/ y \/ x3 \/ ~x4 = ~x1 \/ ~x2 \/ y' \/ x3 \/ ~x4         *)
 321 (*                                                                            *)
 322 (*                                                                            *)
 323 (*    MULTI_DISJ_DISCH (["x1"; "x2"],["~x3"; "x4"]) x1, ~x3, x4, x2 |- y = F  *)
 324 (*    --->                                                                    *)
 325 (*    |- ~x1 \/ ~x2 \/ y \/ x3 \/ ~x4 = ~x1 \/ ~x2 \/ x3 \/ ~x4               *)
 326 (*                                                                            *)
 327 (*                                                                            *)
 328 (*    MULTI_DISJ_DISCH (["x1"; "x2"],["~x3"; "x4"]) x1, ~x3, x4, x2 |- y = T  *)
 329 (*    --->                                                                    *)
 330 (*    |- ~x1 \/ ~x2 \/ y \/ x3 \/ ~x4 = T                                     *)
 331 (*----------------------------------------------------------------------------*)
 332
 333 let MULTI_DISJ_DISCH (overs,unders) th =
 334 try
 335  (let th1 = itlist UNDER_DISJ_DISCH unders th
 336   in  let tm1 = rhs (concl th1)
 337   in  let th2 =
 338          if (try(is_T (fst (dest_disj tm1))) with Failure _ -> false) then
 339             (CONV_RULE (RAND_CONV (REWR_CONV T_OR)) th1)
 340          else if (try(is_F (fst (dest_disj tm1))) with Failure _ -> false) then
 341             (CONV_RULE (RAND_CONV (REWR_CONV F_OR)) th1)
 342          else th1
 343   in  let tm2 = rhs (concl th2)
 344   in  let rule =
 345          if (is_T tm2) then CONV_RULE (RAND_CONV (REWR_CONV OR_T)) else I
 346   in  itlist (fun tm th -> rule (OVER_DISJ_DISCH tm th)) overs th2
 347  ) with Failure _ -> failwith "MULTI_DISJ_DISCH";;