1(* ===================================================================== *) 2(* VERSION : 7.0 *) 3(* FILE : tactics.sml *) 4(* DESCRIPTION : General purpose tactics for obj library. *) 5(* *) 6(* AUTHOR : Peter Vincent Homeier *) 7(* DATE : October 19, 2000 *) 8(* COPYRIGHT : Copyright (c) 2000 by Peter Vincent Homeier *) 9(* *) 10(* ===================================================================== *) 11 12(* --------------------------------------------------------------------- *) 13(* This file contains new tactics of general usefulness. *) 14(* --------------------------------------------------------------------- *) 15 16structure tactics :> tactics = 17struct 18 19 20open HolKernel Parse boolLib; 21 22(* --------------------------------------------------------------------- *) 23(* Need conditional rewriting. *) 24(* --------------------------------------------------------------------- *) 25open dep_rewrite; 26open listTheory; 27open PairedLambda; 28 29 30(* --------------------------------------------------------------------- *) 31(* Load the Hol 98 specific customization. *) 32(* --------------------------------------------------------------------- *) 33(* 34open hol98specific; 35 36See what is needed from the following: 37 38open listTheory; 39open Let_conv; 40open Num_induct; 41 42fun close_theory () = (); 43 44val define_type = Define_type.define_type; 45 46val stdIn = TextIO.stdIn; 47val stdOut = TextIO.stdOut; 48val input_line = TextIO.input; 49val output = TextIO.output; 50val openIn = TextIO.openIn; 51(* val openString = TextIO.openString; CURRENTLY UNSUPPORTED *) 52 53val print_term = Hol_pp.print_term; 54val print_type = Hol_pp.print_type; 55 56fun print_string s = TextIO.output(TextIO.stdOut,s); 57 58val list_to_vector = Vector.fromList; 59 60val list_to_array = Array.fromList; 61 62fun ordof (s,n) = Char.ord(String.sub(s,n)); 63 64fun time f = 65 let val cputimer = Timer.startCPUTimer () 66 in 67 let val res = f () 68 val {usr,sys,gc} = Timer.checkCPUTimer cputimer 69 in 70 print_string "\n"; 71 print_string ("CPU: usr: " ^ Time.toString usr ^ " s "); 72 print_string ( "sys: " ^ Time.toString sys ^ " s "); 73 print_string ( "gc: " ^ Time.toString gc ^ " s\n"); 74 res 75 end 76 end; 77 78val now = Time.now; 79 80val time_to_string = Time.toString; 81 82val sub_time = Time.-; 83 84val system = fn (s:string) => (); 85 86*) 87 88 89fun print_newline() = print "\n"; 90fun print_theorem th = (print (thm_to_string th); print_newline()); 91fun print_terms [] = () 92 | print_terms (t :: []) = print_term t 93 | print_terms (t :: ts) = (print_term t; print ","; print_terms ts); 94fun print_all_thm th = 95 let val (ant,conseq) = dest_thm th 96 in (print "["; print_terms ant; print "] |- "; 97 print_term conseq; print_newline() ) 98 end; 99fun print_theorems [] = () 100 | print_theorems (t :: ts) = (print_theorem t; print "\n"; 101 print_theorems ts); 102fun print_goal (asl,gl) = (print_term gl; print_newline()); 103 104fun print_theory_size () = 105 (print "The theory "; 106 print (current_theory ()); 107 print " has "; 108 print (Int.toString (length (types (current_theory ())))); 109 print " types, "; 110 print (Int.toString (length (axioms "-"))); 111 print " axioms, "; 112 print (Int.toString (length (definitions "-"))); 113 print " definitions, and "; 114 print (Int.toString (length (theorems "-"))); 115 print " theorems."; 116 print "\n" ); 117 118fun pthm th = 119 ( print_thm th; 120 print_newline(); 121 th ); 122 123fun pairf f g (x,y) = (f x,g y); 124fun test f x = ( f x; x ); 125fun try f x = f x handle _ => x; 126 127(* must somehow overload the substitution operator '<|': 128map new_special_symbol [`<|s`;`<|v`;`<|vs`;`<|a`; 129 `<|xs`;`<|e`;`<|es`;`<|b`;`<|c`;`<|env`;`<|g`; 130 `<|vv`;`<|vsv`;`<|av`;`:==`;`//v`;`<<`]; (); 131 132Expect to do this by using alphabetic versions, as 133 subst_s, subst_v, etc. 134*) 135 136 137(* We will need the tools for definitions in the following structure: *) 138(* 139open new_type; 140*) 141 142 143(* --------------------------------------------------------------------- *) 144(* Need the HOL 88 compatibility library. *) 145(* --------------------------------------------------------------------- *) 146open hol88Lib; 147open listLib; 148open Psyntax; 149 150 151 152val ONE_ONE_DEF = boolTheory.ONE_ONE_DEF; 153val ONTO_DEF = boolTheory.ONTO_DEF; 154 155(* These operators transform implications to collect antecedents into 156 a single conjunction, or else to reverse this and spread them into 157 a sequence of individual implications. Each has type thm->thm. 158*) 159 160val AND2IMP = REWRITE_RULE[(SYM o SPEC_ALL)AND_IMP_INTRO]; 161val IMP2AND = REWRITE_RULE[AND_IMP_INTRO]; 162 163fun TACTIC_ERR{function,message} = 164 Feedback.HOL_ERR{origin_structure = "Tactic", 165 origin_function = function, 166 message = message}; 167 168fun failwith function = 169 raise TACTIC_ERR{function = function,message = ""}; 170 171fun fail () = failwith "fail"; 172 173 174(* Here are some useful tactics, that are not included in the standard HOL: *) 175 176val PRINT_TAC :tactic = fn (asl,gl) => 177 (print_goal (asl,gl); 178 ALL_TAC (asl,gl)); 179 180val POP_TAC = POP_ASSUM (fn th => ALL_TAC); 181 182fun ETA_TAC v :tactic = fn (asl,gl) => 183 let val (t1,t2) = dest_eq gl; 184 val at1 = ���\^v.^t1 ^v���; 185 val at2 = ���\^v.^t2 ^v��� in 186 ([(asl,mk_eq(at1,at2))], 187 fn [thm] => TRANS (SYM(ETA_CONV at1)) (TRANS thm (ETA_CONV at2))) 188 end; 189 190fun EXT_TAC v :tactic = fn (asl,gl) => 191 let val (t1,t2) = dest_eq gl; 192 val at1 = mk_comb(t1,v) 193 and at2 = mk_comb(t2,v) in 194 ([(asl,mk_forall(v,mk_eq(at1,at2)))], 195 fn [thm] => EXT thm) 196 end; 197 198val CHECK_TAC :tactic = fn (asl,gl) => 199 if exists (aconv gl) asl 200 then ACCEPT_TAC (ASSUME gl) (asl,gl) 201 else failwith "CHECK_TAC"; 202 203val FALSE_TAC :tactic = fn (asl,gl) => 204 if exists (fn th => th = ���F���) asl 205 then CONTR_TAC (ASSUME ���F���) (asl,gl) 206 else failwith "FALSE_TAC"; 207 208fun MP_IMP_TAC imp_th :tactic = fn (asl,gl) => 209 let val (ant,cns) = dest_imp(concl imp_th) in 210 ([(asl,ant)], 211 fn [thm] => MP imp_th thm) 212 end; 213 214fun UNASSUME_THEN (ttac:thm_tactic) tm :tactic = fn (asl,t) => 215 if mem tm asl 216 then ttac (ASSUME tm) (subtract asl [tm], t) 217 else failwith "UNASSUME_TAC"; 218 219val CONTRAPOS_TAC :tactic = fn (asl,gl) => 220 let val (ant,cns) = dest_imp gl in 221 ([(asl,mk_imp (dest_neg cns, dest_neg ant))], 222 fn [thm] => CONTRAPOS thm) 223 end; 224 225val FORALL_EQ_TAC :tactic = fn (asl,gl) => 226 (let val (allt1,allt2) = dest_eq gl; 227 val (x,t1) = dest_forall allt1 228 and (y,t2) = dest_forall allt2 in 229 if not (x = y) then fail() 230 else 231 ([(asl,mk_eq (t1, t2))], 232 fn [thm] => FORALL_EQ x thm) 233 end) 234 handle _ => failwith "FORALL_EQ_TAC"; 235 236val EXISTS_EQ_TAC :tactic = fn (asl,gl) => 237 (let val (ext1,ext2) = dest_eq gl; 238 val (x,t1) = dest_exists ext1 239 and (y,t2) = dest_exists ext2 in 240 if not (x = y) then fail() 241 else 242 ([(asl,mk_eq (t1, t2))], 243 fn [thm] => EXISTS_EQ x thm) 244 end) 245 handle _ => failwith "EXISTS_EQ_TAC"; 246 247fun EXISTS_VAR (x,u) th = 248 let val p = subst[(x,u)] (concl th) in 249 EXISTS (mk_exists(x,p),u) th 250 end; 251 252val FIND_EXISTS_TAC :tactic = fn (asl,gl) => 253 let val (vars,body) = strip_exists gl 254 val v = hd vars 255 val cnjs = strip_conj body 256 fun find_exists_eq [] = failwith "find_exists_eq" 257 | find_exists_eq (cnj::cnjs) = 258 let val (lhs,rhs) = dest_eq cnj 259 in 260 if lhs = v then rhs 261 else if rhs = v then lhs 262 else failwith "find_exists_eq" 263 end 264 handle _ => find_exists_eq cnjs 265 in 266 EXISTS_TAC (find_exists_eq cnjs) (asl,gl) 267 end 268 handle _ => failwith "FIND_EXISTS_TAC"; 269 270 271(* introducing a beta abstration 272 273 A |- t 274 ======================== 275 A |- (\x.t)x 276*) 277 278(* [PVH 95.2.19] *) 279 280fun UNBETA_TAC x :tactic = fn (asl,gl) => 281 ([(asl,mk_comb(mk_abs(x, gl), x))], 282 fn [thm] => BETA_RULE thm) 283 handle _ => failwith "UNBETA_TAC"; 284 285(* 286g `x < y`; 287e(UNBETA_TAC ���x:num���); 288e(UNBETA_TAC ���y:num���); 289*) 290(* 291val WELL_FOUNDED_NUM_TAC :tactic = fn (asl,gl) => 292 (let val n = (fst o dest_forall) gl in 293 (GEN_TAC 294 THEN UNBETA_TAC n 295 THEN SPEC_TAC(n,n) 296 THEN MATCH_MP_TAC NUM_WELL_FOUNDED 297 THEN BETA_TAC 298 THEN GEN_TAC 299 THEN DISCH_TAC) end) (asl,gl) 300 handle _ => failwith "WELL_FOUNDED_NUM_TAC"; 301*) 302 303(* 304% ! implication abstraction 305 306 A |- t1 ==> t2 307 ----------------------- 308 A |- (!x.t1) ==> (!x.t2) 309% 310 311% Adapted from FORALL_EQ: [PVH 94.12.05] % 312 313let FORALL_IMP = 314 fn x => let all t = mk_forall(x,t) in 315 fn th => let (t1,t2) = dest_imp (concl th) in % t1 ==> t2 % 316 let at1 = all t1 in 317 DISCH at1 (GEN x 318 (MATCH_MP (GEN x th) (SPEC x (ASSUME at1)))) 319 handle _ => failwith "FORALL_IMP"; 320 321% 322FORALL_IMP = - : (term -> thm -> thm) 323FORALL_IMP ���n:num��� (SPEC_ALL SUB_ADD); 324FORALL_IMP ���n:num��� (SPEC_ALL (ASSUME ���!n:num. R n ==> Q n���)); 325% 326 327let FORALL_IMP_TAC :tactic = fn (asl,gl) => 328 (let allt1,allt2 = dest_imp gl in 329 let x,t1 = dest_forall allt1 in 330 let y,t2 = dest_forall allt2 in 331 if not (x = y) then fail() 332 else 333 [asl,mk_imp (t1, t2)], 334 fn [thm] => FORALL_IMP x thm) 335 handle _ => failwith "FORALL_IMP_TAC"; 336*) 337 338val rec UNDISCH_ALL_TAC :tactic = fn (asl,gl) => 339 if asl = [] then ALL_TAC (asl,gl) 340 else (UNDISCH_TAC (hd asl) 341 THEN UNDISCH_ALL_TAC) (asl,gl); 342 343val UNDISCH_LAST_TAC :tactic = 344 POP_ASSUM MP_TAC; 345 346fun DEFINE_NEW_VAR def :tactic = 347 let val (v,tm) = dest_eq def in 348 SUBGOAL_THEN (mk_exists(v,def)) STRIP_ASSUME_TAC 349 THENL 350 [ EXISTS_TAC tm 351 THEN REWRITE_TAC[], 352 ALL_TAC 353 ] 354 end 355 handle _ => failwith "DEFINE_NEW_VAR"; 356 357 358val LIST_INDUCT_TAC = 359 let val tm = Term `!P:'a list -> bool. 360 P [] /\ (!t. P t ==> !x. P (x::t)) ==> !l. P l` 361 val eq = ALPHA (concl listTheory.list_induction) tm 362 val list_induction' = EQ_MP eq listTheory.list_induction 363 in INDUCT_THEN list_induction' ASSUME_TAC 364 end; 365 366 367val DOUBLE_LIST_INDUCT_TAC :tactic = 368 LIST_INDUCT_TAC 369 THENL 370 [ ALL_TAC, 371 GEN_TAC THEN LIST_INDUCT_TAC THEN POP_TAC 372 ]; 373 374val LENGTH_LIST_INDUCT_TAC :tactic = 375 LIST_INDUCT_TAC 376 THEN REWRITE_TAC[LENGTH,LENGTH_NIL,LENGTH_CONS] 377 THEN REPEAT GEN_TAC THEN STRIP_TAC 378 THEN POP_ASSUM (fn th => REWRITE_TAC[th]); 379 380 381val FORALL_SYM_CONV :conv = fn tm1 => 382 let val (x,body1) = dest_forall tm1; 383 val (y,body) = dest_forall body1; 384 val tm2 = mk_forall(y,mk_forall(x,body)) in 385 IMP_ANTISYM_RULE ((DISCH_ALL o GENL[y,x] o SPECL[x,y] o ASSUME) tm1) 386 ((DISCH_ALL o GENL[x,y] o SPECL[y,x] o ASSUME) tm2) 387 end 388 handle _ => failwith "FORALL_SYM_CONV"; 389 390(* 391FORALL_SYM_CONV ���!x y. x+y=z���; 392*) 393 394 395fun NOT_AP_TERM_TAC f :tactic = fn (asl,gl) => 396 let val eq_gl = dest_neg gl; 397 val (a,b) = dest_eq eq_gl in 398 ([(asl,mk_neg(mk_eq(mk_comb(f,a),mk_comb(f,b))))], 399 fn [thm] => MP (CONTRAPOS (DISCH eq_gl (AP_TERM f (ASSUME eq_gl)))) thm) 400 end 401 handle _ => failwith "NOT_AP_TERM_TAC"; 402 403val APP_let_CONV :conv = fn tm1 => 404 let val (f,args) = strip_comb tm1; 405 val lt::rest = args; 406 val (bodyf,vl) = dest_let lt; 407 val (var,body) = dest_abs bodyf; 408 val tm2 = mk_let((mk_abs(var,(list_mk_comb(f,(body::rest))))),vl) 409 in 410 TRANS ((ONCE_DEPTH_CONV let_CONV) tm1) 411 (SYM ((ONCE_DEPTH_CONV let_CONV) tm2)) 412 end 413 handle _ => failwith "APP_LET_CONV"; 414 415val LIFT_let_TAC = (REPEAT o CONV_TAC o CHANGED_CONV o ONCE_DEPTH_CONV) 416 APP_let_CONV; 417 418val STRIP_let_TAC :tactic = fn (asl,gl) => 419 let val (bodyf,vl) = dest_let gl; 420 val (var,body) = dest_abs bodyf; 421 val let_equal = mk_eq(var,vl) in 422 ([(let_equal::asl,body)], 423 fn [thm] => (pthm (SYM (let_CONV gl)); pthm thm; 424 map (pthm o ASSUME) (hyp thm); 425 (pthm o pthm) (EQ_MP (SYM (let_CONV gl)) 426 (DISCH let_equal thm)))) 427 end 428 handle _ => failwith "STRIP_let_TAC"; 429 430fun USE_IMP_EQ_matches th = 431 let val (vars,imps) = strip_forall(concl th); 432 val (hyps,body) = strip_imp imps; 433 val left = fst(dest_eq body) in 434 fn tm => match left tm 435 end 436 handle _ => failwith "USE_IMP_EQ_matches"; 437 438fun USE_IMP_matches th = 439 let val (vars,imps) = strip_forall(concl th); 440 val (hyps,body) = strip_imp imps in 441 fn tm => match body tm 442 end 443 handle _ => failwith "USE_IMP_matches"; 444 445fun SUB_matches (f:term->'a) tm = 446 if is_comb tm then 447 (let val (rator,rand) = dest_comb tm in 448 (f rator handle _ => f rand) 449 end) 450 else 451 if is_abs tm then 452 (let val (bv,body) = dest_abs tm in 453 f body 454 end) 455 else (failwith "SUB_matches"); 456 457fun ONCE_DEPTH_matches (f:term->'a) tm = 458 (f tm handle _ => ((SUB_matches (ONCE_DEPTH_matches f)) tm)); 459 460fun ONCE_DEPTH_USE_IMP_EQ_matches th = 461 ONCE_DEPTH_matches (USE_IMP_EQ_matches th); 462 463fun ONCE_DEPTH_USE_IMP_matches th = 464 ONCE_DEPTH_matches (USE_IMP_matches th); 465 466fun USE_IMP_THEN ttac th :tactic = fn (asl,gl) => 467 let val matches = ONCE_DEPTH_USE_IMP_EQ_matches th gl; 468 val ith = INST_TY_TERM matches (SPEC_ALL th); 469 val subgoal = concl (UNDISCH_ALL ith) in 470 (SUBGOAL_THEN subgoal ttac 471 THEN (MATCH_MP_TAC th ORELSE ALL_TAC)) (asl,gl) 472 end 473 handle _ => failwith "USE_IMP_THEN"; 474 475fun USE_IMP_TAC th :tactic = USE_IMP_THEN ASSUME_TAC th; 476 477fun USE_IMP_AND_THEN ttac th tac :tactic = 478 USE_IMP_THEN ttac th 479 THENL [ tac, ALL_TAC ]; 480 481fun USE_THEN ttac th :tactic = fn (asl,gl) => 482 let val matches = ONCE_DEPTH_USE_IMP_matches th gl; 483 val ith = INST_TY_TERM matches (SPEC_ALL th); 484 val subgoal = concl (UNDISCH_ALL ith) in 485 (SUBGOAL_THEN subgoal ttac 486 THEN (MATCH_MP_TAC th ORELSE ALL_TAC)) (asl,gl) 487 end 488 handle _ => failwith "USE_THEN"; 489 490fun USE_TAC th :tactic = USE_THEN ASSUME_TAC th; 491 492fun USE_AND_THEN ttac th tac :tactic = 493 USE_THEN ttac th 494 THENL [ tac, ALL_TAC ]; 495 496fun RES2_THEN thm_tac = 497 RES_THEN (fn th => IMP_RES_THEN thm_tac th ORELSE ALL_TAC); 498 499fun IMP_RES2_THEN thm_tac = 500 IMP_RES_THEN (fn th => IMP_RES_THEN thm_tac th ORELSE ALL_TAC); 501 502fun IMP_RES_M_THEN tac th g = 503 IMP_RES_THEN (REPEAT_GTCL IMP_RES_THEN tac) th g handle _ => ALL_TAC g; 504 505fun RES_M_THEN tac g = 506 RES_THEN (REPEAT_GTCL IMP_RES_THEN tac) g handle _ => ALL_TAC g; 507 508val REWRITE_THM = fn th => REWRITE_TAC[th]; 509val ASM_REWRITE_THM = fn th => ASM_REWRITE_TAC[th]; 510val ONCE_REWRITE_THM = fn th => ONCE_REWRITE_TAC[th]; 511val IMP_RES_REWRITE_TAC = IMP_RES_THEN REWRITE_THM; 512val RES_REWRITE_TAC = RES_THEN REWRITE_THM; 513 514fun REWRITE_ASSUM_TAC rths :tactic = 515 RULE_ASSUM_TAC (REWRITE_RULE rths); 516 517fun REWRITE_ALL_TAC rths :tactic = 518 REWRITE_TAC rths THEN 519 REWRITE_ASSUM_TAC rths; 520 521fun ASM_REWRITE_ALL_TAC rths :tactic = 522 REWRITE_ASSUM_TAC rths THEN 523 ASM_REWRITE_TAC rths; 524 525fun ONCE_REWRITE_ASSUM_TAC rths :tactic = 526 RULE_ASSUM_TAC (ONCE_REWRITE_RULE rths); 527 528fun ONCE_REWRITE_ALL_TAC rths :tactic = 529 ONCE_REWRITE_TAC rths THEN 530 ONCE_REWRITE_ASSUM_TAC rths; 531 532fun ONCE_ASM_REWRITE_ALL_TAC rths :tactic = 533 ONCE_REWRITE_ASSUM_TAC rths THEN 534 ONCE_ASM_REWRITE_TAC rths; 535 536val REWRITE_ALL_THM = fn th => REWRITE_ALL_TAC[th]; 537val ASM_REWRITE_ALL_THM = fn th => ASM_REWRITE_ALL_TAC[th]; 538val ONCE_REWRITE_ALL_THM = fn th => ONCE_REWRITE_ALL_TAC[th]; 539val ONCE_ASM_REWRITE_ALL_THM = fn th => ONCE_ASM_REWRITE_ALL_TAC[th]; 540 541 542val UNIFY_VARS_TAC :tactic = 543 ASSUM_LIST (fn thms => MAP_EVERY (fn th => REWRITE_ALL_TAC[th]) 544 (mapfilter (SYM o (test ((pairf dest_var dest_var) 545 o dest_eq o concl))) thms)); 546 547 548fun EVERY1 tacl = 549 case tacl 550 of [] => 551 ALL_TAC 552 | (t::tacl') => 553 t THEN1 EVERY1 tacl'; 554 555end; (* struct *) 556