Re: [isabelle] Set notation for tuples broken



Am 10/03/2013 08:36, schrieb John Wickerson:
> When you want to use a pattern in your set comprehension, you can't just write
> 
> {(a,b). P a b}

Yes, you can. It stands for Collect(%(a,b). P a).

> you have to write:
> 
> {(a,b) | a b. P a b}

This produces Collect(%p. EX a b. p = (a,b) & P a b).

Tobias

> cheers,
> john
> 
> On 10 Mar 2013, at 00:00, C. Diekmann wrote:
> 
>> Hi,
>>
>> I want to report that the following set notation is unfortunately not accepted:
>>  {(a,b) ∈ X. P a}
>>
>> The following work-around is accepted:
>>  {(a,b). (a, b) ∈ X ∧ P a b}
>>
>> lemma split_conv_set: "{x ∈ X. case x of (a,b) ⇒ P a b} = {(a,b). (a,
>> b) ∈ X ∧ P a b}"
>>  by fastforce
>>
>> What must I do to use the first notation?
>>
>> Regards
>>  Cornelius
>>
> 





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