src/Tools/solve_direct.ML
author wenzelm
Mon Mar 25 17:21:26 2019 +0100 (8 weeks ago)
changeset 69981 3dced198b9ec
parent 69593 3dda49e08b9d
permissions -rw-r--r--
more strict AFP properties;
blanchet@40116
     1
(*  Title:      Tools/solve_direct.ML
wenzelm@30980
     2
    Author:     Timothy Bourke and Gerwin Klein, NICTA
wenzelm@30980
     3
wenzelm@30980
     4
Check whether a newly stated theorem can be solved directly by an
wenzelm@30980
     5
existing theorem.  Duplicate lemmas can be detected in this way.
wenzelm@30980
     6
blanchet@39329
     7
The implementation relies critically on the Find_Theorems solves
wenzelm@30980
     8
feature.
wenzelm@30980
     9
*)
wenzelm@30980
    10
blanchet@40116
    11
signature SOLVE_DIRECT =
wenzelm@30980
    12
sig
blanchet@43020
    13
  val solve_directN: string
blanchet@43020
    14
  val someN: string
blanchet@43020
    15
  val noneN: string
blanchet@43020
    16
  val unknownN: string
haftmann@64012
    17
  val max_solutions: int Config.T
haftmann@64013
    18
  val strict_warnings: bool Config.T
wenzelm@58892
    19
  val solve_direct: Proof.state -> bool * (string * string list)
wenzelm@30980
    20
end;
wenzelm@30980
    21
wenzelm@40130
    22
structure Solve_Direct: SOLVE_DIRECT =
wenzelm@30980
    23
struct
wenzelm@30980
    24
blanchet@43025
    25
datatype mode = Auto_Try | Try | Normal
blanchet@43025
    26
wenzelm@40129
    27
val solve_directN = "solve_direct";
wenzelm@40129
    28
blanchet@43020
    29
val someN = "some";
blanchet@43020
    30
val noneN = "none";
blanchet@43020
    31
val unknownN = "none";
blanchet@40116
    32
wenzelm@52701
    33
wenzelm@30980
    34
(* preferences *)
wenzelm@30980
    35
wenzelm@67149
    36
val max_solutions = Attrib.setup_config_int \<^binding>\<open>solve_direct_max_solutions\<close> (K 5);
wenzelm@67149
    37
val strict_warnings = Attrib.setup_config_bool \<^binding>\<open>solve_direct_strict_warnings\<close> (K false);
wenzelm@33889
    38
wenzelm@40129
    39
wenzelm@40129
    40
(* solve_direct command *)
wenzelm@40129
    41
blanchet@43025
    42
fun do_solve_direct mode state =
wenzelm@30980
    43
  let
wenzelm@30980
    44
    val ctxt = Proof.context_of state;
wenzelm@30980
    45
wenzelm@64982
    46
    fun find goal =
wenzelm@64983
    47
      #2 (Find_Theorems.find_theorems ctxt (SOME goal)
wenzelm@64983
    48
        (SOME (Config.get ctxt max_solutions)) false [(true, Find_Theorems.Solves)]);
wenzelm@30980
    49
wenzelm@64985
    50
    fun prt_result (subgoal, results) =
wenzelm@64985
    51
      Pretty.big_list
wenzelm@64985
    52
        ((if mode = Auto_Try then "Auto " else "") ^ solve_directN ^ ": " ^
wenzelm@64985
    53
          (case subgoal of NONE => "the current goal" | SOME i => "subgoal #" ^ string_of_int i) ^
wenzelm@64985
    54
          " can be solved directly with")
wenzelm@64985
    55
        (map (Find_Theorems.pretty_thm ctxt) results);
wenzelm@30980
    56
wenzelm@30980
    57
    fun seek_against_goal () =
wenzelm@64984
    58
      (case try (#goal o Proof.simple_goal) state of
wenzelm@30980
    59
        NONE => NONE
wenzelm@64984
    60
      | SOME goal =>
wenzelm@30980
    61
          let
wenzelm@64982
    62
            val subgoals = Drule.strip_imp_prems (Thm.cprop_of goal);
wenzelm@30980
    63
            val rs =
wenzelm@30980
    64
              if length subgoals = 1
wenzelm@64982
    65
              then [(NONE, find goal)]
wenzelm@64985
    66
              else map_index (fn (i, sg) => (SOME (i + 1), find (Goal.init sg))) subgoals;
wenzelm@64982
    67
            val results = filter_out (null o #2) rs;
wenzelm@30980
    68
          in if null results then NONE else SOME results end);
blanchet@40116
    69
  in
blanchet@40116
    70
    (case try seek_against_goal () of
blanchet@40116
    71
      SOME (SOME results) =>
blanchet@43020
    72
        (someN,
haftmann@64013
    73
          let
wenzelm@64985
    74
            val chunks = separate (Pretty.str "") (map prt_result results);
wenzelm@64985
    75
            val msg = Pretty.string_of (Pretty.chunks chunks);
haftmann@64013
    76
          in
wenzelm@64982
    77
            if Config.get ctxt strict_warnings then (warning msg; [])
wenzelm@64982
    78
            else if mode = Auto_Try then [msg]
wenzelm@64982
    79
            else (writeln msg; [])
haftmann@64013
    80
          end)
blanchet@43025
    81
    | SOME NONE =>
wenzelm@64982
    82
        (if mode = Normal then writeln "No proof found" else ();
wenzelm@58892
    83
         (noneN, []))
blanchet@43025
    84
    | NONE =>
wenzelm@64982
    85
        (if mode = Normal then writeln "An error occurred" else ();
wenzelm@58892
    86
         (unknownN, [])))
blanchet@43020
    87
  end
blanchet@43020
    88
  |> `(fn (outcome_code, _) => outcome_code = someN);
wenzelm@30980
    89
blanchet@43025
    90
val solve_direct = do_solve_direct Normal
blanchet@43025
    91
blanchet@40116
    92
val _ =
wenzelm@67149
    93
  Outer_Syntax.command \<^command_keyword>\<open>solve_direct\<close>
wenzelm@46961
    94
    "try to solve conjectures directly with existing theorems"
wenzelm@60190
    95
    (Scan.succeed (Toplevel.keep_proof (ignore o solve_direct o Toplevel.proof_of)));
wenzelm@40129
    96
blanchet@40116
    97
blanchet@40116
    98
(* hook *)
blanchet@40116
    99
blanchet@43025
   100
fun try_solve_direct auto = do_solve_direct (if auto then Auto_Try else Try)
blanchet@43025
   101
wenzelm@64982
   102
val _ =
wenzelm@69593
   103
  Try.tool_setup (solve_directN, (10, \<^system_option>\<open>auto_solve_direct\<close>, try_solve_direct));
wenzelm@30980
   104
wenzelm@30980
   105
end;