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.&&; 16val op-* = simpLib.-*; 17 18val ERR = mk_HOL_ERR "BasicProvers"; 19 20local val EXPAND_COND_CONV = 21 simpLib.SIMP_CONV (pureSimps.pure_ss ++ boolSimps.COND_elim_ss) [] 22 val EXPAND_COND_TAC = CONV_TAC EXPAND_COND_CONV 23 val EXPAND_COND = CONV_RULE EXPAND_COND_CONV 24 val NORM_RULE = CONV_RULE (EXPAND_COND_CONV THENC 25 REWRITE_CONV [markerTheory.Abbrev_def]) 26in 27fun PROVE thl tm = Tactical.prove (tm, 28 EXPAND_COND_TAC THEN mesonLib.MESON_TAC (map NORM_RULE thl)) 29 30fun PROVE_TAC thl (asl, w) = let 31 val working = LLABEL_RESOLVE thl asl 32in 33 EXPAND_COND_TAC THEN CONV_TAC (DEST_LABELS_CONV) THEN 34 mesonLib.MESON_TAC (map NORM_RULE working) 35end (asl, w) 36val prove_tac = PROVE_TAC 37 38fun GEN_PROVE_TAC x y z thl (asl, w) = let 39 val working = LLABEL_RESOLVE thl asl 40in 41 EXPAND_COND_TAC THEN CONV_TAC (DEST_LABELS_CONV) THEN 42 mesonLib.GEN_MESON_TAC x y z (map NORM_RULE working) 43end (asl, w) 44 45end; (* local *) 46 47 48(*---------------------------------------------------------------------------* 49 * A simple aid to reasoning by contradiction. * 50 *---------------------------------------------------------------------------*) 51 52fun SPOSE_NOT_THEN ttac = 53 CCONTR_TAC THEN 54 POP_ASSUM (fn th => ttac (simpLib.SIMP_RULE boolSimps.bool_ss 55 [GSYM boolTheory.IMP_DISJ_THM] th)) 56val spose_not_then = SPOSE_NOT_THEN 57 58(*===========================================================================*) 59(* Case analysis and induction tools that index the TypeBase. *) 60(*===========================================================================*) 61 62fun name_eq s M = ((s = fst(dest_var M)) handle HOL_ERR _ => false) 63 64(*---------------------------------------------------------------------------* 65 * Mildly altered STRUCT_CASES_TAC, so that it does a SUBST_ALL_TAC instead * 66 * of a SUBST1_TAC. * 67 *---------------------------------------------------------------------------*) 68 69val VAR_INTRO_TAC = REPEAT_TCL STRIP_THM_THEN 70 (fn th => SUBST_ALL_TAC th ORELSE ASSUME_TAC th); 71 72val TERM_INTRO_TAC = 73 REPEAT_TCL STRIP_THM_THEN 74 (fn th => TRY (SUBST_ALL_TAC th) THEN ASSUME_TAC th); 75 76fun away gfrees0 bvlist = 77 rev(fst 78 (rev_itlist (fn v => fn (plist,gfrees) => 79 let val v' = prim_variant gfrees v 80 in ((v,v')::plist, v'::gfrees) 81 end) bvlist ([], gfrees0))); 82 83(*---------------------------------------------------------------------------*) 84(* Make free whatever bound variables would prohibit the case split *) 85(* or induction. This is not trivial, since the act of freeing up a variable *) 86(* can change its name (if another with same name already occurs free in *) 87(* hypotheses). Then the term being split (or inducted) on needs to be *) 88(* renamed as well. *) 89(*---------------------------------------------------------------------------*) 90 91fun FREEUP [] M g = (ALL_TAC,M) 92 | FREEUP tofree M (g as (asl,w)) = 93 let val (V,_) = strip_forall w (* ignore renaming here : idleness! *) 94 val Vmap = away (free_varsl (w::asl)) V 95 val theta = filter (fn (v,_) => op_mem aconv v tofree) Vmap 96 val rebind = 97 map snd (filter (fn (v,_) => not (op_mem aconv v tofree)) Vmap) 98 in 99 ((MAP_EVERY X_GEN_TAC (map snd Vmap) 100 THEN MAP_EVERY ID_SPEC_TAC (rev rebind)), 101 subst (map op|-> theta) M) 102 end; 103 104(*---------------------------------------------------------------------------*) 105(* Do case analysis on given term. The quotation is parsed into a term M that*) 106(* must match a subterm in the goal (or the assumptions). If M is a variable,*) 107(* then the match of the names must be exact. Once the term to split over is *) 108(* known, its type and the associated facts are obtained and used to do the *) 109(* split with. Variables of M might be quantified in the goal. If so, we try *) 110(* to unquantify the goal so that the case split has meaning. *) 111(* *) 112(* It can happen that the given term is not found anywhere in the goal. If *) 113(* the term is boolean, we do a case-split on whether it is true or false. *) 114(*---------------------------------------------------------------------------*) 115 116datatype tmkind 117 = Free of term 118 | Bound of term list * term (* in Bound(V,M), V = vars to be freed up *) 119 | Alien of term; 120 121fun dest_tmkind (Free M) = M 122 | dest_tmkind (Bound (_,M)) = M 123 | dest_tmkind (Alien M) = M; 124 125fun prim_find_subterm FVs tm (asl,w) = 126 if is_var tm 127 then let val name = fst(dest_var tm) 128 in Free (Lib.first(name_eq name) FVs) 129 handle HOL_ERR _ 130 => Bound(let val (BV,_) = strip_forall w 131 val v = Lib.first (name_eq name) BV 132 in ([v], v) 133 end) 134 end 135 else if List.exists (free_in tm) (w::asl) then Free tm 136 else let val (V,body) = strip_forall w 137 in if free_in tm body 138 then Bound(op_intersect aconv (free_vars tm) V, tm) 139 else Alien tm 140 end 141 142fun find_subterm qtm (g as (asl,w)) = 143 let val FVs = free_varsl (w::asl) 144 val tm = Parse.parse_in_context FVs qtm 145 in 146 prim_find_subterm FVs tm g 147 end; 148 149(*---------------------------------------------------------------------------*) 150(* Support for pairs copied from coretypes/pairSyntax to be self-contained. *) 151(*---------------------------------------------------------------------------*) 152 153val strip_prod = 154 let fun dest_prod ty = 155 case total dest_thy_type ty of 156 SOME{Tyop = "prod", Thy = "pair", Args = [ty1, ty2]} => (ty1, ty2) 157 | other => raise ERR "dest_prod" "not a product type" 158 in 159 strip_binop dest_prod 160 end 161 162fun mk_prod(ty1,ty2) = mk_thy_type{Thy="pair",Tyop="prod",Args=[ty1,ty2]} 163 164fun mk_pair (t1,t2) = 165 let val pair_const = prim_mk_const {Name=",",Thy="pair"} 166 val pair_const' = inst [alpha |-> type_of t1, beta |-> type_of t2] pair_const 167 in list_mk_comb(pair_const',[t1,t2]) 168 end 169 170(*---------------------------------------------------------------------------*) 171(* *) 172(* Gamma, (x = pat[v1,...,vn]) |- M[x] *) 173(* ------------------------------------------------------------------ *) 174(* Gamma, ?v1 ... vn. (x = pat[v1,...,vn]) |- M[x] *) 175(* *) 176(*---------------------------------------------------------------------------*) 177 178fun CHOOSER v (tm,thm) = 179 let val ex_tm = mk_exists(v,tm) 180 in (ex_tm, CHOOSE(v, ASSUME ex_tm) thm) 181 end; 182 183fun LEFT_EXISTS_INTRO veq thm = 184 let val (_,pat) = dest_eq veq 185 in snd (itlist CHOOSER (free_vars_lr pat) (veq,thm)) 186 end; 187 188fun listpair [a,b] = (a,b) 189 | listpair l = raise ERR "listpair" 190 ("List of wrong length (" ^Int.toString (length l) ^ ")") 191 192(*---------------------------------------------------------------------------*) 193(* Prove a theorem for "deep" case analysis on a term with an (iterated) *) 194(* product type. *) 195(* *) 196(* tupleCases ["a", "b", "c"] (v : ty1 # ty2 # ty3) = *) 197(* |- !v. ?a b c. v = (a,b,c) *) 198(*---------------------------------------------------------------------------*) 199 200 201val rename = (* create names for underscored inputs *) 202 let val prefix = "_gv" 203 fun num2name i = prefix^Int.toString i 204 in fn slist => 205 let val num_stream = Portable.make_counter{init=0,inc=1} 206 fun gname() = num2name(num_stream()) 207 fun transform s = if mem s ["_","-"] then gname() else s 208 in map transform slist 209 end 210 end 211 212fun tupleCases names0 v = 213 let val pthm = TypeBasePure.nchotomy_of 214 (Option.valOf (TypeBase.read{Thy="pair",Tyop="prod"})) 215 val names = rename names0 216 val (vname,vty) = dest_var v 217 val tys = strip_prod vty 218 val vars = Lib.map2 (curry mk_var) names tys 219 fun tmpvar_types 0 ty = [ty] 220 | tmpvar_types n ty = 221 case dest_thy_type ty 222 of {Thy="pair",Tyop="prod",Args=[ty1,ty2]} => ty::tmpvar_types (n-1) ty2 223 | otherwise => [ty] 224 val tmp_vars = map genvar (tl (tmpvar_types (length tys - 2) vty)) 225 val left_vars = List.take (vars,length vars - 2) 226 val last2_vars = listpair(List.drop (vars,length vars - 2)) 227 val rpairs = zip left_vars tmp_vars @ [last2_vars] 228 val rpair_tms = map mk_pair rpairs 229 val eqns = map2 (curry mk_eq) (v::tmp_vars) rpair_tms 230 val thlist = map ASSUME eqns 231 val thm = REWRITE_RULE (tl thlist) (hd thlist) 232 fun step eqn th = 233 let val th1 = LEFT_EXISTS_INTRO eqn th 234 val V = free_vars_lr (rhs eqn) 235 val th2 = DISCH (list_mk_exists(V,eqn)) th1 236 val th3 = ISPEC (lhs eqn) pthm 237 in MP th2 th3 238 end 239 in 240 GEN v (itlist step eqns (itlist SIMPLE_EXISTS vars thm)) 241 end 242 handle e => raise wrap_exn "BasicProvers" "primCases_on (tupleCases)" e 243 244 245(*---------------------------------------------------------------------------*) 246(* Set specified existentially quantified names in nchotomy thm. The input *) 247(* thm0 is direct from the TypeBase and therefore not instantiated to the *) 248(* full type being case-split on. This matters for iterated pair case *) 249(* analysis. *) 250(*---------------------------------------------------------------------------*) 251 252fun envar s v = if mem s ["_","-"] then v else mk_var(s,snd(dest_var v)); 253 254fun set_names names ty thm0 = 255 let val vty0 = type_of (fst(dest_forall(concl thm0))) 256 val thm = INST_TYPE (match_type vty0 ty) thm0 257 val tm = concl thm 258 val (v,body) = dest_forall (concl thm) 259 val vty = type_of v 260 val namelists = List.map (String.tokens Char.isSpace) names 261 in 262 if null names then thm 263 else 264 case dest_thy_type vty 265 of {Thy="pair",Tyop="prod",...} => tupleCases (hd namelists) v 266 | otherwise => 267 let val clauses = zip namelists (strip_disj body) 268 fun rename (slist,clause) = 269 let val (bvs,M) = strip_exists clause 270 in if length bvs <> length slist then 271 clause (* fail in such a way that tactic can still be applied. *) 272 else 273 let val vlist = map2 envar slist bvs 274 val theta = map2 (curry (op |->)) bvs vlist 275 val M' = subst theta M 276 in list_mk_exists(vlist,M') 277 end 278 end 279 val tm' = mk_forall(v,list_mk_disj(map rename clauses)) 280 in 281 EQ_MP (Thm.ALPHA tm tm') thm 282 end 283 end 284 handle e => raise wrap_exn "BasicProvers" "primCases_on (set_names)" e 285; 286 287fun primCases_on names st (g as (_,w)) = 288 let 289 val ty = type_of (dest_tmkind st) 290 fun gen() = 291 case TypeBase.fetch ty of 292 SOME facts => [TypeBasePure.nchotomy_of facts] 293 | NONE => let val {Thy,Tyop,...} = dest_thy_type ty 294 in 295 raise ERR "primCases_on" 296 ("No cases theorem found for type: "^ 297 Lib.quote (Thy^"$"^Tyop)) 298 end 299 fun ttac thm = 300 let 301 val thm' = set_names names ty thm 302 in 303 case st of 304 Free M => 305 if is_var M then VAR_INTRO_TAC (ISPEC M thm') else 306 if ty=bool then ASM_CASES_TAC M 307 else TERM_INTRO_TAC (ISPEC M thm') 308 | Bound(V,M) => let val (tac,M') = FREEUP V M g 309 in (tac THEN VAR_INTRO_TAC (ISPEC M' thm')) 310 end 311 | Alien M => if ty=bool then ASM_CASES_TAC M 312 else TERM_INTRO_TAC (ISPEC M thm') 313 end 314 in 315 markerLib.maybe_using gen ttac g 316 end 317 318fun Cases_on qtm g = primCases_on [] (find_subterm qtm g) g 319 handle e => raise wrap_exn "BasicProvers" "Cases_on" e; 320 321fun tmCases_on tm names (g as (asl,w)) = 322 let 323 val fvs = FVL (w::asl) empty_tmset |> HOLset.listItems 324 in 325 primCases_on names (prim_find_subterm fvs tm g) g 326 end handle e => raise wrap_exn "BasicProvers" "tmCases_on" e; 327 328fun namedCases_on qtm names g = 329 primCases_on names (find_subterm qtm g) g 330 handle e => raise wrap_exn "BasicProvers" "namedCases_on" e; 331 332fun Cases (g as (_,w)) = 333 let val (Bvar,_) = with_exn dest_forall w (ERR "Cases" "not a forall") 334 in primCases_on [] (Bound([Bvar],Bvar)) g 335 end 336 handle e => raise wrap_exn "BasicProvers" "Cases" e; 337 338fun namedCases names (g as (_,w)) = 339 let val (Bvar,_) = with_exn dest_forall w (ERR "namedCases" "not a forall") 340 in primCases_on names (Bound([Bvar],Bvar)) g 341 end 342 handle e => raise wrap_exn "BasicProvers" "Cases" e; 343 344(*---------------------------------------------------------------------------*) 345(* Do induction on a given term. *) 346(*---------------------------------------------------------------------------*) 347 348fun primInduct st ind_tac (g as (asl,c)) = 349 let fun ind_non_var V M = 350 let val (tac,M') = FREEUP V M g 351 val Mfrees = free_vars M' 352 val Mfset = HOLset.addList(empty_tmset, Mfrees) 353 fun has_vars tm = 354 not(HOLset.isEmpty 355 (HOLset.intersection(Mfset, FVL [tm] empty_tmset))) 356 val tms = filter has_vars asl 357 val newvar = variant (free_varsl (c::asl)) 358 (mk_var("v",type_of M')) 359 val tm = mk_exists(newvar, mk_eq(newvar, M')) 360 val th = EXISTS(tm,M') (REFL M') 361 in 362 tac 363 THEN MAP_EVERY UNDISCH_TAC tms 364 THEN CHOOSE_THEN MP_TAC th 365 THEN MAP_EVERY ID_SPEC_TAC Mfrees 366 THEN ID_SPEC_TAC newvar 367 THEN ind_tac 368 end 369 in case st 370 of Free M => 371 if is_var M 372 then let val tms = filter (free_in M) asl 373 in (MAP_EVERY UNDISCH_TAC tms THEN ID_SPEC_TAC M THEN ind_tac) g 374 end 375 else ind_non_var [] M g 376 | Bound(V,M) => 377 if is_var M 378 then let val (tac,M') = FREEUP V M g 379 in (tac THEN ID_SPEC_TAC M' THEN ind_tac) g 380 end 381 else ind_non_var V M g 382 | Alien M => 383 if is_var M then raise ERR "primInduct" "Alien variable" 384 else ind_non_var (free_vars M) M g 385 end 386 387(*---------------------------------------------------------------------------*) 388(* Induct on a quoted term. First determine the term, then use that to *) 389(* select the induction theorem to use. There are 3 kinds of induction *) 390(* supported: (1) on datatypes; (2) on inductively defined relations from *) 391(* IndDefLib; (3) on ad-hoc inductive objects (e.g. finite maps, finite sets,*) 392(* and finite multisets). The latter two are similar but differ in where the *) 393(* induction theorem is fetched from (IndDefLib.rule_induction_map or *) 394(* TypeBase.theTypeBase). *) 395(*---------------------------------------------------------------------------*) 396 397fun induct_on_type st ty g = 398 let 399 val is_mutind_thm = is_conj o snd o strip_imp o snd o 400 strip_forall o concl 401 val facts_opt = TypeBase.fetch ty 402 fun gen() = 403 case facts_opt of 404 SOME facts => 405 let 406 in 407 case total TypeBasePure.induction_of facts of 408 NONE => 409 raise ERR "induct_on_type" 410 (String.concat ["Type :",Hol_pp.type_to_string ty, 411 " is registered in the types \ 412 \database, but there is no associated\ 413 \induction theorem"]) 414 | SOME thm => (* now select induction tactic *) [thm] 415 end 416 | NONE => 417 raise ERR "induct_on_type" 418 (String.concat ["Type: ",Hol_pp.type_to_string ty, 419 " is not registered in the types database"]) 420 fun ttac thm = 421 case Option.map TypeBasePure.constructors_of facts_opt of 422 SOME [] => (* not a datatype*) primInduct st (HO_MATCH_MP_TAC thm) 423 | _ => if is_mutind_thm thm then 424 Mutual.MUTUAL_INDUCT_TAC thm 425 else 426 primInduct st (Prim_rec.INDUCT_THEN thm ASSUME_TAC) ORELSE 427 (primInduct st (HO_MATCH_MP_TAC thm) THEN REPEAT CONJ_TAC) 428 in 429 maybe_using gen ttac g 430 end 431 432fun checkind th = 433 (* if the purported theorem fails to pass muster according to this 434 check, we can still let it pass through to the HO_MATCH_MP_TAC, but 435 we won't attempt to be clever with it and call isolate_to_front. *) 436 let 437 val (_, bod) = strip_forall (concl th) 438 val (_, what_matches_a_goal) = dest_imp bod 439 val (gvs, gimp) = strip_forall what_matches_a_goal 440 val (indR, con) = dest_imp gimp 441 in 442 if List.all is_var (#2 (strip_comb indR)) then ALL_TAC 443 else NO_TAC 444 end 445 446fun Induct_on qtm g = 447 let val st = find_subterm qtm g 448 val tm = dest_tmkind st 449 val ty = type_of (dest_tmkind st) 450 val (_, rngty) = strip_fun ty 451 in 452 if rngty = Type.bool then (* inductive relation *) 453 let 454 val (c, _) = strip_comb tm 455 fun mkpat t = 456 let val (d,_) = dom_rng (type_of t) 457 in 458 mkpat (mk_comb(t, genvar d)) 459 end handle HOL_ERR _ => t 460 val pat = mkpat tm 461 open IndDefLib 462 in 463 case Lib.total dest_thy_const c of 464 SOME {Thy,Name,...} => 465 let 466 fun indths() = 467 Binarymap.find (rule_induction_map(), {Thy=Thy,Name=Name}) 468 handle NotFound => [] 469 fun numSchematics th = 470 let 471 val (_,base) = th |> concl |> strip_forall |> #2 |> dest_imp 472 val (vs, c) = strip_forall base 473 val (l, _) = dest_imp c 474 val numargs = l |> strip_comb |> #2 |> length 475 in 476 numargs - length vs 477 end 478 fun tryind th = 479 TRY (checkind th >> isolate_to_front (numSchematics th) pat) >> 480 HO_MATCH_MP_TAC th 481 in 482 markerLib.maybe_using indths tryind ORELSE induct_on_type st ty 483 end g 484 | NONE => induct_on_type st ty g 485 end 486 else 487 induct_on_type st ty g 488 end 489 handle e => raise wrap_exn "BasicProvers" "Induct_on" e; 490 491(*---------------------------------------------------------------------------*) 492(* Induct on leading quantified variable. *) 493(*---------------------------------------------------------------------------*) 494 495fun grab_var M = 496 if is_forall M then fst(dest_forall M) else 497 if is_conj M then fst(dest_forall(fst(dest_conj M))) 498 else raise ERR "Induct" "expected a forall or a conjunction of foralls"; 499 500fun Induct (g as (_,w)) = 501 let val v = grab_var w 502 val (_,ty) = dest_var (grab_var w) 503 in induct_on_type (Bound([v],v)) ty g 504 end 505 handle e => raise wrap_exn "BasicProvers" "Induct" e 506 507 508(*--------------------------------------------------------------------------- 509 Assertional style reasoning 510 ---------------------------------------------------------------------------*) 511 512fun chop_at n frontacc l = 513 if n <= 0 then (List.rev frontacc, l) 514 else 515 case l of 516 [] => raise Fail "chop_at" 517 | (h::t) => chop_at (n-1) (h::frontacc) t 518 519 520infix gTHEN1 (* "gentle" THEN1 : doesn't fail if the tactic for the 521 head goal doesn't completely solve the subgoal. *) 522fun ((tac1:tactic) gTHEN1 (tac2:tactic)) (asl:term list,w:term) = let 523 val (subgoals, vf) = tac1 (asl,w) 524in 525 case subgoals of 526 [] => ([], vf) 527 | (h::hs) => let 528 val (sgoals2, vf2) = tac2 h 529 in 530 (sgoals2 @ hs, 531 (fn thmlist => let 532 val (firstn, back) = chop_at (length sgoals2) [] thmlist 533 in 534 vf (vf2 firstn :: back) 535 end)) 536 end 537end 538 539 540fun eqTRANS new old = let 541 (* allow for possibility that old might be labelled *) 542 open markerLib markerSyntax 543 val s = #1 (dest_label (concl old)) 544in 545 ASSUME_NAMED_TAC s (TRANS (DEST_LABEL old) new) 546end handle HOL_ERR _ => ASSUME_TAC (TRANS old new) 547 548fun is_labeq t = (* term is a possibly labelled equality *) 549 let open markerSyntax 550 in is_eq t orelse is_label t andalso is_eq (#2 (dest_label t)) 551 end; 552 553fun labrhs t = (* term is a possibly labelled equality *) 554 let open markerSyntax 555 in if is_eq t then rhs t else rhs (#2 (dest_label t)) 556 end; 557 558fun qlinenum q = 559 case q |> qbuf.new_buffer |> qbuf.current |> #2 of 560 locn.Loc(locn.LocA(line, _), _) => SOME (line+1) 561 | _ => NONE 562 563fun by0 k (q, tac) (g as (asl,w)) = let 564 val a = trace ("syntax_error", 0) Parse.Absyn q 565 open errormonad 566 val (goal_pt, finisher) = 567 case Lib.total Absyn.dest_eq a of 568 SOME (Absyn.IDENT(_,"_"), r) => 569 if not (null asl) andalso is_labeq (hd asl) then 570 (Parse.absyn_to_preterm 571 (Absyn.mk_eq(Absyn.mk_AQ (labrhs (hd asl)), r)), 572 POP_ASSUM o eqTRANS) 573 else 574 raise ERR "by" "Top assumption must be an equality" 575 | x => (Parse.absyn_to_preterm a, STRIP_ASSUME_TAC) 576 val tm = trace ("show_typecheck_errors", 0) 577 (Preterm.smash 578 (goal_pt >- 579 TermParse.ctxt_preterm_to_term 580 Parse.stdprinters 581 (SOME bool) 582 (free_varsl (w::asl)))) 583 Pretype.Env.empty 584 fun mk_errmsg () = 585 case qlinenum q of 586 SOME l => " on line "^Int.toString l 587 | NONE => ": "^term_to_string tm 588in 589 (SUBGOAL_THEN tm finisher gTHEN1 (tac THEN k)) g 590 handle HOL_ERR _ => 591 raise ERR "by" ("by's tactic failed to prove subgoal"^mk_errmsg()) 592end 593 594val op by = by0 NO_TAC 595val byA = by0 ALL_TAC 596 597fun (q suffices_by tac) g = 598 (Q_TAC SUFF_TAC q gTHEN1 (tac THEN NO_TAC)) g 599 handle e as HOL_ERR {origin_function,...} => 600 if origin_function = "Q_TAC" then raise e 601 else 602 case qlinenum q of 603 SOME l => raise ERR "suffices_by" 604 ("suffices_by's tactic failed to prove goal on \ 605 \line "^Int.toString l) 606 | NONE => raise ERR "suffices_by" 607 "suffices_by's tactic failed to prove goal" 608 609 610 611fun subgoal q = Q.SUBGOAL_THEN q STRIP_ASSUME_TAC 612val sg = subgoal 613 614 615infix on 616fun ((ttac:thm->tactic) on (q:term frag list, tac:tactic)) : tactic = 617 (fn (g as (asl:term list, w:term)) => let 618 val tm = Parse.parse_in_context (free_varsl (w::asl)) q 619 in 620 (SUBGOAL_THEN tm ttac gTHEN1 tac) g 621 end) 622 623(*===========================================================================*) 624(* General-purpose case-splitting tactics. *) 625(*===========================================================================*) 626 627fun case_find_subterm p = 628 let 629 val f = find_term p 630 fun g t = 631 if is_comb t then 632 g (f (rator t)) 633 handle HOL_ERR _ => (g (f (rand t)) handle HOL_ERR _ => t) 634 else if is_abs t then 635 g (f (body t)) handle HOL_ERR _ => t 636 else t 637 in 638 fn t => g (f t) 639 end; 640 641fun first_term f tm = f (find_term (can f) tm); 642 643fun first_subterm f tm = f (case_find_subterm (can f) tm); 644 645(*---------------------------------------------------------------------------*) 646(* If tm is a fully applied conditional or case expression and the *) 647(* scrutinized subterm of tm is free, return the scrutinized subterm. *) 648(* Otherwise raise an exception. *) 649(*---------------------------------------------------------------------------*) 650 651fun scrutinized_and_free_in tm = 652 let fun free_case t = 653 let val (_, examined, _) = TypeBase.dest_case t 654 in if free_in examined tm 655 then examined else raise ERR "free_case" "" 656 end 657 in 658 free_case 659 end; 660 661fun PURE_TOP_CASE_TAC (g as (_, tm)) = 662 let val t = first_term (scrutinized_and_free_in tm) tm 663 in Cases_on `^t` end g; 664 665fun PURE_CASE_TAC (g as (_, tm)) = 666 let val t = first_subterm (scrutinized_and_free_in tm) tm 667 in Cases_on `^t` end g; 668 669fun PURE_FULL_CASE_TAC (g as (asl,w)) = 670 let val tm = list_mk_conj(w::asl) 671 val t = first_subterm (scrutinized_and_free_in tm) tm 672 in Cases_on `^t` end g; 673 674local 675 fun tot f x = f x handle HOL_ERR _ => NONE 676in 677fun case_rws tyi = 678 List.mapPartial I 679 [Lib.total TypeBasePure.case_def_of tyi, 680 tot TypeBasePure.distinct_of tyi, 681 tot TypeBasePure.one_one_of tyi] 682 683fun case_rwlist () = 684 itlist (fn tyi => fn rws => case_rws tyi @ rws) 685 (TypeBase.elts()) []; 686 687(* Add the rewrites into a simpset to avoid re-processing them when 688 * (PURE_CASE_SIMP_CONV rws) is called multiple times by EVERY_CASE_TAC. This 689 * has an order of magnitude speedup on developments with large datatypes *) 690fun PURE_CASE_SIMP_CONV rws = 691 simpLib.SIMP_CONV (boolSimps.bool_ss++simpLib.rewrites rws) [] 692 693fun CASE_SIMP_CONV tm = PURE_CASE_SIMP_CONV (case_rwlist()) tm 694end; 695 696(*---------------------------------------------------------------------------*) 697(* Q: what should CASE_TAC do with literal case expressions? *) 698(*---------------------------------------------------------------------------*) 699 700fun is_refl tm = 701 let val (l,r) = dest_eq tm 702 in aconv l r 703 end handle HOL_ERR _ => false; 704 705fun TRIV_LET_CONV tm = 706 let val (_,a) = boolSyntax.dest_let tm 707 in if is_var a orelse is_const a 708 orelse Literal.is_literal a 709 then (REWR_CONV LET_THM THENC BETA_CONV) tm 710 else NO_CONV tm 711 end; 712 713fun SIMP_OLD_ASSUMS (orig as (asl1,_)) (gl as (asl2,_)) = 714 let val new = op_set_diff aconv asl2 asl1 715 in if null new then ALL_TAC 716 else let val thms = map ASSUME new 717 in MAP_EVERY (Lib.C UNDISCH_THEN (K ALL_TAC)) new THEN 718 RULE_ASSUM_TAC (REWRITE_RULE thms) THEN 719 MAP_EVERY ASSUME_TAC thms 720 end 721 end gl; 722 723fun USE_NEW_ASSUM orig_goal cgoal = 724 (TRY (WEAKEN_TAC is_refl) THEN 725 ASM_REWRITE_TAC[] THEN 726 SIMP_OLD_ASSUMS orig_goal THEN 727 CONV_TAC (DEPTH_CONV TRIV_LET_CONV)) cgoal; 728 729(*---------------------------------------------------------------------------*) 730(* Do a case analysis in the conclusion of the goal, then simplify a bit. *) 731(*---------------------------------------------------------------------------*) 732 733fun CASE_TAC gl = 734 (PURE_CASE_TAC THEN USE_NEW_ASSUM gl THEN CONV_TAC CASE_SIMP_CONV) gl; 735 736fun TOP_CASE_TAC gl = 737 (PURE_TOP_CASE_TAC THEN USE_NEW_ASSUM gl THEN CONV_TAC CASE_SIMP_CONV) gl; 738 739 740(*---------------------------------------------------------------------------*) 741(* Do a case analysis anywhere in the goal, then simplify a bit. *) 742(*---------------------------------------------------------------------------*) 743 744fun FULL_CASE_TAC goal = 745 let val rws = case_rwlist() 746 val case_conv = PURE_CASE_SIMP_CONV rws 747 val asm_rule = Rewrite.REWRITE_RULE rws 748 in PURE_FULL_CASE_TAC THEN USE_NEW_ASSUM goal 749 THEN RULE_ASSUM_TAC asm_rule 750 THEN CONV_TAC case_conv 751 end goal; 752val full_case_tac = FULL_CASE_TAC 753 754(*---------------------------------------------------------------------------*) 755(* Repeatedly do a case analysis anywhere in the goal. Avoids re-computing *) 756(* case info from the TypeBase each time around the loop, so more efficient *) 757(* than REPEAT FULL_CASE_TAC. *) 758(*---------------------------------------------------------------------------*) 759 760fun EVERY_CASE_TAC goal = 761 let val rws = case_rwlist() 762 val case_conv = PURE_CASE_SIMP_CONV rws 763 val asm_rule = BETA_RULE o Rewrite.REWRITE_RULE rws 764 fun tac a = (PURE_FULL_CASE_TAC THEN USE_NEW_ASSUM a THEN 765 RULE_ASSUM_TAC asm_rule THEN 766 CONV_TAC case_conv) a 767 in REPEAT tac 768 end goal; 769val every_case_tac = EVERY_CASE_TAC 770 771(*===========================================================================*) 772(* Rewriters *) 773(*===========================================================================*) 774 775(*---------------------------------------------------------------------------* 776 * When invoked, we know that th is an equality, at least one side of which * 777 * is a variable. * 778 *---------------------------------------------------------------------------*) 779 780 781val var_eq = Tactic.eliminable 782fun ASSUM_TAC f P = first_x_assum (f o assert (P o concl)) 783 784val old_behaviour = ref false 785val tracename = "BasicProvers.var_eq_old" 786val _ = Feedback.register_btrace(tracename, old_behaviour) 787val behaviour_value = get_tracefn tracename 788fun VAR_EQ_TAC (g as (asl,_)) = 789 let 790 val tidy = if behaviour_value() = 1 then ALL_TAC 791 else markerLib.TIDY_ABBREVS 792 in 793 (ASSUM_TAC VSUBST_TAC var_eq THEN tidy) g 794 end 795val var_eq_tac = VAR_EQ_TAC 796 797fun ASSUMS_TAC f P = W (fn (asl,_) => 798 case filter P asl 799 of [] => NO_TAC 800 | assums => MAP_EVERY (fn t => UNDISCH_THEN t f) (List.rev assums)) 801 802fun CONCL_TAC f P = W (fn (_,c) => if P c then f else NO_TAC); 803 804fun LIFT_SIMP ss = STRIP_ASSUME_TAC o simpLib.SIMP_RULE ss [] 805 806local 807 fun DTHEN ttac = fn (asl,w) => 808 let val (ant,conseq) = dest_imp_only w 809 val (gl,prf) = ttac (ASSUME ant) (asl,conseq) 810 in (gl, Thm.DISCH ant o prf) 811 end 812in 813val BOSS_STRIP_TAC = Tactical.FIRST [GEN_TAC,CONJ_TAC, DTHEN STRIP_ASSUME_TAC] 814end; 815 816fun add_simpls tyinfo ss = 817 (ss ++ simpLib.tyi_to_ssdata tyinfo) handle HOL_ERR _ => ss; 818 819fun is_dneg tm = 1 < snd(strip_neg tm); 820 821val notT = mk_neg T 822val notF = mk_neg F; 823 824fun breakable tm = 825 is_exists tm orelse 826 is_conj tm orelse 827 is_disj tm orelse 828 is_dneg tm orelse 829 aconv notT tm orelse 830 aconv notF tm orelse 831 aconv T tm orelse 832 aconv F tm 833 834(* ---------------------------------------------------------------------- 835 LET_ELIM_TAC 836 837 eliminates lets by pulling them up, turning them into universal 838 quantifiers, and eventually moving new abbreviations into the 839 assumption list. 840 ---------------------------------------------------------------------- *) 841 842val let_movement_thms = let 843 open combinTheory 844in 845 ref [o_THM, o_ABS_R, C_ABS_L, C_THM, 846 GEN_literal_case_RAND, GEN_literal_case_RATOR, 847 GEN_LET_RAND, GEN_LET_RATOR, S_ABS_R] 848end 849 850val IMP_CONG' = REWRITE_RULE [GSYM AND_IMP_INTRO] (SPEC_ALL IMP_CONG) 851 852(*---------------------------------------------------------------------------*) 853(* The staging of first two successive calls to SIMP_CONV ensure that the *) 854(* LET_FORALL_ELIM theorem is applied after all the movement is possible. *) 855(*---------------------------------------------------------------------------*) 856 857fun LET_ELIM_TAC goal = 858 let open simpLib pureSimps boolSimps 859 in 860 CONV_TAC 861 (QCHANGED_CONV 862 (SIMP_CONV pure_ss (!let_movement_thms) THENC 863 SIMP_CONV pure_ss (combinTheory.LET_FORALL_ELIM :: 864 combinTheory.literal_case_FORALL_ELIM :: 865 !let_movement_thms) THENC 866 SIMP_CONV (pure_ss ++ ABBREV_ss ++ UNWIND_ss) [Cong IMP_CONG'])) THEN 867 REPEAT BOSS_STRIP_TAC THEN markerLib.REABBREV_TAC 868 end goal 869 870fun new_let_thms thl = let_movement_thms := thl @ !let_movement_thms 871 872 873(*--------------------------------------------------------------------------- 874 STP_TAC (Simplify then Prove) 875 876 The following is a straightforward but quite helpful simplification 877 procedure. It treats the rewrite rules for all declared datatypes as 878 being built-in, so that the user does not have to mention them. 879 880 0. Build a simpset from the given ss and the rewrites coming from 881 any constructors that are found in TypeBase. 882 883 1. Remove all universal quantifiers and break down all conjunctions 884 885 2. Eliminate all "var-equalities" from the assumptions 886 887 3. Simplify the goal with respect to the assumptions and the given 888 simplification set. 889 890 4. Case split on conditionals as much as possible. 891 892 5. Strip as much as possible to the assumptions. 893 894 6. Until there is no change in the complete goal, attempt to do one 895 of the following: 896 897 * eliminate a var-equality 898 899 * break up an equation between constructors in the assumptions 900 901 * break up an equation between constructors in the goal 902 903 * break up conjunctions, disjunctions, existentials, or 904 double negations occurring in the assumptions 905 906 * eliminate occurrences of T (toss it away) and F (prove the goal) 907 in the assumptions 908 909 * eliminate lets in the goal, by lifting into the assumptions as 910 abbreviations (using LET_ELIM_TAC) 911 912 7. Apply the finishing tactic. 913 914 ---------------------------------------------------------------------------*) 915 916fun tyinfol() = TypeBasePure.listItems (TypeBase.theTypeBase()); 917 918fun mkCSET () = 919 let val CSET = (HOLset.empty 920 (inv_img_cmp (fn {Thy,Name,Ty} => (Thy,Name)) 921 (pair_compare(String.compare,String.compare)))) 922 fun add_const (c,CSET) = HOLset.add(CSET, dest_thy_const c) 923 fun add_tyinfo (tyinfo,CSET) = 924 List.foldl add_const CSET (TypeBasePure.constructors_of tyinfo) 925 val CSET = List.foldl add_tyinfo CSET (tyinfol()) 926 fun inCSET t = HOLset.member(CSET, dest_thy_const t) 927 fun constructed tm = 928 let val (lhs,rhs) = dest_eq tm 929 in aconv lhs rhs orelse 930 let val maybe1 = fst(strip_comb lhs) 931 val maybe2 = fst(strip_comb rhs) 932 in is_const maybe1 andalso is_const maybe2 933 andalso 934 inCSET maybe1 andalso inCSET maybe2 935 end 936 end handle HOL_ERR _ => false 937 in 938 Lib.can (find_term constructed) 939 end; 940 941val leave_lets_var = mk_var("__leave_lets_alone__", bool) 942val LEAVE_LETS = ASSUME leave_lets_var 943 944fun PRIM_STP_TAC ss finisher = 945 let val has_constr_eqn = mkCSET () 946 val ASM_SIMP = simpLib.ASM_SIMP_TAC ss [] 947 (* we don't have access to any theorem list that might have been passed 948 to RW_TAC or SRW_TAC at this point, but we can look for the effect of 949 the LEAVE_LETS theorem by attempting to rewrite something that only it 950 should affect; if the simplifier doesn't change the leave_lets_var, 951 then LEAVE_LETS is not part of the ss, so we should do LET_ELIM_TAC, 952 otherwise, we shouldn't. 953 954 Also, if there are no lets about then 955 don't attempt LET_ELIM_TAC at all. This is because LET_ELIM_TAC 956 includes rewrites like |- f o (\x. g x) = \x. f (g x) and these 957 can alter goals that don't have any lets in them at all, possibly 958 against user expectations. A less sledge-hammer implementation of 959 LET_ELIM_TAC might not have this problem... *) 960 val do_lets = (simpLib.SIMP_CONV ss [] leave_lets_var ; false) 961 handle Conv.UNCHANGED => true 962 val LET_ELIM_TAC = 963 if do_lets then 964 (fn g as (_,w) => 965 if can (find_term is_let) w 966 then LET_ELIM_TAC g 967 else NO_TAC g) 968 else NO_TAC 969 in 970 REPEAT (GEN_TAC ORELSE CONJ_TAC) 971 THEN REPEAT VAR_EQ_TAC 972 THEN ASM_SIMP 973 THEN TRY (IF_CASES_TAC THEN REPEAT IF_CASES_TAC THEN ASM_SIMP) 974 THEN REPEAT BOSS_STRIP_TAC 975 THEN REPEAT (CHANGED_TAC 976 (VAR_EQ_TAC 977 ORELSE ASSUMS_TAC (LIFT_SIMP ss) has_constr_eqn 978 ORELSE ASSUM_TAC (LIFT_SIMP ss) breakable 979 ORELSE CONCL_TAC ASM_SIMP has_constr_eqn 980 ORELSE LET_ELIM_TAC)) 981 THEN TRY finisher 982 end 983 984(*--------------------------------------------------------------------------- 985 PRIM_NORM_TAC: preliminary attempt at keeping the goal in a 986 fully constructor-reduced format. The idea is that there should 987 be no equations between constructor terms anywhere in the goal. 988 (This is what PRIM_STP_TAC already does.) 989 990 Also, no conditionals should occur in the resulting goal. 991 This seems to be an expensive test, especially since the work 992 in detecting the conditional is replicated in IF_CASES_TAC. 993 994 Continuing in this light, it seems possible to eliminate all 995 case expressions in the goal, but that hasn't been implemented yet. 996 ---------------------------------------------------------------------------*) 997 998fun splittable w = 999 Lib.can (find_term (fn tm => (is_cond tm orelse TypeBase.is_case tm) 1000 andalso free_in tm w)) w; 1001 1002fun LIFT_SPLIT_SIMP ss simp th = 1003 MP_TAC (simpLib.SIMP_RULE ss [] th) THEN CASE_TAC THEN simp THEN 1004 REPEAT BOSS_STRIP_TAC 1005 1006fun SPLIT_SIMP simp = TRY (IF_CASES_TAC ORELSE CASE_TAC) THEN simp ; 1007 1008fun PRIM_NORM_TAC ss = 1009 let val has_constr_eqn = mkCSET() 1010 val ASM_SIMP = simpLib.ASM_SIMP_TAC ss [] 1011 in 1012 REPEAT (GEN_TAC ORELSE CONJ_TAC) 1013 THEN REPEAT VAR_EQ_TAC 1014 THEN ASM_SIMP 1015 THEN TRY (IF_CASES_TAC THEN REPEAT IF_CASES_TAC THEN ASM_SIMP) 1016 THEN REPEAT BOSS_STRIP_TAC 1017 THEN REPEAT (CHANGED_TAC 1018 (VAR_EQ_TAC 1019 ORELSE ASSUMS_TAC (LIFT_SIMP ss) has_constr_eqn 1020 ORELSE ASSUM_TAC (LIFT_SIMP ss) breakable 1021 ORELSE CONCL_TAC ASM_SIMP has_constr_eqn 1022 ORELSE ASSUM_TAC (LIFT_SPLIT_SIMP ss ASM_SIMP) splittable 1023 ORELSE CONCL_TAC (SPLIT_SIMP ASM_SIMP) splittable 1024 ORELSE LET_ELIM_TAC)) 1025 end 1026 1027 1028(*--------------------------------------------------------------------------- 1029 Adding simplification sets in for all datatypes each time 1030 STP_TAC is invoked can be slow. In such cases, use 1031 PRIM_STP tac instead. 1032 ---------------------------------------------------------------------------*) 1033 1034fun STP_TAC ss finisher 1035 = PRIM_STP_TAC (rev_itlist add_simpls (tyinfol()) ss) finisher 1036 1037fun RW_TAC ss thl g = markerLib.ABBRS_THEN 1038 (markerLib.mk_require_tac 1039 (fn thl => STP_TAC (ss && thl) NO_TAC)) 1040 thl 1041 g 1042val rw_tac = RW_TAC 1043 1044fun NORM_TAC ss thl g = 1045 markerLib.ABBRS_THEN 1046 (fn thl => PRIM_NORM_TAC (rev_itlist add_simpls (tyinfol()) (ss && thl))) 1047 thl 1048 g 1049 1050val bool_ss = boolSimps.bool_ss; 1051 1052(*--------------------------------------------------------------------------- 1053 Stateful version of RW_TAC: doesn't load the constructor 1054 simplifications into the simpset at each invocation, but 1055 just when a datatype is declared. 1056 ---------------------------------------------------------------------------*) 1057 1058datatype srw_update = ADD_SSFRAG of simpLib.ssfrag | REMOVE_RWT of string 1059type srw_state = simpset * bool * srw_update list 1060 (* simpset, initialised-flag, update list (most recent first), ssfrag *) 1061 1062val initial_simpset = bool_ss ++ combinSimps.COMBIN_ss 1063 ++ boolSimps.NORMEQ_ss 1064 ++ boolSimps.ABBREV_ss 1065 ++ boolSimps.LABEL_CONG_ss 1066 1067fun ssf1 nth = simpLib.empty_ssfrag |> simpLib.add_named_rwt nth 1068 1069val state0 : srw_state = (initial_simpset, false, []) 1070fun apply_delta d ((sset,initp,upds):srw_state) : srw_state = 1071 case d of 1072 ThmSetData.ADD nth => 1073 (sset ++ ssf1 nth, true, []) 1074 | ThmSetData.REMOVE s => (sset -* [s], true, []) 1075 1076fun apply_to_global d (st as (sset,initp,upds):srw_state) : srw_state = 1077 if not initp then 1078 case d of 1079 ThmSetData.ADD nth => 1080 let 1081 open simpLib 1082 val upds' = 1083 case upds of 1084 ADD_SSFRAG ssf :: rest => 1085 ADD_SSFRAG (add_named_rwt nth ssf) :: rest 1086 | _ => ADD_SSFRAG (ssf1 nth) :: upds 1087 in 1088 (sset, initp, upds') 1089 end 1090 | ThmSetData.REMOVE s => (sset, initp, REMOVE_RWT s :: upds) 1091 else 1092 apply_delta d st 1093 1094fun apply_srw_update (ADD_SSFRAG ssf, ss) = ss ++ ssf 1095 | apply_srw_update (REMOVE_RWT n, ss) = ss -* [n] 1096 1097fun init_state (st as (sset,initp,upds)) = 1098 if initp then st 1099 else 1100 let fun init() = 1101 (List.foldl apply_srw_update sset (List.rev upds) 1102 |> rev_itlist add_simpls (tyinfol()), 1103 true, []) 1104 in 1105 HOL_PROGRESS_MESG ("Initialising SRW simpset ... ", "done") init () 1106 end 1107fun opt_partition f g ls = 1108 let 1109 fun recurse As Bs ls = 1110 case ls of 1111 [] => (List.rev As, List.rev Bs) 1112 | h::t => (case f h of 1113 SOME a => recurse (a::As) Bs t 1114 | NONE => (case g h of 1115 SOME b => recurse As (b::Bs) t 1116 | NONE => recurse As Bs t)) 1117 in 1118 recurse [] [] ls 1119 end 1120 1121fun finaliser {thyname} deltas (sset,initp,upds) = 1122 let 1123 fun toNamedAdd (ThmSetData.ADD p) = SOME p | toNamedAdd _ = NONE 1124 fun toRM (ThmSetData.REMOVE s) = SOME s | toRM _ = NONE 1125 val (adds,rms) = opt_partition toNamedAdd toRM deltas 1126 val ssfrag = simpLib.named_rewrites_with_names thyname (List.rev adds) 1127 (* List.rev here preserves old behaviour wrt to the way theorems were 1128 added to the global simpset; it will only make a difference when 1129 overall rewrite system is not confluent *) 1130 val new_upds = ADD_SSFRAG ssfrag :: map REMOVE_RWT rms 1131 in 1132 if initp then (List.foldl apply_srw_update sset new_upds, true, []) 1133 else (sset, false, List.revAppend(new_upds, upds)) 1134 end 1135 1136val adresult as {DB,get_global_value,record_delta,update_global_value,...} = 1137 ThmSetData.export_with_ancestry { 1138 delta_ops = { 1139 apply_delta = apply_delta, 1140 apply_to_global = apply_to_global, 1141 thy_finaliser = SOME finaliser, 1142 initial_value = state0, uptodate_delta = K true 1143 }, 1144 settype = "simp" 1145 }; 1146val get_deltas = #get_deltas adresult 1147fun merge_simpsets ps = 1148 case Option.map (#1 o quiet_messages init_state) (#merge adresult ps) of 1149 NONE => simpLib.empty_ss 1150 | SOME sset => sset 1151 1152fun augment_srw_ss0 ssdl ((sset, initp, upds):srw_state):srw_state = 1153 if initp then (foldl (fn (ssd,ss) => ss ++ ssd) sset ssdl, true, []) 1154 else 1155 (sset, false, List.revAppend(map ADD_SSFRAG ssdl, upds)) 1156val augment_srw_ss = update_global_value o augment_srw_ss0 1157 1158fun diminish_srw_ss0 names st0 = 1159 let val st' as (sset, _, _) = init_state st0 1160 in 1161 (simpLib.remove_ssfrags names sset, true, []) 1162 end 1163val diminish_srw_ss = update_global_value o diminish_srw_ss0 1164 1165fun temp_delsimps0 names (sset, initp, upds) = 1166 if initp then (sset -* names, true, []) 1167 else 1168 (sset, false, List.revAppend (map REMOVE_RWT names, upds)) 1169val temp_delsimps = update_global_value o temp_delsimps0; 1170 1171fun tyi_update tyi sset = sset ++ simpLib.tyi_to_ssdata tyi 1172fun update_fn tyi = 1173 augment_srw_ss ([simpLib.tyi_to_ssdata tyi] handle HOL_ERR _ => []) 1174fun augment_with_typebase tyb = 1175 rev_itlist tyi_update $ TypeBasePure.listItems tyb 1176 1177val () = TypeBase.register_update_fn (fn tyi => (update_fn tyi; tyi)) 1178 1179fun srw_ss () = 1180 (update_global_value init_state; 1181 #1 (get_global_value())) 1182 1183val update_log = 1184 Sref.new (Symtab.empty : (simpset -> simpset) list Symtab.table) 1185fun ap13 f (x,y,z) = (f x, y, z) 1186fun logged_update {thyname} f = 1187 (update_global_value (ap13 f); 1188 Sref.update update_log (Symtab.cons_list (thyname,f))) 1189 1190fun logged_addfrags thy fgs = 1191 List.app (fn f => logged_update thy (fn s => s ++ f)) fgs 1192 1193fun apply_logged_updates {theories} simpset = 1194 let 1195 open Binaryset 1196 val allancs = List.foldl 1197 (fn (thy,s) => addList (add(s,thy), ancestry thy)) 1198 (empty String.compare) 1199 theories 1200 val G = SymGraph.make (map (fn s => ((s,()), Theory.parents s)) 1201 (Binaryset.listItems allancs)) 1202 val sorted_thys = List.rev (SymGraph.topological_order G) 1203 fun app1 thy simpset = 1204 case Symtab.lookup (Sref.value update_log) thy of 1205 NONE => simpset 1206 | SOME fs => List.foldr (fn (f,ss) => f ss) simpset fs 1207 in 1208 rev_itlist app1 sorted_thys simpset 1209 end 1210 1211fun do_logged_updates thys = 1212 update_global_value (ap13 (apply_logged_updates thys) o init_state) 1213 1214fun option_fold f NONE x = x 1215 | option_fold f (SOME a) x = f a x 1216 1217fun SRW_TAC ssdl thl g = let 1218 val ss = foldl (fn (ssd, ss) => ss ++ ssd) (srw_ss()) ssdl 1219in 1220 markerLib.ABBRS_THEN 1221 (markerLib.mk_require_tac (fn thl => PRIM_STP_TAC (ss && thl) NO_TAC)) thl 1222end g; 1223val srw_tac = SRW_TAC 1224 1225fun export_rewrites slist = 1226 let val ds = map ThmSetData.mk_add slist 1227 in 1228 List.app record_delta ds; 1229 update_global_value (rev_itlist apply_to_global ds) 1230 end 1231 1232fun delsimps names = 1233 (List.app (record_delta o ThmSetData.REMOVE) names; 1234 temp_delsimps names) 1235 1236fun thy_ssfrag s = 1237 get_deltas {thyname=s} 1238 |> ThmSetData.added_thms 1239 |> simpLib.rewrites 1240 |> simpLib.name_ss s 1241 1242fun thy_simpset s = Option.map (#1 o init_state) (DB {thyname=s}) 1243 1244fun temp_set_simpset_ancestry sl = 1245 case #merge adresult sl of 1246 NONE => HOL_WARNING "BasicProvers" "temp_set_simpset_ancestry" 1247 "Merge of parental values produces no value; \ 1248 \nothing done" 1249 | SOME v => update_global_value (K v) 1250 1251fun set_simpset_ancestry sl = 1252 case #set_parents adresult sl of 1253 NONE => HOL_WARNING "BasicProvers" "set_simpset_ancestry" 1254 "Merge of parental values produces no value; \ 1255 \nothing done" 1256 | SOME _ => () 1257 1258fun temp_setsimpset ss = update_global_value (K (ss, true, [])) 1259val simpset_state = get_global_value 1260fun recreate_sset_at_parentage ps = 1261 ps |> merge_simpsets 1262 |> option_fold augment_with_typebase (TypeBase.merge_typebases ps) 1263 |> apply_logged_updates {theories = ps} 1264 |> temp_setsimpset 1265 1266 1267end 1268