Re: [isabelle] simple lemma in ring theory



Dear Tao,

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 unfold/blast combination.

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" 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?

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.

Clemens






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