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?
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
that i can add what's missing.
----- 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
This archive was generated by a fusion of
Pipermail (Mailman edition) and