Boyer_Moore/clausal_form.ml

   1 (******************************************************************************)
   2 (* FILE          : clausal_form.ml                                            *)
   3 (* DESCRIPTION   : Functions for putting a formula into clausal form.         *)
   4 (*                                                                            *)
   5 (* READS FILES   : <none>                                                     *)
   6 (* WRITES FILES  : <none>                                                     *)
   7 (*                                                                            *)
   8 (* AUTHOR        : R.J.Boulton                                                *)
   9 (* DATE          : 13th May 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 IMP_DISJ_THM = TAUT `!t1 t2. t1 ==> t2 <=> ~t1 \/ t2`;;
  19 let RIGHT_OR_OVER_AND = TAUT `!t1 t2 t3. t2 /\ t3 \/ t1 <=> (t2 \/ t1) /\ (t3 \/ t1)`;;
  20 let LEFT_OR_OVER_AND = TAUT `!t1 t2 t3. t1 \/ t2 /\ t3 <=> (t1 \/ t2) /\ (t1 \/ t3)`;;
  21
  22 (*============================================================================*)
  23 (* Theorems for normalizing Boolean terms                                     *)
  24 (*============================================================================*)
  25
  26 (*----------------------------------------------------------------------------*)
  27 (* EQ_EXPAND = |- (x = y) = ((~x \/ y) /\ (~y \/ x))                          *)
  28 (*----------------------------------------------------------------------------*)
  29
  30 let EQ_EXPAND =
  31  prove
  32   (`(x = y) = ((~x \/ y) /\ (~y \/ x))`,
  33    BOOL_CASES_TAC `x:bool` THEN
  34    BOOL_CASES_TAC `y:bool` THEN
  35    REWRITE_TAC []);;
  36
  37 (*----------------------------------------------------------------------------*)
  38 (* IMP_EXPAND = |- (x ==> y) = (~x \/ y)                                      *)
  39 (*----------------------------------------------------------------------------*)
  40
  41 let IMP_EXPAND = SPEC `y:bool` (SPEC `x:bool` IMP_DISJ_THM);;
  42
  43 (*----------------------------------------------------------------------------*)
  44 (* COND_EXPAND = |- (x => y | z) = ((~x \/ y) /\ (x \/ z))                    *)
  45 (*----------------------------------------------------------------------------*)
  46
  47 let COND_EXPAND =
  48  prove
  49   (`(if x then y else z) = ((~x \/ y) /\ (x \/ z))`,
  50    BOOL_CASES_TAC `x:bool` THEN
  51    BOOL_CASES_TAC `y:bool` THEN
  52    BOOL_CASES_TAC `z:bool` THEN
  53    REWRITE_TAC []);;
  54
  55 (*----------------------------------------------------------------------------*)
  56 (* NOT_NOT_NORM = |- ~~x = x                                                  *)
  57 (*----------------------------------------------------------------------------*)
  58
  59 let NOT_NOT_NORM = SPEC `x:bool` (CONJUNCT1 NOT_CLAUSES);;
  60
  61 (*----------------------------------------------------------------------------*)
  62 (* NOT_CONJ_NORM = |- ~(x /\ y) = (~x \/ ~y)                                  *)
  63 (*----------------------------------------------------------------------------*)
  64
  65 let NOT_CONJ_NORM = CONJUNCT1 (SPEC `y:bool` (SPEC `x:bool` DE_MORGAN_THM));;
  66
  67 (*----------------------------------------------------------------------------*)
  68 (* NOT_DISJ_NORM = |- ~(x \/ y) = (~x /\ ~y)                                  *)
  69 (*----------------------------------------------------------------------------*)
  70
  71 let NOT_DISJ_NORM = CONJUNCT2 (SPEC `y:bool` (SPEC `x:bool` DE_MORGAN_THM));;
  72
  73 (*----------------------------------------------------------------------------*)
  74 (* LEFT_DIST_NORM = |- x \/ (y /\ z) = (x \/ y) /\ (x \/ z)                   *)
  75 (*----------------------------------------------------------------------------*)
  76
  77 let LEFT_DIST_NORM =
  78  SPEC `z:bool` (SPEC `y:bool` (SPEC `x:bool` LEFT_OR_OVER_AND));;
  79
  80 (*----------------------------------------------------------------------------*)
  81 (* RIGHT_DIST_NORM = |- (x /\ y) \/ z = (x \/ z) /\ (y \/ z)                  *)
  82 (*----------------------------------------------------------------------------*)
  83
  84 let RIGHT_DIST_NORM =
  85  SPEC `y:bool` (SPEC `x:bool` (SPEC `z:bool` RIGHT_OR_OVER_AND));;
  86
  87 (*----------------------------------------------------------------------------*)
  88 (* CONJ_ASSOC_NORM = |- (x /\ y) /\ z = x /\ (y /\ z)                         *)
  89 (*----------------------------------------------------------------------------*)
  90
  91 let CONJ_ASSOC_NORM =
  92  SYM (SPEC `z:bool` (SPEC `y:bool` (SPEC `x:bool` CONJ_ASSOC)));;
  93
  94 (*----------------------------------------------------------------------------*)
  95 (* DISJ_ASSOC_NORM = |- (x \/ y) \/ z = x \/ (y \/ z)                         *)
  96 (*----------------------------------------------------------------------------*)
  97
  98 let DISJ_ASSOC_NORM =
  99  SYM (SPEC `z:bool` (SPEC `y:bool` (SPEC `x:bool` DISJ_ASSOC)));;
 100
 101 (*============================================================================*)
 102 (* Conversions for rewriting Boolean terms                                    *)
 103 (*============================================================================*)
 104
 105 let COND_EXPAND_CONV = REWR_CONV COND_EXPAND;;
 106 let CONJ_ASSOC_NORM_CONV = REWR_CONV CONJ_ASSOC_NORM;;
 107 let DISJ_ASSOC_NORM_CONV = REWR_CONV DISJ_ASSOC_NORM;;
 108 let EQ_EXPAND_CONV = REWR_CONV EQ_EXPAND;;
 109 let IMP_EXPAND_CONV = REWR_CONV IMP_EXPAND;;
 110 let LEFT_DIST_NORM_CONV = REWR_CONV LEFT_DIST_NORM;;
 111 let NOT_CONJ_NORM_CONV = REWR_CONV NOT_CONJ_NORM;;
 112 let NOT_DISJ_NORM_CONV = REWR_CONV NOT_DISJ_NORM;;
 113 let NOT_NOT_NORM_CONV = REWR_CONV NOT_NOT_NORM;;
 114 let RIGHT_DIST_NORM_CONV = REWR_CONV RIGHT_DIST_NORM;;
 115
 116 (*----------------------------------------------------------------------------*)
 117 (* NOT_CONV : conv                                                            *)
 118 (*                                                                            *)
 119 (*    |- !t. ~~t = t                                                          *)
 120 (*    |- ~T = F                                                               *)
 121 (*    |- ~F = T                                                               *)
 122 (*----------------------------------------------------------------------------*)
 123
 124 let NOT_CONV =
 125 try (
 126  let [th1;th2;th3] = CONJUNCTS NOT_CLAUSES
 127  in fun tm ->
 128  (let arg = dest_neg tm
 129   in  if (is_T arg) then th2
 130       else if (is_F arg) then th3
 131       else SPEC (dest_neg arg) th1
 132  )
 133 ) with Failure _ -> failwith "NOT_CONV";;
 134
 135 (*----------------------------------------------------------------------------*)
 136 (* AND_CONV : conv                                                            *)
 137 (*                                                                            *)
 138 (*    |- T /\ t = t                                                           *)
 139 (*    |- t /\ T = t                                                           *)
 140 (*    |- F /\ t = F                                                           *)
 141 (*    |- t /\ F = F                                                           *)
 142 (*    |- t /\ t = t                                                           *)
 143 (*----------------------------------------------------------------------------*)
 144
 145 let AND_CONV =
 146 try (
 147  let [th1;th2;th3;th4;th5] = map GEN_ALL (CONJUNCTS (SPEC_ALL AND_CLAUSES))
 148  in fun tm ->
 149  (let (arg1,arg2) = dest_conj tm
 150   in  if (is_T arg1) then SPEC arg2 th1
 151       else if (is_T arg2) then SPEC arg1 th2
 152       else if (is_F arg1) then SPEC arg2 th3
 153       else if (is_F arg2) then SPEC arg1 th4
 154       else if (arg1 = arg2) then SPEC arg1 th5
 155       else failwith ""
 156   )
 157  ) with Failure _ -> failwith "AND_CONV" ;;
 158
 159 (*----------------------------------------------------------------------------*)
 160 (* OR_CONV : conv                                                             *)
 161 (*                                                                            *)
 162 (*    |- T \/ t = T                                                           *)
 163 (*    |- t \/ T = T                                                           *)
 164 (*    |- F \/ t = t                                                           *)
 165 (*    |- t \/ F = t                                                           *)
 166 (*    |- t \/ t = t                                                           *)
 167 (*----------------------------------------------------------------------------*)
 168
 169 let OR_CONV =
 170 try (
 171  let [th1;th2;th3;th4;th5] = map GEN_ALL (CONJUNCTS (SPEC_ALL OR_CLAUSES))
 172  in fun tm ->
 173  (let (arg1,arg2) = dest_disj tm
 174   in  if (is_T arg1) then SPEC arg2 th1
 175       else if (is_T arg2) then SPEC arg1 th2
 176       else if (is_F arg1) then SPEC arg2 th3
 177       else if (is_F arg2) then SPEC arg1 th4
 178       else if (arg1 = arg2) then SPEC arg1 th5
 179       else failwith ""
 180  )
 181 ) with Failure _ -> failwith "OR_CONV";;
 182
 183 (*============================================================================*)
 184 (* Conversions for obtaining `clausal' form                                   *)
 185 (*============================================================================*)
 186
 187 (*----------------------------------------------------------------------------*)
 188 (* EQ_IMP_COND_ELIM_CONV : (term -> bool) -> conv                             *)
 189 (*                                                                            *)
 190 (* Eliminates Boolean equalities, Boolean conditionals, and implications from *)
 191 (* terms consisting of =,==>,COND,/\,\/,~ and atoms. The atoms are specified  *)
 192 (* by the predicate that the conversion takes as its first argument.          *)
 193 (*----------------------------------------------------------------------------*)
 194
 195 let rec EQ_IMP_COND_ELIM_CONV is_atom tm =
 196 try
 197  (if (is_atom tm) then ALL_CONV tm
 198   else if (is_neg tm) then (RAND_CONV (EQ_IMP_COND_ELIM_CONV is_atom)) tm
 199   else if (is_eq tm) then
 200      ((RATOR_CONV (RAND_CONV (EQ_IMP_COND_ELIM_CONV is_atom))) THENC
 201       (RAND_CONV (EQ_IMP_COND_ELIM_CONV is_atom)) THENC
 202       EQ_EXPAND_CONV) tm
 203   else if (is_imp tm) then
 204      ((RATOR_CONV (RAND_CONV (EQ_IMP_COND_ELIM_CONV is_atom))) THENC
 205       (RAND_CONV (EQ_IMP_COND_ELIM_CONV is_atom)) THENC
 206       IMP_EXPAND_CONV) tm
 207   else if (is_cond tm) then
 208      ((RATOR_CONV
 209         (RATOR_CONV (RAND_CONV (EQ_IMP_COND_ELIM_CONV is_atom)))) THENC
 210       (RATOR_CONV (RAND_CONV (EQ_IMP_COND_ELIM_CONV is_atom))) THENC
 211       (RAND_CONV (EQ_IMP_COND_ELIM_CONV is_atom)) THENC
 212       COND_EXPAND_CONV) tm
 213   else ((RATOR_CONV (RAND_CONV (EQ_IMP_COND_ELIM_CONV is_atom))) THENC
 214         (RAND_CONV (EQ_IMP_COND_ELIM_CONV is_atom))) tm
 215  ) with Failure _ -> failwith "EQ_IMP_COND_ELIM_CONV";;
 216
 217 (*----------------------------------------------------------------------------*)
 218 (* MOVE_NOT_DOWN_CONV : (term -> bool) -> conv -> conv                        *)
 219 (*                                                                            *)
 220 (* Moves negations down through a term consisting of /\,\/,~ and atoms. The   *)
 221 (* atoms are specified by a predicate (first argument). When a negation has   *)
 222 (* reached an atom, the conversion `conv' (second argument) is applied to the *)
 223 (* negation of the atom. `conv' is also applied to any non-negated atoms      *)
 224 (* encountered. T and F are eliminated.                                       *)
 225 (*----------------------------------------------------------------------------*)
 226
 227 let rec MOVE_NOT_DOWN_CONV is_atom conv tm =
 228 try
 229  (if (is_atom tm) then (conv tm)
 230   else if (is_neg tm)
 231   then ((let tm' = rand tm
 232          in  if (is_atom tm') then ((conv THENC (TRY_CONV NOT_CONV)) tm)
 233              else if (is_neg tm') then (NOT_NOT_NORM_CONV THENC
 234                                    (MOVE_NOT_DOWN_CONV is_atom conv)) tm
 235              else if (is_conj tm') then
 236                 (NOT_CONJ_NORM_CONV THENC
 237                  (RATOR_CONV (RAND_CONV (MOVE_NOT_DOWN_CONV is_atom conv)))
 238                                                                           THENC
 239                  (RAND_CONV (MOVE_NOT_DOWN_CONV is_atom conv)) THENC
 240                  (TRY_CONV AND_CONV)) tm
 241              else if (is_disj tm') then
 242                 (NOT_DISJ_NORM_CONV THENC
 243                  (RATOR_CONV (RAND_CONV (MOVE_NOT_DOWN_CONV is_atom conv)))
 244                                                                           THENC
 245                  (RAND_CONV (MOVE_NOT_DOWN_CONV is_atom conv)) THENC
 246                  (TRY_CONV OR_CONV)) tm
 247              else failwith ""))
 248   else if (is_conj tm) then
 249      ((RATOR_CONV (RAND_CONV (MOVE_NOT_DOWN_CONV is_atom conv))) THENC
 250       (RAND_CONV (MOVE_NOT_DOWN_CONV is_atom conv)) THENC
 251       (TRY_CONV AND_CONV)) tm
 252   else if (is_disj tm) then
 253      ((RATOR_CONV (RAND_CONV (MOVE_NOT_DOWN_CONV is_atom conv))) THENC
 254       (RAND_CONV (MOVE_NOT_DOWN_CONV is_atom conv)) THENC
 255       (TRY_CONV OR_CONV)) tm
 256   else failwith ""
 257  ) with Failure _ -> failwith "MOVE_NOT_DOWN_CONV";;
 258
 259 (*----------------------------------------------------------------------------*)
 260 (* CONJ_LINEAR_CONV : conv                                                    *)
 261 (*                                                                            *)
 262 (* Linearizes conjuncts using the following conversion applied recursively:   *)
 263 (*                                                                            *)
 264 (*    "(x /\ y) /\ z"                                                         *)
 265 (*    ================================                                        *)
 266 (*    |- (x /\ y) /\ z = x /\ (y /\ z)                                        *)
 267 (*----------------------------------------------------------------------------*)
 268
 269 let rec CONJ_LINEAR_CONV tm =
 270 try
 271  (if ((is_conj tm) & (is_conj (rand (rator tm))))
 272   then (CONJ_ASSOC_NORM_CONV THENC
 273         (RAND_CONV (TRY_CONV CONJ_LINEAR_CONV)) THENC
 274         (TRY_CONV CONJ_LINEAR_CONV)) tm
 275   else failwith ""
 276  ) with Failure _ -> failwith "CONJ_LINEAR_CONV";;
 277
 278 (*----------------------------------------------------------------------------*)
 279 (* CONJ_NORM_FORM_CONV : conv                                                 *)
 280 (*                                                                            *)
 281 (* Puts a term involving /\ and \/ into conjunctive normal form. Anything     *)
 282 (* other than /\ and \/ is taken to be an atom and is not processed.          *)
 283 (*                                                                            *)
 284 (* The conjunction returned is linear, i.e. the conjunctions are associated   *)
 285 (* to the right. Each conjunct is a linear disjunction.                       *)
 286 (*----------------------------------------------------------------------------*)
 287
 288 let rec CONJ_NORM_FORM_CONV tm =
 289 try
 290  (if (is_disj tm) then
 291      (if (is_conj (rand (rator tm))) then
 292          ((RATOR_CONV
 293               (RAND_CONV ((RATOR_CONV (RAND_CONV CONJ_NORM_FORM_CONV)) THENC
 294                           (RAND_CONV CONJ_NORM_FORM_CONV)))) THENC
 295           (RAND_CONV CONJ_NORM_FORM_CONV) THENC
 296           RIGHT_DIST_NORM_CONV THENC
 297           (RATOR_CONV (RAND_CONV CONJ_NORM_FORM_CONV)) THENC
 298           (RAND_CONV CONJ_NORM_FORM_CONV) THENC
 299           (TRY_CONV CONJ_LINEAR_CONV)) tm
 300       else if (is_conj (rand tm)) then
 301          ((RATOR_CONV (RAND_CONV CONJ_NORM_FORM_CONV)) THENC
 302           (RAND_CONV ((RATOR_CONV (RAND_CONV CONJ_NORM_FORM_CONV)) THENC
 303                       (RAND_CONV CONJ_NORM_FORM_CONV))) THENC
 304           LEFT_DIST_NORM_CONV THENC
 305           (RATOR_CONV (RAND_CONV CONJ_NORM_FORM_CONV)) THENC
 306           (RAND_CONV CONJ_NORM_FORM_CONV) THENC
 307           (TRY_CONV CONJ_LINEAR_CONV)) tm
 308       else if (is_disj (rand (rator tm))) then
 309          (DISJ_ASSOC_NORM_CONV THENC CONJ_NORM_FORM_CONV) tm
 310       else (let th = RAND_CONV CONJ_NORM_FORM_CONV tm
 311             in  let tm' = rhs (concl th)
 312             in  if (is_conj (rand tm'))
 313                 then (TRANS th (CONJ_NORM_FORM_CONV tm'))
 314                 else th))
 315   else if (is_conj tm) then
 316      ((RATOR_CONV (RAND_CONV CONJ_NORM_FORM_CONV)) THENC
 317       (RAND_CONV CONJ_NORM_FORM_CONV) THENC
 318       (TRY_CONV CONJ_LINEAR_CONV)) tm
 319   else ALL_CONV tm
 320  ) with Failure _ -> failwith "CONJ_NORM_FORM_CONV";;
 321
 322 (*----------------------------------------------------------------------------*)
 323 (* has_boolean_args_and_result : term -> bool                                 *)
 324 (*                                                                            *)
 325 (* Yields true if and only if the term is of type ":bool", and if it is a     *)
 326 (* function application, all the arguments are of type ":bool".               *)
 327 (*----------------------------------------------------------------------------*)
 328
 329 let has_boolean_args_and_result tm =
 330 try
 331  (let args = snd (strip_comb tm)
 332   in  let types = (type_of tm)::(map type_of args)
 333   in  (subtract (setify types) [`:bool`]) = [] )
 334  with Failure _ -> (type_of tm = `:bool`);;
 335
 336 (*----------------------------------------------------------------------------*)
 337 (* CLAUSAL_FORM_CONV : conv                                                   *)
 338 (*                                                                            *)
 339 (* Puts into clausal form terms consisting of =,==>,COND,/\,\/,~ and atoms.   *)
 340 (*----------------------------------------------------------------------------*)
 341
 342 let CLAUSAL_FORM_CONV tm =
 343 try (
 344  let is_atom tm =
 345     (not (has_boolean_args_and_result tm)) or (is_var tm) or (is_const tm)
 346  in
 347  ((EQ_IMP_COND_ELIM_CONV is_atom) THENC
 348   (MOVE_NOT_DOWN_CONV is_atom ALL_CONV) THENC
 349   CONJ_NORM_FORM_CONV) tm
 350  ) with Failure _ -> failwith "CLAUSAL_FORM_CONV";;