Re: [isabelle] Sledgehammer and Nitpick from the command line?



On 7/29/2012 4:27 AM, Jens Doll wrote:
Hello Gottfried,
here is a little warning concerning ancient JVMs:
I installed I3p on my Win7 64bit machine and it contained an older JVM, which was also installed. Afterwards the JVM *tried to open ports* on my machine and my *printer configuration was corrupted*.

Jens,

At least with Windows, installing Java is near effortless. In trying to get Suse, Fedora, and Ubuntu going under VirtualBox, I thought I was going to have to install Java, and it's not effortless because Sun Java is never part of the install these days, and they replace Sun Java with openSDK Java.
*
JAVA INCLUDED WITH BOTH CYGWIN & LINUX*

Last year I ran Isabelle2011 under Ubuntu, and I had to install Sun Java to do it, which sudo makes reasonably easy, but you have to hunt down a site for sudo to get it from, and such a site is never going to be an official download site, so installing Sun Java on Linux can become a security risk.

Somewhere in the process of installing Linux distributions this year, the thought occurred to me, "Hmmm, I wonder if Makarius put the JVM runtime under contrib for the linux distribution." I opened up Isabelle2012_bundle_x86_64-linux.tar.gz, and there I saw the folder jdk-6u31_x86_64-linux. Thanks Makarius for no installation necessary on the big components, like Cygwin and Java, which the user used to have to intall, Cygwin not being straightforward at all, and Sun Java on Linux not being straightforward.

One thing that used to concern me was Java constantly updating itself. I'd think, "I better keep these old Windows Java install files because a Java update could break Isabelle." Now the Java runtime version gets fixed for a particular version of Isabelle.

*NORTON QUIT DELETING ISABELLE.EXE*

The thread "Windows Command Line 2012" brought my attention back to "Isabelle.exe" which is now run to start Isabelle.

I thought maybe I had messed up my Isabelle2012 install, so I reinstalled it again, and found out that Norton now finds "Isabelle.exe" acceptable.

One of Norton's scan methods is "reputation". So if Norton thinks a program is acting suspicious, and the program has no reputation because it's a new release, then it quarantines the program. Norton File Insight now tells me about "Isabelle.exe":

1) Very Few Users: Fewer than 5 users in the Norton Community have used this file.
2) Mature: This file was released 1 month ago.
3) Good: Norton has given this file a favorable ratting.

At the time Norton was deleting Isabelle.exe, the rating was "unknown" because Norton knew nothing about the "Isabelle.exe".

*OTHER ANTIVIRUS INFORMATION*

I could use free antivirus software, but Norton has protected me for several years, so I go to a local chain store and pay $40 for a 3 computer license of Norton 360 instead of paying $59 or $89 on their site. Plus, I think they have one of the better firewalls.

Developers playing tricks to get Linux/Unix programs to run on Windows take a chance on getting them blocked by antivirus programs. I've never had Norton ever complain about Cygwin, but it's a native or semi-native application of Windows, based on what I know about it.

The "alt_ergo" executable "alt-ergo-0.94-mingw.exe" got rejected by Norton, so minGW executables can get the reject.

A couple of months ago, Norton deleted the install file for the Coq beta version, which I was trying to use in conjunction with a type theory book. I unquarantined the Coq installer and installed it, then when experimenting with it, I selected "compile" from some menu and Norton shut down the compile executable and deleted it. I figured I didn't need to be doing taht anyway, so I uninstalled Coq, to wait for another day.

Anyway, a person intent on using a program can tell the antivirus program to unblock it, but people trying out a new program will reject it if it ends up being too much trouble.

*COMPILING PROVERS FOR CYGWIN and E's SLOW STARTUP*

The reason I reinstalled Isabelle2012 was because I had been seeing eprover.exe show up as a process, but then it stopped showing up.

It turns out that eprover.exe takes a little over 35 seconds to start up on Cygwin. I had switched to using a timeout of 30 seconds, and I had installed gcc and OCaml for Cygwin, so I thought I might have messed up the Cygwin under the contrib folder, but that wasn't the case

I successfully compiled leo2, satallax, why3, and alt-ergo for Cygwin.

Leo2 built with no hassles. I had problems with the first try of satallax, but I retried with new, untarred sources, and it magically built per the instructions.

For alt-ergo, I had to build why3. Why3 got some kind of error at the end, but a "make install" still seemed to make it work good enough.

There's a minGW exe for alt-ergo, but I rebuilt it because when I run alt-ergo with the minGW exe, I get this error:

    "alt_ergo": A prover error occurred:
   Unknown input format: tff1

