src/HOL/TPTP/sledgehammer_tactics.ML
author wenzelm
Fri, 25 Apr 2014 23:29:54 +0200
changeset 56732 da3fefcb43c3
parent 55212 5832470d956e
child 57754 c822c1c069f8
permissions -rw-r--r--
modernized theory setup;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
47790
2e1636e45770 move file to where it belongs
blanchet
parents: 47773
diff changeset
     1
(*  Title:      HOL/TPTP/sledgehammer_tactics.ML
40633
6cd611ceb64e adding files to use sledgehammer as a tactic for non-interactive use
bulwahn
parents:
diff changeset
     2
    Author:     Jasmin Blanchette, TU Muenchen
42071
04577a7e0c51 move "TPTP" wrapper and "Sledgehammer as a tactic" to "HOL/ex"
blanchet
parents: 41959
diff changeset
     3
    Copyright   2010, 2011
40633
6cd611ceb64e adding files to use sledgehammer as a tactic for non-interactive use
bulwahn
parents:
diff changeset
     4
6cd611ceb64e adding files to use sledgehammer as a tactic for non-interactive use
bulwahn
parents:
diff changeset
     5
Sledgehammer as a tactic.
6cd611ceb64e adding files to use sledgehammer as a tactic for non-interactive use
bulwahn
parents:
diff changeset
     6
*)
6cd611ceb64e adding files to use sledgehammer as a tactic for non-interactive use
bulwahn
parents:
diff changeset
     7
6cd611ceb64e adding files to use sledgehammer as a tactic for non-interactive use
bulwahn
parents:
diff changeset
     8
signature SLEDGEHAMMER_TACTICS =
6cd611ceb64e adding files to use sledgehammer as a tactic for non-interactive use
bulwahn
parents:
diff changeset
     9
sig
48292
7fcee834c7f5 more code rationalization in relevance filter
blanchet
parents: 48289
diff changeset
    10
  type fact_override = Sledgehammer_Fact.fact_override
44462
d9a657c44380 more reliable "sledgehammer\_tac" reconstruction, by avoiding "insert_tac"
blanchet
parents: 44429
diff changeset
    11
44429
e5506cfe1b5a clean up Sledgehammer tactic
blanchet
parents: 44390
diff changeset
    12
  val sledgehammer_with_metis_tac :
48292
7fcee834c7f5 more code rationalization in relevance filter
blanchet
parents: 48289
diff changeset
    13
    Proof.context -> (string * string) list -> fact_override -> int -> tactic
44429
e5506cfe1b5a clean up Sledgehammer tactic
blanchet
parents: 44390
diff changeset
    14
  val sledgehammer_as_oracle_tac :
48292
7fcee834c7f5 more code rationalization in relevance filter
blanchet
parents: 48289
diff changeset
    15
    Proof.context -> (string * string) list -> fact_override -> int -> tactic
40633
6cd611ceb64e adding files to use sledgehammer as a tactic for non-interactive use
bulwahn
parents:
diff changeset
    16
end;
6cd611ceb64e adding files to use sledgehammer as a tactic for non-interactive use
bulwahn
parents:
diff changeset
    17
6cd611ceb64e adding files to use sledgehammer as a tactic for non-interactive use
bulwahn
parents:
diff changeset
    18
structure Sledgehammer_Tactics : SLEDGEHAMMER_TACTICS =
6cd611ceb64e adding files to use sledgehammer as a tactic for non-interactive use
bulwahn
parents:
diff changeset
    19
struct
42071
04577a7e0c51 move "TPTP" wrapper and "Sledgehammer as a tactic" to "HOL/ex"
blanchet
parents: 41959
diff changeset
    20
48299
5e5c6616f0fe centrally construct expensive data structures
blanchet
parents: 48293
diff changeset
    21
open Sledgehammer_Util
48287
61acb731b4a2 killed one file
blanchet
parents: 48250
diff changeset
    22
open Sledgehammer_Fact
55201
1ee776da8da7 renamed ML file
blanchet
parents: 55198
diff changeset
    23
open Sledgehammer_Prover
55212
blanchet
parents: 55205
diff changeset
    24
open Sledgehammer_Prover_ATP
55205
8450622db0c5 refactor large ML file
blanchet
parents: 55201
diff changeset
    25
