# [isabelle] No blast_trace anymore; assumption trace?

Hi,

`It was using "declare[[blast_trace=false]]" and
``"declare[[blast_stats=false]]" with Isabelle2013 that showed me that
``auto sometimes calls blast, but those traces cause an error now. Did
``anything replace them?
`

`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 give here two proofs of the same statement:
(*1*)

`theorem "(P ==> (Q ==> ((P ==> (Q ==> (!!(P::prop). PROP P))) ==>
``(!!(P::prop). PROP P))))"
` by(assumption)
(*2*)

`theorem "(P ==> (Q ==> ((P ==> (Q ==> (!!(P::prop). PROP P))) ==>
``(!!(P::prop). PROP P))))"
` apply(simp del: True_implies_equals)
by(simp only: True_implies_equals)
(* lemma True_implies_equals: "(True ==> PROP P) == PROP P" *)

`The formula "(P ==> (Q ==> (!!(P::prop). PROP P))) ==> (!!(P::prop).
``PROP P)))" is a conjunction, and I'm having to work hard to try and
``prevent the automatic proof methods from proving things using too much HOL.
`

`The proof for (*2*) is undesirable, but the proof for (*1*) seems okay
``because it doesn't look like it's resorting to any HOL other than some
``Trueprop coercion.
`
However, I don't know the details of what's happening, so I could be wrong.
What I'm guessing is something like this:

`There's 3 assumptions: P, Q, and "(P ==> (Q ==> (!!(P::prop). PROP
``P)))". The assumption method starts by using P and Q to reduce the third
``assumption to "(!!(P::prop). PROP P))", which can then be used as an
``assumption for the final conclusion.
`

`If I had a trace to tell me what the assumption method is doing, I might
``could stare at it a long time, and figure out what "assumption" is
``doing, and also do that with future problems.
`
Regards,
GB

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