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
