Email Gateway (Aug 22 2022 at 10:32): Email Gateway (Aug 22 2022 at 10:32):From: "W. Douglas Maurer" <maurer@gwu.edu>
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
Email Gateway (Aug 22 2022 at 10:32):From: Larry Paulson <lp15@cam.ac.uk>
The assumptions are part of the theorem. After all, nobody would state Fermat’s Last Theorem as
x^n + y^n ~= z^m,
without the preconditions on x, y, z and n.
Regarding your other question: many facts can be proved by simp alone, but here the point is to alert you that your proposed theorem has already been proved in essentially the same form.
Larry Paulson
Last updated: Apr 18 2024 at 08:19 UTC