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
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
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
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and