# [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
using assms

`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!
``-WDMaurer
`--
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
MHonArc.*