1structure markerLib :> markerLib = 2struct 3 4open HolKernel boolLib markerTheory markerSyntax; 5 6val ERR = mk_HOL_ERR "markerLib" ; 7 8(*---------------------------------------------------------------------------*) 9(* Support for "short-term markers". *) 10(*---------------------------------------------------------------------------*) 11 12val stmark_term = REWR_CONV (GSYM stmarker_def) 13 14fun stmark_conjunct P tm = let 15in 16 if is_conj tm then 17 LAND_CONV (stmark_conjunct P) ORELSEC RAND_CONV (stmark_conjunct P) 18 else if P tm then stmark_term 19 else NO_CONV 20end tm 21 22fun stmark_disjunct P tm = let 23in 24 if is_disj tm then 25 LAND_CONV (stmark_disjunct P) ORELSEC RAND_CONV (stmark_disjunct P) 26 else if P tm then stmark_term 27 else NO_CONV 28end tm 29 30fun is_stmarked t = same_const stmarker_tm (rator t) handle HOL_ERR _ => false 31 32val [comm, assoc, commassoc] = CONJUNCTS (SPEC_ALL markerTheory.move_left_conj) 33 34fun move_stmarked_conj_left tm = let 35in 36 if is_stmarked tm then ALL_CONV 37 else if is_conj tm then 38 (LAND_CONV move_stmarked_conj_left THENC TRY_CONV (REWR_CONV assoc)) 39 ORELSEC 40 (RAND_CONV move_stmarked_conj_left THENC 41 (REWR_CONV commassoc ORELSEC REWR_CONV comm)) 42 else NO_CONV 43end tm 44 45val move_stmarked_conj_left = 46 move_stmarked_conj_left THENC 47 (LAND_CONV (REWR_CONV stmarker_def) ORELSEC REWR_CONV stmarker_def) 48 49val move_stmarked_conj_right = 50 PURE_REWRITE_CONV [move_right_conj] THENC 51 (RAND_CONV (REWR_CONV stmarker_def) ORELSEC REWR_CONV stmarker_def) 52val move_stmarked_disj_left = 53 PURE_REWRITE_CONV [move_left_disj] THENC 54 (LAND_CONV (REWR_CONV stmarker_def) ORELSEC REWR_CONV stmarker_def) 55 56val move_stmarked_disj_right = 57 PURE_REWRITE_CONV [move_right_conj] THENC 58 (RAND_CONV (REWR_CONV stmarker_def) ORELSEC REWR_CONV stmarker_def) 59 60fun move_conj_left P = stmark_conjunct P THENC move_stmarked_conj_left 61fun move_conj_right P = stmark_conjunct P THENC move_stmarked_conj_right 62fun move_disj_left P = stmark_disjunct P THENC move_stmarked_disj_left 63fun move_disj_right P = stmark_disjunct P THENC move_stmarked_disj_right 64 65(*---------------------------------------------------------------------------*) 66(* Dealing with simplifier directives encoded as tags on theorems. *) 67(*---------------------------------------------------------------------------*) 68 69fun AC th1 th2 = 70 EQ_MP (SYM (SPECL [concl th1, concl th2] markerTheory.AC_DEF)) 71 (CONJ th1 th2); 72 73fun unAC th = let val th1 = PURE_REWRITE_RULE [AC_DEF] th 74 in (CONJUNCT1 th1, CONJUNCT2 th1) 75 end; 76 77fun Cong th = EQ_MP (SYM(SPEC (concl th) markerTheory.Cong_def)) th; 78 79fun unCong th = PURE_REWRITE_RULE [Cong_def] th; 80 81fun Excl nm = 82 let val v = mk_var(nm, alpha) 83 in 84 EQT_ELIM (SPEC v markerTheory.Exclude_def) 85 end 86 87fun mk_marker_const nm = prim_mk_const{Thy = "marker", Name = nm} 88val Excl_t = mk_marker_const "Exclude" 89fun destExcl th = 90 let val c = concl th 91 val f = rator c 92 in 93 if same_const Excl_t f then SOME (#1 (dest_var (rand c))) 94 else NONE 95 end handle HOL_ERR _ => NONE 96 97val Req0_t = mk_marker_const "Req0" 98val Req0_th = EQT_ELIM markerTheory.Req0_def 99val ReqD_t = mk_marker_const "ReqD" 100val ReqD_th = EQT_ELIM markerTheory.ReqD_def 101val mk_Req0 = ADD_ASSUM Req0_t 102val mk_ReqD = ADD_ASSUM ReqD_t 103 104fun dest_Req0 th = 105 if HOLset.member(hypset th, Req0_t) then SOME (PROVE_HYP Req0_th th) 106 else NONE 107fun dest_ReqD th = 108 if HOLset.member(hypset th, ReqD_t) then SOME (PROVE_HYP ReqD_th th) 109 else NONE 110 111fun req0_modify tac th = 112 case dest_Req0 th of 113 NONE => (tac,th) 114 | SOME th => (Ho_Rewrite.REQUIRE0_TAC th o tac, th) 115fun reqD_modify tac th = 116 case dest_ReqD th of 117 NONE => (tac,th) 118 | SOME th => (Ho_Rewrite.REQUIRE_DECREASE_TAC th o tac, th) 119 120fun mk_require_tac tac thl = 121 let 122 fun recurse (accths,acctac) ths = 123 case ths of 124 [] => acctac (List.rev accths) 125 | th::rest => 126 let 127 val (tac,th) = req0_modify tac th 128 val (tac,th) = reqD_modify tac th 129 in 130 recurse (th::accths,tac) rest 131 end 132 in 133 recurse ([], tac) thl 134 end 135 136(*---------------------------------------------------------------------------*) 137(* Support for abbreviations. *) 138(*---------------------------------------------------------------------------*) 139 140val DeAbbrev = CONV_RULE (REWR_CONV Abbrev_def) 141 142fun Abbrev_wrap eqth = 143 EQ_MP (SYM (Thm.SPEC (concl eqth) Abbrev_def)) eqth 144 145fun ABB l r = 146 CHOOSE_THEN (fn th => SUBST_ALL_TAC th THEN ASSUME_TAC (Abbrev_wrap(SYM th))) 147 (Thm.EXISTS(mk_exists(l, mk_eq(r, l)), r) (Thm.REFL r)); 148 149fun ABBREV_TAC eq = let val (l,r) = dest_eq eq in ABB l r end; 150 151local 152 val match_var_or_const = ref true 153in 154 val () = Feedback.register_btrace 155 ("PAT_ABBREV_TAC: match var/const", match_var_or_const) 156 157 fun PAT_ABBREV_TAC fv_set eq (g as (asl, w)) = 158 let 159 open HOLset 160 val (l, r) = dest_eq eq 161 val rvs = FVL [r] empty_tmset 162 val l' = gen_variant Parse.is_constname "" 163 (listItems(union(fv_set, rvs))) l 164 fun matchr t = 165 case raw_match [] fv_set r t ([],[]) of 166 ((tmsub, _), (tysub, _)) => (tmsub, tysub) 167 fun finder (bvs, t) = 168 case List.find (fn v => HOLset.member(rvs, v)) bvs of 169 SOME _ => NONE 170 | NONE => 171 if (is_var t orelse is_const t) andalso not (!match_var_or_const) 172 then NONE 173 else 174 case Lib.total matchr t of 175 NONE => NONE 176 | SOME (tmsub, tysub) => 177 let 178 open HOLset 179 val bv_set = addList(empty_tmset, bvs) 180 fun badt t = 181 not (isEmpty (intersection (FVL [t] empty_tmset, 182 bv_set))) 183 in 184 case List.find (fn {redex,residue=t} => badt t) tmsub of 185 NONE => SOME(t, tysub) 186 | SOME _ => NONE 187 end 188 in 189 case gen_find_term finder w of 190 NONE => raise ERR "PAT_ABBREV_TAC" "No matching term found" 191 | SOME (t, tysub) => ABB (Term.inst tysub l') t g 192 end 193end 194 195fun fixed_tyvars ctxt pattern = 196 Lib.U (map type_vars_in_term (op_intersect aconv ctxt (free_vars pattern))) 197 198fun ABB' {redex=l,residue=r} = ABB l r 199 200val safe_inst_cmp = let 201 fun img {redex,residue} = 202 (term_size residue, (residue, #1 (dest_var redex) handle HOL_ERR _ => "")) 203 val cmp = pair_compare 204 (flip_cmp Int.compare, pair_compare (Term.compare, String.compare)) 205in 206 inv_img_cmp img cmp 207end 208val safe_inst_sort = 209 List.filter 210 (fn {redex,residue} => String.sub(#1 (dest_var redex),0) <> #"_") o 211 Listsort.sort safe_inst_cmp 212 213fun MATCH_ABBREV_TAC fv_set pattern (g as (asl, w)) = let 214 val ctxt = HOLset.listItems fv_set 215 val (tminst,_) = match_terml (fixed_tyvars ctxt pattern) fv_set pattern w 216in 217 MAP_EVERY ABB' (safe_inst_sort tminst) g 218end 219 220fun MATCH_ASSUM_ABBREV_TAC fv_set pattern (g as (asl, w)) = let 221 val ctxt = HOLset.listItems fv_set 222 val fixed = fixed_tyvars ctxt pattern 223 fun find [] = raise ERR "MATCH_ASSUM_ABBREV_TAC" "No matching assumption found" 224 | find (asm::tl) = 225 case total (match_terml fixed fv_set pattern) asm of 226 NONE => find tl 227 | SOME (tminst,_) => MAP_EVERY ABB' (safe_inst_sort tminst) g 228 handle HOL_ERR e => find tl 229in find asl end 230 231fun HO_MATCH_ABBREV_TAC fv_set pattern (gl as (asl,w)) = 232 let val ctxt = HOLset.listItems fv_set 233 val (tminst, tyinst) = ho_match_term (fixed_tyvars ctxt pattern) fv_set pattern w 234 val unbeta_goal = 235 Tactical.default_prover(mk_eq(w, subst tminst (inst tyinst pattern)), 236 BETA_TAC THEN REFL_TAC) 237in 238 CONV_TAC (K unbeta_goal) THEN MAP_EVERY ABB' (safe_inst_sort tminst) 239end gl; 240 241fun UNABBREV_TAC s = 242 FIRST_X_ASSUM(SUBST_ALL_TAC o 243 assert(equal s o fst o dest_var o lhs o concl) o 244 DeAbbrev); 245 246val UNABBREV_ALL_TAC = 247 let fun ttac th0 = 248 let val th = DeAbbrev th0 249 in SUBST_ALL_TAC th ORELSE ASSUME_TAC th 250 end 251 in 252 REPEAT (FIRST_X_ASSUM ttac) 253end 254 255fun RM_ABBREV_TAC s = 256 FIRST_X_ASSUM (K ALL_TAC o 257 assert(equal s o fst o dest_var o lhs o concl) o 258 DeAbbrev) 259 260val RM_ALL_ABBREVS_TAC = REPEAT (FIRST_X_ASSUM (K ALL_TAC o DeAbbrev)) 261 262(*---------------------------------------------------------------------------*) 263(* Given an abbreviation context, and a goal with possibly more abbrevs, *) 264(* reabbreviate the goal. *) 265(*---------------------------------------------------------------------------*) 266 267fun CNTXT_REABBREV_TAC abbrevs (gl as (asl,_)) = 268 let val abbrevs' = filter is_abbrev asl 269 val ordered_abbrevs = topsort compare_abbrev (abbrevs@abbrevs') 270 val lrs = map (dest_eq o rand) ordered_abbrevs 271 in UNABBREV_ALL_TAC THEN MAP_EVERY (uncurry ABB) lrs 272 end gl; 273 274(*---------------------------------------------------------------------------*) 275(* Execute a tactic in a goal with no abbreviations, then restore the *) 276(* abbrevs, also taking account of any new abbreviations that came in from *) 277(* the application of the tactic. *) 278(*---------------------------------------------------------------------------*) 279 280fun WITHOUT_ABBREVS tac (gl as (asl,_)) = 281 let val abbrevs = filter is_abbrev asl 282 in UNABBREV_ALL_TAC THEN tac THEN CNTXT_REABBREV_TAC abbrevs 283 end gl; 284 285(*---------------------------------------------------------------------------*) 286(* REABBREV_TAC ought to be called after BasicProvers.LET_ELIM_TAC, which *) 287(* introduces an abbrev, but doesn't propagate the abbrev. to the other *) 288(* assumptions. This has been done in basicProof/BasicProvers. *) 289(*---------------------------------------------------------------------------*) 290 291val REABBREV_TAC = WITHOUT_ABBREVS ALL_TAC; 292 293(*---------------------------------------------------------------------------*) 294(* ABBRS_THEN: expand specified abbreviations before applying a tactic. *) 295(* Typically, the abbreviations are designated in the thm list of a *) 296(* simplification tactic thusly: *) 297(* *) 298(* ASM_SIMP_TAC ss [ ..., Abbr`m`, ... ] *) 299(* *) 300(* which says to find and expand the abbreviation *) 301(* *) 302(* Abbrev (m = tm) *) 303(* *) 304(* in the assumptions of the goal before proceeding with simplification. *) 305(*---------------------------------------------------------------------------*) 306 307fun ABBRS_THEN thl_tac thl = 308 let val (abbrs, rest) = List.partition is_abbr thl 309 in 310 MAP_EVERY (UNABBREV_TAC o dest_abbr) abbrs THEN thl_tac rest 311 end 312 313val MK_ABBREVS_OLDSTYLE = 314 RULE_ASSUM_TAC (fn th => (th |> DeAbbrev |> SYM) handle HOL_ERR _ => th) 315 316(* ---------------------------------------------------------------------- 317 Abbreviation Tidying 318 319 Abbreviations should be of the form 320 321 Abbrev(v = e) 322 323 with v a variable. The tidying process eliminates assumptions that 324 have Abbrev present at the top with an argument that is not of the 325 right shape. As simplification sees abbreviation equations as 326 rewrites of the form e = v (replacing occurrences of e with the 327 abbreviation), the tidying process will flip equations to keep 328 this "orientation". 329 ---------------------------------------------------------------------- *) 330 331fun TIDY_ABBREV_CONV t = 332 if is_malformed_abbrev t then 333 (REWR_CONV markerTheory.Abbrev_def THENC TRY_CONV (REWR_CONV EQ_SYM_EQ)) t 334 else ALL_CONV t 335val TIDY_ABBREV_RULE = CONV_RULE TIDY_ABBREV_CONV 336val TIDY_ABBREVS = RULE_ASSUM_TAC TIDY_ABBREV_RULE 337 338 339(*---------------------------------------------------------------------------*) 340(* Support for user-defined labels. *) 341(*---------------------------------------------------------------------------*) 342 343val DEST_LABEL_CONV = REWR_CONV label_def 344 345val DEST_LABELS_CONV = PURE_REWRITE_CONV [label_def] 346 347val DEST_LABEL = CONV_RULE DEST_LABEL_CONV 348val DEST_LABELS = CONV_RULE DEST_LABELS_CONV 349 350val DEST_LABELS_TAC = CONV_TAC DEST_LABELS_CONV THEN RULE_ASSUM_TAC DEST_LABELS 351 352 353fun MK_LABEL(s, th) = EQ_MP (SYM (SPECL [mk_label_var s, concl th] label_def)) th 354 355fun ASSUME_NAMED_TAC s bth : tactic = ASSUME_TAC (MK_LABEL(s, bth)) 356 357(*---------------------------------------------------------------------------*) 358(* Given an LB encoded label reference, finds a corresponding term in the *) 359(* assumption list. *) 360(*---------------------------------------------------------------------------*) 361 362fun find_labelled_assumption labelth asl = let 363 val labname = dest_label_ref labelth 364 fun matching_asm t = 365 (#1 (dest_label t) = labname) handle HOL_ERR _ => false 366in 367 case List.find matching_asm asl of 368 SOME t => DEST_LABEL (ASSUME t) 369 | NONE => raise ERR "find_labelled_assumption" 370 ("No assumption with label \""^labname^"\"") 371end; 372 373fun LABEL_ASSUM s ttac (asl, w) = 374 ttac (find_labelled_assumption (L s) asl) (asl, w) 375 376(*---------------------------------------------------------------------------*) 377(* LABEL_X_ASSUM is almost identical to LABEL_ASSUM. But it is not applied *) 378(* to the goal, but to a goal with the labelled assumption removed. *) 379(*---------------------------------------------------------------------------*) 380 381fun name_assoc s [] = NONE 382 | name_assoc s (tm::rst) = 383 case total dest_label tm 384 of NONE => name_assoc s rst 385 | SOME (n,tm') => if s=n then SOME(tm,(n,tm')) 386 else name_assoc s rst; 387 388fun LABEL_X_ASSUM s ttac : tactic = 389 fn (asl,w) => 390 case name_assoc s asl 391 of NONE => raise ERR "LABEL_X_ASSUM" 392 ("Can't find term named by "^Lib.quote s^" in assumptions") 393 | SOME(named_tm,_) 394 => ttac (DEST_LABEL(ASSUME named_tm)) 395 (op_set_diff aconv asl [named_tm],w); 396 397(*---------------------------------------------------------------------------*) 398(* Given a list of theorems thl and a list of assumptions asl, return a list *) 399(* consisting of (a) the elements of thl that are not just tags signifying *) 400(* which elements of asl to assume; (b) the non-labelled elements of asl *) 401(* (just ASSUME'd); (c) the elements of asl having labels obtained by *) 402(* looking at the dummy theorems in thl of the form |- label = label. This *) 403(* means that some labelled elements of asl might be excluded. *) 404(*---------------------------------------------------------------------------*) 405 406fun LLABEL_RESOLVE thl asl = let 407 val (labelled_asms, other_asms) = List.partition is_label asl 408 val (labelrefs, realths) = List.partition is_label_ref thl 409 val wanted_lab_assums = 410 map (fn lb => find_labelled_assumption lb labelled_asms) labelrefs 411in 412 map ASSUME other_asms @ wanted_lab_assums @ realths 413end 414 415fun matching_asm th t = 416 let 417 val labname = dest_label_ref th 418 in 419 #1 (dest_label t) = labname 420 end handle HOL_ERR _ => false 421 422fun has_label_from lrefs t = 423 List.exists (C matching_asm t) lrefs 424 425fun LLABEL_RES_THEN thltac thl (g as (asl,w)) = 426 let 427 val (labelrefs, realths) = List.partition is_label_ref thl 428 val (wanted_labelled_asms, rest) = 429 List.partition (has_label_from labelrefs) asl 430 in 431 thltac (map (DEST_LABEL o ASSUME) wanted_labelled_asms @ realths) g 432 end 433 434 435fun LABEL_RESOLVE th (asl, w) = hd (LLABEL_RESOLVE [th] asl) 436 437(* ---------------------------------------------------------------------- 438 using : tactic * thm -> tactic 439 440 using th tac stashes theorem th in the goal so that tactic tac can 441 use it if desired. If the tactic terminates, the stashed theorem 442 is removed. 443 444 Stashing is done by adding an assumption encoding the name of the 445 theorem to the assumption list. This will cause mess-ups if you 446 attempt something like 447 448 pop_assum foo using bar 449 450 so, don't do that. 451 452 This can be nested, with multiple theorems stashed at once; the 453 cleanup looks for the exact using theorem that it stashed when it 454 removes it and does so with UNDISCH_THEN. So, if there are 455 multiples of the same name, the most recent will be taken. 456 457 ---------------------------------------------------------------------- *) 458 459fun tac using th = 460 let 461 val uth = MK_USING th 462 in 463 ASSUME_TAC uth >> 464 tac >> 465 UNDISCH_THEN (concl uth) (K ALL_TAC) 466 end 467 468fun usingA tac th = tac using th 469 470fun loc2thm loc = 471 case loc of 472 DB.Local s => (valOf (DB.local_thm s) 473 handle Option => raise ERR "loc2thm" "No such theorem") 474 | DB.Stored {Name,Thy} => 475 DB.fetch Thy Name 476 handle HOL_ERR _ => raise ERR "loc2thm" "No such theorem" 477 478 479fun maybe_using gen ttac (g as (asl,w)) = 480 case asl of 481 h::_ => if is_using h then ttac (DEST_USING (ASSUME h)) g 482 else MAP_FIRST ttac (gen()) g 483 | _ => MAP_FIRST ttac (gen()) g 484 485end 486