*To*: Sean McLaughlin <seanmcl at cmu.edu>*Subject*: Re: [isabelle] strange tvar*From*: Stefan Berghofer <berghofe at in.tum.de>*Date*: Fri, 28 Oct 2005 19:55:11 +0200*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <B3BCCB66-2107-4A81-84DC-A5E692ECD0AA@cmu.edu>*Organization*: Technische Universität München*References*: <B3BCCB66-2107-4A81-84DC-A5E692ECD0AA@cmu.edu>*User-agent*: Mozilla/5.0 (X11; U; Linux i686; en-US; rv:1.7.8) Gecko/20050921

Sean McLaughlin wrote: > Hello, > > In examining the proof of HOL.less_max_iff_disj I came upon something > I found strange, which indicates I don't understand this aspect of the > proof term: > > In all the other proofs I've seen up to this point (and I've seen > hundreds), > all the free TVars were contained in the conclusion or premises of the > theorem. Moreover, all of these Hello Sean, this kind of "subformula property" need not hold in general. In particular, it does not hold if the proof is not in "normal form", i.e. contains detours. Due to the fact that type variables that are not contained in the main goal may appear during the proof of a theorem, Isabelle's theorem datatype also contains a list of sort hypotheses (see section 5.1.7 of the Isabelle Reference manual). > TVars had index 0 (as part of the "indexname" type) In this case, > there is a free TVar deep in the proof "'t" with index "111". Now I have > no idea where this came from, nor the significance of the index, > especially > such a seemingly strange one as this. Since type information can be reconstructed, the proof terms of theorems stored in Isabelle's theorem database do not contain any type information. The type reconstruction algorithm first inserts type variables in place of the omitted types, which are then instantiated via unification. In order to be able to generate fresh variables easily, the reconstruction algorithm simply increments the index every time it generates a variable, which may lead to "strange" indices like the one you have encountered. If a type variable (with "?") remains after reconstruction, this means that the choice of the type does not influence the correctness of the proof. The index has no particular significance - one could add a postprocessing stage to the reconstruction algorithm that replaces these "strange" variables by "nicer" ones. 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

**References**:**[isabelle] strange tvar***From:*Sean McLaughlin

- Previous by Date: [isabelle] proofterm bug?
- Next by Date: [isabelle] rep_thm
- Previous by Thread: Re: [isabelle] strange tvar
- Next by Thread: [isabelle] bug in Isabelle2005
- Cl-isabelle-users October 2005 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