# [isabelle] simple lemma in ring theory

hi,
how i can make it (like adding a rule to simp set?) so that the following
lemma
(x | xy in a ring) can be proved by one of the prover(blast, auto, etc)?
thanks
tao
constdefs (structure R)
dvd1 :: "('a, 'm) ring_scheme => 'a => 'a => bool"
"dvd1 R x y == (\<exists> z. z \<in> carrier R & y = x \<otimes> z)"
lemma (in "domain") x_dvd_xy: includes "domain" R
assumes xr: "x \<in> carrier R"
and yr: "y \<in> carrier R"
shows "dvd1 R x (x \<otimes> y)"
proof -
from xr and yr have "\<exists> z. z \<in> carrier R & (x \<otimes> y = x
\<otimes> z)" by blast
from this show ?thesis by (unfold dvd1_def)
qed

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