[isabelle] No blast_trace anymore; assumption trace?


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:

theorem "(P ==> (Q ==> ((P ==> (Q ==> (!!(P::prop). PROP P))) ==> (!!(P::prop). PROP P))))"
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.


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