Re: [isabelle] strange tvar



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





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