/usr/share/hol88-2.02.19940316/Library/arith/instance.ml is in hol88-library-source 2.02.19940316-19.
This file is owned by root:root, with mode 0o644.
The actual contents of the file can be viewed below.
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 | %****************************************************************************%
% FILE : instance.ml %
% DESCRIPTION : Conversional for increasing the power of a conversion by %
% allowing it to work on a substitution instance of a term %
% that is acceptable to it. %
% %
% READS FILES : <none> %
% WRITES FILES : <none> %
% %
% AUTHOR : R.J.Boulton %
% DATE : 30th January 1992 %
% %
% LAST MODIFIED : R.J.Boulton %
% DATE : 29th July 1992 %
%****************************************************************************%
%----------------------------------------------------------------------------%
% INSTANCE_T_CONV : (term -> term list) -> conv -> conv %
% %
% Generalizes a conversion that is used to prove formulae true by replacing %
% any syntactically unacceptable subterms with variables, attempting to %
% prove this generalised formula, and if successful re-instantiating. %
% The first argument is a function for obtaining a list of syntactically %
% unacceptable subterms of a term. This function should include in its %
% result list any variables in the term that do not appear in other subterms %
% returned. The second argument is the conversion to be generalised. %
%----------------------------------------------------------------------------%
let INSTANCE_T_CONV detector conv tm =
let (univs,tm') = strip_forall tm
in let insts = setify (detector tm')
in let vars = map (genvar o type_of) insts
in let tm'' = list_mk_forall (vars,subst (combine (vars,insts)) tm')
in EQT_INTRO (GENL univs (SPECL insts (EQT_ELIM (conv tm''))));;
|