1(*--------------------------------------------------------------------------- 2 Some proof automation, which moreover has few theory 3 dependencies, and so can be used in places where bossLib 4 is overkill. 5 ---------------------------------------------------------------------------*) 6 7structure BasicProvers :> BasicProvers = 8struct 9 10type simpset = simpLib.simpset; 11 12open HolKernel boolLib markerLib; 13 14val op++ = simpLib.++; 15val op&& = simpLib.&&; 16 17val ERR = mk_HOL_ERR "BasicProvers"; 18 19local val EXPAND_COND_CONV = 20 simpLib.SIMP_CONV (pureSimps.pure_ss ++ boolSimps.COND_elim_ss) [] 21 val EXPAND_COND_TAC = CONV_TAC EXPAND_COND_CONV 22 val EXPAND_COND = CONV_RULE EXPAND_COND_CONV 23 val NORM_RULE = CONV_RULE (EXPAND_COND_CONV THENC 24 REWRITE_CONV [markerTheory.Abbrev_def]) 25in 26fun PROVE thl tm = Tactical.prove (tm, 27 EXPAND_COND_TAC THEN mesonLib.MESON_TAC (map NORM_RULE thl)) 28 29fun PROVE_TAC thl (asl, w) = let 30 val working = LLABEL_RESOLVE thl asl 31in 32 EXPAND_COND_TAC THEN CONV_TAC (DEST_LABELS_CONV) THEN 33 mesonLib.MESON_TAC (map NORM_RULE working) 34end (asl, w) 35val prove_tac = PROVE_TAC 36 37fun GEN_PROVE_TAC x y z thl (asl, w) = let 38 val working = LLABEL_RESOLVE thl asl 39in 40 EXPAND_COND_TAC THEN CONV_TAC (DEST_LABELS_CONV) THEN 41 mesonLib.GEN_MESON_TAC x y z (map NORM_RULE working) 42end (asl, w) 43 44end; (* local *) 45 46 47(*---------------------------------------------------------------------------* 48 * A simple aid to reasoning by contradiction. * 49 *---------------------------------------------------------------------------*) 50 51fun SPOSE_NOT_THEN ttac = 52 CCONTR_TAC THEN 53 POP_ASSUM (fn th => ttac (simpLib.SIMP_RULE boolSimps.bool_ss 54 [GSYM boolTheory.IMP_DISJ_THM] th)) 55val spose_not_then = SPOSE_NOT_THEN 56 57(*===========================================================================*) 58(* Case analysis and induction tools that index the TypeBase. *) 59(*===========================================================================*) 60 61fun name_eq s M = ((s = fst(dest_var M)) handle HOL_ERR _ => false) 62 63(*---------------------------------------------------------------------------* 64 * Mildly altered STRUCT_CASES_TAC, so that it does a SUBST_ALL_TAC instead * 65 * of a SUBST1_TAC. * 66 *---------------------------------------------------------------------------*) 67 68val VAR_INTRO_TAC = REPEAT_TCL STRIP_THM_THEN 69 (fn th => SUBST_ALL_TAC th ORELSE ASSUME_TAC th); 70 71val TERM_INTRO_TAC = 72 REPEAT_TCL STRIP_THM_THEN 73 (fn th => TRY (SUBST_ALL_TAC th) THEN ASSUME_TAC th); 74 75fun away gfrees0 bvlist = 76 rev(fst 77 (rev_itlist (fn v => fn (plist,gfrees) => 78 let val v' = prim_variant gfrees v 79 in ((v,v')::plist, v'::gfrees) 80 end) bvlist ([], gfrees0))); 81 82(*---------------------------------------------------------------------------*) 83(* Make free whatever bound variables would prohibit the case split *) 84(* or induction. This is not trivial, since the act of freeing up a variable *) 85(* can change its name (if another with same name already occurs free in *) 86(* hypotheses). Then the term being split (or inducted) on needs to be *) 87(* renamed as well. *) 88(*---------------------------------------------------------------------------*) 89 90fun FREEUP [] M g = (ALL_TAC,M) 91 | FREEUP tofree M (g as (asl,w)) = 92 let val (V,_) = strip_forall w (* ignore renaming here : idleness! *) 93 val Vmap = away (free_varsl (w::asl)) V 94 val theta = filter (fn (v,_) => mem v tofree) Vmap 95 val rebind = map snd (filter (fn (v,_) => not (mem v tofree)) Vmap) 96 in 97 ((MAP_EVERY X_GEN_TAC (map snd Vmap) 98 THEN MAP_EVERY ID_SPEC_TAC (rev rebind)), 99 subst (map op|-> theta) M) 100 end; 101 102(*---------------------------------------------------------------------------*) 103(* Do case analysis on given term. The quotation is parsed into a term M that*) 104(* must match a subterm in the goal (or the assumptions). If M is a variable,*) 105(* then the match of the names must be exact. Once the term to split over is *) 106(* known, its type and the associated facts are obtained and used to do the *) 107(* split with. Variables of M might be quantified in the goal. If so, we try *) 108(* to unquantify the goal so that the case split has meaning. *) 109(* *) 110(* It can happen that the given term is not found anywhere in the goal. If *) 111(* the term is boolean, we do a case-split on whether it is true or false. *) 112(*---------------------------------------------------------------------------*) 113 114datatype tmkind 115 = Free of term 116 | Bound of term list * term (* in Bound(V,M), V = vars to be freed up *) 117 | Alien of term; 118 119fun dest_tmkind (Free M) = M 120 | dest_tmkind (Bound (_,M)) = M 121 | dest_tmkind (Alien M) = M; 122 123fun prim_find_subterm FVs tm (asl,w) = 124 if is_var tm 125 then let val name = fst(dest_var tm) 126 in Free (Lib.first(name_eq name) FVs) 127 handle HOL_ERR _ 128 => Bound(let val (BV,_) = strip_forall w 129 val v = Lib.first (name_eq name) BV 130 in ([v], v) 131 end) 132 end 133 else if List.exists (free_in tm) (w::asl) then Free tm 134 else let val (V,body) = strip_forall w 135 in if free_in tm body 136 then Bound(intersect (free_vars tm) V, tm) 137 else Alien tm 138 end 139 140fun find_subterm qtm (g as (asl,w)) = 141 let val FVs = free_varsl (w::asl) 142 val tm = Parse.parse_in_context FVs qtm 143 in 144 prim_find_subterm FVs tm g 145 end; 146 147 148fun primCases_on st (g as (_,w)) = 149 let val ty = type_of (dest_tmkind st) 150 val {Thy,Tyop,...} = dest_thy_type ty 151 in case TypeBase.fetch ty 152 of SOME facts => 153 let val thm = TypeBasePure.nchotomy_of facts 154 in case st 155 of Free M => 156 if (is_var M) then VAR_INTRO_TAC (ISPEC M thm) else 157 if ty=bool then ASM_CASES_TAC M 158 else TERM_INTRO_TAC (ISPEC M thm) 159 | Bound(V,M) => let val (tac,M') = FREEUP V M g 160 in (tac THEN VAR_INTRO_TAC (ISPEC M' thm)) end 161 | Alien M => if ty=bool then ASM_CASES_TAC M 162 else TERM_INTRO_TAC (ISPEC M thm) 163 end 164 | NONE => raise ERR "primCases_on" 165 ("No cases theorem found for type: "^Lib.quote (Thy^"$"^Tyop)) 166 end g; 167 168fun Cases_on qtm g = primCases_on (find_subterm qtm g) g 169 handle e => raise wrap_exn "BasicProvers" "Cases_on" e; 170 171fun Cases (g as (_,w)) = 172 let val (Bvar,_) = with_exn dest_forall w (ERR "Cases" "not a forall") 173 in primCases_on (Bound([Bvar],Bvar)) g 174 end 175 handle e => raise wrap_exn "BasicProvers" "Cases" e; 176 177(*---------------------------------------------------------------------------*) 178(* Do induction on a given term. *) 179(*---------------------------------------------------------------------------*) 180 181fun primInduct st ind_tac (g as (asl,c)) = 182 let fun ind_non_var V M = 183 let val (tac,M') = FREEUP V M g 184 val Mfrees = free_vars M' 185 fun has_vars tm = not(null_intersection (free_vars tm) Mfrees) 186 val tms = filter has_vars asl 187 val newvar = variant (free_varsl (c::asl)) 188 (mk_var("v",type_of M')) 189 val tm = mk_exists(newvar, mk_eq(newvar, M')) 190 val th = EXISTS(tm,M') (REFL M') 191 in 192 tac 193 THEN MAP_EVERY UNDISCH_TAC tms 194 THEN CHOOSE_THEN MP_TAC th 195 THEN MAP_EVERY ID_SPEC_TAC Mfrees 196 THEN ID_SPEC_TAC newvar 197 THEN ind_tac 198 end 199 in case st 200 of Free M => 201 if is_var M 202 then let val tms = filter (free_in M) asl 203 in (MAP_EVERY UNDISCH_TAC tms THEN ID_SPEC_TAC M THEN ind_tac) g 204 end 205 else ind_non_var [] M g 206 | Bound(V,M) => 207 if is_var M 208 then let val (tac,M') = FREEUP V M g 209 in (tac THEN ID_SPEC_TAC M' THEN ind_tac) g 210 end 211 else ind_non_var V M g 212 | Alien M => 213 if is_var M then raise ERR "primInduct" "Alien variable" 214 else ind_non_var (free_vars M) M g 215 end 216 217(*---------------------------------------------------------------------------*) 218(* Induct on a quoted term. First determine the term, then use that to *) 219(* select the induction theorem to use. There are 3 kinds of induction *) 220(* supported: (1) on datatypes; (2) on inductively defined relations from *) 221(* IndDefLib; (3) on ad-hoc inductive objects (e.g. finite maps, finite sets,*) 222(* and finite multisets). The latter two are similar but differ in where the *) 223(* induction theorem is fetched from (IndDefLib.rule_induction_map or *) 224(* TypeBase.theTypeBase). *) 225(*---------------------------------------------------------------------------*) 226 227fun induct_on_type st ty g = 228 case TypeBase.fetch ty 229 of SOME facts => 230 let val is_mutind_thm = is_conj o snd o strip_imp o snd o strip_forall o concl 231 in 232 case total TypeBasePure.induction_of facts 233 of NONE => raise ERR "induct_on_type" 234 (String.concat ["Type :",Hol_pp.type_to_string ty, 235 " is registed in the types database, ", 236 "but there is no associated induction theorem"]) 237 | SOME thm => (* now select induction tactic *) 238 if null (TypeBasePure.constructors_of facts) (* not a datatype *) 239 then primInduct st (HO_MATCH_MP_TAC thm) else 240 if is_mutind_thm thm 241 then Mutual.MUTUAL_INDUCT_TAC thm 242 else primInduct st (Prim_rec.INDUCT_THEN thm ASSUME_TAC) 243 end g 244 | NONE => raise ERR "induct_on_type" 245 (String.concat ["Type: ",Hol_pp.type_to_string ty, 246 " is not registered in the types database"]); 247 248fun Induct_on qtm g = 249 let val st = find_subterm qtm g 250 val tm = dest_tmkind st 251 val ty = type_of (dest_tmkind st) 252 val (_, rngty) = strip_fun ty 253 in 254 if rngty = Type.bool then (* inductive relation *) 255 let val (c, _) = strip_comb tm 256 in case Lib.total dest_thy_const c 257 of SOME {Thy,Name,...} => 258 let val indth = Binarymap.find 259 (IndDefLib.rule_induction_map(), 260 {Thy=Thy,Name=Name}) handle NotFound => [] 261 in 262 MAP_FIRST HO_MATCH_MP_TAC indth ORELSE 263 induct_on_type st ty 264 end g 265 | NONE => induct_on_type st ty g 266 end 267 else 268 induct_on_type st ty g 269 end 270 handle e => raise wrap_exn "BasicProvers" "Induct_on" e; 271 272(*---------------------------------------------------------------------------*) 273(* Induct on leading quantified variable. *) 274(*---------------------------------------------------------------------------*) 275 276fun grab_var M = 277 if is_forall M then fst(dest_forall M) else 278 if is_conj M then fst(dest_forall(fst(dest_conj M))) 279 else raise ERR "Induct" "expected a forall or a conjunction of foralls"; 280 281fun Induct (g as (_,w)) = 282 let val v = grab_var w 283 val (_,ty) = dest_var (grab_var w) 284 in induct_on_type (Bound([v],v)) ty g 285 end 286 handle e => raise wrap_exn "BasicProvers" "Induct" e 287 288 289(*--------------------------------------------------------------------------- 290 Assertional style reasoning 291 ---------------------------------------------------------------------------*) 292 293fun chop_at n frontacc l = 294 if n <= 0 then (List.rev frontacc, l) 295 else 296 case l of 297 [] => raise Fail "chop_at" 298 | (h::t) => chop_at (n-1) (h::frontacc) t 299 300 301infix gTHEN1 (* "gentle" THEN1 : doesn't fail if the tactic for the 302 head goal doesn't completely solve the subgoal. *) 303fun ((tac1:tactic) gTHEN1 (tac2:tactic)) (asl:term list,w:term) = let 304 val (subgoals, vf) = tac1 (asl,w) 305in 306 case subgoals of 307 [] => ([], vf) 308 | (h::hs) => let 309 val (sgoals2, vf2) = tac2 h 310 in 311 (sgoals2 @ hs, 312 (fn thmlist => let 313 val (firstn, back) = chop_at (length sgoals2) [] thmlist 314 in 315 vf (vf2 firstn :: back) 316 end)) 317 end 318end 319 320 321fun eqTRANS new old = let 322 (* allow for possibility that old might be labelled *) 323 open markerLib markerSyntax 324 val s = #1 (dest_label (concl old)) 325in 326 ASSUME_NAMED_TAC s (TRANS (DEST_LABEL old) new) 327end handle HOL_ERR _ => ASSUME_TAC (TRANS old new) 328 329fun is_labeq t = (* term is a possibly labelled equality *) 330 let open markerSyntax 331 in is_eq t orelse is_label t andalso is_eq (#2 (dest_label t)) 332 end; 333 334fun labrhs t = (* term is a possibly labelled equality *) 335 let open markerSyntax 336 in if is_eq t then rhs t else rhs (#2 (dest_label t)) 337 end; 338 339fun qlinenum q = 340 case q |> qbuf.new_buffer |> qbuf.current |> #2 of 341 locn.Loc(locn.LocA(line, _), _) => SOME (line+1) 342 | _ => NONE 343 344fun by0 k (q, tac) (g as (asl,w)) = let 345 val a = trace ("syntax_error", 0) Parse.Absyn q 346 open errormonad 347 val (goal_pt, finisher) = 348 case Lib.total Absyn.dest_eq a of 349 SOME (Absyn.IDENT(_,"_"), r) => 350 if not (null asl) andalso is_labeq (hd asl) then 351 (Parse.absyn_to_preterm 352 (Absyn.mk_eq(Absyn.mk_AQ (labrhs (hd asl)), r)), 353 POP_ASSUM o eqTRANS) 354 else 355 raise ERR "by" "Top assumption must be an equality" 356 | x => (Parse.absyn_to_preterm a, STRIP_ASSUME_TAC) 357 val tm = trace ("show_typecheck_errors", 0) 358 (Preterm.smash 359 (goal_pt >- 360 TermParse.ctxt_preterm_to_term 361 Parse.stdprinters 362 (SOME bool) 363 (free_varsl (w::asl)))) 364 Pretype.Env.empty 365 fun mk_errmsg () = 366 case qlinenum q of 367 SOME l => " on line "^Int.toString l 368 | NONE => ": "^term_to_string tm 369in 370 (SUBGOAL_THEN tm finisher gTHEN1 (tac THEN k)) g 371 handle HOL_ERR _ => 372 raise ERR "by" ("by's tactic failed to prove subgoal"^mk_errmsg()) 373end 374 375val op by = by0 NO_TAC 376val byA = by0 ALL_TAC 377 378fun (q suffices_by tac) g = 379 (Q_TAC SUFF_TAC q gTHEN1 (tac THEN NO_TAC)) g 380 handle e as HOL_ERR {origin_function,...} => 381 if origin_function = "Q_TAC" then raise e 382 else 383 case qlinenum q of 384 SOME l => raise ERR "suffices_by" 385 ("suffices_by's tactic failed to prove goal on \ 386 \line "^Int.toString l) 387 | NONE => raise ERR "suffices_by" 388 "suffices_by's tactic failed to prove goal" 389 390 391 392fun subgoal q = Q.SUBGOAL_THEN q STRIP_ASSUME_TAC 393val sg = subgoal 394 395 396infix on 397fun ((ttac:thm->tactic) on (q:term frag list, tac:tactic)) : tactic = 398 (fn (g as (asl:term list, w:term)) => let 399 val tm = Parse.parse_in_context (free_varsl (w::asl)) q 400 in 401 (SUBGOAL_THEN tm ttac gTHEN1 tac) g 402 end) 403 404(*===========================================================================*) 405(* General-purpose case-splitting tactics. *) 406(*===========================================================================*) 407 408fun case_find_subterm p = 409 let 410 val f = find_term p 411 fun g t = 412 if is_comb t then 413 g (f (rator t)) 414 handle HOL_ERR _ => (g (f (rand t)) handle HOL_ERR _ => t) 415 else if is_abs t then 416 g (f (body t)) handle HOL_ERR _ => t 417 else t 418 in 419 fn t => g (f t) 420 end; 421 422fun first_term f tm = f (find_term (can f) tm); 423 424fun first_subterm f tm = f (case_find_subterm (can f) tm); 425 426(*---------------------------------------------------------------------------*) 427(* If tm is a fully applied conditional or case expression and the *) 428(* scrutinized subterm of tm is free, return the scrutinized subterm. *) 429(* Otherwise raise an exception. *) 430(*---------------------------------------------------------------------------*) 431 432fun scrutinized_and_free_in tm = 433 let fun free_case t = 434 let val (_, examined, _) = TypeBase.dest_case t 435 in if free_in examined tm 436 then examined else raise ERR "free_case" "" 437 end 438 in 439 free_case 440 end; 441 442fun PURE_TOP_CASE_TAC (g as (_, tm)) = 443 let val t = first_term (scrutinized_and_free_in tm) tm 444 in Cases_on `^t` end g; 445 446fun PURE_CASE_TAC (g as (_, tm)) = 447 let val t = first_subterm (scrutinized_and_free_in tm) tm 448 in Cases_on `^t` end g; 449 450fun PURE_FULL_CASE_TAC (g as (asl,w)) = 451 let val tm = list_mk_conj(w::asl) 452 val t = first_subterm (scrutinized_and_free_in tm) tm 453 in Cases_on `^t` end g; 454 455local 456 fun tot f x = f x handle HOL_ERR _ => NONE 457in 458fun case_rws tyi = 459 List.mapPartial I 460 [Lib.total TypeBasePure.case_def_of tyi, 461 tot TypeBasePure.distinct_of tyi, 462 tot TypeBasePure.one_one_of tyi] 463 464fun case_rwlist () = 465 itlist (fn tyi => fn rws => case_rws tyi @ rws) 466 (TypeBase.elts()) []; 467 468(* Add the rewrites into a simpset to avoid re-processing them when 469 * (PURE_CASE_SIMP_CONV rws) is called multiple times by EVERY_CASE_TAC. This 470 * has an order of magnitude speedup on developments with large datatypes *) 471fun PURE_CASE_SIMP_CONV rws = simpLib.SIMP_CONV (boolSimps.bool_ss++simpLib.rewrites rws) [] 472 473fun CASE_SIMP_CONV tm = PURE_CASE_SIMP_CONV (case_rwlist()) tm 474end; 475 476(*---------------------------------------------------------------------------*) 477(* Q: what should CASE_TAC do with literal case expressions? *) 478(*---------------------------------------------------------------------------*) 479 480fun is_refl tm = 481 let val (l,r) = dest_eq tm 482 in aconv l r 483 end handle HOL_ERR _ => false; 484 485fun TRIV_LET_CONV tm = 486 let val (_,a) = boolSyntax.dest_let tm 487 in if is_var a orelse is_const a 488 orelse Literal.is_literal a 489 then (REWR_CONV LET_THM THENC BETA_CONV) tm 490 else NO_CONV tm 491 end; 492 493fun SIMP_OLD_ASSUMS (orig as (asl1,_)) (gl as (asl2,_)) = 494 let val new = op_set_diff aconv asl2 asl1 495 in if null new then ALL_TAC 496 else let val thms = map ASSUME new 497 in MAP_EVERY (Lib.C UNDISCH_THEN (K ALL_TAC)) new THEN 498 RULE_ASSUM_TAC (REWRITE_RULE thms) THEN 499 MAP_EVERY ASSUME_TAC thms 500 end 501 end gl; 502 503fun USE_NEW_ASSUM orig_goal cgoal = 504 (TRY (WEAKEN_TAC is_refl) THEN 505 ASM_REWRITE_TAC[] THEN 506 SIMP_OLD_ASSUMS orig_goal THEN 507 CONV_TAC (DEPTH_CONV TRIV_LET_CONV)) cgoal; 508 509(*---------------------------------------------------------------------------*) 510(* Do a case analysis in the conclusion of the goal, then simplify a bit. *) 511(*---------------------------------------------------------------------------*) 512 513fun CASE_TAC gl = 514 (PURE_CASE_TAC THEN USE_NEW_ASSUM gl THEN CONV_TAC CASE_SIMP_CONV) gl; 515 516fun TOP_CASE_TAC gl = 517 (PURE_TOP_CASE_TAC THEN USE_NEW_ASSUM gl THEN CONV_TAC CASE_SIMP_CONV) gl; 518 519 520(*---------------------------------------------------------------------------*) 521(* Do a case analysis anywhere in the goal, then simplify a bit. *) 522(*---------------------------------------------------------------------------*) 523 524fun FULL_CASE_TAC goal = 525 let val rws = case_rwlist() 526 val case_conv = PURE_CASE_SIMP_CONV rws 527 val asm_rule = Rewrite.REWRITE_RULE rws 528 in PURE_FULL_CASE_TAC THEN USE_NEW_ASSUM goal 529 THEN RULE_ASSUM_TAC asm_rule 530 THEN CONV_TAC case_conv 531 end goal; 532val full_case_tac = FULL_CASE_TAC 533 534(*---------------------------------------------------------------------------*) 535(* Repeatedly do a case analysis anywhere in the goal. Avoids re-computing *) 536(* case info from the TypeBase each time around the loop, so more efficient *) 537(* than REPEAT FULL_CASE_TAC. *) 538(*---------------------------------------------------------------------------*) 539 540fun EVERY_CASE_TAC goal = 541 let val rws = case_rwlist() 542 val case_conv = PURE_CASE_SIMP_CONV rws 543 val asm_rule = BETA_RULE o Rewrite.REWRITE_RULE rws 544 fun tac a = (PURE_FULL_CASE_TAC THEN USE_NEW_ASSUM a THEN 545 RULE_ASSUM_TAC asm_rule THEN 546 CONV_TAC case_conv) a 547 in REPEAT tac 548 end goal; 549val every_case_tac = EVERY_CASE_TAC 550 551(*===========================================================================*) 552(* Rewriters *) 553(*===========================================================================*) 554 555(*---------------------------------------------------------------------------* 556 * When invoked, we know that th is an equality, at least one side of which * 557 * is a variable. * 558 *---------------------------------------------------------------------------*) 559 560fun is_bool_atom tm = 561 is_var tm andalso (type_of tm = bool) 562 orelse is_neg tm andalso is_var (dest_neg tm); 563 564 565fun orient th = 566 let val c = concl th 567 in if is_bool_atom c 568 then (if is_neg c then EQF_INTRO th else EQT_INTRO th) 569 else let val (lhs,rhs) = dest_eq c 570 in if is_var lhs 571 then if is_var rhs 572 then case Term.compare (lhs, rhs) 573 of LESS => SYM th 574 | other => th 575 else th 576 else SYM th 577 end 578 end; 579 580fun VSUBST_TAC tm = UNDISCH_THEN tm (SUBST_ALL_TAC o orient); 581 582fun var_eq tm = 583 let val (lhs,rhs) = dest_eq tm 584 in 585 aconv lhs rhs 586 orelse 587 (is_var lhs andalso not (free_in lhs rhs)) 588 orelse 589 (is_var rhs andalso not (free_in rhs lhs)) 590 end 591 handle HOL_ERR _ => is_bool_atom tm 592 593 594fun grab P f v = 595 let fun grb [] = v 596 | grb (h::t) = if P h then f h else grb t 597 in grb 598 end; 599 600fun ASSUM_TAC f P = W (fn (asl,_) => grab P f NO_TAC asl) 601 602val VAR_EQ_TAC = ASSUM_TAC VSUBST_TAC var_eq; 603val var_eq_tac = VAR_EQ_TAC 604 605fun ASSUMS_TAC f P = W (fn (asl,_) => 606 case filter P asl 607 of [] => NO_TAC 608 | assums => MAP_EVERY f (List.rev assums)); 609 610fun CONCL_TAC f P = W (fn (_,c) => if P c then f else NO_TAC); 611 612fun LIFT_SIMP ss tm = 613 UNDISCH_THEN tm (STRIP_ASSUME_TAC o simpLib.SIMP_RULE ss []); 614 615local 616 fun DTHEN ttac = fn (asl,w) => 617 let val (ant,conseq) = dest_imp_only w 618 val (gl,prf) = ttac (ASSUME ant) (asl,conseq) 619 in (gl, Thm.DISCH ant o prf) 620 end 621in 622val BOSS_STRIP_TAC = Tactical.FIRST [GEN_TAC,CONJ_TAC, DTHEN STRIP_ASSUME_TAC] 623end; 624 625fun tyi_to_ssdata tyinfo = 626 let open simpLib 627 val (thy,tyop) = TypeBasePure.ty_name_of tyinfo 628 val {rewrs, convs} = TypeBasePure.simpls_of tyinfo; 629in 630 SSFRAG {name = SOME("Datatype "^thy^"$"^tyop), 631 convs = convs, rewrs = rewrs, filter = NONE, 632 dprocs = [], ac = [], congs = []} 633end 634 635fun add_simpls tyinfo ss = (ss ++ tyi_to_ssdata tyinfo) handle HOL_ERR _ => ss; 636 637fun is_dneg tm = 1 < snd(strip_neg tm); 638 639val notT = mk_neg T 640val notF = mk_neg F; 641 642fun breakable tm = 643 is_exists tm orelse 644 is_conj tm orelse 645 is_disj tm orelse 646 is_dneg tm orelse 647 notT = tm orelse 648 notF = tm orelse 649 T=tm orelse F=tm 650 651(* ---------------------------------------------------------------------- 652 LET_ELIM_TAC 653 654 eliminates lets by pulling them up, turning them into universal 655 quantifiers, and eventually moving new abbreviations into the 656 assumption list. 657 ---------------------------------------------------------------------- *) 658 659val let_movement_thms = let 660 open combinTheory 661in 662 ref [o_THM, o_ABS_R, C_ABS_L, C_THM, 663 GEN_literal_case_RAND, GEN_literal_case_RATOR, 664 GEN_LET_RAND, GEN_LET_RATOR, S_ABS_R] 665end 666 667val IMP_CONG' = REWRITE_RULE [GSYM AND_IMP_INTRO] (SPEC_ALL IMP_CONG) 668 669fun ABBREV_CONV tm = let 670 val t = rand tm 671 val (l,r) = dest_eq t 672in 673 if not (is_var l) orelse is_var r then 674 REWR_CONV markerTheory.Abbrev_def THENC 675 REWR_CONV EQ_SYM_EQ 676 else ALL_CONV 677end tm 678 679val ABBREV_ss = 680 simpLib.SSFRAG {name=SOME"ABBREV", 681 ac = [], congs = [], 682 convs = [{conv = K (K ABBREV_CONV), 683 key = SOME ([], ``marker$Abbrev x``), 684 trace = 2, name = "ABBREV_CONV"}], 685 dprocs = [], filter = NONE, rewrs = []} 686 687(*---------------------------------------------------------------------------*) 688(* The staging of first two successive calls to SIMP_CONV ensure that the *) 689(* LET_FORALL_ELIM theorem is applied after all the movement is possible. *) 690(*---------------------------------------------------------------------------*) 691 692fun LET_ELIM_TAC goal = 693 let open simpLib pureSimps boolSimps 694 in 695 CONV_TAC 696 (QCHANGED_CONV 697 (SIMP_CONV pure_ss (!let_movement_thms) THENC 698 SIMP_CONV pure_ss (combinTheory.LET_FORALL_ELIM :: 699 combinTheory.literal_case_FORALL_ELIM :: 700 !let_movement_thms) THENC 701 SIMP_CONV (pure_ss ++ ABBREV_ss ++ UNWIND_ss) [Cong IMP_CONG'])) THEN 702 REPEAT BOSS_STRIP_TAC THEN markerLib.REABBREV_TAC 703 end goal 704 705fun new_let_thms thl = let_movement_thms := thl @ !let_movement_thms 706 707 708(*--------------------------------------------------------------------------- 709 STP_TAC (Simplify then Prove) 710 711 The following is a straightforward but quite helpful simplification 712 procedure. It treats the rewrite rules for all declared datatypes as 713 being built-in, so that the user does not have to mention them. 714 715 0. Build a simpset from the given ss and the rewrites coming from 716 any constructors that are found in TypeBase. 717 718 1. Remove all universal quantifiers and break down all conjunctions 719 720 2. Eliminate all "var-equalities" from the assumptions 721 722 3. Simplify the goal with respect to the assumptions and the given 723 simplification set. 724 725 4. Case split on conditionals as much as possible. 726 727 5. Strip as much as possible to the assumptions. 728 729 6. Until there is no change in the complete goal, attempt to do one 730 of the following: 731 732 * eliminate a var-equality 733 734 * break up an equation between constructors in the assumptions 735 736 * break up an equation between constructors in the goal 737 738 * break up conjunctions, disjunctions, existentials, or 739 double negations occurring in the assumptions 740 741 * eliminate occurrences of T (toss it away) and F (prove the goal) 742 in the assumptions 743 744 * eliminate lets in the goal, by lifting into the assumptions as 745 abbreviations (using LET_ELIM_TAC) 746 747 7. Apply the finishing tactic. 748 749 ---------------------------------------------------------------------------*) 750 751fun tyinfol() = TypeBasePure.listItems (TypeBase.theTypeBase()); 752 753fun mkCSET () = 754 let val CSET = (HOLset.empty 755 (inv_img_cmp (fn {Thy,Name,Ty} => (Thy,Name)) 756 (pair_compare(String.compare,String.compare)))) 757 fun add_const (c,CSET) = HOLset.add(CSET, dest_thy_const c) 758 fun add_tyinfo (tyinfo,CSET) = 759 List.foldl add_const CSET (TypeBasePure.constructors_of tyinfo) 760 val CSET = List.foldl add_tyinfo CSET (tyinfol()) 761 fun inCSET t = HOLset.member(CSET, dest_thy_const t) 762 fun constructed tm = 763 let val (lhs,rhs) = dest_eq tm 764 in aconv lhs rhs orelse 765 let val maybe1 = fst(strip_comb lhs) 766 val maybe2 = fst(strip_comb rhs) 767 in is_const maybe1 andalso is_const maybe2 768 andalso 769 inCSET maybe1 andalso inCSET maybe2 770 end 771 end handle HOL_ERR _ => false 772 in 773 Lib.can (find_term constructed) 774 end; 775 776val leave_lets_var = mk_var("__leave_lets_alone__", bool) 777val LEAVE_LETS = ASSUME leave_lets_var 778 779fun PRIM_STP_TAC ss finisher = 780 let val has_constr_eqn = mkCSET () 781 val ASM_SIMP = simpLib.ASM_SIMP_TAC ss [] 782 (* we don't have access to any theorem list that might have been passed 783 to RW_TAC or SRW_TAC at this point, but we can look for the effect of 784 the LEAVE_LETS theorem by attempting to rewrite something that only it 785 should affect; if the simplifier doesn't change the leave_lets_var, 786 then LEAVE_LETS is not part of the ss, so we should do LET_ELIM_TAC, 787 otherwise, we shouldn't. 788 789 Also, if there are no lets about then 790 don't attempt LET_ELIM_TAC at all. This is because LET_ELIM_TAC 791 includes rewrites like |- f o (\x. g x) = \x. f (g x) and these 792 can alter goals that don't have any lets in them at all, possibly 793 against user expectations. A less sledge-hammer implementation of 794 LET_ELIM_TAC might not have this problem... *) 795 val do_lets = (simpLib.SIMP_CONV ss [] leave_lets_var ; false) 796 handle Conv.UNCHANGED => true 797 val LET_ELIM_TAC = 798 if do_lets then 799 (fn g as (_,w) => 800 if can (find_term is_let) w 801 then LET_ELIM_TAC g 802 else NO_TAC g) 803 else NO_TAC 804 in 805 REPEAT (GEN_TAC ORELSE CONJ_TAC) 806 THEN REPEAT VAR_EQ_TAC 807 THEN ASM_SIMP 808 THEN TRY (IF_CASES_TAC THEN REPEAT IF_CASES_TAC THEN ASM_SIMP) 809 THEN REPEAT BOSS_STRIP_TAC 810 THEN REPEAT (CHANGED_TAC 811 (VAR_EQ_TAC 812 ORELSE ASSUMS_TAC (LIFT_SIMP ss) has_constr_eqn 813 ORELSE ASSUM_TAC (LIFT_SIMP ss) breakable 814 ORELSE CONCL_TAC ASM_SIMP has_constr_eqn 815 ORELSE LET_ELIM_TAC)) 816 THEN TRY finisher 817 end 818 819(*--------------------------------------------------------------------------- 820 PRIM_NORM_TAC: preliminary attempt at keeping the goal in a 821 fully constructor-reduced format. The idea is that there should 822 be no equations between constructor terms anywhere in the goal. 823 (This is what PRIM_STP_TAC already does.) 824 825 Also, no conditionals should occur in the resulting goal. 826 This seems to be an expensive test, especially since the work 827 in detecting the conditional is replicated in IF_CASES_TAC. 828 829 Continuing in this light, it seems possible to eliminate all 830 case expressions in the goal, but that hasn't been implemented yet. 831 ---------------------------------------------------------------------------*) 832 833fun splittable w = 834 Lib.can (find_term (fn tm => (is_cond tm orelse TypeBase.is_case tm) 835 andalso free_in tm w)) w; 836 837fun LIFT_SPLIT_SIMP ss simp tm = 838 UNDISCH_THEN tm 839 (fn th => MP_TAC (simpLib.SIMP_RULE ss [] th) 840 THEN CASE_TAC 841 THEN simp 842 THEN REPEAT BOSS_STRIP_TAC); 843 844fun SPLIT_SIMP simp = TRY (IF_CASES_TAC ORELSE CASE_TAC) THEN simp ; 845 846fun PRIM_NORM_TAC ss = 847 let val has_constr_eqn = mkCSET() 848 val ASM_SIMP = simpLib.ASM_SIMP_TAC ss [] 849 in 850 REPEAT (GEN_TAC ORELSE CONJ_TAC) 851 THEN REPEAT VAR_EQ_TAC 852 THEN ASM_SIMP 853 THEN TRY (IF_CASES_TAC THEN REPEAT IF_CASES_TAC THEN ASM_SIMP) 854 THEN REPEAT BOSS_STRIP_TAC 855 THEN REPEAT (CHANGED_TAC 856 (VAR_EQ_TAC 857 ORELSE ASSUMS_TAC (LIFT_SIMP ss) has_constr_eqn 858 ORELSE ASSUM_TAC (LIFT_SIMP ss) breakable 859 ORELSE CONCL_TAC ASM_SIMP has_constr_eqn 860 ORELSE ASSUM_TAC (LIFT_SPLIT_SIMP ss ASM_SIMP) splittable 861 ORELSE CONCL_TAC (SPLIT_SIMP ASM_SIMP) splittable 862 ORELSE LET_ELIM_TAC)) 863 end 864 865 866(*--------------------------------------------------------------------------- 867 Adding simplification sets in for all datatypes each time 868 STP_TAC is invoked can be slow. In such cases, use 869 PRIM_STP tac instead. 870 ---------------------------------------------------------------------------*) 871 872fun STP_TAC ss finisher 873 = PRIM_STP_TAC (rev_itlist add_simpls (tyinfol()) ss) finisher 874 875fun RW_TAC ss thl g = markerLib.ABBRS_THEN 876 (fn thl => STP_TAC (ss && thl) NO_TAC) thl 877 g 878val rw_tac = RW_TAC 879 880fun NORM_TAC ss thl g = 881 markerLib.ABBRS_THEN 882 (fn thl => PRIM_NORM_TAC (rev_itlist add_simpls (tyinfol()) (ss && thl))) 883 thl 884 g 885 886val bool_ss = boolSimps.bool_ss; 887 888(*--------------------------------------------------------------------------- 889 Stateful version of RW_TAC: doesn't load the constructor 890 simplifications into the simpset at each invocation, but 891 just when a datatype is declared. 892 ---------------------------------------------------------------------------*) 893 894val (srw_ss : simpset ref) = ref (bool_ss ++ combinSimps.COMBIN_ss); 895 896val srw_ss_initialised = ref false; 897 898val pending_updates = ref ([]: simpLib.ssfrag list); 899 900fun initialise_srw_ss() = 901 if !srw_ss_initialised then !srw_ss 902 else let in 903 HOL_PROGRESS_MESG ("Initialising SRW simpset ... ", "done") 904 (fn () => 905 (srw_ss := rev_itlist add_simpls (tyinfol()) (!srw_ss) ; 906 srw_ss := foldl (fn (ssd,ss) => ss ++ ssd) (!srw_ss) 907 (!pending_updates) ; 908 srw_ss_initialised := true)) () ; 909 !srw_ss 910 end; 911 912fun augment_srw_ss ssdl = 913 if !srw_ss_initialised then 914 srw_ss := foldl (fn (ssd,ss) => ss ++ ssd) (!srw_ss) ssdl 915 else 916 pending_updates := !pending_updates @ ssdl; 917 918fun diminish_srw_ss names = 919 if !srw_ss_initialised then 920 let 921 val (frags, rest) = (!srw_ss) |> simpLib.ssfrags_of 922 |> List.rev 923 |> simpLib.partition_ssfrags names 924 val _ = srw_ss := simpLib.mk_simpset rest 925 in 926 frags 927 end 928 else 929 let 930 val (frags, rest) = simpLib.partition_ssfrags names (!pending_updates) 931 val _ = pending_updates := rest 932 in 933 frags 934 end; 935 936fun update_fn tyi = 937 augment_srw_ss ([tyi_to_ssdata tyi] handle HOL_ERR _ => []) 938 939val () = 940 TypeBase.register_update_fn (fn tyinfos => (app update_fn tyinfos; tyinfos)) 941 942fun srw_ss () = initialise_srw_ss(); 943 944fun SRW_TAC ssdl thl g = let 945 val ss = foldl (fn (ssd, ss) => ss ++ ssd) (srw_ss()) ssdl 946in 947 markerLib.ABBRS_THEN (fn thl => PRIM_STP_TAC (ss && thl) NO_TAC) thl 948end g; 949val srw_tac = SRW_TAC 950 951val Abbr = markerSyntax.Abbr 952 953(* ---------------------------------------------------------------------- 954 Make some additions to the srw_ss persistent 955 ---------------------------------------------------------------------- *) 956 957open LoadableThyData 958 959(* store a database of per-theory simpset fragments *) 960val thy_ssfrags = ref (Binarymap.mkDict String.compare) 961fun thy_ssfrag s = Binarymap.find(!thy_ssfrags, s) 962 963fun add_rewrites thyname (thms : (string * thm) list) = let 964 val ssfrag = simpLib.named_rewrites thyname (map #2 thms) 965 open Binarymap 966in 967 augment_srw_ss [ssfrag]; 968 case peek(!thy_ssfrags, thyname) of 969 NONE => thy_ssfrags := insert(!thy_ssfrags, thyname, ssfrag) 970 | SOME sf' => let 971 val sf = simpLib.named_merge_ss thyname [sf', ssfrag] 972 in 973 thy_ssfrags := insert(!thy_ssfrags, thyname, sf) 974 end 975end 976 977val {mk,dest,export} = 978 ThmSetData.new_exporter "simp" add_rewrites 979 980fun export_rewrites slist = List.app export slist 981 982end 983