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