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;