Boyer_Moore/terms_and_clauses.ml

   1
   2 (******************************************************************************)
   3 (* FILE          : terms_and_clauses.ml                                       *)
   4 (* DESCRIPTION   : Rewriting terms and simplifying clauses.                   *)
   5 (*                                                                            *)
   6 (* READS FILES   : <none>                                                     *)
   7 (* WRITES FILES  : <none>                                                     *)
   8 (*                                                                            *)
   9 (* AUTHOR        : R.J.Boulton                                                *)
  10 (* DATE          : 7th June 1991                                              *)
  11 (*                                                                            *)
  12 (* MODIFIED      : R.J.Boulton                                                *)
  13 (* DATE          : 16th October 1992                                          *)
  14 (*                                                                            *)
  15 (* LAST MODIFIED : P. Papapanagiotou (University of Edinburgh)                *)
  16 (* DATE          : July 2009                                                  *)
  17 (******************************************************************************)
  18
  19 let SUBST_CONV thvars template tm =
  20   let thms,vars = unzip thvars in
  21   let gvs = map (genvar o type_of) vars in
  22   let gtemplate = subst (zip gvs vars) template in
  23   SUBST (zip thms gvs) (mk_eq(template,gtemplate)) (REFL tm);;
  24
  25
  26 let bool_EQ_CONV =
  27   let check = let boolty = `:bool` in check (fun tm -> type_of tm = boolty) in
  28   let clist = map (GEN `b:bool`)
  29                   (CONJUNCTS(SPEC `b:bool` EQ_CLAUSES)) in
  30   let tb = hd clist and bt = hd(tl clist) in
  31   let T = `T` and F = `F` in
  32   fun tm ->
  33     try let l,r = (I F_F check) (dest_eq tm) in
  34         if l = r then EQT_INTRO (REFL l) else
  35         if l = T then SPEC r tb else
  36         if r = T then SPEC l bt else fail()
  37     with Failure _ -> failwith "bool_EQ_CONV";;
  38
  39 (*----------------------------------------------------------------------------*)
  40 (* rewrite_with_lemmas : (term list -> term list -> conv) ->                  *)
  41 (*                        term list -> term list -> conv                      *)
  42 (*                                                                            *)
  43 (* Function to rewrite with known lemmas (rewrite rules) in the reverse order *)
  44 (* in which they were introduced. Applies the first applicable lemma, or if   *)
  45 (* none are applicable it leaves the term unchanged.                          *)
  46 (*                                                                            *)
  47 (* A rule is applicable if its LHS matches the term, and it does not violate  *)
  48 (* the `alphabetical' ordering rule if it is a permutative rule. To be        *)
  49 (* applicable, the hypotheses of the rules must be satisfied. The function    *)
  50 (* takes a general rewrite rule, a chain of hypotheses and a list of          *)
  51 (* assumptions as arguments. It uses these to try to satisfy the hypotheses.  *)
  52 (* If a hypotheses is in the assumption list, it is assumed. Otherwise a      *)
  53 (* check is made that the hypothesis is not already a goal of the proof       *)
  54 (* procedure. This is to prevent looping. If it's not already a goal, the     *)
  55 (* function attempts to rewrite the hypotheses, with it added to the chain of *)
  56 (* hypotheses.                                                                *)
  57 (*                                                                            *)
  58 (* Before trying to establish the hypotheses of a rewrite rule, it is         *)
  59 (* necessary to instantiate any free variables in the hypotheses. This is     *)
  60 (* done by trying to find an instantiation that makes one of the hypotheses   *)
  61 (* equal to a term in the assumption list.                                    *)
  62 (*----------------------------------------------------------------------------*)
  63
  64 let rewrite_with_lemmas rewrite hyp_chain assumps tm =
  65    let rewrite_hyp h =
  66 try (EQT_INTRO (ASSUME (find (fun tm -> tm = h) assumps))) with Failure _ ->
  67       (if (mem h hyp_chain)
  68        then ALL_CONV h
  69        else rewrite (h::hyp_chain) assumps h)
  70    in
  71    let rec try_rewrites assumps ths =
  72       if (ths = [])
  73       then failwith "try_rewrites"
  74       else (try (let th = inst_frees_in_hyps assumps (hd ths)
  75               in  let hyp_ths = map (EQT_ELIM o rewrite_hyp) (hyp th)
  76               in  itlist PROVE_HYP hyp_ths th)
  77            with Failure _ -> (try_rewrites assumps (tl ths))
  78            )
  79    in try (try_rewrites assumps (applicable_rewrites tm)) with Failure _ -> ALL_CONV tm;;
  80
  81 (*----------------------------------------------------------------------------*)
  82 (* rewrite_explicit_value : conv                                              *)
  83 (*                                                                            *)
  84 (* Explicit values are normally unchanged by rewriting, but in the case of a  *)
  85 (* numeric constant, it is expanded out into SUC form.                        *)
  86 (*----------------------------------------------------------------------------*)
  87
  88 let rec rewrite_explicit_value tm =
  89    let rec conv tm = (num_CONV THENC TRY_CONV (RAND_CONV conv)) tm
  90    in ((TRY_CONV conv) THENC
  91        (TRY_CONV (ARGS_CONV rewrite_explicit_value))) tm;;
  92
  93 (*----------------------------------------------------------------------------*)
  94 (* COND_T = |- (T => t1 | t2) = t1                                            *)
  95 (* COND_F = |- (F => t1 | t2) = t2                                            *)
  96 (*----------------------------------------------------------------------------*)
  97
  98 let [COND_T;COND_F] = CONJUNCTS (SPEC_ALL COND_CLAUSES);;
  99
 100 (*----------------------------------------------------------------------------*)
 101 (* COND_LEFT =                                                                *)
 102 (* |- !b x x' y. (b ==> (x = x')) ==> ((b => x | y) = (b => x' | y))          *)
 103 (*----------------------------------------------------------------------------*)
 104
 105 let COND_LEFT =
 106  prove
 107   (`!b x x' (y:'a). (b ==> (x = x')) ==> ((if b then x else y) = (if b then x' else y))`,
 108    REPEAT GEN_TAC THEN
 109    BOOL_CASES_TAC `b:bool` THEN
 110    REWRITE_TAC []);;
 111
 112 (*----------------------------------------------------------------------------*)
 113 (* COND_RIGHT =                                                               *)
 114 (* |- !b y y' x. (~b ==> (y = y')) ==> ((b => x | y) = (b => x | y'))         *)
 115 (*----------------------------------------------------------------------------*)
 116
 117 let COND_RIGHT =
 118  prove
 119   (`!b y y' (x:'a). (~b ==> (y = y')) ==> ((if b then x else y) = (if b then x else y'))`,
 120    REPEAT GEN_TAC THEN
 121    BOOL_CASES_TAC `b:bool` THEN
 122    REWRITE_TAC []);;
 123
 124 (*----------------------------------------------------------------------------*)
 125 (* COND_ID = |- !b t. (b => t | t) = t                                        *)
 126 (*----------------------------------------------------------------------------*)
 127
 128 (* Already defined in HOL *)
 129
 130 (*----------------------------------------------------------------------------*)
 131 (* COND_RIGHT_F = |- (b => b | F) = b                                         *)
 132 (*----------------------------------------------------------------------------*)
 133
 134 let COND_RIGHT_F =
 135  prove
 136   (`(if b then b else F) = b`,
 137    BOOL_CASES_TAC `b:bool` THEN
 138    REWRITE_TAC []);;
 139
 140 (*----------------------------------------------------------------------------*)
 141 (* COND_T_F = |- (b => T | F) = b                                             *)
 142 (*----------------------------------------------------------------------------*)
 143
 144 let COND_T_F =
 145  prove
 146   (`(if b then  T else F) = b`,
 147    BOOL_CASES_TAC `b:bool` THEN
 148    REWRITE_TAC []);;
 149
 150 (*----------------------------------------------------------------------------*)
 151 (* rewrite_conditional : (term list -> conv) -> term list -> conv             *)
 152 (*                                                                            *)
 153 (* Rewriting conditionals. Takes a general rewrite function and a list of     *)
 154 (* assumptions as arguments.                                                  *)
 155 (*                                                                            *)
 156 (* The function assumes that the term it is given is of the form "b => x | y" *)
 157 (* First it recursively rewrites b to b'. If b' is T or F, the conditional is *)
 158 (* reduced to x or y, respectively. The result is then rewritten recursively. *)
 159 (* If b' is not T or F, both x and y are rewritten, under suitable additional *)
 160 (* assumptions about b'. An attempt is then made to rewrite the new           *)
 161 (* conditional with one of the following:                                     *)
 162 (*                                                                            *)
 163 (*    (b => x | x) ---> x                                                     *)
 164 (*    (b => b | F) ---> b                                                     *)
 165 (*    (b => T | F) ---> b                                                     *)
 166 (*                                                                            *)
 167 (* The three rules are tried in the order shown above.                        *)
 168 (*----------------------------------------------------------------------------*)
 169
 170 let rewrite_conditional rewrite assumps tm =
 171 try (let th1 = RATOR_CONV (RATOR_CONV (RAND_CONV (rewrite assumps))) tm
 172   in  let tm1 = rhs (concl th1)
 173   in  let (b',(x,y)) = dest_cond tm1
 174   in  if (is_T b') then
 175           TRANS th1 (((REWR_CONV COND_T) THENC (rewrite assumps)) tm1)
 176        else if (is_F b') then
 177           TRANS th1 (((REWR_CONV COND_F) THENC (rewrite assumps)) tm1)
 178       else let th2 = DISCH b' (rewrite (b'::assumps) x)
 179         in let x' = rand (rand (concl th2))
 180         in let th3 = MP (ISPECL [b';x;x';y] COND_LEFT) th2
 181         in let tm3 = rhs (concl th3)
 182         in let notb' = mk_neg b'
 183         in let th4 = DISCH notb' (rewrite (notb'::assumps) y)
 184         in let y' = rand (rand (concl th4))
 185         in let th5 = MP (ISPECL [b';y;y';x'] COND_RIGHT) th4
 186         in let th6 = ((REWR_CONV COND_ID) ORELSEC
 187                       (REWR_CONV COND_RIGHT_F) ORELSEC
 188                       (TRY_CONV (REWR_CONV COND_T_F))) (rhs (concl th5))
 189             in  TRANS (TRANS (TRANS th1 th3) th5) th6
 190  ) with Failure _ -> failwith "rewrite_conditional";;
 191
 192 (*----------------------------------------------------------------------------*)
 193 (* EQ_T = |- (x = T) = x                                                      *)
 194 (*----------------------------------------------------------------------------*)
 195
 196 let EQ_T =
 197  prove
 198   (`(x = T) = x`,
 199    BOOL_CASES_TAC `x:bool` THEN
 200    REWRITE_TAC []);;
 201
 202 (*----------------------------------------------------------------------------*)
 203 (* EQ_EQ = |- (x = (y = z)) = ((y = z) => (x = T) | (x = F))                  *)
 204 (*----------------------------------------------------------------------------*)
 205
 206 let EQ_EQ =
 207  prove
 208   (`(x = ((y:'a) = z)) = (if (y = z) then (x = T) else (x = F))`,
 209    BOOL_CASES_TAC `x:bool` THEN
 210    BOOL_CASES_TAC `(y:'a) = z` THEN
 211    REWRITE_TAC []);;
 212
 213 (*----------------------------------------------------------------------------*)
 214 (* EQ_F = |- (x = F) = (x => F | T)                                           *)
 215 (*----------------------------------------------------------------------------*)
 216
 217 let EQ_F =
 218  prove
 219   (`(x = F) = (if x then F else T)`,
 220    BOOL_CASES_TAC `x:bool` THEN
 221    REWRITE_TAC []);;
 222
 223 (*----------------------------------------------------------------------------*)
 224 (* prove_terms_not_eq : term -> term -> thm                                   *)
 225 (*                                                                            *)
 226 (* Function to prove that the left-hand and right-hand sides of an equation   *)
 227 (* are not equal. Works with Boolean constants, explicit values, and terms    *)
 228 (* involving constructors and variables.                                      *)
 229 (*----------------------------------------------------------------------------*)
 230
 231 let prove_terms_not_eq l r =
 232    let rec STRUCT_CONV tm =
 233       (bool_EQ_CONV ORELSEC
 234        NUM_EQ_CONV ORELSEC
 235        (fun tm -> let (l,r) = dest_eq tm
 236              in  let ty_name = (fst o dest_type) (type_of l)
 237              in  let (ty_info:shell_info) = sys_shell_info ty_name
 238              in  let ty_conv = ty_info.struct_conv
 239              in  ty_conv STRUCT_CONV tm) ORELSEC
 240        (* REFL_CONV ORELSEC   Omitted because it cannot generate false *)
 241        ALL_CONV) tm
 242    in try(let th = STRUCT_CONV (mk_eq (l,r))
 243        in  if (is_F (rhs (concl th))) then th else failwith ""
 244       ) with Failure _ -> failwith "prove_terms_not_eq";;
 245
 246 (*----------------------------------------------------------------------------*)
 247 (* rewrite_equality : (term list -> term list -> conv) ->                     *)
 248 (*                     term list -> term list -> conv                         *)
 249 (*                                                                            *)
 250 (* Function for rewriting equalities. Takes a general rewrite function, a     *)
 251 (* chain of hypotheses and a list of assumptions as arguments.                *)
 252 (*                                                                            *)
 253 (* The left-hand and right-hand sides of the equality are rewritten           *)
 254 (* recursively. If the two sides are then identical, the term is rewritten to *)
 255 (* T. If it can be shown that the two sides are not equal, the term is        *)
 256 (* rewritten to F. Otherwise, the function rewrites with the first of the     *)
 257 (* following rules that is applicable (or it leaves the term unchanged if     *)
 258 (* none are applicable):                                                      *)
 259 (*                                                                            *)
 260 (*    (x = T)       ---> x                                                    *)
 261 (*    (x = (y = z)) ---> ((y = z) => (x = T) | (x = F))                       *)
 262 (*    (x = F)       ---> (x => F | T)                                         *)
 263 (*                                                                            *)
 264 (* The result is then rewritten using the known lemmas (rewrite rules).       *)
 265 (*----------------------------------------------------------------------------*)
 266
 267 let rewrite_equality rewrite hyp_chain assumps tm =
 268 try (let th1 = ((RATOR_CONV (RAND_CONV (rewrite hyp_chain assumps))) THENC
 269              (RAND_CONV (rewrite hyp_chain assumps))) tm
 270   in  let tm1 = rhs (concl th1)
 271   in  let (l,r) = dest_eq tm1
 272   in  if (l = r)
 273       then TRANS th1 (EQT_INTRO (ISPEC l EQ_REFL))
 274       else try(TRANS th1 (prove_terms_not_eq l r))
 275          with Failure _ -> (let th2 = ((REWR_CONV EQ_T) ORELSEC
 276                        (REWR_CONV EQ_EQ) ORELSEC
 277                        (TRY_CONV (REWR_CONV EQ_F))) tm1
 278             in  let th3 = rewrite_with_lemmas
 279                              rewrite hyp_chain assumps (rhs (concl th2))
 280             in  TRANS (TRANS th1 th2) th3)
 281  ) with Failure _ -> failwith "rewrite_equality";;
 282
 283 (*----------------------------------------------------------------------------*)
 284 (* rewrite_application :                                                      *)
 285 (*    (term -> string list -> term list -> term list -> conv) ->              *)
 286 (*     term -> string list -> term list -> term list -> conv                  *)
 287 (*                                                                            *)
 288 (* Function for rewriting applications. It takes a general rewriting function,*)
 289 (* a literal (the literal containing the function call), a list of names of   *)
 290 (* functions that are tentatively being opened up, a chain of hypotheses, and *)
 291 (* a list of assumptions as arguments.                                        *)
 292 (*                                                                            *)
 293 (* The function begins by rewriting the arguments. It then determines the     *)
 294 (* name of the function being applied. If this is a constructor, no further   *)
 295 (* rewriting is done. Otherwise, from the function name, the number of the    *)
 296 (* argument used for recursion (or zero if the definition is not recursive)   *)
 297 (* and expansion theorems for each possible constructor are obtained. If the  *)
 298 (* function is not recursive the call is opened up and the body is rewritten. *)
 299 (* If the function has no definition, the application is rewritten using the  *)
 300 (* known lemmas.                                                              *)
 301 (*                                                                            *)
 302 (* If the definition is recursive, but this function has already been         *)
 303 (* tentatively opened up, the version of the application with the arguments   *)
 304 (* rewritten is returned.                                                     *)
 305 (*                                                                            *)
 306 (* Otherwise, the application is rewritten with the known lemmas. If any of   *)
 307 (* the lemmas are applicable the result of the rewrite is returned. Otherwise *)
 308 (* the function determines the name of the constructor appearing in the       *)
 309 (* recursive argument, and looks up its details. If this process fails due to *)
 310 (* either the recursive argument not being an application of a constructor,   *)
 311 (* or because the constructor is not known, the function call cannot be       *)
 312 (* expanded, so the original call (with arguments rewritten) is returned.     *)
 313 (*                                                                            *)
 314 (* Provided a valid constructor is present in the recursive argument position *)
 315 (* the call is tentatively opened up. The body is rewritten with the name of  *)
 316 (* the function added to the `tentative openings' list. (Actually, the name   *)
 317 (* is not added to the list if the recursive argument of the call was an      *)
 318 (* explicit value). The result is compared with the unopened call to see if   *)
 319 (* it has good properties. If it does, the simplified body is returned.       *)
 320 (* Otherwise the unopened call is returned.                                   *)
 321 (*----------------------------------------------------------------------------*)
 322
 323 let rewrite_application rewrite lit funcs hyp_chain assumps tm =
 324 try (let th1 = ARGS_CONV (rewrite lit funcs hyp_chain assumps) tm
 325   in  let tm1 = rhs (concl th1)
 326   in  let (f,args) = strip_comb tm1
 327   in  let name = fst (dest_const f)
 328   in
 329   if (mem name (all_constructors ()))
 330   then th1
 331   else try
 332   (let (i,constructors) = get_def name
 333    in  if (i = 0) then
 334           (let th2 = REWR_CONV (snd (hd constructors)) tm1
 335            in  let th3 = rewrite lit funcs hyp_chain assumps (rhs (concl th2))
 336            in  TRANS (TRANS th1 th2) th3)
 337        else if (mem name funcs) then th1
 338        else let th2 =
 339                rewrite_with_lemmas (rewrite lit funcs) hyp_chain assumps tm1
 340             in  let tm2 = rhs (concl th2)
 341             in  if (tm2 = tm1)
 342                 then try (let argi = el (i-1) args
 343                      in  let constructor =
 344                             (try (fst (dest_const (fst (strip_comb argi)))) with Failure _ -> "")
 345                      in  (let th = assoc constructor constructors
 346                             in  let th3 = REWR_CONV th tm1
 347                             in  let tm3 = rhs (concl th3)
 348                             in  let funcs' =
 349                                    if (is_explicit_value argi)
 350                                    then funcs
 351                                    else name::funcs
 352                             in  let th4 =
 353                                    rewrite lit funcs' hyp_chain assumps tm3
 354                             in  let tm4 = rhs (concl th4)
 355                             in  if (good_properties assumps tm1 tm4 lit)
 356                                 then TRANS (TRANS th1 th3) th4
 357                                 else th1)
 358                          ) with Failure _ -> th1
 359                 else TRANS th1 th2)
 360   with Failure "get_def" ->
 361     (TRANS th1 (rewrite_with_lemmas (rewrite lit funcs) hyp_chain assumps tm1))
 362  ) with Failure _ -> failwith "rewrite_application";;
 363
 364 (*----------------------------------------------------------------------------*)
 365 (* rewrite_term : term -> string list -> term list -> term list -> conv       *)
 366 (*                                                                            *)
 367 (* Function for rewriting a term. Arguments are as follows:                   *)
 368 (*                                                                            *)
 369 (*    lit       : the literal containing the term to be rewritten.            *)
 370 (*    funcs     : names of functions that have been tentatively opened up.    *)
 371 (*    hyp_chain : hypotheses that we are trying to satisfy by parent calls.   *)
 372 (*    assumps   : a list of assumptions.                                      *)
 373 (*    tm        : the term to be rewritten.                                   *)
 374 (*----------------------------------------------------------------------------*)
 375
 376 let rec rewrite_term lit funcs hyp_chain assumps tm =
 377 try (EQT_INTRO (ASSUME (find (fun t -> t = tm) assumps))) with Failure _ ->
 378 try (EQF_INTRO (ASSUME (find (fun t -> t = mk_neg tm) assumps))) with Failure _ ->
 379 try (let rewrite = rewrite_term lit funcs
 380   in  if (is_var tm) then ALL_CONV tm
 381       else if (is_explicit_value tm) then rewrite_explicit_value tm
 382       else if (is_cond tm) then rewrite_conditional (rewrite hyp_chain) assumps tm
 383       else if (is_eq tm) then rewrite_equality rewrite hyp_chain assumps tm
 384       else rewrite_application rewrite_term lit funcs hyp_chain assumps tm
 385  ) with Failure _ -> failwith "rewrite_term";;
 386
 387 (*----------------------------------------------------------------------------*)
 388 (* COND_RAND = |- !f b x y. f (b => x | y) = (b => f x | f y)                 *)
 389 (*----------------------------------------------------------------------------*)
 390
 391 (* Already defined in HOL *)
 392
 393 (*----------------------------------------------------------------------------*)
 394 (* COND_RATOR = |- !b f g x. (b => f | g) x = (b => f x | g x)                *)
 395 (*----------------------------------------------------------------------------*)
 396
 397 (* Already defined in HOL *)
 398
 399 (*----------------------------------------------------------------------------*)
 400 (* MOVE_COND_UP_CONV : conv                                                   *)
 401 (*                                                                            *)
 402 (* Moves all conditionals in a term up to the top-level. Checks to see if the *)
 403 (* term contains any conditionals before it starts to do inference. This      *)
 404 (* improves the performance significantly. Alternatively, failure could be    *)
 405 (* used to avoid rebuilding unchanged sub-terms. This would be even more      *)
 406 (* efficient.                                                                 *)
 407 (*----------------------------------------------------------------------------*)
 408
 409 let rec MOVE_COND_UP_CONV tm =
 410 try(if (not (can (find_term is_cond) tm)) then ALL_CONV tm
 411   else if (is_cond tm) then
 412      ((RATOR_CONV (RATOR_CONV (RAND_CONV MOVE_COND_UP_CONV))) THENC
 413       (RATOR_CONV (RAND_CONV MOVE_COND_UP_CONV)) THENC
 414       (RAND_CONV MOVE_COND_UP_CONV)) tm
 415   else if (is_comb tm) then
 416      (let (op,arg) = dest_comb tm
 417       in  if (is_cond op) then
 418              ((REWR_CONV COND_RATOR) THENC MOVE_COND_UP_CONV) tm
 419           else if (is_cond arg) then
 420              ((REWR_CONV COND_RAND) THENC MOVE_COND_UP_CONV) tm
 421           else (let th = ((RATOR_CONV MOVE_COND_UP_CONV) THENC
 422                           (RAND_CONV MOVE_COND_UP_CONV)) tm
 423                 in  let tm' = rhs (concl th)
 424                 in  if (tm' = tm)
 425                     then th
 426                     else TRANS th (MOVE_COND_UP_CONV tm')))
 427   else ALL_CONV tm
 428  ) with Failure _ -> failwith "MOVE_COND_UP_CONV";;
 429
 430 (*----------------------------------------------------------------------------*)
 431 (* COND_OR = |- (b => x | y) \/ z = (~b \/ x \/ z) /\ (b \/ y \/ z)           *)
 432 (*----------------------------------------------------------------------------*)
 433
 434 let COND_OR =
 435  prove
 436   (`(if b then x else y) \/ z <=> ((~b \/ x \/ z) /\ (b \/ y \/ z))`,
 437    BOOL_CASES_TAC `b:bool` THEN
 438    REWRITE_TAC []);;
 439
 440 (*----------------------------------------------------------------------------*)
 441 (* COND_EXPAND = |- (x => y | z) = ((~x \/ y) /\ (x \/ z))                    *)
 442 (*----------------------------------------------------------------------------*)
 443
 444 (* Already proved *)
 445
 446 (*----------------------------------------------------------------------------*)
 447 (* NOT_NOT_NORM = |- ~~x = x                                                  *)
 448 (*----------------------------------------------------------------------------*)
 449
 450 (* Already proved *)
 451
 452 (*----------------------------------------------------------------------------*)
 453 (* LEFT_OR_OVER_AND = |- !t1 t2 t3. t1 \/ t2 /\ t3 = (t1 \/ t2) /\ (t1 \/ t3) *)
 454 (*----------------------------------------------------------------------------*)
 455
 456 (* Already available in HOL *)
 457
 458 (*----------------------------------------------------------------------------*)
 459 (* MOVE_NOT_THRU_CONDS_CONV : conv                                            *)
 460 (*                                                                            *)
 461 (* Function to push a negation down through (possibly) nested conditionals.   *)
 462 (* Eliminates any double-negations that may be introduced.                    *)
 463 (*----------------------------------------------------------------------------*)
 464
 465 let rec MOVE_NOT_THRU_CONDS_CONV tm =
 466  try (if (is_neg tm)
 467   then if (is_cond (rand tm))
 468        then ((REWR_CONV COND_RAND) THENC
 469              (RATOR_CONV (RAND_CONV MOVE_NOT_THRU_CONDS_CONV)) THENC
 470              (RAND_CONV MOVE_NOT_THRU_CONDS_CONV)) tm
 471        else TRY_CONV (REWR_CONV NOT_NOT_NORM) tm
 472   else ALL_CONV tm
 473  ) with Failure _ -> failwith "MOVE_NOT_THRU_CONDS_CONV";;
 474
 475 (*----------------------------------------------------------------------------*)
 476 (* EXPAND_ONE_COND_CONV : conv                                                *)
 477 (*                                                                            *)
 478 (* The function takes a term which it assumes to be either a conditional or   *)
 479 (* the disjunction of a conditional and some other term, and applies one of   *)
 480 (* the following rewrites as appropriate:                                     *)
 481 (*                                                                            *)
 482 (*    |- (b => x | y) = (~b \/ x) /\ (b \/ y)                                 *)
 483 (*                                                                            *)
 484 (*    |- (b => x | y) \/ z = (~b \/ x \/ z) /\ (b \/ y \/ z)                  *)
 485 (*                                                                            *)
 486 (* If b happens to be a conditional, the negation of ~b is moved down through *)
 487 (* the conditional (and any nested conditionals).                             *)
 488 (*----------------------------------------------------------------------------*)
 489
 490 let EXPAND_ONE_COND_CONV tm =
 491 try (((REWR_CONV COND_OR) ORELSEC (REWR_CONV COND_EXPAND)) THENC
 492   (RATOR_CONV (RAND_CONV (RATOR_CONV (RAND_CONV MOVE_NOT_THRU_CONDS_CONV)))))
 493  tm with Failure _ -> failwith "EXPAND_ONE_COND_CONV";;
 494
 495 (*----------------------------------------------------------------------------*)
 496 (* OR_OVER_ANDS_CONV : conv -> conv                                           *)
 497 (*                                                                            *)
 498 (* Distributes an OR over an arbitrary tree of conjunctions and applies a     *)
 499 (* conversion to each of the disjunctions that make up the new conjunction.   *)
 500 (*----------------------------------------------------------------------------*)
 501
 502 let rec OR_OVER_ANDS_CONV conv tm =
 503    if (is_disj tm)
 504    then if (is_conj (rand tm))
 505         then ((REWR_CONV LEFT_OR_OVER_AND) THENC
 506               (RATOR_CONV (RAND_CONV (OR_OVER_ANDS_CONV conv))) THENC
 507               (RAND_CONV (OR_OVER_ANDS_CONV conv))) tm
 508         else conv tm
 509    else ALL_CONV tm;;
 510
 511 (*----------------------------------------------------------------------------*)
 512 (* EXPAND_COND_CONV : conv                                                    *)
 513 (*                                                                            *)
 514 (* The function takes a term which it assumes to be either a conditional or   *)
 515 (* the disjunction of a conditional and some other term, and expands the      *)
 516 (* conditional into a disjunction using one of:                               *)
 517 (*                                                                            *)
 518 (*    |- (b => x | y) = (~b \/ x) /\ (b \/ y)                                 *)
 519 (*                                                                            *)
 520 (*    |- (b => x | y) \/ z = (~b \/ x \/ z) /\ (b \/ y \/ z)                  *)
 521 (*                                                                            *)
 522 (* The b, x and y may themselves be conditionals. If so, the function expands *)
 523 (* these as well, and so on, until there are no more conditionals. At each    *)
 524 (* stage disjunctions are distributed over conjunctions so that the final     *)
 525 (* result is a conjunction `tree' where each of the conjuncts is a            *)
 526 (* disjunction. The depth of a disjunction in the conjunction tree indicates  *)
 527 (* the number of literals that have been added to the disjunction compared to *)
 528 (* the original term.                                                         *)
 529 (*----------------------------------------------------------------------------*)
 530
 531 let rec EXPAND_COND_CONV tm =
 532  try (EXPAND_ONE_COND_CONV THENC
 533   (RATOR_CONV (RAND_CONV ((RAND_CONV EXPAND_COND_CONV) THENC
 534                           (OR_OVER_ANDS_CONV EXPAND_COND_CONV)))) THENC
 535   (RAND_CONV ((RAND_CONV EXPAND_COND_CONV) THENC
 536               (OR_OVER_ANDS_CONV EXPAND_COND_CONV)))) tm
 537  with Failure _ -> ALL_CONV tm;;
 538
 539 (*----------------------------------------------------------------------------*)
 540 (* SPLIT_CLAUSE_ON_COND_CONV : int -> conv                                    *)
 541 (*                                                                            *)
 542 (* The function takes a number n and a term which it assumes to be a          *)
 543 (* disjunction of literals in which the (n-1)th argument has had all          *)
 544 (* conditionals moved to the top level.                                       *)
 545 (*                                                                            *)
 546 (* The function dives down to the (n-1)th literal (disjunct) and expands the  *)
 547 (* conditionals into disjunctions, resulting in a conjunction `tree' in which *)
 548 (* each conjunct is a disjunction.                                            *)
 549 (*                                                                            *)
 550 (* As the function `backs out' from the (n-1)th literal it distributes the    *)
 551 (* ORs over the conjunction tree.                                             *)
 552 (*----------------------------------------------------------------------------*)
 553
 554 let SPLIT_CLAUSE_ON_COND_CONV n tm =
 555  try (funpow n (fun conv -> (RAND_CONV conv) THENC (OR_OVER_ANDS_CONV ALL_CONV))
 556      EXPAND_COND_CONV tm
 557  ) with Failure _ -> failwith "SPLIT_CLAUSE_ON_COND_CONV";;
 558
 559 (*----------------------------------------------------------------------------*)
 560 (* simplify_one_literal : int -> term -> (thm # int)                          *)
 561 (*                                                                            *)
 562 (* Attempts to simplify one literal of a clause assuming the negations of the *)
 563 (* other literals. The number n specifies which literal to rewrite. If n = 0, *)
 564 (* the first literal is rewritten. The function fails if n is out of range.   *)
 565 (*                                                                            *)
 566 (* If the literal to be simplified is negative, the function simplifies the   *)
 567 (* corresponding atom, and negates the result. If this new result is T or F,  *)
 568 (* the clause is rebuilt by discharging the assumptions. This process may     *)
 569 (* reduce the number of literals in the clause, so the theorem returned is    *)
 570 (* paired with -1 (except when processing the last literal of a clause in     *)
 571 (* which case returning 0 will, like -1, cause a failure when an attempt is   *)
 572 (* made to simplify the next literal, but is safer because it can't cause     *)
 573 (* looping if the literal has not been removed. This is the case when the     *)
 574 (* last literal has been rewritten to F. In this situation, the discharging   *)
 575 (* function does not eliminate the literal).                                  *)
 576 (*                                                                            *)
 577 (* If the simplified literal contains conditionals, these are brought up to   *)
 578 (* the top-level. The clause is then rebuilt by discharging. If no            *)
 579 (* conditionals were present the theorem is returned with 0, indicating that  *)
 580 (* the number of literals has not changed. Otherwise the clause is split into *)
 581 (* a conjunction of clauses, so that the conditionals are eliminated, and the *)
 582 (* result is returned with the number 1 to indicate that the number of        *)
 583 (* literals has increased.                                                    *)
 584 (*----------------------------------------------------------------------------*)
 585
 586 let simplify_one_literal n tm =
 587 try (let negate tm = if (is_neg tm) then (rand tm) else (mk_neg tm)
 588   and NEGATE th =
 589          let tm = rhs (concl th)
 590          and th' = AP_TERM `(~)` th
 591          in  if (is_T tm) then TRANS th' (el 1 (CONJUNCTS NOT_CLAUSES))
 592              else if (is_F tm) then TRANS th' (el 2 (CONJUNCTS NOT_CLAUSES))
 593              else th'
 594   in let (overs,y,unders) = match (chop_list n (disj_list tm)) with
 595                                        | (overs,y::unders) -> (overs,y,unders)
 596                                        | _ -> failwith ""
 597 (*      ) with Failure _ -> failwith "" *)
 598   in  let overs' = map negate overs
 599       and unders' = map negate unders
 600   in  let th1 =
 601          if (is_neg y)
 602          then NEGATE (rewrite_term y [] [] (overs' @ unders') (rand y))
 603          else rewrite_term y [] [] (overs' @ unders') y
 604   in  let tm1 = rhs (concl th1)
 605   in  if ((is_T tm1) or (is_F tm1))
 606       then (MULTI_DISJ_DISCH (overs',unders') th1,
 607             if (unders = []) then 0 else (-1))
 608       else let th2 = TRANS th1 (MOVE_COND_UP_CONV tm1)
 609            in  let tm2 = rhs (concl th2)
 610            in  let th3 = MULTI_DISJ_DISCH (overs',unders') th2
 611            in  if (is_cond tm2)
 612                then (CONV_RULE (RAND_CONV (SPLIT_CLAUSE_ON_COND_CONV n)) th3,1)
 613                else (th3,0)
 614  ) with Failure _ -> failwith "simplify_one_literal";;
 615
 616 (*----------------------------------------------------------------------------*)
 617 (* simplify_clause : int -> term -> (term list # proof)                       *)
 618 (* simplify_clauses : int -> term -> (term list # proof)                      *)
 619 (*                                                                            *)
 620 (* Functions for simplifying a clause by rewriting each literal in turn       *)
 621 (* assuming the negations of the others.                                      *)
 622 (*                                                                            *)
 623 (* The integer argument to simplify_clause should be zero initially. It will  *)
 624 (* then attempt to simplify the first literal. If the result is true, no new  *)
 625 (* clauses are produced. Otherwise, the function proceeds to simplify the     *)
 626 (* next literal. This has to be done differently according to the changes     *)
 627 (* that took place when simplifying the first literal.                        *)
 628 (*                                                                            *)
 629 (* If there was a reduction in the number of literals, this must have been    *)
 630 (* due to the literal being shown to be false, because the true case has      *)
 631 (* already been eliminated. So, there must be one less literal, and so n is   *)
 632 (* unchanged on the recursive call. If there was no change in the number of   *)
 633 (* literals, n is incremented by 1. Otherwise, not only have new literals     *)
 634 (* been introduced, but also the clause has been split into a conjunction of  *)
 635 (* clauses. simplify_clauses is called to handle this case.                   *)
 636 (*                                                                            *)
 637 (* When all the literals have been processed, n will become out of range and  *)
 638 (* cause a failure. This is trapped, and the simplified clause is returned.   *)
 639 (*                                                                            *)
 640 (* When the clause has been split into a conjunction of clauses, the depth of *)
 641 (* a clause in the tree of conjunctions indicates how many literals have been *)
 642 (* added to that clause. simplify_clauses recursively splits conjunctions,    *)
 643 (* incrementing n as it proceeds, until it reaches a clause. It then calls    *)
 644 (* simplify_clause to deal with the clause.                                   *)
 645 (*----------------------------------------------------------------------------*)
 646
 647 let rec simplify_clause n tm =
 648 try (let (th,change_flag) = simplify_one_literal n tm
 649   in  let tm' = rhs (concl th)
 650   in  if (is_T tm')
 651       then ([],apply_proof ( fun ths -> EQT_ELIM th) [])
 652       else let (tms,proof) =
 653               if (change_flag < 0) then simplify_clause n tm'
 654               else if (change_flag = 0) then simplify_clause (n + 1) tm'
 655               else simplify_clauses (n + 1) tm'
 656            in  (tms,(fun ths -> EQ_MP (SYM th) (proof ths))))
 657  with Failure _ -> ([tm],apply_proof hd [tm])
 658
 659 and simplify_clauses n tm =
 660 try (let (tm1,tm2) = dest_conj tm
 661   in  let (tms1,proof1) = simplify_clauses (n + 1) tm1
 662       and (tms2,proof2) = simplify_clauses (n + 1) tm2
 663   in  (tms1 @ tms2,
 664        fun ths -> let (ths1,ths2) = chop_list (length tms1) ths
 665              in  CONJ (proof1 ths1) (proof2 ths2)))
 666  with Failure _ -> (simplify_clause n tm);;
 667
 668
 669 let HL_simplify_clause tm =
 670 try (
 671   let rules = itlist union [rewrite_rules();flat (defs());all_accessor_thms()] [] in
 672   let th = SIMP_CONV rules tm
 673   in  let tm' = rhs (concl th)
 674   in  let tmc = try (rand o concl o COND_ELIM_CONV) tm' with Failure _ -> tm' in
 675       if (is_T tm')
 676       then ([],apply_proof ( fun ths -> EQT_ELIM th ) [])
 677       else ([tm'],apply_proof ((EQ_MP (SYM th)) o hd) [tm'])
 678  )
 679  with Failure _ -> ([tm],apply_proof hd [tm])
 680
 681 (*----------------------------------------------------------------------------*)
 682 (* simplify_heuristic : (term # bool) -> ((term # bool) list # proof)         *)
 683 (*                                                                            *)
 684 (* Wrapper for simplify_clause. This function has the correct type and        *)
 685 (* properties to be used as a `heuristic'. In particular, if the result of    *)
 686 (* simplify_clause is a single clause identical to the input clause,          *)
 687 (* a failure is generated.                                                    *)
 688 (*----------------------------------------------------------------------------*)
 689
 690 let simplify_heuristic (tm,(ind:bool)) =
 691 try (let (tms,proof) = simplify_clause 0 tm
 692   in  if (tms = [tm])
 693       then failwith ""
 694       else  (proof_print_string_l "-> Simplify Heuristic" () ;  (map (fun tm -> (tm,ind)) tms,proof))
 695  ) with Failure _ -> failwith "simplify_heuristic";;
 696
 697 let HL_simplify_heuristic (tm,(ind:bool)) =
 698 try (let (tms,proof) = HL_simplify_clause tm
 699   in  if (tms = [tm])
 700       then failwith ""
 701       else  (proof_print_string_l "-> HL Simplify Heuristic" () ;  (map (fun tm -> (tm,ind)) tms,proof))
 702  ) with Failure _ -> failwith "HL_simplify_heuristic";;
 703
 704 (*----------------------------------------------------------------------------*)
 705 (* NOT_EQ_F = |- !x. ~(x = x) = F                                             *)
 706 (*----------------------------------------------------------------------------*)
 707
 708 let NOT_EQ_F =
 709  GEN_ALL
 710   (TRANS (AP_TERM `(~)` (SPEC_ALL REFL_CLAUSE))
 711    (el 1 (CONJUNCTS NOT_CLAUSES)));;
 712
 713 (*----------------------------------------------------------------------------*)
 714 (* subst_heuristic : (term # bool) -> ((term # bool) list # proof)            *)
 715 (*                                                                            *)
 716 (* `Heuristic' for eliminating from a clause, a negated equality between a    *)
 717 (* variable and another term not containing the variable. For example, given  *)
 718 (* the clause:                                                                *)
 719 (*                                                                            *)
 720 (*    x1 \/ ~(x = t) \/ x3 \/ f x \/ x5                                       *)
 721 (*                                                                            *)
 722 (* the function returns the clause:                                           *)
 723 (*                                                                            *)
 724 (*    x1 \/ F \/ x3 \/ f t \/ x5                                              *)
 725 (*                                                                            *)
 726 (* So, all occurrences of x are replaced by t, and the equality x = t is      *)
 727 (* `thrown away'. The F could be eliminated, but the simplification heuristic *)
 728 (* will deal with it, so there is no point in duplicating the code.           *)
 729 (*                                                                            *)
 730 (* The function fails if there are no equalities that can be eliminated.      *)
 731 (*                                                                            *)
 732 (* The function proves the following three theorems:                          *)
 733 (*                                                                            *)
 734 (*    ~(x = t) |- x1 \/ ~(x = t) \/ x3 \/ f x \/ x5                           *)
 735 (*                                                                            *)
 736 (*       x = t |- x1 \/ ~(x = t) \/ x3 \/ f x \/ x5 =                         *)
 737 (*                x1 \/     F    \/ x3 \/ f t \/ x5                           *)
 738 (*                                                                            *)
 739 (*             |- (x = t) \/ ~(x = t)                                         *)
 740 (*                                                                            *)
 741 (* and returns the term "x1 \/ F \/ x3 \/ f t \/ x5" to be proved. When given *)
 742 (* this term as a theorem, it is possible to prove from the second theorem:   *)
 743 (*                                                                            *)
 744 (*       x = t |- x1 \/ ~(x = t) \/ x3 \/ f x \/ x5                           *)
 745 (*                                                                            *)
 746 (* which together with the first and third theorems yields a theorem for the  *)
 747 (* original clause.                                                           *)
 748 (*----------------------------------------------------------------------------*)
 749
 750 let subst_heuristic (tm,(ind:bool)) =
 751 try (let checkx (v,t) = (is_var v) & (not (mem v (frees t)))
 752   in  let rec split_disjuncts tml =
 753          if (can (check (checkx o dest_eq o dest_neg)) (hd tml))
 754          then ([],tml)
 755          else (fun (l1,l2) -> ((hd tml)::l1,l2)) (split_disjuncts (tl tml))
 756   in  let (overs,neq::unders) = split_disjuncts (disj_list tm)
 757   in  let eq = dest_neg neq
 758   in  let (v,t) = dest_eq eq
 759   in  let ass = ASSUME neq
 760   in  let th1 = itlist DISJ2 overs (try DISJ1 ass (list_mk_disj unders) with Failure _ -> ass)
 761       and th2 = SUBS [ISPEC t NOT_EQ_F] (SUBST_CONV [(ASSUME eq,v)] tm tm)
 762       and th3 = SPEC eq EXCLUDED_MIDDLE
 763   in  let tm' = rhs (concl th2)
 764   in  let proof th = DISJ_CASES th3 (EQ_MP (SYM th2) th) th1
 765   in   (proof_print_string_l "-> Subst Heuristic" () ;  ([(tm',ind)],apply_proof (proof o hd) [tm']))
 766  ) with Failure _ -> failwith "subst_heuristic";;