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