1structure OldAbbrevTactics :> OldAbbrevTactics = 2struct 3 4open HolKernel boolLib 5 6fun ABB l r = 7 CHOOSE_THEN (fn th => SUBST_ALL_TAC th THEN ASSUME_TAC th) 8 (Thm.EXISTS(mk_exists(l, mk_eq(r, l)), r) (Thm.REFL r)) 9 10fun ABBREV_TAC q (g as (asl,w)) = 11 let val ctxt = free_varsl(w::asl) 12 val (lhs,rhs) = dest_eq (Parse.parse_in_context ctxt q) 13 in 14 ABB lhs rhs g 15 end 16 17fun PAT_ABBREV_TAC q (g as (asl, w)) = 18 let val fv_set = FVL (w::asl) empty_tmset 19 val ctxt = HOLset.listItems fv_set 20 val (l,r) = dest_eq(Parse.parse_in_context ctxt q) 21 fun matchr t = raw_match [] fv_set r t ([],[]) 22 val l = variant (HOLset.listItems (FVL [r] fv_set)) l 23 fun finder t = not (is_var t orelse is_const t) andalso can matchr t 24 in 25 case Lib.total (find_term finder) w of 26 NONE => raise mk_HOL_ERR "OldAbbrevTactics" 27 "PAT_ABBREV_TAC" "No matching term found" 28 | SOME t => ABB l t g 29 end 30 31 32fun UNABBREV_TAC [QUOTE s] = let 33 val s' = Lib.deinitcomment s 34in 35 FIRST_ASSUM(SUBST1_TAC o SYM o 36 assert(curry op = s' o fst o dest_var o rhs o concl)) THEN 37 BETA_TAC 38end 39 | UNABBREV_TAC _ = raise mk_HOL_ERR "OldAbbrevTactics" 40 "UNABBREV_TAC" "unexpected quote format" 41 42end;