[isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation
krauss at in.tum.de
Thu Aug 18 21:56:39 CEST 2011
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
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
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.
More information about the isabelle-dev