Re: [isabelle] Set notation for tuples broken



When you want to use a pattern in your set comprehension, you can't just write

{(a,b). P a b}

you have to write:

{(a,b) | a b. P a b}

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.