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