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

[Gerwin Klein]

On 19/08/2011, at 5:56 AM, Alexander Krauss wrote:
> 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???

Can't really quantify it, but I'm seeing this all the time from not-so-novice users over here. Mixing sets and predicates (e.g. using intersection on predicates) works often enough that people like it and overuse it. Sooner or later you will see unfolding of mem_def. As opposed to unfolding conjunction, unfolding mem_def proves things that otherwise simp/auto/etc fail on.

Gerwin