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.

----- Original Message ----- From: "Clemens Ballarin" <ballarin at>
To: "Tao Ma" <separable at>
Cc: <cl-isabelle-users at>
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


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