src/Tools/solve_direct.ML
author blanchet
Fri, 27 May 2011 10:30:08 +0200
changeset 43024 58150aa44941
parent 43020 abb5d1f907e4
child 43025 5a0dec7bc099
permissions -rw-r--r--
prioritize try and auto try's tools, with fast ones first, with a slight preference for provers vs. counterexample generators
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
40116
9ed3711366c8 introduced manual version of "Auto Solve" as "solve_direct"
blanchet
parents: 39616
diff changeset
     1
(*  Title:      Tools/solve_direct.ML
30980
fe0855471964 misc cleanup of auto_solve and quickcheck:
wenzelm
parents:
diff changeset
     2
    Author:     Timothy Bourke and Gerwin Klein, NICTA
fe0855471964 misc cleanup of auto_solve and quickcheck:
wenzelm
parents:
diff changeset
     3
fe0855471964 misc cleanup of auto_solve and quickcheck:
wenzelm
parents:
diff changeset
     4
Check whether a newly stated theorem can be solved directly by an
fe0855471964 misc cleanup of auto_solve and quickcheck:
wenzelm
parents:
diff changeset
     5
existing theorem.  Duplicate lemmas can be detected in this way.
fe0855471964 misc cleanup of auto_solve and quickcheck:
wenzelm
parents:
diff changeset
     6
39329
0a85f960ac50 make Auto Solve part of the "Auto Tools"
blanchet
parents: 39138
diff changeset
     7
The implementation relies critically on the Find_Theorems solves
30980
fe0855471964 misc cleanup of auto_solve and quickcheck:
wenzelm
parents:
diff changeset
     8
feature.
fe0855471964 misc cleanup of auto_solve and quickcheck:
wenzelm
parents:
diff changeset
     9
*)
fe0855471964 misc cleanup of auto_solve and quickcheck:
wenzelm
parents:
diff changeset
    10
40116
9ed3711366c8 introduced manual version of "Auto Solve" as "solve_direct"
blanchet
parents: 39616
diff changeset
    11
signature SOLVE_DIRECT =
30980
fe0855471964 misc cleanup of auto_solve and quickcheck:
wenzelm
parents:
diff changeset
    12
sig
43020
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 43018
diff changeset
    13
  val solve_directN: string
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 43018
diff changeset
    14
  val someN: string
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 43018
diff changeset
    15
  val noneN: string
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 43018
diff changeset
    16
  val unknownN: string
40130
db6e84082695 export main ML entry by default;
wenzelm
parents: 40129
diff changeset
    17
  val auto: bool Unsynchronized.ref
db6e84082695 export main ML entry by default;
wenzelm
parents: 40129
diff changeset
    18
  val max_solutions: int Unsynchronized.ref
43020
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 43018
diff changeset
    19
  val solve_direct: bool -> Proof.state -> bool * (string * Proof.state)
40130
db6e84082695 export main ML entry by default;
wenzelm
parents: 40129
diff changeset
    20
  val setup: theory -> theory
30980
fe0855471964 misc cleanup of auto_solve and quickcheck:
wenzelm
parents:
diff changeset
    21
end;
fe0855471964 misc cleanup of auto_solve and quickcheck:
wenzelm
parents:
diff changeset
    22
40130
db6e84082695 export main ML entry by default;
wenzelm
parents: 40129
diff changeset
    23
structure Solve_Direct: SOLVE_DIRECT =
30980
fe0855471964 misc cleanup of auto_solve and quickcheck:
wenzelm
parents:
diff changeset
    24
struct
fe0855471964 misc cleanup of auto_solve and quickcheck:
wenzelm
parents:
diff changeset
    25
40129
0843888de43e observe Isabelle/ML coding standards;
wenzelm
parents: 40116
diff changeset
    26
val solve_directN = "solve_direct";
0843888de43e observe Isabelle/ML coding standards;
wenzelm
parents: 40116
diff changeset
    27
43020
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 43018
diff changeset
    28
val someN = "some";
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 43018
diff changeset
    29
val noneN = "none";
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 43018
diff changeset
    30
