Re: [isabelle] Confusing behavior of a paired set comprehension



I think what you really want is "ident S = {(x, x) | x. x \<in> S}".

(This is actually a syntactic abbreviation for "{y. \<exists>x. y =
(x, x) \<and> x \<in> S}".)

- Brian

On Wed, Apr 4, 2012 at 11:11 AM, Giuliano Losa <giuliano.losa at epfl.ch> wrote:
> Hello,
> the following definition is interpreted in a confusing way:
>
> def ident :: "'a set => ('a \times 'a) set"
> where "ident S = {(x,x) . x \in S}"
>
> the command "thm ident_def" yields
> ident ?S \<equiv> {(xa, x). x \<in> ?S}
>
> Should this be considered as a bug?
>
> Giuliano





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