src/Tools/auto_solve.ML
author kleing
Wed, 11 Feb 2009 16:03:10 +1100
changeset 29858 c8cee17d7e50
child 29984 015c56cc1864
child 30240 5b25fee0362c
permissions -rw-r--r--
Autosolve feature for detecting duplicate theorems; patch by Timothy Bourke
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
29858
c8cee17d7e50 Autosolve feature for detecting duplicate theorems; patch by Timothy Bourke
kleing
parents:
diff changeset
     1
(*  Title:      auto_solve.ML
c8cee17d7e50 Autosolve feature for detecting duplicate theorems; patch by Timothy Bourke
kleing
parents:
diff changeset
     2
    Author:     Timothy Bourke and Gerwin Klein, NICTA
c8cee17d7e50 Autosolve feature for detecting duplicate theorems; patch by Timothy Bourke
kleing
parents:
diff changeset
     3
c8cee17d7e50 Autosolve feature for detecting duplicate theorems; patch by Timothy Bourke
kleing
parents:
diff changeset
     4
    Check whether a newly stated theorem can be solved directly
c8cee17d7e50 Autosolve feature for detecting duplicate theorems; patch by Timothy Bourke
kleing
parents:
diff changeset
     5
    by an existing theorem. Duplicate lemmas can be detected in
c8cee17d7e50 Autosolve feature for detecting duplicate theorems; patch by Timothy Bourke
kleing
parents:
diff changeset
     6
    this way.
c8cee17d7e50 Autosolve feature for detecting duplicate theorems; patch by Timothy Bourke
kleing
parents:
diff changeset
     7
c8cee17d7e50 Autosolve feature for detecting duplicate theorems; patch by Timothy Bourke
kleing
parents:
diff changeset
     8
    The implemenation is based in part on Berghofer and
c8cee17d7e50 Autosolve feature for detecting duplicate theorems; patch by Timothy Bourke
kleing
parents:
diff changeset
     9
    Haftmann's Pure/codegen.ML. It relies critically on
c8cee17d7e50 Autosolve feature for detecting duplicate theorems; patch by Timothy Bourke
kleing
parents:
diff changeset
    10
    the FindTheorems solves feature.
c8cee17d7e50 Autosolve feature for detecting duplicate theorems; patch by Timothy Bourke
kleing
parents:
diff changeset
    11
*)
c8cee17d7e50 Autosolve feature for detecting duplicate theorems; patch by Timothy Bourke
kleing
parents:
diff changeset
    12
c8cee17d7e50 Autosolve feature for detecting duplicate theorems; patch by Timothy Bourke
kleing
parents:
diff changeset
    13
signature AUTO_SOLVE =
c8cee17d7e50 Autosolve feature for detecting duplicate theorems; patch by Timothy Bourke
kleing
parents:
diff changeset
    14
sig
c8cee17d7e50 Autosolve feature for detecting duplicate theorems; patch by Timothy Bourke
kleing
parents:
diff changeset
    15
  val auto : bool ref;
c8cee17d7e50 Autosolve feature for detecting duplicate theorems; patch by Timothy Bourke
kleing
parents:
diff changeset
    16
  val auto_time_limit : int ref;
c8cee17d7e50 Autosolve feature for detecting duplicate theorems; patch by Timothy Bourke
kleing
parents:
diff changeset
    17
c8cee17d7e50 Autosolve feature for detecting duplicate theorems; patch by Timothy Bourke
kleing
parents:
diff changeset
    18
  val seek_solution : bool -> Proof.state -> Proof.state;
c8cee17d7e50 Autosolve feature for detecting duplicate theorems; patch by Timothy Bourke
kleing
parents:
diff changeset
    19
end;
c8cee17d7e50 Autosolve feature for detecting duplicate theorems; patch by Timothy Bourke
kleing
parents:
diff changeset
    20
c8cee17d7e50 Autosolve feature for detecting duplicate theorems; patch by Timothy Bourke
kleing
parents:
diff changeset
    21
structure AutoSolve : AUTO_SOLVE =
c8cee17d7e50 Autosolve feature for detecting duplicate theorems; patch by Timothy Bourke
kleing
parents:
diff changeset
    22
