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?

You can tell the simplifier to use it every time by saying

declare dvd1_def [simp]

(and later [simp del] if you no longer want it) but blast does no equational reasoning and does not know about [simp].

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.

Unfortunately that is an open research problem and one of the advantages of the simplifier: it doens't just give up silently but leaves with the rest.

Tobias





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