Besides, I don’t think your original goal is true: the variable L is free in
LHS, but bound in RHS, as shown in different colors.
Chun
Inviato da iPhone
> Il giorno 26 ott 2019, alle ore 17:18, Yassmeen Derhalli
> <derhal...@gmail.com> ha scritto:
>
>
> Dear Thomas,
>
> Thank you so much for your elaborated reply.
> I will go through Section 5.5.1.1 that you referred to
>
> Thanks again!
> Yassmeen
>
>
>
>
>> On Fri, Oct 25, 2019 at 1:22 PM Thomas Tuerk <tho...@tuerk-brechen.de> wrote:
>> Dear Yassmeen,
>>
>> set comprehensions in HOL are a bit cryptic. They are explained in Section
>> 5.5.1.1 of the Description manual. In short, something like {t | p} is
>> syntactic sugar that is turned by the parser into GSPEC(\(x1 ,...,xn).
>> (t,p)). The trick is figuring out, which variables x1, ... xn to use. There
>> are rules for that, which for non-trivial cases gives sometimes unexpected
>> results. See excerpt from Sec. 5.5.1.1 below. For making it unambiguous,
>> there is also the form {t | (x1, ..., xn) | p} where the variables are given
>> explicitly. For complicated sets, I would always use the explicit form and I
>> would not be surprised if L is free in one of the forms below and free in
>> the other. In my opinion the syntax {t | p} should only be used in trivial
>> cases, because it can easily lead to human readers misunderstanding the
>> meaning otherwise. I for one are confused by complicated examples like the
>> comprehensions you use. I need essentially to run the parser and look at the
>> result before knowing what the meaning is. The following trace might be
>> useful to show more information when pretty-printing the parsed
>> comprehensions:
>>
>> set_trace "pp_unambiguous_comprehensions" 1
>>
>>
>>
>> Excerpt from Section 5.5.1.1
>>
>>> The normal interpretation of { t | p } is the set of all ts such that
>>> p. In HOL , such syntax parses to: GSPEC(\(x 1 ,...,x n ).(t,p)) where x 1
>>> , ... , x n are those
>>> free variables that occur in both t and p if both have at least one free
>>> variable. If t or p
>>> has no free variables, then x 1 , ... , x n are taken to be the free
>>> variables of the other term.
>>> If both terms have free variables, but there is no overlap, then an error
>>> results. The
>>> order in which the variables are listed in the variable structure of the
>>> paired abstraction
>>> is an unspecified function of the structure of t (it is approximately left
>>> to right).
>> I hope this helps.
>>
>> Thomas
>>
>>
>>
>> On 25.10.19 18:05, Yassmeen Derhalli wrote:
>>> Hi,
>>> I have this proof goal, where I need to prove that two sets are equal.
>>>
>>> {{f i | i IN if a IN {b | b IN L} then s1 a else s2 a} |
>>> a |
>>> a IN if j IN L then s3 j else s4 j} =
>>> {{f i | i IN if a IN {b | b IN L} then s1 a else s2 a} |
>>> a IN if j IN L then s3 j else s4 j}
>>>
>>> I have two questions regarding this proof, first, what is the difference
>>> between the first format when we use "|a | a IN...." (the left side of the
>>> goal) and the second format "...|a IN..." (the right side of the goal)?
>>> Secondly, are these sets equal? because it seems that HOL treats set L in
>>> the right side of the goal as a dummy variable of the set.
>>> I need help in clarifying the difference between both formats and some
>>> clues about how to proceed with the proof if the sets are equal.
>>>
>>> Best Regards,
>>> Yassmeen Elderhalli
>>>
>>>
>>>
>>> _______________________________________________
>>> hol-info mailing list
>>> hol-info@lists.sourceforge.net
>>> https://lists.sourceforge.net/lists/listinfo/hol-info
> _______________________________________________
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
