# Re: [isabelle] simple lemma in ring theory

hi, Clemens
thank you!

`if i need to use this definition a lot, is it possible to modify the prover
``so that it will
`do the unfold automatically?
another question is, if in this example suppose first i try "by blast" and
it says "empty result sequence", how can i know that i need to add
(unfold dvd1_def). is there a way to make the error message more meaningful?

`basically what i would like to know is how far the automatic prover has
``reached so
`that i can add what's missing.
thanks
tao

`----- Original Message -----
``From: "Clemens Ballarin" <ballarin at in.tum.de>
`To: "Tao Ma" <separable at gmail.com>
Cc: <cl-isabelle-users at lists.cam.ac.uk>
Sent: Friday, December 15, 2006 7:40 AM
Subject: Re: [isabelle] simple lemma in ring theory

Dear Tao Ma,

`blast is usually quite good at proving simple lemmas on divisibility,
``after unfolding the definition, of course. Here's a more concise version
``of your proof:
`
lemma (in "domain")
assumes xr: "x \<in> carrier R"
and yr: "y \<in> carrier R"
shows "dvd1 R x (x \<otimes> y)"
using xr and yr
by (unfold dvd1_def) blast
Clemens

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