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.

Larry

> 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 MHonArc.