src/Tools/solve_direct.ML
author wenzelm
Thu, 18 Jul 2013 22:00:35 +0200
changeset 52701 51dfdcd88e84
parent 52645 e8c1c5612677
child 56467 8d7d6f17c6a7
permissions -rw-r--r--
guard unify tracing via visible status of global theory; find_theorems: back-patching of background theory to observe Context_Position.is_visible avoids spamming via auto solve_direct;
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 max_solutions: int Unsynchronized.ref
43025
5a0dec7bc099 handle non-auto try case gracefully in Solve Direct
blanchet
parents: 43024
diff changeset
    18
  val solve_direct: Proof.state -> bool * (string * Proof.state)
30980
fe0855471964 misc cleanup of auto_solve and quickcheck:
wenzelm
parents:
diff changeset
    19
end;
fe0855471964 misc cleanup of auto_solve and quickcheck:
wenzelm
parents:
diff changeset
    20
40130
db6e84082695 export main ML entry by default;
wenzelm
parents: 40129
diff changeset
    21
structure Solve_Direct: SOLVE_DIRECT =
30980
fe0855471964 misc cleanup of auto_solve and quickcheck:
wenzelm
parents:
diff changeset
    22
struct
fe0855471964 misc cleanup of auto_solve and quickcheck:
wenzelm
parents:
diff changeset
    23
43025
5a0dec7bc099 handle non-auto try case gracefully in Solve Direct
blanchet
parents: 43024
diff changeset
    24
datatype mode = Auto_Try | Try | Normal
5a0dec7bc099 handle non-auto try case gracefully in Solve Direct
blanchet
parents: 43024
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
52701
51dfdcd88e84 guard unify tracing via visible status of global theory;
wenzelm
parents: 52645
diff changeset
    32
30980
fe0855471964 misc cleanup of auto_solve and quickcheck:
wenzelm
parents:
diff changeset
    33
(* preferences *)
fe0855471964 misc cleanup of auto_solve and quickcheck:
wenzelm
parents:
diff changeset
    34
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 _ =
52639
df830310e550 system options for Isabelle/HOL proof tools;
wenzelm
parents: 52017
diff changeset
    38
  ProofGeneral.preference_option ProofGeneral.category_tracing
52645
e8c1c5612677 clarified some default options;
wenzelm
parents: 52643
diff changeset
    39
    NONE
52639
df830310e550 system options for Isabelle/HOL proof tools;
wenzelm
parents: 52017
diff changeset
    40
    @{option auto_solve_direct}
52017
bc0238c1f73a clarified preferences: "override" re-initialized on prover startup, and "default" sent to PG -- thus recover typical defaults like auto-quickcheck in PG 4.x;
wenzelm
parents: 52007
diff changeset
    41
    "auto-solve-direct"
bc0238c1f73a clarified preferences: "override" re-initialized on prover startup, and "default" sent to PG -- thus recover typical defaults like auto-quickcheck in PG 4.x;
wenzelm
parents: 52007
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
43025
5a0dec7bc099 handle non-auto try case gracefully in Solve Direct
blanchet
parents: 43024
diff changeset
    47
fun do_solve_direct mode 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;
52701
51dfdcd88e84 guard unify tracing via visible status of global theory;
wenzelm
parents: 52645
diff changeset
    50
    val find_ctxt = if mode = Auto_Try then Context_Position.set_visible false ctxt else ctxt;
30980
fe0855471964 misc cleanup of auto_solve and quickcheck:
wenzelm
parents:
diff changeset
    51
33301
1fe9fc908ec3 less hermetic ML;
wenzelm
parents: 33290
diff changeset
    52
    val crits = [(true, Find_Theorems.Solves)];
40129
0843888de43e observe Isabelle/ML coding standards;
wenzelm
parents: 40116
diff changeset
    53
    fun find g =
52701
51dfdcd88e84 guard unify tracing via visible status of global theory;
wenzelm
parents: 52645
diff changeset
    54
      snd (Find_Theorems.find_theorems find_ctxt (SOME g) (SOME (! max_solutions)) false crits);
30980
fe0855471964 misc cleanup of auto_solve and quickcheck:
wenzelm
parents:
diff changeset
    55
fe0855471964 misc cleanup of auto_solve and quickcheck:
wenzelm
parents:
diff changeset
    56
    fun prt_result (goal, results) =
fe0855471964 misc cleanup of auto_solve and quickcheck:
wenzelm
parents:
diff changeset
    57
      let
fe0855471964 misc cleanup of auto_solve and quickcheck:
wenzelm
parents:
diff changeset
    58
        val msg =