To build a Cygwin binary for alt-ergo, I had to build "ocamlgraph", and the key to success there was not building the GUI, and to get the correct make file, I had to uninstall the GTK library that was causing problems.

I get the same error with the Cygwin binary, so after reading the description of alt-ergo, I assume alt-ergo does some specialized proving.

*VAMPIRE 0.6 FOR CYGWIN, INSTALLING LINUX TO GET VAMPIRE*

Trying to run Vampire for Cygwin, I get this error:

    "vampire": A prover error occurred:
    User error: forced_options is not a valid option

The Cygwin version is 0.6, and I assume the Linux version is 1.8.

The latest version of Vampire is the local prover that I can't on Cygwin. It seems a shame to have to have to install Linux to get it, when I have all the other local provers, but Vampire appears to be one of the best for first-order logic:

http://www.cs.miami.edu/~tptp/CASC/J6/WWWFiles/DivisionSummary1.html <http://www.cs.miami.edu/%7Etptp/CASC/J6/WWWFiles/DivisionSummary1.html>

I got that link off of the satallax web page:

http://www.ps.uni-saarland.de/~cebrown/satallax/ <http://www.ps.uni-saarland.de/%7Ecebrown/satallax/>

Satallax seems to be at a distinct disadvantage when competing in prover competitions with Sledgehammer, considering that Sledgehammer uses Satallax, in addition to many other provers.

*CREATING 10 FILES TO TEST ONE THEOREM*

I finish up my "the user reports back from the field on using Sledgehammer and Nitpick to test theorems".

First, when using Sledgehammer and Nitpick in jEdit, where "sledgehammer" (or nitpick) is the only proof command in a file, it helps to know that there are only three states:

1) Sledgehammer is running because a "sledgehammer" command exists in the file, and Sledgehammer hasn't finished.

2) Sledgehammer has finished running, the results are in the output panel, and nothing has been done to the jEdit session to make Sledgehammer start over, where Sledgehammer starting over will erase the old results. "Anything" could be editing the file in any way, or working in another file that's also visible in the same jEdit process. The safest way to keep Sledgehammer from starting over is to only scroll through the Sledgehammer results until you know you don't want them anymore. That can be a problem when Sledgehammer is constantly updating its results, but I foresee only running Sledgehammer for hours and hours when no results are being found.

3) Sledgehammer is prevented from running because a "sledgehammer" command doesn't exist in the file, where deleting a "sledgehammer" command will cause the continuous prover to terminate the prover processes that are running. (Deleting running sledgehammer commands before closing a file or closing jEdit is the best thing to do.)

There are commands in the Sledgehammer manual, such as "sledgehammer running_provers", but that doesn't apply to jEdit that I can tell. If I try to run such a command, sledgehammer immediately starts over. I actually use this eagerness of sledgehammer to start as a way to use it like a batch file.

Okay, so to test one theorem and its negation, I create 10 different files that all import their own copy of the main THY file. These 10 files get loaded into 10 different jEdit sessions, where I use the switch "-j -settings=/.isabelle/%ISAVERSION%/jedit%1" to tell jEdit where to store the settings, which require me to copy my main home jEdit folder to 10 different folders, such as /users/me/.isabelle/Isabelle2012/jedit1.

I break the test out into 10 files because I want to learn how the different provers work, want to close jEdit for provers which have finished, and I want to terminate and start provers without causing other provers to start over.

Right now, I'm grouping them like this:

  (*1 e spass_new remote_vampire remote_e_sine remote_iprover_eq*)
(*2 z3_tptp spass metis vampire remote_e_tofof remote_iprover remote_snark*)
  (*3 z3 yices cvc3 smt alt_ergo remote_waldmeister*)
  (*4 satallax leo2*)
(*5 remote_leo2 remote_satallax remote_e remote_z3_tptp remote_cvc3 remote_z3*)

Groups 1 and 2 are first-order provers, and I break them up because "e" is going to run as long as I let it.

Group 3 is mainly the SMT provers.

Group 4 is the higher-order provers, and they'll run as long as I let them. Group 5 is the remote duplicates.

My WinEdt script can create some or all of the 10 files, and then for each file created, it calls a new process of jEdit using a corresponding settings folder. Sledgehammer and nitpick start automatically if a "sledgehammer" or "nitpick" command is in the file. I arrange the 10 windows where I want them, and jEdit will remember the settings.

I set the default for both Sledgehammer and Nitpick at 48 hours. The idea is that I can always terminate by deleting the sledgehammer or nitpick command, but it will always take me, say, 10 minutes to pick up where a test left off if it finished after 10 minutes.

