Re: [isabelle] Lost indexname in instantiated theorem: Eisbach messes up "of" and "where" attributes, when instantiating with "TYPE(...)"



Hi Peter,
Eisbach shadows the existing "of" and "where" attributes to support being re-interpreted in method expressions (which it looks like you've figured out).
What you're seeing is an error in this additional functionality, specifically it decides that "TYPE(nat)" means that you want to instantiate a type attribute to "nat". This results in some inconsistency when forming a static closure.
This should be easy to fix. The easiest workaround in the interim is to avoid using bare "TYPE('a)".

i.e.

thm foo[of "id TYPE(nat)",simplified id_def]

Which I realise is a bit of a pain (sorry about that). Using "Pure.of" is also fine as long as you aren't defining an Eisbach method.




> On 26 Jun 2015, at 11:15 pm, Peter Lammich <lammich at in.tum.de> wrote:
>
>> Consider the following theory, where I use the of and where attributes
>> to instantiate a variable to "TYPE(nat)".
>> Without Eisbach included, everything is fine. With Eisbach included, I
>> get the error "Lost indexname in instantiated theorem".
>>
>> What is going on here, and is there a workaround?
>
> A possible workaround (except from not using Eisbach) is to use
> "Pure.of"/"Pure.where" instead of "of"/"where".
>
> --
>  Peter
>
>
>>
>> --
>>  Peter
>>
>>
>> theory Scratch
>> imports Main
>>  "~~/src/HOL/Eisbach/Eisbach"  (* Remove this line, and everything
>> works fine *)
>> begin
>>
>>  consts f :: "'a â bool"
>>  lemma foo: "f a â True" by auto
>>
>>  thm foo[of "TYPE(nat)"]          (* Error: Lost indexname in
>> instantiated theorem *)
>>  thm foo[where a = "TYPE(nat)"]   (* Error: Lost indexname in
>> instantiated theorem *)
>>
>> end
>>
>>
>>
>
>
>


________________________________

The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.




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