43025
5a0dec7bc099 handle non-auto try case gracefully in Solve Direct
blanchet
parents: 43024
diff changeset
    59
          (if mode = Auto_Try then "Auto " else "") ^ solve_directN ^ ": " ^
30980
fe0855471964 misc cleanup of auto_solve and quickcheck:
wenzelm
parents:
diff changeset
    60
          (case goal of
fe0855471964 misc cleanup of auto_solve and quickcheck:
wenzelm
parents:
diff changeset
    61
            NONE => "The current goal"
fe0855471964 misc cleanup of auto_solve and quickcheck:
wenzelm
parents:
diff changeset
    62
          | SOME sg => Syntax.string_of_term ctxt (Thm.term_of sg));
fe0855471964 misc cleanup of auto_solve and quickcheck:
wenzelm
parents:
diff changeset
    63
      in
fe0855471964 misc cleanup of auto_solve and quickcheck:
wenzelm
parents:
diff changeset
    64
        Pretty.big_list
40116
9ed3711366c8 introduced manual version of "Auto Solve" as "solve_direct"
blanchet
parents: 39616
diff changeset
    65
          (msg ^ " can be solved directly with")
33301
1fe9fc908ec3 less hermetic ML;
wenzelm
parents: 33290
diff changeset
    66
          (map (Find_Theorems.pretty_thm ctxt) results)
30980
fe0855471964 misc cleanup of auto_solve and quickcheck:
wenzelm
parents:
diff changeset
    67
      end;
fe0855471964 misc cleanup of auto_solve and quickcheck:
wenzelm
parents:
diff changeset
    68
fe0855471964 misc cleanup of auto_solve and quickcheck:
wenzelm
parents:
diff changeset
    69
    fun seek_against_goal () =
33290
6dcb0a970783 renamed Proof.flat_goal to Proof.simple_goal;
wenzelm
parents: 32966
diff changeset
    70
      (case try Proof.simple_goal state of
30980
fe0855471964 misc cleanup of auto_solve and quickcheck:
wenzelm
parents:
diff changeset
    71
        NONE => NONE
33290
6dcb0a970783 renamed Proof.flat_goal to Proof.simple_goal;
wenzelm
parents: 32966
diff changeset
    72
      | SOME {goal = st, ...} =>
30980
fe0855471964 misc cleanup of auto_solve and quickcheck:
wenzelm
parents:
diff changeset
    73
          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
    74
            val subgoals = Drule.strip_imp_prems (Thm.cprop_of st);
30980
fe0855471964 misc cleanup of auto_solve and quickcheck:
wenzelm
parents:
diff changeset
    75
            val rs =
fe0855471964 misc cleanup of auto_solve and quickcheck:
wenzelm
parents:
diff changeset
    76
              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
    77
              then [(NONE, find st)]
30980
fe0855471964 misc cleanup of auto_solve and quickcheck:
wenzelm
parents:
diff changeset
    78
              else map (fn sg => (SOME sg, find (Goal.init sg))) subgoals;
fe0855471964 misc cleanup of auto_solve and quickcheck:
wenzelm
parents:
diff changeset
    79
            val results = filter_out (null o snd) rs;
fe0855471964 misc cleanup of auto_solve and quickcheck:
wenzelm
parents:
diff changeset
    80
          in if null results then NONE else SOME results end);
40129
0843888de43e observe Isabelle/ML coding standards;
wenzelm
parents: 40116
diff changeset
    81
    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
    82
  in
