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

[Alexander Krauss]

On 08/19/2011 01:31 AM, Gerwin Klein wrote:
> On 19/08/2011, at 5:56 AM, Alexander Krauss wrote:
>>
>>> * 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.

So your point is actually a different one from Florian's: Users unfold 
mem_def in order to gain automation, which may work in that moment, but 
is usually a bad idea later on. I understand this point.

(Aside: It would be interesting to explore why users actually do this. 
Is there something missing in the automation for sets that works better 
for predicates?)

My understanding of Florian's point above was that sets-as-predicates 
actually hinder automation by enlarging the search space. But it seems 
to me that this is only a theoretical consideration, and that we do not 
actually observe this effect in practice.

Alex