Re: [isabelle] system of representatives of an equivalence relation



A general suggestion that might work in this type of situation is to prove your theorems in a context that assumes that you have an element of an equivalence class. In your case, perhaps you need the additional assumption that this element contains no variants. Then it may be enough to show that every equivalence class contains at least one such element.

Larry Paulson


On 11 Apr 2014, at 13:35, Christian Sternagel <c.sternagel at gmail.com> wrote:

> Dear Larry,
> 
> at least I'm under the impression that the representatives are needed ;).
> 
> Let me elaborate: I am formalizing a proof as part of IsaFoR (mainly first-order term rewriting). In the remainder of IsaFoR (which is already quite huge) term rewrite systems (TRS) are just represented as sets of pairs of terms. This is a well-supported type and easy to use.
> 
> But in the new proof a crucial property is that at a certain point a TRS does not contain variants (i.e., variable renamed versions of rules). Since I want to reuse all the existing lemmas about TRSs but for the current proof I need a TRS without variants, I defined the operation of removing variants from TRSs (via first building the equivalence classes w.r.t. variable renaming and then projecting, using SOME, to a system of representatives).
> 
> Please let me know what you think about this setup or if you have any suggestions for improvements.
> 
> cheers
> 
> chris
> 
> On 04/11/2014 01:41 PM, Lawrence Paulson wrote:
>> Are specific representatives actually needed? It might be better to use the equivalence classes themselves. That is the point of this construction.
>> 
>> --lcp
>> 
>>> On 11 Apr 2014, at 09:16, Christian Sternagel <c.sternagel at gmail.com> wrote:
>>> 
>>> Thanks Dimitriy,
>>> 
>>> That looks similar to the construction I'm currently using ;), i.e.,
>>> 
>>>  "repsys A R = {(SOME x. x ∈ X) | X. X ∈ A // R}"
>>> 
>>> I was hoping that some properties are already proved about it. E.g., that two non-equal elements of "repsys A R" are not in relation w.r.t. "R", "repsys A R" is a subset of "A", ...
>>> 
>>> But it should be easy to do anyway. Would this be interesting for anybody else?
>>> 
>>> cheers
>>> 
>>> chris
>>> 
>>> btw: I could not find the constant "proj" in Equiv_Relations.
>>> 
>>>> On 04/11/2014 10:07 AM, Dmitriy Traytel wrote:
>>>> Hi Chris,
>>>> 
>>>> Am 11.04.2014 09:49, schrieb Christian Sternagel:
>>>>> Dear fellow Isabellers,
>>>>> 
>>>>> I am wondering whether there is already a way in the Isabelle/HOL
>>>>> library (or the AFP, for that matter) to obtain a system of
>>>>> representatives (I'm not sure whether this is the correct term, in
>>>>> German it is called "Repräsentantensystem") for a given equivalence
>>>>> relation, i.e., a set containing one representative of each
>>>>> equivalence class?
>>>> 
>>>> Something like this: "(λX. SOME x. x ∈ X) ` Equiv_Relations.proj r `
>>>> Field r"
>>>> 
>>>> The function Equiv_Relations.proj gives you the (non-empty) equivalence
>>>> class of an element.
>>>> 
>>>> Dmitriy
>>> 





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