struct
c8cee17d7e50 Autosolve feature for detecting duplicate theorems; patch by Timothy Bourke
kleing
parents:
diff changeset
    23
  structure FT = FindTheorems;
c8cee17d7e50 Autosolve feature for detecting duplicate theorems; patch by Timothy Bourke
kleing
parents:
diff changeset
    24
c8cee17d7e50 Autosolve feature for detecting duplicate theorems; patch by Timothy Bourke
kleing
parents:
diff changeset
    25
  val auto = ref false;
c8cee17d7e50 Autosolve feature for detecting duplicate theorems; patch by Timothy Bourke
kleing
parents:
diff changeset
    26
  val auto_time_limit = ref 5000;
c8cee17d7e50 Autosolve feature for detecting duplicate theorems; patch by Timothy Bourke
kleing
parents:
diff changeset
    27
c8cee17d7e50 Autosolve feature for detecting duplicate theorems; patch by Timothy Bourke
kleing
parents:
diff changeset
    28
  fun seek_solution int state = let
c8cee17d7e50 Autosolve feature for detecting duplicate theorems; patch by Timothy Bourke
kleing
parents:
diff changeset
    29
      val ctxt = Proof.context_of state;
c8cee17d7e50 Autosolve feature for detecting duplicate theorems; patch by Timothy Bourke
kleing
parents:
diff changeset
    30
c8cee17d7e50 Autosolve feature for detecting duplicate theorems; patch by Timothy Bourke
kleing
parents:
diff changeset
    31
      fun conj_to_list [] = []
c8cee17d7e50 Autosolve feature for detecting duplicate theorems; patch by Timothy Bourke
kleing
parents:
diff changeset
    32
        | conj_to_list (t::ts) =
c8cee17d7e50 Autosolve feature for detecting duplicate theorems; patch by Timothy Bourke
kleing
parents:
diff changeset
    33
          (Conjunction.dest_conjunction t
c8cee17d7e50 Autosolve feature for detecting duplicate theorems; patch by Timothy Bourke
kleing
parents:
diff changeset
    34
           |> (fn (t1, t2) => conj_to_list (t1::t2::ts)))
c8cee17d7e50 Autosolve feature for detecting duplicate theorems; patch by Timothy Bourke
kleing
parents:
diff changeset
    35
          handle TERM _ => t::conj_to_list ts;
c8cee17d7e50 Autosolve feature for detecting duplicate theorems; patch by Timothy Bourke
kleing
parents:
diff changeset
    36
c8cee17d7e50 Autosolve feature for detecting duplicate theorems; patch by Timothy Bourke
kleing
parents:
diff changeset
    37
      val crits = [(true, FT.Solves)];
c8cee17d7e50 Autosolve feature for detecting duplicate theorems; patch by Timothy Bourke
kleing
parents:
diff changeset
    38
      fun find g = (NONE, FT.find_theorems ctxt g true crits);
c8cee17d7e50 Autosolve feature for detecting duplicate theorems; patch by Timothy Bourke
kleing
parents:
diff changeset
    39
      fun find_cterm g = (SOME g, FT.find_theorems ctxt
c8cee17d7e50 Autosolve feature for detecting duplicate theorems; patch by Timothy Bourke
kleing
parents:
diff changeset
    40
                                    (SOME (Goal.init g)) true crits);
c8cee17d7e50 Autosolve feature for detecting duplicate theorems; patch by Timothy Bourke
kleing
parents:
diff changeset
    41
c8cee17d7e50 Autosolve feature for detecting duplicate theorems; patch by Timothy Bourke
kleing
parents:
diff changeset
    42
      fun prt_result (goal, results) = let
c8cee17d7e50 Autosolve feature for detecting duplicate theorems; patch by Timothy Bourke
kleing
parents:
diff changeset
    43
          val msg = case goal of
c8cee17d7e50 Autosolve feature for detecting duplicate theorems; patch by Timothy Bourke
kleing
parents:
diff changeset
    44
                      NONE => "The current goal"
c8cee17d7e50 Autosolve feature for detecting duplicate theorems; patch by Timothy Bourke
kleing
parents:
diff changeset
    45
                    | SOME g => Syntax.string_of_term ctxt (term_of g);
