# HG changeset patch # User kleing # Date 1234328590 -39600 # Node ID c8cee17d7e50380d43c0a60e80cdb5496c63eeaf # Parent 2cc976ed8a3c269535d321b5d5c28a5adf239fae Autosolve feature for detecting duplicate theorems; patch by Timothy Bourke diff -r 2cc976ed8a3c -r c8cee17d7e50 src/Pure/IsaMakefile --- a/src/Pure/IsaMakefile Wed Feb 11 14:48:14 2009 +1100 +++ b/src/Pure/IsaMakefile Wed Feb 11 16:03:10 2009 +1100 @@ -85,7 +85,7 @@ pure_setup.ML pure_thy.ML search.ML sign.ML simplifier.ML sorts.ML \ subgoal.ML tactic.ML tctical.ML term.ML term_ord.ML term_subst.ML \ theory.ML thm.ML type.ML type_infer.ML unify.ML variable.ML \ - ../Tools/quickcheck.ML + ../Tools/quickcheck.ML ../Tools/auto_solve.ML @./mk diff -r 2cc976ed8a3c -r c8cee17d7e50 src/Pure/Isar/find_theorems.ML --- a/src/Pure/Isar/find_theorems.ML Wed Feb 11 14:48:14 2009 +1100 +++ b/src/Pure/Isar/find_theorems.ML Wed Feb 11 16:03:10 2009 +1100 @@ -370,10 +370,6 @@ val lim = the_default (! limit) opt_limit; val thms = Library.drop (len - lim, matches); - fun prt_fact (thmref, thm) = Pretty.block - [Pretty.str (Facts.string_of_ref thmref), Pretty.str ":", Pretty.brk 1, - ProofContext.pretty_thm ctxt thm]; - val end_msg = " in " ^ (List.nth (String.tokens Char.isSpace (end_timing start), 3)) ^ " secs" @@ -386,7 +382,7 @@ (if len <= lim then "" else " (" ^ string_of_int lim ^ " displayed)") ^ end_msg ^ ":"), Pretty.str ""] @ - map prt_fact thms) + map Display.pretty_fact thms) |> Pretty.chunks |> Pretty.writeln end diff -r 2cc976ed8a3c -r c8cee17d7e50 src/Pure/ProofGeneral/ROOT.ML --- a/src/Pure/ProofGeneral/ROOT.ML Wed Feb 11 14:48:14 2009 +1100 +++ b/src/Pure/ProofGeneral/ROOT.ML Wed Feb 11 16:03:10 2009 +1100 @@ -17,7 +17,8 @@ (use |> setmp Proofterm.proofs 1 |> setmp quick_and_dirty true - |> setmp auto_quickcheck true) "preferences.ML"; + |> setmp auto_quickcheck true + |> setmp auto_solve false) "preferences.ML"; use "pgip_parser.ML"; diff -r 2cc976ed8a3c -r c8cee17d7e50 src/Pure/ProofGeneral/preferences.ML --- a/src/Pure/ProofGeneral/preferences.ML Wed Feb 11 14:48:14 2009 +1100 +++ b/src/Pure/ProofGeneral/preferences.ML Wed Feb 11 16:03:10 2009 +1100 @@ -151,6 +151,12 @@ nat_pref Quickcheck.auto_time_limit "auto-quickcheck-time-limit" "Time limit for automatic quickcheck (in milliseconds).", + bool_pref AutoSolve.auto + "auto-solve" + "Try to solve newly declared lemmas with existing theorems.", + nat_pref AutoSolve.auto_time_limit + "auto-solve-time-limit" + "Time limit for seeking automatic solutions (in milliseconds).", thm_deps_pref]; val proof_preferences = diff -r 2cc976ed8a3c -r c8cee17d7e50 src/Pure/Tools/ROOT.ML --- a/src/Pure/Tools/ROOT.ML Wed Feb 11 14:48:14 2009 +1100 +++ b/src/Pure/Tools/ROOT.ML Wed Feb 11 16:03:10 2009 +1100 @@ -9,5 +9,6 @@ (*basic XML support*) use "xml_syntax.ML"; -(*quickcheck needed here because of pg preferences*) -use "../../Tools/quickcheck.ML" +(*quickcheck/autosolve needed here because of pg preferences*) +use "../../Tools/quickcheck.ML"; +use "../../Tools/auto_solve.ML"; diff -r 2cc976ed8a3c -r c8cee17d7e50 src/Pure/display.ML --- a/src/Pure/display.ML Wed Feb 11 14:48:14 2009 +1100 +++ b/src/Pure/display.ML Wed Feb 11 16:03:10 2009 +1100 @@ -20,6 +20,7 @@ val pretty_thm_aux: Pretty.pp -> bool -> bool -> term list -> thm -> Pretty.T val pretty_thm: thm -> Pretty.T val string_of_thm: thm -> string + val pretty_fact: Facts.ref * thm -> Pretty.T val pretty_thms: thm list -> Pretty.T val pretty_thm_sg: theory -> thm -> Pretty.T val pretty_thms_sg: theory -> thm list -> Pretty.T @@ -92,6 +93,10 @@ val string_of_thm = Pretty.string_of o pretty_thm; +fun pretty_fact (thmref, thm) = Pretty.block + [Pretty.str (Facts.string_of_ref thmref), Pretty.str ":", Pretty.brk 1, + pretty_thm thm]; + fun pretty_thms [th] = pretty_thm th | pretty_thms ths = Pretty.block (Pretty.fbreaks (map pretty_thm ths)); diff -r 2cc976ed8a3c -r c8cee17d7e50 src/Tools/auto_solve.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/auto_solve.ML Wed Feb 11 16:03:10 2009 +1100 @@ -0,0 +1,93 @@ +(* Title: 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 implemenation is based in part on Berghofer and + Haftmann's Pure/codegen.ML. It relies critically on + the FindTheorems solves feature. +*) + +signature AUTO_SOLVE = +sig + val auto : bool ref; + val auto_time_limit : int ref; + + val seek_solution : bool -> Proof.state -> Proof.state; +end; + +structure AutoSolve : AUTO_SOLVE = +struct + structure FT = FindTheorems; + + val auto = ref false; + val auto_time_limit = ref 5000; + + fun seek_solution int state = let + val ctxt = Proof.context_of state; + + fun conj_to_list [] = [] + | conj_to_list (t::ts) = + (Conjunction.dest_conjunction t + |> (fn (t1, t2) => conj_to_list (t1::t2::ts))) + handle TERM _ => t::conj_to_list ts; + + val crits = [(true, FT.Solves)]; + fun find g = (NONE, FT.find_theorems ctxt g true crits); + fun find_cterm g = (SOME g, FT.find_theorems ctxt + (SOME (Goal.init g)) true crits); + + fun prt_result (goal, results) = let + val msg = case goal of + NONE => "The current goal" + | SOME g => Syntax.string_of_term ctxt (term_of g); + in + Pretty.big_list (msg ^ " could be solved directly with:") + (map Display.pretty_fact results) + end; + + fun seek_against_goal () = let + val goal = try Proof.get_goal state + |> Option.map (#2 o #2); + + val goals = goal + |> Option.map (fn g => cprem_of g 1) + |> the_list + |> conj_to_list; + + val rs = if length goals = 1 + then [find goal] + else map find_cterm goals; + val frs = filter_out (null o snd) rs; + + in if null frs then NONE else SOME frs end; + + fun go () = let + val res = TimeLimit.timeLimit + (Time.fromMilliseconds (!auto_time_limit)) + (try seek_against_goal) (); + in + case Option.join res of + NONE => state + | SOME results => (Proof.goal_message + (fn () => Pretty.chunks [Pretty.str "", + Pretty.markup Markup.hilite + (Library.separate (Pretty.brk 0) + (map prt_result results))]) + state) + end handle TimeLimit.TimeOut => (warning "AutoSolve: timeout."; state); + in + if int andalso !auto andalso not (!Toplevel.quiet) + then go () + else state + end; + +end; + +val _ = Context.>> (Specification.add_theorem_hook AutoSolve.seek_solution); + +val auto_solve = AutoSolve.auto; +val auto_solve_time_limit = AutoSolve.auto_time_limit; +