val unknownN = "none";
40116
9ed3711366c8 introduced manual version of "Auto Solve" as "solve_direct"
blanchet
parents: 39616
diff changeset
    31
30980
fe0855471964 misc cleanup of auto_solve and quickcheck:
wenzelm
parents:
diff changeset
    32
(* preferences *)
fe0855471964 misc cleanup of auto_solve and quickcheck:
wenzelm
parents:
diff changeset
    33
32740
9dd0a2f83429 explicit indication of Unsynchronized.ref;
wenzelm
parents: 31007
diff changeset
    34
val auto = Unsynchronized.ref false;
39329
0a85f960ac50 make Auto Solve part of the "Auto Tools"
blanchet
parents: 39138
diff changeset
    35
val max_solutions = Unsynchronized.ref 5;
33889
4328de748fb2 some rearangement of load order to keep preferences adjacent -- slightly fragile;
wenzelm
parents: 33301
diff changeset
    36
4328de748fb2 some rearangement of load order to keep preferences adjacent -- slightly fragile;
wenzelm
parents: 33301
diff changeset
    37
val _ =
4328de748fb2 some rearangement of load order to keep preferences adjacent -- slightly fragile;
wenzelm
parents: 33301
diff changeset
    38
  ProofGeneralPgip.add_preference Preferences.category_tracing
39616
8052101883c3 renamed setmp_noncritical to Unsynchronized.setmp to emphasize its meaning;
wenzelm
parents: 39329
diff changeset
    39
  (Unsynchronized.setmp auto true (fn () =>
30980
fe0855471964 misc cleanup of auto_solve and quickcheck:
wenzelm
parents:
diff changeset
    40
    Preferences.bool_pref auto
40130
db6e84082695 export main ML entry by default;
wenzelm
parents: 40129
diff changeset
    41
      "auto-solve-direct"
40116
9ed3711366c8 introduced manual version of "Auto Solve" as "solve_direct"
blanchet
parents: 39616
diff changeset
    42
      ("Run " ^ quote solve_directN ^ " automatically.")) ());
30980
fe0855471964 misc cleanup of auto_solve and quickcheck:
wenzelm
parents:
diff changeset
    43
40129
0843888de43e observe Isabelle/ML coding standards;
wenzelm
parents: 40116
diff changeset
    44
0843888de43e observe Isabelle/ML coding standards;
wenzelm
parents: 40116
diff changeset
    45
(* solve_direct command *)
0843888de43e observe Isabelle/ML coding standards;
wenzelm
parents: 40116
diff changeset
    46
40116
9ed3711366c8 introduced manual version of "Auto Solve" as "solve_direct"
blanchet
parents: 39616
diff changeset
    47
fun solve_direct auto state =
30980
fe0855471964 misc cleanup of auto_solve and quickcheck:
wenzelm
parents:
diff changeset
    48
  let
fe0855471964 misc cleanup of auto_solve and quickcheck:
wenzelm
parents:
diff changeset
    49
    val ctxt = Proof.context_of state;
fe0855471964 misc cleanup of auto_solve and quickcheck:
wenzelm
parents:
diff changeset
    50
33301
1fe9fc908ec3 less hermetic ML;
wenzelm
parents: 33290
diff changeset
    51
    val crits = [(true, Find_Theorems.Solves)];
40129
0843888de43e observe Isabelle/ML coding standards;
wenzelm
parents: 40116
diff changeset
    52
    fun find g =
0843888de43e observe Isabelle/ML coding standards;
wenzelm
parents: 40116
diff changeset
    53
      snd (Find_Theorems.find_theorems ctxt (SOME g) (SOME (! max_solutions)) false crits);
30980
fe0855471964 misc cleanup of auto_solve and quickcheck:
wenzelm
parents:
diff changeset
    54
fe0855471964 misc cleanup of auto_solve and quickcheck:
wenzelm
parents:
diff changeset
    55
    fun prt_result (goal, results) =
fe0855471964 misc cleanup of auto_solve and quickcheck:
wenzelm
parents:
diff changeset
    56
      let
fe0855471964 misc cleanup of auto_solve and quickcheck:
wenzelm
parents:
diff changeset
    57
        val msg =
