[isabelle] changing smt by automatic reasoning internal to Isabelle



Dear Isabelle users and experts,
  In the rules for submissions to Archives of Formal Proofs, it is written
that "No use of the command smt_oracle". If I well understood, this means
that proofs cannot be done using either "apply smt" or "by smt" (please
correct me if I am wrong). This was also pointed out in Gerwin's Style
Guide (section: "Do not use smt in proofs you need to maintain over longer
time"): http://proofcraft.org/blog/isabelle-style.html

(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?

Sincerely yours,
José M.

--

José Manuel Rodríguez Caballero

arvutiteaduse instituut / Institute of Computer Science
Tartu Ülikool / University of Tartu

Personal Research Page:  https://josephcmac.github.io/



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