# Re: [isabelle] Automating the auto-tools

On 7/21/2012 4:38 AM, Lars Noschinski wrote:

On 21.07.2012 03:39, Gottfried Barrow wrote:

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.

It should process more or less to the point where you are looking at in
the editor. This saves a lot of computing effort, when you are editing
something in the middle of a big theory...

`Okay. I guess the general rule is that if some code can be seen in a
``jEdit view, then the continuous prover will work on the file up to that
``point.
`

`To belabor the point, I suppose if I had 10 jEdit views open of 10
``different .thy files, the continuous prover would try to work on all of
``them up to the code that could be seen in each view.
`

`That's how it appears. I re-generate the tester file from the theorem. I
``click back on the jEdit view which has my main file. jEdit asks me if I
``want to reload the re-generated file. I say yes, and the re-generated
``tester file gets reloaded in both jEdit windows, and the continuous
``prover starts working away on the view that shows it. All of the code
``for the tester file can be seen, so the continuous prover works until it
``gets to the end.
`

`I broke the two tester theorems into four: Sledgehammer on the theorem.
``Nitpick on the theorem. Nitpick on the negation. Sledgehammer on the
``negation.
`
LEARNING BY ACCIDENT WITH AUTO-TOOLS

`By accident, I found out that importing my complete file will allow
``Sledgehammer and Nitpick to find things they otherwise couldn't find,
``which makes sense to do for the purposes of trying to find inconsistencies.
`

`Being back in my original file, rather than a simplified version for
``experimenting, I had the incorrect axiom uncommented out,
`
(x IN u <-> x IN v) --> u = v,
instead of the commented correct version,
!u. !v. (!x. x IN u <-> x IN v) --> u = v

`In my main file, I have the theorem stated before another axiom because
``I don't want the axiom to be used to prove the theorem.
`

`Well, in my tester file, where the negation of the theorem is being
``tested by Nitpick and Sledgehammer, spass and e found proofs for the
``negation using my additional axiom, though yices and Z3 didn't.
`

`Lesson? Axioms. You don't want them, which has been addressed. If you
``use them, be afraid. Very afraid.
`

`Additional lesson? I want to put back in some of those provers to see
``who can find the inconsistency and who can't.
`
The prover e tells me:

`"The prover found a type-unsound proof ... even though a supposedly
``type-sound encoding was used (or, less likely, your axioms are
``inconsistent). Please report this to the Isabelle developers."
`

`We understand that Jasmin or another develop had his peers in mind when
``he said, "or, less likely, your axioms are inconsistent".
`

`I choose the spass metis theorem. After inserting it, in the output
``window, it tells me "Metis: the assumptions are inconsistent".
`

`I comment out the wrong formula and un-comment the right formula. The
``theorem is proved, and nothing else shows up wrong at this point.
`

`Sledgehammer or Nitpick completing their attempts is slowest when I try
``to disprove what's true, and try to prove what's not true.
`
Of course, I have the timeouts for both set to 120 seconds.

`I need to experiment on Linux under VirtualBox to see what kind of
``performance I get. I dread setting it all up, and that kind of setup
``isn't totally trouble free either.
`
Regards,
GB

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