merged
authorwenzelm
Sat Apr 25 22:29:13 2009 +0200 (2009-04-25)
changeset 30984e6349035148a
parent 30983 e54777ab68bd
parent 30982 7882a1268a48
child 30985 2a22c6613dcf
merged
contrib/SystemOnTPTP/remote
src/Pure/Tools/auto_solve.ML
     1.1 --- a/CONTRIBUTORS	Sat Apr 25 21:42:05 2009 +0200
     1.2 +++ b/CONTRIBUTORS	Sat Apr 25 22:29:13 2009 +0200
     1.3 @@ -7,6 +7,10 @@
     1.4  Contributions to this Isabelle version
     1.5  --------------------------------------
     1.6  
     1.7 +
     1.8 +Contributions to Isabelle2009
     1.9 +-----------------------------
    1.10 +
    1.11  * March 2009: Robert Himmelmann, TUM and Amine Chaieb, University of
    1.12    Cambridge
    1.13    Elementary topology in Euclidean space.
     2.1 --- a/contrib/SystemOnTPTP/remote	Sat Apr 25 21:42:05 2009 +0200
     2.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.3 @@ -1,120 +0,0 @@
     2.4 -#!/usr/bin/env perl
     2.5 -#
     2.6 -# Wrapper for custom remote provers on SystemOnTPTP
     2.7 -# Author: Fabian Immler, TU Muenchen
     2.8 -#
     2.9 -
    2.10 -use warnings;
    2.11 -use strict;
    2.12 -use Getopt::Std;
    2.13 -use HTTP::Request::Common;
    2.14 -use LWP;
    2.15 -
    2.16 -my $SystemOnTPTPFormReplyURL = "http://www.cs.miami.edu/~tptp/cgi-bin/SystemOnTPTPFormReply";
    2.17 -
    2.18 -# default parameters
    2.19 -my %URLParameters = (
    2.20 -    "NoHTML" => 1,
    2.21 -    "QuietFlag" => "-q01",
    2.22 -    "X2TPTP" => "-S",
    2.23 -    "SubmitButton" => "RunSelectedSystems",
    2.24 -    "ProblemSource" => "UPLOAD",
    2.25 -    );
    2.26 -
    2.27 -#----Get format and transform options if specified
    2.28 -my %Options;
    2.29 -getopts("hws:t:c:",\%Options);
    2.30 -
    2.31 -#----Usage
    2.32 -sub usage() {
    2.33 -  print("Usage: remote [<options>] <File name>\n");
    2.34 -  print("    <options> are ...\n");
    2.35 -  print("    -h            - print this help\n");
    2.36 -  print("    -w            - list available ATP systems\n");
    2.37 -  print("    -s<system>    - specified system to use\n");
    2.38 -  print("    -t<timelimit> - CPU time limit for system\n");
    2.39 -  print("    -c<command>   - custom command for system\n");
    2.40 -  print("    <File name>   - TPTP problem file\n");
    2.41 -  exit(0);
    2.42 -}
    2.43 -if (exists($Options{'h'})) {
    2.44 -  usage();
    2.45 -}
    2.46 -#----What systems flag
    2.47 -if (exists($Options{'w'})) {
    2.48 -    $URLParameters{"SubmitButton"} = "ListSystems";
    2.49 -    delete($URLParameters{"ProblemSource"});
    2.50 -}
    2.51 -#----Selected system
    2.52 -my $System;
    2.53 -if (exists($Options{'s'})) {
    2.54 -    $System = $Options{'s'};
    2.55 -} else {
    2.56 -    # use Vampire as default
    2.57 -    $System = "Vampire---9.0";
    2.58 -}
    2.59 -$URLParameters{"System___$System"} = $System;
    2.60 -
    2.61 -#----Time limit
    2.62 -if (exists($Options{'t'})) {
    2.63 -    $URLParameters{"TimeLimit___$System"} = $Options{'t'};
    2.64 -}
    2.65 -#----Custom command
    2.66 -if (exists($Options{'c'})) {
    2.67 -    $URLParameters{"Command___$System"} = $Options{'c'};
    2.68 -}
    2.69 -
    2.70 -#----Get single file name
    2.71 -if (exists($URLParameters{"ProblemSource"})) {
    2.72 -    if (scalar(@ARGV) >= 1) {
    2.73 -        $URLParameters{"UPLOADProblem"} = [shift(@ARGV)];
    2.74 -    } else {
    2.75 -      print("Missing problem file\n");
    2.76 -      usage();
    2.77 -      die;
    2.78 -    }
    2.79 -}
    2.80 -
    2.81 -# Query Server
    2.82 -my $Agent = LWP::UserAgent->new;
    2.83 -if (exists($Options{'t'})) {
    2.84 -  # give server more time to respond
    2.85 -  $Agent->timeout($Options{'t'} + 10);
    2.86 -}
    2.87 -my $Request = POST($SystemOnTPTPFormReplyURL,
    2.88 -	Content_Type => 'form-data',Content => \%URLParameters);
    2.89 -my $Response = $Agent->request($Request);
    2.90 -
    2.91 -#catch errors / failure
    2.92 -if(! $Response->is_success){
    2.93 -  print "HTTP-Error: " . $Response->message . "\n";
    2.94 -  exit(-1);
    2.95 -} elsif (exists($Options{'w'})) {
    2.96 -  print $Response->content;
    2.97 -  exit (0);
    2.98 -} elsif ($Response->content =~ /WARNING: (\S*) does not exist/) {
    2.99 -  print "Specified System $1 does not exist\n";
   2.100 -  exit(-1);
   2.101 -} elsif ($Response->content =~ /%\s*Result\s*:\s*Unsatisfiable.*\n%\s*Output\s*:\s*(CNF)?Refutation.*\n%/) {
   2.102 -  my @lines = split( /\n/, $Response->content);
   2.103 -  my $extract = "";
   2.104 -  foreach my $line (@lines){
   2.105 -      #ignore comments
   2.106 -      if ($line !~ /^%/ && !($line eq "")) {
   2.107 -          $extract .= "$line";
   2.108 -      }
   2.109 -  }
   2.110 -  # insert newlines after ').'
   2.111 -  $extract =~ s/\s//g;
   2.112 -  $extract =~ s/\)\.cnf/\)\.\ncnf/g;
   2.113 -
   2.114 -  # orientation for res_reconstruct.ML
   2.115 -  print "# SZS output start CNFRefutation.\n";
   2.116 -  print "$extract\n";
   2.117 -  print "# SZS output end CNFRefutation.\n";
   2.118 -  exit(0);
   2.119 -} else {
   2.120 -  print "Remote-script could not extract proof:\n".$Response->content;
   2.121 -  exit(-1);
   2.122 -}
   2.123 -
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/lib/scripts/SystemOnTPTP	Sat Apr 25 22:29:13 2009 +0200
     3.3 @@ -0,0 +1,120 @@
     3.4 +#!/usr/bin/env perl
     3.5 +#
     3.6 +# Wrapper for custom remote provers on SystemOnTPTP
     3.7 +# Author: Fabian Immler, TU Muenchen
     3.8 +#
     3.9 +
    3.10 +use warnings;
    3.11 +use strict;
    3.12 +use Getopt::Std;
    3.13 +use HTTP::Request::Common;
    3.14 +use LWP;
    3.15 +
    3.16 +my $SystemOnTPTPFormReplyURL = "http://www.cs.miami.edu/~tptp/cgi-bin/SystemOnTPTPFormReply";
    3.17 +
    3.18 +# default parameters
    3.19 +my %URLParameters = (
    3.20 +    "NoHTML" => 1,
    3.21 +    "QuietFlag" => "-q01",
    3.22 +    "X2TPTP" => "-S",
    3.23 +    "SubmitButton" => "RunSelectedSystems",
    3.24 +    "ProblemSource" => "UPLOAD",
    3.25 +    );
    3.26 +
    3.27 +#----Get format and transform options if specified
    3.28 +my %Options;
    3.29 +getopts("hws:t:c:",\%Options);
    3.30 +
    3.31 +#----Usage
    3.32 +sub usage() {
    3.33 +  print("Usage: remote [<options>] <File name>\n");
    3.34 +  print("    <options> are ...\n");
    3.35 +  print("    -h            - print this help\n");
    3.36 +  print("    -w            - list available ATP systems\n");
    3.37 +  print("    -s<system>    - specified system to use\n");
    3.38 +  print("    -t<timelimit> - CPU time limit for system\n");
    3.39 +  print("    -c<command>   - custom command for system\n");
    3.40 +  print("    <File name>   - TPTP problem file\n");
    3.41 +  exit(0);
    3.42 +}
    3.43 +if (exists($Options{'h'})) {
    3.44 +  usage();
    3.45 +}
    3.46 +#----What systems flag
    3.47 +if (exists($Options{'w'})) {
    3.48 +    $URLParameters{"SubmitButton"} = "ListSystems";
    3.49 +    delete($URLParameters{"ProblemSource"});
    3.50 +}
    3.51 +#----Selected system
    3.52 +my $System;
    3.53 +if (exists($Options{'s'})) {
    3.54 +    $System = $Options{'s'};
    3.55 +} else {
    3.56 +    # use Vampire as default
    3.57 +    $System = "Vampire---9.0";
    3.58 +}
    3.59 +$URLParameters{"System___$System"} = $System;
    3.60 +
    3.61 +#----Time limit
    3.62 +if (exists($Options{'t'})) {
    3.63 +    $URLParameters{"TimeLimit___$System"} = $Options{'t'};
    3.64 +}
    3.65 +#----Custom command
    3.66 +if (exists($Options{'c'})) {
    3.67 +    $URLParameters{"Command___$System"} = $Options{'c'};
    3.68 +}
    3.69 +
    3.70 +#----Get single file name
    3.71 +if (exists($URLParameters{"ProblemSource"})) {
    3.72 +    if (scalar(@ARGV) >= 1) {
    3.73 +        $URLParameters{"UPLOADProblem"} = [shift(@ARGV)];
    3.74 +    } else {
    3.75 +      print("Missing problem file\n");
    3.76 +      usage();
    3.77 +      die;
    3.78 +    }
    3.79 +}
    3.80 +
    3.81 +# Query Server
    3.82 +my $Agent = LWP::UserAgent->new;
    3.83 +if (exists($Options{'t'})) {
    3.84 +  # give server more time to respond
    3.85 +  $Agent->timeout($Options{'t'} + 10);
    3.86 +}
    3.87 +my $Request = POST($SystemOnTPTPFormReplyURL,
    3.88 +	Content_Type => 'form-data',Content => \%URLParameters);
    3.89 +my $Response = $Agent->request($Request);
    3.90 +
    3.91 +#catch errors / failure
    3.92 +if(! $Response->is_success){
    3.93 +  print "HTTP-Error: " . $Response->message . "\n";
    3.94 +  exit(-1);
    3.95 +} elsif (exists($Options{'w'})) {
    3.96 +  print $Response->content;
    3.97 +  exit (0);
    3.98 +} elsif ($Response->content =~ /WARNING: (\S*) does not exist/) {
    3.99 +  print "Specified System $1 does not exist\n";
   3.100 +  exit(-1);
   3.101 +} elsif ($Response->content =~ /%\s*Result\s*:\s*Unsatisfiable.*\n%\s*Output\s*:\s*(CNF)?Refutation.*\n%/) {
   3.102 +  my @lines = split( /\n/, $Response->content);
   3.103 +  my $extract = "";
   3.104 +  foreach my $line (@lines){
   3.105 +      #ignore comments
   3.106 +      if ($line !~ /^%/ && !($line eq "")) {
   3.107 +          $extract .= "$line";
   3.108 +      }
   3.109 +  }
   3.110 +  # insert newlines after ').'
   3.111 +  $extract =~ s/\s//g;
   3.112 +  $extract =~ s/\)\.cnf/\)\.\ncnf/g;
   3.113 +
   3.114 +  # orientation for res_reconstruct.ML
   3.115 +  print "# SZS output start CNFRefutation.\n";
   3.116 +  print "$extract\n";
   3.117 +  print "# SZS output end CNFRefutation.\n";
   3.118 +  exit(0);
   3.119 +} else {
   3.120 +  print "Remote-script could not extract proof:\n".$Response->content;
   3.121 +  exit(-1);
   3.122 +}
   3.123 +
     4.1 --- a/src/HOL/HOL.thy	Sat Apr 25 21:42:05 2009 +0200
     4.2 +++ b/src/HOL/HOL.thy	Sat Apr 25 22:29:13 2009 +0200
     4.3 @@ -8,6 +8,7 @@
     4.4  imports Pure "~~/src/Tools/Code_Generator"
     4.5  uses
     4.6    ("Tools/hologic.ML")
     4.7 +  "~~/src/Tools/auto_solve.ML"
     4.8    "~~/src/Tools/IsaPlanner/zipper.ML"
     4.9    "~~/src/Tools/IsaPlanner/isand.ML"
    4.10    "~~/src/Tools/IsaPlanner/rw_tools.ML"
    4.11 @@ -1921,7 +1922,7 @@
    4.12  quickcheck_params [size = 5, iterations = 50]
    4.13  
    4.14  
    4.15 -subsection {* Nitpick hooks *}
    4.16 +subsection {* Nitpick setup *}
    4.17  
    4.18  text {* This will be relocated once Nitpick is moved to HOL. *}
    4.19  
    4.20 @@ -1947,10 +1948,14 @@
    4.21    val description = "introduction rules for (co)inductive predicates as needed by Nitpick"
    4.22  )
    4.23  *}
    4.24 -setup {* Nitpick_Const_Def_Thms.setup
    4.25 -         #> Nitpick_Const_Simp_Thms.setup
    4.26 -         #> Nitpick_Const_Psimp_Thms.setup
    4.27 -         #> Nitpick_Ind_Intro_Thms.setup *}
    4.28 +
    4.29 +setup {*
    4.30 +  Nitpick_Const_Def_Thms.setup
    4.31 +  #> Nitpick_Const_Simp_Thms.setup
    4.32 +  #> Nitpick_Const_Psimp_Thms.setup
    4.33 +  #> Nitpick_Ind_Intro_Thms.setup
    4.34 +*}
    4.35 +
    4.36  
    4.37  subsection {* Legacy tactics and ML bindings *}
    4.38  
     5.1 --- a/src/HOL/IsaMakefile	Sat Apr 25 21:42:05 2009 +0200
     5.2 +++ b/src/HOL/IsaMakefile	Sat Apr 25 22:29:13 2009 +0200
     5.3 @@ -89,6 +89,7 @@
     5.4    $(SRC)/Tools/IsaPlanner/rw_tools.ML \
     5.5    $(SRC)/Tools/IsaPlanner/zipper.ML \
     5.6    $(SRC)/Tools/atomize_elim.ML \
     5.7 +  $(SRC)/Tools/auto_solve.ML \
     5.8    $(SRC)/Tools/code/code_haskell.ML \
     5.9    $(SRC)/Tools/code/code_ml.ML \
    5.10    $(SRC)/Tools/code/code_name.ML \
     6.1 --- a/src/HOL/Tools/atp_manager.ML	Sat Apr 25 21:42:05 2009 +0200
     6.2 +++ b/src/HOL/Tools/atp_manager.ML	Sat Apr 25 22:29:13 2009 +0200
     6.3 @@ -51,15 +51,17 @@
     6.4  fun set_timeout time = CRITICAL (fn () => timeout := time);
     6.5  
     6.6  val _ =
     6.7 -  ProofGeneralPgip.add_preference "Proof"
     6.8 +  ProofGeneralPgip.add_preference Preferences.category_proof
     6.9      (Preferences.string_pref atps
    6.10        "ATP: provers" "Default automatic provers (separated by whitespace)");
    6.11  
    6.12 -val _ = ProofGeneralPgip.add_preference "Proof"
    6.13 +val _ =
    6.14 +  ProofGeneralPgip.add_preference Preferences.category_proof
    6.15      (Preferences.int_pref max_atps
    6.16        "ATP: maximum number" "How many provers may run in parallel");
    6.17  
    6.18 -val _ = ProofGeneralPgip.add_preference "Proof"
    6.19 +val _ =
    6.20 +  ProofGeneralPgip.add_preference Preferences.category_proof
    6.21      (Preferences.int_pref timeout
    6.22        "ATP: timeout" "ATPs will be interrupted after this time (in seconds)");
    6.23  
     7.1 --- a/src/HOL/Tools/atp_wrapper.ML	Sat Apr 25 21:42:05 2009 +0200
     7.2 +++ b/src/HOL/Tools/atp_wrapper.ML	Sat Apr 25 22:29:13 2009 +0200
     7.3 @@ -1,5 +1,4 @@
     7.4  (*  Title:      HOL/Tools/atp_wrapper.ML
     7.5 -    ID:         $Id$
     7.6      Author:     Fabian Immler, TU Muenchen
     7.7  
     7.8  Wrapper functions for external ATPs.
     7.9 @@ -179,7 +178,7 @@
    7.10  
    7.11  fun remote_prover_opts max_new theory_const args timeout =
    7.12    tptp_prover_opts max_new theory_const
    7.13 -  (Path.explode "$ISABELLE_HOME/contrib/SystemOnTPTP/remote", args ^ " -t " ^ string_of_int timeout)
    7.14 +  (Path.explode "$ISABELLE_HOME/lib/scripts/SystemOnTPTP", args ^ " -t " ^ string_of_int timeout)
    7.15    timeout;
    7.16  
    7.17  val remote_prover = remote_prover_opts 60 false;
     8.1 --- a/src/Pure/IsaMakefile	Sat Apr 25 21:42:05 2009 +0200
     8.2 +++ b/src/Pure/IsaMakefile	Sat Apr 25 22:29:13 2009 +0200
     8.3 @@ -40,9 +40,8 @@
     8.4  
     8.5  Pure: $(OUT)/Pure
     8.6  
     8.7 -$(OUT)/Pure: $(BOOTSTRAP_FILES) \
     8.8 -  Concurrent/ROOT.ML Concurrent/future.ML	\
     8.9 -  Concurrent/mailbox.ML Concurrent/par_list.ML				\
    8.10 +$(OUT)/Pure: $(BOOTSTRAP_FILES) Concurrent/ROOT.ML			\
    8.11 +  Concurrent/future.ML Concurrent/mailbox.ML Concurrent/par_list.ML	\
    8.12    Concurrent/par_list_dummy.ML Concurrent/simple_thread.ML		\
    8.13    Concurrent/synchronized.ML Concurrent/task_queue.ML General/ROOT.ML	\
    8.14    General/alist.ML General/antiquote.ML General/balanced_tree.ML	\
    8.15 @@ -87,7 +86,7 @@
    8.16    Thy/html.ML Thy/latex.ML Thy/present.ML Thy/term_style.ML		\
    8.17    Thy/thm_deps.ML Thy/thy_header.ML Thy/thy_info.ML Thy/thy_load.ML	\
    8.18    Thy/thy_output.ML Thy/thy_syntax.ML Tools/ROOT.ML			\
    8.19 -  Tools/auto_solve.ML Tools/find_consts.ML Tools/find_theorems.ML Tools/named_thms.ML	\
    8.20 +  Tools/find_consts.ML Tools/find_theorems.ML Tools/named_thms.ML	\
    8.21    Tools/xml_syntax.ML assumption.ML axclass.ML codegen.ML config.ML	\
    8.22    conjunction.ML consts.ML context.ML context_position.ML conv.ML	\
    8.23    defs.ML display.ML drule.ML envir.ML facts.ML goal.ML			\
     9.1 --- a/src/Pure/ProofGeneral/ROOT.ML	Sat Apr 25 21:42:05 2009 +0200
     9.2 +++ b/src/Pure/ProofGeneral/ROOT.ML	Sat Apr 25 22:29:13 2009 +0200
     9.3 @@ -14,11 +14,7 @@
     9.4  
     9.5  use "pgip_isabelle.ML";
     9.6  
     9.7 -(use
     9.8 -  |> setmp Proofterm.proofs 1
     9.9 -  |> setmp quick_and_dirty true
    9.10 -  |> setmp Quickcheck.auto true
    9.11 -  |> setmp auto_solve true) "preferences.ML";
    9.12 +use "preferences.ML";
    9.13  
    9.14  use "pgip_parser.ML";
    9.15  
    10.1 --- a/src/Pure/ProofGeneral/preferences.ML	Sat Apr 25 21:42:05 2009 +0200
    10.2 +++ b/src/Pure/ProofGeneral/preferences.ML	Sat Apr 25 22:29:13 2009 +0200
    10.3 @@ -6,6 +6,10 @@
    10.4  
    10.5  signature PREFERENCES =
    10.6  sig
    10.7 +  val category_display: string
    10.8 +  val category_advanced_display: string
    10.9 +  val category_tracing: string
   10.10 +  val category_proof: string
   10.11    type preference =
   10.12     {name: string,
   10.13      descr: string,
   10.14 @@ -29,6 +33,14 @@
   10.15  structure Preferences: PREFERENCES =
   10.16  struct
   10.17  
   10.18 +(* categories *)
   10.19 +
   10.20 +val category_display = "Display";
   10.21 +val category_advanced_display = "Advanced Display";
   10.22 +val category_tracing = "Tracing";
   10.23 +val category_proof = "Proof"
   10.24 +
   10.25 +
   10.26  (* preferences and preference tables *)
   10.27  
   10.28  type preference =
   10.29 @@ -66,11 +78,11 @@
   10.30  
   10.31  (* preferences of Pure *)
   10.32  
   10.33 -val proof_pref =
   10.34 +val proof_pref = setmp Proofterm.proofs 1 (fn () =>
   10.35    let
   10.36      fun get () = PgipTypes.bool_to_pgstring (! Proofterm.proofs >= 2);
   10.37      fun set s = Proofterm.proofs := (if PgipTypes.read_pgipbool s then 2 else 1);
   10.38 -  in mkpref get set PgipTypes.Pgipbool "full-proofs" "Record full proof objects internally" end;
   10.39 +  in mkpref get set PgipTypes.Pgipbool "full-proofs" "Record full proof objects internally" end) ();
   10.40  
   10.41  val thm_depsN = "thm_deps";
   10.42  val thm_deps_pref =
   10.43 @@ -145,24 +157,13 @@
   10.44    bool_pref Toplevel.debug
   10.45      "debugging"
   10.46      "Whether to enable debugging.",
   10.47 -  bool_pref Quickcheck.auto
   10.48 -    "auto-quickcheck"
   10.49 -    "Whether to enable quickcheck automatically.",
   10.50 -  nat_pref Quickcheck.auto_time_limit
   10.51 -    "auto-quickcheck-time-limit"
   10.52 -    "Time limit for automatic quickcheck (in milliseconds).",
   10.53 -  bool_pref AutoSolve.auto
   10.54 -    "auto-solve"
   10.55 -    "Try to solve newly declared lemmas with existing theorems.",
   10.56 -  nat_pref AutoSolve.auto_time_limit
   10.57 -    "auto-solve-time-limit"
   10.58 -    "Time limit for seeking automatic solutions (in milliseconds).",
   10.59    thm_deps_pref];
   10.60  
   10.61  val proof_preferences =
   10.62 - [bool_pref quick_and_dirty
   10.63 -    "quick-and-dirty"
   10.64 -    "Take a few short cuts",
   10.65 + [setmp quick_and_dirty true (fn () =>
   10.66 +    bool_pref quick_and_dirty
   10.67 +      "quick-and-dirty"
   10.68 +      "Take a few short cuts") (),
   10.69    bool_pref Toplevel.skip_proofs
   10.70      "skip-proofs"
   10.71      "Skip over proofs (interactive-only)",
   10.72 @@ -175,10 +176,10 @@
   10.73      "Check proofs in parallel"];
   10.74  
   10.75  val pure_preferences =
   10.76 - [("Display", display_preferences),
   10.77 -  ("Advanced Display", advanced_display_preferences),
   10.78 -  ("Tracing", tracing_preferences),
   10.79 -  ("Proof", proof_preferences)];
   10.80 + [(category_display, display_preferences),
   10.81 +  (category_advanced_display, advanced_display_preferences),
   10.82 +  (category_tracing, tracing_preferences),
   10.83 +  (category_proof, proof_preferences)];
   10.84  
   10.85  
   10.86  (* table of categories and preferences; names must be unique *)
    11.1 --- a/src/Pure/Tools/ROOT.ML	Sat Apr 25 21:42:05 2009 +0200
    11.2 +++ b/src/Pure/Tools/ROOT.ML	Sat Apr 25 22:29:13 2009 +0200
    11.3 @@ -1,23 +1,9 @@
    11.4 -(*  Title:      Pure/Tools/ROOT.ML
    11.5 -
    11.6 -Miscellaneous tools and packages for Pure Isabelle.
    11.7 -*)
    11.8 +(* Miscellaneous tools and packages for Pure Isabelle *)
    11.9  
   11.10  use "named_thms.ML";
   11.11  
   11.12 -(*basic XML support*)
   11.13  use "xml_syntax.ML";
   11.14  
   11.15  use "find_theorems.ML";
   11.16  use "find_consts.ML";
   11.17  
   11.18 -use "auto_solve.ML";
   11.19 -
   11.20 -(*quickcheck stub needed here because of pg preferences*)
   11.21 -structure Quickcheck =
   11.22 -struct
   11.23 -
   11.24 -val auto = ref false;
   11.25 -val auto_time_limit = ref 5000;
   11.26 -
   11.27 -end;
    12.1 --- a/src/Pure/Tools/auto_solve.ML	Sat Apr 25 21:42:05 2009 +0200
    12.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    12.3 @@ -1,87 +0,0 @@
    12.4 -(*  Title:      Tools/auto_solve.ML
    12.5 -    Author:     Timothy Bourke and Gerwin Klein, NICTA
    12.6 -
    12.7 -Check whether a newly stated theorem can be solved directly by an
    12.8 -existing theorem.  Duplicate lemmas can be detected in this way.
    12.9 -
   12.10 -The implementation is based in part on Berghofer and Haftmann's
   12.11 -quickcheck.ML.  It relies critically on the FindTheorems solves
   12.12 -feature.
   12.13 -*)
   12.14 -
   12.15 -signature AUTO_SOLVE =
   12.16 -sig
   12.17 -  val auto : bool ref
   12.18 -  val auto_time_limit : int ref
   12.19 -  val limit : int ref
   12.20 -
   12.21 -  val seek_solution : bool -> Proof.state -> Proof.state
   12.22 -end;
   12.23 -
   12.24 -structure AutoSolve : AUTO_SOLVE =
   12.25 -struct
   12.26 -
   12.27 -val auto = ref false;
   12.28 -val auto_time_limit = ref 2500;
   12.29 -val limit = ref 5;
   12.30 -
   12.31 -fun seek_solution int state =
   12.32 -  let
   12.33 -    val ctxt = Proof.context_of state;
   12.34 -
   12.35 -    val crits = [(true, FindTheorems.Solves)];
   12.36 -    fun find g = snd (FindTheorems.find_theorems ctxt (SOME g) (SOME (! limit)) false crits);
   12.37 -
   12.38 -    fun prt_result (goal, results) =
   12.39 -      let
   12.40 -        val msg =
   12.41 -          (case goal of
   12.42 -            NONE => "The current goal"
   12.43 -          | SOME sg => Syntax.string_of_term ctxt (Thm.term_of sg));
   12.44 -      in
   12.45 -        Pretty.big_list
   12.46 -          (msg ^ " could be solved directly with:")
   12.47 -          (map (FindTheorems.pretty_thm ctxt) results)
   12.48 -      end;
   12.49 -
   12.50 -    fun seek_against_goal () =
   12.51 -      (case try Proof.get_goal state of
   12.52 -        NONE => NONE
   12.53 -      | SOME (_, (_, goal)) =>
   12.54 -          let
   12.55 -            val subgoals = Conjunction.dest_conjunctions (Thm.cprem_of goal 1);
   12.56 -            val rs =
   12.57 -              if length subgoals = 1
   12.58 -              then [(NONE, find goal)]
   12.59 -              else map (fn sg => (SOME sg, find (Goal.init sg))) subgoals;
   12.60 -            val results = filter_out (null o snd) rs;
   12.61 -          in if null results then NONE else SOME results end);
   12.62 -
   12.63 -    fun go () =
   12.64 -      let
   12.65 -        val res =
   12.66 -          TimeLimit.timeLimit (Time.fromMilliseconds (! auto_time_limit))
   12.67 -            (try seek_against_goal) ();
   12.68 -      in
   12.69 -        (case res of
   12.70 -          SOME (SOME results) =>
   12.71 -            state |> Proof.goal_message
   12.72 -              (fn () => Pretty.chunks
   12.73 -                [Pretty.str "",
   12.74 -                  Pretty.markup Markup.hilite
   12.75 -                    (separate (Pretty.brk 0) (map prt_result results))])
   12.76 -        | _ => state)
   12.77 -      end handle TimeLimit.TimeOut => (warning "AutoSolve: timeout."; state);
   12.78 -  in
   12.79 -    if int andalso ! auto andalso not (! Toplevel.quiet)
   12.80 -    then go ()
   12.81 -    else state
   12.82 -  end;
   12.83 -
   12.84 -end;
   12.85 -
   12.86 -val _ = Context.>> (Specification.add_theorem_hook AutoSolve.seek_solution);
   12.87 -
   12.88 -val auto_solve = AutoSolve.auto;
   12.89 -val auto_solve_time_limit = AutoSolve.auto_time_limit;
   12.90 -
    13.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    13.2 +++ b/src/Tools/auto_solve.ML	Sat Apr 25 22:29:13 2009 +0200
    13.3 @@ -0,0 +1,101 @@
    13.4 +(*  Title:      Tools/auto_solve.ML
    13.5 +    Author:     Timothy Bourke and Gerwin Klein, NICTA
    13.6 +
    13.7 +Check whether a newly stated theorem can be solved directly by an
    13.8 +existing theorem.  Duplicate lemmas can be detected in this way.
    13.9 +
   13.10 +The implementation is based in part on Berghofer and Haftmann's
   13.11 +quickcheck.ML.  It relies critically on the FindTheorems solves
   13.12 +feature.
   13.13 +*)
   13.14 +
   13.15 +signature AUTO_SOLVE =
   13.16 +sig
   13.17 +  val auto : bool ref
   13.18 +  val auto_time_limit : int ref
   13.19 +  val limit : int ref
   13.20 +end;
   13.21 +
   13.22 +structure AutoSolve : AUTO_SOLVE =
   13.23 +struct
   13.24 +
   13.25 +(* preferences *)
   13.26 +
   13.27 +val auto = ref false;
   13.28 +val auto_time_limit = ref 2500;
   13.29 +val limit = ref 5;
   13.30 +
   13.31 +val _ =
   13.32 +  ProofGeneralPgip.add_preference Preferences.category_tracing
   13.33 +  (setmp auto true (fn () =>
   13.34 +    Preferences.bool_pref auto
   13.35 +      "auto-solve"
   13.36 +      "Try to solve newly declared lemmas with existing theorems.") ());
   13.37 +
   13.38 +val _ =
   13.39 +  ProofGeneralPgip.add_preference Preferences.category_tracing
   13.40 +    (Preferences.nat_pref auto_time_limit
   13.41 +      "auto-solve-time-limit"
   13.42 +      "Time limit for seeking automatic solutions (in milliseconds).");
   13.43 +
   13.44 +
   13.45 +(* hook *)
   13.46 +
   13.47 +val _ = Context.>> (Specification.add_theorem_hook (fn int => fn state =>
   13.48 +  let
   13.49 +    val ctxt = Proof.context_of state;
   13.50 +
   13.51 +    val crits = [(true, FindTheorems.Solves)];
   13.52 +    fun find g = snd (FindTheorems.find_theorems ctxt (SOME g) (SOME (! limit)) false crits);
   13.53 +
   13.54 +    fun prt_result (goal, results) =
   13.55 +      let
   13.56 +        val msg =
   13.57 +          (case goal of
   13.58 +            NONE => "The current goal"
   13.59 +          | SOME sg => Syntax.string_of_term ctxt (Thm.term_of sg));
   13.60 +      in
   13.61 +        Pretty.big_list
   13.62 +          (msg ^ " could be solved directly with:")
   13.63 +          (map (FindTheorems.pretty_thm ctxt) results)
   13.64 +      end;
   13.65 +
   13.66 +    fun seek_against_goal () =
   13.67 +      (case try Proof.get_goal state of
   13.68 +        NONE => NONE
   13.69 +      | SOME (_, (_, goal)) =>
   13.70 +          let
   13.71 +            val subgoals = Conjunction.dest_conjunctions (Thm.cprem_of goal 1);
   13.72 +            val rs =
   13.73 +              if length subgoals = 1
   13.74 +              then [(NONE, find goal)]
   13.75 +              else map (fn sg => (SOME sg, find (Goal.init sg))) subgoals;
   13.76 +            val results = filter_out (null o snd) rs;
   13.77 +          in if null results then NONE else SOME results end);
   13.78 +
   13.79 +    fun go () =
   13.80 +      let
   13.81 +        val res =
   13.82 +          TimeLimit.timeLimit (Time.fromMilliseconds (! auto_time_limit))
   13.83 +            (try seek_against_goal) ();
   13.84 +      in
   13.85 +        (case res of
   13.86 +          SOME (SOME results) =>
   13.87 +            state |> Proof.goal_message
   13.88 +              (fn () => Pretty.chunks
   13.89 +                [Pretty.str "",
   13.90 +                  Pretty.markup Markup.hilite
   13.91 +                    (separate (Pretty.brk 0) (map prt_result results))])
   13.92 +        | _ => state)
   13.93 +      end handle TimeLimit.TimeOut => (warning "AutoSolve: timeout."; state);
   13.94 +  in
   13.95 +    if int andalso ! auto andalso not (! Toplevel.quiet)
   13.96 +    then go ()
   13.97 +    else state
   13.98 +  end));
   13.99 +
  13.100 +end;
  13.101 +
  13.102 +val auto_solve = AutoSolve.auto;
  13.103 +val auto_solve_time_limit = AutoSolve.auto_time_limit;
  13.104 +
    14.1 --- a/src/Tools/quickcheck.ML	Sat Apr 25 21:42:05 2009 +0200
    14.2 +++ b/src/Tools/quickcheck.ML	Sat Apr 25 22:29:13 2009 +0200
    14.3 @@ -6,16 +6,34 @@
    14.4  
    14.5  signature QUICKCHECK =
    14.6  sig
    14.7 -  val test_term: Proof.context -> bool -> string option -> int -> int -> term -> (string * term) list option;
    14.8 -  val add_generator: string * (Proof.context -> term -> int -> term list option) -> theory -> theory
    14.9    val auto: bool ref
   14.10    val auto_time_limit: int ref
   14.11 +  val test_term: Proof.context -> bool -> string option -> int -> int -> term ->
   14.12 +    (string * term) list option
   14.13 +  val add_generator: string * (Proof.context -> term -> int -> term list option) -> theory -> theory
   14.14  end;
   14.15  
   14.16  structure Quickcheck : QUICKCHECK =
   14.17  struct
   14.18  
   14.19 -open Quickcheck; (*c.f. Pure/Tools/ROOT.ML*)
   14.20 +(* preferences *)
   14.21 +
   14.22 +val auto = ref false;
   14.23 +val auto_time_limit = ref 2500;
   14.24 +
   14.25 +val _ =
   14.26 +  ProofGeneralPgip.add_preference Preferences.category_tracing
   14.27 +  (setmp auto true (fn () =>
   14.28 +    Preferences.bool_pref auto
   14.29 +      "auto-quickcheck"
   14.30 +      "Whether to enable quickcheck automatically.") ());
   14.31 +
   14.32 +val _ =
   14.33 +  ProofGeneralPgip.add_preference Preferences.category_tracing
   14.34 +    (Preferences.nat_pref auto_time_limit
   14.35 +      "auto-quickcheck-time-limit"
   14.36 +      "Time limit for automatic quickcheck (in milliseconds).");
   14.37 +
   14.38  
   14.39  (* quickcheck configuration -- default parameters, test generators *)
   14.40  
   14.41 @@ -140,7 +158,7 @@
   14.42  
   14.43  (* automatic testing *)
   14.44  
   14.45 -fun test_goal_auto int state =
   14.46 +val _ = Context.>> (Specification.add_theorem_hook (fn int => fn state =>
   14.47    let
   14.48      val ctxt = Proof.context_of state;
   14.49      val assms = map term_of (Assumption.all_assms_of ctxt);
   14.50 @@ -161,12 +179,10 @@
   14.51      if int andalso !auto andalso not (!Toplevel.quiet)
   14.52      then test ()
   14.53      else state
   14.54 -  end;
   14.55 -
   14.56 -val _ = Context.>> (Specification.add_theorem_hook test_goal_auto);
   14.57 +  end));
   14.58  
   14.59  
   14.60 -(* Isar interfaces *)
   14.61 +(* Isar commands *)
   14.62  
   14.63  fun read_nat s = case (Library.read_int o Symbol.explode) s
   14.64   of (k, []) => if k >= 0 then k