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

[Alexander Krauss]

Hi all,

Here are some critical questions/comments towards two of Florian's 
initial arguments pro 'a set.

[...]

> * Similarly, there is a vast proof search space for automated tools
> which is not worth exploring since it leads to the »wrong world«, making
> vain proof attempts lasting longer instead just failing.

Can this claim be made more concrete (or even quantitative)? Or is it 
merely a conjecture?

 From what Jasmin wrote, this does not seem to hold for sledgehammer, 
and simp/auto/blast should not run into the "wrong world" when 
configured properly.

I understand that this is true for naive users... but automated tools???

> * The logical identification of sets and predicates prevents some
> reasonable simp rules on predicates: e.g. you cannot have (A |inf| B) x
> = A x&  B x
> because then expressions like »set xs |inter| set ys« behave strangely
> if the are eta-expanded (e.g. due to induction).

> * The missing abstraction for sets prevents straightforward code
> generation for them (for the moment, the most pressing, but not the only
> issue).

I want to emphasize that the limitation of the code generator mentioned 
here not only applies to sets-as-predicates but also to 
maps-as-functions and other abstract types that are often specified in 
terms of functions (finite maps, almost constant maps, etc.). Thus, 
having good old 'a set back is does not fully solve this problem as a 
whole, just one (important) instance of it.

My view on this whole topic is outlined in the report I recently sent 
around (http://www4.in.tum.de/~krauss/papers/refinement.pdf, not updated 
since last time). In the long run, I would prefer to see flexible 
transport machinery to move stuff between isomorphic types.

Alex