I'm very new to Isabelle, so apologies if this question is poorly formed.
I'm trying to prove the following:
record
Point =
x :: nat
y :: nat
definition
cond :: "Point ⇒ Point ⇒ 𝔹"
where
"cond point1 point2 ≡
abs (x point1 - x point2) = 1 ∨ abs (y point1 - y point2) = 1"
My proof is:
lemma cond_proof : "∃ point1 point2 . cond point1 point2 = True"
sledgehammer
by (metis Point_ext_def abs_division_segment add_diff_cancel_left' cond_def select_convs(1))
This triggers the warning:
Metis: Unused theorems:
Please could someone explain what this means? And if possible, help me to arrive at a proof which satisfies this condition.
I'm still very new to Isabelle, so all comments are appreciated.
I can comment on some of the practical aspects related to your problem. I believe, the warning is self-explanatory. Normally, you can delete the unused theorems and metis is still able to prove the theorem of interest (see cond_proof_metis in the code listing below).
The lemma cond_proof can be proven by exhibiting two points that satisfy the condition in the lemma. I believe that such an approach may be considered better than using the default proof found by sledgehammer. I have shown how to do this in lemma cond_proof_Isar in the code listing below. There are more compact ways of exhibiting the example. However, given that you are very new to Isabelle, I followed what seemed to me the most natural approach.
I am not certain if you left the command sledgehammer in your proof intentionally. However, in most cases, this is not something that you wish to do. Once a proof is found by sledgehammer, you can remove the command sledgehammer from your proof.
As a side note, I would suggest for you to work through some of the examples and exercises in the books "A Proof Assistant for Higher-Order Logic" by Tobias Nipkow et al and "Concrete Semantics with Isabelle/HOL" by Tobias Nipkow and Gerwin Klein. The aforementioned references contain many examples that are very similar to the problem that you are dealing with.
Unfortunately, I do not know enough about sledgehammer and metis to be able to tell you why the warning is produced upon using the output from sledgehammer to prove the theorem. For further information about sledgehammer and metis see 'A User’s Guide to Sledgehammer for Isabelle/HOL' that was written by Jasmin Christian Blanchette and can be found in the standard Isabelle documentation. Of course, further information about metis can also be found online (e.g. http://www.gilith.com/metis/). Hopefully, someone more knowledgeable than me will be able to provide more details with regard to your query.
section ‹Auxiliary commands›
theory Scratch
imports Complex_Main
begin
record Point =
x :: nat
y :: nat
definition
cond :: "Point ⇒ Point ⇒ bool"
where
"cond point1 point2 ≡
abs (x point1 - x point2) = 1 ∨ abs (y point1 - y point2) = 1"
(*Point_ext_def was part of the output produced by sledgehammer and is
listed as unused by metis. It can be removed with no effect on the
ability of metis to prove the result of interest.*)
lemma cond_proof_metis : "∃ point1 point2 . cond point1 point2 = True"
by (metis (*Point_ext_def*)
abs_1 add_diff_cancel_left' cond_def of_nat_1_eq_iff select_convs(1))
lemma cond_proof_Isar : "∃point1 point2 . cond point1 point2 = True"
proof(intro exI)
define point1::Point where point1: "point1 ≡ ⦇x = 2, y = 0⦈"
define point2::Point where point2: "point2 ≡ ⦇x = 1, y = 0⦈"
show "cond point1 point2 = True"
unfolding cond_def point1 point2 by auto
qed
end
Isabelle version: Isabelle2020