[isabelle] A problem with Auto solve_direct
I have a write-up in which I am trying to teach my students how to
use Auto solve_direct, using as simple an example as I can come up
with. The example I chose was: If x is a multiple of 4, then so is
x^2. So I started my .thy file by writing
lemma fixes x::int assumes "4 dvd x" shows "4 dvd x*x"
and I immediately got an output message saying
Auto solve_direct: The current goal can be solved directly with
Rings.comm_semiring_1_class.dvd_mult: ?a dvd ?c ==> ?a dvd ?b * ?c
Rings.comm_semiring_1_class.dvd_mult2: ?a dvd ?b ==> ?a dvd ?b * ?c
I want to teach the students that, when they get a message saying
that the current goal can be solved directly with alpha, they should
finish the proof by writing
by (rule alpha)
But in this case, when I tried to finish the proof by writing
by (rule Rings.comm_semiring_1_class.dvd_mult)
it didn't go through.
As it so happens, if I precede this with
it does go through, but now it doesn't need anything from theory
Rings; it can be proved by simp, which spoils the example of how to
use Auto solve_direct. So I guess my questions are:
Why does Auto solve_direct tell me that a goal can be solved directly
with some rule alpha, when this is actually not the case without
adding using assms?
And if Auto solve_direct assumes that I'm going to try using assms,
why doesn't it then tell me that the current goal can be solved by
simp, instead of pulling something out of theory Rings? Thanks!
Prof. W. Douglas Maurer Washington, DC 20052, USA
Department of Computer Science Tel. (1-202)994-5921
The George Washington University Fax (1-202)994-4875
This archive was generated by a fusion of
Pipermail (Mailman edition) and