Email Gateway (Aug 18 2022 at 10:00): Email Gateway (Aug 18 2022 at 10:00):From: Tao Ma <separable@gmail.com>
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
Email Gateway (Aug 18 2022 at 10:00):From: Clemens Ballarin <ballarin@in.tum.de>
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
Email Gateway (Aug 18 2022 at 10:00):From: Tao Ma <separable@gmail.com>
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
Email Gateway (Aug 18 2022 at 10:01):From: Tobias Nipkow <nipkow@in.tum.de>
if i need to use this definition a lot, is it possible to modify the
prover so that it will
do the unfold automatically?
You can tell the simplifier to use it every time by saying
declare dvd1_def [simp]
(and later [simp del] if you no longer want it) but blast does no
equational reasoning and does not know about [simp].
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.
Unfortunately that is an open research problem and one of the advantages
of the simplifier: it doens't just give up silently but leaves with the
rest.
Tobias
Email Gateway (Aug 18 2022 at 10:01):From: Clemens Ballarin <ballarin@in.tum.de>
Dear Tao,
if i need to use this definition a lot, is it possible to modify the
prover so that it will do the unfold automatically?
Well, blast is not particularly good at unfolding definitions. You
might use auto, clarsimp and fastsimp which are combinations of
simplifier and classical reasoner. In your case, you might do
declare dvd1_def [simp]
to add the theorem to the simpset. Note, however, that auto implements
a different prover than blast, and it might not be as effective as the
unfold/blast combination.
I would, however, advise against adding the definition to the simpset.
The effect is that definitions are unfolded all the time, and proof
states become big, which in turn confuses automatic methods. The more
disciplined approach is to prove suitable lemmas and make these
introduction, elimination and simplification rules by adding these to
the classical and simpsets. I admit that this is very much a craft,
and coming up with the right lemmas is may require some experimenting.
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?
You can use "apply <method>" to see the subgoal left behind by
<method>. This doesn't work with blast, because blast fails if it
doesn't solve the goal. Other methods of the classical reasoner tell
you how far the prover has reached. These are clarify and the
combinations clarsimp and auto.
Clemens
Last updated: May 03 2024 at 04:19 UTC