--- a/NEWS Mon Oct 25 09:29:43 2010 +0200
+++ b/NEWS Mon Oct 25 10:30:46 2010 +0200
@@ -276,6 +276,9 @@
meson_disj_FalseD2 ~> Meson.disj_FalseD2
INCOMPATIBILITY.
+* Auto Solve: Renamed "Auto Solve Direct". The tool is now available manually as
+ "solve_direct".
+
* Sledgehammer:
- Renamed lemmas:
COMBI_def ~> Meson.COMBI_def
--- a/src/HOL/IsaMakefile Mon Oct 25 09:29:43 2010 +0200
+++ b/src/HOL/IsaMakefile Mon Oct 25 10:30:46 2010 +0200
@@ -122,7 +122,6 @@
$(SRC)/Tools/IsaPlanner/rw_tools.ML \
$(SRC)/Tools/IsaPlanner/zipper.ML \
$(SRC)/Tools/atomize_elim.ML \
- $(SRC)/Tools/auto_solve.ML \
$(SRC)/Tools/auto_tools.ML \
$(SRC)/Tools/coherent.ML \
$(SRC)/Tools/cong_tac.ML \
@@ -134,6 +133,7 @@
$(SRC)/Tools/nbe.ML \
$(SRC)/Tools/project_rule.ML \
$(SRC)/Tools/quickcheck.ML \
+ $(SRC)/Tools/solve_direct.ML \
$(SRC)/Tools/value.ML \
HOL.thy \
Tools/hologic.ML \
--- a/src/Tools/Code_Generator.thy Mon Oct 25 09:29:43 2010 +0200
+++ b/src/Tools/Code_Generator.thy Mon Oct 25 10:30:46 2010 +0200
@@ -9,7 +9,7 @@
uses
"~~/src/Tools/cache_io.ML"
"~~/src/Tools/auto_tools.ML"
- "~~/src/Tools/auto_solve.ML"
+ "~~/src/Tools/solve_direct.ML"
"~~/src/Tools/quickcheck.ML"
"~~/src/Tools/value.ML"
"~~/src/Tools/Code/code_preproc.ML"
@@ -26,7 +26,7 @@
begin
setup {*
- Auto_Solve.setup
+ Solve_Direct.setup
#> Code_Preproc.setup
#> Code_Simp.setup
#> Code_ML.setup
--- a/src/Tools/auto_solve.ML Mon Oct 25 09:29:43 2010 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,80 +0,0 @@
-(* Title: Tools/auto_solve.ML
- Author: Timothy Bourke and Gerwin Klein, NICTA
-
-Check whether a newly stated theorem can be solved directly by an
-existing theorem. Duplicate lemmas can be detected in this way.
-
-The implementation relies critically on the Find_Theorems solves
-feature.
-*)
-
-signature AUTO_SOLVE =
-sig
- val auto : bool Unsynchronized.ref
- val max_solutions : int Unsynchronized.ref
- val setup : theory -> theory
-end;
-
-structure Auto_Solve : AUTO_SOLVE =
-struct
-
-(* preferences *)
-
-val auto = Unsynchronized.ref false;
-val max_solutions = Unsynchronized.ref 5;
-
-val _ =
- ProofGeneralPgip.add_preference Preferences.category_tracing
- (Unsynchronized.setmp auto true (fn () =>
- Preferences.bool_pref auto
- "auto-solve" "Try to solve conjectures with existing theorems.") ());
-
-
-(* hook *)
-
-fun auto_solve state =
- let
- val ctxt = Proof.context_of state;
-
- val crits = [(true, Find_Theorems.Solves)];
- fun find g = snd (Find_Theorems.find_theorems ctxt (SOME g) (SOME (! max_solutions)) false crits);
-
- fun prt_result (goal, results) =
- let
- val msg =
- (case goal of
- NONE => "The current goal"
- | SOME sg => Syntax.string_of_term ctxt (Thm.term_of sg));
- in
- Pretty.big_list
- (msg ^ " could be solved directly with:")
- (map (Find_Theorems.pretty_thm ctxt) results)
- end;
-
- fun seek_against_goal () =
- (case try Proof.simple_goal state of
- NONE => NONE
- | SOME {goal = st, ...} =>
- let
- val subgoals = Drule.strip_imp_prems (Thm.cprop_of st);
- val rs =
- if length subgoals = 1
- then [(NONE, find st)]
- else map (fn sg => (SOME sg, find (Goal.init sg))) subgoals;
- val results = filter_out (null o snd) rs;
- in if null results then NONE else SOME results end);
-
- fun go () =
- (case try seek_against_goal () of
- SOME (SOME results) =>
- (true, state |> Proof.goal_message
- (fn () => Pretty.chunks
- [Pretty.str "",
- Pretty.markup Markup.hilite
- (separate (Pretty.brk 0) (map prt_result results))]))
- | _ => (false, state));
- in if not (!auto) then (false, state) else go () end;
-
-val setup = Auto_Tools.register_tool ("solve", auto_solve)
-
-end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/solve_direct.ML Mon Oct 25 10:30:46 2010 +0200
@@ -0,0 +1,97 @@
+(* Title: Tools/solve_direct.ML
+ Author: Timothy Bourke and Gerwin Klein, NICTA
+
+Check whether a newly stated theorem can be solved directly by an
+existing theorem. Duplicate lemmas can be detected in this way.
+
+The implementation relies critically on the Find_Theorems solves
+feature.
+*)
+
+signature SOLVE_DIRECT =
+sig
+ val auto : bool Unsynchronized.ref
+ val max_solutions : int Unsynchronized.ref
+ val setup : theory -> theory
+end;
+
+structure Solve_Direct : SOLVE_DIRECT =
+struct
+
+val solve_directN = "solve_direct"
+
+(* preferences *)
+
+val auto = Unsynchronized.ref false;
+val max_solutions = Unsynchronized.ref 5;
+
+val _ =
+ ProofGeneralPgip.add_preference Preferences.category_tracing
+ (Unsynchronized.setmp auto true (fn () =>
+ Preferences.bool_pref auto
+ ("Auto " ^ solve_directN)
+ ("Run " ^ quote solve_directN ^ " automatically.")) ());
+
+fun solve_direct auto state =
+ let
+ val ctxt = Proof.context_of state;
+
+ val crits = [(true, Find_Theorems.Solves)];
+ fun find g = snd (Find_Theorems.find_theorems ctxt (SOME g) (SOME (! max_solutions)) false crits);
+
+ fun prt_result (goal, results) =
+ let
+ val msg =
+ (if auto then "Auto " else "") ^ solve_directN ^ ": " ^
+ (case goal of
+ NONE => "The current goal"
+ | SOME sg => Syntax.string_of_term ctxt (Thm.term_of sg));
+ in
+ Pretty.big_list
+ (msg ^ " can be solved directly with")
+ (map (Find_Theorems.pretty_thm ctxt) results)
+ end;
+
+ fun seek_against_goal () =
+ (case try Proof.simple_goal state of
+ NONE => NONE
+ | SOME {goal = st, ...} =>
+ let
+ val subgoals = Drule.strip_imp_prems (Thm.cprop_of st);
+ val rs =
+ if length subgoals = 1
+ then [(NONE, find st)]
+ else map (fn sg => (SOME sg, find (Goal.init sg))) subgoals;
+ val results = filter_out (null o snd) rs;
+ in if null results then NONE else SOME results end);
+ fun message results = separate (Pretty.brk 0) (map prt_result results)
+ in
+ (case try seek_against_goal () of
+ SOME (SOME results) =>
+ (true, state |> (if auto then
+ Proof.goal_message
+ (fn () => Pretty.chunks
+ [Pretty.str "",
+ Pretty.markup Markup.hilite (message results)])
+ else
+ tap (fn _ => priority (Pretty.string_of
+ (Pretty.chunks (message results))))))
+ | _ => (false, state))
+ end;
+
+val invoke_solve_direct = fst o solve_direct false
+
+val _ =
+ Outer_Syntax.improper_command solve_directN
+ "try to solve conjectures directly with existing theorems" Keyword.diag
+ (Scan.succeed (Toplevel.keep (K () o invoke_solve_direct
+ o Toplevel.proof_of)))
+
+(* hook *)
+
+fun auto_solve_direct state =
+ if not (!auto) then (false, state) else solve_direct true state
+
+val setup = Auto_Tools.register_tool (solve_directN, auto_solve_direct)
+
+end;