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