c8cee17d7e50 Autosolve feature for detecting duplicate theorems; patch by Timothy Bourke
kleing
parents:
diff changeset
    46
        in
c8cee17d7e50 Autosolve feature for detecting duplicate theorems; patch by Timothy Bourke
kleing
parents:
diff changeset
    47
          Pretty.big_list (msg ^ " could be solved directly with:")
c8cee17d7e50 Autosolve feature for detecting duplicate theorems; patch by Timothy Bourke
kleing
parents:
diff changeset
    48
                          (map Display.pretty_fact results)
c8cee17d7e50 Autosolve feature for detecting duplicate theorems; patch by Timothy Bourke
kleing
parents:
diff changeset
    49
        end;
c8cee17d7e50 Autosolve feature for detecting duplicate theorems; patch by Timothy Bourke
kleing
parents:
diff changeset
    50
c8cee17d7e50 Autosolve feature for detecting duplicate theorems; patch by Timothy Bourke
kleing
parents:
diff changeset
    51
      fun seek_against_goal () = let
c8cee17d7e50 Autosolve feature for detecting duplicate theorems; patch by Timothy Bourke
kleing
parents:
diff changeset
    52
          val goal = try Proof.get_goal state
c8cee17d7e50 Autosolve feature for detecting duplicate theorems; patch by Timothy Bourke
kleing
parents:
diff changeset
    53
                     |> Option.map (#2 o #2);
c8cee17d7e50 Autosolve feature for detecting duplicate theorems; patch by Timothy Bourke
kleing
parents:
diff changeset
    54
c8cee17d7e50 Autosolve feature for detecting duplicate theorems; patch by Timothy Bourke
kleing
parents:
diff changeset
    55
          val goals = goal
c8cee17d7e50 Autosolve feature for detecting duplicate theorems; patch by Timothy Bourke
kleing
parents:
diff changeset
    56
                      |> Option.map (fn g => cprem_of g 1)
c8cee17d7e50 Autosolve feature for detecting duplicate theorems; patch by Timothy Bourke
kleing
parents:
diff changeset
    57
                      |> the_list
c8cee17d7e50 Autosolve feature for detecting duplicate theorems; patch by Timothy Bourke
kleing
parents:
diff changeset
    58
                      |> conj_to_list;
c8cee17d7e50 Autosolve feature for detecting duplicate theorems; patch by Timothy Bourke
kleing
parents:
diff changeset
    59
c8cee17d7e50 Autosolve feature for detecting duplicate theorems; patch by Timothy Bourke
kleing
parents:
diff changeset
    60
          val rs = if length goals = 1
c8cee17d7e50 Autosolve feature for detecting duplicate theorems; patch by Timothy Bourke
kleing
parents:
diff changeset
    61
                   then [find goal]
c8cee17d7e50 Autosolve feature for detecting duplicate theorems; patch by Timothy Bourke
kleing
parents:
diff changeset
    62
                   else map find_cterm goals;
c8cee17d7e50 Autosolve feature for detecting duplicate theorems; patch by Timothy Bourke
kleing
parents:
diff changeset
    63
          val frs = filter_out (null o snd) rs;
c8cee17d7e50 Autosolve feature for detecting duplicate theorems; patch by Timothy Bourke
kleing
parents:
diff changeset
    64
c8cee17d7e50 Autosolve feature for detecting duplicate theorems; patch by Timothy Bourke
kleing
parents:
diff changeset
    65
        in if null frs then NONE else SOME frs end;
c8cee17d7e50 Autosolve feature for detecting duplicate theorems; patch by Timothy Bourke
kleing
parents:
diff changeset
    66
c8cee17d7e50 Autosolve feature for detecting duplicate theorems; patch by Timothy Bourke
kleing
parents:
diff changeset
    67
      fun go () = let
c8cee17d7e50 Autosolve feature for detecting duplicate theorems; patch by Timothy Bourke
kleing
parents:
diff changeset
    68
          val res = TimeLimit.timeLimit
c8cee17d7e50 Autosolve feature for detecting duplicate theorems; patch by Timothy Bourke
kleing
parents:
diff changeset
    69
                      (Time.fromMilliseconds (!auto_time_limit))
c8cee17d7e50 Autosolve feature for detecting duplicate theorems; patch by Timothy Bourke
kleing
parents:
diff changeset
    70
                      (try seek_against_goal) ();
c8cee17d7e50 Autosolve feature for detecting duplicate theorems; patch by Timothy Bourke
kleing
parents:
diff changeset
    71
        in
c8cee17d7e50 Autosolve feature for detecting duplicate theorems; patch by Timothy Bourke
kleing
parents:
diff changeset
    72
          case Option.join res of
c8cee17d7e50 Autosolve feature for detecting duplicate theorems; patch by Timothy Bourke
kleing
parents:
diff changeset
    73
            NONE => state
c8cee17d7e50 Autosolve feature for detecting duplicate theorems; patch by Timothy Bourke
kleing
parents:
diff changeset
    74
          | SOME results => (Proof.goal_message
c8cee17d7e50 Autosolve feature for detecting duplicate theorems; patch by Timothy Bourke
kleing
parents:
diff changeset
    75
                              (fn () => Pretty.chunks [Pretty.str "",
c8cee17d7e50 Autosolve feature for detecting duplicate theorems; patch by Timothy Bourke
kleing
parents:
diff changeset
    76
                                Pretty.markup Markup.hilite
c8cee17d7e50 Autosolve feature for detecting duplicate theorems; patch by Timothy Bourke
kleing
parents:
diff changeset
    77
                                (Library.separate (Pretty.brk 0)
c8cee17d7e50 Autosolve feature for detecting duplicate theorems; patch by Timothy Bourke
kleing
parents:
diff changeset
    78
                                                  (map prt_result results))])
c8cee17d7e50 Autosolve feature for detecting duplicate theorems; patch by Timothy Bourke
kleing
parents:
diff changeset
    79
                                state)
c8cee17d7e50 Autosolve feature for detecting duplicate theorems; patch by Timothy Bourke
kleing
parents:
diff changeset
    80
        end handle TimeLimit.TimeOut => (warning "AutoSolve: timeout."; state);
c8cee17d7e50 Autosolve feature for detecting duplicate theorems; patch by Timothy Bourke
kleing
parents:
diff changeset
    81
    in
c8cee17d7e50 Autosolve feature for detecting duplicate theorems; patch by Timothy Bourke
kleing
parents:
diff changeset
    82
      if int andalso !auto andalso not (!Toplevel.quiet)
c8cee17d7e50 Autosolve feature for detecting duplicate theorems; patch by Timothy Bourke
kleing
parents:
diff changeset
    83
      then go ()
c8cee17d7e50 Autosolve feature for detecting duplicate theorems; patch by Timothy Bourke
kleing
parents:
diff changeset
    84
      else state
c8cee17d7e50 Autosolve feature for detecting duplicate theorems; patch by Timothy Bourke
kleing
parents:
diff changeset
    85
    end;
c8cee17d7e50 Autosolve feature for detecting duplicate theorems; patch by Timothy Bourke
kleing
parents:
diff changeset
    86
    
c8cee17d7e50 Autosolve feature for detecting duplicate theorems; patch by Timothy Bourke
kleing
parents:
diff changeset
    87
end;
c8cee17d7e50 Autosolve feature for detecting duplicate theorems; patch by Timothy Bourke
kleing
parents:
diff changeset
    88
c8cee17d7e50 Autosolve feature for detecting duplicate theorems; patch by Timothy Bourke
kleing
parents:
diff changeset
    89
val _ = Context.>> (Specification.add_theorem_hook AutoSolve.seek_solution);
c8cee17d7e50 Autosolve feature for detecting duplicate theorems; patch by Timothy Bourke
kleing
parents:
diff changeset
    90
c8cee17d7e50 Autosolve feature for detecting duplicate theorems; patch by Timothy Bourke
kleing
parents:
diff changeset
    91
val auto_solve = AutoSolve.auto;
c8cee17d7e50 Autosolve feature for detecting duplicate theorems; patch by Timothy Bourke
kleing
parents:
diff changeset
    92
val auto_solve_time_limit = AutoSolve.auto_time_limit;
c8cee17d7e50 Autosolve feature for detecting duplicate theorems; patch by Timothy Bourke
kleing
parents:
diff changeset
    93