Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] sledge-hammer


view this post on Zulip Email Gateway (Aug 22 2022 at 13:03):

From: michel levy <michel.levy@imag.fr>
I tried the example (suggested in the User's Guide to Sledgehammer)
theory Scratch
imports Main
begin
lemma "[a] = [b] ⟶ a = b"

I apply sledgehammer (with the button sledgehammer clicked) with
provers cvc4 remote_vampire z3 spass e
and the button Isar proofs clicked

I have in the output window
"cvc4": Try this: by (metis list.inject ) (28 ms ms) .
Warning : Isar proof construction failed.
"z3" : Try this: by auto (0.0 ms).
(No Isar proof available.)
"spass" : Try this : by (metis list.inject) (16 ms)
(No Isar proof available.)
"remote_vampire : Try this : by (metis list.inject) (8 ms)
(No Isar proof available.)
"e" : Try this: by (metis the_elem_set) (12 ms).
(No Isar proof available.)

What that means ? Is the lemma proved ?
Why there is no Isar proof available ?

-- email : michel.levy@imag.fr
http://membres-liglab.imag.fr/michel.levy

view this post on Zulip Email Gateway (Aug 22 2022 at 13:03):

From: Jasmin Blanchette <jasmin.blanchette@inria.fr>
Dear Michel,

I apply sledgehammer (with the button sledgehammer clicked) with
provers cvc4 remote_vampire z3 spass e
and the button Isar proofs clicked

I have in the output window
"cvc4": Try this: by (metis list.inject ) (28 ms ms) .
Warning : Isar proof construction failed.
"z3" : Try this: by auto (0.0 ms).
(No Isar proof available.)
"spass" : Try this : by (metis list.inject) (16 ms)
(No Isar proof available.)
"remote_vampire : Try this : by (metis list.inject) (8 ms)
(No Isar proof available.)
"e" : Try this: by (metis the_elem_set) (12 ms).
(No Isar proof available.)

What that means ? Is the lemma proved ?

The calls such as "by (metis list.inject)" are snippets you can click on and insert in your theory.

Why there is no Isar proof available ?

Multi-line Isar proofs are generated only if the provers provide a multi-line proof in the first place. Here, the property is so simple that there is no such proof, only a one-line proof.

Cheers,

Jasmin


Last updated: Mar 29 2024 at 12:28 UTC