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

[Brian Huffman]

On Fri, Aug 26, 2011 at 9:20 AM, Andreas Schropp <schropp at in.tum.de> wrote:
> On 08/26/2011 06:33 PM, Brian Huffman wrote:
>>
>> This approach would let us avoid having to axiomatize the 'a set type.
>>
>
> Thanks for trying to help me, but as I said:
>  axiomatized set is just a slight inconvenience for me, so if you go for
> sets as a seperate type don't bother introducing a new primitive.

I didn't suggest the idea merely for your benefit. I think this
approach would give Isabelle a nicer, simpler logical foundation.

>> Also, for those of us who like predicates, "pred_typedef" might be
>> rather useful as a user-level command.
>>
>
> Sets and predicates are isomorphic, so if my isomorphic transfer tool works
> out I don't see why this is needed.

I've often had situations where I wished I had a user-level
"pred_typedef" command. Here's an example:

datatype foo = ...
definition is_bar :: "foo => bool" where ...

Now I want to define a type "bar" such that:
Rep_bar :: bar => foo
Abs_bar :: foo => bar
Abs_bar (Rep_bar x) = x
is_bar x ==> Rep_bar (Abs_bar x) = x
is_bar (Rep_bar x)

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.

On the other hand, a "pred_typedef" command could generate exactly the
rules I want. The same "pred_typedef" command could also generate the
same rules that "typedef" currently generates, simply by using a
predicate of the form "%x. x : S". (This is how I expect the "typedef"
wrapper could work.)

- Brian