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 + end));
14.56
14.57 -val _ = Context.>> (Specification.add_theorem_hook test_goal_auto);
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