[isabelle] Automating the auto-tools



I'm in jEdit, so I first open up a second view of jEdit with "View/New View".

I have a theorem:

theorem emS_is_unique1:
  "!u. (!x. ~(x IN u)) --> u EQ emS"

I highlight it, and run my script. It creates a new file which imports my main file, like this:

theory sTs_Simp_X
imports sTs_Simp
begin

theorem emS_is_unique1_S:
  "!u. (!x. ~(x IN u)) --> u EQ emS"
  apply(auto) sledgehammer
  nitpick[sat_solver=MiniSat_JNI]
  nitpick[sat_solver=SAT4J]
  oops

theorem emS_is_unique1_Sn:
  "~(!u. (!x. ~(x IN u)) --> u EQ emS)"
  apply(auto) sledgehammer
  nitpick[sat_solver=MiniSat_JNI]
  nitpick[sat_solver=SAT4J]
  oops
end

It's importing all my nitpick and sledgehammer settings from the main file.

It runs sledgehammer and nitpick on the theorem and its negation. It takes a while, that's why I have the two jEdit views. I watch sTs_Simp_X in one jEdit view and can work on sTs_Simp in the other.

The continuous prover works on sTs_Simp_X while I'm working on sTs_Simp. Of course, if I do a save on my main file, the auto-provers start over in sTs_Simp_X, which is why I try to leave it alone, but that's hard to do. I want to click around in sTs_Simp_X to see if anything is happening. I reduce the 20 provers down to e, spass, and z3, to speed things up; I'll probably put more back in.

I haven't completely figured out how the continuous prover works. In a big file, it sometimes seems to go into a dormant state if I don't go all the way to the bottom and click on the line where the "end" statement is.

I would attach the script, but it's done in a scripting language for WinEdt. jEdit has a scripting language, but I don't know how to use it except for very simple macros for key sequences.

I now return to the drudgery of tutorials and exercises.

Regards,
GB





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