1.1 --- a/src/Pure/IsaMakefile Wed Feb 11 14:48:14 2009 +1100
1.2 +++ b/src/Pure/IsaMakefile Wed Feb 11 16:03:10 2009 +1100
1.3 @@ -85,7 +85,7 @@
1.4 pure_setup.ML pure_thy.ML search.ML sign.ML simplifier.ML sorts.ML \
1.5 subgoal.ML tactic.ML tctical.ML term.ML term_ord.ML term_subst.ML \
1.6 theory.ML thm.ML type.ML type_infer.ML unify.ML variable.ML \
1.7 - ../Tools/quickcheck.ML
1.8 + ../Tools/quickcheck.ML ../Tools/auto_solve.ML
1.9 @./mk
1.10
1.11
2.1 --- a/src/Pure/Isar/find_theorems.ML Wed Feb 11 14:48:14 2009 +1100
2.2 +++ b/src/Pure/Isar/find_theorems.ML Wed Feb 11 16:03:10 2009 +1100
2.3 @@ -370,10 +370,6 @@
2.4 val lim = the_default (! limit) opt_limit;
2.5 val thms = Library.drop (len - lim, matches);
2.6
2.7 - fun prt_fact (thmref, thm) = Pretty.block
2.8 - [Pretty.str (Facts.string_of_ref thmref), Pretty.str ":", Pretty.brk 1,
2.9 - ProofContext.pretty_thm ctxt thm];
2.10 -
2.11 val end_msg = " in " ^
2.12 (List.nth (String.tokens Char.isSpace (end_timing start), 3))
2.13 ^ " secs"
2.14 @@ -386,7 +382,7 @@
2.15 (if len <= lim then ""
2.16 else " (" ^ string_of_int lim ^ " displayed)")
2.17 ^ end_msg ^ ":"), Pretty.str ""] @
2.18 - map prt_fact thms)
2.19 + map Display.pretty_fact thms)
2.20 |> Pretty.chunks |> Pretty.writeln
2.21 end
2.22
3.1 --- a/src/Pure/ProofGeneral/ROOT.ML Wed Feb 11 14:48:14 2009 +1100
3.2 +++ b/src/Pure/ProofGeneral/ROOT.ML Wed Feb 11 16:03:10 2009 +1100
3.3 @@ -17,7 +17,8 @@
3.4 (use
3.5 |> setmp Proofterm.proofs 1
3.6 |> setmp quick_and_dirty true
3.7 - |> setmp auto_quickcheck true) "preferences.ML";
3.8 + |> setmp auto_quickcheck true
3.9 + |> setmp auto_solve false) "preferences.ML";
3.10
3.11 use "pgip_parser.ML";
3.12
4.1 --- a/src/Pure/ProofGeneral/preferences.ML Wed Feb 11 14:48:14 2009 +1100
4.2 +++ b/src/Pure/ProofGeneral/preferences.ML Wed Feb 11 16:03:10 2009 +1100
4.3 @@ -151,6 +151,12 @@
4.4 nat_pref Quickcheck.auto_time_limit
4.5 "auto-quickcheck-time-limit"
4.6 "Time limit for automatic quickcheck (in milliseconds).",
4.7 + bool_pref AutoSolve.auto
4.8 + "auto-solve"
4.9 + "Try to solve newly declared lemmas with existing theorems.",
4.10 + nat_pref AutoSolve.auto_time_limit
4.11 + "auto-solve-time-limit"
4.12 + "Time limit for seeking automatic solutions (in milliseconds).",
4.13 thm_deps_pref];
4.14
4.15 val proof_preferences =
5.1 --- a/src/Pure/Tools/ROOT.ML Wed Feb 11 14:48:14 2009 +1100
5.2 +++ b/src/Pure/Tools/ROOT.ML Wed Feb 11 16:03:10 2009 +1100
5.3 @@ -9,5 +9,6 @@
5.4 (*basic XML support*)
5.5 use "xml_syntax.ML";
5.6
5.7 -(*quickcheck needed here because of pg preferences*)
5.8 -use "../../Tools/quickcheck.ML"
5.9 +(*quickcheck/autosolve needed here because of pg preferences*)
5.10 +use "../../Tools/quickcheck.ML";
5.11 +use "../../Tools/auto_solve.ML";
6.1 --- a/src/Pure/display.ML Wed Feb 11 14:48:14 2009 +1100
6.2 +++ b/src/Pure/display.ML Wed Feb 11 16:03:10 2009 +1100
6.3 @@ -20,6 +20,7 @@
6.4 val pretty_thm_aux: Pretty.pp -> bool -> bool -> term list -> thm -> Pretty.T
6.5 val pretty_thm: thm -> Pretty.T
6.6 val string_of_thm: thm -> string
6.7 + val pretty_fact: Facts.ref * thm -> Pretty.T
6.8 val pretty_thms: thm list -> Pretty.T
6.9 val pretty_thm_sg: theory -> thm -> Pretty.T
6.10 val pretty_thms_sg: theory -> thm list -> Pretty.T
6.11 @@ -92,6 +93,10 @@
6.12
6.13 val string_of_thm = Pretty.string_of o pretty_thm;
6.14
6.15 +fun pretty_fact (thmref, thm) = Pretty.block
6.16 + [Pretty.str (Facts.string_of_ref thmref), Pretty.str ":", Pretty.brk 1,
6.17 + pretty_thm thm];
6.18 +
6.19 fun pretty_thms [th] = pretty_thm th
6.20 | pretty_thms ths = Pretty.block (Pretty.fbreaks (map pretty_thm ths));
6.21
7.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
7.2 +++ b/src/Tools/auto_solve.ML Wed Feb 11 16:03:10 2009 +1100
7.3 @@ -0,0 +1,93 @@
7.4 +(* Title: auto_solve.ML
7.5 + Author: Timothy Bourke and Gerwin Klein, NICTA
7.6 +
7.7 + Check whether a newly stated theorem can be solved directly
7.8 + by an existing theorem. Duplicate lemmas can be detected in
7.9 + this way.
7.10 +
7.11 + The implemenation is based in part on Berghofer and
7.12 + Haftmann's Pure/codegen.ML. It relies critically on
7.13 + the FindTheorems solves feature.
7.14 +*)
7.15 +
7.16 +signature AUTO_SOLVE =
7.17 +sig
7.18 + val auto : bool ref;
7.19 + val auto_time_limit : int ref;
7.20 +
7.21 + val seek_solution : bool -> Proof.state -> Proof.state;
7.22 +end;
7.23 +
7.24 +structure AutoSolve : AUTO_SOLVE =
7.25 +struct
7.26 + structure FT = FindTheorems;
7.27 +
7.28 + val auto = ref false;
7.29 + val auto_time_limit = ref 5000;
7.30 +
7.31 + fun seek_solution int state = let
7.32 + val ctxt = Proof.context_of state;
7.33 +
7.34 + fun conj_to_list [] = []
7.35 + | conj_to_list (t::ts) =
7.36 + (Conjunction.dest_conjunction t
7.37 + |> (fn (t1, t2) => conj_to_list (t1::t2::ts)))
7.38 + handle TERM _ => t::conj_to_list ts;
7.39 +
7.40 + val crits = [(true, FT.Solves)];
7.41 + fun find g = (NONE, FT.find_theorems ctxt g true crits);
7.42 + fun find_cterm g = (SOME g, FT.find_theorems ctxt
7.43 + (SOME (Goal.init g)) true crits);
7.44 +
7.45 + fun prt_result (goal, results) = let
7.46 + val msg = case goal of
7.47 + NONE => "The current goal"
7.48 + | SOME g => Syntax.string_of_term ctxt (term_of g);
7.49 + in
7.50 + Pretty.big_list (msg ^ " could be solved directly with:")
7.51 + (map Display.pretty_fact results)
7.52 + end;
7.53 +
7.54 + fun seek_against_goal () = let
7.55 + val goal = try Proof.get_goal state
7.56 + |> Option.map (#2 o #2);
7.57 +
7.58 + val goals = goal
7.59 + |> Option.map (fn g => cprem_of g 1)
7.60 + |> the_list
7.61 + |> conj_to_list;
7.62 +
7.63 + val rs = if length goals = 1
7.64 + then [find goal]
7.65 + else map find_cterm goals;
7.66 + val frs = filter_out (null o snd) rs;
7.67 +
7.68 + in if null frs then NONE else SOME frs end;
7.69 +
7.70 + fun go () = let
7.71 + val res = TimeLimit.timeLimit
7.72 + (Time.fromMilliseconds (!auto_time_limit))
7.73 + (try seek_against_goal) ();
7.74 + in
7.75 + case Option.join res of
7.76 + NONE => state
7.77 + | SOME results => (Proof.goal_message
7.78 + (fn () => Pretty.chunks [Pretty.str "",
7.79 + Pretty.markup Markup.hilite
7.80 + (Library.separate (Pretty.brk 0)
7.81 + (map prt_result results))])
7.82 + state)
7.83 + end handle TimeLimit.TimeOut => (warning "AutoSolve: timeout."; state);
7.84 + in
7.85 + if int andalso !auto andalso not (!Toplevel.quiet)
7.86 + then go ()
7.87 + else state
7.88 + end;
7.89 +
7.90 +end;
7.91 +
7.92 +val _ = Context.>> (Specification.add_theorem_hook AutoSolve.seek_solution);
7.93 +
7.94 +val auto_solve = AutoSolve.auto;
7.95 +val auto_solve_time_limit = AutoSolve.auto_time_limit;
7.96 +