src/Tools/solve_direct.ML
author wenzelm
Mon, 25 Oct 2010 16:41:23 +0200
changeset 40129 0843888de43e
parent 40116 9ed3711366c8
child 40130 db6e84082695
permissions -rw-r--r--
observe Isabelle/ML coding standards;
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
32740
9dd0a2f83429 explicit indication of Unsynchronized.ref;
wenzelm
parents: 31007
diff changeset
    13
  val auto : bool Unsynchronized.ref
39329
0a85f960ac50 make Auto Solve part of the "Auto Tools"
blanchet
parents: 39138
diff changeset
    14
  val max_solutions : int Unsynchronized.ref
0a85f960ac50 make Auto Solve part of the "Auto Tools"
blanchet
parents: 39138
diff changeset
    15
  val setup : theory -> theory
30980
fe0855471964 misc cleanup of auto_solve and quickcheck:
wenzelm
parents:
diff changeset
    16
end;
fe0855471964 misc cleanup of auto_solve and quickcheck:
wenzelm
parents:
diff changeset
    17
40116
9ed3711366c8 introduced manual version of "Auto Solve" as "solve_direct"
blanchet
parents: 39616
diff changeset
    18
structure Solve_Direct : SOLVE_DIRECT =
30980
fe0855471964 misc cleanup of auto_solve and quickcheck:
wenzelm
parents:
diff changeset
    19
struct
fe0855471964 misc cleanup of auto_solve and quickcheck:
wenzelm
parents:
diff changeset
    20
40129
0843888de43e observe Isabelle/ML coding standards;
wenzelm
parents: 40116
diff changeset
    21
val solve_directN = "solve_direct";
0843888de43e observe Isabelle/ML coding standards;
wenzelm
parents: 40116
diff changeset
    22
40116
9ed3711366c8 introduced manual version of "Auto Solve" as "solve_direct"
blanchet
parents: 39616
diff changeset
    23
30980
fe0855471964 misc cleanup of auto_solve and quickcheck:
wenzelm
parents:
diff changeset
    24
(* preferences *)
fe0855471964 misc cleanup of auto_solve and quickcheck:
wenzelm
parents:
diff changeset
    25
32740
9dd0a2f83429 explicit indication of Unsynchronized.ref;
wenzelm
parents: 31007
diff changeset
    26
val auto = Unsynchronized.ref false;
39329
0a85f960ac50 make Auto Solve part of the "Auto Tools"
blanchet
parents: 39138
diff changeset
    27
val max_solutions = Unsynchronized.ref 5;
33889
4328de748fb2 some rearangement of load order to keep preferences adjacent -- slightly fragile;
wenzelm
parents: 33301
diff changeset
    28
4328de748fb2 some rearangement of load order to keep preferences adjacent -- slightly fragile;
wenzelm
parents: 33301
diff changeset
    29
val _ =
4328de748fb2 some rearangement of load order to keep preferences adjacent -- slightly fragile;
wenzelm
parents: 33301
diff changeset
    30
  ProofGeneralPgip.add_preference Preferences.category_tracing
39616
8052101883c3 renamed setmp_noncritical to Unsynchronized.setmp to emphasize its meaning;
wenzelm
parents: 39329
diff changeset
    31
  (Unsynchronized.setmp auto true (fn () =>
30980
fe0855471964 misc cleanup of auto_solve and quickcheck:
wenzelm
parents:
diff changeset
    32
    Preferences.bool_pref auto
40116
9ed3711366c8 introduced manual version of "Auto Solve" as "solve_direct"
blanchet
parents: 39616
diff changeset
    33
      ("Auto " ^ solve_directN)
9ed3711366c8 introduced manual version of "Auto Solve" as "solve_direct"
blanchet
parents: 39616
diff changeset
    34
      ("Run " ^ quote solve_directN ^ " automatically.")) ());
30980
fe0855471964 misc cleanup of auto_solve and quickcheck:
wenzelm
parents:
diff changeset
    35
40129
0843888de43e observe Isabelle/ML coding standards;
wenzelm
parents: 40116
diff changeset
    36
0843888de43e observe Isabelle/ML coding standards;
wenzelm
parents: 40116
diff changeset
    37
(* solve_direct command *)
0843888de43e observe Isabelle/ML coding standards;
wenzelm
parents: 40116
diff changeset
    38
40116
9ed3711366c8 introduced manual version of "Auto Solve" as "solve_direct"
blanchet
parents: 39616
diff changeset
    39
fun solve_direct auto state =
30980
fe0855471964 misc cleanup of auto_solve and quickcheck:
wenzelm
parents:
diff changeset
    40
  let
