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