Re: [isabelle] RC2 for testing; Toplevel.timing has no affect anymore

On Mon, 14 Oct 2013, Gottfried Barrow wrote:

It would be nice to have the "using[[blast_trace]]" back.

I've rarely used blast, or so I thought, but now that I see that auto calls it a lot, I see I've been using it a lot all along.

You say the blast trace is not meant for user consumption, but I'm using it.

That was just an accident. You found some funny flag and used it for some odd purpose, without any general principle behind it. For every Isabelle feature there need to be 2 or 3 good reasons to be there.

The following user-space attribute definition defines something that is
close to the discontinued blast_trace declaration:

attribute_setup blast_trace = {*
  Scan.succeed (Thm.declaration_attribute (K (Config.put_generic Blast.trace true)))

lemma "A ⟶ A" using [[blast_trace]] by blast

Here is also a slightly more elaborate version with argument parser:

attribute_setup blast_trace = {*
   (Parse.$$$ "=" -- Args.$$$ "true" >> K true ||
    Parse.$$$ "=" -- Args.$$$ "false" >> K false ||
    Scan.succeed true) >>
  (fn b => Thm.declaration_attribute (K (Config.put_generic Blast.trace b)))

These Isabelle/ML operations are much less arcane than the use of blast_trace in the first place.

It's also not about proving the theorem. It's about learning something from the blast method. I allocate a few minutes to look at the HOL.impCE that it lists in the details.

Blast is a slightly more sophisticated version from the basic Classical Reasoner. The latter is definitely worth learning, using its fine documentation in the isar-ref manual and its ML sources.


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