Re: [isabelle] simple lemma in ring theory
if i need to use this definition a lot, is it possible to modify the
prover so that it will do the unfold automatically?
Well, blast is not particularly good at unfolding definitions. You
might use auto, clarsimp and fastsimp which are combinations of
simplifier and classical reasoner. In your case, you might do
declare dvd1_def [simp]
to add the theorem to the simpset. Note, however, that auto implements
a different prover than blast, and it might not be as effective as the
I would, however, advise against adding the definition to the simpset.
The effect is that definitions are unfolded all the time, and proof
states become big, which in turn confuses automatic methods. The more
disciplined approach is to prove suitable lemmas and make these
introduction, elimination and simplification rules by adding these to
the classical and simpsets. I admit that this is very much a craft,
and coming up with the right lemmas is may require some experimenting.
another question is, if in this example suppose first i try "by blast"
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
You can use "apply <method>" to see the subgoal left behind by
<method>. This doesn't work with blast, because blast fails if it
doesn't solve the goal. Other methods of the classical reasoner tell
you how far the prover has reached. These are clarify and the
combinations clarsimp and auto.
This archive was generated by a fusion of
Pipermail (Mailman edition) and