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