src/HOL/ex/sledgehammer_tactics.ML
author huffman
Fri Aug 19 14:17:28 2011 -0700 (2011-08-19)
changeset 44311 42c5cbf68052
parent 43351 b19d95b4d736
child 44390 99ef9fd7341b
permissions -rw-r--r--
Transcendental.thy: add tendsto_intros lemmas;
new isCont theorems;
simplify some proofs.
     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 {relevance_thresholds, max_relevant, slicing, ...} =
    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 =
    27       Sledgehammer_Provers.get_prover ctxt Sledgehammer_Provers.Normal name
    28     val default_max_relevant =
    29       Sledgehammer_Provers.default_max_relevant_for_prover ctxt slicing name
    30     val is_built_in_const =
    31       Sledgehammer_Provers.is_built_in_const_for_prover ctxt name
    32     val relevance_fudge =
    33       Sledgehammer_Provers.relevance_fudge_for_prover ctxt name
    34     val relevance_override = {add = [], del = [], only = false}
    35     val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal i
    36     val facts =
    37       Sledgehammer_Filter.nearly_all_facts ctxt relevance_override chained_ths
    38                                            hyp_ts concl_t
    39       |> Sledgehammer_Filter.relevant_facts ctxt 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 (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;