# HG changeset patch # User blanchet # Date 1287995446 -7200 # Node ID 9ed3711366c8ff6aaf1366bcafd26421c4f052f8 # Parent e5ed638e49b00e7a03b4d4b8d44670ee0660c394 introduced manual version of "Auto Solve" as "solve_direct" diff -r e5ed638e49b0 -r 9ed3711366c8 NEWS --- 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 diff -r e5ed638e49b0 -r 9ed3711366c8 src/HOL/IsaMakefile --- 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 \ diff -r e5ed638e49b0 -r 9ed3711366c8 src/Tools/Code_Generator.thy --- 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 diff -r e5ed638e49b0 -r 9ed3711366c8 src/Tools/auto_solve.ML --- 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; diff -r e5ed638e49b0 -r 9ed3711366c8 src/Tools/solve_direct.ML --- /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;