Re: [isabelle] No blast_trace anymore; assumption trace?



On 10/9/2013 11:32 PM, Gottfried Barrow wrote:
I use that as an excuse to point out that these traces can help educate a man, and I ask here if there's some kind of trace that will give me some details about what the "assumption" method is doing.

I'll state the obvious again, but the more traces the better, though there's already a lot of tools to give feedback.

blast_trace looked like it was going to be useful to me. It's main use was that it was telling me when auto was resorting to something more than simplification, but I would try some to understand the details it was returning.

I've searched in NEWS and in isar-ref.pdf, but I didn't find anything about what would replace blast_trace.

Doing these simple exercises can help make obvious simple things that aren't obvious at first, and it's the feedback tools that help out. Talking to myself is fine when I have tools to eventually lead me to the answers.

In the proof of (*2*) that I gave, the simp trace was doing some substitution of "True", and that contributed to my impression that my false, "(!!(P::prop). PROP P)" was actually important. But then when I used "assumption", it eventually became clear that I was simply doing:

theorem "(P ==> (Q ==> ((P ==> (Q ==> R)) ==> R)))"

Modus ponens came to mind, and "Auto solve_direct", for the unexpanded formula, says "meta_impE" can be used, which is based on "meta_mp", but not quite the same, because of "meta_impE = meta_mp [elim_format]".

All that to say, one thing leads to another, and all the different routes can lead to a better understanding. I could assume I know what "assumption" is doing, but assuming I know the details when I don't, even with something simple, leads to being wrong a significant number of times.

I guess it's not a big deal, but the more access we have to the low-level details, to try and understand them and verify what we think is happening, the better. As I said, there's already a lot of feedback.

Regards,
GB







This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.