[isabelle-dev] lemma addition

[Lars Noschinski]

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.

[1] 
http://www4.in.tum.de/~urbanc/cgi-bin/repos.cgi/isabelle-cookbook/file/95d6853dec4a/progtutorial.pdf

   -- Lars