1(* ===================================================================== *)
2(* FILE          : hol88Lib.sml                                          *)
3(* DESCRIPTION   : Routines that provide some compatibility with hol88.  *)
4(*                                                                       *)
5(* AUTHOR        : Konrad Slind, University of Calgary                   *)
6(* DATE          : September 15, 1991                                    *)
7(* ===================================================================== *)
8
9structure hol88Lib :> hol88Lib =
10struct
11
12open Lib Abbrev
13
14fun HOL88_ERR {function, message} =
15 Feedback.HOL_ERR {origin_structure = "hol88Lib",
16                   origin_function = function,
17                   message = message}
18
19infix ##
20
21type ('a,'b)hol88subst = ('b * 'a) list
22
23fun pair2recd (M,v) = {redex=v, residue=M}
24fun recd2pair {redex, residue} = (residue, redex)
25
26fun hol88subst_of s = map recd2pair s
27fun subst_of s = map pair2recd s
28
29fun match_type ty     = hol88subst_of o Type.match_type ty
30val subst             = Term.subst o subst_of
31val inst              = Term.inst o subst_of
32fun match_term pat ob = (hol88subst_of ## hol88subst_of)
33                          (Term.match_term pat ob)
34
35fun SUBST s template th = Thm.SUBST (subst_of s) template th
36val INST                = Thm.INST o subst_of
37val INST_TYPE           = Thm.INST_TYPE o subst_of
38val INST_TY_TERM        = Drule.INST_TY_TERM o (subst_of ## subst_of)
39
40val match = match_term
41
42fun assoc i alist =
43   case Lib.assoc1 i alist
44     of NONE => raise HOL88_ERR {function = "assoc", message = ""}
45      | (SOME x) => x
46
47fun rev_assoc i alist =
48   case Lib.assoc2 i alist
49     of NONE => raise HOL88_ERR {function = "rev_assoc", message = ""}
50      | (SOME x) => x
51
52val frees = rev o Term.free_vars
53val freesl = rev o Term.free_varsl
54
55fun GEN_ALL th =
56  Lib.itlist Thm.GEN
57    (Lib.set_diff (frees (Thm.concl th)) (freesl (Thm.hyp th))) th
58
59fun GEN_REWRITE_RULE F thlist1 thlist2 =
60    Rewrite.GEN_REWRITE_RULE F
61        (Rewrite.add_rewrites Rewrite.empty_rewrites thlist1) thlist2
62
63fun GEN_REWRITE_TAC F thlist1 thlist2 =
64    Rewrite.GEN_REWRITE_TAC F
65        (Rewrite.add_rewrites Rewrite.empty_rewrites thlist1) thlist2
66
67fun variant L tm =
68   if Term.is_var tm
69   then Term.variant L tm
70   else if Term.is_const tm
71        then Term.variant L (Term.mk_var (Term.dest_const tm))
72        else raise HOL88_ERR {function = "variant",
73                               message = "not a variable or a constant"}
74
75end
76