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
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