9ed3711366c8 introduced manual version of "Auto Solve" as "solve_direct"
blanchet
parents: 39616
diff changeset
    83
    (case try seek_against_goal () of
9ed3711366c8 introduced manual version of "Auto Solve" as "solve_direct"
blanchet
parents: 39616
diff changeset
    84
      SOME (SOME results) =>
43020
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 43018
diff changeset
    85
        (someN,
40129
0843888de43e observe Isabelle/ML coding standards;
wenzelm
parents: 40116
diff changeset
    86
          state |>
43025
5a0dec7bc099 handle non-auto try case gracefully in Solve Direct
blanchet
parents: 43024
diff changeset
    87
            (if mode = Auto_Try then
5a0dec7bc099 handle non-auto try case gracefully in Solve Direct
blanchet
parents: 43024
diff changeset
    88
               Proof.goal_message
5a0dec7bc099 handle non-auto try case gracefully in Solve Direct
blanchet
parents: 43024
diff changeset
    89
                 (fn () =>
52643
34c29356930e more explicit Markup.information for messages produced by "auto" tools;
wenzelm
parents: 52641
diff changeset
    90
                   Pretty.markup Markup.information (message results))
43025
5a0dec7bc099 handle non-auto try case gracefully in Solve Direct
blanchet
parents: 43024
diff changeset
    91
             else
5a0dec7bc099 handle non-auto try case gracefully in Solve Direct
blanchet
parents: 43024
diff changeset
    92
               tap (fn _ =>
5a0dec7bc099 handle non-auto try case gracefully in Solve Direct
blanchet
parents: 43024
diff changeset
    93
                 Output.urgent_message (Pretty.string_of (Pretty.chunks (message results))))))
5a0dec7bc099 handle non-auto try case gracefully in Solve Direct
blanchet
parents: 43024
diff changeset
    94
    | SOME NONE =>
5a0dec7bc099 handle non-auto try case gracefully in Solve Direct
blanchet
parents: 43024
diff changeset
    95
        (if mode = Normal then Output.urgent_message "No proof found."
5a0dec7bc099 handle non-auto try case gracefully in Solve Direct
blanchet
parents: 43024
diff changeset
    96
         else ();
5a0dec7bc099 handle non-auto try case gracefully in Solve Direct
blanchet
parents: 43024
diff changeset
    97
         (noneN, state))
5a0dec7bc099 handle non-auto try case gracefully in Solve Direct
blanchet
parents: 43024
diff changeset
    98
    | NONE =>
5a0dec7bc099 handle non-auto try case gracefully in Solve Direct
blanchet
parents: 43024
diff changeset
    99
        (if mode = Normal then Output.urgent_message "An error occurred."
5a0dec7bc099 handle non-auto try case gracefully in Solve Direct
blanchet
parents: 43024
diff changeset
   100
         else ();
5a0dec7bc099 handle non-auto try case gracefully in Solve Direct
blanchet
parents: 43024
diff changeset
   101
         (unknownN, state)))
43020
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 43018
diff changeset
   102
  end
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 43018
diff changeset
   103
  |> `(fn (outcome_code, _) => outcome_code = someN);
30980
fe0855471964 misc cleanup of auto_solve and quickcheck:
wenzelm
parents:
diff changeset
   104
43025
5a0dec7bc099 handle non-auto try case gracefully in Solve Direct
blanchet
parents: 43024
diff changeset
   105
val solve_direct = do_solve_direct Normal
5a0dec7bc099 handle non-auto try case gracefully in Solve Direct
blanchet
parents: 43024
diff changeset
   106
40116
9ed3711366c8 introduced manual version of "Auto Solve" as "solve_direct"
blanchet
parents: 39616
diff changeset
   107
val _ =
46961
5c6955f487e5 outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents: 45666
diff changeset
   108
  Outer_Syntax.improper_command @{command_spec "solve_direct"}
5c6955f487e5 outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents: 45666
diff changeset
   109
    "try to solve conjectures directly with existing theorems"
51557
4e4b56b7a3a5 more robust access Toplevel.proof_of -- prefer warning via Toplevel.unknown_proof over hard crash (notably for skipped proofs);
wenzelm
parents: 50201
diff changeset
   110
    (Scan.succeed (Toplevel.unknown_proof o
4e4b56b7a3a5 more robust access Toplevel.proof_of -- prefer warning via Toplevel.unknown_proof over hard crash (notably for skipped proofs);
wenzelm
parents: 50201
diff changeset
   111
      Toplevel.keep (ignore o solve_direct o Toplevel.proof_of)));
40129
0843888de43e observe Isabelle/ML coding standards;
wenzelm
parents: 40116
diff changeset
   112
40116
9ed3711366c8 introduced manual version of "Auto Solve" as "solve_direct"
blanchet
parents: 39616
diff changeset
   113
9ed3711366c8 introduced manual version of "Auto Solve" as "solve_direct"
blanchet
parents: 39616
diff changeset
   114
(* hook *)
9ed3711366c8 introduced manual version of "Auto Solve" as "solve_direct"
blanchet
parents: 39616
diff changeset
   115
43025
5a0dec7bc099 handle non-auto try case gracefully in Solve Direct
blanchet
parents: 43024
diff changeset
   116
fun try_solve_direct auto = do_solve_direct (if auto then Auto_Try else Try)
5a0dec7bc099 handle non-auto try case gracefully in Solve Direct
blanchet
parents: 43024
diff changeset
   117
52641
c56b6fa636e8 hybrid "auto" tool setup, for TTY (within theory) and PIDE (global print function);
wenzelm
parents: 52639
diff changeset
   118
val _ = Try.tool_setup (solve_directN, (10, @{option auto_solve_direct}, try_solve_direct));
30980
fe0855471964 misc cleanup of auto_solve and quickcheck:
wenzelm
parents:
diff changeset
   119
fe0855471964 misc cleanup of auto_solve and quickcheck:
wenzelm
parents:
diff changeset
   120
end;