[isabelle-dev] lemma addition

Lars Noschinski noschinl at in.tum.de
Thu Aug 1 22:01:21 CEST 2013

On 01.08.2013 17:19, Makarius wrote:
>> Both of which are discharged by blast. If we look at the theorems
>> blast uses to prove
>> ⋀a b. A¯ ⊆ B¯ ⟹ (a, b) ∈ A ⟹ (a, b) ∈ B
>> (how this can be done is described in Section 3.7 of the Isabelle
>> Cookbook), we see that Relation.converse_iff plays a role, which was
>> declared with the iff attribute.
> I did not understand this mysterious reference. Which version of the
> Cookbook, which page exactly?

It is less mysterious than other references on this list...

Section 3.7, p. 66ff in [1] gives recipes how proof terms can be 
inspected. It is what worked best for me for getting ideas of blast proofs.

`> Using only canonical information reveals these possibilities that might
> be little known:
> * print_options: blast_trace, blast_stats, but this looks a bit chatty
> and of limited practical use

They seem to be mostly useful for debugging blast itself.


   -- Lars

More information about the isabelle-dev mailing list