tactics.ml

   1 (* ========================================================================= *)
   2 (* System of tactics (slightly different from any traditional LCF method).   *)
   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 (*                 (c) Copyright, Marco Maggesi 2012                         *)
   9 (* ========================================================================= *)
  10
  11 needs "drule.ml";;
  12
  13 (* ------------------------------------------------------------------------- *)
  14 (* The common case of trivial instantiations.                                *)
  15 (* ------------------------------------------------------------------------- *)
  16
  17 let null_inst = ([],[],[] :instantiation);;
  18
  19 let null_meta = (([]:term list),null_inst);;
  20
  21 (* ------------------------------------------------------------------------- *)
  22 (* A goal has labelled assumptions, and the hyps are now thms.               *)
  23 (* ------------------------------------------------------------------------- *)
  24
  25 type goal = (string * thm) list * term;;
  26
  27 let equals_goal ((a,w):goal) ((a',w'):goal) =
  28   forall2 (fun (s,th) (s',th') -> s = s' & equals_thm th th') a a' & w = w';;
  29
  30 (* ------------------------------------------------------------------------- *)
  31 (* A justification function for a goalstate [A1 ?- g1; ...; An ?- gn],       *)
  32 (* starting from an initial goal A ?- g, is a function f such that for any   *)
  33 (* instantiation @:                                                          *)
  34 (*                                                                           *)
  35 (*   f(@) [A1@ |- g1@; ...; An@ |- gn@] = A@ |- g@                           *)
  36 (* ------------------------------------------------------------------------- *)
  37
  38 type justification = instantiation -> thm list -> thm;;
  39
  40 (* ------------------------------------------------------------------------- *)
  41 (* The goalstate stores the subgoals, justification, current instantiation,  *)
  42 (* and a list of metavariables.                                              *)
  43 (* ------------------------------------------------------------------------- *)
  44
  45 type goalstate = (term list * instantiation) * goal list * justification;;
  46
  47 (* ------------------------------------------------------------------------- *)
  48 (* A goalstack is just a list of goalstates. Could go for more...            *)
  49 (* ------------------------------------------------------------------------- *)
  50
  51 type goalstack = goalstate list;;
  52
  53 (* ------------------------------------------------------------------------- *)
  54 (* A refinement, applied to a goalstate [A1 ?- g1; ...; An ?- gn]            *)
  55 (* yields a new goalstate with updated justification function, to            *)
  56 (* give a possibly-more-instantiated version of the initial goal.            *)
  57 (* ------------------------------------------------------------------------- *)
  58
  59 type refinement = goalstate -> goalstate;;
  60
  61 (* ------------------------------------------------------------------------- *)
  62 (* A tactic, applied to a goal A ?- g, returns:                              *)
  63 (*                                                                           *)
  64 (*  o A list of new metavariables introduced                                 *)
  65 (*  o An instantiation (%)                                                   *)
  66 (*  o A list of subgoals                                                     *)
  67 (*  o A justification f such that for any instantiation @ we have            *)
  68 (*    f(@) [A1@  |- g1@; ...; An@ |- gn@] = A(%;@) |- g(%;@)                 *)
  69 (* ------------------------------------------------------------------------- *)
  70
  71 type tactic = goal -> goalstate;;
  72
  73 type thm_tactic = thm -> tactic;;
  74
  75 type thm_tactical = thm_tactic -> thm_tactic;;
  76
  77 (* ------------------------------------------------------------------------- *)
  78 (* Apply instantiation to a goal.                                            *)
  79 (* ------------------------------------------------------------------------- *)
  80
  81 let (inst_goal:instantiation->goal->goal) =
  82   fun p (thms,w) ->
  83     map (I F_F INSTANTIATE_ALL p) thms,instantiate p w;;
  84
  85 (* ------------------------------------------------------------------------- *)
  86 (* Perform a sequential composition (left first) of instantiations.          *)
  87 (* ------------------------------------------------------------------------- *)
  88
  89 let (compose_insts :instantiation->instantiation->instantiation) =
  90   fun (pats1,tmin1,tyin1) ((pats2,tmin2,tyin2) as i2) ->
  91     let tmin = map (instantiate i2 F_F inst tyin2) tmin1
  92     and tyin = map (type_subst tyin2 F_F I) tyin1 in
  93     let tmin' = filter (fun (_,x) -> not (can (rev_assoc x) tmin)) tmin2
  94     and tyin' = filter (fun (_,a) -> not (can (rev_assoc a) tyin)) tyin2 in
  95     pats1@pats2,tmin@tmin',tyin@tyin';;
  96
  97 (* ------------------------------------------------------------------------- *)
  98 (* Construct A,_FALSITY_ |- p; contortion so falsity is the last element.    *)
  99 (* ------------------------------------------------------------------------- *)
 100
 101 let _FALSITY_ = new_definition `_FALSITY_ = F`;;
 102
 103 let mk_fthm =
 104   let pth = UNDISCH(fst(EQ_IMP_RULE _FALSITY_))
 105   and qth = ASSUME `_FALSITY_` in
 106   fun (asl,c) -> PROVE_HYP qth (itlist ADD_ASSUM (rev asl) (CONTR c pth));;
 107
 108 (* ------------------------------------------------------------------------- *)
 109 (* Validity checking of tactics. This cannot be 100% accurate without making *)
 110 (* arbitrary theorems, but "mk_fthm" brings us quite close.                  *)
 111 (* ------------------------------------------------------------------------- *)
 112
 113 let (VALID:tactic->tactic) =
 114   let fake_thm (asl,w) =
 115     let asms = itlist (union o hyp o snd) asl [] in
 116     mk_fthm(asms,w)
 117   and false_tm = `_FALSITY_` in
 118   fun tac (asl,w) ->
 119     let ((mvs,i),gls,just as res) = tac (asl,w) in
 120     let ths = map fake_thm gls in
 121     let asl',w' = dest_thm(just null_inst ths) in
 122     let asl'',w'' = inst_goal i (asl,w) in
 123     let maxasms =
 124       itlist (fun (_,th) -> union (insert (concl th) (hyp th))) asl'' [] in
 125     if aconv w' w'' &
 126        forall (fun t -> exists (aconv t) maxasms) (subtract asl' [false_tm])
 127     then res else failwith "VALID: Invalid tactic";;
 128
 129 (* ------------------------------------------------------------------------- *)
 130 (* Various simple combinators for tactics, identity tactic etc.              *)
 131 (* ------------------------------------------------------------------------- *)
 132
 133 let (THEN),(THENL) =
 134   let propagate_empty i [] = []
 135   and propagate_thm th i [] = INSTANTIATE_ALL i th in
 136   let compose_justs n just1 just2 i ths =
 137     let ths1,ths2 = chop_list n ths in
 138     (just1 i ths1)::(just2 i ths2) in
 139   let rec seqapply l1 l2 = match (l1,l2) with
 140      ([],[]) -> null_meta,[],propagate_empty
 141    | ((tac:tactic)::tacs),((goal:goal)::goals) ->
 142             let ((mvs1,insts1),gls1,just1) = tac goal in
 143             let goals' = map (inst_goal insts1) goals in
 144             let ((mvs2,insts2),gls2,just2) = seqapply tacs goals' in
 145             ((union mvs1 mvs2,compose_insts insts1 insts2),
 146              gls1@gls2,compose_justs (length gls1) just1 just2)
 147    | _,_ -> failwith "seqapply: Length mismatch" in
 148   let justsequence just1 just2 insts2 i ths =
 149     just1 (compose_insts insts2 i) (just2 i ths) in
 150   let tacsequence ((mvs1,insts1),gls1,just1) tacl =
 151     let ((mvs2,insts2),gls2,just2) = seqapply tacl gls1 in
 152     let jst = justsequence just1 just2 insts2 in
 153     let just = if gls2 = [] then propagate_thm (jst null_inst []) else jst in
 154     ((union mvs1 mvs2,compose_insts insts1 insts2),gls2,just) in
 155   let (then_: tactic -> tactic -> tactic) =
 156     fun tac1 tac2 g ->
 157       let _,gls,_ as gstate = tac1 g in
 158       tacsequence gstate (replicate tac2 (length gls))
 159   and (thenl_: tactic -> tactic list -> tactic) =
 160     fun tac1 tac2l g ->
 161       let _,gls,_ as gstate = tac1 g in
 162       if gls = [] then tacsequence gstate []
 163       else tacsequence gstate tac2l in
 164   then_,thenl_;;
 165
 166 let ((ORELSE): tactic -> tactic -> tactic) =
 167   fun tac1 tac2 g ->
 168     try tac1 g with Failure _ -> tac2 g;;
 169
 170 let (FAIL_TAC: string -> tactic) =
 171   fun tok g -> failwith tok;;
 172
 173 let (NO_TAC: tactic) =
 174   FAIL_TAC "NO_TAC";;
 175
 176 let (ALL_TAC:tactic) =
 177   fun g -> null_meta,[g],fun _ [th] -> th;;
 178
 179 let TRY tac =
 180   tac ORELSE ALL_TAC;;
 181
 182 let rec REPEAT tac g =
 183   ((tac THEN REPEAT tac) ORELSE ALL_TAC) g;;
 184
 185 let EVERY tacl =
 186   itlist (fun t1 t2 -> t1 THEN t2) tacl ALL_TAC;;
 187
 188 let (FIRST: tactic list -> tactic) =
 189   fun tacl g -> end_itlist (fun t1 t2 -> t1 ORELSE t2) tacl g;;
 190
 191 let MAP_EVERY tacf lst =
 192   EVERY (map tacf lst);;
 193
 194 let MAP_FIRST tacf lst =
 195   FIRST (map tacf lst);;
 196
 197 let (CHANGED_TAC: tactic -> tactic) =
 198   fun tac g ->
 199     let (meta,gl,_ as gstate) = tac g in
 200     if meta = null_meta & length gl = 1 & equals_goal (hd gl) g
 201     then failwith "CHANGED_TAC" else gstate;;
 202
 203 let rec REPLICATE_TAC n tac =
 204   if n <= 0 then ALL_TAC else tac THEN (REPLICATE_TAC (n - 1) tac);;
 205
 206 (* ------------------------------------------------------------------------- *)
 207 (* Combinators for theorem continuations / "theorem tacticals".              *)
 208 (* ------------------------------------------------------------------------- *)
 209
 210 let ((THEN_TCL): thm_tactical -> thm_tactical -> thm_tactical) =
 211   fun ttcl1 ttcl2 ttac -> ttcl1 (ttcl2 ttac);;
 212
 213 let ((ORELSE_TCL): thm_tactical -> thm_tactical -> thm_tactical) =
 214   fun ttcl1 ttcl2 ttac th ->
 215     try ttcl1 ttac th with Failure _ -> ttcl2 ttac th;;
 216
 217 let rec REPEAT_TCL ttcl ttac th =
 218   ((ttcl THEN_TCL (REPEAT_TCL ttcl)) ORELSE_TCL I) ttac th;;
 219
 220 let (REPEAT_GTCL: thm_tactical -> thm_tactical) =
 221   let rec REPEAT_GTCL ttcl ttac th g =
 222     try ttcl (REPEAT_GTCL ttcl ttac) th g with Failure _ -> ttac th g in
 223   REPEAT_GTCL;;
 224
 225 let (ALL_THEN: thm_tactical) =
 226   I;;
 227
 228 let (NO_THEN: thm_tactical) =
 229   fun ttac th -> failwith "NO_THEN";;
 230
 231 let EVERY_TCL ttcll =
 232   itlist (fun t1 t2 -> t1 THEN_TCL t2) ttcll ALL_THEN;;
 233
 234 let FIRST_TCL ttcll =
 235   end_itlist (fun t1 t2 -> t1 ORELSE_TCL t2) ttcll;;
 236
 237 (* ------------------------------------------------------------------------- *)
 238 (* Tactics to augment assumption list. Note that to allow "ASSUME p" for     *)
 239 (* any assumption "p", these add a PROVE_HYP in the justification function,  *)
 240 (* just in case.                                                             *)
 241 (* ------------------------------------------------------------------------- *)
 242
 243 let (LABEL_TAC: string -> thm_tactic) =
 244   fun s thm (asl,w) ->
 245     null_meta,[(s,thm)::asl,w],
 246     fun i [th] -> PROVE_HYP (INSTANTIATE_ALL i thm) th;;
 247
 248 let ASSUME_TAC = LABEL_TAC "";;
 249
 250 (* ------------------------------------------------------------------------- *)
 251 (* Manipulation of assumption list.                                          *)
 252 (* ------------------------------------------------------------------------- *)
 253
 254 let (FIND_ASSUM: thm_tactic -> term -> tactic) =
 255   fun ttac t ((asl,w) as g) ->
 256     ttac(snd(find (fun (_,th) -> concl th = t) asl)) g;;
 257
 258 let (POP_ASSUM: thm_tactic -> tactic) =
 259   fun ttac ->
 260    function (((_,th)::asl),w) -> ttac th (asl,w)
 261     | _ -> failwith "POP_ASSUM: No assumption to pop";;
 262
 263 let (ASSUM_LIST: (thm list -> tactic) -> tactic) =
 264     fun aslfun (asl,w) -> aslfun (map snd asl) (asl,w);;
 265
 266 let (POP_ASSUM_LIST: (thm list -> tactic) -> tactic) =
 267   fun asltac (asl,w) -> asltac (map snd asl) ([],w);;
 268
 269 let (EVERY_ASSUM: thm_tactic -> tactic) =
 270   fun ttac -> ASSUM_LIST (MAP_EVERY ttac);;
 271
 272 let (FIRST_ASSUM: thm_tactic -> tactic) =
 273   fun ttac (asl,w as g) -> tryfind (fun (_,th) -> ttac th g) asl;;
 274
 275 let (RULE_ASSUM_TAC :(thm->thm)->tactic) =
 276   fun rule (asl,w) -> (POP_ASSUM_LIST(K ALL_TAC) THEN
 277                        MAP_EVERY (fun (s,th) -> LABEL_TAC s (rule th))
 278                                  (rev asl)) (asl,w);;
 279
 280 (* ------------------------------------------------------------------------- *)
 281 (* Operate on assumption identified by a label.                              *)
 282 (* ------------------------------------------------------------------------- *)
 283
 284 let (USE_THEN:string->thm_tactic->tactic) =
 285   fun s ttac (asl,w as gl) ->
 286     let th = try assoc s asl with Failure _ ->
 287              failwith("USE_TAC: didn't find assumption "^s) in
 288     ttac th gl;;
 289
 290 let (REMOVE_THEN:string->thm_tactic->tactic) =
 291   fun s ttac (asl,w) ->
 292     let th = try assoc s asl with Failure _ ->
 293              failwith("USE_TAC: didn't find assumption "^s) in
 294     let asl1,asl2 = chop_list(index s (map fst asl)) asl in
 295     let asl' = asl1 @ tl asl2 in
 296     ttac th (asl',w);;
 297
 298 (* ------------------------------------------------------------------------- *)
 299 (* General tools to augment a required set of theorems with assumptions.     *)
 300 (* Here ASM uses all current hypotheses of the goal, while HYP uses only     *)
 301 (* those whose labels are given in the string argument.                      *)
 302 (* ------------------------------------------------------------------------- *)
 303
 304 let (ASM :(thm list -> tactic)->(thm list -> tactic)) =
 305   fun tltac ths (asl,w as g) -> tltac (map snd asl @ ths) g;;
 306
 307 let HYP =
 308   let ident = function
 309       Ident s::rest when isalnum s -> s,rest
 310     | _ -> raise Noparse in
 311   let parse_using = many ident in
 312   let HYP_LIST tac l =
 313     rev_itlist (fun s k l -> USE_THEN s (fun th -> k (th::l))) l tac in
 314   fun tac s ->
 315     let l,rest = (fix "Using pattern" parse_using o lex o explode) s in
 316     if rest=[] then HYP_LIST tac l else failwith "Invalid using pattern";;
 317
 318 (* ------------------------------------------------------------------------- *)
 319 (* Basic tactic to use a theorem equal to the goal. Does *no* matching.      *)
 320 (* ------------------------------------------------------------------------- *)
 321
 322 let (ACCEPT_TAC: thm_tactic) =
 323   let propagate_thm th i [] = INSTANTIATE_ALL i th in
 324   fun th (asl,w) ->
 325     if aconv (concl th) w then
 326       null_meta,[],propagate_thm th
 327     else failwith "ACCEPT_TAC";;
 328
 329 (* ------------------------------------------------------------------------- *)
 330 (* Create tactic from a conversion. This allows the conversion to return     *)
 331 (* |- p rather than |- p = T on a term "p". It also eliminates any goals of  *)
 332 (* the form "T" automatically.                                               *)
 333 (* ------------------------------------------------------------------------- *)
 334
 335 let (CONV_TAC: conv -> tactic) =
 336   let t_tm = `T` in
 337   fun conv ((asl,w) as g) ->
 338     let th = conv w in
 339     let tm = concl th in
 340     if aconv tm w then ACCEPT_TAC th g else
 341     let l,r = dest_eq tm in
 342     if not(aconv l w) then failwith "CONV_TAC: bad equation" else
 343     if r = t_tm then ACCEPT_TAC(EQT_ELIM th) g else
 344     let th' = SYM th in
 345     null_meta,[asl,r],fun i [th] -> EQ_MP (INSTANTIATE_ALL i th') th;;
 346
 347 (* ------------------------------------------------------------------------- *)
 348 (* Tactics for equality reasoning.                                           *)
 349 (* ------------------------------------------------------------------------- *)
 350
 351 let (REFL_TAC: tactic) =
 352   fun ((asl,w) as g) ->
 353     try ACCEPT_TAC(REFL(rand w)) g
 354     with Failure _ -> failwith "REFL_TAC";;
 355
 356 let (ABS_TAC: tactic) =
 357   fun (asl,w) ->
 358     try let l,r = dest_eq w in
 359         let lv,lb = dest_abs l
 360         and rv,rb = dest_abs r in
 361         let avoids = itlist (union o thm_frees o snd) asl (frees w) in
 362         let v = mk_primed_var avoids lv in
 363         null_meta,[asl,mk_eq(vsubst[v,lv] lb,vsubst[v,rv] rb)],
 364         fun i [th] -> let ath = ABS v th in
 365                       EQ_MP (ALPHA (concl ath) (instantiate i w)) ath
 366     with Failure _ -> failwith "ABS_TAC";;
 367
 368 let (MK_COMB_TAC: tactic) =
 369   fun (asl,gl) ->
 370     try let l,r = dest_eq gl in
 371         let f,x = dest_comb l
 372         and g,y = dest_comb r in
 373         null_meta,[asl,mk_eq(f,g); asl,mk_eq(x,y)],
 374         fun _ [th1;th2] -> MK_COMB(th1,th2)
 375     with Failure _ -> failwith "MK_COMB_TAC";;
 376
 377 let (AP_TERM_TAC: tactic) =
 378   let tac = MK_COMB_TAC THENL [REFL_TAC; ALL_TAC] in
 379   fun gl -> try tac gl with Failure _ -> failwith "AP_TERM_TAC";;
 380
 381 let (AP_THM_TAC: tactic) =
 382   let tac = MK_COMB_TAC THENL [ALL_TAC; REFL_TAC] in
 383   fun gl -> try tac gl with Failure _ -> failwith "AP_THM_TAC";;
 384
 385 let (BINOP_TAC: tactic) =
 386   let tac = MK_COMB_TAC THENL [AP_TERM_TAC; ALL_TAC] in
 387   fun gl -> try tac gl with Failure _ -> failwith "AP_THM_TAC";;
 388
 389 let (SUBST1_TAC: thm_tactic) =
 390   fun th -> CONV_TAC(SUBS_CONV [th]);;
 391
 392 let SUBST_ALL_TAC rth =
 393   SUBST1_TAC rth THEN RULE_ASSUM_TAC (SUBS [rth]);;
 394
 395 let BETA_TAC = CONV_TAC(REDEPTH_CONV BETA_CONV);;
 396
 397 (* ------------------------------------------------------------------------- *)
 398 (* Just use an equation to substitute if possible and uninstantiable.        *)
 399 (* ------------------------------------------------------------------------- *)
 400
 401 let SUBST_VAR_TAC th =
 402   try let asm,eq = dest_thm th in
 403       let l,r = dest_eq eq in
 404       if aconv l r then ALL_TAC
 405       else if not (subset (frees eq) (freesl asm)) then fail()
 406       else if (is_const l or is_var l) & not(free_in l r)
 407            then SUBST_ALL_TAC th
 408       else if (is_const r or is_var r) & not(free_in r l)
 409            then SUBST_ALL_TAC(SYM th)
 410       else fail()
 411   with Failure _ -> failwith "SUBST_VAR_TAC";;
 412
 413 (* ------------------------------------------------------------------------- *)
 414 (* Basic logical tactics.                                                    *)
 415 (* ------------------------------------------------------------------------- *)
 416
 417 let (DISCH_TAC: tactic) =
 418   let f_tm = `F` in
 419   fun (asl,w) ->
 420     try let ant,c = dest_imp w in
 421         let th1 = ASSUME ant in
 422         null_meta,[("",th1)::asl,c],
 423         fun i [th] -> DISCH (instantiate i ant) th
 424     with Failure _ -> try
 425         let ant = dest_neg w in
 426         let th1 = ASSUME ant in
 427         null_meta,[("",th1)::asl,f_tm],
 428         fun i [th] -> NOT_INTRO(DISCH (instantiate i ant) th)
 429     with Failure _ -> failwith "DISCH_TAC";;
 430
 431 let (MP_TAC: thm_tactic) =
 432   fun thm (asl,w) ->
 433     null_meta,[asl,mk_imp(concl thm,w)],
 434     fun i [th] -> MP th (INSTANTIATE_ALL i thm);;
 435
 436 let (EQ_TAC: tactic) =
 437   fun (asl,w) ->
 438     try let l,r = dest_eq w in
 439         null_meta,[asl, mk_imp(l,r); asl, mk_imp(r,l)],
 440         fun _ [th1; th2] -> IMP_ANTISYM_RULE th1 th2
 441     with Failure _ -> failwith "EQ_TAC";;
 442
 443 let (UNDISCH_TAC: term -> tactic) =
 444  fun tm (asl,w) ->
 445    try let sthm,asl' = remove (fun (_,asm) -> aconv (concl asm) tm) asl in
 446        let thm = snd sthm in
 447        null_meta,[asl',mk_imp(tm,w)],
 448        fun i [th] -> MP th (INSTANTIATE_ALL i thm)
 449    with Failure _ -> failwith "UNDISCH_TAC";;
 450
 451 let (SPEC_TAC: term * term -> tactic) =
 452   fun (t,x) (asl,w) ->
 453     try null_meta,[asl, mk_forall(x,subst[x,t] w)],
 454         fun i [th] -> SPEC (instantiate i t) th
 455     with Failure _ -> failwith "SPEC_TAC";;
 456
 457 let (X_GEN_TAC: term -> tactic),
 458     (X_CHOOSE_TAC: term -> thm_tactic),
 459     (EXISTS_TAC: term -> tactic) =
 460   let tactic_type_compatibility_check pfx e g =
 461     let et = type_of e and gt = type_of g in
 462     if et = gt then ()
 463     else failwith(pfx ^ ": expected type :"^string_of_type et^" but got :"^
 464                   string_of_type gt) in
 465   let X_GEN_TAC x' =
 466     if not(is_var x') then failwith "X_GEN_TAC: not a variable" else
 467     fun (asl,w) ->
 468         let x,bod = try dest_forall w
 469           with Failure _ -> failwith "X_GEN_TAC: Not universally quantified" in
 470         let _ = tactic_type_compatibility_check "X_GEN_TAC" x x' in
 471         let avoids = itlist (union o thm_frees o snd) asl (frees w) in
 472         if mem x' avoids then failwith "X_GEN_TAC: invalid variable" else
 473         let afn = CONV_RULE(GEN_ALPHA_CONV x) in
 474         null_meta,[asl,vsubst[x',x] bod],
 475         fun i [th] -> afn (GEN x' th)
 476   and X_CHOOSE_TAC x' xth =
 477         let xtm = concl xth in
 478         let x,bod = try dest_exists xtm
 479          with Failure _ -> failwith "X_CHOOSE_TAC: not existential" in
 480         let _ = tactic_type_compatibility_check "X_CHOOSE_TAC" x x' in
 481         let pat = vsubst[x',x] bod in
 482         let xth' = ASSUME pat in
 483         fun (asl,w) ->
 484           let avoids = itlist (union o frees o concl o snd) asl
 485                               (union (frees w) (thm_frees xth)) in
 486           if mem x' avoids then failwith "X_CHOOSE_TAC: invalid variable" else
 487           null_meta,[("",xth')::asl,w],
 488           fun i [th] -> CHOOSE(x',INSTANTIATE_ALL i xth) th
 489   and EXISTS_TAC t (asl,w) =
 490     let v,bod = try dest_exists w with Failure _ ->
 491                 failwith "EXISTS_TAC: Goal not existentially quantified" in
 492     let _ = tactic_type_compatibility_check "EXISTS_TAC" v t in
 493     null_meta,[asl,vsubst[t,v] bod],
 494     fun i [th] -> EXISTS (instantiate i w,instantiate i t) th in
 495   X_GEN_TAC,X_CHOOSE_TAC,EXISTS_TAC;;
 496
 497 let (GEN_TAC: tactic) =
 498   fun (asl,w) ->
 499     try let x = fst(dest_forall w) in
 500         let avoids = itlist (union o thm_frees o snd) asl (frees w) in
 501         let x' = mk_primed_var avoids x in
 502         X_GEN_TAC x' (asl,w)
 503     with Failure _ -> failwith "GEN_TAC";;
 504
 505 let (CHOOSE_TAC: thm_tactic) =
 506   fun xth ->
 507     try let x = fst(dest_exists(concl xth)) in
 508         fun (asl,w) ->
 509           let avoids = itlist (union o thm_frees o snd) asl
 510                               (union (frees w) (thm_frees xth)) in
 511           let x' = mk_primed_var avoids x in
 512           X_CHOOSE_TAC x' xth (asl,w)
 513       with Failure _ -> failwith "CHOOSE_TAC";;
 514
 515 let (CONJ_TAC: tactic) =
 516   fun (asl,w) ->
 517     try let l,r = dest_conj w in
 518         null_meta,[asl,l; asl,r],fun _ [th1;th2] -> CONJ th1 th2
 519     with Failure _ -> failwith "CONJ_TAC";;
 520
 521 let (DISJ1_TAC: tactic) =
 522   fun (asl,w) ->
 523     try let l,r = dest_disj w in
 524         null_meta,[asl,l],fun i [th] -> DISJ1 th (instantiate i r)
 525     with Failure _ -> failwith "DISJ1_TAC";;
 526
 527 let (DISJ2_TAC: tactic) =
 528   fun (asl,w) ->
 529     try let l,r = dest_disj w in
 530           null_meta,[asl,r],fun i [th] -> DISJ2 (instantiate i l) th
 531     with Failure _ -> failwith "DISJ2_TAC";;
 532
 533 let (DISJ_CASES_TAC: thm_tactic) =
 534   fun dth ->
 535     try let dtm = concl dth in
 536         let l,r = dest_disj dtm in
 537         let thl = ASSUME l
 538         and thr = ASSUME r in
 539         fun (asl,w) ->
 540           null_meta,[("",thl)::asl,w; ("",thr)::asl,w],
 541           fun i [th1;th2] -> DISJ_CASES (INSTANTIATE_ALL i dth) th1 th2
 542     with Failure _ -> failwith "DISJ_CASES_TAC";;
 543
 544 let (CONTR_TAC: thm_tactic) =
 545   let propagate_thm th i [] = INSTANTIATE_ALL i th in
 546   fun cth (asl,w) ->
 547     try let th = CONTR w cth in
 548         null_meta,[],propagate_thm th
 549     with Failure _ -> failwith "CONTR_TAC";;
 550
 551 let (MATCH_ACCEPT_TAC:thm_tactic) =
 552   let propagate_thm th i [] = INSTANTIATE_ALL i th in
 553   let rawtac th (asl,w) =
 554     try let ith = PART_MATCH I th w in
 555         null_meta,[],propagate_thm ith
 556     with Failure _ -> failwith "ACCEPT_TAC" in
 557   fun th -> REPEAT GEN_TAC THEN rawtac th;;
 558
 559 let (MATCH_MP_TAC :thm_tactic) =
 560   fun th ->
 561     let sth =
 562       try let tm = concl th in
 563           let avs,bod = strip_forall tm in
 564           let ant,con = dest_imp bod in
 565           let th1 = SPECL avs (ASSUME tm) in
 566           let th2 = UNDISCH th1 in
 567           let evs = filter (fun v -> vfree_in v ant & not (vfree_in v con))
 568                            avs in
 569           let th3 = itlist SIMPLE_CHOOSE evs (DISCH tm th2) in
 570           let tm3 = hd(hyp th3) in
 571           MP (DISCH tm (GEN_ALL (DISCH tm3 (UNDISCH th3)))) th
 572       with Failure _ -> failwith "MATCH_MP_TAC: Bad theorem" in
 573     let match_fun = PART_MATCH (snd o dest_imp) sth in
 574     fun (asl,w) -> try let xth = match_fun w in
 575                        let lant = fst(dest_imp(concl xth)) in
 576                        null_meta,[asl,lant],
 577                        fun i [th] -> MP (INSTANTIATE_ALL i xth) th
 578                    with Failure _ -> failwith "MATCH_MP_TAC: No match";;
 579
 580 let (TRANS_TAC:thm->term->tactic) =
 581   fun th ->
 582     let ctm = snd(strip_forall(concl th)) in
 583     let cl,cr = dest_conj(lhand ctm) in
 584     let x = lhand cl and y = rand cl and z = rand cr in
 585     fun tm (asl,w as gl) ->
 586       let lop,r = dest_comb w in
 587       let op,l = dest_comb lop in
 588       let ilist =
 589         itlist2 type_match (map type_of [x;y;z])(map type_of [l;tm;r]) [] in
 590       let th' = INST_TYPE ilist th in
 591       (MATCH_MP_TAC th' THEN EXISTS_TAC tm) gl;;
 592
 593 (* ------------------------------------------------------------------------- *)
 594 (* Theorem continuations.                                                    *)
 595 (* ------------------------------------------------------------------------- *)
 596
 597 let (CONJUNCTS_THEN2:thm_tactic->thm_tactic->thm_tactic) =
 598   fun ttac1 ttac2 cth ->
 599       let c1,c2 = dest_conj(concl cth) in
 600       fun gl -> let ti,gls,jfn = (ttac1(ASSUME c1) THEN ttac2(ASSUME c2)) gl in
 601                 let jfn' i ths =
 602                   let th1,th2 = CONJ_PAIR(INSTANTIATE_ALL i cth) in
 603                   PROVE_HYP th1 (PROVE_HYP th2 (jfn i ths)) in
 604                 ti,gls,jfn';;
 605
 606 let (CONJUNCTS_THEN: thm_tactical) =
 607   W CONJUNCTS_THEN2;;
 608
 609 let (DISJ_CASES_THEN2:thm_tactic->thm_tactic->thm_tactic) =
 610   fun ttac1 ttac2 cth ->
 611     DISJ_CASES_TAC cth THENL [POP_ASSUM ttac1; POP_ASSUM ttac2];;
 612
 613 let (DISJ_CASES_THEN: thm_tactical) =
 614   W DISJ_CASES_THEN2;;
 615
 616 let (DISCH_THEN: thm_tactic -> tactic) =
 617   fun ttac -> DISCH_TAC THEN POP_ASSUM ttac;;
 618
 619 let (X_CHOOSE_THEN: term -> thm_tactical) =
 620   fun x ttac th -> X_CHOOSE_TAC x th THEN POP_ASSUM ttac;;
 621
 622 let (CHOOSE_THEN: thm_tactical) =
 623   fun ttac th -> CHOOSE_TAC th THEN POP_ASSUM ttac;;
 624
 625 (* ------------------------------------------------------------------------- *)
 626 (* Various derived tactics and theorem continuations.                        *)
 627 (* ------------------------------------------------------------------------- *)
 628
 629 let STRIP_THM_THEN =
 630   FIRST_TCL [CONJUNCTS_THEN; DISJ_CASES_THEN; CHOOSE_THEN];;
 631
 632 let (ANTE_RES_THEN: thm_tactical) =
 633   fun ttac ante ->
 634     ASSUM_LIST
 635      (fun asl ->
 636         let tacs = mapfilter (fun imp -> ttac (MATCH_MP imp ante)) asl in
 637         if tacs = [] then failwith "IMP_RES_THEN"
 638         else EVERY tacs);;
 639
 640 let (IMP_RES_THEN: thm_tactical) =
 641   fun ttac imp ->
 642     ASSUM_LIST
 643      (fun asl ->
 644         let tacs = mapfilter (fun ante -> ttac (MATCH_MP imp ante)) asl in
 645         if tacs = [] then failwith "IMP_RES_THEN"
 646         else EVERY tacs);;
 647
 648 let STRIP_ASSUME_TAC =
 649   let DISCARD_TAC th =
 650     let tm = concl th in
 651     fun (asl,w as g) ->
 652        if exists (fun a -> aconv tm (concl(snd a))) asl then ALL_TAC g
 653        else failwith "DISCARD_TAC: not already present" in
 654   (REPEAT_TCL STRIP_THM_THEN)
 655   (fun gth -> FIRST [CONTR_TAC gth; ACCEPT_TAC gth;
 656                      DISCARD_TAC gth; ASSUME_TAC gth]);;
 657
 658 let STRUCT_CASES_THEN ttac = REPEAT_TCL STRIP_THM_THEN ttac;;
 659
 660 let STRUCT_CASES_TAC = STRUCT_CASES_THEN
 661      (fun th -> SUBST1_TAC th ORELSE ASSUME_TAC th);;
 662
 663 let STRIP_GOAL_THEN ttac =  FIRST [GEN_TAC; CONJ_TAC; DISCH_THEN ttac];;
 664
 665 let (STRIP_TAC: tactic) =
 666   fun g ->
 667     try STRIP_GOAL_THEN STRIP_ASSUME_TAC g
 668     with Failure _ -> failwith "STRIP_TAC";;
 669
 670 let (UNDISCH_THEN:term->thm_tactic->tactic) =
 671   fun tm ttac (asl,w) ->
 672     let thp,asl' = remove (fun (_,th) -> aconv (concl th) tm) asl in
 673     ttac (snd thp) (asl',w);;
 674
 675 let FIRST_X_ASSUM ttac =
 676     FIRST_ASSUM(fun th -> UNDISCH_THEN (concl th) ttac);;
 677
 678 (* ------------------------------------------------------------------------- *)
 679 (* Subgoaling and freezing variables (latter is especially useful now).      *)
 680 (* ------------------------------------------------------------------------- *)
 681
 682 let (SUBGOAL_THEN: term -> thm_tactic -> tactic) =
 683   fun wa ttac (asl,w) ->
 684     let meta,gl,just = ttac (ASSUME wa) (asl,w) in
 685     meta,(asl,wa)::gl,fun i l -> PROVE_HYP (hd l) (just i (tl l));;
 686
 687 let SUBGOAL_TAC s tm prfs =
 688   match prfs with
 689    p::ps -> (warn (ps <> []) "SUBGOAL_TAC: additional subproofs ignored";
 690              SUBGOAL_THEN tm (LABEL_TAC s) THENL [p; ALL_TAC])
 691   | [] -> failwith "SUBGOAL_TAC: no subproof given";;
 692
 693 let (FREEZE_THEN :thm_tactical) =
 694   fun ttac th (asl,w) ->
 695     let meta,gl,just = ttac (ASSUME(concl th)) (asl,w) in
 696     meta,gl,fun i l -> PROVE_HYP th (just i l);;
 697
 698 (* ------------------------------------------------------------------------- *)
 699 (* Metavariable tactics.                                                     *)
 700 (* ------------------------------------------------------------------------- *)
 701
 702 let (X_META_EXISTS_TAC: term -> tactic) =
 703   fun t (asl,w) ->
 704     try if not (is_var t) then fail() else
 705         let v,bod = dest_exists w in
 706         ([t],null_inst),[asl,vsubst[t,v] bod],
 707         fun i [th] -> EXISTS (instantiate i w,instantiate i t) th
 708     with Failure _ -> failwith "X_META_EXISTS_TAC";;
 709
 710 let META_EXISTS_TAC ((asl,w) as gl) =
 711   let v = fst(dest_exists w) in
 712   let avoids = itlist (union o frees o concl o snd) asl (frees w) in
 713   let v' = mk_primed_var avoids v in
 714   X_META_EXISTS_TAC v' gl;;
 715
 716 let (META_SPEC_TAC: term -> thm -> tactic) =
 717   fun t thm (asl,w) ->
 718     let sth = SPEC t thm in
 719     ([t],null_inst),[(("",sth)::asl),w],
 720     fun i [th] -> PROVE_HYP (SPEC (instantiate i t) thm) th;;
 721
 722 (* ------------------------------------------------------------------------- *)
 723 (* If all else fails!                                                        *)
 724 (* ------------------------------------------------------------------------- *)
 725
 726 let (CHEAT_TAC:tactic) =
 727   fun (asl,w) -> ACCEPT_TAC(mk_thm([],w)) (asl,w);;
 728
 729 (* ------------------------------------------------------------------------- *)
 730 (* Intended for time-consuming rules; delays evaluation till it sees goal.   *)
 731 (* ------------------------------------------------------------------------- *)
 732
 733 let RECALL_ACCEPT_TAC r a g = ACCEPT_TAC(time r a) g;;
 734
 735 (* ------------------------------------------------------------------------- *)
 736 (* Split off antecedent of antecedent as a subgoal.                          *)
 737 (* ------------------------------------------------------------------------- *)
 738
 739 let ANTS_TAC =
 740   let tm1 = `p /\ (q ==> r)`
 741   and tm2 = `p ==> q` in
 742   let th1,th2 = CONJ_PAIR(ASSUME tm1) in
 743   let th = itlist DISCH [tm1;tm2] (MP th2 (MP(ASSUME tm2) th1)) in
 744   MATCH_MP_TAC th THEN CONJ_TAC;;
 745
 746 (* ------------------------------------------------------------------------- *)
 747 (* A printer for goals etc.                                                  *)
 748 (* ------------------------------------------------------------------------- *)
 749
 750 let (print_goal:goal->unit) =
 751   let string_of_int3 n =
 752     if n < 10 then "  "^string_of_int n
 753     else if n < 100 then " "^string_of_int n
 754     else string_of_int n in
 755   let print_hyp n (s,th) =
 756     open_hbox();
 757     Format.print_string(string_of_int3 n);
 758     Format.print_string " [";
 759     open_hvbox 0;
 760     print_qterm (concl th);
 761     close_box();
 762     Format.print_string "]";
 763     (if not (s = "") then (Format.print_string (" ("^s^")")) else ());
 764     close_box();
 765     Format.print_newline() in
 766   let rec print_hyps n asl =
 767     if asl = [] then () else
 768     (print_hyp n (hd asl);
 769      print_hyps (n + 1) (tl asl)) in
 770   fun (asl,w) ->
 771     Format.print_newline();
 772     if asl <> [] then (print_hyps 0 (rev asl); Format.print_newline()) else ();
 773     print_qterm w; Format.print_newline();;
 774
 775 let (print_goalstack:goalstack->unit) =
 776   let print_goalstate k gs =
 777     let (_,gl,_) = gs in
 778     let n = length gl in
 779     let s = if n = 0 then "No subgoals" else
 780               (string_of_int k)^" subgoal"^(if k > 1 then "s" else "")
 781            ^" ("^(string_of_int n)^" total)" in
 782     Format.print_string s; Format.print_newline();
 783     if gl = [] then () else
 784     do_list (print_goal o C el gl) (rev(0--(k-1))) in
 785   fun l ->
 786     if l = [] then Format.print_string "Empty goalstack"
 787     else if tl l = [] then
 788       let (_,gl,_ as gs) = hd l in
 789       print_goalstate 1 gs
 790     else
 791       let (_,gl,_ as gs) = hd l
 792       and (_,gl0,_) = hd(tl l) in
 793       let p = length gl - length gl0 in
 794       let p' = if p < 1 then 1 else p + 1 in
 795       print_goalstate p' gs;;
 796
 797 (* ------------------------------------------------------------------------- *)
 798 (* Convert a tactic into a refinement on head subgoal in current state.      *)
 799 (* ------------------------------------------------------------------------- *)
 800
 801 let (by:tactic->refinement) =
 802   fun tac ((mvs,inst),gls,just) ->
 803     if gls = [] then failwith "No goal set" else
 804     let g = hd gls
 805     and ogls = tl gls in
 806     let ((newmvs,newinst),subgls,subjust) = tac g in
 807     let n = length subgls in
 808     let mvs' = union newmvs mvs
 809     and inst' = compose_insts inst newinst
 810     and gls' = subgls @ map (inst_goal newinst) ogls in
 811     let just' i ths =
 812       let i' = compose_insts inst' i in
 813       let cths,oths = chop_list n ths in
 814       let sths = (subjust i cths) :: oths in
 815       just i' sths in
 816     (mvs',inst'),gls',just';;
 817
 818 (* ------------------------------------------------------------------------- *)
 819 (* Rotate the goalstate either way.                                          *)
 820 (* ------------------------------------------------------------------------- *)
 821
 822 let (rotate:int->refinement) =
 823   let rotate_p (meta,sgs,just) =
 824     let sgs' = (tl sgs)@[hd sgs] in
 825     let just' i ths =
 826       let ths' = (last ths)::(butlast ths) in
 827       just i ths' in
 828     (meta,sgs',just')
 829   and rotate_n (meta,sgs,just) =
 830     let sgs' = (last sgs)::(butlast sgs) in
 831     let just' i ths =
 832       let ths' = (tl ths)@[hd ths] in
 833       just i ths' in
 834     (meta,sgs',just') in
 835   fun n -> if n > 0 then funpow n rotate_p
 836            else funpow (-n) rotate_n;;
 837
 838 (* ------------------------------------------------------------------------- *)
 839 (* Perform refinement proof, tactic proof etc.                               *)
 840 (* ------------------------------------------------------------------------- *)
 841
 842 let (mk_goalstate:goal->goalstate) =
 843   fun (asl,w) ->
 844     if type_of w = bool_ty then
 845       null_meta,[asl,w],
 846       (fun inst [th] -> INSTANTIATE_ALL inst th)
 847     else failwith "mk_goalstate: Non-boolean goal";;
 848
 849 let (TAC_PROOF : goal * tactic -> thm) =
 850   fun (g,tac) ->
 851     let gstate = mk_goalstate g in
 852     let _,sgs,just = by tac gstate in
 853     if sgs = [] then just null_inst []
 854     else failwith "TAC_PROOF: Unsolved goals";;
 855
 856 let prove(t,tac) =
 857   let th = TAC_PROOF(([],t),tac) in
 858   let t' = concl th in
 859   if t' = t then th else
 860   try EQ_MP (ALPHA t' t) th
 861   with Failure _ -> failwith "prove: justification generated wrong theorem";;
 862
 863 (* ------------------------------------------------------------------------- *)
 864 (* Interactive "subgoal package" stuff.                                      *)
 865 (* ------------------------------------------------------------------------- *)
 866
 867 let current_goalstack = ref ([] :goalstack);;
 868
 869 let (refine:refinement->goalstack) =
 870   fun r ->
 871     let l = !current_goalstack in
 872     if l = [] then failwith "No current goal" else
 873     let h = hd l in
 874     let res = r h :: l in
 875     current_goalstack := res;
 876     !current_goalstack;;
 877
 878 let flush_goalstack() =
 879   let l = !current_goalstack in
 880   current_goalstack := [hd l];;
 881
 882 let e tac = refine(by(VALID tac));;
 883
 884 let r n = refine(rotate n);;
 885
 886 let set_goal(asl,w) =
 887   current_goalstack :=
 888     [mk_goalstate(map (fun t -> "",ASSUME t) asl,w)];
 889   !current_goalstack;;
 890
 891 let g t =
 892   let fvs = sort (<) (map (fst o dest_var) (frees t)) in
 893   (if fvs <> [] then
 894      let errmsg = end_itlist (fun s t -> s^", "^t) fvs in
 895      warn true ("Free variables in goal: "^errmsg)
 896    else ());
 897    set_goal([],t);;
 898
 899 let b() =
 900   let l = !current_goalstack in
 901   if length l = 1 then failwith "Can't back up any more" else
 902   current_goalstack := tl l;
 903   !current_goalstack;;
 904
 905 let p() =
 906   !current_goalstack;;
 907
 908 let top_realgoal() =
 909   let (_,((asl,w)::_),_)::_ = !current_goalstack in
 910   asl,w;;
 911
 912 let top_goal() =
 913   let asl,w = top_realgoal() in
 914   map (concl o snd) asl,w;;
 915
 916 let top_thm() =
 917   let (_,[],f)::_ = !current_goalstack in
 918   f null_inst [];;
 919
 920 (* ------------------------------------------------------------------------- *)
 921 (* Install the goal-related printers.                                        *)
 922 (* ------------------------------------------------------------------------- *)
 923
 924 #install_printer print_goal;;
 925 #install_printer print_goalstack;;