*To*: Sean McLaughlin <seanmcl at cmu.edu>, "'isabelle-users at cl.cam.ac.uk'" <isabelle-users at cl.cam.ac.uk>*Subject*: Re: [isabelle] free term instantiations*From*: Stefan Berghofer <berghofe at in.tum.de>*Date*: Thu, 09 Mar 2006 12:26:21 +0100*In-reply-to*: <8C3CE2EC-D375-4C56-9582-B0B23940CC79@cmu.edu>*Organization*: Technische Universität München*References*: <8C3CE2EC-D375-4C56-9582-B0B23940CC79@cmu.edu>*User-agent*: Mozilla/5.0 (X11; U; Linux i686; en-US; rv:1.7.12) Gecko/20050920

Sean McLaughlin wrote:

Hello, 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 below,inf,x,y 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. Greetings, Stefan -- Dr. Stefan Berghofer E-Mail: berghofe at in.tum.de 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 http://www.in.tum.de/~berghofe

- Previous by Date: Re: [isabelle] cardinality
- Next by Date: Re: [isabelle] instance theorems
- Previous by Thread: Re: [isabelle] cardinality
- Next by Thread: [isabelle] Sets
- Cl-isabelle-users March 2006 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list