/usr/share/hol88-2.02.19940316/help/ENTRIES/match.doc is in hol88-help 2.02.19940316-35.
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 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 | \DOC match
\TYPE {match : (term -> term -> ((term # term) list # (type # type) list))}
\SYNOPSIS
Finds instantiations to match one term to another.
\DESCRIBE
When applied to two terms, with no outer quantifiers in the first, {match}
attempts to find type and term instantiations for the first term (only) to make
it match the second. If it succeeds, it returns the instantiations in the form
of a pair containing a list of term replacements and a list of type
instantiations. If the first term represents the conclusion of a theorem, the
returned instantiations are of the appropriate form to be passed to
{INST_TY_TERM}.
\FAILURE
Fails if the term cannot be matched by one-way instantiation.
\EXAMPLE
The following shows how {match} could be used to match the conclusion of a
theorem to a term.
{
#let th = REFL "x:*";;
th = |- x = x
#match (concl th) "1 = 1";;
([("1", "x")], [(":num", ":*")])
: ((term # term) list # (type # type) list)
#INST_TY_TERM it th;;
|- 1 = 1
}
\COMMENTS
Note that there is no guarantee that the returned instantiations will be
possible for {INST_TY_TERM} to achieve, because some of the variables (term or
type) which need to be instantiated may be free in the assumptions, eg:
{
#top_print print_all_thm;;
- : (thm -> void)
#let th = ASSUME "x:* = x";;
th = x = x |- x = x
#match (concl th) "1 = 1";;
([("1", "x")], [(":num", ":*")])
: ((term # term) list # (type # type) list)
#INST_TY_TERM it th;;
evaluation failed INST_TYPE: type variable free in assumptions
}
\noindent In fact, for instantiating a theorem, {PART_MATCH} is usually easier.
\SEEALSO
INST_TY_TERM, PART_MATCH.
\ENDDOC
|