open Sledgehammer_Prover_Minimize
48381
1b7d798460bb renamed ML structures
blanchet
parents: 48299
diff changeset
    26
open Sledgehammer_MaSh
55198
7a538e58b64e tuned ML file name
blanchet
parents: 54141
diff changeset
    27
open Sledgehammer_Commands
44462
d9a657c44380 more reliable "sledgehammer\_tac" reconstruction, by avoiding "insert_tac"
blanchet
parents: 44429
diff changeset
    28
48292
7fcee834c7f5 more code rationalization in relevance filter
blanchet
parents: 48289
diff changeset
    29
fun run_prover override_params fact_override i n ctxt goal =
40633
6cd611ceb64e adding files to use sledgehammer as a tactic for non-interactive use
bulwahn
parents:
diff changeset
    30
  let
55205
8450622db0c5 refactor large ML file
blanchet
parents: 55201
diff changeset
    31
    val thy = Proof_Context.theory_of ctxt
48299
5e5c6616f0fe centrally construct expensive data structures
blanchet
parents: 48293
diff changeset
    32
    val mode = Normal
55205
8450622db0c5 refactor large ML file
blanchet
parents: 55201
diff changeset
    33
    val params as {provers, max_facts, ...} = default_params thy override_params
44429
e5506cfe1b5a clean up Sledgehammer tactic
blanchet
parents: 44390
diff changeset
    34
    val name = hd provers
48299
5e5c6616f0fe centrally construct expensive data structures
blanchet
parents: 48293
diff changeset
    35
    val prover = get_prover ctxt mode name
54126
6675cdc0d1ae if slicing is disabled, pick the maximum number of facts, not the number of facts in the last slice
blanchet
parents: 52196
diff changeset
    36
    val default_max_facts = default_max_facts_of_prover ctxt name
52196
2281f33e8da6 redid rac7830871177 to avoid duplicate fixed variable (e.g. lemma "P (a::nat)" proof - have "!!a::int. Q a" sledgehammer [e])
blanchet
parents: 52125
diff changeset
    37
    val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal goal i ctxt
48299
5e5c6616f0fe centrally construct expensive data structures
blanchet
parents: 48293
diff changeset
    38
    val ho_atp = exists (is_ho_atp ctxt) provers
5e5c6616f0fe centrally construct expensive data structures
blanchet
parents: 48293
diff changeset
    39
    val reserved = reserved_isar_keyword_table ()
5e5c6616f0fe centrally construct expensive data structures
blanchet
parents: 48293
diff changeset
    40
    val css_table = clasimpset_rule_table_of ctxt
40921
a516fbdd9931 improving sledgehammer_tactic and adding relevance filtering to the tactic
bulwahn
parents: 40635
diff changeset
    41
    val facts =
54126
6675cdc0d1ae if slicing is disabled, pick the maximum number of facts, not the number of facts in the last slice
blanchet
parents: 52196
diff changeset
    42
      nearly_all_facts ctxt ho_atp fact_override reserved css_table [] hyp_ts concl_t
48299
5e5c6616f0fe centrally construct expensive data structures
blanchet
parents: 48293
diff changeset
    43
      |> relevant_facts ctxt params name
48293
914ca0827804 renamed Sledgehammer options
blanchet
parents: 48292
diff changeset
    44
             (the_default default_max_facts max_facts) fact_override hyp_ts
914ca0827804 renamed Sledgehammer options
blanchet
parents: 48292
diff changeset
    45
             concl_t
51010
afd0213a3dab tuned data structure
blanchet
parents: 51007
diff changeset
    46
      |> hd |> snd
40633
6cd611ceb64e adding files to use sledgehammer as a tactic for non-interactive use
bulwahn
parents:
diff changeset
    47
    val problem =
54141
f57f8e7a879f generate a comment storing the goal nickname in "learn_prover"
blanchet
parents: 54126
diff changeset
    48
      {comment = "", state = Proof.init ctxt, goal = goal, subgoal = i, subgoal_count = n,
51010
afd0213a3dab tuned data structure
blanchet
parents: 51007
diff changeset
    49
       factss = [("", facts)]}
40633
6cd611ceb64e adding files to use sledgehammer as a tactic for non-interactive use
bulwahn
parents:
diff changeset
    50
  in