fe0855471964 misc cleanup of auto_solve and quickcheck:
wenzelm
parents:
diff changeset
    41
    val ctxt = Proof.context_of state;
fe0855471964 misc cleanup of auto_solve and quickcheck:
wenzelm
parents:
diff changeset
    42
33301
1fe9fc908ec3 less hermetic ML;
wenzelm
parents: 33290
diff changeset
    43
    val crits = [(true, Find_Theorems.Solves)];
40129
0843888de43e observe Isabelle/ML coding standards;
wenzelm
parents: 40116
diff changeset
    44
    fun find g =
0843888de43e observe Isabelle/ML coding standards;
wenzelm
parents: 40116
diff changeset
    45
      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
    46
fe0855471964 misc cleanup of auto_solve and quickcheck:
wenzelm
parents:
diff changeset
    47
    fun prt_result (goal, results) =
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 msg =
40116
9ed3711366c8 introduced manual version of "Auto Solve" as "solve_direct"
blanchet
parents: 39616
diff changeset
    50
          (if auto then "Auto " else "") ^ solve_directN ^ ": " ^
30980
fe0855471964 misc cleanup of auto_solve and quickcheck:
wenzelm
parents:
diff changeset
    51
          (case goal of
fe0855471964 misc cleanup of auto_solve and quickcheck:
wenzelm
parents:
diff changeset
    52
            NONE => "The current goal"
fe0855471964 misc cleanup of auto_solve and quickcheck:
wenzelm
parents:
diff changeset
    53
          | SOME sg => Syntax.string_of_term ctxt (Thm.term_of sg));
fe0855471964 misc cleanup of auto_solve and quickcheck:
wenzelm
parents:
diff changeset
    54
      in
fe0855471964 misc cleanup of auto_solve and quickcheck:
wenzelm
parents:
diff changeset
    55
        Pretty.big_list
40116
9ed3711366c8 introduced manual version of "Auto Solve" as "solve_direct"
blanchet
parents: 39616
diff changeset
    56
          (msg ^ " can be solved directly with")
33301
1fe9fc908ec3 less hermetic ML;
wenzelm
parents: 33290
diff changeset
    57
          (map (Find_Theorems.pretty_thm ctxt) results)
30980
fe0855471964 misc cleanup of auto_solve and quickcheck:
wenzelm
parents:
diff changeset
    58
      end;
fe0855471964 misc cleanup of auto_solve and quickcheck:
wenzelm
parents:
diff changeset
    59
fe0855471964 misc cleanup of auto_solve and quickcheck:
wenzelm
parents:
diff changeset
    60
    fun seek_against_goal () =
33290
6dcb0a970783 renamed Proof.flat_goal to Proof.simple_goal;
wenzelm
parents: 32966
diff changeset
    61
      (case try Proof.simple_goal state of
30980
fe0855471964 misc cleanup of auto_solve and quickcheck:
wenzelm
parents:
diff changeset
    62
        NONE => NONE
33290
6dcb0a970783 renamed Proof.flat_goal to Proof.simple_goal;
wenzelm
parents: 32966
diff changeset
    63
      | SOME {goal = st, ...} =>
30980
fe0855471964 misc cleanup of auto_solve and quickcheck:
wenzelm
parents:
diff changeset
    64
          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
    65
            val subgoals = Drule.strip_imp_prems (Thm.cprop_of st);
30980
fe0855471964 misc cleanup of auto_solve and quickcheck:
wenzelm
parents:
diff changeset
    66
            val rs =
fe0855471964 misc cleanup of auto_solve and quickcheck:
wenzelm
parents:
diff changeset
    67
              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
    68
              then [(NONE, find st)]
30980
fe0855471964 misc cleanup of auto_solve and quickcheck:
wenzelm
parents:
diff changeset
    69
              else map (fn sg => (SOME sg, find (Goal.init sg))) subgoals;
fe0855471964 misc cleanup of auto_solve and quickcheck:
wenzelm
parents:
diff changeset
    70
            val results = filter_out (null o snd) rs;
fe0855471964 misc cleanup of auto_solve and quickcheck:
wenzelm
parents:
diff changeset
    71
          in if null results then NONE else SOME results end);
40129
0843888de43e observe Isabelle/ML coding standards;
wenzelm
parents: 40116
diff changeset
    72
    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
    73
  in
