Sender: info-hol-request@leopard.cs.byu.edu
Errors-To: info-hol-request@leopard.cs.byu.edu
Precedence: list
From: Konrad Slind <slind@informatik.tu-muenchen.de>
To: reetz@ira.uka.de, info-hol@leopard.cs.byu.edu
Cc: reetz@ira.uka.de, schneide@ira.uka.de
In-Reply-To: <"iraun1.ira.505:06.02.96.13.38.42"@ira.uka.de> (message from reetz on Tue, 6 Feb 1996 14:37:28 +0100)
Subject: Re: How do I get the definition of a constant in HOL90?
Message-Id: <96Feb6.170228met.8173@sunbroy14.informatik.tu-muenchen.de>
Date: 	Tue, 6 Feb 1996 17:02:22 +0100


> Given the name of a constant "X", how do I get the definition of that
> constant in HOL90 in a COMPUTABLE way? 

You could try the following: it functions by finding the first
definition in which the constant occurs.


fun find_def s =
let val {theory,...} = const_decl s
    fun drop_dollar s = (case(explode s) of ("$"::rst) => implode rst | _ => s)
    fun our_const c = (drop_dollar(#Name(dest_const c)) = s) handle _ => false
in first (can (find_term our_const) o concl o #2) (rev(definitions theory))
end;


Notes. 

* In the implementation, definitions are stacked up, so the list
  returned by "definitions" needs to be reversed. 

* It won't catch members of constant families, like numeric or string
  literals. 

* It won't catch surface syntax, like "{}" (in the sets library).

Konrad.