[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.