Not knowing how the provers work, I assume the first x minutes for a prover is always the same. So a prover run for 1 hour twice is only a 1 hour test, where a 2 hour test has done something different the second hour than the first.

As it turns out, most of the provers give up fairly quickly on the simple theorem I've been testing them with, and so I can close that jEdit process to free up memory, or use it to further experiment with Sledgehammer or Nitpick, without affecting other running processes.

The provers e, leo2, and satallax seem to be willing to run forever. The others, along with Nitpick, give up more readily.

Running these provers like this can be useful. I sometimes go down all sorts of erroneous, confusing paths because I make a change I forget about. In my simple theory, I had commented out the right axiom and put in a modified version of it. My theorem had been proved, but when I ran sledgehammer on the negation of the theorem, the negation was also proved. It then took me about a minute to see that it was because I had commented out the right axiom, and I was given a small logic lesson at that time. That event is what led me to come up with this script to make it convenient, fast, and practical to run Sledgehammer as a test in many ways.

That's the unofficial report from the user in the field. In case anyone is interested, I attach my WinEdit script, include one of the batch file and bash file combinations as an example, and include one of the generated files as an example.

As a quick solution, I get Cygwin Isabelle running on my desktop and network it to my laptop. I'll eventually try to get Linux running on it and networked so I can get Vampire under Linux. These new Linux desktops come up with almost nothing on the desktop. No icons to a terminal window. No button in the task bar to find applications. It totally defeats the purpose of a GUI interface to make it easy to use Linux without searching on the web for documentation.

I make a comment about Python under jEdit. I hate the idea of learning the jEdit scripting language. I'd rather invest my time in learning a scripting language like Python. Maybe I'll try these jEdit plugins for Python (or maybe I'll learn jEdit's language):

http://plugins.jedit.org/plugins/?JythonInterpreter

http://plugins.jedit.org/plugins/?PythonShell

Regards,
GB


