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 > listhol-info@lists.sourceforge.nethttps://lists.sourceforge.net/lists/listinfo/hol-info > >
_______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info