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.