40116
9ed3711366c8 introduced manual version of "Auto Solve" as "solve_direct"
blanchet
parents: 39616
diff changeset
    58
          (if auto then "Auto " else "") ^ solve_directN ^ ": " ^
30980
fe0855471964 misc cleanup of auto_solve and quickcheck:
wenzelm
parents:
diff changeset
    59
          (case goal of
fe0855471964 misc cleanup of auto_solve and quickcheck:
wenzelm
parents:
diff changeset
    60
            NONE => "The current goal"
fe0855471964 misc cleanup of auto_solve and quickcheck:
wenzelm
parents:
diff changeset
    61
          | SOME sg => Syntax.string_of_term ctxt (Thm.term_of sg));
fe0855471964 misc cleanup of auto_solve and quickcheck:
wenzelm
parents:
diff changeset
    62
      in
fe0855471964 misc cleanup of auto_solve and quickcheck:
wenzelm
parents:
diff changeset
    63
        Pretty.big_list
40116
9ed3711366c8 introduced manual version of "Auto Solve" as "solve_direct"
blanchet
parents: 39616
diff changeset
    64
          (msg ^ " can be solved directly with")
33301
1fe9fc908ec3 less hermetic ML;
wenzelm
parents: 33290
diff changeset
    65
          (map (Find_Theorems.pretty_thm ctxt) results)
30980
fe0855471964 misc cleanup of auto_solve and quickcheck:
wenzelm
parents:
diff changeset
    66
      end;
fe0855471964 misc cleanup of auto_solve and quickcheck:
wenzelm
parents:
diff changeset
    67
fe0855471964 misc cleanup of auto_solve and quickcheck:
wenzelm
parents:
diff changeset
    68
    fun seek_against_goal () =
33290
6dcb0a970783 renamed Proof.flat_goal to Proof.simple_goal;
wenzelm
parents: 32966
diff changeset
    69
      (case try Proof.simple_goal state of
30980
fe0855471964 misc cleanup of auto_solve and quickcheck:
wenzelm
parents:
diff changeset
    70
        NONE => NONE
33290
6dcb0a970783 renamed Proof.flat_goal to Proof.simple_goal;
wenzelm
parents: 32966
diff changeset
    71
      | SOME {goal = st, ...} =>
30980
fe0855471964 misc cleanup of auto_solve and quickcheck:
wenzelm
parents:
diff changeset
    72
          let
32860
a4ab5d0cccd1 replaced Proof.get_goal state by Proof.flat_goal state, which provides the standard view on goals for (semi)automated tools;
wenzelm
parents: 32740
diff changeset
    73
            val subgoals = Drule.strip_imp_prems (Thm.cprop_of st);
30980
fe0855471964 misc cleanup of auto_solve and quickcheck:
wenzelm
parents:
diff changeset
    74
            val rs =
fe0855471964 misc cleanup of auto_solve and quickcheck:
wenzelm
parents:
diff changeset
    75
              if length subgoals = 1
32860
a4ab5d0cccd1 replaced Proof.get_goal state by Proof.flat_goal state, which provides the standard view on goals for (semi)automated tools;
wenzelm
parents: 32740
diff changeset
    76
              then [(NONE, find st)]
30980
fe0855471964 misc cleanup of auto_solve and quickcheck:
wenzelm
parents:
diff changeset
    77
              else map (fn sg => (SOME sg, find (Goal.init sg))) subgoals;
fe0855471964 misc cleanup of auto_solve and quickcheck:
wenzelm
parents:
diff changeset
    78
            val results = filter_out (null o snd) rs;
fe0855471964 misc cleanup of auto_solve and quickcheck:
wenzelm
parents:
diff changeset
    79
          in if null results then NONE else SOME results end);
40129
0843888de43e observe Isabelle/ML coding standards;
wenzelm
parents: 40116
diff changeset
    80
    fun message results = separate (Pretty.brk 0) (map prt_result results);
40116
9ed3711366c8 introduced manual version of "Auto Solve" as "solve_direct"
blanchet
parents: 39616
diff changeset
    81
  in
