Re: [isabelle] free term instantiations

Sean McLaughlin wrote:

  I was under the impression that all terms with free variables have
their terms instantiated (in full proof terms) in the order occurring in
the term.  However, I happened upon the following counterexample:
which is instantiated

x, y,below,inf

instead of


as a term order would indicate.  Would someone please explain
the exact order of instantiation.

Hello Sean,

does this happen with a theorem that you have proved yourself, or with
one taken from Isabelle's library?

The order of instantiation corresponds to the order of quantifiers
introduced by the functions forall_intr_frees (for free variables)
and forall_intr_vars (for schematic variables). Drule.forall_intr_vars uses
the vars_of function to determine the list of variables, which returns
the variables in the order they occur in the term. In contrast,
Drule.forall_intr_frees uses

  sort Term.term_ord (term_frees ...)

to determine the list of variables (i.e. the free variables are
sorted alphabetically).
Unfortunately, in Isabelle there are currently thousands of functions
for computing lists of Frees, Vars, TFrees, or TVars, each of which
returns the variables in a different order :-(
To get an idea of the order of instantiation for a particular theorem,
you can try

ML {* forall_intr_vars (forall_intr_frees (thm "...")) *}

where "..." stands for the name of the theorem in question.


Dr. Stefan Berghofer               E-Mail: berghofe at
Institut fuer Informatik           Phone: +49 89 289 17328
Technische Universitaet Muenchen   Fax:   +49 89 289 17307
Boltzmannstr. 3                    Room: 01.11.059
85748 Garching, GERMANY  

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.