1(* =====================================================================*) 2(* FILE : elsaUtils (formerly utilsLib.sml and before that, *) 3(* functions.sml and before that, start_groups.ml) *) 4(* DESCRIPTION : defines a collection of general purpose functions, *) 5(* rules, and tactics which are used throughout the *) 6(* group library entry and the integer library entry. *) 7(* *) 8(* AUTHOR : Elsa Gunter, Bell Labs *) 9(* DATE : 89.3.20 *) 10(* TRANSLATOR : Elsa Gunter, *) 11(* TRANSLATED : 91.22.12 *) 12(* =====================================================================*) 13 14(* Copyright 1991 by AT&T Bell Laboratories *) 15(* Share and Enjoy *) 16 17structure elsaUtils :> elsaUtils = 18struct 19 20open HolKernel Parse Drule Tactical Tactic Conv; 21 22infix THENL THEN ORELSE; 23 24 25type hol_type = Type.hol_type; 26type term = Term.term 27type thm = Thm.thm 28type tactic = Abbrev.tactic 29type conv = Abbrev.conv 30type thm_tactic = Abbrev.thm_tactic; 31 32 33fun UTILSLIB_ERR{function,message} = 34 HOL_ERR{origin_structure = "elsaUtils", 35 origin_function = function, 36 message = message}; 37 38(* Some general-purpose functions *) 39 40fun is_contained_in {subset, superset} = 41 itlist 42 (fn x => fn y => x andalso y) 43 (map (fn x => exists (fn y => (aconv x y)) superset) subset) 44 true 45 46(* find_match was in the original system *) 47 48(* try to match PATTERN against a subterm of TERM, return the term 49 & hol_type substitutions that make PATTERN match the subterm *) 50 51fun find_match {pattern, term} = 52 let 53 fun find_match_aux term = 54 match_term pattern term 55 handle HOL_ERR _ => 56 find_match_aux (#Body(dest_abs term)) 57 handle HOL_ERR _ => 58 find_match_aux (rator term) 59 handle HOL_ERR _ => 60 find_match_aux (rand term) 61 handle HOL_ERR _ => 62 raise UTILSLIB_ERR 63 {function = "find_match", 64 message = "no match"} 65 in 66 find_match_aux term 67 end 68 69(* 70 mapshape applies the functions in functions to argument lists obtained by 71 splitting the list unionlist into sublists of lengths given by partition. 72*) 73 74fun mapshape {partition = [],functions = [], unionlist = []} = [] 75 | mapshape {partition = (n1::rem_lengths), 76 functions = (f::rem_funs), 77 unionlist} = 78 let 79 val (first_list,rem_lists) = split_after n1 unionlist 80 in 81 (f first_list) :: 82 (mapshape 83 {partition = rem_lengths, 84 functions = rem_funs, 85 unionlist = rem_lists}) 86 end 87 | mapshape _ = raise UTILSLIB_ERR{function = "mapshape", 88 message = "bad fit"} 89 90 91 92(* 93 The following are derived proof rules and tactics which I found useful 94 in developing group theory and the integers. 95*) 96 97(* Proof Rules *) 98 99 100(* 101 STRONG_INST, STRONG_INST_TY_TERM and STRONG_INST are like INST, INST_TY_TERM 102 and INST, except that they instantiate free variables in the hypotheses, 103 rather than failing. I have also changed the type of their arguments to 104 use records to state more explictly which piece of the substitution 105 information is the variable bieng substituted for and which piece is the 106 expression being substituted. 107*) 108 109local 110 fun COUNT_UNDISCH 0 thm = thm 111 | COUNT_UNDISCH n thm = COUNT_UNDISCH (n -1) (UNDISCH thm) 112 fun split_subst [] = ([], []) 113 | split_subst ({redex, residue}::rest) = 114 let val (vals, vars) = split_subst rest 115 in 116 (residue::vals, redex::vars) 117 end 118in 119 fun STRONG_INST_TYPE {type_substitution, theorem} = 120 COUNT_UNDISCH 121 (length (hyp theorem)) 122 (INST_TYPE type_substitution (DISCH_ALL theorem)) 123 124 fun STRONG_INST_TY_TERM {type_substitution, term_substitution, theorem} = 125 let 126 val inst_ty_thm = INST_TYPE type_substitution (DISCH_ALL theorem) 127 val (values,variables) = split_subst term_substitution 128 in 129 COUNT_UNDISCH 130 (length (hyp theorem)) 131 (SPECL values (GENL variables inst_ty_thm)) 132 end 133 134 fun STRONG_INST {term_substitution, theorem} = 135 let 136 val (values,variables) = split_subst term_substitution 137 in 138 COUNT_UNDISCH 139 (length (hyp theorem)) 140 (SPECL values (GENL variables (DISCH_ALL theorem))) 141 end 142end 143 144 145(* 146 AUTO_SPEC : {specialization_term:term, generalized_theorem:thm} -> thm 147 148 (specialization_term = t) 149 (Automatically tries to instantiate the type of x to that of t, applying 150 the type substitution to the hypotheses as needed.) 151 152 A |- !x.u 153 ------------------ 154 A |- u[t/x] 155*) 156 157fun AUTO_SPEC {specialization_term, generalized_theorem} = 158 let 159 val type_substitution = 160 match_type 161 (type_of(#Bvar(dest_forall(concl generalized_theorem)))) 162 (type_of specialization_term) 163 in 164 SPEC 165 specialization_term 166 (STRONG_INST_TYPE 167 {type_substitution = type_substitution, 168 theorem = generalized_theorem}) 169 end 170 171 172(* 173 AUTO_SPECL : {specialization_list:term list, 174 generalized_theorem:thm} -> thm 175 176 (specialization_list = [t1;...;tn]) 177 178 A |- !x1 ... xn. t(x1,...,xn) 179 ----------------------------------- 180 A |- t(t1,...,tn) 181 182*) 183 184fun AUTO_SPECL {specialization_list, generalized_theorem} = 185 rev_itlist 186 (fn specialization_term => fn gen_thm => 187 AUTO_SPEC {specialization_term = specialization_term, 188 generalized_theorem = gen_thm}) 189 specialization_list 190 generalized_theorem 191 192(* Are these needed? 193(* 194 EQF_INTRO : thm -> thm 195 196 A |- ~t 197 ------------ 198 A |- t = F 199*) 200 201fun EQF_INTRO neg_thm = 202 EQ_MP 203 (SYM(CONJUNCT2(CONJUNCT2(CONJUNCT2(SPEC 204 (dest_neg(concl neg_thm)) 205 EQ_CLAUSES))))) 206 neg_thm 207 208 209(* 210 FALSITY_INTRO : {theorem:thm, negated_theorem:thm} -> thm 211 212 A1 |- t A2 |- ~t 213 -------------------- 214 A1 u A2 |- F 215 216*) 217 218local 219 val neg_type = (==`:bool -> bool`==) 220in 221 fun FALSITY_INTRO {theorem, negated_theorem} = 222 let 223 val neg_var = 224 variant 225 (all_varsl ((concl negated_theorem)::(hyp negated_theorem))) 226 (mk_var {Name="neg", Ty=neg_type}) 227 in 228 if aconv (concl negated_theorem) (mk_neg (concl theorem)) 229 then 230 MP 231 (BETA_RULE 232 (SUBST[{thm=NOT_DEF, var=neg_var}] 233 (mk_comb {Rator=neg_var, Rand=(concl theorem)}) 234 negated_theorem)) 235 theorem 236 else raise UTILSLIB_ERR 237 {function = "FALSITY_INTRO", 238 message = "negated_theorem is not the "^ 239 "negation of theorem"} 240 end 241end 242 243fun NORMALIZE rewrite_list thm = REWRITE_RULE rewrite_list (BETA_RULE thm) 244*) 245 246(* This should be recordized!! *) 247 248fun MATCH_TERM_SUBS_RULE thm tm = 249 let 250 val strip_thm = hd (IMP_CANON thm) 251 val (term_substitution,type_substitution)= 252 match_term (lhs(concl strip_thm)) tm 253 in 254 SUBS 255 [(STRONG_INST_TY_TERM 256 {term_substitution=term_substitution, 257 type_substitution=type_substitution, 258 theorem = strip_thm})] 259 end 260 261 262(* Tactics *) 263 264(* 265 SUPPOSE_TAC : term -> tactic (term = t) 266 267 [A] t1 268 ======================= 269 [A,t] t1 [A] t 270*) 271 272local 273 val bool = (==`:bool`==) 274in 275 fun SUPPOSE_TAC new_claim current_goal = 276 if type_of new_claim = bool 277 then 278 ([(new_claim::(fst current_goal),snd current_goal), 279 (fst current_goal, new_claim)], 280 fn [goalthm,claimthm] => 281 MP (DISCH new_claim goalthm) claimthm 282 | _ => raise UTILSLIB_ERR 283 {function = "SUPPOSE_TAC", 284 message = "invalid application"}) 285 else raise UTILSLIB_ERR 286 {function = "SUPPOSE_TAC", 287 message = "The claim doesn't have type :bool"} 288end 289 290 291(* 292 REV_SUPPOSE_TAC : term -> tactic (term = t) 293 294 [A] t1 295 ======================= 296 [A] t [A,t] t1 297*) 298 299local 300 val bool = (==`:bool`==) 301in 302 fun REV_SUPPOSE_TAC new_claim current_goal = 303 if type_of new_claim = bool 304 then 305 ([(fst current_goal, new_claim), 306 (new_claim::(fst current_goal),snd current_goal)], 307 fn [claimthm,goalthm] => 308 MP (DISCH new_claim goalthm) claimthm 309 | _ => raise UTILSLIB_ERR 310 {function = "REV_SUPPOSE_TAC", 311 message = "invalid application"}) 312 else raise UTILSLIB_ERR 313 {function = "REV_SUPPOSE_TAC", 314 message = "The claim doesn't have type :bool"} 315end 316 317 318(* 319 ADD_ASSUMS_THEN : {new_assumptions:term list, tactic:tactic} -> tactic 320 321 For adding assumptions to the goal to be used by the given tactic. 322 Returns the result of applying the tactic to the augmented goal, 323 together with a new subgoal for each new assumption added. 324*) 325 326fun ADD_ASSUMS_THEN {new_assumptions = [], tactic} (asms,goal) = 327 tactic (asms,goal) 328 | ADD_ASSUMS_THEN {new_assumptions = (claim::rest), tactic} (asms,goal) = 329 if exists (aconv claim) asms 330 then ADD_ASSUMS_THEN 331 {new_assumptions = rest, 332 tactic = tactic} 333 (asms,goal) 334 else (SUPPOSE_TAC claim THENL 335 [(ADD_ASSUMS_THEN {new_assumptions = rest, tactic = tactic}), 336 ALL_TAC]) 337 (asms,goal) 338 339(* 340 ADD_STRIP_ASSUMS_THEN : {new_assumptions:term list, tactic:tactic} -> tactic 341 342 Like ADD_ASSUMS_THEN except it strips the new assumptions before 343 adding them to the assumptions. 344*) 345 346fun ADD_STRIP_ASSUMS_THEN {new_assumptions = [], tactic} (asms,goal) = 347 tactic (asms,goal) 348 | ADD_STRIP_ASSUMS_THEN {new_assumptions = (claim::rest), tactic} 349 (asms,goal) = 350 if exists (aconv claim) asms 351 then ADD_STRIP_ASSUMS_THEN 352 {new_assumptions = rest, 353 tactic = tactic} 354 (asms,goal) 355 else (SUPPOSE_TAC claim THENL 356 [((POP_ASSUM STRIP_ASSUME_TAC) THEN 357 (ADD_STRIP_ASSUMS_THEN {new_assumptions=rest,tactic=tactic})), 358 ALL_TAC]) 359 (asms,goal) 360 361(* 362 use_thm : {theorem:thm, thm_tactic:(thm -> tactic)} -> tactic 363 364 For adding the hypotheses of a theorem to the assumptions of a goal 365 before applying the tactic resulting from applying thm_tactic to 366 the given theorem. 367*) 368 369fun use_thm {theorem, thm_tactic} = 370 ADD_STRIP_ASSUMS_THEN{new_assumptions = hyp theorem, 371 tactic = thm_tactic theorem} 372 373 374fun NEW_SUBST1_TAC thm = use_thm {theorem = thm, thm_tactic = SUBST1_TAC} 375 376 377fun SUBST_MATCH_TAC thm (asms,goal) = 378 let 379 val strip_thm = hd (IMP_CANON thm) 380 val (term_substitution,type_substitution)= 381 find_match {pattern = (lhs(concl strip_thm)), term = goal} 382 val subst_thm = STRONG_INST_TY_TERM 383 {term_substitution=term_substitution, 384 type_substitution=type_substitution, 385 theorem = strip_thm} 386 in 387 NEW_SUBST1_TAC subst_thm (asms,goal) 388 end 389 390 391 392fun ASSUME_LIST_TAC thms (asms,goal) = 393 let 394 val new_assums = flatten (map hyp thms) 395 val tactic = 396 itlist 397 (fn thm => fn tac => 398 if exists (aconv (concl thm)) asms orelse 399 exists (aconv (concl thm)) new_assums 400 then ALL_TAC 401 else (ASSUME_TAC thm) THEN tac) 402 thms 403 ALL_TAC 404 in 405 ADD_ASSUMS_THEN 406 {new_assumptions=new_assums, 407 tactic = tactic} 408 (asms,goal) 409 end 410 411 412 413(* 414 ASM_CONJ1_TAC : tactic 415 416 [A] T1 /\ T2 417 ====================== 418 [A] T1 [A;T1] T2 419*) 420 421fun ASM_CONJ1_TAC (asms,goal) = 422 if is_conj goal 423 then 424 (REV_SUPPOSE_TAC (rand(rator goal)) THENL 425 [ALL_TAC, 426 CONJ_TAC THENL 427 [ACCEPT_TAC(ASSUME (rand(rator goal))), 428 ALL_TAC]]) 429 (asms,goal) 430 else raise UTILSLIB_ERR 431 {function = "ASM_CONJ1_TAC", 432 message = "goal not a conjuct"} 433 434 435(* 436 ASM_CONJ2_TAC : tactic 437 438 [A] T1 /\ T2 439 ====================== 440 [A;T2] T1 [A] T2 441*) 442 443fun ASM_CONJ2_TAC (asms,goal) = 444 if is_conj goal 445 then 446 (SUPPOSE_TAC (rand goal) THENL 447 [CONJ_TAC THENL 448 [ALL_TAC, 449 ACCEPT_TAC(ASSUME (rand goal))], 450 ALL_TAC]) 451 (asms,goal) 452 else raise UTILSLIB_ERR 453 {function = "ASM_CONJ2_TAC", 454 message = "goal not a conjuct"} 455 456 457(* 458 MP_IMP_TAC : thm -> tactic ( thm = [A1] |- t2 ==> t1 ) 459 460 [A] t1 461 ========== 462 [A] t2 463*) 464 465fun MP_IMP_TAC imp_thm (thisgoal as (asms,goal)) = 466 if is_imp (concl imp_thm) 467 then 468 if aconv (#conseq (dest_imp (concl imp_thm))) goal 469 then 470 use_thm 471 {theorem = imp_thm, 472 thm_tactic = 473 fn imp_thm => fn (asms,goal) => 474 ([(asms,#ant(dest_imp(concl imp_thm)))], 475 fn [thm] => MP imp_thm thm 476 | _ => raise UTILSLIB_ERR 477 {function = "MP_IMP_TAC", 478 message = "invalid application"})} 479 thisgoal 480 else raise UTILSLIB_ERR 481 {function = "MP_IMP_TAC", 482 message = "theorem doesn't imply goal"} 483 else raise UTILSLIB_ERR 484 {function = "MP_IMP_TAC", 485 message = "theorem is not an implication"} 486 487(* 488 MATCH_THM_TAC : {pattern_function:(term -> term), 489 thm_tactic:thm_tactic} -> thm_tactic 490 491 Used to create a version of a theorem tactic that will do matching 492 against the given theorem. 493*) 494 495fun MATCH_THM_TAC {pattern_function, thm_tactic} = 496 let 497 fun sub_tac thm (asms,goal) = 498 let 499 val (term_substitution,type_substitution) = 500 match_term (pattern_function (concl thm)) goal 501 val inst_thm = 502 STRONG_INST_TY_TERM 503 {term_substitution=term_substitution, 504 type_substitution=type_substitution, 505 theorem=thm} 506 in 507 ((thm_tactic inst_thm) ORELSE 508 (thm_tactic (BETA_RULE inst_thm))) 509 (asms,goal) 510 end 511 in 512 fn thm => (REPEAT GEN_TAC) THEN (sub_tac (SPEC_ALL thm)) 513 end 514 515 516 517(* 518 NEW_MATCH_ACCEPT_TAC : thm -> tactic 519 520 Same as MATCH_ACCEPT_TAC, except that if the instantiated version of 521 the theorem has hypotheses that are not among the goal assumptions, 522 then it creates new subgoals for these, rather than failing. 523*) 524 525val NEW_MATCH_ACCEPT_TAC = 526 MATCH_THM_TAC 527 {pattern_function = (fn x => x), 528 thm_tactic = (fn thm => use_thm {theorem = thm, 529 thm_tactic = ACCEPT_TAC})} 530 531 532(* 533 MATCH_MP_IMP_TAC : thm -> tactic ( thm = [A1] |- t2 ==> t1 ) 534 535 536 [A] t1' 537 ========== 538 [A] t2' 539 540 where t2' ==> t1' is an instance of t2 ==> t1 541*) 542 543 544val MATCH_MP_IMP_TAC = 545 MATCH_THM_TAC 546 {pattern_function = fn tm => #conseq(dest_imp tm), 547 thm_tactic = MP_IMP_TAC} 548 549 550(* 551 REDUCE_TAC : thm_list -> tactic 552 Reduces a goal by stripping and using modus ponens and any theorem 553 which is an implication and whose implication conclusion matches the 554 goal statement. It also solves those subgoals which match any of the 555 given theorems, or which are included among the assumptions. 556*) 557 558local 559 fun tryfind f [] = 560 raise UTILSLIB_ERR{function = "REDUCE_TAC-tryfind", 561 message ="impossible to see this"} 562 | tryfind f (x::rest) = f x handle (HOL_ERR _) => tryfind f rest 563in 564 fun REDUCE_TAC reduction_thms = 565 let 566 val new_reduction_thms = 567 map UNDISCH_ALL (flatten (map IMP_CANON reduction_thms)) 568 val tac_list = 569 map 570 (fn thm => (NEW_MATCH_ACCEPT_TAC thm) ORELSE 571 (MATCH_MP_IMP_TAC thm)) 572 new_reduction_thms 573 fun core_reduce_tac goal = 574 ((FIRST_ASSUM ACCEPT_TAC) ORELSE 575 ((REPEAT STRIP_TAC) THEN 576 ((FIRST_ASSUM ACCEPT_TAC) ORELSE 577 ((fn gl => tryfind (fn f => f gl) tac_list) THEN 578 core_reduce_tac) ORELSE 579 ALL_TAC))) goal 580 in 581 core_reduce_tac 582 end 583end 584 585 586(* Replace by CONV_TAC FUN_EQ_CONV 587 EXT_TAC : term -> tactic ( term = x ) 588 589 [A] t1 = t2 590 ======================= 591 [A] !x. t1 x = t2 x 592 593 x should not be free in t1, t2, or [A]. 594*) 595 596end (* structure utilsLib *) 597