Delivery-Date: 
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: list
From: Konrad Slind <slind@informatik.tu-muenchen.de>
To: shaw@cs.ucdavis.edu, info-hol@cs.uidaho.edu
In-Reply-To: <199509282237.PAA05218@roma-cafe.cs.ucdavis.edu> (shaw@cs.ucdavis.edu)
Subject: Re: TRS for HOL90 ?
Message-Id: <95Sep29.174038met.8084@sunbroy14.informatik.tu-muenchen.de>
Date: Fri, 29 Sep 1995 17:40:37 +0100


> Is the theorem retrieval system ported to HOL90 ?

See Richard's message, but also notice that hol90's contrib directory
already contains the "orsml" library. I have used this in some of my
proof efforts and have found it to be useful. The relevant structure has
the following signature:

  signature Hol_queries_sig =
  sig
    val mk_theory_db : string -> Orsml.co
    val mk_all_theories_db : unit -> Orsml.co
    val type_test : (hol_type -> bool) -> HolDbData.hol_theory_data -> bool
    val term_test : (term -> bool) -> HolDbData.hol_theory_data -> bool
    val thm_test : (thm -> bool) -> HolDbData.hol_theory_data -> bool
    val db_find_thms : {test:thm -> bool, theory:string} -> Orsml.co
    val db_find_all_thms : (thm -> bool) -> Orsml.co
    val find_match : {pattern:term, term:term} -> term subst * hol_type subst
    val seek : {pattern:term, theory:string} -> HolDbData.hol_theory_data list
    val seek_all : term -> HolDbData.hol_theory_data list
  end

I only used the package for looking up theorems by patterns (functions
"seek" and "seek_all"), although there are much more advanced things
possible, e.g. looking up all rewrites applicable to a goal, finding all
induction theorems that apply to a goal, etc.

Alas, one downside to the package is a lamentable lack of documentation.

Konrad.