*(THE BATCH FILE, CAN'T BE AN ATTACHMENT)*

12_jedit_set.bat

::Cygwin uses this home
   set HOME=E:\E_main\02-p\pi\home
::Isabelle uses this home
   set USER_HOME=/cygdrive/e/E_main/02-p/pi/home
::Various
   set ISAVERSION=Isabelle2012
   set PATH=E:\E_main2\binp\%ISAVERSION%\bin;%PATH%
   set CHERE_INVOKING=true
::jEdit options, "-j -settings /path" will put and use jEdit settings in %USERPROFILE%\path
   set JEDITOPTIONS=-j -settings=/.isabelle/%ISAVERSION%/jedit%1
::Get command line arg for bash
   cd %2
   set JEDITFILE=%3

E:\E_main2\binp\%ISAVERSION%\contrib\cygwin-1.7.9\bin\bash --login -i %0.bash

*BASH FILE*

12_jedit_set.bat.bash

#!/usr/bin/env bash
#
########################################################
# $ISAVERSION is set in the batch file that calls this.
########################################################
printenv
/cygdrive/e/E_main2/binp/$ISAVERSION/bin/isabelle jedit $JEDITOPTIONS $JEDITFILE

*THEORY FILE*

theory z0_2_neg_FO
imports z0_2
begin
nitpick_params[timeout=172800,sat_solver=Lingeling_JNI,verbose,user_axioms]
sledgehammer_params[timeout=172800,verbose,debug=false,isar_proof,provers="
  e spass_new remote_vampire remote_e_sine remote_iprover_eq
"]
  (*1 e spass_new remote_vampire remote_e_sine remote_iprover_eq*)
(*2 vampire z3_tptp spass metis remote_e_tofof remote_iprover remote_snark*)
  (*3 z3 yices cvc3 smt alt_ergo remote_waldmeister*)
  (*4 satallax leo2*)
(*5 remote_leo2 remote_satallax remote_e remote_z3_tptp remote_cvc3 remote_z3*)

theorem neg_FO__emS_is_unique --"~(The empty set is unique.)":
  "~(\<forall>u. (\<forall>x. x nIN u) \<longrightarrow> u = emS)"
  apply(auto)
  sledgehammer
  oops
end







nitpick_params[timeout=172800,sat_solver=Lingeling_JNI,verbose,user_axioms]
sledgehammer_params[timeout=172800,verbose,debug=false,isar_proof,provers=""]
  (*1 e spass_new remote_vampire remote_e_sine remote_iprover_eq*)
  (*2 vampire z3_tptp spass metis remote_e_tofof remote_iprover remote_snark*)
  (*3 z3 yices cvc3 smt alt_ergo remote_waldmeister*)
  (*4 satallax leo2*)
  (*5 remote_leo2 remote_satallax remote_e remote_z3_tptp remote_cvc3 remote_z3*)

// Compiles Selected Text with LaTeX in "_temp%T" file.
  Requires(20040113); // Requires this build of WinEdt to work properly
  SaveRegisters(1111111111); // Clean Macro writing...

CMD('Save');
SetOK(1);  // Just in case ...
SetErrorFlag(0);
StartWorking("Make tester file...");

// Reg 4: default file name number
// Reg 5: the tester file name
// Reg 0,1,2: Temporary working registers
// Reg 9: Stores user's highlighted theorem text


// Get Selected Text in %!9
GetSel(1,9);
// Get the filename suffix.
GetString(`Enter filename number suffix.`,`File number`,"0");
LetReg(4,"%!?");  // for the file name number, like z0.thy
LetReg(5,"z%!4"); // the tester file name
// Get what test to start at.
GetString(`Enter beginning test number.`,`Test number`,"1");
JMP(`TEST%!?`);

/////////////////////////////////////////
// THEOREM: FIRST-ORDER SLEDGE GROUP 1
/////////////////////////////////////////
:TEST1::
Prompt("%!5_1_lem_FO.thy in jEdit?",1,4,"","JMP(`TEST2`);","JMP(`Exit`);");
// create import file from the main file
CopyFile("%p\%n.thy", "%p\%!5_1.thy",1,0)
ReadFile("%p\%!5_1.thy",0);
SubstituteInString("%!0",`theory+[ ]\(0+[a-zA-Z0-9_]\)`,`theory %!5_1`,111,0);
SubstituteInString("%!0",`"\.\.*/pi/I"`,``,111,0);
WriteFile("%p\%!5_1.thy","%!0");
// create the particular test file
OpenOutput("%p\%!5_1_lem_FO.thy");
WrL("theory %!5_1_lem_FO");
WrL("imports %!5_1");
WrL("begin");
// Put in nitpick params, sledge params, and commented out provers
ReadFile("%b\Macros\+isar-sml\util\NiSl.edt",1);
WrL("%!1");
// put the theorem in
SubstituteInString("%!9",">
\(0{theorem|lemma}+[ ]\)>
\(1+[0-9a-zA-Z_'^\\\<\>]\)>
\(2+[ :\-]\)>
","\0lem_FO__\1\2",111,0);
WrL("%!0");
WrL("  apply(auto)");
WrL(|  sledgehammer|);
WrL(|  oops|);
WrL("end");
WrL;
CloseOutput;
// Put the right group of provers in from %!1 above
ReadFile("%p\%!5_1_lem_FO.thy",0);
SubstituteInString("%!1",`**(\*1 \(0**\)\*)**`,`  \0`,111,1); //delete what I don't want
SubstituteInString("%!0",`\(0provers="\)**\(1"]\)`,`\0>%!1>\1`,111,0);
WriteFile("%p\%!5_1_lem_FO.thy","%!0");
Run(|%@('2p');\pi\home\bin\12_jedit_set.bat 1 %p %!5_1_lem_FO.thy|,'',0,0,'%!5_1_lem_FO',0,0);


/////////////////////////////////////////
// NEGATION: FIRST-ORDER SLEDGE THE NEG GROUP 1
/////////////////////////////////////////
:TEST2::
Prompt("%!5_2_neg_FO.thy in jEdit?",1,4,"","JMP(`TEST3`);","JMP(`Exit`);");
// create import file from the main file
CopyFile("%p\%n.thy", "%p\%!5_2.thy",1,0)
ReadFile("%p\%!5_2.thy",0);
SubstituteInString("%!0",`theory+[ ]\(0+[a-zA-Z0-9_]\)`,`theory %!5_2`,111,0);
SubstituteInString("%!0",`"\.\.*/pi/I"`,``,111,0);
WriteFile("%p\%!5_2.thy","%!0");
// create the particular test file
OpenOutput("%p\%!5_2_neg_FO.thy");
WrL("theory %!5_2_neg_FO");
WrL("imports %!5_2");
WrL("begin");
// Put in nitpick params, sledge params, and commented out provers
ReadFile("%b\Macros\+isar-sml\util\NiSl.edt",1);
WrL("%!1");
// put the theorem in
SubstituteInString("%!9",">
\(0{theorem|lemma}+[ ]\)>
\(1+[0-9a-zA-Z_'^\\\<\>]\)>
\(2+[ :\-]\)>
","\0neg_FO__\1\2",111,0);
//Negate it
SubstituteInString("%!0",`"\(0*\)"`,`"\~(\0)"`,111,0);
WrL("%!0");
WrL("  apply(auto)");
WrL(|  sledgehammer|);
WrL(|  oops|);
WrL("end");
WrL;
CloseOutput;
// Put the right group of provers in from %!1 above
ReadFile("%p\%!5_2_neg_FO.thy",0);
SubstituteInString("%!1",`**(\*1 \(0**\)\*)**`,`  \0`,111,1); //delete what I don't want
SubstituteInString("%!0",`\(0provers="\)**\(1"]\)`,`\0>%!1>\1`,111,0);
WriteFile("%p\%!5_2_neg_FO.thy","%!0");
Run(|%@('2p');\pi\home\bin\12_jedit_set.bat 2 %p %!5_2_neg_FO.thy|,'',0,0,'%!5_2_neg_FO',0,0);

/////////////////////////////////////////
// THEOREM: FIRST-ORDER SLEDGE  GROUP 2
/////////////////////////////////////////
:TEST3::
Prompt("%!5_3_lem_FO.thy in jEdit?",1,4,"","JMP(`TEST4`);","JMP(`Exit`);");
// create import file from the main file
CopyFile("%p\%n.thy", "%p\%!5_3.thy",1,0)
ReadFile("%p\%!5_3.thy",0);
SubstituteInString("%!0",`theory+[ ]\(0+[a-zA-Z0-9_]\)`,`theory %!5_3`,111,0);
SubstituteInString("%!0",`"\.\.*/pi/I"`,``,111,0);
WriteFile("%p\%!5_3.thy","%!0");
// create the particular test file
OpenOutput("%p\%!5_3_lem_FO.thy");
WrL("theory %!5_3_lem_FO");
WrL("imports %!5_3");
WrL("begin");
// Put in nitpick params, sledge params, and commented out provers
ReadFile("%b\Macros\+isar-sml\util\NiSl.edt",1);
WrL("%!1");
// put the theorem in
SubstituteInString("%!9",">
\(0{theorem|lemma}+[ ]\)>
\(1+[0-9a-zA-Z_'^\\\<\>]\)>
\(2+[ :\-]\)>
","\0lem_FO__\1\2",111,0);
WrL("%!0");
WrL("  apply(auto)");
WrL(|  sledgehammer|);
WrL(|  oops|);
WrL("end");
WrL;
CloseOutput;
// Put the right group of provers in from %!1 above
ReadFile("%p\%!5_3_lem_FO.thy",0);
SubstituteInString("%!1",`**(\*2 \(0**\)\*)**`,`  \0`,111,1); //delete what I don't want
SubstituteInString("%!0",`\(0provers="\)**\(1"]\)`,`\0>%!1>\1`,111,0);
WriteFile("%p\%!5_3_lem_FO.thy","%!0");
Run(|%@('2p');\pi\home\bin\12_jedit_set.bat 3 %p %!5_3_lem_FO.thy|,'',0,0,'%!5_3_lem_FO',0,0);


/////////////////////////////////////////
// NEGATION: FIRST-ORDER SLEDGE THE NEG GROUP 2
/////////////////////////////////////////
:TEST4::
Prompt("%!5_4_neg_FO.thy in jEdit?",1,4,"","JMP(`TEST5`);","JMP(`Exit`);");
// create import file from the main file
CopyFile("%p\%n.thy", "%p\%!5_4.thy",1,0)
ReadFile("%p\%!5_4.thy",0);
SubstituteInString("%!0",`theory+[ ]\(0+[a-zA-Z0-9_]\)`,`theory %!5_4`,111,0);
SubstituteInString("%!0",`"\.\.*/pi/I"`,``,111,0);
WriteFile("%p\%!5_4.thy","%!0");
// create the particular test file
OpenOutput("%p\%!5_4_neg_FO.thy");
WrL("theory %!5_4_neg_FO");
WrL("imports %!5_4");
WrL("begin");
// Put in nitpick params, sledge params, and commented out provers
ReadFile("%b\Macros\+isar-sml\util\NiSl.edt",1);
WrL("%!1");
// put the theorem in
SubstituteInString("%!9",">
\(0{theorem|lemma}+[ ]\)>
\(1+[0-9a-zA-Z_'^\\\<\>]\)>
\(2+[ :\-]\)>
","\0neg_FO__\1\2",111,0);
//Negate it
SubstituteInString("%!0",`"\(0*\)"`,`"\~(\0)"`,111,0);
WrL("%!0");
WrL("  apply(auto)");
WrL(|  sledgehammer|);
WrL(|  oops|);
WrL("end");
WrL;
CloseOutput;
// Put the right group of provers in from %!1 above
ReadFile("%p\%!5_4_neg_FO.thy",0);
SubstituteInString("%!1",`**(\*2 \(0**\)\*)**`,`  \0`,111,1); //delete what I don't want
SubstituteInString("%!0",`\(0provers="\)**\(1"]\)`,`\0>%!1>\1`,111,0);
WriteFile("%p\%!5_4_neg_FO.thy","%!0");
Run(|%@('2p');\pi\home\bin\12_jedit_set.bat 4 %p %!5_4_neg_FO.thy|,'',0,0,'%!5_4_neg_FO',0,0);


/////////////////////////////////////////
// NITPICK THE THEOREM (set up for satallax leo2)
/////////////////////////////////////////
:TEST5::
Prompt("%!5_5_lem_NIT.thy in jEdit?",1,4,"","JMP(`TEST6`);","JMP(`Exit`);");
// create import file from the main file
CopyFile("%p\%n.thy", "%p\%!5_5.thy",1,0)
ReadFile("%p\%!5_5.thy",0);
SubstituteInString("%!0",`theory+[ ]\(0+[a-zA-Z0-9_]\)`,`theory %!5_5`,111,0);
SubstituteInString("%!0",`"\.\.*/pi/I"`,``,111,0);
WriteFile("%p\%!5_5.thy","%!0");
// create the particular test file
OpenOutput("%p\%!5_5_lem_NIT.thy");
WrL("theory %!5_5_lem_NIT");
WrL("imports %!5_5");
WrL("begin");
// Put in nitpick params, sledge params, and commented out provers
ReadFile("%b\Macros\+isar-sml\util\NiSl.edt",1);
WrL("%!1");
// put the theorem in
SubstituteInString("%!9",">
\(0{theorem|lemma}+[ ]\)>
\(1+[0-9a-zA-Z_'^\\\<\>]\)>
\(2+[ :\-]\)>
","\0lem_NIT__\1\2",111,0);
WrL("%!0");
WrL(|  nitpick|);
WrL(|  oops|);
WrL("end");
WrL;
CloseOutput;
// Put the right group of provers in from %!1 above
ReadFile("%p\%!5_5_lem_NIT.thy",0);
SubstituteInString("%!1",`**(\*4 \(0**\)\*)**`,`  \0`,111,1); //delete what I don't want
SubstituteInString("%!0",`\(0provers="\)**\(1"]\)`,`\0>%!1>\1`,111,0);
WriteFile("%p\%!5_5_lem_NIT.thy","%!0");
Run(|%@('2p');\pi\home\bin\12_jedit_set.bat 5 %p %!5_5_lem_NIT.thy|,'',0,0,'%!5_5_lem_NIT',0,0);


/////////////////////////////////////////
// NITPICK THE NEGATION (set up for satallax leo2)
/////////////////////////////////////////
:TEST6::
Prompt("%!5_6_neg_NIT.thy in jEdit?",1,4,"","JMP(`TEST7`);","JMP(`Exit`);");
// create import file from the main file
CopyFile("%p\%n.thy", "%p\%!5_6.thy",1,0)
ReadFile("%p\%!5_6.thy",0);
SubstituteInString("%!0",`theory+[ ]\(0+[a-zA-Z0-9_]\)`,`theory %!5_6`,111,0);
SubstituteInString("%!0",`"\.\.*/pi/I"`,``,111,0);
WriteFile("%p\%!5_6.thy","%!0");
// create the particular test file
OpenOutput("%p\%!5_6_neg_NIT.thy");
WrL("theory %!5_6_neg_NIT");
WrL("imports %!5_6");
WrL("begin");
// Put in nitpick params, sledge params, and commented out provers
ReadFile("%b\Macros\+isar-sml\util\NiSl.edt",1);
WrL("%!1");
// put the theorem in
SubstituteInString("%!9",">
\(0{theorem|lemma}+[ ]\)>
\(1+[0-9a-zA-Z_'^\\\<\>]\)>
\(2+[ :\-]\)>
","\0neg_NIT__\1\2",111,0);
//Negate it
SubstituteInString("%!0",`"\(0*\)"`,`"\~(\0)"`,111,0);
WrL("%!0");
WrL(|  nitpick|);
WrL(|  oops|);
WrL("end");
WrL;
CloseOutput;
// Put the right group of provers in from %!1 above
ReadFile("%p\%!5_6_neg_NIT.thy",0);
SubstituteInString("%!1",`**(\*4 \(0**\)\*)**`,`  \0`,111,1); //delete what I don't want
SubstituteInString("%!0",`\(0provers="\)**\(1"]\)`,`\0>%!1>\1`,111,0);
WriteFile("%p\%!5_6_neg_NIT.thy","%!0");
Run(|%@('2p');\pi\home\bin\12_jedit_set.bat 6 %p %!5_6_neg_NIT.thy|,'',0,0,'%!5_6_neg_NIT',0,0);


/////////////////////////////////////////
// THEOREM: SMT SLEDGE THE THEOREM
/////////////////////////////////////////
:TEST7::
Prompt("%!5_7_lem_SMT.thy in jEdit?",1,4,"","JMP(`TEST8`);","JMP(`Exit`);");
// create import file from the main file
CopyFile("%p\%n.thy", "%p\%!5_7.thy",1,0)
ReadFile("%p\%!5_7.thy",0);
SubstituteInString("%!0",`theory+[ ]\(0+[a-zA-Z0-9_]\)`,`theory %!5_7`,111,0);
SubstituteInString("%!0",`"\.\.*/pi/I"`,``,111,0);
WriteFile("%p\%!5_7.thy","%!0");
// create the particular test file
OpenOutput("%p\%!5_7_lem_SMT.thy");
WrL("theory %!5_7_lem_SMT");
WrL("imports %!5_7");
WrL("begin");
// Put in nitpick params, sledge params, and commented out provers
ReadFile("%b\Macros\+isar-sml\util\NiSl.edt",1);
WrL("%!1");
// put the theorem in
SubstituteInString("%!9",">
\(0{theorem|lemma}+[ ]\)>
\(1+[0-9a-zA-Z_'^\\\<\>]\)>
\(2+[ :\-]\)>
","\0lem_SMT__\1\2",111,0);
WrL("%!0");
WrL("  apply(auto)");
WrL(|  sledgehammer|);
WrL(|  oops|);
WrL("end");
WrL;
CloseOutput;
// Put the right group of provers in from %!1 above
ReadFile("%p\%!5_7_lem_SMT.thy",0);
SubstituteInString("%!1",`**(\*3 \(0**\)\*)**`,`  \0`,111,1); //delete what I don't want
SubstituteInString("%!0",`\(0provers="\)**\(1"]\)`,`\0>%!1>\1`,111,0);
WriteFile("%p\%!5_7_lem_SMT.thy","%!0");
Run(|%@('2p');\pi\home\bin\12_jedit_set.bat 7 %p %!5_7_lem_SMT.thy|,'',0,0,'%!5_7_lem_SMT',0,0);


/////////////////////////////////////////
// NEGATION: SMT SLEDGE THE NEG
/////////////////////////////////////////
:TEST8::
Prompt("%!5_8_neg_SMT.thy in jEdit?",1,4,"","JMP(`TEST9`);","JMP(`Exit`);");
// create import file from the main file
CopyFile("%p\%n.thy", "%p\%!5_8.thy",1,0)
ReadFile("%p\%!5_8.thy",0);
SubstituteInString("%!0",`theory+[ ]\(0+[a-zA-Z0-9_]\)`,`theory %!5_8`,111,0);
SubstituteInString("%!0",`"\.\.*/pi/I"`,``,111,0);
WriteFile("%p\%!5_8.thy","%!0");
// create the particular test file
OpenOutput("%p\%!5_8_neg_SMT.thy");
WrL("theory %!5_8_neg_SMT");
WrL("imports %!5_8");
WrL("begin");
// Put in nitpick params, sledge params, and commented out provers
ReadFile("%b\Macros\+isar-sml\util\NiSl.edt",1);
WrL("%!1");
// put the theorem in
SubstituteInString("%!9",">
\(0{theorem|lemma}+[ ]\)>
\(1+[0-9a-zA-Z_'^\\\<\>]\)>
\(2+[ :\-]\)>
","\0neg_SMT__\1\2",111,0);
//Negate it
SubstituteInString("%!0",`"\(0*\)"`,`"\~(\0)"`,111,0);
WrL("%!0");
WrL("  apply(auto)");
WrL(|  sledgehammer|);
WrL(|  oops|);
WrL("end");
WrL;
CloseOutput;
// Put the right group of provers in from %!1 above
ReadFile("%p\%!5_8_neg_SMT.thy",0);
SubstituteInString("%!1",`**(\*3 \(0**\)\*)**`,`  \0`,111,1); //delete what I don't want
SubstituteInString("%!0",`\(0provers="\)**\(1"]\)`,`\0>%!1>\1`,111,0);
WriteFile("%p\%!5_8_neg_SMT.thy","%!0");
Run(|%@('2p');\pi\home\bin\12_jedit_set.bat 8 %p %!5_8_neg_SMT.thy|,'',0,0,'%!5_8_neg_SMT',0,0);

/////////////////////////////////////////
// THEOREM: HOL SLEDGE THE THEOREM
/////////////////////////////////////////
:TEST9::
Prompt("%!5_9_lem_HOL.thy in jEdit?",1,4,"","JMP(`TEST10`);","JMP(`Exit`);");
// create import file from the main file
CopyFile("%p\%n.thy", "%p\%!5_9.thy",1,0)
ReadFile("%p\%!5_9.thy",0);
SubstituteInString("%!0",`theory+[ ]\(0+[a-zA-Z0-9_]\)`,`theory %!5_9`,111,0);
SubstituteInString("%!0",`"\.\.*/pi/I"`,``,111,0);
WriteFile("%p\%!5_9.thy","%!0");
// create the particular test file
OpenOutput("%p\%!5_9_lem_HOL.thy");
WrL("theory %!5_9_lem_HOL");
WrL("imports %!5_9");
WrL("begin");
// Put in nitpick params, sledge params, and commented out provers
ReadFile("%b\Macros\+isar-sml\util\NiSl.edt",1);
WrL("%!1");
// put the theorem in
SubstituteInString("%!9",">
\(0{theorem|lemma}+[ ]\)>
\(1+[0-9a-zA-Z_'^\\\<\>]\)>
\(2+[ :\-]\)>
","\0lem_HOL__\1\2",111,0);
WrL("%!0");
WrL("  apply(auto)");
WrL(|  sledgehammer|);
WrL(|  oops|);
WrL("end");
WrL;
CloseOutput;
// Put the right group of provers in from %!1 above
ReadFile("%p\%!5_9_lem_HOL.thy",0);
SubstituteInString("%!1",`**(\*4 \(0**\)\*)**`,`  \0`,111,1); //delete what I don't want
SubstituteInString("%!0",`\(0provers="\)**\(1"]\)`,`\0>%!1>\1`,111,0);
WriteFile("%p\%!5_9_lem_HOL.thy","%!0");
Run(|%@('2p');\pi\home\bin\12_jedit_set.bat 9 %p %!5_9_lem_HOL.thy|,'',0,0,'%!5_9_lem_HOL',0,0);


/////////////////////////////////////////
// NEGATION: HOL SLEDGE THE NEG
/////////////////////////////////////////
:TEST10::
Prompt("%!5_10_neg_HOL.thy in jEdit?",1,4,"","JMP(`Exit`);","JMP(`Exit`);");
// create import file from the main file
CopyFile("%p\%n.thy", "%p\%!5_10.thy",1,0)
ReadFile("%p\%!5_10.thy",0);
SubstituteInString("%!0",`theory+[ ]\(0+[a-zA-Z0-9_]\)`,`theory %!5_10`,111,0);
SubstituteInString("%!0",`"\.\.*/pi/I"`,``,111,0);
WriteFile("%p\%!5_10.thy","%!0");
// create the particular test file
OpenOutput("%p\%!5_10_neg_HOL.thy");
WrL("theory %!5_10_neg_HOL");
WrL("imports %!5_10");
WrL("begin");
// Put in nitpick params, sledge params, and commented out provers
ReadFile("%b\Macros\+isar-sml\util\NiSl.edt",1);
WrL("%!1");
// put the theorem in
SubstituteInString("%!9",">
\(0{theorem|lemma}+[ ]\)>
\(1+[0-9a-zA-Z_'^\\\<\>]\)>
\(2+[ :\-]\)>
","\0neg_HOL__\1\2",111,0);
//Negate it
SubstituteInString("%!0",`"\(0*\)"`,`"\~(\0)"`,111,0);
WrL("%!0");
WrL("  apply(auto)");
WrL(|  sledgehammer|);
WrL(|  oops|);
WrL("end");
WrL;
CloseOutput;
// Put the right group of provers in from %!1 above
ReadFile("%p\%!5_10_neg_HOL.thy",0);
SubstituteInString("%!1",`**(\*4 \(0**\)\*)**`,`  \0`,111,1); //delete what I don't want
SubstituteInString("%!0",`\(0provers="\)**\(1"]\)`,`\0>%!1>\1`,111,0);
WriteFile("%p\%!5_10_neg_HOL.thy","%!0");
Run(|%@('2p');\pi\home\bin\12_jedit_set.bat 10 %p %!5_10_neg_HOL.thy|,'',0,0,'%!5_10_neg_HOL',0,0);



Prompt("Done. Open Explorer?",1,4,"Run('%b\Macros\Open\explorer.bat %p','%p',0,0,'Explorer',1,1);","","JMP(`Exit`);");
:Exit::
End;



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