45520
2b1dde0b1c30 thread in additional options to minimizer
blanchet
parents: 45514
diff changeset
    51
    (case prover params (K (K (K ""))) problem of
40921
a516fbdd9931 improving sledgehammer_tactic and adding relevance filtering to the tactic
bulwahn
parents: 40635
diff changeset
    52
      {outcome = NONE, used_facts, ...} => used_facts |> map fst |> SOME
a516fbdd9931 improving sledgehammer_tactic and adding relevance filtering to the tactic
bulwahn
parents: 40635
diff changeset
    53
    | _ => NONE)
51010
afd0213a3dab tuned data structure
blanchet
parents: 51007
diff changeset
    54
    handle ERROR message => (warning ("Error: " ^ message ^ "\n"); NONE)
40633
6cd611ceb64e adding files to use sledgehammer as a tactic for non-interactive use
bulwahn
parents:
diff changeset
    55
  end
6cd611ceb64e adding files to use sledgehammer as a tactic for non-interactive use
bulwahn
parents:
diff changeset
    56
48292
7fcee834c7f5 more code rationalization in relevance filter
blanchet
parents: 48289
diff changeset
    57
fun sledgehammer_with_metis_tac ctxt override_params fact_override i th =
7fcee834c7f5 more code rationalization in relevance filter
blanchet
parents: 48289
diff changeset
    58
  let val override_params = override_params @ [("preplay_timeout", "0")] in
7fcee834c7f5 more code rationalization in relevance filter
blanchet
parents: 48289
diff changeset
    59
    case run_prover override_params fact_override i i ctxt th of
47766
9f7cdd5fff7c more work on TPTP Isabelle and Sledgehammer tactics
blanchet
parents: 47532
diff changeset
    60
      SOME facts =>
9f7cdd5fff7c more work on TPTP Isabelle and Sledgehammer tactics
blanchet
parents: 47532
diff changeset
    61
      Metis_Tactic.metis_tac [] ATP_Problem_Generate.combs_or_liftingN ctxt
9f7cdd5fff7c more work on TPTP Isabelle and Sledgehammer tactics
blanchet
parents: 47532
diff changeset
    62
          (maps (thms_of_name ctxt) facts) i th
9f7cdd5fff7c more work on TPTP Isabelle and Sledgehammer tactics
blanchet
parents: 47532
diff changeset
    63
    | NONE => Seq.empty
9f7cdd5fff7c more work on TPTP Isabelle and Sledgehammer tactics
blanchet
parents: 47532
diff changeset
    64
  end
40633
6cd611ceb64e adding files to use sledgehammer as a tactic for non-interactive use
bulwahn
parents:
diff changeset
    65
48292
7fcee834c7f5 more code rationalization in relevance filter
blanchet
parents: 48289
diff changeset
    66
fun sledgehammer_as_oracle_tac ctxt override_params fact_override i th =
40633
6cd611ceb64e adding files to use sledgehammer as a tactic for non-interactive use
bulwahn
parents:
diff changeset
    67
  let
47766
9f7cdd5fff7c more work on TPTP Isabelle and Sledgehammer tactics
blanchet
parents: 47532
diff changeset
    68
    val override_params =
9f7cdd5fff7c more work on TPTP Isabelle and Sledgehammer tactics
blanchet
parents: 47532
diff changeset
    69
      override_params @
9f7cdd5fff7c more work on TPTP Isabelle and Sledgehammer tactics
blanchet
parents: 47532
diff changeset
    70
      [("preplay_timeout", "0"),
9f7cdd5fff7c more work on TPTP Isabelle and Sledgehammer tactics
blanchet
parents: 47532
diff changeset
    71
       ("minimize", "false")]
48292
7fcee834c7f5 more code rationalization in relevance filter
blanchet
parents: 48289
diff changeset
    72
    val xs = run_prover override_params fact_override i i ctxt th
51552
c713c9505f68 clarified Skip_Proof.cheat_tac: more standard tactic;
wenzelm
parents: 51010
diff changeset
    73
  in if is_some xs then ALLGOALS Skip_Proof.cheat_tac th else Seq.empty end
41357
ae76960d86a2 added "sledgehammer_tac" as possible reconstructor in Mirabelle
blanchet
parents: 41243
diff changeset
    74
40633
6cd611ceb64e adding files to use sledgehammer as a tactic for non-interactive use
bulwahn
parents:
diff changeset
    75
end;