Autosolve feature for detecting duplicate theorems; patch by Timothy Bourke
authorkleing
Wed Feb 11 16:03:10 2009 +1100 (2009-02-11)
changeset 29858c8cee17d7e50
parent 29857 2cc976ed8a3c
child 29860 f735e4027656
Autosolve feature for detecting duplicate theorems; patch by Timothy Bourke
src/Pure/IsaMakefile
src/Pure/Isar/find_theorems.ML
src/Pure/ProofGeneral/ROOT.ML
src/Pure/ProofGeneral/preferences.ML
src/Pure/Tools/ROOT.ML
src/Pure/display.ML
src/Tools/auto_solve.ML
     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 +