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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
