[isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation

[Andreas Schropp]

On 08/26/2011 07:02 PM, Brian Huffman wrote:
> With ordinary "typedef", I have to do this:
>
> typedef (open) bar = "{x. is_bar x}"
>
> But then it generates rules of the wrong form:
> x : {x. is_bar x} ==>  Rep_bar (Abs_bar x) = x
> Rep_bar x : {x. is_bar x}
>
> And I have to do an extra step to get the rules I want:
> lemmas Rep_bar' = Rep_bar [unfolded mem_Collect_eq]
> lemmas Abs_bar_inverse' = Abs_bar_inverse [unfolded mem_Collect_eq]
>
> Even with a transfer tool, the extra step would still be necessary.
>    

Predicate application corresponds to set-membership, so
in apart from technicalities (which might be hard, no idea)
I still don't see the problem.

>
> - Brian
>