Re: [isabelle] sledge-hammer



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





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.