Stream: Beginner Questions

Topic: Using Isabelle as an automated testing tool

Nils Buchholz (Mar 29 2024 at 14:35):

I'd like to automatically check if a theorem in my theory is solveable by try/sledgehammer or other tactics.
Is there a way to do this?

I've tried the mirabelle tool, but to my knowledge that requires a proof to already be present.

Fabian Huch (Apr 11 2024 at 10:45):

The mirabelle sledgehammer action does not really require a proof, but it looks for a by. So what you can do is axiomatize your lemma with the attribute [no_atp] (so it doesn't get used by sledgehammer), and "prove" it with by (rule your_axiomatized_lemma).

Nils Buchholz (Apr 11 2024 at 12:30):

Fabian Huch said:

The mirabelle sledgehammer action does not really require a proof, but it looks for a by. So what you can do is axiomatize your lemma with the attribute [no_atp] (so it doesn't get used by sledgehammer), and "prove" it with by (rule your_axiomatized_lemma).

Is there a [no_atp] option for theorems inside locales?
When I prove my theorem in the context of a locale, sledgehammer still uses the axiomatized version.

locale varsAndFunctions =
fixes var_p::"bool"
fixes var_q::"bool"
assumes "True"

theorem (in varsAndFunctions) solve_stub[no_atp]:"False"
  sorry

theorem (in varsAndFunctions) solve:"False"
  sledgehammer

Last updated: May 07 2024 at 01:07 UTC