9ed3711366c8 introduced manual version of "Auto Solve" as "solve_direct"
blanchet
parents: 39616
diff changeset
    74
    (case try seek_against_goal () of
9ed3711366c8 introduced manual version of "Auto Solve" as "solve_direct"
blanchet
parents: 39616
diff changeset
    75
      SOME (SOME results) =>
40129
0843888de43e observe Isabelle/ML coding standards;
wenzelm
parents: 40116
diff changeset
    76
        (true,
0843888de43e observe Isabelle/ML coding standards;
wenzelm
parents: 40116
diff changeset
    77
          state |>
0843888de43e observe Isabelle/ML coding standards;
wenzelm
parents: 40116
diff changeset
    78
           (if auto then
0843888de43e observe Isabelle/ML coding standards;
wenzelm
parents: 40116
diff changeset
    79
             Proof.goal_message
0843888de43e observe Isabelle/ML coding standards;
wenzelm
parents: 40116
diff changeset
    80
               (fn () =>
0843888de43e observe Isabelle/ML coding standards;
wenzelm
parents: 40116
diff changeset
    81
                 Pretty.chunks
0843888de43e observe Isabelle/ML coding standards;
wenzelm
parents: 40116
diff changeset
    82
                  [Pretty.str "",
0843888de43e observe Isabelle/ML coding standards;
wenzelm
parents: 40116
diff changeset
    83
                   Pretty.markup Markup.hilite (message results)])
0843888de43e observe Isabelle/ML coding standards;
wenzelm
parents: 40116
diff changeset
    84
            else
0843888de43e observe Isabelle/ML coding standards;
wenzelm
parents: 40116
diff changeset
    85
              tap (fn _ =>
0843888de43e observe Isabelle/ML coding standards;
wenzelm
parents: 40116
diff changeset
    86
                priority (Pretty.string_of (Pretty.chunks (message results))))))
40116
9ed3711366c8 introduced manual version of "Auto Solve" as "solve_direct"
blanchet
parents: 39616
diff changeset
    87
    | _ => (false, state))
9ed3711366c8 introduced manual version of "Auto Solve" as "solve_direct"
blanchet
parents: 39616
diff changeset
    88
  end;
30980
fe0855471964 misc cleanup of auto_solve and quickcheck:
wenzelm
parents:
diff changeset
    89
40129
0843888de43e observe Isabelle/ML coding standards;
wenzelm
parents: 40116
diff changeset
    90
val invoke_solve_direct = fst o solve_direct false;
39329
0a85f960ac50 make Auto Solve part of the "Auto Tools"
blanchet
parents: 39138
diff changeset
    91
40116
9ed3711366c8 introduced manual version of "Auto Solve" as "solve_direct"
blanchet
parents: 39616
diff changeset
    92
val _ =
9ed3711366c8 introduced manual version of "Auto Solve" as "solve_direct"
blanchet
parents: 39616
diff changeset
    93
  Outer_Syntax.improper_command solve_directN
40129
0843888de43e observe Isabelle/ML coding standards;
wenzelm
parents: 40116
diff changeset
    94
    "try to solve conjectures directly with existing theorems" Keyword.diag
0843888de43e observe Isabelle/ML coding standards;
wenzelm
parents: 40116
diff changeset
    95
    (Scan.succeed (Toplevel.keep (K () o invoke_solve_direct o Toplevel.proof_of)));
0843888de43e observe Isabelle/ML coding standards;
wenzelm
parents: 40116
diff changeset
    96
40116
9ed3711366c8 introduced manual version of "Auto Solve" as "solve_direct"
blanchet
parents: 39616
diff changeset
    97
9ed3711366c8 introduced manual version of "Auto Solve" as "solve_direct"
blanchet
parents: 39616
diff changeset
    98
(* hook *)
9ed3711366c8 introduced manual version of "Auto Solve" as "solve_direct"
blanchet
parents: 39616
diff changeset
    99
9ed3711366c8 introduced manual version of "Auto Solve" as "solve_direct"
blanchet
parents: 39616
diff changeset
   100
fun auto_solve_direct state =
40129
0843888de43e observe Isabelle/ML coding standards;
wenzelm
parents: 40116
diff changeset
   101
  if not (! auto) then (false, state) else solve_direct true state;
40116
9ed3711366c8 introduced manual version of "Auto Solve" as "solve_direct"
blanchet
parents: 39616
diff changeset
   102
40129
0843888de43e observe Isabelle/ML coding standards;
wenzelm
parents: 40116
diff changeset
   103
val setup = Auto_Tools.register_tool (solve_directN, auto_solve_direct);
30980
fe0855471964 misc cleanup of auto_solve and quickcheck:
wenzelm
parents:
diff changeset
   104
fe0855471964 misc cleanup of auto_solve and quickcheck:
wenzelm
parents:
diff changeset
   105
end;