simp.ml

   1 (* ========================================================================= *)
   2 (* Simplification and rewriting.                                             *)
   3 (*                                                                           *)
   4 (*       John Harrison, University of Cambridge Computer Laboratory          *)
   5 (*                                                                           *)
   6 (*            (c) Copyright, University of Cambridge 1998                    *)
   7 (*              (c) Copyright, John Harrison 1998-2007                       *)
   8 (* ========================================================================= *)
   9
  10 needs "itab.ml";;
  11
  12 (* ------------------------------------------------------------------------- *)
  13 (* Generalized conversion (conversion plus a priority).                      *)
  14 (* ------------------------------------------------------------------------- *)
  15
  16 type gconv = int * conv;;
  17
  18 (* ------------------------------------------------------------------------- *)
  19 (* Primitive rewriting conversions: unconditional and conditional equations. *)
  20 (* ------------------------------------------------------------------------- *)
  21
  22 let REWR_CONV = PART_MATCH lhs;;
  23
  24 let IMP_REWR_CONV = PART_MATCH (lhs o snd o dest_imp);;
  25
  26 (* ------------------------------------------------------------------------- *)
  27 (* Versions with ordered rewriting. We must have l' > r' for the rewrite     *)
  28 (* |- l = r (or |- c ==> (l = r)) to apply.                                  *)
  29 (* ------------------------------------------------------------------------- *)
  30
  31 let ORDERED_REWR_CONV ord th =
  32   let basic_conv = REWR_CONV th in
  33   fun tm ->
  34     let thm = basic_conv tm in
  35     let l,r = dest_eq(concl thm) in
  36     if ord l r then thm
  37     else failwith "ORDERED_REWR_CONV: wrong orientation";;
  38
  39 let ORDERED_IMP_REWR_CONV ord th =
  40   let basic_conv = IMP_REWR_CONV th in
  41   fun tm ->
  42     let thm = basic_conv tm in
  43     let l,r = dest_eq(rand(concl thm)) in
  44     if ord l r then thm
  45     else failwith "ORDERED_IMP_REWR_CONV: wrong orientation";;
  46
  47 (* ------------------------------------------------------------------------- *)
  48 (* Standard AC-compatible term ordering: a "dynamic" lexicographic ordering. *)
  49 (*                                                                           *)
  50 (* This is a slight hack to make AC normalization work. However I *think*    *)
  51 (* it's properly AC compatible, i.e. monotonic and total, WF on ground terms *)
  52 (* (over necessarily finite signature) and with the properties for any       *)
  53 (* binary operator +:                                                        *)
  54 (*                                                                           *)
  55 (*         (x + y) + z > x + (y + z)                                         *)
  56 (*         x + y > y + x                   iff x > y                         *)
  57 (*         x + (y + z) > y + (x + z)       iff x > y                         *)
  58 (*                                                                           *)
  59 (* The idea is that when invoking lex ordering with identical head operator  *)
  60 (* "f", one sticks "f" at the head of an otherwise arbitrary ordering on     *)
  61 (* subterms (the built-in CAML one). This avoids the potentially inefficient *)
  62 (* calculation of term size in the standard orderings.                       *)
  63 (* ------------------------------------------------------------------------- *)
  64
  65 let term_order =
  66   let rec lexify ord l1 l2 =
  67     if l1 = [] then false
  68     else if l2 = [] then true else
  69     let h1 = hd l1 and h2 = hd l2 in
  70     ord h1 h2 or (h1 = h2 & lexify ord (tl l1) (tl l2)) in
  71   let rec dyn_order top tm1 tm2 =
  72     let f1,args1 = strip_comb tm1
  73     and f2,args2 = strip_comb tm2 in
  74     if f1 = f2 then
  75       lexify (dyn_order f1) args1 args2
  76     else
  77       if f2 = top then false
  78       else if f1 = top then true
  79       else f1 > f2 in
  80   dyn_order `T`;;
  81
  82 (* ------------------------------------------------------------------------- *)
  83 (* Create a gconv net for a theorem as a (cond) rewrite. The "rep" flag      *)
  84 (* will cause any trivially looping rewrites to be modified, and any that    *)
  85 (* are permutative to be ordered w.r.t. the standard order. The idea is that *)
  86 (* this flag will be set iff the conversion is going to get repeated.        *)
  87 (* This includes a completely ad hoc but useful special case for ETA_AX,     *)
  88 (* which forces a first order match (otherwise it would loop on a lambda).   *)
  89 (* ------------------------------------------------------------------------- *)
  90
  91 let net_of_thm rep th =
  92   let tm = concl th in
  93   let lconsts = freesl (hyp th) in
  94   let matchable = can o term_match lconsts in
  95   match tm with
  96     Comb(Comb(Const("=",_),(Abs(x,Comb(Var(s,ty) as v,x')) as l)),v')
  97          when x' = x & v' = v & not(x = v) ->
  98         let conv tm =
  99           match tm with
 100             Abs(y,Comb(t,y')) when y = y' & not(free_in y t) ->
 101               INSTANTIATE(term_match [] v t) th
 102           | _ -> failwith "REWR_CONV (ETA_AX special case)" in
 103         enter lconsts (l,(1,conv))
 104   | Comb(Comb(Const("=",_),l),r) ->
 105       if rep & free_in l r then
 106         let th' = EQT_INTRO th in
 107         enter lconsts (l,(1,REWR_CONV th'))
 108       else if rep & matchable l r & matchable r l then
 109         enter lconsts (l,(1,ORDERED_REWR_CONV term_order th))
 110       else enter lconsts (l,(1,REWR_CONV th))
 111   | Comb(Comb(_,t),Comb(Comb(Const("=",_),l),r)) ->
 112         if rep & free_in l r then
 113           let th' = DISCH t (EQT_INTRO(UNDISCH th)) in
 114           enter lconsts (l,(3,IMP_REWR_CONV th'))
 115         else if rep & matchable l r & matchable r l then
 116           enter lconsts (l,(3,ORDERED_IMP_REWR_CONV term_order th))
 117         else enter lconsts(l,(3,IMP_REWR_CONV th));;
 118
 119 (* ------------------------------------------------------------------------- *)
 120 (* Create a gconv net for a conversion with a term index.                    *)
 121 (* ------------------------------------------------------------------------- *)
 122
 123 let net_of_conv tm conv sofar =
 124   enter [] (tm,(2,conv)) sofar;;
 125
 126 (* ------------------------------------------------------------------------- *)
 127 (* Create a gconv net for a congruence rule (in canonical form!)             *)
 128 (* ------------------------------------------------------------------------- *)
 129
 130 let net_of_cong th sofar =
 131   let conc,n = repeat (fun (tm,m) -> snd(dest_imp tm),m+1) (concl th,0) in
 132   if n = 0 then failwith "net_of_cong: Non-implicational congruence" else
 133   let pat = lhs conc in
 134   let conv = GEN_PART_MATCH (lhand o funpow n rand) th in
 135   enter [] (pat,(4,conv)) sofar;;
 136
 137 (* ------------------------------------------------------------------------- *)
 138 (* Rewrite maker for ordinary and conditional rewrites (via "cf" flag).      *)
 139 (*                                                                           *)
 140 (* We follow Don in going from ~(s = t) to (s = t) = F *and* (t = s) = F.    *)
 141 (* Well, why not? However, we don't abandon s = t where FV(t) is not a       *)
 142 (* subset of FV(s) in favour of (s = t) = T, as he does.                     *)
 143 (* Note: looping rewrites are not discarded here, only when netted.          *)
 144 (* ------------------------------------------------------------------------- *)
 145
 146 let mk_rewrites =
 147   let IMP_CONJ_CONV = REWR_CONV(ITAUT `p ==> q ==> r <=> p /\ q ==> r`)
 148   and IMP_EXISTS_RULE =
 149     let cnv = REWR_CONV(ITAUT `(!x. P x ==> Q) <=> (?x. P x) ==> Q`) in
 150     fun v th -> CONV_RULE cnv (GEN v th) in
 151   let collect_condition oldhyps th =
 152     let conds = subtract (hyp th) oldhyps in
 153     if conds = [] then th else
 154     let jth = itlist DISCH conds th in
 155     let kth = CONV_RULE (REPEATC IMP_CONJ_CONV) jth in
 156     let cond,eqn = dest_imp(concl kth) in
 157     let fvs = subtract (subtract (frees cond) (frees eqn)) (freesl oldhyps) in
 158     itlist IMP_EXISTS_RULE fvs kth in
 159   let rec split_rewrites oldhyps cf th sofar =
 160     let tm = concl th in
 161     if is_forall tm then
 162       split_rewrites oldhyps cf (SPEC_ALL th) sofar
 163     else if is_conj tm then
 164       split_rewrites oldhyps cf (CONJUNCT1 th)
 165         (split_rewrites oldhyps cf (CONJUNCT2 th) sofar)
 166     else if is_imp tm & cf then
 167       split_rewrites oldhyps cf (UNDISCH th) sofar
 168     else if is_eq tm then
 169       (if cf then collect_condition oldhyps th else th)::sofar
 170     else if is_neg tm then
 171       let ths = split_rewrites oldhyps cf (EQF_INTRO th) sofar in
 172       if is_eq (rand tm)
 173       then split_rewrites oldhyps cf (EQF_INTRO (GSYM th)) ths
 174       else ths
 175     else
 176       split_rewrites oldhyps cf (EQT_INTRO th) sofar in
 177   fun cf th sofar -> split_rewrites (hyp th) cf th sofar;;
 178
 179 (* ------------------------------------------------------------------------- *)
 180 (* Rewriting (and application of other conversions) based on a convnet.      *)
 181 (* ------------------------------------------------------------------------- *)
 182
 183 let REWRITES_CONV net tm =
 184   let pconvs = lookup tm net in
 185   try tryfind (fun (_,cnv) -> cnv tm) pconvs
 186   with Failure _ -> failwith "REWRITES_CONV";;
 187
 188 (* ------------------------------------------------------------------------- *)
 189 (* Decision procedures may accumulate their state in different ways (e.g.    *)
 190 (* term nets and predicate-indexed lists of Horn clauses). To allow mixing   *)
 191 (* of arbitrary types for state storage, we use a trick due to RJB via DRS.  *)
 192 (* ------------------------------------------------------------------------- *)
 193
 194 type prover = Prover of conv * (thm list -> prover);;
 195
 196 let mk_prover applicator augmentor =
 197   let rec mk_prover state =
 198     let apply = applicator state
 199     and augment thms = mk_prover (augmentor state thms) in
 200     Prover(apply,augment) in
 201   mk_prover;;
 202
 203 let augment(Prover(_,aug)) thms = aug thms;;
 204
 205 let apply_prover(Prover(conv,_)) tm = conv tm;;
 206
 207 (* ------------------------------------------------------------------------- *)
 208 (* Type of simpsets. We have a convnet containing rewrites (implicational    *)
 209 (* and otherwise), other term-indexed context-free conversions like          *)
 210 (* BETA_CONV, and congruence rules. Then there is a list of provers that     *)
 211 (* have their own way of storing and using context, and finally a rewrite    *)
 212 (* maker function, to allow customization.                                   *)
 213 (*                                                                           *)
 214 (* We also have a type of (traversal) strategy, following Konrad.            *)
 215 (* ------------------------------------------------------------------------- *)
 216
 217 type simpset =
 218   Simpset of gconv net                          (* Rewrites & congruences *)
 219            * (strategy -> strategy)             (* Prover for conditions  *)
 220            * prover list                        (* Subprovers for prover  *)
 221            * (thm -> thm list -> thm list)      (* Rewrite maker          *)
 222
 223 and strategy = simpset -> int -> term -> thm;;
 224
 225 (* ------------------------------------------------------------------------- *)
 226 (* Very simple prover: recursively simplify then try provers.                *)
 227 (* ------------------------------------------------------------------------- *)
 228
 229 let basic_prover strat (Simpset(net,prover,provers,rewmaker) as ss) lev tm =
 230   let sth = try strat ss lev tm with Failure _ -> REFL tm in
 231   try EQT_ELIM sth
 232   with Failure _ ->
 233     let tth = tryfind (fun pr -> apply_prover pr (rand(concl sth))) provers in
 234     EQ_MP (SYM sth) tth;;
 235
 236 (* ------------------------------------------------------------------------- *)
 237 (* Functions for changing or augmenting components of simpsets.              *)
 238 (* ------------------------------------------------------------------------- *)
 239
 240 let ss_of_thms thms (Simpset(net,prover,provers,rewmaker)) =
 241   let cthms = itlist rewmaker thms [] in
 242   let net' = itlist (net_of_thm true) cthms net in
 243   Simpset(net',prover,provers,rewmaker);;
 244
 245 let ss_of_conv keytm conv (Simpset(net,prover,provers,rewmaker)) =
 246   let net' = net_of_conv keytm conv net in
 247   Simpset(net',prover,provers,rewmaker);;
 248
 249 let ss_of_congs thms (Simpset(net,prover,provers,rewmaker)) =
 250   let net' = itlist net_of_cong thms net in
 251   Simpset(net',prover,provers,rewmaker);;
 252
 253 let ss_of_prover newprover (Simpset(net,_,provers,rewmaker)) =
 254   Simpset(net,newprover,provers,rewmaker);;
 255
 256 let ss_of_provers newprovers (Simpset(net,prover,provers,rewmaker)) =
 257   Simpset(net,prover,newprovers@provers,rewmaker);;
 258
 259 let ss_of_maker newmaker (Simpset(net,prover,provers,_)) =
 260   Simpset(net,prover,provers,newmaker);;
 261
 262 (* ------------------------------------------------------------------------- *)
 263 (* Perform a context-augmentation operation on a simpset.                    *)
 264 (* ------------------------------------------------------------------------- *)
 265
 266 let AUGMENT_SIMPSET cth (Simpset(net,prover,provers,rewmaker)) =
 267   let provers' = map (C augment [cth]) provers in
 268   let cthms = rewmaker cth [] in
 269   let net' = itlist (net_of_thm true) cthms net in
 270   Simpset(net',prover,provers',rewmaker);;
 271
 272 (* ------------------------------------------------------------------------- *)
 273 (* Depth conversions.                                                        *)
 274 (* ------------------------------------------------------------------------- *)
 275
 276 let ONCE_DEPTH_SQCONV,DEPTH_SQCONV,REDEPTH_SQCONV,
 277     TOP_DEPTH_SQCONV,TOP_SWEEP_SQCONV =
 278   let IMP_REWRITES_CONV strat (Simpset(net,prover,provers,rewmaker) as ss) lev
 279                         pconvs tm =
 280     tryfind (fun (n,cnv) ->
 281       if n >= 4 then fail() else
 282       let th = cnv tm in
 283       let etm = concl th in
 284       if is_eq etm then th else
 285       if lev <= 0 then failwith "IMP_REWRITES_CONV: Too deep" else
 286       let cth = prover strat ss (lev-1) (lhand etm) in
 287       MP th cth) pconvs in
 288   let rec RUN_SUB_CONV strat ss lev triv th =
 289     let tm = concl th in
 290     if is_imp tm then
 291       let subtm = lhand tm in
 292       let avs,bod = strip_forall subtm in
 293       let (t,t'),ss',mk_fun =
 294         try dest_eq bod,ss,I with Failure _ ->
 295         let cxt,deq = dest_imp bod in
 296         dest_eq deq,AUGMENT_SIMPSET (ASSUME cxt) ss,DISCH cxt in
 297       let eth,triv' = try strat ss' lev t,false with Failure _ -> REFL t,triv in
 298       let eth' = GENL avs (mk_fun eth) in
 299       let th' = if is_var t' then INST [rand(concl eth),t'] th
 300                 else GEN_PART_MATCH lhand th (concl eth') in
 301       let th'' = MP th' eth' in
 302       RUN_SUB_CONV strat ss lev triv' th''
 303     else if triv then fail() else th in
 304   let GEN_SUB_CONV strat ss lev pconvs tm =
 305     try tryfind (fun (n,cnv) ->
 306           if n < 4 then fail() else
 307           let th = cnv tm in
 308           RUN_SUB_CONV strat ss lev true th) pconvs
 309     with Failure _ ->
 310         if is_comb tm then
 311           let l,r = dest_comb tm in
 312           try let th1 = strat ss lev l in
 313               try let th2 = strat ss lev r in MK_COMB(th1,th2)
 314               with Failure _ -> AP_THM th1 r
 315           with Failure _ -> AP_TERM l (strat ss lev r)
 316         else if is_abs tm then
 317           let v,bod = dest_abs tm in
 318           let th = strat ss lev bod in
 319           try ABS v th with Failure _ ->
 320           let gv = genvar(type_of v) in
 321           let gbod = vsubst[gv,v] bod in
 322           let gth = ABS gv (strat ss lev gbod) in
 323           let gtm = concl gth in
 324           let l,r = dest_eq gtm in
 325           let v' = variant (frees gtm) v in
 326           let l' = alpha v' l and r' = alpha v' r in
 327           EQ_MP (ALPHA gtm (mk_eq(l',r'))) gth
 328         else failwith "GEN_SUB_CONV" in
 329   let rec ONCE_DEPTH_SQCONV
 330        (Simpset(net,prover,provers,rewmaker) as ss) lev tm =
 331     let pconvs = lookup tm net in
 332     try IMP_REWRITES_CONV ONCE_DEPTH_SQCONV ss lev pconvs tm
 333     with Failure _ ->
 334         GEN_SUB_CONV ONCE_DEPTH_SQCONV ss lev pconvs tm in
 335   let rec DEPTH_SQCONV (Simpset(net,prover,provers,rewmaker) as ss) lev tm =
 336     let pconvs = lookup tm net in
 337     try let th1 = GEN_SUB_CONV DEPTH_SQCONV ss lev pconvs tm in
 338         let tm1 = rand(concl th1) in
 339         let pconvs1 = lookup tm1 net in
 340         try TRANS th1 (IMP_REWRITES_CONV DEPTH_SQCONV ss lev pconvs1 tm1)
 341         with Failure _ -> th1
 342     with Failure _ ->
 343         IMP_REWRITES_CONV DEPTH_SQCONV ss lev pconvs tm in
 344   let rec REDEPTH_SQCONV (Simpset(net,prover,provers,rewmaker) as ss) lev tm =
 345     let pconvs = lookup tm net in
 346     let th =
 347       try let th1 = GEN_SUB_CONV REDEPTH_SQCONV ss lev pconvs tm in
 348           let tm1 = rand(concl th1) in
 349           let pconvs1 = lookup tm1 net in
 350           try TRANS th1 (IMP_REWRITES_CONV REDEPTH_SQCONV ss lev pconvs1 tm1)
 351           with Failure _ -> th1
 352       with Failure _ ->
 353           IMP_REWRITES_CONV REDEPTH_SQCONV ss lev pconvs tm in
 354     try let th' = REDEPTH_SQCONV ss lev (rand(concl th)) in
 355         TRANS th th'
 356     with Failure _ -> th in
 357   let rec TOP_DEPTH_SQCONV (Simpset(net,prover,provers,rewmaker) as ss) lev tm =
 358     let pconvs = lookup tm net in
 359     let th1 =
 360       try IMP_REWRITES_CONV TOP_DEPTH_SQCONV ss lev pconvs tm
 361       with Failure _ -> GEN_SUB_CONV TOP_DEPTH_SQCONV ss lev pconvs tm in
 362     try let th2 = TOP_DEPTH_SQCONV ss lev (rand(concl th1)) in
 363             TRANS th1 th2
 364     with Failure _ -> th1 in
 365   let rec TOP_SWEEP_SQCONV (Simpset(net,prover,provers,rewmaker) as ss) lev tm =
 366     let pconvs = lookup tm net in
 367     try let th1 = IMP_REWRITES_CONV TOP_SWEEP_SQCONV ss lev pconvs tm in
 368         try let th2 = TOP_SWEEP_SQCONV ss lev (rand(concl th1)) in
 369             TRANS th1 th2
 370         with Failure _ -> th1
 371     with Failure _ -> GEN_SUB_CONV TOP_SWEEP_SQCONV ss lev pconvs tm in
 372   ONCE_DEPTH_SQCONV,DEPTH_SQCONV,REDEPTH_SQCONV,
 373   TOP_DEPTH_SQCONV,TOP_SWEEP_SQCONV;;
 374
 375 (* ------------------------------------------------------------------------- *)
 376 (* Maintenence of basic rewrites and conv nets for rewriting.                *)
 377 (* ------------------------------------------------------------------------- *)
 378
 379 let set_basic_rewrites,extend_basic_rewrites,basic_rewrites,
 380     set_basic_convs,extend_basic_convs,basic_convs,basic_net =
 381   let rewrites = ref ([]:thm list)
 382   and conversions = ref ([]:(string*(term*conv))list)
 383   and conv_net = ref (empty_net: gconv net) in
 384   let rehash_convnet() =
 385     conv_net := itlist (net_of_thm true) (!rewrites)
 386         (itlist (fun (_,(pat,cnv)) -> net_of_conv pat cnv) (!conversions)
 387                 empty_net) in
 388   let set_basic_rewrites thl =
 389     let canon_thl = itlist (mk_rewrites false) thl [] in
 390     (rewrites := canon_thl; rehash_convnet())
 391   and extend_basic_rewrites thl =
 392     let canon_thl = itlist (mk_rewrites false) thl [] in
 393     (rewrites := canon_thl @ !rewrites; rehash_convnet())
 394   and basic_rewrites() = !rewrites
 395   and set_basic_convs cnvs =
 396     (conversions := cnvs; rehash_convnet())
 397   and extend_basic_convs (name,patcong) =
 398     (conversions :=
 399       (name,patcong)::filter(fun (name',_) -> name <> name') (!conversions);
 400      rehash_convnet())
 401   and basic_convs() = !conversions
 402   and basic_net() = !conv_net in
 403   set_basic_rewrites,extend_basic_rewrites,basic_rewrites,
 404   set_basic_convs,extend_basic_convs,basic_convs,basic_net;;
 405
 406 (* ------------------------------------------------------------------------- *)
 407 (* Same thing for the default congruences.                                   *)
 408 (* ------------------------------------------------------------------------- *)
 409
 410 let set_basic_congs,extend_basic_congs,basic_congs =
 411   let congs = ref ([]:thm list) in
 412   (fun thl -> congs := thl),
 413   (fun thl -> congs := union' equals_thm thl (!congs)),
 414   (fun () -> !congs);;
 415
 416 (* ------------------------------------------------------------------------- *)
 417 (* Main rewriting conversions.                                               *)
 418 (* ------------------------------------------------------------------------- *)
 419
 420 let GENERAL_REWRITE_CONV rep (cnvl:conv->conv) (builtin_net:gconv net) thl =
 421   let thl_canon = itlist (mk_rewrites false) thl [] in
 422   let final_net = itlist (net_of_thm rep) thl_canon builtin_net in
 423   cnvl (REWRITES_CONV final_net);;
 424
 425 let GEN_REWRITE_CONV (cnvl:conv->conv) thl =
 426   GENERAL_REWRITE_CONV false cnvl empty_net thl;;
 427
 428 let PURE_REWRITE_CONV thl =
 429   GENERAL_REWRITE_CONV true TOP_DEPTH_CONV empty_net thl;;
 430
 431 let REWRITE_CONV thl =
 432   GENERAL_REWRITE_CONV true TOP_DEPTH_CONV (basic_net()) thl;;
 433
 434 let PURE_ONCE_REWRITE_CONV thl =
 435   GENERAL_REWRITE_CONV false ONCE_DEPTH_CONV empty_net thl;;
 436
 437 let ONCE_REWRITE_CONV thl =
 438   GENERAL_REWRITE_CONV false ONCE_DEPTH_CONV (basic_net()) thl;;
 439
 440 (* ------------------------------------------------------------------------- *)
 441 (* Rewriting rules and tactics.                                              *)
 442 (* ------------------------------------------------------------------------- *)
 443
 444 let GEN_REWRITE_RULE cnvl thl = CONV_RULE(GEN_REWRITE_CONV cnvl thl);;
 445
 446 let PURE_REWRITE_RULE thl = CONV_RULE(PURE_REWRITE_CONV thl);;
 447
 448 let REWRITE_RULE thl = CONV_RULE(REWRITE_CONV thl);;
 449
 450 let PURE_ONCE_REWRITE_RULE thl = CONV_RULE(PURE_ONCE_REWRITE_CONV thl);;
 451
 452 let ONCE_REWRITE_RULE thl = CONV_RULE(ONCE_REWRITE_CONV thl);;
 453
 454 let PURE_ASM_REWRITE_RULE thl th =
 455     PURE_REWRITE_RULE ((map ASSUME (hyp th)) @ thl) th;;
 456
 457 let ASM_REWRITE_RULE thl th =
 458     REWRITE_RULE ((map ASSUME (hyp th)) @ thl) th;;
 459
 460 let PURE_ONCE_ASM_REWRITE_RULE thl th =
 461     PURE_ONCE_REWRITE_RULE ((map ASSUME (hyp th)) @ thl) th;;
 462
 463 let ONCE_ASM_REWRITE_RULE thl th =
 464     ONCE_REWRITE_RULE ((map ASSUME (hyp th)) @ thl) th;;
 465
 466 let GEN_REWRITE_TAC cnvl thl = CONV_TAC(GEN_REWRITE_CONV cnvl thl);;
 467
 468 let PURE_REWRITE_TAC thl = CONV_TAC(PURE_REWRITE_CONV thl);;
 469
 470 let REWRITE_TAC thl = CONV_TAC(REWRITE_CONV thl);;
 471
 472 let PURE_ONCE_REWRITE_TAC thl = CONV_TAC(PURE_ONCE_REWRITE_CONV thl);;
 473
 474 let ONCE_REWRITE_TAC thl = CONV_TAC(ONCE_REWRITE_CONV thl);;
 475
 476 let (PURE_ASM_REWRITE_TAC: thm list -> tactic) =
 477   ASM PURE_REWRITE_TAC;;
 478
 479 let (ASM_REWRITE_TAC: thm list -> tactic) =
 480   ASM REWRITE_TAC;;
 481
 482 let (PURE_ONCE_ASM_REWRITE_TAC: thm list -> tactic) =
 483   ASM PURE_ONCE_REWRITE_TAC;;
 484
 485 let (ONCE_ASM_REWRITE_TAC: thm list -> tactic) =
 486   ASM ONCE_REWRITE_TAC;;
 487
 488 (* ------------------------------------------------------------------------- *)
 489 (* Simplification functions.                                                 *)
 490 (* ------------------------------------------------------------------------- *)
 491
 492 let GEN_SIMPLIFY_CONV (strat:strategy) ss lev thl =
 493   let ss' = itlist AUGMENT_SIMPSET thl ss in
 494   TRY_CONV (strat ss' lev);;
 495
 496 let ONCE_SIMPLIFY_CONV ss = GEN_SIMPLIFY_CONV ONCE_DEPTH_SQCONV ss 1;;
 497
 498 let SIMPLIFY_CONV ss = GEN_SIMPLIFY_CONV TOP_DEPTH_SQCONV ss 3;;
 499
 500 (* ------------------------------------------------------------------------- *)
 501 (* Simple but useful default version.                                        *)
 502 (* ------------------------------------------------------------------------- *)
 503
 504 let empty_ss = Simpset(empty_net,basic_prover,[],mk_rewrites true);;
 505
 506 let basic_ss =
 507   let rewmaker = mk_rewrites true in
 508   fun thl ->
 509     let cthms = itlist rewmaker thl [] in
 510     let net' = itlist (net_of_thm true) cthms (basic_net()) in
 511     let net'' = itlist net_of_cong (basic_congs()) net' in
 512   Simpset(net'',basic_prover,[],rewmaker);;
 513
 514 let SIMP_CONV thl = SIMPLIFY_CONV (basic_ss []) thl;;
 515
 516 let PURE_SIMP_CONV thl = SIMPLIFY_CONV empty_ss thl;;
 517
 518 let ONCE_SIMP_CONV thl = ONCE_SIMPLIFY_CONV (basic_ss []) thl;;
 519
 520 let SIMP_RULE thl = CONV_RULE(SIMP_CONV thl);;
 521
 522 let PURE_SIMP_RULE thl = CONV_RULE(PURE_SIMP_CONV thl);;
 523
 524 let ONCE_SIMP_RULE thl = CONV_RULE(ONCE_SIMP_CONV thl);;
 525
 526 let SIMP_TAC thl = CONV_TAC(SIMP_CONV thl);;
 527
 528 let PURE_SIMP_TAC thl = CONV_TAC(PURE_SIMP_CONV thl);;
 529
 530 let ONCE_SIMP_TAC thl = CONV_TAC(ONCE_SIMP_CONV thl);;
 531
 532 let ASM_SIMP_TAC = ASM SIMP_TAC;;
 533
 534 let PURE_ASM_SIMP_TAC = ASM PURE_SIMP_TAC;;
 535
 536 let ONCE_ASM_SIMP_TAC = ASM ONCE_SIMP_TAC;;
 537
 538 (* ------------------------------------------------------------------------- *)
 539 (* Abbreviation tactics.                                                     *)
 540 (* ------------------------------------------------------------------------- *)
 541
 542 let ABBREV_TAC tm =
 543   let cvs,t = dest_eq tm in
 544   let v,vs = strip_comb cvs in
 545   let rs = list_mk_abs(vs,t) in
 546   let eq = mk_eq(rs,v) in
 547   let th1 = itlist (fun v th -> CONV_RULE(LAND_CONV BETA_CONV) (AP_THM th v))
 548                    (rev vs) (ASSUME eq) in
 549   let th2 = SIMPLE_CHOOSE v (SIMPLE_EXISTS v (GENL vs th1)) in
 550   let th3 = PROVE_HYP (EXISTS(mk_exists(v,eq),rs) (REFL rs)) th2 in
 551   fun (asl,w as gl) ->
 552     let avoids = itlist (union o frees o concl o snd) asl (frees w) in
 553     if mem v avoids then failwith "ABBREV_TAC: variable already used" else
 554     CHOOSE_THEN
 555      (fun th -> RULE_ASSUM_TAC(PURE_ONCE_REWRITE_RULE[th]) THEN
 556                 PURE_ONCE_REWRITE_TAC[th] THEN
 557                 ASSUME_TAC th)
 558      th3 gl;;
 559
 560 let EXPAND_TAC s = FIRST_ASSUM(SUBST1_TAC o SYM o
 561   check((=) s o fst o dest_var o rhs o concl)) THEN BETA_TAC;;