src/HOL/ex/sledgehammer_tactics.ML
author wenzelm
Sat Apr 16 16:15:37 2011 +0200 (2011-04-16)
changeset 42361 23f352990944
parent 42106 ed1d40888b1b
child 42443 724e612ba248
permissions -rw-r--r--
modernized structure Proof_Context;
     1 (*  Title:      HOL/ex/sledgehammer_tactics.ML
     2     Author:     Jasmin Blanchette, TU Muenchen
     3     Copyright   2010, 2011
     4 
     5 Sledgehammer as a tactic.
     6 *)
     7 
     8 signature SLEDGEHAMMER_TACTICS =
     9 sig
    10   val sledgehammer_with_metis_tac : Proof.context -> int -> tactic
    11   val sledgehammer_as_unsound_oracle_tac : Proof.context -> int -> tactic
    12   val sledgehammer_as_oracle_tac : Proof.context -> int -> tactic
    13 end;
    14 
    15 structure Sledgehammer_Tactics : SLEDGEHAMMER_TACTICS =
    16 struct
    17 
    18 fun run_atp force_full_types timeout i n ctxt goal name =
    19   let
    20     val chained_ths = [] (* a tactic has no chained ths *)
    21     val params as {type_sys, relevance_thresholds, max_relevant, ...} =
    22       ((if force_full_types then [("full_types", "true")] else [])
    23        @ [("timeout", string_of_int (Time.toSeconds timeout))])
    24        (* @ [("overlord", "true")] *)
    25       |> Sledgehammer_Isar.default_params ctxt
    26     val prover = Sledgehammer_Provers.get_prover ctxt false name
    27     val default_max_relevant =
    28       Sledgehammer_Provers.default_max_relevant_for_prover ctxt name
    29     val is_built_in_const =
    30       Sledgehammer_Provers.is_built_in_const_for_prover ctxt name
    31     val relevance_fudge =
    32       Sledgehammer_Provers.relevance_fudge_for_prover ctxt name
    33     val relevance_override = {add = [], del = [], only = false}
    34     val (_, hyp_ts, concl_t) = Sledgehammer_Util.strip_subgoal goal i
    35     val no_dangerous_types =
    36       Sledgehammer_ATP_Translate.types_dangerous_types type_sys
    37     val facts =
    38       Sledgehammer_Filter.relevant_facts ctxt no_dangerous_types
    39           relevance_thresholds
    40           (the_default default_max_relevant max_relevant) is_built_in_const
    41           relevance_fudge relevance_override chained_ths hyp_ts concl_t
    42     val problem =
    43       {state = Proof.init ctxt, goal = goal, subgoal = i, subgoal_count = n,
    44        facts = map Sledgehammer_Provers.Untranslated_Fact facts,
    45        smt_filter = NONE}
    46   in
    47     (case prover params (K "") problem of
    48       {outcome = NONE, used_facts, ...} => used_facts |> map fst |> SOME
    49     | _ => NONE)
    50       handle ERROR message => (warning ("Error: " ^ message ^ "\n"); NONE)
    51   end
    52 
    53 val atp = "e" (* or "vampire" or "spass" etc. *)
    54 
    55 fun thms_of_name ctxt name =
    56   let
    57     val lex = Keyword.get_lexicons
    58     val get = maps (Proof_Context.get_fact ctxt o fst)
    59   in
    60     Source.of_string name
    61     |> Symbol.source
    62     |> Token.source {do_recover=SOME false} lex Position.start
    63     |> Token.source_proper
    64     |> Source.source Token.stopper (Parse_Spec.xthms1 >> get) NONE
    65     |> Source.exhaust
    66   end
    67 
    68 fun sledgehammer_with_metis_tac ctxt i th =
    69   let
    70     val timeout = Time.fromSeconds 30
    71   in
    72     case run_atp false timeout i i ctxt th atp of
    73       SOME facts =>
    74       Metis_Tactics.metis_tac ctxt (maps (thms_of_name ctxt) facts) i th
    75     | NONE => Seq.empty
    76   end
    77 
    78 fun generic_sledgehammer_as_oracle_tac force_full_types ctxt i th =
    79   let
    80     val thy = Proof_Context.theory_of ctxt
    81     val timeout = Time.fromSeconds 30
    82     val xs = run_atp force_full_types timeout i i ctxt th atp
    83   in if is_some xs then Skip_Proof.cheat_tac thy th else Seq.empty end
    84 
    85 val sledgehammer_as_unsound_oracle_tac =
    86   generic_sledgehammer_as_oracle_tac false
    87 val sledgehammer_as_oracle_tac = generic_sledgehammer_as_oracle_tac true
    88 
    89 end;