Re: [isabelle] changing smt by automatic reasoning internal to Isabelle
I still tend to get rid of smt calls, though it’s a chore.
One tip is to use your working smt call to identify the specific instances of the lemmas that you need. So if you have
smt lemma_1 … lemma_n
you can see if it still works with lemma_1 [of a b], where a and b are constants in your problem. Once you’ve done that, then insert
using lemma_1 [of a b]
and try sledgehammer again. You might get a much better proof.
> On 30 Jul 2019, at 21:31, José Manuel Rodríguez Caballero <josephcmac at gmail.com> wrote:
> (i) Is there an automatic way to change "smt" by some automatic reasoning
> internal to Isabelle, e.g., metis, auto, simp?
> (ii) In case of a negative answer for (i), which are the steps "by hand"
> recommended for such a task?
This archive was generated by a fusion of
Pipermail (Mailman edition) and