9ed3711366c8 introduced manual version of "Auto Solve" as "solve_direct"
blanchet
parents: 39616
diff changeset
    82
    (case try seek_against_goal () of
9ed3711366c8 introduced manual version of "Auto Solve" as "solve_direct"
blanchet
parents: 39616
diff changeset
    83
      SOME (SOME results) =>
43020
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 43018
diff changeset
    84
        (someN,
40129
0843888de43e observe Isabelle/ML coding standards;
wenzelm
parents: 40116
diff changeset
    85
          state |>
0843888de43e observe Isabelle/ML coding standards;
wenzelm
parents: 40116
diff changeset
    86
           (if auto then
0843888de43e observe Isabelle/ML coding standards;
wenzelm
parents: 40116
diff changeset
    87
             Proof.goal_message
0843888de43e observe Isabelle/ML coding standards;
wenzelm
parents: 40116
diff changeset
    88
               (fn () =>
0843888de43e observe Isabelle/ML coding standards;
wenzelm
parents: 40116
diff changeset
    89
                 Pretty.chunks
0843888de43e observe Isabelle/ML coding standards;
wenzelm
parents: 40116
diff changeset
    90
                  [Pretty.str "",
0843888de43e observe Isabelle/ML coding standards;
wenzelm
parents: 40116
diff changeset
    91
                   Pretty.markup Markup.hilite (message results)])
0843888de43e observe Isabelle/ML coding standards;
wenzelm
parents: 40116
diff changeset
    92
            else
0843888de43e observe Isabelle/ML coding standards;
wenzelm
parents: 40116
diff changeset
    93
              tap (fn _ =>
40132
7ee65dbffa31 renamed Output.priority to Output.urgent_message to emphasize its special role more clearly;
wenzelm
parents: 40130
diff changeset
    94
                Output.urgent_message (Pretty.string_of (Pretty.chunks (message results))))))
43020
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 43018
diff changeset
    95
    | SOME NONE => (noneN, state)
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 43018
diff changeset
    96
    | NONE => (unknownN, state))
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 43018
diff changeset
    97
  end
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 43018
diff changeset
    98
  |> `(fn (outcome_code, _) => outcome_code = someN);
30980
fe0855471964 misc cleanup of auto_solve and quickcheck:
wenzelm
parents:
diff changeset
    99
40116
9ed3711366c8 introduced manual version of "Auto Solve" as "solve_direct"
blanchet
parents: 39616
diff changeset
   100
val _ =
9ed3711366c8 introduced manual version of "Auto Solve" as "solve_direct"
blanchet
parents: 39616
diff changeset
   101
  Outer_Syntax.improper_command solve_directN
40129
0843888de43e observe Isabelle/ML coding standards;
wenzelm
parents: 40116
diff changeset
   102
    "try to solve conjectures directly with existing theorems" Keyword.diag
40130
db6e84082695 export main ML entry by default;
wenzelm
parents: 40129
diff changeset
   103
    (Scan.succeed
db6e84082695 export main ML entry by default;
wenzelm
parents: 40129
diff changeset
   104
      (Toplevel.keep (fn state => ignore (solve_direct false (Toplevel.proof_of state)))));
40129
0843888de43e observe Isabelle/ML coding standards;
wenzelm
parents: 40116
diff changeset
   105
40116
9ed3711366c8 introduced manual version of "Auto Solve" as "solve_direct"
blanchet
parents: 39616
diff changeset
   106
9ed3711366c8 introduced manual version of "Auto Solve" as "solve_direct"
blanchet
parents: 39616
diff changeset
   107
(* hook *)
9ed3711366c8 introduced manual version of "Auto Solve" as "solve_direct"
blanchet
parents: 39616
diff changeset
   108
43024
58150aa44941 prioritize try and auto try's tools, with fast ones first, with a slight preference for provers vs. counterexample generators
blanchet
parents: 43020
diff changeset
   109
val setup = Try.register_tool (solve_directN, (10, auto, solve_direct));
30980
fe0855471964 misc cleanup of auto_solve and quickcheck:
wenzelm
parents:
diff changeset
   110
fe0855471964 misc cleanup of auto_solve and quickcheck:
wenzelm
parents:
diff changeset
   111
end;