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

Andreas Schropp schropp at in.tum.de
Fri Aug 26 19:02:54 CEST 2011

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

More information about the isabelle-dev mailing list